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 17142-17142 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17141-17141 | 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 17145-17145 | False is the opposite of true |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 59337-59337 | False is the opposite of true |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 59336-59336 | False is the opposite of true |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 59335-59335 | False is the opposite of true |
consequent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2306-2310 |
|
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 19485-19490 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14326-14331 |
|
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 15635-15637 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2835-2837 |
|
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 |
|
![]() |
![]() |