%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN546-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 : 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:55 PM UTC 2026
% Result : Satisfiable 3.90s 1.29s
% Output : Saturation 4.93s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u535,negated_conjecture,
( ~ c7_2(X3,X5)
| c2_2(X3,X5)
| c4_2(X3,X5)
| c5_2(X3,X4)
| c7_2(X3,X4)
| ~ c7_1(X3)
| ~ c3_2(X3,X4)
| ~ ndr1_1(X3) ) ).
cnf(u538,negated_conjecture,
ndr1_0 ).
cnf(u568,negated_conjecture,
~ c5_0 ).
cnf(u574,negated_conjecture,
( ~ c7_2(X0,X2)
| c8_1(X0)
| c8_2(X0,X1)
| c1_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c3_2(X0,X2)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u587,negated_conjecture,
c3_0 ).
cnf(u604,negated_conjecture,
( ~ c1_1(X2)
| c4_1(X2)
| ~ c2_1(X2) ) ).
cnf(u624,negated_conjecture,
c6_0 ).
cnf(u634,negated_conjecture,
( ~ c7_2(X0,X1)
| c2_1(X0)
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u638,negated_conjecture,
( ~ c5_2(X2,X3)
| c8_1(X2)
| c5_1(X2)
| c7_2(X2,X3)
| ~ ndr1_1(X2) ) ).
cnf(u652,negated_conjecture,
( ~ c8_2(X0,X1)
| c7_2(X0,X1)
| c5_2(X0,X1)
| ~ c5_1(X0)
| ~ c6_2(X0,X2)
| ~ c1_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u665,negated_conjecture,
( ~ c7_2(X0,X1)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ c7_1(X0)
| ~ c8_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u714,negated_conjecture,
c2_0 ).
cnf(u718,negated_conjecture,
( ~ c1_2(X0,a427)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c5_2(X0,X2)
| c3_2(X0,X2)
| c1_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u741,negated_conjecture,
~ ndr1_1(a431) ).
cnf(u752,negated_conjecture,
( ~ c8_2(X0,X2)
| c2_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X1)
| ~ c5_1(X0)
| ~ c8_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u756,negated_conjecture,
c4_0 ).
cnf(u760,negated_conjecture,
( ~ c7_2(X0,a319)
| c6_2(X0,X2)
| c8_2(X0,X2)
| c5_2(X0,X1)
| c1_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u769,negated_conjecture,
( ~ c1_2(X0,X1)
| c8_2(X0,a427)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c5_2(X0,X2)
| c3_2(X0,X2)
| c1_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u773,negated_conjecture,
( ~ c7_2(X0,X3)
| c4_2(X0,X3)
| c3_2(X0,X2)
| c8_2(X0,X1)
| c3_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u797,negated_conjecture,
( ~ c2_2(X0,X1)
| c4_2(X0,a319)
| c6_2(X0,X2)
| c8_2(X0,X2)
| c5_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u801,negated_conjecture,
( ~ c2_2(X0,X1)
| c5_2(X0,a319)
| c6_2(X0,X2)
| c8_2(X0,X2)
| c5_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u827,negated_conjecture,
~ ssSkC3 ).
cnf(u834,negated_conjecture,
( ~ c2_1(X0)
| c1_1(X0)
| c3_1(X0) ) ).
cnf(u837,negated_conjecture,
ssSkC8 ).
cnf(u842,negated_conjecture,
~ c7_0 ).
cnf(u846,negated_conjecture,
( ~ c5_2(X0,X1)
| c4_1(X0)
| c7_2(X0,X1)
| ~ c3_2(X0,a310)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u851,negated_conjecture,
( ~ c2_2(X0,X1)
| ~ c1_1(X0)
| ~ c6_2(X0,a401)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u855,negated_conjecture,
( ~ c7_2(X0,a401)
| ~ c1_1(X0)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u859,negated_conjecture,
( ~ c2_2(X0,a401)
| ~ c1_1(X0)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u875,negated_conjecture,
( ~ c5_2(X0,X1)
| c4_1(X0)
| c6_2(X0,a310)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u879,negated_conjecture,
( ~ c5_2(X0,X1)
| c4_1(X0)
| c7_2(X0,a310)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u887,negated_conjecture,
~ ssSkC16 ).
cnf(u890,negated_conjecture,
ssSkC15 ).
cnf(u896,negated_conjecture,
~ c8_2(a405,a406) ).
cnf(u904,negated_conjecture,
~ c6_2(a405,a407) ).
cnf(u909,negated_conjecture,
~ c5_2(a405,a407) ).
cnf(u913,negated_conjecture,
( ~ c5_2(X0,X1)
| c6_1(X0)
| c1_2(X0,X1)
| ~ c1_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u917,negated_conjecture,
( ~ c7_2(X0,a437)
| c6_1(X0)
| c1_2(X0,X1)
| ~ c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u921,negated_conjecture,
~ ssSkC6 ).
cnf(u925,negated_conjecture,
( ~ c7_2(X0,a333)
| c4_1(X0)
| c8_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u930,negated_conjecture,
ssSkC18 ).
cnf(u942,negated_conjecture,
~ c8_0 ).
cnf(u945,negated_conjecture,
( ~ c8_2(X0,X1)
| c3_2(X0,X1)
| ~ c1_2(X0,a318)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u948,negated_conjecture,
ssSkC2 ).
cnf(u953,negated_conjecture,
( ~ c2_2(X0,a318)
| c3_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u970,negated_conjecture,
c2_2(a405,a406) ).
cnf(u975,negated_conjecture,
c7_2(a405,a406) ).
cnf(u979,negated_conjecture,
ndr1_1(a410) ).
cnf(u983,negated_conjecture,
( ~ c2_2(a410,X1)
| ~ c1_2(a410,X1) ) ).
cnf(u991,negated_conjecture,
~ c2_1(a431) ).
cnf(u996,negated_conjecture,
~ c1_1(a431) ).
cnf(u1000,negated_conjecture,
( ~ c5_2(X0,X1)
| c4_1(X0)
| c6_2(X0,a333)
| c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1004,negated_conjecture,
( ~ c5_2(X0,X1)
| c4_1(X0)
| c2_2(X0,a333)
| c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1008,negated_conjecture,
~ ssSkC14 ).
cnf(u1012,negated_conjecture,
( ~ c8_2(X0,a360)
| c4_2(X0,X1)
| c7_2(X0,X1)
| ~ ssSkP1(X0)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1016,negated_conjecture,
( ~ c1_2(X0,X1)
| c4_2(X0,X1)
| c7_2(X0,X1)
| ~ c4_2(X0,a360)
| ~ ndr1_1(X0)
| ~ ssSkP1(X0) ) ).
cnf(u1020,negated_conjecture,
( ~ c5_2(X0,a360)
| c4_2(X0,X1)
| c7_2(X0,X1)
| ~ ssSkP1(X0)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1032,negated_conjecture,
( ~ c8_2(X0,X1)
| c7_2(X0,a318)
| c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1040,negated_conjecture,
~ c1_0 ).
cnf(u1044,negated_conjecture,
( ~ c4_2(X0,a392)
| c8_2(X0,X1)
| ~ c3_1(X0)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1047,negated_conjecture,
ssSkC21 ).
cnf(u1053,negated_conjecture,
c6_1(a405) ).
cnf(u1058,negated_conjecture,
ndr1_1(a405) ).
cnf(u1066,negated_conjecture,
ndr1_1(a374) ).
cnf(u1070,negated_conjecture,
( ~ c5_2(a374,X0)
| c8_2(a374,X0)
| ~ c1_2(a374,X0) ) ).
cnf(u1074,negated_conjecture,
ndr1_1(a376) ).
cnf(u1078,negated_conjecture,
( ~ c5_2(a376,X0)
| c1_2(a376,X0)
| ~ c8_2(a376,X0) ) ).
cnf(u1082,negated_conjecture,
( ~ c4_2(X0,X1)
| c2_2(X0,a392)
| c8_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1102,negated_conjecture,
( ~ c7_2(X0,X1)
| c4_2(X0,a320)
| c4_2(X0,X1)
| ~ c6_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1106,negated_conjecture,
( ~ c7_2(X0,X1)
| c3_2(X0,a320)
| c4_2(X0,X1)
| ~ c6_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1110,negated_conjecture,
( ~ c7_2(X0,X1)
| c1_2(X0,a320)
| c4_2(X0,X1)
| ~ c6_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1114,negated_conjecture,
~ ssSkC23 ).
cnf(u1118,negated_conjecture,
( ~ ssSkP3(X0)
| c8_2(X0,a412)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c7_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1122,negated_conjecture,
( ~ ssSkP3(X0)
| c6_2(X0,a412)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c7_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1126,negated_conjecture,
( ~ ssSkP3(X0)
| c2_2(X0,a412)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c7_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1130,negated_conjecture,
( ~ c1_1(X1)
| c8_1(X1)
| c4_1(X1) ) ).
cnf(u1145,negated_conjecture,
ndr1_1(a305) ).
cnf(u1149,negated_conjecture,
( ~ c8_2(a305,X0)
| c4_2(a305,X0)
| ~ c6_2(a305,X0) ) ).
cnf(u1160,negated_conjecture,
ssSkC4 ).
cnf(u1165,negated_conjecture,
( ~ c5_2(a374,X0)
| c4_2(a374,X0)
| c2_2(a374,X0) ) ).
cnf(u1169,negated_conjecture,
( ~ c1_2(a376,X0)
| c3_2(a376,X0)
| c4_2(a376,X0) ) ).
cnf(u1189,negated_conjecture,
~ ssSkC1 ).
cnf(u1194,negated_conjecture,
~ ndr1_1(a315) ).
cnf(u1213,negated_conjecture,
~ ssSkC10 ).
cnf(u1218,negated_conjecture,
~ ndr1_1(a371) ).
cnf(u1233,negated_conjecture,
( c7_1(X1)
| c5_1(X1) ) ).
cnf(u1241,negated_conjecture,
~ ndr1_1(a453) ).
cnf(u1261,negated_conjecture,
~ ndr1_1(a350) ).
cnf(u1269,negated_conjecture,
~ ndr1_1(a351) ).
cnf(u1277,negated_conjecture,
ssSkC13 ).
cnf(u1292,negated_conjecture,
( c3_2(a369,X0)
| c4_2(a369,X0)
| c1_2(a369,X0) ) ).
cnf(u1295,negated_conjecture,
ndr1_1(a369) ).
cnf(u1299,negated_conjecture,
ssSkC17 ).
cnf(u1312,negated_conjecture,
ndr1_1(a442) ).
cnf(u1316,negated_conjecture,
( ~ c7_2(a442,X0)
| c6_2(a442,X0)
| c8_2(a442,X0) ) ).
cnf(u1319,negated_conjecture,
ssSkC27 ).
cnf(u1323,negated_conjecture,
ssSkC26 ).
cnf(u1328,negated_conjecture,
~ ssSkC0 ).
cnf(u1332,negated_conjecture,
ndr1_1(a300) ).
cnf(u1336,negated_conjecture,
( ~ c2_2(a300,X0)
| c6_2(a300,X0)
| c1_2(a300,X0) ) ).
cnf(u1345,negated_conjecture,
~ ndr1_1(a366) ).
cnf(u1352,negated_conjecture,
ndr1_1(a311) ).
cnf(u1356,negated_conjecture,
( ~ c7_2(a311,X0)
| ~ c8_2(a311,X0) ) ).
cnf(u1369,negated_conjecture,
~ ndr1_1(a309) ).
cnf(u1372,negated_conjecture,
( ~ c2_2(a309,X0)
| c6_2(a309,X0)
| c3_2(a309,X0) ) ).
cnf(u1394,negated_conjecture,
~ ssSkC19 ).
cnf(u1398,negated_conjecture,
ndr1_1(a402) ).
cnf(u1402,negated_conjecture,
( ~ c6_2(a402,X0)
| c2_2(a402,X0)
| c8_2(a402,X0) ) ).
cnf(u1460,negated_conjecture,
~ c6_1(a410) ).
cnf(u1465,negated_conjecture,
ssSkC7 ).
cnf(u1468,negated_conjecture,
( ~ c7_2(X0,a337)
| c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u1472,negated_conjecture,
( ~ c5_2(X0,a378)
| c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u1476,negated_conjecture,
( ~ c2_2(X0,a378)
| c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u1489,negated_conjecture,
ssSkC25 ).
cnf(u1492,negated_conjecture,
( ~ c1_2(X0,a434)
| c7_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1496,negated_conjecture,
( ~ c6_2(X0,a434)
| c7_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1504,negated_conjecture,
~ ssSkC28 ).
cnf(u1508,negated_conjecture,
( ~ c8_1(X0)
| c4_2(X0,a444)
| ~ c4_1(X0) ) ).
cnf(u1512,negated_conjecture,
( ~ c8_1(X0)
| c2_2(X0,a444)
| ~ c4_1(X0) ) ).
cnf(u1516,negated_conjecture,
( ~ c8_1(X0)
| c7_2(X0,a444)
| ~ c4_1(X0) ) ).
cnf(u1525,negated_conjecture,
~ ndr1_1(a400) ).
cnf(u1531,negated_conjecture,
ssSkC22 ).
cnf(u1537,negated_conjecture,
ssSkC12 ).
cnf(u1549,negated_conjecture,
ssSkC20 ).
cnf(u1553,negated_conjecture,
( ~ c8_2(X0,a390)
| ~ c2_1(X0)
| ~ ssSkP2(X0) ) ).
cnf(u1557,negated_conjecture,
( ~ c7_2(X0,a390)
| ~ c2_1(X0)
| ~ ssSkP2(X0) ) ).
cnf(u1561,negated_conjecture,
( ~ c6_2(X0,a404)
| c8_1(X0)
| c2_1(X0) ) ).
cnf(u1570,negated_conjecture,
c1_1(a410) ).
cnf(u1582,negated_conjecture,
( ~ c2_1(X0)
| c3_1(X0)
| c6_2(X0,a378) ) ).
cnf(u1590,negated_conjecture,
( ~ c8_1(X0)
| ndr1_1(X0)
| ~ c4_1(X0) ) ).
cnf(u1658,negated_conjecture,
( ~ ssSkP2(X0)
| c3_2(X0,a390)
| ~ c2_1(X0) ) ).
cnf(u1666,negated_conjecture,
( ~ c2_1(X0)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u1679,negated_conjecture,
( ~ c8_2(X0,a368)
| c6_1(X0) ) ).
cnf(u1687,negated_conjecture,
( ~ ssSkP2(X0)
| ndr1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u1691,negated_conjecture,
( c8_1(X0)
| ndr1_1(X0)
| c2_1(X0) ) ).
cnf(u1700,negated_conjecture,
~ c6_2(a374,a375) ).
cnf(u1705,negated_conjecture,
~ c7_2(a374,a375) ).
cnf(u1710,negated_conjecture,
~ c6_2(a376,a377) ).
cnf(u1715,negated_conjecture,
~ c5_2(a376,a377) ).
cnf(u1720,negated_conjecture,
~ c1_2(a414,a415) ).
cnf(u1725,negated_conjecture,
~ c7_2(a414,a415) ).
cnf(u1731,negated_conjecture,
~ c6_2(a417,a418) ).
cnf(u1736,negated_conjecture,
~ c3_2(a417,a418) ).
cnf(u1744,negated_conjecture,
( c6_1(X0)
| c4_2(X0,a368) ) ).
cnf(u1749,negated_conjecture,
~ c3_1(a298) ).
cnf(u1754,negated_conjecture,
~ c1_1(a298) ).
cnf(u1759,negated_conjecture,
~ c3_2(a305,a306) ).
cnf(u1764,negated_conjecture,
~ c5_2(a311,a312) ).
cnf(u1769,negated_conjecture,
~ c4_2(a311,a312) ).
cnf(u1774,negated_conjecture,
~ c5_2(a311,a313) ).
cnf(u1779,negated_conjecture,
~ c4_2(a311,a313) ).
cnf(u1784,negated_conjecture,
~ c7_2(a311,a313) ).
cnf(u1789,negated_conjecture,
~ c1_2(a330,a331) ).
cnf(u1792,negated_conjecture,
ssSkC5 ).
cnf(u1798,negated_conjecture,
~ c5_2(a330,a331) ).
cnf(u1803,negated_conjecture,
~ c5_2(a330,a332) ).
cnf(u1808,negated_conjecture,
~ c2_2(a330,a332) ).
cnf(u1813,negated_conjecture,
~ c8_2(a330,a332) ).
cnf(u1828,negated_conjecture,
~ c4_2(a347,a348) ).
cnf(u1832,negated_conjecture,
~ ssSkC9 ).
cnf(u1837,negated_conjecture,
~ c6_2(a355,a356) ).
cnf(u1842,negated_conjecture,
~ c8_2(a369,a370) ).
cnf(u1847,negated_conjecture,
~ c5_2(a369,a370) ).
cnf(u1852,negated_conjecture,
~ c4_2(a369,a370) ).
cnf(u1856,negated_conjecture,
~ c5_2(a374,a375) ).
cnf(u1862,negated_conjecture,
c3_2(a376,a377) ).
cnf(u1867,negated_conjecture,
~ c6_2(a385,a386) ).
cnf(u1872,negated_conjecture,
~ c3_2(a385,a386) ).
cnf(u1877,negated_conjecture,
~ c8_2(a385,a386) ).
cnf(u1897,negated_conjecture,
~ c6_1(a414) ).
cnf(u1902,negated_conjecture,
c2_2(a414,a415) ).
cnf(u1907,negated_conjecture,
~ c1_2(a425,a426) ).
cnf(u1910,negated_conjecture,
ssSkC24 ).
cnf(u1961,negated_conjecture,
~ c2_2(a454,a455) ).
cnf(u1972,negated_conjecture,
c8_1(a298) ).
cnf(u1977,negated_conjecture,
~ c5_1(a305) ).
cnf(u1982,negated_conjecture,
c8_2(a305,a306) ).
cnf(u1987,negated_conjecture,
c2_2(a305,a306) ).
cnf(u1997,negated_conjecture,
c1_2(a311,a312) ).
cnf(u2002,negated_conjecture,
~ c8_1(a314) ).
cnf(u2007,negated_conjecture,
~ c1_1(a314) ).
cnf(u2012,negated_conjecture,
~ c6_1(a330) ).
cnf(u2017,negated_conjecture,
c6_2(a330,a331) ).
cnf(u2052,negated_conjecture,
c3_2(a347,a348) ).
cnf(u2056,negated_conjecture,
~ c2_2(a347,a348) ).
cnf(u2062,negated_conjecture,
~ c8_1(a349) ).
cnf(u2067,negated_conjecture,
~ c5_1(a349) ).
cnf(u2072,negated_conjecture,
~ c3_1(a349) ).
cnf(u2082,negated_conjecture,
~ c2_1(a355) ).
cnf(u2087,negated_conjecture,
c8_2(a355,a356) ).
cnf(u2092,negated_conjecture,
c1_2(a355,a356) ).
cnf(u2099,negated_conjecture,
~ c1_2(a380,a381) ).
cnf(u2104,negated_conjecture,
~ c8_2(a380,a381) ).
cnf(u2109,negated_conjecture,
~ c1_2(a380,a382) ).
cnf(u2114,negated_conjecture,
~ c6_2(a380,a382) ).
cnf(u2119,negated_conjecture,
~ c8_2(a380,a383) ).
cnf(u2154,negated_conjecture,
c5_1(a414) ).
cnf(u2159,negated_conjecture,
ndr1_1(a414) ).
cnf(u2164,negated_conjecture,
c5_1(a417) ).
cnf(u2169,negated_conjecture,
c4_1(a417) ).
cnf(u2174,negated_conjecture,
ndr1_1(a417) ).
cnf(u2179,negated_conjecture,
~ c4_1(a425) ).
cnf(u2184,negated_conjecture,
c4_2(a425,a426) ).
cnf(u2189,negated_conjecture,
c3_2(a425,a426) ).
cnf(u2224,negated_conjecture,
~ c1_1(a454) ).
cnf(u2229,negated_conjecture,
~ c2_1(a454) ).
cnf(u2234,negated_conjecture,
c4_2(a454,a455) ).
cnf(u2239,negated_conjecture,
c8_2(a454,a455) ).
cnf(u2244,negated_conjecture,
~ c2_2(a300,a301) ).
cnf(u2249,negated_conjecture,
~ c1_2(a300,a301) ).
cnf(u2274,negated_conjecture,
~ c1_2(a345,a346) ).
cnf(u2356,negated_conjecture,
c6_1(a314) ).
cnf(u2366,negated_conjecture,
ndr1_1(a330) ).
cnf(u2376,negated_conjecture,
c8_1(a347) ).
cnf(u2381,negated_conjecture,
c4_1(a347) ).
cnf(u2386,negated_conjecture,
ndr1_1(a347) ).
cnf(u2401,negated_conjecture,
c6_1(a355) ).
cnf(u2406,negated_conjecture,
ndr1_1(a355) ).
cnf(u2411,negated_conjecture,
c2_1(a369) ).
cnf(u2423,negated_conjecture,
c2_2(a380,a381) ).
cnf(u2428,negated_conjecture,
c3_2(a380,a382) ).
cnf(u2433,negated_conjecture,
c1_2(a380,a383) ).
cnf(u2438,negated_conjecture,
c6_2(a380,a383) ).
cnf(u2443,negated_conjecture,
c2_1(a385) ).
cnf(u2448,negated_conjecture,
c5_1(a385) ).
cnf(u2453,negated_conjecture,
ndr1_1(a385) ).
cnf(u2459,negated_conjecture,
~ c4_2(a402,a403) ).
cnf(u2482,negated_conjecture,
c3_1(a425) ).
cnf(u2487,negated_conjecture,
ndr1_1(a425) ).
cnf(u2502,negated_conjecture,
~ c2_1(a442) ).
cnf(u2507,negated_conjecture,
~ c8_1(a442) ).
cnf(u2522,negated_conjecture,
ndr1_1(a454) ).
cnf(u2527,negated_conjecture,
c5_2(a300,a301) ).
cnf(u2532,negated_conjecture,
~ c2_1(a315) ).
cnf(u2537,negated_conjecture,
~ c4_1(a315) ).
cnf(u2572,negated_conjecture,
c2_2(a345,a346) ).
cnf(u2577,negated_conjecture,
c5_2(a345,a346) ).
cnf(u2676,negated_conjecture,
~ c7_1(a309) ).
cnf(u2694,negated_conjecture,
c1_1(a338) ).
cnf(u2708,negated_conjecture,
c3_1(a371) ).
cnf(u2733,negated_conjecture,
ndr1_1(a380) ).
cnf(u2744,negated_conjecture,
c5_1(a400) ).
cnf(u2749,negated_conjecture,
c7_1(a400) ).
cnf(u2754,negated_conjecture,
~ c7_1(a402) ).
cnf(u2759,negated_conjecture,
c3_2(a402,a403) ).
cnf(u2764,negated_conjecture,
c6_2(a402,a403) ).
cnf(u2783,negated_conjecture,
c3_1(a453) ).
cnf(u2788,negated_conjecture,
c2_1(a300) ).
cnf(u2820,negated_conjecture,
c6_1(a345) ).
cnf(u2825,negated_conjecture,
c2_1(a345) ).
cnf(u2830,negated_conjecture,
ndr1_1(a345) ).
cnf(u2901,negated_conjecture,
c3_1(a309) ).
cnf(u2952,negated_conjecture,
~ c3_1(a417) ).
cnf(u2961,negated_conjecture,
~ c3_1(a414) ).
cnf(u2983,negated_conjecture,
c3_1(a300) ).
cnf(u3001,negated_conjecture,
~ c5_1(a355) ).
cnf(u3012,negated_conjecture,
~ c2_1(a410) ).
cnf(u3015,negated_conjecture,
~ c4_1(a410) ).
cnf(u3037,negated_conjecture,
~ c2_1(a338) ).
cnf(u3040,negated_conjecture,
~ c4_1(a338) ).
cnf(u3075,negated_conjecture,
~ c3_1(a400) ).
cnf(u3094,negated_conjecture,
~ c3_1(a402) ).
cnf(u3107,negated_conjecture,
c8_1(a338) ).
cnf(u3112,negated_conjecture,
c8_1(a410) ).
cnf(u3123,negated_conjecture,
~ c4_1(a298) ).
cnf(u3166,negated_conjecture,
c6_2(a385,a378) ).
cnf(u3170,negated_conjecture,
c3_1(a385) ).
cnf(u3175,negated_conjecture,
c6_2(a300,a378) ).
cnf(u3183,negated_conjecture,
c7_2(a309,a389) ).
cnf(u3192,negated_conjecture,
c7_2(a385,a389) ).
cnf(u3196,negated_conjecture,
c3_2(a385,a390) ).
cnf(u3201,negated_conjecture,
c7_2(a300,a389) ).
cnf(u3205,negated_conjecture,
c3_2(a300,a390) ).
cnf(u3212,negated_conjecture,
~ c2_2(a309,a389) ).
cnf(u3217,negated_conjecture,
~ c2_2(a385,a389) ).
cnf(u3229,negated_conjecture,
~ c1_2(a374,a375) ).
cnf(u3239,negated_conjecture,
~ c6_2(a305,a306) ).
cnf(u3263,negated_conjecture,
c6_2(a309,a389) ).
cnf(u3272,negated_conjecture,
~ c2_1(a309) ).
cnf(u3278,negated_conjecture,
c8_2(a402,a403) ).
cnf(u3302,negated_conjecture,
c6_1(a385) ).
cnf(u3328,negated_conjecture,
c6_1(a300) ).
cnf(u3332,negated_conjecture,
~ c4_2(a309,a389) ).
cnf(u3341,negated_conjecture,
c6_1(a309) ).
cnf(u3347,negated_conjecture,
c4_2(a330,a331) ).
cnf(u3370,negated_conjecture,
c6_2(a369,a378) ).
cnf(u3374,negated_conjecture,
c3_1(a369) ).
cnf(u3383,negated_conjecture,
c3_2(a369,a390) ).
cnf(u3397,negated_conjecture,
ssSkP0(a369) ).
cnf(u3411,negated_conjecture,
c7_1(a369) ).
cnf(u3425,negated_conjecture,
~ c5_1(a300) ).
cnf(u3430,negated_conjecture,
c8_1(a300) ).
cnf(u3439,negated_conjecture,
~ c4_1(a300) ).
cnf(u3469,negated_conjecture,
~ c6_2(a414,a415) ).
cnf(u3482,negated_conjecture,
~ c6_2(a347,a444) ).
cnf(u3486,negated_conjecture,
~ c6_2(a347,a401) ).
cnf(u3490,negated_conjecture,
~ c1_1(a347) ).
cnf(u3500,negated_conjecture,
~ c6_2(a380,a381) ).
cnf(u3514,negated_conjecture,
~ c6_2(a309,a401) ).
cnf(u3518,negated_conjecture,
~ c1_1(a309) ).
cnf(u3566,negated_conjecture,
~ c1_1(a385) ).
cnf(u3587,negated_conjecture,
c4_2(a369,a344) ).
cnf(u3592,negated_conjecture,
c4_2(a385,a344) ).
cnf(u3597,negated_conjecture,
c4_2(a380,a344) ).
cnf(u3618,negated_conjecture,
c4_2(a402,a344) ).
cnf(u3644,negated_conjecture,
~ c3_1(a410) ).
cnf(u3657,negated_conjecture,
~ c3_1(a330) ).
cnf(u3675,negated_conjecture,
~ c3_1(a347) ).
cnf(u3691,negated_conjecture,
~ c3_1(a380) ).
cnf(u3705,negated_conjecture,
c8_2(a369,a344) ).
cnf(u3714,negated_conjecture,
c8_2(a385,a344) ).
cnf(u3717,negated_conjecture,
~ c2_2(a385,a392) ).
cnf(u3723,negated_conjecture,
c8_2(a425,a426) ).
cnf(u3752,negated_conjecture,
c4_2(a385,a320) ).
cnf(u3759,negated_conjecture,
c4_2(a300,a389) ).
cnf(u3780,negated_conjecture,
c8_2(a300,a389) ).
cnf(u3791,negated_conjecture,
~ c8_2(a385,a368) ).
cnf(u3800,negated_conjecture,
c8_2(a309,a320) ).
cnf(u3843,negated_conjecture,
~ c1_2(a369,a344) ).
cnf(u3856,negated_conjecture,
~ c1_2(a385,a344) ).
cnf(u3860,negated_conjecture,
~ c1_2(a385,a318) ).
cnf(u3869,negated_conjecture,
~ c1_2(a454,a455) ).
cnf(u3882,negated_conjecture,
~ c1_2(a300,a389) ).
cnf(u3886,negated_conjecture,
~ c1_2(a300,a318) ).
cnf(u3895,negated_conjecture,
~ c1_2(a305,a306) ).
cnf(u3899,negated_conjecture,
~ c1_2(a305,a318) ).
cnf(u3904,negated_conjecture,
~ c1_2(a355,a318) ).
cnf(u3908,negated_conjecture,
c3_2(a355,a356) ).
cnf(u4171,negated_conjecture,
~ c6_2(a405,a406) ).
cnf(u4179,negated_conjecture,
~ c1_1(a405) ).
cnf(u4194,negated_conjecture,
c5_2(a405,a406) ).
cnf(u4198,negated_conjecture,
c4_2(a405,a406) ).
cnf(u4226,negated_conjecture,
~ c3_1(a405) ).
cnf(u4249,negated_conjecture,
~ ssSkP1(a355) ).
cnf(u4270,negated_conjecture,
~ c4_2(a380,a360) ).
cnf(u4283,negated_conjecture,
~ c4_2(a311,a360) ).
cnf(u4297,negated_conjecture,
~ c1_2(a355,a359) ).
cnf(u4328,negated_conjecture,
~ c8_2(a417,a412) ).
cnf(u4333,negated_conjecture,
c7_2(a417,a418) ).
cnf(u4336,negated_conjecture,
~ c3_2(a417,a411) ).
cnf(u4342,negated_conjecture,
c8_2(a305,a412) ).
cnf(u4350,negated_conjecture,
c3_2(a305,a411) ).
cnf(u4355,negated_conjecture,
c8_2(a385,a412) ).
cnf(u4373,negated_conjecture,
~ c1_2(a417,a412) ).
cnf(u4395,negated_conjecture,
~ c6_2(a305,a412) ).
cnf(u4404,negated_conjecture,
~ c1_2(a305,a412) ).
cnf(u4416,negated_conjecture,
~ c1_2(a385,a412) ).
cnf(u4469,negated_conjecture,
~ c5_1(a369) ).
cnf(u4483,negated_conjecture,
~ c5_1(a425) ).
cnf(u4499,negated_conjecture,
~ c5_1(a454) ).
cnf(u4529,negated_conjecture,
c5_2(a385,a412) ).
cnf(u4538,negated_conjecture,
c5_2(a385,a344) ).
cnf(u4542,negated_conjecture,
( ~ c1_2(a309,X0)
| ~ c6_2(a309,X0) ) ).
cnf(u4554,negated_conjecture,
( ~ c1_2(a402,X0)
| ~ c6_2(a402,X0) ) ).
cnf(u4575,negated_conjecture,
~ c6_1(a417) ).
cnf(u4602,negated_conjecture,
~ c1_1(a417) ).
cnf(u4630,negated_conjecture,
c3_2(a402,a411) ).
cnf(u4651,negated_conjecture,
c7_2(a309,a434) ).
cnf(u4682,negated_conjecture,
c8_2(a349,a412) ).
cnf(u4691,negated_conjecture,
c2_1(a314) ).
cnf(u4717,negated_conjecture,
c7_2(a442,a404) ).
cnf(u4732,negated_conjecture,
c3_1(a314) ).
cnf(u4741,negated_conjecture,
c3_2(a314,a390) ).
cnf(u4758,negated_conjecture,
~ c1_2(a349,a412) ).
cnf(u4785,negated_conjecture,
c8_2(a442,a404) ).
cnf(u4794,negated_conjecture,
~ c6_1(a442) ).
cnf(u4818,negated_conjecture,
~ c5_2(a442,a404) ).
cnf(u4822,negated_conjecture,
~ c1_1(a442) ).
cnf(u4833,negated_conjecture,
~ c1_2(a442,a404) ).
cnf(u4840,negated_conjecture,
~ c3_2(a442,a404) ).
cnf(u4853,negated_conjecture,
~ c3_1(a442) ).
cnf(u4873,negated_conjecture,
c7_2(a417,a444) ).
cnf(u4885,negated_conjecture,
c2_2(a417,a444) ).
cnf(u4894,negated_conjecture,
c4_2(a417,a444) ).
cnf(u4916,negated_conjecture,
c6_2(a385,a412) ).
cnf(u4933,negated_conjecture,
c6_2(a349,a412) ).
cnf(u4944,negated_conjecture,
c4_2(a349,a344) ).
cnf(u4973,negated_conjecture,
c2_2(a385,a412) ).
cnf(u4988,negated_conjecture,
~ c2_2(a349,a412) ).
cnf(u4997,negated_conjecture,
~ c6_2(a349,a401) ).
cnf(u5030,negated_conjecture,
~ c5_1(a442) ).
cnf(u5037,negated_conjecture,
c2_2(a442,a404) ).
cnf(u5049,negated_conjecture,
c2_2(a385,a344) ).
cnf(u5076,negated_conjecture,
~ c1_2(a405,a406) ).
cnf(u5091,negated_conjecture,
c1_2(a417,a444) ).
cnf(u5102,negated_conjecture,
c4_2(a417,a319) ).
cnf(u5108,negated_conjecture,
c1_2(a347,a444) ).
cnf(u5174,negated_conjecture,
c5_2(a414,a415) ).
cnf(u5185,negated_conjecture,
~ c5_2(a305,a306) ).
cnf(u5189,negated_conjecture,
( c6_2(a305,X0)
| c8_2(a305,X0) ) ).
cnf(u5198,negated_conjecture,
c5_2(a380,a381) ).
cnf(u5214,negated_conjecture,
c3_2(a385,a320) ).
cnf(u5219,negated_conjecture,
c1_2(a385,a320) ).
cnf(u5230,negated_conjecture,
c6_2(a345,a378) ).
cnf(u5233,negated_conjecture,
~ c3_1(a345) ).
cnf(u5243,negated_conjecture,
c3_2(a345,a390) ).
cnf(u5253,negated_conjecture,
c1_1(a345) ).
cnf(u5265,negated_conjecture,
~ c6_2(a345,a401) ).
cnf(u5278,negated_conjecture,
c7_2(a345,a346) ).
cnf(u5282,negated_conjecture,
c5_1(a345) ).
cnf(u5326,negated_conjecture,
~ c8_2(a414,a415) ).
cnf(u5352,negated_conjecture,
c6_1(a305) ).
cnf(u5367,negated_conjecture,
c4_2(a345,a346) ).
cnf(u5402,negated_conjecture,
c4_1(a345) ).
cnf(u5425,negated_conjecture,
c7_2(a385,a320) ).
cnf(u5445,negated_conjecture,
c2_1(a305) ).
cnf(u5458,negated_conjecture,
c8_2(a305,a389) ).
cnf(u5490,negated_conjecture,
c3_1(a305) ).
cnf(u5499,negated_conjecture,
c3_2(a305,a390) ).
cnf(u5520,negated_conjecture,
~ c6_2(a305,a389) ).
cnf(u5529,negated_conjecture,
~ c1_2(a305,a389) ).
cnf(u5576,negated_conjecture,
~ c8_2(a380,a434) ).
cnf(u5594,negated_conjecture,
c5_1(a380) ).
cnf(u5628,negated_conjecture,
c7_1(a417) ).
cnf(u5632,negated_conjecture,
( ~ c3_2(a417,X0)
| c5_2(a417,X0)
| c7_2(a417,X0) ) ).
cnf(u5641,negated_conjecture,
~ c7_1(a385) ).
cnf(u5648,negated_conjecture,
c7_1(a442) ).
cnf(u5708,negated_conjecture,
( c6_2(a442,X0)
| c8_2(a442,X0) ) ).
cnf(u5729,negated_conjecture,
ssSkP2(a442) ).
cnf(u5784,negated_conjecture,
( c6_2(a417,X0)
| c5_2(a417,X0)
| c7_2(a417,X0) ) ).
cnf(u5791,negated_conjecture,
( c3_2(a417,X0)
| c7_2(a417,X0)
| c6_2(a417,X0) ) ).
cnf(u5795,negated_conjecture,
c7_2(a417,a411) ).
cnf(u5803,negated_conjecture,
~ c6_2(a417,a411) ).
cnf(u5846,negated_conjecture,
c8_1(a417) ).
cnf(u5851,negated_conjecture,
c3_2(a385,a389) ).
cnf(u5866,negated_conjecture,
~ c2_2(a309,a434) ).
cnf(u5874,negated_conjecture,
~ c3_2(a405,a406) ).
cnf(u5886,negated_conjecture,
~ c2_2(a385,a320) ).
cnf(u5892,negated_conjecture,
~ c3_2(a345,a346) ).
cnf(u5940,negated_conjecture,
c7_2(a417,a359) ).
cnf(u6006,negated_conjecture,
~ c5_2(a300,a389) ).
cnf(u6013,negated_conjecture,
c7_1(a300) ).
cnf(u6023,negated_conjecture,
~ c6_2(a417,a444) ).
cnf(u6031,negated_conjecture,
~ c6_2(a417,a359) ).
cnf(u6041,negated_conjecture,
~ c7_1(a345) ).
cnf(u6054,negated_conjecture,
c3_2(a345,a411) ).
cnf(u6120,negated_conjecture,
( c3_2(a355,X0)
| c1_2(a355,X0)
| c5_2(a355,X0) ) ).
cnf(u6128,negated_conjecture,
( c3_2(a380,X0)
| c1_2(a380,X0)
| c5_2(a380,X0) ) ).
cnf(u6145,negated_conjecture,
c8_2(a311,a427) ).
cnf(u6158,negated_conjecture,
~ c1_2(a311,a427) ).
cnf(u6179,negated_conjecture,
~ c5_1(a311) ).
cnf(u6202,negated_conjecture,
ssSkP0(a355) ).
cnf(u6218,negated_conjecture,
ssSkP0(a380) ).
cnf(u6232,negated_conjecture,
c5_2(a380,a434) ).
cnf(u6250,negated_conjecture,
~ c1_2(a380,a434) ).
cnf(u6307,negated_conjecture,
( ~ c5_2(a417,X1)
| c8_2(a417,X1)
| c3_2(a417,X1) ) ).
cnf(u6327,negated_conjecture,
( ~ c7_2(a385,X0)
| c3_2(a385,X0) ) ).
cnf(u6331,negated_conjecture,
( ~ c5_2(a442,X1)
| c8_2(a442,X1)
| c3_2(a442,X1) ) ).
cnf(clause112,negated_conjecture,
( ssSkP4(X0)
| c1_2(X0,a432) ) ).
cnf(u2945,negated_conjecture,
c4_2(a414,a368) ).
cnf(clause50,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u3265,negated_conjecture,
ssSkP2(a309) ).
cnf(u4963,negated_conjecture,
( c3_2(X0,a411)
| c6_2(X0,a411)
| c7_2(X0,a411)
| ~ ndr1_1(X0)
| c2_2(X0,a412) ) ).
cnf(u2946,negated_conjecture,
c4_2(a330,a368) ).
cnf(u4307,negated_conjecture,
( c3_2(X0,a411)
| c3_2(X0,X1)
| c6_2(X0,X1)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| c2_2(X0,a412) ) ).
cnf(clause45,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(u3147,negated_conjecture,
c4_2(a347,a444) ).
cnf(u5410,negated_conjecture,
c8_2(a385,a320) ).
cnf(clause202,negated_conjecture,
( ~ c6_2(X0,a389)
| ssSkP2(X0) ) ).
cnf(clause204,negated_conjecture,
( ~ c6_2(X0,a359)
| ssSkP1(X0) ) ).
cnf(clause198,negated_conjecture,
( ~ c2_2(X0,a411)
| ssSkP3(X0) ) ).
cnf(u4903,negated_conjecture,
( c3_2(X0,a411)
| c6_2(X0,a411)
| c7_2(X0,a411)
| ~ ndr1_1(X0)
| c6_2(X0,a412) ) ).
cnf(clause197,negated_conjecture,
( ~ c8_2(X0,a411)
| ssSkP3(X0) ) ).
cnf(u4305,negated_conjecture,
( c3_2(X0,a411)
| c3_2(X0,X1)
| c6_2(X0,X1)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| c6_2(X0,a412) ) ).
cnf(u4604,negated_conjecture,
c4_2(a417,a368) ).
cnf(u3049,negated_conjecture,
( ~ c2_1(X0)
| c3_2(X0,a390)
| c7_2(X0,a389) ) ).
cnf(u3024,negated_conjecture,
ndr1_1(a349) ).
cnf(u3159,negated_conjecture,
c7_2(a347,a444) ).
cnf(clause127,negated_conjecture,
( ssSkP1(X0)
| c8_2(X0,a359) ) ).
cnf(u4303,negated_conjecture,
( c3_2(X0,a411)
| c3_2(X0,X1)
| c6_2(X0,X1)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| c8_2(X0,a412) ) ).
cnf(clause210,negated_conjecture,
( ~ c8_2(X0,a340)
| ssSkP0(X0) ) ).
cnf(u3134,negated_conjecture,
( ~ c4_1(X0)
| ndr1_1(X0) ) ).
cnf(u3153,negated_conjecture,
c2_2(a347,a444) ).
cnf(clause62,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(u4824,negated_conjecture,
c4_2(a442,a368) ).
cnf(u3082,negated_conjecture,
c5_1(a402) ).
cnf(clause205,negated_conjecture,
( ~ c4_2(X0,a359)
| ssSkP1(X0) ) ).
cnf(u3004,negated_conjecture,
c4_2(a410,a368) ).
cnf(clause134,negated_conjecture,
( ssSkP0(X0)
| c6_2(X0,a340) ) ).
cnf(clause48,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(clause55,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u4315,negated_conjecture,
( c3_2(X0,a411)
| c6_2(X0,a411)
| c7_2(X0,a411)
| ~ ndr1_1(X0)
| c8_2(X0,a412) ) ).
cnf(u3081,negated_conjecture,
c5_1(a309) ).
cnf(u2941,negated_conjecture,
( ~ c2_1(X0)
| ndr1_1(X0) ) ).
cnf(clause211,negated_conjecture,
( ~ c3_2(X0,a340)
| ssSkP0(X0) ) ).
cnf(clause196,negated_conjecture,
( ~ c7_2(X0,a432)
| ssSkP4(X0) ) ).
cnf(u4289,negated_conjecture,
c8_2(a355,a359) ).
cnf(u3050,negated_conjecture,
( ~ c2_1(X0)
| c3_2(X0,a390)
| c2_2(X0,a389) ) ).
cnf(clause122,negated_conjecture,
( ssSkP2(X0)
| c2_2(X0,a389) ) ).
cnf(clause123,negated_conjecture,
( ssSkP2(X0)
| c7_2(X0,a389) ) ).
cnf(u3065,negated_conjecture,
ndr1_1(a314) ).
cnf(clause117,negated_conjecture,
( ssSkP3(X0)
| c3_2(X0,a411) ) ).
cnf(clause111,negated_conjecture,
( ssSkP4(X0)
| c6_2(X0,a432) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN546-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.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:30:49 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running first-order theorem proving
% 0.09/0.24 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
% 3.90/1.29 % (497666)Input is clausal, will run a generic CNF schedule.
% 3.90/1.29 % (497742)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=451025813:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.90/1.29 % (497739)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=946387951:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.90/1.29 % (497740)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=828527303:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.90/1.29 % (497738)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=1445931017:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.90/1.29 % (497742)Instruction limit reached!
% 3.90/1.29 % (497742)------------------------------
% 3.90/1.29 % (497742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.90/1.29 % (497742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.90/1.29 % (497742)CaDiCaL version: 2.1.3
% 3.90/1.29 % (497742)Termination reason: Instruction limit
% 3.90/1.29 % (497742)Termination phase: Saturation
% 3.90/1.29 % (497742)Time elapsed: 0.038 s
% 3.90/1.29 % (497742)Peak memory usage: 90 MB
% 3.90/1.29 % (497742)Instructions burned: 116 (million)
% 3.90/1.29 % (497741)lrs+10_1_sil=8000:sp=occurrence:random_seed=51122280:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.90/1.29 % (497744)dis-21_1_sil=8000:lcm=predicate:random_seed=257664640: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)
% 3.90/1.29 % (497743)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2222580902:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.90/1.29 % (497743)Refutation not found, incomplete strategy
% 3.90/1.29 % (497743)------------------------------
% 3.90/1.29 % (497743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.90/1.29 % (497743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.90/1.29 % (497743)CaDiCaL version: 2.1.3
% 3.90/1.29 % (497743)Termination reason: Refutation not found, incomplete strategy
% 3.90/1.29 % (497743)Time elapsed: 0.048 s
% 3.90/1.29 % (497743)Peak memory usage: 91 MB
% 3.90/1.29 % (497743)Instructions burned: 82 (million)
% 3.90/1.29 % (497741)Instruction limit reached!
% 3.90/1.29 % (497741)------------------------------
% 3.90/1.29 % (497741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.90/1.29 % (497741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.90/1.29 % (497741)CaDiCaL version: 2.1.3
% 3.90/1.29 % (497741)Termination reason: Instruction limit
% 3.90/1.29 % (497741)Termination phase: Saturation
% 3.90/1.29 % (497741)Time elapsed: 0.060 s
% 3.90/1.29 % (497741)Peak memory usage: 90 MB
% 3.90/1.29 % (497741)Instructions burned: 107 (million)
% 3.90/1.29 % (497744)Instruction limit reached!
% 3.90/1.29 % (497744)------------------------------
% 3.90/1.29 % (497744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.90/1.29 % (497744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.90/1.29 % (497744)CaDiCaL version: 2.1.3
% 3.90/1.29 % (497744)Termination reason: Instruction limit
% 3.90/1.29 % (497744)Termination phase: Saturation
% 3.90/1.29 % (497744)Time elapsed: 0.064 s
% 3.90/1.29 % (497744)Peak memory usage: 91 MB
% 3.90/1.29 % (497744)Instructions burned: 117 (million)
% 3.90/1.29 % (497749)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=4265055147:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 3.90/1.29 % (497749)Instruction limit reached!
% 3.90/1.29 % (497749)------------------------------
% 3.90/1.29 % (497749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.90/1.29 % (497749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.90/1.29 % (497749)CaDiCaL version: 2.1.3
% 3.90/1.29 % (497749)Termination reason: Instruction limit
% 3.90/1.29 % (497749)Termination phase: Saturation
% 3.90/1.29 % (497749)Time elapsed: 0.074 s
% 3.90/1.29 % (497749)Peak memory usage: 91 MB
% 3.90/1.29 % (497749)Instructions burned: 143 (million)
% 3.90/1.29 % (497754)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1723350357:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 3.90/1.29 % (497753)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4005248156: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)
% 3.90/1.29 % (497753)Refutation not found, incomplete strategy
% 3.90/1.29 % (497753)------------------------------
% 3.90/1.29 % (497753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.90/1.29 % (497753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.90/1.29 % (497753)CaDiCaL version: 2.1.3
% 3.90/1.29 % (497753)Termination reason: Refutation not found, incomplete strategy
% 3.90/1.29 % (497753)Time elapsed: 0.036 s
% 3.90/1.29 % (497753)Peak memory usage: 90 MB
% 3.90/1.29 % (497753)Instructions burned: 62 (million)
% 3.90/1.29 % (497756)lrs+10_64_to=lpo:sil=8000:random_seed=1264747672:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 3.90/1.29 % (497743)------------------------------
% 3.90/1.29 % (497743)------------------------------
% 3.90/1.29 % (497756)First to succeed.
% 3.90/1.29 % (497756)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-497666"
% 3.90/1.29 % (497754)Instruction limit reached!
% 3.90/1.29 % (497754)------------------------------
% 3.90/1.29 % (497754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.90/1.29 % (497754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.90/1.29 % (497754)CaDiCaL version: 2.1.3
% 3.90/1.29 % (497754)Termination reason: Instruction limit
% 3.90/1.29 % (497754)Termination phase: Saturation
% 3.90/1.29 % (497754)Time elapsed: 0.123 s
% 3.90/1.29 % (497754)Peak memory usage: 92 MB
% 3.90/1.29 % (497754)Instructions burned: 220 (million)
% 3.90/1.29 % (497760)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3170668620:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 3.90/1.29 % (497761)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1282982120:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 3.90/1.29 % (497760)Refutation not found, incomplete strategy
% 3.90/1.29 % (497760)------------------------------
% 3.90/1.29 % (497760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.90/1.29 % (497760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.90/1.29 % (497760)CaDiCaL version: 2.1.3
% 3.90/1.29 % (497760)Termination reason: Refutation not found, incomplete strategy
% 3.90/1.29 % (497760)Time elapsed: 0.032 s
% 3.90/1.29 % (497760)Peak memory usage: 90 MB
% 3.90/1.29 % (497760)Instructions burned: 50 (million)
% 3.90/1.29 % SZS status Satisfiable for theBenchmark
% 3.90/1.29 % SZS output start Saturation.
% See solution above
% 4.93/1.39 % SZS output start Definitions and Model Updates.
% 4.93/1.39 % SZS output end Definitions and Model Updates.
% 4.93/1.39 % (497756)------------------------------
% 4.93/1.39 % (497756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.93/1.39 % (497756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.93/1.39 % (497756)CaDiCaL version: 2.1.3
% 4.93/1.39 % (497756)Termination reason: Satisfiable
% 4.93/1.39 % (497756)Time elapsed: 0.032 s
% 4.93/1.39 % (497756)Peak memory usage: 91 MB
% 4.93/1.39 % (497756)Instructions burned: 99 (million)
% 4.93/1.39 % (497756)------------------------------
% 4.93/1.39 % (497756)------------------------------
% 4.93/1.39 % (497666)Success in time 0.631 s
% 4.93/1.39 % Vampire exiting
%------------------------------------------------------------------------------