----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sun Nov 30 01:40:18 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). assign(max_mem,64000). assign(max_weight,23). 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("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("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("monotLaws.txt"). ------- start included file monotLaws.txt------- include("1To3monotLaws.txt"). ------- start included file 1To3monotLaws.txt------- formula_list(usable). all x y z (u(x,y)=y->u(k(z,x),k(z,y))=k(z,y)). all x y z (u(x,y)=y->u(c(u(z,y)),c(x))=c(x)). all x y z (u(x,y)=y->u(k(x,z),k(y,z))=k(y,z)). end_of_list. -------> usable clausifies to: list(usable). 0 [] u(x,y)!=y|u(k(z,x),k(z,y))=k(z,y). 0 [] u(x,y)!=y|u(c(u(z,y)),c(x))=c(x). 0 [] u(x,y)!=y|u(k(x,z),k(y,z))=k(y,z). end_of_list. ------- end included file 1To3monotLaws.txt------- include("4_5monotLaws.txt"). ------- start included file 4_5monotLaws.txt------- formula_list(usable). all x y w v i(k(n(x,w),n(y,v)),k(x,y)). all x y w v i(k(n(x,w),n(y,v)),k(w,v)). end_of_list. -------> usable clausifies to: list(usable). 0 [] i(k(n(x,w),n(y,v)),k(x,y)). 0 [] i(k(n(x,w),n(y,v)),k(w,v)). end_of_list. ------- end included file 4_5monotLaws.txt------- ------- end included file monotLaws.txt------- include("xii.txt"). ------- start included file xii.txt------- formula_list(usable). all x y z (i(k(x,y),c(z))<->i(k(r(x),z),c(y))). all x y z (i(k(x,y),c(z))<->i(k(z,r(y)),c(x))). end_of_list. -------> usable clausifies to: list(usable). 0 [] -i(k(x,y),c(z))|i(k(r(x),z),c(y)). 0 [] i(k(x,y),c(z))| -i(k(r(x),z),c(y)). 0 [] -i(k(x,y),c(z))|i(k(z,r(y)),c(x)). 0 [] i(k(x,y),c(z))| -i(k(z,r(y)),c(x)). end_of_list. ------- end included file xii.txt------- include("xviii_ghost.txt"). ------- start included file xviii_ghost.txt------- formula_list(usable). -(all x y z (i(k(r(x),y),z)->i(k(x,c(z)),c(y)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] i(k(r($c3),$c2),$c1). 0 [] -i(k($c3,c($c1)),c($c2)). end_of_list. ------- end included file xviii_ghost.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=16): 3 [] u(x,y)!=y|u(k(z,x),k(z,y))=k(z,y). ** KEPT (pick-wt=15): 4 [] u(x,y)!=y|u(c(u(z,y)),c(x))=c(x). ** KEPT (pick-wt=16): 5 [] u(x,y)!=y|u(k(x,z),k(y,z))=k(y,z). ** KEPT (pick-wt=13): 6 [] -i(k(x,y),c(z))|i(k(r(x),z),c(y)). ** KEPT (pick-wt=13): 7 [] i(k(x,y),c(z))| -i(k(r(x),z),c(y)). ** KEPT (pick-wt=13): 8 [] -i(k(x,y),c(z))|i(k(z,r(y)),c(x)). ** KEPT (pick-wt=13): 9 [] i(k(x,y),c(z))| -i(k(z,r(y)),c(x)). ** KEPT (pick-wt=7): 10 [] -i(k($c3,c($c1)),c($c2)). ------------> process sos: ** KEPT (pick-wt=3): 11 [] x=x. ** KEPT (pick-wt=7): 12 [] u(x,y)=u(y,x). ** KEPT (pick-wt=11): 14 [copy,13,flip.1] u(u(x,y),z)=u(x,u(y,z)). ---> New Demodulator: 15 [new_demod,14] u(u(x,y),z)=u(x,u(y,z)). ** KEPT (pick-wt=14): 16 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ---> New Demodulator: 17 [new_demod,16] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ** KEPT (pick-wt=11): 19 [copy,18,flip.1] k(k(x,y),z)=k(x,k(y,z)). ---> New Demodulator: 20 [new_demod,19] k(k(x,y),z)=k(x,k(y,z)). ** KEPT (pick-wt=5): 21 [] r(r(x))=x. ---> New Demodulator: 22 [new_demod,21] r(r(x))=x. ** KEPT (pick-wt=10): 23 [] r(u(x,y))=u(r(x),r(y)). ---> New Demodulator: 24 [new_demod,23] r(u(x,y))=u(r(x),r(y)). ** KEPT (pick-wt=10): 25 [] r(k(x,y))=k(r(y),r(x)). ---> New Demodulator: 26 [new_demod,25] r(k(x,y))=k(r(y),r(x)). ** KEPT (pick-wt=5): 27 [] k(x,I)=x. ---> New Demodulator: 28 [new_demod,27] k(x,I)=x. ** KEPT (pick-wt=13): 29 [] u(k(r(x),c(k(x,y))),c(y))=c(y). ---> New Demodulator: 30 [new_demod,29] u(k(r(x),c(k(x,y))),c(y))=c(y). ** KEPT (pick-wt=4): 32 [copy,31,flip.1] c(I)=D. ---> New Demodulator: 33 [new_demod,32] c(I)=D. ** KEPT (pick-wt=5): 35 [copy,34,flip.1] u(I,D)=U. ---> New Demodulator: 36 [new_demod,35] u(I,D)=U. ** KEPT (pick-wt=4): 38 [copy,37,flip.1] c(U)=Z. ---> New Demodulator: 39 [new_demod,38] c(U)=Z. ** KEPT (pick-wt=11): 40 [] i(k(n(x,y),n(z,u)),k(x,z)). ** KEPT (pick-wt=11): 41 [] i(k(n(x,y),n(z,u)),k(y,u)). ** KEPT (pick-wt=6): 42 [] i(k(r($c3),$c2),$c1). Following clause subsumed by 11 during input processing: 0 [copy,11,flip.1] x=x. Following clause subsumed by 12 during input processing: 0 [copy,12,flip.1] u(x,y)=u(y,x). >>>> Starting back demodulation with 15. >>>> Starting back demodulation with 17. >>>> Starting back demodulation with 20. >>>> Starting back demodulation with 22. >>>> Starting back demodulation with 24. >>>> Starting back demodulation with 26. >>>> Starting back demodulation with 28. >>>> Starting back demodulation with 30. >>>> Starting back demodulation with 33. >>>> Starting back demodulation with 36. >>>> Starting back demodulation with 39. ======= end of input processing ======= =========== start of search =========== ----> UNIT CONFLICT at 11.83 sec ----> 31467 [binary,31466.1,10.1] $F. Length of proof is 69. Level of proof is 21. ---------------- PROOF ---------------- 1 [] -i(x,y)|u(x,y)=y. 2 [] i(x,y)|u(x,y)!=y. 3 [] u(x,y)!=y|u(k(z,x),k(z,y))=k(z,y). 4 [] u(x,y)!=y|u(c(u(z,y)),c(x))=c(x). 10 [] -i(k($c3,c($c1)),c($c2)). 12 [] u(x,y)=u(y,x). 13 [] u(x,u(y,z))=u(u(x,y),z). 15,14 [copy,13,flip.1] u(u(x,y),z)=u(x,u(y,z)). 16 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 18 [] k(x,k(y,z))=k(k(x,y),z). 19 [copy,18,flip.1] k(k(x,y),z)=k(x,k(y,z)). 22,21 [] r(r(x))=x. 25 [] r(k(x,y))=k(r(y),r(x)). 27 [] k(x,I)=x. 29 [] u(k(r(x),c(k(x,y))),c(y))=c(y). 31 [] D=c(I). 33,32 [copy,31,flip.1] c(I)=D. 34 [] U=u(I,D). 36,35 [copy,34,flip.1] u(I,D)=U. 37 [] Z=c(U). 39,38 [copy,37,flip.1] c(U)=Z. 42 [] i(k(r($c3),$c2),$c1). 43 [para_into,35.1.1,12.1.1] u(D,I)=U. 45 [hyper,42,1] u(k(r($c3),$c2),$c1)=$c1. 49 [hyper,45,4] u(c(u(x,$c1)),c(k(r($c3),$c2)))=c(k(r($c3),$c2)). 58,57 [para_into,14.1.1.1,43.1.1] u(U,x)=u(D,u(I,x)). 61 [para_into,14.1.1.1,12.1.1,demod,15] u(x,u(y,z))=u(y,u(x,z)). 62 [para_into,14.1.1,12.1.1] u(x,u(y,z))=u(y,u(z,x)). 63 [copy,62,flip.1] u(x,u(y,z))=u(z,u(x,y)). 66 [para_into,57.1.1,12.1.1] u(x,U)=u(D,u(I,x)). 67 [copy,66,flip.1] u(D,u(I,x))=u(x,U). 68 [para_into,66.1.1,14.1.1] u(x,u(y,U))=u(D,u(I,u(x,y))). 69 [copy,68,flip.1] u(D,u(I,u(x,y)))=u(x,u(y,U)). 74 [para_into,67.1.1.2,12.1.1] u(D,u(x,I))=u(x,U). 75 [para_into,67.1.1,12.1.1,demod,15] u(I,u(x,D))=u(x,U). 76 [copy,74,flip.1] u(x,U)=u(D,u(x,I)). 77 [copy,75,flip.1] u(x,U)=u(I,u(x,D)). 78 [para_into,16.1.1.1.1.1,38.1.1,demod,39] u(c(u(Z,x)),c(u(Z,c(x))))=U. 80 [para_into,16.1.1.1.1.1,32.1.1,demod,33] u(c(u(D,x)),c(u(D,c(x))))=I. 82 [para_into,16.1.1.1.1,66.1.1,demod,39] u(c(u(D,u(I,c(x)))),c(u(c(x),Z)))=x. 86 [para_into,16.1.1.1.1,12.1.1] u(c(u(x,c(y))),c(u(c(y),c(x))))=y. 94 [para_into,16.1.1.2.1,12.1.1] u(c(u(c(x),y)),c(u(c(y),c(x))))=x. 114 [para_into,19.1.1.1,27.1.1,flip.1] k(x,k(I,y))=k(x,y). 134 [para_into,25.1.1.1,27.1.1,flip.1] k(r(I),r(x))=r(x). 149 [para_into,29.1.1.1.1,21.1.1] u(k(x,c(k(r(x),y))),c(y))=c(y). 170,169 [para_into,134.1.1.2,21.1.1,demod,22] k(r(I),x)=x. 172,171 [para_into,169.1.1,114.1.1,demod,170,flip.1] k(I,x)=x. 173 [para_into,169.1.1,27.1.1] r(I)=I. 179 [para_from,173.1.1,29.1.1.1.1,demod,172,172] u(c(x),c(x))=c(x). 186,185 [hyper,179,4] u(c(u(x,c(y))),c(c(y)))=c(c(y)). 191,190 [para_into,179.1.1.1,38.1.1,demod,39,39] u(Z,Z)=Z. 193,192 [para_into,179.1.1.1,32.1.1,demod,33,33] u(D,D)=D. 208 [hyper,190,4] u(c(u(x,Z)),c(Z))=c(Z). 214 [para_from,190.1.1,14.1.1.1,flip.1] u(Z,u(Z,x))=u(Z,x). 222 [para_from,192.1.1,75.1.1.2,demod,36,flip.1] u(D,U)=U. 270 [hyper,49,3] u(k(x,c(u(y,$c1))),k(x,c(k(r($c3),$c2))))=k(x,c(k(r($c3),$c2))). 378,377 [para_into,61.1.1.2,222.1.1,flip.1] u(D,u(x,U))=u(x,U). 416,415 [hyper,214,4] u(c(u(x,u(Z,y))),c(Z))=c(Z). 419 [hyper,214,2] i(Z,u(Z,x)). 431 [para_into,419.1.2,61.1.1] i(Z,u(x,u(Z,y))). 755,754 [para_into,78.1.1.1.1,77.1.1,demod,39,191,416] c(Z)=U. 787,786 [back_demod,208,demod,755,755] u(c(u(x,Z)),U)=U. 810 [para_from,754.1.1,179.1.1.2,demod,755,58,378,755] u(I,U)=U. 832,831 [para_into,810.1.1,76.1.1] u(D,u(I,I))=U. 873,872 [para_into,80.1.1.1.1,43.1.1,demod,39,33,193] u(Z,c(D))=I. 902 [para_from,872.1.1,431.1.2.2] i(Z,u(x,I)). 906 [para_from,872.1.1,214.1.1.2,demod,873] u(Z,I)=I. 941 [para_from,82.1.1,69.1.1.2.2,demod,787,flip.1] u(c(u(D,u(I,c(x)))),U)=u(D,u(I,x)). 949 [para_into,902.1.2,57.1.1,demod,832] i(Z,U). 951 [hyper,949,1] u(Z,U)=U. 957 [hyper,906,4,demod,755,755] u(c(u(x,I)),U)=U. 1010 [hyper,951,4,demod,755,755] u(c(u(x,U)),U)=U. 1076,1075 [para_into,86.1.1.2.1,179.1.1,demod,186] c(c(x))=x. 1339 [para_into,94.1.1.1.1,68.1.1] u(c(u(D,u(I,u(c(x),y)))),c(u(c(u(y,U)),c(x))))=x. 1871 [para_from,957.1.1,68.1.1.2,flip.1] u(D,u(I,u(x,c(u(y,I)))))=u(x,U). 1906,1905 [para_into,1010.1.1.1.1,66.1.1] u(c(u(D,u(I,x))),U)=U. 1910,1909 [back_demod,941,demod,1906,flip.1] u(D,u(I,x))=U. 1914,1913 [back_demod,1871,demod,1910,flip.1] u(x,U)=U. 1929 [back_demod,1339,demod,1910,39,1914,39] u(Z,c(u(Z,c(x))))=x. 1995,1994 [hyper,1913,4,demod,1914,39] u(Z,c(x))=c(x). 2009 [back_demod,1929,demod,1995,1076] u(Z,x)=x. 2393,2392 [para_into,149.1.1,12.1.1] u(c(x),k(y,c(k(r(y),x))))=c(x). 2394 [para_from,149.1.1,63.1.1.2,flip.1] u(c(x),u(y,k(z,c(k(r(z),x)))))=u(y,c(x)). 2853 [para_into,270.1.1.1.2.1,2009.1.1] u(k(x,c($c1)),k(x,c(k(r($c3),$c2))))=k(x,c(k(r($c3),$c2))). 31406 [para_from,2853.1.1,2394.1.1.2,demod,2393,flip.1] u(k($c3,c($c1)),c($c2))=c($c2). 31466 [hyper,31406,2] i(k($c3,c($c1)),c($c2)). 31467 [binary,31466.1,10.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 1662 clauses generated 212238 clauses kept 22262 clauses forward subsumed 185153 clauses back subsumed 574 Kbytes malloced 16988 ----------- times (seconds) ----------- user CPU time 12.03 (0 hr, 0 min, 12 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 12 (0 hr, 0 min, 12 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 01:40:30 2003