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

adapt code to reflect new signature of "neg_clausify"

rename options and keep track of conjecture shape (to facilitate proof reconstruction)