C cannot be made into a theorem of Ax by extending Ax ~F is valid CTH F is invalid Some models of Ax (and there are some) are models of ~C. ~F is satisfiable CSA C is not a theorem of Ax F is not valid ~C is a theorem of Ax Every model of Ax (and there are some) is a model of ~C. TAC C is a tautology Satisfiable SAT F is satisfiable ~F is not valid C is not a theorem of Ax The problem is satisfiable modula its theory. THM C is a theorem of Ax Every model of Ax (and there are some) is a model of C. F is valid F is valid Every interpretation is a model of C. F is valid Ax and C have the same models (and there are some). C is a theorem of Ax EQV UNC Every interpretation is a model of ~C. ~C is a tautology System ran past user imposed memory limit. ystem gave up before the time limit. System exited before the time limit for unknown reason. ~F is satisfiable C is not a theorem of Ax F is satisfiable Some models of Ax (and there are some) are models of C, and some are models of ~C. ~F is not valid NOC F is not valid Every interpretation is a model of Ax xor a model of C F is not valid Ax and ~C have the same models (and there are some).. ~C is a theorem of Ax CEQ System ran past user imposed CPU time limit. System exited due to an error in its input. F is valid C is a tautology TAU ~F is unsatisfiable UNS Every interpretation is a model of Ax and a model of ~C. F is unsatisfiable ~F is valid The problem is unsatifiable modulo its theory. ~C is a tautology