%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : SEV261^5 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n020.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:40:42 AM UTC 2026
% Result : Theorem 1.76s 1.51s
% Output : Refutation 1.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 14
% Syntax : Number of formulae : 195 ( 7 unt; 0 typ; 13 def)
% Number of atoms : 1959 ( 643 equ; 0 cnn)
% Maximal formula atoms : 18 ( 10 avg)
% Number of connectives : 1748 ( 308 ~; 445 |; 181 &; 563 @)
% ( 13 <=>; 102 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 359 ( 359 >; 0 *; 0 +; 0 <<)
% Number of symbols : 41 ( 36 usr; 29 con; 0-2 aty)
% ( 107 !!; 29 ??; 0 @@+; 0 @@-)
% Number of variables : 686 ( 604 ^; 79 !; 3 ?; 686 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
a: $tType ).
thf(func_def_0,type,
a: $tType ).
thf(func_def_17,type,
ph1:
!>[X0: $tType] : X0 ).
thf(func_def_18,type,
sK2: a > $o ).
thf(func_def_19,type,
sK3: a > $o ).
thf(func_def_20,type,
sK4: a > $o ).
thf(func_def_21,type,
sK5: ( a > $o ) > $o ).
thf(func_def_22,type,
sK6: a ).
thf(func_def_23,type,
sK7: ( a > $o ) > $o ).
thf(func_def_24,type,
sK8: a ).
thf(func_def_25,type,
sK9: a > a > $o ).
thf(func_def_26,type,
sK10: a > $o ).
thf(func_def_27,type,
sK11: a ).
thf(func_def_28,type,
sK12: a > $o ).
thf(func_def_29,type,
sK13: a > $o ).
thf(func_def_30,type,
sK14: a > $o ).
thf(func_def_31,type,
sK15: a ).
thf(func_def_32,type,
sK16: a ).
thf(func_def_33,type,
sK17: a ).
thf(func_def_34,type,
sK18: a ).
thf(func_def_35,type,
sK19: a ).
thf(func_def_36,type,
sK20: a ).
thf(func_def_37,type,
sK21: a ).
thf(func_def_38,type,
sK22: a ).
thf(func_def_39,type,
sK23: a ).
thf(f553,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[f18,f28,f45,f56,f69,f284,f304,f351,f362,f406,f444,f499,f524,f552]) ).
thf(f552,plain,
( ~ spl0_1
| ~ spl0_13
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[status(thm)],[f551]) ).
thf(f551,plain,
( $false
| ~ spl0_1
| ~ spl0_13
| ~ spl0_15 ),
inference(subsumption_resolution,[status(thm)],[f550,f475]) ).
thf(f475,plain,
( ! [X1: a] :
( ( sK10 @ X1 )
= ( sK12 @ X1 ) )
| ~ spl0_1
| ~ spl0_13 ),
inference(boolean_simplification,[status(thm)],[f474]) ).
thf(f474,plain,
( ! [X1: a] :
( ( sK12 @ X1 )
= ( $true
& ( sK10 @ X1 ) ) )
| ~ spl0_1
| ~ spl0_13 ),
inference(forward_demodulation,[status(thm)],[f473,f455]) ).
thf(f455,plain,
( ! [X1: a] :
( ( sK14 @ X1 )
= $true )
| ~ spl0_13 ),
inference(beta_eta_normalization,[status(thm)],[f454]) ).
thf(f454,plain,
( ! [X1: a] :
( ( sK14 @ X1 )
= ( ^ [Y0: a] : $true
@ X1 ) )
| ~ spl0_13 ),
inference(argument_congruence,[status(thm)],[f447]) ).
thf(f447,plain,
( ( ( ^ [Y0: a] : $true )
= sK14 )
| ~ spl0_13 ),
inference(equality_proxy_clausification,[status(thm)],[f405]) ).
thf(f405,plain,
( ( $true
= ( sK14
= ( ^ [Y0: a] : $true ) ) )
| ~ spl0_13 ),
inference(avatar_component_clause,[status(thm)],[f404]) ).
thf(f404,definition,
( spl0_13
<=> ( $true
= ( sK14
= ( ^ [Y0: a] : $true ) ) ) ),
introduced(definition,[new_symbols(naming,[spl0_13])],[avatar_definition]) ).
thf(f473,plain,
( ! [X1: a] :
( ( ( sK14 @ X1 )
& ( sK10 @ X1 ) )
= ( sK12 @ X1 ) )
| ~ spl0_1
| ~ spl0_13 ),
inference(beta_eta_normalization,[status(thm)],[f472]) ).
thf(f472,plain,
( ! [X1: a] :
( ( ^ [Y0: a] :
( ( sK14 @ Y0 )
& ( sK10 @ Y0 ) )
@ X1 )
= ( sK12 @ X1 ) )
| ~ spl0_1
| ~ spl0_13 ),
inference(argument_congruence,[status(thm)],[f467]) ).
thf(f467,plain,
( ( sK12
= ( ^ [Y0: a] :
( ( sK14 @ Y0 )
& ( sK10 @ Y0 ) ) ) )
| ~ spl0_1
| ~ spl0_13 ),
inference(equality_proxy_clausification,[status(thm)],[f464]) ).
thf(f464,plain,
( ( ( ( ^ [Y0: a] :
( ( sK14 @ Y0 )
& ( sK10 @ Y0 ) ) )
= sK12 )
= $true )
| ~ spl0_1
| ~ spl0_13 ),
inference(boolean_simplification,[status(thm)],[f462]) ).
thf(f462,plain,
( ( $true
= ( $true
& ( ( ^ [Y0: a] :
( ( sK14 @ Y0 )
& ( sK10 @ Y0 ) ) )
= sK12 ) ) )
| ~ spl0_1
| ~ spl0_13 ),
inference(backward_demodulation,[status(thm)],[f451,f461]) ).
thf(f461,plain,
( ( $true
= ( ( sK14 = sK10 )
| ( sK10
= ( ^ [Y0: a] : $false ) ) ) )
| ~ spl0_1
| ~ spl0_13 ),
inference(binary_proxy_clausification,[status(thm)],[f451]) ).
thf(f451,plain,
( ( ( ( ( sK14 = sK10 )
| ( sK10
= ( ^ [Y0: a] : $false ) ) )
& ( ( ^ [Y0: a] :
( ( sK14 @ Y0 )
& ( sK10 @ Y0 ) ) )
= sK12 ) )
= $true )
| ~ spl0_1
| ~ spl0_13 ),
inference(backward_demodulation,[status(thm)],[f396,f447]) ).
thf(f396,plain,
( ( $true
= ( ( ( ( ^ [Y0: a] : $true )
= sK10 )
| ( sK10
= ( ^ [Y0: a] : $false ) ) )
& ( ( ^ [Y0: a] :
( ( sK14 @ Y0 )
& ( sK10 @ Y0 ) ) )
= sK12 ) ) )
| ~ spl0_1 ),
inference(binary_proxy_clausification,[status(thm)],[f390]) ).
thf(f390,plain,
( ( ( ( ( ( ^ [Y0: a] : $true )
= sK10 )
| ( sK10
= ( ^ [Y0: a] : $false ) ) )
& ( ( ^ [Y0: a] :
( ( sK14 @ Y0 )
& ( sK10 @ Y0 ) ) )
= sK12 )
& ( ( sK14
= ( ^ [Y0: a] : $true ) )
| ( ( ^ [Y0: a] : $false )
= sK14 ) ) )
= $true )
| ~ spl0_1 ),
inference(not_proxy_clausification,[status(thm)],[f386]) ).
thf(f386,plain,
( ( $false
= ( ~ ( ( ( ( ^ [Y0: a] : $true )
= sK10 )
| ( sK10
= ( ^ [Y0: a] : $false ) ) )
& ( ( ^ [Y0: a] :
( ( sK14 @ Y0 )
& ( sK10 @ Y0 ) ) )
= sK12 )
& ( ( sK14
= ( ^ [Y0: a] : $true ) )
| ( ( ^ [Y0: a] : $false )
= sK14 ) ) ) ) )
| ~ spl0_1 ),
inference(beta_eta_normalization,[status(thm)],[f385]) ).
thf(f385,plain,
( ( $false
= ( ^ [Y0: a > $o] :
~ ( ( ( ( ^ [Y1: a] : $true )
= sK10 )
| ( sK10
= ( ^ [Y1: a] : $false ) ) )
& ( ( ^ [Y1: a] :
( ( Y0 @ Y1 )
& ( sK10 @ Y1 ) ) )
= sK12 )
& ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) )
@ sK14 ) )
| ~ spl0_1 ),
inference(sigma_clausification,[status(thm)],[f377]) ).
thf(f377,plain,
( ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
~ ( ( ( ( ^ [Y1: a] : $true )
= sK10 )
| ( sK10
= ( ^ [Y1: a] : $false ) ) )
& ( ( ^ [Y1: a] :
( ( Y0 @ Y1 )
& ( sK10 @ Y1 ) ) )
= sK12 )
& ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) ) )
| ~ spl0_1 ),
inference(boolean_simplification,[status(thm)],[f376]) ).
thf(f376,plain,
( ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( ( ( ^ [Y1: a] : $true )
= sK10 )
| ( sK10
= ( ^ [Y1: a] : $false ) ) )
& ( ( ^ [Y1: a] :
( ( Y0 @ Y1 )
& ( sK10 @ Y1 ) ) )
= sK12 )
& ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) )
=> $false ) ) )
| ~ spl0_1 ),
inference(backward_demodulation,[status(thm)],[f370,f373]) ).
thf(f373,plain,
( ( ( ( sK12
= ( ^ [Y0: a] : $false ) )
| ( sK12
= ( ^ [Y0: a] : $true ) ) )
= $false )
| ~ spl0_1 ),
inference(binary_proxy_clausification,[status(thm)],[f372]) ).
thf(f372,plain,
( ( $false
= ( ( ( ( ( ^ [Y0: a] : $true )
= sK10 )
| ( sK10
= ( ^ [Y0: a] : $false ) ) )
& ( ( ^ [Y0: a] :
( ( sK13 @ Y0 )
& ( sK10 @ Y0 ) ) )
= sK12 )
& ( ( sK13
= ( ^ [Y0: a] : $true ) )
| ( ( ^ [Y0: a] : $false )
= sK13 ) ) )
=> ( ( sK12
= ( ^ [Y0: a] : $false ) )
| ( sK12
= ( ^ [Y0: a] : $true ) ) ) ) )
| ~ spl0_1 ),
inference(beta_eta_normalization,[status(thm)],[f371]) ).
thf(f371,plain,
( ( ( ^ [Y0: a > $o] :
( ( ( ( ( ^ [Y1: a] : $true )
= sK10 )
| ( sK10
= ( ^ [Y1: a] : $false ) ) )
& ( ( ^ [Y1: a] :
( ( Y0 @ Y1 )
& ( sK10 @ Y1 ) ) )
= sK12 )
& ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) )
=> ( ( sK12
= ( ^ [Y1: a] : $false ) )
| ( sK12
= ( ^ [Y1: a] : $true ) ) ) )
@ sK13 )
= $false )
| ~ spl0_1 ),
inference(sigma_clausification,[status(thm)],[f370]) ).
thf(f370,plain,
( ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( ( ( ^ [Y1: a] : $true )
= sK10 )
| ( sK10
= ( ^ [Y1: a] : $false ) ) )
& ( ( ^ [Y1: a] :
( ( Y0 @ Y1 )
& ( sK10 @ Y1 ) ) )
= sK12 )
& ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) )
=> ( ( sK12
= ( ^ [Y1: a] : $false ) )
| ( sK12
= ( ^ [Y1: a] : $true ) ) ) ) ) )
| ~ spl0_1 ),
inference(beta_eta_normalization,[status(thm)],[f369]) ).
thf(f369,plain,
( ( ( ^ [Y0: a > $o] :
( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( ( ( ^ [Y2: a] : $true )
= sK10 )
| ( sK10
= ( ^ [Y2: a] : $false ) ) )
& ( ( ^ [Y2: a] :
( ( Y1 @ Y2 )
& ( sK10 @ Y2 ) ) )
= Y0 )
& ( ( Y1
= ( ^ [Y2: a] : $true ) )
| ( ( ^ [Y2: a] : $false )
= Y1 ) ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : $true ) ) ) ) )
@ sK12 )
= $false )
| ~ spl0_1 ),
inference(sigma_clausification,[status(thm)],[f366]) ).
thf(f366,plain,
( ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( ( ( ^ [Y2: a] : $true )
= sK10 )
| ( sK10
= ( ^ [Y2: a] : $false ) ) )
& ( ( ^ [Y2: a] :
( ( Y1 @ Y2 )
& ( sK10 @ Y2 ) ) )
= Y0 )
& ( ( Y1
= ( ^ [Y2: a] : $true ) )
| ( ( ^ [Y2: a] : $false )
= Y1 ) ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : $true ) ) ) ) ) ) )
| ~ spl0_1 ),
inference(beta_eta_normalization,[status(thm)],[f365]) ).
thf(f365,plain,
( ( ( ^ [Y0: a > $o] :
( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( ( ( ^ [Y3: a] : $true )
= Y0 )
| ( Y0
= ( ^ [Y3: a] : $false ) ) )
& ( ( ^ [Y3: a] :
( ( Y2 @ Y3 )
& ( Y0 @ Y3 ) ) )
= Y1 )
& ( ( Y2
= ( ^ [Y3: a] : $true ) )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) )
=> ( ( Y1
= ( ^ [Y3: a] : $false ) )
| ( Y1
= ( ^ [Y3: a] : $true ) ) ) ) ) )
@ sK10 )
= $false )
| ~ spl0_1 ),
inference(sigma_clausification,[status(thm)],[f14]) ).
thf(f14,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( ( ( ^ [Y3: a] : $true )
= Y0 )
| ( Y0
= ( ^ [Y3: a] : $false ) ) )
& ( ( ^ [Y3: a] :
( ( Y2 @ Y3 )
& ( Y0 @ Y3 ) ) )
= Y1 )
& ( ( Y2
= ( ^ [Y3: a] : $true ) )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) )
=> ( ( Y1
= ( ^ [Y3: a] : $false ) )
| ( Y1
= ( ^ [Y3: a] : $true ) ) ) ) ) ) )
= $false )
| ~ spl0_1 ),
inference(avatar_component_clause,[status(thm)],[f13]) ).
thf(f13,definition,
( spl0_1
<=> ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( ( ( ^ [Y3: a] : $true )
= Y0 )
| ( Y0
= ( ^ [Y3: a] : $false ) ) )
& ( ( ^ [Y3: a] :
( ( Y2 @ Y3 )
& ( Y0 @ Y3 ) ) )
= Y1 )
& ( ( Y2
= ( ^ [Y3: a] : $true ) )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) )
=> ( ( Y1
= ( ^ [Y3: a] : $false ) )
| ( Y1
= ( ^ [Y3: a] : $true ) ) ) ) ) ) )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl0_1])],[avatar_definition]) ).
thf(f550,plain,
( ( ( sK10 @ sK23 )
!= ( sK12 @ sK23 ) )
| ~ spl0_1
| ~ spl0_15 ),
inference(negative_extensionality,[status(thm)],[f545]) ).
thf(f545,plain,
( ( sK12 != sK10 )
| ~ spl0_1
| ~ spl0_15 ),
inference(backward_demodulation,[status(thm)],[f387,f542]) ).
thf(f542,plain,
( ( sK10
= ( ^ [Y0: a] : $false ) )
| ~ spl0_15 ),
inference(equality_proxy_clausification,[status(thm)],[f498]) ).
thf(f498,plain,
( ( $true
= ( sK10
= ( ^ [Y0: a] : $false ) ) )
| ~ spl0_15 ),
inference(avatar_component_clause,[status(thm)],[f497]) ).
thf(f497,definition,
( spl0_15
<=> ( $true
= ( sK10
= ( ^ [Y0: a] : $false ) ) ) ),
introduced(definition,[new_symbols(naming,[spl0_15])],[avatar_definition]) ).
thf(f387,plain,
( ( sK12
!= ( ^ [Y0: a] : $false ) )
| ~ spl0_1 ),
inference(equality_proxy_clausification,[status(thm)],[f384]) ).
thf(f384,plain,
( ( ( sK12
= ( ^ [Y0: a] : $false ) )
= $false )
| ~ spl0_1 ),
inference(boolean_simplification,[status(thm)],[f383]) ).
thf(f383,plain,
( ( $false
= ( ( sK12
= ( ^ [Y0: a] : $false ) )
| $false ) )
| ~ spl0_1 ),
inference(backward_demodulation,[status(thm)],[f373,f381]) ).
thf(f381,plain,
( ( ( sK12
= ( ^ [Y0: a] : $true ) )
= $false )
| ~ spl0_1 ),
inference(binary_proxy_clausification,[status(thm)],[f373]) ).
thf(f524,plain,
( ~ spl0_1
| ~ spl0_13
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[status(thm)],[f523]) ).
thf(f523,plain,
( $false
| ~ spl0_1
| ~ spl0_13
| ~ spl0_14 ),
inference(subsumption_resolution,[status(thm)],[f522,f511]) ).
thf(f511,plain,
( ! [X1: a] :
( $true
= ( sK10 @ X1 ) )
| ~ spl0_13
| ~ spl0_14 ),
inference(forward_demodulation,[status(thm)],[f510,f455]) ).
thf(f510,plain,
( ! [X1: a] :
( ( sK14 @ X1 )
= ( sK10 @ X1 ) )
| ~ spl0_14 ),
inference(argument_congruence,[status(thm)],[f502]) ).
thf(f502,plain,
( ( sK10 = sK14 )
| ~ spl0_14 ),
inference(equality_proxy_clausification,[status(thm)],[f495]) ).
thf(f495,plain,
( ( ( sK14 = sK10 )
= $true )
| ~ spl0_14 ),
inference(avatar_component_clause,[status(thm)],[f494]) ).
thf(f494,definition,
( spl0_14
<=> ( ( sK14 = sK10 )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl0_14])],[avatar_definition]) ).
thf(f522,plain,
( ( $true
!= ( sK10 @ sK20 ) )
| ~ spl0_1
| ~ spl0_13
| ~ spl0_14 ),
inference(forward_demodulation,[status(thm)],[f521,f517]) ).
thf(f517,plain,
( ! [X1: a] :
( $true
= ( sK12 @ X1 ) )
| ~ spl0_1
| ~ spl0_13
| ~ spl0_14 ),
inference(trivial_inequality_removal,[status(thm)],[f513]) ).
thf(f513,plain,
( ! [X1: a] :
( ( $true = $false )
| ( $true
= ( sK12 @ X1 ) ) )
| ~ spl0_1
| ~ spl0_13
| ~ spl0_14 ),
inference(backward_demodulation,[status(thm)],[f481,f511]) ).
thf(f481,plain,
( ! [X1: a] :
( ( $true
= ( sK12 @ X1 ) )
| ( $false
= ( sK10 @ X1 ) ) )
| ~ spl0_1
| ~ spl0_13 ),
inference(binary_proxy_clausification,[status(thm)],[f475]) ).
thf(f521,plain,
( ( ( sK10 @ sK20 )
!= ( sK12 @ sK20 ) )
| ~ spl0_1
| ~ spl0_13
| ~ spl0_14 ),
inference(negative_extensionality,[status(thm)],[f505]) ).
thf(f505,plain,
( ( sK12 != sK10 )
| ~ spl0_1
| ~ spl0_13
| ~ spl0_14 ),
inference(backward_demodulation,[status(thm)],[f466,f502]) ).
thf(f466,plain,
( ( sK12 != sK14 )
| ~ spl0_1
| ~ spl0_13 ),
inference(equality_proxy_clausification,[status(thm)],[f450]) ).
thf(f450,plain,
( ( $false
= ( sK12 = sK14 ) )
| ~ spl0_1
| ~ spl0_13 ),
inference(backward_demodulation,[status(thm)],[f381,f447]) ).
thf(f499,plain,
( spl0_14
| spl0_15
| ~ spl0_1
| ~ spl0_13 ),
inference(avatar_split_clause,[status(thm)],[f492,f404,f13,f497,f494]) ).
thf(f492,plain,
( ( ( sK14 = sK10 )
= $true )
| ( $true
= ( sK10
= ( ^ [Y0: a] : $false ) ) )
| ~ spl0_1
| ~ spl0_13 ),
inference(binary_proxy_clausification,[status(thm)],[f461]) ).
thf(f444,plain,
( ~ spl0_1
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[status(thm)],[f443]) ).
thf(f443,plain,
( $false
| ~ spl0_1
| ~ spl0_12 ),
inference(trivial_inequality_removal,[status(thm)],[f440]) ).
thf(f440,plain,
( ( $false != $false )
| ~ spl0_1
| ~ spl0_12 ),
inference(superposition,[status(thm)],[f422,f438]) ).
thf(f438,plain,
( ! [X1: a] :
( $false
= ( sK12 @ X1 ) )
| ~ spl0_1
| ~ spl0_12 ),
inference(boolean_simplification,[status(thm)],[f437]) ).
thf(f437,plain,
( ! [X1: a] :
( ( $false
& ( sK10 @ X1 ) )
= ( sK12 @ X1 ) )
| ~ spl0_1
| ~ spl0_12 ),
inference(forward_demodulation,[status(thm)],[f436,f419]) ).
thf(f419,plain,
( ! [X1: a] :
( ( sK14 @ X1 )
= $false )
| ~ spl0_12 ),
inference(beta_eta_normalization,[status(thm)],[f417]) ).
thf(f417,plain,
( ! [X1: a] :
( ( ^ [Y0: a] : $false
@ X1 )
= ( sK14 @ X1 ) )
| ~ spl0_12 ),
inference(argument_congruence,[status(thm)],[f409]) ).
thf(f409,plain,
( ( ( ^ [Y0: a] : $false )
= sK14 )
| ~ spl0_12 ),
inference(equality_proxy_clausification,[status(thm)],[f402]) ).
thf(f402,plain,
( ( $true
= ( ( ^ [Y0: a] : $false )
= sK14 ) )
| ~ spl0_12 ),
inference(avatar_component_clause,[status(thm)],[f401]) ).
thf(f401,definition,
( spl0_12
<=> ( $true
= ( ( ^ [Y0: a] : $false )
= sK14 ) ) ),
introduced(definition,[new_symbols(naming,[spl0_12])],[avatar_definition]) ).
thf(f436,plain,
( ! [X1: a] :
( ( ( sK14 @ X1 )
& ( sK10 @ X1 ) )
= ( sK12 @ X1 ) )
| ~ spl0_1
| ~ spl0_12 ),
inference(beta_eta_normalization,[status(thm)],[f435]) ).
thf(f435,plain,
( ! [X1: a] :
( ( ^ [Y0: a] :
( ( sK14 @ Y0 )
& ( sK10 @ Y0 ) )
@ X1 )
= ( sK12 @ X1 ) )
| ~ spl0_1
| ~ spl0_12 ),
inference(argument_congruence,[status(thm)],[f429]) ).
thf(f429,plain,
( ( sK12
= ( ^ [Y0: a] :
( ( sK14 @ Y0 )
& ( sK10 @ Y0 ) ) ) )
| ~ spl0_1
| ~ spl0_12 ),
inference(equality_proxy_clausification,[status(thm)],[f427]) ).
thf(f427,plain,
( ( ( ( ^ [Y0: a] :
( ( sK14 @ Y0 )
& ( sK10 @ Y0 ) ) )
= sK12 )
= $true )
| ~ spl0_1
| ~ spl0_12 ),
inference(boolean_simplification,[status(thm)],[f426]) ).
thf(f426,plain,
( ( $true
= ( $true
& ( ( ^ [Y0: a] :
( ( sK14 @ Y0 )
& ( sK10 @ Y0 ) ) )
= sK12 ) ) )
| ~ spl0_1
| ~ spl0_12 ),
inference(backward_demodulation,[status(thm)],[f414,f424]) ).
thf(f424,plain,
( ( $true
= ( ( ( ^ [Y0: a] : $true )
= sK10 )
| ( sK10 = sK14 ) ) )
| ~ spl0_1
| ~ spl0_12 ),
inference(binary_proxy_clausification,[status(thm)],[f414]) ).
thf(f414,plain,
( ( ( ( ( ( ^ [Y0: a] : $true )
= sK10 )
| ( sK10 = sK14 ) )
& ( ( ^ [Y0: a] :
( ( sK14 @ Y0 )
& ( sK10 @ Y0 ) ) )
= sK12 ) )
= $true )
| ~ spl0_1
| ~ spl0_12 ),
inference(backward_demodulation,[status(thm)],[f396,f409]) ).
thf(f422,plain,
( ( $false
!= ( sK12 @ sK16 ) )
| ~ spl0_1
| ~ spl0_12 ),
inference(forward_demodulation,[status(thm)],[f421,f419]) ).
thf(f421,plain,
( ( ( sK12 @ sK16 )
!= ( sK14 @ sK16 ) )
| ~ spl0_1
| ~ spl0_12 ),
inference(negative_extensionality,[status(thm)],[f418]) ).
thf(f418,plain,
( ( sK12 != sK14 )
| ~ spl0_1
| ~ spl0_12 ),
inference(superposition,[status(thm)],[f387,f409]) ).
thf(f406,plain,
( spl0_12
| spl0_13
| ~ spl0_1 ),
inference(avatar_split_clause,[status(thm)],[f399,f13,f404,f401]) ).
thf(f399,plain,
( ( $true
= ( sK14
= ( ^ [Y0: a] : $true ) ) )
| ( $true
= ( ( ^ [Y0: a] : $false )
= sK14 ) )
| ~ spl0_1 ),
inference(binary_proxy_clausification,[status(thm)],[f398]) ).
thf(f398,plain,
( ( ( ( sK14
= ( ^ [Y0: a] : $true ) )
| ( ( ^ [Y0: a] : $false )
= sK14 ) )
= $true )
| ~ spl0_1 ),
inference(boolean_simplification,[status(thm)],[f397]) ).
thf(f397,plain,
( ( $true
= ( $true
& ( ( sK14
= ( ^ [Y0: a] : $true ) )
| ( ( ^ [Y0: a] : $false )
= sK14 ) ) ) )
| ~ spl0_1 ),
inference(backward_demodulation,[status(thm)],[f390,f396]) ).
thf(f362,plain,
( ~ spl0_6
| ~ spl0_10 ),
inference(avatar_contradiction_clause,[status(thm)],[f361]) ).
thf(f361,plain,
( $false
| ~ spl0_6
| ~ spl0_10 ),
inference(trivial_inequality_removal,[status(thm)],[f360]) ).
thf(f360,plain,
( ( $false != $false )
| ~ spl0_6
| ~ spl0_10 ),
inference(superposition,[status(thm)],[f97,f299]) ).
thf(f299,plain,
( ! [X0: a] :
( ( sK4 @ X0 )
= $false )
| ~ spl0_10 ),
inference(avatar_component_clause,[status(thm)],[f298]) ).
thf(f298,definition,
( spl0_10
<=> ! [X0: a] :
( ( sK4 @ X0 )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl0_10])],[avatar_definition]) ).
thf(f97,plain,
( ( $false
!= ( sK4 @ sK8 ) )
| ~ spl0_6 ),
inference(beta_eta_normalization,[status(thm)],[f96]) ).
thf(f96,plain,
( ( ( sK4 @ sK8 )
!= ( ^ [Y0: a] : $false
@ sK8 ) )
| ~ spl0_6 ),
inference(negative_extensionality,[status(thm)],[f92]) ).
thf(f92,plain,
( ( sK4
!= ( ^ [Y0: a] : $false ) )
| ~ spl0_6 ),
inference(equality_proxy_clausification,[status(thm)],[f84]) ).
thf(f84,plain,
( ( ( sK4
= ( ^ [Y0: a] : $false ) )
= $false )
| ~ spl0_6 ),
inference(binary_proxy_clausification,[status(thm)],[f80]) ).
thf(f80,plain,
( ( $false
= ( ( sK4
= ( ^ [Y0: a] : $false ) )
| ( sK4
= ( ^ [Y0: a] : $true ) ) ) )
| ~ spl0_6 ),
inference(boolean_simplification,[status(thm)],[f79]) ).
thf(f79,plain,
( ( ( $true
=> ( ( sK4
= ( ^ [Y0: a] : $false ) )
| ( sK4
= ( ^ [Y0: a] : $true ) ) ) )
= $false )
| ~ spl0_6 ),
inference(backward_demodulation,[status(thm)],[f76,f78]) ).
thf(f78,plain,
( ( $true
= ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK5 @ Y0 )
=> ( ( ( ^ [Y1: a] : $true )
= Y0 )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& ( ( ^ [Y0: a] :
( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y1 @ Y0 )
& ( sK5 @ Y1 ) ) ) )
= sK4 ) ) )
| ~ spl0_6 ),
inference(binary_proxy_clausification,[status(thm)],[f76]) ).
thf(f76,plain,
( ( $false
= ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK5 @ Y0 )
=> ( ( ( ^ [Y1: a] : $true )
= Y0 )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& ( ( ^ [Y0: a] :
( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y1 @ Y0 )
& ( sK5 @ Y1 ) ) ) )
= sK4 ) )
=> ( ( sK4
= ( ^ [Y0: a] : $false ) )
| ( sK4
= ( ^ [Y0: a] : $true ) ) ) ) )
| ~ spl0_6 ),
inference(beta_eta_normalization,[status(thm)],[f75]) ).
thf(f75,plain,
( ( $false
= ( ^ [Y0: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y0 @ Y1 )
=> ( ( ( ^ [Y2: a] : $true )
= Y1 )
| ( ( ^ [Y2: a] : $false )
= Y1 ) ) ) )
& ( ( ^ [Y1: a] :
( ?? @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y2 @ Y1 )
& ( Y0 @ Y2 ) ) ) )
= sK4 ) )
=> ( ( sK4
= ( ^ [Y1: a] : $false ) )
| ( sK4
= ( ^ [Y1: a] : $true ) ) ) )
@ sK5 ) )
| ~ spl0_6 ),
inference(sigma_clausification,[status(thm)],[f74]) ).
thf(f74,plain,
( ( $false
= ( !! @ ( ( a > $o ) > $o )
@ ^ [Y0: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y0 @ Y1 )
=> ( ( ( ^ [Y2: a] : $true )
= Y1 )
| ( ( ^ [Y2: a] : $false )
= Y1 ) ) ) )
& ( ( ^ [Y1: a] :
( ?? @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y2 @ Y1 )
& ( Y0 @ Y2 ) ) ) )
= sK4 ) )
=> ( ( sK4
= ( ^ [Y1: a] : $false ) )
| ( sK4
= ( ^ [Y1: a] : $true ) ) ) ) ) )
| ~ spl0_6 ),
inference(beta_eta_normalization,[status(thm)],[f73]) ).
thf(f73,plain,
( ( ( ^ [Y0: a > $o] :
( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( ( ( ^ [Y3: a] : $true )
= Y2 )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) ) )
& ( ( ^ [Y2: a] :
( ?? @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y3 @ Y2 )
& ( Y1 @ Y3 ) ) ) )
= Y0 ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : $true ) ) ) ) )
@ sK4 )
= $false )
| ~ spl0_6 ),
inference(sigma_clausification,[status(thm)],[f55]) ).
thf(f55,plain,
( ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( ( ( ^ [Y3: a] : $true )
= Y2 )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) ) )
& ( ( ^ [Y2: a] :
( ?? @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y3 @ Y2 )
& ( Y1 @ Y3 ) ) ) )
= Y0 ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : $true ) ) ) ) ) ) )
| ~ spl0_6 ),
inference(avatar_component_clause,[status(thm)],[f54]) ).
thf(f54,definition,
( spl0_6
<=> ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( ( ( ^ [Y3: a] : $true )
= Y2 )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) ) )
& ( ( ^ [Y2: a] :
( ?? @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y3 @ Y2 )
& ( Y1 @ Y3 ) ) ) )
= Y0 ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : $true ) ) ) ) ) ) ) ),
introduced(definition,[new_symbols(naming,[spl0_6])],[avatar_definition]) ).
thf(f351,plain,
( ~ spl0_6
| ~ spl0_9 ),
inference(avatar_contradiction_clause,[status(thm)],[f350]) ).
thf(f350,plain,
( $false
| ~ spl0_6
| ~ spl0_9 ),
inference(trivial_inequality_removal,[status(thm)],[f347]) ).
thf(f347,plain,
( ( $true = $false )
| ~ spl0_6
| ~ spl0_9 ),
inference(superposition,[status(thm)],[f138,f322]) ).
thf(f322,plain,
( ! [X0: a] :
( ( sK4 @ X0 )
= $true )
| ~ spl0_6
| ~ spl0_9 ),
inference(trivial_inequality_removal,[status(thm)],[f321]) ).
thf(f321,plain,
( ! [X0: a] :
( ( $true = $false )
| ( ( sK4 @ X0 )
= $true ) )
| ~ spl0_6
| ~ spl0_9 ),
inference(beta_eta_normalization,[status(thm)],[f320]) ).
thf(f320,plain,
( ! [X0: a] :
( ( ( sK4 @ X0 )
= $true )
| ( ( ^ [Y0: a] : $true
@ X0 )
= $false ) )
| ~ spl0_6
| ~ spl0_9 ),
inference(trivial_inequality_removal,[status(thm)],[f306]) ).
thf(f306,plain,
( ! [X0: a] :
( ( ( sK4 @ X0 )
= $true )
| ( $true = $false )
| ( ( ^ [Y0: a] : $true
@ X0 )
= $false ) )
| ~ spl0_6
| ~ spl0_9 ),
inference(superposition,[status(thm)],[f282,f153]) ).
thf(f153,plain,
( ! [X2: a > $o,X1: a] :
( ( ( sK7 @ X2 )
= $false )
| ( ( sK4 @ X1 )
= $true )
| ( ( X2 @ X1 )
= $false ) )
| ~ spl0_6 ),
inference(binary_proxy_clausification,[status(thm)],[f129]) ).
thf(f129,plain,
( ! [X2: a > $o,X1: a] :
( ( ( ( X2 @ X1 )
& ( sK7 @ X2 ) )
= $false )
| ( ( sK4 @ X1 )
= $true ) )
| ~ spl0_6 ),
inference(beta_eta_normalization,[status(thm)],[f126]) ).
thf(f126,plain,
( ! [X2: a > $o,X1: a] :
( ( $false
= ( ^ [Y0: a > $o] :
( ( Y0 @ X1 )
& ( sK7 @ Y0 ) )
@ X2 ) )
| ( ( sK4 @ X1 )
= $true ) )
| ~ spl0_6 ),
inference(pi_clausification,[status(thm)],[f114]) ).
thf(f114,plain,
( ! [X1: a] :
( ( $false
= ( ?? @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0 @ X1 )
& ( sK7 @ Y0 ) ) ) )
| ( ( sK4 @ X1 )
= $true ) )
| ~ spl0_6 ),
inference(binary_proxy_clausification,[status(thm)],[f109]) ).
thf(f109,plain,
( ! [X1: a] :
( ( sK4 @ X1 )
= ( ?? @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0 @ X1 )
& ( sK7 @ Y0 ) ) ) )
| ~ spl0_6 ),
inference(beta_eta_normalization,[status(thm)],[f108]) ).
thf(f108,plain,
( ! [X1: a] :
( ( ^ [Y0: a] :
( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y1 @ Y0 )
& ( sK7 @ Y1 ) ) )
@ X1 )
= ( sK4 @ X1 ) )
| ~ spl0_6 ),
inference(argument_congruence,[status(thm)],[f104]) ).
thf(f104,plain,
( ( sK4
= ( ^ [Y0: a] :
( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y1 @ Y0 )
& ( sK7 @ Y1 ) ) ) ) )
| ~ spl0_6 ),
inference(equality_proxy_clausification,[status(thm)],[f98]) ).
thf(f98,plain,
( ( $true
= ( ( ^ [Y0: a] :
( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y1 @ Y0 )
& ( sK7 @ Y1 ) ) ) )
= sK4 ) )
| ~ spl0_6 ),
inference(binary_proxy_clausification,[status(thm)],[f93]) ).
thf(f93,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK7 @ Y0 )
=> ( ( ( ^ [Y1: a] : $true )
= Y0 )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& ( ( ^ [Y0: a] :
( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y1 @ Y0 )
& ( sK7 @ Y1 ) ) ) )
= sK4 ) )
= $true )
| ~ spl0_6 ),
inference(not_proxy_clausification,[status(thm)],[f91]) ).
thf(f91,plain,
( ( $false
= ( ~ ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK7 @ Y0 )
=> ( ( ( ^ [Y1: a] : $true )
= Y0 )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& ( ( ^ [Y0: a] :
( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y1 @ Y0 )
& ( sK7 @ Y1 ) ) ) )
= sK4 ) ) ) )
| ~ spl0_6 ),
inference(beta_eta_normalization,[status(thm)],[f90]) ).
thf(f90,plain,
( ( $false
= ( ^ [Y0: ( a > $o ) > $o] :
~ ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y0 @ Y1 )
=> ( ( ( ^ [Y2: a] : $true )
= Y1 )
| ( ( ^ [Y2: a] : $false )
= Y1 ) ) ) )
& ( ( ^ [Y1: a] :
( ?? @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y2 @ Y1 )
& ( Y0 @ Y2 ) ) ) )
= sK4 ) )
@ sK7 ) )
| ~ spl0_6 ),
inference(sigma_clausification,[status(thm)],[f82]) ).
thf(f82,plain,
( ( $false
= ( !! @ ( ( a > $o ) > $o )
@ ^ [Y0: ( a > $o ) > $o] :
~ ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y0 @ Y1 )
=> ( ( ( ^ [Y2: a] : $true )
= Y1 )
| ( ( ^ [Y2: a] : $false )
= Y1 ) ) ) )
& ( ( ^ [Y1: a] :
( ?? @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y2 @ Y1 )
& ( Y0 @ Y2 ) ) ) )
= sK4 ) ) ) )
| ~ spl0_6 ),
inference(boolean_simplification,[status(thm)],[f81]) ).
thf(f81,plain,
( ( $false
= ( !! @ ( ( a > $o ) > $o )
@ ^ [Y0: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( Y0 @ Y1 )
=> ( ( ( ^ [Y2: a] : $true )
= Y1 )
| ( ( ^ [Y2: a] : $false )
= Y1 ) ) ) )
& ( ( ^ [Y1: a] :
( ?? @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y2 @ Y1 )
& ( Y0 @ Y2 ) ) ) )
= sK4 ) )
=> $false ) ) )
| ~ spl0_6 ),
inference(backward_demodulation,[status(thm)],[f74,f80]) ).
thf(f282,plain,
( ( $true
= ( sK7
@ ^ [Y0: a] : $true ) )
| ~ spl0_9 ),
inference(avatar_component_clause,[status(thm)],[f281]) ).
thf(f281,definition,
( spl0_9
<=> ( $true
= ( sK7
@ ^ [Y0: a] : $true ) ) ),
introduced(definition,[new_symbols(naming,[spl0_9])],[avatar_definition]) ).
thf(f138,plain,
( ( $false
= ( sK4 @ sK6 ) )
| ~ spl0_6 ),
inference(trivial_inequality_removal,[status(thm)],[f135]) ).
thf(f135,plain,
( ( $true != $true )
| ( $false
= ( sK4 @ sK6 ) )
| ~ spl0_6 ),
inference(superposition,[status(thm)],[f89,f127]) ).
thf(f127,plain,
( ! [X0: a] :
( ( ( sK4 @ X0 )
= $true )
| ( ( sK4 @ X0 )
= $false ) )
| ~ spl0_6 ),
inference(superposition,[status(thm)],[f114,f109]) ).
thf(f89,plain,
( ( $true
!= ( sK4 @ sK6 ) )
| ~ spl0_6 ),
inference(beta_eta_normalization,[status(thm)],[f88]) ).
thf(f88,plain,
( ( ( ^ [Y0: a] : $true
@ sK6 )
!= ( sK4 @ sK6 ) )
| ~ spl0_6 ),
inference(negative_extensionality,[status(thm)],[f87]) ).
thf(f87,plain,
( ( sK4
!= ( ^ [Y0: a] : $true ) )
| ~ spl0_6 ),
inference(equality_proxy_clausification,[status(thm)],[f86]) ).
thf(f86,plain,
( ( ( sK4
= ( ^ [Y0: a] : $true ) )
= $false )
| ~ spl0_6 ),
inference(boolean_simplification,[status(thm)],[f85]) ).
thf(f85,plain,
( ( ( $false
| ( sK4
= ( ^ [Y0: a] : $true ) ) )
= $false )
| ~ spl0_6 ),
inference(backward_demodulation,[status(thm)],[f80,f84]) ).
thf(f304,plain,
( spl0_10
| ~ spl0_6
| ~ spl0_8 ),
inference(avatar_split_clause,[status(thm)],[f293,f277,f54,f298]) ).
thf(f277,definition,
( spl0_8
<=> ! [X0: a] :
( ( ( sK4 @ X0 )
= $false )
| ( ( sK9 @ X0 )
= ( ^ [Y0: a] : $false ) ) ) ),
introduced(definition,[new_symbols(naming,[spl0_8])],[avatar_definition]) ).
thf(f293,plain,
( ! [X0: a] :
( ( sK4 @ X0 )
= $false )
| ~ spl0_6
| ~ spl0_8 ),
inference(trivial_inequality_removal,[status(thm)],[f292]) ).
thf(f292,plain,
( ! [X0: a] :
( ( ( sK4 @ X0 )
= $false )
| ( $true = $false ) )
| ~ spl0_6
| ~ spl0_8 ),
inference(boolean_simplification,[status(thm)],[f291]) ).
thf(f291,plain,
( ! [X0: a] :
( ( ( sK4 @ X0 )
= $false )
| ( ( $false
& ( sK7
@ ^ [Y0: a] : $false ) )
= $true ) )
| ~ spl0_6
| ~ spl0_8 ),
inference(beta_eta_normalization,[status(thm)],[f290]) ).
thf(f290,plain,
( ! [X0: a] :
( ( ( ( ^ [Y0: a] : $false
@ X0 )
& ( sK7
@ ^ [Y0: a] : $false ) )
= $true )
| ( ( sK4 @ X0 )
= $false ) )
| ~ spl0_6
| ~ spl0_8 ),
inference(duplicate_literal_removal,[status(thm)],[f287]) ).
thf(f287,plain,
( ! [X0: a] :
( ( ( sK4 @ X0 )
= $false )
| ( ( ( ^ [Y0: a] : $false
@ X0 )
& ( sK7
@ ^ [Y0: a] : $false ) )
= $true )
| ( ( sK4 @ X0 )
= $false ) )
| ~ spl0_6
| ~ spl0_8 ),
inference(superposition,[status(thm)],[f181,f278]) ).
thf(f278,plain,
( ! [X0: a] :
( ( ( sK9 @ X0 )
= ( ^ [Y0: a] : $false ) )
| ( ( sK4 @ X0 )
= $false ) )
| ~ spl0_8 ),
inference(avatar_component_clause,[status(thm)],[f277]) ).
thf(f181,plain,
( ! [X1: a] :
( ( $true
= ( ( sK9 @ X1 @ X1 )
& ( sK7 @ ( sK9 @ X1 ) ) ) )
| ( ( sK4 @ X1 )
= $false ) )
| ~ spl0_6 ),
inference(beta_eta_normalization,[status(thm)],[f176]) ).
thf(f176,plain,
( ! [X1: a] :
( ( $true
= ( ^ [Y0: a > $o] :
( ( Y0 @ X1 )
& ( sK7 @ Y0 ) )
@ ( sK9 @ X1 ) ) )
| ( ( sK4 @ X1 )
= $false ) )
| ~ spl0_6 ),
inference(sigma_clausification,[status(thm)],[f115]) ).
thf(f115,plain,
( ! [X1: a] :
( ( $true
= ( ?? @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0 @ X1 )
& ( sK7 @ Y0 ) ) ) )
| ( ( sK4 @ X1 )
= $false ) )
| ~ spl0_6 ),
inference(binary_proxy_clausification,[status(thm)],[f109]) ).
thf(f284,plain,
( spl0_8
| spl0_9
| ~ spl0_6 ),
inference(avatar_split_clause,[status(thm)],[f268,f54,f281,f277]) ).
thf(f268,plain,
( ! [X0: a] :
( ( ( sK4 @ X0 )
= $false )
| ( ( sK9 @ X0 )
= ( ^ [Y0: a] : $false ) )
| ( $true
= ( sK7
@ ^ [Y0: a] : $true ) ) )
| ~ spl0_6 ),
inference(duplicate_literal_removal,[status(thm)],[f266]) ).
thf(f266,plain,
( ! [X0: a] :
( ( $true
= ( sK7
@ ^ [Y0: a] : $true ) )
| ( ( sK4 @ X0 )
= $false )
| ( ( sK4 @ X0 )
= $false )
| ( ( sK9 @ X0 )
= ( ^ [Y0: a] : $false ) ) )
| ~ spl0_6 ),
inference(superposition,[status(thm)],[f193,f201]) ).
thf(f201,plain,
( ! [X0: a] :
( ( ( ^ [Y0: a] : $true )
= ( sK9 @ X0 ) )
| ( ( sK9 @ X0 )
= ( ^ [Y0: a] : $false ) )
| ( ( sK4 @ X0 )
= $false ) )
| ~ spl0_6 ),
inference(trivial_inequality_removal,[status(thm)],[f200]) ).
thf(f200,plain,
( ! [X0: a] :
( ( ( sK9 @ X0 )
= ( ^ [Y0: a] : $false ) )
| ( ( sK4 @ X0 )
= $false )
| ( ( ^ [Y0: a] : $true )
= ( sK9 @ X0 ) )
| ( $true = $false ) )
| ~ spl0_6 ),
inference(boolean_simplification,[status(thm)],[f195]) ).
thf(f195,plain,
( ! [X0: a] :
( ( ( sK9 @ X0 )
= ( ^ [Y0: a] : $false ) )
| ( ( ^ [Y0: a] : $true )
= ( sK9 @ X0 ) )
| ( ( sK4 @ X0 )
= $false )
| ( $true
= ( ( sK9 @ X0 @ X0 )
& $false ) ) )
| ~ spl0_6 ),
inference(superposition,[status(thm)],[f181,f158]) ).
thf(f158,plain,
( ! [X1: a > $o] :
( ( $false
= ( sK7 @ X1 ) )
| ( ( ^ [Y0: a] : $true )
= X1 )
| ( ( ^ [Y0: a] : $false )
= X1 ) )
| ~ spl0_6 ),
inference(equality_proxy_clausification,[status(thm)],[f143]) ).
thf(f143,plain,
( ! [X1: a > $o] :
( ( $true
= ( ( ^ [Y0: a] : $false )
= X1 ) )
| ( ( ^ [Y0: a] : $true )
= X1 )
| ( $false
= ( sK7 @ X1 ) ) )
| ~ spl0_6 ),
inference(equality_proxy_clausification,[status(thm)],[f130]) ).
thf(f130,plain,
( ! [X1: a > $o] :
( ( $true
= ( ( ^ [Y0: a] : $true )
= X1 ) )
| ( $true
= ( ( ^ [Y0: a] : $false )
= X1 ) )
| ( $false
= ( sK7 @ X1 ) ) )
| ~ spl0_6 ),
inference(binary_proxy_clausification,[status(thm)],[f107]) ).
thf(f107,plain,
( ! [X1: a > $o] :
( ( ( ( ( ^ [Y0: a] : $true )
= X1 )
| ( ( ^ [Y0: a] : $false )
= X1 ) )
= $true )
| ( $false
= ( sK7 @ X1 ) ) )
| ~ spl0_6 ),
inference(binary_proxy_clausification,[status(thm)],[f103]) ).
thf(f103,plain,
( ! [X1: a > $o] :
( ( ( sK7 @ X1 )
=> ( ( ( ^ [Y0: a] : $true )
= X1 )
| ( ( ^ [Y0: a] : $false )
= X1 ) ) )
= $true )
| ~ spl0_6 ),
inference(beta_eta_normalization,[status(thm)],[f102]) ).
thf(f102,plain,
( ! [X1: a > $o] :
( $true
= ( ^ [Y0: a > $o] :
( ( sK7 @ Y0 )
=> ( ( ( ^ [Y1: a] : $true )
= Y0 )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) )
@ X1 ) )
| ~ spl0_6 ),
inference(pi_clausification,[status(thm)],[f101]) ).
thf(f101,plain,
( ( $true
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK7 @ Y0 )
=> ( ( ( ^ [Y1: a] : $true )
= Y0 )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) ) )
| ~ spl0_6 ),
inference(boolean_simplification,[status(thm)],[f100]) ).
thf(f100,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( sK7 @ Y0 )
=> ( ( ( ^ [Y1: a] : $true )
= Y0 )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& $true )
= $true )
| ~ spl0_6 ),
inference(backward_demodulation,[status(thm)],[f93,f98]) ).
thf(f193,plain,
( ! [X1: a] :
( ( $true
= ( sK7 @ ( sK9 @ X1 ) ) )
| ( ( sK4 @ X1 )
= $false ) )
| ~ spl0_6 ),
inference(binary_proxy_clausification,[status(thm)],[f181]) ).
thf(f69,plain,
~ spl0_5,
inference(avatar_contradiction_clause,[status(thm)],[f68]) ).
thf(f68,plain,
( $false
| ~ spl0_5 ),
inference(trivial_inequality_removal,[status(thm)],[f67]) ).
thf(f67,plain,
( ( $true = $false )
| ~ spl0_5 ),
inference(boolean_simplification,[status(thm)],[f66]) ).
thf(f66,plain,
( ( ( $true
| ( ( ^ [Y0: a] : $false )
= sK3 ) )
= $false )
| ~ spl0_5 ),
inference(backward_demodulation,[status(thm)],[f61,f62]) ).
thf(f62,plain,
( ( ( sK3
= ( ^ [Y0: a] : $true ) )
= $true )
| ~ spl0_5 ),
inference(binary_proxy_clausification,[status(thm)],[f60]) ).
thf(f60,plain,
( ( $false
= ( ( sK3
= ( ^ [Y0: a] : $true ) )
=> ( ( sK3
= ( ^ [Y0: a] : $true ) )
| ( ( ^ [Y0: a] : $false )
= sK3 ) ) ) )
| ~ spl0_5 ),
inference(beta_eta_normalization,[status(thm)],[f59]) ).
thf(f59,plain,
( ( $false
= ( ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $true ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) )
@ sK3 ) )
| ~ spl0_5 ),
inference(sigma_clausification,[status(thm)],[f52]) ).
thf(f52,plain,
( ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $true ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) ) )
| ~ spl0_5 ),
inference(avatar_component_clause,[status(thm)],[f51]) ).
thf(f51,definition,
( spl0_5
<=> ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $true ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) ) ) ),
introduced(definition,[new_symbols(naming,[spl0_5])],[avatar_definition]) ).
thf(f61,plain,
( ( $false
= ( ( sK3
= ( ^ [Y0: a] : $true ) )
| ( ( ^ [Y0: a] : $false )
= sK3 ) ) )
| ~ spl0_5 ),
inference(binary_proxy_clausification,[status(thm)],[f60]) ).
thf(f56,plain,
( spl0_5
| spl0_6
| ~ spl0_4 ),
inference(avatar_split_clause,[status(thm)],[f49,f26,f54,f51]) ).
thf(f26,definition,
( spl0_4
<=> ( $false
= ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( ( ( ^ [Y3: a] : $true )
= Y2 )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) ) )
& ( ( ^ [Y2: a] :
( ?? @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y3 @ Y2 )
& ( Y1 @ Y3 ) ) ) )
= Y0 ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : $true ) ) ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $true ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) ) ) ) ),
introduced(definition,[new_symbols(naming,[spl0_4])],[avatar_definition]) ).
thf(f49,plain,
( ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $true ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) ) )
| ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( ( ( ^ [Y3: a] : $true )
= Y2 )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) ) )
& ( ( ^ [Y2: a] :
( ?? @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y3 @ Y2 )
& ( Y1 @ Y3 ) ) ) )
= Y0 ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : $true ) ) ) ) ) ) )
| ~ spl0_4 ),
inference(binary_proxy_clausification,[status(thm)],[f27]) ).
thf(f27,plain,
( ( $false
= ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( ( ( ^ [Y3: a] : $true )
= Y2 )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) ) )
& ( ( ^ [Y2: a] :
( ?? @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y3 @ Y2 )
& ( Y1 @ Y3 ) ) ) )
= Y0 ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : $true ) ) ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $true ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) ) ) )
| ~ spl0_4 ),
inference(avatar_component_clause,[status(thm)],[f26]) ).
thf(f45,plain,
~ spl0_3,
inference(avatar_contradiction_clause,[status(thm)],[f44]) ).
thf(f44,plain,
( $false
| ~ spl0_3 ),
inference(trivial_inequality_removal,[status(thm)],[f43]) ).
thf(f43,plain,
( ( $true = $false )
| ~ spl0_3 ),
inference(boolean_simplification,[status(thm)],[f42]) ).
thf(f42,plain,
( ( $false
= ( ( sK2
= ( ^ [Y0: a] : $true ) )
| $true ) )
| ~ spl0_3 ),
inference(boolean_simplification,[status(thm)],[f41]) ).
thf(f41,plain,
( ( $false
= ( ( sK2
= ( ^ [Y0: a] : $true ) )
| ( sK2 = sK2 ) ) )
| ~ spl0_3 ),
inference(backward_demodulation,[status(thm)],[f33,f39]) ).
thf(f39,plain,
( ( ( ^ [Y0: a] : $false )
= sK2 )
| ~ spl0_3 ),
inference(equality_proxy_clausification,[status(thm)],[f34]) ).
thf(f34,plain,
( ( $true
= ( sK2
= ( ^ [Y0: a] : $false ) ) )
| ~ spl0_3 ),
inference(binary_proxy_clausification,[status(thm)],[f32]) ).
thf(f32,plain,
( ( ( ( sK2
= ( ^ [Y0: a] : $false ) )
=> ( ( sK2
= ( ^ [Y0: a] : $true ) )
| ( ( ^ [Y0: a] : $false )
= sK2 ) ) )
= $false )
| ~ spl0_3 ),
inference(beta_eta_normalization,[status(thm)],[f31]) ).
thf(f31,plain,
( ( ( ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $false ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) )
@ sK2 )
= $false )
| ~ spl0_3 ),
inference(sigma_clausification,[status(thm)],[f24]) ).
thf(f24,plain,
( ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $false ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) ) )
| ~ spl0_3 ),
inference(avatar_component_clause,[status(thm)],[f23]) ).
thf(f23,definition,
( spl0_3
<=> ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $false ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) ) ) ),
introduced(definition,[new_symbols(naming,[spl0_3])],[avatar_definition]) ).
thf(f33,plain,
( ( ( ( sK2
= ( ^ [Y0: a] : $true ) )
| ( ( ^ [Y0: a] : $false )
= sK2 ) )
= $false )
| ~ spl0_3 ),
inference(binary_proxy_clausification,[status(thm)],[f32]) ).
thf(f28,plain,
( spl0_3
| spl0_4
| ~ spl0_2 ),
inference(avatar_split_clause,[status(thm)],[f21,f16,f26,f23]) ).
thf(f16,definition,
( spl0_2
<=> ( $false
= ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( ( ( ^ [Y3: a] : $true )
= Y2 )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) ) )
& ( ( ^ [Y2: a] :
( ?? @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y3 @ Y2 )
& ( Y1 @ Y3 ) ) ) )
= Y0 ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : $true ) ) ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $true ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $false ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) ) ) ) ),
introduced(definition,[new_symbols(naming,[spl0_2])],[avatar_definition]) ).
thf(f21,plain,
( ( $false
= ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( ( ( ^ [Y3: a] : $true )
= Y2 )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) ) )
& ( ( ^ [Y2: a] :
( ?? @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y3 @ Y2 )
& ( Y1 @ Y3 ) ) ) )
= Y0 ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : $true ) ) ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $true ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) ) ) )
| ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $false ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) ) )
| ~ spl0_2 ),
inference(binary_proxy_clausification,[status(thm)],[f17]) ).
thf(f17,plain,
( ( $false
= ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( ( ( ^ [Y3: a] : $true )
= Y2 )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) ) )
& ( ( ^ [Y2: a] :
( ?? @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y3 @ Y2 )
& ( Y1 @ Y3 ) ) ) )
= Y0 ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : $true ) ) ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $true ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $false ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) ) ) )
| ~ spl0_2 ),
inference(avatar_component_clause,[status(thm)],[f16]) ).
thf(f18,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[status(thm)],[f11,f16,f13]) ).
thf(f11,plain,
( ( $false
= ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( ( ( ^ [Y3: a] : $true )
= Y2 )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) ) )
& ( ( ^ [Y2: a] :
( ?? @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y3 @ Y2 )
& ( Y1 @ Y3 ) ) ) )
= Y0 ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : $true ) ) ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $true ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $false ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) ) ) )
| ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( ( ( ^ [Y3: a] : $true )
= Y0 )
| ( Y0
= ( ^ [Y3: a] : $false ) ) )
& ( ( ^ [Y3: a] :
( ( Y2 @ Y3 )
& ( Y0 @ Y3 ) ) )
= Y1 )
& ( ( Y2
= ( ^ [Y3: a] : $true ) )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) )
=> ( ( Y1
= ( ^ [Y3: a] : $false ) )
| ( Y1
= ( ^ [Y3: a] : $true ) ) ) ) ) ) )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f8]) ).
thf(f8,plain,
( $false
= ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( ( ( ^ [Y3: a] : $true )
= Y2 )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) ) )
& ( ( ^ [Y2: a] :
( ?? @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y3 @ Y2 )
& ( Y1 @ Y3 ) ) ) )
= Y0 ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : $true ) ) ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $true ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $false ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( ( ( ^ [Y3: a] : $true )
= Y0 )
| ( Y0
= ( ^ [Y3: a] : $false ) ) )
& ( ( ^ [Y3: a] :
( ( Y2 @ Y3 )
& ( Y0 @ Y3 ) ) )
= Y1 )
& ( ( Y2
= ( ^ [Y3: a] : $true ) )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) )
=> ( ( Y1
= ( ^ [Y3: a] : $false ) )
| ( Y1
= ( ^ [Y3: a] : $true ) ) ) ) ) ) ) ) ),
inference(not_proxy_clausification,[status(thm)],[f7]) ).
thf(f7,plain,
( ( ~ ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( ( ( ^ [Y3: a] : $true )
= Y2 )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) ) )
& ( ( ^ [Y2: a] :
( ?? @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y3 @ Y2 )
& ( Y1 @ Y3 ) ) ) )
= Y0 ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : $true ) ) ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $true ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $false ) )
=> ( ( Y0
= ( ^ [Y1: a] : $true ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( ( ( ^ [Y3: a] : $true )
= Y0 )
| ( Y0
= ( ^ [Y3: a] : $false ) ) )
& ( ( ^ [Y3: a] :
( ( Y2 @ Y3 )
& ( Y0 @ Y3 ) ) )
= Y1 )
& ( ( Y2
= ( ^ [Y3: a] : $true ) )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) )
=> ( ( Y1
= ( ^ [Y3: a] : $false ) )
| ( Y1
= ( ^ [Y3: a] : $true ) ) ) ) ) ) ) ) )
= $true ),
inference(boolean_simplification,[status(thm)],[f6]) ).
thf(f6,plain,
( ( ~ ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( ( ( ^ [Y3: a] : ~ $false )
= Y2 )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) ) )
& ( ( ^ [Y2: a] :
( ?? @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y3 @ Y2 )
& ( Y1 @ Y3 ) ) ) )
= Y0 ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : ~ $false ) ) ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : ~ $false ) )
=> ( ( Y0
= ( ^ [Y1: a] : ~ $false ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $false ) )
=> ( ( Y0
= ( ^ [Y1: a] : ~ $false ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( ( ( ^ [Y3: a] : ~ $false )
= Y0 )
| ( Y0
= ( ^ [Y3: a] : $false ) ) )
& ( ( ^ [Y3: a] :
( ( Y2 @ Y3 )
& ( Y0 @ Y3 ) ) )
= Y1 )
& ( ( Y2
= ( ^ [Y3: a] : ~ $false ) )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) )
=> ( ( Y1
= ( ^ [Y3: a] : $false ) )
| ( Y1
= ( ^ [Y3: a] : ~ $false ) ) ) ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f5]) ).
thf(f5,plain,
( ( ~ ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( ( a > $o ) > $o )
@ ^ [Y1: ( a > $o ) > $o] :
( ( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( Y1 @ Y2 )
=> ( ( ( ^ [Y3: a] : ~ $false )
= Y2 )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) ) )
& ( ( ^ [Y2: a] :
( ?? @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( Y3 @ Y2 )
& ( Y1 @ Y3 ) ) ) )
= Y0 ) )
=> ( ( Y0
= ( ^ [Y2: a] : $false ) )
| ( Y0
= ( ^ [Y2: a] : ~ $false ) ) ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : ~ $false ) )
=> ( ( Y0
= ( ^ [Y1: a] : ~ $false ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( Y0
= ( ^ [Y1: a] : $false ) )
=> ( ( Y0
= ( ^ [Y1: a] : ~ $false ) )
| ( ( ^ [Y1: a] : $false )
= Y0 ) ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( ( ( ^ [Y3: a] : ~ $false )
= Y0 )
| ( Y0
= ( ^ [Y3: a] : $false ) ) )
& ( ( ^ [Y3: a] :
( ( Y2 @ Y3 )
& ( Y0 @ Y3 ) ) )
= Y1 )
& ( ( Y2
= ( ^ [Y3: a] : ~ $false ) )
| ( ( ^ [Y3: a] : $false )
= Y2 ) ) )
=> ( ( Y1
= ( ^ [Y3: a] : $false ) )
| ( Y1
= ( ^ [Y3: a] : ~ $false ) ) ) ) ) ) ) ) )
= $true ),
inference(fool_elimination,[status(thm)],[f4]) ).
thf(f4,plain,
~ ( ! [X0: a > $o,X1: a > $o,X2: a > $o] :
( ( ( ( ( ^ [X3: a] : $false )
= X0 )
| ( X0
= ( ^ [X4: a] : ~ $false ) ) )
& ( ( ^ [X5: a] :
( ( X2 @ X5 )
& ( X0 @ X5 ) ) )
= X1 )
& ( ( X2
= ( ^ [X6: a] : $false ) )
| ( ( ^ [X7: a] : ~ $false )
= X2 ) ) )
=> ( ( X1
= ( ^ [X8: a] : ~ $false ) )
| ( X1
= ( ^ [X9: a] : $false ) ) ) )
& ! [X10: a > $o] :
( ( X10
= ( ^ [X11: a] : $false ) )
=> ( ( ( ^ [X12: a] : $false )
= X10 )
| ( X10
= ( ^ [X13: a] : ~ $false ) ) ) )
& ! [X14: a > $o] :
( ( X14
= ( ^ [X15: a] : ~ $false ) )
=> ( ( ( ^ [X16: a] : $false )
= X14 )
| ( X14
= ( ^ [X17: a] : ~ $false ) ) ) )
& ! [X18: ( a > $o ) > $o,X19: a > $o] :
( ( ( ( ^ [X20: a] :
? [X21: a > $o] :
( ( X18 @ X21 )
& ( X21 @ X20 ) ) )
= X19 )
& ! [X22: a > $o] :
( ( X18 @ X22 )
=> ( ( ( ^ [X23: a] : $false )
= X22 )
| ( ( ^ [X24: a] : ~ $false )
= X22 ) ) ) )
=> ( ( X19
= ( ^ [X25: a] : ~ $false ) )
| ( X19
= ( ^ [X26: a] : $false ) ) ) ) ),
inference(rectify,[status(thm)],[f2]) ).
thf(f2,negated_conjecture,
~ ( ! [X6: a > $o,X4: a > $o,X5: a > $o] :
( ( ( ( ( ^ [X2: a] : $false )
= X6 )
| ( X6
= ( ^ [X2: a] : ~ $false ) ) )
& ( ( ^ [X1: a] :
( ( X5 @ X1 )
& ( X6 @ X1 ) ) )
= X4 )
& ( ( X5
= ( ^ [X2: a] : $false ) )
| ( ( ^ [X2: a] : ~ $false )
= X5 ) ) )
=> ( ( X4
= ( ^ [X2: a] : ~ $false ) )
| ( X4
= ( ^ [X2: a] : $false ) ) ) )
& ! [X0: a > $o] :
( ( X0
= ( ^ [X1: a] : $false ) )
=> ( ( ( ^ [X2: a] : $false )
= X0 )
| ( X0
= ( ^ [X2: a] : ~ $false ) ) ) )
& ! [X0: a > $o] :
( ( X0
= ( ^ [X1: a] : ~ $false ) )
=> ( ( ( ^ [X2: a] : $false )
= X0 )
| ( X0
= ( ^ [X2: a] : ~ $false ) ) ) )
& ! [X3: ( a > $o ) > $o,X0: a > $o] :
( ( ( ( ^ [X1: a] :
? [X4: a > $o] :
( ( X3 @ X4 )
& ( X4 @ X1 ) ) )
= X0 )
& ! [X1: a > $o] :
( ( X3 @ X1 )
=> ( ( ( ^ [X2: a] : $false )
= X1 )
| ( ( ^ [X2: a] : ~ $false )
= X1 ) ) ) )
=> ( ( X0
= ( ^ [X2: a] : ~ $false ) )
| ( X0
= ( ^ [X2: a] : $false ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
thf(f1,conjecture,
( ! [X6: a > $o,X4: a > $o,X5: a > $o] :
( ( ( ( ( ^ [X2: a] : $false )
= X6 )
| ( X6
= ( ^ [X2: a] : ~ $false ) ) )
& ( ( ^ [X1: a] :
( ( X5 @ X1 )
& ( X6 @ X1 ) ) )
= X4 )
& ( ( X5
= ( ^ [X2: a] : $false ) )
| ( ( ^ [X2: a] : ~ $false )
= X5 ) ) )
=> ( ( X4
= ( ^ [X2: a] : ~ $false ) )
| ( X4
= ( ^ [X2: a] : $false ) ) ) )
& ! [X0: a > $o] :
( ( X0
= ( ^ [X1: a] : $false ) )
=> ( ( ( ^ [X2: a] : $false )
= X0 )
| ( X0
= ( ^ [X2: a] : ~ $false ) ) ) )
& ! [X0: a > $o] :
( ( X0
= ( ^ [X1: a] : ~ $false ) )
=> ( ( ( ^ [X2: a] : $false )
= X0 )
| ( X0
= ( ^ [X2: a] : ~ $false ) ) ) )
& ! [X3: ( a > $o ) > $o,X0: a > $o] :
( ( ( ( ^ [X1: a] :
? [X4: a > $o] :
( ( X3 @ X4 )
& ( X4 @ X1 ) ) )
= X0 )
& ! [X1: a > $o] :
( ( X3 @ X1 )
=> ( ( ( ^ [X2: a] : $false )
= X1 )
| ( ( ^ [X2: a] : ~ $false )
= X1 ) ) ) )
=> ( ( X0
= ( ^ [X2: a] : ~ $false ) )
| ( X0
= ( ^ [X2: a] : $false ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.YfPnjdhobS/DTF2THF_19752.p',cINDISCRETE_TOPOLOGY_pme) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : SEV261^5 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.11 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.12/0.31 % Computer : n020.cluster.edu
% 0.12/0.31 % Model : x86_64 x86_64
% 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.31 % Memory : 8042.1875MB
% 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.31 % CPULimit : 300
% 0.12/0.31 % WCLimit : 300
% 0.12/0.31 % DateTime : Tue Feb 24 12:43:42 EST 2026
% 0.12/0.31 % CPUTime :
% 0.12/0.31 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.16/0.41 ---- Original DTF file ---
% 0.16/0.41 thf(spec,logic,$$dhol).
% 0.16/0.41 %------------------------------------------------------------------------------
% 0.16/0.41 % File : SEV261^5 : TPTP v9.2.1. Released v4.0.0.
% 0.16/0.41 % Domain : Set Theory (Sets of sets)
% 0.16/0.41 % Problem : TPS problem INDISCRETE-TOPOLOGY
% 0.16/0.41 % Version : Especial.
% 0.16/0.41 % English :
% 0.16/0.41
% 0.16/0.41 % Refs : [Bro09] Brown (2009), Email to Geoff Sutcliffe
% 0.16/0.41 % Source : [Bro09]
% 0.16/0.41 % Names : tps_0539 [Bro09]
% 0.16/0.41 % : INDISCRETE-TOPOLOGY [TPS]
% 0.16/0.41
% 0.16/0.41 % Status : Theorem
% 0.16/0.41 % Rating : 0.22 v9.1.0, 0.25 v9.0.0, 0.30 v8.2.0, 0.38 v8.1.0, 0.27 v7.5.0, 0.29 v7.4.0, 0.33 v7.2.0, 0.25 v7.1.0, 0.38 v7.0.0, 0.29 v6.4.0, 0.33 v6.3.0, 0.40 v6.2.0, 0.43 v6.1.0, 0.29 v5.5.0, 0.17 v5.4.0, 0.20 v5.1.0, 0.40 v5.0.0, 0.20 v4.1.0, 0.00 v4.0.1, 0.67 v4.0.0
% 0.16/0.41 % Syntax : Number of formulae : 2 ( 0 unt; 1 typ; 0 def)
% 0.16/0.41 % Number of atoms : 34 ( 18 equ; 0 cnn)
% 0.16/0.41 % Maximal formula atoms : 18 ( 34 avg)
% 0.16/0.41 % Number of connectives : 33 ( 8 ~; 7 |; 8 &; 5 @)
% 0.16/0.41 % ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% 0.16/0.41 % Maximal formula depth : 11 ( 11 avg)
% 0.16/0.41 % Number of types : 2 ( 1 usr)
% 0.16/0.41 % Number of type conns : 10 ( 10 >; 0 *; 0 +; 0 <<)
% 0.16/0.41 % Number of symbols : 2 ( 0 usr; 1 con; 0-2 aty)
% 0.16/0.41 % Number of variables : 27 ( 18 ^; 8 !; 1 ?; 27 :)
% 0.16/0.41 % SPC : TH0_THM_EQU_NAR
% 0.16/0.41
% 0.16/0.41 % Comments : This problem is from the TPS library. Copyright (c) 2009 The TPS
% 0.16/0.41 % project in the Department of Mathematical Sciences at Carnegie
% 0.16/0.41 % Mellon University. Distributed under the Creative Commons copyleft
% 0.16/0.41 % license: http://creativecommons.org/licenses/by-sa/3.0/
% 0.16/0.41 % : Polymorphic definitions expanded.
% 0.16/0.41 %------------------------------------------------------------------------------
% 0.16/0.41 thf(a_type,type,
% 0.16/0.41 a: $tType ).
% 0.16/0.41
% 0.16/0.41 thf(cINDISCRETE_TOPOLOGY_pme,conjecture,
% 0.16/0.41 ( ! [R: a > $o] :
% 0.16/0.41 ( ( R
% 0.16/0.41 = ( ^ [Xx: a] : $false ) )
% 0.16/0.41 => ( ( R
% 0.16/0.41 = ( ^ [Xy: a] : $false ) )
% 0.16/0.41 | ( R
% 0.16/0.41 = ( ^ [Xy: a] : ~ $false ) ) ) )
% 0.16/0.41 & ! [R: a > $o] :
% 0.16/0.41 ( ( R
% 0.16/0.41 = ( ^ [Xx: a] : ~ $false ) )
% 0.16/0.41 => ( ( R
% 0.16/0.41 = ( ^ [Xy: a] : $false ) )
% 0.16/0.41 | ( R
% 0.16/0.41 = ( ^ [Xy: a] : ~ $false ) ) ) )
% 0.16/0.41 & ! [K: ( a > $o ) > $o,R: a > $o] :
% 0.16/0.41 ( ( ! [Xx: a > $o] :
% 0.16/0.41 ( ( K @ Xx )
% 0.16/0.41 => ( ( Xx
% 0.16/0.41 = ( ^ [Xy: a] : $false ) )
% 0.16/0.41 | ( Xx
% 0.16/0.41 = ( ^ [Xy: a] : ~ $false ) ) ) )
% 0.16/0.41 & ( R
% 0.16/0.41 = ( ^ [Xx: a] :
% 0.16/0.41 ? [S: a > $o] :
% 0.16/0.41 ( ( K @ S )
% 0.16/0.41 & ( S @ Xx ) ) ) ) )
% 0.16/0.41 => ( ( R
% 0.16/0.41 = ( ^ [Xy: a] : $false ) )
% 0.16/0.41 | ( R
% 0.16/0.41 = ( ^ [Xy: a] : ~ $false ) ) ) )
% 0.16/0.41 & ! [Y: a > $o,Z: a > $o,S: a > $o] :
% 0.16/0.41 ( ( ( ( Y
% 0.16/0.41 = ( ^ [Xy: a] : $false ) )
% 0.16/0.41 | ( Y
% 0.16/0.41 = ( ^ [Xy: a] : ~ $false ) ) )
% 0.16/0.41 & ( ( Z
% 0.16/0.41 = ( ^ [Xy: a] : $false ) )
% 0.16/0.41 | ( Z
% 0.16/0.41 = ( ^ [Xy: a] : ~ $false ) ) )
% 0.16/0.41 & ( S
% 0.16/0.41 = ( ^ [Xx: a] :
% 0.16/0.41 ( ( Y @ Xx )
% 0.16/0.41 & ( Z @ Xx ) ) ) ) )
% 0.16/0.41 => ( ( S
% 0.16/0.41 = ( ^ [Xy: a] : $false ) )
% 0.16/0.41 | ( S
% 0.16/0.41 = ( ^ [Xy: a] : ~ $false ) ) ) ) ) ).
% 0.16/0.41
% 0.16/0.41 %------------------------------------------------------------------------------
% 0.16/0.41 ------------------------
% 1.56/1.39 ---- Embedded in THF ---
% 1.56/1.39 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.56/1.39 %%% Generated on Tue Feb 24 12:43:43 EST 2026
% 1.56/1.39 %%% using '$$dhol' embedding, version 1.3.0.
% 1.56/1.39 %%% Logic specification used:
% 1.56/1.39 %%% thf(spec, logic, $$dhol).
% 1.56/1.39
% 1.56/1.39 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.YfPnjdhobS/DTF2DTF19752.p
% See solution above
% 1.56/1.39 ------------------------
% 1.75/1.40 ---- Cleaned THF ---
% 1.75/1.40 thf(a_type,type,
% 1.75/1.40 a: $tType ).
% 1.75/1.40
% 1.75/1.40 thf(cINDISCRETE_TOPOLOGY_pme,conjecture,
% 1.75/1.40 ( ! [R: a > $o] :
% 1.75/1.40 ( ( R
% 1.75/1.40 = ( ^ [Xx: a] : $false ) )
% 1.75/1.40 => ( ( R
% 1.75/1.40 = ( ^ [Xy: a] : $false ) )
% 1.75/1.40 | ( R
% 1.75/1.40 = ( ^ [Xy: a] : ~ $false ) ) ) )
% 1.75/1.40 & ! [R: a > $o] :
% 1.75/1.40 ( ( R
% 1.75/1.40 = ( ^ [Xx: a] : ~ $false ) )
% 1.75/1.40 => ( ( R
% 1.75/1.40 = ( ^ [Xy: a] : $false ) )
% 1.75/1.40 | ( R
% 1.75/1.40 = ( ^ [Xy: a] : ~ $false ) ) ) )
% 1.75/1.40 & ! [K: ( a > $o ) > $o,R: a > $o] :
% 1.75/1.40 ( ( ! [Xx: a > $o] :
% 1.75/1.40 ( ( K @ Xx )
% 1.75/1.40 => ( ( Xx
% 1.75/1.40 = ( ^ [Xy: a] : $false ) )
% 1.75/1.40 | ( Xx
% 1.75/1.40 = ( ^ [Xy: a] : ~ $false ) ) ) )
% 1.75/1.40 & ( R
% 1.75/1.40 = ( ^ [Xx: a] :
% 1.75/1.40 ? [S: a > $o] :
% 1.75/1.40 ( ( K @ S )
% 1.75/1.40 & ( S @ Xx ) ) ) ) )
% 1.75/1.40 => ( ( R
% 1.75/1.40 = ( ^ [Xy: a] : $false ) )
% 1.75/1.40 | ( R
% 1.75/1.40 = ( ^ [Xy: a] : ~ $false ) ) ) )
% 1.75/1.40 & ! [Y: a > $o,Z: a > $o,S: a > $o] :
% 1.75/1.40 ( ( ( ( Y
% 1.75/1.40 = ( ^ [Xy: a] : $false ) )
% 1.75/1.40 | ( Y
% 1.75/1.40 = ( ^ [Xy: a] : ~ $false ) ) )
% 1.75/1.40 & ( ( Z
% 1.75/1.40 = ( ^ [Xy: a] : $false ) )
% 1.75/1.40 | ( Z
% 1.75/1.40 = ( ^ [Xy: a] : ~ $false ) ) )
% 1.75/1.40 & ( S
% 1.75/1.40 = ( ^ [Xx: a] :
% 1.75/1.40 ( ( Y @ Xx )
% 1.75/1.40 & ( Z @ Xx ) ) ) ) )
% 1.75/1.40 => ( ( S
% 1.75/1.40 = ( ^ [Xy: a] : $false ) )
% 1.75/1.40 | ( S
% 1.75/1.40 = ( ^ [Xy: a] : ~ $false ) ) ) ) ) ).
% 1.75/1.40 ------------------------
% 1.75/1.42 % (19853)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_19752 for (2999ds/2Mi)
% 1.75/1.42 % (19854)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_19752 for (2999ds/2Mi)
% 1.75/1.42 % (19855)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_19752 for (2999ds/275Mi)
% 1.75/1.42 % (19850)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_19752 for (2999ds/183Mi)
% 1.75/1.42 % (19856)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_19752 for (2999ds/18Mi)
% 1.75/1.42 % (19851)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_19752 for (2999ds/4Mi)
% 1.75/1.42 % (19853)Instruction limit reached!
% 1.75/1.42 % (19853)------------------------------
% 1.75/1.42 % (19853)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.42 % (19853)Termination reason: Unknown
% 1.75/1.42 % (19853)Termination phase: Preprocessing 2
% 1.75/1.42
% 1.75/1.42 % (19853)Memory used [KB]: 1023
% 1.75/1.42 % (19853)Time elapsed: 0.003 s
% 1.75/1.42 % (19853)Instructions burned: 2 (million)
% 1.75/1.42 % (19853)------------------------------
% 1.75/1.42 % (19853)------------------------------
% 1.75/1.42 % (19854)Instruction limit reached!
% 1.75/1.42 % (19854)------------------------------
% 1.75/1.42 % (19854)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.42 % (19854)Termination reason: Unknown
% 1.75/1.42 % (19854)Termination phase: Property scanning
% 1.75/1.42
% 1.75/1.42 % (19854)Memory used [KB]: 1023
% 1.75/1.42 % (19854)Time elapsed: 0.003 s
% 1.75/1.42 % (19854)Instructions burned: 3 (million)
% 1.75/1.42 % (19854)------------------------------
% 1.75/1.42 % (19854)------------------------------
% 1.75/1.42 % (19851)Instruction limit reached!
% 1.75/1.42 % (19851)------------------------------
% 1.75/1.42 % (19851)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.42 % (19851)Termination reason: Unknown
% 1.75/1.42 % (19851)Termination phase: Saturation
% 1.75/1.42
% 1.75/1.42 % (19851)Memory used [KB]: 5500
% 1.75/1.42 % (19851)Time elapsed: 0.005 s
% 1.75/1.42 % (19851)Instructions burned: 5 (million)
% 1.75/1.42 % (19851)------------------------------
% 1.75/1.42 % (19851)------------------------------
% 1.75/1.42 % (19852)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_19752 for (2999ds/27Mi)
% 1.75/1.42 % (19855)Refutation not found, incomplete strategy
% 1.75/1.42 % (19855)------------------------------
% 1.75/1.42 % (19855)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.42 % (19855)Termination reason: Refutation not found, incomplete strategy
% 1.75/1.42
% 1.75/1.42
% 1.75/1.42 % (19855)Memory used [KB]: 5500
% 1.75/1.42 % (19855)Time elapsed: 0.005 s
% 1.75/1.42 % (19855)Instructions burned: 4 (million)
% 1.75/1.42 % (19855)------------------------------
% 1.75/1.42 % (19855)------------------------------
% 1.75/1.43 % (19856)Instruction limit reached!
% 1.75/1.43 % (19856)------------------------------
% 1.75/1.43 % (19856)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.43 % (19856)Termination reason: Unknown
% 1.75/1.43 % (19856)Termination phase: Saturation
% 1.75/1.43
% 1.75/1.43 % (19856)Memory used [KB]: 5628
% 1.75/1.43 % (19856)Time elapsed: 0.013 s
% 1.75/1.43 % (19858)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_19752 for (2999ds/37Mi)
% 1.75/1.43 % (19856)Instructions burned: 19 (million)
% 1.75/1.43 % (19856)------------------------------
% 1.75/1.43 % (19856)------------------------------
% 1.75/1.44 % (19857)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_19752 for (2999ds/3Mi)
% 1.75/1.44 % (19857)Instruction limit reached!
% 1.75/1.44 % (19857)------------------------------
% 1.75/1.44 % (19857)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.44 % (19857)Termination reason: Unknown
% 1.75/1.44 % (19857)Termination phase: Saturation
% 1.75/1.44
% 1.75/1.44 % (19857)Memory used [KB]: 5500
% 1.75/1.44 % (19857)Time elapsed: 0.004 s
% 1.75/1.44 % (19857)Instructions burned: 3 (million)
% 1.75/1.44 % (19857)------------------------------
% 1.75/1.44 % (19857)------------------------------
% 1.75/1.44 % (19860)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_19752 for (2999ds/3Mi)
% 1.75/1.44 % (19852)Instruction limit reached!
% 1.75/1.44 % (19852)------------------------------
% 1.75/1.44 % (19852)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.44 % (19852)Termination reason: Unknown
% 1.75/1.44 % (19852)Termination phase: Saturation
% 1.75/1.44
% 1.75/1.44 % (19852)Memory used [KB]: 5756
% 1.75/1.44 % (19852)Time elapsed: 0.020 s
% 1.75/1.44 % (19852)Instructions burned: 27 (million)
% 1.75/1.44 % (19852)------------------------------
% 1.75/1.44 % (19852)------------------------------
% 1.75/1.44 % (19860)Instruction limit reached!
% 1.75/1.44 % (19860)------------------------------
% 1.75/1.44 % (19860)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.44 % (19860)Termination reason: Unknown
% 1.75/1.44 % (19860)Termination phase: Saturation
% 1.75/1.44
% 1.75/1.44 % (19860)Memory used [KB]: 5500
% 1.75/1.44 % (19860)Time elapsed: 0.004 s
% 1.75/1.44 % (19860)Instructions burned: 4 (million)
% 1.75/1.44 % (19860)------------------------------
% 1.75/1.44 % (19860)------------------------------
% 1.75/1.44 % (19858)Instruction limit reached!
% 1.75/1.44 % (19858)------------------------------
% 1.75/1.44 % (19858)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.44 % (19858)Termination reason: Unknown
% 1.75/1.44 % (19858)Termination phase: Saturation
% 1.75/1.44
% 1.75/1.44 % (19858)Memory used [KB]: 5628
% 1.75/1.44 % (19858)Time elapsed: 0.013 s
% 1.75/1.44 % (19858)Instructions burned: 37 (million)
% 1.75/1.44 % (19858)------------------------------
% 1.75/1.44 % (19858)------------------------------
% 1.75/1.44 % (19859)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_19752 for (2999ds/15Mi)
% 1.75/1.45 % (19861)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_19752 for (2999ds/1041Mi)
% 1.75/1.45 % (19859)Instruction limit reached!
% 1.75/1.45 % (19859)------------------------------
% 1.75/1.45 % (19859)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.45 % (19859)Termination reason: Unknown
% 1.75/1.45 % (19859)Termination phase: Saturation
% 1.75/1.45
% 1.75/1.45 % (19859)Memory used [KB]: 5756
% 1.75/1.45 % (19859)Time elapsed: 0.011 s
% 1.75/1.45 % (19859)Instructions burned: 16 (million)
% 1.75/1.45 % (19859)------------------------------
% 1.75/1.45 % (19859)------------------------------
% 1.75/1.46 % (19863)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_19752 for (2999ds/16Mi)
% 1.75/1.46 % (19864)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_19752 for (2999ds/3Mi)
% 1.75/1.46 % (19862)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_19752 for (2999ds/7Mi)
% 1.75/1.46 % (19865)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_19752 for (2999ds/3Mi)
% 1.75/1.46 % (19864)Instruction limit reached!
% 1.75/1.46 % (19864)------------------------------
% 1.75/1.46 % (19864)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.46 % (19864)Termination reason: Unknown
% 1.75/1.46 % (19864)Termination phase: Saturation
% 1.75/1.46
% 1.75/1.46 % (19864)Memory used [KB]: 1023
% 1.75/1.46 % (19864)Time elapsed: 0.003 s
% 1.75/1.46 % (19864)Instructions burned: 3 (million)
% 1.75/1.46 % (19864)------------------------------
% 1.75/1.46 % (19864)------------------------------
% 1.75/1.46 % (19865)Instruction limit reached!
% 1.75/1.46 % (19865)------------------------------
% 1.75/1.46 % (19865)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.46 % (19865)Termination reason: Unknown
% 1.75/1.46 % (19865)Termination phase: Saturation
% 1.75/1.46
% 1.75/1.46 % (19865)Memory used [KB]: 1023
% 1.75/1.46 % (19865)Time elapsed: 0.003 s
% 1.75/1.46 % (19865)Instructions burned: 4 (million)
% 1.75/1.46 % (19865)------------------------------
% 1.75/1.46 % (19865)------------------------------
% 1.75/1.46 % (19862)Instruction limit reached!
% 1.75/1.46 % (19862)------------------------------
% 1.75/1.46 % (19862)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.46 % (19862)Termination reason: Unknown
% 1.75/1.46 % (19862)Termination phase: Saturation
% 1.75/1.46
% 1.75/1.46 % (19862)Memory used [KB]: 1023
% 1.75/1.46 % (19862)Time elapsed: 0.006 s
% 1.75/1.46 % (19862)Instructions burned: 7 (million)
% 1.75/1.46 % (19862)------------------------------
% 1.75/1.46 % (19862)------------------------------
% 1.75/1.47 % (19863)Instruction limit reached!
% 1.75/1.47 % (19863)------------------------------
% 1.75/1.47 % (19863)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.47 % (19863)Termination reason: Unknown
% 1.75/1.47 % (19863)Termination phase: Saturation
% 1.75/1.47
% 1.75/1.47 % (19863)Memory used [KB]: 5756
% 1.75/1.47 % (19863)Time elapsed: 0.012 s
% 1.75/1.47 % (19863)Instructions burned: 17 (million)
% 1.75/1.47 % (19863)------------------------------
% 1.75/1.47 % (19863)------------------------------
% 1.75/1.47 % (19866)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_19752 for (2999ds/7Mi)
% 1.75/1.47 % (19866)Refutation not found, incomplete strategy
% 1.75/1.47 % (19866)------------------------------
% 1.75/1.47 % (19866)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.47 % (19866)Termination reason: Refutation not found, incomplete strategy
% 1.75/1.47
% 1.75/1.47
% 1.75/1.47 % (19866)Memory used [KB]: 5500
% 1.75/1.47 % (19866)Time elapsed: 0.005 s
% 1.75/1.47 % (19866)Instructions burned: 5 (million)
% 1.75/1.47 % (19866)------------------------------
% 1.75/1.47 % (19866)------------------------------
% 1.75/1.47 % (19867)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_19752 for (2999ds/3Mi)
% 1.75/1.47 % (19868)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_19752 for (2999ds/4Mi)
% 1.75/1.47 % (19867)Instruction limit reached!
% 1.75/1.47 % (19867)------------------------------
% 1.75/1.47 % (19867)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.48 % (19867)Termination reason: Unknown
% 1.75/1.48 % (19867)Termination phase: Property scanning
% 1.75/1.48
% 1.75/1.48 % (19867)Memory used [KB]: 1023
% 1.75/1.48 % (19867)Time elapsed: 0.003 s
% 1.75/1.48 % (19867)Instructions burned: 3 (million)
% 1.75/1.48 % (19867)------------------------------
% 1.75/1.48 % (19867)------------------------------
% 1.75/1.48 % (19868)Instruction limit reached!
% 1.75/1.48 % (19868)------------------------------
% 1.75/1.48 % (19868)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.48 % (19868)Termination reason: Unknown
% 1.75/1.48 % (19868)Termination phase: Saturation
% 1.75/1.48
% 1.75/1.48 % (19868)Memory used [KB]: 5500
% 1.75/1.48 % (19868)Time elapsed: 0.004 s
% 1.75/1.48 % (19868)Instructions burned: 4 (million)
% 1.75/1.48 % (19868)------------------------------
% 1.75/1.48 % (19868)------------------------------
% 1.75/1.48 % (19869)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_19752 for (2999ds/18Mi)
% 1.75/1.48 % (19870)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_19752 for (2999ds/710Mi)
% 1.75/1.49 % (19869)Instruction limit reached!
% 1.75/1.49 % (19869)------------------------------
% 1.75/1.49 % (19869)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.49 % (19869)Termination reason: Unknown
% 1.75/1.49 % (19869)Termination phase: Saturation
% 1.75/1.49
% 1.75/1.49 % (19869)Memory used [KB]: 5756
% 1.75/1.49 % (19869)Time elapsed: 0.013 s
% 1.75/1.49 % (19869)Instructions burned: 19 (million)
% 1.75/1.49 % (19869)------------------------------
% 1.75/1.49 % (19869)------------------------------
% 1.75/1.49 % (19871)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_19752 for (2999ds/6Mi)
% 1.75/1.49 % (19872)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_19752 for (2999ds/902Mi)
% 1.75/1.49 % (19872)Refutation not found, incomplete strategy
% 1.75/1.49 % (19872)------------------------------
% 1.75/1.49 % (19872)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.49 % (19872)Termination reason: Refutation not found, incomplete strategy
% 1.75/1.49
% 1.75/1.49
% 1.75/1.49 % (19872)Memory used [KB]: 5500
% 1.75/1.49 % (19872)Time elapsed: 0.003 s
% 1.75/1.49 % (19872)Instructions burned: 3 (million)
% 1.75/1.49 % (19872)------------------------------
% 1.75/1.49 % (19872)------------------------------
% 1.75/1.49 % (19871)Instruction limit reached!
% 1.75/1.49 % (19871)------------------------------
% 1.75/1.49 % (19871)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.75/1.49 % (19871)Termination reason: Unknown
% 1.75/1.49 % (19871)Termination phase: Saturation
% 1.75/1.49
% 1.75/1.49 % (19871)Memory used [KB]: 5628
% 1.75/1.49 % (19871)Time elapsed: 0.006 s
% 1.75/1.49 % (19871)Instructions burned: 7 (million)
% 1.75/1.49 % (19871)------------------------------
% 1.75/1.49 % (19871)------------------------------
% 1.75/1.49 % (19873)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_19752 for (2999ds/21Mi)
% 1.76/1.50 % (19861)First to succeed.
% 1.76/1.50 % (19874)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_19752 for (2999ds/5Mi)
% 1.76/1.51 % (19873)Instruction limit reached!
% 1.76/1.51 % (19873)------------------------------
% 1.76/1.51 % (19873)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.51 % (19873)Termination reason: Unknown
% 1.76/1.51 % (19873)Termination phase: Saturation
% 1.76/1.51
% 1.76/1.51 % (19873)Memory used [KB]: 5756
% 1.76/1.51 % (19873)Time elapsed: 0.014 s
% 1.76/1.51 % (19873)Instructions burned: 21 (million)
% 1.76/1.51 % (19873)------------------------------
% 1.76/1.51 % (19873)------------------------------
% 1.76/1.51 % (19874)Instruction limit reached!
% 1.76/1.51 % (19874)------------------------------
% 1.76/1.51 % (19874)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.51 % (19874)Termination reason: Unknown
% 1.76/1.51 % (19874)Termination phase: Saturation
% 1.76/1.51
% 1.76/1.51 % (19874)Memory used [KB]: 5500
% 1.76/1.51 % (19874)Time elapsed: 0.005 s
% 1.76/1.51 % (19874)Instructions burned: 6 (million)
% 1.76/1.51 % (19874)------------------------------
% 1.76/1.51 % (19874)------------------------------
% 1.76/1.51 % (19861)Refutation found. Thanks to Tanya!
% 1.76/1.51 % SZS status Theorem for DTF2THF_19752
% 1.76/1.51 % SZS output start Proof for DTF2THF_19752
% 1.76/1.51 thf(type_def_5, type, a: $tType).
% 1.76/1.51 thf(func_def_0, type, a: $tType).
% 1.76/1.51 thf(func_def_17, type, ph1: !>[X0: $tType]:(X0)).
% 1.76/1.51 thf(func_def_18, type, sK2: a > $o).
% 1.76/1.51 thf(func_def_19, type, sK3: a > $o).
% 1.76/1.51 thf(func_def_20, type, sK4: a > $o).
% 1.76/1.51 thf(func_def_21, type, sK5: (a > $o) > $o).
% 1.76/1.51 thf(func_def_22, type, sK6: a).
% 1.76/1.51 thf(func_def_23, type, sK7: (a > $o) > $o).
% 1.76/1.51 thf(func_def_24, type, sK8: a).
% 1.76/1.51 thf(func_def_25, type, sK9: a > a > $o).
% 1.76/1.51 thf(func_def_26, type, sK10: a > $o).
% 1.76/1.51 thf(func_def_27, type, sK11: a).
% 1.76/1.51 thf(func_def_28, type, sK12: a > $o).
% 1.76/1.51 thf(func_def_29, type, sK13: a > $o).
% 1.76/1.51 thf(func_def_30, type, sK14: a > $o).
% 1.76/1.51 thf(func_def_31, type, sK15: a).
% 1.76/1.51 thf(func_def_32, type, sK16: a).
% 1.76/1.51 thf(func_def_33, type, sK17: a).
% 1.76/1.51 thf(func_def_34, type, sK18: a).
% 1.76/1.51 thf(func_def_35, type, sK19: a).
% 1.76/1.51 thf(func_def_36, type, sK20: a).
% 1.76/1.51 thf(func_def_37, type, sK21: a).
% 1.76/1.51 thf(func_def_38, type, sK22: a).
% 1.76/1.51 thf(func_def_39, type, sK23: a).
% 1.76/1.51 thf(f553,plain,(
% 1.76/1.51 $false),
% 1.76/1.51 inference(avatar_sat_refutation,[status(thm)],[f18,f28,f45,f56,f69,f284,f304,f351,f362,f406,f444,f499,f524,f552])).
% 1.76/1.51 thf(f552,plain,(
% 1.76/1.51 ~spl0_1 | ~spl0_13 | ~spl0_15),
% 1.76/1.51 inference(avatar_contradiction_clause,[status(thm)],[f551])).
% 1.76/1.51 thf(f551,plain,(
% 1.76/1.51 $false | (~spl0_1 | ~spl0_13 | ~spl0_15)),
% 1.76/1.51 inference(subsumption_resolution,[status(thm)],[f550,f475])).
% 1.76/1.51 thf(f475,plain,(
% 1.76/1.51 ( ! [X1 : a] : (((sK10 @ X1) = (sK12 @ X1))) ) | (~spl0_1 | ~spl0_13)),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f474])).
% 1.76/1.51 thf(f474,plain,(
% 1.76/1.51 ( ! [X1 : a] : (((sK12 @ X1) = ($true & (sK10 @ X1)))) ) | (~spl0_1 | ~spl0_13)),
% 1.76/1.51 inference(forward_demodulation,[status(thm)],[f473,f455])).
% 1.76/1.51 thf(f455,plain,(
% 1.76/1.51 ( ! [X1 : a] : (((sK14 @ X1) = $true)) ) | ~spl0_13),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f454])).
% 1.76/1.51 thf(f454,plain,(
% 1.76/1.51 ( ! [X1 : a] : (((sK14 @ X1) = ((^[Y0 : a]: ($true)) @ X1))) ) | ~spl0_13),
% 1.76/1.51 inference(argument_congruence,[status(thm)],[f447])).
% 1.76/1.51 thf(f447,plain,(
% 1.76/1.51 ((^[Y0 : a]: ($true)) = sK14) | ~spl0_13),
% 1.76/1.51 inference(equality_proxy_clausification,[status(thm)],[f405])).
% 1.76/1.51 thf(f405,plain,(
% 1.76/1.51 ($true = (sK14 = (^[Y0 : a]: ($true)))) | ~spl0_13),
% 1.76/1.51 inference(avatar_component_clause,[status(thm)],[f404])).
% 1.76/1.51 thf(f404,definition,(
% 1.76/1.51 spl0_13 <=> ($true = (sK14 = (^[Y0 : a]: ($true))))),
% 1.76/1.51 introduced(definition,[new_symbols(naming,[spl0_13])],[avatar_definition])).
% 1.76/1.51 thf(f473,plain,(
% 1.76/1.51 ( ! [X1 : a] : ((((sK14 @ X1) & (sK10 @ X1)) = (sK12 @ X1))) ) | (~spl0_1 | ~spl0_13)),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f472])).
% 1.76/1.51 thf(f472,plain,(
% 1.76/1.51 ( ! [X1 : a] : ((((^[Y0 : a]: ((sK14 @ Y0) & (sK10 @ Y0))) @ X1) = (sK12 @ X1))) ) | (~spl0_1 | ~spl0_13)),
% 1.76/1.51 inference(argument_congruence,[status(thm)],[f467])).
% 1.76/1.51 thf(f467,plain,(
% 1.76/1.51 (sK12 = (^[Y0 : a]: ((sK14 @ Y0) & (sK10 @ Y0)))) | (~spl0_1 | ~spl0_13)),
% 1.76/1.51 inference(equality_proxy_clausification,[status(thm)],[f464])).
% 1.76/1.51 thf(f464,plain,(
% 1.76/1.51 (((^[Y0 : a]: ((sK14 @ Y0) & (sK10 @ Y0))) = sK12) = $true) | (~spl0_1 | ~spl0_13)),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f462])).
% 1.76/1.51 thf(f462,plain,(
% 1.76/1.51 ($true = ($true & ((^[Y0 : a]: ((sK14 @ Y0) & (sK10 @ Y0))) = sK12))) | (~spl0_1 | ~spl0_13)),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f451,f461])).
% 1.76/1.51 thf(f461,plain,(
% 1.76/1.51 ($true = ((sK14 = sK10) | (sK10 = (^[Y0 : a]: ($false))))) | (~spl0_1 | ~spl0_13)),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f451])).
% 1.76/1.51 thf(f451,plain,(
% 1.76/1.51 ((((sK14 = sK10) | (sK10 = (^[Y0 : a]: ($false)))) & ((^[Y0 : a]: ((sK14 @ Y0) & (sK10 @ Y0))) = sK12)) = $true) | (~spl0_1 | ~spl0_13)),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f396,f447])).
% 1.76/1.51 thf(f396,plain,(
% 1.76/1.51 ($true = ((((^[Y0 : a]: ($true)) = sK10) | (sK10 = (^[Y0 : a]: ($false)))) & ((^[Y0 : a]: ((sK14 @ Y0) & (sK10 @ Y0))) = sK12))) | ~spl0_1),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f390])).
% 1.76/1.51 thf(f390,plain,(
% 1.76/1.51 ((((((^[Y0 : a]: ($true)) = sK10) | (sK10 = (^[Y0 : a]: ($false)))) & ((^[Y0 : a]: ((sK14 @ Y0) & (sK10 @ Y0))) = sK12)) & ((sK14 = (^[Y0 : a]: ($true))) | ((^[Y0 : a]: ($false)) = sK14))) = $true) | ~spl0_1),
% 1.76/1.51 inference(not_proxy_clausification,[status(thm)],[f386])).
% 1.76/1.51 thf(f386,plain,(
% 1.76/1.51 ($false = (~ (((((^[Y0 : a]: ($true)) = sK10) | (sK10 = (^[Y0 : a]: ($false)))) & ((^[Y0 : a]: ((sK14 @ Y0) & (sK10 @ Y0))) = sK12)) & ((sK14 = (^[Y0 : a]: ($true))) | ((^[Y0 : a]: ($false)) = sK14))))) | ~spl0_1),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f385])).
% 1.76/1.51 thf(f385,plain,(
% 1.76/1.51 ($false = ((^[Y0 : a > $o]: (~ (((((^[Y1 : a]: ($true)) = sK10) | (sK10 = (^[Y1 : a]: ($false)))) & ((^[Y1 : a]: ((Y0 @ Y1) & (sK10 @ Y1))) = sK12)) & ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0))))) @ sK14)) | ~spl0_1),
% 1.76/1.51 inference(sigma_clausification,[status(thm)],[f377])).
% 1.76/1.51 thf(f377,plain,(
% 1.76/1.51 ($false = (!! @ (a > $o) @ (^[Y0 : a > $o]: (~ (((((^[Y1 : a]: ($true)) = sK10) | (sK10 = (^[Y1 : a]: ($false)))) & ((^[Y1 : a]: ((Y0 @ Y1) & (sK10 @ Y1))) = sK12)) & ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0))))))) | ~spl0_1),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f376])).
% 1.76/1.51 thf(f376,plain,(
% 1.76/1.51 ($false = (!! @ (a > $o) @ (^[Y0 : a > $o]: ((((((^[Y1 : a]: ($true)) = sK10) | (sK10 = (^[Y1 : a]: ($false)))) & ((^[Y1 : a]: ((Y0 @ Y1) & (sK10 @ Y1))) = sK12)) & ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0))) => $false)))) | ~spl0_1),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f370,f373])).
% 1.76/1.51 thf(f373,plain,(
% 1.76/1.51 (((sK12 = (^[Y0 : a]: ($false))) | (sK12 = (^[Y0 : a]: ($true)))) = $false) | ~spl0_1),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f372])).
% 1.76/1.51 thf(f372,plain,(
% 1.76/1.51 ($false = ((((((^[Y0 : a]: ($true)) = sK10) | (sK10 = (^[Y0 : a]: ($false)))) & ((^[Y0 : a]: ((sK13 @ Y0) & (sK10 @ Y0))) = sK12)) & ((sK13 = (^[Y0 : a]: ($true))) | ((^[Y0 : a]: ($false)) = sK13))) => ((sK12 = (^[Y0 : a]: ($false))) | (sK12 = (^[Y0 : a]: ($true)))))) | ~spl0_1),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f371])).
% 1.76/1.51 thf(f371,plain,(
% 1.76/1.51 (((^[Y0 : a > $o]: ((((((^[Y1 : a]: ($true)) = sK10) | (sK10 = (^[Y1 : a]: ($false)))) & ((^[Y1 : a]: ((Y0 @ Y1) & (sK10 @ Y1))) = sK12)) & ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0))) => ((sK12 = (^[Y1 : a]: ($false))) | (sK12 = (^[Y1 : a]: ($true)))))) @ sK13) = $false) | ~spl0_1),
% 1.76/1.51 inference(sigma_clausification,[status(thm)],[f370])).
% 1.76/1.51 thf(f370,plain,(
% 1.76/1.51 ($false = (!! @ (a > $o) @ (^[Y0 : a > $o]: ((((((^[Y1 : a]: ($true)) = sK10) | (sK10 = (^[Y1 : a]: ($false)))) & ((^[Y1 : a]: ((Y0 @ Y1) & (sK10 @ Y1))) = sK12)) & ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0))) => ((sK12 = (^[Y1 : a]: ($false))) | (sK12 = (^[Y1 : a]: ($true)))))))) | ~spl0_1),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f369])).
% 1.76/1.51 thf(f369,plain,(
% 1.76/1.51 (((^[Y0 : a > $o]: (!! @ (a > $o) @ (^[Y1 : a > $o]: ((((((^[Y2 : a]: ($true)) = sK10) | (sK10 = (^[Y2 : a]: ($false)))) & ((^[Y2 : a]: ((Y1 @ Y2) & (sK10 @ Y2))) = Y0)) & ((Y1 = (^[Y2 : a]: ($true))) | ((^[Y2 : a]: ($false)) = Y1))) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: ($true)))))))) @ sK12) = $false) | ~spl0_1),
% 1.76/1.51 inference(sigma_clausification,[status(thm)],[f366])).
% 1.76/1.51 thf(f366,plain,(
% 1.76/1.51 ($false = (!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ (a > $o) @ (^[Y1 : a > $o]: ((((((^[Y2 : a]: ($true)) = sK10) | (sK10 = (^[Y2 : a]: ($false)))) & ((^[Y2 : a]: ((Y1 @ Y2) & (sK10 @ Y2))) = Y0)) & ((Y1 = (^[Y2 : a]: ($true))) | ((^[Y2 : a]: ($false)) = Y1))) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: ($true)))))))))) | ~spl0_1),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f365])).
% 1.76/1.51 thf(f365,plain,(
% 1.76/1.51 (((^[Y0 : a > $o]: (!! @ (a > $o) @ (^[Y1 : a > $o]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((((((^[Y3 : a]: ($true)) = Y0) | (Y0 = (^[Y3 : a]: ($false)))) & ((^[Y3 : a]: ((Y2 @ Y3) & (Y0 @ Y3))) = Y1)) & ((Y2 = (^[Y3 : a]: ($true))) | ((^[Y3 : a]: ($false)) = Y2))) => ((Y1 = (^[Y3 : a]: ($false))) | (Y1 = (^[Y3 : a]: ($true)))))))))) @ sK10) = $false) | ~spl0_1),
% 1.76/1.51 inference(sigma_clausification,[status(thm)],[f14])).
% 1.76/1.51 thf(f14,plain,(
% 1.76/1.51 ((!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ (a > $o) @ (^[Y1 : a > $o]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((((((^[Y3 : a]: ($true)) = Y0) | (Y0 = (^[Y3 : a]: ($false)))) & ((^[Y3 : a]: ((Y2 @ Y3) & (Y0 @ Y3))) = Y1)) & ((Y2 = (^[Y3 : a]: ($true))) | ((^[Y3 : a]: ($false)) = Y2))) => ((Y1 = (^[Y3 : a]: ($false))) | (Y1 = (^[Y3 : a]: ($true))))))))))) = $false) | ~spl0_1),
% 1.76/1.51 inference(avatar_component_clause,[status(thm)],[f13])).
% 1.76/1.51 thf(f13,definition,(
% 1.76/1.51 spl0_1 <=> ((!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ (a > $o) @ (^[Y1 : a > $o]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((((((^[Y3 : a]: ($true)) = Y0) | (Y0 = (^[Y3 : a]: ($false)))) & ((^[Y3 : a]: ((Y2 @ Y3) & (Y0 @ Y3))) = Y1)) & ((Y2 = (^[Y3 : a]: ($true))) | ((^[Y3 : a]: ($false)) = Y2))) => ((Y1 = (^[Y3 : a]: ($false))) | (Y1 = (^[Y3 : a]: ($true))))))))))) = $false)),
% 1.76/1.51 introduced(definition,[new_symbols(naming,[spl0_1])],[avatar_definition])).
% 1.76/1.51 thf(f550,plain,(
% 1.76/1.51 ((sK10 @ sK23) != (sK12 @ sK23)) | (~spl0_1 | ~spl0_15)),
% 1.76/1.51 inference(negative_extensionality,[status(thm)],[f545])).
% 1.76/1.51 thf(f545,plain,(
% 1.76/1.51 (sK12 != sK10) | (~spl0_1 | ~spl0_15)),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f387,f542])).
% 1.76/1.51 thf(f542,plain,(
% 1.76/1.51 (sK10 = (^[Y0 : a]: ($false))) | ~spl0_15),
% 1.76/1.51 inference(equality_proxy_clausification,[status(thm)],[f498])).
% 1.76/1.51 thf(f498,plain,(
% 1.76/1.51 ($true = (sK10 = (^[Y0 : a]: ($false)))) | ~spl0_15),
% 1.76/1.51 inference(avatar_component_clause,[status(thm)],[f497])).
% 1.76/1.51 thf(f497,definition,(
% 1.76/1.51 spl0_15 <=> ($true = (sK10 = (^[Y0 : a]: ($false))))),
% 1.76/1.51 introduced(definition,[new_symbols(naming,[spl0_15])],[avatar_definition])).
% 1.76/1.51 thf(f387,plain,(
% 1.76/1.51 (sK12 != (^[Y0 : a]: ($false))) | ~spl0_1),
% 1.76/1.51 inference(equality_proxy_clausification,[status(thm)],[f384])).
% 1.76/1.51 thf(f384,plain,(
% 1.76/1.51 ((sK12 = (^[Y0 : a]: ($false))) = $false) | ~spl0_1),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f383])).
% 1.76/1.51 thf(f383,plain,(
% 1.76/1.51 ($false = ((sK12 = (^[Y0 : a]: ($false))) | $false)) | ~spl0_1),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f373,f381])).
% 1.76/1.51 thf(f381,plain,(
% 1.76/1.51 ((sK12 = (^[Y0 : a]: ($true))) = $false) | ~spl0_1),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f373])).
% 1.76/1.51 thf(f524,plain,(
% 1.76/1.51 ~spl0_1 | ~spl0_13 | ~spl0_14),
% 1.76/1.51 inference(avatar_contradiction_clause,[status(thm)],[f523])).
% 1.76/1.51 thf(f523,plain,(
% 1.76/1.51 $false | (~spl0_1 | ~spl0_13 | ~spl0_14)),
% 1.76/1.51 inference(subsumption_resolution,[status(thm)],[f522,f511])).
% 1.76/1.51 thf(f511,plain,(
% 1.76/1.51 ( ! [X1 : a] : (($true = (sK10 @ X1))) ) | (~spl0_13 | ~spl0_14)),
% 1.76/1.51 inference(forward_demodulation,[status(thm)],[f510,f455])).
% 1.76/1.51 thf(f510,plain,(
% 1.76/1.51 ( ! [X1 : a] : (((sK14 @ X1) = (sK10 @ X1))) ) | ~spl0_14),
% 1.76/1.51 inference(argument_congruence,[status(thm)],[f502])).
% 1.76/1.51 thf(f502,plain,(
% 1.76/1.51 (sK10 = sK14) | ~spl0_14),
% 1.76/1.51 inference(equality_proxy_clausification,[status(thm)],[f495])).
% 1.76/1.51 thf(f495,plain,(
% 1.76/1.51 ((sK14 = sK10) = $true) | ~spl0_14),
% 1.76/1.51 inference(avatar_component_clause,[status(thm)],[f494])).
% 1.76/1.51 thf(f494,definition,(
% 1.76/1.51 spl0_14 <=> ((sK14 = sK10) = $true)),
% 1.76/1.51 introduced(definition,[new_symbols(naming,[spl0_14])],[avatar_definition])).
% 1.76/1.51 thf(f522,plain,(
% 1.76/1.51 ($true != (sK10 @ sK20)) | (~spl0_1 | ~spl0_13 | ~spl0_14)),
% 1.76/1.51 inference(forward_demodulation,[status(thm)],[f521,f517])).
% 1.76/1.51 thf(f517,plain,(
% 1.76/1.51 ( ! [X1 : a] : (($true = (sK12 @ X1))) ) | (~spl0_1 | ~spl0_13 | ~spl0_14)),
% 1.76/1.51 inference(trivial_inequality_removal,[status(thm)],[f513])).
% 1.76/1.51 thf(f513,plain,(
% 1.76/1.51 ( ! [X1 : a] : (($true = $false) | ($true = (sK12 @ X1))) ) | (~spl0_1 | ~spl0_13 | ~spl0_14)),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f481,f511])).
% 1.76/1.51 thf(f481,plain,(
% 1.76/1.51 ( ! [X1 : a] : (($true = (sK12 @ X1)) | ($false = (sK10 @ X1))) ) | (~spl0_1 | ~spl0_13)),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f475])).
% 1.76/1.51 thf(f521,plain,(
% 1.76/1.51 ((sK10 @ sK20) != (sK12 @ sK20)) | (~spl0_1 | ~spl0_13 | ~spl0_14)),
% 1.76/1.51 inference(negative_extensionality,[status(thm)],[f505])).
% 1.76/1.51 thf(f505,plain,(
% 1.76/1.51 (sK12 != sK10) | (~spl0_1 | ~spl0_13 | ~spl0_14)),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f466,f502])).
% 1.76/1.51 thf(f466,plain,(
% 1.76/1.51 (sK12 != sK14) | (~spl0_1 | ~spl0_13)),
% 1.76/1.51 inference(equality_proxy_clausification,[status(thm)],[f450])).
% 1.76/1.51 thf(f450,plain,(
% 1.76/1.51 ($false = (sK12 = sK14)) | (~spl0_1 | ~spl0_13)),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f381,f447])).
% 1.76/1.51 thf(f499,plain,(
% 1.76/1.51 spl0_14 | spl0_15 | ~spl0_1 | ~spl0_13),
% 1.76/1.51 inference(avatar_split_clause,[status(thm)],[f492,f404,f13,f497,f494])).
% 1.76/1.51 thf(f492,plain,(
% 1.76/1.51 ((sK14 = sK10) = $true) | ($true = (sK10 = (^[Y0 : a]: ($false)))) | (~spl0_1 | ~spl0_13)),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f461])).
% 1.76/1.51 thf(f444,plain,(
% 1.76/1.51 ~spl0_1 | ~spl0_12),
% 1.76/1.51 inference(avatar_contradiction_clause,[status(thm)],[f443])).
% 1.76/1.51 thf(f443,plain,(
% 1.76/1.51 $false | (~spl0_1 | ~spl0_12)),
% 1.76/1.51 inference(trivial_inequality_removal,[status(thm)],[f440])).
% 1.76/1.51 thf(f440,plain,(
% 1.76/1.51 ($false != $false) | (~spl0_1 | ~spl0_12)),
% 1.76/1.51 inference(superposition,[status(thm)],[f422,f438])).
% 1.76/1.51 thf(f438,plain,(
% 1.76/1.51 ( ! [X1 : a] : (($false = (sK12 @ X1))) ) | (~spl0_1 | ~spl0_12)),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f437])).
% 1.76/1.51 thf(f437,plain,(
% 1.76/1.51 ( ! [X1 : a] : ((($false & (sK10 @ X1)) = (sK12 @ X1))) ) | (~spl0_1 | ~spl0_12)),
% 1.76/1.51 inference(forward_demodulation,[status(thm)],[f436,f419])).
% 1.76/1.51 thf(f419,plain,(
% 1.76/1.51 ( ! [X1 : a] : (((sK14 @ X1) = $false)) ) | ~spl0_12),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f417])).
% 1.76/1.51 thf(f417,plain,(
% 1.76/1.51 ( ! [X1 : a] : ((((^[Y0 : a]: ($false)) @ X1) = (sK14 @ X1))) ) | ~spl0_12),
% 1.76/1.51 inference(argument_congruence,[status(thm)],[f409])).
% 1.76/1.51 thf(f409,plain,(
% 1.76/1.51 ((^[Y0 : a]: ($false)) = sK14) | ~spl0_12),
% 1.76/1.51 inference(equality_proxy_clausification,[status(thm)],[f402])).
% 1.76/1.51 thf(f402,plain,(
% 1.76/1.51 ($true = ((^[Y0 : a]: ($false)) = sK14)) | ~spl0_12),
% 1.76/1.51 inference(avatar_component_clause,[status(thm)],[f401])).
% 1.76/1.51 thf(f401,definition,(
% 1.76/1.51 spl0_12 <=> ($true = ((^[Y0 : a]: ($false)) = sK14))),
% 1.76/1.51 introduced(definition,[new_symbols(naming,[spl0_12])],[avatar_definition])).
% 1.76/1.51 thf(f436,plain,(
% 1.76/1.51 ( ! [X1 : a] : ((((sK14 @ X1) & (sK10 @ X1)) = (sK12 @ X1))) ) | (~spl0_1 | ~spl0_12)),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f435])).
% 1.76/1.51 thf(f435,plain,(
% 1.76/1.51 ( ! [X1 : a] : ((((^[Y0 : a]: ((sK14 @ Y0) & (sK10 @ Y0))) @ X1) = (sK12 @ X1))) ) | (~spl0_1 | ~spl0_12)),
% 1.76/1.51 inference(argument_congruence,[status(thm)],[f429])).
% 1.76/1.51 thf(f429,plain,(
% 1.76/1.51 (sK12 = (^[Y0 : a]: ((sK14 @ Y0) & (sK10 @ Y0)))) | (~spl0_1 | ~spl0_12)),
% 1.76/1.51 inference(equality_proxy_clausification,[status(thm)],[f427])).
% 1.76/1.51 thf(f427,plain,(
% 1.76/1.51 (((^[Y0 : a]: ((sK14 @ Y0) & (sK10 @ Y0))) = sK12) = $true) | (~spl0_1 | ~spl0_12)),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f426])).
% 1.76/1.51 thf(f426,plain,(
% 1.76/1.51 ($true = ($true & ((^[Y0 : a]: ((sK14 @ Y0) & (sK10 @ Y0))) = sK12))) | (~spl0_1 | ~spl0_12)),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f414,f424])).
% 1.76/1.51 thf(f424,plain,(
% 1.76/1.51 ($true = (((^[Y0 : a]: ($true)) = sK10) | (sK10 = sK14))) | (~spl0_1 | ~spl0_12)),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f414])).
% 1.76/1.51 thf(f414,plain,(
% 1.76/1.51 (((((^[Y0 : a]: ($true)) = sK10) | (sK10 = sK14)) & ((^[Y0 : a]: ((sK14 @ Y0) & (sK10 @ Y0))) = sK12)) = $true) | (~spl0_1 | ~spl0_12)),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f396,f409])).
% 1.76/1.51 thf(f422,plain,(
% 1.76/1.51 ($false != (sK12 @ sK16)) | (~spl0_1 | ~spl0_12)),
% 1.76/1.51 inference(forward_demodulation,[status(thm)],[f421,f419])).
% 1.76/1.51 thf(f421,plain,(
% 1.76/1.51 ((sK12 @ sK16) != (sK14 @ sK16)) | (~spl0_1 | ~spl0_12)),
% 1.76/1.51 inference(negative_extensionality,[status(thm)],[f418])).
% 1.76/1.51 thf(f418,plain,(
% 1.76/1.51 (sK12 != sK14) | (~spl0_1 | ~spl0_12)),
% 1.76/1.51 inference(superposition,[status(thm)],[f387,f409])).
% 1.76/1.51 thf(f406,plain,(
% 1.76/1.51 spl0_12 | spl0_13 | ~spl0_1),
% 1.76/1.51 inference(avatar_split_clause,[status(thm)],[f399,f13,f404,f401])).
% 1.76/1.51 thf(f399,plain,(
% 1.76/1.51 ($true = (sK14 = (^[Y0 : a]: ($true)))) | ($true = ((^[Y0 : a]: ($false)) = sK14)) | ~spl0_1),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f398])).
% 1.76/1.51 thf(f398,plain,(
% 1.76/1.51 (((sK14 = (^[Y0 : a]: ($true))) | ((^[Y0 : a]: ($false)) = sK14)) = $true) | ~spl0_1),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f397])).
% 1.76/1.51 thf(f397,plain,(
% 1.76/1.51 ($true = ($true & ((sK14 = (^[Y0 : a]: ($true))) | ((^[Y0 : a]: ($false)) = sK14)))) | ~spl0_1),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f390,f396])).
% 1.76/1.51 thf(f362,plain,(
% 1.76/1.51 ~spl0_6 | ~spl0_10),
% 1.76/1.51 inference(avatar_contradiction_clause,[status(thm)],[f361])).
% 1.76/1.51 thf(f361,plain,(
% 1.76/1.51 $false | (~spl0_6 | ~spl0_10)),
% 1.76/1.51 inference(trivial_inequality_removal,[status(thm)],[f360])).
% 1.76/1.51 thf(f360,plain,(
% 1.76/1.51 ($false != $false) | (~spl0_6 | ~spl0_10)),
% 1.76/1.51 inference(superposition,[status(thm)],[f97,f299])).
% 1.76/1.51 thf(f299,plain,(
% 1.76/1.51 ( ! [X0 : a] : (((sK4 @ X0) = $false)) ) | ~spl0_10),
% 1.76/1.51 inference(avatar_component_clause,[status(thm)],[f298])).
% 1.76/1.51 thf(f298,definition,(
% 1.76/1.51 spl0_10 <=> ! [X0 : a] : ((sK4 @ X0) = $false)),
% 1.76/1.51 introduced(definition,[new_symbols(naming,[spl0_10])],[avatar_definition])).
% 1.76/1.51 thf(f97,plain,(
% 1.76/1.51 ($false != (sK4 @ sK8)) | ~spl0_6),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f96])).
% 1.76/1.51 thf(f96,plain,(
% 1.76/1.51 ((sK4 @ sK8) != ((^[Y0 : a]: ($false)) @ sK8)) | ~spl0_6),
% 1.76/1.51 inference(negative_extensionality,[status(thm)],[f92])).
% 1.76/1.51 thf(f92,plain,(
% 1.76/1.51 (sK4 != (^[Y0 : a]: ($false))) | ~spl0_6),
% 1.76/1.51 inference(equality_proxy_clausification,[status(thm)],[f84])).
% 1.76/1.51 thf(f84,plain,(
% 1.76/1.51 ((sK4 = (^[Y0 : a]: ($false))) = $false) | ~spl0_6),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f80])).
% 1.76/1.51 thf(f80,plain,(
% 1.76/1.51 ($false = ((sK4 = (^[Y0 : a]: ($false))) | (sK4 = (^[Y0 : a]: ($true))))) | ~spl0_6),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f79])).
% 1.76/1.51 thf(f79,plain,(
% 1.76/1.51 (($true => ((sK4 = (^[Y0 : a]: ($false))) | (sK4 = (^[Y0 : a]: ($true))))) = $false) | ~spl0_6),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f76,f78])).
% 1.76/1.51 thf(f78,plain,(
% 1.76/1.51 ($true = ((!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK5 @ Y0) => (((^[Y1 : a]: ($true)) = Y0) | ((^[Y1 : a]: ($false)) = Y0))))) & ((^[Y0 : a]: (?? @ (a > $o) @ (^[Y1 : a > $o]: ((Y1 @ Y0) & (sK5 @ Y1))))) = sK4))) | ~spl0_6),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f76])).
% 1.76/1.51 thf(f76,plain,(
% 1.76/1.51 ($false = (((!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK5 @ Y0) => (((^[Y1 : a]: ($true)) = Y0) | ((^[Y1 : a]: ($false)) = Y0))))) & ((^[Y0 : a]: (?? @ (a > $o) @ (^[Y1 : a > $o]: ((Y1 @ Y0) & (sK5 @ Y1))))) = sK4)) => ((sK4 = (^[Y0 : a]: ($false))) | (sK4 = (^[Y0 : a]: ($true)))))) | ~spl0_6),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f75])).
% 1.76/1.51 thf(f75,plain,(
% 1.76/1.51 ($false = ((^[Y0 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y1 : a > $o]: ((Y0 @ Y1) => (((^[Y2 : a]: ($true)) = Y1) | ((^[Y2 : a]: ($false)) = Y1))))) & ((^[Y1 : a]: (?? @ (a > $o) @ (^[Y2 : a > $o]: ((Y2 @ Y1) & (Y0 @ Y2))))) = sK4)) => ((sK4 = (^[Y1 : a]: ($false))) | (sK4 = (^[Y1 : a]: ($true)))))) @ sK5)) | ~spl0_6),
% 1.76/1.51 inference(sigma_clausification,[status(thm)],[f74])).
% 1.76/1.51 thf(f74,plain,(
% 1.76/1.51 ($false = (!! @ ((a > $o) > $o) @ (^[Y0 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y1 : a > $o]: ((Y0 @ Y1) => (((^[Y2 : a]: ($true)) = Y1) | ((^[Y2 : a]: ($false)) = Y1))))) & ((^[Y1 : a]: (?? @ (a > $o) @ (^[Y2 : a > $o]: ((Y2 @ Y1) & (Y0 @ Y2))))) = sK4)) => ((sK4 = (^[Y1 : a]: ($false))) | (sK4 = (^[Y1 : a]: ($true)))))))) | ~spl0_6),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f73])).
% 1.76/1.51 thf(f73,plain,(
% 1.76/1.51 (((^[Y0 : a > $o]: (!! @ ((a > $o) > $o) @ (^[Y1 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y1 @ Y2) => (((^[Y3 : a]: ($true)) = Y2) | ((^[Y3 : a]: ($false)) = Y2))))) & ((^[Y2 : a]: (?? @ (a > $o) @ (^[Y3 : a > $o]: ((Y3 @ Y2) & (Y1 @ Y3))))) = Y0)) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: ($true)))))))) @ sK4) = $false) | ~spl0_6),
% 1.76/1.51 inference(sigma_clausification,[status(thm)],[f55])).
% 1.76/1.51 thf(f55,plain,(
% 1.76/1.51 ($false = (!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ ((a > $o) > $o) @ (^[Y1 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y1 @ Y2) => (((^[Y3 : a]: ($true)) = Y2) | ((^[Y3 : a]: ($false)) = Y2))))) & ((^[Y2 : a]: (?? @ (a > $o) @ (^[Y3 : a > $o]: ((Y3 @ Y2) & (Y1 @ Y3))))) = Y0)) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: ($true)))))))))) | ~spl0_6),
% 1.76/1.51 inference(avatar_component_clause,[status(thm)],[f54])).
% 1.76/1.51 thf(f54,definition,(
% 1.76/1.51 spl0_6 <=> ($false = (!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ ((a > $o) > $o) @ (^[Y1 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y1 @ Y2) => (((^[Y3 : a]: ($true)) = Y2) | ((^[Y3 : a]: ($false)) = Y2))))) & ((^[Y2 : a]: (?? @ (a > $o) @ (^[Y3 : a > $o]: ((Y3 @ Y2) & (Y1 @ Y3))))) = Y0)) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: ($true))))))))))),
% 1.76/1.51 introduced(definition,[new_symbols(naming,[spl0_6])],[avatar_definition])).
% 1.76/1.51 thf(f351,plain,(
% 1.76/1.51 ~spl0_6 | ~spl0_9),
% 1.76/1.51 inference(avatar_contradiction_clause,[status(thm)],[f350])).
% 1.76/1.51 thf(f350,plain,(
% 1.76/1.51 $false | (~spl0_6 | ~spl0_9)),
% 1.76/1.51 inference(trivial_inequality_removal,[status(thm)],[f347])).
% 1.76/1.51 thf(f347,plain,(
% 1.76/1.51 ($true = $false) | (~spl0_6 | ~spl0_9)),
% 1.76/1.51 inference(superposition,[status(thm)],[f138,f322])).
% 1.76/1.51 thf(f322,plain,(
% 1.76/1.51 ( ! [X0 : a] : (((sK4 @ X0) = $true)) ) | (~spl0_6 | ~spl0_9)),
% 1.76/1.51 inference(trivial_inequality_removal,[status(thm)],[f321])).
% 1.76/1.51 thf(f321,plain,(
% 1.76/1.51 ( ! [X0 : a] : (($true = $false) | ((sK4 @ X0) = $true)) ) | (~spl0_6 | ~spl0_9)),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f320])).
% 1.76/1.51 thf(f320,plain,(
% 1.76/1.51 ( ! [X0 : a] : (((sK4 @ X0) = $true) | (((^[Y0 : a]: ($true)) @ X0) = $false)) ) | (~spl0_6 | ~spl0_9)),
% 1.76/1.51 inference(trivial_inequality_removal,[status(thm)],[f306])).
% 1.76/1.51 thf(f306,plain,(
% 1.76/1.51 ( ! [X0 : a] : (((sK4 @ X0) = $true) | ($true = $false) | (((^[Y0 : a]: ($true)) @ X0) = $false)) ) | (~spl0_6 | ~spl0_9)),
% 1.76/1.51 inference(superposition,[status(thm)],[f282,f153])).
% 1.76/1.51 thf(f153,plain,(
% 1.76/1.51 ( ! [X2 : a > $o,X1 : a] : (((sK7 @ X2) = $false) | ((sK4 @ X1) = $true) | ((X2 @ X1) = $false)) ) | ~spl0_6),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f129])).
% 1.76/1.51 thf(f129,plain,(
% 1.76/1.51 ( ! [X2 : a > $o,X1 : a] : ((((X2 @ X1) & (sK7 @ X2)) = $false) | ((sK4 @ X1) = $true)) ) | ~spl0_6),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f126])).
% 1.76/1.51 thf(f126,plain,(
% 1.76/1.51 ( ! [X2 : a > $o,X1 : a] : (($false = ((^[Y0 : a > $o]: ((Y0 @ X1) & (sK7 @ Y0))) @ X2)) | ((sK4 @ X1) = $true)) ) | ~spl0_6),
% 1.76/1.51 inference(pi_clausification,[status(thm)],[f114])).
% 1.76/1.51 thf(f114,plain,(
% 1.76/1.51 ( ! [X1 : a] : (($false = (?? @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 @ X1) & (sK7 @ Y0))))) | ((sK4 @ X1) = $true)) ) | ~spl0_6),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f109])).
% 1.76/1.51 thf(f109,plain,(
% 1.76/1.51 ( ! [X1 : a] : (((sK4 @ X1) = (?? @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 @ X1) & (sK7 @ Y0)))))) ) | ~spl0_6),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f108])).
% 1.76/1.51 thf(f108,plain,(
% 1.76/1.51 ( ! [X1 : a] : ((((^[Y0 : a]: (?? @ (a > $o) @ (^[Y1 : a > $o]: ((Y1 @ Y0) & (sK7 @ Y1))))) @ X1) = (sK4 @ X1))) ) | ~spl0_6),
% 1.76/1.51 inference(argument_congruence,[status(thm)],[f104])).
% 1.76/1.51 thf(f104,plain,(
% 1.76/1.51 (sK4 = (^[Y0 : a]: (?? @ (a > $o) @ (^[Y1 : a > $o]: ((Y1 @ Y0) & (sK7 @ Y1)))))) | ~spl0_6),
% 1.76/1.51 inference(equality_proxy_clausification,[status(thm)],[f98])).
% 1.76/1.51 thf(f98,plain,(
% 1.76/1.51 ($true = ((^[Y0 : a]: (?? @ (a > $o) @ (^[Y1 : a > $o]: ((Y1 @ Y0) & (sK7 @ Y1))))) = sK4)) | ~spl0_6),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f93])).
% 1.76/1.51 thf(f93,plain,(
% 1.76/1.51 (((!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK7 @ Y0) => (((^[Y1 : a]: ($true)) = Y0) | ((^[Y1 : a]: ($false)) = Y0))))) & ((^[Y0 : a]: (?? @ (a > $o) @ (^[Y1 : a > $o]: ((Y1 @ Y0) & (sK7 @ Y1))))) = sK4)) = $true) | ~spl0_6),
% 1.76/1.51 inference(not_proxy_clausification,[status(thm)],[f91])).
% 1.76/1.51 thf(f91,plain,(
% 1.76/1.51 ($false = (~ ((!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK7 @ Y0) => (((^[Y1 : a]: ($true)) = Y0) | ((^[Y1 : a]: ($false)) = Y0))))) & ((^[Y0 : a]: (?? @ (a > $o) @ (^[Y1 : a > $o]: ((Y1 @ Y0) & (sK7 @ Y1))))) = sK4)))) | ~spl0_6),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f90])).
% 1.76/1.51 thf(f90,plain,(
% 1.76/1.51 ($false = ((^[Y0 : (a > $o) > $o]: (~ ((!! @ (a > $o) @ (^[Y1 : a > $o]: ((Y0 @ Y1) => (((^[Y2 : a]: ($true)) = Y1) | ((^[Y2 : a]: ($false)) = Y1))))) & ((^[Y1 : a]: (?? @ (a > $o) @ (^[Y2 : a > $o]: ((Y2 @ Y1) & (Y0 @ Y2))))) = sK4)))) @ sK7)) | ~spl0_6),
% 1.76/1.51 inference(sigma_clausification,[status(thm)],[f82])).
% 1.76/1.51 thf(f82,plain,(
% 1.76/1.51 ($false = (!! @ ((a > $o) > $o) @ (^[Y0 : (a > $o) > $o]: (~ ((!! @ (a > $o) @ (^[Y1 : a > $o]: ((Y0 @ Y1) => (((^[Y2 : a]: ($true)) = Y1) | ((^[Y2 : a]: ($false)) = Y1))))) & ((^[Y1 : a]: (?? @ (a > $o) @ (^[Y2 : a > $o]: ((Y2 @ Y1) & (Y0 @ Y2))))) = sK4)))))) | ~spl0_6),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f81])).
% 1.76/1.51 thf(f81,plain,(
% 1.76/1.51 ($false = (!! @ ((a > $o) > $o) @ (^[Y0 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y1 : a > $o]: ((Y0 @ Y1) => (((^[Y2 : a]: ($true)) = Y1) | ((^[Y2 : a]: ($false)) = Y1))))) & ((^[Y1 : a]: (?? @ (a > $o) @ (^[Y2 : a > $o]: ((Y2 @ Y1) & (Y0 @ Y2))))) = sK4)) => $false)))) | ~spl0_6),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f74,f80])).
% 1.76/1.51 thf(f282,plain,(
% 1.76/1.51 ($true = (sK7 @ (^[Y0 : a]: ($true)))) | ~spl0_9),
% 1.76/1.51 inference(avatar_component_clause,[status(thm)],[f281])).
% 1.76/1.51 thf(f281,definition,(
% 1.76/1.51 spl0_9 <=> ($true = (sK7 @ (^[Y0 : a]: ($true))))),
% 1.76/1.51 introduced(definition,[new_symbols(naming,[spl0_9])],[avatar_definition])).
% 1.76/1.51 thf(f138,plain,(
% 1.76/1.51 ($false = (sK4 @ sK6)) | ~spl0_6),
% 1.76/1.51 inference(trivial_inequality_removal,[status(thm)],[f135])).
% 1.76/1.51 thf(f135,plain,(
% 1.76/1.51 ($true != $true) | ($false = (sK4 @ sK6)) | ~spl0_6),
% 1.76/1.51 inference(superposition,[status(thm)],[f89,f127])).
% 1.76/1.51 thf(f127,plain,(
% 1.76/1.51 ( ! [X0 : a] : (((sK4 @ X0) = $true) | ((sK4 @ X0) = $false)) ) | ~spl0_6),
% 1.76/1.51 inference(superposition,[status(thm)],[f114,f109])).
% 1.76/1.51 thf(f89,plain,(
% 1.76/1.51 ($true != (sK4 @ sK6)) | ~spl0_6),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f88])).
% 1.76/1.51 thf(f88,plain,(
% 1.76/1.51 (((^[Y0 : a]: ($true)) @ sK6) != (sK4 @ sK6)) | ~spl0_6),
% 1.76/1.51 inference(negative_extensionality,[status(thm)],[f87])).
% 1.76/1.51 thf(f87,plain,(
% 1.76/1.51 (sK4 != (^[Y0 : a]: ($true))) | ~spl0_6),
% 1.76/1.51 inference(equality_proxy_clausification,[status(thm)],[f86])).
% 1.76/1.51 thf(f86,plain,(
% 1.76/1.51 ((sK4 = (^[Y0 : a]: ($true))) = $false) | ~spl0_6),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f85])).
% 1.76/1.51 thf(f85,plain,(
% 1.76/1.51 (($false | (sK4 = (^[Y0 : a]: ($true)))) = $false) | ~spl0_6),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f80,f84])).
% 1.76/1.51 thf(f304,plain,(
% 1.76/1.51 spl0_10 | ~spl0_6 | ~spl0_8),
% 1.76/1.51 inference(avatar_split_clause,[status(thm)],[f293,f277,f54,f298])).
% 1.76/1.51 thf(f277,definition,(
% 1.76/1.51 spl0_8 <=> ! [X0 : a] : (((sK4 @ X0) = $false) | ((sK9 @ X0) = (^[Y0 : a]: ($false))))),
% 1.76/1.51 introduced(definition,[new_symbols(naming,[spl0_8])],[avatar_definition])).
% 1.76/1.51 thf(f293,plain,(
% 1.76/1.51 ( ! [X0 : a] : (((sK4 @ X0) = $false)) ) | (~spl0_6 | ~spl0_8)),
% 1.76/1.51 inference(trivial_inequality_removal,[status(thm)],[f292])).
% 1.76/1.51 thf(f292,plain,(
% 1.76/1.51 ( ! [X0 : a] : (((sK4 @ X0) = $false) | ($true = $false)) ) | (~spl0_6 | ~spl0_8)),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f291])).
% 1.76/1.51 thf(f291,plain,(
% 1.76/1.51 ( ! [X0 : a] : (((sK4 @ X0) = $false) | (($false & (sK7 @ (^[Y0 : a]: ($false)))) = $true)) ) | (~spl0_6 | ~spl0_8)),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f290])).
% 1.76/1.51 thf(f290,plain,(
% 1.76/1.51 ( ! [X0 : a] : (((((^[Y0 : a]: ($false)) @ X0) & (sK7 @ (^[Y0 : a]: ($false)))) = $true) | ((sK4 @ X0) = $false)) ) | (~spl0_6 | ~spl0_8)),
% 1.76/1.51 inference(duplicate_literal_removal,[status(thm)],[f287])).
% 1.76/1.51 thf(f287,plain,(
% 1.76/1.51 ( ! [X0 : a] : (((sK4 @ X0) = $false) | ((((^[Y0 : a]: ($false)) @ X0) & (sK7 @ (^[Y0 : a]: ($false)))) = $true) | ((sK4 @ X0) = $false)) ) | (~spl0_6 | ~spl0_8)),
% 1.76/1.51 inference(superposition,[status(thm)],[f181,f278])).
% 1.76/1.51 thf(f278,plain,(
% 1.76/1.51 ( ! [X0 : a] : (((sK9 @ X0) = (^[Y0 : a]: ($false))) | ((sK4 @ X0) = $false)) ) | ~spl0_8),
% 1.76/1.51 inference(avatar_component_clause,[status(thm)],[f277])).
% 1.76/1.51 thf(f181,plain,(
% 1.76/1.51 ( ! [X1 : a] : (($true = ((sK9 @ X1 @ X1) & (sK7 @ (sK9 @ X1)))) | ((sK4 @ X1) = $false)) ) | ~spl0_6),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f176])).
% 1.76/1.51 thf(f176,plain,(
% 1.76/1.51 ( ! [X1 : a] : (($true = ((^[Y0 : a > $o]: ((Y0 @ X1) & (sK7 @ Y0))) @ (sK9 @ X1))) | ((sK4 @ X1) = $false)) ) | ~spl0_6),
% 1.76/1.51 inference(sigma_clausification,[status(thm)],[f115])).
% 1.76/1.51 thf(f115,plain,(
% 1.76/1.51 ( ! [X1 : a] : (($true = (?? @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 @ X1) & (sK7 @ Y0))))) | ((sK4 @ X1) = $false)) ) | ~spl0_6),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f109])).
% 1.76/1.51 thf(f284,plain,(
% 1.76/1.51 spl0_8 | spl0_9 | ~spl0_6),
% 1.76/1.51 inference(avatar_split_clause,[status(thm)],[f268,f54,f281,f277])).
% 1.76/1.51 thf(f268,plain,(
% 1.76/1.51 ( ! [X0 : a] : (((sK4 @ X0) = $false) | ((sK9 @ X0) = (^[Y0 : a]: ($false))) | ($true = (sK7 @ (^[Y0 : a]: ($true))))) ) | ~spl0_6),
% 1.76/1.51 inference(duplicate_literal_removal,[status(thm)],[f266])).
% 1.76/1.51 thf(f266,plain,(
% 1.76/1.51 ( ! [X0 : a] : (($true = (sK7 @ (^[Y0 : a]: ($true)))) | ((sK4 @ X0) = $false) | ((sK4 @ X0) = $false) | ((sK9 @ X0) = (^[Y0 : a]: ($false)))) ) | ~spl0_6),
% 1.76/1.51 inference(superposition,[status(thm)],[f193,f201])).
% 1.76/1.51 thf(f201,plain,(
% 1.76/1.51 ( ! [X0 : a] : (((^[Y0 : a]: ($true)) = (sK9 @ X0)) | ((sK9 @ X0) = (^[Y0 : a]: ($false))) | ((sK4 @ X0) = $false)) ) | ~spl0_6),
% 1.76/1.51 inference(trivial_inequality_removal,[status(thm)],[f200])).
% 1.76/1.51 thf(f200,plain,(
% 1.76/1.51 ( ! [X0 : a] : (((sK9 @ X0) = (^[Y0 : a]: ($false))) | ((sK4 @ X0) = $false) | ((^[Y0 : a]: ($true)) = (sK9 @ X0)) | ($true = $false)) ) | ~spl0_6),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f195])).
% 1.76/1.51 thf(f195,plain,(
% 1.76/1.51 ( ! [X0 : a] : (((sK9 @ X0) = (^[Y0 : a]: ($false))) | ((^[Y0 : a]: ($true)) = (sK9 @ X0)) | ((sK4 @ X0) = $false) | ($true = ((sK9 @ X0 @ X0) & $false))) ) | ~spl0_6),
% 1.76/1.51 inference(superposition,[status(thm)],[f181,f158])).
% 1.76/1.51 thf(f158,plain,(
% 1.76/1.51 ( ! [X1 : a > $o] : (($false = (sK7 @ X1)) | ((^[Y0 : a]: ($true)) = X1) | ((^[Y0 : a]: ($false)) = X1)) ) | ~spl0_6),
% 1.76/1.51 inference(equality_proxy_clausification,[status(thm)],[f143])).
% 1.76/1.51 thf(f143,plain,(
% 1.76/1.51 ( ! [X1 : a > $o] : (($true = ((^[Y0 : a]: ($false)) = X1)) | ((^[Y0 : a]: ($true)) = X1) | ($false = (sK7 @ X1))) ) | ~spl0_6),
% 1.76/1.51 inference(equality_proxy_clausification,[status(thm)],[f130])).
% 1.76/1.51 thf(f130,plain,(
% 1.76/1.51 ( ! [X1 : a > $o] : (($true = ((^[Y0 : a]: ($true)) = X1)) | ($true = ((^[Y0 : a]: ($false)) = X1)) | ($false = (sK7 @ X1))) ) | ~spl0_6),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f107])).
% 1.76/1.51 thf(f107,plain,(
% 1.76/1.51 ( ! [X1 : a > $o] : (((((^[Y0 : a]: ($true)) = X1) | ((^[Y0 : a]: ($false)) = X1)) = $true) | ($false = (sK7 @ X1))) ) | ~spl0_6),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f103])).
% 1.76/1.51 thf(f103,plain,(
% 1.76/1.51 ( ! [X1 : a > $o] : ((((sK7 @ X1) => (((^[Y0 : a]: ($true)) = X1) | ((^[Y0 : a]: ($false)) = X1))) = $true)) ) | ~spl0_6),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f102])).
% 1.76/1.51 thf(f102,plain,(
% 1.76/1.51 ( ! [X1 : a > $o] : (($true = ((^[Y0 : a > $o]: ((sK7 @ Y0) => (((^[Y1 : a]: ($true)) = Y0) | ((^[Y1 : a]: ($false)) = Y0)))) @ X1))) ) | ~spl0_6),
% 1.76/1.51 inference(pi_clausification,[status(thm)],[f101])).
% 1.76/1.51 thf(f101,plain,(
% 1.76/1.51 ($true = (!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK7 @ Y0) => (((^[Y1 : a]: ($true)) = Y0) | ((^[Y1 : a]: ($false)) = Y0)))))) | ~spl0_6),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f100])).
% 1.76/1.51 thf(f100,plain,(
% 1.76/1.51 (((!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK7 @ Y0) => (((^[Y1 : a]: ($true)) = Y0) | ((^[Y1 : a]: ($false)) = Y0))))) & $true) = $true) | ~spl0_6),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f93,f98])).
% 1.76/1.51 thf(f193,plain,(
% 1.76/1.51 ( ! [X1 : a] : (($true = (sK7 @ (sK9 @ X1))) | ((sK4 @ X1) = $false)) ) | ~spl0_6),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f181])).
% 1.76/1.51 thf(f69,plain,(
% 1.76/1.51 ~spl0_5),
% 1.76/1.51 inference(avatar_contradiction_clause,[status(thm)],[f68])).
% 1.76/1.51 thf(f68,plain,(
% 1.76/1.51 $false | ~spl0_5),
% 1.76/1.51 inference(trivial_inequality_removal,[status(thm)],[f67])).
% 1.76/1.51 thf(f67,plain,(
% 1.76/1.51 ($true = $false) | ~spl0_5),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f66])).
% 1.76/1.51 thf(f66,plain,(
% 1.76/1.51 (($true | ((^[Y0 : a]: ($false)) = sK3)) = $false) | ~spl0_5),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f61,f62])).
% 1.76/1.51 thf(f62,plain,(
% 1.76/1.51 ((sK3 = (^[Y0 : a]: ($true))) = $true) | ~spl0_5),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f60])).
% 1.76/1.51 thf(f60,plain,(
% 1.76/1.51 ($false = ((sK3 = (^[Y0 : a]: ($true))) => ((sK3 = (^[Y0 : a]: ($true))) | ((^[Y0 : a]: ($false)) = sK3)))) | ~spl0_5),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f59])).
% 1.76/1.51 thf(f59,plain,(
% 1.76/1.51 ($false = ((^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($true))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0)))) @ sK3)) | ~spl0_5),
% 1.76/1.51 inference(sigma_clausification,[status(thm)],[f52])).
% 1.76/1.51 thf(f52,plain,(
% 1.76/1.51 ($false = (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($true))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0)))))) | ~spl0_5),
% 1.76/1.51 inference(avatar_component_clause,[status(thm)],[f51])).
% 1.76/1.51 thf(f51,definition,(
% 1.76/1.51 spl0_5 <=> ($false = (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($true))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0))))))),
% 1.76/1.51 introduced(definition,[new_symbols(naming,[spl0_5])],[avatar_definition])).
% 1.76/1.51 thf(f61,plain,(
% 1.76/1.51 ($false = ((sK3 = (^[Y0 : a]: ($true))) | ((^[Y0 : a]: ($false)) = sK3))) | ~spl0_5),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f60])).
% 1.76/1.51 thf(f56,plain,(
% 1.76/1.51 spl0_5 | spl0_6 | ~spl0_4),
% 1.76/1.51 inference(avatar_split_clause,[status(thm)],[f49,f26,f54,f51])).
% 1.76/1.51 thf(f26,definition,(
% 1.76/1.51 spl0_4 <=> ($false = ((!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ ((a > $o) > $o) @ (^[Y1 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y1 @ Y2) => (((^[Y3 : a]: ($true)) = Y2) | ((^[Y3 : a]: ($false)) = Y2))))) & ((^[Y2 : a]: (?? @ (a > $o) @ (^[Y3 : a > $o]: ((Y3 @ Y2) & (Y1 @ Y3))))) = Y0)) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: ($true))))))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($true))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0)))))))),
% 1.76/1.51 introduced(definition,[new_symbols(naming,[spl0_4])],[avatar_definition])).
% 1.76/1.51 thf(f49,plain,(
% 1.76/1.51 ($false = (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($true))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0)))))) | ($false = (!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ ((a > $o) > $o) @ (^[Y1 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y1 @ Y2) => (((^[Y3 : a]: ($true)) = Y2) | ((^[Y3 : a]: ($false)) = Y2))))) & ((^[Y2 : a]: (?? @ (a > $o) @ (^[Y3 : a > $o]: ((Y3 @ Y2) & (Y1 @ Y3))))) = Y0)) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: ($true)))))))))) | ~spl0_4),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f27])).
% 1.76/1.51 thf(f27,plain,(
% 1.76/1.51 ($false = ((!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ ((a > $o) > $o) @ (^[Y1 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y1 @ Y2) => (((^[Y3 : a]: ($true)) = Y2) | ((^[Y3 : a]: ($false)) = Y2))))) & ((^[Y2 : a]: (?? @ (a > $o) @ (^[Y3 : a > $o]: ((Y3 @ Y2) & (Y1 @ Y3))))) = Y0)) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: ($true))))))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($true))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0))))))) | ~spl0_4),
% 1.76/1.51 inference(avatar_component_clause,[status(thm)],[f26])).
% 1.76/1.51 thf(f45,plain,(
% 1.76/1.51 ~spl0_3),
% 1.76/1.51 inference(avatar_contradiction_clause,[status(thm)],[f44])).
% 1.76/1.51 thf(f44,plain,(
% 1.76/1.51 $false | ~spl0_3),
% 1.76/1.51 inference(trivial_inequality_removal,[status(thm)],[f43])).
% 1.76/1.51 thf(f43,plain,(
% 1.76/1.51 ($true = $false) | ~spl0_3),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f42])).
% 1.76/1.51 thf(f42,plain,(
% 1.76/1.51 ($false = ((sK2 = (^[Y0 : a]: ($true))) | $true)) | ~spl0_3),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f41])).
% 1.76/1.51 thf(f41,plain,(
% 1.76/1.51 ($false = ((sK2 = (^[Y0 : a]: ($true))) | (sK2 = sK2))) | ~spl0_3),
% 1.76/1.51 inference(backward_demodulation,[status(thm)],[f33,f39])).
% 1.76/1.51 thf(f39,plain,(
% 1.76/1.51 ((^[Y0 : a]: ($false)) = sK2) | ~spl0_3),
% 1.76/1.51 inference(equality_proxy_clausification,[status(thm)],[f34])).
% 1.76/1.51 thf(f34,plain,(
% 1.76/1.51 ($true = (sK2 = (^[Y0 : a]: ($false)))) | ~spl0_3),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f32])).
% 1.76/1.51 thf(f32,plain,(
% 1.76/1.51 (((sK2 = (^[Y0 : a]: ($false))) => ((sK2 = (^[Y0 : a]: ($true))) | ((^[Y0 : a]: ($false)) = sK2))) = $false) | ~spl0_3),
% 1.76/1.51 inference(beta_eta_normalization,[status(thm)],[f31])).
% 1.76/1.51 thf(f31,plain,(
% 1.76/1.51 (((^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($false))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0)))) @ sK2) = $false) | ~spl0_3),
% 1.76/1.51 inference(sigma_clausification,[status(thm)],[f24])).
% 1.76/1.51 thf(f24,plain,(
% 1.76/1.51 ($false = (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($false))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0)))))) | ~spl0_3),
% 1.76/1.51 inference(avatar_component_clause,[status(thm)],[f23])).
% 1.76/1.51 thf(f23,definition,(
% 1.76/1.51 spl0_3 <=> ($false = (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($false))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0))))))),
% 1.76/1.51 introduced(definition,[new_symbols(naming,[spl0_3])],[avatar_definition])).
% 1.76/1.51 thf(f33,plain,(
% 1.76/1.51 (((sK2 = (^[Y0 : a]: ($true))) | ((^[Y0 : a]: ($false)) = sK2)) = $false) | ~spl0_3),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f32])).
% 1.76/1.51 thf(f28,plain,(
% 1.76/1.51 spl0_3 | spl0_4 | ~spl0_2),
% 1.76/1.51 inference(avatar_split_clause,[status(thm)],[f21,f16,f26,f23])).
% 1.76/1.51 thf(f16,definition,(
% 1.76/1.51 spl0_2 <=> ($false = (((!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ ((a > $o) > $o) @ (^[Y1 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y1 @ Y2) => (((^[Y3 : a]: ($true)) = Y2) | ((^[Y3 : a]: ($false)) = Y2))))) & ((^[Y2 : a]: (?? @ (a > $o) @ (^[Y3 : a > $o]: ((Y3 @ Y2) & (Y1 @ Y3))))) = Y0)) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: ($true))))))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($true))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0)))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($false))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0)))))))),
% 1.76/1.51 introduced(definition,[new_symbols(naming,[spl0_2])],[avatar_definition])).
% 1.76/1.51 thf(f21,plain,(
% 1.76/1.51 ($false = ((!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ ((a > $o) > $o) @ (^[Y1 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y1 @ Y2) => (((^[Y3 : a]: ($true)) = Y2) | ((^[Y3 : a]: ($false)) = Y2))))) & ((^[Y2 : a]: (?? @ (a > $o) @ (^[Y3 : a > $o]: ((Y3 @ Y2) & (Y1 @ Y3))))) = Y0)) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: ($true))))))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($true))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0))))))) | ($false = (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($false))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0)))))) | ~spl0_2),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f17])).
% 1.76/1.51 thf(f17,plain,(
% 1.76/1.51 ($false = (((!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ ((a > $o) > $o) @ (^[Y1 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y1 @ Y2) => (((^[Y3 : a]: ($true)) = Y2) | ((^[Y3 : a]: ($false)) = Y2))))) & ((^[Y2 : a]: (?? @ (a > $o) @ (^[Y3 : a > $o]: ((Y3 @ Y2) & (Y1 @ Y3))))) = Y0)) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: ($true))))))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($true))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0)))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($false))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0))))))) | ~spl0_2),
% 1.76/1.51 inference(avatar_component_clause,[status(thm)],[f16])).
% 1.76/1.51 thf(f18,plain,(
% 1.76/1.51 spl0_1 | spl0_2),
% 1.76/1.51 inference(avatar_split_clause,[status(thm)],[f11,f16,f13])).
% 1.76/1.51 thf(f11,plain,(
% 1.76/1.51 ($false = (((!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ ((a > $o) > $o) @ (^[Y1 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y1 @ Y2) => (((^[Y3 : a]: ($true)) = Y2) | ((^[Y3 : a]: ($false)) = Y2))))) & ((^[Y2 : a]: (?? @ (a > $o) @ (^[Y3 : a > $o]: ((Y3 @ Y2) & (Y1 @ Y3))))) = Y0)) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: ($true))))))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($true))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0)))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($false))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0))))))) | ((!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ (a > $o) @ (^[Y1 : a > $o]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((((((^[Y3 : a]: ($true)) = Y0) | (Y0 = (^[Y3 : a]: ($false)))) & ((^[Y3 : a]: ((Y2 @ Y3) & (Y0 @ Y3))) = Y1)) & ((Y2 = (^[Y3 : a]: ($true))) | ((^[Y3 : a]: ($false)) = Y2))) => ((Y1 = (^[Y3 : a]: ($false))) | (Y1 = (^[Y3 : a]: ($true))))))))))) = $false)),
% 1.76/1.51 inference(binary_proxy_clausification,[status(thm)],[f8])).
% 1.76/1.51 thf(f8,plain,(
% 1.76/1.51 ($false = ((((!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ ((a > $o) > $o) @ (^[Y1 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y1 @ Y2) => (((^[Y3 : a]: ($true)) = Y2) | ((^[Y3 : a]: ($false)) = Y2))))) & ((^[Y2 : a]: (?? @ (a > $o) @ (^[Y3 : a > $o]: ((Y3 @ Y2) & (Y1 @ Y3))))) = Y0)) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: ($true))))))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($true))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0)))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($false))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0)))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ (a > $o) @ (^[Y1 : a > $o]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((((((^[Y3 : a]: ($true)) = Y0) | (Y0 = (^[Y3 : a]: ($false)))) & ((^[Y3 : a]: ((Y2 @ Y3) & (Y0 @ Y3))) = Y1)) & ((Y2 = (^[Y3 : a]: ($true))) | ((^[Y3 : a]: ($false)) = Y2))) => ((Y1 = (^[Y3 : a]: ($false))) | (Y1 = (^[Y3 : a]: ($true)))))))))))))),
% 1.76/1.51 inference(not_proxy_clausification,[status(thm)],[f7])).
% 1.76/1.51 thf(f7,plain,(
% 1.76/1.51 ((~ ((((!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ ((a > $o) > $o) @ (^[Y1 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y1 @ Y2) => (((^[Y3 : a]: ($true)) = Y2) | ((^[Y3 : a]: ($false)) = Y2))))) & ((^[Y2 : a]: (?? @ (a > $o) @ (^[Y3 : a > $o]: ((Y3 @ Y2) & (Y1 @ Y3))))) = Y0)) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: ($true))))))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($true))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0)))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($false))) => ((Y0 = (^[Y1 : a]: ($true))) | ((^[Y1 : a]: ($false)) = Y0)))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ (a > $o) @ (^[Y1 : a > $o]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((((((^[Y3 : a]: ($true)) = Y0) | (Y0 = (^[Y3 : a]: ($false)))) & ((^[Y3 : a]: ((Y2 @ Y3) & (Y0 @ Y3))) = Y1)) & ((Y2 = (^[Y3 : a]: ($true))) | ((^[Y3 : a]: ($false)) = Y2))) => ((Y1 = (^[Y3 : a]: ($false))) | (Y1 = (^[Y3 : a]: ($true))))))))))))) = $true)),
% 1.76/1.51 inference(boolean_simplification,[status(thm)],[f6])).
% 1.76/1.51 thf(f6,plain,(
% 1.76/1.51 ((~ ((((!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ ((a > $o) > $o) @ (^[Y1 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y1 @ Y2) => (((^[Y3 : a]: (~ $false)) = Y2) | ((^[Y3 : a]: ($false)) = Y2))))) & ((^[Y2 : a]: (?? @ (a > $o) @ (^[Y3 : a > $o]: ((Y3 @ Y2) & (Y1 @ Y3))))) = Y0)) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: (~ $false))))))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: (~ $false))) => ((Y0 = (^[Y1 : a]: (~ $false))) | ((^[Y1 : a]: ($false)) = Y0)))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($false))) => ((Y0 = (^[Y1 : a]: (~ $false))) | ((^[Y1 : a]: ($false)) = Y0)))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ (a > $o) @ (^[Y1 : a > $o]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((((((^[Y3 : a]: (~ $false)) = Y0) | (Y0 = (^[Y3 : a]: ($false)))) & ((^[Y3 : a]: ((Y2 @ Y3) & (Y0 @ Y3))) = Y1)) & ((Y2 = (^[Y3 : a]: (~ $false))) | ((^[Y3 : a]: ($false)) = Y2))) => ((Y1 = (^[Y3 : a]: ($false))) | (Y1 = (^[Y3 : a]: (~ $false))))))))))))) = $true)),
% 1.76/1.51 inference(cnf_transformation,[status(thm)],[f5])).
% 1.76/1.51 thf(f5,plain,(
% 1.76/1.51 ((~ ((((!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ ((a > $o) > $o) @ (^[Y1 : (a > $o) > $o]: (((!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y1 @ Y2) => (((^[Y3 : a]: (~ $false)) = Y2) | ((^[Y3 : a]: ($false)) = Y2))))) & ((^[Y2 : a]: (?? @ (a > $o) @ (^[Y3 : a > $o]: ((Y3 @ Y2) & (Y1 @ Y3))))) = Y0)) => ((Y0 = (^[Y2 : a]: ($false))) | (Y0 = (^[Y2 : a]: (~ $false))))))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: (~ $false))) => ((Y0 = (^[Y1 : a]: (~ $false))) | ((^[Y1 : a]: ($false)) = Y0)))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((Y0 = (^[Y1 : a]: ($false))) => ((Y0 = (^[Y1 : a]: (~ $false))) | ((^[Y1 : a]: ($false)) = Y0)))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: (!! @ (a > $o) @ (^[Y1 : a > $o]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((((((^[Y3 : a]: (~ $false)) = Y0) | (Y0 = (^[Y3 : a]: ($false)))) & ((^[Y3 : a]: ((Y2 @ Y3) & (Y0 @ Y3))) = Y1)) & ((Y2 = (^[Y3 : a]: (~ $false))) | ((^[Y3 : a]: ($false)) = Y2))) => ((Y1 = (^[Y3 : a]: ($false))) | (Y1 = (^[Y3 : a]: (~ $false))))))))))))) = $true)),
% 1.76/1.51 inference(fool_elimination,[status(thm)],[f4])).
% 1.76/1.51 thf(f4,plain,(
% 1.76/1.51 ~(! [X0 : a > $o,X1 : a > $o,X2 : a > $o] : (((((^[X3 : a] : ($false)) = X0) | (X0 = (^[X4 : a] : (~$false)))) & ((^[X5 : a] : ((X2 @ X5) & (X0 @ X5))) = X1) & ((X2 = (^[X6 : a] : ($false))) | ((^[X7 : a] : (~$false)) = X2))) => ((X1 = (^[X8 : a] : (~$false))) | (X1 = (^[X9 : a] : ($false))))) & ! [X10 : a > $o] : ((X10 = (^[X11 : a] : ($false))) => (((^[X12 : a] : ($false)) = X10) | (X10 = (^[X13 : a] : (~$false))))) & ! [X14 : a > $o] : ((X14 = (^[X15 : a] : (~$false))) => (((^[X16 : a] : ($false)) = X14) | (X14 = (^[X17 : a] : (~$false))))) & ! [X18 : (a > $o) > $o,X19 : a > $o] : ((((^[X20 : a] : (? [X21 : a > $o] : ((X18 @ X21) & (X21 @ X20)))) = X19) & ! [X22 : a > $o] : ((X18 @ X22) => (((^[X23 : a] : ($false)) = X22) | ((^[X24 : a] : (~$false)) = X22)))) => ((X19 = (^[X25 : a] : (~$false))) | (X19 = (^[X26 : a] : ($false))))))),
% 1.76/1.51 inference(rectify,[status(thm)],[f2])).
% 1.76/1.51 thf(f2,negated_conjecture,(
% 1.76/1.51 ~(! [X6 : a > $o,X4 : a > $o,X5 : a > $o] : (((((^[X2 : a] : ($false)) = X6) | (X6 = (^[X2 : a] : (~$false)))) & ((^[X1 : a] : ((X5 @ X1) & (X6 @ X1))) = X4) & ((X5 = (^[X2 : a] : ($false))) | ((^[X2 : a] : (~$false)) = X5))) => ((X4 = (^[X2 : a] : (~$false))) | (X4 = (^[X2 : a] : ($false))))) & ! [X0 : a > $o] : ((X0 = (^[X1 : a] : ($false))) => (((^[X2 : a] : ($false)) = X0) | (X0 = (^[X2 : a] : (~$false))))) & ! [X0 : a > $o] : ((X0 = (^[X1 : a] : (~$false))) => (((^[X2 : a] : ($false)) = X0) | (X0 = (^[X2 : a] : (~$false))))) & ! [X3 : (a > $o) > $o,X0 : a > $o] : ((((^[X1 : a] : (? [X4 : a > $o] : ((X3 @ X4) & (X4 @ X1)))) = X0) & ! [X1 : a > $o] : ((X3 @ X1) => (((^[X2 : a] : ($false)) = X1) | ((^[X2 : a] : (~$false)) = X1)))) => ((X0 = (^[X2 : a] : (~$false))) | (X0 = (^[X2 : a] : ($false))))))),
% 1.76/1.51 inference(negated_conjecture,[status(cth)],[f1])).
% 1.76/1.51 thf(f1,conjecture,(
% 1.76/1.51 ! [X6 : a > $o,X4 : a > $o,X5 : a > $o] : (((((^[X2 : a] : ($false)) = X6) | (X6 = (^[X2 : a] : (~$false)))) & ((^[X1 : a] : ((X5 @ X1) & (X6 @ X1))) = X4) & ((X5 = (^[X2 : a] : ($false))) | ((^[X2 : a] : (~$false)) = X5))) => ((X4 = (^[X2 : a] : (~$false))) | (X4 = (^[X2 : a] : ($false))))) & ! [X0 : a > $o] : ((X0 = (^[X1 : a] : ($false))) => (((^[X2 : a] : ($false)) = X0) | (X0 = (^[X2 : a] : (~$false))))) & ! [X0 : a > $o] : ((X0 = (^[X1 : a] : (~$false))) => (((^[X2 : a] : ($false)) = X0) | (X0 = (^[X2 : a] : (~$false))))) & ! [X3 : (a > $o) > $o,X0 : a > $o] : ((((^[X1 : a] : (? [X4 : a > $o] : ((X3 @ X4) & (X4 @ X1)))) = X0) & ! [X1 : a > $o] : ((X3 @ X1) => (((^[X2 : a] : ($false)) = X1) | ((^[X2 : a] : (~$false)) = X1)))) => ((X0 = (^[X2 : a] : (~$false))) | (X0 = (^[X2 : a] : ($false)))))),
% 1.76/1.51 file('/export/starexec/sandbox/tmp/tmp.YfPnjdhobS/DTF2THF_19752.p',cINDISCRETE_TOPOLOGY_pme)).
% 1.76/1.51 % SZS output end Proof for DTF2THF_19752
% 1.76/1.51 % (19861)------------------------------
% 1.76/1.51 % (19861)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.51 % (19861)Termination reason: Refutation
% 1.76/1.51
% 1.76/1.51 % (19861)Memory used [KB]: 5884
% 1.76/1.51 % (19861)Time elapsed: 0.062 s
% 1.76/1.51 % (19861)Instructions burned: 94 (million)
% 1.76/1.51 % (19861)------------------------------
% 1.76/1.51 % (19861)------------------------------
% 1.76/1.51 % (19849)Success in time 0.097 s
%------------------------------------------------------------------------------