The Refutable item (menu Computations) tests that the current disjunctive normal function is a tautology or not. The algorithm is based on Davies and Putnam method.