No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 1134-1134 |
Le domaine de ShipRegisterFn est une instance de ShipRegister |
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 1198-1198 |
FlagOfConvenienceRegister est une sous-classe de ShipRegister |
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 1168-1168 |
InternalShipRegister est une sous-classe de ShipRegister |
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 1121-1121 |
NationalShipRegister est une sous-classe de ShipRegister |
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 1182-1182 |
OffshoreShipRegister est une sous-classe de ShipRegister |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 52713-52713 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 52712-52712 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 52711-52711 |
|