| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1718-1718 | 电脑协定 是 程序 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1748-1748 | 活性同步 是 电脑协定 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2815-2815 | USB 是 电脑协定 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4025-4025 | DHCPProtocol 是 电脑协定 的 subclass |
|
|