%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN542-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.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 02:00:54 PM UTC 2026
% Result : Satisfiable 3.14s 1.14s
% Output : Saturation 3.91s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u293,negated_conjecture,
( ~ c4_1(X2)
| c5_1(X2)
| c1_1(X2) ) ).
cnf(u299,negated_conjecture,
ndr1_0 ).
cnf(u310,negated_conjecture,
( ~ c0_1(X1)
| c5_1(X1)
| c4_1(X1) ) ).
cnf(u317,negated_conjecture,
( ~ c2_1(X2)
| c5_1(X2)
| c0_1(X2) ) ).
cnf(u327,negated_conjecture,
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ).
cnf(u343,negated_conjecture,
( ~ c0_1(X0)
| c4_1(X0)
| ~ c5_1(X0) ) ).
cnf(u347,negated_conjecture,
~ hskp8 ).
cnf(u351,negated_conjecture,
( ~ c5_1(X1)
| ~ c1_1(X1)
| ~ c4_1(X1) ) ).
cnf(u364,negated_conjecture,
( ~ c0_1(X0)
| c4_1(X0)
| c1_1(X0) ) ).
cnf(u368,negated_conjecture,
~ hskp22 ).
cnf(u375,negated_conjecture,
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u379,negated_conjecture,
~ hskp21 ).
cnf(u383,negated_conjecture,
( ~ c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) ) ).
cnf(u393,negated_conjecture,
( c4_1(X1)
| c1_1(X1)
| c3_1(X1) ) ).
cnf(u403,negated_conjecture,
( ~ c4_1(X0)
| c5_1(X0)
| ~ c1_1(X0) ) ).
cnf(u407,negated_conjecture,
~ hskp37 ).
cnf(u414,negated_conjecture,
( ~ c4_1(X0)
| c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u418,negated_conjecture,
~ hskp23 ).
cnf(u422,negated_conjecture,
( ~ c2_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ).
cnf(u429,negated_conjecture,
~ hskp19 ).
cnf(u433,negated_conjecture,
( ~ c2_1(X1)
| c4_1(X1)
| c1_1(X1) ) ).
cnf(u437,negated_conjecture,
~ hskp12 ).
cnf(u444,negated_conjecture,
( ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u448,negated_conjecture,
~ hskp4 ).
cnf(u457,negated_conjecture,
hskp2 ).
cnf(u463,negated_conjecture,
( ~ c2_1(X0)
| ~ c4_1(X0)
| ~ c3_1(X0) ) ).
cnf(u467,negated_conjecture,
~ hskp1 ).
cnf(u474,negated_conjecture,
( ~ c0_1(X0)
| ~ c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u478,negated_conjecture,
~ hskp53 ).
cnf(u482,negated_conjecture,
( ~ c3_1(X1)
| c5_1(X1)
| c4_1(X1) ) ).
cnf(u490,negated_conjecture,
hskp31 ).
cnf(u500,negated_conjecture,
~ hskp26 ).
cnf(u507,negated_conjecture,
( ~ c1_1(X0)
| c2_1(X0)
| ~ c4_1(X0) ) ).
cnf(u512,negated_conjecture,
hskp24 ).
cnf(u518,negated_conjecture,
( ~ c2_1(X0)
| c4_1(X0)
| c3_1(X0) ) ).
cnf(u522,negated_conjecture,
~ hskp20 ).
cnf(u526,negated_conjecture,
( ~ c0_1(X1)
| c5_1(X1)
| c1_1(X1) ) ).
cnf(u530,negated_conjecture,
~ hskp49 ).
cnf(u537,negated_conjecture,
( ~ c0_1(X0)
| ~ c5_1(X0)
| ~ c1_1(X0) ) ).
cnf(u541,negated_conjecture,
~ hskp25 ).
cnf(u545,negated_conjecture,
( ~ c3_1(X0)
| c4_1(X0)
| c2_1(X0) ) ).
cnf(u549,negated_conjecture,
~ hskp16 ).
cnf(u558,negated_conjecture,
hskp0 ).
cnf(u561,negated_conjecture,
( c4_1(X1)
| c1_1(X1)
| c2_1(X1) ) ).
cnf(u565,negated_conjecture,
~ hskp5 ).
cnf(u569,negated_conjecture,
( ~ c2_1(X1)
| c4_1(X1)
| c0_1(X1) ) ).
cnf(u576,negated_conjecture,
~ hskp50 ).
cnf(u583,negated_conjecture,
( ~ c1_1(X0)
| c0_1(X0)
| ~ c4_1(X0) ) ).
cnf(u591,negated_conjecture,
~ hskp39 ).
cnf(u596,negated_conjecture,
~ hskp55 ).
cnf(u601,negated_conjecture,
~ hskp38 ).
cnf(u605,negated_conjecture,
~ hskp34 ).
cnf(u610,negated_conjecture,
~ hskp36 ).
cnf(u614,negated_conjecture,
~ hskp35 ).
cnf(u618,negated_conjecture,
( ~ c0_1(X0)
| c4_1(X0)
| ~ c2_1(X0) ) ).
cnf(u622,negated_conjecture,
~ hskp54 ).
cnf(u627,negated_conjecture,
~ hskp52 ).
cnf(u635,negated_conjecture,
~ hskp30 ).
cnf(u640,negated_conjecture,
hskp29 ).
cnf(u648,negated_conjecture,
hskp11 ).
cnf(u651,negated_conjecture,
~ hskp10 ).
cnf(u659,negated_conjecture,
~ hskp9 ).
cnf(u663,negated_conjecture,
( ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ) ).
cnf(u668,negated_conjecture,
hskp7 ).
cnf(u671,negated_conjecture,
~ hskp6 ).
cnf(u680,negated_conjecture,
hskp33 ).
cnf(u684,negated_conjecture,
~ hskp32 ).
cnf(u688,negated_conjecture,
~ hskp51 ).
cnf(u693,negated_conjecture,
~ hskp27 ).
cnf(u697,negated_conjecture,
( ~ c0_1(X0)
| c4_1(X0)
| c3_1(X0) ) ).
cnf(u702,negated_conjecture,
hskp28 ).
cnf(u706,negated_conjecture,
~ hskp18 ).
cnf(u710,negated_conjecture,
~ hskp17 ).
cnf(u716,negated_conjecture,
hskp13 ).
cnf(u723,negated_conjecture,
~ hskp15 ).
cnf(u727,negated_conjecture,
~ hskp14 ).
cnf(u732,negated_conjecture,
~ hskp3 ).
cnf(u736,negated_conjecture,
( c5_1(X0)
| c0_1(X0)
| c4_1(X0) ) ).
cnf(u741,negated_conjecture,
~ c0_1(a1) ).
cnf(u745,negated_conjecture,
c5_1(a3) ).
cnf(u751,negated_conjecture,
~ c3_1(a3) ).
cnf(u756,negated_conjecture,
~ c0_1(a3) ).
cnf(u761,negated_conjecture,
~ c2_1(a5) ).
cnf(u766,negated_conjecture,
~ c0_1(a5) ).
cnf(u776,negated_conjecture,
~ c4_1(a7) ).
cnf(u781,negated_conjecture,
~ c3_1(a7) ).
cnf(u786,negated_conjecture,
~ c0_1(a8) ).
cnf(u801,negated_conjecture,
~ c4_1(a10) ).
cnf(u806,negated_conjecture,
~ c3_1(a10) ).
cnf(u811,negated_conjecture,
~ c2_1(a10) ).
cnf(u815,negated_conjecture,
c4_1(a11) ).
cnf(u825,negated_conjecture,
c1_1(a12) ).
cnf(u836,negated_conjecture,
~ c1_1(a15) ).
cnf(u841,negated_conjecture,
~ c2_1(a17) ).
cnf(u845,negated_conjecture,
c1_1(a17) ).
cnf(u851,negated_conjecture,
~ c0_1(a17) ).
cnf(u856,negated_conjecture,
~ c3_1(a19) ).
cnf(u861,negated_conjecture,
~ c0_1(a19) ).
cnf(u865,negated_conjecture,
c5_1(a20) ).
cnf(u871,negated_conjecture,
~ c2_1(a20) ).
cnf(u885,negated_conjecture,
c5_1(a22) ).
cnf(u890,negated_conjecture,
c4_1(a22) ).
cnf(u895,negated_conjecture,
c0_1(a22) ).
cnf(u901,negated_conjecture,
~ c1_1(a23) ).
cnf(u961,negated_conjecture,
~ c4_1(a30) ).
cnf(u966,negated_conjecture,
~ c2_1(a30) ).
cnf(u971,negated_conjecture,
~ c0_1(a30) ).
cnf(u976,negated_conjecture,
~ c4_1(a31) ).
cnf(u991,negated_conjecture,
~ c4_1(a34) ).
cnf(u996,negated_conjecture,
~ c0_1(a34) ).
cnf(u1001,negated_conjecture,
~ c3_1(a35) ).
cnf(u1011,negated_conjecture,
~ c3_1(a37) ).
cnf(u1016,negated_conjecture,
~ c2_1(a37) ).
cnf(u1021,negated_conjecture,
~ c1_1(a37) ).
cnf(u1041,negated_conjecture,
~ c3_1(a45) ).
cnf(u1046,negated_conjecture,
~ c2_1(a45) ).
cnf(u1055,negated_conjecture,
c4_1(a49) ).
cnf(u1061,negated_conjecture,
~ c0_1(a49) ).
cnf(u1065,negated_conjecture,
c4_1(a50) ).
cnf(u1071,negated_conjecture,
~ c3_1(a50) ).
cnf(u1076,negated_conjecture,
~ c1_1(a50) ).
cnf(u1095,negated_conjecture,
c5_1(a59) ).
cnf(u1101,negated_conjecture,
~ c2_1(a59) ).
cnf(u1106,negated_conjecture,
~ c0_1(a59) ).
cnf(u1111,negated_conjecture,
~ hskp40 ).
cnf(u1114,negated_conjecture,
c5_1(a61) ).
cnf(u1119,negated_conjecture,
c4_1(a61) ).
cnf(u1124,negated_conjecture,
hskp41 ).
cnf(u1129,negated_conjecture,
~ c4_1(a62) ).
cnf(u1133,negated_conjecture,
hskp42 ).
cnf(u1138,negated_conjecture,
~ c1_1(a66) ).
cnf(u1143,negated_conjecture,
~ hskp43 ).
cnf(u1157,negated_conjecture,
~ hskp44 ).
cnf(u1160,negated_conjecture,
c5_1(a68) ).
cnf(u1166,negated_conjecture,
~ c4_1(a68) ).
cnf(u1171,negated_conjecture,
~ c3_1(a68) ).
cnf(u1176,negated_conjecture,
~ hskp45 ).
cnf(u1184,negated_conjecture,
hskp46 ).
cnf(u1189,negated_conjecture,
~ c1_1(a73) ).
cnf(u1194,negated_conjecture,
~ c0_1(a73) ).
cnf(u1198,negated_conjecture,
hskp47 ).
cnf(u1203,negated_conjecture,
~ c1_1(a75) ).
cnf(u1208,negated_conjecture,
~ hskp48 ).
cnf(u1212,negated_conjecture,
~ c3_1(a76) ).
cnf(u1217,negated_conjecture,
~ c1_1(a76) ).
cnf(u1222,negated_conjecture,
c4_1(a1) ).
cnf(u1227,negated_conjecture,
c2_1(a1) ).
cnf(u1232,negated_conjecture,
c1_1(a5) ).
cnf(u1246,negated_conjecture,
~ c2_1(a7) ).
cnf(u1251,negated_conjecture,
~ c4_1(a8) ).
cnf(u1257,negated_conjecture,
c1_1(a8) ).
cnf(u1267,negated_conjecture,
c3_1(a11) ).
cnf(u1271,negated_conjecture,
~ c1_1(a11) ).
cnf(u1276,negated_conjecture,
~ c2_1(a12) ).
cnf(u1292,negated_conjecture,
c4_1(a15) ).
cnf(u1297,negated_conjecture,
c3_1(a15) ).
cnf(u1302,negated_conjecture,
c5_1(a19) ).
cnf(u1307,negated_conjecture,
c0_1(a20) ).
cnf(u1316,negated_conjecture,
~ c3_1(a23) ).
cnf(u1322,negated_conjecture,
c2_1(a23) ).
cnf(u1362,negated_conjecture,
c1_1(a31) ).
cnf(u1366,negated_conjecture,
~ c0_1(a31) ).
cnf(u1392,negated_conjecture,
c5_1(a34) ).
cnf(u1397,negated_conjecture,
c5_1(a35) ).
cnf(u1402,negated_conjecture,
c2_1(a35) ).
cnf(u1417,negated_conjecture,
c0_1(a45) ).
cnf(u1432,negated_conjecture,
c2_1(a49) ).
cnf(u1452,negated_conjecture,
c0_1(a61) ).
cnf(u1457,negated_conjecture,
c5_1(a62) ).
cnf(u1462,negated_conjecture,
c1_1(a62) ).
cnf(u1467,negated_conjecture,
c5_1(a66) ).
cnf(u1472,negated_conjecture,
c0_1(a66) ).
cnf(u1492,negated_conjecture,
c2_1(a73) ).
cnf(u1497,negated_conjecture,
c5_1(a75) ).
cnf(u1502,negated_conjecture,
c3_1(a75) ).
cnf(u1507,negated_conjecture,
c5_1(a76) ).
cnf(u1616,negated_conjecture,
~ c2_1(a60) ).
cnf(u1621,negated_conjecture,
~ hskp56 ).
cnf(u1625,negated_conjecture,
~ c1_1(a60) ).
cnf(u1631,negated_conjecture,
c0_1(a60) ).
cnf(u1640,negated_conjecture,
~ hskp57 ).
cnf(u1659,negated_conjecture,
~ hskp58 ).
cnf(u1749,negated_conjecture,
~ c0_1(a12) ).
cnf(u1754,negated_conjecture,
c5_1(a12) ).
cnf(u1764,negated_conjecture,
~ c1_1(a61) ).
cnf(u1768,negated_conjecture,
c3_1(a61) ).
cnf(u1779,negated_conjecture,
c1_1(a3) ).
cnf(u1782,negated_conjecture,
~ c2_1(a3) ).
cnf(u1788,negated_conjecture,
~ c1_1(a22) ).
cnf(u1792,negated_conjecture,
~ c2_1(a22) ).
cnf(u1868,negated_conjecture,
c3_1(a22) ).
cnf(u1877,negated_conjecture,
c1_1(a30) ).
cnf(u1892,negated_conjecture,
~ c1_1(a20) ).
cnf(u1896,negated_conjecture,
c3_1(a20) ).
cnf(u1901,negated_conjecture,
c4_1(a20) ).
cnf(u1987,negated_conjecture,
~ c4_1(a3) ).
cnf(u2034,negated_conjecture,
~ c2_1(a50) ).
cnf(u2073,negated_conjecture,
~ c1_1(a45) ).
cnf(u2077,negated_conjecture,
c5_1(a45) ).
cnf(u2117,negated_conjecture,
~ c3_1(a73) ).
cnf(u2122,negated_conjecture,
c4_1(a73) ).
cnf(u2129,negated_conjecture,
~ c1_1(a19) ).
cnf(u2134,negated_conjecture,
c2_1(a19) ).
cnf(u2139,negated_conjecture,
~ c0_1(a62) ).
cnf(u2143,negated_conjecture,
~ c2_1(a62) ).
cnf(u2148,negated_conjecture,
~ c3_1(a62) ).
cnf(u2158,negated_conjecture,
c4_1(a19) ).
cnf(u2261,negated_conjecture,
~ c2_1(a34) ).
cnf(u2265,negated_conjecture,
~ c3_1(a34) ).
cnf(u2603,negated_conjecture,
c4_1(a60) ).
cnf(u2654,negated_conjecture,
~ c2_1(a68) ).
cnf(u2664,negated_conjecture,
~ c2_1(a66) ).
cnf(u2669,negated_conjecture,
c3_1(a66) ).
cnf(u2687,negated_conjecture,
c0_1(a75) ).
cnf(u2690,negated_conjecture,
~ c2_1(a75) ).
cnf(u2577,negated_conjecture,
~ c1_1(a49) ).
cnf(u2380,negated_conjecture,
c5_1(a1) ).
cnf(u2562,negated_conjecture,
c5_1(a49) ).
cnf(u1736,negated_conjecture,
( ~ c3_1(X1)
| ~ c2_1(X1) ) ).
cnf(u2447,negated_conjecture,
( ~ c4_1(X0)
| ~ c1_1(X0) ) ).
cnf(u2172,negated_conjecture,
c5_1(a50) ).
cnf(u2378,negated_conjecture,
( ~ c0_1(X0)
| ~ c1_1(X0) ) ).
cnf(u2333,negated_conjecture,
( ~ c3_1(X1)
| c5_1(X1) ) ).
cnf(u2085,negated_conjecture,
( ~ c2_1(X0)
| c5_1(X0)
| c1_1(X0) ) ).
cnf(u1839,negated_conjecture,
~ c2_1(a11) ).
cnf(u2248,negated_conjecture,
c1_1(a34) ).
cnf(u2235,negated_conjecture,
( ~ c0_1(X1)
| c4_1(X1) ) ).
cnf(u2334,negated_conjecture,
c5_1(a11) ).
cnf(u2611,negated_conjecture,
c5_1(a60) ).
cnf(u2278,negated_conjecture,
c4_1(a45) ).
cnf(u2416,negated_conjecture,
c5_1(a23) ).
cnf(u2739,negated_conjecture,
( ~ c3_1(X0)
| c4_1(X0) ) ).
cnf(u2415,negated_conjecture,
c5_1(a73) ).
cnf(u2222,negated_conjecture,
( c5_1(X0)
| c1_1(X0) ) ).
cnf(u2004,negated_conjecture,
c1_1(a68) ).
cnf(u2507,negated_conjecture,
c4_1(a35) ).
cnf(u2849,negated_conjecture,
~ c1_1(a35) ).
cnf(u2549,negated_conjecture,
( ~ c2_1(X1)
| c4_1(X1) ) ).
cnf(u2748,negated_conjecture,
c4_1(a75) ).
cnf(u1980,negated_conjecture,
~ c2_1(a61) ).
cnf(u2294,negated_conjecture,
( ~ c0_1(X1)
| c5_1(X1) ) ).
cnf(u2007,negated_conjecture,
c1_1(a10) ).
cnf(u2561,negated_conjecture,
~ c2_1(a15) ).
cnf(u1981,negated_conjecture,
( c4_1(X1)
| c1_1(X1) ) ).
cnf(u2388,negated_conjecture,
~ c1_1(a1) ).
cnf(u2391,negated_conjecture,
( ~ c2_1(X2)
| c5_1(X2) ) ).
cnf(u2055,negated_conjecture,
c1_1(a59) ).
cnf(u2136,negated_conjecture,
( ~ c4_1(X2)
| c5_1(X2) ) ).
cnf(u2188,negated_conjecture,
c4_1(a23) ).
cnf(u2735,negated_conjecture,
( ~ c0_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2021,negated_conjecture,
c1_1(a7) ).
cnf(u2675,negated_conjecture,
c4_1(a66) ).
cnf(u2554,negated_conjecture,
c5_1(a15) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN542-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n011.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 16:27:16 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.14/1.14 % (3513480)Input is clausal, will run a generic CNF schedule.
% 3.14/1.14 % (3513491)dis-21_1_sil=8000:lcm=predicate:random_seed=1617616611: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)
% 3.14/1.14 % (3513489)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3053191985:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.14/1.14 % (3513488)lrs+10_1_sil=8000:sp=occurrence:random_seed=1629011849:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.14/1.14 % (3513486)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4163429563:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.14/1.14 % (3513487)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=891835104:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.14/1.14 % (3513485)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=3283436448:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.14/1.14 % (3513491)Instruction limit reached!
% 3.14/1.14 % (3513491)------------------------------
% 3.14/1.14 % (3513491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.14/1.14 % (3513491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.14/1.14 % (3513491)CaDiCaL version: 2.1.3
% 3.14/1.14 % (3513491)Termination reason: Instruction limit
% 3.14/1.14 % (3513491)Termination phase: Saturation
% 3.14/1.14 % (3513491)Time elapsed: 0.040 s
% 3.14/1.14 % (3513491)Peak memory usage: 90 MB
% 3.14/1.14 % (3513491)Instructions burned: 117 (million)
% 3.14/1.14 % (3513488)First to succeed.
% 3.14/1.14 % (3513490)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1275635862:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.14/1.14 % (3513488)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3513480"
% 3.14/1.14 % (3513489)Refutation not found, incomplete strategy
% 3.14/1.14 % (3513489)------------------------------
% 3.14/1.14 % (3513489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.14/1.14 % (3513489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.14/1.14 % (3513489)CaDiCaL version: 2.1.3
% 3.14/1.14 % (3513489)Termination reason: Refutation not found, incomplete strategy
% 3.14/1.14 % (3513489)Time elapsed: 0.053 s
% 3.14/1.14 % (3513489)Peak memory usage: 89 MB
% 3.14/1.14 % (3513489)Instructions burned: 82 (million)
% 3.14/1.14 % (3513490)Instruction limit reached!
% 3.14/1.14 % (3513490)------------------------------
% 3.14/1.14 % (3513490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.14/1.14 % (3513490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.14/1.14 % (3513490)CaDiCaL version: 2.1.3
% 3.14/1.14 % (3513490)Termination reason: Instruction limit
% 3.14/1.14 % (3513490)Termination phase: Saturation
% 3.14/1.14 % (3513490)Time elapsed: 0.115 s
% 3.14/1.14 % (3513490)Peak memory usage: 91 MB
% 3.14/1.14 % (3513490)Instructions burned: 180 (million)
% 3.14/1.14 % (3513498)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1673729916:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 3.14/1.14 % (3513498)Instruction limit reached!
% 3.14/1.14 % (3513498)------------------------------
% 3.14/1.14 % (3513498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.14/1.14 % (3513498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.14/1.14 % (3513498)CaDiCaL version: 2.1.3
% 3.14/1.14 % (3513498)Termination reason: Instruction limit
% 3.14/1.14 % (3513498)Termination phase: Saturation
% 3.14/1.14 % (3513498)Time elapsed: 0.051 s
% 3.14/1.14 % (3513498)Peak memory usage: 90 MB
% 3.14/1.14 % (3513498)Instructions burned: 145 (million)
% 3.14/1.14 % SZS status Satisfiable for theBenchmark
% 3.14/1.14 % SZS output start Saturation.
% See solution above
% 3.91/1.34 % SZS output start Definitions and Model Updates.
% 3.91/1.34 % SZS output end Definitions and Model Updates.
% 3.91/1.34 % (3513488)------------------------------
% 3.91/1.34 % (3513488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.91/1.34 % (3513488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/1.34 % (3513488)CaDiCaL version: 2.1.3
% 3.91/1.34 % (3513488)Termination reason: Satisfiable
% 3.91/1.34 % (3513488)Time elapsed: 0.026 s
% 3.91/1.34 % (3513488)Peak memory usage: 89 MB
% 3.91/1.34 % (3513488)Instructions burned: 40 (million)
% 3.91/1.34 % (3513488)------------------------------
% 3.91/1.34 % (3513488)------------------------------
% 3.91/1.34 % (3513480)Success in time 0.465 s
% 3.91/1.34 % Vampire exiting
%------------------------------------------------------------------------------