| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14591-14591 | Chinese language is a subclass of sino tibetan language |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14592-14592 | Chinese language is a subclass of spoken human language |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14593-14593 | Chinese language is a subclass of written human language |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14594-14594 | Chinese language is a subclass of natural language |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 319-319 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 320-320 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55725-55725 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1371-1373 |
|
|