appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3796-3796 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17157-17157 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17156-17156 | True is an instance of truth value |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17160-17160 | False is the opposite of true |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 59308-59308 | False is the opposite of true |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 59307-59307 | False is the opposite of true |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 59306-59306 | False is the opposite of true |
consequent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2307-2311 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 540-547 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19468-19473 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14308-14313 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 577-584 |
|
No TPTP formula. May not be expressible in strict first order. | Law.kif 65-78 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15617-15619 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2850-2852 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17704-17710 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17716-17722 |
|
![]() |
![]() |