%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU743^2 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:33:13 AM UTC 2026
% Result : Theorem 169.78s 24.24s
% Output : Refutation 169.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 46
% Syntax : Number of formulae : 330 ( 94 unt; 0 typ; 41 def)
% Number of atoms : 2997 ( 582 equ; 0 cnn)
% Maximal formula atoms : 13 ( 9 avg)
% Number of connectives : 3909 ( 352 ~; 679 |; 28 &;2444 @)
% ( 27 <=>; 242 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 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 : 68 ( 64 usr; 52 con; 0-4 aty)
% ( 137 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 409 ( 0 sgn 245 !; 12 ?; 409 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
in: $i > $i > $o ).
thf(func_def_1,type,
powerset: $i > $i ).
thf(func_def_2,type,
binunion: $i > $i > $i ).
thf(func_def_3,type,
binintersect: $i > $i > $i ).
thf(func_def_4,type,
binintersectT_lem: $o ).
thf(func_def_6,type,
binunionT_lem: $o ).
thf(func_def_7,type,
powersetTI1: $o ).
thf(func_def_8,type,
inIntersectImpInIntersectUnions: $o ).
thf(func_def_9,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_10,type,
vIMP: $o > $o > $o ).
thf(func_def_11,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_12,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_13,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_14,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_15,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_16,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_23,type,
sF4: $o ).
thf(func_def_24,type,
sF5: $o ).
thf(func_def_26,type,
sF7: $o ).
thf(func_def_32,type,
sF13: $o ).
thf(func_def_33,type,
sF14: $o ).
thf(func_def_34,type,
sF15: $o ).
thf(func_def_35,type,
sF16: $o ).
thf(func_def_36,type,
sF17: $o ).
thf(func_def_37,type,
vNOT: $o > $o ).
thf(func_def_38,type,
sK18: $i > $i > $i > $i ).
thf(f1,axiom,
! [X0: $i,X1: $i] :
( ( ( in @ X1 @ ( powerset @ X0 ) )
=> ! [X2: $i] :
( ( in @ X2 @ ( powerset @ X0 ) )
=> ( in @ ( binintersect @ X1 @ X2 ) @ ( powerset @ X0 ) ) ) )
= binintersectT_lem ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',binintersectT_lem) ).
thf(f2,axiom,
( binunionT_lem
= ( ! [X0: $i,X1: $i] :
( ( in @ X1 @ ( powerset @ X0 ) )
=> ! [X2: $i] :
( ( in @ X2 @ ( powerset @ X0 ) )
=> ( in @ ( binunion @ X1 @ X2 ) @ ( powerset @ X0 ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',binunionT_lem) ).
thf(f3,axiom,
! [X0: $i,X1: $i] :
( ( ( in @ X1 @ ( powerset @ X0 ) )
=> ! [X2: $i] :
( ( in @ X2 @ ( powerset @ X0 ) )
=> ( ! [X3: $i] :
( ( in @ X3 @ X0 )
=> ( ( in @ X3 @ X1 )
=> ( in @ X3 @ X2 ) ) )
=> ( in @ X1 @ ( powerset @ X2 ) ) ) ) )
= powersetTI1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',powersetTI1) ).
thf(f4,axiom,
( inIntersectImpInIntersectUnions
= ( ! [X0: $i,X1: $i] :
( ( in @ X1 @ ( powerset @ X0 ) )
=> ! [X2: $i] :
( ( in @ X2 @ ( powerset @ X0 ) )
=> ! [X3: $i] :
( ( in @ X3 @ ( powerset @ X0 ) )
=> ! [X4: $i] :
( ( in @ X4 @ X0 )
=> ( ( in @ X4 @ ( binintersect @ X1 @ X2 ) )
=> ( in @ X4 @ ( binintersect @ ( binunion @ X1 @ X3 ) @ ( binunion @ X2 @ X3 ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inIntersectImpInIntersectUnions) ).
thf(f5,conjecture,
( binintersectT_lem
=> ( binunionT_lem
=> ( powersetTI1
=> ( inIntersectImpInIntersectUnions
=> ! [X1: $i,X0: $i] :
( ( in @ X1 @ ( powerset @ X0 ) )
=> ! [X2: $i] :
( ( in @ X2 @ ( powerset @ X0 ) )
=> ! [X3: $i] :
( ( in @ X3 @ ( powerset @ X0 ) )
=> ( in @ ( binintersect @ X1 @ X2 ) @ ( powerset @ ( binintersect @ ( binunion @ X1 @ X3 ) @ ( binunion @ X2 @ X3 ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersectInPowersetIntersectUnions) ).
thf(f6,negated_conjecture,
~ ( binintersectT_lem
=> ( binunionT_lem
=> ( powersetTI1
=> ( inIntersectImpInIntersectUnions
=> ! [X1: $i,X0: $i] :
( ( in @ X1 @ ( powerset @ X0 ) )
=> ! [X2: $i] :
( ( in @ X2 @ ( powerset @ X0 ) )
=> ! [X3: $i] :
( ( in @ X3 @ ( powerset @ X0 ) )
=> ( in @ ( binintersect @ X1 @ X2 ) @ ( powerset @ ( binintersect @ ( binunion @ X1 @ X3 ) @ ( binunion @ X2 @ X3 ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f5]) ).
thf(f7,plain,
( binunionT_lem
= ( ! [X0: $i,X1: $i] :
( ( in @ X1 @ ( powerset @ X0 ) )
=> ! [X2: $i] :
( ( in @ X2 @ ( powerset @ X0 ) )
=> ( in @ ( binunion @ X1 @ X2 ) @ ( powerset @ X0 ) ) ) ) ) ),
inference(rectify,[],[f2]) ).
thf(f8,plain,
( binunionT_lem
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( in @ ( binunion @ Y0 @ Y2 ) @ ( powerset @ Y1 ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f7]) ).
thf(f9,plain,
( inIntersectImpInIntersectUnions
= ( ! [X0: $i,X1: $i] :
( ( in @ X1 @ ( powerset @ X0 ) )
=> ! [X2: $i] :
( ( in @ X2 @ ( powerset @ X0 ) )
=> ! [X3: $i] :
( ( in @ X3 @ ( powerset @ X0 ) )
=> ! [X4: $i] :
( ( in @ X4 @ X0 )
=> ( ( in @ X4 @ ( binintersect @ X1 @ X2 ) )
=> ( in @ X4 @ ( binintersect @ ( binunion @ X1 @ X3 ) @ ( binunion @ X2 @ X3 ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f4]) ).
thf(f10,plain,
( inIntersectImpInIntersectUnions
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y1 )
=> ( ( in @ Y4 @ ( binintersect @ Y0 @ Y2 ) )
=> ( in @ Y4 @ ( binintersect @ ( binunion @ Y0 @ Y3 ) @ ( binunion @ Y2 @ Y3 ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f9]) ).
thf(f11,plain,
! [X0: $i,X1: $i] :
( ( ( in @ X1 @ ( powerset @ X0 ) )
=> ! [X2: $i] :
( ( in @ X2 @ ( powerset @ X0 ) )
=> ( in @ ( binintersect @ X1 @ X2 ) @ ( powerset @ X0 ) ) ) )
= binintersectT_lem ),
inference(rectify,[],[f1]) ).
thf(f12,plain,
( binintersectT_lem
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( in @ ( binintersect @ Y0 @ Y2 ) @ ( powerset @ Y1 ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f11]) ).
thf(f13,plain,
~ ( binintersectT_lem
=> ( binunionT_lem
=> ( powersetTI1
=> ( inIntersectImpInIntersectUnions
=> ! [X0: $i,X1: $i] :
( ( in @ X0 @ ( powerset @ X1 ) )
=> ! [X2: $i] :
( ( in @ X2 @ ( powerset @ X1 ) )
=> ! [X3: $i] :
( ( in @ X3 @ ( powerset @ X1 ) )
=> ( in @ ( binintersect @ X0 @ X2 ) @ ( powerset @ ( binintersect @ ( binunion @ X0 @ X3 ) @ ( binunion @ X2 @ X3 ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f6]) ).
thf(f14,plain,
~ ( ( binintersectT_lem = $true )
=> ( ( binunionT_lem = $true )
=> ( ( powersetTI1 = $true )
=> ( ( inIntersectImpInIntersectUnions = $true )
=> ! [X0: $i,X1: $i] :
( ( ( in @ X0 @ ( powerset @ X1 ) )
= $true )
=> ! [X2: $i] :
( ( ( in @ X2 @ ( powerset @ X1 ) )
= $true )
=> ! [X3: $i] :
( ( ( in @ X3 @ ( powerset @ X1 ) )
= $true )
=> ( ( in @ ( binintersect @ X0 @ X2 ) @ ( powerset @ ( binintersect @ ( binunion @ X0 @ X3 ) @ ( binunion @ X2 @ X3 ) ) ) )
= $true ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f13]) ).
thf(f15,plain,
! [X0: $i,X1: $i] :
( ( ( in @ X1 @ ( powerset @ X0 ) )
=> ! [X2: $i] :
( ( in @ X2 @ ( powerset @ X0 ) )
=> ( ! [X3: $i] :
( ( in @ X3 @ X0 )
=> ( ( in @ X3 @ X1 )
=> ( in @ X3 @ X2 ) ) )
=> ( in @ X1 @ ( powerset @ X2 ) ) ) ) )
= powersetTI1 ),
inference(rectify,[],[f3]) ).
thf(f16,plain,
( powersetTI1
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y1 )
=> ( ( in @ Y3 @ Y0 )
=> ( in @ Y3 @ Y2 ) ) ) )
=> ( in @ Y0 @ ( powerset @ Y2 ) ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f15]) ).
thf(f17,plain,
( ? [X1: $i,X0: $i] :
( ? [X2: $i] :
( ( ( in @ X2 @ ( powerset @ X1 ) )
= $true )
& ? [X3: $i] :
( ( ( in @ ( binintersect @ X0 @ X2 ) @ ( powerset @ ( binintersect @ ( binunion @ X0 @ X3 ) @ ( binunion @ X2 @ X3 ) ) ) )
!= $true )
& ( ( in @ X3 @ ( powerset @ X1 ) )
= $true ) ) )
& ( ( in @ X0 @ ( powerset @ X1 ) )
= $true ) )
& ( inIntersectImpInIntersectUnions = $true )
& ( powersetTI1 = $true )
& ( binunionT_lem = $true )
& ( binintersectT_lem = $true ) ),
inference(ennf_transformation,[],[f14]) ).
thf(f18,plain,
( ? [X1: $i,X0: $i] :
( ? [X2: $i] :
( ( ( in @ X2 @ ( powerset @ X1 ) )
= $true )
& ? [X3: $i] :
( ( ( in @ ( binintersect @ X0 @ X2 ) @ ( powerset @ ( binintersect @ ( binunion @ X0 @ X3 ) @ ( binunion @ X2 @ X3 ) ) ) )
!= $true )
& ( ( in @ X3 @ ( powerset @ X1 ) )
= $true ) ) )
& ( ( in @ X0 @ ( powerset @ X1 ) )
= $true ) )
& ( binunionT_lem = $true )
& ( binintersectT_lem = $true )
& ( inIntersectImpInIntersectUnions = $true )
& ( powersetTI1 = $true ) ),
inference(flattening,[],[f17]) ).
thf(f19,plain,
( ? [X0: $i,X1: $i] :
( ? [X2: $i] :
( ( ( in @ X2 @ ( powerset @ X0 ) )
= $true )
& ? [X3: $i] :
( ( ( in @ ( binintersect @ X1 @ X2 ) @ ( powerset @ ( binintersect @ ( binunion @ X1 @ X3 ) @ ( binunion @ X2 @ X3 ) ) ) )
!= $true )
& ( ( in @ X3 @ ( powerset @ X0 ) )
= $true ) ) )
& ( ( in @ X1 @ ( powerset @ X0 ) )
= $true ) )
& ( binunionT_lem = $true )
& ( binintersectT_lem = $true )
& ( inIntersectImpInIntersectUnions = $true )
& ( powersetTI1 = $true ) ),
inference(rectify,[],[f18]) ).
thf(f20,plain,
( ( ( in @ sK2 @ ( powerset @ sK0 ) )
= $true )
& ( $true
!= ( in @ ( binintersect @ sK1 @ sK2 ) @ ( powerset @ ( binintersect @ ( binunion @ sK1 @ sK3 ) @ ( binunion @ sK2 @ sK3 ) ) ) ) )
& ( $true
= ( in @ sK3 @ ( powerset @ sK0 ) ) )
& ( $true
= ( in @ sK1 @ ( powerset @ sK0 ) ) )
& ( binunionT_lem = $true )
& ( binintersectT_lem = $true )
& ( inIntersectImpInIntersectUnions = $true )
& ( powersetTI1 = $true ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f19]) ).
thf(f21,plain,
( binunionT_lem
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( in @ ( binunion @ Y0 @ Y2 ) @ ( powerset @ Y1 ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f8]) ).
thf(f22,plain,
( powersetTI1
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y1 )
=> ( ( in @ Y3 @ Y0 )
=> ( in @ Y3 @ Y2 ) ) ) )
=> ( in @ Y0 @ ( powerset @ Y2 ) ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f16]) ).
thf(f23,plain,
powersetTI1 = $true,
inference(cnf_transformation,[],[f20]) ).
thf(f24,plain,
inIntersectImpInIntersectUnions = $true,
inference(cnf_transformation,[],[f20]) ).
thf(f25,plain,
binintersectT_lem = $true,
inference(cnf_transformation,[],[f20]) ).
thf(f26,plain,
binunionT_lem = $true,
inference(cnf_transformation,[],[f20]) ).
thf(f27,plain,
( $true
= ( in @ sK1 @ ( powerset @ sK0 ) ) ),
inference(cnf_transformation,[],[f20]) ).
thf(f28,plain,
( $true
= ( in @ sK3 @ ( powerset @ sK0 ) ) ),
inference(cnf_transformation,[],[f20]) ).
thf(f29,plain,
( $true
!= ( in @ ( binintersect @ sK1 @ sK2 ) @ ( powerset @ ( binintersect @ ( binunion @ sK1 @ sK3 ) @ ( binunion @ sK2 @ sK3 ) ) ) ) ),
inference(cnf_transformation,[],[f20]) ).
thf(f30,plain,
( ( in @ sK2 @ ( powerset @ sK0 ) )
= $true ),
inference(cnf_transformation,[],[f20]) ).
thf(f31,plain,
( binintersectT_lem
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( in @ ( binintersect @ Y0 @ Y2 ) @ ( powerset @ Y1 ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f12]) ).
thf(f32,plain,
( inIntersectImpInIntersectUnions
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y1 )
=> ( ( in @ Y4 @ ( binintersect @ Y0 @ Y2 ) )
=> ( in @ Y4 @ ( binintersect @ ( binunion @ Y0 @ Y3 ) @ ( binunion @ Y2 @ Y3 ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f10]) ).
thf(f35,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( in @ ( binunion @ Y0 @ Y2 ) @ ( powerset @ Y1 ) ) ) ) ) ) )
= $true ),
inference(definition_unfolding,[],[f21,f26]) ).
thf(f36,plain,
( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y1 )
=> ( ( in @ Y3 @ Y0 )
=> ( in @ Y3 @ Y2 ) ) ) )
=> ( in @ Y0 @ ( powerset @ Y2 ) ) ) ) ) ) ) ) ),
inference(definition_unfolding,[],[f22,f23]) ).
thf(f37,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( in @ ( binintersect @ Y0 @ Y2 ) @ ( powerset @ Y1 ) ) ) ) ) ) )
= $true ),
inference(definition_unfolding,[],[f31,f25]) ).
thf(f38,plain,
( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y1 )
=> ( ( in @ Y4 @ ( binintersect @ Y0 @ Y2 ) )
=> ( in @ Y4 @ ( binintersect @ ( binunion @ Y0 @ Y3 ) @ ( binunion @ Y2 @ Y3 ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(definition_unfolding,[],[f32,f24]) ).
thf(f39,definition,
( sF4
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( in @ ( binunion @ Y0 @ Y2 ) @ ( powerset @ Y1 ) ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
thf(f40,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( in @ ( binunion @ Y0 @ Y2 ) @ ( powerset @ Y1 ) ) ) ) ) ) )
= sF4 ),
inference(reorient_equations,[],[f39]) ).
thf(f41,plain,
$true = sF4,
inference(definition_folding,[],[f35,f40]) ).
thf(f42,definition,
( sF5
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y1 )
=> ( ( in @ Y3 @ Y0 )
=> ( in @ Y3 @ Y2 ) ) ) )
=> ( in @ Y0 @ ( powerset @ Y2 ) ) ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
thf(f43,plain,
$true = sF5,
inference(definition_folding,[],[f36,f42]) ).
thf(f44,definition,
( sF6
= ( powerset @ sK0 ) ),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
thf(f45,definition,
( sF7
= ( in @ sK2 @ sF6 ) ),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
thf(f46,plain,
( ( in @ sK2 @ sF6 )
= sF7 ),
inference(reorient_equations,[],[f45]) ).
thf(f47,plain,
sF7 = $true,
inference(definition_folding,[],[f30,f46,f44]) ).
thf(f48,definition,
( sF8
= ( binintersect @ sK1 @ sK2 ) ),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
thf(f49,plain,
( ( binintersect @ sK1 @ sK2 )
= sF8 ),
inference(reorient_equations,[],[f48]) ).
thf(f50,definition,
( sF9
= ( binunion @ sK1 @ sK3 ) ),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
thf(f51,plain,
( ( binunion @ sK1 @ sK3 )
= sF9 ),
inference(reorient_equations,[],[f50]) ).
thf(f52,definition,
( sF10
= ( binunion @ sK2 @ sK3 ) ),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
thf(f53,plain,
( ( binunion @ sK2 @ sK3 )
= sF10 ),
inference(reorient_equations,[],[f52]) ).
thf(f54,definition,
( sF11
= ( binintersect @ sF9 @ sF10 ) ),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
thf(f55,definition,
( sF12
= ( powerset @ sF11 ) ),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
thf(f56,definition,
( sF13
= ( in @ sF8 @ sF12 ) ),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
thf(f57,plain,
$true != sF13,
inference(definition_folding,[],[f29,f56,f55,f54,f53,f51,f49]) ).
thf(f58,definition,
( sF14
= ( in @ sK3 @ sF6 ) ),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
thf(f59,plain,
( ( in @ sK3 @ sF6 )
= sF14 ),
inference(reorient_equations,[],[f58]) ).
thf(f60,plain,
$true = sF14,
inference(definition_folding,[],[f28,f59,f44]) ).
thf(f61,definition,
( sF15
= ( in @ sK1 @ sF6 ) ),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
thf(f62,plain,
$true = sF15,
inference(definition_folding,[],[f27,f61,f44]) ).
thf(f63,definition,
( sF16
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( in @ ( binintersect @ Y0 @ Y2 ) @ ( powerset @ Y1 ) ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
thf(f64,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( in @ ( binintersect @ Y0 @ Y2 ) @ ( powerset @ Y1 ) ) ) ) ) ) )
= sF16 ),
inference(reorient_equations,[],[f63]) ).
thf(f65,plain,
$true = sF16,
inference(definition_folding,[],[f37,f64]) ).
thf(f66,definition,
( sF17
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y1 )
=> ( ( in @ Y4 @ ( binintersect @ Y0 @ Y2 ) )
=> ( in @ Y4 @ ( binintersect @ ( binunion @ Y0 @ Y3 ) @ ( binunion @ Y2 @ Y3 ) ) ) ) ) ) ) ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
thf(f67,plain,
$true = sF17,
inference(definition_folding,[],[f38,f66]) ).
thf(f69,plain,
( ( $false = sF5 )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y1 )
=> ( ( in @ Y3 @ Y0 )
=> ( in @ Y3 @ Y2 ) ) ) )
=> ( in @ Y0 @ ( powerset @ Y2 ) ) ) ) ) ) ) ) ) ),
inference(iff_proxy_clausification,[],[f42]) ).
thf(f70,plain,
! [X1: $i] :
( ( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y1 )
=> ( ( in @ Y3 @ Y0 )
=> ( in @ Y3 @ Y2 ) ) ) )
=> ( in @ Y0 @ ( powerset @ Y2 ) ) ) ) ) ) )
@ X1 )
= $true )
| ( $false = sF5 ) ),
inference(pi_proxy_clausification,[],[f69]) ).
thf(f71,plain,
! [X1: $i] :
( ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ X1 @ ( powerset @ Y0 ) )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ ( powerset @ Y0 ) )
=> ( ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ Y0 )
=> ( ( in @ Y2 @ X1 )
=> ( in @ Y2 @ Y1 ) ) ) )
=> ( in @ X1 @ ( powerset @ Y1 ) ) ) ) ) ) ) )
| ( $false = sF5 ) ),
inference(beta-eta_normalization,[],[f70]) ).
thf(f72,plain,
! [X2: $i,X1: $i] :
( ( $true
= ( ^ [Y0: $i] :
( ( in @ X1 @ ( powerset @ Y0 ) )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ ( powerset @ Y0 ) )
=> ( ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ Y0 )
=> ( ( in @ Y2 @ X1 )
=> ( in @ Y2 @ Y1 ) ) ) )
=> ( in @ X1 @ ( powerset @ Y1 ) ) ) ) ) )
@ X2 ) )
| ( $false = sF5 ) ),
inference(pi_proxy_clausification,[],[f71]) ).
thf(f73,plain,
! [X2: $i,X1: $i] :
( ( $true
= ( ( in @ X1 @ ( powerset @ X2 ) )
=> ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ ( powerset @ X2 ) )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ X2 )
=> ( ( in @ Y1 @ X1 )
=> ( in @ Y1 @ Y0 ) ) ) )
=> ( in @ X1 @ ( powerset @ Y0 ) ) ) ) ) ) )
| ( $false = sF5 ) ),
inference(beta-eta_normalization,[],[f72]) ).
thf(f74,plain,
! [X2: $i,X1: $i] :
( ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ ( powerset @ X2 ) )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ X2 )
=> ( ( in @ Y1 @ X1 )
=> ( in @ Y1 @ Y0 ) ) ) )
=> ( in @ X1 @ ( powerset @ Y0 ) ) ) ) ) )
| ( $false = sF5 )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false ) ),
inference(imp_proxy_clausification,[],[f73]) ).
thf(f75,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $false = sF5 )
| ( ( ^ [Y0: $i] :
( ( in @ Y0 @ ( powerset @ X2 ) )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ X2 )
=> ( ( in @ Y1 @ X1 )
=> ( in @ Y1 @ Y0 ) ) ) )
=> ( in @ X1 @ ( powerset @ Y0 ) ) ) )
@ X3 )
= $true )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false ) ),
inference(pi_proxy_clausification,[],[f74]) ).
thf(f76,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $true
= ( ( in @ X3 @ ( powerset @ X2 ) )
=> ( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ X2 )
=> ( ( in @ Y0 @ X1 )
=> ( in @ Y0 @ X3 ) ) ) )
=> ( in @ X1 @ ( powerset @ X3 ) ) ) ) )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $false = sF5 ) ),
inference(beta-eta_normalization,[],[f75]) ).
thf(f77,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $true
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ X2 )
=> ( ( in @ Y0 @ X1 )
=> ( in @ Y0 @ X3 ) ) ) )
=> ( in @ X1 @ ( powerset @ X3 ) ) ) )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( $false = sF5 ) ),
inference(imp_proxy_clausification,[],[f76]) ).
thf(f78,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $true
= ( in @ X1 @ ( powerset @ X3 ) ) )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ X2 )
=> ( ( in @ Y0 @ X1 )
=> ( in @ Y0 @ X3 ) ) ) ) )
| ( $false = sF5 ) ),
inference(imp_proxy_clausification,[],[f77]) ).
thf(f79,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $false = sF5 )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $true
= ( in @ X1 @ ( powerset @ X3 ) ) )
| ( ( ^ [Y0: $i] :
( ( in @ Y0 @ X2 )
=> ( ( in @ Y0 @ X1 )
=> ( in @ Y0 @ X3 ) ) )
@ ( sK18 @ X3 @ X1 @ X2 ) )
= $false ) ),
inference(sigma_proxy_clausification,[],[f78]) ).
thf(f80,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $true
= ( in @ X1 @ ( powerset @ X3 ) ) )
| ( $false = sF5 )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( ( ( in @ ( sK18 @ X3 @ X1 @ X2 ) @ X2 )
=> ( ( in @ ( sK18 @ X3 @ X1 @ X2 ) @ X1 )
=> ( in @ ( sK18 @ X3 @ X1 @ X2 ) @ X3 ) ) )
= $false )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false ) ),
inference(beta-eta_normalization,[],[f79]) ).
thf(f81,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $false = sF5 )
| ( $true
= ( in @ X1 @ ( powerset @ X3 ) ) )
| ( ( ( in @ ( sK18 @ X3 @ X1 @ X2 ) @ X1 )
=> ( in @ ( sK18 @ X3 @ X1 @ X2 ) @ X3 ) )
= $false ) ),
inference(imp_proxy_clausification,[],[f80]) ).
thf(f82,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $false = sF5 )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $true
= ( in @ X1 @ ( powerset @ X3 ) ) )
| ( $true
= ( in @ ( sK18 @ X3 @ X1 @ X2 ) @ X2 ) )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) ) ),
inference(imp_proxy_clausification,[],[f80]) ).
thf(f83,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $true
= ( in @ X1 @ ( powerset @ X3 ) ) )
| ( $false = sF5 )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( ( in @ ( sK18 @ X3 @ X1 @ X2 ) @ X3 )
= $false ) ),
inference(imp_proxy_clausification,[],[f81]) ).
thf(f84,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( in @ ( sK18 @ X3 @ X1 @ X2 ) @ X1 )
= $true )
| ( $true
= ( in @ X1 @ ( powerset @ X3 ) ) )
| ( $false = sF5 )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false ) ),
inference(imp_proxy_clausification,[],[f81]) ).
thf(f101,plain,
( ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( in @ ( binintersect @ Y0 @ Y2 ) @ ( powerset @ Y1 ) ) ) ) ) ) )
= $true )
| ( $false = sF16 ) ),
inference(iff_proxy_clausification,[],[f64]) ).
thf(f113,plain,
! [X1: $i] :
( ( $false = sF16 )
| ( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( in @ ( binintersect @ Y0 @ Y2 ) @ ( powerset @ Y1 ) ) ) ) ) )
@ X1 ) ) ),
inference(pi_proxy_clausification,[],[f101]) ).
thf(f114,plain,
! [X1: $i] :
( ( $false = sF16 )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ X1 @ ( powerset @ Y0 ) )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ ( powerset @ Y0 ) )
=> ( in @ ( binintersect @ X1 @ Y1 ) @ ( powerset @ Y0 ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f113]) ).
thf(f115,plain,
! [X2: $i,X1: $i] :
( ( $false = sF16 )
| ( $true
= ( ^ [Y0: $i] :
( ( in @ X1 @ ( powerset @ Y0 ) )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ ( powerset @ Y0 ) )
=> ( in @ ( binintersect @ X1 @ Y1 ) @ ( powerset @ Y0 ) ) ) ) )
@ X2 ) ) ),
inference(pi_proxy_clausification,[],[f114]) ).
thf(f116,plain,
! [X2: $i,X1: $i] :
( ( $false = sF16 )
| ( $true
= ( ( in @ X1 @ ( powerset @ X2 ) )
=> ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ ( powerset @ X2 ) )
=> ( in @ ( binintersect @ X1 @ Y0 ) @ ( powerset @ X2 ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f115]) ).
thf(f117,plain,
! [X2: $i,X1: $i] :
( ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $false = sF16 )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ ( powerset @ X2 ) )
=> ( in @ ( binintersect @ X1 @ Y0 ) @ ( powerset @ X2 ) ) ) )
= $true ) ),
inference(imp_proxy_clausification,[],[f116]) ).
thf(f118,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $true
= ( ^ [Y0: $i] :
( ( in @ Y0 @ ( powerset @ X2 ) )
=> ( in @ ( binintersect @ X1 @ Y0 ) @ ( powerset @ X2 ) ) )
@ X3 ) )
| ( $false = sF16 )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false ) ),
inference(pi_proxy_clausification,[],[f117]) ).
thf(f119,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $false = sF16 )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( ( ( in @ X3 @ ( powerset @ X2 ) )
=> ( in @ ( binintersect @ X1 @ X3 ) @ ( powerset @ X2 ) ) )
= $true ) ),
inference(beta-eta_normalization,[],[f118]) ).
thf(f120,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $true
= ( in @ ( binintersect @ X1 @ X3 ) @ ( powerset @ X2 ) ) )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( $false = sF16 ) ),
inference(imp_proxy_clausification,[],[f119]) ).
thf(f121,plain,
( ( $true = sF13 )
| ( $false
= ( in @ sF8 @ sF12 ) ) ),
inference(iff_proxy_clausification,[],[f56]) ).
thf(f123,plain,
( ( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( in @ ( binunion @ Y0 @ Y2 ) @ ( powerset @ Y1 ) ) ) ) ) ) )
= $true )
| ( sF4 = $false ) ),
inference(iff_proxy_clausification,[],[f40]) ).
thf(f135,plain,
! [X1: $i] :
( ( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( in @ ( binunion @ Y0 @ Y2 ) @ ( powerset @ Y1 ) ) ) ) ) )
@ X1 ) )
| ( sF4 = $false ) ),
inference(pi_proxy_clausification,[],[f123]) ).
thf(f136,plain,
! [X1: $i] :
( ( sF4 = $false )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ X1 @ ( powerset @ Y0 ) )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ ( powerset @ Y0 ) )
=> ( in @ ( binunion @ X1 @ Y1 ) @ ( powerset @ Y0 ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f135]) ).
thf(f137,plain,
! [X2: $i,X1: $i] :
( ( sF4 = $false )
| ( $true
= ( ^ [Y0: $i] :
( ( in @ X1 @ ( powerset @ Y0 ) )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ ( powerset @ Y0 ) )
=> ( in @ ( binunion @ X1 @ Y1 ) @ ( powerset @ Y0 ) ) ) ) )
@ X2 ) ) ),
inference(pi_proxy_clausification,[],[f136]) ).
thf(f138,plain,
! [X2: $i,X1: $i] :
( ( $true
= ( ( in @ X1 @ ( powerset @ X2 ) )
=> ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ ( powerset @ X2 ) )
=> ( in @ ( binunion @ X1 @ Y0 ) @ ( powerset @ X2 ) ) ) ) ) )
| ( sF4 = $false ) ),
inference(beta-eta_normalization,[],[f137]) ).
thf(f139,plain,
! [X2: $i,X1: $i] :
( ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ ( powerset @ X2 ) )
=> ( in @ ( binunion @ X1 @ Y0 ) @ ( powerset @ X2 ) ) ) ) )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( sF4 = $false ) ),
inference(imp_proxy_clausification,[],[f138]) ).
thf(f140,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( ( ^ [Y0: $i] :
( ( in @ Y0 @ ( powerset @ X2 ) )
=> ( in @ ( binunion @ X1 @ Y0 ) @ ( powerset @ X2 ) ) )
@ X3 )
= $true )
| ( sF4 = $false ) ),
inference(pi_proxy_clausification,[],[f139]) ).
thf(f141,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( sF4 = $false )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $true
= ( ( in @ X3 @ ( powerset @ X2 ) )
=> ( in @ ( binunion @ X1 @ X3 ) @ ( powerset @ X2 ) ) ) ) ),
inference(beta-eta_normalization,[],[f140]) ).
thf(f142,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( in @ ( binunion @ X1 @ X3 ) @ ( powerset @ X2 ) )
= $true )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( sF4 = $false )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false ) ),
inference(imp_proxy_clausification,[],[f141]) ).
thf(f144,plain,
( ( $false = sF15 )
| ( $true
= ( in @ sK1 @ sF6 ) ) ),
inference(iff_proxy_clausification,[],[f61]) ).
thf(f145,plain,
( ( ( in @ sK2 @ sF6 )
= $true )
| ( sF7 = $false ) ),
inference(iff_proxy_clausification,[],[f46]) ).
thf(f148,plain,
( ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y1 )
=> ( ( in @ Y4 @ ( binintersect @ Y0 @ Y2 ) )
=> ( in @ Y4 @ ( binintersect @ ( binunion @ Y0 @ Y3 ) @ ( binunion @ Y2 @ Y3 ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ( sF17 = $false ) ),
inference(iff_proxy_clausification,[],[f66]) ).
thf(f149,plain,
! [X1: $i] :
( ( $true
= ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y0 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ ( powerset @ Y1 ) )
=> ( !! @ $i
@ ^ [Y4: $i] :
( ( in @ Y4 @ Y1 )
=> ( ( in @ Y4 @ ( binintersect @ Y0 @ Y2 ) )
=> ( in @ Y4 @ ( binintersect @ ( binunion @ Y0 @ Y3 ) @ ( binunion @ Y2 @ Y3 ) ) ) ) ) ) ) ) ) ) ) )
@ X1 ) )
| ( sF17 = $false ) ),
inference(pi_proxy_clausification,[],[f148]) ).
thf(f150,plain,
! [X1: $i] :
( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ X1 @ ( powerset @ Y0 ) )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ ( powerset @ Y0 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y0 ) )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y0 )
=> ( ( in @ Y3 @ ( binintersect @ X1 @ Y1 ) )
=> ( in @ Y3 @ ( binintersect @ ( binunion @ X1 @ Y2 ) @ ( binunion @ Y1 @ Y2 ) ) ) ) ) ) ) ) ) ) ) )
= $true )
| ( sF17 = $false ) ),
inference(beta-eta_normalization,[],[f149]) ).
thf(f151,plain,
! [X2: $i,X1: $i] :
( ( $true
= ( ^ [Y0: $i] :
( ( in @ X1 @ ( powerset @ Y0 ) )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ ( powerset @ Y0 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ ( powerset @ Y0 ) )
=> ( !! @ $i
@ ^ [Y3: $i] :
( ( in @ Y3 @ Y0 )
=> ( ( in @ Y3 @ ( binintersect @ X1 @ Y1 ) )
=> ( in @ Y3 @ ( binintersect @ ( binunion @ X1 @ Y2 ) @ ( binunion @ Y1 @ Y2 ) ) ) ) ) ) ) ) ) ) )
@ X2 ) )
| ( sF17 = $false ) ),
inference(pi_proxy_clausification,[],[f150]) ).
thf(f152,plain,
! [X2: $i,X1: $i] :
( ( ( ( in @ X1 @ ( powerset @ X2 ) )
=> ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ ( powerset @ X2 ) )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ ( powerset @ X2 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ X2 )
=> ( ( in @ Y2 @ ( binintersect @ X1 @ Y0 ) )
=> ( in @ Y2 @ ( binintersect @ ( binunion @ X1 @ Y1 ) @ ( binunion @ Y0 @ Y1 ) ) ) ) ) ) ) ) ) ) )
= $true )
| ( sF17 = $false ) ),
inference(beta-eta_normalization,[],[f151]) ).
thf(f153,plain,
! [X2: $i,X1: $i] :
( ( sF17 = $false )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ ( powerset @ X2 ) )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ ( powerset @ X2 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ X2 )
=> ( ( in @ Y2 @ ( binintersect @ X1 @ Y0 ) )
=> ( in @ Y2 @ ( binintersect @ ( binunion @ X1 @ Y1 ) @ ( binunion @ Y0 @ Y1 ) ) ) ) ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f152]) ).
thf(f154,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( sF17 = $false )
| ( $true
= ( ^ [Y0: $i] :
( ( in @ Y0 @ ( powerset @ X2 ) )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ ( powerset @ X2 ) )
=> ( !! @ $i
@ ^ [Y2: $i] :
( ( in @ Y2 @ X2 )
=> ( ( in @ Y2 @ ( binintersect @ X1 @ Y0 ) )
=> ( in @ Y2 @ ( binintersect @ ( binunion @ X1 @ Y1 ) @ ( binunion @ Y0 @ Y1 ) ) ) ) ) ) ) ) )
@ X3 ) )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false ) ),
inference(pi_proxy_clausification,[],[f153]) ).
thf(f155,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( sF17 = $false )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $true
= ( ( in @ X3 @ ( powerset @ X2 ) )
=> ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ ( powerset @ X2 ) )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ X2 )
=> ( ( in @ Y1 @ ( binintersect @ X1 @ X3 ) )
=> ( in @ Y1 @ ( binintersect @ ( binunion @ X1 @ Y0 ) @ ( binunion @ X3 @ Y0 ) ) ) ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f154]) ).
thf(f156,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ ( powerset @ X2 ) )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ X2 )
=> ( ( in @ Y1 @ ( binintersect @ X1 @ X3 ) )
=> ( in @ Y1 @ ( binintersect @ ( binunion @ X1 @ Y0 ) @ ( binunion @ X3 @ Y0 ) ) ) ) ) ) ) ) )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( sF17 = $false ) ),
inference(imp_proxy_clausification,[],[f155]) ).
thf(f157,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( sF17 = $false )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( ( ^ [Y0: $i] :
( ( in @ Y0 @ ( powerset @ X2 ) )
=> ( !! @ $i
@ ^ [Y1: $i] :
( ( in @ Y1 @ X2 )
=> ( ( in @ Y1 @ ( binintersect @ X1 @ X3 ) )
=> ( in @ Y1 @ ( binintersect @ ( binunion @ X1 @ Y0 ) @ ( binunion @ X3 @ Y0 ) ) ) ) ) ) )
@ X4 )
= $true ) ),
inference(pi_proxy_clausification,[],[f156]) ).
thf(f158,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( sF17 = $false )
| ( $true
= ( ( in @ X4 @ ( powerset @ X2 ) )
=> ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ X2 )
=> ( ( in @ Y0 @ ( binintersect @ X1 @ X3 ) )
=> ( in @ Y0 @ ( binintersect @ ( binunion @ X1 @ X4 ) @ ( binunion @ X3 @ X4 ) ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f157]) ).
thf(f159,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( sF17 = $false )
| ( ( in @ X4 @ ( powerset @ X2 ) )
= $false )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( in @ Y0 @ X2 )
=> ( ( in @ Y0 @ ( binintersect @ X1 @ X3 ) )
=> ( in @ Y0 @ ( binintersect @ ( binunion @ X1 @ X4 ) @ ( binunion @ X3 @ X4 ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f158]) ).
thf(f160,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i,X5: $i] :
( ( sF17 = $false )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( ( in @ X4 @ ( powerset @ X2 ) )
= $false )
| ( $true
= ( ^ [Y0: $i] :
( ( in @ Y0 @ X2 )
=> ( ( in @ Y0 @ ( binintersect @ X1 @ X3 ) )
=> ( in @ Y0 @ ( binintersect @ ( binunion @ X1 @ X4 ) @ ( binunion @ X3 @ X4 ) ) ) ) )
@ X5 ) )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false ) ),
inference(pi_proxy_clausification,[],[f159]) ).
thf(f161,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i,X5: $i] :
( ( $true
= ( ( in @ X5 @ X2 )
=> ( ( in @ X5 @ ( binintersect @ X1 @ X3 ) )
=> ( in @ X5 @ ( binintersect @ ( binunion @ X1 @ X4 ) @ ( binunion @ X3 @ X4 ) ) ) ) ) )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( sF17 = $false )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( ( in @ X4 @ ( powerset @ X2 ) )
= $false ) ),
inference(beta-eta_normalization,[],[f160]) ).
thf(f162,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i,X5: $i] :
( ( $false
= ( in @ X5 @ X2 ) )
| ( ( in @ X4 @ ( powerset @ X2 ) )
= $false )
| ( ( ( in @ X5 @ ( binintersect @ X1 @ X3 ) )
=> ( in @ X5 @ ( binintersect @ ( binunion @ X1 @ X4 ) @ ( binunion @ X3 @ X4 ) ) ) )
= $true )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( sF17 = $false )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) ) ),
inference(imp_proxy_clausification,[],[f161]) ).
thf(f163,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i,X5: $i] :
( ( $false
= ( in @ X5 @ X2 ) )
| ( ( in @ X5 @ ( binintersect @ X1 @ X3 ) )
= $false )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( ( in @ X4 @ ( powerset @ X2 ) )
= $false )
| ( ( in @ X5 @ ( binintersect @ ( binunion @ X1 @ X4 ) @ ( binunion @ X3 @ X4 ) ) )
= $true )
| ( sF17 = $false )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false ) ),
inference(imp_proxy_clausification,[],[f162]) ).
thf(f184,plain,
( ( $false = sF14 )
| ( ( in @ sK3 @ sF6 )
= $true ) ),
inference(iff_proxy_clausification,[],[f59]) ).
thf(f187,definition,
( spl33_1
<=> ! [X2: $i,X1: $i,X3: $i] :
( ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( $true
= ( in @ ( sK18 @ X3 @ X1 @ X2 ) @ X2 ) )
| ( $true
= ( in @ X1 @ ( powerset @ X3 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl33_1])],[avatar_definition]) ).
thf(f188,plain,
( ! [X2: $i,X3: $i,X1: $i] :
( ( $true
= ( in @ ( sK18 @ X3 @ X1 @ X2 ) @ X2 ) )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $true
= ( in @ X1 @ ( powerset @ X3 ) ) )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) ) )
| ~ spl33_1 ),
inference(avatar_component_clause,[],[f187]) ).
thf(f190,definition,
( spl33_2
<=> ( $false = sF5 ) ),
introduced(definition,[new_symbols(definition,[spl33_2])],[avatar_definition]) ).
thf(f192,plain,
( ( $false = sF5 )
| ~ spl33_2 ),
inference(avatar_component_clause,[],[f190]) ).
thf(f193,plain,
( spl33_1
| spl33_2 ),
inference(avatar_split_clause,[],[f82,f190,f187]) ).
thf(f195,definition,
( spl33_3
<=> ! [X2: $i,X1: $i,X3: $i] :
( ( ( in @ ( sK18 @ X3 @ X1 @ X2 ) @ X1 )
= $true )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( $true
= ( in @ X1 @ ( powerset @ X3 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl33_3])],[avatar_definition]) ).
thf(f196,plain,
( ! [X2: $i,X3: $i,X1: $i] :
( ( ( in @ ( sK18 @ X3 @ X1 @ X2 ) @ X1 )
= $true )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $true
= ( in @ X1 @ ( powerset @ X3 ) ) ) )
| ~ spl33_3 ),
inference(avatar_component_clause,[],[f195]) ).
thf(f197,plain,
( spl33_3
| spl33_2 ),
inference(avatar_split_clause,[],[f84,f190,f195]) ).
thf(f199,definition,
( spl33_4
<=> ! [X2: $i,X1: $i,X3: $i] :
( ( $true
= ( in @ X1 @ ( powerset @ X3 ) ) )
| ( ( in @ ( sK18 @ X3 @ X1 @ X2 ) @ X3 )
= $false )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl33_4])],[avatar_definition]) ).
thf(f200,plain,
( ! [X2: $i,X3: $i,X1: $i] :
( ( ( in @ ( sK18 @ X3 @ X1 @ X2 ) @ X3 )
= $false )
| ( $true
= ( in @ X1 @ ( powerset @ X3 ) ) )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) ) )
| ~ spl33_4 ),
inference(avatar_component_clause,[],[f199]) ).
thf(f201,plain,
( spl33_2
| spl33_4 ),
inference(avatar_split_clause,[],[f83,f199,f190]) ).
thf(f203,definition,
( spl33_5
<=> ( $true = sF5 ) ),
introduced(definition,[new_symbols(definition,[spl33_5])],[avatar_definition]) ).
thf(f205,plain,
( ( $true = sF5 )
| ~ spl33_5 ),
inference(avatar_component_clause,[],[f203]) ).
thf(f226,definition,
( spl33_10
<=> ( $true = sF16 ) ),
introduced(definition,[new_symbols(definition,[spl33_10])],[avatar_definition]) ).
thf(f228,plain,
( ( $true = sF16 )
| ~ spl33_10 ),
inference(avatar_component_clause,[],[f226]) ).
thf(f245,definition,
( spl33_14
<=> ( $false = sF16 ) ),
introduced(definition,[new_symbols(definition,[spl33_14])],[avatar_definition]) ).
thf(f247,plain,
( ( $false = sF16 )
| ~ spl33_14 ),
inference(avatar_component_clause,[],[f245]) ).
thf(f249,definition,
( spl33_15
<=> ! [X2: $i,X1: $i,X3: $i] :
( ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( $true
= ( in @ ( binintersect @ X1 @ X3 ) @ ( powerset @ X2 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl33_15])],[avatar_definition]) ).
thf(f250,plain,
( ! [X2: $i,X3: $i,X1: $i] :
( ( $true
= ( in @ ( binintersect @ X1 @ X3 ) @ ( powerset @ X2 ) ) )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false ) )
| ~ spl33_15 ),
inference(avatar_component_clause,[],[f249]) ).
thf(f251,plain,
( spl33_14
| spl33_15 ),
inference(avatar_split_clause,[],[f120,f249,f245]) ).
thf(f252,plain,
spl33_5,
inference(avatar_split_clause,[],[f43,f203]) ).
thf(f263,definition,
( spl33_18
<=> ( $true = sF13 ) ),
introduced(definition,[new_symbols(definition,[spl33_18])],[avatar_definition]) ).
thf(f267,definition,
( spl33_19
<=> ( $false
= ( in @ sF8 @ sF12 ) ) ),
introduced(definition,[new_symbols(definition,[spl33_19])],[avatar_definition]) ).
thf(f269,plain,
( ( $false
= ( in @ sF8 @ sF12 ) )
| ~ spl33_19 ),
inference(avatar_component_clause,[],[f267]) ).
thf(f270,plain,
( spl33_18
| spl33_19 ),
inference(avatar_split_clause,[],[f121,f267,f263]) ).
thf(f272,definition,
( spl33_20
<=> ( $true = sF4 ) ),
introduced(definition,[new_symbols(definition,[spl33_20])],[avatar_definition]) ).
thf(f274,plain,
( ( $true = sF4 )
| ~ spl33_20 ),
inference(avatar_component_clause,[],[f272]) ).
thf(f291,definition,
( spl33_24
<=> ( sF4 = $false ) ),
introduced(definition,[new_symbols(definition,[spl33_24])],[avatar_definition]) ).
thf(f293,plain,
( ( sF4 = $false )
| ~ spl33_24 ),
inference(avatar_component_clause,[],[f291]) ).
thf(f295,definition,
( spl33_25
<=> ! [X2: $i,X1: $i,X3: $i] :
( ( ( in @ ( binunion @ X1 @ X3 ) @ ( powerset @ X2 ) )
= $true )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl33_25])],[avatar_definition]) ).
thf(f296,plain,
( ! [X2: $i,X3: $i,X1: $i] :
( ( ( in @ ( binunion @ X1 @ X3 ) @ ( powerset @ X2 ) )
= $true )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) ) )
| ~ spl33_25 ),
inference(avatar_component_clause,[],[f295]) ).
thf(f297,plain,
( spl33_24
| spl33_25 ),
inference(avatar_split_clause,[],[f142,f295,f291]) ).
thf(f299,definition,
( spl33_26
<=> ( $false = sF15 ) ),
introduced(definition,[new_symbols(definition,[spl33_26])],[avatar_definition]) ).
thf(f301,plain,
( ( $false = sF15 )
| ~ spl33_26 ),
inference(avatar_component_clause,[],[f299]) ).
thf(f303,definition,
( spl33_27
<=> ( $true
= ( in @ sK1 @ sF6 ) ) ),
introduced(definition,[new_symbols(definition,[spl33_27])],[avatar_definition]) ).
thf(f305,plain,
( ( $true
= ( in @ sK1 @ sF6 ) )
| ~ spl33_27 ),
inference(avatar_component_clause,[],[f303]) ).
thf(f306,plain,
( spl33_26
| spl33_27 ),
inference(avatar_split_clause,[],[f144,f303,f299]) ).
thf(f312,definition,
( spl33_29
<=> ( $true = sF15 ) ),
introduced(definition,[new_symbols(definition,[spl33_29])],[avatar_definition]) ).
thf(f314,plain,
( ( $true = sF15 )
| ~ spl33_29 ),
inference(avatar_component_clause,[],[f312]) ).
thf(f317,definition,
( spl33_30
<=> ( ( in @ sK2 @ sF6 )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl33_30])],[avatar_definition]) ).
thf(f318,plain,
( ( ( in @ sK2 @ sF6 )
!= $false )
| spl33_30 ),
inference(avatar_component_clause,[],[f317]) ).
thf(f319,plain,
( ( ( in @ sK2 @ sF6 )
= $false )
| ~ spl33_30 ),
inference(avatar_component_clause,[],[f317]) ).
thf(f321,definition,
( spl33_31
<=> ( sF7 = $true ) ),
introduced(definition,[new_symbols(definition,[spl33_31])],[avatar_definition]) ).
thf(f323,plain,
( ( sF7 = $true )
| ~ spl33_31 ),
inference(avatar_component_clause,[],[f321]) ).
thf(f326,definition,
( spl33_32
<=> ( ( in @ sK2 @ sF6 )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl33_32])],[avatar_definition]) ).
thf(f328,plain,
( ( ( in @ sK2 @ sF6 )
= $true )
| ~ spl33_32 ),
inference(avatar_component_clause,[],[f326]) ).
thf(f330,definition,
( spl33_33
<=> ( sF7 = $false ) ),
introduced(definition,[new_symbols(definition,[spl33_33])],[avatar_definition]) ).
thf(f332,plain,
( ( sF7 = $false )
| ~ spl33_33 ),
inference(avatar_component_clause,[],[f330]) ).
thf(f333,plain,
( spl33_32
| spl33_33 ),
inference(avatar_split_clause,[],[f145,f330,f326]) ).
thf(f334,plain,
spl33_20,
inference(avatar_split_clause,[],[f41,f272]) ).
thf(f336,definition,
( spl33_34
<=> ( sF17 = $false ) ),
introduced(definition,[new_symbols(definition,[spl33_34])],[avatar_definition]) ).
thf(f338,plain,
( ( sF17 = $false )
| ~ spl33_34 ),
inference(avatar_component_clause,[],[f336]) ).
thf(f340,definition,
( spl33_35
<=> ! [X3: $i,X4: $i,X5: $i,X2: $i,X1: $i] :
( ( $false
= ( in @ X5 @ X2 ) )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( ( in @ X5 @ ( binintersect @ ( binunion @ X1 @ X4 ) @ ( binunion @ X3 @ X4 ) ) )
= $true )
| ( ( in @ X4 @ ( powerset @ X2 ) )
= $false )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( ( in @ X5 @ ( binintersect @ X1 @ X3 ) )
= $false ) ) ),
introduced(definition,[new_symbols(definition,[spl33_35])],[avatar_definition]) ).
thf(f341,plain,
( ! [X2: $i,X3: $i,X1: $i,X4: $i,X5: $i] :
( ( ( in @ X5 @ ( binintersect @ ( binunion @ X1 @ X4 ) @ ( binunion @ X3 @ X4 ) ) )
= $true )
| ( $false
= ( in @ X3 @ ( powerset @ X2 ) ) )
| ( ( in @ X4 @ ( powerset @ X2 ) )
= $false )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $false
= ( in @ X5 @ X2 ) )
| ( ( in @ X5 @ ( binintersect @ X1 @ X3 ) )
= $false ) )
| ~ spl33_35 ),
inference(avatar_component_clause,[],[f340]) ).
thf(f342,plain,
( spl33_34
| spl33_35 ),
inference(avatar_split_clause,[],[f163,f340,f336]) ).
thf(f348,definition,
( spl33_37
<=> ( $true = sF17 ) ),
introduced(definition,[new_symbols(definition,[spl33_37])],[avatar_definition]) ).
thf(f350,plain,
( ( $true = sF17 )
| ~ spl33_37 ),
inference(avatar_component_clause,[],[f348]) ).
thf(f377,plain,
spl33_37,
inference(avatar_split_clause,[],[f67,f348]) ).
thf(f378,plain,
~ spl33_18,
inference(avatar_split_clause,[],[f57,f263]) ).
thf(f379,plain,
spl33_31,
inference(avatar_split_clause,[],[f47,f321]) ).
thf(f380,plain,
spl33_10,
inference(avatar_split_clause,[],[f65,f226]) ).
thf(f381,plain,
( ( ( in @ sK3 @ sF6 )
= $true )
| ( $true = $false ) ),
inference(forward_demodulation,[],[f184,f60]) ).
thf(f382,plain,
( ( in @ sK3 @ sF6 )
= $true ),
inference(trivial_inequality_removal,[],[f381]) ).
thf(f383,plain,
spl33_29,
inference(avatar_split_clause,[],[f62,f312]) ).
thf(f384,plain,
( ( $true = $false )
| ~ spl33_20
| ~ spl33_24 ),
inference(forward_demodulation,[],[f274,f293]) ).
thf(f385,plain,
( $false
| ~ spl33_20
| ~ spl33_24 ),
inference(trivial_inequality_removal,[],[f384]) ).
thf(f386,plain,
( ~ spl33_20
| ~ spl33_24 ),
inference(avatar_contradiction_clause,[],[f385]) ).
thf(f387,plain,
( ( $true = $false )
| ~ spl33_26
| ~ spl33_29 ),
inference(forward_demodulation,[],[f314,f301]) ).
thf(f388,plain,
( $false
| ~ spl33_26
| ~ spl33_29 ),
inference(trivial_inequality_removal,[],[f387]) ).
thf(f389,plain,
( ~ spl33_26
| ~ spl33_29 ),
inference(avatar_contradiction_clause,[],[f388]) ).
thf(f390,plain,
( ( $true = $false )
| ~ spl33_10
| ~ spl33_14 ),
inference(forward_demodulation,[],[f228,f247]) ).
thf(f391,plain,
( $false
| ~ spl33_10
| ~ spl33_14 ),
inference(trivial_inequality_removal,[],[f390]) ).
thf(f392,plain,
( ~ spl33_10
| ~ spl33_14 ),
inference(avatar_contradiction_clause,[],[f391]) ).
thf(f414,plain,
( ( $true = $false )
| ~ spl33_2
| ~ spl33_5 ),
inference(constrained_superposition,[],[f205,f192]) ).
thf(f418,plain,
( $false
| ~ spl33_2
| ~ spl33_5 ),
inference(trivial_inequality_removal,[],[f414]) ).
thf(f419,plain,
( ~ spl33_2
| ~ spl33_5 ),
inference(avatar_contradiction_clause,[],[f418]) ).
thf(f431,plain,
( ( $true = $false )
| ~ spl33_34
| ~ spl33_37 ),
inference(constrained_superposition,[],[f338,f350]) ).
thf(f434,plain,
( $false
| ~ spl33_34
| ~ spl33_37 ),
inference(trivial_inequality_removal,[],[f431]) ).
thf(f435,plain,
( ~ spl33_34
| ~ spl33_37 ),
inference(avatar_contradiction_clause,[],[f434]) ).
thf(f437,plain,
( ! [X0: $i,X1: $i] :
( ( $true
= ( in @ ( binintersect @ X0 @ X1 ) @ sF6 ) )
| ( $false
= ( in @ X0 @ sF6 ) )
| ( $false
= ( in @ X1 @ sF6 ) ) )
| ~ spl33_15 ),
inference(constrained_superposition,[],[f250,f44]) ).
thf(f440,plain,
( ! [X0: $i] :
( ( ( in @ sF10 @ ( powerset @ X0 ) )
= $false )
| ( ( in @ sF9 @ ( powerset @ X0 ) )
= $false )
| ( ( in @ sF11 @ ( powerset @ X0 ) )
= $true ) )
| ~ spl33_15 ),
inference(constrained_superposition,[],[f250,f54]) ).
thf(f441,plain,
( ( ( in @ sK2 @ sF6 )
= $false )
| ( $true
= ( in @ sF8 @ sF6 ) )
| ( $false
= ( in @ sK1 @ sF6 ) )
| ~ spl33_15 ),
inference(constrained_superposition,[],[f437,f49]) ).
thf(f444,definition,
( spl33_43
<=> ( $true
= ( in @ sF11 @ sF6 ) ) ),
introduced(definition,[new_symbols(definition,[spl33_43])],[avatar_definition]) ).
thf(f445,plain,
( ( $true
!= ( in @ sF11 @ sF6 ) )
| spl33_43 ),
inference(avatar_component_clause,[],[f444]) ).
thf(f446,plain,
( ( $true
= ( in @ sF11 @ sF6 ) )
| ~ spl33_43 ),
inference(avatar_component_clause,[],[f444]) ).
thf(f448,definition,
( spl33_44
<=> ( $false
= ( in @ sF10 @ sF6 ) ) ),
introduced(definition,[new_symbols(definition,[spl33_44])],[avatar_definition]) ).
thf(f450,plain,
( ( $false
= ( in @ sF10 @ sF6 ) )
| ~ spl33_44 ),
inference(avatar_component_clause,[],[f448]) ).
thf(f456,plain,
( ( $false
= ( in @ sK1 @ sF6 ) )
| ( $true
= ( in @ sF8 @ sF6 ) )
| ( $true = $false )
| ~ spl33_15
| ~ spl33_32 ),
inference(forward_demodulation,[],[f441,f328]) ).
thf(f457,plain,
( ( $false
= ( in @ sK1 @ sF6 ) )
| ( $true
= ( in @ sF8 @ sF6 ) )
| ~ spl33_15
| ~ spl33_32 ),
inference(trivial_inequality_removal,[],[f456]) ).
thf(f458,plain,
( ( $true = $false )
| ( $true
= ( in @ sF8 @ sF6 ) )
| ~ spl33_15
| ~ spl33_27
| ~ spl33_32 ),
inference(forward_demodulation,[],[f457,f305]) ).
thf(f460,plain,
( ! [X0: $i,X1: $i] :
( ( $true
= ( in @ ( binunion @ X0 @ X1 ) @ sF6 ) )
| ( $false
= ( in @ X1 @ sF6 ) )
| ( $false
= ( in @ X0 @ sF6 ) ) )
| ~ spl33_25 ),
inference(constrained_superposition,[],[f296,f44]) ).
thf(f465,plain,
( ! [X2: $i,X0: $i,X1: $i] :
( ( $true
= ( in @ X0 @ ( binintersect @ ( binunion @ X1 @ sK3 ) @ sF10 ) ) )
| ( ( in @ sK3 @ ( powerset @ X2 ) )
= $false )
| ( ( in @ X1 @ ( powerset @ X2 ) )
= $false )
| ( $false
= ( in @ X0 @ X2 ) )
| ( ( in @ sK2 @ ( powerset @ X2 ) )
= $false )
| ( ( in @ X0 @ ( binintersect @ X1 @ sK2 ) )
= $false ) )
| ~ spl33_35 ),
inference(constrained_superposition,[],[f341,f53]) ).
thf(f551,plain,
( ( $false
= ( in @ sK1 @ sF6 ) )
| ( ( in @ sK3 @ sF6 )
= $false )
| ( ( in @ sF9 @ sF6 )
= $true )
| ~ spl33_25 ),
inference(constrained_superposition,[],[f460,f51]) ).
thf(f552,plain,
( ( $true
= ( in @ sF10 @ sF6 ) )
| ( ( in @ sK3 @ sF6 )
= $false )
| ( ( in @ sK2 @ sF6 )
= $false )
| ~ spl33_25 ),
inference(constrained_superposition,[],[f460,f53]) ).
thf(f553,plain,
( ( $true
= ( in @ sF10 @ sF6 ) )
| ( $true = $false )
| ( ( in @ sK2 @ sF6 )
= $false )
| ~ spl33_25 ),
inference(forward_demodulation,[],[f552,f382]) ).
thf(f554,plain,
( ( ( in @ sK2 @ sF6 )
= $false )
| ( $true
= ( in @ sF10 @ sF6 ) )
| ~ spl33_25 ),
inference(trivial_inequality_removal,[],[f553]) ).
thf(f555,plain,
( ( $true = $false )
| ( ( in @ sK3 @ sF6 )
= $false )
| ( ( in @ sF9 @ sF6 )
= $true )
| ~ spl33_25
| ~ spl33_27 ),
inference(forward_demodulation,[],[f551,f305]) ).
thf(f556,plain,
( ( ( in @ sK3 @ sF6 )
= $false )
| ( ( in @ sF9 @ sF6 )
= $true )
| ~ spl33_25
| ~ spl33_27 ),
inference(trivial_inequality_removal,[],[f555]) ).
thf(f557,plain,
( ( $true
= ( in @ sF10 @ sF6 ) )
| ( $true = $false )
| ~ spl33_25
| ~ spl33_32 ),
inference(forward_demodulation,[],[f554,f328]) ).
thf(f558,plain,
( ( $true
= ( in @ sF10 @ sF6 ) )
| ~ spl33_25
| ~ spl33_32 ),
inference(trivial_inequality_removal,[],[f557]) ).
thf(f559,plain,
( ( $true = $false )
| ( ( in @ sF9 @ sF6 )
= $true )
| ~ spl33_25
| ~ spl33_27 ),
inference(forward_demodulation,[],[f556,f382]) ).
thf(f560,plain,
( ( ( in @ sF9 @ sF6 )
= $true )
| ~ spl33_25
| ~ spl33_27 ),
inference(trivial_inequality_removal,[],[f559]) ).
thf(f578,plain,
( ( ( in @ sF9 @ sF6 )
= $false )
| ( $true
= ( in @ sF11 @ sF6 ) )
| ( $false
= ( in @ sF10 @ sF6 ) )
| ~ spl33_15 ),
inference(constrained_superposition,[],[f440,f44]) ).
thf(f1033,plain,
( ! [X0: $i,X1: $i] :
( ( $false
= ( in @ sK3 @ ( powerset @ X1 ) ) )
| ( $false
= ( in @ X0 @ ( binintersect @ sK1 @ sK2 ) ) )
| ( $true
= ( in @ X0 @ ( binintersect @ sF9 @ sF10 ) ) )
| ( $false
= ( in @ sK1 @ ( powerset @ X1 ) ) )
| ( $false
= ( in @ X0 @ X1 ) )
| ( ( in @ sK2 @ ( powerset @ X1 ) )
= $false ) )
| ~ spl33_35 ),
inference(constrained_superposition,[],[f465,f51]) ).
thf(f1123,plain,
( ! [X0: $i,X1: $i] :
( ( $true
= ( in @ X0 @ ( binintersect @ sF9 @ sF10 ) ) )
| ( $false
= ( in @ sK1 @ ( powerset @ X1 ) ) )
| ( $false
= ( in @ X0 @ X1 ) )
| ( ( in @ sK2 @ ( powerset @ X1 ) )
= $false )
| ( $false
= ( in @ sK3 @ ( powerset @ X1 ) ) )
| ( $false
= ( in @ X0 @ sF8 ) ) )
| ~ spl33_35 ),
inference(forward_demodulation,[],[f1033,f49]) ).
thf(f1124,plain,
( ! [X0: $i,X1: $i] :
( ( $false
= ( in @ sK1 @ ( powerset @ X1 ) ) )
| ( $false
= ( in @ X0 @ sF8 ) )
| ( $false
= ( in @ X0 @ X1 ) )
| ( $false
= ( in @ sK3 @ ( powerset @ X1 ) ) )
| ( $true
= ( in @ X0 @ sF11 ) )
| ( ( in @ sK2 @ ( powerset @ X1 ) )
= $false ) )
| ~ spl33_35 ),
inference(forward_demodulation,[],[f1123,f54]) ).
thf(f2522,definition,
( spl33_70
<=> ( $true
= ( in @ sF10 @ sF6 ) ) ),
introduced(definition,[new_symbols(definition,[spl33_70])],[avatar_definition]) ).
thf(f2524,plain,
( ( $true
= ( in @ sF10 @ sF6 ) )
| ~ spl33_70 ),
inference(avatar_component_clause,[],[f2522]) ).
thf(f2533,definition,
( spl33_71
<=> ( $true
= ( in @ sF8 @ sF6 ) ) ),
introduced(definition,[new_symbols(definition,[spl33_71])],[avatar_definition]) ).
thf(f2535,plain,
( ( $true
= ( in @ sF8 @ sF6 ) )
| ~ spl33_71 ),
inference(avatar_component_clause,[],[f2533]) ).
thf(f2542,plain,
( ( $true = $false )
| ~ spl33_31
| ~ spl33_33 ),
inference(constrained_superposition,[],[f323,f332]) ).
thf(f2546,plain,
( $false
| ~ spl33_31
| ~ spl33_33 ),
inference(trivial_inequality_removal,[],[f2542]) ).
thf(f2547,plain,
( ~ spl33_31
| ~ spl33_33 ),
inference(avatar_contradiction_clause,[],[f2546]) ).
thf(f2548,plain,
( ( $true
= ( in @ sF8 @ sF6 ) )
| ~ spl33_15
| ~ spl33_27
| ~ spl33_32 ),
inference(trivial_inequality_removal,[],[f458]) ).
thf(f2552,plain,
( spl33_70
| ~ spl33_25
| ~ spl33_32 ),
inference(avatar_split_clause,[],[f558,f326,f295,f2522]) ).
thf(f2553,plain,
( spl33_71
| ~ spl33_15
| ~ spl33_27
| ~ spl33_32 ),
inference(avatar_split_clause,[],[f2548,f326,f303,f249,f2533]) ).
thf(f2558,plain,
( ( $true = $false )
| ~ spl33_30
| ~ spl33_32 ),
inference(forward_demodulation,[],[f328,f319]) ).
thf(f2559,plain,
( $false
| ~ spl33_30
| ~ spl33_32 ),
inference(trivial_inequality_removal,[],[f2558]) ).
thf(f2560,plain,
( ~ spl33_30
| ~ spl33_32 ),
inference(avatar_contradiction_clause,[],[f2559]) ).
thf(f3458,plain,
( ! [X0: $i] :
( ( $true
= ( in @ X0 @ sF11 ) )
| ( $false
= ( in @ X0 @ sF8 ) )
| ( ( in @ X0 @ sK0 )
= $false )
| ( ( in @ sK3 @ sF6 )
= $false )
| ( $false
= ( in @ sK1 @ sF6 ) )
| ( ( in @ sK2 @ sF6 )
= $false ) )
| ~ spl33_35 ),
inference(constrained_superposition,[],[f1124,f44]) ).
thf(f3590,plain,
( ! [X0: $i] :
( ( ( in @ X0 @ sK0 )
= $false )
| ( $true
= ( in @ X0 @ sF11 ) )
| ( $false
= ( in @ sK1 @ sF6 ) )
| ( $false
= ( in @ X0 @ sF8 ) )
| ( ( in @ sK3 @ sF6 )
= $false ) )
| spl33_30
| ~ spl33_35 ),
inference(forward_subsumption_resolution,[],[f3458,f318]) ).
thf(f3608,plain,
( ! [X0: $i] :
( ( $true = $false )
| ( ( in @ sK3 @ sF6 )
= $false )
| ( $true
= ( in @ X0 @ sF11 ) )
| ( $false
= ( in @ X0 @ sF8 ) )
| ( ( in @ X0 @ sK0 )
= $false ) )
| ~ spl33_27
| spl33_30
| ~ spl33_35 ),
inference(forward_demodulation,[],[f3590,f305]) ).
thf(f3609,plain,
( ! [X0: $i] :
( ( ( in @ sK3 @ sF6 )
= $false )
| ( $true
= ( in @ X0 @ sF11 ) )
| ( $false
= ( in @ X0 @ sF8 ) )
| ( ( in @ X0 @ sK0 )
= $false ) )
| ~ spl33_27
| spl33_30
| ~ spl33_35 ),
inference(trivial_inequality_removal,[],[f3608]) ).
thf(f3610,plain,
( ! [X0: $i] :
( ( ( in @ X0 @ sK0 )
= $false )
| ( $false
= ( in @ X0 @ sF8 ) )
| ( $true
= ( in @ X0 @ sF11 ) )
| ( $true = $false ) )
| ~ spl33_27
| spl33_30
| ~ spl33_35 ),
inference(forward_demodulation,[],[f3609,f382]) ).
thf(f3611,plain,
( ! [X0: $i] :
( ( ( in @ X0 @ sK0 )
= $false )
| ( $false
= ( in @ X0 @ sF8 ) )
| ( $true
= ( in @ X0 @ sF11 ) ) )
| ~ spl33_27
| spl33_30
| ~ spl33_35 ),
inference(trivial_inequality_removal,[],[f3610]) ).
thf(f3615,plain,
( ! [X0: $i,X1: $i] :
( ( ( in @ X1 @ ( powerset @ sK0 ) )
= $false )
| ( $true = $false )
| ( $true
= ( in @ ( sK18 @ X0 @ X1 @ sK0 ) @ sF11 ) )
| ( $false
= ( in @ ( sK18 @ X0 @ X1 @ sK0 ) @ sF8 ) )
| ( ( in @ X1 @ ( powerset @ X0 ) )
= $true )
| ( ( in @ X0 @ ( powerset @ sK0 ) )
= $false ) )
| ~ spl33_1
| ~ spl33_27
| spl33_30
| ~ spl33_35 ),
inference(constrained_superposition,[],[f188,f3611]) ).
thf(f3617,plain,
( ! [X0: $i,X1: $i] :
( ( ( in @ X1 @ ( powerset @ X0 ) )
= $true )
| ( $false
= ( in @ ( sK18 @ X0 @ X1 @ sK0 ) @ sF8 ) )
| ( $true
= ( in @ ( sK18 @ X0 @ X1 @ sK0 ) @ sF11 ) )
| ( ( in @ X0 @ ( powerset @ sK0 ) )
= $false )
| ( ( in @ X1 @ ( powerset @ sK0 ) )
= $false ) )
| ~ spl33_1
| ~ spl33_27
| spl33_30
| ~ spl33_35 ),
inference(trivial_inequality_removal,[],[f3615]) ).
thf(f3622,plain,
( ! [X0: $i,X1: $i] :
( ( $true
= ( in @ ( sK18 @ X0 @ X1 @ sK0 ) @ sF11 ) )
| ( $false
= ( in @ ( sK18 @ X0 @ X1 @ sK0 ) @ sF8 ) )
| ( $false
= ( in @ X0 @ sF6 ) )
| ( ( in @ X1 @ ( powerset @ sK0 ) )
= $false )
| ( ( in @ X1 @ ( powerset @ X0 ) )
= $true ) )
| ~ spl33_1
| ~ spl33_27
| spl33_30
| ~ spl33_35 ),
inference(forward_demodulation,[],[f3617,f44]) ).
thf(f3624,plain,
( ! [X0: $i,X1: $i] :
( ( $false
= ( in @ ( sK18 @ X0 @ X1 @ sK0 ) @ sF8 ) )
| ( ( in @ X1 @ ( powerset @ X0 ) )
= $true )
| ( $false
= ( in @ X1 @ sF6 ) )
| ( $false
= ( in @ X0 @ sF6 ) )
| ( $true
= ( in @ ( sK18 @ X0 @ X1 @ sK0 ) @ sF11 ) ) )
| ~ spl33_1
| ~ spl33_27
| spl33_30
| ~ spl33_35 ),
inference(forward_demodulation,[],[f3622,f44]) ).
thf(f3758,plain,
( ! [X0: $i] :
( ( $true = $false )
| ( ( in @ X0 @ ( powerset @ sK0 ) )
= $false )
| ( $false
= ( in @ X0 @ sF6 ) )
| ( $true
= ( in @ sF8 @ ( powerset @ X0 ) ) )
| ( $true
= ( in @ ( sK18 @ X0 @ sF8 @ sK0 ) @ sF11 ) )
| ( $false
= ( in @ sF8 @ ( powerset @ sK0 ) ) )
| ( $false
= ( in @ sF8 @ sF6 ) )
| ( $true
= ( in @ sF8 @ ( powerset @ X0 ) ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_27
| spl33_30
| ~ spl33_35 ),
inference(constrained_superposition,[],[f3624,f196]) ).
thf(f3760,plain,
( ! [X0: $i] :
( ( $true
= ( in @ ( sK18 @ X0 @ sF8 @ sK0 ) @ sF11 ) )
| ( $false
= ( in @ sF8 @ sF6 ) )
| ( $true = $false )
| ( $false
= ( in @ X0 @ sF6 ) )
| ( $true
= ( in @ sF8 @ ( powerset @ X0 ) ) )
| ( $false
= ( in @ sF8 @ ( powerset @ sK0 ) ) )
| ( ( in @ X0 @ ( powerset @ sK0 ) )
= $false ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_27
| spl33_30
| ~ spl33_35 ),
inference(duplicate_literal_removal,[],[f3758]) ).
thf(f3761,plain,
( ! [X0: $i] :
( ( $false
= ( in @ X0 @ sF6 ) )
| ( $false
= ( in @ sF8 @ sF6 ) )
| ( ( in @ X0 @ ( powerset @ sK0 ) )
= $false )
| ( $true
= ( in @ ( sK18 @ X0 @ sF8 @ sK0 ) @ sF11 ) )
| ( $false
= ( in @ sF8 @ ( powerset @ sK0 ) ) )
| ( $true
= ( in @ sF8 @ ( powerset @ X0 ) ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_27
| spl33_30
| ~ spl33_35 ),
inference(trivial_inequality_removal,[],[f3760]) ).
thf(f3765,plain,
( ! [X0: $i] :
( ( $true = $false )
| ( $true
= ( in @ ( sK18 @ X0 @ sF8 @ sK0 ) @ sF11 ) )
| ( $false
= ( in @ X0 @ sF6 ) )
| ( $false
= ( in @ sF8 @ ( powerset @ sK0 ) ) )
| ( $true
= ( in @ sF8 @ ( powerset @ X0 ) ) )
| ( ( in @ X0 @ ( powerset @ sK0 ) )
= $false ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_71 ),
inference(forward_demodulation,[],[f3761,f2535]) ).
thf(f3766,plain,
( ! [X0: $i] :
( ( $false
= ( in @ X0 @ sF6 ) )
| ( ( in @ X0 @ ( powerset @ sK0 ) )
= $false )
| ( $true
= ( in @ ( sK18 @ X0 @ sF8 @ sK0 ) @ sF11 ) )
| ( $true
= ( in @ sF8 @ ( powerset @ X0 ) ) )
| ( $false
= ( in @ sF8 @ ( powerset @ sK0 ) ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_71 ),
inference(trivial_inequality_removal,[],[f3765]) ).
thf(f3769,plain,
( ! [X0: $i] :
( ( $false
= ( in @ X0 @ sF6 ) )
| ( $false
= ( in @ sF8 @ ( powerset @ sK0 ) ) )
| ( $true
= ( in @ sF8 @ ( powerset @ X0 ) ) )
| ( $false
= ( in @ X0 @ sF6 ) )
| ( $true
= ( in @ ( sK18 @ X0 @ sF8 @ sK0 ) @ sF11 ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_71 ),
inference(forward_demodulation,[],[f3766,f44]) ).
thf(f3770,plain,
( ! [X0: $i] :
( ( $false
= ( in @ X0 @ sF6 ) )
| ( $true
= ( in @ ( sK18 @ X0 @ sF8 @ sK0 ) @ sF11 ) )
| ( $false
= ( in @ sF8 @ ( powerset @ sK0 ) ) )
| ( $true
= ( in @ sF8 @ ( powerset @ X0 ) ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_71 ),
inference(duplicate_literal_removal,[],[f3769]) ).
thf(f3773,plain,
( ! [X0: $i] :
( ( $true
= ( in @ ( sK18 @ X0 @ sF8 @ sK0 ) @ sF11 ) )
| ( $false
= ( in @ X0 @ sF6 ) )
| ( $false
= ( in @ sF8 @ sF6 ) )
| ( $true
= ( in @ sF8 @ ( powerset @ X0 ) ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_71 ),
inference(forward_demodulation,[],[f3770,f44]) ).
thf(f3775,plain,
( ! [X0: $i] :
( ( $false
= ( in @ X0 @ sF6 ) )
| ( $true = $false )
| ( $true
= ( in @ ( sK18 @ X0 @ sF8 @ sK0 ) @ sF11 ) )
| ( $true
= ( in @ sF8 @ ( powerset @ X0 ) ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_71 ),
inference(forward_demodulation,[],[f3773,f2535]) ).
thf(f3776,plain,
( ! [X0: $i] :
( ( $true
= ( in @ ( sK18 @ X0 @ sF8 @ sK0 ) @ sF11 ) )
| ( $true
= ( in @ sF8 @ ( powerset @ X0 ) ) )
| ( $false
= ( in @ X0 @ sF6 ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_71 ),
inference(trivial_inequality_removal,[],[f3775]) ).
thf(f3910,plain,
( ( ( in @ sF11 @ sF6 )
= $false )
| ( $true
= ( in @ sF8 @ ( powerset @ sF11 ) ) )
| ( $true = $false )
| ( $false
= ( in @ sF11 @ ( powerset @ sK0 ) ) )
| ( $true
= ( in @ sF8 @ ( powerset @ sF11 ) ) )
| ( $false
= ( in @ sF8 @ ( powerset @ sK0 ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_71 ),
inference(constrained_superposition,[],[f3776,f200]) ).
thf(f3914,plain,
( ( $true = $false )
| ( $false
= ( in @ sF11 @ ( powerset @ sK0 ) ) )
| ( ( in @ sF11 @ sF6 )
= $false )
| ( $true
= ( in @ sF8 @ ( powerset @ sF11 ) ) )
| ( $false
= ( in @ sF8 @ ( powerset @ sK0 ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_71 ),
inference(duplicate_literal_removal,[],[f3910]) ).
thf(f3915,plain,
( ( $true
= ( in @ sF8 @ ( powerset @ sF11 ) ) )
| ( ( in @ sF11 @ sF6 )
= $false )
| ( $false
= ( in @ sF8 @ ( powerset @ sK0 ) ) )
| ( $false
= ( in @ sF11 @ ( powerset @ sK0 ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_71 ),
inference(trivial_inequality_removal,[],[f3914]) ).
thf(f3918,plain,
( ( $false
= ( in @ sF11 @ ( powerset @ sK0 ) ) )
| ( $false
= ( in @ sF8 @ ( powerset @ sK0 ) ) )
| ( $true
= ( in @ sF8 @ ( powerset @ sF11 ) ) )
| ( $true = $false )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_43
| ~ spl33_71 ),
inference(forward_demodulation,[],[f3915,f446]) ).
thf(f3919,plain,
( ( $false
= ( in @ sF11 @ ( powerset @ sK0 ) ) )
| ( $false
= ( in @ sF8 @ ( powerset @ sK0 ) ) )
| ( $true
= ( in @ sF8 @ ( powerset @ sF11 ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_43
| ~ spl33_71 ),
inference(trivial_inequality_removal,[],[f3918]) ).
thf(f3921,plain,
( ( $false
= ( in @ sF8 @ ( powerset @ sK0 ) ) )
| ( $true
= ( in @ sF8 @ ( powerset @ sF11 ) ) )
| ( ( in @ sF11 @ sF6 )
= $false )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_43
| ~ spl33_71 ),
inference(forward_demodulation,[],[f3919,f44]) ).
thf(f3923,plain,
( ( ( in @ sF11 @ sF6 )
= $false )
| ( $false
= ( in @ sF8 @ sF6 ) )
| ( $true
= ( in @ sF8 @ ( powerset @ sF11 ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_43
| ~ spl33_71 ),
inference(forward_demodulation,[],[f3921,f44]) ).
thf(f3926,plain,
( ( $false
= ( in @ sF8 @ sF6 ) )
| ( $true
= ( in @ sF8 @ ( powerset @ sF11 ) ) )
| ( $true = $false )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_43
| ~ spl33_71 ),
inference(forward_demodulation,[],[f3923,f446]) ).
thf(f3927,plain,
( ( $false
= ( in @ sF8 @ sF6 ) )
| ( $true
= ( in @ sF8 @ ( powerset @ sF11 ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_43
| ~ spl33_71 ),
inference(trivial_inequality_removal,[],[f3926]) ).
thf(f3930,plain,
( ( $true = $false )
| ( $true
= ( in @ sF8 @ ( powerset @ sF11 ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_43
| ~ spl33_71 ),
inference(forward_demodulation,[],[f3927,f2535]) ).
thf(f3931,plain,
( ( $true
= ( in @ sF8 @ ( powerset @ sF11 ) ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_43
| ~ spl33_71 ),
inference(trivial_inequality_removal,[],[f3930]) ).
thf(f3932,plain,
( ( $true
= ( in @ sF8 @ sF12 ) )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_43
| ~ spl33_71 ),
inference(forward_demodulation,[],[f3931,f55]) ).
thf(f3933,plain,
( ( $true = $false )
| ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_19
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_43
| ~ spl33_71 ),
inference(forward_demodulation,[],[f3932,f269]) ).
thf(f3934,plain,
( $false
| ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_19
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_43
| ~ spl33_71 ),
inference(trivial_inequality_removal,[],[f3933]) ).
thf(f3935,plain,
( ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_19
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_43
| ~ spl33_71 ),
inference(avatar_contradiction_clause,[],[f3934]) ).
thf(f3936,plain,
( ( ( in @ sF9 @ sF6 )
= $false )
| ( $false
= ( in @ sF10 @ sF6 ) )
| ~ spl33_15
| spl33_43 ),
inference(forward_subsumption_resolution,[],[f578,f445]) ).
thf(f3951,plain,
( ( $true = $false )
| ~ spl33_44
| ~ spl33_70 ),
inference(constrained_superposition,[],[f450,f2524]) ).
thf(f3956,plain,
( $false
| ~ spl33_44
| ~ spl33_70 ),
inference(trivial_inequality_removal,[],[f3951]) ).
thf(f3957,plain,
( ~ spl33_44
| ~ spl33_70 ),
inference(avatar_contradiction_clause,[],[f3956]) ).
thf(f3958,plain,
( ( $true = $false )
| ( $false
= ( in @ sF10 @ sF6 ) )
| ~ spl33_15
| ~ spl33_25
| ~ spl33_27
| spl33_43 ),
inference(forward_demodulation,[],[f3936,f560]) ).
thf(f3959,plain,
( ( $false
= ( in @ sF10 @ sF6 ) )
| ~ spl33_15
| ~ spl33_25
| ~ spl33_27
| spl33_43 ),
inference(trivial_inequality_removal,[],[f3958]) ).
thf(f3961,plain,
( spl33_44
| ~ spl33_15
| ~ spl33_25
| ~ spl33_27
| spl33_43 ),
inference(avatar_split_clause,[],[f3959,f444,f303,f295,f249,f448]) ).
cnf(s1,plain,
( spl33_1
| spl33_2 ),
inference(sat_conversion,[],[f193]) ).
cnf(s2,plain,
( spl33_2
| spl33_3 ),
inference(sat_conversion,[],[f197]) ).
cnf(s3,plain,
( spl33_2
| spl33_4 ),
inference(sat_conversion,[],[f201]) ).
cnf(s11,plain,
( spl33_14
| spl33_15 ),
inference(sat_conversion,[],[f251]) ).
cnf(s12,plain,
spl33_5,
inference(sat_conversion,[],[f252]) ).
cnf(s14,plain,
( spl33_18
| spl33_19 ),
inference(sat_conversion,[],[f270]) ).
cnf(s18,plain,
( spl33_24
| spl33_25 ),
inference(sat_conversion,[],[f297]) ).
cnf(s19,plain,
( spl33_26
| spl33_27 ),
inference(sat_conversion,[],[f306]) ).
cnf(s22,plain,
( spl33_32
| spl33_33 ),
inference(sat_conversion,[],[f333]) ).
cnf(s23,plain,
spl33_20,
inference(sat_conversion,[],[f334]) ).
cnf(s24,plain,
( spl33_34
| spl33_35 ),
inference(sat_conversion,[],[f342]) ).
cnf(s31,plain,
spl33_37,
inference(sat_conversion,[],[f377]) ).
cnf(s32,plain,
~ spl33_18,
inference(sat_conversion,[],[f378]) ).
cnf(s33,plain,
spl33_31,
inference(sat_conversion,[],[f379]) ).
cnf(s34,plain,
spl33_10,
inference(sat_conversion,[],[f380]) ).
cnf(s35,plain,
spl33_29,
inference(sat_conversion,[],[f383]) ).
cnf(s36,plain,
( ~ spl33_20
| ~ spl33_24 ),
inference(sat_conversion,[],[f386]) ).
cnf(s37,plain,
( ~ spl33_26
| ~ spl33_29 ),
inference(sat_conversion,[],[f389]) ).
cnf(s38,plain,
( ~ spl33_10
| ~ spl33_14 ),
inference(sat_conversion,[],[f392]) ).
cnf(s41,plain,
( ~ spl33_2
| ~ spl33_5 ),
inference(sat_conversion,[],[f419]) ).
cnf(s45,plain,
( ~ spl33_34
| ~ spl33_37 ),
inference(sat_conversion,[],[f435]) ).
cnf(s72,plain,
( ~ spl33_31
| ~ spl33_33 ),
inference(sat_conversion,[],[f2547]) ).
cnf(s73,plain,
( ~ spl33_25
| ~ spl33_32
| spl33_70 ),
inference(sat_conversion,[],[f2552]) ).
cnf(s74,plain,
( ~ spl33_15
| ~ spl33_27
| ~ spl33_32
| spl33_71 ),
inference(sat_conversion,[],[f2553]) ).
cnf(s77,plain,
( ~ spl33_30
| ~ spl33_32 ),
inference(sat_conversion,[],[f2560]) ).
cnf(s88,plain,
( ~ spl33_1
| ~ spl33_3
| ~ spl33_4
| ~ spl33_19
| ~ spl33_27
| spl33_30
| ~ spl33_35
| ~ spl33_43
| ~ spl33_71 ),
inference(sat_conversion,[],[f3935]) ).
cnf(s90,plain,
( ~ spl33_44
| ~ spl33_70 ),
inference(sat_conversion,[],[f3957]) ).
cnf(s91,plain,
( ~ spl33_15
| ~ spl33_25
| ~ spl33_27
| spl33_43
| spl33_44 ),
inference(sat_conversion,[],[f3961]) ).
cnf(s92,plain,
~ spl33_26,
inference(rat,[],[s37,s35]) ).
cnf(s93,plain,
~ spl33_14,
inference(rat,[],[s38,s34]) ).
cnf(s94,plain,
~ spl33_33,
inference(rat,[],[s72,s33]) ).
cnf(s96,plain,
~ spl33_34,
inference(rat,[],[s45,s31]) ).
cnf(s97,plain,
spl33_35,
inference(rat,[],[s24,s96]) ).
cnf(s98,plain,
~ spl33_24,
inference(rat,[],[s36,s23]) ).
cnf(s99,plain,
spl33_32,
inference(rat,[],[s22,s94]) ).
cnf(s100,plain,
~ spl33_30,
inference(rat,[],[s77,s99]) ).
cnf(s102,plain,
spl33_27,
inference(rat,[],[s19,s92]) ).
cnf(s106,plain,
spl33_25,
inference(rat,[],[s18,s98]) ).
cnf(s107,plain,
spl33_70,
inference(rat,[],[s73,s99,s106]) ).
cnf(s108,plain,
~ spl33_44,
inference(rat,[],[s90,s107]) ).
cnf(s109,plain,
spl33_19,
inference(rat,[],[s14,s32]) ).
cnf(s111,plain,
~ spl33_2,
inference(rat,[],[s41,s12]) ).
cnf(s112,plain,
spl33_15,
inference(rat,[],[s11,s93]) ).
cnf(s113,plain,
spl33_43,
inference(rat,[],[s91,s108,s106,s102,s112]) ).
cnf(s114,plain,
spl33_71,
inference(rat,[],[s74,s102,s99,s112]) ).
cnf(s115,plain,
spl33_4,
inference(rat,[],[s3,s111]) ).
cnf(s116,plain,
spl33_3,
inference(rat,[],[s2,s111]) ).
cnf(s117,plain,
~ spl33_1,
inference(rat,[],[s88,s114,s113,s97,s100,s102,s109,s115,s116]) ).
cnf(s120,plain,
$false,
inference(rat,[],[s1,s111,s117]) ).
thf(f3962,plain,
$false,
inference(avatar_sat_refutation,[],[s120]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU743^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.17 % Computer : n014.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 14:19:30 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.69/1.14 % (2733128)Will run a generic schedule for satisfiability detection.
% 5.69/1.14 % (2733135)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1277312452:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.69/1.14 % (2733134)% WARNING: option uhcvi not known.
% 5.69/1.14 % (2733133)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2691147931_2999 on theBenchmark for (2999ds/0Mi)
% 5.69/1.14 % (2733134)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1794487365:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.69/1.14 % (2733136)dis+10_1_sil=32000:sp=arity:random_seed=1194695277:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.69/1.14 % (2733137)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1514432904:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.69/1.14 % (2733139)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2183856604:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.69/1.14 % (2733134)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 5.69/1.14 % (2733137)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 5.69/1.14 % Exception at run slice level
% 5.69/1.14 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.69/1.14 % (2733134)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 5.69/1.14 % (2733138)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1227478254:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.69/1.14 % (2733146)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1255785360:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.69/1.14 % Exception at run slice level
% 5.69/1.14 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.69/1.14 % (2733149)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3809268225:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.69/1.14 % (2733136)Instruction limit reached!
% 5.69/1.14 % (2733136)------------------------------
% 5.69/1.14 % (2733136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.14 % (2733136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.14 % (2733136)CaDiCaL version: 2.1.3
% 5.69/1.14 % (2733136)Termination reason: Instruction limit
% 5.69/1.14 % (2733136)Termination phase: Saturation
% 5.69/1.14 % (2733136)Time elapsed: 0.048 s
% 5.69/1.14 % (2733136)Peak memory usage: 12 MB
% 5.69/1.14 % (2733136)Instructions burned: 105 (million)
% 5.69/1.14 % (2733137)Instruction limit reached!
% 5.69/1.14 % (2733137)------------------------------
% 5.69/1.14 % (2733137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.14 % (2733137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.14 % (2733137)CaDiCaL version: 2.1.3
% 5.69/1.14 % (2733137)Termination reason: Instruction limit
% 5.69/1.14 % (2733137)Termination phase: Saturation
% 5.69/1.14 % (2733137)Time elapsed: 0.053 s
% 5.69/1.14 % (2733137)Peak memory usage: 12 MB
% 5.69/1.14 % (2733137)Instructions burned: 116 (million)
% 5.69/1.14 % (2733151)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=75805104:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 5.69/1.14 % (2733151)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 5.69/1.14 % (2733151)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 5.69/1.14 % (2733152)ott-21_1_sil=16000:fs=off:random_seed=3631313305:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 5.69/1.14 % (2733139)Instruction limit reached!
% 5.69/1.14 % (2733139)------------------------------
% 5.69/1.14 % (2733139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.69/1.14 % (2733139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.69/1.14 % (2733139)CaDiCaL version: 2.1.3
% 5.69/1.14 % (2733139)Termination reason: Instruction limit
% 5.69/1.14 % (2733139)Termination phase: Saturation
% 5.69/1.14 % (2733139)Time elapsed: 0.075 s
% 5.69/1.14 % (2733139)Peak memory usage: 13 MB
% 5.69/1.14 % (2733139)Instructions burned: 159 (million)
% 5.69/1.14 % (2733155)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2419930158:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 17.07/2.79 % (2733149)Instruction limit reached!
% 17.07/2.79 % (2733149)------------------------------
% 17.07/2.79 % (2733149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.07/2.79 % (2733149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.07/2.79 % (2733149)CaDiCaL version: 2.1.3
% 17.07/2.79 % (2733149)Termination reason: Instruction limit
% 17.07/2.79 % (2733149)Termination phase: Saturation
% 17.07/2.79 % (2733149)Time elapsed: 0.061 s
% 17.07/2.79 % (2733149)Peak memory usage: 12 MB
% 17.07/2.79 % (2733149)Instructions burned: 133 (million)
% 17.07/2.79 % (2733138)Instruction limit reached!
% 17.07/2.79 % (2733138)------------------------------
% 17.07/2.79 % (2733138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.07/2.79 % (2733138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.07/2.79 % (2733138)CaDiCaL version: 2.1.3
% 17.07/2.79 % (2733138)Termination reason: Instruction limit
% 17.07/2.79 % (2733138)Termination phase: Saturation
% 17.07/2.79 % (2733138)Time elapsed: 0.104 s
% 17.07/2.79 % (2733138)Peak memory usage: 12 MB
% 17.07/2.79 % (2733138)Instructions burned: 131 (million)
% 17.07/2.79 % (2733157)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1453682809:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 17.07/2.79 % Exception at run slice level
% 17.07/2.79 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.07/2.79 % (2733158)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3599677181:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 17.07/2.79 % (2733160)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3883308747:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 17.07/2.79 % Exception at run slice level
% 17.07/2.79 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.07/2.79 % (2733152)Instruction limit reached!
% 17.07/2.79 % (2733152)------------------------------
% 17.07/2.79 % (2733152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.07/2.79 % (2733152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.07/2.79 % (2733152)CaDiCaL version: 2.1.3
% 17.07/2.79 % (2733152)Termination reason: Instruction limit
% 17.07/2.79 % (2733152)Termination phase: Saturation
% 17.07/2.79 % (2733152)Time elapsed: 0.078 s
% 17.07/2.79 % (2733152)Peak memory usage: 12 MB
% 17.07/2.79 % (2733152)Instructions burned: 181 (million)
% 17.07/2.79 % (2733163)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1019068930:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 17.07/2.79 % (2733163)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 17.07/2.79 % (2733164)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2248722598:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 17.07/2.79 % (2733164)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 17.07/2.79 % (2733155)Instruction limit reached!
% 17.07/2.79 % (2733155)------------------------------
% 17.07/2.79 % (2733155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.07/2.79 % (2733155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.07/2.79 % (2733155)CaDiCaL version: 2.1.3
% 17.07/2.79 % (2733155)Termination reason: Instruction limit
% 17.07/2.79 % (2733155)Termination phase: Saturation
% 17.07/2.79 % (2733155)Time elapsed: 0.235 s
% 17.07/2.79 % (2733155)Peak memory usage: 13 MB
% 17.07/2.79 % (2733155)Instructions burned: 478 (million)
% 17.07/2.79 % (2733167)fmb+10_1_sil=64000:random_seed=974871175:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 17.07/2.79 % (2733167)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 17.07/2.79 % Exception at run slice level
% 17.07/2.79 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.07/2.79 % (2733169)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2090323333:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 17.07/2.79 % Exception at run slice level
% 17.07/2.79 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 45.16/6.63 % (2733151)Instruction limit reached!
% 45.16/6.63 % (2733151)------------------------------
% 45.16/6.63 % (2733151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.16/6.63 % (2733151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.16/6.63 % (2733151)CaDiCaL version: 2.1.3
% 45.16/6.63 % (2733151)Termination reason: Instruction limit
% 45.16/6.63 % (2733151)Termination phase: Saturation
% 45.16/6.63 % (2733151)Time elapsed: 0.312 s
% 45.16/6.63 % (2733151)Peak memory usage: 14 MB
% 45.16/6.63 % (2733151)Instructions burned: 684 (million)
% 45.16/6.63 % (2733171)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=641057236:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 45.16/6.63 % Exception at run slice level
% 45.16/6.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 45.16/6.63 % (2733172)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3415299852:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 45.16/6.63 % (2733172)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 45.16/6.63 % (2733174)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=44324004:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 45.16/6.63 % (2733174)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 45.16/6.63 % (2733174)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 45.16/6.63 % (2733163)Instruction limit reached!
% 45.16/6.63 % (2733163)------------------------------
% 45.16/6.63 % (2733163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.16/6.63 % (2733163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.16/6.63 % (2733163)CaDiCaL version: 2.1.3
% 45.16/6.63 % (2733163)Termination reason: Instruction limit
% 45.16/6.63 % (2733163)Termination phase: Saturation
% 45.16/6.63 % (2733163)Time elapsed: 0.314 s
% 45.16/6.63 % (2733163)Peak memory usage: 16 MB
% 45.16/6.63 % (2733163)Instructions burned: 693 (million)
% 45.16/6.63 % (2733177)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3321410410:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 45.16/6.63 % Exception at run slice level
% 45.16/6.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 45.16/6.63 % (2733179)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3760082994:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 45.16/6.63 % Exception at run slice level
% 45.16/6.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 45.16/6.63 % (2733181)ott-2_1_sil=16000:newcnf=on:random_seed=3492556329:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 45.16/6.63 % (2733181)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 45.16/6.63 % (2733164)Instruction limit reached!
% 45.16/6.63 % (2733164)------------------------------
% 45.16/6.63 % (2733164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.16/6.63 % (2733164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.16/6.63 % (2733164)CaDiCaL version: 2.1.3
% 45.16/6.63 % (2733164)Termination reason: Instruction limit
% 45.16/6.63 % (2733164)Termination phase: Saturation
% 45.16/6.63 % (2733164)Time elapsed: 0.409 s
% 45.16/6.63 % (2733164)Peak memory usage: 13 MB
% 45.16/6.63 % (2733164)Instructions burned: 879 (million)
% 45.16/6.63 % (2733183)ott+10_1_sil=32000:tgt=ground:random_seed=2223932126:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 45.16/6.63 % (2733158)Instruction limit reached!
% 45.16/6.63 % (2733158)------------------------------
% 45.16/6.63 % (2733158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.16/6.63 % (2733158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.16/6.63 % (2733158)CaDiCaL version: 2.1.3
% 45.16/6.63 % (2733158)Termination reason: Instruction limit
% 45.16/6.63 % (2733158)Termination phase: Saturation
% 45.16/6.63 % (2733158)Time elapsed: 0.719 s
% 45.16/6.63 % (2733158)Peak memory usage: 17 MB
% 45.16/6.63 % (2733158)Instructions burned: 1180 (million)
% 45.16/6.63 % (2733185)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3453513179:i=54282_2990 on theBenchmark for (2990ds/54282Mi)
% 45.16/6.63 % Exception at run slice level
% 122.28/17.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 122.28/17.60 % (2733187)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2982799398:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi)
% 122.28/17.60 % (2733187)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 122.28/17.60 % (2733181)Instruction limit reached!
% 122.28/17.60 % (2733181)------------------------------
% 122.28/17.60 % (2733181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.28/17.60 % (2733181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.28/17.60 % (2733181)CaDiCaL version: 2.1.3
% 122.28/17.60 % (2733181)Termination reason: Instruction limit
% 122.28/17.60 % (2733181)Termination phase: Saturation
% 122.28/17.60 % (2733181)Time elapsed: 0.364 s
% 122.28/17.60 % (2733181)Peak memory usage: 15 MB
% 122.28/17.60 % (2733181)Instructions burned: 871 (million)
% 122.28/17.60 % (2733189)dis+21_1_sil=32000:sas=cadical:random_seed=1493770199:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi)
% 122.28/17.60 % (2733174)Instruction limit reached!
% 122.28/17.60 % (2733174)------------------------------
% 122.28/17.60 % (2733174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.28/17.60 % (2733174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.28/17.60 % (2733174)CaDiCaL version: 2.1.3
% 122.28/17.60 % (2733174)Termination reason: Instruction limit
% 122.28/17.60 % (2733174)Termination phase: Saturation
% 122.28/17.60 % (2733174)Time elapsed: 0.681 s
% 122.28/17.60 % (2733174)Peak memory usage: 16 MB
% 122.28/17.60 % (2733174)Instructions burned: 1473 (million)
% 122.28/17.60 % (2733191)ott+11_1_sil=16000:gs=on:random_seed=2630923868:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi)
% 122.28/17.60 % (2733191)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 122.28/17.60 % (2733191)Instruction limit reached!
% 122.28/17.60 % (2733191)------------------------------
% 122.28/17.60 % (2733191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.28/17.60 % (2733191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.28/17.60 % (2733191)CaDiCaL version: 2.1.3
% 122.28/17.60 % (2733191)Termination reason: Instruction limit
% 122.28/17.60 % (2733191)Termination phase: Saturation
% 122.28/17.60 % (2733191)Time elapsed: 0.895 s
% 122.28/17.60 % (2733191)Peak memory usage: 15 MB
% 122.28/17.60 % (2733191)Instructions burned: 2252 (million)
% 122.28/17.60 % (2733193)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=795776409:fmbsr=1.6:i=67534_2979 on theBenchmark for (2979ds/67534Mi)
% 122.28/17.60 % Exception at run slice level
% 122.28/17.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 122.28/17.60 % (2733195)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=259491183:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2979 on theBenchmark for (2979ds/4591Mi)
% 122.28/17.60 % (2733187)Instruction limit reached!
% 122.28/17.60 % (2733187)------------------------------
% 122.28/17.60 % (2733187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.28/17.60 % (2733187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.28/17.60 % (2733187)CaDiCaL version: 2.1.3
% 122.28/17.60 % (2733187)Termination reason: Instruction limit
% 122.28/17.60 % (2733187)Termination phase: Saturation
% 122.28/17.60 % (2733187)Time elapsed: 1.575 s
% 122.28/17.60 % (2733187)Peak memory usage: 19 MB
% 122.28/17.60 % (2733187)Instructions burned: 3514 (million)
% 122.28/17.60 % (2733197)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1037497671:i=29340_2974 on theBenchmark for (2974ds/29340Mi)
% 122.28/17.60 % (2733189)Instruction limit reached!
% 122.28/17.60 % (2733189)------------------------------
% 122.28/17.60 % (2733189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.28/17.60 % (2733189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.28/17.60 % (2733189)CaDiCaL version: 2.1.3
% 122.28/17.60 % (2733189)Termination reason: Instruction limit
% 122.28/17.60 % (2733189)Termination phase: Saturation
% 122.28/17.60 % (2733189)Time elapsed: 1.578 s
% 122.28/17.60 % (2733189)Peak memory usage: 20 MB
% 122.28/17.60 % (2733189)Instructions burned: 3774 (million)
% 122.28/17.60 % (2733199)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4065954315:i=5211_2974 on theBenchmark for (2974ds/5211Mi)
% 150.61/21.58 % (2733172)Instruction limit reached!
% 150.61/21.58 % (2733172)------------------------------
% 150.61/21.58 % (2733172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.61/21.58 % (2733172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.61/21.58 % (2733172)CaDiCaL version: 2.1.3
% 150.61/21.58 % (2733172)Termination reason: Instruction limit
% 150.61/21.58 % (2733172)Termination phase: Saturation
% 150.61/21.58 % (2733172)Time elapsed: 2.147 s
% 150.61/21.58 % (2733172)Peak memory usage: 22 MB
% 150.61/21.58 % (2733172)Instructions burned: 5133 (million)
% 150.61/21.58 % (2733201)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3177031450:i=5497:nm=2_2974 on theBenchmark for (2974ds/5497Mi)
% 150.61/21.58 % Exception at run slice level
% 150.61/21.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 150.61/21.58 % (2733203)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4241472794:fmbsr=2:i=46332_2973 on theBenchmark for (2973ds/46332Mi)
% 150.61/21.58 % Exception at run slice level
% 150.61/21.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 150.61/21.58 % (2733205)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=774769527:i=14071_2973 on theBenchmark for (2973ds/14071Mi)
% 150.61/21.58 % Exception at run slice level
% 150.61/21.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 150.61/21.58 % (2733207)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=233274244:i=22565:add=on:rawr=on_2973 on theBenchmark for (2973ds/22565Mi)
% 150.61/21.58 % (2733183)Instruction limit reached!
% 150.61/21.58 % (2733183)------------------------------
% 150.61/21.58 % (2733183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.61/21.58 % (2733183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.61/21.58 % (2733183)CaDiCaL version: 2.1.3
% 150.61/21.58 % (2733183)Termination reason: Instruction limit
% 150.61/21.58 % (2733183)Termination phase: Saturation
% 150.61/21.58 % (2733183)Time elapsed: 2.209 s
% 150.61/21.58 % (2733183)Peak memory usage: 31 MB
% 150.61/21.58 % (2733183)Instructions burned: 5116 (million)
% 150.61/21.58 % (2733209)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=767317239:i=8173:av=off_2971 on theBenchmark for (2971ds/8173Mi)
% 150.61/21.58 % (2733195)Instruction limit reached!
% 150.61/21.58 % (2733195)------------------------------
% 150.61/21.58 % (2733195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.61/21.58 % (2733195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.61/21.58 % (2733195)CaDiCaL version: 2.1.3
% 150.61/21.58 % (2733195)Termination reason: Instruction limit
% 150.61/21.58 % (2733195)Termination phase: Saturation
% 150.61/21.58 % (2733195)Time elapsed: 2.015 s
% 150.61/21.58 % (2733195)Peak memory usage: 25 MB
% 150.61/21.58 % (2733195)Instructions burned: 4592 (million)
% 150.61/21.58 % (2733211)dis+10_16:1_sil=16000:random_seed=1172480082:i=9155:fsr=off_2958 on theBenchmark for (2958ds/9155Mi)
% 150.61/21.58 % (2733199)Instruction limit reached!
% 150.61/21.58 % (2733199)------------------------------
% 150.61/21.58 % (2733199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.61/21.58 % (2733199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.61/21.58 % (2733199)CaDiCaL version: 2.1.3
% 150.61/21.58 % (2733199)Termination reason: Instruction limit
% 150.61/21.58 % (2733199)Termination phase: Saturation
% 150.61/21.58 % (2733199)Time elapsed: 2.265 s
% 150.61/21.58 % (2733199)Peak memory usage: 23 MB
% 150.61/21.58 % (2733199)Instructions burned: 5213 (million)
% 150.61/21.58 % (2733213)ott-3_8_sil=64000:random_seed=2306212112:i=20139:bs=on_2951 on theBenchmark for (2951ds/20139Mi)
% 150.61/21.58 % (2733209)Instruction limit reached!
% 150.61/21.58 % (2733209)------------------------------
% 150.61/21.58 % (2733209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.61/21.58 % (2733209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.61/21.58 % (2733209)CaDiCaL version: 2.1.3
% 150.61/21.58 % (2733209)Termination reason: Instruction limit
% 150.61/21.58 % (2733209)Termination phase: Saturation
% 150.61/21.58 % (2733209)Time elapsed: 3.512 s
% 150.61/21.58 % (2733209)Peak memory usage: 46 MB
% 150.61/21.58 % (2733209)Instructions burned: 8175 (million)
% 150.61/21.58 % (2733215)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3630814838:fmbsr=2:i=32576_2936 on theBenchmark for (2936ds/32576Mi)
% 159.28/22.80 % Exception at run slice level
% 159.28/22.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 159.28/22.80 % (2733217)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2378736700:i=11404_2935 on theBenchmark for (2935ds/11404Mi)
% 159.28/22.80 % (2733211)Instruction limit reached!
% 159.28/22.80 % (2733211)------------------------------
% 159.28/22.80 % (2733211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.28/22.80 % (2733211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.28/22.80 % (2733211)CaDiCaL version: 2.1.3
% 159.28/22.80 % (2733211)Termination reason: Instruction limit
% 159.28/22.80 % (2733211)Termination phase: Saturation
% 159.28/22.80 % (2733211)Time elapsed: 3.797 s
% 159.28/22.80 % (2733211)Peak memory usage: 21 MB
% 159.28/22.80 % (2733211)Instructions burned: 9157 (million)
% 159.28/22.80 % (2733219)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3316933277:i=14134_2920 on theBenchmark for (2920ds/14134Mi)
% 159.28/22.80 % (2733219)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 159.28/22.80 % (2733217)Instruction limit reached!
% 159.28/22.80 % (2733217)------------------------------
% 159.28/22.80 % (2733217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.28/22.80 % (2733217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.28/22.80 % (2733217)CaDiCaL version: 2.1.3
% 159.28/22.80 % (2733217)Termination reason: Instruction limit
% 159.28/22.80 % (2733217)Termination phase: Saturation
% 159.28/22.80 % (2733217)Time elapsed: 4.833 s
% 159.28/22.80 % (2733217)Peak memory usage: 47 MB
% 159.28/22.80 % (2733217)Instructions burned: 11405 (million)
% 159.28/22.80 % (2733221)dis+33_16_sil=32000:sac=on:random_seed=3635610850:i=15851:nm=0_2887 on theBenchmark for (2887ds/15851Mi)
% 159.28/22.80 % (2733207)Instruction limit reached!
% 159.28/22.80 % (2733207)------------------------------
% 159.28/22.80 % (2733207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.28/22.80 % (2733207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.28/22.80 % (2733207)CaDiCaL version: 2.1.3
% 159.28/22.80 % (2733207)Termination reason: Instruction limit
% 159.28/22.80 % (2733207)Termination phase: Saturation
% 159.28/22.80 % (2733207)Time elapsed: 10.595 s
% 159.28/22.80 % (2733207)Peak memory usage: 60 MB
% 159.28/22.80 % (2733207)Instructions burned: 22567 (million)
% 159.28/22.80 % (2733223)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3986853646:avsq=on:i=17627:add=on:amm=off_2867 on theBenchmark for (2867ds/17627Mi)
% 159.28/22.80 % (2733213)Instruction limit reached!
% 159.28/22.80 % (2733213)------------------------------
% 159.28/22.80 % (2733213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.28/22.80 % (2733213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.28/22.80 % (2733213)CaDiCaL version: 2.1.3
% 159.28/22.80 % (2733213)Termination reason: Instruction limit
% 159.28/22.80 % (2733213)Termination phase: Saturation
% 159.28/22.80 % (2733213)Time elapsed: 8.827 s
% 159.28/22.80 % (2733213)Peak memory usage: 84 MB
% 159.28/22.80 % (2733213)Instructions burned: 20140 (million)
% 159.28/22.80 % (2733225)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=664336216:s2a=on:i=53295_2863 on theBenchmark for (2863ds/53295Mi)
% 159.28/22.80 % (2733219)Instruction limit reached!
% 159.28/22.80 % (2733219)------------------------------
% 159.28/22.80 % (2733219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.28/22.80 % (2733219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.28/22.80 % (2733219)CaDiCaL version: 2.1.3
% 159.28/22.80 % (2733219)Termination reason: Instruction limit
% 159.28/22.80 % (2733219)Termination phase: Saturation
% 159.28/22.80 % (2733219)Time elapsed: 6.581 s
% 159.28/22.80 % (2733219)Peak memory usage: 66 MB
% 159.28/22.80 % (2733219)Instructions burned: 14135 (million)
% 159.28/22.80 % (2733227)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1696732278:i=26857:ins=20_2854 on theBenchmark for (2854ds/26857Mi)
% 159.28/22.80 % Exception at run slice level
% 159.28/22.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 159.28/22.80 % (2733229)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1432885737:i=28120:bs=on:fsr=off_2854 on theBenchmark for (2854ds/28120Mi)
% 159.28/22.80 % (2733197)Instruction limit reached!
% 159.28/22.80 % (2733197)------------------------------
% 159.28/22.80 % (2733197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.78/24.24 % (2733197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.78/24.24 % (2733197)CaDiCaL version: 2.1.3
% 169.78/24.24 % (2733197)Termination reason: Instruction limit
% 169.78/24.24 % (2733197)Termination phase: Saturation
% 169.78/24.24 % (2733197)Time elapsed: 14.839 s
% 169.78/24.24 % (2733197)Peak memory usage: 100 MB
% 169.78/24.24 % (2733197)Instructions burned: 29340 (million)
% 169.78/24.24 % (2733231)fmb+10_1_sil=256000:fmbss=7:random_seed=140840642:fmbsr=1.6:i=182295_2826 on theBenchmark for (2826ds/182295Mi)
% 169.78/24.24 % Exception at run slice level
% 169.78/24.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 169.78/24.24 % (2733233)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=668393761:i=44625:gsp=on_2825 on theBenchmark for (2825ds/44625Mi)
% 169.78/24.24 % (2733233)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 169.78/24.24 % (2733233)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 169.78/24.24 % Exception at run slice level
% 169.78/24.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 169.78/24.24 % (2733235)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2486298845:i=160505_2825 on theBenchmark for (2825ds/160505Mi)
% 169.78/24.24 % Exception at run slice level
% 169.78/24.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 169.78/24.24 % (2733237)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3119803579:fmbsr=1.3:i=225729_2825 on theBenchmark for (2825ds/225729Mi)
% 169.78/24.24 % Exception at run slice level
% 169.78/24.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 169.78/24.24 % (2733239)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1269357832:fmbsr=2:i=185024:ins=7_2825 on theBenchmark for (2825ds/185024Mi)
% 169.78/24.24 % Exception at run slice level
% 169.78/24.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 169.78/24.24 % (2733241)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2913194919:rtra=on_2824 on theBenchmark for (2824ds/0Mi)
% 169.78/24.24 % Exception at run slice level
% 169.78/24.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 169.78/24.24 % (2733243)% WARNING: option uhcvi not known.
% 169.78/24.24 % (2733243)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2530144322:i=271062:add=off:rtra=on:rawr=on_2824 on theBenchmark for (2824ds/271062Mi)
% 169.78/24.24 % (2733243)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 169.78/24.24 % (2733243)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 169.78/24.24 % (2733221)Instruction limit reached!
% 169.78/24.24 % (2733221)------------------------------
% 169.78/24.24 % (2733221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.78/24.24 % (2733221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.78/24.24 % (2733221)CaDiCaL version: 2.1.3
% 169.78/24.24 % (2733221)Termination reason: Instruction limit
% 169.78/24.24 % (2733221)Termination phase: Saturation
% 169.78/24.24 % (2733221)Time elapsed: 6.914 s
% 169.78/24.24 % (2733221)Peak memory usage: 67 MB
% 169.78/24.24 % (2733221)Instructions burned: 15852 (million)
% 169.78/24.24 % (2733245)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4028474949:i=176048:add=on:rtra=on:rawr=on_2817 on theBenchmark for (2817ds/176048Mi)
% 169.78/24.24 % (2733223)Instruction limit reached!
% 169.78/24.24 % (2733223)------------------------------
% 169.78/24.24 % (2733223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.78/24.24 % (2733223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.78/24.24 % (2733223)CaDiCaL version: 2.1.3
% 169.78/24.24 % (2733223)Termination reason: Instruction limit
% 169.78/24.24 % (2733223)Termination phase: Saturation
% 169.78/24.24 % (2733223)Time elapsed: 7.920 s
% 169.78/24.24 % (2733223)Peak memory usage: 91 MB
% 169.78/24.24 % (2733223)Instructions burned: 17627 (million)
% 169.78/24.24 % (2733403)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1908567675:i=206:fgj=on:rtra=on_2787 on theBenchmark for (2787ds/206Mi)
% 169.78/24.24 % (2733403)Instruction limit reached!
% 169.78/24.24 % (2733403)------------------------------
% 169.78/24.24 % (2733403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.78/24.24 % (2733403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.78/24.24 % (2733403)CaDiCaL version: 2.1.3
% 169.78/24.24 % (2733403)Termination reason: Instruction limit
% 169.78/24.24 % (2733403)Termination phase: Saturation
% 169.78/24.24 % (2733403)Time elapsed: 0.092 s
% 169.78/24.24 % (2733403)Peak memory usage: 12 MB
% 169.78/24.24 % (2733403)Instructions burned: 206 (million)
% 169.78/24.24 % (2733405)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1033031043:i=232:rtra=on_2786 on theBenchmark for (2786ds/232Mi)
% 169.78/24.24 % (2733405)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 169.78/24.24 % (2733405)Instruction limit reached!
% 169.78/24.24 % (2733405)------------------------------
% 169.78/24.24 % (2733405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.78/24.24 % (2733405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.78/24.24 % (2733405)CaDiCaL version: 2.1.3
% 169.78/24.24 % (2733405)Termination reason: Instruction limit
% 169.78/24.24 % (2733405)Termination phase: Saturation
% 169.78/24.24 % (2733405)Time elapsed: 0.108 s
% 169.78/24.24 % (2733405)Peak memory usage: 13 MB
% 169.78/24.24 % (2733405)Instructions burned: 233 (million)
% 169.78/24.24 % (2733407)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3857921180:i=262:rtra=on_2785 on theBenchmark for (2785ds/262Mi)
% 169.78/24.24 % (2733407)Instruction limit reached!
% 169.78/24.24 % (2733407)------------------------------
% 169.78/24.24 % (2733407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.78/24.24 % (2733407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.78/24.24 % (2733407)CaDiCaL version: 2.1.3
% 169.78/24.24 % (2733407)Termination reason: Instruction limit
% 169.78/24.24 % (2733407)Termination phase: Saturation
% 169.78/24.24 % (2733407)Time elapsed: 0.120 s
% 169.78/24.24 % (2733407)Peak memory usage: 13 MB
% 169.78/24.24 % (2733407)Instructions burned: 263 (million)
% 169.78/24.24 % (2733409)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2206183556:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2783 on theBenchmark for (2783ds/318Mi)
% 169.78/24.24 % (2733409)Instruction limit reached!
% 169.78/24.24 % (2733409)------------------------------
% 169.78/24.24 % (2733409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.78/24.24 % (2733409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.78/24.24 % (2733409)CaDiCaL version: 2.1.3
% 169.78/24.24 % (2733409)Termination reason: Instruction limit
% 169.78/24.24 % (2733409)Termination phase: Saturation
% 169.78/24.24 % (2733409)Time elapsed: 0.153 s
% 169.78/24.24 % (2733409)Peak memory usage: 14 MB
% 169.78/24.24 % (2733409)Instructions burned: 320 (million)
% 169.78/24.24 % (2733411)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2179723826:i=1428:nm=2:rtra=on_2781 on theBenchmark for (2781ds/1428Mi)
% 169.78/24.24 % Exception at run slice level
% 169.78/24.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 169.78/24.24 % (2733413)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=990935577:i=262:bd=preordered:rtra=on:fsd=on_2781 on theBenchmark for (2781ds/262Mi)
% 169.78/24.24 % (2733413)Instruction limit reached!
% 169.78/24.24 % (2733413)------------------------------
% 169.78/24.24 % (2733413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.78/24.24 % (2733413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.78/24.24 % (2733413)CaDiCaL version: 2.1.3
% 169.78/24.24 % (2733413)Termination reason: Instruction limit
% 169.78/24.24 % (2733413)Termination phase: Saturation
% 169.78/24.24 % (2733413)Time elapsed: 0.118 s
% 169.78/24.24 % (2733413)Peak memory usage: 13 MB
% 169.78/24.24 % (2733413)Instructions burned: 263 (million)
% 169.78/24.24 % (2733415)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2695654171:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2780 on theBenchmark for (2780ds/1368Mi)
% 169.78/24.24 % (2733415)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 169.78/24.24 % (2733415)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 169.78/24.24 % (2733415)Instruction limit reached!
% 169.78/24.24 % (2733415)------------------------------
% 169.78/24.24 % (2733415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.78/24.24 % (2733415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.78/24.24 % (2733415)CaDiCaL version: 2.1.3
% 169.78/24.24 % (2733415)Termination reason: Instruction limit
% 169.78/24.24 % (2733415)Termination phase: Saturation
% 169.78/24.24 % (2733415)Time elapsed: 0.601 s
% 169.78/24.24 % (2733415)Peak memory usage: 16 MB
% 169.78/24.24 % (2733415)Instructions burned: 1369 (million)
% 169.78/24.24 % (2733417)ott-21_1_sil=16000:si=on:fs=off:random_seed=1833348535:i=360:av=off:fsr=off:rtra=on_2774 on theBenchmark for (2774ds/360Mi)
% 169.78/24.24 % (2733417)Instruction limit reached!
% 169.78/24.24 % (2733417)------------------------------
% 169.78/24.24 % (2733417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.78/24.24 % (2733417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.78/24.24 % (2733417)CaDiCaL version: 2.1.3
% 169.78/24.24 % (2733417)Termination reason: Instruction limit
% 169.78/24.24 % (2733417)Termination phase: Saturation
% 169.78/24.24 % (2733417)Time elapsed: 0.155 s
% 169.78/24.24 % (2733417)Peak memory usage: 12 MB
% 169.78/24.24 % (2733417)Instructions burned: 361 (million)
% 169.78/24.24 % (2733419)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3856111341:i=954:bd=all:rtra=on_2772 on theBenchmark for (2772ds/954Mi)
% 169.78/24.24 % (2733419)Instruction limit reached!
% 169.78/24.24 % (2733419)------------------------------
% 169.78/24.24 % (2733419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.78/24.24 % (2733419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.78/24.24 % (2733419)CaDiCaL version: 2.1.3
% 169.78/24.24 % (2733419)Termination reason: Instruction limit
% 169.78/24.24 % (2733419)Termination phase: Saturation
% 169.78/24.24 % (2733419)Time elapsed: 0.470 s
% 169.78/24.24 % (2733419)Peak memory usage: 14 MB
% 169.78/24.24 % (2733419)Instructions burned: 955 (million)
% 169.78/24.24 % (2733421)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3008786877:fmbsr=1.3:i=1730:ins=25:rtra=on_2767 on theBenchmark for (2767ds/1730Mi)
% 169.78/24.24 % Exception at run slice level
% 169.78/24.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 169.78/24.24 % (2733423)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3481805714:i=2358:rtra=on_2767 on theBenchmark for (2767ds/2358Mi)
% 169.78/24.24 % (2733423) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2733128-2733423"...
% 169.78/24.24 % (2733423)...printing done.
% 169.78/24.24 % (2733423)Refutation found. Thanks to Tanya!
% 169.78/24.24 % SZS status Theorem for theBenchmark
% 169.78/24.24 % SZS output start Proof for theBenchmark
% See solution above
% 169.78/24.24 % (2733423)------------------------------
% 169.78/24.24 % (2733423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.78/24.24 % (2733423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.78/24.24 % (2733423)CaDiCaL version: 2.1.3
% 169.78/24.24 % (2733423)Termination reason: Refutation
% 169.78/24.24 % (2733423)Time elapsed: 0.699 s
% 169.78/24.24 % (2733423)Peak memory usage: 18 MB
% 169.78/24.24 % (2733423)Instructions burned: 1535 (million)
% 169.78/24.24 % (2733128)Success in time 24.021 s
% 169.78/24.24 % Vampire exiting
%------------------------------------------------------------------------------