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.