%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN543-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 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:00:54 PM UTC 2026
% Result : Satisfiable 5.31s 1.59s
% Output : Saturation 7.08s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u329,negated_conjecture,
ndr1_0 ).
cnf(u333,negated_conjecture,
( ~ c2_1(X0)
| ~ c4_1(X0)
| ~ c3_1(X0) ) ).
cnf(u340,negated_conjecture,
( ~ c4_1(X1)
| c3_1(X1)
| ~ c5_1(X1) ) ).
cnf(u343,negated_conjecture,
( ~ c1_1(X0)
| c5_1(X0)
| ~ c3_1(X0) ) ).
cnf(u347,negated_conjecture,
( ~ c5_1(X2)
| c1_1(X2)
| ~ c3_1(X2) ) ).
cnf(u350,negated_conjecture,
( ~ c1_1(X1)
| c5_1(X1)
| c2_1(X1) ) ).
cnf(u363,negated_conjecture,
( ~ c2_1(X0)
| c5_1(X0)
| ~ c3_1(X0) ) ).
cnf(u373,negated_conjecture,
( ~ c5_1(X0)
| c2_1(X0)
| c1_1(X0) ) ).
cnf(u377,negated_conjecture,
( c2_1(X2)
| c5_1(X2)
| c3_1(X2) ) ).
cnf(u384,negated_conjecture,
( ~ c3_1(X1)
| c0_1(X1)
| ~ c4_1(X1) ) ).
cnf(u388,negated_conjecture,
( ~ c3_1(X2)
| c1_1(X2)
| c0_1(X2) ) ).
cnf(u395,negated_conjecture,
( c2_1(X2)
| c5_1(X2)
| c4_1(X2) ) ).
cnf(u408,negated_conjecture,
( ~ c0_1(X1)
| c3_1(X1)
| c2_1(X1) ) ).
cnf(u421,negated_conjecture,
( ~ c3_1(X0)
| c5_1(X0)
| c4_1(X0) ) ).
cnf(u428,negated_conjecture,
( ~ c4_1(X1)
| c2_1(X1)
| c0_1(X1) ) ).
cnf(u435,negated_conjecture,
~ hskp4 ).
cnf(u442,negated_conjecture,
( ~ c4_1(X0)
| c5_1(X0)
| ~ c3_1(X0) ) ).
cnf(u447,negated_conjecture,
hskp23 ).
cnf(u458,negated_conjecture,
hskp21 ).
cnf(u465,negated_conjecture,
~ hskp20 ).
cnf(u469,negated_conjecture,
( ~ c0_1(X1)
| c4_1(X1)
| c2_1(X1) ) ).
cnf(u476,negated_conjecture,
~ hskp19 ).
cnf(u480,negated_conjecture,
( ~ c2_1(X1)
| c1_1(X1)
| ~ c4_1(X1) ) ).
cnf(u488,negated_conjecture,
hskp61 ).
cnf(u496,negated_conjecture,
hskp60 ).
cnf(u506,negated_conjecture,
~ hskp16 ).
cnf(u513,negated_conjecture,
( ~ c0_1(X0)
| c2_1(X0)
| ~ c4_1(X0) ) ).
cnf(u518,negated_conjecture,
hskp15 ).
cnf(u528,negated_conjecture,
~ hskp10 ).
cnf(u535,negated_conjecture,
( ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0) ) ).
cnf(u540,negated_conjecture,
hskp6 ).
cnf(u553,negated_conjecture,
( ~ c3_1(X0)
| c2_1(X0)
| ~ c5_1(X0) ) ).
cnf(u557,negated_conjecture,
~ hskp59 ).
cnf(u562,negated_conjecture,
~ hskp0 ).
cnf(u566,negated_conjecture,
( ~ c0_1(X0)
| c5_1(X0)
| c2_1(X0) ) ).
cnf(u571,negated_conjecture,
hskp11 ).
cnf(u579,negated_conjecture,
hskp7 ).
cnf(u583,negated_conjecture,
~ hskp1 ).
cnf(u590,negated_conjecture,
( ~ c4_1(X0)
| c5_1(X0)
| c2_1(X0) ) ).
cnf(u594,negated_conjecture,
~ hskp5 ).
cnf(u600,negated_conjecture,
hskp3 ).
cnf(u607,negated_conjecture,
~ hskp2 ).
cnf(u616,negated_conjecture,
hskp58 ).
cnf(u619,negated_conjecture,
( c0_1(X1)
| c4_1(X1)
| c1_1(X1) ) ).
cnf(u626,negated_conjecture,
~ hskp12 ).
cnf(u630,negated_conjecture,
( c1_1(X1)
| c4_1(X1)
| c2_1(X1) ) ).
cnf(u633,negated_conjecture,
( ~ c4_1(X0)
| c3_1(X0)
| c1_1(X0) ) ).
cnf(u638,negated_conjecture,
~ hskp42 ).
cnf(u642,negated_conjecture,
( ~ c5_1(X0)
| ~ c3_1(X0)
| ~ c4_1(X0) ) ).
cnf(u646,negated_conjecture,
~ hskp41 ).
cnf(u650,negated_conjecture,
( ~ c1_1(X0)
| ~ c5_1(X0)
| ~ c4_1(X0) ) ).
cnf(u655,negated_conjecture,
hskp40 ).
cnf(u659,negated_conjecture,
hskp25 ).
cnf(u664,negated_conjecture,
hskp39 ).
cnf(u667,negated_conjecture,
~ hskp38 ).
cnf(u672,negated_conjecture,
~ hskp37 ).
cnf(u676,negated_conjecture,
~ hskp36 ).
cnf(u682,negated_conjecture,
hskp35 ).
cnf(u685,negated_conjecture,
~ hskp34 ).
cnf(u690,negated_conjecture,
~ hskp33 ).
cnf(u695,negated_conjecture,
hskp13 ).
cnf(u699,negated_conjecture,
~ hskp32 ).
cnf(u704,negated_conjecture,
hskp31 ).
cnf(u711,negated_conjecture,
~ hskp26 ).
cnf(u719,negated_conjecture,
~ hskp24 ).
cnf(u723,negated_conjecture,
( ~ c1_1(X0)
| c2_1(X0)
| ~ c4_1(X0) ) ).
cnf(u727,negated_conjecture,
~ hskp9 ).
cnf(u732,negated_conjecture,
hskp8 ).
cnf(u739,negated_conjecture,
~ hskp30 ).
cnf(u744,negated_conjecture,
hskp29 ).
cnf(u751,negated_conjecture,
~ hskp28 ).
cnf(u756,negated_conjecture,
hskp27 ).
cnf(u764,negated_conjecture,
hskp22 ).
cnf(u768,negated_conjecture,
~ hskp18 ).
cnf(u772,negated_conjecture,
~ hskp17 ).
cnf(u777,negated_conjecture,
~ hskp14 ).
cnf(u781,negated_conjecture,
( ~ c4_1(X0)
| c2_1(X0)
| c1_1(X0) ) ).
cnf(u786,negated_conjecture,
hskp62 ).
cnf(u792,negated_conjecture,
~ c1_1(a80) ).
cnf(u797,negated_conjecture,
~ c5_1(a81) ).
cnf(u802,negated_conjecture,
~ c4_1(a81) ).
cnf(u807,negated_conjecture,
~ c1_1(a81) ).
cnf(u822,negated_conjecture,
~ c4_1(a84) ).
cnf(u827,negated_conjecture,
~ c3_1(a84) ).
cnf(u831,negated_conjecture,
c2_1(a85) ).
cnf(u842,negated_conjecture,
~ c0_1(a87) ).
cnf(u847,negated_conjecture,
~ c0_1(a89) ).
cnf(u852,negated_conjecture,
~ c4_1(a90) ).
cnf(u857,negated_conjecture,
~ c2_1(a90) ).
cnf(u862,negated_conjecture,
~ c3_1(a91) ).
cnf(u866,negated_conjecture,
c2_1(a91) ).
cnf(u877,negated_conjecture,
~ c4_1(a92) ).
cnf(u881,negated_conjecture,
c0_1(a92) ).
cnf(u887,negated_conjecture,
~ c5_1(a93) ).
cnf(u892,negated_conjecture,
~ c3_1(a93) ).
cnf(u897,negated_conjecture,
~ c4_1(a94) ).
cnf(u907,negated_conjecture,
~ c5_1(a95) ).
cnf(u922,negated_conjecture,
~ c3_1(a97) ).
cnf(u931,negated_conjecture,
c5_1(a99) ).
cnf(u936,negated_conjecture,
c5_1(a100) ).
cnf(u941,negated_conjecture,
c0_1(a100) ).
cnf(u946,negated_conjecture,
c5_1(a103) ).
cnf(u951,negated_conjecture,
c1_1(a103) ).
cnf(u957,negated_conjecture,
~ c5_1(a105) ).
cnf(u962,negated_conjecture,
~ c4_1(a106) ).
cnf(u967,negated_conjecture,
~ c5_1(a108) ).
cnf(u972,negated_conjecture,
~ c3_1(a108) ).
cnf(u977,negated_conjecture,
~ c0_1(a108) ).
cnf(u982,negated_conjecture,
~ c4_1(a109) ).
cnf(u987,negated_conjecture,
~ c3_1(a109) ).
cnf(u991,negated_conjecture,
c5_1(a111) ).
cnf(u996,negated_conjecture,
c0_1(a111) ).
cnf(u1002,negated_conjecture,
~ c0_1(a113) ).
cnf(u1007,negated_conjecture,
~ c4_1(a114) ).
cnf(u1011,negated_conjecture,
c2_1(a114) ).
cnf(u1022,negated_conjecture,
~ c2_1(a115) ).
cnf(u1027,negated_conjecture,
~ c0_1(a115) ).
cnf(u1032,negated_conjecture,
~ c5_1(a116) ).
cnf(u1036,negated_conjecture,
c4_1(a116) ).
cnf(u1042,negated_conjecture,
~ c3_1(a116) ).
cnf(u1047,negated_conjecture,
~ c5_1(a117) ).
cnf(u1052,negated_conjecture,
~ c3_1(a117) ).
cnf(u1056,negated_conjecture,
c1_1(a118) ).
cnf(u1062,negated_conjecture,
~ c0_1(a118) ).
cnf(u1067,negated_conjecture,
~ c4_1(a120) ).
cnf(u1072,negated_conjecture,
~ c0_1(a121) ).
cnf(u1077,negated_conjecture,
~ c0_1(a123) ).
cnf(u1081,negated_conjecture,
c5_1(a124) ).
cnf(u1087,negated_conjecture,
~ c3_1(a125) ).
cnf(u1092,negated_conjecture,
~ c0_1(a125) ).
cnf(u1111,negated_conjecture,
c1_1(a128) ).
cnf(u1117,negated_conjecture,
~ c4_1(a129) ).
cnf(u1122,negated_conjecture,
~ c3_1(a131) ).
cnf(u1127,negated_conjecture,
~ c5_1(a133) ).
cnf(u1132,negated_conjecture,
~ c3_1(a133) ).
cnf(u1137,negated_conjecture,
~ c3_1(a135) ).
cnf(u1141,negated_conjecture,
c2_1(a135) ).
cnf(u1146,negated_conjecture,
c0_1(a135) ).
cnf(u1152,negated_conjecture,
~ hskp43 ).
cnf(u1155,negated_conjecture,
c5_1(a137) ).
cnf(u1160,negated_conjecture,
c2_1(a137) ).
cnf(u1166,negated_conjecture,
~ hskp44 ).
cnf(u1170,negated_conjecture,
~ c3_1(a138) ).
cnf(u1174,negated_conjecture,
c1_1(a138) ).
cnf(u1179,negated_conjecture,
hskp45 ).
cnf(u1184,negated_conjecture,
~ c5_1(a140) ).
cnf(u1189,negated_conjecture,
~ c3_1(a140) ).
cnf(u1194,negated_conjecture,
~ hskp46 ).
cnf(u1197,negated_conjecture,
c2_1(a141) ).
cnf(u1202,negated_conjecture,
c1_1(a141) ).
cnf(u1207,negated_conjecture,
c0_1(a141) ).
cnf(u1213,negated_conjecture,
~ hskp47 ).
cnf(u1216,negated_conjecture,
c2_1(a142) ).
cnf(u1222,negated_conjecture,
~ hskp48 ).
cnf(u1226,negated_conjecture,
~ c3_1(a143) ).
cnf(u1230,negated_conjecture,
c2_1(a143) ).
cnf(u1236,negated_conjecture,
~ hskp49 ).
cnf(u1239,negated_conjecture,
c5_1(a145) ).
cnf(u1244,negated_conjecture,
hskp50 ).
cnf(u1249,negated_conjecture,
~ c1_1(a146) ).
cnf(u1254,negated_conjecture,
~ hskp51 ).
cnf(u1258,negated_conjecture,
~ c3_1(a147) ).
cnf(u1263,negated_conjecture,
~ hskp52 ).
cnf(u1266,negated_conjecture,
c5_1(a148) ).
cnf(u1271,negated_conjecture,
hskp53 ).
cnf(u1276,negated_conjecture,
~ c4_1(a149) ).
cnf(u1281,negated_conjecture,
~ c3_1(a149) ).
cnf(u1286,negated_conjecture,
~ hskp54 ).
cnf(u1289,negated_conjecture,
c1_1(a150) ).
cnf(u1294,negated_conjecture,
c0_1(a150) ).
cnf(u1299,negated_conjecture,
hskp55 ).
cnf(u1304,negated_conjecture,
~ c5_1(a152) ).
cnf(u1309,negated_conjecture,
~ c4_1(a152) ).
cnf(u1314,negated_conjecture,
~ hskp56 ).
cnf(u1317,negated_conjecture,
c2_1(a154) ).
cnf(u1322,negated_conjecture,
c0_1(a154) ).
cnf(u1327,negated_conjecture,
hskp57 ).
cnf(u1332,negated_conjecture,
~ c3_1(a156) ).
cnf(u1337,negated_conjecture,
~ c0_1(a156) ).
cnf(u1341,negated_conjecture,
~ c5_1(a80) ).
cnf(u1346,negated_conjecture,
~ c4_1(a80) ).
cnf(u1357,negated_conjecture,
c5_1(a84) ).
cnf(u1361,negated_conjecture,
~ c4_1(a85) ).
cnf(u1367,negated_conjecture,
c0_1(a85) ).
cnf(u1382,negated_conjecture,
c3_1(a87) ).
cnf(u1387,negated_conjecture,
c2_1(a87) ).
cnf(u1392,negated_conjecture,
c3_1(a89) ).
cnf(u1397,negated_conjecture,
c1_1(a89) ).
cnf(u1402,negated_conjecture,
c1_1(a90) ).
cnf(u1407,negated_conjecture,
c3_1(a92) ).
cnf(u1412,negated_conjecture,
c0_1(a93) ).
cnf(u1416,negated_conjecture,
~ c3_1(a94) ).
cnf(u1422,negated_conjecture,
c2_1(a95) ).
cnf(u1427,negated_conjecture,
c0_1(a95) ).
cnf(u1437,negated_conjecture,
c5_1(a97) ).
cnf(u1442,negated_conjecture,
c2_1(a97) ).
cnf(u1456,negated_conjecture,
~ c4_1(a99) ).
cnf(u1462,negated_conjecture,
c3_1(a99) ).
cnf(u1472,negated_conjecture,
c3_1(a103) ).
cnf(u1476,negated_conjecture,
~ c1_1(a105) ).
cnf(u1482,negated_conjecture,
c0_1(a105) ).
cnf(u1487,negated_conjecture,
c3_1(a106) ).
cnf(u1492,negated_conjecture,
c2_1(a106) ).
cnf(u1497,negated_conjecture,
c1_1(a109) ).
cnf(u1502,negated_conjecture,
c2_1(a111) ).
cnf(u1507,negated_conjecture,
c2_1(a113) ).
cnf(u1512,negated_conjecture,
c1_1(a113) ).
cnf(u1517,negated_conjecture,
c5_1(a115) ).
cnf(u1522,negated_conjecture,
c2_1(a117) ).
cnf(u1527,negated_conjecture,
c5_1(a118) ).
cnf(u1532,negated_conjecture,
c2_1(a120) ).
cnf(u1537,negated_conjecture,
c0_1(a120) ).
cnf(u1541,negated_conjecture,
~ c4_1(a121) ).
cnf(u1546,negated_conjecture,
~ c3_1(a121) ).
cnf(u1551,negated_conjecture,
~ c5_1(a123) ).
cnf(u1556,negated_conjecture,
~ c4_1(a123) ).
cnf(u1562,negated_conjecture,
c3_1(a124) ).
cnf(u1567,negated_conjecture,
c0_1(a124) ).
cnf(u1572,negated_conjecture,
c4_1(a125) ).
cnf(u1591,negated_conjecture,
~ c4_1(a128) ).
cnf(u1596,negated_conjecture,
~ c0_1(a128) ).
cnf(u1602,negated_conjecture,
c2_1(a129) ).
cnf(u1607,negated_conjecture,
c1_1(a129) ).
cnf(u1612,negated_conjecture,
c2_1(a131) ).
cnf(u1617,negated_conjecture,
c1_1(a131) ).
cnf(u1621,negated_conjecture,
~ c1_1(a133) ).
cnf(u1632,negated_conjecture,
c4_1(a138) ).
cnf(u1637,negated_conjecture,
c4_1(a140) ).
cnf(u1642,negated_conjecture,
c5_1(a142) ).
cnf(u1646,negated_conjecture,
~ c0_1(a142) ).
cnf(u1652,negated_conjecture,
c0_1(a143) ).
cnf(u1657,negated_conjecture,
c3_1(a145) ).
cnf(u1662,negated_conjecture,
c1_1(a145) ).
cnf(u1667,negated_conjecture,
c5_1(a146) ).
cnf(u1672,negated_conjecture,
c2_1(a146) ).
cnf(u1676,negated_conjecture,
~ c5_1(a147) ).
cnf(u1681,negated_conjecture,
~ c4_1(a147) ).
cnf(u1686,negated_conjecture,
~ c4_1(a148) ).
cnf(u1692,negated_conjecture,
c1_1(a148) ).
cnf(u1697,negated_conjecture,
c2_1(a149) ).
cnf(u1701,negated_conjecture,
~ c4_1(a150) ).
cnf(u1707,negated_conjecture,
c2_1(a152) ).
cnf(u1712,negated_conjecture,
c3_1(a154) ).
cnf(u1717,negated_conjecture,
c5_1(a156) ).
cnf(u1722,negated_conjecture,
c3_1(a78) ).
cnf(u1727,negated_conjecture,
c2_1(a78) ).
cnf(u1732,negated_conjecture,
c1_1(a78) ).
cnf(u1736,negated_conjecture,
~ c4_1(a79) ).
cnf(u1742,negated_conjecture,
c3_1(a79) ).
cnf(u1747,negated_conjecture,
c0_1(a79) ).
cnf(u1752,negated_conjecture,
c5_1(a101) ).
cnf(u1757,negated_conjecture,
c3_1(a101) ).
cnf(u1762,negated_conjecture,
c1_1(a101) ).
cnf(u1767,negated_conjecture,
c3_1(a102) ).
cnf(u1772,negated_conjecture,
c2_1(a102) ).
cnf(u1777,negated_conjecture,
c0_1(a102) ).
cnf(u1782,negated_conjecture,
c2_1(a119) ).
cnf(u1787,negated_conjecture,
c1_1(a119) ).
cnf(u1792,negated_conjecture,
c0_1(a119) ).
cnf(u1797,negated_conjecture,
c4_1(a136) ).
cnf(u1800,negated_conjecture,
hskp63 ).
cnf(u1806,negated_conjecture,
c1_1(a136) ).
cnf(u1811,negated_conjecture,
c0_1(a136) ).
cnf(u1816,negated_conjecture,
c5_1(a153) ).
cnf(u1820,negated_conjecture,
~ hskp64 ).
cnf(u1824,negated_conjecture,
~ c4_1(a153) ).
cnf(u1829,negated_conjecture,
~ c3_1(a153) ).
cnf(u1996,negated_conjecture,
~ c3_1(a113) ).
cnf(u2000,negated_conjecture,
c5_1(a113) ).
cnf(u2012,negated_conjecture,
~ c3_1(a123) ).
cnf(u2016,negated_conjecture,
c1_1(a123) ).
cnf(u2024,negated_conjecture,
c2_1(a148) ).
cnf(u2060,negated_conjecture,
c1_1(a149) ).
cnf(u2065,negated_conjecture,
c0_1(a149) ).
cnf(u2084,negated_conjecture,
c0_1(a137) ).
cnf(u2087,negated_conjecture,
~ c4_1(a137) ).
cnf(u2093,negated_conjecture,
c0_1(a145) ).
cnf(u2096,negated_conjecture,
~ c4_1(a145) ).
cnf(u2107,negated_conjecture,
c0_1(a99) ).
cnf(u2111,negated_conjecture,
c1_1(a99) ).
cnf(u2148,negated_conjecture,
c1_1(a137) ).
cnf(u2169,negated_conjecture,
~ c4_1(a111) ).
cnf(u2174,negated_conjecture,
c1_1(a111) ).
cnf(u2196,negated_conjecture,
~ c2_1(a128) ).
cnf(u2200,negated_conjecture,
~ c3_1(a128) ).
cnf(u2235,negated_conjecture,
~ c4_1(a108) ).
cnf(u2240,negated_conjecture,
c1_1(a108) ).
cnf(u2262,negated_conjecture,
c2_1(a145) ).
cnf(u2309,negated_conjecture,
~ c3_1(a114) ).
cnf(u2313,negated_conjecture,
c5_1(a114) ).
cnf(u2320,negated_conjecture,
~ c3_1(a141) ).
cnf(u2324,negated_conjecture,
c5_1(a141) ).
cnf(u2418,negated_conjecture,
~ c3_1(a129) ).
cnf(u2422,negated_conjecture,
c5_1(a129) ).
cnf(u2440,negated_conjecture,
c1_1(a140) ).
cnf(u2445,negated_conjecture,
c0_1(a140) ).
cnf(u2582,negated_conjecture,
~ c3_1(a85) ).
cnf(u2587,negated_conjecture,
c5_1(a85) ).
cnf(u2606,negated_conjecture,
~ c4_1(a119) ).
cnf(u2609,negated_conjecture,
~ c3_1(a119) ).
cnf(u2624,negated_conjecture,
c0_1(a153) ).
cnf(u2628,negated_conjecture,
c1_1(a153) ).
cnf(u2660,negated_conjecture,
c2_1(a150) ).
cnf(u2663,negated_conjecture,
~ c3_1(a150) ).
cnf(u2796,negated_conjecture,
c0_1(a103) ).
cnf(u2799,negated_conjecture,
~ c4_1(a103) ).
cnf(u2806,negated_conjecture,
c2_1(a103) ).
cnf(u2835,negated_conjecture,
c5_1(a119) ).
cnf(u2840,negated_conjecture,
c5_1(a150) ).
cnf(u2984,negated_conjecture,
c2_1(a136) ).
cnf(u2987,negated_conjecture,
~ c3_1(a136) ).
cnf(u3489,negated_conjecture,
~ c3_1(a146) ).
cnf(u4078,negated_conjecture,
~ c4_1(a142) ).
cnf(u4926,negated_conjecture,
c4_1(a95) ).
cnf(u4929,negated_conjecture,
~ c3_1(a95) ).
cnf(u4934,negated_conjecture,
~ c4_1(a105) ).
cnf(u5055,negated_conjecture,
~ c4_1(a135) ).
cnf(u5060,negated_conjecture,
c5_1(a135) ).
cnf(u5069,negated_conjecture,
c4_1(a143) ).
cnf(u3144,negated_conjecture,
c2_1(a116) ).
cnf(u3718,negated_conjecture,
~ c4_1(a102) ).
cnf(u3139,negated_conjecture,
c2_1(a133) ).
cnf(u3093,negated_conjecture,
c1_1(a154) ).
cnf(u4467,negated_conjecture,
c2_1(a101) ).
cnf(u4743,negated_conjecture,
c2_1(a100) ).
cnf(u4873,negated_conjecture,
c2_1(a89) ).
cnf(u3277,negated_conjecture,
( ~ c3_1(X0)
| c2_1(X0) ) ).
cnf(u4541,negated_conjecture,
c5_1(a87) ).
cnf(u4563,negated_conjecture,
~ c4_1(a87) ).
cnf(u2566,negated_conjecture,
( ~ c3_1(X0)
| c5_1(X0) ) ).
cnf(u3329,negated_conjecture,
c1_1(a79) ).
cnf(u4177,negated_conjecture,
c1_1(a125) ).
cnf(u5082,negated_conjecture,
c1_1(a95) ).
cnf(u3099,negated_conjecture,
c2_1(a153) ).
cnf(u3254,negated_conjecture,
~ c4_1(a141) ).
cnf(u4772,negated_conjecture,
~ c4_1(a115) ).
cnf(u3145,negated_conjecture,
c2_1(a108) ).
cnf(u3477,negated_conjecture,
~ c4_1(a154) ).
cnf(u4174,negated_conjecture,
c1_1(a156) ).
cnf(u4538,negated_conjecture,
~ c4_1(a124) ).
cnf(u4118,negated_conjecture,
( c0_1(X1)
| c1_1(X1) ) ).
cnf(u4764,negated_conjecture,
c1_1(a115) ).
cnf(u4321,negated_conjecture,
~ c4_1(a78) ).
cnf(u4531,negated_conjecture,
c2_1(a124) ).
cnf(u3030,negated_conjecture,
~ c4_1(a156) ).
cnf(u1992,negated_conjecture,
c5_1(a106) ).
cnf(u2035,negated_conjecture,
c1_1(a106) ).
cnf(u3440,negated_conjecture,
~ c4_1(a100) ).
cnf(u3434,negated_conjecture,
c5_1(a92) ).
cnf(u4533,negated_conjecture,
c1_1(a124) ).
cnf(u4874,negated_conjecture,
c5_1(a89) ).
cnf(u4371,negated_conjecture,
c2_1(a80) ).
cnf(u3608,negated_conjecture,
c2_1(a79) ).
cnf(u2005,negated_conjecture,
( c2_1(X1)
| c1_1(X1) ) ).
cnf(u3428,negated_conjecture,
c5_1(a154) ).
cnf(u3693,negated_conjecture,
c1_1(a102) ).
cnf(u3614,negated_conjecture,
c2_1(a99) ).
cnf(u4453,negated_conjecture,
( c5_1(X1)
| c2_1(X1) ) ).
cnf(u3190,negated_conjecture,
c1_1(a92) ).
cnf(u4465,negated_conjecture,
~ c4_1(a101) ).
cnf(u4370,negated_conjecture,
c2_1(a105) ).
cnf(u4138,negated_conjecture,
c2_1(a138) ).
cnf(u4175,negated_conjecture,
c1_1(a142) ).
cnf(u4366,negated_conjecture,
c2_1(a147) ).
cnf(u4741,negated_conjecture,
( ~ c0_1(X1)
| c2_1(X1) ) ).
cnf(u2152,negated_conjecture,
( ~ c4_1(X0)
| c2_1(X0) ) ).
cnf(u4880,negated_conjecture,
~ c4_1(a89) ).
cnf(u3225,negated_conjecture,
~ c4_1(a146) ).
cnf(u4952,negated_conjecture,
c2_1(a93) ).
cnf(u3235,negated_conjecture,
~ c4_1(a113) ).
cnf(u3140,negated_conjecture,
c2_1(a123) ).
cnf(u3923,negated_conjecture,
( ~ c4_1(X0)
| c1_1(X0) ) ).
cnf(u4179,negated_conjecture,
c1_1(a121) ).
cnf(u3276,negated_conjecture,
( ~ c4_1(X0)
| ~ c3_1(X0) ) ).
cnf(u3615,negated_conjecture,
c2_1(a92) ).
cnf(u2050,negated_conjecture,
( ~ c3_1(X0)
| c1_1(X0) ) ).
cnf(u5108,negated_conjecture,
c1_1(a143) ).
cnf(u3011,negated_conjecture,
( ~ c5_1(X1)
| ~ c4_1(X1) ) ).
cnf(u3426,negated_conjecture,
c5_1(a79) ).
cnf(u4768,negated_conjecture,
c1_1(a116) ).
cnf(u3146,negated_conjecture,
c2_1(a81) ).
cnf(u3925,negated_conjecture,
~ c4_1(a97) ).
cnf(u5099,negated_conjecture,
~ c4_1(a118) ).
cnf(u4137,negated_conjecture,
c2_1(a140) ).
cnf(u4140,negated_conjecture,
c2_1(a125) ).
cnf(u4537,negated_conjecture,
c1_1(a87) ).
cnf(u3692,negated_conjecture,
c5_1(a102) ).
cnf(u3427,negated_conjecture,
c5_1(a78) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN543-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n018.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 16:29:25 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.31/1.59 % (3521626)Input is clausal, will run a generic CNF schedule.
% 5.31/1.59 % (3521632)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3159807477:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.31/1.59 % (3521631)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=1446207682:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.31/1.59 % (3521636)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1445218230:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.31/1.59 % (3521634)lrs+10_1_sil=8000:sp=occurrence:random_seed=665683407:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.31/1.59 % (3521635)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3031538783:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.31/1.59 % (3521637)dis-21_1_sil=8000:lcm=predicate:random_seed=3010801009: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)
% 5.31/1.59 % (3521633)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3459893849:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.31/1.59 % (3521634)Instruction limit reached!
% 5.31/1.59 % (3521634)------------------------------
% 5.31/1.59 % (3521634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.59 % (3521634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.59 % (3521634)CaDiCaL version: 2.1.3
% 5.31/1.59 % (3521634)Termination reason: Instruction limit
% 5.31/1.59 % (3521634)Termination phase: Saturation
% 5.31/1.59 % (3521634)Time elapsed: 0.066 s
% 5.31/1.59 % (3521634)Peak memory usage: 90 MB
% 5.31/1.59 % (3521634)Instructions burned: 107 (million)
% 5.31/1.59 % (3521635)Refutation not found, incomplete strategy
% 5.31/1.59 % (3521635)------------------------------
% 5.31/1.59 % (3521635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.59 % (3521635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.59 % (3521635)CaDiCaL version: 2.1.3
% 5.31/1.59 % (3521635)Termination reason: Refutation not found, incomplete strategy
% 5.31/1.59 % (3521635)Time elapsed: 0.070 s
% 5.31/1.59 % (3521635)Peak memory usage: 90 MB
% 5.31/1.59 % (3521635)Instructions burned: 114 (million)
% 5.31/1.59 % (3521637)Instruction limit reached!
% 5.31/1.59 % (3521637)------------------------------
% 5.31/1.59 % (3521637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.59 % (3521637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.59 % (3521637)CaDiCaL version: 2.1.3
% 5.31/1.59 % (3521637)Termination reason: Instruction limit
% 5.31/1.59 % (3521637)Termination phase: Saturation
% 5.31/1.59 % (3521637)Time elapsed: 0.071 s
% 5.31/1.59 % (3521637)Peak memory usage: 90 MB
% 5.31/1.59 % (3521637)Instructions burned: 117 (million)
% 5.31/1.59 % (3521636)Instruction limit reached!
% 5.31/1.59 % (3521636)------------------------------
% 5.31/1.59 % (3521636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.59 % (3521636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.59 % (3521636)CaDiCaL version: 2.1.3
% 5.31/1.59 % (3521636)Termination reason: Instruction limit
% 5.31/1.59 % (3521636)Termination phase: Saturation
% 5.31/1.59 % (3521636)Time elapsed: 0.112 s
% 5.31/1.59 % (3521636)Peak memory usage: 91 MB
% 5.31/1.59 % (3521636)Instructions burned: 181 (million)
% 5.31/1.59 % (3521645)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=2343976549:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 5.31/1.59 % (3521646)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3852815438: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)
% 5.31/1.59 % (3521646)Refutation not found, incomplete strategy
% 5.31/1.59 % (3521646)------------------------------
% 5.31/1.59 % (3521646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.59 % (3521646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.59 % (3521646)CaDiCaL version: 2.1.3
% 5.31/1.59 % (3521646)Termination reason: Refutation not found, incomplete strategy
% 5.31/1.59 % (3521646)Time elapsed: 0.041 s
% 5.31/1.59 % (3521646)Peak memory usage: 90 MB
% 5.31/1.59 % (3521646)Instructions burned: 68 (million)
% 5.31/1.59 % (3521645)Refutation not found, incomplete strategy
% 5.31/1.59 % (3521645)------------------------------
% 5.31/1.59 % (3521645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.59 % (3521645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.59 % (3521645)CaDiCaL version: 2.1.3
% 5.31/1.59 % (3521645)Termination reason: Refutation not found, incomplete strategy
% 5.31/1.59 % (3521645)Time elapsed: 0.054 s
% 5.31/1.59 % (3521645)Peak memory usage: 90 MB
% 5.31/1.59 % (3521645)Instructions burned: 87 (million)
% 5.31/1.59 % (3521647)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2921029905:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.31/1.59 % (3521635)------------------------------
% 5.31/1.59 % (3521635)------------------------------
% 5.31/1.59 % (3521647)Refutation not found, incomplete strategy
% 5.31/1.59 % (3521647)------------------------------
% 5.31/1.59 % (3521647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.59 % (3521647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.59 % (3521647)CaDiCaL version: 2.1.3
% 5.31/1.59 % (3521647)Termination reason: Refutation not found, incomplete strategy
% 5.31/1.59 % (3521647)Time elapsed: 0.066 s
% 5.31/1.59 % (3521647)Peak memory usage: 90 MB
% 5.31/1.59 % (3521647)Instructions burned: 105 (million)
% 5.31/1.59 % (3521632)Refutation not found, incomplete strategy
% 5.31/1.59 % (3521632)------------------------------
% 5.31/1.59 % (3521632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.59 % (3521632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.59 % (3521632)CaDiCaL version: 2.1.3
% 5.31/1.59 % (3521632)Termination reason: Refutation not found, incomplete strategy
% 5.31/1.59 % (3521632)Time elapsed: 0.380 s
% 5.31/1.59 % (3521632)Peak memory usage: 129 MB
% 5.31/1.59 % (3521632)Instructions burned: 926 (million)
% 5.31/1.59 % (3521651)lrs+10_64_to=lpo:sil=8000:random_seed=3502844717:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 5.31/1.59 % (3521646)------------------------------
% 5.31/1.59 % (3521646)------------------------------
% 5.31/1.59 % (3521645)------------------------------
% 5.31/1.59 % (3521645)------------------------------
% 5.31/1.59 % (3521632)------------------------------
% 5.31/1.59 % (3521632)------------------------------
% 5.31/1.59 % (3521651)First to succeed.
% 5.31/1.59 % (3521651)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3521626"
% 5.31/1.59 % (3521647)------------------------------
% 5.31/1.59 % (3521647)------------------------------
% 5.31/1.59 % (3521654)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1818258698:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 5.31/1.59 % (3521653)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2483860969:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 5.31/1.59 % (3521655)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1117633968:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 5.31/1.59 % (3521631)Also succeeded, but the first one will report.
% 5.31/1.59 % (3521654)Also succeeded, but the first one will report.
% 5.31/1.59 % (3521653)Refutation not found, incomplete strategy
% 5.31/1.59 % (3521653)------------------------------
% 5.31/1.59 % (3521653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.59 % (3521653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.59 % (3521653)CaDiCaL version: 2.1.3
% 5.31/1.59 % (3521653)Termination reason: Refutation not found, incomplete strategy
% 5.31/1.59 % (3521653)Time elapsed: 0.068 s
% 5.31/1.59 % (3521653)Peak memory usage: 90 MB
% 5.31/1.59 % (3521653)Instructions burned: 105 (million)
% 5.31/1.59 % (3521656)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3977039614:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 5.31/1.59 % (3521656)Refutation not found, incomplete strategy
% 5.31/1.59 % (3521656)------------------------------
% 5.31/1.59 % (3521656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.59 % (3521656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.59 % (3521656)CaDiCaL version: 2.1.3
% 5.31/1.59 % (3521656)Termination reason: Refutation not found, incomplete strategy
% 5.31/1.59 % (3521656)Time elapsed: 0.019 s
% 5.31/1.59 % (3521656)Peak memory usage: 89 MB
% 5.31/1.59 % (3521656)Instructions burned: 31 (million)
% 5.31/1.59 % SZS status Satisfiable for theBenchmark
% 5.31/1.59 % SZS output start Saturation.
% See solution above
% 7.08/1.75 % SZS output start Definitions and Model Updates.
% 7.08/1.75 % SZS output end Definitions and Model Updates.
% 7.08/1.75 % (3521651)------------------------------
% 7.08/1.75 % (3521651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.08/1.75 % (3521651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.08/1.75 % (3521651)CaDiCaL version: 2.1.3
% 7.08/1.75 % (3521651)Termination reason: Satisfiable
% 7.08/1.75 % (3521651)Time elapsed: 0.055 s
% 7.08/1.75 % (3521651)Peak memory usage: 90 MB
% 7.08/1.75 % (3521651)Instructions burned: 84 (million)
% 7.08/1.75 % (3521651)------------------------------
% 7.08/1.75 % (3521651)------------------------------
% 7.08/1.75 % (3521626)Success in time 0.919 s
% 7.08/1.75 % Vampire exiting
%------------------------------------------------------------------------------