| No TPTP formula. May not be expressible in strict first order. | engineering.kif 1116-1116 | RemoteControl est une sous-classe de Controller |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 413-413 | TVRemoteControl est une sous-classe de RemoteControl |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3738-3738 | RemoteIgnitionControl est une sous-classe de RemoteControl |
|
|