No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 2521-2523 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6824-6830 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 1221-1224 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6822-6822 |
Steradian is an instance of systeme international unit |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6821-6821 |
Steradian is an instance of unit of angular measure |