assign(iterate_up_to, 100).
set(iterate_primes).

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

set(integer_ring).

% For efficiency of the search when doing integer_ring constraints,
% it is important to have a good symbol ordering.  The ring coefficients
% (A,B,C in this case) should be first.  One could use a "lex" command
% to achieve this.  An easier way is to rely on the default ordering,
% which places upper case constants before lower case constants.
% Skolem constants are lower case, so the following gives a good ordering.

formulas(theory).

% f and g in terms of the ring operations (with coefficients A,B,C)

g(x) = A * x.
f(x,y) = (B * x) + (C * y).

f(f(y,g(y)),f(g(f(x,f(g(f(z,z)),z))),x)) = z.  % candidate 23

end_of_list.

formulas(goals).

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

end_of_list.