%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN542+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 : n002.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 : CounterSatisfiable 2.54s 1.01s
% Output : Saturation 0.21s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u328,negated_conjecture,
~ hskp44 ).
cnf(u333,negated_conjecture,
hskp48 ).
cnf(u336,negated_conjecture,
~ hskp47 ).
cnf(u342,negated_conjecture,
hskp9 ).
cnf(u345,negated_conjecture,
~ hskp46 ).
cnf(u349,negated_conjecture,
~ hskp17 ).
cnf(u354,negated_conjecture,
~ hskp45 ).
cnf(u359,negated_conjecture,
hskp34 ).
cnf(u362,negated_conjecture,
~ hskp33 ).
cnf(u367,negated_conjecture,
~ hskp43 ).
cnf(u372,negated_conjecture,
hskp42 ).
cnf(u377,negated_conjecture,
hskp7 ).
cnf(u380,negated_conjecture,
~ hskp58 ).
cnf(u384,negated_conjecture,
~ hskp57 ).
cnf(u390,negated_conjecture,
hskp41 ).
cnf(u393,negated_conjecture,
~ hskp40 ).
cnf(u397,negated_conjecture,
~ hskp56 ).
cnf(u402,negated_conjecture,
~ hskp39 ).
cnf(u406,negated_conjecture,
~ hskp20 ).
cnf(u410,negated_conjecture,
ndr1_0 ).
cnf(u414,negated_conjecture,
( ~ c3_1(X84)
| ~ c4_1(X84)
| ~ c2_1(X84) ) ).
cnf(u418,negated_conjecture,
~ hskp8 ).
cnf(u425,negated_conjecture,
( ~ c1_1(X82)
| ~ c5_1(X82)
| ~ c4_1(X82) ) ).
cnf(u429,negated_conjecture,
~ hskp55 ).
cnf(u433,negated_conjecture,
~ hskp37 ).
cnf(u437,negated_conjecture,
( ~ c1_1(X81)
| ~ c3_1(X81)
| ~ c2_1(X81) ) ).
cnf(u441,negated_conjecture,
~ hskp38 ).
cnf(u449,negated_conjecture,
~ hskp22 ).
cnf(u453,negated_conjecture,
( c5_1(X79)
| ~ c4_1(X79)
| ~ c1_1(X79) ) ).
cnf(u456,negated_conjecture,
( ~ c1_1(X78)
| c5_1(X78)
| ~ c0_1(X78) ) ).
cnf(u460,negated_conjecture,
( c4_1(X76)
| ~ c3_1(X76)
| ~ c1_1(X76) ) ).
cnf(u464,negated_conjecture,
~ hskp36 ).
cnf(u468,negated_conjecture,
~ hskp35 ).
cnf(u472,negated_conjecture,
( ~ c0_1(X75)
| ~ c2_1(X75)
| c4_1(X75) ) ).
cnf(u476,negated_conjecture,
~ hskp54 ).
cnf(u485,negated_conjecture,
~ hskp53 ).
cnf(u489,negated_conjecture,
( c4_1(X72)
| ~ c2_1(X72)
| ~ c1_1(X72) ) ).
cnf(u493,negated_conjecture,
~ hskp24 ).
cnf(u497,negated_conjecture,
~ hskp52 ).
cnf(u501,negated_conjecture,
( c3_1(X70)
| ~ c4_1(X70)
| ~ c1_1(X70) ) ).
cnf(u505,negated_conjecture,
~ hskp32 ).
cnf(u509,negated_conjecture,
~ hskp51 ).
cnf(u513,negated_conjecture,
( c3_1(X69)
| ~ c2_1(X69)
| c4_1(X69) ) ).
cnf(u518,negated_conjecture,
hskp0 ).
cnf(u521,negated_conjecture,
~ hskp27 ).
cnf(u525,negated_conjecture,
( ~ c0_1(X68)
| c3_1(X68)
| c4_1(X68) ) ).
cnf(u529,negated_conjecture,
~ hskp31 ).
cnf(u533,negated_conjecture,
( c3_1(X67)
| ~ c4_1(X67)
| c5_1(X67) ) ).
cnf(u540,negated_conjecture,
~ hskp30 ).
cnf(u544,negated_conjecture,
~ hskp29 ).
cnf(u548,negated_conjecture,
( ~ c1_1(X65)
| c2_1(X65)
| ~ c0_1(X65) ) ).
cnf(u552,negated_conjecture,
~ hskp28 ).
cnf(u556,negated_conjecture,
( ~ c0_1(X64)
| c2_1(X64)
| c4_1(X64) ) ).
cnf(u563,negated_conjecture,
( c4_1(X62)
| ~ c1_1(X62)
| c5_1(X62) ) ).
cnf(u567,negated_conjecture,
~ hskp26 ).
cnf(u571,negated_conjecture,
( c2_1(X60)
| ~ c4_1(X60)
| ~ c1_1(X60) ) ).
cnf(u578,negated_conjecture,
~ hskp25 ).
cnf(u582,negated_conjecture,
( ~ c3_1(X58)
| c2_1(X58)
| c4_1(X58) ) ).
cnf(u590,negated_conjecture,
~ hskp23 ).
cnf(u597,negated_conjecture,
( c1_1(X53)
| ~ c3_1(X53)
| ~ c2_1(X53) ) ).
cnf(u605,negated_conjecture,
~ hskp21 ).
cnf(u609,negated_conjecture,
( ~ c1_1(X50)
| ~ c5_1(X50)
| ~ c2_1(X50) ) ).
cnf(u612,negated_conjecture,
( ~ c0_1(X49)
| ~ c2_1(X49)
| c1_1(X49) ) ).
cnf(u622,negated_conjecture,
( c1_1(X46)
| ~ c4_1(X46)
| c5_1(X46) ) ).
cnf(u626,negated_conjecture,
( ~ c0_1(X44)
| c1_1(X44)
| c5_1(X44) ) ).
cnf(u630,negated_conjecture,
~ hskp19 ).
cnf(u638,negated_conjecture,
~ hskp18 ).
cnf(u642,negated_conjecture,
( ~ c0_1(X41)
| c1_1(X41)
| c4_1(X41) ) ).
cnf(u646,negated_conjecture,
~ hskp16 ).
cnf(u654,negated_conjecture,
~ hskp15 ).
cnf(u658,negated_conjecture,
~ hskp14 ).
cnf(u662,negated_conjecture,
( c1_1(X38)
| c4_1(X38)
| c3_1(X38) ) ).
cnf(u667,negated_conjecture,
hskp13 ).
cnf(u670,negated_conjecture,
~ hskp4 ).
cnf(u678,negated_conjecture,
~ hskp12 ).
cnf(u682,negated_conjecture,
( ~ c1_1(X36)
| ~ c4_1(X36)
| ~ c2_1(X36) ) ).
cnf(u694,negated_conjecture,
hskp11 ).
cnf(u697,negated_conjecture,
~ hskp10 ).
cnf(u709,negated_conjecture,
( ~ c3_1(X29)
| c0_1(X29)
| ~ c2_1(X29) ) ).
cnf(u713,negated_conjecture,
~ hskp6 ).
cnf(u724,negated_conjecture,
( c4_1(X26)
| ~ c0_1(X26)
| c5_1(X26) ) ).
cnf(u731,negated_conjecture,
( ~ c1_1(X24)
| c3_1(X24)
| ~ c0_1(X24) ) ).
cnf(u741,negated_conjecture,
~ hskp5 ).
cnf(u748,negated_conjecture,
( c0_1(X20)
| ~ c2_1(X20)
| c4_1(X20) ) ).
cnf(u752,negated_conjecture,
~ hskp3 ).
cnf(u756,negated_conjecture,
( c5_1(X19)
| c0_1(X19)
| c4_1(X19) ) ).
cnf(u760,negated_conjecture,
~ hskp2 ).
cnf(u768,negated_conjecture,
~ hskp50 ).
cnf(u772,negated_conjecture,
( c0_1(X16)
| ~ c4_1(X16)
| ~ c1_1(X16) ) ).
cnf(u779,negated_conjecture,
~ hskp1 ).
cnf(u783,negated_conjecture,
( ~ c5_1(X14)
| ~ c0_1(X14)
| ~ c2_1(X14) ) ).
cnf(u793,negated_conjecture,
( c0_1(X10)
| c5_1(X10)
| c2_1(X10) ) ).
cnf(u804,negated_conjecture,
~ hskp49 ).
cnf(u808,negated_conjecture,
( ~ c0_1(X6)
| ~ c5_1(X6)
| ~ c1_1(X6) ) ).
cnf(u825,negated_conjecture,
( c1_1(X0)
| c2_1(X0)
| c0_1(X0) ) ).
cnf(u829,negated_conjecture,
~ c3_1(a64) ).
cnf(u834,negated_conjecture,
~ c2_1(a64) ).
cnf(u839,negated_conjecture,
~ c1_1(a64) ).
cnf(u845,negated_conjecture,
~ c3_1(a63) ).
cnf(u850,negated_conjecture,
~ c2_1(a63) ).
cnf(u856,negated_conjecture,
c0_1(a63) ).
cnf(u861,negated_conjecture,
~ c2_1(a60) ).
cnf(u866,negated_conjecture,
~ c1_1(a60) ).
cnf(u872,negated_conjecture,
c0_1(a60) ).
cnf(u878,negated_conjecture,
c4_1(a56) ).
cnf(u883,negated_conjecture,
c3_1(a56) ).
cnf(u887,negated_conjecture,
~ c2_1(a56) ).
cnf(u894,negated_conjecture,
c4_1(a47) ).
cnf(u899,negated_conjecture,
c2_1(a47) ).
cnf(u903,negated_conjecture,
~ c1_1(a47) ).
cnf(u942,negated_conjecture,
c4_1(a40) ).
cnf(u946,negated_conjecture,
~ c2_1(a40) ).
cnf(u952,negated_conjecture,
c0_1(a40) ).
cnf(u958,negated_conjecture,
c5_1(a4) ).
cnf(u963,negated_conjecture,
c4_1(a4) ).
cnf(u967,negated_conjecture,
~ c2_1(a4) ).
cnf(u974,negated_conjecture,
c4_1(a2) ).
cnf(u978,negated_conjecture,
~ c1_1(a2) ).
cnf(u984,negated_conjecture,
c0_1(a2) ).
cnf(u990,negated_conjecture,
~ c3_1(a76) ).
cnf(u995,negated_conjecture,
~ c1_1(a76) ).
cnf(u1000,negated_conjecture,
c5_1(a76) ).
cnf(u1006,negated_conjecture,
~ c1_1(a75) ).
cnf(u1011,negated_conjecture,
c5_1(a75) ).
cnf(u1015,negated_conjecture,
~ c3_1(a75) ).
cnf(u1022,negated_conjecture,
~ c1_1(a73) ).
cnf(u1026,negated_conjecture,
c0_1(a73) ).
cnf(u1031,negated_conjecture,
~ c2_1(a73) ).
cnf(u1037,negated_conjecture,
c0_1(a71) ).
cnf(u1043,negated_conjecture,
c5_1(a71) ).
cnf(u1047,negated_conjecture,
~ c3_1(a71) ).
cnf(u1053,negated_conjecture,
c5_1(a68) ).
cnf(u1058,negated_conjecture,
c4_1(a68) ).
cnf(u1064,negated_conjecture,
~ c3_1(a68) ).
cnf(u1069,negated_conjecture,
c5_1(a67) ).
cnf(u1075,negated_conjecture,
~ c2_1(a67) ).
cnf(u1080,negated_conjecture,
c3_1(a67) ).
cnf(u1086,negated_conjecture,
~ c1_1(a66) ).
cnf(u1091,negated_conjecture,
c5_1(a66) ).
cnf(u1096,negated_conjecture,
c0_1(a66) ).
cnf(u1102,negated_conjecture,
~ c4_1(a62) ).
cnf(u1107,negated_conjecture,
c5_1(a62) ).
cnf(u1112,negated_conjecture,
c1_1(a62) ).
cnf(u1117,negated_conjecture,
c5_1(a61) ).
cnf(u1122,negated_conjecture,
c4_1(a61) ).
cnf(u1128,negated_conjecture,
c0_1(a61) ).
cnf(u1133,negated_conjecture,
c5_1(a59) ).
cnf(u1139,negated_conjecture,
~ c2_1(a59) ).
cnf(u1143,negated_conjecture,
c0_1(a59) ).
cnf(u1150,negated_conjecture,
~ c1_1(a54) ).
cnf(u1154,negated_conjecture,
c0_1(a54) ).
cnf(u1159,negated_conjecture,
~ c3_1(a54) ).
cnf(u1165,negated_conjecture,
c5_1(a51) ).
cnf(u1170,negated_conjecture,
~ c3_1(a51) ).
cnf(u1175,negated_conjecture,
~ c1_1(a51) ).
cnf(u1181,negated_conjecture,
c4_1(a50) ).
cnf(u1187,negated_conjecture,
~ c3_1(a50) ).
cnf(u1192,negated_conjecture,
~ c1_1(a50) ).
cnf(u1214,negated_conjecture,
~ c2_1(a46) ).
cnf(u1219,negated_conjecture,
c4_1(a46) ).
cnf(u1224,negated_conjecture,
c3_1(a46) ).
cnf(u1230,negated_conjecture,
~ c3_1(a45) ).
cnf(u1235,negated_conjecture,
~ c2_1(a45) ).
cnf(u1240,negated_conjecture,
c0_1(a45) ).
cnf(u1245,negated_conjecture,
c5_1(a41) ).
cnf(u1251,negated_conjecture,
~ c3_1(a41) ).
cnf(u1256,negated_conjecture,
~ c1_1(a41) ).
cnf(u1261,negated_conjecture,
c3_1(a37) ).
cnf(u1267,negated_conjecture,
~ c2_1(a37) ).
cnf(u1272,negated_conjecture,
~ c1_1(a37) ).
cnf(u1278,negated_conjecture,
~ c2_1(a36) ).
cnf(u1283,negated_conjecture,
c5_1(a36) ).
cnf(u1288,negated_conjecture,
c4_1(a36) ).
cnf(u1293,negated_conjecture,
c3_1(a35) ).
cnf(u1299,negated_conjecture,
c5_1(a35) ).
cnf(u1303,negated_conjecture,
~ c2_1(a35) ).
cnf(u1315,negated_conjecture,
~ c0_1(a34) ).
cnf(u1320,negated_conjecture,
c5_1(a34) ).
cnf(u1325,negated_conjecture,
c0_1(a33) ).
cnf(u1330,negated_conjecture,
~ c2_1(a33) ).
cnf(u1357,negated_conjecture,
c4_1(a31) ).
cnf(u1362,negated_conjecture,
~ c1_1(a31) ).
cnf(u1368,negated_conjecture,
c0_1(a31) ).
cnf(u1373,negated_conjecture,
c4_1(a30) ).
cnf(u1379,negated_conjecture,
~ c2_1(a30) ).
cnf(u1383,negated_conjecture,
c0_1(a30) ).
cnf(u1389,negated_conjecture,
c5_1(a29) ).
cnf(u1394,negated_conjecture,
c4_1(a29) ).
cnf(u1399,negated_conjecture,
~ c1_1(a29) ).
cnf(u1405,negated_conjecture,
c5_1(a28) ).
cnf(u1411,negated_conjecture,
~ c1_1(a28) ).
cnf(u1416,negated_conjecture,
c0_1(a28) ).
cnf(u1421,negated_conjecture,
c4_1(a27) ).
cnf(u1427,negated_conjecture,
~ c1_1(a27) ).
cnf(u1431,negated_conjecture,
c0_1(a27) ).
cnf(u1437,negated_conjecture,
c0_1(a26) ).
cnf(u1443,negated_conjecture,
c5_1(a26) ).
cnf(u1447,negated_conjecture,
~ c2_1(a26) ).
cnf(u1469,negated_conjecture,
c0_1(a24) ).
cnf(u1475,negated_conjecture,
c4_1(a24) ).
cnf(u1480,negated_conjecture,
c3_1(a24) ).
cnf(u1486,negated_conjecture,
~ c1_1(a23) ).
cnf(u1490,negated_conjecture,
~ c3_1(a23) ).
cnf(u1495,negated_conjecture,
~ c2_1(a23) ).
cnf(u1501,negated_conjecture,
c5_1(a22) ).
cnf(u1506,negated_conjecture,
c4_1(a22) ).
cnf(u1511,negated_conjecture,
c0_1(a22) ).
cnf(u1517,negated_conjecture,
c5_1(a21) ).
cnf(u1523,negated_conjecture,
~ c2_1(a21) ).
cnf(u1528,negated_conjecture,
c4_1(a21) ).
cnf(u1533,negated_conjecture,
c5_1(a20) ).
cnf(u1539,negated_conjecture,
~ c2_1(a20) ).
cnf(u1544,negated_conjecture,
c0_1(a20) ).
cnf(u1550,negated_conjecture,
~ c3_1(a19) ).
cnf(u1555,negated_conjecture,
~ c0_1(a19) ).
cnf(u1560,negated_conjecture,
c5_1(a19) ).
cnf(u1565,negated_conjecture,
c2_1(a17) ).
cnf(u1571,negated_conjecture,
~ c1_1(a17) ).
cnf(u1576,negated_conjecture,
~ c0_1(a17) ).
cnf(u1582,negated_conjecture,
~ c1_1(a15) ).
cnf(u1587,negated_conjecture,
c4_1(a15) ).
cnf(u1592,negated_conjecture,
c3_1(a15) ).
cnf(u1597,negated_conjecture,
c4_1(a14) ).
cnf(u1602,negated_conjecture,
~ c2_1(a14) ).
cnf(u1608,negated_conjecture,
c0_1(a14) ).
cnf(u1614,negated_conjecture,
~ c3_1(a12) ).
cnf(u1619,negated_conjecture,
~ c1_1(a12) ).
cnf(u1624,negated_conjecture,
c2_1(a12) ).
cnf(u1629,negated_conjecture,
c4_1(a11) ).
cnf(u1635,negated_conjecture,
c3_1(a11) ).
cnf(u1639,negated_conjecture,
~ c1_1(a11) ).
cnf(u1646,negated_conjecture,
~ c4_1(a10) ).
cnf(u1651,negated_conjecture,
~ c3_1(a10) ).
cnf(u1656,negated_conjecture,
~ c2_1(a10) ).
cnf(u1661,negated_conjecture,
c3_1(a9) ).
cnf(u1667,negated_conjecture,
~ c2_1(a9) ).
cnf(u1671,negated_conjecture,
~ c1_1(a9) ).
cnf(u1677,negated_conjecture,
c0_1(a8) ).
cnf(u1683,negated_conjecture,
c4_1(a8) ).
cnf(u1687,negated_conjecture,
~ c1_1(a8) ).
cnf(u1693,negated_conjecture,
c4_1(a7) ).
cnf(u1698,negated_conjecture,
c3_1(a7) ).
cnf(u1703,negated_conjecture,
~ c2_1(a7) ).
cnf(u1709,negated_conjecture,
c5_1(a6) ).
cnf(u1714,negated_conjecture,
~ c3_1(a6) ).
cnf(u1720,negated_conjecture,
c0_1(a6) ).
cnf(u1726,negated_conjecture,
~ c2_1(a5) ).
cnf(u1730,negated_conjecture,
c0_1(a5) ).
cnf(u1735,negated_conjecture,
~ c1_1(a5) ).
cnf(u1741,negated_conjecture,
c5_1(a3) ).
cnf(u1747,negated_conjecture,
~ c3_1(a3) ).
cnf(u1752,negated_conjecture,
~ c0_1(a3) ).
cnf(u1758,negated_conjecture,
~ c0_1(a1) ).
cnf(u1763,negated_conjecture,
c4_1(a1) ).
cnf(u1768,negated_conjecture,
c2_1(a1) ).
cnf(u1783,negated_conjecture,
~ c2_1(a71) ).
cnf(u1786,negated_conjecture,
c4_1(a71) ).
cnf(u1836,negated_conjecture,
~ c3_1(a62) ).
cnf(u1840,negated_conjecture,
~ c2_1(a62) ).
cnf(u1874,negated_conjecture,
c3_1(a73) ).
cnf(u1878,negated_conjecture,
c4_1(a73) ).
cnf(u1885,negated_conjecture,
~ c3_1(a17) ).
cnf(u1890,negated_conjecture,
c4_1(a17) ).
cnf(u1899,negated_conjecture,
~ c2_1(a50) ).
cnf(u1903,negated_conjecture,
c5_1(a50) ).
cnf(u1920,negated_conjecture,
~ c3_1(a47) ).
cnf(u1923,negated_conjecture,
~ c0_1(a47) ).
cnf(u1953,negated_conjecture,
c5_1(a73) ).
cnf(u1968,negated_conjecture,
c2_1(a51) ).
cnf(u1972,negated_conjecture,
c4_1(a51) ).
cnf(u1998,negated_conjecture,
c2_1(a29) ).
cnf(u2003,negated_conjecture,
~ c3_1(a29) ).
cnf(u2029,negated_conjecture,
c4_1(a60) ).
cnf(u2032,negated_conjecture,
~ c3_1(a60) ).
cnf(u2042,negated_conjecture,
c5_1(a23) ).
cnf(u2046,negated_conjecture,
c4_1(a23) ).
cnf(u2058,negated_conjecture,
~ c2_1(a11) ).
cnf(u2062,negated_conjecture,
c0_1(a11) ).
cnf(u2076,negated_conjecture,
c5_1(a17) ).
cnf(u2150,negated_conjecture,
c5_1(a63) ).
cnf(u2154,negated_conjecture,
c4_1(a63) ).
cnf(u2165,negated_conjecture,
c3_1(a4) ).
cnf(u2170,negated_conjecture,
c0_1(a4) ).
cnf(u2184,negated_conjecture,
c4_1(a28) ).
cnf(u2187,negated_conjecture,
~ c3_1(a28) ).
cnf(u2241,negated_conjecture,
c2_1(a41) ).
cnf(u2245,negated_conjecture,
c4_1(a41) ).
cnf(u2276,negated_conjecture,
c0_1(a56) ).
cnf(u2281,negated_conjecture,
c5_1(a56) ).
cnf(u2286,negated_conjecture,
c0_1(a46) ).
cnf(u2291,negated_conjecture,
c5_1(a46) ).
cnf(u2395,negated_conjecture,
~ c3_1(a36) ).
cnf(u2399,negated_conjecture,
c0_1(a36) ).
cnf(u2602,negated_conjecture,
c5_1(a64) ).
cnf(u2606,negated_conjecture,
c4_1(a64) ).
cnf(u2611,negated_conjecture,
c0_1(a64) ).
cnf(u2789,negated_conjecture,
~ c2_1(a61) ).
cnf(u2793,negated_conjecture,
~ c1_1(a61) ).
cnf(u2823,negated_conjecture,
~ c3_1(a21) ).
cnf(u2827,negated_conjecture,
c0_1(a21) ).
cnf(u2837,negated_conjecture,
c4_1(a20) ).
cnf(u2840,negated_conjecture,
~ c1_1(a20) ).
cnf(u2860,negated_conjecture,
c0_1(a50) ).
cnf(u2912,negated_conjecture,
c0_1(a23) ).
cnf(u2938,negated_conjecture,
c2_1(a76) ).
cnf(u2942,negated_conjecture,
~ c0_1(a76) ).
cnf(u2983,negated_conjecture,
~ c2_1(a68) ).
cnf(u2988,negated_conjecture,
c0_1(a68) ).
cnf(u2993,negated_conjecture,
~ c0_1(a41) ).
cnf(u3050,negated_conjecture,
~ c1_1(a71) ).
cnf(u3155,negated_conjecture,
c4_1(a35) ).
cnf(u3159,negated_conjecture,
c0_1(a35) ).
cnf(u3169,negated_conjecture,
c3_1(a33) ).
cnf(u3173,negated_conjecture,
c4_1(a33) ).
cnf(u3240,negated_conjecture,
~ c2_1(a54) ).
cnf(u3243,negated_conjecture,
c4_1(a54) ).
cnf(u3257,negated_conjecture,
c4_1(a45) ).
cnf(u3260,negated_conjecture,
~ c1_1(a45) ).
cnf(u3503,negated_conjecture,
~ c3_1(a66) ).
cnf(u3508,negated_conjecture,
c4_1(a66) ).
cnf(u3663,negated_conjecture,
~ c0_1(a75) ).
cnf(u3668,negated_conjecture,
c4_1(a75) ).
cnf(u3803,negated_conjecture,
c4_1(a76) ).
cnf(u3809,negated_conjecture,
~ c0_1(a62) ).
cnf(u3816,negated_conjecture,
~ c3_1(a20) ).
cnf(u3820,negated_conjecture,
c0_1(a67) ).
cnf(u3830,negated_conjecture,
c5_1(a12) ).
cnf(u3833,negated_conjecture,
~ c0_1(a12) ).
cnf(u3844,negated_conjecture,
c0_1(a9) ).
cnf(u3849,negated_conjecture,
c5_1(a7) ).
cnf(u3853,negated_conjecture,
c0_1(a7) ).
cnf(u3870,negated_conjecture,
c3_1(a2) ).
cnf(u4032,negated_conjecture,
c3_1(a8) ).
cnf(u4038,negated_conjecture,
c3_1(a27) ).
cnf(u4718,negated_conjecture,
~ c1_1(a63) ).
cnf(u5006,negated_conjecture,
c2_1(a75) ).
cnf(u5119,negated_conjecture,
~ c2_1(a15) ).
cnf(u5123,negated_conjecture,
c0_1(a15) ).
cnf(u5254,negated_conjecture,
~ c1_1(a6) ).
cnf(u5259,negated_conjecture,
~ c2_1(a6) ).
cnf(u5402,negated_conjecture,
~ c3_1(a34) ).
cnf(u5406,negated_conjecture,
~ c2_1(a34) ).
cnf(u5412,negated_conjecture,
c3_1(a22) ).
cnf(u5415,negated_conjecture,
~ c2_1(a22) ).
cnf(u5515,negated_conjecture,
c2_1(a19) ).
cnf(u5518,negated_conjecture,
~ c1_1(a19) ).
cnf(u5523,negated_conjecture,
~ c1_1(a7) ).
cnf(u5528,negated_conjecture,
~ c2_1(a3) ).
cnf(u5533,negated_conjecture,
c1_1(a3) ).
cnf(u5864,negated_conjecture,
~ c2_1(a24) ).
cnf(u5868,negated_conjecture,
~ c1_1(a24) ).
cnf(u6423,negated_conjecture,
~ c2_1(a2) ).
cnf(u4100,negated_conjecture,
c4_1(a6) ).
cnf(u4431,negated_conjecture,
c4_1(a37) ).
cnf(u4547,negated_conjecture,
c5_1(a54) ).
cnf(u5068,negated_conjecture,
c5_1(a40) ).
cnf(u6552,negated_conjecture,
c4_1(a5) ).
cnf(u3023,negated_conjecture,
c5_1(a2) ).
cnf(u3861,negated_conjecture,
( c5_1(X19)
| c0_1(X19) ) ).
cnf(u4118,negated_conjecture,
( ~ c3_1(X58)
| c4_1(X58) ) ).
cnf(u4429,negated_conjecture,
( c1_1(X38)
| c4_1(X38) ) ).
cnf(u2315,negated_conjecture,
( ~ c2_1(X75)
| c4_1(X75) ) ).
cnf(u5009,negated_conjecture,
( ~ c1_1(X6)
| ~ c0_1(X6) ) ).
cnf(u6780,negated_conjecture,
c4_1(a19) ).
cnf(u6680,negated_conjecture,
( ~ c3_1(X0)
| c0_1(X0) ) ).
cnf(u4034,negated_conjecture,
~ c2_1(a8) ).
cnf(u3513,negated_conjecture,
~ c2_1(a66) ).
cnf(u6534,negated_conjecture,
c4_1(a26) ).
cnf(u6621,negated_conjecture,
~ c2_1(a28) ).
cnf(u4465,negated_conjecture,
c5_1(X0) ).
cnf(u2521,negated_conjecture,
c5_1(a1) ).
cnf(u2487,negated_conjecture,
( ~ c4_1(X46)
| c5_1(X46) ) ).
cnf(u4549,negated_conjecture,
c5_1(a47) ).
cnf(u4933,negated_conjecture,
c4_1(a9) ).
cnf(u4712,negated_conjecture,
( ~ c3_1(X84)
| ~ c2_1(X84) ) ).
cnf(u2208,negated_conjecture,
( ~ c1_1(X79)
| ~ c4_1(X79) ) ).
cnf(u4542,negated_conjecture,
c5_1(a33) ).
cnf(u2297,negated_conjecture,
( ~ c1_1(X76)
| ~ c3_1(X76) ) ).
cnf(u4715,negated_conjecture,
~ c2_1(a31) ).
cnf(u6799,negated_conjecture,
~ c4_1(a3) ).
cnf(u6012,negated_conjecture,
( ~ c0_1(X49)
| ~ c2_1(X49) ) ).
cnf(u5092,negated_conjecture,
c5_1(a15) ).
cnf(u4541,negated_conjecture,
c5_1(a31) ).
cnf(u6515,negated_conjecture,
c4_1(a59) ).
cnf(u4440,negated_conjecture,
c4_1(a12) ).
cnf(u5752,negated_conjecture,
c0_1(a37) ).
cnf(u4535,negated_conjecture,
c5_1(a8) ).
cnf(u2316,negated_conjecture,
( ~ c1_1(X62)
| c5_1(X62) ) ).
cnf(u4924,negated_conjecture,
c4_1(a67) ).
cnf(u4141,negated_conjecture,
( ~ c1_1(X50)
| ~ c2_1(X50) ) ).
cnf(u4539,negated_conjecture,
c5_1(a27) ).
cnf(u1771,negated_conjecture,
( ~ c0_1(X64)
| c4_1(X64) ) ).
cnf(u4040,negated_conjecture,
~ c2_1(a27) ).
cnf(u5720,negated_conjecture,
( ~ c4_1(X0)
| c0_1(X0)
| c2_1(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN542+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.20 % Computer : n002.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 16:29:52 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 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
% 2.54/1.01 % (496553)Detected formulas, will run a generic FOF schedule.
% 2.54/1.01 % (496571)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3332541910:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.54/1.01 % (496574)dis-21_1_sil=8000:lcm=predicate:random_seed=2501281981:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.54/1.01 % (496570)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3153490072:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.54/1.01 % (496568)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2163984546:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.54/1.01 % (496567)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=645418656:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.54/1.01 % (496569)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=4286275445:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.54/1.01 % (496573)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=825022751:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.54/1.01 % (496573)Instruction limit reached!
% 2.54/1.01 % (496573)------------------------------
% 2.54/1.01 % (496573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.54/1.01 % (496573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.54/1.01 % (496573)CaDiCaL version: 2.1.3
% 2.54/1.01 % (496573)Termination reason: Instruction limit
% 2.54/1.01 % (496573)Termination phase: Saturation
% 2.54/1.01 % (496573)Time elapsed: 0.047 s
% 2.54/1.01 % (496573)Peak memory usage: 90 MB
% 2.54/1.01 % (496573)Instructions burned: 139 (million)
% 2.54/1.01 % (496571)Instruction limit reached!
% 2.54/1.01 % (496571)------------------------------
% 2.54/1.01 % (496571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.54/1.01 % (496571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.54/1.01 % (496571)CaDiCaL version: 2.1.3
% 2.54/1.01 % (496571)Termination reason: Instruction limit
% 2.54/1.01 % (496571)Termination phase: Saturation
% 2.54/1.01 % (496571)Time elapsed: 0.058 s
% 2.54/1.01 % (496571)Peak memory usage: 88 MB
% 2.54/1.01 % (496571)Instructions burned: 119 (million)
% 2.54/1.01 % (496570)Instruction limit reached!
% 2.54/1.01 % (496570)------------------------------
% 2.54/1.01 % (496570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.54/1.01 % (496570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.54/1.01 % (496570)CaDiCaL version: 2.1.3
% 2.54/1.01 % (496570)Termination reason: Instruction limit
% 2.54/1.01 % (496570)Termination phase: Saturation
% 2.54/1.01 % (496570)Time elapsed: 0.068 s
% 2.54/1.01 % (496570)Peak memory usage: 90 MB
% 2.54/1.01 % (496570)Instructions burned: 109 (million)
% 2.54/1.01 % (496574)Instruction limit reached!
% 2.54/1.01 % (496574)------------------------------
% 2.54/1.01 % (496574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.54/1.01 % (496574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.54/1.01 % (496574)CaDiCaL version: 2.1.3
% 2.54/1.01 % (496574)Termination reason: Instruction limit
% 2.54/1.01 % (496574)Termination phase: Saturation
% 2.54/1.01 % (496574)Time elapsed: 0.095 s
% 2.54/1.01 % (496574)Peak memory usage: 90 MB
% 2.54/1.01 % (496574)Instructions burned: 130 (million)
% 2.54/1.01 % (496638)lrs+10_1_sil=8000:sp=occurrence:random_seed=309678008:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 2.54/1.01 % (496645)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2055225362:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 2.54/1.01 % (496641)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3839369748:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 2.54/1.01 % (496638)First to succeed.
% 2.54/1.01 % (496638)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-496553"
% 2.54/1.01 % (496653)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3019492753:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 2.54/1.01 % (496641)Refutation not found, incomplete strategy
% 2.54/1.01 % (496641)------------------------------
% 2.54/1.01 % (496641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.54/1.01 % (496641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.54/1.01 % (496641)CaDiCaL version: 2.1.3
% 2.54/1.01 % (496641)Termination reason: Refutation not found, incomplete strategy
% 2.54/1.01 % (496641)Time elapsed: 0.060 s
% 2.54/1.01 % (496641)Peak memory usage: 91 MB
% 2.54/1.01 % (496641)Instructions burned: 92 (million)
% 2.54/1.01 % (496653)Refutation not found, incomplete strategy
% 2.54/1.01 % (496653)------------------------------
% 2.54/1.01 % (496653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.54/1.01 % (496653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.54/1.01 % (496653)CaDiCaL version: 2.1.3
% 2.54/1.01 % (496653)Termination reason: Refutation not found, incomplete strategy
% 2.54/1.01 % (496653)Time elapsed: 0.101 s
% 2.54/1.01 % (496653)Peak memory usage: 92 MB
% 2.54/1.01 % (496653)Instructions burned: 158 (million)
% 2.54/1.01 % SZS status CounterSatisfiable for theBenchmark
% 2.54/1.01 % SZS output start Saturation.
% See solution above
% 0.21/1.20 % SZS output start Definitions and Model Updates.
% 0.21/1.20 % SZS output end Definitions and Model Updates.
% 0.21/1.20 % (496638)------------------------------
% 0.21/1.20 % (496638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.21/1.20 % (496638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/1.20 % (496638)CaDiCaL version: 2.1.3
% 0.21/1.20 % (496638)Termination reason: Satisfiable
% 0.21/1.20 % (496638)Time elapsed: 0.052 s
% 0.21/1.20 % (496638)Peak memory usage: 91 MB
% 0.21/1.20 % (496638)Instructions burned: 144 (million)
% 0.21/1.20 % (496638)------------------------------
% 0.21/1.20 % (496638)------------------------------
% 0.21/1.20 % (496553)Success in time 0.559 s
% 0.21/1.20 % Vampire exiting
%------------------------------------------------------------------------------