| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13463-13463 | Main section trans new guinea language is a subclass of trans new guinea language |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13470-13470 | Central and western main section trans new guinea language is a subclass of main section trans new guinea language |
|
|