============================== Prover9 =============================== Prover9 (64) version 2009-02A, February 2009. Process 30566 was started by veroff on proof, Mon Feb 27 14:20:17 2012 The command was "prover9 -f thm3_final.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file thm3_final.in clear(auto). % clear(auto) -> clear(auto_inference). % clear(auto) -> clear(auto_setup). % clear(auto_setup) -> clear(predicate_elim). % clear(auto_setup) -> assign(eq_defs, pass). % clear(auto) -> clear(auto_limits). % clear(auto_limits) -> assign(max_weight, "1000000000000.000"). % clear(auto_limits) -> assign(sos_limit, -1). % clear(auto) -> clear(auto_denials). % clear(auto) -> clear(auto_process). assign(order,kbo). set(lex_order_vars). set(paramodulation). set(hyper_resolution). % set(hyper_resolution) -> set(pos_hyper_resolution). clear(back_demod). set(para_from_small). set(para_units_only). % set(para_units_only) -> assign(para_lit_limit, 1). formulas(assumptions). x * (y * x) = y. x * y = y * x. e * e = e. x + e = x. e + y = y. (x + y) * z != (x + u) * w | (v5 + y) * z = (v5 + u) * w # label("gL"). (a * b) * e != a + b | a + (a * e) != e | a + b != b + a | a + (b + c) != (a + b) + c. end_of_list. formulas(hints). x + (x * e) = e. x * (y * x) = y. x * y = y * x. e * e = e. x + e = x. e + x = x. c6 + (c6 * e) != e. c6 + (e * c6) != e. x * (x * y) = y. x = (y * x) * y. x = (x * y) * y. x = y * (x * y). (x + y) * (z + u) = (x + u) * (z + y). x * (y + z) = (x + z) * (y + e). x * (y + z) = (x + z) * y. x * (y + z) = y * (x + z). x * (y + z) = (e + z) * (y + x). x * (y + z) = z * (y + x). x * (y + z) = y * (z + x). x * (y + z) = z * (x + y). (x + y) * z = (x + z) * (e + y). z * (x + y) = (x + z) * (e + y). x * (z + y) = (x + z) * (e + y). x * (z + y) = (x + z) * y. x * (z + y) = y * (x + z). x * (y + z) = x * (z + y). x * (y * (x + z)) = z + y. x * (x * (z + y)) = z + y. x * (x * (y + z)) = z + y. x + y = y + x. (x + y) * (y * (z + x)) = z. (x + y) * (y * (x + z)) = z. (x + y) * (x * (z + y)) = z. (x + y) * (x * (y + z)) = z. (x + y) * (x * y) = e. (x * y) * (x + y) = e. y * ((x * y) + x) = e. y * (x + (x * y)) = e. x * ((x * y) + y) = e. x * (y + (x * y)) = e. x * e = y + (x * y). x + (y * x) = y * e. e * e != e. e != e. x + y = (x * y) * e. x + (x * y) = y * e. x + y = e * (x * y). e * (x * y) = x + y. x + (y + z) = (x + y) + z. (x + y) + z = (x * (y + z)) * e. z + (x + y) = (x * (y + z)) * e. z + (x + y) = e * (x * (y + z)). z + (x + y) = x + (y + z). x + (y + z) = z + (x + y). end_of_list. formulas(hints). x6 + (x6 * e) = e. x6 + (e * x6) = e. (x1 * x2) * e = x1 + x2. e * (x1 * x2) = x1 + x2. (x3 + x4) + x5 = x3 + (x4 + x5). x5 + (x3 + x4) = x3 + (x4 + x5). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x * (y * x) = y. [assumption]. x * y = y * x. [assumption]. e * e = e. [assumption]. x + e = x. [assumption]. e + x = x. [assumption]. (x + y) * z != (x + u) * w | (v5 + y) * z = (v5 + u) * w # label("gL"). [assumption]. (a * b) * e != a + b | a + (a * e) != e | a + b != b + a | a + (b + c) != (a + b) + c. [assumption]. end_of_list. formulas(demodulators). end_of_list. % 60 hints input. Term ordering decisions: Function symbol KB weights: e=1. a=1. b=1. c=1. *=1. +=1. Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ e, a, b, c, *, + ]). Skipping inverse_order, because term ordering is KBO. kept: 1 x * (y * x) = y. [assumption]. % Operation * is commutative; C redundancy checks enabled. kept: 2 x * y = y * x. [assumption]. kept: 3 e * e = e. [assumption]. kept: 4 x + e = x. [assumption]. kept: 5 e + x = x. [assumption]. kept: 6 (x + y) * z != (x + u) * w | (v5 + y) * z = (v5 + u) * w # label("gL"). [assumption]. 7 (a * b) * e != a + b | a + (a * e) != e | a + b != b + a | a + (b + c) != (a + b) + c. [assumption]. kept: 8 (a * b) * e != a + b | a + (a * e) != e | b + a != a + b | (a + b) + c != a + (b + c). [copy(7),flip(c),flip(d)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 x * (y * x) = y. [assumption]. 2 x * y = y * x. [assumption]. 3 e * e = e. [assumption]. 4 x + e = x. [assumption]. 5 e + x = x. [assumption]. 6 (x + y) * z != (x + u) * w | (v5 + y) * z = (v5 + u) * w # label("gL"). [assumption]. 8 (a * b) * e != a + b | a + (a * e) != e | b + a != a + b | (a + b) + c != a + (b + c). [copy(7),flip(c),flip(d)]. end_of_list. formulas(demodulators). end_of_list. % 49 hints (60 processed, 11 redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 1 x * (y * x) = y. [assumption]. given #2 (I,wt=7): 2 x * y = y * x. [assumption]. given #3 (I,wt=5): 3 e * e = e. [assumption]. given #4 (I,wt=5): 4 x + e = x. [assumption]. given #5 (I,wt=5): 5 e + x = x. [assumption]. given #6 (I,wt=22): 6 (x + y) * z != (x + u) * w | (v5 + y) * z = (v5 + u) * w # label("gL"). [assumption]. given #7 (I,wt=34): 8 (a * b) * e != a + b | a + (a * e) != e | b + a != a + b | (a + b) + c != a + (b + c). [copy(7),flip(c),flip(d)]. given #8 (H,wt=7): 9 (x * y) * x = y. [para(1(a,1),1(a,1,2))]. given #9 (H,wt=7): 12 x * (x * y) = y. [para(2(a,1),1(a,1,2))]. given #10 (H,wt=7): 13 (x * y) * y = x. [para(2(a,1),1(a,1))]. given #11 (H,wt=15): 35 (x + y) * (z + u) = (x + u) * (z + y). [hyper(6,a,2,a)]. given #12 (H,wt=13): 99 (x + y) * (z + e) = x * (z + y). [para(4(a,1),35(a,1,1)),flip(a)]. given #13 (H,wt=11): 125 (x + y) * z = x * (z + y). [para(4(a,1),99(a,1,2))]. given #14 (H,wt=11): 163 x * (y + z) = y * (x + z). [para(125(a,1),2(a,1))]. given #15 (H,wt=11): 178 (x + y) * (x * (z + y)) = z. [para(125(a,1),12(a,1,2))]. given #16 (H,wt=9): 224 (x + y) * (x * y) = e. [para(5(a,1),178(a,1,2,2))]. given #17 (H,wt=9): 267 (x * y) * e = x + y. [para(224(a,1),1(a,1,2))]. given #18 (H,wt=9): 271 (x * y) * (x + y) = e. [para(224(a,1),2(a,1)),flip(a)]. given #19 (H,wt=9): 288 e * (x * y) = x + y. [para(224(a,1),13(a,1,1))]. given #20 (H,wt=9): 296 x * ((x * y) + y) = e. [para(224(a,1),125(a,1)),flip(a)]. given #21 (H,wt=9): 305 x + (y * x) = y * e. [para(1(a,1),267(a,1,1)),flip(a)]. given #22 (H,wt=7): 468 x + (e * x) = e. [para(305(a,2),3(a,1))]. given #23 (H,wt=7): 521 x + (x * e) = e. [para(2(a,1),468(a,1,2))]. given #24 (H,wt=9): 316 x + (x * y) = y * e. [para(12(a,1),267(a,1,1)),flip(a)]. given #25 (H,wt=9): 345 x * (y + (x * y)) = e. [para(1(a,1),271(a,1,1))]. given #26 (H,wt=9): 357 x * ((y * x) + y) = e. [para(9(a,1),271(a,1,1))]. given #27 (H,wt=9): 360 x * (y + (y * x)) = e. [para(12(a,1),271(a,1,1))]. given #28 (H,wt=13): 103 (e + x) * (y + z) = z * (y + x). [para(5(a,1),35(a,1,1)),flip(a)]. given #29 (H,wt=11): 815 x * (y + z) = z * (y + x). [para(5(a,1),103(a,1,1))]. given #30 (H,wt=11): 908 (x + y) * (y * (x + z)) = z. [para(815(a,1),1(a,1,2))]. given #31 (H,wt=11): 927 x * (y + z) = z * (x + y). [para(815(a,1),163(a,1)),flip(a)]. given #32 (H,wt=11): 928 (x + y) * (y * (z + x)) = z. [para(815(a,1),178(a,1,2))]. given #33 (H,wt=11): 1008 (x + y) * (x * (y + z)) = z. [para(163(a,1),908(a,1,2))]. given #34 (H,wt=11): 1098 (x + y) * z = x * (y + z). [para(927(a,2),2(a,1)),flip(a)]. given #35 (H,wt=11): 1109 x * (y * (x + z)) = z + y. [para(927(a,1),12(a,1,2))]. % Operation + is commutative; C redundancy checks enabled. % back CAC tautology: 1127 x * (y + z) = x * (z + y). [para(927(a,2),163(a,1))]. % back CAC tautology: 1126 (x + y) * z = z * (y + x). [para(927(a,2),125(a,2))]. given #36 (H,wt=7): 1581 x + y = y + x. [para(1109(a,1),12(a,1))]. given #37 (H,wt=11): 1601 x * (x * (y + z)) = z + y. [para(163(a,1),1109(a,1,2))]. given #38 (H,wt=13): 104 (x + y) * (e + z) = (x + z) * y. [para(5(a,1),35(a,1,2)),flip(a)]. given #39 (H,wt=13): 807 (x + y) * (e + z) = y * (x + z). [para(103(a,1),2(a,1)),flip(a)]. given #40 (H,wt=13): 1134 (x * (y + z)) * e = z + (x + y). [para(927(a,2),267(a,1,1))]. given #41 (H,wt=11): 2032 x + (y + z) = z + (x + y). [para(1134(a,1),267(a,1)),flip(a)]. % Operation + is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 2032 x + (y + z) = z + (x + y). [para(1134(a,1),267(a,1)),flip(a)]. % back CAC tautology: 2208 (x + y) + z = y + (z + x). [para(2032(a,1),1581(a,1)),flip(a)]. given #42 (H,wt=11): 2209 (x + y) + z = x + (y + z). [para(2032(a,2),1581(a,1)),flip(a)]. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.06 (+ 0.00) seconds. % Length of proof is 28. % Level of proof is 10. % Maximum clause weight is 34. % Given clauses 42. 1 x * (y * x) = y. [assumption]. 2 x * y = y * x. [assumption]. 3 e * e = e. [assumption]. 4 x + e = x. [assumption]. 5 e + x = x. [assumption]. 6 (x + y) * z != (x + u) * w | (v5 + y) * z = (v5 + u) * w # label("gL"). [assumption]. 7 (a * b) * e != a + b | a + (a * e) != e | a + b != b + a | a + (b + c) != (a + b) + c. [assumption]. 8 (a * b) * e != a + b | a + (a * e) != e | b + a != a + b | (a + b) + c != a + (b + c). [copy(7),flip(c),flip(d)]. 12 x * (x * y) = y. [para(2(a,1),1(a,1,2))]. 35 (x + y) * (z + u) = (x + u) * (z + y). [hyper(6,a,2,a)]. 99 (x + y) * (z + e) = x * (z + y). [para(4(a,1),35(a,1,1)),flip(a)]. 103 (e + x) * (y + z) = z * (y + x). [para(5(a,1),35(a,1,1)),flip(a)]. 125 (x + y) * z = x * (z + y). [para(4(a,1),99(a,1,2))]. 163 x * (y + z) = y * (x + z). [para(125(a,1),2(a,1))]. 178 (x + y) * (x * (z + y)) = z. [para(125(a,1),12(a,1,2))]. 224 (x + y) * (x * y) = e. [para(5(a,1),178(a,1,2,2))]. 267 (x * y) * e = x + y. [para(224(a,1),1(a,1,2))]. 305 x + (y * x) = y * e. [para(1(a,1),267(a,1,1)),flip(a)]. 468 x + (e * x) = e. [para(305(a,2),3(a,1))]. 521 x + (x * e) = e. [para(2(a,1),468(a,1,2))]. 815 x * (y + z) = z * (y + x). [para(5(a,1),103(a,1,1))]. 927 x * (y + z) = z * (x + y). [para(815(a,1),163(a,1)),flip(a)]. 1109 x * (y * (x + z)) = z + y. [para(927(a,1),12(a,1,2))]. 1134 (x * (y + z)) * e = z + (x + y). [para(927(a,2),267(a,1,1))]. 1581 x + y = y + x. [para(1109(a,1),12(a,1))]. 2032 x + (y + z) = z + (x + y). [para(1134(a,1),267(a,1)),flip(a)]. 2209 (x + y) + z = x + (y + z). [para(2032(a,2),1581(a,1)),flip(a)]. 2235 $F. [hyper(8,a,267,a,b,521,a,c,1581,a,d,2209,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=42. Generated=3445. Kept=2233. proofs=1. Usable=41. Sos=2178. Demods=0. Limbo=0, Disabled=21. Hints=60. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=1211. Back_subsumed=10. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=16. Megabytes=2.32. User_CPU=0.06, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 1 proof. ------ process 30566 exit (max_proofs) ------  Process 30566 exit (max_proofs) Mon Feb 27 14:20:17 2012