%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN155-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:49:47 PM UTC 2026
% Result : Unsatisfiable 0.66s 0.95s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 37
% Syntax : Number of formulae : 122 ( 33 unt; 16 def)
% Number of atoms : 251 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 257 ( 128 ~; 113 |; 0 &)
% ( 16 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 34 ( 33 usr; 17 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 66 ( 0 sgn 66 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
r0(b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_9) ).
fof(f14,axiom,
! [X0] : p0(b,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_14) ).
fof(f17,axiom,
! [X0] : q0(X0,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_17) ).
fof(f18,axiom,
p0(c,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_18) ).
fof(f27,axiom,
m0(e,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_27) ).
fof(f30,axiom,
n0(e,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_30) ).
fof(f34,axiom,
n0(c,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_34) ).
fof(f41,axiom,
! [X2,X3,X0,X1] :
( l1(X0,X1)
| ~ p0(X2,X0)
| ~ r0(X3)
| ~ m0(X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_003) ).
fof(f83,axiom,
( n1(d,d,d)
| ~ q0(d,d) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_045) ).
fof(f123,axiom,
! [X0,X1] :
( p1(X0,X0,X0)
| ~ p0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_085) ).
fof(f133,axiom,
! [X0,X1] :
( q1(X0,X1,X1)
| ~ p0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_095) ).
fof(f175,axiom,
! [X2,X0,X1] :
( ~ p1(X1,X2,X0)
| n2(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_137) ).
fof(f203,axiom,
! [X2,X0,X1] :
( p2(X0,X0,X0)
| ~ q1(X1,X2,X1)
| ~ p2(X1,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_165) ).
fof(f209,axiom,
! [X0,X1] :
( p2(X0,X0,X0)
| ~ n1(X1,X1,X1)
| ~ p0(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_171) ).
fof(f224,axiom,
! [X0,X1] :
( q2(X0,X0,X1)
| ~ l1(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_186) ).
fof(f274,axiom,
! [X0] :
( m3(X0,X0,X0)
| ~ n2(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_236) ).
fof(f278,axiom,
! [X2,X0,X1] :
( ~ p2(X1,X2,X0)
| n3(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_240) ).
fof(f293,axiom,
! [X2,X0,X1] :
( ~ q2(X2,X0,X1)
| q3(X0,X1)
| ~ n0(X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_255) ).
fof(f312,axiom,
( k4(c)
| ~ n0(c,d)
| ~ q3(e,b)
| ~ n3(e) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_274) ).
fof(f322,axiom,
! [X0,X1] :
( n4(X0,X0)
| ~ k4(X1)
| ~ m3(X0,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_284) ).
fof(f369,negated_conjecture,
! [X0] : ~ n4(X0,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
fof(f579,definition,
( spl0_62
<=> ! [X0] :
( m3(X0,X0,X0)
| ~ n2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f580,plain,
( ! [X0] :
( m3(X0,X0,X0)
| ~ n2(X0) )
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f579]) ).
fof(f695,definition,
( spl0_95
<=> ! [X1] : ~ p0(X1,X1) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f696,plain,
( ! [X1] : ~ p0(X1,X1)
| ~ spl0_95 ),
inference(avatar_component_clause,[],[f695]) ).
fof(f899,plain,
spl0_62,
inference(avatar_split_clause,[],[f274,f579]) ).
fof(f926,definition,
( spl0_159
<=> n3(e) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f927,plain,
( ~ n3(e)
| spl0_159 ),
inference(avatar_component_clause,[],[f926]) ).
fof(f929,definition,
( spl0_160
<=> q3(e,b) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f930,plain,
( ~ q3(e,b)
| spl0_160 ),
inference(avatar_component_clause,[],[f929]) ).
fof(f932,definition,
( spl0_161
<=> n0(c,d) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f933,plain,
( ~ n0(c,d)
| spl0_161 ),
inference(avatar_component_clause,[],[f932]) ).
fof(f935,definition,
( spl0_162
<=> k4(c) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f936,plain,
( k4(c)
| ~ spl0_162 ),
inference(avatar_component_clause,[],[f935]) ).
fof(f937,plain,
( ~ spl0_159
| ~ spl0_160
| ~ spl0_161
| spl0_162 ),
inference(avatar_split_clause,[],[f312,f935,f932,f929,f926]) ).
fof(f1133,definition,
( spl0_217
<=> ! [X3] : ~ r0(X3) ),
introduced(definition,[new_symbols(definition,[spl0_217])],[avatar_definition]) ).
fof(f1134,plain,
( ! [X3] : ~ r0(X3)
| ~ spl0_217 ),
inference(avatar_component_clause,[],[f1133]) ).
fof(f1136,definition,
( spl0_218
<=> ! [X2,X0,X1] :
( l1(X0,X1)
| ~ m0(X1,X0,X2)
| ~ p0(X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_218])],[avatar_definition]) ).
fof(f1137,plain,
( ! [X2,X0,X1] :
( ~ m0(X1,X0,X2)
| l1(X0,X1)
| ~ p0(X2,X0) )
| ~ spl0_218 ),
inference(avatar_component_clause,[],[f1136]) ).
fof(f1138,plain,
( spl0_217
| spl0_218 ),
inference(avatar_split_clause,[],[f41,f1136,f1133]) ).
fof(f1200,definition,
( spl0_235
<=> q0(d,d) ),
introduced(definition,[new_symbols(definition,[spl0_235])],[avatar_definition]) ).
fof(f1201,plain,
( ~ q0(d,d)
| spl0_235 ),
inference(avatar_component_clause,[],[f1200]) ).
fof(f1203,definition,
( spl0_236
<=> n1(d,d,d) ),
introduced(definition,[new_symbols(definition,[spl0_236])],[avatar_definition]) ).
fof(f1204,plain,
( n1(d,d,d)
| ~ spl0_236 ),
inference(avatar_component_clause,[],[f1203]) ).
fof(f1205,plain,
( ~ spl0_235
| spl0_236 ),
inference(avatar_split_clause,[],[f83,f1203,f1200]) ).
fof(f1231,definition,
( spl0_243
<=> ! [X2,X1] :
( ~ q1(X1,X2,X1)
| ~ p2(X1,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_243])],[avatar_definition]) ).
fof(f1232,plain,
( ! [X2,X1] :
( ~ p2(X1,X1,X2)
| ~ q1(X1,X2,X1) )
| ~ spl0_243 ),
inference(avatar_component_clause,[],[f1231]) ).
fof(f1234,definition,
( spl0_244
<=> ! [X0] : p2(X0,X0,X0) ),
introduced(definition,[new_symbols(definition,[spl0_244])],[avatar_definition]) ).
fof(f1235,plain,
( ! [X0] : p2(X0,X0,X0)
| ~ spl0_244 ),
inference(avatar_component_clause,[],[f1234]) ).
fof(f1236,plain,
( spl0_243
| spl0_244 ),
inference(avatar_split_clause,[],[f203,f1234,f1231]) ).
fof(f1238,definition,
( spl0_245
<=> ! [X1] : ~ n1(X1,X1,X1) ),
introduced(definition,[new_symbols(definition,[spl0_245])],[avatar_definition]) ).
fof(f1239,plain,
( ! [X1] : ~ n1(X1,X1,X1)
| ~ spl0_245 ),
inference(avatar_component_clause,[],[f1238]) ).
fof(f1241,definition,
( spl0_246
<=> ! [X0] :
( p2(X0,X0,X0)
| ~ p0(X0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_246])],[avatar_definition]) ).
fof(f1242,plain,
( ! [X0] :
( p2(X0,X0,X0)
| ~ p0(X0,X0) )
| ~ spl0_246 ),
inference(avatar_component_clause,[],[f1241]) ).
fof(f1243,plain,
( spl0_245
| spl0_246 ),
inference(avatar_split_clause,[],[f209,f1241,f1238]) ).
fof(f1309,definition,
( spl0_265
<=> ! [X1] : ~ k4(X1) ),
introduced(definition,[new_symbols(definition,[spl0_265])],[avatar_definition]) ).
fof(f1310,plain,
( ! [X1] : ~ k4(X1)
| ~ spl0_265 ),
inference(avatar_component_clause,[],[f1309]) ).
fof(f1312,definition,
( spl0_266
<=> ! [X0] :
( n4(X0,X0)
| ~ m3(X0,X0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_266])],[avatar_definition]) ).
fof(f1313,plain,
( ! [X0] :
( ~ m3(X0,X0,X0)
| n4(X0,X0) )
| ~ spl0_266 ),
inference(avatar_component_clause,[],[f1312]) ).
fof(f1314,plain,
( spl0_265
| spl0_266 ),
inference(avatar_split_clause,[],[f322,f1312,f1309]) ).
fof(f1411,plain,
( $false
| ~ spl0_217 ),
inference(resolution,[],[f1134,f9]) ).
fof(f1414,plain,
~ spl0_217,
inference(avatar_contradiction_clause,[],[f1411]) ).
fof(f1415,plain,
( $false
| ~ spl0_95 ),
inference(resolution,[],[f696,f14]) ).
fof(f1416,plain,
~ spl0_95,
inference(avatar_contradiction_clause,[],[f1415]) ).
fof(f1423,plain,
( $false
| spl0_235 ),
inference(forward_subsumption_resolution,[],[f1201,f17]) ).
fof(f1424,plain,
spl0_235,
inference(avatar_contradiction_clause,[],[f1423]) ).
fof(f1442,plain,
( $false
| ~ spl0_236
| ~ spl0_245 ),
inference(resolution,[],[f1239,f1204]) ).
fof(f1443,plain,
( ~ spl0_236
| ~ spl0_245 ),
inference(avatar_contradiction_clause,[],[f1442]) ).
fof(f1649,plain,
! [X0,X1] :
( ~ p0(X0,X1)
| n2(X1) ),
inference(resolution,[],[f123,f175]) ).
fof(f1678,plain,
! [X0] : n2(X0),
inference(resolution,[],[f1649,f14]) ).
fof(f1942,plain,
( ! [X0] :
( ~ q1(X0,X0,X0)
| ~ p0(X0,X0) )
| ~ spl0_243
| ~ spl0_246 ),
inference(resolution,[],[f1232,f1242]) ).
fof(f1951,plain,
( ! [X0] : ~ p0(X0,X0)
| ~ spl0_243
| ~ spl0_246 ),
inference(forward_subsumption_resolution,[],[f1942,f133]) ).
fof(f1958,plain,
( spl0_95
| ~ spl0_243
| ~ spl0_246 ),
inference(avatar_split_clause,[],[f1951,f1241,f1231,f695]) ).
fof(f1961,plain,
( ! [X0] : n3(X0)
| ~ spl0_244 ),
inference(resolution,[],[f1235,f278]) ).
fof(f2286,plain,
! [X0,X1] :
( q3(X0,X1)
| ~ n0(X0,X0)
| ~ l1(X1,X0) ),
inference(resolution,[],[f293,f224]) ).
fof(f2346,plain,
( ~ n0(e,e)
| ~ l1(b,e)
| spl0_160 ),
inference(resolution,[],[f2286,f930]) ).
fof(f2367,plain,
( l1(b,e)
| ~ p0(c,b)
| ~ spl0_218 ),
inference(resolution,[],[f1137,f27]) ).
fof(f2407,plain,
( ~ l1(b,e)
| spl0_160 ),
inference(forward_subsumption_resolution,[],[f2346,f30]) ).
fof(f2408,plain,
( l1(b,e)
| ~ spl0_218 ),
inference(forward_subsumption_resolution,[],[f2367,f18]) ).
fof(f2449,plain,
( $false
| spl0_160
| ~ spl0_218 ),
inference(forward_subsumption_resolution,[],[f2407,f2408]) ).
fof(f2450,plain,
( spl0_160
| ~ spl0_218 ),
inference(avatar_contradiction_clause,[],[f2449]) ).
fof(f2451,plain,
( $false
| spl0_159
| ~ spl0_244 ),
inference(forward_subsumption_resolution,[],[f927,f1961]) ).
fof(f2452,plain,
( spl0_159
| ~ spl0_244 ),
inference(avatar_contradiction_clause,[],[f2451]) ).
fof(f2453,plain,
( $false
| spl0_161 ),
inference(forward_subsumption_resolution,[],[f933,f34]) ).
fof(f2454,plain,
spl0_161,
inference(avatar_contradiction_clause,[],[f2453]) ).
fof(f2455,plain,
( $false
| ~ spl0_162
| ~ spl0_265 ),
inference(forward_subsumption_resolution,[],[f936,f1310]) ).
fof(f2456,plain,
( ~ spl0_162
| ~ spl0_265 ),
inference(avatar_contradiction_clause,[],[f2455]) ).
fof(f2459,plain,
( ! [X0] :
( n4(X0,X0)
| ~ n2(X0) )
| ~ spl0_62
| ~ spl0_266 ),
inference(resolution,[],[f1313,f580]) ).
fof(f2474,plain,
( ! [X0] : n4(X0,X0)
| ~ spl0_62
| ~ spl0_266 ),
inference(forward_subsumption_resolution,[],[f2459,f1678]) ).
fof(f2481,plain,
( $false
| ~ spl0_62
| ~ spl0_266 ),
inference(resolution,[],[f2474,f369]) ).
fof(f2482,plain,
( ~ spl0_62
| ~ spl0_266 ),
inference(avatar_contradiction_clause,[],[f2481]) ).
cnf(s75,plain,
spl0_62,
inference(sat_conversion,[],[f899]) ).
cnf(s80,plain,
( ~ spl0_159
| ~ spl0_160
| ~ spl0_161
| spl0_162 ),
inference(sat_conversion,[],[f937]) ).
cnf(s111,plain,
( spl0_217
| spl0_218 ),
inference(sat_conversion,[],[f1138]) ).
cnf(s124,plain,
( ~ spl0_235
| spl0_236 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s131,plain,
( spl0_243
| spl0_244 ),
inference(sat_conversion,[],[f1236]) ).
cnf(s132,plain,
( spl0_245
| spl0_246 ),
inference(sat_conversion,[],[f1243]) ).
cnf(s142,plain,
( spl0_265
| spl0_266 ),
inference(sat_conversion,[],[f1314]) ).
cnf(s165,plain,
~ spl0_217,
inference(sat_conversion,[],[f1414]) ).
cnf(s166,plain,
~ spl0_95,
inference(sat_conversion,[],[f1416]) ).
cnf(s170,plain,
spl0_235,
inference(sat_conversion,[],[f1424]) ).
cnf(s179,plain,
( ~ spl0_236
| ~ spl0_245 ),
inference(sat_conversion,[],[f1443]) ).
cnf(s292,plain,
( spl0_95
| ~ spl0_243
| ~ spl0_246 ),
inference(sat_conversion,[],[f1958]) ).
cnf(s346,plain,
( spl0_160
| ~ spl0_218 ),
inference(sat_conversion,[],[f2450]) ).
cnf(s347,plain,
( spl0_159
| ~ spl0_244 ),
inference(sat_conversion,[],[f2452]) ).
cnf(s348,plain,
spl0_161,
inference(sat_conversion,[],[f2454]) ).
cnf(s349,plain,
( ~ spl0_162
| ~ spl0_265 ),
inference(sat_conversion,[],[f2456]) ).
cnf(s352,plain,
( ~ spl0_62
| ~ spl0_266 ),
inference(sat_conversion,[],[f2482]) ).
cnf(s371,plain,
spl0_236,
inference(rat,[],[s124,s170]) ).
cnf(s372,plain,
~ spl0_245,
inference(rat,[],[s179,s371]) ).
cnf(s373,plain,
spl0_246,
inference(rat,[],[s132,s372]) ).
cnf(s374,plain,
~ spl0_243,
inference(rat,[],[s292,s166,s373]) ).
cnf(s376,plain,
spl0_244,
inference(rat,[],[s131,s374]) ).
cnf(s377,plain,
spl0_159,
inference(rat,[],[s347,s376]) ).
cnf(s390,plain,
spl0_218,
inference(rat,[],[s111,s165]) ).
cnf(s391,plain,
spl0_160,
inference(rat,[],[s346,s390]) ).
cnf(s409,plain,
spl0_162,
inference(rat,[],[s80,s348,s391,s377]) ).
cnf(s410,plain,
~ spl0_265,
inference(rat,[],[s349,s409]) ).
cnf(s411,plain,
spl0_266,
inference(rat,[],[s142,s410]) ).
cnf(s412,plain,
~ spl0_62,
inference(rat,[],[s352,s411]) ).
cnf(s414,plain,
$false,
inference(rat,[],[s75,s412]) ).
fof(f2483,plain,
$false,
inference(avatar_sat_refutation,[],[s414]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN155-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n014.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 15:37:01 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 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
% 0.66/0.95 % (1859214)Input is clausal, will run a generic CNF schedule.
% 0.66/0.95 % (1859223)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3674514179:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 0.66/0.95 % (1859223)First to succeed.
% 0.66/0.95 % (1859223)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1859214"
% 0.66/0.95 % (1859221)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2562511655:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 0.66/0.95 % (1859224)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=88034917:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 0.66/0.95 % (1859219)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=845735765:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 0.66/0.95 % (1859220)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1349914929:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 0.66/0.95 % (1859225)dis-21_1_sil=8000:lcm=predicate:random_seed=198379234:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 0.66/0.95 % (1859222)lrs+10_1_sil=8000:sp=occurrence:random_seed=1924986778:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 0.66/0.95 % (1859224)Also succeeded, but the first one will report.
% 0.66/0.95 % (1859222)Refutation not found, incomplete strategy
% 0.66/0.95 % (1859222)------------------------------
% 0.66/0.95 % (1859222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.66/0.95 % (1859222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.66/0.95 % (1859222)CaDiCaL version: 2.1.3
% 0.66/0.95 % (1859222)Termination reason: Refutation not found, incomplete strategy
% 0.66/0.95 % (1859222)Time elapsed: 0.019 s
% 0.66/0.95 % (1859222)Peak memory usage: 89 MB
% 0.66/0.95 % (1859222)Instructions burned: 26 (million)
% 0.66/0.95 % (1859225)Also succeeded, but the first one will report.
% 0.66/0.95 % (1859223)Refutation found. Thanks to Tanya!
% 0.66/0.95 % SZS status Unsatisfiable for theBenchmark
% 0.66/0.95 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/1.13 % (1859223)------------------------------
% 0.20/1.13 % (1859223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/1.13 % (1859223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/1.13 % (1859223)CaDiCaL version: 2.1.3
% 0.20/1.13 % (1859223)Termination reason: Refutation
% 0.20/1.13 % (1859223)Time elapsed: 0.015 s
% 0.20/1.13 % (1859223)Peak memory usage: 90 MB
% 0.20/1.13 % (1859223)Instructions burned: 40 (million)
% 0.20/1.13 % (1859223)------------------------------
% 0.20/1.13 % (1859223)------------------------------
% 0.20/1.13 % (1859214)Success in time 0.288 s
% 0.20/1.13 % Vampire exiting
%------------------------------------------------------------------------------