% reflexivity
eq(X,X).

% X*e = X
eq(X*e,W) <- eq(X,W)	if [X>=W].
eq(X,W)	  <- eq(X*e,W)	if [X>=W].

% X*i(X) = e
eq(X*IX,W)   <- eq(e,W),eq(i(X),IX)		if [e>=W,i(X)>=IX].
eq(e,W)	     <- eq(X*IX,W),eq(i(X),IX)		if [e>=W,i(X)>=IX].

% X*(Y*Z) = (X*Y)*Z
eq(X*U,W) <- eq(V*Z,W), eq(Y*Z,U), eq(X*Y,V)	if [X*U>=W,Y*Z>=U,X*Y>=V].
eq(V*Z,W) <- eq(X*U,W), eq(Y*Z,U), eq(X*Y,V)	if [X*U>=W,Y*Z>=U,X*Y>=V].






% all x . e*x = x

% goal [] <- eq(e*X,x), eq(x,X) if [x>=X].

/*
This example requires no splitting of negative equations (original Brand).
proof at depth 4 with 
  588056 steps, 43.2 sec       no constraints
   37293 steps  76.0 sec       with complete constraint solving
   37319 steps, 63.1 sec       with medium constraint solving
   52840 steps, 19.6 sec       with light constraint solving 

 */


% e*e = e
% goal [] <- eq(E*E,e), eq(e,E) if [e>=E].

% all x . i(x)*x = e
% goal [] <- eq(IX*X,e), eq(i(X),IX), eq(x,X) if [i(X)>=IX,x>=X].

/*
no splitting of negative equations
proof at depth 4 with 
   18399350 steps, 1454.3 sec       no constraints
     173293 steps,  375.0 sec       with complete constraint solving
     177703 steps,  255.6 sec       with medium constraint solving
     316375 steps,   95.8 sec       with light constraint solving 
     173138 steps    42.3 sec       light + dual constraints

*/





% goal <- i(X*Y)=i(Y)*i(X)
goal [] <- eq(i(XY),W), eq(IY*IX,W), eq(x*y,XY), eq(i(x),IX), eq(i(y),IY) if [i(XY)>=W,IY*IX>=W,x*y>=XY,i(x)>=IX,i(y)>=IY].






option(horn(off)).