============================== Prover9 =============================== Prover9 (32) version 2009-02A, February 2009. Process 12005 was started by mccune on cleo, Wed Feb 25 09:58:01 2009 The command was "/home/mccune/bin/prover9 -f 2basis.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file 2basis.in assign(max_seconds,30). 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). end_of_list. formulas(goals). f(x,y,z) = f(z,x,y) # label(2a). f(x,y,z) = f(x,z,y) # label(2b). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 f(x,y,z) = f(z,x,y) # label(2a) # label(non_clause) # label(goal). [goal]. 2 f(x,y,z) = f(x,z,y) # label(2b) # label(non_clause) # label(goal). [goal]. ============================== 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(c3,c1,c2) != f(c1,c2,c3) # label(2a). [deny(1)]. f(c4,c6,c5) != f(c4,c5,c6) # label(2b). [deny(2)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label 2a to answer in negative clause % copying label 2b to answer in negative clause % assign(max_proofs, 2). % (Horn set with more than one neg. clause) Term ordering decisions: Function symbol KB weights: c1=1. c2=1. c3=1. c4=1. c5=1. c6=1. f=1. Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, c4, c5, c6, f ]). Skipping inverse_order, because term ordering is KBO. Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). kept: 3 f(x,x,y) = x # label(majority). [assumption]. kept: 4 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2). [assumption]. kept: 5 f(c3,c1,c2) != f(c1,c2,c3) # label(2a) # answer(2a). [deny(1)]. kept: 6 f(c4,c6,c5) != f(c4,c5,c6) # label(2b) # answer(2b). [deny(2)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 3 f(x,x,y) = x # label(majority). [assumption]. 4 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2). [assumption]. 5 f(c3,c1,c2) != f(c1,c2,c3) # label(2a) # answer(2a). [deny(1)]. 6 f(c4,c6,c5) != f(c4,c5,c6) # label(2b) # answer(2b). [deny(2)]. end_of_list. formulas(demodulators). 3 f(x,x,y) = x # label(majority). [assumption]. 4 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.01 seconds. given #1 (I,wt=6): 3 f(x,x,y) = x # label(majority). [assumption]. given #2 (I,wt=15): 4 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2). [assumption]. given #3 (I,wt=9): 5 f(c3,c1,c2) != f(c1,c2,c3) # label(2a) # answer(2a). [deny(1)]. given #4 (I,wt=9): 6 f(c4,c6,c5) != f(c4,c5,c6) # label(2b) # answer(2b). [deny(2)]. given #5 (A,wt=15): 7 f(x,y,f(x,f(y,x,z),z)) = f(y,x,z). [para(4(a,1),3(a,1))]. given #6 (T,wt=6): 8 f(x,y,x) = x. [para(3(a,1),4(a,1,1)),rewrite([3(3)])]. given #7 (T,wt=6): 14 f(x,y,y) = y. [para(8(a,1),7(a,1,3)),rewrite([8(1)]),flip(a)]. given #8 (T,wt=12): 13 f(x,y,f(x,z,y)) = f(y,z,x). [para(8(a,1),4(a,1,1)),flip(a)]. given #9 (T,wt=18): 15 f(x,y,f(x,z,f(y,u,x))) = f(f(x,u,y),z,x). [para(13(a,1),4(a,1,1)),flip(a)]. given #10 (A,wt=21): 9 f(f(x,y,f(x,z,u)),w,z) = f(z,f(y,x,u),f(z,w,x)). [para(4(a,1),4(a,1,1))]. given #11 (T,wt=15): 19 f(x,y,f(f(x,z,y),y,x)) = f(x,z,y). [para(3(a,1),15(a,2)),rewrite([18(3)])]. given #12 (T,wt=12): 45 f(f(x,y,z),x,z) = f(z,y,x). [para(19(a,1),15(a,1,3)),rewrite([14(3),13(3)]),flip(a)]. given #13 (T,wt=9): 69 f(x,y,z) = f(z,y,x). [back_rewrite(19),rewrite([55(2),63(2),13(2)])]. given #14 (T,wt=12): 63 f(x,y,f(y,z,x)) = f(x,z,y). [para(19(a,1),45(a,2)),rewrite([55(2),55(5),45(6),15(3),55(2)])]. given #15 (A,wt=24): 11 f(x,f(y,z,u),f(x,f(z,y,f(z,x,u)),z)) = f(z,y,f(z,x,u)). [para(4(a,1),7(a,1,3,2)),rewrite([4(7)])]. given #16 (F,wt=9): 101 f(c2,c1,c3) != f(c1,c2,c3) # answer(2a). [back_rewrite(5),rewrite([69(4)])]. given #17 (T,wt=15): 64 f(f(x,y,z),x,f(z,y,x)) = f(x,y,z). [para(45(a,1),45(a,2)),rewrite([63(2)])]. given #18 (T,wt=15): 70 f(x,f(x,y,z),f(z,y,x)) = f(z,y,x). [back_rewrite(18),rewrite([69(5),13(5)])]. given #19 (T,wt=15): 72 f(f(x,y,z),z,f(z,y,x)) = f(z,y,x). [back_rewrite(54),rewrite([63(5)])]. given #20 (T,wt=15): 74 f(x,y,f(z,u,x)) = f(x,y,f(x,u,z)). [back_rewrite(67),rewrite([69(2),69(4)])]. given #21 (A,wt=27): 12 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(4(a,1),7(a,1,3))]. given #22 (T,wt=15): 75 f(x,y,f(z,f(x,y,z),x)) = f(x,y,z). [back_rewrite(66),rewrite([69(3)])]. given #23 (T,wt=12): 164 f(x,y,f(z,x,y)) = f(y,x,z). [para(7(a,1),75(a,1,3,2)),rewrite([69(4),50(4),102(3),7(5)])]. given #24 (T,wt=12): 166 f(x,f(x,y,z),z) = f(x,y,z). [para(75(a,1),13(a,2)),rewrite([69(5),75(5),69(4),164(4)])]. given #25 (T,wt=12): 167 f(x,y,f(z,y,x)) = f(x,y,z). [para(69(a,1),75(a,1,3,2)),rewrite([166(2)])]. given #26 (A,wt=21): 16 f(f(x,y,z),y,f(y,x,f(y,u,z))) = f(y,u,f(x,y,z)). [para(4(a,1),13(a,1,3))]. given #27 (T,wt=12): 168 f(x,y,f(x,y,z)) = f(x,y,z). [para(69(a,1),75(a,1,3)),rewrite([166(2)])]. given #28 (T,wt=12): 179 f(x,y,f(y,x,z)) = f(y,x,z). [para(69(a,1),164(a,1,3))]. given #29 (T,wt=12): 190 f(x,f(y,x,z),z) = f(y,x,z). [back_rewrite(80),rewrite([179(4)])]. given #30 (T,wt=12): 213 f(x,f(y,z,x),y) = f(x,z,y). [para(166(a,1),13(a,1,3)),rewrite([13(2)]),flip(a)]. given #31 (A,wt=21): 27 f(x,f(x,y,z),f(x,u,y)) = f(x,y,f(x,u,f(y,x,z))). [para(9(a,1),4(a,1))]. ============================== PROOF ================================= % Proof 1 at 0.07 (+ 0.00) seconds: 2a. % Length of proof is 39. % Level of proof is 16. % Maximum clause weight is 21. % Given clauses 31. 1 f(x,y,z) = f(z,x,y) # label(2a) # label(non_clause) # label(goal). [goal]. 3 f(x,x,y) = x # label(majority). [assumption]. 4 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2). [assumption]. 5 f(c3,c1,c2) != f(c1,c2,c3) # label(2a) # answer(2a). [deny(1)]. 7 f(x,y,f(x,f(y,x,z),z)) = f(y,x,z). [para(4(a,1),3(a,1))]. 8 f(x,y,x) = x. [para(3(a,1),4(a,1,1)),rewrite([3(3)])]. 9 f(f(x,y,f(x,z,u)),w,z) = f(z,f(y,x,u),f(z,w,x)). [para(4(a,1),4(a,1,1))]. 13 f(x,y,f(x,z,y)) = f(y,z,x). [para(8(a,1),4(a,1,1)),flip(a)]. 14 f(x,y,y) = y. [para(8(a,1),7(a,1,3)),rewrite([8(1)]),flip(a)]. 15 f(x,y,f(x,z,f(y,u,x))) = f(f(x,u,y),z,x). [para(13(a,1),4(a,1,1)),flip(a)]. 16 f(f(x,y,z),y,f(y,x,f(y,u,z))) = f(y,u,f(x,y,z)). [para(4(a,1),13(a,1,3))]. 18 f(x,f(x,y,z),f(z,y,x)) = f(f(x,y,z),z,x). [para(13(a,1),13(a,1,3))]. 19 f(x,y,f(f(x,z,y),y,x)) = f(x,z,y). [para(3(a,1),15(a,2)),rewrite([18(3)])]. 27 f(x,f(x,y,z),f(x,u,y)) = f(x,y,f(x,u,f(y,x,z))). [para(9(a,1),4(a,1))]. 32 f(x,f(y,z,x),f(x,u,z)) = f(f(z,y,x),u,x). [para(14(a,1),9(a,1,1,3)),flip(a)]. 33 f(x,f(f(y,x,z),y,z),f(x,u,y)) = f(x,y,f(x,u,z)). [para(14(a,1),9(a,1,1)),rewrite([4(2)]),flip(a)]. 42 f(f(f(x,y,z),z,x),z,x) = f(f(z,f(x,y,z),x),y,x). [para(19(a,1),13(a,1,3)),rewrite([32(4)]),flip(a)]. 45 f(f(x,y,z),x,z) = f(z,y,x). [para(19(a,1),15(a,1,3)),rewrite([14(3),13(3)]),flip(a)]. 50 f(x,f(y,x,z),f(x,u,z)) = f(x,z,f(x,u,y)). [back_rewrite(33),rewrite([45(2)])]. 54 f(f(x,y,z),z,f(z,y,x)) = f(z,x,f(x,y,z)). [para(45(a,1),13(a,1,3))]. 55 f(f(x,y,z),z,x) = f(x,z,f(z,y,x)). [para(13(a,1),45(a,1,1)),rewrite([54(3)]),flip(a)]. 63 f(x,y,f(y,z,x)) = f(x,z,y). [para(19(a,1),45(a,2)),rewrite([55(2),55(5),45(6),15(3),55(2)])]. 66 f(f(x,f(y,z,x),y),z,y) = f(y,z,x). [back_rewrite(42),rewrite([55(2),63(2),55(2),63(2)]),flip(a)]. 69 f(x,y,z) = f(z,y,x). [back_rewrite(19),rewrite([55(2),63(2),13(2)])]. 75 f(x,y,f(z,f(x,y,z),x)) = f(x,y,z). [back_rewrite(66),rewrite([69(3)])]. 90 f(x,f(y,z,x),f(x,u,z)) = f(x,u,f(z,y,x)). [back_rewrite(32),rewrite([69(5)])]. 101 f(c2,c1,c3) != f(c1,c2,c3) # answer(2a). [back_rewrite(5),rewrite([69(4)])]. 102 f(x,y,f(x,f(z,x,y),z)) = f(y,x,z). [para(69(a,1),7(a,1,3,2))]. 164 f(x,y,f(z,x,y)) = f(y,x,z). [para(7(a,1),75(a,1,3,2)),rewrite([69(4),50(4),102(3),7(5)])]. 166 f(x,f(x,y,z),z) = f(x,y,z). [para(75(a,1),13(a,2)),rewrite([69(5),75(5),69(4),164(4)])]. 167 f(x,y,f(z,y,x)) = f(x,y,z). [para(69(a,1),75(a,1,3,2)),rewrite([166(2)])]. 179 f(x,y,f(y,x,z)) = f(y,x,z). [para(69(a,1),164(a,1,3))]. 222 f(f(x,y,z),y,f(y,x,z)) = f(z,y,x). [para(14(a,1),16(a,1,3,3)),rewrite([164(5)])]. 263 f(x,f(x,y,z),y) = f(y,x,z). [para(14(a,1),27(a,1,3)),rewrite([179(4),179(4)])]. 270 f(x,y,f(x,z,f(y,x,u))) = f(x,z,f(y,u,x)). [para(69(a,1),27(a,1,2)),rewrite([90(3)]),flip(a)]. 271 f(x,f(x,y,z),f(y,u,x)) = f(x,u,f(y,z,x)). [para(69(a,1),27(a,1,3)),rewrite([270(6)])]. 297 f(f(x,y,z),y,u) = f(y,u,f(x,z,y)). [para(179(a,1),27(a,1,3)),rewrite([263(4),270(7),69(4),270(5)])]. 331 f(x,y,z) = f(y,x,z). [back_rewrite(222),rewrite([297(3),271(3),167(2)])]. 332 $F # answer(2a). [resolve(331,a,101,a)]. ============================== end of proof ========================== % Redundant proof: 346 $F # answer(2a). [back_rewrite(101),rewrite([331(4)]),xx(a)]. % Disable descendants (x means already disabled): 5x 101x given #32 (T,wt=9): 331 f(x,y,z) = f(y,x,z). [back_rewrite(222),rewrite([297(3),271(3),167(2)])]. ============================== PROOF ================================= % Proof 2 at 0.08 (+ 0.00) seconds: 2b. % Length of proof is 38. % Level of proof is 16. % Maximum clause weight is 21. % Given clauses 32. 2 f(x,y,z) = f(x,z,y) # label(2b) # label(non_clause) # label(goal). [goal]. 3 f(x,x,y) = x # label(majority). [assumption]. 4 f(f(x,y,z),u,y) = f(y,x,f(y,u,z)) # label(associativity2). [assumption]. 6 f(c4,c6,c5) != f(c4,c5,c6) # label(2b) # answer(2b). [deny(2)]. 7 f(x,y,f(x,f(y,x,z),z)) = f(y,x,z). [para(4(a,1),3(a,1))]. 8 f(x,y,x) = x. [para(3(a,1),4(a,1,1)),rewrite([3(3)])]. 9 f(f(x,y,f(x,z,u)),w,z) = f(z,f(y,x,u),f(z,w,x)). [para(4(a,1),4(a,1,1))]. 13 f(x,y,f(x,z,y)) = f(y,z,x). [para(8(a,1),4(a,1,1)),flip(a)]. 14 f(x,y,y) = y. [para(8(a,1),7(a,1,3)),rewrite([8(1)]),flip(a)]. 15 f(x,y,f(x,z,f(y,u,x))) = f(f(x,u,y),z,x). [para(13(a,1),4(a,1,1)),flip(a)]. 16 f(f(x,y,z),y,f(y,x,f(y,u,z))) = f(y,u,f(x,y,z)). [para(4(a,1),13(a,1,3))]. 18 f(x,f(x,y,z),f(z,y,x)) = f(f(x,y,z),z,x). [para(13(a,1),13(a,1,3))]. 19 f(x,y,f(f(x,z,y),y,x)) = f(x,z,y). [para(3(a,1),15(a,2)),rewrite([18(3)])]. 27 f(x,f(x,y,z),f(x,u,y)) = f(x,y,f(x,u,f(y,x,z))). [para(9(a,1),4(a,1))]. 32 f(x,f(y,z,x),f(x,u,z)) = f(f(z,y,x),u,x). [para(14(a,1),9(a,1,1,3)),flip(a)]. 33 f(x,f(f(y,x,z),y,z),f(x,u,y)) = f(x,y,f(x,u,z)). [para(14(a,1),9(a,1,1)),rewrite([4(2)]),flip(a)]. 42 f(f(f(x,y,z),z,x),z,x) = f(f(z,f(x,y,z),x),y,x). [para(19(a,1),13(a,1,3)),rewrite([32(4)]),flip(a)]. 45 f(f(x,y,z),x,z) = f(z,y,x). [para(19(a,1),15(a,1,3)),rewrite([14(3),13(3)]),flip(a)]. 50 f(x,f(y,x,z),f(x,u,z)) = f(x,z,f(x,u,y)). [back_rewrite(33),rewrite([45(2)])]. 54 f(f(x,y,z),z,f(z,y,x)) = f(z,x,f(x,y,z)). [para(45(a,1),13(a,1,3))]. 55 f(f(x,y,z),z,x) = f(x,z,f(z,y,x)). [para(13(a,1),45(a,1,1)),rewrite([54(3)]),flip(a)]. 63 f(x,y,f(y,z,x)) = f(x,z,y). [para(19(a,1),45(a,2)),rewrite([55(2),55(5),45(6),15(3),55(2)])]. 66 f(f(x,f(y,z,x),y),z,y) = f(y,z,x). [back_rewrite(42),rewrite([55(2),63(2),55(2),63(2)]),flip(a)]. 69 f(x,y,z) = f(z,y,x). [back_rewrite(19),rewrite([55(2),63(2),13(2)])]. 75 f(x,y,f(z,f(x,y,z),x)) = f(x,y,z). [back_rewrite(66),rewrite([69(3)])]. 90 f(x,f(y,z,x),f(x,u,z)) = f(x,u,f(z,y,x)). [back_rewrite(32),rewrite([69(5)])]. 102 f(x,y,f(x,f(z,x,y),z)) = f(y,x,z). [para(69(a,1),7(a,1,3,2))]. 164 f(x,y,f(z,x,y)) = f(y,x,z). [para(7(a,1),75(a,1,3,2)),rewrite([69(4),50(4),102(3),7(5)])]. 166 f(x,f(x,y,z),z) = f(x,y,z). [para(75(a,1),13(a,2)),rewrite([69(5),75(5),69(4),164(4)])]. 167 f(x,y,f(z,y,x)) = f(x,y,z). [para(69(a,1),75(a,1,3,2)),rewrite([166(2)])]. 179 f(x,y,f(y,x,z)) = f(y,x,z). [para(69(a,1),164(a,1,3))]. 222 f(f(x,y,z),y,f(y,x,z)) = f(z,y,x). [para(14(a,1),16(a,1,3,3)),rewrite([164(5)])]. 263 f(x,f(x,y,z),y) = f(y,x,z). [para(14(a,1),27(a,1,3)),rewrite([179(4),179(4)])]. 270 f(x,y,f(x,z,f(y,x,u))) = f(x,z,f(y,u,x)). [para(69(a,1),27(a,1,2)),rewrite([90(3)]),flip(a)]. 271 f(x,f(x,y,z),f(y,u,x)) = f(x,u,f(y,z,x)). [para(69(a,1),27(a,1,3)),rewrite([270(6)])]. 297 f(f(x,y,z),y,u) = f(y,u,f(x,z,y)). [para(179(a,1),27(a,1,3)),rewrite([263(4),270(7),69(4),270(5)])]. 331 f(x,y,z) = f(y,x,z). [back_rewrite(222),rewrite([297(3),271(3),167(2)])]. 347 $F # answer(2b). [para(331(a,1),6(a,1)),rewrite([69(4),331(4)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=32. Generated=1488. Kept=342. proofs=2. Usable=16. Sos=151. Demods=144. Limbo=0, Disabled=179. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1144. Back_subsumed=3. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=314 (2 lex), Back_demodulated=172. Back_unit_deleted=0. Demod_attempts=14818. Demod_rewrites=3587. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.33. User_CPU=0.08, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 2 proofs. Process 12005 exit (max_proofs) Wed Feb 25 09:58:01 2009