Prooof out3b2-119 (x + (x + x)')' = g(x). (x + (x + (x + g(x))))' = h(x). % Problem 119 ============================== PROOF ================================= % Proof 1 at 16.67 (+ 0.08) seconds: Winker2a. % Length of proof is 39. % Level of proof is 13. % Maximum clause weight is 35. % Given clauses 390. 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)')' = 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))]. 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)])]. 26 (g(x) + (x + (x + x))')' = x. [para(9(a,1),8(a,1,1,2)),rewrite([6(5)])]. 32 (x + h(x))' = g(x). [para(26(a,1),8(a,1,1,2)),rewrite([17(4),17(3),6(2),10(5),6(2)])]. 33 (g(x) + (x + h(x)')')' = x. [para(32(a,1),8(a,1,1,1))]. 34 ((x + g(y))' + (x + (y + h(y)))')' = x. [para(32(a,1),8(a,1,1,2,1,2)),rewrite([6(8)])]. 37 (x + (x + (g(x) + h(x)'))')' = g(x). [para(33(a,1),8(a,1,1,2)),rewrite([17(5),6(7)])]. 43 ((x + (y + z))' + (z + (x + y)')')' = z. [para(7(a,1),18(a,1,1,1,1))]. 47 (x + (x + (y' + (y + x)'))')' = (y + x)'. [para(18(a,1),8(a,1,1,2)),rewrite([6(5),7(5),6(7)])]. 83 ((x + (y + (y + (y + g(y)))))' + (h(y) + x)')' = x. [para(10(a,1),19(a,1,1,2,1,1))]. 87 ((x + (y + h(y)))' + (g(y) + x)')' = x. [para(32(a,1),19(a,1,1,2,1,1))]. 89 ((x + (y + (y + (g(y) + h(y)'))'))' + (g(y) + x)')' = x. [para(37(a,1),19(a,1,1,2,1,1))]. 112 (h(x) + (x + (x + (x + g(x))'))')' = x + x. [para(10(a,1),20(a,1,1,1))]. 258 (x + (x + (y + (h(y) + (x + g(y))')))')' = (x + g(y))'. [para(34(a,1),8(a,1,1,2)),rewrite([6(7),7(7),7(6),6(9)])]. 321 (g(x) + (x + ((h(x) + y)' + (h(x) + y')'))')' = x. [para(32(a,1),22(a,1,1,1))]. 724 (x + (x + (x + (x + (h(x) + (x + g(x))')))'))' = h(x). [para(112(a,1),8(a,1,1,2)),rewrite([17(7),17(6),6(10),7(10)])]. 4056 (x + (x + (g(x) + ((h(x) + y)' + (h(x) + y')')))')' = g(x). [para(321(a,1),8(a,1,1,2)),rewrite([17(11),6(13)])]. 4435 (x + (x + (h(x) + (x + g(x))'))')' = h(x). [para(724(a,1),23(a,1,1,2,1,2,2)),rewrite([258(10),6(5),724(20)])]. 4512 (h(x) + (x + (x + (h(x) + (x + g(x))')))')' = x. [para(4435(a,1),8(a,1,1,2)),rewrite([6(10)])]. 4598 ((x + (x + (h(x) + (x + g(x))')))' + (x + (h(x)' + (x + (x + (h(x) + (x + g(x))')))'))')' = x. [para(4512(a,1),47(a,1,1,2,1,2,2)),rewrite([6(19),6(20),7(20),4512(34)])]. 4606 (x + (x + (x + (x + (g(x) + (x + (x + (h(x) + (x + g(x))')))'))))')' = (x + (x + (h(x) + (x + g(x))')))'. [para(4512(a,1),83(a,1,1,2)),rewrite([6(13),7(13),7(12),7(11),6(15)])]. 18339 (x + (x + (h(x) + (x + g(x))')))' = g(x). [para(112(a,1),4056(a,1,1,2,1,2,2,2)),rewrite([17(8),17(7),6(11),7(11),17(12),17(11),4606(16)])]. 18537 (g(x) + (x + (g(x) + h(x)'))')' = x. [back_rewrite(4598),rewrite([18339(8),18339(11),6(5)])]. 18557 (g(x) + h(x))' = x. [back_rewrite(4512),rewrite([18339(9),6(3)])]. 18910 (x + (x + (h(x) + (x + (g(x) + h(x)'))'))')' = h(x). [para(18557(a,1),89(a,1,1,2)),rewrite([17(9),6(11)])]. 19332 (x + (g(x) + h(x)'))' = h(x). [para(18537(a,1),87(a,1,1,2)),rewrite([6(9),7(9),6(11),18910(12)]),flip(a)]. 19355 (h(x) + (h(x)' + (x + g(x))')')' = h(x)'. [para(19332(a,1),43(a,1,1,1))]. 19356 $F # answer(Winker2a). [resolve(19355,a,11,a)]. ============================== end of proof ==========================