No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 3281-3281 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13276-13277 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 2979-2979 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 3165-3165 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 3166-3166 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13275-13275 |
命名 是 声明 的 subclass |