appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1811-1815 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2137-2144 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 428-433 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2135-2135 | Set is a subclass of set or class |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2116-2116 | Set or class is exhaustively partitioned into set and class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4262-4262 | The range of property is an instance of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5523-5523 | Finite set is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5513-5513 | Non null set is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5502-5502 | Null set is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | engineering.kif 204-204 | Set of equations is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 887-887 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 976-976 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 563-563 | |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 93-93 | |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 94-94 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2248-2248 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 515-515 | |
No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 98-98 | |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 130-130 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 584-584 | |
No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 97-97 |
appearance as argument number 3 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5401-5401 | The number 2 argument of element is an instance of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5379-5379 | The number 1 argument of subset is an instance of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5380-5380 | The number 2 argument of subset is an instance of set |
antecedent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31232-31239 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31095-31100 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31028-31033 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31073-31078 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31007-31012 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30976-30981 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30927-30932 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31124-31129 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31264-31269 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31146-31151 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31189-31194 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30995-31000 |
|
consequent |
![]() |
![]() |
![]() |