----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sun Nov 30 01:28: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,30). assign(max_distinct_vars,3). assign(max_literals,1). assign(max_mem,30000). assign(max_weight,20). 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("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("ix_b.txt"). ------- start included file ix_b.txt------- formula_list(usable). all x (k(I,x)=x). all x i(x,k(x,U)). all x i(x,k(U,x)). all x i(d(Z,x),x). all x i(d(x,Z),x). all x (k(U,U)=U). all x (d(Z,Z)=Z). end_of_list. -------> usable clausifies to: list(usable). 0 [] k(I,x)=x. 0 [] i(x,k(x,U)). 0 [] i(x,k(U,x)). 0 [] i(d(Z,x),x). 0 [] i(d(x,Z),x). 0 [] k(U,U)=U. 0 [] d(Z,Z)=Z. end_of_list. ------- end included file ix_b.txt------- include("cycleLawC.txt"). ------- start included file cycleLawC.txt------- formula_list(usable). all x y z (n(y,k(n(x,k(y,r(z))),z))=n(k(x,z),y)). end_of_list. -------> usable clausifies to: list(usable). 0 [] n(y,k(n(x,k(y,r(z))),z))=n(k(x,z),y). end_of_list. ------- end included file cycleLawC.txt------- include("xvii_a.txt"). ------- start included file xvii_a.txt------- formula_list(usable). -(all x i(x,k(k(x,r(x)),x))). end_of_list. -------> usable clausifies to: list(usable). 0 [] -i($c1,k(k($c1,r($c1)),$c1)). end_of_list. ------- end included file xvii_a.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=8): 3 [] -i($c1,k(k($c1,r($c1)),$c1)). ------------> process sos: ** KEPT (pick-wt=7): 4 [] u(x,y)=u(y,x). ** KEPT (pick-wt=11): 6 [copy,5,flip.1] u(u(x,y),z)=u(x,u(y,z)). ---> New Demodulator: 7 [new_demod,6] u(u(x,y),z)=u(x,u(y,z)). ** KEPT (pick-wt=14): 8 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ---> New Demodulator: 9 [new_demod,8] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ** KEPT (pick-wt=11): 11 [copy,10,flip.1] k(k(x,y),z)=k(x,k(y,z)). ---> New Demodulator: 12 [new_demod,11] k(k(x,y),z)=k(x,k(y,z)). ** KEPT (pick-wt=5): 13 [] r(r(x))=x. ---> New Demodulator: 14 [new_demod,13] r(r(x))=x. ** KEPT (pick-wt=10): 15 [] r(u(x,y))=u(r(x),r(y)). ---> New Demodulator: 16 [new_demod,15] r(u(x,y))=u(r(x),r(y)). ** KEPT (pick-wt=10): 17 [] r(k(x,y))=k(r(y),r(x)). ---> New Demodulator: 18 [new_demod,17] r(k(x,y))=k(r(y),r(x)). ** KEPT (pick-wt=10): 20 [copy,19,flip.1] c(u(c(x),c(y)))=n(x,y). ---> New Demodulator: 21 [new_demod,20] c(u(c(x),c(y)))=n(x,y). ** KEPT (pick-wt=4): 23 [copy,22,flip.1] c(I)=D. ---> New Demodulator: 24 [new_demod,23] c(I)=D. ** KEPT (pick-wt=5): 26 [copy,25,flip.1] u(I,D)=U. ---> New Demodulator: 27 [new_demod,26] u(I,D)=U. ** KEPT (pick-wt=4): 29 [copy,28,flip.1] c(U)=Z. ---> New Demodulator: 30 [new_demod,29] c(U)=Z. ** KEPT (pick-wt=5): 31 [] k(I,x)=x. ---> New Demodulator: 32 [new_demod,31] k(I,x)=x. ** KEPT (pick-wt=5): 33 [] i(x,k(x,U)). ** KEPT (pick-wt=5): 34 [] i(x,k(U,x)). ** KEPT (pick-wt=5): 35 [] i(d(Z,x),x). ** KEPT (pick-wt=5): 36 [] i(d(x,Z),x). ** KEPT (pick-wt=5): 37 [] k(U,U)=U. ---> New Demodulator: 38 [new_demod,37] k(U,U)=U. ** KEPT (pick-wt=5): 39 [] d(Z,Z)=Z. ---> New Demodulator: 40 [new_demod,39] d(Z,Z)=Z. ** KEPT (pick-wt=16): 41 [] n(x,k(n(y,k(x,r(z))),z))=n(k(y,z),x). Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] u(x,y)=u(y,x). >>>> Starting back demodulation with 7. >>>> Starting back demodulation with 9. >>>> Starting back demodulation with 12. >> back demodulating 3 with 12. >>>> Starting back demodulation with 14. >>>> Starting back demodulation with 16. >>>> Starting back demodulation with 18. >>>> Starting back demodulation with 21. >> back demodulating 8 with 21. >>>> Starting back demodulation with 24. >>>> Starting back demodulation with 27. >>>> Starting back demodulation with 30. >>>> Starting back demodulation with 32. >>>> Starting back demodulation with 38. >>>> Starting back demodulation with 40. ** KEPT (pick-wt=16): 45 [copy,41,flip.1] n(k(x,y),z)=n(z,k(n(x,k(z,r(y))),y)). >>>> Starting back demodulation with 44. Following clause subsumed by 41 during input processing: 0 [copy,45,flip.1] n(x,k(n(y,k(x,r(z))),z))=n(k(y,z),x). ======= end of input processing ======= =========== start of search =========== Resetting weight limit to 10. sos_size=8710 Resetting weight limit to 9. sos_size=4329 ----> UNIT CONFLICT at 25.99 sec ----> 21099 [binary,21098.1,42.1] $F. Length of proof is 229. Level of proof is 36. ---------------- PROOF ---------------- 1 [] -i(x,y)|u(x,y)=y. 2 [] i(x,y)|u(x,y)!=y. 3 [] -i($c1,k(k($c1,r($c1)),$c1)). 4 [] u(x,y)=u(y,x). 5 [] u(x,u(y,z))=u(u(x,y),z). 7,6 [copy,5,flip.1] u(u(x,y),z)=u(x,u(y,z)). 8 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 10 [] k(x,k(y,z))=k(k(x,y),z). 12,11 [copy,10,flip.1] k(k(x,y),z)=k(x,k(y,z)). 14,13 [] r(r(x))=x. 17 [] r(k(x,y))=k(r(y),r(x)). 19 [] n(x,y)=c(u(c(x),c(y))). 21,20 [copy,19,flip.1] c(u(c(x),c(y)))=n(x,y). 22 [] D=c(I). 24,23 [copy,22,flip.1] c(I)=D. 25 [] U=u(I,D). 27,26 [copy,25,flip.1] u(I,D)=U. 28 [] Z=c(U). 30,29 [copy,28,flip.1] c(U)=Z. 32,31 [] k(I,x)=x. 33 [] i(x,k(x,U)). 34 [] i(x,k(U,x)). 35 [] i(d(Z,x),x). 36 [] i(d(x,Z),x). 37 [] k(U,U)=U. 40,39 [] d(Z,Z)=Z. 41 [] n(x,k(n(y,k(x,r(z))),z))=n(k(y,z),x). 42 [back_demod,3,demod,12] -i($c1,k($c1,k(r($c1),$c1))). 44,43 [back_demod,8,demod,21] u(c(u(c(x),y)),n(x,y))=x. 49 [para_into,6.1.1.1,4.1.1,demod,7] u(x,u(y,z))=u(y,u(x,z)). 50 [para_into,6.1.1,4.1.1] u(x,u(y,z))=u(y,u(z,x)). 51 [copy,50,flip.1] u(x,u(y,z))=u(z,u(x,y)). 55,54 [para_into,26.1.1,4.1.1] u(D,I)=U. 57,56 [para_from,26.1.1,6.1.1.1] u(U,x)=u(I,u(D,x)). 58 [hyper,33,1] u(x,k(x,U))=k(x,U). 60 [para_into,33.1.2,31.1.1] i(I,U). 63,62 [hyper,60,1] u(I,U)=U. 64 [hyper,34,1] u(x,k(U,x))=k(U,x). 66 [hyper,35,1] u(d(Z,x),x)=x. 70 [hyper,36,1] u(d(x,Z),x)=x. 72 [para_from,37.1.1,34.1.2] i(U,U). 75 [hyper,72,1,demod,57] u(I,u(D,U))=U. 77 [para_from,39.1.1,36.1.1] i(Z,Z). 80 [para_into,17.1.1.1,31.1.1,flip.1] k(r(x),r(I))=r(x). 83,82 [hyper,77,1] u(Z,Z)=Z. 86 [para_from,62.1.1,6.1.1.1,demod,57,57,flip.1] u(I,u(I,u(D,x)))=u(I,u(D,x)). 90 [para_from,82.1.1,6.1.1.1,flip.1] u(Z,u(Z,x))=u(Z,x). 92 [para_into,20.1.1.1.1,29.1.1] c(u(Z,c(x)))=n(U,x). 95,94 [para_into,20.1.1.1.1,23.1.1] c(u(D,c(x)))=n(I,x). 97,96 [para_into,20.1.1.1.1,20.1.1] c(u(n(x,y),c(z)))=n(u(c(x),c(y)),z). 98 [para_into,20.1.1.1.2,29.1.1] c(u(c(x),Z))=n(x,U). 100 [para_into,20.1.1.1.2,23.1.1] c(u(c(x),D))=n(x,I). 103,102 [para_into,20.1.1.1.2,20.1.1] c(u(c(x),n(y,z)))=n(x,u(c(y),c(z))). 104 [para_into,20.1.1.1,4.1.1,demod,21] n(x,y)=n(y,x). 105 [para_into,66.1.1,4.1.1] u(x,d(Z,x))=x. 111 [para_into,70.1.1,4.1.1] u(x,d(x,Z))=x. 115 [para_from,70.1.1,6.1.1.1,flip.1] u(d(x,Z),u(x,y))=u(x,y). 119 [para_into,75.1.1,4.1.1,demod,7,57,55,63] u(D,U)=U. 124 [para_from,119.1.1,6.1.1.1,demod,57,57,flip.1] u(D,u(I,u(D,x)))=u(I,u(D,x)). 126 [para_into,41.1.1.2.1.2.2,13.1.1] n(x,k(n(y,k(x,z)),r(z)))=n(k(y,r(z)),x). 134 [para_into,105.1.1,6.1.1] u(x,u(y,d(Z,u(x,y))))=u(x,y). 156 [para_into,80.1.1.1,13.1.1,demod,14] k(x,r(I))=x. 159,158 [para_into,156.1.1,31.1.1] r(I)=I. 163,162 [back_demod,156,demod,159] k(x,I)=x. 176 [para_into,43.1.1.1.1.1,29.1.1] u(c(u(Z,x)),n(U,x))=U. 179,178 [para_into,43.1.1.1.1.1,23.1.1] u(c(u(D,x)),n(I,x))=I. 180 [para_into,43.1.1.1.1.1,20.1.1] u(c(u(n(x,y),z)),n(u(c(x),c(y)),z))=u(c(x),c(y)). 186 [para_into,43.1.1.1.1,43.1.1] u(c(x),n(u(c(x),y),n(x,y)))=u(c(x),y). 188 [para_into,43.1.1.1.1,4.1.1] u(c(u(x,c(y))),n(y,x))=y. 190 [para_into,43.1.1.1,20.1.1] u(n(x,y),n(x,c(y)))=x. 192 [para_into,43.1.1.2,104.1.1] u(c(u(c(x),y)),n(y,x))=x. 196 [para_into,43.1.1,4.1.1] u(n(x,y),c(u(c(x),y)))=x. 200 [para_from,43.1.1,6.1.1.1,flip.1] u(c(u(c(x),y)),u(n(x,y),z))=u(x,z). 203,202 [para_from,158.1.1,41.1.1.2.1.2.2,demod,163,163,163] n(x,n(y,x))=n(y,x). 212 [para_into,56.1.1,111.1.1,flip.1] u(I,u(D,d(U,Z)))=U. 216 [para_into,56.1.1,4.1.1] u(x,U)=u(I,u(D,x)). 217 [copy,216,flip.1] u(I,u(D,x))=u(x,U). 220 [para_into,58.1.1,6.1.1] u(x,u(y,k(u(x,y),U)))=k(u(x,y),U). 232 [para_into,49.1.1.2,119.1.1,flip.1] u(D,u(x,U))=u(x,U). 253 [para_into,49.1.1.2,54.1.1] u(x,U)=u(D,u(x,I)). 254 [para_into,49.1.1.2,43.1.1,flip.1] u(c(u(c(x),y)),u(z,n(x,y)))=u(z,x). 256 [para_into,49.1.1.2,26.1.1] u(x,U)=u(I,u(x,D)). 257 [para_into,49.1.1,70.1.1,flip.1] u(x,u(d(u(x,y),Z),y))=u(x,y). 264 [copy,256,flip.1] u(I,u(x,D))=u(x,U). 270 [para_into,64.1.1,6.1.1] u(x,u(y,k(U,u(x,y))))=k(U,u(x,y)). 272 [para_into,64.1.1,4.1.1] u(k(U,x),x)=k(U,x). 292 [para_from,50.1.1,43.1.1.1.1] u(c(u(x,u(y,c(z)))),n(z,u(x,y)))=z. 294 [hyper,90,2] i(Z,u(Z,x)). 300 [para_into,294.1.2,49.1.1] i(Z,u(x,u(Z,y))). 310 [para_into,51.1.1.2,43.1.1,flip.1] u(n(x,y),u(z,c(u(c(x),y))))=u(z,x). 335 [hyper,86,2] i(I,u(I,u(D,x))). 341 [para_into,86.1.1.2.2,50.1.1] u(I,u(I,u(x,u(y,D))))=u(I,u(D,u(x,y))). 343 [para_into,86.1.1.2.2,49.1.1] u(I,u(I,u(x,u(D,y))))=u(I,u(D,u(x,y))). 365 [para_into,335.1.2.2,51.1.1] i(I,u(I,u(x,u(D,y)))). 366 [para_into,335.1.2.2,50.1.1] i(I,u(I,u(x,u(y,D)))). 375,374 [para_into,92.1.1.1.2,29.1.1,demod,83] c(Z)=n(U,U). 376 [para_into,92.1.1.1.2,23.1.1] c(u(Z,D))=n(U,I). 378 [para_into,92.1.1.1.2,20.1.1] c(u(Z,n(x,y)))=n(U,u(c(x),c(y))). 380 [para_from,92.1.1,43.1.1.1.1.1] u(c(u(n(U,x),y)),n(u(Z,c(x)),y))=u(Z,c(x)). 392 [para_into,94.1.1.1.2,29.1.1] c(u(D,Z))=n(I,U). 395,394 [para_into,94.1.1.1.2,23.1.1] c(u(D,D))=n(I,I). 398 [para_from,94.1.1,43.1.1.1.1.1] u(c(u(n(I,x),y)),n(u(D,c(x)),y))=u(D,c(x)). 408 [para_into,96.1.1.1.1,104.1.1,demod,97] n(u(c(x),c(y)),z)=n(u(c(y),c(x)),z). 415 [para_into,96.1.1.1.2,29.1.1] c(u(n(x,y),Z))=n(u(c(x),c(y)),U). 425 [para_from,394.1.1,43.1.1.1.1.1] u(c(u(n(I,I),x)),n(u(D,D),x))=u(D,D). 429 [para_from,98.1.1,43.1.1.1] u(n(x,U),n(x,Z))=x. 441 [para_into,202.1.1.2,104.1.1] n(x,n(x,y))=n(y,x). 442 [para_into,202.1.1,104.1.1] n(n(x,y),y)=n(x,y). 444 [copy,441,flip.1] n(x,y)=n(y,n(y,x)). 447 [para_from,202.1.1,43.1.1.2,demod,103] u(n(x,u(c(y),c(x))),n(y,x))=x. 449 [para_into,212.1.1.2,4.1.1] u(I,u(d(U,Z),D))=U. 519 [para_from,217.1.1,51.1.1.2,demod,7] u(x,u(y,U))=u(D,u(y,u(x,I))). 681 [para_into,115.1.1.2,43.1.1,demod,44] u(d(c(u(c(x),y)),Z),x)=x. 705,704 [para_into,124.1.1.2,49.1.1,flip.1] u(I,u(D,x))=u(D,u(D,u(I,x))). 749 [back_demod,343,demod,705] u(I,u(I,u(x,u(D,y))))=u(D,u(D,u(I,u(x,y)))). 751 [back_demod,341,demod,705] u(I,u(I,u(x,u(y,D))))=u(D,u(D,u(I,u(x,y)))). 766 [back_demod,56,demod,705] u(U,x)=u(D,u(D,u(I,x))). 794 [para_into,126.1.1.2.1,126.1.1,demod,14,14,203] n(n(x,k(y,z)),k(n(k(x,r(z)),y),z))=n(x,k(y,z)). 946 [para_from,134.1.1,49.1.1.2,flip.1] u(x,u(y,u(z,d(Z,u(x,z)))))=u(y,u(x,z)). 959 [hyper,232,2] i(D,u(x,U)). 1019 [para_from,253.1.1,959.1.2] i(D,u(D,u(x,I))). 1081 [para_into,1019.1.2.2,4.1.1] i(D,u(D,u(I,x))). 1094,1093 [hyper,1081,1] u(D,u(D,u(I,x)))=u(D,u(I,x)). 1109,1108 [back_demod,766,demod,1094] u(U,x)=u(D,u(I,x)). 1119,1118 [back_demod,751,demod,1094] u(I,u(I,u(x,u(y,D))))=u(D,u(I,u(x,y))). 1121,1120 [back_demod,749,demod,1094] u(I,u(I,u(x,u(D,y))))=u(D,u(I,u(x,y))). 1189,1188 [para_into,256.1.1,119.1.1,flip.1] u(I,u(D,D))=U. 1303 [para_from,272.1.1,300.1.2] i(Z,k(U,u(Z,x))). 1330 [para_into,176.1.1.1.1,253.1.1] u(c(u(D,u(Z,I))),n(U,U))=U. 1356 [para_into,176.1.1,4.1.1] u(n(U,x),c(u(Z,x)))=U. 1359,1358 [para_from,176.1.1,102.1.1.1,demod,30,30,flip.1] n(u(Z,x),u(Z,c(x)))=Z. 1404,1403 [para_into,178.1.1.1.1,256.1.1,demod,1189,30] u(Z,n(I,U))=I. 1423 [para_into,178.1.1.1.1,54.1.1,demod,30] u(Z,n(I,I))=I. 1467 [para_from,1403.1.1,1303.1.2.2,demod,163] i(Z,U). 1469 [para_from,1403.1.1,176.1.1.1.1,demod,24,203] u(D,n(I,U))=U. 1472,1471 [para_from,1403.1.1,90.1.1.2,demod,1404] u(Z,I)=I. 1487,1486 [back_demod,1330,demod,1472,55,30] u(Z,n(U,U))=U. 1489,1488 [hyper,1467,1] u(Z,U)=U. 1513,1512 [para_into,1471.1.1,4.1.1] u(I,Z)=I. 1514 [para_from,1471.1.1,176.1.1.1.1,demod,24] u(D,n(U,I))=U. 1528,1527 [para_from,1488.1.1,49.1.1.2,flip.1] u(Z,u(x,U))=u(x,U). 1538,1537 [para_from,1512.1.1,6.1.1.1,flip.1] u(I,u(Z,x))=u(I,x). 1693,1692 [para_into,1423.1.1,4.1.1] u(n(I,I),Z)=I. 1708,1707 [para_from,1423.1.1,6.1.1.1,flip.1] u(Z,u(n(I,I),x))=u(I,x). 1746 [para_into,188.1.1.1,92.1.1] u(n(U,x),n(x,Z))=x. 1790 [para_into,1469.1.1,4.1.1] u(n(I,U),D)=U. 1848,1847 [para_into,190.1.1,4.1.1] u(n(x,c(y)),n(x,y))=x. 1849 [para_from,190.1.1,51.1.1.2,flip.1] u(n(x,c(y)),u(z,n(x,y)))=u(z,x). 1862 [para_into,1514.1.1,4.1.1] u(n(U,I),D)=U. 1912 [para_into,192.1.1.1.1,256.1.1] u(c(u(I,u(c(x),D))),n(U,x))=x. 2028 [para_from,1790.1.1,264.1.1.2,demod,63,flip.1] u(n(I,U),U)=U. 2073 [para_into,196.1.1.2.1,256.1.1] u(n(x,U),c(u(I,u(c(x),D))))=x. 2222 [para_from,2028.1.1,180.1.1.1.1,demod,30,24,30,24,30] u(Z,n(u(D,Z),U))=u(D,Z). 2232,2231 [para_into,200.1.1.1.1.1,394.1.1,demod,7] u(c(u(n(I,I),x)),u(n(u(D,D),x),y))=u(D,u(D,y)). 2235 [para_into,200.1.1.1.1.1,376.1.1,demod,7] u(c(u(n(U,I),x)),u(n(u(Z,D),x),y))=u(Z,u(D,y)). 2239 [para_into,200.1.1.1.1,256.1.1] u(c(u(I,u(c(x),D))),u(n(x,U),y))=u(x,y). 2430 [para_into,220.1.1.2.2.1,1692.1.1,demod,32,1489,1693,32] u(n(I,I),U)=U. 2521 [para_from,2430.1.1,180.1.1.1.1,demod,30,24,24,24,24] u(Z,n(u(D,D),U))=u(D,D). 3064 [para_into,257.1.1.2.1.1,264.1.1] u(I,u(d(u(x,U),Z),u(x,D)))=u(I,u(x,D)). 3416,3415 [hyper,365,1,demod,1121,flip.1] u(I,u(x,u(D,y)))=u(D,u(I,u(x,y))). 3424,3423 [hyper,366,1,demod,1119,flip.1] u(I,u(x,u(y,D)))=u(D,u(I,u(x,y))). 3429 [back_demod,3064,demod,3424] u(D,u(I,u(d(u(x,U),Z),x)))=u(I,u(x,D)). 3546 [para_into,441.1.1.2,441.1.1,demod,203,flip.1] n(n(x,y),x)=n(y,x). 3631 [para_into,444.1.1,104.1.1,flip.1] n(x,n(x,y))=n(x,y). 3636,3635 [para_into,449.1.1.2,4.1.1] u(I,u(D,d(U,Z)))=U. 5525 [para_into,378.1.1.1,1423.1.1,demod,24,24,24,flip.1] n(U,u(D,D))=D. 5527 [para_into,378.1.1.1,1403.1.1,demod,24,24,30,flip.1] n(U,u(D,Z))=D. 5574,5573 [para_into,5525.1.1,104.1.1] n(u(D,D),U)=D. 5576,5575 [back_demod,2521,demod,5574] u(Z,D)=u(D,D). 5597 [back_demod,2235,demod,5576] u(c(u(n(U,I),x)),u(n(u(D,D),x),y))=u(Z,u(D,y)). 5618,5617 [back_demod,376,demod,5576,395,flip.1] n(U,I)=n(I,I). 5622,5621 [back_demod,5597,demod,5618,2232,flip.1] u(Z,u(D,x))=u(D,u(D,x)). 5642,5641 [back_demod,1862,demod,5618] u(n(I,I),D)=U. 5664,5663 [para_into,5527.1.1,104.1.1] n(u(D,Z),U)=D. 5666,5665 [back_demod,2222,demod,5664,5576,flip.1] u(D,Z)=u(D,D). 5704,5703 [back_demod,392,demod,5666,395,flip.1] n(I,U)=n(I,I). 5709 [para_from,5573.1.1,202.1.1.2,demod,5574] n(U,D)=D. 5711 [para_from,5573.1.1,442.1.1.1,demod,5574] n(D,U)=D. 5721 [para_from,5709.1.1,380.1.1.1.1.1] u(c(u(D,x)),n(u(Z,c(D)),x))=u(Z,c(D)). 5728,5727 [para_from,5709.1.1,96.1.1.1.1,demod,95,30,flip.1] n(u(Z,c(D)),x)=n(I,x). 5730,5729 [back_demod,5721,demod,5728,179,flip.1] u(Z,c(D))=I. 5787 [para_from,5711.1.1,310.1.1.1] u(D,u(x,c(u(c(D),U))))=u(x,D). 5793 [para_from,5711.1.1,196.1.1.1] u(D,c(u(c(D),U)))=D. 5797 [para_from,5711.1.1,200.1.1.2.1] u(c(u(c(D),U)),u(D,x))=u(D,x). 5850,5849 [para_from,5729.1.1,270.1.1.2.2.2,demod,163,1528,5730,163] u(c(D),U)=U. 5861,5860 [back_demod,5797,demod,5850,30,5622] u(D,u(D,x))=u(D,x). 5865,5864 [back_demod,5793,demod,5850,30,5666] u(D,D)=D. 5870 [back_demod,5787,demod,5850,30] u(D,u(x,Z))=u(x,D). 5884 [back_demod,5621,demod,5861] u(Z,u(D,x))=u(D,x). 5891,5890 [back_demod,5575,demod,5865] u(Z,D)=D. 5925,5924 [back_demod,425,demod,5865,5865] u(c(u(n(I,I),x)),n(D,x))=D. 5926 [back_demod,394,demod,5865] c(D)=n(I,I). 6067,6066 [para_from,5926.1.1,100.1.1.1.1,demod,5642,30,flip.1] n(D,I)=Z. 6072 [para_from,6066.1.1,202.1.1.2,demod,6067] n(I,Z)=Z. 6103,6102 [para_from,6072.1.1,190.1.1.1,demod,375] u(Z,n(I,n(U,U)))=I. 6165,6164 [para_into,408.1.1.1.1,29.1.1,demod,30,flip.1] n(u(c(x),Z),y)=n(u(Z,c(x)),y). 6204 [para_from,5703.1.1,202.1.1.2,demod,5704] n(U,n(I,I))=n(I,I). 6206 [para_from,5703.1.1,442.1.1.1,demod,5704] n(n(I,I),U)=n(I,I). 7627 [para_into,519.1.1,50.1.1,demod,1109] u(x,u(D,u(I,y)))=u(D,u(x,u(y,I))). 7646 [copy,7627,flip.1] u(D,u(x,u(y,I)))=u(x,u(D,u(I,y))). 8595 [para_from,1746.1.1,200.1.1.2,demod,30,1109] u(c(u(Z,x)),x)=u(D,u(I,n(x,Z))). 11405 [para_into,681.1.1.1.1.1,519.1.1] u(d(c(u(D,u(x,u(c(y),I)))),Z),y)=y. 12158 [para_from,3546.1.1,429.1.1.1] u(n(x,U),n(n(U,x),Z))=n(U,x). 15558 [para_into,6102.1.1.2,104.1.1] u(Z,n(n(U,U),I))=I. 15560 [para_into,6102.1.1,4.1.1] u(n(I,n(U,U)),Z)=I. 15584 [para_from,6102.1.1,270.1.1.2.2.2,demod,163,1528,6103,163] u(n(I,n(U,U)),U)=U. 15937,15936 [para_from,6204.1.1,96.1.1.1.1,demod,97,24,24,5865,30,flip.1] n(u(Z,c(n(I,I))),x)=n(D,x). 15948 [para_from,6206.1.1,196.1.1.1] u(n(I,I),c(u(c(n(I,I)),U)))=n(I,I). 15950 [para_from,6206.1.1,200.1.1.2.1] u(c(u(c(n(I,I)),U)),u(n(I,I),x))=u(n(I,I),x). 15952 [para_from,6206.1.1,180.1.1.1.1.1,demod,30,6165,15937,5925,30,flip.1] u(c(n(I,I)),Z)=D. 15962 [para_from,15952.1.1,5870.1.1.2,demod,5865,flip.1] u(c(n(I,I)),D)=D. 16124,16123 [para_from,15962.1.1,264.1.1.2,demod,27,flip.1] u(c(n(I,I)),U)=U. 16154,16153 [back_demod,15950,demod,16124,30,1708,flip.1] u(n(I,I),x)=u(I,x). 16156,16155 [back_demod,15948,demod,16124,30,16154,1513,flip.1] n(I,I)=I. 16228,16227 [back_demod,5926,demod,16156] c(D)=I. 16252,16251 [para_from,16227.1.1,20.1.1.1.2] c(u(c(x),I))=n(x,D). 17443 [para_into,946.1.1.2.2.2.2,3635.1.1,demod,7,3416,3636] u(D,u(I,u(x,u(d(U,Z),d(Z,U)))))=u(x,U). 18083,18082 [para_from,15558.1.1,254.1.1.2,demod,16252,1487] u(n(n(U,U),D),I)=U. 18091,18090 [para_from,15560.1.1,415.1.1.1,demod,24,24,flip.1] n(u(D,c(n(U,U))),U)=D. 18103,18102 [para_from,15584.1.1,398.1.1.1.1,demod,30,18091,5891,flip.1] u(D,c(n(U,U)))=D. 18117 [para_from,18102.1.1,94.1.1.1,demod,16228,flip.1] n(I,n(U,U))=I. 18137,18136 [para_from,18117.1.1,447.1.1.2,demod,24,18103,18083,flip.1] n(U,U)=U. 18149,18148 [back_demod,374,demod,18137] c(Z)=U. 18150 [para_from,18148.1.1,20.1.1.1.2] c(u(c(x),U))=n(x,Z). 18327,18326 [para_from,1356.1.1,96.1.1.1,demod,30,30,flip.1] n(u(Z,c(x)),u(Z,x))=Z. 18330 [para_from,1358.1.1,3631.1.1.2,demod,1359] n(u(Z,x),Z)=Z. 18332 [para_from,1358.1.1,3546.1.1.1,demod,18327] n(Z,u(Z,x))=Z. 18339,18338 [para_into,18330.1.1.1,5884.1.1] n(u(D,x),Z)=Z. 18431,18430 [para_from,18332.1.1,186.1.1.2.2,demod,18149,18149,1109,1538,18339,1109,1513,55,18149,1109,1538,flip.1] u(D,u(I,x))=U. 18433,18432 [back_demod,17443,demod,18431,flip.1] u(x,U)=U. 18444 [back_demod,8595,demod,18431] u(c(u(Z,x)),x)=U. 18447,18446 [back_demod,7646,demod,18431,18433] u(D,u(x,u(y,I)))=U. 18461,18460 [back_demod,3429,demod,18433,18431,flip.1] u(I,u(x,D))=U. 18477,18476 [back_demod,18150,demod,18433,30,flip.1] n(x,Z)=Z. 18507,18506 [back_demod,11405,demod,18447,30,40] u(Z,x)=x. 18520,18519 [back_demod,2239,demod,18461,30,18507] u(n(x,U),y)=u(x,y). 18522,18521 [back_demod,2073,demod,18461,30,18520] u(x,Z)=x. 18524,18523 [back_demod,1912,demod,18461,30,18507] n(U,x)=x. 18528,18527 [back_demod,12158,demod,18524,18477,18522,18524] n(x,U)=x. 18561 [back_demod,18444,demod,18507] u(c(x),x)=U. 18563 [back_demod,18326,demod,18507,18507] n(c(x),x)=Z. 18600,18599 [back_demod,92,demod,18507,18524] c(c(x))=x. 18706 [para_from,18561.1.1,292.1.1.1.1.2,demod,18433,30,18600,18507] n(x,u(y,x))=x. 18726 [para_from,18563.1.1,186.1.1.2.2,demod,18600,18600,18477,18522,18600,flip.1] u(x,x)=x. 18784,18783 [para_into,18706.1.1.2,272.1.1] n(x,k(U,x))=x. 18823 [para_from,18783.1.1,794.1.1.1,demod,18528,12,18784] n(x,k(x,k(r(x),x)))=x. 19230 [para_into,1849.1.1.2,18726.1.1,demod,1848,flip.1] u(n(x,y),x)=x. 19250 [hyper,19230,2] i(n(x,y),x). 19272 [para_into,19250.1.1,202.1.1] i(n(x,y),y). 21098 [para_from,18823.1.1,19272.1.1] i(x,k(x,k(r(x),x))). 21099 [binary,21098.1,42.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 3622 clauses generated 835332 clauses kept 14834 clauses forward subsumed 415502 clauses back subsumed 1829 Kbytes malloced 11208 ----------- times (seconds) ----------- user CPU time 26.19 (0 hr, 0 min, 26 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 26 (0 hr, 0 min, 26 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 01:28:29 2003