No TPTP formula. May not be expressible in strict first order. | Music.kif 1119-1119 | Music charts is a subclass of list |
No TPTP formula. May not be expressible in strict first order. | Music.kif 1132-1132 | Singles chart is a subclass of music charts |
No TPTP formula. May not be expressible in strict first order. | Music.kif 1144-1144 | Album chart is a subclass of music charts |