%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN545-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 : n004.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:55 PM UTC 2026
% Result : Satisfiable 2.96s 1.04s
% Output : Saturation 4.78s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u521,negated_conjecture,
~ c5_0 ).
cnf(u532,negated_conjecture,
ndr1_0 ).
cnf(u536,negated_conjecture,
( ~ c6_2(X0,X1)
| ~ c3_1(X0)
| ~ c3_2(X0,X2)
| ~ c1_2(X0,X2)
| ~ c8_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u545,negated_conjecture,
~ ndr1_1(a189) ).
cnf(u554,negated_conjecture,
ssSkC6 ).
cnf(u567,negated_conjecture,
( ~ c6_2(X2,X3)
| c3_2(X2,X3)
| ~ c5_1(X2)
| ~ c3_1(X2)
| ~ ndr1_1(X2) ) ).
cnf(u589,negated_conjecture,
c4_0 ).
cnf(u593,negated_conjecture,
( ~ c6_2(X2,X3)
| c3_1(X2)
| c2_1(X2)
| ~ ndr1_1(X2)
| ~ c8_2(X2,X3)
| ~ c3_2(X2,X3) ) ).
cnf(u610,negated_conjecture,
c2_0 ).
cnf(u621,negated_conjecture,
( ~ c4_2(X0,X1)
| c2_1(X0)
| c2_2(X0,X1)
| c8_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u625,negated_conjecture,
( ~ c3_2(X1,X2)
| c6_1(X1)
| c5_2(X1,X2)
| c7_2(X1,X2)
| ~ c2_1(X1)
| ~ ndr1_1(X1) ) ).
cnf(u628,negated_conjecture,
ssSkC27 ).
cnf(u647,negated_conjecture,
~ ssSkC8 ).
cnf(u666,negated_conjecture,
( ~ c5_2(X0,X1)
| c4_2(X0,X1)
| c2_2(X0,X1)
| ~ c2_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u669,negated_conjecture,
ssSkC11 ).
cnf(u674,negated_conjecture,
c8_0 ).
cnf(u682,negated_conjecture,
( ~ c6_2(X0,X2)
| c7_1(X0)
| c4_2(X0,X2)
| c7_2(X0,X2)
| c4_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u699,negated_conjecture,
( ~ c5_2(X0,X1)
| c1_1(X0)
| c2_2(X0,X1)
| c3_2(X0,X1)
| ~ c7_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u704,negated_conjecture,
~ ndr1_1(a274) ).
cnf(u713,negated_conjecture,
ssSkC24 ).
cnf(u718,negated_conjecture,
( ~ c6_2(X0,X1)
| ~ c8_1(X0)
| ~ c1_2(X0,X2)
| ~ c4_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u727,negated_conjecture,
( ~ c5_2(X0,a220)
| c8_2(X0,X2)
| c6_2(X0,X1)
| ~ c8_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c1_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u730,negated_conjecture,
ssSkC13 ).
cnf(u735,negated_conjecture,
( ~ c1_2(X0,X2)
| c8_2(X0,X2)
| c6_2(X0,X1)
| ~ c3_2(X0,a220)
| ~ c7_2(X0,X2)
| ~ c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u749,negated_conjecture,
~ c6_1(a189) ).
cnf(u763,negated_conjecture,
( ~ c1_2(X0,X2)
| c1_2(X0,a220)
| c8_2(X0,X2)
| c6_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u767,negated_conjecture,
~ c1_0 ).
cnf(u771,negated_conjecture,
( ~ c1_2(X0,X1)
| c6_2(X0,X2)
| c7_2(X0,X2)
| c5_2(X0,X1)
| c4_2(X0,X1)
| ~ c1_1(X0)
| ~ c8_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u775,negated_conjecture,
ndr1_1(a160) ).
cnf(u779,negated_conjecture,
~ c6_2(a160,X3) ).
cnf(u793,negated_conjecture,
( ~ c6_2(X0,X1)
| c8_1(X0)
| c7_2(X0,X2)
| c6_2(X0,X2)
| c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u796,negated_conjecture,
ssSkC7 ).
cnf(u806,negated_conjecture,
( ~ c6_2(X0,X2)
| c6_1(X0)
| c5_2(X0,X2)
| ~ c8_2(X0,X2)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u810,negated_conjecture,
c3_0 ).
cnf(u814,negated_conjecture,
( ~ c5_2(X0,X1)
| c4_2(X0,X2)
| c3_2(X0,X2)
| c4_2(X0,X1)
| ~ c3_2(X0,a147)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u818,negated_conjecture,
( ~ c5_2(X0,X1)
| c4_2(X0,X2)
| c3_2(X0,X2)
| c4_2(X0,X1)
| ~ c7_2(X0,a147)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u832,negated_conjecture,
~ c6_0 ).
cnf(u843,negated_conjecture,
( ~ c5_1(X0)
| c3_1(X0)
| c1_1(X0) ) ).
cnf(u851,negated_conjecture,
( ~ c6_2(X0,X1)
| c5_1(X0)
| c2_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u865,negated_conjecture,
( ~ c5_2(X0,X1)
| c5_2(X0,a147)
| c4_2(X0,X2)
| c3_2(X0,X2)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u879,negated_conjecture,
c7_0 ).
cnf(u883,negated_conjecture,
( ~ c5_2(X0,X1)
| c7_2(X0,X1)
| ~ c5_1(X0)
| ~ c3_2(X0,a152)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u887,negated_conjecture,
( ~ c5_2(X0,X1)
| c7_2(X0,X1)
| ~ c5_1(X0)
| ~ c4_2(X0,a152)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u897,negated_conjecture,
~ c5_2(a160,a161) ).
cnf(u927,negated_conjecture,
ndr1_1(a296) ).
cnf(u931,negated_conjecture,
( ~ c6_2(a296,X0)
| c2_2(a296,X0)
| ~ c7_2(a296,X0) ) ).
cnf(u935,negated_conjecture,
( ~ c6_2(X0,X1)
| c4_1(X0)
| c8_2(X0,X1)
| ~ c8_1(X0)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u939,negated_conjecture,
( ~ c5_2(X0,X1)
| c2_1(X0)
| c3_2(X0,X1)
| ~ c7_1(X0)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u947,negated_conjecture,
( ~ c5_2(X0,X1)
| c7_2(X0,a152)
| c7_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u957,negated_conjecture,
~ c6_1(a160) ).
cnf(u962,negated_conjecture,
c2_2(a160,a161) ).
cnf(u967,negated_conjecture,
c8_2(a160,a161) ).
cnf(u985,negated_conjecture,
~ ndr1_1(a252) ).
cnf(u1004,negated_conjecture,
ssSkC18 ).
cnf(u1008,negated_conjecture,
( ~ c5_2(X0,X1)
| c7_2(X0,X1)
| c8_2(X0,X1)
| ~ c1_2(X0,a240)
| ~ ndr1_1(X0)
| ~ ssSkP2(X0) ) ).
cnf(u1012,negated_conjecture,
( ~ c6_2(X0,a261)
| c1_2(X0,X1)
| c8_2(X0,X1)
| ~ ssSkP5(X0)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u1024,negated_conjecture,
( ~ c2_2(X0,X1)
| c3_1(X0)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u1028,negated_conjecture,
( ~ c1_2(X0,X1)
| c1_1(X0)
| c8_1(X0)
| c5_2(X0,X1)
| c7_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1035,negated_conjecture,
ssSkC4 ).
cnf(u1040,negated_conjecture,
~ ssSkC3 ).
cnf(u1052,negated_conjecture,
( ~ c5_2(X0,X1)
| c7_2(X0,a240)
| c7_2(X0,X1)
| c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ssSkP2(X0) ) ).
cnf(u1056,negated_conjecture,
( ~ c7_2(X0,X1)
| c1_2(X0,a261)
| c1_2(X0,X1)
| c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ssSkP5(X0) ) ).
cnf(u1060,negated_conjecture,
( ~ c7_2(X0,X1)
| c2_2(X0,a261)
| c1_2(X0,X1)
| c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ssSkP5(X0) ) ).
cnf(u1101,negated_conjecture,
( c6_1(X1)
| c2_1(X1)
| c8_1(X1) ) ).
cnf(u1117,negated_conjecture,
~ c7_1(a274) ).
cnf(u1146,negated_conjecture,
~ ndr1_1(a186) ).
cnf(u1153,negated_conjecture,
( ~ c2_1(X0)
| c7_2(X0,a201)
| c7_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1156,negated_conjecture,
ssSkC10 ).
cnf(u1160,negated_conjecture,
ssSkC9 ).
cnf(u1165,negated_conjecture,
( ~ c2_1(X0)
| c8_2(X0,a201)
| c7_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1169,negated_conjecture,
( ~ c2_1(X0)
| c1_2(X0,a201)
| c7_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1181,negated_conjecture,
~ ssSkC16 ).
cnf(u1186,negated_conjecture,
~ ndr1_1(a249) ).
cnf(u1192,negated_conjecture,
ssSkC20 ).
cnf(u1209,negated_conjecture,
( ~ c8_1(X1)
| c6_1(X1)
| c1_1(X1) ) ).
cnf(u1229,negated_conjecture,
~ ndr1_1(a182) ).
cnf(u1241,negated_conjecture,
~ ndr1_1(a277) ).
cnf(u1247,negated_conjecture,
ssSkC25 ).
cnf(u1252,negated_conjecture,
~ ssSkC1 ).
cnf(u1256,negated_conjecture,
ndr1_1(a155) ).
cnf(u1260,negated_conjecture,
( ~ c2_2(a155,X0)
| c3_2(a155,X0)
| ~ c4_2(a155,X0) ) ).
cnf(u1273,negated_conjecture,
ssSkC5 ).
cnf(u1285,negated_conjecture,
~ ndr1_1(a226) ).
cnf(u1304,negated_conjecture,
ndr1_1(a158) ).
cnf(u1308,negated_conjecture,
( ~ c1_2(a158,X0)
| c8_2(a158,X0)
| c4_2(a158,X0) ) ).
cnf(u1313,negated_conjecture,
~ c1_2(a171,a172) ).
cnf(u1325,negated_conjecture,
~ ndr1_1(a229) ).
cnf(u1332,negated_conjecture,
( ~ c4_2(X0,a236)
| ~ c8_1(X0)
| ~ c6_1(X0) ) ).
cnf(u1336,negated_conjecture,
( ~ c6_2(X0,a236)
| ~ c8_1(X0)
| ~ c6_1(X0) ) ).
cnf(u1344,negated_conjecture,
~ ssSkC21 ).
cnf(u1360,negated_conjecture,
~ ndr1_1(a173) ).
cnf(u1368,negated_conjecture,
~ ndr1_1(a195) ).
cnf(u1387,negated_conjecture,
~ ssSkC14 ).
cnf(u1392,negated_conjecture,
~ ndr1_1(a221) ).
cnf(u1404,negated_conjecture,
ssSkC19 ).
cnf(u1416,negated_conjecture,
ssSkC26 ).
cnf(u1431,negated_conjecture,
ndr1_1(a162) ).
cnf(u1435,negated_conjecture,
( ~ c7_2(a162,X0)
| c3_2(a162,X0)
| c8_2(a162,X0) ) ).
cnf(u1440,negated_conjecture,
~ c2_1(a171) ).
cnf(u1445,negated_conjecture,
c2_2(a171,a172) ).
cnf(u1450,negated_conjecture,
c5_2(a171,a172) ).
cnf(u1462,negated_conjecture,
( ~ c6_1(X0)
| c5_2(X0,a236)
| ~ c8_1(X0) ) ).
cnf(u1487,negated_conjecture,
ssSkC22 ).
cnf(u1504,negated_conjecture,
( ~ c1_2(X0,a293)
| c4_1(X0)
| ~ ssSkP10(X0) ) ).
cnf(u1508,negated_conjecture,
( ~ c3_2(X0,a293)
| c4_1(X0)
| ~ ssSkP10(X0) ) ).
cnf(u1516,negated_conjecture,
~ ndr1_1(a253) ).
cnf(u1520,negated_conjecture,
( ~ c5_1(X1)
| c4_1(X1) ) ).
cnf(u1532,negated_conjecture,
ssSkC2 ).
cnf(u1548,negated_conjecture,
ssSkC17 ).
cnf(u1560,negated_conjecture,
c4_1(a171) ).
cnf(u1565,negated_conjecture,
ndr1_1(a171) ).
cnf(u1569,negated_conjecture,
( ~ c5_1(X0)
| c3_1(X0)
| c5_2(X0,a185) ) ).
cnf(u1573,negated_conjecture,
( ~ c5_1(X0)
| c3_1(X0)
| c4_2(X0,a185) ) ).
cnf(u1577,negated_conjecture,
( ~ c5_1(X0)
| c3_1(X0)
| c7_2(X0,a185) ) ).
cnf(u1584,negated_conjecture,
ssSkC12 ).
cnf(u1597,negated_conjecture,
( ~ c6_1(X0)
| ndr1_1(X0)
| ~ c8_1(X0) ) ).
cnf(u1625,negated_conjecture,
( ~ ssSkP10(X0)
| c4_1(X0)
| c4_2(X0,a293) ) ).
cnf(u1630,negated_conjecture,
~ c2_2(a296,a297) ).
cnf(u1635,negated_conjecture,
~ c7_2(a296,a297) ).
cnf(u1663,negated_conjecture,
~ ssSkC15 ).
cnf(u1667,negated_conjecture,
ndr1_1(a223) ).
cnf(u1671,negated_conjecture,
( ~ c4_2(a223,X0)
| c6_2(a223,X0) ) ).
cnf(u1680,negated_conjecture,
ssSkC23 ).
cnf(u1691,negated_conjecture,
( ~ c5_1(X0)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u1721,negated_conjecture,
( ~ ssSkP10(X0)
| c4_1(X0)
| ndr1_1(X0) ) ).
cnf(u1726,negated_conjecture,
~ c7_1(a296) ).
cnf(u1731,negated_conjecture,
c5_2(a296,a297) ).
cnf(u1764,negated_conjecture,
~ ndr1_1(a235) ).
cnf(u1779,negated_conjecture,
( c2_2(a223,X0)
| c7_2(a223,X0) ) ).
cnf(u1800,negated_conjecture,
~ c7_1(a252) ).
cnf(u1818,negated_conjecture,
( c8_2(a204,X0)
| c2_2(a204,X0) ) ).
cnf(u1821,negated_conjecture,
ndr1_1(a204) ).
cnf(u1839,negated_conjecture,
c1_1(a252) ).
cnf(u1877,negated_conjecture,
~ c3_2(a166,a167) ).
cnf(u1882,negated_conjecture,
~ c8_2(a166,a167) ).
cnf(u1887,negated_conjecture,
~ c6_1(a169) ).
cnf(u1907,negated_conjecture,
~ c1_2(a281,a283) ).
cnf(u1923,negated_conjecture,
c7_2(a166,a167) ).
cnf(u1938,negated_conjecture,
c8_1(a169) ).
cnf(u1943,negated_conjecture,
c2_1(a169) ).
cnf(u1963,negated_conjecture,
~ c7_1(a186) ).
cnf(u2008,negated_conjecture,
~ c7_1(a249) ).
cnf(u2013,negated_conjecture,
~ c1_1(a249) ).
cnf(u2018,negated_conjecture,
~ c6_2(a268,a269) ).
cnf(u2023,negated_conjecture,
c2_2(a281,a282) ).
cnf(u2028,negated_conjecture,
c8_2(a281,a282) ).
cnf(u2033,negated_conjecture,
c7_2(a281,a282) ).
cnf(u2038,negated_conjecture,
c8_2(a281,a283) ).
cnf(u2043,negated_conjecture,
~ c5_2(a155,a156) ).
cnf(u2195,negated_conjecture,
ssSkC0 ).
cnf(u2201,negated_conjecture,
~ c4_1(a158) ).
cnf(u2206,negated_conjecture,
~ c6_2(a162,a163) ).
cnf(u2211,negated_conjecture,
~ c5_2(a162,a163) ).
cnf(u2216,negated_conjecture,
c7_1(a166) ).
cnf(u2221,negated_conjecture,
c1_1(a166) ).
cnf(u2226,negated_conjecture,
ndr1_1(a166) ).
cnf(u2276,negated_conjecture,
c1_1(a186) ).
cnf(u2281,negated_conjecture,
~ c1_2(a197,a198) ).
cnf(u2286,negated_conjecture,
~ c6_2(a197,a198) ).
cnf(u2301,negated_conjecture,
~ c1_1(a217) ).
cnf(u2317,negated_conjecture,
~ c7_1(a268) ).
cnf(u2322,negated_conjecture,
c5_2(a268,a269) ).
cnf(u2327,negated_conjecture,
c2_2(a268,a269) ).
cnf(u2332,negated_conjecture,
c1_2(a268,a270) ).
cnf(u2337,negated_conjecture,
c8_2(a268,a270) ).
cnf(u2342,negated_conjecture,
c6_2(a268,a270) ).
cnf(u2347,negated_conjecture,
ndr1_1(a281) ).
cnf(u2357,negated_conjecture,
~ c8_2(a294,a295) ).
cnf(u2362,negated_conjecture,
~ c2_2(a294,a295) ).
cnf(u2367,negated_conjecture,
~ c7_1(a155) ).
cnf(u2372,negated_conjecture,
c7_2(a155,a156) ).
cnf(u2377,negated_conjecture,
c2_2(a155,a156) ).
cnf(u2387,negated_conjecture,
~ c6_1(a173) ).
cnf(u2432,negated_conjecture,
~ c2_1(a221) ).
cnf(u2437,negated_conjecture,
~ c1_1(a221) ).
cnf(u2442,negated_conjecture,
~ c4_1(a223) ).
cnf(u2447,negated_conjecture,
~ c5_1(a226) ).
cnf(u2487,negated_conjecture,
~ c7_1(a253) ).
cnf(u2492,negated_conjecture,
~ c8_1(a253) ).
cnf(u2562,negated_conjecture,
c1_1(a158) ).
cnf(u2567,negated_conjecture,
~ c8_1(a162) ).
cnf(u2572,negated_conjecture,
c8_2(a162,a163) ).
cnf(u2579,negated_conjecture,
~ c1_1(a182) ).
cnf(u2586,negated_conjecture,
~ c6_1(a197) ).
cnf(u2591,negated_conjecture,
~ c8_1(a197) ).
cnf(u2596,negated_conjecture,
c4_2(a197,a198) ).
cnf(u2601,negated_conjecture,
c3_2(a204,a205) ).
cnf(u2606,negated_conjecture,
c7_2(a204,a205) ).
cnf(u2621,negated_conjecture,
c7_1(a217) ).
cnf(u2626,negated_conjecture,
c8_1(a217) ).
cnf(u2632,negated_conjecture,
c1_1(a229) ).
cnf(u2637,negated_conjecture,
~ c3_1(a235) ).
cnf(u2642,negated_conjecture,
~ c1_1(a235) ).
cnf(u2652,negated_conjecture,
~ ndr1_1(a268) ).
cnf(u2669,negated_conjecture,
~ c3_1(a294) ).
cnf(u2674,negated_conjecture,
c7_2(a294,a295) ).
cnf(u2784,negated_conjecture,
ndr1_1(a197) ).
cnf(u2789,negated_conjecture,
c8_1(a204) ).
cnf(u2801,negated_conjecture,
c2_1(a294) ).
cnf(u2806,negated_conjecture,
ndr1_1(a294) ).
cnf(u2850,negated_conjecture,
~ c3_1(a223) ).
cnf(u2863,negated_conjecture,
~ c4_2(a155,a156) ).
cnf(u2874,negated_conjecture,
~ c3_1(a268) ).
cnf(u2892,negated_conjecture,
~ c2_1(a296) ).
cnf(u2948,negated_conjecture,
~ c8_2(a171,a172) ).
cnf(u2955,negated_conjecture,
~ c3_2(a171,a172) ).
cnf(u2981,negated_conjecture,
~ ndr1_1(a169) ).
cnf(u3006,negated_conjecture,
c1_1(a204) ).
cnf(u3020,negated_conjecture,
( c2_2(a294,X0)
| c7_2(a294,X0) ) ).
cnf(u3055,negated_conjecture,
c2_1(a189) ).
cnf(u3060,negated_conjecture,
c8_1(a160) ).
cnf(u3069,negated_conjecture,
c8_1(a173) ).
cnf(u3091,negated_conjecture,
( c2_2(a197,X0)
| c7_2(a197,X0) ) ).
cnf(u3117,negated_conjecture,
ssSkP8(a204) ).
cnf(u3126,negated_conjecture,
ssSkP9(a204) ).
cnf(u3153,negated_conjecture,
c2_2(a217,a236) ).
cnf(u3156,negated_conjecture,
~ c4_2(a217,a236) ).
cnf(u3165,negated_conjecture,
~ c8_2(a217,a236) ).
cnf(u3168,negated_conjecture,
~ c3_2(a217,a236) ).
cnf(u3180,negated_conjecture,
c8_2(a158,a292) ).
cnf(u3184,negated_conjecture,
c4_2(a158,a293) ).
cnf(u3189,negated_conjecture,
c8_2(a223,a292) ).
cnf(u3193,negated_conjecture,
c4_2(a223,a293) ).
cnf(u3214,negated_conjecture,
~ c3_2(a223,a293) ).
cnf(u3225,negated_conjecture,
~ c8_1(a223) ).
cnf(u3250,negated_conjecture,
~ c3_2(a160,a161) ).
cnf(u3276,negated_conjecture,
~ c4_2(a281,a282) ).
cnf(u3294,negated_conjecture,
c3_1(a197) ).
cnf(u3308,negated_conjecture,
~ c3_1(a158) ).
cnf(u3341,negated_conjecture,
~ c7_2(a217,a236) ).
cnf(u3355,negated_conjecture,
~ c5_1(a296) ).
cnf(u3378,negated_conjecture,
~ ssSkP2(a171) ).
cnf(u3385,negated_conjecture,
~ c7_2(a171,a172) ).
cnf(u3391,negated_conjecture,
~ ssSkP2(a296) ).
cnf(u3395,negated_conjecture,
~ c1_2(a296,a240) ).
cnf(u3404,negated_conjecture,
~ ssSkP2(a217) ).
cnf(u3408,negated_conjecture,
~ c1_2(a217,a240) ).
cnf(u3453,negated_conjecture,
~ ssSkP5(a155) ).
cnf(u3470,negated_conjecture,
~ ssSkP5(a204) ).
cnf(u3488,negated_conjecture,
~ ssSkP5(a166) ).
cnf(u3498,negated_conjecture,
c1_2(a294,a295) ).
cnf(u3527,negated_conjecture,
c2_2(a223,a293) ).
cnf(u3531,negated_conjecture,
( c6_2(a223,X0)
| c7_2(a223,X0) ) ).
cnf(u3550,negated_conjecture,
ssSkP4(a223) ).
cnf(u3565,negated_conjecture,
c7_2(a223,a261) ).
cnf(u3570,negated_conjecture,
c2_1(a223) ).
cnf(u3592,negated_conjecture,
c1_2(a223,a261) ).
cnf(u3614,negated_conjecture,
c6_1(a223) ).
cnf(u3668,negated_conjecture,
c7_1(a223) ).
cnf(u3677,negated_conjecture,
~ c1_1(a294) ).
cnf(u3699,negated_conjecture,
~ c3_2(a294,a220) ).
cnf(u3702,negated_conjecture,
( ~ c8_2(a294,X0)
| ~ c4_2(a294,X0)
| c6_2(a294,X0) ) ).
cnf(u3712,negated_conjecture,
~ c1_2(a294,a220) ).
cnf(u3172,negated_conjecture,
( c4_1(X0)
| c4_2(X0,a293)
| c8_2(X0,a292) ) ).
cnf(clause214,negated_conjecture,
( ~ c8_2(X0,a290)
| ssSkP9(X0) ) ).
cnf(u3431,negated_conjecture,
c8_2(a296,a239) ).
cnf(u3136,negated_conjecture,
ssSkP5(a197) ).
cnf(clause213,negated_conjecture,
( ~ c5_2(X0,a292)
| ssSkP10(X0) ) ).
cnf(clause163,negated_conjecture,
( ssSkP0(X0)
| c6_2(X0,a206) ) ).
cnf(clause63,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(clause216,negated_conjecture,
( ~ c1_2(X0,a290)
| ssSkP9(X0) ) ).
cnf(clause142,negated_conjecture,
( ssSkP3(X0)
| c8_2(X0,a250) ) ).
cnf(clause154,negated_conjecture,
( ssSkP1(X0)
| c3_2(X0,a224) ) ).
cnf(u3173,negated_conjecture,
( c4_1(X0)
| c4_2(X0,a293)
| c7_2(X0,a292) ) ).
cnf(u3111,negated_conjecture,
ssSkP5(a223) ).
cnf(clause51,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(clause220,negated_conjecture,
( ~ c8_2(X0,a285)
| ssSkP8(X0) ) ).
cnf(u3082,negated_conjecture,
c1_1(a173) ).
cnf(clause58,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(clause235,negated_conjecture,
( ~ c6_2(X0,a254)
| ssSkP4(X0) ) ).
cnf(clause162,negated_conjecture,
( ssSkP0(X0)
| c3_2(X0,a206) ) ).
cnf(clause234,negated_conjecture,
( ~ c5_2(X0,a254)
| ssSkP4(X0) ) ).
cnf(u3296,negated_conjecture,
( ~ c4_2(a294,X0)
| ~ c3_2(a294,X0)
| c7_2(a294,X0) ) ).
cnf(u3207,negated_conjecture,
c6_2(a223,a293) ).
cnf(clause147,negated_conjecture,
( ssSkP2(X0)
| c8_2(X0,a239) ) ).
cnf(u3434,negated_conjecture,
c8_2(a217,a239) ).
cnf(u3139,negated_conjecture,
c5_2(a217,a236) ).
cnf(clause121,negated_conjecture,
( ssSkP10(X0)
| c8_2(X0,a292) ) ).
cnf(u2974,negated_conjecture,
c1_1(a169) ).
cnf(clause71,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(clause125,negated_conjecture,
( ssSkP7(X0)
| c1_2(X0,a284) ) ).
cnf(clause229,negated_conjecture,
( ~ c5_2(X0,a263)
| ssSkP6(X0) ) ).
cnf(clause215,negated_conjecture,
( ~ c3_2(X0,a290)
| ssSkP9(X0) ) ).
cnf(clause232,negated_conjecture,
( ~ c2_2(X0,a260)
| ssSkP5(X0) ) ).
cnf(u3432,negated_conjecture,
c7_2(a296,a239) ).
cnf(clause67,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(clause60,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(clause240,negated_conjecture,
( ~ c5_2(X0,a239)
| ssSkP2(X0) ) ).
cnf(clause164,negated_conjecture,
( ssSkP0(X0)
| c4_2(X0,a206) ) ).
cnf(clause243,negated_conjecture,
( ~ c5_2(X0,a224)
| ssSkP1(X0) ) ).
cnf(u3080,negated_conjecture,
c1_1(a160) ).
cnf(clause48,negated_conjecture,
( ssSkP9(X0)
| ndr1_1(X0) ) ).
cnf(clause221,negated_conjecture,
( ~ c7_2(X0,a285)
| ssSkP8(X0) ) ).
cnf(u3282,negated_conjecture,
( ~ c4_2(a223,X0)
| ~ c3_2(a223,X0)
| c7_2(a223,X0) ) ).
cnf(u3075,negated_conjecture,
c2_1(a197) ).
cnf(clause137,negated_conjecture,
( ssSkP6(X0)
| c4_2(X0,a263) ) ).
cnf(clause47,negated_conjecture,
( ssSkP10(X0)
| ndr1_1(X0) ) ).
cnf(clause59,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u2966,negated_conjecture,
( c4_1(X0)
| ndr1_1(X0) ) ).
cnf(clause50,negated_conjecture,
( ssSkP8(X0)
| ndr1_1(X0) ) ).
cnf(u3134,negated_conjecture,
ssSkP5(a294) ).
cnf(u3001,negated_conjecture,
c6_1(a217) ).
cnf(clause141,negated_conjecture,
( ssSkP3(X0)
| c7_2(X0,a250) ) ).
cnf(u3411,negated_conjecture,
c7_2(a171,a239) ).
cnf(clause138,negated_conjecture,
( ssSkP4(X0)
| c1_2(X0,a254) ) ).
cnf(clause126,negated_conjecture,
( ssSkP7(X0)
| c5_2(X0,a284) ) ).
cnf(clause231,negated_conjecture,
( ~ c7_2(X0,a260)
| ssSkP5(X0) ) ).
cnf(clause230,negated_conjecture,
( ~ c7_2(X0,a263)
| ssSkP6(X0) ) ).
cnf(u3410,negated_conjecture,
c8_2(a171,a239) ).
cnf(clause143,negated_conjecture,
( ssSkP3(X0)
| c5_2(X0,a250) ) ).
cnf(clause146,negated_conjecture,
( ssSkP2(X0)
| c7_2(X0,a239) ) ).
cnf(u3435,negated_conjecture,
c7_2(a217,a239) ).
cnf(u3109,negated_conjecture,
ndr1_1(a217) ).
cnf(clause233,negated_conjecture,
( ~ c1_2(X0,a260)
| ssSkP5(X0) ) ).
cnf(clause120,negated_conjecture,
( ssSkP10(X0)
| c7_2(X0,a292) ) ).
cnf(clause123,negated_conjecture,
( ssSkP8(X0)
| c3_2(X0,a285) ) ).
cnf(clause61,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(clause124,negated_conjecture,
( ssSkP7(X0)
| c3_2(X0,a284) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN545-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.09/0.18 % Computer : n004.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 16:27:07 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 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
% 2.96/1.04 % (502491)Input is clausal, will run a generic CNF schedule.
% 2.96/1.04 % (502502)dis-21_1_sil=8000:lcm=predicate:random_seed=2057008214: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)
% 2.96/1.04 % (502502)Instruction limit reached!
% 2.96/1.04 % (502502)------------------------------
% 2.96/1.04 % (502502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.96/1.04 % (502502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.96/1.04 % (502502)CaDiCaL version: 2.1.3
% 2.96/1.04 % (502502)Termination reason: Instruction limit
% 2.96/1.04 % (502502)Termination phase: Saturation
% 2.96/1.04 % (502502)Time elapsed: 0.034 s
% 2.96/1.04 % (502502)Peak memory usage: 90 MB
% 2.96/1.04 % (502502)Instructions burned: 119 (million)
% 2.96/1.04 % (502501)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=513416320:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.96/1.04 % (502498)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=265796903:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.96/1.04 % (502496)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=3167550739:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.96/1.04 % (502497)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1162081569:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.96/1.04 % (502499)lrs+10_1_sil=8000:sp=occurrence:random_seed=2821965400:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.96/1.04 % (502500)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4125265192:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.96/1.04 % (502501)Refutation not found, incomplete strategy
% 2.96/1.04 % (502501)------------------------------
% 2.96/1.04 % (502501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.96/1.04 % (502501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.96/1.04 % (502501)CaDiCaL version: 2.1.3
% 2.96/1.04 % (502501)Termination reason: Refutation not found, incomplete strategy
% 2.96/1.04 % (502501)Time elapsed: 0.025 s
% 2.96/1.04 % (502501)Peak memory usage: 90 MB
% 2.96/1.04 % (502501)Instructions burned: 39 (million)
% 2.96/1.04 % (502499)Instruction limit reached!
% 2.96/1.04 % (502499)------------------------------
% 2.96/1.04 % (502499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.96/1.04 % (502499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.96/1.04 % (502499)CaDiCaL version: 2.1.3
% 2.96/1.04 % (502499)Termination reason: Instruction limit
% 2.96/1.04 % (502499)Termination phase: Saturation
% 2.96/1.04 % (502499)Time elapsed: 0.061 s
% 2.96/1.04 % (502499)Peak memory usage: 90 MB
% 2.96/1.04 % (502499)Instructions burned: 107 (million)
% 2.96/1.04 % (502500)Instruction limit reached!
% 2.96/1.04 % (502500)------------------------------
% 2.96/1.04 % (502500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.96/1.04 % (502500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.96/1.04 % (502500)CaDiCaL version: 2.1.3
% 2.96/1.04 % (502500)Termination reason: Instruction limit
% 2.96/1.04 % (502500)Termination phase: Saturation
% 2.96/1.04 % (502500)Time elapsed: 0.064 s
% 2.96/1.04 % (502500)Peak memory usage: 90 MB
% 2.96/1.04 % (502500)Instructions burned: 114 (million)
% 2.96/1.04 % (502504)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=1518812815:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 2.96/1.04 % (502504)Instruction limit reached!
% 2.96/1.04 % (502504)------------------------------
% 2.96/1.04 % (502504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.96/1.04 % (502504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.96/1.04 % (502504)CaDiCaL version: 2.1.3
% 2.96/1.04 % (502504)Termination reason: Instruction limit
% 2.96/1.04 % (502504)Termination phase: Saturation
% 2.96/1.04 % (502504)Time elapsed: 0.042 s
% 2.96/1.04 % (502504)Peak memory usage: 91 MB
% 2.96/1.04 % (502504)Instructions burned: 143 (million)
% 2.96/1.04 % (502511)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1053727814:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 2.96/1.04 % (502512)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1072551416:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 2.96/1.04 % (502511)Refutation not found, incomplete strategy
% 2.96/1.04 % (502511)------------------------------
% 2.96/1.04 % (502511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.96/1.04 % (502511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.96/1.04 % (502511)CaDiCaL version: 2.1.3
% 2.96/1.04 % (502511)Termination reason: Refutation not found, incomplete strategy
% 2.96/1.04 % (502511)Time elapsed: 0.034 s
% 2.96/1.04 % (502511)Peak memory usage: 90 MB
% 2.96/1.04 % (502511)Instructions burned: 58 (million)
% 2.96/1.04 % (502514)lrs+10_64_to=lpo:sil=8000:random_seed=2344273050:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 2.96/1.04 % (502501)------------------------------
% 2.96/1.04 % (502501)------------------------------
% 2.96/1.04 % (502514)First to succeed.
% 2.96/1.04 % (502514)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-502491"
% 2.96/1.04 % (502512)Instruction limit reached!
% 2.96/1.04 % (502512)------------------------------
% 2.96/1.04 % (502512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.96/1.04 % (502512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.96/1.04 % (502512)CaDiCaL version: 2.1.3
% 2.96/1.04 % (502512)Termination reason: Instruction limit
% 2.96/1.04 % (502512)Termination phase: Saturation
% 2.96/1.04 % (502512)Time elapsed: 0.115 s
% 2.96/1.04 % (502512)Peak memory usage: 91 MB
% 2.96/1.04 % (502512)Instructions burned: 220 (million)
% 2.96/1.04 % (502518)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=850633111:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 2.96/1.04 % SZS status Satisfiable for theBenchmark
% 2.96/1.04 % SZS output start Saturation.
% See solution above
% 4.78/1.24 % SZS output start Definitions and Model Updates.
% 4.78/1.24 % SZS output end Definitions and Model Updates.
% 4.78/1.24 % (502514)------------------------------
% 4.78/1.24 % (502514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.78/1.24 % (502514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.78/1.24 % (502514)CaDiCaL version: 2.1.3
% 4.78/1.24 % (502514)Termination reason: Satisfiable
% 4.78/1.24 % (502514)Time elapsed: 0.014 s
% 4.78/1.24 % (502514)Peak memory usage: 90 MB
% 4.78/1.24 % (502514)Instructions burned: 39 (million)
% 4.78/1.24 % (502514)------------------------------
% 4.78/1.24 % (502514)------------------------------
% 4.78/1.24 % (502491)Success in time 0.621 s
% 4.78/1.24 % Vampire exiting
%------------------------------------------------------------------------------