%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : SYO560^1 : TPTP v9.2.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n027.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 09:54:33 AM UTC 2026
% Result : Theorem 1.62s 1.65s
% Output : Refutation 1.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 26
% Syntax : Number of formulae : 120 ( 18 unt; 0 typ; 18 def)
% Number of atoms : 540 ( 95 equ; 0 cnn)
% Maximal formula atoms : 5 ( 4 avg)
% Number of connectives : 351 ( 96 ~; 111 |; 0 &; 126 @)
% ( 18 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 3 ( 3 >; 0 *; 0 +; 0 <<)
% Number of symbols : 30 ( 27 usr; 23 con; 0-2 aty)
% Number of variables : 41 ( 31 ^; 10 !; 0 ?; 41 :)
% Comments :
%------------------------------------------------------------------------------
thf(func_def_0,type,
epso: ( $o > $o ) > $o ).
thf(func_def_2,type,
epsoo: ( ( $o > $o ) > $o ) > $o > $o ).
thf(func_def_3,type,
q: ( $o > $o ) > $o ).
thf(func_def_4,type,
vEPSILON:
!>[X0: $tType] : ( ( X0 > $o ) > X0 ) ).
thf(func_def_9,type,
sP0: $o > $o ).
thf(func_def_12,type,
ph2:
!>[X0: $tType] : X0 ).
thf(f328,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[f48,f53,f79,f94,f103,f135,f149,f163,f187,f188,f251,f261,f270,f272,f279,f281,f285,f286,f313]) ).
thf(f313,plain,
~ spl1_18,
inference(avatar_contradiction_clause,[status(thm)],[f312]) ).
thf(f312,plain,
( $false
| ~ spl1_18 ),
inference(trivial_inequality_removal,[status(thm)],[f293]) ).
thf(f293,plain,
( ( $true = $false )
| ~ spl1_18 ),
inference(backward_demodulation,[status(thm)],[f29,f176]) ).
thf(f176,plain,
( ! [X1: $o] : ( $false = X1 )
| ~ spl1_18 ),
inference(avatar_component_clause,[status(thm)],[f175]) ).
thf(f175,definition,
( spl1_18
<=> ! [X1: $o] : ( $false = X1 ) ),
introduced(definition,[new_symbols(naming,[spl1_18])],[avatar_definition]) ).
thf(f29,plain,
( ( q
@ ^ [Y0: $o] : $false )
= $true ),
inference(cnf_transformation,[status(thm)],[f18]) ).
thf(f18,plain,
( ( q
@ ^ [Y0: $o] : $false )
= $true ),
inference(fool_elimination,[status(thm)],[f17]) ).
thf(f17,plain,
( q
@ ^ [X0: $o] : $false ),
inference(rectify,[status(thm)],[f4]) ).
thf(f4,axiom,
( q
@ ^ [X1: $o] : $false ),
file('/export/starexec/sandbox2/tmp/tmp.DQ9pP7ssFh/DTF2THF_21362.p',qkf) ).
thf(f286,plain,
( spl1_18
| spl1_16 ),
inference(avatar_split_clause,[status(thm)],[f179,f142,f175]) ).
thf(f142,definition,
( spl1_16
<=> ( $true
= ( epso
@ ^ [Y0: $o] : Y0 ) ) ),
introduced(definition,[new_symbols(naming,[spl1_16])],[avatar_definition]) ).
thf(f179,plain,
! [X1: $o] :
( ( $true
= ( epso
@ ^ [Y0: $o] : Y0 ) )
| ( $false = X1 ) ),
inference(beta_eta_normalization,[status(thm)],[f178]) ).
thf(f178,plain,
! [X1: $o] :
( ( $true
= ( ^ [Y0: $o] : Y0
@ ( epso
@ ^ [Y0: $o] : Y0 ) ) )
| ( $false
= ( ^ [Y0: $o] : Y0
@ X1 ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f285,plain,
( ~ spl1_6
| ~ spl1_16 ),
inference(avatar_contradiction_clause,[status(thm)],[f284]) ).
thf(f284,plain,
( $false
| ~ spl1_6
| ~ spl1_16 ),
inference(trivial_inequality_removal,[status(thm)],[f283]) ).
thf(f283,plain,
( ( $true = $false )
| ~ spl1_6
| ~ spl1_16 ),
inference(backward_demodulation,[status(thm)],[f144,f65]) ).
thf(f65,plain,
( ! [X1: $o > $o] :
( ( epso @ X1 )
= $false )
| ~ spl1_6 ),
inference(avatar_component_clause,[status(thm)],[f64]) ).
thf(f64,definition,
( spl1_6
<=> ! [X1: $o > $o] :
( ( epso @ X1 )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl1_6])],[avatar_definition]) ).
thf(f144,plain,
( ( $true
= ( epso
@ ^ [Y0: $o] : Y0 ) )
| ~ spl1_16 ),
inference(avatar_component_clause,[status(thm)],[f142]) ).
thf(f281,plain,
( spl1_6
| spl1_5 ),
inference(avatar_split_clause,[status(thm)],[f70,f60,f64]) ).
thf(f60,definition,
( spl1_5
<=> ( ( epso @ ( epsoo @ epso ) )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl1_5])],[avatar_definition]) ).
thf(f70,plain,
! [X1: $o > $o] :
( ( ( epso @ X1 )
= $false )
| ( ( epso @ ( epsoo @ epso ) )
= $true ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f279,plain,
( ~ spl1_17
| spl1_9
| ~ spl1_19 ),
inference(avatar_split_clause,[status(thm)],[f278,f195,f91,f158]) ).
thf(f158,definition,
( spl1_17
<=> ( ( epsoo @ epso @ $true )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl1_17])],[avatar_definition]) ).
thf(f91,definition,
( spl1_9
<=> ( ( epsoo @ epso @ sK3 )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl1_9])],[avatar_definition]) ).
thf(f195,definition,
( spl1_19
<=> ( $true = sK3 ) ),
introduced(definition,[new_symbols(naming,[spl1_19])],[avatar_definition]) ).
thf(f278,plain,
( ( ( epsoo @ epso @ $true )
!= $true )
| spl1_9
| ~ spl1_19 ),
inference(backward_demodulation,[status(thm)],[f93,f196]) ).
thf(f196,plain,
( ( $true = sK3 )
| ~ spl1_19 ),
inference(avatar_component_clause,[status(thm)],[f195]) ).
thf(f93,plain,
( ( ( epsoo @ epso @ sK3 )
!= $true )
| spl1_9 ),
inference(avatar_component_clause,[status(thm)],[f91]) ).
thf(f272,plain,
( spl1_12
| spl1_4
| spl1_11 ),
inference(avatar_split_clause,[status(thm)],[f271,f111,f55,f115]) ).
thf(f115,definition,
( spl1_12
<=> ( $true
= ( epsoo @ epso @ sK5 ) ) ),
introduced(definition,[new_symbols(naming,[spl1_12])],[avatar_definition]) ).
thf(f55,definition,
( spl1_4
<=> ( ( epsoo @ epso )
= ( ^ [Y0: $o] : Y0 ) ) ),
introduced(definition,[new_symbols(naming,[spl1_4])],[avatar_definition]) ).
thf(f111,definition,
( spl1_11
<=> ( $true = sK5 ) ),
introduced(definition,[new_symbols(naming,[spl1_11])],[avatar_definition]) ).
thf(f271,plain,
( ( $true
= ( epsoo @ epso @ sK5 ) )
| spl1_4
| spl1_11 ),
inference(subsumption_resolution,[status(thm)],[f108,f112]) ).
thf(f112,plain,
( ( $true != sK5 )
| spl1_11 ),
inference(avatar_component_clause,[status(thm)],[f111]) ).
thf(f108,plain,
( ( $true
= ( epsoo @ epso @ sK5 ) )
| ( $true = sK5 )
| spl1_4 ),
inference(binary_proxy_clausification,[status(thm)],[f107]) ).
thf(f107,plain,
( ( sK5
!= ( epsoo @ epso @ sK5 ) )
| spl1_4 ),
inference(beta_eta_normalization,[status(thm)],[f106]) ).
thf(f106,plain,
( ( ( ^ [Y0: $o] : Y0
@ sK5 )
!= ( epsoo @ epso @ sK5 ) )
| spl1_4 ),
inference(negative_extensionality,[status(thm)],[f57]) ).
thf(f57,plain,
( ( ( epsoo @ epso )
!= ( ^ [Y0: $o] : Y0 ) )
| spl1_4 ),
inference(avatar_component_clause,[status(thm)],[f55]) ).
thf(f270,plain,
( spl1_9
| spl1_11
| ~ spl1_12
| spl1_19 ),
inference(avatar_contradiction_clause,[status(thm)],[f269]) ).
thf(f269,plain,
( $false
| spl1_9
| spl1_11
| ~ spl1_12
| spl1_19 ),
inference(subsumption_resolution,[status(thm)],[f268,f197]) ).
thf(f197,plain,
( ( $true != sK3 )
| spl1_19 ),
inference(avatar_component_clause,[status(thm)],[f195]) ).
thf(f268,plain,
( ( $true = sK3 )
| spl1_9
| spl1_11
| ~ spl1_12 ),
inference(subsumption_resolution,[status(thm)],[f206,f112]) ).
thf(f206,plain,
( ( $true = sK5 )
| ( $true = sK3 )
| spl1_9
| ~ spl1_12 ),
inference(binary_proxy_clausification,[status(thm)],[f205]) ).
thf(f205,plain,
( ( sK5 != sK3 )
| spl1_9
| ~ spl1_12 ),
inference(trivial_inequality_removal,[status(thm)],[f201]) ).
thf(f201,plain,
( ( sK5 != sK3 )
| ( $true != $true )
| spl1_9
| ~ spl1_12 ),
inference(constrained_superposition,[status(thm)],[f93,f117]) ).
thf(f117,plain,
( ( $true
= ( epsoo @ epso @ sK5 ) )
| ~ spl1_12 ),
inference(avatar_component_clause,[status(thm)],[f115]) ).
thf(f261,plain,
( ~ spl1_11
| ~ spl1_14 ),
inference(avatar_contradiction_clause,[status(thm)],[f260]) ).
thf(f260,plain,
( $false
| ~ spl1_11
| ~ spl1_14 ),
inference(trivial_inequality_removal,[status(thm)],[f259]) ).
thf(f259,plain,
( ( $true = $false )
| ~ spl1_11
| ~ spl1_14 ),
inference(backward_demodulation,[status(thm)],[f113,f126]) ).
thf(f126,plain,
( ( $false = sK5 )
| ~ spl1_14 ),
inference(avatar_component_clause,[status(thm)],[f124]) ).
thf(f124,definition,
( spl1_14
<=> ( $false = sK5 ) ),
introduced(definition,[new_symbols(naming,[spl1_14])],[avatar_definition]) ).
thf(f113,plain,
( ( $true = sK5 )
| ~ spl1_11 ),
inference(avatar_component_clause,[status(thm)],[f111]) ).
thf(f251,plain,
( ~ spl1_11
| ~ spl1_13
| ~ spl1_17 ),
inference(avatar_contradiction_clause,[status(thm)],[f250]) ).
thf(f250,plain,
( $false
| ~ spl1_11
| ~ spl1_13
| ~ spl1_17 ),
inference(subsumption_resolution,[status(thm)],[f237,f113]) ).
thf(f237,plain,
( ( $true != sK5 )
| ~ spl1_13
| ~ spl1_17 ),
inference(trivial_inequality_removal,[status(thm)],[f232]) ).
thf(f232,plain,
( ( $true = $false )
| ( $true != sK5 )
| ~ spl1_13
| ~ spl1_17 ),
inference(constrained_superposition,[status(thm)],[f160,f122]) ).
thf(f122,plain,
( ( $false
= ( epsoo @ epso @ sK5 ) )
| ~ spl1_13 ),
inference(avatar_component_clause,[status(thm)],[f120]) ).
thf(f120,definition,
( spl1_13
<=> ( $false
= ( epsoo @ epso @ sK5 ) ) ),
introduced(definition,[new_symbols(naming,[spl1_13])],[avatar_definition]) ).
thf(f160,plain,
( ( ( epsoo @ epso @ $true )
= $true )
| ~ spl1_17 ),
inference(avatar_component_clause,[status(thm)],[f158]) ).
thf(f188,plain,
( spl1_17
| ~ spl1_5
| ~ spl1_7 ),
inference(avatar_split_clause,[status(thm)],[f156,f73,f60,f158]) ).
thf(f73,definition,
( spl1_7
<=> ( ( epsoo @ epso @ ( epso @ ( epsoo @ epso ) ) )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl1_7])],[avatar_definition]) ).
thf(f156,plain,
( ( ( epsoo @ epso @ $true )
= $true )
| ~ spl1_5
| ~ spl1_7 ),
inference(backward_demodulation,[status(thm)],[f75,f62]) ).
thf(f62,plain,
( ( ( epso @ ( epsoo @ epso ) )
= $true )
| ~ spl1_5 ),
inference(avatar_component_clause,[status(thm)],[f60]) ).
thf(f75,plain,
( ( ( epsoo @ epso @ ( epso @ ( epsoo @ epso ) ) )
= $true )
| ~ spl1_7 ),
inference(avatar_component_clause,[status(thm)],[f73]) ).
thf(f187,plain,
( ~ spl1_8
| spl1_10 ),
inference(avatar_contradiction_clause,[status(thm)],[f186]) ).
thf(f186,plain,
( $false
| ~ spl1_8
| spl1_10 ),
inference(trivial_inequality_removal,[status(thm)],[f185]) ).
thf(f185,plain,
( ( $false != $false )
| ~ spl1_8
| spl1_10 ),
inference(superposition,[status(thm)],[f102,f78]) ).
thf(f78,plain,
( ! [X1: $o] :
( ( epsoo @ epso @ X1 )
= $false )
| ~ spl1_8 ),
inference(avatar_component_clause,[status(thm)],[f77]) ).
thf(f77,definition,
( spl1_8
<=> ! [X1: $o] :
( ( epsoo @ epso @ X1 )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl1_8])],[avatar_definition]) ).
thf(f102,plain,
( ( $false
!= ( epsoo @ epso @ sK4 ) )
| spl1_10 ),
inference(avatar_component_clause,[status(thm)],[f100]) ).
thf(f100,definition,
( spl1_10
<=> ( $false
= ( epsoo @ epso @ sK4 ) ) ),
introduced(definition,[new_symbols(naming,[spl1_10])],[avatar_definition]) ).
thf(f163,plain,
( spl1_13
| spl1_4
| spl1_14 ),
inference(avatar_split_clause,[status(thm)],[f162,f124,f55,f120]) ).
thf(f162,plain,
( ( $false
= ( epsoo @ epso @ sK5 ) )
| spl1_4
| spl1_14 ),
inference(subsumption_resolution,[status(thm)],[f109,f125]) ).
thf(f125,plain,
( ( $false != sK5 )
| spl1_14 ),
inference(avatar_component_clause,[status(thm)],[f124]) ).
thf(f109,plain,
( ( $false = sK5 )
| ( $false
= ( epsoo @ epso @ sK5 ) )
| spl1_4 ),
inference(binary_proxy_clausification,[status(thm)],[f107]) ).
thf(f149,plain,
~ spl1_1,
inference(avatar_contradiction_clause,[status(thm)],[f148]) ).
thf(f148,plain,
( $false
| ~ spl1_1 ),
inference(trivial_inequality_removal,[status(thm)],[f147]) ).
thf(f147,plain,
( ( $true = $false )
| ~ spl1_1 ),
inference(backward_demodulation,[status(thm)],[f31,f43]) ).
thf(f43,plain,
( ( ( sP0 @ $true )
= $false )
| ~ spl1_1 ),
inference(avatar_component_clause,[status(thm)],[f41]) ).
thf(f41,definition,
( spl1_1
<=> ( ( sP0 @ $true )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl1_1])],[avatar_definition]) ).
thf(f31,plain,
( ( sP0 @ $true )
= $true ),
inference(inequality_splitting,[status(thm)],[f26,f30]) ).
thf(f30,plain,
( ( sP0 @ ( q @ ( epsoo @ epso ) ) )
= $false ),
introduced(definition,[new_symbols(naming,[sP0])],[inequality_splitting_name_introduction]) ).
thf(f26,plain,
( ( q @ ( epsoo @ epso ) )
!= $true ),
inference(cnf_transformation,[status(thm)],[f21]) ).
thf(f21,plain,
( ( q @ ( epsoo @ epso ) )
!= $true ),
inference(flattening,[status(thm)],[f12]) ).
thf(f12,plain,
( ( q @ ( epsoo @ epso ) )
!= $true ),
inference(fool_elimination,[status(thm)],[f11]) ).
thf(f11,plain,
~ ( q @ ( epsoo @ epso ) ),
inference(rectify,[status(thm)],[f7]) ).
thf(f7,negated_conjecture,
~ ( q @ ( epsoo @ epso ) ),
inference(negated_conjecture,[status(cth)],[f6]) ).
thf(f6,conjecture,
q @ ( epsoo @ epso ),
file('/export/starexec/sandbox2/tmp/tmp.DQ9pP7ssFh/DTF2THF_21362.p',c) ).
thf(f135,plain,
~ spl1_4,
inference(avatar_contradiction_clause,[status(thm)],[f134]) ).
thf(f134,plain,
( $false
| ~ spl1_4 ),
inference(subsumption_resolution,[status(thm)],[f130,f28]) ).
thf(f28,plain,
( ( q
@ ^ [Y0: $o] : Y0 )
= $true ),
inference(cnf_transformation,[status(thm)],[f14]) ).
thf(f14,plain,
( ( q
@ ^ [Y0: $o] : Y0 )
= $true ),
inference(fool_elimination,[status(thm)],[f13]) ).
thf(f13,plain,
( q
@ ^ [X0: $o] : X0 ),
inference(rectify,[status(thm)],[f5]) ).
thf(f5,axiom,
( q
@ ^ [X1: $o] : X1 ),
file('/export/starexec/sandbox2/tmp/tmp.DQ9pP7ssFh/DTF2THF_21362.p',qid) ).
thf(f130,plain,
( ( ( q
@ ^ [Y0: $o] : Y0 )
!= $true )
| ~ spl1_4 ),
inference(backward_demodulation,[status(thm)],[f39,f56]) ).
thf(f56,plain,
( ( ( epsoo @ epso )
= ( ^ [Y0: $o] : Y0 ) )
| ~ spl1_4 ),
inference(avatar_component_clause,[status(thm)],[f55]) ).
thf(f39,plain,
( ( q @ ( epsoo @ epso ) )
!= $true ),
inference(trivial_inequality_removal,[status(thm)],[f37]) ).
thf(f37,plain,
( ( ( q @ ( epsoo @ epso ) )
!= $true )
| ( $true = $false ) ),
inference(constrained_superposition,[status(thm)],[f31,f30]) ).
thf(f103,plain,
( ~ spl1_10
| spl1_3 ),
inference(avatar_split_clause,[status(thm)],[f98,f50,f100]) ).
thf(f50,definition,
( spl1_3
<=> ( ( epsoo @ epso )
= ( ^ [Y0: $o] : $false ) ) ),
introduced(definition,[new_symbols(naming,[spl1_3])],[avatar_definition]) ).
thf(f98,plain,
( ( $false
!= ( epsoo @ epso @ sK4 ) )
| spl1_3 ),
inference(beta_eta_normalization,[status(thm)],[f97]) ).
thf(f97,plain,
( ( ( ^ [Y0: $o] : $false
@ sK4 )
!= ( epsoo @ epso @ sK4 ) )
| spl1_3 ),
inference(negative_extensionality,[status(thm)],[f52]) ).
thf(f52,plain,
( ( ( epsoo @ epso )
!= ( ^ [Y0: $o] : $false ) )
| spl1_3 ),
inference(avatar_component_clause,[status(thm)],[f50]) ).
thf(f94,plain,
( ~ spl1_9
| spl1_2 ),
inference(avatar_split_clause,[status(thm)],[f89,f45,f91]) ).
thf(f45,definition,
( spl1_2
<=> ( ( epsoo @ epso )
= ( ^ [Y0: $o] : $true ) ) ),
introduced(definition,[new_symbols(naming,[spl1_2])],[avatar_definition]) ).
thf(f89,plain,
( ( ( epsoo @ epso @ sK3 )
!= $true )
| spl1_2 ),
inference(beta_eta_normalization,[status(thm)],[f88]) ).
thf(f88,plain,
( ( ( epsoo @ epso @ sK3 )
!= ( ^ [Y0: $o] : $true
@ sK3 ) )
| spl1_2 ),
inference(negative_extensionality,[status(thm)],[f47]) ).
thf(f47,plain,
( ( ( epsoo @ epso )
!= ( ^ [Y0: $o] : $true ) )
| spl1_2 ),
inference(avatar_component_clause,[status(thm)],[f45]) ).
thf(f79,plain,
( spl1_7
| spl1_8 ),
inference(avatar_split_clause,[status(thm)],[f71,f77,f73]) ).
thf(f71,plain,
! [X1: $o] :
( ( ( epsoo @ epso @ X1 )
= $false )
| ( ( epsoo @ epso @ ( epso @ ( epsoo @ epso ) ) )
= $true ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f53,plain,
( spl1_1
| ~ spl1_3 ),
inference(avatar_split_clause,[status(thm)],[f34,f50,f41]) ).
thf(f34,plain,
( ( ( epsoo @ epso )
!= ( ^ [Y0: $o] : $false ) )
| ( ( sP0 @ $true )
= $false ) ),
inference(constrained_superposition,[status(thm)],[f30,f29]) ).
thf(f48,plain,
( spl1_1
| ~ spl1_2 ),
inference(avatar_split_clause,[status(thm)],[f35,f45,f41]) ).
thf(f35,plain,
( ( ( sP0 @ $true )
= $false )
| ( ( epsoo @ epso )
!= ( ^ [Y0: $o] : $true ) ) ),
inference(constrained_superposition,[status(thm)],[f30,f27]) ).
thf(f27,plain,
( ( q
@ ^ [Y0: $o] : $true )
= $true ),
inference(cnf_transformation,[status(thm)],[f10]) ).
thf(f10,plain,
( ( q
@ ^ [Y0: $o] : $true )
= $true ),
inference(fool_elimination,[status(thm)],[f9]) ).
thf(f9,plain,
( q
@ ^ [X0: $o] : $true ),
inference(rectify,[status(thm)],[f3]) ).
thf(f3,axiom,
( q
@ ^ [X1: $o] : $true ),
file('/export/starexec/sandbox2/tmp/tmp.DQ9pP7ssFh/DTF2THF_21362.p',qkt) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SYO560^1 : TPTP v9.2.1. Released v5.2.0.
% 0.12/0.12 % Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.15/0.33 % Computer : n027.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue Feb 24 14:34:07 EST 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.18/0.45 ---- Original DTF file ---
% 0.18/0.45 thf(spec,logic,$$dhol).
% 0.18/0.45 %------------------------------------------------------------------------------
% 0.18/0.45 % File : SYO560^1 : TPTP v9.2.1. Released v5.2.0.
% 0.18/0.45 % Domain : Syntactic
% 0.18/0.45 % Problem : Choice on $o>$o applied to choice on $o is identity or constant
% 0.18/0.45 % Version : Especial.
% 0.18/0.45 % English :
% 0.18/0.45
% 0.18/0.45 % Refs : [Bro11] Brown (2011), Email to Geoff Sutcliffe
% 0.18/0.45 % Source : [Bro11]
% 0.18/0.45 % Names : CHOICE3 [Bro11]
% 0.18/0.45
% 0.18/0.45 % Status : Theorem
% 0.18/0.45 % Rating : 0.25 v8.2.0, 0.27 v8.1.0, 0.33 v7.5.0, 0.42 v7.4.0, 0.33 v7.3.0, 0.30 v7.2.0, 0.38 v7.1.0, 0.43 v7.0.0, 0.38 v6.4.0, 0.43 v6.3.0, 0.50 v6.2.0, 0.67 v6.0.0, 0.50 v5.5.0, 0.40 v5.4.0, 0.75 v5.2.0
% 0.18/0.45 % Syntax : Number of formulae : 9 ( 3 unt; 3 typ; 0 def)
% 0.18/0.45 % Number of atoms : 10 ( 0 equ; 0 cnn)
% 0.18/0.45 % Maximal formula atoms : 3 ( 1 avg)
% 0.18/0.45 % Number of connectives : 13 ( 0 ~; 0 |; 0 &; 11 @)
% 0.18/0.45 % ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% 0.18/0.45 % Maximal formula depth : 5 ( 4 avg)
% 0.18/0.45 % Number of types : 1 ( 0 usr)
% 0.18/0.45 % Number of type conns : 12 ( 12 >; 0 *; 0 +; 0 <<)
% 0.18/0.45 % Number of symbols : 5 ( 3 usr; 2 con; 0-2 aty)
% 0.18/0.45 % Number of variables : 7 ( 3 ^; 2 !; 2 ?; 7 :)
% 0.18/0.45 % SPC : TH0_THM_NEQ_NAR
% 0.18/0.45
% 0.18/0.45 % Comments : Assume epso and epsoo are choice operators on $o and $o>$o,
% 0.18/0.45 % respectively. epso can also be viewed as a predicate on $o>$o,
% 0.18/0.45 % so we can apply epsoo to epso. The term (epsoo @ epso) is of
% 0.18/0.45 % type $o>$o, and cannot be negation. If a predicate q is true for
% 0.18/0.45 % all the other three functions in $o>$o, then q is true for
% 0.18/0.45 % (epsoo @ epso). Proof Sketch: If the conjecture were not true,
% 0.18/0.45 % then (epsoo @ epso) would be the negation function. However,
% 0.18/0.45 % negation is the only function $o>$o for which we are certain
% 0.18/0.45 % epso returns $false.
% 0.18/0.45 %------------------------------------------------------------------------------
% 0.28/0.45 thf(epso,type,
% 0.28/0.45 epso: ( $o > $o ) > $o ).
% 0.28/0.45
% 0.28/0.45 thf(choiceaxo,axiom,
% 0.28/0.45 ! [P: $o > $o] :
% 0.28/0.45 ( ? [X: $o] : ( P @ X )
% 0.28/0.45 => ( P @ ( epso @ P ) ) ) ).
% 0.28/0.45
% 0.28/0.45 thf(epsoo,type,
% 0.28/0.45 epsoo: ( ( $o > $o ) > $o ) > $o > $o ).
% 0.28/0.45
% 0.28/0.45 thf(choiceaxoo,axiom,
% 0.28/0.45 ! [P: ( $o > $o ) > $o] :
% 0.28/0.45 ( ? [X: $o > $o] : ( P @ X )
% 0.28/0.45 => ( P @ ( epsoo @ P ) ) ) ).
% 0.28/0.45
% 0.28/0.45 thf(q,type,
% 0.28/0.45 q: ( $o > $o ) > $o ).
% 0.28/0.45
% 0.28/0.45 thf(qkt,axiom,
% 0.28/0.45 ( q
% 0.28/0.45 @ ^ [X: $o] : $true ) ).
% 0.28/0.45
% 0.28/0.45 thf(qkf,axiom,
% 0.28/0.45 ( q
% 0.28/0.45 @ ^ [X: $o] : $false ) ).
% 0.28/0.45
% 0.28/0.45 thf(qid,axiom,
% 0.28/0.45 ( q
% 0.28/0.45 @ ^ [X: $o] : X ) ).
% 0.28/0.45
% 0.28/0.45 thf(c,conjecture,
% 0.28/0.45 q @ ( epsoo @ epso ) ).
% 0.28/0.45
% 0.28/0.45 %------------------------------------------------------------------------------
% 0.28/0.45 ------------------------
% 1.50/1.26 ---- Embedded in THF ---
% 1.50/1.26 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.50/1.26 %%% Generated on Tue Feb 24 14:34:08 EST 2026
% 1.50/1.26 %%% using '$$dhol' embedding, version 1.3.0.
% 1.50/1.26 %%% Logic specification used:
% 1.50/1.26 %%% thf(spec, logic, $$dhol).
% 1.50/1.26
% 1.50/1.26 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.DQ9pP7ssFh/DTF2DTF21362.p
% See solution above
% 1.50/1.26 ------------------------
% 1.50/1.27 ---- Cleaned THF ---
% 1.50/1.27 thf(epso,type,
% 1.50/1.27 epso: ( $o > $o ) > $o ).
% 1.50/1.27
% 1.50/1.27 thf(choiceaxo,axiom,
% 1.50/1.27 ! [P: $o > $o] :
% 1.50/1.27 ( ? [X: $o] : ( P @ X )
% 1.50/1.27 => ( P @ ( epso @ P ) ) ) ).
% 1.50/1.27
% 1.50/1.27 thf(epsoo,type,
% 1.50/1.27 epsoo: ( ( $o > $o ) > $o ) > $o > $o ).
% 1.50/1.27
% 1.50/1.27 thf(choiceaxoo,axiom,
% 1.50/1.27 ! [P: ( $o > $o ) > $o] :
% 1.50/1.27 ( ? [X: $o > $o] : ( P @ X )
% 1.50/1.27 => ( P @ ( epsoo @ P ) ) ) ).
% 1.50/1.27
% 1.50/1.27 thf(q,type,
% 1.50/1.27 q: ( $o > $o ) > $o ).
% 1.50/1.27
% 1.50/1.27 thf(qkt,axiom,
% 1.50/1.27 ( q
% 1.50/1.27 @ ^ [X: $o] : $true ) ).
% 1.50/1.27
% 1.50/1.27 thf(qkf,axiom,
% 1.50/1.27 ( q
% 1.50/1.27 @ ^ [X: $o] : $false ) ).
% 1.50/1.27
% 1.50/1.27 thf(qid,axiom,
% 1.50/1.27 ( q
% 1.50/1.27 @ ^ [X: $o] : X ) ).
% 1.50/1.27
% 1.50/1.27 thf(c,conjecture,
% 1.50/1.27 q @ ( epsoo @ epso ) ).
% 1.50/1.27 ------------------------
% 1.50/1.29 % (21479)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_21362 for (2999ds/27Mi)
% 1.50/1.29 % (21479)Refutation not found, incomplete strategy
% 1.50/1.29 % (21479)------------------------------
% 1.50/1.29 % (21479)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.50/1.29 % (21479)Termination reason: Refutation not found, incomplete strategy
% 1.50/1.29
% 1.50/1.29
% 1.50/1.29 % (21479)Memory used [KB]: 5500
% 1.50/1.29 % (21479)Time elapsed: 0.002 s
% 1.50/1.29 % (21479)Instructions burned: 2 (million)
% 1.50/1.29 % (21479)------------------------------
% 1.50/1.29 % (21479)------------------------------
% 1.50/1.29 % (21477)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/183Mi)
% 1.50/1.29 % (21478)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_21362 for (2999ds/4Mi)
% 1.50/1.29 % (21481)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_21362 for (2999ds/2Mi)
% 1.50/1.29 % (21483)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/18Mi)
% 1.50/1.29 % (21482)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_21362 for (2999ds/275Mi)
% 1.50/1.29 % (21480)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/2Mi)
% 1.50/1.29 % (21481)Instruction limit reached!
% 1.50/1.29 % (21481)------------------------------
% 1.50/1.29 % (21481)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.50/1.29 % (21481)Termination reason: Unknown
% 1.50/1.29 % (21481)Termination phase: Saturation
% 1.50/1.29
% 1.50/1.29 % (21481)Memory used [KB]: 895
% 1.50/1.29 % (21481)Time elapsed: 0.003 s
% 1.50/1.29 % (21481)Instructions burned: 2 (million)
% 1.50/1.29 % (21481)------------------------------
% 1.50/1.29 % (21481)------------------------------
% 1.50/1.30 % (21482)Refutation not found, incomplete strategy
% 1.50/1.30 % (21482)------------------------------
% 1.50/1.30 % (21482)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.50/1.30 % (21482)Termination reason: Refutation not found, incomplete strategy
% 1.50/1.30
% 1.50/1.30
% 1.50/1.30 % (21482)Memory used [KB]: 5500
% 1.50/1.30 % (21482)Time elapsed: 0.003 s
% 1.50/1.30 % (21482)Instructions burned: 1 (million)
% 1.50/1.30 % (21482)------------------------------
% 1.50/1.30 % (21482)------------------------------
% 1.50/1.30 % (21480)Instruction limit reached!
% 1.50/1.30 % (21480)------------------------------
% 1.50/1.30 % (21480)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.50/1.30 % (21480)Termination reason: Unknown
% 1.50/1.30 % (21480)Termination phase: Saturation
% 1.50/1.30
% 1.50/1.30 % (21480)Memory used [KB]: 5500
% 1.50/1.30 % (21480)Time elapsed: 0.003 s
% 1.50/1.30 % (21480)Instructions burned: 2 (million)
% 1.50/1.30 % (21480)------------------------------
% 1.50/1.30 % (21480)------------------------------
% 1.62/1.30 % (21478)Instruction limit reached!
% 1.62/1.30 % (21478)------------------------------
% 1.62/1.30 % (21478)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.30 % (21478)Termination reason: Unknown
% 1.62/1.30 % (21478)Termination phase: Saturation
% 1.62/1.30
% 1.62/1.30 % (21478)Memory used [KB]: 5500
% 1.62/1.30 % (21478)Time elapsed: 0.005 s
% 1.62/1.30 % (21478)Instructions burned: 4 (million)
% 1.62/1.30 % (21478)------------------------------
% 1.62/1.30 % (21478)------------------------------
% 1.62/1.30 % (21484)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/3Mi)
% 1.62/1.30 % (21484)Instruction limit reached!
% 1.62/1.30 % (21484)------------------------------
% 1.62/1.30 % (21484)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.30 % (21484)Termination reason: Unknown
% 1.62/1.30 % (21484)Termination phase: Saturation
% 1.62/1.30
% 1.62/1.30 % (21484)Memory used [KB]: 5500
% 1.62/1.30 % (21484)Time elapsed: 0.002 s
% 1.62/1.30 % (21484)Instructions burned: 3 (million)
% 1.62/1.30 % (21484)------------------------------
% 1.62/1.30 % (21484)------------------------------
% 1.62/1.31 % (21483)Instruction limit reached!
% 1.62/1.31 % (21483)------------------------------
% 1.62/1.31 % (21483)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.31 % (21483)Termination reason: Unknown
% 1.62/1.31 % (21483)Termination phase: Saturation
% 1.62/1.31
% 1.62/1.31 % (21483)Memory used [KB]: 5628
% 1.62/1.31 % (21483)Time elapsed: 0.014 s
% 1.62/1.31 % (21483)Instructions burned: 18 (million)
% 1.62/1.31 % (21483)------------------------------
% 1.62/1.31 % (21483)------------------------------
% 1.62/1.31 % (21485)lrs+1002_1:1_cnfonf=lazy_not_be_gen:hud=14:prag=on:sp=weighted_frequency:tnu=1:i=37:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/37Mi)
% 1.62/1.31 % (21487)dis+21_1:1_cbe=off:cnfonf=off:fs=off:fsr=off:hud=1:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/3Mi)
% 1.62/1.31 % (21488)lrs+1002_1:1_aac=none:au=on:cnfonf=lazy_gen:plsq=on:plsqc=1:plsqr=4203469,65536:i=1041:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/1041Mi)
% 1.62/1.31 % (21489)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/7Mi)
% 1.62/1.32 % (21486)lrs+2_16:1_acc=model:au=on:bd=off:c=on:e2e=on:nm=2:sos=all:i=15:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/15Mi)
% 1.62/1.32 % (21487)Instruction limit reached!
% 1.62/1.32 % (21487)------------------------------
% 1.62/1.32 % (21487)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.32 % (21487)Termination reason: Unknown
% 1.62/1.32 % (21487)Termination phase: Saturation
% 1.62/1.32
% 1.62/1.32 % (21487)Memory used [KB]: 5500
% 1.62/1.32 % (21487)Time elapsed: 0.004 s
% 1.62/1.32 % (21487)Instructions burned: 3 (million)
% 1.62/1.32 % (21487)------------------------------
% 1.62/1.32 % (21487)------------------------------
% 1.62/1.32 % (21486)Refutation not found, incomplete strategy
% 1.62/1.32 % (21486)------------------------------
% 1.62/1.32 % (21486)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.32 % (21486)Termination reason: Refutation not found, incomplete strategy
% 1.62/1.32
% 1.62/1.32
% 1.62/1.32 % (21486)Memory used [KB]: 5500
% 1.62/1.32 % (21486)Time elapsed: 0.003 s
% 1.62/1.32 % (21486)Instructions burned: 2 (million)
% 1.62/1.32 % (21486)------------------------------
% 1.62/1.32 % (21486)------------------------------
% 1.62/1.32 % (21489)Instruction limit reached!
% 1.62/1.32 % (21489)------------------------------
% 1.62/1.32 % (21489)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.32 % (21489)Termination reason: Unknown
% 1.62/1.32 % (21489)Termination phase: Saturation
% 1.62/1.32
% 1.62/1.32 % (21489)Memory used [KB]: 1023
% 1.62/1.32 % (21489)Time elapsed: 0.006 s
% 1.62/1.32 % (21489)Instructions burned: 8 (million)
% 1.62/1.32 % (21489)------------------------------
% 1.62/1.32 % (21489)------------------------------
% 1.62/1.32 % (21490)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/16Mi)
% 1.62/1.33 % (21493)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/7Mi)
% 1.62/1.33 % (21493)Refutation not found, incomplete strategy
% 1.62/1.33 % (21493)------------------------------
% 1.62/1.33 % (21493)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.33 % (21493)Termination reason: Refutation not found, incomplete strategy
% 1.62/1.33
% 1.62/1.33
% 1.62/1.33 % (21493)Memory used [KB]: 5500
% 1.62/1.33 % (21493)Time elapsed: 0.003 s
% 1.62/1.33 % (21493)Instructions burned: 5 (million)
% 1.62/1.33 % (21493)------------------------------
% 1.62/1.33 % (21493)------------------------------
% 1.62/1.33 % (21491)lrs+21_1:1_au=on:cnfonf=off:fd=preordered:fe=off:fsr=off:hud=11:inj=on:kws=precedence:s2pl=no:sp=weighted_frequency:tgt=full:i=3:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/3Mi)
% 1.62/1.33 % (21490)Instruction limit reached!
% 1.62/1.33 % (21490)------------------------------
% 1.62/1.33 % (21490)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.33 % (21490)Termination reason: Unknown
% 1.62/1.33 % (21490)Termination phase: Saturation
% 1.62/1.33
% 1.62/1.33 % (21490)Memory used [KB]: 5628
% 1.62/1.33 % (21490)Time elapsed: 0.013 s
% 1.62/1.33 % (21490)Instructions burned: 17 (million)
% 1.62/1.33 % (21490)------------------------------
% 1.62/1.33 % (21490)------------------------------
% 1.62/1.33 % (21492)lrs+2_1:1_apa=on:au=on:bd=preordered:cnfonf=off:cs=on:ixr=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/3Mi)
% 1.62/1.33 % (21491)Instruction limit reached!
% 1.62/1.33 % (21491)------------------------------
% 1.62/1.33 % (21491)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.33 % (21491)Termination reason: Unknown
% 1.62/1.34 % (21491)Termination phase: Saturation
% 1.62/1.34
% 1.62/1.34 % (21491)Memory used [KB]: 5500
% 1.62/1.34 % (21491)Time elapsed: 0.004 s
% 1.62/1.34 % (21491)Instructions burned: 3 (million)
% 1.62/1.34 % (21491)------------------------------
% 1.62/1.34 % (21491)------------------------------
% 1.62/1.34 % (21485)Instruction limit reached!
% 1.62/1.34 % (21485)------------------------------
% 1.62/1.34 % (21485)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.34 % (21485)Termination reason: Unknown
% 1.62/1.34 % (21485)Termination phase: Saturation
% 1.62/1.34
% 1.62/1.34 % (21485)Memory used [KB]: 5756
% 1.62/1.34 % (21485)Time elapsed: 0.025 s
% 1.62/1.34 % (21485)Instructions burned: 38 (million)
% 1.62/1.34 % (21485)------------------------------
% 1.62/1.34 % (21485)------------------------------
% 1.62/1.34 % (21492)Instruction limit reached!
% 1.62/1.34 % (21492)------------------------------
% 1.62/1.34 % (21492)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.34 % (21492)Termination reason: Unknown
% 1.62/1.34 % (21492)Termination phase: Saturation
% 1.62/1.34
% 1.62/1.34 % (21492)Memory used [KB]: 1023
% 1.62/1.34 % (21492)Time elapsed: 0.004 s
% 1.62/1.34 % (21492)Instructions burned: 3 (million)
% 1.62/1.34 % (21492)------------------------------
% 1.62/1.34 % (21492)------------------------------
% 1.62/1.34 % (21494)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/3Mi)
% 1.62/1.34 % (21494)Instruction limit reached!
% 1.62/1.34 % (21494)------------------------------
% 1.62/1.34 % (21494)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.34 % (21494)Termination reason: Unknown
% 1.62/1.34 % (21494)Termination phase: Saturation
% 1.62/1.34
% 1.62/1.34 % (21494)Memory used [KB]: 5500
% 1.62/1.34 % (21494)Time elapsed: 0.002 s
% 1.62/1.34 % (21494)Instructions burned: 3 (million)
% 1.62/1.34 % (21494)------------------------------
% 1.62/1.34 % (21494)------------------------------
% 1.62/1.35 % (21499)dis+1002_5:1_au=on:bd=off:e2e=on:fde=none:fs=off:fsr=off:sos=on:i=902:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/902Mi)
% 1.62/1.35 % (21499)Refutation not found, incomplete strategy
% 1.62/1.35 % (21499)------------------------------
% 1.62/1.35 % (21499)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.35 % (21499)Termination reason: Refutation not found, incomplete strategy
% 1.62/1.35
% 1.62/1.35
% 1.62/1.35 % (21499)Memory used [KB]: 5500
% 1.62/1.35 % (21499)Time elapsed: 0.001 s
% 1.62/1.35 % (21499)Instructions burned: 1 (million)
% 1.62/1.35 % (21496)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/18Mi)
% 1.62/1.35 % (21499)------------------------------
% 1.62/1.35 % (21499)------------------------------
% 1.62/1.35 % (21495)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/4Mi)
% 1.62/1.35 % (21496)Refutation not found, incomplete strategy
% 1.62/1.35 % (21496)------------------------------
% 1.62/1.35 % (21496)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.35 % (21496)Termination reason: Refutation not found, incomplete strategy
% 1.62/1.35
% 1.62/1.35
% 1.62/1.35 % (21496)Memory used [KB]: 5500
% 1.62/1.35 % (21496)Time elapsed: 0.004 s
% 1.62/1.35 % (21496)Instructions burned: 3 (million)
% 1.62/1.35 % (21496)------------------------------
% 1.62/1.35 % (21496)------------------------------
% 1.62/1.35 % (21497)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/710Mi)
% 1.62/1.35 % (21498)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/6Mi)
% 1.62/1.35 % (21495)Instruction limit reached!
% 1.62/1.35 % (21495)------------------------------
% 1.62/1.35 % (21495)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.36 % (21495)Termination reason: Unknown
% 1.62/1.36 % (21495)Termination phase: Saturation
% 1.62/1.36
% 1.62/1.36 % (21495)Memory used [KB]: 5500
% 1.62/1.36 % (21495)Time elapsed: 0.005 s
% 1.62/1.36 % (21495)Instructions burned: 5 (million)
% 1.62/1.36 % (21495)------------------------------
% 1.62/1.36 % (21495)------------------------------
% 1.62/1.36 % (21498)Refutation not found, incomplete strategy
% 1.62/1.36 % (21498)------------------------------
% 1.62/1.36 % (21498)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.36 % (21498)Termination reason: Refutation not found, incomplete strategy
% 1.62/1.36
% 1.62/1.36
% 1.62/1.36 % (21498)Memory used [KB]: 5500
% 1.62/1.36 % (21498)Time elapsed: 0.006 s
% 1.62/1.36 % (21498)Instructions burned: 5 (million)
% 1.62/1.36 % (21498)------------------------------
% 1.62/1.36 % (21498)------------------------------
% 1.62/1.36 % (21500)dis+21_1:8_apa=on:cnfonf=off:fd=off:fsr=off:hud=0:ins=1:kws=inv_frequency:nwc=10.0:ss=axioms:st=5.0:i=21:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/21Mi)
% 1.62/1.36 % (21501)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/5Mi)
% 1.62/1.37 % (21501)Instruction limit reached!
% 1.62/1.37 % (21501)------------------------------
% 1.62/1.37 % (21501)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.37 % (21501)Termination reason: Unknown
% 1.62/1.37 % (21501)Termination phase: Saturation
% 1.62/1.37
% 1.62/1.37 % (21501)Memory used [KB]: 5500
% 1.62/1.37 % (21501)Time elapsed: 0.004 s
% 1.62/1.37 % (21501)Instructions burned: 6 (million)
% 1.62/1.37 % (21501)------------------------------
% 1.62/1.37 % (21501)------------------------------
% 1.62/1.37 % (21500)Instruction limit reached!
% 1.62/1.37 % (21500)------------------------------
% 1.62/1.37 % (21500)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.37 % (21500)Termination reason: Unknown
% 1.62/1.37 % (21500)Termination phase: Saturation
% 1.62/1.37
% 1.62/1.37 % (21500)Memory used [KB]: 5756
% 1.62/1.37 % (21500)Time elapsed: 0.008 s
% 1.62/1.37 % (21500)Instructions burned: 21 (million)
% 1.62/1.37 % (21500)------------------------------
% 1.62/1.37 % (21500)------------------------------
% 1.62/1.37 % (21502)lrs+2_1:1_cnfonf=lazy_not_gen_be_off:cs=on:fe=off:hud=10:inj=on:ins=3:plsq=on:plsqc=1:sd=10:ss=axioms:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/6Mi)
% 1.62/1.37 % (21502)Instruction limit reached!
% 1.62/1.37 % (21502)------------------------------
% 1.62/1.37 % (21502)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.37 % (21502)Termination reason: Unknown
% 1.62/1.37 % (21502)Termination phase: Saturation
% 1.62/1.37
% 1.62/1.37 % (21502)Memory used [KB]: 5500
% 1.62/1.37 % (21502)Time elapsed: 0.004 s
% 1.62/1.37 % (21502)Instructions burned: 7 (million)
% 1.62/1.37 % (21502)------------------------------
% 1.62/1.37 % (21502)------------------------------
% 1.62/1.37 % (21477)Instruction limit reached!
% 1.62/1.37 % (21477)------------------------------
% 1.62/1.37 % (21477)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.37 % (21477)Termination reason: Unknown
% 1.62/1.37 % (21477)Termination phase: Saturation
% 1.62/1.37
% 1.62/1.37 % (21477)Memory used [KB]: 6908
% 1.62/1.37 % (21477)Time elapsed: 0.080 s
% 1.62/1.37 % (21477)Instructions burned: 184 (million)
% 1.62/1.37 % (21477)------------------------------
% 1.62/1.37 % (21477)------------------------------
% 1.62/1.38 % (21504)dis+1010_1:4_atotf=0.2:c=on:cbe=off:cnfonf=lazy_simp:fe=off:ins=2:ntd=on:s2a=on:s2at=5.0:sgt=5:ss=axioms:st=1.5:i=779:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/779Mi)
% 1.62/1.38 % (21505)lrs+10_1:1_cnfonf=lazy_not_be_gen:ntd=on:sp=const_min:ss=axioms:sup=off:i=19:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/19Mi)
% 1.62/1.38 % (21503)lrs+1002_1:128_au=on:c=on:fsr=off:piset=equals:i=377:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/377Mi)
% 1.62/1.38 % (21506)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=879:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/879Mi)
% 1.62/1.38 % (21507)dis+1002_1:128_acc=on:er=filter:i=17:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/17Mi)
% 1.62/1.38 % (21505)Instruction limit reached!
% 1.62/1.38 % (21505)------------------------------
% 1.62/1.38 % (21505)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.38 % (21505)Termination reason: Unknown
% 1.62/1.38 % (21505)Termination phase: Saturation
% 1.62/1.38
% 1.62/1.38 % (21505)Memory used [KB]: 5628
% 1.62/1.38 % (21505)Time elapsed: 0.008 s
% 1.62/1.38 % (21505)Instructions burned: 22 (million)
% 1.62/1.38 % (21505)------------------------------
% 1.62/1.38 % (21505)------------------------------
% 1.62/1.39 % (21507)Instruction limit reached!
% 1.62/1.39 % (21507)------------------------------
% 1.62/1.39 % (21507)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.39 % (21507)Termination reason: Unknown
% 1.62/1.39 % (21507)Termination phase: Saturation
% 1.62/1.39
% 1.62/1.39 % (21507)Memory used [KB]: 5628
% 1.62/1.39 % (21507)Time elapsed: 0.031 s
% 1.62/1.39 % (21507)Instructions burned: 19 (million)
% 1.62/1.39 % (21507)------------------------------
% 1.62/1.39 % (21507)------------------------------
% 1.62/1.39 % (21508)ott+21_1:1_apa=on:au=on:cnfonf=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/3Mi)
% 1.62/1.39 % (21508)Instruction limit reached!
% 1.62/1.39 % (21508)------------------------------
% 1.62/1.39 % (21508)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.39 % (21508)Termination reason: Unknown
% 1.62/1.39 % (21508)Termination phase: Saturation
% 1.62/1.39
% 1.62/1.39 % (21508)Memory used [KB]: 5500
% 1.62/1.39 % (21508)Time elapsed: 0.002 s
% 1.62/1.39 % (21508)Instructions burned: 4 (million)
% 1.62/1.39 % (21508)------------------------------
% 1.62/1.39 % (21508)------------------------------
% 1.62/1.40 % (21509)lrs+1010_1:8_cnfonf=off:hud=1:inj=on:tnu=5:i=30:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/30Mi)
% 1.62/1.40 % (21510)dis+10_1:1_ixr=off:plsq=on:plsqc=1:plsqr=32,1:s2a=on:i=127:si=on:rtra=on_0 on DTF2THF_21362 for (2999ds/127Mi)
% 1.62/1.41 % (21509)Instruction limit reached!
% 1.62/1.41 % (21509)------------------------------
% 1.62/1.41 % (21509)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.41 % (21509)Termination reason: Unknown
% 1.62/1.41 % (21509)Termination phase: Saturation
% 1.62/1.41
% 1.62/1.41 % (21509)Memory used [KB]: 5628
% 1.62/1.41 % (21509)Time elapsed: 0.036 s
% 1.62/1.41 % (21509)Instructions burned: 31 (million)
% 1.62/1.41 % (21509)------------------------------
% 1.62/1.41 % (21509)------------------------------
% 1.62/1.42 % (21511)lrs+1002_1:1_au=on:cbe=off:cnfonf=conj_eager:cond=on:hi=on:i=100:si=on:rtra=on_0 on DTF2THF_21362 for (2998ds/100Mi)
% 1.62/1.42 % (21511)Refutation not found, incomplete strategy
% 1.62/1.42 % (21511)------------------------------
% 1.62/1.42 % (21511)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.42 % (21511)Termination reason: Refutation not found, incomplete strategy
% 1.62/1.42
% 1.62/1.42
% 1.62/1.42 % (21511)Memory used [KB]: 5500
% 1.62/1.42 % (21511)Time elapsed: 0.003 s
% 1.62/1.42 % (21511)Instructions burned: 3 (million)
% 1.62/1.42 % (21511)------------------------------
% 1.62/1.42 % (21511)------------------------------
% 1.62/1.43 % (21512)dis+10_1:1_anc=none:cnfonf=lazy_gen:fd=preordered:fe=off:hud=10:ins=3:ixr=off:nwc=5.0:plsq=on:plsqc=1:plsqr=32,1:sp=const_frequency:uhcvi=on:i=3:si=on:rtra=on_0 on DTF2THF_21362 for (2998ds/3Mi)
% 1.62/1.43 % (21512)Instruction limit reached!
% 1.62/1.43 % (21512)------------------------------
% 1.62/1.43 % (21512)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.43 % (21512)Termination reason: Unknown
% 1.62/1.43 % (21512)Termination phase: Saturation
% 1.62/1.43
% 1.62/1.43 % (21512)Memory used [KB]: 5500
% 1.62/1.43 % (21512)Time elapsed: 0.003 s
% 1.62/1.43 % (21512)Instructions burned: 3 (million)
% 1.62/1.43 % (21512)------------------------------
% 1.62/1.43 % (21512)------------------------------
% 1.62/1.44 % (21510)Instruction limit reached!
% 1.62/1.44 % (21510)------------------------------
% 1.62/1.44 % (21510)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.44 % (21510)Termination reason: Unknown
% 1.62/1.44 % (21510)Termination phase: Saturation
% 1.62/1.44
% 1.62/1.44 % (21510)Memory used [KB]: 6012
% 1.62/1.44 % (21510)Time elapsed: 0.065 s
% 1.62/1.44 % (21510)Instructions burned: 129 (million)
% 1.62/1.44 % (21510)------------------------------
% 1.62/1.44 % (21510)------------------------------
% 1.62/1.44 % (21513)lrs+10_8:1_au=on:avsq=on:e2e=on:ins=3:s2a=on:s2at=3.0:ss=axioms:i=20:si=on:rtra=on_0 on DTF2THF_21362 for (2998ds/20Mi)
% 1.62/1.45 % (21513)Instruction limit reached!
% 1.62/1.45 % (21513)------------------------------
% 1.62/1.45 % (21513)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.45 % (21513)Termination reason: Unknown
% 1.62/1.45 % (21513)Termination phase: Saturation
% 1.62/1.45
% 1.62/1.45 % (21513)Memory used [KB]: 5628
% 1.62/1.45 % (21513)Time elapsed: 0.035 s
% 1.62/1.45 % (21513)Instructions burned: 22 (million)
% 1.62/1.45 % (21513)------------------------------
% 1.62/1.45 % (21513)------------------------------
% 1.62/1.45 % (21514)dis+1002_1:1_cbe=off:hud=5:nm=4:plsq=on:plsqr=7,1:prag=on:sp=const_max:tnu=1:i=86:si=on:rtra=on_0 on DTF2THF_21362 for (2998ds/86Mi)
% 1.62/1.46 % (21515)lrs+1010_1:1_au=on:cbe=off:nm=2:ntd=on:sd=2:ss=axioms:st=5.0:i=107:si=on:rtra=on_0 on DTF2THF_21362 for (2998ds/107Mi)
% 1.62/1.46 % (21515)Refutation not found, incomplete strategy
% 1.62/1.46 % (21515)------------------------------
% 1.62/1.46 % (21515)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.46 % (21515)Termination reason: Refutation not found, incomplete strategy
% 1.62/1.46
% 1.62/1.46
% 1.62/1.46 % (21515)Memory used [KB]: 5500
% 1.62/1.46 % (21515)Time elapsed: 0.003 s
% 1.62/1.46 % (21515)Instructions burned: 3 (million)
% 1.62/1.46 % (21515)------------------------------
% 1.62/1.46 % (21515)------------------------------
% 1.62/1.47 % (21516)lrs+2_1:1024_cnfonf=lazy_gen:fe=off:hud=15:plsq=on:plsqc=1:plsqr=32,1:i=39:si=on:rtra=on_0 on DTF2THF_21362 for (2998ds/39Mi)
% 1.62/1.48 % (21514)Instruction limit reached!
% 1.62/1.48 % (21514)------------------------------
% 1.62/1.48 % (21514)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.48 % (21514)Termination reason: Unknown
% 1.62/1.48 % (21514)Termination phase: Saturation
% 1.62/1.48
% 1.62/1.48 % (21514)Memory used [KB]: 6140
% 1.62/1.48 % (21514)Time elapsed: 0.053 s
% 1.62/1.48 % (21514)Instructions burned: 88 (million)
% 1.62/1.48 % (21514)------------------------------
% 1.62/1.48 % (21514)------------------------------
% 1.62/1.49 % (21516)Instruction limit reached!
% 1.62/1.49 % (21516)------------------------------
% 1.62/1.49 % (21516)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.49 % (21516)Termination reason: Unknown
% 1.62/1.49 % (21516)Termination phase: Saturation
% 1.62/1.49
% 1.62/1.49 % (21516)Memory used [KB]: 5884
% 1.62/1.49 % (21516)Time elapsed: 0.014 s
% 1.62/1.49 % (21516)Instructions burned: 39 (million)
% 1.62/1.49 % (21516)------------------------------
% 1.62/1.49 % (21516)------------------------------
% 1.62/1.49 % (21517)dis+10_1:1_cnfonf=lazy_not_gen:fsr=off:kws=precedence:nwc=5.0:s2a=on:ss=axioms:st=1.5:i=448:si=on:rtra=on_0 on DTF2THF_21362 for (2997ds/448Mi)
% 1.62/1.50 % (21518)lrs+10_1:512_au=on:fde=unused:lma=on:nm=32:plsq=on:plsqc=1:plsqr=16121663,131072:sfv=off:sp=const_max:ss=axioms:st=3.0:tgt=full:i=46:si=on:rtra=on_0 on DTF2THF_21362 for (2997ds/46Mi)
% 1.62/1.51 % (21518)Instruction limit reached!
% 1.62/1.51 % (21518)------------------------------
% 1.62/1.51 % (21518)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.51 % (21518)Termination reason: Unknown
% 1.62/1.51 % (21518)Termination phase: Saturation
% 1.62/1.51
% 1.62/1.51 % (21518)Memory used [KB]: 5628
% 1.62/1.51 % (21518)Time elapsed: 0.019 s
% 1.62/1.51 % (21518)Instructions burned: 48 (million)
% 1.62/1.51 % (21518)------------------------------
% 1.62/1.51 % (21518)------------------------------
% 1.62/1.51 % (21503)Instruction limit reached!
% 1.62/1.51 % (21503)------------------------------
% 1.62/1.51 % (21503)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.51 % (21503)Termination reason: Unknown
% 1.62/1.51 % (21503)Termination phase: Saturation
% 1.62/1.51
% 1.62/1.51 % (21503)Memory used [KB]: 6140
% 1.62/1.51 % (21503)Time elapsed: 0.140 s
% 1.62/1.51 % (21503)Instructions burned: 378 (million)
% 1.62/1.51 % (21503)------------------------------
% 1.62/1.51 % (21503)------------------------------
% 1.62/1.52 % (21519)lrs+10_1:10_au=on:av=off:cbe=off:cnfonf=lazy_pi_sigma_gen:ntd=on:plsq=on:plsqc=1:plsqr=32,1:i=98:si=on:rtra=on_0 on DTF2THF_21362 for (2997ds/98Mi)
% 1.62/1.53 % (21520)ott+1002_1:1_apa=on:au=on:bd=off:cnfonf=off:fd=off:sos=on:sp=weighted_frequency:i=507:si=on:rtra=on_0 on DTF2THF_21362 for (2997ds/507Mi)
% 1.62/1.53 % (21520)Refutation not found, incomplete strategy
% 1.62/1.53 % (21520)------------------------------
% 1.62/1.53 % (21520)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.53 % (21520)Termination reason: Refutation not found, incomplete strategy
% 1.62/1.53
% 1.62/1.53
% 1.62/1.53 % (21520)Memory used [KB]: 5500
% 1.62/1.53 % (21520)Time elapsed: 0.003 s
% 1.62/1.53 % (21520)Instructions burned: 3 (million)
% 1.62/1.53 % (21520)------------------------------
% 1.62/1.53 % (21520)------------------------------
% 1.62/1.54 % (21521)dis+1010_2:3_amm=off:fd=preordered:ixr=off:nm=0:pe=on:piset=equals:prag=on:sac=on:tgt=ground:i=149:si=on:rtra=on_0 on DTF2THF_21362 for (2997ds/149Mi)
% 1.62/1.56 % (21519)Instruction limit reached!
% 1.62/1.56 % (21519)------------------------------
% 1.62/1.56 % (21519)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.56 % (21519)Termination reason: Unknown
% 1.62/1.56 % (21519)Termination phase: Saturation
% 1.62/1.56
% 1.62/1.56 % (21519)Memory used [KB]: 1151
% 1.62/1.56 % (21519)Time elapsed: 0.034 s
% 1.62/1.56 % (21519)Instructions burned: 99 (million)
% 1.62/1.56 % (21519)------------------------------
% 1.62/1.56 % (21519)------------------------------
% 1.62/1.57 % (21522)lrs+21_1:16_au=on:bd=off:piset=and:i=39:si=on:rtra=on_0 on DTF2THF_21362 for (2997ds/39Mi)
% 1.62/1.58 % (21522)Instruction limit reached!
% 1.62/1.58 % (21522)------------------------------
% 1.62/1.58 % (21522)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.58 % (21522)Termination reason: Unknown
% 1.62/1.58 % (21522)Termination phase: Saturation
% 1.62/1.58
% 1.62/1.58 % (21522)Memory used [KB]: 5628
% 1.62/1.58 % (21522)Time elapsed: 0.016 s
% 1.62/1.58 % (21522)Instructions burned: 39 (million)
% 1.62/1.58 % (21522)------------------------------
% 1.62/1.58 % (21522)------------------------------
% 1.62/1.59 % (21521)Instruction limit reached!
% 1.62/1.59 % (21521)------------------------------
% 1.62/1.59 % (21521)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.59 % (21521)Termination reason: Unknown
% 1.62/1.59 % (21521)Termination phase: Saturation
% 1.62/1.59
% 1.62/1.59 % (21521)Memory used [KB]: 6140
% 1.62/1.59 % (21521)Time elapsed: 0.051 s
% 1.62/1.59 % (21521)Instructions burned: 151 (million)
% 1.62/1.59 % (21521)------------------------------
% 1.62/1.59 % (21521)------------------------------
% 1.62/1.59 % (21523)lrs+1004_1:1_cnfonf=lazy_pi_sigma_gen:fe=off:gs=on:hud=10:prag=on:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_21362 for (2996ds/6Mi)
% 1.62/1.59 % (21523)Instruction limit reached!
% 1.62/1.59 % (21523)------------------------------
% 1.62/1.59 % (21523)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.59 % (21523)Termination reason: Unknown
% 1.62/1.59 % (21523)Termination phase: Saturation
% 1.62/1.59
% 1.62/1.59 % (21523)Memory used [KB]: 9978
% 1.62/1.59 % (21523)Time elapsed: 0.005 s
% 1.62/1.59 % (21523)Instructions burned: 8 (million)
% 1.62/1.59 % (21523)------------------------------
% 1.62/1.59 % (21523)------------------------------
% 1.62/1.60 % (21524)dis+1002_1:1_aac=none:au=on:e2e=on:nm=2:nwc=10.0:sd=1:ss=axioms:st=3.0:i=1087:si=on:rtra=on_0 on DTF2THF_21362 for (2996ds/1087Mi)
% 1.62/1.60 % (21525)dis+10_1:1_aac=none:cs=on:i=47:si=on:rtra=on_0 on DTF2THF_21362 for (2996ds/47Mi)
% 1.62/1.61 % (21497)Instruction limit reached!
% 1.62/1.61 % (21497)------------------------------
% 1.62/1.61 % (21497)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.61 % (21497)Termination reason: Unknown
% 1.62/1.61 % (21497)Termination phase: Saturation
% 1.62/1.61
% 1.62/1.61 % (21497)Memory used [KB]: 7164
% 1.62/1.61 % (21497)Time elapsed: 0.257 s
% 1.62/1.61 % (21497)Instructions burned: 712 (million)
% 1.62/1.61 % (21497)------------------------------
% 1.62/1.61 % (21497)------------------------------
% 1.62/1.62 % (21526)lrs+1010_1:128_av=off:cbe=off:cnfonf=lazy_simp:fsr=off:ntd=on:ss=axioms:st=1.5:i=44:si=on:rtra=on_0 on DTF2THF_21362 for (2996ds/44Mi)
% 1.62/1.62 % (21525)Instruction limit reached!
% 1.62/1.62 % (21525)------------------------------
% 1.62/1.62 % (21525)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.62 % (21525)Termination reason: Unknown
% 1.62/1.62 % (21525)Termination phase: Saturation
% 1.62/1.62
% 1.62/1.62 % (21525)Memory used [KB]: 5628
% 1.62/1.62 % (21525)Time elapsed: 0.018 s
% 1.62/1.62 % (21525)Instructions burned: 48 (million)
% 1.62/1.62 % (21525)------------------------------
% 1.62/1.62 % (21525)------------------------------
% 1.62/1.62 % (21517)Instruction limit reached!
% 1.62/1.62 % (21517)------------------------------
% 1.62/1.62 % (21517)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.62 % (21517)Termination reason: Unknown
% 1.62/1.62 % (21517)Termination phase: Saturation
% 1.62/1.62
% 1.62/1.62 % (21517)Memory used [KB]: 7164
% 1.62/1.62 % (21517)Time elapsed: 0.136 s
% 1.62/1.62 % (21517)Instructions burned: 448 (million)
% 1.62/1.62 % (21517)------------------------------
% 1.62/1.62 % (21517)------------------------------
% 1.62/1.63 % (21527)dis+10_1:1_av=off:bd=off:cnfonf=lazy_gen:fe=off:hud=10:plsq=on:plsqc=1:plsqr=32,1:prag=on:tnu=1:i=432:si=on:rtra=on_0 on DTF2THF_21362 for (2996ds/432Mi)
% 1.62/1.63 % (21528)lrs+10_7:1_cnfonf=lazy_gen:fe=off:nwc=5.0:plsq=on:i=62:si=on:rtra=on_0 on DTF2THF_21362 for (2996ds/62Mi)
% 1.62/1.63 % (21526)Instruction limit reached!
% 1.62/1.63 % (21526)------------------------------
% 1.62/1.63 % (21526)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.63 % (21526)Termination reason: Unknown
% 1.62/1.63 % (21526)Termination phase: Saturation
% 1.62/1.63
% 1.62/1.63 % (21526)Memory used [KB]: 1151
% 1.62/1.63 % (21526)Time elapsed: 0.017 s
% 1.62/1.63 % (21526)Instructions burned: 45 (million)
% 1.62/1.63 % (21526)------------------------------
% 1.62/1.63 % (21526)------------------------------
% 1.62/1.63 % (21504)Instruction limit reached!
% 1.62/1.63 % (21504)------------------------------
% 1.62/1.63 % (21504)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.63 % (21504)Termination reason: Unknown
% 1.62/1.63 % (21504)Termination phase: Saturation
% 1.62/1.63
% 1.62/1.63 % (21504)Memory used [KB]: 7419
% 1.62/1.63 % (21504)Time elapsed: 0.260 s
% 1.62/1.63 % (21504)Instructions burned: 781 (million)
% 1.62/1.63 % (21504)------------------------------
% 1.62/1.63 % (21504)------------------------------
% 1.62/1.64 % (21529)lrs+1010_1:16_add=large:amm=off:anc=all_dependent:chr=on:fd=off:ins=2:sp=const_max:tnu=5:uhcvi=on:i=31:si=on:rtra=on_0 on DTF2THF_21362 for (2996ds/31Mi)
% 1.62/1.64 % (21530)dis+10_1:128_hud=1:i=96:si=on:rtra=on_0 on DTF2THF_21362 for (2996ds/96Mi)
% 1.62/1.65 % (21529)First to succeed.
% 1.62/1.65 % (21529)Refutation found. Thanks to Tanya!
% 1.62/1.65 % SZS status Theorem for DTF2THF_21362
% 1.62/1.65 % SZS output start Proof for DTF2THF_21362
% 1.62/1.65 thf(func_def_0, type, epso: ($o > $o) > $o).
% 1.62/1.65 thf(func_def_2, type, epsoo: (($o > $o) > $o) > $o > $o).
% 1.62/1.65 thf(func_def_3, type, q: ($o > $o) > $o).
% 1.62/1.65 thf(func_def_4, type, vEPSILON: !>[X0: $tType]:((X0 > $o) > X0)).
% 1.62/1.65 thf(func_def_9, type, sP0: $o > $o).
% 1.62/1.65 thf(func_def_12, type, ph2: !>[X0: $tType]:(X0)).
% 1.62/1.65 thf(f328,plain,(
% 1.62/1.65 $false),
% 1.62/1.65 inference(avatar_sat_refutation,[status(thm)],[f48,f53,f79,f94,f103,f135,f149,f163,f187,f188,f251,f261,f270,f272,f279,f281,f285,f286,f313])).
% 1.62/1.65 thf(f313,plain,(
% 1.62/1.65 ~spl1_18),
% 1.62/1.65 inference(avatar_contradiction_clause,[status(thm)],[f312])).
% 1.62/1.65 thf(f312,plain,(
% 1.62/1.65 $false | ~spl1_18),
% 1.62/1.65 inference(trivial_inequality_removal,[status(thm)],[f293])).
% 1.62/1.65 thf(f293,plain,(
% 1.62/1.65 ($true = $false) | ~spl1_18),
% 1.62/1.65 inference(backward_demodulation,[status(thm)],[f29,f176])).
% 1.62/1.65 thf(f176,plain,(
% 1.62/1.65 ( ! [X1 : $o] : (($false = X1)) ) | ~spl1_18),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f175])).
% 1.62/1.65 thf(f175,definition,(
% 1.62/1.65 spl1_18 <=> ! [X1 : $o] : ($false = X1)),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_18])],[avatar_definition])).
% 1.62/1.65 thf(f29,plain,(
% 1.62/1.65 ((q @ (^[Y0 : $o]: ($false))) = $true)),
% 1.62/1.65 inference(cnf_transformation,[status(thm)],[f18])).
% 1.62/1.65 thf(f18,plain,(
% 1.62/1.65 ((q @ (^[Y0 : $o]: ($false))) = $true)),
% 1.62/1.65 inference(fool_elimination,[status(thm)],[f17])).
% 1.62/1.65 thf(f17,plain,(
% 1.62/1.65 (q @ (^[X0 : $o] : ($false)))),
% 1.62/1.65 inference(rectify,[status(thm)],[f4])).
% 1.62/1.65 thf(f4,axiom,(
% 1.62/1.65 (q @ (^[X1 : $o] : ($false)))),
% 1.62/1.65 file('/export/starexec/sandbox2/tmp/tmp.DQ9pP7ssFh/DTF2THF_21362.p',qkf)).
% 1.62/1.65 thf(f286,plain,(
% 1.62/1.65 spl1_18 | spl1_16),
% 1.62/1.65 inference(avatar_split_clause,[status(thm)],[f179,f142,f175])).
% 1.62/1.65 thf(f142,definition,(
% 1.62/1.65 spl1_16 <=> ($true = (epso @ (^[Y0 : $o]: (Y0))))),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_16])],[avatar_definition])).
% 1.62/1.65 thf(f179,plain,(
% 1.62/1.65 ( ! [X1 : $o] : (($true = (epso @ (^[Y0 : $o]: (Y0)))) | ($false = X1)) )),
% 1.62/1.65 inference(beta_eta_normalization,[status(thm)],[f178])).
% 1.62/1.65 thf(f178,plain,(
% 1.62/1.65 ( ! [X1 : $o] : (($true = ((^[Y0 : $o]: (Y0)) @ (epso @ (^[Y0 : $o]: (Y0))))) | ($false = ((^[Y0 : $o]: (Y0)) @ X1))) )),
% 1.62/1.65 introduced(definition,[],[choice_axiom])).
% 1.62/1.65 thf(f285,plain,(
% 1.62/1.65 ~spl1_6 | ~spl1_16),
% 1.62/1.65 inference(avatar_contradiction_clause,[status(thm)],[f284])).
% 1.62/1.65 thf(f284,plain,(
% 1.62/1.65 $false | (~spl1_6 | ~spl1_16)),
% 1.62/1.65 inference(trivial_inequality_removal,[status(thm)],[f283])).
% 1.62/1.65 thf(f283,plain,(
% 1.62/1.65 ($true = $false) | (~spl1_6 | ~spl1_16)),
% 1.62/1.65 inference(backward_demodulation,[status(thm)],[f144,f65])).
% 1.62/1.65 thf(f65,plain,(
% 1.62/1.65 ( ! [X1 : $o > $o] : (((epso @ X1) = $false)) ) | ~spl1_6),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f64])).
% 1.62/1.65 thf(f64,definition,(
% 1.62/1.65 spl1_6 <=> ! [X1 : $o > $o] : ((epso @ X1) = $false)),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_6])],[avatar_definition])).
% 1.62/1.65 thf(f144,plain,(
% 1.62/1.65 ($true = (epso @ (^[Y0 : $o]: (Y0)))) | ~spl1_16),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f142])).
% 1.62/1.65 thf(f281,plain,(
% 1.62/1.65 spl1_6 | spl1_5),
% 1.62/1.65 inference(avatar_split_clause,[status(thm)],[f70,f60,f64])).
% 1.62/1.65 thf(f60,definition,(
% 1.62/1.65 spl1_5 <=> ((epso @ (epsoo @ epso)) = $true)),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_5])],[avatar_definition])).
% 1.62/1.65 thf(f70,plain,(
% 1.62/1.65 ( ! [X1 : $o > $o] : (((epso @ X1) = $false) | ((epso @ (epsoo @ epso)) = $true)) )),
% 1.62/1.65 introduced(definition,[],[choice_axiom])).
% 1.62/1.65 thf(f279,plain,(
% 1.62/1.65 ~spl1_17 | spl1_9 | ~spl1_19),
% 1.62/1.65 inference(avatar_split_clause,[status(thm)],[f278,f195,f91,f158])).
% 1.62/1.65 thf(f158,definition,(
% 1.62/1.65 spl1_17 <=> ((epsoo @ epso @ $true) = $true)),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_17])],[avatar_definition])).
% 1.62/1.65 thf(f91,definition,(
% 1.62/1.65 spl1_9 <=> ((epsoo @ epso @ sK3) = $true)),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_9])],[avatar_definition])).
% 1.62/1.65 thf(f195,definition,(
% 1.62/1.65 spl1_19 <=> ($true = sK3)),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_19])],[avatar_definition])).
% 1.62/1.65 thf(f278,plain,(
% 1.62/1.65 ((epsoo @ epso @ $true) != $true) | (spl1_9 | ~spl1_19)),
% 1.62/1.65 inference(backward_demodulation,[status(thm)],[f93,f196])).
% 1.62/1.65 thf(f196,plain,(
% 1.62/1.65 ($true = sK3) | ~spl1_19),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f195])).
% 1.62/1.65 thf(f93,plain,(
% 1.62/1.65 ((epsoo @ epso @ sK3) != $true) | spl1_9),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f91])).
% 1.62/1.65 thf(f272,plain,(
% 1.62/1.65 spl1_12 | spl1_4 | spl1_11),
% 1.62/1.65 inference(avatar_split_clause,[status(thm)],[f271,f111,f55,f115])).
% 1.62/1.65 thf(f115,definition,(
% 1.62/1.65 spl1_12 <=> ($true = (epsoo @ epso @ sK5))),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_12])],[avatar_definition])).
% 1.62/1.65 thf(f55,definition,(
% 1.62/1.65 spl1_4 <=> ((epsoo @ epso) = (^[Y0 : $o]: (Y0)))),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_4])],[avatar_definition])).
% 1.62/1.65 thf(f111,definition,(
% 1.62/1.65 spl1_11 <=> ($true = sK5)),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_11])],[avatar_definition])).
% 1.62/1.65 thf(f271,plain,(
% 1.62/1.65 ($true = (epsoo @ epso @ sK5)) | (spl1_4 | spl1_11)),
% 1.62/1.65 inference(subsumption_resolution,[status(thm)],[f108,f112])).
% 1.62/1.65 thf(f112,plain,(
% 1.62/1.65 ($true != sK5) | spl1_11),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f111])).
% 1.62/1.65 thf(f108,plain,(
% 1.62/1.65 ($true = (epsoo @ epso @ sK5)) | ($true = sK5) | spl1_4),
% 1.62/1.65 inference(binary_proxy_clausification,[status(thm)],[f107])).
% 1.62/1.65 thf(f107,plain,(
% 1.62/1.65 (sK5 != (epsoo @ epso @ sK5)) | spl1_4),
% 1.62/1.65 inference(beta_eta_normalization,[status(thm)],[f106])).
% 1.62/1.65 thf(f106,plain,(
% 1.62/1.65 (((^[Y0 : $o]: (Y0)) @ sK5) != (epsoo @ epso @ sK5)) | spl1_4),
% 1.62/1.65 inference(negative_extensionality,[status(thm)],[f57])).
% 1.62/1.65 thf(f57,plain,(
% 1.62/1.65 ((epsoo @ epso) != (^[Y0 : $o]: (Y0))) | spl1_4),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f55])).
% 1.62/1.65 thf(f270,plain,(
% 1.62/1.65 spl1_9 | spl1_11 | ~spl1_12 | spl1_19),
% 1.62/1.65 inference(avatar_contradiction_clause,[status(thm)],[f269])).
% 1.62/1.65 thf(f269,plain,(
% 1.62/1.65 $false | (spl1_9 | spl1_11 | ~spl1_12 | spl1_19)),
% 1.62/1.65 inference(subsumption_resolution,[status(thm)],[f268,f197])).
% 1.62/1.65 thf(f197,plain,(
% 1.62/1.65 ($true != sK3) | spl1_19),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f195])).
% 1.62/1.65 thf(f268,plain,(
% 1.62/1.65 ($true = sK3) | (spl1_9 | spl1_11 | ~spl1_12)),
% 1.62/1.65 inference(subsumption_resolution,[status(thm)],[f206,f112])).
% 1.62/1.65 thf(f206,plain,(
% 1.62/1.65 ($true = sK5) | ($true = sK3) | (spl1_9 | ~spl1_12)),
% 1.62/1.65 inference(binary_proxy_clausification,[status(thm)],[f205])).
% 1.62/1.65 thf(f205,plain,(
% 1.62/1.65 (sK5 != sK3) | (spl1_9 | ~spl1_12)),
% 1.62/1.65 inference(trivial_inequality_removal,[status(thm)],[f201])).
% 1.62/1.65 thf(f201,plain,(
% 1.62/1.65 (sK5 != sK3) | ($true != $true) | (spl1_9 | ~spl1_12)),
% 1.62/1.65 inference(constrained_superposition,[status(thm)],[f93,f117])).
% 1.62/1.65 thf(f117,plain,(
% 1.62/1.65 ($true = (epsoo @ epso @ sK5)) | ~spl1_12),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f115])).
% 1.62/1.65 thf(f261,plain,(
% 1.62/1.65 ~spl1_11 | ~spl1_14),
% 1.62/1.65 inference(avatar_contradiction_clause,[status(thm)],[f260])).
% 1.62/1.65 thf(f260,plain,(
% 1.62/1.65 $false | (~spl1_11 | ~spl1_14)),
% 1.62/1.65 inference(trivial_inequality_removal,[status(thm)],[f259])).
% 1.62/1.65 thf(f259,plain,(
% 1.62/1.65 ($true = $false) | (~spl1_11 | ~spl1_14)),
% 1.62/1.65 inference(backward_demodulation,[status(thm)],[f113,f126])).
% 1.62/1.65 thf(f126,plain,(
% 1.62/1.65 ($false = sK5) | ~spl1_14),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f124])).
% 1.62/1.65 thf(f124,definition,(
% 1.62/1.65 spl1_14 <=> ($false = sK5)),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_14])],[avatar_definition])).
% 1.62/1.65 thf(f113,plain,(
% 1.62/1.65 ($true = sK5) | ~spl1_11),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f111])).
% 1.62/1.65 thf(f251,plain,(
% 1.62/1.65 ~spl1_11 | ~spl1_13 | ~spl1_17),
% 1.62/1.65 inference(avatar_contradiction_clause,[status(thm)],[f250])).
% 1.62/1.65 thf(f250,plain,(
% 1.62/1.65 $false | (~spl1_11 | ~spl1_13 | ~spl1_17)),
% 1.62/1.65 inference(subsumption_resolution,[status(thm)],[f237,f113])).
% 1.62/1.65 thf(f237,plain,(
% 1.62/1.65 ($true != sK5) | (~spl1_13 | ~spl1_17)),
% 1.62/1.65 inference(trivial_inequality_removal,[status(thm)],[f232])).
% 1.62/1.65 thf(f232,plain,(
% 1.62/1.65 ($true = $false) | ($true != sK5) | (~spl1_13 | ~spl1_17)),
% 1.62/1.65 inference(constrained_superposition,[status(thm)],[f160,f122])).
% 1.62/1.65 thf(f122,plain,(
% 1.62/1.65 ($false = (epsoo @ epso @ sK5)) | ~spl1_13),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f120])).
% 1.62/1.65 thf(f120,definition,(
% 1.62/1.65 spl1_13 <=> ($false = (epsoo @ epso @ sK5))),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_13])],[avatar_definition])).
% 1.62/1.65 thf(f160,plain,(
% 1.62/1.65 ((epsoo @ epso @ $true) = $true) | ~spl1_17),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f158])).
% 1.62/1.65 thf(f188,plain,(
% 1.62/1.65 spl1_17 | ~spl1_5 | ~spl1_7),
% 1.62/1.65 inference(avatar_split_clause,[status(thm)],[f156,f73,f60,f158])).
% 1.62/1.65 thf(f73,definition,(
% 1.62/1.65 spl1_7 <=> ((epsoo @ epso @ (epso @ (epsoo @ epso))) = $true)),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_7])],[avatar_definition])).
% 1.62/1.65 thf(f156,plain,(
% 1.62/1.65 ((epsoo @ epso @ $true) = $true) | (~spl1_5 | ~spl1_7)),
% 1.62/1.65 inference(backward_demodulation,[status(thm)],[f75,f62])).
% 1.62/1.65 thf(f62,plain,(
% 1.62/1.65 ((epso @ (epsoo @ epso)) = $true) | ~spl1_5),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f60])).
% 1.62/1.65 thf(f75,plain,(
% 1.62/1.65 ((epsoo @ epso @ (epso @ (epsoo @ epso))) = $true) | ~spl1_7),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f73])).
% 1.62/1.65 thf(f187,plain,(
% 1.62/1.65 ~spl1_8 | spl1_10),
% 1.62/1.65 inference(avatar_contradiction_clause,[status(thm)],[f186])).
% 1.62/1.65 thf(f186,plain,(
% 1.62/1.65 $false | (~spl1_8 | spl1_10)),
% 1.62/1.65 inference(trivial_inequality_removal,[status(thm)],[f185])).
% 1.62/1.65 thf(f185,plain,(
% 1.62/1.65 ($false != $false) | (~spl1_8 | spl1_10)),
% 1.62/1.65 inference(superposition,[status(thm)],[f102,f78])).
% 1.62/1.65 thf(f78,plain,(
% 1.62/1.65 ( ! [X1 : $o] : (((epsoo @ epso @ X1) = $false)) ) | ~spl1_8),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f77])).
% 1.62/1.65 thf(f77,definition,(
% 1.62/1.65 spl1_8 <=> ! [X1 : $o] : ((epsoo @ epso @ X1) = $false)),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_8])],[avatar_definition])).
% 1.62/1.65 thf(f102,plain,(
% 1.62/1.65 ($false != (epsoo @ epso @ sK4)) | spl1_10),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f100])).
% 1.62/1.65 thf(f100,definition,(
% 1.62/1.65 spl1_10 <=> ($false = (epsoo @ epso @ sK4))),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_10])],[avatar_definition])).
% 1.62/1.65 thf(f163,plain,(
% 1.62/1.65 spl1_13 | spl1_4 | spl1_14),
% 1.62/1.65 inference(avatar_split_clause,[status(thm)],[f162,f124,f55,f120])).
% 1.62/1.65 thf(f162,plain,(
% 1.62/1.65 ($false = (epsoo @ epso @ sK5)) | (spl1_4 | spl1_14)),
% 1.62/1.65 inference(subsumption_resolution,[status(thm)],[f109,f125])).
% 1.62/1.65 thf(f125,plain,(
% 1.62/1.65 ($false != sK5) | spl1_14),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f124])).
% 1.62/1.65 thf(f109,plain,(
% 1.62/1.65 ($false = sK5) | ($false = (epsoo @ epso @ sK5)) | spl1_4),
% 1.62/1.65 inference(binary_proxy_clausification,[status(thm)],[f107])).
% 1.62/1.65 thf(f149,plain,(
% 1.62/1.65 ~spl1_1),
% 1.62/1.65 inference(avatar_contradiction_clause,[status(thm)],[f148])).
% 1.62/1.65 thf(f148,plain,(
% 1.62/1.65 $false | ~spl1_1),
% 1.62/1.65 inference(trivial_inequality_removal,[status(thm)],[f147])).
% 1.62/1.65 thf(f147,plain,(
% 1.62/1.65 ($true = $false) | ~spl1_1),
% 1.62/1.65 inference(backward_demodulation,[status(thm)],[f31,f43])).
% 1.62/1.65 thf(f43,plain,(
% 1.62/1.65 ((sP0 @ $true) = $false) | ~spl1_1),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f41])).
% 1.62/1.65 thf(f41,definition,(
% 1.62/1.65 spl1_1 <=> ((sP0 @ $true) = $false)),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_1])],[avatar_definition])).
% 1.62/1.65 thf(f31,plain,(
% 1.62/1.65 ((sP0 @ $true) = $true)),
% 1.62/1.65 inference(inequality_splitting,[status(thm)],[f26,f30])).
% 1.62/1.65 thf(f30,plain,(
% 1.62/1.65 ((sP0 @ (q @ (epsoo @ epso))) = $false)),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[sP0])],[inequality_splitting_name_introduction])).
% 1.62/1.65 thf(f26,plain,(
% 1.62/1.65 ((q @ (epsoo @ epso)) != $true)),
% 1.62/1.65 inference(cnf_transformation,[status(thm)],[f21])).
% 1.62/1.65 thf(f21,plain,(
% 1.62/1.65 ((q @ (epsoo @ epso)) != $true)),
% 1.62/1.65 inference(flattening,[status(thm)],[f12])).
% 1.62/1.65 thf(f12,plain,(
% 1.62/1.65 ~((q @ (epsoo @ epso)) = $true)),
% 1.62/1.65 inference(fool_elimination,[status(thm)],[f11])).
% 1.62/1.65 thf(f11,plain,(
% 1.62/1.65 ~(q @ (epsoo @ epso))),
% 1.62/1.65 inference(rectify,[status(thm)],[f7])).
% 1.62/1.65 thf(f7,negated_conjecture,(
% 1.62/1.65 ~(q @ (epsoo @ epso))),
% 1.62/1.65 inference(negated_conjecture,[status(cth)],[f6])).
% 1.62/1.65 thf(f6,conjecture,(
% 1.62/1.65 (q @ (epsoo @ epso))),
% 1.62/1.65 file('/export/starexec/sandbox2/tmp/tmp.DQ9pP7ssFh/DTF2THF_21362.p',c)).
% 1.62/1.65 thf(f135,plain,(
% 1.62/1.65 ~spl1_4),
% 1.62/1.65 inference(avatar_contradiction_clause,[status(thm)],[f134])).
% 1.62/1.65 thf(f134,plain,(
% 1.62/1.65 $false | ~spl1_4),
% 1.62/1.65 inference(subsumption_resolution,[status(thm)],[f130,f28])).
% 1.62/1.65 thf(f28,plain,(
% 1.62/1.65 ((q @ (^[Y0 : $o]: (Y0))) = $true)),
% 1.62/1.65 inference(cnf_transformation,[status(thm)],[f14])).
% 1.62/1.65 thf(f14,plain,(
% 1.62/1.65 ((q @ (^[Y0 : $o]: (Y0))) = $true)),
% 1.62/1.65 inference(fool_elimination,[status(thm)],[f13])).
% 1.62/1.65 thf(f13,plain,(
% 1.62/1.65 (q @ (^[X0 : $o] : (X0)))),
% 1.62/1.65 inference(rectify,[status(thm)],[f5])).
% 1.62/1.65 thf(f5,axiom,(
% 1.62/1.65 (q @ (^[X1 : $o] : (X1)))),
% 1.62/1.65 file('/export/starexec/sandbox2/tmp/tmp.DQ9pP7ssFh/DTF2THF_21362.p',qid)).
% 1.62/1.65 thf(f130,plain,(
% 1.62/1.65 ((q @ (^[Y0 : $o]: (Y0))) != $true) | ~spl1_4),
% 1.62/1.65 inference(backward_demodulation,[status(thm)],[f39,f56])).
% 1.62/1.65 thf(f56,plain,(
% 1.62/1.65 ((epsoo @ epso) = (^[Y0 : $o]: (Y0))) | ~spl1_4),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f55])).
% 1.62/1.65 thf(f39,plain,(
% 1.62/1.65 ((q @ (epsoo @ epso)) != $true)),
% 1.62/1.65 inference(trivial_inequality_removal,[status(thm)],[f37])).
% 1.62/1.65 thf(f37,plain,(
% 1.62/1.65 ((q @ (epsoo @ epso)) != $true) | ($true = $false)),
% 1.62/1.65 inference(constrained_superposition,[status(thm)],[f31,f30])).
% 1.62/1.65 thf(f103,plain,(
% 1.62/1.65 ~spl1_10 | spl1_3),
% 1.62/1.65 inference(avatar_split_clause,[status(thm)],[f98,f50,f100])).
% 1.62/1.65 thf(f50,definition,(
% 1.62/1.65 spl1_3 <=> ((epsoo @ epso) = (^[Y0 : $o]: ($false)))),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_3])],[avatar_definition])).
% 1.62/1.65 thf(f98,plain,(
% 1.62/1.65 ($false != (epsoo @ epso @ sK4)) | spl1_3),
% 1.62/1.65 inference(beta_eta_normalization,[status(thm)],[f97])).
% 1.62/1.65 thf(f97,plain,(
% 1.62/1.65 (((^[Y0 : $o]: ($false)) @ sK4) != (epsoo @ epso @ sK4)) | spl1_3),
% 1.62/1.65 inference(negative_extensionality,[status(thm)],[f52])).
% 1.62/1.65 thf(f52,plain,(
% 1.62/1.65 ((epsoo @ epso) != (^[Y0 : $o]: ($false))) | spl1_3),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f50])).
% 1.62/1.65 thf(f94,plain,(
% 1.62/1.65 ~spl1_9 | spl1_2),
% 1.62/1.65 inference(avatar_split_clause,[status(thm)],[f89,f45,f91])).
% 1.62/1.65 thf(f45,definition,(
% 1.62/1.65 spl1_2 <=> ((epsoo @ epso) = (^[Y0 : $o]: ($true)))),
% 1.62/1.65 introduced(definition,[new_symbols(naming,[spl1_2])],[avatar_definition])).
% 1.62/1.65 thf(f89,plain,(
% 1.62/1.65 ((epsoo @ epso @ sK3) != $true) | spl1_2),
% 1.62/1.65 inference(beta_eta_normalization,[status(thm)],[f88])).
% 1.62/1.65 thf(f88,plain,(
% 1.62/1.65 ((epsoo @ epso @ sK3) != ((^[Y0 : $o]: ($true)) @ sK3)) | spl1_2),
% 1.62/1.65 inference(negative_extensionality,[status(thm)],[f47])).
% 1.62/1.65 thf(f47,plain,(
% 1.62/1.65 ((epsoo @ epso) != (^[Y0 : $o]: ($true))) | spl1_2),
% 1.62/1.65 inference(avatar_component_clause,[status(thm)],[f45])).
% 1.62/1.65 thf(f79,plain,(
% 1.62/1.65 spl1_7 | spl1_8),
% 1.62/1.65 inference(avatar_split_clause,[status(thm)],[f71,f77,f73])).
% 1.62/1.65 thf(f71,plain,(
% 1.62/1.65 ( ! [X1 : $o] : (((epsoo @ epso @ X1) = $false) | ((epsoo @ epso @ (epso @ (epsoo @ epso))) = $true)) )),
% 1.62/1.65 introduced(definition,[],[choice_axiom])).
% 1.62/1.65 thf(f53,plain,(
% 1.62/1.65 spl1_1 | ~spl1_3),
% 1.62/1.65 inference(avatar_split_clause,[status(thm)],[f34,f50,f41])).
% 1.62/1.65 thf(f34,plain,(
% 1.62/1.65 ((epsoo @ epso) != (^[Y0 : $o]: ($false))) | ((sP0 @ $true) = $false)),
% 1.62/1.65 inference(constrained_superposition,[status(thm)],[f30,f29])).
% 1.62/1.65 thf(f48,plain,(
% 1.62/1.65 spl1_1 | ~spl1_2),
% 1.62/1.65 inference(avatar_split_clause,[status(thm)],[f35,f45,f41])).
% 1.62/1.65 thf(f35,plain,(
% 1.62/1.65 ((sP0 @ $true) = $false) | ((epsoo @ epso) != (^[Y0 : $o]: ($true)))),
% 1.62/1.65 inference(constrained_superposition,[status(thm)],[f30,f27])).
% 1.62/1.65 thf(f27,plain,(
% 1.62/1.65 ((q @ (^[Y0 : $o]: ($true))) = $true)),
% 1.62/1.65 inference(cnf_transformation,[status(thm)],[f10])).
% 1.62/1.65 thf(f10,plain,(
% 1.62/1.65 ((q @ (^[Y0 : $o]: ($true))) = $true)),
% 1.62/1.65 inference(fool_elimination,[status(thm)],[f9])).
% 1.62/1.65 thf(f9,plain,(
% 1.62/1.65 (q @ (^[X0 : $o] : ($true)))),
% 1.62/1.65 inference(rectify,[status(thm)],[f3])).
% 1.62/1.65 thf(f3,axiom,(
% 1.62/1.65 (q @ (^[X1 : $o] : ($true)))),
% 1.62/1.65 file('/export/starexec/sandbox2/tmp/tmp.DQ9pP7ssFh/DTF2THF_21362.p',qkt)).
% 1.62/1.65 % SZS output end Proof for DTF2THF_21362
% 1.62/1.65 % (21529)------------------------------
% 1.62/1.65 % (21529)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.62/1.65 % (21529)Termination reason: Refutation
% 1.62/1.65
% 1.62/1.65 % (21529)Memory used [KB]: 5628
% 1.62/1.65 % (21529)Time elapsed: 0.009 s
% 1.62/1.65 % (21529)Instructions burned: 16 (million)
% 1.62/1.65 % (21529)------------------------------
% 1.62/1.65 % (21529)------------------------------
% 1.62/1.65 % (21476)Success in time 0.37 s
%------------------------------------------------------------------------------