op(500, infix, "==>").

lex([0,m,c,+,==>]).

clear(back_demod).
set(restrict_denials).

assign(max_weight,  5  ).

% *************************
% axioms - equality version
% *************************

formulas(assumptions).

%
% The (0, +) substructure is a commutative monoid:
%
   (x + y) + z = x + (y + z).
   x + y = y + x.
   x + 0 = x.
%
% imp-self:
%
   x ==> x = 0.
%
% imp-zero:
%
   x ==> 0 = 0.
%
% zero-imp:
%
   0 ==> x = x.
%
% conj-imp:
%
   (x + y) ==> z = x ==> (y ==> z) # label("conj-imp").
%
% cwc:
%
   x + (x ==> y) = y + (y ==> x) # label("cwc").
%
% abbreviations:
%
   c(x,y) = x + (x ==> y) # label("weak conjunction").
   m(x,y) = x ==> (x + y) # label("strong implication").
%

end_of_list.

formulas(goals).

%
% Strong implication m(x,y) and weak conjunction c(x,y) form an "adjunction"
%
   m(c(x,y),z) = m(x,m(y,z)) # label("main conjecture").

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

(x + y) + z = x + (y + z).
x + y = y + x.
x + 0 = x.
x ==> x = 0.
x ==> 0 = 0.
0 ==> x = x.
(x + y) ==> z = x ==> (y ==> z).
x + (x ==> y) = y + (y ==> x).
c(x,y) = x + (x ==> y).
x + (x ==> y) = c(x,y).
m(x,y) = x ==> (x + y).
x ==> (x + y) = m(x,y).
(x + y) + z = y + (x + z).
x = 0 + x.
0 + x = x.
(x + y) ==> z = y ==> (x ==> z).
x ==> (y ==> (x + y)) = 0.
((x ==> y) + x) ==> y = 0.
c(x + y,z) = x + (y + ((x + y) ==> z)).
x + (y + ((x + y) ==> z)) = c(x + y,z).
x + 0 = c(x,0).
c(x,y) ==> z = x ==> ((x ==> y) ==> z).
x ==> ((x ==> y) ==> z) = c(x,y) ==> z.
c(x,y) = y + (y ==> x).
x + (x ==> y) = c(y,x).
x ==> (y + x) = m(x,y).
m(0,x) = 0 + x.
0 + x = m(0,x).
x + m(x,y) = c(x,x + y).
c(x,0) = x.
m(0,x) = x.
(x + (x ==> y)) ==> y = 0.
c(x,y) = c(y,x).
x ==> c(y,x) = m(x,x ==> y).
x ==> (y + (z + x)) = m(x,y + z).
m(x + y,z) = x ==> (y ==> (z + (x + y))).
x ==> (y ==> (z + (x + y))) = m(x + y,z).
(x ==> y) ==> c(x,y) = m(x ==> y,x).
x ==> m(y,x) = 0.
(x ==> y) ==> c(y,x) = m(x ==> y,x).
x + 0 = c(x,m(y,x)).
c(x,m(y,x)) = x + 0.
0 = x ==> ((x ==> y) ==> y).
x ==> ((x ==> y) ==> y) = 0.
c(x,y) ==> y = 0.
c(x,y) ==> x = 0.
c(x,m(y,x)) = x.
x + 0 = c(x,(x ==> y) ==> y).
c(x,(x ==> y) ==> y) = x + 0.
x + (y + z) = y + (x + z).
x ==> (y ==> z) = y ==> (x ==> z).
m(x,y) ==> c(x,x + y) = m(m(x,y),x).
c(x,(x ==> y) ==> y) = x.
x + c(y,z) = y + (x + (y ==> z)).
x + (y + (x ==> z)) = y + c(x,z).
x ==> 0 = y ==> (x ==> y).
x ==> (y ==> x) = y ==> 0.
x + (y ==> (x ==> z)) = c(x,y ==> z).
x ==> m(y,z) = y ==> (x ==> (y + z)).
x ==> (y ==> (x + z)) = y ==> m(x,z).
x ==> 0 = c(y,z) ==> (x ==> y).
c(x,y) ==> (z ==> x) = z ==> 0.
x ==> (y ==> x) = 0.
x + 0 = c(x,y ==> x).
c(x,y ==> x) = x + 0.
c(x,y ==> x) = x.
(x ==> y) + ((x ==> y) ==> y) = y.
c(x,y) ==> (z ==> x) = 0.
((x ==> y) ==> y) ==> y = m((x ==> y) ==> y,x ==> y).
x + (c(x,y) ==> z) = c(x,(x ==> y) ==> z).
c(x,(x ==> y) ==> z) = x + (c(x,y) ==> z).
x ==> (m(x,y) ==> z) = c(x,y + x) ==> z.
c(x,y + x) ==> z = x ==> (m(x,y) ==> z).
c(c(x,y),z) ==> x = 0.
c(x,c(y,z)) ==> y = 0.
x ==> m(y ==> z,y) = (y ==> z) ==> (x ==> c(y,z)).
(x ==> y) ==> (z ==> c(x,y)) = z ==> m(x ==> y,x).
(m(x,y) ==> y) ==> y = m(m(x,y) ==> y,m(x,y)).
x + 0 = c(x,c(y,x ==> z) ==> z).
c(x,c(y,x ==> z) ==> z) = x + 0.
(x ==> y) + (c(x,y) ==> z) = c(x ==> y,x ==> z).
(x ==> y) ==> m(x,z) = c(x,y) ==> (x + z).
c(x,c(y,x ==> z) ==> z) = x.
x + (y + (x ==> (y ==> z))) = c(x + y,z).
x ==> m(y,z + x) = m(x + y,z).
x ==> m(y,x + z) = m(x + y,z).
x ==> m(y,x + z) = m(y + x,z).
c(x,(x ==> y) ==> z) = x + (c(y,x) ==> z).
c(x + y,z) = y + c(x,y ==> z).
x + c(y,x ==> z) = c(x + y,z).
c(x + y,m(z,y)) = y + c(x,0).
c(x + y,x) = y + x.
x + y = c(y,y + x).
c(x,x + y) = y + x.
c(x,x + y) = x + y.
x + m(x,y) = y + x.
m(x,y) ==> (y + x) = m(m(x,y),x).
c(x,y + x) = x + y.
x + m(x,y) = x + y.
c(x,y + z) ==> y = 0.
x ==> m(y,z + x) = m(x + y,m(x,z)).
(x + y) ==> z = x ==> (m(x,y) ==> z).
x ==> (x + y) = m(x,m(x,y)).
c(x,(x ==> (y + z)) ==> y) = x + 0.
m(x,m(x,y)) = m(x,y).
x ==> c(x + y,z) = m(x,c(y,x ==> z)).
c(x,y ==> z) ==> c(y + x,z) = m(c(x,y ==> z),y).
c(x + y,m(z,y)) = y + x.
x ==> (m(x,y) ==> z) = x ==> (y ==> z).
c(x,(x ==> (y + z)) ==> y) = x.
c(x ==> (y + z),x ==> y) = x ==> (y + z).
x + (x ==> (y ==> z)) = c(x,m(x,y) ==> z).
c(x,m(x,y) ==> z) = x + (x ==> (y ==> z)).
x ==> (y ==> (x + z)) = m(x,y) ==> m(x,z).
m(x,y) ==> m(x,z) = x ==> (y ==> (x + z)).
c(x ==> y,((x ==> y) ==> y) ==> z) = (x ==> y) + (y ==> z).
m(x + y,m(x,z)) = m(x + y,z).
m(c(x,y),m(x,z)) = m(x + (x ==> y),z).
m(x + (x ==> y),z) = m(c(x,y),m(x,z)).
x ==> (y + z) = c(x ==> y,x ==> (y + z)).
c(x ==> y,x ==> (y + z)) = x ==> (y + z).
c(x,m(x,y) ==> z) = c(x,y ==> z).
m(x,y) ==> m(x,z) = y ==> m(x,z).
m(c(x,y),z) = m(c(x,y),m(x,z)).
m(c(x,y),m(x,z)) = m(c(x,y),z).
m(c(x,y),m(y,z)) = m(c(y,x),z).
m(x,m(m(y,x),z)) = m(c(m(y,x),x),z).
m(c(m(x,y),y),z) = m(y,m(m(x,y),z)).
m(x,m(y ==> x,z)) = m(c(y ==> x,x),z).
m(c(x ==> y,y),z) = m(y,m(x ==> y,z)).
c(x ==> y,x ==> c(y,z)) = x ==> (y + (y ==> z)).
x ==> (y + (y ==> z)) = c(x ==> y,x ==> c(y,z)).
m(c(x,m(y,x)),z) = m(x,m(m(y,x),z)).
m(c(x,y ==> x),z) = m(x,m(y ==> x,z)).
m(x,y) = m(x,m(m(z,x),y)).
m(x,m(m(y,x),z)) = m(x,z).
x + m(x,y) = m(m(z,x),y) + x.
m(m(x,y),z) + y = y + m(y,z).
m(m(m(x,y),z),m(m(y,z),u)) = m(m(m(x,y),z),u).
m(m(x,y),z) + y = z + y.
x + y = y + m(m(z,y),x).
x + m(m(y,x),z) = z + x.
m(m(x,y),z) ==> (z + y) = m(m(m(x,y),z),y).
m(x,y) = m(x,m(z ==> x,y)).
m(x,m(y ==> x,z)) = m(x,z).
(x ==> y) + (c(y,x) ==> z) = c(x ==> y,x ==> z).
x ==> c(y,z) = c(x ==> y,x ==> c(y,z)).
c(x ==> y,x ==> c(y,z)) = x ==> c(y,z).
c(x ==> y,m(x,x ==> y)) = x ==> c(y,x).
x ==> c(y,x) = c(x ==> y,m(x,x ==> y)).
(x ==> y) + (c(x,y) ==> c(y,z)) = x ==> c(y,z).
x ==> c(y,x) = x ==> y.
x ==> c(x,y) = x ==> y.
x ==> y = m(x,x ==> y).
m(x,x ==> y) = x ==> y.
x ==> (y ==> z) = y ==> (x ==> c(y,z)).
x ==> (y ==> c(x,z)) = y ==> (x ==> z).
m(x,y ==> m(x,z)) = x ==> (y ==> (x + z)).
x ==> (y ==> (x + z)) = m(x,y ==> m(x,z)).
m(x,m(x + y,z)) = x ==> m(y,z + x).
x ==> m(y,z + x) = m(x,m(x + y,z)).
(x ==> y) ==> (x ==> z) = c(x,y) ==> c(x,z).
m(x,y ==> m(x,z)) = y ==> m(x,z).
m(x,m(x + y,z)) = m(x + y,z).
m(x,m(c(x,y),z)) = m(x + (x ==> y),z).
m(x + (x ==> y),z) = m(x,m(c(x,y),z)).
c(x,y) ==> c(x,z) = x ==> ((x ==> y) ==> z).
x ==> ((x ==> y) ==> z) = c(x,y) ==> c(x,z).
m(c(x,y),z) = m(x,m(c(x,y),z)).
m(x,m(c(x,y),z)) = m(c(x,y),z).
m(x,m(c(y,x),z)) = m(c(x,y),z).
m(c(x,y),z) = m(x,m(c(y,x),z)).
m(c(x,y),z) = m(y,m(c(x,y),z)).
m(x,m(c(y,x),z)) = m(c(y,x),z).
m(m(x,y),m(y,z)) = m(c(y,m(x,y)),z).
m(c(x,m(y,x)),z) = m(m(y,x),m(x,z)).
m((x ==> y) ==> y,m(x,z)) = m(c(x,(x ==> y) ==> y),z).
m(c(x,(x ==> y) ==> y),z) = m((x ==> y) ==> y,m(x,z)).
c(x,y) ==> c(x,z) = c(x,y) ==> z.
c(x,y) ==> c(y,z) = c(y,x) ==> z.
m(x,y) = m(m(z,x),m(x,y)).
m(m(x,y),m(y,z)) = m(y,z).
m(m(x,y),x) ==> (x + m(x,y)) = m(x,y).
m(m(x,y),x) ==> (x + y) = m(x,y).
m(m(m(x,y),x),y) = m(x,y).
m(c(m(m(x,y),x),z),m(x,y)) = m(c(m(m(x,y),x),z),y).
(x ==> y) + (c(y,x) ==> z) = x ==> c(y,z).
x ==> c(y,z) = c(x ==> y,x ==> z).
x ==> c(x + y,z) = c(m(x,y),x ==> z).
c(m(x,y),x ==> z) = m(x,c(y,x ==> z)).
c(m(x,y),m(x,z)) = m(x,c(y,x ==> (x + z))).
m(x,c(y,x ==> (x + z))) = c(m(x,y),m(x,z)).
(m(x,y) ==> (x ==> z)) ==> m(x,c(y,x ==> z)) = m(m(x,y) ==> (x ==> z),m(x,y)).
m(x,c(y,m(x,z))) = c(m(x,y),m(x,z)).
c(m(x,y),m(x,z)) = m(x,c(y,m(x,z))).
c(m(x,y + z),m(x,z)) = m(x,z + y).
m(x,y + z) = c(m(x,z + y),m(x,y)).
m(x,y + z) = c(m(x,y),m(x,z + y)).
m(x,y + z) = c(m(x,y),m(x,y + z)).
c(m(x,y),m(x,y + z)) = m(x,y + z).
m(x,y) + (m(x,y) ==> m(x,y + z)) = m(x,y + z).
m(m(m(x,m(y,z)),y),m(y,z)) = m(m(m(x,m(y,z)),y),z).
m(x,y) = m((x ==> z) ==> z,m(x,y)).
m((x ==> y) ==> y,m(x,z)) = m(x,z).
m((x ==> y) ==> y,x ==> z) = m(x,x ==> z).
m((x ==> y) ==> y,x ==> z) = x ==> z.
((x ==> y) ==> y) ==> y = x ==> y.
x ==> (y ==> z) = ((y ==> z) ==> z) ==> (x ==> z).
((x ==> y) ==> y) ==> (z ==> y) = z ==> (x ==> y).
((x ==> y) ==> y) ==> c(y,z) = c(x ==> y,((x ==> y) ==> y) ==> z).
m(x,y) + (y ==> m(x,y + z)) = m(x,y + z).
m(x,y) + m(y + x,z) = m(x,y + z).
m(x,y) + m(x + y,z) = m(x,y + z).
m(x,y) + m(y + m(m(x,y),x),z) = m(m(m(x,y),x),y + z).
m(m(m(x,m(y,z)),y),z) = m(y,z).
((x ==> y) ==> y) ==> c(y,z) = (x ==> y) + (y ==> z).
m(x,y) + m(x + y,z) = m(m(m(x,y),x),y + z).
m(m(m(x,y),x),y + z) = m(x,y + z).
x ==> m(y,z + x) = m(x + m(m(y,z),y),z).
m(x + m(m(y,z),y),z) = m(x + y,z).
m(x + m(m(y,z),m(m(u,m(y,z)),y)),z) = m(x + m(m(u,m(y,z)),y),z).
(x ==> (m(x,y) ==> z)) ==> m(x,c(y,x ==> z)) = m(m(x,y) ==> (x ==> z),m(x,y)).
m(x + m(m(y,z),y),z) = m(x + m(m(u,m(y,z)),y),z).
m(x + m(m(y,m(z,u)),z),u) = m(x + m(m(z,u),z),u).
m(x + m(m(y,m(z,u)),z),u) = m(x + z,u).
(x ==> (y ==> z)) ==> m(x,c(y,x ==> z)) = m(m(x,y) ==> (x ==> z),m(x,y)).
m(m(x,y) ==> (x ==> z),m(x,y)) = c(x,y ==> z) ==> (x + c(y,x ==> z)).
c(x,y ==> z) ==> (x + c(y,x ==> z)) = m(m(x,y) ==> (x ==> z),m(x,y)).
c(x,y ==> z) ==> c(y + x,z) = m(m(x,y) ==> (x ==> z),m(x,y)).
m(m(x,y) ==> (x ==> z),m(x,y)) = m(c(x,y ==> z),y).
m(x ==> (m(x,y) ==> z),m(x,y)) = m(c(x,y ==> z),y).
m(x ==> (y ==> z),m(x,y)) = m(c(x,y ==> z),y).
m(x ==> y,m(c(z,x ==> y),x)) = m(x ==> y,m(z,x)).
m(c(x ==> y,z),x) = m(x ==> y,m(z,x)).
m(x ==> y,m(z,x)) = m(c(z,x ==> y),x).
m(c(x,y ==> z),y) = m(y ==> z,m(x,y)).
m(c(m(x,y),z),x) = m(x ==> (x + y),m(z,x)).
m(c(x,m(x,y) ==> z),m(x,y)) = m(m(x,y) ==> z,m(x,y)).
m(c(m(x,y),z),x) = m(m(x,y),m(z,x)).
m(m(m(x,y),x),m(z,m(x,y))) = m(c(m(m(x,y),x),z),y).
m(c(m(m(x,y),x),z),y) = m(m(m(x,y),x),m(z,m(x,y))).
m(c(x,y ==> z),m(x,y)) = m(m(x,y) ==> z,m(x,y)).
m(m(x,y) ==> z,m(x,y)) = m(c(x,y ==> z),m(x,y)).
m(m(x,y) ==> z,m(x,y)) = m(c(x,y ==> z),y).
m(m(x,y) ==> z,m(x,y)) = m(y ==> z,m(x,y)).
(m(x,y) ==> y) ==> y = m(y ==> y,m(x,y)).
(m(x,y) ==> y) ==> y = m(0,m(x,y)).
(m(x,y) ==> y) ==> y = m(x,y).
x ==> m(y,z) = (m(y,z) ==> z) ==> (x ==> z).
(m(x,y) ==> y) ==> (z ==> y) = z ==> m(x,y).
m(x,m(y,m(x,z))) = (m(y,m(x,z)) ==> m(x,z)) ==> m(x,z).
(m(x,m(y,z)) ==> m(y,z)) ==> m(y,z) = m(y,m(x,m(y,z))).
((x ==> y) ==> y) ==> m(z,y) = (m(z,y) ==> y) ==> (x ==> y).
(m(x,y) ==> y) ==> (z ==> y) = ((z ==> y) ==> y) ==> m(x,y).
((x ==> y) ==> y) ==> m(z,y) = x ==> m(z,y).
(x ==> y) ==> (((z ==> x) ==> x) ==> c(x,y)) = z ==> m(x ==> y,x).
m(x,m(y,m(x,z))) = m(y,m(x,z)).
m(m(x,y),m(z,m(y,u))) = m(y,m(z,m(y,u))).
m(m(x,y),m(z,m(y,u))) = m(z,m(y,u)).
m(c(m(m(x,y),x),z),y) = m(z,m(x,y)).
m(c(x,m(m(y,z),y)),z) = m(x,m(y,z)).
(x ==> y) ==> ((z ==> x) + (x ==> y)) = z ==> m(x ==> y,x).
x ==> m(y ==> z,y) = m(y ==> z,x ==> y).
x ==> m(m(y,z),y) = m(y ==> (y + z),x ==> y).
m(x ==> (x + y),z ==> x) = z ==> m(m(x,y),x).
m(m(x,y),z ==> x) = z ==> m(m(x,y),x).
x ==> m(m(y,z),y) = m(m(y,z),x ==> y).
x + m(m(y,z),x ==> y) = c(x,m(m(y,z),y)).
m(c(x,m(m(y,m(x ==> y,z)),y)),z) = m(x + (x ==> y),z).
m(c(x,m(m(y,z),y)),z) = m(x + (x ==> y),z).
m(x + (x ==> y),z) = m(x,m(y,z)).

end_of_list.
