op(450, infix_right, +).   % ring sum
op(400, infix_right, *).   % ring product
op(350, prefix, -).        % ring minus

set(print_models_portable).
assign(iterate_up_to, 19).

% The following fixes the operations [+,-,*] as the ring of
% integers (mod domain_size).

set(integer_ring).

% It is important, for performance reasons, that the ring coefficients
% (H and K below) precede Skolem constants in the denial (A, B, C below).
% This is ordinarily determined by position in the input file, but
% it can be forced by a lex command such as the following.

lex([H,K,A,B,C]).

clauses(theory).

f(x,y) = (H * x) + (K * y).

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

f(A,B) != f(B,A) | f(f(A,B),f(A,f(B,C))) != A.  % denial of BA 2-basis

end_of_list.
