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

clear(back_demod).
set(restrict_denials).
set(para_from_small).
set(para_into_vars).

assign(max_weight, 5 ).

formulas(assumptions).

% *********************
% axioms (Horn version)
% *********************

%
% The (0, +) substructure is a commutative monoid:
%
   (x + y) + z = x + (y + z).
   x + y = y + x.
   x + 0 = x.
%
% >= is a partial order:
%
   x >= x.
   x >= y & y >= z -> x >= z.
   x >= y & y >= x -> x = y.
%
% Residuation law:
%
   (x + z) >= y <-> z >= (x ==> y).
%
% 0 is the least element:
%
   x >= 0.
%
% Monotonicity laws:
%
   x >= y -> x + z >= y + z.

   x >= y -> y ==> z >= x ==> z.
   x >= y -> z ==> x >= z ==> y.
%
% Weak conjunction is commutative (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").

% ****************
% defined operator
% ****************

   x v y = (y ==> x) ==> x # label("strong disjunction").

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).

m(c(x,y),z) = m(x,m(y,z)).
(x + y) + z = x + (y + z).
x + y = y + x.
x + 0 = x.
x >= x.
-(x >= y) | -(y >= z) | x >= z.
-(x >= y) | -(y >= x) | y = x.
-(x + y >= z) | y >= x ==> z.
x + y >= z | -(y >= x ==> z).
x >= 0.
-(x >= y) | y ==> z >= x ==> z.
-(x >= y) | z ==> x >= z ==> y.
x + (x ==> y) = y + (y ==> x).
c(x,y) = x + (x ==> y).
m(x,y) = x ==> (x + y).
x v y = (y ==> x) ==> x.
m(c(c1,c2),c3) != m(c1,m(c2,c3)).
(x + y) + z = y + (x + z).
x >= y ==> (y + x).
-(x + (y + z) >= u) | z >= (x + y) ==> u.
-(x >= y) | 0 >= x ==> y.
x + (x ==> y) >= y.
x >= y ==> 0.
x + (x ==> (y + z)) = y + (z + ((y + z) ==> x)).
c(x,y) = y + (y ==> x).
m(x,y) = x ==> (y + x).
-(0 >= x) | 0 = x.
0 = x ==> 0.
x ==> 0 = 0.
0 >= x ==> x.
x >= m(y,x).
0 = x ==> x.
x ==> x = 0.
x ==> (y ==> y) = 0.
x ==> (y + (y ==> z)) >= x ==> z.
x + (y + ((x + y) ==> z)) >= z.
(x ==> y) + x >= y.
c(x,y) >= y.
x + c(y,x ==> z) >= z.
x >= (x ==> y) ==> y.
0 ==> x >= x.
x ==> y >= (y v x) ==> y.
x >= y v x.
(x v y) ==> z >= y ==> z.
-(x >= y) | c(z,x) >= y.
c(x,y) >= z v y.
0 >= c(x,y) ==> (z v y).
c(x,y) = c(y,x).
m(x,y + z) = x ==> (y + (z + x)).
-((x v y) ==> x >= y ==> x) | (x v y) ==> x = y ==> x.
(x v y) ==> x = y ==> x.
0 = c(x,y) ==> (z v y).
c(x,y) ==> (z v y) = 0.
x + (y + z) = y + (x + z).
-(x ==> (x + y) >= y) | x ==> (x + y) = y.
x ==> (x + (x ==> y)) = x ==> y.
-(x + (y + z) >= u) | x + z >= y ==> u.
x + (y + (y ==> z)) = z + (x + (z ==> y)).
m(x,y + z) = x ==> (y + (x + z)).
x ==> c(x,y) = x ==> y.
m(x,x ==> y) = x ==> y.
-(x + c(y,z) >= u) | y ==> z >= (x + y) ==> u.
x + ((x + y) ==> z) >= y ==> z.
(x + y) ==> z >= x ==> (y ==> z).
m(x ==> y,z + x) = (x ==> y) ==> (y + (z + (y ==> x))).
m(x,y + (x ==> z)) = x ==> (z + (y + (z ==> x))).
x ==> (y ==> z) >= (y + x) ==> z.
x ==> (y ==> z) >= (x + y) ==> z.
-(x ==> (y ==> z) >= (x + y) ==> z) | x ==> (y ==> z) = (x + y) ==> z.
x ==> (y ==> z) = (x + y) ==> z.
(x + y) ==> z = x ==> (y ==> z).
(x + y) ==> z = y ==> (x ==> z).
c(x,y) ==> z = x ==> ((x ==> y) ==> z).
x v (y + z) = (y ==> (z ==> x)) ==> x.
x ==> (y ==> (x + y)) = 0.
m(x + y,z) = x ==> (y ==> (z + (x + y))).
(x + y) ==> x = 0.
x ==> (y ==> z) = y ==> (x ==> z).
x v (x + y) = 0 ==> x.
0 = x ==> (y ==> x).
x ==> (y ==> x) = 0.
x + (y ==> (z ==> y)) = x.
x = (y ==> x) + ((y ==> x) ==> x).
(x ==> y) + ((x ==> y) ==> y) = y.
x >= y ==> x.
-(x >= 0 ==> x) | x = 0 ==> x.
x = 0 ==> x.
0 ==> x = x.
x v (x + y) = x.
x v c(x,y) = x.
x v c(y,x) = x.
c(x,c(y,z)) ==> y = 0.
x + (y ==> (x ==> z)) = (y ==> z) + ((y ==> z) ==> x).
(x ==> y) + ((x ==> y) ==> z) = z + (x ==> (z ==> y)).
c(x,y ==> z) = x + (y ==> (x ==> z)).
(x ==> y) v z = x ==> ((z ==> (x ==> y)) ==> y).
x ==> (y ==> z) = y ==> (x ==> c(y,z)).
x ==> (y ==> c(x,z)) = y ==> (x ==> z).
(x ==> y) + (y v x) = y.
x = (x v y) + (y ==> x).
(x v y) + (y ==> x) = x.
x + y = (y v z) + (x + (z ==> y)).
(x v y) + (z + (y ==> x)) = z + x.
x v (y + (x v z)) = (y ==> (z ==> x)) ==> x.
c(x ==> y,x ==> z) = (x ==> y) + (c(x,y) ==> z).
c(x,y) ==> c(x,z) = (x ==> y) ==> (x ==> z).
m(x + y,z) = x ==> m(y,z + x).
m(x + y,z) = x ==> m(y,x + z).
m(x,m(x + y,z)) = x ==> m(y,z + x).
m((x v y) + z,y ==> x) = (x v y) ==> m(z,x).
m(x + y,z) = y ==> m(x,y + z).
(x ==> y) v z = x ==> (y v (z + x)).
(x ==> y) v z = x ==> (y v (x + z)).
x v (y + z) = x v (y + (x v z)).
x v (y + (x v z)) = x v (y + z).
(x ==> y) v (y v z) = x ==> (y v (x + z)).
c(x,y) ==> c(x,z) = x ==> ((x ==> y) ==> z).
m(x + y,z) = m(x,m(x + y,z)).
m(x,m(x + y,z)) = m(x + y,z).
m(x + y,z) = x ==> (m(x + y,z) + x).
x ==> (m(x + y,z) + x) = m(x + y,z).
(x ==> y) v z = (x ==> y) v (y v z).
(x ==> y) v (y v z) = (x ==> y) v z.
(x v y) v (x v z) = ((y ==> x) ==> x) v z.
c(x,y) ==> z = c(x,y) ==> c(x,z).
c(x,y) ==> c(x,z) = c(x,y) ==> z.
x ==> ((x v y) + (m(x + z,u) + (y ==> x))) = m(x + z,u).
(x v y) v (x v z) = (x v y) v z.
((x v y) v z) ==> (x v y) = (x v z) ==> (x v y).
(x + (x ==> (y + z))) ==> y = 0.
x + (x ==> (x + y)) = x + (y + 0).
(x + (x ==> (y + z))) ==> z = 0.
0 = x ==> ((x ==> (y + z)) ==> y).
x ==> ((x ==> (y + z)) ==> y) = 0.
0 = x ==> ((x ==> (y + z)) ==> z).
x ==> ((x ==> (y + z)) ==> z) = 0.
x + (y ==> ((y ==> (z + u)) ==> z)) = x.
x ==> (m(x,y) ==> y) = 0.
x + (x ==> (x + y)) = x + y.
x + ((x ==> (x + y)) + 0) = x + y.
x + m(x,y) = x + y.
(x + y) + z = x + (m(x,y) + z).
x + (m(x,y) + z) = (x + y) + z.
(x + y) + z = x + (y + m(x + y,z)).
x + (y + m(x + y,z)) = (x + y) + z.
m(x,y + m(x,z)) = x ==> (y + (x + z)).
(x + y) ==> z = x ==> (m(x,y) ==> z).
x ==> (m(x,y) ==> z) = (x + y) ==> z.
x + ((y ==> (z + u)) ==> (y ==> z)) = x.
x + y = (x ==> (x + y)) + (x + 0).
(x ==> (x + y)) + (x + 0) = x + y.
x + (m(x,y) + z) = x + (y + z).
x ==> (m(x,y) ==> z) = x ==> (y ==> z).
(x ==> (x + y)) + (x + (z ==> (m(z,u) ==> u))) = x + y.
x ==> m(m(x,y),z) = x ==> (y ==> (m(x,y) + z)).
x + (y + m(x + y,z)) = x + (y + z).
m(x,y + z) = m(x,y + m(x,z)).
m(x,y + m(x,z)) = m(x,y + z).
m(x,y + m(x,z)) = m(x,z + y).
m(x + y,m(x,z)) = y ==> m(x,y + z).
m(x,m(x,y) + z) = m(x,y + z).
m(x,y + m(x + y,z)) = x ==> (x + (y + z)).
m(x + y,z) = m(x + y,m(x,z)).
m(x + y,m(x,z)) = m(x + y,z).
m(c(x,y),m(x,z)) = m(x + (x ==> y),z).
m(c(x,y),m(x,z)) = m(c(x,y),z).
m(c(x,y),m(x,z)) = m(c(y,x),z).
m(x,y) >= m(c(x,z),y).
m(x,y) >= m(c(z,x),y).
m(x,m(y,z)) >= m(c(x,y),z).
m(x ==> y,z + (y v x)) = (x ==> y) ==> (y + (z + (y ==> (x ==> y)))).
m(x,m(y,z) + (x ==> y)) = x ==> (y + (z + (y ==> x))).
(x ==> y) + (x ==> ((x ==> y) ==> (y + z))) = x ==> (y + z).
c(x ==> c(y,z),x ==> y) = (x ==> c(y,z)) + 0.
(x v y) ==> (x v z) = y ==> (x v z).
x ==> (y v x) = 0.
x + (y ==> (z v y)) = x.
x ==> 0 = y ==> (x ==> (z v y)).
x ==> (y ==> (z v x)) = y ==> 0.
c(x,y v x) = x.
c(c(x,y),y) = c(x,y).
c(x,y) = c(y,c(x,y)).
c(x,c(y,x)) = c(y,x).
c(x,y) ==> c(y,z) = c(y,c(x,y)) ==> z.
c(x,c(y,x)) ==> z = c(y,x) ==> c(x,z).
x ==> (y ==> (z v x)) = 0.
x ==> (y ==> ((x ==> z) ==> z)) = 0.
c(x,y) ==> z = c(x,y) ==> c(y,z).
c(x,y) ==> c(y,z) = c(x,y) ==> z.
c(x ==> y,x ==> c(y,z)) = (x ==> y) + (c(x,y) ==> z).
m(x,y + z) = m(x,y + m(x + y,z)).
m(x,y + m(x + y,z)) = m(x,y + z).
c(x ==> c(y,z),x ==> y) = x ==> c(y,z).
x ==> c(y,z) = c(x ==> y,x ==> c(y,z)).
c(x ==> y,x ==> c(y,z)) = x ==> c(y,z).
m(x,y) + (x + (z ==> (m(z,u) ==> u))) = x + y.
m(x,y) + ((m(x,z) ==> z) + ((m(x,z) ==> z) ==> x)) = x + y.
m(x,y + (x ==> z)) = m(x,m(z,y) + (x ==> z)).
m(x,m(y,z) + (x ==> y)) = m(x,z + (x ==> y)).
m(x,m(y v x,z)) = m(x,z + (x ==> (y v x))).
m(x,m(y v x,z)) = m(x,z).
m(x,m(y v x,z + u)) = m(x,z + m((y v x) + z,u)).
m(x,y + m((z v x) + y,u)) = m(x,m(z v x,y + u)).
c(x ==> y,x ==> z) = c(x ==> y,x ==> c(y,z)).
c(x ==> y,x ==> c(y,z)) = c(x ==> y,x ==> z).
c(x ==> y,x ==> z) = x ==> c(y,z).
x ==> c(y,z) = (x ==> z) + ((x ==> z) ==> (x ==> y)).
x ==> (y + (y ==> z)) = (x ==> y) + ((x ==> y) ==> (x ==> z)).
(x ==> y) + ((x ==> y) ==> (x ==> z)) = x ==> (y + (y ==> z)).
(x ==> y) + (x ==> ((x ==> y) ==> z)) = x ==> (y + (y ==> z)).
(x ==> y) + (x ==> m(x ==> y,z)) = x ==> (y + (y ==> ((x ==> y) + z))).
x ==> ((x v y) + ((y ==> x) + m(x + z,u))) = m(x + z,u).
(m(x,y) + (m(x,z) ==> z)) + ((m(x,z) ==> z) ==> x) = x + y.
m(x,y + m((z v x) + y,u)) = m(x,y + u).
m(x,m(x,y) + z) = m(x,y + m((u v x) + m(x,y),z)).
m(x,y + m((z v x) + m(x,y),u)) = m(x,m(x,y) + u).
x ==> ((x v y) + ((y ==> x) + m(z + (z ==> x),u))) = m(x + (x ==> z),u).
m(x + (x ==> y),z) = x ==> ((x v u) + ((u ==> x) + m(y + (y ==> x),z))).
(x + (x ==> m(y,x))) + ((m(y,x) ==> x) ==> y) = y + x.
(x + (x ==> (y ==> (x + y)))) + ((m(y,x) ==> x) ==> y) = y + x.
m(x,y + m((z v x) + m(x,y),u)) = m(x,y + u).
(x + 0) + ((m(y,x) ==> x) ==> y) = y + x.
x + ((m(y,x) ==> x) ==> y) = y + x.
x + (((y ==> (y + x)) ==> x) ==> y) = y + x.
(x + (x ==> y)) + (((z ==> (z + (y + (y ==> x)))) ==> (y + (y ==> x))) ==> z) = z + (y + (y ==> x)).
m(x ==> y,z + (y v x)) = (x ==> y) ==> (y + z).
m(x ==> y,z + x) = m(x ==> y,(z + (y ==> x)) + (y v x)).
m(x ==> y,(z + (y ==> x)) + (y v x)) = m(x ==> y,z + x).
(x ==> y) + (x ==> m(x ==> y,z + (y v x))) = x ==> (y + z).
m(x,y + (x ==> z)) = (x ==> z) + (x ==> m(x ==> z,(y + (z ==> x)) + (z v x))).
(x ==> y) + (x ==> m(x ==> y,(z + (y ==> x)) + (y v x))) = m(x,z + (x ==> y)).
(x ==> y) + (x ==> m(x ==> y,z + x)) = m(x,z + (x ==> y)).
(x ==> y) + m(x + (x ==> y),z) = m(x,z + (x ==> y)).
m(x + (x ==> y),z) = x ==> ((x v y) + m(y,z + (y ==> x))).
m(x + (x ==> y),z) = y ==> ((y v x) + m(x,z + (x ==> y))).
x + m(y + (y ==> x),z) = ((x v y) + m(y,z + (y ==> x))) + (((x v y) + m(y,z + (y ==> x))) ==> x).
((x v y) + m(y,z + (y ==> x))) + (((x v y) + m(y,z + (y ==> x))) ==> x) = x + m(y + (y ==> x),z).
x + (y + (y ==> z)) = z + ((z ==> y) + (((x ==> (x + (y + (y ==> z)))) ==> (y + (y ==> z))) ==> x)).
x + ((x ==> y) + (((z ==> (z + (y + (y ==> x)))) ==> (y + (y ==> x))) ==> z)) = z + (y + (y ==> x)).
(x ==> y) + (((x ==> y) ==> y) + (((z ==> (z + y)) ==> (y + (y ==> (x ==> y)))) ==> z)) = z + (y + (y ==> (x ==> y))).
((x v y) + m(y,z + (y ==> x))) + ((x v y) ==> (m(y,z + (y ==> x)) ==> x)) = x + m(y + (y ==> x),z).
(x ==> y) + (((x ==> y) ==> y) + (((z ==> (z + y)) ==> y) ==> z)) = z + (y + (y ==> (x ==> y))).
(x ==> y) + (((x ==> y) ==> y) + (((z ==> (z + y)) ==> y) ==> z)) = z + y.
(((x ==> (x + y)) ==> y) ==> y) + (x + (x ==> ((x ==> (x + y)) ==> y))) = x + y.
(((x ==> (x + y)) ==> y) ==> y) + (x + 0) = x + y.
(((x ==> (x + y)) ==> y) ==> y) + x = x + y.
x + y = x + (((x ==> (x + y)) ==> y) ==> y).
x + (((x ==> (x + y)) ==> y) ==> y) = x + y.
x + (y v (x ==> (x + y))) = x + y.
x + (y v m(x,y)) = x + y.
m(x,y v m(x,y)) = x ==> (x + y).
m(x,y) = m(x,y v m(x,y)).
m(x,y v m(x,y)) = m(x,y).
x v m(y,x) >= m(y,x).
-(x v y >= y) | x v y = y.
x v m(y,x) = m(y,x).
(x v y) ==> m(z,x) = y ==> (x v m(z,x)).
m((x v y) + z,y ==> x) = y ==> (x v m(z,x)).
m((x v y) + z,y ==> x) = y ==> m(z,x).
m((x v y) + m(y,z),y ==> x) = y ==> (z ==> (m(y,z) + x)).
(x ==> y) + m((z v x) + (x ==> y),x ==> z) = x ==> (y + (y ==> ((x ==> y) + z))).
(x ==> (x + y)) + m((z v x) + (x ==> (x + y)),x ==> z) = x ==> ((x + y) + ((x + y) ==> (m(x,y) + z))).
x + m(y + (y ==> x),z) = (x v y) + (m(y,z + (y ==> x)) + ((x v y) ==> (m(y,z + (y ==> x)) ==> x))).
(x v y) + (m(y,z + (y ==> x)) + ((x v y) ==> (m(y,z + (y ==> x)) ==> x))) = x + m(y + (y ==> x),z).
(x ==> (x + y)) + m((z v x) + (x ==> (x + y)),x ==> z) = x ==> ((x + y) + (x ==> (y ==> (m(x,y) + z)))).
(x v y) + (m(y,z + (y ==> x)) + (m(y,z + (y ==> x)) ==> ((x v y) ==> x))) = x + m(y + (y ==> x),z).
(x ==> (x + y)) + m((z v x) + (x ==> (x + y)),x ==> z) = x ==> ((x + y) + m((z v x) + m(x,y),x ==> z)).
x ==> ((x + y) + m((z v x) + m(x,y),x ==> z)) = (x ==> (x + y)) + m((z v x) + (x ==> (x + y)),x ==> z).
(x v y) + (m(y,z + (y ==> x)) + (m(y,z + (y ==> x)) ==> (y ==> x))) = x + m(y + (y ==> x),z).
(x v y) + (m(y,z + (y ==> x)) + (y ==> (m(y,z + (y ==> x)) ==> x))) = x + m(y + (y ==> x),z).
(x v y) + (m(y,z + (y ==> x)) + (y ==> ((z + (y ==> x)) ==> x))) = x + m(y + (y ==> x),z).
(x v y) + (m(y,z + (y ==> x)) + (y ==> (z ==> ((y ==> x) ==> x)))) = x + m(y + (y ==> x),z).
(x v y) + (m(y,z + (y ==> x)) + 0) = x + m(y + (y ==> x),z).
(x v y) + m(y,z + (y ==> x)) = x + m(y + (y ==> x),z).
x ==> (x + (y + m((z v x) + m(x,y),x ==> z))) = (x ==> (x + y)) + m((z v x) + (x ==> (x + y)),x ==> z).
m(x,y + m((z v x) + m(x,y),x ==> z)) = (x ==> (x + y)) + m((z v x) + (x ==> (x + y)),x ==> z).
m(x,y + m((z v x) + m(x,y),x ==> z)) = m(x,y) + m((z v x) + (x ==> (x + y)),x ==> z).
m(x,y + m((z v x) + m(x,y),x ==> z)) = m(x,y) + m((z v x) + m(x,y),x ==> z).
m(x,y) + m((z v x) + m(x,y),x ==> z) = m(x,y + (x ==> z)).
(x v y) + m(y,z + (y ==> x)) = (x v y) + (m(y,z) + (y ==> x)).
(x v y) + (m(y,z) + (y ==> x)) = x + m(y + (y ==> x),z).
x + m(y + (y ==> x),z) = m(y,z) + x.
m(x,m(y + (y ==> x),z)) = x ==> (m(y,z) + x).
m(x,m(y,z)) = m(x,m(y + (y ==> x),z)).
m(x,m(y + (y ==> x),z)) = m(x,m(y,z)).
m(x + (x ==> y),z) >= m(y,m(x,z)).
m(c(x,y),z) >= m(x,m(y,z)).
-(m(c(x,y),z) >= m(x,m(y,z))) | m(c(x,y),z) = m(x,m(y,z)).

end_of_list.
