d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder%------------------------------------------------------------------------------
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% File : CSR134^1 : TPTP v5.4.0. Released v4.1.0.
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Domain : Commonsense Reasoning
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Problem : In 2009, what are different feelings of people to Anna?
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Version : Especial.
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% English : In the context of year 2009: Does there exists a relation ?R and
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% persons ?X and ?Y so that ?R holds between ?X and Anna but not
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% between ?Y and Anna.
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Refs : [Ben10] Benzmueller (2010), Email to Geoff Sutcliffe
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Source : [Ben10]
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Names : ef_rv_6.tq_SUMO_local [Ben10]
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Status : Theorem
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Rating : 0.40 v5.4.0, 0.50 v5.1.0, 0.75 v5.0.0, 0.50 v4.1.0
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Syntax : Number of formulae : 23 ( 8 unit; 12 type; 0 defn)
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Number of atoms : 92 ( 0 equality; 4 variable)
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Maximal formula depth : 9 ( 4 average)
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Number of connectives : 62 ( 0 ~; 0 |; 1 &; 61 @)
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% ( 0 ~|; 0 ~&; 0 !!; 0 ??)
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Number of type conns : 9 ( 9 >; 0 *; 0 +; 0 <<)
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Number of symbols : 16 ( 12 :)
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Number of variables : 3 ( 0 sgn; 0 !; 3 ?; 0 ^)
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% ( 3 :; 0 !>; 0 ?*)
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% SPC : THF_THM_NEQ
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Comments : This is a simple test problem for reasoning in/about SUMO.
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% Initally the problem has been hand generated in KIF syntax in
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% SigmaKEE and then automatically translated by Benzmueller's
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% KIF2THF translator into THF syntax.
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% : The translation has been applied in two modes: local and SInE.
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% The local mode only translates the local assumptions and the
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% query. The SInE mode additionally translates the SInE-extract
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% of the loaded knowledge base (usually SUMO).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% : The examples are selected to illustrate the benefits of
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder% higher-order reasoning in ontology reasoning.
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder%------------------------------------------------------------------------------
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder%----The extracted signature
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(numbers,type,(
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder num: $tType )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(holdsDuring_THFTYPE_IiooI,type,(
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder holdsDuring_THFTYPE_IiooI: $i > $o > $o )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(lAnna_THFTYPE_i,type,(
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder lAnna_THFTYPE_i: $i )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(lBen_THFTYPE_i,type,(
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder lBen_THFTYPE_i: $i )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(lBill_THFTYPE_i,type,(
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder lBill_THFTYPE_i: $i )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(lBob_THFTYPE_i,type,(
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder lBob_THFTYPE_i: $i )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(lMary_THFTYPE_i,type,(
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder lMary_THFTYPE_i: $i )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(lSue_THFTYPE_i,type,(
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder lSue_THFTYPE_i: $i )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(lYearFn_THFTYPE_IiiI,type,(
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder lYearFn_THFTYPE_IiiI: $i > $i )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(likes_THFTYPE_IiioI,type,(
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder likes_THFTYPE_IiioI: $i > $i > $o )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(n2009_THFTYPE_i,type,(
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder n2009_THFTYPE_i: $i )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(parent_THFTYPE_IiioI,type,(
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder parent_THFTYPE_IiioI: $i > $i > $o )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder%----The translated axioms
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i ) )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(ax_001,axiom,
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i ) )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(ax_002,axiom,
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( ~ @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ) ) )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(ax_003,axiom,
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i ) )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(ax_004,axiom,
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i ) )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(ax_005,axiom,
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( ~ @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBen_THFTYPE_i ) ) )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(ax_006,axiom,
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i ) )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(ax_007,axiom,
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i ) )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(ax_008,axiom,
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i ) )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(ax_009,axiom,
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( ~ @ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i ) ) )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder%----The translated conjecture
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroederthf(con,conjecture,(
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder ? [R: $i > $i > $o,X: $i,Y: $i] :
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder ( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder @ ( ( R @ X @ lAnna_THFTYPE_i )
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder & ( ~ @ ( R @ Y @ lAnna_THFTYPE_i ) ) ) ) )).
d648ccc675f318e26fad4c12f00562e7e0048851Jonathan von Schroeder%------------------------------------------------------------------------------