No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15257-15257 |
Adjective is a subclass of word |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15261-15261 |
Adverb is a subclass of word |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15248-15248 |
Noun is a subclass of word |
No TPTP formula. May not be expressible in strict first order. |
Media.kif 3092-3092 |
Palindrome is a subclass of word |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15265-15265 |
Particle word is a subclass of word |
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 2504-2504 |
Search term is a subclass of word |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15253-15253 |
Verb is a subclass of word |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 846-846 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 894-894 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 522-522 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 53-53 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 56-56 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2207-2207 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 474-474 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 58-58 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 89-89 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 543-543 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 57-57 |
|