assign(iterate_up_to, 100). formulas(theory). f(f(g(f(x,x)),y),g(f(g(f(x,f(x,z))),y))) = z # label(candidate_10). % inverse loop axioms f(g(x),x) = 1. f(x,g(x)) = 1. f(g(x),f(x,y)) = y. f(f(y,x),g(x)) = y. % inverse loop lemmmas (these help Mace4 a lot for this example) f(1,x) = x. f(x,1) = x. g(g(x)) = x. g(1) = 1. end_of_list. formulas(goals). f(f(x,y),z) = f(x,f(y,z)) # label(associativity). end_of_list.