%
Length of proof is 13.
%
Level of proof is 7.
%
Maximum clause weight is 15.
%
Given clauses 26.
1
(A / A) * x = x # label(non_clause) # label(goal). [goal].
3
x * (x \ y) = y. [assumption].
4
x \ (x * y) = y. [assumption].
5
(x * y) / y = x. [assumption].
7
A * ((x * y) * A) = (A * x) * (y * A).
[assumption].
8
(A * x) * (y * A) = A * ((x * y) * A).
[copy(7),flip(a)].
11
(A / A) * c1 != c1. [deny(1)].
15
A * (((A \ x) * y) * A) = x * (y * A).
[para(3(a,1),8(a,1,1)),flip(a)].
25
A \ (x * (y * A)) = ((A \ x) * y) * A.
[para(15(a,1),4(a,1,2))].
72
((A \ A) * x) * A = x * A.
[para(25(a,1),4(a,1))].
80
(A \ A) * x = x.
[para(72(a,1),5(a,1,1)),rewrite([5(4)]),flip(a)].
83
A \ A = x / x.
[para(80(a,1),5(a,1,1)),flip(a)].
94
$F.
[para(83(a,2),11(a,1,1)),rewrite([80(5)]),xx(a)].
==============================
end of proof ==========================
% Length of proof is 24.
% Level of proof is 11.
% Maximum clause weight is
15.
% Given clauses 44.
2 x * (A / A) = x # label(non_clause)
# label(goal). [goal].
3 x * (x \ y) = y. [assumption].
4 x \ (x * y) = y. [assumption].
5 (x * y) / y = x. [assumption].
7 A * ((x * y) * A) = (A *
x) * (y * A). [assumption].
8 (A * x) * (y * A) = A *
((x * y) * A). [copy(7),flip(a)].
9 A * (x * (A * y)) = ((A
* x) * A) * y. [assumption].
10 ((A * x) * A) * y = A *
(x * (A * y)). [copy(9),flip(a)].
12 c2 * (A / A) !=
c2. [deny(2)].
15 A * (((A \ x) * y) * A)
= x * (y * A).
[para(3(a,1),8(a,1,1)),flip(a)].
24 x * (((A \ x) \ y) * A)
= A * (y * A).
[para(3(a,1),15(a,1,2,1)),flip(a)].
25 A \ (x * (y * A)) = ((A
\ x) * y) * A.
[para(15(a,1),4(a,1,2))].
65 x \ (A * (y * A)) = ((A
\ x) \ y) * A.
[para(24(a,1),4(a,1,2))].
72 ((A \ A) * x) * A = x *
A. [para(25(a,1),4(a,1))].
80 (A \ A) * x = x.
[para(72(a,1),5(a,1,1)),rewrite([5(4)]),flip(a)].
83 A \ A = x / x. [para(80(a,1),5(a,1,1)),flip(a)].
85 (A * A) * x = A * (A *
x).
[para(80(a,1),10(a,2,2)),rewrite([3(5)])].
95 c2 * (A \ A) !=
c2. [para(83(a,2),12(a,1,2))].
114 c2 * (x / x) !=
c2. [para(83(a,1),95(a,1,2))].
129 (A * x) * A = A * (x *
A).
[para(85(a,1),25(a,1,2)),rewrite([4(8),4(9)]),flip(a)].
177 (x \ x) * A = A.
[para(129(a,1),4(a,1,2)),rewrite([65(7),4(4)])].
214 x \ x = A / A. [para(177(a,1),5(a,1,1)),flip(a)].
217 x * (A / A) = x. [para(214(a,1),3(a,1,2))].
218 $F. [resolve(217,a,114,a)].
==============================
end of proof ==========================
%
Length of proof is 22.
%
Level of proof is 9.
%
Maximum clause weight is 15.
%
Given clauses 37.
2
x * (A / A) = x # label(non_clause) # label(goal). [goal].
3
x * (x \ y) = y. [assumption].
4
x \ (x * y) = y. [assumption].
5
(x * y) / y = x. [assumption].
7
A * ((x * y) * A) = (A * x) * (y * A).
[assumption].
8
(A * x) * (y * A) = A * ((x * y) * A).
[copy(7),flip(a)].
9
((x * A) * y) * A = x * (A * (y * A)).
[assumption].
11
c2 * (A / A) != c2. [deny(2)].
14
A * (((A \ x) * y) * A) = x * (y * A).
[para(3(a,1),8(a,1,1)),flip(a)].
19
((x * A) * y) \ (x * (A * (y * A))) = A.
[para(9(a,1),4(a,1,2))].
26
x * (((A \ x) \ y) * A) = A * (y * A).
[para(3(a,1),14(a,1,2,1)),flip(a)].
27
A \ (x * (y * A)) = ((A \ x) * y) * A.
[para(14(a,1),4(a,1,2))].
74
x \ (A * (y * A)) = ((A \ x) \ y) * A.
[para(26(a,1),4(a,1,2))].
84
((A \ A) * x) * A = x * A.
[para(27(a,1),4(a,1))].
92
(A \ A) * x = x.
[para(84(a,1),5(a,1,1)),rewrite([5(4)]),flip(a)].
97
A \ A = x / x.
[para(92(a,1),5(a,1,1)),flip(a)].
100
(x \ x) * A = A.
[para(92(a,1),19(a,1,1,1)),rewrite([92(10),74(7),4(4)])].
135
x / x = y / y.
[para(97(a,1),97(a,1))].
138
x \ x = A / A.
[para(100(a,1),5(a,1,1)),flip(a)].
164
c2 * (x / x) != c2.
[para(135(a,1),11(a,1,2))].
170
x * (A / A) = x.
[para(138(a,1),3(a,1,2))].
171
$F. [resolve(170,a,164,a)].
==============================
end of proof ==========================
% Length of proof is 25.
% Level of proof is 12.
% Maximum clause weight is
15.
% Given clauses 63.
1 (A / A) * x = x #
label(non_clause) # label(goal).
[goal].
3 x * (x \ y) = y. [assumption].
4 x \ (x * y) = y. [assumption].
5 (x * y) / y = x. [assumption].
6 (x / y) * y = x. [assumption].
7 A * (x * (A * y)) = ((A
* x) * A) * y. [assumption].
8 ((A * x) * A) * y = A *
(x * (A * y)). [copy(7),flip(a)].
9 ((x * A) * y) * A = x *
(A * (y * A)). [assumption].
10 (A / A) * c1 !=
c1. [deny(1)].
12 x / (y \ x) = y. [para(3(a,1),5(a,1,1))].
15 A * ((A \ x) * (A * y))
= (x * A) * y.
[para(3(a,1),8(a,1,1,1)),flip(a)].
17 (A * (x * (A * y))) / y
= (A * x) * A.
[para(8(a,1),5(a,1,1))].
21 (x / A) * (A * (y * A))
= (x * y) * A.
[para(6(a,1),9(a,1,1,1)),flip(a)].
29 A \ ((x * A) * y) = (A
\ x) * (A * y).
[para(15(a,1),4(a,1,2))].
37 (A * (x / (A * y))) * A
= (A * x) / y.
[para(6(a,1),17(a,1,1,2)),flip(a)].
81 (A \ (x / A)) * (A * y)
= A \ (x * y).
[para(6(a,1),29(a,1,2,1)),flip(a)].
105 (A * (x / (A * y))) \
((A * x) / y) = A.
[para(37(a,1),4(a,1,2))].
282 (A * (x / (A * x))) \
A = A. [para(5(a,1),105(a,1,2))].
296 (A * ((A \ x) / x)) \
A = A.
[para(3(a,1),282(a,1,1,2,2))].
302 A * ((A \ x) / x) = A
/ A.
[para(296(a,1),12(a,1,2)),flip(a)].
325 A \ (A / A) = (A \ x)
/ x. [para(302(a,1),4(a,1,2))].
371 ((A \ A) * x) * A = x
* A.
[para(325(a,2),21(a,1,1)),rewrite([81(10),4(6)]),flip(a)].
430 (A \ A) * x = x. [para(371(a,1),5(a,1,1)),rewrite([5(4)]),flip(a)].
450 A \ A = x / x. [para(430(a,1),5(a,1,1)),flip(a)].
571 $F.
[para(450(a,2),10(a,1,1)),rewrite([430(5)]),xx(a)].
==============================
end of proof ==========================
% Length of proof is 32.
% Level of proof is 14.
% Maximum clause weight is
15.
% Given clauses 63.
2 x * (A / A) = x #
label(non_clause) # label(goal).
[goal].
3 x * (x \ y) = y. [assumption].
4 x \ (x * y) = y. [assumption].
5 (x * y) / y = x. [assumption].
6 (x / y) * y = x. [assumption].
7 A * (x * (A * y)) = ((A
* x) * A) * y. [assumption].
8 ((A * x) * A) * y = A *
(x * (A * y)). [copy(7),flip(a)].
9 ((x * A) * y) * A = x *
(A * (y * A)). [assumption].
11 c2 * (A / A) !=
c2. [deny(2)].
12 x / (y \ x) = y. [para(3(a,1),5(a,1,1))].
15 A * ((A \ x) * (A * y))
= (x * A) * y.
[para(3(a,1),8(a,1,1,1)),flip(a)].
17 (A * (x * (A * y))) / y
= (A * x) * A.
[para(8(a,1),5(a,1,1))].
18 x * (A * (((x * A) \ y)
* A)) = y * A.
[para(3(a,1),9(a,1,1)),flip(a)].
21 (x / A) * (A * (y * A))
= (x * y) * A. [para(6(a,1),9(a,1,1,1)),flip(a)].
28 (x * A) * (A \ y) = A *
((A \ x) * y).
[para(3(a,1),15(a,1,2,2)),flip(a)].
29 A \ ((x * A) * y) = (A
\ x) * (A * y).
[para(15(a,1),4(a,1,2))].
37 (A * (x / (A * y))) * A
= (A * x) / y.
[para(6(a,1),17(a,1,1,2)),flip(a)].
40 A * (((x * A) \ y) * A)
= x \ (y * A).
[para(18(a,1),4(a,1,2)),flip(a)].
75 A * ((A \ (x / A)) * y)
= x * (A \ y).
[para(6(a,1),28(a,1,1)),flip(a)].
81 (A \ (x / A)) * (A * y)
= A \ (x * y).
[para(6(a,1),29(a,1,2,1)),flip(a)].
105 (A * (x / (A * y))) \
((A * x) / y) = A.
[para(37(a,1),4(a,1,2))].
282 (A * (x / (A * x))) \
A = A. [para(5(a,1),105(a,1,2))].
296 (A * ((A \ x) / x)) \
A = A.
[para(3(a,1),282(a,1,1,2,2))].
302 A * ((A \ x) / x) = A
/ A.
[para(296(a,1),12(a,1,2)),flip(a)].
325 A \ (A / A) = (A \ x)
/ x. [para(302(a,1),4(a,1,2))].
371 ((A \ A) * x) * A = x
* A.
[para(325(a,2),21(a,1,1)),rewrite([81(10),4(6)]),flip(a)].
430 (A \ A) * x = x.
[para(371(a,1),5(a,1,1)),rewrite([5(4)]),flip(a)].
449 (A \ A) \ x = x. [para(430(a,1),3(a,1))].
450 A \ A = x / x. [para(430(a,1),5(a,1,1)),flip(a)].
461 A * ((A \ x) * A) = x
* A.
[para(430(a,1),40(a,1,2,1,1)),rewrite([449(12)])].
579 x * (y / y) = x.
[para(450(a,1),75(a,2,2)),rewrite([461(8),6(4)]),flip(a)].
580 $F. [resolve(579,a,11,a)].
==============================
end of proof ==========================