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 2146-2153 | |
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 2144-2144 | 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 2125-2125 | Set or class is exhaustively partitioned into set and class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4288-4288 | The range of property is an instance of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5547-5547 | Finite set is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5537-5537 | Non null set is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5526-5526 | 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 | Set of equations is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 976-976 | Set of equations is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 563-563 | Set of equations is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 93-93 | Set of equations is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 96-96 | Set of equations is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2248-2248 | Set of equations is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 515-515 | Set of equations is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 98-98 | Set of equations is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 130-130 | Set of equations is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 389-389 | Set of equations is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 584-584 | Set of equations is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 97-97 | Set of equations is a subclass of set |
appearance as argument number 3 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5425-5425 | The number 2 argument of element is an instance of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5405-5405 | The number 1 argument of subset is an instance of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5406-5406 | The number 2 argument of subset is an instance of set |
antecedent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12181-12197 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12149-12161 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 33020-33027 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32883-32888 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32807-32812 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32861-32866 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32786-32791 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32755-32760 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32706-32711 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32912-32917 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 33052-33057 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32934-32939 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32977-32982 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32774-32779 |
|
consequent |
![]() |
![]() |
![]() |