============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 10833 was started by mccune on cleo.thornwood, Sat Aug 12 20:58:51 2006 The command was "/home/mccune/bin/prover9 -f bw.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file bw.in formulas(sos). a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). a(a(W,x),y) = a(a(x,y),y) # label(W). end_of_list. formulas(sos). a(y,f(y)) != a(f(y),a(y,f(y))) # answer(y). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). [assumption]. a(a(W,x),y) = a(a(x,y),y) # label(W). [assumption]. a(x,f(x)) != a(f(x),a(x,f(x))) # answer(x). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ B, W, a, f ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). [assumption]. 2 a(a(W,x),y) = a(a(x,y),y) # label(W). [assumption]. 4 a(f(x),a(x,f(x))) != a(x,f(x)) # answer(x). [copy(3),flip(a)]. end_of_list. formulas(demodulators). 1 a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). [assumption]. 2 a(a(W,x),y) = a(a(x,y),y) # label(W). [assumption]. % (lex-dep) end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=13): 1 a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). [assumption]. given #2 (I,wt=11): 2 a(a(W,x),y) = a(a(x,y),y) # label(W). [assumption]. given #3 (I,wt=12): 4 a(f(x),a(x,f(x))) != a(x,f(x)) # answer(x). [copy(3),flip(a)]. given #4 (T,wt=11): 9 a(a(W,W),x) = a(a(x,x),x). [para(2(a,2),2(a,1))]. given #5 (T,wt=13): 5 a(a(a(W,B),x),y) = a(x,a(x,y)). [para(2(a,2),1(a,1,1))]. given #6 (A,wt=13): 6 a(a(W,a(B,x)),y) = a(x,a(y,y)). [para(2(a,2),1(a,1))]. given #7 (F,wt=28): 11 a(f(a(a(B,x),y)),a(x,a(y,f(a(a(B,x),y))))) != a(x,a(y,f(a(a(B,x),y)))) # answer(a(a(B,x),y)). [para(1(a,1),4(a,1,2)),rewrite(1(19))]. given #8 (F,wt=28): 18 a(f(a(a(W,B),x)),a(x,a(x,f(a(a(W,B),x))))) != a(x,a(x,f(a(a(W,B),x)))) # answer(a(a(W,B),x)). [para(5(a,1),4(a,1,2)),rewrite(5(23))]. given #9 (T,wt=13): 17 a(a(W,a(W,B)),x) = a(x,a(x,x)). [para(5(a,1),2(a,2))]. given #10 (T,wt=15): 7 a(x,a(a(W,y),z)) = a(x,a(a(y,z),z)). [para(2(a,1),1(a,2,2)),rewrite(1(6))]. given #11 (A,wt=17): 8 a(a(W,a(a(B,x),y)),z) = a(a(x,a(y,z)),z). [para(1(a,1),2(a,2,1))]. given #12 (F,wt=28): 45 a(f(a(a(W,B),x)),a(x,a(x,f(a(a(B,x),x))))) != a(x,a(x,f(a(a(B,x),x)))) # answer(a(a(B,x),x)). [para(2(a,2),11(a,1,1,1))]. given #13 (F,wt=28): 46 a(f(a(a(B,x),x)),a(x,a(x,f(a(a(W,B),x))))) != a(x,a(x,f(a(a(B,x),x)))) # answer(a(a(B,x),x)). [para(2(a,2),11(a,1,2,2,2,1))]. given #14 (T,wt=15): 10 a(a(W,a(W,x)),y) = a(a(W,a(x,y)),y). [para(2(a,1),2(a,2,1)),rewrite(2(8,R))]. given #15 (T,wt=13): 264 a(a(W,a(W,W)),B) = a(B,a(B,B)). [para(10(a,2),17(a,1))]. given #16 (A,wt=17): 12 a(a(W,W),a(B,x)) = a(x,a(a(B,x),a(B,x))). [para(9(a,2),1(a,1))]. given #17 (F,wt=28): 47 a(f(a(a(B,x),x)),a(x,a(x,f(a(a(B,x),x))))) != a(x,a(x,f(a(a(W,B),x)))) # answer(a(a(B,x),x)). [para(2(a,2),11(a,2,2,2,1))]. given #18 (F,wt=28): 61 a(f(a(a(B,x),x)),a(x,a(x,f(a(a(W,B),x))))) != a(x,a(x,f(a(a(W,B),x)))) # answer(a(a(W,B),x)). [para(2(a,1),18(a,1,1,1))]. given #19 (T,wt=15): 13 a(x,a(a(W,W),y)) = a(x,a(a(y,y),y)). [para(9(a,1),1(a,2,2)),rewrite(1(7))]. given #20 (T,wt=15): 15 a(a(W,a(W,W)),x) = a(a(W,a(x,x)),x). [para(9(a,1),2(a,2,1)),rewrite(2(9,R))]. given #21 (A,wt=25): 14 a(a(x,a(y,a(a(B,x),y))),a(a(B,x),y)) = a(a(W,W),a(a(B,x),y)). [para(1(a,1),9(a,2,1)),flip(a)]. given #22 (F,wt=28): 62 a(f(a(a(W,B),x)),a(x,a(x,f(a(a(B,x),x))))) != a(x,a(x,f(a(a(W,B),x)))) # answer(a(a(W,B),x)). [para(2(a,1),18(a,1,2,2,2,1))]. given #23 (F,wt=28): 63 a(f(a(a(W,B),x)),a(x,a(x,f(a(a(W,B),x))))) != a(x,a(x,f(a(a(B,x),x)))) # answer(a(a(W,B),x)). [para(2(a,1),18(a,2,2,2,1))]. given #24 (T,wt=15): 39 a(a(a(W,a(B,W)),B),x) = a(B,a(x,x)). [para(6(a,2),6(a,1,1))]. given #25 (T,wt=15): 288 a(a(a(W,a(B,W)),W),B) = a(B,a(B,B)). [para(6(a,2),264(a,1,1))]. given #26 (A,wt=17): 16 a(a(W,a(a(W,B),x)),y) = a(a(x,a(x,y)),y). [para(5(a,1),2(a,2,1))]. given #27 (F,wt=35): 31 a(f(a(W,a(B,x))),a(x,a(f(a(W,a(B,x))),f(a(W,a(B,x)))))) != a(a(W,a(B,x)),f(a(W,a(B,x)))) # answer(a(W,a(B,x))). [para(6(a,1),4(a,1,2))]. given #28 (F,wt=34): 717 a(f(a(W,a(B,B))),a(a(a(W,a(B,W)),B),f(a(W,a(B,B))))) != a(a(W,a(B,B)),f(a(W,a(B,B)))) # answer(a(W,a(B,B))). [para(39(a,2),31(a,1,2))]. given #29 (T,wt=17): 24 a(x,a(a(W,a(B,y)),z)) = a(x,a(y,a(z,z))). [para(6(a,1),1(a,2,2)),rewrite(1(8))]. given #30 (T,wt=17): 26 a(a(a(W,a(B,W)),x),y) = a(a(W,a(x,x)),y). [para(6(a,2),2(a,1,1)),rewrite(2(10,R))]. given #31 (A,wt=25): 19 a(a(x,a(x,a(a(W,B),x))),a(a(W,B),x)) = a(a(W,W),a(a(W,B),x)). [para(5(a,1),9(a,2,1)),flip(a)]. given #32 (F,wt=34): 911 a(f(a(W,a(x,x))),a(a(a(W,a(B,W)),x),f(a(W,a(x,x))))) != a(a(W,a(x,x)),f(a(W,a(x,x)))) # answer(a(W,a(x,x))). [para(26(a,2),4(a,1,2))]. given #33 (F,wt=34): 913 a(f(a(W,a(x,x))),a(a(W,a(x,x)),f(a(W,a(x,x))))) != a(a(a(W,a(B,W)),x),f(a(W,a(x,x)))) # answer(a(W,a(x,x))). [para(26(a,2),4(a,2))]. given #34 (T,wt=17): 28 a(a(W,a(W,a(B,x))),y) = a(a(x,a(y,y)),y). [para(6(a,1),2(a,2,1))]. given #35 (T,wt=17): 73 a(x,a(a(W,a(W,B)),y)) = a(x,a(y,a(y,y))). [para(17(a,1),1(a,2,2)),rewrite(1(9))]. given #36 (A,wt=19): 20 a(a(W,W),a(W,B)) = a(a(W,B),a(a(W,B),a(W,B))). [para(5(a,1),9(a,2))]. given #37 (F,wt=35): 32 a(f(a(W,a(B,x))),a(a(W,a(B,x)),f(a(W,a(B,x))))) != a(x,a(f(a(W,a(B,x))),f(a(W,a(B,x))))) # answer(a(W,a(B,x))). [para(6(a,1),4(a,2))]. given #38 (F,wt=36): 725 a(a(W,a(B,B)),f(a(a(W,a(B,W)),B))) != a(f(a(W,a(B,B))),a(a(a(W,a(B,W)),B),f(a(W,a(B,B))))) # answer(a(W,a(B,B))). [para(6(a,2),717(a,2,2,1)),flip(a)]. given #39 (T,wt=17): 74 a(a(a(W,a(W,B)),W),x) = a(a(W,a(W,W)),x). [para(17(a,2),2(a,1,1)),rewrite(2(13,R))]. given #40 (T,wt=17): 75 a(a(W,a(W,a(W,B))),x) = a(a(x,a(x,x)),x). [para(17(a,1),2(a,2,1))]. given #41 (A,wt=19): 21 a(a(a(a(W,a(B,B)),x),y),z) = a(a(x,x),a(y,z)). [para(6(a,2),1(a,1,1,1))]. given #42 (F,wt=34): 1528 a(a(W,a(B,B)),f(a(a(W,a(B,W)),B))) != a(f(a(W,a(B,B))),a(a(W,a(B,B)),f(a(W,a(B,B))))) # answer(a(W,a(B,B))). [para(6(a,1),725(a,2,2,1))]. given #43 (F,wt=36): 1022 a(f(a(a(W,a(B,W)),x)),a(a(a(W,a(B,W)),x),f(a(W,a(x,x))))) != a(a(W,a(x,x)),f(a(W,a(x,x)))) # answer(a(W,a(x,x))). [para(6(a,2),911(a,1,1,1))]. given #44 (T,wt=17): 254 a(a(a(W,a(B,W)),W),x) = a(a(W,a(W,x)),x). [para(6(a,2),10(a,1,1))]. given #45 (T,wt=17): 283 a(a(W,a(a(B,W),x)),y) = a(a(W,a(W,x)),y). [para(10(a,2),8(a,2))]. given #46 (A,wt=19): 22 a(a(a(W,a(B,a(B,x))),y),z) = a(x,a(a(y,y),z)). [para(6(a,2),1(a,1,1))]. given #47 (F,wt=26): 1864 a(a(a(W,a(B,a(B,f(a(x,x))))),x),f(a(x,x))) != a(a(x,x),f(a(x,x))) # answer(a(x,x)). [para(22(a,2),4(a,1))]. given #48 (F,wt=34): 1677 a(f(a(a(W,a(B,W)),x)),a(a(W,a(x,x)),f(a(W,a(x,x))))) != a(a(W,a(x,x)),f(a(W,a(x,x)))) # answer(a(W,a(x,x))). [para(6(a,1),1022(a,1,2,1))]. given #49 (T,wt=17): 287 a(a(W,a(W,a(W,W))),B) = a(a(B,a(B,B)),B). [para(264(a,1),2(a,2,1))]. given #50 (T,wt=17): 434 a(a(a(W,a(B,W)),W),x) = a(a(W,a(x,x)),x). [para(6(a,2),15(a,1,1))]. given #51 (A,wt=19): 23 a(a(W,a(B,a(a(B,x),y))),z) = a(x,a(y,a(z,z))). [para(6(a,2),1(a,1))]. given #52 (F,wt=34): 2211 a(f(a(a(W,a(W,B)),W)),a(a(W,a(W,W)),f(a(W,a(W,W))))) != a(a(W,a(W,W)),f(a(W,a(W,W)))) # answer(a(W,a(W,W))). [para(8(a,2),1677(a,1,1,1)),rewrite(283(9))]. given #53 (F,wt=36): 1025 a(f(a(W,a(x,x))),a(a(a(W,a(B,W)),x),f(a(a(W,a(B,W)),x)))) != a(a(W,a(x,x)),f(a(W,a(x,x)))) # answer(a(W,a(x,x))). [para(6(a,2),911(a,1,2,2,1))]. given #54 (T,wt=17): 436 a(a(W,a(W,a(B,W))),x) = a(a(W,a(W,W)),x). [para(6(a,2),15(a,2,1)),rewrite(2(13,R)),flip(a)]. given #55 (T,wt=17): 461 a(a(a(W,W),a(B,W)),x) = a(a(W,a(W,W)),x). [back_rewrite(294),rewrite(436(16))]. given #56 (A,wt=23): 25 a(a(W,a(B,x)),a(a(B,y),z)) = a(x,a(y,a(z,a(a(B,y),z)))). [para(1(a,1),6(a,2,2))]. given #57 (F,wt=34): 2409 a(f(a(W,a(x,x))),a(a(W,a(x,x)),f(a(a(W,a(B,W)),x)))) != a(a(W,a(x,x)),f(a(W,a(x,x)))) # answer(a(W,a(x,x))). [para(6(a,1),1025(a,1,2,1))]. given #58 (F,wt=34): 2854 a(f(a(W,a(W,W))),a(a(W,a(W,W)),f(a(a(W,a(W,B)),W)))) != a(a(W,a(W,W)),f(a(W,a(W,W)))) # answer(a(W,a(W,W))). [para(8(a,2),2409(a,1,2,2,1)),rewrite(283(20))]. given #59 (T,wt=19): 27 a(a(W,a(B,a(W,x))),y) = a(a(x,a(y,y)),a(y,y)). [para(6(a,2),2(a,1))]. given #60 (T,wt=19): 29 a(a(a(W,a(B,x)),y),a(y,y)) = a(a(W,x),a(y,y)). [para(6(a,2),2(a,2,1)),flip(a)]. given #61 (A,wt=19): 30 a(a(W,a(B,a(x,a(y,y)))),y) = a(a(W,x),a(y,y)). [para(6(a,2),2(a,2)),flip(a)]. given #62 (F,wt=36): 1029 a(f(a(W,a(x,x))),a(a(a(W,a(B,W)),x),f(a(W,a(x,x))))) != a(a(a(W,a(B,W)),x),f(a(W,a(x,x)))) # answer(a(W,a(x,x))). [para(6(a,2),911(a,2,1))]. given #63 (F,wt=36): 1031 a(f(a(W,a(x,x))),a(a(a(W,a(B,W)),x),f(a(W,a(x,x))))) != a(a(W,a(x,x)),f(a(a(W,a(B,W)),x))) # answer(a(W,a(x,x))). [para(6(a,2),911(a,2,2,1))]. given #64 (T,wt=19): 35 a(a(W,a(B,a(a(W,B),x))),y) = a(x,a(x,a(y,y))). [para(6(a,2),5(a,1))]. given #65 (T,wt=19): 38 a(a(W,a(a(W,a(B,B)),x)),y) = a(a(x,x),a(y,y)). [para(6(a,2),6(a,1,1,2))]. given #66 (A,wt=21): 34 a(a(a(W,a(B,a(W,B))),x),y) = a(a(x,x),a(a(x,x),y)). [para(6(a,2),5(a,1,1))]. given #67 (F,wt=34): 3241 a(f(a(W,a(x,x))),a(a(W,a(x,x)),f(a(W,a(x,x))))) != a(a(W,a(x,x)),f(a(a(W,a(B,W)),x))) # answer(a(W,a(x,x))). [para(6(a,1),1031(a,1,2,1))]. given #68 (F,wt=34): 3263 a(a(W,a(W,W)),f(a(a(W,a(B,W)),W))) != a(f(a(W,a(W,W))),a(a(W,a(W,W)),f(a(W,a(W,W))))) # answer(a(W,a(W,W))). [para(8(a,2),1031(a,1,2,1)),rewrite(283(15),74(20)),flip(a)]. given #69 (T,wt=19): 70 a(a(a(a(W,a(W,B)),B),x),y) = a(a(B,B),a(x,y)). [para(17(a,2),1(a,1,1,1))]. given #70 (T,wt=19): 76 a(a(a(W,a(W,B)),x),a(x,x)) = a(a(W,x),a(x,x)). [para(17(a,2),2(a,2,1)),flip(a)]. given #71 (A,wt=31): 36 a(x,a(a(a(W,a(B,x)),y),a(a(W,a(B,x)),y))) = a(a(W,a(B,x)),a(a(W,a(B,x)),y)). [para(6(a,1),5(a,2)),rewrite(5(9)),flip(a)]. given #72 (F,wt=34): 3884 a(a(W,a(W,W)),f(a(a(W,a(W,B)),W))) != a(f(a(W,a(W,W))),a(a(W,a(W,W)),f(a(W,a(W,W))))) # answer(a(W,a(W,W))). [para(8(a,2),3241(a,2,2,1)),rewrite(283(33)),flip(a)]. given #73 (F,wt=36): 1034 a(f(a(a(W,a(W,B)),W)),a(a(a(W,a(B,W)),W),f(a(W,a(W,W))))) != a(a(W,a(W,W)),f(a(W,a(W,W)))) # answer(a(W,a(W,W))). [para(17(a,2),911(a,1,1,1))]. given #74 (T,wt=19): 102 a(a(a(W,x),y),a(z,u)) = a(a(a(x,y),y),a(z,u)). [para(7(a,1),1(a,1,1,1)),rewrite(1(6)),flip(a)]. given #75 (T,wt=19): 103 a(x,a(a(a(W,y),z),u)) = a(x,a(a(a(y,z),z),u)). [para(7(a,1),1(a,1,1)),rewrite(1(6)),flip(a)]. given #76 (A,wt=23): 37 a(a(W,a(B,x)),a(a(W,B),y)) = a(x,a(y,a(y,a(a(W,B),y)))). [para(5(a,1),6(a,2,2))]. Demod_limit: a(a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(W,B))))))))))),a(a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(W,B)))))))))),a(a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(W,B))))))))),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,B),a(a(W,a(W,B)),a(a(W,B),a(a(W,B),a(a(W,B),a(W,B)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) = a(a(W,W),a(a(W,B),a(a(W,B),a(a(W,B),a(W,B))))). [para(37(a,2),19(a,1)),rewrite(5(40),5(43),5(44),5(45),5(48),5(49),3342(59),3342(98),3342(133),3342(164),3342(191),3342(214),3342(233),3101(248),5(239),5(250),5(257),5(260),5(261),5(262),5(265),5(266),5(267),5(274),5(277),5(278),5(279),5(282),5(283),5(284),5(299),5(310),5(317),5(320),5(321),5(322),5(325),5(326),5(327),5(334),5(337),5(338),5(339),5(342),5(343),5(344),5(355),5(362),5(365),5(366),5(367),5(370),5(371),5(372),5(379),5(382),5(383),5(384),5(387),5(388),5(389),5(408),5(423),5(434),5(441),5(444),5(445),5(446),5(449),5(450),5(451),5(458),5(461),5(462),5(463),5(466),5(467),5(468),5(479),5(486),5(489),5(490),5(491),5(494),5(495),5(496),5(503),5(506),5(507),5(508),5(511),5(512),5(513),5(528),5(539),5(546),5(549),5(550),5(551),5(554),5(555),5(556),5(563),5(566),5(567),5(568),5(571),5(572),5(573),5(584),5(591),5(594),5(595),5(596),5(599),5(600),5(601),5(608),5(611),5(612),5(613),5(616),5(617),5(618),5(641),5(660),5(675),5(686),5(693),5(696),5(697),5(698),5(701),5(702),5(703),5(710),5(713),5(714),5(715),5(718),5(719),5(720),5(731),5(738),5(741),5(742),5(743),5(746),5(747),5(748),5(755),5(758),5(759),5(760),5(763),5(764),5(765),5(780),5(791),5(798),5(801),5(802),5(803),5(806),5(807),5(808),5(815),5(818),5(819),5(820),5(823),5(824),5(825),5(836),5(843),5(846),5(847),5(848),5(851),5(852),5(853),5(860),5(863),5(864),5(865),5(868),5(869),5(870),5(889),5(904),5(915),5(922),5(925),5(926),5(927),5(930),5(931),5(932),5(939),5(942),5(943),5(944),5(947),5(948),5(949),5(960),5(967),5(970),5(971),5(972),5(975),5(976),5(977),5(984),5(987),5(988),5(989),5(992),5(993),5(994),5(1009),5(1020),5(1027),5(1030),5(1031),5(1032),5(1035),5(1036),5(1037),5(1044),5(1047),5(1048),5(1049),5(1052),5(1053),5(1054),5(1065),5(1072),5(1075),5(1076),5(1077),5(1080),5(1081),5(1082),5(1089),5(1092),5(1093),5(1094),5(1097),5(1098))]. Demod_limit (steps=-1, size=1121). The most recent kept clause is 4986. From here on, a short message will be printed for each 100 times the limit is hit. given #77 (F,wt=32): 4464 a(f(a(a(W,x),y)),a(a(a(x,y),y),f(a(a(W,x),y)))) != a(a(a(W,x),y),f(a(a(W,x),y))) # answer(a(a(W,x),y)). [para(103(a,1),4(a,1))]. given #78 (F,wt=32): 4465 a(f(a(a(x,y),y)),a(a(a(W,x),y),f(a(a(x,y),y)))) != a(a(a(x,y),y),f(a(a(x,y),y))) # answer(a(a(x,y),y)). [para(103(a,2),4(a,1))]. given #79 (T,wt=19): 104 a(x,a(y,a(a(W,z),u))) = a(x,a(y,a(a(z,u),u))). [para(7(a,1),1(a,1)),rewrite(1(6)),flip(a)]. given #80 (T,wt=19): 106 a(a(W,a(a(W,x),y)),z) = a(a(W,a(a(x,y),y)),z). [para(7(a,1),2(a,1,1)),rewrite(2(10,R)),flip(a)]. given #81 (A,wt=21): 40 a(a(W,a(B,a(W,a(B,x)))),y) = a(x,a(a(y,y),a(y,y))). [para(6(a,2),6(a,1))]. given #82 (F,wt=32): 5164 a(f(a(a(x,y),y)),a(a(a(x,y),y),f(a(a(W,x),y)))) != a(a(a(W,x),y),f(a(a(W,x),y))) # answer(a(a(W,x),y)). [para(2(a,1),4464(a,1,1,1))]. given #83 (F,wt=32): 5166 a(f(a(a(W,W),x)),a(a(a(x,x),x),f(a(a(W,W),x)))) != a(a(a(W,W),x),f(a(a(W,W),x))) # answer(a(a(W,W),x)). [para(2(a,1),4464(a,1,2,1))]. given #84 (T,wt=19): 113 a(x,a(a(W,a(W,y)),z)) = a(x,a(a(W,a(y,z)),z)). [para(2(a,1),7(a,2,2,1)),rewrite(2(9,R))]. given #85 (T,wt=19): 118 a(x,a(a(W,a(W,W)),y)) = a(x,a(a(W,a(y,y)),y)). [para(9(a,1),7(a,2,2,1)),rewrite(2(10,R))]. given #86 (A,wt=27): 41 a(a(W,a(B,x)),a(W,a(B,y))) = a(x,a(y,a(a(W,a(B,y)),a(W,a(B,y))))). [para(6(a,1),6(a,2,2))]. given #87 (F,wt=32): 5167 a(f(a(a(W,x),y)),a(a(a(x,y),y),f(a(a(x,y),y)))) != a(a(a(W,x),y),f(a(a(W,x),y))) # answer(a(a(W,x),y)). [para(2(a,1),4464(a,1,2,2,1))]. given #88 (F,wt=32): 5168 a(f(a(a(W,W),x)),a(a(a(x,x),x),f(a(a(W,x),x)))) != a(a(a(W,x),x),f(a(a(W,x),x))) # answer(a(a(W,x),x)). [para(2(a,2),4464(a,1,1,1))]. given #89 (T,wt=19): 161 a(a(a(W,a(a(B,B),x)),y),z) = a(a(x,y),a(y,z)). [para(8(a,2),1(a,1,1))]. given #90 (T,wt=19): 162 a(a(W,a(a(B,a(B,x)),y)),z) = a(x,a(a(y,z),z)). [para(8(a,2),1(a,1))]. given #91 (A,wt=21): 42 a(a(W,a(B,x)),a(y,y)) = a(x,a(a(W,a(B,a(y,y))),y)). [para(6(a,2),6(a,2,2))]. given #92 (F,wt=32): 5170 a(f(a(a(W,x),x)),a(a(a(x,x),x),f(a(a(W,W),x)))) != a(a(a(W,x),x),f(a(a(W,x),x))) # answer(a(a(W,x),x)). [para(2(a,2),4464(a,1,2,2,1))]. given #93 (F,wt=32): 5171 a(f(a(a(W,x),y)),a(a(a(x,y),y),f(a(a(W,x),y)))) != a(a(a(x,y),y),f(a(a(W,x),y))) # answer(a(a(W,x),y)). [para(2(a,1),4464(a,2,1))]. given #94 (T,wt=19): 191 a(a(W,a(a(B,x),y)),y) = a(a(W,a(W,a(B,x))),y). [para(6(a,2),8(a,2,1)),rewrite(2(12,R))]. given #95 (T,wt=19): 241 a(a(W,a(W,a(W,x))),y) = a(a(W,a(W,a(x,y))),y). [para(10(a,1),2(a,2,1)),rewrite(2(12,R))]. given #96 (A,wt=44): 43 a(f(a(a(B,x),a(a(B,y),z))),a(x,a(y,a(z,f(a(a(B,x),a(a(B,y),z))))))) != a(x,a(y,a(z,f(a(a(B,x),a(a(B,y),z)))))) # answer(a(a(B,x),a(a(B,y),z))). [para(1(a,1),11(a,1,2,2)),rewrite(1(29))]. ============================== PROOF ================================= % Proof 1 at 7.32 (+ 0.03) seconds: a(a(B,a(W,W)),a(a(B,a(B,W)),a(a(B,B),B))). % Length of proof is 13. % Level of proof is 5. % Maximum clause weight is 60. % Given clauses 96. 1 a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). [assumption]. 2 a(a(W,x),y) = a(a(x,y),y) # label(W). [assumption]. 3 a(x,f(x)) != a(f(x),a(x,f(x))) # answer(x). [assumption]. 4 a(f(x),a(x,f(x))) != a(x,f(x)) # answer(x). [copy(3),flip(a)]. 8 a(a(W,a(a(B,x),y)),z) = a(a(x,a(y,z)),z). [para(1(a,1),2(a,2,1))]. 9 a(a(W,W),x) = a(a(x,x),x). [para(2(a,2),2(a,1))]. 11 a(f(a(a(B,x),y)),a(x,a(y,f(a(a(B,x),y))))) != a(x,a(y,f(a(a(B,x),y)))) # answer(a(a(B,x),y)). [para(1(a,1),4(a,1,2)),rewrite(1(19))]. 14 a(a(x,a(y,a(a(B,x),y))),a(a(B,x),y)) = a(a(W,W),a(a(B,x),y)). [para(1(a,1),9(a,2,1)),flip(a)]. 43 a(f(a(a(B,x),a(a(B,y),z))),a(x,a(y,a(z,f(a(a(B,x),a(a(B,y),z))))))) != a(x,a(y,a(z,f(a(a(B,x),a(a(B,y),z)))))) # answer(a(a(B,x),a(a(B,y),z))). [para(1(a,1),11(a,1,2,2)),rewrite(1(29))]. 162 a(a(W,a(a(B,a(B,x)),y)),z) = a(x,a(a(y,z),z)). [para(8(a,2),1(a,1))]. 8042 a(x,a(a(W,W),a(a(B,W),a(B,a(B,x))))) = a(a(W,W),a(a(B,W),a(B,a(B,x)))). [para(162(a,1),14(a,1)),rewrite(1(17),14(24))]. 8595 a(f(a(a(B,x),a(a(B,y),a(a(B,z),u)))),a(x,a(y,a(z,a(u,f(a(a(B,x),a(a(B,y),a(a(B,z),u))))))))) != a(x,a(y,a(z,a(u,f(a(a(B,x),a(a(B,y),a(a(B,z),u)))))))) # answer(a(a(B,x),a(a(B,y),a(a(B,z),u)))). [para(1(a,1),43(a,1,2,2,2)),rewrite(1(39))]. 8596 $F # answer(a(a(B,a(W,W)),a(a(B,a(B,W)),a(a(B,B),B)))). [resolve(8595,a,8042,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=96. Generated=26662. Kept=8594. proofs=1. Usable=91. Sos=7896. Demods=1339. Limbo=0, Disabled=609. Hints=0. Weight_deleted=227. Literals_deleted=0. Forward_subsumed=16265. Back_subsumed=140. Sos_limit_deleted=1576. Sos_displaced=0. Sos_removed=0. New_demodulators=1528 (2 lex), Back_demodulated=466. Back_unit_deleted=0. Demod_attempts=1264541. Demod_rewrites=39638. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=19.09. User_CPU=7.32, System_CPU=0.03, Wall_clock=7. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 10833 exit (max_proofs) Sat Aug 12 20:58:58 2006