Prover9 New Constants

   assign(new_constants, 1).   % introduce up to 1 new constant

If an equation alhpa = beta is derived, in which both sides have variables, and they share no variables, a new constant can be introduced. For example,

   9492 f(x,f(x,x)) = f(y,f(y,y)). [ … ]
   9670 f(x,f(x,x)) = c0.  [new_symbol 9492]

Notes

set(auto) -> assign(new_constants, 1)
useful for nonstandard axiomatizations, e.g., single axioms
if you allow more than one constant to be introduced, beware
a more general rule introduces functions of the shared variables (not implemented)