============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13904 was started by mccune on cleo.thornwood, Mon Jun 19 17:06:22 2006 The command was "/home/mccune/bin/prover9 -f dep-2b.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file dep-2b.in assign(order,kbo). clauses(sos). f(x,x,y) = x # label(majority). f(x,y,z) = f(z,x,y) # label(2a). f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). end_of_list. clauses(goals). f(x,y,z) = f(x,z,y) # answer(2b). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). f(c1,c3,c2) != f(c1,c2,c3) # answer(2b). end_of_list. ============================== end of process goals ================== ============================== 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(x,y,z) = f(z,x,y) # label(2a). [input]. 3 f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [input]. 4 f(c1,c3,c2) != f(c1,c2,c3) # answer(2b). [clausify]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: no changes. Term ordering decisions: Function symbol KB weights: c1=1. c2=1. c3=1. f=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, 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). Auto_process settings: no changes. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 5 f(x,x,y) = x # label(majority). [input]. 6 f(x,y,z) = f(z,x,y) # label(2a). [input]. 7 f(x,y,f(z,y,u)) = f(y,u,f(x,y,z)) # label(associativity). [copy(3),demod(6(2,R)),flip(a)]. 8 f(c1,c3,c2) != f(c1,c2,c3) # answer(2b). [clausify]. end_of_list. clauses(demodulators). 5 f(x,x,y) = x # label(majority). [input]. 6 f(x,y,z) = f(z,x,y) # label(2a). [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=6): 5 f(x,x,y) = x # label(majority). [input]. given #2 (I,wt=9): 6 f(x,y,z) = f(z,x,y) # label(2a). [input]. given #3 (I,wt=15): 7 f(x,y,f(z,y,u)) = f(y,u,f(x,y,z)) # label(associativity). [copy(3),demod(6(2,R)),flip(a)]. given #4 (I,wt=9): 8 f(c1,c3,c2) != f(c1,c2,c3) # answer(2b). [clausify]. given #5 (T,wt=6): 9 f(x,y,y) = y. [para(6(a,1),5(a,1))]. given #6 (A,wt=6): 10 f(x,y,x) = x. [para(6(a,2),5(a,1))]. given #7 (F,wt=12): 21 f(x,y,f(z,x,y)) = f(z,x,y). [para(10(a,1),7(a,1,3)),flip(a)]. given #8 (F,wt=12): 23 f(x,y,f(x,y,z)) = f(y,z,x). [para(10(a,1),7(a,2,3))]. given #9 (T,wt=12): 24 f(x,f(y,z,x),z) = f(y,z,x). [para(21(a,1),6(a,1)),demod(6(3)),flip(a)]. given #10 (T,wt=12): 25 f(x,y,f(y,z,x)) = f(z,x,y). [para(6(a,1),21(a,1,3))]. given #11 (A,wt=15): 11 f(x,f(y,x,z),u) = f(x,z,f(u,x,y)). [para(7(a,1),6(a,1)),demod(6(4)),flip(a)]. given #12 (F,wt=15): 12 f(x,f(y,z,u),z) = f(y,z,f(u,z,x)). [para(7(a,2),6(a,2))]. given #13 (F,wt=15): 13 f(x,y,f(z,u,y)) = f(y,z,f(x,y,u)). [para(6(a,1),7(a,1,3))]. given #14 (T,wt=15): 14 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)). [para(6(a,2),7(a,1,3)),flip(a)]. given #15 (T,wt=15): 15 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(6(a,1),7(a,2,3)),flip(a)]. given #16 (A,wt=15): 16 f(x,y,f(z,y,u)) = f(y,u,f(y,z,x)). [para(6(a,2),7(a,2,3))]. given #17 (F,wt=15): 20 f(x,y,f(z,y,f(x,y,z))) = f(x,y,z). [para(9(a,1),7(a,2))]. given #18 (F,wt=15): 31 f(x,y,f(z,x,u)) = f(x,y,f(x,u,z)). [para(7(a,1),23(a,1,3)),demod(30(3),11(4)),flip(a)]. given #19 (T,wt=15): 45 f(x,y,f(z,x,f(x,z,y))) = f(z,x,y). [para(25(a,1),23(a,2)),demod(6(3),36(3),6(3,R),11(3),6(2),11(2))]. given #20 (T,wt=12): 325 f(x,y,f(x,z,y)) = f(x,y,z). [back_demod(234),demod(295(3))]. given #21 (A,wt=21): 17 f(x,y,f(y,z,f(u,y,v))) = f(y,z,f(y,v,f(x,y,u))). [para(7(a,1),7(a,1,3)),demod(11(6),6(5,R))]. given #22 (F,wt=9): 337 f(x,y,z) = f(z,y,x). [para(325(a,1),6(a,1)),demod(6(3),46(3),328(3))]. ============================== PROOF ================================= % Proof 1 at 0.10 (+ 0.00) seconds: 2b. % Length of proof is 28. % Level of proof is 12. % Maximum clause weight is 18. % Given clauses 22. 3 f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [input]. 5 f(x,x,y) = x # label(majority). [input]. 6 f(x,y,z) = f(z,x,y) # label(2a). [input]. 7 f(x,y,f(z,y,u)) = f(y,u,f(x,y,z)) # label(associativity). [copy(3),demod(6(2,R)),flip(a)]. 8 f(c1,c3,c2) != f(c1,c2,c3) # answer(2b). [clausify]. 9 f(x,y,y) = y. [para(6(a,1),5(a,1))]. 10 f(x,y,x) = x. [para(6(a,2),5(a,1))]. 11 f(x,f(y,x,z),u) = f(x,z,f(u,x,y)). [para(7(a,1),6(a,1)),demod(6(4)),flip(a)]. 15 f(x,y,f(z,u,x)) = f(u,x,f(z,x,y)). [para(6(a,1),7(a,2,3)),flip(a)]. 20 f(x,y,f(z,y,f(x,y,z))) = f(x,y,z). [para(9(a,1),7(a,2))]. 21 f(x,y,f(z,x,y)) = f(z,x,y). [para(10(a,1),7(a,1,3)),flip(a)]. 23 f(x,y,f(x,y,z)) = f(y,z,x). [para(10(a,1),7(a,2,3))]. 24 f(x,f(y,z,x),z) = f(y,z,x). [para(21(a,1),6(a,1)),demod(6(3)),flip(a)]. 25 f(x,y,f(y,z,x)) = f(z,x,y). [para(6(a,1),21(a,1,3))]. 36 f(x,f(x,y,z),z) = f(y,z,x). [para(6(a,1),24(a,1,2))]. 45 f(x,y,f(z,x,f(x,z,y))) = f(z,x,y). [para(25(a,1),23(a,2)),demod(6(3),36(3),6(3,R),11(3),6(2),11(2))]. 46 f(x,f(y,z,x),u) = f(x,y,f(u,x,z)). [para(6(a,1),11(a,1,2))]. 47 f(x,f(x,y,z),u) = f(x,y,f(u,x,z)). [para(6(a,2),11(a,1,2))]. 149 f(x,y,f(z,y,f(z,x,y))) = f(z,x,y). [para(15(a,1),9(a,1))]. 234 f(x,y,f(z,y,f(x,z,f(x,y,z)))) = f(x,y,z). [para(20(a,1),23(a,2)),demod(6(5),11(5),9(5),6(4),6(4),47(4),6(3),47(3))]. 295 f(x,y,f(z,x,f(z,y,x))) = f(z,x,y). [para(6(a,2),45(a,1,3,3))]. 300 f(x,y,f(x,z,f(y,z,x))) = f(z,x,y). [para(7(a,2),45(a,1,3))]. 325 f(x,y,f(x,z,y)) = f(x,y,z). [back_demod(234),demod(295(3))]. 327 f(x,y,f(z,y,x)) = f(z,x,y). [back_demod(149),demod(325(2))]. 328 f(x,y,f(y,x,z)) = f(z,x,y). [back_demod(300),demod(327(2))]. 337 f(x,y,z) = f(z,y,x). [para(325(a,1),6(a,1)),demod(6(3),46(3),328(3))]. 451 f(x,y,z) = f(x,z,y). [para(337(a,1),6(a,1))]. 452 $F # answer(2b). [resolve(451,a,8,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=22. Generated=1788. Kept=447. proofs=1. Usable=19. Sos=358. Demods=101. Denials=0. Limbo=0, Disabled=73. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=1341. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=170 (3 lex), Back_demodulated=69. Back_unit_deleted=0. Demod_attempts=14263. Demod_rewrites=3778. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.38. User_CPU=0.10, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13904 exit (max_proofs) Mon Jun 19 17:06:22 2006