larger |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2664-2665 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7755-7756 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1384-1385 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7752-7752 | The number 1 argument of larger is an instance of object |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7753-7753 | The number 2 argument of larger is an instance of object |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7747-7747 | larger is an instance of binary predicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7750-7750 | larger is an instance of irreflexive relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7748-7748 | larger is an instance of spatial relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7751-7751 | larger is an instance of total valued relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7749-7749 | larger is an instance of transitive relation |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 623-623 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 626-626 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 376-376 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 160-160 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2110-2110 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 328-328 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 385-385 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 818-818 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 199-199 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 398-398 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 418-418 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 320-320 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7775-7775 | smaller is an inverse of larger |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 624-624 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 33366-33366 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 33365-33365 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 321-321 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7758-7766 | An object is larger than another object if and only if for all a real number, another real number and an unit of measure
|
consequent |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 5330-5335 |
|
No TPTP formula. May not be expressible in strict first order. | Geography.kif 5270-5274 |
|
No TPTP formula. May not be expressible in strict first order. | Geography.kif 5145-5149 |
|
No TPTP formula. May not be expressible in strict first order. | Geography.kif 4523-4528 |
|
No TPTP formula. May not be expressible in strict first order. | Geography.kif 5305-5310 |
|