| 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 14549-14552 | |
| 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 14548-14548 | Virus is a subclass of microorganism |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 100-100 | DNA virus is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 141-141 | Enveloped virus is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 126-126 | 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 137-137 | 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 146-146 | Virus double stranded is a subclass of virus |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 150-150 | 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 1112-1112 | A viral genome is typically a part of a virus |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1137-1137 | 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 1158-1158 | 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 14554-14558 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14560-14568 |
|
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1146-1151 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3738-3750 |
|
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1139-1144 |
|
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1105-1110 |
|
|
|
|