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 16374-16377 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16372-16372 |
The number 1 argument of ancestor is an instance of organism |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16373-16373 |
The number 2 argument of ancestor is an instance of organism |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16371-16371 |
ancestor is an instance of binary predicate |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16369-16369 |
ancestor is an instance of irreflexive relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16370-16370 |
ancestor is an instance of total valued relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16368-16368 |
ancestor is an instance of transitive relation |