CNF                                     // former LogicSimplify
LogicSimplify                           // (expression, level=1..3
CanProve                                // <==> LogicSimplify(expr, 3)
LogicRemoveTautologies                  // not clear is this will stay, but it is eq. to LogicSimplify(expr, 2)
Subsumes
//~
//|
//&
=>
}