| No TPTP formula. May not be expressible in strict first order. | Food.kif 3377-3383 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14566-14566 | 子類 Fish and ColdBloodedVertebrate |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2535-2535 | 子類 Cod and Fish |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2536-2536 | 子類 鮭魚 and Fish |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3403-3403 | 子類 Skate and Fish |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3518-3518 | 子類 Tuna and Fish |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4926-4926 | 子類 觀賞魚 and Fish |
|
|