starts |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2701-2703 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8040-8042 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1424-1426 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8037-8037 | 域 啟動, 1 and TimeInterval |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8038-8038 | 域 啟動, 2 and TimeInterval |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8035-8035 | 例 啟動 and IrreflexiveRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8033-8033 | 例 啟動 and TemporalRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8036-8036 | 例 啟動 and TotalValuedRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8034-8034 | 例 啟動 and TransitiveRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8032-8032 | 子關係 啟動 and 時間部分 |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 419-419 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 425-425 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 244-244 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 269-269 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2038-2038 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 196-196 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 249-249 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 544-544 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 306-306 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 265-265 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 265-265 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 461-461 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55074-55074 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 420-420 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55073-55073 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55072-55072 |
antecedent |
consequent |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2881-2897 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2854-2870 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8054-8062 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3754-3764 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 487-499 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 21474-21489 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16380-16389 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16294-16299 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 11305-11328 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16395-16404 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9409-9414 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9435-9445 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8795-8801 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19095-19102 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1025-1034 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8879-8886 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8456-8463 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8535-8537 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17300-17306 | |
No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 285-299 |
|
No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 305-319 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8901-8908 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19109-19116 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 424-429 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17070-17076 | |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
statement |
No TPTP formula. May not be expressible in strict first order. | Media.kif 1970-1978 | TimeInterval 例 TimeInterval and TimeInterval 飾面 TimeInterval and 何時 JesusOfNazareth 啟動 TimeInterval and 何時 TwelveApostles entity
|