Prooof out3b2-222

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

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

% Proof 1 at 52.56 (+ 0.24) seconds: Winker2b.
% Length of proof is 29.
% Level of proof is 11.
% Maximum clause weight is 29.
% Given clauses 757.

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 + x)')' = g(x).  [assumption].
10 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)])].
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)])].
24 x + ((x + (x + x)')' + y) = g(x) + y.  [para(9(a,1),7(a,1,1)),flip(a)].
31 x + (y + (x + (x + x)')') = y + g(x).  [para(9(a,1),17(a,1,2)),flip(a)].
32 x + (y + (x + (x + g(x)))') = y + h(x).  [para(10(a,1),17(a,1,2)),flip(a)].
53 (x + (x + (y + (x + y')'))')' = (x + y')'.  [para(8(a,1),19(a,1,1,2)),rewrite([6(5),7(5),6(7)])].
93 (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)])].
224 (h(x)' + (x + (((x + (x + g(x)))' + y)' + ((x + (x + g(x)))' + y')'))')' = x.  [para(10(a,1),22(a,1,1,1,1))].
1756 (x + (x + x)')' = h(x)'.  [para(31(a,1),53(a,1,1,2,1)),rewrite([6(3),17(3),6(2),10(5)]),flip(a)].
1971 x + (h(x)' + y) = g(x) + y.  [back_rewrite(24),rewrite([1756(4)])].
1972 x + h(x)' = g(x).  [back_rewrite(9),rewrite([1756(4)])].
2033 (x + (x + (h(x) + g(x)'))')' = g(x)'.  [para(1972(a,1),53(a,1,1,2,1,2,2,1)),rewrite([1972(11)])].
16416 (x + (x + (x + (h(x) + g(x)'))'))' = (x + (x + g(x)))'.  [para(32(a,1),93(a,1,1,2,2,1,2)),rewrite([6(4)])].
17678 ((x + (x + g(x)))' + (x + g(x)')')' = x.  [para(16416(a,1),8(a,1,1,1)),rewrite([2033(12)])].
17756 ((x + (x + g(x)))' + (x + (h(x) + g(x)'))')' = x.  [para(17678(a,1),53(a,1,1,2,1,2,2)),rewrite([6(12),6(13),7(13),7(12),32(12),6(8),17678(22)])].
17939 (x + (x + (x + (g(x) + (x + (h(x) + g(x)'))')))')' = (x + (h(x) + g(x)'))'.  [para(17756(a,1),19(a,1,1,2)),rewrite([6(10),7(10),7(9),6(12)])].
24737 (h(x)' + (x + (x + (x + (x + (h(x) + g(x)'))')))')' = x.  [para(20(a,1),224(a,1,1,2,1,2,2)),rewrite([6(11),7(11),7(10),32(10),6(6),6(10),7(10)])].
24937 (x + (h(x) + g(x)'))' = h(x)'.  [para(24737(a,1),8(a,1,1,2)),rewrite([17(12),17(11),17(10),1971(10),6(12),17939(13)])].
25125 (x + (x + g(x)))' = (x + g(x))'.  [back_rewrite(16416),rewrite([24937(6),1972(3)]),flip(a)].
25126 $F # answer(Winker2b).  [resolve(25125,a,12,a)].

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