No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13604-13604 |
Hearing is a subclass of perception |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13543-13543 |
Seeing is a subclass of perception |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13578-13578 |
Smelling is a subclass of perception |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13653-13653 |
Tactile perception is a subclass of perception |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13591-13591 |
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 |
|