%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KRS157+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.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 11:41:47 AM UTC 2026
% Result : Theorem 2.95s 1.31s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 20
% Syntax : Number of formulae : 113 ( 35 unt; 12 def)
% Number of atoms : 347 ( 0 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 391 ( 157 ~; 160 |; 52 &)
% ( 20 <=>; 1 =>; 0 <=; 1 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 26 ( 25 usr; 13 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 36 ( 0 sgn 32 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( cowlThing(X0)
& ~ cowlNothing(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_0) ).
fof(f2,axiom,
! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
fof(f122,axiom,
! [X0] :
( cC216(X0)
<=> ( cC64(X0)
& cC214xcomp(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_121) ).
fof(f133,axiom,
! [X0] :
( cC30(X0)
<=> ( cC28(X0)
& cC14(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_132) ).
fof(f149,axiom,
! [X0] :
( cC46(X0)
<=> ( cC30(X0)
& cC44(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_148) ).
fof(f202,axiom,
! [X0] :
( cTEST(X0)
<=> ( cC216(X0)
& cC46(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_201) ).
fof(f203,axiom,
cTEST(iV3102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_202) ).
fof(f220,conjecture,
( ! [X0] :
( cowlThing(X0)
& ~ cowlNothing(X0) )
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& cC14(iV3102)
& cC44(iV3102)
& cC216(iV3102)
& cC64(iV3102)
& cC46(iV3102)
& cC28(iV3102)
& cowlThing(iV3102)
& cC30(iV3102) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
fof(f221,negated_conjecture,
~ ( ! [X0] :
( cowlThing(X0)
& ~ cowlNothing(X0) )
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& cC14(iV3102)
& cC44(iV3102)
& cC216(iV3102)
& cC64(iV3102)
& cC46(iV3102)
& cC28(iV3102)
& cowlThing(iV3102)
& cC30(iV3102) ),
inference(negated_conjecture,[status(cth)],[f220]) ).
fof(f222,plain,
~ ( ! [X0] :
( cowlThing(X0)
& ~ cowlNothing(X0) )
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& cC14(iV3102)
& cC44(iV3102)
& cC216(iV3102)
& cC64(iV3102)
& cC46(iV3102)
& cC28(iV3102)
& cowlThing(iV3102)
& cC30(iV3102) ),
inference(rectify,[],[f221]) ).
fof(f223,plain,
! [X0] :
( cTEST(X0)
=> ( cC216(X0)
& cC46(X0) ) ),
inference(unused_predicate_definition_removal,[],[f202]) ).
fof(f279,plain,
! [X0] :
( ( cC216(X0)
& cC46(X0) )
| ~ cTEST(X0) ),
inference(ennf_transformation,[],[f223]) ).
fof(f285,plain,
( ? [X0] :
( ~ cowlThing(X0)
| cowlNothing(X0) )
| ? [X1] :
( xsd_string(X1)
<~> ~ xsd_integer(X1) )
| ~ cC14(iV3102)
| ~ cC44(iV3102)
| ~ cC216(iV3102)
| ~ cC64(iV3102)
| ~ cC46(iV3102)
| ~ cC28(iV3102)
| ~ cowlThing(iV3102)
| ~ cC30(iV3102) ),
inference(ennf_transformation,[],[f222]) ).
fof(f286,plain,
! [X0] :
( ( xsd_string(X0)
| xsd_integer(X0) )
& ( ~ xsd_integer(X0)
| ~ xsd_string(X0) ) ),
inference(nnf_transformation,[],[f2]) ).
fof(f609,plain,
! [X0] :
( ( cC216(X0)
| ~ cC64(X0)
| ~ cC214xcomp(X0) )
& ( ( cC64(X0)
& cC214xcomp(X0) )
| ~ cC216(X0) ) ),
inference(nnf_transformation,[],[f122]) ).
fof(f610,plain,
! [X0] :
( ( cC216(X0)
| ~ cC64(X0)
| ~ cC214xcomp(X0) )
& ( ( cC64(X0)
& cC214xcomp(X0) )
| ~ cC216(X0) ) ),
inference(flattening,[],[f609]) ).
fof(f637,plain,
! [X0] :
( ( cC30(X0)
| ~ cC28(X0)
| ~ cC14(X0) )
& ( ( cC28(X0)
& cC14(X0) )
| ~ cC30(X0) ) ),
inference(nnf_transformation,[],[f133]) ).
fof(f638,plain,
! [X0] :
( ( cC30(X0)
| ~ cC28(X0)
| ~ cC14(X0) )
& ( ( cC28(X0)
& cC14(X0) )
| ~ cC30(X0) ) ),
inference(flattening,[],[f637]) ).
fof(f678,plain,
! [X0] :
( ( cC46(X0)
| ~ cC30(X0)
| ~ cC44(X0) )
& ( ( cC30(X0)
& cC44(X0) )
| ~ cC46(X0) ) ),
inference(nnf_transformation,[],[f149]) ).
fof(f679,plain,
! [X0] :
( ( cC46(X0)
| ~ cC30(X0)
| ~ cC44(X0) )
& ( ( cC30(X0)
& cC44(X0) )
| ~ cC46(X0) ) ),
inference(flattening,[],[f678]) ).
fof(f821,plain,
( ? [X0] :
( ~ cowlThing(X0)
| cowlNothing(X0) )
| ? [X1] :
( ( xsd_integer(X1)
| ~ xsd_string(X1) )
& ( ~ xsd_integer(X1)
| xsd_string(X1) ) )
| ~ cC14(iV3102)
| ~ cC44(iV3102)
| ~ cC216(iV3102)
| ~ cC64(iV3102)
| ~ cC46(iV3102)
| ~ cC28(iV3102)
| ~ cowlThing(iV3102)
| ~ cC30(iV3102) ),
inference(nnf_transformation,[],[f285]) ).
fof(f822,plain,
( ~ cowlThing(sK146)
| cowlNothing(sK146)
| ( ( xsd_integer(sK147)
| ~ xsd_string(sK147) )
& ( ~ xsd_integer(sK147)
| xsd_string(sK147) ) )
| ~ cC14(iV3102)
| ~ cC44(iV3102)
| ~ cC216(iV3102)
| ~ cC64(iV3102)
| ~ cC46(iV3102)
| ~ cC28(iV3102)
| ~ cowlThing(iV3102)
| ~ cC30(iV3102) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK146,sK147]),skolemize(X0,sK146),skolemize(X1,sK147)],[f821]) ).
fof(f823,plain,
! [X0] : ~ cowlNothing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f824,plain,
! [X0] : cowlThing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f825,plain,
! [X0] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[],[f286]) ).
fof(f826,plain,
! [X0] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[],[f286]) ).
fof(f1127,plain,
! [X0] :
( ~ cC216(X0)
| cC64(X0) ),
inference(cnf_transformation,[],[f610]) ).
fof(f1152,plain,
! [X0] :
( ~ cC30(X0)
| cC14(X0) ),
inference(cnf_transformation,[],[f638]) ).
fof(f1153,plain,
! [X0] :
( ~ cC30(X0)
| cC28(X0) ),
inference(cnf_transformation,[],[f638]) ).
fof(f1191,plain,
! [X0] :
( ~ cC46(X0)
| cC44(X0) ),
inference(cnf_transformation,[],[f679]) ).
fof(f1192,plain,
! [X0] :
( ~ cC46(X0)
| cC30(X0) ),
inference(cnf_transformation,[],[f679]) ).
fof(f1325,plain,
! [X0] :
( ~ cTEST(X0)
| cC46(X0) ),
inference(cnf_transformation,[],[f279]) ).
fof(f1326,plain,
! [X0] :
( ~ cTEST(X0)
| cC216(X0) ),
inference(cnf_transformation,[],[f279]) ).
fof(f1327,plain,
cTEST(iV3102),
inference(cnf_transformation,[],[f203]) ).
fof(f1344,plain,
( ~ cowlThing(sK146)
| cowlNothing(sK146)
| ~ xsd_integer(sK147)
| xsd_string(sK147)
| ~ cC14(iV3102)
| ~ cC44(iV3102)
| ~ cC216(iV3102)
| ~ cC64(iV3102)
| ~ cC46(iV3102)
| ~ cC28(iV3102)
| ~ cowlThing(iV3102)
| ~ cC30(iV3102) ),
inference(cnf_transformation,[],[f822]) ).
fof(f1345,plain,
( ~ cowlThing(sK146)
| cowlNothing(sK146)
| xsd_integer(sK147)
| ~ xsd_string(sK147)
| ~ cC14(iV3102)
| ~ cC44(iV3102)
| ~ cC216(iV3102)
| ~ cC64(iV3102)
| ~ cC46(iV3102)
| ~ cC28(iV3102)
| ~ cowlThing(iV3102)
| ~ cC30(iV3102) ),
inference(cnf_transformation,[],[f822]) ).
fof(f1347,definition,
( spl148_1
<=> cC30(iV3102) ),
introduced(definition,[new_symbols(definition,[spl148_1])],[avatar_definition]) ).
fof(f1348,plain,
( ~ cC30(iV3102)
| spl148_1 ),
inference(avatar_component_clause,[],[f1347]) ).
fof(f1350,definition,
( spl148_2
<=> cowlThing(iV3102) ),
introduced(definition,[new_symbols(definition,[spl148_2])],[avatar_definition]) ).
fof(f1351,plain,
( ~ cowlThing(iV3102)
| spl148_2 ),
inference(avatar_component_clause,[],[f1350]) ).
fof(f1353,definition,
( spl148_3
<=> cC28(iV3102) ),
introduced(definition,[new_symbols(definition,[spl148_3])],[avatar_definition]) ).
fof(f1354,plain,
( ~ cC28(iV3102)
| spl148_3 ),
inference(avatar_component_clause,[],[f1353]) ).
fof(f1356,definition,
( spl148_4
<=> cC46(iV3102) ),
introduced(definition,[new_symbols(definition,[spl148_4])],[avatar_definition]) ).
fof(f1357,plain,
( ~ cC46(iV3102)
| spl148_4 ),
inference(avatar_component_clause,[],[f1356]) ).
fof(f1359,definition,
( spl148_5
<=> cC64(iV3102) ),
introduced(definition,[new_symbols(definition,[spl148_5])],[avatar_definition]) ).
fof(f1360,plain,
( ~ cC64(iV3102)
| spl148_5 ),
inference(avatar_component_clause,[],[f1359]) ).
fof(f1362,definition,
( spl148_6
<=> cC216(iV3102) ),
introduced(definition,[new_symbols(definition,[spl148_6])],[avatar_definition]) ).
fof(f1363,plain,
( ~ cC216(iV3102)
| spl148_6 ),
inference(avatar_component_clause,[],[f1362]) ).
fof(f1365,definition,
( spl148_7
<=> cC44(iV3102) ),
introduced(definition,[new_symbols(definition,[spl148_7])],[avatar_definition]) ).
fof(f1366,plain,
( ~ cC44(iV3102)
| spl148_7 ),
inference(avatar_component_clause,[],[f1365]) ).
fof(f1368,definition,
( spl148_8
<=> cC14(iV3102) ),
introduced(definition,[new_symbols(definition,[spl148_8])],[avatar_definition]) ).
fof(f1369,plain,
( ~ cC14(iV3102)
| spl148_8 ),
inference(avatar_component_clause,[],[f1368]) ).
fof(f1371,definition,
( spl148_9
<=> xsd_string(sK147) ),
introduced(definition,[new_symbols(definition,[spl148_9])],[avatar_definition]) ).
fof(f1374,definition,
( spl148_10
<=> xsd_integer(sK147) ),
introduced(definition,[new_symbols(definition,[spl148_10])],[avatar_definition]) ).
fof(f1375,plain,
( ~ xsd_integer(sK147)
| spl148_10 ),
inference(avatar_component_clause,[],[f1374]) ).
fof(f1377,definition,
( spl148_11
<=> cowlNothing(sK146) ),
introduced(definition,[new_symbols(definition,[spl148_11])],[avatar_definition]) ).
fof(f1378,plain,
( cowlNothing(sK146)
| ~ spl148_11 ),
inference(avatar_component_clause,[],[f1377]) ).
fof(f1380,definition,
( spl148_12
<=> cowlThing(sK146) ),
introduced(definition,[new_symbols(definition,[spl148_12])],[avatar_definition]) ).
fof(f1381,plain,
( ~ cowlThing(sK146)
| spl148_12 ),
inference(avatar_component_clause,[],[f1380]) ).
fof(f1382,plain,
( ~ spl148_1
| ~ spl148_2
| ~ spl148_3
| ~ spl148_4
| ~ spl148_5
| ~ spl148_6
| ~ spl148_7
| ~ spl148_8
| spl148_9
| ~ spl148_10
| spl148_11
| ~ spl148_12 ),
inference(avatar_split_clause,[],[f1344,f1380,f1377,f1374,f1371,f1368,f1365,f1362,f1359,f1356,f1353,f1350,f1347]) ).
fof(f1384,plain,
( xsd_integer(sK147)
| ~ spl148_10 ),
inference(avatar_component_clause,[],[f1374]) ).
fof(f1385,plain,
( ~ spl148_1
| ~ spl148_2
| ~ spl148_3
| ~ spl148_4
| ~ spl148_5
| ~ spl148_6
| ~ spl148_7
| ~ spl148_8
| ~ spl148_9
| spl148_10
| spl148_11
| ~ spl148_12 ),
inference(avatar_split_clause,[],[f1345,f1380,f1377,f1374,f1371,f1368,f1365,f1362,f1359,f1356,f1353,f1350,f1347]) ).
fof(f1387,plain,
cC46(iV3102),
inference(resolution,[],[f1325,f1327]) ).
fof(f1388,plain,
cC216(iV3102),
inference(resolution,[],[f1326,f1327]) ).
fof(f1389,plain,
cC30(iV3102),
inference(resolution,[],[f1387,f1192]) ).
fof(f1390,plain,
cC44(iV3102),
inference(resolution,[],[f1387,f1191]) ).
fof(f1391,plain,
cC64(iV3102),
inference(resolution,[],[f1388,f1127]) ).
fof(f1392,plain,
( $false
| spl148_1 ),
inference(resolution,[],[f1389,f1348]) ).
fof(f1393,plain,
cC28(iV3102),
inference(resolution,[],[f1389,f1153]) ).
fof(f1394,plain,
cC14(iV3102),
inference(resolution,[],[f1389,f1152]) ).
fof(f1395,plain,
spl148_1,
inference(avatar_contradiction_clause,[],[f1392]) ).
fof(f1396,plain,
( $false
| spl148_2 ),
inference(resolution,[],[f1351,f824]) ).
fof(f1397,plain,
spl148_2,
inference(avatar_contradiction_clause,[],[f1396]) ).
fof(f1399,plain,
( $false
| spl148_3 ),
inference(resolution,[],[f1393,f1354]) ).
fof(f1401,plain,
spl148_3,
inference(avatar_contradiction_clause,[],[f1399]) ).
fof(f1402,plain,
( $false
| spl148_4 ),
inference(resolution,[],[f1357,f1387]) ).
fof(f1403,plain,
spl148_4,
inference(avatar_contradiction_clause,[],[f1402]) ).
fof(f1404,plain,
( $false
| spl148_5 ),
inference(resolution,[],[f1360,f1391]) ).
fof(f1405,plain,
spl148_5,
inference(avatar_contradiction_clause,[],[f1404]) ).
fof(f1406,plain,
( $false
| spl148_6 ),
inference(resolution,[],[f1363,f1388]) ).
fof(f1407,plain,
spl148_6,
inference(avatar_contradiction_clause,[],[f1406]) ).
fof(f1408,plain,
( $false
| spl148_7 ),
inference(resolution,[],[f1366,f1390]) ).
fof(f1409,plain,
spl148_7,
inference(avatar_contradiction_clause,[],[f1408]) ).
fof(f1410,plain,
( $false
| spl148_8 ),
inference(resolution,[],[f1394,f1369]) ).
fof(f1412,plain,
spl148_8,
inference(avatar_contradiction_clause,[],[f1410]) ).
fof(f1413,plain,
( $false
| spl148_12 ),
inference(resolution,[],[f1381,f824]) ).
fof(f1414,plain,
spl148_12,
inference(avatar_contradiction_clause,[],[f1413]) ).
fof(f1415,plain,
( xsd_string(sK147)
| spl148_10 ),
inference(resolution,[],[f1375,f826]) ).
fof(f1416,plain,
( spl148_9
| spl148_10 ),
inference(avatar_split_clause,[],[f1415,f1374,f1371]) ).
fof(f1417,plain,
( $false
| ~ spl148_11 ),
inference(resolution,[],[f1378,f823]) ).
fof(f1418,plain,
~ spl148_11,
inference(avatar_contradiction_clause,[],[f1417]) ).
fof(f1419,plain,
( ~ xsd_string(sK147)
| ~ spl148_10 ),
inference(resolution,[],[f1384,f825]) ).
fof(f1420,plain,
( ~ spl148_9
| ~ spl148_10 ),
inference(avatar_split_clause,[],[f1419,f1374,f1371]) ).
cnf(s1,plain,
( ~ spl148_1
| ~ spl148_2
| ~ spl148_3
| ~ spl148_4
| ~ spl148_5
| ~ spl148_6
| ~ spl148_7
| ~ spl148_8
| spl148_9
| ~ spl148_10
| spl148_11
| ~ spl148_12 ),
inference(sat_conversion,[],[f1382]) ).
cnf(s2,plain,
( ~ spl148_1
| ~ spl148_2
| ~ spl148_3
| ~ spl148_4
| ~ spl148_5
| ~ spl148_6
| ~ spl148_7
| ~ spl148_8
| ~ spl148_9
| spl148_10
| spl148_11
| ~ spl148_12 ),
inference(sat_conversion,[],[f1385]) ).
cnf(s3,plain,
spl148_1,
inference(sat_conversion,[],[f1395]) ).
cnf(s4,plain,
spl148_2,
inference(sat_conversion,[],[f1397]) ).
cnf(s5,plain,
spl148_3,
inference(sat_conversion,[],[f1401]) ).
cnf(s6,plain,
spl148_4,
inference(sat_conversion,[],[f1403]) ).
cnf(s7,plain,
spl148_5,
inference(sat_conversion,[],[f1405]) ).
cnf(s8,plain,
spl148_6,
inference(sat_conversion,[],[f1407]) ).
cnf(s9,plain,
spl148_7,
inference(sat_conversion,[],[f1409]) ).
cnf(s10,plain,
spl148_8,
inference(sat_conversion,[],[f1412]) ).
cnf(s11,plain,
spl148_12,
inference(sat_conversion,[],[f1414]) ).
cnf(s12,plain,
( spl148_9
| spl148_10 ),
inference(sat_conversion,[],[f1416]) ).
cnf(s13,plain,
~ spl148_11,
inference(sat_conversion,[],[f1418]) ).
cnf(s14,plain,
( ~ spl148_9
| ~ spl148_10 ),
inference(sat_conversion,[],[f1420]) ).
cnf(s15,plain,
( ~ spl148_9
| spl148_10 ),
inference(rat,[],[s2,s11,s13,s10,s9,s8,s7,s6,s5,s4,s3]) ).
cnf(s16,plain,
( spl148_9
| ~ spl148_10 ),
inference(rat,[],[s1,s11,s13,s10,s9,s8,s7,s6,s5,s4,s3]) ).
cnf(s17,plain,
spl148_9,
inference(rat,[],[s16,s12]) ).
cnf(s18,plain,
~ spl148_10,
inference(rat,[],[s14,s17]) ).
cnf(s19,plain,
$false,
inference(rat,[],[s15,s18,s17]) ).
fof(f1421,plain,
$false,
inference(avatar_sat_refutation,[],[s19]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS157+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n018.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 13:34:23 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.95/1.31 % (2357655)Detected formulas, will run a generic FOF schedule.
% 2.95/1.31 % (2357663)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2107756565:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.95/1.31 % (2357663)Refutation not found, incomplete strategy
% 2.95/1.31 % (2357663)------------------------------
% 2.95/1.31 % (2357663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.95/1.31 % (2357663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.95/1.31 % (2357663)CaDiCaL version: 2.1.3
% 2.95/1.31 % (2357663)Termination reason: Refutation not found, incomplete strategy
% 2.95/1.31 % (2357663)Time elapsed: 0.001 s
% 2.95/1.31 % (2357663)Peak memory usage: 87 MB
% 2.95/1.31 % (2357663)Instructions burned: 1 (million)
% 2.95/1.31 % (2357660)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3330894648:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.95/1.31 % (2357661)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3740549987:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.95/1.31 % (2357662)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3411633533:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.95/1.31 % (2357664)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3391078923:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.95/1.31 % (2357666)dis-21_1_sil=8000:lcm=predicate:random_seed=3950561917:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.95/1.31 % (2357664)Refutation not found, incomplete strategy
% 2.95/1.31 % (2357664)------------------------------
% 2.95/1.31 % (2357664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.95/1.31 % (2357664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.95/1.31 % (2357664)CaDiCaL version: 2.1.3
% 2.95/1.31 % (2357664)Termination reason: Refutation not found, incomplete strategy
% 2.95/1.31 % (2357664)Time elapsed: 0.001 s
% 2.95/1.31 % (2357664)Peak memory usage: 87 MB
% 2.95/1.31 % (2357664)Instructions burned: 1 (million)
% 2.95/1.31 % (2357665)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=968782195:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.95/1.31 % (2357666)First to succeed.
% 2.95/1.31 % (2357666)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2357655"
% 2.95/1.31 % (2357665)Also succeeded, but the first one will report.
% 2.95/1.31 % (2357663)------------------------------
% 2.95/1.31 % (2357663)------------------------------
% 2.95/1.31 % (2357674)lrs+10_1_sil=8000:sp=occurrence:random_seed=2851940045:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 2.95/1.31 % (2357674)Also succeeded, but the first one will report.
% 2.95/1.31 % (2357664)------------------------------
% 2.95/1.31 % (2357664)------------------------------
% 2.95/1.31 % (2357666)Refutation found. Thanks to Tanya!
% 2.95/1.31 % SZS status Theorem for theBenchmark
% 2.95/1.31 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/1.50 % (2357666)------------------------------
% 0.17/1.50 % (2357666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/1.50 % (2357666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/1.50 % (2357666)CaDiCaL version: 2.1.3
% 0.17/1.50 % (2357666)Termination reason: Refutation
% 0.17/1.50 % (2357666)Time elapsed: 0.010 s
% 0.17/1.50 % (2357666)Peak memory usage: 90 MB
% 0.17/1.50 % (2357666)Instructions burned: 15 (million)
% 0.17/1.50 % (2357666)------------------------------
% 0.17/1.50 % (2357666)------------------------------
% 0.17/1.50 % (2357655)Success in time 0.446 s
% 0.17/1.50 % Vampire exiting
%------------------------------------------------------------------------------