Prooof out3-58

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

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

% Proof 1 at 72.45 (+ 0.35) seconds: Winker2a.
% Length of proof is 32.
% Level of proof is 10.
% Maximum clause weight is 26.
% Given clauses 788.

1 (exists a exists b (a + b)' = a') # answer(Winker2a) # 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 + (x + g(x)')) = h(x).  [assumption].
11 (x + y)' != x' # answer(Winker2a).  [deny(1)].
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)])].
29 (h(x)' + (x + (x + (x + g(x)'))')')' = x.  [para(10(a,1),8(a,1,1,1,1))].
37 (x + (x + (x + g(x)'))')' = g(x)'.  [para(26(a,1),8(a,1,1,2)),rewrite([6(4),7(4),6(6)])].
38 (g(x)' + h(x)')' = x.  [back_rewrite(29),rewrite([37(9),6(5)])].
40 ((x + y)' + (x + (g(y)' + h(y)'))')' = x.  [para(38(a,1),8(a,1,1,2,1,2)),rewrite([6(10)])].
41 (x + (h(x) + g(x)')')' = g(x)'.  [para(38(a,1),8(a,1,1,2)),rewrite([6(4),6(6)])].
46 ((x + (y + z))' + (z + (x + y)')')' = z.  [para(7(a,1),18(a,1,1,1,1))].
48 (x + ((y + x)' + (x + y')'')')' = (y + x)'.  [para(18(a,1),8(a,1,1,1))].
65 (g(x)' + (x + (h(x) + g(x)'))')' = x.  [para(41(a,1),8(a,1,1,2)),rewrite([6(9)])].
79 (x + (x + (y + (x + y')'))')' = (x + y')'.  [para(8(a,1),19(a,1,1,2)),rewrite([6(5),7(5),6(7)])].
84 ((x + (g(y)' + h(y)'))' + (y + x)')' = x.  [para(38(a,1),19(a,1,1,2,1,1))].
252 ((x + (g(y)' + (y + (h(y) + g(y)'))'))' + (y + x)')' = x.  [para(65(a,1),19(a,1,1,2,1,1))].
300 (x + (g(x)' + (((x + x)' + y)' + ((x + x)' + y')'))')' = g(x)'.  [para(26(a,1),22(a,1,1,1))].
830 (h(x)' + (x + (g(x)' + (x + x)'))')' = x + g(x)'.  [para(10(a,1),46(a,1,1,1,1)),rewrite([7(8)])].
12641 (x + (g(x)' + (x + (g(x)' + (h(x)' + (x + x)')))'))' = h(x)'.  [para(830(a,1),8(a,1,1,2)),rewrite([17(9),17(8),6(14),7(14)])].
22972 (x + h(x)')' = g(x)'.  [para(40(a,1),300(a,1,1,2,1,2,2)),rewrite([6(11),7(11),7(10),6(13),17(14),12641(15)])].
23033 (x + (x + (h(x) + g(x)'))')' = g(x)'.  [para(22972(a,1),79(a,1,1,2,1,2,2)),rewrite([22972(12)])].
23154 (g(x)' + (g(x)' + (h(x)' + (x + (h(x) + g(x)'))'))')' = h(x)'.  [para(22972(a,1),252(a,1,1,2)),rewrite([17(12),6(16)])].
23599 (x + (h(x) + g(x)'))' = h(x)'.  [para(23033(a,1),84(a,1,1,2)),rewrite([6(12),7(12),6(16),23154(17)]),flip(a)].
23628 (h(x) + (g(x)' + (h(x)' + (h(x) + (x' + g(x)'))'')'))' = h(x)'.  [para(23599(a,1),48(a,1,1,2,1,1)),rewrite([6(12),17(12),7(17),23599(24)])].
23629 $F # answer(Winker2a).  [resolve(23628,a,11,a)].

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