% problem-set/analysis/limits/prob1.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(sum(abs(sum(f(fp33(x)),minus(l1))), abs(sum(g(fp33(x)),minus(l2)))),b). % axiom 4 -LT(sum(abs(x),abs(y)),xa) | LT(abs(sum(x,y)),xa).