% Proof 1 at 110.75 (+ 0.45) seconds.
% Length of proof is 124.
% Level of proof is 14.
% Maximum clause weight is 27.000.
% Given clauses 2212.
3 R(R(R(x,y,C),y,C),y,C) = x # label(non_clause)
# label(goal). [goal].
4 0 * x = x. [assumption].
5 x * 0 = x. [assumption].
6 x * (x \ y) = y. [assumption].
8 (x * y) / y = x. [assumption].
9 (x / y) * y = x. [assumption].
10 ((x * y) * x) * z = x * (y * (x * z)). [assumption].
11 ((x * y) * z) * y = x * (y * (z * y)). [assumption].
12 (x * y) * (z * x) = x * ((y * z) * x). [assumption].
15 x' * (x * y) = y. [assumption].
16 (x * y) * y' = x. [assumption].
17 C * x = x * C. [assumption].
18 R(x,y,z) = ((x * y) * z) * (y * z)'. [assumption].
19 ((x * y) * z) * (y * z)' = R(x,y,z). [copy(18),flip(a)].
22 R(R(R(c5,c6,C),c6,C),c6,C) != c5. [deny(3)].
27 x / (y \ x) = y. [para(6(a,1),8(a,1,1))].
29 (x * x) * y = x * (x * y).
[para(4(a,1),10(a,2,2)),rewrite([5(2)])].
30 (x * y) * x = x * (y * x). [para(10(a,1),5(a,1)),rewrite([5(2)]),flip(a)].
32 x * ((x \ y) * (x * z)) = (y * x) * z. [para(6(a,1),10(a,1,1,1)),flip(a)].
40 (x * (y * (x * (x * y)))) * z = (x * y) * (x *
((x * y) * z)).
[para(10(a,1),10(a,1,1))].
44 (x * (y * x)) * z = x * (y * (x * z)). [back_rewrite(10),rewrite([30(2)])].
48 (x * y) * y = x * (y * y).
[para(4(a,1),11(a,2,2,2)),rewrite([5(3)])].
65 (x * y) * (z * (x * (u * x))) = x * ((y * ((z
* x) * u)) * x).
[para(11(a,1),12(a,1,2))].
70 x' * x = 0. [para(5(a,1),15(a,1,2))].
71 x \ y = x' * y. [para(6(a,1),15(a,1,2)),flip(a)].
73 x / (y * x) = y'. [para(15(a,1),8(a,1,1))].
77 x' * (((x * y) * z) * x') = y * (z * x'). [para(15(a,1),12(a,1,1)),flip(a)].
85 x * ((x' * y) * (x * z)) = (y * x) * z. [back_rewrite(32),rewrite([71(1)])].
87 x'' = x.
[back_rewrite(27),rewrite([71(1),73(3)])].
88 x * (x' * y) = y. [back_rewrite(6),rewrite([71(1)])].
89 x * x' = 0. [para(4(a,1),16(a,1,1))].
92 x / y = x * y'. [para(9(a,1),16(a,1,1)),flip(a)].
93 (x * y) * (y' * (z * y')) = (x * z) * y'. [para(16(a,1),11(a,1,1,1)),flip(a)].
96 x' * ((y * (z * x)) * x') = (x' * y) * z. [para(16(a,1),12(a,1,2)),flip(a)].
98 (x * y)' * x = y'. [para(16(a,1),15(a,1,2))].
99 x * (y * x)' = y'. [para(15(a,1),16(a,1,1))].
105 (x * y') * y = x. [back_rewrite(9),rewrite([92(1)])].
107 (C * (x * y)) * y = x * (y * (y * C)).
[para(17(a,1),11(a,2,2,2)),rewrite([17(3,R)])].
109 C * ((C * x) * y) = x * (C * (y * C)).
[para(17(a,2),11(a,1,1,1)),rewrite([17(5,R)])].
110 x * (y * (C * y)) = x * (y * (y * C)). [para(17(a,2),11(a,1,1)),rewrite([107(4)]),flip(a)].
117 C' * (x * C) = x. [para(17(a,1),15(a,1,2))].
118 x' * (C * x) = C. [para(17(a,2),15(a,1,2))].
132 (x * ((y * z) * (x * u))) * ((z * x) * u)' =
R(x * y,z * x,u).
[para(12(a,1),19(a,1,1,1)),rewrite([44(4)])].
138 R(x,y,z) * (y * z) = (x * y) * z.
[para(19(a,1),16(a,1,1)),rewrite([87(4)])].
141 ((x * (y * z)) * z') * y' = R(x,y *
z,z').
[para(16(a,1),19(a,1,2,1))].
146 (C * (x * y)) * (C * y)' = R(x,y,C).
[para(17(a,2),19(a,1,2,1)),rewrite([17(3,R)])].
164 R(x,y,x * y) = x. [para(29(a,1),19(a,1)),rewrite([99(6),16(3)]),flip(a)].
166 x' * ((x * y) * x') = y * x'.
[para(70(a,1),12(a,1,1)),rewrite([4(4)]),flip(a)].
176 (x * (y * (x * z))) * (x * z)' = R(x *
y,x,z).
[para(30(a,1),19(a,1,1,1)),rewrite([44(3)])].
178 ((x * (y * z)) * y) * (y * (z * y))' = R(x,y
* z,y).
[para(30(a,1),19(a,1,2,1))].
182 x * ((x' * y) * x) = y * x.
[para(89(a,1),12(a,1,1)),rewrite([4(3)]),flip(a)].
183 (x * y)' = y' * x'. [para(89(a,1),12(a,2,2)),rewrite([98(3),99(4),5(7)]),flip(a)].
187 R(x,y * z,z') = R(x,y * z,y).
[back_rewrite(178),rewrite([183(6),183(5),30(8),93(9),141(6)])].
188 (x * (y * (x * z))) * (z' * x') = R(x *
y,x,z).
[back_rewrite(176),rewrite([183(5)])].
194 (C * (x * y)) * (y' * C') = R(x,y,C). [back_rewrite(146),rewrite([183(6)])].
204 (x * ((y * z) * (x * u))) * (u' * (x' * z'))
= R(x * y,z * x,u).
[back_rewrite(132),rewrite([183(7),183(7)])].
214 ((x * y) * z) * (z' * y') = R(x,y,z). [back_rewrite(19),rewrite([183(4)])].
227 (x * (x * (y * x))) * z = x * ((x * y) * (x *
z)).
[para(16(a,1),40(a,1,1,2,2,2)),rewrite([30(4),65(6),182(4),30(2),16(7),16(8)])].
258 (x * (y * (y * x))) * z = x * (y * (y * (x *
z))).
[para(29(a,1),44(a,1,1,2)),rewrite([29(7)])].
273 x * (C * x') = C. [para(17(a,2),88(a,1,2))].
318 C * (x * C') = x. [para(105(a,1),17(a,2))].
319 (x' * C) * x = C. [para(17(a,1),105(a,1,1))].
334 x * (C' * x') = C'. [para(117(a,1),16(a,1,1)),rewrite([183(3)])].
336 C' * x = x * C'. [para(117(a,1),30(a,1,1)),rewrite([16(10)]),flip(a)].
340 C * (x * (C' * x)) = x * x.
[para(117(a,1),44(a,2,2)),rewrite([17(6,R)])].
441 (x * (C * C)) * y = C * (x * (C * y)).
[para(273(a,1),40(a,1,1,2,2,2)),rewrite([12(6),70(3),4(4),273(9),273(10)])].
490 C' * (x * (C * C)) = x * C. [para(48(a,1),117(a,1,2))].
497 C * (x * (C' * C')) = x * C'. [para(48(a,1),318(a,1,2))].
506 (C * x) * y = (x * C) * y.
[para(319(a,1),44(a,1,1,2)),rewrite([85(9)]),flip(a)].
621 (x' * C') * x = C'. [para(336(a,1),105(a,1,1))].
738 (x * y) * ((y' * x') * z) = z. [para(183(a,1),88(a,1,2,1))].
757 (x * (C' * C')) * y = C' * (x * (C' *
y)).
[para(334(a,1),40(a,1,1,2,2,2)),rewrite([12(8),70(4),4(6),334(12),334(14)])].
1090 (C' * x) * y = (x * C') * y.
[para(621(a,1),44(a,1,1,2)),rewrite([85(11)]),flip(a)].
1218 (x * y) * x' = x * (y * x').
[para(29(a,1),77(a,1,2,1)),rewrite([166(6)])].
1225 (x * (y * z)) * y' = (x * y) * (z *
y').
[para(44(a,1),77(a,1,2,1)),rewrite([1218(6),15(7)])].
1555 (x * y') * (y * z) = y' * ((y * x) *
z). [para(15(a,1),85(a,1,2,2)),rewrite([87(3)]),flip(a)].
1570 (x * y) * (x' * z) = x * ((y * x') *
z).
[para(85(a,1),88(a,1,2)),rewrite([87(6)]),flip(a)].
1571 (x * y) * (y' * z) = y * ((y' * x) *
z).
[para(88(a,1),85(a,1,2,2)),flip(a)].
1583 (x * y) * (C * y') = y * (C * (y' *
x)).
[para(273(a,1),85(a,1,2,2)),rewrite([17(4,R)]),flip(a)].
1586 (x * C) * (y * C') = C * ((C' * x) *
y).
[para(318(a,1),85(a,1,2,2)),flip(a)].
1602 (x * y) * (C' * y') = y * (C' * (y' *
x)).
[para(334(a,1),85(a,1,2,2)),rewrite([336(5,R)]),flip(a)].
1665 x * ((x' * (y * z)) * z') = R(y,z,x). [back_rewrite(214),rewrite([1571(6)])].
1798 (C * x) * ((C' * x') * y) = y.
[para(506(a,2),88(a,1)),rewrite([183(5)])].
1862 (x * (y * z)) * z' = z * ((z' * x) *
y).
[para(96(a,1),15(a,1,2)),rewrite([87(2)]),flip(a)].
1889 C * (C * (x * (C' * y))) = (C * x) * y.
[para(336(a,2),96(a,1,2,1,2)),rewrite([87(3),87(8),17(7,R),87(11)])].
1922 x * (y * ((y' * x') * z)) = R(z,y,x).
[back_rewrite(1665),rewrite([1862(5)])].
1930 R(x,y * z,z') = R(x,z,y).
[back_rewrite(141),rewrite([1862(4),1862(6),1571(5),1922(6)]),flip(a)].
1941 R(x,y * z,y) = R(x,z,y).
[back_rewrite(187),rewrite([1930(3)]),flip(a)].
2261 R(x,C * y,y) = R(x,C,y). [para(17(a,2),1941(a,1,2))].
2269 R(x,C,y) = R(x,y,C').
[para(117(a,1),1941(a,1,2)),rewrite([1930(8)]),flip(a)].
2270 R(x,C,y') = R(x,y,C).
[para(118(a,1),1941(a,1,2)),rewrite([1930(7)])].
2279 R(x,C' * y,y) = R(x,C',y). [para(336(a,2),1941(a,1,2))].
2762 R(R(R(c5,C,c6'),c6,C),c6,C) != c5. [para(2270(a,2),22(a,1,1,1))].
2766 R(x,y * z,C) = R(x,C,z' * y'). [para(183(a,1),2270(a,1,3)),flip(a)].
2914 R(R(R(c5,C,c6'),C,c6'),c6,C) != c5. [para(2270(a,2),2762(a,1,1))].
3066 R(R(R(c5,C,c6'),C,c6'),C,c6') != c5. [para(2270(a,2),2914(a,1))].
3250 (C * x) * (x * y) = x * (x * (y * C)).
[para(340(a,1),12(a,1,1)),rewrite([29(4),44(10),17(12,R),1889(13)]),flip(a)].
3502 C' * (x * (C * y)) = C * ((C' * x) *
y).
[para(490(a,1),12(a,1,1)),rewrite([1586(6),441(13),336(16,R),15(16)]),flip(a)].
3506 C' * (x * (y * C)) = C * ((C' * x) *
y).
[para(490(a,1),44(a,2,2,2)),rewrite([44(11),3502(9),17(8,R),88(8),3502(6)]),flip(a)].
3851 (x * y) * (x * y) = x * (y * (x * y)). [para(164(a,1),138(a,1,1)),flip(a)].
3852 C * R(x,y,C * y') = y * (C * (y' * x)). [para(273(a,1),138(a,1,2)),rewrite([17(6,R),1583(11)])].
3868 C' * R(x,y,C' * y') = y * (C' * (y' *
x)).
[para(334(a,1),138(a,1,2)),rewrite([336(8,R),1602(14)])].
4501 R(x,y,z * y') = R(x,z,y'). [para(105(a,1),1930(a,1,2)),flip(a)].
4502 R(x,C',y') = R(x,C,y). [para(117(a,1),1930(a,1,2)),rewrite([183(3),4501(5),1930(9)])].
4506 R(x,C,y' * C) = R(x,C',y).
[para(336(a,2),1930(a,1,2)),rewrite([87(6),2766(5),87(5)])].
4529 R(x,C,y * C) = R(x,C,y). [para(1930(a,1),2269(a,2))].
4588 x * (C' * (x' * y)) = C' * R(y,C,x).
[back_rewrite(3868),rewrite([4501(7),4502(6)]),flip(a)].
4589 x * (C * (x' * y)) = C * R(y,C,x').
[back_rewrite(3852),rewrite([4501(5)]),flip(a)].
4592 R(x,C',y) = R(x,C,y').
[back_rewrite(4506),rewrite([4529(5)]),flip(a)].
4653 (x * y) * (C * y') = C * R(x,C,y').
[back_rewrite(1583),rewrite([4589(10)])].
4668 R(x,C' * y,y) = R(x,C,y').
[back_rewrite(2279),rewrite([4592(7)])].
5295 x * R(y,C,x') = R(x * y,x,C).
[para(336(a,1),188(a,1,2)),rewrite([1570(9),1225(5),4653(5),336(8,R),15(8)])].
5298 C * R(x,C,y) = R(C * x,C,y).
[para(336(a,2),188(a,1,2)),rewrite([1570(10),336(7,R),3502(7),1862(9),1571(8),1922(9)])].
5449 (x * y) * (C * y') = R(C * x,C,y').
[back_rewrite(4653),rewrite([5298(10)])].
5471 x * (C * (x' * y)) = R(C * y,C,x').
[back_rewrite(4589),rewrite([5298(10)])].
5572 C * R(x,y,C) = R(C * x,C,y').
[para(194(a,1),109(a,1,2)),rewrite([17(12,R),318(12),5449(9)])].
6714 x * R(y,C,x) = R(x * y,C,x). [para(2261(a,1),204(a,2)),rewrite([1570(12),1225(6),89(5),5(5),1571(8),336(7,R),3506(7),1922(8)])].
9162 (x * (y * (x * y))) * z = (x * y) * ((x * y)
* z).
[para(738(a,1),227(a,1,1,2)),rewrite([3851(3),1571(10),16(9),89(7),4(9)])].
9255 (C' * x) * ((C' * x) * y) = x * (C' * (C' *
(x * y))).
[para(1090(a,1),29(a,1,1)),rewrite([12(7),29(6),258(8)]),flip(a)].
10804 R(R(x,C,y),C,y') = x.
[para(110(a,1),1798(a,1,1)),rewrite([183(11),183(10),30(13),9162(15),9255(15),258(16),5471(14),88(11),5295(10),4
588(7),5572(9),88(7)])].
36358 C' * R(x,C,y) = R(x * C',C,y).
[para(497(a,1),188(a,2,1)),rewrite([757(10),15(8),88(6),1571(6),336(5,R),4588(6)])].
36411 x * (C' * (x' * y)) = R(y * C',C,x).
[back_rewrite(4588),rewrite([36358(11)])].
72380 R(R(x,C,y),C,y) = R(x,C,y'). [para(4668(a,1),1922(a,2)),rewrite([183(7),87(7),30(8),44(9),1571(10),1555(9),3250(8),36411(10),336(7,R),
3506(7),6714(10),1922(8)])].
72512 $F.
[back_rewrite(3066),rewrite([72380(9),87(5),10804(8)]),xx(a)].
============================== end of proof
==========================
% Proof
2 at 110.75 (+ 0.45) seconds.
% Length
of proof is 127.
% Level
of proof is 15.
%
Maximum clause weight is 27.000.
% Given
clauses 2212.
2
R(R(R(x,C,y),C,y),C,y) = x # label(non_clause) # label(goal). [goal].
4 0 * x
= x. [assumption].
5 x * 0 =
x. [assumption].
6 x * (x
\ y) = y. [assumption].
8 (x *
y) / y = x. [assumption].
9 (x /
y) * y = x. [assumption].
10 ((x *
y) * x) * z = x * (y * (x * z)).
[assumption].
11 ((x *
y) * z) * y = x * (y * (z * y)).
[assumption].
12 (x *
y) * (z * x) = x * ((y * z) * x).
[assumption].
15 x' *
(x * y) = y. [assumption].
16 (x *
y) * y' = x. [assumption].
17 C * x
= x * C. [assumption].
18
R(x,y,z) = ((x * y) * z) * (y * z)'.
[assumption].
19 ((x *
y) * z) * (y * z)' = R(x,y,z).
[copy(18),flip(a)].
21
R(R(R(c3,C,c4),C,c4),C,c4) != c3.
[deny(2)].
27 x /
(y \ x) = y.
[para(6(a,1),8(a,1,1))].
29 (x *
x) * y = x * (x * y).
[para(4(a,1),10(a,2,2)),rewrite([5(2)])].
30 (x *
y) * x = x * (y * x).
[para(10(a,1),5(a,1)),rewrite([5(2)]),flip(a)].
32 x *
((x \ y) * (x * z)) = (y * x) * z.
[para(6(a,1),10(a,1,1,1)),flip(a)].
40 (x *
(y * (x * (x * y)))) * z = (x * y) * (x * ((x * y) * z)). [para(10(a,1),10(a,1,1))].
44 (x *
(y * x)) * z = x * (y * (x * z)).
[back_rewrite(10),rewrite([30(2)])].
48 (x *
y) * y = x * (y * y).
[para(4(a,1),11(a,2,2,2)),rewrite([5(3)])].
65 (x *
y) * (z * (x * (u * x))) = x * ((y * ((z * x) * u)) * x). [para(11(a,1),12(a,1,2))].
70 x' *
x = 0. [para(5(a,1),15(a,1,2))].
71 x \ y
= x' * y. [para(6(a,1),15(a,1,2)),flip(a)].
73 x /
(y * x) = y'.
[para(15(a,1),8(a,1,1))].
77 x' *
(((x * y) * z) * x') = y * (z * x').
[para(15(a,1),12(a,1,1)),flip(a)].
85 x *
((x' * y) * (x * z)) = (y * x) * z.
[back_rewrite(32),rewrite([71(1)])].
87 x'' =
x. [back_rewrite(27),rewrite([71(1),73(3)])].
88 x *
(x' * y) = y.
[back_rewrite(6),rewrite([71(1)])].
89 x *
x' = 0. [para(4(a,1),16(a,1,1))].
92 x / y
= x * y'.
[para(9(a,1),16(a,1,1)),flip(a)].
93 (x *
y) * (y' * (z * y')) = (x * z) * y'.
[para(16(a,1),11(a,1,1,1)),flip(a)].
96 x' *
((y * (z * x)) * x') = (x' * y) * z.
[para(16(a,1),12(a,1,2)),flip(a)].
98 (x *
y)' * x = y'.
[para(16(a,1),15(a,1,2))].
99 x *
(y * x)' = y'.
[para(15(a,1),16(a,1,1))].
105 (x *
y') * y = x.
[back_rewrite(9),rewrite([92(1)])].
107 (C *
(x * y)) * y = x * (y * (y * C)).
[para(17(a,1),11(a,2,2,2)),rewrite([17(3,R)])].
109 C *
((C * x) * y) = x * (C * (y * C)).
[para(17(a,2),11(a,1,1,1)),rewrite([17(5,R)])].
110 x *
(y * (C * y)) = x * (y * (y * C)).
[para(17(a,2),11(a,1,1)),rewrite([107(4)]),flip(a)].
117 C' *
(x * C) = x.
[para(17(a,1),15(a,1,2))].
118 x' *
(C * x) = C.
[para(17(a,2),15(a,1,2))].
132 (x *
((y * z) * (x * u))) * ((z * x) * u)' = R(x * y,z * x,u).
[para(12(a,1),19(a,1,1,1)),rewrite([44(4)])].
138
R(x,y,z) * (y * z) = (x * y) * z.
[para(19(a,1),16(a,1,1)),rewrite([87(4)])].
141 ((x
* (y * z)) * z') * y' = R(x,y * z,z').
[para(16(a,1),19(a,1,2,1))].
146 (C *
(x * y)) * (C * y)' = R(x,y,C).
[para(17(a,2),19(a,1,2,1)),rewrite([17(3,R)])].
164
R(x,y,x * y) = x. [para(29(a,1),19(a,1)),rewrite([99(6),16(3)]),flip(a)].
166 x' *
((x * y) * x') = y * x'.
[para(70(a,1),12(a,1,1)),rewrite([4(4)]),flip(a)].
176 (x *
(y * (x * z))) * (x * z)' = R(x * y,x,z).
[para(30(a,1),19(a,1,1,1)),rewrite([44(3)])].
178 ((x
* (y * z)) * y) * (y * (z * y))' = R(x,y * z,y). [para(30(a,1),19(a,1,2,1))].
182 x *
((x' * y) * x) = y * x.
[para(89(a,1),12(a,1,1)),rewrite([4(3)]),flip(a)].
183 (x *
y)' = y' * x'.
[para(89(a,1),12(a,2,2)),rewrite([98(3),99(4),5(7)]),flip(a)].
187
R(x,y * z,z') = R(x,y * z,y).
[back_rewrite(178),rewrite([183(6),183(5),30(8),93(9),141(6)])].
188 (x *
(y * (x * z))) * (z' * x') = R(x * y,x,z). [back_rewrite(176),rewrite([183(5)])].
194 (C *
(x * y)) * (y' * C') = R(x,y,C).
[back_rewrite(146),rewrite([183(6)])].
204 (x *
((y * z) * (x * u))) * (u' * (x' * z')) = R(x * y,z * x,u).
[back_rewrite(132),rewrite([183(7),183(7)])].
214 ((x
* y) * z) * (z' * y') = R(x,y,z).
[back_rewrite(19),rewrite([183(4)])].
227 (x *
(x * (y * x))) * z = x * ((x * y) * (x * z)).
[para(16(a,1),40(a,1,1,2,2,2)),rewrite([30(4),65(6),182(4),30(2),16(7),16(8)])].
258 (x *
(y * (y * x))) * z = x * (y * (y * (x * z))). [para(29(a,1),44(a,1,1,2)),rewrite([29(7)])].
273 x *
(C * x') = C.
[para(17(a,2),88(a,1,2))].
318 C *
(x * C') = x.
[para(105(a,1),17(a,2))].
319 (x'
* C) * x = C.
[para(17(a,1),105(a,1,1))].
334 x *
(C' * x') = C'.
[para(117(a,1),16(a,1,1)),rewrite([183(3)])].
336 C' *
x = x * C'.
[para(117(a,1),30(a,1,1)),rewrite([16(10)]),flip(a)].
340 C *
(x * (C' * x)) = x * x.
[para(117(a,1),44(a,2,2)),rewrite([17(6,R)])].
441 (x *
(C * C)) * y = C * (x * (C * y)).
[para(273(a,1),40(a,1,1,2,2,2)),rewrite([12(6),70(3),4(4),273(9),273(10)])].
490 C' *
(x * (C * C)) = x * C.
[para(48(a,1),117(a,1,2))].
497 C *
(x * (C' * C')) = x * C'.
[para(48(a,1),318(a,1,2))].
506 (C *
x) * y = (x * C) * y.
[para(319(a,1),44(a,1,1,2)),rewrite([85(9)]),flip(a)].
621 (x'
* C') * x = C'.
[para(336(a,1),105(a,1,1))].
738 (x *
y) * ((y' * x') * z) = z.
[para(183(a,1),88(a,1,2,1))].
757 (x *
(C' * C')) * y = C' * (x * (C' * y)).
[para(334(a,1),40(a,1,1,2,2,2)),rewrite([12(8),70(4),4(6),334(12),334(14)])].
1090 (C'
* x) * y = (x * C') * y.
[para(621(a,1),44(a,1,1,2)),rewrite([85(11)]),flip(a)].
1218 (x
* y) * x' = x * (y * x').
[para(29(a,1),77(a,1,2,1)),rewrite([166(6)])].
1225 (x
* (y * z)) * y' = (x * y) * (z * y').
[para(44(a,1),77(a,1,2,1)),rewrite([1218(6),15(7)])].
1555 (x
* y') * (y * z) = y' * ((y * x) * z).
[para(15(a,1),85(a,1,2,2)),rewrite([87(3)]),flip(a)].
1570 (x
* y) * (x' * z) = x * ((y * x') * z).
[para(85(a,1),88(a,1,2)),rewrite([87(6)]),flip(a)].
1571 (x
* y) * (y' * z) = y * ((y' * x) * z).
[para(88(a,1),85(a,1,2,2)),flip(a)].
1583 (x
* y) * (C * y') = y * (C * (y' * x)).
[para(273(a,1),85(a,1,2,2)),rewrite([17(4,R)]),flip(a)].
1586 (x
* C) * (y * C') = C * ((C' * x) * y).
[para(318(a,1),85(a,1,2,2)),flip(a)].
1602 (x
* y) * (C' * y') = y * (C' * (y' * x)).
[para(334(a,1),85(a,1,2,2)),rewrite([336(5,R)]),flip(a)].
1665 x *
((x' * (y * z)) * z') = R(y,z,x).
[back_rewrite(214),rewrite([1571(6)])].
1798 (C
* x) * ((C' * x') * y) = y.
[para(506(a,2),88(a,1)),rewrite([183(5)])].
1862 (x
* (y * z)) * z' = z * ((z' * x) * y).
[para(96(a,1),15(a,1,2)),rewrite([87(2)]),flip(a)].
1889 C *
(C * (x * (C' * y))) = (C * x) * y.
[para(336(a,2),96(a,1,2,1,2)),rewrite([87(3),87(8),17(7,R),87(11)])].
1922 x *
(y * ((y' * x') * z)) = R(z,y,x).
[back_rewrite(1665),rewrite([1862(5)])].
1930
R(x,y * z,z') = R(x,z,y).
[back_rewrite(141),rewrite([1862(4),1862(6),1571(5),1922(6)]),flip(a)].
1941
R(x,y * z,y) = R(x,z,y).
[back_rewrite(187),rewrite([1930(3)]),flip(a)].
2261
R(x,C * y,y) = R(x,C,y).
[para(17(a,2),1941(a,1,2))].
2269
R(x,C,y) = R(x,y,C').
[para(117(a,1),1941(a,1,2)),rewrite([1930(8)]),flip(a)].
2270 R(x,C,y')
= R(x,y,C).
[para(118(a,1),1941(a,1,2)),rewrite([1930(7)])].
2279
R(x,C' * y,y) = R(x,C',y).
[para(336(a,2),1941(a,1,2))].
2633
R(R(R(c3,C,c4),C,c4),c4,C') != c3.
[para(2269(a,1),21(a,1))].
2765
R(x,y',C) = R(x,C,y).
[para(87(a,1),2270(a,1,3)),flip(a)].
2766
R(x,y * z,C) = R(x,C,z' * y').
[para(183(a,1),2270(a,1,3)),flip(a)].
2769
R(x,y',C') = R(x,y,C).
[para(2270(a,1),2269(a,1)),flip(a)].
2946
R(x,y',C) = R(x,y,C').
[para(2765(a,2),2269(a,1))].
3250 (C
* x) * (x * y) = x * (x * (y * C)).
[para(340(a,1),12(a,1,1)),rewrite([29(4),44(10),17(12,R),1889(13)]),flip(a)].
3502 C'
* (x * (C * y)) = C * ((C' * x) * y).
[para(490(a,1),12(a,1,1)),rewrite([1586(6),441(13),336(16,R),15(16)]),flip(a)].
3506 C'
* (x * (y * C)) = C * ((C' * x) * y).
[para(490(a,1),44(a,2,2,2)),rewrite([44(11),3502(9),17(8,R),88(8),3502(6)]),flip(a)].
3851 (x
* y) * (x * y) = x * (y * (x * y)).
[para(164(a,1),138(a,1,1)),flip(a)].
3852 C *
R(x,y,C * y') = y * (C * (y' * x)).
[para(273(a,1),138(a,1,2)),rewrite([17(6,R),1583(11)])].
3868 C'
* R(x,y,C' * y') = y * (C' * (y' * x)).
[para(334(a,1),138(a,1,2)),rewrite([336(8,R),1602(14)])].
4501
R(x,y,z * y') = R(x,z,y').
[para(105(a,1),1930(a,1,2)),flip(a)].
4502
R(x,C',y') = R(x,C,y).
[para(117(a,1),1930(a,1,2)),rewrite([183(3),4501(5),1930(9)])].
4506
R(x,C,y' * C) = R(x,C',y).
[para(336(a,2),1930(a,1,2)),rewrite([87(6),2766(5),87(5)])].
4529
R(x,C,y * C) = R(x,C,y).
[para(1930(a,1),2269(a,2))].
4588 x *
(C' * (x' * y)) = C' * R(y,C,x).
[back_rewrite(3868),rewrite([4501(7),4502(6)]),flip(a)].
4589 x *
(C * (x' * y)) = C * R(y,C,x').
[back_rewrite(3852),rewrite([4501(5)]),flip(a)].
4592
R(x,C',y) = R(x,C,y').
[back_rewrite(4506),rewrite([4529(5)]),flip(a)].
4653 (x
* y) * (C * y') = C * R(x,C,y').
[back_rewrite(1583),rewrite([4589(10)])].
4668
R(x,C' * y,y) = R(x,C,y').
[back_rewrite(2279),rewrite([4592(7)])].
5295 x *
R(y,C,x') = R(x * y,x,C).
[para(336(a,1),188(a,1,2)),rewrite([1570(9),1225(5),4653(5),336(8,R),15(8)])].
5298 C *
R(x,C,y) = R(C * x,C,y).
[para(336(a,2),188(a,1,2)),rewrite([1570(10),336(7,R),3502(7),1862(9),1571(8),1922(9)])].
5449 (x
* y) * (C * y') = R(C * x,C,y').
[back_rewrite(4653),rewrite([5298(10)])].
5471 x *
(C * (x' * y)) = R(C * y,C,x').
[back_rewrite(4589),rewrite([5298(10)])].
5572 C *
R(x,y,C) = R(C * x,C,y').
[para(194(a,1),109(a,1,2)),rewrite([17(12,R),318(12),5449(9)])].
6714 x *
R(y,C,x) = R(x * y,C,x).
[para(2261(a,1),204(a,2)),rewrite([1570(12),1225(6),89(5),5(5),1571(8),336(7,R),3506(7),1922(8)])].
9162 (x
* (y * (x * y))) * z = (x * y) * ((x * y) * z).
[para(738(a,1),227(a,1,1,2)),rewrite([3851(3),1571(10),16(9),89(7),4(9)])].
9255 (C'
* x) * ((C' * x) * y) = x * (C' * (C' * (x * y))). [para(1090(a,1),29(a,1,1)),rewrite([12(7),29(6),258(8)]),flip(a)].
10804
R(R(x,C,y),C,y') = x.
[para(110(a,1),1798(a,1,1)),rewrite([183(11),183(10),30(13),9162(15),9255(15),258(16),5471(14),88(11),5295(10),4
588(7),5572(9),88(7)])].
11080
R(R(x,C,y),y,C) = x.
[para(10804(a,1),2269(a,1)),rewrite([2769(6)]),flip(a)].
11090
R(R(x,C,y'),y,C') = x.
[para(11080(a,1),2946(a,1)),flip(a)].
36358 C'
* R(x,C,y) = R(x * C',C,y).
[para(497(a,1),188(a,2,1)),rewrite([757(10),15(8),88(6),1571(6),336(5,R),4588(6)])].
36411 x
* (C' * (x' * y)) = R(y * C',C,x).
[back_rewrite(4588),rewrite([36358(11)])].
72380
R(R(x,C,y),C,y) = R(x,C,y').
[para(4668(a,1),1922(a,2)),rewrite([183(7),87(7),30(8),44(9),1571(10),1555(9),3250(8),36411(10),336(7,R),
3506(7),6714(10),1922(8)])].
72515
$F.
[back_rewrite(2633),rewrite([72380(7),11090(9)]),xx(a)].
==============================
end of proof ==========================
% Proof
3 at 320.15 (+ 1.68) seconds.
% Length
of proof is 207.
% Level
of proof is 23.
%
Maximum clause weight is 30.000.
% Given
clauses 5098.
1
R(R(R(C,x,y),x,y),x,y) = C # label(non_clause) # label(goal). [goal].
4 0 * x
= x. [assumption].
5 x * 0
= x. [assumption].
6 x * (x
\ y) = y. [assumption].
8 (x *
y) / y = x. [assumption].
9 (x /
y) * y = x. [assumption].
10 ((x *
y) * x) * z = x * (y * (x * z)).
[assumption].
11 ((x *
y) * z) * y = x * (y * (z * y)).
[assumption].
12 (x *
y) * (z * x) = x * ((y * z) * x).
[assumption].
15 x' *
(x * y) = y. [assumption].
16 (x *
y) * y' = x. [assumption].
17 C * x
= x * C. [assumption].
18
R(x,y,z) = ((x * y) * z) * (y * z)'.
[assumption].
19 ((x *
y) * z) * (y * z)' = R(x,y,z).
[copy(18),flip(a)].
20
R(R(R(C,c1,c2),c1,c2),c1,c2) != C.
[deny(1)].
27 x /
(y \ x) = y.
[para(6(a,1),8(a,1,1))].
29 (x *
x) * y = x * (x * y).
[para(4(a,1),10(a,2,2)),rewrite([5(2)])].
30 (x *
y) * x = x * (y * x).
[para(10(a,1),5(a,1)),rewrite([5(2)]),flip(a)].
32 x *
((x \ y) * (x * z)) = (y * x) * z.
[para(6(a,1),10(a,1,1,1)),flip(a)].
35 (x *
(y * (x * z))) / z = x * (y * x).
[para(10(a,1),8(a,1,1)),rewrite([30(6)])].
40 (x *
(y * (x * (x * y)))) * z = (x * y) * (x * ((x * y) * z)). [para(10(a,1),10(a,1,1))].
42 (x *
((y * (z * y)) * x)) * u = x * (y * (z * (y * (x * u)))).
[para(10(a,1),10(a,2,2)),rewrite([30(2),30(4)])].
44 (x *
(y * x)) * z = x * (y * (x * z)).
[back_rewrite(10),rewrite([30(2)])].
46 (x *
(y * (z * (y * x)))) * u = x * (y * (z * (y * (x * u)))). [back_rewrite(42),rewrite([44(3)])].
48 (x *
y) * y = x * (y * y).
[para(4(a,1),11(a,2,2,2)),rewrite([5(3)])].
53 (x /
y) * (y * (z * y)) = (x * z) * y.
[para(9(a,1),11(a,1,1,1)),flip(a)].
55 (x *
(y * (z * y))) * z = (x * y) * (z * (y * z)). [para(11(a,1),11(a,1,1))].
56 x *
(((x \ y) * z) * x) = y * (z * x).
[para(6(a,1),12(a,1,1)),flip(a)].
61 x *
((y * (z / x)) * x) = (x * y) * z.
[para(9(a,1),12(a,1,2)),flip(a)].
62 (x *
y) * ((z * x) * (u * (z * x))) = x * ((y * (z * ((x * u) * z))) * x).
[para(12(a,1),11(a,1,1,1)),rewrite([44(4),12(6),11(4)]),flip(a
)].
65 (x *
y) * (z * (x * (u * x))) = x * ((y * ((z * x) * u)) * x). [para(11(a,1),12(a,1,2))].
70 x' *
x = 0. [para(5(a,1),15(a,1,2))].
71 x \ y
= x' * y.
[para(6(a,1),15(a,1,2)),flip(a)].
73 x /
(y * x) = y'.
[para(15(a,1),8(a,1,1))].
77 x' *
(((x * y) * z) * x') = y * (z * x').
[para(15(a,1),12(a,1,1)),flip(a)].
81 x *
(((x' * y) * z) * x) = y * (z * x).
[back_rewrite(56),rewrite([71(1)])].
85 x *
((x' * y) * (x * z)) = (y * x) * z.
[back_rewrite(32),rewrite([71(1)])].
87 x'' =
x. [back_rewrite(27),rewrite([71(1),73(3)])].
88 x *
(x' * y) = y.
[back_rewrite(6),rewrite([71(1)])].
89 x *
x' = 0. [para(4(a,1),16(a,1,1))].
92 x / y
= x * y'.
[para(9(a,1),16(a,1,1)),flip(a)].
93 (x *
y) * (y' * (z * y')) = (x * z) * y'.
[para(16(a,1),11(a,1,1,1)),flip(a)].
96 x' *
((y * (z * x)) * x') = (x' * y) * z.
[para(16(a,1),12(a,1,2)),flip(a)].
98 (x *
y)' * x = y'.
[para(16(a,1),15(a,1,2))].
99 x *
(y * x)' = y'. [para(15(a,1),16(a,1,1))].
100 x *
((y * (z * x')) * x) = (x * y) * z.
[back_rewrite(61),rewrite([92(1)])].
102 (x *
y') * (y * (z * y)) = (x * z) * y.
[back_rewrite(53),rewrite([92(1)])].
104 (x *
(y * (x * z))) * z' = x * (y * x).
[back_rewrite(35),rewrite([92(4)])].
105 (x *
y') * y = x.
[back_rewrite(9),rewrite([92(1)])].
109 C *
((C * x) * y) = x * (C * (y * C)).
[para(17(a,2),11(a,1,1,1)),rewrite([17(5,R)])].
113 (x *
y) * (x * C) = x * ((y * C) * x).
[para(17(a,1),12(a,1,2))].
117 C' *
(x * C) = x. [para(17(a,1),15(a,1,2))].
118 x' *
(C * x) = C.
[para(17(a,2),15(a,1,2))].
119 (x *
C) * x' = C.
[para(17(a,1),16(a,1,1))].
126 ((x
* (y * (z * y))) * u) * (y * u)' = R((x * y) * z,y,u). [para(11(a,1),19(a,1,1,1))].
127 (x *
(y * (z * y))) * (z * y)' = R(x * y,z,y).
[para(11(a,1),19(a,1,1))].
131 (x *
y)' * R(z,x,y) = ((x * y)' * (z * x)) * x'. [para(19(a,1),12(a,2,2)),rewrite([99(7)]),flip(a)].
132 (x *
((y * z) * (x * u))) * ((z * x) * u)' = R(x * y,z * x,u).
[para(12(a,1),19(a,1,1,1)),rewrite([44(4)])].
133 x *
((y * z) * (x * (y * (z * x))')) = R(x,y,z * x). [para(12(a,1),19(a,1,1)),rewrite([44(7)])].
134 ((x
* (y * z)) * (u * y)) * (y * ((z * u) * y))' = R(x,y * z,u * y). [para(12(a,1),19(a,1,2,1))].
136
R(x',x * y,z) = (y * z) * ((x * y) * z)'.
[para(15(a,1),19(a,1,1,1)),flip(a)].
138
R(x,y,z) * (y * z) = (x * y) * z.
[para(19(a,1),16(a,1,1)),rewrite([87(4)])].
141 ((x
* (y * z)) * z') * y' = R(x,y * z,z').
[para(16(a,1),19(a,1,2,1))].
146 (C *
(x * y)) * (C * y)' = R(x,y,C).
[para(17(a,2),19(a,1,2,1)),rewrite([17(3,R)])].
148 R(x
* y,z,(y * z)') = R(x,y,z) * y.
[para(19(a,1),19(a,1,1)),rewrite([99(4),87(3)]),flip(a)].
166 x' *
((x * y) * x') = y * x'.
[para(70(a,1),12(a,1,1)),rewrite([4(4)]),flip(a)].
176 (x *
(y * (x * z))) * (x * z)' = R(x * y,x,z).
[para(30(a,1),19(a,1,1,1)),rewrite([44(3)])].
178 ((x
* (y * z)) * y) * (y * (z * y))' = R(x,y * z,y). [para(30(a,1),19(a,1,2,1))].
182 x *
((x' * y) * x) = y * x.
[para(89(a,1),12(a,1,1)),rewrite([4(3)]),flip(a)].
183 (x *
y)' = y' * x'. [para(89(a,1),12(a,2,2)),rewrite([98(3),99(4),5(7)]),flip(a)].
187
R(x,y * z,z') = R(x,y * z,y).
[back_rewrite(178),rewrite([183(6),183(5),30(8),93(9),141(6)])].
188 (x *
(y * (x * z))) * (z' * x') = R(x * y,x,z). [back_rewrite(176),rewrite([183(5)])].
192 R(x
* y,z,z' * y') = R(x,y,z) * y.
[back_rewrite(148),rewrite([183(3)])].
194 (C *
(x * y)) * (y' * C') = R(x,y,C).
[back_rewrite(146),rewrite([183(6)])].
200
R(x',x * y,z) = (y * z) * (z' * (y' * x')). [back_rewrite(136),rewrite([183(7),183(7)])].
202 ((x
* (y * z)) * (u * y)) * (y' * ((u' * z') * y')) = R(x,y * z,u * y).
[back_rewrite(134),rewrite([183(8),183(7),183(7),30(11)])].
203 x *
((y * z) * (x * ((x' * z') * y'))) = R(x,y,z * x). [back_rewrite(133),rewrite([183(4),183(3)])].
204 (x *
((y * z) * (x * u))) * (u' * (x' * z')) = R(x * y,z * x,u).
[back_rewrite(132),rewrite([183(7),183(7)])].
205 (x'
* y') * R(z,y,x) = x' * (y' * z).
[back_rewrite(131),rewrite([183(2),183(7),11(12),16(10)])].
209 (x *
(y * (z * y))) * (y' * z') = R(x * y,z,y). [back_rewrite(127),rewrite([183(5)])].
210 ((x
* (y * (z * y))) * u) * (u' * y') = R((x * y) * z,y,u). [back_rewrite(126),rewrite([183(6)])].
214 ((x
* y) * z) * (z' * y') = R(x,y,z).
[back_rewrite(19),rewrite([183(4)])].
246 (x *
(y * (x * (z * x)))) * u = x * (((y * x) * z) * (x * u)). [para(11(a,1),44(a,1,1,2))].
254 (C *
(C * x)) * y = C * (x * (C * y)).
[para(17(a,2),44(a,1,1,2))].
258 (x *
(y * (y * x))) * z = x * (y * (y * (x * z))). [para(29(a,1),44(a,1,1,2)),rewrite([29(7)])].
273 x *
(C * x') = C.
[para(17(a,2),88(a,1,2))].
318 C *
(x * C') = x.
[para(105(a,1),17(a,2))].
319 (x'
* C) * x = C.
[para(17(a,1),105(a,1,1))].
332 C' *
(((x * C) * y) * C') = x * (y * C').
[para(117(a,1),12(a,1,1)),flip(a)].
336 C' *
x = x * C'. [para(117(a,1),30(a,1,1)),rewrite([16(10)]),flip(a)].
345 C' *
(C' * ((x * C) * y)) = x * (y * C').
[back_rewrite(332),rewrite([336(8,R)])].
358 C *
(x * C) = x * (C * C).
[para(119(a,1),29(a,2,2)),rewrite([113(5),29(4),258(7),89(4),5(4),17(8,R)]),flip(a)].
441 (x *
(C * C)) * y = C * (x * (C * y)).
[para(273(a,1),40(a,1,1,2,2,2)),rewrite([12(6),70(3),4(4),273(9),273(10)])].
463 C' *
(x * (C * (y * (C * x)))) = x * (C * (y * x)). [para(318(a,1),46(a,2,2,2,2)),rewrite([336(9,R)])].
490 C' *
(x * (C * C)) = x * C. [para(48(a,1),117(a,1,2))].
506 (C *
x) * y = (x * C) * y.
[para(319(a,1),44(a,1,1,2)),rewrite([85(9)]),flip(a)].
605 x' *
(C' * x) = C'.
[para(336(a,2),15(a,1,2))].
621 (x'
* C') * x = C'.
[para(336(a,1),105(a,1,1))].
689 (x *
(y * z)) * (z' * y) = (x * z) * (z' * (y * y)). [para(88(a,1),55(a,2,2,2)),rewrite([182(4),48(9)])].
692 (x *
C) * (C' * (y * y)) = C' * (x * (y * (C * y))).
[para(117(a,1),55(a,1,1,2,2)),rewrite([30(3),336(7,R),336(17,R),117(17),689(14)]),f
lip(a)].
731 (x *
(y * z)) * (z' * y') = x.
[para(183(a,1),16(a,1,2))].
791 (x *
y) * (z * (x * y)) = x * (y * ((z * x) * y)).
[para(62(a,1),15(a,1,2)),rewrite([183(2),102(10),15(6),44(4),12(3)]),flip(a)].
794 x' *
((y * (z * (u * (z * x)))) * x') = (x' * y) * (z * (u * z)).
[para(16(a,1),62(a,1,2,1)),rewrite([16(5),791(12),81(11)]),flip(a)].
1090 (C'
* x) * y = (x * C') * y.
[para(621(a,1),44(a,1,1,2)),rewrite([85(11)]),flip(a)].
1218 (x
* y) * x' = x * (y * x').
[para(29(a,1),77(a,1,2,1)),rewrite([166(6)])].
1284 x *
((C * (x' * y)) * x) = y * (x * C).
[para(17(a,1),81(a,2,2)),rewrite([17(4,R)])].
1285 x *
(C * y) = x * (y * C).
[para(17(a,2),81(a,1,2,1)),rewrite([1284(6)]),flip(a)].
1287 (x'
* y) * x = x' * (y * x).
[para(29(a,1),81(a,1,2,1)),rewrite([182(6)])].
1295 (x
* (y' * z)) * y = (x * y') * (z * y).
[para(44(a,1),81(a,1,2,1)),rewrite([1287(6),88(7)])].
1555 (x
* y') * (y * z) = y' * ((y * x) * z).
[para(15(a,1),85(a,1,2,2)),rewrite([87(3)]),flip(a)].
1570 (x
* y) * (x' * z) = x * ((y * x') * z).
[para(85(a,1),88(a,1,2)),rewrite([87(6)]),flip(a)].
1571 (x
* y) * (y' * z) = y * ((y' * x) * z).
[para(88(a,1),85(a,1,2,2)),flip(a)].
1577 (x
* y') * (C * y) = y' * (C * (y * x)).
[para(118(a,1),85(a,1,2,2)),rewrite([87(3),17(4,R)]),flip(a)].
1583 (x
* y) * (C * y') = y * (C * (y' * x)).
[para(273(a,1),85(a,1,2,2)),rewrite([17(4,R)]),flip(a)].
1586 (x
* C) * (y * C') = C * ((C' * x) * y).
[para(318(a,1),85(a,1,2,2)),flip(a)].
1661 C'
* (x * (y * (C * y))) = C * ((C' * x) * (y * y)). [back_rewrite(692),rewrite([1571(7)]),flip(a)].
1665 x *
((x' * (y * z)) * z') = R(y,z,x).
[back_rewrite(214),rewrite([1571(6)])].
1667 x *
((x' * (y * (z * (u * z)))) * z') = R((y * z) * u,z,x). [back_rewrite(210),rewrite([1571(8)])].
1669
R(x',x * y,z) = z * (y * ((y' * z') * x')). [back_rewrite(200),rewrite([1571(10),1571(9)])].
1770 (x'
* C') * ((x * C) * y) = y.
[para(506(a,1),15(a,1,2)),rewrite([183(3)])].
1779 (C
* x) * (y * (x * C)) = x * (C * (C * (y * x))). [para(506(a,2),30(a,2)),rewrite([30(6),791(6),17(4,R)]),flip(a)].
1794 (x
* (C * (C * (y * x)))) * z = (x * C) * (y * ((x * C) * z)).
[para(506(a,2),44(a,1,1)),rewrite([1779(6)])].
1797 (x
* C) * ((x' * C') * y) = y.
[para(506(a,1),88(a,1)),rewrite([183(5)])].
1862 (x
* (y * z)) * z' = z * ((z' * x) * y). [para(96(a,1),15(a,1,2)),rewrite([87(2)]),flip(a)].
1922 x *
(y * ((y' * x') * z)) = R(z,y,x).
[back_rewrite(1665),rewrite([1862(5)])].
1930
R(x,y * z,z') = R(x,z,y).
[back_rewrite(141),rewrite([1862(4),1862(6),1571(5),1922(6)]),flip(a)].
1934
R(x',x * y,z) = R(x',y,z).
[back_rewrite(1669),rewrite([1922(10)])].
1941
R(x,y * z,y) = R(x,z,y).
[back_rewrite(187),rewrite([1930(3)]),flip(a)].
1958 C *
(C * (x * (y * C'))) = (C * x) * y.
[para(100(a,1),17(a,1)),rewrite([17(9,R),17(11,R)]),flip(a)].
2258
R(x,y * z,y') = R(x,z,y').
[para(15(a,1),1941(a,1,2)),flip(a)].
2267
R(x,y' * z,y) = R(x,z,y).
[para(88(a,1),1941(a,1,2)),flip(a)].
2269
R(x,C,y) = R(x,y,C').
[para(117(a,1),1941(a,1,2)),rewrite([1930(8)]),flip(a)].
2270
R(x,C,y') = R(x,y,C). [para(118(a,1),1941(a,1,2)),rewrite([1930(7)])].
2765
R(x,y',C) = R(x,C,y).
[para(87(a,1),2270(a,1,3)),flip(a)].
2766
R(x,y * z,C) = R(x,C,z' * y').
[para(183(a,1),2270(a,1,3)),flip(a)].
2769
R(x,y',C') = R(x,y,C).
[para(2270(a,1),2269(a,1)),flip(a)].
2946 R(x,y',C)
= R(x,y,C').
[para(2765(a,2),2269(a,1))].
3502 C'
* (x * (C * y)) = C * ((C' * x) * y).
[para(490(a,1),12(a,1,1)),rewrite([1586(6),441(13),336(16,R),15(16)]),flip(a)].
3537 C *
((C' * x) * (y * (C * x))) = x * (C * (y * x)). [back_rewrite(463),rewrite([3502(9)])].
3846 C *
R(x,y',C * y) = y' * (C * (y * x)).
[para(118(a,1),138(a,1,2)),rewrite([17(6,R),1577(11)])].
3852 C *
R(x,y,C * y') = y * (C * (y' * x)).
[para(273(a,1),138(a,1,2)),rewrite([17(6,R),1583(11)])].
4494
R(x,y',z * y) = R(x,z,y).
[para(16(a,1),1930(a,1,2)),rewrite([87(2)]),flip(a)].
4496
R(x,y * z',z) = R(x,z',y).
[para(87(a,1),1930(a,1,3))].
4497
R(x,y,y * z) = R(x,y,z).
[para(30(a,1),1930(a,1,2)),rewrite([2258(4),1930(3)]),flip(a)].
4500
R(x,y,y' * z) = R(x,y,z).
[para(88(a,1),1930(a,1,2)),rewrite([183(3),87(3),2267(6)])].
4501
R(x,y,z * y') = R(x,z,y').
[para(105(a,1),1930(a,1,2)),flip(a)].
4506
R(x,C,y' * C) = R(x,C',y).
[para(336(a,2),1930(a,1,2)),rewrite([87(6),2766(5),87(5)])].
4508
R(x,y * (z * u),u' * z') = R(x,z * u,y).
[para(183(a,1),1930(a,1,3))].
4529
R(x,C,y * C) = R(x,C,y).
[para(1930(a,1),2269(a,2))].
4557
R(x,y,z) * y = R(x * y,z,y').
[back_rewrite(192),rewrite([4500(5)]),flip(a)].
4559 x'
* (C * (x * y)) = C * R(y,C,x).
[back_rewrite(3846),rewrite([4494(5)]),flip(a)].
4589 x *
(C * (x' * y)) = C * R(y,C,x').
[back_rewrite(3852),rewrite([4501(5)]),flip(a)].
4592
R(x,C',y) = R(x,C,y').
[back_rewrite(4506),rewrite([4529(5)]),flip(a)].
4630 (x
* y') * (C * y) = C * R(x,C,y).
[back_rewrite(1577),rewrite([4559(10)])].
4653 (x
* y) * (C * y') = C * R(x,C,y').
[back_rewrite(1583),rewrite([4589(10)])].
5245
R((x * y) * z,y,x) = x * (y * z).
[para(16(a,1),188(a,1,1,2,2)),rewrite([12(3),87(5),183(5),88(7),1218(5),16(4),1930(7)]),flip(a)].
5271 x *
((x' * C') * y) = R(C' * y,x,C).
[para(117(a,1),188(a,1,1,2,2)),rewrite([183(7),87(11),17(10,R),88(10),1862(6),4494(14)])].
5274 x *
(C * R(x',C,y)) = R(C,y',x).
[para(118(a,1),188(a,2,1)),rewrite([1571(6),15(7),87(7),1571(7),1295(6),4630(6)])].
5282 x *
((x' * C) * y) = R(C * y,x,C').
[para(318(a,1),188(a,1,1,2,2)),rewrite([183(7),87(6),336(9,R),15(9),1862(5),4501(12)])].
5298 C *
R(x,C,y) = R(C * x,C,y).
[para(336(a,2),188(a,1,2)),rewrite([1570(10),336(7,R),3502(7),1862(9),1571(8),1922(9)])].
5397
R(x,x * y,z) * z = R(x * z,x,y).
[para(188(a,1),138(a,2)),rewrite([4508(6),731(8)])].
5442 x *
R(C * x',C,y) = R(C,y',x).
[back_rewrite(5274),rewrite([5298(5)])].
5449 (x
* y) * (C * y') = R(C * x,C,y').
[back_rewrite(4653),rewrite([5298(10)])].
5562 R(C
* x,y,C) = R(x * C,y,C).
[para(506(a,2),194(a,1,1,2)),rewrite([194(10)])].
5572 C *
R(x,y,C) = R(C * x,C,y').
[para(194(a,1),109(a,1,2)),rewrite([17(12,R),318(12),5449(9)])].
5843 x *
R(C * x',y,C') = R(C,x * C',y * x).
[para(318(a,1),202(a,1,1,1)),rewrite([87(7),1570(10),16(3),5282(6)])].
5922 x *
(C * (y * (C * ((y' * C') * x')))) = R(C,x * C,y * x).
[para(358(a,1),202(a,1,1,1)),rewrite([12(6),29(4),254(5),1570(15),104(7),44(
11)])].
7352
R(R(x * y,y,z),z,y) = x * y.
[para(138(a,1),209(a,1,1)),rewrite([731(7),4557(4),1930(5)]),flip(a)].
9329 (C'
* x) * (y * C) = C' * ((C * x) * y).
[para(1090(a,1),1285(a,1)),rewrite([1555(6)]),flip(a)].
10773 x
* (C * ((x' * C') * y)) = R(y,C,x).
[para(205(a,1),1797(a,1,2)),rewrite([1570(8),1570(7)])].
10788
R(C,x * C,y * x) = R(C,y',x).
[back_rewrite(5922),rewrite([10773(10),5298(5),5442(6)]),flip(a)].
13231
R(x,x * y,z) = R(x,y,z).
[para(15(a,1),1934(a,1,2)),rewrite([87(2),87(3)]),flip(a)].
13236
R(x,x' * y,z) = R(x,y,z).
[para(87(a,1),1934(a,1,1)),rewrite([87(5)])].
13241
R(C,x * C,y) = R(C,x,y).
[para(117(a,1),1934(a,1,2)),rewrite([87(3),87(5)]),flip(a)].
13248
R(C,x * C',y) = R(C,x,y).
[para(336(a,1),1934(a,1,2)),rewrite([87(3),87(8)])].
13253
R(x,C' * x,y) = R(x,C,y').
[para(605(a,1),1934(a,1,2)),rewrite([87(2),4592(3),87(5)]),flip(a)].
13340
R(x * y,x,z) = R(x,z,y) * y.
[back_rewrite(5397),rewrite([13231(2)]),flip(a)].
13380
R(C,x,y * x) = R(C,y',x).
[back_rewrite(10788),rewrite([13241(5)])].
13386 x
* R(C * x',y,C') = R(C,y',x).
[back_rewrite(5843),rewrite([13248(13),13380(10)])].
14299
R(x * y,x,z * x) = x * R(y,x,z).
[para(246(a,1),188(a,1)),rewrite([183(4),30(7),88(8),1571(6),1862(5),1922(6)]),flip(a)].
16165
R(C,x * y,y) = R(C,x,y).
[para(15(a,1),13380(a,1,3)),rewrite([87(6),4497(6)])].
16170
R(C,x',y) = R(C,y,x).
[para(105(a,1),13380(a,1,3)),rewrite([183(6),87(5),1941(6)]),flip(a)].
16185
R(C,x' * y',y * C) = R(C,x',y).
[para(113(a,1),13380(a,1,3)),rewrite([13241(8),4497(6),13380(5),183(4),13236(6),183(6)]),flip(a)].
16219
R(C,x,y') = R(C,y,x).
[para(87(a,1),16170(a,1,2)),flip(a)].
16227
R(C,x,y * C) = R(C,y',x).
[para(16170(a,2),203(a,2)),rewrite([203(12),183(8),13236(10)])].
16239
R(C,x',y) = R(C,x,y').
[back_rewrite(16185),rewrite([16227(7),13380(6),87(3)]),flip(a)].
16283 x
* R(C * x',y,C') = R(C,y,x').
[back_rewrite(13386),rewrite([16239(10)])].
19549 (x
* C) * (y * R(y',C,x')) = R(C * x,C,x' * y').
[para(5562(a,2),204(a,2)),rewrite([12(5),17(4,R),1794(13),1571(11),1571(10),5271(10),
5572(10),88(8),2766(13)])].
20693
R(R(x,y,z),z,y) = x.
[para(105(a,1),7352(a,1,1,1)),rewrite([105(5)])].
20697
R(R(x,C,y'),y,x * C') = x.
[para(318(a,1),7352(a,1,1,1)),rewrite([13231(4),4592(3),318(12)])].
20739
R(R(C,x,y'),x,y) = C.
[para(16219(a,2),20693(a,1,1))].
23661 C'
* ((x * C) * y) = C * (x * (y * C')).
[para(345(a,1),15(a,1,2)),rewrite([87(3)]),flip(a)].
23698 C'
* ((C * x) * y) = C * (x * (y * C')).
[para(345(a,1),1218(a,1,1)),rewrite([87(7),17(6,R),23661(14),87(17),17(16,R),1958(16)]),flip(
a)].
23780
(C' * x) * (y * C) = C * (x * (y * C')).
[back_rewrite(9329),rewrite([23698(12)])].
25534
R(x * y,x,y' * z) = R(x,z,y) * y.
[para(2267(a,1),13340(a,2,1))].
25895
R(C,x,y') * y = R(C * y,y,x).
[para(13340(a,1),13253(a,2)),rewrite([15(7),16239(6)]),flip(a)].
25912 (x
* C) * (y * R(y',C,x')) = R(C * x,x,y).
[back_rewrite(19549),rewrite([25534(15),16239(11),25895(12)])].
29876
R(R(x,y,C),y,x * C') = x.
[para(2269(a,1),20697(a,1,1)),rewrite([2769(4)])].
29896
R(R(x * C,y,C),y,x) = x * C.
[para(16(a,1),29876(a,1,3))].
39656 R(x
* C,y,C) = R(x * C,x,y).
[para(29896(a,1),20693(a,1,1)),flip(a)].
41610 x
* R(C,x,y) = R(C * x,x,y).
[para(39656(a,1),204(a,2)),rewrite([12(5),17(4,R),1794(13),1571(11),1571(10),5271(10),5572(10),88(8),2591
2(8),14299(7)]),flip(a)].
42370
R(C * (x * y),x * y,y) = (x * y) * R(C,x,y). [para(16165(a,1),41610(a,1,2)),flip(a)].
44970 x
* ((C * x') * y) = R(C * y,x,C').
[para(273(a,1),5245(a,1,1,1)),rewrite([4496(6),2946(5)]),flip(a)].
54586 (C
* (x * (y * y))) * y' = x * (y * C).
[para(1770(a,1),794(a,2)),rewrite([30(8),65(10),17(7,R),254(9),3502(11),3537(11),48(4),1218(8)
,15(9)])].
69098 (x
* y) * R(C,x,y) = (C * x) * y.
[para(39656(a,1),1667(a,2)),rewrite([1661(8),54586(10),23780(7),1958(8),17(6,R),42370(8)]),flip(a)].
91884
R(R(C,x,y),x,y) = R(C,x,y').
[para(69098(a,1),1922(a,1,2,2)),rewrite([44970(6),16283(7),16239(7),87(6)]),flip(a)].
91889
$F.
[back_rewrite(20),rewrite([91884(7),20739(8)]),xx(a)].
==============================
end of proof ==========================