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.