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 15384-15387 | |
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 15383-15383 | Text is a subclass of artifact |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15382-15382 | Text is a subclass of content bearing object |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15381-15381 | 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 14618-14618 | 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 14676-14676 | 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 15655-15655 | 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 7869-7869 | 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 15403-15403 | Factual text is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15431-15431 | Fictional text is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14484-14484 | 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 14471-14471 | 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 14419-14419 | Music text is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14923-14923 | 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 9264-9264 | Prescription is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14644-14644 | 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 15608-15608 | 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 16606-16606 | 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 15499-15499 | The number 2 argument of editor is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15509-15509 | 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 15389-15394 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15396-15401 |
|
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 18223-18227 |
|
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 8466-8473 |
|
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 12876-12881 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15920-15926 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12711-12717 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15612-15617 |
|
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 |