graphPart |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2349-2350 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5891-5893 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1024-1026 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5888-5888 | 图形部分 的 1 数量 是 图元素 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5889-5889 | 图形部分 的 2 数量 是 图 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5885-5885 | 图形部分 是 非对称关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5884-5884 | 图形部分 是 二元谓语 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5887-5887 | 图形部分 是 非自反关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5886-5886 | 图形部分 是 总值关系 的 instance |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 749-749 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 751-751 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 452-452 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 119-119 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2160-2160 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 404-404 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 465-465 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 966-966 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 159-159 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 474-474 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 517-517 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 246-246 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 750-750 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 26459-26459 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 26458-26458 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5993-6006 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5979-5991 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6165-6176 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5790-5799 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6062-6068 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5675-5683 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5630-5650 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5726-5737 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5739-5750 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5813-5817 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5905-5909 |
consequent |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2846-2856 | |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2858-2868 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5905-5909 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6157-6163 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5652-5666 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5777-5788 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5806-5811 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5706-5716 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5698-5704 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5690-5696 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5825-5830 |