============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 26506 was started by mccune on cleo, Fri Apr 13 09:15:33 2007 The command was "/home/mccune/bin/prover9 -f bw.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file bw.in assign(max_seconds,30). formulas(assumptions). 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(goals). (exists Q all x a(Q,x) = a(x,a(Q,x))) # label(fixed_point_combinator). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (exists Q all x a(Q,x) = a(x,a(Q,x))) # label(fixed_point_combinator) # label(goal). [goal]. ============================== 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,f1(x)) != a(f1(x),a(x,f1(x))) # label(fixed_point_combinator). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label fixed_point_combinator to answer in negative clause Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ B, W, a, f1 ]). 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). 2 a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). [assumption]. 3 a(a(W,x),y) = a(a(x,y),y) # label(W). [assumption]. 5 a(f1(x),a(x,f1(x))) != a(x,f1(x)) # answer(fixed_point_combinator). [copy(4),flip(a)]. end_of_list. formulas(demodulators). 2 a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). [assumption]. 3 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): 2 a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). [assumption]. given #2 (I,wt=11): 3 a(a(W,x),y) = a(a(x,y),y) # label(W). [assumption]. given #3 (I,wt=12): 5 a(f1(x),a(x,f1(x))) != a(x,f1(x)) # answer(fixed_point_combinator). [copy(4),flip(a)]. given #4 (A,wt=13): 6 a(a(a(W,B),x),y) = a(x,a(x,y)). [para(3(a,2),2(a,1,1))]. given #5 (F,wt=28): 12 a(f1(a(a(B,x),y)),a(x,a(y,f1(a(a(B,x),y))))) != a(x,a(y,f1(a(a(B,x),y)))) # answer(fixed_point_combinator). [para(2(a,1),5(a,1,2)),rewrite(2(19))]. given #6 (F,wt=28): 15 a(f1(a(a(W,B),x)),a(x,a(x,f1(a(a(W,B),x))))) != a(x,a(x,f1(a(a(W,B),x)))) # answer(fixed_point_combinator). [para(6(a,1),5(a,1,2)),rewrite(6(23))]. given #7 (F,wt=28): 18 a(f1(a(a(W,B),x)),a(x,a(x,f1(a(a(B,x),x))))) != a(x,a(x,f1(a(a(B,x),x)))) # answer(fixed_point_combinator). [para(3(a,2),12(a,1,1,1))]. given #8 (F,wt=28): 19 a(f1(a(a(B,x),x)),a(x,a(x,f1(a(a(W,B),x))))) != a(x,a(x,f1(a(a(B,x),x)))) # answer(fixed_point_combinator). [para(3(a,2),12(a,1,2,2,2,1))]. given #9 (T,wt=11): 10 a(a(W,W),x) = a(a(x,x),x). [para(3(a,2),3(a,1))]. given #10 (T,wt=13): 7 a(a(W,a(B,x)),y) = a(x,a(y,y)). [para(3(a,2),2(a,1))]. given #11 (T,wt=13): 14 a(a(W,a(W,B)),x) = a(x,a(x,x)). [para(6(a,1),3(a,2))]. given #12 (T,wt=15): 8 a(x,a(a(W,y),z)) = a(x,a(a(y,z),z)). [para(3(a,1),2(a,2,2)),rewrite(2(6))]. given #13 (A,wt=17): 9 a(a(W,a(a(B,x),y)),z) = a(a(x,a(y,z)),z). [para(2(a,1),3(a,2,1))]. given #14 (F,wt=28): 20 a(f1(a(a(B,x),x)),a(x,a(x,f1(a(a(B,x),x))))) != a(x,a(x,f1(a(a(W,B),x)))) # answer(fixed_point_combinator). [para(3(a,2),12(a,2,2,2,1))]. given #15 (F,wt=28): 24 a(f1(a(a(B,x),x)),a(x,a(x,f1(a(a(W,B),x))))) != a(x,a(x,f1(a(a(W,B),x)))) # answer(fixed_point_combinator). [para(3(a,1),15(a,1,1,1))]. given #16 (F,wt=28): 25 a(f1(a(a(W,B),x)),a(x,a(x,f1(a(a(B,x),x))))) != a(x,a(x,f1(a(a(W,B),x)))) # answer(fixed_point_combinator). [para(3(a,1),15(a,1,2,2,2,1))]. given #17 (F,wt=28): 26 a(f1(a(a(W,B),x)),a(x,a(x,f1(a(a(W,B),x))))) != a(x,a(x,f1(a(a(B,x),x)))) # answer(fixed_point_combinator). [para(3(a,1),15(a,2,2,2,1))]. given #18 (T,wt=15): 11 a(a(W,a(W,x)),y) = a(a(W,a(x,y)),y). [para(3(a,1),3(a,2,1)),rewrite(3(8,R))]. given #19 (T,wt=13): 272 a(a(W,a(W,W)),B) = a(B,a(B,B)). [para(11(a,2),14(a,1))]. given #20 (T,wt=15): 29 a(x,a(a(W,W),y)) = a(x,a(a(y,y),y)). [para(10(a,1),2(a,2,2)),rewrite(2(7))]. given #21 (T,wt=15): 31 a(a(W,a(W,W)),x) = a(a(W,a(x,x)),x). [para(10(a,1),3(a,2,1)),rewrite(3(9,R))]. given #22 (A,wt=17): 13 a(a(W,a(a(W,B),x)),y) = a(a(x,a(x,y)),y). [para(6(a,1),3(a,2,1))]. given #23 (F,wt=35): 44 a(f1(a(W,a(B,x))),a(x,a(f1(a(W,a(B,x))),f1(a(W,a(B,x)))))) != a(a(W,a(B,x)),f1(a(W,a(B,x)))) # answer(fixed_point_combinator). [para(7(a,1),5(a,1,2))]. given #24 (F,wt=35): 45 a(f1(a(W,a(B,x))),a(a(W,a(B,x)),f1(a(W,a(B,x))))) != a(x,a(f1(a(W,a(B,x))),f1(a(W,a(B,x))))) # answer(fixed_point_combinator). [para(7(a,1),5(a,2))]. given #25 (F,wt=37): 253 a(f1(a(W,a(W,x))),a(a(W,a(x,f1(a(W,a(W,x))))),f1(a(W,a(W,x))))) != a(a(W,a(W,x)),f1(a(W,a(W,x)))) # answer(fixed_point_combinator). [para(11(a,1),5(a,1,2))]. given #26 (F,wt=37): 254 a(a(W,a(x,f1(a(W,a(W,x))))),f1(a(W,a(W,x)))) != a(f1(a(W,a(W,x))),a(a(W,a(W,x)),f1(a(W,a(W,x))))) # answer(fixed_point_combinator). [para(11(a,1),5(a,2)),flip(a)]. given #27 (T,wt=15): 69 a(a(a(W,a(B,W)),B),x) = a(B,a(x,x)). [para(7(a,2),7(a,1,1))]. given #28 (T,wt=15): 296 a(a(a(W,a(B,W)),W),B) = a(B,a(B,B)). [para(7(a,2),272(a,1,1))]. given #29 (T,wt=17): 28 a(a(W,W),a(B,x)) = a(x,a(a(B,x),a(B,x))). [para(10(a,2),2(a,1))]. given #30 (T,wt=17): 37 a(x,a(a(W,a(B,y)),z)) = a(x,a(y,a(z,z))). [para(7(a,1),2(a,2,2)),rewrite(2(8))]. given #31 (A,wt=44): 16 a(f1(a(a(B,x),a(a(B,y),z))),a(x,a(y,a(z,f1(a(a(B,x),a(a(B,y),z))))))) != a(x,a(y,a(z,f1(a(a(B,x),a(a(B,y),z)))))) # answer(fixed_point_combinator). [para(2(a,1),12(a,1,2,2)),rewrite(2(29))]. given #32 (F,wt=34): 716 a(f1(a(W,a(B,B))),a(a(a(W,a(B,W)),B),f1(a(W,a(B,B))))) != a(a(W,a(B,B)),f1(a(W,a(B,B)))) # answer(fixed_point_combinator). [para(69(a,2),44(a,1,2))]. given #33 (F,wt=34): 725 a(f1(a(W,a(B,B))),a(a(W,a(B,B)),f1(a(W,a(B,B))))) != a(a(a(W,a(B,W)),B),f1(a(W,a(B,B)))) # answer(fixed_point_combinator). [para(69(a,2),45(a,2))]. given #34 (F,wt=36): 1164 a(f1(a(a(W,a(B,W)),B)),a(a(a(W,a(B,W)),B),f1(a(W,a(B,B))))) != a(a(W,a(B,B)),f1(a(W,a(B,B)))) # answer(fixed_point_combinator). [para(7(a,2),716(a,1,1,1))]. given #35 (F,wt=34): 1171 a(f1(a(a(W,a(B,W)),B)),a(a(W,a(B,B)),f1(a(W,a(B,B))))) != a(a(W,a(B,B)),f1(a(W,a(B,B)))) # answer(fixed_point_combinator). [para(7(a,1),1164(a,1,2,1))]. given #36 (T,wt=17): 39 a(a(a(W,a(B,W)),x),y) = a(a(W,a(x,x)),y). [para(7(a,2),3(a,1,1)),rewrite(3(10,R))]. given #37 (T,wt=17): 41 a(a(W,a(W,a(B,x))),y) = a(a(x,a(y,y)),y). [para(7(a,1),3(a,2,1))]. given #38 (T,wt=17): 76 a(x,a(a(W,a(W,B)),y)) = a(x,a(y,a(y,y))). [para(14(a,1),2(a,2,2)),rewrite(2(9))]. given #39 (T,wt=17): 77 a(a(a(W,a(W,B)),W),x) = a(a(W,a(W,W)),x). [para(14(a,2),3(a,1,1)),rewrite(3(13,R))]. given #40 (A,wt=44): 17 a(f1(a(a(B,a(a(B,x),y)),z)),a(x,a(y,a(z,f1(a(a(B,a(a(B,x),y)),z)))))) != a(x,a(y,a(z,f1(a(a(B,a(a(B,x),y)),z))))) # answer(fixed_point_combinator). [para(2(a,1),12(a,1,2)),rewrite(2(30))]. given #41 (F,wt=34): 1180 a(f1(a(W,a(x,x))),a(a(a(W,a(B,W)),x),f1(a(W,a(x,x))))) != a(a(W,a(x,x)),f1(a(W,a(x,x)))) # answer(fixed_point_combinator). [para(39(a,2),5(a,1,2))]. given #42 (F,wt=34): 1182 a(f1(a(W,a(x,x))),a(a(W,a(x,x)),f1(a(W,a(x,x))))) != a(a(a(W,a(B,W)),x),f1(a(W,a(x,x)))) # answer(fixed_point_combinator). [para(39(a,2),5(a,2))]. given #43 (F,wt=36): 1167 a(a(W,a(B,B)),f1(a(a(W,a(B,W)),B))) != a(f1(a(W,a(B,B))),a(a(a(W,a(B,W)),B),f1(a(W,a(B,B))))) # answer(fixed_point_combinator). [para(7(a,2),716(a,2,2,1)),flip(a)]. given #44 (F,wt=34): 1941 a(a(W,a(B,B)),f1(a(a(W,a(B,W)),B))) != a(f1(a(W,a(B,B))),a(a(W,a(B,B)),f1(a(W,a(B,B))))) # answer(fixed_point_combinator). [para(7(a,1),1167(a,2,2,1))]. given #45 (T,wt=17): 78 a(a(W,a(W,a(W,B))),x) = a(a(x,a(x,x)),x). [para(14(a,1),3(a,2,1))]. given #46 (T,wt=17): 268 a(a(a(W,a(B,W)),W),x) = a(a(W,a(W,x)),x). [para(7(a,2),11(a,1,1))]. given #47 (T,wt=17): 291 a(a(W,a(a(B,W),x)),y) = a(a(W,a(W,x)),y). [para(11(a,2),9(a,2))]. given #48 (T,wt=17): 295 a(a(W,a(W,a(W,W))),B) = a(a(B,a(B,B)),B). [para(272(a,1),3(a,2,1))]. given #49 (A,wt=44): 21 a(f1(a(a(B,x),a(a(W,B),y))),a(x,a(y,a(y,f1(a(a(B,x),a(a(W,B),y))))))) != a(x,a(y,a(y,f1(a(a(B,x),a(a(W,B),y)))))) # answer(fixed_point_combinator). [para(6(a,1),12(a,1,2,2)),rewrite(6(33))]. given #50 (F,wt=36): 1170 a(a(a(W,a(B,W)),B),f1(a(a(W,a(B,W)),B))) != a(f1(a(W,a(B,B))),a(a(W,a(B,B)),f1(a(W,a(B,B))))) # answer(fixed_point_combinator). [para(7(a,2),725(a,2,2,1)),flip(a)]. given #51 (F,wt=36): 1176 a(f1(a(a(W,a(B,W)),B)),a(a(W,a(B,B)),f1(a(a(W,a(B,W)),B)))) != a(a(W,a(B,B)),f1(a(W,a(B,B)))) # answer(fixed_point_combinator). [para(7(a,2),1171(a,1,2,2,1))]. given #52 (F,wt=34): 2253 a(f1(a(W,a(B,B))),a(a(W,a(B,B)),f1(a(a(W,a(B,W)),B)))) != a(a(W,a(B,B)),f1(a(W,a(B,B)))) # answer(fixed_point_combinator). [para(7(a,1),1176(a,1,1,1))]. given #53 (F,wt=36): 1177 a(f1(a(a(W,a(B,W)),B)),a(a(W,a(B,B)),f1(a(W,a(B,B))))) != a(a(W,a(B,B)),f1(a(a(W,a(B,W)),B))) # answer(fixed_point_combinator). [para(7(a,2),1171(a,2,2,1))]. given #54 (T,wt=17): 389 a(a(a(W,a(B,W)),W),x) = a(a(W,a(x,x)),x). [para(7(a,2),31(a,1,1))]. given #55 (T,wt=17): 391 a(a(W,a(W,a(B,W))),x) = a(a(W,a(W,W)),x). [para(7(a,2),31(a,2,1)),rewrite(3(13,R)),flip(a)]. given #56 (T,wt=17): 736 a(a(a(W,W),a(B,W)),x) = a(a(W,a(W,W)),x). [para(28(a,2),3(a,1,1)),rewrite(2(16),215(15),391(16))]. given #57 (T,wt=19): 32 a(a(W,W),a(W,B)) = a(a(W,B),a(a(W,B),a(W,B))). [para(10(a,2),6(a,1))]. given #58 (A,wt=44): 22 a(f1(a(a(B,a(a(W,B),x)),y)),a(x,a(x,a(y,f1(a(a(B,a(a(W,B),x)),y)))))) != a(x,a(x,a(y,f1(a(a(B,a(a(W,B),x)),y))))) # answer(fixed_point_combinator). [para(6(a,1),12(a,1,2)),rewrite(6(34))]. given #59 (F,wt=36): 1794 a(f1(a(a(W,a(B,W)),x)),a(a(a(W,a(B,W)),x),f1(a(W,a(x,x))))) != a(a(W,a(x,x)),f1(a(W,a(x,x)))) # answer(fixed_point_combinator). [para(7(a,2),1180(a,1,1,1))]. given #60 (F,wt=34): 2503 a(f1(a(a(W,a(B,W)),x)),a(a(W,a(x,x)),f1(a(W,a(x,x))))) != a(a(W,a(x,x)),f1(a(W,a(x,x)))) # answer(fixed_point_combinator). [para(7(a,1),1794(a,1,2,1))]. given #61 (F,wt=34): 2607 a(f1(a(a(W,a(W,B)),W)),a(a(W,a(W,W)),f1(a(W,a(W,W))))) != a(a(W,a(W,W)),f1(a(W,a(W,W)))) # answer(fixed_point_combinator). [para(9(a,2),2503(a,1,1,1)),rewrite(291(9))]. given #62 (F,wt=36): 1797 a(f1(a(W,a(x,x))),a(a(a(W,a(B,W)),x),f1(a(a(W,a(B,W)),x)))) != a(a(W,a(x,x)),f1(a(W,a(x,x)))) # answer(fixed_point_combinator). [para(7(a,2),1180(a,1,2,2,1))]. given #63 (T,wt=19): 34 a(a(a(a(W,a(B,B)),x),y),z) = a(a(x,x),a(y,z)). [para(7(a,2),2(a,1,1,1))]. given #64 (T,wt=19): 35 a(a(a(W,a(B,a(B,x))),y),z) = a(x,a(a(y,y),z)). [para(7(a,2),2(a,1,1))]. ============================== PROOF ================================= % Proof 1 at 1.12 (+ 0.02) seconds: fixed_point_combinator. % Length of proof is 15. % Level of proof is 6. % Maximum clause weight is 76. % Given clauses 64. 1 (exists Q all x a(Q,x) = a(x,a(Q,x))) # label(fixed_point_combinator) # label(goal). [goal]. 2 a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). [assumption]. 3 a(a(W,x),y) = a(a(x,y),y) # label(W). [assumption]. 4 a(x,f1(x)) != a(f1(x),a(x,f1(x))) # label(fixed_point_combinator) # answer(fixed_point_combinator). [deny(1)]. 5 a(f1(x),a(x,f1(x))) != a(x,f1(x)) # answer(fixed_point_combinator). [copy(4),flip(a)]. 6 a(a(a(W,B),x),y) = a(x,a(x,y)). [para(3(a,2),2(a,1,1))]. 7 a(a(W,a(B,x)),y) = a(x,a(y,y)). [para(3(a,2),2(a,1))]. 10 a(a(W,W),x) = a(a(x,x),x). [para(3(a,2),3(a,1))]. 12 a(f1(a(a(B,x),y)),a(x,a(y,f1(a(a(B,x),y))))) != a(x,a(y,f1(a(a(B,x),y)))) # answer(fixed_point_combinator). [para(2(a,1),5(a,1,2)),rewrite(2(19))]. 21 a(f1(a(a(B,x),a(a(W,B),y))),a(x,a(y,a(y,f1(a(a(B,x),a(a(W,B),y))))))) != a(x,a(y,a(y,f1(a(a(B,x),a(a(W,B),y)))))) # answer(fixed_point_combinator). [para(6(a,1),12(a,1,2,2)),rewrite(6(33))]. 34 a(a(a(a(W,a(B,B)),x),y),z) = a(a(x,x),a(y,z)). [para(7(a,2),2(a,1,1,1))]. 35 a(a(a(W,a(B,a(B,x))),y),z) = a(x,a(a(y,y),z)). [para(7(a,2),2(a,1,1))]. 2798 a(f1(a(a(B,a(a(a(W,a(B,B)),x),y)),a(a(W,B),z))),a(a(x,x),a(y,a(z,a(z,f1(a(a(B,a(a(a(W,a(B,B)),x),y)),a(a(W,B),z)))))))) != a(a(x,x),a(y,a(z,a(z,f1(a(a(B,a(a(a(W,a(B,B)),x),y)),a(a(W,B),z))))))) # answer(fixed_point_combinator). [para(34(a,1),21(a,1,2)),rewrite(34(61))]. 2849 a(x,a(a(W,W),a(W,a(B,a(B,x))))) = a(a(W,W),a(W,a(B,a(B,x)))). [para(35(a,1),10(a,2)),rewrite(10(30,R)),flip(a)]. 2850 $F # answer(fixed_point_combinator). [resolve(2849,a,2798,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=64. Generated=7142. Kept=2847. proofs=1. Usable=57. Sos=2653. Demods=327. Limbo=43, Disabled=96. Hints=0. Weight_deleted=64. Literals_deleted=0. Forward_subsumed=4231. Back_subsumed=27. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=358 (2 lex), Back_demodulated=66. Back_unit_deleted=0. Demod_attempts=343230. Demod_rewrites=8043. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=7.59. User_CPU=1.12, System_CPU=0.02, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 26506 exit (max_proofs) Fri Apr 13 09:15:34 2007