| No TPTP formula. May not be expressible in strict first order. | Food.kif 645-647 | |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 628-628 | 咖啡 是 饮料 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 739-739 | Espresso 是 咖啡 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 764-764 | Lungo 是 咖啡 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1264-1264 | Cappuccino 是 咖啡 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1303-1303 | Americano 是 咖啡 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1334-1334 | FlatWhite 是 咖啡 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1387-1387 | Latte 是 咖啡 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1417-1417 | LongBlack 是 咖啡 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1452-1452 | VietnameseCoffee 是 咖啡 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1453-1453 | TurkishCoffee 是 咖啡 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1454-1454 | Manilo 是 咖啡 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1455-1455 | Instant 是 咖啡 的 subclass |
|
|