assign(iterate_up_to, 100).

formulas(theory).
f(f(g(f(y,z)),y),g(f(g(f(f(x,z),z)),x))) = z.  % candidate 3
f(f(A,B),C) != f(A,f(B,C)).                    % denial of associativity
end_of_list.