Class
|
|
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1806-1810 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2138-2146 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 421-427 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10629-10629 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10628-10628 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10631-10631 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10630-10630 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10627-10627 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10626-10626 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 9942-9942 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10633-10633 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10625-10625 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2136-2136 | Classe e' uma sub-classe de Conjunto ou Classe |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1762-1762 | O contra-dominio de ExtensionFn e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5584-5584 | O contra-dominio de KappaFn e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1516-1516 | O contra-dominio de WeekBeforeMenstruationFn e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 886-886 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 974-974 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 562-562 | |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 92-92 | |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 95-95 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2247-2247 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 514-514 | |
No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 97-97 | |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 129-129 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 583-583 | |
No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 96-96 |
appearance as argument number 3 |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1490-1490 | O argumento numero 1 de TTFxFn e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3575-3575 | O argumento numero 2 de closedOn e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 395-395 | O argumento numero 1 de disjoint e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 396-396 | O argumento numero 2 de disjoint e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 566-566 | O argumento numero 1 de disjointDecomposition e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 567-567 | O argumento numero 2 de disjointDecomposition e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 210-210 | O argumento numero 3 de domain e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 232-232 | O argumento numero 3 de domainSubclass e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3706-3706 | O argumento numero 2 de equivalenceRelationOn e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 548-548 | O argumento numero 1 de exhaustiveDecomposition e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 549-549 | O argumento numero 2 de exhaustiveDecomposition e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 91-91 | O argumento numero 2 de immediateInstance e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 153-153 | O argumento numero 1 de immediateSubclass e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 154-154 | O argumento numero 2 de immediateSubclass e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 82-82 | O argumento numero 2 de instance e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31007-31007 | O argumento numero 1 de memberMeasure e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22650-22650 | O argumento numero 2 de memberType e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22664-22664 | O argumento numero 2 de memberTypeCount e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3643-3643 | O argumento numero 2 de partialOrderingOn e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 582-582 | O argumento numero 1 de partition e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 583-583 | O argumento numero 2 de partition e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 307-307 | O argumento numero 2 de range e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3604-3604 | O argumento numero 2 de reflexiveOn e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 131-131 | O argumento numero 1 de subclass e' uma instancia de Classe |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 132-132 | O argumento numero 2 de subclass e' uma instancia de Classe |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31018-31023 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31025-31030 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31186-31191 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31215-31220 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31119-31124 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31164-31169 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31325-31332 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31053-31058 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31355-31360 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31237-31242 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31280-31285 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31098-31103 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31072-31077 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 828-830 |
consequent |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 145-160 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 574-578 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 558-562 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2034-2041 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2043-2052 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 137-141 |