% Status : Unsatisfiable

cnf( axiom, axiom, h(a,X) ).

cnf( axiom, axiom, ~h(X,f(X)) ).