This is a chart showing the inference rate of CARINE 0.72 over 4500+ theorems from the TPTP version 2.6.0 library. The system is a Pentium 4 - 2.6GHz machine equipped with 1GB RAM running Windows 2000. The compiler used is gcc 3.2 for Cygwin.

The inference rate is the number of inferences per second. The above figure indicates that CARINE was able to perform up to 1.6 million inferences per second. The reason why CARINE performed less than 200,000 inferences per second on many theorems is due to many factors. Some of those factors are:

• Not enough time. CARINE proved about 900 theorems in a short period of time (mostly less than 1 second) and therefore, there wasn’t enough clauses generated to get an accurate inference-rate measurement.
• The nature of the clauses. Delayed clause-construction does not provide a significant boost to the inference rate if the clauses are short and their terms are shallow.
• The ratio of unification failures to the successful unifications. A higher number of failures implies a lower inference rate.

A Note about Version 0.72

   Version 0.72 does not make use of the full potential of the system. Due to the time limitations (deadlines on the submissions), information gathered during the parsing and processing of the input clauses, as well as data collected and retained by CARINE while carrying out its search are not fully exploited in this version. In its current state, the system performs more of a brute force search than a selective search. Therefore, its efficiency is low by comparison with other theorem provers. Its inference-rate, on the other hand, is relatively high.