set(print_models_portable).

clauses(theory).

f(x,y) != f(x,z) | y = z.
f(y,x) != f(z,x) | y = z.

f(0,x) = x.
f(x,0) = x.
f(g(x),x) = 0.
f(x,g(x)) = 0.
g(g(x)) = x.
g(0) = 0.
g(f(x,y)) = f(g(y),g(x)).
f(x,f(g(x),y)) = y.
f(g(x),f(x,y)) = y.

f(f(x,x),y) = f(x,f(x,y)).
f(f(x,y),x) = f(x,f(y,x)).
f(f(y,x),x) = f(y,f(x,x)).

f(f(A,B),C) != f(A,f(B,C)).

% f(f(g(f(x,x)),y),g(f(g(f(x,f(x,z))),y))) = z.  % model of size 10
% g(f(x,f(f(f(g(x),g(f(y,f(z,y)))),y),z))) = y.  % model of size 12

end_of_list.