| No TPTP formula. May not be expressible in strict first order. | engineering.kif 776-776 | Spring is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 723-723 | Wire spring is a subclass of spring |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 887-887 | Leaf spring is a subclass of spring |
|
|