Prooof out3-53

x + x' = g(x).   x + (x + g(x)') = h(x). % Problem 53

============================== PROOF =================================

% Proof 1 at 103.80 (+ 0.48) seconds: Winker1a.
% Length of proof is 36.
% Level of proof is 10.
% Maximum clause weight is 26.
% Given clauses 969.

3 (exists a exists b a + b = a) # answer(Winker1a) # 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' = g(x).  [assumption].
10 x + (x + g(x)') = h(x).  [assumption].
13 x + y != x # answer(Winker1a).  [deny(3)].
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))].
22 ((x + y)' + (x + ((y + z)' + (y + z')'))')' = x.  [para(8(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])].
26 (g(x)' + (x + x)')' = x.  [para(9(a,1),8(a,1,1,2,1)),rewrite([6(5)])].
27 x + (x + (g(x)' + y)) = h(x) + y.  [para(10(a,1),7(a,1,1)),rewrite([7(6)]),flip(a)].
28 x + (y + (x + g(x)')) = y + h(x).  [para(10(a,1),7(a,2,2)),rewrite([17(5),7(4)])].
36 (x + h(x)')' = g(x)'.  [para(26(a,1),8(a,1,1,2)),rewrite([6(4),7(4),10(4),6(3)])].
39 (g(x)' + (x + h(x))')' = x.  [para(36(a,1),8(a,1,1,2)),rewrite([6(6)])].
44 ((x + (y + z))' + (z + (x + y)')')' = z.  [para(7(a,1),18(a,1,1,1,1))].
62 ((x + y)' + (x + (g(y)' + (y + h(y))'))')' = x.  [para(39(a,1),8(a,1,1,2,1,2)),rewrite([6(11)])].
63 (x + (x + (h(x) + g(x)'))')' = g(x)'.  [para(39(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])].
75 x + (x + (y + g(x)')) = y + h(x).  [para(28(a,1),7(a,2)),rewrite([17(5),7(4)])].
79 ((x' + y)' + (y + x)')' = y.  [para(6(a,1),19(a,1,1))].
85 (x + (x + (y + (x + y')'))')' = (x + y')'.  [para(8(a,1),19(a,1,1,2)),rewrite([6(5),7(5),6(7)])].
95 ((x + (g(y)' + (y + h(y))'))' + (y + x)')' = x.  [para(39(a,1),19(a,1,1,2,1,1))].
210 (g(x)' + (h(x) + h(x))')' = x.  [para(63(a,1),8(a,1,1,2)),rewrite([75(6),6(7)])].
222 ((x + (g(y)' + (h(y) + h(y))'))' + (y + x)')' = x.  [para(210(a,1),19(a,1,1,2,1,1))].
278 ((x + y)' + (y + (g(x)' + (x + x)'))')' = y.  [para(26(a,1),79(a,1,1,1,1,1))].
342 (x + (g(x)' + (((x + x)' + y)' + ((x + x)' + y')'))')' = g(x)'.  [para(26(a,1),22(a,1,1,1))].
917 ((h(x) + y)' + (g(x)' + (y + (x + x)'))')' = g(x)' + y.  [para(27(a,1),44(a,1,1,1,1)),rewrite([7(9)])].
919 ((x + h(y))' + (y + (g(y)' + (y + x)'))')' = y + g(y)'.  [para(28(a,1),44(a,1,1,1,1)),rewrite([7(9)])].
23866 (x + (g(x)' + (x + (g(x)' + ((x + y)' + (y + h(x))')))'))' = (y + h(x))'.  [para(919(a,1),18(a,1,1,2)),rewrite([7(10),7(9),6(15),7(15)])].
25268 (x + (x + h(x))')' = g(x)'.  [para(62(a,1),342(a,1,1,2,1,2,2)),rewrite([17(12),17(11),6(14),17(15),23866(16)])].
25315 (g(x)' + (g(x)' + ((x + h(x))' + (h(x) + h(x))'))')' = (x + h(x))'.  [para(25268(a,1),222(a,1,1,2)),rewrite([17(11),6(15)])].
25321 (x + (h(x) + h(x))')' = g(x)'.  [para(25268(a,1),85(a,1,1,2,1,2,2)),rewrite([7(5),75(6),25268(11)])].
25560 (h(x) + h(x))' = (x + h(x))'.  [para(25321(a,1),95(a,1,1,2)),rewrite([6(11),7(11),6(15),25315(16)]),flip(a)].
25729 h(x) + g(x)' = h(x).  [para(25560(a,1),917(a,1,1,1)),rewrite([17(10),278(13),6(5)]),flip(a)].
25730 $F # answer(Winker1a).  [resolve(25729,a,13,a)].

============================== end of proof ==========================