% Ternary Boolean Algebra.  Independence of axiom 2.

assign(domain_size, 3).
set(print_models_portable).  % 3-ary operations look better this way

% set(verbose).

clauses(theory).

f(f(v,w,x),y,f(v,w,z)) = f(v,w,f(x,y,z)).
% f(y,x,x) = x.  % We're showing that this axiom is independent.
f(x,x,y) = x.
f(g(y),y,x) = x.
f(x,y,g(y)) = x.

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

end_of_list.