% problem-set/analysis/limits/prob2.ver1.clauses
% created : 07/21/86
% revised : 07/20/88

% description :
%
% Problem 0ntributed through private 0rrespondance with W.W. Bledsoe.

% representation :
%
% declare_predicates(2,[EQUAL,LT]).
% declare_functions(2,[sum,f1]).
% declare_functions(1,[h,fp31,minus,f,fp32,g,fp33,abs]).
% declare_0nstants([0,a,l1,l2,b]).
% declare_variables([x,y,z,xa]).
%
% No interpretations are available at this time.

% axiom 1 

EQUAL(sum(x,0),x).
EQUAL(sum(0,x),x).
-LT(x,x).

% LT transitivity

-LT(x,y)  | -LT(y,z)  |  LT(x,z).

% axiom 2 

-LT(0,x) | -LT(0,y) |  LT(0,f1(x,y)).
-LT(0,x) | -LT(0,y) |  LT(f1(x,y),x).
-LT(0,x) | -LT(0,y) |  LT(f1(x,y),y).

% axiom 3 

-LT(x,h(xa))  | -LT(y,h(xa))  |  LT(sum(x,y),xa).

% axiom 7 

-LT(0,xa)    |  LT(0,h(xa)).


% denial of the theorem 

-LT(0,x)  |  LT(0,fp31(x)).
-LT(0,x)  | -LT(abs(sum(y,minus(a))),fp31(x)) 
	   |  LT(abs(sum(f(y),minus(l1))),x).
-LT(0,x)  |  LT(0,fp32(x)).
-LT(0,x)  | -LT(abs(sum(y,minus(a))),fp32(x)) 
	   |  LT(abs(sum(g(y),minus(l2))),x).
LT(0,b).
-LT(0,x)  |  LT(abs(sum(fp33(x),minus(a))),x).
-LT(0,x)  
        | -LT(abs(sum(sum(f(fp33(x)),g(fp33(x))),minus(sum(l1,l2)))),b).