CARINE is a first-order classical logic automated theorem prover.
CARINE performs an iteratively-deepening depth first search. Its main search strategy is semi-linear resolution (SLR). It employs delayed clause-construction (DCC) to achieve a high inference rate, and attribute sequences to reduce its search space.
