No TPTP formula. May not be expressible in strict first order. | Merge.kif 3005-3010 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3339-3339 | Predicate is a subclass of relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3340-3340 | Predicate is a subclass of inheritable relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3478-3478 | Binary predicate is a subclass of predicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3489-3489 | Ternary predicate is a subclass of predicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3500-3500 | Quaternary predicate is a subclass of predicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3511-3511 | Quintary predicate is a subclass of predicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3550-3550 | Logical operator is a subclass of predicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18470-18470 | ClosedWorldPredicate is a subclass of predicate |