inList |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1973-1975 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3109-3111 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 605-607 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3106-3106 | 域 在列表中, 1 and Entity |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3107-3107 | 域 在列表中, 2 and List |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3104-3104 | 例 在列表中 and BinaryPredicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3105-3105 | 例 在列表中 and PartialValuedRelation |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 131-131 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 132-132 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 87-87 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 147-147 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1914-1914 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 39-39 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 103-103 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 157-157 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 186-186 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 106-106 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 86-86 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 298-298 | |
No TPTP formula. May not be expressible in strict first order. | Music.kif 332-332 | 子關係 albumTrack and 在列表中 |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30193-30193 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 132-132 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30192-30192 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30191-30191 | |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 47-47 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 299-299 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3286-3290 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 2005-2017 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1998-2003 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 503-507 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 497-501 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7582-7587 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1975-1980 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1966-1973 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2491-2498 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2483-2489 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1929-1933 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1716-1720 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1784-1788 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1750-1754 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1819-1823 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2677-2682 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1769-1775 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1860-1864 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16921-16929 |
|
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 694-710 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 771-781 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3113-3116 |
|
consequent |
No TPTP formula. May not be expressible in strict first order. | People.kif 357-390 | 例 年 and 年 年EAR 等於 GeopoliticalArea 和 年 的 male 出生估計壽命 and RealNumber List Integer, SymbolicString, entity, entity and entity 例 List and List 例 列表長度 List and Integer ListITEM
|
No TPTP formula. May not be expressible in strict first order. | People.kif 403-436 | 例 年 and 年 Integer 等於 GeopoliticalArea 和 年 的 female 出生預期壽命 and RealNumber List Integer, SymbolicString, entity, entity and entity 例 List and List 例 列表長度 List and Integer ListITEM
|
No TPTP formula. May not be expressible in strict first order. | People.kif 310-342 | 例 年 and 年 Integer 等於 GeopoliticalArea 和 年 的出生預期 life and RealNumber List Integer, SymbolicString, entity, entity and entity 例 List and List 例 列表長度 List and Integer ListITEM
|
No TPTP formula. May not be expressible in strict first order. | People.kif 272-293 | RealNumber 是 List 的 average List PositiveInteger 等於 列表長度 List and 列表長度 List 等於 清單順序 List and 1 and 清單順序 List and 1 PositiveInteger
|
No TPTP formula. May not be expressible in strict first order. | Music.kif 280-287 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7596-7611 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4861-4872 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4874-4888 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4946-4956 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4958-4972 | |
No TPTP formula. May not be expressible in strict first order. | Music.kif 936-946 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 2005-2017 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 801-812 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1532-1547 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5369-5374 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 464-468 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2950-2955 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2957-2966 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 574-578 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4854-4859 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4939-4944 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1685-1692 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 509-517 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2940-2948 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 558-562 | |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |