introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
the code is still somewhat experimental but any exceptions it throws are catched, and Sledgehammer will still yield a one-line metis proof in case of proof reconstruction failure