![]() |
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 2127-2134 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2125-2125 | 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 2106-2106 | Set or class is exhaustively partitioned into set and class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4252-4252 | The range of property is an instance of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5504-5504 | Finite set is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5494-5494 | Non null set is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5483-5483 | 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 |
appearance as argument number 3 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5382-5382 | The number 2 argument of element is an instance of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5360-5360 | The number 1 argument of subset is an instance of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5361-5361 | 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 31225-31232 |
|
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 31117-31122 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31257-31262 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31139-31144 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31182-31187 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30995-31000 |
|
consequent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29946-29976 |
|
![]() |
![]() |