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:
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.
Sorry downloads are currently not available.