Test to show whether or not the expression before and after eliminate_implications() is equivalent. If they are equivalent, then the formula Equivalent(expr, eliminate_implications(expr)) is valid i.e. Not(formula) is unsatisfiable. Once valid is implemented by PR #2830, it can be called directly. This method proves the soundness of the function better than individual test cases.