Specialist Problem Classes
- CNF - Clause Normal Form
- FOF - First-Order Form
- TF0 - Typed First-order form Monomorphic
- TF1 - Typed First-order form Polymorphic
- TFX - Typed First-order form eXtended
- TH0 - Typed Higher-order form Monomorphic
- TH1 - Typed Higher-order form Polymorphic
- THM - THeoreM
- CAX - Contradictory AXioms
- CSA - CounterSAtisfiable
- UNS - UNSatisfiable
- SAT - SATisfiable
- OPN - OPeN
- UNK - UNKown
- PRP - PRoPositional
- EPR - Effectively PRopositional
- RFO - Real First-Order
- NEQ - No EQuality
- EQU - With EQUality
- SEQ - Some EQuality
- PEQ - Pure EQuality
- NAR - No ARithmetic
- ARI - ARIthmetic
- HRN - HoRN
- NHN - Non-HorN
Current SPCs
- 225 in use (127 empty)
- Largest FOF_THM_RFO_SEQ - 5349 problems