AC Associativity and Commutativity   Efficiency of a Theorem Prover Total number of inference rules attempted before a proof is found.   Inference Rule An n+1-ary relation on clauses written as      are called premises and  is the conclusion.   Speed of a Theorem Prover Number of inferences generated per unit of time (usually, per second).   TPTP Thousands of Problems for Theorem Provers.