----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sun Nov 30 22:06:31 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,20). assign(max_distinct_vars,3). assign(max_literals,1). 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("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("booleanLaws.txt"). ------- start included file booleanLaws.txt------- include("1To4booleanLaws.txt"). ------- start included file 1To4booleanLaws.txt------- formula_list(usable). -(all x y z (i(x,u(y,z))->i(n(x,c(z)),y))). end_of_list. -------> usable clausifies to: list(usable). 0 [] i($c3,u($c2,$c1)). 0 [] -i(n($c3,c($c1)),$c2). end_of_list. ------- end included file 1To4booleanLaws.txt------- ------- end included file booleanLaws.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=6): 3 [] -i(n($c3,c($c1)),$c2). ------------> 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=14): 8 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ---> New Demodulator: 9 [new_demod,8] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ** KEPT (pick-wt=10): 11 [copy,10,flip.1] c(u(c(x),c(y)))=n(x,y). ---> New Demodulator: 12 [new_demod,11] c(u(c(x),c(y)))=n(x,y). ** KEPT (pick-wt=4): 14 [copy,13,flip.1] c(I)=D. ---> New Demodulator: 15 [new_demod,14] c(I)=D. ** KEPT (pick-wt=5): 17 [copy,16,flip.1] u(I,D)=U. ---> New Demodulator: 18 [new_demod,17] u(I,D)=U. ** KEPT (pick-wt=4): 20 [copy,19,flip.1] c(U)=Z. ---> New Demodulator: 21 [new_demod,20] c(U)=Z. ** KEPT (pick-wt=5): 22 [] i($c3,u($c2,$c1)). 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. >> back demodulating 8 with 12. >>>> Starting back demodulation with 15. >>>> Starting back demodulation with 18. >>>> Starting back demodulation with 21. >>>> Starting back demodulation with 24. ======= end of input processing ======= =========== start of search =========== Resetting weight limit to 13. sos_size=2611 Resetting weight limit to 12. sos_size=2345 Resetting weight limit to 11. sos_size=2390 Resetting weight limit to 10. sos_size=1633 Resetting weight limit to 9. sos_size=502 Resetting weight limit to 8. sos_size=553 ----> UNIT CONFLICT at 5.82 sec ----> 10437 [binary,10436.1,3.1] $F. Length of proof is 339. Level of proof is 51. ---------------- PROOF ---------------- 1 [] -i(x,y)|u(x,y)=y. 2 [] i(x,y)|u(x,y)!=y. 3 [] -i(n($c3,c($c1)),$c2). 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)). 8 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 10 [] n(x,y)=c(u(c(x),c(y))). 12,11 [copy,10,flip.1] c(u(c(x),c(y)))=n(x,y). 13 [] D=c(I). 15,14 [copy,13,flip.1] c(I)=D. 16 [] U=u(I,D). 18,17 [copy,16,flip.1] u(I,D)=U. 19 [] Z=c(U). 21,20 [copy,19,flip.1] c(U)=Z. 22 [] i($c3,u($c2,$c1)). 24,23 [back_demod,8,demod,12] u(c(u(c(x),y)),n(x,y))=x. 28 [para_into,6.1.1.1,4.1.1,demod,7] u(x,u(y,z))=u(y,u(x,z)). 29 [para_into,6.1.1,4.1.1] u(x,u(y,z))=u(y,u(z,x)). 30 [copy,29,flip.1] u(x,u(y,z))=u(z,u(x,y)). 33,32 [para_into,17.1.1,4.1.1] u(D,I)=U. 35,34 [para_from,17.1.1,6.1.1.1] u(U,x)=u(I,u(D,x)). 36 [hyper,22,1] u($c3,u($c2,$c1))=u($c2,$c1). 38 [para_into,22.1.2,4.1.1] i($c3,u($c1,$c2)). 40,39 [para_into,11.1.1.1.1,20.1.1] c(u(Z,c(x)))=n(U,x). 42,41 [para_into,11.1.1.1.1,14.1.1] c(u(D,c(x)))=n(I,x). 43 [para_into,11.1.1.1.1,11.1.1] c(u(n(x,y),c(z)))=n(u(c(x),c(y)),z). 45 [para_into,11.1.1.1.2,20.1.1] c(u(c(x),Z))=n(x,U). 48,47 [para_into,11.1.1.1.2,14.1.1] c(u(c(x),D))=n(x,I). 49 [para_into,11.1.1.1.2,11.1.1] c(u(c(x),n(y,z)))=n(x,u(c(y),c(z))). 51 [para_into,11.1.1.1,4.1.1,demod,12] n(x,y)=n(y,x). 53 [hyper,38,1] u($c3,u($c1,$c2))=u($c1,$c2). 57,56 [para_into,23.1.1.1.1.1,20.1.1] u(c(u(Z,x)),n(U,x))=U. 59,58 [para_into,23.1.1.1.1.1,14.1.1] u(c(u(D,x)),n(I,x))=I. 60 [para_into,23.1.1.1.1.1,11.1.1] u(c(u(n(x,y),z)),n(u(c(x),c(y)),z))=u(c(x),c(y)). 62 [para_into,23.1.1.1.1,23.1.1] u(c(x),n(u(c(x),y),n(x,y)))=u(c(x),y). 64 [para_into,23.1.1.1.1,4.1.1] u(c(u(x,c(y))),n(y,x))=y. 66 [para_into,23.1.1.1,11.1.1] u(n(x,y),n(x,c(y)))=x. 68 [para_into,23.1.1.2,51.1.1] u(c(u(c(x),y)),n(y,x))=x. 71 [para_into,23.1.1,4.1.1] u(n(x,y),c(u(c(x),y)))=x. 73 [para_from,23.1.1,6.1.1.1,flip.1] u(c(u(c(x),y)),u(n(x,y),z))=u(x,z). 75 [para_into,34.1.1,4.1.1] u(x,U)=u(I,u(D,x)). 76 [copy,75,flip.1] u(I,u(D,x))=u(x,U). 79 [para_from,36.1.1,6.1.1.1,demod,7,7,flip.1] u($c3,u($c2,u($c1,x)))=u($c2,u($c1,x)). 84,83 [para_into,39.1.1.1.2,20.1.1] c(u(Z,Z))=n(U,U). 85 [para_into,39.1.1.1.2,14.1.1] c(u(Z,D))=n(U,I). 88,87 [para_into,39.1.1.1.2,11.1.1] c(u(Z,n(x,y)))=n(U,u(c(x),c(y))). 94 [para_into,28.1.1.2,32.1.1] u(x,U)=u(D,u(x,I)). 95 [para_into,28.1.1.2,23.1.1,flip.1] u(c(u(c(x),y)),u(z,n(x,y)))=u(z,x). 97 [para_into,28.1.1.2,17.1.1] u(x,U)=u(I,u(x,D)). 101 [para_into,28.1.1,4.1.1,demod,7] u(x,u(y,z))=u(x,u(z,y)). 104 [para_from,28.1.1,23.1.1.1.1] u(c(u(x,u(c(y),z))),n(y,u(x,z)))=y. 106 [para_from,83.1.1,23.1.1.1.1.1] u(c(u(n(U,U),x)),n(u(Z,Z),x))=u(Z,Z). 109,108 [para_into,85.1.1.1,4.1.1] c(u(D,Z))=n(U,I). 116 [para_from,108.1.1,23.1.1.1.1.1] u(c(u(n(U,I),x)),n(u(D,Z),x))=u(D,Z). 127,126 [para_into,41.1.1.1.2,14.1.1] c(u(D,D))=n(I,I). 129,128 [para_into,41.1.1.1.2,11.1.1] c(u(D,n(x,y)))=n(I,u(c(x),c(y))). 133 [para_into,29.1.1.2,32.1.1] u(x,U)=u(D,u(I,x)). 134 [para_into,29.1.1.2,4.1.1] u(x,u(y,z))=u(z,u(y,x)). 137 [copy,133,flip.1] u(D,u(I,x))=u(x,U). 141 [para_from,126.1.1,23.1.1.1.1.1] u(c(u(n(I,I),x)),n(u(D,D),x))=u(D,D). 157 [para_from,45.1.1,23.1.1.1] u(n(x,U),n(x,Z))=x. 177 [para_from,47.1.1,23.1.1.1] u(n(x,I),n(x,D))=x. 181 [para_into,53.1.1,29.1.1] u($c1,u($c2,$c3))=u($c1,$c2). 205 [para_into,76.1.1.2,30.1.1,demod,7] u(I,u(x,u(D,y)))=u(y,u(x,U)). 207 [para_into,76.1.1.2,28.1.1,demod,7] u(I,u(x,u(D,y)))=u(x,u(y,U)). 210 [copy,207,flip.1] u(x,u(y,U))=u(I,u(x,u(D,y))). 224 [para_from,94.1.1,23.1.1.1.1] u(c(u(D,u(c(x),I))),n(x,U))=x. 281 [para_into,49.1.1.1,23.1.1,flip.1] n(u(c(x),y),u(c(x),c(y)))=c(x). 285 [para_into,133.1.1,6.1.1] u(x,u(y,U))=u(D,u(I,u(x,y))). 287 [para_from,133.1.1,23.1.1.1.1] u(c(u(D,u(I,c(x)))),n(x,U))=x. 297 [para_into,137.1.1.2,28.1.1,demod,7] u(D,u(x,u(I,y)))=u(x,u(y,U)). 300 [para_from,137.1.1,29.1.1.2,demod,7] u(x,u(y,U))=u(D,u(I,u(y,x))). 302 [copy,300,flip.1] u(D,u(I,u(x,y)))=u(y,u(x,U)). 303 [para_into,157.1.1.1,51.1.1] u(n(U,x),n(x,Z))=x. 305 [para_into,157.1.1.2,51.1.1] u(n(x,U),n(Z,x))=x. 309 [para_from,157.1.1,30.1.1.2,flip.1] u(n(x,Z),u(y,n(x,U)))=u(y,x). 312 [para_from,157.1.1,28.1.1.2,flip.1] u(n(x,U),u(y,n(x,Z)))=u(y,x). 315,314 [para_from,157.1.1,6.1.1.1,flip.1] u(n(x,U),u(n(x,Z),y))=u(x,y). 316 [para_into,177.1.1.1,51.1.1] u(n(I,x),n(x,D))=x. 318 [para_into,177.1.1.2,51.1.1] u(n(x,I),n(D,x))=x. 322 [para_from,177.1.1,30.1.1.2,flip.1] u(n(x,D),u(y,n(x,I)))=u(y,x). 325 [para_from,177.1.1,28.1.1.2,flip.1] u(n(x,I),u(y,n(x,D)))=u(y,x). 337 [para_into,56.1.1.1.1,30.1.1] u(c(u(x,u(Z,y))),n(U,u(y,x)))=U. 343 [para_into,56.1.1.1.1,4.1.1] u(c(u(x,Z)),n(U,x))=U. 345 [para_into,56.1.1.2,51.1.1] u(c(u(Z,x)),n(x,U))=U. 347 [para_into,56.1.1,4.1.1] u(n(U,x),c(u(Z,x)))=U. 349 [para_from,56.1.1,49.1.1.1,demod,21,21,flip.1] n(u(Z,x),u(Z,c(x)))=Z. 364 [para_from,181.1.1,6.1.1.1,demod,7,7,flip.1] u($c1,u($c2,u($c3,x)))=u($c1,u($c2,x)). 374 [para_into,303.1.1.2,51.1.1] u(n(U,x),n(Z,x))=x. 376 [para_into,303.1.1,4.1.1] u(n(x,Z),n(U,x))=x. 378 [para_from,303.1.1,30.1.1.2,flip.1] u(n(x,Z),u(y,n(U,x)))=u(y,x). 382,381 [para_from,303.1.1,28.1.1.2,flip.1] u(n(U,x),u(y,n(x,Z)))=u(y,x). 386,385 [para_into,305.1.1,4.1.1] u(n(Z,x),n(x,U))=x. 394 [para_into,58.1.1.1.1,137.1.1] u(c(u(x,U)),n(I,u(I,x)))=I. 401,400 [para_into,58.1.1.1.1,32.1.1,demod,21] u(Z,n(I,I))=I. 408 [para_into,58.1.1.1.1,4.1.1] u(c(u(x,D)),n(I,x))=I. 410 [para_into,58.1.1.2,51.1.1] u(c(u(D,x)),n(x,I))=I. 412 [para_into,58.1.1,4.1.1] u(n(I,x),c(u(D,x)))=I. 414 [para_from,58.1.1,49.1.1.1,demod,15,15,flip.1] n(u(D,x),u(D,c(x)))=D. 426,425 [para_into,400.1.1,4.1.1] u(n(I,I),Z)=I. 430,429 [para_from,400.1.1,30.1.1.2,flip.1] u(n(I,I),u(x,Z))=u(x,I). 432 [para_from,400.1.1,28.1.1.2,flip.1] u(Z,u(x,n(I,I)))=u(x,I). 438,437 [para_from,425.1.1,6.1.1.1,flip.1] u(n(I,I),u(Z,x))=u(I,x). 442 [para_into,316.1.1.2,51.1.1] u(n(I,x),n(D,x))=x. 444 [para_into,316.1.1,4.1.1] u(n(x,D),n(I,x))=x. 453 [para_into,60.1.1.1.1.1,51.1.1] u(c(u(n(x,y),z)),n(u(c(y),c(x)),z))=u(c(y),c(x)). 473 [para_into,60.1.1.1.1,4.1.1] u(c(u(x,n(y,z))),n(u(c(y),c(z)),x))=u(c(y),c(z)). 507 [para_from,60.1.1,49.1.1.1,demod,12,12,flip.1] n(u(n(x,y),z),u(n(x,y),c(z)))=n(x,y). 511 [para_into,318.1.1,4.1.1] u(n(D,x),n(x,I))=x. 527 [para_into,374.1.1,4.1.1] u(n(Z,x),n(U,x))=x. 570,569 [para_into,62.1.1.2.1,58.1.1,demod,59] u(c(u(D,x)),n(I,n(u(D,x),n(I,x))))=I. 572,571 [para_into,62.1.1.2.1,56.1.1,demod,57] u(c(u(Z,x)),n(U,n(u(Z,x),n(U,x))))=U. 579 [para_into,62.1.1.2.1,23.1.1,demod,24] u(c(u(c(x),y)),n(x,n(u(c(x),y),n(x,y))))=x. 601 [para_from,385.1.1,6.1.1.1,flip.1] u(n(Z,x),u(n(x,U),y))=u(x,y). 618 [para_into,442.1.1,4.1.1] u(n(D,x),n(I,x))=x. 646 [para_into,64.1.1.1.1.2,39.1.1] u(c(u(x,n(U,y))),n(u(Z,c(y)),x))=u(Z,c(y)). 650 [para_into,64.1.1.1,11.1.1] u(n(x,y),n(y,c(x)))=y. 652 [para_into,64.1.1.2,51.1.1] u(c(u(x,c(y))),n(x,y))=y. 654 [para_into,64.1.1,4.1.1] u(n(x,y),c(u(y,c(x))))=x. 663 [para_from,64.1.1,28.1.1.2,flip.1] u(c(u(x,c(y))),u(z,n(y,x)))=u(z,y). 709 [para_into,66.1.1.2,51.1.1] u(n(x,y),n(c(y),x))=x. 712,711 [para_into,66.1.1,4.1.1] u(n(x,c(y)),n(x,y))=x. 713 [para_from,66.1.1,30.1.1.2,flip.1] u(n(x,c(y)),u(z,n(x,y)))=u(z,x). 716 [para_from,66.1.1,28.1.1.2,flip.1] u(n(x,y),u(z,n(x,c(y))))=u(z,x). 730 [para_into,343.1.1.2,51.1.1] u(c(u(x,Z)),n(x,U))=U. 732 [para_into,343.1.1,4.1.1] u(n(U,x),c(u(x,Z)))=U. 753 [para_into,345.1.1,4.1.1] u(n(x,U),c(u(Z,x)))=U. 755 [para_from,345.1.1,49.1.1.1,demod,21,21,flip.1] n(u(Z,x),u(c(x),Z))=Z. 794 [para_into,68.1.1.1.1,68.1.1] u(c(x),n(n(y,x),u(c(x),y)))=u(c(x),y). 814 [para_into,68.1.1,4.1.1] u(n(x,y),c(u(c(y),x)))=y. 823 [para_from,68.1.1,28.1.1.2,flip.1] u(c(u(c(x),y)),u(z,n(y,x)))=u(z,x). 843 [para_from,347.1.1,43.1.1.1,demod,21,21,flip.1] n(u(Z,c(x)),u(Z,x))=Z. 850 [para_into,349.1.1.1,133.1.1,demod,21] n(u(D,u(I,Z)),u(Z,Z))=Z. 884 [para_into,349.1.1.2.2,20.1.1] n(u(Z,U),u(Z,Z))=Z. 928 [para_into,884.1.1,51.1.1] n(u(Z,Z),u(Z,U))=Z. 982 [para_into,71.1.1.2.1,29.1.1] u(n(x,u(y,z)),c(u(y,u(z,c(x)))))=x. 1132,1131 [para_into,73.1.1.2,618.1.1] u(c(u(c(D),x)),x)=u(D,n(I,x)). 1134,1133 [para_into,73.1.1.2,527.1.1] u(c(u(c(Z),x)),x)=u(Z,n(U,x)). 1139,1138 [para_into,73.1.1.2,442.1.1,demod,15] u(c(u(D,x)),x)=u(I,n(D,x)). 1140 [para_into,73.1.1.2,385.1.1,demod,1134] u(Z,n(U,x))=u(Z,n(x,U)). 1148 [para_into,73.1.1.2,316.1.1,demod,15,1139] u(I,n(D,x))=u(I,n(x,D)). 1164,1163 [para_into,73.1.1.2,66.1.1] u(c(u(c(x),y)),x)=u(x,n(x,c(y))). 1239 [hyper,79,2] i($c3,u($c2,u($c1,x))). 1272 [para_into,1239.1.2.2,4.1.1] i($c3,u($c2,u(x,$c1))). 1276 [para_into,1272.1.2,29.1.1] i($c3,u(x,u($c1,$c2))). 1282,1281 [para_into,87.1.1.1,400.1.1,demod,15,15,15,flip.1] n(U,u(D,D))=D. 1301 [para_into,1276.1.2,6.1.1] i($c3,u(x,u(y,u($c1,$c2)))). 1303,1302 [para_into,1281.1.1,51.1.1] n(u(D,D),U)=D. 1578,1577 [para_into,95.1.1.2,511.1.1,demod,1164,15,flip.1] u(n(D,x),x)=u(x,n(x,D)). 1580,1579 [para_into,95.1.1.2,444.1.1,demod,15,1139,flip.1] u(n(x,D),I)=u(I,n(D,x)). 1589,1588 [para_into,95.1.1.2,318.1.1,demod,1132,flip.1] u(n(x,I),D)=u(D,n(I,x)). 1591,1590 [para_into,95.1.1.2,305.1.1,demod,1134,flip.1] u(n(x,U),Z)=u(Z,n(U,x)). 1618 [para_into,408.1.1.2,51.1.1] u(c(u(x,D)),n(x,I))=I. 1663 [para_into,410.1.1,4.1.1] u(n(x,I),c(u(D,x)))=I. 1708 [para_from,412.1.1,43.1.1.1,demod,15,15,flip.1] n(u(D,c(x)),u(D,x))=D. 1719 [para_into,414.1.1.1,133.1.1,demod,18,21] n(u(D,U),u(D,Z))=D. 1946 [para_into,650.1.1.2,51.1.1] u(n(x,y),n(c(x),y))=y. 1948 [para_into,650.1.1,4.1.1] u(n(x,c(y)),n(y,x))=x. 1952,1951 [para_from,650.1.1,73.1.1.2] u(c(u(c(x),y)),y)=u(x,n(y,c(x))). 2002 [para_into,709.1.1,4.1.1] u(n(c(x),y),n(y,x))=y. 2019,2018 [para_into,101.1.1.2,133.1.1,demod,35,flip.1] u(x,u(I,u(D,y)))=u(x,u(D,u(I,y))). 2022,2021 [para_into,101.1.1.2,97.1.1,demod,35,2019] u(x,u(I,u(y,D)))=u(x,u(D,u(I,y))). 2230 [para_into,711.1.1.2,928.1.1] u(n(u(Z,Z),c(u(Z,U))),Z)=u(Z,Z). 2245 [para_from,730.1.1,49.1.1.1,demod,21,21,flip.1] n(u(x,Z),u(c(x),Z))=Z. 2270,2269 [para_from,732.1.1,43.1.1.1,demod,21,21,flip.1] n(u(Z,c(x)),u(x,Z))=Z. 2361 [para_into,104.1.1.2.2,94.1.1] u(c(u(x,u(c(y),U))),n(y,u(D,u(x,I))))=y. 2390,2389 [para_from,104.1.1,95.1.1.2,demod,1164,flip.1] u(c(u(x,u(c(y),z))),y)=u(y,n(y,c(u(x,z)))). 2507 [para_from,843.1.1,62.1.1.2.2,demod,40,40,40] u(n(U,x),n(u(n(U,x),u(Z,x)),Z))=u(n(U,x),u(Z,x)). 2550 [para_into,106.1.1.2,755.1.1,demod,2390,1591,88,21,21] u(Z,n(Z,n(U,u(Z,Z))))=u(Z,Z). 2653 [para_from,1618.1.1,49.1.1.1,demod,15,15,flip.1] n(u(x,D),u(c(x),D))=D. 2757 [para_from,1663.1.1,43.1.1.1,demod,15,15,flip.1] n(u(c(x),D),u(D,x))=D. 2950 [para_into,1946.1.1,4.1.1] u(n(c(x),y),n(x,y))=y. 2996,2995 [para_from,1948.1.1,73.1.1.2,demod,12] u(n(x,y),x)=u(x,n(y,x)). 3036 [para_into,2002.1.1.2,928.1.1] u(n(c(u(Z,U)),u(Z,Z)),Z)=u(Z,Z). 3134 [para_from,2245.1.1,116.1.1.2] u(c(u(n(U,I),u(c(D),Z))),Z)=u(D,Z). 3144 [para_from,2245.1.1,64.1.1.2,demod,7] u(c(u(c(x),u(Z,c(u(x,Z))))),Z)=u(x,Z). 3538,3537 [para_from,2757.1.1,64.1.1.2,demod,48,7] u(c(u(D,u(x,n(x,I)))),D)=u(c(x),D). 3572,3571 [para_from,2950.1.1,95.1.1.2,demod,1952,flip.1] u(n(c(x),y),x)=u(x,n(y,c(x))). 3708 [para_into,432.1.1.2,2950.1.1,demod,15,1578] u(Z,I)=u(I,n(I,D)). 3769 [para_into,3708.1.1,4.1.1,flip.1] u(I,n(I,D))=u(I,Z). 3842 [para_into,3769.1.1.2,51.1.1] u(I,n(D,I))=u(I,Z). 3859 [para_from,3842.1.1,95.1.1.2,demod,18] u(c(u(c(D),I)),u(I,Z))=U. 4020 [para_into,652.1.1,4.1.1] u(n(x,y),c(u(x,c(y))))=y. 4093 [para_into,654.1.1.1,884.1.1,demod,7] u(Z,c(u(Z,u(Z,c(u(Z,U))))))=u(Z,U). 4147 [para_into,141.1.1.2,2653.1.1,demod,2390,1589,129,15,15] u(D,n(D,n(I,u(D,D))))=u(D,D). 4285,4284 [para_from,814.1.1,73.1.1.2,demod,1952,flip.1] u(x,c(u(c(y),x)))=u(x,n(y,c(x))). 4327 [para_from,850.1.1,66.1.1.1,demod,84] u(Z,n(u(D,u(I,Z)),n(U,U)))=u(D,u(I,Z)). 4521,4520 [para_into,1140.1.1,4.1.1] u(n(U,x),Z)=u(Z,n(x,U)). 4703,4702 [para_into,1148.1.1,4.1.1] u(n(D,x),I)=u(I,n(x,D)). 4705,4704 [para_from,1148.1.1,137.1.1.2,flip.1] u(n(D,x),U)=u(D,u(I,n(x,D))). 5879,5878 [para_from,1590.1.1,429.1.1.2,demod,438,flip.1] u(n(x,U),I)=u(I,n(U,x)). 5910 [para_into,2995.1.1,4.1.1] u(x,n(x,y))=u(x,n(y,x)). 5911 [copy,5910,flip.1] u(x,n(y,x))=u(x,n(x,y)). 5918 [para_into,3859.1.1,134.1.1,demod,4285,15] u(Z,u(I,n(D,D)))=U. 5922 [para_into,3859.1.1,28.1.1] u(I,u(c(u(c(D),I)),Z))=U. 5924 [para_into,5918.1.1,134.1.1] u(n(D,D),u(I,Z))=U. 5997,5996 [para_into,5911.1.1,4.1.1] u(n(x,y),y)=u(y,n(y,x)). 6013 [para_from,5922.1.1,137.1.1.2,demod,7,flip.1] u(c(u(c(D),I)),u(Z,U))=u(D,U). 6074,6073 [para_into,1138.1.1.1,126.1.1,demod,1589,flip.1] u(I,n(D,D))=u(D,n(I,I)). 6075 [para_into,1138.1.1.1,108.1.1,demod,4521] u(Z,n(I,U))=u(I,n(D,Z)). 6078,6077 [para_into,1138.1.1.1,41.1.1] u(n(I,x),c(x))=u(I,n(D,c(x))). 6149 [para_from,1138.1.1,1301.1.2.2] i($c3,u(x,u(I,n(D,u($c1,$c2))))). 6191 [para_into,6075.1.1.2,51.1.1] u(Z,n(U,I))=u(I,n(D,Z)). 6219 [para_into,6149.1.2,95.1.1,demod,18] i($c3,U). 6223 [hyper,6219,1] u($c3,U)=U. 6231 [para_into,6223.1.1,133.1.1] u(D,u(I,$c3))=U. 6241 [para_from,6223.1.1,394.1.1.1.1,demod,21] u(Z,n(I,u(I,$c3)))=I. 6258 [para_from,6223.1.1,28.1.1.2,flip.1] u($c3,u(x,U))=u(x,U). 6263,6262 [para_from,6223.1.1,6.1.1.1,demod,35,35,2019] u(I,u(D,x))=u($c3,u(D,u(I,x))). 6279 [back_demod,34,demod,6263] u(U,x)=u($c3,u(D,u(I,x))). 6281 [para_from,6231.1.1,1708.1.1.2] n(u(D,c(u(I,$c3))),U)=D. 6351,6350 [para_from,6241.1.1,437.1.1.2,demod,2996,flip.1] u(I,n(I,u(I,$c3)))=u(I,n(I,I)). 6371 [hyper,6258,2] i($c3,u(x,U)). 6379 [para_into,6371.1.2,133.1.1] i($c3,u(D,u(I,x))). 6386,6385 [hyper,6379,1] u($c3,u(D,u(I,x)))=u(D,u(I,x)). 6388,6387 [back_demod,6279,demod,6386] u(U,x)=u(D,u(I,x)). 6510,6509 [para_from,6281.1.1,287.1.1.2,demod,42,6351,3538,15,flip.1] u(D,c(u(I,$c3)))=u(D,D). 6511 [para_from,6281.1.1,71.1.1.1,demod,6510,127,6510] u(D,c(u(n(I,I),U)))=u(D,D). 6513 [para_from,6281.1.1,23.1.1.2,demod,6510,127,6510] u(c(u(n(I,I),U)),D)=u(D,D). 6613,6612 [para_into,309.1.1.2,618.1.1,demod,5879] u(n(I,Z),U)=u(I,n(U,D)). 6616 [para_into,309.1.1.2,345.1.1,flip.1] u(c(u(Z,x)),x)=u(n(x,Z),U). 6618 [para_from,309.1.1,205.1.1.2,demod,315] u(I,u(D,x))=u(x,U). 6619 [copy,6618,flip.1] u(x,U)=u(I,u(D,x)). 6628 [para_from,6619.1.1,1719.1.1.1] n(u(I,u(D,D)),u(D,Z))=D. 6633 [para_from,6619.1.1,345.1.1.1.1] u(c(u(I,u(D,Z))),n(U,U))=U. 6645 [para_into,312.1.1.2,2950.1.1,demod,1591,3572,flip.1] u(x,n(Z,c(x)))=u(Z,n(U,x)). 6648 [para_into,312.1.1.2,1948.1.1,demod,1591,flip.1] u(n(Z,c(x)),x)=u(Z,n(U,x)). 6660,6659 [para_into,322.1.1.2,6191.1.1,demod,382,18,flip.1] u(Z,U)=U. 6665 [back_demod,6013,demod,6660] u(c(u(c(D),I)),U)=u(D,U). 6669 [back_demod,4093,demod,6660,21,6660] u(Z,c(u(Z,u(Z,Z))))=U. 6671 [back_demod,3036,demod,6660,21,2996] u(Z,n(u(Z,Z),Z))=u(Z,Z). 6676,6675 [back_demod,2230,demod,6660,21,5997] u(Z,n(Z,u(Z,Z)))=u(Z,Z). 6678,6677 [back_demod,928,demod,6660] n(u(Z,Z),U)=Z. 6680,6679 [back_demod,884,demod,6660] n(U,u(Z,Z))=Z. 6683 [back_demod,2550,demod,6680] u(Z,n(Z,Z))=u(Z,Z). 6687,6686 [para_into,6659.1.1,6619.1.1] u(I,u(D,Z))=U. 6691,6690 [para_into,6659.1.1,133.1.1] u(D,u(I,Z))=U. 6694 [para_into,6659.1.1,94.1.1] u(D,u(Z,I))=U. 6697,6696 [back_demod,6633,demod,6687,21] u(Z,n(U,U))=U. 6698 [back_demod,4327,demod,6691,6691] u(Z,n(U,n(U,U)))=U. 6716,6715 [para_from,6659.1.1,285.1.1.2,flip.1] u(D,u(I,u(x,Z)))=u(x,U). 6728,6727 [para_from,6659.1.1,437.1.1.2] u(n(I,I),U)=u(I,U). 6730,6729 [para_from,6659.1.1,28.1.1.2,flip.1] u(Z,u(x,U))=u(x,U). 6739,6738 [back_demod,6513,demod,6728] u(c(u(I,U)),D)=u(D,D). 6740 [back_demod,6511,demod,6728] u(D,c(u(I,U)))=u(D,D). 6742 [para_into,325.1.1.2,374.1.1,demod,1589,4521,flip.1] u(Z,n(D,U))=u(D,n(I,Z)). 6770 [para_from,6694.1.1,134.1.1.2,demod,7] u(x,U)=u(Z,u(I,u(D,x))). 6771 [copy,6770,flip.1] u(Z,u(I,u(D,x)))=u(x,U). 6774 [para_from,6696.1.1,843.1.1.2] n(u(Z,c(n(U,U))),U)=Z. 6779,6778 [para_from,6696.1.1,437.1.1.2,demod,6728,flip.1] u(I,n(U,U))=u(I,U). 6788 [para_from,6683.1.1,312.1.1.2] u(n(Z,U),u(Z,Z))=u(Z,Z). 6814 [para_from,6698.1.1,437.1.1.2,demod,6728,flip.1] u(I,n(U,n(U,U)))=u(I,U). 7031 [para_from,6669.1.1,2269.1.1.1,demod,7,7] n(U,u(Z,u(Z,u(Z,Z))))=Z. 7223 [para_from,6671.1.1,302.1.1.2.2,demod,6716,6660,6660,flip.1] u(n(u(Z,Z),Z),U)=U. 7234 [para_from,7223.1.1,507.1.1.1,demod,21,5997,6676,6680,flip.1] n(u(Z,Z),Z)=Z. 7244 [para_from,7234.1.1,4020.1.1.1,demod,7] u(Z,c(u(Z,u(Z,c(Z)))))=Z. 7266 [para_into,6771.1.1.2.2,6740.1.1,demod,2022,18,6730,flip.1] u(c(u(I,U)),U)=u(D,U). 7335 [para_from,6788.1.1,507.1.1.1,demod,84,386,6678,flip.1] n(Z,U)=Z. 7340,7339 [para_from,6788.1.1,453.1.1.1.1,demod,84,21,2270,1591,6697,21,flip.1] u(Z,c(Z))=U. 7347,7346 [back_demod,7244,demod,7340,6660,21] u(Z,Z)=Z. 7349,7348 [back_demod,7031,demod,7347,7347,7347] n(U,Z)=Z. 7386,7385 [back_demod,83,demod,7347] c(Z)=n(U,U). 7393 [para_from,7335.1.1,287.1.1.2,demod,7386,6779] u(c(u(D,u(I,U))),Z)=Z. 7401 [para_from,7346.1.1,429.1.1.2,demod,426,flip.1] u(Z,I)=I. 7404,7403 [para_from,7346.1.1,437.1.1.2,demod,426,flip.1] u(I,Z)=I. 7406 [back_demod,5924,demod,7404,1580,6074] u(D,n(I,I))=U. 7454 [para_from,7401.1.1,337.1.1.2.2,demod,7347,7404,15] u(D,n(U,I))=U. 7463 [para_from,7401.1.1,347.1.1.2.1,demod,15,1589] u(D,n(I,U))=U. 7467,7466 [para_from,7401.1.1,30.1.1.2,flip.1] u(I,u(x,Z))=u(x,I). 7499 [para_from,7403.1.1,6.1.1.1,flip.1] u(I,u(Z,x))=u(I,x). 7508,7507 [para_from,7406.1.1,128.1.1.1,demod,21,15,15,flip.1] n(I,u(D,D))=Z. 7532 [back_demod,4147,demod,7508] u(D,n(D,Z))=u(D,D). 7550,7549 [para_from,7454.1.1,378.1.1.2,demod,6613,33] u(I,n(U,D))=U. 7565 [back_demod,6612,demod,7550] u(n(I,Z),U)=U. 7591,7590 [para_from,7463.1.1,28.1.1.2,flip.1] u(D,u(x,n(I,U)))=u(x,U). 7614,7613 [para_from,7549.1.1,378.1.1.2,demod,4705,18] u(D,u(I,n(Z,D)))=U. 7656 [para_from,7565.1.1,507.1.1.1,demod,21,5997] n(U,u(Z,n(Z,I)))=n(I,Z). 7743,7742 [para_from,7532.1.1,6618.1.1.2,demod,4705,7614] u(I,u(D,D))=U. 7756 [back_demod,6628,demod,7743] n(U,u(D,Z))=D. 7777,7776 [para_into,7742.1.1,6618.1.1] u(D,U)=U. 7780 [back_demod,7266,demod,7777] u(c(u(I,U)),U)=U. 7786 [back_demod,6665,demod,7777] u(c(u(c(D),I)),U)=U. 7803,7802 [para_from,7742.1.1,297.1.1.2.2,demod,7,7777,7777] u(D,u(x,U))=u(x,U). 7810,7809 [back_demod,7393,demod,7803] u(c(u(I,U)),Z)=Z. 7847,7846 [para_from,7756.1.1,68.1.1.2,demod,109,2996,6388,7591,6739,flip.1] u(D,Z)=u(D,D). 7851,7850 [para_from,7756.1.1,4520.1.1.1,demod,7847,7847,1303,flip.1] u(Z,D)=u(D,D). 7857,7856 [para_from,7756.1.1,87.1.1.1.2,demod,7851,127,21,7847,127,401,flip.1] n(U,I)=n(I,I). 7871,7870 [back_demod,3134,demod,7857,430,7847] u(c(u(c(D),I)),Z)=u(D,D). 7984,7983 [para_from,7780.1.1,281.1.1.1,demod,21,7810,7349,flip.1] c(u(I,U))=Z. 8024,8023 [para_from,7983.1.1,11.1.1.1.1,demod,40,flip.1] n(u(I,U),x)=n(U,x). 8026,8025 [para_from,7983.1.1,579.1.1.2.2.1.1,demod,7984,8024,8024,572,flip.1] u(I,U)=U. 8036,8035 [back_demod,6814,demod,8026] u(I,n(U,n(U,U)))=U. 8037 [back_demod,6778,demod,8026] u(I,n(U,U))=U. 8039 [back_demod,6727,demod,8026] u(n(I,I),U)=U. 8053,8052 [para_from,8025.1.1,210.1.1.2,demod,33,flip.1] u(I,u(x,U))=u(x,U). 8061,8060 [para_from,8037.1.1,473.1.1.1.1,demod,21,21,21,7347,21,21,7347] u(Z,n(Z,I))=Z. 8070,8069 [back_demod,7656,demod,8061,7349,flip.1] n(I,Z)=Z. 8075,8074 [back_demod,6742,demod,8070,7847] u(Z,n(D,U))=u(D,D). 8146,8145 [para_from,8039.1.1,28.1.1.2,flip.1] u(n(I,I),u(x,U))=u(x,U). 8231,8230 [para_from,7786.1.1,281.1.1.1,demod,21,7871,1282,flip.1] c(u(c(D),I))=D. 8259,8258 [para_from,8230.1.1,11.1.1.1.1,demod,42,flip.1] n(u(c(D),I),x)=n(I,x). 8260 [para_from,8230.1.1,579.1.1.2.2.1.1,demod,8231,8259,8259,570,flip.1] u(c(D),I)=I. 8266,8265 [para_from,8260.1.1,224.1.1.1.1.2,demod,33,21,8075] u(D,D)=D. 8375,8374 [back_demod,126,demod,8266] c(D)=n(I,I). 8429 [para_into,646.1.1.2,6774.1.1,demod,6388,8036,7777,21,7347,flip.1] u(Z,c(n(U,U)))=Z. 8472 [para_into,8429.1.1,4.1.1] u(c(n(U,U)),Z)=Z. 8474 [para_from,8429.1.1,7499.1.1.2,demod,7404,flip.1] u(I,c(n(U,U)))=I. 8490,8489 [para_from,8472.1.1,45.1.1.1,demod,7386,flip.1] n(n(U,U),U)=n(U,U). 8496,8495 [para_from,8474.1.1,287.1.1.1.1.2,demod,33,21,8490,6697,flip.1] n(U,U)=U. 8506,8505 [back_demod,7385,demod,8496] c(Z)=U. 8513 [para_from,8505.1.1,11.1.1.1.2] c(u(c(x),U))=n(x,Z). 8517 [para_from,8505.1.1,11.1.1.1.1,demod,6388] c(u(D,u(I,c(x))))=n(Z,x). 8520 [para_from,7802.1.1,412.1.1.2.1,demod,6078] u(I,n(D,c(u(x,U))))=I. 9639 [para_from,8520.1.1,716.1.1.2,demod,4703,18] u(I,n(u(x,U),D))=U. 9649 [para_from,9639.1.1,823.1.1.2,demod,8375,8146,18] u(c(u(x,U)),U)=U. 9663,9662 [para_into,9649.1.1.1,8513.1.1] u(n(x,Z),U)=U. 9672 [back_demod,6616,demod,9663] u(c(u(Z,x)),x)=U. 9680 [para_from,9649.1.1,8513.1.1.1,demod,21,flip.1] n(u(x,U),Z)=Z. 9727,9726 [para_into,9680.1.1,51.1.1] n(Z,u(x,U))=Z. 9733,9732 [para_from,9680.1.1,794.1.1.2.1,demod,8506,8506,6388,8053,7803,9727,6388,7404,33,8506,6388,8053,7803,flip.1] u(x,U)=U. 9735,9734 [para_from,9680.1.1,663.1.1.2.2,demod,9733,21,7347,8506,6388,7467,9733,9733] u(D,u(x,I))=U. 9747,9746 [back_demod,8513,demod,9733,21,flip.1] n(x,Z)=Z. 9813,9812 [back_demod,2361,demod,9733,9733,21,9735] u(Z,n(x,U))=x. 9845,9844 [back_demod,137,demod,9733] u(D,u(I,x))=U. 9858 [back_demod,2507,demod,9747,4521,9813,flip.1] u(n(U,x),u(Z,x))=x. 9861,9860 [back_demod,376,demod,9747] u(Z,n(U,x))=x. 9879,9878 [back_demod,8517,demod,9845,21,flip.1] n(Z,x)=Z. 9883,9882 [back_demod,6648,demod,9879,9861] u(Z,x)=x. 9885,9884 [back_demod,6645,demod,9879,9883] u(x,Z)=n(U,x). 9895,9894 [back_demod,1590,demod,9885,9883] n(U,n(x,U))=n(U,x). 9901,9900 [back_demod,601,demod,9879,9883] u(n(x,U),y)=u(x,y). 9910,9909 [back_demod,305,demod,9879,9885,9895] n(U,x)=x. 9916,9915 [back_demod,9858,demod,9910,9883] u(x,x)=x. 9925 [back_demod,9672,demod,9883] u(c(x),x)=U. 9969,9968 [back_demod,3144,demod,9885,9910,9883,9916,9885,9910,9885,9910] c(c(x))=x. 9982 [back_demod,753,demod,9883,9901] u(x,c(x))=U. 9999,9998 [back_demod,9884,demod,9910] u(x,Z)=x. 10050,10049 [para_from,9909.1.1,49.1.1.1.2,demod,21,9883] c(u(c(x),y))=n(x,c(y)). 10055 [para_from,9909.1.1,507.1.1.1.1,demod,9910,9910] n(u(x,y),u(x,c(y)))=x. 10079,10078 [para_from,9915.1.1,713.1.1.2,demod,712,2996,flip.1] u(x,n(y,x))=x. 10082 [back_demod,2995,demod,10079] u(n(x,y),x)=x. 10099 [para_from,9925.1.1,982.1.1.2.1.2,demod,9969,9733,21,9999] n(x,u(y,x))=x. 10121 [para_from,9982.1.1,364.1.1.2.2,demod,9733,9733,flip.1] u($c1,u($c2,c($c3)))=U. 10175 [hyper,10082,2] i(n(x,y),x). 10186 [para_into,10175.1.1,51.1.1] i(n(x,y),y). 10203 [para_from,10099.1.1,10186.1.1] i(x,u(y,x)). 10332 [para_into,10121.1.1,29.1.1] u($c2,u(c($c3),$c1))=U. 10426 [para_into,10055.1.1.1,10332.1.1,demod,10050,9910] u($c2,n($c3,c($c1)))=$c2. 10436 [para_from,10426.1.1,10203.1.2] i(n($c3,c($c1)),$c2). 10437 [binary,10436.1,3.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 1640 clauses generated 186251 clauses kept 6213 clauses forward subsumed 89825 clauses back subsumed 394 Kbytes malloced 5652 ----------- times (seconds) ----------- user CPU time 6.02 (0 hr, 0 min, 6 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 6 (0 hr, 0 min, 6 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 22:06:37 2003