Restore lift of unfailing knuth-bendix completion to full theorem proving

[wisnesky]

Because solving equality of open terms using CQL's built-in unfailing completion spawns a new completion process for each equality to be solved, CQL's lifted unfailing Knuth bendix completion theorem prover is exponentially slower than the ground version and was disabled when its performance became apparent. But having it built-in would still be nice, so as not to have to use E or maedmax or vampire for the full problem on small examples.