----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sat Nov 29 23:56:55 2003 The command was "otter". set(auto). dependent: set(auto1). dependent: set(process_input). dependent: clear(print_kept). dependent: clear(print_new_demod). dependent: clear(print_back_demod). dependent: clear(print_back_sub). dependent: set(control_memory). dependent: assign(max_mem, 12000). dependent: assign(pick_given_ratio, 4). dependent: assign(stats_level, 1). dependent: assign(max_seconds, 10800). clear(print_given). assign(max_seconds,60). assign(max_distinct_vars,3). assign(max_literals,1). assign(max_mem,32000). assign(max_weight,25). 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("robbinsAx.txt"). ------- start included file robbinsAx.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("3robbinsAx.txt"). ------- start included file 3robbinsAx.txt------- formula_list(usable). all x y (c(u(c(u(x,y)),c(u(x,c(y)))))=x). end_of_list. -------> usable clausifies to: list(usable). 0 [] c(u(c(u(x,y)),c(u(x,c(y)))))=x. end_of_list. ------- end included file 3robbinsAx.txt------- ------- end included file robbinsAx.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("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("xxii.txt"). ------- start included file xxii.txt------- formula_list(usable). all x (i(x,I)->k(x,x)=x). -(all x (i(x,I)->r(x)=x)). end_of_list. -------> usable clausifies to: list(usable). 0 [] -i(x,I)|k(x,x)=x. 0 [] i($c1,I). 0 [] r($c1)!=$c1. end_of_list. ------- end included file xxii.txt------- SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=2. This is a Horn set with equality. The strategy will be Knuth-Bendix and hyper_res, with positive clauses in sos and nonpositive clauses in usable. dependent: set(knuth_bendix). dependent: set(para_from). dependent: set(para_into). dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). dependent: set(back_demod). dependent: set(lrpo). dependent: set(hyper_res). dependent: clear(order_hyper). ------------> process usable: ** KEPT (pick-wt=8): 1 [] -i(x,y)|u(x,y)=y. ** KEPT (pick-wt=8): 2 [] i(x,y)|u(x,y)!=y. ** KEPT (pick-wt=8): 3 [] -i(x,I)|k(x,x)=x. ** KEPT (pick-wt=4): 4 [] r($c1)!=$c1. ------------> process sos: ** 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=13): 9 [] c(u(c(u(x,y)),c(u(x,c(y)))))=x. ---> New Demodulator: 10 [new_demod,9] c(u(c(u(x,y)),c(u(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=4): 28 [copy,27,flip.1] c(I)=D. ---> New Demodulator: 29 [new_demod,28] c(I)=D. ** KEPT (pick-wt=5): 31 [copy,30,flip.1] u(I,D)=U. ---> New Demodulator: 32 [new_demod,31] u(I,D)=U. ** KEPT (pick-wt=4): 34 [copy,33,flip.1] c(U)=Z. ---> New Demodulator: 35 [new_demod,34] c(U)=Z. ** KEPT (pick-wt=3): 36 [] i($c1,I). 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. >>>> Starting back demodulation with 32. >>>> Starting back demodulation with 35. ======= end of input processing ======= =========== start of search =========== Resetting weight limit to 10. sos_size=6409 ----> UNIT CONFLICT at 40.14 sec ----> 18944 [binary,18942.1,4.1] $F. Length of proof is 189. Level of proof is 38. ---------------- PROOF ---------------- 1 [] -i(x,y)|u(x,y)=y. 2 [] i(x,y)|u(x,y)!=y. 3 [] -i(x,I)|k(x,x)=x. 4 [] r($c1)!=$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)). 10,9 [] c(u(c(u(x,y)),c(u(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)). 22,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 [] D=c(I). 29,28 [copy,27,flip.1] c(I)=D. 30 [] U=u(I,D). 32,31 [copy,30,flip.1] u(I,D)=U. 33 [] Z=c(U). 35,34 [copy,33,flip.1] c(U)=Z. 36 [] i($c1,I). 38 [hyper,36,3] k($c1,$c1)=$c1. 41,40 [hyper,36,1] u($c1,I)=I. 44 [para_into,7.1.1.1,5.1.1,demod,8] u(x,u(y,z))=u(y,u(x,z)). 45 [para_into,7.1.1,5.1.1] u(x,u(y,z))=u(y,u(z,x)). 46 [copy,45,flip.1] u(x,u(y,z))=u(z,u(x,y)). 49 [para_into,9.1.1.1.1.1,7.1.1,demod,8] c(u(c(u(x,u(y,z))),c(u(x,u(y,c(z))))))=u(x,y). 51 [para_into,9.1.1.1.1.1,5.1.1] c(u(c(u(x,y)),c(u(y,c(x)))))=y. 55 [para_into,9.1.1.1.2.1.2,34.1.1] c(u(c(u(x,U)),c(u(x,Z))))=x. 57 [para_into,9.1.1.1.2.1.2,28.1.1] c(u(c(u(x,I)),c(u(x,D))))=x. 59 [para_into,9.1.1.1.2.1.2,9.1.1] c(u(c(u(x,u(c(u(y,z)),c(u(y,c(z)))))),c(u(x,y))))=x. 61 [para_into,9.1.1.1.2.1,5.1.1] c(u(c(u(x,y)),c(u(c(y),x))))=x. 65 [para_into,9.1.1.1,5.1.1] c(u(c(u(x,c(y))),c(u(x,y))))=x. 68,67 [para_into,31.1.1,5.1.1] u(D,I)=U. 72,71 [para_from,31.1.1,7.1.1.1] u(U,x)=u(I,u(D,x)). 73 [para_into,40.1.1,5.1.1] u(I,$c1)=I. 75 [para_from,40.1.1,9.1.1.1.1.1,demod,29,29] c(u(D,c(u($c1,D))))=$c1. 112 [para_into,16.1.1.1,73.1.1,flip.1] u(r(I),r($c1))=r(I). 116 [para_into,16.1.1.1,67.1.1] r(U)=u(r(D),r(I)). 118 [para_into,16.1.1.1,40.1.1,flip.1] u(r($c1),r(I))=r(I). 129 [para_into,18.1.1.1,38.1.1,flip.1] k(r($c1),r($c1))=r($c1). 131 [para_into,18.1.1.1,23.1.1,flip.1] k(r(I),r(x))=r(x). 148 [para_into,21.1.1.1,38.1.1] u($c1,k(x,$c1))=k(u($c1,x),$c1). 150 [para_into,21.1.1.2,38.1.1] u(k(x,$c1),$c1)=k(u(x,$c1),$c1). 153 [para_from,21.1.1,16.1.1.1,demod,19,17,19,19,flip.1] u(k(r(x),r(y)),k(r(x),r(z)))=k(r(x),u(r(y),r(z))). 155 [para_from,21.1.1,9.1.1.1.1.1] c(u(c(k(u(x,y),z)),c(u(k(x,z),c(k(y,z))))))=k(x,z). 177 [para_into,25.1.1.1.2.1,23.1.1,demod,29,29] u(k(r(x),c(x)),D)=D. 181 [para_into,25.1.1.2,34.1.1,demod,35] u(k(r(x),c(k(x,U))),Z)=Z. 189 [para_from,25.1.1,16.1.1.1,demod,19,15,flip.1] u(k(r(c(k(x,y))),x),r(c(y)))=r(c(y)). 193 [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). 195 [para_from,129.1.1,21.1.1.2] u(k(x,r($c1)),r($c1))=k(u(x,r($c1)),r($c1)). 209 [para_into,131.1.1.2,14.1.1,demod,15] k(r(I),x)=x. 212,211 [para_into,209.1.1,23.1.1] r(I)=I. 214,213 [back_demod,209,demod,212] k(I,x)=x. 228 [back_demod,118,demod,212,212] u(r($c1),I)=I. 230 [back_demod,116,demod,212] r(U)=u(r(D),I). 232 [back_demod,112,demod,212,212] u(I,r($c1))=I. 234 [para_from,211.1.1,25.1.1.1.1,demod,214,214] u(c(x),c(x))=c(x). 237 [para_into,44.1.1.2,67.1.1] u(x,U)=u(D,u(x,I)). 238 [para_into,44.1.1.2,31.1.1] u(x,U)=u(I,u(x,D)). 243 [copy,237,flip.1] u(D,u(x,I))=u(x,U). 244 [copy,238,flip.1] u(I,u(x,D))=u(x,U). 245 [para_from,44.1.1,9.1.1.1.1.1] c(u(c(u(x,u(y,z))),c(u(y,c(u(x,z))))))=y. 248,247 [para_from,213.1.1,21.1.1.2] u(k(x,y),y)=k(u(x,I),y). 249 [para_from,213.1.1,21.1.1.1] u(x,k(y,x))=k(u(I,y),x). 250 [back_demod,195,demod,248,flip.1] k(u(x,r($c1)),r($c1))=k(u(x,I),r($c1)). 252 [back_demod,150,demod,248] k(u(x,I),$c1)=k(u(x,$c1),$c1). 254 [copy,249,flip.1] k(u(I,x),y)=u(y,k(x,y)). 276,275 [para_into,234.1.1.1,9.1.1,demod,10,10] u(x,x)=x. 293 [para_into,275.1.1,71.1.1] u(I,u(D,U))=U. 297 [para_into,275.1.1,44.1.1,demod,8,276] u(x,u(x,y))=u(x,y). 302,301 [para_from,275.1.1,46.1.1.2,flip.1] u(x,u(y,x))=u(y,x). 318,317 [para_into,293.1.1.2,5.1.1,demod,72,276,32] u(I,U)=U. 320,319 [para_into,293.1.1,45.1.1,demod,72,68,318] u(D,U)=U. 350 [para_into,49.1.1.1.1.1.2,5.1.1] c(u(c(u(x,u(y,z))),c(u(x,u(z,c(y))))))=u(x,z). 358 [para_into,49.1.1.1.1.1,45.1.1] c(u(c(u(x,u(y,z))),c(u(z,u(x,c(y))))))=u(z,x). 372 [para_into,49.1.1.1.2.1.2,5.1.1] c(u(c(u(x,u(y,z))),c(u(x,u(c(z),y)))))=u(x,y). 403,402 [para_into,51.1.1.1.1.1,317.1.1,demod,35,29,72,276,32,35,276] c(Z)=U. 428 [para_into,51.1.1.1.2.1.2,51.1.1,demod,8] c(u(c(u(c(u(x,y)),u(c(u(y,c(x))),z))),c(u(z,y))))=z. 432 [para_into,51.1.1.1.2.1.2,9.1.1,demod,8] c(u(c(u(c(u(x,y)),u(c(u(x,c(y))),z))),c(u(z,x))))=z. 440 [para_into,51.1.1.1.2.1,5.1.1] c(u(c(u(x,y)),c(u(c(x),y))))=y. 602,601 [para_into,55.1.1.1.2.1,275.1.1,demod,403] c(u(c(u(Z,U)),U))=Z. 661 [para_into,57.1.1.1.1.1,275.1.1,demod,29,32,35] c(u(D,Z))=I. 668,667 [para_into,57.1.1.1,5.1.1] c(u(c(u(x,D)),c(u(x,I))))=x. 687 [para_into,661.1.1.1,5.1.1] c(u(Z,D))=I. 699 [para_from,661.1.1,9.1.1.1.1,demod,403,320,35] c(u(I,Z))=D. 880 [para_into,177.1.1.1.2,699.1.1,demod,17,212,248,8,302] k(u(r(Z),I),D)=D. 883,882 [para_into,177.1.1.1.2,687.1.1,demod,17,24,8] u(r(Z),u(r(D),D))=D. 900 [para_into,177.1.1.1.2,57.1.1,demod,17] u(k(u(r(c(u(x,I))),r(c(u(x,D)))),x),D)=D. 978 [para_into,61.1.1.1.1.1,46.1.1] c(u(c(u(x,u(y,z))),c(u(c(u(z,x)),y))))=y. 1052 [para_into,61.1.1.1,5.1.1] c(u(c(u(c(x),y)),c(u(y,x))))=y. 1157 [para_into,880.1.1.1,5.1.1] k(u(I,r(Z)),D)=D. 1161 [para_from,880.1.1,25.1.1.1.2.1,demod,17,15,212,248,8,276] k(u(Z,I),c(D))=c(D). 1263 [para_into,65.1.1.1.2.1,275.1.1] c(u(c(u(x,c(x))),c(x)))=x. 1653 [hyper,297,2] i(x,u(x,y)). 1702 [para_into,1653.1.2,5.1.1] i(x,u(y,x)). 1745 [para_into,1702.1.2,21.1.1] i(k(x,y),k(u(z,x),y)). 1933 [para_from,148.1.1,45.1.1.2] u(x,k(u($c1,y),$c1))=u($c1,u(k(y,$c1),x)). 1951 [copy,1933,flip.1] u($c1,u(k(x,$c1),y))=u(y,k(u($c1,x),$c1)). 2010 [para_into,153.1.1.1.2,211.1.1,demod,24,212] u(r(x),k(r(x),r(y)))=k(r(x),u(I,r(y))). 2049 [para_into,155.1.1.1.1.1.1,237.1.1] c(u(c(k(u(D,u(x,I)),y)),c(u(k(x,y),c(k(U,y))))))=k(x,y). 2650 [para_into,601.1.1.1.1.1,237.1.1] c(u(c(u(D,u(Z,I))),U))=Z. 2676 [para_from,601.1.1,25.1.1.2,demod,602] u(k(r(x),c(k(x,u(c(u(Z,U)),U)))),Z)=Z. 2866 [para_into,882.1.1.2,5.1.1] u(r(Z),u(D,r(D)))=D. 2875,2874 [para_from,882.1.1,301.1.1.2,demod,8,276,883] u(r(D),D)=D. 2895 [para_from,882.1.1,16.1.1.1,demod,15,2875,flip.1] u(Z,r(D))=r(D). 2897 [para_from,882.1.1,65.1.1.1.2.1,demod,2875] c(u(c(u(r(Z),c(D))),c(D)))=r(Z). 2912,2911 [para_from,882.1.1,7.1.1.1,demod,2875,flip.1] u(r(Z),u(D,x))=u(D,x). 2918,2917 [back_demod,2866,demod,2912] u(D,r(D))=D. 2935 [para_from,181.1.1,44.1.1.2,flip.1] u(k(r(x),c(k(x,U))),u(y,Z))=u(y,Z). 2972,2971 [para_from,2874.1.1,16.1.1.1,demod,15,2918] r(D)=D. 2978,2977 [back_demod,2895,demod,2972,2972] u(Z,D)=D. 3032,3031 [back_demod,230,demod,2972,68] r(U)=U. 3049,3048 [back_demod,687,demod,2978] c(D)=I. 3062 [back_demod,2897,demod,3049,3049] c(u(c(u(r(Z),I)),I))=r(Z). 3134,3133 [back_demod,1161,demod,3049,24,3049] u(Z,I)=I. 3158,3157 [back_demod,2650,demod,3134,68,35] c(u(Z,U))=Z. 3166 [back_demod,2676,demod,3158] u(k(r(x),c(k(x,u(Z,U)))),Z)=Z. 3324,3323 [para_from,2977.1.1,244.1.1.2,demod,32,flip.1] u(Z,U)=U. 3327,3326 [para_from,2977.1.1,49.1.1.1.1.1.2,demod,3049,3134,668,flip.1] u(x,Z)=x. 3346,3345 [back_demod,3166,demod,3324,3327] k(r(x),c(k(x,U)))=Z. 3378,3377 [back_demod,2935,demod,3346,3327,3327] u(Z,x)=x. 3653,3652 [para_from,3377.1.1,59.1.1.1.1.1,demod,10,3378] c(u(x,c(x)))=Z. 3665,3664 [back_demod,1263,demod,3653,3378] c(c(x))=x. 3886 [para_into,3664.1.1.1,75.1.1,flip.1] u(D,c(u($c1,D)))=c($c1). 3900 [para_into,3664.1.1.1,49.1.1,flip.1] u(c(u(x,u(y,z))),c(u(x,u(y,c(z)))))=c(u(x,y)). 3953,3952 [para_into,189.1.1.1.1.1.1,1157.1.1,demod,3049,212,214,3049,212,8,302,3049,212] u(r(Z),I)=I. 3971,3970 [back_demod,3062,demod,3953,29,68,35,flip.1] r(Z)=Z. 4223,4222 [para_from,3652.1.1,3664.1.1.1,demod,403,flip.1] u(x,c(x))=U. 4226 [para_into,4222.1.1.2,3664.1.1] u(c(x),x)=U. 4241 [para_from,4222.1.1,46.1.1.2] u(x,U)=u(c(y),u(x,y)). 4242 [para_from,4222.1.1,45.1.1.2] u(x,U)=u(y,u(c(y),x)). 4243 [para_from,4222.1.1,44.1.1.2,flip.1] u(x,u(y,c(x)))=u(y,U). 4247,4246 [para_from,4222.1.1,297.1.1.2,demod,4223] u(x,U)=U. 4250 [para_from,4222.1.1,16.1.1.1,demod,3032,flip.1] u(r(x),r(c(x)))=U. 4253,4252 [para_from,4222.1.1,7.1.1.1,demod,72,flip.1] u(x,u(c(x),y))=u(I,u(D,y)). 4264 [copy,4241,flip.1,demod,4247] u(c(x),u(y,x))=U. 4267,4266 [copy,4242,flip.1,demod,4253,4247] u(I,u(D,x))=U. 4268 [back_demod,4243,demod,4247] u(x,u(y,c(x)))=U. 4359,4358 [back_demod,243,demod,4247] u(D,u(x,I))=U. 4360 [back_demod,4252,demod,4267] u(x,u(c(x),y))=U. 4371,4370 [back_demod,71,demod,4267] u(U,x)=U. 4372 [back_demod,2049,demod,4359] c(u(c(k(U,x)),c(u(k(y,x),c(k(U,x))))))=k(y,x). 4392 [para_from,4226.1.1,45.1.1.2,demod,4247,flip.1] u(c(x),u(x,y))=U. 4396 [para_from,4226.1.1,16.1.1.1,demod,3032,flip.1] u(r(c(x)),r(x))=U. 4483 [para_into,245.1.1.1.1.1.2,4222.1.1,demod,4247,35,3378,3665] u(x,c(u(y,c(x))))=x. 4767 [para_from,250.1.1,18.1.1.1,demod,19,15,17,212,15,17,15] k($c1,u(r(x),I))=k($c1,u(r(x),$c1)). 4809 [para_into,252.1.1.1,4226.1.1,demod,29,flip.1] k(u(D,$c1),$c1)=k(U,$c1). 4830 [para_into,4250.1.1.1,14.1.1] u(x,r(c(r(x))))=U. 4874 [para_into,4268.1.1,193.1.1] u(c(x),c(k(r(y),c(k(y,x)))))=U. 4896 [para_into,254.1.1.1,232.1.1,demod,214,flip.1] u(x,k(r($c1),x))=x. 4902 [para_into,254.1.1.1,73.1.1,demod,214,flip.1] u(x,k($c1,x))=x. 4934 [para_from,4902.1.1,4264.1.1.2] u(c(k($c1,x)),x)=U. 5333 [para_into,4396.1.1.2,14.1.1] u(r(c(r(x))),x)=U. 5643 [para_from,4896.1.1,16.1.1.1,demod,19,15,flip.1] u(r(x),k(r(x),$c1))=r(x). 5703 [para_into,4934.1.1,5.1.1] u(x,c(k($c1,x)))=U. 5729 [para_into,350.1.1.1.1.1.2,4902.1.1] c(u(c(u(x,y)),c(u(x,u(k($c1,y),c(y))))))=u(x,k($c1,y)). 5905 [para_into,358.1.1.1.1.1.2,4896.1.1] c(u(c(u(x,y)),c(u(k(r($c1),y),u(x,c(y))))))=u(k(r($c1),y),x). 5959 [para_into,358.1.1.1.1.1,4226.1.1,demod,35,3378,3665] u(x,u(c(u(y,x)),c(y)))=u(x,c(u(y,x))). 6192,6191 [para_into,372.1.1.1.1.1.2,4392.1.1,demod,4247,35,3378,3665] u(x,u(c(u(y,z)),c(y)))=u(x,c(y)). 6198,6197 [para_into,372.1.1.1.1.1.2,4360.1.1,demod,4247,35,3378,3665] u(x,u(c(u(c(y),z)),y))=u(x,y). 6282,6281 [back_demod,5959,demod,6192,flip.1] u(x,c(u(y,x)))=u(x,c(y)). 6313 [back_demod,4372,demod,6282] c(u(c(k(U,x)),c(k(y,x))))=k(y,x). 6316,6315 [back_demod,3886,demod,6282] u(D,c($c1))=c($c1). 6996 [para_into,428.1.1.1.2.1,5703.1.1,demod,35,3327,3665] u(c(u(x,c(k($c1,y)))),u(c(u(c(k($c1,y)),c(x))),y))=y. 7037,7036 [para_into,428.1.1.1.2.1,4222.1.1,demod,6198,35,3327,3665] u(c(u(x,c(y))),y)=y. 7246 [para_into,432.1.1.1.2.1,4226.1.1,demod,6192,35,3327,3665] u(c(u(x,y)),c(x))=c(x). 7299 [para_into,440.1.1.1.1.1,5333.1.1,demod,35,3378,3665] u(c(r(c(r(x)))),x)=x. 8953 [para_from,4483.1.1,1745.1.2.1] i(k(c(u(x,c(y))),z),k(y,z)). 9845 [para_into,4809.1.1.1,5.1.1] k(u($c1,D),$c1)=k(U,$c1). 10295,10294 [para_into,978.1.1.1.1.1.2,5703.1.1,demod,4247,35,3378,3665] u(c(u(c(k($c1,x)),y)),x)=x. 10446 [back_demod,6996,demod,10295] u(c(u(x,c(k($c1,y)))),y)=y. 11188,11187 [para_into,1052.1.1.1.1.1,4830.1.1,demod,35,3378,3665] u(r(c(r(c(x)))),x)=r(c(r(c(x)))). 13591 [para_from,7299.1.1,16.1.1.1,demod,11188,flip.1] r(c(r(c(r(x)))))=r(x). 16014,16013 [para_from,9845.1.1,21.1.1.1,demod,22,4371,8,flip.1] k(u($c1,u(D,x)),$c1)=k(U,$c1). 16409 [para_into,1951.1.1.2,900.1.1,demod,41,29,2972,16014,flip.1] u(D,k(U,$c1))=u($c1,D). 16483 [para_into,13591.1.1.1.1.1.1,14.1.1,demod,15] r(c(r(c(x))))=x. 16485 [para_into,16483.1.1.1.1.1,3664.1.1] r(c(r(x)))=c(x). 16490,16489 [para_into,16485.1.1.1.1,14.1.1] r(c(x))=c(r(x)). 16630 [para_from,2010.1.1,1653.1.2] i(r(x),k(r(x),u(I,r(y)))). 16902 [para_into,5643.1.1.1,14.1.1,demod,15,15] u(x,k(x,$c1))=x. 16907,16906 [para_into,16902.1.1,5.1.1] u(k(x,$c1),x)=x. 16920 [para_from,16902.1.1,4264.1.1.2] u(c(k(x,$c1)),x)=U. 17004 [para_into,16920.1.1,5.1.1] u(x,c(k(x,$c1)))=U. 17716 [para_into,16630.1.2.2.2,3031.1.1,demod,4247] i(r(x),k(r(x),U)). 17719 [para_into,17716.1.1,14.1.1,demod,15] i(x,k(x,U)). 17720 [hyper,17719,1] u(x,k(x,U))=k(x,U). 17816,17815 [para_from,17720.1.1,7246.1.1.1.1] u(c(k(x,U)),c(x))=c(x). 17876 [para_into,4767.1.1.2.1,2971.1.1,demod,68,2972,flip.1] k($c1,u(D,$c1))=k($c1,U). 17878 [para_into,4767.1.1.2,228.1.1,demod,24,flip.1] k($c1,u(r($c1),$c1))=$c1. 17933 [para_from,17876.1.1,4934.1.1.1.1] u(c(k($c1,U)),u(D,$c1))=U. 18268 [para_from,17933.1.1,3900.1.1.1.1,demod,35,6316,17816,3665,3378,flip.1] c(u(c(k($c1,U)),D))=$c1. 18270 [para_into,18268.1.1.1,5.1.1] c(u(D,c(k($c1,U))))=$c1. 18275,18274 [para_from,18270.1.1,3664.1.1.1,flip.1] u(D,c(k($c1,U)))=c($c1). 18808 [para_into,6313.1.1.1,17004.1.1,demod,35,flip.1] k(c(k(U,$c1)),$c1)=Z. 18821 [para_from,18808.1.1,8953.1.2,demod,3665] i(k(c(u(x,k(U,$c1))),$c1),Z). 18848 [hyper,18821,1,demod,3327] k(c(u(x,k(U,$c1))),$c1)=Z. 18856 [para_into,18848.1.1.1.1,16409.1.1] k(c(u($c1,D)),$c1)=Z. 18866 [para_from,18856.1.1,18.1.1.1,demod,3971,16490,17,2972,flip.1] k(r($c1),c(u(r($c1),D)))=Z. 18890 [para_from,18866.1.1,4874.1.1.2.1.2.1,demod,3665,15,403,8,18275] u(r($c1),c($c1))=U. 18909,18908 [para_from,18890.1.1,5905.1.1.1.2.1.2,demod,4247,35,3327,3665,16907] u(r($c1),$c1)=r($c1). 18923,18922 [para_from,18890.1.1,16.1.1.1,demod,3032,15,16490,flip.1] u($c1,c(r($c1)))=U. 18926,18925 [back_demod,17878,demod,18909] k($c1,r($c1))=$c1. 18940,18939 [para_from,18925.1.1,5729.1.1.1.2.1.2.1,demod,18923,4247,35,3327,3665,18926] u(x,r($c1))=u(x,$c1). 18942 [para_from,18925.1.1,10446.1.1.1.1.2.1,demod,18940,7037,flip.1] r($c1)=$c1. 18944 [binary,18942.1,4.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 4365 clauses generated 1548828 clauses kept 12433 clauses forward subsumed 780290 clauses back subsumed 441 Kbytes malloced 12070 ----------- times (seconds) ----------- user CPU time 40.34 (0 hr, 0 min, 40 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 41 (0 hr, 0 min, 41 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 29 23:57:36 2003