----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sat Nov 22 00:14:33 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_weight,19). assign(max_distinct_vars,3). assign(max_literals,1). assign(max_mem,64000). formula_list(usable). all x (x=x). end_of_list. -------> usable clausifies to: list(usable). 0 [] x=x. end_of_list. 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("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("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("xi_b.txt"). ------- start included file xi_b.txt------- formula_list(usable). all x i(I,u(c(x),r(x))). -(all x i(n(r(x),c(x)),D)). end_of_list. -------> usable clausifies to: list(usable). 0 [] i(I,u(c(x),r(x))). 0 [] -i(n(r($c1),c($c1)),D). end_of_list. ------- end included file xi_b.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=7): 3 [] -i(n(r($c1),c($c1)),D). ------------> process sos: ** KEPT (pick-wt=3): 4 [] x=x. ** 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=14): 9 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ---> New Demodulator: 10 [new_demod,9] u(c(u(c(x),y)),c(u(c(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=10): 28 [copy,27,flip.1] c(u(c(x),c(y)))=n(x,y). ---> New Demodulator: 29 [new_demod,28] c(u(c(x),c(y)))=n(x,y). ** KEPT (pick-wt=4): 31 [copy,30,flip.1] c(I)=D. ---> New Demodulator: 32 [new_demod,31] c(I)=D. ** KEPT (pick-wt=5): 34 [copy,33,flip.1] u(I,D)=U. ---> New Demodulator: 35 [new_demod,34] u(I,D)=U. ** KEPT (pick-wt=4): 37 [copy,36,flip.1] c(U)=Z. ---> New Demodulator: 38 [new_demod,37] c(U)=Z. ** KEPT (pick-wt=7): 39 [] i(I,u(c(x),r(x))). Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] x=x. 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. >> back demodulating 9 with 29. >>>> Starting back demodulation with 32. >>>> Starting back demodulation with 35. >>>> Starting back demodulation with 38. >>>> Starting back demodulation with 41. ======= end of input processing ======= =========== start of search =========== ----> UNIT CONFLICT at 0.37 sec ----> 3709 [binary,3708.1,198.1] $F. Length of proof is 58. Level of proof is 18. ---------------- PROOF ---------------- 1 [] -i(x,y)|u(x,y)=y. 2 [] i(x,y)|u(x,y)!=y. 3 [] -i(n(r($c1),c($c1)),D). 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)). 9 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 11 [] k(x,k(y,z))=k(k(x,y),z). 12 [copy,11,flip.1] k(k(x,y),z)=k(x,k(y,z)). 15,14 [] r(r(x))=x. 18 [] r(k(x,y))=k(r(y),r(x)). 23 [] k(x,I)=x. 25 [] u(k(r(x),c(k(x,y))),c(y))=c(y). 27 [] n(x,y)=c(u(c(x),c(y))). 29,28 [copy,27,flip.1] c(u(c(x),c(y)))=n(x,y). 30 [] D=c(I). 31 [copy,30,flip.1] c(I)=D. 33 [] U=u(I,D). 34 [copy,33,flip.1] u(I,D)=U. 36 [] Z=c(U). 38,37 [copy,36,flip.1] c(U)=Z. 39 [] i(I,u(c(x),r(x))). 40 [back_demod,9,demod,29] u(c(u(c(x),y)),n(x,y))=x. 43,42 [para_into,34.1.1,5.1.1] u(D,I)=U. 47 [para_into,39.1.2.1,31.1.1] i(I,u(D,r(I))). 48 [para_into,39.1.2.2,14.1.1] i(I,u(c(r(x)),x)). 54,53 [para_into,7.1.1.1,42.1.1] u(U,x)=u(D,u(I,x)). 56,55 [para_into,7.1.1.1,34.1.1,demod,54,flip.1] u(I,u(D,x))=u(D,u(I,x)). 60 [hyper,47,1,demod,56] u(D,u(I,r(I)))=u(D,r(I)). 69 [para_into,48.1.2,5.1.1] i(I,u(x,c(r(x)))). 70 [para_into,12.1.1.1,23.1.1,flip.1] k(x,k(I,y))=k(x,y). 74 [hyper,69,1] u(I,u(x,c(r(x))))=u(x,c(r(x))). 77 [para_into,53.1.1,5.1.1] u(x,U)=u(D,u(I,x)). 94 [para_into,77.1.1,7.1.1] u(x,u(y,U))=u(D,u(I,u(x,y))). 95 [copy,94,flip.1] u(D,u(I,u(x,y)))=u(x,u(y,U)). 96 [para_from,77.1.1,7.1.1.1,demod,8,8,54] u(D,u(I,u(x,y)))=u(x,u(D,u(I,y))). 108 [para_into,18.1.1.1,23.1.1,flip.1] k(r(I),r(x))=r(x). 121,120 [para_into,108.1.1.2,14.1.1,demod,15] k(r(I),x)=x. 123,122 [para_into,120.1.1,70.1.1,demod,121,flip.1] k(I,x)=x. 125,124 [para_into,120.1.1,23.1.1] r(I)=I. 141,140 [back_demod,60,demod,125,125,43] u(D,u(I,I))=U. 157 [para_into,25.1.1.1.1,124.1.1,demod,123,123] u(c(x),c(x))=c(x). 181 [para_into,28.1.1.1.1,37.1.1] c(u(Z,c(x)))=n(U,x). 193 [para_into,28.1.1.1,5.1.1,demod,29] n(x,y)=n(y,x). 198 [para_from,193.1.1,3.1.1] -i(n(c($c1),r($c1)),D). 206 [para_from,157.1.1,28.1.1.1] c(c(x))=n(x,x). 210 [para_from,157.1.1,7.1.1.1,flip.1] u(c(x),u(c(x),y))=u(c(x),y). 215 [para_into,40.1.1.1.1.1,37.1.1] u(c(u(Z,x)),n(U,x))=U. 217 [para_into,40.1.1.1.1.1,31.1.1] u(c(u(D,x)),n(I,x))=I. 222,221 [para_into,40.1.1.1.1,77.1.1] u(c(u(D,u(I,c(x)))),n(x,U))=x. 229 [para_into,40.1.1.2,193.1.1] u(c(u(c(x),y)),n(y,x))=x. 495 [para_into,181.1.1.1.2,31.1.1] c(u(Z,D))=n(U,I). 2357 [hyper,210,2] i(c(x),u(c(x),y)). 2396 [para_into,2357.1.2,40.1.1] i(c(u(c(x),y)),x). 2399 [para_into,2396.1.1.1.1,495.1.1] i(c(u(n(U,I),x)),u(Z,D)). 2424 [para_into,2396.1.1,28.1.1] i(n(x,y),x). 2438 [hyper,2424,1] u(n(x,y),x)=x. 2440 [para_into,2424.1.1,193.1.1] i(n(x,y),y). 2491,2490 [hyper,2440,1] u(n(x,y),y)=y. 2581 [para_from,217.1.1,96.1.1.2.2,demod,141,flip.1] u(c(u(D,x)),u(D,u(I,n(I,x))))=U. 2722 [para_into,221.1.1.2,193.1.1] u(c(u(D,u(I,c(x)))),n(U,x))=x. 2730 [para_from,221.1.1,210.1.1.2,demod,222] u(c(u(D,u(I,c(x)))),x)=x. 2737 [para_from,221.1.1,95.1.1.2.2,demod,2491,flip.1] u(c(u(D,u(I,c(x)))),U)=u(D,u(I,x)). 2967 [para_into,229.1.1.1.1,215.1.1,demod,38] u(Z,n(n(U,x),u(Z,x)))=u(Z,x). 3043,3042 [para_into,2438.1.1,5.1.1] u(x,n(x,y))=x. 3049,3048 [back_demod,2581,demod,3043,43] u(c(u(D,x)),U)=U. 3051,3050 [back_demod,2737,demod,3049,flip.1] u(D,u(I,x))=U. 3067,3066 [back_demod,2730,demod,3051,38] u(Z,x)=x. 3075,3074 [back_demod,2722,demod,3051,38,3067] n(U,x)=x. 3155,3154 [back_demod,2967,demod,3075,3067,3067,3067] n(x,x)=x. 3170 [back_demod,2399,demod,3075,3067] i(c(u(I,x)),D). 3350 [back_demod,206,demod,3155] c(c(x))=x. 3552,3551 [para_from,3350.1.1,28.1.1.1.1] c(u(x,c(y)))=n(c(x),y). 3708 [para_into,3170.1.1.1,74.1.1,demod,3552] i(n(c(x),r(x)),D). 3709 [binary,3708.1,198.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 340 clauses generated 7983 clauses kept 2563 clauses forward subsumed 6110 clauses back subsumed 229 Kbytes malloced 2075 ----------- times (seconds) ----------- user CPU time 0.57 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 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 22 00:14:34 2003