%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN453-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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 01:52:10 PM UTC 2026
% Result : Satisfiable 3.01s 1.13s
% Output : Saturation 3.81s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u350,negated_conjecture,
( ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1) ) ).
cnf(u1640,negated_conjecture,
ndr1_0 ).
cnf(u363,negated_conjecture,
( c3_1(X1)
| ~ c1_1(X1)
| c0_1(X1) ) ).
cnf(u376,negated_conjecture,
( c2_1(X0)
| c0_1(X0)
| ~ c1_1(X0) ) ).
cnf(u380,negated_conjecture,
( c3_1(X2)
| c2_1(X2)
| c1_1(X2) ) ).
cnf(u387,negated_conjecture,
hskp0 ).
cnf(u934,negated_conjecture,
~ hskp30 ).
cnf(u890,negated_conjecture,
~ hskp24 ).
cnf(u404,negated_conjecture,
( c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ) ).
cnf(u408,negated_conjecture,
hskp56 ).
cnf(u415,negated_conjecture,
hskp42 ).
cnf(u423,negated_conjecture,
( ~ c3_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ) ).
cnf(u427,negated_conjecture,
hskp10 ).
cnf(u431,negated_conjecture,
hskp20 ).
cnf(u924,negated_conjecture,
~ hskp28 ).
cnf(u919,negated_conjecture,
~ hskp27 ).
cnf(u445,negated_conjecture,
( c3_1(X1)
| c2_1(X1)
| ~ c1_1(X1) ) ).
cnf(u452,negated_conjecture,
hskp54 ).
cnf(u749,negated_conjecture,
~ hskp9 ).
cnf(u462,negated_conjecture,
( c3_1(X1)
| c0_1(X1)
| ~ c2_1(X1) ) ).
cnf(u466,negated_conjecture,
hskp6 ).
cnf(u1355,negated_conjecture,
~ hskp39 ).
cnf(u992,negated_conjecture,
~ hskp38 ).
cnf(u678,negated_conjecture,
~ hskp2 ).
cnf(u485,negated_conjecture,
hskp33 ).
cnf(u495,negated_conjecture,
( c2_1(X1)
| c1_1(X1)
| c0_1(X1) ) ).
cnf(u499,negated_conjecture,
hskp47 ).
cnf(u503,negated_conjecture,
hskp43 ).
cnf(u507,negated_conjecture,
hskp11 ).
cnf(u687,negated_conjecture,
~ hskp3 ).
cnf(u520,negated_conjecture,
( c3_1(X1)
| c1_1(X1)
| c0_1(X1) ) ).
cnf(u525,negated_conjecture,
hskp14 ).
cnf(u727,negated_conjecture,
~ hskp7 ).
cnf(u736,negated_conjecture,
~ hskp8 ).
cnf(u960,negated_conjecture,
~ hskp32 ).
cnf(u1429,negated_conjecture,
~ hskp48 ).
cnf(u548,negated_conjecture,
hskp67 ).
cnf(u552,negated_conjecture,
hskp59 ).
cnf(u866,negated_conjecture,
~ hskp22 ).
cnf(u559,negated_conjecture,
hskp21 ).
cnf(u1036,negated_conjecture,
~ hskp46 ).
cnf(u772,negated_conjecture,
~ hskp12 ).
cnf(u574,negated_conjecture,
hskp44 ).
cnf(u578,negated_conjecture,
hskp1 ).
cnf(u978,negated_conjecture,
~ hskp36 ).
cnf(u585,negated_conjecture,
hskp29 ).
cnf(u1607,negated_conjecture,
~ hskp70 ).
cnf(u592,negated_conjecture,
hskp65 ).
cnf(u899,negated_conjecture,
~ hskp25 ).
cnf(u599,negated_conjecture,
hskp63 ).
cnf(u1123,negated_conjecture,
~ hskp62 ).
cnf(u1533,negated_conjecture,
~ hskp61 ).
cnf(u1118,negated_conjecture,
~ hskp60 ).
cnf(u1065,negated_conjecture,
~ hskp52 ).
cnf(u619,negated_conjecture,
hskp16 ).
cnf(u801,negated_conjecture,
~ hskp15 ).
cnf(u629,negated_conjecture,
hskp51 ).
cnf(u1001,negated_conjecture,
~ hskp40 ).
cnf(u637,negated_conjecture,
hskp37 ).
cnf(u696,negated_conjecture,
~ hskp4 ).
cnf(u1326,negated_conjecture,
~ hskp35 ).
cnf(u973,negated_conjecture,
~ hskp34 ).
cnf(u947,negated_conjecture,
~ hskp31 ).
cnf(u1133,negated_conjecture,
~ hskp64 ).
cnf(u658,negated_conjecture,
( c3_1(X0)
| c0_1(X0)
| c2_1(X0) ) ).
cnf(u1372,negated_conjecture,
~ hskp41 ).
cnf(u667,negated_conjecture,
~ c3_1(a1994) ).
cnf(u671,negated_conjecture,
~ c1_1(a1994) ).
cnf(u676,negated_conjecture,
~ c1_1(a1998) ).
cnf(u690,negated_conjecture,
~ c0_1(a2000) ).
cnf(u3023,negated_conjecture,
c1_1(a2001) ).
cnf(u2945,negated_conjecture,
c2_1(a2001) ).
cnf(u707,negated_conjecture,
~ c3_1(a2001) ).
cnf(u712,negated_conjecture,
~ c0_1(a2006) ).
cnf(u716,negated_conjecture,
~ c1_1(a2006) ).
cnf(u721,negated_conjecture,
~ c1_1(a2009) ).
cnf(u725,negated_conjecture,
~ c0_1(a2009) ).
cnf(u2131,negated_conjecture,
c2_1(a2011) ).
cnf(u734,negated_conjecture,
~ c3_1(a2011) ).
cnf(u2363,negated_conjecture,
c0_1(a2014) ).
cnf(u2385,negated_conjecture,
c2_1(a2014) ).
cnf(u760,negated_conjecture,
~ c3_1(a2014) ).
cnf(u765,negated_conjecture,
~ c0_1(a2015) ).
cnf(u770,negated_conjecture,
~ c1_1(a2016) ).
cnf(u2109,negated_conjecture,
c0_1(a2019) ).
cnf(u779,negated_conjecture,
~ c2_1(a2019) ).
cnf(u783,negated_conjecture,
~ c1_1(a2019) ).
cnf(u787,negated_conjecture,
~ hskp13 ).
cnf(u799,negated_conjecture,
~ c3_1(a2023) ).
cnf(u2020,negated_conjecture,
c0_1(a2031) ).
cnf(u817,negated_conjecture,
~ c2_1(a2032) ).
cnf(u821,negated_conjecture,
~ c1_1(a2032) ).
cnf(u825,negated_conjecture,
~ hskp17 ).
cnf(u832,negated_conjecture,
~ c1_1(a2034) ).
cnf(u1631,negated_conjecture,
hskp18 ).
cnf(u843,negated_conjecture,
~ c1_1(a2036) ).
cnf(u847,negated_conjecture,
~ hskp19 ).
cnf(u855,negated_conjecture,
~ c0_1(a2041) ).
cnf(u860,negated_conjecture,
~ c0_1(a2044) ).
cnf(u864,negated_conjecture,
~ c1_1(a2044) ).
cnf(u873,negated_conjecture,
~ c0_1(a2045) ).
cnf(u877,negated_conjecture,
~ hskp23 ).
cnf(u884,negated_conjecture,
~ c0_1(a2050) ).
cnf(u1787,negated_conjecture,
c2_1(a2050) ).
cnf(u1876,negated_conjecture,
c0_1(a2057) ).
cnf(u897,negated_conjecture,
~ c3_1(a2057) ).
cnf(u906,negated_conjecture,
~ c1_1(a2062) ).
cnf(u914,negated_conjecture,
~ hskp26 ).
cnf(u2328,negated_conjecture,
c0_1(a2069) ).
cnf(u932,negated_conjecture,
~ c1_1(a2079) ).
cnf(u941,negated_conjecture,
~ c0_1(a2080) ).
cnf(u3411,negated_conjecture,
c2_1(a2081) ).
cnf(u954,negated_conjecture,
~ c3_1(a2081) ).
cnf(u958,negated_conjecture,
~ c1_1(a2081) ).
cnf(u3636,negated_conjecture,
c1_1(a2083) ).
cnf(u967,negated_conjecture,
~ c3_1(a2083) ).
cnf(u4216,negated_conjecture,
c2_1(a2083) ).
cnf(u3561,negated_conjecture,
c2_1(a1997) ).
cnf(u990,negated_conjecture,
~ c0_1(a2002) ).
cnf(u1824,negated_conjecture,
c2_1(a2003) ).
cnf(u999,negated_conjecture,
~ c1_1(a2003) ).
cnf(u1004,negated_conjecture,
~ c3_1(a2005) ).
cnf(u2391,negated_conjecture,
c1_1(a2005) ).
cnf(u1013,negated_conjecture,
~ c0_1(a2010) ).
cnf(u1018,negated_conjecture,
~ c0_1(a2017) ).
cnf(u1022,negated_conjecture,
~ c1_1(a2017) ).
cnf(u1027,negated_conjecture,
~ c1_1(a2018) ).
cnf(u1637,negated_conjecture,
hskp45 ).
cnf(u1034,negated_conjecture,
~ c0_1(a2022) ).
cnf(u1039,negated_conjecture,
~ c2_1(a2025) ).
cnf(u1044,negated_conjecture,
~ c3_1(a2026) ).
cnf(u1621,negated_conjecture,
hskp49 ).
cnf(u1051,negated_conjecture,
~ c1_1(a2028) ).
cnf(u1055,negated_conjecture,
~ hskp50 ).
cnf(u1063,negated_conjecture,
~ c0_1(a2030) ).
cnf(u1068,negated_conjecture,
~ c1_1(a2033) ).
cnf(u1076,negated_conjecture,
~ hskp53 ).
cnf(u1079,negated_conjecture,
~ c0_1(a2035) ).
cnf(u1084,negated_conjecture,
~ c0_1(a2037) ).
cnf(u1089,negated_conjecture,
~ c2_1(a2047) ).
cnf(u1096,negated_conjecture,
~ c1_1(a2048) ).
cnf(u1100,negated_conjecture,
~ c3_1(a2048) ).
cnf(u1104,negated_conjecture,
~ hskp58 ).
cnf(u1107,negated_conjecture,
~ c1_1(a2051) ).
cnf(u1116,negated_conjecture,
~ c1_1(a2052) ).
cnf(u4128,negated_conjecture,
c2_1(a2058) ).
cnf(u1131,negated_conjecture,
~ c3_1(a2059) ).
cnf(u1141,negated_conjecture,
~ c3_1(a2063) ).
cnf(u1146,negated_conjecture,
~ c0_1(a2070) ).
cnf(u1150,negated_conjecture,
~ c1_1(a2070) ).
cnf(u1154,negated_conjecture,
~ hskp68 ).
cnf(u1161,negated_conjecture,
~ hskp69 ).
cnf(u1168,negated_conjecture,
~ c2_1(a2074) ).
cnf(u1172,negated_conjecture,
c0_1(a1994) ).
cnf(u1176,negated_conjecture,
c3_1(a1998) ).
cnf(u1180,negated_conjecture,
c0_1(a1998) ).
cnf(u2177,negated_conjecture,
~ c1_1(a1999) ).
cnf(u3035,negated_conjecture,
~ c1_1(a2000) ).
cnf(u1192,negated_conjecture,
c2_1(a2006) ).
cnf(u1196,negated_conjecture,
c3_1(a2009) ).
cnf(u1200,negated_conjecture,
c0_1(a2011) ).
cnf(u1204,negated_conjecture,
c1_1(a2015) ).
cnf(u1208,negated_conjecture,
c3_1(a2015) ).
cnf(u1212,negated_conjecture,
c2_1(a2016) ).
cnf(u1216,negated_conjecture,
c0_1(a2016) ).
cnf(u1736,negated_conjecture,
~ c1_1(a2020) ).
cnf(u1224,negated_conjecture,
c0_1(a2023) ).
cnf(u1228,negated_conjecture,
c2_1(a2023) ).
cnf(u1232,negated_conjecture,
c0_1(a2032) ).
cnf(u1236,negated_conjecture,
c0_1(a2036) ).
cnf(u1240,negated_conjecture,
c3_1(a2036) ).
cnf(u1244,negated_conjecture,
c0_1(a2038) ).
cnf(u1248,negated_conjecture,
c1_1(a2038) ).
cnf(u1252,negated_conjecture,
c3_1(a2041) ).
cnf(u1256,negated_conjecture,
c1_1(a2041) ).
cnf(u1260,negated_conjecture,
c3_1(a2044) ).
cnf(u1264,negated_conjecture,
c2_1(a2045) ).
cnf(u1268,negated_conjecture,
c2_1(a2057) ).
cnf(u1284,negated_conjecture,
c0_1(a2068) ).
cnf(u1288,negated_conjecture,
c2_1(a2069) ).
cnf(u1296,negated_conjecture,
c2_1(a2079) ).
cnf(u1300,negated_conjecture,
c3_1(a2079) ).
cnf(u1304,negated_conjecture,
c0_1(a1993) ).
cnf(u1309,negated_conjecture,
c1_1(a1993) ).
cnf(u1313,negated_conjecture,
c2_1(a1993) ).
cnf(u2679,negated_conjecture,
~ c1_1(a1995) ).
cnf(u1321,negated_conjecture,
c0_1(a1995) ).
cnf(u2197,negated_conjecture,
~ c0_1(a1996) ).
cnf(u1330,negated_conjecture,
c3_1(a1996) ).
cnf(u1334,negated_conjecture,
c2_1(a1996) ).
cnf(u1338,negated_conjecture,
c1_1(a1997) ).
cnf(u1342,negated_conjecture,
c1_1(a2002) ).
cnf(u1346,negated_conjecture,
c3_1(a2002) ).
cnf(u1807,negated_conjecture,
~ c1_1(a2004) ).
cnf(u2226,negated_conjecture,
~ c0_1(a2004) ).
cnf(u1367,negated_conjecture,
c0_1(a2005) ).
cnf(u1371,negated_conjecture,
c0_1(a2007) ).
cnf(u1881,negated_conjecture,
~ c1_1(a2007) ).
cnf(u1380,negated_conjecture,
c3_1(a2007) ).
cnf(u1384,negated_conjecture,
c2_1(a2010) ).
cnf(u1388,negated_conjecture,
c3_1(a2010) ).
cnf(u1392,negated_conjecture,
c2_1(a2017) ).
cnf(u1396,negated_conjecture,
c0_1(a2018) ).
cnf(u1400,negated_conjecture,
c2_1(a2018) ).
cnf(u1404,negated_conjecture,
c3_1(a2022) ).
cnf(u1408,negated_conjecture,
c2_1(a2022) ).
cnf(u1412,negated_conjecture,
c0_1(a2025) ).
cnf(u1420,negated_conjecture,
c0_1(a2026) ).
cnf(u1424,negated_conjecture,
c2_1(a2026) ).
cnf(u1428,negated_conjecture,
c0_1(a2027) ).
cnf(u1437,negated_conjecture,
c1_1(a2027) ).
cnf(u1441,negated_conjecture,
c3_1(a2028) ).
cnf(u1445,negated_conjecture,
c0_1(a2028) ).
cnf(u1449,negated_conjecture,
c2_1(a2029) ).
cnf(u1453,negated_conjecture,
c1_1(a2029) ).
cnf(u1457,negated_conjecture,
c1_1(a2030) ).
cnf(u1461,negated_conjecture,
c2_1(a2030) ).
cnf(u4166,negated_conjecture,
~ c2_1(a2033) ).
cnf(u2334,negated_conjecture,
~ c1_1(a2035) ).
cnf(u1473,negated_conjecture,
c2_1(a2035) ).
cnf(u1477,negated_conjecture,
c3_1(a2037) ).
cnf(u1481,negated_conjecture,
c2_1(a2037) ).
cnf(u1488,negated_conjecture,
~ hskp55 ).
cnf(u1720,negated_conjecture,
~ c1_1(a2046) ).
cnf(u1500,negated_conjecture,
c0_1(a2047) ).
cnf(u1504,negated_conjecture,
c3_1(a2047) ).
cnf(u1508,negated_conjecture,
c0_1(a2048) ).
cnf(u1512,negated_conjecture,
c3_1(a2051) ).
cnf(u1516,negated_conjecture,
c2_1(a2052) ).
cnf(u1520,negated_conjecture,
c0_1(a2052) ).
cnf(u1528,negated_conjecture,
c0_1(a2053) ).
cnf(u1532,negated_conjecture,
c3_1(a2054) ).
cnf(u2418,negated_conjecture,
~ c2_1(a2054) ).
cnf(u2417,negated_conjecture,
~ c1_1(a2054) ).
cnf(u1549,negated_conjecture,
c1_1(a2058) ).
cnf(u1553,negated_conjecture,
c1_1(a2059) ).
cnf(u1557,negated_conjecture,
c2_1(a2059) ).
cnf(u1561,negated_conjecture,
c1_1(a2061) ).
cnf(u1569,negated_conjecture,
c1_1(a2063) ).
cnf(u1573,negated_conjecture,
c0_1(a2063) ).
cnf(u1577,negated_conjecture,
c2_1(a2067) ).
cnf(u1582,negated_conjecture,
c3_1(a2067) ).
cnf(u1586,negated_conjecture,
c0_1(a2067) ).
cnf(u1590,negated_conjecture,
c3_1(a2070) ).
cnf(u1594,negated_conjecture,
c0_1(a2073) ).
cnf(u1598,negated_conjecture,
c1_1(a2073) ).
cnf(u1602,negated_conjecture,
c0_1(a2074) ).
cnf(u1611,negated_conjecture,
c0_1(a2078) ).
cnf(u1615,negated_conjecture,
c2_1(a2078) ).
cnf(u1731,negated_conjecture,
~ c1_1(a2050) ).
cnf(u1735,negated_conjecture,
c0_1(a2020) ).
cnf(u1745,negated_conjecture,
c2_1(a2027) ).
cnf(u1769,negated_conjecture,
~ c1_1(a2010) ).
cnf(u1986,negated_conjecture,
c2_1(a2038) ).
cnf(u1823,negated_conjecture,
~ c0_1(a2003) ).
cnf(u1865,negated_conjecture,
c2_1(a2002) ).
cnf(u2014,negated_conjecture,
c1_1(a2057) ).
cnf(u2280,negated_conjecture,
c2_1(a2007) ).
cnf(u1891,negated_conjecture,
~ c1_1(a2037) ).
cnf(u1960,negated_conjecture,
c2_1(a2015) ).
cnf(u2023,negated_conjecture,
~ c1_1(a2031) ).
cnf(u2504,negated_conjecture,
c2_1(a2009) ).
cnf(u2510,negated_conjecture,
c2_1(a2044) ).
cnf(u2519,negated_conjecture,
c2_1(a2070) ).
cnf(u2084,negated_conjecture,
~ c0_1(a2079) ).
cnf(u2125,negated_conjecture,
~ c1_1(a2011) ).
cnf(u2138,negated_conjecture,
~ c1_1(a2023) ).
cnf(u2152,negated_conjecture,
~ c1_1(a2067) ).
cnf(u2367,negated_conjecture,
c0_1(a1999) ).
cnf(u2508,negated_conjecture,
c2_1(a2041) ).
cnf(u2200,negated_conjecture,
~ c1_1(a1996) ).
cnf(u2228,negated_conjecture,
~ c1_1(a2026) ).
cnf(u2298,negated_conjecture,
~ c1_1(a2047) ).
cnf(u2309,negated_conjecture,
~ c1_1(a2022) ).
cnf(u2912,negated_conjecture,
c0_1(a2051) ).
cnf(u2362,negated_conjecture,
~ c1_1(a2014) ).
cnf(u2394,negated_conjecture,
c2_1(a2005) ).
cnf(u2400,negated_conjecture,
c2_1(a2048) ).
cnf(u2429,negated_conjecture,
c0_1(a2054) ).
cnf(u2589,negated_conjecture,
c0_1(a2029) ).
cnf(u2626,negated_conjecture,
~ c1_1(a2025) ).
cnf(u2792,negated_conjecture,
c2_1(a1995) ).
cnf(u2952,negated_conjecture,
c2_1(a1994) ).
cnf(u2920,negated_conjecture,
c0_1(a2062) ).
cnf(u3022,negated_conjecture,
c0_1(a2001) ).
cnf(u3066,negated_conjecture,
c0_1(a2081) ).
cnf(u3236,negated_conjecture,
c1_1(a2078) ).
cnf(u3265,negated_conjecture,
c2_1(a2063) ).
cnf(u3360,negated_conjecture,
~ c1_1(a2045) ).
cnf(u3368,negated_conjecture,
~ c1_1(a2074) ).
cnf(u3551,negated_conjecture,
c2_1(a1998) ).
cnf(u3565,negated_conjecture,
c0_1(a1997) ).
cnf(u3635,negated_conjecture,
c0_1(a2083) ).
cnf(u4108,negated_conjecture,
c0_1(a2058) ).
cnf(u4119,negated_conjecture,
c0_1(a2059) ).
cnf(u4169,negated_conjecture,
c0_1(a2033) ).
cnf(u2786,negated_conjecture,
( c2_1(X0)
| ~ c1_1(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN453-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n003.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:06:57 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running first-order theorem proving
% 0.08/0.24 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
% 3.01/1.13 % (1723775)Input is clausal, will run a generic CNF schedule.
% 3.01/1.13 % (1723904)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=3778111619:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.01/1.13 % (1723909)lrs+10_1_sil=8000:sp=occurrence:random_seed=1728756649:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.01/1.13 % (1723906)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1040929804:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.01/1.13 % (1723910)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2119090914:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.01/1.13 % (1723911)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1800389119:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.01/1.13 % (1723907)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=926646599:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.01/1.13 % (1723912)dis-21_1_sil=8000:lcm=predicate:random_seed=2048855664: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.01/1.13 % (1723910)Refutation not found, incomplete strategy
% 3.01/1.13 % (1723910)------------------------------
% 3.01/1.13 % (1723910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.01/1.13 % (1723910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.01/1.13 % (1723910)CaDiCaL version: 2.1.3
% 3.01/1.13 % (1723910)Termination reason: Refutation not found, incomplete strategy
% 3.01/1.13 % (1723910)Time elapsed: 0.043 s
% 3.01/1.13 % (1723910)Peak memory usage: 89 MB
% 3.01/1.13 % (1723910)Instructions burned: 67 (million)
% 3.01/1.13 % (1723912)First to succeed.
% 3.01/1.13 % (1723912)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1723775"
% 3.01/1.13 % (1723909)Instruction limit reached!
% 3.01/1.13 % (1723909)------------------------------
% 3.01/1.13 % (1723909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.01/1.13 % (1723909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.01/1.13 % (1723909)CaDiCaL version: 2.1.3
% 3.01/1.13 % (1723909)Termination reason: Instruction limit
% 3.01/1.13 % (1723909)Termination phase: Saturation
% 3.01/1.13 % (1723909)Time elapsed: 0.068 s
% 3.01/1.13 % (1723909)Peak memory usage: 90 MB
% 3.01/1.13 % (1723909)Instructions burned: 107 (million)
% 3.01/1.13 % (1723911)Refutation not found, incomplete strategy
% 3.01/1.13 % (1723911)------------------------------
% 3.01/1.13 % (1723911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.01/1.13 % (1723911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.01/1.13 % (1723911)CaDiCaL version: 2.1.3
% 3.01/1.13 % (1723911)Termination reason: Refutation not found, incomplete strategy
% 3.01/1.13 % (1723911)Time elapsed: 0.091 s
% 3.01/1.13 % (1723911)Peak memory usage: 91 MB
% 3.01/1.13 % (1723911)Instructions burned: 142 (million)
% 3.01/1.13 % (1723924)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=1449937306:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 3.01/1.13 % (1723924)Refutation not found, incomplete strategy
% 3.01/1.13 % (1723924)------------------------------
% 3.01/1.13 % (1723924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.01/1.13 % (1723924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.01/1.13 % (1723924)CaDiCaL version: 2.1.3
% 3.01/1.13 % (1723924)Termination reason: Refutation not found, incomplete strategy
% 3.01/1.13 % (1723924)Time elapsed: 0.032 s
% 3.01/1.13 % (1723924)Peak memory usage: 89 MB
% 3.01/1.13 % (1723924)Instructions burned: 50 (million)
% 3.01/1.13 % (1723910)------------------------------
% 3.01/1.13 % (1723910)------------------------------
% 3.01/1.13 % SZS status Satisfiable for theBenchmark
% 3.01/1.13 % SZS output start Saturation.
% See solution above
% 3.81/1.22 % SZS output start Definitions and Model Updates.
% 3.81/1.22 % SZS output end Definitions and Model Updates.
% 3.81/1.22 % (1723912)------------------------------
% 3.81/1.22 % (1723912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.81/1.22 % (1723912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.81/1.22 % (1723912)CaDiCaL version: 2.1.3
% 3.81/1.22 % (1723912)Termination reason: Satisfiable
% 3.81/1.22 % (1723912)Time elapsed: 0.059 s
% 3.81/1.22 % (1723912)Peak memory usage: 90 MB
% 3.81/1.22 % (1723912)Instructions burned: 92 (million)
% 3.81/1.22 % (1723912)------------------------------
% 3.81/1.22 % (1723912)------------------------------
% 3.81/1.22 % (1723775)Success in time 0.456 s
% 3.81/1.22 % Vampire exiting
%------------------------------------------------------------------------------