comment |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 4051-4053 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18362-18364 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18366-18366 | 注释 的 1 数量 是 实体 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18367-18367 | 注释 的 2 数量 是 符号串 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18368-18368 | 注释 的 3 数量 是 符号串 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18361-18361 | 注释 是 三元谓语 的 instance |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 3042-3042 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 3041-3041 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 3040-3040 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 4054-4054 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 1855-1855 |
appearance as argument number 0 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14295-14301 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13789-13791 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 13700-13701 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 13726-13728 | |
No TPTP formula. May not be expressible in strict first order. | Music.kif 971-974 | |
No TPTP formula. May not be expressible in strict first order. | Government.kif 197-197 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22240-22246 | |
No TPTP formula. May not be expressible in strict first order. | Music.kif 825-826 | |
No TPTP formula. May not be expressible in strict first order. | Music.kif 141-144 | |
No TPTP formula. May not be expressible in strict first order. | Music.kif 1076-1078 | |
No TPTP formula. May not be expressible in strict first order. | Music.kif 1099-1103 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14328-14331 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14355-14357 |