% Proof 1 at 0.36 (+ 0.01) seconds.
% Length of proof is 41.
% Level of proof is 13.
% Maximum clause weight is 45.
% Given clauses 94.

1 (all a all b all c all d (tu(a,b,c,d) <-> (exists e exists f exists g exists h ((a * e) + (b * g) = 1 & (a * f) + (b * h) = 0 & (c * e) + (d * g) = 0 & (c * f) + (d * h) = 1)))) # label(non_clause).  [assumption].
2 (all a all b all c all d all e all f all g all h (tu(a,b,c,d) & tu(e,f,g,h) -> (a * e) + (b * g) = (e * a) + (f * c) & (a * f) + (b * h) = (e * b) + (f * d) & (c * e) + (d * g) = (g * a) + (h * c) & (c * f) + (d * h) = (g * b) + (h * d))) # l…

x+(y+z) = (x+y)+z.
x+0=x.
0+x=x.
x+(-x)=0.
(-x)+x=0.
x+y=y+x.
x*(y*z) = (x*y)*z.
x*(y+z) = (x*y)+(x*z).
(y+z)*x = (y*x)+(z*x).

x*1=x.
all a all b all c all d
(tu(a,b,c,d) <-> exists e exists f exists g exists h (
(a*e)+(b*g)=1 &
(a*f)+(b*h)=0 &
(c*e)+(d*g)=0 &
(c*f)+(d*h)=1)).

all a all b all c all d
all e all f all g all h
((tu(a,b,c,d) & tu(e,f,g,h)) ->
((a*e)+(b*g)=(e*a)+(f*c) &
 (a*f)+(b*h)=(e*b)+(f*d) &
 (c*e)+(d*g)=(g*a)+(h*c) &
 (c*f)+(d*h)=(g*b)+(h*d))).

(exists y x*y=1) -> (x=1).

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.00) seconds.
% Length of proof is 12.
% Level of proof is 6.
% Maximum clause weight is 11.
% Given clauses 9.

1 0 + x = x # label(non_clause) # label(goal).  [goal].
3 x + (y + z) = (x + y) + z.  [assumption].
4 (x + y) + z = x + (y + z).  [copy(3),flip(a)].
5 x + 0 = x.  [assumption].
6 x + -x = 0.  [assumption].
7 0 + c1 != c1.  [deny(1)].
9A x + y = x + (0 + y).  [para(5(a,1),4(a,1,1))].

1 (all x (unit(x) <-> (exists y x * y = 1))) # label(non_clause).  [assumption].
2 (all x all y (unit(x) & unit(y) -> unit(x * y))) # label(non_clause) # label(goal).  [goal].
9 x * (y * z) = (x * y) * z.  [assumption].
10 (x * y) * z = x * (y * z).  [copy(9),flip(a)].
12 1 * x = x.  [assumption].
13 -unit(x) | x * f1(x) = 1.  [clausify(1)].
14 unit(x) | x * y != 1.  [clausify(1)].
15 unit(c1).  [deny(2)].
16 unit(c2).  [deny(2)].
17 -unit(c1 * c2).  [deny(2)].
25 c1 * f1(c1) = 1.  [hyper(13,a,15,a)].

x+(y+z) = (x+y)+z.
x+0=x.
0+x=x.
x+(-x)=0.
(-x)+x=0.
x+y=y+x.

x*(y*z) = (x*y)*z.
x*1=x.
1*x=x.
0!=1.

x*(y+z) = (x*y)+(x*z).
(y+z)*x = (y*x)+(z*x).

(x<=y & y<=x) -> x=y.
(x<=y & y<=z) -> x<=z.
x<=y | y<=x.
x<=y -> (x+z)<=(y+z).
(0<=x & 0<=y) -> 0<=(x*y).

all x all y (x<y <-> (x<=y & x!=y)).

0<1.

2 x <= y & y <= z -> x <= z # label(non_clause).  [assumption].
3 x <= y -> x + z <= y + z # label(non_clause).  [assumption].
4 0 <= x & 0 <= y -> 0 <= x * y # label(non_clause).  [assumption].
5 (all x all y (x < y <-> x <= y & x != y)) # label(non_clause).  [assumption].
6 0 < 1 # label(non_clause) # label(goal).  [goal].
7 x + (y + z) = (x + y) + z.  [assumption].
8 (x + y) + z = x + (y + z).  [copy(7),flip(a)].
9 x + 0 = x.  [assumption].
10 0 + x = x.  [assumption].
11 x + -x = 0.  [assumption].