%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : CSR137^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 : n028.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:06 AM UTC 2026
% Result : Theorem 1.80s 1.38s
% Output : Refutation 1.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 9
% Syntax : Number of formulae : 72 ( 7 unt; 0 typ; 6 def)
% Number of atoms : 490 ( 170 equ; 0 cnn)
% Maximal formula atoms : 4 ( 6 avg)
% Number of connectives : 623 ( 153 ~; 130 |; 12 &; 288 @)
% ( 6 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 7 avg)
% Number of types : 3 ( 1 usr)
% Number of type conns : 94 ( 94 >; 0 *; 0 +; 0 <<)
% Number of symbols : 27 ( 23 usr; 13 con; 0-3 aty)
% ( 34 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 247 ( 44 ^; 191 !; 12 ?; 247 :)
% 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_35,type,
ph1:
!>[X0: $tType] : X0 ).
thf(f297,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[f192,f199,f228,f232,f234,f294,f296]) ).
thf(f296,plain,
( ~ spl0_5
| ~ spl0_6 ),
inference(avatar_contradiction_clause,[status(thm)],[f295]) ).
thf(f295,plain,
( $false
| ~ spl0_5
| ~ spl0_6 ),
inference(subsumption_resolution,[status(thm)],[f227,f231]) ).
thf(f231,plain,
( ! [X0: $i] : ( lAnna_THFTYPE_i = X0 )
| ~ spl0_6 ),
inference(avatar_component_clause,[status(thm)],[f230]) ).
thf(f230,definition,
( spl0_6
<=> ! [X0: $i] : ( lAnna_THFTYPE_i = X0 ) ),
introduced(definition,[new_symbols(naming,[spl0_6])],[avatar_definition]) ).
thf(f227,plain,
( ! [X0: $i] : ( lAnna_THFTYPE_i != X0 )
| ~ spl0_5 ),
inference(avatar_component_clause,[status(thm)],[f226]) ).
thf(f226,definition,
( spl0_5
<=> ! [X0: $i] : ( lAnna_THFTYPE_i != X0 ) ),
introduced(definition,[new_symbols(naming,[spl0_5])],[avatar_definition]) ).
thf(f294,plain,
~ spl0_4,
inference(avatar_contradiction_clause,[status(thm)],[f293]) ).
thf(f293,plain,
( $false
| ~ spl0_4 ),
inference(trivial_inequality_removal,[status(thm)],[f292]) ).
thf(f292,plain,
( ( $false = $true )
| ~ spl0_4 ),
inference(forward_demodulation,[status(thm)],[f240,f282]) ).
thf(f282,plain,
( ! [X0: $i] :
( $false
= ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0 ) )
| ~ spl0_4 ),
inference(not_proxy_clausification,[status(thm)],[f265]) ).
thf(f265,plain,
( ! [X0: $i] :
( ( ~ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0 ) )
= $true )
| ~ spl0_4 ),
inference(superposition,[status(thm)],[f140,f198]) ).
thf(f198,plain,
( ! [X6: $i,X5: $i] : ( X5 = X6 )
| ~ spl0_4 ),
inference(avatar_component_clause,[status(thm)],[f197]) ).
thf(f197,definition,
( spl0_4
<=> ! [X6: $i,X5: $i] : ( X5 = X6 ) ),
introduced(definition,[new_symbols(naming,[spl0_4])],[avatar_definition]) ).
thf(f140,plain,
( ( ~ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f125]) ).
thf(f125,plain,
( ( ~ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i ) )
= $true ),
inference(fool_elimination,[status(thm)],[f124]) ).
thf(f124,plain,
~ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i ),
inference(rectify,[status(thm)],[f3]) ).
thf(f3,axiom,
~ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i ),
file('/export/starexec/sandbox/tmp/tmp.JfLqaL197y/DTF2THF_16718.p',ax_002) ).
thf(f240,plain,
( ! [X0: $i] :
( ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0 )
= $true )
| ~ spl0_4 ),
inference(superposition,[status(thm)],[f144,f198]) ).
thf(f144,plain,
( ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i )
= $true ),
inference(cnf_transformation,[status(thm)],[f99]) ).
thf(f99,plain,
( ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i )
= $true ),
inference(fool_elimination,[status(thm)],[f98]) ).
thf(f98,plain,
likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i,
inference(rectify,[status(thm)],[f1]) ).
thf(f1,axiom,
likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i,
file('/export/starexec/sandbox/tmp/tmp.JfLqaL197y/DTF2THF_16718.p',ax) ).
thf(f234,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[status(thm)],[f233]) ).
thf(f233,plain,
( $false
| ~ spl0_1 ),
inference(flex-flex_simplify,[status(thm)],[f188]) ).
thf(f188,plain,
( ! [X6: $i,X5: $i] : ( X5 != X6 )
| ~ spl0_1 ),
inference(avatar_component_clause,[status(thm)],[f187]) ).
thf(f187,definition,
( spl0_1
<=> ! [X6: $i,X5: $i] : ( X5 != X6 ) ),
introduced(definition,[new_symbols(naming,[spl0_1])],[avatar_definition]) ).
thf(f232,plain,
( spl0_1
| spl0_6
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[status(thm)],[f216,f194,f190,f230,f187]) ).
thf(f190,definition,
( spl0_2
<=> ! [X4: $i,X0: $i,X3: $i,X1: $i > $i > $o] :
( ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( lBill_THFTYPE_i = X0 )
| ( ( X1 @ X4 @ X3 )
= $true ) ) ),
introduced(definition,[new_symbols(naming,[spl0_2])],[avatar_definition]) ).
thf(f194,definition,
( spl0_3
<=> ! [X4: $i,X0: $i,X3: $i,X1: $i > $i > $o] :
( ( ( X1 @ X4 @ X3 )
= $true )
| ( lBill_THFTYPE_i != X0 )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true ) ) ),
introduced(definition,[new_symbols(naming,[spl0_3])],[avatar_definition]) ).
thf(f216,plain,
( ! [X3: $i,X0: $i,X4: $i] :
( ( lAnna_THFTYPE_i = X0 )
| ( X3 != X4 ) )
| ~ spl0_2
| ~ spl0_3 ),
inference(equality_proxy_clausification,[status(thm)],[f215]) ).
thf(f215,plain,
( ! [X3: $i,X0: $i,X4: $i] :
( ( ( X3 = X4 )
= $false )
| ( lAnna_THFTYPE_i = X0 ) )
| ~ spl0_2
| ~ spl0_3 ),
inference(equality_proxy_clausification,[status(thm)],[f214]) ).
thf(f214,plain,
( ! [X3: $i,X0: $i,X4: $i] :
( ( ( lAnna_THFTYPE_i = X0 )
= $true )
| ( ( X3 = X4 )
= $false ) )
| ~ spl0_2
| ~ spl0_3 ),
inference(not_proxy_clausification,[status(thm)],[f213]) ).
thf(f213,plain,
( ! [X3: $i,X0: $i,X4: $i] :
( ( ( X3 != X4 )
= $true )
| ( ( lAnna_THFTYPE_i = X0 )
= $true ) )
| ~ spl0_2
| ~ spl0_3 ),
inference(not_proxy_clausification,[status(thm)],[f212]) ).
thf(f212,plain,
( ! [X3: $i,X0: $i,X4: $i] :
( ( ( lAnna_THFTYPE_i != X0 )
!= $true )
| ( ( X3 != X4 )
= $true ) )
| ~ spl0_2
| ~ spl0_3 ),
inference(beta_eta_normalization,[status(thm)],[f202]) ).
thf(f202,plain,
( ! [X3: $i,X0: $i,X4: $i] :
( ( ( ^ [Y0: $i,Y1: $i] : ( Y1 != Y0 )
@ X0
@ lAnna_THFTYPE_i )
!= $true )
| ( ( ^ [Y0: $i,Y1: $i] : ( Y1 != Y0 )
@ X4
@ X3 )
= $true ) )
| ~ spl0_2
| ~ spl0_3 ),
inference(primitive_instantiation,[status(thm)],[f200]) ).
thf(f200,plain,
( ! [X3: $i,X0: $i,X1: $i > $i > $o,X4: $i] :
( ( ( X1 @ X4 @ X3 )
= $true )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true ) )
| ~ spl0_2
| ~ spl0_3 ),
inference(subsumption_resolution,[status(thm)],[f191,f195]) ).
thf(f195,plain,
( ! [X3: $i,X0: $i,X1: $i > $i > $o,X4: $i] :
( ( ( X1 @ X4 @ X3 )
= $true )
| ( lBill_THFTYPE_i != X0 )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true ) )
| ~ spl0_3 ),
inference(avatar_component_clause,[status(thm)],[f194]) ).
thf(f191,plain,
( ! [X3: $i,X0: $i,X1: $i > $i > $o,X4: $i] :
( ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( ( X1 @ X4 @ X3 )
= $true )
| ( lBill_THFTYPE_i = X0 ) )
| ~ spl0_2 ),
inference(avatar_component_clause,[status(thm)],[f190]) ).
thf(f228,plain,
( spl0_4
| spl0_5
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[status(thm)],[f223,f194,f190,f226,f197]) ).
thf(f223,plain,
( ! [X3: $i,X0: $i,X4: $i] :
( ( lAnna_THFTYPE_i != X0 )
| ( X3 = X4 ) )
| ~ spl0_2
| ~ spl0_3 ),
inference(equality_proxy_clausification,[status(thm)],[f222]) ).
thf(f222,plain,
( ! [X3: $i,X0: $i,X4: $i] :
( ( ( X3 = X4 )
= $true )
| ( lAnna_THFTYPE_i != X0 ) )
| ~ spl0_2
| ~ spl0_3 ),
inference(equality_proxy_clausification,[status(thm)],[f221]) ).
thf(f221,plain,
( ! [X3: $i,X0: $i,X4: $i] :
( ( ( lAnna_THFTYPE_i = X0 )
!= $true )
| ( ( X3 = X4 )
= $true ) )
| ~ spl0_2
| ~ spl0_3 ),
inference(beta_eta_normalization,[status(thm)],[f201]) ).
thf(f201,plain,
( ! [X3: $i,X0: $i,X4: $i] :
( ( ( ^ [Y0: $i,Y1: $i] : ( Y1 = Y0 )
@ X4
@ X3 )
= $true )
| ( ( ^ [Y0: $i,Y1: $i] : ( Y1 = Y0 )
@ X0
@ lAnna_THFTYPE_i )
!= $true ) )
| ~ spl0_2
| ~ spl0_3 ),
inference(primitive_instantiation,[status(thm)],[f200]) ).
thf(f199,plain,
( spl0_3
| spl0_4 ),
inference(avatar_split_clause,[status(thm)],[f171,f197,f194]) ).
thf(f171,plain,
! [X3: $i,X0: $i,X1: $i > $i > $o,X6: $i,X4: $i,X5: $i] :
( ( ( X1 @ X4 @ X3 )
= $true )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( lBill_THFTYPE_i != X0 )
| ( X5 = X6 ) ),
inference(equality_proxy_clausification,[status(thm)],[f170]) ).
thf(f170,plain,
! [X3: $i,X0: $i,X1: $i > $i > $o,X6: $i,X4: $i,X5: $i] :
( ( ( X1 @ X4 @ X3 )
= $true )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( lBill_THFTYPE_i != X0 )
| ( $true
= ( X6 = X5 ) ) ),
inference(equality_proxy_clausification,[status(thm)],[f169]) ).
thf(f169,plain,
! [X3: $i,X0: $i,X1: $i > $i > $o,X6: $i,X4: $i,X5: $i] :
( ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( ( lBill_THFTYPE_i = X0 )
!= $true )
| ( $true
= ( X6 = X5 ) )
| ( ( X1 @ X4 @ X3 )
= $true ) ),
inference(beta_eta_normalization,[status(thm)],[f160]) ).
thf(f160,plain,
! [X3: $i,X0: $i,X1: $i > $i > $o,X6: $i,X4: $i,X5: $i] :
( ( ( ^ [Y0: $i,Y1: $i] : ( Y1 = Y0 )
@ X0
@ lBill_THFTYPE_i )
!= $true )
| ( ( X1 @ X4 @ X3 )
= $true )
| ( ( ^ [Y0: $i,Y1: $i] : ( Y1 = Y0 )
@ X5
@ X6 )
= $true )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true ) ),
inference(primitive_instantiation,[status(thm)],[f159]) ).
thf(f159,plain,
! [X2: $i > $i > $o,X3: $i,X0: $i,X1: $i > $i > $o,X6: $i,X4: $i,X5: $i] :
( ( ( X2 @ X5 @ X6 )
= $true )
| ( ( X1 @ X4 @ X3 )
= $true )
| ( ( X2 @ X0 @ lBill_THFTYPE_i )
!= $true )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true ) ),
inference(pi_clausification,[status(thm)],[f158]) ).
thf(f158,plain,
! [X2: $i > $i > $o,X3: $i,X0: $i,X1: $i > $i > $o,X4: $i,X5: $i] :
( ( ( !! @ $i @ ( X2 @ X5 ) )
= $true )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( ( X1 @ X4 @ X3 )
= $true )
| ( ( X2 @ X0 @ lBill_THFTYPE_i )
!= $true ) ),
inference(beta_eta_normalization,[status(thm)],[f157]) ).
thf(f157,plain,
! [X2: $i > $i > $o,X3: $i,X0: $i,X1: $i > $i > $o,X4: $i,X5: $i] :
( ( ( X2 @ X0 @ lBill_THFTYPE_i )
!= $true )
| ( ( X1 @ X4 @ X3 )
= $true )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( ( ^ [Y0: $i] : ( !! @ $i @ ( X2 @ Y0 ) )
@ X5 )
= $true ) ),
inference(pi_clausification,[status(thm)],[f156]) ).
thf(f156,plain,
! [X2: $i > $i > $o,X3: $i,X0: $i,X1: $i > $i > $o,X4: $i] :
( ( ( X1 @ X4 @ X3 )
= $true )
| ( ( X2 @ X0 @ lBill_THFTYPE_i )
!= $true )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( ( !! @ $i
@ ^ [Y0: $i] : ( !! @ $i @ ( X2 @ Y0 ) ) )
= $true ) ),
inference(not_proxy_clausification,[status(thm)],[f155]) ).
thf(f155,plain,
! [X2: $i > $i > $o,X3: $i,X0: $i,X1: $i > $i > $o,X4: $i] :
( ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( ( X1 @ X4 @ X3 )
= $true )
| ( ( X2 @ X0 @ lBill_THFTYPE_i )
!= $true )
| ( ( ~ ( !! @ $i
@ ^ [Y0: $i] : ( !! @ $i @ ( X2 @ Y0 ) ) ) )
!= $true ) ),
inference(beta_eta_normalization,[status(thm)],[f154]) ).
thf(f154,plain,
! [X2: $i > $i > $o,X3: $i,X0: $i,X1: $i > $i > $o,X4: $i] :
( ( ( X2 @ X0 @ lBill_THFTYPE_i )
!= $true )
| ( $true
= ( ^ [Y0: $i] : ( X1 @ Y0 @ X3 )
@ X4 ) )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( ( ~ ( !! @ $i
@ ^ [Y0: $i] : ( !! @ $i @ ( X2 @ Y0 ) ) ) )
!= $true ) ),
inference(pi_clausification,[status(thm)],[f153]) ).
thf(f153,plain,
! [X2: $i > $i > $o,X3: $i,X0: $i,X1: $i > $i > $o] :
( ( ( !! @ $i
@ ^ [Y0: $i] : ( X1 @ Y0 @ X3 ) )
= $true )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( ( X2 @ X0 @ lBill_THFTYPE_i )
!= $true )
| ( ( ~ ( !! @ $i
@ ^ [Y0: $i] : ( !! @ $i @ ( X2 @ Y0 ) ) ) )
!= $true ) ),
inference(beta_eta_normalization,[status(thm)],[f152]) ).
thf(f152,plain,
! [X2: $i > $i > $o,X3: $i,X0: $i,X1: $i > $i > $o] :
( ( ( X2 @ X0 @ lBill_THFTYPE_i )
!= $true )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] : ( X1 @ Y1 @ Y0 ) )
@ X3 )
= $true )
| ( ( ~ ( !! @ $i
@ ^ [Y0: $i] : ( !! @ $i @ ( X2 @ Y0 ) ) ) )
!= $true ) ),
inference(pi_clausification,[status(thm)],[f151]) ).
thf(f151,plain,
! [X2: $i > $i > $o,X0: $i,X1: $i > $i > $o] :
( ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] : ( X1 @ Y1 @ Y0 ) ) )
= $true )
| ( ( ~ ( !! @ $i
@ ^ [Y0: $i] : ( !! @ $i @ ( X2 @ Y0 ) ) ) )
!= $true )
| ( ( X2 @ X0 @ lBill_THFTYPE_i )
!= $true ) ),
inference(not_proxy_clausification,[status(thm)],[f150]) ).
thf(f150,plain,
! [X2: $i > $i > $o,X0: $i,X1: $i > $i > $o] :
( ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( ( X2 @ X0 @ lBill_THFTYPE_i )
!= $true )
| ( ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] : ( X1 @ Y1 @ Y0 ) ) ) )
!= $true )
| ( ( ~ ( !! @ $i
@ ^ [Y0: $i] : ( !! @ $i @ ( X2 @ Y0 ) ) ) )
!= $true ) ),
inference(beta_eta_normalization,[status(thm)],[f146]) ).
thf(f146,plain,
! [X2: $i > $i > $o,X0: $i,X1: $i > $i > $o] :
( ( ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] : ( X1 @ Y1 @ Y0 ) ) ) )
!= $true )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] : ( X2 @ Y0 @ Y1 ) ) ) )
!= $true )
| ( ( X2 @ X0 @ lBill_THFTYPE_i )
!= $true ) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
thf(f138,plain,
! [X0: $i,X1: $i > $i > $o,X2: $i > $i > $o] :
( ( ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] : ( X2 @ Y0 @ Y1 ) ) ) )
!= $true )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( ( X2 @ X0 @ lBill_THFTYPE_i )
!= $true )
| ( ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] : ( X1 @ Y1 @ Y0 ) ) ) )
!= $true ) ),
inference(ennf_transformation,[status(thm)],[f89]) ).
thf(f89,plain,
~ ? [X0: $i,X1: $i > $i > $o,X2: $i > $i > $o] :
( ( ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] : ( X2 @ Y0 @ Y1 ) ) ) )
= $true )
& ( ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] : ( X1 @ Y1 @ Y0 ) ) ) )
= $true )
& ( ( X2 @ X0 @ lBill_THFTYPE_i )
= $true )
& ( ( X1 @ X0 @ lAnna_THFTYPE_i )
= $true ) ),
inference(fool_elimination,[status(thm)],[f88]) ).
thf(f88,plain,
~ ? [X0: $i,X1: $i > $i > $o,X2: $i > $i > $o] :
( ( X2 @ X0 @ lBill_THFTYPE_i )
& ~ ! [X3: $i,X4: $i] : ( X1 @ X3 @ X4 )
& ~ ! [X5: $i,X6: $i] : ( X2 @ X6 @ X5 )
& ( X1 @ X0 @ lAnna_THFTYPE_i ) ),
inference(rectify,[status(thm)],[f46]) ).
thf(f46,negated_conjecture,
~ ? [X1: $i,X21: $i > $i > $o,X22: $i > $i > $o] :
( ( X22 @ X1 @ lBill_THFTYPE_i )
& ~ ! [X23: $i,X24: $i] : ( X21 @ X23 @ X24 )
& ~ ! [X24: $i,X23: $i] : ( X22 @ X23 @ X24 )
& ( X21 @ X1 @ lAnna_THFTYPE_i ) ),
inference(negated_conjecture,[status(cth)],[f45]) ).
thf(f45,conjecture,
? [X1: $i,X21: $i > $i > $o,X22: $i > $i > $o] :
( ( X22 @ X1 @ lBill_THFTYPE_i )
& ~ ! [X23: $i,X24: $i] : ( X21 @ X23 @ X24 )
& ~ ! [X24: $i,X23: $i] : ( X22 @ X23 @ X24 )
& ( X21 @ X1 @ lAnna_THFTYPE_i ) ),
file('/export/starexec/sandbox/tmp/tmp.JfLqaL197y/DTF2THF_16718.p',con) ).
thf(f192,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[status(thm)],[f182,f190,f187]) ).
thf(f182,plain,
! [X3: $i,X0: $i,X1: $i > $i > $o,X6: $i,X4: $i,X5: $i] :
( ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( ( X1 @ X4 @ X3 )
= $true )
| ( X5 != X6 )
| ( lBill_THFTYPE_i = X0 ) ),
inference(equality_proxy_clausification,[status(thm)],[f181]) ).
thf(f181,plain,
! [X3: $i,X0: $i,X1: $i > $i > $o,X6: $i,X4: $i,X5: $i] :
( ( X5 != X6 )
| ( ( X1 @ X4 @ X3 )
= $true )
| ( ( lBill_THFTYPE_i = X0 )
= $true )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true ) ),
inference(equality_proxy_clausification,[status(thm)],[f180]) ).
thf(f180,plain,
! [X3: $i,X0: $i,X1: $i > $i > $o,X6: $i,X4: $i,X5: $i] :
( ( ( X1 @ X4 @ X3 )
= $true )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( $false
= ( X6 = X5 ) )
| ( ( lBill_THFTYPE_i = X0 )
= $true ) ),
inference(not_proxy_clausification,[status(thm)],[f179]) ).
thf(f179,plain,
! [X3: $i,X0: $i,X1: $i > $i > $o,X6: $i,X4: $i,X5: $i] :
( ( ( lBill_THFTYPE_i != X0 )
!= $true )
| ( ( X1 @ X4 @ X3 )
= $true )
| ( $false
= ( X6 = X5 ) )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true ) ),
inference(not_proxy_clausification,[status(thm)],[f178]) ).
thf(f178,plain,
! [X3: $i,X0: $i,X1: $i > $i > $o,X6: $i,X4: $i,X5: $i] :
( ( ( X6 != X5 )
= $true )
| ( ( X1 @ X4 @ X3 )
= $true )
| ( ( lBill_THFTYPE_i != X0 )
!= $true )
| ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true ) ),
inference(beta_eta_normalization,[status(thm)],[f161]) ).
thf(f161,plain,
! [X3: $i,X0: $i,X1: $i > $i > $o,X6: $i,X4: $i,X5: $i] :
( ( ( X1 @ X0 @ lAnna_THFTYPE_i )
!= $true )
| ( ( ^ [Y0: $i,Y1: $i] : ( Y1 != Y0 )
@ X5
@ X6 )
= $true )
| ( ( X1 @ X4 @ X3 )
= $true )
| ( ( ^ [Y0: $i,Y1: $i] : ( Y1 != Y0 )
@ X0
@ lBill_THFTYPE_i )
!= $true ) ),
inference(primitive_instantiation,[status(thm)],[f159]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : CSR137^2 : TPTP v9.2.1. Released v4.1.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.16/0.34 % Computer : n028.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue Feb 24 05:52:12 EST 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.29/0.46 ---- Original DTF file ---
% 0.29/0.46 thf(spec,logic,$$dhol).
% 0.29/0.46 %------------------------------------------------------------------------------
% 0.29/0.46 % File : CSR137^2 : TPTP v9.2.1. Released v4.1.0.
% 0.29/0.46 % Domain : Commonsense Reasoning
% 0.29/0.46 % Problem : Feelings from people to Bill and Anna
% 0.29/0.46 % Version : Especial > Augmented > Especial.
% 0.29/0.46 % English : Do there exist relations ?R and ?Q so that ?R holds between a
% 0.29/0.46 % person ?Y and Bill and ?Q between ?Y and Anna.
% 0.29/0.46
% 0.29/0.46 % Refs : [Ben10] Benzmueller (2010), Email to Geoff Sutcliffe
% 0.29/0.46 % Source : [Ben10]
% 0.29/0.46 % Names : rv_3.tq_SUMO_sine [Ben10]
% 0.29/0.46
% 0.29/0.46 % Status : Theorem
% 0.29/0.46 % Rating : 0.33 v9.1.0, 0.25 v9.0.0, 0.10 v8.2.0, 0.23 v8.1.0, 0.18 v7.5.0, 0.14 v7.4.0, 0.11 v7.2.0, 0.00 v7.1.0, 0.25 v7.0.0, 0.29 v6.4.0, 0.33 v6.3.0, 0.40 v6.2.0, 0.43 v6.1.0, 0.71 v6.0.0, 0.29 v5.5.0, 0.50 v5.4.0, 0.60 v5.2.0, 0.40 v5.1.0, 0.60 v5.0.0, 0.40 v4.1.0
% 0.29/0.46 % Syntax : Number of formulae : 71 ( 17 unt; 26 typ; 0 def)
% 0.29/0.46 % Number of atoms : 86 ( 2 equ; 10 cnn)
% 0.29/0.46 % Maximal formula atoms : 4 ( 1 avg)
% 0.29/0.46 % Number of connectives : 188 ( 10 ~; 2 |; 11 &; 152 @)
% 0.29/0.46 % ( 2 <=>; 11 =>; 0 <=; 0 <~>)
% 0.29/0.46 % Maximal formula depth : 12 ( 5 avg)
% 0.29/0.46 % Number of types : 3 ( 1 usr)
% 0.29/0.46 % Number of type conns : 40 ( 40 >; 0 *; 0 +; 0 <<)
% 0.29/0.46 % Number of symbols : 27 ( 25 usr; 14 con; 0-3 aty)
% 0.29/0.46 % Number of variables : 40 ( 0 ^; 36 !; 4 ?; 40 :)
% 0.29/0.46 % SPC : TH0_THM_EQU_NAR
% 0.29/0.46
% 0.29/0.46 % Comments : This is a simple test problem for reasoning in/about SUMO.
% 0.29/0.46 % Initally the problem has been hand generated in KIF syntax in
% 0.29/0.46 % SigmaKEE and then automatically translated by Benzmueller's
% 0.29/0.46 % KIF2TH0 translator into THF syntax.
% 0.29/0.46 % : The translation has been applied in two modes: local and SInE.
% 0.29/0.46 % The local mode only translates the local assumptions and the
% 0.29/0.46 % query. The SInE mode additionally translates the SInE-extract
% 0.29/0.46 % of the loaded knowledge base (usually SUMO).
% 0.29/0.46 % : The examples are selected to illustrate the benefits of
% 0.29/0.46 % higher-order reasoning in ontology reasoning.
% 0.29/0.46 % : Note that the universal predicates are excluded for ?R and Q?
% 0.29/0.46 % with the second and third conjuncts in the query.
% 0.29/0.46 %------------------------------------------------------------------------------
% 0.29/0.46 %----The extracted signature
% 0.29/0.46 thf(numbers,type,
% 0.29/0.46 num: $tType ).
% 0.29/0.46
% 0.29/0.46 thf(attribute_THFTYPE_i,type,
% 0.29/0.46 attribute_THFTYPE_i: $i ).
% 0.29/0.46
% 0.29/0.46 thf(domain_THFTYPE_IIiioIiioI,type,
% 0.29/0.46 domain_THFTYPE_IIiioIiioI: ( $i > $i > $o ) > $i > $i > $o ).
% 0.29/0.46
% 0.29/0.46 thf(domain_THFTYPE_IiiioI,type,
% 0.29/0.46 domain_THFTYPE_IiiioI: $i > $i > $i > $o ).
% 0.29/0.46
% 0.29/0.46 thf(equal_THFTYPE_i,type,
% 0.29/0.46 equal_THFTYPE_i: $i ).
% 0.29/0.46
% 0.29/0.46 thf(holdsDuring_THFTYPE_IiooI,type,
% 0.29/0.46 holdsDuring_THFTYPE_IiooI: $i > $o > $o ).
% 0.29/0.46
% 0.29/0.46 thf(instance_THFTYPE_IIiioIioI,type,
% 0.29/0.46 instance_THFTYPE_IIiioIioI: ( $i > $i > $o ) > $i > $o ).
% 0.29/0.46
% 0.29/0.46 thf(instance_THFTYPE_IIiooIioI,type,
% 0.29/0.46 instance_THFTYPE_IIiooIioI: ( $i > $o > $o ) > $i > $o ).
% 0.29/0.46
% 0.29/0.46 thf(instance_THFTYPE_IiioI,type,
% 0.29/0.46 instance_THFTYPE_IiioI: $i > $i > $o ).
% 0.29/0.46
% 0.29/0.46 thf(lAnna_THFTYPE_i,type,
% 0.29/0.46 lAnna_THFTYPE_i: $i ).
% 0.29/0.46
% 0.29/0.46 thf(lAsymmetricRelation_THFTYPE_i,type,
% 0.29/0.46 lAsymmetricRelation_THFTYPE_i: $i ).
% 0.29/0.46
% 0.29/0.46 thf(lBen_THFTYPE_i,type,
% 0.29/0.46 lBen_THFTYPE_i: $i ).
% 0.29/0.46
% 0.29/0.46 thf(lBill_THFTYPE_i,type,
% 0.29/0.46 lBill_THFTYPE_i: $i ).
% 0.29/0.46
% 0.29/0.46 thf(lBinaryPredicate_THFTYPE_i,type,
% 0.29/0.46 lBinaryPredicate_THFTYPE_i: $i ).
% 0.29/0.46
% 0.29/0.46 thf(lBob_THFTYPE_i,type,
% 0.29/0.46 lBob_THFTYPE_i: $i ).
% 0.29/0.46
% 0.29/0.46 thf(lMary_THFTYPE_i,type,
% 0.29/0.46 lMary_THFTYPE_i: $i ).
% 0.29/0.46
% 0.29/0.46 thf(lOrganism_THFTYPE_i,type,
% 0.29/0.46 lOrganism_THFTYPE_i: $i ).
% 0.29/0.46
% 0.29/0.46 thf(lSue_THFTYPE_i,type,
% 0.29/0.46 lSue_THFTYPE_i: $i ).
% 0.29/0.46
% 0.29/0.46 thf(likes_THFTYPE_IiioI,type,
% 0.29/0.46 likes_THFTYPE_IiioI: $i > $i > $o ).
% 0.29/0.46
% 0.29/0.46 thf(n1_THFTYPE_i,type,
% 0.29/0.46 n1_THFTYPE_i: $i ).
% 0.29/0.46
% 0.29/0.46 thf(n2_THFTYPE_i,type,
% 0.29/0.46 n2_THFTYPE_i: $i ).
% 0.29/0.46
% 0.29/0.46 thf(parent_THFTYPE_IiioI,type,
% 0.29/0.46 parent_THFTYPE_IiioI: $i > $i > $o ).
% 0.29/0.46
% 0.29/0.46 thf(range_THFTYPE_IiioI,type,
% 0.29/0.46 range_THFTYPE_IiioI: $i > $i > $o ).
% 0.29/0.46
% 0.29/0.46 thf(subclass_THFTYPE_IiioI,type,
% 0.29/0.46 subclass_THFTYPE_IiioI: $i > $i > $o ).
% 0.29/0.46
% 0.29/0.46 thf(subrelation_THFTYPE_IIioIIioIoI,type,
% 0.29/0.46 subrelation_THFTYPE_IIioIIioIoI: ( $i > $o ) > ( $i > $o ) > $o ).
% 0.29/0.46
% 0.29/0.46 thf(subrelation_THFTYPE_IiioI,type,
% 0.29/0.46 subrelation_THFTYPE_IiioI: $i > $i > $o ).
% 0.29/0.46
% 0.29/0.46 %----The translated axioms
% 0.29/0.46 thf(ax,axiom,
% 0.29/0.46 likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_001,axiom,
% 0.29/0.46 likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_002,axiom,
% 0.29/0.46 (~) @ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i ) ).
% 0.29/0.46
% 0.29/0.46 thf(ax_003,axiom,
% 0.29/0.46 (~) @ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i ) ).
% 0.29/0.46
% 0.29/0.46 %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.29/0.46 %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.29/0.46 %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.29/0.46 thf(ax_004,axiom,
% 0.29/0.46 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_005,axiom,
% 0.29/0.46 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_006,axiom,
% 0.29/0.46 ! [X: $i,Y: $i,Z: $i] :
% 0.29/0.46 ( ( ( subclass_THFTYPE_IiioI @ X @ Y )
% 0.29/0.46 & ( instance_THFTYPE_IiioI @ Z @ X ) )
% 0.29/0.46 => ( instance_THFTYPE_IiioI @ Z @ Y ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(ax_007,axiom,
% 0.29/0.46 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_008,axiom,
% 0.29/0.46 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_009,axiom,
% 0.29/0.46 ! [CLASS1: $i,CLASS2: $i] :
% 0.29/0.46 ( ( CLASS1 = CLASS2 )
% 0.29/0.46 => ! [THING: $i] :
% 0.29/0.46 ( ( instance_THFTYPE_IiioI @ THING @ CLASS1 )
% 0.29/0.46 <=> ( instance_THFTYPE_IiioI @ THING @ CLASS2 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 %KIF documentation:(documentation equal EnglishLanguage "(equal ?ENTITY1 ?ENTITY2) is true just in case ?ENTITY1 is identical with ?ENTITY2.")
% 0.29/0.46 %KIF documentation:(documentation AsymmetricRelation EnglishLanguage "A &%BinaryRelation is asymmetric if and only if it is both an &%AntisymmetricRelation and an &%IrreflexiveRelation.")
% 0.29/0.46 thf(ax_010,axiom,
% 0.29/0.46 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBen_THFTYPE_i ) ).
% 0.29/0.46
% 0.29/0.46 thf(ax_011,axiom,
% 0.29/0.46 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBen_THFTYPE_i ) ).
% 0.29/0.46
% 0.29/0.46 thf(ax_012,axiom,
% 0.29/0.46 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_013,axiom,
% 0.29/0.46 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_014,axiom,
% 0.29/0.46 ! [REL2: $i > $o,ROW: $i,REL1: $i > $o] :
% 0.29/0.46 ( ( ( subrelation_THFTYPE_IIioIIioIoI @ REL1 @ REL2 )
% 0.29/0.46 & ( REL1 @ ROW ) )
% 0.29/0.46 => ( REL2 @ ROW ) ) ).
% 0.29/0.46
% 0.29/0.46 %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.29/0.46 thf(ax_015,axiom,
% 0.29/0.46 ! [ORGANISM: $i] :
% 0.29/0.46 ( ( instance_THFTYPE_IiioI @ ORGANISM @ lOrganism_THFTYPE_i )
% 0.29/0.46 => ? [PARENT: $i] : ( parent_THFTYPE_IiioI @ ORGANISM @ PARENT ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(ax_016,axiom,
% 0.29/0.46 ! [TIME: $i,SITUATION: $o] :
% 0.29/0.46 ( ( holdsDuring_THFTYPE_IiooI @ TIME @ ( (~) @ SITUATION ) )
% 0.29/0.46 => ( (~) @ ( holdsDuring_THFTYPE_IiooI @ TIME @ SITUATION ) ) ) ).
% 0.29/0.46
% 0.29/0.46 %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.29/0.46 thf(ax_017,axiom,
% 0.29/0.46 likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_018,axiom,
% 0.29/0.46 likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_019,axiom,
% 0.29/0.46 ! [THING2: $i,THING1: $i] :
% 0.29/0.46 ( ( THING1 = THING2 )
% 0.29/0.46 => ! [CLASS: $i] :
% 0.29/0.46 ( ( instance_THFTYPE_IiioI @ THING1 @ CLASS )
% 0.29/0.46 <=> ( instance_THFTYPE_IiioI @ THING2 @ CLASS ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(ax_020,axiom,
% 0.29/0.46 ! [CLASS1: $i,REL: $i,CLASS2: $i] :
% 0.29/0.46 ( ( ( range_THFTYPE_IiioI @ REL @ CLASS1 )
% 0.29/0.46 & ( range_THFTYPE_IiioI @ REL @ CLASS2 ) )
% 0.29/0.46 => ( ( subclass_THFTYPE_IiioI @ CLASS1 @ CLASS2 )
% 0.29/0.46 | ( subclass_THFTYPE_IiioI @ CLASS2 @ CLASS1 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 %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.29/0.46 thf(ax_021,axiom,
% 0.29/0.46 likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_022,axiom,
% 0.29/0.46 likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 %KIF documentation:(documentation attribute EnglishLanguage "(&%attribute ?OBJECT ?PROPERTY) means that ?PROPERTY is a &%Attribute of ?OBJECT. For example, (&%attribute &%MyLittleRedWagon &%Red).")
% 0.29/0.46 %KIF documentation:(documentation Organism EnglishLanguage "Generally, a living individual, including all &%Plants and &%Animals.")
% 0.29/0.46 thf(ax_023,axiom,
% 0.29/0.46 ! [CLASS: $i,CHILD: $i,PARENT: $i] :
% 0.29/0.46 ( ( ( parent_THFTYPE_IiioI @ CHILD @ PARENT )
% 0.29/0.46 & ( subclass_THFTYPE_IiioI @ CLASS @ lOrganism_THFTYPE_i )
% 0.29/0.46 & ( instance_THFTYPE_IiioI @ PARENT @ CLASS ) )
% 0.29/0.46 => ( instance_THFTYPE_IiioI @ CHILD @ CLASS ) ) ).
% 0.29/0.46
% 0.29/0.46 %KIF documentation:(documentation BinaryPredicate EnglishLanguage "A &%Predicate relating two items - its valence is two.")
% 0.29/0.46 thf(ax_024,axiom,
% 0.29/0.46 ! [REL2: $i,CLASS1: $i,REL1: $i] :
% 0.29/0.46 ( ( ( subrelation_THFTYPE_IiioI @ REL1 @ REL2 )
% 0.29/0.46 & ( range_THFTYPE_IiioI @ REL2 @ CLASS1 ) )
% 0.29/0.46 => ( range_THFTYPE_IiioI @ REL1 @ CLASS1 ) ) ).
% 0.29/0.46
% 0.29/0.46 %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.29/0.46 thf(ax_025,axiom,
% 0.29/0.46 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ) ).
% 0.29/0.46
% 0.29/0.46 thf(ax_026,axiom,
% 0.29/0.46 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ) ).
% 0.29/0.46
% 0.29/0.46 %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.29/0.46 thf(ax_027,axiom,
% 0.29/0.46 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_028,axiom,
% 0.29/0.46 ! [NUMBER: $i,CLASS1: $i,REL: $i,CLASS2: $i] :
% 0.29/0.46 ( ( ( domain_THFTYPE_IiiioI @ REL @ NUMBER @ CLASS1 )
% 0.29/0.46 & ( domain_THFTYPE_IiiioI @ REL @ NUMBER @ CLASS2 ) )
% 0.29/0.46 => ( ( subclass_THFTYPE_IiioI @ CLASS1 @ CLASS2 )
% 0.29/0.46 | ( subclass_THFTYPE_IiioI @ CLASS2 @ CLASS1 ) ) ) ).
% 0.29/0.46
% 0.29/0.46 thf(ax_029,axiom,
% 0.29/0.46 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_030,axiom,
% 0.29/0.46 ! [NUMBER: $i,PRED1: $i,CLASS1: $i,PRED2: $i] :
% 0.29/0.46 ( ( ( subrelation_THFTYPE_IiioI @ PRED1 @ PRED2 )
% 0.29/0.46 & ( domain_THFTYPE_IiiioI @ PRED2 @ NUMBER @ CLASS1 ) )
% 0.29/0.46 => ( domain_THFTYPE_IiiioI @ PRED1 @ NUMBER @ CLASS1 ) ) ).
% 0.29/0.46
% 0.29/0.46 %KIF documentation:(documentation parent EnglishLanguage "The general relationship of parenthood. (&%parent ?CHILD ?PARENT) means that ?PARENT is a biological parent of ?CHILD.")
% 0.29/0.46 thf(ax_031,axiom,
% 0.29/0.46 instance_THFTYPE_IIiioIioI @ parent_THFTYPE_IiioI @ lAsymmetricRelation_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_032,axiom,
% 0.29/0.46 instance_THFTYPE_IIiioIioI @ range_THFTYPE_IiioI @ lAsymmetricRelation_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_033,axiom,
% 0.29/0.46 instance_THFTYPE_IIiioIioI @ range_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_034,axiom,
% 0.29/0.46 instance_THFTYPE_IIiioIioI @ parent_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_035,axiom,
% 0.29/0.46 domain_THFTYPE_IIiioIiioI @ parent_THFTYPE_IiioI @ n1_THFTYPE_i @ lOrganism_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_036,axiom,
% 0.29/0.46 instance_THFTYPE_IIiooIioI @ holdsDuring_THFTYPE_IiooI @ lAsymmetricRelation_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_037,axiom,
% 0.29/0.46 domain_THFTYPE_IIiioIiioI @ parent_THFTYPE_IiioI @ n2_THFTYPE_i @ lOrganism_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_038,axiom,
% 0.29/0.46 instance_THFTYPE_IIiioIioI @ subrelation_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_039,axiom,
% 0.29/0.46 instance_THFTYPE_IiioI @ equal_THFTYPE_i @ lBinaryPredicate_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_040,axiom,
% 0.29/0.46 instance_THFTYPE_IIiioIioI @ subclass_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_041,axiom,
% 0.29/0.46 instance_THFTYPE_IiioI @ attribute_THFTYPE_i @ lAsymmetricRelation_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_042,axiom,
% 0.29/0.46 instance_THFTYPE_IIiioIioI @ instance_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 thf(ax_043,axiom,
% 0.29/0.46 instance_THFTYPE_IIiooIioI @ holdsDuring_THFTYPE_IiooI @ lBinaryPredicate_THFTYPE_i ).
% 0.29/0.46
% 0.29/0.46 %----The translated conjecture
% 0.29/0.46 thf(con,conjecture,
% 0.29/0.46 ? [Q: $i > $i > $o,R: $i > $i > $o,Y: $i] :
% 0.29/0.46 ( ( R @ Y @ lBill_THFTYPE_i )
% 0.29/0.46 & ( Q @ Y @ lAnna_THFTYPE_i )
% 0.29/0.46 & ( (~)
% 0.29/0.46 @ ! [A: $i,B: $i] : ( R @ A @ B ) )
% 0.29/0.46 & ( (~)
% 0.29/0.46 @ ! [A: $i,B: $i] : ( Q @ A @ B ) ) ) ).
% 0.29/0.46
% 0.29/0.46 %------------------------------------------------------------------------------
% 0.29/0.46 ------------------------
% 1.80/1.34 ---- Embedded in THF ---
% 1.80/1.34 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.80/1.34 %%% Generated on Tue Feb 24 05:52:12 EST 2026
% 1.80/1.34 %%% using '$$dhol' embedding, version 1.3.0.
% 1.80/1.34 %%% Logic specification used:
% 1.80/1.34 %%% thf(spec, logic, $$dhol).
% 1.80/1.34
% 1.80/1.34 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.JfLqaL197y/DTF2DTF16718.p
% See solution above
% 1.80/1.34 ------------------------
% 1.80/1.35 ---- Cleaned THF ---
% 1.80/1.36 thf(numbers,type,
% 1.80/1.36 num: $tType ).
% 1.80/1.36
% 1.80/1.36 thf(attribute_THFTYPE_i,type,
% 1.80/1.36 attribute_THFTYPE_i: $i ).
% 1.80/1.36
% 1.80/1.36 thf(domain_THFTYPE_IIiioIiioI,type,
% 1.80/1.36 domain_THFTYPE_IIiioIiioI: ( $i > $i > $o ) > $i > $i > $o ).
% 1.80/1.36
% 1.80/1.36 thf(domain_THFTYPE_IiiioI,type,
% 1.80/1.36 domain_THFTYPE_IiiioI: $i > $i > $i > $o ).
% 1.80/1.36
% 1.80/1.36 thf(equal_THFTYPE_i,type,
% 1.80/1.36 equal_THFTYPE_i: $i ).
% 1.80/1.36
% 1.80/1.36 thf(holdsDuring_THFTYPE_IiooI,type,
% 1.80/1.36 holdsDuring_THFTYPE_IiooI: $i > $o > $o ).
% 1.80/1.36
% 1.80/1.36 thf(instance_THFTYPE_IIiioIioI,type,
% 1.80/1.36 instance_THFTYPE_IIiioIioI: ( $i > $i > $o ) > $i > $o ).
% 1.80/1.36
% 1.80/1.36 thf(instance_THFTYPE_IIiooIioI,type,
% 1.80/1.36 instance_THFTYPE_IIiooIioI: ( $i > $o > $o ) > $i > $o ).
% 1.80/1.36
% 1.80/1.36 thf(instance_THFTYPE_IiioI,type,
% 1.80/1.36 instance_THFTYPE_IiioI: $i > $i > $o ).
% 1.80/1.36
% 1.80/1.36 thf(lAnna_THFTYPE_i,type,
% 1.80/1.36 lAnna_THFTYPE_i: $i ).
% 1.80/1.36
% 1.80/1.36 thf(lAsymmetricRelation_THFTYPE_i,type,
% 1.80/1.36 lAsymmetricRelation_THFTYPE_i: $i ).
% 1.80/1.36
% 1.80/1.36 thf(lBen_THFTYPE_i,type,
% 1.80/1.36 lBen_THFTYPE_i: $i ).
% 1.80/1.36
% 1.80/1.36 thf(lBill_THFTYPE_i,type,
% 1.80/1.36 lBill_THFTYPE_i: $i ).
% 1.80/1.36
% 1.80/1.36 thf(lBinaryPredicate_THFTYPE_i,type,
% 1.80/1.36 lBinaryPredicate_THFTYPE_i: $i ).
% 1.80/1.36
% 1.80/1.36 thf(lBob_THFTYPE_i,type,
% 1.80/1.36 lBob_THFTYPE_i: $i ).
% 1.80/1.36
% 1.80/1.36 thf(lMary_THFTYPE_i,type,
% 1.80/1.36 lMary_THFTYPE_i: $i ).
% 1.80/1.36
% 1.80/1.36 thf(lOrganism_THFTYPE_i,type,
% 1.80/1.36 lOrganism_THFTYPE_i: $i ).
% 1.80/1.36
% 1.80/1.36 thf(lSue_THFTYPE_i,type,
% 1.80/1.36 lSue_THFTYPE_i: $i ).
% 1.80/1.36
% 1.80/1.36 thf(likes_THFTYPE_IiioI,type,
% 1.80/1.36 likes_THFTYPE_IiioI: $i > $i > $o ).
% 1.80/1.36
% 1.80/1.36 thf(n1_THFTYPE_i,type,
% 1.80/1.36 n1_THFTYPE_i: $i ).
% 1.80/1.36
% 1.80/1.36 thf(n2_THFTYPE_i,type,
% 1.80/1.36 n2_THFTYPE_i: $i ).
% 1.80/1.36
% 1.80/1.36 thf(parent_THFTYPE_IiioI,type,
% 1.80/1.36 parent_THFTYPE_IiioI: $i > $i > $o ).
% 1.80/1.36
% 1.80/1.36 thf(range_THFTYPE_IiioI,type,
% 1.80/1.36 range_THFTYPE_IiioI: $i > $i > $o ).
% 1.80/1.36
% 1.80/1.36 thf(subclass_THFTYPE_IiioI,type,
% 1.80/1.36 subclass_THFTYPE_IiioI: $i > $i > $o ).
% 1.80/1.36
% 1.80/1.36 thf(subrelation_THFTYPE_IIioIIioIoI,type,
% 1.80/1.36 subrelation_THFTYPE_IIioIIioIoI: ( $i > $o ) > ( $i > $o ) > $o ).
% 1.80/1.36
% 1.80/1.36 thf(subrelation_THFTYPE_IiioI,type,
% 1.80/1.36 subrelation_THFTYPE_IiioI: $i > $i > $o ).
% 1.80/1.36
% 1.80/1.36 thf(ax,axiom,
% 1.80/1.36 likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_001,axiom,
% 1.80/1.36 likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_002,axiom,
% 1.80/1.36 (~) @ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_003,axiom,
% 1.80/1.36 (~) @ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_004,axiom,
% 1.80/1.36 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_005,axiom,
% 1.80/1.36 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_006,axiom,
% 1.80/1.36 ! [X: $i,Y: $i,Z: $i] :
% 1.80/1.36 ( ( ( subclass_THFTYPE_IiioI @ X @ Y )
% 1.80/1.36 & ( instance_THFTYPE_IiioI @ Z @ X ) )
% 1.80/1.36 => ( instance_THFTYPE_IiioI @ Z @ Y ) ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_007,axiom,
% 1.80/1.36 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_008,axiom,
% 1.80/1.36 parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_009,axiom,
% 1.80/1.36 ! [CLASS1: $i,CLASS2: $i] :
% 1.80/1.36 ( ( CLASS1 = CLASS2 )
% 1.80/1.36 => ! [THING: $i] :
% 1.80/1.36 ( ( instance_THFTYPE_IiioI @ THING @ CLASS1 )
% 1.80/1.36 <=> ( instance_THFTYPE_IiioI @ THING @ CLASS2 ) ) ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_010,axiom,
% 1.80/1.36 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBen_THFTYPE_i ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_011,axiom,
% 1.80/1.36 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBen_THFTYPE_i ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_012,axiom,
% 1.80/1.36 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_013,axiom,
% 1.80/1.36 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_014,axiom,
% 1.80/1.36 ! [REL2: $i > $o,ROW: $i,REL1: $i > $o] :
% 1.80/1.36 ( ( ( subrelation_THFTYPE_IIioIIioIoI @ REL1 @ REL2 )
% 1.80/1.36 & ( REL1 @ ROW ) )
% 1.80/1.36 => ( REL2 @ ROW ) ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_015,axiom,
% 1.80/1.36 ! [ORGANISM: $i] :
% 1.80/1.36 ( ( instance_THFTYPE_IiioI @ ORGANISM @ lOrganism_THFTYPE_i )
% 1.80/1.36 => ? [PARENT: $i] : ( parent_THFTYPE_IiioI @ ORGANISM @ PARENT ) ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_016,axiom,
% 1.80/1.36 ! [TIME: $i,SITUATION: $o] :
% 1.80/1.36 ( ( holdsDuring_THFTYPE_IiooI @ TIME @ ( (~) @ SITUATION ) )
% 1.80/1.36 => ( (~) @ ( holdsDuring_THFTYPE_IiooI @ TIME @ SITUATION ) ) ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_017,axiom,
% 1.80/1.36 likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_018,axiom,
% 1.80/1.36 likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_019,axiom,
% 1.80/1.36 ! [THING2: $i,THING1: $i] :
% 1.80/1.36 ( ( THING1 = THING2 )
% 1.80/1.36 => ! [CLASS: $i] :
% 1.80/1.36 ( ( instance_THFTYPE_IiioI @ THING1 @ CLASS )
% 1.80/1.36 <=> ( instance_THFTYPE_IiioI @ THING2 @ CLASS ) ) ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_020,axiom,
% 1.80/1.36 ! [CLASS1: $i,REL: $i,CLASS2: $i] :
% 1.80/1.36 ( ( ( range_THFTYPE_IiioI @ REL @ CLASS1 )
% 1.80/1.36 & ( range_THFTYPE_IiioI @ REL @ CLASS2 ) )
% 1.80/1.36 => ( ( subclass_THFTYPE_IiioI @ CLASS1 @ CLASS2 )
% 1.80/1.36 | ( subclass_THFTYPE_IiioI @ CLASS2 @ CLASS1 ) ) ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_021,axiom,
% 1.80/1.36 likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_022,axiom,
% 1.80/1.36 likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_023,axiom,
% 1.80/1.36 ! [CLASS: $i,CHILD: $i,PARENT: $i] :
% 1.80/1.36 ( ( ( parent_THFTYPE_IiioI @ CHILD @ PARENT )
% 1.80/1.36 & ( subclass_THFTYPE_IiioI @ CLASS @ lOrganism_THFTYPE_i )
% 1.80/1.36 & ( instance_THFTYPE_IiioI @ PARENT @ CLASS ) )
% 1.80/1.36 => ( instance_THFTYPE_IiioI @ CHILD @ CLASS ) ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_024,axiom,
% 1.80/1.36 ! [REL2: $i,CLASS1: $i,REL1: $i] :
% 1.80/1.36 ( ( ( subrelation_THFTYPE_IiioI @ REL1 @ REL2 )
% 1.80/1.36 & ( range_THFTYPE_IiioI @ REL2 @ CLASS1 ) )
% 1.80/1.36 => ( range_THFTYPE_IiioI @ REL1 @ CLASS1 ) ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_025,axiom,
% 1.80/1.36 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_026,axiom,
% 1.80/1.36 (~) @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_027,axiom,
% 1.80/1.36 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_028,axiom,
% 1.80/1.36 ! [NUMBER: $i,CLASS1: $i,REL: $i,CLASS2: $i] :
% 1.80/1.36 ( ( ( domain_THFTYPE_IiiioI @ REL @ NUMBER @ CLASS1 )
% 1.80/1.36 & ( domain_THFTYPE_IiiioI @ REL @ NUMBER @ CLASS2 ) )
% 1.80/1.36 => ( ( subclass_THFTYPE_IiioI @ CLASS1 @ CLASS2 )
% 1.80/1.36 | ( subclass_THFTYPE_IiioI @ CLASS2 @ CLASS1 ) ) ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_029,axiom,
% 1.80/1.36 parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_030,axiom,
% 1.80/1.36 ! [NUMBER: $i,PRED1: $i,CLASS1: $i,PRED2: $i] :
% 1.80/1.36 ( ( ( subrelation_THFTYPE_IiioI @ PRED1 @ PRED2 )
% 1.80/1.36 & ( domain_THFTYPE_IiiioI @ PRED2 @ NUMBER @ CLASS1 ) )
% 1.80/1.36 => ( domain_THFTYPE_IiiioI @ PRED1 @ NUMBER @ CLASS1 ) ) ).
% 1.80/1.36
% 1.80/1.36 thf(ax_031,axiom,
% 1.80/1.36 instance_THFTYPE_IIiioIioI @ parent_THFTYPE_IiioI @ lAsymmetricRelation_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_032,axiom,
% 1.80/1.36 instance_THFTYPE_IIiioIioI @ range_THFTYPE_IiioI @ lAsymmetricRelation_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_033,axiom,
% 1.80/1.36 instance_THFTYPE_IIiioIioI @ range_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_034,axiom,
% 1.80/1.36 instance_THFTYPE_IIiioIioI @ parent_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_035,axiom,
% 1.80/1.36 domain_THFTYPE_IIiioIiioI @ parent_THFTYPE_IiioI @ n1_THFTYPE_i @ lOrganism_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_036,axiom,
% 1.80/1.36 instance_THFTYPE_IIiooIioI @ holdsDuring_THFTYPE_IiooI @ lAsymmetricRelation_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_037,axiom,
% 1.80/1.36 domain_THFTYPE_IIiioIiioI @ parent_THFTYPE_IiioI @ n2_THFTYPE_i @ lOrganism_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_038,axiom,
% 1.80/1.36 instance_THFTYPE_IIiioIioI @ subrelation_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_039,axiom,
% 1.80/1.36 instance_THFTYPE_IiioI @ equal_THFTYPE_i @ lBinaryPredicate_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_040,axiom,
% 1.80/1.36 instance_THFTYPE_IIiioIioI @ subclass_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_041,axiom,
% 1.80/1.36 instance_THFTYPE_IiioI @ attribute_THFTYPE_i @ lAsymmetricRelation_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_042,axiom,
% 1.80/1.36 instance_THFTYPE_IIiioIioI @ instance_THFTYPE_IiioI @ lBinaryPredicate_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(ax_043,axiom,
% 1.80/1.36 instance_THFTYPE_IIiooIioI @ holdsDuring_THFTYPE_IiooI @ lBinaryPredicate_THFTYPE_i ).
% 1.80/1.36
% 1.80/1.36 thf(con,conjecture,
% 1.80/1.36 ? [Q: $i > $i > $o,R: $i > $i > $o,Y: $i] :
% 1.80/1.36 ( ( R @ Y @ lBill_THFTYPE_i )
% 1.80/1.36 & ( Q @ Y @ lAnna_THFTYPE_i )
% 1.80/1.36 & ( (~)
% 1.80/1.36 @ ! [A: $i,B: $i] : ( R @ A @ B ) )
% 1.80/1.36 & ( (~)
% 1.80/1.36 @ ! [A: $i,B: $i] : ( Q @ A @ B ) ) ) ).
% 1.80/1.36 ------------------------
% 1.80/1.37 % (17010)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_16718 for (2999ds/18Mi)
% 1.80/1.37 % (17009)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_16718 for (2999ds/275Mi)
% 1.80/1.38 % (17009)First to succeed.
% 1.80/1.38 % (17004)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_16718 for (2999ds/183Mi)
% 1.80/1.38 % (17005)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_16718 for (2999ds/4Mi)
% 1.80/1.38 % (17010)Instruction limit reached!
% 1.80/1.38 % (17010)------------------------------
% 1.80/1.38 % (17010)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.38 % (17010)Termination reason: Unknown
% 1.80/1.38 % (17010)Termination phase: Saturation
% 1.80/1.38
% 1.80/1.38 % (17010)Memory used [KB]: 5628
% 1.80/1.38 % (17010)Time elapsed: 0.008 s
% 1.80/1.38 % (17010)Instructions burned: 19 (million)
% 1.80/1.38 % (17010)------------------------------
% 1.80/1.38 % (17010)------------------------------
% 1.80/1.38 % (17006)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_16718 for (2999ds/27Mi)
% 1.80/1.38 % (17007)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_16718 for (2999ds/2Mi)
% 1.80/1.38 % (17008)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_16718 for (2999ds/2Mi)
% 1.80/1.38 % (17007)Instruction limit reached!
% 1.80/1.38 % (17007)------------------------------
% 1.80/1.38 % (17007)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.38 % (17007)Termination reason: Unknown
% 1.80/1.38 % (17007)Termination phase: shuffling
% 1.80/1.38
% 1.80/1.38 % (17007)Memory used [KB]: 1023
% 1.80/1.38 % (17007)Time elapsed: 0.003 s
% 1.80/1.38 % (17007)Instructions burned: 2 (million)
% 1.80/1.38 % (17007)------------------------------
% 1.80/1.38 % (17007)------------------------------
% 1.80/1.38 % (17008)Instruction limit reached!
% 1.80/1.38 % (17008)------------------------------
% 1.80/1.38 % (17008)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.38 % (17008)Termination reason: Unknown
% 1.80/1.38 % (17008)Termination phase: shuffling
% 1.80/1.38
% 1.80/1.38 % (17008)Memory used [KB]: 1023
% 1.80/1.38 % (17008)Time elapsed: 0.003 s
% 1.80/1.38 % (17008)Instructions burned: 2 (million)
% 1.80/1.38 % (17008)------------------------------
% 1.80/1.38 % (17008)------------------------------
% 1.80/1.38 % (17009)Refutation found. Thanks to Tanya!
% 1.80/1.38 % SZS status Theorem for DTF2THF_16718
% 1.80/1.38 % SZS output start Proof for DTF2THF_16718
% 1.80/1.38 thf(func_def_0, type, num: $tType).
% 1.80/1.38 thf(func_def_2, type, domain_THFTYPE_IIiioIiioI: ($i > $i > $o) > $i > $i > $o).
% 1.80/1.38 thf(func_def_3, type, domain_THFTYPE_IiiioI: $i > $i > $i > $o).
% 1.80/1.38 thf(func_def_5, type, holdsDuring_THFTYPE_IiooI: $i > $o > $o).
% 1.80/1.38 thf(func_def_6, type, instance_THFTYPE_IIiioIioI: ($i > $i > $o) > $i > $o).
% 1.80/1.38 thf(func_def_7, type, instance_THFTYPE_IIiooIioI: ($i > $o > $o) > $i > $o).
% 1.80/1.38 thf(func_def_8, type, instance_THFTYPE_IiioI: $i > $i > $o).
% 1.80/1.38 thf(func_def_18, type, likes_THFTYPE_IiioI: $i > $i > $o).
% 1.80/1.38 thf(func_def_21, type, parent_THFTYPE_IiioI: $i > $i > $o).
% 1.80/1.38 thf(func_def_22, type, range_THFTYPE_IiioI: $i > $i > $o).
% 1.80/1.38 thf(func_def_23, type, subclass_THFTYPE_IiioI: $i > $i > $o).
% 1.80/1.38 thf(func_def_24, type, subrelation_THFTYPE_IIioIIioIoI: ($i > $o) > ($i > $o) > $o).
% 1.80/1.38 thf(func_def_25, type, subrelation_THFTYPE_IiioI: $i > $i > $o).
% 1.80/1.38 thf(func_def_35, type, ph1: !>[X0: $tType]:(X0)).
% 1.80/1.38 thf(f297,plain,(
% 1.80/1.38 $false),
% 1.80/1.38 inference(avatar_sat_refutation,[status(thm)],[f192,f199,f228,f232,f234,f294,f296])).
% 1.80/1.38 thf(f296,plain,(
% 1.80/1.38 ~spl0_5 | ~spl0_6),
% 1.80/1.38 inference(avatar_contradiction_clause,[status(thm)],[f295])).
% 1.80/1.38 thf(f295,plain,(
% 1.80/1.38 $false | (~spl0_5 | ~spl0_6)),
% 1.80/1.38 inference(subsumption_resolution,[status(thm)],[f227,f231])).
% 1.80/1.38 thf(f231,plain,(
% 1.80/1.38 ( ! [X0 : $i] : ((lAnna_THFTYPE_i = X0)) ) | ~spl0_6),
% 1.80/1.38 inference(avatar_component_clause,[status(thm)],[f230])).
% 1.80/1.38 thf(f230,definition,(
% 1.80/1.38 spl0_6 <=> ! [X0 : $i] : (lAnna_THFTYPE_i = X0)),
% 1.80/1.38 introduced(definition,[new_symbols(naming,[spl0_6])],[avatar_definition])).
% 1.80/1.38 thf(f227,plain,(
% 1.80/1.38 ( ! [X0 : $i] : ((lAnna_THFTYPE_i != X0)) ) | ~spl0_5),
% 1.80/1.38 inference(avatar_component_clause,[status(thm)],[f226])).
% 1.80/1.38 thf(f226,definition,(
% 1.80/1.38 spl0_5 <=> ! [X0 : $i] : (lAnna_THFTYPE_i != X0)),
% 1.80/1.38 introduced(definition,[new_symbols(naming,[spl0_5])],[avatar_definition])).
% 1.80/1.38 thf(f294,plain,(
% 1.80/1.38 ~spl0_4),
% 1.80/1.38 inference(avatar_contradiction_clause,[status(thm)],[f293])).
% 1.80/1.38 thf(f293,plain,(
% 1.80/1.38 $false | ~spl0_4),
% 1.80/1.38 inference(trivial_inequality_removal,[status(thm)],[f292])).
% 1.80/1.38 thf(f292,plain,(
% 1.80/1.38 ($false = $true) | ~spl0_4),
% 1.80/1.38 inference(forward_demodulation,[status(thm)],[f240,f282])).
% 1.80/1.38 thf(f282,plain,(
% 1.80/1.38 ( ! [X0 : $i] : (($false = (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0))) ) | ~spl0_4),
% 1.80/1.38 inference(not_proxy_clausification,[status(thm)],[f265])).
% 1.80/1.38 thf(f265,plain,(
% 1.80/1.38 ( ! [X0 : $i] : (((~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0)) = $true)) ) | ~spl0_4),
% 1.80/1.38 inference(superposition,[status(thm)],[f140,f198])).
% 1.80/1.38 thf(f198,plain,(
% 1.80/1.38 ( ! [X6 : $i,X5 : $i] : ((X5 = X6)) ) | ~spl0_4),
% 1.80/1.38 inference(avatar_component_clause,[status(thm)],[f197])).
% 1.80/1.38 thf(f197,definition,(
% 1.80/1.38 spl0_4 <=> ! [X6 : $i,X5 : $i] : (X5 = X6)),
% 1.80/1.38 introduced(definition,[new_symbols(naming,[spl0_4])],[avatar_definition])).
% 1.80/1.38 thf(f140,plain,(
% 1.80/1.38 ((~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)) = $true)),
% 1.80/1.38 inference(cnf_transformation,[status(thm)],[f125])).
% 1.80/1.38 thf(f125,plain,(
% 1.80/1.38 ((~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)) = $true)),
% 1.80/1.38 inference(fool_elimination,[status(thm)],[f124])).
% 1.80/1.38 thf(f124,plain,(
% 1.80/1.38 (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i))),
% 1.80/1.38 inference(rectify,[status(thm)],[f3])).
% 1.80/1.38 thf(f3,axiom,(
% 1.80/1.38 (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i))),
% 1.80/1.38 file('/export/starexec/sandbox/tmp/tmp.JfLqaL197y/DTF2THF_16718.p',ax_002)).
% 1.80/1.38 thf(f240,plain,(
% 1.80/1.38 ( ! [X0 : $i] : (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0) = $true)) ) | ~spl0_4),
% 1.80/1.38 inference(superposition,[status(thm)],[f144,f198])).
% 1.80/1.38 thf(f144,plain,(
% 1.80/1.38 ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i) = $true)),
% 1.80/1.38 inference(cnf_transformation,[status(thm)],[f99])).
% 1.80/1.38 thf(f99,plain,(
% 1.80/1.38 ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i) = $true)),
% 1.80/1.38 inference(fool_elimination,[status(thm)],[f98])).
% 1.80/1.38 thf(f98,plain,(
% 1.80/1.38 (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)),
% 1.80/1.38 inference(rectify,[status(thm)],[f1])).
% 1.80/1.38 thf(f1,axiom,(
% 1.80/1.38 (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)),
% 1.80/1.38 file('/export/starexec/sandbox/tmp/tmp.JfLqaL197y/DTF2THF_16718.p',ax)).
% 1.80/1.38 thf(f234,plain,(
% 1.80/1.38 ~spl0_1),
% 1.80/1.38 inference(avatar_contradiction_clause,[status(thm)],[f233])).
% 1.80/1.38 thf(f233,plain,(
% 1.80/1.38 $false | ~spl0_1),
% 1.80/1.38 inference(flex-flex_simplify,[status(thm)],[f188])).
% 1.80/1.38 thf(f188,plain,(
% 1.80/1.38 ( ! [X6 : $i,X5 : $i] : ((X5 != X6)) ) | ~spl0_1),
% 1.80/1.38 inference(avatar_component_clause,[status(thm)],[f187])).
% 1.80/1.38 thf(f187,definition,(
% 1.80/1.38 spl0_1 <=> ! [X6 : $i,X5 : $i] : (X5 != X6)),
% 1.80/1.38 introduced(definition,[new_symbols(naming,[spl0_1])],[avatar_definition])).
% 1.80/1.38 thf(f232,plain,(
% 1.80/1.38 spl0_1 | spl0_6 | ~spl0_2 | ~spl0_3),
% 1.80/1.38 inference(avatar_split_clause,[status(thm)],[f216,f194,f190,f230,f187])).
% 1.80/1.38 thf(f190,definition,(
% 1.80/1.38 spl0_2 <=> ! [X4 : $i,X0 : $i,X3 : $i,X1 : $i > $i > $o] : (((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | (lBill_THFTYPE_i = X0) | ((X1 @ X4 @ X3) = $true))),
% 1.80/1.38 introduced(definition,[new_symbols(naming,[spl0_2])],[avatar_definition])).
% 1.80/1.38 thf(f194,definition,(
% 1.80/1.38 spl0_3 <=> ! [X4 : $i,X0 : $i,X3 : $i,X1 : $i > $i > $o] : (((X1 @ X4 @ X3) = $true) | (lBill_THFTYPE_i != X0) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true))),
% 1.80/1.38 introduced(definition,[new_symbols(naming,[spl0_3])],[avatar_definition])).
% 1.80/1.38 thf(f216,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X4 : $i] : ((lAnna_THFTYPE_i = X0) | (X3 != X4)) ) | (~spl0_2 | ~spl0_3)),
% 1.80/1.38 inference(equality_proxy_clausification,[status(thm)],[f215])).
% 1.80/1.38 thf(f215,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X4 : $i] : (((X3 = X4) = $false) | (lAnna_THFTYPE_i = X0)) ) | (~spl0_2 | ~spl0_3)),
% 1.80/1.38 inference(equality_proxy_clausification,[status(thm)],[f214])).
% 1.80/1.38 thf(f214,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X4 : $i] : (((lAnna_THFTYPE_i = X0) = $true) | ((X3 = X4) = $false)) ) | (~spl0_2 | ~spl0_3)),
% 1.80/1.38 inference(not_proxy_clausification,[status(thm)],[f213])).
% 1.80/1.38 thf(f213,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X4 : $i] : (((~ (X3 = X4)) = $true) | ((lAnna_THFTYPE_i = X0) = $true)) ) | (~spl0_2 | ~spl0_3)),
% 1.80/1.38 inference(not_proxy_clausification,[status(thm)],[f212])).
% 1.80/1.38 thf(f212,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X4 : $i] : (((~ (lAnna_THFTYPE_i = X0)) != $true) | ((~ (X3 = X4)) = $true)) ) | (~spl0_2 | ~spl0_3)),
% 1.80/1.38 inference(beta_eta_normalization,[status(thm)],[f202])).
% 1.80/1.38 thf(f202,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X4 : $i] : ((((^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y1 = Y0))))) @ X0 @ lAnna_THFTYPE_i) != $true) | (((^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y1 = Y0))))) @ X4 @ X3) = $true)) ) | (~spl0_2 | ~spl0_3)),
% 1.80/1.38 inference(primitive_instantiation,[status(thm)],[f200])).
% 1.80/1.38 thf(f200,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X1 : $i > $i > $o,X4 : $i] : (((X1 @ X4 @ X3) = $true) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true)) ) | (~spl0_2 | ~spl0_3)),
% 1.80/1.38 inference(subsumption_resolution,[status(thm)],[f191,f195])).
% 1.80/1.38 thf(f195,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X1 : $i > $i > $o,X4 : $i] : (((X1 @ X4 @ X3) = $true) | (lBill_THFTYPE_i != X0) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true)) ) | ~spl0_3),
% 1.80/1.38 inference(avatar_component_clause,[status(thm)],[f194])).
% 1.80/1.38 thf(f191,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X1 : $i > $i > $o,X4 : $i] : (((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | ((X1 @ X4 @ X3) = $true) | (lBill_THFTYPE_i = X0)) ) | ~spl0_2),
% 1.80/1.38 inference(avatar_component_clause,[status(thm)],[f190])).
% 1.80/1.38 thf(f228,plain,(
% 1.80/1.38 spl0_4 | spl0_5 | ~spl0_2 | ~spl0_3),
% 1.80/1.38 inference(avatar_split_clause,[status(thm)],[f223,f194,f190,f226,f197])).
% 1.80/1.38 thf(f223,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X4 : $i] : ((lAnna_THFTYPE_i != X0) | (X3 = X4)) ) | (~spl0_2 | ~spl0_3)),
% 1.80/1.38 inference(equality_proxy_clausification,[status(thm)],[f222])).
% 1.80/1.38 thf(f222,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X4 : $i] : (((X3 = X4) = $true) | (lAnna_THFTYPE_i != X0)) ) | (~spl0_2 | ~spl0_3)),
% 1.80/1.38 inference(equality_proxy_clausification,[status(thm)],[f221])).
% 1.80/1.38 thf(f221,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X4 : $i] : (((lAnna_THFTYPE_i = X0) != $true) | ((X3 = X4) = $true)) ) | (~spl0_2 | ~spl0_3)),
% 1.80/1.38 inference(beta_eta_normalization,[status(thm)],[f201])).
% 1.80/1.38 thf(f201,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X4 : $i] : ((((^[Y0 : $i]: ((^[Y1 : $i]: (Y1 = Y0)))) @ X4 @ X3) = $true) | (((^[Y0 : $i]: ((^[Y1 : $i]: (Y1 = Y0)))) @ X0 @ lAnna_THFTYPE_i) != $true)) ) | (~spl0_2 | ~spl0_3)),
% 1.80/1.38 inference(primitive_instantiation,[status(thm)],[f200])).
% 1.80/1.38 thf(f199,plain,(
% 1.80/1.38 spl0_3 | spl0_4),
% 1.80/1.38 inference(avatar_split_clause,[status(thm)],[f171,f197,f194])).
% 1.80/1.38 thf(f171,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X1 : $i > $i > $o,X6 : $i,X4 : $i,X5 : $i] : (((X1 @ X4 @ X3) = $true) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | (lBill_THFTYPE_i != X0) | (X5 = X6)) )),
% 1.80/1.38 inference(equality_proxy_clausification,[status(thm)],[f170])).
% 1.80/1.38 thf(f170,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X1 : $i > $i > $o,X6 : $i,X4 : $i,X5 : $i] : (((X1 @ X4 @ X3) = $true) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | (lBill_THFTYPE_i != X0) | ($true = (X6 = X5))) )),
% 1.80/1.38 inference(equality_proxy_clausification,[status(thm)],[f169])).
% 1.80/1.38 thf(f169,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X1 : $i > $i > $o,X6 : $i,X4 : $i,X5 : $i] : (((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | ((lBill_THFTYPE_i = X0) != $true) | ($true = (X6 = X5)) | ((X1 @ X4 @ X3) = $true)) )),
% 1.80/1.38 inference(beta_eta_normalization,[status(thm)],[f160])).
% 1.80/1.38 thf(f160,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X1 : $i > $i > $o,X6 : $i,X4 : $i,X5 : $i] : ((((^[Y0 : $i]: ((^[Y1 : $i]: (Y1 = Y0)))) @ X0 @ lBill_THFTYPE_i) != $true) | ((X1 @ X4 @ X3) = $true) | (((^[Y0 : $i]: ((^[Y1 : $i]: (Y1 = Y0)))) @ X5 @ X6) = $true) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true)) )),
% 1.80/1.38 inference(primitive_instantiation,[status(thm)],[f159])).
% 1.80/1.38 thf(f159,plain,(
% 1.80/1.38 ( ! [X2 : $i > $i > $o,X3 : $i,X0 : $i,X1 : $i > $i > $o,X6 : $i,X4 : $i,X5 : $i] : (((X2 @ X5 @ X6) = $true) | ((X1 @ X4 @ X3) = $true) | ((X2 @ X0 @ lBill_THFTYPE_i) != $true) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true)) )),
% 1.80/1.38 inference(pi_clausification,[status(thm)],[f158])).
% 1.80/1.38 thf(f158,plain,(
% 1.80/1.38 ( ! [X2 : $i > $i > $o,X3 : $i,X0 : $i,X1 : $i > $i > $o,X4 : $i,X5 : $i] : (((!! @ $i @ (X2 @ X5)) = $true) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | ((X1 @ X4 @ X3) = $true) | ((X2 @ X0 @ lBill_THFTYPE_i) != $true)) )),
% 1.80/1.38 inference(beta_eta_normalization,[status(thm)],[f157])).
% 1.80/1.38 thf(f157,plain,(
% 1.80/1.38 ( ! [X2 : $i > $i > $o,X3 : $i,X0 : $i,X1 : $i > $i > $o,X4 : $i,X5 : $i] : (((X2 @ X0 @ lBill_THFTYPE_i) != $true) | ((X1 @ X4 @ X3) = $true) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | (((^[Y0 : $i]: (!! @ $i @ (X2 @ Y0))) @ X5) = $true)) )),
% 1.80/1.38 inference(pi_clausification,[status(thm)],[f156])).
% 1.80/1.38 thf(f156,plain,(
% 1.80/1.38 ( ! [X2 : $i > $i > $o,X3 : $i,X0 : $i,X1 : $i > $i > $o,X4 : $i] : (((X1 @ X4 @ X3) = $true) | ((X2 @ X0 @ lBill_THFTYPE_i) != $true) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X2 @ Y0)))) = $true)) )),
% 1.80/1.38 inference(not_proxy_clausification,[status(thm)],[f155])).
% 1.80/1.38 thf(f155,plain,(
% 1.80/1.38 ( ! [X2 : $i > $i > $o,X3 : $i,X0 : $i,X1 : $i > $i > $o,X4 : $i] : (((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | ((X1 @ X4 @ X3) = $true) | ((X2 @ X0 @ lBill_THFTYPE_i) != $true) | ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X2 @ Y0))))) != $true)) )),
% 1.80/1.38 inference(beta_eta_normalization,[status(thm)],[f154])).
% 1.80/1.38 thf(f154,plain,(
% 1.80/1.38 ( ! [X2 : $i > $i > $o,X3 : $i,X0 : $i,X1 : $i > $i > $o,X4 : $i] : (((X2 @ X0 @ lBill_THFTYPE_i) != $true) | ($true = ((^[Y0 : $i]: (X1 @ Y0 @ X3)) @ X4)) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X2 @ Y0))))) != $true)) )),
% 1.80/1.38 inference(pi_clausification,[status(thm)],[f153])).
% 1.80/1.38 thf(f153,plain,(
% 1.80/1.38 ( ! [X2 : $i > $i > $o,X3 : $i,X0 : $i,X1 : $i > $i > $o] : (((!! @ $i @ (^[Y0 : $i]: (X1 @ Y0 @ X3))) = $true) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | ((X2 @ X0 @ lBill_THFTYPE_i) != $true) | ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X2 @ Y0))))) != $true)) )),
% 1.80/1.38 inference(beta_eta_normalization,[status(thm)],[f152])).
% 1.80/1.38 thf(f152,plain,(
% 1.80/1.38 ( ! [X2 : $i > $i > $o,X3 : $i,X0 : $i,X1 : $i > $i > $o] : (((X2 @ X0 @ lBill_THFTYPE_i) != $true) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X1 @ Y1 @ Y0)))) @ X3) = $true) | ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X2 @ Y0))))) != $true)) )),
% 1.80/1.38 inference(pi_clausification,[status(thm)],[f151])).
% 1.80/1.38 thf(f151,plain,(
% 1.80/1.38 ( ! [X2 : $i > $i > $o,X0 : $i,X1 : $i > $i > $o] : (((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X1 @ Y1 @ Y0))))) = $true) | ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X2 @ Y0))))) != $true) | ((X2 @ X0 @ lBill_THFTYPE_i) != $true)) )),
% 1.80/1.38 inference(not_proxy_clausification,[status(thm)],[f150])).
% 1.80/1.38 thf(f150,plain,(
% 1.80/1.38 ( ! [X2 : $i > $i > $o,X0 : $i,X1 : $i > $i > $o] : (((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | ((X2 @ X0 @ lBill_THFTYPE_i) != $true) | ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X1 @ Y1 @ Y0)))))) != $true) | ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X2 @ Y0))))) != $true)) )),
% 1.80/1.38 inference(beta_eta_normalization,[status(thm)],[f146])).
% 1.80/1.38 thf(f146,plain,(
% 1.80/1.38 ( ! [X2 : $i > $i > $o,X0 : $i,X1 : $i > $i > $o] : (((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X1 @ Y1 @ Y0)))))) != $true) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y0 @ Y1)))))) != $true) | ((X2 @ X0 @ lBill_THFTYPE_i) != $true)) )),
% 1.80/1.38 inference(cnf_transformation,[status(thm)],[f138])).
% 1.80/1.38 thf(f138,plain,(
% 1.80/1.38 ! [X0 : $i,X1 : $i > $i > $o,X2 : $i > $i > $o] : (((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y0 @ Y1)))))) != $true) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | ((X2 @ X0 @ lBill_THFTYPE_i) != $true) | ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X1 @ Y1 @ Y0)))))) != $true))),
% 1.80/1.38 inference(ennf_transformation,[status(thm)],[f89])).
% 1.80/1.38 thf(f89,plain,(
% 1.80/1.38 ~? [X0 : $i,X1 : $i > $i > $o,X2 : $i > $i > $o] : (((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y0 @ Y1)))))) = $true) & ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X1 @ Y1 @ Y0)))))) = $true) & ((X2 @ X0 @ lBill_THFTYPE_i) = $true) & ((X1 @ X0 @ lAnna_THFTYPE_i) = $true))),
% 1.80/1.38 inference(fool_elimination,[status(thm)],[f88])).
% 1.80/1.38 thf(f88,plain,(
% 1.80/1.38 ~? [X0 : $i,X1 : $i > $i > $o,X2 : $i > $i > $o] : ((X2 @ X0 @ lBill_THFTYPE_i) & (~ ! [X3 : $i,X4 : $i] : (X1 @ X3 @ X4)) & (~ ! [X5 : $i,X6 : $i] : (X2 @ X6 @ X5)) & (X1 @ X0 @ lAnna_THFTYPE_i))),
% 1.80/1.38 inference(rectify,[status(thm)],[f46])).
% 1.80/1.38 thf(f46,negated_conjecture,(
% 1.80/1.38 ~? [X1 : $i,X21 : $i > $i > $o,X22 : $i > $i > $o] : ((X22 @ X1 @ lBill_THFTYPE_i) & (~ ! [X23 : $i,X24 : $i] : (X21 @ X23 @ X24)) & (~ ! [X24 : $i,X23 : $i] : (X22 @ X23 @ X24)) & (X21 @ X1 @ lAnna_THFTYPE_i))),
% 1.80/1.38 inference(negated_conjecture,[status(cth)],[f45])).
% 1.80/1.38 thf(f45,conjecture,(
% 1.80/1.38 ? [X1 : $i,X21 : $i > $i > $o,X22 : $i > $i > $o] : ((X22 @ X1 @ lBill_THFTYPE_i) & (~ ! [X23 : $i,X24 : $i] : (X21 @ X23 @ X24)) & (~ ! [X24 : $i,X23 : $i] : (X22 @ X23 @ X24)) & (X21 @ X1 @ lAnna_THFTYPE_i))),
% 1.80/1.38 file('/export/starexec/sandbox/tmp/tmp.JfLqaL197y/DTF2THF_16718.p',con)).
% 1.80/1.38 thf(f192,plain,(
% 1.80/1.38 spl0_1 | spl0_2),
% 1.80/1.38 inference(avatar_split_clause,[status(thm)],[f182,f190,f187])).
% 1.80/1.38 thf(f182,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X1 : $i > $i > $o,X6 : $i,X4 : $i,X5 : $i] : (((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | ((X1 @ X4 @ X3) = $true) | (X5 != X6) | (lBill_THFTYPE_i = X0)) )),
% 1.80/1.38 inference(equality_proxy_clausification,[status(thm)],[f181])).
% 1.80/1.38 thf(f181,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X1 : $i > $i > $o,X6 : $i,X4 : $i,X5 : $i] : ((X5 != X6) | ((X1 @ X4 @ X3) = $true) | ((lBill_THFTYPE_i = X0) = $true) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true)) )),
% 1.80/1.38 inference(equality_proxy_clausification,[status(thm)],[f180])).
% 1.80/1.38 thf(f180,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X1 : $i > $i > $o,X6 : $i,X4 : $i,X5 : $i] : (((X1 @ X4 @ X3) = $true) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | ($false = (X6 = X5)) | ((lBill_THFTYPE_i = X0) = $true)) )),
% 1.80/1.38 inference(not_proxy_clausification,[status(thm)],[f179])).
% 1.80/1.38 thf(f179,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X1 : $i > $i > $o,X6 : $i,X4 : $i,X5 : $i] : (((~ (lBill_THFTYPE_i = X0)) != $true) | ((X1 @ X4 @ X3) = $true) | ($false = (X6 = X5)) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true)) )),
% 1.80/1.38 inference(not_proxy_clausification,[status(thm)],[f178])).
% 1.80/1.38 thf(f178,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X1 : $i > $i > $o,X6 : $i,X4 : $i,X5 : $i] : (((~ (X6 = X5)) = $true) | ((X1 @ X4 @ X3) = $true) | ((~ (lBill_THFTYPE_i = X0)) != $true) | ((X1 @ X0 @ lAnna_THFTYPE_i) != $true)) )),
% 1.80/1.38 inference(beta_eta_normalization,[status(thm)],[f161])).
% 1.80/1.38 thf(f161,plain,(
% 1.80/1.38 ( ! [X3 : $i,X0 : $i,X1 : $i > $i > $o,X6 : $i,X4 : $i,X5 : $i] : (((X1 @ X0 @ lAnna_THFTYPE_i) != $true) | (((^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y1 = Y0))))) @ X5 @ X6) = $true) | ((X1 @ X4 @ X3) = $true) | (((^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y1 = Y0))))) @ X0 @ lBill_THFTYPE_i) != $true)) )),
% 1.80/1.38 inference(primitive_instantiation,[status(thm)],[f159])).
% 1.80/1.38 % SZS output end Proof for DTF2THF_16718
% 1.80/1.38 % (17009)------------------------------
% 1.80/1.38 % (17009)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.38 % (17009)Termination reason: Refutation
% 1.80/1.38
% 1.80/1.38 % (17009)Memory used [KB]: 5628
% 1.80/1.38 % (17009)Time elapsed: 0.008 s
% 1.80/1.38 % (17009)Instructions burned: 14 (million)
% 1.80/1.38 % (17009)------------------------------
% 1.80/1.38 % (17009)------------------------------
% 1.80/1.38 % (17003)Success in time 0.019 s
%------------------------------------------------------------------------------