trichotomizingOn |
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2051-2054 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3612-3615 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3609-3609 | The number 1 argument of trichotomizing on is an instance of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3610-3610 | The number 2 argument of trichotomizing on is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3608-3608 | trichotomizing on is an instance of asymmetric relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3607-3607 | trichotomizing on is an instance of binary predicate |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 195-195 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 196-196 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 59153-59153 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 196-196 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 59152-59152 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 59151-59151 |
antecedent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3601-3605 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3617-3629 |
|
consequent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3595-3599 |
|
appearance as argument number 0 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1787-1787 | greater than is trichotomizing on real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1816-1816 | greater than or equal to is trichotomizing on real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1775-1775 | less than is trichotomizing on real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1799-1799 | less than or equal to is trichotomizing on real number |
![]() |
![]() |