----- Prover9 July-2005D, 18 July 2005 ----- Process 14909 was started by mccune on theorem.mcs.anl.gov, Fri Jul 22 15:34:02 2005 The command was "prover9 -f dist-short-long.in". % Reading from file dist-short-long.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). set(lex_order_vars). clauses(sos). f(x,x,y) = x # label(majority). f(x,y,z) = f(z,x,y) # label(2a). f(x,y,z) = f(x,z,y) # label(2b). f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). f(f(x,y,z),u,v) = f(x,f(y,u,v),f(z,u,v)) # label(dist_short). f(f(A,B,C),D,E) != f(f(A,D,E),f(B,D,E),f(C,D,E)) # answer(dist_long). end_of_list. % Finished reading the input. % Entering prover search function. % Assigned IDs to 6 clauses. % Predicate elimination: (none). % Function symbol KB weights: A=1. B=1. C=1. D=1. E=1. f=1. % Relation symbol precedence: lex([ = ]). % Function symbol precedence: lex([ A, B, C, D, E, 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). 7 f(x,x,y) = x # label(majority). [input] 8 f(x,y,z) = f(z,x,y) # label(2a). [input] 9 f(x,y,z) = f(x,z,y) # label(2b). [input] 10 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)) # label(associativity). [copy 4 demod (8 8 8 (R) 9)] 11 f(x,f(y,z,u),f(v,z,u)) = f(z,u,f(x,y,v)) # label(dist_short). [copy 5 demod (8 8) flip a] 12 f(D,E,f(B,C,f(A,D,E))) != f(D,E,f(A,B,C)) # answer(dist_long). [copy 6 demod (8 8 11 8 8) flip a] end_of_list. clauses(demodulators). 7 f(x,x,y) = x # label(majority). [input] 8 f(x,y,z) = f(z,x,y) # label(2a). [input] % (lex-dep) 9 f(x,y,z) = f(x,z,y) # label(2b). [input] % (lex-dep) 11 f(x,f(y,z,u),f(v,z,u)) = f(z,u,f(x,y,v)) # label(dist_short). [copy 5 demod (8 8) flip a] end_of_list. clauses(goals). end_of_list. % Starting search at 0.00 seconds. given #1 (wt=6): 7 f(x,x,y) = x # label(majority). [input] given #2 (wt=9): 8 f(x,y,z) = f(z,x,y) # label(2a). [input] given #3 (wt=9): 9 f(x,y,z) = f(x,z,y) # label(2b). [input] given #4 (wt=15): 10 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)) # label(associativity). [copy 4 demod (8 8 8 (R) 9)] given #5 (wt=18): 11 f(x,f(y,z,u),f(v,z,u)) = f(z,u,f(x,y,v)) # label(dist_short). [copy 5 demod (8 8) flip a] given #6 (wt=18): 12 f(D,E,f(B,C,f(A,D,E))) != f(D,E,f(A,B,C)) # answer(dist_long). [copy 6 demod (8 8 11 8 8) flip a] given #7 (wt=6): 13 f(x,y,y) = y. [para (8 (a 1) 7 (a 1))] given #8 (wt=12): 20 f(x,y,f(x,z,y)) = f(x,z,y). [para (10 (a 2) 10 (a 1)) demod (8 (R) 13 8 9) flip a] given #9 (wt=12): 44 f(x,y,f(x,y,z)) = f(x,y,z). [para (13 (a 1) 10 (a 2 3)) demod (8 8 8 8)] given #10 (wt=15): 14 f(x,y,f(x,z,u)) = f(x,z,f(x,y,u)). [para (10 (a 2) 8 (a 1)) demod (8 (R) 9 9 8 9)] given #11 (wt=15): 15 f(x,y,f(z,y,u)) = f(z,y,f(x,y,u)). [para (10 (a 1) 8 (a 2)) demod (9 8)] given #12 (wt=15): 16 f(x,y,f(x,z,u)) = f(x,u,f(x,z,y)). [para (10 (a 2) 8 (a 2)) demod (9 8 8)] given #13 (wt=15): 17 f(x,y,f(x,z,u)) = f(x,u,f(x,y,z)). [para (8 (a 1) 10 (a 1 3)) demod (8 9 8 (R) 9)] given #14 (wt=15): 23 f(x,y,f(z,u,f(x,y,z))) = f(x,y,z). [para (11 (a 1) 7 (a 1)) demod (8 8 8 8 8 8)] given #15 (wt=12): 98 f(x,y,f(z,x,y)) = f(z,x,y). [para (23 (a 1) 15 (a 1)) demod (44 8 (R) 9) flip a] given #16 (wt=21): 18 f(x,y,f(z,u,f(x,u,v))) = f(x,u,f(x,y,f(z,u,v))). [para (10 (a 1) 10 (a 1 3)) demod (8 9 8 (R) 9)] given #17 (wt=15): 24 f(x,y,f(z,u,x)) = f(z,x,f(u,x,y)). [para (7 (a 1) 11 (a 1 3)) demod (9) flip a] given #18 (wt=15): 46 f(x,y,f(z,x,u)) = f(z,x,f(x,y,u)). [back_demod 36 demod (44) flip a] given #19 (wt=15): 52 f(x,y,f(z,u,f(x,z,y))) = f(x,z,y). [back_demod 33 demod (8 8 48 7 8 20 8 8 (R) 9) flip a] given #20 (wt=15): 58 f(x,y,f(x,z,f(y,u,z))) = f(x,y,z). [para (14 (a 1) 11 (a 1)) demod (8 (R) 9 9 8 7 8)] given #21 (wt=21): 19 f(x,y,f(x,z,f(x,u,v))) = f(x,u,f(x,y,f(x,z,v))). [para (10 (a 2) 10 (a 1 3)) demod (8 (R) 9 9 9 8 (R) 9)] given #22 (wt=15): 60 f(x,y,f(z,y,f(x,z,u))) = f(x,z,y). [para (11 (a 1) 14 (a 1)) demod (8 7 8 8 8 8 (R) 9) flip a] given #23 (wt=15): 78 f(x,y,f(x,z,f(y,z,u))) = f(x,y,z). [para (16 (a 1) 11 (a 1)) demod (8 9 8 7 8 9)] given #24 (wt=15): 80 f(x,y,f(z,y,f(z,x,u))) = f(z,x,y). [para (11 (a 1) 16 (a 1)) demod (8 7 8 8 8 (R) 9 8 (R) 9) flip a] given #25 (wt=15): 88 f(x,y,f(z,u,f(z,x,y))) = f(z,x,y). [para (8 (a 1) 23 (a 1)) demod (8 8 8 8)] given #26 (wt=21): 22 f(x,f(y,z,u),f(x,y,v)) = f(x,v,f(y,u,f(x,y,z))). [para (10 (a 2) 10 (a 2 3)) demod (8 8 8 (R) 9)] given #27 (wt=15): 89 f(x,y,f(z,u,f(x,y,u))) = f(x,y,u). [para (8 (a 2) 23 (a 1 3)) demod (9)] given #28 (wt=15): 96 f(x,y,f(y,z,f(x,z,u))) = f(x,y,z). [para (11 (a 1) 23 (a 1 3)) demod (8)] given #29 (wt=15): 99 f(x,y,f(z,x,u)) = f(x,u,f(z,x,y)). [para (15 (a 1) 23 (a 2)) demod (8 (R) 9 8 (R) 9 8 (R) 9 49 8 8 93 8 (R) 9)] given #30 (wt=15): 111 f(x,y,f(z,x,f(z,y,u))) = f(z,x,y). [para (18 (a 1) 10 (a 2)) demod (8 (R) 9 29 7 8 8 (R) 9) flip a] given #31 (wt=18): 26 f(x,f(y,z,u),f(y,z,v)) = f(y,z,f(x,u,v)). [para (11 (a 1) 8 (a 1)) demod (8 8 8 8 8 (R)) flip a] -------- Proof 1 -------- (0.34 + 0.00 seconds) dist_long. -------- PROOF -------- Length of proof is 18. Maximum clause weight is 18. 4 f(f(x,y,z),y,u) = f(x,y,f(z,y,u)) # label(associativity). [input] 5 f(f(x,y,z),u,v) = f(x,f(y,u,v),f(z,u,v)) # label(dist_short). [input] 6 f(f(A,B,C),D,E) != f(f(A,D,E),f(B,D,E),f(C,D,E)) # answer(dist_long). [input] 7 f(x,x,y) = x # label(majority). [input] 8 f(x,y,z) = f(z,x,y) # label(2a). [input] 9 f(x,y,z) = f(x,z,y) # label(2b). [input] 10 f(x,y,f(z,x,u)) = f(z,x,f(x,u,y)) # label(associativity). [copy 4 demod (8 8 8 (R) 9)] 11 f(x,f(y,z,u),f(v,z,u)) = f(z,u,f(x,y,v)) # label(dist_short). [copy 5 demod (8 8) flip a] 12 f(D,E,f(B,C,f(A,D,E))) != f(D,E,f(A,B,C)) # answer(dist_long). [copy 6 demod (8 8 11 8 8) flip a] 13 f(x,y,y) = y. [para (8 (a 1) 7 (a 1))] 15 f(x,y,f(z,y,u)) = f(z,y,f(x,y,u)). [para (10 (a 1) 8 (a 2)) demod (9 8)] 23 f(x,y,f(z,u,f(x,y,z))) = f(x,y,z). [para (11 (a 1) 7 (a 1)) demod (8 8 8 8 8 8)] 26 f(x,f(y,z,u),f(y,z,v)) = f(y,z,f(x,u,v)). [para (11 (a 1) 8 (a 1)) demod (8 8 8 8 8 (R)) flip a] 27 f(x,f(y,z,u),f(z,u,v)) = f(z,u,f(y,v,x)). [para (11 (a 1) 8 (a 2)) demod (8 8 8 8 8)] 44 f(x,y,f(x,y,z)) = f(x,y,z). [para (13 (a 1) 10 (a 2 3)) demod (8 8 8 8)] 98 f(x,y,f(z,x,y)) = f(z,x,y). [para (23 (a 1) 15 (a 1)) demod (44 8 (R) 9) flip a] 485 f(x,y,f(z,u,f(v,x,y))) = f(x,y,f(z,v,u)). [para (98 (a 1) 26 (a 1 2)) demod (27 8 9) flip a] 508 $F # answer(dist_long). [back_demod 12 demod (485 8 (R) 9) xx a] -------- end of proof ------- Given=31. Generated=4243. Kept=501. Proofs=1. Usable=25. Sos=367. Demods=236. Goals=0. Limbo=23, Disabled=92. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=3741. Back_subsumed=5. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=298 (2 lex), Back_demodulated=81. Back_unit_deleted=0. Demod_attempts=47121. Demod_rewrites=19426. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.53. User_CPU=0.34, System_CPU=0.00, Wall_clock=0. THEOREM PROVED Exiting with 1 proof. Process 14909 exit (max_proofs) Fri Jul 22 15:34:02 2005