| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 2035-2035 | 子類 用戶帳號 and ContentBearingObject |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4542-4542 | 子類 用戶帳號 and Account |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2001-2001 | 子類 蘋果ID and 用戶帳號 |
|
|