----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Mon Dec 29 21:21:38 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_literals,1). assign(max_mem,13000). assign(max_weight,16). 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("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("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("30booleanLaws.txt"). ------- start included file 30booleanLaws.txt------- formula_list(usable). -(all x y z w (n(n(x,y),n(z,w))=n(n(x,w),n(z,y)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] n(n($c4,$c3),n($c2,$c1))!=n(n($c4,$c1),n($c2,$c3)). end_of_list. ------- end included file 30booleanLaws.txt------- SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=1. All clauses are units, and equality is present; the strategy will be Knuth-Bendix with positive clauses in sos. 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). ------------> process usable: ** KEPT (pick-wt=15): 1 [] n(n($c4,$c3),n($c2,$c1))!=n(n($c4,$c1),n($c2,$c3)). ------------> process sos: ** KEPT (pick-wt=7): 2 [] u(x,y)=u(y,x). ** KEPT (pick-wt=11): 4 [copy,3,flip.1] u(u(x,y),z)=u(x,u(y,z)). ---> New Demodulator: 5 [new_demod,4] u(u(x,y),z)=u(x,u(y,z)). ** KEPT (pick-wt=14): 6 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ---> New Demodulator: 7 [new_demod,6] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ** KEPT (pick-wt=11): 9 [copy,8,flip.1] k(k(x,y),z)=k(x,k(y,z)). ---> New Demodulator: 10 [new_demod,9] k(k(x,y),z)=k(x,k(y,z)). ** KEPT (pick-wt=5): 11 [] r(r(x))=x. ---> New Demodulator: 12 [new_demod,11] r(r(x))=x. ** KEPT (pick-wt=10): 13 [] r(u(x,y))=u(r(x),r(y)). ---> New Demodulator: 14 [new_demod,13] r(u(x,y))=u(r(x),r(y)). ** KEPT (pick-wt=10): 15 [] r(k(x,y))=k(r(y),r(x)). ---> New Demodulator: 16 [new_demod,15] r(k(x,y))=k(r(y),r(x)). ** KEPT (pick-wt=5): 17 [] k(x,I)=x. ---> New Demodulator: 18 [new_demod,17] k(x,I)=x. ** KEPT (pick-wt=13): 19 [] u(k(r(x),c(k(x,y))),c(y))=c(y). ---> New Demodulator: 20 [new_demod,19] u(k(r(x),c(k(x,y))),c(y))=c(y). ** KEPT (pick-wt=10): 22 [copy,21,flip.1] c(u(c(x),c(y)))=n(x,y). ---> New Demodulator: 23 [new_demod,22] c(u(c(x),c(y)))=n(x,y). Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] u(x,y)=u(y,x). >>>> Starting back demodulation with 5. >>>> Starting back demodulation with 7. >>>> Starting back demodulation with 10. >>>> Starting back demodulation with 12. >>>> Starting back demodulation with 14. >>>> Starting back demodulation with 16. >>>> Starting back demodulation with 18. >>>> Starting back demodulation with 20. >>>> Starting back demodulation with 23. >> back demodulating 6 with 23. >>>> Starting back demodulation with 25. ======= end of input processing ======= =========== start of search =========== ----> UNIT CONFLICT at 1.73 sec ----> 6919 [binary,6918.1,6887.1] $F. Length of proof is 74. Level of proof is 22. ---------------- PROOF ---------------- 1 [] n(n($c4,$c3),n($c2,$c1))!=n(n($c4,$c1),n($c2,$c3)). 2 [] u(x,y)=u(y,x). 3 [] u(x,u(y,z))=u(u(x,y),z). 5,4 [copy,3,flip.1] u(u(x,y),z)=u(x,u(y,z)). 6 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 12,11 [] r(r(x))=x. 13 [] r(u(x,y))=u(r(x),r(y)). 15 [] r(k(x,y))=k(r(y),r(x)). 17 [] k(x,I)=x. 19 [] u(k(r(x),c(k(x,y))),c(y))=c(y). 21 [] n(x,y)=c(u(c(x),c(y))). 23,22 [copy,21,flip.1] c(u(c(x),c(y)))=n(x,y). 24 [back_demod,6,demod,23] u(c(u(c(x),y)),n(x,y))=x. 29 [para_into,4.1.1.1,2.1.1,demod,5] u(x,u(y,z))=u(y,u(x,z)). 30 [para_into,4.1.1,2.1.1] u(x,u(y,z))=u(y,u(z,x)). 32 [para_into,15.1.1.1,17.1.1,flip.1] k(r(I),r(x))=r(x). 38 [para_into,32.1.1.2,11.1.1,demod,12] k(r(I),x)=x. 41,40 [para_into,38.1.1,17.1.1] r(I)=I. 43,42 [back_demod,38,demod,41] k(I,x)=x. 46 [para_into,22.1.1.1.2,22.1.1] c(u(c(x),n(y,z)))=n(x,u(c(y),c(z))). 48 [para_into,22.1.1.1,2.1.1,demod,23] n(x,y)=n(y,x). 50 [para_from,48.1.1,1.1.1.2] n(n($c4,$c3),n($c1,$c2))!=n(n($c4,$c1),n($c2,$c3)). 54 [para_into,24.1.1.1.1,2.1.1] u(c(u(x,c(y))),n(y,x))=y. 56 [para_into,24.1.1.1,22.1.1] u(n(x,y),n(x,c(y)))=x. 59,58 [para_into,24.1.1.2,48.1.1] u(c(u(c(x),y)),n(y,x))=x. 64 [para_from,24.1.1,4.1.1.1,flip.1] u(c(u(c(x),y)),u(n(x,y),z))=u(x,z). 66 [para_into,19.1.1.1.1,40.1.1,demod,43,43] u(c(x),c(x))=c(x). 76 [para_into,66.1.1.1,22.1.1,demod,23,23] u(n(x,y),n(x,y))=n(x,y). 79,78 [para_from,66.1.1,22.1.1.1] c(c(x))=n(x,x). 82 [para_from,66.1.1,4.1.1.1,flip.1] u(c(x),u(c(x),y))=u(c(x),y). 87,86 [para_into,78.1.1.1,22.1.1] c(n(x,y))=n(u(c(x),c(y)),u(c(x),c(y))). 90 [para_from,78.1.1,24.1.1.1.1.1] u(c(u(n(x,x),y)),n(c(x),y))=c(x). 92 [para_into,56.1.1.1,48.1.1] u(n(x,y),n(y,c(x)))=y. 105,104 [para_from,56.1.1,4.1.1.1,flip.1] u(n(x,y),u(n(x,c(y)),z))=u(x,z). 110 [para_into,92.1.1.2,48.1.1] u(n(x,y),n(c(x),y))=y. 128 [para_into,29.1.1,2.1.1,demod,5] u(x,u(y,z))=u(x,u(z,y)). 178 [para_into,30.1.1.2,2.1.1] u(x,u(y,z))=u(z,u(y,x)). 217,216 [para_into,54.1.1.2,48.1.1] u(c(u(x,c(y))),n(x,y))=y. 298,297 [para_into,76.1.1.1,48.1.1] u(n(x,y),n(y,x))=n(y,x). 444 [para_into,50.1.1,48.1.1,flip.1] n(n($c4,$c1),n($c2,$c3))!=n(n($c1,$c2),n($c4,$c3)). 448,447 [para_from,297.1.1,4.1.1.1,flip.1] u(n(x,y),u(n(y,x),z))=u(n(y,x),z). 449 [para_from,297.1.1,178.1.1.2,demod,448] u(x,n(y,z))=u(n(z,y),x). 450 [para_from,297.1.1,128.1.1.2,demod,298] u(x,n(y,z))=u(x,n(z,y)). 454 [copy,449,flip.1] u(n(x,y),z)=u(z,n(y,x)). 518 [para_into,82.1.1.2,216.1.1,demod,217] u(c(u(x,c(y))),y)=y. 522,521 [para_into,82.1.1.2,58.1.1,demod,59] u(c(u(c(x),y)),x)=x. 552 [para_into,518.1.1.1,22.1.1] u(n(x,y),y)=y. 576 [para_from,518.1.1,22.1.1.1,demod,79,79,flip.1] n(u(x,n(y,y)),y)=n(y,y). 596 [para_into,552.1.1.1,48.1.1] u(n(x,y),x)=x. 598 [para_into,552.1.1,454.1.1] u(x,n(x,y))=x. 624 [para_from,552.1.1,13.1.1.1,flip.1] u(r(n(x,y)),r(y))=r(y). 763,762 [para_into,64.1.1.2,596.1.1,demod,522,flip.1] u(x,x)=x. 765,764 [para_into,64.1.1.2,552.1.1] u(c(u(c(x),y)),y)=u(x,y). 772 [para_into,64.1.1.2,110.1.1,demod,765,flip.1] u(x,n(c(x),y))=u(x,y). 774 [para_into,64.1.1.2,92.1.1,demod,765,flip.1] u(x,n(y,c(x)))=u(x,y). 988 [para_into,624.1.1.2,11.1.1,demod,12] u(r(n(x,r(y))),y)=y. 1028 [para_into,988.1.1.1.1,48.1.1] u(r(n(r(x),y)),x)=x. 1124 [para_into,772.1.1,449.1.1] u(n(x,c(y)),y)=u(y,x). 1133,1132 [para_from,772.1.1,46.1.1.1,demod,79,87,763,763] c(u(c(x),y))=n(x,u(n(c(x),c(x)),c(y))). 1153 [back_demod,22,demod,1133,79] n(x,u(n(c(x),c(x)),n(y,y)))=n(x,y). 1182 [para_from,1124.1.1,90.1.1.1.1,demod,79,79] u(c(u(x,c(x))),n(n(x,x),x))=n(x,x). 1239,1238 [para_into,576.1.1.1,1028.1.1] n(n(x,x),x)=n(x,x). 1248,1247 [back_demod,1182,demod,1239,217,flip.1] n(x,x)=x. 1265,1264 [back_demod,1153,demod,1248,1248] n(x,u(c(x),y))=n(x,y). 1315,1314 [back_demod,86,demod,1248] c(n(x,y))=u(c(x),c(y)). 1317,1316 [back_demod,78,demod,1248] c(c(x))=x. 1509 [para_into,104.1.1.2,774.1.1,demod,105,1315,1317,flip.1] u(x,n(y,u(c(x),z)))=u(x,y). 1601 [para_into,1264.1.1.2,450.1.1,demod,1265] n(x,n(y,z))=n(x,n(z,y)). 1609 [para_into,1264.1.1.2,128.1.1,demod,1265] n(x,u(y,z))=n(x,u(z,y)). 1620,1619 [para_into,1264.1.1,48.1.1] n(u(c(x),y),x)=n(x,y). 3445 [para_into,1601.1.1,48.1.1] n(n(x,y),z)=n(z,n(y,x)). 3451 [copy,3445,flip.1] n(x,n(y,z))=n(n(z,y),x). 3513 [para_into,1609.1.1,48.1.1] n(u(x,y),z)=n(z,u(y,x)). 3518 [copy,3513,flip.1] n(x,u(y,z))=n(u(z,y),x). 6361 [para_into,444.1.1,48.1.1] n(n($c2,$c3),n($c4,$c1))!=n(n($c1,$c2),n($c4,$c3)). 6414 [para_from,1509.1.1,1619.1.1.1,demod,1620,1317,flip.1] n(x,n(y,u(x,z)))=n(x,y). 6470 [para_into,6414.1.1.2,3518.1.1] n(x,n(u(y,x),z))=n(x,z). 6476 [para_into,6414.1.1,3451.1.1] n(n(u(x,y),z),x)=n(x,z). 6570,6569 [para_into,6470.1.1.2.1,598.1.1] n(n(x,y),n(x,z))=n(n(x,y),z). 6661 [para_into,6476.1.1.1.1,596.1.1,demod,6570] n(n(x,y),z)=n(n(x,z),y). 6785 [para_into,6661.1.1.1,3451.1.1] n(n(n(x,y),z),u)=n(n(z,u),n(y,x)). 6868,6867 [para_into,6661.1.1,48.1.1,flip.1] n(n(x,y),z)=n(y,n(x,z)). 6887 [back_demod,6785,demod,6868,6868,6868,6868] n(x,n(y,n(z,u)))=n(u,n(x,n(z,y))). 6918 [back_demod,6361,demod,6868,6868,flip.1] n($c2,n($c1,n($c4,$c3)))!=n($c3,n($c2,n($c4,$c1))). 6919 [binary,6918.1,6887.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 465 clauses generated 85391 clauses kept 4016 clauses forward subsumed 65855 clauses back subsumed 31 Kbytes malloced 4215 ----------- times (seconds) ----------- user CPU time 1.93 (0 hr, 0 min, 1 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 2 (0 hr, 0 min, 2 sec) 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 Mon Dec 29 21:21:40 2003