![]() |
![]() ![]()
|
![]() |
|
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17145-17145 | False is the opposite of true |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3797-3797 | False is the opposite of true |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17146-17146 | False is the opposite of true |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17144-17144 | False is an instance of truth value |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 23203-23203 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 23202-23202 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 23201-23201 |
consequent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2317-2321 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 549-556 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7366-7376 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 4201-4216 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 915-922 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 586-593 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20919-20925 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 13166-13171 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17689-17695 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17701-17707 |
|
![]() |
![]() |