No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17652-17652 |
无光的 是 发光的 的相反 |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 3943-3944 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17653-17654 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 10319-10319 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 12107-12107 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17651-17651 |
无光的 是 视觉属性 的 instance |