set(print_models_portable).
assign(domain_size, 16).

clauses(theory).

% All of these are consequences of C1 below.

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)).

% Some of the following are redundant.

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

f(f(g(f(y,x)),x),g(f(g(f(y,f(x,z))),x))) = z.  % C1

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

end_of_list.
