% Length of proof is 7.
% Level of proof is 2.
% Maximum clause weight is 15.
% Given clauses 0.
1 (z * (A * y)) * z = (z * A) * (y * z) #
label(non_clause) # label(goal). [goal].
8 x * (y * x) = (x * y) * x. [assumption].
9 (x * y) * x = x * (y * x). [copy(8),flip(a)].
15 x * ((A * y) * x) = (x * A) * (y * x). [assumption].
16 (x * A) * (y * x) = x * ((A * y) * x). [copy(15),flip(a)].
20 (c1 * (A * c2)) * c1 != (c1 * A) * (c2 *
c1). [deny(1)].
21 $F.
[copy(20),rewrite([9(7),16(14)]),xx(a)].
============================== end of proof
==========================
% Length
of proof is 7.
% Level
of proof is 2.
%
Maximum clause weight is 15.
% Given
clauses 0.
1 (z *
(x * A)) * z = (z * x) * (A * z) # label(non_clause)
# label(goal). [goal].
8 x * (y
* x) = (x * y) * x. [assumption].
9 (x *
y) * x = x * (y * x).
[copy(8),flip(a)].
17 x *
((y * A) * x) = (x * y) * (A * x).
[assumption].
18 (x *
y) * (A * x) = x * ((y * A) * x).
[copy(17),flip(a)].
21 (c1 *
(c2 * A)) * c1 != (c1 * c2) * (A * c1). [deny(1)].
22
$F.
[copy(21),rewrite([9(7),18(14)]),xx(a)].
==============================
end of proof ==========================
% Length
of proof is 42.
% Level
of proof is 15.
%
Maximum clause weight is 23.
% Given
clauses 1825.
1 z * (A
* (z * y)) = ((z * A) * z) * y # label(non_clause) #
label(goal). [goal].
2 1 * x
= x. [assumption].
3 x * 1
= x. [assumption].
4 x * (x
\ y) = y. [assumption].
5 x \ (x
* y) = y. [assumption].
6 (x *
y) / y = x. [assumption].
7 (x /
y) * y = x. [assumption].
8 x * (y
* x) = (x * y) * x. [assumption].
9 (x *
y) * x = x * (y * x).
[copy(8),flip(a)].
10 x *
(x * y) = (x * x) * y.
[assumption].
11 (x *
x) * y = x * (x * y).
[copy(10),flip(a)].
12 (x *
y) * y = x * (y * y).
[assumption].
13 A *
((x * y) * A) = (A * x) * (y * A).
[assumption].
14 (A *
x) * (y * A) = A * ((x * y) * A).
[copy(13),flip(a)].
22 ((c1
* A) * c1) * c2 != c1 * (A * (c1 * c2)).
[deny(1)].
23 (c1 *
(A * c1)) * c2 != c1 * (A * (c1 * c2)).
[copy(22),rewrite([9(5)])].
25 x \ x
= 1. [para(3(a,1),5(a,1,2))].
28 x /
(y \ x) = y. [para(4(a,1),6(a,1,1))].
29 (x /
y) \ x = y. [para(7(a,1),5(a,1,2))].
30 x *
((x \ y) * x) = y * x. [para(4(a,1),9(a,1,1)),flip(a)].
32 (x *
(y * x)) / x = x * y. [para(9(a,1),6(a,1,1))].
37 (x *
(x * y)) / y = x * x. [para(11(a,1),6(a,1,1))].
43 (x /
y) * (y * y) = x * y. [para(7(a,1),12(a,1,1)),flip(a)].
50 (A *
((x * y) * A)) / (y * A) = A * x.
[para(14(a,1),6(a,1,1))].
53 (A *
x) * (A * (y * A)) = A * ((x * (A * y)) * A). [para(9(a,1),14(a,1,2))].
88 x \
(y * x) = (x \ y) * x. [para(30(a,1),5(a,1,2))].
113 (x *
y) / x = x * (y / x). [para(7(a,1),32(a,1,1,2))].
135 (A *
((x * (A * (x * y))) * A)) / (y * A) = (A * x) * (A * x). [para(14(a,1),37(a,1,1,2)),rewrite([53(8)])].
178 (x /
y) \ (x * y) = y * y. [para(43(a,1),5(a,1,2))].
188 (x \
1) * x = 1. [para(2(a,1),88(a,1,2)),rewrite([25(1)]),flip(a)].
202 x *
(1 / x) = 1. [para(29(a,1),188(a,1,1))].
231 A *
(((1 / A) * x) * A) = x * A. [para(202(a,1),14(a,1,1)),rewrite([2(4)]),flip(a)].
626 ((1
/ A) \ x) * A = A * (x * A). [para(4(a,1),231(a,1,2,1)),flip(a)].
672 (1 /
A) \ x = A * x. [para(626(a,1),6(a,1,1)),rewrite([113(6),6(5)]),flip(a)].
677 x /
(A * x) = 1 / A. [para(672(a,1),28(a,1,2))].
704 (A *
x) * (A * x) = A * (x * (A * x)).
[para(677(a,1),178(a,1,1)),rewrite([672(7)]),flip(a)].
721 (A *
((x * (A * (x * y))) * A)) / (y * A) = A * (x * (A * x)). [back_rewrite(135),rewrite([704(16)])].
724 (A *
(x * A)) / (y * A) = A * (x / y).
[para(7(a,1),50(a,1,1,2,1))].
743 A *
((x * (A * (x * y))) / y) = A * (x * (A * x)). [back_rewrite(721),rewrite([724(11)])].
39589 (x
* (A * (x * y))) / y = x * (A * x).
[para(743(a,1),5(a,1,2)),rewrite([5(7)]),flip(a)].
39638 (x
* (A * x)) * y = x * (A * (x * y)).
[para(39589(a,1),7(a,1,1))].
39639
$F. [resolve(39638,a,23,a)].
==============================
end of proof ==========================
% Length
of proof is 44.
% Level
of proof is 16.
%
Maximum clause weight is 19.
% Given
clauses 2106.
1 ((x *
z) * A) * z = x * (z * (A * z)) # label(non_clause) #
label(goal). [goal].
2 1 * x
= x. [assumption].
3 x * 1
= x. [assumption].
4 x * (x
\ y) = y. [assumption].
5 x \ (x
* y) = y. [assumption].
6 (x *
y) / y = x. [assumption].
7 (x /
y) * y = x. [assumption].
8 x * (y
* x) = (x * y) * x. [assumption].
9 (x *
y) * x = x * (y * x).
[copy(8),flip(a)].
12 (x *
y) * y = x * (y * y).
[assumption].
13 A *
((x * y) * A) = (A * x) * (y * A).
[assumption].
14 (A *
x) * (y * A) = A * ((x * y) * A).
[copy(13),flip(a)].
17 x *
((y * A) * x) = (x * y) * (A * x).
[assumption].
18 (x *
y) * (A * x) = x * ((y * A) * x).
[copy(17),flip(a)].
22 x *
(A * (x * y)) = ((x * A) * x) * y.
[assumption].
23 (x *
(A * x)) * y = x * (A * (x * y)).
[copy(22),rewrite([9(7)]),flip(a)].
24 ((c1
* c2) * A) * c2 != c1 * (c2 * (A * c2)).
[deny(1)].
26 x \ x
= 1. [para(3(a,1),5(a,1,2))].
30 (x /
y) \ x = y. [para(7(a,1),5(a,1,2))].
31 x *
((x \ y) * x) = y * x. [para(4(a,1),9(a,1,1)),flip(a)].
33 (x *
(y * x)) / x = x * y. [para(9(a,1),6(a,1,1))].
44 (x /
y) * (y * y) = x * y. [para(7(a,1),12(a,1,1)),flip(a)].
50 (A *
x) \ (A * ((x * y) * A)) = y * A.
[para(14(a,1),5(a,1,2))].
51 (A *
((x * y) * A)) / (y * A) = A * x.
[para(14(a,1),6(a,1,1))].
92 (x *
(A * (x * y))) / y = x * (A * x).
[para(23(a,1),6(a,1,1))].
104 x \
(y * x) = (x \ y) * x. [para(31(a,1),5(a,1,2))].
134 (x *
y) / x = x * (y / x). [para(7(a,1),33(a,1,1,2))].
217 (x /
y) \ (x * y) = y * y. [para(44(a,1),5(a,1,2))].
229 (x \
1) * x = 1. [para(2(a,1),104(a,1,2)),rewrite([26(1)]),flip(a)].
244 x *
(1 / x) = 1. [para(30(a,1),229(a,1,1))].
276 A *
(((1 / A) * x) * A) = x * A. [para(244(a,1),14(a,1,1)),rewrite([2(4)]),flip(a)].
703 ((1
/ A) \ x) * A = A * (x * A). [para(4(a,1),276(a,1,2,1)),flip(a)].
741 (A *
x) \ (A * (y * A)) = (x \ y) * A.
[para(4(a,1),50(a,1,2,2,1))].
752 (1 /
A) \ x = A * x. [para(703(a,1),6(a,1,1)),rewrite([134(6),6(5)]),flip(a)].
756 (1 /
A) * (A * x) = x. [para(752(a,1),4(a,1,2))].
759 (A *
x) * (1 / A) = A * (x * (1 / A)).
[para(752(a,1),104(a,1)),rewrite([752(10)]),flip(a)].
765 (1 /
A) * x = A \ x. [para(4(a,1),756(a,1,2))].
769 (x *
A) * (1 / A) = x. [para(756(a,1),18(a,1,1)),rewrite([244(5),3(2),9(7),759(11),765(12),5(10)]),flip(a)].
803 (x \
(((x * y) * A) * y)) * A = (y * A) * (y * A). [para(51(a,1),217(a,1,1)),rewrite([14(10),741(11)])].
836 (x *
A) * (x * A) = x * (A * (x * A)).
[para(769(a,1),18(a,1,1)),rewrite([7(12),2(11)]),flip(a)].
857 (x \
(((x * y) * A) * y)) * A = y * (A * (y * A)). [back_rewrite(803),rewrite([836(12)])].
40454 x
\ (((x * y) * A) * y) = y * (A * y).
[para(857(a,1),6(a,1,1)),rewrite([92(7)]),flip(a)].
40461
((x * y) * A) * y = x * (y * (A * y)).
[para(40454(a,1),4(a,1,2)),flip(a)].
40462
$F. [resolve(40461,a,24,a)].
==============================
end of proof ==========================
% Length
of proof is 108.
% Level
of proof is 23.
%
Maximum clause weight is 23.
% Given
clauses 5194.
1 A * (x
* (A * y)) = ((A * x) * A) * y # label(non_clause) #
label(goal). [goal].
2 1 * x
= x. [assumption].
3 x * 1
= x. [assumption].
4 x * (x
\ y) = y. [assumption].
5 x \ (x
* y) = y. [assumption].
6 (x *
y) / y = x. [assumption].
7 (x /
y) * y = x. [assumption].
8 x * (y
* x) = (x * y) * x. [assumption].
9 (x *
y) * x = x * (y * x).
[copy(8),flip(a)].
10 x *
(x * y) = (x * x) * y.
[assumption].
11 (x *
x) * y = x * (x * y).
[copy(10),flip(a)].
12 (x *
y) * y = x * (y * y).
[assumption].
13 A *
((x * y) * A) = (A * x) * (y * A).
[assumption].
14 (A *
x) * (y * A) = A * ((x * y) * A).
[copy(13),flip(a)].
15 x *
((A * y) * x) = (x * A) * (y * x).
[assumption].
16 (x *
A) * (y * x) = x * ((A * y) * x).
[copy(15),flip(a)].
17 x *
((y * A) * x) = (x * y) * (A * x).
[assumption].
18 (x *
y) * (A * x) = x * ((y * A) * x).
[copy(17),flip(a)].
25 ((A *
c1) * A) * c2 != A * (c1 * (A * c2)).
[deny(1)].
26 (A *
(c1 * A)) * c2 != A * (c1 * (A * c2)).
[copy(25),rewrite([9(5)])].
28 x \ x
= 1. [para(3(a,1),5(a,1,2))].
32 (x /
y) \ x = y. [para(7(a,1),5(a,1,2))].
33 x *
((x \ y) * x) = y * x. [para(4(a,1),9(a,1,1)),flip(a)].
35 (x *
(y * x)) / x = x * y. [para(9(a,1),6(a,1,1))].
38 x *
(x * ((x * x) \ y)) = y. [para(11(a,1),4(a,1))].
43 x *
((x \ y) * (x \ y)) = y * (x \ y).
[para(4(a,1),12(a,1,1)),flip(a)].
45 (x *
(y * y)) / y = x * y. [para(12(a,1),6(a,1,1))].
47 (x *
(y * y)) * (x * y) = (x * y) * (y * (x * y)). [para(12(a,1),9(a,1,1))].
51 A *
(((A \ x) * y) * A) = x * (y * A).
[para(4(a,1),14(a,1,1)),flip(a)].
53 (A *
((x * y) * A)) / (y * A) = A * x.
[para(14(a,1),6(a,1,1))].
54 A *
((x * (y / A)) * A) = (A * x) * y.
[para(7(a,1),14(a,1,2)),flip(a)].
62 (x *
A) \ (x * ((A * y) * x)) = y * x.
[para(16(a,1),5(a,1,2))].
65 x *
((A * (y / x)) * x) = (x * A) * y.
[para(7(a,1),16(a,1,2)),flip(a)].
76 x *
(((x \ y) * A) * x) = y * (A * x).
[para(4(a,1),18(a,1,1)),flip(a)].
79 (x *
((y * A) * x)) / (A * x) = x * y.
[para(18(a,1),6(a,1,1))].
129 x \
(y * x) = (x \ y) * x. [para(33(a,1),5(a,1,2))].
162 (x *
y) / x = x * (y / x). [para(7(a,1),35(a,1,1,2))].
165 x *
((x * x) \ y) = x \ y. [para(38(a,1),5(a,1,2)),flip(a)].
220 (x /
(y * y)) * y = x / y. [para(7(a,1),45(a,1,1)),flip(a)].
275 (x \
1) * x = 1. [para(2(a,1),129(a,1,2)),rewrite([28(1)]),flip(a)].
277 (x \
(y / x)) * x = x \ y. [para(7(a,1),129(a,1,2)),flip(a)].
291 x *
(1 / x) = 1. [para(32(a,1),275(a,1,1))].
327 A *
(((1 / A) * x) * A) = x * A. [para(291(a,1),14(a,1,1)),rewrite([2(4)]),flip(a)].
344 (x *
(A \ x)) * (y * A) = x * (((A \ x) * y) * A). [para(43(a,1),14(a,1,1)),rewrite([11(13),51(16)])].
379 x *
((x \ y) / x) = y / x. [para(4(a,1),162(a,1,1)),flip(a)].
394 (x *
x) \ y = x \ (x \ y). [para(165(a,1),5(a,1,2)),flip(a)].
452 (x /
y) / y = x / (y * y). [para(220(a,1),6(a,1,1))].
554 x \
(y / x) = (x \ y) / x. [para(277(a,1),6(a,1,1)),flip(a)].
737 x *
(((A \ x) \ y) * A) = A * (y * A).
[para(4(a,1),51(a,1,2,1)),flip(a)].
738 A \
(x * (y * A)) = ((A \ x) * y) * A.
[para(51(a,1),5(a,1,2))].
776 ((1
/ A) \ x) * A = A * (x * A). [para(4(a,1),327(a,1,2,1)),flip(a)].
835 (1 /
A) \ x = A * x. [para(776(a,1),6(a,1,1)),rewrite([162(6),6(5)]),flip(a)].
839 (1 /
A) * (A * x) = x. [para(835(a,1),4(a,1,2))].
842 (A *
x) * (1 / A) = A * (x * (1 / A)).
[para(835(a,1),129(a,1)),rewrite([835(10)]),flip(a)].
848 (1 /
A) * x = A \ x. [para(4(a,1),839(a,1,2))].
851 (x *
A) * (1 / A) = x. [para(839(a,1),18(a,1,1)),rewrite([291(5),3(2),9(7),842(11),848(12),5(10)]),flip(a)].
872 (A *
(x * A)) / (y * A) = A * (x / y).
[para(7(a,1),53(a,1,1,2,1))].
895 (x *
A) * (A \ x) = x * x. [para(848(a,1),16(a,1,2)),rewrite([291(10),2(7)])].
915 x *
(1 / A) = x / A. [para(7(a,1),851(a,1,1))].
916 (x *
A) * (1 / (A * A)) = x / A. [para(851(a,1),12(a,1,1)),rewrite([915(4),915(11),452(9)]),flip(a)].
923 (x /
A) * x = x * (A \ x). [para(851(a,1),47(a,1,2)),rewrite([915(9),452(7),916(8),915(9),6(7),915(12),6(10),848(7)])].
981 (A *
(x / ((y / A) * (y / A)))) * y = A * ((x / (y / A)) * A). [para(220(a,1),54(a,1,2,1)),flip(a)].
1076 (x
/ A) * (x / A) = x * ((A \ x) / A).
[para(7(a,1),895(a,1,1)),rewrite([554(4)]),flip(a)].
1103 (A
* (x / (y * ((A \ y) / A)))) * y = A * ((x / (y / A)) * A). [back_rewrite(981),rewrite([1076(6)])].
1587 (x
* A) \ (x * (y * x)) = (A \ y) * x.
[para(4(a,1),62(a,1,2,2,1))].
1908 x \
((x * A) * y) = (A * (y / x)) * x.
[para(65(a,1),5(a,1,2))].
3556 x \
(y * (A * x)) = ((x \ y) * A) * x.
[para(76(a,1),5(a,1,2))].
3871 (x
* (y * x)) / (A * x) = x * (y / A).
[para(7(a,1),79(a,1,1,2,1))].
18163 x
\ (A * (y * A)) = ((A \ x) \ y) * A.
[para(737(a,1),5(a,1,2))].
18254
((A \ x) * (y / A)) * A = A \ (x * y).
[para(7(a,1),738(a,1,2,2)),flip(a)].
19054 (A
* x) / (y * A) = A * ((x / A) / y).
[para(7(a,1),872(a,1,1,2))].
19055 (A
* (x * A)) / y = A * (x / (y / A)).
[para(7(a,1),872(a,1,2))].
19056 (x
* A) / (y * A) = A * ((A \ x) / y).
[para(33(a,1),872(a,1,1))].
20291 (x
* ((A \ x) / A)) * y = (x / A) * ((x / A) * y). [para(1076(a,1),11(a,1,1))].
21276 (x
* A) \ (x * y) = (A \ (y / x)) * x.
[para(7(a,1),1587(a,1,2,2))].
27232 (x
* y) / (A * x) = x * ((y / x) / A).
[para(7(a,1),3871(a,1,1,2))].
28727
((A \ x) \ (y / A)) * A = x \ (A * y).
[para(7(a,1),18163(a,1,2,2)),flip(a)].
28841 (A
\ (x * y)) / A = (A \ x) * (y / A).
[para(18254(a,1),6(a,1,1))].
29097 A
* (((A \ x) / A) / y) = x / (y * A).
[para(4(a,1),19054(a,1,1)),flip(a)].
29163 A
* ((A \ x) / (y / A)) = (x * A) / y.
[para(33(a,1),19055(a,1,1)),flip(a)].
29491 (A
\ ((x \ y) / x)) * x = (x * A) \ y.
[para(4(a,1),21276(a,1,2)),flip(a)].
29505 (A
\ ((x \ y) / (x * x))) * x = (x * A) \ (y / x). [para(379(a,1),21276(a,1,2)),rewrite([452(8)]),flip(a)].
30459 (x
* (A \ x)) * y = x * (A \ (x * y)).
[para(7(a,1),344(a,1,2)),rewrite([18254(11)])].
31668 x
* (((x \ y) / x) / A) = y / (A * x).
[para(4(a,1),27232(a,1,1)),flip(a)].
31675 x
* (((x \ y) / (x * x)) / A) = (y / x) / (A * x). [para(379(a,1),27232(a,1,1)),rewrite([452(7)]),flip(a)].
33150 (A
\ x) \ ((y / A) * x) = (x \ (A * y)) * (A \ x). [para(28727(a,1),3556(a,2,1)),rewrite([4(8)])].
33452 (A
\ (x / y)) * (y / A) = (A \ x) / A.
[para(7(a,1),28841(a,1,1,2)),flip(a)].
33974 (x
/ A) \ (x * (A \ y)) = ((y * A) / x) * (x / A). [para(29163(a,1),1908(a,2,1)),rewrite([7(6)])].
34461 (x
* A) \ ((x \ y) / x) = ((x * (x * A)) \ y) / x. [para(29491(a,1),45(a,1,1)),rewrite([11(3),394(8),29505(12)]),flip(a)].
34957 x
* (A \ (x * ((x * (A \ x)) \ y))) = y.
[para(30459(a,1),4(a,1))].
35674 x
* (((x \ y) / x) / (A * x)) = y / (A * (x * x)). [para(31668(a,1),11(a,1)),rewrite([394(6),31675(11)]),flip(a)].
36697
((A \ x) / A) / (y / A) = A \ (x / y).
[para(33452(a,1),6(a,1,1))].
38054 A
\ (x * ((x * (A \ x)) \ y)) = x \ y.
[para(34957(a,1),5(a,1,2)),flip(a)].
39635 x
* ((x * (A \ x)) \ y) = A * (x \ y).
[para(38054(a,1),4(a,1,2)),flip(a)].
40283 (x
* (A \ x)) \ y = x \ (A * (x \ y)).
[para(39635(a,1),5(a,1,2)),flip(a)].
43237 (x
/ (y * (A \ y))) * y = (x / y) * A.
[para(29097(a,1),1103(a,1,1)),rewrite([20291(7),7(6),923(3),36697(13),33(12)])].
43244
((x / y) * A) / y = x / (y * (A \ y)).
[para(43237(a,1),6(a,1,1))].
43304 (x
* y) / (y * (A \ y)) = (x * A) / y.
[para(6(a,1),43244(a,1,1,1)),flip(a)].
45785 (x
\ (y * A)) / x = (x \ y) / (x / A).
[para(33974(a,1),34461(a,1,2,1)),rewrite([7(4),6(9),554(4),7(10),923(7),40283(11),5(9),4(8)])].
45805 x
* ((x \ y) / (x / A)) = (y * A) / x.
[para(45785(a,1),162(a,2,2)),rewrite([4(4)]),flip(a)].
45962
((x * y) * A) / x = x * (y / (x / A)).
[para(5(a,1),45805(a,1,2,1)),flip(a)].
46111 A
* ((A \ (x * ((A * y) * x))) / x) = (x * A) * y. [para(16(a,1),45962(a,1,1,1)),rewrite([19056(9),6(16),6(13)])].
46663 (A
\ x) * ((x \ (A * y)) / x) = y / x.
[para(33150(a,1),35674(a,1,2,1,1)),rewrite([6(11),4(9),43(17),43304(14),7(11)])].
46674 (A
\ x) * ((x \ y) / x) = (A \ y) / x.
[para(4(a,1),46663(a,1,2,1,2))].
46698 (A
\ (x * y)) / x = (A \ x) * (y / x).
[para(5(a,1),46674(a,1,2,1)),flip(a)].
46727 A
* ((A \ x) * (A * y)) = (x * A) * y.
[back_rewrite(46111),rewrite([46698(8),6(7)])].
47192 (A
* (x * A)) * y = A * (x * (A * y)).
[para(5(a,1),46727(a,1,2,1)),rewrite([9(9)]),flip(a)].
47193
$F. [resolve(47192,a,26,a)].
==============================
end of proof ==========================
% Length
of proof is 14.
% Level
of proof is 5.
%
Maximum clause weight is 15.
% Given
clauses 416.
1 ((x *
A) * y) * A = x * (A * (y * A)) # label(non_clause) #
label(goal). [goal].
4 x * (x
\ y) = y. [assumption].
8 x * (y
* x) = (x * y) * x. [assumption].
9 (x *
y) * x = x * (y * x).
[copy(8),flip(a)].
13 A *
((x * y) * A) = (A * x) * (y * A).
[assumption].
14 (A *
x) * (y * A) = A * ((x * y) * A).
[copy(13),flip(a)].
25 A *
(x * (A * y)) = ((A * x) * A) * y.
[assumption].
26 (A *
(x * A)) * y = A * (x * (A * y)).
[copy(25),rewrite([9(9)]),flip(a)].
27 ((c1
* A) * c2) * A != c1 * (A * (c2 * A)).
[deny(1)].
34 x *
((x \ y) * x) = y * x. [para(4(a,1),9(a,1,1)),flip(a)].
52 A *
(((A \ x) * y) * A) = x * (y * A).
[para(4(a,1),14(a,1,1)),flip(a)].
166 A *
((A \ x) * (A * y)) = (x * A) * y.
[para(34(a,1),26(a,1,1)),flip(a)].
14665
((x * A) * y) * A = x * (A * (y * A)).
[para(166(a,1),9(a,1,1)),rewrite([52(14),9(9)])].
14666
$F. [resolve(14665,a,27,a)].
==============================
end of proof ==========================
% Length
of proof is 15.
% Level
of proof is 4.
%
Maximum clause weight is 19.
% Given
clauses 463.
1 z * (x
* (z * A)) = ((z * x) * z) * A # label(non_clause) #
label(goal). [goal].
4 x * (x
\ y) = y. [assumption].
8 x * (y
* x) = (x * y) * x. [assumption].
9 (x *
y) * x = x * (y * x).
[copy(8),flip(a)].
13 A *
((x * y) * A) = (A * x) * (y * A).
[assumption].
14 (A *
x) * (y * A) = A * ((x * y) * A).
[copy(13),flip(a)].
15 x *
((A * y) * x) = (x * A) * (y * x).
[assumption].
16 (x *
A) * (y * x) = x * ((A * y) * x).
[copy(15),flip(a)].
27 ((x *
A) * y) * A = x * (A * (y * A)).
[assumption].
28 ((c1
* c2) * c1) * A != c1 * (c2 * (c1 * A)).
[deny(1)].
29 (c1 *
(c2 * c1)) * A != c1 * (c2 * (c1 * A)).
[copy(28),rewrite([9(5)])].
54 A *
(((A \ x) * y) * A) = x * (y * A).
[para(4(a,1),14(a,1,1)),flip(a)].
167 (x *
((A * y) * x)) * A = x * (A * ((y * x) * A)). [para(16(a,1),27(a,1,1))].
18784 (x
* (y * x)) * A = x * (y * (x * A)).
[para(4(a,1),167(a,1,1,2,1)),rewrite([54(11)])].
18785
$F. [resolve(18784,a,29,a)].
==============================
end of proof ==========================
% Length
of proof is 46.
% Level
of proof is 9.
%
Maximum clause weight is 23.
% Given
clauses 1317.
1 ((A *
z) * y) * z = A * (z * (y * z)) # label(non_clause) #
label(goal). [goal].
4 x * (x
\ y) = y. [assumption].
5 x \ (x
* y) = y. [assumption].
6 (x *
y) / y = x. [assumption].
7 (x /
y) * y = x. [assumption].
8 x * (y
* x) = (x * y) * x. [assumption].
9 (x *
y) * x = x * (y * x).
[copy(8),flip(a)].
10 x *
(x * y) = (x * x) * y.
[assumption].
11 (x *
x) * y = x * (x * y).
[copy(10),flip(a)].
12 (x *
y) * y = x * (y * y).
[assumption].
13 A *
((x * y) * A) = (A * x) * (y * A).
[assumption].
14 (A *
x) * (y * A) = A * ((x * y) * A).
[copy(13),flip(a)].
17 x *
((y * A) * x) = (x * y) * (A * x).
[assumption].
18 (x *
y) * (A * x) = x * ((y * A) * x).
[copy(17),flip(a)].
25 A *
(x * (A * y)) = ((A * x) * A) * y.
[assumption].
26 (A *
(x * A)) * y = A * (x * (A * y)).
[copy(25),rewrite([9(9)]),flip(a)].
27 ((x *
A) * y) * A = x * (A * (y * A)).
[assumption].
28 x *
(y * (x * A)) = ((x * y) * x) * A.
[assumption].
29 (x *
(y * x)) * A = x * (y * (x * A)).
[copy(28),rewrite([9(6)]),flip(a)].
30 ((A *
c1) * c2) * c1 != A * (c1 * (c2 * c1)).
[deny(1)].
37 x *
((x \ y) * x) = y * x. [para(4(a,1),9(a,1,1)),flip(a)].
44 (x *
(x * y)) / y = x * x. [para(11(a,1),6(a,1,1))].
55 A *
(((A \ x) * y) * A) = x * (y * A).
[para(4(a,1),14(a,1,1)),flip(a)].
58 A *
((x * (y / A)) * A) = (A * x) * y.
[para(7(a,1),14(a,1,2)),flip(a)].
80 x *
(((x \ y) * A) * x) = y * (A * x).
[para(4(a,1),18(a,1,1)),flip(a)].
84 (x /
y) * ((y * A) * (x / y)) = x * (A * (x / y)). [para(7(a,1),18(a,1,1)),flip(a)].
135 A *
((x / A) * (A * y)) = (A * x) * y.
[para(7(a,1),26(a,1,1,2)),flip(a)].
141 (A *
(x * (A * y))) * y = A * (x * (A * (y * y))). [para(26(a,1),12(a,1,1)),rewrite([26(12)])].
172 (x *
(A * (y * (A * x)))) * A = (x * A) * ((y * A) * (x * A)). [para(18(a,1),27(a,2)),rewrite([27(5),9(6),26(5)])].
211 (x *
A) * ((y * A) * (x * A)) = x * (A * (y * (A * (x * A)))). [para(26(a,1),29(a,1,1,2)),rewrite([172(8),14(15),27(14)])].
218 x \
(y * x) = (x \ y) * x. [para(37(a,1),5(a,1,2))].
226 (((A
\ x) * A) * y) * (x * A) = (A \ x) * (A * (y * (x * A))). [para(37(a,1),18(a,1,2)),rewrite([211(20),37(17)])].
291 (x *
y) / (x \ y) = x * x. [para(4(a,1),44(a,1,1,2))].
395 (x \
(y / x)) * x = x \ y. [para(7(a,1),218(a,1,2)),flip(a)].
725 x \
(y / x) = (x \ y) / x. [para(395(a,1),6(a,1,1)),flip(a)].
926 A \
(x * (y * A)) = ((A \ x) * y) * A.
[para(55(a,1),5(a,1,2))].
1155 A \
((A * x) * y) = (x * (y / A)) * A.
[para(58(a,1),5(a,1,2))].
3686 x *
(((x \ y) * A) * (x * x)) = (y * (A * x)) * x. [para(80(a,1),9(a,1,1)),rewrite([12(9)]),flip(a)].
4309 (x
* y) * (A * (x * x)) = x * ((y * (A * x)) * x). [para(291(a,1),84(a,1,1)),rewrite([291(7),11(7),3686(6),291(10)]),flip(a)].
10710 (x
* (y / A)) * A = (x / A) * (A * y).
[para(135(a,1),5(a,1,2)),rewrite([1155(5)])].
10876 A
\ ((A * x) * y) = (x / A) * (A * y).
[back_rewrite(1155),rewrite([10710(10)])].
20821 ((A
\ x) / A) * (A * y) = A \ (x * y).
[para(7(a,1),926(a,1,2,2)),rewrite([10710(10)]),flip(a)].
25835 A
\ (x * (y * x)) = ((A \ x) * y) * x.
[para(7(a,1),226(a,1,2)),rewrite([725(4),7(6),725(8),7(13),20821(12)]),flip(a)].
35132
((A \ x) * (y / x)) * x = A \ (x * y).
[para(7(a,1),25835(a,1,2,2)),flip(a)].
40529
((A * x) * y) * x = A * (x * (y * x)).
[para(35132(a,1),141(a,1,1,2)),rewrite([10876(6),135(7),5(9),4309(13),7(11)])].
40530
$F. [resolve(40529,a,30,a)].
==============================
end of proof ==========================