----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sat Nov 22 15:57:24 2003 The command was "otter". set(auto). dependent: set(auto1). dependent: set(process_input). dependent: clear(print_kept). dependent: clear(print_new_demod). dependent: clear(print_back_demod). dependent: clear(print_back_sub). dependent: set(control_memory). dependent: assign(max_mem, 12000). dependent: assign(pick_given_ratio, 4). dependent: assign(stats_level, 1). dependent: assign(max_seconds, 10800). clear(print_given). include("xtremeOptions.txt"). ------- start included file xtremeOptions.txt------- assign(max_weight,19). assign(max_distinct_vars,3). assign(max_literals,1). assign(max_mem,64000). formula_list(usable). all x (x=x). end_of_list. -------> usable clausifies to: list(usable). 0 [] x=x. end_of_list. ------- end included file xtremeOptions.txt------- include("booleanAx.txt"). ------- start included file booleanAx.txt------- include("1_2booleanAx.txt"). ------- start included file 1_2booleanAx.txt------- formula_list(usable). all x y (u(x,y)=u(y,x)). all x y z (u(x,u(y,z))=u(u(x,y),z)). end_of_list. -------> usable clausifies to: list(usable). 0 [] u(x,y)=u(y,x). 0 [] u(x,u(y,z))=u(u(x,y),z). end_of_list. ------- end included file 1_2booleanAx.txt------- include("3booleanAx.txt"). ------- start included file 3booleanAx.txt------- formula_list(usable). all x y (u(c(u(c(x),y)),c(u(c(x),c(y))))=x). end_of_list. -------> usable clausifies to: list(usable). 0 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. end_of_list. ------- end included file 3booleanAx.txt------- ------- end included file booleanAx.txt------- include("peirceanAx0.txt"). ------- start included file peirceanAx0.txt------- formula_list(usable). all x y z (k(x,k(y,z))=k(k(x,y),z)). all x (r(r(x))=x). all x y (r(u(x,y))=u(r(x),r(y))). all x y (r(k(x,y))=k(r(y),r(x))). end_of_list. -------> usable clausifies to: list(usable). 0 [] k(x,k(y,z))=k(k(x,y),z). 0 [] r(r(x))=x. 0 [] r(u(x,y))=u(r(x),r(y)). 0 [] r(k(x,y))=k(r(y),r(x)). end_of_list. ------- end included file peirceanAx0.txt------- include("peirceanAx1.txt"). ------- start included file peirceanAx1.txt------- formula_list(usable). all x y z (k(u(x,y),z)=u(k(x,z),k(y,z))). end_of_list. -------> usable clausifies to: list(usable). 0 [] k(u(x,y),z)=u(k(x,z),k(y,z)). end_of_list. ------- end included file peirceanAx1.txt------- include("peirceanAx2.txt"). ------- start included file peirceanAx2.txt------- formula_list(usable). all x (k(x,I)=x). all x y (u(k(r(x),c(k(x,y))),c(y))=c(y)). end_of_list. -------> usable clausifies to: list(usable). 0 [] k(x,I)=x. 0 [] u(k(r(x),c(k(x,y))),c(y))=c(y). end_of_list. ------- end included file peirceanAx2.txt------- include("iDef.txt"). ------- start included file iDef.txt------- formula_list(usable). all x y (i(x,y)<->u(x,y)=y). end_of_list. -------> usable clausifies to: list(usable). 0 [] -i(x,y)|u(x,y)=y. 0 [] i(x,y)|u(x,y)!=y. end_of_list. ------- end included file iDef.txt------- include("uzDef.txt"). ------- start included file uzDef.txt------- formula_list(usable). D=c(I). U=u(I,D). Z=c(U). end_of_list. -------> usable clausifies to: list(usable). 0 [] D=c(I). 0 [] U=u(I,D). 0 [] Z=c(U). end_of_list. ------- end included file uzDef.txt------- include("xx.txt"). ------- start included file xx.txt------- formula_list(usable). -(all x (k(x,U)=U->i(I,k(x,r(x))))). end_of_list. -------> usable clausifies to: list(usable). 0 [] k($c1,U)=U. 0 [] -i(I,k($c1,r($c1))). end_of_list. ------- end included file xx.txt------- SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=2. This is a Horn set with equality. The strategy will be Knuth-Bendix and hyper_res, with positive clauses in sos and nonpositive clauses in usable. dependent: set(knuth_bendix). dependent: set(para_from). dependent: set(para_into). dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). dependent: set(back_demod). dependent: set(lrpo). dependent: set(hyper_res). dependent: clear(order_hyper). ------------> process usable: ** KEPT (pick-wt=8): 1 [] -i(x,y)|u(x,y)=y. ** KEPT (pick-wt=8): 2 [] i(x,y)|u(x,y)!=y. ** KEPT (pick-wt=6): 3 [] -i(I,k($c1,r($c1))). ------------> process sos: ** KEPT (pick-wt=3): 4 [] x=x. ** KEPT (pick-wt=7): 5 [] u(x,y)=u(y,x). ** KEPT (pick-wt=11): 7 [copy,6,flip.1] u(u(x,y),z)=u(x,u(y,z)). ---> New Demodulator: 8 [new_demod,7] u(u(x,y),z)=u(x,u(y,z)). ** KEPT (pick-wt=14): 9 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ---> New Demodulator: 10 [new_demod,9] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ** KEPT (pick-wt=11): 12 [copy,11,flip.1] k(k(x,y),z)=k(x,k(y,z)). ---> New Demodulator: 13 [new_demod,12] k(k(x,y),z)=k(x,k(y,z)). ** KEPT (pick-wt=5): 14 [] r(r(x))=x. ---> New Demodulator: 15 [new_demod,14] r(r(x))=x. ** KEPT (pick-wt=10): 16 [] r(u(x,y))=u(r(x),r(y)). ---> New Demodulator: 17 [new_demod,16] r(u(x,y))=u(r(x),r(y)). ** KEPT (pick-wt=10): 18 [] r(k(x,y))=k(r(y),r(x)). ---> New Demodulator: 19 [new_demod,18] r(k(x,y))=k(r(y),r(x)). ** KEPT (pick-wt=13): 21 [copy,20,flip.1] u(k(x,y),k(z,y))=k(u(x,z),y). ---> New Demodulator: 22 [new_demod,21] u(k(x,y),k(z,y))=k(u(x,z),y). ** KEPT (pick-wt=5): 23 [] k(x,I)=x. ---> New Demodulator: 24 [new_demod,23] k(x,I)=x. ** KEPT (pick-wt=13): 25 [] u(k(r(x),c(k(x,y))),c(y))=c(y). ---> New Demodulator: 26 [new_demod,25] u(k(r(x),c(k(x,y))),c(y))=c(y). ** KEPT (pick-wt=4): 28 [copy,27,flip.1] c(I)=D. ---> New Demodulator: 29 [new_demod,28] c(I)=D. ** KEPT (pick-wt=5): 31 [copy,30,flip.1] u(I,D)=U. ---> New Demodulator: 32 [new_demod,31] u(I,D)=U. ** KEPT (pick-wt=4): 34 [copy,33,flip.1] c(U)=Z. ---> New Demodulator: 35 [new_demod,34] c(U)=Z. ** KEPT (pick-wt=5): 36 [] k($c1,U)=U. ---> New Demodulator: 37 [new_demod,36] k($c1,U)=U. Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] x=x. Following clause subsumed by 5 during input processing: 0 [copy,5,flip.1] u(x,y)=u(y,x). >>>> Starting back demodulation with 8. >>>> Starting back demodulation with 10. >>>> Starting back demodulation with 13. >>>> Starting back demodulation with 15. >>>> Starting back demodulation with 17. >>>> Starting back demodulation with 19. >>>> Starting back demodulation with 22. >>>> Starting back demodulation with 24. >>>> Starting back demodulation with 26. >>>> Starting back demodulation with 29. >>>> Starting back demodulation with 32. >>>> Starting back demodulation with 35. >>>> Starting back demodulation with 37. ======= end of input processing ======= =========== start of search =========== Resetting weight limit to 12. sos_size=20621 Resetting weight limit to 11. sos_size=16364 ----> UNIT CONFLICT at 611.41 sec ----> 44856 [binary,44855.1,3.1] $F. Length of proof is 196. Level of proof is 37. ---------------- PROOF ---------------- 1 [] -i(x,y)|u(x,y)=y. 2 [] i(x,y)|u(x,y)!=y. 3 [] -i(I,k($c1,r($c1))). 5 [] u(x,y)=u(y,x). 6 [] u(x,u(y,z))=u(u(x,y),z). 8,7 [copy,6,flip.1] u(u(x,y),z)=u(x,u(y,z)). 10,9 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 11 [] k(x,k(y,z))=k(k(x,y),z). 12 [copy,11,flip.1] k(k(x,y),z)=k(x,k(y,z)). 15,14 [] r(r(x))=x. 17,16 [] r(u(x,y))=u(r(x),r(y)). 19,18 [] r(k(x,y))=k(r(y),r(x)). 20 [] k(u(x,y),z)=u(k(x,z),k(y,z)). 21 [copy,20,flip.1] u(k(x,y),k(z,y))=k(u(x,z),y). 24,23 [] k(x,I)=x. 26,25 [] u(k(r(x),c(k(x,y))),c(y))=c(y). 27 [] D=c(I). 29,28 [copy,27,flip.1] c(I)=D. 30 [] U=u(I,D). 32,31 [copy,30,flip.1] u(I,D)=U. 33 [] Z=c(U). 35,34 [copy,33,flip.1] c(U)=Z. 36 [] k($c1,U)=U. 39,38 [para_into,31.1.1,5.1.1] u(D,I)=U. 41,40 [para_into,16.1.1.1,38.1.1] r(U)=u(r(D),r(I)). 43,42 [para_into,7.1.1.1,38.1.1] u(U,x)=u(D,u(I,x)). 46 [para_into,7.1.1.1,5.1.1,demod,8] u(x,u(y,z))=u(y,u(x,z)). 47 [para_into,7.1.1,5.1.1] u(x,u(y,z))=u(y,u(z,x)). 48 [copy,47,flip.1] u(x,u(y,z))=u(z,u(x,y)). 49 [para_into,42.1.1,5.1.1] u(x,U)=u(D,u(I,x)). 50 [copy,49,flip.1] u(D,u(I,x))=u(x,U). 51 [para_into,49.1.1,7.1.1] u(x,u(y,U))=u(D,u(I,u(x,y))). 52 [copy,51,flip.1] u(D,u(I,u(x,y)))=u(x,u(y,U)). 53 [para_from,49.1.1,7.1.1.1,demod,8,8,43] u(D,u(I,u(x,y)))=u(x,u(D,u(I,y))). 54 [copy,53,flip.1] u(x,u(D,u(I,y)))=u(D,u(I,u(x,y))). 57 [para_into,50.1.1.2,5.1.1] u(D,u(x,I))=u(x,U). 58 [para_into,50.1.1,5.1.1,demod,8] u(I,u(x,D))=u(x,U). 59 [copy,57,flip.1] u(x,U)=u(D,u(x,I)). 60 [copy,58,flip.1] u(x,U)=u(I,u(x,D)). 61 [para_into,9.1.1.1.1.1,34.1.1,demod,35] u(c(u(Z,x)),c(u(Z,c(x))))=U. 63 [para_into,9.1.1.1.1.1,28.1.1,demod,29] u(c(u(D,x)),c(u(D,c(x))))=I. 65 [para_into,9.1.1.1.1,49.1.1,demod,35] u(c(u(D,u(I,c(x)))),c(u(c(x),Z)))=x. 67 [para_into,9.1.1.1.1,5.1.1] u(c(u(x,c(y))),c(u(c(y),c(x))))=y. 69 [para_into,9.1.1.2.1.2,34.1.1] u(c(u(c(x),U)),c(u(c(x),Z)))=x. 73 [para_into,9.1.1.2.1,5.1.1] u(c(u(c(x),y)),c(u(c(y),c(x))))=x. 75 [para_into,9.1.1,5.1.1] u(c(u(c(x),c(y))),c(u(c(x),y)))=x. 79 [para_from,9.1.1,7.1.1.1,flip.1] u(c(u(c(x),y)),u(c(u(c(x),c(y))),z))=u(x,z). 93 [para_from,60.1.1,9.1.1.1.1,demod,35] u(c(u(I,u(c(x),D))),c(u(c(x),Z)))=x. 97 [para_into,12.1.1.1,23.1.1,flip.1] k(x,k(I,y))=k(x,y). 101 [para_into,18.1.1.1,36.1.1,demod,41,41,flip.1] k(u(r(D),r(I)),r($c1))=u(r(D),r(I)). 103 [para_into,18.1.1.1,23.1.1,flip.1] k(r(I),r(x))=r(x). 112,111 [para_into,103.1.1.2,14.1.1,demod,15] k(r(I),x)=x. 119 [para_into,21.1.1.2,36.1.1] u(k(x,U),U)=k(u(x,$c1),U). 123,122 [para_into,111.1.1,97.1.1,demod,112,flip.1] k(I,x)=x. 125,124 [para_into,111.1.1,23.1.1] r(I)=I. 126 [back_demod,101,demod,125,125] k(u(r(D),I),r($c1))=u(r(D),I). 129,128 [back_demod,40,demod,125] r(U)=u(r(D),I). 131,130 [para_from,122.1.1,21.1.1.2] u(k(x,y),y)=k(u(x,I),y). 132 [para_from,122.1.1,21.1.1.1] u(x,k(y,x))=k(u(I,y),x). 134,133 [back_demod,119,demod,131] k(u(x,I),U)=k(u(x,$c1),U). 137 [copy,132,flip.1] k(u(I,x),y)=u(y,k(x,y)). 142,141 [para_into,25.1.1.1.1,124.1.1,demod,123,123] u(c(x),c(x))=c(x). 153 [para_into,25.1.1.1.2.1,23.1.1,demod,29,29] u(k(r(x),c(x)),D)=D. 155 [para_into,25.1.1.2,34.1.1,demod,35] u(k(r(x),c(k(x,U))),Z)=Z. 165,164 [para_into,141.1.1.1,34.1.1,demod,35,35] u(Z,Z)=Z. 167,166 [para_into,141.1.1.1,28.1.1,demod,29,29] u(D,D)=D. 184 [para_into,46.1.1.2,25.1.1,flip.1] u(k(r(x),c(k(x,y))),u(z,c(y)))=u(z,c(y)). 195 [para_from,164.1.1,46.1.1.2,flip.1] u(Z,u(x,Z))=u(x,Z). 199 [para_from,164.1.1,7.1.1.1,flip.1] u(Z,u(Z,x))=u(Z,x). 202,201 [para_from,166.1.1,58.1.1.2,demod,32,flip.1] u(D,U)=U. 211,210 [para_from,201.1.1,46.1.1.2,flip.1] u(D,u(x,U))=u(x,U). 285 [para_into,153.1.1.1.1,14.1.1] u(k(x,c(r(x))),D)=D. 324 [hyper,195,2] i(Z,u(x,Z)). 354 [para_into,324.1.2,5.1.1] i(Z,u(Z,x)). 358 [para_into,354.1.2,48.1.1] i(Z,u(x,u(Z,y))). 444 [para_into,61.1.1.1.1,59.1.1,demod,35,165] u(c(u(D,u(Z,I))),c(Z))=U. 460 [para_into,61.1.1.2.1.2,28.1.1] u(c(u(Z,I)),c(u(Z,D)))=U. 479 [para_from,61.1.1,16.1.1.1,demod,129,flip.1] u(r(c(u(Z,x))),r(c(u(Z,c(x)))))=u(r(D),I). 481 [para_from,61.1.1,7.1.1.1,demod,43,flip.1] u(c(u(Z,x)),u(c(u(Z,c(x))),y))=u(D,u(I,y)). 526,525 [para_into,63.1.1.1.1,38.1.1,demod,35,29,167] u(Z,c(D))=I. 549,548 [para_into,525.1.1,5.1.1] u(c(D),Z)=I. 550 [para_from,525.1.1,358.1.2.2] i(Z,u(x,I)). 555,554 [para_from,525.1.1,199.1.1.2,demod,526] u(Z,I)=I. 563 [para_from,525.1.1,53.1.1.2.2,flip.1] u(Z,u(D,u(I,c(D))))=u(D,u(I,I)). 571 [back_demod,460,demod,555,29] u(D,c(u(Z,D)))=U. 574,573 [back_demod,444,demod,555,39,35] u(Z,c(Z))=U. 580 [para_into,550.1.2,38.1.1] i(Z,U). 584,583 [hyper,580,1] u(Z,U)=U. 587 [para_into,65.1.1,5.1.1] u(c(u(c(x),Z)),c(u(D,u(I,c(x)))))=x. 596 [para_from,65.1.1,7.1.1.1,flip.1] u(c(u(D,u(I,c(x)))),u(c(u(c(x),Z)),y))=u(x,y). 599,598 [para_into,554.1.1,5.1.1] u(I,Z)=I. 607 [para_from,554.1.1,16.1.1.1,demod,125,125,flip.1] u(r(Z),I)=I. 620,619 [para_from,583.1.1,46.1.1.2,flip.1] u(Z,u(x,U))=u(x,U). 624,623 [para_from,583.1.1,7.1.1.1,demod,43,43,flip.1] u(Z,u(D,u(I,x)))=u(D,u(I,x)). 626,625 [back_demod,563,demod,624] u(D,u(I,c(D)))=u(D,u(I,I)). 667 [para_from,548.1.1,65.1.1.2.1,demod,626,29] u(c(u(D,u(I,I))),D)=D. 676 [para_from,573.1.1,67.1.1.1.1,demod,35,142] u(Z,c(c(Z)))=Z. 766 [para_into,73.1.1.1.1,548.1.1,demod,29] u(D,c(u(c(Z),c(D))))=D. 778 [para_into,73.1.1.1.1,48.1.1] u(c(u(x,u(c(y),z))),c(u(c(u(z,x)),c(y))))=y. 801 [para_from,73.1.1,7.1.1.1,flip.1] u(c(u(c(x),y)),u(c(u(c(y),c(x))),z))=u(x,z). 803 [para_into,676.1.1,5.1.1] u(c(c(Z)),Z)=Z. 817,816 [para_from,676.1.1,52.1.1.2.2,demod,599,39,620,flip.1] u(c(c(Z)),U)=U. 824,823 [para_from,803.1.1,69.1.1.2.1,demod,817,35,574,flip.1] c(Z)=U. 825 [back_demod,766,demod,824,43,626] u(D,c(u(D,u(I,I))))=D. 839 [para_from,823.1.1,141.1.1.2,demod,824,43,211,824] u(I,U)=U. 861 [para_into,75.1.1.1.1,69.1.1] u(c(x),c(u(c(u(c(x),U)),u(c(x),Z))))=u(c(x),U). 886 [para_from,75.1.1,7.1.1.1,flip.1] u(c(u(c(x),c(y))),u(c(u(c(x),y)),z))=u(x,z). 890,889 [para_into,839.1.1,59.1.1] u(D,u(I,I))=U. 892,891 [back_demod,825,demod,890,35] u(D,Z)=D. 896,895 [back_demod,667,demod,890,35] u(Z,D)=D. 899 [back_demod,571,demod,896] u(D,c(D))=U. 921 [para_from,891.1.1,46.1.1.2,flip.1] u(D,u(x,Z))=u(x,D). 940 [para_from,895.1.1,16.1.1.1,flip.1] u(r(Z),r(D))=r(D). 955 [para_into,79.1.1.2.1.1,141.1.1] u(c(u(c(x),x)),u(c(c(x)),y))=u(x,y). 958,957 [para_into,79.1.1.2,141.1.1,demod,10,flip.1] u(x,c(u(c(x),c(y))))=x. 961 [para_into,79.1.1.2,9.1.1,demod,958] u(c(u(c(x),y)),x)=x. 978 [para_from,899.1.1,67.1.1.1.1,demod,35,142] u(Z,c(c(D)))=D. 1036 [para_from,978.1.1,67.1.1.1.1,demod,824] u(c(D),c(u(c(c(D)),U)))=c(D). 1047,1046 [para_from,978.1.1,52.1.1.2.2,demod,32,202,620,flip.1] u(c(c(D)),U)=U. 1049,1048 [back_demod,1036,demod,1047,35,549,flip.1] c(D)=I. 1082 [para_from,1048.1.1,153.1.1.1.2,demod,24] u(r(D),D)=D. 1085,1084 [para_from,1048.1.1,141.1.1.2,demod,1049,1049] u(I,I)=I. 1124,1123 [para_into,1082.1.1,5.1.1] u(D,r(D))=D. 1134,1133 [para_from,1082.1.1,16.1.1.1,demod,15,1124] r(D)=D. 1137 [back_demod,940,demod,1134,1134] u(r(Z),D)=D. 1141 [back_demod,479,demod,1134,39] u(r(c(u(Z,x))),r(c(u(Z,c(x)))))=U. 1151,1150 [back_demod,128,demod,1134,39] r(U)=U. 1152 [back_demod,126,demod,1134,39,1134,39] k(U,r($c1))=U. 1257 [para_from,285.1.1,7.1.1.1,flip.1] u(k(x,c(r(x))),u(D,y))=u(D,y). 1387,1386 [para_into,130.1.1.1,122.1.1,demod,1085,123] u(x,x)=x. 1393 [para_into,130.1.1,51.1.1] u(D,u(I,u(k(x,u(y,U)),y)))=k(u(x,I),u(y,U)). 1571 [para_into,133.1.1.1,38.1.1,flip.1] k(u(D,$c1),U)=k(U,U). 1613 [para_into,137.1.1.1,839.1.1,flip.1] u(x,k(U,x))=k(U,x). 1937 [para_into,155.1.1.1.1,1150.1.1] u(k(U,c(k(U,U))),Z)=Z. 2485 [hyper,961,2] i(c(u(c(x),y)),x). 2507,2506 [para_into,961.1.1.1.1,79.1.1] u(c(u(x,y)),u(c(x),z))=u(c(x),z). 2512 [para_into,961.1.1.1.1,54.1.1] u(c(u(D,u(I,u(c(x),y)))),x)=x. 2520 [para_into,961.1.1.1.1,5.1.1] u(c(u(x,c(y))),y)=y. 2549,2548 [back_demod,955,demod,2507] u(c(c(x)),y)=u(x,y). 2573,2572 [para_from,961.1.1,921.1.1.2,demod,892,824,43,flip.1] u(c(u(D,u(I,x))),D)=D. 2575,2574 [para_from,961.1.1,184.1.1.2,demod,26,2549,flip.1] u(c(u(x,y)),c(x))=c(x). 2594,2593 [para_from,961.1.1,73.1.1.2.1,demod,2549,2575] c(c(x))=x. 2598,2597 [para_from,961.1.1,93.1.1.2.1,demod,824,43,2573,32,35,824,584,824,43,flip.1] u(D,u(I,x))=U. 2612,2611 [para_from,961.1.1,51.1.1.2,demod,35,2598] u(x,U)=U. 2628 [para_from,961.1.1,16.1.1.1,flip.1] u(r(c(u(c(x),y))),r(x))=r(x). 2630 [para_from,961.1.1,7.1.1.1,flip.1] u(c(u(c(x),y)),u(x,z))=u(x,z). 2653,2652 [back_demod,2512,demod,2598,35] u(Z,x)=x. 2669,2668 [back_demod,1393,demod,2612,2598,2612,134,flip.1] k(u(x,$c1),U)=U. 2695,2694 [back_demod,596,demod,2598,35,2653] u(c(u(c(x),Z)),y)=u(x,y). 2702,2701 [back_demod,587,demod,2598,35,2695] u(x,Z)=x. 2703 [back_demod,481,demod,2653,2653,2594,2598] u(c(x),u(x,y))=U. 2712,2711 [back_demod,42,demod,2598] u(U,x)=U. 2729 [back_demod,861,demod,2612,35,2702,2653,2594,2612] u(c(x),x)=U. 2757 [back_demod,1141,demod,2653,2653,2594] u(r(c(x)),r(x))=U. 2777,2776 [back_demod,1571,demod,2669,flip.1] k(U,U)=U. 2785,2784 [back_demod,1937,demod,2777,35,2702] k(U,Z)=Z. 2809 [para_from,2593.1.1,67.1.1.2.1.1,demod,2594] u(c(u(x,y)),c(u(y,c(x))))=c(y). 2817 [para_from,2593.1.1,73.1.1.2.1.2,demod,2594] u(c(u(x,y)),c(u(c(y),x)))=c(x). 2872 [para_from,2784.1.1,21.1.1.2,demod,2702,2612,2785] k(x,Z)=Z. 2878 [para_from,2872.1.1,18.1.1.1,flip.1] k(r(Z),r(x))=r(Z). 2898 [para_into,2729.1.1,46.1.1] u(x,u(c(u(x,y)),y))=U. 2906 [para_into,2485.1.1.1.1,2593.1.1] i(c(u(x,y)),c(x)). 2909 [para_into,2485.1.1.1,961.1.1] i(c(x),u(c(x),y)). 3034 [para_into,2906.1.1.1,607.1.1,demod,29] i(D,c(r(Z))). 3054,3053 [hyper,3034,1] u(D,c(r(Z)))=c(r(Z)). 3055 [para_into,2909.1.1,2593.1.1,demod,2594] i(x,u(x,y)). 3072 [para_into,3055.1.2,48.1.1] i(x,u(y,u(x,z))). 3075 [para_into,3055.1.2,5.1.1] i(x,u(y,x)). 3083 [para_into,3075.1.2,48.1.1] i(u(x,y),u(y,u(z,x))). 3084 [para_into,3075.1.2,46.1.1] i(u(x,y),u(x,u(z,y))). 3246 [para_into,3072.1.2.2,961.1.1] i(c(u(c(x),y)),u(z,x)). 3396 [para_into,2703.1.1.2,1137.1.1] u(c(r(Z)),D)=U. 3440 [para_into,3396.1.1,5.1.1,demod,3054] c(r(Z))=U. 3458,3457 [para_from,3440.1.1,2593.1.1.1,demod,35,flip.1] r(Z)=Z. 3482 [back_demod,2878,demod,3458,3458] k(Z,r(x))=Z. 3560,3559 [para_into,3482.1.1.2,14.1.1] k(Z,x)=Z. 3640 [para_into,2757.1.1.2,14.1.1] u(r(c(r(x))),x)=U. 4131 [para_from,1613.1.1,2906.1.1.1] i(c(k(U,x)),c(x)). 4151 [hyper,4131,1] u(c(k(U,x)),c(x))=c(x). 4353,4352 [para_from,2520.1.1,7.1.1.1,flip.1] u(c(u(x,c(y))),u(y,z))=u(y,z). 4373 [para_into,778.1.1.1.1.2.1,2593.1.1,demod,2594] u(c(u(x,u(y,z))),c(u(c(u(z,x)),y)))=c(y). 4393 [para_into,778.1.1.1.1,3640.1.1,demod,35,17,2653] c(u(c(u(x,r(c(u(r(c(y)),r(x)))))),c(y)))=y. 4752 [para_into,801.1.1.2,801.1.1,demod,2594] u(c(u(c(x),y)),u(y,z))=u(x,u(c(u(x,c(y))),z)). 4755 [copy,4752,flip.1] u(x,u(c(u(x,c(y))),z))=u(c(u(c(x),y)),u(y,z)). 4977 [para_into,3246.1.1.1.1,2593.1.1] i(c(u(x,y)),u(z,c(x))). 4998 [para_into,886.1.1.1.1,2520.1.1,demod,2594,2594,2594,8] u(x,u(c(u(c(u(y,x)),x)),z))=u(y,u(x,z)). 5572 [para_from,1257.1.1,3084.1.2] i(u(k(x,c(r(x))),y),u(D,y)). 6021,6020 [hyper,4977,1] u(c(u(x,y)),u(z,c(x)))=u(z,c(x)). 17593 [hyper,2628,2] i(r(c(u(c(x),y))),r(x)). 17664 [para_into,17593.1.1.1.1.1,2593.1.1] i(r(c(u(x,y))),r(c(x))). 17665 [para_into,17593.1.1.1.1,4151.1.1,demod,2594,19,1151] i(r(x),k(r(x),U)). 17695 [para_into,17665.1.1,14.1.1,demod,15] i(x,k(x,U)). 17696 [hyper,17695,1] u(x,k(x,U))=k(x,U). 17740 [para_from,2630.1.1,3083.1.2] i(u(x,c(u(c(y),z))),u(y,x)). 19062,19061 [para_into,2809.1.1.1.1,2898.1.1,demod,35,8,6021,2653,flip.1] c(u(c(u(x,y)),y))=c(u(y,c(x))). 19068,19067 [para_into,2809.1.1.1.1,2809.1.1,demod,2594,2594,4353,2594] u(x,c(u(y,x)))=u(x,c(y)). 19069 [para_into,2809.1.1.1.1,2757.1.1,demod,35,2653] c(u(r(x),c(r(c(x)))))=c(r(x)). 19113,19112 [back_demod,4998,demod,19062] u(x,u(c(u(x,c(y))),z))=u(y,u(x,z)). 19191,19190 [back_demod,4755,demod,19113,flip.1] u(c(u(c(x),y)),u(y,z))=u(y,u(x,z)). 19699,19698 [para_from,2817.1.1,2809.1.1.1.1,demod,2594,2594,19191,1387,2594] u(x,c(u(x,y)))=u(c(y),x). 34895 [para_into,5572.1.1,21.1.1] i(k(u(x,y),c(r(x))),u(D,k(y,c(r(x))))). 40174 [para_from,4373.1.1,17740.1.1,demod,8,19699] i(c(x),u(y,u(c(u(x,y)),z))). 40255 [para_from,4393.1.1,17664.1.1.1,demod,2594,17,15,19068] i(r(x),u(r(y),c(r(c(x))))). 40269 [para_into,40255.1.2.1,3457.1.1,demod,2653] i(r(x),c(r(c(x)))). 40276,40275 [hyper,40269,1] u(r(x),c(r(c(x))))=c(r(c(x))). 40278,40277 [back_demod,19069,demod,40276,2594] r(c(x))=c(r(x)). 41923 [para_into,40174.1.1,1048.1.1] i(I,u(x,u(c(u(D,x)),y))). 41947 [para_into,41923.1.2.2,17696.1.1] i(I,u(x,k(c(u(D,x)),U))). 41979 [para_into,41947.1.2,5.1.1] i(I,u(k(c(u(D,x)),U),x)). 44821 [para_into,34895.1.1.1,2729.1.1,demod,40278,2594,40278,2594] i(k(U,r(x)),u(D,k(x,r(x)))). 44823 [para_into,44821.1.1,1152.1.1] i(U,u(D,k($c1,r($c1)))). 44824 [hyper,44823,1,demod,2712,flip.1] u(D,k($c1,r($c1)))=U. 44855 [para_from,44824.1.1,41979.1.2.1.1.1,demod,35,3560,2653] i(I,k($c1,r($c1))). 44856 [binary,44855.1,3.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 15038 clauses generated 24284346 clauses kept 34173 clauses forward subsumed 12983071 clauses back subsumed 3127 Kbytes malloced 25451 ----------- times (seconds) ----------- user CPU time 611.62 (0 hr, 10 min, 11 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 611 (0 hr, 10 min, 11 sec) hyper_res time 0.00 para_into time 0.00 para_from time 0.00 for_sub time 0.00 back_sub time 0.00 conflict time 0.00 demod time 0.00 That finishes the proof of the theorem. Process 0 finished Sat Nov 22 16:07:35 2003