%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU524^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:29:55 AM UTC 2026
% Result : Theorem 1.58s 0.50s
% Output : Refutation 1.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 9
% Syntax : Number of formulae : 125 ( 69 unt; 0 typ; 6 def)
% Number of atoms : 1718 ( 118 equ; 0 cnn)
% Maximal formula atoms : 42 ( 13 avg)
% Number of connectives : 2187 ( 65 ~; 64 |; 0 &; 804 @)
% ( 8 <=>;1113 =>; 0 <=; 0 <~>)
% Maximal formula depth : 48 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 81 ( 77 usr; 52 con; 0-4 aty)
% ( 133 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 185 ( 0 sgn 44 !; 0 ?; 185 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
in: $i > $i > $o ).
thf(func_def_1,type,
exu: ( $i > $o ) > $o ).
thf(func_def_3,type,
setextAx: $o ).
thf(func_def_5,type,
emptysetAx: $o ).
thf(func_def_6,type,
setadjoin: $i > $i > $i ).
thf(func_def_7,type,
setadjoinAx: $o ).
thf(func_def_8,type,
powerset: $i > $i ).
thf(func_def_9,type,
powersetAx: $o ).
thf(func_def_10,type,
setunion: $i > $i ).
thf(func_def_11,type,
setunionAx: $o ).
thf(func_def_13,type,
omega0Ax: $o ).
thf(func_def_14,type,
omegaSAx: $o ).
thf(func_def_15,type,
omegaIndAx: $o ).
thf(func_def_16,type,
replAx: $o ).
thf(func_def_17,type,
foundationAx: $o ).
thf(func_def_18,type,
wellorderingAx: $o ).
thf(func_def_19,type,
descr: ( $i > $o ) > $i ).
thf(func_def_20,type,
descrp: $o ).
thf(func_def_21,type,
dsetconstr: $i > ( $i > $o ) > $i ).
thf(func_def_22,type,
dsetconstrI: $o ).
thf(func_def_23,type,
dsetconstrEL: $o ).
thf(func_def_24,type,
dsetconstrER: $o ).
thf(func_def_25,type,
exuE1: $o ).
thf(func_def_26,type,
prop2set: $o > $i ).
thf(func_def_27,type,
prop2setE: $o ).
thf(func_def_28,type,
emptysetE: $o ).
thf(func_def_29,type,
emptysetimpfalse: $o ).
thf(func_def_30,type,
notinemptyset: $o ).
thf(func_def_31,type,
exuE3e: $o ).
thf(func_def_32,type,
setext: $o ).
thf(func_def_33,type,
emptyI: $o ).
thf(func_def_34,type,
noeltsimpempty: $o ).
thf(func_def_35,type,
setbeta: $o ).
thf(func_def_36,type,
nonempty: $i > $o ).
thf(func_def_37,type,
nonemptyE1: $o ).
thf(func_def_38,type,
nonemptyI: $o ).
thf(func_def_39,type,
nonemptyI1: $o ).
thf(func_def_40,type,
setadjoinIL: $o ).
thf(func_def_41,type,
emptyinunitempty: $o ).
thf(func_def_42,type,
setadjoinIR: $o ).
thf(func_def_43,type,
setadjoinE: $o ).
thf(func_def_44,type,
setadjoinOr: $o ).
thf(func_def_45,type,
setoftrueEq: $o ).
thf(func_def_46,type,
powersetI: $o ).
thf(func_def_47,type,
emptyinPowerset: $o ).
thf(func_def_48,type,
emptyInPowerset: $o ).
thf(func_def_49,type,
powersetE: $o ).
thf(func_def_50,type,
setunionI: $o ).
thf(func_def_51,type,
setunionE: $o ).
thf(func_def_52,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_53,type,
vIMP: $o > $o > $o ).
thf(func_def_54,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_55,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_56,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_57,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_58,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_59,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_60,type,
vAND: $o > $o > $o ).
thf(func_def_61,type,
vIFF: $o > $o > $o ).
thf(func_def_62,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_63,type,
vOR: $o > $o > $o ).
thf(func_def_64,type,
vNOT: $o > $o ).
thf(func_def_65,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_71,type,
sK3: $i > $i ).
thf(func_def_72,type,
sK4: $i > $i ).
thf(func_def_73,type,
sK5: $i > $i > $i ).
thf(func_def_75,type,
sK7: $i > $i > $i ).
thf(f5,axiom,
( powersetAx
= ( ! [X1: $i,X0: $i] :
( ! [X2: $i] :
( ( in @ X2 @ X1 )
=> ( in @ X2 @ X0 ) )
<=> ( in @ X1 @ ( powerset @ X0 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',powersetAx) ).
thf(f42,axiom,
( setunionI
= ( ! [X0: $i,X1: $i,X2: $i] :
( ( in @ X1 @ X2 )
=> ( ( in @ X2 @ X0 )
=> ( in @ X1 @ ( setunion @ X0 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',setunionI) ).
thf(f44,conjecture,
( setextAx
=> ( emptysetAx
=> ( setadjoinAx
=> ( powersetAx
=> ( setunionAx
=> ( omega0Ax
=> ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ! [X1: $i,X0: $i] :
( ( in @ X1 @ X0 )
=> ( in @ X1 @ ( powerset @ ( setunion @ X0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subPowSU) ).
thf(f45,negated_conjecture,
~ ( setextAx
=> ( emptysetAx
=> ( setadjoinAx
=> ( powersetAx
=> ( setunionAx
=> ( omega0Ax
=> ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ! [X1: $i,X0: $i] :
( ( in @ X1 @ X0 )
=> ( in @ X1 @ ( powerset @ ( setunion @ X0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f44]) ).
thf(f52,plain,
( powersetAx
= ( ! [X0: $i,X1: $i] :
( ! [X2: $i] :
( ( in @ X2 @ X0 )
=> ( in @ X2 @ X1 ) )
<=> ( in @ X0 @ ( powerset @ X1 ) ) ) ) ),
inference(rectify,[],[f5]) ).
thf(f53,plain,
( powersetAx
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ Y1 )
=> ( in @ Y2 @ Y0 ) ) )
= ( in @ Y1 @ ( powerset @ Y0 ) ) ) ) ) ),
inference(fool_elimination,[],[f52]) ).
thf(f70,plain,
( setunionI
= ( ! [X0: $i,X1: $i,X2: $i] :
( ( in @ X1 @ X2 )
=> ( ( in @ X2 @ X0 )
=> ( in @ X1 @ ( setunion @ X0 ) ) ) ) ) ),
inference(rectify,[],[f42]) ).
thf(f71,plain,
( setunionI
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y1 @ Y0 )
=> ( ( in @ Y0 @ Y2 )
=> ( in @ Y1 @ ( setunion @ Y2 ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f70]) ).
thf(f99,plain,
~ ( setextAx
=> ( emptysetAx
=> ( setadjoinAx
=> ( powersetAx
=> ( setunionAx
=> ( omega0Ax
=> ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ! [X0: $i,X1: $i] :
( ( in @ X0 @ X1 )
=> ( in @ X0 @ ( powerset @ ( setunion @ X1 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f45]) ).
thf(f100,plain,
( $true
= ( ~ ( setextAx
=> ( emptysetAx
=> ( setadjoinAx
=> ( powersetAx
=> ( setunionAx
=> ( omega0Ax
=> ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f99]) ).
thf(f146,plain,
( powersetAx
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ Y1 )
=> ( in @ Y2 @ Y0 ) ) )
= ( in @ Y1 @ ( powerset @ Y0 ) ) ) ) ) ),
inference(cnf_transformation,[],[f53]) ).
thf(f153,plain,
( setunionI
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y1 @ Y0 )
=> ( ( in @ Y0 @ Y2 )
=> ( in @ Y1 @ ( setunion @ Y2 ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f71]) ).
thf(f170,plain,
( $true
= ( ~ ( setextAx
=> ( emptysetAx
=> ( setadjoinAx
=> ( powersetAx
=> ( setunionAx
=> ( omega0Ax
=> ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f100]) ).
thf(f203,plain,
( ( powersetAx = $false )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ Y1 )
=> ( in @ Y2 @ Y0 ) ) )
= ( in @ Y1 @ ( powerset @ Y0 ) ) ) ) ) ) ),
inference(iff_proxy_clausification,[],[f146]) ).
thf(f239,plain,
( ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y1 @ Y0 )
=> ( ( in @ Y0 @ Y2 )
=> ( in @ Y1 @ ( setunion @ Y2 ) ) ) ) ) ) ) )
| ( setunionI = $false ) ),
inference(iff_proxy_clausification,[],[f153]) ).
thf(f262,plain,
( $false
= ( setextAx
=> ( emptysetAx
=> ( setadjoinAx
=> ( powersetAx
=> ( setunionAx
=> ( omega0Ax
=> ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(not_proxy_clausification,[],[f170]) ).
thf(f316,definition,
( spl0_9
<=> ( powersetAx = $true ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
thf(f318,plain,
( ( powersetAx = $true )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f316]) ).
thf(f325,definition,
( spl0_11
<=> ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ Y1 )
=> ( in @ Y2 @ Y0 ) ) )
= ( in @ Y1 @ ( powerset @ Y0 ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
thf(f327,plain,
( ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ Y1 )
=> ( in @ Y2 @ Y0 ) ) )
= ( in @ Y1 @ ( powerset @ Y0 ) ) ) ) ) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f325]) ).
thf(f329,definition,
( spl0_12
<=> ( powersetAx = $false ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
thf(f331,plain,
( ( powersetAx = $false )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f329]) ).
thf(f332,plain,
( spl0_11
| spl0_12 ),
inference(avatar_split_clause,[],[f203,f329,f325]) ).
thf(f644,definition,
( spl0_82
<=> ( setunionI = $true ) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
thf(f646,plain,
( ( setunionI = $true )
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f644]) ).
thf(f649,definition,
( spl0_83
<=> ( setunionI = $false ) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
thf(f651,plain,
( ( setunionI = $false )
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f649]) ).
thf(f653,definition,
( spl0_84
<=> ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y1 @ Y0 )
=> ( ( in @ Y0 @ Y2 )
=> ( in @ Y1 @ ( setunion @ Y2 ) ) ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
thf(f655,plain,
( ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y1 @ Y0 )
=> ( ( in @ Y0 @ Y2 )
=> ( in @ Y1 @ ( setunion @ Y2 ) ) ) ) ) ) ) )
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f653]) ).
thf(f656,plain,
( spl0_83
| spl0_84 ),
inference(avatar_split_clause,[],[f239,f653,f649]) ).
thf(f847,plain,
( ( emptysetAx
=> ( setadjoinAx
=> ( powersetAx
=> ( setunionAx
=> ( omega0Ax
=> ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f262]) ).
thf(f969,plain,
( ( setadjoinAx
=> ( powersetAx
=> ( setunionAx
=> ( omega0Ax
=> ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f847]) ).
thf(f973,plain,
( $false
= ( powersetAx
=> ( setunionAx
=> ( omega0Ax
=> ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f969]) ).
thf(f975,plain,
( $false
= ( setunionAx
=> ( omega0Ax
=> ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f973]) ).
thf(f976,plain,
powersetAx = $true,
inference(imp_proxy_clausification,[],[f973]) ).
thf(f978,plain,
( ( omega0Ax
=> ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f975]) ).
thf(f980,plain,
spl0_9,
inference(avatar_split_clause,[],[f976,f316]) ).
thf(f981,plain,
( ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f978]) ).
thf(f984,plain,
( ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f981]) ).
thf(f988,plain,
( $false
= ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f984]) ).
thf(f990,plain,
( $false
= ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f988]) ).
thf(f993,plain,
( ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f990]) ).
thf(f996,plain,
( $false
= ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f993]) ).
thf(f1000,plain,
( ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f996]) ).
thf(f1003,plain,
( ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1000]) ).
thf(f1005,plain,
( ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1003]) ).
thf(f1008,plain,
( ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1005]) ).
thf(f1011,plain,
( ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1008]) ).
thf(f1014,plain,
( $false
= ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1011]) ).
thf(f1018,plain,
( ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1014]) ).
thf(f1020,plain,
( ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1018]) ).
thf(f1024,plain,
( ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1020]) ).
thf(f1027,plain,
( $false
= ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1024]) ).
thf(f1030,plain,
( ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1027]) ).
thf(f1033,plain,
( $false
= ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1030]) ).
thf(f1036,plain,
( ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1033]) ).
thf(f1039,plain,
( $false
= ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1036]) ).
thf(f1042,plain,
( $false
= ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1039]) ).
thf(f1045,plain,
( ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1042]) ).
thf(f1047,plain,
( ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1045]) ).
thf(f1050,plain,
( $false
= ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1047]) ).
thf(f1054,plain,
( ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1050]) ).
thf(f1056,plain,
( $false
= ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1054]) ).
thf(f1059,plain,
( ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1056]) ).
thf(f1062,plain,
( ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1059]) ).
thf(f1066,plain,
( $false
= ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1062]) ).
thf(f1069,plain,
( ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1066]) ).
thf(f1072,plain,
( ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1069]) ).
thf(f1075,plain,
( ( powersetE
=> ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1072]) ).
thf(f1077,plain,
( ( setunionI
=> ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1075]) ).
thf(f1081,plain,
( ( setunionE
=> ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1077]) ).
thf(f1082,plain,
setunionI = $true,
inference(imp_proxy_clausification,[],[f1077]) ).
thf(f1083,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1081]) ).
thf(f1085,plain,
spl0_82,
inference(avatar_split_clause,[],[f1082,f644]) ).
thf(f1087,plain,
( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ ( powerset @ ( setunion @ Y0 ) ) ) ) )
@ sK1 )
= $false ),
inference(sigma_proxy_clausification,[],[f1083]) ).
thf(f1088,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ sK1 )
=> ( in @ Y0 @ ( powerset @ ( setunion @ sK1 ) ) ) ) )
= $false ),
inference(beta-eta_normalization,[],[f1087]) ).
thf(f1089,plain,
( $false
= ( ^ [Y0: $i] :
( ( in @ Y0 @ sK1 )
=> ( in @ Y0 @ ( powerset @ ( setunion @ sK1 ) ) ) )
@ sK2 ) ),
inference(sigma_proxy_clausification,[],[f1088]) ).
thf(f1090,plain,
( ( ( in @ sK2 @ sK1 )
=> ( in @ sK2 @ ( powerset @ ( setunion @ sK1 ) ) ) )
= $false ),
inference(beta-eta_normalization,[],[f1089]) ).
thf(f1091,plain,
( ( in @ sK2 @ ( powerset @ ( setunion @ sK1 ) ) )
= $false ),
inference(imp_proxy_clausification,[],[f1090]) ).
thf(f1092,plain,
( $true
= ( in @ sK2 @ sK1 ) ),
inference(imp_proxy_clausification,[],[f1090]) ).
thf(f1177,plain,
( ( $true = $false )
| ~ spl0_82
| ~ spl0_83 ),
inference(superposition,[],[f646,f651]) ).
thf(f1181,plain,
( $false
| ~ spl0_82
| ~ spl0_83 ),
inference(trivial_inequality_removal,[],[f1177]) ).
thf(f1182,plain,
( ~ spl0_82
| ~ spl0_83 ),
inference(avatar_contradiction_clause,[],[f1181]) ).
thf(f1455,plain,
( ! [X1: $i] :
( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ Y1 )
=> ( in @ Y2 @ Y0 ) ) )
= ( in @ Y1 @ ( powerset @ Y0 ) ) ) )
@ X1 )
= $true )
| ~ spl0_11 ),
inference(pi_proxy_clausification,[],[f327]) ).
thf(f1456,plain,
( ! [X1: $i] :
( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ X1 ) ) )
= ( in @ Y0 @ ( powerset @ X1 ) ) ) ) )
| ~ spl0_11 ),
inference(beta-eta_normalization,[],[f1455]) ).
thf(f1457,plain,
( ! [X2: $i,X1: $i] :
( $true
= ( ^ [Y0: $i] :
( ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ Y0 )
=> ( in @ Y1 @ X1 ) ) )
= ( in @ Y0 @ ( powerset @ X1 ) ) )
@ X2 ) )
| ~ spl0_11 ),
inference(pi_proxy_clausification,[],[f1456]) ).
thf(f1458,plain,
( ! [X2: $i,X1: $i] :
( $true
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ X2 )
=> ( in @ Y0 @ X1 ) ) )
= ( in @ X2 @ ( powerset @ X1 ) ) ) )
| ~ spl0_11 ),
inference(beta-eta_normalization,[],[f1457]) ).
thf(f1469,plain,
( ( $true
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ sK2 )
=> ( in @ Y0 @ ( setunion @ sK1 ) ) ) )
= $false ) )
| ~ spl0_11 ),
inference(superposition,[],[f1458,f1091]) ).
thf(f1484,plain,
( ( $true
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ sK2 )
=> ( in @ Y0 @ ( setunion @ sK1 ) ) ) ) ) )
| ~ spl0_11 ),
inference(boolean_simplification,[],[f1469]) ).
thf(f1485,plain,
( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ sK2 )
=> ( in @ Y0 @ ( setunion @ sK1 ) ) ) )
= $false )
| ~ spl0_11 ),
inference(not_proxy_clausification,[],[f1484]) ).
thf(f1486,plain,
( ( ( ^ [Y0: $i] :
( ( in @ Y0 @ sK2 )
=> ( in @ Y0 @ ( setunion @ sK1 ) ) )
@ sK6 )
= $false )
| ~ spl0_11 ),
inference(sigma_proxy_clausification,[],[f1485]) ).
thf(f1489,plain,
( ( ( ( in @ sK6 @ sK2 )
=> ( in @ sK6 @ ( setunion @ sK1 ) ) )
= $false )
| ~ spl0_11 ),
inference(beta-eta_normalization,[],[f1486]) ).
thf(f1490,plain,
( ( $false
= ( in @ sK6 @ ( setunion @ sK1 ) ) )
| ~ spl0_11 ),
inference(imp_proxy_clausification,[],[f1489]) ).
thf(f1491,plain,
( ( ( in @ sK6 @ sK2 )
= $true )
| ~ spl0_11 ),
inference(imp_proxy_clausification,[],[f1489]) ).
thf(f1590,plain,
( ! [X1: $i] :
( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y1 @ Y0 )
=> ( ( in @ Y0 @ Y2 )
=> ( in @ Y1 @ ( setunion @ Y2 ) ) ) ) ) )
@ X1 ) )
| ~ spl0_84 ),
inference(pi_proxy_clausification,[],[f655]) ).
thf(f1591,plain,
( ! [X1: $i] :
( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ X1 )
=> ( ( in @ X1 @ Y1 )
=> ( in @ Y0 @ ( setunion @ Y1 ) ) ) ) ) ) )
| ~ spl0_84 ),
inference(beta-eta_normalization,[],[f1590]) ).
thf(f1592,plain,
( ! [X2: $i,X1: $i] :
( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ X1 )
=> ( ( in @ X1 @ Y1 )
=> ( in @ Y0 @ ( setunion @ Y1 ) ) ) ) )
@ X2 ) )
| ~ spl0_84 ),
inference(pi_proxy_clausification,[],[f1591]) ).
thf(f1593,plain,
( ! [X2: $i,X1: $i] :
( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ X2 @ X1 )
=> ( ( in @ X1 @ Y0 )
=> ( in @ X2 @ ( setunion @ Y0 ) ) ) ) ) )
| ~ spl0_84 ),
inference(beta-eta_normalization,[],[f1592]) ).
thf(f1596,plain,
( ! [X2: $i,X3: $i,X1: $i] :
( $true
= ( ^ [Y0: $i] :
( ( in @ X2 @ X1 )
=> ( ( in @ X1 @ Y0 )
=> ( in @ X2 @ ( setunion @ Y0 ) ) ) )
@ X3 ) )
| ~ spl0_84 ),
inference(pi_proxy_clausification,[],[f1593]) ).
thf(f1597,plain,
( ! [X2: $i,X3: $i,X1: $i] :
( $true
= ( ( in @ X2 @ X1 )
=> ( ( in @ X1 @ X3 )
=> ( in @ X2 @ ( setunion @ X3 ) ) ) ) )
| ~ spl0_84 ),
inference(beta-eta_normalization,[],[f1596]) ).
thf(f1598,plain,
( ! [X2: $i,X3: $i,X1: $i] :
( ( $true
= ( ( in @ X1 @ X3 )
=> ( in @ X2 @ ( setunion @ X3 ) ) ) )
| ( ( in @ X2 @ X1 )
= $false ) )
| ~ spl0_84 ),
inference(imp_proxy_clausification,[],[f1597]) ).
thf(f1599,plain,
( ! [X2: $i,X3: $i,X1: $i] :
( ( $true
= ( in @ X2 @ ( setunion @ X3 ) ) )
| ( ( in @ X2 @ X1 )
= $false )
| ( ( in @ X1 @ X3 )
= $false ) )
| ~ spl0_84 ),
inference(imp_proxy_clausification,[],[f1598]) ).
thf(f1600,plain,
( ! [X0: $i] :
( ( ( in @ sK6 @ X0 )
= $false )
| ( $true = $false )
| ( ( in @ X0 @ sK1 )
= $false ) )
| ~ spl0_11
| ~ spl0_84 ),
inference(superposition,[],[f1599,f1490]) ).
thf(f1609,plain,
( ! [X0: $i] :
( ( ( in @ sK6 @ X0 )
= $false )
| ( ( in @ X0 @ sK1 )
= $false ) )
| ~ spl0_11
| ~ spl0_84 ),
inference(trivial_inequality_removal,[],[f1600]) ).
thf(f1628,plain,
( ( $false
= ( in @ sK2 @ sK1 ) )
| ( $true = $false )
| ~ spl0_11
| ~ spl0_84 ),
inference(superposition,[],[f1491,f1609]) ).
thf(f1630,plain,
( ( $false
= ( in @ sK2 @ sK1 ) )
| ~ spl0_11
| ~ spl0_84 ),
inference(trivial_inequality_removal,[],[f1628]) ).
thf(f1648,plain,
( ( $true = $false )
| ~ spl0_11
| ~ spl0_84 ),
inference(superposition,[],[f1092,f1630]) ).
thf(f1652,plain,
( $false
| ~ spl0_11
| ~ spl0_84 ),
inference(trivial_inequality_removal,[],[f1648]) ).
thf(f1653,plain,
( ~ spl0_11
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f1652]) ).
thf(f1654,plain,
( ( $true = $false )
| ~ spl0_9
| ~ spl0_12 ),
inference(superposition,[],[f331,f318]) ).
thf(f1660,plain,
( $false
| ~ spl0_9
| ~ spl0_12 ),
inference(trivial_inequality_removal,[],[f1654]) ).
thf(f1661,plain,
( ~ spl0_9
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f1660]) ).
cnf(s6,plain,
( spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f332]) ).
cnf(s42,plain,
( spl0_83
| spl0_84 ),
inference(sat_conversion,[],[f656]) ).
cnf(s84,plain,
spl0_9,
inference(sat_conversion,[],[f980]) ).
cnf(s119,plain,
spl0_82,
inference(sat_conversion,[],[f1085]) ).
cnf(s134,plain,
( ~ spl0_82
| ~ spl0_83 ),
inference(sat_conversion,[],[f1182]) ).
cnf(s149,plain,
( ~ spl0_11
| ~ spl0_84 ),
inference(sat_conversion,[],[f1653]) ).
cnf(s151,plain,
( ~ spl0_9
| ~ spl0_12 ),
inference(sat_conversion,[],[f1661]) ).
cnf(s152,plain,
~ spl0_83,
inference(rat,[],[s134,s119]) ).
cnf(s170,plain,
~ spl0_12,
inference(rat,[],[s151,s84]) ).
cnf(s179,plain,
spl0_84,
inference(rat,[],[s42,s152]) ).
cnf(s180,plain,
~ spl0_11,
inference(rat,[],[s149,s179]) ).
cnf(s189,plain,
$false,
inference(rat,[],[s6,s170,s180]) ).
thf(f1662,plain,
$false,
inference(avatar_sat_refutation,[],[s189]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU524^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n005.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Tue Sep 29 13:48:01 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running higher-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.35 % (1693208)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.21/0.35 % (1693235)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2366195345:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.21/0.35 % (1693237)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.21/0.35 % (1693237)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.21/0.35 % (1693235)Instruction limit reached!
% 0.21/0.35 % (1693235)------------------------------
% 0.21/0.35 % (1693235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (1693235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (1693235)CaDiCaL version: 2.1.3
% 0.21/0.35 % (1693235)Termination reason: Instruction limit
% 0.21/0.35 % (1693235)Termination phase: Property scanning
% 0.21/0.35 % (1693235)Time elapsed: 0.006 s
% 0.21/0.35 % (1693235)Peak memory usage: 11 MB
% 0.21/0.35 % (1693235)Instructions burned: 25 (million)
% 0.21/0.35 % (1693230)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1446940665:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.21/0.35 % (1693232)lrs+10_16_si=on:nwc=1.5:random_seed=4089604638:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.21/0.35 % (1693233)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3335506711:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.21/0.35 % (1693234)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=2762889417:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.21/0.35 % (1693237)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=2279108230:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.21/0.35 % (1693236)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3289815881:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.21/0.35 % (1693233)Instruction limit reached!
% 0.21/0.35 % (1693233)------------------------------
% 0.21/0.35 % (1693233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (1693233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (1693233)CaDiCaL version: 2.1.3
% 0.21/0.35 % (1693233)Termination reason: Instruction limit
% 0.21/0.35 % (1693233)Termination phase: shuffling
% 0.21/0.35 % (1693233)Time elapsed: 0.002 s
% 0.21/0.35 % (1693233)Peak memory usage: 9 MB
% 0.21/0.35 % (1693233)Instructions burned: 4 (million)
% 0.21/0.35 % (1693232)Instruction limit reached!
% 0.21/0.35 % (1693232)------------------------------
% 0.21/0.35 % (1693232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (1693232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (1693232)CaDiCaL version: 2.1.3
% 0.21/0.35 % (1693232)Termination reason: Instruction limit
% 0.21/0.35 % (1693232)Termination phase: Saturation
% 0.21/0.35 % (1693232)Time elapsed: 0.009 s
% 0.21/0.35 % (1693232)Peak memory usage: 11 MB
% 0.21/0.35 % (1693232)Instructions burned: 19 (million)
% 0.21/0.35 % (1693250)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=554237844:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.21/0.35 % (1693250)Instruction limit reached!
% 0.21/0.35 % (1693250)------------------------------
% 0.21/0.35 % (1693250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (1693250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (1693250)CaDiCaL version: 2.1.3
% 0.21/0.35 % (1693250)Termination reason: Instruction limit
% 0.21/0.35 % (1693250)Termination phase: shuffling
% 0.21/0.35 % (1693250)Time elapsed: 0.001 s
% 0.21/0.35 % (1693250)Peak memory usage: 9 MB
% 0.21/0.35 % (1693250)Instructions burned: 4 (million)
% 0.21/0.35 % (1693264)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=803634364:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.85/0.39 % (1693259)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3354401619:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.85/0.39 % (1693264)Instruction limit reached!
% 0.85/0.39 % (1693264)------------------------------
% 0.85/0.39 % (1693264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.39 % (1693264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.39 % (1693264)CaDiCaL version: 2.1.3
% 0.85/0.39 % (1693264)Termination reason: Instruction limit
% 0.85/0.39 % (1693264)Termination phase: Property scanning
% 0.85/0.39 % (1693264)Time elapsed: 0.003 s
% 0.85/0.39 % (1693264)Peak memory usage: 10 MB
% 0.85/0.39 % (1693264)Instructions burned: 13 (million)
% 0.85/0.39 % (1693263)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.85/0.39 % (1693259)Instruction limit reached!
% 0.85/0.39 % (1693259)------------------------------
% 0.85/0.39 % (1693259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.39 % (1693259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.39 % (1693259)CaDiCaL version: 2.1.3
% 0.85/0.39 % (1693259)Termination reason: Instruction limit
% 0.85/0.39 % (1693259)Termination phase: Property scanning
% 0.85/0.39 % (1693259)Time elapsed: 0.003 s
% 0.85/0.39 % (1693259)Peak memory usage: 10 MB
% 0.85/0.39 % (1693259)Instructions burned: 6 (million)
% 0.85/0.39 % (1693263)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=599492726:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.85/0.39 % (1693263)Instruction limit reached!
% 0.85/0.39 % (1693263)------------------------------
% 0.85/0.39 % (1693263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.39 % (1693263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.39 % (1693271)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.85/0.39 % (1693263)CaDiCaL version: 2.1.3
% 0.85/0.39 % (1693263)Termination reason: Instruction limit
% 0.85/0.39 % (1693263)Termination phase: Property scanning
% 0.85/0.39 % (1693263)Time elapsed: 0.004 s
% 0.85/0.39 % (1693271)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.85/0.39 % (1693263)Peak memory usage: 10 MB
% 0.85/0.39 % (1693263)Instructions burned: 9 (million)
% 0.85/0.39 % (1693271)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=313696436:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.85/0.39 % (1693236)Instruction limit reached!
% 0.85/0.39 % (1693236)------------------------------
% 0.85/0.39 % (1693236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.39 % (1693236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.39 % (1693236)CaDiCaL version: 2.1.3
% 0.85/0.39 % (1693236)Termination reason: Instruction limit
% 0.85/0.39 % (1693236)Termination phase: Saturation
% 0.85/0.39 % (1693236)Time elapsed: 0.038 s
% 0.85/0.39 % (1693236)Peak memory usage: 13 MB
% 0.85/0.39 % (1693236)Instructions burned: 75 (million)
% 0.85/0.39 % (1693271)Instruction limit reached!
% 0.85/0.39 % (1693271)------------------------------
% 0.85/0.39 % (1693271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.39 % (1693271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.39 % (1693271)CaDiCaL version: 2.1.3
% 0.85/0.39 % (1693271)Termination reason: Instruction limit
% 0.85/0.39 % (1693271)Termination phase: Saturation
% 0.85/0.39 % (1693271)Time elapsed: 0.007 s
% 0.85/0.39 % (1693271)Peak memory usage: 11 MB
% 0.85/0.39 % (1693271)Instructions burned: 32 (million)
% 0.85/0.39 % (1693272)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=4231028132:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.85/0.39 % (1693230)Instruction limit reached!
% 0.85/0.39 % (1693230)------------------------------
% 0.85/0.39 % (1693230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.43 % (1693230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.43 % (1693230)CaDiCaL version: 2.1.3
% 0.85/0.43 % (1693230)Termination reason: Instruction limit
% 0.85/0.43 % (1693230)Termination phase: Saturation
% 0.85/0.43 % (1693230)Time elapsed: 0.046 s
% 0.85/0.43 % (1693230)Peak memory usage: 13 MB
% 0.85/0.43 % (1693230)Instructions burned: 88 (million)
% 0.85/0.43 % (1693274)lrs+10_1_si=on:cs=on:random_seed=2150046904:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.85/0.43 % (1693277)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3998893013:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.85/0.43 % (1693276)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.85/0.43 % (1693274)Instruction limit reached!
% 0.85/0.43 % (1693274)------------------------------
% 0.85/0.43 % (1693274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.43 % (1693274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.43 % (1693274)CaDiCaL version: 2.1.3
% 0.85/0.43 % (1693274)Termination reason: Instruction limit
% 0.85/0.43 % (1693274)Termination phase: Preprocessing 3
% 0.85/0.43 % (1693274)Time elapsed: 0.004 s
% 0.85/0.43 % (1693274)Peak memory usage: 10 MB
% 0.85/0.43 % (1693274)Instructions burned: 9 (million)
% 0.85/0.43 % (1693276)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=1952186550:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.85/0.43 % (1693276)Instruction limit reached!
% 0.85/0.43 % (1693276)------------------------------
% 0.85/0.43 % (1693276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.43 % (1693276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.43 % (1693276)CaDiCaL version: 2.1.3
% 0.85/0.43 % (1693276)Termination reason: Instruction limit
% 0.85/0.43 % (1693276)Termination phase: Property scanning
% 0.85/0.43 % (1693276)Time elapsed: 0.003 s
% 0.85/0.43 % (1693276)Peak memory usage: 9 MB
% 0.85/0.43 % (1693276)Instructions burned: 7 (million)
% 0.85/0.43 % (1693277)Instruction limit reached!
% 0.85/0.43 % (1693277)------------------------------
% 0.85/0.43 % (1693277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.43 % (1693277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.43 % (1693277)CaDiCaL version: 2.1.3
% 0.85/0.43 % (1693277)Termination reason: Instruction limit
% 0.85/0.43 % (1693277)Termination phase: Saturation
% 0.85/0.43 % (1693277)Time elapsed: 0.010 s
% 0.85/0.43 % (1693277)Peak memory usage: 12 MB
% 0.85/0.43 % (1693277)Instructions burned: 42 (million)
% 0.85/0.43 % (1693279)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=486705019:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.85/0.43 % (1693237)Instruction limit reached!
% 0.85/0.43 % (1693237)------------------------------
% 0.85/0.43 % (1693237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.43 % (1693237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.43 % (1693237)CaDiCaL version: 2.1.3
% 0.85/0.43 % (1693237)Termination reason: Instruction limit
% 0.85/0.43 % (1693237)Termination phase: Saturation
% 0.85/0.43 % (1693237)Time elapsed: 0.069 s
% 0.85/0.43 % (1693237)Peak memory usage: 14 MB
% 0.85/0.43 % (1693237)Instructions burned: 162 (million)
% 0.85/0.43 % (1693282)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1207588733:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.85/0.43 % (1693286)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2278665446:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.85/0.43 % (1693272)Instruction limit reached!
% 0.85/0.43 % (1693272)------------------------------
% 0.85/0.43 % (1693272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.43 % (1693272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.43 % (1693272)CaDiCaL version: 2.1.3
% 0.85/0.43 % (1693272)Termination reason: Instruction limit
% 0.85/0.43 % (1693272)Termination phase: Saturation
% 0.85/0.43 % (1693272)Time elapsed: 0.037 s
% 1.58/0.48 % (1693272)Peak memory usage: 12 MB
% 1.58/0.48 % (1693272)Instructions burned: 88 (million)
% 1.58/0.48 % (1693284)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3465254664:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 1.58/0.48 % (1693282)Instruction limit reached!
% 1.58/0.48 % (1693282)------------------------------
% 1.58/0.48 % (1693282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.48 % (1693282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.48 % (1693282)CaDiCaL version: 2.1.3
% 1.58/0.48 % (1693282)Termination reason: Instruction limit
% 1.58/0.48 % (1693282)Termination phase: Property scanning
% 1.58/0.48 % (1693282)Time elapsed: 0.012 s
% 1.58/0.48 % (1693282)Peak memory usage: 11 MB
% 1.58/0.48 % (1693282)Instructions burned: 26 (million)
% 1.58/0.48 % (1693287)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1805841633:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.58/0.48 % (1693284)Instruction limit reached!
% 1.58/0.48 % (1693284)------------------------------
% 1.58/0.48 % (1693284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.48 % (1693284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.48 % (1693284)CaDiCaL version: 2.1.3
% 1.58/0.48 % (1693284)Termination reason: Instruction limit
% 1.58/0.48 % (1693284)Termination phase: Property scanning
% 1.58/0.48 % (1693284)Time elapsed: 0.007 s
% 1.58/0.48 % (1693284)Peak memory usage: 11 MB
% 1.58/0.48 % (1693284)Instructions burned: 16 (million)
% 1.58/0.48 % (1693287)Instruction limit reached!
% 1.58/0.48 % (1693287)------------------------------
% 1.58/0.48 % (1693287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.48 % (1693287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.48 % (1693287)CaDiCaL version: 2.1.3
% 1.58/0.48 % (1693287)Termination reason: Instruction limit
% 1.58/0.48 % (1693287)Termination phase: Property scanning
% 1.58/0.48 % (1693287)Time elapsed: 0.007 s
% 1.58/0.48 % (1693287)Peak memory usage: 10 MB
% 1.58/0.48 % (1693287)Instructions burned: 16 (million)
% 1.58/0.48 % (1693291)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3882652624:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.58/0.48 % (1693291)Instruction limit reached!
% 1.58/0.48 % (1693291)------------------------------
% 1.58/0.48 % (1693291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.48 % (1693291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.48 % (1693291)CaDiCaL version: 2.1.3
% 1.58/0.48 % (1693291)Termination reason: Instruction limit
% 1.58/0.48 % (1693291)Termination phase: shuffling
% 1.58/0.48 % (1693291)Time elapsed: 0.002 s
% 1.58/0.48 % (1693291)Peak memory usage: 9 MB
% 1.58/0.48 % (1693291)Instructions burned: 4 (million)
% 1.58/0.48 % (1693292)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2611079175:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.58/0.48 % (1693294)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3688139736:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.58/0.48 % (1693295)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=871320100:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.58/0.48 % (1693297)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.58/0.48 % (1693297)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.58/0.48 % (1693292)Instruction limit reached!
% 1.58/0.48 % (1693292)------------------------------
% 1.58/0.48 % (1693292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.48 % (1693292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.48 % (1693292)CaDiCaL version: 2.1.3
% 1.58/0.48 % (1693292)Termination reason: Instruction limit
% 1.58/0.48 % (1693292)Termination phase: Saturation
% 1.58/0.48 % (1693292)Time elapsed: 0.012 s
% 1.58/0.48 % (1693292)Peak memory usage: 11 MB
% 1.58/0.50 % (1693292)Instructions burned: 28 (million)
% 1.58/0.50 % (1693294)Instruction limit reached!
% 1.58/0.50 % (1693294)------------------------------
% 1.58/0.50 % (1693294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (1693294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (1693294)CaDiCaL version: 2.1.3
% 1.58/0.50 % (1693294)Termination reason: Instruction limit
% 1.58/0.50 % (1693294)Termination phase: Saturation
% 1.58/0.50 % (1693294)Time elapsed: 0.010 s
% 1.58/0.50 % (1693294)Peak memory usage: 12 MB
% 1.58/0.50 % (1693294)Instructions burned: 23 (million)
% 1.58/0.50 % (1693297)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=2171713734:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.58/0.50 % (1693297)Instruction limit reached!
% 1.58/0.50 % (1693297)------------------------------
% 1.58/0.50 % (1693297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (1693297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (1693297)CaDiCaL version: 2.1.3
% 1.58/0.50 % (1693297)Termination reason: Instruction limit
% 1.58/0.50 % (1693297)Termination phase: Function definition elimination
% 1.58/0.50 % (1693297)Time elapsed: 0.006 s
% 1.58/0.50 % (1693297)Peak memory usage: 10 MB
% 1.58/0.50 % (1693297)Instructions burned: 15 (million)
% 1.58/0.50 % (1693301)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.58/0.50 % (1693301)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=2537161098:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.58/0.50 % (1693302)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=2069550567:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.58/0.50 % (1693301)Instruction limit reached!
% 1.58/0.50 % (1693301)------------------------------
% 1.58/0.50 % (1693301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (1693301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (1693301)CaDiCaL version: 2.1.3
% 1.58/0.50 % (1693301)Termination reason: Instruction limit
% 1.58/0.50 % (1693301)Termination phase: SInE selection
% 1.58/0.50 % (1693301)Time elapsed: 0.004 s
% 1.58/0.50 % (1693301)Peak memory usage: 10 MB
% 1.58/0.50 % (1693301)Instructions burned: 9 (million)
% 1.58/0.50 % (1693295)Instruction limit reached!
% 1.58/0.50 % (1693295)------------------------------
% 1.58/0.50 % (1693295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (1693295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (1693295)CaDiCaL version: 2.1.3
% 1.58/0.50 % (1693295)Termination reason: Instruction limit
% 1.58/0.50 % (1693295)Termination phase: Saturation
% 1.58/0.50 % (1693295)Time elapsed: 0.030 s
% 1.58/0.50 % (1693295)Peak memory usage: 12 MB
% 1.58/0.50 % (1693295)Instructions burned: 61 (million)
% 1.58/0.50 % (1693304)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=750069782:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.58/0.50 % (1693304)Instruction limit reached!
% 1.58/0.50 % (1693304)------------------------------
% 1.58/0.50 % (1693304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (1693304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (1693304)CaDiCaL version: 2.1.3
% 1.58/0.50 % (1693304)Termination reason: Instruction limit
% 1.58/0.50 % (1693304)Termination phase: Naming
% 1.58/0.50 % (1693304)Time elapsed: 0.004 s
% 1.58/0.50 % (1693304)Peak memory usage: 10 MB
% 1.58/0.50 % (1693304)Instructions burned: 9 (million)
% 1.58/0.50 % (1693302)Instruction limit reached!
% 1.58/0.50 % (1693302)------------------------------
% 1.58/0.50 % (1693302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (1693302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (1693302)CaDiCaL version: 2.1.3
% 1.58/0.50 % (1693302)Termination reason: Instruction limit
% 1.58/0.50 % (1693302)Termination phase: Saturation
% 1.58/0.50 % (1693302)Time elapsed: 0.015 s
% 1.58/0.50 % (1693302)Peak memory usage: 12 MB
% 1.58/0.50 % (1693302)Instructions burned: 31 (million)
% 1.58/0.50 % (1693307)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2270762176:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.58/0.50 % (1693286)Instruction limit reached!
% 1.58/0.50 % (1693286)------------------------------
% 1.58/0.50 % (1693286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (1693286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (1693286)CaDiCaL version: 2.1.3
% 1.58/0.50 % (1693286)Termination reason: Instruction limit
% 1.58/0.50 % (1693286)Termination phase: Saturation
% 1.58/0.50 % (1693286)Time elapsed: 0.090 s
% 1.58/0.50 % (1693286)Peak memory usage: 14 MB
% 1.58/0.50 % (1693286)Instructions burned: 336 (million)
% 1.58/0.50 % (1693308)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3837455937:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.58/0.50 % (1693310)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1897145133:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.58/0.50 % (1693307)Instruction limit reached!
% 1.58/0.50 % (1693307)------------------------------
% 1.58/0.50 % (1693307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (1693307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (1693307)CaDiCaL version: 2.1.3
% 1.58/0.50 % (1693307)Termination reason: Instruction limit
% 1.58/0.50 % (1693307)Termination phase: Saturation
% 1.58/0.50 % (1693307)Time elapsed: 0.010 s
% 1.58/0.50 % (1693307)Peak memory usage: 11 MB
% 1.58/0.50 % (1693307)Instructions burned: 23 (million)
% 1.58/0.50 % (1693311)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1302271:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.58/0.50 % (1693314)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2074577435:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 1.58/0.50 % (1693308)Instruction limit reached!
% 1.58/0.50 % (1693308)------------------------------
% 1.58/0.50 % (1693308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (1693308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (1693308)CaDiCaL version: 2.1.3
% 1.58/0.50 % (1693308)Termination reason: Instruction limit
% 1.58/0.50 % (1693308)Termination phase: Saturation
% 1.58/0.50 % (1693308)Time elapsed: 0.010 s
% 1.58/0.50 % (1693308)Peak memory usage: 12 MB
% 1.58/0.50 % (1693308)Instructions burned: 21 (million)
% 1.58/0.50 % (1693316)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3604164990:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 1.58/0.50 % (1693279)Instruction limit reached!
% 1.58/0.50 % (1693279)------------------------------
% 1.58/0.50 % (1693279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (1693279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (1693279)CaDiCaL version: 2.1.3
% 1.58/0.50 % (1693279)Termination reason: Instruction limit
% 1.58/0.50 % (1693279)Termination phase: Saturation
% 1.58/0.50 % (1693279)Time elapsed: 0.128 s
% 1.58/0.50 % (1693279)Peak memory usage: 13 MB
% 1.58/0.50 % (1693279)Instructions burned: 251 (million)
% 1.58/0.50 % (1693319)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.58/0.50 % (1693319)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=566550086:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 1.58/0.50 % (1693319)Instruction limit reached!
% 1.58/0.50 % (1693319)------------------------------
% 1.58/0.50 % (1693319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (1693319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (1693319)CaDiCaL version: 2.1.3
% 1.58/0.50 % (1693319)Termination reason: Instruction limit
% 1.58/0.50 % (1693319)Termination phase: Property scanning
% 1.58/0.50 % (1693319)Time elapsed: 0.004 s
% 1.58/0.50 % (1693319)Peak memory usage: 9 MB
% 1.58/0.50 % (1693319)Instructions burned: 9 (million)
% 1.58/0.50 % (1693316)Instruction limit reached!
% 1.58/0.50 % (1693316)------------------------------
% 1.58/0.50 % (1693316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (1693316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (1693316)CaDiCaL version: 2.1.3
% 1.58/0.50 % (1693316)Termination reason: Instruction limit
% 1.58/0.50 % (1693316)Termination phase: Saturation
% 1.58/0.50 % (1693316)Time elapsed: 0.021 s
% 1.58/0.50 % (1693316)Peak memory usage: 13 MB
% 1.58/0.50 % (1693316)Instructions burned: 43 (million)
% 1.58/0.50 % (1693321)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3379391220:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 1.58/0.50 % (1693310) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1693208-1693310"...
% 1.58/0.50 % (1693323)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=3130409192:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 1.58/0.50 % (1693310)...printing done.
% 1.58/0.50 % (1693324)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 1.58/0.50 % (1693310)Refutation found. Thanks to Tanya!
% 1.58/0.50 % SZS status Theorem for theBenchmark
% 1.58/0.50 % SZS output start Proof for theBenchmark
% See solution above
% 1.58/0.50 % (1693310)------------------------------
% 1.58/0.50 % (1693310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.51 % (1693310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.51 % (1693310)CaDiCaL version: 2.1.3
% 1.58/0.51 % (1693310)Termination reason: Refutation
% 1.58/0.51 % (1693310)Time elapsed: 0.056 s
% 1.58/0.51 % (1693310)Peak memory usage: 14 MB
% 1.58/0.51 % (1693310)Instructions burned: 111 (million)
% 1.58/0.51 % (1693208)Success in time 0.268 s
% 1.58/0.51 % Vampire exiting
%------------------------------------------------------------------------------