----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sun Nov 30 15:34:57 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("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("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("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("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("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("11booleanLaws.txt"). ------- start included file 11booleanLaws.txt------- formula_list(usable). all x y (c(n(x,y))=u(c(x),c(y))). all x y (c(u(x,y))=n(c(x),c(y))). end_of_list. -------> usable clausifies to: list(usable). 0 [] c(n(x,y))=u(c(x),c(y)). 0 [] c(u(x,y))=n(c(x),c(y)). end_of_list. ------- end included file 11booleanLaws.txt------- include("cycleLawC.txt"). ------- start included file cycleLawC.txt------- formula_list(usable). all x y z (n(y,k(n(x,k(y,r(z))),z))=n(k(x,z),y)). end_of_list. -------> usable clausifies to: list(usable). 0 [] n(y,k(n(x,k(y,r(z))),z))=n(k(x,z),y). end_of_list. ------- end included file cycleLawC.txt------- include("xix_b_ghost.txt"). ------- start included file xix_b_ghost.txt------- formula_list(usable). all x y (k(x,r(y))=Z->n(k(U,x),k(U,y))=Z). -(all x y (n(k(U,x),k(U,y))=Z->k(x,r(y))=Z)). end_of_list. -------> usable clausifies to: list(usable). 0 [] k(x,r(y))!=Z|n(k(U,x),k(U,y))=Z. 0 [] n(k(U,$c2),k(U,$c1))=Z. 0 [] k($c2,r($c1))!=Z. end_of_list. ------- end included file xix_b_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=12): 1 [] u(x,y)!=y|c(u(y,c(x)))=Z. ** KEPT (pick-wt=12): 2 [] c(u(x,c(y)))!=Z|u(y,x)=x. ** KEPT (pick-wt=8): 3 [] -i(x,y)|i(r(x),r(y)). ** KEPT (pick-wt=15): 4 [] k(x,r(y))!=Z|n(k(U,x),k(U,y))=Z. ** KEPT (pick-wt=6): 5 [] k($c2,r($c1))!=Z. ------------> process sos: ** KEPT (pick-wt=10): 7 [copy,6,flip.1] c(u(c(x),c(y)))=n(x,y). ---> New Demodulator: 8 [new_demod,7] c(u(c(x),c(y)))=n(x,y). ** KEPT (pick-wt=10): 10 [copy,9,flip.1] c(k(c(x),c(y)))=d(x,y). ---> New Demodulator: 11 [new_demod,10] c(k(c(x),c(y)))=d(x,y). ** KEPT (pick-wt=4): 13 [copy,12,flip.1] c(I)=D. ---> New Demodulator: 14 [new_demod,13] c(I)=D. ** KEPT (pick-wt=5): 16 [copy,15,flip.1] u(I,D)=U. ---> New Demodulator: 17 [new_demod,16] u(I,D)=U. ** KEPT (pick-wt=4): 19 [copy,18,flip.1] c(U)=Z. ---> New Demodulator: 20 [new_demod,19] c(U)=Z. ** KEPT (pick-wt=7): 21 [] u(x,y)=u(y,x). ** KEPT (pick-wt=11): 23 [copy,22,flip.1] u(u(x,y),z)=u(x,u(y,z)). ---> New Demodulator: 24 [new_demod,23] u(u(x,y),z)=u(x,u(y,z)). ** KEPT (pick-wt=11): 26 [copy,25,demod,8] u(c(u(c(x),y)),n(x,y))=x. ---> New Demodulator: 27 [new_demod,26] u(c(u(c(x),y)),n(x,y))=x. ** KEPT (pick-wt=11): 29 [copy,28,flip.1] k(k(x,y),z)=k(x,k(y,z)). ---> New Demodulator: 30 [new_demod,29] k(k(x,y),z)=k(x,k(y,z)). ** KEPT (pick-wt=5): 31 [] r(r(x))=x. ---> New Demodulator: 32 [new_demod,31] r(r(x))=x. ** KEPT (pick-wt=10): 33 [] r(u(x,y))=u(r(x),r(y)). ---> New Demodulator: 34 [new_demod,33] r(u(x,y))=u(r(x),r(y)). ** KEPT (pick-wt=10): 35 [] r(k(x,y))=k(r(y),r(x)). ---> New Demodulator: 36 [new_demod,35] r(k(x,y))=k(r(y),r(x)). ** KEPT (pick-wt=5): 37 [] k(x,I)=x. ---> New Demodulator: 38 [new_demod,37] k(x,I)=x. ** KEPT (pick-wt=13): 39 [] u(k(r(x),c(k(x,y))),c(y))=c(y). ---> New Demodulator: 40 [new_demod,39] u(k(r(x),c(k(x,y))),c(y))=c(y). ** KEPT (pick-wt=5): 41 [] c(c(x))=x. ---> New Demodulator: 42 [new_demod,41] c(c(x))=x. ** KEPT (pick-wt=11): 44 [copy,43,demod,34] u(r(x),r(y))=u(r(x),r(y)). ** KEPT (pick-wt=7): 45 [] r(c(x))=c(r(x)). ---> New Demodulator: 46 [new_demod,45] r(c(x))=c(r(x)). ** KEPT (pick-wt=10): 47 [] r(n(x,y))=n(r(x),r(y)). ---> New Demodulator: 48 [new_demod,47] r(n(x,y))=n(r(x),r(y)). ** KEPT (pick-wt=3): 50 [copy,49,demod,32] x=x. ** KEPT (pick-wt=10): 51 [] r(d(x,y))=d(r(y),r(x)). ---> New Demodulator: 52 [new_demod,51] r(d(x,y))=d(r(y),r(x)). Following clause subsumed by 50 during input processing: 0 [demod,36] k(r(y),r(x))=k(r(y),r(x)). ** KEPT (pick-wt=4): 53 [] r(I)=I. ---> New Demodulator: 54 [new_demod,53] r(I)=I. ** KEPT (pick-wt=4): 55 [] r(Z)=Z. ---> New Demodulator: 56 [new_demod,55] r(Z)=Z. ** KEPT (pick-wt=4): 57 [] r(U)=U. ---> New Demodulator: 58 [new_demod,57] r(U)=U. ** KEPT (pick-wt=10): 59 [] c(n(x,y))=u(c(x),c(y)). ---> New Demodulator: 60 [new_demod,59] c(n(x,y))=u(c(x),c(y)). ** KEPT (pick-wt=10): 61 [] c(u(x,y))=n(c(x),c(y)). ---> New Demodulator: 62 [new_demod,61] c(u(x,y))=n(c(x),c(y)). ** KEPT (pick-wt=16): 63 [] n(x,k(n(y,k(x,r(z))),z))=n(k(y,z),x). ** KEPT (pick-wt=9): 64 [] n(k(U,$c2),k(U,$c1))=Z. ---> New Demodulator: 65 [new_demod,64] n(k(U,$c2),k(U,$c1))=Z. >>>> Starting back demodulation with 8. >>>> Starting back demodulation with 11. >>>> Starting back demodulation with 14. >>>> Starting back demodulation with 17. >>>> Starting back demodulation with 20. Following clause subsumed by 21 during input processing: 0 [copy,21,flip.1] u(x,y)=u(y,x). >>>> Starting back demodulation with 24. >>>> Starting back demodulation with 27. >>>> Starting back demodulation with 30. >>>> Starting back demodulation with 32. >>>> Starting back demodulation with 34. >>>> Starting back demodulation with 36. >>>> Starting back demodulation with 38. >>>> Starting back demodulation with 40. >>>> Starting back demodulation with 42. Following clause subsumed by 50 during input processing: 0 [copy,44,flip.1] u(r(x),r(y))=u(r(x),r(y)). >>>> Starting back demodulation with 46. >>>> Starting back demodulation with 48. Following clause subsumed by 50 during input processing: 0 [copy,50,flip.1] x=x. 50 back subsumes 44. >>>> Starting back demodulation with 52. >>>> Starting back demodulation with 54. >>>> Starting back demodulation with 56. >>>> Starting back demodulation with 58. >>>> Starting back demodulation with 60. >>>> Starting back demodulation with 62. >> back demodulating 26 with 62. >> back demodulating 7 with 62. >> back demodulating 2 with 62. >> back demodulating 1 with 62. ** KEPT (pick-wt=16): 70 [copy,63,flip.1] n(k(x,y),z)=n(z,k(n(x,k(z,r(y))),y)). >>>> Starting back demodulation with 65. >>>> Starting back demodulation with 67. Following clause subsumed by 63 during input processing: 0 [copy,70,flip.1] n(x,k(n(y,k(x,r(z))),z))=n(k(y,z),x). ======= end of input processing ======= =========== start of search =========== Resetting weight limit to 10. sos_size=5217 Resetting weight limit to 9. sos_size=5267 ----> UNIT CONFLICT at 10.03 sec ----> 8537 [binary,8535.1,5.1] $F. Length of proof is 57. Level of proof is 24. ---------------- PROOF ---------------- 1 [] u(x,y)!=y|c(u(y,c(x)))=Z. 4 [] k(x,r(y))!=Z|n(k(U,x),k(U,y))=Z. 5 [] k($c2,r($c1))!=Z. 6 [] n(x,y)=c(u(c(x),c(y))). 8,7 [copy,6,flip.1] c(u(c(x),c(y)))=n(x,y). 9 [] d(x,y)=c(k(c(x),c(y))). 10 [copy,9,flip.1] c(k(c(x),c(y)))=d(x,y). 18 [] Z=c(U). 20,19 [copy,18,flip.1] c(U)=Z. 21 [] u(x,y)=u(y,x). 25 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 26 [copy,25,demod,8] u(c(u(c(x),y)),n(x,y))=x. 28 [] k(x,k(y,z))=k(k(x,y),z). 30,29 [copy,28,flip.1] k(k(x,y),z)=k(x,k(y,z)). 32,31 [] r(r(x))=x. 36,35 [] r(k(x,y))=k(r(y),r(x)). 38,37 [] k(x,I)=x. 39 [] u(k(r(x),c(k(x,y))),c(y))=c(y). 42,41 [] c(c(x))=x. 47 [] r(n(x,y))=n(r(x),r(y)). 52,51 [] r(d(x,y))=d(r(y),r(x)). 54,53 [] r(I)=I. 56,55 [] r(Z)=Z. 58,57 [] r(U)=U. 59 [] c(n(x,y))=u(c(x),c(y)). 62,61 [] c(u(x,y))=n(c(x),c(y)). 63 [] n(x,k(n(y,k(x,r(z))),z))=n(k(y,z),x). 64 [] n(k(U,$c2),k(U,$c1))=Z. 66 [back_demod,26,demod,62,42] u(n(x,c(y)),n(x,y))=x. 69 [back_demod,1,demod,62,42] u(x,y)!=y|n(c(y),x)=Z. 70 [copy,63,flip.1] n(k(x,y),z)=n(z,k(n(x,k(z,r(y))),y)). 83 [para_from,53.1.1,4.1.1.2,demod,38,38] x!=Z|n(k(U,x),U)=Z. 99,98 [para_into,41.1.1.1,19.1.1] c(Z)=U. 104 [para_from,41.1.1,10.1.1.1.2] c(k(c(x),y))=d(x,c(y)). 107,106 [para_from,41.1.1,10.1.1.1.1] c(k(x,c(y)))=d(c(x),y). 157 [para_into,35.1.1.1,37.1.1,demod,54,flip.1] k(I,r(x))=r(x). 191 [para_into,39.1.1.1.1,53.1.1] u(k(I,c(k(I,x))),c(x))=c(x). 209 [para_into,39.1.1.2,19.1.1,demod,20] u(k(r(x),c(k(x,U))),Z)=Z. 236,235 [para_into,157.1.1.2,31.1.1,demod,32] k(I,x)=x. 237 [back_demod,191,demod,236,236] u(c(x),c(x))=c(x). 283,282 [para_into,237.1.1.1,41.1.1,demod,42,42] u(x,x)=x. 350 [para_into,61.1.1.1,282.1.1,flip.1] n(c(x),c(x))=c(x). 356 [para_into,61.1.1.1,39.1.1,demod,42,107,42,flip.1] n(d(c(r(x)),k(x,y)),y)=y. 375 [para_into,63.1.1.2.1.2.2,31.1.1] n(x,k(n(y,k(x,z)),r(z)))=n(k(y,r(z)),x). 405,404 [para_into,350.1.1.1,41.1.1,demod,42,42] n(x,x)=x. 427 [para_into,66.1.1.1.2,19.1.1] u(n(x,Z),n(x,U))=x. 433 [para_into,66.1.1.2,404.1.1] u(n(x,c(x)),x)=x. 495 [hyper,69,282] n(c(x),x)=Z. 572,571 [para_into,495.1.1.1,41.1.1] n(x,c(x))=Z. 576,575 [back_demod,433,demod,572] u(Z,x)=x. 582 [hyper,575,69] n(c(x),Z)=Z. 585,584 [para_into,575.1.1,21.1.1] u(x,Z)=x. 592 [back_demod,209,demod,585] k(r(x),c(k(x,U)))=Z. 594 [para_from,575.1.1,61.1.1.1,demod,99,flip.1] n(U,c(x))=c(x). 596 [hyper,83,575,demod,283] n(k(U,Z),U)=Z. 686,685 [para_into,582.1.1.1,41.1.1] n(x,Z)=Z. 691,690 [back_demod,427,demod,686,576] n(x,U)=x. 697 [back_demod,596,demod,691] k(U,Z)=Z. 706 [para_from,685.1.1,59.1.1.1,demod,99,99,flip.1] u(c(x),U)=U. 728 [para_from,697.1.1,70.1.1.1,demod,56] n(Z,x)=n(x,k(n(U,k(x,Z)),Z)). 733 [para_from,697.1.1,29.1.1.1,flip.1] k(U,k(Z,x))=k(Z,x). 737 [copy,728,flip.1] n(x,k(n(U,k(x,Z)),Z))=n(Z,x). 796 [para_into,706.1.1.1,41.1.1] u(x,U)=U. 815,814 [hyper,796,69,demod,20] n(Z,x)=Z. 816 [back_demod,737,demod,815] n(x,k(n(U,k(x,Z)),Z))=Z. 1003,1002 [para_into,104.1.1.1.1,41.1.1] c(k(x,y))=d(c(x),c(y)). 1024 [back_demod,592,demod,1003,20] k(r(x),d(c(x),Z))=Z. 1210,1209 [para_into,594.1.1.2,41.1.1,demod,42] n(U,x)=x. 1211 [back_demod,816,demod,1210,30] n(x,k(x,k(Z,Z)))=Z. 7809 [para_into,1024.1.1.1,57.1.1,demod,20] k(U,d(Z,Z))=Z. 7924,7923 [para_into,1211.1.1.2,733.1.1,demod,1210] k(Z,Z)=Z. 7937 [back_demod,1211,demod,7924] n(x,k(x,Z))=Z. 7955 [para_from,7923.1.1,29.1.1.1,flip.1] k(Z,k(Z,x))=k(Z,x). 7991 [para_from,7937.1.1,47.1.1.1,demod,56,36,56,flip.1] n(r(x),k(Z,r(x)))=Z. 8297 [para_into,7991.1.1.1,31.1.1,demod,32] n(x,k(Z,x))=Z. 8302,8301 [para_into,8297.1.1.2,7955.1.1,demod,405] k(Z,x)=Z. 8470 [para_into,375.1.1.2.1.2,7809.1.1,demod,686,52,56,56,8302,686,52,56,56,691,flip.1] k(x,d(Z,Z))=Z. 8474 [para_into,375.1.1.2.1,64.1.1,demod,8302,686,30,691,flip.1] k(U,k($c2,r($c1)))=Z. 8477,8476 [para_into,8470.1.1,235.1.1] d(Z,Z)=Z. 8535 [para_from,8474.1.1,356.1.1.1.2,demod,58,20,8477,815,flip.1] k($c2,r($c1))=Z. 8537 [binary,8535.1,5.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 823 clauses generated 193250 clauses kept 7962 clauses forward subsumed 64203 clauses back subsumed 1790 Kbytes malloced 4470 ----------- times (seconds) ----------- user CPU time 10.24 (0 hr, 0 min, 10 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 10 (0 hr, 0 min, 10 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:35:07 2003