C | |
| CLAUSIFIER_RESOURCE_OUT [Const] |
clausfier ran out of resources.
|
| CLOSE [Context_unifier] |
raised if Close is triggered by the given closing context unifier.
|
E | |
| EMPTY_CLAUSE [Preprocessing_unit] |
this clause is simplified to the empty clause,
so the clause set is unsatisfiable.
|
| EMPTY_CLAUSE [Preprocessing_resolution] |
these clauses simplify to the empty clause,
so the clause set is unsatisfiable.
|
| EMPTY_CLAUSE [Preprocessing_equality] |
this clause is simplified to the empty clause,
so the clause set is unsatisfiable.
|
F | |
| FOF [Const] | FOF theorem is raised if the input is in fof format.
|
I | |
| ITERATOR_EMPTY [Term_indexing] |
raised by
Term_indexing.iterator.next if no element is left.
|
N | |
| NO_SOLUTION [Const] |
the derivation is aborted because of a limitation of the implementation.
|
O | |
| OVERFLOW [Stack] |
thrown if a stack exceeds the system given maximum size.
|
| OVERFLOW [Heap] |
thrown if a heap exceeds its maximum size.
|
| OVERFLOW [Counter] |
raised if the counter is exhausted.
|
P | |
| PARSE_ERROR [Const] |
error in the input file.
|
S | |
| SATISFIABLE [Selection] |
no further applicable candidate available -
satisfiability of the problem detected
|
| SET_FAIL [Subst] |
see
Subst.set
|
U | |
| UNIFICATION_FAIL [Unification] |
raised by all functions when the unification fails.
|
| UNSATISFIABLE [Context_unifier] |
refutation found
|