----- Otter 3.2, August 2001 ----- The process was started by bezem on busk, Mon Jul 1 16:57:44 2002 The command was "/Home/busk/bezem/tar/otter-3.2/source/otter". The process ID is 247. 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->RR1(X,Y)). all X Y (X=Y->RR2(X,Y)). all X Y Z (RR1(X,Y)&RR1(Y,Z)->RR1(X,Z)). all X Y Z (RR2(X,Y)&RR2(Y,Z)->RR2(X,Z)). all X Y (RR1(X,Y)->X=Y| (exists I (R1(X,I)&RR1(I,Y)))). all X Y (RR2(X,Y)->X=Y| (exists I (R2(X,I)&RR2(I,Y)))). all X Y Z (R1(X,Y)&R2(X,Z)-> (exists J (RR2(Y,J)&RR1(Z,J)))). all X Y Z ((R1(x,X)|R2(x,X))&RR1(X,Y)&RR2(X,Z)-> (exists J (RR2(Y,J)&RR1(Z,J)))). -(all Z Y (RR1(x,Y)&RR2(x,Z)-> (exists J (RR2(Y,J)&RR1(Z,J))))). end_of_list. -------> sos clausifies to: list(sos). 1 [] -> X=X. 2 [] X=Y -> Y=X. 3 [] X=Y -> RR1(X,Y). 4 [] X=Y -> RR2(X,Y). 5 [] RR1(X,Y), RR1(Y,Z) -> RR1(X,Z). 6 [] RR2(X,Y), RR2(Y,Z) -> RR2(X,Z). 7 [] RR1(X,Y) -> X=Y, R1(X,$f1(X,Y)). 8 [] RR1(X,Y) -> X=Y, RR1($f1(X,Y),Y). 9 [] RR2(X,Y) -> X=Y, R2(X,$f2(X,Y)). 10 [] RR2(X,Y) -> X=Y, RR2($f2(X,Y),Y). 11 [] R1(X,Y), R2(X,Z) -> RR2(Y,$f3(X,Y,Z)). 12 [] R1(X,Y), R2(X,Z) -> RR1(Z,$f3(X,Y,Z)). 13 [] R1(x,X), RR1(X,Y), RR2(X,Z) -> RR2(Y,$f4(X,Y,Z)). 14 [] R1(x,X), RR1(X,Y), RR2(X,Z) -> RR1(Z,$f4(X,Y,Z)). 15 [] R2(x,X), RR1(X,Y), RR2(X,Z) -> RR2(Y,$f4(X,Y,Z)). 16 [] R2(x,X), RR1(X,Y), RR2(X,Z) -> RR1(Z,$f4(X,Y,Z)). 17 [] -> RR1(x,$c1). 18 [] -> RR2(x,$c2). 19 [] RR2($c1,J), RR1($c2,J) -> . end_of_list. ======= end of input processing ======= =========== start of search =========== ----> UNIT CONFLICT at 0.49 sec ----> 375 [binary,374.1,347.1] -> . Length of proof is 23. Level of proof is 12. ---------------- PROOF ---------------- 1 [] -> X=X. 2 [] X=Y -> Y=X. 3 [] X=Y -> RR1(X,Y). 4 [] X=Y -> RR2(X,Y). 5 [] RR1(X,Y), RR1(Y,Z) -> RR1(X,Z). 6 [] RR2(X,Y), RR2(Y,Z) -> RR2(X,Z). 7 [] RR1(X,Y) -> X=Y, R1(X,$f1(X,Y)). 8 [] RR1(X,Y) -> X=Y, RR1($f1(X,Y),Y). 9 [] RR2(X,Y) -> X=Y, R2(X,$f2(X,Y)). 10 [] RR2(X,Y) -> X=Y, RR2($f2(X,Y),Y). 11 [] R1(X,Y), R2(X,Z) -> RR2(Y,$f3(X,Y,Z)). 12 [] R1(X,Y), R2(X,Z) -> RR1(Z,$f3(X,Y,Z)). 13 [] R1(x,X), RR1(X,Y), RR2(X,Z) -> RR2(Y,$f4(X,Y,Z)). 14 [] R1(x,X), RR1(X,Y), RR2(X,Z) -> RR1(Z,$f4(X,Y,Z)). 15 [] R2(x,X), RR1(X,Y), RR2(X,Z) -> RR2(Y,$f4(X,Y,Z)). 16 [] R2(x,X), RR1(X,Y), RR2(X,Z) -> RR1(Z,$f4(X,Y,Z)). 17 [] -> RR1(x,$c1). 18 [] -> RR2(x,$c2). 19 [] RR2($c1,J), RR1($c2,J) -> . 20 [hyper,3,1] -> RR1(A,A). 21 [hyper,4,1] -> RR2(A,A). 22 [ur,19,20] RR2($c1,$c2) -> . 23 [ur,19,21] RR1($c2,$c1) -> . 26 [ur,5,17,23] RR1($c2,x) -> . 27 [ur,26,3] $c2=x -> . 28 [ur,27,2] x=$c2 -> . 29 [ur,6,18,22] RR2($c1,x) -> . 30 [ur,29,4] $c1=x -> . 31 [ur,30,2] x=$c1 -> . 33 [ur,7,17,31] -> R1(x,$f1(x,$c1)). 35 [ur,8,17,31] -> RR1($f1(x,$c1),$c1). 42 [ur,9,18,28] -> R2(x,$f2(x,$c2)). 44 [ur,10,18,28] -> RR2($f2(x,$c2),$c2). 50 [hyper,11,33,42] -> RR2($f1(x,$c1),$f3(x,$f1(x,$c1),$f2(x,$c2))). 51 [hyper,12,33,42] -> RR1($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2))). 60 [hyper,13,33,35,50] -> RR2($c1,$f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2)))). 81 [hyper,14,33,35,50] -> RR1($f3(x,$f1(x,$c1),$f2(x,$c2)),$f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2)))). 306 [hyper,81,5,51] -> RR1($f2(x,$c2),$f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2)))). 341 [hyper,306,16,42,44] -> RR1($c2,$f4($f2(x,$c2),$f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2))),$c2)). 347 [hyper,306,15,42,44] -> RR2($f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2))),$f4($f2(x,$c2),$f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2))),$c2)). 363 [ur,341,19] RR2($c1,$f4($f2(x,$c2),$f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2))),$c2)) -> . 374 [ur,363,6,60] RR2($f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2))),$f4($f2(x,$c2),$f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2))),$c2)) -> . 375 [binary,374.1,347.1] -> . ------------ end of proof ------------- ----> UNIT CONFLICT at 0.58 sec ----> 472 [binary,471.1,434.1] -> . Length of proof is 23. Level of proof is 12. ---------------- PROOF ---------------- 1 [] -> X=X. 2 [] X=Y -> Y=X. 3 [] X=Y -> RR1(X,Y). 4 [] X=Y -> RR2(X,Y). 5 [] RR1(X,Y), RR1(Y,Z) -> RR1(X,Z). 6 [] RR2(X,Y), RR2(Y,Z) -> RR2(X,Z). 7 [] RR1(X,Y) -> X=Y, R1(X,$f1(X,Y)). 8 [] RR1(X,Y) -> X=Y, RR1($f1(X,Y),Y). 9 [] RR2(X,Y) -> X=Y, R2(X,$f2(X,Y)). 10 [] RR2(X,Y) -> X=Y, RR2($f2(X,Y),Y). 11 [] R1(X,Y), R2(X,Z) -> RR2(Y,$f3(X,Y,Z)). 12 [] R1(X,Y), R2(X,Z) -> RR1(Z,$f3(X,Y,Z)). 13 [] R1(x,X), RR1(X,Y), RR2(X,Z) -> RR2(Y,$f4(X,Y,Z)). 14 [] R1(x,X), RR1(X,Y), RR2(X,Z) -> RR1(Z,$f4(X,Y,Z)). 15 [] R2(x,X), RR1(X,Y), RR2(X,Z) -> RR2(Y,$f4(X,Y,Z)). 16 [] R2(x,X), RR1(X,Y), RR2(X,Z) -> RR1(Z,$f4(X,Y,Z)). 17 [] -> RR1(x,$c1). 18 [] -> RR2(x,$c2). 19 [] RR2($c1,J), RR1($c2,J) -> . 20 [hyper,3,1] -> RR1(A,A). 21 [hyper,4,1] -> RR2(A,A). 22 [ur,19,20] RR2($c1,$c2) -> . 23 [ur,19,21] RR1($c2,$c1) -> . 26 [ur,5,17,23] RR1($c2,x) -> . 27 [ur,26,3] $c2=x -> . 28 [ur,27,2] x=$c2 -> . 29 [ur,6,18,22] RR2($c1,x) -> . 30 [ur,29,4] $c1=x -> . 31 [ur,30,2] x=$c1 -> . 33 [ur,7,17,31] -> R1(x,$f1(x,$c1)). 35 [ur,8,17,31] -> RR1($f1(x,$c1),$c1). 42 [ur,9,18,28] -> R2(x,$f2(x,$c2)). 44 [ur,10,18,28] -> RR2($f2(x,$c2),$c2). 50 [hyper,11,33,42] -> RR2($f1(x,$c1),$f3(x,$f1(x,$c1),$f2(x,$c2))). 51 [hyper,12,33,42] -> RR1($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2))). 102 [hyper,15,42,51,44] -> RR2($f3(x,$f1(x,$c1),$f2(x,$c2)),$f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$c2)). 116 [hyper,16,42,51,44] -> RR1($c2,$f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$c2)). 398 [hyper,102,6,50] -> RR2($f1(x,$c1),$f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$c2)). 434 [hyper,398,14,33,35] -> RR1($f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$c2),$f4($f1(x,$c1),$c1,$f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$c2))). 440 [hyper,398,13,33,35] -> RR2($c1,$f4($f1(x,$c1),$c1,$f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$c2))). 456 [ur,440,19] RR1($c2,$f4($f1(x,$c1),$c1,$f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$c2))) -> . 471 [ur,456,5,116] RR1($f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$c2),$f4($f1(x,$c1),$c1,$f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$c2))) -> . 472 [binary,471.1,434.1] -> . ------------ end of proof ------------- ----> UNIT CONFLICT at 2.43 sec ----> 1680 [binary,1679.1,1620.1] -> . Length of proof is 26. Level of proof is 12. ---------------- PROOF ---------------- 1 [] -> X=X. 2 [] X=Y -> Y=X. 3 [] X=Y -> RR1(X,Y). 4 [] X=Y -> RR2(X,Y). 5 [] RR1(X,Y), RR1(Y,Z) -> RR1(X,Z). 6 [] RR2(X,Y), RR2(Y,Z) -> RR2(X,Z). 7 [] RR1(X,Y) -> X=Y, R1(X,$f1(X,Y)). 8 [] RR1(X,Y) -> X=Y, RR1($f1(X,Y),Y). 9 [] RR2(X,Y) -> X=Y, R2(X,$f2(X,Y)). 10 [] RR2(X,Y) -> X=Y, RR2($f2(X,Y),Y). 11 [] R1(X,Y), R2(X,Z) -> RR2(Y,$f3(X,Y,Z)). 12 [] R1(X,Y), R2(X,Z) -> RR1(Z,$f3(X,Y,Z)). 13 [] R1(x,X), RR1(X,Y), RR2(X,Z) -> RR2(Y,$f4(X,Y,Z)). 14 [] R1(x,X), RR1(X,Y), RR2(X,Z) -> RR1(Z,$f4(X,Y,Z)). 15 [] R2(x,X), RR1(X,Y), RR2(X,Z) -> RR2(Y,$f4(X,Y,Z)). 16 [] R2(x,X), RR1(X,Y), RR2(X,Z) -> RR1(Z,$f4(X,Y,Z)). 17 [] -> RR1(x,$c1). 18 [] -> RR2(x,$c2). 19 [] RR2($c1,J), RR1($c2,J) -> . 20 [hyper,3,1] -> RR1(A,A). 21 [hyper,4,1] -> RR2(A,A). 22 [ur,19,20] RR2($c1,$c2) -> . 23 [ur,19,21] RR1($c2,$c1) -> . 26 [ur,5,17,23] RR1($c2,x) -> . 27 [ur,26,3] $c2=x -> . 28 [ur,27,2] x=$c2 -> . 29 [ur,6,18,22] RR2($c1,x) -> . 30 [ur,29,4] $c1=x -> . 31 [ur,30,2] x=$c1 -> . 33 [ur,7,17,31] -> R1(x,$f1(x,$c1)). 35 [ur,8,17,31] -> RR1($f1(x,$c1),$c1). 42 [ur,9,18,28] -> R2(x,$f2(x,$c2)). 44 [ur,10,18,28] -> RR2($f2(x,$c2),$c2). 50 [hyper,11,33,42] -> RR2($f1(x,$c1),$f3(x,$f1(x,$c1),$f2(x,$c2))). 51 [hyper,12,33,42] -> RR1($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2))). 61 [hyper,13,33,35,21] -> RR2($c1,$f4($f1(x,$c1),$c1,$f1(x,$c1))). 82 [hyper,14,33,35,21] -> RR1($f1(x,$c1),$f4($f1(x,$c1),$c1,$f1(x,$c1))). 87 [hyper,82,14,33,50] -> RR1($f3(x,$f1(x,$c1),$f2(x,$c2)),$f4($f1(x,$c1),$f4($f1(x,$c1),$c1,$f1(x,$c1)),$f3(x,$f1(x,$c1),$f2(x,$c2)))). 90 [hyper,82,13,33,50] -> RR2($f4($f1(x,$c1),$c1,$f1(x,$c1)),$f4($f1(x,$c1),$f4($f1(x,$c1),$c1,$f1(x,$c1)),$f3(x,$f1(x,$c1),$f2(x,$c2)))). 1597 [hyper,87,5,51] -> RR1($f2(x,$c2),$f4($f1(x,$c1),$f4($f1(x,$c1),$c1,$f1(x,$c1)),$f3(x,$f1(x,$c1),$f2(x,$c2)))). 1608 [hyper,1597,16,42,44] -> RR1($c2,$f4($f2(x,$c2),$f4($f1(x,$c1),$f4($f1(x,$c1),$c1,$f1(x,$c1)),$f3(x,$f1(x,$c1),$f2(x,$c2))),$c2)). 1620 [hyper,1597,15,42,44] -> RR2($f4($f1(x,$c1),$f4($f1(x,$c1),$c1,$f1(x,$c1)),$f3(x,$f1(x,$c1),$f2(x,$c2))),$f4($f2(x,$c2),$f4($f1(x,$c1),$f4($f1(x,$c1),$c1,$f1(x,$c1)),$f3(x,$f1(x,$c1),$f2(x,$c2))),$c2)). 1626 [ur,1608,19] RR2($c1,$f4($f2(x,$c2),$f4($f1(x,$c1),$f4($f1(x,$c1),$c1,$f1(x,$c1)),$f3(x,$f1(x,$c1),$f2(x,$c2))),$c2)) -> . 1662 [hyper,90,6,61] -> RR2($c1,$f4($f1(x,$c1),$f4($f1(x,$c1),$c1,$f1(x,$c1)),$f3(x,$f1(x,$c1),$f2(x,$c2)))). 1679 [ur,1662,6,1626] RR2($f4($f1(x,$c1),$f4($f1(x,$c1),$c1,$f1(x,$c1)),$f3(x,$f1(x,$c1),$f2(x,$c2))),$f4($f2(x,$c2),$f4($f1(x,$c1),$f4($f1(x,$c1),$c1,$f1(x,$c1)),$f3(x,$f1(x,$c1),$f2(x,$c2))),$c2)) -> . 1680 [binary,1679.1,1620.1] -> . ------------ end of proof ------------- ----> UNIT CONFLICT at 2.70 sec ----> 1803 [binary,1802.1,1730.1] -> . Length of proof is 26. Level of proof is 12. ---------------- PROOF ---------------- 1 [] -> X=X. 2 [] X=Y -> Y=X. 3 [] X=Y -> RR1(X,Y). 4 [] X=Y -> RR2(X,Y). 5 [] RR1(X,Y), RR1(Y,Z) -> RR1(X,Z). 6 [] RR2(X,Y), RR2(Y,Z) -> RR2(X,Z). 7 [] RR1(X,Y) -> X=Y, R1(X,$f1(X,Y)). 8 [] RR1(X,Y) -> X=Y, RR1($f1(X,Y),Y). 9 [] RR2(X,Y) -> X=Y, R2(X,$f2(X,Y)). 10 [] RR2(X,Y) -> X=Y, RR2($f2(X,Y),Y). 11 [] R1(X,Y), R2(X,Z) -> RR2(Y,$f3(X,Y,Z)). 12 [] R1(X,Y), R2(X,Z) -> RR1(Z,$f3(X,Y,Z)). 13 [] R1(x,X), RR1(X,Y), RR2(X,Z) -> RR2(Y,$f4(X,Y,Z)). 14 [] R1(x,X), RR1(X,Y), RR2(X,Z) -> RR1(Z,$f4(X,Y,Z)). 15 [] R2(x,X), RR1(X,Y), RR2(X,Z) -> RR2(Y,$f4(X,Y,Z)). 16 [] R2(x,X), RR1(X,Y), RR2(X,Z) -> RR1(Z,$f4(X,Y,Z)). 17 [] -> RR1(x,$c1). 18 [] -> RR2(x,$c2). 19 [] RR2($c1,J), RR1($c2,J) -> . 20 [hyper,3,1] -> RR1(A,A). 21 [hyper,4,1] -> RR2(A,A). 22 [ur,19,20] RR2($c1,$c2) -> . 23 [ur,19,21] RR1($c2,$c1) -> . 26 [ur,5,17,23] RR1($c2,x) -> . 27 [ur,26,3] $c2=x -> . 28 [ur,27,2] x=$c2 -> . 29 [ur,6,18,22] RR2($c1,x) -> . 30 [ur,29,4] $c1=x -> . 31 [ur,30,2] x=$c1 -> . 33 [ur,7,17,31] -> R1(x,$f1(x,$c1)). 35 [ur,8,17,31] -> RR1($f1(x,$c1),$c1). 42 [ur,9,18,28] -> R2(x,$f2(x,$c2)). 44 [ur,10,18,28] -> RR2($f2(x,$c2),$c2). 50 [hyper,11,33,42] -> RR2($f1(x,$c1),$f3(x,$f1(x,$c1),$f2(x,$c2))). 51 [hyper,12,33,42] -> RR1($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2))). 104 [hyper,15,42,20,44] -> RR2($f2(x,$c2),$f4($f2(x,$c2),$f2(x,$c2),$c2)). 106 [hyper,104,15,42,51] -> RR2($f3(x,$f1(x,$c1),$f2(x,$c2)),$f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$f4($f2(x,$c2),$f2(x,$c2),$c2))). 115 [hyper,16,42,51,104] -> RR1($f4($f2(x,$c2),$f2(x,$c2),$c2),$f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$f4($f2(x,$c2),$f2(x,$c2),$c2))). 120 [hyper,16,42,20,44] -> RR1($c2,$f4($f2(x,$c2),$f2(x,$c2),$c2)). 1719 [hyper,106,6,50] -> RR2($f1(x,$c1),$f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$f4($f2(x,$c2),$f2(x,$c2),$c2))). 1730 [hyper,1719,14,33,35] -> RR1($f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$f4($f2(x,$c2),$f2(x,$c2),$c2)),$f4($f1(x,$c1),$c1,$f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$f4($f2(x,$c2),$f2(x,$c2),$c2)))). 1742 [hyper,1719,13,33,35] -> RR2($c1,$f4($f1(x,$c1),$c1,$f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$f4($f2(x,$c2),$f2(x,$c2),$c2)))). 1748 [ur,1742,19] RR1($c2,$f4($f1(x,$c1),$c1,$f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$f4($f2(x,$c2),$f2(x,$c2),$c2)))) -> . 1785 [hyper,115,5,120] -> RR1($c2,$f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$f4($f2(x,$c2),$f2(x,$c2),$c2))). 1802 [ur,1785,5,1748] RR1($f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$f4($f2(x,$c2),$f2(x,$c2),$c2)),$f4($f1(x,$c1),$c1,$f4($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2)),$f4($f2(x,$c2),$f2(x,$c2),$c2)))) -> . 1803 [binary,1802.1,1730.1] -> . ------------ end of proof ------------- ----> UNIT CONFLICT at 4.69 sec ----> 2795 [binary,2794.1,363.1] -> . Length of proof is 23. Level of proof is 11. ---------------- PROOF ---------------- 1 [] -> X=X. 2 [] X=Y -> Y=X. 3 [] X=Y -> RR1(X,Y). 4 [] X=Y -> RR2(X,Y). 5 [] RR1(X,Y), RR1(Y,Z) -> RR1(X,Z). 6 [] RR2(X,Y), RR2(Y,Z) -> RR2(X,Z). 7 [] RR1(X,Y) -> X=Y, R1(X,$f1(X,Y)). 8 [] RR1(X,Y) -> X=Y, RR1($f1(X,Y),Y). 9 [] RR2(X,Y) -> X=Y, R2(X,$f2(X,Y)). 10 [] RR2(X,Y) -> X=Y, RR2($f2(X,Y),Y). 11 [] R1(X,Y), R2(X,Z) -> RR2(Y,$f3(X,Y,Z)). 12 [] R1(X,Y), R2(X,Z) -> RR1(Z,$f3(X,Y,Z)). 13 [] R1(x,X), RR1(X,Y), RR2(X,Z) -> RR2(Y,$f4(X,Y,Z)). 14 [] R1(x,X), RR1(X,Y), RR2(X,Z) -> RR1(Z,$f4(X,Y,Z)). 15 [] R2(x,X), RR1(X,Y), RR2(X,Z) -> RR2(Y,$f4(X,Y,Z)). 16 [] R2(x,X), RR1(X,Y), RR2(X,Z) -> RR1(Z,$f4(X,Y,Z)). 17 [] -> RR1(x,$c1). 18 [] -> RR2(x,$c2). 19 [] RR2($c1,J), RR1($c2,J) -> . 20 [hyper,3,1] -> RR1(A,A). 21 [hyper,4,1] -> RR2(A,A). 22 [ur,19,20] RR2($c1,$c2) -> . 23 [ur,19,21] RR1($c2,$c1) -> . 26 [ur,5,17,23] RR1($c2,x) -> . 27 [ur,26,3] $c2=x -> . 28 [ur,27,2] x=$c2 -> . 29 [ur,6,18,22] RR2($c1,x) -> . 30 [ur,29,4] $c1=x -> . 31 [ur,30,2] x=$c1 -> . 33 [ur,7,17,31] -> R1(x,$f1(x,$c1)). 35 [ur,8,17,31] -> RR1($f1(x,$c1),$c1). 42 [ur,9,18,28] -> R2(x,$f2(x,$c2)). 44 [ur,10,18,28] -> RR2($f2(x,$c2),$c2). 50 [hyper,11,33,42] -> RR2($f1(x,$c1),$f3(x,$f1(x,$c1),$f2(x,$c2))). 51 [hyper,12,33,42] -> RR1($f2(x,$c2),$f3(x,$f1(x,$c1),$f2(x,$c2))). 60 [hyper,13,33,35,50] -> RR2($c1,$f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2)))). 81 [hyper,14,33,35,50] -> RR1($f3(x,$f1(x,$c1),$f2(x,$c2)),$f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2)))). 306 [hyper,81,5,51] -> RR1($f2(x,$c2),$f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2)))). 341 [hyper,306,16,42,44] -> RR1($c2,$f4($f2(x,$c2),$f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2))),$c2)). 347 [hyper,306,15,42,44] -> RR2($f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2))),$f4($f2(x,$c2),$f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2))),$c2)). 363 [ur,341,19] RR2($c1,$f4($f2(x,$c2),$f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2))),$c2)) -> . 2794 [hyper,347,6,60] -> RR2($c1,$f4($f2(x,$c2),$f4($f1(x,$c1),$c1,$f3(x,$f1(x,$c1),$f2(x,$c2))),$c2)). 2795 [binary,2794.1,363.1] -> . ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 1028 clauses generated 5511 hyper_res generated 1450 ur_res generated 4061 demod & eval rewrites 0 clauses wt,lit,sk delete 0 tautologies deleted 0 clauses forward subsumed 2740 (subsumed by sos) 1175 unit deletions 0 factor simplifications 0 clauses kept 2771 new demodulators 0 empty clauses 5 clauses back demodulated 0 clauses back subsumed 44 usable size 1022 sos size 1724 demodulators size 0 passive size 0 hot size 0 Kbytes malloced 2331 ----------- times (seconds) ----------- user CPU time 4.70 (0 hr, 0 min, 4 sec) system CPU time 8.02 (0 hr, 0 min, 8 sec) wall-clock time 13 (0 hr, 0 min, 13 sec) input time 0.00 clausify time 0.00 pick given time 0.38 hyper_res time 0.24 ur_res time 0.83 pre_process time 2.23 renumber time 0.23 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 0.30 delete cl time 0.07 keep cl time 0.68 hints time 0.11 print_cl time 0.00 conflict time 0.38 new demod time 0.00 post_process time 0.57 back demod time 0.00 back subsume 0.41 factor time 0.00 unindex time 0.00 That finishes the proof of the theorem. Process 247 finished Mon Jul 1 16:57:57 2002