| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15939-15939 | 子類 Device and Artifact |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 3072-3072 | 子類 運河閘門 and Device |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 3074-3074 | 子類 紅綠燈 and Device |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 2015-2015 | 子類 壅 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1317-1317 | 子類 Lever and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1722-1722 | 子類 傳感器 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1882-1882 | 子類 增氧機 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1920-1920 | 子類 刷子或梳子 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1934-1934 | 子類 匹配設備 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1997-1997 | 子類 寫作設備 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2009-2009 | 子類 吸煙裝置 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2198-2198 | 子類 廁所 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2248-2248 | 子類 餐具 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2260-2260 | 子類 羅盤 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2271-2271 | 子類 主要電器 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2282-2282 | 子類 冷卻裝置 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2305-2305 | 子類 加熱裝置 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2374-2374 | 子類 娛樂或運動器材 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2385-2385 | 子類 Toy and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2438-2438 | 子類 拐杖 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2450-2450 | 子類 洗滌設備 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2462-2462 | 子類 物料搬運設備 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2493-2493 | 子類 光學設備 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2519-2519 | 子類 過濾 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2533-2533 | 子類 文件設備 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2542-2542 | 子類 電器 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2565-2565 | 子類 能量源 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2659-2659 | 子類 安全裝置 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2734-2734 | 子類 動物控制器 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2749-2749 | 子類 自供電設備 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2762-2762 | 子類 動物動力裝置 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2850-2850 | 子類 指揮棒 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3014-3014 | 子類 燈具 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3252-3252 | 子類 繪畫裝置 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3384-3384 | 子類 車輛控制器 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3535-3535 | 子類 軸 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4007-4007 | 子類 蓋子 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4193-4193 | 子類 Screwdriver and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4208-4208 | 子類 錘子 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4277-4277 | 子類 墊圈 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4314-4314 | 子類 持有人 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 5588-5588 | 子類 清潔設備 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13313-13313 | 子類 相機 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15034-15034 | 子類 煙囪 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15256-15256 | 子類 門 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15354-15354 | 子類 壁爐 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17841-17841 | 子類 爆炸裝置 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 21994-21994 | 子類 切割裝置 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24055-24055 | 子類 避孕器具 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25197-25197 | 子類 IroningBoard and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25363-25363 | 子類 DryingDevice and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25419-25419 | 子類 SmokeDetector and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25434-25434 | 子類 Sprinkler and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25478-25478 | 子類 滅火器 and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25618-25618 | 子類 DataStorageDevice and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25816-25816 | 子類 KnockLight and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25905-25905 | 子類 ElectricalOutlet and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25962-25962 | 子類 OutletAdapter and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26048-26048 | 子類 Earphone and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26245-26245 | 子類 AudioRecorder and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26437-26437 | 子類 TelephoneHandset and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26452-26452 | 子類 FireAlarm and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26703-26703 | 子類 Tripod and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29377-29377 | 子類 VehicleDoor and Device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30785-30785 | 子類 Carabiner and Device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15957-15957 | 子類 MusicalInstrument and Device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15965-15965 | 子類 TransportationDevice and Device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16000-16000 | 子類 測量工具 and Device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16012-16012 | 子類 附著裝置 and Device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16023-16023 | 子類 Weapon and Device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16041-16041 | 子類 Machine and Device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16056-16056 | 子類 EngineeringComponent and Device |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 661-661 | 子類 MedicalDevice and Device |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1360-1360 | 子類 InternetAccessPoint and Device |
| No TPTP formula. May not be expressible in strict first order. | engineering.kif 753-753 | 子類 擺 and Device |
| No TPTP formula. May not be expressible in strict first order. | engineering.kif 776-776 | 子類 彈簧 and Device |
| No TPTP formula. May not be expressible in strict first order. | engineering.kif 880-880 | 子類 轉換開關 and Device |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5160-5160 | 子類 熱封機 and Device |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3758-3758 | 子類 LaptopScreenPart and Device |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3775-3775 | 子類 LaptopKeyboardPart and Device |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 112-112 | 子類 Keyboard and Device |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 475-475 | 子類 SpeakerDevice and Device |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 59-59 | 子類 TelephoneCradle and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 538-538 | 子類 Brake and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 582-582 | 子類 WearingFrictionSurface and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 660-660 | 子類 BrakeRotor and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 666-666 | 子類 BrakeDrum and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 672-672 | 子類 BrakeCaliper and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 677-677 | 子類 BrakePedal and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 770-770 | 子類 Damper and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1105-1105 | 子類 FuelAtomizer and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1309-1309 | 子類 EngineChoke and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1404-1404 | 子類 BallBearing and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1634-1634 | 子類 Cam and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1695-1695 | 子類 CombustionChamber and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1808-1808 | 子類 Clutch and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1967-1967 | 子類 EngineConnectingRod and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2267-2267 | 子類 Distributor and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2310-2310 | 子類 Drivebelt and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2534-2534 | 子類 GasPedal and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2613-2613 | 子類 AutomobileMuffler and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2619-2619 | 子類 ExhaustManifold and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2832-2832 | 子類 Gasket and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2904-2904 | 子類 SpeedGovernor and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3006-3006 | 子類 GreaseFitting and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3030-3030 | 子類 GreaseGun and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3209-3209 | 子類 JumperCable and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3350-3350 | 子類 SafetyDevice and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3836-3836 | 子類 RockerArm and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4115-4115 | 子類 Rod and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4145-4145 | 子類 Wrench and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4201-4201 | 子類 MechanicalTap and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4215-4215 | 子類 MechanicalDie and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4268-4268 | 子類 捲軸 and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4316-4316 | 子類 WheelChock and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4438-4438 | 子類 TireChain and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4480-4480 | 子類 UnpoweredDevice and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4664-4664 | 子類 VehicleRoofRack and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4780-4780 | 子類 Tire and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4806-4806 | 子類 WheelRim and Device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4870-4870 | 子類 TireChanger and Device |
|
|