fixed to refactoring; uf proof sketches now go through
printing bv proof atoms
refactored SatProof to work with BVMinisat and Minisat
doesn't compile