exists |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 65825-65825 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 1818-1828 | 过程 是 退出 的 instance 和 金融账户 是 金融账户 的 instance 和 那个 金融账户 的 currency 是 那个 过程 的源头 和 不存在 另一个 过程 这样 那个 另外 过程 是 罚款 的 instance 和 那个 另外 过程 在 那个 金融账户 的 currency 结束 和 那个 过程 causes 那个 另外 过程 若且唯若 那个 金融账户 的 liqudity 是 高流动性 |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3920-3926 | 有存在 时距 这样 贷款 是 贷款 的 instance 和 那个 时距 是 那个 贷款 的 agreement 週期 和 那个 贷款 是 对于 %3 的赚取 interest 若且唯若 利益 是 那个 贷款 的 loan 利息 |
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 989-992 | 有存在 电脑程序 这样 电脑程序 是 那个 电脑程序 的执行 program 若且唯若 那个 电脑程序 有 可执行 的 attribute |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 981-984 | 有存在 数字 这样 那个 数字 是 金融账户 的 fixed 固定利息 若且唯若 那个 金融账户 是 固定利率账户 的 instance |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3051-3062 | 有存在 金融工具, 那个 金融工具Price, and 和 另一个 实数 这样 协议 是 看涨期权 的 instance 和 那个 金融工具 是 那个 协议 的 underlier 和 那个 金融工具 是 对于 施事体 的 price 那个 金融工具Price 测量单位 和 那个 测量单位 是 UnitOfCurrency 的 instance 和 那个 另外 实数 那个 测量单位 是 那个 协议 的 strike 价钱 和 那个 金融工具Price 是 lessThan 那个 另外 实数 若且唯若 那个 施事体 是 那个 协议 的 out 资兂短缺 |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3002-3013 | 有存在 金融工具, 那个 金融工具Price, and 和 另一个 实数 这样 协议 是 看涨期权 的 instance 和 那个 金融工具 是 那个 协议 的 underlier 和 那个 金融工具 是 对于 施事体 的 price 那个 金融工具Price 测量单位 和 那个 测量单位 是 UnitOfCurrency 的 instance 和 那个 另外 实数 那个 测量单位 是 那个 协议 的 strike 价钱 和 那个 另外 实数 是 lessThan 那个 金融工具Price 若且唯若 那个 施事体 是 那个 协议 的 in 金钱 |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3034-3042 | 有存在 金融工具, 那个 金融工具Price, and 和 另一个 货币测量 这样 协议 是 选项 的 instance 和 那个 金融工具 是 那个 协议 的 underlier 和 那个 金融工具 是 对于 施事体 的 price 那个 金融工具Price 和 那个 另外 货币测量 是 那个 协议 的 strike 价钱 和 那个 金融工具Price equal 那个 另外 货币测量 若且唯若 那个 施事体 是 那个 协议 at 的钱 |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3015-3026 | 有存在 金融工具, 那个 金融工具Price, and 和 另一个 实数 这样 协议 是 放选项 的 instance 和 那个 金融工具 是 那个 协议 的 underlier 和 那个 金融工具 是 对于 施事体 的 price 那个 金融工具Price 测量单位 和 那个 测量单位 是 UnitOfCurrency 的 instance 和 那个 另外 实数 那个 测量单位 是 那个 协议 的 strike 价钱 和 那个 金融工具Price 是 lessThan 那个 另外 实数 若且唯若 那个 施事体 是 那个 协议 的 in 金钱 |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3064-3075 | 有存在 金融工具, 那个 金融工具Price, and 和 另一个 实数 这样 协议 是 放选项 的 instance 和 那个 金融工具 是 那个 协议 的 underlier 和 那个 金融工具 是 对于 施事体 的 price 那个 金融工具Price 测量单位 和 那个 测量单位 是 UnitOfCurrency 的 instance 和 那个 另外 实数 那个 测量单位 是 那个 协议 的 strike 价钱 和 那个 另外 实数 是 lessThan 那个 金融工具Price 若且唯若 那个 施事体 是 那个 协议 的 out 资兂短缺 |
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. | Military.kif 772-778 | |
No TPTP formula. May not be expressible in strict first order. | Dining.kif 130-150 |
|
No TPTP formula. May not be expressible in strict first order. | Dining.kif 336-350 | |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 853-866 |
|
No TPTP formula. May not be expressible in strict first order. | Dining.kif 772-795 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 759-775 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 5016-5025 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3239-3259 | |
No TPTP formula. May not be expressible in strict first order. | Dining.kif 586-602 |
|
No TPTP formula. May not be expressible in strict first order. | Cars.kif 1772-1786 |
|
No TPTP formula. May not be expressible in strict first order. | Cars.kif 3905-3921 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1417-1436 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1395-1413 | |
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. | MilitaryDevices.kif 1409-1418 | |
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. | Mid-level-ontology.kif 30178-30188 | 实体 是 身体部位 的 instance 和 Bare 是 那个 实体 的 attribute 在 时间位置 holdsDuring 若且唯若 不存在 另一个 实体 这样 那个 另外 实体 是 服装 的 instance 和 covers 那个 另外 实体 and 那个 实体 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26329-26340 | 过程 是 Photocopying 的 instance 和 内容承载物理 是 那个 过程 的 patient 和 那个 内容承载物理 是 VisualContentBearingObject 的 instance 和 那个 内容承载物理 contains 命题 的资料 若且唯若 有存在 另一个 内容承载物理 和 另一个 命题 这样 那个 另外 内容承载物理 是 那个 过程 的 result 和 那个 另外 内容承载物理 是 VisualContentBearingObject 的 instance 和 那个 另外 内容承载物理 contains 那个 另外 命题 的资料 和 那个 命题 equal 那个 另外 命题 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 7440-7451 | 客体 是 悬浮颗粒 的 instance 和 自身连接物体 是 那个 客体 的 part 和 1 的 approximate diameter 是 %2 和 10.0 是 greaterThan 实数 和 那个 实数 是 greaterThan 2.5 若且唯若 有存在 那个 客体10 这样 那个 客体10 是 粗悬浮颗粒 的 instance 和 那个 客体10 是 那个 客体 的 part |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 7469-7479 | 客体 是 悬浮颗粒 的 instance 和 自身连接物体 是 那个 客体 的 part 和 1 的 approximate diameter 是 %2 和 实数 是 greaterThanOrEqualTo 2.5 若且唯若 有存在 那个 客体25 这样 那个 客体25 是 细悬浮颗粒 的 instance 和 那个 客体25 是 那个 客体 的 part |
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 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. | Economy.kif 1517-1522 | 1 对于 %3 在周期 %2 的 annual 地区消费 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 货币测量 是 地缘政治区域 在 annual 地区消费 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 1488-1493 | 地缘政治区域 annual 对于 有点 时距 在周期 货币测量 的地区收入 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 货币测量 是 那个 地缘政治区域 的 annual 地区收入 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 751-762 | 和弦音乐 是 客体 的 attribute 若且唯若 有存在 过程 和 另一个 过程 这样 那个 客体 是 制作音乐 的 instance 和 那个 过程 是 制作音乐 的 instance 和 那个 另外 过程 是 制作音乐 的 instance 和 那个 过程%n是那个 客体的subProcess 和 那个 另外 过程%n是那个 客体的subProcess 和 那个 过程 不 equal 那个 另外 过程 和 那个 过程 和 那个 客体 同时发生 和 那个 另外 过程 和 那个 客体 同时发生 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 4711-4720 | 公海 是 客体 的 attribute 若且唯若 有存在 物理 和 实数 这样 那个 客体 是 盐水区 的 instance 和 那个 客体 不 是 内陆水域 的 instance 和 那个 物理 和 那个 客体 的 distance 是 那个 实数 海里 和 那个 实数 是 greaterThan 5.0 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23046-23051 | 女人 是 人类 的 aunt 若且唯若 有存在 另一个 人类 这样 那个 女人 是 那个 另外 人类 的 sister 和 那个 另外 人类 是 那个 人类 的 parent |
No TPTP formula. May not be expressible in strict first order. | People.kif 272-293 | 实数 是 串列 的 average 若且唯若 有存在 另一个 串列 和 正整数 这样 那个 另外 串列 的长度 equal 那个 串列 的长度 和 那个 另外 串列 的第 1 几个元素 equal 那个 串列 的第 1 几个元素 和 对所有 另一个 正整数
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3943-3948 | BankFinancialOrganization 是 有点 金融账户 的 bank 帐号 若且唯若 有存在 另一个 金融账户 这样 那个 另外 金融账户 是 有点 金融账户 的 instance 和 那个 另外 金融账户 是被 那个 BankFinancialOrganization held |
No TPTP formula. May not be expressible in strict first order. | People.kif 1528-1539 | 百分之 实数 在 信仰团体 的人相信 那个 信仰团体 若且唯若 有存在 群体, 另一个 群体,, , 物理,, , 那个 物理2,, , 那个 实数1, and 和 那个 实数2 这样 那个 物理 是 located 在 地理区域 和 那个 物理 是 那个 信仰团体 的 member 和 那个 物理 是 那个 群体 的 member 和 那个 实数1 是 那个 群体 的 member 计数 和 那个 物理2 是 located 在 那个 地理区域 和 那个 物理2 是 那个 另外 群体 的 member 和 那个 实数2 是 那个 另外 群体 的 member 计数 和 那个 实数 和 100 equal 那个 实数1 和 那个 实数2 |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 1565-1570 | 地缘政治区域 在周期 货币测量 对于 有点 时距 的 capital 地区支出 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 货币测量 是 那个 地缘政治区域 的 capital 地区支出 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23061-23076 | 人类 另一个 人类 是 cousins 若且唯若 有存在 女人 和 人 这样 那个 人类 的 grandmother 是 那个 女人 和 那个 人类 的 grandfather 是 那个 人 和 那个 另外 人类 的 grandmother 是 那个 女人 和 那个 另外 人类 的 grandfather 是 那个 人 和 不存在 生物 和 另一个 生物 这样 那个 生物 是 那个 人类 的 mother 和 那个 另外 生物 是 那个 人类 father 和 那个 生物 是 那个 另外 人类 的 mother 和 那个 另外 生物 是 那个 另外 人类 father |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3661-3666 | 有点 时距 是 货币测量 的 currency 交换 每美元 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 货币测量 是 美国美元 的 currency 交换汇率 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3668-3673 | UnitOfCurrency 对于 有点 时距 在周期 货币测量 的 currency 交换汇率 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 货币测量 是 那个 UnitOfCurrency 的 currency 交换汇率 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7727-7733 | 施事体 是 有认知的主事 的 customer 若且唯若 有存在 过程 这样 那个 过程 是 金融交易 的 instance 和 那个 施事体 是 那个 过程 的 agent 和 那个 过程 在 那个 有认知的主事 结束 |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3635-3642 | 有认知的主事 对于 %3 的 customer 代表 若且唯若 有存在 过程 这样 那个 过程 是 金融交易 的 instance 和 机构 employs 那个 有认知的主事 和 那个 有认知的主事 是 那个 过程 的 agent 和 那个 过程 在 另一个 有认知的主事 结束 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 2781-2786 | 客体 是 长度测量 above 地表 若且唯若 有存在 自身连接物体 这样 那个 客体 的 altitude 是 那个 自身连接物体 和 那个 自身连接物体 是 行星地球 的 surface |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2819-2824 | 地缘政治区域 是 对于 有点 时距 在期间 货币测量 的 economic 间赠补助 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 货币测量 是 那个 地缘政治区域 的 economic 捐赠补助 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2859-2864 | 地缘政治区域 是 对于 有点 时距 在期间 货币测量 总共收到的 economic 补助 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 货币测量 是 那个 地缘政治区域 总共收到的 economic 补助 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2056-2061 | 地缘政治区域 是 对于 实数 和 有点 时距 在周期 有点 发电 从来源的 electricity 分支 若且唯若 有存在 时间位置 这样 那个 时间位置 是 有点 时距 的 instance 和 那个 地缘政治区域 is 对于 那个 实数 从来源 有点 发电 的 electricity 分支 在 那个 时间位置 holdsDuring |
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. | Government.kif 1160-1174 | 对所有 ?POLITY, ?VOTER,, , ?ELECTION,, , ?VOTINGAGE, and 和 ?AGE
|
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. | ComputingBrands.kif 3309-3315 | IBookstore 的 目的 是 有存在 ?D 这样 ?D 是 下載 的 instance 和 iBookstore 是导致 ?D 的 instrument 和 ?T 是 文本 的 instance 和 objectTransferred ?D and ?T |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6099-6106 | 不存在 图路径 和 另一个 图路径 这样 那个 图路径 是 把 图 分成另外两个图的路径 Set 的 instance 和 那个 另外 图路径 是 把 那个 图 分成另外两个图的最短路径 Set 的 instance 和 那个 图路径 的 length 是 正整数 和 那个 另外 图路径 的 length 是 另一个 正整数 和 那个 正整数 是 lessThan 那个 另外 正整数 |
appearance as argument number 0 |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 4559-4564 | 有存在 过程 和 实体 这样 那个 过程 是 传播 的 instance 和 Netflix 是 那个 过程 的 agent 和 那个 实体 是 那个 过程 的 patient 和 那个 实体 是 动态映像 的 instance |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 4566-4569 | 有存在 过程 这样 那个 过程 是 电影制作 的 instance 和 Netflix 是 那个 过程 的 agent |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 4590-4593 | 有存在 有认知的主事 这样 NewReporter 是 那个 有认知的主事 的 attribute 和 ProPublica employs 那个 有认知的主事 |
No TPTP formula. May not be expressible in strict first order. | Food.kif 1902-1903 | 有存在 Meal 和 地区 这样 对于 那个 Meal 合适的 meal 在 那个 地区 是 那个 Meal 的 attribute |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2453-2457 | 有存在 时间位置 这样 那个 时间位置 是 1976 year 的 instance 和 斯蒂夫·沃兹尼亚克 是 史蒂芬·贾伯斯 的 coworker 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2441-2445 | 有存在 时间位置 这样 那个 时间位置 是 2002 year 的 instance 和 提姆·库克 是 史蒂芬·贾伯斯 的 coworker 在 那个 时间位置 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 5109-5112 | 有存在 有点 客体 这样 有点 客体 是 HandToolBox 的 subclass 和 manufacturer 那个 有点 客体 and SortimoCorp |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 825-826 | 有存在 实体 这样 那个 实体 是 实体 的 instance |
No TPTP formula. May not be expressible in strict first order. | Media.kif 1970-1978 | 有存在 时距 这样 那个 时距 是 时距 的 instance 和 那个 时距 finishes了才到 JesusOfNazareth 出现 的 time 和 那个 时距 starts了才到 TwelveApostles 出现 的 time 和 对所有 实体
|