%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW470+3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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 : Tue Sep 29 01:40:05 PM UTC 2026
% Result : Theorem 17.03s 2.85s
% Output : Refutation 17.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 18
% Syntax : Number of formulae : 77 ( 30 unt; 4 def)
% Number of atoms : 134 ( 36 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 105 ( 48 ~; 46 |; 1 &)
% ( 6 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 5 prp; 0-2 aty)
% Number of functors : 48 ( 48 usr; 24 con; 0-4 aty)
% Number of variables : 55 ( 0 sgn 53 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X0] : is_bool(finite1973466193nt_int(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gsy_c_Finite__Set_Ocomp__fun__commute_000tc__Int__Oint_000tc__Int__Oint) ).
fof(f22,axiom,
is_bool(bot_bot_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gsy_c_Orderings_Obot__class_Obot_000tc__HOL__Obool) ).
fof(f23,axiom,
is_bool(fFalse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gsy_c_fFalse) ).
fof(f41,axiom,
! [X0,X1,X2,X3] :
( ! [X4,X5] :
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,X4),X5))
=> hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(X0),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_s1806633685e_bool(hAPP_f817621513e_bool(cOMBC_2027030106e_bool,fequal_state),X5)),X1,hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_a2036067514e_bool(X2,X4)))),bot_bo797238721a_bool))) )
=> hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(X0),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_a(X3,X1,X2)),bot_bo797238721a_bool))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_escape) ).
fof(f55,axiom,
! [X0] : hAPP_f20753329a_bool(collec351493750iple_a,hAPP_H426895267a_bool(fequal963300192iple_a,X0)) = hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,X0),bot_bo797238721a_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_19_singleton__conv2) ).
fof(f69,axiom,
! [X0] :
( hAPP_f20753329a_bool(collec351493750iple_a,X0) = bot_bo797238721a_bool
<=> ! [X1] : ~ hBOOL(hAPP_H1037229737a_bool(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_33_Collect__empty__eq) ).
fof(f141,axiom,
! [X0] :
( hBOOL(hAPP_H1037229737a_bool(bot_bo797238721a_bool,X0))
<=> hBOOL(bot_bot_bool) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_105_bot__apply) ).
fof(f235,axiom,
! [X0] : hAPP_f20753329a_bool(collec351493750iple_a,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_199_Collect__def) ).
fof(f570,axiom,
hBOOL(finite1973466193nt_int(times_times_int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_534_comp__fun__commute) ).
fof(f1242,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
fof(f1243,axiom,
! [X0] :
( is_bool(X0)
=> ( X0 = fTrue
| X0 = fFalse ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fFalse_1_1_T) ).
fof(f1264,axiom,
! [X0,X1] :
( is_bool(X0)
=> hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,X0),X1) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Ostate_U) ).
fof(f1287,axiom,
! [X0,X1] : hAPP_a2036067514e_bool(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,X0),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000t__a_U) ).
fof(f1399,conjecture,
hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(g),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo797238721a_bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1400,negated_conjecture,
~ hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(g),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo797238721a_bool))),
inference(negated_conjecture,[status(cth)],[f1399]) ).
fof(f1407,plain,
~ hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(g),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo797238721a_bool))),
inference(flattening,[],[f1400]) ).
fof(f1415,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(X0),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_a(X3,X1,X2)),bot_bo797238721a_bool)))
| ? [X4,X5] :
( ~ hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(X0),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_s1806633685e_bool(hAPP_f817621513e_bool(cOMBC_2027030106e_bool,fequal_state),X5)),X1,hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_a2036067514e_bool(X2,X4)))),bot_bo797238721a_bool)))
& hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,X4),X5)) ) ),
inference(ennf_transformation,[],[f41]) ).
fof(f2476,plain,
! [X0] :
( X0 = fTrue
| X0 = fFalse
| ~ is_bool(X0) ),
inference(ennf_transformation,[],[f1243]) ).
fof(f2477,plain,
! [X0] :
( X0 = fTrue
| X0 = fFalse
| ~ is_bool(X0) ),
inference(flattening,[],[f2476]) ).
fof(f2482,plain,
! [X0,X1] :
( hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,X0),X1) = X0
| ~ is_bool(X0) ),
inference(ennf_transformation,[],[f1264]) ).
fof(f2489,plain,
! [X0] : is_bool(finite1973466193nt_int(X0)),
inference(cnf_transformation,[],[f6]) ).
fof(f2505,plain,
is_bool(bot_bot_bool),
inference(cnf_transformation,[],[f22]) ).
fof(f2506,plain,
is_bool(fFalse),
inference(cnf_transformation,[],[f23]) ).
fof(f2528,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,sK0(X0,X1,X2,X3)),sK1(X0,X1,X2,X3)))
| hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(X0),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_a(X3,X1,X2)),bot_bo797238721a_bool))) ),
inference(cnf_transformation,[],[f1415]) ).
fof(f2550,plain,
! [X0] : hAPP_f20753329a_bool(collec351493750iple_a,hAPP_H426895267a_bool(fequal963300192iple_a,X0)) = hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,X0),bot_bo797238721a_bool),
inference(cnf_transformation,[],[f55]) ).
fof(f2571,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_H1037229737a_bool(X0,X1))
| bot_bo797238721a_bool != hAPP_f20753329a_bool(collec351493750iple_a,X0) ),
inference(cnf_transformation,[],[f69]) ).
fof(f2687,plain,
! [X0] :
( ~ hBOOL(bot_bot_bool)
| hBOOL(hAPP_H1037229737a_bool(bot_bo797238721a_bool,X0)) ),
inference(cnf_transformation,[],[f141]) ).
fof(f2825,plain,
! [X0] : hAPP_f20753329a_bool(collec351493750iple_a,X0) = X0,
inference(cnf_transformation,[],[f235]) ).
fof(f3336,plain,
hBOOL(finite1973466193nt_int(times_times_int)),
inference(cnf_transformation,[],[f570]) ).
fof(f4247,plain,
~ hBOOL(fFalse),
inference(cnf_transformation,[],[f1242]) ).
fof(f4248,plain,
! [X0] :
( ~ is_bool(X0)
| fFalse = X0
| fTrue = X0 ),
inference(cnf_transformation,[],[f2477]) ).
fof(f4269,plain,
! [X0,X1] :
( ~ is_bool(X0)
| hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,X0),X1) = X0 ),
inference(cnf_transformation,[],[f2482]) ).
fof(f4292,plain,
! [X0,X1] : hAPP_a2036067514e_bool(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,X0),X1) = X0,
inference(cnf_transformation,[],[f1287]) ).
fof(f4404,plain,
~ hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(g),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo797238721a_bool))),
inference(cnf_transformation,[],[f1407]) ).
fof(f4649,definition,
( spl228_1
<=> ! [X0] : hBOOL(hAPP_H1037229737a_bool(bot_bo797238721a_bool,X0)) ),
introduced(definition,[new_symbols(definition,[spl228_1])],[avatar_definition]) ).
fof(f4650,plain,
( ! [X0] : hBOOL(hAPP_H1037229737a_bool(bot_bo797238721a_bool,X0))
| ~ spl228_1 ),
inference(avatar_component_clause,[],[f4649]) ).
fof(f4652,definition,
( spl228_2
<=> hBOOL(bot_bot_bool) ),
introduced(definition,[new_symbols(definition,[spl228_2])],[avatar_definition]) ).
fof(f4654,plain,
( ~ hBOOL(bot_bot_bool)
| spl228_2 ),
inference(avatar_component_clause,[],[f4652]) ).
fof(f4655,plain,
( spl228_1
| ~ spl228_2 ),
inference(avatar_split_clause,[],[f2687,f4652,f4649]) ).
fof(f4679,plain,
! [X0] :
( finite1973466193nt_int(X0) = fFalse
| finite1973466193nt_int(X0) = fTrue ),
inference(resolution,[],[f4248,f2489]) ).
fof(f4695,plain,
( bot_bot_bool = fFalse
| bot_bot_bool = fTrue ),
inference(resolution,[],[f4248,f2505]) ).
fof(f4710,definition,
( spl228_3
<=> bot_bot_bool = fTrue ),
introduced(definition,[new_symbols(definition,[spl228_3])],[avatar_definition]) ).
fof(f4712,plain,
( bot_bot_bool = fTrue
| ~ spl228_3 ),
inference(avatar_component_clause,[],[f4710]) ).
fof(f4714,definition,
( spl228_4
<=> bot_bot_bool = fFalse ),
introduced(definition,[new_symbols(definition,[spl228_4])],[avatar_definition]) ).
fof(f4716,plain,
( bot_bot_bool = fFalse
| ~ spl228_4 ),
inference(avatar_component_clause,[],[f4714]) ).
fof(f4717,plain,
( spl228_3
| spl228_4 ),
inference(avatar_split_clause,[],[f4695,f4714,f4710]) ).
fof(f4721,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_H1037229737a_bool(X0,X1))
| bot_bo797238721a_bool != X0 ),
inference(forward_demodulation,[],[f2571,f2825]) ).
fof(f4741,plain,
( ! [X0] :
( finite1973466193nt_int(X0) = fFalse
| finite1973466193nt_int(X0) = bot_bot_bool )
| ~ spl228_3 ),
inference(forward_demodulation,[],[f4679,f4712]) ).
fof(f4773,plain,
( hBOOL(fFalse)
| bot_bot_bool = finite1973466193nt_int(times_times_int)
| ~ spl228_3 ),
inference(superposition,[],[f3336,f4741]) ).
fof(f4775,plain,
( bot_bot_bool = finite1973466193nt_int(times_times_int)
| ~ spl228_3 ),
inference(forward_subsumption_resolution,[],[f4773,f4247]) ).
fof(f4777,plain,
( hBOOL(bot_bot_bool)
| ~ spl228_3 ),
inference(superposition,[],[f3336,f4775]) ).
fof(f4779,plain,
( $false
| spl228_2
| ~ spl228_3 ),
inference(forward_subsumption_resolution,[],[f4777,f4654]) ).
fof(f4780,plain,
( spl228_2
| ~ spl228_3 ),
inference(avatar_contradiction_clause,[],[f4779]) ).
fof(f4781,plain,
( bot_bo797238721a_bool != bot_bo797238721a_bool
| ~ spl228_1 ),
inference(resolution,[],[f4650,f4721]) ).
fof(f4782,plain,
( $false
| ~ spl228_1 ),
inference(trivial_inequality_removal,[],[f4781]) ).
fof(f4783,plain,
~ spl228_1,
inference(avatar_contradiction_clause,[],[f4782]) ).
fof(f4916,plain,
! [X0] : fFalse = hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse),X0),
inference(resolution,[],[f4269,f2506]) ).
fof(f4929,plain,
( ! [X0] : bot_bot_bool = hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool),X0)
| ~ spl228_4 ),
inference(forward_demodulation,[],[f4916,f4716]) ).
fof(f5441,plain,
! [X0] : hAPP_H426895267a_bool(fequal963300192iple_a,X0) = hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,X0),bot_bo797238721a_bool),
inference(forward_demodulation,[],[f2550,f2825]) ).
fof(f5442,plain,
~ hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(g),hAPP_H426895267a_bool(fequal963300192iple_a,hoare_1916936827iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))))),
inference(superposition,[],[f4404,f5441]) ).
fof(f5451,plain,
( ~ hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(g),hAPP_H426895267a_bool(fequal963300192iple_a,hoare_1916936827iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b))))))
| ~ spl228_4 ),
inference(forward_demodulation,[],[f5442,f4716]) ).
fof(f34454,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(X0),hAPP_H426895267a_bool(fequal963300192iple_a,hoare_1916936827iple_a(X3,X1,X2))))
| hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,sK0(X0,X1,X2,X3)),sK1(X0,X1,X2,X3))) ),
inference(forward_demodulation,[],[f2528,f5441]) ).
fof(f34488,plain,
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)),sK0(g,c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)),hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)))),sK1(g,c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)),hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)))))
| ~ spl228_4 ),
inference(resolution,[],[f34454,f5451]) ).
fof(f34503,plain,
( hBOOL(hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool),sK1(g,c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)),hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)))))
| ~ spl228_4 ),
inference(forward_demodulation,[],[f34488,f4292]) ).
fof(f34534,plain,
( hBOOL(bot_bot_bool)
| ~ spl228_4 ),
inference(forward_demodulation,[],[f34503,f4929]) ).
fof(f34565,plain,
( $false
| spl228_2
| ~ spl228_4 ),
inference(forward_subsumption_resolution,[],[f34534,f4654]) ).
fof(f34566,plain,
( spl228_2
| ~ spl228_4 ),
inference(avatar_contradiction_clause,[],[f34565]) ).
cnf(s1,plain,
( spl228_1
| ~ spl228_2 ),
inference(sat_conversion,[],[f4655]) ).
cnf(s2,plain,
( spl228_3
| spl228_4 ),
inference(sat_conversion,[],[f4717]) ).
cnf(s4,plain,
( spl228_2
| ~ spl228_3 ),
inference(sat_conversion,[],[f4780]) ).
cnf(s5,plain,
~ spl228_1,
inference(sat_conversion,[],[f4783]) ).
cnf(s18,plain,
( spl228_2
| ~ spl228_4 ),
inference(sat_conversion,[],[f34566]) ).
cnf(s26,plain,
~ spl228_2,
inference(rat,[],[s1,s5]) ).
cnf(s27,plain,
~ spl228_4,
inference(rat,[],[s18,s26]) ).
cnf(s28,plain,
~ spl228_3,
inference(rat,[],[s4,s26]) ).
cnf(s29,plain,
$false,
inference(rat,[],[s2,s27,s28]) ).
fof(f34596,plain,
$false,
inference(avatar_sat_refutation,[],[s29]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW470+3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n007.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 14:00:29 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.37/2.39 % (2399625)Will run a generic schedule for satisfiability detection.
% 14.37/2.39 % (2399636)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=578576946:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.37/2.39 % (2399631)% WARNING: option uhcvi not known.
% 14.37/2.39 % (2399630)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=903671171_2999 on theBenchmark for (2999ds/0Mi)
% 14.37/2.39 % (2399633)dis+10_1_sil=32000:sp=arity:random_seed=3655436491:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.37/2.39 % (2399634)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2180100946:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.37/2.39 % (2399632)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1927968190:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.37/2.39 % (2399631)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=725752301:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.37/2.39 % (2399635)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=370694593:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.37/2.39 % (2399636)Instruction limit reached!
% 14.37/2.39 % (2399636)------------------------------
% 14.37/2.39 % (2399636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.37/2.39 % (2399636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.37/2.39 % (2399636)CaDiCaL version: 2.1.3
% 14.37/2.39 % (2399636)Termination reason: Instruction limit
% 14.37/2.39 % (2399636)Termination phase: Saturation
% 14.37/2.39 % (2399636)Time elapsed: 0.064 s
% 14.37/2.39 % (2399636)Peak memory usage: 16 MB
% 14.37/2.39 % (2399636)Instructions burned: 161 (million)
% 14.37/2.39 % (2399634)Instruction limit reached!
% 14.37/2.39 % (2399634)------------------------------
% 14.37/2.39 % (2399634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.37/2.39 % (2399634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.37/2.39 % (2399634)CaDiCaL version: 2.1.3
% 14.37/2.39 % (2399634)Termination reason: Instruction limit
% 14.37/2.39 % (2399634)Termination phase: Blocked clause elimination
% 14.37/2.39 % (2399634)Time elapsed: 0.066 s
% 14.37/2.39 % (2399634)Peak memory usage: 14 MB
% 14.37/2.39 % (2399634)Instructions burned: 116 (million)
% 14.37/2.39 % (2399651)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3123446871:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 14.37/2.39 % (2399633)Instruction limit reached!
% 14.37/2.39 % (2399633)------------------------------
% 14.37/2.39 % (2399633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.37/2.39 % (2399633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.37/2.39 % (2399633)CaDiCaL version: 2.1.3
% 14.37/2.39 % (2399633)Termination reason: Instruction limit
% 14.37/2.39 % (2399633)Termination phase: Saturation
% 14.37/2.39 % (2399633)Time elapsed: 0.081 s
% 14.37/2.39 % (2399633)Peak memory usage: 14 MB
% 14.37/2.39 % (2399633)Instructions burned: 103 (million)
% 14.37/2.39 % (2399652)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2397630955:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.37/2.39 % (2399635)Instruction limit reached!
% 14.37/2.39 % (2399635)------------------------------
% 14.37/2.39 % (2399635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.37/2.39 % (2399635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.37/2.39 % (2399635)CaDiCaL version: 2.1.3
% 14.37/2.39 % (2399635)Termination reason: Instruction limit
% 14.37/2.39 % (2399635)Termination phase: Saturation
% 14.37/2.39 % (2399635)Time elapsed: 0.108 s
% 14.37/2.39 % (2399635)Peak memory usage: 15 MB
% 14.37/2.39 % (2399635)Instructions burned: 132 (million)
% 14.37/2.39 % (2399654)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=3281147010:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.37/2.39 % (2399656)ott-21_1_sil=16000:fs=off:random_seed=1606910768:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.37/2.39 % (2399652)Instruction limit reached!
% 14.37/2.39 % (2399652)------------------------------
% 14.37/2.39 % (2399652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.37/2.39 % (2399652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.03/2.85 % (2399652)CaDiCaL version: 2.1.3
% 17.03/2.85 % (2399652)Termination reason: Instruction limit
% 17.03/2.85 % (2399652)Termination phase: Blocked clause elimination
% 17.03/2.85 % (2399652)Time elapsed: 0.103 s
% 17.03/2.85 % (2399652)Peak memory usage: 14 MB
% 17.03/2.85 % (2399652)Instructions burned: 131 (million)
% 17.03/2.85 % (2399661)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3470354887:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 17.03/2.85 % (2399656)Instruction limit reached!
% 17.03/2.85 % (2399656)------------------------------
% 17.03/2.85 % (2399656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.03/2.85 % (2399656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.03/2.85 % (2399656)CaDiCaL version: 2.1.3
% 17.03/2.85 % (2399656)Termination reason: Instruction limit
% 17.03/2.85 % (2399656)Termination phase: Saturation
% 17.03/2.85 % (2399656)Time elapsed: 0.143 s
% 17.03/2.85 % (2399656)Peak memory usage: 15 MB
% 17.03/2.85 % (2399656)Instructions burned: 180 (million)
% 17.03/2.85 % (2399669)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3032708063:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 17.03/2.85 % (2399651)Instruction limit reached!
% 17.03/2.85 % (2399651)------------------------------
% 17.03/2.85 % (2399651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.03/2.85 % (2399651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.03/2.85 % (2399651)CaDiCaL version: 2.1.3
% 17.03/2.85 % (2399651)Termination reason: Instruction limit
% 17.03/2.85 % (2399651)Termination phase: Finite model building preprocessing
% 17.03/2.85 % (2399651)Time elapsed: 0.281 s
% 17.03/2.85 % (2399651)Peak memory usage: 23 MB
% 17.03/2.85 % (2399651)Instructions burned: 716 (million)
% 17.03/2.85 % (2399671)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2035594601:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 17.03/2.85 % (2399661)Instruction limit reached!
% 17.03/2.85 % (2399661)------------------------------
% 17.03/2.85 % (2399661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.03/2.85 % (2399661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.03/2.85 % (2399661)CaDiCaL version: 2.1.3
% 17.03/2.85 % (2399661)Termination reason: Instruction limit
% 17.03/2.85 % (2399661)Termination phase: Saturation
% 17.03/2.85 % (2399661)Time elapsed: 0.449 s
% 17.03/2.85 % (2399661)Peak memory usage: 17 MB
% 17.03/2.85 % (2399661)Instructions burned: 478 (million)
% 17.03/2.85 % (2399654)Instruction limit reached!
% 17.03/2.85 % (2399654)------------------------------
% 17.03/2.85 % (2399654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.03/2.85 % (2399654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.03/2.85 % (2399654)CaDiCaL version: 2.1.3
% 17.03/2.85 % (2399654)Termination reason: Instruction limit
% 17.03/2.85 % (2399654)Termination phase: Saturation
% 17.03/2.85 % (2399654)Time elapsed: 0.590 s
% 17.03/2.85 % (2399654)Peak memory usage: 21 MB
% 17.03/2.85 % (2399654)Instructions burned: 685 (million)
% 17.03/2.85 % (2399680)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=877759195:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 17.03/2.85 % (2399681)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=2714493579:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi)
% 17.03/2.85 % (2399671)Instruction limit reached!
% 17.03/2.85 % (2399671)------------------------------
% 17.03/2.85 % (2399671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.03/2.85 % (2399671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.03/2.85 % (2399671)CaDiCaL version: 2.1.3
% 17.03/2.85 % (2399671)Termination reason: Instruction limit
% 17.03/2.85 % (2399671)Termination phase: Saturation
% 17.03/2.85 % (2399671)Time elapsed: 0.594 s
% 17.03/2.85 % (2399671)Peak memory usage: 27 MB
% 17.03/2.85 % (2399671)Instructions burned: 1180 (million)
% 17.03/2.85 % (2399686)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2718775644:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 17.03/2.85 % (2399669)Instruction limit reached!
% 17.03/2.85 % (2399669)------------------------------
% 17.03/2.85 % (2399669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.03/2.85 % (2399669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.03/2.85 % (2399669)CaDiCaL version: 2.1.3
% 17.03/2.85 % (2399669)Termination reason: Instruction limit
% 17.03/2.85 % (2399669)Termination phase: Finite model building preprocessing
% 17.03/2.85 % (2399669)Time elapsed: 0.769 s
% 17.03/2.85 % (2399669)Peak memory usage: 27 MB
% 17.03/2.85 % (2399669)Instructions burned: 865 (million)
% 17.03/2.85 % (2399689)fmb+10_1_sil=64000:random_seed=1700004334:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 17.03/2.85 % TRYING [1]
% 17.03/2.85 % TRYING [2]
% 17.03/2.85 % (2399686)Instruction limit reached!
% 17.03/2.85 % (2399686)------------------------------
% 17.03/2.85 % (2399686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.03/2.85 % (2399686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.03/2.85 % (2399686)CaDiCaL version: 2.1.3
% 17.03/2.85 % (2399686)Termination reason: Instruction limit
% 17.03/2.85 % (2399686)Termination phase: Saturation
% 17.03/2.85 % (2399686)Time elapsed: 0.265 s
% 17.03/2.85 % (2399686)Peak memory usage: 21 MB
% 17.03/2.85 % (2399686)Instructions burned: 882 (million)
% 17.03/2.85 % (2399691)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=547976692:i=9515:nm=5_2986 on theBenchmark for (2986ds/9515Mi)
% 17.03/2.85 % (2399680)Instruction limit reached!
% 17.03/2.85 % (2399680)------------------------------
% 17.03/2.85 % (2399680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.03/2.85 % (2399680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.03/2.85 % (2399680)CaDiCaL version: 2.1.3
% 17.03/2.85 % (2399680)Termination reason: Instruction limit
% 17.03/2.85 % (2399680)Termination phase: Finite model building preprocessing
% 17.03/2.85 % (2399680)Time elapsed: 0.574 s
% 17.03/2.85 % (2399680)Peak memory usage: 27 MB
% 17.03/2.85 % (2399680)Instructions burned: 889 (million)
% 17.03/2.85 % (2399693)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3672979141:fmbsr=1.7:i=920_2986 on theBenchmark for (2986ds/920Mi)
% 17.03/2.85 % (2399681)Instruction limit reached!
% 17.03/2.85 % (2399681)------------------------------
% 17.03/2.85 % (2399681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.03/2.85 % (2399681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.03/2.85 % (2399681)CaDiCaL version: 2.1.3
% 17.03/2.85 % (2399681)Termination reason: Instruction limit
% 17.03/2.85 % (2399681)Termination phase: Saturation
% 17.03/2.85 % (2399681)Time elapsed: 0.588 s
% 17.03/2.85 % (2399681)Peak memory usage: 23 MB
% 17.03/2.85 % (2399681)Instructions burned: 692 (million)
% 17.03/2.85 % (2399695)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=200818009:i=5131_2986 on theBenchmark for (2986ds/5131Mi)
% 17.03/2.85 % TRYING [3]
% 17.03/2.85 % (2399691)Cannot represent all propositional literals internally
% 17.03/2.85 % (2399691)Refutation not found, incomplete strategy
% 17.03/2.85 % (2399691)------------------------------
% 17.03/2.85 % (2399691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.03/2.85 % (2399691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.03/2.85 % (2399691)CaDiCaL version: 2.1.3
% 17.03/2.85 % (2399691)Termination reason: Refutation not found, incomplete strategy
% 17.03/2.85 % (2399691)Time elapsed: 0.388 s
% 17.03/2.85 % (2399691)Peak memory usage: 37 MB
% 17.03/2.85 % (2399691)Instructions burned: 1485 (million)
% 17.03/2.85 % (2399691)------------------------------
% 17.03/2.85 % (2399691)------------------------------
% 17.03/2.85 % (2399765)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3452173116:i=1472:ins=7:fdi=8:gsp=on_2982 on theBenchmark for (2982ds/1472Mi)
% 17.03/2.85 % (2399693)Instruction limit reached!
% 17.03/2.85 % (2399693)------------------------------
% 17.03/2.85 % (2399693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.03/2.85 % (2399693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.03/2.85 % (2399693)CaDiCaL version: 2.1.3
% 17.03/2.85 % (2399693)Termination reason: Instruction limit
% 17.03/2.85 % (2399693)Termination phase: Finite model building preprocessing
% 17.03/2.85 % (2399693)Time elapsed: 0.474 s
% 17.03/2.85 % (2399693)Peak memory usage: 27 MB
% 17.03/2.85 % (2399693)Instructions burned: 920 (million)
% 17.03/2.85 % TRYING [1]
% 17.03/2.85 % (2399804)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1993170541:i=6324_2981 on theBenchmark for (2981ds/6324Mi)
% 17.03/2.85 % TRYING [2]
% 17.03/2.85 % (2399765)Instruction limit reached!
% 17.03/2.85 % (2399765)------------------------------
% 17.03/2.85 % (2399765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.03/2.85 % (2399765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.03/2.85 % (2399765)CaDiCaL version: 2.1.3
% 17.03/2.85 % (2399765)Termination reason: Instruction limit
% 17.03/2.85 % (2399765)Termination phase: Saturation
% 17.03/2.85 % (2399765)Time elapsed: 0.439 s
% 17.03/2.85 % (2399765)Peak memory usage: 28 MB
% 17.03/2.85 % (2399765)Instructions burned: 1474 (million)
% 17.03/2.85 % (2399854)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2516389194:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 17.03/2.85 % (2399695) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2399625-2399695"...
% 17.03/2.85 % (2399695)...printing done.
% 17.03/2.85 % (2399695)Refutation found. Thanks to Tanya!
% 17.03/2.85 % SZS status Theorem for theBenchmark
% 17.03/2.85 % SZS output start Proof for theBenchmark
% See solution above
% 17.03/2.85 % (2399695)------------------------------
% 17.03/2.85 % (2399695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.03/2.85 % (2399695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.03/2.85 % (2399695)CaDiCaL version: 2.1.3
% 17.03/2.85 % (2399695)Termination reason: Refutation
% 17.03/2.85 % (2399695)Time elapsed: 1.186 s
% 17.03/2.85 % (2399695)Peak memory usage: 33 MB
% 17.03/2.85 % (2399695)Instructions burned: 2039 (million)
% 17.03/2.85 % (2399625)Success in time 2.617 s
% 17.03/2.85 % Vampire exiting
%------------------------------------------------------------------------------