%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : CSR140^2 : TPTP v9.2.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Feb 25 08:43:08 AM UTC 2026
% Result : Theorem 1.85s 1.48s
% Output : Refutation 1.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 3
% Syntax : Number of formulae : 21 ( 8 unt; 0 typ; 0 def)
% Number of atoms : 88 ( 19 equ; 0 cnn)
% Maximal formula atoms : 3 ( 4 avg)
% Number of connectives : 85 ( 22 ~; 5 |; 4 &; 54 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Number of types : 3 ( 1 usr)
% Number of type conns : 16 ( 16 >; 0 *; 0 +; 0 <<)
% Number of symbols : 21 ( 18 usr; 5 con; 0-3 aty)
% Number of variables : 26 ( 0 ^; 14 !; 12 ?; 26 :)
% Comments :
%------------------------------------------------------------------------------
thf(func_def_0,type,
num: $tType ).
thf(func_def_2,type,
domain_THFTYPE_IIiioIiioI: ( $i > $i > $o ) > $i > $i > $o ).
thf(func_def_3,type,
domain_THFTYPE_IiiioI: $i > $i > $i > $o ).
thf(func_def_5,type,
holdsDuring_THFTYPE_IiooI: $i > $o > $o ).
thf(func_def_6,type,
instance_THFTYPE_IIiioIioI: ( $i > $i > $o ) > $i > $o ).
thf(func_def_7,type,
instance_THFTYPE_IIiooIioI: ( $i > $o > $o ) > $i > $o ).
thf(func_def_8,type,
instance_THFTYPE_IiioI: $i > $i > $o ).
thf(func_def_18,type,
likes_THFTYPE_IiioI: $i > $i > $o ).
thf(func_def_21,type,
parent_THFTYPE_IiioI: $i > $i > $o ).
thf(func_def_22,type,
range_THFTYPE_IiioI: $i > $i > $o ).
thf(func_def_23,type,
subclass_THFTYPE_IiioI: $i > $i > $o ).
thf(func_def_24,type,
subrelation_THFTYPE_IIioIIioIoI: ( $i > $o ) > ( $i > $o ) > $o ).
thf(func_def_25,type,
subrelation_THFTYPE_IiioI: $i > $i > $o ).
thf(func_def_28,type,
vEPSILON:
!>[X0: $tType] : ( ( X0 > $o ) > X0 ) ).
thf(func_def_31,type,
sK0: $i > $i ).
thf(func_def_33,type,
ph2:
!>[X0: $tType] : X0 ).
thf(f230,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[f227]) ).
thf(f227,plain,
$false = $true,
inference(superposition,[status(thm)],[f225,f215]) ).
thf(f215,plain,
( ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i )
= $false ),
inference(not_proxy_clausification,[status(thm)],[f177]) ).
thf(f177,plain,
( ( ~ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f123]) ).
thf(f123,plain,
( ( ~ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ) )
= $true ),
inference(fool_elimination,[status(thm)],[f122]) ).
thf(f122,plain,
~ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ),
inference(rectify,[status(thm)],[f26]) ).
thf(f26,axiom,
~ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ),
file('/export/starexec/sandbox/tmp/tmp.00Y5TSrdar/DTF2THF_24285.p',ax_025) ).
thf(f225,plain,
! [X0: $i] :
( $true
= ( parent_THFTYPE_IiioI @ X0 @ lAnna_THFTYPE_i ) ),
inference(trivial_inequality_removal,[status(thm)],[f222]) ).
thf(f222,plain,
! [X0: $i] :
( ( $true != $true )
| ( $true
= ( parent_THFTYPE_IiioI @ X0 @ lAnna_THFTYPE_i ) ) ),
inference(superposition,[status(thm)],[f221,f178]) ).
thf(f178,plain,
( ( parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i )
= $true ),
inference(cnf_transformation,[status(thm)],[f135]) ).
thf(f135,plain,
( ( parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i )
= $true ),
inference(fool_elimination,[status(thm)],[f134]) ).
thf(f134,plain,
parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i,
inference(rectify,[status(thm)],[f14]) ).
thf(f14,axiom,
parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i,
file('/export/starexec/sandbox/tmp/tmp.00Y5TSrdar/DTF2THF_24285.p',ax_013) ).
thf(f221,plain,
! [X2: $i,X0: $i > $i > $o,X1: $i] :
( ( ( X0 @ X2 @ lAnna_THFTYPE_i )
!= $true )
| ( $true
= ( X0 @ X1 @ lAnna_THFTYPE_i ) ) ),
inference(not_proxy_clausification,[status(thm)],[f210]) ).
thf(f210,plain,
! [X2: $i,X0: $i > $i > $o,X1: $i] :
( ( ( ~ ( X0 @ X1 @ lAnna_THFTYPE_i ) )
!= $true )
| ( ( X0 @ X2 @ lAnna_THFTYPE_i )
!= $true ) ),
inference(cnf_transformation,[status(thm)],[f166]) ).
thf(f166,plain,
! [X0: $i > $i > $o,X1: $i,X2: $i] :
( ( ( X0 @ X2 @ lAnna_THFTYPE_i )
!= $true )
| ( ( ~ ( X0 @ X1 @ lAnna_THFTYPE_i ) )
!= $true ) ),
inference(rectify,[status(thm)],[f148]) ).
thf(f148,plain,
! [X1: $i > $i > $o,X2: $i,X0: $i] :
( ( $true
!= ( X1 @ X0 @ lAnna_THFTYPE_i ) )
| ( $true
!= ( ~ ( X1 @ X2 @ lAnna_THFTYPE_i ) ) ) ),
inference(ennf_transformation,[status(thm)],[f75]) ).
thf(f75,plain,
~ ? [X0: $i,X1: $i > $i > $o,X2: $i] :
( ( $true
= ( X1 @ X0 @ lAnna_THFTYPE_i ) )
& ( $true
= ( ~ ( X1 @ X2 @ lAnna_THFTYPE_i ) ) ) ),
inference(fool_elimination,[status(thm)],[f74]) ).
thf(f74,plain,
~ ? [X0: $i,X1: $i > $i > $o,X2: $i] :
( ( X1 @ X0 @ lAnna_THFTYPE_i )
& ~ ( X1 @ X2 @ lAnna_THFTYPE_i ) ),
inference(rectify,[status(thm)],[f46]) ).
thf(f46,negated_conjecture,
~ ? [X0: $i,X21: $i > $i > $o,X1: $i] :
( ( X21 @ X0 @ lAnna_THFTYPE_i )
& ~ ( X21 @ X1 @ lAnna_THFTYPE_i ) ),
inference(negated_conjecture,[status(cth)],[f45]) ).
thf(f45,conjecture,
? [X0: $i,X21: $i > $i > $o,X1: $i] :
( ( X21 @ X0 @ lAnna_THFTYPE_i )
& ~ ( X21 @ X1 @ lAnna_THFTYPE_i ) ),
file('/export/starexec/sandbox/tmp/tmp.00Y5TSrdar/DTF2THF_24285.p',con) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : CSR140^2 : TPTP v9.2.1. Released v4.1.0.
% 0.00/0.10 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.12/0.30 % Computer : n002.cluster.edu
% 0.12/0.30 % Model : x86_64 x86_64
% 0.12/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.30 % Memory : 8042.1875MB
% 0.12/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.30 % CPULimit : 300
% 0.12/0.30 % WCLimit : 300
% 0.12/0.30 % DateTime : Tue Feb 24 05:50:03 EST 2026
% 0.12/0.30 % CPUTime :
% 0.12/0.30 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.17/0.40 ---- Original DTF file ---
% 0.17/0.40 thf(spec,logic,$$dhol).
% 0.17/0.40 %------------------------------------------------------------------------------
% 0.17/0.40 % File : CSR140^2 : TPTP v9.2.1. Released v4.1.0.
% 0.17/0.40 % Domain : Commonsense Reasoning
% 0.17/0.40 % Problem : Different feelings for Anna
% 0.17/0.40 % Version : Especial > Augmented > Especial.
% 0.17/0.40 % English : Does there exists a relation ?R and persons ?X and ?Y so that ?R
% 0.17/0.40 % holds between ?X and Anna but not between ?Y and Anna.
% 0.17/0.40
% 0.17/0.40 % Refs : [Ben10] Benzmueller (2010), Email to Geoff Sutcliffe
% 0.17/0.40 % Source : [Ben10]
% 0.17/0.40 % Names : rv_6.tq_SUMO_sine [Ben10]
% 0.17/0.40
% 0.17/0.40 % Status : Theorem
% 0.17/0.40 % Rating : 0.22 v9.1.0, 0.25 v9.0.0, 0.10 v8.2.0, 0.08 v8.1.0, 0.00 v7.4.0, 0.11 v7.2.0, 0.00 v7.1.0, 0.25 v7.0.0, 0.14 v6.4.0, 0.17 v6.3.0, 0.20 v6.2.0, 0.14 v6.1.0, 0.71 v6.0.0, 0.29 v5.5.0, 0.17 v5.4.0, 0.20 v5.3.0, 0.40 v5.1.0, 0.60 v5.0.0, 0.40 v4.1.0
% 0.17/0.40 % Syntax : Number of formulae : 71 ( 18 unt; 26 typ; 0 def)
% 0.17/0.40 % Number of atoms : 85 ( 2 equ; 9 cnn)
% 0.17/0.40 % Maximal formula atoms : 4 ( 1 avg)
% 0.17/0.40 % Number of connectives : 180 ( 9 ~; 2 |; 9 &; 147 @)
% 0.17/0.40 % ( 2 <=>; 11 =>; 0 <=; 0 <~>)
% 0.17/0.40 % Maximal formula depth : 10 ( 5 avg)
% 0.17/0.40 % Number of types : 3 ( 1 usr)
% 0.17/0.40 % Number of type conns : 38 ( 38 >; 0 *; 0 +; 0 <<)
% 0.17/0.40 % Number of symbols : 27 ( 25 usr; 14 con; 0-3 aty)
% 0.17/0.40 % Number of variables : 36 ( 0 ^; 32 !; 4 ?; 36 :)
% 0.17/0.40 % SPC : TH0_THM_EQU_NAR
% 0.17/0.40
% 0.17/0.40 % Comments : This is a simple test problem for reasoning in/about SUMO.
% 0.17/0.40 % Initally the problem has been hand generated in KIF syntax in
% 0.17/0.40 % SigmaKEE and then automatically translated by Benzmueller's
% 0.17/0.40 % KIF2TH0 translator into THF syntax.
% 0.17/0.40 % : The translation has been applied in two modes: local and SInE.
% 0.17/0.40 % The local mode only translates the local assumptions and the
% 0.17/0.40 % query. The SInE mode additionally translates the SInE-extract
% 0.17/0.40 % of the loaded knowledge base (usually SUMO).
% 0.17/0.40 % : The examples are selected to illustrate the benefits of
% 0.17/0.40 % higher-order reasoning in ontology reasoning.
% 0.17/0.40 %------------------------------------------------------------------------------
% 0.17/0.40 %----The extracted signature
% 0.17/0.40 thf(numbers,type,
% 0.17/0.40 num: $tType ).
% 0.17/0.40
% 0.17/0.40 thf(attribute_THFTYPE_i,type,
% 0.17/0.40 attribute_THFTYPE_i: $i ).
% 0.17/0.40
% 0.17/0.40 thf(domain_THFTYPE_IIiioIiioI,type,
% 0.17/0.40 domain_THFTYPE_IIiioIiioI: ( $i > $i > $o ) > $i > $i > $o ).
% 0.17/0.40
% 0.17/0.40 thf(domain_THFTYPE_IiiioI,type,
% 0.17/0.40 domain_THFTYPE_IiiioI: $i > $i > $i > $o ).
% 0.17/0.40
% 0.17/0.40 thf(equal_THFTYPE_i,type,
% 0.17/0.40 equal_THFTYPE_i: $i ).
% 0.17/0.40
% 0.17/0.40 thf(holdsDuring_THFTYPE_IiooI,type,
% 0.17/0.40 holdsDuring_THFTYPE_IiooI: $i > $o > $o ).
% 0.17/0.40
% 0.17/0.40 thf(instance_THFTYPE_IIiioIioI,type,
% 0.17/0.40 instance_THFTYPE_IIiioIioI: ( $i > $i > $o ) > $i > $o ).
% 0.17/0.40
% 0.17/0.40 thf(instance_THFTYPE_IIiooIioI,type,
% 0.17/0.40 instance_THFTYPE_IIiooIioI: ( $i > $o > $o ) > $i > $o ).
% 0.17/0.40
% 0.17/0.40 thf(instance_THFTYPE_IiioI,type,
% 0.17/0.40 instance_THFTYPE_IiioI: $i > $i > $o ).
% 0.17/0.40
% 0.17/0.40 thf(lAnna_THFTYPE_i,type,
% 0.17/0.40 lAnna_THFTYPE_i: $i ).
% 0.17/0.40
% 0.17/0.40 thf(lAsymmetricRelation_THFTYPE_i,type,
% 0.17/0.40 lAsymmetricRelation_THFTYPE_i: $i ).
% 0.17/0.40
% 0.17/0.40 thf(lBen_THFTYPE_i,type,
% 0.17/0.40 lBen_THFTYPE_i: $i ).
% 0.17/0.40
% 0.17/0.40 thf(lBill_THFTYPE_i,type,
% 0.17/0.40 lBill_THFTYPE_i: $i ).
% 0.17/0.40
% 0.17/0.40 thf(lBinaryPredicate_THFTYPE_i,type,
% 0.17/0.40 lBinaryPredicate_THFTYPE_i: $i ).
% 0.17/0.40
% 0.17/0.40 thf(lBob_THFTYPE_i,type,
% 0.17/0.40 lBob_THFTYPE_i: $i ).
% 0.17/0.40
% 0.17/0.40 thf(lMary_THFTYPE_i,type,
% 0.17/0.40 lMary_THFTYPE_i: $i ).
% 0.17/0.40
% 0.17/0.40 thf(lOrganism_THFTYPE_i,type,
% 0.17/0.40 lOrganism_THFTYPE_i: $i ).
% 0.17/0.40
% 0.17/0.40 thf(lSue_THFTYPE_i,type,
% 0.17/0.40 lSue_THFTYPE_i: $i ).
% 0.17/0.40
% 0.17/0.40 thf(likes_THFTYPE_IiioI,type,
% 0.17/0.40 likes_THFTYPE_IiioI: $i > $i > $o ).
% 0.17/0.40
% 0.17/0.40 thf(n1_THFTYPE_i,type,
% 0.17/0.40 n1_THFTYPE_i: $i ).
% 0.17/0.40
% 0.17/0.40 thf(n2_THFTYPE_i,type,
% 0.17/0.40 n2_THFTYPE_i: $i ).
% 0.17/0.40
% 0.17/0.40 thf(parent_THFTYPE_IiioI,type,
% 0.17/0.40 parent_THFTYPE_IiioI: $i > $i > $o ).
% 0.17/0.40
% 0.17/0.40 thf(range_THFTYPE_IiioI,type,
% 0.17/0.40 range_THFTYPE_IiioI: $i > $i > $o ).
% 0.17/0.40
% 0.17/0.40 thf(subclass_THFTYPE_IiioI,type,
% 0.17/0.40 subclass_THFTYPE_IiioI: $i > $i > $o ).
% 0.17/0.40
% 0.17/0.40 thf(subrelation_THFTYPE_IIioIIioIoI,type,
% 0.17/0.40 subrelation_THFTYPE_IIioIIioIoI: ( $i > $o ) > ( $i > $o ) > $o ).
% 0.17/0.40
% 0.17/0.40 thf(subrelation_THFTYPE_IiioI,type,
% 0.17/0.40 subrelation_THFTYPE_IiioI: $i > $i > $o ).
% 0.17/0.40
% 0.17/0.40 %----The translated axioms
% 0.17/0.40 thf(ax,axiom,
% 0.17/0.40 likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_001,axiom,
% 0.17/0.40 likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_002,axiom,
% 0.17/0.40 (~) @ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i ) ).
% 0.17/0.40
% 0.17/0.40 thf(ax_003,axiom,
% 0.17/0.40 (~) @ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i ) ).
% 0.17/0.40
% 0.17/0.40 %KIF documentation:(documentation instance EnglishLanguage "An object is an &%instance of a &%SetOrClass if it is included in that &%SetOrClass. An individual may be an instance of many classes, some of which may be subclasses of others. Thus, there is no assumption in the meaning of &%instance about specificity or uniqueness.")
% 0.17/0.40 %KIF documentation:(documentation range EnglishLanguage "Gives the range of a function. In other words, (&%range ?FUNCTION ?CLASS) means that all of the values assigned by ?FUNCTION are &%instances of ?CLASS.")
% 0.17/0.40 %KIF documentation:(documentation EnglishLanguage EnglishLanguage "A Germanic language that incorporates many roots from the Romance languages. It is the official language of the &%UnitedStates, the &%UnitedKingdom, and many other countries.")
% 0.17/0.40 thf(ax_004,axiom,
% 0.17/0.40 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_005,axiom,
% 0.17/0.40 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_006,axiom,
% 0.17/0.40 ! [X: $i,Y: $i,Z: $i] :
% 0.17/0.40 ( ( ( subclass_THFTYPE_IiioI @ X @ Y )
% 0.17/0.40 & ( instance_THFTYPE_IiioI @ Z @ X ) )
% 0.17/0.40 => ( instance_THFTYPE_IiioI @ Z @ Y ) ) ).
% 0.17/0.40
% 0.17/0.40 thf(ax_007,axiom,
% 0.17/0.40 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_008,axiom,
% 0.17/0.40 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_009,axiom,
% 0.17/0.40 ! [CLASS1: $i,CLASS2: $i] :
% 0.17/0.40 ( ( CLASS1 = CLASS2 )
% 0.17/0.40 => ! [THING: $i] :
% 0.17/0.40 ( ( instance_THFTYPE_IiioI @ THING @ CLASS1 )
% 0.17/0.40 <=> ( instance_THFTYPE_IiioI @ THING @ CLASS2 ) ) ) ).
% 0.17/0.40
% 0.17/0.40 %KIF documentation:(documentation equal EnglishLanguage "(equal ?ENTITY1 ?ENTITY2) is true just in case ?ENTITY1 is identical with ?ENTITY2.")
% 0.17/0.40 %KIF documentation:(documentation AsymmetricRelation EnglishLanguage "A &%BinaryRelation is asymmetric if and only if it is both an &%AntisymmetricRelation and an &%IrreflexiveRelation.")
% 0.17/0.40 thf(ax_010,axiom,
% 0.17/0.40 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBen_THFTYPE_i ) ).
% 0.17/0.40
% 0.17/0.40 thf(ax_011,axiom,
% 0.17/0.40 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBen_THFTYPE_i ) ).
% 0.17/0.40
% 0.17/0.40 thf(ax_012,axiom,
% 0.17/0.40 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_013,axiom,
% 0.17/0.40 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_014,axiom,
% 0.17/0.40 ! [REL2: $i > $o,ROW: $i,REL1: $i > $o] :
% 0.17/0.40 ( ( ( subrelation_THFTYPE_IIioIIioIoI @ REL1 @ REL2 )
% 0.17/0.40 & ( REL1 @ ROW ) )
% 0.17/0.40 => ( REL2 @ ROW ) ) ).
% 0.17/0.40
% 0.17/0.40 %KIF documentation:(documentation subrelation EnglishLanguage "(&%subrelation ?REL1 ?REL2) means that every tuple of ?REL1 is also a tuple of ?REL2. In other words, if the &%Relation ?REL1 holds for some arguments arg_1, arg_2, ... arg_n, then the &%Relation ?REL2 holds for the same arguments. A consequence of this is that a &%Relation and its subrelations must have the same &%valence.")
% 0.17/0.40 thf(ax_015,axiom,
% 0.17/0.40 ! [ORGANISM: $i] :
% 0.17/0.40 ( ( instance_THFTYPE_IiioI @ ORGANISM @ lOrganism_THFTYPE_i )
% 0.17/0.40 => ? [PARENT: $i] : ( parent_THFTYPE_IiioI @ ORGANISM @ PARENT ) ) ).
% 0.17/0.40
% 0.17/0.40 thf(ax_016,axiom,
% 0.17/0.40 ! [TIME: $i,SITUATION: $o] :
% 0.17/0.40 ( ( holdsDuring_THFTYPE_IiooI @ TIME @ ( (~) @ SITUATION ) )
% 0.17/0.40 => ( (~) @ ( holdsDuring_THFTYPE_IiooI @ TIME @ SITUATION ) ) ) ).
% 0.17/0.40
% 0.17/0.40 %KIF documentation:(documentation holdsDuring EnglishLanguage "(&%holdsDuring ?TIME ?FORMULA) means that the proposition denoted by ?FORMULA is true in the time frame ?TIME. Note that this implies that ?FORMULA is true at every &%TimePoint which is a &%temporalPart of ?TIME.")
% 0.17/0.40 thf(ax_017,axiom,
% 0.17/0.40 likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_018,axiom,
% 0.17/0.40 likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_019,axiom,
% 0.17/0.40 ! [THING2: $i,THING1: $i] :
% 0.17/0.40 ( ( THING1 = THING2 )
% 0.17/0.40 => ! [CLASS: $i] :
% 0.17/0.40 ( ( instance_THFTYPE_IiioI @ THING1 @ CLASS )
% 0.17/0.40 <=> ( instance_THFTYPE_IiioI @ THING2 @ CLASS ) ) ) ).
% 0.17/0.40
% 0.17/0.40 thf(ax_020,axiom,
% 0.17/0.40 ! [CLASS1: $i,REL: $i,CLASS2: $i] :
% 0.17/0.40 ( ( ( range_THFTYPE_IiioI @ REL @ CLASS1 )
% 0.17/0.40 & ( range_THFTYPE_IiioI @ REL @ CLASS2 ) )
% 0.17/0.40 => ( ( subclass_THFTYPE_IiioI @ CLASS1 @ CLASS2 )
% 0.17/0.40 | ( subclass_THFTYPE_IiioI @ CLASS2 @ CLASS1 ) ) ) ).
% 0.17/0.40
% 0.17/0.40 %KIF documentation:(documentation domain EnglishLanguage "Provides a computationally and heuristically convenient mechanism for declaring the argument types of a given relation. The formula (&%domain ?REL ?INT ?CLASS) means that the ?INT'th element of each tuple in the relation ?REL must be an instance of ?CLASS. Specifying argument types is very helpful in maintaining ontologies. Representation systems can use these specifications to classify terms and check integrity constraints. If the restriction on the argument type of a &%Relation is not captured by a &%SetOrClass already defined in the ontology, one can specify a &%SetOrClass compositionally with the functions &%UnionFn, &%IntersectionFn, etc.")
% 0.17/0.40 thf(ax_021,axiom,
% 0.17/0.40 likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_022,axiom,
% 0.17/0.40 likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 %KIF documentation:(documentation attribute EnglishLanguage "(&%attribute ?OBJECT ?PROPERTY) means that ?PROPERTY is a &%Attribute of ?OBJECT. For example, (&%attribute &%MyLittleRedWagon &%Red).")
% 0.17/0.40 %KIF documentation:(documentation Organism EnglishLanguage "Generally, a living individual, including all &%Plants and &%Animals.")
% 0.17/0.40 thf(ax_023,axiom,
% 0.17/0.40 ! [CLASS: $i,CHILD: $i,PARENT: $i] :
% 0.17/0.40 ( ( ( parent_THFTYPE_IiioI @ CHILD @ PARENT )
% 0.17/0.40 & ( subclass_THFTYPE_IiioI @ CLASS @ lOrganism_THFTYPE_i )
% 0.17/0.40 & ( instance_THFTYPE_IiioI @ PARENT @ CLASS ) )
% 0.17/0.40 => ( instance_THFTYPE_IiioI @ CHILD @ CLASS ) ) ).
% 0.17/0.40
% 0.17/0.40 %KIF documentation:(documentation BinaryPredicate EnglishLanguage "A &%Predicate relating two items - its valence is two.")
% 0.17/0.40 thf(ax_024,axiom,
% 0.17/0.40 ! [REL2: $i,CLASS1: $i,REL1: $i] :
% 0.17/0.40 ( ( ( subrelation_THFTYPE_IiioI @ REL1 @ REL2 )
% 0.17/0.40 & ( range_THFTYPE_IiioI @ REL2 @ CLASS1 ) )
% 0.17/0.40 => ( range_THFTYPE_IiioI @ REL1 @ CLASS1 ) ) ).
% 0.17/0.40
% 0.17/0.40 %KIF documentation:(documentation subclass EnglishLanguage "(&%subclass ?CLASS1 ?CLASS2) means that ?CLASS1 is a subclass of ?CLASS2, i.e. every instance of ?CLASS1 is also an instance of ?CLASS2. A class may have multiple superclasses and subclasses.")
% 0.17/0.40 thf(ax_025,axiom,
% 0.17/0.40 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ) ).
% 0.17/0.40
% 0.17/0.40 thf(ax_026,axiom,
% 0.17/0.40 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ) ).
% 0.17/0.40
% 0.17/0.40 %KIF documentation:(documentation documentation EnglishLanguage "A relation between objects in the domain of discourse and strings of natural language text stated in a particular &%HumanLanguage. The domain of &%documentation is not constants (names), but the objects themselves. This means that one does not quote the names when associating them with their documentation.")
% 0.17/0.40 thf(ax_027,axiom,
% 0.17/0.40 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_028,axiom,
% 0.17/0.40 ! [NUMBER: $i,CLASS1: $i,REL: $i,CLASS2: $i] :
% 0.17/0.40 ( ( ( domain_THFTYPE_IiiioI @ REL @ NUMBER @ CLASS1 )
% 0.17/0.40 & ( domain_THFTYPE_IiiioI @ REL @ NUMBER @ CLASS2 ) )
% 0.17/0.40 => ( ( subclass_THFTYPE_IiioI @ CLASS1 @ CLASS2 )
% 0.17/0.40 | ( subclass_THFTYPE_IiioI @ CLASS2 @ CLASS1 ) ) ) ).
% 0.17/0.40
% 0.17/0.40 thf(ax_029,axiom,
% 0.17/0.40 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_030,axiom,
% 0.17/0.40 ! [NUMBER: $i,PRED1: $i,CLASS1: $i,PRED2: $i] :
% 0.17/0.40 ( ( ( subrelation_THFTYPE_IiioI @ PRED1 @ PRED2 )
% 0.17/0.40 & ( domain_THFTYPE_IiiioI @ PRED2 @ NUMBER @ CLASS1 ) )
% 0.17/0.40 => ( domain_THFTYPE_IiiioI @ PRED1 @ NUMBER @ CLASS1 ) ) ).
% 0.17/0.40
% 0.17/0.40 %KIF documentation:(documentation parent EnglishLanguage "The general relationship of parenthood. (&%parent ?CHILD ?PARENT) means that ?PARENT is a biological parent of ?CHILD.")
% 0.17/0.40 thf(ax_031,axiom,
% 0.17/0.40 instance_THFTYPE_IIiioIioI @ parent_THFTYPE_IiioI @ lAsymmetricRelation_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_032,axiom,
% 0.17/0.40 instance_THFTYPE_IIiioIioI @ range_THFTYPE_IiioI @ lAsymmetricRelation_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_033,axiom,
% 0.17/0.40 instance_THFTYPE_IIiioIioI @ range_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_034,axiom,
% 0.17/0.40 instance_THFTYPE_IIiioIioI @ parent_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_035,axiom,
% 0.17/0.40 domain_THFTYPE_IIiioIiioI @ parent_THFTYPE_IiioI @ n1_THFTYPE_i @ lOrganism_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_036,axiom,
% 0.17/0.40 instance_THFTYPE_IIiooIioI @ holdsDuring_THFTYPE_IiooI @ lAsymmetricRelation_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_037,axiom,
% 0.17/0.40 domain_THFTYPE_IIiioIiioI @ parent_THFTYPE_IiioI @ n2_THFTYPE_i @ lOrganism_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_038,axiom,
% 0.17/0.40 instance_THFTYPE_IIiioIioI @ subrelation_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_039,axiom,
% 0.17/0.40 instance_THFTYPE_IiioI @ equal_THFTYPE_i @ lBinaryPredicate_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_040,axiom,
% 0.17/0.40 instance_THFTYPE_IIiioIioI @ subclass_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_041,axiom,
% 0.17/0.40 instance_THFTYPE_IiioI @ attribute_THFTYPE_i @ lAsymmetricRelation_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_042,axiom,
% 0.17/0.40 instance_THFTYPE_IIiioIioI @ instance_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 thf(ax_043,axiom,
% 0.17/0.40 instance_THFTYPE_IIiooIioI @ holdsDuring_THFTYPE_IiooI @ lBinaryPredicate_THFTYPE_i ).
% 0.17/0.40
% 0.17/0.40 %----The translated conjecture
% 0.17/0.40 thf(con,conjecture,
% 0.17/0.40 ? [R: $i > $i > $o,X: $i,Y: $i] :
% 0.17/0.40 ( ( R @ X @ lAnna_THFTYPE_i )
% 0.17/0.40 & ( (~) @ ( R @ Y @ lAnna_THFTYPE_i ) ) ) ).
% 0.17/0.40
% 0.17/0.40 %------------------------------------------------------------------------------
% 0.17/0.40 ------------------------
% 1.85/1.44 ---- Embedded in THF ---
% 1.85/1.44 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.85/1.44 %%% Generated on Tue Feb 24 05:50:04 EST 2026
% 1.85/1.44 %%% using '$$dhol' embedding, version 1.3.0.
% 1.85/1.44 %%% Logic specification used:
% 1.85/1.44 %%% thf(spec, logic, $$dhol).
% 1.85/1.44
% 1.85/1.44 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.00Y5TSrdar/DTF2DTF24285.p
% See solution above
% 1.85/1.44 ------------------------
% 1.85/1.45 ---- Cleaned THF ---
% 1.85/1.45 thf(numbers,type,
% 1.85/1.45 num: $tType ).
% 1.85/1.45
% 1.85/1.45 thf(attribute_THFTYPE_i,type,
% 1.85/1.45 attribute_THFTYPE_i: $i ).
% 1.85/1.45
% 1.85/1.45 thf(domain_THFTYPE_IIiioIiioI,type,
% 1.85/1.45 domain_THFTYPE_IIiioIiioI: ( $i > $i > $o ) > $i > $i > $o ).
% 1.85/1.45
% 1.85/1.45 thf(domain_THFTYPE_IiiioI,type,
% 1.85/1.45 domain_THFTYPE_IiiioI: $i > $i > $i > $o ).
% 1.85/1.45
% 1.85/1.45 thf(equal_THFTYPE_i,type,
% 1.85/1.45 equal_THFTYPE_i: $i ).
% 1.85/1.45
% 1.85/1.45 thf(holdsDuring_THFTYPE_IiooI,type,
% 1.85/1.45 holdsDuring_THFTYPE_IiooI: $i > $o > $o ).
% 1.85/1.45
% 1.85/1.45 thf(instance_THFTYPE_IIiioIioI,type,
% 1.85/1.45 instance_THFTYPE_IIiioIioI: ( $i > $i > $o ) > $i > $o ).
% 1.85/1.45
% 1.85/1.45 thf(instance_THFTYPE_IIiooIioI,type,
% 1.85/1.45 instance_THFTYPE_IIiooIioI: ( $i > $o > $o ) > $i > $o ).
% 1.85/1.45
% 1.85/1.45 thf(instance_THFTYPE_IiioI,type,
% 1.85/1.45 instance_THFTYPE_IiioI: $i > $i > $o ).
% 1.85/1.45
% 1.85/1.45 thf(lAnna_THFTYPE_i,type,
% 1.85/1.45 lAnna_THFTYPE_i: $i ).
% 1.85/1.45
% 1.85/1.45 thf(lAsymmetricRelation_THFTYPE_i,type,
% 1.85/1.45 lAsymmetricRelation_THFTYPE_i: $i ).
% 1.85/1.45
% 1.85/1.45 thf(lBen_THFTYPE_i,type,
% 1.85/1.45 lBen_THFTYPE_i: $i ).
% 1.85/1.45
% 1.85/1.45 thf(lBill_THFTYPE_i,type,
% 1.85/1.45 lBill_THFTYPE_i: $i ).
% 1.85/1.45
% 1.85/1.45 thf(lBinaryPredicate_THFTYPE_i,type,
% 1.85/1.45 lBinaryPredicate_THFTYPE_i: $i ).
% 1.85/1.45
% 1.85/1.45 thf(lBob_THFTYPE_i,type,
% 1.85/1.45 lBob_THFTYPE_i: $i ).
% 1.85/1.45
% 1.85/1.45 thf(lMary_THFTYPE_i,type,
% 1.85/1.45 lMary_THFTYPE_i: $i ).
% 1.85/1.45
% 1.85/1.45 thf(lOrganism_THFTYPE_i,type,
% 1.85/1.45 lOrganism_THFTYPE_i: $i ).
% 1.85/1.45
% 1.85/1.45 thf(lSue_THFTYPE_i,type,
% 1.85/1.45 lSue_THFTYPE_i: $i ).
% 1.85/1.45
% 1.85/1.45 thf(likes_THFTYPE_IiioI,type,
% 1.85/1.45 likes_THFTYPE_IiioI: $i > $i > $o ).
% 1.85/1.45
% 1.85/1.45 thf(n1_THFTYPE_i,type,
% 1.85/1.45 n1_THFTYPE_i: $i ).
% 1.85/1.45
% 1.85/1.45 thf(n2_THFTYPE_i,type,
% 1.85/1.45 n2_THFTYPE_i: $i ).
% 1.85/1.45
% 1.85/1.45 thf(parent_THFTYPE_IiioI,type,
% 1.85/1.45 parent_THFTYPE_IiioI: $i > $i > $o ).
% 1.85/1.45
% 1.85/1.45 thf(range_THFTYPE_IiioI,type,
% 1.85/1.45 range_THFTYPE_IiioI: $i > $i > $o ).
% 1.85/1.45
% 1.85/1.45 thf(subclass_THFTYPE_IiioI,type,
% 1.85/1.45 subclass_THFTYPE_IiioI: $i > $i > $o ).
% 1.85/1.45
% 1.85/1.45 thf(subrelation_THFTYPE_IIioIIioIoI,type,
% 1.85/1.45 subrelation_THFTYPE_IIioIIioIoI: ( $i > $o ) > ( $i > $o ) > $o ).
% 1.85/1.45
% 1.85/1.45 thf(subrelation_THFTYPE_IiioI,type,
% 1.85/1.45 subrelation_THFTYPE_IiioI: $i > $i > $o ).
% 1.85/1.45
% 1.85/1.45 thf(ax,axiom,
% 1.85/1.45 likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_001,axiom,
% 1.85/1.45 likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_002,axiom,
% 1.85/1.45 (~) @ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_003,axiom,
% 1.85/1.45 (~) @ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_004,axiom,
% 1.85/1.45 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_005,axiom,
% 1.85/1.45 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_006,axiom,
% 1.85/1.45 ! [X: $i,Y: $i,Z: $i] :
% 1.85/1.45 ( ( ( subclass_THFTYPE_IiioI @ X @ Y )
% 1.85/1.45 & ( instance_THFTYPE_IiioI @ Z @ X ) )
% 1.85/1.45 => ( instance_THFTYPE_IiioI @ Z @ Y ) ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_007,axiom,
% 1.85/1.45 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_008,axiom,
% 1.85/1.45 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_009,axiom,
% 1.85/1.45 ! [CLASS1: $i,CLASS2: $i] :
% 1.85/1.45 ( ( CLASS1 = CLASS2 )
% 1.85/1.45 => ! [THING: $i] :
% 1.85/1.45 ( ( instance_THFTYPE_IiioI @ THING @ CLASS1 )
% 1.85/1.45 <=> ( instance_THFTYPE_IiioI @ THING @ CLASS2 ) ) ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_010,axiom,
% 1.85/1.45 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBen_THFTYPE_i ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_011,axiom,
% 1.85/1.45 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBen_THFTYPE_i ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_012,axiom,
% 1.85/1.45 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_013,axiom,
% 1.85/1.45 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_014,axiom,
% 1.85/1.45 ! [REL2: $i > $o,ROW: $i,REL1: $i > $o] :
% 1.85/1.45 ( ( ( subrelation_THFTYPE_IIioIIioIoI @ REL1 @ REL2 )
% 1.85/1.45 & ( REL1 @ ROW ) )
% 1.85/1.45 => ( REL2 @ ROW ) ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_015,axiom,
% 1.85/1.45 ! [ORGANISM: $i] :
% 1.85/1.45 ( ( instance_THFTYPE_IiioI @ ORGANISM @ lOrganism_THFTYPE_i )
% 1.85/1.45 => ? [PARENT: $i] : ( parent_THFTYPE_IiioI @ ORGANISM @ PARENT ) ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_016,axiom,
% 1.85/1.45 ! [TIME: $i,SITUATION: $o] :
% 1.85/1.45 ( ( holdsDuring_THFTYPE_IiooI @ TIME @ ( (~) @ SITUATION ) )
% 1.85/1.45 => ( (~) @ ( holdsDuring_THFTYPE_IiooI @ TIME @ SITUATION ) ) ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_017,axiom,
% 1.85/1.45 likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_018,axiom,
% 1.85/1.45 likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_019,axiom,
% 1.85/1.45 ! [THING2: $i,THING1: $i] :
% 1.85/1.45 ( ( THING1 = THING2 )
% 1.85/1.45 => ! [CLASS: $i] :
% 1.85/1.45 ( ( instance_THFTYPE_IiioI @ THING1 @ CLASS )
% 1.85/1.45 <=> ( instance_THFTYPE_IiioI @ THING2 @ CLASS ) ) ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_020,axiom,
% 1.85/1.45 ! [CLASS1: $i,REL: $i,CLASS2: $i] :
% 1.85/1.45 ( ( ( range_THFTYPE_IiioI @ REL @ CLASS1 )
% 1.85/1.45 & ( range_THFTYPE_IiioI @ REL @ CLASS2 ) )
% 1.85/1.45 => ( ( subclass_THFTYPE_IiioI @ CLASS1 @ CLASS2 )
% 1.85/1.45 | ( subclass_THFTYPE_IiioI @ CLASS2 @ CLASS1 ) ) ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_021,axiom,
% 1.85/1.45 likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_022,axiom,
% 1.85/1.45 likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_023,axiom,
% 1.85/1.45 ! [CLASS: $i,CHILD: $i,PARENT: $i] :
% 1.85/1.45 ( ( ( parent_THFTYPE_IiioI @ CHILD @ PARENT )
% 1.85/1.45 & ( subclass_THFTYPE_IiioI @ CLASS @ lOrganism_THFTYPE_i )
% 1.85/1.45 & ( instance_THFTYPE_IiioI @ PARENT @ CLASS ) )
% 1.85/1.45 => ( instance_THFTYPE_IiioI @ CHILD @ CLASS ) ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_024,axiom,
% 1.85/1.45 ! [REL2: $i,CLASS1: $i,REL1: $i] :
% 1.85/1.45 ( ( ( subrelation_THFTYPE_IiioI @ REL1 @ REL2 )
% 1.85/1.45 & ( range_THFTYPE_IiioI @ REL2 @ CLASS1 ) )
% 1.85/1.45 => ( range_THFTYPE_IiioI @ REL1 @ CLASS1 ) ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_025,axiom,
% 1.85/1.45 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_026,axiom,
% 1.85/1.45 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_027,axiom,
% 1.85/1.45 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_028,axiom,
% 1.85/1.45 ! [NUMBER: $i,CLASS1: $i,REL: $i,CLASS2: $i] :
% 1.85/1.45 ( ( ( domain_THFTYPE_IiiioI @ REL @ NUMBER @ CLASS1 )
% 1.85/1.45 & ( domain_THFTYPE_IiiioI @ REL @ NUMBER @ CLASS2 ) )
% 1.85/1.45 => ( ( subclass_THFTYPE_IiioI @ CLASS1 @ CLASS2 )
% 1.85/1.45 | ( subclass_THFTYPE_IiioI @ CLASS2 @ CLASS1 ) ) ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_029,axiom,
% 1.85/1.45 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_030,axiom,
% 1.85/1.45 ! [NUMBER: $i,PRED1: $i,CLASS1: $i,PRED2: $i] :
% 1.85/1.45 ( ( ( subrelation_THFTYPE_IiioI @ PRED1 @ PRED2 )
% 1.85/1.45 & ( domain_THFTYPE_IiiioI @ PRED2 @ NUMBER @ CLASS1 ) )
% 1.85/1.45 => ( domain_THFTYPE_IiiioI @ PRED1 @ NUMBER @ CLASS1 ) ) ).
% 1.85/1.45
% 1.85/1.45 thf(ax_031,axiom,
% 1.85/1.45 instance_THFTYPE_IIiioIioI @ parent_THFTYPE_IiioI @ lAsymmetricRelation_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_032,axiom,
% 1.85/1.45 instance_THFTYPE_IIiioIioI @ range_THFTYPE_IiioI @ lAsymmetricRelation_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_033,axiom,
% 1.85/1.45 instance_THFTYPE_IIiioIioI @ range_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_034,axiom,
% 1.85/1.45 instance_THFTYPE_IIiioIioI @ parent_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_035,axiom,
% 1.85/1.45 domain_THFTYPE_IIiioIiioI @ parent_THFTYPE_IiioI @ n1_THFTYPE_i @ lOrganism_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_036,axiom,
% 1.85/1.45 instance_THFTYPE_IIiooIioI @ holdsDuring_THFTYPE_IiooI @ lAsymmetricRelation_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_037,axiom,
% 1.85/1.45 domain_THFTYPE_IIiioIiioI @ parent_THFTYPE_IiioI @ n2_THFTYPE_i @ lOrganism_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_038,axiom,
% 1.85/1.45 instance_THFTYPE_IIiioIioI @ subrelation_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_039,axiom,
% 1.85/1.45 instance_THFTYPE_IiioI @ equal_THFTYPE_i @ lBinaryPredicate_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_040,axiom,
% 1.85/1.45 instance_THFTYPE_IIiioIioI @ subclass_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_041,axiom,
% 1.85/1.45 instance_THFTYPE_IiioI @ attribute_THFTYPE_i @ lAsymmetricRelation_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_042,axiom,
% 1.85/1.45 instance_THFTYPE_IIiioIioI @ instance_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(ax_043,axiom,
% 1.85/1.45 instance_THFTYPE_IIiooIioI @ holdsDuring_THFTYPE_IiooI @ lBinaryPredicate_THFTYPE_i ).
% 1.85/1.45
% 1.85/1.45 thf(con,conjecture,
% 1.85/1.45 ? [R: $i > $i > $o,X: $i,Y: $i] :
% 1.85/1.45 ( ( R @ X @ lAnna_THFTYPE_i )
% 1.85/1.45 & ( (~) @ ( R @ Y @ lAnna_THFTYPE_i ) ) ) ).
% 1.85/1.45 ------------------------
% 1.85/1.47 % (24385)dis+1010_1:1_au=on:cbe=off:chr=on:fsr=off:hfsq=on:nm=64:sos=theory:sp=weighted_frequency:i=27:si=on:rtra=on_0 on DTF2THF_24285 for (2999ds/27Mi)
% 1.85/1.47 % (24383)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_24285 for (2999ds/183Mi)
% 1.85/1.47 % (24386)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_24285 for (2999ds/2Mi)
% 1.85/1.47 % (24389)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_24285 for (2999ds/18Mi)
% 1.85/1.47 % (24388)lrs+1002_1:1_au=on:bd=off:e2e=on:sd=2:sos=on:ss=axioms:i=275:si=on:rtra=on_0 on DTF2THF_24285 for (2999ds/275Mi)
% 1.85/1.47 % (24384)lrs+10_1:1_c=on:cnfonf=conj_eager:fd=off:fe=off:kws=frequency:spb=intro:i=4:si=on:rtra=on_0 on DTF2THF_24285 for (2999ds/4Mi)
% 1.85/1.47 % (24387)lrs+1002_1:128_aac=none:au=on:cnfonf=lazy_not_gen_be_off:sos=all:i=2:si=on:rtra=on_0 on DTF2THF_24285 for (2999ds/2Mi)
% 1.85/1.47 % (24386)Instruction limit reached!
% 1.85/1.47 % (24386)------------------------------
% 1.85/1.47 % (24386)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.85/1.47 % (24386)Termination reason: Unknown
% 1.85/1.47 % (24386)Termination phase: Property scanning
% 1.85/1.48
% 1.85/1.48 % (24387)Instruction limit reached!
% 1.85/1.48 % (24387)------------------------------
% 1.85/1.48 % (24387)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.85/1.48 % (24386)Memory used [KB]: 1023
% 1.85/1.48 % (24386)Time elapsed: 0.003 s
% 1.85/1.48 % (24386)Instructions burned: 3 (million)
% 1.85/1.48 % (24386)------------------------------
% 1.85/1.48 % (24386)------------------------------
% 1.85/1.48 % (24387)Termination reason: Unknown
% 1.85/1.48 % (24387)Termination phase: shuffling
% 1.85/1.48
% 1.85/1.48 % (24387)Memory used [KB]: 1023
% 1.85/1.48 % (24387)Time elapsed: 0.003 s
% 1.85/1.48 % (24387)Instructions burned: 3 (million)
% 1.85/1.48 % (24387)------------------------------
% 1.85/1.48 % (24387)------------------------------
% 1.85/1.48 % (24384)Instruction limit reached!
% 1.85/1.48 % (24384)------------------------------
% 1.85/1.48 % (24384)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.85/1.48 % (24384)Termination reason: Unknown
% 1.85/1.48 % (24384)Termination phase: Property scanning
% 1.85/1.48
% 1.85/1.48 % (24384)Memory used [KB]: 1023
% 1.85/1.48 % (24384)Time elapsed: 0.004 s
% 1.85/1.48 % (24384)Instructions burned: 5 (million)
% 1.85/1.48 % (24384)------------------------------
% 1.85/1.48 % (24384)------------------------------
% 1.85/1.48 % (24385)First to succeed.
% 1.85/1.48 % (24385)Refutation found. Thanks to Tanya!
% 1.85/1.48 % SZS status Theorem for DTF2THF_24285
% 1.85/1.48 % SZS output start Proof for DTF2THF_24285
% 1.85/1.48 thf(func_def_0, type, num: $tType).
% 1.85/1.48 thf(func_def_2, type, domain_THFTYPE_IIiioIiioI: ($i > $i > $o) > $i > $i > $o).
% 1.85/1.48 thf(func_def_3, type, domain_THFTYPE_IiiioI: $i > $i > $i > $o).
% 1.85/1.48 thf(func_def_5, type, holdsDuring_THFTYPE_IiooI: $i > $o > $o).
% 1.85/1.48 thf(func_def_6, type, instance_THFTYPE_IIiioIioI: ($i > $i > $o) > $i > $o).
% 1.85/1.48 thf(func_def_7, type, instance_THFTYPE_IIiooIioI: ($i > $o > $o) > $i > $o).
% 1.85/1.48 thf(func_def_8, type, instance_THFTYPE_IiioI: $i > $i > $o).
% 1.85/1.48 thf(func_def_18, type, likes_THFTYPE_IiioI: $i > $i > $o).
% 1.85/1.48 thf(func_def_21, type, parent_THFTYPE_IiioI: $i > $i > $o).
% 1.85/1.48 thf(func_def_22, type, range_THFTYPE_IiioI: $i > $i > $o).
% 1.85/1.48 thf(func_def_23, type, subclass_THFTYPE_IiioI: $i > $i > $o).
% 1.85/1.48 thf(func_def_24, type, subrelation_THFTYPE_IIioIIioIoI: ($i > $o) > ($i > $o) > $o).
% 1.85/1.48 thf(func_def_25, type, subrelation_THFTYPE_IiioI: $i > $i > $o).
% 1.85/1.48 thf(func_def_28, type, vEPSILON: !>[X0: $tType]:((X0 > $o) > X0)).
% 1.85/1.48 thf(func_def_31, type, sK0: $i > $i).
% 1.85/1.48 thf(func_def_33, type, ph2: !>[X0: $tType]:(X0)).
% 1.85/1.48 thf(f230,plain,(
% 1.85/1.48 $false),
% 1.85/1.48 inference(trivial_inequality_removal,[status(thm)],[f227])).
% 1.85/1.48 thf(f227,plain,(
% 1.85/1.48 ($false = $true)),
% 1.85/1.48 inference(superposition,[status(thm)],[f225,f215])).
% 1.85/1.48 thf(f215,plain,(
% 1.85/1.48 ((parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i) = $false)),
% 1.85/1.48 inference(not_proxy_clausification,[status(thm)],[f177])).
% 1.85/1.48 thf(f177,plain,(
% 1.85/1.48 ((~ (parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)) = $true)),
% 1.85/1.48 inference(cnf_transformation,[status(thm)],[f123])).
% 1.85/1.48 thf(f123,plain,(
% 1.85/1.48 ((~ (parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)) = $true)),
% 1.85/1.48 inference(fool_elimination,[status(thm)],[f122])).
% 1.85/1.48 thf(f122,plain,(
% 1.85/1.48 (~ (parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i))),
% 1.85/1.48 inference(rectify,[status(thm)],[f26])).
% 1.85/1.48 thf(f26,axiom,(
% 1.85/1.48 (~ (parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i))),
% 1.85/1.48 file('/export/starexec/sandbox/tmp/tmp.00Y5TSrdar/DTF2THF_24285.p',ax_025)).
% 1.85/1.48 thf(f225,plain,(
% 1.85/1.48 ( ! [X0 : $i] : (($true = (parent_THFTYPE_IiioI @ X0 @ lAnna_THFTYPE_i))) )),
% 1.85/1.48 inference(trivial_inequality_removal,[status(thm)],[f222])).
% 1.85/1.48 thf(f222,plain,(
% 1.85/1.48 ( ! [X0 : $i] : (($true != $true) | ($true = (parent_THFTYPE_IiioI @ X0 @ lAnna_THFTYPE_i))) )),
% 1.85/1.48 inference(superposition,[status(thm)],[f221,f178])).
% 1.85/1.48 thf(f178,plain,(
% 1.85/1.48 ((parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i) = $true)),
% 1.85/1.48 inference(cnf_transformation,[status(thm)],[f135])).
% 1.85/1.48 thf(f135,plain,(
% 1.85/1.48 ((parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i) = $true)),
% 1.85/1.48 inference(fool_elimination,[status(thm)],[f134])).
% 1.85/1.48 thf(f134,plain,(
% 1.85/1.48 (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i)),
% 1.85/1.48 inference(rectify,[status(thm)],[f14])).
% 1.85/1.48 thf(f14,axiom,(
% 1.85/1.48 (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i)),
% 1.85/1.48 file('/export/starexec/sandbox/tmp/tmp.00Y5TSrdar/DTF2THF_24285.p',ax_013)).
% 1.85/1.48 thf(f221,plain,(
% 1.85/1.48 ( ! [X2 : $i,X0 : $i > $i > $o,X1 : $i] : (((X0 @ X2 @ lAnna_THFTYPE_i) != $true) | ($true = (X0 @ X1 @ lAnna_THFTYPE_i))) )),
% 1.85/1.48 inference(not_proxy_clausification,[status(thm)],[f210])).
% 1.85/1.48 thf(f210,plain,(
% 1.85/1.48 ( ! [X2 : $i,X0 : $i > $i > $o,X1 : $i] : (((~ (X0 @ X1 @ lAnna_THFTYPE_i)) != $true) | ((X0 @ X2 @ lAnna_THFTYPE_i) != $true)) )),
% 1.85/1.48 inference(cnf_transformation,[status(thm)],[f166])).
% 1.85/1.48 thf(f166,plain,(
% 1.85/1.48 ! [X0 : $i > $i > $o,X1 : $i,X2 : $i] : (((X0 @ X2 @ lAnna_THFTYPE_i) != $true) | ((~ (X0 @ X1 @ lAnna_THFTYPE_i)) != $true))),
% 1.85/1.48 inference(rectify,[status(thm)],[f148])).
% 1.85/1.48 thf(f148,plain,(
% 1.85/1.48 ! [X1 : $i > $i > $o,X2 : $i,X0 : $i] : (($true != (X1 @ X0 @ lAnna_THFTYPE_i)) | ($true != (~ (X1 @ X2 @ lAnna_THFTYPE_i))))),
% 1.85/1.48 inference(ennf_transformation,[status(thm)],[f75])).
% 1.85/1.48 thf(f75,plain,(
% 1.85/1.48 ~? [X0 : $i,X1 : $i > $i > $o,X2 : $i] : (($true = (X1 @ X0 @ lAnna_THFTYPE_i)) & ($true = (~ (X1 @ X2 @ lAnna_THFTYPE_i))))),
% 1.85/1.48 inference(fool_elimination,[status(thm)],[f74])).
% 1.85/1.48 thf(f74,plain,(
% 1.85/1.48 ~? [X0 : $i,X1 : $i > $i > $o,X2 : $i] : ((X1 @ X0 @ lAnna_THFTYPE_i) & (~ (X1 @ X2 @ lAnna_THFTYPE_i)))),
% 1.85/1.48 inference(rectify,[status(thm)],[f46])).
% 1.85/1.48 thf(f46,negated_conjecture,(
% 1.85/1.48 ~? [X0 : $i,X21 : $i > $i > $o,X1 : $i] : ((X21 @ X0 @ lAnna_THFTYPE_i) & (~ (X21 @ X1 @ lAnna_THFTYPE_i)))),
% 1.85/1.48 inference(negated_conjecture,[status(cth)],[f45])).
% 1.85/1.48 thf(f45,conjecture,(
% 1.85/1.48 ? [X0 : $i,X21 : $i > $i > $o,X1 : $i] : ((X21 @ X0 @ lAnna_THFTYPE_i) & (~ (X21 @ X1 @ lAnna_THFTYPE_i)))),
% 1.85/1.48 file('/export/starexec/sandbox/tmp/tmp.00Y5TSrdar/DTF2THF_24285.p',con)).
% 1.85/1.48 % SZS output end Proof for DTF2THF_24285
% 1.85/1.48 % (24385)------------------------------
% 1.85/1.48 % (24385)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.85/1.48 % (24385)Termination reason: Refutation
% 1.85/1.48
% 1.85/1.48 % (24385)Memory used [KB]: 5628
% 1.85/1.48 % (24385)Time elapsed: 0.009 s
% 1.85/1.48 % (24385)Instructions burned: 13 (million)
% 1.85/1.48 % (24385)------------------------------
% 1.85/1.48 % (24385)------------------------------
% 1.85/1.48 % (24382)Success in time 0.025 s
%------------------------------------------------------------------------------