tokens: Then if a solver for the proposed problem deems S to not be optimal , there must clearly be a valuation which yields a 1 according to our crafted function and thus satisfies the whole formula - in turn providing a valuation that does not satisfy the original input to TAUTOLOGY .
ner_tags: O O O O O O O O O B-Variable O O O O O O O O O O O O O O B-Value O O O O O O O O O O O O O O O O O O O O O O O O O O O