No TPTP formula. May not be expressible in strict first order. |
Government.kif 2869-2869 |
Big seven is a conventional long name of "Big Seven" |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 10994-10994 |
Big seven is a conventional long name of "Big Seven" |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 10993-10993 |
Big seven is a conventional long name of "Big Seven" |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 10992-10992 |
Big seven is a conventional long name of "Big Seven" |