Problem Characteristics

Language property
Logical Form
  • Typed Higher-order Form
  • Typed First-order Form
    • Polymorphic or Monomorphic
  • Typed First-order Form
    • Polymorphic or Monomorphic
    • With or without Arithmetic
  • First Order Form
  • Clause Normal Form
    • Really first-order or Effectively propositional
Logical property
SZS Status
  • Theorem
  • CounterSatisfiable
  • Unsatisfiable
  • Satisfiable
Syntactic property
Equality
  • No equality
  • Some equality
  • Pure equality
CNF Literals
  • Horn
  • Non-Horn
CNF Pure Equality
  • Non-Unit
  • Unit