% Length of proof is 9.
% Level of proof is 4.
% Maximum clause weight is 11.
% Given clauses 13.
1 (A / A) * x = x # label(non_clause) #
label(goal). [goal].
3 x * (x \ y) = y. [assumption].
6 (x / y) * y = x. [assumption].
7 x * (A * y) = (x * A) * y. [assumption].
8 (x * A) * y = x * (A * y). [copy(7),flip(a)].
9 (A / A) * c1 != c1. [deny(1)].
16 (x / A) * (A * y) = x * y. [para(6(a,1),8(a,1,1)),flip(a)].
26 (x / A) * y = x * (A \ y). [para(3(a,1),16(a,1,2))].
29 $F.
[back_rewrite(9),rewrite([26(5),3(5)]),xx(a)].
============================== end of proof
==========================
% Length
of proof is 22.
% Level
of proof is 8.
%
Maximum clause weight is 11.
% Given
clauses 39.
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 x * (A
* y) = (x * A) * y. [assumption].
8 (x *
A) * y = x * (A * y).
[copy(7),flip(a)].
10 c2 *
(A / A) != c2. [deny(2)].
11 x /
(y \ x) = y.
[para(3(a,1),5(a,1,1))].
15 (x *
(A * y)) / y = x * A. [para(8(a,1),5(a,1,1))].
16 (x /
A) * (A * y) = x * y.
[para(6(a,1),8(a,1,1)),flip(a)].
23 (x *
y) / (A \ y) = x * A.
[para(3(a,1),15(a,1,1,2))].
26 (x /
A) * y = x * (A \ y).
[para(3(a,1),16(a,1,2))].
34 x /
(A \ y) = (x / y) * A.
[para(6(a,1),23(a,1,1))].
40 x *
(A \ A) = x.
[para(26(a,1),6(a,1))].
45 A \ A
= x \ x.
[para(40(a,1),4(a,1,2)),flip(a)].
49 x *
(y \ y) = x.
[para(45(a,1),26(a,2,2)),rewrite([6(4)]),flip(a)].
51 x /
(y \ y) = x.
[para(49(a,1),5(a,1,1))].
68 (x /
x) * A = A. [para(34(a,1),11(a,1))].
70 A / A
= x / x. [para(68(a,1),5(a,1,1))].
81 c2 *
(x / x) != c2.
[para(70(a,1),10(a,1,2))].
103
$F.
[para(51(a,1),81(a,1,2)),rewrite([49(3)]),xx(a)].
==============================
end of proof ==========================