============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13903 was started by mccune on cleo.thornwood, Mon Jun 19 17:06:22 2006 The command was "/home/mccune/bin/prover9 -f 2basis.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file 2basis.in assign(order,kbo). clauses(sos). f(x,x,y) = x # label(majority). f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # 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 INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 f(x,x,y) = x # label(majority). [input]. 2 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2). [input]. 3 f(A,B,C) != f(C,A,B) | f(A,B,C) != f(A,C,B) # answer(2a_2b). [input]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). 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: clauses(usable). end_of_list. clauses(sos). 4 f(x,x,y) = x # label(majority). [input]. 5 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2). [input]. 6 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. clauses(demodulators). 4 f(x,x,y) = x # label(majority). [input]. 5 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2). [input]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=6): 4 f(x,x,y) = x # label(majority). [input]. given #2 (I,wt=15): 5 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2). [input]. given #3 (I,wt=18): 6 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): 8 f(x,y,x) = x. [para(4(a,1),5(a,1,1)),demod(4(3))]. given #5 (T,wt=12): 10 f(x,y,f(x,z,y)) = f(y,z,x). [para(8(a,1),5(a,1,1)),flip(a)]. given #6 (A,wt=15): 7 f(x,y,f(x,f(y,x,z),z)) = f(y,x,z). [para(5(a,1),4(a,1))]. given #7 (F,wt=6): 11 f(x,y,y) = y. [para(4(a,1),10(a,1,3)),demod(8(1)),flip(a)]. given #8 (F,wt=15): 19 f(x,y,f(f(x,z,y),y,x)) = f(x,z,y). [para(10(a,1),7(a,1,3,2)),demod(14(3),10(5))]. given #9 (T,wt=18): 12 f(x,y,f(x,z,f(y,u,x))) = f(f(x,u,y),z,x). [para(10(a,1),5(a,1,1)),flip(a)]. given #10 (T,wt=12): 34 f(f(x,y,z),x,z) = f(z,y,x). [para(19(a,1),12(a,1,3)),demod(11(3),10(3)),flip(a)]. given #11 (A,wt=21): 13 f(f(x,y,z),y,f(y,x,f(y,u,z))) = f(y,u,f(x,y,z)). [para(5(a,1),10(a,1,3))]. given #12 (F,wt=18): 72 f(B,A,C) != f(A,B,C) | f(A,C,B) != f(A,B,C) # answer(2a_2b). [back_demod(6),demod(51(4))]. given #13 (F,wt=9): 51 f(x,y,z) = f(z,y,x). [back_demod(19),demod(39(2),44(2),10(2))]. given #14 (T,wt=12): 44 f(x,y,f(y,z,x)) = f(x,z,y). [para(19(a,1),34(a,2)),demod(39(2),39(5),34(6),12(3),39(2))]. given #15 (T,wt=12): 78 f(x,y,f(z,y,x)) = f(x,y,z). [para(11(a,1),13(a,1,3)),demod(51(2),44(2),53(3),51(3),44(3)),flip(a)]. given #16 (A,wt=24): 16 f(x,f(y,z,u),f(x,f(z,y,f(z,x,u)),z)) = f(z,y,f(z,x,u)). [para(5(a,1),7(a,1,3,2)),demod(5(7))]. given #17 (F,wt=12): 89 f(x,y,f(y,x,z)) = f(y,x,z). [para(7(a,1),78(a,2)),demod(51(3),7(3))]. given #18 (F,wt=12): 93 f(x,y,f(x,y,z)) = f(x,y,z). [para(51(a,1),78(a,1,3))]. given #19 (T,wt=12): 95 f(x,f(y,x,z),z) = f(y,x,z). [back_demod(58),demod(89(4))]. given #20 (T,wt=12): 121 f(x,y,f(z,x,y)) = f(z,x,y). [para(89(a,1),13(a,2)),demod(93(3),77(3))]. given #21 (A,wt=27): 17 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(5(a,1),7(a,1,3))]. given #22 (F,wt=12): 128 f(x,f(y,z,x),z) = f(y,z,x). [para(95(a,1),10(a,1,3)),demod(121(2)),flip(a)]. given #23 (F,wt=12): 132 f(x,f(y,x,z),y) = f(z,x,y). [para(51(a,1),95(a,1,2))]. given #24 (T,wt=12): 151 f(x,f(x,y,z),y) = f(z,y,x). [para(51(a,1),128(a,1,2))]. given #25 (T,wt=12): 152 f(x,f(x,y,z),z) = f(x,y,z). [para(10(a,1),132(a,1,2)),demod(51(4),10(4))]. given #26 (A,wt=27): 46 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(34(a,1),12(a,2,1)),demod(44(4))]. given #27 (F,wt=12): 156 f(x,f(y,z,x),y) = f(y,z,x). [para(44(a,1),132(a,1,2)),demod(51(4),44(4))]. given #28 (F,wt=15): 52 f(x,f(x,y,z),f(z,y,x)) = f(z,y,x). [back_demod(14),demod(51(5),10(5))]. given #29 (T,wt=15): 54 f(x,f(y,z,x),f(x,z,y)) = f(x,z,y). [back_demod(31),demod(51(3),44(5))]. given #30 (T,wt=15): 55 f(x,y,f(z,u,x)) = f(x,y,f(x,u,z)). [back_demod(50),demod(51(2),51(4))]. given #31 (A,wt=24): 56 f(f(x,y,f(x,z,u)),x,f(x,y,f(u,z,x))) = f(x,y,f(x,z,u)). [back_demod(47),demod(51(2),51(8),12(8),51(7))]. given #32 (F,wt=15): 67 f(x,y,f(z,x,u)) = f(x,z,f(x,y,u)). [back_demod(21),demod(51(5),13(5),44(4),51(2))]. given #33 (F,wt=9): 310 f(A,C,B) != f(A,B,C) # answer(2a_2b). [back_demod(72),demod(219(4)),xx(a)]. given #34 (T,wt=9): 219 f(x,y,z) = f(y,x,z). [para(11(a,1),67(a,2,3)),demod(121(2))]. ============================== PROOF ================================= % Proof 1 at 0.07 (+ 0.01) seconds: 2a_2b. % Length of proof is 30. % Level of proof is 15. % Maximum clause weight is 27. % Given clauses 34. 3 f(A,B,C) != f(C,A,B) | f(A,B,C) != f(A,C,B) # answer(2a_2b). [input]. 4 f(x,x,y) = x # label(majority). [input]. 5 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2). [input]. 6 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)]. 7 f(x,y,f(x,f(y,x,z),z)) = f(y,x,z). [para(5(a,1),4(a,1))]. 8 f(x,y,x) = x. [para(4(a,1),5(a,1,1)),demod(4(3))]. 10 f(x,y,f(x,z,y)) = f(y,z,x). [para(8(a,1),5(a,1,1)),flip(a)]. 11 f(x,y,y) = y. [para(4(a,1),10(a,1,3)),demod(8(1)),flip(a)]. 12 f(x,y,f(x,z,f(y,u,x))) = f(f(x,u,y),z,x). [para(10(a,1),5(a,1,1)),flip(a)]. 13 f(f(x,y,z),y,f(y,x,f(y,u,z))) = f(y,u,f(x,y,z)). [para(5(a,1),10(a,1,3))]. 14 f(x,f(x,y,z),f(z,y,x)) = f(f(x,y,z),z,x). [para(10(a,1),10(a,1,3))]. 19 f(x,y,f(f(x,z,y),y,x)) = f(x,z,y). [para(10(a,1),7(a,1,3,2)),demod(14(3),10(5))]. 21 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(5(a,1),19(a,1,3,1)),demod(5(8))]. 34 f(f(x,y,z),x,z) = f(z,y,x). [para(19(a,1),12(a,1,3)),demod(11(3),10(3)),flip(a)]. 38 f(f(x,y,z),z,f(z,y,x)) = f(z,x,f(x,y,z)). [para(34(a,1),10(a,1,3))]. 39 f(f(x,y,z),z,x) = f(x,z,f(z,y,x)). [para(10(a,1),34(a,1,1)),demod(38(3)),flip(a)]. 44 f(x,y,f(y,z,x)) = f(x,z,y). [para(19(a,1),34(a,2)),demod(39(2),39(5),34(6),12(3),39(2))]. 51 f(x,y,z) = f(z,y,x). [back_demod(19),demod(39(2),44(2),10(2))]. 53 f(f(x,y,z),z,f(z,y,x)) = f(z,y,x). [back_demod(38),demod(44(5))]. 67 f(x,y,f(z,x,u)) = f(x,z,f(x,y,u)). [back_demod(21),demod(51(5),13(5),44(4),51(2))]. 72 f(B,A,C) != f(A,B,C) | f(A,C,B) != f(A,B,C) # answer(2a_2b). [back_demod(6),demod(51(4))]. 77 f(f(x,y,z),y,f(y,x,z)) = f(y,z,f(x,y,z)). [para(11(a,1),13(a,1,3,3))]. 78 f(x,y,f(z,y,x)) = f(x,y,z). [para(11(a,1),13(a,1,3)),demod(51(2),44(2),53(3),51(3),44(3)),flip(a)]. 89 f(x,y,f(y,x,z)) = f(y,x,z). [para(7(a,1),78(a,2)),demod(51(3),7(3))]. 93 f(x,y,f(x,y,z)) = f(x,y,z). [para(51(a,1),78(a,1,3))]. 121 f(x,y,f(z,x,y)) = f(z,x,y). [para(89(a,1),13(a,2)),demod(93(3),77(3))]. 219 f(x,y,z) = f(y,x,z). [para(11(a,1),67(a,2,3)),demod(121(2))]. 310 f(A,C,B) != f(A,B,C) # answer(2a_2b). [back_demod(72),demod(219(4)),xx(a)]. 326 f(x,y,z) = f(x,z,y). [para(219(a,1),44(a,1,3)),demod(78(2))]. 327 $F # answer(2a_2b). [resolve(326,a,310,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=34. Generated=2035. Kept=323. proofs=1. Usable=16. Sos=151. Demods=140. Denials=0. 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=19612. 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.27. User_CPU=0.07, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13903 exit (max_proofs) Mon Jun 19 17:06:22 2006