% Proof 1 at 3.50 (+ 0.02) seconds.

% Length of proof is 67.

% Level of proof is 13.

% Maximum clause weight is 21.000.

% Given clauses 396.

2 z * ((x * (A / B)) * z) = (z * x) * ((A / B) * z) # label(non_clause) # label(goal). [goal].

4 0 * x = x. [assumption].

5 x * 0 = x. [assumption].

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

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

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

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

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

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

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

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

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

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

17 x * ((y * B) * x) = (x * y) * (B * x). [assumption].

18 (x * y) * (B * x) = x * ((y * B) * x). [copy(17),flip(a)].

20 (c3 * c4) * ((A / B) * c3) != c3 * ((c4 * (A / B)) * c3). [deny(2)].

25 x \ 0 = x'. [para(6(a,1),9(a,1,2))].

26 x'' = x. [para(7(a,1),9(a,1,2)),rewrite([25(3)])].

33 x \ y = x' * y. [para(8(a,1),12(a,1,2)),flip(a)].

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

37 x * (x' * y) = y. [back_rewrite(8),rewrite([33(1)])].

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

44 x * ((y / x) * (x * z)) = (x * y) * z. [para(11(a,1),14(a,1,1,2)),flip(a)].

52 x * ((x' * A) * x) = A * x. [para(6(a,1),16(a,1,1)),rewrite([4(4)]),flip(a)].

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

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

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

65 x * ((x' * B) * x) = B * x. [para(6(a,1),18(a,1,1)),rewrite([4(4)]),flip(a)].

66 B' * ((x * B) * B') = B' * x. [para(6(a,1),18(a,1,2)),rewrite([5(5)]),flip(a)].

80 (x / y)' = y / x. [para(11(a,1),34(a,1,2)),flip(a)].

141 (x * A) * x' = x * (A * x'). [para(52(a,1),37(a,1,2)),rewrite([26(6)]),flip(a)].

148 (x * B) * x' = x * (B * x'). [para(65(a,1),37(a,1,2)),rewrite([26(6)]),flip(a)].

152 x * ((x * y)' * x) = x / y. [para(7(a,1),43(a,1,1,2)),rewrite([5(2)]),flip(a)].

153 ((x / y) * (z * x)) / y = (x / y) * (z * (x / y)). [para(11(a,1),43(a,1,1,2,2))].

164 (x * (y * z)) / (x' * z) = x * (y * x). [para(37(a,1),43(a,1,1,2,2))].

195 (x * y)' * x = x' * (x / y). [para(152(a,1),12(a,1,2)),flip(a)].

196 x' / (x * y) = x' * (y' * x'). [para(12(a,1),152(a,1,2,1,1)),flip(a)].

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

233 x * (B / x) = x * (B * x'). [back_rewrite(148),rewrite([214(4)])].

234 x * (A / x) = x * (A * x'). [back_rewrite(141),rewrite([214(4)])].

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

262 B / x = B * x'. [para(233(a,1),12(a,1,2)),rewrite([12(6)]),flip(a)].

266 (B * x') * x = B. [para(262(a,1),11(a,1,1))].

267 B * (x * B)' = x'. [para(262(a,1),34(a,1))].

278 (B * x) * x' = B. [para(26(a,1),266(a,1,1,2))].

315 (B * x)' = x' / B. [para(278(a,1),34(a,1,2)),flip(a)].

325 (x * B)' = B' * x'. [para(267(a,1),12(a,1,2)),flip(a)].

386 (x * B) * (B' * x') = 0. [para(325(a,1),6(a,1,2))].

469 (B' * x) * x' = B'. [para(386(a,1),14(a,2,2)),rewrite([66(8),5(9)])].

483 x * (x' / B) = B'. [para(12(a,1),469(a,1,1)),rewrite([315(3)])].

513 x / B = x * B'. [para(483(a,1),37(a,1,2)),rewrite([26(5)]),flip(a)].

552 (c3 * c4) * ((A * B') * c3) != c3 * ((c4 * (A * B')) * c3). [back_rewrite(20),rewrite([513(6),513(15)])].

556 (x * A) * A' = x. [para(53(a,1),12(a,1,2)),rewrite([26(3),37(5)]),flip(a)].

578 (x * A)' = A' / x. [para(556(a,1),34(a,1,2)),flip(a)].

716 (x / y) * ((y * A) * x) = x * (A * x). [para(57(a,1),14(a,2,2)),rewrite([195(3),37(4)])].

726 (x * (A * x)) / ((y * A) * x) = x / y. [para(57(a,1),43(a,1,1,2)),rewrite([195(10),37(11)])].

1092 A / x = A * x'. [para(234(a,1),12(a,1,2)),rewrite([12(6)]),flip(a)].

1183 A * (A' / x) = x'. [para(1092(a,1),34(a,1)),rewrite([578(4)])].

1232 A' / x = A' * x'. [para(1183(a,1),12(a,1,2)),flip(a)].

1286 (x * A)' = A' * x'. [back_rewrite(578),rewrite([1232(6)])].

5895 (x * (A * x)) / y = x * (A * (x / y)). [para(56(a,1),153(a,2)),rewrite([716(5)])].

6027 x / y = x * y'. [back_rewrite(726),rewrite([5895(7),34(5),1286(4),37(6)]),flip(a)].

7337 (x * y)' = y' * x'. [back_rewrite(253),rewrite([6027(2),214(5),6027(3),12(6)]),flip(a)].

7380 (x * (y * z)) * (z' * x) = x * (y * x). [back_rewrite(164),rewrite([6027(5),7337(5),26(5)])].

7403 (x * y) * y' = x. [back_rewrite(10),rewrite([6027(2)])].

17708 (x * y) * (z * x) = x * ((y * z) * x). [para(7403(a,1),7380(a,1,1,2)),rewrite([26(3)])].

17709 $F. [resolve(17708,a,552,a)].

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

============================== PROOF =================================

% Proof 2 at 3.50 (+ 0.02) seconds.

% Length of proof is 51.

% Level of proof is 13.

% Maximum clause weight is 21.000.

% Given clauses 396.

3 z * ((x * (A \ B)) * z) = (z * x) * ((A \ B) * z) # label(non_clause) # label(goal). [goal].

4 0 * x = x. [assumption].

5 x * 0 = x. [assumption].

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

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

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

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

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

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

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

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

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

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

21 (c5 * c6) * ((A \ B) * c5) != c5 * ((c6 * (A \ B)) * c5). [deny(3)].

25 x \ 0 = x'. [para(6(a,1),9(a,1,2))].

26 x'' = x. [para(7(a,1),9(a,1,2)),rewrite([25(3)])].

33 x \ y = x' * y. [para(8(a,1),12(a,1,2)),flip(a)].

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

36 (c5 * c6) * ((A' * B) * c5) != c5 * ((c6 * (A' * B)) * c5). [back_rewrite(21),rewrite([33(6),33(15)])].

37 x * (x' * y) = y. [back_rewrite(8),rewrite([33(1)])].

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

44 x * ((y / x) * (x * z)) = (x * y) * z. [para(11(a,1),14(a,1,1,2)),flip(a)].

52 x * ((x' * A) * x) = A * x. [para(6(a,1),16(a,1,1)),rewrite([4(4)]),flip(a)].

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

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

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

80 (x / y)' = y / x. [para(11(a,1),34(a,1,2)),flip(a)].

141 (x * A) * x' = x * (A * x'). [para(52(a,1),37(a,1,2)),rewrite([26(6)]),flip(a)].

152 x * ((x * y)' * x) = x / y. [para(7(a,1),43(a,1,1,2)),rewrite([5(2)]),flip(a)].

153 ((x / y) * (z * x)) / y = (x / y) * (z * (x / y)). [para(11(a,1),43(a,1,1,2,2))].

164 (x * (y * z)) / (x' * z) = x * (y * x). [para(37(a,1),43(a,1,1,2,2))].

195 (x * y)' * x = x' * (x / y). [para(152(a,1),12(a,1,2)),flip(a)].

196 x' / (x * y) = x' * (y' * x'). [para(12(a,1),152(a,1,2,1,1)),flip(a)].

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

234 x * (A / x) = x * (A * x'). [back_rewrite(141),rewrite([214(4)])].

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

556 (x * A) * A' = x. [para(53(a,1),12(a,1,2)),rewrite([26(3),37(5)]),flip(a)].

578 (x * A)' = A' / x. [para(556(a,1),34(a,1,2)),flip(a)].

716 (x / y) * ((y * A) * x) = x * (A * x). [para(57(a,1),14(a,2,2)),rewrite([195(3),37(4)])].

726 (x * (A * x)) / ((y * A) * x) = x / y. [para(57(a,1),43(a,1,1,2)),rewrite([195(10),37(11)])].

1092 A / x = A * x'. [para(234(a,1),12(a,1,2)),rewrite([12(6)]),flip(a)].

1183 A * (A' / x) = x'. [para(1092(a,1),34(a,1)),rewrite([578(4)])].

1232 A' / x = A' * x'. [para(1183(a,1),12(a,1,2)),flip(a)].

1286 (x * A)' = A' * x'. [back_rewrite(578),rewrite([1232(6)])].

5895 (x * (A * x)) / y = x * (A * (x / y)). [para(56(a,1),153(a,2)),rewrite([716(5)])].

6027 x / y = x * y'. [back_rewrite(726),rewrite([5895(7),34(5),1286(4),37(6)]),flip(a)].

7337 (x * y)' = y' * x'. [back_rewrite(253),rewrite([6027(2),214(5),6027(3),12(6)]),flip(a)].

7380 (x * (y * z)) * (z' * x) = x * (y * x). [back_rewrite(164),rewrite([6027(5),7337(5),26(5)])].

7403 (x * y) * y' = x. [back_rewrite(10),rewrite([6027(2)])].

17708 (x * y) * (z * x) = x * ((y * z) * x). [para(7403(a,1),7380(a,1,1,2)),rewrite([26(3)])].

17710 $F. [resolve(17708,a,36,a)].

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

============================== PROOF =================================

% Proof 3 at 3.51 (+ 0.02) seconds.

% Length of proof is 50.

% Level of proof is 13.

% Maximum clause weight is 19.000.

% Given clauses 396.

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

4 0 * x = x. [assumption].

5 x * 0 = x. [assumption].

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

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

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

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

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

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

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

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

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

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

19 (c1 * c2) * ((A * B) * c1) != c1 * ((c2 * (A * B)) * c1). [deny(1)].

25 x \ 0 = x'. [para(6(a,1),9(a,1,2))].

26 x'' = x. [para(7(a,1),9(a,1,2)),rewrite([25(3)])].

33 x \ y = x' * y. [para(8(a,1),12(a,1,2)),flip(a)].

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

37 x * (x' * y) = y. [back_rewrite(8),rewrite([33(1)])].

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

44 x * ((y / x) * (x * z)) = (x * y) * z. [para(11(a,1),14(a,1,1,2)),flip(a)].

52 x * ((x' * A) * x) = A * x. [para(6(a,1),16(a,1,1)),rewrite([4(4)]),flip(a)].

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

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

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

80 (x / y)' = y / x. [para(11(a,1),34(a,1,2)),flip(a)].

141 (x * A) * x' = x * (A * x'). [para(52(a,1),37(a,1,2)),rewrite([26(6)]),flip(a)].

152 x * ((x * y)' * x) = x / y. [para(7(a,1),43(a,1,1,2)),rewrite([5(2)]),flip(a)].

153 ((x / y) * (z * x)) / y = (x / y) * (z * (x / y)). [para(11(a,1),43(a,1,1,2,2))].

164 (x * (y * z)) / (x' * z) = x * (y * x). [para(37(a,1),43(a,1,1,2,2))].

195 (x * y)' * x = x' * (x / y). [para(152(a,1),12(a,1,2)),flip(a)].

196 x' / (x * y) = x' * (y' * x'). [para(12(a,1),152(a,1,2,1,1)),flip(a)].

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

234 x * (A / x) = x * (A * x'). [back_rewrite(141),rewrite([214(4)])].

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

556 (x * A) * A' = x. [para(53(a,1),12(a,1,2)),rewrite([26(3),37(5)]),flip(a)].

578 (x * A)' = A' / x. [para(556(a,1),34(a,1,2)),flip(a)].

716 (x / y) * ((y * A) * x) = x * (A * x). [para(57(a,1),14(a,2,2)),rewrite([195(3),37(4)])].

726 (x * (A * x)) / ((y * A) * x) = x / y. [para(57(a,1),43(a,1,1,2)),rewrite([195(10),37(11)])].

1092 A / x = A * x'. [para(234(a,1),12(a,1,2)),rewrite([12(6)]),flip(a)].

1183 A * (A' / x) = x'. [para(1092(a,1),34(a,1)),rewrite([578(4)])].

1232 A' / x = A' * x'. [para(1183(a,1),12(a,1,2)),flip(a)].

1286 (x * A)' = A' * x'. [back_rewrite(578),rewrite([1232(6)])].

5895 (x * (A * x)) / y = x * (A * (x / y)). [para(56(a,1),153(a,2)),rewrite([716(5)])].

6027 x / y = x * y'. [back_rewrite(726),rewrite([5895(7),34(5),1286(4),37(6)]),flip(a)].

7337 (x * y)' = y' * x'. [back_rewrite(253),rewrite([6027(2),214(5),6027(3),12(6)]),flip(a)].

7380 (x * (y * z)) * (z' * x) = x * (y * x). [back_rewrite(164),rewrite([6027(5),7337(5),26(5)])].

7403 (x * y) * y' = x. [back_rewrite(10),rewrite([6027(2)])].

17708 (x * y) * (z * x) = x * ((y * z) * x). [para(7403(a,1),7380(a,1,1,2)),rewrite([26(3)])].

17711 $F. [resolve(17708,a,19,a)].

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

% Proof 1 at 48.37 (+ 0.27) seconds.

% Length of proof is 99.

% Level of proof is 16.

% Maximum clause weight is 30.000.

% Given clauses 1703.

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

4 0 * x = x. [assumption].

5 x * 0 = x. [assumption].

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

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

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

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

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

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

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

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

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

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

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

17 x * ((B * y) * x) = (x * B) * (y * x). [assumption].

18 (x * B) * (y * x) = x * ((B * y) * x). [copy(17),flip(a)].

19 (c1 * (A * B)) * (c2 * c1) != c1 * (((A * B) * c2) * c1). [deny(1)].

25 x \ 0 = x'. [para(6(a,1),9(a,1,2))].

26 x'' = x. [para(7(a,1),9(a,1,2)),rewrite([25(3)])].

33 x \ y = x' * y. [para(8(a,1),12(a,1,2)),flip(a)].

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

37 x * (x' * y) = y. [back_rewrite(8),rewrite([33(1)])].

39 (x * (x * y)) / y = x * x. [para(13(a,1),10(a,1,1))].

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

44 x * ((y / x) * (x * z)) = (x * y) * z. [para(11(a,1),14(a,1,1,2)),flip(a)].

54 A' * ((A * x) * A') = x * A'. [para(7(a,1),16(a,1,1)),rewrite([4(5)]),flip(a)].

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

67 (x * A) * (y * (z * (y * x))) = x * ((A * (y * (z * y))) * x). [para(14(a,1),16(a,1,2))].

69 (x * B) * x = x * (B * x). [para(4(a,1),18(a,1,2)),rewrite([5(6)])].

71 B' * ((B * x) * B') = x * B'. [para(7(a,1),18(a,1,1)),rewrite([4(5)]),flip(a)].

72 x * ((B * x') * x) = x * B. [para(7(a,1),18(a,1,2)),rewrite([5(4)]),flip(a)].

84 (x * B) * (y * (z * (y * x))) = x * ((B * (y * (z * y))) * x). [para(14(a,1),18(a,1,2))].

88 (x / y)' = y / x. [para(11(a,1),34(a,1,2)),flip(a)].

127 (x * y) / (x' * y) = x * x. [para(37(a,1),39(a,1,1,2))].

151 (x * B)' * (x * (B * x)) = x. [para(69(a,1),12(a,1,2))].

164 (x * y) / x' = x * (y * x). [para(6(a,1),43(a,1,1,2,2)),rewrite([5(2)])].

166 x * ((x * y)' * x) = x / y. [para(7(a,1),43(a,1,1,2)),rewrite([5(2)]),flip(a)].

168 x * ((y / (x * z)) * x) = (x * y) / z. [para(11(a,1),43(a,1,1,2)),flip(a)].

192 (A * x') * x = A. [para(55(a,1),12(a,1,2)),rewrite([12(4)]),flip(a)].

195 (A * x) * x' = A. [para(55(a,1),37(a,1,2)),rewrite([37(4),26(4)]),flip(a)].

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

214 (x / y) * (y * z) = y' * ((y * x) * z). [para(44(a,1),12(a,1,2)),flip(a)].

222 (x * y) * (x' * z) = x * ((y / x) * z). [para(37(a,1),44(a,1,2,2)),flip(a)].

232 x / B = x * B'. [back_rewrite(71),rewrite([210(7),12(7)])].

233 x / A = x * A'. [back_rewrite(54),rewrite([210(7),12(7)])].

249 (A * x)' = x' * A'. [para(195(a,1),34(a,1,2)),rewrite([233(3)]),flip(a)].

262 (x * B) * B' = x. [para(232(a,1),10(a,1))].

263 (x * B') * B = x. [para(232(a,1),11(a,1,1))].

269 (x * (y * (x * B))) * B' = x * (y * x). [para(232(a,1),43(a,1))].

270 (x * A) * A' = x. [para(233(a,1),10(a,1))].

271 (x * A') * A = x. [para(233(a,1),11(a,1,1))].

297 x / B' = x * B. [para(262(a,1),10(a,1,1))].

300 B' * ((A * (x * B)) * B') = (B' * A) * x. [para(262(a,1),16(a,1,2)),flip(a)].

301 (x * B)' = B' / x. [para(262(a,1),34(a,1,2)),flip(a)].

307 x' * ((x * B') * (B * x)) = x. [back_rewrite(151),rewrite([301(3),214(7)])].

317 (x * (y * (x * B'))) * B = x * (y * x). [para(14(a,1),263(a,1,1))].

321 x / A' = x * A. [para(270(a,1),10(a,1,1))].

327 (x * A) * (y * (x * A)) = x * ((A * y) * (x * A)). [para(270(a,1),43(a,1,1,2,2)),rewrite([16(4),321(7),14(6)]),flip(a)].

343 A * ((B * (x * A')) * A) = (A * B) * x. [para(271(a,1),18(a,1,2)),flip(a)].

827 (B * x') * x = B. [para(72(a,1),12(a,1,2)),rewrite([12(4)]),flip(a)].

830 (B * x) * x' = B. [para(72(a,1),37(a,1,2)),rewrite([37(4),26(4)]),flip(a)].

836 B / x = B * x'. [para(827(a,1),10(a,1,1))].

848 (B * (x' * A')) * (A * x) = B. [para(249(a,1),827(a,1,1,2))].

914 x * (B' * x)' = B. [para(37(a,1),830(a,1,1))].

929 B * (B' / x) = x'. [para(836(a,1),34(a,1)),rewrite([301(4)])].

931 (B' * x)' = x' * B. [para(914(a,1),12(a,1,2)),flip(a)].

941 B' / x = B' * x'. [para(929(a,1),12(a,1,2)),flip(a)].

980 (x * B)' = B' * x'. [back_rewrite(301),rewrite([941(6)])].

1046 (A * (x' * B)) * (B' * x) = A. [para(931(a,1),192(a,1,1,2))].

1059 (B' * x') * x = B'. [para(941(a,1),11(a,1,1))].

1118 (B' * x) * x' = B'. [para(26(a,1),1059(a,1,1,2))].

1396 (x * y) * ((A * (x' * (z * x'))) * (x * y)) = ((x * y) * A) * (x' * (z * y)). [para(12(a,1),67(a,1,2,2,2)),flip(a)].

1506 (B' * x) * (B' * x) = B' * (x' * (B * x'))'. [para(1118(a,1),127(a,1,1)),rewrite([931(6),69(7),941(8)]),flip(a)].

1531 (x * (y * x))' = x' / (x * y). [para(164(a,1),88(a,1,1))].

1547 (B * x) * B = B * (x * B). [para(164(a,1),297(a,1)),flip(a)].

1579 (B' * x) * (B' * x) = B' * (x / (x' * B)). [back_rewrite(1506),rewrite([1531(15),26(11)])].

1668 x / (x' * y) = x * (y' * x). [para(37(a,1),166(a,1,2,1,1)),flip(a)].

1746 (B' * x) * (B' * x) = B' * (x * (B' * x)). [back_rewrite(1579),rewrite([1668(13)])].

2772 (x * B') * (B * x) = x * x. [para(307(a,1),12(a,1,2)),rewrite([26(2)]),flip(a)].

2796 (x * x) / (B * x) = x * B'. [para(2772(a,1),10(a,1,1))].

3050 (B' * x) * B' = B' * (x * B'). [para(37(a,1),2796(a,1,2)),rewrite([1746(7),43(8)]),flip(a)].

5123 ((A * B) * x') * x = A * B. [para(848(a,1),14(a,2,2)),rewrite([343(10)])].

5127 (A * B) / x = (A * B) * x'. [para(848(a,1),43(a,1,1,2)),rewrite([343(14)])].

6913 x * ((B * ((B' * A) * x')) * x) = (x * B) * (B' * A). [para(1046(a,1),84(a,1,2,2)),rewrite([300(19)]),flip(a)].

9920 (A * x) * ((y * A') * (A * x)) = ((A * x) * y) / x'. [para(195(a,1),168(a,1,2,1,2)),rewrite([233(4)])].

16009 (x * A') * (A * y) = A' * ((A * x) * y). [para(233(a,1),214(a,1,1))].

16017 (x * B) * (B' * y) = B * ((B' * x) * y). [para(297(a,1),214(a,1,1)),rewrite([26(9)])].

16174 ((A * B) * x') * (x * y) = x' * ((x * (A * B)) * y). [para(5127(a,1),214(a,1,1))].

16404 A * ((x * A') * ((A * y) * x)) = ((A * x) * y) / x'. [back_rewrite(9920),rewrite([16009(8),222(9),233(3)])].

16449 x * ((B * ((B' * A) * x')) * x) = B * ((B' * x) * A). [back_rewrite(6913),rewrite([16017(17)])].

20169 (x * (A * B)) * B' = B * ((B' * x) * A). [para(5123(a,1),269(a,1,1,2)),rewrite([980(13),16017(15),16449(17)])].

22598 B * (((B' * x) * A) * B) = x * (A * B). [para(5123(a,1),317(a,2,2)),rewrite([16174(9),20169(8),37(10),1547(9)])].

23287 (x * A') * ((A * y) * x) = x * (y * x). [para(11(a,1),327(a,1,1)),rewrite([233(2),271(5),233(4),233(9),271(12)]),flip(a)].

23341 ((A * x) * y) / x' = A * (x * (y * x)). [back_rewrite(16404),rewrite([23287(8)]),flip(a)].

33745 ((B' * x) * A) * B = B' * (x * (A * B)). [para(22598(a,1),12(a,1,2)),flip(a)].

33754 ((B' * x) * A) * (B * y) = B' * ((x * (A * B)) * y). [para(22598(a,1),214(a,2,2,1)),rewrite([33745(7),232(9),3050(10),20169(9),12(10)]

)].

33913 (A * (x * (y * x))) * (x' * z) = x * ((x' * ((A * x) * y)) * z). [para(23341(a,1),214(a,1,1)),rewrite([26(9)])].

48357 (x * (A * B)) * (y * x) = x * (((A * B) * y) * x). [para(1396(a,1),16017(a,2,2)),rewrite([26(8),26(9),33913(14),12(15),18(11),37(9),26

(15),33754(16),37(17)]),flip(a)].

48358 $F. [resolve(48357,a,19,a)].

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

% Proof 1 at 635.17 (+ 4.28) seconds.

% Length of proof is 88.

% Level of proof is 18.

% Maximum clause weight is 27.000.

% Given clauses 7837.

1 z * (((A \ B) * y) * z) = (z * (A \ B)) * (y * z) # label(non_clause) # label(goal). [goal].

3 0 * x = x. [assumption].

4 x * 0 = x. [assumption].

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

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

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

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

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

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

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

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

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

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

16 x * ((B * y) * x) = (x * B) * (y * x). [assumption].

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

18 x * (((A * B) * y) * x) = (x * (A * B)) * (y * x). [assumption].

19 (x * (A * B)) * (y * x) = x * (((A * B) * y) * x) # label(non_clause) # label(goal). [copy(18),flip(a)].

20 (c1 * (A \ B)) * (c2 * c1) != c1 * (((A \ B) * c2) * c1). [deny(1)].

25 x \ 0 = x'. [para(5(a,1),8(a,1,2))].

26 x'' = x. [para(6(a,1),8(a,1,2)),rewrite([25(3)])].

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

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

36 (c1 * (A' * B)) * (c2 * c1) != c1 * (((A' * B) * c2) * c1). [back_rewrite(20),rewrite([33(4),33(14)])].

37 x * (x' * y) = y. [back_rewrite(7),rewrite([33(1)])].

43 (x * (y * (x * z))) / z = x * (y * x). [para(13(a,1),9(a,1,1))].

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

54 A' * ((A * x) * A') = x * A'. [para(6(a,1),15(a,1,1)),rewrite([3(5)]),flip(a)].

55 x * ((A * x') * x) = x * A. [para(6(a,1),15(a,1,2)),rewrite([4(4)]),flip(a)].

71 B' * ((B * x) * B') = x * B'. [para(6(a,1),17(a,1,1)),rewrite([3(5)]),flip(a)].

72 x * ((B * x') * x) = x * B. [para(6(a,1),17(a,1,2)),rewrite([4(4)]),flip(a)].

84 (x * B) * (y * (z * (y * x))) = x * ((B * (y * (z * y))) * x). [para(13(a,1),17(a,1,2))].

95 (x * (A * B))' * (x * (((A * B) * y) * x)) = y * x. [para(19(a,1),11(a,1,2))].

155 (A * x') * x = A. [para(55(a,1),11(a,1,2)),rewrite([11(4)]),flip(a)].

157 (A * x) * x' = A. [para(55(a,1),37(a,1,2)),rewrite([37(4),26(4)]),flip(a)].

177 (A * x)' = x' / A. [para(157(a,1),34(a,1,2)),flip(a)].

178 x * (A' * x)' = A. [para(37(a,1),157(a,1,1))].

190 (B * x') * x = B. [para(72(a,1),11(a,1,2)),rewrite([11(4)]),flip(a)].

194 (B * x) * x' = B. [para(72(a,1),37(a,1,2)),rewrite([37(4),26(4)]),flip(a)].

197 B / x = B * x'. [para(190(a,1),9(a,1,1))].

207 (B * (x' / A)) * (A * x) = B. [para(177(a,1),190(a,1,1,2))].

215 x * (B' * x)' = B. [para(37(a,1),194(a,1,1))].

218 B * (x * B)' = x'. [para(197(a,1),34(a,1))].

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

221 (x * B)' = B' * x'. [para(218(a,1),11(a,1,2)),flip(a)].

235 (A * (x' * B)) * (B' * x) = A. [para(219(a,1),155(a,1,1,2))].

277 (x * A) * A' = x. [para(13(a,1),54(a,1,2)),rewrite([5(7),4(5),11(5)]),flip(a)].

281 x / A' = x * A. [para(277(a,1),9(a,1,1))].

282 x / A = x * A'. [para(10(a,1),277(a,1,1)),flip(a)].

287 A' * ((B * (x * A)) * A') = (A' * B) * x. [para(277(a,1),17(a,1,2)),flip(a)].

288 (x * A)' = A' / x. [para(277(a,1),34(a,1,2)),flip(a)].

293 (B * (x' * A')) * (A * x) = B. [back_rewrite(207),rewrite([282(4)])].

309 (x * A') * A = x. [para(281(a,1),9(a,1))].

314 A * ((B * (x * A')) * A) = (A * B) * x. [para(309(a,1),17(a,1,2)),flip(a)].

319 ((A * B) * x') * x = A * B. [para(293(a,1),13(a,2,2)),rewrite([314(10)])].

328 (A * B) / x = (A * B) * x'. [para(319(a,1),9(a,1,1))].

342 (A * B) * (x * (A * B))' = x'. [para(328(a,1),34(a,1))].

347 (x * B) * B' = x. [para(13(a,1),71(a,1,2)),rewrite([5(7),4(5),11(5)]),flip(a)].

351 x / B' = x * B. [para(347(a,1),9(a,1,1))].

352 x / B = x * B'. [para(10(a,1),347(a,1,1)),flip(a)].

357 B' * ((A * (x * B)) * B') = (B' * A) * x. [para(347(a,1),15(a,1,2)),flip(a)].

400 x * ((x * y)' * x) = x / y. [para(6(a,1),43(a,1,1,2)),rewrite([4(2)]),flip(a)].

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

410 ((x * B) * (y * (x * ((B * z) * x)))) / (z * x) = (x * B) * (y * (x * B)). [para(17(a,1),43(a,1,1,2,2))].

430 (x * B) * (y * (x * B)) = x * ((B * y) * (x * B)). [para(347(a,1),43(a,1,1,2,2)),rewrite([17(4),351(7),13(6)]),flip(a)].

438 ((x * B) * (y * (x * ((B * z) * x)))) / (z * x) = x * ((B * y) * (x * B)). [back_rewrite(410),rewrite([430(16)])].

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

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

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

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

793 ((A * B) * x') * (x * y) = x' * ((x * (A * B)) * y). [para(328(a,1),546(a,1,1))].

794 (B' * x') * (((x * B) * y) * B') = x' * ((x * y) * B'). [para(347(a,1),546(a,1,2)),rewrite([654(4),352(4),221(9)]),flip(a)].

796 (x * B) * (B' * y) = B * ((B' * x) * y). [para(351(a,1),546(a,1,1)),rewrite([26(9)])].

991 (A * (x * B)) * B' = B * ((B' * A) * x). [para(357(a,1),11(a,1,2)),rewrite([26(3)]),flip(a)].

1177 (B * ((B' * A) * x')) * x = x' * ((x * (A * B)) * B'). [para(347(a,1),793(a,1,2)),rewrite([221(6),796(8),221(12),794(23)])].

1311 (x * (A * B)) * B' = B * ((B' * x) * A). [para(235(a,1),84(a,1,2,2)),rewrite([796(7),991(18),11(19),1177(16),37(17)]),flip(a)].

1353 (x * (A * B))' = (B' * A') / x. [para(1311(a,1),34(a,1,2)),rewrite([505(10),288(8),654(11),26(5),11(11)]),flip(a)].

1374 (A * B) * ((B' * A') / x) = x'. [back_rewrite(342),rewrite([1353(8)])].

1377 x' * ((x * (B' * A')) * (((A * B) * y) * x)) = y * x. [back_rewrite(95),rewrite([1353(5),546(13)])].

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

2112 (B * (x' * A)) * (A' * x) = B. [para(1681(a,1),190(a,1,1,2))].

7107 ((A' * B) * x') * x = A' * B. [para(2112(a,1),13(a,2,2)),rewrite([287(11)])].

12111 (B' * A') / x = (B' * A') * x'. [para(1374(a,1),11(a,1,2)),rewrite([221(4)]),flip(a)].

13537 (B * ((B' * A') * x')) * (x * B) = A' * B. [para(221(a,1),7107(a,1,1,2)),rewrite([796(9)])].

31919 ((B' * A') * x') * (x * y) = x' * ((x * (B' * A')) * y). [para(12111(a,1),546(a,1,1))].

51009 x' * ((x * (B' * A')) * (y * x)) = ((B' * A') * y) * x. [para(37(a,1),1377(a,1,2,2,1)),rewrite([221(14)])].

57200 (x * (((A' * B) * y) * x)) / (y * x) = x * (A' * B). [para(13537(a,1),438(a,2,2)),rewrite([31919(14),51009(14),547(10),351(9),17(12),3

7(10)])].

70990 (x * (A' * B)) * (y * x) = x * (((A' * B) * y) * x). [para(57200(a,1),10(a,1,1))].

70991 $F. [resolve(70990,a,36,a)].

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

% Proof 2 at 706.08 (+ 4.72) seconds.

% Length of proof is 182.

% Level of proof is 26.

% Maximum clause weight is 27.000.

% Given clauses 8334.

2 z * (((A / B) * y) * z) = (z * (A / B)) * (y * z) # label(non_clause) # label(goal). [goal].

3 0 * x = x. [assumption].

4 x * 0 = x. [assumption].

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

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

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

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

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

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

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

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

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

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

16 x * ((B * y) * x) = (x * B) * (y * x). [assumption].

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

21 (c3 * (A / B)) * (c4 * c3) != c3 * (((A / B) * c4) * c3). [deny(2)].

25 x \ 0 = x'. [para(5(a,1),8(a,1,2))].

26 x'' = x. [para(6(a,1),8(a,1,2)),rewrite([25(3)])].

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

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

37 x * (x' * y) = y. [back_rewrite(7),rewrite([33(1)])].

43 (x * (y * (x * z))) / z = x * (y * x). [para(13(a,1),9(a,1,1))].

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

54 A' * ((A * x) * A') = x * A'. [para(6(a,1),15(a,1,1)),rewrite([3(5)]),flip(a)].

55 x * ((A * x') * x) = x * A. [para(6(a,1),15(a,1,2)),rewrite([4(4)]),flip(a)].

60 (x * y) * ((A * x') * (x * y)) = ((x * y) * A) * y. [para(11(a,1),15(a,1,2)),flip(a)].

67 (x * A) * (y * (z * (y * x))) = x * ((A * (y * (z * y))) * x). [para(13(a,1),15(a,1,2))].

69 (x * B) * x = x * (B * x). [para(3(a,1),17(a,1,2)),rewrite([4(6)])].

71 B' * ((B * x) * B') = x * B'. [para(6(a,1),17(a,1,1)),rewrite([3(5)]),flip(a)].

72 x * ((B * x') * x) = x * B. [para(6(a,1),17(a,1,2)),rewrite([4(4)]),flip(a)].

75 x * ((B * (y / x)) * x) = (x * B) * y. [para(10(a,1),17(a,1,2)),flip(a)].

84 (x * B) * (y * (z * (y * x))) = x * ((B * (y * (z * y))) * x). [para(13(a,1),17(a,1,2))].

113 (x / y)' = y / x. [para(10(a,1),34(a,1,2)),flip(a)].

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

155 (A * x') * x = A. [para(55(a,1),11(a,1,2)),rewrite([11(4)]),flip(a)].

157 (A * x) * x' = A. [para(55(a,1),37(a,1,2)),rewrite([37(4),26(4)]),flip(a)].

159 A / x = A * x'. [para(155(a,1),9(a,1,1))].

170 (c3 * (A * B')) * (c4 * c3) != c3 * (((A * B') * c4) * c3). [back_rewrite(21),rewrite([159(4),159(14)])].

177 (A * x)' = x' / A. [para(157(a,1),34(a,1,2)),flip(a)].

178 x * (A' * x)' = A. [para(37(a,1),157(a,1,1))].

186 (A' * x)' / A = x'. [para(37(a,1),177(a,1,1)),flip(a)].

190 (B * x') * x = B. [para(72(a,1),11(a,1,2)),rewrite([11(4)]),flip(a)].

194 (B * x) * x' = B. [para(72(a,1),37(a,1,2)),rewrite([37(4),26(4)]),flip(a)].

197 B / x = B * x'. [para(190(a,1),9(a,1,1))].

207 (B * (x' / A)) * (A * x) = B. [para(177(a,1),190(a,1,1,2))].

209 x' * ((B * x) * (x' * y)) = (x' * B) * y. [para(194(a,1),13(a,1,1,2)),flip(a)].

214 (B * x)' = x' / B. [para(194(a,1),34(a,1,2)),flip(a)].

215 x * (B' * x)' = B. [para(37(a,1),194(a,1,1))].

218 B * (x * B)' = x'. [para(197(a,1),34(a,1))].

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

221 (x * B)' = B' * x'. [para(218(a,1),11(a,1,2)),flip(a)].

235 (A * (x' * B)) * (B' * x) = A. [para(219(a,1),155(a,1,1,2))].

277 (x * A) * A' = x. [para(13(a,1),54(a,1,2)),rewrite([5(7),4(5),11(5)]),flip(a)].

281 x / A' = x * A. [para(277(a,1),9(a,1,1))].

282 x / A = x * A'. [para(10(a,1),277(a,1,1)),flip(a)].

288 (x * A)' = A' / x. [para(277(a,1),34(a,1,2)),flip(a)].

293 (B * (x' * A')) * (A * x) = B. [back_rewrite(207),rewrite([282(4)])].

296 (A' * x)' * A' = x'. [back_rewrite(186),rewrite([282(6)])].

301 (A * x)' = x' * A'. [back_rewrite(177),rewrite([282(6)])].

309 (x * A') * A = x. [para(281(a,1),9(a,1))].

311 (x * A')' = A * x'. [para(282(a,1),113(a,1,1)),rewrite([159(6)])].

314 A * ((B * (x * A')) * A) = (A * B) * x. [para(309(a,1),17(a,1,2)),flip(a)].

319 ((A * B) * x') * x = A * B. [para(293(a,1),13(a,2,2)),rewrite([314(10)])].

328 (A * B) / x = (A * B) * x'. [para(319(a,1),9(a,1,1))].

342 (A * B) * (x * (A * B))' = x'. [para(328(a,1),34(a,1))].

347 (x * B) * B' = x. [para(13(a,1),71(a,1,2)),rewrite([5(7),4(5),11(5)]),flip(a)].

350 (B' * x) * B' = B' * (x * B'). [para(37(a,1),71(a,1,2,1)),flip(a)].

351 x / B' = x * B. [para(347(a,1),9(a,1,1))].

352 x / B = x * B'. [para(10(a,1),347(a,1,1)),flip(a)].

353 (B' * x') * x = B'. [para(347(a,1),11(a,1,2)),rewrite([221(3)])].

357 B' * ((A * (x * B)) * B') = (B' * A) * x. [para(347(a,1),15(a,1,2)),flip(a)].

359 B' / x = B' * x'. [para(347(a,1),34(a,1,2)),rewrite([221(6)])].

362 (B * x)' = x' * B'. [back_rewrite(214),rewrite([352(6)])].

369 (x * B') * B = x. [para(351(a,1),9(a,1))].

371 (x * B')' = B * x'. [para(352(a,1),113(a,1,1)),rewrite([197(6)])].

373 (x * (y * (x * B'))) * B = x * (y * x). [para(13(a,1),369(a,1,1))].

378 x * ((A * (B' * x')) * x) = (x * A) * B'. [para(353(a,1),15(a,1,2)),flip(a)].

398 (x * y) / x' = x * (y * x). [para(5(a,1),43(a,1,1,2,2)),rewrite([4(2)])].

399 (x' * y) / x = x' * (y * x'). [para(6(a,1),43(a,1,1,2,2)),rewrite([4(3)])].

400 x * ((x * y)' * x) = x / y. [para(6(a,1),43(a,1,1,2)),rewrite([4(2)]),flip(a)].

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

421 x * ((B * (x * y)') * x) = (x * B) / y. [para(190(a,1),43(a,1,1,2)),flip(a)].

425 (x * A) * (y * (x * A)) = x * ((A * y) * (x * A)). [para(277(a,1),43(a,1,1,2,2)),rewrite([15(4),281(7),13(6)]),flip(a)].

430 (x * B) * (y * (x * B)) = x * ((B * y) * (x * B)). [para(347(a,1),43(a,1,1,2,2)),rewrite([17(4),351(7),13(6)]),flip(a)].

450 (x * (y * x))' = x' / (x * y). [para(398(a,1),113(a,1,1))].

466 x / (B' * x') = x * (x * B). [para(347(a,1),398(a,1,1)),rewrite([221(3),430(13),5(9),3(9)])].

479 x / (y * (z * (y * x))) = y' / (y * z). [back_rewrite(115),rewrite([450(7)])].

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

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

514 (x * B) / x = (x * B) * x'. [para(69(a,1),400(a,1,2,1,1)),rewrite([450(6),505(6),13(11),11(9),6(7),4(5)]),flip(a)].

525 A * (A' / x) = x'. [back_rewrite(296),rewrite([504(7),26(3)])].

526 x / (y * (z * (y * x))) = y' * (z' * y'). [back_rewrite(479),rewrite([505(7)])].

531 (x * (y * x))' = x' * (y' * x'). [back_rewrite(450),rewrite([505(6)])].

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

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

557 (x * y) * (x' * z) = x * ((y / x) * z). [para(37(a,1),44(a,1,2,2)),flip(a)].

593 (x * B) / x = x * (B * x'). [back_rewrite(514),rewrite([542(7),197(5)])].

634 (x * B') * (B * (B * x')) = x * (B * x'). [para(369(a,1),542(a,1,1)),rewrite([371(4),197(12),371(12)]),flip(a)].

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

657 x * ((y / (x * z)) * (x * u)) = ((x * y) / z) * u. [para(402(a,1),13(a,1,1)),flip(a)].

667 (A * x) * ((y * A') * (A * x)) = ((A * x) * y) / x'. [para(157(a,1),402(a,1,2,1,2)),rewrite([282(4)])].

671 (B * x) * ((y * B') * (B * x)) = ((B * x) * y) / x'. [para(194(a,1),402(a,1,2,1,2)),rewrite([352(4)])].

786 (x * A') * (A * y) = A' * ((A * x) * y). [para(282(a,1),546(a,1,1))].

793 ((A * B) * x') * (x * y) = x' * ((x * (A * B)) * y). [para(328(a,1),546(a,1,1))].

794 (B' * x') * (((x * B) * y) * B') = x' * ((x * y) * B'). [para(347(a,1),546(a,1,2)),rewrite([654(4),352(4),221(9)]),flip(a)].

796 (x * B) * (B' * y) = B * ((B' * x) * y). [para(351(a,1),546(a,1,1)),rewrite([26(9)])].

797 (x * B') * (B * y) = B' * ((B * x) * y). [para(352(a,1),546(a,1,1))].

824 A * ((x * A') * ((A * y) * x)) = ((A * x) * y) / x'. [back_rewrite(667),rewrite([786(8),557(9),282(3)])].

840 B * ((x * B') * ((B * y) * x)) = ((B * x) * y) / x'. [back_rewrite(671),rewrite([797(8),557(9),352(3)])].

841 B' * ((B * x) * (B * x')) = x * (B * x'). [back_rewrite(634),rewrite([797(9)])].

991 (A * (x * B)) * B' = B * ((B' * A) * x). [para(357(a,1),11(a,1,2)),rewrite([26(3)]),flip(a)].

1005 (x * A') * ((A * y) * x) = x * (y * x). [para(10(a,1),425(a,1,1)),rewrite([282(2),309(5),282(4),282(9),309(12)]),flip(a)].

1046 ((A * x) * y) / x' = A * (x * (y * x)). [back_rewrite(824),rewrite([1005(8)]),flip(a)].

1082 B * ((x * (A * B')) * B) = (B * x) * A. [para(373(a,1),1005(a,1,2)),rewrite([786(9),17(8),11(9)]),flip(a)].

1133 (A * (x * (y * x))) * (x' * z) = x * ((x' * ((A * x) * y)) * z). [para(1046(a,1),546(a,1,1)),rewrite([26(9)])].

1177 (B * ((B' * A) * x')) * x = x' * ((x * (A * B)) * B'). [para(347(a,1),793(a,1,2)),rewrite([221(6),796(8),221(12),794(23)])].

1250 (x * (y * ((A * (x * (z * x))) * y))) / (z * (x * y)) = x * ((y * A) * x). [para(67(a,1),43(a,1,1,2))].

1311 (x * (A * B)) * B' = B * ((B' * x) * A). [para(235(a,1),84(a,1,2,2)),rewrite([796(7),991(18),11(19),1177(16),37(17)]),flip(a)].

1353 (x * (A * B))' = (B' * A') / x. [para(1311(a,1),34(a,1,2)),rewrite([505(10),288(8),654(11),26(5),11(11)]),flip(a)].

1374 (A * B) * ((B' * A') / x) = x'. [back_rewrite(342),rewrite([1353(8)])].

1457 (A * x') * (x * y) = x' * ((x * A) * y). [para(5(a,1),1133(a,1,1,2,2)),rewrite([4(4),26(5),26(8),155(10)])].

1483 (A * (x' * (y * x'))) * (x * z) = x' * ((x * ((A * x') * y)) * z). [para(26(a,1),1133(a,1,2,1)),rewrite([26(11)])].

1551 x * ((y / x) * ((x * A) * y)) = ((x * y) * A) * y. [back_rewrite(60),rewrite([1457(6),557(7)])].

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

1825 A' / x = A' * x'. [para(525(a,1),11(a,1,2)),flip(a)].

1894 (x * A)' = A' * x'. [back_rewrite(288),rewrite([1825(6)])].

1919 (B' * (x' * A')) * (A * x) = B'. [para(301(a,1),353(a,1,1,2))].

2071 (x' * B') * ((B * x) * y) = y. [para(362(a,1),11(a,1,1))].

2072 (B * x) * ((x' * B') * y) = y. [para(362(a,1),37(a,1,2,1))].

2154 (A' * x') * x = A'. [para(1825(a,1),10(a,1,1))].

2165 (A' * (x / y)) * (y / x) = A'. [para(113(a,1),2154(a,1,1,2))].

2819 x / (x * B') = x * (B * x'). [para(10(a,1),593(a,1,1)),rewrite([352(2),352(6),352(10),371(12),797(13),841(13)])].

2822 (x * (B * x'))' = x / (x * B). [para(593(a,1),113(a,1,1))].

3747 (B * (x / y)) * y = y' * ((y * B) * x). [para(75(a,1),11(a,1,2)),flip(a)].

4040 (x * B') * x = x * (B' * x). [para(10(a,1),466(a,2,2)),rewrite([352(2),352(7),371(9),11(9),398(5),352(6)]),flip(a)].

6002 ((x' * A) * B') * ((B * (A' * x)) * y) = y. [para(1681(a,1),2071(a,1,1,1))].

6033 (B * (A' * x)) * (((x' * A) * B') * y) = y. [para(1681(a,1),2072(a,1,2,1,1))].

7213 (A' * (x / (x * B))) * (x * (B * x')) = A'. [para(593(a,1),2165(a,1,2))].

7473 (x * B') / x = x / (x * B). [para(2819(a,1),113(a,1,1)),rewrite([2822(5)]),flip(a)].

7502 (B * x') * (x / (x * B)) = x'. [para(7473(a,1),504(a,2,2)),rewrite([4040(4),531(5),26(4),13(9),11(7),5(5),4(3),371(5)]),flip(a)].

9753 x / (x * B) = x * (B' * x'). [para(7502(a,1),11(a,1,2)),rewrite([362(4),26(2),542(5),359(3)]),flip(a)].

9900 (A' * (x * (B' * x'))) * (x * (B * x')) = A'. [back_rewrite(7213),rewrite([9753(5)])].

10602 (x * (B' * x'))' = x * (B * x'). [para(9753(a,1),113(a,1,1)),rewrite([593(9)])].

12010 (B' * A') / (x * A') = (B' * (x' * A')) * A. [para(546(a,1),1353(a,1,1)),rewrite([1681(8),221(5),301(5),282(16)]),flip(a)].

12111 (B' * A') / x = (B' * A') * x'. [para(1374(a,1),11(a,1,2)),rewrite([221(4)]),flip(a)].

12216 (B' * (x' * A')) * A = A' * ((A * B') * x'). [back_rewrite(12010),rewrite([12111(9),311(9),786(9)]),flip(a)].

14082 (B * x) * (x' * y) = x * ((x' * B) * y). [para(209(a,1),11(a,1,2)),rewrite([26(2)]),flip(a)].

16953 ((A * B') * x') * x = A * B'. [para(1919(a,1),13(a,2,2)),rewrite([12216(10),37(11)])].

17084 ((A * B') * x) * x' = A * B'. [para(26(a,1),16953(a,1,1,2))].

17196 x * ((B * A') * x)' = A * B'. [para(37(a,1),17084(a,1,1)),rewrite([371(5)])].

17232 ((B * A') * x)' = x' * (A * B'). [para(17196(a,1),11(a,1,2)),flip(a)].

19927 ((B * x) * ((A * B') * x')) / x' = ((B * x) * A) * B'. [para(362(a,1),378(a,1,2,1,2,2)),rewrite([1483(14),557(15),352(3),840(15)])].

23648 (B * (x * y)') * x = x' * ((x * B) / y). [para(421(a,1),11(a,1,2)),flip(a)].

24697 (x * B') * ((B * y) * x) = x * (y * x). [para(10(a,1),430(a,1,1)),rewrite([352(2),369(5),352(4),352(9),369(12)]),flip(a)].

24760 ((B * x) * y) / x' = B * (x * (y * x)). [back_rewrite(840),rewrite([24697(8)]),flip(a)].

24775 ((B * x) * A) * B' = B * (x * (A * B')). [back_rewrite(19927),rewrite([24760(11),16953(8)]),flip(a)].

24940 (x' * (A * B')) * (B * A') = (A * B') * ((B * A') / x). [para(17232(a,1),504(a,1,1)),rewrite([311(16)])].

27697 (x * (A * B')) * B = B' * ((B * x) * A). [para(1082(a,1),11(a,1,2)),flip(a)].

27703 (x * (A * B')) * (B * y) = B' * (((B * x) * A) * y). [para(1082(a,1),546(a,2,2,1)),rewrite([27697(7),352(9),350(10),24775(9),11(10)])]

.

27746 (A * B') * ((B * A') / x) = x'. [back_rewrite(24940),rewrite([27703(11),277(10),11(6)]),flip(a)].

27783 (B * A') / x = (B * A') * x'. [para(27746(a,1),11(a,1,2)),rewrite([371(5)]),flip(a)].

27867 x / (B * A') = x * (A * B'). [para(27783(a,1),113(a,1,1)),rewrite([17232(7),26(2)]),flip(a)].

29776 x' * (((x * B) * y) * x') = B * (y / x). [para(3747(a,1),9(a,1,1)),rewrite([399(6)])].

33892 ((x * y) / z) * x' = x * (y / (x * z)). [para(5(a,1),657(a,1,2,2)),rewrite([4(4)]),flip(a)].

33897 (x / (y * z)) * (y * u) = y' * (((y * x) / z) * u). [para(657(a,1),11(a,1,2)),flip(a)].

34211 (x * B') * (y * x) = x * ((B' * y) * x). [para(37(a,1),24697(a,1,2,1))].

36867 ((x * y) * A) * x' = x * (y / (x * A')). [para(281(a,1),33892(a,1,1))].

40970 ((x * y) * B') * (x' * ((x * B) / y)) = x. [para(23648(a,1),11(a,1,2)),rewrite([362(5),26(3)])].

42089 ((x * B) * y) * x' = x * (B * (y / x)). [para(29776(a,1),11(a,1,2)),rewrite([26(2)]),flip(a)].

46265 (B * (A' * x)) * x' = x * ((x' * B) * A'). [para(40970(a,1),6033(a,1,2)),rewrite([26(9),282(12)])].

54354 x * ((B * x') / (x * A')) = x * ((B * x') * (A * x')). [para(42089(a,1),1551(a,1,2,2)),rewrite([505(6),159(11),13(15),11(13),11(11),55

7(8),197(2),542(12),197(10),36867(16)]),flip(a)].

61345 (B * x') / (x * A') = (B * x') * (A * x'). [para(9900(a,1),526(a,1,2,2)),rewrite([1681(17),10602(14),36867(16),54354(16),11(17)])].

61353 (B * x) / (x' * A') = (B * x) * (A * x). [para(26(a,1),61345(a,1,1,2)),rewrite([26(10),26(12)])].

61361 (B * (A' * x)) / x' = (B * (A' * x)) * x. [para(504(a,1),61345(a,1,2)),rewrite([1681(5),1894(5),26(5),26(8),1825(9),37(11),1681(12),18

94(12),26(12),1681(17),1894(17),26(17),37(17)])].

61384 (x * ((x' * B) * A'))' * (B * x) = A * x. [para(61353(a,1),504(a,2,2)),rewrite([14082(7),362(14),2071(21)])].

61411 (x * ((x' * B) * A'))' * (B * (A' * x)) = x. [para(61361(a,1),504(a,2,2)),rewrite([46265(7),362(20),1681(18),6002(27)])].

61439 (x * ((x' * B) * A'))' = (A * x) / (B * x). [para(61384(a,1),9(a,1,1)),flip(a)].

61448 B' * (((B * (A * x)) / x) * (A' * x)) = x. [back_rewrite(61411),rewrite([61439(8),33897(11)])].

61509 ((B * (A * x)) / x) * (A' * x) = B * x. [para(61448(a,1),11(a,1,2)),rewrite([26(3)]),flip(a)].

61513 (x * (((A * B') * y) * x)) / (y * x) = x * (A * B'). [para(61448(a,1),1250(a,1,2,2)),rewrite([61509(11),61509(21),1483(15),557(16),352

(5),34211(15),11(13),11(12),61509(20),36867(18),27867(17),11(19)])].

71515 (x * (A * B')) * (y * x) = x * (((A * B') * y) * x). [para(61513(a,1),10(a,1,1))].

71516 $F. [resolve(71515,a,170,a)].

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