% Find up to 1000 models up through size 25 assign(iterate_up_to, 25). assign(max_models, 1000). % 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. % Change operator name to @, because * is the ring product. formulas(theory). x @ y = (A * x) + (B * y). (x @ e) @ x = x. x @ (x @ y) = y. (x @ y) @ (z @ u) = (x @ z) @ (y @ u). ((x @ x) @ x) @ x = e. end_of_list.