%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN426-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 : n018.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:07:51 PM UTC 2026
% Result : Satisfiable 0.18s 0.28s
% Output : Saturation 0.18s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u734,negated_conjecture,
c8_1(a429) ).
cnf(u739,negated_conjecture,
~ ssSkC42 ).
cnf(u744,negated_conjecture,
~ c4_1(a403) ).
cnf(u748,negated_conjecture,
~ ssSkC33 ).
cnf(u753,negated_conjecture,
~ c1_0 ).
cnf(u756,negated_conjecture,
c3_1(a327) ).
cnf(u761,negated_conjecture,
c9_0 ).
cnf(u766,negated_conjecture,
~ c10_1(a265) ).
cnf(u770,negated_conjecture,
c8_1(a425) ).
cnf(u774,negated_conjecture,
ssSkC41 ).
cnf(u779,negated_conjecture,
~ ssSkC40 ).
cnf(u784,negated_conjecture,
~ c2_1(a408) ).
cnf(u787,negated_conjecture,
ssSkC35 ).
cnf(u792,negated_conjecture,
~ ssSkC34 ).
cnf(u796,negated_conjecture,
c8_1(a397) ).
cnf(u801,negated_conjecture,
~ ssSkC31 ).
cnf(u810,negated_conjecture,
~ c6_1(a376) ).
cnf(u813,negated_conjecture,
ssSkC24 ).
cnf(u817,negated_conjecture,
ssSkC23 ).
cnf(u822,negated_conjecture,
c2_0 ).
cnf(u831,negated_conjecture,
~ ssSkC16 ).
cnf(u836,negated_conjecture,
~ c10_0 ).
cnf(u840,negated_conjecture,
~ c5_1(a337) ).
cnf(u843,negated_conjecture,
ssSkC15 ).
cnf(u849,negated_conjecture,
~ c7_0 ).
cnf(u852,negated_conjecture,
c3_0 ).
cnf(u857,negated_conjecture,
~ c2_1(a342) ).
cnf(u862,negated_conjecture,
~ c4_2(a418,a419) ).
cnf(u865,negated_conjecture,
ssSkC38 ).
cnf(u870,negated_conjecture,
~ ssSkC37 ).
cnf(u884,negated_conjecture,
c4_0 ).
cnf(u893,negated_conjecture,
~ ssSkC18 ).
cnf(u899,negated_conjecture,
~ ssSkC29 ).
cnf(u902,negated_conjecture,
ssSkC28 ).
cnf(u906,negated_conjecture,
~ c9_2(X0,a394) ).
cnf(u921,negated_conjecture,
~ c10_2(a414,a415) ).
cnf(u924,negated_conjecture,
~ c5_1(X0) ).
cnf(u944,negated_conjecture,
ndr1_1(a403) ).
cnf(u972,negated_conjecture,
c10_1(a423) ).
cnf(u977,negated_conjecture,
ssSkC39 ).
cnf(u985,negated_conjecture,
~ c2_1(a417) ).
cnf(u991,negated_conjecture,
c3_1(a417) ).
cnf(u1004,negated_conjecture,
ssSkC26 ).
cnf(u1013,negated_conjecture,
ndr1_1(a374) ).
cnf(u1018,negated_conjecture,
c10_1(a374) ).
cnf(u1022,negated_conjecture,
~ c2_1(a374) ).
cnf(u1028,negated_conjecture,
ssSkC19 ).
cnf(u1038,negated_conjecture,
ndr1_1(a335) ).
cnf(u1043,negated_conjecture,
c3_1(a335) ).
cnf(u1048,negated_conjecture,
ssSkC14 ).
cnf(u1057,negated_conjecture,
ssSkC12 ).
cnf(u1066,negated_conjecture,
ssSkC2 ).
cnf(u1076,negated_conjecture,
~ c6_1(a423) ).
cnf(u1081,negated_conjecture,
ssSkC32 ).
cnf(u1090,negated_conjecture,
c7_1(a335) ).
cnf(u1117,negated_conjecture,
c9_1(a227) ).
cnf(u1121,negated_conjecture,
~ ssSkC0 ).
cnf(u1131,negated_conjecture,
c2_2(a335,a336) ).
cnf(u1136,negated_conjecture,
c8_2(a335,a336) ).
cnf(u1146,negated_conjecture,
~ c4_1(a314) ).
cnf(u1150,negated_conjecture,
~ ssSkC11 ).
cnf(u1161,negated_conjecture,
~ c4_1(a229) ).
cnf(u1165,negated_conjecture,
~ ssSkC1 ).
cnf(u1184,negated_conjecture,
~ c4_2(a335,a336) ).
cnf(u1192,negated_conjecture,
c2_2(X0,a378) ).
cnf(u1195,negated_conjecture,
ssSkP19(X0) ).
cnf(u1198,negated_conjecture,
c2_2(X0,a365) ).
cnf(u1201,negated_conjecture,
ssSkP17(X0) ).
cnf(u1207,negated_conjecture,
ssSkP16(X0) ).
cnf(u1213,negated_conjecture,
ssSkP15(X0) ).
cnf(u1216,negated_conjecture,
c1_2(X0,a307) ).
cnf(u1219,negated_conjecture,
ssSkP14(X0) ).
cnf(u1222,negated_conjecture,
c5_2(X0,a305) ).
cnf(u1225,negated_conjecture,
ssSkP13(X0) ).
cnf(u1228,negated_conjecture,
c5_2(X0,a302) ).
cnf(u1231,negated_conjecture,
ssSkP12(X0) ).
cnf(u1234,negated_conjecture,
c2_2(X0,a300) ).
cnf(u1237,negated_conjecture,
ssSkP11(X0) ).
cnf(u1240,negated_conjecture,
c1_2(X0,a290) ).
cnf(u1246,negated_conjecture,
c1_2(X0,a277) ).
cnf(u1249,negated_conjecture,
ssSkP7(X0) ).
cnf(u1252,negated_conjecture,
c2_2(X0,a275) ).
cnf(u1255,negated_conjecture,
ssSkP6(X0) ).
cnf(u1258,negated_conjecture,
c3_2(X0,a271) ).
cnf(u1261,negated_conjecture,
ssSkP5(X0) ).
cnf(u1264,negated_conjecture,
c10_2(X0,a260) ).
cnf(u1270,negated_conjecture,
c1_2(X0,a254) ).
cnf(u1273,negated_conjecture,
ssSkP3(X0) ).
cnf(u1279,negated_conjecture,
ssSkP2(X0) ).
cnf(u1282,negated_conjecture,
c10_2(X0,a231) ).
cnf(u1285,negated_conjecture,
ssSkP1(X0) ).
cnf(u1288,negated_conjecture,
c6_2(X0,a225) ).
cnf(u1291,negated_conjecture,
ssSkP0(X0) ).
cnf(u1310,negated_conjecture,
ssSkP18(X0) ).
cnf(u1316,negated_conjecture,
ssSkP10(X0) ).
cnf(u1319,negated_conjecture,
~ c2_2(X0,a279) ).
cnf(u1336,negated_conjecture,
ssSkC17 ).
cnf(u1342,negated_conjecture,
c1_2(X0,a344) ).
cnf(u1366,negated_conjecture,
c2_2(X0,a243) ).
cnf(u1378,negated_conjecture,
ssSkC27 ).
cnf(u1381,negated_conjecture,
c3_1(X0) ).
cnf(u1384,negated_conjecture,
c7_1(X0) ).
cnf(u1387,negated_conjecture,
c6_2(X0,a386) ).
cnf(u1453,negated_conjecture,
c9_1(a293) ).
cnf(u1457,negated_conjecture,
~ ssSkC7 ).
cnf(u1483,negated_conjecture,
c5_2(a262,X0) ).
cnf(u1503,negated_conjecture,
~ c5_1(a269) ).
cnf(u1508,negated_conjecture,
~ ssSkC3 ).
cnf(u1512,negated_conjecture,
c4_2(X0,a268) ).
cnf(u1519,negated_conjecture,
~ c2_2(X0,a268) ).
cnf(u1523,negated_conjecture,
~ c3_2(X0,a268) ).
cnf(u1539,negated_conjecture,
~ c4_2(X0,a261) ).
cnf(u1542,negated_conjecture,
c7_2(X0,a261) ).
cnf(u1547,negated_conjecture,
c9_1(X0) ).
cnf(u1550,negated_conjecture,
c4_2(X0,a405) ).
cnf(u1553,negated_conjecture,
( c4_2(X0,a405)
| c9_1(X0) ) ).
cnf(u1560,negated_conjecture,
c10_2(X0,a395) ).
cnf(u1563,negated_conjecture,
( c10_2(X0,a395)
| c5_1(X0) ) ).
cnf(u1569,negated_conjecture,
c3_2(X0,a395) ).
cnf(u1572,negated_conjecture,
( c3_2(X0,a395)
| c5_1(X0) ) ).
cnf(u1577,negated_conjecture,
c5_2(X0,a391) ).
cnf(u1580,negated_conjecture,
( ~ c1_1(X0)
| c5_1(X0)
| c5_2(X0,a391) ) ).
cnf(u1585,negated_conjecture,
c7_2(X0,a391) ).
cnf(u1588,negated_conjecture,
( ~ c1_1(X0)
| c5_1(X0)
| c7_2(X0,a391) ) ).
cnf(u1594,negated_conjecture,
ssSkC21 ).
cnf(u1597,negated_conjecture,
c6_2(X0,a360) ).
cnf(u1619,negated_conjecture,
ssSkC9 ).
cnf(u1633,negated_conjecture,
ssSkC6 ).
cnf(u1643,negated_conjecture,
c6_2(X0,a226) ).
cnf(u1656,negated_conjecture,
~ c9_2(X0,a395) ).
cnf(u1659,negated_conjecture,
( ~ c9_2(X0,a395)
| c5_1(X0) ) ).
cnf(u1674,negated_conjecture,
~ c6_1(X0) ).
cnf(u1677,negated_conjecture,
c3_2(X0,a313) ).
cnf(u1683,negated_conjecture,
ssSkC8 ).
cnf(u1686,negated_conjecture,
~ c2_2(X0,a297) ).
cnf(u1696,negated_conjecture,
~ c4_2(X0,a226) ).
cnf(u1702,negated_conjecture,
~ c7_2(X0,a226) ).
cnf(u1715,negated_conjecture,
c5_2(X0,a276) ).
cnf(u1719,negated_conjecture,
~ ssSkC5 ).
cnf(u1727,negated_conjecture,
c6_2(X0,a272) ).
cnf(u1731,negated_conjecture,
~ ssSkC4 ).
cnf(u1772,negated_conjecture,
~ c9_2(X0,a291) ).
cnf(u1776,negated_conjecture,
c5_2(a269,X0) ).
cnf(u1779,negated_conjecture,
c6_2(a269,X0) ).
cnf(u1837,negated_conjecture,
~ c5_2(a265,a266) ).
cnf(u1845,negated_conjecture,
~ c7_2(X0,a366) ).
cnf(u1849,negated_conjecture,
~ c9_2(X0,a366) ).
cnf(u1854,negated_conjecture,
~ c4_2(a369,a372) ).
cnf(u1858,negated_conjecture,
~ ssSkC22 ).
cnf(u1868,negated_conjecture,
~ c4_2(a411,a413) ).
cnf(u1872,negated_conjecture,
~ ssSkC36 ).
cnf(u1882,negated_conjecture,
~ c4_2(a414,a415) ).
cnf(u1885,negated_conjecture,
( ~ c8_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1893,negated_conjecture,
~ ssSkP9(X0) ).
cnf(u1896,negated_conjecture,
( ~ ssSkP9(X0)
| ~ c5_2(X0,a291) ) ).
cnf(u1973,negated_conjecture,
c2_2(X0,a402) ).
cnf(u1976,negated_conjecture,
c8_1(X0) ).
cnf(u1989,negated_conjecture,
~ c3_2(X0,a402) ).
cnf(u2003,negated_conjecture,
~ c1_1(a364) ).
cnf(u2016,negated_conjecture,
c3_2(X0,a373) ).
cnf(u2019,negated_conjecture,
( ~ c8_1(X0)
| c1_1(X0)
| c3_2(X0,a373) ) ).
cnf(u2030,negated_conjecture,
~ c8_2(X0,a373) ).
cnf(u2033,negated_conjecture,
( ~ c8_2(X0,a373)
| c1_1(X0)
| ~ c8_1(X0) ) ).
cnf(u2087,negated_conjecture,
c7_2(a281,a271) ).
cnf(u2096,negated_conjecture,
c7_2(a281,a395) ).
cnf(u2105,negated_conjecture,
c7_2(a281,a373) ).
cnf(u2114,negated_conjecture,
c7_2(a281,a313) ).
cnf(u2128,negated_conjecture,
c6_2(X0,X1) ).
cnf(u2131,negated_conjecture,
c2_2(X0,a396) ).
cnf(u2173,negated_conjecture,
c6_2(X0,a396) ).
cnf(u2194,negated_conjecture,
c3_2(X0,a228) ).
cnf(u2206,negated_conjecture,
c7_2(a281,a228) ).
cnf(u2221,negated_conjecture,
~ c4_2(X0,a280) ).
cnf(u2279,negated_conjecture,
c1_2(X0,a393) ).
cnf(u2282,negated_conjecture,
ssSkP20(X0) ).
cnf(u2302,negated_conjecture,
c3_2(X0,a290) ).
cnf(u2308,negated_conjecture,
c3_2(X0,a261) ).
cnf(u2314,negated_conjecture,
c3_2(X0,a391) ).
cnf(u2321,negated_conjecture,
c3_2(a265,a266) ).
cnf(u2362,negated_conjecture,
c5_2(a401,X1) ).
cnf(u2365,negated_conjecture,
~ c8_2(a401,X1) ).
cnf(u2371,negated_conjecture,
~ c4_1(X0) ).
cnf(u2374,negated_conjecture,
( ~ c4_1(X0)
| c8_1(X0) ) ).
cnf(u2398,negated_conjecture,
c2_2(X0,a392) ).
cnf(u2432,negated_conjecture,
c3_2(X0,a392) ).
cnf(u2449,negated_conjecture,
ssSkC10 ).
cnf(u2452,negated_conjecture,
c1_2(X0,X1) ).
cnf(u2455,negated_conjecture,
c5_2(X0,a306) ).
cnf(u2608,negated_conjecture,
c4_2(X0,a377) ).
cnf(u2611,negated_conjecture,
( ~ c4_1(X0)
| c4_2(X0,a377) ) ).
cnf(u2682,negated_conjecture,
c2_2(a376,a271) ).
cnf(u2691,negated_conjecture,
c2_2(a376,a395) ).
cnf(u2700,negated_conjecture,
c2_2(a376,a373) ).
cnf(u2709,negated_conjecture,
c2_2(a376,a313) ).
cnf(u2718,negated_conjecture,
c2_2(a376,a228) ).
cnf(u2727,negated_conjecture,
c2_2(a376,a261) ).
cnf(u2742,negated_conjecture,
c3_2(X0,a270) ).
cnf(u2771,negated_conjecture,
c7_2(a281,a270) ).
cnf(u2782,negated_conjecture,
c2_2(a376,a270) ).
cnf(u2795,negated_conjecture,
~ c9_2(X0,a392) ).
cnf(u2819,negated_conjecture,
~ c8_2(X0,a279) ).
cnf(u2822,negated_conjecture,
~ c9_2(X0,a279) ).
cnf(u2825,negated_conjecture,
~ ssSkP8(X0) ).
cnf(u2851,negated_conjecture,
~ c10_2(X0,a270) ).
cnf(u2879,negated_conjecture,
c9_2(X0,a361) ).
cnf(u2899,negated_conjecture,
~ c2_2(X0,a361) ).
cnf(u2916,negated_conjecture,
~ c8_2(X0,a361) ).
cnf(u2933,negated_conjecture,
~ c10_2(a383,a385) ).
cnf(u2939,negated_conjecture,
( ~ c3_2(X0,X1)
| c9_2(X0,X1)
| ~ c8_2(X0,X1) ) ).
cnf(u2992,negated_conjecture,
c9_2(X0,a271) ).
cnf(u2995,negated_conjecture,
~ c8_2(X0,a271) ).
cnf(u2998,negated_conjecture,
c9_2(X0,a313) ).
cnf(u3001,negated_conjecture,
~ c8_2(X0,a313) ).
cnf(u3004,negated_conjecture,
c9_2(X0,a228) ).
cnf(u3007,negated_conjecture,
~ c8_2(X0,a228) ).
cnf(u3010,negated_conjecture,
c9_2(X0,a270) ).
cnf(u3013,negated_conjecture,
~ c8_2(X0,a270) ).
cnf(u3017,negated_conjecture,
~ c8_2(a265,a266) ).
cnf(u3025,negated_conjecture,
c9_2(X0,a290) ).
cnf(u3028,negated_conjecture,
~ c8_2(X0,a290) ).
cnf(u3031,negated_conjecture,
c9_2(X0,a261) ).
cnf(u3034,negated_conjecture,
~ c8_2(X0,a261) ).
cnf(u3037,negated_conjecture,
c9_2(X0,a391) ).
cnf(u3040,negated_conjecture,
~ c8_2(X0,a391) ).
cnf(u2637,negated_conjecture,
c2_2(a376,a290) ).
cnf(u1970,negated_conjecture,
c7_2(X0,a290) ).
cnf(u2589,negated_conjecture,
c8_0 ).
cnf(u731,negated_conjecture,
~ c6_0 ).
cnf(u2988,negated_conjecture,
~ c8_2(X0,a392) ).
cnf(u1498,negated_conjecture,
~ c5_1(a259) ).
cnf(u727,negated_conjecture,
ndr1_0 ).
cnf(u1898,negated_conjecture,
c8_1(a265) ).
cnf(u1693,negated_conjecture,
( ~ c4_2(X0,a226)
| ~ c5_1(X0) ) ).
cnf(u2736,negated_conjecture,
( ~ c7_2(X0,X1)
| c8_2(X0,X1)
| c3_2(X0,a270)
| c10_1(X0) ) ).
cnf(u1969,negated_conjecture,
c5_2(X0,a290) ).
cnf(u1699,negated_conjecture,
( ~ c7_2(X0,a226)
| ~ c5_1(X0) ) ).
cnf(u1704,negated_conjecture,
( ~ c6_2(X0,a416)
| ~ c1_1(X0)
| ~ c5_1(X0) ) ).
cnf(u2615,negated_conjecture,
( ~ c3_2(a376,X0)
| ~ c5_2(a376,X0)
| c2_2(a376,X0) ) ).
cnf(clause305,negated_conjecture,
( ~ c2_2(X0,a279)
| ssSkP8(X0) ) ).
cnf(clause180,negated_conjecture,
( c4_2(X0,a311)
| ssSkP15(X0) ) ).
cnf(u2977,negated_conjecture,
( ~ c8_2(X0,a271)
| c9_2(X0,a271) ) ).
cnf(u1034,negated_conjecture,
c3_1(a339) ).
cnf(u2896,negated_conjecture,
( ~ c4_2(X0,X1)
| ~ c2_2(X0,a361)
| c2_2(X0,X1) ) ).
cnf(clause171,negated_conjecture,
( c9_2(X0,a348)
| ssSkP16(X0) ) ).
cnf(u2848,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ c10_2(X0,a270)
| c8_2(X0,X1)
| c10_1(X0) ) ).
cnf(clause201,negated_conjecture,
( c1_2(X0,a254)
| ssSkP3(X0) ) ).
cnf(clause195,negated_conjecture,
( c2_2(X0,a275)
| ssSkP6(X0) ) ).
cnf(clause160,negated_conjecture,
( c1_2(X0,a393)
| ssSkP20(X0) ) ).
cnf(clause197,negated_conjecture,
( c3_2(X0,a271)
| ssSkP5(X0) ) ).
cnf(u1671,negated_conjecture,
( c3_2(X0,a313)
| ~ c6_1(X0)
| ~ c5_1(X0) ) ).
cnf(u946,negated_conjecture,
ndr1_1(a281) ).
cnf(u1968,negated_conjecture,
c7_2(a265,a266) ).
cnf(u966,negated_conjecture,
c10_1(a427) ).
cnf(u2441,negated_conjecture,
c7_2(a281,a392) ).
cnf(u3045,negated_conjecture,
( ~ c3_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c8_2(X0,X2)
| c4_2(X0,X1)
| c10_2(X0,X2)
| c10_2(X0,X3)
| c8_2(X0,X3) ) ).
cnf(u2598,negated_conjecture,
~ ssSkP4(X0) ).
cnf(u1175,negated_conjecture,
~ c10_2(a427,a428) ).
cnf(u2389,negated_conjecture,
( c7_2(X0,X1)
| c2_2(X0,X1)
| c2_2(X0,a392) ) ).
cnf(clause307,negated_conjecture,
( ~ c9_2(X0,a279)
| ssSkP8(X0) ) ).
cnf(u2636,negated_conjecture,
c2_2(a376,a391) ).
cnf(u2976,negated_conjecture,
( ~ c8_2(X0,a290)
| c9_2(X0,a290) ) ).
cnf(u1072,negated_conjecture,
~ c4_1(a259) ).
cnf(u1915,negated_conjecture,
~ c5_1(a265) ).
cnf(u1176,negated_conjecture,
~ c7_2(a427,a428) ).
cnf(u2803,negated_conjecture,
c7_2(X0,a260) ).
cnf(u2876,negated_conjecture,
( ~ c4_2(X0,X1)
| c2_2(X0,X1)
| c9_2(X0,a361) ) ).
cnf(clause186,negated_conjecture,
( c5_2(X0,a302)
| ssSkP12(X0) ) ).
cnf(u2987,negated_conjecture,
( ~ c8_2(X0,a270)
| c9_2(X0,a270) ) ).
cnf(clause188,negated_conjecture,
( c2_2(X0,a300)
| ssSkP11(X0) ) ).
cnf(clause209,negated_conjecture,
( c6_2(X0,a225)
| ssSkP0(X0) ) ).
cnf(clause181,negated_conjecture,
( c1_2(X0,a307)
| ssSkP14(X0) ) ).
cnf(u2599,negated_conjecture,
c4_2(X0,a260) ).
cnf(u965,negated_conjecture,
ndr1_1(a427) ).
cnf(u2979,negated_conjecture,
( ~ c8_2(X0,a261)
| c9_2(X0,a261) ) ).
cnf(u1640,negated_conjecture,
( c6_2(X0,a226)
| ~ c5_1(X0) ) ).
cnf(clause285,negated_conjecture,
( ~ c1_2(X0,a367)
| ssSkP18(X0) ) ).
cnf(u2597,negated_conjecture,
c1_1(a262) ).
cnf(u2801,negated_conjecture,
( ~ c4_2(X0,X1)
| c7_2(X0,X1) ) ).
cnf(u1499,negated_conjecture,
~ c5_1(a423) ).
cnf(u2792,negated_conjecture,
( ~ c9_2(X0,a392)
| c2_2(X0,X1)
| c7_2(X0,X1) ) ).
cnf(u2913,negated_conjecture,
( ~ c4_2(X0,X1)
| ~ c8_2(X0,a361)
| c2_2(X0,X1) ) ).
cnf(u1966,negated_conjecture,
c4_2(a265,a266) ).
cnf(u1125,negated_conjecture,
c9_2(a427,a428) ).
cnf(clause205,negated_conjecture,
( c4_2(X0,a232)
| ssSkP2(X0) ) ).
cnf(clause199,negated_conjecture,
( c10_2(X0,a260)
| ssSkP4(X0) ) ).
cnf(u2543,negated_conjecture,
~ c2_1(X0) ).
cnf(u1108,negated_conjecture,
c8_2(a281,a282) ).
cnf(u1087,negated_conjecture,
~ c6_1(a339) ).
cnf(u1497,negated_conjecture,
~ c5_1(a281) ).
cnf(u2806,negated_conjecture,
c7_2(X0,a405) ).
cnf(u2429,negated_conjecture,
( c7_2(X0,X1)
| c2_2(X0,X1)
| c3_2(X0,a392) ) ).
cnf(u2985,negated_conjecture,
( ~ c8_2(X0,a228)
| c9_2(X0,a228) ) ).
cnf(u1152,negated_conjecture,
~ c4_2(a281,a282) ).
cnf(u2981,negated_conjecture,
( ~ c8_2(X0,a391)
| c9_2(X0,a391) ) ).
cnf(u2989,negated_conjecture,
~ c8_2(X0,a395) ).
cnf(u2983,negated_conjecture,
( ~ c8_2(X0,a313)
| c9_2(X0,a313) ) ).
cnf(u2807,negated_conjecture,
c7_2(X0,a377) ).
cnf(clause190,negated_conjecture,
( c1_2(X0,a290)
| ssSkP9(X0) ) ).
cnf(u2600,negated_conjecture,
~ c3_2(X0,a260) ).
cnf(u2036,negated_conjecture,
( ~ c3_2(a281,X0)
| ~ c2_2(a281,X0)
| c7_2(a281,X0) ) ).
cnf(clause183,negated_conjecture,
( c5_2(X0,a305)
| ssSkP13(X0) ) ).
cnf(clause169,negated_conjecture,
( c2_2(X0,a365)
| ssSkP17(X0) ) ).
cnf(clause207,negated_conjecture,
( c10_2(X0,a231)
| ssSkP1(X0) ) ).
cnf(u2805,negated_conjecture,
c7_2(X0,a268) ).
cnf(clause193,negated_conjecture,
( c1_2(X0,a277)
| ssSkP7(X0) ) ).
cnf(u2257,negated_conjecture,
ndr1_1(X0) ).
cnf(clause165,negated_conjecture,
( c2_2(X0,a378)
| ssSkP19(X0) ) ).
cnf(clause306,negated_conjecture,
( ~ c8_2(X0,a279)
| ssSkP8(X0) ) ).
cnf(u2813,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ ssSkP8(X0)
| ~ c5_2(X0,a280)
| c3_2(X0,X1) ) ).
cnf(clause302,negated_conjecture,
( ~ c1_2(X0,a298)
| ssSkP10(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN426-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.16 % Computer : n018.cluster.edu
% 0.11/0.16 % Model : x86_64 x86_64
% 0.11/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.16 % Memory : 8046.5625MB
% 0.11/0.16 % OS : Linux 6.8.0-71-generic
% 0.11/0.16 % CPULimit : 300
% 0.11/0.16 % WCLimit : 300
% 0.11/0.16 % DateTime : Mon Sep 28 15:58:25 UTC 2026
% 0.11/0.16 % CPUTime :
% 0.11/0.16 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.19 Running first-order model finding
% 0.11/0.20 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.28 % (3508034)Will run a generic schedule for satisfiability detection.
% 0.18/0.28 % (3508041)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=995663774:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.28 % (3508040)% WARNING: option uhcvi not known.
% 0.18/0.28 % (3508039)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=976968016_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.28 % (3508043)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2443821364:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.28 % (3508040)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4000929160:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.28 % (3508042)dis+10_1_sil=32000:sp=arity:random_seed=4228741728:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.28 % (3508044)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2821540648:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.28 % (3508045)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3769861818:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.28 % (3508041) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3508034-3508041"...
% 0.18/0.28 % (3508041)...printing done.
% 0.18/0.28 % SZS status Satisfiable for theBenchmark
% 0.18/0.28 % SZS output start Saturation.
% See solution above
% 0.18/0.28 % SZS output start Definitions and Model Updates.
% 0.18/0.28 for all inputs,
% 0.18/0.28 define c5_0 := $false
% 0.18/0.28 % SZS output end Definitions and Model Updates.
% 0.18/0.28 % (3508041)------------------------------
% 0.18/0.28 % (3508041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.28 % (3508041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.28 % (3508041)CaDiCaL version: 2.1.3
% 0.18/0.28 % (3508041)Termination reason: Satisfiable
% 0.18/0.28 % (3508041)Time elapsed: 0.029 s
% 0.18/0.28 % (3508041)Peak memory usage: 14 MB
% 0.18/0.28 % (3508041)Instructions burned: 84 (million)
% 0.18/0.28 % (3508034)Success in time 0.073 s
% 0.18/0.28 % Vampire exiting
%------------------------------------------------------------------------------