----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Fri Nov 21 22:58:38 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,5). 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("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("ii.txt"). ------- start included file ii.txt------- formula_list(usable). k(U,U)=U. -(r(U)=U&r(Z)=Z&r(I)=I&r(D)=D). end_of_list. -------> usable clausifies to: list(usable). 0 [] k(U,U)=U. 0 [] r(U)!=U|r(Z)!=Z|r(I)!=I|r(D)!=D. end_of_list. ------- end included file ii.txt------- SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=4. 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=16): 1 [] r(U)!=U|r(Z)!=Z|r(I)!=I|r(D)!=D. ------------> 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=13): 18 [copy,17,flip.1] u(k(x,y),k(z,y))=k(u(x,z),y). ---> New Demodulator: 19 [new_demod,18] u(k(x,y),k(z,y))=k(u(x,z),y). ** KEPT (pick-wt=5): 20 [] k(x,I)=x. ---> New Demodulator: 21 [new_demod,20] k(x,I)=x. ** KEPT (pick-wt=13): 22 [] u(k(r(x),c(k(x,y))),c(y))=c(y). ---> New Demodulator: 23 [new_demod,22] u(k(r(x),c(k(x,y))),c(y))=c(y). ** KEPT (pick-wt=4): 25 [copy,24,flip.1] c(I)=D. ---> New Demodulator: 26 [new_demod,25] c(I)=D. ** KEPT (pick-wt=5): 28 [copy,27,flip.1] u(I,D)=U. ---> New Demodulator: 29 [new_demod,28] u(I,D)=U. ** KEPT (pick-wt=4): 31 [copy,30,flip.1] c(U)=Z. ---> New Demodulator: 32 [new_demod,31] c(U)=Z. ** KEPT (pick-wt=5): 33 [] k(U,U)=U. ---> New Demodulator: 34 [new_demod,33] k(U,U)=U. 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. >>>> Starting back demodulation with 23. >>>> Starting back demodulation with 26. >>>> Starting back demodulation with 29. >>>> Starting back demodulation with 32. >>>> Starting back demodulation with 34. ======= end of input processing ======= =========== start of search =========== Resetting weight limit to 11. sos_size=2077 -----> EMPTY CLAUSE at 4.16 sec ----> 6618 [hyper,2523,42,42,42,42] $F. Length of proof is 106. Level of proof is 32. ---------------- PROOF ---------------- 1 [] r(U)!=U|r(Z)!=Z|r(I)!=I|r(D)!=D. 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)). 7,6 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 8 [] k(x,k(y,z))=k(k(x,y),z). 9 [copy,8,flip.1] k(k(x,y),z)=k(x,k(y,z)). 12,11 [] r(r(x))=x. 14,13 [] r(u(x,y))=u(r(x),r(y)). 15 [] r(k(x,y))=k(r(y),r(x)). 17 [] k(u(x,y),z)=u(k(x,z),k(y,z)). 18 [copy,17,flip.1] u(k(x,y),k(z,y))=k(u(x,z),y). 21,20 [] k(x,I)=x. 22 [] u(k(r(x),c(k(x,y))),c(y))=c(y). 24 [] D=c(I). 26,25 [copy,24,flip.1] c(I)=D. 27 [] U=u(I,D). 29,28 [copy,27,flip.1] u(I,D)=U. 30 [] Z=c(U). 32,31 [copy,30,flip.1] c(U)=Z. 33 [] k(U,U)=U. 38 [para_into,4.1.1.1,2.1.1,demod,5] u(x,u(y,z))=u(y,u(x,z)). 39 [para_into,4.1.1,2.1.1] u(x,u(y,z))=u(y,u(z,x)). 40 [copy,39,flip.1] u(x,u(y,z))=u(z,u(x,y)). 42 [para_into,11.1.1,11.1.1] x=x. 44,43 [para_into,28.1.1,2.1.1] u(D,I)=U. 46,45 [para_from,28.1.1,4.1.1.1] u(U,x)=u(I,u(D,x)). 47 [para_into,6.1.1.1.1.1,31.1.1,demod,32] u(c(u(Z,x)),c(u(Z,c(x))))=U. 49 [para_into,6.1.1.1.1.1,25.1.1,demod,26] u(c(u(D,x)),c(u(D,c(x))))=I. 55 [para_into,6.1.1.2.1.2,31.1.1] u(c(u(c(x),U)),c(u(c(x),Z)))=x. 61 [para_into,6.1.1.2.1,2.1.1] u(c(u(c(x),y)),c(u(c(y),c(x))))=x. 63 [para_into,6.1.1,2.1.1] u(c(u(c(x),c(y))),c(u(c(x),y)))=x. 65 [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). 67 [para_into,45.1.1,2.1.1] u(x,U)=u(I,u(D,x)). 68 [copy,67,flip.1] u(I,u(D,x))=u(x,U). 69 [para_into,67.1.1,4.1.1] u(x,u(y,U))=u(I,u(D,u(x,y))). 71 [para_from,67.1.1,6.1.1.1.1,demod,32] u(c(u(I,u(D,c(x)))),c(u(c(x),Z)))=x. 77 [para_into,9.1.1.1,20.1.1,flip.1] k(x,k(I,y))=k(x,y). 81 [para_into,68.1.1.2,2.1.1] u(I,u(x,D))=u(x,U). 82 [para_into,68.1.1,2.1.1,demod,5] u(D,u(x,I))=u(x,U). 84 [copy,82,flip.1] u(x,U)=u(D,u(x,I)). 93,92 [para_into,13.1.1.1,43.1.1] r(U)=u(r(D),r(I)). 94 [para_into,13.1.1.1,6.1.1,flip.1] u(r(c(u(c(x),y))),r(c(u(c(x),c(y)))))=r(x). 98 [back_demod,1,demod,93] u(r(D),r(I))!=U|r(Z)!=Z|r(I)!=I|r(D)!=D. 100 [para_into,82.1.1.2,2.1.1] u(D,u(I,x))=u(x,U). 102 [copy,100,flip.1] u(x,U)=u(D,u(I,x)). 119 [para_into,15.1.1.1,20.1.1,flip.1] k(r(I),r(x))=r(x). 128,127 [para_into,119.1.1.2,11.1.1,demod,12] k(r(I),x)=x. 130,129 [para_into,127.1.1,77.1.1,demod,128,flip.1] k(I,x)=x. 132,131 [para_into,127.1.1,20.1.1] r(I)=I. 135 [back_demod,98,demod,132,132] u(r(D),I)!=U|r(Z)!=Z|I!=I|r(D)!=D. 139,138 [back_demod,92,demod,132] r(U)=u(r(D),I). 148,147 [para_into,18.1.1.2,129.1.1] u(k(x,y),y)=k(u(x,I),y). 195,194 [para_into,22.1.1.1.1,131.1.1,demod,130,130] u(c(x),c(x))=c(x). 204 [para_into,22.1.1.1.2.1,33.1.1,demod,139,32,32,148,5,32] k(u(r(D),u(I,I)),Z)=Z. 206 [para_into,22.1.1.1.2.1,20.1.1,demod,26,26] u(k(r(x),c(x)),D)=D. 219,218 [para_into,194.1.1.1,31.1.1,demod,32,32] u(Z,Z)=Z. 221,220 [para_into,194.1.1.1,25.1.1,demod,26,26] u(D,D)=D. 234 [para_from,218.1.1,4.1.1.1,flip.1] u(Z,u(Z,x))=u(Z,x). 237,236 [para_from,218.1.1,38.1.1.2,flip.1] u(Z,u(x,Z))=u(x,Z). 239,238 [para_from,220.1.1,81.1.1.2,demod,29,flip.1] u(D,U)=U. 296 [para_into,206.1.1,2.1.1] u(D,k(r(x),c(x)))=D. 298 [para_from,206.1.1,81.1.1.2,demod,29,flip.1] u(k(r(x),c(x)),U)=U. 355 [para_into,47.1.1.1.1,218.1.1] u(c(Z),c(u(Z,c(Z))))=U. 359 [para_into,47.1.1.1.1,84.1.1,demod,32,219] u(c(u(D,u(Z,I))),c(Z))=U. 375 [para_into,47.1.1.2.1.2,25.1.1] u(c(u(Z,I)),c(u(Z,D)))=U. 409 [para_into,296.1.1.2.1,138.1.1,demod,32] u(D,k(u(r(D),I),Z))=D. 453 [para_into,49.1.1.1.1,238.1.1,demod,32,32] u(Z,c(u(D,Z)))=I. 462,461 [para_into,49.1.1.1.1,43.1.1,demod,32,26,221] u(Z,c(D))=I. 492,491 [para_from,461.1.1,234.1.1.2,demod,462] u(Z,I)=I. 503 [back_demod,375,demod,492,26] u(D,c(u(Z,D)))=U. 506,505 [back_demod,359,demod,492,44,32] u(Z,c(Z))=U. 507 [back_demod,355,demod,506,32] u(c(Z),Z)=U. 510,509 [para_into,491.1.1,2.1.1] u(I,Z)=I. 517 [para_from,491.1.1,40.1.1.2,flip.1] u(I,u(x,Z))=u(x,I). 609 [para_from,507.1.1,6.1.1.1.1,demod,32,195] u(Z,c(c(Z)))=Z. 673 [para_into,609.1.1,2.1.1] u(c(c(Z)),Z)=Z. 691 [para_into,55.1.1.2.1,673.1.1] u(c(u(c(c(Z)),U)),c(Z))=c(Z). 725 [para_from,453.1.1,47.1.1.2.1,demod,237,26] u(c(u(D,Z)),D)=U. 757 [para_into,503.1.1.2.1,2.1.1] u(D,c(u(D,Z)))=U. 929 [para_from,757.1.1,49.1.1.1.1,demod,32] u(Z,c(u(D,c(c(u(D,Z))))))=I. 1064 [para_into,517.1.1.2,673.1.1,demod,510,flip.1] u(c(c(Z)),I)=I. 1083,1082 [para_from,1064.1.1,82.1.1.2,demod,44,flip.1] u(c(c(Z)),U)=U. 1101,1100 [back_demod,691,demod,1083,32,506,flip.1] c(Z)=U. 1146 [para_into,63.1.1.2.1,725.1.1,demod,32] u(c(u(c(u(D,Z)),c(D))),Z)=u(D,Z). 1208 [para_from,1100.1.1,194.1.1.2,demod,1101,46,239,1101] u(I,U)=U. 1226 [para_into,1208.1.1,102.1.1] u(D,u(I,I))=U. 1239,1238 [para_from,1226.1.1,13.1.1.1,demod,139,14,132,132,flip.1] u(r(D),u(I,I))=u(r(D),I). 1246,1245 [back_demod,204,demod,1239] k(u(r(D),I),Z)=Z. 1251,1250 [back_demod,409,demod,1246] u(D,Z)=D. 1254 [back_demod,1146,demod,1251,195,1251] u(c(c(D)),Z)=D. 1265,1264 [back_demod,929,demod,1251] u(Z,c(u(D,c(c(D)))))=I. 1355,1354 [para_into,65.1.1.2,194.1.1,demod,7,flip.1] u(x,c(u(c(x),c(y))))=x. 1375 [para_into,65.1.1.2,6.1.1,demod,1355] u(c(u(c(x),y)),x)=x. 1417 [para_from,69.1.1,63.1.1.2.1] u(c(u(c(x),c(u(y,U)))),c(u(I,u(D,u(c(x),y)))))=x. 1425 [para_from,69.1.1,6.1.1.1.1] u(c(u(I,u(D,u(c(x),y)))),c(u(c(x),c(u(y,U)))))=x. 1436 [para_from,1254.1.1,517.1.1.2,demod,29,flip.1] u(c(c(D)),I)=U. 1469,1468 [para_from,1436.1.1,61.1.1.1.1,demod,32,26,1265,flip.1] c(D)=I. 1486 [para_from,1468.1.1,298.1.1.1.2,demod,21] u(r(D),U)=U. 1488 [para_from,1468.1.1,296.1.1.2.2,demod,21] u(D,r(D))=D. 1491,1490 [para_from,1468.1.1,206.1.1.1.2,demod,21] u(r(D),D)=D. 1531,1530 [para_into,1486.1.1,84.1.1] u(D,u(r(D),I))=U. 1535,1534 [para_from,1486.1.1,13.1.1.1,demod,139,12,139,1531] u(r(D),I)=U. 1552 [back_demod,135,demod,1535] U!=U|r(Z)!=Z|I!=I|r(D)!=D. 1569 [para_from,71.1.1,61.1.1.2.1] u(c(u(c(u(c(x),Z)),u(I,u(D,c(x))))),c(x))=u(c(x),Z). 1602,1601 [para_from,1488.1.1,13.1.1.1,demod,12,1491] r(D)=D. 1605 [back_demod,1552,demod,1602] U!=U|r(Z)!=Z|I!=I|D!=D. 1764 [para_into,94.1.1.2.1.1.2,1100.1.1] u(r(c(u(c(x),Z))),r(c(u(c(x),U))))=r(x). 1853 [para_into,1375.1.1.1.1,69.1.1] u(c(u(I,u(D,u(c(x),y)))),x)=x. 2064,2063 [para_from,1375.1.1,81.1.1.2,demod,29,1469,flip.1] u(c(u(I,x)),U)=U. 2067 [para_from,1375.1.1,69.1.1.2,demod,32,flip.1] u(I,u(D,u(x,c(u(Z,y)))))=u(x,U). 2074,2073 [para_from,1375.1.1,71.1.1.2.1,demod,1101,46,1101,2064,1101,46,flip.1] u(I,u(D,x))=U. 2098,2097 [back_demod,2067,demod,2074,flip.1] u(x,U)=U. 2104,2103 [back_demod,1853,demod,2074,32] u(Z,x)=x. 2117,2116 [back_demod,1569,demod,2074,2098,32,2104,flip.1] u(c(x),Z)=c(x). 2121,2120 [back_demod,1425,demod,2074,32,2098,32,2117,2104] c(c(x))=x. 2125,2124 [back_demod,1417,demod,2098,32,2117,2121,2074,32] u(x,Z)=x. 2146 [back_demod,1764,demod,2125,2121,2098,32] u(r(x),r(Z))=r(x). 2511 [para_into,2146.1.1.1,11.1.1,demod,12] u(x,r(Z))=x. 2516,2515 [para_into,2511.1.1,2103.1.1] r(Z)=Z. 2523 [back_demod,1605,demod,2516] U!=U|Z!=Z|I!=I|D!=D. 6618 [hyper,2523,42,42,42,42] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 834 clauses generated 168270 clauses kept 3838 clauses forward subsumed 106605 clauses back subsumed 44 Kbytes malloced 4502 ----------- times (seconds) ----------- user CPU time 4.36 (0 hr, 0 min, 4 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 4 (0 hr, 0 min, 4 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 Fri Nov 21 22:58:42 2003