fix wrong answer from -newcnf on with two or more Boolean lets

[shalashaska117]

Closes #893.

NewCNF stores formulas in generalised clauses with any leading negation stripped and the sign of the generalised literal flipped instead (pushLiteral). Occurrences::replaceBy broke that invariant: it wrote the formula in unchanged, and enqueue compensated by dropping the negation from the queue key and flipping the occurrence signs. The slot was left holding ~A with a sign that every later lookup reads as the sign of A.

processLet produces that state whenever ennf has pushed a negation into a let body. With one $let the slot is only ever rewritten in place, so nothing shows. With two, clausifying the first copies the second's slot into new generalised clauses through pushLiteral, which strips the negation again and flips the sign a second time. The second definition gets the wrong polarity, its clauses come out as tautologies, and tautologies are deleted, so the whole problem clausifies to nothing and saturation reports a model. On master (9f47172, Release):

$ vampire --input_syntax smtlib2 -newcnf on checks/theory/let-bool-twice.smt2
% SZS status Satisfiable for let-bool-twice
$ vampire -newcnf on checks/theory/let-bool-twice.p
% SZS status CounterSatisfiable for let-bool-twice
$ vampire -newcnf on -ile off checks/theory/let-bool-twice.p
% SZS status Theorem for let-bool-twice

-ile off was already correct: the naming path never hands replaceBy a negated formula there.

The stale ~A also breaks the occurrence count that pop maintains by looking the slot formula up in _occurrences. A Debug build dies on the same input without printing anything; under gdb:

#5  Debug::Assertion::violatedEquality<unsigned int, int> (val1Str="_size", val2Str="0", val1=1, val2=0)
#6  Shell::NewCNF::Occurrences::isNonEmpty at Shell/NewCNF.hpp:327
#7  Shell::NewCNF::process(JunctionFormula*, Occurrences&) at Shell/NewCNF.cpp:449

The fix handles the negation where the formula is written into the clause: replaceBy drops it and flips the sign of every occurrence, the same way it already normalises negative shared literals, and enqueue leaves the signs alone. Its invert() helper lost its only caller and is removed. process(QuantifiedFormula*) uses the same replaceBy/enqueue pair on the quantifier body, so it is covered by the same change.

With the fix, Debug build with assertions enabled:

PASS: twice.smt2 default
PASS: twice.smt2 newcnf
PASS: twice.smt2 newcnf ile off
PASS: twice.p default
PASS: twice.p newcnf
PASS: twice.p ile off
PASS: twice.p newcnf ile off
PASS: let-bool.p newcnf
PASS: let-bool.p newcnf ile off
PASS: let-bool-pred.p newcnf
PASS: let-bool-pred.p newcnf ile off
PASS: let-bool-simultaneous.p newcnf
PASS: let-function.p newcnf
PASS: let-tuple.p newcnf
PASS: let-tuple-bool.p newcnf

Also checked in default, -newcnf on and -newcnf on -ile off: three sibling lets and nested lets (Unsatisfiable), a satisfiable two-let problem (still Satisfiable), and two $lets under a universal quantifier (Theorem). checks/sanity passes with a Release+Z3 build and ctest is 97/97 with the Debug build. The new checks cover the TPTP and SMT-LIB shape of the problem in the same configurations as the other let-bool files.