- Specify the problem - the axioms and the conjecture
- Write the problem's axioms and conjecture in the domain language
- Write the problem in a logic
- Write the problem in a machine readable syntax (using a TPTP language).
- Check the syntax of the problem
(using SystemB4TPTP)
- Yes - move on to check the semantics of the problem
- No - return to creating the machine readable file

- Check the semantics (types) of the problem
(using SystemB4TPTP)
- Yes - move on to check the consistency of the axioms
- No - return to creating the machine readable file

- Check the consistency of the axioms
(using SystemOnTPTP)
- Establish that the axioms are satisfiable
- Yes - move on to establish logical consequence
- No - examine model/saturation, return to specify the problem
- Unknown - establish that the axioms are unsatisfiable

- Establish that the axioms are unsatisfiable
- Yes - examine the refutation (using IDV), return to specify the problem
- No - move on to establish logical consequence
- Unknown - move on to establish logical consequence (and worry)

- Establish that the axioms are satisfiable
- Establish logical consequence
(using SystemOnTPTP)
- Prove the theorem
- Yes - move on to process the proof
- No - return to specify the problem
- Unknown - prove it's not a theorem

- Prove it's not a theorem
- Yes - return to specify the problem
- No - move on to processing the proof
- Unknown - return to specify the problem

- Prove the theorem
- Process the proof
- Are the axioms are known to be SAT?
- Yes - verify the proof
- No - check if the conjecture is used in proof
- If the axioms used in the proof are a subset of all the axioms, could check for their consistency.

- Check if the conjecture is used in proof
- Yes - assume the axioms are OK, verify the proof
- No - return to specify the problem
- Unknown - ask if the ATP system is trusted

- Verify the proof
(using GDV)
- Yes - happiness
- No - return to establish logical consequence with a different ATP system
- Unknown - ask if the ATP system is trusted

- Is the ATP system trusted?
- Yes - happiness
- No - return to specify the problem
- Unknown - confusion, return to specify the problem

- Are the axioms are known to be SAT?
- Examples for the ATP Process
- A Theorem with Nice Axioms
- A Non-Theorem with Nice Axioms
- A Theorem with Nasty Axioms
- A Challenge Theorem