| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1947-1947 | 汽车 是 自供电公路车辆 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1948-1948 | 汽车 是 乘用车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 836-836 | 汽车 是 物理系统 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1962-1962 | 出租车 是 汽车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4513-4513 | CommodoreAutomobile 是 汽车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4859-4859 | MiniCooper 是 汽车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4871-4871 | HoldenToranaAutomobile 是 汽车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4917-4917 | FordAutomobile 是 汽车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4974-4974 | ChevroletAutomobile 是 汽车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 5126-5126 | Corvette 是 汽车 的 subclass |
|
|