| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1947-1947 | Automobile est une sous-classe de SelfPoweredRoadVehicle |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1948-1948 | Automobile est une sous-classe de PassengerVehicle |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 836-836 | Automobile est une sous-classe de PhysicalSystem |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1962-1962 | Taxicab est une sous-classe de Automobile |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4513-4513 | CommodoreAutomobile est une sous-classe de Automobile |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4859-4859 | MiniCooper est une sous-classe de Automobile |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4871-4871 | HoldenToranaAutomobile est une sous-classe de Automobile |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4917-4917 | FordAutomobile est une sous-classe de Automobile |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4974-4974 | ChevroletAutomobile est une sous-classe de Automobile |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 5126-5126 | Corvette est une sous-classe de Automobile |
|
|