----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Tue Dec 02 00:04:17 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,40000). assign(max_weight,15). 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("ii.txt"). ------- start included file ii.txt------- formula_list(usable). k(U,U)=U. r(U)=U&r(Z)=Z&r(I)=I&r(D)=D. end_of_list. -------> usable clausifies to: list(usable). 0 [] k(U,U)=U. 0 [] r(U)=U. 0 [] r(Z)=Z. 0 [] r(I)=I. 0 [] r(D)=D. end_of_list. ------- end included file ii.txt------- include("v.txt"). ------- start included file v.txt------- formula_list(usable). all x y z (k(x,u(y,z))=u(k(x,y),k(x,z))). 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(x,u(y,z))=u(k(x,y),k(x,z)). 0 [] k(u(x,y),z)=u(k(x,z),k(y,z)). end_of_list. ------- end included file v.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("xxxi_ghost.txt"). ------- start included file xxxi_ghost.txt------- formula_list(usable). -(all x y (n(k(x,U),k(y,U))=Z->k(r(x),y)=Z)). end_of_list. -------> usable clausifies to: list(usable). 0 [] n(k($c2,U),k($c1,U))=Z. 0 [] k(r($c2),$c1)!=Z. end_of_list. ------- end included file xxxi_ghost.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=6): 1 [] k(r($c2),$c1)!=Z. ------------> process sos: ** KEPT (pick-wt=7): 2 [] u(x,y)=u(y,x). ** KEPT (pick-wt=11): 4 [copy,3,flip.1] u(u(x,y),z)=u(x,u(y,z)). ---> New Demodulator: 5 [new_demod,4] u(u(x,y),z)=u(x,u(y,z)). ** KEPT (pick-wt=14): 6 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ---> New Demodulator: 7 [new_demod,6] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ** KEPT (pick-wt=11): 9 [copy,8,flip.1] k(k(x,y),z)=k(x,k(y,z)). ---> New Demodulator: 10 [new_demod,9] k(k(x,y),z)=k(x,k(y,z)). ** KEPT (pick-wt=5): 11 [] r(r(x))=x. ---> New Demodulator: 12 [new_demod,11] r(r(x))=x. ** KEPT (pick-wt=10): 13 [] r(u(x,y))=u(r(x),r(y)). ---> New Demodulator: 14 [new_demod,13] r(u(x,y))=u(r(x),r(y)). ** KEPT (pick-wt=10): 15 [] r(k(x,y))=k(r(y),r(x)). ---> New Demodulator: 16 [new_demod,15] r(k(x,y))=k(r(y),r(x)). ** KEPT (pick-wt=10): 18 [copy,17,flip.1] c(u(c(x),c(y)))=n(x,y). ---> New Demodulator: 19 [new_demod,18] c(u(c(x),c(y)))=n(x,y). ** KEPT (pick-wt=4): 21 [copy,20,flip.1] c(I)=D. ---> New Demodulator: 22 [new_demod,21] c(I)=D. ** KEPT (pick-wt=5): 24 [copy,23,flip.1] u(I,D)=U. ---> New Demodulator: 25 [new_demod,24] u(I,D)=U. ** KEPT (pick-wt=4): 27 [copy,26,flip.1] c(U)=Z. ---> New Demodulator: 28 [new_demod,27] c(U)=Z. ** KEPT (pick-wt=5): 29 [] k(U,U)=U. ---> New Demodulator: 30 [new_demod,29] k(U,U)=U. ** KEPT (pick-wt=4): 31 [] r(U)=U. ---> New Demodulator: 32 [new_demod,31] r(U)=U. ** KEPT (pick-wt=4): 33 [] r(Z)=Z. ---> New Demodulator: 34 [new_demod,33] r(Z)=Z. ** KEPT (pick-wt=4): 35 [] r(I)=I. ---> New Demodulator: 36 [new_demod,35] r(I)=I. ** KEPT (pick-wt=4): 37 [] r(D)=D. ---> New Demodulator: 38 [new_demod,37] r(D)=D. ** KEPT (pick-wt=13): 40 [copy,39,flip.1] u(k(x,y),k(x,z))=k(x,u(y,z)). ---> New Demodulator: 41 [new_demod,40] u(k(x,y),k(x,z))=k(x,u(y,z)). ** KEPT (pick-wt=13): 43 [copy,42,flip.1] u(k(x,y),k(z,y))=k(u(x,z),y). ---> New Demodulator: 44 [new_demod,43] u(k(x,y),k(z,y))=k(u(x,z),y). ** KEPT (pick-wt=16): 45 [] n(x,k(n(y,k(x,r(z))),z))=n(k(y,z),x). ** KEPT (pick-wt=9): 46 [] n(k($c2,U),k($c1,U))=Z. ---> New Demodulator: 47 [new_demod,46] n(k($c2,U),k($c1,U))=Z. Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] u(x,y)=u(y,x). >>>> Starting back demodulation with 5. >>>> Starting back demodulation with 7. >>>> Starting back demodulation with 10. >>>> Starting back demodulation with 12. >>>> Starting back demodulation with 14. >>>> Starting back demodulation with 16. >>>> Starting back demodulation with 19. >> back demodulating 6 with 19. >>>> Starting back demodulation with 22. >>>> Starting back demodulation with 25. >>>> Starting back demodulation with 28. >>>> Starting back demodulation with 30. >>>> Starting back demodulation with 32. >>>> Starting back demodulation with 34. >>>> Starting back demodulation with 36. >>>> Starting back demodulation with 38. >>>> Starting back demodulation with 41. >>>> Starting back demodulation with 44. ** KEPT (pick-wt=16): 50 [copy,45,flip.1] n(k(x,y),z)=n(z,k(n(x,k(z,r(y))),y)). >>>> Starting back demodulation with 47. >>>> Starting back demodulation with 49. Following clause subsumed by 45 during input processing: 0 [copy,50,flip.1] n(x,k(n(y,k(x,r(z))),z))=n(k(y,z),x). ======= end of input processing ======= =========== start of search =========== ----> UNIT CONFLICT at 3.91 sec ----> 17176 [binary,17174.1,1.1] $F. Length of proof is 287. Level of proof is 56. ---------------- PROOF ---------------- 1 [] k(r($c2),$c1)!=Z. 2 [] u(x,y)=u(y,x). 3 [] u(x,u(y,z))=u(u(x,y),z). 5,4 [copy,3,flip.1] u(u(x,y),z)=u(x,u(y,z)). 6 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 8 [] k(x,k(y,z))=k(k(x,y),z). 10,9 [copy,8,flip.1] k(k(x,y),z)=k(x,k(y,z)). 12,11 [] r(r(x))=x. 14,13 [] r(u(x,y))=u(r(x),r(y)). 16,15 [] r(k(x,y))=k(r(y),r(x)). 17 [] n(x,y)=c(u(c(x),c(y))). 19,18 [copy,17,flip.1] c(u(c(x),c(y)))=n(x,y). 20 [] D=c(I). 22,21 [copy,20,flip.1] c(I)=D. 23 [] U=u(I,D). 25,24 [copy,23,flip.1] u(I,D)=U. 26 [] Z=c(U). 28,27 [copy,26,flip.1] c(U)=Z. 30,29 [] k(U,U)=U. 32,31 [] r(U)=U. 34,33 [] r(Z)=Z. 39 [] k(x,u(y,z))=u(k(x,y),k(x,z)). 40 [copy,39,flip.1] u(k(x,y),k(x,z))=k(x,u(y,z)). 45 [] n(x,k(n(y,k(x,r(z))),z))=n(k(y,z),x). 46 [] n(k($c2,U),k($c1,U))=Z. 48 [back_demod,6,demod,19] u(c(u(c(x),y)),n(x,y))=x. 50 [copy,45,flip.1] n(k(x,y),z)=n(z,k(n(x,k(z,r(y))),y)). 54 [para_into,4.1.1.1,2.1.1,demod,5] u(x,u(y,z))=u(y,u(x,z)). 55 [para_into,4.1.1,2.1.1] u(x,u(y,z))=u(y,u(z,x)). 56 [copy,55,flip.1] u(x,u(y,z))=u(z,u(x,y)). 62 [para_into,24.1.1,2.1.1] u(D,I)=U. 65,64 [para_from,24.1.1,4.1.1.1] u(U,x)=u(I,u(D,x)). 68 [para_into,64.1.1,2.1.1] u(x,U)=u(I,u(D,x)). 69 [copy,68,flip.1] u(I,u(D,x))=u(x,U). 70 [para_into,68.1.1,4.1.1] u(x,u(y,U))=u(I,u(D,u(x,y))). 71 [copy,70,flip.1] u(I,u(D,u(x,y)))=u(x,u(y,U)). 77 [para_into,69.1.1,2.1.1,demod,5] u(D,u(x,I))=u(x,U). 81,80 [para_into,18.1.1.1.1,27.1.1] c(u(Z,c(x)))=n(U,x). 84 [para_into,18.1.1.1.1,18.1.1] c(u(n(x,y),c(z)))=n(u(c(x),c(y)),z). 87,86 [para_into,18.1.1.1.2,27.1.1] c(u(c(x),Z))=n(x,U). 88 [para_into,18.1.1.1.2,21.1.1] c(u(c(x),D))=n(x,I). 90 [para_into,18.1.1.1.2,18.1.1] c(u(c(x),n(y,z)))=n(x,u(c(y),c(z))). 92 [para_into,18.1.1.1,2.1.1,demod,19] n(x,y)=n(y,x). 93 [para_into,92.1.1,46.1.1,flip.1] n(k($c1,U),k($c2,U))=Z. 98 [para_into,77.1.1.2,2.1.1] u(D,u(I,x))=u(x,U). 100 [copy,98,flip.1] u(x,U)=u(D,u(I,x)). 119,118 [para_into,80.1.1.1.2,27.1.1] c(u(Z,Z))=n(U,U). 122 [para_into,80.1.1.1.2,18.1.1] c(u(Z,n(x,y)))=n(U,u(c(x),c(y))). 161 [para_into,86.1.1.1.1,18.1.1] c(u(n(x,y),Z))=n(u(c(x),c(y)),U). 166 [para_into,45.1.1.2.1.2.2,31.1.1] n(x,k(n(y,k(x,U)),U))=n(k(y,U),x). 195 [para_into,48.1.1.1.1.1,27.1.1] u(c(u(Z,x)),n(U,x))=U. 197 [para_into,48.1.1.1.1.1,21.1.1] u(c(u(D,x)),n(I,x))=I. 207 [para_into,48.1.1.1.1,2.1.1] u(c(u(x,c(y))),n(y,x))=y. 209 [para_into,48.1.1.1,88.1.1] u(n(x,I),n(x,D))=x. 211 [para_into,48.1.1.1,86.1.1] u(n(x,U),n(x,Z))=x. 213 [para_into,48.1.1.1,18.1.1] u(n(x,y),n(x,c(y)))=x. 215 [para_into,48.1.1.2,93.1.1] u(c(u(c(k($c1,U)),k($c2,U))),Z)=k($c1,U). 217 [para_into,48.1.1.2,92.1.1] u(c(u(c(x),y)),n(y,x))=x. 219 [para_into,48.1.1.2,46.1.1] u(c(u(c(k($c2,U)),k($c1,U))),Z)=k($c2,U). 221 [para_into,48.1.1,2.1.1] u(n(x,y),c(u(c(x),y)))=x. 225 [para_from,48.1.1,4.1.1.1,flip.1] u(c(u(c(x),y)),u(n(x,y),z))=u(x,z). 227 [para_into,209.1.1.1,92.1.1] u(n(I,x),n(x,D))=x. 231 [para_into,209.1.1,2.1.1] u(n(x,D),n(x,I))=x. 237 [para_into,211.1.1.1,92.1.1] u(n(U,x),n(x,Z))=x. 239 [para_into,211.1.1.2,92.1.1] u(n(x,U),n(Z,x))=x. 241 [para_into,211.1.1,2.1.1] u(n(x,Z),n(x,U))=x. 245 [para_from,211.1.1,4.1.1.1,flip.1] u(n(x,U),u(n(x,Z),y))=u(x,y). 247 [para_into,227.1.1.2,92.1.1] u(n(I,x),n(D,x))=x. 263 [para_into,50.1.1,93.1.1,demod,32,10,30,flip.1] n(k($c2,U),k(n($c1,k($c2,U)),U))=Z. 269 [para_from,231.1.1,4.1.1.1,flip.1] u(n(x,D),u(n(x,I),y))=u(x,y). 271 [para_into,237.1.1.2,92.1.1] u(n(U,x),n(Z,x))=x. 277 [para_from,237.1.1,4.1.1.1,flip.1] u(n(U,x),u(n(x,Z),y))=u(x,y). 279 [para_into,239.1.1,2.1.1] u(n(Z,x),n(x,U))=x. 287 [para_from,241.1.1,4.1.1.1,flip.1] u(n(x,Z),u(n(x,U),y))=u(x,y). 292,291 [para_into,54.1.1.2,239.1.1,flip.1] u(n(x,U),u(y,n(Z,x)))=u(y,x). 294,293 [para_into,54.1.1.2,237.1.1,flip.1] u(n(U,x),u(y,n(x,Z)))=u(y,x). 311 [para_into,54.1.1.2,48.1.1,flip.1] u(c(u(c(x),y)),u(z,n(x,y)))=u(z,x). 320 [para_from,54.1.1,48.1.1.1.1] u(c(u(x,u(c(y),z))),n(y,u(x,z)))=y. 342 [para_into,271.1.1,2.1.1] u(n(Z,x),n(U,x))=x. 356 [para_into,55.1.1.2,69.1.1,demod,5] u(x,u(y,U))=u(I,u(D,u(y,x))). 359 [para_into,55.1.1.2,2.1.1] u(x,u(y,z))=u(z,u(y,x)). 392 [para_from,342.1.1,54.1.1.2,flip.1] u(n(Z,x),u(y,n(U,x)))=u(y,x). 399 [para_into,56.1.1.2,48.1.1,flip.1] u(n(x,y),u(z,c(u(c(x),y))))=u(z,x). 406 [para_from,56.1.1,48.1.1.1.1] u(c(u(x,u(c(y),z))),n(y,u(z,x)))=y. 422 [para_into,195.1.1.1.1,2.1.1] u(c(u(x,Z)),n(U,x))=U. 424 [para_into,195.1.1.2,92.1.1] u(c(u(Z,x)),n(x,U))=U. 426 [para_into,195.1.1,2.1.1] u(n(U,x),c(u(Z,x)))=U. 444 [para_into,197.1.1.1.1,62.1.1,demod,28] u(Z,n(I,I))=I. 469,468 [para_into,444.1.1,2.1.1] u(n(I,I),Z)=I. 477,476 [para_from,444.1.1,56.1.1.2,flip.1] u(n(I,I),u(x,Z))=u(x,I). 483,482 [para_from,468.1.1,4.1.1.1,flip.1] u(n(I,I),u(Z,x))=u(I,x). 538 [para_into,213.1.1.1,92.1.1] u(n(x,y),n(y,c(x)))=y. 558 [para_into,213.1.1.2,92.1.1] u(n(x,y),n(c(y),x))=x. 561,560 [para_into,213.1.1,2.1.1] u(n(x,c(y)),n(x,y))=x. 566 [para_from,213.1.1,56.1.1.2,flip.1] u(n(x,c(y)),u(z,n(x,y)))=u(z,x). 570 [para_into,422.1.1.2,92.1.1] u(c(u(x,Z)),n(x,U))=U. 608 [para_into,424.1.1,2.1.1] u(n(x,U),c(u(Z,x)))=U. 628 [para_into,426.1.1.2.1,68.1.1] u(n(U,U),c(u(I,u(D,Z))))=U. 764 [para_into,84.1.1.1,426.1.1,demod,28,28,flip.1] n(u(Z,c(x)),u(Z,x))=Z. 786 [para_into,538.1.1.2,92.1.1] u(n(x,y),n(c(x),y))=y. 788 [para_into,538.1.1,2.1.1] u(n(x,c(y)),n(y,x))=x. 818 [para_into,558.1.1,2.1.1] u(n(c(x),y),n(y,x))=y. 837 [para_into,90.1.1.1,424.1.1,demod,28,28,flip.1] n(u(Z,x),u(c(x),Z))=Z. 845 [para_into,90.1.1.1,48.1.1,flip.1] n(u(c(x),y),u(c(x),c(y)))=c(x). 871 [para_into,570.1.1,2.1.1] u(n(x,U),c(u(x,Z)))=U. 877 [para_from,570.1.1,13.1.1.1,demod,32,flip.1] u(r(c(u(x,Z))),r(n(x,U)))=U. 919 [para_from,608.1.1,84.1.1.1,demod,28,28,flip.1] n(u(c(x),Z),u(Z,x))=Z. 1099 [para_into,764.1.1.1.2,27.1.1] n(u(Z,Z),u(Z,U))=Z. 1163 [para_into,1099.1.1,92.1.1] n(u(Z,U),u(Z,Z))=Z. 1167 [para_from,1099.1.1,558.1.1.1] u(Z,n(c(u(Z,U)),u(Z,Z)))=u(Z,Z). 1243 [para_into,1163.1.1.1,68.1.1] n(u(I,u(D,Z)),u(Z,Z))=Z. 1328 [para_into,786.1.1,2.1.1] u(n(c(x),y),n(x,y))=y. 1400 [para_into,818.1.1.2,1099.1.1] u(n(c(u(Z,U)),u(Z,Z)),Z)=u(Z,Z). 1612 [para_from,871.1.1,84.1.1.1,demod,28,28,flip.1] n(u(c(x),Z),u(x,Z))=Z. 1614 [para_from,871.1.1,13.1.1.1,demod,32,flip.1] u(r(n(x,U)),r(c(u(x,Z))))=U. 1880 [para_from,1328.1.1,13.1.1.1,flip.1] u(r(n(c(x),y)),r(n(x,y)))=r(y). 1995 [para_into,207.1.1.2,1612.1.1,demod,87,5] u(c(u(x,u(Z,n(x,U)))),Z)=u(c(x),Z). 2025 [para_into,207.1.1.2,92.1.1] u(c(u(x,c(y))),n(x,y))=y. 2029 [para_into,207.1.1,2.1.1] u(n(x,y),c(u(y,c(x))))=x. 2057 [para_into,217.1.1,2.1.1] u(n(x,y),c(u(c(y),x)))=y. 2441 [para_into,166.1.1.2.1,93.1.1,demod,10,30,flip.1] n(k($c1,U),$c2)=n($c2,k(Z,U)). 2443 [para_into,166.1.1.2.1,92.1.1] n(x,k(n(k(x,U),y),U))=n(k(y,U),x). 2444 [para_into,166.1.1.2.1,46.1.1,demod,10,30,flip.1] n(k($c2,U),$c1)=n($c1,k(Z,U)). 2807 [para_into,2025.1.1,2.1.1] u(n(x,y),c(u(x,c(y))))=y. 2891 [para_into,2441.1.1,92.1.1,flip.1] n($c2,k(Z,U))=n($c2,k($c1,U)). 2893 [para_into,2444.1.1,92.1.1,flip.1] n($c1,k(Z,U))=n($c1,k($c2,U)). 2895 [para_from,215.1.1,86.1.1.1,flip.1] n(u(c(k($c1,U)),k($c2,U)),U)=c(k($c1,U)). 2921 [para_into,2893.1.1,92.1.1] n(k(Z,U),$c1)=n($c1,k($c2,U)). 2939 [para_from,219.1.1,86.1.1.1,flip.1] n(u(c(k($c2,U)),k($c1,U)),U)=c(k($c2,U)). 2987 [para_into,225.1.1.2,2807.1.1] u(c(u(c(x),y)),y)=u(x,c(u(x,c(y)))). 3004,3003 [para_into,225.1.1.2,788.1.1,demod,19] u(n(x,y),x)=u(x,n(y,x)). 3006,3005 [para_into,225.1.1.2,786.1.1] u(c(u(c(x),y)),y)=u(x,n(c(x),y)). 3013 [para_into,225.1.1.2,560.1.1,demod,19,3004] u(x,n(y,x))=u(x,n(x,y)). 3016 [para_into,225.1.1.2,538.1.1,demod,3006] u(x,n(c(x),y))=u(x,n(y,c(x))). 3018,3017 [para_into,225.1.1.2,342.1.1,demod,3006] u(Z,n(c(Z),x))=u(Z,n(U,x)). 3021 [para_into,225.1.1.2,279.1.1,demod,3006,3018] u(Z,n(U,x))=u(Z,n(x,U)). 3022 [para_into,225.1.1.2,271.1.1,demod,28,65] u(c(u(Z,x)),x)=u(I,u(D,n(Z,x))). 3026,3025 [para_into,225.1.1.2,247.1.1,demod,22] u(c(u(D,x)),x)=u(I,n(D,x)). 3028 [para_into,225.1.1.2,227.1.1,demod,22,3026] u(I,n(D,x))=u(I,n(x,D)). 3032,3031 [copy,2987,flip.1,demod,3006] u(x,c(u(x,c(y))))=u(x,n(c(x),y)). 3049 [copy,3016,flip.1] u(x,n(y,c(x)))=u(x,n(c(x),y)). 3050 [copy,3021,flip.1] u(Z,n(x,U))=u(Z,n(U,x)). 3053 [copy,3028,flip.1] u(I,n(x,D))=u(I,n(D,x)). 3260 [para_into,245.1.1.2,2807.1.1,demod,3032,flip.1] u(x,n(c(x),Z))=u(n(x,U),Z). 3266 [para_into,245.1.1.2,538.1.1,flip.1] u(x,n(Z,c(x)))=u(n(x,U),Z). 3270 [para_into,245.1.1.2,271.1.1,demod,65] u(n(U,U),Z)=u(I,u(D,n(Z,Z))). 3361,3360 [para_into,3003.1.1,100.1.1,demod,65,flip.1] u(I,u(D,n(x,U)))=u(D,u(I,n(U,x))). 3373,3372 [para_from,3003.1.1,476.1.1.2,demod,483,flip.1] u(n(Z,x),I)=u(I,n(x,Z)). 3412 [para_from,3003.1.1,54.1.1.2] u(x,u(y,n(z,y)))=u(n(y,z),u(x,y)). 3425 [copy,3412,flip.1] u(n(x,y),u(z,x))=u(z,u(x,n(y,x))). 3429,3428 [para_into,3013.1.1,2.1.1] u(n(x,y),y)=u(y,n(y,x)). 3442 [para_from,3013.1.1,482.1.1.2,demod,483] u(I,n(Z,x))=u(I,n(x,Z)). 3452,3451 [para_from,3013.1.1,98.1.1.2,flip.1] u(n(x,I),U)=u(D,u(I,n(I,x))). 3471 [para_from,3013.1.1,13.1.1.1,demod,14] u(r(x),r(n(x,y)))=u(r(x),r(n(y,x))). 3481 [copy,3442,flip.1] u(I,n(x,Z))=u(I,n(Z,x)). 3482 [copy,3471,flip.1] u(r(x),r(n(y,x)))=u(r(x),r(n(x,y))). 3489,3488 [para_into,3021.1.1,2.1.1] u(n(U,x),Z)=u(Z,n(x,U)). 3491,3490 [back_demod,3270,demod,3489] u(Z,n(U,U))=u(I,u(D,n(Z,Z))). 3609,3608 [para_into,3050.1.1,2.1.1] u(n(x,U),Z)=u(Z,n(U,x)). 3612 [back_demod,3266,demod,3609] u(x,n(Z,c(x)))=u(Z,n(U,x)). 3617,3616 [back_demod,3260,demod,3609] u(x,n(c(x),Z))=u(Z,n(U,x)). 3658 [para_into,263.1.1.2.1,92.1.1] n(k($c2,U),k(n(k($c2,U),$c1),U))=Z. 3697,3696 [para_into,3053.1.1,2.1.1] u(n(x,D),I)=u(I,n(D,x)). 3783,3782 [para_from,3372.1.1,77.1.1.2,flip.1] u(n(Z,x),U)=u(D,u(I,n(x,Z))). 3812,3811 [para_into,269.1.1.2,279.1.1,demod,3697,flip.1] u(Z,n(I,U))=u(I,n(D,Z)). 3838 [para_from,3428.1.1,13.1.1.1,demod,14] u(r(x),r(n(x,y)))=u(r(n(y,x)),r(x)). 3844 [copy,3838,flip.1] u(r(n(x,y)),r(y))=u(r(y),r(n(y,x))). 3851,3850 [para_from,3481.1.1,98.1.1.2,flip.1] u(n(x,Z),U)=u(D,u(I,n(Z,x))). 3863,3862 [para_from,3488.1.1,269.1.1.2,demod,3812,294,25,65,flip.1] u(I,u(D,Z))=U. 3865,3864 [para_from,3488.1.1,245.1.1.2,demod,292,65,3863] u(Z,U)=U. 3871 [back_demod,1243,demod,3863] n(U,u(Z,Z))=Z. 3876,3875 [back_demod,628,demod,3863,28,3609,3491] u(I,u(D,n(Z,Z)))=U. 3894 [back_demod,1400,demod,3865,28,3004] u(Z,n(u(Z,Z),Z))=u(Z,Z). 3896 [back_demod,1167,demod,3865,28] u(Z,n(Z,u(Z,Z)))=u(Z,Z). 3904,3903 [back_demod,3490,demod,3876] u(Z,n(U,U))=U. 3913,3912 [para_into,277.1.1.2,818.1.1,demod,3489,flip.1] u(c(x),n(Z,x))=u(Z,n(c(x),U)). 3919,3918 [para_into,277.1.1.2,213.1.1,demod,3429,flip.1] u(x,n(x,c(Z)))=u(x,n(x,U)). 3925,3924 [para_into,3864.1.1,100.1.1] u(D,u(I,Z))=U. 3941,3940 [para_from,3864.1.1,482.1.1.2,demod,3452] u(D,u(I,n(I,I)))=u(I,U). 3947,3946 [para_from,3864.1.1,70.1.1.2,flip.1] u(I,u(D,u(x,Z)))=u(x,U). 3954,3953 [para_from,3864.1.1,54.1.1.2,flip.1] u(Z,u(x,U))=u(x,U). 3959,3958 [para_from,3862.1.1,4.1.1.1,demod,65,5,flip.1] u(I,u(D,u(Z,x)))=u(I,u(D,x)). 3966 [para_from,3871.1.1,818.1.1.2,demod,119,3609] u(Z,n(U,n(U,U)))=U. 3968 [para_from,3871.1.1,217.1.1.2,demod,119,3004,65,3361] u(c(u(D,u(I,n(U,U)))),Z)=u(Z,Z). 3994 [para_from,3903.1.1,919.1.1.2] n(u(c(n(U,U)),Z),U)=Z. 4001,4000 [para_from,3903.1.1,482.1.1.2,demod,3452,3941,flip.1] u(I,n(U,U))=u(I,U). 4014,4013 [back_demod,3968,demod,4001] u(c(u(D,u(I,U))),Z)=u(Z,Z). 4118 [para_into,287.1.1.2,2029.1.1,demod,3004,65,flip.1] u(x,c(u(I,u(D,c(x)))))=u(x,n(Z,x)). 4239,4238 [para_from,3966.1.1,482.1.1.2,demod,3452,3941,flip.1] u(I,n(U,n(U,U)))=u(I,U). 4708 [para_from,3994.1.1,207.1.1.2,demod,87,65,3361,4239,4014,flip.1] u(c(n(U,U)),Z)=u(Z,Z). 5188,5187 [para_into,311.1.1.2,788.1.1,demod,3006,flip.1] u(n(x,c(y)),y)=u(y,n(c(y),x)). 5258,5257 [para_from,4708.1.1,86.1.1.1,demod,119,flip.1] n(n(U,U),U)=n(U,U). 5261 [para_from,4708.1.1,71.1.1.2.2,demod,3947,3865,3865,flip.1] u(c(n(U,U)),U)=U. 5280,5279 [para_from,5261.1.1,2057.1.1.2.1,demod,28,3489,5258,3904,flip.1] n(U,U)=U. 5314,5313 [back_demod,118,demod,5280] c(u(Z,Z))=U. 5326,5325 [para_from,5279.1.1,90.1.1.1.2,demod,28,28] c(u(c(x),U))=n(x,u(Z,Z)). 5332,5331 [para_from,5279.1.1,84.1.1.1.1,demod,65,28,28] c(u(I,u(D,c(x))))=n(u(Z,Z),x). 5351,5350 [back_demod,4118,demod,5332] u(x,n(u(Z,Z),x))=u(x,n(Z,x)). 5353 [back_demod,3894,demod,5351] u(Z,n(Z,Z))=u(Z,Z). 5377 [para_from,5353.1.1,482.1.1.2,demod,477] u(Z,I)=u(I,n(Z,Z)). 5383 [para_from,5353.1.1,122.1.1.1,demod,5314,flip.1] n(U,u(c(Z),c(Z)))=U. 5512,5511 [para_into,5377.1.1,2.1.1,flip.1] u(I,n(Z,Z))=u(I,Z). 5515 [para_from,5383.1.1,217.1.1.2,demod,19,3851,5512,3925,28,3865,flip.1] u(c(Z),c(Z))=U. 5534 [para_from,5515.1.1,2057.1.1.2.1,demod,28,3429,3919] u(Z,n(Z,U))=Z. 5536 [para_from,5515.1.1,2029.1.1.2.1,demod,28,3004,3617] u(Z,n(U,Z))=Z. 5588 [para_from,5534.1.1,482.1.1.2,demod,469,flip.1] u(I,n(Z,U))=I. 5604 [para_from,5536.1.1,837.1.1.1] n(Z,u(c(n(U,Z)),Z))=Z. 5616 [para_from,5536.1.1,195.1.1.1.1] u(c(Z),n(U,n(U,Z)))=U. 5655,5654 [para_from,5588.1.1,311.1.1.2,demod,5326,3373] u(I,n(u(Z,Z),Z))=u(I,Z). 6222 [para_from,5604.1.1,320.1.1.2] u(c(u(c(n(U,Z)),u(c(Z),Z))),Z)=Z. 6265 [para_from,5616.1.1,311.1.1.1.1,demod,28] u(Z,u(x,n(Z,n(U,n(U,Z)))))=u(x,Z). 6739 [para_from,3896.1.1,122.1.1.1,demod,5314,5314,flip.1] n(U,u(c(Z),U))=U. 6757 [para_from,6739.1.1,217.1.1.2,demod,5326,3783,5655,3925,28,3865,flip.1] u(c(Z),U)=U. 6779 [para_from,6757.1.1,320.1.1.1.1.2,demod,3913] u(Z,n(c(u(x,U)),U))=Z. 6969 [para_into,6779.1.1.2,92.1.1] u(Z,n(U,c(u(x,U))))=Z. 7178,7177 [para_from,6969.1.1,311.1.1.2,demod,28,81,3489,3865] u(Z,n(u(x,U),U))=U. 7227 [para_into,7177.1.1.2,92.1.1] u(Z,n(U,u(x,U)))=U. 7277 [para_from,7227.1.1,311.1.1.2,demod,28,3954,3865] u(c(u(x,U)),U)=U. 7344,7343 [para_from,7277.1.1,2057.1.1.2.1,demod,28,3489,7178,flip.1] u(x,U)=U. 7346,7345 [para_from,7277.1.1,356.1.1.2,demod,7344,7344,28,3959,flip.1] u(I,u(D,x))=U. 7350,7349 [para_from,7277.1.1,320.1.1.2.2,demod,7344,28,7344,7344,28] u(Z,n(x,U))=x. 7573 [back_demod,5325,demod,7344,28,flip.1] n(x,u(Z,Z))=Z. 7911 [back_demod,5331,demod,7346,28,flip.1] n(u(Z,Z),x)=Z. 7931 [back_demod,3022,demod,7346] u(c(u(Z,x)),x)=U. 7990,7989 [back_demod,3050,demod,7350,flip.1] u(Z,n(U,x))=x. 7993 [back_demod,1995,demod,7350] u(c(u(x,x)),Z)=u(c(x),Z). 8264 [back_demod,3612,demod,7990] u(x,n(Z,c(x)))=x. 8420 [para_into,7349.1.1.2,50.1.1,demod,7990] k(n(x,k(U,r(y))),y)=k(x,y). 8488 [para_from,7573.1.1,2029.1.1.1,demod,5] u(Z,c(u(Z,u(Z,c(x)))))=x. 8756 [para_into,399.1.1.2,2807.1.1,demod,5188] u(x,n(c(x),y))=u(n(c(y),x),y). 8757 [copy,8756,flip.1] u(n(c(x),y),x)=u(y,n(c(y),x)). 8822 [para_into,406.1.1.1.1.2,422.1.1,demod,7344,28] u(Z,n(u(x,Z),u(n(U,x),y)))=u(x,Z). 9294 [para_into,7931.1.1,56.1.1] u(x,u(c(u(Z,u(y,x))),y))=U. 9313,9312 [para_from,7931.1.1,392.1.1.2,demod,7344,7990,flip.1] u(c(x),x)=U. 9353 [para_from,7931.1.1,221.1.1.2.1,demod,28] u(n(u(Z,x),x),Z)=u(Z,x). 9370,9369 [back_demod,6222,demod,9313,7344,28] u(Z,Z)=Z. 9383,9382 [back_demod,7911,demod,9370] n(Z,x)=Z. 9385,9384 [back_demod,7573,demod,9370] n(x,Z)=Z. 9413,9412 [back_demod,8264,demod,9383] u(x,Z)=x. 9421,9420 [back_demod,6265,demod,9385,9385,9385,9413,9413] u(Z,x)=x. 9437,9436 [back_demod,271,demod,9383,9413] n(U,x)=x. 9439,9438 [back_demod,239,demod,9383,9413] n(x,U)=x. 9463,9462 [back_demod,8488,demod,9421,9421,9421] c(c(x))=x. 9498,9497 [back_demod,9353,demod,9421,9413,9421] n(x,x)=x. 9501 [back_demod,8822,demod,9413,9437,9421,9413] n(x,u(x,y))=x. 9505 [back_demod,7993,demod,9413,9413] c(u(x,x))=c(x). 9535 [back_demod,1614,demod,9439,9413] u(r(x),r(c(x)))=U. 9541 [back_demod,877,demod,9413,9439] u(r(c(x)),r(x))=U. 9552,9551 [back_demod,161,demod,9413,9439] c(n(x,y))=u(c(x),c(y)). 9563 [back_demod,9294,demod,9421] u(x,u(c(u(y,x)),y))=U. 9589 [back_demod,2939,demod,9439] u(c(k($c2,U)),k($c1,U))=c(k($c2,U)). 9591 [back_demod,2895,demod,9439] u(c(k($c1,U)),k($c2,U))=c(k($c1,U)). 9675 [para_from,9436.1.1,90.1.1.1.2,demod,28,9421] c(u(c(x),y))=n(x,c(y)). 9834 [para_into,9501.1.1.2,359.1.1] n(x,u(y,u(z,x)))=x. 9862 [para_into,9501.1.1,92.1.1] n(u(x,y),x)=x. 10007,10006 [para_from,9505.1.1,9462.1.1.1,demod,9463,flip.1] u(x,x)=x. 10028 [para_into,10006.1.1,359.1.1] u(x,u(y,u(y,x)))=u(y,x). 10033,10032 [para_into,10006.1.1,54.1.1,demod,5,10007] u(x,u(x,y))=u(x,y). 10037,10036 [back_demod,10028,demod,10033] u(x,u(y,x))=u(y,x). 10220 [para_into,9862.1.1.1,786.1.1] n(x,n(y,x))=n(y,x). 10467,10466 [para_into,566.1.1.2,10006.1.1,demod,561,3004,flip.1] u(x,n(y,x))=x. 10484,10483 [back_demod,3425,demod,10467] u(n(x,y),u(z,x))=u(z,x). 10531,10530 [para_from,10466.1.1,566.1.1.2,demod,5188] u(x,n(c(x),y))=u(x,y). 10545,10544 [para_from,10466.1.1,13.1.1.1,flip.1] u(r(x),r(n(y,x)))=r(x). 10557,10556 [back_demod,8757,demod,10531] u(n(c(x),y),x)=u(y,x). 10560 [back_demod,3049,demod,10531] u(x,n(y,c(x)))=u(x,y). 10591,10590 [back_demod,3482,demod,10545,flip.1] u(r(x),r(n(x,y)))=r(x). 10606 [back_demod,3844,demod,10591] u(r(n(x,y)),r(y))=r(y). 10716 [para_into,9535.1.1.1,11.1.1] u(x,r(c(r(x))))=U. 10730 [para_into,9541.1.1.2,11.1.1] u(r(c(r(x))),x)=U. 11940 [para_into,845.1.1.1.1,9462.1.1,demod,9463,9463] n(u(x,y),u(x,c(y)))=x. 12156,12155 [para_into,9675.1.1.1.1,9462.1.1] c(u(x,y))=n(c(x),c(y)). 12161 [para_into,9675.1.1.1,9563.1.1,demod,28,12156,9463,10557,12156,flip.1] n(x,n(c(x),c(y)))=Z. 12427 [para_into,12161.1.1.2.2,9462.1.1] n(x,n(c(x),y))=Z. 12461 [para_into,12427.1.1.2,10220.1.1] n(x,n(y,c(x)))=Z. 12481 [para_into,12461.1.1,92.1.1] n(n(x,c(y)),y)=Z. 13159 [para_into,11940.1.1.1,10716.1.1,demod,9437] u(x,c(r(c(r(x)))))=x. 13165 [para_into,11940.1.1.1,10560.1.1,demod,9552,9463,10037] n(u(x,y),u(c(y),x))=x. 13193,13192 [para_into,11940.1.1.1,538.1.1,demod,9552,9463,10484] n(x,u(c(x),y))=n(y,x). 13217,13216 [para_into,11940.1.1.2,10730.1.1,demod,9439] u(r(c(r(c(x)))),x)=r(c(r(c(x)))). 13305 [para_into,13159.1.1,2.1.1] u(c(r(c(r(x)))),x)=x. 13562 [para_from,13305.1.1,13.1.1.1,demod,13217,flip.1] r(c(r(c(r(x)))))=r(x). 13714 [para_into,13562.1.1.1.1.1.1,11.1.1,demod,12] r(c(r(c(x))))=x. 13717 [para_into,1880.1.1.1.1,9501.1.1,demod,13193,14] u(r(c(x)),r(n(y,x)))=u(r(c(x)),r(y)). 13721 [para_into,13714.1.1.1.1.1,9462.1.1] r(c(r(x)))=c(x). 13762,13761 [para_into,13721.1.1.1.1,11.1.1] r(c(x))=c(r(x)). 13772,13771 [back_demod,13717,demod,13762,13762] u(c(r(x)),r(n(y,x)))=u(c(r(x)),r(y)). 13928,13927 [para_into,13165.1.1.1,10606.1.1,demod,13772,13193,flip.1] r(n(x,y))=n(r(x),r(y)). 14096,14095 [para_into,13927.1.1.1,2921.1.1,demod,13928,16,32,16,32,34] n(r($c1),k(U,r($c2)))=n(k(U,Z),r($c1)). 14230 [para_into,2443.1.1.2.1,9438.1.1,demod,10,30,30,9437] n(x,k(x,U))=x. 14282 [para_from,14230.1.1,10466.1.1.2] u(k(x,U),x)=k(x,U). 14748 [para_from,14282.1.1,9834.1.1.2.2] n(x,u(y,k(x,U)))=x. 15854 [para_from,9589.1.1,14748.1.1.2] n($c1,c(k($c2,U)))=$c1. 15881,15880 [para_from,15854.1.1,12461.1.1.2] n(k($c2,U),$c1)=Z. 15884 [para_from,15854.1.1,12481.1.1.1] n($c1,k($c2,U))=Z. 15920 [back_demod,3658,demod,15881] n(k($c2,U),k(Z,U))=Z. 15951,15950 [para_from,15884.1.1,13927.1.1.1,demod,34,16,32,14096,flip.1] n(k(U,Z),r($c1))=Z. 15958 [back_demod,14095,demod,15951] n(r($c1),k(U,r($c2)))=Z. 15974 [para_from,9591.1.1,14748.1.1.2] n($c2,c(k($c1,U)))=$c2. 16093,16092 [para_from,15974.1.1,12481.1.1.1] n($c2,k($c1,U))=Z. 16135,16134 [back_demod,2891,demod,16093] n($c2,k(Z,U))=Z. 17049,17048 [para_into,15920.1.1,50.1.1,demod,32,10,30,16135,9498] k(Z,U)=Z. 17057,17056 [para_from,17048.1.1,40.1.1.2,demod,9413,7344,17049] k(Z,x)=Z. 17124 [para_from,15958.1.1,8420.1.1.1,demod,17057,flip.1] k(r($c1),$c2)=Z. 17174 [para_from,17124.1.1,15.1.1.1,demod,34,12,flip.1] k(r($c2),$c1)=Z. 17176 [binary,17174.1,1.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 1187 clauses generated 94283 clauses kept 9332 clauses forward subsumed 78387 clauses back subsumed 79 Kbytes malloced 7887 ----------- times (seconds) ----------- user CPU time 4.12 (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 Tue Dec 02 00:04:21 2003