----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sun Nov 30 16:00:53 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,64000). 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("peirceanAx1.txt"). ------- start included file peirceanAx1.txt------- formula_list(usable). 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(u(x,y),z)=u(k(x,z),k(y,z)). end_of_list. ------- end included file peirceanAx1.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("cycleLawA.txt"). ------- start included file cycleLawA.txt------- formula_list(usable). all x y z (n(x,k(z,r(y)))=Z->n(z,k(x,y))=Z). end_of_list. -------> usable clausifies to: list(usable). 0 [] n(x,k(z,r(y)))!=Z|n(z,k(x,y))=Z. end_of_list. ------- end included file cycleLawA.txt------- include("xxiv_a.txt"). ------- start included file xxiv_a.txt------- formula_list(usable). -(all x (n(k(n(I,x),U),k(n(I,c(x)),U))=Z)). end_of_list. -------> usable clausifies to: list(usable). 0 [] n(k(n(I,$c1),U),k(n(I,c($c1)),U))!=Z. end_of_list. ------- end included file xxiv_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=15): 1 [] n(x,k(y,r(z)))!=Z|n(y,k(x,z))=Z. ** KEPT (pick-wt=14): 2 [] n(k(n(I,$c1),U),k(n(I,c($c1)),U))!=Z. ------------> process sos: ** KEPT (pick-wt=7): 3 [] u(x,y)=u(y,x). ** KEPT (pick-wt=11): 5 [copy,4,flip.1] u(u(x,y),z)=u(x,u(y,z)). ---> New Demodulator: 6 [new_demod,5] u(u(x,y),z)=u(x,u(y,z)). ** KEPT (pick-wt=14): 7 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ---> New Demodulator: 8 [new_demod,7] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ** KEPT (pick-wt=11): 10 [copy,9,flip.1] k(k(x,y),z)=k(x,k(y,z)). ---> New Demodulator: 11 [new_demod,10] k(k(x,y),z)=k(x,k(y,z)). ** KEPT (pick-wt=5): 12 [] r(r(x))=x. ---> New Demodulator: 13 [new_demod,12] r(r(x))=x. ** KEPT (pick-wt=10): 14 [] r(u(x,y))=u(r(x),r(y)). ---> New Demodulator: 15 [new_demod,14] r(u(x,y))=u(r(x),r(y)). ** KEPT (pick-wt=10): 16 [] r(k(x,y))=k(r(y),r(x)). ---> New Demodulator: 17 [new_demod,16] r(k(x,y))=k(r(y),r(x)). ** KEPT (pick-wt=13): 19 [copy,18,flip.1] u(k(x,y),k(z,y))=k(u(x,z),y). ---> New Demodulator: 20 [new_demod,19] u(k(x,y),k(z,y))=k(u(x,z),y). ** 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. Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] u(x,y)=u(y,x). >>>> Starting back demodulation with 6. >>>> Starting back demodulation with 8. >>>> Starting back demodulation with 11. >>>> Starting back demodulation with 13. >>>> Starting back demodulation with 15. >>>> Starting back demodulation with 17. >>>> Starting back demodulation with 20. >>>> Starting back demodulation with 23. >> back demodulating 7 with 23. >>>> Starting back demodulation with 26. >>>> Starting back demodulation with 29. >>>> Starting back demodulation with 32. >>>> Starting back demodulation with 34. >>>> Starting back demodulation with 36. ======= end of input processing ======= =========== start of search =========== Resetting weight limit to 12. sos_size=7941 ----> UNIT CONFLICT at 78.97 sec ----> 47703 [binary,47702.1,44.1] $F. Length of proof is 554. Level of proof is 71. ---------------- PROOF ---------------- 1 [] n(x,k(y,r(z)))!=Z|n(y,k(x,z))=Z. 2 [] n(k(n(I,$c1),U),k(n(I,c($c1)),U))!=Z. 3 [] u(x,y)=u(y,x). 4 [] u(x,u(y,z))=u(u(x,y),z). 6,5 [copy,4,flip.1] u(u(x,y),z)=u(x,u(y,z)). 7 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 9 [] k(x,k(y,z))=k(k(x,y),z). 11,10 [copy,9,flip.1] k(k(x,y),z)=k(x,k(y,z)). 13,12 [] r(r(x))=x. 15,14 [] r(u(x,y))=u(r(x),r(y)). 17,16 [] r(k(x,y))=k(r(y),r(x)). 18 [] k(u(x,y),z)=u(k(x,z),k(y,z)). 19 [copy,18,flip.1] u(k(x,y),k(z,y))=k(u(x,z),y). 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. 36,35 [back_demod,7,demod,23] u(c(u(c(x),y)),n(x,y))=x. 40 [para_into,5.1.1.1,3.1.1,demod,6] u(x,u(y,z))=u(y,u(x,z)). 41 [para_into,5.1.1,3.1.1] u(x,u(y,z))=u(y,u(z,x)). 42 [copy,41,flip.1] u(x,u(y,z))=u(z,u(x,y)). 44 [para_into,12.1.1,12.1.1] x=x. 46,45 [para_into,28.1.1,3.1.1] u(D,I)=U. 48,47 [para_from,28.1.1,5.1.1.1] u(U,x)=u(I,u(D,x)). 49 [para_into,10.1.1.1,33.1.1,flip.1] k(x,k(I,y))=k(x,y). 51 [para_into,47.1.1,3.1.1] u(x,U)=u(I,u(D,x)). 52 [copy,51,flip.1] u(I,u(D,x))=u(x,U). 60 [para_into,14.1.1.1,45.1.1] r(U)=u(r(D),r(I)). 64 [para_into,52.1.1.2,3.1.1] u(I,u(x,D))=u(x,U). 65 [para_into,52.1.1,3.1.1,demod,6] u(D,u(x,I))=u(x,U). 66 [copy,64,flip.1] u(x,U)=u(I,u(x,D)). 67 [copy,65,flip.1] u(x,U)=u(D,u(x,I)). 70 [para_into,65.1.1.2,5.1.1,demod,6] u(D,u(x,u(y,I)))=u(x,u(y,U)). 71 [para_into,65.1.1.2,3.1.1] u(D,u(I,x))=u(x,U). 72 [copy,70,flip.1] u(x,u(y,U))=u(D,u(x,u(y,I))). 73 [copy,71,flip.1] u(x,U)=u(D,u(I,x)). 74 [para_from,65.1.1,5.1.1.1,demod,6,48,6] u(x,u(I,u(D,y)))=u(D,u(x,u(I,y))). 75 [copy,74,flip.1] u(D,u(x,u(I,y)))=u(x,u(I,u(D,y))). 78 [para_into,16.1.1.1,33.1.1,flip.1] k(r(I),r(x))=r(x). 87,86 [para_into,78.1.1.2,12.1.1,demod,13] k(r(I),x)=x. 89,88 [para_into,86.1.1,49.1.1,demod,87,flip.1] k(I,x)=x. 91,90 [para_into,86.1.1,33.1.1] r(I)=I. 93,92 [back_demod,60,demod,91] r(U)=u(r(D),I). 94 [para_into,19.1.1.1,88.1.1] u(x,k(y,x))=k(u(I,y),x). 95 [para_into,19.1.1.2,88.1.1] u(k(x,y),y)=k(u(x,I),y). 98 [copy,94,flip.1] k(u(I,x),y)=u(y,k(x,y)). 108,107 [para_into,22.1.1.1.1,31.1.1] c(u(Z,c(x)))=n(U,x). 110,109 [para_into,22.1.1.1.1,25.1.1] c(u(D,c(x)))=n(I,x). 112,111 [para_into,22.1.1.1.1,22.1.1] c(u(n(x,y),c(z)))=n(u(c(x),c(y)),z). 113 [para_into,22.1.1.1.2,31.1.1] c(u(c(x),Z))=n(x,U). 116,115 [para_into,22.1.1.1.2,25.1.1] c(u(c(x),D))=n(x,I). 118,117 [para_into,22.1.1.1.2,22.1.1] c(u(c(x),n(y,z)))=n(x,u(c(y),c(z))). 119 [para_into,22.1.1.1,3.1.1,demod,23] n(x,y)=n(y,x). 120 [para_from,119.1.1,2.1.1] n(k(n(I,c($c1)),U),k(n(I,$c1),U))!=Z. 124 [para_into,73.1.1,5.1.1] u(x,u(y,U))=u(D,u(I,u(x,y))). 129 [para_into,107.1.1.1.2,31.1.1] c(u(Z,Z))=n(U,U). 131 [para_into,107.1.1.1.2,25.1.1] c(u(Z,D))=n(U,I). 133 [para_into,107.1.1.1.2,22.1.1] c(u(Z,n(x,y)))=n(U,u(c(x),c(y))). 135 [para_into,35.1.1.1.1.1,31.1.1] u(c(u(Z,x)),n(U,x))=U. 137 [para_into,35.1.1.1.1.1,25.1.1] u(c(u(D,x)),n(I,x))=I. 141 [para_into,35.1.1.1.1,67.1.1] u(c(u(D,u(c(x),I))),n(x,U))=x. 147 [para_into,35.1.1.1.1,3.1.1] u(c(u(x,c(y))),n(y,x))=y. 149 [para_into,35.1.1.1,22.1.1] u(n(x,y),n(x,c(y)))=x. 151 [para_into,35.1.1.2,119.1.1] u(c(u(c(x),y)),n(y,x))=x. 153 [para_into,35.1.1,3.1.1] u(n(x,y),c(u(c(x),y)))=x. 158,157 [para_from,35.1.1,5.1.1.1,flip.1] u(c(u(c(x),y)),u(n(x,y),z))=u(x,z). 160,159 [para_into,131.1.1.1,3.1.1] c(u(D,Z))=n(U,I). 164,163 [para_from,159.1.1,22.1.1.1.1,demod,112,32,26] n(u(Z,D),x)=n(u(D,Z),x). 174,173 [para_into,109.1.1.1.2,25.1.1] c(u(D,D))=n(I,I). 175 [para_into,109.1.1.1.2,22.1.1] c(u(D,n(x,y)))=n(I,u(c(x),c(y))). 177 [para_into,40.1.1.2,73.1.1] u(x,u(D,u(I,y)))=u(y,u(x,U)). 178 [para_into,40.1.1.2,71.1.1] u(x,u(y,U))=u(D,u(x,u(I,y))). 179 [para_into,40.1.1.2,67.1.1] u(x,u(D,u(y,I)))=u(y,u(x,U)). 181 [para_into,40.1.1.2,52.1.1] u(x,u(y,U))=u(I,u(x,u(D,y))). 183 [para_into,40.1.1.2,35.1.1,flip.1] u(c(u(c(x),y)),u(z,n(x,y)))=u(z,x). 187 [copy,178,flip.1] u(D,u(x,u(I,y)))=u(x,u(y,U)). 188 [copy,179,flip.1] u(x,u(y,U))=u(y,u(D,u(x,I))). 206 [para_into,113.1.1.1.1,22.1.1] c(u(n(x,y),Z))=n(u(c(x),c(y)),U). 208 [para_from,113.1.1,35.1.1.1] u(n(x,U),n(x,Z))=x. 224 [para_into,115.1.1.1.1,22.1.1] c(u(n(x,y),D))=n(u(c(x),c(y)),I). 226 [para_from,115.1.1,35.1.1.1] u(n(x,I),n(x,D))=x. 228 [para_into,208.1.1.1,119.1.1] u(n(U,x),n(x,Z))=x. 230 [para_into,208.1.1.2,119.1.1] u(n(x,U),n(Z,x))=x. 232 [para_into,208.1.1,3.1.1] u(n(x,Z),n(x,U))=x. 236 [para_from,208.1.1,5.1.1.1,flip.1] u(n(x,U),u(n(x,Z),y))=u(x,y). 240 [para_into,226.1.1.1,119.1.1] u(n(I,x),n(x,D))=x. 242 [para_into,226.1.1.2,119.1.1] u(n(x,I),n(D,x))=x. 248 [para_from,226.1.1,5.1.1.1,flip.1] u(n(x,I),u(n(x,D),y))=u(x,y). 250 [para_from,226.1.1,40.1.1.2,flip.1] u(n(x,I),u(y,n(x,D)))=u(y,x). 253 [para_into,41.1.1.2,71.1.1,demod,6] u(x,u(y,U))=u(D,u(I,u(y,x))). 261 [para_into,41.1.1.2,3.1.1] u(x,u(y,z))=u(z,u(y,x)). 263 [copy,253,flip.1] u(D,u(I,u(x,y)))=u(y,u(x,U)). 270 [para_from,41.1.1,35.1.1.1.1] u(c(u(x,u(y,c(z)))),n(z,u(x,y)))=z. 272 [para_into,228.1.1.2,119.1.1] u(n(U,x),n(Z,x))=x. 278 [para_from,228.1.1,5.1.1.1,flip.1] u(n(U,x),u(n(x,Z),y))=u(x,y). 281,280 [para_from,228.1.1,40.1.1.2,flip.1] u(n(U,x),u(y,n(x,Z)))=u(y,x). 282 [para_into,230.1.1,3.1.1] u(n(Z,x),n(x,U))=x. 286 [para_from,230.1.1,5.1.1.1,flip.1] u(n(x,U),u(n(Z,x),y))=u(x,y). 289,288 [para_from,230.1.1,40.1.1.2,flip.1] u(n(x,U),u(y,n(Z,x)))=u(y,x). 292 [para_from,232.1.1,5.1.1.1,flip.1] u(n(x,Z),u(n(x,U),y))=u(x,y). 296 [para_into,240.1.1.2,119.1.1] u(n(I,x),n(D,x))=x. 298 [para_into,240.1.1,3.1.1] u(n(x,D),n(I,x))=x. 304 [para_from,240.1.1,40.1.1.2,flip.1] u(n(I,x),u(y,n(x,D)))=u(y,x). 308 [para_into,42.1.1.2,230.1.1,flip.1] u(n(Z,x),u(y,n(x,U)))=u(y,x). 319 [para_into,42.1.1.2,35.1.1,flip.1] u(n(x,y),u(z,c(u(c(x),y))))=u(z,x). 326 [para_from,42.1.1,35.1.1.1.1] u(c(u(x,u(c(y),z))),n(y,u(z,x)))=y. 328 [para_into,242.1.1,3.1.1] u(n(D,x),n(x,I))=x. 332 [para_from,242.1.1,5.1.1.1,flip.1] u(n(x,I),u(n(D,x),y))=u(x,y). 334 [para_from,242.1.1,42.1.1.2,flip.1] u(n(D,x),u(y,n(x,I)))=u(y,x). 336 [para_from,242.1.1,40.1.1.2,flip.1] u(n(x,I),u(y,n(D,x)))=u(y,x). 342 [para_into,272.1.1,3.1.1] u(n(Z,x),n(U,x))=x. 360 [para_into,296.1.1,3.1.1] u(n(D,x),n(I,x))=x. 366 [para_from,296.1.1,42.1.1.2,flip.1] u(n(D,x),u(y,n(I,x)))=u(y,x). 376 [para_from,328.1.1,5.1.1.1,flip.1] u(n(D,x),u(n(x,I),y))=u(x,y). 406 [para_into,135.1.1.1.1,40.1.1] u(c(u(x,u(Z,y))),n(U,u(x,y)))=U. 408 [para_into,135.1.1.1.1,3.1.1] u(c(u(x,Z)),n(U,x))=U. 412 [para_into,135.1.1,3.1.1] u(n(U,x),c(u(Z,x)))=U. 420 [para_from,135.1.1,41.1.1.2] u(x,U)=u(c(u(Z,y)),u(n(U,y),x)). 421 [para_from,135.1.1,40.1.1.2,flip.1] u(c(u(Z,x)),u(y,n(U,x)))=u(y,U). 423 [copy,420,flip.1] u(c(u(Z,x)),u(n(U,x),y))=u(y,U). 431,430 [para_into,137.1.1.1.1,45.1.1,demod,32] u(Z,n(I,I))=I. 432 [para_into,137.1.1.1.1,42.1.1] u(c(u(x,u(D,y))),n(I,u(y,x)))=I. 440 [para_into,137.1.1.2,119.1.1] u(c(u(D,x)),n(x,I))=I. 442 [para_into,137.1.1,3.1.1] u(n(I,x),c(u(D,x)))=I. 465,464 [para_into,430.1.1,3.1.1] u(n(I,I),Z)=I. 466 [para_from,430.1.1,135.1.1.1.1,demod,26] u(D,n(U,n(I,I)))=U. 474 [para_from,430.1.1,5.1.1.1,flip.1] u(Z,u(n(I,I),x))=u(I,x). 476 [para_from,430.1.1,42.1.1.2,flip.1] u(n(I,I),u(x,Z))=u(x,I). 487,486 [para_from,464.1.1,5.1.1.1,flip.1] u(n(I,I),u(Z,x))=u(I,x). 488 [para_into,466.1.1.2,119.1.1] u(D,n(n(I,I),U))=U. 498 [para_from,466.1.1,5.1.1.1,demod,48,flip.1] u(D,u(n(U,n(I,I)),x))=u(I,u(D,x)). 551 [para_into,149.1.1.1,119.1.1] u(n(x,y),n(y,c(x)))=y. 553 [para_into,149.1.1.2.2,173.1.1] u(n(x,u(D,D)),n(x,n(I,I)))=x. 569 [para_into,149.1.1.2,119.1.1] u(n(x,y),n(c(y),x))=x. 572,571 [para_into,149.1.1,3.1.1] u(n(x,c(y)),n(x,y))=x. 575 [para_from,149.1.1,5.1.1.1,flip.1] u(n(x,y),u(n(x,c(y)),z))=u(x,z). 578,577 [para_from,149.1.1,42.1.1.2,flip.1] u(n(x,c(y)),u(z,n(x,y)))=u(z,x). 581 [para_into,408.1.1.2,119.1.1] u(c(u(x,Z)),n(x,U))=U. 583 [para_into,408.1.1,3.1.1] u(n(U,x),c(u(x,Z)))=U. 629 [para_from,412.1.1,41.1.1.2] u(x,U)=u(n(U,y),u(c(u(Z,y)),x)). 630 [copy,629,flip.1] u(n(U,x),u(c(u(Z,x)),y))=u(y,U). 671 [para_into,440.1.1,3.1.1] u(n(x,I),c(u(D,x)))=I. 723 [para_into,551.1.1.2,119.1.1] u(n(x,y),n(c(x),y))=y. 725 [para_into,551.1.1,3.1.1] u(n(x,c(y)),n(y,x))=x. 727 [para_from,551.1.1,14.1.1.1,flip.1] u(r(n(x,y)),r(n(y,c(x))))=r(y). 753 [para_into,569.1.1.2.1,22.1.1] u(n(x,u(c(y),c(z))),n(n(y,z),x))=x. 755 [para_into,569.1.1,3.1.1] u(n(c(x),y),n(y,x))=y. 779 [para_into,571.1.1.1.2,22.1.1] u(n(x,n(y,z)),n(x,u(c(y),c(z))))=x. 785 [para_into,581.1.1,3.1.1] u(n(x,U),c(u(x,Z)))=U. 845 [para_into,671.1.1.2.1,71.1.1] u(n(u(I,x),I),c(u(x,U)))=I. 847 [para_into,671.1.1.2.1,66.1.1] u(n(U,I),c(u(I,u(D,D))))=I. 893 [para_from,723.1.1,14.1.1.1,flip.1] u(r(n(x,y)),r(n(c(x),y)))=r(y). 895 [para_from,723.1.1,5.1.1.1,flip.1] u(n(x,y),u(n(c(x),y),z))=u(y,z). 911 [para_into,725.1.1.1.2,109.1.1] u(n(x,n(I,y)),n(u(D,c(y)),x))=x. 948,947 [para_into,75.1.1,40.1.1,flip.1] u(x,u(I,u(D,y)))=u(x,u(D,u(I,y))). 1002 [para_into,94.1.1.2,88.1.1] u(x,x)=k(u(I,I),x). 1035,1034 [para_into,1002.1.1,73.1.1] u(D,u(I,U))=k(u(I,I),U). 1068 [para_from,1002.1.1,64.1.1.2] u(I,k(u(I,I),D))=u(D,U). 1070 [para_from,1002.1.1,173.1.1.1] c(k(u(I,I),D))=n(I,I). 1073,1072 [para_from,1002.1.1,72.1.1.2,demod,48,46,flip.1] u(D,u(x,u(I,U)))=u(x,k(u(I,I),U)). 1079 [para_from,1002.1.1,14.1.1.1,demod,17,15,91,91,flip.1] u(r(x),r(x))=k(r(x),u(I,I)). 1095 [para_into,95.1.1,3.1.1] u(x,k(y,x))=k(u(y,I),x). 1097 [copy,1095,flip.1] k(u(x,I),y)=u(y,k(x,y)). 1163,1162 [para_from,1070.1.1,22.1.1.1.2,demod,118,26,26,flip.1] n(x,k(u(I,I),D))=n(x,u(D,D)). 1172 [para_from,1070.1.1,113.1.1.1.1,demod,465,26,flip.1] n(k(u(I,I),D),U)=D. 1174 [para_from,1070.1.1,107.1.1.1.2,demod,431,26,1163,flip.1] n(U,u(D,D))=D. 1177,1176 [para_from,1070.1.1,22.1.1.1.1,demod,112,26,26,flip.1] n(k(u(I,I),D),x)=n(u(D,D),x). 1178 [back_demod,1172,demod,1177] n(u(D,D),U)=D. 1181,1180 [para_from,1174.1.1,725.1.1.2,demod,32] u(n(u(D,D),Z),D)=u(D,D). 1286 [para_into,98.1.1.1,28.1.1,flip.1] u(x,k(D,x))=k(U,x). 1346 [para_from,1286.1.1,40.1.1.2] u(x,k(U,y))=u(y,u(x,k(D,y))). 1349 [copy,1346,flip.1] u(x,u(y,k(D,x)))=u(y,k(U,x)). 1355 [para_into,111.1.1.1,785.1.1,demod,32,32,flip.1] n(u(c(x),Z),u(x,Z))=Z. 1357 [para_into,111.1.1.1,671.1.1,demod,26,26,flip.1] n(u(c(x),D),u(D,x))=D. 1367 [para_into,111.1.1.1,412.1.1,demod,32,32,flip.1] n(u(Z,c(x)),u(Z,x))=Z. 1400 [para_into,117.1.1.1,440.1.1,demod,26,26,flip.1] n(u(D,x),u(c(x),D))=D. 1406 [para_into,117.1.1.1,408.1.1,demod,32,32,flip.1] n(u(x,Z),u(Z,c(x)))=Z. 1408 [para_into,117.1.1.1,137.1.1,demod,26,26,flip.1] n(u(D,x),u(D,c(x)))=D. 1410 [para_into,117.1.1.1,135.1.1,demod,32,32,flip.1] n(u(Z,x),u(Z,c(x)))=Z. 1412 [para_into,117.1.1.1,35.1.1,flip.1] n(u(c(x),y),u(c(x),c(y)))=c(x). 1488 [para_into,1355.1.1.1.1,25.1.1] n(u(D,Z),u(I,Z))=Z. 1510 [para_into,1488.1.1,119.1.1] n(u(I,Z),u(D,Z))=Z. 1528 [para_into,120.1.1.1.1,119.1.1] n(k(n(c($c1),I),U),k(n(I,$c1),U))!=Z. 1568 [para_into,1357.1.1.1.1,31.1.1,demod,164] n(u(D,Z),u(D,U))=D. 1599 [para_into,1568.1.1,119.1.1] n(u(D,U),u(D,Z))=D. 1603 [para_from,1568.1.1,571.1.1.2] u(n(u(D,Z),c(u(D,U))),D)=u(D,Z). 1775 [para_into,1367.1.1.1.2,107.1.1] n(u(Z,n(U,x)),u(Z,u(Z,c(x))))=Z. 1791 [para_from,1367.1.1,723.1.1.1,demod,108] u(Z,n(n(U,x),u(Z,x)))=u(Z,x). 1881 [para_into,1400.1.1.1,65.1.1] n(u(x,U),u(c(u(x,I)),D))=D. 1993 [para_into,1406.1.1.2.2,109.1.1,demod,6] n(u(D,u(c(x),Z)),u(Z,n(I,x)))=Z. 2041 [para_into,1410.1.1.2.2,115.1.1] n(u(Z,u(c(x),D)),u(Z,n(x,I)))=Z. 2047 [para_into,1410.1.1.2.2,107.1.1] n(u(Z,u(Z,c(x))),u(Z,n(U,x)))=Z. 2101 [para_into,147.1.1.2,119.1.1] u(c(u(x,c(y))),n(x,y))=y. 2103 [para_into,147.1.1,3.1.1] u(n(x,y),c(u(y,c(x))))=x. 2105 [para_from,147.1.1,117.1.1.1,flip.1] n(u(x,c(y)),u(c(y),c(x)))=c(y). 2117 [para_into,151.1.1.1.1,67.1.1] u(c(u(D,u(c(x),I))),n(U,x))=x. 2129 [para_into,151.1.1,3.1.1] u(n(x,y),c(u(c(y),x)))=y. 2173 [para_into,153.1.1.2.1,67.1.1] u(n(x,U),c(u(D,u(c(x),I))))=x. 2271 [para_from,261.1.1,1367.1.1.2] n(u(Z,c(u(x,y))),u(y,u(x,Z)))=Z. 2312,2311 [para_into,474.1.1.2,723.1.1,demod,26] u(Z,I)=u(I,n(D,I)). 2313 [para_into,474.1.1.2,671.1.1,demod,2312,46,32] u(I,n(D,I))=u(I,Z). 2349 [para_into,2313.1.1,3.1.1] u(n(D,I),I)=u(I,Z). 2523 [para_into,157.1.1.2,2349.1.1,demod,46] u(c(u(c(D),I)),u(I,Z))=U. 2533,2532 [para_into,157.1.1.2,725.1.1,demod,23] u(n(x,y),x)=u(x,n(y,x)). 2535,2534 [para_into,157.1.1.2,723.1.1] u(c(u(c(x),y)),y)=u(x,n(c(x),y)). 2542 [para_into,157.1.1.2,571.1.1,demod,23,2533] u(x,n(y,x))=u(x,n(x,y)). 2544,2543 [para_into,157.1.1.2,569.1.1] u(c(u(c(x),y)),x)=u(x,n(c(y),x)). 2545 [para_into,157.1.1.2,551.1.1,demod,2535] u(x,n(c(x),y))=u(x,n(y,c(x))). 2547,2546 [para_into,157.1.1.2,360.1.1,demod,2535] u(D,n(c(D),x))=u(D,n(I,x)). 2549,2548 [para_into,157.1.1.2,342.1.1,demod,2535] u(Z,n(c(Z),x))=u(Z,n(U,x)). 2550 [para_into,157.1.1.2,328.1.1,demod,2535,2547] u(D,n(I,x))=u(D,n(x,I)). 2552,2551 [para_into,157.1.1.2,296.1.1,demod,26] u(c(u(D,x)),x)=u(I,n(D,x)). 2553 [para_into,157.1.1.2,282.1.1,demod,2535,2549] u(Z,n(U,x))=u(Z,n(x,U)). 2556 [para_into,157.1.1.2,240.1.1,demod,26,2552] u(I,n(D,x))=u(I,n(x,D)). 2572 [copy,2545,flip.1] u(x,n(y,c(x)))=u(x,n(c(x),y)). 2802,2801 [para_into,181.1.1,124.1.1,flip.1] u(I,u(x,u(D,y)))=u(D,u(I,u(x,y))). 2836,2835 [para_into,183.1.1.2,725.1.1,demod,2535,flip.1] u(n(x,c(y)),y)=u(y,n(c(y),x)). 2849,2848 [para_into,183.1.1.2,298.1.1,demod,26,2552,flip.1] u(n(x,D),I)=u(I,n(D,x)). 2853,2852 [para_into,183.1.1.2,242.1.1,demod,2535,2547,flip.1] u(n(x,I),D)=u(D,n(I,x)). 2855,2854 [para_into,183.1.1.2,230.1.1,demod,2535,2549,flip.1] u(n(x,U),Z)=u(Z,n(U,x)). 2863 [para_into,183.1.1.2,141.1.1,demod,2544,32,flip.1] u(c(u(D,u(c(x),I))),x)=u(x,n(Z,x)). 2910 [para_into,2101.1.1,3.1.1] u(n(x,y),c(u(x,c(y))))=y. 2968 [para_into,2129.1.1.2.1,67.1.1] u(n(U,x),c(u(D,u(c(x),I))))=x. 2981,2980 [para_from,2129.1.1,157.1.1.2,demod,2535,flip.1] u(x,c(u(c(y),x)))=u(x,n(c(x),y)). 3025 [para_into,2523.1.1.1.1,3.1.1] u(c(u(I,c(D))),u(I,Z))=U. 3029 [para_into,2523.1.1,261.1.1,demod,2981,26] u(Z,u(I,n(D,D)))=U. 3037 [para_from,2523.1.1,187.1.1.2,flip.1] u(c(u(c(D),I)),u(Z,U))=u(D,U). 3053 [para_into,3029.1.1,261.1.1] u(n(D,D),u(I,Z))=U. 3119 [para_from,3053.1.1,187.1.1.2,flip.1] u(n(D,D),u(Z,U))=u(D,U). 3191 [para_from,2532.1.1,476.1.1.2,demod,487,flip.1] u(n(Z,x),I)=u(I,n(x,Z)). 3203,3202 [para_from,2532.1.1,183.1.1.2,demod,158,flip.1] u(n(n(x,y),z),x)=u(x,n(z,n(x,y))). 3204 [para_from,2532.1.1,1097.1.1.1] k(u(I,n(x,I)),y)=u(y,k(n(I,x),y)). 3206,3205 [para_from,2532.1.1,65.1.1.2,flip.1] u(n(I,x),U)=u(D,u(I,n(x,I))). 3223 [para_from,2532.1.1,64.1.1.2,flip.1] u(n(D,x),U)=u(I,u(D,n(x,D))). 3226 [para_from,2532.1.1,14.1.1.1,demod,15] u(r(x),r(n(y,x)))=u(r(n(x,y)),r(x)). 3230 [para_from,2532.1.1,42.1.1.2] u(x,u(y,n(z,y)))=u(y,u(x,n(y,z))). 3232 [para_from,2532.1.1,40.1.1.2] u(x,u(y,n(z,y)))=u(n(y,z),u(x,y)). 3234 [copy,3204,flip.1] u(x,k(n(I,y),x))=k(u(I,n(y,I)),x). 3238 [copy,3226,flip.1] u(r(n(x,y)),r(x))=u(r(x),r(n(y,x))). 3242 [copy,3230,flip.1] u(x,u(y,n(x,z)))=u(y,u(x,n(z,x))). 3244 [copy,3232,flip.1] u(n(x,y),u(z,x))=u(z,u(x,n(y,x))). 3246,3245 [para_into,2542.1.1,3.1.1] u(n(x,y),y)=u(y,n(y,x)). 3270,3269 [para_from,2542.1.1,71.1.1.2,flip.1] u(n(x,I),U)=u(D,u(I,n(I,x))). 3288,3287 [para_from,2542.1.1,52.1.1.2,flip.1] u(n(x,D),U)=u(I,u(D,n(D,x))). 3292 [para_from,2542.1.1,42.1.1.2] u(x,u(y,n(y,z)))=u(n(z,y),u(x,y)). 3294 [para_from,2542.1.1,40.1.1.2] u(x,u(y,n(y,z)))=u(y,u(x,n(z,y))). 3302 [copy,3292,flip.1] u(n(x,y),u(z,y))=u(z,u(y,n(y,x))). 3304 [copy,3294,flip.1] u(x,u(y,n(z,x)))=u(y,u(x,n(x,z))). 3306,3305 [para_into,2550.1.1,3.1.1] u(n(I,x),D)=u(D,n(x,I)). 3334,3333 [para_into,2553.1.1,3.1.1] u(n(U,x),Z)=u(Z,n(x,U)). 3392,3391 [para_into,2556.1.1,3.1.1] u(n(D,x),I)=u(I,n(x,D)). 3507 [para_into,236.1.1.2,296.1.1,demod,2855] u(Z,n(U,I))=u(I,n(D,Z)). 3557 [para_from,3025.1.1,187.1.1.2,flip.1] u(c(u(I,c(D))),u(Z,U))=u(D,U). 3559 [para_from,3025.1.1,153.1.1.2.1,demod,32] u(n(u(I,c(D)),u(I,Z)),Z)=u(I,c(D)). 3653,3652 [para_from,3191.1.1,65.1.1.2,flip.1] u(n(Z,x),U)=u(D,u(I,n(x,Z))). 3672,3671 [para_into,3245.1.1,73.1.1,demod,48,flip.1] u(I,u(D,n(U,x)))=u(D,u(I,n(x,U))). 3684,3683 [para_from,3245.1.1,183.1.1.2,demod,158,flip.1] u(n(x,n(y,z)),y)=u(y,n(n(y,z),x)). 3717 [para_into,248.1.1.2,296.1.1,demod,2853,flip.1] u(I,n(D,D))=u(D,n(I,I)). 3720,3719 [para_into,248.1.1.2,282.1.1,demod,2853,flip.1] u(Z,n(D,U))=u(D,n(I,Z)). 3723 [para_into,248.1.1.2,228.1.1,demod,2853,48,flip.1] u(I,u(D,n(D,Z)))=u(D,n(I,U)). 3784,3783 [para_from,3333.1.1,248.1.1.2,demod,3720,281,46,48,flip.1] u(I,u(D,Z))=U. 3786,3785 [para_from,3333.1.1,236.1.1.2,demod,289,48,3784] u(Z,U)=U. 3798 [back_demod,3557,demod,3786] u(c(u(I,c(D))),U)=u(D,U). 3801,3800 [back_demod,3119,demod,3786,3288] u(I,u(D,n(D,D)))=u(D,U). 3802 [back_demod,3037,demod,3786] u(c(u(c(D),I)),U)=u(D,U). 3819 [para_into,3785.1.1,73.1.1] u(D,u(I,Z))=U. 3823 [para_into,3785.1.1,66.1.1] u(I,u(Z,D))=U. 3830,3829 [para_from,3785.1.1,486.1.1.2,demod,3270] u(D,u(I,n(I,I)))=u(I,U). 3894 [para_from,3819.1.1,1408.1.1.1] n(U,u(D,c(u(I,Z))))=D. 3896 [para_from,3819.1.1,1400.1.1.1] n(U,u(c(u(I,Z)),D))=D. 3902 [para_from,3819.1.1,671.1.1.2.1,demod,32] u(n(u(I,Z),I),Z)=I. 3904 [para_from,3819.1.1,442.1.1.2.1,demod,32] u(n(I,u(I,Z)),Z)=I. 3912 [para_from,3819.1.1,5.1.1.1,demod,48,6,flip.1] u(D,u(I,u(Z,x)))=u(I,u(D,x)). 4087,4086 [para_from,3902.1.1,476.1.1.2,demod,2533,3246,flip.1] u(I,n(I,u(I,Z)))=u(I,n(I,I)). 4115,4114 [para_from,3904.1.1,476.1.1.2,demod,2533,2533,flip.1] u(I,n(u(I,Z),I))=u(I,n(I,I)). 4294 [para_from,3894.1.1,151.1.1.2,demod,110,3206,4115,3830,flip.1] u(D,c(u(I,Z)))=u(c(u(I,U)),D). 4327,4326 [para_from,3896.1.1,151.1.1.2,demod,116,3270,4087,3830,flip.1] u(c(u(I,Z)),D)=u(c(u(I,U)),D). 4423,4422 [para_into,278.1.1.2,296.1.1,demod,3334] u(Z,n(I,U))=u(I,n(D,Z)). 4486 [para_from,3507.1.1,486.1.1.2] u(n(I,I),u(I,n(D,Z)))=u(I,n(U,I)). 4509,4508 [para_into,280.1.1,248.1.1,demod,48,2849] u(I,u(D,n(I,Z)))=u(I,n(D,U)). 4557 [para_from,3717.1.1,71.1.1.2,demod,3288,3801] u(D,u(D,n(I,I)))=u(D,U). 4572 [para_from,3719.1.1,183.1.1.2] u(c(u(c(D),U)),u(D,n(I,Z)))=u(Z,D). 4693,4692 [para_into,3829.1.1,41.1.1,demod,2853] u(I,u(D,n(I,I)))=u(I,U). 5285,5284 [para_into,308.1.1.2,488.1.1,demod,3653] u(D,u(I,n(n(I,I),Z)))=u(D,n(I,I)). 5581 [para_into,319.1.1.2,2910.1.1,demod,2836] u(x,n(c(x),y))=u(n(c(y),x),y). 5582 [copy,5581,flip.1] u(n(c(x),y),x)=u(y,n(c(y),x)). 5761 [para_from,4422.1.1,42.1.1.2] u(x,u(I,n(D,Z)))=u(n(I,U),u(x,Z)). 5763 [copy,5761,flip.1] u(n(I,U),u(x,Z))=u(x,u(I,n(D,Z))). 5801 [para_into,326.1.1.2,1510.1.1,demod,4327] u(c(u(Z,u(c(u(I,U)),D))),Z)=u(I,Z). 5930 [para_into,332.1.1,188.1.1,demod,3246] u(n(D,x),u(D,u(I,n(I,x))))=u(x,U). 5989 [para_from,334.1.1,292.1.1.2] u(n(D,Z),u(x,U))=u(D,u(x,n(U,I))). 6072 [para_from,336.1.1,286.1.1.2] u(n(I,U),u(x,Z))=u(I,u(x,n(D,Z))). 6074 [copy,6072,flip.1] u(I,u(x,n(D,Z)))=u(n(I,U),u(x,Z)). 6699 [para_into,1079.1.1.1,12.1.1,demod,13,13] u(x,x)=k(x,u(I,I)). 6701,6700 [para_into,1079.1.1,1002.1.1,flip.1] k(r(x),u(I,I))=k(u(I,I),r(x)). 6703 [para_into,6699.1.1,1002.1.1] k(u(I,I),x)=k(x,u(I,I)). 6789 [para_from,6699.1.1,129.1.1.1] c(k(Z,u(I,I)))=n(U,U). 6816,6815 [para_from,6699.1.1,64.1.1.2] u(I,k(D,u(I,I)))=u(D,U). 6841 [para_from,6699.1.1,1178.1.1.1] n(k(D,u(I,I)),U)=D. 6846,6845 [para_from,6699.1.1,173.1.1.1] c(k(D,u(I,I)))=n(I,I). 6848,6847 [para_from,6699.1.1,178.1.1.2,demod,1073,flip.1] u(x,k(u(I,I),U))=u(x,k(U,u(I,I))). 6851 [para_from,6699.1.1,22.1.1.1] c(k(c(x),u(I,I)))=n(x,x). 6857,6856 [para_from,6699.1.1,5.1.1.1] u(k(x,u(I,I)),y)=u(x,u(x,y)). 6874,6873 [para_from,6841.1.1,147.1.1.2,demod,6846,48,4693] u(c(u(I,U)),D)=k(D,u(I,I)). 6875 [para_from,6841.1.1,2103.1.1.1,demod,6846,48,4693] u(D,c(u(I,U)))=k(D,u(I,I)). 6878,6877 [para_from,6841.1.1,157.1.1.2.1,demod,6846,3270,3830,6857] u(c(u(I,U)),u(D,x))=u(D,u(D,x)). 6881 [back_demod,5801,demod,6874] u(c(u(Z,k(D,u(I,I)))),Z)=u(I,Z). 6890,6889 [back_demod,4294,demod,6874] u(D,c(u(I,Z)))=k(D,u(I,I)). 6946,6945 [para_into,376.1.1.2,583.1.1,demod,3246,48,3672,48,6890,6816] u(D,u(I,n(D,U)))=u(D,U). 6979 [para_from,6845.1.1,22.1.1.1.1,demod,112,26,26,flip.1] n(k(D,u(I,I)),x)=n(u(D,D),x). 7015 [para_from,6703.1.1,1095.1.1.2,demod,6] u(x,k(x,u(I,I)))=k(u(I,u(I,I)),x). 7017 [copy,7015,flip.1] k(u(I,u(I,I)),x)=u(x,k(x,u(I,I))). 7667 [para_from,2546.1.1,334.1.1.2] u(n(D,c(D)),u(D,n(I,I)))=u(D,c(D)). 7676,7675 [para_from,2546.1.1,304.1.1.2,demod,578,46,flip.1] u(D,c(D))=U. 7709 [back_demod,7667,demod,7676] u(n(D,c(D)),u(D,n(I,I)))=U. 7714,7713 [para_into,7675.1.1,3.1.1] u(c(D),D)=U. 7723 [para_from,7675.1.1,109.1.1.1,demod,32,flip.1] n(I,D)=Z. 7761 [para_from,7675.1.1,440.1.1.1.1,demod,32] u(Z,n(c(D),I))=I. 7766,7765 [para_from,7675.1.1,52.1.1.2,flip.1] u(c(D),U)=u(I,U). 7777 [para_from,7675.1.1,263.1.1.2.2,demod,1035,flip.1] u(c(D),u(D,U))=k(u(I,I),U). 7790,7789 [para_from,7675.1.1,40.1.1.2,flip.1] u(D,u(x,c(D)))=u(x,U). 7792,7791 [back_demod,4572,demod,7766,6878,flip.1] u(Z,D)=u(D,u(D,n(I,Z))). 7800,7799 [back_demod,3823,demod,7792,2802,4509,6946] u(D,U)=U. 7818,7817 [back_demod,7777,demod,7800,7766] u(I,U)=k(u(I,I),U). 7926,7925 [back_demod,4557,demod,7800] u(D,u(D,n(I,I)))=U. 7927 [back_demod,3802,demod,7800] u(c(u(c(D),I)),U)=U. 7931 [back_demod,3798,demod,7800] u(c(u(I,c(D))),U)=U. 7951 [back_demod,1603,demod,7800,32] u(n(u(D,Z),Z),D)=u(D,Z). 7955 [back_demod,1599,demod,7800] n(U,u(D,Z))=D. 7959 [back_demod,1068,demod,7800] u(I,k(u(I,I),D))=U. 7963 [back_demod,7765,demod,7818] u(c(D),U)=k(u(I,I),U). 7974,7973 [back_demod,6875,demod,7818] u(D,c(k(u(I,I),U)))=k(D,u(I,I)). 7975 [back_demod,6873,demod,7818] u(c(k(u(I,I),U)),D)=k(D,u(I,I)). 8100,8099 [back_demod,3829,demod,7818] u(D,u(I,n(I,I)))=k(u(I,I),U). 8106,8105 [back_demod,1034,demod,7818,6848] u(D,k(U,u(I,I)))=k(u(I,I),U). 8118,8117 [para_into,498.1.1.2,2103.1.1,demod,7800,32,465,26,flip.1] u(I,u(D,D))=U. 8121 [para_into,498.1.1.2,551.1.1,demod,32,flip.1] u(I,u(D,n(n(I,I),Z)))=u(D,n(I,I)). 8142,8141 [back_demod,847,demod,8118,32,3334,4423] u(I,n(D,Z))=I. 8166,8165 [back_demod,5763,demod,8142] u(n(I,U),u(x,Z))=u(x,I). 8180,8179 [back_demod,4486,demod,8142,2533,flip.1] u(I,n(U,I))=u(I,n(I,I)). 8220,8219 [back_demod,6074,demod,8166] u(I,u(x,n(D,Z)))=u(x,I). 8223 [back_demod,3723,demod,8220,46,flip.1] u(D,n(I,U))=U. 8239 [para_into,7723.1.1,119.1.1] n(D,I)=Z. 8241 [para_from,7723.1.1,151.1.1.2] u(c(u(c(D),I)),Z)=D. 8257 [para_from,7723.1.1,2910.1.1.1] u(Z,c(u(I,c(D))))=D. 8265 [para_from,7799.1.1,1881.1.1.1,demod,46,32] n(U,u(Z,D))=D. 8282,8281 [para_from,7799.1.1,5.1.1.1,demod,48,48,948] u(I,u(D,x))=u(D,u(D,u(I,x))). 8295,8294 [back_demod,8121,demod,8282,5285,7926,flip.1] u(D,n(I,I))=U. 8327 [back_demod,3912,demod,8282] u(D,u(I,u(Z,x)))=u(D,u(D,u(I,x))). 8336,8335 [back_demod,3223,demod,8282] u(n(D,x),U)=u(D,u(D,u(I,n(x,D)))). 8352,8351 [back_demod,47,demod,8282] u(U,x)=u(D,u(D,u(I,x))). 8353 [back_demod,7709,demod,8295,8336] u(D,u(D,u(I,n(c(D),D))))=U. 8393 [para_from,8239.1.1,224.1.1.1.1,demod,26,7714] c(u(Z,D))=n(U,I). 8508,8507 [para_from,7955.1.1,2910.1.1.1,demod,160,8352,8180,8100,6848,8106,7974] k(D,u(I,I))=u(D,Z). 8519 [back_demod,7975,demod,8508] u(c(k(u(I,I),U)),D)=u(D,Z). 8548,8547 [back_demod,6979,demod,8508] n(u(D,Z),x)=n(u(D,D),x). 8555 [back_demod,6881,demod,8508] u(c(u(Z,u(D,Z))),Z)=u(I,Z). 8558,8557 [back_demod,6845,demod,8508,160] n(U,I)=n(I,I). 8579,8578 [back_demod,7951,demod,8548,1181,flip.1] u(D,Z)=u(D,D). 8683,8682 [back_demod,8393,demod,8558] c(u(Z,D))=n(I,I). 8687 [back_demod,5989,demod,8558] u(n(D,Z),u(x,U))=u(D,u(x,n(I,I))). 8782,8781 [back_demod,8555,demod,8579] u(c(u(Z,u(D,D))),Z)=u(I,Z). 8896,8895 [back_demod,8519,demod,8579] u(c(k(u(I,I),U)),D)=u(D,D). 8991,8990 [para_from,8141.1.1,177.1.1.2.2,demod,46,flip.1] u(n(D,Z),u(x,U))=u(x,U). 8998,8997 [back_demod,8687,demod,8991,flip.1] u(D,u(x,n(I,I)))=u(x,U). 9023,9022 [para_from,8223.1.1,175.1.1.1,demod,32,26,32,8579,flip.1] n(I,u(D,D))=Z. 9077,9076 [para_from,8265.1.1,151.1.1.2,demod,8683,3270,8998,7818,8896,flip.1] u(Z,D)=u(D,D). 9081,9080 [para_from,8265.1.1,206.1.1.1.1,demod,8579,174,32,9077,174,431,flip.1] n(I,U)=n(I,I). 9287,9286 [para_from,8578.1.1,432.1.1.2.2,demod,9023,8782] u(I,Z)=I. 9343,9342 [back_demod,3559,demod,9287] u(n(u(I,c(D)),I),Z)=u(I,c(D)). 9361,9360 [para_from,9286.1.1,476.1.1.2,demod,2533] u(I,n(I,I))=u(I,I). 9372 [para_from,9286.1.1,14.1.1.1,demod,91,91,flip.1] u(I,r(Z))=I. 9375,9374 [para_from,9286.1.1,5.1.1.1,flip.1] u(I,u(Z,x))=u(I,x). 9408,9407 [back_demod,8327,demod,9375,flip.1] u(D,u(D,u(I,x)))=u(D,u(I,x)). 9436 [back_demod,8353,demod,9408] u(D,u(I,n(c(D),D)))=U. 9438 [back_demod,8351,demod,9408] u(U,x)=u(D,u(I,x)). 9445,9444 [back_demod,8335,demod,9408] u(n(D,x),U)=u(D,u(I,n(x,D))). 9491 [para_from,9372.1.1,98.1.1.1,demod,89,flip.1] u(x,k(r(Z),x))=x. 9957,9956 [para_from,7761.1.1,334.1.1.2,demod,3392,flip.1] u(Z,c(D))=u(I,n(c(D),D)). 10128 [para_from,9491.1.1,263.1.1.2.2,flip.1] u(k(r(Z),x),u(x,U))=u(D,u(I,x)). 10235,10234 [para_from,553.1.1,366.1.1.2,demod,3684,9023,431] u(I,n(n(I,I),D))=I. 10381 [para_from,7927.1.1,2129.1.1.2.1,demod,32,3334] u(Z,n(u(c(D),I),U))=u(c(D),I). 10402 [para_from,7931.1.1,153.1.1.2.1,demod,32,2855] u(Z,n(U,u(I,c(D))))=u(I,c(D)). 10410,10409 [para_from,7959.1.1,14.1.1.1,demod,93,91,17,15,91,91,6701] u(r(D),I)=u(I,k(u(I,I),r(D))). 10423 [back_demod,92,demod,10410] r(U)=u(I,k(u(I,I),r(D))). 10476,10475 [para_from,8241.1.1,113.1.1.1,flip.1] n(u(c(D),I),U)=c(D). 10487,10486 [back_demod,10381,demod,10476,9957,flip.1] u(c(D),I)=u(I,n(c(D),D)). 10490 [back_demod,10475,demod,10487] n(u(I,n(c(D),D)),U)=c(D). 10573,10572 [para_from,8257.1.1,107.1.1.1,flip.1] n(U,u(I,c(D)))=c(D). 10581 [para_from,8257.1.1,42.1.1.2,flip.1] u(c(u(I,c(D))),u(x,Z))=u(x,D). 10583 [para_from,8257.1.1,40.1.1.2,flip.1] u(Z,u(x,c(u(I,c(D)))))=u(x,D). 10586,10585 [back_demod,10402,demod,10573,9957] u(I,n(c(D),D))=u(I,c(D)). 10596 [back_demod,10490,demod,10586] n(u(I,c(D)),U)=c(D). 10609,10608 [back_demod,9436,demod,10586,7790,7818] k(u(I,I),U)=U. 10674 [back_demod,7963,demod,10609] u(c(D),U)=U. 10773,10772 [para_from,10674.1.1,845.1.1.2.1,demod,32,9343] u(I,c(D))=I. 10781 [para_from,10674.1.1,124.1.1.2,flip.1] u(D,u(I,u(x,c(D))))=u(x,U). 10802,10801 [back_demod,10596,demod,10773,9081,flip.1] c(D)=n(I,I). 10812,10811 [back_demod,10585,demod,10802,10235,10802,9361,flip.1] u(I,I)=I. 10814,10813 [back_demod,10583,demod,10802,9361,10812,26] u(Z,u(x,D))=u(x,D). 10816,10815 [back_demod,10581,demod,10802,9361,10812,26] u(D,u(x,Z))=u(x,D). 10830 [back_demod,10781,demod,10802] u(D,u(I,u(x,n(I,I))))=u(x,U). 11026,11025 [back_demod,10423,demod,10812,89] r(U)=u(I,r(D)). 11066,11065 [back_demod,7017,demod,10812,10812,89,10812,34,flip.1] u(x,x)=x. 11097,11096 [back_demod,6856,demod,11066,34,flip.1] u(x,u(x,y))=u(x,y). 11098 [back_demod,6851,demod,11066,34] c(c(x))=n(x,x). 11100 [back_demod,6789,demod,11066,34] c(Z)=n(U,U). 11104 [back_demod,2041,demod,10814] n(u(c(x),D),u(Z,n(x,I)))=Z. 11122 [back_demod,1993,demod,10816] n(u(c(x),D),u(Z,n(I,x)))=Z. 11252 [back_demod,2047,demod,11097] n(u(Z,c(x)),u(Z,n(U,x)))=Z. 11254 [back_demod,1775,demod,11097] n(u(Z,n(U,x)),u(Z,c(x)))=Z. 11348 [para_into,575.1.1.2,723.1.1] u(n(x,y),c(y))=u(x,n(c(x),c(y))). 11357 [copy,11348,flip.1] u(x,n(c(x),c(y)))=u(n(x,y),c(y)). 11376 [para_from,11065.1.1,406.1.1.1.1,demod,6,11066] u(c(u(Z,x)),n(U,u(Z,x)))=U. 11409,11408 [para_from,11065.1.1,183.1.1.2,demod,36,2533,flip.1] u(x,n(y,x))=x. 11413,11412 [para_from,11065.1.1,157.1.1.2,demod,36,flip.1] u(x,n(x,y))=x. 11436 [back_demod,5930,demod,11413,46,9445] u(D,u(I,n(x,D)))=u(x,U). 11460 [back_demod,3234,demod,11409,89] u(x,k(n(I,y),x))=x. 11466 [back_demod,2863,demod,11409] u(c(u(D,u(c(x),I))),x)=x. 11471,11470 [back_demod,3244,demod,11409] u(n(x,y),u(z,x))=u(z,x). 11474,11473 [back_demod,3242,demod,11409] u(x,u(y,n(x,z)))=u(y,x). 11494 [back_demod,2532,demod,11409] u(n(x,y),x)=x. 11497,11496 [back_demod,3304,demod,11413] u(x,u(y,n(z,x)))=u(y,x). 11499 [back_demod,3302,demod,11413] u(n(x,y),u(z,y))=u(z,y). 11521,11520 [back_demod,3245,demod,11413] u(n(x,y),y)=y. 11523,11522 [copy,11436,flip.1,demod,11497,29] u(x,U)=U. 11529,11528 [back_demod,10830,demod,11474,11523] u(D,u(x,I))=U. 11577,11576 [back_demod,10128,demod,11523,11523,flip.1] u(D,u(I,x))=U. 11782 [back_demod,630,demod,11523] u(n(U,x),u(c(u(Z,x)),y))=U. 11800 [back_demod,423,demod,11523] u(c(u(Z,x)),u(n(U,x),y))=U. 11802 [back_demod,421,demod,11523] u(c(u(Z,x)),u(y,n(U,x)))=U. 11817,11816 [back_demod,11466,demod,11529,32] u(Z,x)=x. 11819,11818 [back_demod,2968,demod,11529,32,3334,11817] n(x,U)=x. 11823,11822 [back_demod,2173,demod,11819,11529,32] u(x,Z)=x. 11825,11824 [back_demod,2117,demod,11529,32,11817] n(U,x)=x. 11833,11832 [back_demod,9438,demod,11577] u(U,x)=U. 11872 [back_demod,11802,demod,11817,11825] u(c(x),u(y,x))=U. 11874 [back_demod,11800,demod,11817,11825] u(c(x),u(x,y))=U. 11880 [back_demod,11782,demod,11825,11817] u(x,u(c(x),y))=U. 11898 [back_demod,11376,demod,11817,11817,11825] u(c(x),x)=U. 11905,11904 [back_demod,11254,demod,11825,11817,11817] n(x,c(x))=Z. 11907,11906 [back_demod,11252,demod,11817,11825,11817] n(c(x),x)=Z. 11910 [back_demod,11122,demod,11817] n(u(c(x),D),n(I,x))=Z. 11914 [back_demod,11104,demod,11817] n(u(c(x),D),n(x,I))=Z. 11960 [back_demod,2271,demod,11817,11823] n(c(u(x,y)),u(y,x))=Z. 11977,11976 [back_demod,1791,demod,11825,11817,11817,11817] n(x,x)=x. 11987,11986 [back_demod,133,demod,11817,11825] c(n(x,y))=u(c(x),c(y)). 11997,11996 [back_demod,11100,demod,11977] c(Z)=U. 12061,12060 [back_demod,10801,demod,11977] c(D)=I. 12075,12074 [back_demod,11098,demod,11977] c(c(x))=x. 12089,12088 [para_from,11996.1.1,2129.1.1.2.1.1,demod,11833,32,11823] n(x,Z)=Z. 12159,12158 [para_into,11816.1.1,9491.1.1,flip.1] k(r(Z),Z)=Z. 12168 [para_from,11818.1.1,117.1.1.1.2,demod,32,11823] c(u(c(x),y))=n(x,c(y)). 12171,12170 [para_from,11818.1.1,224.1.1.1.1,demod,32,11823] c(u(x,D))=n(c(x),I). 12172 [para_from,11818.1.1,175.1.1.1.2,demod,32,11823] c(u(D,x))=n(I,c(x)). 12175,12174 [para_from,11818.1.1,111.1.1.1.1,demod,32,11823] c(u(x,c(y)))=n(c(x),y). 12216,12215 [para_into,11832.1.1,1286.1.1] k(U,U)=U. 12246,12245 [para_from,11898.1.1,270.1.1.1.1.2,demod,11523,32,12075,11817] n(x,u(y,x))=x. 12253 [para_from,11898.1.1,14.1.1.1,demod,11026,flip.1] u(r(c(x)),r(x))=u(I,r(D)). 12267 [hyper,11906,1] n(x,k(c(k(x,r(y))),y))=Z. 12275,12274 [para_from,12158.1.1,16.1.1.1,demod,13,12159] r(Z)=Z. 12292,12291 [para_from,11408.1.1,304.1.1.2,demod,3306] u(D,n(x,I))=u(D,x). 12294,12293 [para_from,11408.1.1,250.1.1.2,demod,2853] u(D,n(I,x))=u(D,x). 12302,12301 [para_from,11408.1.1,577.1.1.2,demod,2836] u(x,n(c(x),y))=u(x,y). 12316,12315 [para_from,11408.1.1,14.1.1.1,flip.1] u(r(x),r(n(y,x)))=r(x). 12372 [back_demod,3305,demod,12292] u(n(I,x),D)=u(D,x). 12387,12386 [back_demod,2852,demod,12294] u(n(x,I),D)=u(D,x). 12391,12390 [back_demod,11357,demod,12302,flip.1] u(n(x,y),c(y))=u(x,c(y)). 12392 [back_demod,5582,demod,12302] u(n(c(x),y),x)=u(y,x). 12396 [back_demod,2572,demod,12302] u(x,n(y,c(x)))=u(x,y). 12400 [back_demod,3238,demod,12316] u(r(n(x,y)),r(x))=r(x). 12455,12454 [para_from,11494.1.1,577.1.1.2,demod,572,3203,flip.1] u(x,n(y,n(x,z)))=x. 12458 [back_demod,3202,demod,12455] u(n(n(x,y),z),x)=x. 12640 [para_into,12245.1.1,119.1.1] n(u(x,y),y)=y. 12735,12734 [para_into,12640.1.1.1,11412.1.1] n(x,n(x,y))=n(x,y). 12737,12736 [para_into,12640.1.1.1,11408.1.1] n(x,n(y,x))=n(y,x). 13076 [para_from,727.1.1,11874.1.1.2] u(c(r(n(x,y))),r(y))=U. 13201 [para_from,11460.1.1,12245.1.1.2] n(k(n(I,x),y),y)=k(n(I,x),y). 13349 [para_into,12172.1.1.1,11460.1.1,demod,12061,flip.1] n(I,c(k(n(I,x),D)))=I. 13514 [para_into,753.1.1.1.2,3.1.1] u(n(x,u(c(y),c(z))),n(n(z,y),x))=x. 14037,14036 [para_from,11960.1.1,779.1.1.2,demod,12175,12075,11823,12175,12075] n(n(x,y),n(y,x))=n(x,y). 14233 [para_into,893.1.1.1.1,11910.1.1,demod,12275,12171,12075,14037,11817] r(n(x,I))=r(n(I,x)). 14234 [copy,14233,flip.1] r(n(I,x))=r(n(x,I)). 14243,14242 [para_into,12168.1.1.1.1,12074.1.1] c(u(x,y))=n(c(x),c(y)). 14244 [para_into,12168.1.1.1.1,11986.1.1,demod,6,14243,12075,14243,12075,flip.1] n(n(x,y),c(z))=n(x,n(y,c(z))). 14258 [para_into,12168.1.1.1,11880.1.1,demod,32,12075,14243,flip.1] n(x,n(c(x),c(y)))=Z. 14533,14532 [para_into,14258.1.1.2.2,12074.1.1] n(x,n(c(x),y))=Z. 14622 [para_into,12315.1.1.1,90.1.1,demod,91] u(I,r(n(x,I)))=I. 14624 [para_into,12315.1.1.1,12.1.1,demod,13] u(x,r(n(y,r(x))))=x. 14649,14648 [para_from,14622.1.1,12245.1.1.2] n(r(n(x,I)),I)=r(n(x,I)). 14652 [para_from,14622.1.1,98.1.1.1,demod,89,flip.1] u(x,k(r(n(y,I)),x))=x. 14718 [para_from,14624.1.1,11872.1.1.2] u(c(r(n(x,r(y)))),y)=U. 14907,14906 [para_from,12400.1.1,5.1.1.1,flip.1] u(r(n(x,y)),u(r(x),z))=u(r(x),z). 15394 [para_into,14242.1.1.1,13076.1.1,demod,32,12075,flip.1] n(r(n(x,y)),c(r(y)))=Z. 15446,15445 [para_into,14242.1.1.1,1286.1.1] c(k(U,x))=n(c(x),c(k(D,x))). 15660 [para_from,14652.1.1,14.1.1.1,demod,17,13,flip.1] u(r(x),k(r(x),n(y,I)))=r(x). 15720 [para_from,14718.1.1,11914.1.1.1,demod,11825] n(r(n(x,r(D))),I)=Z. 15734 [para_into,15720.1.1.1,14234.1.1,demod,14649] r(n(r(D),I))=Z. 15766 [para_from,15734.1.1,12.1.1.1,demod,12275,flip.1] n(r(D),I)=Z. 15774 [para_from,15766.1.1,12386.1.1.1,demod,11817,flip.1] u(D,r(D))=D. 15867,15866 [para_into,15774.1.1,3.1.1] u(r(D),D)=D. 15875,15874 [para_from,15774.1.1,14.1.1.1,demod,13,15867] r(D)=D. 15922 [back_demod,12253,demod,15875,29] u(r(c(x)),r(x))=U. 15927,15926 [back_demod,11025,demod,15875,29] r(U)=U. 16025 [para_into,15922.1.1.2,12.1.1] u(r(c(r(x))),x)=U. 16029 [para_from,15922.1.1,14242.1.1.1,demod,32,flip.1] n(c(r(c(x))),c(r(x)))=Z. 16121 [para_from,16025.1.1,14242.1.1.1,demod,32,flip.1] n(c(r(c(r(x)))),c(x))=Z. 16977 [para_into,15394.1.1.1.1,13349.1.1,demod,91] n(I,c(r(c(k(n(I,x),D)))))=Z. 17301 [para_from,16029.1.1,12396.1.1.2,demod,11823,flip.1] u(r(x),c(r(c(x))))=r(x). 17414,17413 [para_from,16121.1.1,12392.1.1.1,demod,11817,flip.1] u(c(x),r(c(r(x))))=r(c(r(x))). 18946 [para_into,1412.1.1.1.1,12074.1.1,demod,12075,12075] n(u(x,y),u(x,c(y)))=x. 19097 [para_into,1528.1.1.2.1,119.1.1] n(k(n(c($c1),I),U),k(n($c1,I),U))!=Z. 19491 [para_from,17301.1.1,14.1.1.1,demod,13,13,flip.1] u(x,r(c(r(c(x)))))=x. 19503 [para_into,19491.1.1.2.1.1.1,12074.1.1,demod,17414] r(c(r(x)))=c(x). 19530,19529 [para_into,19503.1.1.1.1,12.1.1] r(c(x))=c(r(x)). 19585 [back_demod,16977,demod,19530,17,15875,12075] n(I,k(D,r(n(I,x))))=Z. 19636,19635 [para_into,19529.1.1.1,11986.1.1,demod,15,19530,19530,flip.1] c(r(n(x,y)))=u(c(r(x)),c(r(y))). 20271 [para_into,2105.1.1.1.2,12074.1.1,demod,12075,12075] n(u(x,y),u(y,c(x)))=y. 20411,20410 [para_into,18946.1.1.1,12386.1.1,demod,12061,11521] n(u(D,x),I)=n(x,I). 20415,20414 [para_into,18946.1.1.1,11520.1.1,demod,12391] n(x,u(y,c(x)))=n(y,x). 20423,20422 [para_into,18946.1.1.1,893.1.1,demod,19636,19530,12075,14907,20415,flip.1] r(n(x,y))=n(r(x),r(y)). 20429,20428 [para_into,18946.1.1.1,551.1.1,demod,11987,12075,11471] n(x,u(c(x),y))=n(y,x). 20464 [back_demod,19585,demod,20423,91] n(I,k(D,n(I,r(x))))=Z. 20563 [para_into,20410.1.1.1,3.1.1] n(u(x,D),I)=n(x,I). 20566,20565 [para_into,20410.1.1,119.1.1] n(I,u(D,x))=n(x,I). 21080 [para_into,20271.1.1,119.1.1] n(u(x,c(y)),u(y,x))=x. 21133 [para_into,20414.1.1.2,12458.1.1,demod,11905,flip.1] n(n(n(c(x),y),z),x)=Z. 21137,21136 [para_into,20414.1.1.2,5.1.1] n(x,u(y,u(z,c(x))))=n(u(y,z),x). 21155,21154 [para_from,20414.1.1,895.1.1.1,demod,12246,6] u(n(x,y),u(c(y),z))=u(x,u(c(y),z)). 21204,21203 [para_into,20428.1.1.2,11096.1.1,demod,20429,flip.1] n(u(c(x),y),x)=n(y,x). 21212 [para_into,20428.1.1.2,261.1.1,demod,21137] n(u(x,y),z)=n(u(y,x),z). 21260 [para_into,20464.1.1.2.2.2,12.1.1] n(I,k(D,n(I,x)))=Z. 21262 [para_into,21260.1.1.2.2,20565.1.1] n(I,k(D,n(x,I)))=Z. 21296 [para_from,21262.1.1,755.1.1.2,demod,11823] n(c(k(D,n(x,I))),I)=I. 21300 [para_from,21262.1.1,12372.1.1.1,demod,11817,flip.1] u(D,k(D,n(x,I)))=D. 21362 [para_from,21300.1.1,1349.1.1.2,demod,12387,flip.1] u(D,k(U,n(x,I)))=u(D,x). 21552 [para_into,21080.1.1.1,11494.1.1,demod,12302] n(c(x),u(x,y))=n(c(x),y). 21769 [para_from,21296.1.1,21133.1.1.1.1] n(n(I,x),k(D,n(y,I)))=Z. 22370 [para_into,12267.1.1.2.1.1.2,12.1.1] n(x,k(c(k(x,y)),r(y)))=Z. 25003,25002 [para_from,14036.1.1,11408.1.1.2] u(n(x,y),n(y,x))=n(x,y). 25020,25019 [para_from,14036.1.1,11499.1.1.1] u(n(x,y),u(z,n(y,x)))=u(z,n(y,x)). 27588 [para_into,21212.1.1,119.1.1] n(x,u(y,z))=n(u(z,y),x). 27880,27879 [para_into,21552.1.1.2,21362.1.1,demod,12061,20566,12061,flip.1] n(I,k(U,n(x,I)))=n(x,I). 28276,28275 [para_from,21769.1.1,755.1.1.2,demod,11823] n(c(k(D,n(x,I))),n(I,y))=n(I,y). 28633 [para_from,22370.1.1,755.1.1.2,demod,11823] n(c(k(c(k(x,y)),r(y))),x)=x. 30021 [para_from,13514.1.1,21080.1.1.2,demod,11987,14243,12075,12075,21155,25020,21204] n(n(x,y),z)=n(n(y,x),z). 32170 [para_into,27588.1.1.2,25002.1.1,demod,25003] n(x,n(y,z))=n(n(z,y),x). 32174 [copy,32170,flip.1] n(n(x,y),z)=n(z,n(y,x)). 32458 [para_from,27879.1.1,20422.1.1.1,demod,20423,91,91,17,20423,91,15927,flip.1] n(I,k(n(r(x),I),U))=n(r(x),I). 36318,36317 [para_into,14244.1.1.2,12074.1.1,demod,12075] n(n(x,y),z)=n(x,n(y,z)). 36567 [back_demod,32174,demod,36318] n(x,n(y,z))=n(z,n(y,x)). 36716 [back_demod,30021,demod,36318,36318] n(x,n(y,z))=n(y,n(x,z)). 37901,37900 [para_into,36317.1.1.1,20563.1.1,demod,36318,flip.1] n(u(x,D),n(I,y))=n(x,n(I,y)). 38243,38242 [para_into,36716.1.1.2,27879.1.1,flip.1] n(I,n(x,k(U,n(y,I))))=n(x,n(y,I)). 44557 [para_into,15660.1.1.1,12.1.1,demod,13,13] u(x,k(x,n(y,I)))=x. 44599 [para_from,44557.1.1,21552.1.1.2,demod,11907,flip.1] n(c(x),k(x,n(y,I)))=Z. 44733 [para_from,44599.1.1,36567.1.1.2,demod,12089,flip.1] n(k(x,n(y,I)),n(c(x),z))=Z. 45839 [para_into,44733.1.1,13201.1.1,demod,11987,26,20411] k(n(I,x),n(c(x),I))=Z. 45848,45847 [para_from,45839.1.1,28633.1.1.1.1.1.1,demod,11997,20423,19530,91,15446,11987,12075,26,36318,28276,37901] n(r(x),n(I,x))=n(I,x). 45851 [para_from,45839.1.1,22370.1.1.2.1.1,demod,11997,20423,19530,91,36318,38243] n(x,n(c(r(x)),I))=Z. 45948,45947 [para_from,45851.1.1,911.1.1.2,demod,15,15875,19530,14243,12061,12075,36318,12737,36318,12735,45848,11823,15,15875,19530,14243,12061,12075,36318,12737,flip.1] n(r(x),I)=n(I,x). 45991 [back_demod,32458,demod,45948,45948] n(I,k(n(I,x),U))=n(I,x). 46842,46841 [para_into,45991.1.1.2.1,27879.1.1,demod,27880] n(I,k(n(x,I),U))=n(x,I). 47702 [para_into,19097.1.1,1.2.1,demod,15927,11,12216,36318,46842,14533] Z!=Z. 47703 [binary,47702.1,44.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 4591 clauses generated 3051690 clauses kept 25169 clauses forward subsumed 2347690 clauses back subsumed 143 Kbytes malloced 23311 ----------- times (seconds) ----------- user CPU time 79.19 (0 hr, 1 min, 19 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 80 (0 hr, 1 min, 20 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 16:02:13 2003