----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sun Nov 30 15:45:47 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_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("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_a.txt"). ------- start included file ix_a.txt------- formula_list(usable). all x (k(x,I)=x). end_of_list. -------> usable clausifies to: list(usable). 0 [] k(x,I)=x. end_of_list. ------- end included file ix_a.txt------- include("i.txt"). ------- start included file i.txt------- formula_list(usable). all x y (i(x,y)->i(r(x),r(y))). all x y (r(u(x,y))=u(r(x),r(y))). all x (r(c(x))=c(r(x))). all x y (r(n(x,y))=n(r(x),r(y))). all x (r(r(x))=x). all x y (r(d(x,y))=d(r(y),r(x))). all x y (r(k(x,y))=k(r(y),r(x))). r(I)=I. r(Z)=Z. r(U)=U. end_of_list. -------> usable clausifies to: list(usable). 0 [] -i(x,y)|i(r(x),r(y)). 0 [] r(u(x,y))=u(r(x),r(y)). 0 [] r(c(x))=c(r(x)). 0 [] r(n(x,y))=n(r(x),r(y)). 0 [] r(r(x))=x. 0 [] r(d(x,y))=d(r(y),r(x)). 0 [] r(k(x,y))=k(r(y),r(x)). 0 [] r(I)=I. 0 [] r(Z)=Z. 0 [] r(U)=U. end_of_list. ------- end included file i.txt------- include("15_16booleanLaws.txt"). ------- start included file 15_16booleanLaws.txt------- formula_list(usable). all x (c(c(x))=x). all x y (u(x,y)=y->c(u(y,c(x)))=Z). all x y (c(u(y,c(x)))=Z->u(x,y)=y). end_of_list. -------> usable clausifies to: list(usable). 0 [] c(c(x))=x. 0 [] u(x,y)!=y|c(u(y,c(x)))=Z. 0 [] c(u(y,c(x)))!=Z|u(x,y)=y. end_of_list. ------- end included file 15_16booleanLaws.txt------- include("cycleLawsB.txt"). ------- start included file cycleLawsB.txt------- formula_list(usable). all x y z (n(y,k(x,n(z,c(k(r(x),y)))))=Z). all x y z v (n(k(x,z),y)=n(u(k(n(x,v),z),k(n(x,c(v)),z)),y)). all x y z (n(y,k(n(x,c(k(y,r(z)))),z))=Z). end_of_list. -------> usable clausifies to: list(usable). 0 [] n(y,k(x,n(z,c(k(r(x),y)))))=Z. 0 [] n(k(x,z),y)=n(u(k(n(x,v),z),k(n(x,c(v)),z)),y). 0 [] n(y,k(n(x,c(k(y,r(z)))),z))=Z. end_of_list. ------- end included file cycleLawsB.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("xxi_a_ghost.txt"). ------- start included file xxi_a_ghost.txt------- formula_list(usable). -(all x (n(x,I)=n(r(x),I))). end_of_list. -------> usable clausifies to: list(usable). 0 [] n($c1,I)!=n(r($c1),I). end_of_list. ------- end included file xxi_a_ghost.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)|i(r(x),r(y)). ** KEPT (pick-wt=12): 2 [] u(x,y)!=y|c(u(y,c(x)))=Z. ** KEPT (pick-wt=12): 3 [] c(u(x,c(y)))!=Z|u(y,x)=x. ** KEPT (pick-wt=8): 5 [copy,4,flip.1] n(r($c1),I)!=n($c1,I). ------------> 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=11): 13 [copy,12,flip.1] k(k(x,y),z)=k(x,k(y,z)). ---> New Demodulator: 14 [new_demod,13] k(k(x,y),z)=k(x,k(y,z)). ** KEPT (pick-wt=5): 15 [] r(r(x))=x. ---> New Demodulator: 16 [new_demod,15] r(r(x))=x. ** KEPT (pick-wt=10): 17 [] r(u(x,y))=u(r(x),r(y)). ---> New Demodulator: 18 [new_demod,17] r(u(x,y))=u(r(x),r(y)). ** KEPT (pick-wt=10): 19 [] r(k(x,y))=k(r(y),r(x)). ---> New Demodulator: 20 [new_demod,19] r(k(x,y))=k(r(y),r(x)). ** KEPT (pick-wt=10): 22 [copy,21,flip.1] c(u(c(x),c(y)))=n(x,y). ---> New Demodulator: 23 [new_demod,22] c(u(c(x),c(y)))=n(x,y). ** KEPT (pick-wt=4): 25 [copy,24,flip.1] c(I)=D. ---> New Demodulator: 26 [new_demod,25] c(I)=D. ** KEPT (pick-wt=5): 28 [copy,27,flip.1] u(I,D)=U. ---> New Demodulator: 29 [new_demod,28] u(I,D)=U. ** KEPT (pick-wt=4): 31 [copy,30,flip.1] c(U)=Z. ---> New Demodulator: 32 [new_demod,31] c(U)=Z. ** KEPT (pick-wt=5): 33 [] k(x,I)=x. ---> New Demodulator: 34 [new_demod,33] k(x,I)=x. ** KEPT (pick-wt=11): 36 [copy,35,demod,18] u(r(x),r(y))=u(r(x),r(y)). ** KEPT (pick-wt=7): 37 [] r(c(x))=c(r(x)). ---> New Demodulator: 38 [new_demod,37] r(c(x))=c(r(x)). ** KEPT (pick-wt=10): 39 [] r(n(x,y))=n(r(x),r(y)). ---> New Demodulator: 40 [new_demod,39] r(n(x,y))=n(r(x),r(y)). ** KEPT (pick-wt=3): 42 [copy,41,demod,16] x=x. ** KEPT (pick-wt=10): 43 [] r(d(x,y))=d(r(y),r(x)). ---> New Demodulator: 44 [new_demod,43] r(d(x,y))=d(r(y),r(x)). Following clause subsumed by 42 during input processing: 0 [demod,20] k(r(y),r(x))=k(r(y),r(x)). ** KEPT (pick-wt=4): 45 [] r(I)=I. ---> New Demodulator: 46 [new_demod,45] r(I)=I. ** KEPT (pick-wt=4): 47 [] r(Z)=Z. ---> New Demodulator: 48 [new_demod,47] r(Z)=Z. ** KEPT (pick-wt=4): 49 [] r(U)=U. ---> New Demodulator: 50 [new_demod,49] r(U)=U. ** KEPT (pick-wt=5): 51 [] c(c(x))=x. ---> New Demodulator: 52 [new_demod,51] c(c(x))=x. ** KEPT (pick-wt=13): 53 [] n(x,k(y,n(z,c(k(r(y),x)))))=Z. ---> New Demodulator: 54 [new_demod,53] n(x,k(y,n(z,c(k(r(y),x)))))=Z. ** KEPT (pick-wt=20): 56 [copy,55,flip.1] n(u(k(n(x,y),z),k(n(x,c(y)),z)),u)=n(k(x,z),u). ---> New Demodulator: 57 [new_demod,56] n(u(k(n(x,y),z),k(n(x,c(y)),z)),u)=n(k(x,z),u). ** KEPT (pick-wt=13): 58 [] n(x,k(n(y,c(k(x,r(z)))),z))=Z. ---> New Demodulator: 59 [new_demod,58] n(x,k(n(y,c(k(x,r(z)))),z))=Z. ** KEPT (pick-wt=16): 60 [] n(x,k(n(y,k(x,r(z))),z))=n(k(y,z),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. >>>> Starting back demodulation with 16. >>>> Starting back demodulation with 18. >>>> Starting back demodulation with 20. >>>> Starting back demodulation with 23. >> back demodulating 10 with 23. >>>> Starting back demodulation with 26. >>>> Starting back demodulation with 29. >>>> Starting back demodulation with 32. >>>> Starting back demodulation with 34. Following clause subsumed by 42 during input processing: 0 [copy,36,flip.1] u(r(x),r(y))=u(r(x),r(y)). >>>> Starting back demodulation with 38. >>>> Starting back demodulation with 40. Following clause subsumed by 42 during input processing: 0 [copy,42,flip.1] x=x. 42 back subsumes 36. >>>> Starting back demodulation with 44. >>>> Starting back demodulation with 46. >>>> Starting back demodulation with 48. >>>> Starting back demodulation with 50. >>>> Starting back demodulation with 52. >>>> Starting back demodulation with 54. >>>> Starting back demodulation with 57. >>>> Starting back demodulation with 59. ** KEPT (pick-wt=16): 63 [copy,60,flip.1] n(k(x,y),z)=n(z,k(n(x,k(z,r(y))),y)). >>>> Starting back demodulation with 62. Following clause subsumed by 60 during input processing: 0 [copy,63,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 12. sos_size=4641 ----> UNIT CONFLICT at 26.54 sec ----> 21171 [binary,21169.1,126.1] $F. Length of proof is 211. Level of proof is 31. ---------------- PROOF ---------------- 4 [] n($c1,I)!=n(r($c1),I). 5 [copy,4,flip.1] n(r($c1),I)!=n($c1,I). 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 [] k(x,k(y,z))=k(k(x,y),z). 14,13 [copy,12,flip.1] k(k(x,y),z)=k(x,k(y,z)). 16,15 [] r(r(x))=x. 18,17 [] r(u(x,y))=u(r(x),r(y)). 20,19 [] r(k(x,y))=k(r(y),r(x)). 21 [] n(x,y)=c(u(c(x),c(y))). 23,22 [copy,21,flip.1] c(u(c(x),c(y)))=n(x,y). 24 [] D=c(I). 26,25 [copy,24,flip.1] c(I)=D. 27 [] U=u(I,D). 29,28 [copy,27,flip.1] u(I,D)=U. 30 [] Z=c(U). 32,31 [copy,30,flip.1] c(U)=Z. 34,33 [] k(x,I)=x. 38,37 [] r(c(x))=c(r(x)). 40,39 [] r(n(x,y))=n(r(x),r(y)). 46,45 [] r(I)=I. 50,49 [] r(U)=U. 52,51 [] c(c(x))=x. 53 [] n(x,k(y,n(z,c(k(r(y),x)))))=Z. 55 [] n(k(x,y),z)=n(u(k(n(x,u),y),k(n(x,c(u)),y)),z). 57,56 [copy,55,flip.1] n(u(k(n(x,y),z),k(n(x,c(y)),z)),u)=n(k(x,z),u). 58 [] n(x,k(n(y,c(k(x,r(z)))),z))=Z. 60 [] n(x,k(n(y,k(x,r(z))),z))=n(k(y,z),x). 61 [back_demod,10,demod,23] u(c(u(c(x),y)),n(x,y))=x. 64 [para_into,8.1.1.1,6.1.1,demod,9] u(x,u(y,z))=u(y,u(x,z)). 65 [para_into,8.1.1,6.1.1] u(x,u(y,z))=u(y,u(z,x)). 66 [copy,65,flip.1] u(x,u(y,z))=u(z,u(x,y)). 68,67 [para_into,28.1.1,6.1.1] u(D,I)=U. 70,69 [para_from,28.1.1,8.1.1.1] u(U,x)=u(I,u(D,x)). 74,73 [para_into,51.1.1.1,31.1.1] c(Z)=U. 76,75 [para_into,51.1.1.1,25.1.1] c(D)=I. 87 [para_into,37.1.1.1,25.1.1,demod,46,26] r(D)=D. 89 [para_into,19.1.1.1,33.1.1,demod,46,flip.1] k(I,r(x))=r(x). 104,103 [para_into,89.1.1.2,15.1.1,demod,16] k(I,x)=x. 105 [para_into,69.1.1,6.1.1] u(x,U)=u(I,u(D,x)). 112,111 [para_into,22.1.1.1.1,51.1.1] c(u(x,c(y)))=n(c(x),y). 114,113 [para_into,22.1.1.1.1,22.1.1,demod,112] n(c(n(x,y)),z)=n(u(c(x),c(y)),z). 120,119 [para_into,22.1.1.1.2,51.1.1] c(u(c(x),y))=n(x,c(y)). 121 [para_into,22.1.1.1.2,22.1.1,demod,120] n(x,c(n(y,z)))=n(x,u(c(y),c(z))). 123 [para_into,22.1.1.1,6.1.1,demod,112,52] n(x,y)=n(y,x). 125,124 [back_demod,61,demod,120] u(n(x,c(y)),n(x,y))=x. 126 [para_from,123.1.1,5.1.1] n(I,r($c1))!=n($c1,I). 127 [para_into,105.1.1,8.1.1] u(x,u(y,U))=u(I,u(D,u(x,y))). 164,163 [para_into,111.1.1.1.2,51.1.1] c(u(x,y))=n(c(x),c(y)). 165 [para_into,111.1.1.1,69.1.1,demod,164,26,164,76,52,32,flip.1] n(Z,x)=n(D,n(I,x)). 168,167 [para_into,111.1.1.1,8.1.1,demod,164,164,52,164,flip.1] n(n(c(x),c(y)),z)=n(c(x),n(c(y),z)). 171 [para_into,53.1.1.2.2.2.1.1,87.1.1] n(x,k(D,n(y,c(k(D,x)))))=Z. 177 [para_into,53.1.1.2.2.2.1.1,45.1.1,demod,104,104] n(x,n(y,c(x)))=Z. 179 [para_into,53.1.1.2.2.2.1.1,37.1.1] n(x,k(c(y),n(z,c(k(c(r(y)),x)))))=Z. 185 [para_into,53.1.1.2.2,165.1.1] n(x,k(y,n(D,n(I,c(k(r(y),x))))))=Z. 195 [para_into,177.1.1.2.2,75.1.1] n(D,n(x,I))=Z. 199 [para_into,177.1.1.2.2,51.1.1] n(c(x),n(y,x))=Z. 205 [para_into,177.1.1.2,165.1.1] n(x,n(D,n(I,c(x))))=Z. 207 [para_into,177.1.1.2,123.1.1] n(x,n(c(x),y))=Z. 214,213 [para_into,195.1.1.2,123.1.1] n(D,n(I,x))=Z. 218,217 [back_demod,205,demod,214] n(x,Z)=Z. 219 [back_demod,185,demod,214] n(x,k(y,Z))=Z. 222,221 [back_demod,165,demod,214] n(Z,x)=Z. 224,223 [para_into,56.1.1.1.1.1,221.1.1,demod,222] n(u(k(Z,x),k(Z,x)),y)=n(k(Z,x),y). 231 [para_into,56.1.1.1.2.1.2,75.1.1] n(u(k(n(x,D),y),k(n(x,I),y)),z)=n(k(x,y),z). 250,249 [para_into,219.1.1,123.1.1] n(k(x,Z),y)=Z. 264,263 [para_into,58.1.1.2.1,221.1.1] n(x,k(Z,y))=Z. 276,275 [para_from,249.1.1,56.1.1.1.2.1,demod,250,224,14,flip.1] n(k(x,k(Z,y)),z)=n(k(Z,y),z). 282,281 [para_into,60.1.1.2.1.2.2,45.1.1,demod,34,34,34] n(x,n(y,x))=n(y,x). 284 [para_into,60.1.1.2.1.2.2,15.1.1] n(x,k(n(y,k(x,z)),r(z)))=n(k(y,r(z)),x). 285 [para_into,60.1.1.2.1.2,103.1.1] n(I,k(n(x,r(y)),y))=n(k(x,y),I). 287,286 [para_into,60.1.1.2.1,249.1.1,demod,264,14,276,flip.1] n(k(Z,x),y)=Z. 288 [para_into,60.1.1.2.1,123.1.1] n(x,k(n(k(x,r(y)),z),y))=n(k(z,y),x). 289 [para_into,60.1.1.2.1,60.1.1,demod,16,16,282] n(n(x,k(y,z)),k(n(k(x,r(z)),y),z))=n(x,k(y,z)). 303 [para_into,199.1.1.2,123.1.1] n(c(x),n(x,y))=Z. 305 [para_into,199.1.1.2,60.1.1] n(c(k(n(x,k(y,r(z))),z)),n(k(x,z),y))=Z. 315,314 [para_into,303.1.1,123.1.1] n(n(x,y),c(x))=Z. 338 [para_into,65.1.1.2,6.1.1] u(x,u(y,z))=u(z,u(y,x)). 349 [para_into,281.1.1.2,123.1.1] n(x,n(x,y))=n(y,x). 351,350 [para_into,281.1.1,303.1.1,flip.1] n(x,c(x))=Z. 356 [para_into,281.1.1,207.1.1,flip.1] n(c(x),x)=Z. 384,383 [para_into,349.1.1.2,349.1.1,demod,282,flip.1] n(n(x,y),x)=n(y,x). 387 [para_from,349.1.1,199.1.1.2,demod,114] n(u(c(x),c(y)),n(y,x))=Z. 486 [para_into,124.1.1.1.2,75.1.1] u(n(x,I),n(x,D))=x. 488 [para_into,124.1.1.1.2,73.1.1,demod,218] u(n(x,U),Z)=x. 491,490 [para_into,124.1.1.1.2,51.1.1] u(n(x,y),n(x,c(y)))=x. 494 [para_into,124.1.1.1.2,25.1.1] u(n(x,D),n(x,I))=x. 498 [para_into,124.1.1.1,356.1.1,demod,52,52] u(Z,n(x,x))=x. 501,500 [para_into,124.1.1.1,314.1.1,demod,384] u(Z,n(x,y))=n(y,x). 507,506 [para_into,124.1.1.1,221.1.1,demod,222] u(Z,Z)=Z. 513,512 [para_into,124.1.1.1,113.1.1,demod,114,125,flip.1] c(n(x,y))=u(c(x),c(y)). 514 [para_into,124.1.1.1,56.1.1,demod,57,125,flip.1] u(k(n(x,y),z),k(n(x,c(y)),z))=k(x,z). 526 [para_into,124.1.1.2,350.1.1,demod,52] u(n(x,x),Z)=x. 529,528 [para_into,124.1.1.2,314.1.1,demod,52,384] u(n(x,y),Z)=n(y,x). 535,534 [para_into,124.1.1.2,286.1.1,demod,287,507,flip.1] k(Z,x)=Z. 541,540 [para_into,124.1.1.2,263.1.1,demod,535,74,529] n(U,x)=x. 548 [para_into,124.1.1.2,207.1.1,demod,513,52,529] n(u(x,c(y)),x)=x. 558 [para_into,124.1.1.2,123.1.1] u(n(x,c(y)),n(y,x))=x. 560 [para_into,124.1.1.2,121.1.1,demod,513,164,52,52] u(n(x,n(y,z)),n(x,u(c(y),c(z))))=x. 567,566 [back_demod,498,demod,501] n(x,x)=x. 600,599 [back_demod,526,demod,567] u(x,Z)=x. 602,601 [back_demod,488,demod,600] n(x,U)=x. 638 [para_from,124.1.1,66.1.1.2,flip.1] u(n(x,y),u(z,n(x,c(y))))=u(z,x). 641 [para_from,124.1.1,64.1.1.2,flip.1] u(n(x,c(y)),u(z,n(x,y)))=u(z,x). 643 [para_from,124.1.1,8.1.1.1,flip.1] u(n(x,c(y)),u(n(x,y),z))=u(x,z). 651 [para_from,540.1.1,124.1.1.1,demod,541] u(c(x),x)=U. 662 [para_from,127.1.1,65.1.1.2,demod,9,70] u(x,u(I,u(D,u(y,z))))=u(y,u(z,u(I,u(D,x)))). 664 [para_from,127.1.1,8.1.1.1,demod,9,9,9,9,70] u(I,u(D,u(x,u(y,z))))=u(x,u(y,u(I,u(D,z)))). 668 [copy,662,flip.1] u(x,u(y,u(I,u(D,z))))=u(z,u(I,u(D,u(x,y)))). 670 [copy,664,flip.1] u(x,u(y,u(I,u(D,z))))=u(I,u(D,u(x,u(y,z)))). 672,671 [para_from,566.1.1,124.1.1.2,demod,351] u(Z,x)=x. 698,697 [para_into,651.1.1,127.1.1,demod,164,32,218,672] u(I,u(D,x))=U. 710,709 [back_demod,670,demod,698,698] u(x,u(y,U))=U. 713,712 [back_demod,668,demod,698,710,698,flip.1] u(x,U)=U. 744 [para_from,651.1.1,65.1.1.2,demod,713,flip.1] u(c(x),u(x,y))=U. 750 [para_into,163.1.1.1,124.1.1,demod,513,52,513,flip.1] n(u(c(x),y),u(c(x),c(y)))=c(x). 759 [para_from,163.1.1,124.1.1.1.2] u(n(x,n(c(y),c(z))),n(x,u(y,z)))=x. 763 [para_from,163.1.1,356.1.1.1,demod,168] n(c(x),n(c(y),u(x,y)))=Z. 773 [para_from,163.1.1,207.1.1.2.1,demod,168] n(u(x,y),n(c(x),n(c(y),z)))=Z. 781 [para_into,167.1.1.1.1,51.1.1,demod,52] n(n(x,c(y)),z)=n(x,n(c(y),z)). 786,785 [para_into,167.1.1.1.2,51.1.1,demod,52] n(n(c(x),y),z)=n(c(x),n(y,z)). 795,794 [para_into,548.1.1.1.2,51.1.1] n(u(x,y),x)=x. 808 [para_into,794.1.1,123.1.1] n(x,u(x,y))=x. 830 [para_into,171.1.1.2.2.2.1,33.1.1,demod,76] n(I,k(D,n(x,I)))=Z. 880 [para_into,486.1.1.1,123.1.1] u(n(I,x),n(x,D))=x. 886 [para_into,486.1.1.2,123.1.1] u(n(x,I),n(D,x))=x. 888 [para_from,486.1.1,66.1.1.2,flip.1] u(n(x,D),u(y,n(x,I)))=u(y,x). 901 [para_into,494.1.1.1,123.1.1] u(n(D,x),n(x,I))=x. 907 [para_into,494.1.1.2,123.1.1] u(n(x,D),n(I,x))=x. 918 [para_into,179.1.1.2.2.2.1.1.1,15.1.1] n(x,k(c(r(y)),n(z,c(k(c(y),x)))))=Z. 1000 [para_into,830.1.1.2.2,123.1.1] n(I,k(D,n(I,x)))=Z. 1004 [para_from,830.1.1,124.1.1.2,demod,600] n(I,c(k(D,n(x,I))))=I. 1026 [para_into,880.1.1.1,830.1.1,demod,672] n(k(D,n(x,I)),D)=k(D,n(x,I)). 1044 [para_into,880.1.1.2,123.1.1] u(n(I,x),n(D,x))=x. 1125,1124 [para_from,1000.1.1,907.1.1.2,demod,600] n(k(D,n(I,x)),D)=k(D,n(I,x)). 1224 [para_into,231.1.1.1.1.1,540.1.1,demod,541,104] n(u(k(D,x),x),y)=n(k(U,x),y). 1316 [para_into,490.1.1.1,123.1.1] u(n(x,y),n(y,c(x)))=y. 1332 [para_into,490.1.1.2,123.1.1] u(n(x,y),n(c(y),x))=x. 1430 [para_into,512.1.1.1,566.1.1,flip.1] u(c(x),c(x))=c(x). 1499,1498 [para_into,1430.1.1.1,51.1.1,demod,52,52] u(x,x)=x. 1503,1502 [para_into,1498.1.1,64.1.1,demod,9,1499] u(x,u(x,y))=u(x,y). 1504 [para_from,1498.1.1,66.1.1.2,flip.1] u(x,u(y,x))=u(y,x). 1526 [para_into,1502.1.1.2,490.1.1,demod,491] u(n(x,y),x)=x. 1530,1529 [para_into,1502.1.1.2,65.1.1] u(x,u(y,u(z,x)))=u(x,u(y,z)). 1532,1531 [para_into,1502.1.1.2,64.1.1] u(x,u(y,u(x,z)))=u(x,u(y,z)). 1586,1585 [para_into,1526.1.1.1,281.1.1] u(n(x,y),y)=y. 1593 [para_into,1526.1.1,6.1.1] u(x,n(x,y))=x. 1599,1598 [para_from,1526.1.1,64.1.1.2,flip.1] u(n(x,y),u(z,x))=u(z,x). 1637,1636 [para_into,1585.1.1,6.1.1] u(x,n(y,x))=x. 1642 [para_from,1585.1.1,66.1.1.2,flip.1] u(x,u(y,n(z,x)))=u(y,x). 1650 [para_from,1593.1.1,8.1.1.1,flip.1] u(x,u(n(x,y),z))=u(x,z). 1653 [para_from,1636.1.1,8.1.1.1,flip.1] u(x,u(n(y,x),z))=u(x,z). 1719 [para_into,558.1.1.1,794.1.1] u(c(x),n(x,u(c(x),y)))=u(c(x),y). 1904 [para_from,1004.1.1,512.1.1.1,demod,26,26,52,flip.1] u(D,k(D,n(x,I)))=D. 2088 [para_into,284.1.1.2.1.2,103.1.1,flip.1] n(k(x,r(y)),I)=n(I,k(n(x,y),r(y))). 2173,2172 [para_into,285.1.1.2.1,540.1.1] n(I,k(r(x),x))=n(k(U,x),I). 2265 [para_into,288.1.1,540.1.1,demod,602] k(n(k(U,r(x)),y),x)=k(y,x). 2324 [para_into,289.1.1.1,566.1.1,demod,14,567] n(k(x,y),k(n(k(x,k(y,r(y))),x),y))=k(x,y). 2368,2367 [para_from,1904.1.1,64.1.1.2,flip.1] u(D,u(x,k(D,n(y,I))))=u(x,D). 2906 [para_into,305.1.1.2.1,103.1.1] n(c(k(n(I,k(x,r(y))),y)),n(y,x))=Z. 3485 [para_into,1316.1.1.2,123.1.1] u(n(x,y),n(c(x),y))=y. 4403 [para_from,514.1.1,744.1.1.2] u(c(k(n(x,y),z)),k(x,z))=U. 5023 [para_into,638.1.1.1,383.1.1,demod,315,600] u(n(x,y),z)=u(z,n(y,x)). 5054 [copy,5023,flip.1] u(x,n(y,z))=u(n(z,y),x). 5186,5185 [para_into,641.1.1.2,1636.1.1] u(n(x,c(y)),y)=u(y,x). 5189 [para_into,641.1.1.2,1526.1.1,demod,125,flip.1] u(n(n(x,y),z),x)=x. 5197 [para_into,641.1.1.2,1044.1.1,demod,5186,flip.1] u(n(I,x),D)=u(x,D). 5201 [para_into,641.1.1.2,886.1.1,demod,5186,flip.1] u(n(x,I),D)=u(x,D). 5353 [para_from,5189.1.1,808.1.1.2] n(n(n(x,y),z),x)=n(n(x,y),z). 5438 [para_into,5197.1.1,6.1.1] u(D,n(I,x))=u(x,D). 5517 [para_into,643.1.1.2,901.1.1,demod,5186] u(x,D)=u(D,n(x,I)). 5978 [para_from,5438.1.1,638.1.1.2,demod,68] u(n(I,x),u(c(x),D))=U. 6039,6038 [para_into,5517.1.1,6.1.1,flip.1] u(D,n(x,I))=u(D,x). 6199,6198 [para_from,6038.1.1,8.1.1.1,demod,9,flip.1] u(D,u(n(x,I),y))=u(D,u(x,y)). 6319 [para_into,750.1.1.1.1,51.1.1,demod,52,52] n(u(x,y),u(x,c(y)))=x. 6678 [para_into,759.1.1.1,387.1.1,demod,52,52,672,52,52] n(u(x,y),u(y,x))=u(x,y). 6759 [para_from,3485.1.1,641.1.1.2,demod,5186,flip.1] u(n(x,y),c(x))=u(y,c(x)). 6872 [para_from,763.1.1,1332.1.1.2,demod,786,795,600,flip.1] n(c(x),u(y,x))=n(c(x),y). 7875,7874 [para_into,781.1.1.1.2,51.1.1,demod,52] n(n(x,y),z)=n(x,n(y,z)). 8075 [back_demod,5353,demod,7875,384,7875,7875] n(x,n(y,z))=n(z,n(x,y)). 8366,8365 [para_into,5185.1.1,6.1.1] u(x,n(y,c(x)))=u(x,y). 8828 [para_into,6319.1.1.1,5201.1.1,demod,76,1586] n(u(x,D),I)=n(x,I). 8871 [para_into,6319.1.1.1,1504.1.1,demod,164,8366] n(u(x,y),u(y,c(x)))=y. 8876,8875 [para_into,6319.1.1.1,1316.1.1,demod,513,52,1599] n(x,u(c(x),y))=n(y,x). 8901 [para_into,6319.1.1.2.2,25.1.1] n(u(x,I),u(x,D))=x. 8909 [para_into,6319.1.1.2,6.1.1] n(u(x,y),u(c(y),x))=x. 8919 [back_demod,1719,demod,8876] u(c(x),n(y,x))=u(c(x),y). 8943,8942 [para_into,8828.1.1,123.1.1] n(I,u(x,D))=n(x,I). 9036 [para_into,8901.1.1.1,6.1.1] n(u(I,x),u(x,D))=x. 9041,9040 [para_into,8901.1.1.2,5185.1.1,demod,76,1586,76] n(I,u(D,x))=n(x,I). 9153 [para_into,9036.1.1.2,6.1.1] n(u(I,x),u(D,x))=x. 10510 [para_from,918.1.1,5978.1.1.1,demod,34,52,672] u(c(k(c(r(x)),n(y,x))),D)=U. 10602 [para_into,8871.1.1.2.2,51.1.1] n(u(c(x),y),u(y,x))=y. 11020 [para_into,10602.1.1.2,6.1.1] n(u(c(x),y),u(x,y))=y. 11859 [para_from,1642.1.1,9040.1.1.2,demod,8943,flip.1] n(u(x,n(y,D)),I)=n(x,I). 12168,12167 [para_into,1653.1.1.2,888.1.1,flip.1] u(D,u(x,n(y,I)))=u(D,u(x,y)). 12221,12220 [para_from,1653.1.1,9153.1.1.1,demod,6199,flip.1] u(n(x,I),y)=n(u(I,y),u(D,u(x,y))). 12820 [para_into,1026.1.1.1.2,123.1.1,demod,1125] k(D,n(I,x))=k(D,n(x,I)). 16666,16665 [para_into,1224.1.1,6678.1.1] u(k(D,x),x)=n(k(U,x),u(x,k(D,x))). 16702,16701 [para_into,1224.1.1,601.1.1,demod,16666,602] n(k(U,x),u(x,k(D,x)))=k(U,x). 16714,16713 [back_demod,16665,demod,16702] u(k(D,x),x)=k(U,x). 16728,16727 [para_into,16713.1.1,5054.1.1] u(n(x,y),k(D,n(y,x)))=k(U,n(y,x)). 16741 [para_into,16713.1.1,6.1.1] u(x,k(D,x))=k(U,x). 16818,16817 [para_from,16713.1.1,8.1.1.1] u(k(U,x),y)=u(k(D,x),u(x,y)). 17170,17169 [para_from,16741.1.1,1650.1.1.2] u(x,k(U,n(x,y)))=u(x,k(D,n(x,y))). 17960 [para_into,11859.1.1,123.1.1] n(I,u(x,n(y,D)))=n(x,I). 18002 [para_from,12820.1.1,16741.1.1.2,demod,16728] k(U,n(x,I))=k(U,n(I,x)). 18003 [copy,18002,flip.1] k(U,n(I,x))=k(U,n(x,I)). 18233,18232 [para_from,2172.1.1,6759.1.1.1,demod,26,12221,29,16818,1530,16714,541,26,flip.1] u(k(r(x),x),D)=u(D,k(U,x)). 18235,18234 [para_from,2172.1.1,39.1.1.1,demod,40,20,50,46,46,20,16,2173] n(k(r(x),U),I)=n(k(U,x),I). 18364 [para_into,4403.1.1.1.1.1,17960.1.1,demod,104] u(c(k(n(x,I),y)),y)=U. 18422 [para_from,18364.1.1,11020.1.1.1,demod,541] u(k(n(x,I),y),y)=y. 18436 [para_from,18364.1.1,773.1.1.1,demod,52,541] n(k(n(x,I),y),n(c(y),z))=Z. 19478 [para_from,2088.1.1,2265.1.1.1,demod,541,104] k(n(I,k(x,r(x))),x)=x. 19480 [para_into,19478.1.1.1.2.2,15.1.1,demod,2173] k(n(k(U,x),I),r(x))=r(x). 19498 [para_from,19480.1.1,19.1.1.1,demod,16,16,40,20,50,46,18235,flip.1] k(x,n(k(U,x),I))=x. 19504 [para_from,19498.1.1,18422.1.1.1,demod,12221,1637,12168,17170,2368,8943,flip.1] n(k(U,n(x,I)),I)=n(x,I). 19528 [para_into,19504.1.1.1.2,123.1.1] n(k(U,n(I,x)),I)=n(x,I). 19533,19532 [para_from,19504.1.1,8919.1.1.2,demod,26,6039,26,flip.1] u(D,k(U,n(x,I)))=u(D,x). 19543,19542 [para_from,19528.1.1,8919.1.1.2,demod,26,6039,26,flip.1] u(D,k(U,n(I,x)))=u(D,x). 20737 [para_from,18436.1.1,2324.1.1.2.1,demod,535,218,flip.1] k(n(c(k(x,r(x))),I),x)=Z. 20743 [para_from,20737.1.1,2906.1.1.1.1.1.2,demod,218,535,74,16,541] n(x,n(c(k(r(x),x)),I))=Z. 20765 [para_into,20743.1.1,8075.1.1] n(I,n(x,c(k(r(x),x))))=Z. 20813 [para_from,20765.1.1,560.1.1.1,demod,52,672] n(I,u(c(x),k(r(x),x)))=I. 20867 [para_from,20813.1.1,10510.1.1.1.1.2,demod,18,38,20,16,164,52,34,513,52,9,18233] u(c(r(x)),u(D,k(U,x)))=U. 20953 [para_into,20867.1.1.2.2,18003.1.1,demod,40,46,513,26,19533,9,1532] u(D,u(c(r(x)),x))=U. 20955 [para_into,20867.1.1.2.2,18002.1.1,demod,40,46,513,26,19543,9,1503] u(c(r(x)),u(D,x))=U. 20969 [para_into,20953.1.1,338.1.1] u(x,u(c(r(x)),D))=U. 21026,21025 [para_from,20955.1.1,11020.1.1.1,demod,541] u(r(x),u(D,x))=u(D,x). 21117 [para_from,20969.1.1,8909.1.1.2,demod,38,52,9,21026,602,38,52,flip.1] u(r(x),D)=u(D,x). 21169 [para_from,21117.1.1,6872.1.1.2,demod,76,9041,76,flip.1] n(I,r(x))=n(x,I). 21171 [binary,21169.1,126.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 2459 clauses generated 1074863 clauses kept 11002 clauses forward subsumed 849052 clauses back subsumed 74 Kbytes malloced 11943 ----------- times (seconds) ----------- user CPU time 26.75 (0 hr, 0 min, 26 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 27 (0 hr, 0 min, 27 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 15:46:14 2003