| GraphElement(graph element)
|
| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2340-2341 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5847-5848 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1014-1015 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 1788-1788 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5845-5845 | Graph element is exhaustively partitioned into graph node and graph arc |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5844-5844 | Graph element is a subclass of proposition |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5867-5867 | Graph arc is a subclass of graph element |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5857-5857 | Graph node is a subclass of graph element |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 940-940 | Graph node is a subclass of graph element |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 1087-1087 | Graph node is a subclass of graph element |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 616-616 | Graph node is a subclass of graph element |
| No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 147-147 | Graph node is a subclass of graph element |
| No TPTP formula. May not be expressible in strict first order. | terms-it.txt 150-150 | Graph node is a subclass of graph element |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2301-2301 | Graph node is a subclass of graph element |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 568-568 | Graph node is a subclass of graph element |
| No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 152-152 | Graph node is a subclass of graph element |
| No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 184-184 | Graph node is a subclass of graph element |
| No TPTP formula. May not be expressible in strict first order. | terms-de.txt 443-443 | Graph node is a subclass of graph element |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 637-637 | Graph node is a subclass of graph element |
| No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 151-151 | Graph node is a subclass of graph element |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5913-5913 | The number 1 argument of graph part is an instance of graph element |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5850-5855 |
|
|
|
|