%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR061+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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:48 AM UTC 2026
% Result : Theorem 0.26s 0.33s
% Output : Refutation 0.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 23
% Syntax : Number of formulae : 116 ( 59 unt; 2 def)
% Number of atoms : 203 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 164 ( 77 ~; 76 |; 4 &)
% ( 2 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 3 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 62 ( 0 sgn 62 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just5) ).
fof(f7,axiom,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just7) ).
fof(f9,axiom,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just9) ).
fof(f11,axiom,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just11) ).
fof(f13,axiom,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just13) ).
fof(f15,axiom,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just15) ).
fof(f17,axiom,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just17) ).
fof(f19,axiom,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just19) ).
fof(f21,axiom,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just21) ).
fof(f23,axiom,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just23) ).
fof(f25,axiom,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just25) ).
fof(f27,axiom,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just27) ).
fof(f29,axiom,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just29) ).
fof(f31,axiom,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just31) ).
fof(f33,axiom,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just33) ).
fof(f35,axiom,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just35) ).
fof(f37,axiom,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just37) ).
fof(f55,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X1) )
=> disjointwith(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just55) ).
fof(f56,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X0) )
=> disjointwith(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just56) ).
fof(f97,axiom,
! [X0,X1,X2] :
( ( genls(X0,X1)
& genls(X1,X2) )
=> genls(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just97) ).
fof(f119,conjecture,
( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query61) ).
fof(f120,negated_conjecture,
~ ( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
inference(negated_conjecture,[status(cth)],[f119]) ).
fof(f160,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(ennf_transformation,[],[f55]) ).
fof(f161,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(flattening,[],[f160]) ).
fof(f162,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(ennf_transformation,[],[f56]) ).
fof(f163,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(flattening,[],[f162]) ).
fof(f204,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X0,X1)
| ~ genls(X1,X2) ),
inference(ennf_transformation,[],[f97]) ).
fof(f205,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X0,X1)
| ~ genls(X1,X2) ),
inference(flattening,[],[f204]) ).
fof(f228,plain,
( ~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118)
& mtvisible(c_timehasnoendmt) ),
inference(ennf_transformation,[],[f120]) ).
fof(f233,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(cnf_transformation,[],[f5]) ).
fof(f235,plain,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
inference(cnf_transformation,[],[f7]) ).
fof(f237,plain,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
inference(cnf_transformation,[],[f9]) ).
fof(f239,plain,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
inference(cnf_transformation,[],[f11]) ).
fof(f241,plain,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
inference(cnf_transformation,[],[f13]) ).
fof(f243,plain,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
inference(cnf_transformation,[],[f15]) ).
fof(f245,plain,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
inference(cnf_transformation,[],[f17]) ).
fof(f247,plain,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
inference(cnf_transformation,[],[f19]) ).
fof(f249,plain,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
inference(cnf_transformation,[],[f21]) ).
fof(f251,plain,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
inference(cnf_transformation,[],[f23]) ).
fof(f253,plain,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
inference(cnf_transformation,[],[f25]) ).
fof(f255,plain,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
inference(cnf_transformation,[],[f27]) ).
fof(f257,plain,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
inference(cnf_transformation,[],[f29]) ).
fof(f259,plain,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
inference(cnf_transformation,[],[f31]) ).
fof(f261,plain,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
inference(cnf_transformation,[],[f33]) ).
fof(f263,plain,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
inference(cnf_transformation,[],[f35]) ).
fof(f265,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
inference(cnf_transformation,[],[f37]) ).
fof(f281,plain,
! [X2,X0,X1] :
( ~ genls(X2,X1)
| ~ disjointwith(X0,X1)
| disjointwith(X0,X2) ),
inference(cnf_transformation,[],[f161]) ).
fof(f282,plain,
! [X2,X0,X1] :
( ~ genls(X2,X0)
| ~ disjointwith(X0,X1)
| disjointwith(X2,X1) ),
inference(cnf_transformation,[],[f163]) ).
fof(f323,plain,
! [X2,X0,X1] :
( ~ genls(X1,X2)
| ~ genls(X0,X1)
| genls(X0,X2) ),
inference(cnf_transformation,[],[f205]) ).
fof(f344,plain,
~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(cnf_transformation,[],[f228]) ).
fof(f349,plain,
~ genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(consistent_polarity_flipping,[],[f233]) ).
fof(f351,plain,
~ genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
inference(consistent_polarity_flipping,[],[f235]) ).
fof(f353,plain,
~ genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
inference(consistent_polarity_flipping,[],[f237]) ).
fof(f355,plain,
~ genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
inference(consistent_polarity_flipping,[],[f239]) ).
fof(f357,plain,
~ genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
inference(consistent_polarity_flipping,[],[f241]) ).
fof(f359,plain,
~ genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
inference(consistent_polarity_flipping,[],[f243]) ).
fof(f361,plain,
~ genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
inference(consistent_polarity_flipping,[],[f245]) ).
fof(f363,plain,
~ genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
inference(consistent_polarity_flipping,[],[f247]) ).
fof(f365,plain,
~ genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
inference(consistent_polarity_flipping,[],[f249]) ).
fof(f367,plain,
~ genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
inference(consistent_polarity_flipping,[],[f251]) ).
fof(f369,plain,
~ genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
inference(consistent_polarity_flipping,[],[f253]) ).
fof(f370,plain,
~ genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
inference(consistent_polarity_flipping,[],[f255]) ).
fof(f372,plain,
~ genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
inference(consistent_polarity_flipping,[],[f257]) ).
fof(f374,plain,
~ genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
inference(consistent_polarity_flipping,[],[f259]) ).
fof(f376,plain,
~ genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
inference(consistent_polarity_flipping,[],[f261]) ).
fof(f378,plain,
~ genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
inference(consistent_polarity_flipping,[],[f263]) ).
fof(f379,plain,
~ disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
inference(consistent_polarity_flipping,[],[f265]) ).
fof(f388,plain,
! [X2,X0,X1] :
( ~ disjointwith(X0,X2)
| disjointwith(X0,X1)
| genls(X2,X1) ),
inference(consistent_polarity_flipping,[],[f281]) ).
fof(f389,plain,
! [X2,X0,X1] :
( ~ disjointwith(X2,X1)
| disjointwith(X0,X1)
| genls(X2,X0) ),
inference(consistent_polarity_flipping,[],[f282]) ).
fof(f416,plain,
! [X2,X0,X1] :
( ~ genls(X0,X2)
| genls(X0,X1)
| genls(X1,X2) ),
inference(consistent_polarity_flipping,[],[f323]) ).
fof(f434,plain,
disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(consistent_polarity_flipping,[],[f344]) ).
fof(f628,plain,
! [X0] :
( disjointwith(c_tptpcol_8_114177,X0)
| genls(c_tptpcol_14_118118,X0) ),
inference(resolution,[],[f388,f434]) ).
fof(f638,plain,
! [X0,X1] :
( disjointwith(X1,X0)
| genls(c_tptpcol_14_118118,X0)
| genls(c_tptpcol_8_114177,X1) ),
inference(resolution,[],[f628,f389]) ).
fof(f669,plain,
( genls(c_tptpcol_14_118118,c_tptpcol_3_114688)
| genls(c_tptpcol_8_114177,c_tptpcol_3_98305) ),
inference(resolution,[],[f638,f379]) ).
fof(f674,definition,
( spl0_25
<=> genls(c_tptpcol_8_114177,c_tptpcol_3_98305) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f676,plain,
( genls(c_tptpcol_8_114177,c_tptpcol_3_98305)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f674]) ).
fof(f678,definition,
( spl0_26
<=> genls(c_tptpcol_14_118118,c_tptpcol_3_114688) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f680,plain,
( genls(c_tptpcol_14_118118,c_tptpcol_3_114688)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f678]) ).
fof(f681,plain,
( spl0_25
| spl0_26 ),
inference(avatar_split_clause,[],[f669,f678,f674]) ).
fof(f894,plain,
( ! [X0] :
( genls(c_tptpcol_8_114177,X0)
| genls(X0,c_tptpcol_3_98305) )
| ~ spl0_25 ),
inference(resolution,[],[f676,f416]) ).
fof(f898,plain,
( genls(c_tptpcol_7_113665,c_tptpcol_3_98305)
| ~ spl0_25 ),
inference(resolution,[],[f894,f357]) ).
fof(f902,plain,
( ! [X0] :
( genls(c_tptpcol_7_113665,X0)
| genls(X0,c_tptpcol_3_98305) )
| ~ spl0_25 ),
inference(resolution,[],[f898,f416]) ).
fof(f912,plain,
( genls(c_tptpcol_6_112641,c_tptpcol_3_98305)
| ~ spl0_25 ),
inference(resolution,[],[f902,f355]) ).
fof(f917,plain,
( ! [X0] :
( genls(c_tptpcol_6_112641,X0)
| genls(X0,c_tptpcol_3_98305) )
| ~ spl0_25 ),
inference(resolution,[],[f912,f416]) ).
fof(f918,plain,
( genls(c_tptpcol_5_110593,c_tptpcol_3_98305)
| ~ spl0_25 ),
inference(resolution,[],[f917,f353]) ).
fof(f993,plain,
( ! [X0] :
( genls(c_tptpcol_5_110593,X0)
| genls(X0,c_tptpcol_3_98305) )
| ~ spl0_25 ),
inference(resolution,[],[f918,f416]) ).
fof(f1002,plain,
( genls(c_tptpcol_4_106497,c_tptpcol_3_98305)
| ~ spl0_25 ),
inference(resolution,[],[f993,f351]) ).
fof(f1006,plain,
( $false
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f1002,f349]) ).
fof(f1007,plain,
~ spl0_25,
inference(avatar_contradiction_clause,[],[f1006]) ).
fof(f1021,plain,
( ! [X0] :
( genls(c_tptpcol_14_118118,X0)
| genls(X0,c_tptpcol_3_114688) )
| ~ spl0_26 ),
inference(resolution,[],[f680,f416]) ).
fof(f1107,plain,
( genls(c_tptpcol_13_118117,c_tptpcol_3_114688)
| ~ spl0_26 ),
inference(resolution,[],[f1021,f378]) ).
fof(f1111,plain,
( ! [X0] :
( genls(c_tptpcol_13_118117,X0)
| genls(X0,c_tptpcol_3_114688) )
| ~ spl0_26 ),
inference(resolution,[],[f1107,f416]) ).
fof(f1112,plain,
( genls(c_tptpcol_12_118116,c_tptpcol_3_114688)
| ~ spl0_26 ),
inference(resolution,[],[f1111,f376]) ).
fof(f1116,plain,
( ! [X0] :
( genls(c_tptpcol_12_118116,X0)
| genls(X0,c_tptpcol_3_114688) )
| ~ spl0_26 ),
inference(resolution,[],[f1112,f416]) ).
fof(f1118,plain,
( genls(c_tptpcol_11_118084,c_tptpcol_3_114688)
| ~ spl0_26 ),
inference(resolution,[],[f1116,f374]) ).
fof(f1134,plain,
( ! [X0] :
( genls(c_tptpcol_11_118084,X0)
| genls(X0,c_tptpcol_3_114688) )
| ~ spl0_26 ),
inference(resolution,[],[f1118,f416]) ).
fof(f1135,plain,
( genls(c_tptpcol_10_118020,c_tptpcol_3_114688)
| ~ spl0_26 ),
inference(resolution,[],[f1134,f372]) ).
fof(f1139,plain,
( ! [X0] :
( genls(c_tptpcol_10_118020,X0)
| genls(X0,c_tptpcol_3_114688) )
| ~ spl0_26 ),
inference(resolution,[],[f1135,f416]) ).
fof(f1223,plain,
( genls(c_tptpcol_9_118019,c_tptpcol_3_114688)
| ~ spl0_26 ),
inference(resolution,[],[f1139,f370]) ).
fof(f1227,plain,
( ! [X0] :
( genls(c_tptpcol_9_118019,X0)
| genls(X0,c_tptpcol_3_114688) )
| ~ spl0_26 ),
inference(resolution,[],[f1223,f416]) ).
fof(f1230,plain,
( genls(c_tptpcol_8_117763,c_tptpcol_3_114688)
| ~ spl0_26 ),
inference(resolution,[],[f1227,f369]) ).
fof(f1236,plain,
( ! [X0] :
( genls(c_tptpcol_8_117763,X0)
| genls(X0,c_tptpcol_3_114688) )
| ~ spl0_26 ),
inference(resolution,[],[f1230,f416]) ).
fof(f1237,plain,
( genls(c_tptpcol_7_117762,c_tptpcol_3_114688)
| ~ spl0_26 ),
inference(resolution,[],[f1236,f367]) ).
fof(f1244,plain,
( ! [X0] :
( genls(c_tptpcol_7_117762,X0)
| genls(X0,c_tptpcol_3_114688) )
| ~ spl0_26 ),
inference(resolution,[],[f1237,f416]) ).
fof(f1252,plain,
( genls(c_tptpcol_6_116738,c_tptpcol_3_114688)
| ~ spl0_26 ),
inference(resolution,[],[f1244,f365]) ).
fof(f1256,plain,
( ! [X0] :
( genls(c_tptpcol_6_116738,X0)
| genls(X0,c_tptpcol_3_114688) )
| ~ spl0_26 ),
inference(resolution,[],[f1252,f416]) ).
fof(f1257,plain,
( genls(c_tptpcol_5_114690,c_tptpcol_3_114688)
| ~ spl0_26 ),
inference(resolution,[],[f1256,f363]) ).
fof(f1265,plain,
( ! [X0] :
( genls(c_tptpcol_5_114690,X0)
| genls(X0,c_tptpcol_3_114688) )
| ~ spl0_26 ),
inference(resolution,[],[f1257,f416]) ).
fof(f1272,plain,
( genls(c_tptpcol_4_114689,c_tptpcol_3_114688)
| ~ spl0_26 ),
inference(resolution,[],[f1265,f361]) ).
fof(f1276,plain,
( $false
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f1272,f359]) ).
fof(f1277,plain,
~ spl0_26,
inference(avatar_contradiction_clause,[],[f1276]) ).
cnf(s17,plain,
( spl0_25
| spl0_26 ),
inference(sat_conversion,[],[f681]) ).
cnf(s54,plain,
~ spl0_25,
inference(sat_conversion,[],[f1007]) ).
cnf(s87,plain,
~ spl0_26,
inference(sat_conversion,[],[f1277]) ).
cnf(s88,plain,
$false,
inference(rat,[],[s17,s87,s54]) ).
fof(f1278,plain,
$false,
inference(avatar_sat_refutation,[],[s88]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR061+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.23 % Computer : n003.cluster.edu
% 0.12/0.23 % Model : x86_64 x86_64
% 0.12/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.23 % Memory : 8046.5625MB
% 0.12/0.23 % OS : Linux 6.8.0-71-generic
% 0.12/0.23 % CPULimit : 300
% 0.12/0.23 % WCLimit : 300
% 0.12/0.23 % DateTime : Mon Sep 28 22:23:28 UTC 2026
% 0.12/0.24 % CPUTime :
% 0.12/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.28 Running first-order model finding
% 0.12/0.28 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
% 0.26/0.33 % (2099474)Will run a generic schedule for satisfiability detection.
% 0.26/0.33 % (2099480)% WARNING: option uhcvi not known.
% 0.26/0.33 % (2099480)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1482746473:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.26/0.33 % (2099479)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1609271408_2999 on theBenchmark for (2999ds/0Mi)
% 0.26/0.33 % Detected minimum model sizes of [1]
% 0.26/0.33 % Detected maximum model sizes of [24]
% 0.26/0.33 % TRYING [1]
% 0.26/0.33 % TRYING [2]
% 0.26/0.33 % TRYING [3]
% 0.26/0.33 % (2099480) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2099474-2099480"...
% 0.26/0.33 % TRYING [4]
% 0.26/0.33 % (2099480)...printing done.
% 0.26/0.33 % (2099480)Refutation found. Thanks to Tanya!
% 0.26/0.33 % SZS status Theorem for theBenchmark
% 0.26/0.33 % SZS output start Proof for theBenchmark
% See solution above
% 0.26/0.33 % (2099480)------------------------------
% 0.26/0.33 % (2099480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.26/0.33 % (2099480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.26/0.33 % (2099480)CaDiCaL version: 2.1.3
% 0.26/0.33 % (2099480)Termination reason: Refutation
% 0.26/0.33 % (2099480)Time elapsed: 0.011 s
% 0.26/0.33 % (2099480)Peak memory usage: 12 MB
% 0.26/0.33 % (2099480)Instructions burned: 17 (million)
% 0.26/0.33 % (2099474)Success in time 0.038 s
% 0.26/0.33 % Vampire exiting
%------------------------------------------------------------------------------