cnf(equation_1, axiom, (g(f(X, b)) = c)).
cnf(equation_2, axiom, (f(g(X), Y) = f(X, g(Y)))).