No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13582-13582 |
Hearing is a subclass of perception |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13521-13521 |
Seeing is a subclass of perception |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13556-13556 |
Smelling is a subclass of perception |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13631-13631 |
Tactile perception is a subclass of perception |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13569-13569 |
Tasting is a subclass of perception |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1216-1216 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1653-1653 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 894-894 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 427-427 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 430-430 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2578-2578 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 846-846 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 466-466 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 915-915 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 431-431 |
|