============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13069 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:01 2006 The command was "/home/mccune/bin/prover9 -f bw.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file bw.in clauses(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. clauses(sos). a(x,f(x)) != a(f(x),a(x,f(x))) # answer(x). end_of_list. ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). [input]. 2 a(a(W,x),y) = a(a(x,y),y) # label(W). [input]. 3 a(x,f(x)) != a(f(x),a(x,f(x))) # answer(x). [input]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: no changes. Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ B, W, a, f ]). After inverse_order: Function symbol precedence: lex([ B, W, a, f ]). 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: clauses(usable). end_of_list. clauses(sos). 4 a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). [input]. 5 a(a(W,x),y) = a(a(x,y),y) # label(W). [input]. 6 a(f(x),a(x,f(x))) != a(x,f(x)) # answer(x). [copy(3),flip(a)]. end_of_list. clauses(demodulators). 4 a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). [input]. 5 a(a(W,x),y) = a(a(x,y),y) # label(W). [input]. % (lex-dep) end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=13): 4 a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). [input]. given #2 (I,wt=11): 5 a(a(W,x),y) = a(a(x,y),y) # label(W). [input]. given #3 (I,wt=12): 6 a(f(x),a(x,f(x))) != a(x,f(x)) # answer(x). [copy(3),flip(a)]. given #4 (T,wt=11): 11 a(a(W,W),x) = a(a(x,x),x). [para(5(a,2),5(a,1))]. given #5 (T,wt=13): 7 a(a(a(W,B),x),y) = a(x,a(x,y)). [para(5(a,2),4(a,1,1))]. given #6 (A,wt=13): 8 a(a(W,a(B,x)),y) = a(x,a(y,y)). [para(5(a,2),4(a,1))]. given #7 (F,wt=28): 13 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(4(a,1),6(a,1,2)),demod(4(19))]. given #8 (F,wt=28): 20 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(7(a,1),6(a,1,2)),demod(7(23))]. given #9 (T,wt=13): 19 a(a(W,a(W,B)),x) = a(x,a(x,x)). [para(7(a,1),5(a,2))]. given #10 (T,wt=15): 9 a(x,a(a(W,y),z)) = a(x,a(a(y,z),z)). [para(5(a,1),4(a,2,2)),demod(4(6))]. given #11 (A,wt=17): 10 a(a(W,a(a(B,x),y)),z) = a(a(x,a(y,z)),z). [para(4(a,1),5(a,2,1))]. given #12 (F,wt=28): 47 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(5(a,2),13(a,1,1,1))]. given #13 (F,wt=28): 48 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(5(a,2),13(a,1,2,2,2,1))]. given #14 (T,wt=15): 12 a(a(W,a(W,x)),y) = a(a(W,a(x,y)),y). [para(5(a,1),5(a,2,1)),demod(5(8,R))]. given #15 (T,wt=13): 266 a(a(W,a(W,W)),B) = a(B,a(B,B)). [para(12(a,2),19(a,1))]. given #16 (A,wt=17): 14 a(a(W,W),a(B,x)) = a(x,a(a(B,x),a(B,x))). [para(11(a,2),4(a,1))]. given #17 (F,wt=28): 49 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(5(a,2),13(a,2,2,2,1))]. given #18 (F,wt=28): 63 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(5(a,1),20(a,1,1,1))]. given #19 (T,wt=15): 15 a(x,a(a(W,W),y)) = a(x,a(a(y,y),y)). [para(11(a,1),4(a,2,2)),demod(4(7))]. given #20 (T,wt=15): 17 a(a(W,a(W,W)),x) = a(a(W,a(x,x)),x). [para(11(a,1),5(a,2,1)),demod(5(9,R))]. given #21 (A,wt=25): 16 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(4(a,1),11(a,2,1)),flip(a)]. given #22 (F,wt=28): 64 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(5(a,1),20(a,1,2,2,2,1))]. given #23 (F,wt=28): 65 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(5(a,1),20(a,2,2,2,1))]. given #24 (T,wt=15): 41 a(a(a(W,a(B,W)),B),x) = a(B,a(x,x)). [para(8(a,2),8(a,1,1))]. given #25 (T,wt=15): 290 a(a(a(W,a(B,W)),W),B) = a(B,a(B,B)). [para(8(a,2),266(a,1,1))]. given #26 (A,wt=17): 18 a(a(W,a(a(W,B),x)),y) = a(a(x,a(x,y)),y). [para(7(a,1),5(a,2,1))]. given #27 (F,wt=35): 33 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(8(a,1),6(a,1,2))]. given #28 (F,wt=34): 719 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(41(a,2),33(a,1,2))]. given #29 (T,wt=17): 26 a(x,a(a(W,a(B,y)),z)) = a(x,a(y,a(z,z))). [para(8(a,1),4(a,2,2)),demod(4(8))]. given #30 (T,wt=17): 28 a(a(a(W,a(B,W)),x),y) = a(a(W,a(x,x)),y). [para(8(a,2),5(a,1,1)),demod(5(10,R))]. given #31 (A,wt=25): 21 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(7(a,1),11(a,2,1)),flip(a)]. given #32 (F,wt=34): 913 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(28(a,2),6(a,1,2))]. given #33 (F,wt=34): 915 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(28(a,2),6(a,2))]. given #34 (T,wt=17): 30 a(a(W,a(W,a(B,x))),y) = a(a(x,a(y,y)),y). [para(8(a,1),5(a,2,1))]. given #35 (T,wt=17): 75 a(x,a(a(W,a(W,B)),y)) = a(x,a(y,a(y,y))). [para(19(a,1),4(a,2,2)),demod(4(9))]. given #36 (A,wt=19): 22 a(a(W,W),a(W,B)) = a(a(W,B),a(a(W,B),a(W,B))). [para(7(a,1),11(a,2))]. given #37 (F,wt=35): 34 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(8(a,1),6(a,2))]. given #38 (F,wt=36): 727 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(8(a,2),719(a,2,2,1)),flip(a)]. given #39 (T,wt=17): 76 a(a(a(W,a(W,B)),W),x) = a(a(W,a(W,W)),x). [para(19(a,2),5(a,1,1)),demod(5(13,R))]. given #40 (T,wt=17): 77 a(a(W,a(W,a(W,B))),x) = a(a(x,a(x,x)),x). [para(19(a,1),5(a,2,1))]. given #41 (A,wt=19): 23 a(a(a(a(W,a(B,B)),x),y),z) = a(a(x,x),a(y,z)). [para(8(a,2),4(a,1,1,1))]. given #42 (F,wt=34): 1530 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(8(a,1),727(a,2,2,1))]. given #43 (F,wt=36): 1024 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(8(a,2),913(a,1,1,1))]. given #44 (T,wt=17): 256 a(a(a(W,a(B,W)),W),x) = a(a(W,a(W,x)),x). [para(8(a,2),12(a,1,1))]. given #45 (T,wt=17): 285 a(a(W,a(a(B,W),x)),y) = a(a(W,a(W,x)),y). [para(12(a,2),10(a,2))]. given #46 (A,wt=19): 24 a(a(a(W,a(B,a(B,x))),y),z) = a(x,a(a(y,y),z)). [para(8(a,2),4(a,1,1))]. given #47 (F,wt=26): 1866 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(24(a,2),6(a,1))]. given #48 (F,wt=34): 1679 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(8(a,1),1024(a,1,2,1))]. given #49 (T,wt=17): 289 a(a(W,a(W,a(W,W))),B) = a(a(B,a(B,B)),B). [para(266(a,1),5(a,2,1))]. given #50 (T,wt=17): 436 a(a(a(W,a(B,W)),W),x) = a(a(W,a(x,x)),x). [para(8(a,2),17(a,1,1))]. given #51 (A,wt=19): 25 a(a(W,a(B,a(a(B,x),y))),z) = a(x,a(y,a(z,z))). [para(8(a,2),4(a,1))]. given #52 (F,wt=34): 2213 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(10(a,2),1679(a,1,1,1)),demod(285(9))]. given #53 (F,wt=36): 1027 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(8(a,2),913(a,1,2,2,1))]. given #54 (T,wt=17): 438 a(a(W,a(W,a(B,W))),x) = a(a(W,a(W,W)),x). [para(8(a,2),17(a,2,1)),demod(5(13,R)),flip(a)]. given #55 (T,wt=17): 463 a(a(a(W,W),a(B,W)),x) = a(a(W,a(W,W)),x). [back_demod(296),demod(438(16))]. given #56 (A,wt=23): 27 a(a(W,a(B,x)),a(a(B,y),z)) = a(x,a(y,a(z,a(a(B,y),z)))). [para(4(a,1),8(a,2,2))]. given #57 (F,wt=34): 2411 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(8(a,1),1027(a,1,2,1))]. given #58 (F,wt=34): 2856 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(10(a,2),2411(a,1,2,2,1)),demod(285(20))]. given #59 (T,wt=19): 29 a(a(W,a(B,a(W,x))),y) = a(a(x,a(y,y)),a(y,y)). [para(8(a,2),5(a,1))]. given #60 (T,wt=19): 31 a(a(a(W,a(B,x)),y),a(y,y)) = a(a(W,x),a(y,y)). [para(8(a,2),5(a,2,1)),flip(a)]. given #61 (A,wt=19): 32 a(a(W,a(B,a(x,a(y,y)))),y) = a(a(W,x),a(y,y)). [para(8(a,2),5(a,2)),flip(a)]. given #62 (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(a(W,a(B,W)),x),f(a(W,a(x,x)))) # answer(a(W,a(x,x))). [para(8(a,2),913(a,2,1))]. given #63 (F,wt=36): 1033 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(8(a,2),913(a,2,2,1))]. given #64 (T,wt=19): 37 a(a(W,a(B,a(a(W,B),x))),y) = a(x,a(x,a(y,y))). [para(8(a,2),7(a,1))]. given #65 (T,wt=19): 40 a(a(W,a(a(W,a(B,B)),x)),y) = a(a(x,x),a(y,y)). [para(8(a,2),8(a,1,1,2))]. given #66 (A,wt=21): 36 a(a(a(W,a(B,a(W,B))),x),y) = a(a(x,x),a(a(x,x),y)). [para(8(a,2),7(a,1,1))]. given #67 (F,wt=34): 3243 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(8(a,1),1033(a,1,2,1))]. given #68 (F,wt=34): 3265 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(10(a,2),1033(a,1,2,1)),demod(285(15),76(20)),flip(a)]. given #69 (T,wt=19): 72 a(a(a(a(W,a(W,B)),B),x),y) = a(a(B,B),a(x,y)). [para(19(a,2),4(a,1,1,1))]. given #70 (T,wt=19): 78 a(a(a(W,a(W,B)),x),a(x,x)) = a(a(W,x),a(x,x)). [para(19(a,2),5(a,2,1)),flip(a)]. given #71 (A,wt=31): 38 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(8(a,1),7(a,2)),demod(7(9)),flip(a)]. given #72 (F,wt=34): 3886 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(10(a,2),3243(a,2,2,1)),demod(285(33)),flip(a)]. given #73 (F,wt=36): 1036 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(19(a,2),913(a,1,1,1))]. given #74 (T,wt=19): 104 a(a(a(W,x),y),a(z,u)) = a(a(a(x,y),y),a(z,u)). [para(9(a,1),4(a,1,1,1)),demod(4(6)),flip(a)]. given #75 (T,wt=19): 105 a(x,a(a(a(W,y),z),u)) = a(x,a(a(a(y,z),z),u)). [para(9(a,1),4(a,1,1)),demod(4(6)),flip(a)]. given #76 (A,wt=23): 39 a(a(W,a(B,x)),a(a(W,B),y)) = a(x,a(y,a(y,a(a(W,B),y)))). [para(7(a,1),8(a,2,2))]. Demod_limit: 0 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(39(a,2),21(a,1)),demod(7(40),7(43),7(44),7(45),7(48),7(49),3344(59),3344(98),3344(133),3344(164),3344(191),3344(214),3344(233),3103(248),7(239),7(250),7(257),7(260),7(261),7(262),7(265),7(266),7(267),7(274),7(277),7(278),7(279),7(282),7(283),7(284),7(299),7(310),7(317),7(320),7(321),7(322),7(325),7(326),7(327),7(334),7(337),7(338),7(339),7(342),7(343),7(344),7(355),7(362),7(365),7(366),7(367),7(370),7(371),7(372),7(379),7(382),7(383),7(384),7(387),7(388),7(389),7(408),7(423),7(434),7(441),7(444),7(445),7(446),7(449),7(450),7(451),7(458),7(461),7(462),7(463),7(466),7(467),7(468),7(479),7(486),7(489),7(490),7(491),7(494),7(495),7(496),7(503),7(506),7(507),7(508),7(511),7(512),7(513),7(528),7(539),7(546),7(549),7(550),7(551),7(554),7(555),7(556),7(563),7(566),7(567),7(568),7(571),7(572),7(573),7(584),7(591),7(594),7(595),7(596),7(599),7(600),7(601),7(608),7(611),7(612),7(613),7(616),7(617),7(618),7(641),7(660),7(675),7(686),7(693),7(696),7(697),7(698),7(701),7(702),7(703),7(710),7(713),7(714),7(715),7(718),7(719),7(720),7(731),7(738),7(741),7(742),7(743),7(746),7(747),7(748),7(755),7(758),7(759),7(760),7(763),7(764),7(765),7(780),7(791),7(798),7(801),7(802),7(803),7(806),7(807),7(808),7(815),7(818),7(819),7(820),7(823),7(824),7(825),7(836),7(843),7(846),7(847),7(848),7(851),7(852),7(853),7(860),7(863),7(864),7(865),7(868),7(869),7(870),7(889),7(904),7(915),7(922),7(925),7(926),7(927),7(930),7(931),7(932),7(939),7(942),7(943),7(944),7(947),7(948),7(949),7(960),7(967),7(970),7(971),7(972),7(975),7(976),7(977),7(984),7(987),7(988),7(989),7(992),7(993),7(994),7(1009),7(1020),7(1027),7(1030),7(1031),7(1032),7(1035),7(1036),7(1037),7(1044),7(1047),7(1048),7(1049),7(1052),7(1053),7(1054),7(1065),7(1072),7(1075),7(1076),7(1077),7(1080),7(1081),7(1082),7(1089),7(1092),7(1093),7(1094),7(1097),7(1098))]. Demod_limit (steps=-1, size=1121). The most recent kept clause is 4988. From here on, a short message will be printed for each 100 times the limit is hit. given #77 (F,wt=32): 4466 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(105(a,1),6(a,1))]. given #78 (F,wt=32): 4467 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(105(a,2),6(a,1))]. given #79 (T,wt=19): 106 a(x,a(y,a(a(W,z),u))) = a(x,a(y,a(a(z,u),u))). [para(9(a,1),4(a,1)),demod(4(6)),flip(a)]. given #80 (T,wt=19): 108 a(a(W,a(a(W,x),y)),z) = a(a(W,a(a(x,y),y)),z). [para(9(a,1),5(a,1,1)),demod(5(10,R)),flip(a)]. given #81 (A,wt=21): 42 a(a(W,a(B,a(W,a(B,x)))),y) = a(x,a(a(y,y),a(y,y))). [para(8(a,2),8(a,1))]. given #82 (F,wt=32): 5166 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(5(a,1),4466(a,1,1,1))]. given #83 (F,wt=32): 5168 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(5(a,1),4466(a,1,2,1))]. given #84 (T,wt=19): 115 a(x,a(a(W,a(W,y)),z)) = a(x,a(a(W,a(y,z)),z)). [para(5(a,1),9(a,2,2,1)),demod(5(9,R))]. given #85 (T,wt=19): 120 a(x,a(a(W,a(W,W)),y)) = a(x,a(a(W,a(y,y)),y)). [para(11(a,1),9(a,2,2,1)),demod(5(10,R))]. given #86 (A,wt=27): 43 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(8(a,1),8(a,2,2))]. given #87 (F,wt=32): 5169 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(5(a,1),4466(a,1,2,2,1))]. given #88 (F,wt=32): 5170 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(5(a,2),4466(a,1,1,1))]. given #89 (T,wt=19): 163 a(a(a(W,a(a(B,B),x)),y),z) = a(a(x,y),a(y,z)). [para(10(a,2),4(a,1,1))]. given #90 (T,wt=19): 164 a(a(W,a(a(B,a(B,x)),y)),z) = a(x,a(a(y,z),z)). [para(10(a,2),4(a,1))]. given #91 (A,wt=21): 44 a(a(W,a(B,x)),a(y,y)) = a(x,a(a(W,a(B,a(y,y))),y)). [para(8(a,2),8(a,2,2))]. given #92 (F,wt=32): 5172 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(5(a,2),4466(a,1,2,2,1))]. given #93 (F,wt=32): 5173 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(5(a,1),4466(a,2,1))]. given #94 (T,wt=19): 193 a(a(W,a(a(B,x),y)),y) = a(a(W,a(W,a(B,x))),y). [para(8(a,2),10(a,2,1)),demod(5(12,R))]. given #95 (T,wt=19): 243 a(a(W,a(W,a(W,x))),y) = a(a(W,a(W,a(x,y))),y). [para(12(a,1),5(a,2,1)),demod(5(12,R))]. given #96 (A,wt=44): 45 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(4(a,1),13(a,1,2,2)),demod(4(29))]. ============================== PROOF ================================= % Proof 1 at 6.76 (+ 0.04) 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. 3 a(x,f(x)) != a(f(x),a(x,f(x))) # answer(x). [input]. 4 a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). [input]. 5 a(a(W,x),y) = a(a(x,y),y) # label(W). [input]. 6 a(f(x),a(x,f(x))) != a(x,f(x)) # answer(x). [copy(3),flip(a)]. 10 a(a(W,a(a(B,x),y)),z) = a(a(x,a(y,z)),z). [para(4(a,1),5(a,2,1))]. 11 a(a(W,W),x) = a(a(x,x),x). [para(5(a,2),5(a,1))]. 13 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(4(a,1),6(a,1,2)),demod(4(19))]. 16 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(4(a,1),11(a,2,1)),flip(a)]. 45 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(4(a,1),13(a,1,2,2)),demod(4(29))]. 164 a(a(W,a(a(B,a(B,x)),y)),z) = a(x,a(a(y,z),z)). [para(10(a,2),4(a,1))]. 8044 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(164(a,1),16(a,1)),demod(4(17),16(24))]. 8597 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(4(a,1),45(a,1,2,2,2)),demod(4(39))]. 8598 $F # answer(a(a(B,a(W,W)),a(a(B,a(B,W)),a(a(B,B),B)))). [resolve(8597,a,8044,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=96. Generated=26662. Kept=8594. proofs=1. Usable=91. Sos=7896. Demods=1339. Denials=0. 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=1264528. 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=6.76, System_CPU=0.04, Wall_clock=7. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13069 exit (max_proofs) Mon Jun 19 16:41:08 2006