| TimeInterval(时距) | |
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1785-1786 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2086-2089 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 398-401 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2084-2084 | 时距 是 时间位置 的 subclass |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7885-7885 | 共同的时代之前 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7893-7893 | 共同时代 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2079-2079 | 时间位置 详尽无遗地 partition 成 时距 和 时点 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3726-3726 | 财政年度开始 的 range 是 时距 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8512-8512 | 未来函数 的 range 是 时距 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8529-8529 | 紧接未来函数 的 range 是 时距 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8498-8498 | 紧接过去函数 的 range 是 时距 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8480-8480 | 过去函数 的 range 是 时距 的实例 |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3749-3749 | SiteSpeedFn 的 range 是 时距 的实例 |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1494-1494 | TTFxFn 的 range 是 时距 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8413-8413 | 时段函数 的 range 是 时距 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14038-14038 | TimePeriodFn 的 range 是 时距 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8469-8469 | 何时函数 的 range 是 时距 的实例 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3698-3698 | 财政年度 的所得值 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8446-8446 | 重复发生时间函数 的所得值 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9375-9375 | 时间分拆函数 的所得值 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19091-19091 | 上午 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1849-1849 | BreakfastTime 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9230-9230 | 日 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8857-8857 | 一天的时间 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8765-8765 | Decade 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 112-112 | Dhu al hijjah 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1878-1878 | DinnerTime 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14848-14848 | 假日 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9340-9340 | 小时 是 时距 的 subclass |
| 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. | Merge.kif 7982-7982 | 开始函数 的 1 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 1048-1048 | ContestFn 的 2 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8010-8010 | 结束函数 的 1 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3160-3160 | GPIFn 的 2 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 2219-2219 | 10分钟平均地面风速 的 2 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 2324-2324 | 1分钟平均地面风速 的 2 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 2289-2289 | 2分钟平均地面风速 的 2 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 2254-2254 | 3分钟平均地面风速 的 2 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1900-1900 | 3秒平均地面风速 的 2 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1994-1994 | 平均3秒风速表列 的 2 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 847-847 | MusicalInterpretationFn 的 3 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3086-3086 | PPIFn 的 2 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3660-3660 | SCRFn 的 2 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3364-3364 | SiteWideNewBuyersFn 的 1 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3416-3416 | SiteWideNewRegistrationsFn 的 1 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3463-3463 | SiteWideNewSellersFn 的 1 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9373-9373 | 时间分拆函数 的 1 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 2034-2034 | 3秒阵风风速 的 2 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1956-1956 | 时间间隔表列 的 1 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14011-14011 | 协议期限 的 2 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 986-986 | 期间平均温度 的 2 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10378-10378 | breathingRate 的 2 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4303-4303 | burnInPeriod 的 2 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 554-554 | 复利 的 3 数量 是 时距 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20803-20803 | constructionPeriod 的 2 数量 是 时距 的 instance |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 151-167 |
|
| No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 26-47 |
|
| No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 120-131 | |
| No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 101-111 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7972-7982 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3836-3843 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3759-3784 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3095-3114 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3056-3073 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23513-23526 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3376-3408 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3428-3455 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3475-3507 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8354-8364 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8242-8247 | |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 466-482 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8420-8428 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8430-8439 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1496-1518 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8262-8267 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8269-8279 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 440-447 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 456-463 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 465-472 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 481-488 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 26-47 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1326-1342 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 643-661 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23513-23526 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3376-3408 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3428-3455 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3475-3507 |
|
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1929-1933 | |
| No TPTP formula. May not be expressible in strict first order. | naics.kif 8776-8797 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18150-18184 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1605-1621 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3629-3638 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3640-3650 |
|
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2808-2820 | |
| No TPTP formula. May not be expressible in strict first order. | Catalog.kif 467-492 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14376-14382 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22334-22346 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17323-17345 |
|
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 266-286 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7940-7945 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8345-8352 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8234-8240 |
| statement |
|
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 1970-1978 | 有存在 时距 这样 那个 时距 是 时距 的 instance 和 那个 时距 finishes了才到 JesusOfNazareth 出现 的 time 和 那个 时距 starts了才到 TwelveApostles 出现 的 time 和 对所有 实体
|
|
|
|