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

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

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

set(integer_ring).

clauses(theory).

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

% denial of group

f(f(X,Y),Z) != f(X,f(Y,Z)) | f(f(g(X),X),Y) != Y | f(g(X),X) != f(g(Y),Y).

end_of_list.