No TPTP formula. May not be expressible in strict first order. |
People.kif 238-264 |
A year is an instance of the year an integer and the deaths per thousand live births of a geopolitical area and the year is equal to a real number if and only if another integer is equal to the number of instances in the class described by a symbolic string and the other integer and 1000 is equal to another real number and a third integer is equal to the number of instances in the class described by another symbolic string and the third integer and the other real number is equal to the real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1942-1946 |
A real number is an instance of negative real number if and only if the real number is less than 0 and the real number is an instance of real number |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1860-1864 |
A real number is less than or equal to another real number if and only if the real number is equal to the other real number or the real number is less than the other real number |
No TPTP formula. May not be expressible in strict first order. |
Medicine.kif 172-187 |
|
No TPTP formula. May not be expressible in strict first order. |
Medicine.kif 155-170 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 19646-19655 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 19661-19671 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 19677-19687 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 19693-19703 |
|
No TPTP formula. May not be expressible in strict first order. |
Dining.kif 1148-1156 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2617-2622 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14401-14410 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14329-14338 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14340-14351 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14291-14301 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4948-4962 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 5032-5037 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 5337-5346 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 5321-5330 |
|
No TPTP formula. May not be expressible in strict first order. |
Dining.kif 772-795 |
|
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 1520-1529 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 1928-1942 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 876-882 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 866-874 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 4693-4703 |
|
|
Display limited to 25 items. Show next 25 |
|
Display limited to 25 items. Show next 25 |