%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : SYO515^1 : TPTP v9.2.1. Bugfixed v9.2.1.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n024.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 : Sat Feb 28 09:54:02 AM UTC 2026
% Result : Theorem 1.53s 1.34s
% Output : Refutation 1.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 25
% Syntax : Number of formulae : 217 ( 15 unt; 0 typ; 21 def)
% Number of atoms : 1513 ( 323 equ; 64 cnn)
% Maximal formula atoms : 6 ( 6 avg)
% Number of connectives : 1155 ( 443 ~; 383 |; 31 &; 271 @)
% ( 21 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 30 ( 30 >; 0 *; 0 +; 0 <<)
% Number of symbols : 38 ( 33 usr; 32 con; 0-2 aty)
% Number of variables : 166 ( 152 ^; 4 !; 10 ?; 166 :)
% Comments :
%------------------------------------------------------------------------------
thf(func_def_0,type,
t: ( ( $o > $o ) > $o ) > $o > $o ).
thf(func_def_11,type,
sK0: ( $o > $o ) > $o ).
thf(func_def_12,type,
sK1: $o > $o ).
thf(func_def_14,type,
ph3:
!>[X0: $tType] : X0 ).
thf(f738,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[f51,f64,f73,f86,f87,f88,f133,f142,f175,f195,f203,f210,f304,f319,f331,f341,f347,f381,f393,f401,f439,f480,f489,f536,f553,f604,f731]) ).
thf(f731,plain,
( spl2_2
| ~ spl2_10 ),
inference(avatar_contradiction_clause,[status(thm)],[f730]) ).
thf(f730,plain,
( $false
| spl2_2
| ~ spl2_10 ),
inference(subsumption_resolution,[status(thm)],[f729,f49]) ).
thf(f49,plain,
( ( ( sK0
@ ^ [Y0: $o] : $false )
!= $false )
| spl2_2 ),
inference(avatar_component_clause,[status(thm)],[f48]) ).
thf(f48,definition,
( spl2_2
<=> ( ( sK0
@ ^ [Y0: $o] : $false )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl2_2])],[avatar_definition]) ).
thf(f729,plain,
( ( ( sK0
@ ^ [Y0: $o] : $false )
= $false )
| ~ spl2_10 ),
inference(not_proxy_clausification,[status(thm)],[f721]) ).
thf(f721,plain,
( ( $true
= ( ~ ( sK0
@ ^ [Y0: $o] : $false ) ) )
| ~ spl2_10 ),
inference(binary_proxy_clausification,[status(thm)],[f720]) ).
thf(f720,plain,
( ( $false
!= ( ( ( ( sK0 @ (~) )
= ( ~ sK19 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) )
& ~ ( sK0
@ ^ [Y0: $o] : $false ) ) )
| ~ spl2_10 ),
inference(beta_eta_normalization,[status(thm)],[f719]) ).
thf(f719,plain,
( ( ( ^ [Y0: $o] : $false
@ sK19 )
!= ( ^ [Y0: $o] :
( ( ( ( sK0 @ (~) )
= ( ~ Y0 ) )
| ( sK0
@ ^ [Y1: $o] : $true ) )
& ~ ( sK0
@ ^ [Y1: $o] : $false ) )
@ sK19 ) )
| ~ spl2_10 ),
inference(negative_extensionality,[status(thm)],[f715]) ).
thf(f715,plain,
( ( ( ^ [Y0: $o] : $false )
!= ( ^ [Y0: $o] :
( ( ( ( sK0 @ (~) )
= ( ~ Y0 ) )
| ( sK0
@ ^ [Y1: $o] : $true ) )
& ~ ( sK0
@ ^ [Y1: $o] : $false ) ) ) )
| ~ spl2_10 ),
inference(trivial_inequality_removal,[status(thm)],[f710]) ).
thf(f710,plain,
( ( $true != $true )
| ( ( ^ [Y0: $o] : $false )
!= ( ^ [Y0: $o] :
( ( ( ( sK0 @ (~) )
= ( ~ Y0 ) )
| ( sK0
@ ^ [Y1: $o] : $true ) )
& ~ ( sK0
@ ^ [Y1: $o] : $false ) ) ) )
| ~ spl2_10 ),
inference(constrained_superposition,[status(thm)],[f17,f85]) ).
thf(f85,plain,
( ( ( sK0
@ ^ [Y0: $o] : $false )
= $true )
| ~ spl2_10 ),
inference(avatar_component_clause,[status(thm)],[f83]) ).
thf(f83,definition,
( spl2_10
<=> ( ( sK0
@ ^ [Y0: $o] : $false )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl2_10])],[avatar_definition]) ).
thf(f17,plain,
( $true
!= ( sK0
@ ^ [Y0: $o] :
( ( ( ( sK0 @ (~) )
= ( ~ Y0 ) )
| ( sK0
@ ^ [Y1: $o] : $true ) )
& ~ ( sK0
@ ^ [Y1: $o] : $false ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f16]) ).
thf(f16,plain,
( $true
!= ( sK0
@ ( ^ [Y0: ( $o > $o ) > $o,Y1: $o] :
( ( ( ( Y0
@ ^ [Y2: $o] : ~ Y2 )
= ( ~ Y1 ) )
| ( Y0
@ ^ [Y2: $o] : $true ) )
& ~ ( Y0
@ ^ [Y2: $o] : $false ) )
@ sK0 ) ) ),
inference(definition_unfolding,[status(thm)],[f13,f15]) ).
thf(f15,plain,
( t
= ( ^ [Y0: ( $o > $o ) > $o,Y1: $o] :
( ( ( ( Y0
@ ^ [Y2: $o] : ~ Y2 )
= ( ~ Y1 ) )
| ( Y0
@ ^ [Y2: $o] : $true ) )
& ~ ( Y0
@ ^ [Y2: $o] : $false ) ) ) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
thf(f8,plain,
( t
= ( ^ [Y0: ( $o > $o ) > $o,Y1: $o] :
( ( ( ( Y0
@ ^ [Y2: $o] : ~ Y2 )
= ( ~ Y1 ) )
| ( Y0
@ ^ [Y2: $o] : $true ) )
& ~ ( Y0
@ ^ [Y2: $o] : $false ) ) ) ),
inference(fool_elimination,[status(thm)],[f7]) ).
thf(f7,plain,
( t
= ( ^ [X0: ( $o > $o ) > $o,X1: $o] :
( ~ ( X0
@ ^ [X2: $o] : $false )
& ( ( X0
@ ^ [X3: $o] : $true )
| ( ( X0
@ ^ [X4: $o] : ~ X4 )
= ( ~ X1 ) ) ) ) ) ),
inference(rectify,[status(thm)],[f1]) ).
thf(f1,axiom,
( t
= ( ^ [X0: ( $o > $o ) > $o,X1: $o] :
( ~ ( X0
@ ^ [X1: $o] : $false )
& ( ( X0
@ ^ [X1: $o] : $true )
| ( ( X0
@ ^ [X1: $o] : ~ X1 )
= ( ~ X1 ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.EKm7Nwuf6V/DTF2THF_30244.p',t) ).
thf(f13,plain,
( $true
!= ( sK0 @ ( t @ sK0 ) ) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
thf(f12,plain,
( ( $true
= ( sK0 @ sK1 ) )
& ( $true
!= ( sK0 @ ( t @ sK0 ) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1])],[f9,f11,f10]) ).
thf(f10,plain,
( ? [X0: ( $o > $o ) > $o] :
( ? [X1: $o > $o] :
( ( X0 @ X1 )
= $true )
& ( ( X0 @ ( t @ X0 ) )
!= $true ) )
=> ( ? [X1: $o > $o] :
( $true
= ( sK0 @ X1 ) )
& ( $true
!= ( sK0 @ ( t @ sK0 ) ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f11,plain,
( ? [X1: $o > $o] :
( $true
= ( sK0 @ X1 ) )
=> ( $true
= ( sK0 @ sK1 ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f9,plain,
? [X0: ( $o > $o ) > $o] :
( ? [X1: $o > $o] :
( ( X0 @ X1 )
= $true )
& ( ( X0 @ ( t @ X0 ) )
!= $true ) ),
inference(ennf_transformation,[status(thm)],[f6]) ).
thf(f6,plain,
~ ! [X0: ( $o > $o ) > $o] :
( ? [X1: $o > $o] :
( ( X0 @ X1 )
= $true )
=> ( ( X0 @ ( t @ X0 ) )
= $true ) ),
inference(fool_elimination,[status(thm)],[f5]) ).
thf(f5,plain,
~ ! [X0: ( $o > $o ) > $o] :
( ? [X1: $o > $o] : ( X0 @ X1 )
=> ( X0 @ ( t @ X0 ) ) ),
inference(rectify,[status(thm)],[f3]) ).
thf(f3,negated_conjecture,
~ ! [X0: ( $o > $o ) > $o] :
( ? [X2: $o > $o] : ( X0 @ X2 )
=> ( X0 @ ( t @ X0 ) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
thf(f2,conjecture,
! [X0: ( $o > $o ) > $o] :
( ? [X2: $o > $o] : ( X0 @ X2 )
=> ( X0 @ ( t @ X0 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.EKm7Nwuf6V/DTF2THF_30244.p',choiceoo1) ).
thf(f604,plain,
( ~ spl2_1
| ~ spl2_4
| ~ spl2_9
| spl2_21
| ~ spl2_22 ),
inference(avatar_contradiction_clause,[status(thm)],[f603]) ).
thf(f603,plain,
( $false
| ~ spl2_1
| ~ spl2_4
| ~ spl2_9
| spl2_21
| ~ spl2_22 ),
inference(subsumption_resolution,[status(thm)],[f597,f602]) ).
thf(f602,plain,
( ( sK16 = $false )
| ~ spl2_9
| spl2_21
| ~ spl2_22 ),
inference(subsumption_resolution,[status(thm)],[f600,f474]) ).
thf(f474,plain,
( ( $false != sK15 )
| spl2_21 ),
inference(avatar_component_clause,[status(thm)],[f473]) ).
thf(f473,definition,
( spl2_21
<=> ( $false = sK15 ) ),
introduced(definition,[new_symbols(naming,[spl2_21])],[avatar_definition]) ).
thf(f600,plain,
( ( $false = sK15 )
| ( sK16 = $false )
| ~ spl2_9
| ~ spl2_22 ),
inference(binary_proxy_clausification,[status(thm)],[f598]) ).
thf(f598,plain,
( ( sK16 != sK15 )
| ~ spl2_9
| ~ spl2_22 ),
inference(trivial_inequality_removal,[status(thm)],[f586]) ).
thf(f586,plain,
( ( $true != $true )
| ( sK16 != sK15 )
| ~ spl2_9
| ~ spl2_22 ),
inference(constrained_superposition,[status(thm)],[f580,f479]) ).
thf(f479,plain,
( ( $true
= ( sK1 @ sK15 ) )
| ~ spl2_22 ),
inference(avatar_component_clause,[status(thm)],[f477]) ).
thf(f477,definition,
( spl2_22
<=> ( $true
= ( sK1 @ sK15 ) ) ),
introduced(definition,[new_symbols(naming,[spl2_22])],[avatar_definition]) ).
thf(f580,plain,
( ( $true
!= ( sK1 @ sK16 ) )
| ~ spl2_9 ),
inference(beta_eta_normalization,[status(thm)],[f579]) ).
thf(f579,plain,
( ( ( ^ [Y0: $o] : $true
@ sK16 )
!= ( sK1 @ sK16 ) )
| ~ spl2_9 ),
inference(negative_extensionality,[status(thm)],[f374]) ).
thf(f374,plain,
( ( sK1
!= ( ^ [Y0: $o] : $true ) )
| ~ spl2_9 ),
inference(trivial_inequality_removal,[status(thm)],[f370]) ).
thf(f370,plain,
( ( sK1
!= ( ^ [Y0: $o] : $true ) )
| ( $true = $false )
| ~ spl2_9 ),
inference(constrained_superposition,[status(thm)],[f14,f81]) ).
thf(f81,plain,
( ( ( sK0
@ ^ [Y0: $o] : $true )
= $false )
| ~ spl2_9 ),
inference(avatar_component_clause,[status(thm)],[f79]) ).
thf(f79,definition,
( spl2_9
<=> ( ( sK0
@ ^ [Y0: $o] : $true )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl2_9])],[avatar_definition]) ).
thf(f14,plain,
( $true
= ( sK0 @ sK1 ) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
thf(f597,plain,
( ( sK16 != $false )
| ~ spl2_1
| ~ spl2_4
| ~ spl2_9 ),
inference(trivial_inequality_removal,[status(thm)],[f588]) ).
thf(f588,plain,
( ( $true != $true )
| ( sK16 != $false )
| ~ spl2_1
| ~ spl2_4
| ~ spl2_9 ),
inference(constrained_superposition,[status(thm)],[f580,f445]) ).
thf(f445,plain,
( ( $true
= ( sK1 @ $false ) )
| ~ spl2_1
| ~ spl2_4 ),
inference(superposition,[status(thm)],[f46,f59]) ).
thf(f59,plain,
( ( $false = sK4 )
| ~ spl2_4 ),
inference(avatar_component_clause,[status(thm)],[f57]) ).
thf(f57,definition,
( spl2_4
<=> ( $false = sK4 ) ),
introduced(definition,[new_symbols(naming,[spl2_4])],[avatar_definition]) ).
thf(f46,plain,
( ( ( sK1 @ sK4 )
= $true )
| ~ spl2_1 ),
inference(avatar_component_clause,[status(thm)],[f44]) ).
thf(f44,definition,
( spl2_1
<=> ( ( sK1 @ sK4 )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl2_1])],[avatar_definition]) ).
thf(f553,plain,
( ~ spl2_21
| ~ spl2_24 ),
inference(avatar_contradiction_clause,[status(thm)],[f552]) ).
thf(f552,plain,
( $false
| ~ spl2_21
| ~ spl2_24 ),
inference(trivial_inequality_removal,[status(thm)],[f549]) ).
thf(f549,plain,
( ( $true = $false )
| ~ spl2_21
| ~ spl2_24 ),
inference(superposition,[status(thm)],[f475,f488]) ).
thf(f488,plain,
( ( $true = sK15 )
| ~ spl2_24 ),
inference(avatar_component_clause,[status(thm)],[f486]) ).
thf(f486,definition,
( spl2_24
<=> ( $true = sK15 ) ),
introduced(definition,[new_symbols(naming,[spl2_24])],[avatar_definition]) ).
thf(f475,plain,
( ( $false = sK15 )
| ~ spl2_21 ),
inference(avatar_component_clause,[status(thm)],[f473]) ).
thf(f536,plain,
( ~ spl2_1
| ~ spl2_4
| ~ spl2_21
| ~ spl2_23 ),
inference(avatar_contradiction_clause,[status(thm)],[f535]) ).
thf(f535,plain,
( $false
| ~ spl2_1
| ~ spl2_4
| ~ spl2_21
| ~ spl2_23 ),
inference(subsumption_resolution,[status(thm)],[f521,f475]) ).
thf(f521,plain,
( ( $false != sK15 )
| ~ spl2_1
| ~ spl2_4
| ~ spl2_23 ),
inference(trivial_inequality_removal,[status(thm)],[f506]) ).
thf(f506,plain,
( ( $true = $false )
| ( $false != sK15 )
| ~ spl2_1
| ~ spl2_4
| ~ spl2_23 ),
inference(constrained_superposition,[status(thm)],[f445,f484]) ).
thf(f484,plain,
( ( ( sK1 @ sK15 )
= $false )
| ~ spl2_23 ),
inference(avatar_component_clause,[status(thm)],[f482]) ).
thf(f482,definition,
( spl2_23
<=> ( ( sK1 @ sK15 )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl2_23])],[avatar_definition]) ).
thf(f489,plain,
( spl2_23
| spl2_24
| ~ spl2_5 ),
inference(avatar_split_clause,[status(thm)],[f470,f61,f486,f482]) ).
thf(f61,definition,
( spl2_5
<=> ( $false
= ( sK0 @ (~) ) ) ),
introduced(definition,[new_symbols(naming,[spl2_5])],[avatar_definition]) ).
thf(f470,plain,
( ( $true = sK15 )
| ( ( sK1 @ sK15 )
= $false )
| ~ spl2_5 ),
inference(not_proxy_clausification,[status(thm)],[f469]) ).
thf(f469,plain,
( ( ( ~ sK15 ) = $false )
| ( ( sK1 @ sK15 )
= $false )
| ~ spl2_5 ),
inference(binary_proxy_clausification,[status(thm)],[f467]) ).
thf(f467,plain,
( ( ( sK1 @ sK15 )
!= ( ~ sK15 ) )
| ~ spl2_5 ),
inference(negative_extensionality,[status(thm)],[f466]) ).
thf(f466,plain,
( ( sK1 != (~) )
| ~ spl2_5 ),
inference(trivial_inequality_removal,[status(thm)],[f461]) ).
thf(f461,plain,
( ( sK1 != (~) )
| ( $true = $false )
| ~ spl2_5 ),
inference(constrained_superposition,[status(thm)],[f63,f14]) ).
thf(f63,plain,
( ( $false
= ( sK0 @ (~) ) )
| ~ spl2_5 ),
inference(avatar_component_clause,[status(thm)],[f61]) ).
thf(f480,plain,
( spl2_21
| spl2_22
| ~ spl2_5 ),
inference(avatar_split_clause,[status(thm)],[f471,f61,f477,f473]) ).
thf(f471,plain,
( ( $false = sK15 )
| ( $true
= ( sK1 @ sK15 ) )
| ~ spl2_5 ),
inference(not_proxy_clausification,[status(thm)],[f468]) ).
thf(f468,plain,
( ( $true = ( ~ sK15 ) )
| ( $true
= ( sK1 @ sK15 ) )
| ~ spl2_5 ),
inference(binary_proxy_clausification,[status(thm)],[f467]) ).
thf(f439,plain,
( spl2_1
| ~ spl2_7
| ~ spl2_13
| ~ spl2_15 ),
inference(avatar_contradiction_clause,[status(thm)],[f438]) ).
thf(f438,plain,
( $false
| spl2_1
| ~ spl2_7
| ~ spl2_13
| ~ spl2_15 ),
inference(subsumption_resolution,[status(thm)],[f403,f359]) ).
thf(f359,plain,
( ( ( sK1 @ $true )
!= $true )
| spl2_1
| ~ spl2_7 ),
inference(superposition,[status(thm)],[f45,f72]) ).
thf(f72,plain,
( ( $true = sK4 )
| ~ spl2_7 ),
inference(avatar_component_clause,[status(thm)],[f70]) ).
thf(f70,definition,
( spl2_7
<=> ( $true = sK4 ) ),
introduced(definition,[new_symbols(naming,[spl2_7])],[avatar_definition]) ).
thf(f45,plain,
( ( ( sK1 @ sK4 )
!= $true )
| spl2_1 ),
inference(avatar_component_clause,[status(thm)],[f44]) ).
thf(f403,plain,
( ( ( sK1 @ $true )
= $true )
| ~ spl2_13
| ~ spl2_15 ),
inference(superposition,[status(thm)],[f128,f137]) ).
thf(f137,plain,
( ( $true = sK6 )
| ~ spl2_15 ),
inference(avatar_component_clause,[status(thm)],[f135]) ).
thf(f135,definition,
( spl2_15
<=> ( $true = sK6 ) ),
introduced(definition,[new_symbols(naming,[spl2_15])],[avatar_definition]) ).
thf(f128,plain,
( ( $true
= ( sK1 @ sK6 ) )
| ~ spl2_13 ),
inference(avatar_component_clause,[status(thm)],[f126]) ).
thf(f126,definition,
( spl2_13
<=> ( $true
= ( sK1 @ sK6 ) ) ),
introduced(definition,[new_symbols(naming,[spl2_13])],[avatar_definition]) ).
thf(f401,plain,
( ~ spl2_14
| ~ spl2_15 ),
inference(avatar_contradiction_clause,[status(thm)],[f400]) ).
thf(f400,plain,
( $false
| ~ spl2_14
| ~ spl2_15 ),
inference(trivial_inequality_removal,[status(thm)],[f397]) ).
thf(f397,plain,
( ( $true = $false )
| ~ spl2_14
| ~ spl2_15 ),
inference(superposition,[status(thm)],[f132,f137]) ).
thf(f132,plain,
( ( sK6 = $false )
| ~ spl2_14 ),
inference(avatar_component_clause,[status(thm)],[f130]) ).
thf(f130,definition,
( spl2_14
<=> ( sK6 = $false ) ),
introduced(definition,[new_symbols(naming,[spl2_14])],[avatar_definition]) ).
thf(f393,plain,
( spl2_15
| ~ spl2_2
| ~ spl2_16
| spl2_20 ),
inference(avatar_split_clause,[status(thm)],[f392,f354,f139,f48,f135]) ).
thf(f139,definition,
( spl2_16
<=> ( ( sK1 @ sK6 )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl2_16])],[avatar_definition]) ).
thf(f354,definition,
( spl2_20
<=> ( $true = sK10 ) ),
introduced(definition,[new_symbols(naming,[spl2_20])],[avatar_definition]) ).
thf(f392,plain,
( ( $true = sK6 )
| ~ spl2_2
| ~ spl2_16
| spl2_20 ),
inference(subsumption_resolution,[status(thm)],[f388,f355]) ).
thf(f355,plain,
( ( $true != sK10 )
| spl2_20 ),
inference(avatar_component_clause,[status(thm)],[f354]) ).
thf(f388,plain,
( ( $true = sK6 )
| ( $true = sK10 )
| ~ spl2_2
| ~ spl2_16 ),
inference(binary_proxy_clausification,[status(thm)],[f387]) ).
thf(f387,plain,
( ( sK6 != sK10 )
| ~ spl2_2
| ~ spl2_16 ),
inference(trivial_inequality_removal,[status(thm)],[f385]) ).
thf(f385,plain,
( ( $false != $false )
| ( sK6 != sK10 )
| ~ spl2_2
| ~ spl2_16 ),
inference(constrained_superposition,[status(thm)],[f235,f141]) ).
thf(f141,plain,
( ( ( sK1 @ sK6 )
= $false )
| ~ spl2_16 ),
inference(avatar_component_clause,[status(thm)],[f139]) ).
thf(f235,plain,
( ( ( sK1 @ sK10 )
!= $false )
| ~ spl2_2 ),
inference(beta_eta_normalization,[status(thm)],[f234]) ).
thf(f234,plain,
( ( ( ^ [Y0: $o] : $false
@ sK10 )
!= ( sK1 @ sK10 ) )
| ~ spl2_2 ),
inference(negative_extensionality,[status(thm)],[f228]) ).
thf(f228,plain,
( ( sK1
!= ( ^ [Y0: $o] : $false ) )
| ~ spl2_2 ),
inference(trivial_inequality_removal,[status(thm)],[f219]) ).
thf(f219,plain,
( ( sK1
!= ( ^ [Y0: $o] : $false ) )
| ( $true = $false )
| ~ spl2_2 ),
inference(constrained_superposition,[status(thm)],[f50,f14]) ).
thf(f50,plain,
( ( ( sK0
@ ^ [Y0: $o] : $false )
= $false )
| ~ spl2_2 ),
inference(avatar_component_clause,[status(thm)],[f48]) ).
thf(f381,plain,
( ~ spl2_20
| ~ spl2_2
| ~ spl2_7
| ~ spl2_8 ),
inference(avatar_split_clause,[status(thm)],[f380,f75,f70,f48,f354]) ).
thf(f75,definition,
( spl2_8
<=> ( ( sK1 @ sK4 )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl2_8])],[avatar_definition]) ).
thf(f380,plain,
( ( $true != sK10 )
| ~ spl2_2
| ~ spl2_7
| ~ spl2_8 ),
inference(trivial_inequality_removal,[status(thm)],[f378]) ).
thf(f378,plain,
( ( $false != $false )
| ( $true != sK10 )
| ~ spl2_2
| ~ spl2_7
| ~ spl2_8 ),
inference(constrained_superposition,[status(thm)],[f235,f360]) ).
thf(f360,plain,
( ( ( sK1 @ $true )
= $false )
| ~ spl2_7
| ~ spl2_8 ),
inference(superposition,[status(thm)],[f77,f72]) ).
thf(f77,plain,
( ( ( sK1 @ sK4 )
= $false )
| ~ spl2_8 ),
inference(avatar_component_clause,[status(thm)],[f75]) ).
thf(f347,plain,
( ~ spl2_17
| ~ spl2_18 ),
inference(avatar_contradiction_clause,[status(thm)],[f346]) ).
thf(f346,plain,
( $false
| ~ spl2_17
| ~ spl2_18 ),
inference(trivial_inequality_removal,[status(thm)],[f343]) ).
thf(f343,plain,
( ( $true = $false )
| ~ spl2_17
| ~ spl2_18 ),
inference(superposition,[status(thm)],[f337,f318]) ).
thf(f318,plain,
( ( sK13 = $false )
| ~ spl2_17 ),
inference(avatar_component_clause,[status(thm)],[f316]) ).
thf(f316,definition,
( spl2_17
<=> ( sK13 = $false ) ),
introduced(definition,[new_symbols(naming,[spl2_17])],[avatar_definition]) ).
thf(f337,plain,
( ( sK13 = $true )
| ~ spl2_18 ),
inference(avatar_component_clause,[status(thm)],[f335]) ).
thf(f335,definition,
( spl2_18
<=> ( sK13 = $true ) ),
introduced(definition,[new_symbols(naming,[spl2_18])],[avatar_definition]) ).
thf(f341,plain,
( spl2_18
| spl2_5
| ~ spl2_6
| spl2_10 ),
inference(avatar_split_clause,[status(thm)],[f340,f83,f66,f61,f335]) ).
thf(f66,definition,
( spl2_6
<=> ( $true
= ( sK0 @ (~) ) ) ),
introduced(definition,[new_symbols(naming,[spl2_6])],[avatar_definition]) ).
thf(f340,plain,
( ( sK13 = $true )
| spl2_5
| ~ spl2_6
| spl2_10 ),
inference(subsumption_resolution,[status(thm)],[f339,f62]) ).
thf(f62,plain,
( ( $false
!= ( sK0 @ (~) ) )
| spl2_5 ),
inference(avatar_component_clause,[status(thm)],[f61]) ).
thf(f339,plain,
( ( sK13 = $true )
| ( $false
= ( sK0 @ (~) ) )
| ~ spl2_6
| spl2_10 ),
inference(subsumption_resolution,[status(thm)],[f274,f84]) ).
thf(f84,plain,
( ( ( sK0
@ ^ [Y0: $o] : $false )
!= $true )
| spl2_10 ),
inference(avatar_component_clause,[status(thm)],[f83]) ).
thf(f274,plain,
( ( ( sK0
@ ^ [Y0: $o] : $false )
= $true )
| ( sK13 = $true )
| ( $false
= ( sK0 @ (~) ) )
| ~ spl2_6 ),
inference(duplicate_literal_removal,[status(thm)],[f273]) ).
thf(f273,plain,
( ( $false
= ( sK0 @ (~) ) )
| ( ( sK0
@ ^ [Y0: $o] : $false )
= $true )
| ( sK13 = $true )
| ( sK13 = $true )
| ~ spl2_6 ),
inference(not_proxy_clausification,[status(thm)],[f272]) ).
thf(f272,plain,
( ( ( sK0
@ ^ [Y0: $o] : $false )
= $true )
| ( ( ~ sK13 ) = $false )
| ( sK13 = $true )
| ( $false
= ( sK0 @ (~) ) )
| ~ spl2_6 ),
inference(binary_proxy_clausification,[status(thm)],[f270]) ).
thf(f270,plain,
( ( ( ~ sK13 )
!= ( sK0 @ (~) ) )
| ( sK13 = $true )
| ( ( sK0
@ ^ [Y0: $o] : $false )
= $true )
| ~ spl2_6 ),
inference(equality_proxy_clausification,[status(thm)],[f269]) ).
thf(f269,plain,
( ( sK13 = $true )
| ( ( sK0
@ ^ [Y0: $o] : $false )
= $true )
| ( ( ( sK0 @ (~) )
= ( ~ sK13 ) )
= $false )
| ~ spl2_6 ),
inference(not_proxy_clausification,[status(thm)],[f268]) ).
thf(f268,plain,
( ( sK13 = $true )
| ( $false
= ( ~ ( sK0
@ ^ [Y0: $o] : $false ) ) )
| ( ( ( sK0 @ (~) )
= ( ~ sK13 ) )
= $false )
| ~ spl2_6 ),
inference(binary_proxy_clausification,[status(thm)],[f266]) ).
thf(f266,plain,
( ( sK13 = $true )
| ( ( ( ( sK0 @ (~) )
= ( ~ sK13 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) )
= $false )
| ( $false
= ( ~ ( sK0
@ ^ [Y0: $o] : $false ) ) )
| ~ spl2_6 ),
inference(binary_proxy_clausification,[status(thm)],[f265]) ).
thf(f265,plain,
( ( ( ( ( ( sK0 @ (~) )
= ( ~ sK13 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) )
& ~ ( sK0
@ ^ [Y0: $o] : $false ) )
= $false )
| ( sK13 = $true )
| ~ spl2_6 ),
inference(not_proxy_clausification,[status(thm)],[f264]) ).
thf(f264,plain,
( ( ( ~ sK13 ) = $false )
| ( ( ( ( ( sK0 @ (~) )
= ( ~ sK13 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) )
& ~ ( sK0
@ ^ [Y0: $o] : $false ) )
= $false )
| ~ spl2_6 ),
inference(binary_proxy_clausification,[status(thm)],[f262]) ).
thf(f262,plain,
( ( ( ( ( ( sK0 @ (~) )
= ( ~ sK13 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) )
& ~ ( sK0
@ ^ [Y0: $o] : $false ) )
!= ( ~ sK13 ) )
| ~ spl2_6 ),
inference(beta_eta_normalization,[status(thm)],[f261]) ).
thf(f261,plain,
( ( ( ^ [Y0: $o] :
( ( ( ( sK0 @ (~) )
= ( ~ Y0 ) )
| ( sK0
@ ^ [Y1: $o] : $true ) )
& ~ ( sK0
@ ^ [Y1: $o] : $false ) )
@ sK13 )
!= ( ~ sK13 ) )
| ~ spl2_6 ),
inference(negative_extensionality,[status(thm)],[f158]) ).
thf(f158,plain,
( ~ !=(^ [Y0: $o] :
( ( ( ( sK0 @ (~) )
= ( ~ Y0 ) )
| ( sK0
@ ^ [Y1: $o] : $true ) )
& ~ ( sK0
@ ^ [Y1: $o] : $false ) ))
| ~ spl2_6 ),
inference(trivial_inequality_removal,[status(thm)],[f154]) ).
thf(f154,plain,
( ( $true != $true )
| ~ !=(^ [Y0: $o] :
( ( ( ( sK0 @ (~) )
= ( ~ Y0 ) )
| ( sK0
@ ^ [Y1: $o] : $true ) )
& ~ ( sK0
@ ^ [Y1: $o] : $false ) ))
| ~ spl2_6 ),
inference(constrained_superposition,[status(thm)],[f17,f68]) ).
thf(f68,plain,
( ( $true
= ( sK0 @ (~) ) )
| ~ spl2_6 ),
inference(avatar_component_clause,[status(thm)],[f66]) ).
thf(f331,plain,
( ~ spl2_5
| ~ spl2_6 ),
inference(avatar_contradiction_clause,[status(thm)],[f330]) ).
thf(f330,plain,
( $false
| ~ spl2_5
| ~ spl2_6 ),
inference(trivial_inequality_removal,[status(thm)],[f320]) ).
thf(f320,plain,
( ( $true = $false )
| ~ spl2_5
| ~ spl2_6 ),
inference(superposition,[status(thm)],[f63,f68]) ).
thf(f319,plain,
( spl2_17
| spl2_5
| spl2_3
| ~ spl2_6 ),
inference(avatar_split_clause,[status(thm)],[f307,f66,f53,f61,f316]) ).
thf(f53,definition,
( spl2_3
<=> ( $true
= ( sK0
@ ^ [Y0: $o] : $true ) ) ),
introduced(definition,[new_symbols(naming,[spl2_3])],[avatar_definition]) ).
thf(f307,plain,
( ( $false
= ( sK0 @ (~) ) )
| ( sK13 = $false )
| spl2_3
| ~ spl2_6 ),
inference(subsumption_resolution,[status(thm)],[f286,f54]) ).
thf(f54,plain,
( ( $true
!= ( sK0
@ ^ [Y0: $o] : $true ) )
| spl2_3 ),
inference(avatar_component_clause,[status(thm)],[f53]) ).
thf(f286,plain,
( ( $true
= ( sK0
@ ^ [Y0: $o] : $true ) )
| ( sK13 = $false )
| ( $false
= ( sK0 @ (~) ) )
| ~ spl2_6 ),
inference(duplicate_literal_removal,[status(thm)],[f285]) ).
thf(f285,plain,
( ( $false
= ( sK0 @ (~) ) )
| ( sK13 = $false )
| ( $true
= ( sK0
@ ^ [Y0: $o] : $true ) )
| ( sK13 = $false )
| ~ spl2_6 ),
inference(not_proxy_clausification,[status(thm)],[f282]) ).
thf(f282,plain,
( ( $false
= ( sK0 @ (~) ) )
| ( $true = ( ~ sK13 ) )
| ( sK13 = $false )
| ( $true
= ( sK0
@ ^ [Y0: $o] : $true ) )
| ~ spl2_6 ),
inference(binary_proxy_clausification,[status(thm)],[f281]) ).
thf(f281,plain,
( ( ( ~ sK13 )
= ( sK0 @ (~) ) )
| ( sK13 = $false )
| ( $true
= ( sK0
@ ^ [Y0: $o] : $true ) )
| ~ spl2_6 ),
inference(equality_proxy_clausification,[status(thm)],[f280]) ).
thf(f280,plain,
( ( $true
= ( sK0
@ ^ [Y0: $o] : $true ) )
| ( $true
= ( ( sK0 @ (~) )
= ( ~ sK13 ) ) )
| ( sK13 = $false )
| ~ spl2_6 ),
inference(binary_proxy_clausification,[status(thm)],[f279]) ).
thf(f279,plain,
( ( sK13 = $false )
| ( $true
= ( ( ( sK0 @ (~) )
= ( ~ sK13 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) ) )
| ~ spl2_6 ),
inference(not_proxy_clausification,[status(thm)],[f278]) ).
thf(f278,plain,
( ( $true = ( ~ sK13 ) )
| ( $true
= ( ( ( sK0 @ (~) )
= ( ~ sK13 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) ) )
| ~ spl2_6 ),
inference(binary_proxy_clausification,[status(thm)],[f263]) ).
thf(f263,plain,
( ( $true
= ( ( ( ( sK0 @ (~) )
= ( ~ sK13 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) )
& ~ ( sK0
@ ^ [Y0: $o] : $false ) ) )
| ( $true = ( ~ sK13 ) )
| ~ spl2_6 ),
inference(binary_proxy_clausification,[status(thm)],[f262]) ).
thf(f304,plain,
( ~ spl2_3
| spl2_9
| spl2_10 ),
inference(avatar_contradiction_clause,[status(thm)],[f303]) ).
thf(f303,plain,
( $false
| ~ spl2_3
| spl2_9
| spl2_10 ),
inference(subsumption_resolution,[status(thm)],[f302,f84]) ).
thf(f302,plain,
( ( ( sK0
@ ^ [Y0: $o] : $false )
= $true )
| ~ spl2_3
| spl2_9 ),
inference(subsumption_resolution,[status(thm)],[f295,f80]) ).
thf(f80,plain,
( ( ( sK0
@ ^ [Y0: $o] : $true )
!= $false )
| spl2_9 ),
inference(avatar_component_clause,[status(thm)],[f79]) ).
thf(f295,plain,
( ( ( sK0
@ ^ [Y0: $o] : $true )
= $false )
| ( ( sK0
@ ^ [Y0: $o] : $false )
= $true )
| ~ spl2_3 ),
inference(binary_proxy_clausification,[status(thm)],[f294]) ).
thf(f294,plain,
( ( ( ( ( sK0 @ (~) )
= ( ~ sK14 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) )
= $false )
| ( ( sK0
@ ^ [Y0: $o] : $false )
= $true )
| ~ spl2_3 ),
inference(not_proxy_clausification,[status(thm)],[f293]) ).
thf(f293,plain,
( ( $false
= ( ~ ( sK0
@ ^ [Y0: $o] : $false ) ) )
| ( ( ( ( sK0 @ (~) )
= ( ~ sK14 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) )
= $false )
| ~ spl2_3 ),
inference(binary_proxy_clausification,[status(thm)],[f292]) ).
thf(f292,plain,
( ( $true
!= ( ( ( ( sK0 @ (~) )
= ( ~ sK14 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) )
& ~ ( sK0
@ ^ [Y0: $o] : $false ) ) )
| ~ spl2_3 ),
inference(beta_eta_normalization,[status(thm)],[f291]) ).
thf(f291,plain,
( ( ( ^ [Y0: $o] :
( ( ( ( sK0 @ (~) )
= ( ~ Y0 ) )
| ( sK0
@ ^ [Y1: $o] : $true ) )
& ~ ( sK0
@ ^ [Y1: $o] : $false ) )
@ sK14 )
!= ( ^ [Y0: $o] : $true
@ sK14 ) )
| ~ spl2_3 ),
inference(negative_extensionality,[status(thm)],[f171]) ).
thf(f171,plain,
( ( ( ^ [Y0: $o] : $true )
!= ( ^ [Y0: $o] :
( ( ( ( sK0 @ (~) )
= ( ~ Y0 ) )
| ( sK0
@ ^ [Y1: $o] : $true ) )
& ~ ( sK0
@ ^ [Y1: $o] : $false ) ) ) )
| ~ spl2_3 ),
inference(trivial_inequality_removal,[status(thm)],[f167]) ).
thf(f167,plain,
( ( $true != $true )
| ( ( ^ [Y0: $o] : $true )
!= ( ^ [Y0: $o] :
( ( ( ( sK0 @ (~) )
= ( ~ Y0 ) )
| ( sK0
@ ^ [Y1: $o] : $true ) )
& ~ ( sK0
@ ^ [Y1: $o] : $false ) ) ) )
| ~ spl2_3 ),
inference(constrained_superposition,[status(thm)],[f17,f55]) ).
thf(f55,plain,
( ( $true
= ( sK0
@ ^ [Y0: $o] : $true ) )
| ~ spl2_3 ),
inference(avatar_component_clause,[status(thm)],[f53]) ).
thf(f210,plain,
( ~ spl2_4
| ~ spl2_7 ),
inference(avatar_contradiction_clause,[status(thm)],[f209]) ).
thf(f209,plain,
( $false
| ~ spl2_4
| ~ spl2_7 ),
inference(trivial_inequality_removal,[status(thm)],[f206]) ).
thf(f206,plain,
( ( $true = $false )
| ~ spl2_4
| ~ spl2_7 ),
inference(superposition,[status(thm)],[f72,f59]) ).
thf(f203,plain,
( ~ spl2_1
| ~ spl2_8 ),
inference(avatar_contradiction_clause,[status(thm)],[f202]) ).
thf(f202,plain,
( $false
| ~ spl2_1
| ~ spl2_8 ),
inference(trivial_inequality_removal,[status(thm)],[f199]) ).
thf(f199,plain,
( ( $true = $false )
| ~ spl2_1
| ~ spl2_8 ),
inference(superposition,[status(thm)],[f46,f77]) ).
thf(f195,plain,
( ~ spl2_2
| ~ spl2_10 ),
inference(avatar_contradiction_clause,[status(thm)],[f194]) ).
thf(f194,plain,
( $false
| ~ spl2_2
| ~ spl2_10 ),
inference(trivial_inequality_removal,[status(thm)],[f186]) ).
thf(f186,plain,
( ( $true = $false )
| ~ spl2_2
| ~ spl2_10 ),
inference(superposition,[status(thm)],[f85,f50]) ).
thf(f175,plain,
( ~ spl2_3
| ~ spl2_9 ),
inference(avatar_contradiction_clause,[status(thm)],[f174]) ).
thf(f174,plain,
( $false
| ~ spl2_3
| ~ spl2_9 ),
inference(trivial_inequality_removal,[status(thm)],[f170]) ).
thf(f170,plain,
( ( $true = $false )
| ~ spl2_3
| ~ spl2_9 ),
inference(superposition,[status(thm)],[f81,f55]) ).
thf(f142,plain,
( spl2_15
| spl2_16
| ~ spl2_5 ),
inference(avatar_split_clause,[status(thm)],[f123,f61,f139,f135]) ).
thf(f123,plain,
( ( ( sK1 @ sK6 )
= $false )
| ( $true = sK6 )
| ~ spl2_5 ),
inference(not_proxy_clausification,[status(thm)],[f122]) ).
thf(f122,plain,
( ( ( ~ sK6 ) = $false )
| ( ( sK1 @ sK6 )
= $false )
| ~ spl2_5 ),
inference(binary_proxy_clausification,[status(thm)],[f120]) ).
thf(f120,plain,
( ( ( ~ sK6 )
!= ( sK1 @ sK6 ) )
| ~ spl2_5 ),
inference(negative_extensionality,[status(thm)],[f114]) ).
thf(f114,plain,
( ( sK1 != (~) )
| ~ spl2_5 ),
inference(trivial_inequality_removal,[status(thm)],[f110]) ).
thf(f110,plain,
( ( sK1 != (~) )
| ( $true = $false )
| ~ spl2_5 ),
inference(constrained_superposition,[status(thm)],[f63,f14]) ).
thf(f133,plain,
( spl2_13
| spl2_14
| ~ spl2_5 ),
inference(avatar_split_clause,[status(thm)],[f124,f61,f130,f126]) ).
thf(f124,plain,
( ( $true
= ( sK1 @ sK6 ) )
| ( sK6 = $false )
| ~ spl2_5 ),
inference(not_proxy_clausification,[status(thm)],[f121]) ).
thf(f121,plain,
( ( ( ~ sK6 ) = $true )
| ( $true
= ( sK1 @ sK6 ) )
| ~ spl2_5 ),
inference(binary_proxy_clausification,[status(thm)],[f120]) ).
thf(f88,plain,
( spl2_7
| spl2_8
| spl2_5
| spl2_10 ),
inference(avatar_split_clause,[status(thm)],[f31,f83,f61,f75,f70]) ).
thf(f31,plain,
( ( ( sK1 @ sK4 )
= $false )
| ( ( sK0
@ ^ [Y0: $o] : $false )
= $true )
| ( $true = sK4 )
| ( $false
= ( sK0 @ (~) ) ) ),
inference(not_proxy_clausification,[status(thm)],[f30]) ).
thf(f30,plain,
( ( $false
= ( sK0 @ (~) ) )
| ( ( sK1 @ sK4 )
= $false )
| ( ( sK0
@ ^ [Y0: $o] : $false )
= $true )
| ( ( ~ sK4 ) = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f28]) ).
thf(f28,plain,
( ( ( sK0
@ ^ [Y0: $o] : $false )
= $true )
| ( ( sK1 @ sK4 )
= $false )
| ( ( ~ sK4 )
!= ( sK0 @ (~) ) ) ),
inference(not_proxy_clausification,[status(thm)],[f27]) ).
thf(f27,plain,
( ( $false
= ( ~ ( sK0
@ ^ [Y0: $o] : $false ) ) )
| ( ( ~ sK4 )
!= ( sK0 @ (~) ) )
| ( ( sK1 @ sK4 )
= $false ) ),
inference(equality_proxy_clausification,[status(thm)],[f26]) ).
thf(f26,plain,
( ( ( sK1 @ sK4 )
= $false )
| ( $false
= ( ( sK0 @ (~) )
= ( ~ sK4 ) ) )
| ( $false
= ( ~ ( sK0
@ ^ [Y0: $o] : $false ) ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f24]) ).
thf(f24,plain,
( ( ( sK1 @ sK4 )
= $false )
| ( ( ( ( sK0 @ (~) )
= ( ~ sK4 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) )
= $false )
| ( $false
= ( ~ ( sK0
@ ^ [Y0: $o] : $false ) ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f23]) ).
thf(f23,plain,
( ( ( ( ( ( sK0 @ (~) )
= ( ~ sK4 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) )
& ~ ( sK0
@ ^ [Y0: $o] : $false ) )
= $false )
| ( ( sK1 @ sK4 )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f21]) ).
thf(f21,plain,
( ( sK1 @ sK4 )
!= ( ( ( ( sK0 @ (~) )
= ( ~ sK4 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) )
& ~ ( sK0
@ ^ [Y0: $o] : $false ) ) ),
inference(beta_eta_normalization,[status(thm)],[f20]) ).
thf(f20,plain,
( ( sK1 @ sK4 )
!= ( ^ [Y0: $o] :
( ( ( ( sK0 @ (~) )
= ( ~ Y0 ) )
| ( sK0
@ ^ [Y1: $o] : $true ) )
& ~ ( sK0
@ ^ [Y1: $o] : $false ) )
@ sK4 ) ),
inference(negative_extensionality,[status(thm)],[f19]) ).
thf(f19,plain,
( sK1
!= ( ^ [Y0: $o] :
( ( ( ( sK0 @ (~) )
= ( ~ Y0 ) )
| ( sK0
@ ^ [Y1: $o] : $true ) )
& ~ ( sK0
@ ^ [Y1: $o] : $false ) ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f18]) ).
thf(f18,plain,
( ( sK1
!= ( ^ [Y0: $o] :
( ( ( ( sK0 @ (~) )
= ( ~ Y0 ) )
| ( sK0
@ ^ [Y1: $o] : $true ) )
& ~ ( sK0
@ ^ [Y1: $o] : $false ) ) ) )
| ( $true != $true ) ),
inference(constrained_superposition,[status(thm)],[f17,f14]) ).
thf(f87,plain,
( spl2_8
| spl2_4
| spl2_10
| spl2_6 ),
inference(avatar_split_clause,[status(thm)],[f32,f66,f83,f57,f75]) ).
thf(f32,plain,
( ( ( sK1 @ sK4 )
= $false )
| ( $true
= ( sK0 @ (~) ) )
| ( ( sK0
@ ^ [Y0: $o] : $false )
= $true )
| ( $false = sK4 ) ),
inference(not_proxy_clausification,[status(thm)],[f29]) ).
thf(f29,plain,
( ( ( sK1 @ sK4 )
= $false )
| ( $true
= ( sK0 @ (~) ) )
| ( $true = ( ~ sK4 ) )
| ( ( sK0
@ ^ [Y0: $o] : $false )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f28]) ).
thf(f86,plain,
( spl2_8
| spl2_9
| spl2_10 ),
inference(avatar_split_clause,[status(thm)],[f33,f83,f79,f75]) ).
thf(f33,plain,
( ( ( sK0
@ ^ [Y0: $o] : $false )
= $true )
| ( ( sK1 @ sK4 )
= $false )
| ( ( sK0
@ ^ [Y0: $o] : $true )
= $false ) ),
inference(not_proxy_clausification,[status(thm)],[f25]) ).
thf(f25,plain,
( ( $false
= ( ~ ( sK0
@ ^ [Y0: $o] : $false ) ) )
| ( ( sK0
@ ^ [Y0: $o] : $true )
= $false )
| ( ( sK1 @ sK4 )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f24]) ).
thf(f73,plain,
( spl2_6
| spl2_7
| spl2_1
| spl2_3 ),
inference(avatar_split_clause,[status(thm)],[f40,f53,f44,f70,f66]) ).
thf(f40,plain,
( ( $true
= ( sK0 @ (~) ) )
| ( $true
= ( sK0
@ ^ [Y0: $o] : $true ) )
| ( ( sK1 @ sK4 )
= $true )
| ( $true = sK4 ) ),
inference(not_proxy_clausification,[status(thm)],[f39]) ).
thf(f39,plain,
( ( $true
= ( sK0 @ (~) ) )
| ( ( ~ sK4 ) = $false )
| ( ( sK1 @ sK4 )
= $true )
| ( $true
= ( sK0
@ ^ [Y0: $o] : $true ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f37]) ).
thf(f37,plain,
( ( ( ~ sK4 )
= ( sK0 @ (~) ) )
| ( ( sK1 @ sK4 )
= $true )
| ( $true
= ( sK0
@ ^ [Y0: $o] : $true ) ) ),
inference(equality_proxy_clausification,[status(thm)],[f36]) ).
thf(f36,plain,
( ( $true
= ( ( sK0 @ (~) )
= ( ~ sK4 ) ) )
| ( $true
= ( sK0
@ ^ [Y0: $o] : $true ) )
| ( ( sK1 @ sK4 )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f35]) ).
thf(f35,plain,
( ( $true
= ( ( ( sK0 @ (~) )
= ( ~ sK4 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) ) )
| ( ( sK1 @ sK4 )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f22]) ).
thf(f22,plain,
( ( $true
= ( ( ( ( sK0 @ (~) )
= ( ~ sK4 ) )
| ( sK0
@ ^ [Y0: $o] : $true ) )
& ~ ( sK0
@ ^ [Y0: $o] : $false ) ) )
| ( ( sK1 @ sK4 )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f21]) ).
thf(f64,plain,
( spl2_1
| spl2_3
| spl2_4
| spl2_5 ),
inference(avatar_split_clause,[status(thm)],[f41,f61,f57,f53,f44]) ).
thf(f41,plain,
( ( $false
= ( sK0 @ (~) ) )
| ( $false = sK4 )
| ( ( sK1 @ sK4 )
= $true )
| ( $true
= ( sK0
@ ^ [Y0: $o] : $true ) ) ),
inference(not_proxy_clausification,[status(thm)],[f38]) ).
thf(f38,plain,
( ( $false
= ( sK0 @ (~) ) )
| ( $true
= ( sK0
@ ^ [Y0: $o] : $true ) )
| ( ( sK1 @ sK4 )
= $true )
| ( $true = ( ~ sK4 ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f37]) ).
thf(f51,plain,
( spl2_1
| spl2_2 ),
inference(avatar_split_clause,[status(thm)],[f42,f48,f44]) ).
thf(f42,plain,
( ( ( sK0
@ ^ [Y0: $o] : $false )
= $false )
| ( ( sK1 @ sK4 )
= $true ) ),
inference(not_proxy_clausification,[status(thm)],[f34]) ).
thf(f34,plain,
( ( $true
= ( ~ ( sK0
@ ^ [Y0: $o] : $false ) ) )
| ( ( sK1 @ sK4 )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f22]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : SYO515^1 : TPTP v9.2.1. Bugfixed v9.2.1.
% 0.00/0.09 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.29 % Computer : n024.cluster.edu
% 0.11/0.29 % Model : x86_64 x86_64
% 0.11/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.29 % Memory : 8042.1875MB
% 0.11/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.29 % CPULimit : 300
% 0.11/0.29 % WCLimit : 300
% 0.11/0.29 % DateTime : Wed Feb 25 01:21:40 EST 2026
% 0.11/0.29 % CPUTime :
% 0.11/0.29 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.17/0.38 ---- Original DTF file ---
% 0.17/0.38 thf(spec,logic,$$dhol).
% 0.17/0.38 %------------------------------------------------------------------------------
% 0.17/0.38 % File : SYO515^1 : TPTP v9.2.1. Bugfixed v9.2.1.
% 0.17/0.38 % Domain : Syntactic
% 0.17/0.38 % Problem : A choice operator at type oo
% 0.17/0.38 % Version : Especial.
% 0.17/0.38 % English :
% 0.17/0.38
% 0.17/0.38 % Refs : [Bro09] Brown E. (2009), Email to Geoff Sutcliffe
% 0.17/0.38 % : [Hoe09] Hoeschele (2009), Towards a Semi-Automatic Higher-Orde
% 0.17/0.38 % Source : [Bro09]
% 0.17/0.38 % Names : choiceoo1 [Bro09]
% 0.17/0.38
% 0.17/0.38 % Status : Theorem
% 0.17/0.38 % Rating : ? v9.2.1
% 0.17/0.38 % Syntax : Number of formulae : 3 ( 2 unt; 1 typ; 1 def)
% 0.17/0.38 % Number of atoms : 6 ( 2 equ; 0 cnn)
% 0.17/0.38 % Maximal formula atoms : 1 ( 3 avg)
% 0.17/0.38 % Number of connectives : 12 ( 3 ~; 1 |; 1 &; 6 @)
% 0.17/0.38 % ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% 0.17/0.38 % Maximal formula depth : 5 ( 3 avg)
% 0.17/0.38 % Number of types : 1 ( 0 usr)
% 0.17/0.38 % Number of type conns : 9 ( 9 >; 0 *; 0 +; 0 <<)
% 0.17/0.38 % Number of symbols : 4 ( 1 usr; 2 con; 0-2 aty)
% 0.17/0.38 % Number of variables : 7 ( 5 ^; 1 !; 1 ?; 7 :)
% 0.17/0.38 % SPC : TH0_THM_EQU_NAR
% 0.17/0.38
% 0.17/0.38 % Comments :
% 0.17/0.38 % Bugfixes : v5.2.0 - Definition of t converted to =
% 0.17/0.38 % Bugfixes : Added ()s around negated sides of equations.
% 0.17/0.38 %------------------------------------------------------------------------------
% 0.17/0.38 thf(t_type,type,
% 0.17/0.38 t: ( ( $o > $o ) > $o ) > $o > $o ).
% 0.17/0.38
% 0.17/0.38 thf(t,definition,
% 0.17/0.38 ( t
% 0.17/0.38 = ( ^ [P: ( $o > $o ) > $o,X: $o] :
% 0.17/0.38 ( ~ ( P
% 0.17/0.38 @ ^ [X: $o] : $false )
% 0.17/0.38 & ( ( P
% 0.17/0.38 @ ^ [X: $o] : $true )
% 0.17/0.38 | ( ( P
% 0.17/0.38 @ ^ [X: $o] : ~ X )
% 0.17/0.38 = ( ~ X ) ) ) ) ) ) ).
% 0.17/0.38
% 0.17/0.38 thf(choiceoo1,conjecture,
% 0.17/0.38 ! [P: ( $o > $o ) > $o] :
% 0.17/0.38 ( ? [Y: $o > $o] : ( P @ Y )
% 0.17/0.38 => ( P @ ( t @ P ) ) ) ).
% 0.17/0.38
% 0.17/0.38 %------------------------------------------------------------------------------
% 0.17/0.38 ------------------------
% 1.34/1.29 ---- Embedded in THF ---
% 1.34/1.29 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.34/1.29 %%% Generated on Wed Feb 25 01:21:41 EST 2026
% 1.34/1.29 %%% using '$$dhol' embedding, version 1.3.0.
% 1.34/1.29 %%% Logic specification used:
% 1.34/1.29 %%% thf(spec, logic, $$dhol).
% 1.34/1.29
% 1.34/1.29 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.EKm7Nwuf6V/DTF2DTF30244.p
% See solution above
% 1.34/1.29 ------------------------
% 1.53/1.30 ---- Cleaned THF ---
% 1.53/1.30 thf(t_type,type,
% 1.53/1.30 t: ( ( $o > $o ) > $o ) > $o > $o ).
% 1.53/1.30
% 1.53/1.30 thf(t,definition,
% 1.53/1.30 ( t
% 1.53/1.30 = ( ^ [P: ( $o > $o ) > $o,X: $o] :
% 1.53/1.30 ( ~ ( P
% 1.53/1.30 @ ^ [X: $o] : $false )
% 1.53/1.30 & ( ( P
% 1.53/1.30 @ ^ [X: $o] : $true )
% 1.53/1.30 | ( ( P
% 1.53/1.30 @ ^ [X: $o] : ~ X )
% 1.53/1.30 = ~ X ) ) ) ) ) ).
% 1.53/1.30
% 1.53/1.30 thf(choiceoo1,conjecture,
% 1.53/1.30 ! [P: ( $o > $o ) > $o] :
% 1.53/1.30 ( ? [Y: $o > $o] : ( P @ Y )
% 1.53/1.30 => ( P @ ( t @ P ) ) ) ).
% 1.53/1.30 ------------------------
% 1.53/1.32 % (30345)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_30244 for (3000ds/2Mi)
% 1.53/1.32 % (30347)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_30244 for (3000ds/18Mi)
% 1.53/1.32 % (30343)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_30244 for (3000ds/27Mi)
% 1.53/1.32 % (30341)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_30244 for (3000ds/183Mi)
% 1.53/1.32 % (30344)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_30244 for (3000ds/2Mi)
% 1.53/1.32 % (30342)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_30244 for (3000ds/4Mi)
% 1.53/1.32 % (30346)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_30244 for (3000ds/275Mi)
% 1.53/1.32 % (30346)Refutation not found, incomplete strategy
% 1.53/1.32 % (30346)------------------------------
% 1.53/1.32 % (30346)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.53/1.32 % (30344)Instruction limit reached!
% 1.53/1.32 % (30344)------------------------------
% 1.53/1.32 % (30344)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.53/1.32 % (30344)Termination reason: Unknown
% 1.53/1.32 % (30344)Termination phase: Saturation
% 1.53/1.32
% 1.53/1.32 % (30344)Memory used [KB]: 5500
% 1.53/1.32 % (30344)Time elapsed: 0.003 s
% 1.53/1.32 % (30344)Instructions burned: 2 (million)
% 1.53/1.32 % (30344)------------------------------
% 1.53/1.32 % (30344)------------------------------
% 1.53/1.32 % (30346)Termination reason: Refutation not found, incomplete strategy
% 1.53/1.32
% 1.53/1.32 % (30345)Instruction limit reached!
% 1.53/1.32 % (30345)------------------------------
% 1.53/1.32 % (30345)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.53/1.32 % (30345)Termination reason: Unknown
% 1.53/1.32 % (30345)Termination phase: Saturation
% 1.53/1.32
% 1.53/1.32 % (30345)Memory used [KB]: 5500
% 1.53/1.32 % (30345)Time elapsed: 0.003 s
% 1.53/1.32 % (30345)Instructions burned: 2 (million)
% 1.53/1.32 % (30345)------------------------------
% 1.53/1.32 % (30345)------------------------------
% 1.53/1.32
% 1.53/1.32 % (30346)Memory used [KB]: 5500
% 1.53/1.32 % (30346)Time elapsed: 0.003 s
% 1.53/1.32 % (30346)Instructions burned: 1 (million)
% 1.53/1.32 % (30346)------------------------------
% 1.53/1.32 % (30346)------------------------------
% 1.53/1.32 % (30343)Refutation not found, incomplete strategy
% 1.53/1.32 % (30343)------------------------------
% 1.53/1.32 % (30343)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.53/1.32 % (30343)Termination reason: Refutation not found, incomplete strategy
% 1.53/1.32
% 1.53/1.32
% 1.53/1.32 % (30343)Memory used [KB]: 5500
% 1.53/1.32 % (30343)Time elapsed: 0.003 s
% 1.53/1.32 % (30343)Instructions burned: 2 (million)
% 1.53/1.32 % (30343)------------------------------
% 1.53/1.32 % (30343)------------------------------
% 1.53/1.32 % (30342)Refutation not found, incomplete strategy
% 1.53/1.32 % (30342)------------------------------
% 1.53/1.32 % (30342)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.53/1.32 % (30342)Termination reason: Refutation not found, incomplete strategy
% 1.53/1.32
% 1.53/1.32
% 1.53/1.32 % (30342)Memory used [KB]: 5500
% 1.53/1.32 % (30342)Time elapsed: 0.003 s
% 1.53/1.32 % (30342)Instructions burned: 2 (million)
% 1.53/1.32 % (30342)------------------------------
% 1.53/1.32 % (30342)------------------------------
% 1.53/1.33 % (30347)Refutation not found, incomplete strategy
% 1.53/1.33 % (30347)------------------------------
% 1.53/1.33 % (30347)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.53/1.33 % (30347)Termination reason: Refutation not found, incomplete strategy
% 1.53/1.33
% 1.53/1.33
% 1.53/1.33 % (30347)Memory used [KB]: 5628
% 1.53/1.33 % (30347)Time elapsed: 0.010 s
% 1.53/1.33 % (30347)Instructions burned: 15 (million)
% 1.53/1.33 % (30347)------------------------------
% 1.53/1.33 % (30347)------------------------------
% 1.53/1.33 % (30349)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_30244 for (2999ds/37Mi)
% 1.53/1.33 % (30348)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_30244 for (2999ds/3Mi)
% 1.53/1.33 % (30350)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_30244 for (2999ds/15Mi)
% 1.53/1.33 % (30351)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_30244 for (2999ds/3Mi)
% 1.53/1.33 % (30352)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_30244 for (2999ds/1041Mi)
% 1.53/1.34 % (30348)Instruction limit reached!
% 1.53/1.34 % (30348)------------------------------
% 1.53/1.34 % (30348)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.53/1.34 % (30348)Termination reason: Unknown
% 1.53/1.34 % (30348)Termination phase: Saturation
% 1.53/1.34
% 1.53/1.34 % (30348)Memory used [KB]: 5500
% 1.53/1.34 % (30348)Time elapsed: 0.003 s
% 1.53/1.34 % (30348)Instructions burned: 3 (million)
% 1.53/1.34 % (30348)------------------------------
% 1.53/1.34 % (30348)------------------------------
% 1.53/1.34 % (30341)First to succeed.
% 1.53/1.34 % (30351)Instruction limit reached!
% 1.53/1.34 % (30351)------------------------------
% 1.53/1.34 % (30351)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.53/1.34 % (30351)Termination reason: Unknown
% 1.53/1.34 % (30351)Termination phase: Saturation
% 1.53/1.34
% 1.53/1.34 % (30351)Memory used [KB]: 5500
% 1.53/1.34 % (30351)Time elapsed: 0.003 s
% 1.53/1.34 % (30350)Refutation not found, incomplete strategy
% 1.53/1.34 % (30350)------------------------------
% 1.53/1.34 % (30350)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.53/1.34 % (30350)Termination reason: Refutation not found, incomplete strategy
% 1.53/1.34
% 1.53/1.34
% 1.53/1.34 % (30350)Memory used [KB]: 5500
% 1.53/1.34 % (30350)Time elapsed: 0.003 s
% 1.53/1.34 % (30350)Instructions burned: 3 (million)
% 1.53/1.34 % (30350)------------------------------
% 1.53/1.34 % (30350)------------------------------
% 1.53/1.34 % (30351)Instructions burned: 3 (million)
% 1.53/1.34 % (30351)------------------------------
% 1.53/1.34 % (30351)------------------------------
% 1.53/1.34 % (30352)Refutation not found, incomplete strategy
% 1.53/1.34 % (30352)------------------------------
% 1.53/1.34 % (30352)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.53/1.34 % (30352)Termination reason: Refutation not found, incomplete strategy
% 1.53/1.34
% 1.53/1.34
% 1.53/1.34 % (30352)Memory used [KB]: 5500
% 1.53/1.34 % (30352)Time elapsed: 0.004 s
% 1.53/1.34 % (30352)Instructions burned: 3 (million)
% 1.53/1.34 % (30352)------------------------------
% 1.53/1.34 % (30352)------------------------------
% 1.53/1.34 % (30341)Refutation found. Thanks to Tanya!
% 1.53/1.34 % SZS status Theorem for DTF2THF_30244
% 1.53/1.34 % SZS output start Proof for DTF2THF_30244
% 1.53/1.34 thf(func_def_0, type, t: (($o > $o) > $o) > $o > $o).
% 1.53/1.34 thf(func_def_11, type, sK0: ($o > $o) > $o).
% 1.53/1.34 thf(func_def_12, type, sK1: $o > $o).
% 1.53/1.34 thf(func_def_14, type, ph3: !>[X0: $tType]:(X0)).
% 1.53/1.34 thf(f738,plain,(
% 1.53/1.34 $false),
% 1.53/1.34 inference(avatar_sat_refutation,[status(thm)],[f51,f64,f73,f86,f87,f88,f133,f142,f175,f195,f203,f210,f304,f319,f331,f341,f347,f381,f393,f401,f439,f480,f489,f536,f553,f604,f731])).
% 1.53/1.34 thf(f731,plain,(
% 1.53/1.34 spl2_2 | ~spl2_10),
% 1.53/1.34 inference(avatar_contradiction_clause,[status(thm)],[f730])).
% 1.53/1.34 thf(f730,plain,(
% 1.53/1.34 $false | (spl2_2 | ~spl2_10)),
% 1.53/1.34 inference(subsumption_resolution,[status(thm)],[f729,f49])).
% 1.53/1.34 thf(f49,plain,(
% 1.53/1.34 ((sK0 @ (^[Y0 : $o]: ($false))) != $false) | spl2_2),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f48])).
% 1.53/1.34 thf(f48,definition,(
% 1.53/1.34 spl2_2 <=> ((sK0 @ (^[Y0 : $o]: ($false))) = $false)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_2])],[avatar_definition])).
% 1.53/1.34 thf(f729,plain,(
% 1.53/1.34 ((sK0 @ (^[Y0 : $o]: ($false))) = $false) | ~spl2_10),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f721])).
% 1.53/1.34 thf(f721,plain,(
% 1.53/1.34 ($true = (~ (sK0 @ (^[Y0 : $o]: ($false))))) | ~spl2_10),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f720])).
% 1.53/1.34 thf(f720,plain,(
% 1.53/1.34 ($false != ((((sK0 @ ~) = (~ sK19)) | (sK0 @ (^[Y0 : $o]: ($true)))) & (~ (sK0 @ (^[Y0 : $o]: ($false)))))) | ~spl2_10),
% 1.53/1.34 inference(beta_eta_normalization,[status(thm)],[f719])).
% 1.53/1.34 thf(f719,plain,(
% 1.53/1.34 (((^[Y0 : $o]: ($false)) @ sK19) != ((^[Y0 : $o]: ((((sK0 @ ~) = (~ Y0)) | (sK0 @ (^[Y1 : $o]: ($true)))) & (~ (sK0 @ (^[Y1 : $o]: ($false)))))) @ sK19)) | ~spl2_10),
% 1.53/1.34 inference(negative_extensionality,[status(thm)],[f715])).
% 1.53/1.34 thf(f715,plain,(
% 1.53/1.34 ((^[Y0 : $o]: ($false)) != (^[Y0 : $o]: ((((sK0 @ ~) = (~ Y0)) | (sK0 @ (^[Y1 : $o]: ($true)))) & (~ (sK0 @ (^[Y1 : $o]: ($false))))))) | ~spl2_10),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f710])).
% 1.53/1.34 thf(f710,plain,(
% 1.53/1.34 ($true != $true) | ((^[Y0 : $o]: ($false)) != (^[Y0 : $o]: ((((sK0 @ ~) = (~ Y0)) | (sK0 @ (^[Y1 : $o]: ($true)))) & (~ (sK0 @ (^[Y1 : $o]: ($false))))))) | ~spl2_10),
% 1.53/1.34 inference(constrained_superposition,[status(thm)],[f17,f85])).
% 1.53/1.34 thf(f85,plain,(
% 1.53/1.34 ((sK0 @ (^[Y0 : $o]: ($false))) = $true) | ~spl2_10),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f83])).
% 1.53/1.34 thf(f83,definition,(
% 1.53/1.34 spl2_10 <=> ((sK0 @ (^[Y0 : $o]: ($false))) = $true)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_10])],[avatar_definition])).
% 1.53/1.34 thf(f17,plain,(
% 1.53/1.34 ($true != (sK0 @ (^[Y0 : $o]: ((((sK0 @ ~) = (~ Y0)) | (sK0 @ (^[Y1 : $o]: ($true)))) & (~ (sK0 @ (^[Y1 : $o]: ($false))))))))),
% 1.53/1.34 inference(beta_eta_normalization,[status(thm)],[f16])).
% 1.53/1.34 thf(f16,plain,(
% 1.53/1.34 ($true != (sK0 @ ((^[Y0 : ($o > $o) > $o]: ((^[Y1 : $o]: ((((Y0 @ (^[Y2 : $o]: (~ Y2))) = (~ Y1)) | (Y0 @ (^[Y2 : $o]: ($true)))) & (~ (Y0 @ (^[Y2 : $o]: ($false)))))))) @ sK0)))),
% 1.53/1.34 inference(definition_unfolding,[status(thm)],[f13,f15])).
% 1.53/1.34 thf(f15,plain,(
% 1.53/1.34 (t = (^[Y0 : ($o > $o) > $o]: ((^[Y1 : $o]: ((((Y0 @ (^[Y2 : $o]: (~ Y2))) = (~ Y1)) | (Y0 @ (^[Y2 : $o]: ($true)))) & (~ (Y0 @ (^[Y2 : $o]: ($false)))))))))),
% 1.53/1.34 inference(cnf_transformation,[status(thm)],[f8])).
% 1.53/1.34 thf(f8,plain,(
% 1.53/1.34 (t = (^[Y0 : ($o > $o) > $o]: ((^[Y1 : $o]: ((((Y0 @ (^[Y2 : $o]: (~ Y2))) = (~ Y1)) | (Y0 @ (^[Y2 : $o]: ($true)))) & (~ (Y0 @ (^[Y2 : $o]: ($false)))))))))),
% 1.53/1.34 inference(fool_elimination,[status(thm)],[f7])).
% 1.53/1.34 thf(f7,plain,(
% 1.53/1.34 (t = (^[X0 : ($o > $o) > $o, X1 : $o] : (~(X0 @ (^[X2 : $o] : ($false))) & ((X0 @ (^[X3 : $o] : ($true))) | ((X0 @ (^[X4 : $o] : (~X4))) = ~X1)))))),
% 1.53/1.34 inference(rectify,[status(thm)],[f1])).
% 1.53/1.34 thf(f1,axiom,(
% 1.53/1.34 (t = (^[X0 : ($o > $o) > $o, X1 : $o] : (~(X0 @ (^[X1 : $o] : ($false))) & ((X0 @ (^[X1 : $o] : ($true))) | ((X0 @ (^[X1 : $o] : (~X1))) = ~X1)))))),
% 1.53/1.34 file('/export/starexec/sandbox/tmp/tmp.EKm7Nwuf6V/DTF2THF_30244.p',t)).
% 1.53/1.34 thf(f13,plain,(
% 1.53/1.34 ($true != (sK0 @ (t @ sK0)))),
% 1.53/1.34 inference(cnf_transformation,[status(thm)],[f12])).
% 1.53/1.34 thf(f12,plain,(
% 1.53/1.34 ($true = (sK0 @ sK1)) & ($true != (sK0 @ (t @ sK0)))),
% 1.53/1.34 inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1])],[f9,f11,f10])).
% 1.53/1.34 thf(f10,plain,(
% 1.53/1.34 ? [X0 : ($o > $o) > $o] : (? [X1 : $o > $o] : ((X0 @ X1) = $true) & ((X0 @ (t @ X0)) != $true)) => (? [X1 : $o > $o] : ($true = (sK0 @ X1)) & ($true != (sK0 @ (t @ sK0))))),
% 1.53/1.34 introduced(definition,[],[choice_axiom])).
% 1.53/1.34 thf(f11,plain,(
% 1.53/1.34 ? [X1 : $o > $o] : ($true = (sK0 @ X1)) => ($true = (sK0 @ sK1))),
% 1.53/1.34 introduced(definition,[],[choice_axiom])).
% 1.53/1.34 thf(f9,plain,(
% 1.53/1.34 ? [X0 : ($o > $o) > $o] : (? [X1 : $o > $o] : ((X0 @ X1) = $true) & ((X0 @ (t @ X0)) != $true))),
% 1.53/1.34 inference(ennf_transformation,[status(thm)],[f6])).
% 1.53/1.34 thf(f6,plain,(
% 1.53/1.34 ~! [X0 : ($o > $o) > $o] : (? [X1 : $o > $o] : ((X0 @ X1) = $true) => ((X0 @ (t @ X0)) = $true))),
% 1.53/1.34 inference(fool_elimination,[status(thm)],[f5])).
% 1.53/1.34 thf(f5,plain,(
% 1.53/1.34 ~! [X0 : ($o > $o) > $o] : (? [X1 : $o > $o] : (X0 @ X1) => (X0 @ (t @ X0)))),
% 1.53/1.34 inference(rectify,[status(thm)],[f3])).
% 1.53/1.34 thf(f3,negated_conjecture,(
% 1.53/1.34 ~! [X0 : ($o > $o) > $o] : (? [X2 : $o > $o] : (X0 @ X2) => (X0 @ (t @ X0)))),
% 1.53/1.34 inference(negated_conjecture,[status(cth)],[f2])).
% 1.53/1.34 thf(f2,conjecture,(
% 1.53/1.34 ! [X0 : ($o > $o) > $o] : (? [X2 : $o > $o] : (X0 @ X2) => (X0 @ (t @ X0)))),
% 1.53/1.34 file('/export/starexec/sandbox/tmp/tmp.EKm7Nwuf6V/DTF2THF_30244.p',choiceoo1)).
% 1.53/1.34 thf(f604,plain,(
% 1.53/1.34 ~spl2_1 | ~spl2_4 | ~spl2_9 | spl2_21 | ~spl2_22),
% 1.53/1.34 inference(avatar_contradiction_clause,[status(thm)],[f603])).
% 1.53/1.34 thf(f603,plain,(
% 1.53/1.34 $false | (~spl2_1 | ~spl2_4 | ~spl2_9 | spl2_21 | ~spl2_22)),
% 1.53/1.34 inference(subsumption_resolution,[status(thm)],[f597,f602])).
% 1.53/1.34 thf(f602,plain,(
% 1.53/1.34 (sK16 = $false) | (~spl2_9 | spl2_21 | ~spl2_22)),
% 1.53/1.34 inference(subsumption_resolution,[status(thm)],[f600,f474])).
% 1.53/1.34 thf(f474,plain,(
% 1.53/1.34 ($false != sK15) | spl2_21),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f473])).
% 1.53/1.34 thf(f473,definition,(
% 1.53/1.34 spl2_21 <=> ($false = sK15)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_21])],[avatar_definition])).
% 1.53/1.34 thf(f600,plain,(
% 1.53/1.34 ($false = sK15) | (sK16 = $false) | (~spl2_9 | ~spl2_22)),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f598])).
% 1.53/1.34 thf(f598,plain,(
% 1.53/1.34 (sK16 != sK15) | (~spl2_9 | ~spl2_22)),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f586])).
% 1.53/1.34 thf(f586,plain,(
% 1.53/1.34 ($true != $true) | (sK16 != sK15) | (~spl2_9 | ~spl2_22)),
% 1.53/1.34 inference(constrained_superposition,[status(thm)],[f580,f479])).
% 1.53/1.34 thf(f479,plain,(
% 1.53/1.34 ($true = (sK1 @ sK15)) | ~spl2_22),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f477])).
% 1.53/1.34 thf(f477,definition,(
% 1.53/1.34 spl2_22 <=> ($true = (sK1 @ sK15))),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_22])],[avatar_definition])).
% 1.53/1.34 thf(f580,plain,(
% 1.53/1.34 ($true != (sK1 @ sK16)) | ~spl2_9),
% 1.53/1.34 inference(beta_eta_normalization,[status(thm)],[f579])).
% 1.53/1.34 thf(f579,plain,(
% 1.53/1.34 (((^[Y0 : $o]: ($true)) @ sK16) != (sK1 @ sK16)) | ~spl2_9),
% 1.53/1.34 inference(negative_extensionality,[status(thm)],[f374])).
% 1.53/1.34 thf(f374,plain,(
% 1.53/1.34 (sK1 != (^[Y0 : $o]: ($true))) | ~spl2_9),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f370])).
% 1.53/1.34 thf(f370,plain,(
% 1.53/1.34 (sK1 != (^[Y0 : $o]: ($true))) | ($true = $false) | ~spl2_9),
% 1.53/1.34 inference(constrained_superposition,[status(thm)],[f14,f81])).
% 1.53/1.34 thf(f81,plain,(
% 1.53/1.34 ((sK0 @ (^[Y0 : $o]: ($true))) = $false) | ~spl2_9),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f79])).
% 1.53/1.34 thf(f79,definition,(
% 1.53/1.34 spl2_9 <=> ((sK0 @ (^[Y0 : $o]: ($true))) = $false)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_9])],[avatar_definition])).
% 1.53/1.34 thf(f14,plain,(
% 1.53/1.34 ($true = (sK0 @ sK1))),
% 1.53/1.34 inference(cnf_transformation,[status(thm)],[f12])).
% 1.53/1.34 thf(f597,plain,(
% 1.53/1.34 (sK16 != $false) | (~spl2_1 | ~spl2_4 | ~spl2_9)),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f588])).
% 1.53/1.34 thf(f588,plain,(
% 1.53/1.34 ($true != $true) | (sK16 != $false) | (~spl2_1 | ~spl2_4 | ~spl2_9)),
% 1.53/1.34 inference(constrained_superposition,[status(thm)],[f580,f445])).
% 1.53/1.34 thf(f445,plain,(
% 1.53/1.34 ($true = (sK1 @ $false)) | (~spl2_1 | ~spl2_4)),
% 1.53/1.34 inference(superposition,[status(thm)],[f46,f59])).
% 1.53/1.34 thf(f59,plain,(
% 1.53/1.34 ($false = sK4) | ~spl2_4),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f57])).
% 1.53/1.34 thf(f57,definition,(
% 1.53/1.34 spl2_4 <=> ($false = sK4)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_4])],[avatar_definition])).
% 1.53/1.34 thf(f46,plain,(
% 1.53/1.34 ((sK1 @ sK4) = $true) | ~spl2_1),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f44])).
% 1.53/1.34 thf(f44,definition,(
% 1.53/1.34 spl2_1 <=> ((sK1 @ sK4) = $true)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_1])],[avatar_definition])).
% 1.53/1.34 thf(f553,plain,(
% 1.53/1.34 ~spl2_21 | ~spl2_24),
% 1.53/1.34 inference(avatar_contradiction_clause,[status(thm)],[f552])).
% 1.53/1.34 thf(f552,plain,(
% 1.53/1.34 $false | (~spl2_21 | ~spl2_24)),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f549])).
% 1.53/1.34 thf(f549,plain,(
% 1.53/1.34 ($true = $false) | (~spl2_21 | ~spl2_24)),
% 1.53/1.34 inference(superposition,[status(thm)],[f475,f488])).
% 1.53/1.34 thf(f488,plain,(
% 1.53/1.34 ($true = sK15) | ~spl2_24),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f486])).
% 1.53/1.34 thf(f486,definition,(
% 1.53/1.34 spl2_24 <=> ($true = sK15)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_24])],[avatar_definition])).
% 1.53/1.34 thf(f475,plain,(
% 1.53/1.34 ($false = sK15) | ~spl2_21),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f473])).
% 1.53/1.34 thf(f536,plain,(
% 1.53/1.34 ~spl2_1 | ~spl2_4 | ~spl2_21 | ~spl2_23),
% 1.53/1.34 inference(avatar_contradiction_clause,[status(thm)],[f535])).
% 1.53/1.34 thf(f535,plain,(
% 1.53/1.34 $false | (~spl2_1 | ~spl2_4 | ~spl2_21 | ~spl2_23)),
% 1.53/1.34 inference(subsumption_resolution,[status(thm)],[f521,f475])).
% 1.53/1.34 thf(f521,plain,(
% 1.53/1.34 ($false != sK15) | (~spl2_1 | ~spl2_4 | ~spl2_23)),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f506])).
% 1.53/1.34 thf(f506,plain,(
% 1.53/1.34 ($true = $false) | ($false != sK15) | (~spl2_1 | ~spl2_4 | ~spl2_23)),
% 1.53/1.34 inference(constrained_superposition,[status(thm)],[f445,f484])).
% 1.53/1.34 thf(f484,plain,(
% 1.53/1.34 ((sK1 @ sK15) = $false) | ~spl2_23),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f482])).
% 1.53/1.34 thf(f482,definition,(
% 1.53/1.34 spl2_23 <=> ((sK1 @ sK15) = $false)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_23])],[avatar_definition])).
% 1.53/1.34 thf(f489,plain,(
% 1.53/1.34 spl2_23 | spl2_24 | ~spl2_5),
% 1.53/1.34 inference(avatar_split_clause,[status(thm)],[f470,f61,f486,f482])).
% 1.53/1.34 thf(f61,definition,(
% 1.53/1.34 spl2_5 <=> ($false = (sK0 @ ~))),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_5])],[avatar_definition])).
% 1.53/1.34 thf(f470,plain,(
% 1.53/1.34 ($true = sK15) | ((sK1 @ sK15) = $false) | ~spl2_5),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f469])).
% 1.53/1.34 thf(f469,plain,(
% 1.53/1.34 ((~ sK15) = $false) | ((sK1 @ sK15) = $false) | ~spl2_5),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f467])).
% 1.53/1.34 thf(f467,plain,(
% 1.53/1.34 ((sK1 @ sK15) != (~ sK15)) | ~spl2_5),
% 1.53/1.34 inference(negative_extensionality,[status(thm)],[f466])).
% 1.53/1.34 thf(f466,plain,(
% 1.53/1.34 (sK1 != ~) | ~spl2_5),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f461])).
% 1.53/1.34 thf(f461,plain,(
% 1.53/1.34 (sK1 != ~) | ($true = $false) | ~spl2_5),
% 1.53/1.34 inference(constrained_superposition,[status(thm)],[f63,f14])).
% 1.53/1.34 thf(f63,plain,(
% 1.53/1.34 ($false = (sK0 @ ~)) | ~spl2_5),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f61])).
% 1.53/1.34 thf(f480,plain,(
% 1.53/1.34 spl2_21 | spl2_22 | ~spl2_5),
% 1.53/1.34 inference(avatar_split_clause,[status(thm)],[f471,f61,f477,f473])).
% 1.53/1.34 thf(f471,plain,(
% 1.53/1.34 ($false = sK15) | ($true = (sK1 @ sK15)) | ~spl2_5),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f468])).
% 1.53/1.34 thf(f468,plain,(
% 1.53/1.34 ($true = (~ sK15)) | ($true = (sK1 @ sK15)) | ~spl2_5),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f467])).
% 1.53/1.34 thf(f439,plain,(
% 1.53/1.34 spl2_1 | ~spl2_7 | ~spl2_13 | ~spl2_15),
% 1.53/1.34 inference(avatar_contradiction_clause,[status(thm)],[f438])).
% 1.53/1.34 thf(f438,plain,(
% 1.53/1.34 $false | (spl2_1 | ~spl2_7 | ~spl2_13 | ~spl2_15)),
% 1.53/1.34 inference(subsumption_resolution,[status(thm)],[f403,f359])).
% 1.53/1.34 thf(f359,plain,(
% 1.53/1.34 ((sK1 @ $true) != $true) | (spl2_1 | ~spl2_7)),
% 1.53/1.34 inference(superposition,[status(thm)],[f45,f72])).
% 1.53/1.34 thf(f72,plain,(
% 1.53/1.34 ($true = sK4) | ~spl2_7),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f70])).
% 1.53/1.34 thf(f70,definition,(
% 1.53/1.34 spl2_7 <=> ($true = sK4)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_7])],[avatar_definition])).
% 1.53/1.34 thf(f45,plain,(
% 1.53/1.34 ((sK1 @ sK4) != $true) | spl2_1),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f44])).
% 1.53/1.34 thf(f403,plain,(
% 1.53/1.34 ((sK1 @ $true) = $true) | (~spl2_13 | ~spl2_15)),
% 1.53/1.34 inference(superposition,[status(thm)],[f128,f137])).
% 1.53/1.34 thf(f137,plain,(
% 1.53/1.34 ($true = sK6) | ~spl2_15),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f135])).
% 1.53/1.34 thf(f135,definition,(
% 1.53/1.34 spl2_15 <=> ($true = sK6)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_15])],[avatar_definition])).
% 1.53/1.34 thf(f128,plain,(
% 1.53/1.34 ($true = (sK1 @ sK6)) | ~spl2_13),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f126])).
% 1.53/1.34 thf(f126,definition,(
% 1.53/1.34 spl2_13 <=> ($true = (sK1 @ sK6))),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_13])],[avatar_definition])).
% 1.53/1.34 thf(f401,plain,(
% 1.53/1.34 ~spl2_14 | ~spl2_15),
% 1.53/1.34 inference(avatar_contradiction_clause,[status(thm)],[f400])).
% 1.53/1.34 thf(f400,plain,(
% 1.53/1.34 $false | (~spl2_14 | ~spl2_15)),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f397])).
% 1.53/1.34 thf(f397,plain,(
% 1.53/1.34 ($true = $false) | (~spl2_14 | ~spl2_15)),
% 1.53/1.34 inference(superposition,[status(thm)],[f132,f137])).
% 1.53/1.34 thf(f132,plain,(
% 1.53/1.34 (sK6 = $false) | ~spl2_14),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f130])).
% 1.53/1.34 thf(f130,definition,(
% 1.53/1.34 spl2_14 <=> (sK6 = $false)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_14])],[avatar_definition])).
% 1.53/1.34 thf(f393,plain,(
% 1.53/1.34 spl2_15 | ~spl2_2 | ~spl2_16 | spl2_20),
% 1.53/1.34 inference(avatar_split_clause,[status(thm)],[f392,f354,f139,f48,f135])).
% 1.53/1.34 thf(f139,definition,(
% 1.53/1.34 spl2_16 <=> ((sK1 @ sK6) = $false)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_16])],[avatar_definition])).
% 1.53/1.34 thf(f354,definition,(
% 1.53/1.34 spl2_20 <=> ($true = sK10)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_20])],[avatar_definition])).
% 1.53/1.34 thf(f392,plain,(
% 1.53/1.34 ($true = sK6) | (~spl2_2 | ~spl2_16 | spl2_20)),
% 1.53/1.34 inference(subsumption_resolution,[status(thm)],[f388,f355])).
% 1.53/1.34 thf(f355,plain,(
% 1.53/1.34 ($true != sK10) | spl2_20),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f354])).
% 1.53/1.34 thf(f388,plain,(
% 1.53/1.34 ($true = sK6) | ($true = sK10) | (~spl2_2 | ~spl2_16)),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f387])).
% 1.53/1.34 thf(f387,plain,(
% 1.53/1.34 (sK6 != sK10) | (~spl2_2 | ~spl2_16)),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f385])).
% 1.53/1.34 thf(f385,plain,(
% 1.53/1.34 ($false != $false) | (sK6 != sK10) | (~spl2_2 | ~spl2_16)),
% 1.53/1.34 inference(constrained_superposition,[status(thm)],[f235,f141])).
% 1.53/1.34 thf(f141,plain,(
% 1.53/1.34 ((sK1 @ sK6) = $false) | ~spl2_16),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f139])).
% 1.53/1.34 thf(f235,plain,(
% 1.53/1.34 ((sK1 @ sK10) != $false) | ~spl2_2),
% 1.53/1.34 inference(beta_eta_normalization,[status(thm)],[f234])).
% 1.53/1.34 thf(f234,plain,(
% 1.53/1.34 (((^[Y0 : $o]: ($false)) @ sK10) != (sK1 @ sK10)) | ~spl2_2),
% 1.53/1.34 inference(negative_extensionality,[status(thm)],[f228])).
% 1.53/1.34 thf(f228,plain,(
% 1.53/1.34 (sK1 != (^[Y0 : $o]: ($false))) | ~spl2_2),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f219])).
% 1.53/1.34 thf(f219,plain,(
% 1.53/1.34 (sK1 != (^[Y0 : $o]: ($false))) | ($true = $false) | ~spl2_2),
% 1.53/1.34 inference(constrained_superposition,[status(thm)],[f50,f14])).
% 1.53/1.34 thf(f50,plain,(
% 1.53/1.34 ((sK0 @ (^[Y0 : $o]: ($false))) = $false) | ~spl2_2),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f48])).
% 1.53/1.34 thf(f381,plain,(
% 1.53/1.34 ~spl2_20 | ~spl2_2 | ~spl2_7 | ~spl2_8),
% 1.53/1.34 inference(avatar_split_clause,[status(thm)],[f380,f75,f70,f48,f354])).
% 1.53/1.34 thf(f75,definition,(
% 1.53/1.34 spl2_8 <=> ((sK1 @ sK4) = $false)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_8])],[avatar_definition])).
% 1.53/1.34 thf(f380,plain,(
% 1.53/1.34 ($true != sK10) | (~spl2_2 | ~spl2_7 | ~spl2_8)),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f378])).
% 1.53/1.34 thf(f378,plain,(
% 1.53/1.34 ($false != $false) | ($true != sK10) | (~spl2_2 | ~spl2_7 | ~spl2_8)),
% 1.53/1.34 inference(constrained_superposition,[status(thm)],[f235,f360])).
% 1.53/1.34 thf(f360,plain,(
% 1.53/1.34 ((sK1 @ $true) = $false) | (~spl2_7 | ~spl2_8)),
% 1.53/1.34 inference(superposition,[status(thm)],[f77,f72])).
% 1.53/1.34 thf(f77,plain,(
% 1.53/1.34 ((sK1 @ sK4) = $false) | ~spl2_8),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f75])).
% 1.53/1.34 thf(f347,plain,(
% 1.53/1.34 ~spl2_17 | ~spl2_18),
% 1.53/1.34 inference(avatar_contradiction_clause,[status(thm)],[f346])).
% 1.53/1.34 thf(f346,plain,(
% 1.53/1.34 $false | (~spl2_17 | ~spl2_18)),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f343])).
% 1.53/1.34 thf(f343,plain,(
% 1.53/1.34 ($true = $false) | (~spl2_17 | ~spl2_18)),
% 1.53/1.34 inference(superposition,[status(thm)],[f337,f318])).
% 1.53/1.34 thf(f318,plain,(
% 1.53/1.34 (sK13 = $false) | ~spl2_17),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f316])).
% 1.53/1.34 thf(f316,definition,(
% 1.53/1.34 spl2_17 <=> (sK13 = $false)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_17])],[avatar_definition])).
% 1.53/1.34 thf(f337,plain,(
% 1.53/1.34 (sK13 = $true) | ~spl2_18),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f335])).
% 1.53/1.34 thf(f335,definition,(
% 1.53/1.34 spl2_18 <=> (sK13 = $true)),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_18])],[avatar_definition])).
% 1.53/1.34 thf(f341,plain,(
% 1.53/1.34 spl2_18 | spl2_5 | ~spl2_6 | spl2_10),
% 1.53/1.34 inference(avatar_split_clause,[status(thm)],[f340,f83,f66,f61,f335])).
% 1.53/1.34 thf(f66,definition,(
% 1.53/1.34 spl2_6 <=> ($true = (sK0 @ ~))),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_6])],[avatar_definition])).
% 1.53/1.34 thf(f340,plain,(
% 1.53/1.34 (sK13 = $true) | (spl2_5 | ~spl2_6 | spl2_10)),
% 1.53/1.34 inference(subsumption_resolution,[status(thm)],[f339,f62])).
% 1.53/1.34 thf(f62,plain,(
% 1.53/1.34 ($false != (sK0 @ ~)) | spl2_5),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f61])).
% 1.53/1.34 thf(f339,plain,(
% 1.53/1.34 (sK13 = $true) | ($false = (sK0 @ ~)) | (~spl2_6 | spl2_10)),
% 1.53/1.34 inference(subsumption_resolution,[status(thm)],[f274,f84])).
% 1.53/1.34 thf(f84,plain,(
% 1.53/1.34 ((sK0 @ (^[Y0 : $o]: ($false))) != $true) | spl2_10),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f83])).
% 1.53/1.34 thf(f274,plain,(
% 1.53/1.34 ((sK0 @ (^[Y0 : $o]: ($false))) = $true) | (sK13 = $true) | ($false = (sK0 @ ~)) | ~spl2_6),
% 1.53/1.34 inference(duplicate_literal_removal,[status(thm)],[f273])).
% 1.53/1.34 thf(f273,plain,(
% 1.53/1.34 ($false = (sK0 @ ~)) | ((sK0 @ (^[Y0 : $o]: ($false))) = $true) | (sK13 = $true) | (sK13 = $true) | ~spl2_6),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f272])).
% 1.53/1.34 thf(f272,plain,(
% 1.53/1.34 ((sK0 @ (^[Y0 : $o]: ($false))) = $true) | ((~ sK13) = $false) | (sK13 = $true) | ($false = (sK0 @ ~)) | ~spl2_6),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f270])).
% 1.53/1.34 thf(f270,plain,(
% 1.53/1.34 ((~ sK13) != (sK0 @ ~)) | (sK13 = $true) | ((sK0 @ (^[Y0 : $o]: ($false))) = $true) | ~spl2_6),
% 1.53/1.34 inference(equality_proxy_clausification,[status(thm)],[f269])).
% 1.53/1.34 thf(f269,plain,(
% 1.53/1.34 (sK13 = $true) | ((sK0 @ (^[Y0 : $o]: ($false))) = $true) | (((sK0 @ ~) = (~ sK13)) = $false) | ~spl2_6),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f268])).
% 1.53/1.34 thf(f268,plain,(
% 1.53/1.34 (sK13 = $true) | ($false = (~ (sK0 @ (^[Y0 : $o]: ($false))))) | (((sK0 @ ~) = (~ sK13)) = $false) | ~spl2_6),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f266])).
% 1.53/1.34 thf(f266,plain,(
% 1.53/1.34 (sK13 = $true) | ((((sK0 @ ~) = (~ sK13)) | (sK0 @ (^[Y0 : $o]: ($true)))) = $false) | ($false = (~ (sK0 @ (^[Y0 : $o]: ($false))))) | ~spl2_6),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f265])).
% 1.53/1.34 thf(f265,plain,(
% 1.53/1.34 (((((sK0 @ ~) = (~ sK13)) | (sK0 @ (^[Y0 : $o]: ($true)))) & (~ (sK0 @ (^[Y0 : $o]: ($false))))) = $false) | (sK13 = $true) | ~spl2_6),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f264])).
% 1.53/1.34 thf(f264,plain,(
% 1.53/1.34 ((~ sK13) = $false) | (((((sK0 @ ~) = (~ sK13)) | (sK0 @ (^[Y0 : $o]: ($true)))) & (~ (sK0 @ (^[Y0 : $o]: ($false))))) = $false) | ~spl2_6),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f262])).
% 1.53/1.34 thf(f262,plain,(
% 1.53/1.34 (((((sK0 @ ~) = (~ sK13)) | (sK0 @ (^[Y0 : $o]: ($true)))) & (~ (sK0 @ (^[Y0 : $o]: ($false))))) != (~ sK13)) | ~spl2_6),
% 1.53/1.34 inference(beta_eta_normalization,[status(thm)],[f261])).
% 1.53/1.34 thf(f261,plain,(
% 1.53/1.34 (((^[Y0 : $o]: ((((sK0 @ ~) = (~ Y0)) | (sK0 @ (^[Y1 : $o]: ($true)))) & (~ (sK0 @ (^[Y1 : $o]: ($false)))))) @ sK13) != (~ sK13)) | ~spl2_6),
% 1.53/1.34 inference(negative_extensionality,[status(thm)],[f158])).
% 1.53/1.34 thf(f158,plain,(
% 1.53/1.34 (~ != (^[Y0 : $o]: ((((sK0 @ ~) = (~ Y0)) | (sK0 @ (^[Y1 : $o]: ($true)))) & (~ (sK0 @ (^[Y1 : $o]: ($false))))))) | ~spl2_6),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f154])).
% 1.53/1.34 thf(f154,plain,(
% 1.53/1.34 ($true != $true) | (~ != (^[Y0 : $o]: ((((sK0 @ ~) = (~ Y0)) | (sK0 @ (^[Y1 : $o]: ($true)))) & (~ (sK0 @ (^[Y1 : $o]: ($false))))))) | ~spl2_6),
% 1.53/1.34 inference(constrained_superposition,[status(thm)],[f17,f68])).
% 1.53/1.34 thf(f68,plain,(
% 1.53/1.34 ($true = (sK0 @ ~)) | ~spl2_6),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f66])).
% 1.53/1.34 thf(f331,plain,(
% 1.53/1.34 ~spl2_5 | ~spl2_6),
% 1.53/1.34 inference(avatar_contradiction_clause,[status(thm)],[f330])).
% 1.53/1.34 thf(f330,plain,(
% 1.53/1.34 $false | (~spl2_5 | ~spl2_6)),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f320])).
% 1.53/1.34 thf(f320,plain,(
% 1.53/1.34 ($true = $false) | (~spl2_5 | ~spl2_6)),
% 1.53/1.34 inference(superposition,[status(thm)],[f63,f68])).
% 1.53/1.34 thf(f319,plain,(
% 1.53/1.34 spl2_17 | spl2_5 | spl2_3 | ~spl2_6),
% 1.53/1.34 inference(avatar_split_clause,[status(thm)],[f307,f66,f53,f61,f316])).
% 1.53/1.34 thf(f53,definition,(
% 1.53/1.34 spl2_3 <=> ($true = (sK0 @ (^[Y0 : $o]: ($true))))),
% 1.53/1.34 introduced(definition,[new_symbols(naming,[spl2_3])],[avatar_definition])).
% 1.53/1.34 thf(f307,plain,(
% 1.53/1.34 ($false = (sK0 @ ~)) | (sK13 = $false) | (spl2_3 | ~spl2_6)),
% 1.53/1.34 inference(subsumption_resolution,[status(thm)],[f286,f54])).
% 1.53/1.34 thf(f54,plain,(
% 1.53/1.34 ($true != (sK0 @ (^[Y0 : $o]: ($true)))) | spl2_3),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f53])).
% 1.53/1.34 thf(f286,plain,(
% 1.53/1.34 ($true = (sK0 @ (^[Y0 : $o]: ($true)))) | (sK13 = $false) | ($false = (sK0 @ ~)) | ~spl2_6),
% 1.53/1.34 inference(duplicate_literal_removal,[status(thm)],[f285])).
% 1.53/1.34 thf(f285,plain,(
% 1.53/1.34 ($false = (sK0 @ ~)) | (sK13 = $false) | ($true = (sK0 @ (^[Y0 : $o]: ($true)))) | (sK13 = $false) | ~spl2_6),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f282])).
% 1.53/1.34 thf(f282,plain,(
% 1.53/1.34 ($false = (sK0 @ ~)) | ($true = (~ sK13)) | (sK13 = $false) | ($true = (sK0 @ (^[Y0 : $o]: ($true)))) | ~spl2_6),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f281])).
% 1.53/1.34 thf(f281,plain,(
% 1.53/1.34 ((~ sK13) = (sK0 @ ~)) | (sK13 = $false) | ($true = (sK0 @ (^[Y0 : $o]: ($true)))) | ~spl2_6),
% 1.53/1.34 inference(equality_proxy_clausification,[status(thm)],[f280])).
% 1.53/1.34 thf(f280,plain,(
% 1.53/1.34 ($true = (sK0 @ (^[Y0 : $o]: ($true)))) | ($true = ((sK0 @ ~) = (~ sK13))) | (sK13 = $false) | ~spl2_6),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f279])).
% 1.53/1.34 thf(f279,plain,(
% 1.53/1.34 (sK13 = $false) | ($true = (((sK0 @ ~) = (~ sK13)) | (sK0 @ (^[Y0 : $o]: ($true))))) | ~spl2_6),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f278])).
% 1.53/1.34 thf(f278,plain,(
% 1.53/1.34 ($true = (~ sK13)) | ($true = (((sK0 @ ~) = (~ sK13)) | (sK0 @ (^[Y0 : $o]: ($true))))) | ~spl2_6),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f263])).
% 1.53/1.34 thf(f263,plain,(
% 1.53/1.34 ($true = ((((sK0 @ ~) = (~ sK13)) | (sK0 @ (^[Y0 : $o]: ($true)))) & (~ (sK0 @ (^[Y0 : $o]: ($false)))))) | ($true = (~ sK13)) | ~spl2_6),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f262])).
% 1.53/1.34 thf(f304,plain,(
% 1.53/1.34 ~spl2_3 | spl2_9 | spl2_10),
% 1.53/1.34 inference(avatar_contradiction_clause,[status(thm)],[f303])).
% 1.53/1.34 thf(f303,plain,(
% 1.53/1.34 $false | (~spl2_3 | spl2_9 | spl2_10)),
% 1.53/1.34 inference(subsumption_resolution,[status(thm)],[f302,f84])).
% 1.53/1.34 thf(f302,plain,(
% 1.53/1.34 ((sK0 @ (^[Y0 : $o]: ($false))) = $true) | (~spl2_3 | spl2_9)),
% 1.53/1.34 inference(subsumption_resolution,[status(thm)],[f295,f80])).
% 1.53/1.34 thf(f80,plain,(
% 1.53/1.34 ((sK0 @ (^[Y0 : $o]: ($true))) != $false) | spl2_9),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f79])).
% 1.53/1.34 thf(f295,plain,(
% 1.53/1.34 ((sK0 @ (^[Y0 : $o]: ($true))) = $false) | ((sK0 @ (^[Y0 : $o]: ($false))) = $true) | ~spl2_3),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f294])).
% 1.53/1.34 thf(f294,plain,(
% 1.53/1.34 ((((sK0 @ ~) = (~ sK14)) | (sK0 @ (^[Y0 : $o]: ($true)))) = $false) | ((sK0 @ (^[Y0 : $o]: ($false))) = $true) | ~spl2_3),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f293])).
% 1.53/1.34 thf(f293,plain,(
% 1.53/1.34 ($false = (~ (sK0 @ (^[Y0 : $o]: ($false))))) | ((((sK0 @ ~) = (~ sK14)) | (sK0 @ (^[Y0 : $o]: ($true)))) = $false) | ~spl2_3),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f292])).
% 1.53/1.34 thf(f292,plain,(
% 1.53/1.34 ($true != ((((sK0 @ ~) = (~ sK14)) | (sK0 @ (^[Y0 : $o]: ($true)))) & (~ (sK0 @ (^[Y0 : $o]: ($false)))))) | ~spl2_3),
% 1.53/1.34 inference(beta_eta_normalization,[status(thm)],[f291])).
% 1.53/1.34 thf(f291,plain,(
% 1.53/1.34 (((^[Y0 : $o]: ((((sK0 @ ~) = (~ Y0)) | (sK0 @ (^[Y1 : $o]: ($true)))) & (~ (sK0 @ (^[Y1 : $o]: ($false)))))) @ sK14) != ((^[Y0 : $o]: ($true)) @ sK14)) | ~spl2_3),
% 1.53/1.34 inference(negative_extensionality,[status(thm)],[f171])).
% 1.53/1.34 thf(f171,plain,(
% 1.53/1.34 ((^[Y0 : $o]: ($true)) != (^[Y0 : $o]: ((((sK0 @ ~) = (~ Y0)) | (sK0 @ (^[Y1 : $o]: ($true)))) & (~ (sK0 @ (^[Y1 : $o]: ($false))))))) | ~spl2_3),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f167])).
% 1.53/1.34 thf(f167,plain,(
% 1.53/1.34 ($true != $true) | ((^[Y0 : $o]: ($true)) != (^[Y0 : $o]: ((((sK0 @ ~) = (~ Y0)) | (sK0 @ (^[Y1 : $o]: ($true)))) & (~ (sK0 @ (^[Y1 : $o]: ($false))))))) | ~spl2_3),
% 1.53/1.34 inference(constrained_superposition,[status(thm)],[f17,f55])).
% 1.53/1.34 thf(f55,plain,(
% 1.53/1.34 ($true = (sK0 @ (^[Y0 : $o]: ($true)))) | ~spl2_3),
% 1.53/1.34 inference(avatar_component_clause,[status(thm)],[f53])).
% 1.53/1.34 thf(f210,plain,(
% 1.53/1.34 ~spl2_4 | ~spl2_7),
% 1.53/1.34 inference(avatar_contradiction_clause,[status(thm)],[f209])).
% 1.53/1.34 thf(f209,plain,(
% 1.53/1.34 $false | (~spl2_4 | ~spl2_7)),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f206])).
% 1.53/1.34 thf(f206,plain,(
% 1.53/1.34 ($true = $false) | (~spl2_4 | ~spl2_7)),
% 1.53/1.34 inference(superposition,[status(thm)],[f72,f59])).
% 1.53/1.34 thf(f203,plain,(
% 1.53/1.34 ~spl2_1 | ~spl2_8),
% 1.53/1.34 inference(avatar_contradiction_clause,[status(thm)],[f202])).
% 1.53/1.34 thf(f202,plain,(
% 1.53/1.34 $false | (~spl2_1 | ~spl2_8)),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f199])).
% 1.53/1.34 thf(f199,plain,(
% 1.53/1.34 ($true = $false) | (~spl2_1 | ~spl2_8)),
% 1.53/1.34 inference(superposition,[status(thm)],[f46,f77])).
% 1.53/1.34 thf(f195,plain,(
% 1.53/1.34 ~spl2_2 | ~spl2_10),
% 1.53/1.34 inference(avatar_contradiction_clause,[status(thm)],[f194])).
% 1.53/1.34 thf(f194,plain,(
% 1.53/1.34 $false | (~spl2_2 | ~spl2_10)),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f186])).
% 1.53/1.34 thf(f186,plain,(
% 1.53/1.34 ($true = $false) | (~spl2_2 | ~spl2_10)),
% 1.53/1.34 inference(superposition,[status(thm)],[f85,f50])).
% 1.53/1.34 thf(f175,plain,(
% 1.53/1.34 ~spl2_3 | ~spl2_9),
% 1.53/1.34 inference(avatar_contradiction_clause,[status(thm)],[f174])).
% 1.53/1.34 thf(f174,plain,(
% 1.53/1.34 $false | (~spl2_3 | ~spl2_9)),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f170])).
% 1.53/1.34 thf(f170,plain,(
% 1.53/1.34 ($true = $false) | (~spl2_3 | ~spl2_9)),
% 1.53/1.34 inference(superposition,[status(thm)],[f81,f55])).
% 1.53/1.34 thf(f142,plain,(
% 1.53/1.34 spl2_15 | spl2_16 | ~spl2_5),
% 1.53/1.34 inference(avatar_split_clause,[status(thm)],[f123,f61,f139,f135])).
% 1.53/1.34 thf(f123,plain,(
% 1.53/1.34 ((sK1 @ sK6) = $false) | ($true = sK6) | ~spl2_5),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f122])).
% 1.53/1.34 thf(f122,plain,(
% 1.53/1.34 ((~ sK6) = $false) | ((sK1 @ sK6) = $false) | ~spl2_5),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f120])).
% 1.53/1.34 thf(f120,plain,(
% 1.53/1.34 ((~ sK6) != (sK1 @ sK6)) | ~spl2_5),
% 1.53/1.34 inference(negative_extensionality,[status(thm)],[f114])).
% 1.53/1.34 thf(f114,plain,(
% 1.53/1.34 (sK1 != ~) | ~spl2_5),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f110])).
% 1.53/1.34 thf(f110,plain,(
% 1.53/1.34 (sK1 != ~) | ($true = $false) | ~spl2_5),
% 1.53/1.34 inference(constrained_superposition,[status(thm)],[f63,f14])).
% 1.53/1.34 thf(f133,plain,(
% 1.53/1.34 spl2_13 | spl2_14 | ~spl2_5),
% 1.53/1.34 inference(avatar_split_clause,[status(thm)],[f124,f61,f130,f126])).
% 1.53/1.34 thf(f124,plain,(
% 1.53/1.34 ($true = (sK1 @ sK6)) | (sK6 = $false) | ~spl2_5),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f121])).
% 1.53/1.34 thf(f121,plain,(
% 1.53/1.34 ((~ sK6) = $true) | ($true = (sK1 @ sK6)) | ~spl2_5),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f120])).
% 1.53/1.34 thf(f88,plain,(
% 1.53/1.34 spl2_7 | spl2_8 | spl2_5 | spl2_10),
% 1.53/1.34 inference(avatar_split_clause,[status(thm)],[f31,f83,f61,f75,f70])).
% 1.53/1.34 thf(f31,plain,(
% 1.53/1.34 ((sK1 @ sK4) = $false) | ((sK0 @ (^[Y0 : $o]: ($false))) = $true) | ($true = sK4) | ($false = (sK0 @ ~))),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f30])).
% 1.53/1.34 thf(f30,plain,(
% 1.53/1.34 ($false = (sK0 @ ~)) | ((sK1 @ sK4) = $false) | ((sK0 @ (^[Y0 : $o]: ($false))) = $true) | ((~ sK4) = $false)),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f28])).
% 1.53/1.34 thf(f28,plain,(
% 1.53/1.34 ((sK0 @ (^[Y0 : $o]: ($false))) = $true) | ((sK1 @ sK4) = $false) | ((~ sK4) != (sK0 @ ~))),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f27])).
% 1.53/1.34 thf(f27,plain,(
% 1.53/1.34 ($false = (~ (sK0 @ (^[Y0 : $o]: ($false))))) | ((~ sK4) != (sK0 @ ~)) | ((sK1 @ sK4) = $false)),
% 1.53/1.34 inference(equality_proxy_clausification,[status(thm)],[f26])).
% 1.53/1.34 thf(f26,plain,(
% 1.53/1.34 ((sK1 @ sK4) = $false) | ($false = ((sK0 @ ~) = (~ sK4))) | ($false = (~ (sK0 @ (^[Y0 : $o]: ($false)))))),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f24])).
% 1.53/1.34 thf(f24,plain,(
% 1.53/1.34 ((sK1 @ sK4) = $false) | ((((sK0 @ ~) = (~ sK4)) | (sK0 @ (^[Y0 : $o]: ($true)))) = $false) | ($false = (~ (sK0 @ (^[Y0 : $o]: ($false)))))),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f23])).
% 1.53/1.34 thf(f23,plain,(
% 1.53/1.34 (((((sK0 @ ~) = (~ sK4)) | (sK0 @ (^[Y0 : $o]: ($true)))) & (~ (sK0 @ (^[Y0 : $o]: ($false))))) = $false) | ((sK1 @ sK4) = $false)),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f21])).
% 1.53/1.34 thf(f21,plain,(
% 1.53/1.34 ((sK1 @ sK4) != ((((sK0 @ ~) = (~ sK4)) | (sK0 @ (^[Y0 : $o]: ($true)))) & (~ (sK0 @ (^[Y0 : $o]: ($false))))))),
% 1.53/1.34 inference(beta_eta_normalization,[status(thm)],[f20])).
% 1.53/1.34 thf(f20,plain,(
% 1.53/1.34 ((sK1 @ sK4) != ((^[Y0 : $o]: ((((sK0 @ ~) = (~ Y0)) | (sK0 @ (^[Y1 : $o]: ($true)))) & (~ (sK0 @ (^[Y1 : $o]: ($false)))))) @ sK4))),
% 1.53/1.34 inference(negative_extensionality,[status(thm)],[f19])).
% 1.53/1.34 thf(f19,plain,(
% 1.53/1.34 (sK1 != (^[Y0 : $o]: ((((sK0 @ ~) = (~ Y0)) | (sK0 @ (^[Y1 : $o]: ($true)))) & (~ (sK0 @ (^[Y1 : $o]: ($false)))))))),
% 1.53/1.34 inference(trivial_inequality_removal,[status(thm)],[f18])).
% 1.53/1.34 thf(f18,plain,(
% 1.53/1.34 (sK1 != (^[Y0 : $o]: ((((sK0 @ ~) = (~ Y0)) | (sK0 @ (^[Y1 : $o]: ($true)))) & (~ (sK0 @ (^[Y1 : $o]: ($false))))))) | ($true != $true)),
% 1.53/1.34 inference(constrained_superposition,[status(thm)],[f17,f14])).
% 1.53/1.34 thf(f87,plain,(
% 1.53/1.34 spl2_8 | spl2_4 | spl2_10 | spl2_6),
% 1.53/1.34 inference(avatar_split_clause,[status(thm)],[f32,f66,f83,f57,f75])).
% 1.53/1.34 thf(f32,plain,(
% 1.53/1.34 ((sK1 @ sK4) = $false) | ($true = (sK0 @ ~)) | ((sK0 @ (^[Y0 : $o]: ($false))) = $true) | ($false = sK4)),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f29])).
% 1.53/1.34 thf(f29,plain,(
% 1.53/1.34 ((sK1 @ sK4) = $false) | ($true = (sK0 @ ~)) | ($true = (~ sK4)) | ((sK0 @ (^[Y0 : $o]: ($false))) = $true)),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f28])).
% 1.53/1.34 thf(f86,plain,(
% 1.53/1.34 spl2_8 | spl2_9 | spl2_10),
% 1.53/1.34 inference(avatar_split_clause,[status(thm)],[f33,f83,f79,f75])).
% 1.53/1.34 thf(f33,plain,(
% 1.53/1.34 ((sK0 @ (^[Y0 : $o]: ($false))) = $true) | ((sK1 @ sK4) = $false) | ((sK0 @ (^[Y0 : $o]: ($true))) = $false)),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f25])).
% 1.53/1.34 thf(f25,plain,(
% 1.53/1.34 ($false = (~ (sK0 @ (^[Y0 : $o]: ($false))))) | ((sK0 @ (^[Y0 : $o]: ($true))) = $false) | ((sK1 @ sK4) = $false)),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f24])).
% 1.53/1.34 thf(f73,plain,(
% 1.53/1.34 spl2_6 | spl2_7 | spl2_1 | spl2_3),
% 1.53/1.34 inference(avatar_split_clause,[status(thm)],[f40,f53,f44,f70,f66])).
% 1.53/1.34 thf(f40,plain,(
% 1.53/1.34 ($true = (sK0 @ ~)) | ($true = (sK0 @ (^[Y0 : $o]: ($true)))) | ((sK1 @ sK4) = $true) | ($true = sK4)),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f39])).
% 1.53/1.34 thf(f39,plain,(
% 1.53/1.34 ($true = (sK0 @ ~)) | ((~ sK4) = $false) | ((sK1 @ sK4) = $true) | ($true = (sK0 @ (^[Y0 : $o]: ($true))))),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f37])).
% 1.53/1.34 thf(f37,plain,(
% 1.53/1.34 ((~ sK4) = (sK0 @ ~)) | ((sK1 @ sK4) = $true) | ($true = (sK0 @ (^[Y0 : $o]: ($true))))),
% 1.53/1.34 inference(equality_proxy_clausification,[status(thm)],[f36])).
% 1.53/1.34 thf(f36,plain,(
% 1.53/1.34 ($true = ((sK0 @ ~) = (~ sK4))) | ($true = (sK0 @ (^[Y0 : $o]: ($true)))) | ((sK1 @ sK4) = $true)),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f35])).
% 1.53/1.34 thf(f35,plain,(
% 1.53/1.34 ($true = (((sK0 @ ~) = (~ sK4)) | (sK0 @ (^[Y0 : $o]: ($true))))) | ((sK1 @ sK4) = $true)),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f22])).
% 1.53/1.34 thf(f22,plain,(
% 1.53/1.34 ($true = ((((sK0 @ ~) = (~ sK4)) | (sK0 @ (^[Y0 : $o]: ($true)))) & (~ (sK0 @ (^[Y0 : $o]: ($false)))))) | ((sK1 @ sK4) = $true)),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f21])).
% 1.53/1.34 thf(f64,plain,(
% 1.53/1.34 spl2_1 | spl2_3 | spl2_4 | spl2_5),
% 1.53/1.34 inference(avatar_split_clause,[status(thm)],[f41,f61,f57,f53,f44])).
% 1.53/1.34 thf(f41,plain,(
% 1.53/1.34 ($false = (sK0 @ ~)) | ($false = sK4) | ((sK1 @ sK4) = $true) | ($true = (sK0 @ (^[Y0 : $o]: ($true))))),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f38])).
% 1.53/1.34 thf(f38,plain,(
% 1.53/1.34 ($false = (sK0 @ ~)) | ($true = (sK0 @ (^[Y0 : $o]: ($true)))) | ((sK1 @ sK4) = $true) | ($true = (~ sK4))),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f37])).
% 1.53/1.34 thf(f51,plain,(
% 1.53/1.34 spl2_1 | spl2_2),
% 1.53/1.34 inference(avatar_split_clause,[status(thm)],[f42,f48,f44])).
% 1.53/1.34 thf(f42,plain,(
% 1.53/1.34 ((sK0 @ (^[Y0 : $o]: ($false))) = $false) | ((sK1 @ sK4) = $true)),
% 1.53/1.34 inference(not_proxy_clausification,[status(thm)],[f34])).
% 1.53/1.34 thf(f34,plain,(
% 1.53/1.34 ($true = (~ (sK0 @ (^[Y0 : $o]: ($false))))) | ((sK1 @ sK4) = $true)),
% 1.53/1.34 inference(binary_proxy_clausification,[status(thm)],[f22])).
% 1.53/1.34 % SZS output end Proof for DTF2THF_30244
% 1.53/1.34 % (30341)------------------------------
% 1.53/1.34 % (30341)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.53/1.34 % (30341)Termination reason: Refutation
% 1.53/1.34
% 1.53/1.34 % (30341)Memory used [KB]: 5756
% 1.53/1.34 % (30341)Time elapsed: 0.024 s
% 1.53/1.34 % (30341)Instructions burned: 31 (million)
% 1.53/1.34 % (30341)------------------------------
% 1.53/1.34 % (30341)------------------------------
% 1.53/1.34 % (30340)Success in time 0.036 s
%------------------------------------------------------------------------------