============================== Prover9 ===============================
Prover9 (64) version 2009-11A, November 2009.
Process 7784 was started by koen on vdheijden-arch,
Sat Jan 14 16:51:59 2017
The command was "prover9 -f logic_a.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file logic_a.in


formulas(sos).
a(x,x) = x.
a(x,y) = a(y,x).
a(x,a(y,z)) = a(a(x,y),z).
end_of_list.

formulas(goals).
(all p all q a(p,a(q,a(p,a(q,a(p,a(q,p)))))) = a(p,q)).
end_of_list.

============================== end of input ==========================

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:
1 (all p all q a(p,a(q,a(p,a(q,a(p,a(q,p)))))) = a(p,q)) # label(non_clause) # label(goal).  [goal].

============================== end of process non-clausal formulas ===

============================== PROCESS INITIAL CLAUSES ===============

% Clauses before input processing:

formulas(usable).
end_of_list.

formulas(sos).
a(x,x) = x.  [assumption].
a(x,y) = a(y,x).  [assumption].
a(x,a(y,z)) = a(a(x,y),z).  [assumption].
a(c1,a(c2,a(c1,a(c2,a(c1,a(c2,c1)))))) != a(c1,c2).  [deny(1)].
end_of_list.

formulas(demodulators).
end_of_list.

============================== PREDICATE ELIMINATION =================

No predicates eliminated.

============================== end predicate elimination =============

Auto_denials:  (no changes).

Term ordering decisions:
Predicate symbol precedence:  predicate_order([ = ]).
Function symbol precedence:  function_order([ c1, c2, a ]).
After inverse_order:  (no changes).
Unfolding symbols: (none).

Auto_inference settings:
  % set(paramodulation).  % (positive equality literals)

Auto_process settings:  (no changes).

kept:      2 a(x,x) = x.  [assumption].

% Operation a is commutative; C redundancy checks enabled.
kept:      3 a(x,y) = a(y,x).  [assumption].
           4 a(x,a(y,z)) = a(a(x,y),z).  [assumption].
kept:      5 a(a(x,y),z) = a(x,a(y,z)).  [copy(4),flip(a)].
           6 a(c1,a(c2,a(c1,a(c2,a(c1,a(c2,c1)))))) != a(c1,c2).  [deny(1)].
kept:      7 a(c1,a(c2,a(c1,a(c2,a(c1,a(c1,c2)))))) != a(c1,c2).  [copy(6),rewrite([3(8)])].

============================== end of process initial clauses ========

============================== CLAUSES FOR SEARCH ====================

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
2 a(x,x) = x.  [assumption].
3 a(x,y) = a(y,x).  [assumption].
5 a(a(x,y),z) = a(x,a(y,z)).  [copy(4),flip(a)].
7 a(c1,a(c2,a(c1,a(c2,a(c1,a(c1,c2)))))) != a(c1,c2).  [copy(6),rewrite([3(8)])].
end_of_list.

formulas(demodulators).
2 a(x,x) = x.  [assumption].
3 a(x,y) = a(y,x).  [assumption].
        % (lex-dep)
5 a(a(x,y),z) = a(x,a(y,z)).  [copy(4),flip(a)].
end_of_list.

============================== end of clauses for search =============

============================== SEARCH ================================

% Starting search at 0.02 seconds.

given #1 (I,wt=5): 2 a(x,x) = x.  [assumption].

given #2 (I,wt=7): 3 a(x,y) = a(y,x).  [assumption].

given #3 (I,wt=11): 5 a(a(x,y),z) = a(x,a(y,z)).  [copy(4),flip(a)].

% Operation a is associative-commutative; CAC redundancy checks enabled.

============================== PROOF =================================

% Proof 1 at 0.02 (+ 0.00) seconds.
% Length of proof is 10.
% Level of proof is 3.
% Maximum clause weight is 17.000.
% Given clauses 3.

1 (all p all q a(p,a(q,a(p,a(q,a(p,a(q,p)))))) = a(p,q)) # label(non_clause) # label(goal).  [goal].
2 a(x,x) = x.  [assumption].
3 a(x,y) = a(y,x).  [assumption].
4 a(x,a(y,z)) = a(a(x,y),z).  [assumption].
5 a(a(x,y),z) = a(x,a(y,z)).  [copy(4),flip(a)].
6 a(c1,a(c2,a(c1,a(c2,a(c1,a(c2,c1)))))) != a(c1,c2).  [deny(1)].
7 a(c1,a(c2,a(c1,a(c2,a(c1,a(c1,c2)))))) != a(c1,c2).  [copy(6),rewrite([3(8)])].
9 a(x,a(x,y)) = a(x,y).  [para(2(a,1),5(a,1,1)),flip(a)].
10 a(x,a(y,x)) = a(y,x).  [para(2(a,1),5(a,2,2)),rewrite([3(2)])].
13 $F.  [back_rewrite(7),rewrite([9(9),10(8),9(7),10(6),9(5)]),xx(a)].

============================== end of proof ==========================

============================== STATISTICS ============================

Given=3. Generated=27. Kept=9. proofs=1.
Usable=3. Sos=1. Demods=8. Limbo=4, Disabled=5. Hints=0.
Kept_by_rule=0, Deleted_by_rule=0.
Forward_subsumed=17. Back_subsumed=0.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=8 (3 lex), Back_demodulated=1. Back_unit_deleted=0.
Demod_attempts=222. Demod_rewrites=33.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=0.05.
User_CPU=0.02, System_CPU=0.00, Wall_clock=0.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 7784 exit (max_proofs) Sat Jan 14 16:51:59 2017