Prooof out3b2-213 x + (x + (x + x)')' = g(x). (x + (x + g(x)))' = h(x). % Problem 213 ============================== PROOF ================================= % Proof 1 at 44.43 (+ 0.21) seconds: Winker2a. % Length of proof is 41. % Level of proof is 14. % Maximum clause weight is 29. % Given clauses 668. 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 + (x + x)')' = g(x). [assumption]. 10 (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))]. 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)])]. 30 x + (y + (x + (x + x)')') = y + g(x). [para(9(a,1),17(a,1,2)),flip(a)]. 36 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),18(a,1,1,1,1))]. 40 (x + (x + (y' + (y + x)'))')' = (y + x)'. [para(18(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 55 (x + (y' + (x + (x + y)'))')' = (x + y)'. [para(19(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 57 (x + (x + (y + (x + y')'))')' = (x + y')'. [para(8(a,1),19(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 58 ((x + (y + (y + g(y))))' + (h(y) + x)')' = x. [para(10(a,1),19(a,1,1,2,1,1))]. 93 (h(x) + (x + (x + g(x)'))')' = x + x. [para(10(a,1),20(a,1,1,1))]. 196 (x + (x + (x + (x + (h(x) + g(x)')))'))' = h(x). [para(93(a,1),8(a,1,1,2)),rewrite([17(6),17(5),6(9),7(9)])]. 500 (h(x) + (x + (x + (x + (x + (h(x) + g(x)')))')')')' = x. [para(196(a,1),8(a,1,1,1))]. 718 ((x + g(y))' + ((y + (y + y)')' + (y + x)')')' = (y + (y + y)')'. [para(30(a,1),36(a,1,1,1,1))]. 2596 (x + (x + x)')' = (x + h(x))'. [para(30(a,1),57(a,1,1,2,1)),rewrite([6(3),17(3),6(2),10(4)]),flip(a)]. 2817 ((x + g(y))' + ((y + h(y))' + (y + x)')')' = (y + h(y))'. [back_rewrite(718),rewrite([2596(7),2596(16)])]. 2860 x + (y + (x + h(x))') = y + g(x). [back_rewrite(30),rewrite([2596(4)])]. 2862 x + (x + h(x))' = g(x). [back_rewrite(9),rewrite([2596(4)])]. 2872 (x + (g(x) + h(x)')')' = (x + h(x))'. [para(2862(a,1),55(a,1,1,2,1,2)),rewrite([6(4)])]. 2873 (x + (x + (x + (h(x) + g(x)')))')' = g(x)'. [para(2862(a,1),57(a,1,1,2,1,2,2,1)),rewrite([7(5),2862(13)])]. 2878 (h(x) + (x + g(x)')')' = x. [back_rewrite(500),rewrite([2873(10)])]. 2946 (h(x) + (x + (x + (h(x) + g(x)')))')' = x. [para(2878(a,1),57(a,1,1,2,1,2,2)),rewrite([6(6),17(7),17(6),2878(17)])]. 3188 ((x + (y + h(y))')' + (x + (y + (g(y) + h(y)')'))')' = x. [para(2872(a,1),8(a,1,1,2,1,2)),rewrite([6(14)])]. 3423 (x + (x + (x + (g(x) + (x + (x + (h(x) + g(x)')))')))')' = (x + (x + (h(x) + g(x)')))'. [para(2946(a,1),58(a,1,1,2)),rewrite([6(11),7(11),7(10),6(13)])]. 3433 ((x + (x + (h(x) + g(x)')))' + (x + (h(x)' + (x + (x + (h(x) + g(x)')))'))')' = x. [para(2946(a,1),40(a,1,1,2,1,2,2)),rewrite([6(17),6(18),7(18),2946(31)])]. 21095 (x + (g(x) + ((h(x) + y)' + (h(x) + y')'))')' = (x + h(x))'. [para(22(a,1),2817(a,1,1,2)),rewrite([6(10),6(12)])]. 22068 (x + (x + (h(x) + g(x)')))' = (x + h(x))'. [para(93(a,1),21095(a,1,1,2,1,2,2)),rewrite([17(7),17(6),6(10),7(10),17(11),17(10),3423(14)])]. 22353 ((x + h(x))' + (g(x) + h(x)')')' = x. [back_rewrite(3433),rewrite([22068(7),22068(12),2860(10),6(7)])]. 22379 (h(x) + (x + h(x))')' = x. [back_rewrite(2946),rewrite([22068(8)])]. 23280 (x + (x + (h(x) + (g(x) + h(x)')'))')' = h(x). [para(22379(a,1),3188(a,1,1,1)),rewrite([17(8)])]. 24643 (g(x) + h(x)')' = h(x). [para(22353(a,1),19(a,1,1,2)),rewrite([6(8),7(8),6(10),23280(11)]),flip(a)]. 24668 (h(x) + (g(x)' + h(x)')')' = h(x)'. [para(24643(a,1),18(a,1,1,1)),rewrite([6(6)])]. 24669 $F # answer(Winker2a). [resolve(24668,a,11,a)]. ============================== end of proof ==========================