/*

Shows, for the particular case of 2 binary function symbols,
one unary smaller function symbol and one minimal constant, 
that entailment of atomic lpo constraints
from conjunctions of inequalities is
decidable in quadratic time (=< 2 covering terms in each clause).

*/


predicates([>,>=]).
precedence([f,>=,>]).

%:-option([special_relations(off)]).


% non-strict inequality
X>=X.
X>Y -> X>=Y.
0>X -> [].	% for testing inconsistency of atomic constraints

% embedded terms are smaller
X>=Y -> f(U,X)>Y.  
X>=Y -> f(X,U)>Y.
X>=Y -> g(U,X)>Y.
X>=Y -> g(X,U)>Y.
X>=Y -> h(X)>Y.


% lexicographic comparison of subterms
X>Y, f(X,U)>Z -> f(X,U)>f(Y,Z).
U>Z	      -> f(X,U)>f(X,Z).
X>Y, g(X,U)>Z -> g(X,U)>g(Y,Z).
U>Z	      -> g(X,U)>g(X,Z).
X>Y	      -> h(X)>h(Y).


% precedence-based comparisons
% f>g in precedence:
f(X,Y)>U, f(X,Y)>V -> f(X,Y)>g(U,V).  

% f>h in precedence
f(X,Y)>Z -> f(X,Y)>h(Z).

% g>h in precedence
g(X,Y)>Z -> g(X,Y)>h(Z).

% 0 is minimal
f(X,Y)>0.
g(X,Y)>0.
h(X)>0.


f(h(0),0)>f(0,0) -> [].

%:-option([crw_depth(1),memo_constraints(on)]).
:-sarp([1-7,10-15]). % the usual + clausal rewriting  
:-sama([]).
%:-saci([2]).        % not needed
:-sams([3,19]).      % messages about redundancy proofs by clausal rewrtng.
:-ordering(sto).     % subterm ordering



/* 20000731
Saturation terminated.

Persisting Clauses:

    1(1) : B>=B
    2(1) : B>C -> B>=C
    3(1) : 0>B -> 
    4(1) : B>=C -> f(D,B)>C
    5(1) : B>=C -> f(B,D)>C
    6(1) : B>=C -> g(D,B)>C
    7(1) : B>=C -> g(B,D)>C
    8(1) : B>=C -> h(B)>C
    9(1) : B>C,f(B,D)>E -> f(B,D)>f(C,E)
   10(1) : B>C -> f(D,B)>f(D,C)
   11(1) : B>C,g(B,D)>E -> g(B,D)>g(C,E)
   12(1) : B>C -> g(D,B)>g(D,C)
   13(1) : B>C -> h(B)>h(C)
   14(1) : f(B,C)>D,f(B,C)>E -> f(B,C)>g(D,E)
   15(1) : f(B,C)>D -> f(B,C)>h(D)
   16(1) : g(B,C)>D -> g(B,C)>h(D)
   17(1) : f(B,C)>0
   18(1) : g(B,C)>0
   19(1) : h(B)>0
   20(2) : B>C -> h(B)>C
   21(2) : B>C -> f(D,B)>C
   22(2) : B>C -> f(B,D)>C
   23(2) : B>C -> g(D,B)>C
   24(2) : B>C -> g(B,D)>C



Total time: 6280 milliseconds

Number of forward inferences: 5
Number of tableau inferences: 0
Number of kept clauses: 24

*/