![]() |
![]() ![]() ![]()
|
![]() |
|
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 2150-2157 | |
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 2148-2148 | Ensemble est une sous-classe de ensemble ou classe |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2129-2129 | Ensemble ou classe est compl�tement d�compos� en ensemble + classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4275-4275 | Le domaine de PropertyFn est une instance de ensemble |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5537-5537 | Ensemble fini est une sous-classe de ensemble |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5527-5527 | NonNullSet est une sous-classe de ensemble |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5516-5516 | NullSet est une sous-classe de ensemble |
No TPTP formula. May not be expressible in strict first order. | engineering.kif 205-205 | SetOfEquations est une sous-classe de ensemble |
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 96-96 | |
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 5415-5415 | Le nombre 2 argument de element est une instance de ensemble |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5393-5393 | Le nombre 1 argument de sous-ensemble est une instance de ensemble |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5394-5394 | Le nombre 2 argument de sous-ensemble est une instance de ensemble |
antecedent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12068-12084 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12036-12048 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31312-31319 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31175-31180 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31100-31105 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31153-31158 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31079-31084 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31048-31053 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30999-31004 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31204-31209 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31344-31349 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31226-31231 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31269-31274 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31067-31072 |
|
consequent |
![]() |
![]() |
![]() |