%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR052+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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 09:44:41 AM UTC 2026
% Result : Theorem 221.28s 37.21s
% Output : Refutation 221.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 33
% Syntax : Number of formulae : 149 ( 53 unt; 23 def)
% Number of atoms : 318 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 314 ( 145 ~; 141 |; 2 &)
% ( 23 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 26 ( 25 usr; 24 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 11 con; 0-2 aty)
% Number of variables : 39 ( 0 sgn 39 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f19555,axiom,
genls(c_tptpcol_15_40430,c_tptpcol_14_40429),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+3.ax',ax3_19555) ).
fof(f20155,axiom,
genls(c_tptpcol_12_40420,c_tptpcol_11_40388),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+3.ax',ax3_20155) ).
fof(f23182,axiom,
genls(c_tptpcol_14_40429,c_tptpcol_13_40421),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+3.ax',ax3_23182) ).
fof(f25246,axiom,
genls(c_tptpcol_10_40324,c_tptpcol_9_40196),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+3.ax',ax3_25246) ).
fof(f25964,axiom,
genls(c_tptpcol_13_40421,c_tptpcol_12_40420),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+3.ax',ax3_25964) ).
fof(f25995,axiom,
genls(c_tptpcol_11_40388,c_tptpcol_10_40324),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+3.ax',ax3_25995) ).
fof(f27219,axiom,
genls(c_tptpcol_8_39940,c_tptpcol_7_39939),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+3.ax',ax3_27219) ).
fof(f28911,axiom,
genls(c_tptpcol_9_40196,c_tptpcol_8_39940),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+3.ax',ax3_28911) ).
fof(f44182,axiom,
! [X0,X1,X2] :
( ( genls(X0,X1)
& genls(X1,X2) )
=> genls(X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+3.ax',ax3_44182) ).
fof(f44217,conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml)),c_translation_33))
=> genls(c_tptpcol_15_40430,c_tptpcol_7_39939) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query202) ).
fof(f44218,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml)),c_translation_33))
=> genls(c_tptpcol_15_40430,c_tptpcol_7_39939) ),
inference(negated_conjecture,[status(cth)],[f44217]) ).
fof(f66300,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X0,X1)
| ~ genls(X1,X2) ),
inference(ennf_transformation,[],[f44182]) ).
fof(f66301,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X0,X1)
| ~ genls(X1,X2) ),
inference(flattening,[],[f66300]) ).
fof(f66315,plain,
( ~ genls(c_tptpcol_15_40430,c_tptpcol_7_39939)
& mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml)),c_translation_33)) ),
inference(ennf_transformation,[],[f44218]) ).
fof(f85502,plain,
genls(c_tptpcol_15_40430,c_tptpcol_14_40429),
inference(cnf_transformation,[],[f19555]) ).
fof(f86091,plain,
genls(c_tptpcol_12_40420,c_tptpcol_11_40388),
inference(cnf_transformation,[],[f20155]) ).
fof(f89052,plain,
genls(c_tptpcol_14_40429,c_tptpcol_13_40421),
inference(cnf_transformation,[],[f23182]) ).
fof(f91080,plain,
genls(c_tptpcol_10_40324,c_tptpcol_9_40196),
inference(cnf_transformation,[],[f25246]) ).
fof(f91784,plain,
genls(c_tptpcol_13_40421,c_tptpcol_12_40420),
inference(cnf_transformation,[],[f25964]) ).
fof(f91815,plain,
genls(c_tptpcol_11_40388,c_tptpcol_10_40324),
inference(cnf_transformation,[],[f25995]) ).
fof(f93016,plain,
genls(c_tptpcol_8_39940,c_tptpcol_7_39939),
inference(cnf_transformation,[],[f27219]) ).
fof(f94671,plain,
genls(c_tptpcol_9_40196,c_tptpcol_8_39940),
inference(cnf_transformation,[],[f28911]) ).
fof(f108024,plain,
! [X2,X0,X1] :
( genls(X0,X2)
| ~ genls(X0,X1)
| ~ genls(X1,X2) ),
inference(cnf_transformation,[],[f66301]) ).
fof(f108043,plain,
~ genls(c_tptpcol_15_40430,c_tptpcol_7_39939),
inference(cnf_transformation,[],[f66315]) ).
fof(f108055,definition,
( spl0_2
<=> genls(c_tptpcol_15_40430,c_tptpcol_7_39939) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f108057,plain,
( ~ genls(c_tptpcol_15_40430,c_tptpcol_7_39939)
| spl0_2 ),
inference(avatar_component_clause,[],[f108055]) ).
fof(f108058,plain,
~ spl0_2,
inference(avatar_split_clause,[],[f108043,f108055]) ).
fof(f108163,definition,
( spl0_32
<=> ! [X2,X0,X1] :
( genls(X0,X2)
| ~ genls(X0,X1)
| ~ genls(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f108164,plain,
( ! [X2,X0,X1] :
( ~ genls(X1,X2)
| ~ genls(X0,X1)
| genls(X0,X2) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f108163]) ).
fof(f108165,plain,
spl0_32,
inference(avatar_split_clause,[],[f108024,f108163]) ).
fof(f231241,definition,
( spl0_36371
<=> genls(c_tptpcol_9_40196,c_tptpcol_8_39940) ),
introduced(definition,[new_symbols(definition,[spl0_36371])],[avatar_definition]) ).
fof(f231243,plain,
( genls(c_tptpcol_9_40196,c_tptpcol_8_39940)
| ~ spl0_36371 ),
inference(avatar_component_clause,[],[f231241]) ).
fof(f231244,plain,
spl0_36371,
inference(avatar_split_clause,[],[f94671,f231241]) ).
fof(f239274,definition,
( spl0_38049
<=> genls(c_tptpcol_8_39940,c_tptpcol_7_39939) ),
introduced(definition,[new_symbols(definition,[spl0_38049])],[avatar_definition]) ).
fof(f239276,plain,
( genls(c_tptpcol_8_39940,c_tptpcol_7_39939)
| ~ spl0_38049 ),
inference(avatar_component_clause,[],[f239274]) ).
fof(f239277,plain,
spl0_38049,
inference(avatar_split_clause,[],[f93016,f239274]) ).
fof(f245092,definition,
( spl0_39258
<=> genls(c_tptpcol_11_40388,c_tptpcol_10_40324) ),
introduced(definition,[new_symbols(definition,[spl0_39258])],[avatar_definition]) ).
fof(f245094,plain,
( genls(c_tptpcol_11_40388,c_tptpcol_10_40324)
| ~ spl0_39258 ),
inference(avatar_component_clause,[],[f245092]) ).
fof(f245095,plain,
spl0_39258,
inference(avatar_split_clause,[],[f91815,f245092]) ).
fof(f245240,definition,
( spl0_39289
<=> genls(c_tptpcol_13_40421,c_tptpcol_12_40420) ),
introduced(definition,[new_symbols(definition,[spl0_39289])],[avatar_definition]) ).
fof(f245242,plain,
( genls(c_tptpcol_13_40421,c_tptpcol_12_40420)
| ~ spl0_39289 ),
inference(avatar_component_clause,[],[f245240]) ).
fof(f245243,plain,
spl0_39289,
inference(avatar_split_clause,[],[f91784,f245240]) ).
fof(f248625,definition,
( spl0_39994
<=> genls(c_tptpcol_10_40324,c_tptpcol_9_40196) ),
introduced(definition,[new_symbols(definition,[spl0_39994])],[avatar_definition]) ).
fof(f248627,plain,
( genls(c_tptpcol_10_40324,c_tptpcol_9_40196)
| ~ spl0_39994 ),
inference(avatar_component_clause,[],[f248625]) ).
fof(f248628,plain,
spl0_39994,
inference(avatar_split_clause,[],[f91080,f248625]) ).
fof(f258371,definition,
( spl0_42027
<=> genls(c_tptpcol_14_40429,c_tptpcol_13_40421) ),
introduced(definition,[new_symbols(definition,[spl0_42027])],[avatar_definition]) ).
fof(f258373,plain,
( genls(c_tptpcol_14_40429,c_tptpcol_13_40421)
| ~ spl0_42027 ),
inference(avatar_component_clause,[],[f258371]) ).
fof(f258374,plain,
spl0_42027,
inference(avatar_split_clause,[],[f89052,f258371]) ).
fof(f272443,definition,
( spl0_44960
<=> genls(c_tptpcol_12_40420,c_tptpcol_11_40388) ),
introduced(definition,[new_symbols(definition,[spl0_44960])],[avatar_definition]) ).
fof(f272445,plain,
( genls(c_tptpcol_12_40420,c_tptpcol_11_40388)
| ~ spl0_44960 ),
inference(avatar_component_clause,[],[f272443]) ).
fof(f272446,plain,
spl0_44960,
inference(avatar_split_clause,[],[f86091,f272443]) ).
fof(f275276,definition,
( spl0_45553
<=> genls(c_tptpcol_15_40430,c_tptpcol_14_40429) ),
introduced(definition,[new_symbols(definition,[spl0_45553])],[avatar_definition]) ).
fof(f275278,plain,
( genls(c_tptpcol_15_40430,c_tptpcol_14_40429)
| ~ spl0_45553 ),
inference(avatar_component_clause,[],[f275276]) ).
fof(f275279,plain,
spl0_45553,
inference(avatar_split_clause,[],[f85502,f275276]) ).
fof(f472587,plain,
( ! [X0] :
( ~ genls(X0,c_tptpcol_8_39940)
| genls(X0,c_tptpcol_7_39939) )
| ~ spl0_32
| ~ spl0_38049 ),
inference(resolution,[],[f108164,f239276]) ).
fof(f472606,definition,
( spl0_63969
<=> ! [X0] :
( ~ genls(X0,c_tptpcol_8_39940)
| genls(X0,c_tptpcol_7_39939) ) ),
introduced(definition,[new_symbols(definition,[spl0_63969])],[avatar_definition]) ).
fof(f472607,plain,
( ! [X0] :
( ~ genls(X0,c_tptpcol_8_39940)
| genls(X0,c_tptpcol_7_39939) )
| ~ spl0_63969 ),
inference(avatar_component_clause,[],[f472606]) ).
fof(f472608,plain,
( spl0_63969
| ~ spl0_32
| ~ spl0_38049 ),
inference(avatar_split_clause,[],[f472587,f239274,f108163,f472606]) ).
fof(f472633,plain,
( ! [X0] :
( ~ genls(X0,c_tptpcol_14_40429)
| genls(X0,c_tptpcol_13_40421) )
| ~ spl0_32
| ~ spl0_42027 ),
inference(resolution,[],[f258373,f108164]) ).
fof(f472643,definition,
( spl0_63975
<=> ! [X0] :
( ~ genls(X0,c_tptpcol_14_40429)
| genls(X0,c_tptpcol_13_40421) ) ),
introduced(definition,[new_symbols(definition,[spl0_63975])],[avatar_definition]) ).
fof(f472644,plain,
( ! [X0] :
( ~ genls(X0,c_tptpcol_14_40429)
| genls(X0,c_tptpcol_13_40421) )
| ~ spl0_63975 ),
inference(avatar_component_clause,[],[f472643]) ).
fof(f472645,plain,
( spl0_63975
| ~ spl0_32
| ~ spl0_42027 ),
inference(avatar_split_clause,[],[f472633,f258371,f108163,f472643]) ).
fof(f472674,plain,
( genls(c_tptpcol_9_40196,c_tptpcol_7_39939)
| ~ spl0_36371
| ~ spl0_63969 ),
inference(resolution,[],[f472607,f231243]) ).
fof(f472676,definition,
( spl0_63980
<=> genls(c_tptpcol_9_40196,c_tptpcol_7_39939) ),
introduced(definition,[new_symbols(definition,[spl0_63980])],[avatar_definition]) ).
fof(f472678,plain,
( genls(c_tptpcol_9_40196,c_tptpcol_7_39939)
| ~ spl0_63980 ),
inference(avatar_component_clause,[],[f472676]) ).
fof(f472679,plain,
( spl0_63980
| ~ spl0_36371
| ~ spl0_63969 ),
inference(avatar_split_clause,[],[f472674,f472606,f231241,f472676]) ).
fof(f481681,plain,
( ! [X0] :
( ~ genls(X0,c_tptpcol_13_40421)
| genls(X0,c_tptpcol_12_40420) )
| ~ spl0_32
| ~ spl0_39289 ),
inference(resolution,[],[f245242,f108164]) ).
fof(f481691,definition,
( spl0_64008
<=> ! [X0] :
( ~ genls(X0,c_tptpcol_13_40421)
| genls(X0,c_tptpcol_12_40420) ) ),
introduced(definition,[new_symbols(definition,[spl0_64008])],[avatar_definition]) ).
fof(f481692,plain,
( ! [X0] :
( ~ genls(X0,c_tptpcol_13_40421)
| genls(X0,c_tptpcol_12_40420) )
| ~ spl0_64008 ),
inference(avatar_component_clause,[],[f481691]) ).
fof(f481693,plain,
( spl0_64008
| ~ spl0_32
| ~ spl0_39289 ),
inference(avatar_split_clause,[],[f481681,f245240,f108163,f481691]) ).
fof(f481701,plain,
( ! [X0] :
( ~ genls(X0,c_tptpcol_10_40324)
| genls(X0,c_tptpcol_9_40196) )
| ~ spl0_32
| ~ spl0_39994 ),
inference(resolution,[],[f248627,f108164]) ).
fof(f481709,definition,
( spl0_64011
<=> ! [X0] :
( ~ genls(X0,c_tptpcol_10_40324)
| genls(X0,c_tptpcol_9_40196) ) ),
introduced(definition,[new_symbols(definition,[spl0_64011])],[avatar_definition]) ).
fof(f481710,plain,
( ! [X0] :
( ~ genls(X0,c_tptpcol_10_40324)
| genls(X0,c_tptpcol_9_40196) )
| ~ spl0_64011 ),
inference(avatar_component_clause,[],[f481709]) ).
fof(f481711,plain,
( spl0_64011
| ~ spl0_32
| ~ spl0_39994 ),
inference(avatar_split_clause,[],[f481701,f248625,f108163,f481709]) ).
fof(f481718,plain,
( ! [X0] :
( ~ genls(X0,c_tptpcol_9_40196)
| genls(X0,c_tptpcol_7_39939) )
| ~ spl0_32
| ~ spl0_63980 ),
inference(resolution,[],[f472678,f108164]) ).
fof(f481720,definition,
( spl0_64012
<=> ! [X0] :
( ~ genls(X0,c_tptpcol_9_40196)
| genls(X0,c_tptpcol_7_39939) ) ),
introduced(definition,[new_symbols(definition,[spl0_64012])],[avatar_definition]) ).
fof(f481721,plain,
( ! [X0] :
( ~ genls(X0,c_tptpcol_9_40196)
| genls(X0,c_tptpcol_7_39939) )
| ~ spl0_64012 ),
inference(avatar_component_clause,[],[f481720]) ).
fof(f481722,plain,
( spl0_64012
| ~ spl0_32
| ~ spl0_63980 ),
inference(avatar_split_clause,[],[f481718,f472676,f108163,f481720]) ).
fof(f481760,plain,
( ! [X0] :
( ~ genls(X0,c_tptpcol_11_40388)
| genls(X0,c_tptpcol_10_40324) )
| ~ spl0_32
| ~ spl0_39258 ),
inference(resolution,[],[f245094,f108164]) ).
fof(f481768,definition,
( spl0_64020
<=> ! [X0] :
( ~ genls(X0,c_tptpcol_11_40388)
| genls(X0,c_tptpcol_10_40324) ) ),
introduced(definition,[new_symbols(definition,[spl0_64020])],[avatar_definition]) ).
fof(f481769,plain,
( ! [X0] :
( ~ genls(X0,c_tptpcol_11_40388)
| genls(X0,c_tptpcol_10_40324) )
| ~ spl0_64020 ),
inference(avatar_component_clause,[],[f481768]) ).
fof(f481770,plain,
( spl0_64020
| ~ spl0_32
| ~ spl0_39258 ),
inference(avatar_split_clause,[],[f481760,f245092,f108163,f481768]) ).
fof(f481777,plain,
( ! [X0] :
( ~ genls(X0,c_tptpcol_12_40420)
| genls(X0,c_tptpcol_11_40388) )
| ~ spl0_32
| ~ spl0_44960 ),
inference(resolution,[],[f272445,f108164]) ).
fof(f481787,definition,
( spl0_64023
<=> ! [X0] :
( ~ genls(X0,c_tptpcol_12_40420)
| genls(X0,c_tptpcol_11_40388) ) ),
introduced(definition,[new_symbols(definition,[spl0_64023])],[avatar_definition]) ).
fof(f481788,plain,
( ! [X0] :
( ~ genls(X0,c_tptpcol_12_40420)
| genls(X0,c_tptpcol_11_40388) )
| ~ spl0_64023 ),
inference(avatar_component_clause,[],[f481787]) ).
fof(f481789,plain,
( spl0_64023
| ~ spl0_32
| ~ spl0_44960 ),
inference(avatar_split_clause,[],[f481777,f272443,f108163,f481787]) ).
fof(f481852,plain,
( genls(c_tptpcol_15_40430,c_tptpcol_13_40421)
| ~ spl0_45553
| ~ spl0_63975 ),
inference(resolution,[],[f472644,f275278]) ).
fof(f481854,definition,
( spl0_64033
<=> genls(c_tptpcol_15_40430,c_tptpcol_13_40421) ),
introduced(definition,[new_symbols(definition,[spl0_64033])],[avatar_definition]) ).
fof(f481856,plain,
( genls(c_tptpcol_15_40430,c_tptpcol_13_40421)
| ~ spl0_64033 ),
inference(avatar_component_clause,[],[f481854]) ).
fof(f481857,plain,
( spl0_64033
| ~ spl0_45553
| ~ spl0_63975 ),
inference(avatar_split_clause,[],[f481852,f472643,f275276,f481854]) ).
fof(f482618,plain,
( genls(c_tptpcol_15_40430,c_tptpcol_12_40420)
| ~ spl0_64008
| ~ spl0_64033 ),
inference(resolution,[],[f481692,f481856]) ).
fof(f482626,definition,
( spl0_64182
<=> genls(c_tptpcol_15_40430,c_tptpcol_12_40420) ),
introduced(definition,[new_symbols(definition,[spl0_64182])],[avatar_definition]) ).
fof(f482628,plain,
( genls(c_tptpcol_15_40430,c_tptpcol_12_40420)
| ~ spl0_64182 ),
inference(avatar_component_clause,[],[f482626]) ).
fof(f482629,plain,
( spl0_64182
| ~ spl0_64008
| ~ spl0_64033 ),
inference(avatar_split_clause,[],[f482618,f481854,f481691,f482626]) ).
fof(f483124,plain,
( genls(c_tptpcol_15_40430,c_tptpcol_11_40388)
| ~ spl0_64023
| ~ spl0_64182 ),
inference(resolution,[],[f481788,f482628]) ).
fof(f483138,definition,
( spl0_64276
<=> genls(c_tptpcol_15_40430,c_tptpcol_11_40388) ),
introduced(definition,[new_symbols(definition,[spl0_64276])],[avatar_definition]) ).
fof(f483140,plain,
( genls(c_tptpcol_15_40430,c_tptpcol_11_40388)
| ~ spl0_64276 ),
inference(avatar_component_clause,[],[f483138]) ).
fof(f483141,plain,
( spl0_64276
| ~ spl0_64023
| ~ spl0_64182 ),
inference(avatar_split_clause,[],[f483124,f482626,f481787,f483138]) ).
fof(f483174,plain,
( genls(c_tptpcol_15_40430,c_tptpcol_10_40324)
| ~ spl0_64020
| ~ spl0_64276 ),
inference(resolution,[],[f483140,f481769]) ).
fof(f483177,definition,
( spl0_64283
<=> genls(c_tptpcol_15_40430,c_tptpcol_10_40324) ),
introduced(definition,[new_symbols(definition,[spl0_64283])],[avatar_definition]) ).
fof(f483179,plain,
( genls(c_tptpcol_15_40430,c_tptpcol_10_40324)
| ~ spl0_64283 ),
inference(avatar_component_clause,[],[f483177]) ).
fof(f483180,plain,
( spl0_64283
| ~ spl0_64020
| ~ spl0_64276 ),
inference(avatar_split_clause,[],[f483174,f483138,f481768,f483177]) ).
fof(f483213,plain,
( genls(c_tptpcol_15_40430,c_tptpcol_9_40196)
| ~ spl0_64011
| ~ spl0_64283 ),
inference(resolution,[],[f483179,f481710]) ).
fof(f483216,definition,
( spl0_64290
<=> genls(c_tptpcol_15_40430,c_tptpcol_9_40196) ),
introduced(definition,[new_symbols(definition,[spl0_64290])],[avatar_definition]) ).
fof(f483218,plain,
( genls(c_tptpcol_15_40430,c_tptpcol_9_40196)
| ~ spl0_64290 ),
inference(avatar_component_clause,[],[f483216]) ).
fof(f483219,plain,
( spl0_64290
| ~ spl0_64011
| ~ spl0_64283 ),
inference(avatar_split_clause,[],[f483213,f483177,f481709,f483216]) ).
fof(f483264,plain,
( genls(c_tptpcol_15_40430,c_tptpcol_7_39939)
| ~ spl0_64012
| ~ spl0_64290 ),
inference(resolution,[],[f483218,f481721]) ).
fof(f483272,plain,
( $false
| spl0_2
| ~ spl0_64012
| ~ spl0_64290 ),
inference(forward_subsumption_resolution,[],[f483264,f108057]) ).
fof(f483273,plain,
( spl0_2
| ~ spl0_64012
| ~ spl0_64290 ),
inference(avatar_contradiction_clause,[],[f483272]) ).
cnf(s2,plain,
~ spl0_2,
inference(sat_conversion,[],[f108058]) ).
cnf(s20,plain,
spl0_32,
inference(sat_conversion,[],[f108165]) ).
cnf(s13370,plain,
spl0_36371,
inference(sat_conversion,[],[f231244]) ).
cnf(s15025,plain,
spl0_38049,
inference(sat_conversion,[],[f239277]) ).
cnf(s16226,plain,
spl0_39258,
inference(sat_conversion,[],[f245095]) ).
cnf(s16257,plain,
spl0_39289,
inference(sat_conversion,[],[f245243]) ).
cnf(s16961,plain,
spl0_39994,
inference(sat_conversion,[],[f248628]) ).
cnf(s18989,plain,
spl0_42027,
inference(sat_conversion,[],[f258374]) ).
cnf(s21950,plain,
spl0_44960,
inference(sat_conversion,[],[f272446]) ).
cnf(s22539,plain,
spl0_45553,
inference(sat_conversion,[],[f275279]) ).
cnf(s90214,plain,
( ~ spl0_32
| ~ spl0_38049
| spl0_63969 ),
inference(sat_conversion,[],[f472608]) ).
cnf(s90223,plain,
( ~ spl0_32
| ~ spl0_42027
| spl0_63975 ),
inference(sat_conversion,[],[f472645]) ).
cnf(s90230,plain,
( ~ spl0_36371
| ~ spl0_63969
| spl0_63980 ),
inference(sat_conversion,[],[f472679]) ).
cnf(s94688,plain,
( ~ spl0_32
| ~ spl0_39289
| spl0_64008 ),
inference(sat_conversion,[],[f481693]) ).
cnf(s94692,plain,
( ~ spl0_32
| ~ spl0_39994
| spl0_64011 ),
inference(sat_conversion,[],[f481711]) ).
cnf(s94696,plain,
( ~ spl0_32
| ~ spl0_63980
| spl0_64012 ),
inference(sat_conversion,[],[f481722]) ).
cnf(s94703,plain,
( ~ spl0_32
| ~ spl0_39258
| spl0_64020 ),
inference(sat_conversion,[],[f481770]) ).
cnf(s94708,plain,
( ~ spl0_32
| ~ spl0_44960
| spl0_64023 ),
inference(sat_conversion,[],[f481789]) ).
cnf(s94723,plain,
( ~ spl0_45553
| ~ spl0_63975
| spl0_64033 ),
inference(sat_conversion,[],[f481857]) ).
cnf(s94879,plain,
( ~ spl0_64008
| ~ spl0_64033
| spl0_64182 ),
inference(sat_conversion,[],[f482629]) ).
cnf(s94981,plain,
( ~ spl0_64023
| ~ spl0_64182
| spl0_64276 ),
inference(sat_conversion,[],[f483141]) ).
cnf(s94988,plain,
( ~ spl0_64020
| ~ spl0_64276
| spl0_64283 ),
inference(sat_conversion,[],[f483180]) ).
cnf(s94995,plain,
( ~ spl0_64011
| ~ spl0_64283
| spl0_64290 ),
inference(sat_conversion,[],[f483219]) ).
cnf(s95005,plain,
( spl0_2
| ~ spl0_64012
| ~ spl0_64290 ),
inference(sat_conversion,[],[f483273]) ).
cnf(s96133,plain,
spl0_64023,
inference(rat,[],[s94708,s21950,s20]) ).
cnf(s96134,plain,
spl0_64020,
inference(rat,[],[s94703,s16226,s20]) ).
cnf(s96135,plain,
spl0_64011,
inference(rat,[],[s94692,s16961,s20]) ).
cnf(s96136,plain,
spl0_64008,
inference(rat,[],[s94688,s16257,s20]) ).
cnf(s96137,plain,
spl0_63975,
inference(rat,[],[s90223,s18989,s20]) ).
cnf(s96139,plain,
spl0_63969,
inference(rat,[],[s90214,s15025,s20]) ).
cnf(s96145,plain,
spl0_64033,
inference(rat,[],[s94723,s22539,s96137]) ).
cnf(s96147,plain,
spl0_63980,
inference(rat,[],[s90230,s13370,s96139]) ).
cnf(s96158,plain,
spl0_64182,
inference(rat,[],[s94879,s96136,s96145]) ).
cnf(s96162,plain,
spl0_64012,
inference(rat,[],[s94696,s20,s96147]) ).
cnf(s96173,plain,
spl0_64276,
inference(rat,[],[s94981,s96133,s96158]) ).
cnf(s96185,plain,
spl0_64283,
inference(rat,[],[s94988,s96134,s96173]) ).
cnf(s96191,plain,
spl0_64290,
inference(rat,[],[s94995,s96135,s96185]) ).
cnf(s96193,plain,
spl0_2,
inference(rat,[],[s95005,s96162,s96191]) ).
cnf(s96209,plain,
$false,
inference(rat,[],[s2,s96193]) ).
fof(f483274,plain,
$false,
inference(avatar_sat_refutation,[],[s96209]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR052+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.04/0.12 % Computer : n012.cluster.edu
% 0.04/0.12 % Model : x86_64 x86_64
% 0.04/0.12 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.12 % Memory : 8046.5625MB
% 0.04/0.12 % OS : Linux 6.8.0-71-generic
% 0.04/0.12 % CPULimit : 300
% 0.04/0.12 % WCLimit : 300
% 0.04/0.12 % DateTime : Mon Sep 28 22:18:19 UTC 2026
% 0.04/0.12 % CPUTime :
% 0.04/0.12 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.04/0.13 Running first-order model finding
% 0.04/0.13 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
% 16.33/2.97 % (3855748)Will run a generic schedule for satisfiability detection.
% 16.33/2.97 % (3855754)% WARNING: option uhcvi not known.
% 16.33/2.97 % (3855754)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=350205642:i=135531:add=off:rawr=on_2996 on theBenchmark for (2996ds/135531Mi)
% 16.33/2.97 % (3855755)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1195341744:i=88024:add=on:rawr=on_2996 on theBenchmark for (2996ds/88024Mi)
% 16.33/2.97 % (3855753)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=877196858_2996 on theBenchmark for (2996ds/0Mi)
% 16.33/2.97 % (3855756)dis+10_1_sil=32000:sp=arity:random_seed=3069502066:i=103:fgj=on_2996 on theBenchmark for (2996ds/103Mi)
% 16.33/2.97 % (3855757)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4116250565:i=116_2996 on theBenchmark for (2996ds/116Mi)
% 16.33/2.97 % (3855758)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=216614312:i=131_2996 on theBenchmark for (2996ds/131Mi)
% 16.33/2.97 % (3855759)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4139905585:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2996 on theBenchmark for (2996ds/159Mi)
% 16.33/2.97 % (3855756)Instruction limit reached!
% 16.33/2.97 % (3855756)------------------------------
% 16.33/2.97 % (3855756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.33/2.97 % (3855756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.33/2.97 % (3855756)CaDiCaL version: 2.1.3
% 16.33/2.97 % (3855756)Termination reason: Instruction limit
% 16.33/2.97 % (3855756)Termination phase: Preprocessing 2
% 16.33/2.97 % (3855756)Time elapsed: 0.058 s
% 16.33/2.97 % (3855756)Peak memory usage: 61 MB
% 16.33/2.97 % (3855756)Instructions burned: 104 (million)
% 16.33/2.97 % (3855757)Instruction limit reached!
% 16.33/2.97 % (3855757)------------------------------
% 16.33/2.97 % (3855757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.33/2.97 % (3855757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.33/2.97 % (3855757)CaDiCaL version: 2.1.3
% 16.33/2.97 % (3855757)Termination reason: Instruction limit
% 16.33/2.97 % (3855757)Termination phase: Preprocessing 2
% 16.33/2.97 % (3855757)Time elapsed: 0.068 s
% 16.33/2.97 % (3855757)Peak memory usage: 61 MB
% 16.33/2.97 % (3855757)Instructions burned: 117 (million)
% 16.33/2.97 % (3855758)Instruction limit reached!
% 16.33/2.97 % (3855758)------------------------------
% 16.33/2.97 % (3855758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.33/2.97 % (3855758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.33/2.97 % (3855758)CaDiCaL version: 2.1.3
% 16.33/2.97 % (3855758)Termination reason: Instruction limit
% 16.33/2.97 % (3855758)Termination phase: Preprocessing 2
% 16.33/2.97 % (3855758)Time elapsed: 0.070 s
% 16.33/2.97 % (3855758)Peak memory usage: 61 MB
% 16.33/2.97 % (3855758)Instructions burned: 131 (million)
% 16.33/2.97 % (3855767)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4242825235:i=714:nm=2_2995 on theBenchmark for (2995ds/714Mi)
% 16.33/2.97 % (3855759)Instruction limit reached!
% 16.33/2.97 % (3855759)------------------------------
% 16.33/2.97 % (3855759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.33/2.97 % (3855759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.33/2.97 % (3855759)CaDiCaL version: 2.1.3
% 16.33/2.97 % (3855759)Termination reason: Instruction limit
% 16.33/2.97 % (3855759)Termination phase: Naming
% 16.33/2.97 % (3855759)Time elapsed: 0.079 s
% 16.33/2.97 % (3855759)Peak memory usage: 62 MB
% 16.33/2.97 % (3855759)Instructions burned: 163 (million)
% 16.33/2.97 % (3855768)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1009760126:i=131:bd=preordered:fsd=on_2995 on theBenchmark for (2995ds/131Mi)
% 16.33/2.97 % (3855769)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=938668284:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2995 on theBenchmark for (2995ds/684Mi)
% 16.33/2.97 % (3855773)ott-21_1_sil=16000:fs=off:random_seed=861105117:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 16.33/2.97 % (3855768)Instruction limit reached!
% 16.33/2.97 % (3855768)------------------------------
% 16.33/2.97 % (3855768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.33/2.97 % (3855768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.24/5.27 % (3855768)CaDiCaL version: 2.1.3
% 33.24/5.27 % (3855768)Termination reason: Instruction limit
% 33.24/5.27 % (3855768)Termination phase: Preprocessing 2
% 33.24/5.27 % (3855768)Time elapsed: 0.068 s
% 33.24/5.27 % (3855768)Peak memory usage: 61 MB
% 33.24/5.27 % (3855768)Instructions burned: 132 (million)
% 33.24/5.27 % (3855775)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2963682570:i=477:bd=all_2994 on theBenchmark for (2994ds/477Mi)
% 33.24/5.27 % (3855773)Instruction limit reached!
% 33.24/5.27 % (3855773)------------------------------
% 33.24/5.27 % (3855773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.24/5.27 % (3855773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.24/5.27 % (3855773)CaDiCaL version: 2.1.3
% 33.24/5.27 % (3855773)Termination reason: Instruction limit
% 33.24/5.27 % (3855773)Termination phase: Preprocessing 3
% 33.24/5.27 % (3855773)Time elapsed: 0.082 s
% 33.24/5.27 % (3855773)Peak memory usage: 62 MB
% 33.24/5.27 % (3855773)Instructions burned: 184 (million)
% 33.24/5.27 % (3855777)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3287269410:fmbsr=1.3:i=865:ins=25_2994 on theBenchmark for (2994ds/865Mi)
% 33.24/5.27 % (3855767)Instruction limit reached!
% 33.24/5.27 % (3855767)------------------------------
% 33.24/5.27 % (3855767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.24/5.27 % (3855767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.24/5.27 % (3855767)CaDiCaL version: 2.1.3
% 33.24/5.27 % (3855767)Termination reason: Instruction limit
% 33.24/5.27 % (3855767)Termination phase: Finite model building preprocessing
% 33.24/5.27 % (3855767)Time elapsed: 0.253 s
% 33.24/5.27 % (3855767)Peak memory usage: 68 MB
% 33.24/5.27 % (3855767)Instructions burned: 716 (million)
% 33.24/5.27 % (3855775)Instruction limit reached!
% 33.24/5.27 % (3855775)------------------------------
% 33.24/5.27 % (3855775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.24/5.27 % (3855775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.24/5.27 % (3855775)CaDiCaL version: 2.1.3
% 33.24/5.27 % (3855775)Termination reason: Instruction limit
% 33.24/5.27 % (3855775)Termination phase: Property scanning
% 33.24/5.27 % (3855775)Time elapsed: 0.176 s
% 33.24/5.27 % (3855775)Peak memory usage: 66 MB
% 33.24/5.27 % (3855775)Instructions burned: 480 (million)
% 33.24/5.27 % (3855779)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2423742766:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 33.24/5.27 % (3855769)Instruction limit reached!
% 33.24/5.27 % (3855769)------------------------------
% 33.24/5.27 % (3855769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.24/5.27 % (3855769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.24/5.27 % (3855769)CaDiCaL version: 2.1.3
% 33.24/5.27 % (3855769)Termination reason: Instruction limit
% 33.24/5.27 % (3855769)Termination phase: Property scanning
% 33.24/5.27 % (3855769)Time elapsed: 0.269 s
% 33.24/5.27 % (3855769)Peak memory usage: 73 MB
% 33.24/5.27 % (3855769)Instructions burned: 687 (million)
% 33.24/5.27 % (3855781)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2404674860:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 33.24/5.27 % (3855782)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=176375196: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)
% 33.24/5.27 % (3855777)Instruction limit reached!
% 33.24/5.27 % (3855777)------------------------------
% 33.24/5.27 % (3855777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.24/5.27 % (3855777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.24/5.27 % (3855777)CaDiCaL version: 2.1.3
% 33.24/5.27 % (3855777)Termination reason: Instruction limit
% 33.24/5.27 % (3855777)Termination phase: Finite model building preprocessing
% 33.24/5.27 % (3855777)Time elapsed: 0.304 s
% 33.24/5.27 % (3855777)Peak memory usage: 86 MB
% 33.24/5.27 % (3855777)Instructions burned: 865 (million)
% 33.24/5.27 % (3855785)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=936663403:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 33.24/5.27 % (3855782)Instruction limit reached!
% 33.24/5.27 % (3855782)------------------------------
% 33.24/5.27 % (3855782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.24/5.27 % (3855782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/9.79 % (3855782)CaDiCaL version: 2.1.3
% 65.07/9.79 % (3855782)Termination reason: Instruction limit
% 65.07/9.79 % (3855782)Termination phase: Property scanning
% 65.07/9.79 % (3855782)Time elapsed: 0.276 s
% 65.07/9.79 % (3855782)Peak memory usage: 75 MB
% 65.07/9.79 % (3855782)Instructions burned: 696 (million)
% 65.07/9.79 % (3855787)fmb+10_1_sil=64000:random_seed=1486696697:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 65.07/9.79 % (3855781)Instruction limit reached!
% 65.07/9.79 % (3855781)------------------------------
% 65.07/9.79 % (3855781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.07/9.79 % (3855781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/9.79 % (3855781)CaDiCaL version: 2.1.3
% 65.07/9.79 % (3855781)Termination reason: Instruction limit
% 65.07/9.79 % (3855781)Termination phase: Finite model building preprocessing
% 65.07/9.79 % (3855781)Time elapsed: 0.335 s
% 65.07/9.79 % (3855781)Peak memory usage: 86 MB
% 65.07/9.79 % (3855781)Instructions burned: 891 (million)
% 65.07/9.79 % (3855789)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3687777827:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 65.07/9.79 % (3855779)Instruction limit reached!
% 65.07/9.79 % (3855779)------------------------------
% 65.07/9.79 % (3855779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.07/9.79 % (3855779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/9.79 % (3855779)CaDiCaL version: 2.1.3
% 65.07/9.79 % (3855779)Termination reason: Instruction limit
% 65.07/9.79 % (3855779)Termination phase: Saturation
% 65.07/9.79 % (3855779)Time elapsed: 0.401 s
% 65.07/9.79 % (3855779)Peak memory usage: 81 MB
% 65.07/9.79 % (3855779)Instructions burned: 1181 (million)
% 65.07/9.79 % (3855791)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=92777934:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 65.07/9.79 % (3855785)Instruction limit reached!
% 65.07/9.79 % (3855785)------------------------------
% 65.07/9.79 % (3855785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.07/9.79 % (3855785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/9.79 % (3855785)CaDiCaL version: 2.1.3
% 65.07/9.79 % (3855785)Termination reason: Instruction limit
% 65.07/9.79 % (3855785)Termination phase: Saturation
% 65.07/9.79 % (3855785)Time elapsed: 0.335 s
% 65.07/9.79 % (3855785)Peak memory usage: 91 MB
% 65.07/9.79 % (3855785)Instructions burned: 879 (million)
% 65.07/9.79 % (3855793)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4136861756:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 65.07/9.79 % TRYING [1]
% 65.07/9.79 % TRYING [2]
% 65.07/9.79 % (3855791)Instruction limit reached!
% 65.07/9.79 % (3855791)------------------------------
% 65.07/9.79 % (3855791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.07/9.79 % (3855791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/9.79 % (3855791)CaDiCaL version: 2.1.3
% 65.07/9.79 % (3855791)Termination reason: Instruction limit
% 65.07/9.79 % (3855791)Termination phase: Finite model building preprocessing
% 65.07/9.79 % (3855791)Time elapsed: 0.320 s
% 65.07/9.79 % (3855791)Peak memory usage: 79 MB
% 65.07/9.79 % (3855791)Instructions burned: 923 (million)
% 65.07/9.79 % (3855795)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3563644475:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 65.07/9.79 % TRYING [3]
% 65.07/9.79 % TRYING [1]
% 65.07/9.79 % (3855795)Instruction limit reached!
% 65.07/9.79 % (3855795)------------------------------
% 65.07/9.79 % (3855795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.07/9.79 % (3855795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.07/9.79 % (3855795)CaDiCaL version: 2.1.3
% 65.07/9.79 % (3855795)Termination reason: Instruction limit
% 65.07/9.79 % (3855795)Termination phase: Saturation
% 65.07/9.79 % (3855795)Time elapsed: 0.443 s
% 65.07/9.79 % (3855795)Peak memory usage: 82 MB
% 65.07/9.79 % (3855795)Instructions burned: 1478 (million)
% 65.07/9.79 % (3855797)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=258776247:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 65.07/9.79 % TRYING [20]
% 65.07/9.79 % TRYING [4]
% 65.07/9.79 % TRYING [2]
% 65.07/9.79 % (3855797)Cannot represent all propositional literals internally
% 65.07/9.79 % (3855797)Refutation not found, incomplete strategy
% 65.07/9.79 % (3855797)------------------------------
% 65.07/9.79 % (3855797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.14/23.69 % (3855797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.14/23.69 % (3855797)CaDiCaL version: 2.1.3
% 163.14/23.69 % (3855797)Termination reason: Refutation not found, incomplete strategy
% 163.14/23.69 % (3855797)Time elapsed: 0.864 s
% 163.14/23.69 % (3855797)Peak memory usage: 115 MB
% 163.14/23.69 % (3855797)Instructions burned: 2685 (million)
% 163.14/23.69 % (3855797)------------------------------
% 163.14/23.69 % (3855797)------------------------------
% 163.14/23.69 % (3855799)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1744425436:fmbsr=2.30978:i=2174_2971 on theBenchmark for (2971ds/2174Mi)
% 163.14/23.69 % (3855793)Instruction limit reached!
% 163.14/23.69 % (3855793)------------------------------
% 163.14/23.69 % (3855793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.14/23.69 % (3855793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.14/23.69 % (3855793)CaDiCaL version: 2.1.3
% 163.14/23.69 % (3855793)Termination reason: Instruction limit
% 163.14/23.69 % (3855793)Termination phase: Saturation
% 163.14/23.69 % (3855793)Time elapsed: 1.844 s
% 163.14/23.69 % (3855793)Peak memory usage: 159 MB
% 163.14/23.69 % (3855793)Instructions burned: 5134 (million)
% 163.14/23.69 % (3855801)ott-2_1_sil=16000:newcnf=on:random_seed=2554306737:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2968 on theBenchmark for (2968ds/869Mi)
% 163.14/23.69 % (3855789)Instruction limit reached!
% 163.14/23.69 % (3855789)------------------------------
% 163.14/23.69 % (3855789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.14/23.69 % (3855789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.14/23.69 % (3855789)CaDiCaL version: 2.1.3
% 163.14/23.69 % (3855789)Termination reason: Instruction limit
% 163.14/23.69 % (3855789)Termination phase: Finite model building constraint generation
% 163.14/23.69 % (3855789)Time elapsed: 2.213 s
% 163.14/23.69 % (3855789)Peak memory usage: 509 MB
% 163.14/23.69 % (3855789)Instructions burned: 9517 (million)
% 163.14/23.69 % (3855803)ott+10_1_sil=32000:tgt=ground:random_seed=2731112057:i=5114:av=off_2966 on theBenchmark for (2966ds/5114Mi)
% 163.14/23.69 % (3855801)Instruction limit reached!
% 163.14/23.69 % (3855801)------------------------------
% 163.14/23.69 % (3855801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.14/23.69 % (3855801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.14/23.69 % (3855801)CaDiCaL version: 2.1.3
% 163.14/23.69 % (3855801)Termination reason: Instruction limit
% 163.14/23.69 % (3855801)Termination phase: Saturation
% 163.14/23.69 % (3855801)Time elapsed: 0.319 s
% 163.14/23.69 % (3855801)Peak memory usage: 78 MB
% 163.14/23.69 % (3855801)Instructions burned: 871 (million)
% 163.14/23.69 % (3855805)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=24154887:i=54282_2965 on theBenchmark for (2965ds/54282Mi)
% 163.14/23.69 % TRYING [5]
% 163.14/23.69 % (3855799)Instruction limit reached!
% 163.14/23.69 % (3855799)------------------------------
% 163.14/23.69 % (3855799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.14/23.69 % (3855799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.14/23.69 % (3855799)CaDiCaL version: 2.1.3
% 163.14/23.69 % (3855799)Termination reason: Instruction limit
% 163.14/23.69 % (3855799)Termination phase: Finite model building preprocessing
% 163.14/23.69 % (3855799)Time elapsed: 0.763 s
% 163.14/23.69 % (3855799)Peak memory usage: 139 MB
% 163.14/23.69 % (3855799)Instructions burned: 2175 (million)
% 163.14/23.69 % (3855807)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=587015303:i=3512:aac=none_2963 on theBenchmark for (2963ds/3512Mi)
% 163.14/23.69 % TRYING [1]
% 163.14/23.69 % TRYING [2]
% 163.14/23.69 % TRYING [3]
% 163.14/23.69 % (3855807)Instruction limit reached!
% 163.14/23.69 % (3855807)------------------------------
% 163.14/23.69 % (3855807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.14/23.69 % (3855807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.14/23.69 % (3855807)CaDiCaL version: 2.1.3
% 163.14/23.69 % (3855807)Termination reason: Instruction limit
% 163.14/23.69 % (3855807)Termination phase: Saturation
% 163.14/23.69 % (3855807)Time elapsed: 1.262 s
% 163.14/23.69 % (3855807)Peak memory usage: 116 MB
% 163.14/23.69 % (3855807)Instructions burned: 3514 (million)
% 163.14/23.69 % (3855809)dis+21_1_sil=32000:sas=cadical:random_seed=4079820163:i=3773:amm=off_2950 on theBenchmark for (2950ds/3773Mi)
% 163.14/23.69 % (3855803)Instruction limit reached!
% 163.14/23.69 % (3855803)------------------------------
% 163.14/23.69 % (3855803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 235.85/33.90 % (3855803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 235.85/33.90 % (3855803)CaDiCaL version: 2.1.3
% 235.85/33.90 % (3855803)Termination reason: Instruction limit
% 235.85/33.90 % (3855803)Termination phase: Saturation
% 235.85/33.90 % (3855803)Time elapsed: 1.736 s
% 235.85/33.90 % (3855803)Peak memory usage: 137 MB
% 235.85/33.90 % (3855803)Instructions burned: 5116 (million)
% 235.85/33.90 % (3855811)ott+11_1_sil=16000:gs=on:random_seed=45913843:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2948 on theBenchmark for (2948ds/2251Mi)
% 235.85/33.90 % TRYING [4]
% 235.85/33.90 % (3855787)Instruction limit reached!
% 235.85/33.90 % (3855787)------------------------------
% 235.85/33.90 % (3855787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 235.85/33.90 % (3855787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 235.85/33.90 % (3855787)CaDiCaL version: 2.1.3
% 235.85/33.90 % (3855787)Termination reason: Instruction limit
% 235.85/33.90 % (3855787)Termination phase: Finite model building SAT solving
% 235.85/33.90 % (3855787)Time elapsed: 4.839 s
% 235.85/33.90 % (3855787)Peak memory usage: 178 MB
% 235.85/33.90 % (3855787)Instructions burned: 22064 (million)
% 235.85/33.90 % (3855813)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2707708927:fmbsr=1.6:i=67534_2940 on theBenchmark for (2940ds/67534Mi)
% 235.85/33.90 % (3855811)Instruction limit reached!
% 235.85/33.90 % (3855811)------------------------------
% 235.85/33.90 % (3855811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 235.85/33.90 % (3855811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 235.85/33.90 % (3855811)CaDiCaL version: 2.1.3
% 235.85/33.90 % (3855811)Termination reason: Instruction limit
% 235.85/33.90 % (3855811)Termination phase: Saturation
% 235.85/33.90 % (3855811)Time elapsed: 0.796 s
% 235.85/33.90 % (3855811)Peak memory usage: 99 MB
% 235.85/33.90 % (3855811)Instructions burned: 2253 (million)
% 235.85/33.90 % (3855815)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=552492020:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2940 on theBenchmark for (2940ds/4591Mi)
% 235.85/33.90 % (3855809)Instruction limit reached!
% 235.85/33.90 % (3855809)------------------------------
% 235.85/33.90 % (3855809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 235.85/33.90 % (3855809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 235.85/33.90 % (3855809)CaDiCaL version: 2.1.3
% 235.85/33.90 % (3855809)Termination reason: Instruction limit
% 235.85/33.90 % (3855809)Termination phase: Saturation
% 235.85/33.90 % (3855809)Time elapsed: 1.176 s
% 235.85/33.90 % (3855809)Peak memory usage: 106 MB
% 235.85/33.90 % (3855809)Instructions burned: 3774 (million)
% 235.85/33.90 % (3855817)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=15576682:i=29340_2938 on theBenchmark for (2938ds/29340Mi)
% 235.85/33.90 % TRYING [6]
% 235.85/33.90 % TRYING [5]
% 235.85/33.90 % TRYING [7]
% 235.85/33.90 % (3855815)Instruction limit reached!
% 235.85/33.90 % (3855815)------------------------------
% 235.85/33.90 % (3855815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 235.85/33.90 % (3855815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 235.85/33.90 % (3855815)CaDiCaL version: 2.1.3
% 235.85/33.90 % (3855815)Termination reason: Instruction limit
% 235.85/33.90 % (3855815)Termination phase: Saturation
% 235.85/33.90 % (3855815)Time elapsed: 1.027 s
% 235.85/33.90 % (3855815)Peak memory usage: 85 MB
% 235.85/33.90 % (3855815)Instructions burned: 4595 (million)
% 235.85/33.90 % (3855819)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3535600248:i=5211_2929 on theBenchmark for (2929ds/5211Mi)
% 235.85/33.90 % (3855819)Instruction limit reached!
% 235.85/33.90 % (3855819)------------------------------
% 235.85/33.90 % (3855819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 235.85/33.90 % (3855819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 235.85/33.90 % (3855819)CaDiCaL version: 2.1.3
% 235.85/33.90 % (3855819)Termination reason: Instruction limit
% 235.85/33.90 % (3855819)Termination phase: Saturation
% 235.85/33.90 % (3855819)Time elapsed: 1.135 s
% 235.85/33.90 % (3855819)Peak memory usage: 111 MB
% 235.85/33.90 % (3855819)Instructions burned: 5213 (million)
% 235.85/33.90 % (3855821)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3351790898:i=5497:nm=2_2918 on theBenchmark for (2918ds/5497Mi)
% 235.85/33.90 % TRYING [17]
% 235.85/33.90 % TRYING [6]
% 235.85/33.90 % (3855821)Instruction limit reached!
% 235.85/33.90 % (3855821)------------------------------
% 235.85/33.90 % (3855821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 221.28/37.21 % (3855821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.28/37.21 % (3855821)CaDiCaL version: 2.1.3
% 221.28/37.21 % (3855821)Termination reason: Instruction limit
% 221.28/37.21 % (3855821)Termination phase: Finite model building constraint generation
% 221.28/37.21 % (3855821)Time elapsed: 1.469 s
% 221.28/37.21 % (3855821)Peak memory usage: 278 MB
% 221.28/37.21 % (3855821)Instructions burned: 5502 (million)
% 221.28/37.21 % (3855823)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2047379774:fmbsr=2:i=46332_2903 on theBenchmark for (2903ds/46332Mi)
% 221.28/37.21 % TRYING [15]
% 221.28/37.21 % TRYING [7]
% 221.28/37.21 % TRYING [7]
% 221.28/37.21 % (3855817)Instruction limit reached!
% 221.28/37.21 % (3855817)------------------------------
% 221.28/37.21 % (3855817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 221.28/37.21 % (3855817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.28/37.21 % (3855817)CaDiCaL version: 2.1.3
% 221.28/37.21 % (3855817)Termination reason: Instruction limit
% 221.28/37.21 % (3855817)Termination phase: Saturation
% 221.28/37.21 % (3855817)Time elapsed: 11.597 s
% 221.28/37.21 % (3855817)Peak memory usage: 827 MB
% 221.28/37.21 % (3855817)Instructions burned: 29340 (million)
% 221.28/37.21 % (3855825)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2340175463:i=14071_2821 on theBenchmark for (2821ds/14071Mi)
% 221.28/37.21 % TRYING [12]
% 221.28/37.21 % (3855823)Instruction limit reached!
% 221.28/37.21 % (3855823)------------------------------
% 221.28/37.21 % (3855823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 221.28/37.21 % (3855823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.28/37.21 % (3855823)CaDiCaL version: 2.1.3
% 221.28/37.21 % (3855823)Termination reason: Instruction limit
% 221.28/37.21 % (3855823)Termination phase: Finite model building constraint generation
% 221.28/37.21 % (3855823)Time elapsed: 9.310 s
% 221.28/37.21 % (3855823)Peak memory usage: 2587 MB
% 221.28/37.21 % (3855823)Instructions burned: 46335 (million)
% 221.28/37.21 % (3855828)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3997604941:i=22565:add=on:rawr=on_2807 on theBenchmark for (2807ds/22565Mi)
% 221.28/37.21 % (3855805)Instruction limit reached!
% 221.28/37.21 % (3855805)------------------------------
% 221.28/37.21 % (3855805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 221.28/37.21 % (3855805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.28/37.21 % (3855805)CaDiCaL version: 2.1.3
% 221.28/37.21 % (3855805)Termination reason: Instruction limit
% 221.28/37.21 % (3855805)Termination phase: Finite model building constraint generation
% 221.28/37.21 % (3855805)Time elapsed: 16.214 s
% 221.28/37.21 % (3855805)Peak memory usage: 1017 MB
% 221.28/37.21 % (3855805)Instructions burned: 54284 (million)
% 221.28/37.21 % (3855830)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3544776017:i=8173:av=off_2802 on theBenchmark for (2802ds/8173Mi)
% 221.28/37.21 % (3855825)Instruction limit reached!
% 221.28/37.21 % (3855825)------------------------------
% 221.28/37.21 % (3855825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 221.28/37.21 % (3855825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.28/37.21 % (3855825)CaDiCaL version: 2.1.3
% 221.28/37.21 % (3855825)Termination reason: Instruction limit
% 221.28/37.21 % (3855825)Termination phase: Finite model building constraint generation
% 221.28/37.21 % (3855825)Time elapsed: 3.098 s
% 221.28/37.21 % (3855825)Peak memory usage: 779 MB
% 221.28/37.21 % (3855825)Instructions burned: 14074 (million)
% 221.28/37.21 % (3855832)dis+10_16:1_sil=16000:random_seed=3713987868:i=9155:fsr=off_2789 on theBenchmark for (2789ds/9155Mi)
% 221.28/37.21 % (3855830)Instruction limit reached!
% 221.28/37.21 % (3855830)------------------------------
% 221.28/37.21 % (3855830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 221.28/37.21 % (3855830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.28/37.21 % (3855830)CaDiCaL version: 2.1.3
% 221.28/37.21 % (3855830)Termination reason: Instruction limit
% 221.28/37.21 % (3855830)Termination phase: Saturation
% 221.28/37.21 % (3855830)Time elapsed: 2.755 s
% 221.28/37.21 % (3855830)Peak memory usage: 167 MB
% 221.28/37.21 % (3855830)Instructions burned: 8180 (million)
% 221.28/37.21 % (3855876)ott-3_8_sil=64000:random_seed=3439584452:i=20139:bs=on_2774 on theBenchmark for (2774ds/20139Mi)
% 221.28/37.21 % (3855832)Instruction limit reached!
% 221.28/37.21 % (3855832)------------------------------
% 221.28/37.21 % (3855832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 221.28/37.21 % (3855832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.28/37.21 % (3855832)CaDiCaL version: 2.1.3
% 221.28/37.21 % (3855832)Termination reason: Instruction limit
% 221.28/37.21 % (3855832)Termination phase: Saturation
% 221.28/37.21 % (3855832)Time elapsed: 2.513 s
% 221.28/37.21 % (3855832)Peak memory usage: 125 MB
% 221.28/37.21 % (3855832)Instructions burned: 9156 (million)
% 221.28/37.21 % (3855878)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2540563003:fmbsr=2:i=32576_2764 on theBenchmark for (2764ds/32576Mi)
% 221.28/37.21 % TRYING [9]
% 221.28/37.21 % (3855828)Instruction limit reached!
% 221.28/37.21 % (3855828)------------------------------
% 221.28/37.21 % (3855828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 221.28/37.21 % (3855828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.28/37.21 % (3855828)CaDiCaL version: 2.1.3
% 221.28/37.21 % (3855828)Termination reason: Instruction limit
% 221.28/37.21 % (3855828)Termination phase: Saturation
% 221.28/37.21 % (3855828)Time elapsed: 5.360 s
% 221.28/37.21 % (3855828)Peak memory usage: 317 MB
% 221.28/37.21 % (3855828)Instructions burned: 22571 (million)
% 221.28/37.21 % (3855880)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3837036747:i=11404_2753 on theBenchmark for (2753ds/11404Mi)
% 221.28/37.21 % (3855880)Instruction limit reached!
% 221.28/37.21 % (3855880)------------------------------
% 221.28/37.21 % (3855880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 221.28/37.21 % (3855880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.28/37.21 % (3855880)CaDiCaL version: 2.1.3
% 221.28/37.21 % (3855880)Termination reason: Instruction limit
% 221.28/37.21 % (3855880)Termination phase: Saturation
% 221.28/37.21 % (3855880)Time elapsed: 3.117 s
% 221.28/37.21 % (3855880)Peak memory usage: 168 MB
% 221.28/37.21 % (3855880)Instructions burned: 11407 (million)
% 221.28/37.21 % (3855882)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2253183889:i=14134_2722 on theBenchmark for (2722ds/14134Mi)
% 221.28/37.21 % (3855813)Instruction limit reached!
% 221.28/37.21 % (3855813)------------------------------
% 221.28/37.21 % (3855813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 221.28/37.21 % (3855813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.28/37.21 % (3855813)CaDiCaL version: 2.1.3
% 221.28/37.21 % (3855813)Termination reason: Instruction limit
% 221.28/37.21 % (3855813)Termination phase: Finite model building SAT solving
% 221.28/37.21 % (3855813)Time elapsed: 22.883 s
% 221.28/37.21 % (3855813)Peak memory usage: 1505 MB
% 221.28/37.21 % (3855813)Instructions burned: 67535 (million)
% 221.28/37.21 % (3855966)dis+33_16_sil=32000:sac=on:random_seed=1252884998:i=15851:nm=0_2710 on theBenchmark for (2710ds/15851Mi)
% 221.28/37.21 % (3855882)Instruction limit reached!
% 221.28/37.21 % (3855882)------------------------------
% 221.28/37.21 % (3855882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 221.28/37.21 % (3855882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.28/37.21 % (3855882)CaDiCaL version: 2.1.3
% 221.28/37.21 % (3855882)Termination reason: Instruction limit
% 221.28/37.21 % (3855882)Termination phase: Saturation
% 221.28/37.21 % (3855882)Time elapsed: 4.831 s
% 221.28/37.21 % (3855882)Peak memory usage: 116 MB
% 221.28/37.21 % (3855882)Instructions burned: 14136 (million)
% 221.28/37.21 % (3856331)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2470212835:avsq=on:i=17627:add=on:amm=off_2673 on theBenchmark for (2673ds/17627Mi)
% 221.28/37.21 % (3855878)Instruction limit reached!
% 221.28/37.21 % (3855878)------------------------------
% 221.28/37.21 % (3855878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 221.28/37.21 % (3855878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.28/37.21 % (3855878)CaDiCaL version: 2.1.3
% 221.28/37.21 % (3855878)Termination reason: Instruction limit
% 221.28/37.21 % (3855878)Termination phase: Finite model building constraint generation
% 221.28/37.21 % (3855878)Time elapsed: 9.110 s
% 221.28/37.21 % (3855878)Peak memory usage: 1948 MB
% 221.28/37.21 % (3855878)Instructions burned: 32578 (million)
% 221.28/37.21 % (3856333)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=201189053:s2a=on:i=53295_2671 on theBenchmark for (2671ds/53295Mi)
% 221.28/37.21 % (3855876)Instruction limit reached!
% 221.28/37.21 % (3855876)------------------------------
% 221.28/37.21 % (3855876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 221.28/37.21 % (3855876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.28/37.21 % (3855876)CaDiCaL version: 2.1.3
% 221.28/37.21 % (3855876)Termination reason: Instruction limit
% 221.28/37.21 % (3855876)Termination phase: Saturation
% 221.28/37.21 % (3855876)Time elapsed: 11.163 s
% 221.28/37.21 % (3855876)Peak memory usage: 251 MB
% 221.28/37.21 % (3855876)Instructions burned: 20140 (million)
% 221.28/37.21 % (3856335)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=848361897:i=26857:ins=20_2662 on theBenchmark for (2662ds/26857Mi)
% 221.28/37.21 % TRYING [16]
% 221.28/37.21 % (3855966)Instruction limit reached!
% 221.28/37.21 % (3855966)------------------------------
% 221.28/37.21 % (3855966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 221.28/37.21 % (3855966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.28/37.21 % (3855966)CaDiCaL version: 2.1.3
% 221.28/37.21 % (3855966)Termination reason: Instruction limit
% 221.28/37.21 % (3855966)Termination phase: Saturation
% 221.28/37.21 % (3855966)Time elapsed: 6.905 s
% 221.28/37.21 % (3855966)Peak memory usage: 236 MB
% 221.28/37.21 % (3855966)Instructions burned: 15853 (million)
% 221.28/37.21 % (3856337)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1524073288:i=28120:bs=on:fsr=off_2641 on theBenchmark for (2641ds/28120Mi)
% 221.28/37.21 % (3856333) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3855748-3856333"...
% 221.28/37.21 % (3856333)...printing done.
% 221.28/37.21 % (3856333)Refutation found. Thanks to Tanya!
% 221.28/37.21 % SZS status Theorem for theBenchmark
% 221.28/37.21 % SZS output start Proof for theBenchmark
% See solution above
% 221.28/37.24 % (3856333)------------------------------
% 221.28/37.24 % (3856333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 221.28/37.24 % (3856333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 221.28/37.24 % (3856333)CaDiCaL version: 2.1.3
% 221.28/37.24 % (3856333)Termination reason: Refutation
% 221.28/37.24 % (3856333)Time elapsed: 3.905 s
% 221.28/37.24 % (3856333)Peak memory usage: 265 MB
% 221.28/37.24 % (3856333)Instructions burned: 11796 (million)
% 221.28/37.24 % (3855748)Success in time 37.067 s
% 221.28/37.24 % Vampire exiting
%------------------------------------------------------------------------------