The output from current ATP systems varies widely in quantity, quality, and meaning. At the low end of the scale, systems that search for a refutation of a set of clauses may output only an assurance that a refutation exists (the wonderful "yes" output). At the high end of the scale a system may output a natural deduction proof of a problem expressed in FOF. In some cases the output is misleading, e.g., when a CNF based system claims that a FOF input problem is "unsatisfiable" it typically means that the negated CNF of the problem is unsatisfiable.

In order to use ATP systems' results, e.g., as input to other tools, it is necessary that the ATP systems correctly and precisely specify what has been established. To this end a hierarchy of result status values has been established. The hierarchy was based on initial work done to establish communication protocols for systems on the MathWeb Software Bus. The hierarchy is shown below: 

                                  Result
                                     |
           --------------------------+--------------------------
          /               |          |          |               \
   Satisfiability         |       Vacuous       |       Counter satisfiability
     preserving           |       theorem       |            preserving 
         |                |                     |                |
   Satisfiability    Satisfiable             Counter    Counter satisfiability
   partial mapping        |     \          satisfiable      partial mapping  
         |                |      \   &   /      |                |
   Satisfiability      Theorem    Neither    Counter    Counter satisfiability
      mapping             |                  theorem          mapping  
         |                |                     |                |
   Satisfiability    Tautologies          Unsatisfiable Counter satisfiability
     bijection                                               bijection

                                   Error 
                                     |
           --------------------------+--------------------------
          /               |                     |               \
    Input error        Gave up             Resource out       Unknown
                                            /        \
                                        Timeout     Other

Let F be a formula in classical first order logic, of the form Ax => C.

By showing that F is valid, an ATP system shows that C is a theorem (a logical consequence) of Ax, i.e., Ax |= C where |= is the standard first order entailment. If F is not valid, there are several other possible relationships between Ax and C, as shown in the hierarchy and enumerated below Associated with each possible status are the possible outputs from the ATP system. The status values and possible outputs are ordered as follows:

  1. Every interpretation is a model of Ax and a model of C

  2. Every model of Ax (and there are some) is a model of C, but not case "Tautologies"

  3. Some models of Ax (and there are some) are models of C

  4. There is a bijection between the models of Ax (and there are some) and models of C

  5. There is a mapping from the models of Ax (and there are some) to models of C

  6. There is a partial mapping from the models of Ax (and there are some) to models of C

  7. If there exists a model of Ax then there exists a model of C

  8. There are no models of Ax

  9. Some models of Ax (and there are some) are models of C, and some are models of ~C.

  10. If there exists a model of Ax then there exists a model of ~C

  11. There is a partial mapping from the models of Ax (and there are some) to models of ~C

  12. There is a mapping from the models of Ax (and there are some) to models of ~C

  13. There is a bijection between the models of Ax (and there are some) and models of ~C

  14. Some models of Ax (and there are some) are models of ~C

  15. Every model of Ax (and there are some) is a model of ~C, but not "Unsatisfiable"

  16. Every interpretation is a model of Ax and a model of ~C