|
|
  ChineseTraditionalLanguage
|
|
|
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1522-1524 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 2641-2641 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 2817-2817 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 19-19 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 23-23 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 27-27 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 35-35 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55-55 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 2701-2701 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 2713-2713 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 91-91 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 2741-2741 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 207-207 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 219-219 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 2837-2837 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 223-223 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 2877-2877 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 2885-2885 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 279-279 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 283-283 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 315-315 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 323-323 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 2905-2905 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 3133-3133 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 331-331 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2132-2138 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2159-2160 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1753-1754 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2958-2962 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1611-1615 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1836-1840 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1879-1882 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1780-1783 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1950-1950 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1976-1976 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 928-930 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 945-946 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3058-3062 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 747-747 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 616-616 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 631-631 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 117-118 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 146-146 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 820-820 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 871-871 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 845-845 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 858-858 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 832-832 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 805-805 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 790-790 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
|
|
|