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 13254-13255 |
|
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 13253-13253 |
Naming is a subclass of declaring |