/*

This system can be viewed as modelling rational unification
The variables in input equations are constants which may be equated
to any other term in the course of unification.

With the precedence-modified subterm order
we may use an auxiliary projection function
p to formalize injectivity of function symbols
even though input queries do not contain p.
We have inp(f(X))> s(f(X)) in the ordering.

Therefore we get complexity n log n.

*/


:-option(special_relations(off)).  

% equality
eq(X,X).
eq(X,Y) -> eq(Y,X).
eq(X,Y), eq(Y,Z) -> eq(X,Z).

eq(X,Y), eq(U,V), eq(f(X,U),Z) -> eq(f(Y,V),Z).
eq(X,Y), eq(p1(X),Z) -> eq(p1(Y),Z).
eq(X,Y), eq(p2(X),Z) -> eq(p2(Y),Z).

% injectivity

eq(inp(f(X,Y)),tt) -> eq(p1(f(X,Y)),X).
eq(inp(f(X,Y)),tt) -> eq(p2(f(X,Y)),Y).

eq(inp(f(X,Y)),tt) -> eq(inp(X),tt).
eq(inp(f(X,Y)),tt) -> eq(inp(Y),tt).

eq(p1(a),b).
eq(p2(a),b).

% clash

eq(a,b) -> [].

% example for clash situation that will be refuted
% eq(inp(f(f(a,a),a)),tt).
% eq(f(f(a,a),a),a).


:-option([crw_depth(1),memo_constraints(on)]).
:-sama([]).             % We want saturation by ordered resolution w/o sel.
:-sarp([1-7,10-15]).    % the usual + clausal rewriting  
:-sams([3,19]).      % messages about redundancy proofs by clausal rewrtng.

:-ordering(sto).  % subterm ordering

precedence([f,inp,p1,p2,a,b,tt,eq]).

/*
As usual, ``negative substitutions'' X=t can be applied
(whenever X appears only in places where substitution is allowed)
without affecting locality of an equational
theory. In this sense, all added
clauses are redundant, that is, subsumed by input
clauses.

Saturation terminated.

Persisting Clauses:

    1(1) : eq(B,B)
    2(1) : eq(B,C) -> eq(C,B)
    3(1) : eq(B,C),eq(C,D) -> eq(B,D)
    4(1) : eq(B,C),eq(D,E),eq(f(B,D),F) -> eq(f(C,E),F)
    5(1) : eq(B,C),eq(p1(B),D) -> eq(p1(C),D)
    6(1) : eq(B,C),eq(p2(B),D) -> eq(p2(C),D)
    7(1) : eq(inp(f(B,C)),tt) -> eq(p1(f(B,C)),B)
    8(1) : eq(inp(f(B,C)),tt) -> eq(p2(f(B,C)),C)
    9(1) : eq(inp(f(B,C)),tt) -> eq(inp(B),tt)
   10(1) : eq(inp(f(B,C)),tt) -> eq(inp(C),tt)
   13(1) : eq(a,b) -> 
   18(2) : eq(p1(a),B) -> eq(b,B)
   22(2) : eq(p2(a),B) -> eq(b,B)
   47(3) : eq(b,B),eq(a,C) -> eq(p1(C),B)
   63(3) : eq(b,B),eq(a,C) -> eq(p2(C),B)
   70(4) : eq(b,B),eq(p1(C),D),eq(a,C) -> eq(B,D)
   83(4) : eq(b,B),eq(p2(C),D),eq(a,C) -> eq(B,D)



Total time: 53830 milliseconds

Number of forward inferences: 126
Number of tableau inferences: 0
Number of kept clauses: 21

*/