| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3397-3398 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14617-14620 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 887-887 | |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 40-40 | Virus is exhaustively partitioned into DNA virus and RNA virus |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 42-42 | Virus is exhaustively partitioned into unenveloped virus and enveloped virus |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 41-41 | Virus is exhaustively partitioned into virus double stranded and virus single stranded |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14616-14616 | Virus is a subclass of microorganism |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 104-104 | DNA virus is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 145-145 | Enveloped virus is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 130-130 | RNA virus is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 2017-2017 | Tick borne encephalitis virus is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 141-141 | Unenveloped virus is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 231-231 | Viral agent is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 150-150 | Virus double stranded is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 154-154 | Virus single stranded is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 975-975 | Virus single stranded is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 1157-1157 | Virus single stranded is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 652-652 | Virus single stranded is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 183-183 | Virus single stranded is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | terms-it.txt 186-186 | Virus single stranded is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2336-2336 | Virus single stranded is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 604-604 | Virus single stranded is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 220-220 | Virus single stranded is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 479-479 | Virus single stranded is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 673-673 | Virus single stranded is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 187-187 | Virus single stranded is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1119-1119 | A viral genome is typically a part of a virus |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1144-1144 | A virion enzyme is typically a part of a virus |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1165-1165 | The number 1 argument of viral part is an instance of virus |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 35-35 | The number 1 argument of genetic substrate of virus is an instance of virus |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 25-25 | The number 2 argument of invading virus is an instance of virus |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 1085-1085 | The number 2 argument of vaccine is a subclass of virus |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14622-14626 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14628-14636 |
|
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1153-1158 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3753-3765 |
|
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1146-1151 |
|
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1112-1117 |
|
|
|
|