============================== Prover9 =============================== Prover9 (64) version 2008-09A, September 2008. Process 7570 was started by veroff on rhea, Sun Nov 16 12:38:51 2008 The command was "prover9 -f com2d.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file com2d.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. x + y = y + x. end_of_list. formulas(goals). d(x,y) = 1 # label("nearfield"). end_of_list. formulas(hints). -x + x = 0. --x + y = x + y. -(x * y) + (x * (y + z)) = x * z. --(x + y) + (-x + (-y + z)) = d(-x,-y) * z. -(x + y) + (y + (x + z)) = d(y,x) * z. 0 = x + -x. x + -x = 0. -(x + y) + (x + 0) = d(x,y) * -y. d(x,y) * -y = -(x + y) + (x + 0). x + 0 = --x. --x = x + 0. x + (-x + y) = y. --x = x. x + -(x + y) = -y. (x + y) + (d(x,y) * z) = x + (y + z). x + (y + -x) = y. -(x * y) + (x * y) = x * 0. -(x * y) + (x * 0) = x * -y. x * 0 = 0. -(x * y) + 0 = x * -y. x * -y = -(x * y). -(x * y) = x * -y. d(x,y) * -y = -(x + y) + x. d(x,y) * -y = x + -(x + y). d(x,y) * -y = -y. --x = d(y,x) * --x. d(x,y) * --y = --y. d(x,y) * --y = y. d(x,y) * y = y. 1 = d(x,1). d(x,1) = 1. (x + y) + (d(y,x) * z) = y + (x + z). (x + 1) + (1 * y) = x + (1 + y). (x + 1) + y = x + (1 + y). x + (1 + y) = y + (x + 1). x + (y + 1) = y + (x + 1). -(x + y) + (y + (x + 1)) = d(y,x). -(x + y) + (x + (y + 1)) = d(y,x). d(x,y) = d(y,x) * 1. d(x,y) * 1 = d(y,x). d(x,y) = d(y,x). (x + y) + (d(x,y) * z) = y + (x + z). x + (y + z) = y + (x + z). d(-x,-y) * z = (x + y) + (-x + (-y + z)). (x + y) + (-x + (-y + z)) = d(-x,-y) * z. (x + y) + (-x + (z + -y)) = d(-x,-y) * z. (-x + y) + (x + (z + -y)) = d(--x,-y) * z. (x + -y) + (y + (z + -x)) = d(--y,-x) * z. (x + -y) + (y + (z + -x)) = d(y,-x) * z. d(x,-y) * z = x + ((y + -x) + (z + -y)). x + ((y + -x) + (z + -y)) = d(x,-y) * z. x + (y + ((z + -x) + -z)) = d(x,-z) * y. x + (y + (-z + (z + -x))) = d(x,-z) * y. x + (y + -x) = d(x,-z) * y. d(x,-y) * z = x + (z + -x). d(x,-y) * z = z. d(x,y) * z = z. 1 = d(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 d(x,y) = 1 # label("nearfield") # 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]. x + y = y + x. [assumption]. d(c1,c2) != 1 # label("nearfield"). [deny(5)]. end_of_list. formulas(demodulators). end_of_list. % 58 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]. % Operation + is commutative; C redundancy checks enabled. kept: 28 x + y = y + x. [assumption]. kept: 29 d(c1,c2) != 1 # label("nearfield"). [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 d(c1,c2) != 1 # label("nearfield"). [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 x + y = y + x. [assumption]. 30 0 = x | x' * x' = (x * x)'. [factor(19,a,b)]. end_of_list. formulas(demodulators). end_of_list. % 58 hints processed (10 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=7): 28 x + y = y + x. [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=6): 138 x + -x = 0. [para(31(a,1),28(a,1)),flip(a)]. given #22 (H,wt=9): 33 --x + y = x + y. [para(8(a,1),8(a,1,2))]. given #23 (H,wt=7): 147 --x = x + 0. [para(33(a,1),6(a,1)),flip(a)]. given #24 (H,wt=5): 170 --x = x. [para(6(a,1),147(a,2))]. given #25 (H,wt=8): 150 x + (-x + y) = y. [para(33(a,1),8(a,1))]. given #26 (H,wt=8): 194 x + (y + -x) = y. [para(28(a,1),150(a,1,2))]. given #27 (H,wt=9): 187 x + -(x + y) = -y. [para(11(a,1),150(a,1,2))]. given #28 (H,wt=14): 69 -(x * y) + (x * (y + z)) = x * z. [para(22(a,1),8(a,1,2))]. given #29 (H,wt=12): 234 -(x * y) + (x * y) = x * 0. [para(6(a,1),69(a,1,2,2))]. given #30 (H,wt=5): 285 x * 0 = 0. [para(234(a,1),31(a,1))]. given #31 (H,wt=13): 261 -(x * y) + (x * 0) = x * -y. [para(138(a,1),69(a,1,2,2))]. given #32 (H,wt=11): 322 -(x * y) + 0 = x * -y. [para(285(a,1),261(a,1,2))]. given #33 (H,wt=9): 323 -(x * y) = x * -y. [para(322(a,1),6(a,1)),flip(a)]. given #34 (H,wt=15): 146 d(x,y) * -y = -(x + y) + (x + 0). [para(138(a,1),27(a,1,2,2)),flip(a)]. given #35 (H,wt=13): 369 d(x,y) * -y = -(x + y) + x. [para(6(a,1),146(a,2,2))]. given #36 (H,wt=13): 446 d(x,y) * -y = x + -(x + y). [para(369(a,2),28(a,1))]. given #37 (H,wt=9): 514 d(x,y) * -y = -y. [para(446(a,2),187(a,1))]. given #38 (H,wt=11): 555 d(x,y) * --y = --y. [para(514(a,1),323(a,1,1)),flip(a)]. given #39 (H,wt=9): 572 d(x,y) * --y = y. [para(170(a,1),555(a,2))]. given #40 (H,wt=7): 593 d(x,y) * y = y. [para(170(a,1),572(a,1,2))]. given #41 (H,wt=5): 608 d(x,1) = 1. [para(593(a,1),14(a,1)),flip(a)]. given #42 (H,wt=15): 192 (x + y) + (d(x,y) * z) = x + (y + z). [para(27(a,1),150(a,1,2))]. given #43 (H,wt=13): 701 (x + 1) + (1 * y) = x + (1 + y). [para(608(a,1),192(a,1,2,1))]. given #44 (H,wt=11): 713 (x + 1) + y = x + (1 + y). [para(13(a,1),701(a,1,2))]. given #45 (H,wt=11): 760 x + (1 + y) = y + (x + 1). [para(713(a,1),28(a,1))]. given #46 (H,wt=11): 827 x + (y + 1) = y + (x + 1). [para(28(a,1),760(a,1,2))]. given #47 (H,wt=15): 654 (x + y) + (d(y,x) * z) = y + (x + z). [para(28(a,1),192(a,1,1))]. given #48 (H,wt=16): 123 -(x + y) + (y + (x + z)) = d(y,x) * z. [para(28(a,1),27(a,1,1,1))]. given #49 (H,wt=14): 1000 -(x + y) + (y + (x + 1)) = d(y,x). [para(14(a,1),123(a,2))]. given #50 (H,wt=14): 1148 -(x + y) + (x + (y + 1)) = d(y,x). [para(827(a,1),1000(a,1,2))]. given #51 (H,wt=9): 1175 d(x,y) * 1 = d(y,x). [para(1148(a,1),27(a,1)),flip(a)]. % Operation d is commutative; C redundancy checks enabled. given #52 (H,wt=7): 1234 d(x,y) = d(y,x). [para(1175(a,1),14(a,1))]. given #53 (H,wt=15): 1256 (x + y) + (d(x,y) * z) = y + (x + z). [para(1234(a,1),654(a,1,2,1))]. given #54 (H,wt=11): 1327 x + (y + z) = y + (x + z). [para(1256(a,1),192(a,1))]. given #55 (H,wt=21): 104 --(x + y) + (-x + (-y + z)) = d(-x,-y) * z. [para(11(a,1),27(a,1,1,1))]. given #56 (H,wt=19): 1466 (x + y) + (-x + (-y + z)) = d(-x,-y) * z. [para(104(a,1),33(a,1)),flip(a)]. given #57 (H,wt=19): 1581 (x + y) + (-x + (z + -y)) = d(-x,-y) * z. [para(28(a,1),1466(a,1,2,2))]. given #58 (H,wt=20): 1709 (-x + y) + (x + (z + -y)) = d(--x,-y) * z. [para(33(a,1),1581(a,1,2))]. given #59 (H,wt=20): 1803 (x + -y) + (y + (z + -x)) = d(--y,-x) * z. [para(28(a,1),1709(a,1,1))]. given #60 (H,wt=18): 1924 (x + -y) + (y + (z + -x)) = d(y,-x) * z. [para(170(a,1),1803(a,2,1,1))]. given #61 (H,wt=18): 2058 x + ((y + -x) + (z + -y)) = d(x,-y) * z. [para(1924(a,1),1327(a,1)),flip(a)]. given #62 (H,wt=18): 2147 x + (y + ((z + -x) + -z)) = d(x,-z) * y. [para(1327(a,1),2058(a,1,2))]. given #63 (H,wt=18): 2172 x + (y + (-z + (z + -x))) = d(x,-z) * y. [para(28(a,1),2147(a,1,2,2))]. given #64 (H,wt=13): 2251 d(x,-y) * z = x + (z + -x). [para(8(a,1),2172(a,1,2,2)),flip(a)]. given #65 (H,wt=8): 2387 d(x,-y) * z = z. [para(2251(a,2),194(a,1))]. given #66 (H,wt=7): 2474 d(x,y) * z = z. [para(170(a,1),2387(a,1,1,2))]. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 0.14 (+ 0.01) seconds. % Length of proof is 61. % Level of proof is 27. % Maximum clause weight is 21. % Given clauses 66. 5 d(x,y) = 1 # label("nearfield") # 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]. 14 x * 1 = x. [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 x + y = y + x. [assumption]. 29 d(c1,c2) != 1 # label("nearfield"). [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))]. 104 --(x + y) + (-x + (-y + z)) = d(-x,-y) * z. [para(11(a,1),27(a,1,1,1))]. 123 -(x + y) + (y + (x + z)) = d(y,x) * z. [para(28(a,1),27(a,1,1,1))]. 138 x + -x = 0. [para(31(a,1),28(a,1)),flip(a)]. 146 d(x,y) * -y = -(x + y) + (x + 0). [para(138(a,1),27(a,1,2,2)),flip(a)]. 147 --x = x + 0. [para(33(a,1),6(a,1)),flip(a)]. 150 x + (-x + y) = y. [para(33(a,1),8(a,1))]. 170 --x = x. [para(6(a,1),147(a,2))]. 187 x + -(x + y) = -y. [para(11(a,1),150(a,1,2))]. 192 (x + y) + (d(x,y) * z) = x + (y + z). [para(27(a,1),150(a,1,2))]. 194 x + (y + -x) = y. [para(28(a,1),150(a,1,2))]. 234 -(x * y) + (x * y) = x * 0. [para(6(a,1),69(a,1,2,2))]. 261 -(x * y) + (x * 0) = x * -y. [para(138(a,1),69(a,1,2,2))]. 285 x * 0 = 0. [para(234(a,1),31(a,1))]. 322 -(x * y) + 0 = x * -y. [para(285(a,1),261(a,1,2))]. 323 -(x * y) = x * -y. [para(322(a,1),6(a,1)),flip(a)]. 369 d(x,y) * -y = -(x + y) + x. [para(6(a,1),146(a,2,2))]. 446 d(x,y) * -y = x + -(x + y). [para(369(a,2),28(a,1))]. 514 d(x,y) * -y = -y. [para(446(a,2),187(a,1))]. 555 d(x,y) * --y = --y. [para(514(a,1),323(a,1,1)),flip(a)]. 572 d(x,y) * --y = y. [para(170(a,1),555(a,2))]. 593 d(x,y) * y = y. [para(170(a,1),572(a,1,2))]. 608 d(x,1) = 1. [para(593(a,1),14(a,1)),flip(a)]. 654 (x + y) + (d(y,x) * z) = y + (x + z). [para(28(a,1),192(a,1,1))]. 701 (x + 1) + (1 * y) = x + (1 + y). [para(608(a,1),192(a,1,2,1))]. 713 (x + 1) + y = x + (1 + y). [para(13(a,1),701(a,1,2))]. 760 x + (1 + y) = y + (x + 1). [para(713(a,1),28(a,1))]. 827 x + (y + 1) = y + (x + 1). [para(28(a,1),760(a,1,2))]. 1000 -(x + y) + (y + (x + 1)) = d(y,x). [para(14(a,1),123(a,2))]. 1148 -(x + y) + (x + (y + 1)) = d(y,x). [para(827(a,1),1000(a,1,2))]. 1175 d(x,y) * 1 = d(y,x). [para(1148(a,1),27(a,1)),flip(a)]. 1234 d(x,y) = d(y,x). [para(1175(a,1),14(a,1))]. 1256 (x + y) + (d(x,y) * z) = y + (x + z). [para(1234(a,1),654(a,1,2,1))]. 1327 x + (y + z) = y + (x + z). [para(1256(a,1),192(a,1))]. 1466 (x + y) + (-x + (-y + z)) = d(-x,-y) * z. [para(104(a,1),33(a,1)),flip(a)]. 1581 (x + y) + (-x + (z + -y)) = d(-x,-y) * z. [para(28(a,1),1466(a,1,2,2))]. 1709 (-x + y) + (x + (z + -y)) = d(--x,-y) * z. [para(33(a,1),1581(a,1,2))]. 1803 (x + -y) + (y + (z + -x)) = d(--y,-x) * z. [para(28(a,1),1709(a,1,1))]. 1924 (x + -y) + (y + (z + -x)) = d(y,-x) * z. [para(170(a,1),1803(a,2,1,1))]. 2058 x + ((y + -x) + (z + -y)) = d(x,-y) * z. [para(1924(a,1),1327(a,1)),flip(a)]. 2147 x + (y + ((z + -x) + -z)) = d(x,-z) * y. [para(1327(a,1),2058(a,1,2))]. 2172 x + (y + (-z + (z + -x))) = d(x,-z) * y. [para(28(a,1),2147(a,1,2,2))]. 2251 d(x,-y) * z = x + (z + -x). [para(8(a,1),2172(a,1,2,2)),flip(a)]. 2387 d(x,-y) * z = z. [para(2251(a,2),194(a,1))]. 2474 d(x,y) * z = z. [para(170(a,1),2387(a,1,1,2))]. 2500 d(x,y) = 1. [para(2474(a,1),14(a,1)),flip(a)]. 2501 $F. [resolve(2500,a,29,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=66. Generated=3046. Kept=2492. proofs=1. Usable=62. Sos=2310. Demods=0. Limbo=2, Disabled=138. Hints=58. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=554. Back_subsumed=117. 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=3.59. User_CPU=0.14, System_CPU=0.01, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 1 proof. ------ process 7570 exit (max_proofs) ------  Process 7570 exit (max_proofs) Sun Nov 16 12:38:52 2008