Prooof out3b2-47 x + (x + x')' = g(x). x + (x + (x + g(x)))' = h(x). % Problem 47 ============================== PROOF ================================= % Proof 1 at 112.08 (+ 0.33) seconds: Winker2b. % Length of proof is 44. % Level of proof is 12. % Maximum clause weight is 29. % Given clauses 878. 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 + 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 + g(x)))' + y) = h(x) + y. [para(10(a,1),7(a,1,1)),flip(a)]. 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)]. 32 x + (y + (x + (x + g(x)))') = y + h(x). [para(10(a,1),17(a,1,2)),flip(a)]. 35 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),18(a,1,1,1,1))]. 53 (x + (x + (y + (x + y')'))')' = (x + y')'. [para(8(a,1),19(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 77 (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)])]. 184 h(x) + (x + x')' = g(x) + (x + (x + g(x)))'. [para(27(a,1),31(a,1)),rewrite([6(11)])]. 223 (h(x)' + (x + (((x + (x + g(x)))' + y)' + ((x + (x + g(x)))' + y')'))')' = x. [para(10(a,1),22(a,1,1,1,1))]. 273 ((x + x)' + (h(x) + (x + (x + g(x))')')')' = x. [para(27(a,1),22(a,1,1,2,1))]. 330 h(x) + (y + (x + x')') = y + (g(x) + (x + (x + g(x)))'). [para(184(a,1),17(a,1,2)),flip(a)]. 340 ((x + y)' + (x + (x + (y' + (x + y)')))')' = x. [para(23(a,1),8(a,1,1,2)),rewrite([6(10)])]. 413 ((g(x) + y)' + ((x + x')' + (x + y)')')' = (x + x')'. [para(24(a,1),30(a,1,1,1,1))]. 448 (x + (x + ((y + z)' + (y + (z + x))'))')' = (y + (z + x))'. [para(35(a,1),8(a,1,1,2)),rewrite([6(7),7(7),6(9)])]. 1787 (x + (h(x) + ((x + x)' + (x + (x + g(x))')'))')' = (x + x)'. [para(273(a,1),8(a,1,1,2)),rewrite([17(10),6(12)])]. 2163 (x + (x + g(x))')' = (x + x')'. [para(9(a,1),53(a,1,1,2,1,2))]. 2315 (x + (g(x) + ((x + x)' + (x + (x + g(x)))'))')' = (x + x)'. [back_rewrite(1787),rewrite([2163(8),330(8),17(9)])]. 9315 (x + (x + (x + (h(x) + g(x)'))'))' = (x + (x + g(x)))'. [para(32(a,1),77(a,1,1,2,2,1,2)),rewrite([6(4)])]. 13846 ((x + (x + g(x)))' + (x + (h(x) + (x + (x + (h(x) + g(x)'))')'))')' = x. [para(9315(a,1),340(a,1,1,1)),rewrite([9315(21),6(17),27(18)])]. 21794 (h(x)' + (x + (x + (x + (x + (h(x) + g(x)'))')))')' = x. [para(20(a,1),223(a,1,1,2,1,2,2)),rewrite([6(11),7(11),7(10),32(10),6(6),6(10),7(10)])]. 21959 (x + (x + (x + (x + (h(x)' + (x + (h(x) + g(x)'))'))))')' = h(x)'. [para(21794(a,1),8(a,1,1,2)),rewrite([17(12),17(11),17(10),6(14)])]. 22382 (x + x')' = h(x)'. [para(2315(a,1),413(a,1,1,2,1,2)),rewrite([448(13),6(10),8(11),6(5),10(5)]),flip(a)]. 27402 x + (h(x)' + y) = g(x) + y. [back_rewrite(24),rewrite([22382(3)])]. 27403 x + h(x)' = g(x). [back_rewrite(9),rewrite([22382(3)])]. 27606 (x + (x + (x + (g(x) + (x + (h(x) + g(x)'))')))')' = h(x)'. [back_rewrite(21959),rewrite([27402(10)])]. 27876 (x + (x + (h(x) + g(x)'))')' = g(x)'. [para(27403(a,1),53(a,1,1,2,1,2,2,1)),rewrite([27403(11)])]. 27944 ((x + (x + g(x)))' + (x + (h(x) + g(x)'))')' = x. [back_rewrite(13846),rewrite([27876(13)])]. 31241 (x + (h(x) + g(x)'))' = h(x)'. [para(27944(a,1),19(a,1,1,2)),rewrite([6(10),7(10),7(9),6(12),27606(13)]),flip(a)]. 31283 (x + (x + g(x)))' = (x + g(x))'. [back_rewrite(9315),rewrite([31241(6),27403(3)]),flip(a)]. 31284 $F # answer(Winker2b). [resolve(31283,a,12,a)]. ============================== end of proof ==========================