WhenFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2736-2738 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8471-8474 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1462-1464 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8468-8468 | 何时函数 的 1 数量 是 物理 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8465-8465 | 何时函数 是 时间关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8467-8467 | 何时函数 是 总值关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8466-8466 | 何时函数 是 一元函数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8469-8469 | 何时函数 的 range 是 时距 的实例 |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 455-455 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 461-461 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 264-264 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 314-314 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2054-2054 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 216-216 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 270-270 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 595-595 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 349-349 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 285-285 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 290-290 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 506-506 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4225-4225 | 表示位置的函数 和 何时函数 是 内部相关 |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 62985-62985 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 456-456 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 62984-62984 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 62983-62983 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3984-4004 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 367-385 |
|
No TPTP formula. May not be expressible in strict first order. | Cars.kif 2585-2603 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22920-22925 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29595-29604 | |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6470-6482 | |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6447-6459 | |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1500-1512 | |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3231-3245 | |
No TPTP formula. May not be expressible in strict first order. | Law.kif 480-489 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30662-30683 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18203-18209 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18181-18187 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17193-17203 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 501-514 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9839-9861 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12383-12397 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9900-9922 |
|
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. | Mid-level-ontology.kif 487-499 | |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 89-103 | |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 665-671 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 13831-13839 | |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6505-6529 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 11647-11654 | |
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. | Merge.kif 12466-12473 | 过程 是 结合 的 instance 和 客体 是 那个 过程 的 resource 和 实体 是 那个 过程 的 result 若且唯若 那个 客体 不 是 那个 实体 的 part 在 那个 过程 出现 的 time 的开始 holdsDuring 和 那个 客体 是 那个 实体 的 part 在 那个 过程 出现 的 time 的结束 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | People.kif 357-390 | 年 是 那个 年EAR year 的 instance 和 地缘政治区域 和 那个 年 的 male 出生估计寿命 equal 实数 若且唯若 有存在 串列, 另一个 整数,, , 符号串,, , 实体,, , 另一个 实体, and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
No TPTP formula. May not be expressible in strict first order. | People.kif 82-97 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千的 births equal 实数 若且唯若 那个 地缘政治区域 的 population 和 1000 equal 另一个 实数 和 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 那个 另外 实数 equal 那个 实数 |
No TPTP formula. May not be expressible in strict first order. | People.kif 118-133 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千里的 deaths equal 实数 若且唯若 那个 地缘政治区域 的 population 和 1000 equal 另一个 实数 和 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 那个 另外 实数 equal 那个 实数 |
No TPTP formula. May not be expressible in strict first order. | People.kif 238-264 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千个生存出生里的 deaths equal 实数 若且唯若 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 1000 equal 另一个 实数 和 第三 整数 equal 另一个 符号串 所描述的类别 instance 的数量 和 那个 第三 整数 和 那个 另外 实数 equal 那个 实数 |
No TPTP formula. May not be expressible in strict first order. | People.kif 403-436 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的 female 出生预期寿命 equal 实数 若且唯若 有存在 串列, 另一个 整数,, , 符号串,, , 实体,, , 另一个 实体, and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
No TPTP formula. May not be expressible in strict first order. | People.kif 310-342 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的出生预期 life equal 实数 若且唯若 有存在 串列, 另一个 整数,, , 符号串,, , 实体,, , 另一个 实体, and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30223-30236 | Alone 是 实体 的 attribute 在 时距 holdsDuring 若且唯若 不存在 那个 实体2 和 过程 这样 那个 实体 不 equal 那个 实体2 和 那个 实体2 是 施事体 的 instance 和 那个 过程 是 社交 的 instance 和 那个 过程 出现 的 time 在 那个 时距 时段内发生 和 那个 实体 是事件 那个 过程 的 involved 和 那个 实体2 是事件 那个 过程 的 involved |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30271-30279 | Mute 是 施事体 的 attribute 在 时距 holdsDuring 若且唯若 不存在 过程 这样 那个 过程 是 说话 的 instance 和 那个 过程 出现 的 time 在 那个 时距 时段内发生 和 那个 施事体 是 那个 过程 的 agent |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 968-975 | 整数 是 机构 的 year 资金 若且唯若 有存在 过程 和 那个 整数EAR 这样 那个 整数EAR 时段 和 那个 过程 出现 的 time 重叠 和 那个 整数EAR 是 那个 整数 year 的 instance 和 那个 过程 是 创建 的 instance 和 那个 机构 是 那个 过程 的 result |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16852-16861 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20760-20767 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18837-18843 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6231-6244 | |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4373-4382 | |
No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 204-223 |
|
No TPTP formula. May not be expressible in strict first order. | Music.kif 457-470 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2881-2897 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2917-2933 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2854-2870 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2008-2029 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2031-2052 |
|
No TPTP formula. May not be expressible in strict first order. | Dining.kif 1207-1224 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 13841-13854 |
|
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 684-695 | |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
statement |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18202-18219 | 有存在 ?X, ?CUT,, , ?PAPER,, , ?CBO, and 和 ?INFO 这样 ?X 是 PaperShredder 的 instance 和 ?CUT 是 切开 的 instance 和 ?X 是导致 ?CUT 的 instrument 和 ?PAPER 是 纸 的 instance 和 ?PAPER 是 ?CUT 的 patient 和 ?CBO 是 located 在 ?PAPER 和 ?CBO 是 VisualContentBearingObject 的 instance 和 ?CBO contains ?INFO 的资料 减少 有存在 ?READ 这样 ?READ 是 解读 的 instance 和 ?INFO 是 ?READ 的 patient 和 ?CUT 出现 的 time 比?READ 出现 的 time发生的earlier 发生的机率 |
No TPTP formula. May not be expressible in strict first order. | Media.kif 1970-1978 | 有存在 时距 这样 那个 时距 是 时距 的 instance 和 那个 时距 finishes了才到 JesusOfNazareth 出现 的 time 和 那个 时距 starts了才到 TwelveApostles 出现 的 time 和 对所有 实体
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 1920-1920 | JesusOfNazareth 是 located 在 巴勒斯坦 在 JesusOfNazareth 出现 的 time holdsDuring |