%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : ALG290^5 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Feb 25 08:37:51 AM UTC 2026
% Result : Theorem 1.70s 1.58s
% Output : Refutation 1.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 7
% Syntax : Number of formulae : 182 ( 10 unt; 0 typ; 6 def)
% Number of atoms : 1737 ( 366 equ; 0 cnn)
% Maximal formula atoms : 7 ( 9 avg)
% Number of connectives : 4661 ( 318 ~; 326 |; 421 &;2600 @)
% ( 9 <=>; 434 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 258 ( 258 >; 0 *; 0 +; 0 <<)
% Number of symbols : 37 ( 32 usr; 24 con; 0-2 aty)
% ( 370 !!; 183 ??; 0 @@+; 0 @@-)
% Number of variables : 687 ( 596 ^; 70 !; 21 ?; 687 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
a: $tType ).
thf(func_def_0,type,
a: $tType ).
thf(func_def_1,type,
cP: a > a > a ).
thf(func_def_2,type,
cG: a > $o ).
thf(func_def_3,type,
cX: a > $o ).
thf(func_def_4,type,
cR: a > a ).
thf(func_def_5,type,
cL: a > a ).
thf(func_def_6,type,
cF: a > $o ).
thf(func_def_7,type,
cZ: a ).
thf(func_def_24,type,
ph1:
!>[X0: $tType] : X0 ).
thf(func_def_25,type,
sK2: a ).
thf(func_def_26,type,
sK3: a ).
thf(func_def_27,type,
sK4: a ).
thf(func_def_28,type,
sK5: a > $o ).
thf(func_def_29,type,
sK6: a ).
thf(func_def_30,type,
sK7: a ).
thf(func_def_31,type,
sK8: a ).
thf(func_def_32,type,
sK9: a ).
thf(func_def_33,type,
sK10: a > $o ).
thf(func_def_34,type,
sK11: a > $o ).
thf(func_def_35,type,
sK12: a ).
thf(func_def_36,type,
sK13: a ).
thf(func_def_37,type,
sK14: a > $o ).
thf(func_def_38,type,
sK15: a ).
thf(func_def_39,type,
sK16: a > $o ).
thf(func_def_40,type,
sK17: a ).
thf(func_def_41,type,
sK18: a ).
thf(func_def_42,type,
sK19: a ).
thf(f1297,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[f36,f70,f227,f561,f799,f1163,f1296]) ).
thf(f1296,plain,
( ~ spl0_2
| ~ spl0_5 ),
inference(avatar_contradiction_clause,[status(thm)],[f1295]) ).
thf(f1295,plain,
( $false
| ~ spl0_2
| ~ spl0_5 ),
inference(trivial_inequality_removal,[status(thm)],[f1294]) ).
thf(f1294,plain,
( ( $false = $true )
| ~ spl0_2
| ~ spl0_5 ),
inference(boolean_simplification,[status(thm)],[f1293]) ).
thf(f1293,plain,
( ( $true = ( ~ $true ) )
| ~ spl0_2
| ~ spl0_5 ),
inference(forward_demodulation,[status(thm)],[f1291,f1292]) ).
thf(f1292,plain,
( ( ( sK5 @ sK3 )
= $true )
| ~ spl0_2
| ~ spl0_5 ),
inference(boolean_simplification,[status(thm)],[f1290]) ).
thf(f1290,plain,
( ( $true
= ( ( sK5 @ sK3 )
& $true ) )
| ~ spl0_2
| ~ spl0_5 ),
inference(backward_demodulation,[status(thm)],[f1255,f1287]) ).
thf(f1287,plain,
( ( $true
= ( !! @ a
@ ^ [Y0: a] :
( ( sK5 @ Y0 )
=> ( sK5 @ ( cL @ Y0 ) ) ) ) )
| ~ spl0_2
| ~ spl0_5 ),
inference(binary_proxy_clausification,[status(thm)],[f1255]) ).
thf(f1255,plain,
( ( ( ( sK5 @ sK3 )
& ( !! @ a
@ ^ [Y0: a] :
( ( sK5 @ Y0 )
=> ( sK5 @ ( cL @ Y0 ) ) ) ) )
= $true )
| ~ spl0_2
| ~ spl0_5 ),
inference(binary_proxy_clausification,[status(thm)],[f1222]) ).
thf(f1222,plain,
( ( ( ( ( sK5 @ sK3 )
& ( !! @ a
@ ^ [Y0: a] :
( ( sK5 @ Y0 )
=> ( sK5 @ ( cL @ Y0 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y0: a] :
( ( ( cR @ Y0 )
= sK4 )
& ( sK5 @ Y0 ) ) ) )
= $false )
| ~ spl0_2
| ~ spl0_5 ),
inference(beta_eta_normalization,[status(thm)],[f1219]) ).
thf(f1219,plain,
( ( $false
= ( ^ [Y0: a > $o] :
( ( ( Y0 @ sK3 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK4 )
& ( Y0 @ Y1 ) ) ) )
@ sK5 ) )
| ~ spl0_2
| ~ spl0_5 ),
inference(sigma_clausification,[status(thm)],[f1216]) ).
thf(f1216,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( Y0 @ sK3 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK4 )
& ( Y0 @ Y1 ) ) ) ) )
= $false )
| ~ spl0_2
| ~ spl0_5 ),
inference(not_proxy_clausification,[status(thm)],[f1191]) ).
thf(f1191,plain,
( ( $true
= ( ~ ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( Y0 @ sK3 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK4 )
& ( Y0 @ Y1 ) ) ) ) ) ) )
| ~ spl0_2
| ~ spl0_5 ),
inference(boolean_simplification,[status(thm)],[f1190]) ).
thf(f1190,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( Y0 @ sK3 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK4 )
& ( Y0 @ Y1 ) ) ) ) )
=> $false )
= $true )
| ~ spl0_2
| ~ spl0_5 ),
inference(superposition,[status(thm)],[f1168,f1184]) ).
thf(f1184,plain,
( ( ( cX @ sK4 )
= $false )
| ~ spl0_2
| ~ spl0_5 ),
inference(binary_proxy_clausification,[status(thm)],[f1178]) ).
thf(f1178,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK3 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK4 )
& ( Y0 @ Y1 ) ) ) ) )
=> ( cX @ sK4 ) )
= $false )
| ~ spl0_2
| ~ spl0_5 ),
inference(beta_eta_normalization,[status(thm)],[f1174]) ).
thf(f1174,plain,
( ( $false
= ( ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) )
& ( Y1 @ sK3 ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) )
@ sK4 ) )
| ~ spl0_2
| ~ spl0_5 ),
inference(sigma_clausification,[status(thm)],[f1170]) ).
thf(f1170,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) )
& ( Y1 @ sK3 ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
= $false )
| ~ spl0_2
| ~ spl0_5 ),
inference(boolean_simplification,[status(thm)],[f1169]) ).
thf(f1169,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) )
& ( Y1 @ sK3 ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
& $true )
= $false )
| ~ spl0_2
| ~ spl0_5 ),
inference(superposition,[status(thm)],[f855,f66]) ).
thf(f66,plain,
( ( $true
= ( cF @ ( cP @ sK3 @ sK2 ) ) )
| ~ spl0_5 ),
inference(avatar_component_clause,[status(thm)],[f65]) ).
thf(f65,definition,
( spl0_5
<=> ( $true
= ( cF @ ( cP @ sK3 @ sK2 ) ) ) ),
introduced(definition,[new_symbols(naming,[spl0_5])],[avatar_definition]) ).
thf(f855,plain,
( ! [X1: a] :
( $false
= ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) )
& ( Y1 @ X1 ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
& ( cF @ ( cP @ X1 @ sK2 ) ) ) )
| ~ spl0_2 ),
inference(beta_eta_normalization,[status(thm)],[f854]) ).
thf(f854,plain,
( ! [X1: a] :
( $false
= ( ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cF @ ( cP @ Y0 @ sK2 ) ) )
@ X1 ) )
| ~ spl0_2 ),
inference(pi_clausification,[status(thm)],[f849]) ).
thf(f849,plain,
( ( $false
= ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cF @ ( cP @ Y0 @ sK2 ) ) ) ) )
| ~ spl0_2 ),
inference(boolean_simplification,[status(thm)],[f848]) ).
thf(f848,plain,
( ( $false
= ( $false
| ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cF @ ( cP @ Y0 @ sK2 ) ) ) ) ) )
| ~ spl0_2 ),
inference(backward_demodulation,[status(thm)],[f35,f847]) ).
thf(f847,plain,
( ( $false
= ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cG @ ( cP @ Y0 @ sK2 ) ) ) ) )
| ~ spl0_2 ),
inference(binary_proxy_clausification,[status(thm)],[f35]) ).
thf(f35,plain,
( ( $false
= ( ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cG @ ( cP @ Y0 @ sK2 ) ) ) )
| ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cF @ ( cP @ Y0 @ sK2 ) ) ) ) ) )
| ~ spl0_2 ),
inference(avatar_component_clause,[status(thm)],[f34]) ).
thf(f34,definition,
( spl0_2
<=> ( $false
= ( ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cG @ ( cP @ Y0 @ sK2 ) ) ) )
| ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cF @ ( cP @ Y0 @ sK2 ) ) ) ) ) ) ),
introduced(definition,[new_symbols(naming,[spl0_2])],[avatar_definition]) ).
thf(f1168,plain,
( ! [X1: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( Y0 @ sK3 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= X1 )
& ( Y0 @ Y1 ) ) ) ) )
=> ( cX @ X1 ) )
= $true )
| ~ spl0_2
| ~ spl0_5 ),
inference(beta_eta_normalization,[status(thm)],[f1167]) ).
thf(f1167,plain,
( ! [X1: a] :
( ( ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK3 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) )
@ X1 )
= $true )
| ~ spl0_2
| ~ spl0_5 ),
inference(pi_clausification,[status(thm)],[f1166]) ).
thf(f1166,plain,
( ( $true
= ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK3 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
| ~ spl0_2
| ~ spl0_5 ),
inference(boolean_simplification,[status(thm)],[f1165]) ).
thf(f1165,plain,
( ( $true
= ( $true
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK3 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) ) )
| ~ spl0_2
| ~ spl0_5 ),
inference(boolean_simplification,[status(thm)],[f1164]) ).
thf(f1164,plain,
( ( ( ( ( cG @ ( cP @ sK3 @ sK2 ) )
| $true )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK3 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
= $true )
| ~ spl0_2
| ~ spl0_5 ),
inference(backward_demodulation,[status(thm)],[f807,f66]) ).
thf(f807,plain,
( ( $true
= ( ( ( cG @ ( cP @ sK3 @ sK2 ) )
| ( cF @ ( cP @ sK3 @ sK2 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK3 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) ) )
| ~ spl0_2 ),
inference(beta_eta_normalization,[status(thm)],[f806]) ).
thf(f806,plain,
( ( $true
= ( ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK2 ) )
| ( cF @ ( cP @ Y0 @ sK2 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) )
@ sK3 ) )
| ~ spl0_2 ),
inference(sigma_clausification,[status(thm)],[f800]) ).
thf(f800,plain,
( ( $false
!= ( ?? @ a
@ ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK2 ) )
| ( cF @ ( cP @ Y0 @ sK2 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
| ~ spl0_2 ),
inference(backward_demodulation,[status(thm)],[f20,f35]) ).
thf(f20,plain,
( ( ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cG @ ( cP @ Y0 @ sK2 ) ) ) )
| ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cF @ ( cP @ Y0 @ sK2 ) ) ) ) )
!= ( ?? @ a
@ ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK2 ) )
| ( cF @ ( cP @ Y0 @ sK2 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f19]) ).
thf(f19,plain,
( ( ^ [Y0: a] :
( ?? @ a
@ ^ [Y1: a] :
( ( ( cG @ ( cP @ Y1 @ Y0 ) )
| ( cF @ ( cP @ Y1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) )
@ sK2 )
!= ( ^ [Y0: a] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) )
& ( Y3 @ Y1 ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) )
& ( cG @ ( cP @ Y1 @ Y0 ) ) ) )
| ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) )
& ( Y3 @ Y1 ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) )
& ( cF @ ( cP @ Y1 @ Y0 ) ) ) ) )
@ sK2 ) ),
inference(negative_extensionality,[status(thm)],[f14]) ).
thf(f14,plain,
( ( ^ [Y0: a] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) )
& ( Y3 @ Y1 ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) )
& ( cG @ ( cP @ Y1 @ Y0 ) ) ) )
| ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) )
& ( Y3 @ Y1 ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) )
& ( cF @ ( cP @ Y1 @ Y0 ) ) ) ) ) )
!= ( ^ [Y0: a] :
( ?? @ a
@ ^ [Y1: a] :
( ( ( cG @ ( cP @ Y1 @ Y0 ) )
| ( cF @ ( cP @ Y1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) ) ),
inference(equality_proxy_clausification,[status(thm)],[f13]) ).
thf(f13,plain,
( ( ( ^ [Y0: a] :
( ?? @ a
@ ^ [Y1: a] :
( ( ( cG @ ( cP @ Y1 @ Y0 ) )
| ( cF @ ( cP @ Y1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) )
= ( ^ [Y0: a] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) )
& ( Y3 @ Y1 ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) )
& ( cG @ ( cP @ Y1 @ Y0 ) ) ) )
| ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) )
& ( Y3 @ Y1 ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) )
& ( cF @ ( cP @ Y1 @ Y0 ) ) ) ) ) ) )
= $false ),
inference(boolean_simplification,[status(thm)],[f12]) ).
thf(f12,plain,
( ( $true
=> ( ( ^ [Y0: a] :
( ?? @ a
@ ^ [Y1: a] :
( ( ( cG @ ( cP @ Y1 @ Y0 ) )
| ( cF @ ( cP @ Y1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) )
= ( ^ [Y0: a] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) )
& ( Y3 @ Y1 ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) )
& ( cG @ ( cP @ Y1 @ Y0 ) ) ) )
| ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) )
& ( Y3 @ Y1 ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) )
& ( cF @ ( cP @ Y1 @ Y0 ) ) ) ) ) ) ) )
= $false ),
inference(backward_demodulation,[status(thm)],[f7,f11]) ).
thf(f11,plain,
( ( ( cZ
= ( cL @ cZ ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( cL @ ( cP @ Y0 @ Y1 ) )
= Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( cZ != Y0 )
= ( ( cP @ ( cL @ Y0 ) @ ( cR @ Y0 ) )
= Y0 ) ) )
& ( cZ
= ( cR @ cZ ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( cR @ ( cP @ Y1 @ Y0 ) )
= Y0 ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
=> ( Y0 @ ( cL @ Y2 ) ) ) )
& ( Y0 @ Y1 ) ) )
=> ( Y0 @ cZ ) ) ) )
= $true ),
inference(binary_proxy_clausification,[status(thm)],[f7]) ).
thf(f7,plain,
( $false
= ( ( ( cZ
= ( cL @ cZ ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( cL @ ( cP @ Y0 @ Y1 ) )
= Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( cZ != Y0 )
= ( ( cP @ ( cL @ Y0 ) @ ( cR @ Y0 ) )
= Y0 ) ) )
& ( cZ
= ( cR @ cZ ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( cR @ ( cP @ Y1 @ Y0 ) )
= Y0 ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
=> ( Y0 @ ( cL @ Y2 ) ) ) )
& ( Y0 @ Y1 ) ) )
=> ( Y0 @ cZ ) ) ) )
=> ( ( ^ [Y0: a] :
( ?? @ a
@ ^ [Y1: a] :
( ( ( cG @ ( cP @ Y1 @ Y0 ) )
| ( cF @ ( cP @ Y1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) )
= ( ^ [Y0: a] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) )
& ( Y3 @ Y1 ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) )
& ( cG @ ( cP @ Y1 @ Y0 ) ) ) )
| ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) )
& ( Y3 @ Y1 ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) )
& ( cF @ ( cP @ Y1 @ Y0 ) ) ) ) ) ) ) ) ),
inference(not_proxy_clausification,[status(thm)],[f6]) ).
thf(f6,plain,
( $true
= ( ~ ( ( ( cZ
= ( cL @ cZ ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( cL @ ( cP @ Y0 @ Y1 ) )
= Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( cZ != Y0 )
= ( ( cP @ ( cL @ Y0 ) @ ( cR @ Y0 ) )
= Y0 ) ) )
& ( cZ
= ( cR @ cZ ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( cR @ ( cP @ Y1 @ Y0 ) )
= Y0 ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
=> ( Y0 @ ( cL @ Y2 ) ) ) )
& ( Y0 @ Y1 ) ) )
=> ( Y0 @ cZ ) ) ) )
=> ( ( ^ [Y0: a] :
( ?? @ a
@ ^ [Y1: a] :
( ( ( cG @ ( cP @ Y1 @ Y0 ) )
| ( cF @ ( cP @ Y1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) )
= ( ^ [Y0: a] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) )
& ( Y3 @ Y1 ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) )
& ( cG @ ( cP @ Y1 @ Y0 ) ) ) )
| ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) )
& ( Y3 @ Y1 ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) )
& ( cF @ ( cP @ Y1 @ Y0 ) ) ) ) ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
thf(f5,plain,
( $true
= ( ~ ( ( ( cZ
= ( cL @ cZ ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( cL @ ( cP @ Y0 @ Y1 ) )
= Y0 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( cZ != Y0 )
= ( ( cP @ ( cL @ Y0 ) @ ( cR @ Y0 ) )
= Y0 ) ) )
& ( cZ
= ( cR @ cZ ) )
& ( !! @ a
@ ^ [Y0: a] :
( !! @ a
@ ^ [Y1: a] :
( ( cR @ ( cP @ Y1 @ Y0 ) )
= Y0 ) ) )
& ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( Y0 @ Y2 )
=> ( Y0 @ ( cL @ Y2 ) ) ) )
& ( Y0 @ Y1 ) ) )
=> ( Y0 @ cZ ) ) ) )
=> ( ( ^ [Y0: a] :
( ?? @ a
@ ^ [Y1: a] :
( ( ( cG @ ( cP @ Y1 @ Y0 ) )
| ( cF @ ( cP @ Y1 @ Y0 ) ) )
& ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( Y3 @ Y1 )
& ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) ) ) ) )
= ( ^ [Y0: a] :
( ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) )
& ( Y3 @ Y1 ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) )
& ( cG @ ( cP @ Y1 @ Y0 ) ) ) )
| ( ?? @ a
@ ^ [Y1: a] :
( ( !! @ a
@ ^ [Y2: a] :
( ( !! @ ( a > $o )
@ ^ [Y3: a > $o] :
( ( ( !! @ a
@ ^ [Y4: a] :
( ( Y3 @ Y4 )
=> ( Y3 @ ( cL @ Y4 ) ) ) )
& ( Y3 @ Y1 ) )
=> ( ?? @ a
@ ^ [Y4: a] :
( ( ( cR @ Y4 )
= Y2 )
& ( Y3 @ Y4 ) ) ) ) )
=> ( cX @ Y2 ) ) )
& ( cF @ ( cP @ Y1 @ Y0 ) ) ) ) ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f4]) ).
thf(f4,plain,
~ ( ( ! [X0: a > $o] :
( ? [X1: a] :
( ( X0 @ X1 )
& ! [X2: a] :
( ( X0 @ X2 )
=> ( X0 @ ( cL @ X2 ) ) ) )
=> ( X0 @ cZ ) )
& ! [X3: a,X4: a] :
( ( cR @ ( cP @ X3 @ X4 ) )
= X4 )
& ( cZ
= ( cR @ cZ ) )
& ! [X5: a] :
( ( cZ != X5 )
<=> ( ( cP @ ( cL @ X5 ) @ ( cR @ X5 ) )
= X5 ) )
& ! [X6: a,X7: a] :
( ( cL @ ( cP @ X7 @ X6 ) )
= X7 )
& ( cZ
= ( cL @ cZ ) ) )
=> ( ( ^ [X8: a] :
? [X9: a] :
( ! [X10: a] :
( ! [X11: a > $o] :
( ( ! [X12: a] :
( ( X11 @ X12 )
=> ( X11 @ ( cL @ X12 ) ) )
& ( X11 @ X9 ) )
=> ? [X13: a] :
( ( X11 @ X13 )
& ( ( cR @ X13 )
= X10 ) ) )
=> ( cX @ X10 ) )
& ( ( cF @ ( cP @ X9 @ X8 ) )
| ( cG @ ( cP @ X9 @ X8 ) ) ) ) )
= ( ^ [X14: a] :
( ? [X15: a] :
( ( cF @ ( cP @ X15 @ X14 ) )
& ! [X16: a] :
( ! [X17: a > $o] :
( ( ( X17 @ X15 )
& ! [X18: a] :
( ( X17 @ X18 )
=> ( X17 @ ( cL @ X18 ) ) ) )
=> ? [X19: a] :
( ( X17 @ X19 )
& ( ( cR @ X19 )
= X16 ) ) )
=> ( cX @ X16 ) ) )
| ? [X20: a] :
( ( cG @ ( cP @ X20 @ X14 ) )
& ! [X21: a] :
( ! [X22: a > $o] :
( ( ( X22 @ X20 )
& ! [X23: a] :
( ( X22 @ X23 )
=> ( X22 @ ( cL @ X23 ) ) ) )
=> ? [X24: a] :
( ( X22 @ X24 )
& ( ( cR @ X24 )
= X21 ) ) )
=> ( cX @ X21 ) ) ) ) ) ) ),
inference(rectify,[status(thm)],[f2]) ).
thf(f2,negated_conjecture,
~ ( ( ! [X3: a > $o] :
( ? [X2: a] :
( ( X3 @ X2 )
& ! [X4: a] :
( ( X3 @ X4 )
=> ( X3 @ ( cL @ X4 ) ) ) )
=> ( X3 @ cZ ) )
& ! [X0: a,X1: a] :
( ( cR @ ( cP @ X0 @ X1 ) )
= X1 )
& ( cZ
= ( cR @ cZ ) )
& ! [X2: a] :
( ( cZ != X2 )
<=> ( ( cP @ ( cL @ X2 ) @ ( cR @ X2 ) )
= X2 ) )
& ! [X1: a,X0: a] :
( ( cL @ ( cP @ X0 @ X1 ) )
= X0 )
& ( cZ
= ( cL @ cZ ) ) )
=> ( ( ^ [X1: a] :
? [X0: a] :
( ! [X5: a] :
( ! [X3: a > $o] :
( ( ! [X6: a] :
( ( X3 @ X6 )
=> ( X3 @ ( cL @ X6 ) ) )
& ( X3 @ X0 ) )
=> ? [X7: a] :
( ( X3 @ X7 )
& ( ( cR @ X7 )
= X5 ) ) )
=> ( cX @ X5 ) )
& ( ( cF @ ( cP @ X0 @ X1 ) )
| ( cG @ ( cP @ X0 @ X1 ) ) ) ) )
= ( ^ [X6: a] :
( ? [X0: a] :
( ( cF @ ( cP @ X0 @ X6 ) )
& ! [X8: a] :
( ! [X3: a > $o] :
( ( ( X3 @ X0 )
& ! [X9: a] :
( ( X3 @ X9 )
=> ( X3 @ ( cL @ X9 ) ) ) )
=> ? [X7: a] :
( ( X3 @ X7 )
& ( ( cR @ X7 )
= X8 ) ) )
=> ( cX @ X8 ) ) )
| ? [X0: a] :
( ( cG @ ( cP @ X0 @ X6 ) )
& ! [X10: a] :
( ! [X3: a > $o] :
( ( ( X3 @ X0 )
& ! [X9: a] :
( ( X3 @ X9 )
=> ( X3 @ ( cL @ X9 ) ) ) )
=> ? [X7: a] :
( ( X3 @ X7 )
& ( ( cR @ X7 )
= X10 ) ) )
=> ( cX @ X10 ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
thf(f1,conjecture,
( ( ! [X3: a > $o] :
( ? [X2: a] :
( ( X3 @ X2 )
& ! [X4: a] :
( ( X3 @ X4 )
=> ( X3 @ ( cL @ X4 ) ) ) )
=> ( X3 @ cZ ) )
& ! [X0: a,X1: a] :
( ( cR @ ( cP @ X0 @ X1 ) )
= X1 )
& ( cZ
= ( cR @ cZ ) )
& ! [X2: a] :
( ( cZ != X2 )
<=> ( ( cP @ ( cL @ X2 ) @ ( cR @ X2 ) )
= X2 ) )
& ! [X1: a,X0: a] :
( ( cL @ ( cP @ X0 @ X1 ) )
= X0 )
& ( cZ
= ( cL @ cZ ) ) )
=> ( ( ^ [X1: a] :
? [X0: a] :
( ! [X5: a] :
( ! [X3: a > $o] :
( ( ! [X6: a] :
( ( X3 @ X6 )
=> ( X3 @ ( cL @ X6 ) ) )
& ( X3 @ X0 ) )
=> ? [X7: a] :
( ( X3 @ X7 )
& ( ( cR @ X7 )
= X5 ) ) )
=> ( cX @ X5 ) )
& ( ( cF @ ( cP @ X0 @ X1 ) )
| ( cG @ ( cP @ X0 @ X1 ) ) ) ) )
= ( ^ [X6: a] :
( ? [X0: a] :
( ( cF @ ( cP @ X0 @ X6 ) )
& ! [X8: a] :
( ! [X3: a > $o] :
( ( ( X3 @ X0 )
& ! [X9: a] :
( ( X3 @ X9 )
=> ( X3 @ ( cL @ X9 ) ) ) )
=> ? [X7: a] :
( ( X3 @ X7 )
& ( ( cR @ X7 )
= X8 ) ) )
=> ( cX @ X8 ) ) )
| ? [X0: a] :
( ( cG @ ( cP @ X0 @ X6 ) )
& ! [X10: a] :
( ! [X3: a > $o] :
( ( ( X3 @ X0 )
& ! [X9: a] :
( ( X3 @ X9 )
=> ( X3 @ ( cL @ X9 ) ) ) )
=> ? [X7: a] :
( ( X3 @ X7 )
& ( ( cR @ X7 )
= X10 ) ) )
=> ( cX @ X10 ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.Td4sovfI6f/DTF2THF_8033.p',cPU_X2310A_pme) ).
thf(f1291,plain,
( ( ( ~ ( sK5 @ sK3 ) )
= $true )
| ~ spl0_2
| ~ spl0_5 ),
inference(boolean_simplification,[status(thm)],[f1289]) ).
thf(f1289,plain,
( ( ( ~ ( $true
& ( sK5 @ sK3 ) ) )
= $true )
| ~ spl0_2
| ~ spl0_5 ),
inference(backward_demodulation,[status(thm)],[f1263,f1287]) ).
thf(f1263,plain,
( ( ( ~ ( ( !! @ a
@ ^ [Y0: a] :
( ( sK5 @ Y0 )
=> ( sK5 @ ( cL @ Y0 ) ) ) )
& ( sK5 @ sK3 ) ) )
= $true )
| ~ spl0_2
| ~ spl0_5 ),
inference(boolean_simplification,[status(thm)],[f1261]) ).
thf(f1261,plain,
( ( $true
= ( ( ( !! @ a
@ ^ [Y0: a] :
( ( sK5 @ Y0 )
=> ( sK5 @ ( cL @ Y0 ) ) ) )
& ( sK5 @ sK3 ) )
=> $false ) )
| ~ spl0_2
| ~ spl0_5 ),
inference(superposition,[status(thm)],[f1193,f1254]) ).
thf(f1254,plain,
( ( $false
= ( ?? @ a
@ ^ [Y0: a] :
( ( ( cR @ Y0 )
= sK4 )
& ( sK5 @ Y0 ) ) ) )
| ~ spl0_2
| ~ spl0_5 ),
inference(binary_proxy_clausification,[status(thm)],[f1222]) ).
thf(f1193,plain,
( ! [X1: a > $o] :
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( X1 @ ( cL @ Y0 ) ) ) )
& ( X1 @ sK3 ) )
=> ( ?? @ a
@ ^ [Y0: a] :
( ( ( cR @ Y0 )
= sK4 )
& ( X1 @ Y0 ) ) ) )
= $true )
| ~ spl0_2
| ~ spl0_5 ),
inference(beta_eta_normalization,[status(thm)],[f1192]) ).
thf(f1192,plain,
( ! [X1: a > $o] :
( $true
= ( ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK3 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK4 )
& ( Y0 @ Y1 ) ) ) )
@ X1 ) )
| ~ spl0_2
| ~ spl0_5 ),
inference(pi_clausification,[status(thm)],[f1185]) ).
thf(f1185,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK3 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK4 )
& ( Y0 @ Y1 ) ) ) ) )
= $true )
| ~ spl0_2
| ~ spl0_5 ),
inference(binary_proxy_clausification,[status(thm)],[f1178]) ).
thf(f1163,plain,
( ~ spl0_2
| ~ spl0_6 ),
inference(avatar_contradiction_clause,[status(thm)],[f1162]) ).
thf(f1162,plain,
( $false
| ~ spl0_2
| ~ spl0_6 ),
inference(trivial_inequality_removal,[status(thm)],[f1161]) ).
thf(f1161,plain,
( ( $false = $true )
| ~ spl0_2
| ~ spl0_6 ),
inference(boolean_simplification,[status(thm)],[f1160]) ).
thf(f1160,plain,
( ( $true = ( ~ $true ) )
| ~ spl0_2
| ~ spl0_6 ),
inference(backward_demodulation,[status(thm)],[f1159,f1158]) ).
thf(f1158,plain,
( ( $true
= ( !! @ a
@ ^ [Y0: a] :
( ( sK5 @ Y0 )
=> ( sK5 @ ( cL @ Y0 ) ) ) ) )
| ~ spl0_2
| ~ spl0_6 ),
inference(boolean_simplification,[status(thm)],[f1157]) ).
thf(f1157,plain,
( ( $true
= ( $true
& ( !! @ a
@ ^ [Y0: a] :
( ( sK5 @ Y0 )
=> ( sK5 @ ( cL @ Y0 ) ) ) ) ) )
| ~ spl0_2
| ~ spl0_6 ),
inference(backward_demodulation,[status(thm)],[f1029,f1155]) ).
thf(f1155,plain,
( ( ( sK5 @ sK3 )
= $true )
| ~ spl0_2
| ~ spl0_6 ),
inference(binary_proxy_clausification,[status(thm)],[f1029]) ).
thf(f1029,plain,
( ( ( ( sK5 @ sK3 )
& ( !! @ a
@ ^ [Y0: a] :
( ( sK5 @ Y0 )
=> ( sK5 @ ( cL @ Y0 ) ) ) ) )
= $true )
| ~ spl0_2
| ~ spl0_6 ),
inference(binary_proxy_clausification,[status(thm)],[f1015]) ).
thf(f1015,plain,
( ( ( ( ( sK5 @ sK3 )
& ( !! @ a
@ ^ [Y0: a] :
( ( sK5 @ Y0 )
=> ( sK5 @ ( cL @ Y0 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y0: a] :
( ( ( cR @ Y0 )
= sK4 )
& ( sK5 @ Y0 ) ) ) )
= $false )
| ~ spl0_2
| ~ spl0_6 ),
inference(beta_eta_normalization,[status(thm)],[f1012]) ).
thf(f1012,plain,
( ( $false
= ( ^ [Y0: a > $o] :
( ( ( Y0 @ sK3 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK4 )
& ( Y0 @ Y1 ) ) ) )
@ sK5 ) )
| ~ spl0_2
| ~ spl0_6 ),
inference(sigma_clausification,[status(thm)],[f1009]) ).
thf(f1009,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( Y0 @ sK3 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK4 )
& ( Y0 @ Y1 ) ) ) ) )
= $false )
| ~ spl0_2
| ~ spl0_6 ),
inference(not_proxy_clausification,[status(thm)],[f977]) ).
thf(f977,plain,
( ( $true
= ( ~ ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( Y0 @ sK3 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK4 )
& ( Y0 @ Y1 ) ) ) ) ) ) )
| ~ spl0_2
| ~ spl0_6 ),
inference(boolean_simplification,[status(thm)],[f976]) ).
thf(f976,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( Y0 @ sK3 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK4 )
& ( Y0 @ Y1 ) ) ) ) )
=> $false )
= $true )
| ~ spl0_2
| ~ spl0_6 ),
inference(superposition,[status(thm)],[f946,f970]) ).
thf(f970,plain,
( ( ( cX @ sK4 )
= $false )
| ~ spl0_2
| ~ spl0_6 ),
inference(binary_proxy_clausification,[status(thm)],[f967]) ).
thf(f967,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK3 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK4 )
& ( Y0 @ Y1 ) ) ) ) )
=> ( cX @ sK4 ) )
= $false )
| ~ spl0_2
| ~ spl0_6 ),
inference(beta_eta_normalization,[status(thm)],[f964]) ).
thf(f964,plain,
( ( $false
= ( ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) )
& ( Y1 @ sK3 ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) )
@ sK4 ) )
| ~ spl0_2
| ~ spl0_6 ),
inference(sigma_clausification,[status(thm)],[f944]) ).
thf(f944,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) )
& ( Y1 @ sK3 ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
= $false )
| ~ spl0_2
| ~ spl0_6 ),
inference(boolean_simplification,[status(thm)],[f943]) ).
thf(f943,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) )
& ( Y1 @ sK3 ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
& $true )
= $false )
| ~ spl0_2
| ~ spl0_6 ),
inference(superposition,[status(thm)],[f892,f69]) ).
thf(f69,plain,
( ( $true
= ( cG @ ( cP @ sK3 @ sK2 ) ) )
| ~ spl0_6 ),
inference(avatar_component_clause,[status(thm)],[f68]) ).
thf(f68,definition,
( spl0_6
<=> ( $true
= ( cG @ ( cP @ sK3 @ sK2 ) ) ) ),
introduced(definition,[new_symbols(naming,[spl0_6])],[avatar_definition]) ).
thf(f892,plain,
( ! [X1: a] :
( ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) )
& ( Y1 @ X1 ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
& ( cG @ ( cP @ X1 @ sK2 ) ) )
= $false )
| ~ spl0_2 ),
inference(beta_eta_normalization,[status(thm)],[f891]) ).
thf(f891,plain,
( ! [X1: a] :
( $false
= ( ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cG @ ( cP @ Y0 @ sK2 ) ) )
@ X1 ) )
| ~ spl0_2 ),
inference(pi_clausification,[status(thm)],[f847]) ).
thf(f946,plain,
( ! [X1: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( Y0 @ sK3 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= X1 )
& ( Y0 @ Y1 ) ) ) ) )
=> ( cX @ X1 ) )
= $true )
| ~ spl0_2
| ~ spl0_6 ),
inference(beta_eta_normalization,[status(thm)],[f945]) ).
thf(f945,plain,
( ! [X1: a] :
( ( ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK3 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) )
@ X1 )
= $true )
| ~ spl0_2
| ~ spl0_6 ),
inference(pi_clausification,[status(thm)],[f942]) ).
thf(f942,plain,
( ( $true
= ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK3 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
| ~ spl0_2
| ~ spl0_6 ),
inference(boolean_simplification,[status(thm)],[f941]) ).
thf(f941,plain,
( ( $true
= ( $true
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK3 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) ) )
| ~ spl0_2
| ~ spl0_6 ),
inference(boolean_simplification,[status(thm)],[f940]) ).
thf(f940,plain,
( ( $true
= ( ( $true
| ( cF @ ( cP @ sK3 @ sK2 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK3 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) ) )
| ~ spl0_2
| ~ spl0_6 ),
inference(backward_demodulation,[status(thm)],[f807,f69]) ).
thf(f1159,plain,
( ( ( ~ ( !! @ a
@ ^ [Y0: a] :
( ( sK5 @ Y0 )
=> ( sK5 @ ( cL @ Y0 ) ) ) ) )
= $true )
| ~ spl0_2
| ~ spl0_6 ),
inference(boolean_simplification,[status(thm)],[f1156]) ).
thf(f1156,plain,
( ( ( ~ ( ( !! @ a
@ ^ [Y0: a] :
( ( sK5 @ Y0 )
=> ( sK5 @ ( cL @ Y0 ) ) ) )
& $true ) )
= $true )
| ~ spl0_2
| ~ spl0_6 ),
inference(backward_demodulation,[status(thm)],[f1034,f1155]) ).
thf(f1034,plain,
( ( ( ~ ( ( !! @ a
@ ^ [Y0: a] :
( ( sK5 @ Y0 )
=> ( sK5 @ ( cL @ Y0 ) ) ) )
& ( sK5 @ sK3 ) ) )
= $true )
| ~ spl0_2
| ~ spl0_6 ),
inference(boolean_simplification,[status(thm)],[f1033]) ).
thf(f1033,plain,
( ( $true
= ( ( ( !! @ a
@ ^ [Y0: a] :
( ( sK5 @ Y0 )
=> ( sK5 @ ( cL @ Y0 ) ) ) )
& ( sK5 @ sK3 ) )
=> $false ) )
| ~ spl0_2
| ~ spl0_6 ),
inference(superposition,[status(thm)],[f979,f1031]) ).
thf(f1031,plain,
( ( $false
= ( ?? @ a
@ ^ [Y0: a] :
( ( ( cR @ Y0 )
= sK4 )
& ( sK5 @ Y0 ) ) ) )
| ~ spl0_2
| ~ spl0_6 ),
inference(boolean_simplification,[status(thm)],[f1030]) ).
thf(f1030,plain,
( ( ( $true
=> ( ?? @ a
@ ^ [Y0: a] :
( ( ( cR @ Y0 )
= sK4 )
& ( sK5 @ Y0 ) ) ) )
= $false )
| ~ spl0_2
| ~ spl0_6 ),
inference(backward_demodulation,[status(thm)],[f1015,f1029]) ).
thf(f979,plain,
( ! [X1: a > $o] :
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( X1 @ ( cL @ Y0 ) ) ) )
& ( X1 @ sK3 ) )
=> ( ?? @ a
@ ^ [Y0: a] :
( ( ( cR @ Y0 )
= sK4 )
& ( X1 @ Y0 ) ) ) )
= $true )
| ~ spl0_2
| ~ spl0_6 ),
inference(beta_eta_normalization,[status(thm)],[f978]) ).
thf(f978,plain,
( ! [X1: a > $o] :
( $true
= ( ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK3 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK4 )
& ( Y0 @ Y1 ) ) ) )
@ X1 ) )
| ~ spl0_2
| ~ spl0_6 ),
inference(pi_clausification,[status(thm)],[f971]) ).
thf(f971,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK3 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK4 )
& ( Y0 @ Y1 ) ) ) ) )
= $true )
| ~ spl0_2
| ~ spl0_6 ),
inference(binary_proxy_clausification,[status(thm)],[f967]) ).
thf(f799,plain,
( ~ spl0_1
| ~ spl0_10 ),
inference(avatar_contradiction_clause,[status(thm)],[f798]) ).
thf(f798,plain,
( $false
| ~ spl0_1
| ~ spl0_10 ),
inference(trivial_inequality_removal,[status(thm)],[f797]) ).
thf(f797,plain,
( ( $false = $true )
| ~ spl0_1
| ~ spl0_10 ),
inference(boolean_simplification,[status(thm)],[f796]) ).
thf(f796,plain,
( ( $true = ( ~ $true ) )
| ~ spl0_1
| ~ spl0_10 ),
inference(forward_demodulation,[status(thm)],[f791,f792]) ).
thf(f792,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( sK16 @ Y0 )
=> ( sK16 @ ( cL @ Y0 ) ) ) )
= $true )
| ~ spl0_1
| ~ spl0_10 ),
inference(boolean_simplification,[status(thm)],[f790]) ).
thf(f790,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( sK16 @ Y0 )
=> ( sK16 @ ( cL @ Y0 ) ) ) )
& $true )
= $true )
| ~ spl0_1
| ~ spl0_10 ),
inference(backward_demodulation,[status(thm)],[f699,f787]) ).
thf(f787,plain,
( ( ( sK16 @ sK12 )
= $true )
| ~ spl0_1
| ~ spl0_10 ),
inference(binary_proxy_clausification,[status(thm)],[f699]) ).
thf(f699,plain,
( ( $true
= ( ( !! @ a
@ ^ [Y0: a] :
( ( sK16 @ Y0 )
=> ( sK16 @ ( cL @ Y0 ) ) ) )
& ( sK16 @ sK12 ) ) )
| ~ spl0_1
| ~ spl0_10 ),
inference(binary_proxy_clausification,[status(thm)],[f697]) ).
thf(f697,plain,
( ( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( sK16 @ Y0 )
=> ( sK16 @ ( cL @ Y0 ) ) ) )
& ( sK16 @ sK12 ) )
=> ( ?? @ a
@ ^ [Y0: a] :
( ( ( cR @ Y0 )
= sK13 )
& ( sK16 @ Y0 ) ) ) )
= $false )
| ~ spl0_1
| ~ spl0_10 ),
inference(beta_eta_normalization,[status(thm)],[f694]) ).
thf(f694,plain,
( ( $false
= ( ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK12 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK13 )
& ( Y0 @ Y1 ) ) ) )
@ sK16 ) )
| ~ spl0_1
| ~ spl0_10 ),
inference(sigma_clausification,[status(thm)],[f686]) ).
thf(f686,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK12 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK13 )
& ( Y0 @ Y1 ) ) ) ) )
= $false )
| ~ spl0_1
| ~ spl0_10 ),
inference(not_proxy_clausification,[status(thm)],[f619]) ).
thf(f619,plain,
( ( $true
= ( ~ ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK12 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK13 )
& ( Y0 @ Y1 ) ) ) ) ) ) )
| ~ spl0_1
| ~ spl0_10 ),
inference(boolean_simplification,[status(thm)],[f618]) ).
thf(f618,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK12 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK13 )
& ( Y0 @ Y1 ) ) ) ) )
=> $false )
= $true )
| ~ spl0_1
| ~ spl0_10 ),
inference(superposition,[status(thm)],[f583,f617]) ).
thf(f617,plain,
( ( ( cX @ sK13 )
= $false )
| ~ spl0_1
| ~ spl0_10 ),
inference(boolean_simplification,[status(thm)],[f616]) ).
thf(f616,plain,
( ( $false
= ( $true
=> ( cX @ sK13 ) ) )
| ~ spl0_1
| ~ spl0_10 ),
inference(backward_demodulation,[status(thm)],[f604,f615]) ).
thf(f615,plain,
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( Y0 @ sK12 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK13 )
& ( Y0 @ Y1 ) ) ) ) )
= $true )
| ~ spl0_1
| ~ spl0_10 ),
inference(binary_proxy_clausification,[status(thm)],[f604]) ).
thf(f604,plain,
( ( $false
= ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( Y0 @ sK12 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK13 )
& ( Y0 @ Y1 ) ) ) ) )
=> ( cX @ sK13 ) ) )
| ~ spl0_1
| ~ spl0_10 ),
inference(beta_eta_normalization,[status(thm)],[f602]) ).
thf(f602,plain,
( ( $false
= ( ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK12 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) )
@ sK13 ) )
| ~ spl0_1
| ~ spl0_10 ),
inference(sigma_clausification,[status(thm)],[f581]) ).
thf(f581,plain,
( ( $false
= ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK12 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
| ~ spl0_1
| ~ spl0_10 ),
inference(boolean_simplification,[status(thm)],[f580]) ).
thf(f580,plain,
( ( ( $true
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK12 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
= $false )
| ~ spl0_1
| ~ spl0_10 ),
inference(boolean_simplification,[status(thm)],[f579]) ).
thf(f579,plain,
( ( $false
= ( ( $true
| ( cF @ ( cP @ sK12 @ sK2 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK12 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) ) )
| ~ spl0_1
| ~ spl0_10 ),
inference(superposition,[status(thm)],[f308,f575]) ).
thf(f575,plain,
( ( $true
= ( cG @ ( cP @ sK12 @ sK2 ) ) )
| ~ spl0_10 ),
inference(binary_proxy_clausification,[status(thm)],[f570]) ).
thf(f570,plain,
( ( $true
= ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) )
& ( Y1 @ sK12 ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
& ( cG @ ( cP @ sK12 @ sK2 ) ) ) )
| ~ spl0_10 ),
inference(beta_eta_normalization,[status(thm)],[f569]) ).
thf(f569,plain,
( ( $true
= ( ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cG @ ( cP @ Y0 @ sK2 ) ) )
@ sK12 ) )
| ~ spl0_10 ),
inference(sigma_clausification,[status(thm)],[f226]) ).
thf(f226,plain,
( ( ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cG @ ( cP @ Y0 @ sK2 ) ) ) )
= $true )
| ~ spl0_10 ),
inference(avatar_component_clause,[status(thm)],[f225]) ).
thf(f225,definition,
( spl0_10
<=> ( ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cG @ ( cP @ Y0 @ sK2 ) ) ) )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl0_10])],[avatar_definition]) ).
thf(f308,plain,
( ! [X1: a] :
( $false
= ( ( ( cG @ ( cP @ X1 @ sK2 ) )
| ( cF @ ( cP @ X1 @ sK2 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ X1 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) ) )
| ~ spl0_1 ),
inference(beta_eta_normalization,[status(thm)],[f307]) ).
thf(f307,plain,
( ! [X1: a] :
( ( ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK2 ) )
| ( cF @ ( cP @ Y0 @ sK2 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) )
@ X1 )
= $false )
| ~ spl0_1 ),
inference(pi_clausification,[status(thm)],[f32]) ).
thf(f32,plain,
( ( $false
= ( ?? @ a
@ ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK2 ) )
| ( cF @ ( cP @ Y0 @ sK2 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
| ~ spl0_1 ),
inference(avatar_component_clause,[status(thm)],[f31]) ).
thf(f31,definition,
( spl0_1
<=> ( $false
= ( ?? @ a
@ ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK2 ) )
| ( cF @ ( cP @ Y0 @ sK2 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) ) ),
introduced(definition,[new_symbols(naming,[spl0_1])],[avatar_definition]) ).
thf(f583,plain,
( ! [X1: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK12 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= X1 )
& ( Y0 @ Y1 ) ) ) ) )
=> ( cX @ X1 ) )
= $true )
| ~ spl0_10 ),
inference(beta_eta_normalization,[status(thm)],[f582]) ).
thf(f582,plain,
( ! [X1: a] :
( $true
= ( ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) )
& ( Y1 @ sK12 ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) )
@ X1 ) )
| ~ spl0_10 ),
inference(pi_clausification,[status(thm)],[f578]) ).
thf(f578,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) )
& ( Y1 @ sK12 ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
= $true )
| ~ spl0_10 ),
inference(boolean_simplification,[status(thm)],[f577]) ).
thf(f577,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) )
& ( Y1 @ sK12 ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
& $true )
= $true )
| ~ spl0_10 ),
inference(backward_demodulation,[status(thm)],[f570,f575]) ).
thf(f791,plain,
( ( $true
= ( ~ ( !! @ a
@ ^ [Y0: a] :
( ( sK16 @ Y0 )
=> ( sK16 @ ( cL @ Y0 ) ) ) ) ) )
| ~ spl0_1
| ~ spl0_10 ),
inference(boolean_simplification,[status(thm)],[f789]) ).
thf(f789,plain,
( ( ( ~ ( $true
& ( !! @ a
@ ^ [Y0: a] :
( ( sK16 @ Y0 )
=> ( sK16 @ ( cL @ Y0 ) ) ) ) ) )
= $true )
| ~ spl0_1
| ~ spl0_10 ),
inference(backward_demodulation,[status(thm)],[f705,f787]) ).
thf(f705,plain,
( ( $true
= ( ~ ( ( sK16 @ sK12 )
& ( !! @ a
@ ^ [Y0: a] :
( ( sK16 @ Y0 )
=> ( sK16 @ ( cL @ Y0 ) ) ) ) ) ) )
| ~ spl0_1
| ~ spl0_10 ),
inference(boolean_simplification,[status(thm)],[f703]) ).
thf(f703,plain,
( ( ( ( ( sK16 @ sK12 )
& ( !! @ a
@ ^ [Y0: a] :
( ( sK16 @ Y0 )
=> ( sK16 @ ( cL @ Y0 ) ) ) ) )
=> $false )
= $true )
| ~ spl0_1
| ~ spl0_10 ),
inference(superposition,[status(thm)],[f621,f701]) ).
thf(f701,plain,
( ( $false
= ( ?? @ a
@ ^ [Y0: a] :
( ( ( cR @ Y0 )
= sK13 )
& ( sK16 @ Y0 ) ) ) )
| ~ spl0_1
| ~ spl0_10 ),
inference(boolean_simplification,[status(thm)],[f700]) ).
thf(f700,plain,
( ( ( $true
=> ( ?? @ a
@ ^ [Y0: a] :
( ( ( cR @ Y0 )
= sK13 )
& ( sK16 @ Y0 ) ) ) )
= $false )
| ~ spl0_1
| ~ spl0_10 ),
inference(backward_demodulation,[status(thm)],[f697,f699]) ).
thf(f621,plain,
( ! [X1: a > $o] :
( ( ( ( X1 @ sK12 )
& ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( X1 @ ( cL @ Y0 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y0: a] :
( ( ( cR @ Y0 )
= sK13 )
& ( X1 @ Y0 ) ) ) )
= $true )
| ~ spl0_1
| ~ spl0_10 ),
inference(beta_eta_normalization,[status(thm)],[f620]) ).
thf(f620,plain,
( ! [X1: a > $o] :
( ( ^ [Y0: a > $o] :
( ( ( Y0 @ sK12 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK13 )
& ( Y0 @ Y1 ) ) ) )
@ X1 )
= $true )
| ~ spl0_1
| ~ spl0_10 ),
inference(pi_clausification,[status(thm)],[f615]) ).
thf(f561,plain,
( ~ spl0_1
| ~ spl0_9 ),
inference(avatar_contradiction_clause,[status(thm)],[f560]) ).
thf(f560,plain,
( $false
| ~ spl0_1
| ~ spl0_9 ),
inference(trivial_inequality_removal,[status(thm)],[f559]) ).
thf(f559,plain,
( ( $false = $true )
| ~ spl0_1
| ~ spl0_9 ),
inference(boolean_simplification,[status(thm)],[f558]) ).
thf(f558,plain,
( ( $true = ( ~ $true ) )
| ~ spl0_1
| ~ spl0_9 ),
inference(backward_demodulation,[status(thm)],[f557,f556]) ).
thf(f556,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( sK11 @ Y0 )
=> ( sK11 @ ( cL @ Y0 ) ) ) )
= $true )
| ~ spl0_1
| ~ spl0_9 ),
inference(boolean_simplification,[status(thm)],[f555]) ).
thf(f555,plain,
( ( $true
= ( ( !! @ a
@ ^ [Y0: a] :
( ( sK11 @ Y0 )
=> ( sK11 @ ( cL @ Y0 ) ) ) )
& $true ) )
| ~ spl0_1
| ~ spl0_9 ),
inference(backward_demodulation,[status(thm)],[f469,f552]) ).
thf(f552,plain,
( ( $true
= ( sK11 @ sK6 ) )
| ~ spl0_1
| ~ spl0_9 ),
inference(binary_proxy_clausification,[status(thm)],[f469]) ).
thf(f469,plain,
( ( ( ( !! @ a
@ ^ [Y0: a] :
( ( sK11 @ Y0 )
=> ( sK11 @ ( cL @ Y0 ) ) ) )
& ( sK11 @ sK6 ) )
= $true )
| ~ spl0_1
| ~ spl0_9 ),
inference(binary_proxy_clausification,[status(thm)],[f460]) ).
thf(f460,plain,
( ( $false
= ( ( ( !! @ a
@ ^ [Y0: a] :
( ( sK11 @ Y0 )
=> ( sK11 @ ( cL @ Y0 ) ) ) )
& ( sK11 @ sK6 ) )
=> ( ?? @ a
@ ^ [Y0: a] :
( ( ( cR @ Y0 )
= sK9 )
& ( sK11 @ Y0 ) ) ) ) )
| ~ spl0_1
| ~ spl0_9 ),
inference(beta_eta_normalization,[status(thm)],[f457]) ).
thf(f457,plain,
( ( $false
= ( ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK6 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK9 )
& ( Y0 @ Y1 ) ) ) )
@ sK11 ) )
| ~ spl0_1
| ~ spl0_9 ),
inference(sigma_clausification,[status(thm)],[f450]) ).
thf(f450,plain,
( ( $false
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK6 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK9 )
& ( Y0 @ Y1 ) ) ) ) ) )
| ~ spl0_1
| ~ spl0_9 ),
inference(not_proxy_clausification,[status(thm)],[f354]) ).
thf(f354,plain,
( ( ( ~ ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK6 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK9 )
& ( Y0 @ Y1 ) ) ) ) ) )
= $true )
| ~ spl0_1
| ~ spl0_9 ),
inference(boolean_simplification,[status(thm)],[f353]) ).
thf(f353,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK6 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK9 )
& ( Y0 @ Y1 ) ) ) ) )
=> $false )
= $true )
| ~ spl0_1
| ~ spl0_9 ),
inference(superposition,[status(thm)],[f281,f352]) ).
thf(f352,plain,
( ( ( cX @ sK9 )
= $false )
| ~ spl0_1
| ~ spl0_9 ),
inference(boolean_simplification,[status(thm)],[f351]) ).
thf(f351,plain,
( ( $false
= ( $true
=> ( cX @ sK9 ) ) )
| ~ spl0_1
| ~ spl0_9 ),
inference(backward_demodulation,[status(thm)],[f342,f350]) ).
thf(f350,plain,
( ( $true
= ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( Y0 @ sK6 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK9 )
& ( Y0 @ Y1 ) ) ) ) ) )
| ~ spl0_1
| ~ spl0_9 ),
inference(binary_proxy_clausification,[status(thm)],[f342]) ).
thf(f342,plain,
( ( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( Y0 @ sK6 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK9 )
& ( Y0 @ Y1 ) ) ) ) )
=> ( cX @ sK9 ) )
= $false )
| ~ spl0_1
| ~ spl0_9 ),
inference(beta_eta_normalization,[status(thm)],[f340]) ).
thf(f340,plain,
( ( $false
= ( ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK6 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) )
@ sK9 ) )
| ~ spl0_1
| ~ spl0_9 ),
inference(sigma_clausification,[status(thm)],[f321]) ).
thf(f321,plain,
( ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK6 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
= $false )
| ~ spl0_1
| ~ spl0_9 ),
inference(boolean_simplification,[status(thm)],[f320]) ).
thf(f320,plain,
( ( $false
= ( $true
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK6 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) ) )
| ~ spl0_1
| ~ spl0_9 ),
inference(boolean_simplification,[status(thm)],[f317]) ).
thf(f317,plain,
( ( ( ( ( cG @ ( cP @ sK6 @ sK2 ) )
| $true )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK6 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
= $false )
| ~ spl0_1
| ~ spl0_9 ),
inference(superposition,[status(thm)],[f308,f279]) ).
thf(f279,plain,
( ( $true
= ( cF @ ( cP @ sK6 @ sK2 ) ) )
| ~ spl0_9 ),
inference(boolean_simplification,[status(thm)],[f278]) ).
thf(f278,plain,
( ( ( $true
& ( cF @ ( cP @ sK6 @ sK2 ) ) )
= $true )
| ~ spl0_9 ),
inference(backward_demodulation,[status(thm)],[f247,f277]) ).
thf(f277,plain,
( ( $true
= ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) )
& ( Y1 @ sK6 ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) )
| ~ spl0_9 ),
inference(binary_proxy_clausification,[status(thm)],[f247]) ).
thf(f247,plain,
( ( $true
= ( ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) )
& ( Y1 @ sK6 ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) )
& ( cF @ ( cP @ sK6 @ sK2 ) ) ) )
| ~ spl0_9 ),
inference(beta_eta_normalization,[status(thm)],[f246]) ).
thf(f246,plain,
( ( ( ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cF @ ( cP @ Y0 @ sK2 ) ) )
@ sK6 )
= $true )
| ~ spl0_9 ),
inference(sigma_clausification,[status(thm)],[f223]) ).
thf(f223,plain,
( ( ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cF @ ( cP @ Y0 @ sK2 ) ) ) )
= $true )
| ~ spl0_9 ),
inference(avatar_component_clause,[status(thm)],[f222]) ).
thf(f222,definition,
( spl0_9
<=> ( ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cF @ ( cP @ Y0 @ sK2 ) ) ) )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl0_9])],[avatar_definition]) ).
thf(f281,plain,
( ! [X1: a] :
( ( ( !! @ ( a > $o )
@ ^ [Y0: a > $o] :
( ( ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) )
& ( Y0 @ sK6 ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= X1 )
& ( Y0 @ Y1 ) ) ) ) )
=> ( cX @ X1 ) )
= $true )
| ~ spl0_9 ),
inference(beta_eta_normalization,[status(thm)],[f280]) ).
thf(f280,plain,
( ! [X1: a] :
( ( ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) )
& ( Y1 @ sK6 ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) )
@ X1 )
= $true )
| ~ spl0_9 ),
inference(pi_clausification,[status(thm)],[f277]) ).
thf(f557,plain,
( ( $true
= ( ~ ( !! @ a
@ ^ [Y0: a] :
( ( sK11 @ Y0 )
=> ( sK11 @ ( cL @ Y0 ) ) ) ) ) )
| ~ spl0_1
| ~ spl0_9 ),
inference(boolean_simplification,[status(thm)],[f554]) ).
thf(f554,plain,
( ( $true
= ( ~ ( $true
& ( !! @ a
@ ^ [Y0: a] :
( ( sK11 @ Y0 )
=> ( sK11 @ ( cL @ Y0 ) ) ) ) ) ) )
| ~ spl0_1
| ~ spl0_9 ),
inference(backward_demodulation,[status(thm)],[f486,f552]) ).
thf(f486,plain,
( ( $true
= ( ~ ( ( sK11 @ sK6 )
& ( !! @ a
@ ^ [Y0: a] :
( ( sK11 @ Y0 )
=> ( sK11 @ ( cL @ Y0 ) ) ) ) ) ) )
| ~ spl0_1
| ~ spl0_9 ),
inference(boolean_simplification,[status(thm)],[f484]) ).
thf(f484,plain,
( ( ( ( ( sK11 @ sK6 )
& ( !! @ a
@ ^ [Y0: a] :
( ( sK11 @ Y0 )
=> ( sK11 @ ( cL @ Y0 ) ) ) ) )
=> $false )
= $true )
| ~ spl0_1
| ~ spl0_9 ),
inference(superposition,[status(thm)],[f372,f468]) ).
thf(f468,plain,
( ( ( ?? @ a
@ ^ [Y0: a] :
( ( ( cR @ Y0 )
= sK9 )
& ( sK11 @ Y0 ) ) )
= $false )
| ~ spl0_1
| ~ spl0_9 ),
inference(binary_proxy_clausification,[status(thm)],[f460]) ).
thf(f372,plain,
( ! [X1: a > $o] :
( ( ( ( X1 @ sK6 )
& ( !! @ a
@ ^ [Y0: a] :
( ( X1 @ Y0 )
=> ( X1 @ ( cL @ Y0 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y0: a] :
( ( ( cR @ Y0 )
= sK9 )
& ( X1 @ Y0 ) ) ) )
= $true )
| ~ spl0_1
| ~ spl0_9 ),
inference(beta_eta_normalization,[status(thm)],[f371]) ).
thf(f371,plain,
( ! [X1: a > $o] :
( ( ^ [Y0: a > $o] :
( ( ( Y0 @ sK6 )
& ( !! @ a
@ ^ [Y1: a] :
( ( Y0 @ Y1 )
=> ( Y0 @ ( cL @ Y1 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y1: a] :
( ( ( cR @ Y1 )
= sK9 )
& ( Y0 @ Y1 ) ) ) )
@ X1 )
= $true )
| ~ spl0_1
| ~ spl0_9 ),
inference(pi_clausification,[status(thm)],[f350]) ).
thf(f227,plain,
( spl0_9
| spl0_10
| ~ spl0_1 ),
inference(avatar_split_clause,[status(thm)],[f220,f31,f225,f222]) ).
thf(f220,plain,
( ( ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cF @ ( cP @ Y0 @ sK2 ) ) ) )
= $true )
| ( ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cG @ ( cP @ Y0 @ sK2 ) ) ) )
= $true )
| ~ spl0_1 ),
inference(binary_proxy_clausification,[status(thm)],[f219]) ).
thf(f219,plain,
( ( $false
!= ( ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cG @ ( cP @ Y0 @ sK2 ) ) ) )
| ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cF @ ( cP @ Y0 @ sK2 ) ) ) ) ) )
| ~ spl0_1 ),
inference(forward_demodulation,[status(thm)],[f20,f32]) ).
thf(f70,plain,
( spl0_5
| spl0_6
| ~ spl0_2 ),
inference(avatar_split_clause,[status(thm)],[f63,f34,f68,f65]) ).
thf(f63,plain,
( ( $true
= ( cF @ ( cP @ sK3 @ sK2 ) ) )
| ( $true
= ( cG @ ( cP @ sK3 @ sK2 ) ) )
| ~ spl0_2 ),
inference(binary_proxy_clausification,[status(thm)],[f52]) ).
thf(f52,plain,
( ( $true
= ( ( cG @ ( cP @ sK3 @ sK2 ) )
| ( cF @ ( cP @ sK3 @ sK2 ) ) ) )
| ~ spl0_2 ),
inference(binary_proxy_clausification,[status(thm)],[f48]) ).
thf(f48,plain,
( ( $true
= ( ( ( cG @ ( cP @ sK3 @ sK2 ) )
| ( cF @ ( cP @ sK3 @ sK2 ) ) )
& ( !! @ a
@ ^ [Y0: a] :
( ( !! @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( ( Y1 @ sK3 )
& ( !! @ a
@ ^ [Y2: a] :
( ( Y1 @ Y2 )
=> ( Y1 @ ( cL @ Y2 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y2: a] :
( ( ( cR @ Y2 )
= Y0 )
& ( Y1 @ Y2 ) ) ) ) )
=> ( cX @ Y0 ) ) ) ) )
| ~ spl0_2 ),
inference(beta_eta_normalization,[status(thm)],[f47]) ).
thf(f47,plain,
( ( $true
= ( ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK2 ) )
| ( cF @ ( cP @ Y0 @ sK2 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) )
@ sK3 ) )
| ~ spl0_2 ),
inference(sigma_clausification,[status(thm)],[f44]) ).
thf(f44,plain,
( ( $false
!= ( ?? @ a
@ ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK2 ) )
| ( cF @ ( cP @ Y0 @ sK2 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) )
| ~ spl0_2 ),
inference(backward_demodulation,[status(thm)],[f20,f35]) ).
thf(f36,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[status(thm)],[f29,f34,f31]) ).
thf(f29,plain,
( ( $false
= ( ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cG @ ( cP @ Y0 @ sK2 ) ) ) )
| ( ?? @ a
@ ^ [Y0: a] :
( ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) )
& ( Y2 @ Y0 ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) )
& ( cF @ ( cP @ Y0 @ sK2 ) ) ) ) ) )
| ( $false
= ( ?? @ a
@ ^ [Y0: a] :
( ( ( cG @ ( cP @ Y0 @ sK2 ) )
| ( cF @ ( cP @ Y0 @ sK2 ) ) )
& ( !! @ a
@ ^ [Y1: a] :
( ( !! @ ( a > $o )
@ ^ [Y2: a > $o] :
( ( ( Y2 @ Y0 )
& ( !! @ a
@ ^ [Y3: a] :
( ( Y2 @ Y3 )
=> ( Y2 @ ( cL @ Y3 ) ) ) ) )
=> ( ?? @ a
@ ^ [Y3: a] :
( ( ( cR @ Y3 )
= Y1 )
& ( Y2 @ Y3 ) ) ) ) )
=> ( cX @ Y1 ) ) ) ) ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : ALG290^5 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.09 % Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.29 % Computer : n022.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 300
% 0.10/0.29 % DateTime : Tue Feb 24 03:43:06 EST 2026
% 0.10/0.29 % CPUTime :
% 0.10/0.30 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.39 ---- Original DTF file ---
% 0.16/0.39 thf(spec,logic,$$dhol).
% 0.16/0.39 %------------------------------------------------------------------------------
% 0.16/0.39 % File : ALG290^5 : TPTP v9.2.1. Released v4.0.0.
% 0.16/0.39 % Domain : General Algebra (Domain theory)
% 0.16/0.39 % Problem : TPS problem from PU-LAMBDA-MODEL-THMS
% 0.16/0.39 % Version : Especial.
% 0.16/0.39 % English :
% 0.16/0.39
% 0.16/0.39 % Refs : [Bro09] Brown (2009), Email to Geoff Sutcliffe
% 0.16/0.39 % Source : [Bro09]
% 0.16/0.39 % Names : tps_1190 [Bro09]
% 0.16/0.39
% 0.16/0.39 % Status : Theorem
% 0.16/0.39 % Rating : 0.56 v9.1.0, 0.38 v9.0.0, 0.50 v8.2.0, 0.62 v8.1.0, 0.64 v7.5.0, 0.57 v7.4.0, 0.44 v7.2.0, 0.38 v7.1.0, 0.50 v7.0.0, 0.43 v6.4.0, 0.50 v6.3.0, 0.60 v6.2.0, 0.57 v5.5.0, 0.50 v5.4.0, 0.80 v4.1.0, 1.00 v4.0.0
% 0.16/0.39 % Syntax : Number of formulae : 9 ( 0 unt; 8 typ; 0 def)
% 0.16/0.39 % Number of atoms : 17 ( 10 equ; 0 cnn)
% 0.16/0.39 % Maximal formula atoms : 7 ( 17 avg)
% 0.16/0.39 % Number of connectives : 81 ( 1 ~; 2 |; 15 &; 50 @)
% 0.16/0.39 % ( 1 <=>; 12 =>; 0 <=; 0 <~>)
% 0.16/0.39 % Maximal formula depth : 15 ( 15 avg)
% 0.16/0.39 % Number of types : 2 ( 1 usr)
% 0.16/0.39 % Number of type conns : 11 ( 11 >; 0 *; 0 +; 0 <<)
% 0.16/0.39 % Number of symbols : 8 ( 7 usr; 1 con; 0-2 aty)
% 0.16/0.39 % Number of variables : 25 ( 2 ^; 16 !; 7 ?; 25 :)
% 0.16/0.39 % SPC : TH0_THM_EQU_NAR
% 0.16/0.39
% 0.16/0.39 % Comments : This problem is from the TPS library. Copyright (c) 2009 The TPS
% 0.16/0.39 % project in the Department of Mathematical Sciences at Carnegie
% 0.16/0.39 % Mellon University. Distributed under the Creative Commons copyleft
% 0.16/0.39 % license: http://creativecommons.org/licenses/by-sa/3.0/
% 0.16/0.39 %------------------------------------------------------------------------------
% 0.16/0.39 thf(a_type,type,
% 0.16/0.39 a: $tType ).
% 0.16/0.39
% 0.16/0.39 thf(cP,type,
% 0.16/0.39 cP: a > a > a ).
% 0.16/0.39
% 0.16/0.39 thf(cG,type,
% 0.16/0.39 cG: a > $o ).
% 0.16/0.39
% 0.16/0.39 thf(cX,type,
% 0.16/0.39 cX: a > $o ).
% 0.16/0.39
% 0.16/0.39 thf(cR,type,
% 0.16/0.39 cR: a > a ).
% 0.16/0.39
% 0.16/0.39 thf(cL,type,
% 0.16/0.39 cL: a > a ).
% 0.16/0.39
% 0.16/0.39 thf(cF,type,
% 0.16/0.39 cF: a > $o ).
% 0.16/0.39
% 0.16/0.39 thf(cZ,type,
% 0.16/0.39 cZ: a ).
% 0.16/0.39
% 0.16/0.39 thf(cPU_X2310A_pme,conjecture,
% 0.16/0.39 ( ( ( ( cL @ cZ )
% 0.16/0.39 = cZ )
% 0.16/0.39 & ( ( cR @ cZ )
% 0.16/0.39 = cZ )
% 0.16/0.39 & ! [Xx: a,Xy: a] :
% 0.16/0.39 ( ( cL @ ( cP @ Xx @ Xy ) )
% 0.16/0.39 = Xx )
% 0.16/0.39 & ! [Xx: a,Xy: a] :
% 0.16/0.39 ( ( cR @ ( cP @ Xx @ Xy ) )
% 0.16/0.39 = Xy )
% 0.16/0.39 & ! [Xt: a] :
% 0.16/0.39 ( ( Xt != cZ )
% 0.16/0.39 <=> ( Xt
% 0.16/0.39 = ( cP @ ( cL @ Xt ) @ ( cR @ Xt ) ) ) )
% 0.16/0.39 & ! [X0: a > $o] :
% 0.16/0.39 ( ? [Xt: a] :
% 0.16/0.39 ( ( X0 @ Xt )
% 0.16/0.39 & ! [Xu: a] :
% 0.16/0.39 ( ( X0 @ Xu )
% 0.16/0.39 => ( X0 @ ( cL @ Xu ) ) ) )
% 0.16/0.39 => ( X0 @ cZ ) ) )
% 0.16/0.39 => ( ( ^ [Xy: a] :
% 0.16/0.39 ? [Xx: a] :
% 0.16/0.39 ( ! [Xx_17: a] :
% 0.16/0.39 ( ! [X0: a > $o] :
% 0.16/0.39 ( ( ( X0 @ Xx )
% 0.16/0.39 & ! [Xz: a] :
% 0.16/0.39 ( ( X0 @ Xz )
% 0.16/0.39 => ( X0 @ ( cL @ Xz ) ) ) )
% 0.16/0.39 => ? [Xv: a] :
% 0.16/0.39 ( ( X0 @ Xv )
% 0.16/0.39 & ( ( cR @ Xv )
% 0.16/0.39 = Xx_17 ) ) )
% 0.16/0.39 => ( cX @ Xx_17 ) )
% 0.16/0.39 & ( ( cF @ ( cP @ Xx @ Xy ) )
% 0.16/0.39 | ( cG @ ( cP @ Xx @ Xy ) ) ) ) )
% 0.16/0.39 = ( ^ [Xz: a] :
% 0.16/0.39 ( ? [Xx: a] :
% 0.16/0.39 ( ! [Xx_18: a] :
% 0.16/0.39 ( ! [X0: a > $o] :
% 0.16/0.39 ( ( ( X0 @ Xx )
% 0.16/0.39 & ! [Xz0: a] :
% 0.16/0.39 ( ( X0 @ Xz0 )
% 0.16/0.39 => ( X0 @ ( cL @ Xz0 ) ) ) )
% 0.16/0.39 => ? [Xv: a] :
% 0.16/0.39 ( ( X0 @ Xv )
% 0.16/0.39 & ( ( cR @ Xv )
% 0.16/0.39 = Xx_18 ) ) )
% 0.16/0.39 => ( cX @ Xx_18 ) )
% 0.16/0.39 & ( cF @ ( cP @ Xx @ Xz ) ) )
% 0.16/0.39 | ? [Xx: a] :
% 0.16/0.39 ( ! [Xx_19: a] :
% 0.16/0.39 ( ! [X0: a > $o] :
% 0.16/0.39 ( ( ( X0 @ Xx )
% 0.16/0.39 & ! [Xz0: a] :
% 0.16/0.39 ( ( X0 @ Xz0 )
% 0.16/0.39 => ( X0 @ ( cL @ Xz0 ) ) ) )
% 0.16/0.39 => ? [Xv: a] :
% 0.16/0.39 ( ( X0 @ Xv )
% 0.16/0.39 & ( ( cR @ Xv )
% 0.16/0.39 = Xx_19 ) ) )
% 0.16/0.39 => ( cX @ Xx_19 ) )
% 0.16/0.39 & ( cG @ ( cP @ Xx @ Xz ) ) ) ) ) ) ) ).
% 0.16/0.39
% 0.16/0.39 %------------------------------------------------------------------------------
% 0.16/0.39 ------------------------
% 1.61/1.34 ---- Embedded in THF ---
% 1.61/1.35 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.61/1.35 %%% Generated on Tue Feb 24 03:43:07 EST 2026
% 1.61/1.35 %%% using '$$dhol' embedding, version 1.3.0.
% 1.61/1.35 %%% Logic specification used:
% 1.61/1.35 %%% thf(spec, logic, $$dhol).
% 1.61/1.35
% 1.61/1.35 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.Td4sovfI6f/DTF2DTF8033.p
% See solution above
% 1.61/1.35 ------------------------
% 1.61/1.36 ---- Cleaned THF ---
% 1.61/1.36 thf(a_type,type,
% 1.61/1.36 a: $tType ).
% 1.61/1.36
% 1.61/1.36 thf(cP,type,
% 1.61/1.36 cP: a > a > a ).
% 1.61/1.36
% 1.61/1.36 thf(cG,type,
% 1.61/1.36 cG: a > $o ).
% 1.61/1.36
% 1.61/1.36 thf(cX,type,
% 1.61/1.36 cX: a > $o ).
% 1.61/1.36
% 1.61/1.36 thf(cR,type,
% 1.61/1.36 cR: a > a ).
% 1.61/1.36
% 1.61/1.36 thf(cL,type,
% 1.61/1.36 cL: a > a ).
% 1.61/1.36
% 1.61/1.36 thf(cF,type,
% 1.61/1.36 cF: a > $o ).
% 1.61/1.36
% 1.61/1.36 thf(cZ,type,
% 1.61/1.36 cZ: a ).
% 1.61/1.36
% 1.61/1.36 thf(cPU_X2310A_pme,conjecture,
% 1.61/1.36 ( ( ( ( cL @ cZ )
% 1.61/1.36 = cZ )
% 1.61/1.36 & ( ( cR @ cZ )
% 1.61/1.36 = cZ )
% 1.61/1.36 & ! [Xx: a,Xy: a] :
% 1.61/1.36 ( ( cL @ ( cP @ Xx @ Xy ) )
% 1.61/1.36 = Xx )
% 1.61/1.36 & ! [Xx: a,Xy: a] :
% 1.61/1.36 ( ( cR @ ( cP @ Xx @ Xy ) )
% 1.61/1.36 = Xy )
% 1.61/1.36 & ! [Xt: a] :
% 1.61/1.36 ( ( Xt != cZ )
% 1.61/1.36 <=> ( Xt
% 1.61/1.36 = ( cP @ ( cL @ Xt ) @ ( cR @ Xt ) ) ) )
% 1.61/1.36 & ! [X0: a > $o] :
% 1.61/1.36 ( ? [Xt: a] :
% 1.61/1.36 ( ( X0 @ Xt )
% 1.61/1.36 & ! [Xu: a] :
% 1.61/1.36 ( ( X0 @ Xu )
% 1.61/1.36 => ( X0 @ ( cL @ Xu ) ) ) )
% 1.61/1.36 => ( X0 @ cZ ) ) )
% 1.61/1.36 => ( ( ^ [Xy: a] :
% 1.61/1.36 ? [Xx: a] :
% 1.61/1.36 ( ! [Xx_17: a] :
% 1.61/1.36 ( ! [X0: a > $o] :
% 1.61/1.36 ( ( ( X0 @ Xx )
% 1.61/1.36 & ! [Xz: a] :
% 1.61/1.36 ( ( X0 @ Xz )
% 1.61/1.36 => ( X0 @ ( cL @ Xz ) ) ) )
% 1.61/1.36 => ? [Xv: a] :
% 1.61/1.36 ( ( X0 @ Xv )
% 1.61/1.36 & ( ( cR @ Xv )
% 1.61/1.36 = Xx_17 ) ) )
% 1.61/1.36 => ( cX @ Xx_17 ) )
% 1.61/1.36 & ( ( cF @ ( cP @ Xx @ Xy ) )
% 1.61/1.36 | ( cG @ ( cP @ Xx @ Xy ) ) ) ) )
% 1.61/1.36 = ( ^ [Xz: a] :
% 1.61/1.36 ( ? [Xx: a] :
% 1.61/1.36 ( ! [Xx_18: a] :
% 1.61/1.36 ( ! [X0: a > $o] :
% 1.61/1.36 ( ( ( X0 @ Xx )
% 1.61/1.36 & ! [Xz0: a] :
% 1.61/1.36 ( ( X0 @ Xz0 )
% 1.61/1.36 => ( X0 @ ( cL @ Xz0 ) ) ) )
% 1.61/1.36 => ? [Xv: a] :
% 1.61/1.36 ( ( X0 @ Xv )
% 1.61/1.36 & ( ( cR @ Xv )
% 1.61/1.36 = Xx_18 ) ) )
% 1.61/1.36 => ( cX @ Xx_18 ) )
% 1.61/1.36 & ( cF @ ( cP @ Xx @ Xz ) ) )
% 1.61/1.36 | ? [Xx: a] :
% 1.61/1.36 ( ! [Xx_19: a] :
% 1.61/1.36 ( ! [X0: a > $o] :
% 1.61/1.36 ( ( ( X0 @ Xx )
% 1.61/1.36 & ! [Xz0: a] :
% 1.61/1.36 ( ( X0 @ Xz0 )
% 1.61/1.36 => ( X0 @ ( cL @ Xz0 ) ) ) )
% 1.61/1.36 => ? [Xv: a] :
% 1.61/1.36 ( ( X0 @ Xv )
% 1.61/1.36 & ( ( cR @ Xv )
% 1.61/1.36 = Xx_19 ) ) )
% 1.61/1.36 => ( cX @ Xx_19 ) )
% 1.61/1.36 & ( cG @ ( cP @ Xx @ Xz ) ) ) ) ) ) ) ).
% 1.61/1.36 ------------------------
% 1.61/1.38 % (8132)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_8033 for (2999ds/27Mi)
% 1.61/1.38 % (8133)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_8033 for (2999ds/2Mi)
% 1.61/1.38 % (8131)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_8033 for (2999ds/4Mi)
% 1.61/1.38 % (8135)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_8033 for (2999ds/275Mi)
% 1.61/1.38 % (8130)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_8033 for (2999ds/183Mi)
% 1.61/1.38 % (8136)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_8033 for (2999ds/18Mi)
% 1.61/1.38 % (8134)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_8033 for (2999ds/2Mi)
% 1.61/1.38 % (8133)Instruction limit reached!
% 1.61/1.38 % (8133)------------------------------
% 1.61/1.38 % (8133)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.61/1.38 % (8133)Termination reason: Unknown
% 1.61/1.38 % (8133)Termination phase: Property scanning
% 1.61/1.38
% 1.61/1.38 % (8133)Memory used [KB]: 1023
% 1.61/1.38 % (8133)Time elapsed: 0.003 s
% 1.61/1.38 % (8133)Instructions burned: 2 (million)
% 1.61/1.38 % (8133)------------------------------
% 1.61/1.38 % (8133)------------------------------
% 1.61/1.38 % (8134)Instruction limit reached!
% 1.61/1.38 % (8134)------------------------------
% 1.61/1.38 % (8134)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.61/1.38 % (8134)Termination reason: Unknown
% 1.61/1.38 % (8134)Termination phase: Property scanning
% 1.61/1.38
% 1.61/1.38 % (8134)Memory used [KB]: 1023
% 1.61/1.38 % (8134)Time elapsed: 0.003 s
% 1.61/1.38 % (8134)Instructions burned: 2 (million)
% 1.61/1.38 % (8134)------------------------------
% 1.61/1.38 % (8134)------------------------------
% 1.61/1.38 % (8131)Instruction limit reached!
% 1.61/1.38 % (8131)------------------------------
% 1.61/1.38 % (8131)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.61/1.38 % (8131)Termination reason: Unknown
% 1.61/1.38 % (8131)Termination phase: Property scanning
% 1.61/1.38
% 1.61/1.38 % (8131)Memory used [KB]: 1023
% 1.61/1.38 % (8131)Time elapsed: 0.004 s
% 1.61/1.38 % (8131)Instructions burned: 4 (million)
% 1.61/1.38 % (8131)------------------------------
% 1.61/1.38 % (8131)------------------------------
% 1.61/1.39 % (8136)Instruction limit reached!
% 1.61/1.39 % (8136)------------------------------
% 1.61/1.39 % (8136)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.61/1.39 % (8136)Termination reason: Unknown
% 1.61/1.39 % (8136)Termination phase: Saturation
% 1.61/1.39
% 1.61/1.39 % (8136)Memory used [KB]: 5628
% 1.61/1.39 % (8136)Time elapsed: 0.012 s
% 1.61/1.39 % (8136)Instructions burned: 18 (million)
% 1.61/1.39 % (8136)------------------------------
% 1.61/1.39 % (8136)------------------------------
% 1.61/1.39 % (8132)Instruction limit reached!
% 1.61/1.39 % (8132)------------------------------
% 1.61/1.39 % (8132)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.61/1.39 % (8132)Termination reason: Unknown
% 1.61/1.39 % (8132)Termination phase: Saturation
% 1.61/1.39
% 1.61/1.39 % (8132)Memory used [KB]: 5628
% 1.61/1.39 % (8132)Time elapsed: 0.016 s
% 1.61/1.39 % (8132)Instructions burned: 28 (million)
% 1.61/1.39 % (8132)------------------------------
% 1.61/1.39 % (8132)------------------------------
% 1.61/1.39 % (8137)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_8033 for (2999ds/3Mi)
% 1.61/1.39 % (8138)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_8033 for (2999ds/37Mi)
% 1.61/1.39 % (8139)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_8033 for (2999ds/15Mi)
% 1.61/1.40 % (8137)Instruction limit reached!
% 1.61/1.40 % (8137)------------------------------
% 1.61/1.40 % (8137)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.61/1.40 % (8137)Termination reason: Unknown
% 1.61/1.40 % (8137)Termination phase: Preprocessing 3
% 1.61/1.40
% 1.61/1.40 % (8137)Memory used [KB]: 1023
% 1.61/1.40 % (8137)Time elapsed: 0.003 s
% 1.61/1.40 % (8137)Instructions burned: 3 (million)
% 1.61/1.40 % (8137)------------------------------
% 1.61/1.40 % (8137)------------------------------
% 1.70/1.40 % (8139)Instruction limit reached!
% 1.70/1.40 % (8139)------------------------------
% 1.70/1.40 % (8139)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.40 % (8139)Termination reason: Unknown
% 1.70/1.40 % (8139)Termination phase: Saturation
% 1.70/1.40
% 1.70/1.40 % (8139)Memory used [KB]: 5756
% 1.70/1.40 % (8139)Time elapsed: 0.010 s
% 1.70/1.40 % (8139)Instructions burned: 17 (million)
% 1.70/1.40 % (8139)------------------------------
% 1.70/1.40 % (8139)------------------------------
% 1.70/1.40 % (8140)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_8033 for (2999ds/3Mi)
% 1.70/1.40 % (8140)Instruction limit reached!
% 1.70/1.40 % (8140)------------------------------
% 1.70/1.40 % (8140)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.40 % (8140)Termination reason: Unknown
% 1.70/1.40 % (8140)Termination phase: Property scanning
% 1.70/1.40
% 1.70/1.40 % (8140)Memory used [KB]: 1023
% 1.70/1.40 % (8140)Time elapsed: 0.003 s
% 1.70/1.40 % (8140)Instructions burned: 3 (million)
% 1.70/1.40 % (8140)------------------------------
% 1.70/1.40 % (8140)------------------------------
% 1.70/1.41 % (8141)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_8033 for (2999ds/1041Mi)
% 1.70/1.41 % (8142)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_8033 for (2999ds/7Mi)
% 1.70/1.41 % (8138)Instruction limit reached!
% 1.70/1.41 % (8138)------------------------------
% 1.70/1.41 % (8138)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.41 % (8138)Termination reason: Unknown
% 1.70/1.41 % (8138)Termination phase: Saturation
% 1.70/1.41
% 1.70/1.41 % (8138)Memory used [KB]: 5628
% 1.70/1.41 % (8138)Time elapsed: 0.019 s
% 1.70/1.41 % (8138)Instructions burned: 37 (million)
% 1.70/1.41 % (8138)------------------------------
% 1.70/1.41 % (8138)------------------------------
% 1.70/1.41 % (8142)Instruction limit reached!
% 1.70/1.41 % (8142)------------------------------
% 1.70/1.41 % (8142)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.41 % (8142)Termination reason: Unknown
% 1.70/1.41 % (8142)Termination phase: Saturation
% 1.70/1.41
% 1.70/1.41 % (8142)Memory used [KB]: 1023
% 1.70/1.41 % (8142)Time elapsed: 0.005 s
% 1.70/1.41 % (8142)Instructions burned: 7 (million)
% 1.70/1.41 % (8142)------------------------------
% 1.70/1.41 % (8142)------------------------------
% 1.70/1.42 % (8143)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_8033 for (2999ds/16Mi)
% 1.70/1.42 % (8144)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_8033 for (2999ds/3Mi)
% 1.70/1.42 % (8144)Instruction limit reached!
% 1.70/1.42 % (8144)------------------------------
% 1.70/1.42 % (8144)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.42 % (8144)Termination reason: Unknown
% 1.70/1.42 % (8144)Termination phase: Preprocessing 3
% 1.70/1.42
% 1.70/1.42 % (8144)Memory used [KB]: 1023
% 1.70/1.42 % (8144)Time elapsed: 0.003 s
% 1.70/1.42 % (8144)Instructions burned: 3 (million)
% 1.70/1.42 % (8144)------------------------------
% 1.70/1.42 % (8144)------------------------------
% 1.70/1.43 % (8145)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_8033 for (2999ds/3Mi)
% 1.70/1.43 % (8143)Instruction limit reached!
% 1.70/1.43 % (8143)------------------------------
% 1.70/1.43 % (8143)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.43 % (8143)Termination reason: Unknown
% 1.70/1.43 % (8143)Termination phase: Saturation
% 1.70/1.43
% 1.70/1.43 % (8143)Memory used [KB]: 5756
% 1.70/1.43 % (8143)Time elapsed: 0.010 s
% 1.70/1.43 % (8143)Instructions burned: 16 (million)
% 1.70/1.43 % (8143)------------------------------
% 1.70/1.43 % (8143)------------------------------
% 1.70/1.43 % (8145)Instruction limit reached!
% 1.70/1.43 % (8145)------------------------------
% 1.70/1.43 % (8145)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.43 % (8145)Termination reason: Unknown
% 1.70/1.43 % (8145)Termination phase: Preprocessing 3
% 1.70/1.43
% 1.70/1.43 % (8145)Memory used [KB]: 1023
% 1.70/1.43 % (8145)Time elapsed: 0.003 s
% 1.70/1.43 % (8145)Instructions burned: 3 (million)
% 1.70/1.43 % (8145)------------------------------
% 1.70/1.43 % (8145)------------------------------
% 1.70/1.43 % (8146)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_8033 for (2999ds/7Mi)
% 1.70/1.43 % (8146)Instruction limit reached!
% 1.70/1.43 % (8146)------------------------------
% 1.70/1.43 % (8146)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.43 % (8146)Termination reason: Unknown
% 1.70/1.43 % (8146)Termination phase: Saturation
% 1.70/1.43
% 1.70/1.43 % (8146)Memory used [KB]: 5500
% 1.70/1.43 % (8146)Time elapsed: 0.005 s
% 1.70/1.43 % (8146)Instructions burned: 7 (million)
% 1.70/1.43 % (8146)------------------------------
% 1.70/1.43 % (8146)------------------------------
% 1.70/1.44 % (8147)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_8033 for (2999ds/3Mi)
% 1.70/1.44 % (8147)Instruction limit reached!
% 1.70/1.44 % (8147)------------------------------
% 1.70/1.44 % (8147)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.44 % (8147)Termination reason: Unknown
% 1.70/1.44 % (8147)Termination phase: Property scanning
% 1.70/1.44
% 1.70/1.44 % (8147)Memory used [KB]: 1023
% 1.70/1.44 % (8147)Time elapsed: 0.003 s
% 1.70/1.44 % (8147)Instructions burned: 4 (million)
% 1.70/1.44 % (8147)------------------------------
% 1.70/1.44 % (8147)------------------------------
% 1.70/1.44 % (8148)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_8033 for (2999ds/4Mi)
% 1.70/1.44 % (8149)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_8033 for (2999ds/18Mi)
% 1.70/1.45 % (8148)Instruction limit reached!
% 1.70/1.45 % (8148)------------------------------
% 1.70/1.45 % (8148)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.45 % (8148)Termination reason: Unknown
% 1.70/1.45 % (8148)Termination phase: Saturation
% 1.70/1.45
% 1.70/1.45 % (8148)Memory used [KB]: 5500
% 1.70/1.45 % (8148)Time elapsed: 0.004 s
% 1.70/1.45 % (8148)Instructions burned: 5 (million)
% 1.70/1.45 % (8148)------------------------------
% 1.70/1.45 % (8148)------------------------------
% 1.70/1.45 % (8150)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_8033 for (2999ds/710Mi)
% 1.70/1.45 % (8149)Instruction limit reached!
% 1.70/1.45 % (8149)------------------------------
% 1.70/1.45 % (8149)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.45 % (8149)Termination reason: Unknown
% 1.70/1.45 % (8149)Termination phase: Saturation
% 1.70/1.45
% 1.70/1.45 % (8149)Memory used [KB]: 5628
% 1.70/1.45 % (8149)Time elapsed: 0.010 s
% 1.70/1.45 % (8149)Instructions burned: 18 (million)
% 1.70/1.45 % (8149)------------------------------
% 1.70/1.45 % (8149)------------------------------
% 1.70/1.46 % (8151)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_8033 for (2999ds/6Mi)
% 1.70/1.46 % (8151)Instruction limit reached!
% 1.70/1.46 % (8151)------------------------------
% 1.70/1.46 % (8151)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.46 % (8151)Termination reason: Unknown
% 1.70/1.46 % (8151)Termination phase: Saturation
% 1.70/1.46
% 1.70/1.46 % (8151)Memory used [KB]: 5500
% 1.70/1.46 % (8151)Time elapsed: 0.005 s
% 1.70/1.46 % (8151)Instructions burned: 7 (million)
% 1.70/1.46 % (8151)------------------------------
% 1.70/1.46 % (8151)------------------------------
% 1.70/1.46 % (8152)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_8033 for (2999ds/902Mi)
% 1.70/1.47 % (8130)Instruction limit reached!
% 1.70/1.47 % (8130)------------------------------
% 1.70/1.47 % (8130)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.47 % (8130)Termination reason: Unknown
% 1.70/1.47 % (8130)Termination phase: Saturation
% 1.70/1.47
% 1.70/1.47 % (8130)Memory used [KB]: 6524
% 1.70/1.47 % (8130)Time elapsed: 0.091 s
% 1.70/1.47 % (8130)Instructions burned: 183 (million)
% 1.70/1.47 % (8130)------------------------------
% 1.70/1.47 % (8130)------------------------------
% 1.70/1.47 % (8153)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_8033 for (2999ds/21Mi)
% 1.70/1.48 % (8154)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_8033 for (2999ds/5Mi)
% 1.70/1.48 % (8154)Instruction limit reached!
% 1.70/1.48 % (8154)------------------------------
% 1.70/1.48 % (8154)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.48 % (8154)Termination reason: Unknown
% 1.70/1.48 % (8154)Termination phase: Saturation
% 1.70/1.48
% 1.70/1.48 % (8154)Memory used [KB]: 5500
% 1.70/1.48 % (8154)Time elapsed: 0.004 s
% 1.70/1.48 % (8154)Instructions burned: 5 (million)
% 1.70/1.48 % (8154)------------------------------
% 1.70/1.48 % (8154)------------------------------
% 1.70/1.48 % (8153)Instruction limit reached!
% 1.70/1.48 % (8153)------------------------------
% 1.70/1.48 % (8153)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.48 % (8153)Termination reason: Unknown
% 1.70/1.48 % (8153)Termination phase: Saturation
% 1.70/1.48
% 1.70/1.48 % (8153)Memory used [KB]: 5628
% 1.70/1.48 % (8153)Time elapsed: 0.013 s
% 1.70/1.48 % (8153)Instructions burned: 21 (million)
% 1.70/1.48 % (8153)------------------------------
% 1.70/1.48 % (8153)------------------------------
% 1.70/1.48 % (8155)lrs+2_1:1_cnfonf=lazy_not_gen_be_off:cs=on:fe=off:hud=10:inj=on:ins=3:plsq=on:plsqc=1:sd=10:ss=axioms:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_8033 for (2999ds/6Mi)
% 1.70/1.49 % (8155)Instruction limit reached!
% 1.70/1.49 % (8155)------------------------------
% 1.70/1.49 % (8155)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.49 % (8155)Termination reason: Unknown
% 1.70/1.49 % (8155)Termination phase: Saturation
% 1.70/1.49
% 1.70/1.49 % (8155)Memory used [KB]: 5500
% 1.70/1.49 % (8155)Time elapsed: 0.005 s
% 1.70/1.49 % (8155)Instructions burned: 8 (million)
% 1.70/1.49 % (8155)------------------------------
% 1.70/1.49 % (8155)------------------------------
% 1.70/1.49 % (8156)lrs+1002_1:128_au=on:c=on:fsr=off:piset=equals:i=377:si=on:rtra=on_0 on DTF2THF_8033 for (2998ds/377Mi)
% 1.70/1.50 % (8157)dis+1010_1:4_atotf=0.2:c=on:cbe=off:cnfonf=lazy_simp:fe=off:ins=2:ntd=on:s2a=on:s2at=5.0:sgt=5:ss=axioms:st=1.5:i=779:si=on:rtra=on_0 on DTF2THF_8033 for (2998ds/779Mi)
% 1.70/1.50 % (8158)lrs+10_1:1_cnfonf=lazy_not_be_gen:ntd=on:sp=const_min:ss=axioms:sup=off:i=19:si=on:rtra=on_0 on DTF2THF_8033 for (2998ds/19Mi)
% 1.70/1.51 % (8158)Instruction limit reached!
% 1.70/1.51 % (8158)------------------------------
% 1.70/1.51 % (8158)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.51 % (8158)Termination reason: Unknown
% 1.70/1.51 % (8158)Termination phase: Saturation
% 1.70/1.51
% 1.70/1.51 % (8158)Memory used [KB]: 5500
% 1.70/1.51 % (8158)Time elapsed: 0.011 s
% 1.70/1.51 % (8158)Instructions burned: 21 (million)
% 1.70/1.51 % (8158)------------------------------
% 1.70/1.51 % (8158)------------------------------
% 1.70/1.51 % (8135)Instruction limit reached!
% 1.70/1.51 % (8135)------------------------------
% 1.70/1.51 % (8135)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.51 % (8135)Termination reason: Unknown
% 1.70/1.51 % (8135)Termination phase: Saturation
% 1.70/1.51
% 1.70/1.51 % (8135)Memory used [KB]: 6780
% 1.70/1.51 % (8135)Time elapsed: 0.139 s
% 1.70/1.51 % (8135)Instructions burned: 275 (million)
% 1.70/1.51 % (8135)------------------------------
% 1.70/1.51 % (8135)------------------------------
% 1.70/1.53 % (8159)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=879:si=on:rtra=on_0 on DTF2THF_8033 for (2998ds/879Mi)
% 1.70/1.53 % (8160)dis+1002_1:128_acc=on:er=filter:i=17:si=on:rtra=on_0 on DTF2THF_8033 for (2998ds/17Mi)
% 1.70/1.54 % (8160)Instruction limit reached!
% 1.70/1.54 % (8160)------------------------------
% 1.70/1.54 % (8160)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.54 % (8160)Termination reason: Unknown
% 1.70/1.54 % (8160)Termination phase: Saturation
% 1.70/1.54
% 1.70/1.54 % (8160)Memory used [KB]: 5756
% 1.70/1.54 % (8160)Time elapsed: 0.011 s
% 1.70/1.54 % (8160)Instructions burned: 17 (million)
% 1.70/1.54 % (8160)------------------------------
% 1.70/1.54 % (8160)------------------------------
% 1.70/1.56 % (8161)ott+21_1:1_apa=on:au=on:cnfonf=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_8033 for (2998ds/3Mi)
% 1.70/1.56 % (8161)Instruction limit reached!
% 1.70/1.56 % (8161)------------------------------
% 1.70/1.56 % (8161)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.56 % (8161)Termination reason: Unknown
% 1.70/1.56 % (8161)Termination phase: Naming
% 1.70/1.56
% 1.70/1.56 % (8161)Memory used [KB]: 1023
% 1.70/1.56 % (8161)Time elapsed: 0.003 s
% 1.70/1.56 % (8161)Instructions burned: 3 (million)
% 1.70/1.56 % (8161)------------------------------
% 1.70/1.56 % (8161)------------------------------
% 1.70/1.56 % (8141)First to succeed.
% 1.70/1.57 % (8162)lrs+1010_1:8_cnfonf=off:hud=1:inj=on:tnu=5:i=30:si=on:rtra=on_0 on DTF2THF_8033 for (2998ds/30Mi)
% 1.70/1.58 % (8141)Refutation found. Thanks to Tanya!
% 1.70/1.58 % SZS status Theorem for DTF2THF_8033
% 1.70/1.58 % SZS output start Proof for DTF2THF_8033
% 1.70/1.58 thf(type_def_5, type, a: $tType).
% 1.70/1.58 thf(func_def_0, type, a: $tType).
% 1.70/1.58 thf(func_def_1, type, cP: a > a > a).
% 1.70/1.58 thf(func_def_2, type, cG: a > $o).
% 1.70/1.58 thf(func_def_3, type, cX: a > $o).
% 1.70/1.58 thf(func_def_4, type, cR: a > a).
% 1.70/1.58 thf(func_def_5, type, cL: a > a).
% 1.70/1.58 thf(func_def_6, type, cF: a > $o).
% 1.70/1.58 thf(func_def_7, type, cZ: a).
% 1.70/1.58 thf(func_def_24, type, ph1: !>[X0: $tType]:(X0)).
% 1.70/1.58 thf(func_def_25, type, sK2: a).
% 1.70/1.58 thf(func_def_26, type, sK3: a).
% 1.70/1.58 thf(func_def_27, type, sK4: a).
% 1.70/1.58 thf(func_def_28, type, sK5: a > $o).
% 1.70/1.58 thf(func_def_29, type, sK6: a).
% 1.70/1.58 thf(func_def_30, type, sK7: a).
% 1.70/1.58 thf(func_def_31, type, sK8: a).
% 1.70/1.58 thf(func_def_32, type, sK9: a).
% 1.70/1.58 thf(func_def_33, type, sK10: a > $o).
% 1.70/1.58 thf(func_def_34, type, sK11: a > $o).
% 1.70/1.58 thf(func_def_35, type, sK12: a).
% 1.70/1.58 thf(func_def_36, type, sK13: a).
% 1.70/1.58 thf(func_def_37, type, sK14: a > $o).
% 1.70/1.58 thf(func_def_38, type, sK15: a).
% 1.70/1.58 thf(func_def_39, type, sK16: a > $o).
% 1.70/1.58 thf(func_def_40, type, sK17: a).
% 1.70/1.58 thf(func_def_41, type, sK18: a).
% 1.70/1.58 thf(func_def_42, type, sK19: a).
% 1.70/1.58 thf(f1297,plain,(
% 1.70/1.58 $false),
% 1.70/1.58 inference(avatar_sat_refutation,[status(thm)],[f36,f70,f227,f561,f799,f1163,f1296])).
% 1.70/1.58 thf(f1296,plain,(
% 1.70/1.58 ~spl0_2 | ~spl0_5),
% 1.70/1.58 inference(avatar_contradiction_clause,[status(thm)],[f1295])).
% 1.70/1.58 thf(f1295,plain,(
% 1.70/1.58 $false | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(trivial_inequality_removal,[status(thm)],[f1294])).
% 1.70/1.58 thf(f1294,plain,(
% 1.70/1.58 ($false = $true) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f1293])).
% 1.70/1.58 thf(f1293,plain,(
% 1.70/1.58 ($true = (~ $true)) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(forward_demodulation,[status(thm)],[f1291,f1292])).
% 1.70/1.58 thf(f1292,plain,(
% 1.70/1.58 ((sK5 @ sK3) = $true) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f1290])).
% 1.70/1.58 thf(f1290,plain,(
% 1.70/1.58 ($true = ((sK5 @ sK3) & $true)) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f1255,f1287])).
% 1.70/1.58 thf(f1287,plain,(
% 1.70/1.58 ($true = (!! @ a @ (^[Y0 : a]: ((sK5 @ Y0) => (sK5 @ (cL @ Y0)))))) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f1255])).
% 1.70/1.58 thf(f1255,plain,(
% 1.70/1.58 (((sK5 @ sK3) & (!! @ a @ (^[Y0 : a]: ((sK5 @ Y0) => (sK5 @ (cL @ Y0)))))) = $true) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f1222])).
% 1.70/1.58 thf(f1222,plain,(
% 1.70/1.58 ((((sK5 @ sK3) & (!! @ a @ (^[Y0 : a]: ((sK5 @ Y0) => (sK5 @ (cL @ Y0)))))) => (?? @ a @ (^[Y0 : a]: (((cR @ Y0) = sK4) & (sK5 @ Y0))))) = $false) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f1219])).
% 1.70/1.58 thf(f1219,plain,(
% 1.70/1.58 ($false = ((^[Y0 : a > $o]: (((Y0 @ sK3) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK4) & (Y0 @ Y1)))))) @ sK5)) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(sigma_clausification,[status(thm)],[f1216])).
% 1.70/1.58 thf(f1216,plain,(
% 1.70/1.58 ((!! @ (a > $o) @ (^[Y0 : a > $o]: (((Y0 @ sK3) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK4) & (Y0 @ Y1))))))) = $false) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(not_proxy_clausification,[status(thm)],[f1191])).
% 1.70/1.58 thf(f1191,plain,(
% 1.70/1.58 ($true = (~ (!! @ (a > $o) @ (^[Y0 : a > $o]: (((Y0 @ sK3) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK4) & (Y0 @ Y1))))))))) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f1190])).
% 1.70/1.58 thf(f1190,plain,(
% 1.70/1.58 (((!! @ (a > $o) @ (^[Y0 : a > $o]: (((Y0 @ sK3) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK4) & (Y0 @ Y1))))))) => $false) = $true) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(superposition,[status(thm)],[f1168,f1184])).
% 1.70/1.58 thf(f1184,plain,(
% 1.70/1.58 ((cX @ sK4) = $false) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f1178])).
% 1.70/1.58 thf(f1178,plain,(
% 1.70/1.58 (((!! @ (a > $o) @ (^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK3)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK4) & (Y0 @ Y1))))))) => (cX @ sK4)) = $false) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f1174])).
% 1.70/1.58 thf(f1174,plain,(
% 1.70/1.58 ($false = ((^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2))))) & (Y1 @ sK3)) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))) @ sK4)) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(sigma_clausification,[status(thm)],[f1170])).
% 1.70/1.58 thf(f1170,plain,(
% 1.70/1.58 ((!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2))))) & (Y1 @ sK3)) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))) = $false) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f1169])).
% 1.70/1.58 thf(f1169,plain,(
% 1.70/1.58 (((!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2))))) & (Y1 @ sK3)) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))) & $true) = $false) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(superposition,[status(thm)],[f855,f66])).
% 1.70/1.58 thf(f66,plain,(
% 1.70/1.58 ($true = (cF @ (cP @ sK3 @ sK2))) | ~spl0_5),
% 1.70/1.58 inference(avatar_component_clause,[status(thm)],[f65])).
% 1.70/1.58 thf(f65,definition,(
% 1.70/1.58 spl0_5 <=> ($true = (cF @ (cP @ sK3 @ sK2)))),
% 1.70/1.58 introduced(definition,[new_symbols(naming,[spl0_5])],[avatar_definition])).
% 1.70/1.58 thf(f855,plain,(
% 1.70/1.58 ( ! [X1 : a] : (($false = ((!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2))))) & (Y1 @ X1)) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))) & (cF @ (cP @ X1 @ sK2))))) ) | ~spl0_2),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f854])).
% 1.70/1.58 thf(f854,plain,(
% 1.70/1.58 ( ! [X1 : a] : (($false = ((^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cF @ (cP @ Y0 @ sK2)))) @ X1))) ) | ~spl0_2),
% 1.70/1.58 inference(pi_clausification,[status(thm)],[f849])).
% 1.70/1.58 thf(f849,plain,(
% 1.70/1.58 ($false = (?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cF @ (cP @ Y0 @ sK2)))))) | ~spl0_2),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f848])).
% 1.70/1.58 thf(f848,plain,(
% 1.70/1.58 ($false = ($false | (?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cF @ (cP @ Y0 @ sK2))))))) | ~spl0_2),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f35,f847])).
% 1.70/1.58 thf(f847,plain,(
% 1.70/1.58 ($false = (?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cG @ (cP @ Y0 @ sK2)))))) | ~spl0_2),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f35])).
% 1.70/1.58 thf(f35,plain,(
% 1.70/1.58 ($false = ((?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cG @ (cP @ Y0 @ sK2))))) | (?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cF @ (cP @ Y0 @ sK2))))))) | ~spl0_2),
% 1.70/1.58 inference(avatar_component_clause,[status(thm)],[f34])).
% 1.70/1.58 thf(f34,definition,(
% 1.70/1.58 spl0_2 <=> ($false = ((?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cG @ (cP @ Y0 @ sK2))))) | (?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cF @ (cP @ Y0 @ sK2)))))))),
% 1.70/1.58 introduced(definition,[new_symbols(naming,[spl0_2])],[avatar_definition])).
% 1.70/1.58 thf(f1168,plain,(
% 1.70/1.58 ( ! [X1 : a] : ((((!! @ (a > $o) @ (^[Y0 : a > $o]: (((Y0 @ sK3) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = X1) & (Y0 @ Y1))))))) => (cX @ X1)) = $true)) ) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f1167])).
% 1.70/1.58 thf(f1167,plain,(
% 1.70/1.58 ( ! [X1 : a] : ((((^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK3) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))) @ X1) = $true)) ) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(pi_clausification,[status(thm)],[f1166])).
% 1.70/1.58 thf(f1166,plain,(
% 1.70/1.58 ($true = (!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK3) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))))) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f1165])).
% 1.70/1.58 thf(f1165,plain,(
% 1.70/1.58 ($true = ($true & (!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK3) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))))) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f1164])).
% 1.70/1.58 thf(f1164,plain,(
% 1.70/1.58 ((((cG @ (cP @ sK3 @ sK2)) | $true) & (!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK3) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))))) = $true) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f807,f66])).
% 1.70/1.58 thf(f807,plain,(
% 1.70/1.58 ($true = (((cG @ (cP @ sK3 @ sK2)) | (cF @ (cP @ sK3 @ sK2))) & (!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK3) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))))) | ~spl0_2),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f806])).
% 1.70/1.58 thf(f806,plain,(
% 1.70/1.58 ($true = ((^[Y0 : a]: (((cG @ (cP @ Y0 @ sK2)) | (cF @ (cP @ Y0 @ sK2))) & (!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((Y2 @ Y0) & (!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3)))))) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))))) @ sK3)) | ~spl0_2),
% 1.70/1.58 inference(sigma_clausification,[status(thm)],[f800])).
% 1.70/1.58 thf(f800,plain,(
% 1.70/1.58 ($false != (?? @ a @ (^[Y0 : a]: (((cG @ (cP @ Y0 @ sK2)) | (cF @ (cP @ Y0 @ sK2))) & (!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((Y2 @ Y0) & (!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3)))))) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))))))) | ~spl0_2),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f20,f35])).
% 1.70/1.58 thf(f20,plain,(
% 1.70/1.58 (((?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cG @ (cP @ Y0 @ sK2))))) | (?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cF @ (cP @ Y0 @ sK2)))))) != (?? @ a @ (^[Y0 : a]: (((cG @ (cP @ Y0 @ sK2)) | (cF @ (cP @ Y0 @ sK2))) & (!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((Y2 @ Y0) & (!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3)))))) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1))))))))),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f19])).
% 1.70/1.58 thf(f19,plain,(
% 1.70/1.58 (((^[Y0 : a]: (?? @ a @ (^[Y1 : a]: (((cG @ (cP @ Y1 @ Y0)) | (cF @ (cP @ Y1 @ Y0))) & (!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((Y3 @ Y1) & (!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4)))))) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))))))) @ sK2) != ((^[Y0 : a]: ((?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4))))) & (Y3 @ Y1)) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))) & (cG @ (cP @ Y1 @ Y0))))) | (?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4))))) & (Y3 @ Y1)) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))) & (cF @ (cP @ Y1 @ Y0))))))) @ sK2))),
% 1.70/1.58 inference(negative_extensionality,[status(thm)],[f14])).
% 1.70/1.58 thf(f14,plain,(
% 1.70/1.58 ((^[Y0 : a]: ((?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4))))) & (Y3 @ Y1)) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))) & (cG @ (cP @ Y1 @ Y0))))) | (?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4))))) & (Y3 @ Y1)) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))) & (cF @ (cP @ Y1 @ Y0))))))) != (^[Y0 : a]: (?? @ a @ (^[Y1 : a]: (((cG @ (cP @ Y1 @ Y0)) | (cF @ (cP @ Y1 @ Y0))) & (!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((Y3 @ Y1) & (!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4)))))) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))))))))),
% 1.70/1.58 inference(equality_proxy_clausification,[status(thm)],[f13])).
% 1.70/1.58 thf(f13,plain,(
% 1.70/1.58 (((^[Y0 : a]: (?? @ a @ (^[Y1 : a]: (((cG @ (cP @ Y1 @ Y0)) | (cF @ (cP @ Y1 @ Y0))) & (!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((Y3 @ Y1) & (!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4)))))) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))))))) = (^[Y0 : a]: ((?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4))))) & (Y3 @ Y1)) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))) & (cG @ (cP @ Y1 @ Y0))))) | (?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4))))) & (Y3 @ Y1)) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))) & (cF @ (cP @ Y1 @ Y0)))))))) = $false)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f12])).
% 1.70/1.58 thf(f12,plain,(
% 1.70/1.58 (($true => ((^[Y0 : a]: (?? @ a @ (^[Y1 : a]: (((cG @ (cP @ Y1 @ Y0)) | (cF @ (cP @ Y1 @ Y0))) & (!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((Y3 @ Y1) & (!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4)))))) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))))))) = (^[Y0 : a]: ((?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4))))) & (Y3 @ Y1)) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))) & (cG @ (cP @ Y1 @ Y0))))) | (?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4))))) & (Y3 @ Y1)) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))) & (cF @ (cP @ Y1 @ Y0))))))))) = $false)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f7,f11])).
% 1.70/1.58 thf(f11,plain,(
% 1.70/1.58 (((((((cZ = (cL @ cZ)) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((cL @ (cP @ Y0 @ Y1)) = Y0)))))) & (!! @ a @ (^[Y0 : a]: ((~ (cZ = Y0)) = ((cP @ (cL @ Y0) @ (cR @ Y0)) = Y0))))) & (cZ = (cR @ cZ))) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((cR @ (cP @ Y1 @ Y0)) = Y0)))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) => (Y0 @ (cL @ Y2))))) & (Y0 @ Y1)))) => (Y0 @ cZ))))) = $true)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f7])).
% 1.70/1.58 thf(f7,plain,(
% 1.70/1.58 ($false = (((((((cZ = (cL @ cZ)) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((cL @ (cP @ Y0 @ Y1)) = Y0)))))) & (!! @ a @ (^[Y0 : a]: ((~ (cZ = Y0)) = ((cP @ (cL @ Y0) @ (cR @ Y0)) = Y0))))) & (cZ = (cR @ cZ))) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((cR @ (cP @ Y1 @ Y0)) = Y0)))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) => (Y0 @ (cL @ Y2))))) & (Y0 @ Y1)))) => (Y0 @ cZ))))) => ((^[Y0 : a]: (?? @ a @ (^[Y1 : a]: (((cG @ (cP @ Y1 @ Y0)) | (cF @ (cP @ Y1 @ Y0))) & (!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((Y3 @ Y1) & (!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4)))))) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))))))) = (^[Y0 : a]: ((?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4))))) & (Y3 @ Y1)) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))) & (cG @ (cP @ Y1 @ Y0))))) | (?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4))))) & (Y3 @ Y1)) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))) & (cF @ (cP @ Y1 @ Y0))))))))))),
% 1.70/1.58 inference(not_proxy_clausification,[status(thm)],[f6])).
% 1.70/1.58 thf(f6,plain,(
% 1.70/1.58 ($true = (~ (((((((cZ = (cL @ cZ)) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((cL @ (cP @ Y0 @ Y1)) = Y0)))))) & (!! @ a @ (^[Y0 : a]: ((~ (cZ = Y0)) = ((cP @ (cL @ Y0) @ (cR @ Y0)) = Y0))))) & (cZ = (cR @ cZ))) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((cR @ (cP @ Y1 @ Y0)) = Y0)))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) => (Y0 @ (cL @ Y2))))) & (Y0 @ Y1)))) => (Y0 @ cZ))))) => ((^[Y0 : a]: (?? @ a @ (^[Y1 : a]: (((cG @ (cP @ Y1 @ Y0)) | (cF @ (cP @ Y1 @ Y0))) & (!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((Y3 @ Y1) & (!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4)))))) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))))))) = (^[Y0 : a]: ((?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4))))) & (Y3 @ Y1)) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))) & (cG @ (cP @ Y1 @ Y0))))) | (?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4))))) & (Y3 @ Y1)) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))) & (cF @ (cP @ Y1 @ Y0)))))))))))),
% 1.70/1.58 inference(cnf_transformation,[status(thm)],[f5])).
% 1.70/1.58 thf(f5,plain,(
% 1.70/1.58 ($true = (~ (((((((cZ = (cL @ cZ)) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((cL @ (cP @ Y0 @ Y1)) = Y0)))))) & (!! @ a @ (^[Y0 : a]: ((~ (cZ = Y0)) = ((cP @ (cL @ Y0) @ (cR @ Y0)) = Y0))))) & (cZ = (cR @ cZ))) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((cR @ (cP @ Y1 @ Y0)) = Y0)))))) & (!! @ (a > $o) @ (^[Y0 : a > $o]: ((?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((Y0 @ Y2) => (Y0 @ (cL @ Y2))))) & (Y0 @ Y1)))) => (Y0 @ cZ))))) => ((^[Y0 : a]: (?? @ a @ (^[Y1 : a]: (((cG @ (cP @ Y1 @ Y0)) | (cF @ (cP @ Y1 @ Y0))) & (!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((Y3 @ Y1) & (!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4)))))) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))))))) = (^[Y0 : a]: ((?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4))))) & (Y3 @ Y1)) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))) & (cG @ (cP @ Y1 @ Y0))))) | (?? @ a @ (^[Y1 : a]: ((!! @ a @ (^[Y2 : a]: ((!! @ (a > $o) @ (^[Y3 : a > $o]: (((!! @ a @ (^[Y4 : a]: ((Y3 @ Y4) => (Y3 @ (cL @ Y4))))) & (Y3 @ Y1)) => (?? @ a @ (^[Y4 : a]: (((cR @ Y4) = Y2) & (Y3 @ Y4))))))) => (cX @ Y2)))) & (cF @ (cP @ Y1 @ Y0)))))))))))),
% 1.70/1.58 inference(fool_elimination,[status(thm)],[f4])).
% 1.70/1.58 thf(f4,plain,(
% 1.70/1.58 ~((! [X0 : a > $o] : (? [X1 : a] : ((X0 @ X1) & ! [X2 : a] : ((X0 @ X2) => (X0 @ (cL @ X2)))) => (X0 @ cZ)) & ! [X3 : a,X4 : a] : ((cR @ (cP @ X3 @ X4)) = X4) & (cZ = (cR @ cZ)) & ! [X5 : a] : ((cZ != X5) <=> ((cP @ (cL @ X5) @ (cR @ X5)) = X5)) & ! [X6 : a,X7 : a] : ((cL @ (cP @ X7 @ X6)) = X7) & (cZ = (cL @ cZ))) => ((^[X8 : a] : (? [X9 : a] : (! [X10 : a] : (! [X11 : a > $o] : ((! [X12 : a] : ((X11 @ X12) => (X11 @ (cL @ X12))) & (X11 @ X9)) => ? [X13 : a] : ((X11 @ X13) & ((cR @ X13) = X10))) => (cX @ X10)) & ((cF @ (cP @ X9 @ X8)) | (cG @ (cP @ X9 @ X8)))))) = (^[X14 : a] : (? [X15 : a] : ((cF @ (cP @ X15 @ X14)) & ! [X16 : a] : (! [X17 : a > $o] : (((X17 @ X15) & ! [X18 : a] : ((X17 @ X18) => (X17 @ (cL @ X18)))) => ? [X19 : a] : ((X17 @ X19) & ((cR @ X19) = X16))) => (cX @ X16))) | ? [X20 : a] : ((cG @ (cP @ X20 @ X14)) & ! [X21 : a] : (! [X22 : a > $o] : (((X22 @ X20) & ! [X23 : a] : ((X22 @ X23) => (X22 @ (cL @ X23)))) => ? [X24 : a] : ((X22 @ X24) & ((cR @ X24) = X21))) => (cX @ X21)))))))),
% 1.70/1.58 inference(rectify,[status(thm)],[f2])).
% 1.70/1.58 thf(f2,negated_conjecture,(
% 1.70/1.58 ~((! [X3 : a > $o] : (? [X2 : a] : ((X3 @ X2) & ! [X4 : a] : ((X3 @ X4) => (X3 @ (cL @ X4)))) => (X3 @ cZ)) & ! [X0 : a,X1 : a] : ((cR @ (cP @ X0 @ X1)) = X1) & (cZ = (cR @ cZ)) & ! [X2 : a] : ((cZ != X2) <=> ((cP @ (cL @ X2) @ (cR @ X2)) = X2)) & ! [X1 : a,X0 : a] : ((cL @ (cP @ X0 @ X1)) = X0) & (cZ = (cL @ cZ))) => ((^[X1 : a] : (? [X0 : a] : (! [X5 : a] : (! [X3 : a > $o] : ((! [X6 : a] : ((X3 @ X6) => (X3 @ (cL @ X6))) & (X3 @ X0)) => ? [X7 : a] : ((X3 @ X7) & ((cR @ X7) = X5))) => (cX @ X5)) & ((cF @ (cP @ X0 @ X1)) | (cG @ (cP @ X0 @ X1)))))) = (^[X6 : a] : (? [X0 : a] : ((cF @ (cP @ X0 @ X6)) & ! [X8 : a] : (! [X3 : a > $o] : (((X3 @ X0) & ! [X9 : a] : ((X3 @ X9) => (X3 @ (cL @ X9)))) => ? [X7 : a] : ((X3 @ X7) & ((cR @ X7) = X8))) => (cX @ X8))) | ? [X0 : a] : ((cG @ (cP @ X0 @ X6)) & ! [X10 : a] : (! [X3 : a > $o] : (((X3 @ X0) & ! [X9 : a] : ((X3 @ X9) => (X3 @ (cL @ X9)))) => ? [X7 : a] : ((X3 @ X7) & ((cR @ X7) = X10))) => (cX @ X10)))))))),
% 1.70/1.58 inference(negated_conjecture,[status(cth)],[f1])).
% 1.70/1.58 thf(f1,conjecture,(
% 1.70/1.58 (! [X3 : a > $o] : (? [X2 : a] : ((X3 @ X2) & ! [X4 : a] : ((X3 @ X4) => (X3 @ (cL @ X4)))) => (X3 @ cZ)) & ! [X0 : a,X1 : a] : ((cR @ (cP @ X0 @ X1)) = X1) & (cZ = (cR @ cZ)) & ! [X2 : a] : ((cZ != X2) <=> ((cP @ (cL @ X2) @ (cR @ X2)) = X2)) & ! [X1 : a,X0 : a] : ((cL @ (cP @ X0 @ X1)) = X0) & (cZ = (cL @ cZ))) => ((^[X1 : a] : (? [X0 : a] : (! [X5 : a] : (! [X3 : a > $o] : ((! [X6 : a] : ((X3 @ X6) => (X3 @ (cL @ X6))) & (X3 @ X0)) => ? [X7 : a] : ((X3 @ X7) & ((cR @ X7) = X5))) => (cX @ X5)) & ((cF @ (cP @ X0 @ X1)) | (cG @ (cP @ X0 @ X1)))))) = (^[X6 : a] : (? [X0 : a] : ((cF @ (cP @ X0 @ X6)) & ! [X8 : a] : (! [X3 : a > $o] : (((X3 @ X0) & ! [X9 : a] : ((X3 @ X9) => (X3 @ (cL @ X9)))) => ? [X7 : a] : ((X3 @ X7) & ((cR @ X7) = X8))) => (cX @ X8))) | ? [X0 : a] : ((cG @ (cP @ X0 @ X6)) & ! [X10 : a] : (! [X3 : a > $o] : (((X3 @ X0) & ! [X9 : a] : ((X3 @ X9) => (X3 @ (cL @ X9)))) => ? [X7 : a] : ((X3 @ X7) & ((cR @ X7) = X10))) => (cX @ X10))))))),
% 1.70/1.58 file('/export/starexec/sandbox2/tmp/tmp.Td4sovfI6f/DTF2THF_8033.p',cPU_X2310A_pme)).
% 1.70/1.58 thf(f1291,plain,(
% 1.70/1.58 ((~ (sK5 @ sK3)) = $true) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f1289])).
% 1.70/1.58 thf(f1289,plain,(
% 1.70/1.58 ((~ ($true & (sK5 @ sK3))) = $true) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f1263,f1287])).
% 1.70/1.58 thf(f1263,plain,(
% 1.70/1.58 ((~ ((!! @ a @ (^[Y0 : a]: ((sK5 @ Y0) => (sK5 @ (cL @ Y0))))) & (sK5 @ sK3))) = $true) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f1261])).
% 1.70/1.58 thf(f1261,plain,(
% 1.70/1.58 ($true = (((!! @ a @ (^[Y0 : a]: ((sK5 @ Y0) => (sK5 @ (cL @ Y0))))) & (sK5 @ sK3)) => $false)) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(superposition,[status(thm)],[f1193,f1254])).
% 1.70/1.58 thf(f1254,plain,(
% 1.70/1.58 ($false = (?? @ a @ (^[Y0 : a]: (((cR @ Y0) = sK4) & (sK5 @ Y0))))) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f1222])).
% 1.70/1.58 thf(f1193,plain,(
% 1.70/1.58 ( ! [X1 : a > $o] : (((((!! @ a @ (^[Y0 : a]: ((X1 @ Y0) => (X1 @ (cL @ Y0))))) & (X1 @ sK3)) => (?? @ a @ (^[Y0 : a]: (((cR @ Y0) = sK4) & (X1 @ Y0))))) = $true)) ) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f1192])).
% 1.70/1.58 thf(f1192,plain,(
% 1.70/1.58 ( ! [X1 : a > $o] : (($true = ((^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK3)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK4) & (Y0 @ Y1)))))) @ X1))) ) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(pi_clausification,[status(thm)],[f1185])).
% 1.70/1.58 thf(f1185,plain,(
% 1.70/1.58 ((!! @ (a > $o) @ (^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK3)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK4) & (Y0 @ Y1))))))) = $true) | (~spl0_2 | ~spl0_5)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f1178])).
% 1.70/1.58 thf(f1163,plain,(
% 1.70/1.58 ~spl0_2 | ~spl0_6),
% 1.70/1.58 inference(avatar_contradiction_clause,[status(thm)],[f1162])).
% 1.70/1.58 thf(f1162,plain,(
% 1.70/1.58 $false | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(trivial_inequality_removal,[status(thm)],[f1161])).
% 1.70/1.58 thf(f1161,plain,(
% 1.70/1.58 ($false = $true) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f1160])).
% 1.70/1.58 thf(f1160,plain,(
% 1.70/1.58 ($true = (~ $true)) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f1159,f1158])).
% 1.70/1.58 thf(f1158,plain,(
% 1.70/1.58 ($true = (!! @ a @ (^[Y0 : a]: ((sK5 @ Y0) => (sK5 @ (cL @ Y0)))))) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f1157])).
% 1.70/1.58 thf(f1157,plain,(
% 1.70/1.58 ($true = ($true & (!! @ a @ (^[Y0 : a]: ((sK5 @ Y0) => (sK5 @ (cL @ Y0))))))) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f1029,f1155])).
% 1.70/1.58 thf(f1155,plain,(
% 1.70/1.58 ((sK5 @ sK3) = $true) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f1029])).
% 1.70/1.58 thf(f1029,plain,(
% 1.70/1.58 (((sK5 @ sK3) & (!! @ a @ (^[Y0 : a]: ((sK5 @ Y0) => (sK5 @ (cL @ Y0)))))) = $true) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f1015])).
% 1.70/1.58 thf(f1015,plain,(
% 1.70/1.58 ((((sK5 @ sK3) & (!! @ a @ (^[Y0 : a]: ((sK5 @ Y0) => (sK5 @ (cL @ Y0)))))) => (?? @ a @ (^[Y0 : a]: (((cR @ Y0) = sK4) & (sK5 @ Y0))))) = $false) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f1012])).
% 1.70/1.58 thf(f1012,plain,(
% 1.70/1.58 ($false = ((^[Y0 : a > $o]: (((Y0 @ sK3) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK4) & (Y0 @ Y1)))))) @ sK5)) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(sigma_clausification,[status(thm)],[f1009])).
% 1.70/1.58 thf(f1009,plain,(
% 1.70/1.58 ((!! @ (a > $o) @ (^[Y0 : a > $o]: (((Y0 @ sK3) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK4) & (Y0 @ Y1))))))) = $false) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(not_proxy_clausification,[status(thm)],[f977])).
% 1.70/1.58 thf(f977,plain,(
% 1.70/1.58 ($true = (~ (!! @ (a > $o) @ (^[Y0 : a > $o]: (((Y0 @ sK3) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK4) & (Y0 @ Y1))))))))) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f976])).
% 1.70/1.58 thf(f976,plain,(
% 1.70/1.58 (((!! @ (a > $o) @ (^[Y0 : a > $o]: (((Y0 @ sK3) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK4) & (Y0 @ Y1))))))) => $false) = $true) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(superposition,[status(thm)],[f946,f970])).
% 1.70/1.58 thf(f970,plain,(
% 1.70/1.58 ((cX @ sK4) = $false) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f967])).
% 1.70/1.58 thf(f967,plain,(
% 1.70/1.58 (((!! @ (a > $o) @ (^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK3)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK4) & (Y0 @ Y1))))))) => (cX @ sK4)) = $false) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f964])).
% 1.70/1.58 thf(f964,plain,(
% 1.70/1.58 ($false = ((^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2))))) & (Y1 @ sK3)) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))) @ sK4)) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(sigma_clausification,[status(thm)],[f944])).
% 1.70/1.58 thf(f944,plain,(
% 1.70/1.58 ((!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2))))) & (Y1 @ sK3)) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))) = $false) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f943])).
% 1.70/1.58 thf(f943,plain,(
% 1.70/1.58 (((!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2))))) & (Y1 @ sK3)) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))) & $true) = $false) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(superposition,[status(thm)],[f892,f69])).
% 1.70/1.58 thf(f69,plain,(
% 1.70/1.58 ($true = (cG @ (cP @ sK3 @ sK2))) | ~spl0_6),
% 1.70/1.58 inference(avatar_component_clause,[status(thm)],[f68])).
% 1.70/1.58 thf(f68,definition,(
% 1.70/1.58 spl0_6 <=> ($true = (cG @ (cP @ sK3 @ sK2)))),
% 1.70/1.58 introduced(definition,[new_symbols(naming,[spl0_6])],[avatar_definition])).
% 1.70/1.58 thf(f892,plain,(
% 1.70/1.58 ( ! [X1 : a] : ((((!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2))))) & (Y1 @ X1)) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))) & (cG @ (cP @ X1 @ sK2))) = $false)) ) | ~spl0_2),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f891])).
% 1.70/1.58 thf(f891,plain,(
% 1.70/1.58 ( ! [X1 : a] : (($false = ((^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cG @ (cP @ Y0 @ sK2)))) @ X1))) ) | ~spl0_2),
% 1.70/1.58 inference(pi_clausification,[status(thm)],[f847])).
% 1.70/1.58 thf(f946,plain,(
% 1.70/1.58 ( ! [X1 : a] : ((((!! @ (a > $o) @ (^[Y0 : a > $o]: (((Y0 @ sK3) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = X1) & (Y0 @ Y1))))))) => (cX @ X1)) = $true)) ) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f945])).
% 1.70/1.58 thf(f945,plain,(
% 1.70/1.58 ( ! [X1 : a] : ((((^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK3) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))) @ X1) = $true)) ) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(pi_clausification,[status(thm)],[f942])).
% 1.70/1.58 thf(f942,plain,(
% 1.70/1.58 ($true = (!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK3) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))))) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f941])).
% 1.70/1.58 thf(f941,plain,(
% 1.70/1.58 ($true = ($true & (!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK3) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))))) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f940])).
% 1.70/1.58 thf(f940,plain,(
% 1.70/1.58 ($true = (($true | (cF @ (cP @ sK3 @ sK2))) & (!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK3) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))))) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f807,f69])).
% 1.70/1.58 thf(f1159,plain,(
% 1.70/1.58 ((~ (!! @ a @ (^[Y0 : a]: ((sK5 @ Y0) => (sK5 @ (cL @ Y0)))))) = $true) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f1156])).
% 1.70/1.58 thf(f1156,plain,(
% 1.70/1.58 ((~ ((!! @ a @ (^[Y0 : a]: ((sK5 @ Y0) => (sK5 @ (cL @ Y0))))) & $true)) = $true) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f1034,f1155])).
% 1.70/1.58 thf(f1034,plain,(
% 1.70/1.58 ((~ ((!! @ a @ (^[Y0 : a]: ((sK5 @ Y0) => (sK5 @ (cL @ Y0))))) & (sK5 @ sK3))) = $true) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f1033])).
% 1.70/1.58 thf(f1033,plain,(
% 1.70/1.58 ($true = (((!! @ a @ (^[Y0 : a]: ((sK5 @ Y0) => (sK5 @ (cL @ Y0))))) & (sK5 @ sK3)) => $false)) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(superposition,[status(thm)],[f979,f1031])).
% 1.70/1.58 thf(f1031,plain,(
% 1.70/1.58 ($false = (?? @ a @ (^[Y0 : a]: (((cR @ Y0) = sK4) & (sK5 @ Y0))))) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f1030])).
% 1.70/1.58 thf(f1030,plain,(
% 1.70/1.58 (($true => (?? @ a @ (^[Y0 : a]: (((cR @ Y0) = sK4) & (sK5 @ Y0))))) = $false) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f1015,f1029])).
% 1.70/1.58 thf(f979,plain,(
% 1.70/1.58 ( ! [X1 : a > $o] : (((((!! @ a @ (^[Y0 : a]: ((X1 @ Y0) => (X1 @ (cL @ Y0))))) & (X1 @ sK3)) => (?? @ a @ (^[Y0 : a]: (((cR @ Y0) = sK4) & (X1 @ Y0))))) = $true)) ) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f978])).
% 1.70/1.58 thf(f978,plain,(
% 1.70/1.58 ( ! [X1 : a > $o] : (($true = ((^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK3)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK4) & (Y0 @ Y1)))))) @ X1))) ) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(pi_clausification,[status(thm)],[f971])).
% 1.70/1.58 thf(f971,plain,(
% 1.70/1.58 ((!! @ (a > $o) @ (^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK3)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK4) & (Y0 @ Y1))))))) = $true) | (~spl0_2 | ~spl0_6)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f967])).
% 1.70/1.58 thf(f799,plain,(
% 1.70/1.58 ~spl0_1 | ~spl0_10),
% 1.70/1.58 inference(avatar_contradiction_clause,[status(thm)],[f798])).
% 1.70/1.58 thf(f798,plain,(
% 1.70/1.58 $false | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(trivial_inequality_removal,[status(thm)],[f797])).
% 1.70/1.58 thf(f797,plain,(
% 1.70/1.58 ($false = $true) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f796])).
% 1.70/1.58 thf(f796,plain,(
% 1.70/1.58 ($true = (~ $true)) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(forward_demodulation,[status(thm)],[f791,f792])).
% 1.70/1.58 thf(f792,plain,(
% 1.70/1.58 ((!! @ a @ (^[Y0 : a]: ((sK16 @ Y0) => (sK16 @ (cL @ Y0))))) = $true) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f790])).
% 1.70/1.58 thf(f790,plain,(
% 1.70/1.58 (((!! @ a @ (^[Y0 : a]: ((sK16 @ Y0) => (sK16 @ (cL @ Y0))))) & $true) = $true) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f699,f787])).
% 1.70/1.58 thf(f787,plain,(
% 1.70/1.58 ((sK16 @ sK12) = $true) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f699])).
% 1.70/1.58 thf(f699,plain,(
% 1.70/1.58 ($true = ((!! @ a @ (^[Y0 : a]: ((sK16 @ Y0) => (sK16 @ (cL @ Y0))))) & (sK16 @ sK12))) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f697])).
% 1.70/1.58 thf(f697,plain,(
% 1.70/1.58 ((((!! @ a @ (^[Y0 : a]: ((sK16 @ Y0) => (sK16 @ (cL @ Y0))))) & (sK16 @ sK12)) => (?? @ a @ (^[Y0 : a]: (((cR @ Y0) = sK13) & (sK16 @ Y0))))) = $false) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f694])).
% 1.70/1.58 thf(f694,plain,(
% 1.70/1.58 ($false = ((^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK12)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK13) & (Y0 @ Y1)))))) @ sK16)) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(sigma_clausification,[status(thm)],[f686])).
% 1.70/1.58 thf(f686,plain,(
% 1.70/1.58 ((!! @ (a > $o) @ (^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK12)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK13) & (Y0 @ Y1))))))) = $false) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(not_proxy_clausification,[status(thm)],[f619])).
% 1.70/1.58 thf(f619,plain,(
% 1.70/1.58 ($true = (~ (!! @ (a > $o) @ (^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK12)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK13) & (Y0 @ Y1))))))))) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f618])).
% 1.70/1.58 thf(f618,plain,(
% 1.70/1.58 (((!! @ (a > $o) @ (^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK12)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK13) & (Y0 @ Y1))))))) => $false) = $true) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(superposition,[status(thm)],[f583,f617])).
% 1.70/1.58 thf(f617,plain,(
% 1.70/1.58 ((cX @ sK13) = $false) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f616])).
% 1.70/1.58 thf(f616,plain,(
% 1.70/1.58 ($false = ($true => (cX @ sK13))) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f604,f615])).
% 1.70/1.58 thf(f615,plain,(
% 1.70/1.58 ((!! @ (a > $o) @ (^[Y0 : a > $o]: (((Y0 @ sK12) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK13) & (Y0 @ Y1))))))) = $true) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f604])).
% 1.70/1.58 thf(f604,plain,(
% 1.70/1.58 ($false = ((!! @ (a > $o) @ (^[Y0 : a > $o]: (((Y0 @ sK12) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK13) & (Y0 @ Y1))))))) => (cX @ sK13))) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f602])).
% 1.70/1.58 thf(f602,plain,(
% 1.70/1.58 ($false = ((^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK12) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))) @ sK13)) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(sigma_clausification,[status(thm)],[f581])).
% 1.70/1.58 thf(f581,plain,(
% 1.70/1.58 ($false = (!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK12) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))))) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f580])).
% 1.70/1.58 thf(f580,plain,(
% 1.70/1.58 (($true & (!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK12) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))))) = $false) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f579])).
% 1.70/1.58 thf(f579,plain,(
% 1.70/1.58 ($false = (($true | (cF @ (cP @ sK12 @ sK2))) & (!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK12) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))))) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(superposition,[status(thm)],[f308,f575])).
% 1.70/1.58 thf(f575,plain,(
% 1.70/1.58 ($true = (cG @ (cP @ sK12 @ sK2))) | ~spl0_10),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f570])).
% 1.70/1.58 thf(f570,plain,(
% 1.70/1.58 ($true = ((!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2))))) & (Y1 @ sK12)) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))) & (cG @ (cP @ sK12 @ sK2)))) | ~spl0_10),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f569])).
% 1.70/1.58 thf(f569,plain,(
% 1.70/1.58 ($true = ((^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cG @ (cP @ Y0 @ sK2)))) @ sK12)) | ~spl0_10),
% 1.70/1.58 inference(sigma_clausification,[status(thm)],[f226])).
% 1.70/1.58 thf(f226,plain,(
% 1.70/1.58 ((?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cG @ (cP @ Y0 @ sK2))))) = $true) | ~spl0_10),
% 1.70/1.58 inference(avatar_component_clause,[status(thm)],[f225])).
% 1.70/1.58 thf(f225,definition,(
% 1.70/1.58 spl0_10 <=> ((?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cG @ (cP @ Y0 @ sK2))))) = $true)),
% 1.70/1.58 introduced(definition,[new_symbols(naming,[spl0_10])],[avatar_definition])).
% 1.70/1.58 thf(f308,plain,(
% 1.70/1.58 ( ! [X1 : a] : (($false = (((cG @ (cP @ X1 @ sK2)) | (cF @ (cP @ X1 @ sK2))) & (!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ X1) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))))))) ) | ~spl0_1),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f307])).
% 1.70/1.58 thf(f307,plain,(
% 1.70/1.58 ( ! [X1 : a] : ((((^[Y0 : a]: (((cG @ (cP @ Y0 @ sK2)) | (cF @ (cP @ Y0 @ sK2))) & (!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((Y2 @ Y0) & (!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3)))))) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))))) @ X1) = $false)) ) | ~spl0_1),
% 1.70/1.58 inference(pi_clausification,[status(thm)],[f32])).
% 1.70/1.58 thf(f32,plain,(
% 1.70/1.58 ($false = (?? @ a @ (^[Y0 : a]: (((cG @ (cP @ Y0 @ sK2)) | (cF @ (cP @ Y0 @ sK2))) & (!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((Y2 @ Y0) & (!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3)))))) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))))))) | ~spl0_1),
% 1.70/1.58 inference(avatar_component_clause,[status(thm)],[f31])).
% 1.70/1.58 thf(f31,definition,(
% 1.70/1.58 spl0_1 <=> ($false = (?? @ a @ (^[Y0 : a]: (((cG @ (cP @ Y0 @ sK2)) | (cF @ (cP @ Y0 @ sK2))) & (!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((Y2 @ Y0) & (!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3)))))) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1))))))))),
% 1.70/1.58 introduced(definition,[new_symbols(naming,[spl0_1])],[avatar_definition])).
% 1.70/1.58 thf(f583,plain,(
% 1.70/1.58 ( ! [X1 : a] : ((((!! @ (a > $o) @ (^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK12)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = X1) & (Y0 @ Y1))))))) => (cX @ X1)) = $true)) ) | ~spl0_10),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f582])).
% 1.70/1.58 thf(f582,plain,(
% 1.70/1.58 ( ! [X1 : a] : (($true = ((^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2))))) & (Y1 @ sK12)) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))) @ X1))) ) | ~spl0_10),
% 1.70/1.58 inference(pi_clausification,[status(thm)],[f578])).
% 1.70/1.58 thf(f578,plain,(
% 1.70/1.58 ((!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2))))) & (Y1 @ sK12)) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))) = $true) | ~spl0_10),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f577])).
% 1.70/1.58 thf(f577,plain,(
% 1.70/1.58 (((!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2))))) & (Y1 @ sK12)) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))) & $true) = $true) | ~spl0_10),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f570,f575])).
% 1.70/1.58 thf(f791,plain,(
% 1.70/1.58 ($true = (~ (!! @ a @ (^[Y0 : a]: ((sK16 @ Y0) => (sK16 @ (cL @ Y0))))))) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f789])).
% 1.70/1.58 thf(f789,plain,(
% 1.70/1.58 ((~ ($true & (!! @ a @ (^[Y0 : a]: ((sK16 @ Y0) => (sK16 @ (cL @ Y0))))))) = $true) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f705,f787])).
% 1.70/1.58 thf(f705,plain,(
% 1.70/1.58 ($true = (~ ((sK16 @ sK12) & (!! @ a @ (^[Y0 : a]: ((sK16 @ Y0) => (sK16 @ (cL @ Y0)))))))) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f703])).
% 1.70/1.58 thf(f703,plain,(
% 1.70/1.58 ((((sK16 @ sK12) & (!! @ a @ (^[Y0 : a]: ((sK16 @ Y0) => (sK16 @ (cL @ Y0)))))) => $false) = $true) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(superposition,[status(thm)],[f621,f701])).
% 1.70/1.58 thf(f701,plain,(
% 1.70/1.58 ($false = (?? @ a @ (^[Y0 : a]: (((cR @ Y0) = sK13) & (sK16 @ Y0))))) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f700])).
% 1.70/1.58 thf(f700,plain,(
% 1.70/1.58 (($true => (?? @ a @ (^[Y0 : a]: (((cR @ Y0) = sK13) & (sK16 @ Y0))))) = $false) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f697,f699])).
% 1.70/1.58 thf(f621,plain,(
% 1.70/1.58 ( ! [X1 : a > $o] : (((((X1 @ sK12) & (!! @ a @ (^[Y0 : a]: ((X1 @ Y0) => (X1 @ (cL @ Y0)))))) => (?? @ a @ (^[Y0 : a]: (((cR @ Y0) = sK13) & (X1 @ Y0))))) = $true)) ) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f620])).
% 1.70/1.58 thf(f620,plain,(
% 1.70/1.58 ( ! [X1 : a > $o] : ((((^[Y0 : a > $o]: (((Y0 @ sK12) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK13) & (Y0 @ Y1)))))) @ X1) = $true)) ) | (~spl0_1 | ~spl0_10)),
% 1.70/1.58 inference(pi_clausification,[status(thm)],[f615])).
% 1.70/1.58 thf(f561,plain,(
% 1.70/1.58 ~spl0_1 | ~spl0_9),
% 1.70/1.58 inference(avatar_contradiction_clause,[status(thm)],[f560])).
% 1.70/1.58 thf(f560,plain,(
% 1.70/1.58 $false | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(trivial_inequality_removal,[status(thm)],[f559])).
% 1.70/1.58 thf(f559,plain,(
% 1.70/1.58 ($false = $true) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f558])).
% 1.70/1.58 thf(f558,plain,(
% 1.70/1.58 ($true = (~ $true)) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f557,f556])).
% 1.70/1.58 thf(f556,plain,(
% 1.70/1.58 ((!! @ a @ (^[Y0 : a]: ((sK11 @ Y0) => (sK11 @ (cL @ Y0))))) = $true) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f555])).
% 1.70/1.58 thf(f555,plain,(
% 1.70/1.58 ($true = ((!! @ a @ (^[Y0 : a]: ((sK11 @ Y0) => (sK11 @ (cL @ Y0))))) & $true)) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f469,f552])).
% 1.70/1.58 thf(f552,plain,(
% 1.70/1.58 ($true = (sK11 @ sK6)) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f469])).
% 1.70/1.58 thf(f469,plain,(
% 1.70/1.58 (((!! @ a @ (^[Y0 : a]: ((sK11 @ Y0) => (sK11 @ (cL @ Y0))))) & (sK11 @ sK6)) = $true) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f460])).
% 1.70/1.58 thf(f460,plain,(
% 1.70/1.58 ($false = (((!! @ a @ (^[Y0 : a]: ((sK11 @ Y0) => (sK11 @ (cL @ Y0))))) & (sK11 @ sK6)) => (?? @ a @ (^[Y0 : a]: (((cR @ Y0) = sK9) & (sK11 @ Y0)))))) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f457])).
% 1.70/1.58 thf(f457,plain,(
% 1.70/1.58 ($false = ((^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK6)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK9) & (Y0 @ Y1)))))) @ sK11)) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(sigma_clausification,[status(thm)],[f450])).
% 1.70/1.58 thf(f450,plain,(
% 1.70/1.58 ($false = (!! @ (a > $o) @ (^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK6)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK9) & (Y0 @ Y1)))))))) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(not_proxy_clausification,[status(thm)],[f354])).
% 1.70/1.58 thf(f354,plain,(
% 1.70/1.58 ((~ (!! @ (a > $o) @ (^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK6)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK9) & (Y0 @ Y1)))))))) = $true) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f353])).
% 1.70/1.58 thf(f353,plain,(
% 1.70/1.58 (((!! @ (a > $o) @ (^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK6)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK9) & (Y0 @ Y1))))))) => $false) = $true) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(superposition,[status(thm)],[f281,f352])).
% 1.70/1.58 thf(f352,plain,(
% 1.70/1.58 ((cX @ sK9) = $false) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f351])).
% 1.70/1.58 thf(f351,plain,(
% 1.70/1.58 ($false = ($true => (cX @ sK9))) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f342,f350])).
% 1.70/1.58 thf(f350,plain,(
% 1.70/1.58 ($true = (!! @ (a > $o) @ (^[Y0 : a > $o]: (((Y0 @ sK6) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK9) & (Y0 @ Y1)))))))) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f342])).
% 1.70/1.58 thf(f342,plain,(
% 1.70/1.58 (((!! @ (a > $o) @ (^[Y0 : a > $o]: (((Y0 @ sK6) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK9) & (Y0 @ Y1))))))) => (cX @ sK9)) = $false) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f340])).
% 1.70/1.58 thf(f340,plain,(
% 1.70/1.58 ($false = ((^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK6) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))) @ sK9)) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(sigma_clausification,[status(thm)],[f321])).
% 1.70/1.58 thf(f321,plain,(
% 1.70/1.58 ((!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK6) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))) = $false) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f320])).
% 1.70/1.58 thf(f320,plain,(
% 1.70/1.58 ($false = ($true & (!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK6) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))))) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f317])).
% 1.70/1.58 thf(f317,plain,(
% 1.70/1.58 ((((cG @ (cP @ sK6 @ sK2)) | $true) & (!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK6) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))))) = $false) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(superposition,[status(thm)],[f308,f279])).
% 1.70/1.58 thf(f279,plain,(
% 1.70/1.58 ($true = (cF @ (cP @ sK6 @ sK2))) | ~spl0_9),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f278])).
% 1.70/1.58 thf(f278,plain,(
% 1.70/1.58 (($true & (cF @ (cP @ sK6 @ sK2))) = $true) | ~spl0_9),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f247,f277])).
% 1.70/1.58 thf(f277,plain,(
% 1.70/1.58 ($true = (!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2))))) & (Y1 @ sK6)) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))))) | ~spl0_9),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f247])).
% 1.70/1.58 thf(f247,plain,(
% 1.70/1.58 ($true = ((!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2))))) & (Y1 @ sK6)) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))) & (cF @ (cP @ sK6 @ sK2)))) | ~spl0_9),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f246])).
% 1.70/1.58 thf(f246,plain,(
% 1.70/1.58 (((^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cF @ (cP @ Y0 @ sK2)))) @ sK6) = $true) | ~spl0_9),
% 1.70/1.58 inference(sigma_clausification,[status(thm)],[f223])).
% 1.70/1.58 thf(f223,plain,(
% 1.70/1.58 ((?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cF @ (cP @ Y0 @ sK2))))) = $true) | ~spl0_9),
% 1.70/1.58 inference(avatar_component_clause,[status(thm)],[f222])).
% 1.70/1.58 thf(f222,definition,(
% 1.70/1.58 spl0_9 <=> ((?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cF @ (cP @ Y0 @ sK2))))) = $true)),
% 1.70/1.58 introduced(definition,[new_symbols(naming,[spl0_9])],[avatar_definition])).
% 1.70/1.58 thf(f281,plain,(
% 1.70/1.58 ( ! [X1 : a] : ((((!! @ (a > $o) @ (^[Y0 : a > $o]: (((!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1))))) & (Y0 @ sK6)) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = X1) & (Y0 @ Y1))))))) => (cX @ X1)) = $true)) ) | ~spl0_9),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f280])).
% 1.70/1.58 thf(f280,plain,(
% 1.70/1.58 ( ! [X1 : a] : ((((^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2))))) & (Y1 @ sK6)) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0))) @ X1) = $true)) ) | ~spl0_9),
% 1.70/1.58 inference(pi_clausification,[status(thm)],[f277])).
% 1.70/1.58 thf(f557,plain,(
% 1.70/1.58 ($true = (~ (!! @ a @ (^[Y0 : a]: ((sK11 @ Y0) => (sK11 @ (cL @ Y0))))))) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f554])).
% 1.70/1.58 thf(f554,plain,(
% 1.70/1.58 ($true = (~ ($true & (!! @ a @ (^[Y0 : a]: ((sK11 @ Y0) => (sK11 @ (cL @ Y0)))))))) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f486,f552])).
% 1.70/1.58 thf(f486,plain,(
% 1.70/1.58 ($true = (~ ((sK11 @ sK6) & (!! @ a @ (^[Y0 : a]: ((sK11 @ Y0) => (sK11 @ (cL @ Y0)))))))) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(boolean_simplification,[status(thm)],[f484])).
% 1.70/1.58 thf(f484,plain,(
% 1.70/1.58 ((((sK11 @ sK6) & (!! @ a @ (^[Y0 : a]: ((sK11 @ Y0) => (sK11 @ (cL @ Y0)))))) => $false) = $true) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(superposition,[status(thm)],[f372,f468])).
% 1.70/1.58 thf(f468,plain,(
% 1.70/1.58 ((?? @ a @ (^[Y0 : a]: (((cR @ Y0) = sK9) & (sK11 @ Y0)))) = $false) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f460])).
% 1.70/1.58 thf(f372,plain,(
% 1.70/1.58 ( ! [X1 : a > $o] : (((((X1 @ sK6) & (!! @ a @ (^[Y0 : a]: ((X1 @ Y0) => (X1 @ (cL @ Y0)))))) => (?? @ a @ (^[Y0 : a]: (((cR @ Y0) = sK9) & (X1 @ Y0))))) = $true)) ) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f371])).
% 1.70/1.58 thf(f371,plain,(
% 1.70/1.58 ( ! [X1 : a > $o] : ((((^[Y0 : a > $o]: (((Y0 @ sK6) & (!! @ a @ (^[Y1 : a]: ((Y0 @ Y1) => (Y0 @ (cL @ Y1)))))) => (?? @ a @ (^[Y1 : a]: (((cR @ Y1) = sK9) & (Y0 @ Y1)))))) @ X1) = $true)) ) | (~spl0_1 | ~spl0_9)),
% 1.70/1.58 inference(pi_clausification,[status(thm)],[f350])).
% 1.70/1.58 thf(f227,plain,(
% 1.70/1.58 spl0_9 | spl0_10 | ~spl0_1),
% 1.70/1.58 inference(avatar_split_clause,[status(thm)],[f220,f31,f225,f222])).
% 1.70/1.58 thf(f220,plain,(
% 1.70/1.58 ((?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cF @ (cP @ Y0 @ sK2))))) = $true) | ((?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cG @ (cP @ Y0 @ sK2))))) = $true) | ~spl0_1),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f219])).
% 1.70/1.58 thf(f219,plain,(
% 1.70/1.58 ($false != ((?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cG @ (cP @ Y0 @ sK2))))) | (?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cF @ (cP @ Y0 @ sK2))))))) | ~spl0_1),
% 1.70/1.58 inference(forward_demodulation,[status(thm)],[f20,f32])).
% 1.70/1.58 thf(f70,plain,(
% 1.70/1.58 spl0_5 | spl0_6 | ~spl0_2),
% 1.70/1.58 inference(avatar_split_clause,[status(thm)],[f63,f34,f68,f65])).
% 1.70/1.58 thf(f63,plain,(
% 1.70/1.58 ($true = (cF @ (cP @ sK3 @ sK2))) | ($true = (cG @ (cP @ sK3 @ sK2))) | ~spl0_2),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f52])).
% 1.70/1.58 thf(f52,plain,(
% 1.70/1.58 ($true = ((cG @ (cP @ sK3 @ sK2)) | (cF @ (cP @ sK3 @ sK2)))) | ~spl0_2),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f48])).
% 1.70/1.58 thf(f48,plain,(
% 1.70/1.58 ($true = (((cG @ (cP @ sK3 @ sK2)) | (cF @ (cP @ sK3 @ sK2))) & (!! @ a @ (^[Y0 : a]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: (((Y1 @ sK3) & (!! @ a @ (^[Y2 : a]: ((Y1 @ Y2) => (Y1 @ (cL @ Y2)))))) => (?? @ a @ (^[Y2 : a]: (((cR @ Y2) = Y0) & (Y1 @ Y2))))))) => (cX @ Y0)))))) | ~spl0_2),
% 1.70/1.58 inference(beta_eta_normalization,[status(thm)],[f47])).
% 1.70/1.58 thf(f47,plain,(
% 1.70/1.58 ($true = ((^[Y0 : a]: (((cG @ (cP @ Y0 @ sK2)) | (cF @ (cP @ Y0 @ sK2))) & (!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((Y2 @ Y0) & (!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3)))))) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))))) @ sK3)) | ~spl0_2),
% 1.70/1.58 inference(sigma_clausification,[status(thm)],[f44])).
% 1.70/1.58 thf(f44,plain,(
% 1.70/1.58 ($false != (?? @ a @ (^[Y0 : a]: (((cG @ (cP @ Y0 @ sK2)) | (cF @ (cP @ Y0 @ sK2))) & (!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((Y2 @ Y0) & (!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3)))))) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))))))) | ~spl0_2),
% 1.70/1.58 inference(backward_demodulation,[status(thm)],[f20,f35])).
% 1.70/1.58 thf(f36,plain,(
% 1.70/1.58 spl0_1 | spl0_2),
% 1.70/1.58 inference(avatar_split_clause,[status(thm)],[f29,f34,f31])).
% 1.70/1.58 thf(f29,plain,(
% 1.70/1.58 ($false = ((?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cG @ (cP @ Y0 @ sK2))))) | (?? @ a @ (^[Y0 : a]: ((!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3))))) & (Y2 @ Y0)) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1)))) & (cF @ (cP @ Y0 @ sK2))))))) | ($false = (?? @ a @ (^[Y0 : a]: (((cG @ (cP @ Y0 @ sK2)) | (cF @ (cP @ Y0 @ sK2))) & (!! @ a @ (^[Y1 : a]: ((!! @ (a > $o) @ (^[Y2 : a > $o]: (((Y2 @ Y0) & (!! @ a @ (^[Y3 : a]: ((Y2 @ Y3) => (Y2 @ (cL @ Y3)))))) => (?? @ a @ (^[Y3 : a]: (((cR @ Y3) = Y1) & (Y2 @ Y3))))))) => (cX @ Y1))))))))),
% 1.70/1.58 inference(binary_proxy_clausification,[status(thm)],[f20])).
% 1.70/1.58 % SZS output end Proof for DTF2THF_8033
% 1.70/1.58 % (8141)------------------------------
% 1.70/1.58 % (8141)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.58 % (8141)Termination reason: Refutation
% 1.70/1.58
% 1.70/1.58 % (8141)Memory used [KB]: 6396
% 1.70/1.58 % (8141)Time elapsed: 0.168 s
% 1.70/1.58 % (8141)Instructions burned: 296 (million)
% 1.70/1.58 % (8141)------------------------------
% 1.70/1.58 % (8141)------------------------------
% 1.70/1.58 % (8129)Success in time 0.199 s
%------------------------------------------------------------------------------