----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sun Nov 30 22:07:03 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)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] -i(x,u(y,z))|i(n(x,c(z)),y). 0 [] i($c3,$c2). 0 [] -i(u($c1,$c3),u($c1,$c2)). 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=7): 4 [] -i(u($c1,$c3),u($c1,$c2)). ------------> process sos: ** 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=10): 12 [copy,11,flip.1] c(u(c(x),c(y)))=n(x,y). ---> New Demodulator: 13 [new_demod,12] c(u(c(x),c(y)))=n(x,y). ** KEPT (pick-wt=4): 15 [copy,14,flip.1] c(I)=D. ---> New Demodulator: 16 [new_demod,15] c(I)=D. ** KEPT (pick-wt=5): 18 [copy,17,flip.1] u(I,D)=U. ---> New Demodulator: 19 [new_demod,18] u(I,D)=U. ** KEPT (pick-wt=4): 21 [copy,20,flip.1] c(U)=Z. ---> New Demodulator: 22 [new_demod,21] c(U)=Z. ** KEPT (pick-wt=3): 23 [] i($c3,$c2). 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. >> back demodulating 9 with 13. >>>> Starting back demodulation with 16. >>>> Starting back demodulation with 19. >>>> Starting back demodulation with 22. >>>> Starting back demodulation with 25. ======= end of input processing ======= =========== start of search =========== Resetting weight limit to 10. sos_size=1550 Resetting weight limit to 8. sos_size=750 ----> UNIT CONFLICT at 1.41 sec ----> 7444 [binary,7443.1,4.1] $F. Length of proof is 208. Level of proof is 41. ---------------- 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(u($c1,$c3),u($c1,$c2)). 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)). 9 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 11 [] n(x,y)=c(u(c(x),c(y))). 13,12 [copy,11,flip.1] c(u(c(x),c(y)))=n(x,y). 14 [] D=c(I). 16,15 [copy,14,flip.1] c(I)=D. 17 [] U=u(I,D). 19,18 [copy,17,flip.1] u(I,D)=U. 20 [] Z=c(U). 22,21 [copy,20,flip.1] c(U)=Z. 23 [] i($c3,$c2). 24 [back_demod,9,demod,13] u(c(u(c(x),y)),n(x,y))=x. 30,29 [hyper,23,1] u($c3,$c2)=$c2. 33 [para_into,7.1.1.1,5.1.1,demod,8] u(x,u(y,z))=u(y,u(x,z)). 34 [para_into,7.1.1,5.1.1] u(x,u(y,z))=u(y,u(z,x)). 35 [copy,34,flip.1] u(x,u(y,z))=u(z,u(x,y)). 38,37 [para_into,18.1.1,5.1.1] u(D,I)=U. 39 [para_from,18.1.1,7.1.1.1] u(U,x)=u(I,u(D,x)). 42 [para_into,29.1.1,5.1.1] u($c2,$c3)=$c2. 44 [para_from,29.1.1,7.1.1.1,flip.1] u($c3,u($c2,x))=u($c2,x). 47,46 [para_into,12.1.1.1.1,21.1.1] c(u(Z,c(x)))=n(U,x). 48 [para_into,12.1.1.1.1,15.1.1] c(u(D,c(x)))=n(I,x). 51,50 [para_into,12.1.1.1.1,12.1.1] c(u(n(x,y),c(z)))=n(u(c(x),c(y)),z). 52 [para_into,12.1.1.1.2,21.1.1] c(u(c(x),Z))=n(x,U). 55,54 [para_into,12.1.1.1.2,15.1.1] c(u(c(x),D))=n(x,I). 57,56 [para_into,12.1.1.1.2,12.1.1] c(u(c(x),n(y,z)))=n(x,u(c(y),c(z))). 58 [para_into,12.1.1.1,5.1.1,demod,13] n(x,y)=n(y,x). 60 [para_from,42.1.1,7.1.1.1,flip.1] u($c2,u($c3,x))=u($c2,x). 62 [para_into,24.1.1.1.1.1,21.1.1] u(c(u(Z,x)),n(U,x))=U. 66 [para_into,24.1.1.1.1.1,12.1.1] u(c(u(n(x,y),z)),n(u(c(x),c(y)),z))=u(c(x),c(y)). 68 [para_into,24.1.1.1.1,24.1.1] u(c(x),n(u(c(x),y),n(x,y)))=u(c(x),y). 70 [para_into,24.1.1.1.1,5.1.1] u(c(u(x,c(y))),n(y,x))=y. 72 [para_into,24.1.1.1,12.1.1] u(n(x,y),n(x,c(y)))=x. 75 [para_into,24.1.1,5.1.1] u(n(x,y),c(u(c(x),y)))=x. 77 [para_from,24.1.1,7.1.1.1,flip.1] u(c(u(c(x),y)),u(n(x,y),z))=u(x,z). 80 [para_from,58.1.1,24.1.1.2] u(c(u(c(x),y)),n(y,x))=x. 82 [para_into,33.1.1.2,42.1.1,flip.1] u($c2,u(x,$c3))=u(x,$c2). 87 [para_into,33.1.1.2,24.1.1,flip.1] u(c(u(c(x),y)),u(z,n(x,y)))=u(z,x). 89 [para_into,33.1.1.2,18.1.1] u(x,U)=u(I,u(x,D)). 92 [copy,89,flip.1] u(I,u(x,D))=u(x,U). 99 [hyper,44,2] i($c3,u($c2,x)). 102 [hyper,99,3] i(n($c3,c(x)),$c2). 103 [para_into,99.1.2,33.1.1] i($c3,u(x,u($c2,y))). 104 [para_into,99.1.2,5.1.1] i($c3,u(x,$c2)). 108 [para_into,34.1.1,39.1.1] u(I,u(D,u(x,y)))=u(x,u(y,U)). 115 [para_from,34.1.1,24.1.1.1.1] u(c(u(x,u(y,c(z)))),n(z,u(x,y)))=z. 117 [hyper,104,3] i(n($c3,c($c2)),x). 118 [hyper,102,1] u(n($c3,c(x)),$c2)=$c2. 136 [para_from,35.1.1,24.1.1.1.1] u(c(u(x,u(c(y),z))),n(y,u(z,x)))=y. 144,143 [hyper,117,1] u(n($c3,c($c2)),x)=x. 145 [para_into,117.1.1,58.1.1] i(n(c($c2),$c3),x). 151 [para_into,46.1.1.1.2,21.1.1] c(u(Z,Z))=n(U,U). 155 [para_into,46.1.1.1.2,12.1.1] c(u(Z,n(x,y)))=n(U,u(c(x),c(y))). 161,160 [hyper,145,1] u(n(c($c2),$c3),x)=x. 162 [hyper,103,3] i(n($c3,c(u($c2,x))),y). 176 [para_into,48.1.1.1.2,12.1.1] c(u(D,n(x,y)))=n(I,u(c(x),c(y))). 216 [para_into,50.1.1.1.1,58.1.1,demod,51] n(u(c(x),c(y)),z)=n(u(c(y),c(x)),z). 220,219 [para_into,50.1.1.1.2,46.1.1] c(u(n(x,y),n(U,z)))=n(u(c(x),c(y)),u(Z,c(z))). 221 [para_into,50.1.1.1.2,21.1.1] c(u(n(x,y),Z))=n(u(c(x),c(y)),U). 241,240 [para_from,52.1.1,50.1.1.1.2] c(u(n(x,y),n(z,U)))=n(u(c(x),c(y)),u(c(z),Z)). 257,256 [para_into,143.1.1,5.1.1] u(x,n($c3,c($c2)))=x. 258 [para_from,143.1.1,50.1.1.1] c(c(x))=n(u(c($c3),c(c($c2))),x). 259 [copy,258,flip.1] n(u(c($c3),c(c($c2))),x)=c(c(x)). 281 [para_into,160.1.1,5.1.1] u(x,n(c($c2),$c3))=x. 283 [para_from,160.1.1,50.1.1.1] c(c(x))=n(u(c(c($c2)),c($c3)),x). 284 [copy,283,flip.1] n(u(c(c($c2)),c($c3)),x)=c(c(x)). 286 [hyper,162,1] u(n($c3,c(u($c2,x))),y)=y. 303 [para_into,56.1.1.1.2,58.1.1,demod,57] n(x,u(c(y),c(z)))=n(x,u(c(z),c(y))). 304 [para_into,56.1.1.1,24.1.1,flip.1] n(u(c(x),y),u(c(x),c(y)))=c(x). 346 [para_into,256.1.1,24.1.1,demod,13,flip.1] n($c3,$c2)=$c3. 352 [para_into,346.1.1,58.1.1] n($c2,$c3)=$c3. 379 [para_from,62.1.1,56.1.1.1,demod,22,22,flip.1] n(u(Z,x),u(Z,c(x)))=Z. 692 [para_into,70.1.1.1,48.1.1] u(n(I,x),n(x,D))=x. 694 [para_into,70.1.1.1,46.1.1] u(n(U,x),n(x,Z))=x. 765 [para_into,72.1.1.1,352.1.1] u($c3,n($c2,c($c3)))=$c2. 839 [para_into,75.1.1.1,346.1.1] u($c3,c(u(c($c3),$c2)))=$c3. 879 [para_into,75.1.1.2.1,62.1.1,demod,22] u(n(u(Z,x),n(U,x)),Z)=u(Z,x). 889 [para_into,75.1.1.2,54.1.1] u(n(x,D),n(x,I))=x. 891 [para_into,75.1.1.2,52.1.1] u(n(x,Z),n(x,U))=x. 903 [para_into,765.1.1.2,58.1.1] u($c3,n(c($c3),$c2))=$c2. 992 [para_into,77.1.1.2,118.1.1,demod,13,30] u(n($c3,x),$c2)=$c2. 1003,1002 [para_into,77.1.1.2,72.1.1] u(c(u(c(x),y)),x)=u(x,n(x,c(y))). 1015 [para_from,992.1.1,77.1.1.2,demod,30] u(c(u(c($c3),x)),$c2)=$c2. 1090 [para_into,80.1.1.1,54.1.1] u(n(x,I),n(D,x))=x. 1181 [para_from,903.1.1,87.1.1.2] u(c(u(c(c($c3)),$c2)),$c2)=u($c3,c($c3)). 1364 [para_into,692.1.1.2,58.1.1] u(n(I,x),n(D,x))=x. 1400 [para_into,694.1.1,5.1.1] u(n(x,Z),n(U,x))=x. 1427 [para_into,839.1.1.2.1,5.1.1] u($c3,c(u($c2,c($c3))))=$c3. 1440 [para_into,889.1.1.1,58.1.1] u(n(D,x),n(x,I))=x. 1481 [para_into,891.1.1.1,58.1.1] u(n(Z,x),n(x,U))=x. 1512,1511 [para_into,1015.1.1.1.1,281.1.1] u(c(c($c3)),$c2)=$c2. 1525 [back_demod,1181,demod,1512,flip.1] u($c3,c($c3))=u(c($c2),$c2). 1677,1676 [para_from,1090.1.1,87.1.1.2] u(c(u(c(D),x)),x)=u(n(x,I),D). 1771 [para_into,1364.1.1,5.1.1] u(n(D,x),n(I,x))=x. 1828 [para_into,115.1.1.2.2,108.1.1,demod,8,8] u(c(u(I,u(D,u(x,u(y,c(z)))))),n(z,u(x,u(y,U))))=z. 1891 [para_from,1427.1.1,70.1.1.1.1] u(c($c3),n(u($c2,c($c3)),$c3))=u($c2,c($c3)). 1911,1910 [para_from,1440.1.1,87.1.1.2,demod,1003,16,flip.1] u(n(D,x),x)=u(x,n(x,D)). 2038,2037 [para_into,1525.1.1,5.1.1] u(c($c3),$c3)=u(c($c2),$c2). 2047,2046 [para_from,1525.1.1,60.1.1.2,flip.1] u($c2,c($c3))=u($c2,u(c($c2),$c2)). 2069 [back_demod,1891,demod,2047,2047] u(c($c3),n(u($c2,u(c($c2),$c2)),$c3))=u($c2,u(c($c2),$c2)). 2150 [para_from,136.1.1,108.1.1.2.2,flip.1] u(c(u(x,u(c(y),z))),u(n(y,u(z,x)),U))=u(I,u(D,y)). 2199 [para_into,155.1.1.1,256.1.1,flip.1] n(U,u(c($c3),c(c($c2))))=c(Z). 2354,2353 [para_into,176.1.1.1,256.1.1,flip.1] n(I,u(c($c3),c(c($c2))))=c(D). 2380,2379 [para_from,1771.1.1,77.1.1.2,demod,1677] u(n(x,I),D)=u(D,n(I,x)). 2390,2389 [back_demod,1676,demod,2380] u(c(u(c(D),x)),x)=u(D,n(I,x)). 2491 [para_from,2037.1.1,82.1.1.2,flip.1] u(c($c3),$c2)=u($c2,u(c($c2),$c2)). 2575,2574 [para_into,216.1.1.1.1,21.1.1,demod,22,flip.1] n(u(c(x),Z),y)=n(u(Z,c(x)),y). 2741 [para_into,286.1.1,75.1.1,demod,13,flip.1] n($c3,u($c2,x))=$c3. 2748,2747 [para_into,219.1.1.1.2,58.1.1,demod,241] n(u(c(x),c(y)),u(c(z),Z))=n(u(c(x),c(y)),u(Z,c(z))). 2752,2751 [para_into,219.1.1.1,1481.1.1,demod,22,22,22,2575,flip.1] n(u(Z,c(Z)),u(Z,Z))=Z. 2778,2777 [para_into,2741.1.1,58.1.1] n(u($c2,x),$c3)=$c3. 2780,2779 [back_demod,2069,demod,2778,2038,flip.1] u($c2,u(c($c2),$c2))=u(c($c2),$c2). 2783 [back_demod,2491,demod,2780] u(c($c3),$c2)=u(c($c2),$c2). 2813 [para_from,2741.1.1,68.1.1.2.2] u(c($c3),n(u(c($c3),u($c2,x)),$c3))=u(c($c3),u($c2,x)). 2860,2859 [para_into,2777.1.1.1,35.1.1] n(u(x,u($c2,y)),$c3)=$c3. 2864,2863 [back_demod,2813,demod,2860,2038,flip.1] u(c($c3),u($c2,x))=u(c($c2),$c2). 2925,2924 [para_into,221.1.1.1,143.1.1,flip.1] n(u(c($c3),c(c($c2))),U)=c(Z). 3057 [para_from,2783.1.1,34.1.1.2,demod,2864] u(x,u(c($c2),$c2))=u(c($c2),$c2). 3310,3309 [para_from,259.1.1,692.1.1.2,demod,2354] u(c(D),c(c(D)))=u(c($c3),c(c($c2))). 3335 [para_from,259.1.1,70.1.1.2,demod,13,257] u(c(x),c(c(x)))=u(c($c3),c(c($c2))). 3338 [para_from,259.1.1,75.1.1.1,demod,13,144] u(c(c(x)),c(x))=u(c($c3),c(c($c2))). 3339 [para_from,259.1.1,68.1.1.2.2,demod,13,13,144,144,13,144] n(x,c(c(x)))=x. 3345 [copy,3338,flip.1] u(c($c3),c(c($c2)))=u(c(c(x)),c(x)). 3367 [para_into,3339.1.1.2.1,151.1.1] n(u(Z,Z),c(n(U,U)))=u(Z,Z). 3382,3381 [para_into,3339.1.1.2.1,21.1.1] n(U,c(Z))=U. 3383 [para_into,3339.1.1.2.1,15.1.1] n(I,c(D))=I. 3393 [para_into,3339.1.1,58.1.1] n(c(c(x)),x)=x. 3413 [para_from,3339.1.1,72.1.1.2] u(n(x,c(x)),x)=x. 3417 [para_from,3339.1.1,70.1.1.2,demod,13] u(n(c(x),x),x)=x. 3434,3433 [para_from,3339.1.1,1400.1.1.2,demod,22,22] u(n(c(Z),Z),U)=c(Z). 3488 [para_from,3381.1.1,155.1.1.1.2,demod,22,flip.1] n(U,u(Z,c(c(Z))))=c(u(Z,U)). 3509 [para_from,3383.1.1,70.1.1.2,demod,16,55,1911] u(I,n(I,D))=I. 3783 [para_into,283.1.1.1,52.1.1,demod,2748] c(n(x,U))=n(u(c(c($c2)),c($c3)),u(Z,c(x))). 3794 [copy,3783,flip.1] n(u(c(c($c2)),c($c3)),u(Z,c(x)))=c(n(x,U)). 3803 [para_from,283.1.1,3393.1.1.1] n(n(u(c(c($c2)),c($c3)),x),x)=x. 3805 [para_from,283.1.1,3339.1.1.2] n(x,n(u(c(c($c2)),c($c3)),x))=x. 3815 [para_from,283.1.1,259.1.1.1.2] n(u(c($c3),n(u(c(c($c2)),c($c3)),$c2)),x)=c(c(x)). 3856 [copy,3815,flip.1] c(c(x))=n(u(c($c3),n(u(c(c($c2)),c($c3)),$c2)),x). 3859 [para_into,3509.1.1.2,58.1.1] u(I,n(D,I))=I. 3901 [para_into,284.1.1.1.1,258.1.1] n(u(n(u(c($c3),c(c($c2))),$c2),c($c3)),x)=c(c(x)). 3902 [para_into,284.1.1,3339.1.1,demod,13,flip.1] c(c(c(n(c($c2),$c3))))=u(c(c($c2)),c($c3)). 3905 [copy,3901,flip.1] c(c(x))=n(u(n(u(c($c3),c(c($c2))),$c2),c($c3)),x). 3925 [para_from,284.1.1,75.1.1.1,demod,13,161] u(c(c(x)),c(x))=u(c(c($c2)),c($c3)). 3930 [copy,3925,flip.1] u(c(c($c2)),c($c3))=u(c(c(x)),c(x)). 3932 [para_from,3859.1.1,87.1.1.2,demod,2390,19] u(D,n(I,I))=U. 3973,3972 [para_from,3932.1.1,87.1.1.2,demod,16,38,22,38] u(Z,U)=U. 3995 [back_demod,3488,demod,3973,22] n(U,u(Z,c(c(Z))))=Z. 4024 [para_from,3972.1.1,33.1.1.2,flip.1] u(Z,u(x,U))=u(x,U). 4282 [para_from,3413.1.1,92.1.1.2,demod,19,flip.1] u(n(D,c(D)),U)=U. 4447,4446 [para_into,3417.1.1,5.1.1] u(x,n(c(x),x))=x. 4472 [para_from,3417.1.1,66.1.1.1.1] u(c(x),n(u(c(c(x)),c(x)),x))=u(c(c(x)),c(x)). 4610 [para_into,303.1.1,259.1.1,demod,13] c(n(x,y))=n(u(c($c3),c(c($c2))),u(c(y),c(x))). 4646 [copy,4610,flip.1] n(u(c($c3),c(c($c2))),u(c(x),c(y)))=c(n(y,x)). 4682,4681 [para_from,4282.1.1,66.1.1.1.1,demod,22,3310,2925,3310,flip.1] u(c($c3),c(c($c2)))=u(Z,c(Z)). 4688,4687 [back_demod,4646,demod,4682,flip.1] c(n(x,y))=n(u(Z,c(Z)),u(c(y),c(x))). 4708,4707 [back_demod,3905,demod,4682] c(c(x))=n(u(n(u(Z,c(Z)),$c2),c($c3)),x). 4718,4717 [back_demod,3345,demod,4708,4708,flip.1] u(n(u(n(u(Z,c(Z)),$c2),c($c3)),x),c(x))=u(c($c3),n(u(n(u(Z,c(Z)),$c2),c($c3)),$c2)). 4724 [back_demod,3335,demod,4708,4708] u(c(x),n(u(n(u(Z,c(Z)),$c2),c($c3)),x))=u(c($c3),n(u(n(u(Z,c(Z)),$c2),c($c3)),$c2)). 4838 [back_demod,2199,demod,4708] n(U,u(c($c3),n(u(n(u(Z,c(Z)),$c2),c($c3)),$c2)))=c(Z). 4845,4844 [back_demod,259,demod,4708,4708] n(u(c($c3),n(u(n(u(Z,c(Z)),$c2),c($c3)),$c2)),x)=n(u(n(u(Z,c(Z)),$c2),c($c3)),x). 4910 [back_demod,3902,demod,4688,4708,4688,57,51,47,47,4688,220,51,51,22,4845,47,4708] n(u(Z,c(Z)),u(n(u(n(u(Z,c(Z)),$c2),c($c3)),u(Z,c(Z))),n(U,Z)))=u(n(u(n(u(Z,c(Z)),$c2),c($c3)),$c2),c($c3)). 4913 [back_demod,3794,demod,4708,4688,22] n(u(n(u(n(u(Z,c(Z)),$c2),c($c3)),$c2),c($c3)),u(Z,c(x)))=n(u(Z,c(Z)),u(Z,c(x))). 4990 [back_demod,3367,demod,4688,22,22,2752] n(u(Z,Z),Z)=u(Z,Z). 5037,5036 [back_demod,4681,demod,4708] u(c($c3),n(u(n(u(Z,c(Z)),$c2),c($c3)),$c2))=u(Z,c(Z)). 5063,5062 [back_demod,4472,demod,4708,4718,5037,4708,4718,5037] u(c(x),n(u(Z,c(Z)),x))=u(Z,c(Z)). 5108 [back_demod,3995,demod,4708] n(U,u(Z,n(u(n(u(Z,c(Z)),$c2),c($c3)),Z)))=Z. 5112,5111 [back_demod,3930,demod,4708,4708,4718,5037] u(n(u(n(u(Z,c(Z)),$c2),c($c3)),$c2),c($c3))=u(Z,c(Z)). 5139,5138 [back_demod,3856,demod,4708,4708,5112] n(u(n(u(Z,c(Z)),$c2),c($c3)),x)=n(u(c($c3),n(u(Z,c(Z)),$c2)),x). 5190 [back_demod,3805,demod,4708,5139] n(x,n(u(n(u(c($c3),n(u(Z,c(Z)),$c2)),$c2),c($c3)),x))=x. 5192 [back_demod,3803,demod,4708,5139] n(n(u(n(u(c($c3),n(u(Z,c(Z)),$c2)),$c2),c($c3)),x),x)=x. 5479,5478 [back_demod,284,demod,4708,5139,4708,5139] n(u(n(u(c($c3),n(u(Z,c(Z)),$c2)),$c2),c($c3)),x)=n(u(c($c3),n(u(Z,c(Z)),$c2)),x). 5485 [copy,4724,flip.1,demod,5139,5139] u(c($c3),n(u(c($c3),n(u(Z,c(Z)),$c2)),$c2))=u(c(x),n(u(c($c3),n(u(Z,c(Z)),$c2)),x)). 5633 [back_demod,4838,demod,5139] n(U,u(c($c3),n(u(c($c3),n(u(Z,c(Z)),$c2)),$c2)))=c(Z). 5848,5847 [back_demod,4913,demod,5139,5479] n(u(c($c3),n(u(Z,c(Z)),$c2)),u(Z,c(x)))=n(u(Z,c(Z)),u(Z,c(x))). 5850,5849 [back_demod,4910,demod,5139,5848,5139,flip.1] u(n(u(c($c3),n(u(Z,c(Z)),$c2)),$c2),c($c3))=n(u(Z,c(Z)),u(n(u(Z,c(Z)),u(Z,c(Z))),n(U,Z))). 5884,5883 [back_demod,5111,demod,5139,5850] n(u(Z,c(Z)),u(n(u(Z,c(Z)),u(Z,c(Z))),n(U,Z)))=u(Z,c(Z)). 5885 [back_demod,5108,demod,5139] n(U,u(Z,n(u(c($c3),n(u(Z,c(Z)),$c2)),Z)))=Z. 5939 [back_demod,4707,demod,5139] c(c(x))=n(u(c($c3),n(u(Z,c(Z)),$c2)),x). 6332 [back_demod,5192,demod,5850,5884] n(n(u(Z,c(Z)),x),x)=x. 6334 [back_demod,5190,demod,5850,5884] n(x,n(u(Z,c(Z)),x))=x. 6397,6396 [back_demod,5478,demod,5850,5884,flip.1] n(u(c($c3),n(u(Z,c(Z)),$c2)),x)=n(u(Z,c(Z)),x). 6410,6409 [back_demod,5485,demod,6397,6397,5063] u(c($c3),n(u(Z,c(Z)),$c2))=u(Z,c(Z)). 6430 [back_demod,5633,demod,6410,6410] n(U,u(Z,c(Z)))=c(Z). 6636 [back_demod,5939,demod,6410] c(c(x))=n(u(Z,c(Z)),x). 6680 [back_demod,5885,demod,6410] n(U,u(Z,n(u(Z,c(Z)),Z)))=Z. 6937 [hyper,4024,2] i(Z,u(x,U)). 6939,6938 [para_into,4024.1.1.2,3433.1.1,demod,3434] u(Z,c(Z))=c(Z). 6953,6952 [back_demod,6680,demod,6939,4447] n(U,Z)=Z. 6956 [back_demod,6636,demod,6939] c(c(x))=n(c(Z),x). 6961,6960 [back_demod,6430,demod,6939,3382,flip.1] c(Z)=U. 6975,6974 [back_demod,6334,demod,6961,3973] n(x,n(U,x))=x. 6977,6976 [back_demod,6332,demod,6961,3973] n(n(U,x),x)=x. 6982 [back_demod,5062,demod,6961,3973,6961,3973] u(c(x),n(U,x))=U. 6991,6990 [back_demod,6956,demod,6961] c(c(x))=n(U,x). 7022,7021 [para_from,6960.1.1,4446.1.1.2.1,demod,6953] u(Z,Z)=Z. 7029,7028 [back_demod,4990,demod,7022,7022] n(Z,Z)=Z. 7039 [hyper,6937,3,demod,22,7029] i(Z,x). 7042,7041 [hyper,7039,1] u(Z,x)=x. 7090,7089 [back_demod,879,demod,7042,6975,7042] u(x,Z)=x. 7091 [back_demod,379,demod,7042,7042] n(x,c(x))=Z. 7133 [para_into,7091.1.1,58.1.1] n(c(x),x)=Z. 7166,7165 [para_from,7133.1.1,72.1.1.2,demod,6991,6977,7090,6991,flip.1] n(U,x)=x. 7168,7167 [back_demod,6990,demod,7166] c(c(x))=x. 7170,7169 [back_demod,6982,demod,7166] u(c(x),x)=U. 7196,7195 [back_demod,3057,demod,7170,7170] u(x,U)=U. 7216,7215 [back_demod,2150,demod,7196,7196,flip.1] u(I,u(D,x))=U. 7218,7217 [back_demod,1828,demod,7216,22,7196,7196,7042] n(x,U)=x. 7261 [para_from,7169.1.1,304.1.1.2,demod,7168,7218,7168] u(x,x)=x. 7269 [para_from,7169.1.1,33.1.1.2,demod,7196,flip.1] u(c(x),u(y,x))=U. 7277 [hyper,7261,2] i(x,x). 7278 [hyper,7277,3] i(n(u(x,y),c(y)),x). 7328 [para_into,7278.1.1.1,5.1.1] i(n(u(x,y),c(x)),y). 7432 [para_into,7328.1.1.1,7269.1.1,demod,7168,7166] i(x,u(y,x)). 7443 [para_into,7432.1.2,82.1.1] i(u(x,$c3),u(x,$c2)). 7444 [binary,7443.1,4.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 487 clauses generated 19420 clauses kept 4333 clauses forward subsumed 11904 clauses back subsumed 147 Kbytes malloced 5141 ----------- times (seconds) ----------- user CPU time 1.62 (0 hr, 0 min, 1 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:05 2003