|
|
  JapaneseLanguage
|
|
|
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11323-11340 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 6642-6642 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 7123-7123 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 7124-7124 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2134-2134 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2131-2131 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2013-2013 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1974-1974 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2051-2051 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2166-2166 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2073-2073 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2135-2135 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2070-2070 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2136-2136 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2172-2172 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2061-2061 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2137-2137 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2125-2125 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2133-2133 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2093-2093 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2052-2052 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2167-2167 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2138-2138 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1975-1975 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2139-2139 | |
| 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 2148-2154 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2165-2167 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 888-889 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 306-310 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1759-1763 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 878-879 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2970-2976 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1622-1632 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1515-1516 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 275-276 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1848-1851 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1889-1893 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1790-1798 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1769-1770 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1193-1196 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1293-1294 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1113-1113 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1298-1299 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1332-1332 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 249-250 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 461-465 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1953-1953 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 1978-1979 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 934-938 | |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 949-953 | |
| 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. | Languages.kif 14778-14778 | "ja" in ISO-639-1 denotes japanese language |
|
|
|
