----- Prover9 July-2005D, 18 July 2005 ----- Process 14302 was started by mccune on theorem.mcs.anl.gov, Fri Jul 22 14:47:19 2005 The command was "prover9 -f dependency.in". % Reading from file dependency.in set(auto). % set(auto) -> set(auto1). % set(auto1) -> set(auto_inference). % set(auto1) -> set(fof_reduction). % set(auto1) -> set(predicate_elimination). % set(auto1) -> set(unfold_eq). % set(unfold_eq) -> assign(unfold_eq_limit, 2147483647). % set(unfold_eq) -> clear(fold_eq). % set(auto1) -> set(inverse_order). % set(auto1) -> assign(new_constants, 1). % assign(new_constants, 1) -> clear(x_proofs). % assign(new_constants, 1) -> clear(rx_proofs). % set(auto1) -> assign(lex_dep_demod_lim, 11). % set(auto1) -> set(lex_dep_demod_sane). % set(auto1) -> assign(max_weight, 100). % set(auto1) -> assign(age_part, 1). % set(auto1) -> assign(weight_part, 2). % set(auto1) -> assign(weight_neg_part, 2). % set(auto1) -> assign(sos_limit, 10000). % set(auto1) -> clear(x_proofs). % set(auto1) -> assign(stats, lots). % set(auto1) -> assign(max_megs, 200). % set(auto1) -> clear(clocks). 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). f(A,B,C) != f(A,C,B) # answer(2b). end_of_list. % Finished reading the input. % Entering prover search function. % Assigned IDs to 4 clauses. % Predicate elimination: (none). % 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). % Reasonable options, based on the structure of the clauses: % (nothing changed) % 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 (R)) flip a] 8 f(A,C,B) != f(A,B,C) # answer(2b). [copy 4 flip a] 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(goals). end_of_list. % Starting search at 0.00 seconds. given #1 (wt=6): 5 f(x,x,y) = x # label(majority). [input] given #2 (wt=9): 6 f(x,y,z) = f(z,x,y) # label(2a). [input] given #3 (wt=15): 7 f(x,y,f(z,y,u)) = f(y,u,f(x,y,z)) # label(associativity). [copy 3 demod (6 (R)) flip a] given #4 (wt=9): 8 f(A,C,B) != f(A,B,C) # answer(2b). [copy 4 flip a] given #5 (wt=6): 9 f(x,y,y) = y. [para (6 (a 1) 5 (a 1))] given #6 (wt=6): 10 f(x,y,x) = x. [para (6 (a 2) 5 (a 1))] given #7 (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 (wt=12): 23 f(x,y,f(x,y,z)) = f(y,z,x). [para (10 (a 1) 7 (a 2 3))] given #9 (wt=12): 24 f(x,f(y,z,x),z) = f(y,z,x). [para (21 (a 1) 6 (a 1)) demod (6) flip a] given #10 (wt=12): 25 f(x,y,f(y,z,x)) = f(z,x,y). [para (6 (a 1) 21 (a 1 3))] given #11 (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) flip a] given #12 (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 (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 (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 (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 (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 (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 (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 11) flip a] given #19 (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 36 6 (R) 11 6 11)] given #20 (wt=12): 325 f(x,y,f(x,z,y)) = f(x,y,z). [back_demod 234 demod (295)] given #21 (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 (R))] given #22 (wt=9): 337 f(x,y,z) = f(z,y,x). [para (325 (a 1) 6 (a 1)) demod (6 46 328)] -------- Proof 1 -------- (0.12 + 0.01 seconds) 2b. -------- PROOF -------- Length of proof is 29. Maximum clause weight is 18. 3 f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [input] 4 f(A,B,C) != f(A,C,B) # answer(2b). [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 (R)) flip a] 8 f(A,C,B) != f(A,B,C) # answer(2b). [copy 4 flip a] 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) 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) 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 36 6 (R) 11 6 11)] 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 11 9 6 6 47 6 47)] 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)] 327 f(x,y,f(z,y,x)) = f(z,x,y). [back_demod 149 demod (325)] 328 f(x,y,f(y,x,z)) = f(z,x,y). [back_demod 300 demod (327)] 337 f(x,y,z) = f(z,y,x). [para (325 (a 1) 6 (a 1)) demod (6 46 328)] 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 ------- Given=22. Generated=1788. Kept=447. Proofs=1. Usable=19. Sos=358. Demods=101. Goals=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.40. User_CPU=0.12, System_CPU=0.01, Wall_clock=0. THEOREM PROVED Exiting with 1 proof. Process 14302 exit (max_proofs) Fri Jul 22 14:47:19 2005