%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN546-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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:17:33 PM UTC 2026
% Result : Satisfiable 0.21s 0.30s
% Output : Saturation 0.21s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u535,negated_conjecture,
( ~ c7_1(X3)
| c2_2(X3,X5)
| c4_2(X3,X5)
| c5_2(X3,X4)
| c7_2(X3,X4)
| ~ c3_2(X3,X4)
| ~ c7_2(X3,X5)
| ~ ndr1_1(X3) ) ).
cnf(u538,negated_conjecture,
ndr1_0 ).
cnf(u567,negated_conjecture,
c5_0 ).
cnf(u574,negated_conjecture,
( c8_1(X0)
| ~ c2_2(X0,X1)
| c8_2(X0,X1)
| c1_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c3_2(X0,X2)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u587,negated_conjecture,
c3_0 ).
cnf(u604,negated_conjecture,
( ~ c1_1(X2)
| c4_1(X2)
| ~ c2_1(X2) ) ).
cnf(u623,negated_conjecture,
~ c6_0 ).
cnf(u634,negated_conjecture,
( ~ c1_1(X0)
| c2_1(X0)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u652,negated_conjecture,
( ~ c5_1(X0)
| c7_2(X0,X1)
| c5_2(X0,X1)
| ~ c8_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c1_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u665,negated_conjecture,
( ~ c7_1(X0)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ c6_2(X0,X1)
| ~ c8_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u714,negated_conjecture,
c2_0 ).
cnf(u718,negated_conjecture,
( c3_2(X0,X2)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c5_2(X0,X2)
| ~ ndr1_1(X0)
| c1_2(X0,X2)
| ~ c1_2(X0,a427)
| ~ c1_2(X0,X1) ) ).
cnf(u722,negated_conjecture,
( ~ c3_1(X1)
| c2_1(X1)
| ~ c5_1(X1) ) ).
cnf(u737,negated_conjecture,
( c3_2(a431,X2)
| c1_2(a431,X2) ) ).
cnf(u740,negated_conjecture,
ndr1_1(a431) ).
cnf(u752,negated_conjecture,
( ~ c5_1(X0)
| c2_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X1)
| ~ c8_2(X0,X1)
| ~ c8_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u757,negated_conjecture,
~ c4_0 ).
cnf(u769,negated_conjecture,
( c3_2(X0,X2)
| c8_2(X0,a427)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c5_2(X0,X2)
| ~ ndr1_1(X0)
| c1_2(X0,X2)
| ~ c1_2(X0,X1) ) ).
cnf(u823,negated_conjecture,
( c1_1(X0)
| ~ c6_1(X0)
| c4_1(X0) ) ).
cnf(u826,negated_conjecture,
ssSkC3 ).
cnf(u834,negated_conjecture,
( c3_1(X0)
| c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u837,negated_conjecture,
ssSkC8 ).
cnf(u843,negated_conjecture,
c7_0 ).
cnf(u851,negated_conjecture,
( ~ c1_1(X0)
| ~ c2_2(X0,X1)
| ~ c6_2(X0,a401)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u855,negated_conjecture,
( ~ c1_1(X0)
| ~ c2_2(X0,X1)
| ~ c7_2(X0,a401)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u859,negated_conjecture,
( ~ c1_1(X0)
| ~ c2_2(X0,X1)
| ~ c2_2(X0,a401)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u887,negated_conjecture,
~ ssSkC16 ).
cnf(u890,negated_conjecture,
ssSkC15 ).
cnf(u899,negated_conjecture,
( c4_1(X0)
| ~ ndr1_1(X0)
| c8_1(X0)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c6_2(X0,X1) ) ).
cnf(u913,negated_conjecture,
( c6_1(X0)
| ~ c8_2(X0,X1)
| c1_2(X0,X1)
| ~ c1_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u917,negated_conjecture,
( c6_1(X0)
| ~ c8_2(X0,X1)
| c1_2(X0,X1)
| ~ c7_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u921,negated_conjecture,
~ ssSkC6 ).
cnf(u925,negated_conjecture,
( c4_1(X0)
| ~ c1_2(X0,X1)
| c8_2(X0,X1)
| ~ c7_2(X0,a333)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u930,negated_conjecture,
ssSkC18 ).
cnf(u941,negated_conjecture,
c8_0 ).
cnf(u945,negated_conjecture,
( c3_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c1_2(X0,a318)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u948,negated_conjecture,
ssSkC2 ).
cnf(u953,negated_conjecture,
( c3_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c2_2(X0,a318)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u986,negated_conjecture,
( c5_1(X0)
| ~ c6_1(X0)
| c8_1(X0) ) ).
cnf(u991,negated_conjecture,
~ c2_1(a431) ).
cnf(u996,negated_conjecture,
~ c1_1(a431) ).
cnf(u1000,negated_conjecture,
( c4_1(X0)
| ~ c1_2(X0,X1)
| c6_2(X0,a333)
| c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u1004,negated_conjecture,
( c4_1(X0)
| ~ c1_2(X0,X1)
| c2_2(X0,a333)
| c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u1008,negated_conjecture,
~ ssSkC14 ).
cnf(u1012,negated_conjecture,
( ~ ssSkP1(X0)
| c4_2(X0,X1)
| c7_2(X0,X1)
| ~ c8_2(X0,a360)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1016,negated_conjecture,
( ~ ssSkP1(X0)
| c4_2(X0,X1)
| c7_2(X0,X1)
| ~ c4_2(X0,a360)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1020,negated_conjecture,
( ~ ssSkP1(X0)
| c4_2(X0,X1)
| c7_2(X0,X1)
| ~ c5_2(X0,a360)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1032,negated_conjecture,
( c3_2(X0,X1)
| c7_2(X0,a318)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1040,negated_conjecture,
~ c1_0 ).
cnf(u1044,negated_conjecture,
( ~ c3_1(X0)
| c8_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c4_2(X0,a392)
| ~ ndr1_1(X0) ) ).
cnf(u1048,negated_conjecture,
~ ssSkC21 ).
cnf(u1066,negated_conjecture,
ndr1_1(a374) ).
cnf(u1070,negated_conjecture,
( ~ c1_2(a374,X0)
| c8_2(a374,X0)
| ~ c5_2(a374,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(u1145,negated_conjecture,
ndr1_1(a305) ).
cnf(u1149,negated_conjecture,
( ~ c6_2(a305,X0)
| c4_2(a305,X0)
| ~ c8_2(a305,X0) ) ).
cnf(u1160,negated_conjecture,
ssSkC4 ).
cnf(u1165,negated_conjecture,
( c2_2(a374,X0)
| c4_2(a374,X0)
| ~ c5_2(a374,X0) ) ).
cnf(u1194,negated_conjecture,
~ ndr1_1(a315) ).
cnf(u1213,negated_conjecture,
~ ssSkC10 ).
cnf(u1241,negated_conjecture,
~ ndr1_1(a453) ).
cnf(u1244,negated_conjecture,
( c3_2(a453,X0)
| ~ c8_2(a453,X0)
| ~ c4_2(a453,X0) ) ).
cnf(u1248,negated_conjecture,
( ~ c3_2(a453,X0)
| c7_2(a453,X0)
| ~ c2_2(a453,X0) ) ).
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,
( c6_2(a442,X0)
| ~ c7_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,
( c6_2(a300,X0)
| ~ c2_2(a300,X0)
| c1_2(a300,X0) ) ).
cnf(u1345,negated_conjecture,
~ ndr1_1(a366) ).
cnf(u1393,negated_conjecture,
ssSkC19 ).
cnf(u1430,negated_conjecture,
( ~ c5_1(X0)
| ~ c6_1(X0)
| ~ c4_2(X0,a391) ) ).
cnf(u1464,negated_conjecture,
~ ssSkC7 ).
cnf(u1468,negated_conjecture,
( c3_1(X0)
| ~ c7_2(X0,a337)
| ~ c2_1(X0) ) ).
cnf(u1480,negated_conjecture,
( ~ c5_1(X0)
| c8_2(X0,a391)
| ~ c6_1(X0) ) ).
cnf(u1484,negated_conjecture,
( ~ c5_1(X0)
| c7_2(X0,a391)
| ~ c6_1(X0) ) ).
cnf(u1488,negated_conjecture,
~ ssSkC25 ).
cnf(u1492,negated_conjecture,
( c7_1(X0)
| ~ c1_2(X0,a434)
| ~ c5_1(X0) ) ).
cnf(u1496,negated_conjecture,
( c7_1(X0)
| ~ c6_2(X0,a434)
| ~ c5_1(X0) ) ).
cnf(u1500,negated_conjecture,
( c7_1(X0)
| ~ c3_2(X0,a434)
| ~ c5_1(X0) ) ).
cnf(u1505,negated_conjecture,
ssSkC28 ).
cnf(u1531,negated_conjecture,
ssSkC22 ).
cnf(u1537,negated_conjecture,
ssSkC12 ).
cnf(u1549,negated_conjecture,
ssSkC20 ).
cnf(u1553,negated_conjecture,
( ~ ssSkP2(X0)
| ~ c2_1(X0)
| ~ c8_2(X0,a390) ) ).
cnf(u1557,negated_conjecture,
( ~ ssSkP2(X0)
| ~ c2_1(X0)
| ~ c7_2(X0,a390) ) ).
cnf(u1561,negated_conjecture,
( c8_1(X0)
| ~ c6_2(X0,a404)
| c2_1(X0) ) ).
cnf(u1565,negated_conjecture,
( c8_1(X0)
| ~ c3_2(X0,a404)
| c2_1(X0) ) ).
cnf(u1574,negated_conjecture,
( c3_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a337) ) ).
cnf(u1578,negated_conjecture,
( c3_1(X0)
| ~ c2_1(X0)
| c8_2(X0,a337) ) ).
cnf(u1586,negated_conjecture,
( ~ c5_1(X0)
| ndr1_1(X0)
| ~ c6_1(X0) ) ).
cnf(u1658,negated_conjecture,
( ~ ssSkP2(X0)
| c3_2(X0,a390)
| ~ c2_1(X0) ) ).
cnf(u1662,negated_conjecture,
( c8_1(X0)
| c1_2(X0,a404)
| c2_1(X0) ) ).
cnf(u1666,negated_conjecture,
( c3_1(X0)
| ~ c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u1671,negated_conjecture,
( c7_1(X0)
| ~ c5_1(X0)
| ndr1_1(X0) ) ).
cnf(u1679,negated_conjecture,
( c6_1(X0)
| ~ c8_2(X0,a368) ) ).
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(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(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(u1831,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(u1857,negated_conjecture,
c5_2(a374,a375) ).
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(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(u2012,negated_conjecture,
~ c6_1(a330) ).
cnf(u2017,negated_conjecture,
c6_2(a330,a331) ).
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(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(u2244,negated_conjecture,
~ c2_2(a300,a301) ).
cnf(u2249,negated_conjecture,
~ c1_2(a300,a301) ).
cnf(u2366,negated_conjecture,
ndr1_1(a330) ).
cnf(u2401,negated_conjecture,
c6_1(a355) ).
cnf(u2406,negated_conjecture,
ndr1_1(a355) ).
cnf(u2411,negated_conjecture,
c2_1(a369) ).
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(u2527,negated_conjecture,
c5_2(a300,a301) ).
cnf(u2532,negated_conjecture,
~ c2_1(a315) ).
cnf(u2537,negated_conjecture,
~ c4_1(a315) ).
cnf(u2780,negated_conjecture,
c3_1(a453) ).
cnf(u2785,negated_conjecture,
c2_1(a300) ).
cnf(u2943,negated_conjecture,
~ c5_1(a453) ).
cnf(u2952,negated_conjecture,
~ c5_1(a425) ).
cnf(u2969,negated_conjecture,
~ c6_1(a298) ).
cnf(u2978,negated_conjecture,
~ c6_1(a431) ).
cnf(u2986,negated_conjecture,
~ c2_1(a349) ).
cnf(u3008,negated_conjecture,
~ c6_1(a305) ).
cnf(u3017,negated_conjecture,
~ c6_1(a425) ).
cnf(u3026,negated_conjecture,
~ c6_1(a453) ).
cnf(u3093,negated_conjecture,
~ c8_2(a442,a404) ).
cnf(u3098,negated_conjecture,
~ c7_2(a442,a404) ).
cnf(u3119,negated_conjecture,
~ c4_2(a453,a392) ).
cnf(u3127,negated_conjecture,
~ c4_2(a425,a392) ).
cnf(u3167,negated_conjecture,
~ c4_2(a417,a391) ).
cnf(u3171,negated_conjecture,
~ c6_1(a417) ).
cnf(u3203,negated_conjecture,
~ c8_2(a417,a418) ).
cnf(u3218,negated_conjecture,
~ c1_2(a453,a318) ).
cnf(u3226,negated_conjecture,
~ c8_2(a349,a404) ).
cnf(u3230,negated_conjecture,
~ c1_2(a349,a318) ).
cnf(u3239,negated_conjecture,
~ c1_2(a305,a306) ).
cnf(u3244,negated_conjecture,
~ c1_2(a442,a318) ).
cnf(u3257,negated_conjecture,
~ c2_2(a453,a318) ).
cnf(u3287,negated_conjecture,
( c3_2(a425,X0)
| c6_2(a425,X0)
| c2_2(a425,X0) ) ).
cnf(u3302,negated_conjecture,
~ ndr1_1(a298) ).
cnf(u3320,negated_conjecture,
~ c1_2(a431,a437) ).
cnf(u3328,negated_conjecture,
~ c1_2(a349,a437) ).
cnf(u3336,negated_conjecture,
~ c1_2(a414,a437) ).
cnf(u3344,negated_conjecture,
~ c1_2(a417,a437) ).
cnf(u3352,negated_conjecture,
~ c1_2(a305,a437) ).
cnf(u3360,negated_conjecture,
~ c1_2(a330,a437) ).
cnf(u3368,negated_conjecture,
~ c1_2(a425,a437) ).
cnf(u3392,negated_conjecture,
~ c7_2(a431,a437) ).
cnf(u3397,negated_conjecture,
~ c7_2(a349,a437) ).
cnf(u3402,negated_conjecture,
~ c7_2(a414,a437) ).
cnf(u3407,negated_conjecture,
~ c7_2(a417,a437) ).
cnf(u3412,negated_conjecture,
~ c7_2(a305,a437) ).
cnf(u3417,negated_conjecture,
~ c7_2(a330,a437) ).
cnf(u3422,negated_conjecture,
~ c7_2(a425,a437) ).
cnf(u3430,negated_conjecture,
~ c7_2(a425,a333) ).
cnf(u3433,negated_conjecture,
( ~ c1_2(a425,X0)
| ~ c5_2(a425,X0)
| c8_2(a425,X0) ) ).
cnf(u3471,negated_conjecture,
( ~ c6_2(a417,X1)
| ~ c1_2(a417,X1) ) ).
cnf(u3478,negated_conjecture,
( ~ c6_2(a414,X1)
| ~ c1_2(a414,X1) ) ).
cnf(u3491,negated_conjecture,
( ~ c8_2(a417,X1)
| c5_2(a417,X1) ) ).
cnf(u3498,negated_conjecture,
( ~ c8_2(a414,X1)
| c5_2(a414,X1) ) ).
cnf(u3513,negated_conjecture,
( ~ c3_2(a442,X1)
| ~ c7_2(a442,X1)
| ~ c2_2(a442,X1) ) ).
cnf(u3520,negated_conjecture,
( ~ c3_2(a349,X1)
| ~ c7_2(a349,X1)
| ~ c2_2(a349,X1) ) ).
cnf(u3539,negated_conjecture,
~ c1_2(a417,a427) ).
cnf(u3543,negated_conjecture,
c5_2(a417,a418) ).
cnf(u3552,negated_conjecture,
~ c1_2(a305,a427) ).
cnf(u3556,negated_conjecture,
c5_2(a305,a306) ).
cnf(u3594,negated_conjecture,
c8_1(a355) ).
cnf(u3598,negated_conjecture,
~ c4_2(a355,a391) ).
cnf(u3620,negated_conjecture,
~ c6_2(a369,a389) ).
cnf(u3624,negated_conjecture,
~ c8_2(a369,a390) ).
cnf(u3629,negated_conjecture,
~ c6_2(a300,a389) ).
cnf(u3633,negated_conjecture,
~ c8_2(a300,a390) ).
cnf(u3649,negated_conjecture,
~ c7_2(a300,a390) ).
cnf(u3659,negated_conjecture,
~ c2_2(a300,a389) ).
cnf(u3666,negated_conjecture,
~ c7_2(a369,a390) ).
cnf(u3671,negated_conjecture,
c7_2(a300,a389) ).
cnf(u3682,negated_conjecture,
c3_2(a369,a390) ).
cnf(u3687,negated_conjecture,
c3_2(a300,a390) ).
cnf(u3712,negated_conjecture,
~ c2_2(a442,a318) ).
cnf(u3717,negated_conjecture,
c7_2(a442,a318) ).
cnf(u3722,negated_conjecture,
~ c1_2(a442,a427) ).
cnf(u3733,negated_conjecture,
c8_2(a442,a427) ).
cnf(u3746,negated_conjecture,
( ~ c2_2(a349,X0)
| ~ c8_2(a349,X0)
| ~ c1_2(a349,X0)
| ~ c7_2(a349,X0) ) ).
cnf(u3759,negated_conjecture,
( ~ c1_2(a349,X1)
| c5_2(a349,X1)
| c4_2(a349,X1) ) ).
cnf(u3787,negated_conjecture,
~ c7_2(a369,a337) ).
cnf(u3791,negated_conjecture,
~ c4_2(a369,a392) ).
cnf(u3803,negated_conjecture,
~ c4_2(a300,a392) ).
cnf(u3828,negated_conjecture,
~ c4_2(a442,a391) ).
cnf(u3843,negated_conjecture,
c8_2(a442,a391) ).
cnf(u3854,negated_conjecture,
~ c4_2(a349,a359) ).
cnf(u3862,negated_conjecture,
~ c8_2(a349,a360) ).
cnf(u3872,negated_conjecture,
~ c4_2(a355,a359) ).
cnf(u3880,negated_conjecture,
~ c8_2(a355,a360) ).
cnf(u3889,negated_conjecture,
~ c4_2(a442,a359) ).
cnf(u3897,negated_conjecture,
~ c8_2(a442,a360) ).
cnf(u3909,negated_conjecture,
~ c2_2(a300,a359) ).
cnf(u3936,negated_conjecture,
~ c4_2(a355,a360) ).
cnf(u3941,negated_conjecture,
~ c4_2(a442,a360) ).
cnf(u3953,negated_conjecture,
~ c4_2(a349,a360) ).
cnf(u3968,negated_conjecture,
~ c5_2(a442,a360) ).
cnf(u3981,negated_conjecture,
~ c5_2(a349,a360) ).
cnf(u3987,negated_conjecture,
~ c5_2(a355,a360) ).
cnf(u4011,negated_conjecture,
~ c2_2(a305,a411) ).
cnf(u4029,negated_conjecture,
~ c2_2(a349,a411) ).
cnf(u4038,negated_conjecture,
~ c2_2(a417,a411) ).
cnf(u4042,negated_conjecture,
c7_2(a417,a418) ).
cnf(u4052,negated_conjecture,
~ c2_2(a442,a411) ).
cnf(u4056,negated_conjecture,
c8_2(a442,a412) ).
cnf(u4075,negated_conjecture,
~ c8_2(a305,a411) ).
cnf(u4081,negated_conjecture,
~ c8_2(a349,a411) ).
cnf(u4086,negated_conjecture,
~ c8_2(a417,a411) ).
cnf(u4092,negated_conjecture,
~ c8_2(a442,a411) ).
cnf(u4115,negated_conjecture,
c3_2(a305,a411) ).
cnf(u4121,negated_conjecture,
c3_2(a349,a411) ).
cnf(u4132,negated_conjecture,
c3_2(a442,a411) ).
cnf(u4217,negated_conjecture,
~ c3_2(a417,a434) ).
cnf(u4223,negated_conjecture,
( c2_2(a417,X0)
| c4_2(a417,X0)
| ~ c7_2(a417,X0) ) ).
cnf(u4227,negated_conjecture,
c3_2(a414,a434) ).
cnf(u4234,negated_conjecture,
( c2_2(a414,X0)
| c4_2(a414,X0)
| ~ c7_2(a414,X0) ) ).
cnf(u4245,negated_conjecture,
~ c6_2(a417,a434) ).
cnf(u4250,negated_conjecture,
~ c6_2(a414,a434) ).
cnf(u4260,negated_conjecture,
c1_2(a417,a434) ).
cnf(u4266,negated_conjecture,
~ c1_2(a414,a434) ).
cnf(u4307,negated_conjecture,
c7_2(a417,a434) ).
cnf(u4333,negated_conjecture,
~ c8_2(a417,a434) ).
cnf(u4448,negated_conjecture,
c7_2(a442,a391) ).
cnf(u4462,negated_conjecture,
c5_2(a349,a404) ).
cnf(u4468,negated_conjecture,
~ c7_2(a417,a411) ).
cnf(u4585,negated_conjecture,
( ~ c6_2(a442,X1)
| ~ c1_2(a442,X1) ) ).
cnf(u4597,negated_conjecture,
( c3_2(a442,X1)
| ~ c8_2(a442,X1)
| c2_2(a442,X1) ) ).
cnf(u4644,negated_conjecture,
~ c3_2(a442,a434) ).
cnf(u4676,negated_conjecture,
~ c8_2(a442,a434) ).
cnf(u4689,negated_conjecture,
~ c6_2(a442,a434) ).
cnf(u4700,negated_conjecture,
~ c1_2(a442,a434) ).
cnf(u4608,negated_conjecture,
( c8_1(X0)
| c7_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c3_2(X0,a434)
| c2_2(X0,X2)
| c4_2(X0,X2)
| c5_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c7_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(u3450,negated_conjecture,
( ~ c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c4_2(X0,a360)
| ~ ndr1_1(X0)
| c4_2(X0,X1)
| c8_2(X0,a359) ) ).
cnf(u3028,negated_conjecture,
c4_2(a431,a368) ).
cnf(u3089,negated_conjecture,
( ~ c2_2(a453,X0)
| c7_2(a453,X0)
| ~ c8_2(a453,X0)
| ~ c4_2(a453,X0) ) ).
cnf(clause50,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u3588,negated_conjecture,
( c8_1(X0)
| ~ c4_2(X0,a391)
| ~ c8_2(X0,X1)
| c1_2(X0,X1)
| ~ c1_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u3113,negated_conjecture,
( ~ c2_1(X0)
| ~ c4_2(X0,X1)
| ~ c4_2(X0,a392)
| c8_2(X0,X1)
| c8_2(X0,a337) ) ).
cnf(u3069,negated_conjecture,
~ c6_2(a442,a404) ).
cnf(u3279,negated_conjecture,
( ~ c6_1(X0)
| ndr1_1(X0)
| c8_1(X0) ) ).
cnf(u3040,negated_conjecture,
~ c8_2(a305,a368) ).
cnf(u3527,negated_conjecture,
( ~ c5_1(X0)
| c4_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X2)
| ~ c5_2(X0,X2)
| ~ c1_2(X0,a434)
| c5_2(X0,X1) ) ).
cnf(u2936,negated_conjecture,
c4_2(a414,a368) ).
cnf(u4620,negated_conjecture,
( c8_1(X0)
| c7_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c1_2(X0,a434)
| c2_2(X0,X2)
| c4_2(X0,X2)
| c5_2(X0,X1)
| c4_2(X0,a368) ) ).
cnf(u3036,negated_conjecture,
c4_2(a349,a368) ).
cnf(u4614,negated_conjecture,
( c8_1(X0)
| c7_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c6_2(X0,a434)
| c2_2(X0,X2)
| c4_2(X0,X2)
| c5_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c1_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(u4630,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c6_2(X0,a434)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ c6_2(X0,X1)
| c4_2(X0,a368) ) ).
cnf(u2992,negated_conjecture,
~ c2_1(a298) ).
cnf(u3454,negated_conjecture,
( c3_2(X0,X1)
| c6_2(X0,X1)
| c8_2(X0,a412)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,a411) ) ).
cnf(u3453,negated_conjecture,
( ~ c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c5_2(X0,a360)
| ~ ndr1_1(X0)
| c4_2(X0,X1)
| c8_2(X0,a359) ) ).
cnf(u3183,negated_conjecture,
~ c8_2(a417,a368) ).
cnf(u3604,negated_conjecture,
( c8_1(X0)
| c8_2(X0,a391)
| ~ c8_2(X0,a368) ) ).
cnf(u3064,negated_conjecture,
( ~ c2_1(X0)
| ~ c7_2(X0,a390)
| c7_2(X0,a389) ) ).
cnf(u4609,negated_conjecture,
( c8_1(X0)
| c7_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c3_2(X0,a434)
| c2_2(X0,X2)
| c4_2(X0,X2)
| c5_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c1_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(u3601,negated_conjecture,
( c8_1(X0)
| c8_2(X0,a391)
| ~ c8_2(X0,X1)
| c1_2(X0,X1)
| ~ c7_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u3051,negated_conjecture,
c4_2(a425,a368) ).
cnf(u4635,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c1_2(X0,a434)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ c6_2(X0,X1)
| c4_2(X0,a368) ) ).
cnf(clause197,negated_conjecture,
( ssSkP3(X0)
| ~ c8_2(X0,a411) ) ).
cnf(u3070,negated_conjecture,
~ c6_2(a349,a404) ).
cnf(u4202,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c1_2(X0,X2)
| c7_2(X0,X1)
| c5_2(X0,X1)
| ~ c8_2(X0,a368) ) ).
cnf(u4631,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c6_2(X0,a434)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ c6_2(X0,X1)
| ~ c8_2(X0,a368) ) ).
cnf(u3456,negated_conjecture,
( c3_2(X0,X1)
| c3_2(X0,a411)
| c8_2(X0,a412)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| c6_2(X0,X1) ) ).
cnf(u4239,negated_conjecture,
( ~ c6_1(X0)
| c5_2(X0,X2)
| c7_2(X0,X2)
| ~ c3_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c6_2(X0,a434)
| c2_2(X0,X1)
| c4_2(X0,X1)
| c8_1(X0) ) ).
cnf(u4633,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c1_2(X0,a434)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ c6_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c7_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(u4255,negated_conjecture,
( ~ c6_1(X0)
| c5_2(X0,X2)
| c7_2(X0,X2)
| ~ c3_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,a434)
| c2_2(X0,X1)
| c4_2(X0,X1)
| c8_1(X0) ) ).
cnf(u4211,negated_conjecture,
( ~ c6_1(X0)
| c5_2(X0,X2)
| c7_2(X0,X2)
| ~ c3_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c3_2(X0,a434)
| c2_2(X0,X1)
| c4_2(X0,X1)
| c8_1(X0) ) ).
cnf(u4629,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c6_2(X0,a434)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ c6_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c1_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(clause123,negated_conjecture,
( ssSkP2(X0)
| c7_2(X0,a389) ) ).
cnf(u3060,negated_conjecture,
( ~ c2_1(X0)
| ~ c8_2(X0,a390)
| c7_2(X0,a389) ) ).
cnf(u3460,negated_conjecture,
( c3_2(X0,X1)
| c6_2(X0,X1)
| c2_2(X0,a412)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,a411) ) ).
cnf(clause112,negated_conjecture,
( ssSkP4(X0)
| c1_2(X0,a432) ) ).
cnf(u3101,negated_conjecture,
( c4_1(X0)
| ~ c7_2(X0,a401)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1)
| ~ c6_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u4611,negated_conjecture,
( c8_1(X0)
| c7_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c3_2(X0,a434)
| c2_2(X0,X2)
| c4_2(X0,X2)
| c5_2(X0,X1)
| ~ c8_2(X0,a368) ) ).
cnf(u3176,negated_conjecture,
( ~ c6_1(X0)
| c8_2(X0,a391)
| c8_1(X0) ) ).
cnf(u3087,negated_conjecture,
c1_2(a442,a404) ).
cnf(clause202,negated_conjecture,
( ssSkP2(X0)
| ~ c6_2(X0,a389) ) ).
cnf(clause204,negated_conjecture,
( ssSkP1(X0)
| ~ c6_2(X0,a359) ) ).
cnf(u3449,negated_conjecture,
( ~ c6_2(X0,a359)
| c7_2(X0,X1)
| ~ c4_2(X0,a360)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| c4_2(X0,X1) ) ).
cnf(u3779,negated_conjecture,
( ~ c2_1(X0)
| ~ c4_2(X0,a392)
| c8_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c2_2(X0,a401)
| ~ c6_2(X0,X2) ) ).
cnf(u3451,negated_conjecture,
( ~ c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c5_2(X0,a360)
| ~ ndr1_1(X0)
| c4_2(X0,X1)
| ~ c4_2(X0,a359) ) ).
cnf(u3602,negated_conjecture,
( c8_1(X0)
| c8_2(X0,a391)
| ~ c8_2(X0,X1)
| c1_2(X0,X1)
| ~ c1_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(clause198,negated_conjecture,
( ssSkP3(X0)
| ~ c2_2(X0,a411) ) ).
cnf(u4160,negated_conjecture,
( c3_2(X0,a411)
| c6_2(X0,a412)
| c7_2(X0,a411)
| ~ ndr1_1(X0)
| c6_2(X0,a411) ) ).
cnf(u3447,negated_conjecture,
( ~ c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c8_2(X0,a360)
| ~ ndr1_1(X0)
| c4_2(X0,X1)
| c8_2(X0,a359) ) ).
cnf(u3584,negated_conjecture,
( c8_1(X0)
| ndr1_1(X0)
| c4_2(X0,a368) ) ).
cnf(u4636,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c1_2(X0,a434)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ c6_2(X0,X1)
| ~ c8_2(X0,a368) ) ).
cnf(u3613,negated_conjecture,
( c8_1(X0)
| c7_2(X0,a391)
| c4_2(X0,a368) ) ).
cnf(u2930,negated_conjecture,
( ~ c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u4271,negated_conjecture,
( ~ c6_1(X0)
| ~ c6_2(X0,X2)
| ~ c8_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c5_2(X0,X2)
| ~ c3_2(X0,a434)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c8_1(X0) ) ).
cnf(u3111,negated_conjecture,
( ~ c2_1(X0)
| ~ c4_2(X0,X1)
| ~ c4_2(X0,a392)
| ~ c7_2(X0,a337)
| c8_2(X0,X1) ) ).
cnf(u3466,negated_conjecture,
( ~ c6_1(X0)
| c5_2(X0,X1)
| ~ c8_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c1_2(X0,X2)
| c7_2(X0,X1)
| c8_1(X0) ) ).
cnf(u3525,negated_conjecture,
( ~ c5_1(X0)
| c4_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X2)
| ~ c5_2(X0,X2)
| ~ c3_2(X0,a434)
| c5_2(X0,X1) ) ).
cnf(u4280,negated_conjecture,
( ~ c6_1(X0)
| ~ c6_2(X0,X2)
| ~ c8_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c5_2(X0,X2)
| ~ c1_2(X0,a434)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c8_1(X0) ) ).
cnf(u3587,negated_conjecture,
( c8_1(X0)
| ~ c4_2(X0,a391)
| ~ c8_2(X0,X1)
| c1_2(X0,X1)
| ~ c7_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u3462,negated_conjecture,
( c3_2(X0,X1)
| c3_2(X0,a411)
| c2_2(X0,a412)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| c6_2(X0,X1) ) ).
cnf(u3045,negated_conjecture,
ndr1_1(a349) ).
cnf(u4206,negated_conjecture,
( c8_1(X0)
| c5_2(X0,X2)
| ~ c8_2(X0,X2)
| ~ c8_2(X0,X1)
| c2_2(X0,X1)
| c3_2(X0,X1)
| c4_2(X0,a368) ) ).
cnf(u3073,negated_conjecture,
~ c3_2(a442,a404) ).
cnf(u4205,negated_conjecture,
( c8_1(X0)
| c5_2(X0,X2)
| ~ c8_2(X0,X2)
| ~ c8_2(X0,X1)
| c2_2(X0,X1)
| c3_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c1_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(u2934,negated_conjecture,
~ c8_2(a414,a368) ).
cnf(u3505,negated_conjecture,
( ~ c5_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X2)
| c7_2(X0,X2)
| ~ c3_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,a434)
| c2_2(X0,X1) ) ).
cnf(u3102,negated_conjecture,
( c4_1(X0)
| ~ c2_2(X0,a401)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1)
| ~ c6_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u3778,negated_conjecture,
( ~ c2_1(X0)
| ~ c4_2(X0,a392)
| c8_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c7_2(X0,a401)
| ~ c6_2(X0,X2) ) ).
cnf(u3486,negated_conjecture,
( ~ c6_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X2)
| ~ c8_2(X0,X2)
| ~ c8_2(X0,X1)
| c2_2(X0,X1)
| c8_1(X0) ) ).
cnf(u4618,negated_conjecture,
( c8_1(X0)
| c7_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c1_2(X0,a434)
| c2_2(X0,X2)
| c4_2(X0,X2)
| c5_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c7_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(u3614,negated_conjecture,
( c8_1(X0)
| c7_2(X0,a391)
| ~ c8_2(X0,a368) ) ).
cnf(u3448,negated_conjecture,
( ~ c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c4_2(X0,a360)
| ~ ndr1_1(X0)
| c4_2(X0,X1)
| ~ c4_2(X0,a359) ) ).
cnf(u4634,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c1_2(X0,a434)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ c6_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c1_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(u3590,negated_conjecture,
( c8_1(X0)
| ~ c4_2(X0,a391)
| ~ c8_2(X0,a368) ) ).
cnf(u3110,negated_conjecture,
( c1_1(X0)
| ~ c4_2(X0,X1)
| ~ c4_2(X0,a392)
| c8_2(X0,X1)
| ~ c2_1(X0) ) ).
cnf(u3611,negated_conjecture,
( c8_1(X0)
| c7_2(X0,a391)
| ~ c8_2(X0,X1)
| c1_2(X0,X1)
| ~ c7_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u3055,negated_conjecture,
~ c8_2(a453,a368) ).
cnf(u3074,negated_conjecture,
~ c3_2(a349,a404) ).
cnf(u4692,negated_conjecture,
~ c7_2(a442,a434) ).
cnf(u3585,negated_conjecture,
( c8_1(X0)
| ndr1_1(X0)
| ~ c8_2(X0,a368) ) ).
cnf(u3188,negated_conjecture,
( ~ c6_1(X0)
| c7_2(X0,a391)
| c8_1(X0) ) ).
cnf(u3000,negated_conjecture,
~ c6_1(a349) ).
cnf(u3503,negated_conjecture,
( ~ c5_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X2)
| c7_2(X0,X2)
| ~ c3_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,a434)
| c2_2(X0,X1) ) ).
cnf(u3054,negated_conjecture,
c4_2(a453,a368) ).
cnf(u3777,negated_conjecture,
( ~ c2_1(X0)
| ~ c4_2(X0,a392)
| c8_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c6_2(X0,a401)
| ~ c6_2(X0,X2) ) ).
cnf(clause210,negated_conjecture,
( ssSkP0(X0)
| ~ c8_2(X0,a340) ) ).
cnf(u4592,negated_conjecture,
( ~ c1_2(a442,X0)
| ~ c7_2(a442,X0)
| c8_2(a442,X0) ) ).
cnf(u4624,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c3_2(X0,a434)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ c6_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c1_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(u4201,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c1_2(X0,X2)
| c7_2(X0,X1)
| c5_2(X0,X1)
| c4_2(X0,a368) ) ).
cnf(u4204,negated_conjecture,
( c8_1(X0)
| c5_2(X0,X2)
| ~ c8_2(X0,X2)
| ~ c8_2(X0,X1)
| c2_2(X0,X1)
| c3_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c7_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(u3776,negated_conjecture,
( c4_1(X0)
| ~ c4_2(X0,a392)
| c8_2(X0,X1)
| ~ c2_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u4610,negated_conjecture,
( c8_1(X0)
| c7_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c3_2(X0,a434)
| c2_2(X0,X2)
| c4_2(X0,X2)
| c5_2(X0,X1)
| c4_2(X0,a368) ) ).
cnf(clause127,negated_conjecture,
( ssSkP1(X0)
| c8_2(X0,a359) ) ).
cnf(u3452,negated_conjecture,
( ~ c6_2(X0,a359)
| c7_2(X0,X1)
| ~ c5_2(X0,a360)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| c4_2(X0,X1) ) ).
cnf(u3458,negated_conjecture,
( c3_2(X0,X1)
| c6_2(X0,X1)
| c6_2(X0,a412)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,a411) ) ).
cnf(u3457,negated_conjecture,
( c3_2(X0,X1)
| c6_2(X0,X1)
| c6_2(X0,a412)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,a411) ) ).
cnf(u3446,negated_conjecture,
( ~ c6_2(X0,a359)
| c7_2(X0,X1)
| ~ c8_2(X0,a360)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| c4_2(X0,X1) ) ).
cnf(u3083,negated_conjecture,
( ~ c2_1(X0)
| c3_2(X0,a390)
| c2_2(X0,a389) ) ).
cnf(u3182,negated_conjecture,
c4_2(a417,a368) ).
cnf(u3088,negated_conjecture,
c1_2(a349,a404) ).
cnf(u3281,negated_conjecture,
( c4_1(X0)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c6_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u3082,negated_conjecture,
( ~ c2_1(X0)
| c3_2(X0,a390)
| c7_2(X0,a389) ) ).
cnf(u3052,negated_conjecture,
~ c8_2(a425,a368) ).
cnf(u4207,negated_conjecture,
( c8_1(X0)
| c5_2(X0,X2)
| ~ c8_2(X0,X2)
| ~ c8_2(X0,X1)
| c2_2(X0,X1)
| c3_2(X0,X1)
| ~ c8_2(X0,a368) ) ).
cnf(clause205,negated_conjecture,
( ssSkP1(X0)
| ~ c4_2(X0,a359) ) ).
cnf(u3059,negated_conjecture,
( ~ c2_1(X0)
| ~ c8_2(X0,a390)
| ~ c6_2(X0,a389) ) ).
cnf(u3459,negated_conjecture,
( c3_2(X0,X1)
| c3_2(X0,a411)
| c6_2(X0,a412)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| c6_2(X0,X1) ) ).
cnf(clause62,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(u3589,negated_conjecture,
( c8_1(X0)
| ~ c4_2(X0,a391)
| c4_2(X0,a368) ) ).
cnf(u3461,negated_conjecture,
( c3_2(X0,X1)
| c6_2(X0,X1)
| c2_2(X0,a412)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,a411) ) ).
cnf(u3112,negated_conjecture,
( ~ c2_1(X0)
| ~ c4_2(X0,X1)
| ~ c4_2(X0,a392)
| c8_2(X0,X1)
| c5_2(X0,a337) ) ).
cnf(u2961,negated_conjecture,
( c4_1(X0)
| ~ c6_1(X0)
| ~ c2_1(X0) ) ).
cnf(clause134,negated_conjecture,
( ssSkP0(X0)
| c6_2(X0,a340) ) ).
cnf(u4275,negated_conjecture,
( ~ c6_1(X0)
| ~ c6_2(X0,X2)
| ~ c8_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c5_2(X0,X2)
| ~ c6_2(X0,a434)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c8_1(X0) ) ).
cnf(clause196,negated_conjecture,
( ssSkP4(X0)
| ~ c7_2(X0,a432) ) ).
cnf(u3612,negated_conjecture,
( c8_1(X0)
| c7_2(X0,a391)
| ~ c8_2(X0,X1)
| c1_2(X0,X1)
| ~ c1_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u4200,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c1_2(X0,X2)
| c7_2(X0,X1)
| c5_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c1_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(u4621,negated_conjecture,
( c8_1(X0)
| c7_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c1_2(X0,a434)
| c2_2(X0,X2)
| c4_2(X0,X2)
| c5_2(X0,X1)
| ~ c8_2(X0,a368) ) ).
cnf(u3029,negated_conjecture,
~ c8_2(a431,a368) ).
cnf(u4626,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c3_2(X0,a434)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ c6_2(X0,X1)
| ~ c8_2(X0,a368) ) ).
cnf(u3445,negated_conjecture,
( ~ c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c8_2(X0,a360)
| ~ ndr1_1(X0)
| c4_2(X0,X1)
| ~ c4_2(X0,a359) ) ).
cnf(u4625,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c3_2(X0,a434)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ c6_2(X0,X1)
| c4_2(X0,a368) ) ).
cnf(u3163,negated_conjecture,
( ~ c6_1(X0)
| ~ c4_2(X0,a391)
| c8_1(X0) ) ).
cnf(u2937,negated_conjecture,
c4_2(a330,a368) ).
cnf(u3037,negated_conjecture,
~ c8_2(a349,a368) ).
cnf(u3455,negated_conjecture,
( c3_2(X0,X1)
| c6_2(X0,X1)
| c8_2(X0,a412)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,a411) ) ).
cnf(u3081,negated_conjecture,
( ~ c2_1(X0)
| c3_2(X0,a390)
| ~ c6_2(X0,a389) ) ).
cnf(u3100,negated_conjecture,
( c4_1(X0)
| ~ c6_2(X0,a401)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1)
| ~ c6_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u4619,negated_conjecture,
( c8_1(X0)
| c7_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c1_2(X0,a434)
| c2_2(X0,X2)
| c4_2(X0,X2)
| c5_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c1_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(u3039,negated_conjecture,
c4_2(a305,a368) ).
cnf(u4616,negated_conjecture,
( c8_1(X0)
| c7_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c6_2(X0,a434)
| c2_2(X0,X2)
| c4_2(X0,X2)
| c5_2(X0,X1)
| ~ c8_2(X0,a368) ) ).
cnf(u4623,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c3_2(X0,a434)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ c6_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c7_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(u2935,negated_conjecture,
~ c8_2(a330,a368) ).
cnf(u2993,negated_conjecture,
c4_2(a298,a368) ).
cnf(u4196,negated_conjecture,
( c3_2(X0,a411)
| c2_2(X0,a412)
| c7_2(X0,a411)
| ~ ndr1_1(X0)
| c6_2(X0,a411) ) ).
cnf(clause211,negated_conjecture,
( ssSkP0(X0)
| ~ c3_2(X0,a340) ) ).
cnf(u4628,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c6_2(X0,a434)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ c6_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c7_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(u2994,negated_conjecture,
~ c8_2(a298,a368) ).
cnf(u4199,negated_conjecture,
( c8_1(X0)
| ~ c8_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c1_2(X0,X2)
| c7_2(X0,X1)
| c5_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c7_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(u3063,negated_conjecture,
( ~ c2_1(X0)
| ~ c7_2(X0,a390)
| ~ c6_2(X0,a389) ) ).
cnf(u4615,negated_conjecture,
( c8_1(X0)
| c7_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c6_2(X0,a434)
| c2_2(X0,X2)
| c4_2(X0,X2)
| c5_2(X0,X1)
| c4_2(X0,a368) ) ).
cnf(clause122,negated_conjecture,
( ssSkP2(X0)
| c2_2(X0,a389) ) ).
cnf(u4613,negated_conjecture,
( c8_1(X0)
| c7_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ c6_2(X0,a434)
| c2_2(X0,X2)
| c4_2(X0,X2)
| c5_2(X0,X1)
| ~ c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c7_2(X0,a437)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X3) ) ).
cnf(u3504,negated_conjecture,
( ~ c5_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X2)
| c7_2(X0,X2)
| ~ c3_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c6_2(X0,a434)
| c2_2(X0,X1) ) ).
cnf(u3526,negated_conjecture,
( ~ c5_1(X0)
| c4_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X2)
| ~ c5_2(X0,X2)
| ~ c6_2(X0,a434)
| c5_2(X0,X1) ) ).
cnf(u3065,negated_conjecture,
( ~ c2_1(X0)
| ~ c7_2(X0,a390)
| c2_2(X0,a389) ) ).
cnf(clause117,negated_conjecture,
( ssSkP3(X0)
| c3_2(X0,a411) ) ).
cnf(u3603,negated_conjecture,
( c8_1(X0)
| c8_2(X0,a391)
| c4_2(X0,a368) ) ).
cnf(u4104,negated_conjecture,
( c3_2(X0,a411)
| c8_2(X0,a412)
| c7_2(X0,a411)
| ~ ndr1_1(X0)
| c6_2(X0,a411) ) ).
cnf(clause111,negated_conjecture,
( ssSkP4(X0)
| c6_2(X0,a432) ) ).
cnf(u3061,negated_conjecture,
( ~ c2_1(X0)
| ~ c8_2(X0,a390)
| c2_2(X0,a389) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN546-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n016.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:33:00 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.30 % (3748082)Will run a generic schedule for satisfiability detection.
% 0.21/0.30 % (3748091)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4170423415:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.21/0.30 % (3748088)% WARNING: option uhcvi not known.
% 0.21/0.30 % (3748087)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2152828544_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.30 % (3748088)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=73341203:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.30 % (3748089)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1151782084:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.30 % (3748090)dis+10_1_sil=32000:sp=arity:random_seed=459589202:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.30 % (3748092)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2165349915:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.30 % (3748093)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=280967255:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.21/0.30 % Detected minimum model sizes of [1]
% 0.21/0.30 % Detected maximum model sizes of [158]
% 0.21/0.30 % TRYING [1]
% 0.21/0.30 % (3748091) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3748082-3748091"...
% 0.21/0.30 % TRYING [2]
% 0.21/0.30 % (3748091)...printing done.
% 0.21/0.30 % SZS status Satisfiable for theBenchmark
% 0.21/0.30 % SZS output start Saturation.
% See solution above
% 0.21/0.31 % SZS output start Definitions and Model Updates.
% 0.21/0.31 for all groundings,
% 0.21/0.31 whenever ~ssSkC7 | ndr1_0 | c4_0 is false, set ~ssSkC7 to true
% 0.21/0.31 for all groundings,
% 0.21/0.31 whenever ndr1_0 | ssSkC20 is false, set ssSkC20 to true
% 0.21/0.31 for all groundings,
% 0.21/0.31 whenever ndr1_0 | ssSkC13 is false, set ssSkC13 to true
% 0.21/0.31 for all groundings,
% 0.21/0.31 whenever ~ssSkC18 | ndr1_0 | c2_0 is false, set ~ssSkC18 to true
% 0.21/0.31 for all groundings,
% 0.21/0.31 whenever ndr1_0 | ssSkC15 is false, set ssSkC15 to true
% 0.21/0.31 for all groundings,
% 0.21/0.31 whenever ndr1_0 | ssSkC16 is false, set ssSkC16 to true
% 0.21/0.31 for all groundings,
% 0.21/0.31 whenever ndr1_0 | ssSkC2 is false, set ssSkC2 to true
% 0.21/0.31 for all groundings,
% 0.21/0.31 whenever ndr1_0 | ssSkC8 is false, set ssSkC8 to true
% 0.21/0.31 for all groundings,
% 0.21/0.31 whenever ~ssSkC23 | ~c3_0 | ndr1_0 is false, set ~ssSkC23 to true
% 0.21/0.31 for all groundings,
% 0.21/0.31 whenever ndr1_1(X0) | ssSkP1(X0) is false, set ssSkP1(X0) to true
% 0.21/0.31 for all groundings,
% 0.21/0.31 whenever ndr1_1(X0) | ssSkP3(X0) is false, set ssSkP3(X0) to true
% 0.21/0.31 for all groundings,
% 0.21/0.31 whenever ndr1_1(X0) | ssSkP4(X0) is false, set ssSkP4(X0) to true
% 0.21/0.31 for all groundings,
% 0.21/0.31 whenever ~ssSkC6 | ~c3_0 | ndr1_0 is false, set ~ssSkC6 to true
% 0.21/0.31 for all groundings,
% 0.21/0.31 whenever ~ssSkC17 | ~c2_0 | ndr1_0 is false, set ~ssSkC17 to true
% 0.21/0.31 % SZS output end Definitions and Model Updates.
% 0.21/0.31 % (3748091)------------------------------
% 0.21/0.31 % (3748091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.31 % (3748091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.31 % (3748091)CaDiCaL version: 2.1.3
% 0.21/0.31 % (3748091)Termination reason: Satisfiable
% 0.21/0.31 % (3748091)Time elapsed: 0.036 s
% 0.21/0.31 % (3748091)Peak memory usage: 15 MB
% 0.21/0.31 % (3748091)Instructions burned: 117 (million)
% 0.21/0.31 % (3748082)Success in time 0.076 s
% 0.21/0.31 % Vampire exiting
%------------------------------------------------------------------------------