| System | Domains | SPCs |
|---|---|---|
| E | BOO GEO (CNF) GRP LAT RNG ROB | Unit equality, Some equality Horn Some equality non-Horn Unit equality, Mixed equality and Horn status Unit equality Unit equality, Some equality Horn Unit equality, Some equality Horn |
| Gandalf | CAT FLD GEO (CNF) SET (CNF) | Some equality Horn and non-Horn No equality non-Horn Some equality non-Horn Some equality non-Horn |
| Vampire | BOO FLD GEO (CNF) GEO (FOF) LDA NUM RNG SET (CNF) SET (FOF) | Unit equality, Some equality Horn No equality non-Horn Some equality non-Horn First order Some equality non-Horn Some equality non-Horn Unit equality, Some equality Horn Some equality non-Horn First order |