No TPTP formula. May not be expressible in strict first order. |
Merge.kif 12945-12945 |
Hunting is a subclass of pursuing |
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 2342-2342 |
Search attempt is a subclass of pursuing |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1190-1190 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1597-1597 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 868-868 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 401-401 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 404-404 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2552-2552 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 820-820 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 406-406 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 440-440 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 889-889 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 405-405 |
|