%1
f(U,V,f(X,Y,Z)) = f(f(U,V,X),Y,f(U,V,Z)).
%2
f(Y,X,X) = X.
%3
f(X,Y,g(Y)) = X.
%4
%f(X,X,Y) = X.
%5
%f(g(Y),Y,X) = X.

precedence([f,g,a,b,c,d,e]).

% 1,2,3 -> 4

goal f(a,a,b)=a -> [].

/*
Proof:
======

   1 : f(B,C,f(D,E,F))=f(f(B,C,D),E,f(B,C,F))                           [axiom]
   2 : f(B,C,C)=C                                                       [axiom]
   3 : f(B,C,g(C))=B                                                    [axiom]
   4 + f(a,a,b)=a ->                                                    [axiom]
   7 : f(B,C,f(D,B,E))=f(D,B,f(B,C,E))                   [chaining of 2 from 1]
  31 : f(B,C,C)=f(C,D,f(B,C,g(D)))                       [chaining of 3 from 7]
  39 : B=f(B,C,f(D,B,g(C)))                            [reduction of 31 by [2]]
  62 : f(B,B,C)=B                                       [chaining of 3 from 39]
  69 + false                                         [reduction of 4 by [62,0]]


Length = 9, Depth = 6



Total time: 5960 milliseconds

of which: 

 1150		milliseconds of inference computation
 220		milliseconds of clause simplification
 870		milliseconds of rule simplification
 360		milliseconds of constraint solving
 470		milliseconds of clause preprocessing
 2000		milliseconds of rewriting
 870		milliseconds for the rest


Number of inferences: 59
Number of nonredundant clauses: 33

*/