%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN464+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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:09:47 PM UTC 2026
% Result : CounterSatisfiable 0.18s 0.29s
% Output : Saturation 0.18s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u384,negated_conjecture,
ndr1_0 ).
cnf(u388,negated_conjecture,
( ~ c0_1(X88)
| c2_1(X88)
| ~ c1_1(X88) ) ).
cnf(u392,negated_conjecture,
~ hskp46 ).
cnf(u396,negated_conjecture,
( ~ c1_1(X86)
| c0_1(X86)
| c3_1(X86) ) ).
cnf(u400,negated_conjecture,
~ hskp35 ).
cnf(u404,negated_conjecture,
( ~ c3_1(X85)
| c0_1(X85)
| ~ c1_1(X85) ) ).
cnf(u407,negated_conjecture,
~ hskp34 ).
cnf(u412,negated_conjecture,
~ hskp33 ).
cnf(u417,negated_conjecture,
hskp59 ).
cnf(u424,negated_conjecture,
~ hskp32 ).
cnf(u428,negated_conjecture,
~ hskp31 ).
cnf(u432,negated_conjecture,
( ~ c1_1(X83)
| ~ c0_1(X83)
| ~ c2_1(X83) ) ).
cnf(u436,negated_conjecture,
( ~ c1_1(X82)
| c0_1(X82)
| c2_1(X82) ) ).
cnf(u439,negated_conjecture,
~ hskp69 ).
cnf(u444,negated_conjecture,
hskp27 ).
cnf(u449,negated_conjecture,
hskp52 ).
cnf(u459,negated_conjecture,
( ~ c2_1(X79)
| c0_1(X79)
| c3_1(X79) ) ).
cnf(u462,negated_conjecture,
~ hskp30 ).
cnf(u466,negated_conjecture,
~ hskp68 ).
cnf(u471,negated_conjecture,
~ hskp21 ).
cnf(u475,negated_conjecture,
( ~ c0_1(X78)
| c1_1(X78)
| ~ c3_1(X78) ) ).
cnf(u479,negated_conjecture,
~ hskp67 ).
cnf(u483,negated_conjecture,
( ~ c1_1(X76)
| c2_1(X76)
| c3_1(X76) ) ).
cnf(u486,negated_conjecture,
( ~ c3_1(X75)
| c2_1(X75)
| c1_1(X75) ) ).
cnf(u490,negated_conjecture,
( ~ c2_1(X74)
| c3_1(X74)
| ~ c1_1(X74) ) ).
cnf(u493,negated_conjecture,
~ hskp66 ).
cnf(u498,negated_conjecture,
~ hskp29 ).
cnf(u502,negated_conjecture,
~ hskp65 ).
cnf(u507,negated_conjecture,
~ hskp64 ).
cnf(u511,negated_conjecture,
~ hskp28 ).
cnf(u516,negated_conjecture,
hskp39 ).
cnf(u520,negated_conjecture,
~ hskp63 ).
cnf(u525,negated_conjecture,
~ hskp62 ).
cnf(u529,negated_conjecture,
~ hskp26 ).
cnf(u534,negated_conjecture,
~ hskp61 ).
cnf(u541,negated_conjecture,
( ~ c0_1(X69)
| ~ c1_1(X69)
| c3_1(X69) ) ).
cnf(u545,negated_conjecture,
~ hskp54 ).
cnf(u553,negated_conjecture,
( ~ c3_1(X66)
| ~ c2_1(X66)
| ~ c0_1(X66) ) ).
cnf(u556,negated_conjecture,
~ hskp25 ).
cnf(u561,negated_conjecture,
~ hskp60 ).
cnf(u565,negated_conjecture,
( ~ c0_1(X65)
| c3_1(X65)
| c2_1(X65) ) ).
cnf(u568,negated_conjecture,
~ hskp24 ).
cnf(u574,negated_conjecture,
hskp23 ).
cnf(u577,negated_conjecture,
~ hskp57 ).
cnf(u585,negated_conjecture,
~ hskp22 ).
cnf(u593,negated_conjecture,
( ~ c1_1(X59)
| ~ c3_1(X59)
| ~ c0_1(X59) ) ).
cnf(u597,negated_conjecture,
( c2_1(X58)
| ~ c0_1(X58)
| c1_1(X58) ) ).
cnf(u604,negated_conjecture,
~ hskp13 ).
cnf(u610,negated_conjecture,
hskp38 ).
cnf(u614,negated_conjecture,
~ hskp20 ).
cnf(u620,negated_conjecture,
~ hskp7 ).
cnf(u624,negated_conjecture,
( ~ c1_1(X48)
| ~ c3_1(X48)
| c2_1(X48) ) ).
cnf(u627,negated_conjecture,
~ hskp58 ).
cnf(u635,negated_conjecture,
hskp12 ).
cnf(u639,negated_conjecture,
~ hskp19 ).
cnf(u644,negated_conjecture,
hskp18 ).
cnf(u648,negated_conjecture,
~ hskp56 ).
cnf(u652,negated_conjecture,
~ hskp17 ).
cnf(u657,negated_conjecture,
~ hskp55 ).
cnf(u662,negated_conjecture,
hskp8 ).
cnf(u669,negated_conjecture,
~ hskp16 ).
cnf(u674,negated_conjecture,
~ hskp36 ).
cnf(u679,negated_conjecture,
~ hskp15 ).
cnf(u692,negated_conjecture,
hskp14 ).
cnf(u695,negated_conjecture,
~ hskp53 ).
cnf(u700,negated_conjecture,
~ hskp51 ).
cnf(u708,negated_conjecture,
hskp50 ).
cnf(u711,negated_conjecture,
~ hskp49 ).
cnf(u715,negated_conjecture,
~ hskp48 ).
cnf(u720,negated_conjecture,
( ~ c3_1(X22)
| c2_1(X22)
| ~ c0_1(X22) ) ).
cnf(u727,negated_conjecture,
~ hskp11 ).
cnf(u732,negated_conjecture,
~ hskp47 ).
cnf(u738,negated_conjecture,
~ hskp41 ).
cnf(u743,negated_conjecture,
hskp0 ).
cnf(u746,negated_conjecture,
~ hskp10 ).
cnf(u751,negated_conjecture,
~ hskp45 ).
cnf(u756,negated_conjecture,
hskp9 ).
cnf(u760,negated_conjecture,
~ hskp44 ).
cnf(u765,negated_conjecture,
~ hskp6 ).
cnf(u770,negated_conjecture,
~ hskp5 ).
cnf(u775,negated_conjecture,
~ hskp4 ).
cnf(u779,negated_conjecture,
~ hskp43 ).
cnf(u784,negated_conjecture,
~ hskp3 ).
cnf(u788,negated_conjecture,
~ hskp42 ).
cnf(u794,negated_conjecture,
~ hskp2 ).
cnf(u798,negated_conjecture,
~ hskp40 ).
cnf(u805,negated_conjecture,
hskp37 ).
cnf(u810,negated_conjecture,
hskp1 ).
cnf(u831,negated_conjecture,
~ c1_1(a2505) ).
cnf(u841,negated_conjecture,
~ c0_1(a2505) ).
cnf(u880,negated_conjecture,
c0_1(a2499) ).
cnf(u884,negated_conjecture,
c2_1(a2499) ).
cnf(u890,negated_conjecture,
~ c1_1(a2499) ).
cnf(u896,negated_conjecture,
c2_1(a2498) ).
cnf(u901,negated_conjecture,
~ c3_1(a2498) ).
cnf(u905,negated_conjecture,
~ c1_1(a2498) ).
cnf(u911,negated_conjecture,
~ c1_1(a2494) ).
cnf(u917,negated_conjecture,
c2_1(a2494) ).
cnf(u922,negated_conjecture,
~ c0_1(a2494) ).
cnf(u928,negated_conjecture,
c2_1(a2493) ).
cnf(u933,negated_conjecture,
c0_1(a2493) ).
cnf(u937,negated_conjecture,
~ c3_1(a2493) ).
cnf(u943,negated_conjecture,
~ c1_1(a2491) ).
cnf(u949,negated_conjecture,
~ c3_1(a2491) ).
cnf(u953,negated_conjecture,
c2_1(a2491) ).
cnf(u959,negated_conjecture,
~ c0_1(a2487) ).
cnf(u965,negated_conjecture,
~ c3_1(a2487) ).
cnf(u970,negated_conjecture,
~ c1_1(a2487) ).
cnf(u976,negated_conjecture,
c2_1(a2479) ).
cnf(u981,negated_conjecture,
~ c1_1(a2479) ).
cnf(u986,negated_conjecture,
c0_1(a2479) ).
cnf(u1007,negated_conjecture,
~ c1_1(a2475) ).
cnf(u1012,negated_conjecture,
~ c2_1(a2475) ).
cnf(u1024,negated_conjecture,
c2_1(a2471) ).
cnf(u1028,negated_conjecture,
~ c0_1(a2471) ).
cnf(u1033,negated_conjecture,
c3_1(a2471) ).
cnf(u1040,negated_conjecture,
c3_1(a2468) ).
cnf(u1044,negated_conjecture,
~ c0_1(a2468) ).
cnf(u1050,negated_conjecture,
~ c1_1(a2468) ).
cnf(u1055,negated_conjecture,
~ c1_1(a2463) ).
cnf(u1060,negated_conjecture,
c2_1(a2463) ).
cnf(u1066,negated_conjecture,
~ c3_1(a2463) ).
cnf(u1072,negated_conjecture,
c3_1(a2461) ).
cnf(u1077,negated_conjecture,
~ c0_1(a2461) ).
cnf(u1081,negated_conjecture,
~ c1_1(a2461) ).
cnf(u1088,negated_conjecture,
c2_1(a2460) ).
cnf(u1093,negated_conjecture,
~ c3_1(a2460) ).
cnf(u1098,negated_conjecture,
c0_1(a2460) ).
cnf(u1103,negated_conjecture,
~ c1_1(a2459) ).
cnf(u1114,negated_conjecture,
~ c0_1(a2459) ).
cnf(u1120,negated_conjecture,
c2_1(a2457) ).
cnf(u1125,negated_conjecture,
c3_1(a2457) ).
cnf(u1130,negated_conjecture,
~ c1_1(a2457) ).
cnf(u1140,negated_conjecture,
c2_1(a2456) ).
cnf(u1146,negated_conjecture,
~ c1_1(a2456) ).
cnf(u1151,negated_conjecture,
~ c0_1(a2455) ).
cnf(u1157,negated_conjecture,
c2_1(a2455) ).
cnf(u1162,negated_conjecture,
c3_1(a2455) ).
cnf(u1167,negated_conjecture,
~ c0_1(a2452) ).
cnf(u1173,negated_conjecture,
~ c1_1(a2452) ).
cnf(u1177,negated_conjecture,
c2_1(a2452) ).
cnf(u1183,negated_conjecture,
~ c1_1(a2451) ).
cnf(u1189,negated_conjecture,
c0_1(a2451) ).
cnf(u1193,negated_conjecture,
~ c3_1(a2451) ).
cnf(u1199,negated_conjecture,
~ c1_1(a2447) ).
cnf(u1204,negated_conjecture,
c2_1(a2447) ).
cnf(u1210,negated_conjecture,
~ c0_1(a2447) ).
cnf(u1216,negated_conjecture,
c0_1(a2444) ).
cnf(u1220,negated_conjecture,
~ c1_1(a2444) ).
cnf(u1225,negated_conjecture,
c2_1(a2444) ).
cnf(u1231,negated_conjecture,
~ c1_1(a2439) ).
cnf(u1241,negated_conjecture,
~ c2_1(a2439) ).
cnf(u1247,negated_conjecture,
~ c1_1(a2437) ).
cnf(u1252,negated_conjecture,
~ c0_1(a2437) ).
cnf(u1257,negated_conjecture,
c2_1(a2437) ).
cnf(u1263,negated_conjecture,
~ c1_1(a2436) ).
cnf(u1269,negated_conjecture,
c0_1(a2436) ).
cnf(u1274,negated_conjecture,
c2_1(a2436) ).
cnf(u1279,negated_conjecture,
~ c1_1(a2434) ).
cnf(u1285,negated_conjecture,
c2_1(a2434) ).
cnf(u1290,negated_conjecture,
c0_1(a2434) ).
cnf(u1296,negated_conjecture,
c0_1(a2433) ).
cnf(u1301,negated_conjecture,
~ c1_1(a2433) ).
cnf(u1306,negated_conjecture,
c2_1(a2433) ).
cnf(u1312,negated_conjecture,
c2_1(a2432) ).
cnf(u1317,negated_conjecture,
~ c1_1(a2432) ).
cnf(u1322,negated_conjecture,
c3_1(a2432) ).
cnf(u1328,negated_conjecture,
c2_1(a2431) ).
cnf(u1333,negated_conjecture,
~ c1_1(a2431) ).
cnf(u1338,negated_conjecture,
~ c0_1(a2431) ).
cnf(u1343,negated_conjecture,
~ c1_1(a2429) ).
cnf(u1349,negated_conjecture,
~ c0_1(a2429) ).
cnf(u1354,negated_conjecture,
~ c3_1(a2429) ).
cnf(u1360,negated_conjecture,
~ c1_1(a2515) ).
cnf(u1365,negated_conjecture,
~ c2_1(a2515) ).
cnf(u1369,negated_conjecture,
~ c0_1(a2515) ).
cnf(u1375,negated_conjecture,
c2_1(a2514) ).
cnf(u1381,negated_conjecture,
~ c3_1(a2514) ).
cnf(u1386,negated_conjecture,
~ c1_1(a2514) ).
cnf(u1391,negated_conjecture,
c2_1(a2513) ).
cnf(u1397,negated_conjecture,
c0_1(a2513) ).
cnf(u1401,negated_conjecture,
~ c3_1(a2513) ).
cnf(u1408,negated_conjecture,
~ c0_1(a2511) ).
cnf(u1412,negated_conjecture,
~ c1_1(a2511) ).
cnf(u1418,negated_conjecture,
~ c3_1(a2511) ).
cnf(u1423,negated_conjecture,
c2_1(a2510) ).
cnf(u1429,negated_conjecture,
~ c3_1(a2510) ).
cnf(u1433,negated_conjecture,
~ c1_1(a2510) ).
cnf(u1439,negated_conjecture,
c2_1(a2506) ).
cnf(u1444,negated_conjecture,
c3_1(a2506) ).
cnf(u1450,negated_conjecture,
~ c0_1(a2506) ).
cnf(u1456,negated_conjecture,
~ c1_1(a2501) ).
cnf(u1461,negated_conjecture,
c2_1(a2501) ).
cnf(u1466,negated_conjecture,
c0_1(a2501) ).
cnf(u1471,negated_conjecture,
c2_1(a2497) ).
cnf(u1477,negated_conjecture,
c3_1(a2497) ).
cnf(u1482,negated_conjecture,
~ c1_1(a2497) ).
cnf(u1488,negated_conjecture,
~ c0_1(a2495) ).
cnf(u1493,negated_conjecture,
~ c2_1(a2495) ).
cnf(u1498,negated_conjecture,
~ c3_1(a2495) ).
cnf(u1504,negated_conjecture,
~ c3_1(a2492) ).
cnf(u1509,negated_conjecture,
c2_1(a2492) ).
cnf(u1513,negated_conjecture,
c0_1(a2492) ).
cnf(u1519,negated_conjecture,
c2_1(a2489) ).
cnf(u1525,negated_conjecture,
c0_1(a2489) ).
cnf(u1530,negated_conjecture,
~ c3_1(a2489) ).
cnf(u1536,negated_conjecture,
~ c1_1(a2486) ).
cnf(u1540,negated_conjecture,
c0_1(a2486) ).
cnf(u1546,negated_conjecture,
c2_1(a2486) ).
cnf(u1552,negated_conjecture,
~ c1_1(a2485) ).
cnf(u1557,negated_conjecture,
c2_1(a2485) ).
cnf(u1562,negated_conjecture,
~ c0_1(a2485) ).
cnf(u1568,negated_conjecture,
~ c1_1(a2483) ).
cnf(u1573,negated_conjecture,
c3_1(a2483) ).
cnf(u1577,negated_conjecture,
c2_1(a2483) ).
cnf(u1584,negated_conjecture,
~ c1_1(a2482) ).
cnf(u1588,negated_conjecture,
c2_1(a2482) ).
cnf(u1594,negated_conjecture,
~ c0_1(a2482) ).
cnf(u1599,negated_conjecture,
c2_1(a2478) ).
cnf(u1605,negated_conjecture,
~ c0_1(a2478) ).
cnf(u1609,negated_conjecture,
c3_1(a2478) ).
cnf(u1632,negated_conjecture,
~ c0_1(a2472) ).
cnf(u1637,negated_conjecture,
c2_1(a2472) ).
cnf(u1642,negated_conjecture,
c3_1(a2472) ).
cnf(u1647,negated_conjecture,
c2_1(a2469) ).
cnf(u1653,negated_conjecture,
~ c0_1(a2469) ).
cnf(u1658,negated_conjecture,
~ c1_1(a2469) ).
cnf(u1668,negated_conjecture,
c2_1(a2466) ).
cnf(u1673,negated_conjecture,
c0_1(a2466) ).
cnf(u1679,negated_conjecture,
c2_1(a2464) ).
cnf(u1685,negated_conjecture,
~ c0_1(a2464) ).
cnf(u1689,negated_conjecture,
~ c1_1(a2464) ).
cnf(u1696,negated_conjecture,
~ c0_1(a2462) ).
cnf(u1701,negated_conjecture,
c3_1(a2462) ).
cnf(u1706,negated_conjecture,
c2_1(a2462) ).
cnf(u1712,negated_conjecture,
~ c0_1(a2458) ).
cnf(u1716,negated_conjecture,
~ c1_1(a2458) ).
cnf(u1728,negated_conjecture,
~ c3_1(a2454) ).
cnf(u1733,negated_conjecture,
~ c1_1(a2454) ).
cnf(u1738,negated_conjecture,
~ c0_1(a2454) ).
cnf(u1744,negated_conjecture,
~ c0_1(a2453) ).
cnf(u1749,negated_conjecture,
~ c1_1(a2453) ).
cnf(u1753,negated_conjecture,
c2_1(a2453) ).
cnf(u1759,negated_conjecture,
c2_1(a2448) ).
cnf(u1764,negated_conjecture,
~ c1_1(a2448) ).
cnf(u1769,negated_conjecture,
~ c3_1(a2448) ).
cnf(u1776,negated_conjecture,
~ c1_1(a2446) ).
cnf(u1781,negated_conjecture,
~ c3_1(a2446) ).
cnf(u1786,negated_conjecture,
~ c0_1(a2446) ).
cnf(u1792,negated_conjecture,
~ c1_1(a2445) ).
cnf(u1797,negated_conjecture,
~ c0_1(a2445) ).
cnf(u1802,negated_conjecture,
c3_1(a2445) ).
cnf(u1808,negated_conjecture,
~ c3_1(a2443) ).
cnf(u1812,negated_conjecture,
c0_1(a2443) ).
cnf(u1817,negated_conjecture,
c2_1(a2443) ).
cnf(u1823,negated_conjecture,
c2_1(a2442) ).
cnf(u1829,negated_conjecture,
~ c1_1(a2442) ).
cnf(u1834,negated_conjecture,
c0_1(a2442) ).
cnf(u1839,negated_conjecture,
c3_1(a2441) ).
cnf(u1844,negated_conjecture,
~ c0_1(a2441) ).
cnf(u1849,negated_conjecture,
c2_1(a2441) ).
cnf(u1855,negated_conjecture,
c2_1(a2440) ).
cnf(u1860,negated_conjecture,
c3_1(a2440) ).
cnf(u1865,negated_conjecture,
~ c0_1(a2440) ).
cnf(u1871,negated_conjecture,
c0_1(a2438) ).
cnf(u1877,negated_conjecture,
~ c3_1(a2438) ).
cnf(u1881,negated_conjecture,
~ c1_1(a2438) ).
cnf(u1888,negated_conjecture,
~ c1_1(a2435) ).
cnf(u1897,negated_conjecture,
~ c2_1(a2435) ).
cnf(u1904,negated_conjecture,
~ c3_1(a2430) ).
cnf(u1909,negated_conjecture,
c2_1(a2430) ).
cnf(u1914,negated_conjecture,
~ c1_1(a2430) ).
cnf(u1920,negated_conjecture,
~ c0_1(a2428) ).
cnf(u1925,negated_conjecture,
~ c1_1(a2428) ).
cnf(u1930,negated_conjecture,
c2_1(a2428) ).
cnf(u3617,negated_conjecture,
~ c3_1(a2501) ).
cnf(u3622,negated_conjecture,
~ c3_1(a2433) ).
cnf(u4121,negated_conjecture,
~ c1_1(a2460) ).
cnf(u4131,negated_conjecture,
~ c1_1(a2443) ).
cnf(u4136,negated_conjecture,
~ c1_1(a2462) ).
cnf(u4141,negated_conjecture,
~ c1_1(a2466) ).
cnf(u4478,negated_conjecture,
c0_1(a2456) ).
cnf(u4489,negated_conjecture,
~ c0_1(a2497) ).
cnf(u4485,negated_conjecture,
c0_1(a2510) ).
cnf(u1941,negated_conjecture,
~ c1_1(X83) ).
cnf(u1935,negated_conjecture,
( ~ c1_1(X82)
| c2_1(X82) ) ).
cnf(u4314,negated_conjecture,
( ~ c1_1(X74)
| c3_1(X74) ) ).
cnf(u4504,negated_conjecture,
c3_1(a2428) ).
cnf(u4494,negated_conjecture,
c3_1(a2482) ).
cnf(u4174,negated_conjecture,
c2_1(a2451) ).
cnf(u4500,negated_conjecture,
c0_1(a2448) ).
cnf(u2373,negated_conjecture,
c2_1(a2461) ).
cnf(u3408,negated_conjecture,
( ~ c3_1(X22)
| ~ c0_1(X22) ) ).
cnf(u4471,negated_conjecture,
c3_1(a2494) ).
cnf(u4484,negated_conjecture,
c0_1(a2514) ).
cnf(u2432,negated_conjecture,
~ c0_1(a2457) ).
cnf(u4474,negated_conjecture,
c0_1(a2463) ).
cnf(u4379,negated_conjecture,
~ c0_1(a2483) ).
cnf(u4483,negated_conjecture,
c3_1(a2431) ).
cnf(u4482,negated_conjecture,
c3_1(a2437) ).
cnf(u4493,negated_conjecture,
c3_1(a2485) ).
cnf(u4496,negated_conjecture,
c3_1(a2469) ).
cnf(u4503,negated_conjecture,
c0_1(a2430) ).
cnf(u2404,negated_conjecture,
( ~ c0_1(X58)
| c2_1(X58) ) ).
cnf(u4499,negated_conjecture,
c3_1(a2453) ).
cnf(u2366,negated_conjecture,
c2_1(a2445) ).
cnf(u4472,negated_conjecture,
c0_1(a2491) ).
cnf(u4498,negated_conjecture,
c3_1(a2464) ).
cnf(u4481,negated_conjecture,
c3_1(a2447) ).
cnf(u2364,negated_conjecture,
( ~ c3_1(X75)
| c2_1(X75) ) ).
cnf(u4470,negated_conjecture,
c0_1(a2498) ).
cnf(u1933,negated_conjecture,
( ~ c1_1(X85)
| c0_1(X85) ) ).
cnf(u4330,negated_conjecture,
c2_1(a2438) ).
cnf(u4480,negated_conjecture,
c3_1(a2452) ).
cnf(u3081,negated_conjecture,
~ c0_1(a2432) ).
cnf(u2147,negated_conjecture,
c2_1(a2468) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN464+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.19 % Computer : n007.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 16:06:25 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.22 Running first-order model finding
% 0.07/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.29 % (2526853)Will run a generic schedule for satisfiability detection.
% 0.18/0.29 % (2526863)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4230736605:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.29 % (2526859)% WARNING: option uhcvi not known.
% 0.18/0.29 % (2526858)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=233535520_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.29 % (2526860)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1625004315:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.29 % (2526859)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2942282368:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.29 % (2526861)dis+10_1_sil=32000:sp=arity:random_seed=2979016797:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.29 % (2526862)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=371913544:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.29 % (2526864)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3047842541:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.29 % Detected minimum model sizes of [1]
% 0.18/0.29 % Detected maximum model sizes of [70]
% 0.18/0.29 % TRYING [1]
% 0.18/0.29 % TRYING [2]
% 0.18/0.29 % TRYING [3]
% 0.18/0.29 % Finite Model Found!
% 0.18/0.29 % SZS status CounterSatisfiable for theBenchmark
% 0.18/0.29 % (2526863) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2526853-2526863"...
% 0.18/0.29 % (2526858) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2526853-2526858"...
% 0.18/0.29 % (2526858)...printing done.
% 0.18/0.29 % (2526863)...printing done.
% 0.18/0.29 % SZS status CounterSatisfiable for theBenchmark
% 0.18/0.29 % SZS output start Saturation.
% See solution above
% 0.18/0.30 % SZS output start Definitions and Model Updates.
% 0.18/0.30 % SZS output end Definitions and Model Updates.
% 0.18/0.30 % (2526863)------------------------------
% 0.18/0.30 % (2526863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.30 % (2526863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.30 % (2526863)CaDiCaL version: 2.1.3
% 0.18/0.30 % (2526863)Termination reason: Satisfiable
% 0.18/0.30 % (2526863)Time elapsed: 0.028 s
% 0.18/0.30 % (2526863)Peak memory usage: 13 MB
% 0.18/0.30 % (2526863)Instructions burned: 80 (million)
% 0.18/0.30 % (2526853)Success in time 0.062 s
% 0.18/0.30 % Vampire exiting
%------------------------------------------------------------------------------