appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3550-3552 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15362-15365 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 3008-3008 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 3229-3229 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15361-15361 | Text is a subclass of artifact |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15360-15360 | Text is a subclass of content bearing object |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15359-15359 | Text is a subclass of linguistic expression |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3013-3013 | The values returned by document are subclasses of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14619-14619 | The values returned by series volume are subclasses of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14677-14677 | Article is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2287-2287 | Calendar is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15633-15633 | Certificate is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 1025-1025 | Chairman publication is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7870-7870 | Christian gospel is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 993-993 | Doctrine is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15381-15381 | Factual text is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15409-15409 | Fictional text is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14485-14485 | Form text is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 921-921 | Joint publication is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14472-14472 | Label is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 3012-3012 | LTU is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 694-694 | Lyrics is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1392-1392 | Motion picture is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14420-14420 | Music text is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14924-14924 | Narrative text is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 705-705 | Paragraph is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9265-9265 | Prescription is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14645-14645 | Series is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4222-4222 | Spam is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15586-15586 | Summary is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3034-3034 | Treaty document is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1038-1038 | |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
appearance as argument number 3 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16607-16607 | The number 1 argument of registered item is an instance of text |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15477-15477 | The number 2 argument of editor is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15487-15487 | The number 2 argument of publishes is a subclass of text |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Biography.kif 730-740 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 1894-1898 |
|
No TPTP formula. May not be expressible in strict first order. | Biography.kif 742-751 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 938-943 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15367-15372 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15374-15379 |
|
consequent |
No TPTP formula. May not be expressible in strict first order. | Communications.kif 202-214 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18224-18228 |
|
No TPTP formula. May not be expressible in strict first order. | Biography.kif 717-726 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8467-8474 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 931-936 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3574-3582 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12854-12859 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15921-15927 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12689-12695 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15590-15595 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1514-1520 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 679-688 |
|
statement |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3309-3315 | IBookstore has the purpose there exists ?D such that ?D is an instance of downloading and iBookstore is an instrument for ?D and ?T is an instance of text and the object transferred in ?D is ?T |