% Status : Unsatisfiable cnf( axiom, axiom, ~h(X) | f(X) = X ). cnf( axiom, axiom, h(X) ). cnf( axiom, axiom, f(X) = a | f(X) = b ). cnf( axiom, axiom, p != q ). cnf( axiom, axiom, r != q ). cnf( axiom, axiom, r != p ).