%------------------------------------------------------------------------------
% 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 : n020.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 : CounterSatisfiable 3.08s 1.12s
% Output : Saturation 3.88s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u382,negated_conjecture,
hskp20 ).
cnf(u765,negated_conjecture,
ndr1_0 ).
cnf(u395,negated_conjecture,
hskp10 ).
cnf(u1288,negated_conjecture,
~ hskp32 ).
cnf(u405,negated_conjecture,
hskp47 ).
cnf(u1302,negated_conjecture,
~ hskp31 ).
cnf(u1316,negated_conjecture,
~ hskp30 ).
cnf(u421,negated_conjecture,
( ~ c3_1(X81)
| ~ c1_1(X81)
| ~ c0_1(X81) ) ).
cnf(u425,negated_conjecture,
( c3_1(X80)
| c2_1(X80)
| c1_1(X80) ) ).
cnf(u435,negated_conjecture,
hskp29 ).
cnf(u755,negated_conjecture,
~ hskp70 ).
cnf(u445,negated_conjecture,
( ~ c3_1(X76)
| ~ c0_1(X76)
| c2_1(X76) ) ).
cnf(u448,negated_conjecture,
hskp54 ).
cnf(u1064,negated_conjecture,
~ hskp48 ).
cnf(u770,negated_conjecture,
~ hskp69 ).
cnf(u465,negated_conjecture,
hskp68 ).
cnf(u1442,negated_conjecture,
~ hskp21 ).
cnf(u798,negated_conjecture,
~ hskp67 ).
cnf(u479,negated_conjecture,
hskp28 ).
cnf(u489,negated_conjecture,
hskp27 ).
cnf(u500,negated_conjecture,
( ~ c3_1(X63)
| c1_1(X63)
| ~ c0_1(X63) ) ).
cnf(u812,negated_conjecture,
~ hskp66 ).
cnf(u507,negated_conjecture,
( c2_1(X61)
| c1_1(X61)
| c0_1(X61) ) ).
cnf(u1652,negated_conjecture,
~ hskp6 ).
cnf(u514,negated_conjecture,
hskp26 ).
cnf(u1050,negated_conjecture,
~ hskp49 ).
cnf(u521,negated_conjecture,
( ~ c3_1(X60)
| c2_1(X60)
| ~ c1_1(X60) ) ).
cnf(u525,negated_conjecture,
( ~ c3_1(X57)
| c0_1(X57)
| c2_1(X57) ) ).
cnf(u1386,negated_conjecture,
~ hskp25 ).
cnf(u840,negated_conjecture,
~ hskp64 ).
cnf(u538,negated_conjecture,
hskp2 ).
cnf(u545,negated_conjecture,
hskp63 ).
cnf(u868,negated_conjecture,
~ hskp62 ).
cnf(u555,negated_conjecture,
hskp24 ).
cnf(u559,negated_conjecture,
hskp59 ).
cnf(u562,negated_conjecture,
hskp33 ).
cnf(u569,negated_conjecture,
hskp61 ).
cnf(u896,negated_conjecture,
~ hskp60 ).
cnf(u924,negated_conjecture,
~ hskp58 ).
cnf(u1414,negated_conjecture,
~ hskp23 ).
cnf(u583,negated_conjecture,
( ~ c3_1(X50)
| ~ c2_1(X50)
| ~ c0_1(X50) ) ).
cnf(u952,negated_conjecture,
~ hskp56 ).
cnf(u593,negated_conjecture,
hskp57 ).
cnf(u966,negated_conjecture,
~ hskp55 ).
cnf(u600,negated_conjecture,
hskp22 ).
cnf(u604,negated_conjecture,
hskp43 ).
cnf(u1162,negated_conjecture,
~ hskp41 ).
cnf(u1470,negated_conjecture,
~ hskp19 ).
cnf(u1484,negated_conjecture,
~ hskp18 ).
cnf(u623,negated_conjecture,
hskp53 ).
cnf(u1498,negated_conjecture,
~ hskp17 ).
cnf(u1008,negated_conjecture,
~ hskp52 ).
cnf(u633,negated_conjecture,
( c2_1(X42)
| c1_1(X42)
| ~ c0_1(X42) ) ).
cnf(u1512,negated_conjecture,
~ hskp16 ).
cnf(u1526,negated_conjecture,
~ hskp15 ).
cnf(u643,negated_conjecture,
hskp51 ).
cnf(u647,negated_conjecture,
hskp50 ).
cnf(u1092,negated_conjecture,
~ hskp46 ).
cnf(u1666,negated_conjecture,
~ hskp5 ).
cnf(u1540,negated_conjecture,
~ hskp14 ).
cnf(u666,negated_conjecture,
hskp45 ).
cnf(u1204,negated_conjecture,
~ hskp38 ).
cnf(u1554,negated_conjecture,
~ hskp13 ).
cnf(u1568,negated_conjecture,
~ hskp12 ).
cnf(u679,negated_conjecture,
hskp44 ).
cnf(u693,negated_conjecture,
hskp9 ).
cnf(u1638,negated_conjecture,
~ hskp7 ).
cnf(u707,negated_conjecture,
hskp37 ).
cnf(u711,negated_conjecture,
hskp40 ).
cnf(u715,negated_conjecture,
hskp39 ).
cnf(u1680,negated_conjecture,
~ hskp4 ).
cnf(u724,negated_conjecture,
hskp3 ).
cnf(u1722,negated_conjecture,
~ hskp1 ).
cnf(u735,negated_conjecture,
hskp36 ).
cnf(u1246,negated_conjecture,
~ hskp35 ).
cnf(u742,negated_conjecture,
hskp34 ).
cnf(u746,negated_conjecture,
hskp0 ).
cnf(u2065,negated_conjecture,
~ c0_1(a2078) ).
cnf(u763,negated_conjecture,
c2_1(a2078) ).
cnf(u1751,negated_conjecture,
~ c0_1(a2074) ).
cnf(u1831,negated_conjecture,
c2_1(a2074) ).
cnf(u783,negated_conjecture,
c0_1(a2073) ).
cnf(u788,negated_conjecture,
~ c2_1(a2073) ).
cnf(u792,negated_conjecture,
c1_1(a2073) ).
cnf(u802,negated_conjecture,
~ c0_1(a2070) ).
cnf(u1935,negated_conjecture,
c1_1(a2070) ).
cnf(u811,negated_conjecture,
c2_1(a2067) ).
cnf(u2105,negated_conjecture,
~ c0_1(a2067) ).
cnf(u825,negated_conjecture,
c1_1(a2063) ).
cnf(u830,negated_conjecture,
c0_1(a2063) ).
cnf(u834,negated_conjecture,
~ c3_1(a2063) ).
cnf(u839,negated_conjecture,
c1_1(a2061) ).
cnf(u2218,negated_conjecture,
c2_1(a2061) ).
cnf(u853,negated_conjecture,
c1_1(a2059) ).
cnf(u858,negated_conjecture,
c2_1(a2059) ).
cnf(u862,negated_conjecture,
~ c3_1(a2059) ).
cnf(u867,negated_conjecture,
c3_1(a2058) ).
cnf(u872,negated_conjecture,
c1_1(a2058) ).
cnf(u2295,negated_conjecture,
c2_1(a2058) ).
cnf(u881,negated_conjecture,
c3_1(a2054) ).
cnf(u886,negated_conjecture,
c2_1(a2054) ).
cnf(u890,negated_conjecture,
c1_1(a2054) ).
cnf(u909,negated_conjecture,
c2_1(a2052) ).
cnf(u914,negated_conjecture,
c0_1(a2052) ).
cnf(u918,negated_conjecture,
~ c1_1(a2052) ).
cnf(u2241,negated_conjecture,
c1_1(a2051) ).
cnf(u2236,negated_conjecture,
c2_1(a2051) ).
cnf(u937,negated_conjecture,
c0_1(a2048) ).
cnf(u942,negated_conjecture,
~ c1_1(a2048) ).
cnf(u946,negated_conjecture,
~ c3_1(a2048) ).
cnf(u2430,negated_conjecture,
c2_1(a2047) ).
cnf(u965,negated_conjecture,
c2_1(a2046) ).
cnf(u970,negated_conjecture,
c1_1(a2046) ).
cnf(u1861,negated_conjecture,
~ c0_1(a2046) ).
cnf(u979,negated_conjecture,
c3_1(a2037) ).
cnf(u984,negated_conjecture,
c2_1(a2037) ).
cnf(u988,negated_conjecture,
~ c0_1(a2037) ).
cnf(u993,negated_conjecture,
c1_1(a2035) ).
cnf(u998,negated_conjecture,
~ c0_1(a2035) ).
cnf(u1002,negated_conjecture,
c2_1(a2035) ).
cnf(u1021,negated_conjecture,
c1_1(a2030) ).
cnf(u1026,negated_conjecture,
c2_1(a2030) ).
cnf(u1030,negated_conjecture,
~ c0_1(a2030) ).
cnf(u1035,negated_conjecture,
c2_1(a2029) ).
cnf(u1040,negated_conjecture,
~ c3_1(a2029) ).
cnf(u1044,negated_conjecture,
c1_1(a2029) ).
cnf(u1054,negated_conjecture,
~ c1_1(a2028) ).
cnf(u1058,negated_conjecture,
c0_1(a2028) ).
cnf(u1894,negated_conjecture,
~ c0_1(a2027) ).
cnf(u1072,negated_conjecture,
c1_1(a2027) ).
cnf(u1077,negated_conjecture,
c0_1(a2026) ).
cnf(u1082,negated_conjecture,
~ c3_1(a2026) ).
cnf(u1086,negated_conjecture,
c2_1(a2026) ).
cnf(u3089,negated_conjecture,
c2_1(a2025) ).
cnf(u1105,negated_conjecture,
c3_1(a2022) ).
cnf(u1110,negated_conjecture,
~ c0_1(a2022) ).
cnf(u1114,negated_conjecture,
c2_1(a2022) ).
cnf(u1119,negated_conjecture,
c0_1(a2018) ).
cnf(u1124,negated_conjecture,
~ c1_1(a2018) ).
cnf(u1128,negated_conjecture,
c2_1(a2018) ).
cnf(u1133,negated_conjecture,
c2_1(a2017) ).
cnf(u1138,negated_conjecture,
~ c0_1(a2017) ).
cnf(u1142,negated_conjecture,
~ c1_1(a2017) ).
cnf(u1147,negated_conjecture,
c2_1(a2010) ).
cnf(u1152,negated_conjecture,
~ c0_1(a2010) ).
cnf(u1156,negated_conjecture,
c3_1(a2010) ).
cnf(u1803,negated_conjecture,
~ c0_1(a2007) ).
cnf(u1166,negated_conjecture,
c1_1(a2007) ).
cnf(u1175,negated_conjecture,
c0_1(a2005) ).
cnf(u1180,negated_conjecture,
~ c3_1(a2005) ).
cnf(u1184,negated_conjecture,
~ c1_1(a2005) ).
cnf(u1189,negated_conjecture,
c1_1(a2004) ).
cnf(u1194,negated_conjecture,
c2_1(a2004) ).
cnf(u1198,negated_conjecture,
c0_1(a2004) ).
cnf(u2812,negated_conjecture,
c2_1(a2003) ).
cnf(u1212,negated_conjecture,
~ c1_1(a2003) ).
cnf(u1217,negated_conjecture,
c1_1(a2002) ).
cnf(u1222,negated_conjecture,
~ c0_1(a2002) ).
cnf(u1226,negated_conjecture,
c3_1(a2002) ).
cnf(u1231,negated_conjecture,
c1_1(a1997) ).
cnf(u1236,negated_conjecture,
~ c3_1(a1997) ).
cnf(u1240,negated_conjecture,
~ c2_1(a1997) ).
cnf(u3218,negated_conjecture,
~ c0_1(a1996) ).
cnf(u1250,negated_conjecture,
c3_1(a1996) ).
cnf(u1254,negated_conjecture,
c2_1(a1996) ).
cnf(u1259,negated_conjecture,
c1_1(a1995) ).
cnf(u1264,negated_conjecture,
~ c3_1(a1995) ).
cnf(u1268,negated_conjecture,
c0_1(a1995) ).
cnf(u1273,negated_conjecture,
c0_1(a1993) ).
cnf(u1278,negated_conjecture,
c1_1(a1993) ).
cnf(u1282,negated_conjecture,
c2_1(a1993) ).
cnf(u1287,negated_conjecture,
~ c1_1(a2083) ).
cnf(u3460,negated_conjecture,
c2_1(a2083) ).
cnf(u1837,negated_conjecture,
c2_1(a2081) ).
cnf(u1310,negated_conjecture,
~ c1_1(a2081) ).
cnf(u2096,negated_conjecture,
c0_1(a2080) ).
cnf(u1329,negated_conjecture,
~ c1_1(a2079) ).
cnf(u1334,negated_conjecture,
c2_1(a2079) ).
cnf(u1338,negated_conjecture,
c3_1(a2079) ).
cnf(u1343,negated_conjecture,
~ c0_1(a2069) ).
cnf(u1348,negated_conjecture,
c2_1(a2069) ).
cnf(u1352,negated_conjecture,
c1_1(a2069) ).
cnf(u1357,negated_conjecture,
~ c2_1(a2068) ).
cnf(u1362,negated_conjecture,
c1_1(a2068) ).
cnf(u1366,negated_conjecture,
c0_1(a2068) ).
cnf(u1371,negated_conjecture,
~ c0_1(a2065) ).
cnf(u1376,negated_conjecture,
c2_1(a2065) ).
cnf(u1380,negated_conjecture,
c3_1(a2065) ).
cnf(u3462,negated_conjecture,
c2_1(a2062) ).
cnf(u1390,negated_conjecture,
~ c1_1(a2062) ).
cnf(u1399,negated_conjecture,
~ c0_1(a2057) ).
cnf(u1404,negated_conjecture,
~ c3_1(a2057) ).
cnf(u1408,negated_conjecture,
c2_1(a2057) ).
cnf(u1413,negated_conjecture,
~ c3_1(a2050) ).
cnf(u1787,negated_conjecture,
c0_1(a2050) ).
cnf(u1839,negated_conjecture,
c2_1(a2050) ).
cnf(u1427,negated_conjecture,
~ c3_1(a2045) ).
cnf(u1432,negated_conjecture,
~ c0_1(a2045) ).
cnf(u1436,negated_conjecture,
c2_1(a2045) ).
cnf(u1441,negated_conjecture,
~ c0_1(a2044) ).
cnf(u1911,negated_conjecture,
c1_1(a2044) ).
cnf(u1450,negated_conjecture,
c3_1(a2044) ).
cnf(u1455,negated_conjecture,
~ c0_1(a2041) ).
cnf(u1460,negated_conjecture,
c3_1(a2041) ).
cnf(u1464,negated_conjecture,
c1_1(a2041) ).
cnf(u1474,negated_conjecture,
c0_1(a2038) ).
cnf(u1478,negated_conjecture,
c1_1(a2038) ).
cnf(u1483,negated_conjecture,
~ c1_1(a2036) ).
cnf(u2487,negated_conjecture,
~ c0_1(a2036) ).
cnf(u1497,negated_conjecture,
~ c0_1(a2034) ).
cnf(u1502,negated_conjecture,
~ c1_1(a2034) ).
cnf(u1525,negated_conjecture,
~ c0_1(a2031) ).
cnf(u1841,negated_conjecture,
c2_1(a2031) ).
cnf(u3538,negated_conjecture,
c2_1(a2020) ).
cnf(u1558,negated_conjecture,
~ c3_1(a2020) ).
cnf(u1562,negated_conjecture,
c1_1(a2020) ).
cnf(u3645,negated_conjecture,
c0_1(a2019) ).
cnf(u1581,negated_conjecture,
~ c1_1(a2016) ).
cnf(u1586,negated_conjecture,
c2_1(a2016) ).
cnf(u1590,negated_conjecture,
c0_1(a2016) ).
cnf(u1595,negated_conjecture,
~ c0_1(a2015) ).
cnf(u1600,negated_conjecture,
c1_1(a2015) ).
cnf(u1604,negated_conjecture,
c3_1(a2015) ).
cnf(u1609,negated_conjecture,
~ c0_1(a2014) ).
cnf(u1614,negated_conjecture,
~ c2_1(a2014) ).
cnf(u1618,negated_conjecture,
~ c3_1(a2014) ).
cnf(u1623,negated_conjecture,
~ c1_1(a2013) ).
cnf(u1628,negated_conjecture,
~ c0_1(a2013) ).
cnf(u1632,negated_conjecture,
~ c3_1(a2013) ).
cnf(u2210,negated_conjecture,
c2_1(a2011) ).
cnf(u2116,negated_conjecture,
~ c0_1(a2011) ).
cnf(u1992,negated_conjecture,
c1_1(a2009) ).
cnf(u1656,negated_conjecture,
~ c0_1(a2009) ).
cnf(u1660,negated_conjecture,
c3_1(a2009) ).
cnf(u1665,negated_conjecture,
~ c0_1(a2006) ).
cnf(u1670,negated_conjecture,
c2_1(a2006) ).
cnf(u2351,negated_conjecture,
c1_1(a2006) ).
cnf(u2079,negated_conjecture,
c1_1(a2001) ).
cnf(u1693,negated_conjecture,
~ c0_1(a2000) ).
cnf(u1698,negated_conjecture,
c1_1(a2000) ).
cnf(u1702,negated_conjecture,
~ c3_1(a2000) ).
cnf(u1707,negated_conjecture,
~ c3_1(a1999) ).
cnf(u1712,negated_conjecture,
c1_1(a1999) ).
cnf(u1716,negated_conjecture,
~ c2_1(a1999) ).
cnf(u3585,negated_conjecture,
c1_1(a1998) ).
cnf(u1730,negated_conjecture,
c0_1(a1998) ).
cnf(u1735,negated_conjecture,
~ c3_1(a1994) ).
cnf(u1740,negated_conjecture,
c0_1(a1994) ).
cnf(u1744,negated_conjecture,
~ c1_1(a1994) ).
cnf(u1754,negated_conjecture,
c1_1(a2074) ).
cnf(u1822,negated_conjecture,
~ c1_1(a2026) ).
cnf(u1849,negated_conjecture,
c1_1(a2022) ).
cnf(u1833,negated_conjecture,
c2_1(a2048) ).
cnf(u1948,negated_conjecture,
~ c1_1(a2050) ).
cnf(u1795,negated_conjecture,
c1_1(a2031) ).
cnf(u1845,negated_conjecture,
c2_1(a2013) ).
cnf(u1875,negated_conjecture,
~ c0_1(a2081) ).
cnf(u1888,negated_conjecture,
c2_1(a2028) ).
cnf(u1893,negated_conjecture,
c2_1(a2027) ).
cnf(u1898,negated_conjecture,
c2_1(a2007) ).
cnf(u1914,negated_conjecture,
c2_1(a2044) ).
cnf(u2739,negated_conjecture,
c2_1(a1995) ).
cnf(u1964,negated_conjecture,
c2_1(a2041) ).
cnf(u1995,negated_conjecture,
c2_1(a2009) ).
cnf(u2650,negated_conjecture,
~ c1_1(a2057) ).
cnf(u2746,negated_conjecture,
c2_1(a1994) ).
cnf(u2069,negated_conjecture,
c1_1(a2078) ).
cnf(u2078,negated_conjecture,
~ c0_1(a2001) ).
cnf(u2108,negated_conjecture,
c1_1(a2067) ).
cnf(u2119,negated_conjecture,
c1_1(a2011) ).
cnf(u2125,negated_conjecture,
c1_1(a2010) ).
cnf(u2730,negated_conjecture,
c2_1(a2063) ).
cnf(u2221,negated_conjecture,
~ c0_1(a2061) ).
cnf(u2239,negated_conjecture,
~ c0_1(a2051) ).
cnf(u2248,negated_conjecture,
~ c0_1(a1999) ).
cnf(u2298,negated_conjecture,
~ c0_1(a2058) ).
cnf(u2326,negated_conjecture,
c0_1(a2059) ).
cnf(u2732,negated_conjecture,
c2_1(a2005) ).
cnf(u2347,negated_conjecture,
c1_1(a2014) ).
cnf(u2363,negated_conjecture,
c2_1(a2002) ).
cnf(u2456,negated_conjecture,
c0_1(a2029) ).
cnf(u2464,negated_conjecture,
~ c0_1(a2079) ).
cnf(u2741,negated_conjecture,
c2_1(a2038) ).
cnf(u2486,negated_conjecture,
c2_1(a2036) ).
cnf(u2532,negated_conjecture,
~ c0_1(a2083) ).
cnf(u2542,negated_conjecture,
c2_1(a2015) ).
cnf(u2682,negated_conjecture,
~ c2_1(a1998) ).
cnf(u2798,negated_conjecture,
c0_1(a1997) ).
cnf(u2815,negated_conjecture,
~ c0_1(a2003) ).
cnf(u2982,negated_conjecture,
~ c0_1(a2054) ).
cnf(u2993,negated_conjecture,
c0_1(a2020) ).
cnf(u3060,negated_conjecture,
c1_1(a2025) ).
cnf(u3205,negated_conjecture,
c1_1(a2037) ).
cnf(u3432,negated_conjecture,
~ c1_1(a1996) ).
cnf(u3545,negated_conjecture,
c2_1(a2000) ).
%------------------------------------------------------------------------------
%----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.17 % Computer : n020.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 16:06:19 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 Running first-order theorem proving
% 0.08/0.20 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.08/1.12 % (275939)Detected formulas, will run a generic FOF schedule.
% 3.08/1.12 % (275945)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=1016903150:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.08/1.12 % (275944)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=1481633395:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.08/1.12 % (275947)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1668727306:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.08/1.12 % (275946)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=3707278098:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.08/1.12 % (275949)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1517315122:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.08/1.12 % (275948)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4238870017:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.08/1.12 % (275950)dis-21_1_sil=8000:lcm=predicate:random_seed=620221728: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)
% 3.08/1.12 % (275947)Refutation not found, incomplete strategy
% 3.08/1.12 % (275947)------------------------------
% 3.08/1.12 % (275947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/1.12 % (275947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/1.12 % (275947)CaDiCaL version: 2.1.3
% 3.08/1.12 % (275947)Termination reason: Refutation not found, incomplete strategy
% 3.08/1.12 % (275947)Time elapsed: 0.045 s
% 3.08/1.12 % (275947)Peak memory usage: 90 MB
% 3.08/1.12 % (275947)Instructions burned: 74 (million)
% 3.08/1.12 % (275950)First to succeed.
% 3.08/1.12 % (275950)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-275939"
% 3.08/1.12 % (275948)Instruction limit reached!
% 3.08/1.12 % (275948)------------------------------
% 3.08/1.12 % (275948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/1.12 % (275948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/1.12 % (275948)CaDiCaL version: 2.1.3
% 3.08/1.12 % (275948)Termination reason: Instruction limit
% 3.08/1.12 % (275948)Termination phase: Saturation
% 3.08/1.12 % (275948)Time elapsed: 0.057 s
% 3.08/1.12 % (275948)Peak memory usage: 87 MB
% 3.08/1.12 % (275948)Instructions burned: 119 (million)
% 3.08/1.12 % (275949)Instruction limit reached!
% 3.08/1.12 % (275949)------------------------------
% 3.08/1.12 % (275949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/1.12 % (275949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/1.12 % (275949)CaDiCaL version: 2.1.3
% 3.08/1.12 % (275949)Termination reason: Instruction limit
% 3.08/1.12 % (275949)Termination phase: Saturation
% 3.08/1.12 % (275949)Time elapsed: 0.087 s
% 3.08/1.12 % (275949)Peak memory usage: 90 MB
% 3.08/1.12 % (275949)Instructions burned: 139 (million)
% 3.08/1.12 % (275958)lrs+10_1_sil=8000:sp=occurrence:random_seed=3249567122:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 3.08/1.12 % (275959)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1891338354:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 3.08/1.12 % (275947)------------------------------
% 3.08/1.12 % (275947)------------------------------
% 3.08/1.12 % (275958)Also succeeded, but the first one will report.
% 3.08/1.12 % SZS status CounterSatisfiable for theBenchmark
% 3.08/1.12 % SZS output start Saturation.
% See solution above
% 3.88/1.22 % SZS output start Definitions and Model Updates.
% 3.88/1.22 % SZS output end Definitions and Model Updates.
% 3.88/1.22 % (275950)------------------------------
% 3.88/1.22 % (275950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.88/1.22 % (275950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.88/1.22 % (275950)CaDiCaL version: 2.1.3
% 3.88/1.22 % (275950)Termination reason: Satisfiable
% 3.88/1.22 % (275950)Time elapsed: 0.049 s
% 3.88/1.22 % (275950)Peak memory usage: 90 MB
% 3.88/1.22 % (275950)Instructions burned: 79 (million)
% 3.88/1.22 % (275950)------------------------------
% 3.88/1.22 % (275950)------------------------------
% 3.88/1.22 % (275939)Success in time 0.475 s
% 3.88/1.22 % Vampire exiting
%------------------------------------------------------------------------------