CARINE performs an iteratively-deepening depth-first search (IDDFS) using a resolution refinement called semi-linear resolution (SLR). The delayed clause-construction strategy is implemented to allow CARINE to achieve a high inference-rate. Attribute sequences are used to reduce the search space and thereby, improve the efficiency of CARINE.

   Benefits of IDDFS

   At every iteration, clauses inferred from previous iterations are repeatedly inferred again. This implies that redundancies occur. However, the algorithm does ensure a systematic search process which uses storage space equivalent to a depth-first search (DFS). Its advantage over DFS is that the search is bounded by the iteration depth. This bounded search explores all paths up to the iteration depth leading to the discovery of the optimal proof length. This is a characteristic of a breadth-first search. Therefore, the benefits of IDDFS are low memory requirements, bounded search, and (theoretically) optimal proof lengths.

   Attribute Sequences

   An attribute sequence is a sequence of length k (k>0) that is a projection of one or more search paths.