----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sat Nov 22 00:21:03 2003 The command was "otter". set(auto). dependent: set(auto1). dependent: set(process_input). dependent: clear(print_kept). dependent: clear(print_new_demod). dependent: clear(print_back_demod). dependent: clear(print_back_sub). dependent: set(control_memory). dependent: assign(max_mem, 12000). dependent: assign(pick_given_ratio, 4). dependent: assign(stats_level, 1). dependent: assign(max_seconds, 10800). clear(print_given). assign(max_weight,19). assign(max_distinct_vars,3). assign(max_literals,1). assign(max_mem,64000). formula_list(usable). all x (x=x). end_of_list. -------> usable clausifies to: list(usable). 0 [] x=x. end_of_list. 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("peirceanAx2.txt"). ------- start included file peirceanAx2.txt------- formula_list(usable). all x (k(x,I)=x). all x y (u(k(r(x),c(k(x,y))),c(y))=c(y)). end_of_list. -------> usable clausifies to: list(usable). 0 [] k(x,I)=x. 0 [] u(k(r(x),c(k(x,y))),c(y))=c(y). end_of_list. ------- end included file peirceanAx2.txt------- include("iDef.txt"). ------- start included file iDef.txt------- formula_list(usable). all x y (i(x,y)<->u(x,y)=y). end_of_list. -------> usable clausifies to: list(usable). 0 [] -i(x,y)|u(x,y)=y. 0 [] i(x,y)|u(x,y)!=y. end_of_list. ------- end included file iDef.txt------- include("nDef.txt"). ------- start included file nDef.txt------- formula_list(usable). all x y (n(x,y)=c(u(c(x),c(y)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] n(x,y)=c(u(c(x),c(y))). end_of_list. ------- end included file nDef.txt------- include("uzDef.txt"). ------- start included file uzDef.txt------- formula_list(usable). D=c(I). U=u(I,D). Z=c(U). end_of_list. -------> usable clausifies to: list(usable). 0 [] D=c(I). 0 [] U=u(I,D). 0 [] Z=c(U). end_of_list. ------- end included file uzDef.txt------- include("xi_b.txt"). ------- start included file xi_b.txt------- formula_list(usable). -(all x i(I,u(c(x),r(x)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] -i(I,u(c($c1),r($c1))). end_of_list. ------- end included file xi_b.txt------- SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=2. This is a Horn set with equality. The strategy will be Knuth-Bendix and hyper_res, with positive clauses in sos and nonpositive clauses in usable. dependent: set(knuth_bendix). dependent: set(para_from). dependent: set(para_into). dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). dependent: set(back_demod). dependent: set(lrpo). dependent: set(hyper_res). dependent: clear(order_hyper). ------------> process usable: ** KEPT (pick-wt=8): 1 [] -i(x,y)|u(x,y)=y. ** KEPT (pick-wt=8): 2 [] i(x,y)|u(x,y)!=y. ** KEPT (pick-wt=7): 3 [] -i(I,u(c($c1),r($c1))). ------------> process sos: ** KEPT (pick-wt=3): 4 [] x=x. ** KEPT (pick-wt=7): 5 [] u(x,y)=u(y,x). ** KEPT (pick-wt=11): 7 [copy,6,flip.1] u(u(x,y),z)=u(x,u(y,z)). ---> New Demodulator: 8 [new_demod,7] u(u(x,y),z)=u(x,u(y,z)). ** KEPT (pick-wt=14): 9 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ---> New Demodulator: 10 [new_demod,9] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ** KEPT (pick-wt=11): 12 [copy,11,flip.1] k(k(x,y),z)=k(x,k(y,z)). ---> New Demodulator: 13 [new_demod,12] k(k(x,y),z)=k(x,k(y,z)). ** KEPT (pick-wt=5): 14 [] r(r(x))=x. ---> New Demodulator: 15 [new_demod,14] r(r(x))=x. ** KEPT (pick-wt=10): 16 [] r(u(x,y))=u(r(x),r(y)). ---> New Demodulator: 17 [new_demod,16] r(u(x,y))=u(r(x),r(y)). ** KEPT (pick-wt=10): 18 [] r(k(x,y))=k(r(y),r(x)). ---> New Demodulator: 19 [new_demod,18] r(k(x,y))=k(r(y),r(x)). ** KEPT (pick-wt=13): 21 [copy,20,flip.1] u(k(x,y),k(z,y))=k(u(x,z),y). ---> New Demodulator: 22 [new_demod,21] u(k(x,y),k(z,y))=k(u(x,z),y). ** KEPT (pick-wt=5): 23 [] k(x,I)=x. ---> New Demodulator: 24 [new_demod,23] k(x,I)=x. ** KEPT (pick-wt=13): 25 [] u(k(r(x),c(k(x,y))),c(y))=c(y). ---> New Demodulator: 26 [new_demod,25] u(k(r(x),c(k(x,y))),c(y))=c(y). ** KEPT (pick-wt=10): 28 [copy,27,flip.1] c(u(c(x),c(y)))=n(x,y). ---> New Demodulator: 29 [new_demod,28] c(u(c(x),c(y)))=n(x,y). ** KEPT (pick-wt=4): 31 [copy,30,flip.1] c(I)=D. ---> New Demodulator: 32 [new_demod,31] c(I)=D. ** KEPT (pick-wt=5): 34 [copy,33,flip.1] u(I,D)=U. ---> New Demodulator: 35 [new_demod,34] u(I,D)=U. ** KEPT (pick-wt=4): 37 [copy,36,flip.1] c(U)=Z. ---> New Demodulator: 38 [new_demod,37] c(U)=Z. Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] x=x. Following clause subsumed by 5 during input processing: 0 [copy,5,flip.1] u(x,y)=u(y,x). >>>> Starting back demodulation with 8. >>>> Starting back demodulation with 10. >>>> Starting back demodulation with 13. >>>> Starting back demodulation with 15. >>>> Starting back demodulation with 17. >>>> Starting back demodulation with 19. >>>> Starting back demodulation with 22. >>>> Starting back demodulation with 24. >>>> Starting back demodulation with 26. >>>> Starting back demodulation with 29. >> back demodulating 9 with 29. >>>> Starting back demodulation with 32. >>>> Starting back demodulation with 35. >>>> Starting back demodulation with 38. >>>> Starting back demodulation with 40. ======= end of input processing ======= =========== start of search =========== Resetting weight limit to 11. sos_size=15008 Resetting weight limit to 10. sos_size=3741 ----> UNIT CONFLICT at 825.43 sec ----> 54984 [binary,54983.1,41.1] $F. Length of proof is 246. Level of proof is 36. ---------------- PROOF ---------------- 1 [] -i(x,y)|u(x,y)=y. 2 [] i(x,y)|u(x,y)!=y. 3 [] -i(I,u(c($c1),r($c1))). 5 [] u(x,y)=u(y,x). 6 [] u(x,u(y,z))=u(u(x,y),z). 8,7 [copy,6,flip.1] u(u(x,y),z)=u(x,u(y,z)). 9 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 15,14 [] r(r(x))=x. 17,16 [] r(u(x,y))=u(r(x),r(y)). 19,18 [] r(k(x,y))=k(r(y),r(x)). 20 [] k(u(x,y),z)=u(k(x,z),k(y,z)). 21 [copy,20,flip.1] u(k(x,y),k(z,y))=k(u(x,z),y). 24,23 [] k(x,I)=x. 25 [] u(k(r(x),c(k(x,y))),c(y))=c(y). 27 [] n(x,y)=c(u(c(x),c(y))). 29,28 [copy,27,flip.1] c(u(c(x),c(y)))=n(x,y). 30 [] D=c(I). 32,31 [copy,30,flip.1] c(I)=D. 33 [] U=u(I,D). 35,34 [copy,33,flip.1] u(I,D)=U. 36 [] Z=c(U). 38,37 [copy,36,flip.1] c(U)=Z. 39 [back_demod,9,demod,29] u(c(u(c(x),y)),n(x,y))=x. 41 [para_from,5.1.1,3.1.2] -i(I,u(r($c1),c($c1))). 43,42 [para_into,34.1.1,5.1.1] u(D,I)=U. 44 [para_into,16.1.1.1,42.1.1] r(U)=u(r(D),r(I)). 47,46 [para_into,7.1.1.1,42.1.1] u(U,x)=u(D,u(I,x)). 50 [para_into,7.1.1.1,5.1.1,demod,8] u(x,u(y,z))=u(y,u(x,z)). 51 [para_into,7.1.1,5.1.1] u(x,u(y,z))=u(y,u(z,x)). 52 [copy,51,flip.1] u(x,u(y,z))=u(z,u(x,y)). 53 [para_into,46.1.1,5.1.1] u(x,U)=u(D,u(I,x)). 54 [copy,53,flip.1] u(D,u(I,x))=u(x,U). 55 [para_into,53.1.1,7.1.1] u(x,u(y,U))=u(D,u(I,u(x,y))). 56 [copy,55,flip.1] u(D,u(I,u(x,y)))=u(x,u(y,U)). 57 [para_from,53.1.1,7.1.1.1,demod,8,8,47] u(D,u(I,u(x,y)))=u(x,u(D,u(I,y))). 58 [copy,57,flip.1] u(x,u(D,u(I,y)))=u(D,u(I,u(x,y))). 61 [para_into,54.1.1.2,5.1.1] u(D,u(x,I))=u(x,U). 62 [para_into,54.1.1,5.1.1,demod,8] u(I,u(x,D))=u(x,U). 63 [copy,61,flip.1] u(x,U)=u(D,u(x,I)). 64 [copy,62,flip.1] u(x,U)=u(I,u(x,D)). 77 [para_into,18.1.1.1,23.1.1,flip.1] k(r(I),r(x))=r(x). 85 [para_into,77.1.1.2,14.1.1,demod,15] k(r(I),x)=x. 88,87 [para_into,85.1.1,23.1.1] r(I)=I. 90,89 [back_demod,85,demod,88] k(I,x)=x. 92,91 [back_demod,44,demod,88] r(U)=u(r(D),I). 93 [para_into,21.1.1.1,89.1.1] u(x,k(y,x))=k(u(I,y),x). 95,94 [para_into,21.1.1.2,89.1.1] u(k(x,y),y)=k(u(x,I),y). 97 [copy,93,flip.1] k(u(I,x),y)=u(y,k(x,y)). 99,98 [para_into,28.1.1.1.1,37.1.1] c(u(Z,c(x)))=n(U,x). 109,108 [para_into,28.1.1.1.2,28.1.1] c(u(c(x),n(y,z)))=n(x,u(c(y),c(z))). 110 [para_into,28.1.1.1,5.1.1,demod,29] n(x,y)=n(y,x). 113 [para_into,98.1.1.1.2,37.1.1] c(u(Z,Z))=n(U,U). 117 [para_into,98.1.1.1.2,28.1.1] c(u(Z,n(x,y)))=n(U,u(c(x),c(y))). 122 [para_into,25.1.1.1.1,87.1.1,demod,90,90] u(c(x),c(x))=c(x). 130 [para_into,25.1.1.1.2.1,23.1.1,demod,32,32] u(k(r(x),c(x)),D)=D. 132 [para_into,25.1.1.2,98.1.1,demod,99] u(k(r(x),c(k(x,u(Z,c(y))))),n(U,y))=n(U,y). 143,142 [para_from,25.1.1,7.1.1.1,flip.1] u(k(r(x),c(k(x,y))),u(c(y),z))=u(c(y),z). 158,157 [para_into,122.1.1.1,37.1.1,demod,38,38] u(Z,Z)=Z. 159 [para_into,122.1.1.1,31.1.1,demod,32,32] u(D,D)=D. 167 [back_demod,113,demod,158] c(Z)=n(U,U). 169 [para_from,122.1.1,28.1.1.1] c(c(x))=n(x,x). 173 [para_from,122.1.1,7.1.1.1,flip.1] u(c(x),u(c(x),y))=u(c(x),y). 182 [para_into,39.1.1.1.1.1,98.1.1] u(c(u(n(U,x),y)),n(u(Z,c(x)),y))=u(Z,c(x)). 184 [para_into,39.1.1.1.1.1,37.1.1] u(c(u(Z,x)),n(U,x))=U. 186 [para_into,39.1.1.1.1.1,31.1.1] u(c(u(D,x)),n(I,x))=I. 195,194 [para_into,39.1.1.1.1,53.1.1] u(c(u(D,u(I,c(x)))),n(x,U))=x. 196 [para_into,39.1.1.1.1,39.1.1] u(c(x),n(u(c(x),y),n(x,y)))=u(c(x),y). 200 [para_into,39.1.1.1,28.1.1] u(n(x,y),n(x,c(y)))=x. 202 [para_into,39.1.1.2,110.1.1] u(c(u(c(x),y)),n(y,x))=x. 204 [para_into,39.1.1,5.1.1] u(n(x,y),c(u(c(x),y)))=x. 212 [para_from,157.1.1,7.1.1.1,flip.1] u(Z,u(Z,x))=u(Z,x). 215,214 [para_from,159.1.1,62.1.1.2,demod,35,flip.1] u(D,U)=U. 219,218 [para_from,159.1.1,7.1.1.1,flip.1] u(D,u(D,x))=u(D,x). 222 [para_into,50.1.1.2,157.1.1,flip.1] u(Z,u(x,Z))=u(x,Z). 239 [para_from,50.1.1,39.1.1.1.1] u(c(u(x,u(c(y),z))),n(y,u(x,z)))=y. 242 [para_from,214.1.1,50.1.1.2,flip.1] u(D,u(x,U))=u(x,U). 254 [para_into,169.1.1.1,31.1.1] c(D)=n(I,I). 256 [para_into,169.1.1.1,28.1.1] c(n(x,y))=n(u(c(x),c(y)),u(c(x),c(y))). 276 [para_from,51.1.1,39.1.1.1.1] u(c(u(x,u(y,c(z)))),n(z,u(x,y)))=z. 307 [para_from,52.1.1,39.1.1.1.1] u(c(u(x,u(c(y),z))),n(y,u(z,x)))=y. 404 [para_into,130.1.1.1.2,254.1.1] u(k(r(D),n(I,I)),D)=D. 424 [para_into,130.1.1,5.1.1] u(D,k(r(x),c(x)))=D. 518 [para_into,212.1.1.2,51.1.1] u(Z,u(x,u(y,Z)))=u(Z,u(x,y)). 547 [para_from,58.1.1,39.1.1.1.1] u(c(u(D,u(I,u(c(x),y)))),n(x,u(D,u(I,y))))=x. 695 [para_into,424.1.1.2.2,254.1.1] u(D,k(r(D),n(I,I)))=D. 785 [para_into,93.1.1.2,89.1.1] u(x,x)=k(u(I,I),x). 809 [para_from,93.1.1,16.1.1.1,demod,19,17,88,19,flip.1] u(r(x),k(r(x),r(y)))=k(r(x),u(I,r(y))). 811 [para_from,93.1.1,7.1.1.1] u(k(u(I,x),y),z)=u(y,u(k(x,y),z)). 865,864 [para_from,94.1.1,242.1.1.2,demod,95] u(D,k(u(x,I),U))=k(u(x,I),U). 1052 [para_into,108.1.1.1.1,98.1.1] c(u(n(U,x),n(y,z)))=n(u(Z,c(x)),u(c(y),c(z))). 1054 [para_into,108.1.1.1.2,110.1.1,demod,109] n(x,u(c(y),c(z)))=n(x,u(c(z),c(y))). 1226,1225 [para_into,785.1.1,64.1.1,demod,47,35,215] u(I,U)=k(u(I,I),U). 1227 [para_into,785.1.1,63.1.1,demod,47,219] u(D,u(I,I))=k(u(I,I),U). 1235 [para_into,785.1.1,50.1.1,demod,8] u(x,u(x,u(y,y)))=k(u(I,I),u(x,y)). 1241 [copy,1235,flip.1] k(u(I,I),u(x,y))=u(x,u(x,u(y,y))). 1462 [para_into,132.1.1,5.1.1] u(n(U,x),k(r(y),c(k(y,u(Z,c(x))))))=n(U,x). 1792 [hyper,173,2] i(c(x),u(c(x),y)). 1830 [para_into,1792.1.2,39.1.1] i(c(u(c(x),y)),x). 1831 [para_into,1792.1.2,5.1.1] i(c(x),u(y,c(x))). 1836 [para_into,1830.1.1.1.1,117.1.1] i(c(u(n(U,u(c(x),c(y))),z)),u(Z,n(x,y))). 1841 [para_into,1830.1.1.1.1,98.1.1] i(c(u(n(U,x),y)),u(Z,c(x))). 1842 [para_into,1830.1.1.1.1,37.1.1] i(c(u(Z,x)),U). 1856 [para_into,1830.1.1.1,5.1.1] i(c(u(x,c(y))),y). 1860 [para_into,1830.1.1,28.1.1] i(n(x,y),x). 1864,1863 [hyper,1860,1] u(n(x,y),x)=x. 1865 [para_into,1860.1.1,110.1.1] i(n(x,y),y). 1886 [para_into,182.1.1.2,110.1.1] u(c(u(n(U,x),y)),n(y,u(Z,c(x))))=u(Z,c(x)). 1888 [para_into,182.1.1,5.1.1] u(n(u(Z,c(x)),y),c(u(n(U,x),y)))=u(Z,c(x)). 1890 [para_from,182.1.1,108.1.1.1,demod,99,99,flip.1] n(u(n(U,x),y),u(n(U,x),c(y)))=n(U,x). 1895,1894 [hyper,1865,1] u(n(x,y),y)=y. 1897,1896 [hyper,1842,1] u(c(u(Z,x)),U)=U. 1949 [para_into,184.1.1.2,110.1.1] u(c(u(Z,x)),n(x,U))=U. 1951 [para_into,184.1.1,5.1.1] u(n(U,x),c(u(Z,x)))=U. 1959 [para_from,184.1.1,108.1.1.1,demod,38,38,flip.1] n(u(Z,x),u(Z,c(x)))=Z. 1961 [para_from,184.1.1,39.1.1.1.1,demod,38] u(Z,n(u(Z,x),n(U,x)))=u(Z,x). 1971,1970 [para_from,184.1.1,56.1.1.2.2,demod,1226,865,1864,1897] k(u(I,I),U)=U. 1972 [para_from,184.1.1,16.1.1.1,demod,92,flip.1] u(r(c(u(Z,x))),r(n(U,x)))=u(r(D),I). 1983,1982 [back_demod,1227,demod,1971] u(D,u(I,I))=U. 1984 [back_demod,1225,demod,1971] u(I,U)=U. 2013 [para_from,1984.1.1,97.1.1.1,flip.1] u(x,k(U,x))=k(U,x). 2103 [para_from,186.1.1,57.1.1.2.2,demod,1983,flip.1] u(c(u(D,x)),u(D,u(I,n(I,x))))=U. 2238 [para_into,194.1.1.2,110.1.1] u(c(u(D,u(I,c(x)))),n(U,x))=x. 2246 [para_from,194.1.1,173.1.1.2,demod,195] u(c(u(D,u(I,c(x)))),x)=x. 2253 [para_from,194.1.1,56.1.1.2.2,demod,1895,flip.1] u(c(u(D,u(I,c(x)))),U)=u(D,u(I,x)). 2300 [para_into,196.1.1.2,110.1.1] u(c(x),n(n(x,y),u(c(x),y)))=u(c(x),y). 2338 [para_into,1863.1.1,55.1.1] u(D,u(I,u(n(u(x,U),y),x)))=u(x,U). 2349,2348 [para_into,1863.1.1,5.1.1] u(x,n(x,y))=x. 2351,2350 [back_demod,2103,demod,2349,43] u(c(u(D,x)),U)=U. 2353,2352 [back_demod,2253,demod,2351,flip.1] u(D,u(I,x))=U. 2355,2354 [back_demod,2338,demod,2353,flip.1] u(x,U)=U. 2366,2365 [back_demod,2246,demod,2353,38] u(Z,x)=x. 2374,2373 [back_demod,2238,demod,2353,38,2366] n(U,x)=x. 2410,2409 [back_demod,547,demod,2353,38,2353,2366] n(x,U)=x. 2459 [back_demod,1972,demod,2366,2374] u(r(c(x)),r(x))=u(r(D),I). 2462,2461 [back_demod,1961,demod,2366,2374,2366,2366] n(x,x)=x. 2464,2463 [back_demod,1959,demod,2366,2366] n(x,c(x))=Z. 2465 [back_demod,1951,demod,2374,2366] u(x,c(x))=U. 2467 [back_demod,1949,demod,2366,2410] u(c(x),x)=U. 2473 [back_demod,1888,demod,2366,2374,2366] u(n(c(x),y),c(u(x,y)))=c(x). 2475 [back_demod,1886,demod,2374,2366,2366] u(c(u(x,y)),n(y,c(x)))=c(x). 2485 [back_demod,1841,demod,2374,2366] i(c(u(x,y)),c(x)). 2487 [back_demod,1836,demod,2374,8,2366] i(c(u(c(x),u(c(y),z))),n(x,y)). 2496 [back_demod,1462,demod,2374,2366,2374] u(x,k(r(y),c(k(y,c(x)))))=x. 2509 [back_demod,1052,demod,2374,2366] c(u(x,n(y,z)))=n(c(x),u(c(y),c(z))). 2516,2515 [back_demod,518,demod,2366,2366] u(x,u(y,Z))=u(x,y). 2522,2521 [back_demod,222,demod,2516,2366,flip.1] u(x,Z)=x. 2527 [back_demod,1890,demod,2374,2374,2374] n(u(x,y),u(x,c(y)))=x. 2575,2574 [back_demod,167,demod,2462] c(Z)=U. 2608 [back_demod,695,demod,2462,24] u(D,r(D))=D. 2612,2611 [back_demod,404,demod,2462,24] u(r(D),D)=D. 2614,2613 [back_demod,254,demod,2462] c(D)=I. 2630,2629 [back_demod,256,demod,2462] c(n(x,y))=u(c(x),c(y)). 2632,2631 [back_demod,169,demod,2462] c(c(x))=x. 2659 [para_from,1863.1.1,1856.1.1.1,demod,2632] i(x,x). 2663 [para_from,1863.1.1,50.1.1.2,flip.1] u(n(x,y),u(z,x))=u(z,x). 2667 [para_from,1863.1.1,16.1.1.1,flip.1] u(r(n(x,y)),r(x))=r(x). 2697,2696 [hyper,2659,1] u(x,x)=x. 2702 [back_demod,1241,demod,2697,90,2697,flip.1] u(x,u(x,y))=u(x,y). 2727 [para_from,200.1.1,16.1.1.1,flip.1] u(r(n(x,y)),r(n(x,c(y))))=r(x). 2768 [para_into,202.1.1.1.1,186.1.1,demod,32] u(D,n(n(I,x),u(D,x)))=u(D,x). 2787 [para_from,202.1.1,50.1.1.2,flip.1] u(c(u(c(x),y)),u(z,n(y,x)))=u(z,x). 2791 [para_from,202.1.1,7.1.1.1,flip.1] u(c(u(c(x),y)),u(n(y,x),z))=u(x,z). 2801 [para_into,204.1.1.2.1,186.1.1,demod,32] u(n(u(D,x),n(I,x)),D)=u(D,x). 2831,2830 [para_from,2631.1.1,28.1.1.1.2] c(u(c(x),y))=n(x,c(y)). 2832 [para_from,2631.1.1,1831.1.1,demod,2632] i(x,u(y,x)). 2833 [para_from,2631.1.1,1792.1.1,demod,2632] i(x,u(x,y)). 2841,2840 [para_from,2631.1.1,28.1.1.1.1] c(u(x,c(y)))=n(c(x),y). 2844 [back_demod,2791,demod,2831] u(n(x,c(y)),u(n(y,x),z))=u(x,z). 2848 [back_demod,2787,demod,2831] u(n(x,c(y)),u(z,n(y,x)))=u(z,x). 2856 [back_demod,2487,demod,2831,2831] i(n(x,n(y,c(z))),n(x,y)). 2907 [para_into,2832.1.2,52.1.1] i(u(x,y),u(y,u(z,x))). 2908 [para_into,2832.1.2,51.1.1] i(u(x,y),u(x,u(y,z))). 2914 [para_into,2833.1.2,52.1.1] i(x,u(y,u(x,z))). 2944,2943 [para_into,2463.1.1.2,2631.1.1] n(c(x),x)=Z. 2947 [para_from,2465.1.1,239.1.1.1.1.2,demod,2355,38,2632,2366] n(x,u(y,x))=x. 3002,3001 [para_from,2608.1.1,16.1.1.1,demod,15,2612] r(D)=D. 3014 [back_demod,2459,demod,3002,43] u(r(c(x)),r(x))=U. 3085 [para_into,276.1.1.2.2,142.1.1,demod,8,143,2831,2841] u(n(x,n(c(y),z)),n(z,u(c(x),y)))=z. 3136 [para_into,1894.1.1,5.1.1] u(x,n(y,x))=x. 3151,3150 [para_from,1894.1.1,50.1.1.2,flip.1] u(n(x,y),u(z,y))=u(z,y). 3200 [para_from,2348.1.1,97.1.1.1,demod,90,flip.1] u(x,k(n(I,y),x))=x. 3214 [para_into,307.1.1.1.1.2,2467.1.1,demod,2355,38,2366] n(x,u(x,y))=x. 3327 [para_into,2485.1.1.1,52.1.1] i(c(u(x,u(y,z))),c(y)). 3454 [para_into,2914.1.2.2,1894.1.1] i(n(x,y),u(z,y)). 3496 [para_into,2947.1.1.2,21.1.1] n(k(x,y),k(u(z,x),y))=k(x,y). 3498 [para_into,2947.1.1.2,7.1.1] n(x,u(y,u(z,x)))=x. 3500 [para_into,2947.1.1,110.1.1] n(u(x,y),y)=y. 3516 [para_from,3136.1.1,97.1.1.1,demod,90,flip.1] u(x,k(n(y,I),x))=x. 3570 [para_into,3214.1.1,110.1.1] n(u(x,y),x)=x. 3680 [para_into,3454.1.2,3136.1.1] i(n(x,n(y,z)),z). 3681 [para_into,3454.1.2,2348.1.1] i(n(x,n(y,z)),y). 3700 [para_into,3500.1.1.1,3136.1.1] n(x,n(y,x))=n(y,x). 3730 [para_into,3500.1.1.1,7.1.1] n(u(x,u(y,z)),z)=z. 3783 [para_into,3570.1.1.1,52.1.1] n(u(x,u(y,z)),y)=y. 3870 [hyper,3680,1] u(n(x,n(y,z)),z)=z. 3872 [hyper,3681,1] u(n(x,n(y,z)),y)=y. 4653 [para_into,3014.1.1.2,14.1.1] u(r(c(r(x))),x)=U. 5438 [para_into,809.1.1.1,14.1.1,demod,15,15] u(x,k(x,r(y)))=k(x,u(I,r(y))). 5489 [para_into,811.1.1.1.1,2348.1.1,demod,90,flip.1] u(x,u(k(n(I,y),x),z))=u(x,z). 6153 [para_into,2907.1.2.2,3136.1.1] i(u(n(x,y),z),u(z,y)). 6185 [para_into,2908.1.2.2,1894.1.1] i(u(x,n(y,z)),u(x,z)). 6876 [para_into,3327.1.1.1.2,2013.1.1] i(c(u(x,k(U,y))),c(y)). 7151,7150 [para_into,3498.1.1.2.2,3136.1.1] n(n(x,y),u(z,y))=n(x,y). 7167,7166 [back_demod,2768,demod,7151] u(D,n(I,x))=u(D,x). 7169,7168 [back_demod,2300,demod,7151] u(c(x),n(x,y))=u(c(x),y). 7463,7462 [para_into,3730.1.1.1.2,3136.1.1] n(u(x,y),n(z,y))=n(z,y). 7486 [back_demod,2801,demod,7463] u(n(I,x),D)=u(D,x). 7578 [para_into,3783.1.1.1.2,2013.1.1] n(u(x,k(U,y)),y)=y. 7718,7717 [para_from,3870.1.1,3570.1.1.1] n(x,n(y,n(z,x)))=n(y,n(z,x)). 7748,7747 [para_from,3872.1.1,3570.1.1.1] n(x,n(y,n(x,z)))=n(y,n(x,z)). 9779,9778 [para_into,1054.1.1.2.1,31.1.1,demod,32,flip.1] n(x,u(c(y),D))=n(x,u(D,c(y))). 11138,11137 [hyper,6876,1] u(c(u(x,k(U,y))),c(y))=c(y). 17511 [para_from,2473.1.1,6153.1.1] i(c(x),u(c(u(x,y)),y)). 19301 [para_into,17511.1.2.1.1,4653.1.1,demod,38,2366] i(c(r(c(r(x)))),x). 19391 [hyper,19301,1] u(c(r(c(r(x)))),x)=x. 19424,19423 [para_into,2509.1.1.1.2,7578.1.1,demod,11138] c(u(x,y))=n(c(x),c(y)). 19439 [para_into,2509.1.1.1,2475.1.1,demod,2632,19424,2630,2632,2632,2632,flip.1] n(u(x,y),u(c(y),x))=x. 20921,20920 [para_into,2527.1.1.1,7486.1.1,demod,2614,1864] n(u(D,x),I)=n(I,x). 21047,21046 [para_into,2527.1.1.1,200.1.1,demod,2630,2632,3151] n(x,u(c(x),y))=n(x,y). 21073,21072 [para_into,2527.1.1.2,4653.1.1,demod,2410] u(r(c(r(c(x)))),x)=r(c(r(c(x)))). 21935 [para_from,19391.1.1,16.1.1.1,demod,21073,flip.1] r(c(r(c(r(x)))))=r(x). 22201,22200 [para_into,20920.1.1.1,2702.1.1,demod,20921,flip.1] n(I,u(D,x))=n(I,x). 22765 [para_into,21935.1.1.1.1.1.1,14.1.1,demod,15] r(c(r(c(x))))=x. 22767 [para_into,22765.1.1.1.1.1,2631.1.1] r(c(r(x)))=c(x). 22820,22819 [para_into,22767.1.1.1.1,14.1.1] r(c(x))=c(r(x)). 23554,23553 [para_into,22819.1.1.1,2629.1.1,demod,17,22820,22820,flip.1] c(r(n(x,y)))=u(c(r(x)),c(r(y))). 23811 [para_from,2667.1.1,2914.1.2.2] i(r(n(x,y)),u(z,r(x))). 24960 [para_from,2727.1.1,2527.1.1.1,demod,23554,22820,2632] n(r(x),u(r(n(x,y)),u(c(r(x)),r(y))))=r(n(x,y)). 25583 [para_into,23811.1.1.1,3700.1.1] i(r(n(x,y)),u(z,r(y))). 27073,27072 [para_into,2844.1.1.2,2663.1.1] u(n(x,c(y)),u(z,y))=u(x,u(z,y)). 27324,27323 [para_from,2848.1.1,2844.1.1.2,demod,27073,flip.1] u(c(x),u(y,n(x,z)))=u(c(x),u(y,z)). 27539 [para_into,2856.1.1.2.2,2631.1.1] i(n(x,n(y,z)),n(x,y)). 27713,27712 [hyper,25583,1] u(r(n(x,y)),u(z,r(y)))=u(z,r(y)). 27715,27714 [back_demod,24960,demod,27713,21047,flip.1] r(n(x,y))=n(r(x),r(y)). 29114 [hyper,27539,1] u(n(x,n(y,z)),n(x,y))=n(x,y). 29134 [para_into,27539.1.1.2,3500.1.1] i(n(x,y),n(x,u(z,y))). 30919 [para_into,29134.1.1,110.1.1] i(n(x,y),n(y,u(z,x))). 32533 [para_into,30919.1.2,110.1.1] i(n(x,y),n(u(z,x),y)). 33160 [para_from,3085.1.1,6185.1.1] i(x,u(n(y,n(c(z),x)),u(c(y),z))). 33533 [para_into,32533.1.2.1,3200.1.1] i(n(k(n(I,x),y),z),n(y,z)). 38577,38576 [para_into,21046.1.1.2.1,2629.1.1,demod,8] n(n(x,y),u(c(x),u(c(y),z)))=n(n(x,y),z). 38621 [para_into,21046.1.1.2,2496.1.1,demod,2464,2632,flip.1] n(x,k(r(y),c(k(y,x))))=Z. 38669 [para_into,21046.1.1,110.1.1] n(u(c(x),y),x)=n(x,y). 43274 [para_into,3496.1.1.2.1,3136.1.1] n(k(n(x,y),z),k(y,z))=k(n(x,y),z). 45230 [para_into,5438.1.1.2.2,3001.1.1,demod,3002,35] u(x,k(x,D))=k(x,U). 45232 [para_into,5438.1.1.2.2,14.1.1,demod,15] u(x,k(x,y))=k(x,u(I,y)). 45233 [copy,45232,flip.1] k(x,u(I,y))=u(x,k(x,y)). 45234 [para_into,45230.1.1,5.1.1] u(k(x,D),x)=k(x,U). 45430 [para_into,5489.1.1.2,45234.1.1,demod,7167] u(D,k(n(I,x),U))=u(D,x). 48490 [para_into,45233.1.1.2,3516.1.1,demod,24,24,flip.1] u(x,k(x,n(y,I)))=x. 48587 [para_from,48490.1.1,38669.1.1.1,demod,2944,flip.1] n(x,k(c(x),n(y,I)))=Z. 48856,48855 [para_from,45430.1.1,22200.1.1.2,demod,22201,flip.1] n(I,k(n(I,x),U))=n(I,x). 53405,53404 [para_from,29114.1.1,19439.1.1.1,demod,2630,8,27324,7169,38577] n(n(x,y),z)=n(x,n(y,z)). 53406 [para_from,29114.1.1,3214.1.1.2,demod,53405,53405,7718,7748] n(x,n(y,z))=n(y,n(z,x)). 53455 [copy,53406,flip.1] n(x,n(y,z))=n(z,n(x,y)). 53830 [para_from,43274.1.1,33533.1.1] i(k(n(I,x),y),n(y,k(x,y))). 54003 [para_into,53830.1.2,48587.1.1,demod,2630,32,9779,22201] i(k(n(I,c(x)),n(x,I)),Z). 54009 [hyper,54003,1,demod,2522] k(n(I,c(x)),n(x,I))=Z. 54030 [para_from,54009.1.1,38621.1.1.2.2.1,demod,27715,88,22820,2575,53405,48856] n(x,n(I,c(r(x))))=Z. 54039 [para_into,54030.1.1,53455.1.1] n(c(r(x)),n(x,I))=Z. 54972 [para_from,54039.1.1,33160.1.2.1,demod,22820,2632,2366] i(I,u(c(r(x)),x)). 54983 [para_into,54972.1.2.1.1,22819.1.1,demod,2632] i(I,u(r(x),c(x))). 54984 [binary,54983.1,41.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 20220 clauses generated 34779575 clauses kept 42747 clauses forward subsumed 16846788 clauses back subsumed 4532 Kbytes malloced 28101 ----------- times (seconds) ----------- user CPU time 825.64 (0 hr, 13 min, 45 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 826 (0 hr, 13 min, 46 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 Sat Nov 22 00:34:49 2003