assign(iterate_up_to, 100).

formulas(theory).

  f(f(g(f(y,z)),y),g(f(g(f(f(x,z),z)),x))) = z # label(candidate_3).

end_of_list.

formulas(goals).

  f(f(x,y),z) = f(x,f(y,z)) # label(associativity).

end_of_list.