% Length of proof is 430.

% Level of proof is 56.

% Maximum clause weight is 31.

% Given clauses 316.

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

2 1 * x = x. [assumption].

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 * y) * z) = (y * (z * x)) * x. [assumption].

9 (x * (y * z)) * z = z * ((z * x) * y). [copy(8),flip(a)].

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

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

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

13 (x * y) * (y \ (z * y)) = (x * z) * y. [copy(12),flip(a)].

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

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

16 x * ((y * x) \ 1) = y \ 1. [assumption].

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

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

19 (x * y) * z = (x * (y * z)) * a(x,y,z). [assumption].

20 (x * (y * z)) * a(x,y,z) = (x * y) * z. [copy(19),flip(a)].

21 x * y = (y * x) * K(x,y). [assumption].

22 (x * y) * K(y,x) = y * x. [copy(21),flip(a)].

23 K(K(c1,c2),c3) != 1. [deny(1)].

24 1 \ x = x. [para(4(a,1),2(a,1)),flip(a)].

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

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

30 (x * y) * y = y * (y * x). [para(2(a,1),9(a,1,1,2)),rewrite([3(5)])].

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

56 (x * y) * (y * z) = y * ((y * x) * z). [para(9(a,1),13(a,2)),rewrite([30(3),5(4)])].

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

67 (x * x) * ((y * (x * x)) * z) = (x * x) * (y * (z * (x * x))). [para(15(a,1),9(a,2,2,1)),rewrite([15(5,R)]),flip(a)].

69 (x * x) * (((x * x) * y) * z) = (x * x) * (y * (z * (x * x))). [para(15(a,1),9(a,2)),rewrite([15(5,R),15(10,R)]),flip(a)].

70 (x * x) * (y * ((x * x) * z)) = (x * x) * (y * (z * (x * x))). [para(15(a,2),9(a,1,1,2)),rewrite([15(5,R),69(10)])].

71 ((x * x) * y) * x = x * ((x * y) * x). [para(15(a,2),9(a,1,1))].

76 ((x * x) * y) * z = (y * (x * x)) * z. [para(15(a,1),13(a,2,1)),rewrite([13(5)])].

78 (x * (y * y)) * z = (y * y) * (x * z). [para(15(a,2),13(a,2)),rewrite([59(6)])].

80 ((x * x) * y) * z = (x * x) * (y * z). [back_rewrite(76),rewrite([78(6)])].

82 (x * x) * ((x * x) * (y * z)) = (x * x) * (y * (z * (x * x))). [back_rewrite(67),rewrite([78(4)])].

84 (x * x) * (y * x) = x * ((x * y) * x). [back_rewrite(71),rewrite([80(3)])].

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

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

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

92 1' = 1. [para(17(a,1),3(a,1)),flip(a)].

94 1 / x = x'. [para(17(a,1),6(a,1,1))].

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

97 x \ (y * x) = (x' * y) * x. [para(17(a,1),13(a,1,1)),rewrite([2(4)])].

98 (x * y) * (y \ 1) = (x * y') * y. [para(17(a,1),13(a,1,2,2))].

101 (x * x) * ((x * x)' * y) = y. [back_rewrite(59),rewrite([97(4),15(5,R)])].

111 x \ 1 = x'. [para(18(a,1),5(a,1,2))].

112 x'' = x. [para(18(a,1),6(a,1,1)),rewrite([94(3)])].

115 (x * y') * y = (x * y) * y'. [back_rewrite(98),rewrite([111(3)]),flip(a)].

119 (x / y)' = y * x'. [back_rewrite(87),rewrite([111(3),111(4)])].

120 (x * y)' = y \ x'. [back_rewrite(86),rewrite([111(3),111(4)])].

121 (x \ y) * y' = x'. [back_rewrite(85),rewrite([111(3),111(5)])].

123 (x * x) * ((x \ x') * y) = y. [back_rewrite(101),rewrite([120(3)])].

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

140 (x * ((y * y) * z)) * a(x,z,y * y) = (x * z) * (y * y). [para(15(a,2),20(a,1,1,2))].

150 (x * y) \ (y * x) = K(y,x). [para(22(a,1),5(a,1,2))].

151 (x * y) / K(x,y) = y * x. [para(22(a,1),6(a,1,1))].

166 x / y = x' \ y'. [para(119(a,1),112(a,1,1)),rewrite([120(3)]),flip(a)].

167 (x \ y')' = y * x. [para(112(a,1),119(a,2,2)),rewrite([166(2),112(2)])].

170 (x \ y') \ K(y,x)' = x * y. [back_rewrite(151),rewrite([166(3),120(2)])].

186 ((x \ y') \ y') * z = y * (x * (y \ z)). [back_rewrite(39),rewrite([166(2),120(2)])].

191 (x' \ y') \ x = y. [back_rewrite(29),rewrite([166(1)])].

195 (x \ y) \ x' = y'. [para(4(a,1),120(a,1,1)),flip(a)].

196 ((x * y) * z) \ x' = x \ ((z * x) \ y'). [para(9(a,1),120(a,1,1)),rewrite([120(4),120(7)])].

201 K(x,y) \ (x \ y') = y \ x'. [para(22(a,1),120(a,1,1)),rewrite([120(2),120(5)]),flip(a)].

205 (x \ y') * y = x'. [para(112(a,1),121(a,1,2))].

211 (x \ y)' = y' * x. [para(112(a,1),167(a,1,1,2))].

214 (x' \ y) \ x = y'. [para(112(a,1),191(a,1,1,2))].

217 x * ((x * y) * (z \ x')) = (y * z') * x. [para(205(a,1),9(a,1,1,2)),flip(a)].

226 (x \ (y' * z)) * (z \ y) = x'. [para(211(a,1),205(a,1,1,2))].

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

256 (x * y) \ x' = x \ (x \ y'). [para(30(a,1),120(a,1,1)),rewrite([120(3),120(5)])].

257 x' * (x' * (y \ x)) = y' * x'. [para(121(a,1),30(a,1,1)),flip(a)].

258 x * (x * (y \ x')) = y' * x. [para(205(a,1),30(a,1,1)),flip(a)].

263 x \ ((y \ x) * y) = K(y \ x,y). [para(4(a,1),150(a,1,1))].

264 ((x \ y) * x) \ y = K(x,x \ y). [para(4(a,1),150(a,1,2))].

267 K(x,y * y) = 1. [para(15(a,1),150(a,1,1)),rewrite([25(5)]),flip(a)].

274 K(x,y) * (y \ x') = x \ y'. [para(150(a,1),121(a,1,1)),rewrite([120(3),120(6)])].

275 x' \ (y' * (x \ y)) = K(y',x \ y). [para(121(a,1),150(a,1,1))].

276 (x' * (y \ x)) \ y' = K(y \ x,x'). [para(121(a,1),150(a,1,2))].

277 x' \ (y * (x \ y')) = K(y,x \ y'). [para(205(a,1),150(a,1,1))].

278 (x * (y \ x')) \ y' = K(y \ x',x). [para(205(a,1),150(a,1,2))].

279 (x \ y') * (x * y) = K(y,x)'. [para(150(a,1),211(a,1,1)),rewrite([120(4)]),flip(a)].

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

288 x' * (x * (y * y)) = y * y. [para(15(a,1),244(a,1,2,2)),rewrite([97(7),120(3),15(5,R),4(5)])].

291 x' * (x * x) = x. [para(15(a,2),244(a,1,2)),rewrite([15(3),97(4),120(2),205(3)])].

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

308 x \ x' = x' * x'. [para(112(a,1),298(a,1,1))].

319 (x * x) * ((x' * x') * y) = y. [back_rewrite(123),rewrite([308(3)])].

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

336 (x' * y') * x = x * (y \ x'). [para(284(a,1),121(a,1,1)),rewrite([120(2),120(6),211(5),97(6)]),flip(a)].

345 ((x * x) \ y) \ y = x * x. [para(15(a,2),331(a,1,1)),rewrite([4(6)])].

354 x' * ((y * y) \ x) = y' * y'. [para(345(a,1),211(a,1,1)),rewrite([120(2),308(2)]),flip(a)].

356 (x * x) \ y = (x' * x') * y. [para(345(a,1),284(a,1,1,1)),rewrite([4(4),97(4),354(4)]),flip(a)].

364 (x \ y) * x = x * (y * x'). [para(4(a,1),95(a,1,2,1)),flip(a)].

366 (x' * y) * x = (x * y) * x'. [para(95(a,1),5(a,1,2)),rewrite([97(2)])].

368 (x * y) * y' = y' * (y * x). [para(95(a,1),9(a,1,1)),rewrite([17(6),2(7)])].

370 x' * (x * y) = x * (x' * y). [para(9(a,1),95(a,1,2)),rewrite([17(3),2(3),115(6),368(6)]),flip(a)].

405 (x * ((x \ y) * x')) \ y = x. [back_rewrite(331),rewrite([364(3)])].

406 (x * (y * x')) \ (x * y) = x. [back_rewrite(284),rewrite([364(2)])].

407 (x * (y * x')) \ y = K(x,x \ y). [back_rewrite(264),rewrite([364(2)])].

408 x \ (y * (x * y')) = K(y \ x,y). [back_rewrite(263),rewrite([364(2)])].

411 (x * y') * x' = x * (y \ x'). [back_rewrite(336),rewrite([366(4)])].

420 x \ (y * x) = (x * y) * x'. [back_rewrite(97),rewrite([366(5)])].

423 (x * y') * y = y * (y' * x). [back_rewrite(115),rewrite([368(6),370(6)])].

424 (x * y) * y' = y * (y' * x). [back_rewrite(368),rewrite([370(6)])].

425 x * (x' * (y * y)) = y * y. [back_rewrite(288),rewrite([370(4)])].

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

432 x * ((y * y) * x') = y * y. [para(15(a,1),364(a,2,2)),rewrite([364(3),425(8)])].

436 (x * y') \ y' = y * (x \ y'). [para(364(a,1),120(a,1,1)),rewrite([120(4),211(6),420(7),411(8)])].

437 (x' \ y) * (x * (y' * x')) = y' * (x' \ y). [para(214(a,1),364(a,1,1)),rewrite([211(9)]),flip(a)].

450 (x * y') \ (x * (y \ x)) = x. [para(121(a,1),406(a,1,1,2))].

453 (x * (y * x')) * ((x * y) * (x * (y \ x'))) = x * (x * (y * x')). [para(406(a,1),364(a,1,1)),rewrite([120(12),436(12)]),flip(a)].

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

466 (x \ y) * ((y' * x) * (z * z)) = z * z. [para(211(a,1),425(a,1,2,1))].

474 (x \ (y \ x)) \ (x * y') = x. [para(121(a,1),428(a,1,2,2))].

488 K((x * x) * y',y) = 1. [para(432(a,1),150(a,1,1)),rewrite([423(5),425(5),25(3)]),flip(a)].

492 K((x * x) * y,y') = 1. [para(112(a,1),488(a,1,1,2))].

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

504 (x * y) \ (x * (y' \ x)) = x. [para(112(a,1),450(a,1,1,2))].

508 (x \ y) \ y' = y \ (x' \ y'). [para(450(a,1),195(a,1,1)),rewrite([120(3),120(7)]),flip(a)].

521 (x \ (y' \ x)) \ (x * y) = x. [para(112(a,1),474(a,1,2,2))].

523 (x * y) * x' = x * (y' \ x'). [para(474(a,1),121(a,1,1)),rewrite([120(3),211(7),211(6),366(7)]),flip(a)].

539 x \ (y * x) = x * (y' \ x'). [back_rewrite(420),rewrite([523(5)])].

556 (x' * y) * x = x * (y' \ x'). [back_rewrite(366),rewrite([523(6)])].

565 (x * y) * x = x * (y' \ x). [para(112(a,1),501(a,1,1,2))].

566 (x \ y) * (y \ (x \ y)) = x' * (x \ y). [para(121(a,1),501(a,1,1)),flip(a)].

589 (x * x) * (y * x) = x * (x * (y' \ x)). [back_rewrite(84),rewrite([565(5)])].

613 (x \ (y' \ x)) * ((x * y) * (x * (y \ x'))) = y' \ x. [para(521(a,1),364(a,1,1)),rewrite([4(4),211(10),211(9),556(10),112(8)]),flip(a)].

628 (x * (y' \ x)) \ (x * (x * y)) = K(x,x * y). [para(565(a,1),150(a,1,1))].

656 (K(x,y)' \ (y * x)) \ (K(x,y)' * (x * y)) = K(x,y)'. [para(170(a,1),474(a,1,1,2)),rewrite([211(9),112(8)])].

701 K(x',y) * (y \ x) = x' \ y'. [para(150(a,1),226(a,1,1)),rewrite([120(7)])].

705 (x * y) \ y = y' * (x \ y). [para(406(a,1),226(a,1,1)),rewrite([112(6),120(7),112(6)]),flip(a)].

706 x' * ((y \ x') \ x) = y' \ x. [para(450(a,1),226(a,1,1)),rewrite([120(9),112(8)])].

709 x' * (y \ x) = x * (y \ x'). [para(521(a,1),226(a,1,1)),rewrite([211(9),211(7),112(5),523(7),112(5)])].

712 (x' \ y) * (x * (y' * x')) = y * (x' \ y'). [back_rewrite(437),rewrite([709(11)])].

714 x * ((y \ x') \ x') = y' \ x. [back_rewrite(706),rewrite([709(5)])].

715 (x * y) \ y = y * (x \ y'). [back_rewrite(705),rewrite([709(5)])].

719 K(x \ y',y) = K(x \ y,y'). [back_rewrite(276),rewrite([709(3),278(5)])].

720 K(x',y \ x) = K(x,y \ x'). [back_rewrite(275),rewrite([709(4),277(5)]),flip(a)].

721 x * (x' * (y \ x')) = y' * x'. [back_rewrite(257),rewrite([709(4),370(5)])].

729 (x' * y) \ x = x' \ (x' \ y'). [para(112(a,1),256(a,1,2))].

731 x * ((x \ y') * x') = y \ x'. [para(256(a,1),121(a,1,1)),rewrite([112(5),364(4),120(7)])].

766 x \ (x \ ((y \ x') \ x')) = (y' * x) \ x'. [para(258(a,1),256(a,1,1)),rewrite([120(8)]),flip(a)].

799 x' * (y * (x * y')) = K(y,y \ x)'. [para(195(a,1),279(a,1,1)),rewrite([364(3)])].

804 ((x * y) * (x \ y')) \ K(y,x)' = K(x \ y',x * y). [para(279(a,1),150(a,1,2))].

806 x * (y * (x' * y')) = K(y,y \ x')'. [para(405(a,1),279(a,1,1)),rewrite([731(5),364(3),731(10)])].

820 (x * x) * (y * z) = y * (z * (x * x)). [para(319(a,1),9(a,2,2,1)),rewrite([80(7),15(9,R),319(9)]),flip(a)].

832 x * (x' * (x \ y)) = x' * y. [para(4(a,1),370(a,1,2)),flip(a)].

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

841 (x * y) * ((y \ x') * K(y,x)) = K(x,y)'. [para(22(a,1),370(a,1,2)),rewrite([120(2),279(4),120(5)]),flip(a)].

842 (x' * y) \ x' = (x * y) \ x. [para(370(a,1),120(a,1,1)),rewrite([120(4),112(7)])].

845 (x \ y') * (y * (x' \ y)) = x * (x' * y). [para(205(a,1),370(a,1,2)),rewrite([211(3),112(2),424(3),211(8),112(7),565(7)]),flip(a)].

846 (x \ y) * ((y' * x) * z) = (y' * x) * ((x \ y) * z). [para(211(a,1),370(a,1,1)),rewrite([211(8)]),flip(a)].

850 x * (x' * (x' * y)) = x \ y. [para(370(a,1),30(a,2,2)),rewrite([523(3),523(6),211(4),112(2),256(4),112(2),4(3),370(6)]),flip(a)].

871 (x' * y) * ((y \ x) * (z * z)) = z * z. [back_rewrite(466),rewrite([846(6)])].

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

887 (x \ y') \ y' = (x \ y) \ y. [para(709(a,1),120(a,1,1)),rewrite([120(4),112(7)])].

888 (x \ y') * (z \ (y * x)) = (y * x) * (z \ (x \ y')). [para(120(a,1),709(a,1,1)),rewrite([120(8)])].

910 x * (y * (x \ y')) = K(x \ y,y')'. [para(709(a,1),279(a,1,2)),rewrite([211(3),5(4)])].

913 x \ (x \ ((y \ x) \ x)) = (y' * x) \ x'. [back_rewrite(766),rewrite([887(4)])].

915 x * ((y \ x) \ x) = y' \ x. [back_rewrite(714),rewrite([887(4)])].

916 ((x \ y) \ y) * z = y * (x * (y \ z)). [back_rewrite(186),rewrite([887(4)])].

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

932 x' \ (x * y) = (x * x) * y. [para(5(a,1),915(a,1,2,1)),rewrite([539(3),56(6),217(6),112(2)]),flip(a)].

934 (x' * y) \ y' = y' * (x' \ y'). [para(195(a,1),915(a,1,2,1)),rewrite([211(7)]),flip(a)].

936 (x \ (y' \ x)) * (x * y) = y * (y' \ x). [para(915(a,1),30(a,1,1)),rewrite([931(4),566(6),112(2),931(5),931(8),364(10),121(10),112(8)]),flip(a)].

937 K(x \ (y' \ x),x) = (y' \ x) \ (x * y). [para(915(a,1),150(a,1,1)),rewrite([931(4),364(6),121(6),112(4),931(6)]),flip(a)].

942 (x * y') \ y = y * (x \ y). [para(405(a,1),915(a,1,2,1)),rewrite([120(7),715(7),112(6),709(6),195(5)]),flip(a)].

954 x' \ (y' \ x') = x' * (y * x). [para(256(a,1),915(a,1,2,1)),rewrite([195(6),211(4),112(3),120(5),931(7)]),flip(a)].

956 K(x \ (y' \ x),x)' = (y \ x') * (y' \ x). [para(915(a,1),279(a,1,2)),rewrite([931(2),211(4),211(3),556(4),112(2),5(4),931(7)]),flip(a)].

960 (x \ (y' \ x)) * z = x * (y * (x \ z)). [back_rewrite(916),rewrite([931(2)])].

962 x \ (x \ (x \ (y' \ x))) = x' * (y' \ x'). [back_rewrite(913),rewrite([931(2),934(9)])].

967 x \ (y' \ x) = x' * (y * x). [back_rewrite(887),rewrite([931(4),954(5),931(5)]),flip(a)].

971 (x * x) * (y \ x') = y \ x. [back_rewrite(882),rewrite([932(5)])].

972 (x * x) * (x' * y) = x * y. [back_rewrite(833),rewrite([932(5)])].

979 (x' * (y * x)) * (x * y) = y * (y' \ x). [back_rewrite(936),rewrite([967(3)])].

981 (x' * (y * x)) * ((x * y) * (x * (y \ x'))) = y' \ x. [back_rewrite(613),rewrite([967(3)])].

985 x \ (x \ (x' * (y * x))) = x' * (y' \ x'). [back_rewrite(962),rewrite([967(3)])].

987 (x' * (y * x)) * z = x * (y * (x \ z)). [back_rewrite(960),rewrite([967(3)])].

991 K(x' * (y * x),x)' = (y \ x') * (y' \ x). [back_rewrite(956),rewrite([967(3)])].

992 x' * (y * x) = x * (y * x'). [back_rewrite(954),rewrite([967(5),112(2)]),flip(a)].

996 K(x * (y * x'),x) = (y' \ x) \ (x * y). [back_rewrite(937),rewrite([967(3),992(3)])].

998 (x \ y) \ y = y * (x * y'). [back_rewrite(931),rewrite([967(5),992(5)])].

1006 x * (x * (y * x')) = y' \ x. [back_rewrite(981),rewrite([992(3),453(9)])].

1007 (x * (y * x')) * (x * y) = y * (y' \ x). [back_rewrite(979),rewrite([992(3)])].

1010 K(x * (y * x'),x)' = (y \ x') * (y' \ x). [back_rewrite(991),rewrite([992(3)])].

1014 (x * (y * x')) * z = x * (y * (x \ z)). [back_rewrite(987),rewrite([992(3)])].

1015 x \ (y * x') = x' * (y' \ x'). [back_rewrite(985),rewrite([992(3),5(4)])].

1033 x * (x' \ y) = y * (x * x). [back_rewrite(1007),rewrite([1014(5),5(2)]),flip(a)].

1047 (x * y) \ y' = y' * (x \ y'). [para(112(a,1),942(a,1,1,2))].

1051 x \ (y' \ x') = x' * (y * x'). [para(942(a,1),211(a,1,1)),rewrite([120(3),508(3)])].

1085 (x \ y) \ y' = y' * (x * y'). [back_rewrite(508),rewrite([1051(7)])].

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

1091 (x' * y) * (x * x) = x * y. [para(972(a,1),15(a,1)),flip(a)].

1094 (x * (y * z)) * a(x,y * y,y' * z) = y * (y' \ (x * (y' * z))). [para(972(a,1),20(a,1,1,2)),rewrite([78(12),1087(12)])].

1108 x * (y * (y' \ x')) = y * y. [para(432(a,1),972(a,2)),rewrite([1087(5),1087(8),5(8)])].

1109 K(x * y,y \ x) = 1. [para(972(a,1),492(a,1,1)),rewrite([120(4),112(3)])].

1124 x * (x' \ (y \ x')) = y \ x. [back_rewrite(971),rewrite([1087(4)])].

1125 x' \ (x * y) = x * (x' \ y). [back_rewrite(932),rewrite([1087(5)])].

1133 x * (x' \ (y * z)) = y * (z * (x * x)). [back_rewrite(820),rewrite([1087(3)])].

1143 x * (x' \ (y * x)) = x * (x * (y' \ x)). [back_rewrite(589),rewrite([1087(3)])].

1165 (x * x) \ y = x' * (x \ y). [back_rewrite(356),rewrite([1087(6),112(5)])].

1168 (x * (y * (y' \ z))) * a(x,z,y * y) = (x * z) * (y * y). [back_rewrite(140),rewrite([1087(2)])].

1171 x * (x' \ (y * (z * (x * x)))) = x * (x * (x' \ (x' \ (y * z)))). [back_rewrite(82),rewrite([1087(4),1087(6),1125(6),1087(12)]),flip(a)].

1173 (x * (x' \ y)) * z = x * (x' \ (y * z)). [back_rewrite(80),rewrite([1087(2),1087(7)])].

1174 (x * (y * y)) * z = y * (y' \ (x * z)). [back_rewrite(78),rewrite([1087(6)])].

1176 x * (x' \ (y * (x * (x' \ z)))) = x * (x * (x' \ (x' \ (y * z)))). [back_rewrite(70),rewrite([1087(3),1087(6),1087(12),1171(13)])].

1181 K(x * (y' \ x),y) = 1. [para(5(a,1),1109(a,1,2)),rewrite([565(2)])].

1184 (x \ y) * (y * x) = (y * x) * (x \ y). [para(1109(a,1),22(a,1,2)),rewrite([3(5)])].

1187 K(x' * (x \ y),y') = 1. [para(195(a,1),1109(a,1,2))].

1214 K(x * (y \ x),y') = 1. [para(112(a,1),1181(a,1,1,2,1))].

1233 K(x * y,y' * x) = 1. [para(428(a,1),1214(a,1,1,2)),rewrite([565(4),120(3),214(4),112(2),211(3)])].

1245 K((x' \ y) * x,y) = 1. [para(4(a,1),1233(a,1,2))].

1266 ((x' \ y) * x) * y = y * ((x' \ y) * x). [para(1245(a,1),22(a,1,2)),rewrite([3(6)]),flip(a)].

1270 ((x \ y') \ y) * x = x * ((y' \ x) * y). [para(1245(a,1),170(a,1,2,1)),rewrite([120(4),211(3),1015(4),112(3),92(7),111(7),211(6),120(5),112(4)])].

1284 (x' * (x \ y)) \ y = y' \ ((x \ y) \ x). [para(1187(a,1),201(a,1,1)),rewrite([112(6),24(6),120(9),112(8)])].

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

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

1301 (x \ y) \ x = x * (x' \ y'). [para(1033(a,2),211(a,2)),rewrite([1165(2),120(4),112(3)])].

1324 x' * (y * (x * x)) = x * y. [para(1033(a,1),370(a,1,2)),rewrite([4(8)])].

1334 (x' * (x \ y)) \ y = x * x. [back_rewrite(1284),rewrite([1301(7),1289(10)])].

1358 (x * y) * (x' * x') = x' * y. [para(112(a,1),1091(a,1,1,1))].

1365 (x * y) * (y \ x) = x * x. [para(1091(a,1),370(a,1,2)),rewrite([120(3),112(2),1184(3),120(8),112(7),871(9)])].

1369 (x \ y) * (y * x) = y * y. [back_rewrite(1184),rewrite([1365(6)])].

1370 (x \ y') * (y * y) = x \ y. [para(1365(a,1),5(a,1,2)),rewrite([456(3),120(2)])].

1380 (x \ y) * (x \ y) = x' * (y' \ (x \ y)). [para(121(a,1),1365(a,1,1)),flip(a)].

1384 K(x \ y,y * x) = 1. [para(1365(a,1),150(a,1,1)),rewrite([1369(4),25(3)]),flip(a)].

1436 K(x' \ (y \ x),y') = 1. [para(121(a,1),1384(a,1,2))].

1471 x' * (y' \ (x \ y)) = x' * ((y' \ x') * y). [para(1436(a,1),170(a,1,2,1)),rewrite([211(5),211(3),565(5),92(9),111(9),211(8),120(6),112(5),1270(6)]),flip(a)].

1484 (x \ y) * (x \ y) = x' * ((y' \ x') * y). [back_rewrite(1380),rewrite([1471(8)])].

1521 (x' \ y) * x = x * (y * x). [para(1288(a,1),364(a,1,1)),rewrite([1174(7),539(7),112(7),709(7),258(8),112(5)])].

1543 (x \ y) * (x \ y) = x' * (y * (x' * y)). [back_rewrite(1484),rewrite([1521(8)])].

1561 (x * (y * x)) * y = y * (x * (y * x)). [back_rewrite(1266),rewrite([1521(3),1521(6)])].

1630 K(x',y * (x * x)) = K(x,y). [para(1324(a,1),150(a,1,2)),rewrite([1174(4),539(4),112(4),709(4),258(5),112(2),150(3)]),flip(a)].

1633 (x * (y * x)) \ (x * y) = x'. [para(1324(a,1),406(a,1,2)),rewrite([112(5),1174(4),1143(5),370(6),370(5),709(4),258(5),112(2)])].

1637 (x * y) \ x = x' \ (x \ y'). [para(1324(a,1),256(a,1,1)),rewrite([112(3),120(7),1165(7),5(9)])].

1656 x' \ (x \ y') = x \ (x' \ y'). [back_rewrite(842),rewrite([1637(4),112(2),1637(6)]),flip(a)].

1664 (x * y) \ x = x \ (x' \ y'). [back_rewrite(1637),rewrite([1656(6)])].

1668 (x \ y) * y = y * (y' \ x'). [para(1370(a,1),9(a,1,1)),rewrite([565(6),211(5),112(4),1664(4),4(7)])].

1675 (x \ y') * (x \ y) = (x \ y) * (x \ y'). [para(1370(a,1),30(a,2,2)),rewrite([1087(4),1124(5)]),flip(a)].

1685 (x \ (x \ y')) * (x * x) = x \ (x' \ y'). [para(256(a,1),1370(a,1,1)),rewrite([1664(7)])].

1734 (x * (y' \ x)) * (x' \ y) = (x' \ y) * (y * (x * x)). [para(1033(a,1),1521(a,2,2)),rewrite([211(3),942(4)])].

1803 K(x',x * y) = K(x,x' * y). [para(1091(a,1),1630(a,1,2))].

1824 (x * (y * x)) * ((x * y) * (x' * (y \ x'))) = y' \ x. [para(1633(a,1),364(a,1,1)),rewrite([370(4),992(3),1006(4),120(8),1047(8)]),flip(a)].

1826 x' \ (y' \ x) = x * (y * x). [para(1633(a,1),428(a,1,1)),rewrite([120(7),1047(7),1824(10)])].

1872 K(x' * (y \ x'),x) = K(x * (y \ x'),x'). [para(942(a,1),719(a,1,1)),rewrite([112(7),715(7)])].

1873 K(x * (y \ x'),x) = K(x * (y \ x),x'). [para(942(a,1),719(a,2,1)),rewrite([715(4),112(3),709(3)])].

1883 K(x * y,x \ (y \ x')) = K(y \ x',y). [para(5(a,1),720(a,1,2)),rewrite([120(2),120(6)]),flip(a)].

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

1915 K(x' * (x \ y),x) = K(y,x'). [para(832(a,1),150(a,1,1)),rewrite([556(6),211(4),1047(6),721(8),112(4),150(5)]),flip(a)].

1923 x \ (x \ y) = x' * (x' * y). [para(832(a,1),370(a,1,2)),rewrite([850(10)]),flip(a)].

1970 x \ (x' \ y') = x * (x' * y'). [back_rewrite(1685),rewrite([1923(3),1091(7)]),flip(a)].

2001 x * (x' \ (y * (x * (x' \ z)))) = x * (x * (x * (x * (y * z)))). [back_rewrite(1176),rewrite([1923(12),112(9),112(9)])].

2021 (x' * y) \ x = x * (x * y'). [back_rewrite(729),rewrite([1923(8),112(5),112(5)])].

2038 (x * y) \ x = x * (x' * y'). [back_rewrite(1664),rewrite([1970(6)])].

2044 x \ (x' \ y) = x * (x' * y). [para(4(a,1),850(a,1,2,2)),flip(a)].

2052 x * (x * (x' * y)) = x' \ y. [para(112(a,1),850(a,1,2,1)),rewrite([112(3),370(4),370(3)])].

2068 x \ (y \ x) = x * (y' * x'). [para(258(a,1),850(a,1,2)),rewrite([112(6)]),flip(a)].

2116 (x \ y) * (z * (y' * x)) = (y' * x) * (z * (x \ y)). [para(211(a,1),992(a,1,1)),rewrite([211(8)]),flip(a)].

2119 x * ((x * y) * (x' * y)) = x * (y * (x * (y' \ x'))). [para(992(a,1),30(a,1,1)),rewrite([1014(5),539(2),424(10),56(11)]),flip(a)].

2120 (x * (y * x')) \ (x * (x' * y)) = K(y * x,x'). [para(992(a,1),150(a,1,1)),rewrite([424(6)])].

2145 (x' * y') * (y * (y' \ x)) = x * (y' \ x'). [back_rewrite(712),rewrite([2116(7)])].

2215 (x' \ y) * (x * (y' \ x')) = y * (x * y). [para(214(a,1),1301(a,1,1)),rewrite([1826(4),211(7),715(9),112(8),709(8)]),flip(a)].

2216 (x * y) * ((y \ x') \ (x \ y')) = K(y,x) \ (x * y). [para(150(a,1),1301(a,1,1)),rewrite([120(6),120(8)]),flip(a)].

2249 (x * (y \ x)) \ (x * (x' \ y')) = K(y \ x,x). [para(1668(a,1),150(a,1,2))].

2250 K(x,y) \ (y * x) = K(y,x) * (y * x). [para(150(a,1),1668(a,1,1)),rewrite([120(6),120(8),2216(10)]),flip(a)].

2266 (x \ y) * (y * (x' \ y')) = (y' * x) * (y * (y' \ x')). [para(1668(a,1),370(a,1,2)),rewrite([211(2),211(10),556(11)]),flip(a)].

2272 (x' \ y) * (y * (x * x)) = x * (x' \ (y * (y' \ x))). [para(1288(a,1),1668(a,1,1)),rewrite([120(10),1165(10),2038(13),112(10),211(11),112(10),370(11),992(10),1006(11),1174(10)])].

2288 (x * (y' \ x)) * (x' \ y) = x * (x' \ (y * (y' \ x))). [back_rewrite(1734),rewrite([2272(11)])].

2293 K(x * y,(y \ x') * K(y,x)) = K(y \ x',y * x). [para(22(a,1),1803(a,1,2)),rewrite([120(2),120(7)]),flip(a)].

2294 K(x \ y',(y * x) * z) = K(y * x,(x \ y') * z). [para(120(a,1),1803(a,1,1)),rewrite([120(8)])].

2325 (x * y) \ K(x,y)' = (y \ x') * K(y,x). [para(150(a,1),1905(a,2,2)),rewrite([120(3),279(5),120(6)])].

2369 x \ (y \ x') = x' * (y' * x'). [para(258(a,1),1923(a,2,2)),rewrite([112(3),709(3),5(4)])].

2401 K(x * y,x' * (y' * x')) = K(y \ x',y). [back_rewrite(1883),rewrite([2369(4)])].

2420 x' \ (x \ y) = x * (x' * y). [para(112(a,1),2044(a,1,2,1)),rewrite([112(6),370(6)])].

2430 (x \ y) * (x * x) = x' \ y. [para(2044(a,1),1033(a,1,2)),rewrite([112(3),370(3),2052(4),112(4)]),flip(a)].

2436 (x' * y) * (x * (x' \ y')) = y * (y' * x). [para(2044(a,1),1006(a,2)),rewrite([112(2),112(3),112(4),211(4),2116(6),4(5),556(4),2266(6),112(10),370(10)])].

2437 (x * (x' * y)) * (x' \ y) = y * (x * y). [para(2044(a,1),1668(a,1,1)),rewrite([211(11),715(13),112(12),709(12),2215(13)])].

2517 K(x * (x' * y),x) = (x' \ y) \ (y' \ x). [para(2052(a,1),150(a,1,1)),rewrite([565(6),120(5),112(4),998(4),1006(6)]),flip(a)].

2518 K(x,x * (x' * y)) = (y' \ x) \ (x' \ y). [para(2052(a,1),150(a,1,2)),rewrite([565(4),120(3),112(2),998(2),1006(4)]),flip(a)].

2526 x * (y * (x * (y' \ x'))) = y * (x * y). [para(2052(a,1),1521(a,2,2)),rewrite([120(4),2038(4),112(3),370(4),2038(5),120(5),112(4),709(4),258(5),112(2),56(5),2119(5),2437(12)])].

2531 x' \ (y * x) = x * (y' \ x). [para(992(a,1),2052(a,1,2,2)),rewrite([1006(4)]),flip(a)].

2532 x' \ (y * (y' \ x)) = x * (x * (y * y)). [para(1108(a,1),2052(a,1,2,2)),rewrite([112(7)]),flip(a)].

2536 x * ((x * y) * (x' * y)) = y * (x * y). [back_rewrite(2119),rewrite([2526(11)])].

2543 (x * (y' \ x)) * (x' \ y) = x * (x * (x * (y * y))). [back_rewrite(2288),rewrite([2532(11)])].

2587 (x \ y') \ y = y * (x * y). [para(504(a,1),2420(a,1,2)),rewrite([120(2),120(6),845(10),56(8),2536(8)])].

2589 (x \ y) * (x * (y \ x)) = x * ((x * y') * (x' * y)). [para(2420(a,1),709(a,1,2)),rewrite([211(2),56(6),211(10),2531(11),112(9)]),flip(a)].

2600 K(x \ y,x * (y \ x)) = K(y' * x,x * (x' * y)). [para(2420(a,1),720(a,1,2)),rewrite([211(2),211(10),2531(11),112(9)]),flip(a)].

2642 K(x * (y * x'),x) = K(x * (y * x),x'). [para(2587(a,1),719(a,2,1)),rewrite([998(4),112(3),992(3)])].

2662 K(x * (y * x),x')' = (y \ x') * (y' \ x). [back_rewrite(1010),rewrite([2642(4)])].

2663 K(x * (y * x),x') = (y' \ x) \ (x * y). [back_rewrite(996),rewrite([2642(4)])].

2728 (x * (y \ x)) * (x \ y) = x. [para(2531(a,1),226(a,1,1)),rewrite([112(2),112(6)])].

2763 K(x' * y,y * (y' * x)) = (y * x') * (y' * x). [para(2728(a,1),150(a,1,1)),rewrite([2589(4),5(7),2600(9)]),flip(a)].

2818 K(x \ y,x * (y \ x)) = (x * y') * (x' * y). [back_rewrite(2600),rewrite([2763(10)])].

2857 K(x,x' * (y' * x')) = (x' * y') \ (y \ x'). [para(1668(a,1),407(a,1,1,2)),rewrite([112(3),832(5),2369(9)]),flip(a)].

2871 K(x' \ y,x') = K(x \ y,x). [para(112(a,1),408(a,1,2,2,2)),rewrite([992(3),408(4)]),flip(a)].

2873 K(x * (y' * x),x') = (y \ x) \ (x * y'). [para(121(a,1),408(a,1,2,2)),rewrite([2068(6),2642(9)]),flip(a)].

2875 x \ (y * (x' \ y')) = K(y,x' \ y'). [para(214(a,1),408(a,2,1)),rewrite([211(5),2116(7),2145(7),720(9)])].

2892 K(x \ y',x) = K(x \ y,x). [para(408(a,1),1288(a,2)),rewrite([1014(6),456(3),1324(5),408(4)]),flip(a)].

2898 x * (x' * K(y \ x,y)) = K(y,y \ x)'. [para(408(a,1),832(a,1,2,2)),rewrite([799(10)])].

2899 x * (x' * K(y,y \ x)') = K(y \ x,y). [para(408(a,1),850(a,2)),rewrite([799(6)])].

2902 K(x * (x' \ y'),x \ y) = K(y,x' \ y'). [para(1301(a,1),408(a,2,1)),rewrite([211(3),2116(5),4(4),556(3),2875(5)]),flip(a)].

2929 K(x * y,x' * (y' * x')) = K(y \ x,y). [back_rewrite(2401),rewrite([2892(10)])].

2931 x' * K(y \ x,y) = y * (x' * y'). [para(2892(a,1),22(a,1,2)),rewrite([4(3),364(7)])].

2933 K(x,y' \ x') = K(x,y \ x'). [para(195(a,1),2892(a,1,1)),rewrite([720(3),1301(5),2902(9)]),flip(a)].

2940 K((x * y) \ (x' * (y' * x')),x * y) = K(x,x * y). [para(504(a,1),2892(a,2,1)),rewrite([120(5),1085(5)])].

2947 K(x' * (x' * (x' * y')),x) = K(x' \ y,x). [para(1288(a,1),2892(a,2,1)),rewrite([120(3),1165(3),1905(5),1923(4)])].

2950 K(x * (y' * x),x') = K(y,x'). [para(1905(a,1),2892(a,2,1)),rewrite([120(3),112(2),2068(2),2642(5),1915(9)])].

2951 K(x' * (x' * y),x) = K(x * (y \ x),x'). [para(1923(a,1),2892(a,2,1)),rewrite([211(2),539(3),112(2),1873(4)]),flip(a)].

2952 K(x * (y \ x'),x') = K(x * (x' * y),x). [para(2044(a,1),2892(a,2,1)),rewrite([211(3),1015(4),112(3),1872(5)])].

2962 K(x,x \ y')' = K(x,x \ y)'. [back_rewrite(2898),rewrite([2931(4),806(5)])].

2973 (x \ y) \ (y * x') = K(x,y'). [back_rewrite(2873),rewrite([2950(5)]),flip(a)].

2974 K(x * (x * (x * y)),x') = K(x' \ y,x). [back_rewrite(2947),rewrite([2951(8),2021(4),112(2)])].

2991 x * (y * (x' * y')) = K(y,y \ x)'. [back_rewrite(806),rewrite([2962(9)])].

2993 K(x * (x' \ y),x') = K(y,x). [para(5(a,1),2871(a,2,1)),rewrite([1125(3)])].

2996 K((x \ y) \ z,x \ y) = K((y' * x) \ z,y' * x). [para(211(a,1),2871(a,1,1,1)),rewrite([211(5)]),flip(a)].

3008 K(x * (x' * y),x) = K(x * (x * y),x'). [para(1923(a,1),2871(a,1,1)),rewrite([112(2),112(2),2044(7)]),flip(a)].

3021 K(x * (y \ x'),x') = K(x * (x * y),x'). [back_rewrite(2952),rewrite([3008(9)])].

3024 K(x * (x * y),x') = (x' \ y) \ (y' \ x). [back_rewrite(2517),rewrite([3008(4)])].

3028 (x' \ y) \ (y * x) = K(x',y'). [para(112(a,1),2973(a,1,2,2))].

3031 K(x,x \ y') = K(x,x' * y). [para(121(a,1),2973(a,1,2)),rewrite([2068(2),407(6),211(5)])].

3035 K(x',x' * y) = K(x,x' \ y'). [para(30(a,1),2973(a,1,2)),rewrite([1015(3),628(10),120(7)])].

3048 K(x,y) * (x' \ y) = y * x. [para(2973(a,1),226(a,1,1)),rewrite([112(2),211(7),112(6)])].

3050 K(x \ y,y) = K(x * y',y'). [para(942(a,1),2973(a,1,1)),rewrite([120(5),2249(7)])].

3061 K(x \ y,y') = K(x * y,y'). [para(719(a,1),2973(a,2)),rewrite([112(2),998(2),112(5),211(5),2120(7),112(7),719(6)]),flip(a)].

3084 K(x * (y * x),x') = K(y',x'). [back_rewrite(2663),rewrite([3028(8)])].

3091 K(x,x \ y)' = K(x,x' * y)'. [back_rewrite(2962),rewrite([3031(3)]),flip(a)].

3140 x * (y * (x \ y')) = K(x * y,y')'. [back_rewrite(910),rewrite([3061(7)])].

3147 (x \ y') * (x' \ y) = K(x',y')'. [back_rewrite(2662),rewrite([3084(4)]),flip(a)].

3153 x * (y * (x' * y')) = K(y,y' * x)'. [back_rewrite(2991),rewrite([3091(8)])].

3161 x * (x' * K(y,y' * x)') = K(y \ x,y). [back_rewrite(2899),rewrite([3091(4)])].

3164 K(x,y) * (x * y) = y' \ x. [para(3048(a,1),5(a,1,2)),rewrite([2250(3)])].

3240 (x \ y') * K(x,y) = y' * x'. [para(3164(a,1),120(a,1,1)),rewrite([211(3),2325(7)]),flip(a)].

3273 (x * y) * (x \ y') = K(y',x')'. [para(3164(a,1),992(a,1,2)),rewrite([120(2),3147(5),120(8),274(9)]),flip(a)].

3292 K(x \ y',x * y) = K(y * x,y' * x'). [back_rewrite(2293),rewrite([3240(5)]),flip(a)].

3296 (x * y) * (x' * y') = K(x,y)'. [back_rewrite(841),rewrite([3240(5)])].

3304 K(x * y,x' * y') = K(x',y')' \ K(x,y)'. [back_rewrite(804),rewrite([3273(4),3292(11)]),flip(a)].

3316 K(x \ y',x * y) = K(y',x')' \ K(y,x)'. [back_rewrite(3292),rewrite([3304(9)])].

3335 K(x' * y,x) = K(x * y,x'). [para(5(a,1),2993(a,1,1,2)),flip(a)].

3502 (x * y) * ((x \ y') \ (y \ x')) = K(x,y)' * (x * y). [para(279(a,1),523(a,1,1)),rewrite([211(5),112(4),120(8),211(11),112(10),888(11)]),flip(a)].

3542 (x \ y') \ (y \ x') = K(y',x'). [para(150(a,1),701(a,1,2)),rewrite([120(2),3316(4),205(9),112(5),120(5),120(7)]),flip(a)].

3576 K(x,y)' * (x * y) = (x * y) * K(y',x'). [back_rewrite(3502),rewrite([3542(6)]),flip(a)].

3592 (K(x,y)' \ (y * x)) \ ((x * y) * K(y',x')) = K(x,y)'. [back_rewrite(656),rewrite([3576(8)])].

3984 x * (x' \ (y' * (x' * (y' * x')))) = (y \ x) * (y \ x'). [para(1365(a,1),1358(a,1,1)),rewrite([120(3),120(5),1543(6),1087(9),120(12),1675(14)])].

4093 K(x,x' * (y * x')) = K(x,x * (x' * y')). [para(2587(a,1),2933(a,2,2)),rewrite([112(2),211(2),2038(4),112(3),370(4)]),flip(a)].

4099 K(x,x * (x' * y)) = (x' * y') \ (y \ x'). [back_rewrite(2857),rewrite([4093(6),112(3)])].

4110 K(x' \ y,x) = K(x \ y',x'). [para(30(a,1),3084(a,1,1,2)),rewrite([2974(5),120(5)])].

4142 K(x * (x * (x * y)),x') = K(x \ y',x'). [back_rewrite(2974),rewrite([4110(8)])].

4201 (x * y') * (x' * y) = K(x,y')'. [para(112(a,1),3296(a,1,2,2))].

4202 (x' * y') \ (y \ x') = K(x,y). [para(3296(a,1),120(a,1,1)),rewrite([112(3),120(6)]),flip(a)].

4205 K(x' * y,y')' = K(x * y,y')'. [para(121(a,1),3296(a,1,1)),rewrite([211(3),112(5),556(4),3140(6),3061(8)])].

4215 K(x,y)' \ ((x * y) * K(y',x')) = x * y. [para(3296(a,1),504(a,1,1)),rewrite([120(7),112(6),3028(7)])].

4274 K(x \ y,x * (y \ x)) = K(x,y')'. [back_rewrite(2818),rewrite([4201(9)])].

4275 K(x' * y,y * (y' * x)) = K(y,x')'. [back_rewrite(2763),rewrite([4201(11)])].

4276 K(x,x * (x' * y)) = K(x,y). [back_rewrite(4099),rewrite([4202(10)])].

4321 (x' \ y) \ (y' \ x) = K(y,x). [back_rewrite(2518),rewrite([4276(4)]),flip(a)].

4338 K(x * (x * y),x') = K(y,x). [back_rewrite(3024),rewrite([4321(9)])].

4356 K(x \ y',x') = K(x * y,x). [back_rewrite(4142),rewrite([4338(5)]),flip(a)].

4359 K(x * (y \ x'),x') = K(y,x). [back_rewrite(3021),rewrite([4338(9)])].

4387 K(x,x' \ y) = K(x,x * y). [para(4(a,1),4276(a,1,2,2)),flip(a)].

4408 K(x * y,x') = K(y,x')'. [para(3335(a,1),4276(a,2)),rewrite([120(7),112(6),1668(6),2436(9),4275(6)]),flip(a)].

4417 K(x',x' * y) = K(x,x * y'). [back_rewrite(3035),rewrite([4387(8)])].

4511 K(x * y,y)' = K(x,y). [back_rewrite(4359),rewrite([4408(5),3050(4),112(2),112(3)])].

4513 K(x,y') = K(x,y). [back_rewrite(4338),rewrite([4408(4),4408(3),112(4)])].

4562 K(x',y) = K(x,y). [back_rewrite(4205),rewrite([4513(4),4511(4),4513(5),4511(5)])].

4605 K(x * y,x) = K(y,x)'. [back_rewrite(4408),rewrite([4513(3),4513(4)])].

4621 K(x \ y,x) = K(y,x)'. [back_rewrite(4356),rewrite([4513(4),2892(3),4605(4)])].

4668 K(x \ y,x * (y \ x)) = K(x,y)'. [back_rewrite(4274),rewrite([4513(6)])].

4681 K(x,y)' \ (y * x) = x * y. [back_rewrite(4215),rewrite([4513(6),4562(5),22(5)])].

4743 K(x,y)' = K(y,x). [back_rewrite(3592),rewrite([4681(4),4513(5),4562(4),22(4),150(3)]),flip(a)].

4892 K(x,x' * y) = K(x,x * y'). [back_rewrite(4417),rewrite([4562(4)])].

4943 K(x,x * y') = K(x,x * y). [back_rewrite(1803),rewrite([4562(3),4892(5)]),flip(a)].

5012 x * (x' * K(y,x)) = K(y,x). [back_rewrite(3161),rewrite([4892(4),4943(4),4743(4),4605(3),4743(3),4621(6),4743(6)])].

5019 K(x \ y,z) = K(y' * x,z). [back_rewrite(2996),rewrite([4621(4),4743(3),4621(8),4743(6)])].

5021 K(x,x * y) = K(y,x). [back_rewrite(2940),rewrite([4621(9),4743(8),2929(7),4621(2),4743(2)]),flip(a)].

5093 K(x' * y,y * (x \ y)) = K(x,y). [back_rewrite(4668),rewrite([5019(4),4743(7)])].

5168 x * (y * (x' * y')) = K(y,x). [back_rewrite(3153),rewrite([4892(8),5021(8),4562(7),4743(7)])].

5370 K(x * y,(y \ x') * z) = K(z,x * y). [back_rewrite(2294),rewrite([5019(5),112(2),5021(4)]),flip(a)].

5549 K(x,y \ z) = K(x,z' * y). [para(211(a,1),4513(a,1,2)),flip(a)].

6547 K(x,y * (z \ y')) = K(x,y * (z * y')). [para(709(a,1),5549(a,2,2)),rewrite([998(2)]),flip(a)].

6548 K(x,y' * (z * y')) = K(x,y * (z \ y)). [para(942(a,1),5549(a,1,2)),flip(a)].

6553 K(x,y' * (z \ y')) = K(x,y * (z * y)). [para(2587(a,1),5549(a,1,2)),flip(a)].

7096 K(K(x,y) * z,z * (K(y,x) \ z)) = K(K(y,x),z). [para(4743(a,1),5093(a,1,1,1))].

7684 (x * y) * (x * z) = x * ((y' \ x) * z). [para(1006(a,1),56(a,2,2,1)),rewrite([565(4),120(3),214(4),112(2)])].

8245 x' \ (y * (x * (x' \ y))) = x * (x * (x * (y * y))). [para(1561(a,1),1288(a,1,2)),rewrite([1087(3),1087(6),2001(7),5(6),1087(7)]),flip(a)].

10572 a(x * y,x,z) = a(x,y' \ x,z). [para(565(a,1),128(a,1,2,1)),rewrite([7684(3),128(9)]),flip(a)].

10598 a(x * x,y,z) = 1. [para(1087(a,1),128(a,1,1)),rewrite([1087(6),1173(8),25(9)]),flip(a)].

10640 (x * (y' \ z)) \ ((x * (y \ z)) * (y * y)) = a(x,y \ z,y * y). [para(2430(a,1),128(a,1,1,2))].

11403 a(x,y * y,z) = 1. [para(425(a,1),10572(a,1,1)),rewrite([10598(2),120(5),112(4),1165(3),1334(5)]),flip(a)].

11463 x * (x' \ (y * (x' * z))) = y * (x * z). [back_rewrite(1094),rewrite([11403(6),3(4)]),flip(a)].

11500 (x \ y) * (x \ y') = x' * (y * (x' * y')). [back_rewrite(3984),rewrite([11463(10)]),flip(a)].

11503 (x \ y') * (x \ y) = x' * (y * (x' * y')). [back_rewrite(1675),rewrite([11500(8)])].

12074 x \ (y * (z * (x * x))) = x' \ (y * z). [para(1133(a,1),5(a,1,2))].

12096 (x * (y * y)) \ z' = y' * (y \ (x \ z')). [para(1133(a,1),120(a,1,1)),rewrite([120(4),1301(9),112(7),120(7)])].

12136 (x * y) * (z * z) = x * (y * (z * z)). [para(1133(a,1),1033(a,1)),flip(a)].

12154 (x \ (y' * (y \ z'))) * (y * (y * (y * (y * (z * z))))) = x \ (z * (y * y)). [para(1133(a,2),1370(a,1,2)),rewrite([120(3),1165(3),565(9),120(8),308(8),1165(10),112(8),8245(11)])].

12164 x \ (y * (z * z)) = z * (z' \ (x \ y)). [para(850(a,1),1133(a,1,2,2)),rewrite([12136(10),12136(9),850(11)]),flip(a)].

12418 a(x,y \ z,y * y) = 1. [back_rewrite(10640),rewrite([12136(7),2430(6),25(7)]),flip(a)].

12454 (x * (y * (y' \ z))) * a(x,z,y * y) = x * (z * (y * y)). [back_rewrite(1168),rewrite([12136(10)])].

12459 (x \ (y' * (y \ z'))) * (y * (y * (y * (y * (z * z))))) = y * (y' \ (x \ z)). [back_rewrite(12154),rewrite([12164(14)])].

12581 a(x,y,z * z) = 1. [para(5(a,1),12418(a,1,2))].

12605 x * (y * (y' \ z)) = x * (z * (y * y)). [back_rewrite(12454),rewrite([12581(6),3(6)])].

12915 K(x * (x' \ y),(x' * (x \ y')) * z) = K(z,y * (x * x)). [para(1033(a,1),5370(a,2,2)),rewrite([1301(7),112(6)])].

12918 K(x,y * (y' \ z)) = K(x,z * (y * y)). [para(1301(a,1),5370(a,1,2,1)),rewrite([112(6),12915(9)]),flip(a)].

13294 (x * y) * (z * (x * x)) = x * ((y' \ x) * (x' \ z)). [para(1033(a,1),7684(a,1,2))].

14357 x' \ (y * (x' * (x \ z))) = x \ (y * z). [para(364(a,1),12074(a,1,2,2)),rewrite([120(3),308(3),1087(6),12164(6),112(3),2044(4),370(5),850(5),4(2),1165(5)]),flip(a)].

14530 (x * (x' \ y)) \ z' = x' * (x \ (y \ z')). [para(12605(a,1),120(a,1,1)),rewrite([120(4),12096(4)]),flip(a)].

14555 x \ (y * (y' \ z)) = y * (y' \ (x \ z)). [para(12605(a,1),1370(a,1,2)),rewrite([120(4),1301(4),112(3),13294(11),211(8),942(9),2543(11),12459(11)]),flip(a)].

14778 x * (x' \ (y * ((x' * (x \ y')) * K(z,y * (x * x))))) = K(z,x * (x' \ y)). [para(12918(a,1),5012(a,1,2,2)),rewrite([120(7),1301(7),112(6),1173(12)])].

14790 x * (x' \ (((x' * (x \ y')) \ z) \ (z' \ y))) = K(z,y * (x * x)). [para(12918(a,1),4321(a,2)),rewrite([120(4),1301(4),112(3),14555(10),14555(11)])].

15350 x \ ((y * x) \ (z' * (z \ x))) = z' * (z \ (y \ x')). [para(425(a,1),196(a,1,1,1)),rewrite([1087(2),14530(5),120(10),112(9),1165(8)]),flip(a)].

15491 (x * (x' \ y)) \ (z \ u) = x' * (x \ (y \ (z \ u))). [para(871(a,1),196(a,1,1,1)),rewrite([1087(2),120(6),112(5),120(14),211(13),1165(14),15350(17),120(9),112(8)])].

16015 (x' * (x \ y)) * z = x' * (x \ (y * z)). [para(112(a,1),1173(a,1,1,2,1)),rewrite([112(7)])].

16036 (x' * (x \ y')) \ z = x * (x' \ (y' \ z)). [para(1173(a,1),2052(a,1,2)),rewrite([120(8),1301(8),112(7),16015(9),14357(11),4(8),1173(7),2052(5),120(9),1301(9),112(8)]),flip(a)].

16146 x * (x' * K(y,x * (z * z))) = K(y,z * (z' \ x)). [back_rewrite(14778),rewrite([16015(9),14357(11),4(8)])].

16208 K(x,y * (z * z)) = K(x,y). [back_rewrite(14790),rewrite([16036(6),15491(9),4321(7),5(6),4(3)]),flip(a)].

16260 K(x,y * (y' \ z)) = K(x,z). [back_rewrite(16146),rewrite([16208(4),5012(4)]),flip(a)].

16634 K(x,y' * z) = K(x,y * z). [para(5(a,1),16260(a,1,2,2)),flip(a)].

16738 K(x,y * (z * y')) = K(x,y * (z * y)). [back_rewrite(6553),rewrite([16634(5),6547(4)])].

16741 K(x,y * (z \ y)) = K(x,y * (z * y)). [back_rewrite(6548),rewrite([16634(5),16738(4)]),flip(a)].

16932 K(K(x,y) * z,z * (K(y,x) * z)) = K(K(y,x),z). [back_rewrite(7096),rewrite([16741(6)])].

17286 K(x,y * (z' * y)) = K(x,z). [para(121(a,1),16634(a,2,2)),rewrite([211(2),565(4),16741(6),16634(6),16738(5),4513(6)])].

17288 K(x,y * (y * z)) = K(x,z). [para(30(a,1),16634(a,2,2)),rewrite([120(2),364(3),16738(5),17286(4)]),flip(a)].

17289 K(x,y * (z * y)) = K(x,z). [para(364(a,1),16634(a,2,2)),rewrite([211(2),30(3),17288(4),4513(2),16738(5)]),flip(a)].

17291 K(x,K(y,z)) = 1. [para(1365(a,1),16634(a,2,2)),rewrite([120(2),11503(4),16634(7),5168(5),267(4)])].

17420 K(K(x,y),z) = 1 # label(non_clause) # label(goal). [back_rewrite(16932),rewrite([17289(6),17291(4)]),flip(a)].

17421 $F. [resolve(17420,a,23,a)].

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

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

Given=316. Generated=45776. Kept=17413. proofs=1.

Usable=191. Sos=6895. Demods=6513. Limbo=131, Disabled=10211. Hints=5294.

Kept_by_rule=0, Deleted_by_rule=0.

Forward_subsumed=28363. Back_subsumed=398.

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

New_demodulators=16197 (13 lex), Back_demodulated=9797. Back_unit_deleted=0.

Demod_attempts=981550. Demod_rewrites=187583.

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

Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.

Megabytes=17.18.

User_CPU=3.32, System_CPU=0.11, Wall_clock=4.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 4110 exit (max_proofs) Wed Oct 7 11:26:58 2009

% Length of proof is 28.

% Level of proof is 7.

% Maximum clause weight is 23.

% Given clauses 26.

1 a(K(x,y),u,v) = 1 # label(non_clause) # label(goal). [goal].

2 1 * x = x. [assumption].

3 x * 1 = x. [assumption].

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

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

9 (x * (y * z)) * z = z * ((z * x) * y). [copy(8),flip(a)].

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

13 (x * y) * (y \ (z * y)) = (x * z) * y. [copy(12),flip(a)].

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

19 (x * y) * z = (x * (y * z)) * a(x,y,z). [assumption].

20 (x * (y * z)) * a(x,y,z) = (x * y) * z. [copy(19),flip(a)].

21 x * y = (y * x) * K(x,y). [assumption].

22 (x * y) * K(y,x) = y * x. [copy(21),flip(a)].

23 K(K(x,y),z) = 1. [assumption].

24 a(K(c1,c2),c3,c4) != 1. [deny(1)].

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

57 (x * y) * (y * z) = y * ((y * x) * z). [para(9(a,1),13(a,2)),rewrite([31(3),5(4)])].

98 x \ (y * x) = (x' * y) * x. [para(17(a,1),13(a,1,1)),rewrite([2(4)])].

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

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

164 K(x,y) * z = z * K(x,y). [para(23(a,1),22(a,1,2)),rewrite([3(4)]),flip(a)].

198 K(x,y) * (K(x,y)' * z) = z. [para(164(a,1),5(a,1,2)),rewrite([98(4),164(5,R)])].

206 K(x,y) * ((K(x,y) * z) * u) = K(x,y) * (z * (u * K(x,y))). [para(164(a,1),9(a,2)),rewrite([164(5,R),164(10,R)]),flip(a)].

212 (K(x,y) * z) * u = (z * K(x,y)) * u. [para(164(a,1),20(a,2,1)),rewrite([20(6)])].

269 (x * K(y,z)) * u = K(y,z) * (x * u). [para(198(a,1),57(a,1,2)),rewrite([206(11),164(9,R),198(9)])].

276 (K(x,y) * z) * u = K(x,y) * (z * u). [back_rewrite(212),rewrite([269(6)])].

365 a(K(x,y),z,u) = 1 # label(non_clause) # label(goal). [para(164(a,1),129(a,1,1)),rewrite([276(6),151(7),23(3)]),flip(a)].

366 $F. [resolve(365,a,24,a)].

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

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

Given=26. Generated=815. Kept=358. proofs=1.

Usable=23. Sos=226. Demods=244. Limbo=35, Disabled=90. Hints=46.

Kept_by_rule=0, Deleted_by_rule=0.

Forward_subsumed=457. Back_subsumed=7.

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

New_demodulators=307 (2 lex), Back_demodulated=66. Back_unit_deleted=0.

Demod_attempts=9889. Demod_rewrites=1347.

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

Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.

Megabytes=0.44.

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

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 4152 exit (max_proofs) Wed Oct 7 11:31:55 2009

% Length of proof is 78.

% Level of proof is 16.

% Maximum clause weight is 26.

% Given clauses 66.

1 a(u,v,K(x,y)) = 1 # label(non_clause) # label(goal). [goal].

2 1 * x = x. [assumption].

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 * y) * z) = (y * (z * x)) * x. [assumption].

9 (x * (y * z)) * z = z * ((z * x) * y). [copy(8),flip(a)].

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

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

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

13 (x * y) * (y \ (z * y)) = (x * z) * y. [copy(12),flip(a)].

16 x * ((y * x) \ 1) = y \ 1. [assumption].

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

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

19 (x * y) * z = (x * (y * z)) * a(x,y,z). [assumption].

20 (x * (y * z)) * a(x,y,z) = (x * y) * z. [copy(19),flip(a)].

21 x * y = (y * x) * K(x,y). [assumption].

22 (x * y) * K(y,x) = y * x. [copy(21),flip(a)].

23 K(K(x,y),z) = 1. [assumption].

24 a(K(x,y),z,u) = 1. [assumption].

25 a(c1,c2,K(c3,c4)) != 1. [deny(1)].

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

32 (x * y) * y = y * (y * x). [para(2(a,1),9(a,1,1,2)),rewrite([3(5)])].

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

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

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

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

96 1 / x = x'. [para(17(a,1),6(a,1,1))].

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

99 x \ (y * x) = (x' * y) * x. [para(17(a,1),13(a,1,1)),rewrite([2(4)])].

113 x \ 1 = x'. [para(18(a,1),5(a,1,2))].

114 x'' = x. [para(18(a,1),6(a,1,1)),rewrite([96(3)])].

121 (x / y)' = y * x'. [back_rewrite(89),rewrite([113(3),113(4)])].

122 (x * y)' = y \ x'. [back_rewrite(88),rewrite([113(3),113(4)])].

123 (x \ y) * y' = x'. [back_rewrite(87),rewrite([113(3),113(5)])].

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

134 (x * ((x \ y) * z)) * a(y / x,x,z) = y * z. [para(7(a,1),20(a,2,1)),rewrite([40(3)])].

152 (x * y) \ (y * x) = K(y,x). [para(22(a,1),5(a,1,2))].

153 (x * y) / K(x,y) = y * x. [para(22(a,1),6(a,1,1))].

165 K(x,y) * z = z * K(x,y). [para(23(a,1),22(a,1,2)),rewrite([3(4)]),flip(a)].

174 x / y = x' \ y'. [para(121(a,1),114(a,1,1)),rewrite([122(3)]),flip(a)].

175 (x \ y')' = y * x. [para(114(a,1),121(a,2,2)),rewrite([174(2),114(2)])].

178 (x \ y') \ K(y,x)' = x * y. [back_rewrite(153),rewrite([174(3),122(2)])].

179 (x * ((x \ y) * z)) * a(y' \ x',x,z) = y * z. [back_rewrite(134),rewrite([174(4)])].

213 (x \ y') * y = x'. [para(114(a,1),123(a,1,2))].

219 (x \ y)' = y' * x. [para(114(a,1),175(a,1,1,2))].

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

277 K(x,y) * (K(x,y)' * z) = z. [para(165(a,1),5(a,1,2)),rewrite([99(4),165(5,R)])].

288 (x * K(y,z)) * u = K(y,z) * (x * u). [para(165(a,1),20(a,2,1)),rewrite([24(5),3(5)]),flip(a)].

291 K(x,y) \ z' = z \ K(x,y)'. [para(165(a,1),122(a,1,1)),rewrite([122(3)])].

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

314 K(x,y)' * (z * K(x,y)) = z. [para(165(a,1),241(a,1,1)),rewrite([99(6),122(3),213(4)])].

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

343 (K(x,y) \ z) \ z = K(x,y). [para(165(a,2),327(a,1,1)),rewrite([4(6)])].

347 x' * (K(y,z) \ x) = K(y,z)'. [para(343(a,1),219(a,1,1)),flip(a)].

349 K(x,y) \ z = K(x,y)' * z. [para(343(a,1),300(a,1,1,1)),rewrite([4(4),99(4),347(4)]),flip(a)].

353 (K(x,y)' * z) \ z = K(x,y). [back_rewrite(343),rewrite([349(2)])].

354 x \ K(y,z)' = K(y,z)' * x'. [back_rewrite(291),rewrite([349(3)]),flip(a)].

357 K(x,y)' * (x * y) = y * x. [back_rewrite(178),rewrite([354(5),219(5),114(4)])].

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

360 (x' * y) * x = (x * y) * x'. [para(97(a,1),5(a,1,2)),rewrite([99(2)])].

405 (x * (y * x')) \ (x * y) = x. [back_rewrite(300),rewrite([358(2)])].

419 x \ (y * x) = (x * y) * x'. [back_rewrite(99),rewrite([360(5)])].

447 (x * K(y,z)') \ x = K(y,z). [para(97(a,1),353(a,1,1)),rewrite([114(9),165(8,R),277(8)])].

492 K(x,y)' = K(y,x). [para(357(a,1),405(a,1,2)),rewrite([114(6),314(6),152(3)]),flip(a)].

499 (x * K(y,z)) \ x = K(z,y). [back_rewrite(447),rewrite([492(2)])].

508 K(x,y) \ z = K(y,x) * z. [back_rewrite(349),rewrite([492(4)])].

509 K(x,y) * (K(y,x) * z) = z. [back_rewrite(277),rewrite([492(3)])].

830 (x * (y * K(z,u))) \ (K(z,u) * (x * y)) = a(x,K(z,u),y). [para(165(a,1),130(a,1,1,2)),rewrite([288(6)])].

833 a(x,K(y,z),u) = a(x,u,K(y,z)). [para(165(a,2),130(a,1,2)),rewrite([830(7)])].

842 (x * y) \ (K(z,u) * (x * (K(u,z) * y))) = a(x,K(z,u),K(u,z) * y). [para(509(a,1),130(a,1,1,2)),rewrite([288(6)])].

869 a(c1,K(c3,c4),c2) != 1. [para(833(a,2),25(a,1))].

920 K(x,y) * (z * (K(y,x) * u)) = z * u. [para(499(a,1),179(a,1,1,2,1)),rewrite([288(5),122(9),508(9),419(10),114(10),288(9),17(8),3(8),24(9),3(7)])].

940 a(x,K(y,z),K(z,y) * u) = 1. [back_rewrite(842),rewrite([920(6),27(3)]),flip(a)].

944 a(x,K(y,z),u) = 1. [para(4(a,1),940(a,1,3))].

945 $F. [resolve(944,a,869,a)].

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

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

Given=66. Generated=2489. Kept=937. proofs=1.

Usable=49. Sos=587. Demods=588. Limbo=1, Disabled=317. Hints=323.

Kept_by_rule=0, Deleted_by_rule=0.

Forward_subsumed=1552. Back_subsumed=13.

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

New_demodulators=873 (2 lex), Back_demodulated=286. Back_unit_deleted=0.

Demod_attempts=34880. Demod_rewrites=5959.

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

Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.

Megabytes=1.17.

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

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 4175 exit (max_proofs) Wed Oct 7 11:34:37 2009

% Length of proof is 273.

% Level of proof is 41.

% Maximum clause weight is 27.

% Given clauses 233.

1 K(a(x,y,z),u) = 1 # label(non_clause) # label(goal). [goal].

2 1 * x = x. [assumption].

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 * y) * z) = (y * (z * x)) * x. [assumption].

9 (x * (y * z)) * z = z * ((z * x) * y). [copy(8),flip(a)].

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

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

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

13 (x * y) * (y \ (z * y)) = (x * z) * y. [copy(12),flip(a)].

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

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

16 x * ((y * x) \ 1) = y \ 1. [assumption].

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

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

19 (x * y) * z = (x * (y * z)) * a(x,y,z). [assumption].

20 (x * (y * z)) * a(x,y,z) = (x * y) * z. [copy(19),flip(a)].

21 x * y = (y * x) * K(x,y). [assumption].

22 (x * y) * K(y,x) = y * x. [copy(21),flip(a)].

23 K(K(x,y),z) = 1. [assumption].

24 a(K(x,y),z,u) = 1. [assumption].

25 a(x,y,K(z,u)) = 1. [assumption].

26 K(a(c1,c2,c3),c4) != 1. [deny(1)].

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

33 (x * y) * y = y * (y * x). [para(2(a,1),9(a,1,1,2)),rewrite([3(5)])].

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

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

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

59 (x * y) * (y * z) = y * ((y * x) * z). [para(9(a,1),13(a,2)),rewrite([33(3),5(4)])].

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

81 (x * (y * y)) * z = (y * y) * (x * z). [para(15(a,2),13(a,2)),rewrite([62(6)])].

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

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

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

95 1' = 1. [para(17(a,1),3(a,1)),flip(a)].

97 1 / x = x'. [para(17(a,1),6(a,1,1))].

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

100 x \ (y * x) = (x' * y) * x. [para(17(a,1),13(a,1,1)),rewrite([2(4)])].

101 (x * y) * (y \ 1) = (x * y') * y. [para(17(a,1),13(a,1,2,2))].

111 (x * y) \ ((x * z) * y) = (y' * z) * y. [back_rewrite(52),rewrite([100(6)])].

114 x \ 1 = x'. [para(18(a,1),5(a,1,2))].

115 x'' = x. [para(18(a,1),6(a,1,1)),rewrite([97(3)])].

118 (x * y') * y = (x * y) * y'. [back_rewrite(101),rewrite([114(3)]),flip(a)].

122 (x / y)' = y * x'. [back_rewrite(90),rewrite([114(3),114(4)])].

123 (x * y)' = y \ x'. [back_rewrite(89),rewrite([114(3),114(4)])].

124 (x \ y) * y' = x'. [back_rewrite(88),rewrite([114(3),114(5)])].

152 x * K(y \ x,y) = (y \ x) * y. [para(4(a,1),22(a,1,1))].

153 (x * y) \ (y * x) = K(y,x). [para(22(a,1),5(a,1,2))].

154 (x * y) / K(x,y) = y * x. [para(22(a,1),6(a,1,1))].

162 (x * (y * z)) * K(z,y) = x * (z * y). [para(22(a,1),20(a,1,1,2)),rewrite([25(5),3(4)]),flip(a)].

163 x * (y * K(y,x)) = y * x. [para(22(a,1),20(a,2)),rewrite([25(5),3(5)])].

167 K(x,y) * z = z * K(x,y). [para(23(a,1),22(a,1,2)),rewrite([3(4)]),flip(a)].

169 K(x,y) * (z * (y * x)) = z * (x * y). [back_rewrite(162),rewrite([167(4,R)])].

171 (K(x,y) * z) * u = K(x,y) * (z * u). [para(24(a,1),20(a,1,2)),rewrite([3(5)]),flip(a)].

173 (x * y) * K(z,u) = x * (y * K(z,u)). [para(25(a,1),20(a,1,2)),rewrite([3(5)]),flip(a)].

180 x / y = x' \ y'. [para(122(a,1),115(a,1,1)),rewrite([123(3)]),flip(a)].

181 (x \ y')' = y * x. [para(115(a,1),122(a,2,2)),rewrite([180(2),115(2)])].

184 (x \ y') \ K(y,x)' = x * y. [back_rewrite(154),rewrite([180(3),123(2)])].

200 ((x \ y') \ y') * z = y * (x * (y \ z)). [back_rewrite(42),rewrite([180(2),123(2)])].

201 (x' \ y') * (y * z) = y * ((y \ x) * z). [back_rewrite(41),rewrite([180(1)])].

217 (x \ y') * y = x'. [para(115(a,1),124(a,1,2))].

226 (x \ y)' = y' * x. [para(115(a,1),181(a,1,1,2))].

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

273 x * (x * (y \ x')) = y' * x. [para(217(a,1),33(a,1,1)),flip(a)].

275 K(x,1) = 1. [para(2(a,1),153(a,1,1)),rewrite([3(2),28(1)]),flip(a)].

280 K(x,y * y) = 1. [para(15(a,1),153(a,1,1)),rewrite([28(5)]),flip(a)].

284 K(x,x) = 1. [para(153(a,1),28(a,1))].

285 K(x,y) * (y \ x') = x \ y'. [para(153(a,1),124(a,1,1)),rewrite([123(3),123(6)])].

298 (x' * y) * x = y * K(y,x). [para(163(a,1),5(a,1,2)),rewrite([100(2)])].

304 a(x,y,z) * (x * (y * (z * K(x * (y * z),a(x,y,z))))) = (x * y) * z. [para(20(a,1),163(a,2)),rewrite([173(8),173(7)])].

310 K(x * K(x,y),y) = (y' * K(x,y)) * y. [para(163(a,1),153(a,1,1)),rewrite([111(5)]),flip(a)].

312 K(x,y) * (K(x,y)' * z) = z. [para(167(a,1),5(a,1,2)),rewrite([100(4),167(5,R)])].

323 (x * K(y,z)) * u = K(y,z) * (x * u). [para(167(a,1),20(a,2,1)),rewrite([24(5),3(5)]),flip(a)].

325 K(x,y) \ z' = z \ K(x,y)'. [para(167(a,1),123(a,1,1)),rewrite([123(3)])].

329 K(x,K(y,z)) = 1. [para(167(a,1),153(a,1,1)),rewrite([28(5)]),flip(a)].

330 K(x * K(x,y),y) = K(x,y). [back_rewrite(310),rewrite([323(7),17(6),3(6)])].

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

340 x' * (x * (y * y)) = y * y. [para(15(a,1),261(a,1,2,2)),rewrite([100(7),123(3),15(5,R),4(5)])].

343 x' * (x * x) = x. [para(15(a,2),261(a,1,2)),rewrite([15(3),100(4),123(2),217(3)])].

351 K(x,y)' * (z * K(x,y)) = z. [para(167(a,1),261(a,1,1)),rewrite([100(6),123(3),217(4)])].

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

365 x \ x' = x' * x'. [para(115(a,1),355(a,1,1))].

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

396 (x' * y') * x = x * (y \ x'). [para(336(a,1),124(a,1,1)),rewrite([123(2),123(6),226(5),100(6)]),flip(a)].

409 ((x * x) \ y) \ y = x * x. [para(15(a,2),392(a,1,1)),rewrite([4(6)])].

415 (K(x,y) \ z) \ z = K(x,y). [para(167(a,2),392(a,1,1)),rewrite([4(6)])].

422 x' * ((y * y) \ x) = y' * y'. [para(409(a,1),226(a,1,1)),rewrite([123(2),365(2)]),flip(a)].

424 (x * x) \ y = (x' * x') * y. [para(409(a,1),336(a,1,1,1)),rewrite([4(4),100(4),422(4)]),flip(a)].

435 x' * (K(y,z) \ x) = K(y,z)'. [para(415(a,1),226(a,1,1)),flip(a)].

436 K(x,y) \ z = K(x,y)' * z. [para(415(a,1),336(a,1,1,1)),rewrite([4(4),100(4),435(4)]),flip(a)].

442 x \ K(y,z)' = K(y,z)' * x'. [back_rewrite(325),rewrite([436(3)]),flip(a)].

445 K(x,y)' * (x * y) = y * x. [back_rewrite(184),rewrite([442(5),226(5),115(4)])].

446 (x \ y) * x = x * (y * x'). [para(4(a,1),98(a,1,2,1)),flip(a)].

448 (x' * y) * x = (x * y) * x'. [para(98(a,1),5(a,1,2)),rewrite([100(2)])].

450 (x * y) * y' = y' * (y * x). [para(98(a,1),9(a,1,1)),rewrite([17(6),2(7)])].

453 x' * (x * y) = x * (x' * y). [para(9(a,1),98(a,1,2)),rewrite([17(3),2(3),118(6),450(6)]),flip(a)].

468 x * (y * K(x,y)) = y * (y * (y' * x)). [para(163(a,1),98(a,1,2,1)),rewrite([450(3),453(3),323(7),167(7),173(7)]),flip(a)].

497 (x * (y * x')) \ (x * y) = x. [back_rewrite(336),rewrite([446(2)])].

501 x * K(y \ x,y) = y * (x * y'). [back_rewrite(152),rewrite([446(5)])].

502 (x * y') * x' = x * (y \ x'). [back_rewrite(396),rewrite([448(4)])].

503 (x * y) * x' = y * K(y,x). [back_rewrite(298),rewrite([448(3)])].

512 x \ (y * x) = (x * y) * x'. [back_rewrite(100),rewrite([448(5)])].

516 (x * y') * y = y * (y' * x). [back_rewrite(118),rewrite([450(6),453(6)])].

517 (x * y) * y' = y * (y' * x). [back_rewrite(450),rewrite([453(6)])].

519 x * (x' * (y * y)) = y * y. [back_rewrite(340),rewrite([453(4)])].

544 x * (K(y,z)' * x') = K(y,z)'. [para(351(a,1),261(a,1,2,2)),rewrite([517(5),312(5),512(4),502(5),436(3)])].

550 x \ K(y,z) = x' * K(y,z). [para(436(a,1),226(a,1,1)),rewrite([123(4),115(3)])].

557 x * ((x * K(y,x)') * y) = (x * y) * x. [para(445(a,1),9(a,1,1)),flip(a)].

569 K(x,y)' * (x * (y * K(x,y))) = x * y. [para(163(a,1),445(a,2)),rewrite([330(3),323(5),167(5),173(5)])].

589 (x * y') \ y' = y * (x \ y'). [para(446(a,1),123(a,1,1)),rewrite([123(4),226(6),512(7),502(8)])].

605 K(x,y)' = K(y,x). [para(445(a,1),497(a,1,2)),rewrite([115(6),173(5),569(6),153(3)]),flip(a)].

618 x * (x * (y * K(x,y))) = (x * y) * x. [back_rewrite(557),rewrite([605(2),323(3),167(3),173(3)])].

626 x * (K(y,z) * x') = K(y,z). [back_rewrite(544),rewrite([605(2),605(6)])].

632 K(x,y) \ z = K(y,x) * z. [back_rewrite(436),rewrite([605(4)])].

636 K(x,y * K(y,x)) = K(x,y). [para(330(a,1),605(a,1,1)),rewrite([605(2)]),flip(a)].

639 K(x,K(y,x) * (y * K(y,x))) = K(x,y). [para(330(a,1),636(a,1,2,2)),rewrite([167(4,R),636(8)])].

640 (x \ y) * K(x \ y,x) = y * x'. [para(4(a,1),503(a,1,1)),flip(a)].

642 x \ ((y * x) * y') = K(x,y). [para(503(a,2),5(a,1,2))].

664 x * (y' * K(x,y)) = y * (y' * (y' * x)). [para(503(a,1),33(a,1,1)),rewrite([323(4),167(4),173(4),453(8),453(9)])].

668 (x * K(x,y)) \ (y * (y' * x)) = K(y',y * x). [para(503(a,1),153(a,1,1)),rewrite([453(5)])].

673 K(x,y) * (x * K(x,y)) = y * (y' * x). [para(163(a,1),503(a,1,1)),rewrite([517(3),330(8),167(7,R)]),flip(a)].

690 K(x,x * (x' * y)) = K(x,y). [back_rewrite(639),rewrite([673(4)])].

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

733 (x * y) * (K(z,u) * (y \ x')) = K(z,u). [para(626(a,1),20(a,2)),rewrite([123(3),123(9),20(12)])].

741 K(x,y') = K(x,y). [para(115(a,1),642(a,1,2,2)),rewrite([448(3),642(4)]),flip(a)].

749 K(x',x * y) = K(y,x). [para(163(a,1),642(a,1,2,1)),rewrite([517(5),668(6),330(6)])].

758 K(x,y \ z) = K(x,z' * y). [para(226(a,1),741(a,1,2)),flip(a)].

759 x' * (y * K(y,x)) = y * x'. [para(741(a,1),163(a,1,2,2))].

760 K(x',y) = K(x,y). [para(741(a,1),605(a,1,1)),rewrite([605(2)]),flip(a)].

777 K(x,x * y) = K(y,x). [back_rewrite(749),rewrite([760(3)])].

785 K(x' * y,x) = K(x,y). [back_rewrite(690),rewrite([777(4)])].

787 K(x \ y,z) = K(y' * x,z). [para(226(a,1),760(a,1,1)),flip(a)].

788 x * (y' * K(y,x)) = y' * x. [para(760(a,1),163(a,1,2,2))].

794 (x \ y) * K(y' * x,x) = y * x'. [back_rewrite(640),rewrite([787(3)])].

795 x * K(x' * y,y) = y * (x * y'). [back_rewrite(501),rewrite([787(2)])].

801 K(x * y,y) = K(y,x). [para(217(a,1),777(a,1,2)),rewrite([741(4),787(3),115(2),758(5),115(4),777(4)])].

804 K(x,y * x) = K(y,x). [para(163(a,1),777(a,1,2)),rewrite([330(5)])].

807 K(x * y,x) = K(x,y). [para(777(a,1),605(a,1,1)),rewrite([605(2)]),flip(a)].

814 K(x,x' * y) = K(y,x). [para(777(a,1),760(a,1)),rewrite([741(2)]),flip(a)].

816 x * K(y,x) = y * (x * y'). [back_rewrite(795),rewrite([801(3),741(2)])].

817 K(x,y) * (x \ y) = y * x'. [back_rewrite(794),rewrite([801(4),741(3),167(3,R)])].

835 K((x * y) * z,a(x,y,z)) = K(a(x,y,z),x * (y * z)). [para(20(a,1),801(a,1,1))].

838 K(x,y * x') = K(y,x). [para(446(a,1),801(a,1,1)),rewrite([807(4),758(5),804(6),760(5)])].

843 K(x * (y * z),a(x,y,z)) = K(a(x,y,z),(x * y) * z). [para(20(a,1),804(a,1,2)),flip(a)].

848 a(x,y,z) * (x * (y * (z * K(a(x,y,z),(x * y) * z)))) = (x * y) * z. [back_rewrite(304),rewrite([843(5)])].

851 K((x * y) * z,x * (y * z)) = K(a(x,y,z),(x * y) * z). [para(20(a,1),807(a,1,1)),rewrite([843(9)])].

957 K(x,y) * (y * z) = (x * (y * x')) * z. [para(816(a,1),20(a,2,1)),rewrite([20(6),323(3)])].

1004 x * (y' * K(x,y)) = y \ x. [para(817(a,1),5(a,1,2)),rewrite([632(4),167(4),173(4)])].

1010 x' * (y * K(x,y)) = y' \ x'. [para(817(a,1),123(a,1,1)),rewrite([123(3),605(6),550(6),226(5),173(7)]),flip(a)].

1022 K(x,y) * (x \ y') = y' * x'. [para(741(a,1),817(a,1,1))].

1030 x * (x' * (x' * y)) = x \ y. [back_rewrite(664),rewrite([1004(4)]),flip(a)].

1042 x * (y * K(x,y)) = y' \ x. [para(115(a,1),1004(a,1,2,1)),rewrite([741(2)])].

1061 (x * y) \ x = x * (x' * y'). [para(777(a,1),1004(a,1,2,2)),rewrite([123(2),167(4,R),1022(4)]),flip(a)].

1065 (x * y) \ y = y * (x \ y'). [para(804(a,1),1004(a,1,2,2)),rewrite([123(2),167(4,R),285(4)]),flip(a)].

1068 (x' * y) \ x = x * (x * y'). [para(814(a,1),1004(a,1,2,2)),rewrite([123(3),115(2),167(3,R),817(3)]),flip(a)].

1069 x * (K(y,x) * (x' \ y')) = (y * x') \ x. [para(838(a,1),1004(a,1,2,2)),rewrite([123(3),167(5,R)])].

1080 (x * y) * x = x * (y' \ x). [back_rewrite(618),rewrite([1042(3)]),flip(a)].

1082 x * (x * (x' * y)) = x' \ y. [back_rewrite(468),rewrite([1042(3)]),flip(a)].

1087 x' * (y \ x) = x * (y \ x'). [back_rewrite(589),rewrite([1065(4),115(3)])].

1115 (x \ y') \ y = (y' \ x) * y. [para(1042(a,1),9(a,2)),rewrite([777(2),167(2),1042(3),123(5)]),flip(a)].

1129 (x' \ y) * x = x * (y * x). [para(777(a,1),1042(a,1,2,2)),rewrite([173(3),163(3),123(4),1115(5)]),flip(a)].

1133 (x \ y') \ x = x * (x' \ y). [para(804(a,1),1042(a,1,2,2)),rewrite([173(3),1042(3),123(5)]),flip(a)].

1136 (x \ y) \ y = y * (x * y'). [para(814(a,1),1042(a,1,2,2)),rewrite([173(4),759(4),123(6),115(5)]),flip(a)].

1145 (x' * (y * x)) * z = x * (y * (x \ z)). [back_rewrite(200),rewrite([1136(4),115(3)])].

1192 (x' \ y) \ y' = y \ (x \ y'). [para(1080(a,1),123(a,1,1)),rewrite([123(4),123(6)])].

1207 x * ((y * K(y,x)) \ x) = (y \ x) * x. [para(1004(a,1),1080(a,1,1)),rewrite([123(6),115(5),632(4),167(4)]),flip(a)].

1217 (x \ y) * x' = x' * (y * x'). [para(115(a,1),1129(a,1,1,1))].

1354 K(x,y) * (y' \ x') = x \ y. [para(115(a,1),285(a,2,2)),rewrite([741(2)])].

1373 (x * y') \ y = y * (x \ y). [back_rewrite(1069),rewrite([1354(5)]),flip(a)].

1386 (x \ y) \ y' = y' * (x * y'). [para(1373(a,1),226(a,1,1)),rewrite([123(3)])].

1392 (x * K(x,y)) \ y = y' \ x'. [para(503(a,1),1373(a,1,1)),rewrite([1061(5),1082(8)])].

1407 x \ (y \ x') = x' * (y' * x'). [back_rewrite(1192),rewrite([1386(4)]),flip(a)].

1409 (x \ y) * y = y * (y' \ x'). [back_rewrite(1207),rewrite([1392(3)]),flip(a)].

1448 (x * y) * x' = x * (y' \ x'). [para(448(a,1),163(a,2)),rewrite([785(5),173(4),1010(4)]),flip(a)].

1459 x * (x' * (x \ y)) = x' * y. [para(816(a,2),448(a,2,1)),rewrite([448(5),1448(5),123(3),1133(5),115(3),323(8),167(8),173(8),788(8)])].

1514 x \ (y * (x' \ y')) = K(x,y). [back_rewrite(642),rewrite([1448(3)])].

1540 (x \ y') * (x * (x * y)) = x * ((x * y) * (y' * x')). [para(33(a,1),453(a,1,2)),rewrite([123(2),123(8),446(9),59(11)])].

1541 x' * (y * x) = x * (y * x'). [para(163(a,1),453(a,1,2)),rewrite([759(7)])].

1552 (x * (y * x')) * (x * y) = (x * y) * (x * (x' * y)). [para(453(a,1),1129(a,2,2)),rewrite([123(2),1136(4),115(3),1541(3)])].

1558 (x * y) * ((x * y) * (x' * (y' * x'))) = x * (x' * y). [para(453(a,1),273(a,2)),rewrite([123(4),1407(5)])].

1576 (x * (y * x')) * z = x * (y * (x \ z)). [back_rewrite(1145),rewrite([1541(3)])].

1583 (x * y) * (x * (x' * y)) = x * (y * y). [back_rewrite(1552),rewrite([1576(5),5(2)]),flip(a)].

1588 K(x,y) * (y * z) = x * (y * (x \ z)). [back_rewrite(957),rewrite([1576(7)])].

1633 x \ (x' \ y) = x * (x' * y). [para(4(a,1),1030(a,1,2,2)),flip(a)].

1730 (x \ y) \ x = x * (x' \ y'). [para(1030(a,1),1061(a,1,1)),rewrite([123(8),115(7),1068(6),453(7),453(6),1082(7)])].

1800 (x * y) * (x' * (y' * x')) = y * (x' * y'). [para(5(a,1),1087(a,1,2)),rewrite([123(2),446(3),123(7),1407(8)]),flip(a)].

1818 x * ((x * y) * (y' * x')) = y * (y' * x). [back_rewrite(1558),rewrite([1800(8),59(6)])].

1826 (x \ y') * (x * (x * y)) = y * (y' * x). [back_rewrite(1540),rewrite([1818(11)])].

2000 x' \ (x \ y) = x * (x' * y). [para(1459(a,1),1082(a,1,2)),flip(a)].

2177 x * (x' \ y) = y * (x * x). [para(261(a,1),2000(a,1,2)),rewrite([123(2),1730(3),115(3),123(6),1826(9),1583(8)])].

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

2213 (x * x) * y = x * (x' \ y). [para(2177(a,2),15(a,2))].

2215 (x * (x' \ y)) * z = x * (x' \ (y * z)). [para(2177(a,1),20(a,2,1)),rewrite([20(8),81(7),2213(7)])].

2220 (x * y) * (z * z) = z * (z' \ (x * y)). [para(2177(a,2),20(a,2)),rewrite([20(6)])].

2304 (x * x) \ y = x' * (x \ y). [back_rewrite(424),rewrite([2213(6),115(5)])].

2308 (x * (y * y)) * z = y * (y' \ (x * z)). [back_rewrite(81),rewrite([2213(6)])].

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

2780 (x * y) * (x * z) = x * ((y' \ x) * z). [para(1042(a,1),59(a,2,2,1)),rewrite([323(3),167(3),173(3),163(3)])].

3064 x * (y * (z * K(z * y,x))) = K(y,z) * ((z * y) * x). [para(169(a,1),169(a,1,2)),rewrite([167(5),173(5),173(4)])].

3086 x \ (y' * K(z,u)) = (x \ y') * K(z,u). [para(171(a,1),123(a,1,1)),rewrite([123(4),605(3),550(3),123(2),123(7),605(6),550(6)]),flip(a)].

3115 K(x,K(y,z) * (u * x')) = K(K(y,z) * u,x). [para(171(a,1),838(a,1,2))].

3147 x \ (K(y,z) * (u * ((x' \ u') * K(z,y)))) = K(x,K(y,z) * u). [para(171(a,1),1514(a,1,2)),rewrite([123(5),605(4),550(4),3086(6)])].

3204 K(x,y) * (z * (u * K(y,x))) = z * u. [para(173(a,1),497(a,1,2)),rewrite([123(4),733(6),632(5)])].

3261 K(x,K(y,z) * u) = K(x,u). [back_rewrite(3147),rewrite([3204(8),1514(5)]),flip(a)].

3280 K(K(x,y) * z,u) = K(z,u). [back_rewrite(3115),rewrite([3261(5),838(3)]),flip(a)].

3313 K(x,y * K(z,u)) = K(x,y). [para(163(a,1),3261(a,1,2)),rewrite([329(5),3(5)])].

3320 K(x,y * z) = K(x,z * y). [para(285(a,1),3261(a,1,2)),rewrite([758(3),115(2),758(5),115(4)])].

3329 K(x,y * (z * u)) = K(x,y * (u * z)). [para(169(a,1),3261(a,1,2))].

3378 K(x * K(y,z),u) = K(x,u). [para(163(a,1),3280(a,1,1)),rewrite([329(5),3(5)])].

3383 K(x * y,z) = K(y * x,z). [para(285(a,1),3280(a,1,1)),rewrite([787(3),115(2),787(5),115(4)])].

3392 K(x * (y * z),u) = K(x * (z * y),u). [para(169(a,1),3280(a,1,1))].

3504 K(x,y * (K(z,u) * w)) = K(x,w * y). [para(171(a,1),3320(a,1,2)),rewrite([3261(4)]),flip(a)].

3531 K(x,y) * ((y * x) * z) = (x * y) * z. [para(3383(a,1),163(a,1,2,2)),rewrite([173(4),3064(5)])].

3538 K(x * (x' * y),z) = K(y,z). [para(816(a,2),3383(a,1,1)),rewrite([3378(3),516(4)]),flip(a)].

3555 K(x * (K(y,z) * u),w) = K(u * x,w). [para(171(a,1),3383(a,1,1)),rewrite([3280(4)]),flip(a)].

4209 x * (y * (y' \ (x \ z))) = y * (y' \ z). [para(280(a,1),1588(a,1,1)),rewrite([2213(3),2(5),2213(6)]),flip(a)].

4236 K(x,y) * ((x * y) * z) = y * ((x * y) * (y \ z)). [para(804(a,1),1588(a,1,1))].

4238 K(x,y) * ((x * y') * z) = y * ((x * y') * (y \ z)). [para(838(a,1),1588(a,1,1))].

4335 K(x,y * (z * (y \ u))) = K(x,z * u). [para(1588(a,1),3261(a,1,2))].

4342 K((x * y) * z,u) = K(x * (z' \ y),u). [para(1588(a,2),3538(a,1,1,2)),rewrite([760(2),3555(5)])].

4387 K(x * (y' \ z),x * (z * y)) = K(a(x,z,y),(x * z) * y). [back_rewrite(851),rewrite([4342(5)])].

4388 K(x * (y' \ z),a(x,z,y)) = K(a(x,z,y),x * (z * y)). [back_rewrite(835),rewrite([4342(4)])].

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

4429 x * ((y * x) * (x \ z)) = (x' \ y) * z. [para(163(a,1),2730(a,1,2,1)),rewrite([323(7),167(7),173(7),1042(7)])].

4523 K(x,y) * ((x * y) * z) = (y' \ x) * z. [back_rewrite(4236),rewrite([4429(8)])].

4685 K(x,y * (z \ u)) = K(x,y * (u * z')). [para(1004(a,1),3329(a,1,2,2)),rewrite([323(7),167(7),173(7),759(7)])].

4688 K(x,y * (z * (z' \ u))) = K(x,y * (z * (u * z))). [para(1129(a,1),3329(a,1,2,2)),flip(a)].

4697 K(x,y * (z * (u \ z))) = K(x,y * (z * (u' * z))). [para(1409(a,1),3329(a,1,2,2)),rewrite([4688(6)]),flip(a)].

4707 K(x,y * (z * (K(u,w) * v5))) = K(x,(v5 * z) * y). [para(171(a,1),3329(a,1,2,2)),rewrite([3504(5)]),flip(a)].

4709 K(x,y * (z * (u * K(w,v5)))) = K(x,(z * u) * y). [para(173(a,1),3329(a,1,2,2)),rewrite([3504(10)])].

4719 K(x,y * ((y \ z) * u)) = K(x,u * z). [para(1588(a,2),3329(a,1,2)),rewrite([3261(4)]),flip(a)].

4761 K(x * (y \ z),u) = K(x * (z * y'),u). [para(1004(a,1),3392(a,1,1,2)),rewrite([323(7),167(7),173(7),759(7)])].

4808 K(a(x,y,z),(x * y) * z) = K(a(x,y,z),x * (y * z)). [back_rewrite(4388),rewrite([4761(5),115(2),843(4)])].

4809 K(a(x,y,z),x * (y * z)) = 1. [back_rewrite(4387),rewrite([4761(6),115(2),284(5),4808(5)]),flip(a)].

4861 a(x,y,z) * (x * (y * z)) = (x * y) * z. [back_rewrite(848),rewrite([4808(5),4809(5),3(3)])].

5124 K(x,y) * ((x * y') * z) = (y \ x) * z. [para(1004(a,1),3531(a,2,1)),rewrite([3313(4),741(2),323(5),167(5),173(5),759(5)])].

5197 x * ((y * x') * (x \ z)) = (x \ y) * z. [back_rewrite(4238),rewrite([5124(5)]),flip(a)].

5284 K(x,y * (z * u)) = K(x,z * (y * u)). [para(5(a,1),4335(a,1,2,2,2))].

5403 K(x,y * (z * u)) = K(x,u * (y * z)). [para(5(a,1),4719(a,1,2,2,1))].

5719 K(x,(y * z) * u) = K(x,y * (z * u)). [para(163(a,1),5284(a,1,2,2)),rewrite([4709(8)]),flip(a)].

5734 K(x,y * (z * (u * z))) = K(x,z * (u * (y * z))). [para(1080(a,1),5284(a,1,2,2)),rewrite([4697(5),115(2),5719(8)])].

5823 K(x,y * (z * (K(u,w) * v5))) = K(x,v5 * (z * y)). [back_rewrite(4707),rewrite([5719(8)])].

5851 K(x,y * (z * (u * y))) = K(x,z * (y * (y * u))). [para(33(a,1),5403(a,1,2,2)),flip(a)].

5875 K(x,y * (z * (u * z))) = K(x,z * (y * (z * u))). [para(1080(a,1),5403(a,1,2,2)),rewrite([4697(5),115(2)])].

6951 K(x,y * (z * ((u * w) * z))) = K(x,u * (w * (z * (y * z)))). [para(2220(a,1),5403(a,2,2,2)),rewrite([2213(3),4688(6),5719(5),4688(11)]),flip(a)].

6997 x * ((y' \ x) * (x' * (z * z))) = (x * y) * (z * z). [para(519(a,1),2780(a,1,2)),flip(a)].

7717 x * (x' * ((x' * y) * (z * z))) = (x \ y) * (z * z). [para(706(a,1),5197(a,1,2,2)),rewrite([59(6)])].

7731 x * ((y' \ x) * (x' * z)) = x * (x' * ((x' \ y) * z)). [para(5197(a,1),1030(a,1,2,2)),rewrite([115(8),4410(11),1633(10),2780(11)]),flip(a)].

7753 (x' * (x \ y)) * z = y * (x' * (x \ z)). [para(5197(a,1),2213(a,1)),rewrite([2304(2),123(7),365(7),2304(11),2308(13),115(8),5(13),4(10)])].

7821 x * (x' * ((x' \ y) * (z * z))) = (x * y) * (z * z). [back_rewrite(6997),rewrite([7731(7)])].

7901 (x \ y') * (y * z) = y * ((y \ x') * z). [para(115(a,1),201(a,1,1,1))].

7967 x * ((x \ y) * (z * z)) = z * (z' \ y). [para(2177(a,2),201(a,2,2)),rewrite([7901(6),115(2),4209(9)])].

8083 (x * y) * (z * z) = x * (z * (z' \ y)). [back_rewrite(7821),rewrite([7967(6)]),flip(a)].

8088 x \ (y * (y' \ z)) = (x \ z) * (y * y). [back_rewrite(7717),rewrite([8083(5),1030(8)])].

8427 x \ (y' * (y \ z)) = (x \ z) * (y' * y'). [para(115(a,1),8088(a,1,2,2,1))].

8450 x * (x' \ (y * ((z \ y') * (x' * x')))) = y * (z \ y'). [para(8088(a,1),1087(a,1,2)),rewrite([123(4),1730(4),115(3),7753(8),2200(6),4(6),1087(3),123(10),1730(10),115(9),

8427(11),2215(13)]),flip(a)].

8575 K(x,y * (z * y)) = K(x,z). [para(2215(a,1),1514(a,1,2)),rewrite([123(6),1730(6),115(5),8427(7),8450(11),1514(5),4685(5),115(3)]),flip(a)].

8591 K(x,y * (z * (u * z))) = K(x,u * y). [para(2215(a,1),3320(a,1,2)),rewrite([4685(5),115(3),8575(4),4688(7)]),flip(a)].

8698 K(x,y * (z * (u * (w * u)))) = K(x,y * (z * w)). [back_rewrite(6951),rewrite([8591(5),5719(3)]),flip(a)].

8708 K(x,y * (z * (y * u))) = K(x,u * z). [back_rewrite(5875),rewrite([8591(4)]),flip(a)].

8710 K(x,y * (z * (u * y))) = K(x,z * u). [back_rewrite(5734),rewrite([8591(4)]),flip(a)].

8878 K(x,y * (z * (z * u))) = K(x,y * u). [back_rewrite(5851),rewrite([8710(4)]),flip(a)].

9072 K(x,y * ((z * u) * ((y * z) * u))) = K(x,a(y,z,u)). [para(4861(a,1),8575(a,1,2,2)),rewrite([5719(6)])].

9495 K(x,y * ((z \ u) * w)) = K(x,y * (u * (w * z))). [para(1588(a,2),8708(a,1,2,2,2)),rewrite([5823(6),5719(4),5719(8)]),flip(a)].

9623 K(x,y * ((z * u) * (z \ w))) = K(x,y * (z * ((u * z) * w))). [para(2730(a,1),8878(a,1,2,2,2)),flip(a)].

9626 K(x,y * ((z * u) * w)) = K(x,y * (u * (w * z'))). [para(3531(a,1),8878(a,1,2,2,2)),rewrite([4523(4),9495(5)]),flip(a)].

9638 K(x,y * (z * ((u * z) * w))) = K(x,y * (u * w)). [back_rewrite(9623),rewrite([9626(5),1217(3),8698(7)]),flip(a)].

9651 K(x,a(y,z,u)) = 1. [back_rewrite(9072),rewrite([9626(6),9638(7),517(3),8710(5),18(2),275(2)]),flip(a)].

9711 K(a(x,y,z),u) = 1 # label(non_clause) # label(goal). [para(9651(a,1),605(a,1,1)),rewrite([95(2)]),flip(a)].

9712 $F. [resolve(9711,a,26,a)].

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

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

Given=233. Generated=36819. Kept=9704. proofs=1.

Usable=170. Sos=4521. Demods=4043. Limbo=1, Disabled=5030. Hints=2377.

Kept_by_rule=0, Deleted_by_rule=0.

Forward_subsumed=27115. Back_subsumed=327.

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

New_demodulators=8379 (6 lex), Back_demodulated=4684. Back_unit_deleted=0.

Demod_attempts=667481. Demod_rewrites=129801.

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

Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.

Megabytes=9.41.

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

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 4222 exit (max_proofs) Wed Oct 7 11:38:51 2009

% Length of proof is 114.

% Level of proof is 22.

% Maximum clause weight is 25.

% Given clauses 901.

1 a(x,y,a(u,v,w)) = 1 # label(non_clause) # label(goal). [goal].

2 1 * x = x. [assumption].

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 * y) * z) = (y * (z * x)) * x. [assumption].

9 (x * (y * z)) * z = z * ((z * x) * y). [copy(8),flip(a)].

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

13 (x * y) * (y \ (z * y)) = (x * z) * y. [copy(12),flip(a)].

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

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

16 x * ((y * x) \ 1) = y \ 1. [assumption].

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

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

19 (x * y) * z = (x * (y * z)) * a(x,y,z). [assumption].

20 (x * (y * z)) * a(x,y,z) = (x * y) * z. [copy(19),flip(a)].

21 x * y = (y * x) * K(x,y). [assumption].

22 (x * y) * K(y,x) = y * x. [copy(21),flip(a)].

23 K(K(x,y),z) = 1. [assumption].

24 a(K(x,y),z,u) = 1. [assumption].

25 a(x,y,K(z,u)) = 1. [assumption].

26 K(a(x,y,z),u) = 1. [assumption].

27 a(c1,c2,a(c3,c4,c5)) != 1. [deny(1)].

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

34 (x * y) * y = y * (y * x). [para(2(a,1),9(a,1,1,2)),rewrite([3(5)])].

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

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

59 (x * (y * (z * u))) * u = (x * u) * ((u * y) * z). [para(9(a,1),13(a,1,2,2)),rewrite([5(5)]),flip(a)].

60 (x * y) * (y * z) = y * ((y * x) * z). [para(9(a,1),13(a,2)),rewrite([34(3),5(4)])].

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

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

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

96 1' = 1. [para(17(a,1),3(a,1)),flip(a)].

98 1 / x = x'. [para(17(a,1),6(a,1,1))].

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

101 x \ (y * x) = (x' * y) * x. [para(17(a,1),13(a,1,1)),rewrite([2(4)])].

102 (x * y) * (y \ 1) = (x * y') * y. [para(17(a,1),13(a,1,2,2))].

112 (x * y) \ ((x * z) * y) = (y' * z) * y. [back_rewrite(53),rewrite([101(6)])].

115 x \ 1 = x'. [para(18(a,1),5(a,1,2))].

116 x'' = x. [para(18(a,1),6(a,1,1)),rewrite([98(3)])].

119 (x * y') * y = (x * y) * y'. [back_rewrite(102),rewrite([115(3)]),flip(a)].

123 (x / y)' = y * x'. [back_rewrite(91),rewrite([115(3),115(4)])].

124 (x * y)' = y \ x'. [back_rewrite(90),rewrite([115(3),115(4)])].

125 (x \ y) * y' = x'. [back_rewrite(89),rewrite([115(3),115(5)])].

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

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

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

163 (x * (y * z)) * K(z,y) = x * (z * y). [para(22(a,1),20(a,1,1,2)),rewrite([25(5),3(4)]),flip(a)].

164 x * (y * K(y,x)) = y * x. [para(22(a,1),20(a,2)),rewrite([25(5),3(5)])].

169 K(x,y) * z = z * K(x,y). [para(23(a,1),22(a,1,2)),rewrite([3(4)]),flip(a)].

171 K(x,y) * (z * (y * x)) = z * (x * y). [back_rewrite(163),rewrite([169(4,R)])].

175 (x * y) * K(z,u) = x * (y * K(z,u)). [para(25(a,1),20(a,1,2)),rewrite([3(5)]),flip(a)].

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

198 x / y = x' \ y'. [para(123(a,1),116(a,1,1)),rewrite([124(3)]),flip(a)].

199 (x \ y')' = y * x. [para(116(a,1),123(a,2,2)),rewrite([198(2),116(2)])].

259 (x \ y') * y = x'. [para(116(a,1),125(a,1,2))].

284 (x' * (y * x)) \ (x * y) = x. [para(18(a,1),36(a,1,2,2,1)),rewrite([2(5)])].

297 (x \ y)' = y' * x. [para(116(a,1),199(a,1,1,2))].

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

627 (x * (x * y)) \ (x * (y * x)) = K(x,y * x). [para(34(a,1),154(a,1,1))].

628 (x * (y * x)) \ (x * (x * y)) = K(y * x,x). [para(34(a,1),154(a,1,2))].

639 (x \ y') * (x * y) = K(y,x)'. [para(154(a,1),297(a,1,1)),rewrite([124(4)]),flip(a)].

712 (x' * y) * x = y * K(y,x). [para(164(a,1),5(a,1,2)),rewrite([101(2)])].

718 a(x,y,z) * u = u * a(x,y,z). [para(26(a,1),164(a,1,2,2)),rewrite([3(3)]),flip(a)].

751 K(x * K(x,y),y) = (y' * K(x,y)) * y. [para(164(a,1),154(a,1,1)),rewrite([112(5)]),flip(a)].

754 K(x,y) * (K(x,y)' * z) = z. [para(169(a,1),5(a,1,2)),rewrite([101(4),169(5,R)])].

765 (x * K(y,z)) * u = K(y,z) * (x * u). [para(169(a,1),20(a,2,1)),rewrite([24(5),3(5)]),flip(a)].

811 K(x,K(y,z)) = 1. [para(169(a,1),154(a,1,1)),rewrite([29(5)]),flip(a)].

813 K(x * K(x,y),y) = K(x,y). [back_rewrite(751),rewrite([765(7),17(6),3(6)])].

835 x' * (x * x) = x. [para(15(a,2),181(a,1,2)),rewrite([15(3),101(4),124(2),259(3)])].

918 x' * (x * y) = x * (x' * y). [para(835(a,1),60(a,2,2,1)),rewrite([15(3),835(3)]),flip(a)].

1969 (x \ y) * x = x * (y * x'). [para(4(a,1),99(a,1,2,1)),flip(a)].

1971 (x' * y) * x = (x * y) * x'. [para(99(a,1),5(a,1,2)),rewrite([101(2)])].

1973 (x * y) * y' = y * (y' * x). [para(99(a,1),9(a,1,1)),rewrite([17(6),2(7),918(6)])].

2002 (x * (y * z')) * z = z * ((z' * x) * y). [para(59(a,1),99(a,1,2)),rewrite([18(2),2(5)]),flip(a)].

2077 (x * y) * x' = y * K(y,x). [back_rewrite(712),rewrite([1971(3)])].

2091 (x * y') * y = y * (y' * x). [back_rewrite(119),rewrite([1973(6)])].

3065 (x * (y * z)) \ ((x * z) * (y * K(y,z))) = a(x,z,y * K(y,z)). [para(164(a,1),132(a,1,1,2))].

3066 (x * (K(y,x) * (y * z))) \ ((y * x) * z) = a(x,y * K(y,x),z). [para(164(a,1),132(a,1,2,1)),rewrite([765(3)])].

4250 K(x,y)' = K(y,x). [para(17(a,1),171(a,1,2)),rewrite([3(3),124(3),639(5)]),flip(a)].

4305 (x * (y * z)) \ (x * (z * y)) = K(z,y). [para(171(a,1),284(a,1,2)),rewrite([4250(2),169(5,R),171(5),171(4)])].

4307 K(x,y) * (z * K(y,x)) = z. [para(754(a,1),171(a,1,2)),rewrite([4250(2),811(2),2(2),4250(3)]),flip(a)].

4361 K(x * y,y) = K(y,x). [back_rewrite(628),rewrite([4305(5)]),flip(a)].

4362 K(x,y * x) = K(y,x). [back_rewrite(627),rewrite([4305(5)]),flip(a)].

4466 K(x,a(y,z,u)) = 1. [para(26(a,1),4250(a,1,1)),rewrite([96(2)]),flip(a)].

4470 K(x,y * K(y,x)) = K(x,y). [para(813(a,1),4250(a,1,1)),rewrite([4250(2)]),flip(a)].

4577 K(x * (x * y),x) = K(y,x). [para(34(a,1),4361(a,1,1)),rewrite([4362(5)])].

4589 K(x * y,x) = K(x,y). [para(4361(a,1),813(a,1,1,2)),rewrite([175(3),164(3),4361(4)])].

4600 K(x,x * y) = K(y,x). [back_rewrite(4577),rewrite([4589(3)])].

4636 K(x,x \ y) = K(y,x). [para(4(a,1),4589(a,1,1)),flip(a)].

4666 (x \ y) * (y' * K(z,u)) = x' * K(z,u). [para(125(a,1),175(a,1,1)),flip(a)].

4763 (x \ y) * (x * K(y,x)) = y. [para(4636(a,1),164(a,1,2,2)),rewrite([4(6)])].

5659 x * ((x * K(y,z)) \ u) = K(z,y) * u. [para(4307(a,1),131(a,2,1)),rewrite([24(9),3(4)]),flip(a)].

5833 ((x * y) \ x) * (y * x) = x. [para(4600(a,1),4763(a,1,2,2)),rewrite([175(5),164(5)])].

5855 ((x * K(x,y)) \ y) * x = y. [para(4470(a,1),4763(a,1,2,2)),rewrite([169(7,R),4307(7)])].

6668 (x \ (y \ x)) * (x * K(x,y)) = y \ x. [para(4763(a,1),5833(a,1,1,1)),rewrite([765(6),4(5),169(4)])].

6785 x * (K(y,x) * (y * z)) = y * (x * z). [para(5855(a,1),60(a,1,1)),rewrite([5659(6),169(4),765(5)]),flip(a)].

6846 a(x,y * K(y,x),z) = a(y,x,z). [back_rewrite(3066),rewrite([6785(4),132(5)]),flip(a)].

7215 (x \ y) * (x * K(z,u)) = x * (y * (x' * K(z,u))). [para(1969(a,1),175(a,1,1)),rewrite([175(5),175(4)]),flip(a)].

7282 x * (y' * K(x,y)) = y \ x. [back_rewrite(6668),rewrite([7215(5),4666(5)])].

7398 (x * y) * (z * K(z,y)) = (x * z) * y. [para(2077(a,1),59(a,2,2)),rewrite([17(2),3(2)]),flip(a)].

7542 a(x,y,z * K(z,y)) = a(x,z,y). [back_rewrite(3065),rewrite([7398(6),132(5)]),flip(a)].

16380 a(x,y,z) \ u = u * a(x,y,z)'. [para(4466(a,1),7282(a,1,2,2)),rewrite([3(4)]),flip(a)].

37090 a(x,y,z) * (a(x,y,z)' * u) = u. [para(718(a,1),4(a,1)),rewrite([16380(2),2091(5)])].

37108 (a(x,y,z) * (u * w)) \ ((u * a(x,y,z)) * w) = a(a(x,y,z),u,w). [para(718(a,1),132(a,1,2,1))].

39361 a(a(x,y,z),u,w) = a(u,a(x,y,z),w). [para(26(a,1),6846(a,1,2,2)),rewrite([3(3)]),flip(a)].

42051 a(x,a(y,z,u),w) = a(x,w,a(y,z,u)). [para(26(a,1),7542(a,1,3,2)),rewrite([3(3)]),flip(a)].

42748 (x * a(y,z,u)) * w = a(y,z,u) * (x * w). [para(576(a,1),718(a,1)),rewrite([16380(7),2002(11),918(9),37090(9)])].

42831 a(a(x,y,z),u,w) = 1. [back_rewrite(37108),rewrite([42748(6),29(7)]),flip(a)].

42868 a(x,a(y,z,u),w) = 1. [back_rewrite(39361),rewrite([42831(2)]),flip(a)].

42880 a(x,y,a(z,u,w)) = 1. [back_rewrite(42051),rewrite([42868(2)]),flip(a)].

42881 $F. [resolve(42880,a,27,a)].

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

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

Given=901. Generated=261956. Kept=42873. proofs=1.

Usable=503. Sos=17525. Demods=16916. Limbo=12, Disabled=24852. Hints=0.

Kept_by_rule=0, Deleted_by_rule=9220.

Forward_subsumed=157563. Back_subsumed=910.

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

New_demodulators=39967 (32 lex), Back_demodulated=23922. Back_unit_deleted=0.

Demod_attempts=8318851. Demod_rewrites=1284417.

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

Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.

Megabytes=43.93.

User_CPU=19.13, System_CPU=0.39, Wall_clock=19.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 4259 exit (max_proofs) Wed Oct 7 11:43:59 2009

% Length of proof is 138.

% Level of proof is 24.

% Maximum clause weight is 25.

% Given clauses 117.

1 a(a(x,y,z),u,v) = 1 # label(non_clause) # label(goal). [goal].

2 1 * x = x. [assumption].

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 * y) * z) = (y * (z * x)) * x. [assumption].

9 (x * (y * z)) * z = z * ((z * x) * y). [copy(8),flip(a)].

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

13 (x * y) * (y \ (z * y)) = (x * z) * y. [copy(12),flip(a)].

16 x * ((y * x) \ 1) = y \ 1. [assumption].

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

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

19 (x * y) * z = (x * (y * z)) * a(x,y,z). [assumption].

20 (x * (y * z)) * a(x,y,z) = (x * y) * z. [copy(19),flip(a)].

21 x * y = (y * x) * K(x,y). [assumption].

22 (x * y) * K(y,x) = y * x. [copy(21),flip(a)].

23 K(K(x,y),z) = 1. [assumption].

25 a(x,y,K(z,u)) = 1. [assumption].

26 a(x,y,a(z,u,w)) = 1. [assumption].

27 K(a(x,y,z),u) = 1. [assumption].

29 a(a(c1,c2,c3),c4,c5) != 1. [deny(1)].

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

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

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

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

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

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

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

100 1 / x = x'. [para(17(a,1),6(a,1,1))].

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

103 x \ (y * x) = (x' * y) * x. [para(17(a,1),13(a,1,1)),rewrite([2(4)])].

104 (x * y) * (y \ 1) = (x * y') * y. [para(17(a,1),13(a,1,2,2))].

114 (x * y) \ ((x * z) * y) = (y' * z) * y. [back_rewrite(55),rewrite([103(6)])].

117 x \ 1 = x'. [para(18(a,1),5(a,1,2))].

118 x'' = x. [para(18(a,1),6(a,1,1)),rewrite([100(3)])].

121 (x * y') * y = (x * y) * y'. [back_rewrite(104),rewrite([117(3)]),flip(a)].

125 (x / y)' = y * x'. [back_rewrite(93),rewrite([117(3),117(4)])].

126 (x * y)' = y \ x'. [back_rewrite(92),rewrite([117(3),117(4)])].

127 (x \ y) * y' = x'. [back_rewrite(91),rewrite([117(3),117(5)])].

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

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

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

167 x * (y * K(y,x)) = y * x. [para(22(a,1),20(a,2)),rewrite([25(5),3(5)])].

172 K(x,y) * z = z * K(x,y). [para(23(a,1),22(a,1,2)),rewrite([3(4)]),flip(a)].

178 (x * y) * K(z,u) = x * (y * K(z,u)). [para(25(a,1),20(a,1,2)),rewrite([3(5)]),flip(a)].

183 (x * y) * a(z,u,w) = x * (y * a(z,u,w)). [para(26(a,1),20(a,1,2)),rewrite([3(5)]),flip(a)].

197 x / y = x' \ y'. [para(125(a,1),118(a,1,1)),rewrite([126(3)]),flip(a)].

198 (x \ y')' = y * x. [para(118(a,1),125(a,2,2)),rewrite([197(2),118(2)])].

226 (x \ y) \ x' = y'. [para(4(a,1),126(a,1,1)),flip(a)].

227 ((x * y) * z) \ x' = x \ ((z * x) \ y'). [para(9(a,1),126(a,1,1)),rewrite([126(4),126(7)])].

237 (x \ y)' = y' * x. [para(118(a,1),198(a,1,1,2))].

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

280 (x \ y') * (x * y) = K(y,x)'. [para(157(a,1),237(a,1,1)),rewrite([126(4)]),flip(a)].

286 (x' * y) * x = y * K(y,x). [para(167(a,1),5(a,1,2)),rewrite([103(2)])].

291 a(x,y,z) * u = u * a(x,y,z). [para(27(a,1),167(a,1,2,2)),rewrite([3(3)]),flip(a)].

295 K(x * K(x,y),y) = (y' * K(x,y)) * y. [para(167(a,1),157(a,1,1)),rewrite([114(5)]),flip(a)].

297 K(x,y) * (K(x,y)' * z) = z. [para(172(a,1),5(a,1,2)),rewrite([103(4),172(5,R)])].

298 (x' * K(y,z)) * x = K(y,z). [para(172(a,2),5(a,1,2)),rewrite([103(3)])].

314 K(x * K(x,y),y) = K(x,y). [back_rewrite(295),rewrite([298(7)])].

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

330 x' * (x * K(y,z)) = K(y,z). [para(172(a,1),254(a,1,2,2)),rewrite([103(7),126(3),172(5,R),4(5)])].

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

366 (x' * y') * x = x * (y \ x'). [para(316(a,1),127(a,1,1)),rewrite([126(2),126(6),237(5),103(6)]),flip(a)].

381 (K(x,y) \ z) \ z = K(x,y). [para(172(a,2),363(a,1,1)),rewrite([4(6)])].

385 x' * (K(y,z) \ x) = K(y,z)'. [para(381(a,1),237(a,1,1)),flip(a)].

386 K(x,y) \ z = K(x,y)' * z. [para(381(a,1),316(a,1,1,1)),rewrite([4(4),103(4),385(4)]),flip(a)].

389 (K(x,y)' * z) \ z = K(x,y). [back_rewrite(381),rewrite([386(2)])].

396 (x \ y) * x = x * (y * x'). [para(4(a,1),101(a,1,2,1)),flip(a)].

398 (x' * y) * x = (x * y) * x'. [para(101(a,1),5(a,1,2)),rewrite([103(2)])].

400 (x * y) * y' = y' * (y * x). [para(101(a,1),9(a,1,1)),rewrite([17(6),2(7)])].

403 x' * (x * y) = x * (x' * y). [para(9(a,1),101(a,1,2)),rewrite([17(3),2(3),121(6),400(6)]),flip(a)].

443 x * K(y \ x,y) = y * (x * y'). [back_rewrite(156),rewrite([396(5)])].

444 (x * y') * x' = x * (y \ x'). [back_rewrite(366),rewrite([398(4)])].

445 (x * K(y,z)) * x' = K(y,z). [back_rewrite(298),rewrite([398(4)])].

446 (x * y) * x' = y * K(y,x). [back_rewrite(286),rewrite([398(3)])].

455 x \ (y * x) = (x * y) * x'. [back_rewrite(103),rewrite([398(5)])].

461 x * (x' * K(y,z)) = K(y,z). [back_rewrite(330),rewrite([403(4)])].

470 K(x,y) * (z * K(x,y)') = z * K(z,K(x,y)'). [para(167(a,1),297(a,1,2))].

473 K(x,y) * (z * K(x,y)') = z. [para(297(a,1),101(a,1,2,1)),rewrite([172(10,R),297(10)])].

474 x * K(x,K(y,z)') = x. [back_rewrite(470),rewrite([473(5)]),flip(a)].

475 K(x,K(y,z)') = 1. [para(474(a,1),5(a,1,2)),rewrite([31(1)]),flip(a)].

477 x \ K(y,z) = x' * K(y,z). [para(386(a,1),237(a,1,1)),rewrite([126(4),118(3)])].

480 (x * K(y,z)') \ x = K(y,z). [para(167(a,1),389(a,1,1)),rewrite([475(6),3(5)])].

522 (x \ y) * K(x \ y,x) = y * x'. [para(4(a,1),446(a,1,1)),flip(a)].

526 x * (y' * K(x * y',y)) = y' * x. [para(446(a,1),9(a,1)),rewrite([178(6),17(9),2(9)])].

557 K((x * y) * x',x) = K(y,x). [para(446(a,2),314(a,1,1))].

565 (x * (y * x')) * (y' * x) = x * K(x,x \ y). [para(396(a,1),446(a,1,1)),rewrite([237(5)])].

580 K(x \ y,x) = K(y * x',x). [para(4(a,1),557(a,1,1,1)),flip(a)].

582 K((x * y) * x',x') = K(y,x'). [para(118(a,1),557(a,1,1,2)),rewrite([398(3)])].

588 (x \ y) * K(y * x',x) = y * x'. [back_rewrite(522),rewrite([580(3)])].

590 x * K(x * y',y) = y * (x * y'). [back_rewrite(443),rewrite([580(2)])].

594 (x * (y \ x')) * y = K(y * x',x)'. [para(4(a,1),280(a,1,2)),rewrite([237(2),455(3),444(4),580(6)])].

596 x * K(y * x',x)' = K(x,y)' * x. [para(280(a,1),9(a,1,1)),rewrite([594(7)]),flip(a)].

676 (x * (x * y')) * (x \ y) = x * K(x,x \ y). [para(396(a,1),398(a,2,1)),rewrite([237(2),36(3),237(10),565(11)])].

680 K(x * y',y)' = K(x',y). [para(446(a,2),398(a,1,1)),rewrite([444(4),594(4),445(9)])].

696 K(x,y)' * x = x * K(y',x). [back_rewrite(596),rewrite([680(4)]),flip(a)].

702 K(x * y',y) = K(x',y)'. [para(680(a,1),118(a,1,1)),flip(a)].

703 K(x * y,y')' = K(x',y'). [para(118(a,1),680(a,1,1,1,2))].

705 K(x' * y,x) = K(y',x)'. [para(127(a,1),680(a,1,1,1)),rewrite([237(5)]),flip(a)].

708 K(x' \ y',x) = K(y \ x,x). [para(36(a,1),680(a,1,1,1)),rewrite([705(5),126(3),118(2),118(4),126(5)]),flip(a)].

711 K(x \ y',y) = K(x,y)'. [para(446(a,1),680(a,1,1,1)),rewrite([314(3),126(4)]),flip(a)].

712 (x * K(y',z)) \ x = K(y',z)'. [para(680(a,1),480(a,1,1,2)),rewrite([702(7)])].

715 x * K(x',y)' = y * (x * y'). [back_rewrite(590),rewrite([702(3)])].

716 (x \ y) * K(y',x)' = y * x'. [back_rewrite(588),rewrite([702(4)])].

718 x * (y' * K(x',y)') = y' * x. [back_rewrite(526),rewrite([702(4)])].

752 K(x',y)' = K(y,x). [para(696(a,1),389(a,1,1)),rewrite([712(4)])].

753 K(x',y') = K(x,y). [para(696(a,1),396(a,2,2)),rewrite([752(3),477(2),398(4),445(4),461(7)]),flip(a)].

760 x * (y' * K(y,x)) = y' * x. [back_rewrite(718),rewrite([752(4)])].

762 K(x,y) * (x \ y) = y * x'. [back_rewrite(716),rewrite([752(4),172(3,R)])].

763 x * K(y,x) = y * (x * y'). [back_rewrite(715),rewrite([752(3)])].

769 K(x * y',y) = K(y,x). [back_rewrite(702),rewrite([752(6)])].

774 K(x * y,y')' = K(x,y). [back_rewrite(703),rewrite([753(7)])].

777 K(x,y)' = K(y',x). [para(752(a,1),118(a,1,1))].

778 K(x',y) = K(x,y'). [para(118(a,1),752(a,1,1,1)),rewrite([777(2)])].

794 K(x,y * x) = K(y,x). [back_rewrite(774),rewrite([777(4),118(2)])].

805 K(x \ y',y) = K(y,x'). [back_rewrite(711),rewrite([777(5),778(5)])].

870 K(x \ y',z) = K(y * x,z'). [para(126(a,1),778(a,1,1))].

876 K(x * y,x') = K(x,y'). [back_rewrite(805),rewrite([870(3)])].

879 K(x \ y,y) = K(x * y',y'). [back_rewrite(708),rewrite([870(4)]),flip(a)].

885 K(x * y',y') = K(x,x \ y). [para(4(a,1),794(a,1,2)),rewrite([879(2)])].

888 K(x,x * (x * y)) = K(y * x,x). [para(36(a,1),794(a,1,2))].

912 K(x,y') = K(x,y). [para(762(a,1),254(a,1,2,2)),rewrite([172(3,R),762(3),172(6),178(6),760(6),157(5),778(2)])].

929 K(x,x \ y) = K(y,x). [back_rewrite(885),rewrite([912(4),769(3)]),flip(a)].

936 K(x * y,x) = K(x,y). [back_rewrite(876),rewrite([912(3),912(4)])].

986 K(x',y) = K(x,y). [back_rewrite(778),rewrite([912(4)])].

987 K(x,x * y) = K(y,x). [back_rewrite(582),rewrite([912(5),769(4),912(4)])].

992 (x * (x * y')) * (x \ y) = x * K(y,x). [back_rewrite(676),rewrite([929(7)])].

1009 K(x * y,y) = K(y,x). [back_rewrite(888),rewrite([987(3),936(2)]),flip(a)].

1084 K(x,(x * y) * z) = K(x,y * (z * x)). [para(9(a,1),1009(a,1,1)),rewrite([936(4)])].

2092 (x * y) * (z * K(x,y * (z * x))) = x * (((x * y) * z) * x'). [para(1084(a,1),763(a,1,2)),rewrite([178(6)])].

2226 (x * (y * a(z,u,w))) \ ((a(z,u,w) * x) * y) = a(a(z,u,w),x,y). [para(291(a,1),134(a,1,1)),rewrite([183(3)])].

2708 (x \ y) \ y = x * K(y,x). [para(17(a,1),54(a,1,1)),rewrite([2(4),237(4),36(5),992(7)])].

2787 x * (((x * y) * z) * x') = y * (z * x). [para(227(a,1),2708(a,1,1)),rewrite([226(6),237(4),118(2),986(8),1084(7),178(8),2092(8)]),flip(a)].

3082 (a(x,y,z) * u) * w = u * (w * a(x,y,z)). [para(2787(a,1),291(a,1)),rewrite([183(11),17(10),3(8)]),flip(a)].

3462 a(a(x,y,z),u,w) = 1 # label(non_clause) # label(goal). [back_rewrite(2226),rewrite([3082(6),31(7)]),flip(a)].

3463 $F. [resolve(3462,a,29,a)].

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

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

Given=117. Generated=8851. Kept=3454. proofs=1.

Usable=72. Sos=1326. Demods=1500. Limbo=380, Disabled=1697. Hints=698.

Kept_by_rule=0, Deleted_by_rule=0.

Forward_subsumed=5397. Back_subsumed=69.

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

New_demodulators=2916 (3 lex), Back_demodulated=1606. Back_unit_deleted=0.

Demod_attempts=141266. Demod_rewrites=25144.

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

Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.

Megabytes=3.55.

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

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 4283 exit (max_proofs) Wed Oct 7 11:47:24 2009