----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sun Nov 30 15:29: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_distinct_vars,3). 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("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("15_16booleanLaws.txt"). ------- start included file 15_16booleanLaws.txt------- formula_list(usable). all x (c(c(x))=x). all x y (u(x,y)=y->c(u(y,c(x)))=Z). all x y (c(u(y,c(x)))=Z->u(x,y)=y). end_of_list. -------> usable clausifies to: list(usable). 0 [] c(c(x))=x. 0 [] u(x,y)!=y|c(u(y,c(x)))=Z. 0 [] c(u(y,c(x)))!=Z|u(x,y)=y. end_of_list. ------- end included file 15_16booleanLaws.txt------- include("i.txt"). ------- start included file i.txt------- formula_list(usable). all x y (i(x,y)->i(r(x),r(y))). all x y (r(u(x,y))=u(r(x),r(y))). all x (r(c(x))=c(r(x))). all x y (r(n(x,y))=n(r(x),r(y))). all x (r(r(x))=x). all x y (r(d(x,y))=d(r(y),r(x))). all x y (r(k(x,y))=k(r(y),r(x))). r(I)=I. r(Z)=Z. r(U)=U. end_of_list. -------> usable clausifies to: list(usable). 0 [] -i(x,y)|i(r(x),r(y)). 0 [] r(u(x,y))=u(r(x),r(y)). 0 [] r(c(x))=c(r(x)). 0 [] r(n(x,y))=n(r(x),r(y)). 0 [] r(r(x))=x. 0 [] r(d(x,y))=d(r(y),r(x)). 0 [] r(k(x,y))=k(r(y),r(x)). 0 [] r(I)=I. 0 [] r(Z)=Z. 0 [] r(U)=U. end_of_list. ------- end included file i.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("xix_a_ghost.txt"). ------- start included file xix_a_ghost.txt------- formula_list(usable). all x y (k(c(x),c(r(y)))=Z<->i(k(U,c(x)),y)). all x y (c(k(c(x),c(r(y))))=U<->i(k(U,c(x)),y)). all x y (i(x,y)<->u(c(x),y)=U). -(all x y (c(k(c(x),c(r(y))))=U<->u(c(k(U,c(x))),y)=U)). end_of_list. -------> usable clausifies to: list(usable). 0 [] k(c(x),c(r(y)))!=Z|i(k(U,c(x)),y). 0 [] k(c(x),c(r(y)))=Z| -i(k(U,c(x)),y). 0 [] c(k(c(x),c(r(y))))!=U|i(k(U,c(x)),y). 0 [] c(k(c(x),c(r(y))))=U| -i(k(U,c(x)),y). 0 [] -i(x,y)|u(c(x),y)=U. 0 [] i(x,y)|u(c(x),y)!=U. 0 [] c(k(c($c2),c(r($c1))))=U|u(c(k(U,c($c2))),$c1)=U. 0 [] c(k(c($c2),c(r($c1))))!=U|u(c(k(U,c($c2))),$c1)!=U. end_of_list. ------- end included file xix_a_ghost.txt------- SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=2. This ia a non-Horn set with equality. The strategy will be Knuth-Bendix, ordered hyper_res, factoring, and unit deletion, 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: set(unit_deletion). dependent: set(factor). ------------> 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=12): 3 [] u(x,y)!=y|c(u(y,c(x)))=Z. ** KEPT (pick-wt=12): 4 [] c(u(x,c(y)))!=Z|u(y,x)=x. ** KEPT (pick-wt=8): 5 [] -i(x,y)|i(r(x),r(y)). ** 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=14): 10 [] k(c(x),c(r(y)))!=Z|i(k(U,c(x)),y). ** KEPT (pick-wt=14): 11 [] k(c(x),c(r(y)))=Z| -i(k(U,c(x)),y). ** KEPT (pick-wt=15): 12 [] c(k(c(x),c(r(y))))!=U|i(k(U,c(x)),y). ** KEPT (pick-wt=15): 13 [] c(k(c(x),c(r(y))))=U| -i(k(U,c(x)),y). ** KEPT (pick-wt=9): 14 [] -i(x,y)|u(c(x),y)=U. ** KEPT (pick-wt=9): 15 [] i(x,y)|u(c(x),y)!=U. ** KEPT (pick-wt=18): 16 [] c(k(c($c2),c(r($c1))))!=U|u(c(k(U,c($c2))),$c1)!=U. ------------> process sos: ** KEPT (pick-wt=4): 18 [copy,17,flip.1] c(I)=D. ---> New Demodulator: 19 [new_demod,18] c(I)=D. ** KEPT (pick-wt=5): 21 [copy,20,flip.1] u(I,D)=U. ---> New Demodulator: 22 [new_demod,21] u(I,D)=U. ** KEPT (pick-wt=4): 24 [copy,23,flip.1] c(U)=Z. ---> New Demodulator: 25 [new_demod,24] c(U)=Z. ** KEPT (pick-wt=7): 26 [] u(x,y)=u(y,x). ** KEPT (pick-wt=11): 28 [copy,27,flip.1] u(u(x,y),z)=u(x,u(y,z)). ---> New Demodulator: 29 [new_demod,28] u(u(x,y),z)=u(x,u(y,z)). ** KEPT (pick-wt=14): 30 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ---> New Demodulator: 31 [new_demod,30] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ** KEPT (pick-wt=5): 32 [] c(c(x))=x. ---> New Demodulator: 33 [new_demod,32] c(c(x))=x. ** KEPT (pick-wt=10): 34 [] r(u(x,y))=u(r(x),r(y)). ---> New Demodulator: 35 [new_demod,34] r(u(x,y))=u(r(x),r(y)). ** KEPT (pick-wt=7): 36 [] r(c(x))=c(r(x)). ---> New Demodulator: 37 [new_demod,36] r(c(x))=c(r(x)). ** KEPT (pick-wt=10): 38 [] r(n(x,y))=n(r(x),r(y)). ---> New Demodulator: 39 [new_demod,38] r(n(x,y))=n(r(x),r(y)). ** KEPT (pick-wt=5): 40 [] r(r(x))=x. ---> New Demodulator: 41 [new_demod,40] r(r(x))=x. ** KEPT (pick-wt=10): 42 [] r(d(x,y))=d(r(y),r(x)). ---> New Demodulator: 43 [new_demod,42] r(d(x,y))=d(r(y),r(x)). ** KEPT (pick-wt=10): 44 [] r(k(x,y))=k(r(y),r(x)). ---> New Demodulator: 45 [new_demod,44] r(k(x,y))=k(r(y),r(x)). ** KEPT (pick-wt=4): 46 [] r(I)=I. ---> New Demodulator: 47 [new_demod,46] r(I)=I. ** KEPT (pick-wt=4): 48 [] r(Z)=Z. ---> New Demodulator: 49 [new_demod,48] r(Z)=Z. ** KEPT (pick-wt=4): 50 [] r(U)=U. ---> New Demodulator: 51 [new_demod,50] r(U)=U. ** KEPT (pick-wt=18): 52 [] c(k(c($c2),c(r($c1))))=U|u(c(k(U,c($c2))),$c1)=U. >>>> Starting back demodulation with 19. >>>> Starting back demodulation with 22. >>>> Starting back demodulation with 25. Following clause subsumed by 26 during input processing: 0 [copy,26,flip.1] u(x,y)=u(y,x). >>>> Starting back demodulation with 29. >>>> Starting back demodulation with 31. >>>> Starting back demodulation with 33. >>>> Starting back demodulation with 35. >>>> Starting back demodulation with 37. >>>> Starting back demodulation with 39. >>>> Starting back demodulation with 41. >>>> Starting back demodulation with 43. >>>> Starting back demodulation with 45. >>>> Starting back demodulation with 47. >>>> Starting back demodulation with 49. >>>> Starting back demodulation with 51. ======= end of input processing ======= =========== start of search =========== Resetting weight limit to 9. sos_size=5082 Resetting weight limit to 8. sos_size=4967 ----> UNIT CONFLICT at 45.06 sec ----> 9172 [binary,9171.1,8821.1] $F. Length of proof is 60. Level of proof is 19. ---------------- PROOF ---------------- 1 [] -i(x,y)|u(x,y)=y. 2 [] i(x,y)|u(x,y)!=y. 3 [] u(x,y)!=y|c(u(y,c(x)))=Z. 4 [] c(u(x,c(y)))!=Z|u(y,x)=x. 6 [] -i(k(x,y),c(z))|i(k(r(x),z),c(y)). 12 [] c(k(c(x),c(r(y))))!=U|i(k(U,c(x)),y). 13 [] c(k(c(x),c(r(y))))=U| -i(k(U,c(x)),y). 14 [] -i(x,y)|u(c(x),y)=U. 15 [] i(x,y)|u(c(x),y)!=U. 16 [] c(k(c($c2),c(r($c1))))!=U|u(c(k(U,c($c2))),$c1)!=U. 17 [] D=c(I). 19,18 [copy,17,flip.1] c(I)=D. 20 [] U=u(I,D). 22,21 [copy,20,flip.1] u(I,D)=U. 23 [] Z=c(U). 25,24 [copy,23,flip.1] c(U)=Z. 26 [] u(x,y)=u(y,x). 27 [] u(x,u(y,z))=u(u(x,y),z). 29,28 [copy,27,flip.1] u(u(x,y),z)=u(x,u(y,z)). 30 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 33,32 [] c(c(x))=x. 37,36 [] r(c(x))=c(r(x)). 41,40 [] r(r(x))=x. 45,44 [] r(k(x,y))=k(r(y),r(x)). 51,50 [] r(U)=U. 52 [] c(k(c($c2),c(r($c1))))=U|u(c(k(U,c($c2))),$c1)=U. 60 [para_from,18.1.1,4.1.1.1.2] c(u(x,D))!=Z|u(I,x)=x. 61 [para_from,18.1.1,15.2.1.1] i(I,x)|u(D,x)!=U. 62 [para_from,18.1.1,14.2.1.1] -i(I,x)|u(D,x)=U. 118 [para_into,26.1.1,21.1.1,flip.1] u(D,I)=U. 120 [para_into,26.1.1,14.2.1,flip.1] u(x,c(y))=U| -i(y,x). 122 [para_into,26.1.1,1.2.1,flip.1] u(x,y)=x| -i(y,x). 123 [para_from,26.1.1,16.2.1] c(k(c($c2),c(r($c1))))!=U|u($c1,c(k(U,c($c2))))!=U. 124 [para_from,26.1.1,15.2.1] i(x,y)|u(y,c(x))!=U. 125 [para_from,26.1.1,4.1.1.1] c(u(c(x),y))!=Z|u(x,y)=y. 126 [para_from,26.1.1,3.2.1.1] u(x,y)!=y|c(u(c(x),y))=Z. 131,130 [para_into,32.1.1.1,24.1.1] c(Z)=U. 132 [para_into,32.1.1.1,18.1.1] c(D)=I. 135 [para_into,32.1.1,32.1.1] x=x. 143 [para_from,32.1.1,6.1.2] -i(k(x,y),z)|i(k(r(x),c(z)),c(y)). 148 [para_from,32.1.1,14.2.1.1] -i(c(x),y)|u(x,y)=U. 150 [para_from,32.1.1,13.2.1.2,demod,33] c(k(x,c(r(y))))=U| -i(k(U,x),y). 151 [para_from,32.1.1,12.2.1.2,demod,33] c(k(x,c(r(y))))!=U|i(k(U,x),y). 175 [para_from,132.1.1,15.2.1.1] i(D,x)|u(I,x)!=U. 182,181 [para_into,28.1.1.1,21.1.1] u(U,x)=u(I,u(D,x)). 207 [hyper,30,15,demod,25,25] i(u(Z,x),c(u(Z,c(x)))). 364 [hyper,52,15] c(k(c($c2),c(r($c1))))=U|i(k(U,c($c2)),$c1). 377 [para_from,52.1.1,36.1.1.1,demod,51,45,37,41,37,flip.1] c(k(c($c1),c(r($c2))))=U|u(c(k(U,c($c2))),$c1)=U. 476 [hyper,61,118] i(I,I). 480 [hyper,476,1] u(I,I)=I. 484 [para_from,480.1.1,28.1.1.1,flip.1] u(I,u(I,x))=u(I,x). 602 [hyper,175,21] i(D,D). 619,618 [hyper,602,122] u(D,D)=D. 1281 [para_from,120.1.1,15.2.1,unit_del,135] i(x,c(y))| -i(y,c(x)). 1352 [para_into,1281.2.2,32.1.1] i(c(x),c(y))| -i(y,x). 1430 [para_into,124.2.1.2,130.1.1] i(Z,x)|u(x,U)!=U. 1448 [para_into,1430.2.1,60.2.1,demod,182,619,22,25,unit_del,135,135] i(Z,I). 1450 [para_into,1430.2.1,4.2.1,demod,182,unit_del,135] i(Z,x)|c(u(I,u(D,c(x))))!=Z. 1472 [hyper,1448,1352,demod,19,131] i(D,U). 1482 [hyper,1472,1] u(D,U)=U. 1523 [para_from,1482.1.1,28.1.1.1,demod,182,182,flip.1] u(D,u(I,u(D,x)))=u(I,u(D,x)). 2077 [para_into,123.2.1,120.1.1,unit_del,135] c(k(c($c2),c(r($c1))))!=U| -i(k(U,c($c2)),$c1). 2082 [para_into,125.1.1.1.1,130.1.1,demod,182] c(u(I,u(D,x)))!=Z|u(Z,x)=x. 2847 [hyper,207,120] u(c(u(Z,c(x))),c(u(Z,x)))=U. 2849 [hyper,207,1,demod,29] u(Z,u(x,c(u(Z,c(x)))))=c(u(Z,c(x))). 3311 [hyper,484,2] i(I,u(I,x)). 3323,3322 [hyper,3311,62] u(D,u(I,x))=U. 3326,3325 [back_demod,1523,demod,3323,flip.1] u(I,u(D,x))=U. 3353,3352 [back_demod,2082,demod,3326,25,unit_del,135] u(Z,x)=x. 3354 [back_demod,1450,demod,3326,25,unit_del,135] i(Z,x). 3425 [back_demod,2849,demod,3353,33,3353,3353,33] u(x,x)=x. 3428,3427 [back_demod,2847,demod,3353,33,3353] u(x,c(x))=U. 3587 [para_into,3425.1.1,148.2.1] U=x| -i(c(x),x). 3592 [para_from,3425.1.1,126.2.1.1,demod,3428,33,flip.1] c(x)!=U|x=Z. 6593 [para_from,3592.2.1,3587.2.1,demod,33,unit_del,3354] U=x|x!=U. 6708 [para_from,6593.1.1,16.2.1.1.1.1] c(k(c($c2),c(r($c1))))!=U|u(c(k(x,c($c2))),$c1)!=U|x!=U. 6711 [factor,6708.1.3] c(k(c($c2),c(r($c1))))!=U|u(c(k(c(k(c($c2),c(r($c1)))),c($c2))),$c1)!=U. 8795,8794 [hyper,364,150,factor_simp] c(k(c($c2),c(r($c1))))=U. 8799 [back_demod,6711,demod,8795,8795,unit_del,135] u(c(k(U,c($c2))),$c1)!=U. 8821 [back_demod,2077,demod,8795,unit_del,135] -i(k(U,c($c2)),$c1). 9048 [hyper,377,151,unit_del,8799] i(k(U,c($c1)),$c2). 9171 [hyper,9048,143,demod,51,33] i(k(U,c($c2)),$c1). 9172 [binary,9171.1,8821.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 854 clauses generated 107953 clauses kept 9041 clauses forward subsumed 46187 clauses back subsumed 2766 Kbytes malloced 4374 ----------- times (seconds) ----------- user CPU time 45.27 (0 hr, 0 min, 45 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 45 (0 hr, 0 min, 45 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 15:30:03 2003