============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11676 was started by mccune on cleo.thornwood, Sat Aug 12 21:22:12 2006 The command was "/home/mccune/bin/prover9 -f 2basis.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file 2basis.in assign(order,kbo). formulas(sos). f(x,x,y) = x # label(majority). f(f(x,w,y),z,w) = f(w,x,f(w,z,y)) # label(associativity2). f(A,B,C) != f(C,A,B) | f(A,B,C) != f(A,C,B) # answer(2a_2b). 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). f(x,x,y) = x # label(majority). [assumption]. f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2). [assumption]. f(A,B,C) != f(C,A,B) | f(A,B,C) != f(A,C,B) # answer(2a_2b). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Function symbol KB weights: A=1. B=1. C=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ A, B, C, f ]). Skipping inverse_order, because term ordering is KBO. Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 2). % (nonunit Horn with equality) Auto_process settings: % set(back_unit_deletion). % (Horn set with negative nonunits) % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 f(x,x,y) = x # label(majority). [assumption]. 2 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2). [assumption]. 4 f(C,A,B) != f(A,B,C) | f(A,C,B) != f(A,B,C) # answer(2a_2b). [copy(3),flip(a),flip(b)]. end_of_list. formulas(demodulators). 1 f(x,x,y) = x # label(majority). [assumption]. 2 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2). [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=6): 1 f(x,x,y) = x # label(majority). [assumption]. given #2 (I,wt=15): 2 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2). [assumption]. given #3 (I,wt=18): 4 f(C,A,B) != f(A,B,C) | f(A,C,B) != f(A,B,C) # answer(2a_2b). [copy(3),flip(a),flip(b)]. given #4 (T,wt=6): 6 f(x,y,x) = x. [para(1(a,1),2(a,1,1)),rewrite(1(3))]. given #5 (T,wt=12): 8 f(x,y,f(x,z,y)) = f(y,z,x). [para(6(a,1),2(a,1,1)),flip(a)]. given #6 (A,wt=15): 5 f(x,y,f(x,f(y,x,z),z)) = f(y,x,z). [para(2(a,1),1(a,1))]. given #7 (F,wt=6): 9 f(x,y,y) = y. [para(1(a,1),8(a,1,3)),rewrite(6(1)),flip(a)]. given #8 (F,wt=15): 17 f(x,y,f(f(x,z,y),y,x)) = f(x,z,y). [para(8(a,1),5(a,1,3,2)),rewrite(12(3),8(5))]. given #9 (T,wt=18): 10 f(x,y,f(x,z,f(y,u,x))) = f(f(x,u,y),z,x). [para(8(a,1),2(a,1,1)),flip(a)]. given #10 (T,wt=12): 32 f(f(x,y,z),x,z) = f(z,y,x). [para(17(a,1),10(a,1,3)),rewrite(9(3),8(3)),flip(a)]. given #11 (A,wt=21): 11 f(f(x,y,z),y,f(y,x,f(y,u,z))) = f(y,u,f(x,y,z)). [para(2(a,1),8(a,1,3))]. given #12 (F,wt=18): 70 f(B,A,C) != f(A,B,C) | f(A,C,B) != f(A,B,C) # answer(2a_2b). [back_rewrite(4),rewrite(49(4))]. given #13 (F,wt=9): 49 f(x,y,z) = f(z,y,x). [back_rewrite(17),rewrite(37(2),42(2),8(2))]. given #14 (T,wt=12): 42 f(x,y,f(y,z,x)) = f(x,z,y). [para(17(a,1),32(a,2)),rewrite(37(2),37(5),32(6),10(3),37(2))]. given #15 (T,wt=12): 76 f(x,y,f(z,y,x)) = f(x,y,z). [para(9(a,1),11(a,1,3)),rewrite(49(2),42(2),51(3),49(3),42(3)),flip(a)]. given #16 (A,wt=24): 14 f(x,f(y,z,u),f(x,f(z,y,f(z,x,u)),z)) = f(z,y,f(z,x,u)). [para(2(a,1),5(a,1,3,2)),rewrite(2(7))]. given #17 (F,wt=12): 87 f(x,y,f(y,x,z)) = f(y,x,z). [para(5(a,1),76(a,2)),rewrite(49(3),5(3))]. given #18 (F,wt=12): 91 f(x,y,f(x,y,z)) = f(x,y,z). [para(49(a,1),76(a,1,3))]. given #19 (T,wt=12): 93 f(x,f(y,x,z),z) = f(y,x,z). [back_rewrite(56),rewrite(87(4))]. given #20 (T,wt=12): 119 f(x,y,f(z,x,y)) = f(z,x,y). [para(87(a,1),11(a,2)),rewrite(91(3),75(3))]. given #21 (A,wt=27): 15 f(f(x,y,z),u,f(y,x,f(y,f(u,f(x,y,z),y),z))) = f(u,f(x,y,z),y). [para(2(a,1),5(a,1,3))]. given #22 (F,wt=12): 126 f(x,f(y,z,x),z) = f(y,z,x). [para(93(a,1),8(a,1,3)),rewrite(119(2)),flip(a)]. given #23 (F,wt=12): 130 f(x,f(y,x,z),y) = f(z,x,y). [para(49(a,1),93(a,1,2))]. given #24 (T,wt=12): 149 f(x,f(x,y,z),y) = f(z,y,x). [para(49(a,1),126(a,1,2))]. given #25 (T,wt=12): 150 f(x,f(x,y,z),z) = f(x,y,z). [para(8(a,1),130(a,1,2)),rewrite(49(4),8(4))]. given #26 (A,wt=27): 44 f(f(x,y,z),z,f(f(x,y,z),u,f(z,y,x))) = f(f(z,y,x),u,f(x,y,z)). [para(32(a,1),10(a,2,1)),rewrite(42(4))]. given #27 (F,wt=12): 154 f(x,f(y,z,x),y) = f(y,z,x). [para(42(a,1),130(a,1,2)),rewrite(49(4),42(4))]. given #28 (F,wt=15): 50 f(x,f(x,y,z),f(z,y,x)) = f(z,y,x). [back_rewrite(12),rewrite(49(5),8(5))]. given #29 (T,wt=15): 52 f(x,f(y,z,x),f(x,z,y)) = f(x,z,y). [back_rewrite(29),rewrite(49(3),42(5))]. given #30 (T,wt=15): 53 f(x,y,f(z,u,x)) = f(x,y,f(x,u,z)). [back_rewrite(48),rewrite(49(2),49(4))]. given #31 (A,wt=24): 54 f(f(x,y,f(x,z,u)),x,f(x,y,f(u,z,x))) = f(x,y,f(x,z,u)). [back_rewrite(45),rewrite(49(2),49(8),10(8),49(7))]. given #32 (F,wt=15): 65 f(x,y,f(z,x,u)) = f(x,z,f(x,y,u)). [back_rewrite(19),rewrite(49(5),11(5),42(4),49(2))]. given #33 (F,wt=9): 308 f(A,C,B) != f(A,B,C) # answer(2a_2b). [back_rewrite(70),rewrite(217(4)),xx(a)]. given #34 (T,wt=9): 217 f(x,y,z) = f(y,x,z). [para(9(a,1),65(a,2,3)),rewrite(119(2))]. ============================== PROOF ================================= % Proof 1 at 0.07 (+ 0.00) seconds: 2a_2b. % Length of proof is 30. % Level of proof is 15. % Maximum clause weight is 27. % Given clauses 34. 1 f(x,x,y) = x # label(majority). [assumption]. 2 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2). [assumption]. 3 f(A,B,C) != f(C,A,B) | f(A,B,C) != f(A,C,B) # answer(2a_2b). [assumption]. 4 f(C,A,B) != f(A,B,C) | f(A,C,B) != f(A,B,C) # answer(2a_2b). [copy(3),flip(a),flip(b)]. 5 f(x,y,f(x,f(y,x,z),z)) = f(y,x,z). [para(2(a,1),1(a,1))]. 6 f(x,y,x) = x. [para(1(a,1),2(a,1,1)),rewrite(1(3))]. 8 f(x,y,f(x,z,y)) = f(y,z,x). [para(6(a,1),2(a,1,1)),flip(a)]. 9 f(x,y,y) = y. [para(1(a,1),8(a,1,3)),rewrite(6(1)),flip(a)]. 10 f(x,y,f(x,z,f(y,u,x))) = f(f(x,u,y),z,x). [para(8(a,1),2(a,1,1)),flip(a)]. 11 f(f(x,y,z),y,f(y,x,f(y,u,z))) = f(y,u,f(x,y,z)). [para(2(a,1),8(a,1,3))]. 12 f(x,f(x,y,z),f(z,y,x)) = f(f(x,y,z),z,x). [para(8(a,1),8(a,1,3))]. 17 f(x,y,f(f(x,z,y),y,x)) = f(x,z,y). [para(8(a,1),5(a,1,3,2)),rewrite(12(3),8(5))]. 19 f(f(x,y,z),y,f(f(y,x,f(y,u,z)),y,f(x,y,z))) = f(y,x,f(y,u,z)). [para(2(a,1),17(a,1,3,1)),rewrite(2(8))]. 32 f(f(x,y,z),x,z) = f(z,y,x). [para(17(a,1),10(a,1,3)),rewrite(9(3),8(3)),flip(a)]. 36 f(f(x,y,z),z,f(z,y,x)) = f(z,x,f(x,y,z)). [para(32(a,1),8(a,1,3))]. 37 f(f(x,y,z),z,x) = f(x,z,f(z,y,x)). [para(8(a,1),32(a,1,1)),rewrite(36(3)),flip(a)]. 42 f(x,y,f(y,z,x)) = f(x,z,y). [para(17(a,1),32(a,2)),rewrite(37(2),37(5),32(6),10(3),37(2))]. 49 f(x,y,z) = f(z,y,x). [back_rewrite(17),rewrite(37(2),42(2),8(2))]. 51 f(f(x,y,z),z,f(z,y,x)) = f(z,y,x). [back_rewrite(36),rewrite(42(5))]. 65 f(x,y,f(z,x,u)) = f(x,z,f(x,y,u)). [back_rewrite(19),rewrite(49(5),11(5),42(4),49(2))]. 70 f(B,A,C) != f(A,B,C) | f(A,C,B) != f(A,B,C) # answer(2a_2b). [back_rewrite(4),rewrite(49(4))]. 75 f(f(x,y,z),y,f(y,x,z)) = f(y,z,f(x,y,z)). [para(9(a,1),11(a,1,3,3))]. 76 f(x,y,f(z,y,x)) = f(x,y,z). [para(9(a,1),11(a,1,3)),rewrite(49(2),42(2),51(3),49(3),42(3)),flip(a)]. 87 f(x,y,f(y,x,z)) = f(y,x,z). [para(5(a,1),76(a,2)),rewrite(49(3),5(3))]. 91 f(x,y,f(x,y,z)) = f(x,y,z). [para(49(a,1),76(a,1,3))]. 119 f(x,y,f(z,x,y)) = f(z,x,y). [para(87(a,1),11(a,2)),rewrite(91(3),75(3))]. 217 f(x,y,z) = f(y,x,z). [para(9(a,1),65(a,2,3)),rewrite(119(2))]. 308 f(A,C,B) != f(A,B,C) # answer(2a_2b). [back_rewrite(70),rewrite(217(4)),xx(a)]. 324 f(x,y,z) = f(x,z,y). [para(217(a,1),42(a,1,3)),rewrite(76(2))]. 325 $F # answer(2a_2b). [resolve(324,a,308,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=34. Generated=2035. Kept=323. proofs=1. Usable=16. Sos=151. Demods=140. Limbo=1, Disabled=157. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=1712. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=287 (3 lex), Back_demodulated=153. Back_unit_deleted=0. Demod_attempts=19635. Demod_rewrites=5453. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=4. Nonunit_bsub_feature_tests=2. Megabytes=0.26. User_CPU=0.07, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 11676 exit (max_proofs) Sat Aug 12 21:22:12 2006