| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2112-2112 | Unary constant function quantity is a subclass of function quantity |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2120-2120 | Time dependent quantity is a subclass of unary constant function quantity |
|
|