% Proof 1 at 38.26 (+ 0.22) seconds.
% Length of proof is 125.
% Level of proof is 25.
% Maximum clause weight is 27.000.
% Given clauses 1209.
2 A * ((x * y) * A) = (A * x) * (y * A) #
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].
12 (x * x) * y = x * (x * y). [assumption].
13 (x * (y * x)) * z = x * (y * (x * z)). [assumption].
14 (x * y)' = x' * y'. [assumption].
15 (x * (y * A)) * x = (x * y) * (A * x). [assumption].
17 (A * c3) * (c4 * A) != A * ((c3 * c4) *
A). [deny(2)].
21 x \ 0 = x'. [para(5(a,1),8(a,1,2))].
22 x'' = x.
[para(6(a,1),8(a,1,2)),rewrite([21(3)])].
29 x \ y = x' * y. [para(7(a,1),11(a,1,2)),flip(a)].
30 x / (y * x) = y'. [para(11(a,1),9(a,1,1))].
32 x * (x' * y) = y. [back_rewrite(7),rewrite([29(1)])].
33 (x * (x * y)) / y = x * x. [para(12(a,1),9(a,1,1))].
36 (x * (y * (x * z))) / z = x * (y * x). [para(13(a,1),9(a,1,1))].
37 x * ((y / x) * (x * z)) = (x * y) * z. [para(10(a,1),13(a,1,1,2)),flip(a)].
40 (x * (y * (y * x))) * z = x * (y * (y * (x *
z))).
[para(12(a,1),13(a,1,1,2)),rewrite([12(7)])].
46 (x / y)' * y' = x'. [para(10(a,1),14(a,1,1)),flip(a)].
48 (x * A) * x = x * (A * x).
[para(3(a,1),15(a,1,1,2)),rewrite([4(5)])].
49 (x * A') * (A * x) = x * x. [para(6(a,1),15(a,1,1,2)),rewrite([4(2)]),flip(a)].
51 ((x * y) * (A * x)) / x = x * (y * A). [para(15(a,1),9(a,1,1))].
54 (x' * (y' * A')) * ((x * y) * (A * x)) =
x.
[para(15(a,1),11(a,1,2)),rewrite([14(4),14(4)])].
59 (A * x) * (A * A) = A * (x * (A * A)). [para(15(a,1),13(a,1))].
64 (x / y)' = y / x. [para(10(a,1),30(a,1,2)),flip(a)].
68 (x / y) * x' = y'. [back_rewrite(46),rewrite([64(2)])].
73 x' / y' = y / x. [para(68(a,1),9(a,1,1))].
76 (x' / y) * x = y'. [para(22(a,1),68(a,1,2))].
85 (x * y) / (x' * y) = x * x. [para(32(a,1),33(a,1,1,2))].
91 (x' * y') / z' = z / (x * y). [para(14(a,1),73(a,1,1))].
93 x / y' = y / x'. [para(22(a,1),73(a,1,1))].
95 (x / y) / z' = z / (y / x). [para(64(a,1),73(a,1,1))].
107 (x' * y) / x = x' * (y * x').
[para(6(a,1),36(a,1,1,2,2)),rewrite([4(3)])].
110 x * ((y / (x * z)) * x) = (x * y) / z. [para(10(a,1),36(a,1,1,2)),flip(a)].
139 (x * y) * x' = x * (y / x).
[para(5(a,1),37(a,1,2,2)),rewrite([4(3)]),flip(a)].
140 (x' * y) * x = x' * (y / x').
[para(6(a,1),37(a,1,2,2)),rewrite([4(5)]),flip(a)].
143 (x / y) * (y * z) = y' * ((y * x) * z). [para(37(a,1),11(a,1,2)),flip(a)].
144 (x' * y) * (x * z) = x' * ((y / x') *
z).
[para(11(a,1),37(a,1,2,2)),flip(a)].
148 x' * ((x / ((x' * y') * (x / y))) * z) = (y /
x) * ((x * y) * z).
[para(37(a,1),13(a,2,2)),rewrite([143(4),144(7),93(6),14(5),14(3),64(6
)])].
151 (x * y) * (x' * z) = x * ((y / x) * z). [para(32(a,1),37(a,1,2,2)),flip(a)].
160 (x * (A * x)) / x = x * A. [para(48(a,1),9(a,1,1))].
230 (x * x) / (A * x) = x * A'. [para(49(a,1),9(a,1,1))].
238 (A * x) / (x * x) = x' * A.
[para(49(a,1),30(a,1,2)),rewrite([14(8),22(8)])].
249 (x * (y * (z * (z * (y * x))))) * u = x * (y
* (z * (z * (y * (x * u))))).
[para(40(a,1),13(a,1,1,2)),rewrite([40(11)])].
386 (x * A) * (x / (x * A)) = x. [para(48(a,1),139(a,1,1)),rewrite([14(6),151(8),9(3),5(4),4(2)]),flip(a)].
402 x * ((x / A) / x) = x / A.
[para(10(a,1),386(a,1,1)),rewrite([10(6)])].
403 x / (x * A) = x' * (A' / x').
[para(386(a,1),11(a,1,2)),rewrite([14(3),140(5)]),flip(a)].
407 x' * (x / (x / A')) = A' / x.
[para(76(a,1),386(a,1,1)),rewrite([76(9),93(6),64(5)])].
422 x / (A / x') = x * (x' / A).
[para(402(a,1),32(a,1,2)),rewrite([93(9),64(8)]),flip(a)].
472 x * (x * (A / x)) = x * A.
[para(238(a,1),139(a,2,2)),rewrite([12(4),14(6),151(8),160(4),139(4),12(9),32(8)])].
475 x * (A / x) = A. [para(472(a,1),11(a,1,2)),rewrite([11(4)]),flip(a)].
487 A / x = x' * A. [para(475(a,1),11(a,1,2)),flip(a)].
497 x' * (A' / x') = x * (x' / A).
[back_rewrite(422),rewrite([487(3),22(2),403(3)])].
507 x / (x * A) = x * (x' / A). [back_rewrite(403),rewrite([497(9)])].
511 x / A = x * A'. [para(487(a,1),64(a,1,1)),rewrite([14(4),22(2)]),flip(a)].
515 x / A' = x * A. [para(487(a,1),93(a,1)),rewrite([22(2)]),flip(a)].
520 x / (x * A) = A'. [back_rewrite(507),rewrite([511(6),32(8)])].
538 A' / x = x' * A'. [back_rewrite(407),rewrite([515(4),520(4)]),flip(a)].
552 (x * (A * y)) / y = y * ((y' * x) * A). [para(32(a,1),51(a,1,1,1))].
571 (x * A') * A = x. [para(511(a,1),10(a,1,1))].
577 A' * (x * A) = x. [para(520(a,1),10(a,1,1))].
580 (x * A) / x = A. [para(520(a,1),64(a,1,1)),rewrite([22(3)]),flip(a)].
582 A' * x = x * A'. [para(520(a,1),76(a,1,1)),rewrite([14(7),22(5)])].
596 A * x = x * A. [para(580(a,1),10(a,1,1))].
605 A * (x * A') = x. [back_rewrite(571),rewrite([596(5,R)])].
609 (x * (A * y)) / y = y * (A * (y' * x)).
[back_rewrite(552),rewrite([596(8,R)])].
620 (A * c3) * (A * c4) != A * (A * (c3 *
c4)).
[back_rewrite(17),rewrite([596(6,R),596(13,R)])].
672 x' * (A * x) = A. [para(596(a,2),11(a,1,2))].
678 (A * (A * x)) * y = A * (x * (A * y)). [para(596(a,2),13(a,1,1,2))].
679 A * (x * (y * x)) = x * (y * (x * A)). [para(596(a,2),13(a,1))].
680 A * (x * (y * x)) = x * (y * (A * x)).
[para(596(a,2),13(a,2,2,2)),rewrite([596(4,R)])].
685 x' * A = A * x'. [para(596(a,2),29(a,2)),rewrite([29(2)])].
686 x * (A * x') = A. [para(596(a,2),32(a,1,2))].
687 (A * (x * A)) / x = A * A. [para(596(a,1),33(a,1,1,2))].
697 (A * (x * (A * x))) * y = A * (x * (x * (A *
y))). [para(596(a,2),40(a,1,1,2,2))].
724 A * (x * A) = x * (A * A).
[para(15(a,1),577(a,1,2)),rewrite([59(8),11(9)]),flip(a)].
730 x / (A * (x * A)) = A' * A'.
[para(577(a,1),85(a,1,1)),rewrite([22(3)])].
740 A * (A * x) = x * (A * A).
[para(605(a,1),15(a,2,1)),rewrite([596(6,R),605(6),596(4,R)])].
768 x * (A * y) = x * (y * A).
[para(54(a,1),30(a,1,2)),rewrite([609(5),11(4),14(10),22(5),14(8),22(5),22(6)])].
812 (A * A) / x = A * (x' * A). [para(672(a,1),36(a,1,1,2))].
1393 x / (A' * A') = A * (x * A). [para(687(a,1),95(a,1,1)),rewrite([812(5),22(3),730(9)]),flip(a)].
1439 x' * (A * (x * A)) = A * A. [para(724(a,2),11(a,1,2))].
1452 x * (A * (x' * A)) = A * A. [para(724(a,2),32(a,1,2))].
1681 (x * (y * A)) / (A * y) = x. [para(768(a,1),9(a,1,1))].
1683 (x / (A * y)) * (y * A) = x. [para(768(a,1),10(a,1))].
1684 (x / (y * A)) * (A * y) = x. [para(768(a,2),10(a,1))].
2099 x / (A * y) = x / (y * A). [para(10(a,1),1681(a,1,1))].
2258 (A * x) / y = (x * A) / y.
[para(1683(a,1),30(a,1,2)),rewrite([64(7)]),flip(a)].
2298 A * (A * (x / (y * A))) = (A * x) / y.
[para(1684(a,1),36(a,1,1,2)),rewrite([596(9,R)]),flip(a)].
2533 (A * (A * x)) / y = (x * (A * A)) / y.
[para(740(a,1),2258(a,1,1)),rewrite([596(9,R)]),flip(a)].
3320 x' * (A' * (x * A')) = A' * A'. [para(1452(a,1),14(a,1,1)),rewrite([14(4),14(12),14(12),22(10)]),flip(a)].
3594 (x' * A) / y' = y / (A' * x).
[para(582(a,2),91(a,2,2)),rewrite([22(4)])].
5266 (x / (y * z)) * y = y' * ((y * x) / z). [para(110(a,1),11(a,1,2)),flip(a)].
9681 (x / y) * (A * y) = y' * (A * (y * x)).
[para(596(a,2),143(a,1,2)),rewrite([596(8,R)])].
10060 (x * y) * (A * x') = x * (A * (y /
x)).
[para(685(a,1),144(a,1,2)),rewrite([22(2),22(7),22(7),596(8,R)])].
10956 (x' * A) * ((A * x) * y) = x' * (A * (x *
(A * y))).
[para(596(a,2),148(a,2,2,1)),rewrite([511(7),144(9),538(6),22(4),582(8,R),3320(9)
,1393(7),13(6),487(9)]),flip(a)].
18985 (A * (x * (y * x))) * (x' * z) = x * (((y *
(x * A)) / x) * z).
[para(679(a,2),151(a,1,1))].
19224 (x * (A * (x' * y))) * (x * z) = x' * ((A *
(x * (y * x))) * z).
[para(680(a,2),143(a,2,2,1)),rewrite([609(4)])].
19231 x * (((y * (x * A)) / x) * z) = x * ((x *
(A * (x' * y))) * z).
[para(680(a,2),151(a,1,1)),rewrite([18985(7),609(10)])].
19272 (A * (x * (y * x))) * (x' * z) = x * ((x *
(A * (x' * y))) * z).
[back_rewrite(18985),rewrite([19231(13)])].
24873 (A * (A * x)) / (y * A) = (x * (A * A)) /
(A * y).
[para(2533(a,1),2099(a,1)),flip(a)].
38534 (x * (y * A)) / y = y * (A * (y' * x)). [para(596(a,1),609(a,1,1,2))].
43730 A' * (x / (A' * y)) = A * ((A' * x) /
y).
[para(5266(a,1),230(a,2)),rewrite([230(16),582(7,R),22(10)])].
43817 (A * (x * y)) * x' = x * (y / (A' *
x)).
[para(3594(a,1),5266(a,2,2)),rewrite([487(5),14(4),22(2),22(2),596(3,R),22(7)])].
46287 x * (A * (x' * (y / x))) = y / (A' *
x).
[para(9681(a,1),609(a,1,1)),rewrite([107(6),43817(6),11(7)]),flip(a)].
50958 x * (A * (x' * (y / (x * A)))) = y /
x.
[para(10(a,1),38534(a,1,1)),flip(a)].
52078 x * (A * (x' * (y / (A * x)))) = y /
x.
[para(596(a,2),50958(a,1,2,2,2,2))].
52094 x' * (A * (x * (y / x))) = (A * y) /
x.
[para(50958(a,1),249(a,2,2,2,2)),rewrite([686(6),1439(6),12(7),2298(7)]),flip(a)].
52101 A * (x * (y / x)) = x * ((A * y) / x). [para(50958(a,1),697(a,2,2,2)),rewrite([19272(11),1452(6),12(7),2298(7)]),flip(a)].
52280 x * ((A * (y * x)) / x) = A * (x * y). [para(9(a,1),52101(a,1,2,2)),flip(a)].
52604 x / (A' * (y' * x)) = x * (A * (x' *
y)).
[para(52280(a,1),32(a,1,2)),rewrite([93(11),14(10),14(10),22(10)]),flip(a)].
52698 x' * (A * (x * (A * y))) = x * (A * (A *
(x' * y))).
[para(52280(a,1),38534(a,2,2,2)),rewrite([93(6),14(5),14(5),22(5),52604(6),19224(
8),596(7,R),107(9),678(9),10060(8),9(5)])].
52720 (x' * A) * ((A * x) * y) = x * (A * (A *
(x' * y))). [back_rewrite(10956),rewrite([52698(14)])].
53093 A * (x' * (y / (A * x))) = x' * (y /
x).
[para(52078(a,1),11(a,1,2)),flip(a)].
53131 (A * x) / (y * A) = A * ((A' * x) /
y).
[para(2099(a,1),52094(a,2)),rewrite([14(3),144(13),515(6),52720(12),53093(10),46287(8),43730(7
)]),flip(a)].
53220 (x * (A * A)) / (A * y) = A * (x / y).
[back_rewrite(24873),rewrite([53131(7),11(6)]),flip(a)].
53407 (A * (x / y)) * (A * y) = x * (A * A). [para(53220(a,1),10(a,1,1))].
53970 (A * x) * (A * y) = A * (A * (x * y)). [para(9(a,1),53407(a,1,1,2)),rewrite([724(10,R),596(9,R)])].
53971 $F.
[resolve(53970,a,620,a)].
============================== end of proof
==========================
% Proof
2 at 38.70 (+ 0.22) seconds.
% Length
of proof is 319.
% Level
of proof is 34.
%
Maximum clause weight is 38.000.
% Given
clauses 1210.
1 z *
((A * y) * z) = (z * A) * (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].
12 (x *
x) * y = x * (x * y).
[assumption].
13 (x *
(y * x)) * z = x * (y * (x * z)).
[assumption].
14 (x *
y)' = x' * y'. [assumption].
15 (x *
(y * A)) * x = (x * y) * (A * x).
[assumption].
16 (c1 *
A) * (c2 * c1) != c1 * ((A * c2) * c1).
[deny(1)].
18 0' =
0. [para(5(a,1),3(a,1)),flip(a)].
21 x \ 0
= x'. [para(5(a,1),8(a,1,2))].
22 x'' =
x.
[para(6(a,1),8(a,1,2)),rewrite([21(3)])].
23 x / x
= 0. [para(3(a,1),9(a,1,1))].
29 x \ y
= x' * y. [para(7(a,1),11(a,1,2)),flip(a)].
30 x /
(y * x) = y'.
[para(11(a,1),9(a,1,1))].
32 x *
(x' * y) = y.
[back_rewrite(7),rewrite([29(1)])].
33 (x *
(x * y)) / y = x * x.
[para(12(a,1),9(a,1,1))].
36 (x *
(y * (x * z))) / z = x * (y * x).
[para(13(a,1),9(a,1,1))].
37 x *
((y / x) * (x * z)) = (x * y) * z.
[para(10(a,1),13(a,1,1,2)),flip(a)].
40 (x *
(y * (y * x))) * z = x * (y * (y * (x * z))). [para(12(a,1),13(a,1,1,2)),rewrite([12(7)])].
42 (x *
(y * (z * (y * x)))) * u = x * (y * (z * (y * (x * u)))).
[para(13(a,1),13(a,1,1,2)),rewrite([13(9)])].
46 (x /
y)' * y' = x'.
[para(10(a,1),14(a,1,1)),flip(a)].
47 (x' *
y') * ((x * y) * z) = z.
[para(14(a,1),11(a,1,1))].
48 (x *
A) * x = x * (A * x).
[para(3(a,1),15(a,1,1,2)),rewrite([4(5)])].
49 (x *
A') * (A * x) = x * x.
[para(6(a,1),15(a,1,1,2)),rewrite([4(2)]),flip(a)].
51 ((x *
y) * (A * x)) / x = x * (y * A).
[para(15(a,1),9(a,1,1))].
53 ((x /
(y * A)) * y) * (A * (x / (y * A))) = x * (x / (y * A)). [para(10(a,1),15(a,1,1)),flip(a)].
54 (x' *
(y' * A')) * ((x * y) * (A * x)) = x.
[para(15(a,1),11(a,1,2)),rewrite([14(4),14(4)])].
56 (x *
(y * (y * A))) * x = (x * (y * y)) * (A * x). [para(12(a,1),15(a,1,1,2))].
57 (x *
(x * (y * A))) * (x * x) = (x * (x * y)) * (A * (x * x)).
[para(12(a,1),15(a,1,1)),rewrite([12(8)])].
58 (x *
((x * y) * (A * x))) * z = x * ((x * (y * A)) * (x * z)). [para(15(a,1),13(a,1,1,2))].
59 (A *
x) * (A * A) = A * (x * (A * A)).
[para(15(a,1),13(a,1))].
61 (x *
(y * (x * (z * A)))) * (x * (y * x)) = (x * (y * (x * z))) * (A * (x * (y *
x))).
[para(13(a,1),15(a,1,1)),rewrite([13(11)])].
62 (x' *
(y' * A')) * x' = (x' * y') * (A' * x').
[para(15(a,1),14(a,1,1)),rewrite([14(5),14(2),14(6),14(12),14(12)]),flip(a)].
64 (x /
y)' = y / x.
[para(10(a,1),30(a,1,2)),flip(a)].
66 x /
(y * (z * (y * x))) = y' * (z' * y').
[para(13(a,1),30(a,1,2)),rewrite([14(7),14(7)])].
68 (x /
y) * x' = y'.
[back_rewrite(46),rewrite([64(2)])].
70 (x *
y) * ((x' * y') * z) = z. [para(14(a,1),32(a,1,2,1))].
73 x' /
y' = y / x.
[para(68(a,1),9(a,1,1))].
74 x' *
((x / y) * (x' * z)) = (x' * y') * z.
[para(68(a,1),13(a,1,1,2)),flip(a)].
76 (x' /
y) * x = y'.
[para(22(a,1),68(a,1,2))].
78 x /
x' = x * x.
[para(5(a,1),33(a,1,1,2)),rewrite([4(2)])].
85 (x *
y) / (x' * y) = x * x.
[para(32(a,1),33(a,1,1,2))].
91 (x' *
y') / z' = z / (x * y).
[para(14(a,1),73(a,1,1))].
93 x /
y' = y / x'.
[para(22(a,1),73(a,1,1))].
95 (x /
y) / z' = z / (y / x).
[para(64(a,1),73(a,1,1))].
100 x *
((x' / y) * (x * z)) = (x * y') * z.
[para(76(a,1),13(a,1,1,2)),flip(a)].
107 (x'
* y) / x = x' * (y * x').
[para(6(a,1),36(a,1,1,2,2)),rewrite([4(3)])].
109 ((x
/ y) * (z * x)) / y = (x / y) * (z * (x / y)). [para(10(a,1),36(a,1,1,2,2))].
110 x *
((y / (x * z)) * x) = (x * y) / z.
[para(10(a,1),36(a,1,1,2)),flip(a)].
115 (x *
(y * (z * (y * (x * u))))) / u = x * (y * (z * (y * x))).
[para(13(a,1),36(a,1,1,2)),rewrite([13(9)])].
116 ((x
* (y * A)) * (z * ((x * y) * (A * x)))) / x = (x * (y * A)) * (z * (x * (y *
A))).
[para(15(a,1),36(a,1,1,2,2))].
122 x *
(((x' * y') / z) * x) = (x * z') / y.
[para(76(a,1),36(a,1,1,2)),rewrite([14(5)]),flip(a)].
123 (x *
y) / z' = z / (x' * y').
[para(14(a,1),93(a,1,2)),flip(a)].
139 (x *
y) * x' = x * (y / x).
[para(5(a,1),37(a,1,2,2)),rewrite([4(3)]),flip(a)].
140 (x'
* y) * x = x' * (y / x').
[para(6(a,1),37(a,1,2,2)),rewrite([4(5)]),flip(a)].
142 (x /
y) * ((z / (x / y)) * x) = ((x / y) * z) * y. [para(10(a,1),37(a,1,2,2))].
143 (x /
y) * (y * z) = y' * ((y * x) * z).
[para(37(a,1),11(a,1,2)),flip(a)].
144 (x'
* y) * (x * z) = x' * ((y / x') * z).
[para(11(a,1),37(a,1,2,2)),flip(a)].
148 x' *
((x / ((x' * y') * (x / y))) * z) = (y / x) * ((x * y) * z).
[para(37(a,1),13(a,2,2)),rewrite([143(4),144(7),93(6),14(5),14(3),64(6
)])].
151 (x *
y) * (x' * z) = x * ((y / x) * z).
[para(32(a,1),37(a,1,2,2)),flip(a)].
160 (x *
(A * x)) / x = x * A.
[para(48(a,1),9(a,1,1))].
230 (x *
x) / (A * x) = x * A'.
[para(49(a,1),9(a,1,1))].
238 (A *
x) / (x * x) = x' * A.
[para(49(a,1),30(a,1,2)),rewrite([14(8),22(8)])].
239 ((A'
* x) * A') * x = (A' * x) * (A' * x).
[para(32(a,1),49(a,1,2))].
249 (x *
(y * (z * (z * (y * x))))) * u = x * (y * (z * (z * (y * (x * u))))).
[para(40(a,1),13(a,1,1,2)),rewrite([40(11)])].
386 (x *
A) * (x / (x * A)) = x.
[para(48(a,1),139(a,1,1)),rewrite([14(6),151(8),9(3),5(4),4(2)]),flip(a)].
387 (A *
(x / A)) * (A * (A * x)) = (A * x) * (A * x). [para(139(a,1),49(a,1,1))].
402 x *
((x / A) / x) = x / A.
[para(10(a,1),386(a,1,1)),rewrite([10(6)])].
403 x /
(x * A) = x' * (A' / x').
[para(386(a,1),11(a,1,2)),rewrite([14(3),140(5)]),flip(a)].
404 (x *
(x * A)) * ((x * x) / (x * (x * A))) = x * x. [para(12(a,1),386(a,1,1)),rewrite([12(7)])].
407 x' *
(x / (x / A')) = A' / x. [para(76(a,1),386(a,1,1)),rewrite([76(9),93(6),64(5)])].
422 x /
(A / x') = x * (x' / A).
[para(402(a,1),32(a,1,2)),rewrite([93(9),64(8)]),flip(a)].
432 (x *
(x * (x * x))) / (A * (x * x)) = x * (x * A'). [para(12(a,1),230(a,1,1)),rewrite([12(11)])].
472 x * (x
* (A / x)) = x * A.
[para(238(a,1),139(a,2,2)),rewrite([12(4),14(6),151(8),160(4),139(4),12(9),32(8)])].
475 x *
(A / x) = A.
[para(472(a,1),11(a,1,2)),rewrite([11(4)]),flip(a)].
487 A /
x = x' * A.
[para(475(a,1),11(a,1,2)),flip(a)].
492 x' *
((x * A) * (y * (x * ((x' * A) * z)))) = (x' * ((x * A) * (y * A))) * z.
[para(475(a,1),42(a,1,1,2,2,2)),rewrite([487(2),144(7),487
(4),22(3),487(10),487(13),144(19),487(12),22(11)]),flip(a)].
497 x' *
(A' / x') = x * (x' / A).
[back_rewrite(422),rewrite([487(3),22(2),403(3)])].
507 x /
(x * A) = x * (x' / A).
[back_rewrite(403),rewrite([497(9)])].
511 x /
A = x * A'.
[para(487(a,1),64(a,1,1)),rewrite([14(4),22(2)]),flip(a)].
515 x /
A' = x * A.
[para(487(a,1),93(a,1)),rewrite([22(2)]),flip(a)].
520 x /
(x * A) = A'.
[back_rewrite(507),rewrite([511(6),32(8)])].
535 (A *
(x * A')) * (A * (A * x)) = (A * x) * (A * x). [back_rewrite(387),rewrite([511(3)])].
538 A' /
x = x' * A'.
[back_rewrite(407),rewrite([515(4),520(4)]),flip(a)].
552 (x *
(A * y)) / y = y * ((y' * x) * A).
[para(32(a,1),51(a,1,1,1))].
569 (x *
(y * (z * (y * (x * (A * x)))))) / x = x * ((y * (z * (y * x))) * A). [para(42(a,1),51(a,1,1))].
571 (x *
A') * A = x.
[para(511(a,1),10(a,1,1))].
577 A' *
(x * A) = x. [para(520(a,1),10(a,1,1))].
578 (x *
x) / (x * (x * A)) = A'.
[para(12(a,1),520(a,1,2))].
580 (x *
A) / x = A.
[para(520(a,1),64(a,1,1)),rewrite([22(3)]),flip(a)].
582 A' *
x = x * A'.
[para(520(a,1),76(a,1,1)),rewrite([14(7),22(5)])].
589 A' *
(x * (x * A)) = x * x.
[back_rewrite(404),rewrite([578(8),582(6,R)])].
593 (A'
* (A' * x)) * x = (A' * x) * (A' * x).
[back_rewrite(239),rewrite([582(6,R)])].
596 A *
x = x * A.
[para(580(a,1),10(a,1,1))].
605 A *
(x * A') = x.
[back_rewrite(571),rewrite([596(5,R)])].
606 (x *
(y * (z * (y * (x * (A * x)))))) / x = x * (A * (y * (z * (y * x)))).
[back_rewrite(569),rewrite([596(13,R)])].
609 (x *
(A * y)) / y = y * (A * (y' * x)).
[back_rewrite(552),rewrite([596(8,R)])].
621 (A *
c1) * (c2 * c1) != c1 * ((A * c2) * c1).
[back_rewrite(16),rewrite([596(3,R)])].
623 (A *
x) * (A * x) = x * (A * (A * x)).
[back_rewrite(535),rewrite([605(5)]),flip(a)].
625 (x *
A') * x = x * (x * A').
[para(3(a,1),53(a,1,1,1,2)),rewrite([511(2),4(5),3(7),511(6),605(8),3(7),511(6)])].
640 (x *
A') * (A * (x / (x' * A))) = x * (x / (x' * A)). [para(68(a,1),53(a,1,1)),rewrite([14(4),22(2)])].
672 x' *
(A * x) = A.
[para(596(a,2),11(a,1,2))].
676 (x *
(x * A)) * y = x * (A * (x * y)).
[para(596(a,1),13(a,1,1,2))].
678 (A *
(A * x)) * y = A * (x * (A * y)).
[para(596(a,2),13(a,1,1,2))].
679 A *
(x * (y * x)) = x * (y * (x * A)).
[para(596(a,2),13(a,1))].
680 A *
(x * (y * x)) = x * (y * (A * x)).
[para(596(a,2),13(a,2,2,2)),rewrite([596(4,R)])].
685 x' *
A = A * x'.
[para(596(a,2),29(a,2)),rewrite([29(2)])].
686 x *
(A * x') = A.
[para(596(a,2),32(a,1,2))].
687 (A *
(x * A)) / x = A * A.
[para(596(a,1),33(a,1,1,2))].
691 A' *
(x * (y * (A * x))) = x * (y * x).
[para(596(a,2),36(a,1,1,2,2)),rewrite([511(6),582(7,R)])].
697 (A *
(x * (A * x))) * y = A * (x * (x * (A * y))). [para(596(a,2),40(a,1,1,2,2))].
708 (A *
x) * x' = A.
[para(596(a,2),139(a,1,1)),rewrite([487(6),32(8)])].
710 (A'
* x') * ((x * A) * y) = y.
[para(596(a,1),47(a,1,2,1))].
711 (x'
* A') * ((A * x) * y) = y.
[para(596(a,2),47(a,1,2,1))].
723 A *
(x * (A' * x)) = x * x.
[para(577(a,1),13(a,2,2)),rewrite([596(6,R)])].
724 A *
(x * A) = x * (A * A).
[para(15(a,1),577(a,1,2)),rewrite([59(8),11(9)]),flip(a)].
730 x /
(A * (x * A)) = A' * A'.
[para(577(a,1),85(a,1,1)),rewrite([22(3)])].
740 A *
(A * x) = x * (A * A).
[para(605(a,1),15(a,2,1)),rewrite([596(6,R),605(6),596(4,R)])].
746 x /
(A' * (x * A')) = A * A.
[para(605(a,1),85(a,1,1))].
754 x' *
(A' * x) = A'. [para(5(a,1),54(a,1,2,2)),rewrite([22(3),605(6),4(6)])].
768 x *
(A * y) = x * (y * A).
[para(54(a,1),30(a,1,2)),rewrite([609(5),11(4),14(10),22(5),14(8),22(5),22(6)])].
769 (x'
* (A' * (x * y'))) * (y * (A * x)) = x.
[para(32(a,1),54(a,1,2,1)),rewrite([14(4),22(3),582(6,R)])].
804 (A'
* x') * (x * (A * A)) = A.
[para(605(a,1),54(a,1,2,1)),rewrite([14(6),22(6),582(8,R),577(8)])].
809 (A *
x') * x = A.
[para(32(a,1),672(a,1,2)),rewrite([14(4),22(3)])].
812 (A *
A) / x = A * (x' * A).
[para(672(a,1),36(a,1,1,2))].
829 x *
((A * x') / x) = A * x'.
[para(686(a,1),139(a,1,1)),flip(a)].
832 (A'
* x') * x = A'.
[para(708(a,1),14(a,1,1)),rewrite([14(5),22(8)]),flip(a)].
841 x' *
(A * A) = A * (A * x').
[para(809(a,1),12(a,2,2)),rewrite([623(7),40(8),6(5),4(5),596(10,R)])].
844 (A'
* x) * x' = A'.
[para(809(a,1),14(a,1,1)),rewrite([14(6),22(6)]),flip(a)].
893 A' *
(x * x) = x * (x * A').
[para(56(a,1),230(a,2)),rewrite([589(6),589(7),12(3),589(10),432(7),5(12),4(10)]),flip(a)].
911 (x *
(x * A')) * y = x * (A' * (x * y)).
[para(582(a,1),13(a,1,1,2))].
913 (A'
* (A' * x)) * y = A' * (x * (A' * y)).
[para(582(a,2),13(a,1,1,2))].
923 (A'
* (x * (A' * x))) * y = A' * (x * (x * (A' * y))). [para(582(a,2),40(a,1,1,2,2))].
931 (A'
* (x * (y * (A' * x)))) * z = A' * (x * (y * (x * (A' * z)))). [para(582(a,2),42(a,1,1,2,2,2))].
934 (A *
x') * ((x * A') * y) = y.
[para(582(a,1),47(a,1,2,1)),rewrite([22(3)])].
936 (x'
* y') * (A' * (x * y)) = A'.
[para(582(a,2),47(a,1,2))].
940 (A'
* x) * (A' * x) = A' * (x * (A' * x)).
[back_rewrite(593),rewrite([913(7)]),flip(a)].
960 x *
(x * (A * y)) = x * (x * (y * A)).
[para(57(a,1),9(a,1,1)),rewrite([609(8),14(4),12(8),11(7),11(5),12(4)])].
1004 A'
* (A' * x) = x * (A' * A').
[para(577(a,1),57(a,2,1,2)),rewrite([596(8,R),11(9),577(5),32(16),582(12,R)]),flip(a)].
1019 (A'
* A') / x = A' * (x' * A').
[para(754(a,1),36(a,1,1,2))].
1393 x /
(A' * A') = A * (x * A).
[para(687(a,1),95(a,1,1)),rewrite([812(5),22(3),730(9)]),flip(a)].
1394 x /
(A * A) = A' * (x * A').
[para(687(a,1),95(a,2,2)),rewrite([730(5),1019(7),22(4)]),flip(a)].
1439 x'
* (A * (x * A)) = A * A.
[para(724(a,2),11(a,1,2))].
1440 A *
(A * (x * x)) = x * (x * (A * A)).
[para(724(a,2),12(a,1)),rewrite([596(4,R)])].
1450 x'
* (A * A) = A * (x' * A).
[para(724(a,2),29(a,2)),rewrite([29(4)])].
1452 x *
(A * (x' * A)) = A * A.
[para(724(a,2),32(a,1,2))].
1468 (x
* (A * A)) / x = A * A.
[para(724(a,1),85(a,1,1)),rewrite([577(9)])].
1679 (A'
* x') * (x * A) = 0. [para(768(a,1),6(a,1)),rewrite([14(3)])].
1680 (x'
* A') * (A * x) = 0.
[para(768(a,2),6(a,1)),rewrite([14(3)])].
1681 (x
* (y * A)) / (A * y) = x.
[para(768(a,1),9(a,1,1))].
1683 (x
/ (A * y)) * (y * A) = x.
[para(768(a,1),10(a,1))].
1684 (x
/ (y * A)) * (A * y) = x.
[para(768(a,2),10(a,1))].
1814
((x' * y') * (A' * x')) * (x * (y * A)) = (x' * (y' * A')) * (x' / (x' * (y' *
A'))).
[para(62(a,1),139(a,1,1)),rewrite([14(15),22(10),
14(13),22(10),22(11)])].
2008 x /
(x * (A' * A')) = A * A.
[para(1468(a,1),93(a,1)),rewrite([14(9),22(5),14(7)]),flip(a)].
2024 (A
* x) * (x' * A') = 0.
[para(1679(a,1),14(a,1,1)),rewrite([18(2),14(6),22(4),22(4),14(6)]),flip(a)].
2025 (A'
* x) * (x' * A) = 0.
[para(22(a,1),1679(a,1,1,2))].
2028 ((x
* A) * (A' * x')) * y = (x * A) * ((A' * x') * y). [para(1679(a,1),40(a,1,1,2,2)),rewrite([4(8),710(22)])].
2043 (x
* A) * (x * A') = x * x.
[para(1679(a,1),61(a,2,1,2)),rewrite([804(9),832(7),4(8),832(12),605(11)])].
2051 (x
* A) * (A' * x') = 0.
[para(1680(a,1),14(a,1,1)),rewrite([18(2),14(6),22(3),22(4),14(6)]),flip(a)].
2055 (A
* x) * ((x' * A') * y) = y.
[para(1680(a,1),40(a,1,1,2,2)),rewrite([4(8),2024(7),3(2),711(14)]),flip(a)].
2063 (x
* A) * ((A' * x') * y) = y.
[back_rewrite(2028),rewrite([2051(7),3(2)]),flip(a)].
2099 x /
(A * y) = x / (y * A).
[para(10(a,1),1681(a,1,1))].
2166 x /
(x' * y) = x * (y' * x).
[para(6(a,1),66(a,1,2,2,2)),rewrite([4(3),22(5),22(6)])].
2168 x'
* (((x * y) / z) * x') = y / (x * z).
[para(10(a,1),66(a,1,2,2)),rewrite([64(6)]),flip(a)].
2205 x'
* ((A' * (x * y)) * x') = y / (x * A).
[para(809(a,1),66(a,1,2,2)),rewrite([14(7),14(10),14(10),22(8),22(8)]),flip(a)].
2246 (x
* A') * (x * x) = x * (x * (A' * x)).
[back_rewrite(640),rewrite([2166(8),723(9),2166(9)])].
2258 (A
* x) / y = (x * A) / y.
[para(1683(a,1),30(a,1,2)),rewrite([64(7)]),flip(a)].
2261 x *
((y / (A * x)) * x) = A' * (x * y).
[para(1683(a,1),36(a,1,1,2)),rewrite([511(3),582(4,R)]),flip(a)].
2280 (x
/ (y * (A * A))) * (A * (y * A)) = x.
[para(724(a,1),1683(a,1,1,2)),rewrite([596(9,R)])].
2298 A *
(A * (x / (y * A))) = (A * x) / y.
[para(1684(a,1),36(a,1,1,2)),rewrite([596(9,R)]),flip(a)].
2325 (A
* x') * (x * A') = 0.
[para(22(a,1),2024(a,1,2,1))].
2327 A'
* (x' * ((A * x) * (y * A))) = x' * ((A * x) * y). [para(2024(a,1),42(a,2,2,2,2)),rewrite([708(7),582(10,R),4(15)])].
2339 (A'
* x) * ((A' * x) * y) = A' * (x * (x * (A' * y))).
[para(2025(a,1),58(a,2,2,1)),rewrite([844(8),32(10),940(7),923(8),3(17)]),flip(a
)].
2340
((A' * x) * (((A' * x) * y) * x)) * (x' * A) = A' * (x * (x * y)).
[para(2025(a,1),58(a,2,2,2)),rewrite([32(12),4(24),2339(23),577(20)]
)].
2450 x /
(A * (y * y)) = x / (y * (y * A)).
[para(12(a,1),2099(a,2,2))].
2498 x /
(A * (A * y)) = x / (y * (A * A)).
[para(740(a,1),2099(a,1,2)),rewrite([596(9,R)]),flip(a)].
2509 (x
* A) / y' = y / (A' * x').
[para(2258(a,1),93(a,1)),rewrite([14(7)])].
2533 (A
* (A * x)) / y = (x * (A * A)) / y.
[para(740(a,1),2258(a,1,1)),rewrite([596(9,R)]),flip(a)].
2541 (x
* (y * z)) * ((x' * (y' * z')) * u) = u.
[para(14(a,1),70(a,1,2,1,2))].
2571 A'
* (x * ((A * x') * (y * A))) = x * ((A * x') * y).
[para(2325(a,1),42(a,2,2,2,2)),rewrite([809(7),582(10,R),4(15)])].
2633 (x
/ y) * (x' * z) = x * ((x' * y') * z).
[para(74(a,1),11(a,1,2)),rewrite([22(2)]),flip(a)].
2996 (A
* x') * (x * A) = A * A.
[para(812(a,1),1683(a,1,1)),rewrite([14(4),596(7,R),32(7)])].
3320 x'
* (A' * (x * A')) = A' * A'.
[para(1452(a,1),14(a,1,1)),rewrite([14(4),14(12),14(12),22(10)]),flip(a)].
3454 (x
* A) * (A' * x) = x * x.
[para(15(a,1),2043(a,1,2)),rewrite([577(5),5(9),4(7),577(11),577(11)])].
3536 (A
* x) * (x' * A) = A * A.
[para(22(a,1),2996(a,1,1,2))].
3594 (x'
* A) / y' = y / (A' * x).
[para(582(a,2),91(a,2,2)),rewrite([22(4)])].
3748 (A'
* x) / (x * x) = x' * A'.
[para(3454(a,1),30(a,1,2)),rewrite([14(8)])].
3984 (A'
* x) * y = (x * A') * y.
[para(582(a,2),100(a,2,1)),rewrite([511(3),144(6),538(5),22(3),32(7)]),flip(a)].
4279 (A
* x) * y = (x * A) * y.
[para(710(a,1),11(a,1,2)),rewrite([14(5),22(3),22(3)])].
4382 (A
* x) * (A * y) = (x * A) * (y * A).
[para(4279(a,1),768(a,2))].
4741 x /
(A' * x') = x * (A * x).
[para(829(a,1),32(a,1,2)),rewrite([22(3),22(6),93(7),14(6)]),flip(a)].
4761 x'
/ (A * x) = x' * (x' * A').
[para(829(a,1),711(a,1,2)),rewrite([14(8),32(10),625(6),14(10),32(12)]),flip(a)].
4770 (A'
* x') / x = x' * (A' * x').
[para(582(a,2),107(a,1,1))].
4958 (x
* A') * (y * (x * A')) = A' * ((x * A') * (y * x)).
[para(109(a,1),511(a,1)),rewrite([511(2),511(5),511(10),582(16,R)])].
5138 (A'
* (x * x)) / (x * A') = x.
[para(893(a,2),9(a,1,1))].
5151 (x
* A') * (A' * (x * x)) = A' * (x * (x * (A' * x))).
[para(893(a,2),36(a,2,2)),rewrite([36(10),4958(8),2246(7)]),flip(a)].
5266 (x
/ (y * z)) * y = y' * ((y * x) / z).
[para(110(a,1),11(a,1,2)),flip(a)].
5274 (x
* y) / (x' * z) = x * ((y / z) * x).
[para(32(a,1),110(a,1,2,1,2)),flip(a)].
5276 (x
* y) * (x * y) = x * (y * (y * x)).
[para(78(a,1),110(a,2)),rewrite([14(2),32(4),78(2),12(2)]),flip(a)].
5288 ((x
* y) / z) * x' = x * (y / (x * z)).
[para(110(a,1),139(a,1,1)),rewrite([5266(7),107(9),2168(10)])].
5293 A *
(A * (x / (A * y))) = (A * x) / y.
[para(110(a,1),596(a,1)),rewrite([596(8,R),596(10,R)]),flip(a)].
5295 (A
* x) / (y * A') = A * (A * (x / y)).
[para(605(a,1),110(a,1,2,1,2)),rewrite([596(4,R)]),flip(a)].
5347 (x
* (A * y)) / z = (x * (y * A)) / z.
[para(768(a,1),110(a,2,1)),rewrite([5266(5),32(7)])].
5424 (A'
* x) / (x * A') = 0.
[para(746(a,1),110(a,1,2,1)),rewrite([582(8,R),724(8,R),596(7,R),5(7),4(5),596(4,R),5(4)]),flip(a)].
5780 (x
* A') / (A' * x) = 0.
[para(5424(a,1),64(a,1,1)),rewrite([18(2)]),flip(a)].
5784 (x
* (A' * y)) / (y * A') = x.
[para(5424(a,1),109(a,1,1,1)),rewrite([3(6),5424(15),5424(16),4(11),3(10)])].
5790 (x
* (y * A')) / (A' * y) = x.
[para(5780(a,1),109(a,1,1,1)),rewrite([3(6),5780(15),5780(16),4(11),3(10)])].
6116 A *
((x * y) * ((x' * (y' * A')) * (A * (x * y)))) = (A * ((x * y) * x)) / x.
[para(54(a,1),115(a,1,1,2,2)),rewrite([596(16,R)]),flip(a
)].
6224 A'
* (x * ((A * x') * (y * (A * A)))) = x * ((A * x') * (y * A)).
[para(2996(a,1),115(a,1,1,2,2,2)),rewrite([511(11),582(12,R),809(19)]
)].
6236 A'
* (x' * ((A * x) * (y * (A * A)))) = x' * ((A * x) * (y * A)).
[para(3536(a,1),115(a,1,1,2,2,2)),rewrite([511(11),582(12,R),708(19)]
)].
6319 A *
(A * (x * (A' * A'))) = x.
[para(1393(a,1),9(a,1)),rewrite([596(9,R)])].
6359 (x
* (y * A)) / x = x' / (x' * (y' * A')).
[para(6(a,1),116(a,1,1,2)),rewrite([4(5),14(12),14(9),14(13),1814(19),2541(23)])].
6648 A'
* (x * A') = x * (A' * A').
[para(1450(a,1),14(a,1,1)),rewrite([14(6),14(6),22(4),22(8),14(10)])].
7106
((x' * y') / z) * x = x' * ((x * z') / y). [para(122(a,1),11(a,1,2)),flip(a)].
7272 x *
(A * (A * (x * ((A' * x') * y)))) = (x * A) * y. [para(2063(a,1),12(a,2,2)),rewrite([5276(5),40(11)])].
7362 (x'
* (A * A)) / y' = y / (A' * (A' * x)).
[para(841(a,2),123(a,1,1)),rewrite([14(13),22(13)])].
9114 (A'
* x) * (y * A) = A' * ((x * A) * y).
[para(520(a,1),142(a,1,1)),rewrite([520(5),515(5),520(9)]),flip(a)].
9259 (x
* A') * ((A' * x) * y) = A' * (x * (x * (A' * y))). [para(3984(a,1),12(a,2)),rewrite([5276(7),40(8)]),flip(a)].
9295
((A' * x) * y) * (x' * A) = (x * A') * (y / (x * A')).
[para(3984(a,2),139(a,1,1)),rewrite([14(8),22(8)])].
9348 (x
* A') * (A * y) = A' * ((x * A) * y).
[para(3984(a,1),768(a,1)),rewrite([9114(12)])].
9349 (x
* A') * (y * A) = A' * ((x * A) * y).
[para(3984(a,1),768(a,2)),rewrite([144(6),515(5)]),flip(a)].
9446 (x
* A') * ((((A' * x) * y) * x) / (x * A')) = A' * (x * (x * y)). [back_rewrite(2340),rewrite([9295(13)])].
9651 (x
/ (y * y)) * (y * (y * z)) = y' * (y' * ((y * (y * x)) * z)).
[para(12(a,1),143(a,1,2)),rewrite([14(7),12(10),12(12)])].
9680 (x
* A) * (A' * y) = A * ((A' * x) * y).
[para(515(a,1),143(a,1,1)),rewrite([22(9)])].
9681 (x
/ y) * (A * y) = y' * (A * (y * x)).
[para(596(a,2),143(a,1,2)),rewrite([596(8,R)])].
9689 x'
* (A' * (x' * ((A * x) * y))) = A' * ((x' * A) * y).
[para(708(a,1),143(a,2,2,1)),rewrite([4761(4),911(10),14(13),144(17),515(16)])]
.
10051 (A
* x') * (x * y) = x' * ((x * A) * y).
[para(596(a,2),144(a,1,1)),rewrite([487(9),22(8)])].
10060 (x
* y) * (A * x') = x * (A * (y / x)).
[para(685(a,1),144(a,1,2)),rewrite([22(2),22(7),22(7),596(8,R)])].
10733
(((A' * x) * y) * x) / (x * A') = A' * ((x * A) * y). [para(15(a,1),5784(a,1,1)),rewrite([32(9),9114(15)])].
10750 (x
* A') * (A' * ((x * A) * y)) = A' * (x * (x * y)). [back_rewrite(9446),rewrite([10733(12)])].
10864 A
* (x * (A' * A')) = A' * x.
[para(6319(a,1),11(a,1,2)),flip(a)].
10950
(x' * A) * ((x * A) * y) = x' * (A * (x * (A * y))).
[para(487(a,1),148(a,2,1)),rewrite([511(7),144(9),538(6),22(4),582(8,R),3320(9),1
393(7),13(6)]),flip(a)].
10956
(x' * A) * ((A * x) * y) = x' * (A * (x * (A * y))).
[para(596(a,2),148(a,2,2,1)),rewrite([511(7),144(9),538(6),22(4),582(8,R),3320(9)
,1393(7),13(6),487(9)]),flip(a)].
10979 (A
* x) * ((x * A') * y) = x * (A * (x * (A' * y))).
[para(832(a,1),148(a,2,2,1)),rewrite([14(5),22(3),22(3),14(11),22(9),22(9),708(10
),4770(12),723(14),3748(10),22(4),4741(12),13(14)])].
11482 A'
* (x * (x * (x * (A' * ((x' * A) * y))))) = (x * A') * (x * y).
[para(5138(a,1),151(a,2,2,1)),rewrite([5151(8),14(12),22(12),931(13
)])].
18983 (x
* y) * ((x' * z) * (A * (x * y))) = A * (x * ((y / x) * ((z / x') * y))).
[para(144(a,1),679(a,1,2,2)),rewrite([151(8),596(14,R)]),
flip(a)].
18985 (A
* (x * (y * x))) * (x' * z) = x * (((y * (x * A)) / x) * z). [para(679(a,2),151(a,1,1))].
19078 (A
* ((x * y) * x)) / x = A * (A * (x * (y * A'))).
[back_rewrite(6116),rewrite([18983(13),7106(10),22(6),511(7),582(8,R),2633(10),936
(10)]),flip(a)].
19224 (x
* (A * (x' * y))) * (x * z) = x' * ((A * (x * (y * x))) * z). [para(680(a,2),143(a,2,2,1)),rewrite([609(4)])].
19231 x
* (((y * (x * A)) / x) * z) = x * ((x * (A * (x' * y))) * z).
[para(680(a,2),151(a,1,1)),rewrite([18985(7),609(10)])].
19272 (A
* (x * (y * x))) * (x' * z) = x * ((x * (A * (x' * y))) * z). [back_rewrite(18985),rewrite([19231(13)])].
19774 A
* (x' * ((x * A') * (x * y))) = A' * ((x * A) * y).
[para(960(a,1),934(a,1,2)),rewrite([9349(12),10750(13),151(9),511(4),144(8),538(
6),22(4),9348(15)])].
20679 x'
* (A * (x * (x * (A * y)))) = A * (A * (x * y)). [para(1440(a,2),143(a,2,2,1)),rewrite([6359(5),2008(9),12(5),678(12),12(11)]),flip
(a)].
22244 x
* (A * ((y / (x * (A * A))) * (A * x))) = A' * (x * (A * y)).
[para(2280(a,1),115(a,1,1,2,2)),rewrite([511(5),582(6,R)]),flip(a)].
24873 (A
* (A * x)) / (y * A) = (x * (A * A)) / (A * y). [para(2533(a,1),2099(a,1)),flip(a)].
26074 (x
/ (A * y)) * (A * z) = A' * (((A * x) / y) * z).
[para(5293(a,1),143(a,2,2,1)),rewrite([511(7),582(8,R),11(8)])].
26436 (x
* (A * y)) / (x * (y * A)) = 0.
[para(5347(a,2),23(a,1))].
26743 (x
* (y * (A * z))) / (y * (z * A)) = x.
[para(26436(a,1),109(a,1,1,1)),rewrite([3(6),26436(15),26436(16),4(11),3(10)])].
38534 (x
* (y * A)) / y = y * (A * (y' * x)).
[para(596(a,1),609(a,1,1,2))].
38565 A'
* (x' * (A * (x * (A * y)))) = (x * A) / (y' * x). [para(609(a,1),2509(a,2)),rewrite([32(8),14(5),22(5),14(15),22(13),22(13),144(15
),515(11),10956(14)]),flip(a)].
39668 (x
/ (A * y)) * y = y' * (A' * (y * x)).
[para(2261(a,1),11(a,1,2)),flip(a)].
39670
(A' * (x * y)) * x' = x * (y / (x * A)).
[para(2261(a,1),139(a,1,1)),rewrite([39668(10),107(13),2205(14)])].
39677 (x
/ (y * A)) * (y * z) = y' * ((A' * (y * x)) * z).
[para(2261(a,1),143(a,2,2,1)),rewrite([39668(4),107(7),39670(7),11(6)])].
43730 A'
* (x / (A' * y)) = A * ((A' * x) / y).
[para(5266(a,1),230(a,2)),rewrite([230(16),582(7,R),22(10)])].
43817 (A
* (x * y)) * x' = x * (y / (A' * x)).
[para(3594(a,1),5266(a,2,2)),rewrite([487(5),14(4),22(2),22(2),596(3,R),22(7)])].
43827 A
* ((x * (A' * A')) / (A * y)) = A' * ((A' * x) / y). [para(10864(a,1),5266(a,2,2,1)),rewrite([596(11,R)])].
43838 (x
/ (A' * (A' * y))) * y = y' * (A * (A * (y * x))).
[para(1004(a,2),5266(a,1,1,2)),rewrite([1393(16),596(13,R)])].
43883 A
* ((A' * (x * A')) / y) = A * ((x * (A' * A')) / y). [para(6648(a,1),5266(a,2,2,1)),rewrite([582(10,R),43730(10),22(12)])].
44115 A'
* (x' * ((x * A) * (y * A))) = x' * ((x * A) * y).
[para(582(a,2),492(a,1,2,2,2,2)),rewrite([577(9),5(5),4(5),582(15,R)]),flip(a)].
46239 (x
* A) / (y' * x) = x' * (A * (x * y)).
[para(724(a,1),9681(a,1,2)),rewrite([39677(8),724(9,R),596(8,R),32(8),14(8),9348(15),10950(14
),38565(15)]),flip(a)].
46263 (A
* x) * (A * ((A' * x') * y)) = x * (A * (x' * y)).
[para(2509(a,2),9681(a,1,1)),rewrite([32(10),5288(6),487(4),14(3),22(3),596(4,R)
,14(10),22(8),22(8)]),flip(a)].
46277 A'
* (x' * (A * (A * (x * y)))) = (A * (x' / y')) * x.
[para(2450(a,2),9681(a,1,1)),rewrite([26074(10),9651(10),596(10,R),20679(11),14
(14),14(14),676(21),911(23),38565(22),14(15),140(17),5274(19),487(16),64(15),596(16,R),11(19)])].
46287 x
* (A * (x' * (y / x))) = y / (A' * x).
[para(9681(a,1),609(a,1,1)),rewrite([107(6),43817(6),11(7)]),flip(a)].
46290 A'
* (x' * (A * (x * (A * y)))) = x' * (A * (x * y)). [back_rewrite(38565),rewrite([46239(15)])].
46401 x'
* (A * (x * (x * y))) = x * ((A * (y / x)) * x).
[para(10060(a,1),609(a,1,1)),rewrite([93(6),14(5),14(5),64(5),2166(7),14(5),22(3),
64(3),22(9)]),flip(a)].
46422 (A
* x) * (A * ((x' * A') * y)) = x * (A * (x' * y)). [para(711(a,1),606(a,1,1,2,2,2)),rewrite([2055(13),609(8),14(6),46263(10),9348(1
9),140(18),487(18),22(17),11(18),596(16,R),5(16),4(14)]),flip(a)].
50580 x
/ (y * (x * A)) = x' * (A' * (x * y')).
[para(769(a,1),26743(a,1,1))].
50958 x
* (A * (x' * (y / (x * A)))) = y / x.
[para(10(a,1),38534(a,1,1)),flip(a)].
52078 x
* (A * (x' * (y / (A * x)))) = y / x.
[para(596(a,2),50958(a,1,2,2,2,2))].
52094 x'
* (A * (x * (y / x))) = (A * y) / x.
[para(50958(a,1),249(a,2,2,2,2)),rewrite([686(6),1439(6),12(7),2298(7)]),flip(a)].
52101 A
* (x * (y / x)) = x * ((A * y) / x).
[para(50958(a,1),697(a,2,2,2)),rewrite([19272(11),1452(6),12(7),2298(7)]),flip(a)].
52280 x
* ((A * (y * x)) / x) = A * (x * y).
[para(9(a,1),52101(a,1,2,2)),flip(a)].
52599 (A
* (x * y)) / y = y' * (A * (y * x)).
[para(52280(a,1),11(a,1,2)),flip(a)].
52604 x
/ (A' * (y' * x)) = x * (A * (x' * y)).
[para(52280(a,1),32(a,1,2)),rewrite([93(11),14(10),14(10),22(10)]),flip(a)].
52609 A
* (A * (x' * (A' * (x * y)))) = x * (A * (x' * y)). [para(52280(a,1),2055(a,1,2)),rewrite([46422(10),5295(17),93(14),14(13),14(13),2
2(10),22(11),50580(12),22(12)]),flip(a)].
52698 x'
* (A * (x * (A * y))) = x * (A * (A * (x' * y))).
[para(52280(a,1),38534(a,2,2,2)),rewrite([93(6),14(5),14(5),22(5),52604(6),19224(
8),596(7,R),107(9),678(9),10060(8),9(5)])].
52715 A
* (A * (x * (y * A'))) = x * ((A * (y / x)) * x). [back_rewrite(19078),rewrite([52599(5),46401(6)]),flip(a)].
52718 A'
* (x * (A * (A * (x' * y)))) = x' * (A * (x * y)). [back_rewrite(46290),rewrite([52698(9)])].
52720
(x' * A) * ((A * x) * y) = x * (A * (A * (x' * y))). [back_rewrite(10956),rewrite([52698(14)])].
53093 A
* (x' * (y / (A * x))) = x' * (y / x).
[para(52078(a,1),11(a,1,2)),flip(a)].
53131 (A
* x) / (y * A) = A * ((A' * x) / y).
[para(2099(a,1),52094(a,2)),rewrite([14(3),144(13),515(6),52720(12),53093(10),46287(8),43730(7
)]),flip(a)].
53220 (x
* (A * A)) / (A * y) = A * (x / y).
[back_rewrite(24873),rewrite([53131(7),11(6)]),flip(a)].
53407 (A
* (x / y)) * (A * y) = x * (A * A).
[para(53220(a,1),10(a,1,1))].
53408 A
* ((A' * (x * A')) / y) = x / (A * y).
[para(10(a,1),53220(a,1,1)),rewrite([1394(8)]),flip(a)].
53410 (x
* (A * A)) / y = A * (x / (A' * y)).
[para(32(a,1),53220(a,1,2))].
53589 A
* ((x * (A' * A')) / y) = x / (A * y).
[back_rewrite(43883),rewrite([53408(9)]),flip(a)].
53703 x
/ (A' * (A' * y)) = A * (y' / (A' * x')).
[back_rewrite(7362),rewrite([53410(7)]),flip(a)].
53749 x
/ (A * (A * y)) = A' * ((A' * x) / y).
[back_rewrite(43827),rewrite([53589(11)])].
53800 (A
* (x' / (A' * y'))) * x = x' * (A * (A * (x * y))). [back_rewrite(43838),rewrite([53703(7)])].
53917 x
/ (y * (A * A)) = A' * ((A' * x) / y).
[back_rewrite(2498),rewrite([53749(5)]),flip(a)].
53930 x
* ((A * ((A' * y) / x)) * x) = A' * (x * (A * y)). [back_rewrite(22244),rewrite([53917(6),144(11),93(10),64(9),487(9),64(8),596(9,R)
,32(12)])].
53970 (A
* x) * (A * y) = A * (A * (x * y)).
[para(9(a,1),53407(a,1,1,2)),rewrite([724(10,R),596(9,R)])].
53976 (A
* x) * (y * (A * A)) = A * (A * (x * (A * y))). [para(53407(a,1),36(a,2,2)),rewrite([36(11),53970(8),10(6),53970(7)]),flip(a)].
53981 A
* (A * (x * (A' * y))) = (A * x) * y.
[para(5784(a,1),53407(a,1,1,2)),rewrite([605(7),724(11,R),596(10,R)]),flip(a)].
53982 A
* (A * (x * (y * A'))) = (A * x) * y.
[para(5790(a,1),53407(a,1,1,2)),rewrite([32(7),724(11,R),596(10,R)]),flip(a)].
54055 A
* (A * (x * ((A' * x') * y))) = x * (A * (x' * y)). [back_rewrite(46263),rewrite([53970(10)])].
54115 (x
* A) * (y * A) = A * (A * (x * y)).
[back_rewrite(4382),rewrite([53970(5)]),flip(a)].
54130 x'
* ((A * x) * (y * A)) = x' * (A * (A * (x * y))).
[back_rewrite(6236),rewrite([53976(10),46277(12),14(5),53800(9)]),flip(a)].
54131 x
* ((A * x') * (y * A)) = x * (A * (A * (x' * y))).
[back_rewrite(6224),rewrite([53976(10),52718(12),52698(7)]),flip(a)].
54135 x'
* ((x * A) * y) = x * (A * (x' * y)).
[back_rewrite(52609),rewrite([53981(10),10051(5)])].
54137 x
* ((A * (y / x)) * x) = (A * x) * y.
[back_rewrite(52715),rewrite([53982(8)]),flip(a)].
54143 x
* (x * (A * (x' * y))) = (x * A) * y.
[back_rewrite(7272),rewrite([54055(10)])].
54153 (A
* (x' / y')) * x = x * (A * (x' * y)).
[back_rewrite(44115),rewrite([54115(8),46277(10),54135(11)])].
54181 x'
* ((A * x) * y) = x * (A * (x' * y)).
[back_rewrite(2327),rewrite([54130(9),46277(10),54153(6)]),flip(a)].
54185 x'
* (A * (x * y)) = x * ((A * x') * y).
[back_rewrite(2571),rewrite([54131(9),52718(10)])].
54205 A'
* (x * (A * y)) = A * ((x * A') * y).
[back_rewrite(53930),rewrite([54137(8),151(6),511(3)]),flip(a)].
54242 A'
* ((x' * A) * y) = A * (x' * (A' * y)).
[back_rewrite(9689),rewrite([54181(8),54205(9),151(8),538(5),54185(10),10979(9),32(10)]),fl
ip(a)].
54426 (x
* A') * (x * y) = x * (x * (A' * y)).
[back_rewrite(11482),rewrite([54242(9),54143(11),9680(8),54205(10),9259(9),32(10)]),flip(a)].
54515 A'
* ((x * A) * y) = A * (x * (A' * y)).
[back_rewrite(19774),rewrite([54426(7),11(8)]),flip(a)].
54569 (x
* A') * (A * y) = A * (x * (A' * y)).
[back_rewrite(9348),rewrite([54515(12)])].
54648 (A
* x) * (y * x) = x * ((A * y) * x).
[para(53970(a,1),691(a,1,2,2)),rewrite([54205(9),54569(8),53981(9)])].
54649
$F. [resolve(54648,a,621,a)].
==============================
end of proof ==========================
% Proof
1 at 11.85 (+ 0.08) seconds.
% Length
of proof is 184.
% Level
of proof is 27.
%
Maximum clause weight is 31.000.
% Given
clauses 720.
1 (z *
(x * A)) * z = (z * x) * (A * 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' *
(x * y) = y. [assumption].
11 (x *
x) * y = x * (x * y).
[assumption].
12 (x *
(y * x)) * z = x * (y * (x * z)).
[assumption].
13 (x *
y)' = x' * y'. [assumption].
14 A *
((x * y) * A) = (A * x) * (y * A).
[assumption].
15 (A *
x) * (y * A) = A * ((x * y) * A).
[copy(14),flip(a)].
16 (c1 *
(c2 * A)) * c1 != (c1 * c2) * (A * c1).
[deny(1)].
20 x \ 0
= x'. [para(4(a,1),7(a,1,2))].
21 x'' =
x.
[para(5(a,1),7(a,1,2)),rewrite([20(3)])].
22 x / x
= 0. [para(2(a,1),8(a,1,1))].
28 x \ y
= x' * y.
[para(6(a,1),10(a,1,2)),flip(a)].
29 x /
(y * x) = y'.
[para(10(a,1),8(a,1,1))].
31 x *
(x' * y) = y.
[back_rewrite(6),rewrite([28(1)])].
32 (x *
(x * y)) / y = x * x.
[para(11(a,1),8(a,1,1))].
35 (x *
(y * (x * z))) / z = x * (y * x).
[para(12(a,1),8(a,1,1))].
36 x *
((y / x) * (x * z)) = (x * y) * z.
[para(9(a,1),12(a,1,1,2)),flip(a)].
39 (x *
(y * (y * x))) * z = x * (y * (y * (x * z))). [para(11(a,1),12(a,1,1,2)),rewrite([11(7)])].
41 (x *
(y * (z * (y * x)))) * u = x * (y * (z * (y * (x * u)))).
[para(12(a,1),12(a,1,1,2)),rewrite([12(9)])].
43 (x *
y) * (x' * y') = 0.
[para(13(a,1),4(a,1,2))].
45 (x /
y)' * y' = x'.
[para(9(a,1),13(a,1,1)),flip(a)].
46 (x' *
y') * ((x * y) * z) = z.
[para(13(a,1),10(a,1,1))].
47 (A *
x) * A = A * (x * A).
[para(2(a,1),15(a,1,2)),rewrite([3(7)])].
48 A *
((A' * x) * A) = x * A.
[para(4(a,1),15(a,1,1)),rewrite([2(4)]),flip(a)].
50 (A *
((x * y) * A)) / (y * A) = A * x.
[para(15(a,1),8(a,1,1))].
59 (x /
y)' = y / x.
[para(9(a,1),29(a,1,2)),flip(a)].
60 x /
(y * (y * x)) = y' * y'.
[para(11(a,1),29(a,1,2)),rewrite([13(5)])].
63 (x /
y) * x' = y'.
[back_rewrite(45),rewrite([59(2)])].
66 A *
(((A' * x) * y) * A) = x * (y * A).
[para(31(a,1),15(a,1,1)),flip(a)].
68 (x /
y) * (y / x) = 0. [para(59(a,1),4(a,1,2))].
70 x' /
y' = y / x.
[para(63(a,1),8(a,1,1))].
72 ((x *
y) / z) * (x' * y') = z'.
[para(13(a,1),63(a,1,2))].
75 x /
x' = x * x.
[para(4(a,1),32(a,1,1,2)),rewrite([3(2)])].
83 (x *
y) / (x' * y) = x * x.
[para(31(a,1),32(a,1,1,2))].
91 x /
y' = y / x'.
[para(21(a,1),70(a,1,1))].
104 (x'
* y) / x = x' * (y * x').
[para(5(a,1),35(a,1,1,2,2)),rewrite([3(3)])].
106 ((x
/ y) * (z * x)) / y = (x / y) * (z * (x / y)). [para(9(a,1),35(a,1,1,2,2))].
107 x *
((y / (x * z)) * x) = (x * y) / z.
[para(9(a,1),35(a,1,1,2)),flip(a)].
114 (x *
(A * ((y * x) * A))) / A = x * ((A * y) * x). [para(15(a,1),35(a,1,1,2))].
120 (x *
y) / z' = z / (x' * y').
[para(13(a,1),91(a,1,2)),flip(a)].
122 (x'
/ y) * (x / y') = 0.
[para(91(a,1),68(a,1,2))].
133 ((x
* y) * z) / (x' * y') = (x * y) * (z * (x * y)). [para(43(a,1),35(a,1,1,2,2)),rewrite([3(3)])].
135 (x *
y) * x' = x * (y / x).
[para(4(a,1),36(a,1,2,2)),rewrite([3(3)]),flip(a)].
136 (x'
* y) * x = x' * (y / x').
[para(5(a,1),36(a,1,2,2)),rewrite([3(5)]),flip(a)].
138 (x /
y) * ((z / (x / y)) * x) = ((x / y) * z) * y. [para(9(a,1),36(a,1,2,2))].
139 (x /
y) * (y * z) = y' * ((y * x) * z).
[para(36(a,1),10(a,1,2)),flip(a)].
140 (x'
* y) * (x * z) = x' * ((y / x') * z).
[para(10(a,1),36(a,1,2,2)),flip(a)].
144 x' *
((x / ((x' * y') * (x / y))) * z) = (y / x) * ((x * y) * z).
[para(36(a,1),12(a,2,2)),rewrite([139(4),140(7),91(6),13(5),13(3),59(6
)])].
147 (x *
y) * (x' * z) = x * ((y / x) * z).
[para(31(a,1),36(a,1,2,2)),flip(a)].
152 x /
A' = x * A.
[back_rewrite(48),rewrite([136(6),31(8)])].
158 (x *
A') * A = x.
[para(152(a,1),8(a,1))].
159 (x *
A) * A' = x.
[para(152(a,1),9(a,1,1))].
163 A' /
x = x' * A'.
[para(152(a,1),59(a,1,1)),rewrite([13(3)]),flip(a)].
165 (x *
(x * A')) * A = x * x.
[para(152(a,1),32(a,1))].
166 A /
x = x' * A.
[para(152(a,1),70(a,1)),flip(a)].
169 x /
A = x * A'.
[para(158(a,1),8(a,1,1))].
171 A *
((x * (y * A')) * A) = (A * x) * y.
[para(158(a,1),15(a,1,2)),flip(a)].
172 ((x
* A') * x) * A' = (x * A') * (x * A').
[para(158(a,1),32(a,1,1,2)),rewrite([169(6)])].
173 ((x
* A') * (y * x)) * A' = (x * A') * (y * (x * A')). [para(158(a,1),35(a,1,1,2,2)),rewrite([169(7)])].
175 (x *
(A * ((y * x) * A))) * A' = x * ((A * y) * x). [back_rewrite(114),rewrite([169(8)])].
177 (x *
(x * A)) * A' = x * x.
[para(11(a,1),159(a,1,1))].
227 (x *
(y * (z * (z * (y * x))))) * u = x * (y * (z * (z * (y * (x * u))))).
[para(39(a,1),12(a,1,1,2)),rewrite([39(11)])].
279 (x *
(y * (z * (u * (z * (y * x)))))) * w = x * (y * (z * (u * (z * (y * (x *
w)))))).
[para(41(a,1),12(a,1,1,2)),rewrite([41(13)])].
296 (x *
(y * (z * (u * (z * (y * (x * w))))))) / w = x * (y * (z * (u * (z * (y *
x))))).
[para(41(a,1),35(a,1,1,2)),rewrite([41(13)])].
391 x /
(x' * (x / y)) = x * y.
[para(135(a,1),8(a,1,1)),rewrite([91(4),13(3),59(3)])].
392 (x /
y) * (y / (x / y)) = x * (y / x).
[para(9(a,1),135(a,1,1)),rewrite([59(2)]),flip(a)].
421 (A *
x) * x = A * (x * x).
[para(165(a,1),15(a,2,2)),rewrite([158(7)])].
431 (A *
(x * x)) / x = A * x.
[para(421(a,1),8(a,1,1))].
458 (A *
A) / (x * A) = A * x'.
[para(5(a,1),50(a,1,1,2,1)),rewrite([2(4)])].
469 (A *
(A * (x * (A * A)))) / (A * A) = A * (A * x). [para(47(a,1),50(a,1,1,2,1)),rewrite([12(7)])].
479 (A *
(x * (x * A))) / (A * A) = A * (x * (x * A')). [para(165(a,1),50(a,1,1,2,1)),rewrite([11(4)])].
503 (A'
* (x * A)) * A' = A' * x.
[para(391(a,1),163(a,1)),rewrite([21(6),163(7),13(10),13(10),21(7),21(8)]),flip(a)].
512 (A *
x) / (A' * (x' * A)) = A * (x * x).
[para(421(a,1),391(a,2)),rewrite([13(5),8(9),136(8),152(8)])].
514 (A *
A) / x = A * (x' * A).
[para(9(a,1),458(a,1,2)),rewrite([169(7),13(9),21(9)])].
527 A *
(x' * A') = x'.
[para(514(a,1),29(a,1)),rewrite([13(6),13(6),171(11),135(6),169(4)])].
528 x /
(A * A) = A' * (x * A').
[para(514(a,1),59(a,1,1)),rewrite([13(6),13(6),21(4)]),flip(a)].
530 x /
(A' * A') = A * (x * A).
[para(514(a,1),91(a,1)),rewrite([21(3),13(8)]),flip(a)].
541 A *
(x * (x * A')) = x * x.
[back_rewrite(479),rewrite([528(9),135(10),169(8),177(9),10(6)]),flip(a)].
542 A *
((x * (A * A)) * A') = A * (A * x).
[back_rewrite(469),rewrite([528(12),135(13),169(11),135(12),169(10),10(14)])].
569 A' *
(x * A) = x.
[para(527(a,1),13(a,1,1)),rewrite([21(2),13(7),21(4),21(5)]),flip(a)].
573 A *
(x * A') = x.
[para(21(a,1),527(a,1,2,1)),rewrite([21(7)])].
574 x /
(x * A) = A'.
[para(527(a,1),29(a,1,2)),rewrite([91(6),13(5),21(2),21(3)])].
585 x /
(A' * x') = A * (x * x).
[back_rewrite(512),rewrite([569(8),91(4),13(3)])].
586 A' *
x = x * A'.
[back_rewrite(503),rewrite([569(5)]),flip(a)].
588 A *
(A * x) = x * (A * A).
[back_rewrite(542),rewrite([586(8,R),31(9)]),flip(a)].
612 A' *
(x * (A * ((y * x) * A))) = x * ((A * y) * x). [back_rewrite(175),rewrite([586(9,R)])].
613 (x *
A') * (y * (x * A')) = A' * ((x * A') * (y * x)). [back_rewrite(173),rewrite([586(8,R)]),flip(a)].
614 (x *
A') * (x * A') = A' * ((x * A') * x).
[back_rewrite(172),rewrite([586(7,R)]),flip(a)].
625 A *
x = x * A.
[para(569(a,1),10(a,1,2)),rewrite([21(3)])].
627 A *
(x * (A' * x)) = x * x.
[para(569(a,1),12(a,2,2)),rewrite([625(6,R)])].
631 A' *
(x * x) = x * (A' * x).
[para(569(a,1),35(a,1,1,2)),rewrite([169(3),586(4,R)])].
647 A' *
(x * (A * (A * (y * x)))) = x * ((A * y) * x). [back_rewrite(612),rewrite([625(6,R)])].
704 A *
(A * ((A' * x) * y)) = x * (y * A).
[back_rewrite(66),rewrite([625(7,R)])].
711 (c1
* (A * c2)) * c1 != (c1 * c2) * (A * c1).
[back_rewrite(16),rewrite([625(4,R)])].
712 (A *
x) * (y * A) = A * (A * (x * y)).
[back_rewrite(15),rewrite([625(9,R)])].
716 x' *
(A * x) = A.
[para(625(a,2),10(a,1,2))].
717 A *
(x * x) = x * (x * A).
[para(625(a,2),11(a,1))].
718 A *
(x * x) = x * (A * x).
[para(625(a,2),11(a,2,2)),rewrite([625(3,R)])].
721 (A *
(A * x)) * y = A * (x * (A * y)).
[para(625(a,2),12(a,1,1,2))].
722 A *
(x * (y * x)) = x * (y * (x * A)).
[para(625(a,2),12(a,1))].
740 (x *
A) / (A' * x) = A * A.
[para(625(a,1),83(a,1,1))].
742 (x *
A) / (A * x') = x * x. [para(625(a,2),83(a,1,2))].
743 (A'
* x') * ((x * A) * y) = y.
[para(625(a,1),46(a,1,2,1))].
746 (A *
x) * x' = A.
[para(625(a,2),135(a,1,1)),rewrite([166(6),31(8)])].
747 (x *
A) * x = A * (x * x).
[para(625(a,1),421(a,1,1))].
800 (x *
A') * x = x * (x * A').
[para(573(a,1),421(a,1,1)),rewrite([614(12),31(13)]),flip(a)].
805 (x *
A') * (x * A') = A' * (x * (x * A')).
[back_rewrite(614),rewrite([800(13)])].
813 x *
(A' * x') = A'.
[para(716(a,1),13(a,1,1)),rewrite([21(4),13(5)]),flip(a)].
869 (A'
* x') * x = A'.
[para(746(a,1),13(a,1,1)),rewrite([13(5),21(8)]),flip(a)].
929 (x *
(x * A')) * y = x * (A' * (x * y)).
[para(586(a,1),12(a,1,1,2))].
1044 (x
* (A * A)) / (A * x) = A.
[para(588(a,1),8(a,1,1))].
1056 (A
* x) / (x * (A * A)) = A'.
[para(588(a,1),29(a,1,2))].
1089 x /
(x * (A * A)) = A' * A'.
[para(588(a,1),60(a,1,2))].
1111
((x' * y) / z) * (x * y') = z'.
[para(21(a,1),72(a,1,2,1))].
1165 (A
* (x * x)) / (x * A) = x.
[para(717(a,2),8(a,1,1))].
1208 (x
* (x * A)) / x = A * x.
[para(717(a,1),431(a,1,1))].
1223 (A
* (x * x)) / (A * x) = x.
[para(718(a,2),8(a,1,1))].
1395 (x
* (A * A)) / (x * A) = A.
[para(625(a,1),1044(a,1,2))].
1540 (x
* (x * A')) / x = x * A'.
[para(9(a,1),1165(a,1,2)),rewrite([169(3),169(6),805(8),31(9),169(7)])].
1566 (x
* A') * (A * x') = 0.
[para(1208(a,1),122(a,1,2)),rewrite([13(6),21(2),13(4),21(2),1540(5)])].
1675 ((x
* A') * y) / (A * x') = A' * ((x * A') * (y * x)). [para(1566(a,1),35(a,1,1,2,2)),rewrite([3(5),613(16)])].
1908 (A
* x') * (x * x) = A * x. [para(742(a,1),135(a,2,2)),rewrite([712(6),5(4),3(4),13(7),21(7),11(7),31(6)]),flip(a)].
2175 (A'
* x') / x = x' * (A' * x').
[para(586(a,2),104(a,1,1))].
2361 (A
* x) / (x * x) = A * x'.
[para(1908(a,1),8(a,1,1))].
2368 (x
* x) / (A * x) = A' * x.
[para(1908(a,1),29(a,1,2)),rewrite([13(8),21(8)])].
2389 (x
* y) * (x * y) = x * (y * (y * x)).
[para(75(a,1),107(a,2)),rewrite([13(2),31(4),75(2),11(2)]),flip(a)].
2406 A *
(A * (x / (A * y))) = (A * x) / y.
[para(107(a,1),625(a,1)),rewrite([625(8,R),625(10,R)]),flip(a)].
2408 (A
* x) / y = (x * A) / y.
[para(625(a,1),107(a,2,1)),rewrite([625(6,R),2406(7)])].
2426 (x
* y) / (A' * x') = x * ((y * A) * x).
[para(813(a,1),107(a,1,2,1,2)),rewrite([152(3)]),flip(a)].
2568 (x
* A) / (A * x) = 0.
[para(2408(a,1),22(a,1))].
2569 (A
* x) / (x * A) = 0.
[para(2408(a,2),22(a,1))].
2572 x /
(A * y) = x / (y * A).
[para(2408(a,1),59(a,1,1)),rewrite([59(4)]),flip(a)].
2655 (x
* (y * A)) / (A * y) = x.
[para(2568(a,1),106(a,1,1,1)),rewrite([2(5),2568(11),2568(12),3(9),2(8)])].
2664 (x
/ (A * y)) * (y * A) = x.
[para(2572(a,2),9(a,1,1))].
2790 x *
(A * y) = x * (y * A).
[para(2655(a,1),9(a,1,1))].
3090 (x
* A) / (x * x) = A * x'.
[para(625(a,1),2361(a,1,1))].
3171 (A'
* x) * (x * A) = x * x.
[para(2368(a,1),2664(a,1,1))].
3348 A *
(x * ((A' * x) * (x * (A * y)))) = (A * (x * (x * x))) * y.
[para(3171(a,1),41(a,1,1,2,2)),flip(a)].
3432 (x
* x) / (A' * x) = A * x.
[para(120(a,2),2361(a,1)),rewrite([13(5),21(5),21(8)])].
3439 (x
* x) / (x * A') = A * x.
[para(120(a,2),3090(a,1)),rewrite([13(5),21(3),21(8)])].
3473 (A'
* x) / (x * x) = A' * x'.
[para(3432(a,1),59(a,1,1)),rewrite([13(3)]),flip(a)].
3485 (A
* x) * (x * A') = x * x.
[para(3439(a,1),9(a,1,1))].
3543 (A
* x) * (x * x) = A * (x * (x * x)).
[para(3485(a,1),11(a,2,2)),rewrite([2389(5),39(9),573(6)]),flip(a)].
3873 (A'
* x) * (y * (A' * x)) = A' * ((x * A') * (y * x)).
[para(586(a,1),133(a,1,1,1)),rewrite([21(7),1675(8)]),flip(a)].
4027 (A'
* (x * x)) * y = x * (A' * (x * y)).
[para(631(a,2),12(a,1,1))].
4231 (A
* x) * y = (x * A) * y.
[para(743(a,1),10(a,1,2)),rewrite([13(5),21(3),21(3)])].
4317 (x
* A) * (A * y) = A * (A * (x * y)).
[para(4231(a,1),2790(a,1)),rewrite([712(10)])].
4426 (A'
* x) * (y * A) = A' * ((x * A) * y).
[para(574(a,1),138(a,1,1)),rewrite([574(5),152(5),574(9)]),flip(a)].
4438 A *
((x * A') * (y * (A * A))) = (A * x) * (A * y).
[para(1044(a,1),138(a,1,1)),rewrite([1044(8),169(3),1044(17)])].
4443 (A
* x) * (A * y) = A * (A * (x * y)).
[para(1395(a,1),138(a,1,1)),rewrite([1395(8),169(3),4438(10),1395(12),712(10)])].
4463 (A'
* x) * (y * (A * A)) = A * (x * y).
[para(1056(a,1),138(a,1,1)),rewrite([1056(9),152(5),4317(7),10(8),1056(10)]),flip(a)].
4626 (x
* A') * (A * y) = A' * ((A * x) * y).
[para(169(a,1),139(a,1,1))].
4698 (A
* x') * (x * (x * y)) = x * (y * A).
[para(740(a,1),139(a,1,1)),rewrite([11(8),704(8),13(7),21(6),4426(12),747(11),10(12),11(8)]),fl
ip(a)].
4723 A'
* (x * (A * (A * y))) = (x * A) * y.
[para(2569(a,1),139(a,1,1)),rewrite([2(5),13(6),4317(12),721(13),11(12),4626(14),4698(13),625(9
,R)]),flip(a)].
4815 (x
* A) * (y * x) = x * ((A * y) * x).
[back_rewrite(647),rewrite([4723(9)])].
5010 (A'
* x') * (x * y) = x' * ((x * A') * y).
[para(586(a,2),140(a,1,1)),rewrite([163(11),21(9)])].
5523 (A
* x) * ((A' * x) * y) = A * (x * (A' * (x * y))).
[para(869(a,1),144(a,2,2,1)),rewrite([13(5),21(3),21(3),13(11),21(9),21(9),746(10)
,2175(12),627(14),3473(10),21(6),585(12),147(14),169(11),586(12,R),4027(13)])].
5927 A *
(x * (x * (x * (A * ((A' * x') * y))))) = (A * x) * (x * y).
[para(1223(a,1),147(a,2,2,1)),rewrite([4443(6),13(9),721(12),12(11)])]
.
5951 (A
* (x * (x * x))) * ((A' * x') * y) = A * (x * (A' * (x * y))).
[para(2368(a,1),147(a,2,2,1)),rewrite([3543(4),13(7),5523(17)])].
6022 A'
* (x * (A * y)) = A * ((A' * x) * y).
[para(1089(a,1),138(a,1,1)),rewrite([1089(10),530(11),12(10),11(11),10(10),1089(11),11(12),446
3(17)])].
8433 A *
(x * ((A' * x) * y)) = x * (x * y).
[para(569(a,1),227(a,1,1,2,2,2)),rewrite([627(6),11(2),6022(11),10(12)]),flip(a)].
8754 (A
* (x * (x * x))) * y = x * (x * (x * (A * y))). [back_rewrite(3348),rewrite([8433(10)]),flip(a)].
8766 x *
(x * (x * (A * ((A' * x') * y)))) = A * (x * (A' * (x * y))).
[back_rewrite(5951),rewrite([8754(10)])].
8778 A *
(A * (x * (A' * (x * y)))) = (A * x) * (x * y). [back_rewrite(5927),rewrite([8766(11)])].
13078 A
* (x * (A' * A')) = A' * x.
[para(1044(a,1),1111(a,1,1)),rewrite([13(5),13(12),21(12)])].
14760 A
* ((A' * x) * (y * (A * (x * (A' * z))))) = (A * ((A' * x) * (y * x))) *
z.
[para(573(a,1),279(a,1,1,2,2,2,2)),rewrite([6022(7),6022
(21)]),flip(a)].
17096 A
* ((A' * x) * (y * x)) = A * (x * ((A' * y) * x)). [para(13078(a,1),296(a,1,1,2,2,2,2)),rewrite([6022(10),3873(9),31(10),91(8),13(7)
,13(5),21(5),13(6),4815(8),166(9),13(8),21(2),13(6),13(4),21(4),21(5),625(7,R),573(15),6022(14)]),flip(a)].
17097 A'
* ((x * A') * (y * x)) = A' * (x * ((A' * y) * x)). [para(13078(a,1),296(a,2,2,2,2,2)),rewrite([11(13),11(19),6022(18),14760(18),17
096(9),147(13),169(10),586(11,R),10(14),8(10),11(21),6022(20),3873(19),31(20)]),flip(a)].
17170 (x
* A') * (y * (x * A')) = A' * (x * ((A' * y) * x)). [back_rewrite(613),rewrite([17097(16)])].
18109 (A
* x) * (x * y) = x * (x * (y * A)).
[para(541(a,1),712(a,1,1)),rewrite([11(4),929(11),8778(13)]),flip(a)].
18758 (x
* A') * (y * x) = x * ((A' * y) * x).
[para(9(a,1),722(a,2,2,2)),rewrite([169(3),169(6),17170(9),31(10),169(7)]),flip(a)].
31944 (x
* (x * (y * A))) / (x * y) = A * x.
[para(18109(a,1),8(a,1,1))].
34941 (x
* (x * (A * y))) / (x * y) = A * x.
[para(625(a,2),31944(a,1,1,2,2))].
36284 (x
* y) / (x * (x * (A * y))) = A' * x'.
[para(34941(a,1),59(a,1,1)),rewrite([13(3)]),flip(a)].
36296 (x
* (A * y)) * x = (x * y) * (A * x).
[para(34941(a,1),392(a,2,2)),rewrite([36284(6),36284(14),2426(13),625(9,R),5010(12),18758(11),1
0(9),10(7)])].
36297
$F. [resolve(36296,a,711,a)].
==============================
end of proof ==========================
% Proof
1 at 0.22 (+ 0.01) seconds.
% Length
of proof is 47.
% Level
of proof is 15.
%
Maximum clause weight is 19.000.
% Given
clauses 159.
1 A * (x
* (A * y)) = ((A * x) * A) * y # label(non_clause) # label(goal). [goal].
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' *
(x * y) = y. [assumption].
11 (x *
x) * y = x * (x * y).
[assumption].
12 (x *
(y * x)) * z = x * (y * (x * z)).
[assumption].
13 (x *
y)' = x' * y'. [assumption].
14 x *
(A * (x * y)) = ((x * A) * x) * y.
[assumption].
15 ((x *
A) * x) * y = x * (A * (x * y)).
[copy(14),flip(a)].
16 ((A *
c1) * A) * c2 != A * (c1 * (A * c2)).
[deny(1)].
20 x \ 0
= x'. [para(4(a,1),7(a,1,2))].
21 x'' =
x.
[para(5(a,1),7(a,1,2)),rewrite([20(3)])].
28 x \ y
= x' * y.
[para(6(a,1),10(a,1,2)),flip(a)].
29 x /
(y * x) = y'.
[para(10(a,1),8(a,1,1))].
31 x *
(x' * y) = y.
[back_rewrite(6),rewrite([28(1)])].
32 (x *
(x * y)) / y = x * x.
[para(11(a,1),8(a,1,1))].
35 (x *
(y * (x * z))) / z = x * (y * x).
[para(12(a,1),8(a,1,1))].
36 x *
((y / x) * (x * z)) = (x * y) * z.
[para(9(a,1),12(a,1,1,2)),flip(a)].
45 (x /
y)' * y' = x'.
[para(9(a,1),13(a,1,1)),flip(a)].
47 (x *
A) * x = x * (A * x).
[para(15(a,1),3(a,1)),rewrite([3(3)]),flip(a)].
51 (x /
y)' = y / x.
[para(9(a,1),29(a,1,2)),flip(a)].
54 (x /
y) * x' = y'.
[back_rewrite(45),rewrite([51(2)])].
59 x' /
y' = y / x.
[para(54(a,1),8(a,1,1))].
60 x' *
((x / y) * (x' * z)) = (x' * y') * z.
[para(54(a,1),12(a,1,1,2)),flip(a)].
64 x /
x' = x * x.
[para(4(a,1),32(a,1,1,2)),rewrite([3(2)])].
78 x /
y' = y / x'.
[para(21(a,1),59(a,1,1))].
93 x *
((y / (x * z)) * x) = (x * y) / z.
[para(9(a,1),35(a,1,1,2)),flip(a)].
124 (x'
* y) * (x * z) = x' * ((y / x') * z).
[para(10(a,1),36(a,1,2,2)),flip(a)].
138 (x *
(A * x)) / x = x * A.
[para(47(a,1),8(a,1,1))].
200 x /
(x * (A' * x)) = x' * A.
[para(138(a,1),78(a,1)),rewrite([13(9),21(5),13(7),21(7)]),flip(a)].
753 (x /
y) * (x' * z) = x * ((x' * y') * z).
[para(60(a,1),10(a,1,2)),rewrite([21(2)]),flip(a)].
787 x' *
(A * ((A' * x) * x)) = x.
[para(200(a,1),9(a,1,1)),rewrite([124(8),753(8),21(6)])].
1507 A *
((A' * x) * x) = x * x.
[para(787(a,1),10(a,1,2)),rewrite([21(2)]),flip(a)].
1525 (A'
* x) * x = A' * (x * x).
[para(1507(a,1),10(a,1,2)),flip(a)].
1947 (A'
* (x * x)) / x = A' * x.
[para(1525(a,1),8(a,1,1))].
2442 (x
* y) * (x * y) = x * (y * (y * x)).
[para(64(a,1),93(a,2)),rewrite([13(2),31(4),64(2),11(2)]),flip(a)].
2919 (x
* (x * A)) / (A * x) = x.
[para(10(a,1),1947(a,2)),rewrite([2442(7),10(8)])].
2934 x *
(A * x) = x * (x * A).
[para(2919(a,1),9(a,1,1))].
2969 A *
x = x * A. [para(2934(a,1),10(a,1,2)),rewrite([10(5)]),flip(a)].
3167 (A
* (A * c1)) * c2 != A * (c1 * (A * c2)).
[back_rewrite(16),rewrite([2969(5,R)])].
3273 (A
* (A * x)) * y = A * (x * (A * y)).
[para(2969(a,2),12(a,1,1,2))].
3274
$F. [resolve(3273,a,3167,a)].
==============================
end of proof ==========================