============================== prooftrans ============================ 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 =========================== ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original 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 ==========================