----- Otter 3.2, August 2001 ----- The process was started by bezem on busk, Mon Dec 30 15:04:48 2002 The command was "/Home/busk/bezem/tar/otter-3.2/source/otter". The process ID is 14222. 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 E(X,X). all X Y (E(X,Y)->E(Y,X)). all X Y Z (E(X,Y)&E(Y,Z)->E(X,Z)). all X Y (E(X,Y)->S(X,Y)). all X Y (R(X,Y)->S(X,Y)). all X Y Z (S(X,Y)&S(Y,Z)->S(X,Z)). all X Y (S(X,Y)->E(X,Y)| (exists I (R(X,I)&S(I,Y)))). all X Y Z (R(X,Y)&R(X,Z)-> (exists J (S(Y,J)&S(Z,J)))). all X Y Z (R(a,X)&S(X,Y)&S(X,Z)-> (exists J (S(Y,J)&S(Z,J)))). S(a,b). S(a,c). -(exists J (S(b,J)&S(c,J))). end_of_list. -------> sos clausifies to: list(sos). 1 [] -> E(X,X). 2 [] E(X,Y) -> E(Y,X). 3 [] E(X,Y), E(Y,Z) -> E(X,Z). 4 [] E(X,Y) -> S(X,Y). 5 [] R(X,Y) -> S(X,Y). 6 [] S(X,Y), S(Y,Z) -> S(X,Z). 7 [] S(X,Y) -> E(X,Y), R(X,$f1(X,Y)). 8 [] S(X,Y) -> E(X,Y), S($f1(X,Y),Y). 9 [] R(X,Y), R(X,Z) -> S(Y,$f2(X,Y,Z)). 10 [] R(X,Y), R(X,Z) -> S(Z,$f2(X,Y,Z)). 11 [] R(a,X), S(X,Y), S(X,Z) -> S(Y,$f3(X,Y,Z)). 12 [] R(a,X), S(X,Y), S(X,Z) -> S(Z,$f3(X,Y,Z)). 13 [] -> S(a,b). 14 [] -> S(a,c). 15 [] S(b,J), S(c,J) -> . end_of_list. ======= end of input processing ======= =========== start of search =========== ----> UNIT CONFLICT at 594.93 sec ----> 49790 [binary,49789.1,41386.1] -> . Length of proof is 22. Level of proof is 12. ---------------- PROOF ---------------- 1 [] -> E(X,X). 2 [] E(X,Y) -> E(Y,X). 4 [] E(X,Y) -> S(X,Y). 6 [] S(X,Y), S(Y,Z) -> S(X,Z). 7 [] S(X,Y) -> E(X,Y), R(X,$f1(X,Y)). 8 [] S(X,Y) -> E(X,Y), S($f1(X,Y),Y). 9 [] R(X,Y), R(X,Z) -> S(Y,$f2(X,Y,Z)). 10 [] R(X,Y), R(X,Z) -> S(Z,$f2(X,Y,Z)). 11 [] R(a,X), S(X,Y), S(X,Z) -> S(Y,$f3(X,Y,Z)). 12 [] R(a,X), S(X,Y), S(X,Z) -> S(Z,$f3(X,Y,Z)). 13 [] -> S(a,b). 14 [] -> S(a,c). 15 [] S(b,J), S(c,J) -> . 16 [hyper,4,1] -> S(A,A). 17 [ur,15,16] S(b,c) -> . 18 [ur,15,16] S(c,b) -> . 23 [ur,6,14,17] S(b,a) -> . 24 [ur,6,13,18] S(c,a) -> . 26 [ur,23,4] E(b,a) -> . 28 [ur,24,4] E(c,a) -> . 29 [ur,26,2] E(a,b) -> . 30 [ur,28,2] E(a,c) -> . 33 [ur,7,14,30] -> R(a,$f1(a,c)). 34 [ur,7,13,29] -> R(a,$f1(a,b)). 43 [ur,8,14,30] -> S($f1(a,c),c). 44 [ur,8,13,29] -> S($f1(a,b),b). 59 [hyper,9,33,34] -> S($f1(a,c),$f2(a,$f1(a,c),$f1(a,b))). 62 [hyper,10,33,34] -> S($f1(a,b),$f2(a,$f1(a,c),$f1(a,b))). 179 [hyper,11,34,62,44] -> S($f2(a,$f1(a,c),$f1(a,b)),$f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b)). 733 [hyper,12,34,62,44] -> S(b,$f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b)). 37426 [hyper,179,6,59] -> S($f1(a,c),$f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b)). 41242 [hyper,37426,12,33,43] -> S(c,$f3($f1(a,c),$f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b),c)). 41386 [hyper,37426,11,33,43] -> S($f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b),$f3($f1(a,c),$f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b),c)). 49252 [ur,41242,15] S(b,$f3($f1(a,c),$f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b),c)) -> . 49789 [ur,49252,6,733] S($f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b),$f3($f1(a,c),$f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b),c)) -> . 49790 [binary,49789.1,41386.1] -> . ------------ end of proof ------------- ----> UNIT CONFLICT at 597.30 sec ----> 49854 [binary,49853.1,41170.1] -> . Length of proof is 22. Level of proof is 12. ---------------- PROOF ---------------- 1 [] -> E(X,X). 2 [] E(X,Y) -> E(Y,X). 4 [] E(X,Y) -> S(X,Y). 6 [] S(X,Y), S(Y,Z) -> S(X,Z). 7 [] S(X,Y) -> E(X,Y), R(X,$f1(X,Y)). 8 [] S(X,Y) -> E(X,Y), S($f1(X,Y),Y). 9 [] R(X,Y), R(X,Z) -> S(Y,$f2(X,Y,Z)). 10 [] R(X,Y), R(X,Z) -> S(Z,$f2(X,Y,Z)). 11 [] R(a,X), S(X,Y), S(X,Z) -> S(Y,$f3(X,Y,Z)). 12 [] R(a,X), S(X,Y), S(X,Z) -> S(Z,$f3(X,Y,Z)). 13 [] -> S(a,b). 14 [] -> S(a,c). 15 [] S(b,J), S(c,J) -> . 16 [hyper,4,1] -> S(A,A). 17 [ur,15,16] S(b,c) -> . 18 [ur,15,16] S(c,b) -> . 23 [ur,6,14,17] S(b,a) -> . 24 [ur,6,13,18] S(c,a) -> . 26 [ur,23,4] E(b,a) -> . 28 [ur,24,4] E(c,a) -> . 29 [ur,26,2] E(a,b) -> . 30 [ur,28,2] E(a,c) -> . 33 [ur,7,14,30] -> R(a,$f1(a,c)). 34 [ur,7,13,29] -> R(a,$f1(a,b)). 43 [ur,8,14,30] -> S($f1(a,c),c). 44 [ur,8,13,29] -> S($f1(a,b),b). 59 [hyper,9,33,34] -> S($f1(a,c),$f2(a,$f1(a,c),$f1(a,b))). 62 [hyper,10,33,34] -> S($f1(a,b),$f2(a,$f1(a,c),$f1(a,b))). 179 [hyper,11,34,62,44] -> S($f2(a,$f1(a,c),$f1(a,b)),$f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b)). 733 [hyper,12,34,62,44] -> S(b,$f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b)). 37426 [hyper,179,6,59] -> S($f1(a,c),$f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b)). 41170 [hyper,37426,12,33,43] -> S($f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b),$f3($f1(a,c),c,$f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b))). 41314 [hyper,37426,11,33,43] -> S(c,$f3($f1(a,c),c,$f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b))). 49325 [ur,41314,15] S(b,$f3($f1(a,c),c,$f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b))) -> . 49853 [ur,49325,6,733] S($f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b),$f3($f1(a,c),c,$f3($f1(a,b),$f2(a,$f1(a,c),$f1(a,b)),b))) -> . 49854 [binary,49853.1,41170.1] -> . ------------ end of proof ------------- ----> UNIT CONFLICT at 926.25 sec ----> 71604 [binary,71603.1,71389.1] -> . Length of proof is 22. Level of proof is 12. ---------------- PROOF ---------------- 1 [] -> E(X,X). 2 [] E(X,Y) -> E(Y,X). 4 [] E(X,Y) -> S(X,Y). 6 [] S(X,Y), S(Y,Z) -> S(X,Z). 7 [] S(X,Y) -> E(X,Y), R(X,$f1(X,Y)). 8 [] S(X,Y) -> E(X,Y), S($f1(X,Y),Y). 9 [] R(X,Y), R(X,Z) -> S(Y,$f2(X,Y,Z)). 10 [] R(X,Y), R(X,Z) -> S(Z,$f2(X,Y,Z)). 11 [] R(a,X), S(X,Y), S(X,Z) -> S(Y,$f3(X,Y,Z)). 12 [] R(a,X), S(X,Y), S(X,Z) -> S(Z,$f3(X,Y,Z)). 13 [] -> S(a,b). 14 [] -> S(a,c). 15 [] S(b,J), S(c,J) -> . 16 [hyper,4,1] -> S(A,A). 17 [ur,15,16] S(b,c) -> . 18 [ur,15,16] S(c,b) -> . 23 [ur,6,14,17] S(b,a) -> . 24 [ur,6,13,18] S(c,a) -> . 26 [ur,23,4] E(b,a) -> . 28 [ur,24,4] E(c,a) -> . 29 [ur,26,2] E(a,b) -> . 30 [ur,28,2] E(a,c) -> . 33 [ur,7,14,30] -> R(a,$f1(a,c)). 34 [ur,7,13,29] -> R(a,$f1(a,b)). 43 [ur,8,14,30] -> S($f1(a,c),c). 44 [ur,8,13,29] -> S($f1(a,b),b). 58 [hyper,9,34,33] -> S($f1(a,b),$f2(a,$f1(a,b),$f1(a,c))). 61 [hyper,10,34,33] -> S($f1(a,c),$f2(a,$f1(a,b),$f1(a,c))). 185 [hyper,11,34,58,44] -> S($f2(a,$f1(a,b),$f1(a,c)),$f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b)). 742 [hyper,12,34,58,44] -> S(b,$f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b)). 70813 [hyper,185,6,61] -> S($f1(a,c),$f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b)). 71145 [hyper,70813,12,33,43] -> S(c,$f3($f1(a,c),$f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b),c)). 71389 [hyper,70813,11,33,43] -> S($f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b),$f3($f1(a,c),$f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b),c)). 71420 [ur,71145,15] S(b,$f3($f1(a,c),$f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b),c)) -> . 71603 [ur,71420,6,742] S($f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b),$f3($f1(a,c),$f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b),c)) -> . 71604 [binary,71603.1,71389.1] -> . ------------ end of proof ------------- ----> UNIT CONFLICT at 929.96 sec ----> 71668 [binary,71667.1,71023.1] -> . Length of proof is 22. Level of proof is 12. ---------------- PROOF ---------------- 1 [] -> E(X,X). 2 [] E(X,Y) -> E(Y,X). 4 [] E(X,Y) -> S(X,Y). 6 [] S(X,Y), S(Y,Z) -> S(X,Z). 7 [] S(X,Y) -> E(X,Y), R(X,$f1(X,Y)). 8 [] S(X,Y) -> E(X,Y), S($f1(X,Y),Y). 9 [] R(X,Y), R(X,Z) -> S(Y,$f2(X,Y,Z)). 10 [] R(X,Y), R(X,Z) -> S(Z,$f2(X,Y,Z)). 11 [] R(a,X), S(X,Y), S(X,Z) -> S(Y,$f3(X,Y,Z)). 12 [] R(a,X), S(X,Y), S(X,Z) -> S(Z,$f3(X,Y,Z)). 13 [] -> S(a,b). 14 [] -> S(a,c). 15 [] S(b,J), S(c,J) -> . 16 [hyper,4,1] -> S(A,A). 17 [ur,15,16] S(b,c) -> . 18 [ur,15,16] S(c,b) -> . 23 [ur,6,14,17] S(b,a) -> . 24 [ur,6,13,18] S(c,a) -> . 26 [ur,23,4] E(b,a) -> . 28 [ur,24,4] E(c,a) -> . 29 [ur,26,2] E(a,b) -> . 30 [ur,28,2] E(a,c) -> . 33 [ur,7,14,30] -> R(a,$f1(a,c)). 34 [ur,7,13,29] -> R(a,$f1(a,b)). 43 [ur,8,14,30] -> S($f1(a,c),c). 44 [ur,8,13,29] -> S($f1(a,b),b). 58 [hyper,9,34,33] -> S($f1(a,b),$f2(a,$f1(a,b),$f1(a,c))). 61 [hyper,10,34,33] -> S($f1(a,c),$f2(a,$f1(a,b),$f1(a,c))). 185 [hyper,11,34,58,44] -> S($f2(a,$f1(a,b),$f1(a,c)),$f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b)). 742 [hyper,12,34,58,44] -> S(b,$f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b)). 70813 [hyper,185,6,61] -> S($f1(a,c),$f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b)). 71023 [hyper,70813,12,33,43] -> S($f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b),$f3($f1(a,c),c,$f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b))). 71267 [hyper,70813,11,33,43] -> S(c,$f3($f1(a,c),c,$f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b))). 71494 [ur,71267,15] S(b,$f3($f1(a,c),c,$f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b))) -> . 71667 [ur,71494,6,742] S($f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b),$f3($f1(a,c),c,$f3($f1(a,b),$f2(a,$f1(a,b),$f1(a,c)),b))) -> . 71668 [binary,71667.1,71023.1] -> . ------------ end of proof ------------- ----> UNIT CONFLICT at 1632.77 sec ----> 86805 [binary,86804.1,76849.1] -> . Length of proof is 22. Level of proof is 12. ---------------- PROOF ---------------- 1 [] -> E(X,X). 2 [] E(X,Y) -> E(Y,X). 4 [] E(X,Y) -> S(X,Y). 6 [] S(X,Y), S(Y,Z) -> S(X,Z). 7 [] S(X,Y) -> E(X,Y), R(X,$f1(X,Y)). 8 [] S(X,Y) -> E(X,Y), S($f1(X,Y),Y). 9 [] R(X,Y), R(X,Z) -> S(Y,$f2(X,Y,Z)). 10 [] R(X,Y), R(X,Z) -> S(Z,$f2(X,Y,Z)). 11 [] R(a,X), S(X,Y), S(X,Z) -> S(Y,$f3(X,Y,Z)). 12 [] R(a,X), S(X,Y), S(X,Z) -> S(Z,$f3(X,Y,Z)). 13 [] -> S(a,b). 14 [] -> S(a,c). 15 [] S(b,J), S(c,J) -> . 16 [hyper,4,1] -> S(A,A). 17 [ur,15,16] S(b,c) -> . 18 [ur,15,16] S(c,b) -> . 23 [ur,6,14,17] S(b,a) -> . 24 [ur,6,13,18] S(c,a) -> . 26 [ur,23,4] E(b,a) -> . 28 [ur,24,4] E(c,a) -> . 29 [ur,26,2] E(a,b) -> . 30 [ur,28,2] E(a,c) -> . 33 [ur,7,14,30] -> R(a,$f1(a,c)). 34 [ur,7,13,29] -> R(a,$f1(a,b)). 43 [ur,8,14,30] -> S($f1(a,c),c). 44 [ur,8,13,29] -> S($f1(a,b),b). 58 [hyper,9,34,33] -> S($f1(a,b),$f2(a,$f1(a,b),$f1(a,c))). 61 [hyper,10,34,33] -> S($f1(a,c),$f2(a,$f1(a,b),$f1(a,c))). 215 [hyper,11,33,61,43] -> S($f2(a,$f1(a,b),$f1(a,c)),$f3($f1(a,c),$f2(a,$f1(a,b),$f1(a,c)),c)). 822 [hyper,12,33,61,43] -> S(c,$f3($f1(a,c),$f2(a,$f1(a,b),$f1(a,c)),c)). 72393 [hyper,215,6,58] -> S($f1(a,b),$f3($f1(a,c),$f2(a,$f1(a,b),$f1(a,c)),c)). 76697 [hyper,72393,12,34,44] -> S(b,$f3($f1(a,b),$f3($f1(a,c),$f2(a,$f1(a,b),$f1(a,c)),c),b)). 76849 [hyper,72393,11,34,44] -> S($f3($f1(a,c),$f2(a,$f1(a,b),$f1(a,c)),c),$f3($f1(a,b),$f3($f1(a,c),$f2(a,$f1(a,b),$f1(a,c)),c),b)). 86159 [ur,76697,15] S(c,$f3($f1(a,b),$f3($f1(a,c),$f2(a,$f1(a,b),$f1(a,c)),c),b)) -> . 86804 [ur,86159,6,822] S($f3($f1(a,c),$f2(a,$f1(a,b),$f1(a,c)),c),$f3($f1(a,b),$f3($f1(a,c),$f2(a,$f1(a,b),$f1(a,c)),c),b)) -> . 86805 [binary,86804.1,76849.1] -> . ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 4063 clauses generated 148493 hyper_res generated 73914 ur_res generated 74579 demod & eval rewrites 0 clauses wt,lit,sk delete 0 tautologies deleted 0 clauses forward subsumed 61708 (subsumed by sos) 51326 unit deletions 0 factor simplifications 0 clauses kept 86785 new demodulators 0 empty clauses 5 clauses back demodulated 0 clauses back subsumed 4228 usable size 4017 sos size 78555 demodulators size 0 passive size 0 hot size 0 Kbytes malloced 56873 ----------- times (seconds) ----------- user CPU time 1632.77 (0 hr, 27 min, 12 sec) system CPU time 212.68 (0 hr, 3 min, 32 sec) wall-clock time 1927 (0 hr, 32 min, 7 sec) input time 0.00 clausify time 0.00 pick given time 109.88 hyper_res time 7.52 ur_res time 56.77 pre_process time 609.37 renumber time 7.99 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 153.14 delete cl time 2.51 keep cl time 34.41 hints time 1.97 print_cl time 0.00 conflict time 392.46 new demod time 0.00 post_process time 841.02 back demod time 0.00 back subsume 429.39 factor time 0.00 unindex time 408.87 That finishes the proof of the theorem. Process 14222 finished Mon Dec 30 15:36:55 2002