I | |
| Insuficient_hyps [Res_intf.S] | Raised when a complete resolution derivation cannot be found using the current hypotheses. |
U | |
| UndecidedLit [Internal.Make] | |
| UndecidedLit [Solver_intf.S] | Exception raised by the evaluating functions when a literal has not yet been assigned a value. |
| Unsat [Internal.Make] |