----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sat Nov 29 23:55:43 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)). end_of_list. -------> usable clausifies to: list(usable). 0 [] i($c1,I). 0 [] k($c1,$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=5): 3 [] k($c1,$c1)!=$c1. ------------> process sos: ** KEPT (pick-wt=7): 4 [] u(x,y)=u(y,x). ** KEPT (pick-wt=11): 6 [copy,5,flip.1] u(u(x,y),z)=u(x,u(y,z)). ---> New Demodulator: 7 [new_demod,6] u(u(x,y),z)=u(x,u(y,z)). ** KEPT (pick-wt=13): 8 [] c(u(c(u(x,y)),c(u(x,c(y)))))=x. ---> New Demodulator: 9 [new_demod,8] c(u(c(u(x,y)),c(u(x,c(y)))))=x. ** KEPT (pick-wt=11): 11 [copy,10,flip.1] k(k(x,y),z)=k(x,k(y,z)). ---> New Demodulator: 12 [new_demod,11] k(k(x,y),z)=k(x,k(y,z)). ** KEPT (pick-wt=5): 13 [] r(r(x))=x. ---> New Demodulator: 14 [new_demod,13] r(r(x))=x. ** KEPT (pick-wt=10): 15 [] r(u(x,y))=u(r(x),r(y)). ---> New Demodulator: 16 [new_demod,15] r(u(x,y))=u(r(x),r(y)). ** KEPT (pick-wt=10): 17 [] r(k(x,y))=k(r(y),r(x)). ---> New Demodulator: 18 [new_demod,17] r(k(x,y))=k(r(y),r(x)). ** KEPT (pick-wt=13): 20 [copy,19,flip.1] u(k(x,y),k(z,y))=k(u(x,z),y). ---> New Demodulator: 21 [new_demod,20] u(k(x,y),k(z,y))=k(u(x,z),y). ** KEPT (pick-wt=5): 22 [] k(x,I)=x. ---> New Demodulator: 23 [new_demod,22] k(x,I)=x. ** KEPT (pick-wt=13): 24 [] u(k(r(x),c(k(x,y))),c(y))=c(y). ---> New Demodulator: 25 [new_demod,24] u(k(r(x),c(k(x,y))),c(y))=c(y). ** KEPT (pick-wt=4): 27 [copy,26,flip.1] c(I)=D. ---> New Demodulator: 28 [new_demod,27] c(I)=D. ** KEPT (pick-wt=5): 30 [copy,29,flip.1] u(I,D)=U. ---> New Demodulator: 31 [new_demod,30] u(I,D)=U. ** KEPT (pick-wt=4): 33 [copy,32,flip.1] c(U)=Z. ---> New Demodulator: 34 [new_demod,33] c(U)=Z. ** KEPT (pick-wt=3): 35 [] i($c1,I). Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] u(x,y)=u(y,x). >>>> Starting back demodulation with 7. >>>> Starting back demodulation with 9. >>>> Starting back demodulation with 12. >>>> Starting back demodulation with 14. >>>> Starting back demodulation with 16. >>>> Starting back demodulation with 18. >>>> Starting back demodulation with 21. >>>> Starting back demodulation with 23. >>>> Starting back demodulation with 25. >>>> Starting back demodulation with 28. >>>> Starting back demodulation with 31. >>>> Starting back demodulation with 34. ======= end of input processing ======= =========== start of search =========== Resetting weight limit to 10. sos_size=6633 ----> UNIT CONFLICT at 55.62 sec ----> 19584 [binary,19582.1,3.1] $F. Length of proof is 196. Level of proof is 41. ---------------- PROOF ---------------- 1 [] -i(x,y)|u(x,y)=y. 2 [] i(x,y)|u(x,y)!=y. 3 [] k($c1,$c1)!=$c1. 4 [] u(x,y)=u(y,x). 5 [] u(x,u(y,z))=u(u(x,y),z). 7,6 [copy,5,flip.1] u(u(x,y),z)=u(x,u(y,z)). 9,8 [] c(u(c(u(x,y)),c(u(x,c(y)))))=x. 10 [] k(x,k(y,z))=k(k(x,y),z). 12,11 [copy,10,flip.1] k(k(x,y),z)=k(x,k(y,z)). 14,13 [] r(r(x))=x. 16,15 [] r(u(x,y))=u(r(x),r(y)). 18,17 [] r(k(x,y))=k(r(y),r(x)). 19 [] k(u(x,y),z)=u(k(x,z),k(y,z)). 20 [copy,19,flip.1] u(k(x,y),k(z,y))=k(u(x,z),y). 23,22 [] k(x,I)=x. 24 [] u(k(r(x),c(k(x,y))),c(y))=c(y). 26 [] D=c(I). 28,27 [copy,26,flip.1] c(I)=D. 29 [] U=u(I,D). 31,30 [copy,29,flip.1] u(I,D)=U. 32 [] Z=c(U). 34,33 [copy,32,flip.1] c(U)=Z. 35 [] i($c1,I). 37 [hyper,35,1] u($c1,I)=I. 41 [para_into,6.1.1.1,4.1.1,demod,7] u(x,u(y,z))=u(y,u(x,z)). 42 [para_into,6.1.1,4.1.1] u(x,u(y,z))=u(y,u(z,x)). 43 [copy,42,flip.1] u(x,u(y,z))=u(z,u(x,y)). 46 [para_into,8.1.1.1.1.1,6.1.1,demod,7] c(u(c(u(x,u(y,z))),c(u(x,u(y,c(z))))))=u(x,y). 48 [para_into,8.1.1.1.1.1,4.1.1] c(u(c(u(x,y)),c(u(y,c(x)))))=y. 52 [para_into,8.1.1.1.2.1.2,33.1.1] c(u(c(u(x,U)),c(u(x,Z))))=x. 54 [para_into,8.1.1.1.2.1.2,27.1.1] c(u(c(u(x,I)),c(u(x,D))))=x. 56 [para_into,8.1.1.1.2.1.2,8.1.1] c(u(c(u(x,u(c(u(y,z)),c(u(y,c(z)))))),c(u(x,y))))=x. 58 [para_into,8.1.1.1.2.1,4.1.1] c(u(c(u(x,y)),c(u(c(y),x))))=x. 62 [para_into,8.1.1.1,4.1.1] c(u(c(u(x,c(y))),c(u(x,y))))=x. 65,64 [para_into,30.1.1,4.1.1] u(D,I)=U. 69,68 [para_from,30.1.1,6.1.1.1] u(U,x)=u(I,u(D,x)). 71,70 [para_into,37.1.1,4.1.1] u(I,$c1)=I. 72 [para_from,37.1.1,8.1.1.1.1.1,demod,28,28] c(u(D,c(u($c1,D))))=$c1. 80 [para_from,70.1.1,6.1.1.1,flip.1] u(I,u($c1,x))=u(I,x). 86 [para_into,72.1.1.1.2.1,4.1.1] c(u(D,c(u(D,$c1))))=$c1. 90 [para_from,72.1.1,8.1.1.1.2] c(u(c(u(D,u($c1,D))),$c1))=D. 109 [para_into,15.1.1.1,70.1.1,flip.1] u(r(I),r($c1))=r(I). 113 [para_into,15.1.1.1,64.1.1] r(U)=u(r(D),r(I)). 115 [para_into,15.1.1.1,37.1.1,flip.1] u(r($c1),r(I))=r(I). 130 [para_into,17.1.1.1,22.1.1,flip.1] k(r(I),r(x))=r(x). 143 [para_from,109.1.1,6.1.1.1,flip.1] u(r(I),u(r($c1),x))=u(r(I),x). 148 [para_from,20.1.1,8.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). 161 [para_into,130.1.1.2,13.1.1,demod,14] k(r(I),x)=x. 170 [para_into,24.1.1.1.1,13.1.1] u(k(x,c(k(r(x),y))),c(y))=c(y). 172 [para_into,24.1.1.1.2.1,22.1.1,demod,28,28] u(k(r(x),c(x)),D)=D. 176 [para_into,24.1.1.2,33.1.1,demod,34] u(k(r(x),c(k(x,U))),Z)=Z. 184 [para_from,24.1.1,15.1.1.1,demod,18,14,flip.1] u(k(r(c(k(x,y))),x),r(c(y)))=r(c(y)). 191,190 [para_into,161.1.1,22.1.1] r(I)=I. 195,194 [back_demod,161,demod,191] k(I,x)=x. 201 [back_demod,143,demod,191,191] u(I,u(r($c1),x))=u(I,x). 208,207 [back_demod,115,demod,191,191] u(r($c1),I)=I. 209 [back_demod,113,demod,191] r(U)=u(r(D),I). 211 [back_demod,109,demod,191,191] u(I,r($c1))=I. 213 [para_from,190.1.1,24.1.1.1.1,demod,195,195] u(c(x),c(x))=c(x). 216,215 [para_from,194.1.1,20.1.1.2] u(k(x,y),y)=k(u(x,I),y). 217 [para_from,194.1.1,20.1.1.1] u(x,k(y,x))=k(u(I,y),x). 218 [copy,217,flip.1] k(u(I,x),y)=u(y,k(x,y)). 220 [para_into,41.1.1.2,64.1.1] u(x,U)=u(D,u(x,I)). 221 [para_into,41.1.1.2,30.1.1] u(x,U)=u(I,u(x,D)). 226 [copy,220,flip.1] u(D,u(x,I))=u(x,U). 227 [copy,221,flip.1] u(I,u(x,D))=u(x,U). 228 [para_from,41.1.1,8.1.1.1.1.1] c(u(c(u(x,u(y,z))),c(u(y,c(u(x,z))))))=y. 242,241 [para_into,213.1.1.1,8.1.1,demod,9,9] u(x,x)=x. 258 [para_into,241.1.1,68.1.1] u(I,u(D,U))=U. 263,262 [para_into,241.1.1,41.1.1,demod,7,242] u(x,u(x,y))=u(x,y). 267,266 [para_from,241.1.1,41.1.1.2,flip.1] u(x,u(y,x))=u(y,x). 270 [back_demod,90,demod,267] c(u(c(u($c1,D)),$c1))=D. 293,292 [para_into,258.1.1.2,4.1.1,demod,69,242,31] u(I,U)=U. 294 [para_into,258.1.1,42.1.1,demod,69,65,293] u(D,U)=U. 307 [para_from,294.1.1,8.1.1.1.1.1,demod,34,34] c(u(Z,c(u(D,Z))))=D. 331 [para_into,46.1.1.1.1.1.2,37.1.1,demod,28] c(u(c(u(x,I)),c(u(x,u($c1,D)))))=u(x,$c1). 335 [para_into,46.1.1.1.1.1.2,4.1.1] c(u(c(u(x,u(y,z))),c(u(x,u(z,c(y))))))=u(x,z). 343 [para_into,46.1.1.1.1.1,42.1.1] c(u(c(u(x,u(y,z))),c(u(z,u(x,c(y))))))=u(z,x). 345 [para_into,46.1.1.1.1.1,41.1.1] c(u(c(u(x,u(y,z))),c(u(y,u(x,c(z))))))=u(y,x). 357 [para_into,46.1.1.1.2.1.2,4.1.1] c(u(c(u(x,u(y,z))),c(u(x,u(c(z),y)))))=u(x,y). 361 [para_into,46.1.1.1.2.1,43.1.1] c(u(c(u(x,u(y,z))),c(u(c(z),u(x,y)))))=u(x,y). 363 [para_into,46.1.1.1.2.1,42.1.1] c(u(c(u(x,u(y,z))),c(u(y,u(c(z),x)))))=u(x,y). 365 [para_into,46.1.1.1,4.1.1] c(u(c(u(x,u(y,c(z)))),c(u(x,u(y,z)))))=u(x,y). 392,391 [para_into,48.1.1.1.1.1,292.1.1,demod,34,28,69,242,31,34,242] c(Z)=U. 401 [para_into,48.1.1.1.1.1,20.1.1] c(u(c(k(u(x,y),z)),c(u(k(y,z),c(k(x,z))))))=k(y,z). 429 [para_into,48.1.1.1.2.1,4.1.1] c(u(c(u(x,y)),c(u(c(x),y))))=y. 477 [para_from,86.1.1,8.1.1.1.2,demod,263] c(u(c(u(D,$c1)),$c1))=D. 603,602 [para_into,52.1.1.1.2.1,241.1.1,demod,392] c(u(c(u(Z,U)),U))=Z. 643 [para_into,172.1.1.1.1,13.1.1] u(k(x,c(r(x))),D)=D. 689,688 [para_into,54.1.1.1.1.1,241.1.1,demod,28,31,34] c(u(D,Z))=I. 697,696 [para_into,54.1.1.1,4.1.1] c(u(c(u(x,D)),c(u(x,I))))=x. 700 [back_demod,307,demod,689] c(u(Z,I))=D. 718 [para_into,688.1.1.1,4.1.1] c(u(Z,D))=I. 721,720 [para_from,688.1.1,172.1.1.1.2,demod,16,23,7] u(r(D),u(r(Z),D))=D. 734 [para_from,700.1.1,172.1.1.1.2,demod,16,191,216,7,242] k(u(r(Z),I),D)=D. 1026 [para_into,58.1.1.1,4.1.1] c(u(c(u(c(x),y)),c(u(y,x))))=y. 1070 [para_into,734.1.1.1,4.1.1] k(u(I,r(Z)),D)=D. 1074 [para_from,734.1.1,24.1.1.1.2.1,demod,16,14,191,216,7,242] k(u(Z,I),c(D))=c(D). 1269 [para_into,62.1.1.1.2.1,241.1.1] c(u(c(u(x,c(x))),c(x)))=x. 1330 [para_from,62.1.1,48.1.1.1.2.1.2,demod,7] c(u(c(u(c(u(x,c(y))),u(c(u(x,y)),z))),c(u(z,x))))=z. 1595 [hyper,262,2] i(x,u(x,y)). 1607 [para_into,262.1.1.2,41.1.1] u(x,u(y,u(x,z)))=u(x,u(y,z)). 1669 [para_into,1595.1.2,43.1.1] i(x,u(y,u(x,z))). 1673 [para_into,1595.1.2,4.1.1] i(x,u(y,x)). 1687 [para_into,1673.1.2,20.1.1] i(k(x,y),k(u(z,x),y)). 1975 [para_into,148.1.1.1.1.1.1,220.1.1] c(u(c(k(u(D,u(x,I)),y)),c(u(k(x,y),c(k(U,y))))))=k(x,y). 2582 [para_into,602.1.1.1.1.1,220.1.1] c(u(c(u(D,u(Z,I))),U))=Z. 2606 [para_from,602.1.1,24.1.1.2,demod,603] u(k(r(x),c(k(x,u(c(u(Z,U)),U)))),Z)=Z. 2690 [para_from,170.1.1,1669.1.2.2] i(k(x,c(k(r(x),y))),u(z,c(y))). 2729 [para_from,643.1.1,43.1.1.2,flip.1] u(D,u(x,k(y,c(r(y)))))=u(x,D). 2842,2841 [para_from,720.1.1,266.1.1.2,demod,7,242,721] u(r(Z),D)=D. 2856,2855 [para_from,720.1.1,4.1.1,demod,2842,flip.1] u(D,r(D))=D. 2863,2862 [para_from,720.1.1,15.1.1.1,demod,14,2842,2856] r(D)=D. 2934,2933 [back_demod,209,demod,2863,65] r(U)=U. 2994,2993 [para_from,2841.1.1,15.1.1.1,demod,2863,14,2863,flip.1] u(Z,D)=D. 2995 [para_from,2841.1.1,62.1.1.1.2.1] c(u(c(u(r(Z),c(D))),c(D)))=r(Z). 3029,3028 [back_demod,718,demod,2994] c(D)=I. 3042 [back_demod,2995,demod,3029,3029] c(u(c(u(r(Z),I)),I))=r(Z). 3114,3113 [back_demod,1074,demod,3029,23,3029] u(Z,I)=I. 3150,3149 [back_demod,2582,demod,3114,65,34] c(u(Z,U))=Z. 3157 [back_demod,2606,demod,3150] u(k(r(x),c(k(x,u(Z,U)))),Z)=Z. 3188 [para_from,176.1.1,41.1.1.2,flip.1] u(k(r(x),c(k(x,U))),u(y,Z))=u(y,Z). 3212,3211 [para_from,2993.1.1,227.1.1.2,demod,31,flip.1] u(Z,U)=U. 3215,3214 [para_from,2993.1.1,46.1.1.1.1.1.2,demod,3029,3114,697,flip.1] u(x,Z)=x. 3232,3231 [back_demod,3157,demod,3212,3215] k(r(x),c(k(x,U)))=Z. 3240,3239 [back_demod,3188,demod,3232,3215,3215] u(Z,x)=x. 3564,3563 [para_from,3239.1.1,56.1.1.1.1.1,demod,9,3240] c(u(x,c(x)))=Z. 3576,3575 [back_demod,1269,demod,3564,3240] c(c(x))=x. 3773 [para_into,3575.1.1.1,477.1.1,demod,3029,flip.1] u(c(u(D,$c1)),$c1)=I. 3777 [para_into,3575.1.1.1,270.1.1,demod,3029,flip.1] u(c(u($c1,D)),$c1)=I. 3791 [para_into,3575.1.1.1,72.1.1,flip.1] u(D,c(u($c1,D)))=c($c1). 3889,3888 [para_into,184.1.1.1.1.1.1,1070.1.1,demod,3029,191,195,3029,191,7,267,3029,191] u(r(Z),I)=I. 3903,3902 [back_demod,3042,demod,3889,28,65,34,flip.1] r(Z)=Z. 4123,4122 [para_from,3563.1.1,3575.1.1.1,demod,392,flip.1] u(x,c(x))=U. 4126 [para_into,4122.1.1.2,3575.1.1] u(c(x),x)=U. 4139 [para_from,4122.1.1,201.1.1.2,demod,293,flip.1] u(I,c(r($c1)))=U. 4143 [para_from,4122.1.1,43.1.1.2] u(x,U)=u(c(y),u(x,y)). 4149,4148 [para_from,4122.1.1,262.1.1.2,demod,4123] u(x,U)=U. 4152 [para_from,4122.1.1,15.1.1.1,demod,2934,flip.1] u(r(x),r(c(x)))=U. 4166 [copy,4143,flip.1,demod,4149] u(c(x),u(y,x))=U. 4263,4262 [back_demod,226,demod,4149] u(D,u(x,I))=U. 4276 [back_demod,1975,demod,4263] c(u(c(k(U,x)),c(u(k(y,x),c(k(U,x))))))=k(y,x). 4348 [para_from,4126.1.1,42.1.1.2,demod,4149,flip.1] u(c(x),u(x,y))=U. 4352 [para_from,4126.1.1,15.1.1.1,demod,2934,flip.1] u(r(c(x)),r(x))=U. 4388 [para_into,218.1.1.1,4148.1.1,flip.1] u(x,k(U,x))=k(U,x). 4396 [para_into,218.1.1.1,211.1.1,demod,195,flip.1] u(x,k(r($c1),x))=x. 4402 [para_into,218.1.1.1,70.1.1,demod,195,flip.1] u(x,k($c1,x))=x. 4447 [para_from,4139.1.1,218.1.1.1,flip.1] u(x,k(c(r($c1)),x))=k(U,x). 4531,4530 [para_into,228.1.1.1.1.1.2,4126.1.1,demod,4149,34,3240,3576] u(c(x),c(u(y,x)))=c(x). 4532 [para_into,228.1.1.1.1.1.2,4122.1.1,demod,4149,34,3240,3576] u(x,c(u(y,c(x))))=x. 4658 [para_from,4402.1.1,80.1.1.2,demod,71,flip.1] u(I,k($c1,$c1))=I. 4684 [para_into,4658.1.1,4.1.1] u(k($c1,$c1),I)=I. 4998 [para_into,4152.1.1.1,13.1.1] u(x,r(c(r(x))))=U. 5012 [para_into,4166.1.1.2,4658.1.1] u(c(k($c1,$c1)),I)=U. 5248,5247 [para_into,331.1.1.1,4.1.1] c(u(c(u(x,u($c1,D))),c(u(x,I))))=u(x,$c1). 5345 [para_into,335.1.1.1,4.1.1] c(u(c(u(x,u(y,c(z)))),c(u(x,u(z,y)))))=u(x,y). 5465 [para_into,4352.1.1.2,13.1.1] u(r(c(r(x))),x)=U. 5517 [para_into,343.1.1.1.1.1,4126.1.1,demod,34,3240,3576] u(x,u(c(u(y,x)),c(y)))=u(x,c(u(y,x))). 5555 [para_from,4396.1.1,43.1.1.2,flip.1] u(k(r($c1),x),u(y,x))=u(y,x). 5562 [para_from,4396.1.1,15.1.1.1,demod,18,14,flip.1] u(r(x),k(r(x),$c1))=r(x). 5605 [para_into,345.1.1.1.1.1.2,3777.1.1] c(u(c(u(x,I)),c(u(c(u($c1,D)),u(x,c($c1))))))=u(c(u($c1,D)),x). 5635 [para_into,345.1.1.1.1.1,4126.1.1,demod,34,3240,3576] u(x,u(c(u(x,y)),c(y)))=u(x,c(u(x,y))). 5744,5743 [para_into,357.1.1.1.1.1.2,4348.1.1,demod,4149,34,3240,3576] u(x,u(c(u(y,z)),c(y)))=u(x,c(y)). 5766,5765 [para_into,357.1.1.1.1.1.2,4166.1.1,demod,4149,34,3240,3576] u(x,u(c(u(y,z)),c(z)))=u(x,c(z)). 5776,5775 [para_into,357.1.1.1.1.1.2,3773.1.1,demod,4531] c(u(c(u(x,I)),c(u(x,c($c1)))))=u(x,c(u(D,$c1))). 5824,5823 [back_demod,5517,demod,5744,flip.1] u(x,c(u(y,x)))=u(x,c(y)). 5826,5825 [back_demod,5635,demod,5766,flip.1] u(x,c(u(x,y)))=u(x,c(y)). 5853 [back_demod,4276,demod,5824] c(u(c(k(U,x)),c(k(y,x))))=k(y,x). 5858,5857 [back_demod,3791,demod,5824] u(D,c($c1))=c($c1). 5919,5918 [para_into,361.1.1.1.1.1.2,4348.1.1,demod,4149,34,3240,3576] u(c(u(x,y)),u(z,c(x)))=u(z,c(x)). 5994 [back_demod,5605,demod,5919,5776] u(x,c(u(D,$c1)))=u(c(u($c1,D)),x). 6009 [copy,5994,flip.1] u(c(u($c1,D)),x)=u(x,c(u(D,$c1))). 6105 [para_into,363.1.1.1.2.1.2,4396.1.1] c(u(c(u(k(r($c1),c(x)),u(y,x))),c(u(y,c(x)))))=u(k(r($c1),c(x)),y). 6145 [para_into,5012.1.1,4.1.1] u(I,c(k($c1,$c1)))=U. 6169 [para_into,365.1.1.1.2.1.2,4684.1.1,demod,28] c(u(c(u(x,u(k($c1,$c1),D))),c(u(x,I))))=u(x,k($c1,$c1)). 6584 [para_into,401.1.1.1.1.1.1,4126.1.1] c(u(c(k(U,x)),c(u(k(y,x),c(k(c(y),x))))))=k(y,x). 7050 [para_from,6145.1.1,218.1.1.1,flip.1] u(x,k(c(k($c1,$c1)),x))=k(U,x). 7069 [para_into,429.1.1.1.1.1,5465.1.1,demod,34,3240,3576] u(c(r(c(r(x)))),x)=x. 8747 [para_from,4388.1.1,4348.1.1.2] u(c(x),k(U,x))=U. 8963 [para_into,8747.1.1,4.1.1] u(k(U,x),c(x))=U. 9039 [para_from,8963.1.1,15.1.1.1,demod,2934,18,2934,flip.1] u(k(r(x),U),r(c(x)))=U. 9342 [para_from,4532.1.1,1687.1.2.1] i(k(c(u(x,c(y))),z),k(y,z)). 10458,10457 [para_into,1026.1.1.1.1.1,4998.1.1,demod,34,3240,3576] u(r(c(r(c(x)))),x)=r(c(r(c(x)))). 12499 [para_into,1330.1.1.1.2.1,4684.1.1,demod,28] c(u(c(u(c(u(I,c(x))),u(c(u(I,x)),k($c1,$c1)))),D))=k($c1,$c1). 12526,12525 [para_into,1330.1.1.1.2.1,37.1.1,demod,28] c(u(c(u(c(u(I,c(x))),u(c(u(I,x)),$c1))),D))=$c1. 13128 [para_from,7069.1.1,15.1.1.1,demod,10458,flip.1] r(c(r(c(r(x)))))=r(x). 16598 [para_into,13128.1.1.1.1.1.1,13.1.1,demod,14] r(c(r(c(x))))=x. 16600 [para_into,16598.1.1.1.1.1,3575.1.1] r(c(r(x)))=c(x). 16604,16603 [para_into,16600.1.1.1.1,13.1.1] r(c(x))=c(r(x)). 16639 [back_demod,9039,demod,16604] u(k(r(x),U),c(r(x)))=U. 17052 [para_into,5562.1.1.1,13.1.1,demod,14,14] u(x,k(x,$c1))=x. 17057,17056 [para_into,17052.1.1,4.1.1] u(k(x,$c1),x)=x. 17070 [para_from,17052.1.1,4166.1.1.2] u(c(k(x,$c1)),x)=U. 17154 [para_into,17070.1.1,4.1.1] u(x,c(k(x,$c1)))=U. 17489,17488 [para_from,4447.1.1,2729.1.1.2,demod,16604,14,3576,16604,14,3576] u(D,k(U,$c1))=u($c1,D). 17746 [para_into,16639.1.1.1.1,13.1.1,demod,14] u(k(x,U),c(x))=U. 17759,17758 [para_from,17746.1.1,1607.1.1.2.2,demod,4149,4149,flip.1] u(k(x,U),u(y,c(x)))=U. 18672 [para_into,5853.1.1.1,17154.1.1,demod,34,flip.1] k(c(k(U,$c1)),$c1)=Z. 18903 [para_into,9342.1.2,18672.1.1,demod,3576] i(k(c(u(x,k(U,$c1))),$c1),Z). 18905 [hyper,18903,1,demod,3215] k(c(u(x,k(U,$c1))),$c1)=Z. 18911 [para_into,18905.1.1.1.1,17488.1.1] k(c(u($c1,D)),$c1)=Z. 18922 [para_from,18911.1.1,17.1.1.1,demod,3903,16604,16,2863,flip.1] k(r($c1),c(u(r($c1),D)))=Z. 18945 [para_from,18922.1.1,2690.1.1.2.1,demod,392,3576] i(k($c1,U),u(x,u(r($c1),D))). 18976 [para_into,18945.1.2,6009.1.1,demod,7,5826,5858] i(k($c1,U),u(r($c1),c($c1))). 18980 [hyper,18976,1,demod,17759,flip.1] u(r($c1),c($c1))=U. 18987,18986 [para_from,18980.1.1,6105.1.1.1.1.1.2,demod,3576,4149,34,3576,3240,3576,3576,17057] u(r($c1),$c1)=r($c1). 19011,19010 [para_from,18980.1.1,15.1.1.1,demod,2934,14,16604,flip.1] u($c1,c(r($c1)))=U. 19026,19025 [para_from,18986.1.1,5345.1.1.1.2.1.2,demod,19011,4149,34,3240,3576] u(x,r($c1))=u(x,$c1). 19041,19040 [para_from,18986.1.1,5555.1.1.2,demod,19026,216,208,195,18987,flip.1] r($c1)=$c1. 19374,19373 [para_into,6584.1.1.1.2.1.2.1,18672.1.1,demod,12,392,4149,34,3215,3576,12,flip.1] k(U,k($c1,$c1))=k(U,$c1). 19579,19578 [para_from,7050.1.1,2729.1.1.2,demod,16604,18,19041,19041,3576,19374,17489,16604,18,19041,19041,3576,flip.1] u(k($c1,$c1),D)=u($c1,D). 19581,19580 [back_demod,6169,demod,19579,5248,flip.1] u(x,k($c1,$c1))=u(x,$c1). 19582 [back_demod,12499,demod,19581,12526,flip.1] k($c1,$c1)=$c1. 19584 [binary,19582.1,3.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 5100 clauses generated 2047215 clauses kept 13130 clauses forward subsumed 968481 clauses back subsumed 363 Kbytes malloced 12198 ----------- times (seconds) ----------- user CPU time 55.82 (0 hr, 0 min, 55 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 56 (0 hr, 0 min, 56 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:56:39 2003