%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 -> 5

goal f(g(b),b,a)=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(g(b),b,a)=a ->                                                 [axiom]
   7 : f(B,C,f(D,B,E))=f(D,B,f(B,C,E))                   [chaining of 2 from 1]
  29 : f(B,C,D)=f(C,D,f(B,C,D))                          [chaining of 2 from 7]
  41 : f(B,g(B),C)=f(C,B,g(B))                          [chaining of 3 from 29]
  45 : f(B,g(B),C)=C                                   [reduction of 41 by [3]]
  47 : B=g(g(B))                                        [chaining of 3 from 45]
  56 : f(g(B),B,C)=C                                   [chaining of 47 from 45]
  57 + false                                         [reduction of 4 by [56,0]]


Length = 11, Depth = 8



Total time: 4540 milliseconds

of which: 

 860		milliseconds of inference computation
 230		milliseconds of clause simplification
 670		milliseconds of rule simplification
 290		milliseconds of constraint solving
 460		milliseconds of clause preprocessing
 1380		milliseconds of rewriting
 600		milliseconds for the rest


Number of inferences: 48
Number of nonredundant clauses: 29


*/