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 2144-2151 | |
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 2142-2142 | 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 2123-2123 | Set or class is exhaustively partitioned into set and class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4271-4271 | The range of property is an instance of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5528-5528 | Finite set is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5518-5518 | Non null set is a subclass of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5507-5507 | 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 5406-5406 | The number 2 argument of element is an instance of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5386-5386 | The number 1 argument of subset is an instance of set |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5387-5387 | 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 12121-12137 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12089-12101 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32439-32446 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32302-32307 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32226-32231 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32280-32285 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32205-32210 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32174-32179 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32125-32130 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32331-32336 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32471-32476 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32353-32358 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32396-32401 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32193-32198 |
|
consequent |
![]() |
![]() |
![]() |