small fixes, allowing E and SPASS to prove problems transformed to CNF
fixed bugs in Cnf (unsound skolemization/removal of forall)