No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13118-13118 |
Advertising is a subclass of disseminating |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 15785-15785 |
Broadcasting is a subclass of disseminating |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13094-13094 |
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 |
|