%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN419-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 : n019.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:50:34 PM UTC 2026
% Result : Satisfiable 4.35s 1.32s
% Output : Saturation 5.36s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u442,negated_conjecture,
ndr1_0 ).
cnf(u446,negated_conjecture,
( ~ c2_2(X0,X1)
| c3_1(X0)
| c6_2(X0,X4)
| c4_2(X0,X4)
| c8_2(X0,X4)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1)
| ~ c4_2(X0,X1) ) ).
cnf(u458,negated_conjecture,
c8_0 ).
cnf(u462,negated_conjecture,
( ~ c3_2(X2,X3)
| c10_1(X2)
| c6_2(X2,X3)
| c7_2(X2,X3)
| ~ c5_1(X2)
| ~ ndr1_1(X2) ) ).
cnf(u470,negated_conjecture,
c3_0 ).
cnf(u487,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c3_1(X0)
| ~ c10_1(X0)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u503,negated_conjecture,
( ~ c2_1(X0)
| c3_2(X0,X3)
| c6_2(X0,X2)
| c5_2(X0,X2)
| c9_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u506,negated_conjecture,
ssSkC3 ).
cnf(u516,negated_conjecture,
~ c7_0 ).
cnf(u521,negated_conjecture,
~ c10_0 ).
cnf(u524,negated_conjecture,
( ~ c8_2(X0,X2)
| c4_2(X0,X1)
| ~ c4_2(X0,a209)
| ~ c2_2(X0,X2)
| ~ c4_2(X0,X2)
| ~ c9_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u528,negated_conjecture,
( ~ c8_2(X0,X2)
| c4_2(X0,X1)
| ~ c2_2(X0,a209)
| ~ c2_2(X0,X2)
| ~ c4_2(X0,X2)
| ~ c9_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u532,negated_conjecture,
( ~ c2_1(X3)
| c9_1(X3)
| c7_1(X3) ) ).
cnf(u546,negated_conjecture,
c6_0 ).
cnf(u554,negated_conjecture,
( ~ c8_2(X0,X2)
| c10_2(X0,a209)
| c4_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c4_2(X0,X2)
| ~ c9_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u562,negated_conjecture,
( ~ c2_2(X1,a182)
| c7_2(X1,X3)
| c10_2(X1,X3)
| c3_2(X1,X3)
| c3_2(X1,X2)
| ~ c6_2(X1,X2)
| ~ ndr1_1(X1) ) ).
cnf(u568,negated_conjecture,
ssSkC6 ).
cnf(u573,negated_conjecture,
( ~ c9_2(X1,a182)
| c7_2(X1,X3)
| c10_2(X1,X3)
| c3_2(X1,X3)
| c3_2(X1,X2)
| ~ c6_2(X1,X2)
| ~ ndr1_1(X1) ) ).
cnf(u584,negated_conjecture,
( ~ c10_1(X0)
| c1_1(X0)
| ~ c9_1(X0) ) ).
cnf(u595,negated_conjecture,
( ~ c4_2(X0,X1)
| c5_1(X0)
| c3_1(X0)
| c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u599,negated_conjecture,
( ~ c8_2(X0,a244)
| c7_2(X0,X2)
| c4_2(X0,X2)
| c7_2(X0,X1)
| c4_2(X0,X1)
| ~ c9_2(X0,X1)
| ~ c8_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u602,negated_conjecture,
ssSkC24 ).
cnf(u607,negated_conjecture,
( ~ c8_2(X0,X2)
| c7_2(X0,X2)
| c4_2(X0,X2)
| c7_2(X0,X1)
| c4_2(X0,X1)
| ~ c3_2(X0,a244)
| ~ c9_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u620,negated_conjecture,
c4_0 ).
cnf(u631,negated_conjecture,
( ~ c8_2(X0,X2)
| c5_2(X0,a244)
| c7_2(X0,X2)
| c4_2(X0,X2)
| c7_2(X0,X1)
| c4_2(X0,X1)
| ~ c9_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u639,negated_conjecture,
( ~ c1_2(X0,X2)
| c6_1(X0)
| c9_2(X0,X2)
| c3_2(X0,X1)
| c6_2(X0,X1)
| ~ c8_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u644,negated_conjecture,
c9_0 ).
cnf(u662,negated_conjecture,
ssSkC7 ).
cnf(u690,negated_conjecture,
( ~ c9_1(X2)
| c3_1(X2)
| ~ c2_1(X2) ) ).
cnf(u697,negated_conjecture,
c2_0 ).
cnf(u701,negated_conjecture,
( ~ c4_2(X0,X1)
| c10_1(X0)
| c1_2(X0,X1)
| ~ c7_1(X0)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u709,negated_conjecture,
~ ssSkC22 ).
cnf(u713,negated_conjecture,
( ~ c2_2(X0,X1)
| c8_2(X0,X1)
| ~ c7_1(X0)
| ~ c10_2(X0,a236)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u717,negated_conjecture,
( ~ c2_2(X0,X1)
| c8_2(X0,X1)
| ~ c7_1(X0)
| ~ c6_2(X0,a236)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u721,negated_conjecture,
( ~ c8_2(X0,a236)
| c8_2(X0,X1)
| ~ c7_1(X0)
| ~ c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u728,negated_conjecture,
ssSkC18 ).
cnf(u746,negated_conjecture,
~ ssSkC10 ).
cnf(u750,negated_conjecture,
( ~ c5_2(X0,a197)
| c10_2(X0,X1)
| c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c9_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u754,negated_conjecture,
( ~ c8_2(X0,a197)
| c10_2(X0,X1)
| c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c9_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u758,negated_conjecture,
( ~ c7_2(X0,a197)
| c10_2(X0,X1)
| c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c9_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u767,negated_conjecture,
( ~ c10_1(X0)
| c3_1(X0)
| c10_2(X0,X1)
| c7_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u771,negated_conjecture,
c5_0 ).
cnf(u775,negated_conjecture,
( ~ c10_2(X0,X1)
| c1_2(X0,X2)
| c10_2(X0,X2)
| c6_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u780,negated_conjecture,
ssSkC17 ).
cnf(u787,negated_conjecture,
~ ssSkC20 ).
cnf(u791,negated_conjecture,
( ~ c1_2(X0,a228)
| c8_1(X0)
| ~ c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u795,negated_conjecture,
( ~ c8_2(X0,X1)
| c8_1(X0)
| ~ c10_2(X0,a228)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u803,negated_conjecture,
( ~ c10_2(X0,X1)
| c4_1(X0)
| c8_2(X0,X1)
| ~ c9_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u807,negated_conjecture,
ndr1_1(a152) ).
cnf(u811,negated_conjecture,
( ~ c2_2(a152,X0)
| ~ c10_2(a152,X0)
| ~ c4_2(a152,X0) ) ).
cnf(u814,negated_conjecture,
ssSkC1 ).
cnf(u820,negated_conjecture,
~ c1_0 ).
cnf(u831,negated_conjecture,
ndr1_1(a232) ).
cnf(u835,negated_conjecture,
( ~ c9_2(a232,X0)
| ~ c3_2(a232,X0)
| ~ c6_2(a232,X0) ) ).
cnf(u838,negated_conjecture,
ssSkC21 ).
cnf(u859,negated_conjecture,
ndr1_1(a165) ).
cnf(u863,negated_conjecture,
( ~ c4_2(a165,X0)
| c8_2(a165,X0)
| ~ c10_2(a165,X0) ) ).
cnf(u867,negated_conjecture,
ndr1_1(a240) ).
cnf(u871,negated_conjecture,
( ~ c1_2(a240,X0)
| ~ c5_2(a240,X0)
| ~ c9_2(a240,X0) ) ).
cnf(u874,negated_conjecture,
ssSkC23 ).
cnf(u880,negated_conjecture,
~ ndr1_1(a245) ).
cnf(u888,negated_conjecture,
~ ndr1_1(a246) ).
cnf(u896,negated_conjecture,
ssSkC2 ).
cnf(u899,negated_conjecture,
( ~ c5_2(X0,a159)
| c2_1(X0)
| c10_2(X0,X1)
| c5_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u903,negated_conjecture,
( ~ c8_2(X0,a159)
| c2_1(X0)
| c10_2(X0,X1)
| c5_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u916,negated_conjecture,
ssSkC8 ).
cnf(u928,negated_conjecture,
ssSkC15 ).
cnf(u948,negated_conjecture,
~ ndr1_1(a160) ).
cnf(u955,negated_conjecture,
( ~ c2_2(a165,X0)
| c5_2(a165,X0)
| c3_2(a165,X0) ) ).
cnf(u975,negated_conjecture,
~ ssSkC12 ).
cnf(u978,negated_conjecture,
ssSkC11 ).
cnf(u983,negated_conjecture,
ndr1_1(a216) ).
cnf(u987,negated_conjecture,
( ~ c6_2(a216,X0)
| c8_2(a216,X0)
| c5_2(a216,X0) ) ).
cnf(u990,negated_conjecture,
ssSkC16 ).
cnf(u1024,negated_conjecture,
~ ndr1_1(a261) ).
cnf(u1048,negated_conjecture,
~ ndr1_1(a172) ).
cnf(u1054,negated_conjecture,
ssSkC4 ).
cnf(u1063,negated_conjecture,
( ~ c9_2(X0,a220)
| c10_1(X0)
| ~ c9_1(X0) ) ).
cnf(u1067,negated_conjecture,
( ~ c4_2(X0,a220)
| c10_1(X0)
| ~ c9_1(X0) ) ).
cnf(u1071,negated_conjecture,
( ~ c2_2(X0,a220)
| c10_1(X0)
| ~ c9_1(X0) ) ).
cnf(u1079,negated_conjecture,
ndr1_1(a171) ).
cnf(u1087,negated_conjecture,
~ ssSkC5 ).
cnf(u1091,negated_conjecture,
ndr1_1(a174) ).
cnf(u1095,negated_conjecture,
( ~ c8_2(a174,X0)
| c6_2(a174,X0)
| c4_2(a174,X0) ) ).
cnf(u1104,negated_conjecture,
~ ndr1_1(a206) ).
cnf(u1115,negated_conjecture,
~ ssSkC19 ).
cnf(u1119,negated_conjecture,
ndr1_1(a224) ).
cnf(u1123,negated_conjecture,
( ~ c9_2(a224,X0)
| c8_2(a224,X0)
| c4_2(a224,X0) ) ).
cnf(u1131,negated_conjecture,
( c1_2(X0,X1)
| ~ ndr1_1(X0)
| c8_2(X0,X1)
| c7_2(X0,X1) ) ).
cnf(u1135,negated_conjecture,
( ~ c1_2(X0,a194)
| c8_1(X0)
| ~ c10_1(X0) ) ).
cnf(u1138,negated_conjecture,
ssSkC9 ).
cnf(u1143,negated_conjecture,
( ~ c3_2(X0,a194)
| c8_1(X0)
| ~ c10_1(X0) ) ).
cnf(u1215,negated_conjecture,
( ~ c9_1(X0)
| c10_1(X0)
| ndr1_1(X0) ) ).
cnf(u1235,negated_conjecture,
( ~ c5_2(X0,a148)
| ~ c4_1(X0) ) ).
cnf(u1238,negated_conjecture,
ssSkC0 ).
cnf(u1295,negated_conjecture,
( ~ c7_2(X0,a227)
| c8_1(X0)
| ~ ssSkP4(X0) ) ).
cnf(u1319,negated_conjecture,
( ~ c3_2(X0,a203)
| c6_1(X0)
| c1_1(X0) ) ).
cnf(u1323,negated_conjecture,
~ ssSkC14 ).
cnf(u1327,negated_conjecture,
( ~ c2_2(X0,a211)
| c3_1(X0)
| ~ ssSkP3(X0) ) ).
cnf(u1331,negated_conjecture,
( ~ c4_2(X0,a211)
| c3_1(X0)
| ~ ssSkP3(X0) ) ).
cnf(u1347,negated_conjecture,
( ~ c4_1(X0)
| c3_2(X0,a148) ) ).
cnf(u1351,negated_conjecture,
( ~ c4_1(X0)
| c7_2(X0,a148) ) ).
cnf(u1363,negated_conjecture,
( ~ c2_2(X0,a260)
| ~ c2_1(X0) ) ).
cnf(u1366,negated_conjecture,
ssSkC25 ).
cnf(u1371,negated_conjecture,
( ~ c10_2(X0,a260)
| ~ c2_1(X0) ) ).
cnf(u1404,negated_conjecture,
( c6_1(X0)
| c10_2(X0,a203)
| c1_1(X0) ) ).
cnf(u1408,negated_conjecture,
( c6_1(X0)
| c7_2(X0,a203)
| c1_1(X0) ) ).
cnf(u1412,negated_conjecture,
( ~ ssSkP3(X0)
| c3_1(X0)
| c9_2(X0,a211) ) ).
cnf(u1424,negated_conjecture,
( ~ c4_1(X0)
| ndr1_1(X0) ) ).
cnf(u1432,negated_conjecture,
( ~ c2_1(X0)
| c6_2(X0,a260) ) ).
cnf(u1448,negated_conjecture,
( c6_1(X0)
| ndr1_1(X0)
| c1_1(X0) ) ).
cnf(u1452,negated_conjecture,
( ~ ssSkP3(X0)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u1477,negated_conjecture,
( ~ c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u1486,negated_conjecture,
~ c10_2(a152,a153) ).
cnf(u1501,negated_conjecture,
~ c2_2(a165,a166) ).
cnf(u1506,negated_conjecture,
~ c10_1(a173) ).
cnf(u1511,negated_conjecture,
~ c6_2(a175,a176) ).
cnf(u1516,negated_conjecture,
~ c4_2(a175,a176) ).
cnf(u1521,negated_conjecture,
~ c8_2(a190,a191) ).
cnf(u1526,negated_conjecture,
~ c8_2(a190,a192) ).
cnf(u1531,negated_conjecture,
~ c10_2(a190,a192) ).
cnf(u1536,negated_conjecture,
~ c1_2(a195,a196) ).
cnf(u1541,negated_conjecture,
~ c8_2(a216,a217) ).
cnf(u1546,negated_conjecture,
~ c6_2(a216,a217) ).
cnf(u1551,negated_conjecture,
~ c7_2(a232,a233) ).
cnf(u1561,negated_conjecture,
~ c6_2(a247,a248) ).
cnf(u1566,negated_conjecture,
~ c4_2(a247,a249) ).
cnf(u1571,negated_conjecture,
~ c10_2(a247,a249) ).
cnf(u1576,negated_conjecture,
~ c6_2(a247,a249) ).
cnf(u1586,negated_conjecture,
~ c5_2(a266,a267) ).
cnf(u1591,negated_conjecture,
~ c9_2(a266,a267) ).
cnf(u1596,negated_conjecture,
~ c2_2(a266,a268) ).
cnf(u1601,negated_conjecture,
~ c8_1(a152) ).
cnf(u1606,negated_conjecture,
c9_2(a152,a153) ).
cnf(u1611,negated_conjecture,
c7_2(a152,a153) ).
cnf(u1616,negated_conjecture,
~ c7_1(a160) ).
cnf(u1627,negated_conjecture,
c3_2(a165,a166) ).
cnf(u1632,negated_conjecture,
c5_2(a165,a166) ).
cnf(u1642,negated_conjecture,
c6_1(a173) ).
cnf(u1647,negated_conjecture,
c7_1(a173) ).
cnf(u1652,negated_conjecture,
c10_2(a175,a176) ).
cnf(u1657,negated_conjecture,
c7_2(a190,a191) ).
cnf(u1662,negated_conjecture,
c3_2(a190,a191) ).
cnf(u1667,negated_conjecture,
c4_2(a190,a192) ).
cnf(u1672,negated_conjecture,
c2_2(a195,a196) ).
cnf(u1677,negated_conjecture,
c10_2(a195,a196) ).
cnf(u1691,negated_conjecture,
~ c10_2(a216,a217) ).
cnf(u1697,negated_conjecture,
~ c5_1(a219) ).
cnf(u1702,negated_conjecture,
~ c7_1(a219) ).
cnf(u1707,negated_conjecture,
c8_2(a232,a233) ).
cnf(u1727,negated_conjecture,
~ c4_2(a240,a241) ).
cnf(u1731,negated_conjecture,
c7_2(a240,a242) ).
cnf(u1737,negated_conjecture,
~ c1_1(a246) ).
cnf(u1742,negated_conjecture,
~ c8_1(a247) ).
cnf(u1747,negated_conjecture,
c3_2(a247,a248) ).
cnf(u1752,negated_conjecture,
c5_2(a247,a248) ).
cnf(u1787,negated_conjecture,
~ c7_1(a266) ).
cnf(u1792,negated_conjecture,
c7_2(a266,a267) ).
cnf(u1797,negated_conjecture,
c6_2(a266,a268) ).
cnf(u1802,negated_conjecture,
c10_2(a266,a268) ).
cnf(u1852,negated_conjecture,
~ c4_2(a224,a225) ).
cnf(u1879,negated_conjecture,
c10_1(a160) ).
cnf(u1897,negated_conjecture,
c1_1(a175) ).
cnf(u1902,negated_conjecture,
c5_1(a175) ).
cnf(u1906,negated_conjecture,
~ ndr1_1(a175) ).
cnf(u1927,negated_conjecture,
ndr1_1(a190) ).
cnf(u1932,negated_conjecture,
c2_1(a195) ).
cnf(u1937,negated_conjecture,
c7_1(a195) ).
cnf(u1942,negated_conjecture,
ndr1_1(a195) ).
cnf(u1973,negated_conjecture,
c6_1(a232) ).
cnf(u1985,negated_conjecture,
c9_2(a240,a241) ).
cnf(u1990,negated_conjecture,
c3_2(a240,a241) ).
cnf(u1995,negated_conjecture,
c8_2(a240,a242) ).
cnf(u2000,negated_conjecture,
c5_1(a245) ).
cnf(u2005,negated_conjecture,
c9_1(a245) ).
cnf(u2010,negated_conjecture,
ndr1_1(a247) ).
cnf(u2055,negated_conjecture,
ndr1_1(a266) ).
cnf(u2070,negated_conjecture,
~ c8_1(a171) ).
cnf(u2075,negated_conjecture,
~ c1_1(a171) ).
cnf(u2080,negated_conjecture,
~ c1_1(a174) ).
cnf(u2135,negated_conjecture,
~ c5_1(a206) ).
cnf(u2155,negated_conjecture,
~ c1_1(a224) ).
cnf(u2160,negated_conjecture,
c9_2(a224,a225) ).
cnf(u2165,negated_conjecture,
c3_2(a224,a225) ).
cnf(u2180,negated_conjecture,
~ c9_1(a261) ).
cnf(u2211,negated_conjecture,
~ c5_1(a172) ).
cnf(u2265,negated_conjecture,
c9_1(a174) ).
cnf(u2411,negated_conjecture,
~ c2_1(a245) ).
cnf(u2509,negated_conjecture,
~ c10_2(a247,a227) ).
cnf(u2518,negated_conjecture,
~ c10_2(a171,a227) ).
cnf(u2527,negated_conjecture,
~ c10_2(a152,a227) ).
cnf(u2550,negated_conjecture,
c7_2(a195,a196) ).
cnf(u2570,negated_conjecture,
c8_2(a247,a227) ).
cnf(u2575,negated_conjecture,
c8_2(a171,a227) ).
cnf(u2579,negated_conjecture,
~ c8_2(a152,a227) ).
cnf(u2589,negated_conjecture,
c7_2(a173,a231) ).
cnf(u2652,negated_conjecture,
~ c6_2(a195,a196) ).
cnf(u2693,negated_conjecture,
~ c2_2(a152,a227) ).
cnf(u2706,negated_conjecture,
~ c2_2(a232,a233) ).
cnf(u2719,negated_conjecture,
~ c2_2(a247,a227) ).
cnf(u2723,negated_conjecture,
~ c10_1(a247) ).
cnf(u2732,negated_conjecture,
~ c2_2(a171,a227) ).
cnf(u2745,negated_conjecture,
~ c2_2(a240,a242) ).
cnf(u2753,negated_conjecture,
~ c3_1(a240) ).
cnf(u2758,negated_conjecture,
~ c2_2(a224,a225) ).
cnf(u2765,negated_conjecture,
c3_1(a224) ).
cnf(u2778,negated_conjecture,
c9_2(a240,a211) ).
cnf(u2795,negated_conjecture,
c9_2(a224,a211) ).
cnf(u2820,negated_conjecture,
c8_2(a245,a194) ).
cnf(u2835,negated_conjecture,
c4_2(a224,a211) ).
cnf(u2913,negated_conjecture,
~ c10_1(a195) ).
cnf(u2979,negated_conjecture,
~ c9_1(a175) ).
cnf(u2992,negated_conjecture,
~ c9_1(a195) ).
cnf(u2995,negated_conjecture,
~ c4_1(a195) ).
cnf(u3002,negated_conjecture,
~ c9_1(a266) ).
cnf(u3015,negated_conjecture,
~ c9_1(a216) ).
cnf(u3044,negated_conjecture,
~ c10_2(a232,a233) ).
cnf(u3059,negated_conjecture,
~ c10_2(a240,a242) ).
cnf(u3072,negated_conjecture,
~ c10_2(a224,a225) ).
cnf(u3085,negated_conjecture,
~ c10_2(a152,a228) ).
cnf(u3095,negated_conjecture,
~ c10_2(a171,a228) ).
cnf(u3247,negated_conjecture,
~ c9_1(a160) ).
cnf(u3256,negated_conjecture,
c8_2(a160,a194) ).
cnf(u3351,negated_conjecture,
( c1_2(a195,X0)
| c10_2(a195,X0) ) ).
cnf(u3403,negated_conjecture,
~ c2_1(a174) ).
cnf(u3445,negated_conjecture,
~ ssSkP4(a195) ).
cnf(u3458,negated_conjecture,
c10_2(a195,a187) ).
cnf(u3462,negated_conjecture,
~ ssSkP3(a195) ).
cnf(u3467,negated_conjecture,
c10_2(a195,a210) ).
cnf(u3472,negated_conjecture,
( ~ c8_2(a195,X0)
| ~ c10_2(a195,X0) ) ).
cnf(u3561,negated_conjecture,
~ c5_1(a165) ).
cnf(u3576,negated_conjecture,
~ c5_1(a240) ).
cnf(u3589,negated_conjecture,
~ c5_1(a224) ).
cnf(u3593,negated_conjecture,
c7_2(a224,a225) ).
cnf(u3602,negated_conjecture,
~ c5_1(a195) ).
cnf(u3616,negated_conjecture,
~ c5_1(a247) ).
cnf(u3629,negated_conjecture,
~ c7_2(a190,a192) ).
cnf(u3646,negated_conjecture,
~ c6_2(a224,a211) ).
cnf(u3663,negated_conjecture,
~ c7_1(a190) ).
cnf(u3675,negated_conjecture,
( c5_2(a195,X1)
| c9_2(a195,X1)
| c6_2(a195,X1) ) ).
cnf(u3739,negated_conjecture,
( ~ c8_2(a195,X1)
| c3_2(a195,X1)
| c6_2(a195,X1) ) ).
cnf(u3789,negated_conjecture,
c6_2(a247,a227) ).
cnf(u3801,negated_conjecture,
c6_1(a171) ).
cnf(u3821,negated_conjecture,
c6_2(a240,a242) ).
cnf(u3946,negated_conjecture,
c4_2(a247,a227) ).
cnf(u3963,negated_conjecture,
~ c4_2(a240,a209) ).
cnf(u4004,negated_conjecture,
~ c3_2(a247,a244) ).
cnf(u4016,negated_conjecture,
~ c3_2(a171,a244) ).
cnf(u4019,negated_conjecture,
( ~ c9_2(a171,X0)
| c7_2(a171,X0)
| c4_2(a171,X0) ) ).
cnf(u4034,negated_conjecture,
~ c3_2(a232,a244) ).
cnf(u4037,negated_conjecture,
( ~ c9_2(a232,X0)
| c7_2(a232,X0)
| c4_2(a232,X0) ) ).
cnf(u4046,negated_conjecture,
~ c3_2(a240,a244) ).
cnf(u4054,negated_conjecture,
~ c3_2(a224,a244) ).
cnf(u4107,negated_conjecture,
~ c7_1(a247) ).
cnf(u3497,negated_conjecture,
c3_2(a195,a210) ).
cnf(u2811,negated_conjecture,
c10_1(a245) ).
cnf(clause37,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(clause51,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(clause172,negated_conjecture,
( ~ c8_2(X0,a226)
| ssSkP4(X0) ) ).
cnf(clause179,negated_conjecture,
( ~ c7_2(X0,a187)
| ssSkP1(X0) ) ).
cnf(clause85,negated_conjecture,
( ssSkP6(X0)
| c10_2(X0,a254) ) ).
cnf(clause88,negated_conjecture,
( ssSkP5(X0)
| c7_2(X0,a230) ) ).
cnf(clause183,negated_conjecture,
( ~ c1_2(X0,a155)
| ssSkP0(X0) ) ).
cnf(u2376,negated_conjecture,
( c3_1(X0)
| c9_2(X0,a211)
| c7_2(X0,a210) ) ).
cnf(u3696,negated_conjecture,
~ c10_2(a195,a236) ).
cnf(clause171,negated_conjecture,
( ~ c4_2(X0,a226)
| ssSkP4(X0) ) ).
cnf(clause34,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(u2375,negated_conjecture,
( c3_1(X0)
| c9_2(X0,a211)
| c3_2(X0,a210) ) ).
cnf(clause36,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(clause43,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(clause181,negated_conjecture,
( ~ c2_2(X0,a187)
| ssSkP1(X0) ) ).
cnf(clause184,negated_conjecture,
( ~ c4_2(X0,a155)
| ssSkP0(X0) ) ).
cnf(clause97,negated_conjecture,
( ssSkP3(X0)
| c7_2(X0,a210) ) ).
cnf(u2558,negated_conjecture,
( ssSkP1(X0)
| c8_2(X0,a187) ) ).
cnf(clause169,negated_conjecture,
( ~ c8_2(X0,a254)
| ssSkP6(X0) ) ).
cnf(clause86,negated_conjecture,
( ssSkP6(X0)
| c6_2(X0,a254) ) ).
cnf(clause104,negated_conjecture,
( ssSkP2(X0)
| c7_2(X0,a198) ) ).
cnf(u2546,negated_conjecture,
( ssSkP0(X0)
| c7_2(X0,a155)
| c8_2(X0,a155) ) ).
cnf(clause45,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(clause89,negated_conjecture,
( ssSkP5(X0)
| c6_2(X0,a230) ) ).
cnf(clause178,negated_conjecture,
( ~ c5_2(X0,a198)
| ssSkP2(X0) ) ).
cnf(u3025,negated_conjecture,
( ~ c8_2(X0,X1)
| c8_1(X0)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1)
| c8_2(X0,a228)
| c7_2(X0,a228) ) ).
cnf(clause115,negated_conjecture,
( ssSkP0(X0)
| c10_2(X0,a155) ) ).
cnf(u2537,negated_conjecture,
( ~ c10_1(X0)
| c8_2(X0,a194)
| c7_2(X0,a194)
| c8_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(clause175,negated_conjecture,
( ~ c1_2(X0,a210)
| ssSkP3(X0) ) ).
cnf(u2350,negated_conjecture,
( c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u3735,negated_conjecture,
( ~ c8_2(X0,X2)
| c9_2(X0,X1)
| c3_2(X0,X2)
| c6_2(X0,X2)
| c6_1(X0)
| ~ ndr1_1(X0)
| c8_2(X0,X1)
| c7_2(X0,X1) ) ).
cnf(u2816,negated_conjecture,
c1_1(a245) ).
cnf(u3701,negated_conjecture,
~ c6_2(a195,a236) ).
cnf(clause98,negated_conjecture,
( ssSkP3(X0)
| c3_2(X0,a210) ) ).
cnf(clause170,negated_conjecture,
( ~ c3_2(X0,a230)
| ssSkP5(X0) ) ).
cnf(u2540,negated_conjecture,
( ~ c5_2(a240,X0)
| c7_2(a240,X0)
| c8_2(a240,X0)
| ~ c9_2(a240,X0) ) ).
cnf(u2531,negated_conjecture,
c8_2(a224,a225) ).
cnf(clause180,negated_conjecture,
( ~ c1_2(X0,a187)
| ssSkP1(X0) ) ).
cnf(u3498,negated_conjecture,
c7_2(a195,a210) ).
cnf(clause46,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(clause90,negated_conjecture,
( ssSkP4(X0)
| c3_2(X0,a226) ) ).
cnf(u2403,negated_conjecture,
c6_2(a195,a260) ).
cnf(clause105,negated_conjecture,
( ssSkP2(X0)
| c6_2(X0,a198) ) ).
cnf(u3485,negated_conjecture,
c3_2(a195,a226) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN419-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n019.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 15:55:33 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 4.35/1.32 % (4118489)Input is clausal, will run a generic CNF schedule.
% 4.35/1.32 % (4118498)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2572852122:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.35/1.32 % (4118495)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=309930952:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.35/1.32 % (4118498)Instruction limit reached!
% 4.35/1.32 % (4118498)------------------------------
% 4.35/1.32 % (4118498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.32 % (4118498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.32 % (4118498)CaDiCaL version: 2.1.3
% 4.35/1.32 % (4118498)Termination reason: Instruction limit
% 4.35/1.32 % (4118498)Termination phase: Saturation
% 4.35/1.32 % (4118498)Time elapsed: 0.037 s
% 4.35/1.32 % (4118498)Peak memory usage: 90 MB
% 4.35/1.32 % (4118498)Instructions burned: 115 (million)
% 4.35/1.32 % (4118499)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2449087696:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.35/1.32 % (4118494)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=3503598326:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.35/1.32 % (4118496)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1025455390:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.35/1.32 % (4118497)lrs+10_1_sil=8000:sp=occurrence:random_seed=2620580492:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.35/1.32 % (4118500)dis-21_1_sil=8000:lcm=predicate:random_seed=1468646488: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)
% 4.35/1.32 % (4118499)Refutation not found, incomplete strategy
% 4.35/1.32 % (4118499)------------------------------
% 4.35/1.32 % (4118499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.32 % (4118499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.32 % (4118499)CaDiCaL version: 2.1.3
% 4.35/1.32 % (4118499)Termination reason: Refutation not found, incomplete strategy
% 4.35/1.32 % (4118499)Time elapsed: 0.017 s
% 4.35/1.32 % (4118499)Peak memory usage: 90 MB
% 4.35/1.32 % (4118499)Instructions burned: 25 (million)
% 4.35/1.32 % (4118497)Instruction limit reached!
% 4.35/1.32 % (4118497)------------------------------
% 4.35/1.32 % (4118497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.32 % (4118497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.32 % (4118497)CaDiCaL version: 2.1.3
% 4.35/1.32 % (4118497)Termination reason: Instruction limit
% 4.35/1.32 % (4118497)Termination phase: Saturation
% 4.35/1.32 % (4118497)Time elapsed: 0.055 s
% 4.35/1.32 % (4118497)Peak memory usage: 90 MB
% 4.35/1.32 % (4118497)Instructions burned: 107 (million)
% 4.35/1.32 % (4118500)Instruction limit reached!
% 4.35/1.32 % (4118500)------------------------------
% 4.35/1.32 % (4118500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.32 % (4118500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.32 % (4118500)CaDiCaL version: 2.1.3
% 4.35/1.32 % (4118500)Termination reason: Instruction limit
% 4.35/1.32 % (4118500)Termination phase: Saturation
% 4.35/1.32 % (4118500)Time elapsed: 0.062 s
% 4.35/1.32 % (4118500)Peak memory usage: 90 MB
% 4.35/1.32 % (4118500)Instructions burned: 117 (million)
% 4.35/1.32 % (4118505)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=4045455347:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 4.35/1.32 % (4118505)Refutation not found, incomplete strategy
% 4.35/1.32 % (4118505)------------------------------
% 4.35/1.32 % (4118505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.32 % (4118505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.32 % (4118505)CaDiCaL version: 2.1.3
% 4.35/1.32 % (4118505)Termination reason: Refutation not found, incomplete strategy
% 4.35/1.32 % (4118505)Time elapsed: 0.021 s
% 4.35/1.32 % (4118505)Peak memory usage: 90 MB
% 4.35/1.32 % (4118505)Instructions burned: 68 (million)
% 4.35/1.32 % (4118510)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3102888670:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 4.35/1.32 % (4118509)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3306804357: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)
% 4.35/1.32 % (4118509)Refutation not found, incomplete strategy
% 4.35/1.32 % (4118509)------------------------------
% 4.35/1.32 % (4118509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.32 % (4118509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.32 % (4118509)CaDiCaL version: 2.1.3
% 4.35/1.32 % (4118509)Termination reason: Refutation not found, incomplete strategy
% 4.35/1.32 % (4118509)Time elapsed: 0.027 s
% 4.35/1.32 % (4118509)Peak memory usage: 90 MB
% 4.35/1.32 % (4118509)Instructions burned: 46 (million)
% 4.35/1.32 % (4118505)------------------------------
% 4.35/1.32 % (4118505)------------------------------
% 4.35/1.32 % (4118499)------------------------------
% 4.35/1.32 % (4118499)------------------------------
% 4.35/1.32 % (4118510)Instruction limit reached!
% 4.35/1.32 % (4118510)------------------------------
% 4.35/1.32 % (4118510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.32 % (4118510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.32 % (4118510)CaDiCaL version: 2.1.3
% 4.35/1.32 % (4118510)Termination reason: Instruction limit
% 4.35/1.32 % (4118510)Termination phase: Saturation
% 4.35/1.32 % (4118510)Time elapsed: 0.118 s
% 4.35/1.32 % (4118510)Peak memory usage: 91 MB
% 4.35/1.32 % (4118510)Instructions burned: 220 (million)
% 4.35/1.32 % (4118514)lrs+10_64_to=lpo:sil=8000:random_seed=4134930776:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 4.35/1.32 % (4118514)First to succeed.
% 4.35/1.32 % (4118514)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4118489"
% 4.35/1.32 % (4118515)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2033696645:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 4.35/1.32 % (4118515)Refutation not found, incomplete strategy
% 4.35/1.32 % (4118515)------------------------------
% 4.35/1.32 % (4118515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.32 % (4118515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.32 % (4118515)CaDiCaL version: 2.1.3
% 4.35/1.32 % (4118515)Termination reason: Refutation not found, incomplete strategy
% 4.35/1.32 % (4118515)Time elapsed: 0.013 s
% 4.35/1.32 % (4118515)Peak memory usage: 89 MB
% 4.35/1.32 % (4118515)Instructions burned: 19 (million)
% 4.35/1.32 % (4118516)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2843211134:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 4.35/1.32 % (4118509)------------------------------
% 4.35/1.32 % (4118509)------------------------------
% 4.35/1.32 % SZS status Satisfiable for theBenchmark
% 4.35/1.32 % SZS output start Saturation.
% See solution above
% 5.36/1.52 % SZS output start Definitions and Model Updates.
% 5.36/1.52 % SZS output end Definitions and Model Updates.
% 5.36/1.52 % (4118514)------------------------------
% 5.36/1.52 % (4118514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.36/1.52 % (4118514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.36/1.52 % (4118514)CaDiCaL version: 2.1.3
% 5.36/1.52 % (4118514)Termination reason: Satisfiable
% 5.36/1.52 % (4118514)Time elapsed: 0.016 s
% 5.36/1.52 % (4118514)Peak memory usage: 90 MB
% 5.36/1.52 % (4118514)Instructions burned: 46 (million)
% 5.36/1.52 % (4118514)------------------------------
% 5.36/1.52 % (4118514)------------------------------
% 5.36/1.52 % (4118489)Success in time 0.673 s
% 5.36/1.52 % Vampire exiting
%------------------------------------------------------------------------------