----- Otter 3.2, August 2001 ----- The process was started by bezem on busk, Mon Dec 30 15:56:56 2002 The command was "/Home/busk/bezem/tar/otter-3.2/source/otter". The process ID is 14369. set(hyper_res). set(ur_res). set(prolog_style_variables). set(output_sequent). clear(print_kept). clear(print_given). clear(print_back_sub). assign(max_proofs,5). formula_list(sos). all X (X=X). all X Y (X=Y->Y=X). all X Y (X=Y->RR(X,Y)). all X Y Z (RR(X,Y)&RR(Y,Z)->RR(X,Z)). all X Y (RR(X,Y)->X=Y| (exists I (R(X,I)&RR(I,Y)))). all X Y Z (R(X,Y)&R(X,Z)-> (exists J (RR(Y,J)&RR(Z,J)))). -(all Y Z (RR(x,Y)&RR(x,Z)-> (exists J (RR(Y,J)&RR(Z,J))))). all X Y Z (R(x,X)&RR(X,Y)&RR(X,Z)-> (exists J (RR(Y,J)&RR(Z,J)))). end_of_list. -------> sos clausifies to: list(sos). 1 [] -> X=X. 2 [] X=Y -> Y=X. 3 [] X=Y -> RR(X,Y). 4 [] RR(X,Y), RR(Y,Z) -> RR(X,Z). 5 [] RR(X,Y) -> X=Y, R(X,$f1(X,Y)). 6 [] RR(X,Y) -> X=Y, RR($f1(X,Y),Y). 7 [] R(X,Y), R(X,Z) -> RR(Y,$f2(X,Y,Z)). 8 [] R(X,Y), R(X,Z) -> RR(Z,$f2(X,Y,Z)). 9 [] -> RR(x,$c2). 10 [] -> RR(x,$c1). 11 [] RR($c2,J), RR($c1,J) -> . 12 [] R(x,X), RR(X,Y), RR(X,Z) -> RR(Y,$f3(X,Y,Z)). 13 [] R(x,X), RR(X,Y), RR(X,Z) -> RR(Z,$f3(X,Y,Z)). end_of_list. ======= end of input processing ======= =========== start of search =========== ----> UNIT CONFLICT at 167.78 sec ----> 25720 [binary,25719.1,25291.1] -> . Length of proof is 22. Level of proof is 12. ---------------- PROOF ---------------- 1 [] -> X=X. 2 [] X=Y -> Y=X. 3 [] X=Y -> RR(X,Y). 4 [] RR(X,Y), RR(Y,Z) -> RR(X,Z). 5 [] RR(X,Y) -> X=Y, R(X,$f1(X,Y)). 6 [] RR(X,Y) -> X=Y, RR($f1(X,Y),Y). 7 [] R(X,Y), R(X,Z) -> RR(Y,$f2(X,Y,Z)). 8 [] R(X,Y), R(X,Z) -> RR(Z,$f2(X,Y,Z)). 9 [] -> RR(x,$c2). 10 [] -> RR(x,$c1). 11 [] RR($c2,J), RR($c1,J) -> . 12 [] R(x,X), RR(X,Y), RR(X,Z) -> RR(Y,$f3(X,Y,Z)). 13 [] R(x,X), RR(X,Y), RR(X,Z) -> RR(Z,$f3(X,Y,Z)). 14 [hyper,3,1] -> RR(A,A). 15 [ur,11,14] RR($c2,$c1) -> . 16 [ur,11,14] RR($c1,$c2) -> . 19 [ur,4,10,15] RR($c2,x) -> . 20 [ur,4,9,16] RR($c1,x) -> . 21 [ur,19,3] $c2=x -> . 22 [ur,20,3] $c1=x -> . 23 [ur,21,2] x=$c2 -> . 24 [ur,22,2] x=$c1 -> . 27 [ur,5,10,24] -> R(x,$f1(x,$c1)). 28 [ur,5,9,23] -> R(x,$f1(x,$c2)). 31 [ur,6,10,24] -> RR($f1(x,$c1),$c1). 32 [ur,6,9,23] -> RR($f1(x,$c2),$c2). 45 [hyper,7,27,28] -> RR($f1(x,$c1),$f2(x,$f1(x,$c1),$f1(x,$c2))). 48 [hyper,8,27,28] -> RR($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2))). 70 [hyper,12,28,48,32] -> RR($f2(x,$f1(x,$c1),$f1(x,$c2)),$f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2)). 477 [hyper,13,28,48,32] -> RR($c2,$f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2)). 24727 [hyper,70,4,45] -> RR($f1(x,$c1),$f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2)). 25185 [hyper,24727,13,27,31] -> RR($c1,$f3($f1(x,$c1),$f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2),$c1)). 25291 [hyper,24727,12,27,31] -> RR($f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2),$f3($f1(x,$c1),$f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2),$c1)). 25536 [ur,25185,11] RR($c2,$f3($f1(x,$c1),$f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2),$c1)) -> . 25719 [ur,25536,4,477] RR($f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2),$f3($f1(x,$c1),$f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2),$c1)) -> . 25720 [binary,25719.1,25291.1] -> . ------------ end of proof ------------- ----> UNIT CONFLICT at 168.98 sec ----> 25781 [binary,25780.1,25132.1] -> . Length of proof is 22. Level of proof is 12. ---------------- PROOF ---------------- 1 [] -> X=X. 2 [] X=Y -> Y=X. 3 [] X=Y -> RR(X,Y). 4 [] RR(X,Y), RR(Y,Z) -> RR(X,Z). 5 [] RR(X,Y) -> X=Y, R(X,$f1(X,Y)). 6 [] RR(X,Y) -> X=Y, RR($f1(X,Y),Y). 7 [] R(X,Y), R(X,Z) -> RR(Y,$f2(X,Y,Z)). 8 [] R(X,Y), R(X,Z) -> RR(Z,$f2(X,Y,Z)). 9 [] -> RR(x,$c2). 10 [] -> RR(x,$c1). 11 [] RR($c2,J), RR($c1,J) -> . 12 [] R(x,X), RR(X,Y), RR(X,Z) -> RR(Y,$f3(X,Y,Z)). 13 [] R(x,X), RR(X,Y), RR(X,Z) -> RR(Z,$f3(X,Y,Z)). 14 [hyper,3,1] -> RR(A,A). 15 [ur,11,14] RR($c2,$c1) -> . 16 [ur,11,14] RR($c1,$c2) -> . 19 [ur,4,10,15] RR($c2,x) -> . 20 [ur,4,9,16] RR($c1,x) -> . 21 [ur,19,3] $c2=x -> . 22 [ur,20,3] $c1=x -> . 23 [ur,21,2] x=$c2 -> . 24 [ur,22,2] x=$c1 -> . 27 [ur,5,10,24] -> R(x,$f1(x,$c1)). 28 [ur,5,9,23] -> R(x,$f1(x,$c2)). 31 [ur,6,10,24] -> RR($f1(x,$c1),$c1). 32 [ur,6,9,23] -> RR($f1(x,$c2),$c2). 45 [hyper,7,27,28] -> RR($f1(x,$c1),$f2(x,$f1(x,$c1),$f1(x,$c2))). 48 [hyper,8,27,28] -> RR($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2))). 70 [hyper,12,28,48,32] -> RR($f2(x,$f1(x,$c1),$f1(x,$c2)),$f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2)). 477 [hyper,13,28,48,32] -> RR($c2,$f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2)). 24727 [hyper,70,4,45] -> RR($f1(x,$c1),$f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2)). 25132 [hyper,24727,13,27,31] -> RR($f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2),$f3($f1(x,$c1),$c1,$f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2))). 25238 [hyper,24727,12,27,31] -> RR($c1,$f3($f1(x,$c1),$c1,$f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2))). 25606 [ur,25238,11] RR($c2,$f3($f1(x,$c1),$c1,$f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2))) -> . 25780 [ur,25606,4,477] RR($f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2),$f3($f1(x,$c1),$c1,$f3($f1(x,$c2),$f2(x,$f1(x,$c1),$f1(x,$c2)),$c2))) -> . 25781 [binary,25780.1,25132.1] -> . ------------ end of proof ------------- ----> UNIT CONFLICT at 180.46 sec ----> 27070 [binary,27069.1,26871.1] -> . Length of proof is 22. Level of proof is 12. ---------------- PROOF ---------------- 1 [] -> X=X. 2 [] X=Y -> Y=X. 3 [] X=Y -> RR(X,Y). 4 [] RR(X,Y), RR(Y,Z) -> RR(X,Z). 5 [] RR(X,Y) -> X=Y, R(X,$f1(X,Y)). 6 [] RR(X,Y) -> X=Y, RR($f1(X,Y),Y). 7 [] R(X,Y), R(X,Z) -> RR(Y,$f2(X,Y,Z)). 8 [] R(X,Y), R(X,Z) -> RR(Z,$f2(X,Y,Z)). 9 [] -> RR(x,$c2). 10 [] -> RR(x,$c1). 11 [] RR($c2,J), RR($c1,J) -> . 12 [] R(x,X), RR(X,Y), RR(X,Z) -> RR(Y,$f3(X,Y,Z)). 13 [] R(x,X), RR(X,Y), RR(X,Z) -> RR(Z,$f3(X,Y,Z)). 14 [hyper,3,1] -> RR(A,A). 15 [ur,11,14] RR($c2,$c1) -> . 16 [ur,11,14] RR($c1,$c2) -> . 19 [ur,4,10,15] RR($c2,x) -> . 20 [ur,4,9,16] RR($c1,x) -> . 21 [ur,19,3] $c2=x -> . 22 [ur,20,3] $c1=x -> . 23 [ur,21,2] x=$c2 -> . 24 [ur,22,2] x=$c1 -> . 27 [ur,5,10,24] -> R(x,$f1(x,$c1)). 28 [ur,5,9,23] -> R(x,$f1(x,$c2)). 31 [ur,6,10,24] -> RR($f1(x,$c1),$c1). 32 [ur,6,9,23] -> RR($f1(x,$c2),$c2). 44 [hyper,7,28,27] -> RR($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1))). 47 [hyper,8,28,27] -> RR($f1(x,$c1),$f2(x,$f1(x,$c2),$f1(x,$c1))). 75 [hyper,12,28,44,32] -> RR($f2(x,$f1(x,$c2),$f1(x,$c1)),$f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2)). 485 [hyper,13,28,44,32] -> RR($c2,$f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2)). 26593 [hyper,75,4,47] -> RR($f1(x,$c1),$f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2)). 26763 [hyper,26593,13,27,31] -> RR($c1,$f3($f1(x,$c1),$f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2),$c1)). 26871 [hyper,26593,12,27,31] -> RR($f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2),$f3($f1(x,$c1),$f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2),$c1)). 26889 [ur,26763,11] RR($c2,$f3($f1(x,$c1),$f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2),$c1)) -> . 27069 [ur,26889,4,485] RR($f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2),$f3($f1(x,$c1),$f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2),$c1)) -> . 27070 [binary,27069.1,26871.1] -> . ------------ end of proof ------------- ----> UNIT CONFLICT at 181.66 sec ----> 27131 [binary,27130.1,26709.1] -> . Length of proof is 22. Level of proof is 12. ---------------- PROOF ---------------- 1 [] -> X=X. 2 [] X=Y -> Y=X. 3 [] X=Y -> RR(X,Y). 4 [] RR(X,Y), RR(Y,Z) -> RR(X,Z). 5 [] RR(X,Y) -> X=Y, R(X,$f1(X,Y)). 6 [] RR(X,Y) -> X=Y, RR($f1(X,Y),Y). 7 [] R(X,Y), R(X,Z) -> RR(Y,$f2(X,Y,Z)). 8 [] R(X,Y), R(X,Z) -> RR(Z,$f2(X,Y,Z)). 9 [] -> RR(x,$c2). 10 [] -> RR(x,$c1). 11 [] RR($c2,J), RR($c1,J) -> . 12 [] R(x,X), RR(X,Y), RR(X,Z) -> RR(Y,$f3(X,Y,Z)). 13 [] R(x,X), RR(X,Y), RR(X,Z) -> RR(Z,$f3(X,Y,Z)). 14 [hyper,3,1] -> RR(A,A). 15 [ur,11,14] RR($c2,$c1) -> . 16 [ur,11,14] RR($c1,$c2) -> . 19 [ur,4,10,15] RR($c2,x) -> . 20 [ur,4,9,16] RR($c1,x) -> . 21 [ur,19,3] $c2=x -> . 22 [ur,20,3] $c1=x -> . 23 [ur,21,2] x=$c2 -> . 24 [ur,22,2] x=$c1 -> . 27 [ur,5,10,24] -> R(x,$f1(x,$c1)). 28 [ur,5,9,23] -> R(x,$f1(x,$c2)). 31 [ur,6,10,24] -> RR($f1(x,$c1),$c1). 32 [ur,6,9,23] -> RR($f1(x,$c2),$c2). 44 [hyper,7,28,27] -> RR($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1))). 47 [hyper,8,28,27] -> RR($f1(x,$c1),$f2(x,$f1(x,$c2),$f1(x,$c1))). 75 [hyper,12,28,44,32] -> RR($f2(x,$f1(x,$c2),$f1(x,$c1)),$f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2)). 485 [hyper,13,28,44,32] -> RR($c2,$f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2)). 26593 [hyper,75,4,47] -> RR($f1(x,$c1),$f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2)). 26709 [hyper,26593,13,27,31] -> RR($f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2),$f3($f1(x,$c1),$c1,$f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2))). 26817 [hyper,26593,12,27,31] -> RR($c1,$f3($f1(x,$c1),$c1,$f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2))). 26960 [ur,26817,11] RR($c2,$f3($f1(x,$c1),$c1,$f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2))) -> . 27130 [ur,26960,4,485] RR($f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2),$f3($f1(x,$c1),$c1,$f3($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c2))) -> . 27131 [binary,27130.1,26709.1] -> . ------------ end of proof ------------- ----> UNIT CONFLICT at 201.59 sec ----> 28329 [binary,28328.1,27876.1] -> . Length of proof is 22. Level of proof is 12. ---------------- PROOF ---------------- 1 [] -> X=X. 2 [] X=Y -> Y=X. 3 [] X=Y -> RR(X,Y). 4 [] RR(X,Y), RR(Y,Z) -> RR(X,Z). 5 [] RR(X,Y) -> X=Y, R(X,$f1(X,Y)). 6 [] RR(X,Y) -> X=Y, RR($f1(X,Y),Y). 7 [] R(X,Y), R(X,Z) -> RR(Y,$f2(X,Y,Z)). 8 [] R(X,Y), R(X,Z) -> RR(Z,$f2(X,Y,Z)). 9 [] -> RR(x,$c2). 10 [] -> RR(x,$c1). 11 [] RR($c2,J), RR($c1,J) -> . 12 [] R(x,X), RR(X,Y), RR(X,Z) -> RR(Y,$f3(X,Y,Z)). 13 [] R(x,X), RR(X,Y), RR(X,Z) -> RR(Z,$f3(X,Y,Z)). 14 [hyper,3,1] -> RR(A,A). 15 [ur,11,14] RR($c2,$c1) -> . 16 [ur,11,14] RR($c1,$c2) -> . 19 [ur,4,10,15] RR($c2,x) -> . 20 [ur,4,9,16] RR($c1,x) -> . 21 [ur,19,3] $c2=x -> . 22 [ur,20,3] $c1=x -> . 23 [ur,21,2] x=$c2 -> . 24 [ur,22,2] x=$c1 -> . 27 [ur,5,10,24] -> R(x,$f1(x,$c1)). 28 [ur,5,9,23] -> R(x,$f1(x,$c2)). 31 [ur,6,10,24] -> RR($f1(x,$c1),$c1). 32 [ur,6,9,23] -> RR($f1(x,$c2),$c2). 44 [hyper,7,28,27] -> RR($f1(x,$c2),$f2(x,$f1(x,$c2),$f1(x,$c1))). 47 [hyper,8,28,27] -> RR($f1(x,$c1),$f2(x,$f1(x,$c2),$f1(x,$c1))). 95 [hyper,12,27,47,31] -> RR($f2(x,$f1(x,$c2),$f1(x,$c1)),$f3($f1(x,$c1),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c1)). 548 [hyper,13,27,47,31] -> RR($c1,$f3($f1(x,$c1),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c1)). 27308 [hyper,95,4,44] -> RR($f1(x,$c2),$f3($f1(x,$c1),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c1)). 27770 [hyper,27308,13,28,32] -> RR($c2,$f3($f1(x,$c2),$f3($f1(x,$c1),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c1),$c2)). 27876 [hyper,27308,12,28,32] -> RR($f3($f1(x,$c1),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c1),$f3($f1(x,$c2),$f3($f1(x,$c1),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c1),$c2)). 28125 [ur,27770,11] RR($c1,$f3($f1(x,$c2),$f3($f1(x,$c1),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c1),$c2)) -> . 28328 [ur,28125,4,548] RR($f3($f1(x,$c1),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c1),$f3($f1(x,$c2),$f3($f1(x,$c1),$f2(x,$f1(x,$c2),$f1(x,$c1)),$c1),$c2)) -> . 28329 [binary,28328.1,27876.1] -> . ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 2100 clauses generated 52279 hyper_res generated 20348 ur_res generated 31931 demod & eval rewrites 0 clauses wt,lit,sk delete 0 tautologies deleted 0 clauses forward subsumed 23968 (subsumed by sos) 19659 unit deletions 0 factor simplifications 0 clauses kept 28311 new demodulators 0 empty clauses 5 clauses back demodulated 0 clauses back subsumed 568 usable size 2088 sos size 25668 demodulators size 0 passive size 0 hot size 0 Kbytes malloced 17563 ----------- times (seconds) ----------- user CPU time 201.59 (0 hr, 3 min, 21 sec) system CPU time 71.06 (0 hr, 1 min, 11 sec) wall-clock time 301 (0 hr, 5 min, 1 sec) input time 0.00 clausify time 0.00 pick given time 25.73 hyper_res time 2.03 ur_res time 12.56 pre_process time 103.94 renumber time 2.84 demod time 0.00 order equalities 0.00 unit deleletion 0.00 factor simplify 0.00 weigh cl time 0.00 hints keep time 0.00 sort lits time 0.00 forward subsume 4.16 delete cl time 0.89 keep cl time 7.74 hints time 0.78 print_cl time 0.00 conflict time 82.09 new demod time 0.00 post_process time 54.30 back demod time 0.00 back subsume 47.75 factor time 0.00 unindex time 5.60 That finishes the proof of the theorem. Process 14369 finished Mon Dec 30 16:01:57 2002