Prooof out3b2-46 x + (x + x')' = g(x). x + (x + (x + (x + g(x)))') = h(x). % Problem 46 ============================== PROOF ================================= % Proof 1 at 121.63 (+ 0.40) seconds: Winker2b. % Length of proof is 43. % Level of proof is 13. % Maximum clause weight is 34. % Given clauses 898. 2 (exists a exists b (a + b)' = b') # answer(Winker2b) # label(non_clause) # label(goal). [goal]. 6 x + y = y + x # label(Commutativity). [assumption]. 7 (x + y) + z = x + (y + z) # label(Associativity). [assumption]. 8 ((x + y)' + (x + y')')' = x # label(Robbins). [assumption]. 9 x + (x + x')' = g(x). [assumption]. 10 x + (x + (x + (x + g(x)))') = h(x). [assumption]. 12 (x + y)' != y' # answer(Winker2b). [deny(2)]. 17 x + (y + z) = y + (x + z). [para(6(a,1),7(a,1,1)),rewrite([7(2)])]. 18 ((x + y)' + (y + x')')' = y. [para(6(a,1),8(a,1,1,1,1))]. 19 ((x + y)' + (y' + x)')' = x. [para(6(a,1),8(a,1,1,2,1))]. 20 ((x + (y + z))' + (x + (y + z'))')' = x + y. [para(7(a,1),8(a,1,1,1,1)),rewrite([7(6)])]. 22 ((x + y)' + (x + ((y + z)' + (y + z')'))')' = x. [para(8(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])]. 23 (x + (x + (y' + (x + y)'))')' = (x + y)'. [para(8(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 24 x + ((x + x')' + y) = g(x) + y. [para(9(a,1),7(a,1,1)),flip(a)]. 27 x + (x + ((x + (x + g(x)))' + y)) = h(x) + y. [para(10(a,1),7(a,1,1)),rewrite([7(8)]),flip(a)]. 28 x + (y + (x + (x + (x + g(x)))')) = y + h(x). [para(10(a,1),7(a,2,2)),rewrite([17(7),7(6)])]. 29 (h(x)' + (x + (x + (x + (x + g(x)))')')')' = x. [para(10(a,1),8(a,1,1,1,1))]. 30 ((x + (y + z))' + (y + (x + z)')')' = y. [para(17(a,1),8(a,1,1,1,1))]. 31 x + (y + (x + x')') = y + g(x). [para(9(a,1),17(a,1,2)),flip(a)]. 34 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),18(a,1,1,1,1))]. 52 (x + (x + (y + (x + y')'))')' = (x + y')'. [para(8(a,1),19(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 76 (x + (y + (x + (y + (z' + (x + (y + z))')))'))' = (x + (y + z))'. [para(20(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(10),7(10)])]. 95 ((x + g(y))' + (y + (x + (y + y')')')')' = y. [para(31(a,1),8(a,1,1,1,1))]. 200 x + (x + (y + (x + (x + g(x)))')) = y + h(x). [para(28(a,1),7(a,2)),rewrite([17(7),7(6)])]. 249 ((x + (y + (z + u))')' + (x + (y + (z + (y + (z + (u' + (y + (z + u))')))')))')' = x. [para(20(a,1),22(a,1,1,2,1,2,2)),rewrite([6(12),7(12),7(11),6(15),7(15)])]. 319 ((g(x) + y)' + ((x + x')' + (x + y)')')' = (x + x')'. [para(24(a,1),30(a,1,1,1,1))]. 348 (x + (x + ((y + z)' + (y + (z + x))'))')' = (y + (z + x))'. [para(34(a,1),8(a,1,1,2)),rewrite([6(7),7(7),6(9)])]. 377 ((x + y)' + (x + (x + (y' + (x + y)')))')' = x. [para(23(a,1),8(a,1,1,2)),rewrite([6(10)])]. 505 (x + (h(x) + (x + (x + (x + (x + g(x)))')')')')' = (x + (x + (x + (x + g(x)))')')'. [para(29(a,1),19(a,1,1,2)),rewrite([6(10),6(12)])]. 1947 (x + (x + g(x))')' = (x + x')'. [para(9(a,1),52(a,1,1,2,1,2))]. 2067 ((x + (x + g(x)))' + (x + x')')' = x. [para(1947(a,1),8(a,1,1,2))]. 3555 ((x + x)' + (g(x) + (x + (x + g(x)))')')' = x. [para(2067(a,1),95(a,1,1,2,1,2)),rewrite([6(6),6(10)])]. 3569 (x + (g(x) + ((x + x)' + (x + (x + g(x)))'))')' = (x + x)'. [para(3555(a,1),8(a,1,1,2)),rewrite([17(9),6(11)])]. 10391 (x + (x + (h(x) + g(x)')'))' = (x + (x + g(x)))'. [para(200(a,1),76(a,1,1,2,2,1)),rewrite([6(4)])]. 12609 ((x + (x + g(x)))' + (h(x) + (x + (h(x) + g(x)')')')')' = x. [para(10391(a,1),377(a,1,1,1)),rewrite([10391(19),6(16),27(18)])]. 20382 (x + (x + (x + g(x)))')' = (x + x')'. [para(3569(a,1),319(a,1,1,2,1,2)),rewrite([348(13),6(10),8(11),6(5)])]. 20531 (x + (h(x) + g(x)')')' = g(x)'. [back_rewrite(505),rewrite([20382(7),9(5),20382(13),9(11)])]. 20563 ((x + (x + g(x)))' + (h(x) + g(x)')')' = x. [back_rewrite(12609),rewrite([20531(12)])]. 22796 (x + (x + (x + (g(x) + (h(x) + g(x)')')))')' = (h(x) + g(x)')'. [para(20563(a,1),19(a,1,1,2)),rewrite([6(9),7(9),7(8),6(11)])]. 24206 ((x + x')' + (x + (x + (x + (h(x) + g(x)')')))')' = x. [para(20382(a,1),249(a,1,1,1)),rewrite([200(12),6(7)])]. 25309 (h(x) + g(x)')' = (x + x')'. [para(24206(a,1),8(a,1,1,2)),rewrite([17(12),17(11),17(10),24(10),6(11),22796(12)])]. 25424 (x + (x + g(x)))' = (x + g(x))'. [back_rewrite(10391),rewrite([25309(5),9(4)]),flip(a)]. 25425 $F # answer(Winker2b). [resolve(25424,a,12,a)]. ============================== end of proof ==========================