----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sun Nov 30 22:07:29 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_seconds,20). assign(max_distinct_vars,3). 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("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("nDef.txt"). ------- start included file nDef.txt------- formula_list(usable). all x y (n(x,y)=c(u(c(x),c(y)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] n(x,y)=c(u(c(x),c(y))). end_of_list. ------- end included file nDef.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("booleanLaws.txt"). ------- start included file booleanLaws.txt------- include("1To4booleanLaws.txt"). ------- start included file 1To4booleanLaws.txt------- formula_list(usable). all x y z (i(x,u(y,z))->i(n(x,c(z)),y)). all x y z (i(x,y)->i(u(z,x),u(z,y))). all x y (x=u(n(x,c(y)),n(x,y))). -(all x y i(n(x,y),y)). end_of_list. -------> usable clausifies to: list(usable). 0 [] -i(x,u(y,z))|i(n(x,c(z)),y). 0 [] -i(x,y)|i(u(z,x),u(z,y)). 0 [] x=u(n(x,c(y)),n(x,y)). 0 [] -i(n($c2,$c1),$c1). end_of_list. ------- end included file 1To4booleanLaws.txt------- ------- end included file booleanLaws.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=11): 3 [] -i(x,u(y,z))|i(n(x,c(z)),y). ** KEPT (pick-wt=10): 4 [] -i(x,y)|i(u(z,x),u(z,y)). ** KEPT (pick-wt=5): 5 [] -i(n($c2,$c1),$c1). ------------> process sos: ** KEPT (pick-wt=7): 6 [] u(x,y)=u(y,x). ** KEPT (pick-wt=11): 8 [copy,7,flip.1] u(u(x,y),z)=u(x,u(y,z)). ---> New Demodulator: 9 [new_demod,8] u(u(x,y),z)=u(x,u(y,z)). ** KEPT (pick-wt=14): 10 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ---> New Demodulator: 11 [new_demod,10] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ** KEPT (pick-wt=10): 13 [copy,12,flip.1] c(u(c(x),c(y)))=n(x,y). ---> New Demodulator: 14 [new_demod,13] c(u(c(x),c(y)))=n(x,y). ** KEPT (pick-wt=4): 16 [copy,15,flip.1] c(I)=D. ---> New Demodulator: 17 [new_demod,16] c(I)=D. ** KEPT (pick-wt=5): 19 [copy,18,flip.1] u(I,D)=U. ---> New Demodulator: 20 [new_demod,19] u(I,D)=U. ** KEPT (pick-wt=4): 22 [copy,21,flip.1] c(U)=Z. ---> New Demodulator: 23 [new_demod,22] c(U)=Z. ** KEPT (pick-wt=10): 25 [copy,24,flip.1] u(n(x,c(y)),n(x,y))=x. ---> New Demodulator: 26 [new_demod,25] u(n(x,c(y)),n(x,y))=x. Following clause subsumed by 6 during input processing: 0 [copy,6,flip.1] u(x,y)=u(y,x). >>>> Starting back demodulation with 9. >>>> Starting back demodulation with 11. >>>> Starting back demodulation with 14. >> back demodulating 10 with 14. >>>> Starting back demodulation with 17. >>>> Starting back demodulation with 20. >>>> Starting back demodulation with 23. >>>> Starting back demodulation with 26. >>>> Starting back demodulation with 28. ======= end of input processing ======= =========== start of search =========== Resetting weight limit to 13. sos_size=2655 Resetting weight limit to 12. sos_size=2537 Resetting weight limit to 11. sos_size=2412 Resetting weight limit to 10. sos_size=1940 Resetting weight limit to 9. sos_size=1650 Resetting weight limit to 8. sos_size=695 ----> UNIT CONFLICT at 1.95 sec ----> 7706 [binary,7705.1,5.1] $F. Length of proof is 227. Level of proof is 45. ---------------- PROOF ---------------- 1 [] -i(x,y)|u(x,y)=y. 2 [] i(x,y)|u(x,y)!=y. 3 [] -i(x,u(y,z))|i(n(x,c(z)),y). 4 [] -i(x,y)|i(u(z,x),u(z,y)). 5 [] -i(n($c2,$c1),$c1). 6 [] u(x,y)=u(y,x). 7 [] u(x,u(y,z))=u(u(x,y),z). 9,8 [copy,7,flip.1] u(u(x,y),z)=u(x,u(y,z)). 10 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 12 [] n(x,y)=c(u(c(x),c(y))). 14,13 [copy,12,flip.1] c(u(c(x),c(y)))=n(x,y). 15 [] D=c(I). 17,16 [copy,15,flip.1] c(I)=D. 18 [] U=u(I,D). 20,19 [copy,18,flip.1] u(I,D)=U. 21 [] Z=c(U). 23,22 [copy,21,flip.1] c(U)=Z. 24 [] x=u(n(x,c(y)),n(x,y)). 25 [copy,24,flip.1] u(n(x,c(y)),n(x,y))=x. 27 [back_demod,10,demod,14] u(c(u(c(x),y)),n(x,y))=x. 32 [para_into,8.1.1.1,6.1.1,demod,9] u(x,u(y,z))=u(y,u(x,z)). 33 [para_into,8.1.1,6.1.1] u(x,u(y,z))=u(y,u(z,x)). 34 [copy,33,flip.1] u(x,u(y,z))=u(z,u(x,y)). 37,36 [para_into,19.1.1,6.1.1] u(D,I)=U. 39,38 [para_from,19.1.1,8.1.1.1] u(U,x)=u(I,u(D,x)). 41,40 [para_into,13.1.1.1.1,22.1.1] c(u(Z,c(x)))=n(U,x). 42 [para_into,13.1.1.1.1,16.1.1] c(u(D,c(x)))=n(I,x). 44 [para_into,13.1.1.1.1,13.1.1] c(u(n(x,y),c(z)))=n(u(c(x),c(y)),z). 46 [para_into,13.1.1.1.2,22.1.1] c(u(c(x),Z))=n(x,U). 48 [para_into,13.1.1.1.2,16.1.1] c(u(c(x),D))=n(x,I). 50 [para_into,13.1.1.1.2,13.1.1] c(u(c(x),n(y,z)))=n(x,u(c(y),c(z))). 52 [para_into,13.1.1.1,6.1.1,demod,14] n(x,y)=n(y,x). 55 [para_into,38.1.1,6.1.1] u(x,U)=u(I,u(D,x)). 56 [copy,55,flip.1] u(I,u(D,x))=u(x,U). 58,57 [para_into,25.1.1.1.2,22.1.1] u(n(x,Z),n(x,U))=x. 59 [para_into,25.1.1.1.2,16.1.1] u(n(x,D),n(x,I))=x. 65 [para_into,25.1.1.2,52.1.1] u(n(x,c(y)),n(y,x))=x. 70 [para_from,25.1.1,8.1.1.1,flip.1] u(n(x,c(y)),u(n(x,y),z))=u(x,z). 74 [para_into,40.1.1.1.2,22.1.1] c(u(Z,Z))=n(U,U). 76 [para_into,40.1.1.1.2,16.1.1] c(u(Z,D))=n(U,I). 79,78 [para_into,40.1.1.1.2,13.1.1] c(u(Z,n(x,y)))=n(U,u(c(x),c(y))). 84 [para_into,76.1.1.1,6.1.1] c(u(D,Z))=n(U,I). 90 [para_into,27.1.1.1.1.1,74.1.1] u(c(u(n(U,U),x)),n(u(Z,Z),x))=u(Z,Z). 95,94 [para_into,27.1.1.1.1.1,22.1.1] u(c(u(Z,x)),n(U,x))=U. 96 [para_into,27.1.1.1.1.1,16.1.1] u(c(u(D,x)),n(I,x))=I. 98 [para_into,27.1.1.1.1.1,13.1.1] u(c(u(n(x,y),z)),n(u(c(x),c(y)),z))=u(c(x),c(y)). 102 [para_into,27.1.1.1.1,6.1.1] u(c(u(x,c(y))),n(y,x))=y. 108 [para_from,27.1.1,8.1.1.1,flip.1] u(c(u(c(x),y)),u(n(x,y),z))=u(x,z). 127,126 [para_into,42.1.1.1.2,16.1.1] c(u(D,D))=n(I,I). 129,128 [para_into,42.1.1.1.2,13.1.1] c(u(D,n(x,y)))=n(I,u(c(x),c(y))). 136 [para_from,126.1.1,27.1.1.1.1.1] u(c(u(n(I,I),x)),n(u(D,D),x))=u(D,D). 154 [para_from,46.1.1,27.1.1.1] u(n(x,U),n(x,Z))=x. 159 [para_into,32.1.1.2,36.1.1] u(x,U)=u(D,u(x,I)). 160 [para_into,32.1.1.2,27.1.1,flip.1] u(c(u(c(x),y)),u(z,n(x,y)))=u(z,x). 162 [para_into,32.1.1.2,25.1.1,flip.1] u(n(x,c(y)),u(z,n(x,y)))=u(z,x). 164 [para_into,32.1.1.2,19.1.1] u(x,U)=u(I,u(x,D)). 169 [para_from,32.1.1,27.1.1.1.1] u(c(u(x,u(c(y),z))),n(y,u(x,z)))=y. 185 [para_into,48.1.1.1.1,13.1.1] c(u(n(x,y),D))=n(u(c(x),c(y)),I). 189 [para_from,48.1.1,27.1.1.1] u(n(x,I),n(x,D))=x. 195 [para_from,55.1.1,27.1.1.1.1] u(c(u(I,u(D,c(x)))),n(x,U))=x. 202 [para_into,56.1.1,32.1.1] u(D,u(I,x))=u(x,U). 204 [copy,202,flip.1] u(x,U)=u(D,u(I,x)). 205 [para_into,57.1.1.1,52.1.1] u(n(Z,x),n(x,U))=x. 207 [para_into,57.1.1.2,52.1.1] u(n(x,Z),n(U,x))=x. 209 [para_from,57.1.1,32.1.1.2,flip.1] u(n(x,Z),u(y,n(x,U)))=u(y,x). 216 [para_into,33.1.1.2,6.1.1] u(x,u(y,z))=u(z,u(y,x)). 223 [para_into,59.1.1.1,52.1.1] u(n(D,x),n(x,I))=x. 228 [para_from,59.1.1,32.1.1.2,flip.1] u(n(x,D),u(y,n(x,I)))=u(y,x). 230 [para_from,59.1.1,8.1.1.1,flip.1] u(n(x,D),u(n(x,I),y))=u(x,y). 232 [para_into,154.1.1.1,52.1.1] u(n(U,x),n(x,Z))=x. 243 [para_from,159.1.1,27.1.1.1.1] u(c(u(D,u(c(x),I))),n(x,U))=x. 251 [para_from,164.1.1,27.1.1.1.1] u(c(u(I,u(c(x),D))),n(x,U))=x. 275 [para_into,189.1.1.1,52.1.1] u(n(I,x),n(x,D))=x. 277 [para_into,189.1.1.2,52.1.1] u(n(x,I),n(D,x))=x. 315 [para_into,205.1.1.2,52.1.1] u(n(Z,x),n(U,x))=x. 325,324 [para_from,207.1.1,34.1.1.2,flip.1] u(n(U,x),u(y,n(x,Z)))=u(y,x). 331 [para_into,223.1.1.2,52.1.1] u(n(D,x),n(I,x))=x. 366 [para_into,232.1.1.2,52.1.1] u(n(U,x),n(Z,x))=x. 374 [para_into,275.1.1.2,52.1.1] u(n(I,x),n(D,x))=x. 475 [para_into,65.1.1,6.1.1] u(n(x,y),n(y,c(x)))=y. 515 [para_into,94.1.1.1.1,6.1.1] u(c(u(x,Z)),n(U,x))=U. 517 [para_into,94.1.1.2,52.1.1] u(c(u(Z,x)),n(x,U))=U. 519 [para_into,94.1.1,6.1.1] u(n(U,x),c(u(Z,x)))=U. 521 [para_from,94.1.1,50.1.1.1,demod,23,23,flip.1] n(u(Z,x),u(Z,c(x)))=Z. 547,546 [para_into,70.1.1.2,374.1.1] u(n(I,c(x)),x)=u(I,n(D,x)). 551,550 [para_into,70.1.1.2,331.1.1] u(n(D,c(x)),x)=u(D,n(I,x)). 553,552 [para_into,70.1.1.2,315.1.1] u(n(Z,c(x)),x)=u(Z,n(U,x)). 556 [para_into,70.1.1.2,275.1.1,demod,547] u(I,n(D,x))=u(I,n(x,D)). 562 [para_into,70.1.1.2,223.1.1,demod,551] u(D,n(I,x))=u(D,n(x,I)). 565 [para_into,70.1.1.2,205.1.1,demod,553] u(Z,n(U,x))=u(Z,n(x,U)). 577,576 [para_into,70.1.1.2,65.1.1] u(n(x,c(c(y))),x)=u(x,n(y,x)). 586 [para_into,70.1.1.2,25.1.1,demod,577] u(x,n(y,x))=u(x,n(x,y)). 587 [copy,556,flip.1] u(I,n(x,D))=u(I,n(D,x)). 589 [copy,562,flip.1] u(D,n(x,I))=u(D,n(I,x)). 590 [copy,565,flip.1] u(Z,n(x,U))=u(Z,n(U,x)). 603,602 [para_into,96.1.1.1.1,36.1.1,demod,23] u(Z,n(I,I))=I. 610 [para_into,96.1.1.1.1,6.1.1] u(c(u(x,D)),n(I,x))=I. 612 [para_into,96.1.1.2,52.1.1] u(c(u(D,x)),n(x,I))=I. 616 [para_from,96.1.1,50.1.1.1,demod,17,17,flip.1] n(u(D,x),u(D,c(x)))=D. 627 [para_into,602.1.1,6.1.1] u(n(I,I),Z)=I. 629 [para_from,602.1.1,94.1.1.1.1,demod,17] u(D,n(U,n(I,I)))=U. 641 [para_from,627.1.1,8.1.1.1,flip.1] u(n(I,I),u(Z,x))=u(I,x). 643 [para_into,629.1.1.2,52.1.1] u(D,n(n(I,I),U))=U. 658 [para_into,78.1.1.1,602.1.1,demod,17,17,17,flip.1] n(U,u(D,D))=D. 671,670 [para_into,658.1.1,52.1.1] n(u(D,D),U)=D. 675,674 [para_from,658.1.1,315.1.1.2] u(n(Z,u(D,D)),D)=u(D,D). 676 [para_from,658.1.1,232.1.1.1] u(D,n(u(D,D),Z))=u(D,D). 703 [para_from,643.1.1,96.1.1.1.1,demod,23] u(Z,n(I,n(n(I,I),U)))=I. 1022 [para_from,515.1.1,50.1.1.1,demod,23,23,flip.1] n(u(x,Z),u(Z,c(x)))=Z. 1043 [para_into,517.1.1,6.1.1] u(n(x,U),c(u(Z,x)))=U. 1045 [para_from,517.1.1,50.1.1.1,demod,23,23,flip.1] n(u(Z,x),u(c(x),Z))=Z. 1068 [para_into,519.1.1.2.1,55.1.1] u(n(U,U),c(u(I,u(D,Z))))=U. 1199 [para_into,521.1.1.1,55.1.1,demod,23] n(u(I,u(D,Z)),u(Z,Z))=Z. 1207 [para_into,521.1.1.2.2,126.1.1,demod,603] n(u(Z,u(D,D)),I)=Z. 1255 [para_into,1207.1.1.1,33.1.1] n(u(D,u(D,Z)),I)=Z. 1400 [para_into,1255.1.1,52.1.1] n(I,u(D,u(D,Z)))=Z. 1476 [para_into,102.1.1.2,52.1.1] u(c(u(x,c(y))),n(x,y))=y. 1478 [para_into,102.1.1,6.1.1] u(n(x,y),c(u(y,c(x))))=x. 1551 [para_from,1400.1.1,98.1.1.1.1.1,demod,17,17] u(c(u(Z,x)),n(u(D,c(u(D,u(D,Z)))),x))=u(D,c(u(D,u(D,Z)))). 1556,1555 [para_from,1400.1.1,44.1.1.1.1,demod,41,17,flip.1] n(u(D,c(u(D,u(D,Z)))),x)=n(U,x). 1557 [back_demod,1551,demod,1556,95,flip.1] u(D,c(u(D,u(D,Z))))=U. 1628 [para_into,610.1.1.2,52.1.1] u(c(u(x,D)),n(x,I))=I. 1663 [para_into,612.1.1,6.1.1] u(n(x,I),c(u(D,x)))=I. 1665 [para_from,612.1.1,50.1.1.1,demod,17,17,flip.1] n(u(D,x),u(c(x),D))=D. 1796 [para_into,616.1.1.1,204.1.1,demod,20,23] n(u(D,U),u(D,Z))=D. 1852 [para_into,1796.1.1,52.1.1] n(u(D,Z),u(D,U))=D. 1874 [para_into,1852.1.1.2,164.1.1] n(u(D,Z),u(I,u(D,D)))=D. 1982,1981 [para_into,108.1.1.2,475.1.1] u(c(u(c(x),y)),y)=u(x,n(y,c(x))). 1989,1988 [para_into,108.1.1.2,366.1.1,demod,23,39] u(c(u(Z,x)),x)=u(I,u(D,n(Z,x))). 2007,2006 [para_into,108.1.1.2,65.1.1,demod,14] u(n(x,y),x)=u(x,n(y,x)). 2175,2174 [para_from,1043.1.1,108.1.1.2,demod,1982,flip.1] u(x,c(u(Z,x)))=u(x,n(U,c(x))). 2179,2178 [para_from,1043.1.1,70.1.1.2,demod,23,2175,flip.1] u(x,n(U,c(x)))=u(n(x,Z),U). 2223 [para_from,1045.1.1,90.1.1.2] u(c(u(n(U,U),u(c(Z),Z))),Z)=u(Z,Z). 2369 [para_from,1628.1.1,50.1.1.1,demod,17,17,flip.1] n(u(x,D),u(c(x),D))=D. 2481 [para_into,1663.1.1.2.1,643.1.1,demod,23] u(n(n(n(I,I),U),I),Z)=I. 2530 [para_into,1665.1.1.2.1,84.1.1] n(u(D,u(D,Z)),u(n(U,I),D))=D. 3364,3363 [para_into,562.1.1,6.1.1] u(n(I,x),D)=u(D,n(x,I)). 3423 [para_into,136.1.1.2,2369.1.1] u(c(u(n(I,I),u(c(D),D))),D)=u(D,D). 3444,3443 [para_into,565.1.1,6.1.1] u(n(U,x),Z)=u(Z,n(x,U)). 3510,3509 [para_from,586.1.1,202.1.1.2,flip.1] u(n(x,I),U)=u(D,u(I,n(I,x))). 3574,3573 [para_into,587.1.1,6.1.1] u(n(x,D),I)=u(I,n(D,x)). 3590,3589 [para_into,589.1.1,6.1.1] u(n(x,I),D)=u(D,n(I,x)). 3605 [back_demod,2530,demod,3590] n(u(D,u(D,Z)),u(D,n(I,U)))=D. 3694,3693 [para_into,590.1.1,6.1.1] u(n(x,U),Z)=u(Z,n(U,x)). 4043,4042 [para_from,703.1.1,641.1.1.2,demod,2007,flip.1] u(I,n(I,n(n(I,I),U)))=u(I,n(I,I)). 4163,4162 [para_into,160.1.1.2,517.1.1,demod,1982,2179,1989] u(n(x,Z),U)=u(I,u(D,n(Z,x))). 4664 [para_into,169.1.1.2,521.1.1] u(c(u(Z,u(c(u(Z,x)),c(x)))),Z)=u(Z,x). 4667,4666 [para_from,169.1.1,162.1.1.2,demod,2007,flip.1] u(c(u(x,u(c(y),z))),y)=u(y,n(c(u(x,z)),y)). 4676 [back_demod,3423,demod,4667,3590,129,17,17] u(D,n(n(I,u(D,D)),D))=u(D,D). 4678 [back_demod,2223,demod,4667,3694,79,23,23] u(Z,n(n(U,u(Z,Z)),Z))=u(Z,Z). 4734 [para_into,1476.1.1,6.1.1] u(n(x,y),c(u(x,c(y))))=y. 4901 [para_into,1478.1.1.1,521.1.1,demod,9] u(Z,c(u(Z,u(c(x),c(u(Z,x))))))=u(Z,x). 5735 [para_into,195.1.1.1.1.2,1557.1.1] u(c(u(I,U)),n(u(D,u(D,Z)),U))=u(D,u(D,Z)). 5941 [para_into,209.1.1.2,374.1.1,demod,4163,3364] u(I,u(D,n(Z,D)))=u(D,n(U,I)). 5944,5943 [para_into,209.1.1.2,366.1.1,demod,4163,3694,flip.1] u(Z,n(U,U))=u(I,u(D,n(Z,Z))). 6041 [para_into,546.1.1,159.1.1,demod,23,2007] u(D,u(I,n(Z,I)))=u(I,n(D,U)). 6049 [para_into,550.1.1,204.1.1,demod,23] u(D,u(I,n(D,Z)))=u(D,n(I,U)). 6090,6089 [para_into,228.1.1.2,366.1.1,demod,3574,3444,flip.1] u(Z,n(I,U))=u(I,n(D,Z)). 6108,6107 [para_into,230.1.1.2,3443.1.1,demod,6090,325,20,39,flip.1] u(I,u(D,Z))=U. 6132,6131 [back_demod,1199,demod,6108] n(U,u(Z,Z))=Z. 6134,6133 [back_demod,1068,demod,6108,23,3694,5944] u(I,u(D,n(Z,Z)))=U. 6135 [back_demod,4678,demod,6132] u(Z,n(Z,Z))=u(Z,Z). 6137 [back_demod,5943,demod,6134] u(Z,n(U,U))=U. 6141 [para_into,6107.1.1,216.1.1,demod,37] u(Z,U)=U. 6146,6145 [para_into,6107.1.1,32.1.1] u(D,u(I,Z))=U. 6184 [hyper,6141,2] i(Z,U). 6190,6189 [para_from,6141.1.1,641.1.1.2,demod,3510] u(D,u(I,n(I,I)))=u(I,U). 6194 [para_from,6141.1.1,32.1.1.2,flip.1] u(Z,u(x,U))=u(x,U). 6200 [hyper,6184,4] i(u(x,Z),u(x,U)). 6294 [hyper,6200,3,demod,23] i(n(u(x,Z),Z),x). 6297 [para_into,6200.1.1,2481.1.1,demod,3510,4043,6190] i(I,u(I,U)). 6308 [hyper,6297,3,demod,23] i(n(I,Z),I). 6313,6312 [hyper,6308,1,demod,2007] u(I,n(Z,I))=I. 6314 [back_demod,6041,demod,6313,37,flip.1] u(I,n(D,U))=U. 6337 [para_into,6294.1.1.1,627.1.1] i(n(I,Z),n(I,I)). 6342 [para_into,6294.1.1.1,6.1.1] i(n(u(Z,x),Z),x). 6343 [para_into,6294.1.1,52.1.1] i(n(Z,u(x,Z)),x). 6367,6366 [para_into,243.1.1.1.1.2.1,126.1.1,demod,2007,6190,671] u(c(u(I,U)),D)=u(D,D). 6369,6368 [para_from,6312.1.1,228.1.1.2,demod,3574] u(I,n(D,Z))=u(I,Z). 6394,6393 [back_demod,6089,demod,6369] u(Z,n(I,U))=u(I,Z). 6396,6395 [back_demod,6049,demod,6369,6146,flip.1] u(D,n(I,U))=U. 6407,6406 [back_demod,3605,demod,6396] n(u(D,u(D,Z)),U)=D. 6419,6418 [back_demod,5735,demod,6407,6367,flip.1] u(D,u(D,Z))=u(D,D). 6481,6480 [back_demod,1400,demod,6419] n(I,u(D,D))=Z. 6497,6496 [back_demod,4676,demod,6481] u(D,n(Z,D))=u(D,D). 6499,6498 [back_demod,5941,demod,6497] u(I,u(D,D))=u(D,n(U,I)). 6502 [back_demod,1874,demod,6499] n(u(D,Z),u(D,n(U,I)))=D. 6513,6512 [para_from,6314.1.1,209.1.1.2,demod,4163,6497,6499,20] u(D,n(U,I))=U. 6522,6521 [back_demod,6502,demod,6513] n(u(D,Z),U)=D. 6524,6523 [back_demod,6498,demod,6513] u(I,u(D,D))=U. 6552 [para_into,6337.1.1,52.1.1] i(n(Z,I),n(I,I)). 6556 [para_into,6342.1.1.1,6137.1.1] i(n(U,Z),n(U,U)). 6597 [para_into,251.1.1.1.1.2.1,84.1.1,demod,3590,6396,6522,6367,flip.1] u(D,Z)=u(D,D). 6601 [para_into,251.1.1.1.1.2.1,16.1.1,demod,6524,23,6394] u(I,Z)=I. 6680,6679 [para_into,6601.1.1,6.1.1] u(Z,I)=I. 6685 [hyper,6679,2] i(Z,I). 6688 [hyper,6685,4] i(u(x,Z),u(x,I)). 6775,6774 [hyper,6552,1] u(n(Z,I),n(I,I))=n(I,I). 6777 [hyper,6556,1,demod,58,flip.1] n(U,U)=U. 6805 [para_from,6777.1.1,185.1.1.1.1,demod,39,6524,23,23,23,flip.1] n(u(Z,Z),I)=Z. 6859 [para_from,6597.1.1,6343.1.1.2] i(n(Z,u(D,D)),D). 6867 [para_from,6597.1.1,1022.1.1.1] n(u(D,D),u(Z,c(D)))=Z. 6888,6887 [para_from,6597.1.1,1663.1.1.2.1,demod,127,6775] n(I,I)=I. 6940 [back_demod,126,demod,6888] c(u(D,D))=I. 6977 [hyper,6688,3,demod,17] i(n(u(x,Z),D),x). 7012 [para_from,6805.1.1,277.1.1.1] u(Z,n(D,u(Z,Z)))=u(Z,Z). 7016 [para_from,6805.1.1,59.1.1.2] u(n(u(Z,Z),D),Z)=u(Z,Z). 7023,7022 [hyper,6859,1,demod,675] u(D,D)=D. 7035,7034 [back_demod,6940,demod,7023] c(D)=I. 7053,7052 [back_demod,6867,demod,7023,7035,6680] n(D,I)=Z. 7093 [back_demod,676,demod,7023,7023] u(D,n(D,Z))=D. 7122 [hyper,7022,2] i(D,D). 7132 [hyper,7122,4] i(u(x,D),u(x,D)). 7139,7138 [hyper,6977,1] u(n(u(x,Z),D),x)=x. 7141,7140 [back_demod,7016,demod,7139,flip.1] u(Z,Z)=Z. 7145,7144 [back_demod,7012,demod,7141,7141] u(Z,n(D,Z))=Z. 7163,7162 [back_demod,6135,demod,7141] u(Z,n(Z,Z))=Z. 7169 [para_into,6977.1.1.1,6.1.1] i(n(u(Z,x),D),x). 7179 [hyper,7140,2] i(Z,Z). 7186,7185 [para_from,7140.1.1,8.1.1.1,flip.1] u(Z,u(Z,x))=u(Z,x). 7187 [hyper,7179,4] i(u(x,Z),u(x,Z)). 7219 [hyper,7132,3,demod,7035] i(n(u(x,D),I),x). 7244 [para_into,7169.1.1.1,7162.1.1] i(n(Z,D),n(Z,Z)). 7256 [para_into,7187.1.2,6.1.1] i(u(x,Z),u(Z,x)). 7286 [para_into,7219.1.1.1,6.1.1] i(n(u(D,x),I),x). 7316 [para_into,7244.1.1,52.1.1] i(n(D,Z),n(Z,Z)). 7326 [hyper,7256,1,demod,9,7186] u(x,u(Z,x))=u(Z,x). 7337 [para_into,7286.1.1.1,7093.1.1,demod,7053] i(Z,n(D,Z)). 7345,7344 [hyper,7337,1,demod,7145,flip.1] n(D,Z)=Z. 7346 [back_demod,7316,demod,7345] i(Z,n(Z,Z)). 7352,7351 [hyper,7346,1,demod,7163,flip.1] n(Z,Z)=Z. 7434 [hyper,6194,2] i(Z,u(x,U)). 7436 [hyper,7434,3,demod,23,7352] i(Z,x). 7437 [hyper,7436,4] i(u(x,Z),u(x,y)). 7440,7439 [hyper,7436,1] u(Z,x)=x. 7457,7456 [back_demod,7326,demod,7440,7440] u(x,x)=x. 7502,7501 [back_demod,4901,demod,7440,7457,7440,7440,7440] c(c(x))=x. 7508,7507 [back_demod,4664,demod,7440,7457,7440,7502,7440] u(x,Z)=x. 7537 [back_demod,7437,demod,7508] i(x,u(x,y)). 7705 [para_into,7537.1.2,4734.1.1] i(n(x,y),y). 7706 [binary,7705.1,5.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 553 clauses generated 28943 clauses kept 4451 clauses forward subsumed 15852 clauses back subsumed 83 Kbytes malloced 4534 ----------- times (seconds) ----------- user CPU time 2.34 (0 hr, 0 min, 2 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 2 (0 hr, 0 min, 2 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 Sun Nov 30 22:07:31 2003