| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1944-1944 | 子類 LCAC and 兩棲車輛 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1945-1945 | 子類 LCAC and 軍車 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1946-1946 | 子類 LCAC and 乘用車 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1947-1947 | 子類 LCAC and 動力車輛 |
|
|