| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7461-7461 |
Le domaine de DescendantsFn est une instance de family groupe familiale |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16308-16308 |
Le domaine de ImmediateFamilyFn est une instance de family groupe familiale |
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 23177-23177 |
NuclearFamily est une sous-classe de family groupe familiale |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1065-1065 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1341-1341 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 743-743 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 274-274 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 277-277 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2427-2427 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 695-695 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 279-279 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 313-313 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 764-764 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 278-278 |
|
