----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sat Nov 22 00:44:38 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). assign(max_literals,1). 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("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("dDef.txt"). ------- start included file dDef.txt------- formula_list(usable). all x y (d(x,y)=c(k(c(x),c(y)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] d(x,y)=c(k(c(x),c(y))). end_of_list. ------- end included file dDef.txt------- include("xiv.txt"). ------- start included file xiv.txt------- formula_list(usable). -(all x (k(U,x)=d(Z,k(U,x)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] k(U,$c1)!=d(Z,k(U,$c1)). end_of_list. ------- end included file xiv.txt------- SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=1. All clauses are units, and equality is present; the strategy will be Knuth-Bendix with positive clauses in sos. 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). ------------> process usable: ** KEPT (pick-wt=9): 2 [copy,1,flip.1] d(Z,k(U,$c1))!=k(U,$c1). ------------> process sos: ** KEPT (pick-wt=7): 3 [] u(x,y)=u(y,x). ** KEPT (pick-wt=11): 5 [copy,4,flip.1] u(u(x,y),z)=u(x,u(y,z)). ---> New Demodulator: 6 [new_demod,5] u(u(x,y),z)=u(x,u(y,z)). ** KEPT (pick-wt=14): 7 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ---> New Demodulator: 8 [new_demod,7] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ** KEPT (pick-wt=11): 10 [copy,9,flip.1] k(k(x,y),z)=k(x,k(y,z)). ---> New Demodulator: 11 [new_demod,10] k(k(x,y),z)=k(x,k(y,z)). ** KEPT (pick-wt=5): 12 [] r(r(x))=x. ---> New Demodulator: 13 [new_demod,12] r(r(x))=x. ** KEPT (pick-wt=10): 14 [] r(u(x,y))=u(r(x),r(y)). ---> New Demodulator: 15 [new_demod,14] r(u(x,y))=u(r(x),r(y)). ** KEPT (pick-wt=10): 16 [] r(k(x,y))=k(r(y),r(x)). ---> New Demodulator: 17 [new_demod,16] r(k(x,y))=k(r(y),r(x)). ** KEPT (pick-wt=13): 19 [copy,18,flip.1] u(k(x,y),k(z,y))=k(u(x,z),y). ---> New Demodulator: 20 [new_demod,19] u(k(x,y),k(z,y))=k(u(x,z),y). ** KEPT (pick-wt=5): 21 [] k(x,I)=x. ---> New Demodulator: 22 [new_demod,21] k(x,I)=x. ** KEPT (pick-wt=13): 23 [] u(k(r(x),c(k(x,y))),c(y))=c(y). ---> New Demodulator: 24 [new_demod,23] u(k(r(x),c(k(x,y))),c(y))=c(y). ** KEPT (pick-wt=4): 26 [copy,25,flip.1] c(I)=D. ---> New Demodulator: 27 [new_demod,26] c(I)=D. ** KEPT (pick-wt=5): 29 [copy,28,flip.1] u(I,D)=U. ---> New Demodulator: 30 [new_demod,29] u(I,D)=U. ** KEPT (pick-wt=4): 32 [copy,31,flip.1] c(U)=Z. ---> New Demodulator: 33 [new_demod,32] c(U)=Z. ** KEPT (pick-wt=10): 35 [copy,34,flip.1] c(k(c(x),c(y)))=d(x,y). ---> New Demodulator: 36 [new_demod,35] c(k(c(x),c(y)))=d(x,y). Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] u(x,y)=u(y,x). >>>> Starting back demodulation with 6. >>>> Starting back demodulation with 8. >>>> Starting back demodulation with 11. >>>> Starting back demodulation with 13. >>>> Starting back demodulation with 15. >>>> Starting back demodulation with 17. >>>> Starting back demodulation with 20. >>>> Starting back demodulation with 22. >>>> Starting back demodulation with 24. >>>> Starting back demodulation with 27. >>>> Starting back demodulation with 30. >>>> Starting back demodulation with 33. >>>> Starting back demodulation with 36. ======= end of input processing ======= =========== start of search =========== Resetting weight limit to 10. sos_size=1324 ----> UNIT CONFLICT at 3.96 sec ----> 7008 [binary,7006.1,2.1] $F. Length of proof is 141. Level of proof is 34. ---------------- PROOF ---------------- 1 [] k(U,$c1)!=d(Z,k(U,$c1)). 2 [copy,1,flip.1] d(Z,k(U,$c1))!=k(U,$c1). 3 [] u(x,y)=u(y,x). 4 [] u(x,u(y,z))=u(u(x,y),z). 6,5 [copy,4,flip.1] u(u(x,y),z)=u(x,u(y,z)). 8,7 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 9 [] k(x,k(y,z))=k(k(x,y),z). 10 [copy,9,flip.1] k(k(x,y),z)=k(x,k(y,z)). 13,12 [] r(r(x))=x. 14 [] r(u(x,y))=u(r(x),r(y)). 16 [] r(k(x,y))=k(r(y),r(x)). 18 [] k(u(x,y),z)=u(k(x,z),k(y,z)). 19 [copy,18,flip.1] u(k(x,y),k(z,y))=k(u(x,z),y). 22,21 [] k(x,I)=x. 23 [] u(k(r(x),c(k(x,y))),c(y))=c(y). 25 [] D=c(I). 27,26 [copy,25,flip.1] c(I)=D. 28 [] U=u(I,D). 30,29 [copy,28,flip.1] u(I,D)=U. 31 [] Z=c(U). 33,32 [copy,31,flip.1] c(U)=Z. 34 [] d(x,y)=c(k(c(x),c(y))). 35 [copy,34,flip.1] c(k(c(x),c(y)))=d(x,y). 40 [para_into,5.1.1.1,3.1.1,demod,6] u(x,u(y,z))=u(y,u(x,z)). 41 [para_into,5.1.1,3.1.1] u(x,u(y,z))=u(y,u(z,x)). 42 [copy,41,flip.1] u(x,u(y,z))=u(z,u(x,y)). 46,45 [para_into,29.1.1,3.1.1] u(D,I)=U. 48,47 [para_from,29.1.1,5.1.1.1] u(U,x)=u(I,u(D,x)). 49 [para_into,7.1.1.1.1.1,32.1.1,demod,33] u(c(u(Z,x)),c(u(Z,c(x))))=U. 51 [para_into,7.1.1.1.1.1,26.1.1,demod,27] u(c(u(D,x)),c(u(D,c(x))))=I. 57 [para_into,7.1.1.2.1.2,32.1.1] u(c(u(c(x),U)),c(u(c(x),Z)))=x. 61 [para_into,7.1.1.2.1,7.1.1] u(c(u(c(u(c(x),y)),u(c(x),c(y)))),c(x))=u(c(x),y). 63 [para_into,7.1.1.2.1,3.1.1] u(c(u(c(x),y)),c(u(c(y),c(x))))=x. 65 [para_into,7.1.1,3.1.1] u(c(u(c(x),c(y))),c(u(c(x),y)))=x. 67 [para_from,7.1.1,5.1.1.1,flip.1] u(c(u(c(x),y)),u(c(u(c(x),c(y))),z))=u(x,z). 69 [para_into,47.1.1,3.1.1] u(x,U)=u(I,u(D,x)). 70 [copy,69,flip.1] u(I,u(D,x))=u(x,U). 71 [para_into,69.1.1,5.1.1] u(x,u(y,U))=u(I,u(D,u(x,y))). 72 [copy,71,flip.1] u(I,u(D,u(x,y)))=u(x,u(y,U)). 73 [para_from,69.1.1,7.1.1.1.1,demod,33] u(c(u(I,u(D,c(x)))),c(u(c(x),Z)))=x. 79 [para_into,70.1.1.2,3.1.1] u(I,u(x,D))=u(x,U). 80 [para_into,70.1.1,3.1.1,demod,6] u(D,u(x,I))=u(x,U). 82 [copy,80,flip.1] u(x,U)=u(D,u(x,I)). 83 [para_into,10.1.1.1,21.1.1,flip.1] k(x,k(I,y))=k(x,y). 88 [para_into,80.1.1.2,3.1.1] u(D,u(I,x))=u(x,U). 90 [copy,88,flip.1] u(x,U)=u(D,u(I,x)). 99 [para_from,82.1.1,7.1.1.1.1,demod,33] u(c(u(D,u(c(x),I))),c(u(c(x),Z)))=x. 109 [para_into,14.1.1.1,45.1.1] r(U)=u(r(D),r(I)). 127 [para_into,16.1.1.1,21.1.1,flip.1] k(r(I),r(x))=r(x). 136,135 [para_into,127.1.1.2,12.1.1,demod,13] k(r(I),x)=x. 138,137 [para_into,135.1.1,83.1.1,demod,136,flip.1] k(I,x)=x. 140,139 [para_into,135.1.1,21.1.1] r(I)=I. 144,143 [back_demod,109,demod,140] r(U)=u(r(D),I). 145 [para_into,19.1.1.1,137.1.1] u(x,k(y,x))=k(u(I,y),x). 149,148 [para_into,19.1.1.2,137.1.1] u(k(x,y),y)=k(u(x,I),y). 189,188 [para_into,23.1.1.1.1,139.1.1,demod,138,138] u(c(x),c(x))=c(x). 196 [para_into,23.1.1.1.2.1,21.1.1,demod,27,27] u(k(r(x),c(x)),D)=D. 202 [para_into,23.1.1.1.2,35.1.1] u(k(r(c(x)),d(x,y)),c(c(y)))=c(c(y)). 212 [para_into,23.1.1,3.1.1] u(c(x),k(r(y),c(k(y,x))))=c(x). 233,232 [para_into,188.1.1.1,32.1.1,demod,33,33] u(Z,Z)=Z. 235,234 [para_into,188.1.1.1,26.1.1,demod,27,27] u(D,D)=D. 246 [para_from,232.1.1,5.1.1.1,flip.1] u(Z,u(Z,x))=u(Z,x). 249,248 [para_from,234.1.1,79.1.1.2,demod,30,flip.1] u(D,U)=U. 257,256 [para_into,40.1.1.2,232.1.1,flip.1] u(Z,u(x,Z))=u(x,Z). 281 [para_from,40.1.1,7.1.1.1.1] u(c(u(x,u(c(y),z))),c(u(c(y),c(u(x,z)))))=y. 451 [para_from,196.1.1,79.1.1.2,demod,30,flip.1] u(k(r(x),c(x)),U)=U. 481 [para_into,49.1.1.1.1,232.1.1] u(c(Z),c(u(Z,c(Z))))=U. 485 [para_into,49.1.1.1.1,82.1.1,demod,33,233] u(c(u(D,u(Z,I))),c(Z))=U. 535 [para_from,49.1.1,40.1.1.2,flip.1] u(c(u(Z,x)),u(y,c(u(Z,c(x)))))=u(y,U). 597 [para_into,51.1.1.1.1,248.1.1,demod,33,33] u(Z,c(u(D,Z)))=I. 606,605 [para_into,51.1.1.1.1,45.1.1,demod,33,27,235] u(Z,c(D))=I. 650,649 [para_into,605.1.1,3.1.1] u(c(D),Z)=I. 654,653 [para_from,605.1.1,246.1.1.2,demod,606] u(Z,I)=I. 668,667 [back_demod,485,demod,654,46,33] u(Z,c(Z))=U. 669 [back_demod,481,demod,668,33] u(c(Z),Z)=U. 672,671 [para_into,653.1.1,3.1.1] u(I,Z)=I. 674,673 [para_from,653.1.1,80.1.1.2,demod,46,flip.1] u(Z,U)=U. 679 [para_from,653.1.1,42.1.1.2,flip.1] u(I,u(x,Z))=u(x,I). 692,691 [para_from,673.1.1,40.1.1.2,flip.1] u(Z,u(x,U))=u(x,U). 787 [para_from,649.1.1,7.1.1.1.1,demod,27] u(D,c(u(c(D),c(Z))))=D. 805 [para_from,669.1.1,7.1.1.1.1,demod,33,189] u(Z,c(c(Z)))=Z. 905 [para_into,805.1.1,3.1.1] u(c(c(Z)),Z)=Z. 941 [para_into,57.1.1.2.1,905.1.1] u(c(u(c(c(Z)),U)),c(Z))=c(Z). 975 [para_from,597.1.1,49.1.1.2.1,demod,257,27] u(c(u(D,Z)),D)=U. 1299 [para_into,63.1.1.1.1,975.1.1,demod,33] u(Z,c(u(c(D),c(u(D,Z)))))=u(D,Z). 1434 [para_into,679.1.1.2,905.1.1,demod,672,flip.1] u(c(c(Z)),I)=I. 1438 [para_into,679.1.1.2,649.1.1,flip.1] u(c(D),I)=u(I,I). 1508 [para_into,65.1.1.2.1,975.1.1,demod,33] u(c(u(c(u(D,Z)),c(D))),Z)=u(D,Z). 1526 [para_into,65.1.1.2.1,69.1.1,demod,33] u(c(u(c(x),Z)),c(u(I,u(D,c(x)))))=x. 1571,1570 [para_from,1434.1.1,80.1.1.2,demod,46,flip.1] u(c(c(Z)),U)=U. 1591,1590 [back_demod,941,demod,1571,33,668,flip.1] c(Z)=U. 1610 [back_demod,787,demod,1591] u(D,c(u(c(D),U)))=D. 1624 [para_from,1590.1.1,35.1.1.1.2] c(k(c(x),U))=d(x,Z). 1632 [para_from,1590.1.1,188.1.1.2,demod,1591,48,249,1591] u(I,U)=U. 1650 [para_from,1590.1.1,35.1.1.1.1] c(k(U,c(x)))=d(Z,x). 1661,1660 [para_into,1632.1.1,90.1.1] u(D,u(I,I))=U. 1783,1782 [para_into,67.1.1.2,188.1.1,demod,8,flip.1] u(x,c(u(c(x),c(y))))=x. 1803 [para_into,67.1.1.2,7.1.1,demod,1783] u(c(u(c(x),y)),x)=x. 1825,1824 [para_from,1438.1.1,80.1.1.2,demod,1661,flip.1] u(c(D),U)=U. 1848,1847 [back_demod,1610,demod,1825,33] u(D,Z)=D. 1852 [back_demod,1508,demod,1848,189,1848] u(c(c(D)),Z)=D. 1856 [back_demod,1299,demod,1848,189,1848] u(Z,c(c(D)))=D. 1915 [para_from,71.1.1,67.1.1.1.1] u(c(u(I,u(D,u(c(x),y)))),u(c(u(c(x),c(u(y,U)))),z))=u(x,z). 1919 [para_from,71.1.1,63.1.1.1.1] u(c(u(I,u(D,u(c(x),y)))),c(u(c(u(y,U)),c(x))))=x. 1946 [para_from,1852.1.1,7.1.1.1.1,demod,1591] u(c(D),c(u(c(c(D)),U)))=c(D). 1959,1958 [para_into,72.1.1.2.2,1856.1.1,demod,235,30,692,flip.1] u(c(c(D)),U)=U. 1968 [back_demod,1946,demod,1959,33,650,flip.1] c(D)=I. 2003,2002 [para_from,1968.1.1,35.1.1.1.2,demod,22] c(c(x))=d(x,D). 2010 [para_from,1968.1.1,451.1.1.1.2,demod,22] u(r(D),U)=U. 2273 [back_demod,202,demod,2003,2003] u(k(r(c(x)),d(x,y)),d(y,D))=d(y,D). 2308 [para_from,73.1.1,61.1.1.1.1.2] u(c(u(c(u(c(u(I,u(D,c(x)))),u(c(x),Z))),x)),c(u(I,u(D,c(x)))))=u(c(u(I,u(D,c(x)))),u(c(x),Z)). 2310 [para_from,73.1.1,67.1.1.2.1.1,demod,6,6] u(c(u(c(u(I,u(D,c(x)))),u(c(x),Z))),u(c(x),y))=u(I,u(D,u(c(x),y))). 2331,2330 [para_into,2010.1.1,82.1.1] u(D,u(r(D),I))=U. 2335,2334 [para_from,2010.1.1,14.1.1.1,demod,144,13,144,2331] u(r(D),I)=U. 2353,2352 [back_demod,143,demod,2335] r(U)=U. 2495,2494 [para_into,2002.1.1.1,35.1.1] c(d(x,y))=d(k(c(x),c(y)),D). 2987,2986 [para_into,1624.1.1.1.1,1590.1.1] c(k(U,U))=d(Z,Z). 3105 [para_from,2986.1.1,23.1.1.1.2,demod,2353,33,33] u(k(U,d(Z,Z)),Z)=Z. 3131 [para_from,2986.1.1,49.1.1.2.1.2] u(c(u(Z,k(U,U))),c(u(Z,d(Z,Z))))=U. 3296 [para_into,1803.1.1.1.1,71.1.1] u(c(u(I,u(D,u(c(x),y)))),x)=x. 3303,3302 [para_into,1803.1.1.1.1,42.1.1] u(c(u(x,u(c(y),z))),y)=y. 3337,3336 [back_demod,2308,demod,3303,flip.1] u(c(u(I,u(D,c(x)))),u(c(x),Z))=u(c(x),c(u(I,u(D,c(x))))). 3380 [back_demod,2310,demod,3337] u(c(u(c(x),c(u(I,u(D,c(x)))))),u(c(x),y))=u(I,u(D,u(c(x),y))). 3469,3468 [para_from,1803.1.1,679.1.1.2,demod,672,1591,48,flip.1] u(c(u(I,u(D,x))),I)=I. 3484 [para_from,1803.1.1,71.1.1.2,demod,33,flip.1] u(I,u(D,u(x,c(u(Z,y)))))=u(x,U). 3497,3496 [para_from,1803.1.1,99.1.1.2.1,demod,1591,48,3469,46,33,1591,674,1591,48,flip.1] u(I,u(D,x))=U. 3529,3528 [back_demod,3484,demod,3497,flip.1] u(x,U)=U. 3532 [back_demod,3380,demod,3497,33,3497] u(c(u(c(x),Z)),u(c(x),y))=U. 3539,3538 [back_demod,3296,demod,3497,33] u(Z,x)=x. 3586,3585 [back_demod,1919,demod,3497,33,3529,33,3539,2003,3539] d(x,D)=x. 3590,3589 [back_demod,1915,demod,3497,33,3529,33,3539] u(c(u(c(x),Z)),y)=u(x,y). 3592,3591 [back_demod,1526,demod,3497,33,3590] u(x,Z)=x. 3596,3595 [back_demod,47,demod,3497] u(U,x)=U. 3647 [back_demod,535,demod,3539,3539,2003,3586,3529] u(c(x),u(y,x))=U. 3659 [back_demod,3131,demod,3539,2987,3539,2495,1591,1591,3586] u(d(Z,Z),k(U,U))=U. 3728,3727 [back_demod,2494,demod,3586] c(d(x,y))=k(c(x),c(y)). 3735 [back_demod,2273,demod,3586,3586] u(k(r(c(x)),d(x,y)),y)=y. 3808,3807 [back_demod,2002,demod,3586] c(c(x))=x. 3809 [back_demod,3532,demod,3592,3808] u(x,u(c(x),y))=U. 3814,3813 [back_demod,3105,demod,3592] k(U,d(Z,Z))=Z. 3907 [para_from,3807.1.1,35.1.1.1.2] c(k(c(x),y))=d(x,c(y)). 3910,3909 [para_from,3807.1.1,1650.1.1.1.2] c(k(U,x))=d(Z,c(x)). 3926,3925 [para_from,3807.1.1,35.1.1.1.1] c(k(x,c(y)))=d(c(x),y). 4012,4011 [para_from,3813.1.1,145.1.1.2,demod,3592,3529,3814] d(Z,Z)=Z. 4023 [back_demod,3659,demod,4012,3539] k(U,U)=U. 4080 [para_from,4023.1.1,10.1.1.1,flip.1] k(U,k(U,x))=k(U,x). 4884 [para_into,212.1.1.1,3807.1.1,demod,3926,3808] u(x,k(r(y),d(c(y),x)))=x. 6052 [para_from,4080.1.1,3909.1.1.1,demod,3910,3910,flip.1] d(Z,d(Z,c(x)))=d(Z,c(x)). 6317 [para_into,281.1.1.1.1.2,3809.1.1,demod,3529,33,3808,3539] c(u(c(x),c(u(y,u(x,z)))))=x. 6516,6515 [para_into,3907.1.1.1.1,3807.1.1] c(k(x,y))=d(c(x),c(y)). 6852 [para_into,4884.1.1.2.1,2352.1.1,demod,33] u(x,k(U,d(Z,x)))=x. 6856 [para_from,6852.1.1,3647.1.1.2,demod,6516,33,3728,1591] u(d(Z,k(U,c(x))),x)=U. 6866 [para_into,6856.1.1.1.2.2,3807.1.1] u(d(Z,k(U,x)),c(x))=U. 6890 [para_into,6052.1.1.2.2,3807.1.1,demod,3808] d(Z,d(Z,x))=d(Z,x). 6893,6892 [para_from,6890.1.1,3735.1.1.1.2,demod,1591,2353,149,3596] k(U,d(Z,x))=d(Z,x). 7006 [para_into,6317.1.1.1.2.1.2,6866.1.1,demod,3728,1591,6516,33,6893,3529,33,3592,3728,1591,3808,flip.1] d(Z,k(U,x))=k(U,x). 7008 [binary,7006.1,2.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 943 clauses generated 172061 clauses kept 3772 clauses forward subsumed 101189 clauses back subsumed 34 Kbytes malloced 4470 ----------- times (seconds) ----------- user CPU time 4.16 (0 hr, 0 min, 4 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 4 (0 hr, 0 min, 4 sec) 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 00:44:42 2003