No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 3686-3688 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16352-16355 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16350-16350 |
The number 1 argument of ancestor is an instance of organism |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16351-16351 |
The number 2 argument of ancestor is an instance of organism |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16349-16349 |
ancestor is an instance of binary predicate |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16347-16347 |
ancestor is an instance of irreflexive relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16348-16348 |
ancestor is an instance of total valued relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16346-16346 |
ancestor is an instance of transitive relation |