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 15466-15469 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 3007-3007 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 3228-3228 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15465-15465 | Text is a subclass of artifact |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15464-15464 | Text is a subclass of content bearing object |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15463-15463 | 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 3001-3001 | The values returned by document are subclasses of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16000-16000 | 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 16058-16058 | 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 15734-15734 | 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 9059-9059 | 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 15485-15485 | Factual text is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15513-15513 | Fictional text is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15866-15866 | 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 15853-15853 | 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 687-687 | Lyrics is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1385-1385 | Motion picture is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15801-15801 | Music text is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16305-16305 | Narrative text is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 698-698 | Paragraph is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10614-10614 | Prescription is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16026-16026 | 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 15687-15687 | Summary is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3022-3022 | Treaty document is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1038-1038 | Treaty document is a subclass of text |
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 18004-18004 | 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 15579-15579 | The number 2 argument of editor is a subclass of text |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15588-15588 | 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 15471-15476 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15478-15483 |
|
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 19802-19806 |
|
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 9693-9700 |
|
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 4043-4051 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12959-12964 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17318-17324 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12794-12800 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15691-15696 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1507-1513 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 672-681 |
|
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 |
![]() |
![]() |