SWI-Prolog -- taut/2

Documentation
- Reference manual
  - The SWI-Prolog library
    - library(clpb): CLP(B): Constraint Logic Programming over Boolean Variables
      - CLP(B) predicate index
        
        sat/1
        
        taut/2
        
        labeling/1
        
        sat_count/2
        
        weighted_maximum/3
        
        random_labeling/2
- Packages

Availability::- use_module(library(clpb)).

[semidet]taut(+Expr, -T)

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.