| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15939-15939 | Device is a subclass of artifact |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 3072-3072 | Canal lock gate is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 3074-3074 | Traffic light is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 2015-2015 | Barricade is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1317-1317 | Lever is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1722-1722 | Transducer is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1882-1882 | Aerator is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1920-1920 | Brush or comb is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1934-1934 | Match device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1997-1997 | Writing device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2009-2009 | Smoking device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2198-2198 | Toilet is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2248-2248 | Tableware is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2260-2260 | Compass is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2271-2271 | Major appliance is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2282-2282 | Cooling device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2305-2305 | Heating device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2374-2374 | Recreation or exercise device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2385-2385 | Toy is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2438-2438 | Walking cane is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2450-2450 | Washing device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2462-2462 | Material handling equipment is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2493-2493 | Optical device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2519-2519 | Filter is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2533-2533 | File device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2542-2542 | Electric device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2565-2565 | Power source is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2659-2659 | Security device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2734-2734 | Animal controller is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2749-2749 | Self powered device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2762-2762 | Animal powered device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2850-2850 | Baton is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3014-3014 | Light fixture is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3252-3252 | Painting device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3384-3384 | Vehicle controller is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3535-3535 | Axle is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4007-4007 | Lid is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4193-4193 | Screwdriver is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4208-4208 | Hammer is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4277-4277 | Washer is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4314-4314 | Holder is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 5588-5588 | Cleaning device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13313-13313 | Camera is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15034-15034 | Chimney is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15256-15256 | Door is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15354-15354 | Fireplace is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17841-17841 | Explosive device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 21994-21994 | Cutting device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24055-24055 | Contraceptive device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25197-25197 | Ironing board is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25363-25363 | Drying device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25419-25419 | Smoke detector is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25434-25434 | Sprinkler is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25478-25478 | Fire extinguisher is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25618-25618 | Data storage device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25816-25816 | Knock light is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25905-25905 | Electrical outlet is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25962-25962 | Outlet adapter is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26048-26048 | Earphone is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26245-26245 | Audio recorder is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26437-26437 | Telephone handset is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26452-26452 | Fire alarm is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26703-26703 | Tripod is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29377-29377 | Vehicle door is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30785-30785 | Karabiner is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15957-15957 | Musical instrument is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15965-15965 | Transportation device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16000-16000 | Measuring device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16012-16012 | Attaching device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16023-16023 | Weapon is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16041-16041 | Machine is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16056-16056 | Engineering component is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 661-661 | Medical device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1360-1360 | Internet access point is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | engineering.kif 753-753 | Pendulum is a subclass of device |
| 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. | engineering.kif 880-880 | Transfer switch is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5160-5160 | Heat sealer is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3758-3758 | Clamshell is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3775-3775 | Keyboard is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 112-112 | Keyboard is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 475-475 | Speaker is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 59-59 | Telephone cradle is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 538-538 | Brake is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 582-582 | Wearing friction surface is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 660-660 | Brake rotor is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 666-666 | Brake drum is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 672-672 | Brake caliper is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 677-677 | Brake pedal is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 770-770 | Damper is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1105-1105 | Fuel atomizer is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1309-1309 | Engine choke is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1404-1404 | Ball bearing is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1634-1634 | Cam is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1695-1695 | Combustion chamber is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1808-1808 | Clutch is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 1967-1967 | Engine connecting rod is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2267-2267 | Distributor is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2310-2310 | Drivebelt is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2534-2534 | Gas pedal is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2613-2613 | Muffler is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2619-2619 | Exhaust manifold is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2832-2832 | Gasket is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 2904-2904 | Governor is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3006-3006 | Grease fitting is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3030-3030 | Grease gun is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3209-3209 | Jumper cable is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3350-3350 | Safety device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3836-3836 | Rocker arm is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4115-4115 | Rod is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4145-4145 | Wrench is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4201-4201 | Tap is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4215-4215 | Die is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4268-4268 | Reel is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4316-4316 | Wheel chock is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4438-4438 | Snow chain is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4480-4480 | Unpowered device is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4664-4664 | Cargo rack is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4780-4780 | Tire is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4806-4806 | Rim is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4870-4870 | Tire changer is a subclass of device |
|
|