clpb:taut/2

taut(+Expr, -T) is semidet: Tautology check. Succeeds with T = 0 if the Boolean expression Expr cannot be satisfied, and with T = 1 if Expr is always true with respect to the current constraints. Fails otherwise.