% Length of proof is 281.

% Level of proof is 49.

% Maximum clause weight is 27.

% Given clauses 207.

1 x * ((x * y) * z) = (y * (z * x)) * x # label(non_clause) # label(goal). [goal].

3 x * 1 = x. [assumption].

4 x * (x \ y) = y. [assumption].

5 x \ (x * y) = y. [assumption].

6 (x * y) / y = x. [assumption].

7 (x / y) * y = x. [assumption].

8 x' * x = 1. [assumption].

9 x * x' = 1. [assumption].

10 x * ((x * y) * z) = (y * x) * (x * z). [assumption].

11 (x * y) * (y * z) = y * ((y * x) * z). [copy(10),flip(a)].

12 (x * y) * y = y * (y * x). [assumption].

13 x * (y * z) = ((x * y) / x) * (x * z). [assumption].

14 ((x * y) / x) * (x * z) = x * (y * z). [copy(13),flip(a)].

15 x * (y * y) = (y * y) * x. [assumption].

16 (x * x) * y = y * (x * x). [copy(15),flip(a)].

17 (c2 * (c3 * c1)) * c1 != c1 * ((c1 * c2) * c3). [deny(1)].

22 x / (y \ x) = y. [para(4(a,1),6(a,1,1))].

23 (x / y) \ x = y. [para(7(a,1),5(a,1,2))].

26 1 / x = x'. [para(8(a,1),6(a,1,1))].

27 x \ 1 = x'. [para(9(a,1),5(a,1,2))].

28 x'' = x. [para(9(a,1),6(a,1,1)),rewrite([26(3)])].

30 x * ((x * y) * (x \ z)) = (y * x) * z. [para(4(a,1),11(a,1,2)),flip(a)].

31 (x * y) \ (y * ((y * x) * z)) = y * z. [para(11(a,1),5(a,1,2))].

33 x * ((x * (y / x)) * z) = y * (x * z). [para(7(a,1),11(a,1,1)),flip(a)].

36 x * ((x * y) * x') = y * x. [para(9(a,1),11(a,1,2)),rewrite([3(3)]),flip(a)].

40 (x * y) \ (y * (y * x)) = y. [para(12(a,1),5(a,1,2))].

42 x * (x * (y / x)) = y * x. [para(7(a,1),12(a,1,1)),flip(a)].

47 (x / y) * (y * z) = y * ((y \ x) * z). [para(4(a,1),14(a,1,1,1))].

48 ((x * y) / x) * z = x * (y * (x \ z)). [para(4(a,1),14(a,1,2))].

51 x' * (x * y) = x * (x' * y). [para(8(a,1),14(a,1,1,1)),rewrite([26(3),28(2)]),flip(a)].

54 (x * y) / x = x * (y * x'). [para(9(a,1),14(a,1,2)),rewrite([3(4)])].

73 (x * (y * x')) * z = x * (y * (x \ z)). [back_rewrite(48),rewrite([54(2)])].

79 x \ ((y * y) * x) = y * y. [para(16(a,2),5(a,1,2))].

80 x * ((y * y) * x') = y * y. [para(16(a,1),6(a,1,1)),rewrite([54(3)])].

81 (x * x) * (y * (x * x)') = y. [para(16(a,2),6(a,1,1)),rewrite([54(4)])].

82 (x * x) * (y / (x * x)) = y. [para(16(a,2),7(a,1))].

90 (x * x) * (y * x) = x * ((x * y) * x). [para(16(a,2),11(a,1))].

97 ((x \ y) * x) \ (x * y) = x. [para(4(a,1),40(a,1,2,2))].

105 x \ (y * x) = x * (y / x). [para(42(a,1),5(a,1,2))].

113 x * ((y * y) / x) = y * y. [back_rewrite(79),rewrite([105(3)])].

114 (x * x) \ y = y / (x * x). [para(82(a,1),5(a,1,2))].

118 (x * x) * (y * z) = y * ((x * x) * z). [para(82(a,1),11(a,2,2,1)),rewrite([16(4,R),82(4)]),flip(a)].

124 ((x \ x') * x)' = x. [para(9(a,1),97(a,1,2)),rewrite([27(5)])].

128 (x \ y) * x = x * (y * x'). [para(97(a,1),22(a,1,2)),rewrite([54(2)]),flip(a)].

129 (x * (x * (y * x'))) \ (x * (y * y)) = x * (y * x'). [para(97(a,1),97(a,1,1,1)),rewrite([128(2),128(6),73(9),5(6),128(9)])].

132 (x * (x' * x'))' = x. [back_rewrite(124),rewrite([128(3)])].

135 (x * (y * x')) \ (x * y) = x. [back_rewrite(97),rewrite([128(2)])].

139 x * (x' * x') = x'. [para(132(a,1),28(a,1,1)),flip(a)].

140 x \ x' = x' * x'. [para(139(a,1),5(a,1,2))].

143 x' \ x = x * x. [para(28(a,1),140(a,1,2)),rewrite([28(4),28(4)])].

144 x / (x * x) = x'. [para(143(a,1),22(a,1,2))].

147 x * ((y / x) / x) = x \ y. [para(7(a,1),105(a,1,2)),flip(a)].

154 x \ (y * y) = (y * y) / x. [para(113(a,1),5(a,1,2))].

162 x \ (x \ y) = (y / x) / x. [para(147(a,1),5(a,1,2))].

170 x * (x' * (x' * y)) = x \ y. [para(5(a,1),162(a,1,2)),rewrite([54(3),54(5),12(5)]),flip(a)].

174 x \ ((y / x) / x) = ((x \ y) / x) / x. [para(162(a,1),162(a,1,2))].

175 (x * y) * x' = x * (y / x). [para(36(a,1),5(a,1,2)),rewrite([105(2)]),flip(a)].

182 x * ((x \ y) * x') = y / x. [para(147(a,1),36(a,1,2,1)),rewrite([7(7)])].

188 x * (x' * (y * y)) = y * y. [para(16(a,1),54(a,2,2)),rewrite([54(3),80(4)]),flip(a)].

192 (x * x) / y = (x * x) * y'. [para(80(a,1),5(a,1,2)),rewrite([154(2)])].

199 x' * ((y * y) * x) = y * y. [para(28(a,1),80(a,1,2,2))].

203 x \ (y * y) = (y * y) * x'. [back_rewrite(154),rewrite([192(4)])].

205 x / (y * y) = x * (y * y)'. [para(81(a,1),5(a,1,2)),rewrite([114(2)])].

213 x * (x * x)' = x'. [back_rewrite(144),rewrite([205(2)])].

214 (x * x) \ y = y * (x * x)'. [back_rewrite(114),rewrite([205(4)])].

215 (x * x)' = x' * x'. [para(213(a,1),5(a,1,2)),rewrite([140(2)]),flip(a)].

219 (x * x) \ y = y * (x' * x'). [back_rewrite(214),rewrite([215(4)])].

223 x / (y * y) = x * (y' * y'). [back_rewrite(205),rewrite([215(4)])].

225 (x * x) * (y * (x' * x')) = y. [back_rewrite(81),rewrite([215(3)])].

233 ((x * x) * y') * y = x * x. [para(16(a,1),128(a,2,2)),rewrite([203(2),188(8)])].

234 x * ((x \ y) / x) = y * x'. [para(128(a,1),105(a,1,2)),rewrite([5(4)]),flip(a)].

236 (x * y) \ (x * (y / x')) = x. [para(7(a,1),135(a,1,1,2))].

242 (x * y) \ (x * (y / x)) = x'. [para(175(a,1),5(a,1,2))].

243 (x * (y / x)) / x' = x * y. [para(175(a,1),6(a,1,1))].

251 (x' * x') * (y * (x * x)) = y. [para(16(a,1),175(a,1,1)),rewrite([215(4),16(6,R),223(9),225(12)])].

252 ((x * x) * y) * y' = x * x. [para(16(a,2),175(a,1,1)),rewrite([192(6),80(8)])].

253 (x' * y) * x = x' * (y / x'). [para(28(a,1),175(a,1,2))].

256 x * (x * ((y / x) * x')) = (y * x) * x'. [para(42(a,1),175(a,1,1)),rewrite([54(6)]),flip(a)].

258 x \ (y / x) = (x \ y) * x'. [para(147(a,1),175(a,1,1)),rewrite([147(7)]),flip(a)].

265 ((x \ y) / x) / x = x' * (x' * (x \ y)). [back_rewrite(174),rewrite([258(3),258(2),12(5)]),flip(a)].

295 (x * x) * (y * (x * x))' = y'. [para(199(a,1),135(a,1,2)),rewrite([28(5),12(4),51(5),51(4),188(4),203(4)])].

301 x \ (y * x') = (x \ y) / x. [para(234(a,1),5(a,1,2))].

305 (x \ y) * (x * z) = x * ((y * x') * z). [para(234(a,1),11(a,2,2,1)),rewrite([7(3)])].

307 (x / y) / y = y' * (y' * x). [para(12(a,1),234(a,2)),rewrite([301(3),265(3),170(6),162(2)])].

322 x \ (x \ y) = x' * (x' * y). [back_rewrite(162),rewrite([307(4)])].

323 (x * y) * x = x * (y / x'). [para(236(a,1),4(a,1,2))].

340 (x * x) * (y * x) = x * (x * (y / x')). [back_rewrite(90),rewrite([323(5)])].

342 (x * (y * x)) \ (x * y) = x'. [para(6(a,1),242(a,1,2,2))].

353 (x * y) / x' = x * (y * x). [para(6(a,1),243(a,1,1,2))].

370 ((x \ y) * x') * x = x * ((y / x) * x'). [para(258(a,1),128(a,1,1))].

384 x' \ (y * x) = (x' \ y) / x'. [para(28(a,1),301(a,1,2,2))].

387 x * ((x \ y) / x') = y * x. [para(4(a,1),323(a,1,1)),flip(a)].

396 x * (x * (y * x')) = y / x'. [para(323(a,1),105(a,1,2)),rewrite([5(4),54(4)]),flip(a)].

404 (x / y) / y' = (x * y) * y'. [back_rewrite(256),rewrite([396(5)])].

406 (x / y') \ (y * (x * x)) = y * (x * y'). [back_rewrite(129),rewrite([396(4)])].

418 ((x * y) * y') \ (x / y) = y'. [para(182(a,1),342(a,1,2)),rewrite([370(4),396(5),404(3)])].

429 (x' * y) / x = x' * (y * x'). [para(28(a,1),353(a,1,2))].

439 (x \ y) / x' = x * (y / x). [para(387(a,1),5(a,1,2)),rewrite([105(2)]),flip(a)].

445 (x' \ y) / x = x' * (y / x'). [para(28(a,1),439(a,1,2))].

464 x * (x' * ((x \ y) * x')) = x' * (y / x). [para(182(a,1),51(a,1,2)),flip(a)].

466 x * (x' * ((x \ y) / x)) = x' * (y * x'). [para(234(a,1),51(a,1,2)),flip(a)].

474 x * (x * (x' * y)) = x' \ y. [para(28(a,1),170(a,1,2,1)),rewrite([28(3),51(4),51(3)])].

483 x \ (x' * y) = x' * (x \ y). [para(170(a,1),51(a,1,2)),rewrite([170(10)]),flip(a)].

486 (x * x) * (x' * (x' * (y / x))) = y * x'. [para(11(a,1),225(a,1,2)),rewrite([323(6),28(5)])].

499 (x * (y * y))' = x' * (y' * y'). [para(295(a,1),5(a,1,2)),rewrite([219(3)]),flip(a)].

512 x' * (x' * (y * x)) = y / x. [para(6(a,1),307(a,1,1)),flip(a)].

528 (x * y) * (x * z) = x * ((y / x') * z). [para(396(a,1),11(a,2,2,1)),rewrite([323(4),6(4)])].

532 (x / y') / y = (x * y') * y. [para(396(a,1),54(a,1,1)),rewrite([175(8),42(8)])].

534 x * (x * ((y * x') * x)) = (y / x') * x. [para(396(a,1),323(a,1,1)),rewrite([353(8)]),flip(a)].

573 ((x * y) * y') / y = ((x / y) * y') * y. [para(404(a,1),404(a,1,1)),rewrite([28(5),28(9)])].

654 ((x * y') * y) / y' = ((x / y') * y) * y'. [para(532(a,1),404(a,1,1))].

687 x \ ((y * x) * z) = (x * y) * (x \ z). [para(30(a,1),5(a,1,2))].

696 (x / y') * y = (y * y) * x. [para(16(a,1),30(a,1,2)),rewrite([305(3),534(5)])].

704 x * ((y * y) * (x \ z)) = (y * y) * z. [para(80(a,1),30(a,1,2,1)),rewrite([233(8)])].

722 x * ((x \ y) * (x \ z)) = (y / x) * z. [para(170(a,1),30(a,1,2,1)),rewrite([253(9),54(9),28(8),512(9)])].

752 ((x * x) * y) / x = y / x'. [para(696(a,1),6(a,1,1))].

754 (x * x) * (y * x') = y * x. [para(6(a,1),696(a,1,1)),flip(a)].

766 (x * x) * (y * (x * x)) = x * (x * (x * (x * y))). [para(696(a,2),12(a,2,2)),rewrite([16(4,R),340(9),307(8),28(6),28(6)])].

769 (x / y') * y = x * (y * y). [para(696(a,2),16(a,1))].

778 (x * x) * (x' * y) = x' * ((y * x) / x'). [para(54(a,1),696(a,1,1)),rewrite([28(3),253(4)]),flip(a)].

783 (x * y') / y = x * (y' * y'). [para(696(a,2),182(a,1)),rewrite([219(2),215(6),16(8,R),766(8),54(10),28(9),253(8),54(8),28(7),253(6),42(8),253(7),54(7),28(6),512(7),223(5)])].

784 (x * x) * (y * y) = x * (x * (y * y)). [para(192(a,1),696(a,1,1)),rewrite([28(3),12(3)]),flip(a)].

796 (x * x) * ((x * x) * y) = x * (x * (x * (x * y))). [para(696(a,2),323(a,2)),rewrite([16(4,R),215(6),223(8),28(6),28(6),769(9),16(8,R),766(8)])].

809 x * (x * ((x' * x') * y)) = (y * x) * x'. [para(696(a,1),396(a,1,2,2)),rewrite([28(8),404(9)])].

810 ((x * y) * y') * y = (y * y) * (x / y). [para(404(a,1),696(a,1,1))].

812 x' * (x' * ((x * x) * y)) = (y * x') * x. [para(696(a,1),512(a,1,2,2)),rewrite([532(9)])].

818 (x * y) / y' = (y * y) * x. [para(696(a,2),30(a,1,2)),rewrite([439(3),323(3),404(3),396(5)])].

835 (x * (y * y)) * y' = x * y. [back_rewrite(654),rewrite([818(5),754(4),769(4)]),flip(a)].

837 ((x / y) * y') * y = x * y'. [back_rewrite(486),rewrite([778(7),253(5),404(5),54(8),28(7),810(6),812(7)])].

839 (x * y) * (y' * y') = x * y'. [back_rewrite(573),rewrite([783(4),837(9)])].

864 (x * (y * y)) / y = x / y'. [para(16(a,1),752(a,1,1))].

866 (x * (y' * y')) / y = y' * (y' * (x * y')). [para(182(a,1),752(a,1,1)),rewrite([223(2),219(7),215(11),16(13,R),766(13),54(15),28(14),253(13),54(13),28(12),253(11),42(13)])].

886 (x * y') \ (x * y) = y * y. [para(754(a,1),105(a,1,2)),rewrite([192(10),80(12)])].

891 (x' * (y * (y * (y * (y * x'))))) * (x * (x * (y' * y'))) = y * y. [para(188(a,1),754(a,2)),rewrite([528(7),28(4),192(3),16(6,R),796(6),499(11),28(9)])].

942 x * (x * (y * (x' * x'))) = (y * x) * x'. [para(769(a,1),396(a,1,2,2)),rewrite([28(8),404(9)])].

943 (x * x) * (y / x) = y / x'. [para(404(a,1),769(a,1,1)),rewrite([810(4),47(6),128(5),396(7)])].

946 (x * (y' * y')) * y = x * y'. [para(769(a,1),532(a,2,1)),rewrite([28(2),404(3),783(4),839(5)]),flip(a)].

958 x / (y \ x)' = (x / y) * x. [para(4(a,1),818(a,1,1)),rewrite([16(7),722(7)])].

959 ((x * x) * y) * x' = y * x. [para(818(a,1),7(a,1,1))].

961 ((x * x) * y) \ (y * x) = x'. [para(818(a,1),23(a,1,1))].

962 (x * y') * y = (x * y) * y'. [para(818(a,1),42(a,1,2,2)),rewrite([812(6)])].

1061 (x / y') / (x / y) = y * y. [para(943(a,1),6(a,1,1))].

1065 (x / y') * (x / y) = (x / y) * (x / y'). [para(943(a,1),12(a,1,1)),rewrite([47(8),128(7),396(9)])].

1084 (x / (x / y)) * x = x / y'. [para(23(a,1),958(a,1,2,1)),flip(a)].

1145 (x * (x * (y * y))) \ ((x * x) * y) = y'. [para(16(a,2),961(a,1,1)),rewrite([784(3)])].

1199 ((x / y) * x) / y = (y \ x) * (y \ x). [para(22(a,1),1061(a,1,2)),rewrite([958(3)])].

1209 (x * x) * (y / x')' = (y / x)'. [para(1061(a,1),418(a,1,2)),rewrite([1065(4),175(7),1061(5),47(3),128(2),396(4),203(4)])].

1225 (x / (x / y)) \ (x / y') = x. [para(1084(a,1),5(a,1,2))].

1248 (x / (x / y)) / x = x' * (x' * (x / y')). [para(1084(a,1),512(a,1,2,2)),flip(a)].

1253 (x' / (x' / y)) * x = (x * x) * (x' / y'). [para(1084(a,1),754(a,1,2)),flip(a)].

1260 (x / (x / y')) \ (x / y) = x. [para(28(a,1),1225(a,1,2,2))].

1280 (x / y) / x = x / (x / y'). [para(1260(a,1),22(a,1,2))].

1293 x / (x / (x / y)') = x' * (x' * (x / y')). [back_rewrite(1248),rewrite([1280(3)])].

1314 (x' / y) * (x * x) = (x * x) * (x' / y). [para(1280(a,1),769(a,1,1)),rewrite([1253(6),28(4)]),flip(a)].

1358 (x / y) * (y' * y') = y' * (y' * (x * y')). [para(769(a,1),783(a,1,1)),rewrite([866(5),28(8)]),flip(a)].

1370 (x * y') / (x * y) = y' * y'. [para(839(a,1),54(a,1,1)),rewrite([80(12)])].

1394 (x / (x / y)) * x' = (x / y') * (x' * x'). [para(1084(a,1),839(a,1,1)),flip(a)].

1413 x * ((x * (y * (x' * x'))) * z) = (y * x') * (x * z). [para(946(a,1),11(a,1,1)),flip(a)].

1480 (x / y')' * y = (x / y)' * y'. [para(1209(a,1),959(a,1,1)),flip(a)].

1496 (x * y) \ (y * z) = y * ((y * x) \ z). [para(4(a,1),31(a,1,2,2))].

1497 (x * y) \ y = y * (y * x)'. [para(9(a,1),31(a,1,2,2)),rewrite([3(3)])].

1539 x * (x * (y / x))' = y \ x. [para(7(a,1),1497(a,1,1)),flip(a)].

1557 (x / y) \ y = y * (y \ x)'. [para(170(a,1),1497(a,2,2,1)),rewrite([253(5),54(5),28(4),512(5)])].

1560 (x * y) \ x = x * (y / x')'. [para(396(a,1),1497(a,2,2,1)),rewrite([323(4),6(4)])].

1571 x / (x * (x * y)')' = (x / (y * x)) * x. [para(1497(a,1),958(a,1,2,1))].

1592 (x * (y / x))' = x \ (y \ x). [para(1539(a,1),5(a,1,2)),flip(a)].

1646 ((x * x) * y) \ x' = x' * ((x' \ y) / x')'. [para(384(a,1),1557(a,2,2,1)),rewrite([818(3)])].

1653 x * (x \ (x / y))' = x / y'. [para(1280(a,1),1557(a,1,1)),rewrite([23(4)]),flip(a)].

1656 (x \ (y \ x))' = x * (y / x). [para(1592(a,1),28(a,1,1))].

1714 (x * x) * (y * x)' = (y * x')'. [para(886(a,1),1592(a,2,2)),rewrite([1370(5),839(5),203(6)]),flip(a)].

1741 x * (x / (x / y')) = (x \ y)'. [para(23(a,1),1656(a,1,1,2)),rewrite([1280(4)]),flip(a)].

1829 x / (x * (y / x')')' = (x / (x * y)) * x. [para(1560(a,1),958(a,1,2,1))].

1836 (x \ (x / y))' = x \ (x / y'). [para(1653(a,1),5(a,1,2)),flip(a)].

1839 (x / y) * x = x * (x \ y)'. [para(22(a,1),1653(a,1,2,1,2)),rewrite([958(6)]),flip(a)].

1871 x / (x * (y / x')')' = x * y'. [back_rewrite(1829),rewrite([1839(9),5(8)])].

1878 x / (x * (x * y)')' = y \ x. [back_rewrite(1571),rewrite([1839(8),105(7),1592(8),4(8)])].

1892 (x * (x \ y)') / y = (y \ x) * (y \ x). [back_rewrite(1199),rewrite([1839(2)])].

1942 (x / y) \ (x * (x \ y)') = x. [para(1839(a,1),5(a,1,2))].

1943 x * ((x \ y)' * x') = x / y. [para(1839(a,1),6(a,1,1)),rewrite([54(4)])].

1995 (x / (y * x)) \ (y \ x) = x. [para(105(a,1),1942(a,1,2,2,1)),rewrite([1592(5),4(5)])].

2024 (x \ y) / y = y / (x * y). [para(1995(a,1),22(a,1,2))].

2110 (x' / (y * x')) * x = (y \ x') * (x * x). [para(2024(a,1),769(a,1,1))].

2114 (x \ y') / y = y' / (x * y). [para(959(a,1),2024(a,2,2)),rewrite([1646(4),54(9),28(8),1480(7),445(4),1592(6),128(7),28(6),512(7)])].

2159 x * (x / (x / y)) = (x \ y')'. [para(28(a,1),1741(a,1,2,2,2))].

2161 x * ((x / y) * (x' * x')) = (x \ y)' / x. [para(1741(a,1),54(a,1,1)),rewrite([1394(8),28(5)]),flip(a)].

2163 x \ (x / y) = (x \ y)' * x'. [para(1741(a,1),175(a,1,1)),rewrite([1280(8),1293(9),28(8),170(10)]),flip(a)].

2223 ((x \ y)' * x')' = (x \ y')' * x'. [back_rewrite(1836),rewrite([2163(2),2163(8)])].

2239 x / (x * y) = x * (y' * x'). [para(5(a,1),1943(a,1,2,1,1)),flip(a)].

2258 x * (x' * ((x \ y)' * x')) = x' * (x / y). [para(1943(a,1),51(a,1,2)),flip(a)].

2379 (x * x) * (x' / (y * x)) = x' / (y * x'). [para(2114(a,1),943(a,1,2)),rewrite([2024(9)])].

2445 x * (x' * (x / (x / y))) = x' * (x \ y')'. [para(2159(a,1),51(a,1,2)),flip(a)].

2560 x * ((x * (y * x'))' * x') = x / (y / x'). [para(396(a,1),2239(a,1,2)),flip(a)].

2566 x * ((y' * x') * ((x' \ y) * (x' \ y))) = x / (x * y)'. [para(2239(a,1),943(a,1,2)),rewrite([528(3),1839(3),528(10),1892(6),16(9)])].

2678 (x' * x') * (x \ (y \ x)) = (x * (y / x'))'. [para(175(a,1),1714(a,1,2,1)),rewrite([1592(6),28(9),323(8)])].

2764 x \ (y * (x * z)) = (x * (y / x)) * z. [para(33(a,1),5(a,1,2))].

2765 (x * (y * z)) / ((y * (x / y)) * z) = y. [para(33(a,1),6(a,1,1))].

2771 (x * y) * (z * z) = x * ((z * z) * y). [para(33(a,1),16(a,1)),rewrite([223(6),225(9)]),flip(a)].

2804 x' * ((x' * ((y * x) * x')) * z) = (y / x) * (x' * z). [para(404(a,1),33(a,1,2,1,2))].

2815 x * ((x * (x' * (y * x'))) * z) = (x' * y) * (x * z). [para(429(a,1),33(a,1,2,1,2))].

2857 x * (y * (y' * (y \ x')')) = x / (x * y)'. [back_rewrite(2566),rewrite([2771(9),16(8),722(8),1839(4),51(6)])].

3349 x \ ((y * y) * z) = (y * y) * (x \ z). [para(80(a,1),687(a,2,1)),rewrite([962(4),252(4)])].

3389 (x * (y * y)) * (x \ y') = y. [para(959(a,1),687(a,1,2)),rewrite([5(2)]),flip(a)].

3445 (x * x) * ((x * (x * (y * y))) \ y) = y'. [back_rewrite(1145),rewrite([3349(6)])].

3476 x / (y \ x') = y * (x * x). [para(3389(a,1),6(a,1,1))].

3486 ((x * x) * y) * (y \ x') = x. [para(16(a,2),3389(a,1,1))].

3544 (x' / y) * (x * x) = x / y. [para(23(a,1),3476(a,1,2)),flip(a)].

3575 (x * x) * (x' / y) = x / y. [back_rewrite(1314),rewrite([3544(4)]),flip(a)].

3578 x' / (y * x') = x / (y * x). [back_rewrite(2379),rewrite([3575(5)]),flip(a)].

3594 (x \ y') * (y * y) = x \ y. [back_rewrite(2110),rewrite([3578(4),1839(3),105(2),1592(3),4(3)]),flip(a)].

3599 (x \ y') * ((x \ y') * ((y * y) * x)) = y * (x \ y'). [para(3486(a,1),12(a,1,1)),flip(a)].

3636 (x / y) * (x' * x') = x' / y. [para(3544(a,1),6(a,1,1)),rewrite([223(3)])].

3660 (x' / y) * x = (x / y) * x'. [para(3544(a,1),835(a,1,1)),flip(a)].

3685 (x \ y)' / x = x * (x' / y). [back_rewrite(2161),rewrite([3636(5)]),flip(a)].

3752 (x \ y') * ((x \ y') * ((y * y) * z)) = (z * (x \ y')) * (x \ y). [para(3594(a,1),11(a,1,2)),rewrite([2771(12)]),flip(a)].

3755 (x' / y) \ x = y * (x * x). [para(23(a,1),3594(a,1,1)),flip(a)].

3762 (x * x) * (y \ x)' = (y \ x')'. [para(3594(a,1),242(a,1,1)),rewrite([192(7),80(9),203(3)])].

3806 x' * (y \ x) = x * (y \ x'). [back_rewrite(3599),rewrite([3752(8),4(3)])].

3830 (x / y) \ x' = y * (x' * x'). [para(28(a,1),3755(a,1,1,1))].

3831 x / (y * (x * x)) = x' / y. [para(3755(a,1),22(a,1,2))].

3841 (x * ((y * x) * x'))' = x * ((x' / y) / x). [para(3755(a,1),1656(a,1,1,2)),rewrite([2764(3),323(3),404(3)])].

3846 x / ((x / y) * x') = y / x'. [para(3755(a,1),2024(a,1,1)),rewrite([864(3),3660(5)]),flip(a)].

3939 x' / (x' / y) = x / (x / y). [para(3544(a,1),3831(a,1,2)),flip(a)].

4007 (x \ y)' * (x' * x') = x * ((x' / y) / x). [para(3660(a,1),105(a,1,2)),rewrite([301(4),2163(2),783(5)])].

4085 x * ((x' / y') / x) = x * (x' / (x / y)). [para(2163(a,1),3685(a,1,1,1)),rewrite([2223(5),783(6),4007(7)])].

4110 x * (y * (x' * x')) = x' * y. [para(23(a,1),3806(a,1,2)),rewrite([3830(5)]),flip(a)].

4111 x' * (y * (x * x)) = x * y. [para(23(a,1),3806(a,2,2)),rewrite([3755(4)])].

4184 (x * y') * (y * z) = y * ((y' * x) * z). [back_rewrite(1413),rewrite([4110(5)]),flip(a)].

4188 (x * y) * y' = y * (y' * x). [back_rewrite(942),rewrite([4110(5)]),flip(a)].

4282 x * ((x' / y) / x) = (x' \ y)'. [back_rewrite(3841),rewrite([4188(3),474(4)]),flip(a)].

4296 (x / y) * (y' * z) = y' * ((y \ x) * z). [back_rewrite(2804),rewrite([4188(5),51(6),170(6)]),flip(a)].

4366 x * (x * ((x' * x') * y)) = x * (x' * y). [back_rewrite(809),rewrite([4188(9)])].

4416 x * (x' / (x / y)) = (x' \ y')'. [back_rewrite(4085),rewrite([4282(5)]),flip(a)].

4453 x' * ((x \ y) * x') = x' * (x' * (y * x')). [back_rewrite(1358),rewrite([4296(5)])].

4478 (x \ y) / x = x' * (y / x). [back_rewrite(464),rewrite([4453(5),170(7),301(3)])].

4590 (x \ y) * x' = x' * (y * x'). [back_rewrite(466),rewrite([4478(3),170(6),258(2)])].

4594 x \ (y * x') = x' * (y / x). [back_rewrite(301),rewrite([4478(5)])].

4676 x * (x' * (y * x')) = y / x. [back_rewrite(182),rewrite([4590(3)])].

4693 (x' * y) * (x * z) = x * ((y / x) * z). [back_rewrite(2815),rewrite([4676(5)]),flip(a)].

4694 x' * (x / y) = x * (x' / y). [back_rewrite(2258),rewrite([4676(7),3685(3)]),flip(a)].

4780 x * (y * (y' \ x')) = y * y. [back_rewrite(891),rewrite([4693(13),47(11),16(10,R),704(11),4184(9),4184(8),4184(7),4184(6),4366(7),474(5)])].

4796 x' * (x \ y')' = x * (x' \ y')'. [back_rewrite(2445),rewrite([4694(4),4416(4)]),flip(a)].

4800 x * (y * (y * (y' \ x')')) = x / (x * y)'. [back_rewrite(2857),rewrite([4796(5)])].

4812 x' * (y / x') = x * (y / x). [para(4111(a,1),323(a,1,1)),rewrite([175(3),28(7),864(6)]),flip(a)].

4816 x' * (y * x) = x * (y * x'). [para(4111(a,1),353(a,1,1)),rewrite([28(3),54(2),835(8)]),flip(a)].

4819 x * ((x' * x') * y) = x' * y. [para(253(a,1),4111(a,1,2)),rewrite([215(3),215(6),223(8),28(6),28(6),251(7),215(4)]),flip(a)].

4847 (x * x) * y = x * (x' \ y). [para(118(a,2),4111(a,1,2)),rewrite([215(2),766(7),4184(8),4184(7),4184(6),4184(5),4819(5),474(4)]),flip(a)].

4875 (x' * y) * x = x * (y / x). [back_rewrite(253),rewrite([4812(7)])].

5024 x * (x' \ (y \ x)') = (y \ x')'. [back_rewrite(3762),rewrite([4847(4)])].

5090 x * (x' \ ((x * (x * (y * y))) \ y)) = y'. [back_rewrite(3445),rewrite([4847(6)])].

5335 (x * (y / x'))' = x \ (y \ x'). [back_rewrite(2678),rewrite([4847(6),28(3),322(4),3806(5),51(6),51(7),170(7)]),flip(a)].

5389 x * (x' \ (y / x')') = (y / x)'. [back_rewrite(1209),rewrite([4847(5)])].

5447 x \ (y * y) = y * (y' \ x'). [back_rewrite(203),rewrite([4847(5)])].

5448 (x * x) / y = x * (x' \ y'). [back_rewrite(192),rewrite([4847(5)])].

5613 (x * (x' \ y')) * y = x * x. [para(4847(a,1),128(a,2,2)),rewrite([5447(2),4780(10)])].

5619 (x * (x' \ y')) / y = x * (y' * (y \ x)). [para(4847(a,1),783(a,1,1)),rewrite([4847(10),5447(10),28(8),28(8)])].

5912 (x' / y) / x = x' / (x / y'). [para(3939(a,1),3846(a,1,2,1)),rewrite([28(5),1839(4),2163(3),2223(6),1943(7),28(8)]),flip(a)].

6551 x' * (x \ (x' * y)') = (x * y)'. [para(6(a,1),5335(a,1,1,2)),rewrite([1497(6),483(8)]),flip(a)].

6913 (x * (y * x'))' * x' = (x * (y * x))' * x. [para(54(a,1),1480(a,2,1,1)),rewrite([353(3)]),flip(a)].

6954 x * ((x * (y * x))' * x) = x / (y / x'). [back_rewrite(2560),rewrite([6913(6)])].

6996 (x / y') \ (y * z) = y * ((y' \ x) \ z). [para(474(a,1),1496(a,2,2,1)),rewrite([323(4),54(4),28(3),4816(3),396(4)])].

7176 x * (x' \ y')' = x * (y * x'). [back_rewrite(406),rewrite([6996(5),5447(4),5024(6)])].

7241 x / (x * y)' = x * (x / y'). [back_rewrite(4800),rewrite([7176(5),396(4)]),flip(a)].

7266 x \ y = x' / y'. [back_rewrite(1878),rewrite([7241(5),28(3),2239(2),396(5)]),flip(a)].

7268 x * (x / (y / x')) = x * y'. [back_rewrite(1871),rewrite([7241(6),28(4)])].

7886 (x * y)' = y' / x. [back_rewrite(6551),rewrite([7266(5),28(6),2239(5),28(5),4816(5),51(6),4676(6)]),flip(a)].

8391 (x * (x / y)) / y = x * (y' * (y' / x')). [back_rewrite(5619),rewrite([7266(3),28(2),28(2),7266(5)])].

8394 (x * (x / y)) * y = x * x. [back_rewrite(5613),rewrite([7266(3),28(2),28(2)])].

8459 (x * x) / y = x * (x / y). [back_rewrite(5448),rewrite([7266(5),28(4),28(4)])].

8500 (x / y)' = y * x'. [back_rewrite(5389),rewrite([7266(5),28(2),28(4),7268(4)]),flip(a)].

8731 x * (x' / y) = y'. [back_rewrite(5090),rewrite([7266(5),7886(5),7886(4),215(3),8459(5),8391(6),28(6),54(9),28(8),8394(7),7266(7),28(2),7886(6),215(4),28(2),28(2),8459(3),2239(4),8500(3),12(5),170(6),7266(2),28(3)])].

8952 x' / (x / y) = x' * (y / x). [back_rewrite(4594),rewrite([7266(3),7886(4),28(3)])].

9571 x * (x' * (x' * y)) = x' / y'. [back_rewrite(170),rewrite([7266(6)])].

9643 x / (y / x') = y'. [back_rewrite(6954),rewrite([7886(3),7886(2),5912(3),8952(4),4875(5),307(3),9571(6),28(3),8731(3)]),flip(a)].

10985 (x / y) / (z / (y * x')) = z'. [para(8500(a,1),9643(a,1,2,2))].

11178 (x / (y * (z / y))) / y = (x / y) / z. [para(2765(a,1),10985(a,1,2)),rewrite([7886(8),7886(7),28(6)])].

11200 (x / (y * z)) / y = (x / y) / (z * y). [para(6(a,1),11178(a,1,1,2,2))].

11382 ((x * (y * z)) / y) / (z * y) = x / y. [para(6(a,1),11200(a,1,1)),flip(a)].

11487 (x * (y * z)) / y = (x / y) * (z * y). [para(11382(a,1),7(a,1,1)),flip(a)].

11557 ((x / y) * (z * y)) * y = x * (y * z). [para(11487(a,1),7(a,1,1))].

11711 (x * (y * z)) * z = z * ((z * x) * y) # label(non_clause) # label(goal). [para(6(a,1),11557(a,1,1,1)),rewrite([11(6)])].

11712 $F. [resolve(11711,a,17,a)].

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

============================== STATISTICS ============================

Given=207. Generated=26017. Kept=11707. proofs=1.

Usable=57. Sos=2483. Demods=2414. Limbo=0, Disabled=9179. Hints=2365.

Kept_by_rule=0, Deleted_by_rule=0.

Forward_subsumed=14310. Back_subsumed=154.

Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.

New_demodulators=11328 (1 lex), Back_demodulated=9012. Back_unit_deleted=0.

Demod_attempts=588661. Demod_rewrites=116049.

Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.

Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.

Megabytes=10.70.

User_CPU=2.00, System_CPU=0.06, Wall_clock=2.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 79425 exit (max_proofs) Thu Oct 1 13:06:02 2009

% Length of proof is 121.

% Level of proof is 29.

% Maximum clause weight is 30.

% Given clauses 113.

1 x * ((x * y) * z) = (y * (z * x)) * x # label(non_clause) # label(goal). [goal].

3 x * 1 = x. [assumption].

4 x * (x \ y) = y. [assumption].

5 x \ (x * y) = y. [assumption].

6 (x * y) / y = x. [assumption].

7 (x / y) * y = x. [assumption].

8 x' * x = 1. [assumption].

9 x * x' = 1. [assumption].

10 x * ((x * y) * z) = (y * x) * (x * z). [assumption].

11 (x * y) * (y * z) = y * ((y * x) * z). [copy(10),flip(a)].

12 (x * y) * y = y * (y * x). [assumption].

13 x * (y * z) = ((x * y) / x) * (x * z). [assumption].

14 ((x * y) / x) * (x * z) = x * (y * z). [copy(13),flip(a)].

15 x * (y * x) = (x * y) * x. [assumption].

16 (x * y) * x = x * (y * x). [copy(15),flip(a)].

17 (c2 * (c3 * c1)) * c1 != c1 * ((c1 * c2) * c3). [deny(1)].

26 1 / x = x'. [para(8(a,1),6(a,1,1))].

28 x'' = x. [para(9(a,1),6(a,1,1)),rewrite([26(3)])].

30 x * ((x * y) * (x \ z)) = (y * x) * z. [para(4(a,1),11(a,1,2)),flip(a)].

33 x * ((x * (y / x)) * z) = y * (x * z). [para(7(a,1),11(a,1,1)),flip(a)].

36 x * ((x * y) * x') = y * x. [para(9(a,1),11(a,1,2)),rewrite([3(3)]),flip(a)].

42 x * (x * (y / x)) = y * x. [para(7(a,1),12(a,1,1)),flip(a)].

46 (x / y) * (y * z) = y * ((y \ x) * z). [para(4(a,1),14(a,1,1,1))].

47 ((x * y) / x) * z = x * (y * (x \ z)). [para(4(a,1),14(a,1,2))].

49 (x * (y * z)) / (x * z) = (x * y) / x. [para(14(a,1),6(a,1,1))].

50 x' * (x * y) = x * (x' * y). [para(8(a,1),14(a,1,1,1)),rewrite([26(3),28(2)]),flip(a)].

53 (x * y) / x = x * (y * x'). [para(9(a,1),14(a,1,2)),rewrite([3(4)])].

70 (x * (y * z)) / (x * z) = x * (y * x'). [back_rewrite(49),rewrite([53(6)])].

72 (x * (y * x')) * z = x * (y * (x \ z)). [back_rewrite(47),rewrite([53(2)])].

79 x * ((y * x) * x') = x * y. [para(16(a,1),6(a,1,1)),rewrite([53(3)])].

86 x \ (y * x) = x * (y / x). [para(42(a,1),5(a,1,2))].

87 (x * y) / (y * (x / y)) = y. [para(42(a,1),6(a,1,1))].

90 (x * y) * (x * z) = x * ((y * x) * z). [para(42(a,1),11(a,2,2,1)),rewrite([16(3),7(2)])].

91 x * ((x * y) * (y / x)) = x * (y * y). [para(42(a,1),12(a,1,1)),rewrite([11(4),16(9),7(8),90(8),7(6)])].

107 x * ((y / x) / x) = x \ y. [para(7(a,1),86(a,1,2)),flip(a)].

111 x * (x * (y * x')) = y * x. [para(16(a,1),86(a,1,2)),rewrite([5(3),53(3)]),flip(a)].

115 x * (y / x) = x * (y * x'). [para(87(a,1),87(a,1,2,2)),rewrite([11(4),91(4),16(5),7(4),70(4)]),flip(a)].

121 x * ((y / x) * x') = x \ y. [back_rewrite(107),rewrite([115(3)])].

129 x \ (y * x) = x * (y * x'). [back_rewrite(86),rewrite([115(4)])].

130 x * (x * (y * (x \ z))) = y * (x * z). [back_rewrite(33),rewrite([115(2),72(4)])].

131 (x * y) * x' = x * (y * x'). [para(36(a,1),5(a,1,2)),rewrite([129(2)]),flip(a)].

137 x * ((y * x') * (x * ((y * x') * x))) = x * (y * ((y * x) * x')). [para(36(a,1),12(a,1,1)),rewrite([131(4),11(5),11(4),131(8),131(11),16(12),90(13),90(12),16(11)]),flip(a)].

141 x * ((y * x') * x) = x * y. [para(36(a,1),36(a,1,2,1)),rewrite([79(4),131(4),16(5)]),flip(a)].

143 x * ((y * x') * (x * y)) = x * (y * ((y * x) * x')). [back_rewrite(137),rewrite([141(6)])].

151 (x * y) * y' = x. [para(79(a,1),5(a,1,2)),rewrite([5(2)]),flip(a)].

155 x * ((y * x') * (x * y)) = x * (y * y). [back_rewrite(143),rewrite([151(8)])].

156 x * (y \ x)' = y. [para(4(a,1),151(a,1,1))].

157 (x * y) \ x = y'. [para(151(a,1),5(a,1,2))].

159 x / y = x * y'. [para(7(a,1),151(a,1,1)),flip(a)].

165 (x * y') * y = x. [para(28(a,1),151(a,1,2))].

175 x * (x' * (x' * y)) = x \ y. [back_rewrite(121),rewrite([159(1),12(4)])].

179 (x * y') * (y * z) = y * ((y \ x) * z). [back_rewrite(46),rewrite([159(1)])].

184 x * (x * ((x \ y) * y)) = x * (y * y). [back_rewrite(155),rewrite([179(4)])].

185 (x \ y)' = y \ x. [para(156(a,1),5(a,1,2)),flip(a)].

213 (x * (x' * y)) \ x' = (x * y)'. [para(50(a,1),157(a,1,1))].

231 x * (x * (x' * y)) = x' \ y. [para(28(a,1),175(a,1,2,1)),rewrite([28(3),50(4),50(3)])].

254 x \ ((y * x) * z) = (x * y) * (x \ z). [para(30(a,1),5(a,1,2))].

265 ((x \ y) * y) * x = y * y. [para(165(a,1),30(a,1,2)),rewrite([185(3)]),flip(a)].

268 x * ((y * x) * (x \ z)) = (x * y) * z. [para(111(a,1),30(a,1,2,1)),rewrite([16(8),165(7)])].

283 x * ((x * ((x \ y) * y)) * z) = (y * y) * (x * z). [para(265(a,1),11(a,1,1)),flip(a)].

286 (x * x) * y = y * (x * x). [para(265(a,1),12(a,1,1)),rewrite([184(6)])].

288 (x \ y) * y = (y * y) * x'. [para(265(a,1),151(a,1,1)),flip(a)].

293 ((x' \ y) * y) * x = x * (x * (y * y)). [para(265(a,1),111(a,1,2,2)),flip(a)].

299 x * ((y * y) * x') = y * y. [para(286(a,2),5(a,1,2)),rewrite([129(3)])].

302 x * ((x * x) * y) = x * (x * (x * y)). [para(286(a,1),11(a,1)),rewrite([90(3),12(2)]),flip(a)].

319 ((x * x) * y) * z = (y * (x * x)) * z. [para(286(a,1),30(a,1,2,1)),rewrite([268(7)])].

320 x * ((x \ y) * (x * x)) = (x * x) * y. [para(286(a,1),30(a,1,2))].

321 x * (y * y) = y * (y * x). [para(286(a,1),30(a,2)),rewrite([302(4),4(2)]),flip(a)].

327 (x * x) * y = x * (x * y). [back_rewrite(320),rewrite([321(3),4(2)]),flip(a)].

331 (x * (y * y)) * z = (y * (y * x)) * z. [back_rewrite(319),rewrite([327(2)]),flip(a)].

344 x * (y * (y * x')) = y * y. [back_rewrite(299),rewrite([327(3)])].

351 (x \ y) * y = y * (y * x'). [back_rewrite(288),rewrite([327(5)])].

352 x * (y * (y * z)) = y * (y * (x * z)). [back_rewrite(283),rewrite([351(2),344(4),327(2),327(6)])].

353 (x * (x * y)) * y = y * (y * (x * x)). [back_rewrite(293),rewrite([351(3),28(2)])].

361 (x * (x * y')) * y = x * x. [back_rewrite(265),rewrite([351(2)])].

384 x' * (y * (x * x)) = x' \ y. [para(321(a,2),50(a,1,2)),rewrite([50(7),231(8)])].

387 (x * (y * y)) * y' = x * y. [para(321(a,2),131(a,1,1)),rewrite([131(7),111(8)])].

423 x * (y * (y * (x \ z))) = y * (y * z). [para(344(a,1),30(a,1,2,1)),rewrite([327(3),361(8),327(6)])].

438 x \ y = x' * y. [para(351(a,1),151(a,1,1)),rewrite([131(5),131(4),111(5)]),flip(a)].

453 x * (y * (y * (x' * z))) = y * (y * z). [back_rewrite(423),rewrite([438(1)])].

464 x' * (y * (x * x)) = x * y. [back_rewrite(384),rewrite([438(6),28(6)])].

487 (x * y) * (x' * z) = x' * ((y * x) * z). [back_rewrite(254),rewrite([438(3),438(6)]),flip(a)].

505 (x * (x' * y))' * x' = (x * y)'. [back_rewrite(213),rewrite([438(5)])].

527 x * (x * (y * (x' * z))) = y * (x * z). [back_rewrite(130),rewrite([438(1)])].

535 (x * (y * x')) * z = x * (y * (x' * z)). [back_rewrite(72),rewrite([438(5)])].

540 x * (x' * y) = y. [back_rewrite(5),rewrite([438(2),50(3)])].

566 (x * y)' = y' * x'. [back_rewrite(505),rewrite([540(3)]),flip(a)].

570 x' * (x * y) = y. [back_rewrite(50),rewrite([540(6)])].

611 (x * y) * (y' * z) = y' * ((y * x) * z). [para(387(a,1),11(a,1,1)),rewrite([464(9)])].

667 x * ((y * x) * (z * (z * x'))) = (x * y) * (z * z). [para(344(a,1),90(a,1,2)),flip(a)].

668 (x * y) * (z * (z * y')) = x * (z * z). [para(344(a,1),90(a,2,2)),rewrite([566(3),453(7)])].

683 (x * y) * (z * z) = x * (y * (z * z)). [back_rewrite(667),rewrite([668(5)]),flip(a)].

717 (x * (y * (y * z))) * y = y * (y * ((x * z) * y)). [para(352(a,2),16(a,1,1)),rewrite([16(7)])].

734 (x * (y * (y * z))) * y' = (x * z) * y. [para(352(a,2),131(a,1,1)),rewrite([131(9),111(10)])].

740 x * (y * (z * z)) = x * (z * (z * y)). [para(352(a,2),321(a,2)),rewrite([683(3)])].

745 x * (y * (z * z)) = z * (z * (x * y)). [para(321(a,2),352(a,1,2))].

759 (x * (y * (y * (z * (z * (y * y)))))) * (y' * (y' * z')) = x * (y * (y * z)). [para(352(a,1),387(a,1,1,2)),rewrite([353(3),566(9),566(8),12(11)])].

818 (x * (y * (z * z))) * z' = (x * y) * z. [para(745(a,2),131(a,1,1)),rewrite([131(9),111(10)])].

889 (x * (y' * z)) * y = (x * (y * z)) * y'. [para(527(a,1),131(a,1,1)),rewrite([131(10),111(11)]),flip(a)].

891 x' * (y * (x * z)) = x * (y * (x' * z)). [para(527(a,1),540(a,1,2)),rewrite([28(7)]),flip(a)].

995 (x * (y * (z * (z * (u * u))))) * u' = (z * (z * (x * y))) * u. [para(745(a,1),818(a,2,1)),rewrite([683(4),327(3)])].

1002 (x * (y * (z * (u * u)))) * u' = (x * (y * z)) * u. [para(527(a,1),818(a,2,1)),rewrite([683(6),683(5),683(4),527(7)])].

1025 (x * (y * y)) * (y' * z) = y' * ((y * (x * y)) * z). [para(321(a,2),487(a,1,1)),rewrite([16(8)])].

1044 (x * (y * (y * z))) * (y' * u) = y' * ((y * ((x * z) * y)) * u). [para(352(a,2),487(a,1,1)),rewrite([16(10)])].

1068 x' * (x' * ((x * (x * (y * (z * (z * (x * x)))))) * z')) = y * (x * (x * z)). [back_rewrite(759),rewrite([1044(12),487(11),12(8)])].

1089 x' * (y * (y * (x * z))) = z * (y * y). [para(321(a,1),611(a,2,2)),rewrite([611(5),683(4),570(5)]),flip(a)].

2532 ((x * (y * y)) * z) * u = ((y * (y * x)) * z) * u. [para(331(a,1),818(a,1,1)),rewrite([818(7)]),flip(a)].

2534 (x * (y * (y * z))) * u = (y * (y * (x * z))) * u. [para(331(a,2),818(a,1,1,2)),rewrite([683(4),327(3),995(7)]),flip(a)].

2724 (x * (y * (y * (z * z)))) * z = z * (z * ((x * (y * y)) * z)). [para(353(a,1),818(a,1,1,2)),rewrite([327(4),327(5),734(8),717(5)]),flip(a)].

3289 x' * (x' * ((x * (x * (x * (x * (y * (z * z)))))) * z')) = y * (z * (x * x)). [para(740(a,2),387(a,2)),rewrite([90(5),16(2),90(4),12(2),353(3),566(9),566(8),12(11),1044(12),2724(6),487(11),16(8),16(7),12(6)])].

3914 x' * (x' * ((x * (x * y)) * z)) = y * z. [para(668(a,1),151(a,1,1)),rewrite([566(6),566(5),28(4),12(6),1025(7),487(6),12(4)])].

3997 (x * (x * y)) * z = y * (z * (x * x)). [back_rewrite(3289),rewrite([3914(12),1002(6)])].

4006 (x * (y * y)) * z = x * (y * (y * z)). [back_rewrite(1068),rewrite([3997(10),1044(10),321(9),1089(10),321(7),570(8),570(6)])].

4372 (x * (y * (y * z))) * u = (x * z) * (u * (y * y)). [back_rewrite(2534),rewrite([3997(8)])].

4373 (x * (y * (z * z))) * u = (x * y) * (u * (z * z)). [back_rewrite(2532),rewrite([4006(3),4372(4),3997(7)]),flip(a)].

4767 (x * (y * x)) * z = x * (y * (x * z)). [para(111(a,1),3997(a,1,1,2)),rewrite([535(9),891(7),8(5),3(5)])].

5499 (x * (y * (x * z))) * z' = x * (y * x). [para(4767(a,1),151(a,1,1))].

7654 (x * y) * (z * x) = x * ((y * z) * x). [para(668(a,1),5499(a,1,1,2)),rewrite([566(6),28(5),4373(6),321(5),111(5)])].

8431 (x * (y * z)) * y = (x * y) * (z * y). [para(111(a,1),7654(a,1,1)),rewrite([535(7),16(8),889(7),111(9)]),flip(a)].

9168 (x * (y * z)) * z = z * ((z * x) * y) # label(non_clause) # label(goal). [para(111(a,1),8431(a,1,1,2)),rewrite([16(8),165(7),11(6)])].

9169 $F. [resolve(9168,a,17,a)].

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

============================== STATISTICS ============================

Given=113. Generated=25852. Kept=9164. proofs=1.

Usable=68. Sos=3363. Demods=2681. Limbo=15, Disabled=5730. Hints=262.

Kept_by_rule=0, Deleted_by_rule=0.

Forward_subsumed=16688. Back_subsumed=364.

Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.

New_demodulators=7508 (2 lex), Back_demodulated=5353. Back_unit_deleted=0.

Demod_attempts=741473. Demod_rewrites=123222.

Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.

Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.

Megabytes=10.09.

User_CPU=3.08, System_CPU=0.05, Wall_clock=3.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 3523 exit (max_proofs) Tue Oct 6 14:53:42 2009

% Length of proof is 68.

% Level of proof is 23.

% Maximum clause weight is 20.

% Given clauses 54.

1 x * ((x * y) * z) = (y * (z * x)) * x # label(non_clause) # label(goal). [goal].

3 x * 1 = x. [assumption].

4 x * (x \ y) = y. [assumption].

5 x \ (x * y) = y. [assumption].

6 (x * y) / y = x. [assumption].

7 (x / y) * y = x. [assumption].

8 x' * x = 1. [assumption].

9 x * x' = 1. [assumption].

10 x * ((x * y) * z) = (y * x) * (x * z). [assumption].

11 (x * y) * (y * z) = y * ((y * x) * z). [copy(10),flip(a)].

12 (x * y) * y = y * (y * x). [assumption].

13 x * (y * z) = ((x * y) / x) * (x * z). [assumption].

14 ((x * y) / x) * (x * z) = x * (y * z). [copy(13),flip(a)].

15 (x * y) * y = x * (y * y). [assumption].

16 x * (y * y) = y * (y * x). [copy(15),rewrite([12(2)]),flip(a)].

17 (c2 * (c3 * c1)) * c1 != c1 * ((c1 * c2) * c3). [deny(1)].

19 x \ x = 1. [para(3(a,1),5(a,1,2))].

26 1 / x = x'. [para(8(a,1),6(a,1,1))].

28 x'' = x. [para(9(a,1),6(a,1,1)),rewrite([26(3)])].

31 (x * y) \ (y * ((y * x) * z)) = y * z. [para(11(a,1),5(a,1,2))].

33 x * ((x * (y / x)) * z) = y * (x * z). [para(7(a,1),11(a,1,1)),flip(a)].

42 x * (x * (y / x)) = y * x. [para(7(a,1),12(a,1,1)),flip(a)].

48 ((x * y) / x) * z = x * (y * (x \ z)). [para(4(a,1),14(a,1,2))].

51 x' * (x * y) = x * (x' * y). [para(8(a,1),14(a,1,1,1)),rewrite([26(3),28(2)]),flip(a)].

54 (x * y) / x = x * (y * x'). [para(9(a,1),14(a,1,2)),rewrite([3(4)])].

73 (x * (y * x')) * z = x * (y * (x \ z)). [back_rewrite(48),rewrite([54(2)])].

80 (x * (x * y)) / (x * x) = y. [para(16(a,1),6(a,1,1))].

85 x * (x' * x') = x'. [para(8(a,1),16(a,2,2)),rewrite([3(7)])].

119 x * (x * (x' * (x' * y))) = (y * x) * x'. [para(85(a,1),11(a,1,2)),rewrite([16(8),51(7),51(8)]),flip(a)].

135 x \ (y * x) = x * (y / x). [para(42(a,1),5(a,1,2))].

142 (x * y) / (x * x) = x \ y. [para(4(a,1),80(a,1,1,2))].

147 (x * y) / (y * y) = x / y. [para(42(a,1),80(a,1,1))].

154 (x * y) \ (y * (x * x)) = (x * y) * (x / (x * y)). [para(16(a,2),135(a,1,2))].

165 (x / y) / y = x / (y * y). [para(7(a,1),147(a,1,1)),flip(a)].

176 x * (x' * (x' * y)) = x \ y. [para(142(a,1),165(a,2)),rewrite([54(2),54(4),12(4)])].

180 (x * y) * y' = x. [back_rewrite(119),rewrite([176(5),4(2)]),flip(a)].

183 (x * y) \ x = y'. [para(180(a,1),5(a,1,2))].

185 x / y = x * y'. [para(7(a,1),180(a,1,1)),flip(a)].

193 (x * y') * y = x. [para(28(a,1),180(a,1,2))].

214 (x * y) \ (y * (x * x)) = (x * y) * (x * (x * y)'). [back_rewrite(154),rewrite([185(7)])].

221 x \ (y * x) = x * (y * x'). [back_rewrite(135),rewrite([185(3)])].

224 (x * y) * x' = x * (y * x'). [back_rewrite(54),rewrite([185(2)])].

226 x * (x * (y * x')) = y * x. [back_rewrite(42),rewrite([185(1)])].

228 x * (x * (y * (x \ z))) = y * (x * z). [back_rewrite(33),rewrite([185(1),73(4)])].

236 (x * y) * (x * z) = x * ((y * x) * z). [para(226(a,1),11(a,2,2,1)),rewrite([73(4),19(1),3(2)])].

238 (x * y) * x = x * (y * x). [para(226(a,1),12(a,2,2)),rewrite([73(4),19(1),3(2)])].

244 (x * y) \ (y * (x * x)) = x * ((y * x) * (x * y)'). [back_rewrite(214),rewrite([236(9)])].

261 x * ((x \ y) * x) = y * x. [para(4(a,1),238(a,1,1)),flip(a)].

277 (x \ y) * x = x * (y * x'). [para(261(a,1),5(a,1,2)),rewrite([221(2)]),flip(a)].

285 x * ((y * x) * (x * y)') = y' * (x * y). [para(183(a,1),277(a,1,1)),rewrite([236(8)]),flip(a)].

289 (x * y) \ (y * (x * x)) = y' * (x * y). [back_rewrite(244),rewrite([285(9)])].

303 (x * (x' * y)) \ x' = (x * y)'. [para(51(a,1),183(a,1,1))].

396 (x * y) \ (y * z) = y * ((y * x) \ z). [para(4(a,1),31(a,1,2,2))].

416 x' * (y * x) = x * (y * x'). [back_rewrite(289),rewrite([396(4),396(3),183(2)]),flip(a)].

456 x \ y = x' * y. [para(12(a,1),416(a,2,2)),rewrite([193(4),176(7)]),flip(a)].

527 (x * (x' * y))' * x' = (x * y)'. [back_rewrite(303),rewrite([456(5)])].

543 x * (x * (y * (x' * z))) = y * (x * z). [back_rewrite(228),rewrite([456(1)])].

551 (x * (y * x')) * z = x * (y * (x' * z)). [back_rewrite(73),rewrite([456(5)])].

553 x * (x' * y) = y. [back_rewrite(5),rewrite([456(2),51(3)])].

573 (x * y)' = y' * x'. [back_rewrite(527),rewrite([553(3)]),flip(a)].

681 x * (x * (y * (z * x'))) = y * (z * x). [para(226(a,1),543(a,1,2,2,2)),rewrite([28(8),416(8),226(9)])].

686 (x * (y' * z)) * y = (x * (y * z)) * y'. [para(543(a,1),224(a,1,1)),rewrite([224(10),226(11)]),flip(a)].

724 (x * (y * z')) * (z * y) = y * (y * x). [para(193(a,1),681(a,1,2,2)),rewrite([573(5),28(4)]),flip(a)].

765 (x * (y * z')) * (z * x) = x * (y * x). [para(226(a,1),724(a,2,2)),rewrite([236(6),193(3)])].

801 (x * y) * (z * x) = x * ((y * z) * x). [para(180(a,1),765(a,1,1,2))].

871 (x * (y * z)) * y = (x * y) * (z * y). [para(226(a,1),801(a,1,1)),rewrite([551(7),238(8),686(7),226(9)]),flip(a)].

954 (x * (y * z)) * z = z * ((z * x) * y) # label(non_clause) # label(goal). [para(226(a,1),871(a,1,1,2)),rewrite([238(8),193(7),11(6)])].

955 $F. [resolve(954,a,17,a)].

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

============================== STATISTICS ============================

Given=54. Generated=2429. Kept=950. proofs=1.

Usable=24. Sos=293. Demods=305. Limbo=24, Disabled=621. Hints=165.

Kept_by_rule=0, Deleted_by_rule=0.

Forward_subsumed=1479. Back_subsumed=39.

Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.

New_demodulators=901 (1 lex), Back_demodulated=569. Back_unit_deleted=0.

Demod_attempts=36472. Demod_rewrites=6211.

Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.

Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.

Megabytes=0.85.

User_CPU=0.11, System_CPU=0.01, Wall_clock=0.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 3543 exit (max_proofs) Tue Oct 6 14:55:23 2009

% Length of proof is 27.

% Level of proof is 10.

% Maximum clause weight is 17.

% Given clauses 30.

1 x * ((x * y) * z) = (y * (z * x)) * x # label(non_clause) # label(goal). [goal].

4 x * (x \ y) = y. [assumption].

5 x \ (x * y) = y. [assumption].

6 (x * y) / y = x. [assumption].

7 (x / y) * y = x. [assumption].

8 x' * x = 1. [assumption].

9 x * x' = 1. [assumption].

10 x * ((x * y) * z) = (y * x) * (x * z). [assumption].

11 (x * y) * (y * z) = y * ((y * x) * z). [copy(10),flip(a)].

15 x * (y * x)' = y'. [assumption].

16 (c2 * (c3 * c1)) * c1 != c1 * ((c1 * c2) * c3). [deny(1)].

25 1 / x = x'. [para(8(a,1),6(a,1,1))].

27 x'' = x. [para(9(a,1),6(a,1,1)),rewrite([25(3)])].

32 x * ((x * (y / x)) * z) = y * (x * z). [para(7(a,1),11(a,1,1)),flip(a)].

77 (x \ y) * y' = x'. [para(4(a,1),15(a,1,2,1))].

78 (x * y)' = y \ x'. [para(15(a,1),5(a,1,2)),flip(a)].

87 x \ y = x' / y'. [para(77(a,1),6(a,1,1)),flip(a)].

93 (x * y)' = y' / x. [back_rewrite(78),rewrite([87(4),27(5)])].

107 (x * (y * z)) / ((y * (x / y)) * z) = y. [para(32(a,1),6(a,1,1))].

117 x / ((y * ((x / (y * z)) / y)) * z) = y. [para(7(a,1),107(a,1,1))].

141 (x' / (y * z)) / y = (x' / y) / (z * y). [para(11(a,1),93(a,1,1)),rewrite([93(4),93(3),93(6)])].

151 (x / (y * z)) / y = (x / y) / (z * y). [para(27(a,1),141(a,1,1,1)),rewrite([27(5)])].

161 x / ((y * ((x / y) / (z * y))) * z) = y. [back_rewrite(117),rewrite([151(3)])].

173 (x * y) / ((y * (x / (z * y))) * z) = y. [para(6(a,1),161(a,1,2,1,2,1))].

184 ((x * (y * z)) * z) / ((z * x) * y) = z. [para(6(a,1),173(a,1,2,1,2))].

204 (x * (y * z)) * z = z * ((z * x) * y) # label(non_clause) # label(goal). [para(184(a,1),7(a,1,1)),flip(a)].

205 $F. [resolve(204,a,16,a)].

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

============================== STATISTICS ============================

Given=30. Generated=548. Kept=201. proofs=1.

Usable=23. Sos=100. Demods=120. Limbo=0, Disabled=90. Hints=36.

Kept_by_rule=0, Deleted_by_rule=0.

Forward_subsumed=347. Back_subsumed=11.

Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.

New_demodulators=197 (0 lex), Back_demodulated=66. Back_unit_deleted=0.

Demod_attempts=6503. Demod_rewrites=1055.

Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.

Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.

Megabytes=0.31.

User_CPU=0.02, System_CPU=0.00, Wall_clock=0.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 3551 exit (max_proofs) Tue Oct 6 14:56:25 2009