% Proof 1 at 15.21 (+ 0.13) seconds.

% Length of proof is 163.

% Level of proof is 27.

% Maximum clause weight is 32.000.

% Given clauses 789.

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

2 0 * x = x. [assumption].

3 x * 0 = x. [assumption].

4 x * x' = 0. [assumption].

5 x' * x = 0. [assumption].

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

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

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

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

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

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

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

13 L(x,y,z) = (z * y)' * (z * (y * x)). [assumption].

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

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

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

18 (c1 * c2) * (D * c1) != c1 * ((c2 * D) * c1). [deny(1)].

22 x \ 0 = x'. [para(4(a,1),7(a,1,2))].

23 x'' = x. [para(5(a,1),7(a,1,2)),rewrite([22(3)])].

34 (x * (y * (x * z))) / z = x * (y * x). [para(10(a,1),8(a,1,1))].

35 x * ((y / x) * (x * z)) = (x * y) * z. [para(9(a,1),10(a,1,1,2)),flip(a)].

36 (x * (y * (z * (y * x)))) * u = x * (y * (z * (y * (x * u)))). [para(10(a,1),10(a,1,1,2)),rewrite([10(9)])].

38 x \ y = x' * y. [para(6(a,1),11(a,1,2)),flip(a)].

39 x / (y * x) = y'. [para(11(a,1),8(a,1,1))].

42 (x * (y * x))' * (x * (y * (x * z))) = z. [para(10(a,1),11(a,1,2))].

45 x * (x' * y) = y. [back_rewrite(6),rewrite([38(1)])].

55 L(x',x,y) = (y * x)' * y. [para(4(a,1),14(a,1,2,2)),rewrite([3(4)]),flip(a)].

57 L(x,x',y) = (y * x')' * y. [para(5(a,1),14(a,1,2,2)),rewrite([3(5)]),flip(a)].

58 L(x,y,(y * x)') = ((y * x)' * y)'. [para(5(a,1),14(a,1,2)),rewrite([3(6)]),flip(a)].

59 L(x,y,z) / (z * (y * x)) = (z * y)'. [para(14(a,1),8(a,1,1))].

60 x' * ((x / y) * (y * z)) = L(z,y,x / y). [para(9(a,1),14(a,1,1,1))].

61 L(x,y / x,z) = (z * (y / x))' * (z * y). [para(9(a,1),14(a,1,2,2)),flip(a)].

62 L(x,y,z / (y * x)) = ((z / (y * x)) * y)' * z. [para(9(a,1),14(a,1,2)),flip(a)].

64 (x * (y * (x * z)))' * (x * (y * (x * (z * u)))) = L(u,z,x * (y * x)). [para(10(a,1),14(a,1,1,1)),rewrite([10(8)])].

65 (x * (y * (z * y)))' * (x * (y * (z * (y * u)))) = L(u,y * (z * y),x). [para(10(a,1),14(a,1,2,2))].

66 (x * y) * L(z,y,x) = x * (y * z). [para(14(a,1),11(a,1,2)),rewrite([23(3)])].

67 x' * (y' * ((y * x) * z)) = L(z,y * x,y'). [para(11(a,1),14(a,1,1,1))].

68 L(x * y,x',z) = (z * x')' * (z * y). [para(11(a,1),14(a,1,2,2)),flip(a)].

75 A' * ((x * A) * A') = A' * x. [para(4(a,1),16(a,1,2)),rewrite([3(5)]),flip(a)].

76 x' * ((x * A) * x') = A * x'. [para(5(a,1),16(a,1,1)),rewrite([2(5)]),flip(a)].

78 (x / y) * ((y * A) * (x / y)) = x * (A * (x / y)). [para(9(a,1),16(a,1,1)),flip(a)].

80 x * (((y * x) * A) * x) = x * (y * (x * (A * x))). [para(16(a,1),10(a,1))].

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

101 x * ((x * y)' * x) = x / y. [para(5(a,1),34(a,1,1,2)),rewrite([3(2)]),flip(a)].

102 ((x / y) * (z * x)) / y = (x / y) * (z * (x / y)). [para(9(a,1),34(a,1,1,2,2))].

112 (x / y)' = y / x. [para(9(a,1),39(a,1,2)),flip(a)].

117 (x * y) * x' = x * (y / x). [para(4(a,1),35(a,1,2,2)),rewrite([3(3)]),flip(a)].

118 (x' * y) * x = x' * (y / x'). [para(5(a,1),35(a,1,2,2)),rewrite([3(5)]),flip(a)].

123 (x / y) * (y * z) = y' * ((y * x) * z). [para(35(a,1),11(a,1,2)),flip(a)].

137 A / x = A * x'. [back_rewrite(76),rewrite([117(5),11(5)])].

139 L(x,y * z,y') = L(x,y,z / y). [back_rewrite(60),rewrite([123(4),67(6)])].

149 (x / y) * (y / x) = 0. [para(112(a,1),4(a,1,2))].

153 A * (x * A)' = x'. [para(137(a,1),39(a,1))].

165 x * (y * L(z,x,y)) = (x * y) * z. [para(5(a,1),36(a,1,1,2,2)),rewrite([3(2),14(7)]),flip(a)].

205 L(x / y,y / x,z) = (z * (y / x))' * z. [para(149(a,1),14(a,1,2,2)),rewrite([3(5)]),flip(a)].

212 (x * A)' = A' * x'. [para(153(a,1),11(a,1,2)),flip(a)].

229 (x * (y * x))' * (x * y) = x'. [para(4(a,1),42(a,1,2,2,2)),rewrite([3(5)])].

307 (x * A) * (A' * x') = 0. [para(212(a,1),4(a,1,2))].

410 L(x',x,y) / y = (y * x)'. [para(55(a,2),8(a,1,1))].

411 L(x',x,y / x) = y' * (y / x). [para(9(a,1),55(a,2,1,1))].

412 (x * L(y',y,x)) * z = x * ((x * y)' * (x * z)). [para(55(a,2),10(a,1,1,2))].

420 (((x * y) * z)' * x)' * L(z',z,x * y) = L(y,x,((x * y) * z)'). [para(55(a,2),14(a,1,2))].

427 x * L(y',y,x) = x / y. [para(55(a,2),34(a,2,2)),rewrite([34(6),101(4)]),flip(a)].

439 (A' * x') * x = L(A',A,x). [para(212(a,1),55(a,2,1)),flip(a)].

451 x * ((x * y)' * (x * z)) = (x / y) * z. [back_rewrite(412),rewrite([427(3)]),flip(a)].

473 L(x,x',y / x') = y' * (y / x'). [para(9(a,1),57(a,2,1,1))].

477 L(x,x',y * (z * y)) = (y * (z * (y * x')))' * (y * (z * y)). [para(10(a,1),57(a,2,1,1))].

485 x * L(y,y',x) = x / y'. [para(57(a,2),34(a,2,2)),rewrite([451(6),8(4)]),flip(a)].

512 (A' * x) * x' = A'. [para(307(a,1),10(a,2,2)),rewrite([75(8),3(9)])].

532 L(A',A,x) = A'. [para(23(a,1),512(a,1,2)),rewrite([439(5)])].

546 (A' * x') * x = A'. [back_rewrite(439),rewrite([532(9)])].

550 L(x,y / x,y') = (y' * (y / x))'. [para(9(a,1),58(a,1,3,1)),rewrite([9(5)])].

568 L(x',x,y)' = ((y * x)' * y)'. [para(55(a,2),58(a,2,1)),rewrite([58(3)]),flip(a)].

755 L(x,y / x,(y * z)') = ((y * z)' * (y / x))' * L(z',z,y). [para(55(a,2),61(a,2,2))].

1007 L(x,y,z / y) = L(x,y,z). [para(5(a,1),64(a,1,1,1,2)),rewrite([3(2),14(6),11(4),101(5)]),flip(a)].

1117 L(x,x',y) = y' * (y / x'). [back_rewrite(473),rewrite([1007(4)])].

1119 L(x',x,y) = y' * (y / x). [back_rewrite(411),rewrite([1007(3)])].

1121 L(x,y * z,y') = L(x,y,z). [back_rewrite(139),rewrite([1007(5)])].

1147 L(x,y,z * y) = L(x,y,z). [para(11(a,1),65(a,1,1,1)),rewrite([11(7),14(5),1121(5)]),flip(a)].

1266 x' * ((x * y) * z) = y * L(z,x,y). [para(9(a,1),66(a,1,1)),rewrite([1007(2),123(5)]),flip(a)].

1288 L(L(x,y,z)',L(x,y,z),z * y) = (z * (y * x))' * (z * y). [para(66(a,1),55(a,2,1,1))].

1294 L(L(x,y,z),z * y,(z * (y * x))') = ((z * (y * x))' * (z * y))'. [para(66(a,1),58(a,1,3,1)),rewrite([66(9)])].

1365 (x / y) / L(y',y,x) = x. [para(427(a,1),8(a,1,1))].

1386 L(L(x',x,y),y,x) = x'. [para(427(a,1),58(a,1,3,1)),rewrite([112(4),1007(4),427(6),112(5),9(5)])].

1403 L(x * (y * z),x',y') = (y' * x')' * z. [para(11(a,1),68(a,2,2))].

1442 L(L(x',x,y),y * x,z) = (z * (y * x))' * (z * y). [para(55(a,2),68(a,1,1)),rewrite([23(5),23(7)])].

1460 L(L(x,y / x,z),z * (y / x),u) = (u * (z * (y / x)))' * (u * (z * y)). [para(61(a,2),68(a,1,1)),rewrite([23(6),23(9)])].

1705 L(x,y * z,z) = L(x,y,z). [para(39(a,1),1007(a,1,3)),rewrite([1121(3)]),flip(a)].

1930 L(x,y * z,L(u,z / u,y)) = L(x,y * z,(y * (z / u))'). [para(61(a,2),1147(a,1,3))].

1937 ((x * y') * y')' * ((x * y') * z) = L(y * z,y',x). [para(1147(a,1),68(a,1)),flip(a)].

2163 L(L(x,x',y),y,x') = x. [para(23(a,1),1386(a,1,1,1)),rewrite([23(6)])].

2274 L(x,y / z,z) = L(x,y,z). [para(9(a,1),1705(a,1,2)),flip(a)].

2436 x * L(x,A,x) = x * x. [para(14(a,1),80(a,2,2)),rewrite([212(3),546(5),5(4),2(2)]),flip(a)].

2471 L(x,A,x) = x. [para(2436(a,1),11(a,1,2)),rewrite([11(3)]),flip(a)].

2478 (x * A) * x = x * (A * x). [para(2471(a,1),66(a,1,2))].

2500 x / (x' * (y / x')) = (x' * y)'. [para(2163(a,1),59(a,1,1)),rewrite([485(4)])].

2612 (x * (y / x))' * (x * y) = L(x,y,x). [para(2274(a,1),61(a,1)),flip(a)].

2669 (x / y) * ((y * A) * x) = x * (A * x). [para(82(a,1),10(a,2,2)),rewrite([101(4)])].

2679 (x * (A * x)) / ((y * A) * x) = x / y. [para(82(a,1),34(a,1,1,2)),rewrite([101(11)])].

2769 L(x',x,x * A) = x'. [para(2478(a,1),55(a,2,1,1)),rewrite([229(11)])].

2851 L(x / y,y / x,(y / x) * A) = x / y. [para(112(a,1),2769(a,1,1)),rewrite([112(8)])].

3776 (x * y)' * x = x' * (x / y). [para(101(a,1),11(a,1,2)),flip(a)].

3781 x / (x' * y) = x * (y' * x). [para(45(a,1),101(a,1,2,1,1)),flip(a)].

3943 L(x',x,y)' = (y' * (y / x))'. [back_rewrite(568),rewrite([3776(6)])].

3964 L(x / y,y / x,z) = z' * (z / (y / x)). [back_rewrite(205),rewrite([3776(7)])].

4080 x * ((x' / y) * x) = (x' * y)'. [back_rewrite(2500),rewrite([3781(5),112(3)])].

4630 (x * (A * x)) / y = x * (A * (x / y)). [para(78(a,1),102(a,2)),rewrite([2669(5)])].

4660 x / y = x * y'. [back_rewrite(2679),rewrite([4630(7),39(5),212(4),45(6)]),flip(a)].

4934 (x' * y)' = y' * x. [back_rewrite(4080),rewrite([4660(2),118(4),4660(4),23(4),45(5)]),flip(a)].

4952 L(x * y',y * x',z) = (y * x')'. [back_rewrite(3964),rewrite([4660(1),4660(3),4660(7),4660(9),11(11)])].

4971 L(x',x,y)' = x. [back_rewrite(3943),rewrite([4660(5),11(7),23(5)])].

5241 (x * y')' = y * x'. [back_rewrite(2851),rewrite([4660(1),4660(3),4660(5),4952(9),4660(4)])].

5280 (x * (y * x'))' * (x * y) = L(x,y,x). [back_rewrite(2612),rewrite([4660(1)])].

5347 L(x,y * z',z) = L(x,y,z). [back_rewrite(2274),rewrite([4660(1)])].

5436 L(x,y * z,L(u,z * u',y)) = L(x,y * z,(y * (z * u'))'). [back_rewrite(1930),rewrite([4660(2),4660(7)])].

5486 L(L(x,y * x',z),z * (y * x'),u) = (u * (z * (y * x')))' * (u * (z * y)). [back_rewrite(1460),rewrite([4660(1),4660(4),4660(8)])].

5513 (x * y') * y = x. [back_rewrite(1365),rewrite([4660(1),4660(5),4971(5)])].

5555 L(x',x,y) = x'. [back_rewrite(1119),rewrite([4660(4),11(6)])].

5556 L(x,x',y) = x. [back_rewrite(1117),rewrite([4660(5),23(5),11(5)])].

5590 L(x,y,z * y') = L(x,y,z). [back_rewrite(1007),rewrite([4660(1)])].

5667 L(x,y * x',(y * z)') = ((x * y') * (y * z)) * z'. [back_rewrite(755),rewrite([4660(1),4660(8),4934(11),5241(8),5555(11)])].

5733 L(x,y,x') = x. [back_rewrite(550),rewrite([4660(1),1121(4),4660(4),11(6),23(4)])].

5745 (x * y)' = y' * x'. [back_rewrite(410),rewrite([5555(2),4660(2)]),flip(a)].

5784 (x * y') * (y * z) = y' * ((y * x) * z). [back_rewrite(123),rewrite([4660(1)])].

5788 (x * y) * x' = x * (y * x'). [back_rewrite(117),rewrite([4660(4)])].

5801 L(x,y,z * (x' * y')) = (y' * ((y * x) * z')) * z. [back_rewrite(62),rewrite([4660(2),5745(2),4660(7),5745(7),5745(11),5745(11),5745(10)

,23(8),23(8)])].

6096 L(x * (y * z),x',y') = (x * y) * z. [back_rewrite(1403),rewrite([5745(9),23(7),23(7)])].

6097 L(L(x,y,z),z * y,(x' * y') * z') = (y' * ((y * x) * z')) * z. [back_rewrite(1294),rewrite([5745(5),5745(4),5745(11),5745(10),5784(15),5

745(16),5745(14),5745(14),5745(13),23(11),23(11),23(15)])].

6120 L(x,y,z' * (x' * y')) = (y' * ((y * x) * z)) * z'. [back_rewrite(420),rewrite([5745(3),5745(3),5745(7),5745(7),5745(5),23(3),23(3),23(4

),5555(7),5745(9),5745(9)]),flip(a)].

6297 (x * (x * y')) * ((y * x') * z) = L(x * z,x',y). [back_rewrite(1937),rewrite([5745(5),23(2),5745(3),23(2)])].

6512 L(x',y * x,z) = z' * ((z * (x' * y')) * y). [back_rewrite(1442),rewrite([5555(2),5745(6),5745(5),5784(10)])].

6514 x' * ((x * (y' * z')) * z) = L(y,z,x)'. [back_rewrite(1288),rewrite([5555(5),5745(5),5745(4),5784(9)]),flip(a)].

6522 x' * ((x * ((y * x') * z')) * (z * x)) = y. [back_rewrite(477),rewrite([5556(4),5745(5),5745(4),5745(3),23(2),5784(9)]),flip(a)].

6612 L(x,y * z,L(u,z * u',y)) = L(x,y * z,(u * z') * y'). [back_rewrite(5436),rewrite([5745(10),5745(9),23(8)])].

6634 (x * (y' * x')) * (x * y) = L(x,y,x). [back_rewrite(5280),rewrite([5745(4),5745(3),23(2),5788(4)])].

6701 L(x,y * x',z' * y') = (y' * ((y * x) * z)) * z'. [back_rewrite(5667),rewrite([5745(4),5784(10)])].

6785 L(L(x,y * x',z),z * (y * x'),u) = u' * ((u * ((x * y') * z')) * (z * y)). [back_rewrite(5486),rewrite([5745(12),5745(11),5745(10),23(9)

,5784(16)])].

7429 L(x',y * x,z) = L(x,y,z)'. [back_rewrite(6512),rewrite([6514(10)])].

7559 (x * (y' * z')) * (z * y) = x. [para(5513(a,1),66(a,2)),rewrite([5745(2),5745(7),66(11)])].

7562 L(x,y,x) = x. [back_rewrite(6634),rewrite([7559(6)]),flip(a)].

7644 (x * y) * y = x * (y * y). [para(7562(a,1),165(a,1,2,2)),flip(a)].

8222 (x * (y' * y')) * y = x * y'. [para(7644(a,1),5513(a,1,1))].

8705 L(x,y * (z' * z'),z) = L(x,y,z). [para(7644(a,1),5347(a,1,2)),rewrite([5347(8)])].

10236 L(x,y * x',z) = L(x',y,z)'. [para(23(a,1),7429(a,1,1))].

10241 L(L(x,y,z)',z * (y * x),u) = L(L(x,y,z),z * y,u)'. [para(66(a,1),7429(a,1,2))].

10302 x' * ((x * ((y * z') * u')) * (u * z)) = L(L(y',z,u),u * z,x)'. [back_rewrite(6785),rewrite([10236(3),10241(7)]),flip(a)].

10307 (x' * ((x * y) * z)) * z' = L(y',x,z')'. [back_rewrite(6701),rewrite([10236(6),5590(5)]),flip(a)].

10338 L(x,y * z,(u * z') * y') = L(x,y * z,L(u',z,y)'). [back_rewrite(6612),rewrite([10236(4)]),flip(a)].

10400 L(L(x',y,z),z,y)' = x. [back_rewrite(6522),rewrite([10302(9),1705(4)])].

10401 L(x,y,z' * (x' * y')) = L(x',y,z')'. [back_rewrite(6120),rewrite([10307(12)])].

10414 (x' * ((x * y) * z')) * z = L(y,x,z). [back_rewrite(6097),rewrite([10338(8),23(4),5733(5)]),flip(a)].

10457 L(x,y,z * (x' * y')) = L(x,y,z). [back_rewrite(5801),rewrite([10414(11)])].

10496 L(x',y,z')' = L(x,y,z'). [back_rewrite(10401),rewrite([10457(6)]),flip(a)].

10644 L(L(x',y,z),z,y) = x'. [para(10400(a,1),23(a,1,1)),flip(a)].

10736 L(L(x,y,z),z,y) = x. [para(23(a,1),10644(a,1,1,1)),rewrite([23(4)])].

16022 L(x',y,z)' = L(x,y,z). [para(23(a,1),10496(a,1,1,3)),rewrite([23(5)])].

16334 L(x,y,z)' = L(x',y,z). [para(16022(a,1),23(a,1,1))].

16394 L(x,y * x,z) = L(x,y,z). [para(7429(a,1),16022(a,1,1)),rewrite([16334(2),16334(3),23(2)]),flip(a)].

17374 L(L(x,y,z),z,y * x) = x. [para(16394(a,1),10736(a,1,1))].

17681 L(L(x * y,x',z),z,y) = x * y. [para(11(a,1),17374(a,1,3))].

33948 x * L(y,z,x) = L(x * y,x',z). [para(8222(a,1),1266(a,1,2,1)),rewrite([5745(5),5745(4),23(2),23(2),12(3),6297(7),8705(8)]),flip(a)].

36237 (x * y) * (z * x) = x * ((y * z) * x). [para(17681(a,1),66(a,1,2)),rewrite([33948(7),6096(8)])].

36238 $F. [resolve(36237,a,18,a)].

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

% Proof 1 at 43.31 (+ 0.13) seconds.

% Length of proof is 116.

% Level of proof is 27.

% Maximum clause weight is 28.000.

% Given clauses 1137.

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

2 0 * x = x. [assumption].

3 x * 0 = x. [assumption].

4 x * x' = 0. [assumption].

5 x' * x = 0. [assumption].

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

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

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

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

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

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

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

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

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

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

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

18 (c1 * c2) * (D * c1) != c1 * ((c2 * D) * c1). [deny(1)].

22 x \ 0 = x'. [para(4(a,1),7(a,1,2))].

23 x'' = x. [para(5(a,1),7(a,1,2)),rewrite([22(3)])].

25 x / 0 = x. [para(3(a,1),8(a,1,1))].

27 0 / x = x'. [para(5(a,1),8(a,1,1))].

34 (x * (y * (x * z))) / z = x * (y * x). [para(10(a,1),8(a,1,1))].

35 x * ((y / x) * (x * z)) = (x * y) * z. [para(9(a,1),10(a,1,1,2)),flip(a)].

38 x \ y = x' * y. [para(6(a,1),11(a,1,2)),flip(a)].

39 x / (y * x) = y'. [para(11(a,1),8(a,1,1))].

45 x * (x' * y) = y. [back_rewrite(6),rewrite([38(1)])].

47 (x * (x * y)) / y = x * x. [para(12(a,1),8(a,1,1))].

56 (x * y) * y' = R(x,y,y'). [para(4(a,1),14(a,1,2)),rewrite([25(5)])].

58 (x * y') * y = R(x,y',y). [para(5(a,1),14(a,1,2)),rewrite([25(5)])].

59 R(x,y,z) * (y * z) = (x * y) * z. [para(14(a,1),9(a,1,1))].

65 R(x',x * y,z) = (y * z) / ((x * y) * z). [para(11(a,1),14(a,1,1,1)),flip(a)].

71 A' * R(x,A,A') = A' * x. [para(4(a,1),16(a,1,2)),rewrite([3(5),56(10)]),flip(a)].

72 x' * ((x * A) * x') = A * x'. [para(5(a,1),16(a,1,1)),rewrite([2(5)]),flip(a)].

79 x' * (((x * y) * A) * x') = y * (A * x'). [para(11(a,1),16(a,1,1)),flip(a)].

93 (x * y) / x' = x * (y * x). [para(4(a,1),34(a,1,1,2,2)),rewrite([3(2)])].

104 (x / y)' = y / x. [para(9(a,1),39(a,1,2)),flip(a)].

115 (x * y) * x' = x * (y / x). [para(4(a,1),35(a,1,2,2)),rewrite([3(3)]),flip(a)].

116 (x' * y) * x = x' * (y / x'). [para(5(a,1),35(a,1,2,2)),rewrite([3(5)]),flip(a)].

121 (x / y) * (y * z) = y' * ((y * x) * z). [para(35(a,1),11(a,1,2)),flip(a)].

130 (x * y) * (x' * z) = x * ((y / x) * z). [para(45(a,1),35(a,1,2,2)),flip(a)].

131 A / x = A * x'. [back_rewrite(72),rewrite([115(5),11(5)])].

137 (x * y) / ((z * x) * y) = R(z,x,y)'. [para(14(a,1),104(a,1,1)),flip(a)].

141 R(x',x * y,z) = R(x,y,z)'. [back_rewrite(65),rewrite([137(7)])].

143 A * (x * A)' = x'. [para(131(a,1),39(a,1))].

144 (A * x')' = x / A. [para(131(a,1),104(a,1,1))].

179 (x * A)' = A' * x'. [para(143(a,1),11(a,1,2)),flip(a)].

184 (A * x)' = x' / A. [para(23(a,1),144(a,1,1,2))].

207 (A * x) * (x' / A) = 0. [para(184(a,1),4(a,1,2))].

211 (A' * x)' / A = x'. [para(45(a,1),184(a,1,1)),flip(a)].

261 (x * A) * (A' * x') = 0. [para(179(a,1),4(a,1,2))].

273 R(A,x,x' / A) = (x * (x' / A))'. [para(207(a,1),14(a,1,1)),rewrite([27(6)]),flip(a)].

284 (x * y) / (x' * y) = x * x. [para(45(a,1),47(a,1,1,2))].

293 (A' * x)' = x' * A. [para(211(a,1),9(a,1,1)),flip(a)].

377 R(A',x,x') = A'. [para(261(a,1),10(a,2,2)),rewrite([56(7),71(7),56(5),3(8)])].

383 A' / x' = A' * x. [para(261(a,1),34(a,1,1,2)),rewrite([3(4),56(11),71(11)])].

394 R(x / y,y,y') = x * y'. [para(9(a,1),56(a,1,1)),flip(a)].

400 (R(x,y,y') * z) / (y' * z) = R(x * y,y',z). [para(56(a,1),14(a,1,1,1))].

405 x' / R(y,x,x') = (y * x)'. [para(56(a,1),39(a,1,2))].

420 x * (x' / A) = A'. [para(184(a,1),377(a,1,3)),rewrite([141(8),273(5),23(6)])].

440 x / A = x * A'. [para(420(a,1),45(a,1,2)),rewrite([23(5)]),flip(a)].

470 (A * x)' = x' * A'. [back_rewrite(184),rewrite([440(6)])].

493 R(x,A',A) = x. [para(440(a,1),9(a,1,1)),rewrite([58(5)])].

502 (x * (y * (x * z'))) * z = R(x * (y * x),z',z). [para(10(a,1),58(a,1,1))].

523 A' / x = A' * x'. [para(23(a,1),383(a,1,2))].

542 R(x,y,y' * z) * z = (x * y) * (y' * z). [para(45(a,1),59(a,1,2))].

551 R(R(x,y,z),y * z,(y * z)') = ((x * y) * z) * (y * z)'. [para(59(a,1),56(a,1,1)),flip(a)].

575 x / A' = x * A. [para(523(a,1),104(a,1,1)),rewrite([293(5),23(2)]),flip(a)].

1341 R(x * x,x' * y,(x' * y)') = (x * y) * (x' * y)'. [para(284(a,1),394(a,1,1))].

1742 R(x,y * A',A * y') = x. [para(58(a,1),79(a,2)),rewrite([470(5),23(3),502(8),493(7),115(5),8(3),11(3),470(4),23(2)]),flip(a)].

2065 R(x,y,y') = x. [para(9(a,1),1742(a,1,2)),rewrite([575(4),179(4),45(6)])].

2080 (x * y) * (x' * y)' = x * x. [back_rewrite(1341),rewrite([2065(7)]),flip(a)].

2106 ((x * y) * z) * (y * z)' = R(x,y,z). [back_rewrite(551),rewrite([2065(5)]),flip(a)].

2117 (x * y)' = y' / x. [back_rewrite(405),rewrite([2065(3)]),flip(a)].

2121 R(x * y,y',z) = (x * z) / (y' * z). [back_rewrite(400),rewrite([2065(2)]),flip(a)].

2126 x / y = x * y'. [back_rewrite(394),rewrite([2065(3)])].

2127 (x * y) * y' = x. [back_rewrite(56),rewrite([2065(5)])].

2136 ((x * y) * z) * (z' * y') = R(x,y,z). [back_rewrite(2106),rewrite([2117(4),2126(4)])].

2146 (x * y) * (y' * x) = x * x. [back_rewrite(2080),rewrite([2117(4),2126(4),23(4)])].

2375 R(x * y,y',z) = (x * z) * (z' * y). [back_rewrite(2121),rewrite([2126(7),2117(7),2126(7),23(7)])].

2378 (x * y)' = y' * x'. [back_rewrite(2117),rewrite([2126(4)])].

3044 (x * y) * (x' * z) = x * ((y * x') * z). [back_rewrite(130),rewrite([2126(5)])].

3047 (x * y') * (y * z) = y' * ((y * x) * z). [back_rewrite(121),rewrite([2126(1)])].

3050 (x' * y) * x = x' * (y * x). [back_rewrite(116),rewrite([2126(6),23(6)])].

3051 (x * y) * x' = x * (y * x'). [back_rewrite(115),rewrite([2126(4)])].

3058 (x * y) * x = x * (y * x). [back_rewrite(93),rewrite([2126(3),23(3)])].

3649 (x' * (y * x)) * (x' * y) = (x' * y) * y. [para(45(a,1),3058(a,2,2)),rewrite([3050(3)])].

3715 R(R(x,y,z)',(x * y) * z,u) = R(R(x,y,z),y * z,u)'. [para(59(a,1),141(a,1,2))].

4013 (x' * y) * y = x' * (y * y). [para(2146(a,1),10(a,2,2)),rewrite([2127(4)])].

4018 x' * ((x * y) * y) = y * y. [para(23(a,1),2146(a,1,2,1)),rewrite([3047(4)])].

4050 (x' * (y * x)) * (x' * y) = x' * (y * y). [back_rewrite(3649),rewrite([4013(9)])].

4434 (x * y) * y = x * (y * y). [para(4018(a,1),11(a,1,2)),rewrite([23(2)]),flip(a)].

5583 (x' * y) * (y' * (x * y)) = y. [para(3050(a,1),11(a,1,2)),rewrite([2378(3),23(3)])].

6420 (x' * y) * (y' * (x * x)) = x. [para(5583(a,1),3051(a,1,1)),rewrite([2378(3),23(3),45(3),2378(8),23(8),4050(8)]),flip(a)].

6850 R(x,y' * z,z' * (y * y)) * y = (x * (y' * z)) * (z' * (y * y)). [para(6420(a,1),59(a,1,2))].

22929 R((x * y) * z,z',y') = x * (y * z). [para(2127(a,1),2375(a,2,1)),rewrite([23(7)])].

22939 R((x * y) * z,z',x) = x * (y * z). [para(3058(a,1),2375(a,2,1)),rewrite([3044(9),2127(7)])].

23382 R(R(x,y,z),y * z,x * y) = x. [para(2136(a,1),22939(a,1,1)),rewrite([2378(5),23(3),23(3),45(9),2127(7)])].

23384 R(x,y,(x * y) * z) = R(x,y,z). [para(2136(a,1),22939(a,2)),rewrite([2127(4),2127(3),23(2)])].

23637 R(R(x,y,z),y * z,y)' = x'. [para(11(a,1),23382(a,1,3)),rewrite([141(3),3715(5)])].

26924 R(R(x,y,z),y * z,y) = x. [para(23637(a,1),23(a,1,1)),rewrite([23(2)]),flip(a)].

27136 R(R(x,y,y' * z),z,y) = x. [para(45(a,1),26924(a,1,2))].

27146 R(R(x,y * z,y),y * (z * y),y * z) = x. [para(3058(a,1),26924(a,1,2))].

27305 R(x,(y * z) * (x * y),y * z) = R(x,y,z). [para(23382(a,1),26924(a,1,1))].

27345 R(x,y * (z * y),y * z) = R(x,y,z). [para(26924(a,1),26924(a,1,1)),rewrite([3058(2)])].

27393 R(R(x,y * z,y),y,z) = x. [back_rewrite(27146),rewrite([27345(6)])].

27994 R(R(x,y,z),z,z' * y) = x. [para(45(a,1),27393(a,1,1,2))].

28032 (R(x,y,z) * z) * (z' * y) = x * y. [para(27393(a,1),542(a,1,1)),rewrite([45(4)]),flip(a)].

28188 R(x,y' * z,z' * (y * y)) = R(x,z,y). [para(27136(a,1),27136(a,1,1)),rewrite([2378(6),23(6),4434(6)]),flip(a)].

28328 (x * (y' * z)) * (z' * (y * y)) = R(x,z,y) * y. [back_rewrite(6850),rewrite([28188(6)]),flip(a)].

29301 R(R(x,y,z),z,x * y) = x. [para(27994(a,1),23384(a,2)),rewrite([28032(6)])].

29810 R(R(x * y,y',z),z,x) = x * y. [para(2127(a,1),29301(a,1,3))].

29961 R(x,y * (x * z),y) = R(x,z,y). [para(29301(a,1),26924(a,1,1))].

29977 R(x,y,y * z) = R(x,y,z). [back_rewrite(27305),rewrite([29961(5)])].

31749 R(x,y,z) * z = R(x * z,z',y). [para(29977(a,1),2375(a,1)),rewrite([2378(9),23(9),4434(9),28328(10)]),flip(a)].

42177 (x * y) * (z * x) = x * ((y * z) * x). [para(29810(a,1),59(a,1,1)),rewrite([31749(7),22929(8),3058(6)])].

42178 $F. [resolve(42177,a,18,a)].

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

% Proof 1 at 68.22 (+ 0.52) seconds.

% Length of proof is 43.

% Level of proof is 11.

% Maximum clause weight is 19.000.

% Given clauses 2131.

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

2 0 * x = x. [assumption].

3 x * 0 = x. [assumption].

4 x * x' = 0. [assumption].

5 x' * x = 0. [assumption].

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

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

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

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

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

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

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

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

18 (c1 * c2) * (D * c1) != c1 * ((c2 * D) * c1). [deny(1)].

22 x \ 0 = x'. [para(4(a,1),7(a,1,2))].

23 x'' = x. [para(5(a,1),7(a,1,2)),rewrite([22(3)])].

34 (x * (y * (x * z))) / z = x * (y * x). [para(10(a,1),8(a,1,1))].

35 x * ((y / x) * (x * z)) = (x * y) * z. [para(9(a,1),10(a,1,1,2)),flip(a)].

38 x \ y = x' * y. [para(6(a,1),11(a,1,2)),flip(a)].

39 x / (y * x) = y'. [para(11(a,1),8(a,1,1))].

45 x * (x' * y) = y. [back_rewrite(6),rewrite([38(1)])].

66 x' * ((x * A) * x') = A * x'. [para(5(a,1),16(a,1,1)),rewrite([2(5)]),flip(a)].

68 (x / y) * ((y * A) * (x / y)) = x * (A * (x / y)). [para(9(a,1),16(a,1,1)),flip(a)].

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

102 x * ((x * y)' * x) = x / y. [para(5(a,1),34(a,1,1,2)),rewrite([3(2)]),flip(a)].

103 ((x / y) * (z * x)) / y = (x / y) * (z * (x / y)). [para(9(a,1),34(a,1,1,2,2))].

113 (x * (y * z)) / (x' * z) = x * (y * x). [para(45(a,1),34(a,1,1,2,2))].

128 (x * y) * x' = x * (y / x). [para(4(a,1),35(a,1,2,2)),rewrite([3(3)]),flip(a)].

144 A / x = A * x'. [back_rewrite(66),rewrite([128(5),11(5)])].

149 A * (x * A)' = x'. [para(144(a,1),39(a,1))].

215 (x * A)' = A' * x'. [para(149(a,1),11(a,1,2)),flip(a)].

1348 (x / y) * ((y * A) * x) = x * (A * x). [para(72(a,1),10(a,2,2)),rewrite([102(4)])].

1357 (x * (A * x)) / ((y * A) * x) = x / y. [para(72(a,1),34(a,1,1,2)),rewrite([102(11)])].

2989 (x * y)' * x = x' * (x / y). [para(102(a,1),11(a,1,2)),flip(a)].

3249 (x * (A * x)) / y = x * (A * (x / y)). [para(68(a,1),103(a,2)),rewrite([1348(5)])].

3299 x / y = x * y'. [back_rewrite(1357),rewrite([3249(7),39(5),215(4),45(6)]),flip(a)].

3466 (x * y)' * x = y'. [back_rewrite(2989),rewrite([3299(5),11(7)])].

3972 (x * (y * z)) * (x' * z)' = x * (y * x). [back_rewrite(113),rewrite([3299(5)])].

3997 (x * y) * y' = x. [back_rewrite(8),rewrite([3299(2)])].

4355 (x * y)' = y' * x'. [para(11(a,1),3466(a,1,1,1)),flip(a)].

4453 (x * (y * z)) * (z' * x) = x * (y * x). [back_rewrite(3972),rewrite([4355(5),23(5)])].

64467 (x * y) * (z * x) = x * ((y * z) * x). [para(3997(a,1),4453(a,1,1,2)),rewrite([23(3)])].

64468 $F. [resolve(64467,a,18,a)].

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