============================== Prover9 =============================== Prover9 (64) version 2008-09A, September 2008. Process 7580 was started by veroff on rhea, Sun Nov 16 12:38:57 2008 The command was "prover9 -f d2com.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file d2com.in assign(order,kbo). set(lex_order_vars). set(para_units_only). % set(para_units_only) -> assign(para_lit_limit, 1). clear(back_demod). set(restrict_denials). formulas(assumptions). x + 0 = x. 0 + x = x. -x + (x + y) = y. (x + (y + x)) + z = x + (y + (x + z)). -(x + y) = -x + -y. (x * y) * z = x * (y * z). 1 * x = x. x * 1 = x. x != 0 -> x' * x = 1. x != 0 -> x * x' = 1. x != 0 -> x'' = x. x != 0 & y != 0 -> (x * y)' = y' * x'. 0 * x = 0. x * (y + z) = (x * y) + (x * z). 1 != 0. 1' = 1. -1 != 0. (-1)' = -1. -(x + y) + (x + (y + z)) = d(x,y) * z. d(x,y) = 1 # label("nearfield"). end_of_list. formulas(goals). x + y = y + x # label("commutativity of +"). end_of_list. formulas(hints). -x + x = 0. --x + y = x + y. -(x * y) + (x * (y + z)) = x * z. 0 = -0. -0 = 0. --x + 0 = x. x + 0 = --x. --x = x + 0. x + (-x + y) = y. x + -x = 0. x + -(x + y) = -y. (x + y) + (d(x,y) * z) = x + (y + z). -(x * y) + (x * y) = x * 0. -(x * y) + (x * 0) = x * -y. x * 0 = 0. x * -0 = 0. -(x * y) + 0 = x * -y. x * -y = -(x * y). -(x * y) = x * -y. -(0 * x) = 0. (x + y) + (1 * z) = x + (y + z). (x + y) + z = x + (y + z). 0 + (0 + x) = x. -(x * 0) = 0. 0 + (0 * x) = 0. 0 + (x * 0) = 0. (x + 0) + 0 = x. 0 + 0 = 0 * x. 0 * x = 0 + 0. 0 + 0 = x * 0. x * 0 = 0 + 0. x = x + (0 + 0). x + (0 + 0) = x. x + (0 * y) = x. x + (y * 0) = x. -x + x = y * 0. x * 0 = -y + y. x + (-y + y) = x. (x + -y) + y = x. -x + (y + x) = y. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x != 0 -> x' * x = 1 # label(non_clause). [assumption]. 2 x != 0 -> x * x' = 1 # label(non_clause). [assumption]. 3 x != 0 -> x'' = x # label(non_clause). [assumption]. 4 x != 0 & y != 0 -> (x * y)' = y' * x' # label(non_clause). [assumption]. 5 x + y = y + x # label("commutativity of +") # 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). x + 0 = x. [assumption]. 0 + x = x. [assumption]. -x + (x + y) = y. [assumption]. (x + (y + x)) + z = x + (y + (x + z)). [assumption]. -(x + y) = -x + -y. [assumption]. (x * y) * z = x * (y * z). [assumption]. 1 * x = x. [assumption]. x * 1 = x. [assumption]. 0 = x | x' * x = 1. [clausify(1)]. 0 = x | x * x' = 1. [clausify(2)]. 0 = x | x'' = x. [clausify(3)]. 0 = x | y = 0 | (x * y)' = y' * x'. [clausify(4)]. 0 * x = 0. [assumption]. x * (y + z) = (x * y) + (x * z). [assumption]. 1 != 0. [assumption]. 1' = 1. [assumption]. -1 != 0. [assumption]. (-1)' = -1. [assumption]. -(x + y) + (x + (y + z)) = d(x,y) * z. [assumption]. d(x,y) = 1 # label("nearfield"). [assumption]. c2 + c1 != c1 + c2 # label("commutativity of +"). [deny(5)]. end_of_list. formulas(demodulators). end_of_list. % 40 hints input. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (non-Horn, no changes). Term ordering decisions: Function symbol KB weights: 0=1. 1=1. c1=1. c2=1. +=1. *=1. d=1. '=1. -=1. Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ 0, 1, c1, c2, +, *, d, ', - ]). Skipping inverse_order, because term ordering is KBO. Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(unit_deletion). % (non-Horn) kept: 6 x + 0 = x. [assumption]. kept: 7 0 + x = x. [assumption]. kept: 8 -x + (x + y) = y. [assumption]. kept: 9 (x + (y + x)) + z = x + (y + (x + z)). [assumption]. 10 -(x + y) = -x + -y. [assumption]. kept: 11 -x + -y = -(x + y). [copy(10),flip(a)]. kept: 12 (x * y) * z = x * (y * z). [assumption]. kept: 13 1 * x = x. [assumption]. kept: 14 x * 1 = x. [assumption]. kept: 15 0 = x | x' * x = 1. [clausify(1)]. kept: 16 0 = x | x * x' = 1. [clausify(2)]. kept: 17 0 = x | x'' = x. [clausify(3)]. 18 0 = x | y = 0 | (x * y)' = y' * x'. [clausify(4)]. kept: 19 0 = x | 0 = y | y' * x' = (x * y)'. [copy(18),flip(b),flip(c)]. kept: 20 0 * x = 0. [assumption]. 21 x * (y + z) = (x * y) + (x * z). [assumption]. kept: 22 (x * y) + (x * z) = x * (y + z). [copy(21),flip(a)]. kept: 23 1 != 0. [assumption]. kept: 24 1' = 1. [assumption]. kept: 25 -1 != 0. [assumption]. kept: 26 (-1)' = -1. [assumption]. kept: 27 -(x + y) + (x + (y + z)) = d(x,y) * z. [assumption]. kept: 28 d(x,y) = 1 # label("nearfield"). [assumption]. kept: 29 c2 + c1 != c1 + c2 # label("commutativity of +"). [deny(5)]. kept: 30 0 = x | x' * x' = (x * x)'. [factor(19,a,b)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 23 1 != 0. [assumption]. 25 -1 != 0. [assumption]. 29 c2 + c1 != c1 + c2 # label("commutativity of +"). [deny(5)]. end_of_list. formulas(sos). 6 x + 0 = x. [assumption]. 7 0 + x = x. [assumption]. 8 -x + (x + y) = y. [assumption]. 9 (x + (y + x)) + z = x + (y + (x + z)). [assumption]. 11 -x + -y = -(x + y). [copy(10),flip(a)]. 12 (x * y) * z = x * (y * z). [assumption]. 13 1 * x = x. [assumption]. 14 x * 1 = x. [assumption]. 15 0 = x | x' * x = 1. [clausify(1)]. 16 0 = x | x * x' = 1. [clausify(2)]. 17 0 = x | x'' = x. [clausify(3)]. 19 0 = x | 0 = y | y' * x' = (x * y)'. [copy(18),flip(b),flip(c)]. 20 0 * x = 0. [assumption]. 22 (x * y) + (x * z) = x * (y + z). [copy(21),flip(a)]. 24 1' = 1. [assumption]. 26 (-1)' = -1. [assumption]. 27 -(x + y) + (x + (y + z)) = d(x,y) * z. [assumption]. 28 d(x,y) = 1 # label("nearfield"). [assumption]. 30 0 = x | x' * x' = (x * x)'. [factor(19,a,b)]. end_of_list. formulas(demodulators). end_of_list. % 40 hints processed (7 are redundant). ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=5): 6 x + 0 = x. [assumption]. given #2 (I,wt=5): 7 0 + x = x. [assumption]. given #3 (I,wt=8): 8 -x + (x + y) = y. [assumption]. given #4 (I,wt=15): 9 (x + (y + x)) + z = x + (y + (x + z)). [assumption]. given #5 (I,wt=10): 11 -x + -y = -(x + y). [copy(10),flip(a)]. given #6 (I,wt=11): 12 (x * y) * z = x * (y * z). [assumption]. given #7 (I,wt=5): 13 1 * x = x. [assumption]. given #8 (I,wt=5): 14 x * 1 = x. [assumption]. given #9 (I,wt=9): 15 0 = x | x' * x = 1. [clausify(1)]. given #10 (I,wt=9): 16 0 = x | x * x' = 1. [clausify(2)]. given #11 (I,wt=8): 17 0 = x | x'' = x. [clausify(3)]. given #12 (I,wt=16): 19 0 = x | 0 = y | y' * x' = (x * y)'. [copy(18),flip(b),flip(c)]. given #13 (I,wt=5): 20 0 * x = 0. [assumption]. given #14 (I,wt=13): 22 (x * y) + (x * z) = x * (y + z). [copy(21),flip(a)]. given #15 (I,wt=4): 24 1' = 1. [assumption]. given #16 (I,wt=6): 26 (-1)' = -1. [assumption]. given #17 (I,wt=16): 27 -(x + y) + (x + (y + z)) = d(x,y) * z. [assumption]. given #18 (I,wt=5): 28 d(x,y) = 1 # label("nearfield"). [assumption]. given #19 (I,wt=13): 30 0 = x | x' * x' = (x * x)'. [factor(19,a,b)]. given #20 (H,wt=6): 31 -x + x = 0. [para(6(a,1),8(a,1,2))]. given #21 (H,wt=4): 114 -0 = 0. [para(31(a,1),6(a,1)),flip(a)]. given #22 (H,wt=7): 115 --x + 0 = x. [para(31(a,1),8(a,1,2))]. given #23 (H,wt=7): 125 0 + (0 + x) = x. [para(114(a,1),8(a,1,1))]. given #24 (H,wt=9): 33 --x + y = x + y. [para(8(a,1),8(a,1,2))]. given #25 (H,wt=6): 163 x + -x = 0. [para(33(a,1),31(a,1))]. given #26 (H,wt=7): 145 --x = x + 0. [para(33(a,1),6(a,1)),flip(a)]. given #27 (H,wt=7): 184 (x + 0) + 0 = x. [para(145(a,1),115(a,1,1))]. given #28 (H,wt=8): 148 x + (-x + y) = y. [para(33(a,1),8(a,1))]. given #29 (H,wt=9): 204 x + -(x + y) = -y. [para(11(a,1),148(a,1,2))]. given #30 (H,wt=14): 69 -(x * y) + (x * (y + z)) = x * z. [para(22(a,1),8(a,1,2))]. given #31 (H,wt=12): 231 -(x * y) + (x * y) = x * 0. [para(6(a,1),69(a,1,2,2))]. given #32 (H,wt=5): 281 x * 0 = 0. [para(231(a,1),31(a,1))]. given #33 (H,wt=13): 260 -(x * y) + (x * 0) = x * -y. [para(163(a,1),69(a,1,2,2))]. given #34 (H,wt=6): 311 x * -0 = 0. [para(260(a,1),31(a,1))]. given #35 (H,wt=11): 317 -(x * y) + 0 = x * -y. [para(281(a,1),260(a,1,2))]. given #36 (H,wt=9): 329 -(x * y) = x * -y. [para(317(a,1),6(a,1)),flip(a)]. given #37 (H,wt=6): 362 -(0 * x) = 0. [para(20(a,1),329(a,2))]. given #38 (H,wt=6): 374 -(x * 0) = 0. [para(311(a,1),329(a,2))]. given #39 (H,wt=7): 380 0 + (0 * x) = 0. [para(362(a,1),31(a,1,1))]. given #40 (H,wt=7): 398 0 + (x * 0) = 0. [para(374(a,1),31(a,1,1))]. given #41 (H,wt=7): 417 0 * x = 0 + 0. [para(380(a,1),125(a,1,2)),flip(a)]. given #42 (H,wt=7): 428 x * 0 = 0 + 0. [para(398(a,1),125(a,1,2)),flip(a)]. given #43 (H,wt=15): 209 (x + y) + (d(x,y) * z) = x + (y + z). [para(27(a,1),148(a,1,2))]. given #44 (H,wt=13): 517 (x + y) + (1 * z) = x + (y + z). [para(28(a,1),209(a,1,2,1))]. given #45 (H,wt=11): 578 (x + y) + z = x + (y + z). [para(13(a,1),517(a,1,2))]. given #46 (H,wt=7): 677 x + (0 + 0) = x. [para(578(a,1),184(a,1))]. given #47 (H,wt=7): 728 x + (0 * y) = x. [para(417(a,2),677(a,1,2))]. given #48 (H,wt=7): 729 x + (y * 0) = x. [para(428(a,2),677(a,1,2))]. given #49 (H,wt=8): 755 x * 0 = -y + y. [para(729(a,1),8(a,1,2)),flip(a)]. given #50 (H,wt=8): 811 x + (-y + y) = x. [para(755(a,1),728(a,1,2))]. given #51 (H,wt=8): 842 (x + -y) + y = x. [para(811(a,1),578(a,2))]. given #52 (H,wt=8): 860 -x + (y + x) = y. [para(204(a,1),842(a,1,1))]. % Operation + is commutative; C redundancy checks enabled. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.04 (+ 0.00) seconds. % Length of proof is 47. % Level of proof is 16. % Maximum clause weight is 16. % Given clauses 52. 5 x + y = y + x # label("commutativity of +") # label(non_clause) # label(goal). [goal]. 6 x + 0 = x. [assumption]. 8 -x + (x + y) = y. [assumption]. 10 -(x + y) = -x + -y. [assumption]. 11 -x + -y = -(x + y). [copy(10),flip(a)]. 13 1 * x = x. [assumption]. 20 0 * x = 0. [assumption]. 21 x * (y + z) = (x * y) + (x * z). [assumption]. 22 (x * y) + (x * z) = x * (y + z). [copy(21),flip(a)]. 27 -(x + y) + (x + (y + z)) = d(x,y) * z. [assumption]. 28 d(x,y) = 1 # label("nearfield"). [assumption]. 29 c2 + c1 != c1 + c2 # label("commutativity of +"). [deny(5)]. 31 -x + x = 0. [para(6(a,1),8(a,1,2))]. 33 --x + y = x + y. [para(8(a,1),8(a,1,2))]. 69 -(x * y) + (x * (y + z)) = x * z. [para(22(a,1),8(a,1,2))]. 114 -0 = 0. [para(31(a,1),6(a,1)),flip(a)]. 115 --x + 0 = x. [para(31(a,1),8(a,1,2))]. 125 0 + (0 + x) = x. [para(114(a,1),8(a,1,1))]. 145 --x = x + 0. [para(33(a,1),6(a,1)),flip(a)]. 148 x + (-x + y) = y. [para(33(a,1),8(a,1))]. 163 x + -x = 0. [para(33(a,1),31(a,1))]. 184 (x + 0) + 0 = x. [para(145(a,1),115(a,1,1))]. 204 x + -(x + y) = -y. [para(11(a,1),148(a,1,2))]. 209 (x + y) + (d(x,y) * z) = x + (y + z). [para(27(a,1),148(a,1,2))]. 231 -(x * y) + (x * y) = x * 0. [para(6(a,1),69(a,1,2,2))]. 260 -(x * y) + (x * 0) = x * -y. [para(163(a,1),69(a,1,2,2))]. 281 x * 0 = 0. [para(231(a,1),31(a,1))]. 311 x * -0 = 0. [para(260(a,1),31(a,1))]. 317 -(x * y) + 0 = x * -y. [para(281(a,1),260(a,1,2))]. 329 -(x * y) = x * -y. [para(317(a,1),6(a,1)),flip(a)]. 362 -(0 * x) = 0. [para(20(a,1),329(a,2))]. 374 -(x * 0) = 0. [para(311(a,1),329(a,2))]. 380 0 + (0 * x) = 0. [para(362(a,1),31(a,1,1))]. 398 0 + (x * 0) = 0. [para(374(a,1),31(a,1,1))]. 417 0 * x = 0 + 0. [para(380(a,1),125(a,1,2)),flip(a)]. 428 x * 0 = 0 + 0. [para(398(a,1),125(a,1,2)),flip(a)]. 517 (x + y) + (1 * z) = x + (y + z). [para(28(a,1),209(a,1,2,1))]. 578 (x + y) + z = x + (y + z). [para(13(a,1),517(a,1,2))]. 677 x + (0 + 0) = x. [para(578(a,1),184(a,1))]. 728 x + (0 * y) = x. [para(417(a,2),677(a,1,2))]. 729 x + (y * 0) = x. [para(428(a,2),677(a,1,2))]. 755 x * 0 = -y + y. [para(729(a,1),8(a,1,2)),flip(a)]. 811 x + (-y + y) = x. [para(755(a,1),728(a,1,2))]. 842 (x + -y) + y = x. [para(811(a,1),578(a,2))]. 860 -x + (y + x) = y. [para(204(a,1),842(a,1,1))]. 893 x + y = y + x. [para(860(a,1),148(a,1,2))]. 894 $F. [resolve(893,a,29,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=52. Generated=1198. Kept=885. proofs=1. Usable=52. Sos=738. Demods=0. Limbo=17, Disabled=98. Hints=40. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=313. Back_subsumed=77. 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=3. Nonunit_bsub_feature_tests=9. Megabytes=1.10. User_CPU=0.04, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 1 proof. ------ process 7580 exit (max_proofs) ------  Process 7580 exit (max_proofs) Sun Nov 16 12:38:57 2008