----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sat Nov 22 17:13:53 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). 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("dDef.txt"). ------- start included file dDef.txt------- formula_list(usable). all x y (d(x,y)=c(k(c(x),c(y)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] d(x,y)=c(k(c(x),c(y))). end_of_list. ------- end included file dDef.txt------- include("iii.txt"). ------- start included file iii.txt------- formula_list(usable). all x y (c(k(x,y))=d(c(x),c(y))). all x y (c(d(x,y))=k(c(x),c(y))). all x y (r(k(x,y))=k(r(y),r(x))). -(all x y (r(d(x,y))=d(r(y),r(x)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] c(k(x,y))=d(c(x),c(y)). 0 [] c(d(x,y))=k(c(x),c(y)). 0 [] r(k(x,y))=k(r(y),r(x)). 0 [] r(d($c2,$c1))!=d(r($c1),r($c2)). end_of_list. ------- end included file iii.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=10): 1 [] r(d($c2,$c1))!=d(r($c1),r($c2)). ------------> 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=10): 18 [copy,17,flip.1] c(k(c(x),c(y)))=d(x,y). ---> New Demodulator: 19 [new_demod,18] c(k(c(x),c(y)))=d(x,y). ** KEPT (pick-wt=10): 20 [] c(k(x,y))=d(c(x),c(y)). ---> New Demodulator: 21 [new_demod,20] c(k(x,y))=d(c(x),c(y)). ** KEPT (pick-wt=10): 22 [] c(d(x,y))=k(c(x),c(y)). ---> New Demodulator: 23 [new_demod,22] c(d(x,y))=k(c(x),c(y)). ** KEPT (pick-wt=11): 25 [copy,24,demod,16] k(r(x),r(y))=k(r(x),r(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 19. >>>> Starting back demodulation with 21. >> back demodulating 18 with 21. >>>> Starting back demodulation with 23. Following clause subsumed by 25 during input processing: 0 [copy,25,flip.1] k(r(x),r(y))=k(r(x),r(y)). >>>> Starting back demodulation with 27. ======= end of input processing ======= =========== start of search =========== Resetting weight limit to 19. sos_size=3055 Resetting weight limit to 15. sos_size=3387 Resetting weight limit to 13. sos_size=2079 ----> UNIT CONFLICT at 6.69 sec ----> 6698 [binary,6696.1,1.1] $F. Length of proof is 113. Level of proof is 38. ---------------- PROOF ---------------- 1 [] r(d($c2,$c1))!=d(r($c1),r($c2)). 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. 14,13 [] r(u(x,y))=u(r(x),r(y)). 16,15 [] r(k(x,y))=k(r(y),r(x)). 23,22 [] c(d(x,y))=k(c(x),c(y)). 31 [para_into,4.1.1.1,2.1.1,demod,5] u(x,u(y,z))=u(y,u(x,z)). 32 [para_into,4.1.1,2.1.1] u(x,u(y,z))=u(y,u(z,x)). 33 [copy,32,flip.1] u(x,u(y,z))=u(z,u(x,y)). 46 [para_into,6.1.1.1.1.1,22.1.1,demod,23] u(c(u(k(c(x),c(y)),z)),c(u(k(c(x),c(y)),c(z))))=d(x,y). 52 [para_into,6.1.1.1.1,2.1.1] u(c(u(x,c(y))),c(u(c(y),c(x))))=y. 60 [para_into,6.1.1.2.1,2.1.1] u(c(u(c(x),y)),c(u(c(y),c(x))))=x. 62 [para_into,6.1.1,2.1.1] u(c(u(c(x),c(y))),c(u(c(x),y)))=x. 66 [para_from,6.1.1,4.1.1.1,flip.1] u(c(u(c(x),y)),u(c(u(c(x),c(y))),z))=u(x,z). 68 [para_into,31.1.1.2,31.1.1] u(x,u(y,u(z,u)))=u(z,u(x,u(y,u))). 69 [para_into,31.1.1.2,6.1.1,flip.1] u(c(u(c(x),y)),u(z,c(u(c(x),c(y)))))=u(z,x). 72 [para_into,31.1.1,2.1.1,demod,5] u(x,u(y,z))=u(x,u(z,y)). 73 [para_from,31.1.1,6.1.1.1.1] u(c(u(x,u(c(y),z))),c(u(c(y),c(u(x,z)))))=y. 78 [para_into,32.1.1.2,2.1.1] u(x,u(y,z))=u(z,u(y,x)). 85 [para_into,33.1.1.2,6.1.1,flip.1] u(c(u(c(x),c(y))),u(z,c(u(c(x),y))))=u(z,x). 116 [para_into,78.1.1.2,72.1.1,demod,5] u(x,u(y,u(z,u)))=u(u,u(z,u(y,x))). 121 [para_from,78.1.1,4.1.1.1,demod,5,5,5] u(x,u(y,u(z,u)))=u(z,u(y,u(x,u))). 148 [para_into,52.1.1.2.1,2.1.1] u(c(u(x,c(y))),c(u(c(x),c(y))))=y. 150 [para_into,52.1.1,2.1.1] u(c(u(c(x),c(y))),c(u(y,c(x))))=x. 158 [para_from,52.1.1,4.1.1.1,flip.1] u(c(u(x,c(y))),u(c(u(c(y),c(x))),z))=u(y,z). 206 [para_into,60.1.1,2.1.1] u(c(u(c(x),c(y))),c(u(c(y),x)))=y. 208 [para_from,60.1.1,52.1.1.2.1,demod,5] u(c(u(c(x),u(c(y),c(u(c(y),x))))),c(y))=u(c(y),x). 218 [para_from,60.1.1,4.1.1.1,flip.1] u(c(u(c(x),y)),u(c(u(c(y),c(x))),z))=u(x,z). 221 [para_from,60.1.1,33.1.1.2,flip.1] u(c(u(c(x),c(y))),u(z,c(u(c(y),x))))=u(z,y). 223 [para_from,60.1.1,31.1.1.2,flip.1] u(c(u(c(x),y)),u(z,c(u(c(y),c(x)))))=u(z,x). 242 [para_into,62.1.1.2.1,78.1.1] u(c(u(c(x),c(u(y,z)))),c(u(z,u(y,c(x)))))=x. 288 [para_into,148.1.1,2.1.1] u(c(u(c(x),c(y))),c(u(x,c(y))))=y. 328 [para_into,150.1.1.1.1,62.1.1,demod,5] u(c(x),c(u(c(x),u(y,c(u(c(x),c(y)))))))=u(c(x),c(y)). 463 [para_from,68.1.1,6.1.1.1.1] u(c(u(x,u(c(y),u(z,u)))),c(u(c(y),c(u(z,u(x,u))))))=y. 487,486 [para_into,46.1.1.1.1,68.1.1] u(c(u(x,u(k(c(y),c(z)),u(u,v)))),c(u(k(c(y),c(z)),c(u(u,u(x,v))))))=d(y,z). 1978 [para_into,66.1.1.2,288.1.1] u(c(u(c(x),y)),y)=u(x,c(u(x,c(y)))). 1979 [para_into,66.1.1.2,206.1.1] u(c(u(c(x),y)),y)=u(x,c(u(c(y),x))). 1980 [para_into,66.1.1.2,150.1.1] u(c(u(c(x),y)),x)=u(x,c(u(y,c(x)))). 2010 [copy,1978,flip.1] u(x,c(u(x,c(y))))=u(c(u(c(x),y)),y). 2012 [copy,1980,flip.1] u(x,c(u(y,c(x))))=u(c(u(c(x),y)),x). 2361,2360 [para_into,69.1.1.2,288.1.1,flip.1] u(c(u(c(c(x)),c(y))),x)=u(c(u(c(x),y)),y). 2364 [para_into,69.1.1.2,148.1.1] u(c(u(c(x),y)),y)=u(c(u(x,c(y))),x). 2370 [para_into,69.1.1.2,52.1.1] u(c(u(c(x),y)),x)=u(c(u(y,c(x))),x). 2384 [copy,2370,flip.1] u(c(u(x,c(y))),y)=u(c(u(c(y),x)),y). 2466 [para_into,1978.1.1.1.1,2.1.1] u(c(u(x,c(y))),x)=u(y,c(u(y,c(x)))). 2494 [para_into,1978.1.1,2.1.1] u(x,c(u(c(y),x)))=u(y,c(u(y,c(x)))). 2552 [copy,2494,flip.1] u(x,c(u(x,c(y))))=u(y,c(u(c(x),y))). 2779 [para_into,1979.1.1.1.1,2.1.1] u(c(u(x,c(y))),x)=u(y,c(u(c(x),y))). 3089 [para_into,1980.1.1,2.1.1] u(x,c(u(c(x),y)))=u(x,c(u(y,c(x)))). 4300 [para_from,2364.1.1,60.1.1.1.1] u(c(u(c(u(x,c(y))),x)),c(u(c(y),c(u(c(x),y)))))=u(c(x),y). 4409 [para_into,85.1.1.2,288.1.1,demod,2361] u(c(u(c(x),c(c(y)))),y)=u(c(u(c(x),y)),y). 4412 [para_from,2466.1.1,66.1.1.2] u(c(u(c(x),y)),u(y,c(u(y,c(c(x))))))=u(x,c(x)). 4603,4602 [para_into,218.1.1.2,4409.1.1] u(c(u(c(c(x)),y)),u(c(u(c(y),x)),x))=u(c(x),x). 4610 [para_into,221.1.1.2,2010.1.1,demod,4603] u(c(x),x)=u(c(y),y). 4636 [para_into,4610.1.1,72.1.1] u(c(u(x,y)),u(y,x))=u(c(z),z). 4642 [para_into,4610.1.1,2.1.1] u(x,c(x))=u(c(y),y). 4689,4688 [para_from,4610.1.1,158.1.1.2] u(c(u(x,c(y))),u(c(z),z))=u(y,u(c(y),c(x))). 4692 [para_from,4610.1.1,150.1.1.2.1] u(c(u(c(x),c(c(c(x))))),c(u(c(y),y)))=x. 4702 [para_from,4610.1.1,73.1.1.1.1.2] u(c(u(x,u(c(y),y))),c(u(c(z),c(u(x,z)))))=z. 4757,4756 [para_from,4610.1.1,52.1.1.2.1] u(c(u(x,c(c(x)))),c(u(c(y),y)))=c(x). 4799 [para_from,4610.1.1,62.1.1.1.1] u(c(u(c(x),x)),c(u(c(c(y)),y)))=c(y). 4801 [para_from,4610.1.1,6.1.1.2.1] u(c(u(c(c(x)),x)),c(u(c(y),y)))=c(x). 4807 [para_from,4610.1.1,13.1.1.1,demod,14] u(r(c(x)),r(x))=u(r(c(y)),r(y)). 4872,4871 [back_demod,4692,demod,4757] c(c(x))=x. 4885,4884 [back_demod,4801,demod,4872] u(c(u(x,x)),c(u(c(y),y)))=c(x). 4887,4886 [back_demod,4799,demod,4872] u(c(u(c(x),x)),c(u(y,y)))=c(y). 4927 [back_demod,4412,demod,4872] u(c(u(c(x),y)),u(y,c(u(y,x))))=u(x,c(x)). 4997 [para_from,4871.1.1,2494.1.1.2.1.1,flip.1] u(c(x),c(u(c(x),c(y))))=u(y,c(u(x,y))). 5003,5002 [para_from,4871.1.1,221.1.1.2.2.1.1,demod,4872] u(c(u(c(x),y)),u(z,c(u(y,x))))=u(z,c(y)). 5031 [para_from,4871.1.1,2779.1.1.1.1.2,flip.1] u(c(x),c(u(c(y),c(x))))=u(c(u(y,x)),y). 5073,5072 [para_from,4871.1.1,218.1.1.2.1.1.2,demod,4872] u(c(u(x,y)),u(c(u(c(y),x)),z))=u(c(x),z). 5077,5076 [para_from,4871.1.1,60.1.1.2.1.2,demod,4872] u(c(u(x,y)),c(u(c(y),x)))=c(x). 5094 [para_from,4871.1.1,6.1.1.2.1.1,demod,4872] u(c(u(x,y)),c(u(x,c(y))))=c(x). 5099 [para_from,4871.1.1,3089.1.1.2.1.1,demod,4872] u(c(x),c(u(x,y)))=u(c(x),c(u(y,x))). 5101 [para_from,4871.1.1,1980.1.1.1.1.1,demod,4872] u(c(u(x,y)),c(x))=u(c(x),c(u(y,x))). 5106 [back_demod,4927,demod,5003] u(x,c(x))=u(y,c(y)). 5329 [para_into,4636.1.1.1.1,5106.1.1,demod,4689] u(x,u(c(x),c(x)))=u(c(y),y). 5349 [para_into,5329.1.1.2.1,4871.1.1,demod,4872] u(c(x),u(x,x))=u(c(y),y). 5432 [para_into,5349.1.1,78.1.1] u(x,u(x,c(x)))=u(c(y),y). 5564 [para_into,5432.1.1.2,5106.1.1] u(x,u(y,c(y)))=u(c(z),z). 5565 [para_into,5432.1.1.2,4642.1.1] u(x,u(c(y),y))=u(c(z),z). 5566 [copy,5564,flip.1] u(c(x),x)=u(y,u(z,c(z))). 5567 [copy,5565,flip.1] u(c(x),x)=u(y,u(c(z),z)). 5608 [para_into,5564.1.1,32.1.1] u(x,u(c(x),y))=u(c(z),z). 5728 [para_into,5566.1.1.1,4871.1.1] u(x,c(x))=u(y,u(z,c(z))). 5930 [para_into,208.1.1.1.1,5608.1.1,demod,4872,4872] u(c(u(c(x),x)),y)=u(y,y). 6066 [para_into,5930.1.1.1.1,5567.1.1] u(c(u(x,u(c(y),y))),z)=u(z,z). 6082 [copy,6066,flip.1] u(x,x)=u(c(u(y,u(c(z),z))),x). 6095,6094 [para_from,5930.1.1,208.1.1.1.1.2.2.1,demod,4887,4885,4872,flip.1] u(c(u(c(x),x)),y)=y. 6097,6096 [para_from,5930.1.1,223.1.1.2,demod,5073,4872,6095] u(x,c(u(c(y),c(x))))=x. 6101,6100 [para_from,5930.1.1,2012.1.1.2.1,demod,6097,flip.1] u(c(u(c(x),c(u(c(y),y)))),x)=x. 6116,6115 [para_from,5930.1.1,2779.1.1.1.1,demod,4885,4872,4872,5,flip.1] u(x,c(u(c(y),u(y,x))))=x. 6118,6117 [para_from,5930.1.1,2552.1.1.2.1,demod,6095,4872,5,6116] c(u(c(x),c(x)))=x. 6120,6119 [para_from,5930.1.1,2384.1.1.1.1,demod,6118,6101] u(x,x)=x. 6142,6141 [back_demod,328,demod,6097] u(c(x),c(u(c(x),y)))=u(c(x),c(y)). 6158,6157 [back_demod,6082,demod,6120,flip.1] u(c(u(x,u(c(y),y))),z)=z. 6170,6169 [back_demod,4997,demod,6142,4872,flip.1] u(x,c(u(y,x)))=u(c(y),x). 6174,6173 [back_demod,4702,demod,6158] c(u(c(x),c(u(y,x))))=x. 6192,6191 [back_demod,5031,demod,6170,4872,flip.1] u(c(u(x,y)),x)=u(x,c(y)). 6225,6224 [back_demod,4300,demod,6192,4872,6174] u(c(u(x,y)),y)=u(c(x),y). 6268,6267 [para_into,6119.1.1,121.1.1,demod,5,5,6120] u(x,u(y,u(y,u(x,z))))=u(y,u(x,z)). 6270,6269 [para_into,6119.1.1,116.1.1,demod,6268] u(x,u(y,u(z,x)))=u(y,u(z,x)). 6274 [para_into,6119.1.1,78.1.1,demod,6270] u(x,u(x,y))=u(x,y). 6360 [para_into,6274.1.1,223.1.1,demod,5077,4872] u(c(u(c(x),y)),x)=x. 6405,6404 [para_into,6360.1.1.1.1.1,4871.1.1] u(c(u(x,y)),c(x))=c(x). 6407,6406 [back_demod,5101,demod,6405,flip.1] u(c(x),c(u(y,x)))=c(x). 6411,6410 [back_demod,5099,demod,6407] u(c(x),c(u(x,y)))=c(x). 6441 [para_into,242.1.1.2.1.2,5728.1.1,demod,6411,4872] u(x,c(u(y,u(z,u(u,c(u))))))=x. 6556 [para_into,4807.1.1.2,11.1.1] u(r(c(r(x))),x)=u(r(c(y)),r(y)). 6589,6588 [para_from,6556.1.1,6441.1.1.2.1] u(x,c(u(r(c(y)),r(y))))=x. 6600 [para_from,6556.1.1,6169.1.1.2.1,demod,6589,flip.1] u(c(r(c(r(x)))),x)=x. 6655,6654 [para_from,6600.1.1,5094.1.1.2.1,demod,4872,6225,4872,4872] u(r(c(r(c(x)))),x)=r(c(r(c(x)))). 6660 [para_from,6600.1.1,13.1.1.1,demod,6655,flip.1] r(c(r(c(r(x)))))=r(x). 6686 [para_into,6660.1.1.1.1.1.1,11.1.1,demod,12] r(c(r(c(x))))=x. 6688 [para_into,6686.1.1.1.1.1,4871.1.1] r(c(r(x)))=c(x). 6693,6692 [para_into,6688.1.1.1.1,11.1.1] r(c(x))=c(r(x)). 6695,6694 [para_into,6692.1.1.1,22.1.1,demod,16,6693,6693,flip.1] c(r(d(x,y)))=k(c(r(y)),c(r(x))). 6696 [para_from,6694.1.1,463.1.1.2.1.1,demod,6695,487,flip.1] r(d(x,y))=d(r(y),r(x)). 6698 [binary,6696.1,1.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 487 clauses generated 187110 clauses kept 5166 clauses forward subsumed 87243 clauses back subsumed 260 Kbytes malloced 5205 ----------- times (seconds) ----------- user CPU time 6.89 (0 hr, 0 min, 6 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 7 (0 hr, 0 min, 7 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 Sat Nov 22 17:14:00 2003