No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13096-13096 |
Advertising is a subclass of disseminating |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 15786-15786 |
Broadcasting is a subclass of disseminating |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13072-13072 |
Demonstrating is a subclass of disseminating |
No TPTP formula. May not be expressible in strict first order. |
MilitaryProcesses.kif 1218-1218 |
Disseminate products is a subclass of disseminating |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1196-1196 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1609-1609 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 874-874 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 407-407 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 410-410 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2558-2558 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 826-826 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 412-412 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 446-446 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 895-895 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 411-411 |
|