No TPTP formula. May not be expressible in strict first order. | Merge.kif 13096-13096 | Advertising is a subclass of disseminating |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 26-26 | Web listing is a subclass of advertising |