%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN421-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 : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:50:34 PM UTC 2026
% Result : Satisfiable 4.19s 1.52s
% Output : Saturation 5.85s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u550,negated_conjecture,
~ c6_0 ).
cnf(u2063,negated_conjecture,
ndr1_0 ).
cnf(u567,negated_conjecture,
~ ndr1_1(a566) ).
cnf(u1389,negated_conjecture,
ssSkC23 ).
cnf(u870,negated_conjecture,
c4_0 ).
cnf(u597,negated_conjecture,
( c3_1(X0)
| c1_1(X0)
| ~ ndr1_1(X0)
| c1_2(X0,X2)
| c10_2(X0,X2)
| c6_2(X0,X2) ) ).
cnf(u601,negated_conjecture,
~ c3_1(a566) ).
cnf(u605,negated_conjecture,
~ c10_0 ).
cnf(u608,negated_conjecture,
~ c8_0 ).
cnf(u626,negated_conjecture,
ssSkC2 ).
cnf(u637,negated_conjecture,
~ c7_0 ).
cnf(u659,negated_conjecture,
~ c9_0 ).
cnf(u842,negated_conjecture,
c1_0 ).
cnf(u676,negated_conjecture,
( c7_1(X0)
| ~ c2_2(X0,X1)
| c2_2(X0,X2)
| c10_2(X0,X2)
| c4_2(X0,X1)
| c3_2(X0,X1)
| ~ c4_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u683,negated_conjecture,
( ~ c2_1(X0)
| c7_1(X0)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u1282,negated_conjecture,
ssSkC22 ).
cnf(u729,negated_conjecture,
~ c1_2(a502,a503) ).
cnf(u1746,negated_conjecture,
~ ssSkC24 ).
cnf(u748,negated_conjecture,
( ~ ssSkP10(X0)
| ~ c10_2(X0,a568)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u766,negated_conjecture,
~ c3_0 ).
cnf(u781,negated_conjecture,
~ c9_1(a502) ).
cnf(u785,negated_conjecture,
~ c5_1(a502) ).
cnf(u789,negated_conjecture,
c8_2(a502,a503) ).
cnf(u814,negated_conjecture,
~ ssSkC29 ).
cnf(u1295,negated_conjecture,
ssSkC28 ).
cnf(u829,negated_conjecture,
( ~ c6_1(X0)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c6_2(X0,a604)
| ~ ndr1_1(X0) ) ).
cnf(u1111,negated_conjecture,
ssSkC32 ).
cnf(u1300,negated_conjecture,
ssSkC31 ).
cnf(u839,negated_conjecture,
( ~ ssSkP10(X0)
| c9_2(X0,a568)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u891,negated_conjecture,
ssSkC9 ).
cnf(u868,negated_conjecture,
ndr1_1(a502) ).
cnf(u885,negated_conjecture,
( ~ c6_1(X0)
| c10_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u889,negated_conjecture,
( ~ c6_1(X0)
| c3_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u898,negated_conjecture,
ssSkC10 ).
cnf(u1854,negated_conjecture,
~ ssSkC11 ).
cnf(u908,negated_conjecture,
( ~ ssSkP4(X0)
| c3_2(X0,a508)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u912,negated_conjecture,
( ~ ssSkP4(X0)
| c2_2(X0,a508)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u916,negated_conjecture,
( ~ ssSkP4(X0)
| c7_2(X0,a508)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u1022,negated_conjecture,
~ ssSkC21 ).
cnf(u923,negated_conjecture,
( ~ c5_1(X0)
| c2_2(X0,X1)
| c10_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,a548) ) ).
cnf(u927,negated_conjecture,
( ~ c5_1(X0)
| c2_2(X0,X1)
| c10_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c6_2(X0,a548) ) ).
cnf(u932,negated_conjecture,
c5_0 ).
cnf(u939,negated_conjecture,
~ c2_0 ).
cnf(u946,negated_conjecture,
( c10_1(X0)
| ~ ndr1_1(X0)
| c7_2(X0,X1)
| c2_2(X0,X1)
| c10_2(X0,X1)
| ~ c9_2(X0,a459) ) ).
cnf(u972,negated_conjecture,
( c9_2(X0,a548)
| ~ ndr1_1(X0)
| c2_2(X0,X1)
| c10_2(X0,X1)
| c3_2(X0,X1)
| ~ c5_1(X0) ) ).
cnf(u1574,negated_conjecture,
~ ssSkC27 ).
cnf(u979,negated_conjecture,
( c10_1(X0)
| ~ c1_2(X0,X1)
| ~ c7_2(X0,a589)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u983,negated_conjecture,
( c10_1(X0)
| ~ c1_2(X0,X1)
| ~ c10_2(X0,a589)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u987,negated_conjecture,
( c10_1(X0)
| ~ c1_2(X0,X1)
| ~ c2_2(X0,a589)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u991,negated_conjecture,
( c10_1(X0)
| ~ ndr1_1(X0)
| c8_2(X0,a459)
| c7_2(X0,X1)
| c2_2(X0,X1)
| c10_2(X0,X1) ) ).
cnf(u995,negated_conjecture,
( c10_1(X0)
| ~ ndr1_1(X0)
| c2_2(X0,a459)
| c7_2(X0,X1)
| c2_2(X0,X1)
| c10_2(X0,X1) ) ).
cnf(u2411,negated_conjecture,
ndr1_1(a481) ).
cnf(u1007,negated_conjecture,
( ~ c5_2(a481,X0)
| ~ c7_2(a481,X0)
| ~ c3_2(a481,X0) ) ).
cnf(u1995,negated_conjecture,
ssSkC6 ).
cnf(u1014,negated_conjecture,
( ~ ssSkP6(X0)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u1154,negated_conjecture,
~ ssSkC12 ).
cnf(u1029,negated_conjecture,
( ~ ssSkP5(X0)
| c2_2(X0,a512)
| c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u1033,negated_conjecture,
( ~ ssSkP5(X0)
| c1_2(X0,a512)
| c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u1037,negated_conjecture,
( ~ ssSkP5(X0)
| c7_2(X0,a512)
| c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u2652,negated_conjecture,
ndr1_1(a470) ).
cnf(u1051,negated_conjecture,
( c8_2(a470,X0)
| ~ c4_2(a470,X0)
| ~ c5_2(a470,X0) ) ).
cnf(u1093,negated_conjecture,
ssSkC3 ).
cnf(u1990,negated_conjecture,
ssSkC4 ).
cnf(u1068,negated_conjecture,
( ~ ssSkP6(X0)
| c6_2(X0,a530)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u1072,negated_conjecture,
( ~ ssSkP6(X0)
| c9_2(X0,a530)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u1077,negated_conjecture,
~ ndr1_1(a550) ).
cnf(u1103,negated_conjecture,
ssSkC30 ).
cnf(u1166,negated_conjecture,
( ~ c2_1(X0)
| ~ c3_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(u1354,negated_conjecture,
ssSkC15 ).
cnf(u1173,negated_conjecture,
( ~ c2_1(X0)
| ~ c2_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(u1177,negated_conjecture,
( ~ c2_1(X0)
| ~ c4_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(u2357,negated_conjecture,
ssSkC18 ).
cnf(u1190,negated_conjecture,
~ ssSkC17 ).
cnf(u1215,negated_conjecture,
( ~ c5_1(X0)
| ~ c1_1(X0)
| ~ c6_2(X0,a450) ) ).
cnf(u1517,negated_conjecture,
ssSkC0 ).
cnf(u1222,negated_conjecture,
( ~ c8_2(X0,a450)
| ~ c1_1(X0)
| ~ c5_1(X0) ) ).
cnf(u2303,negated_conjecture,
ssSkC1 ).
cnf(u1261,negated_conjecture,
( ~ c8_1(X0)
| c7_2(X0,a574)
| ~ c6_1(X0) ) ).
cnf(u1265,negated_conjecture,
( ~ c8_1(X0)
| c4_2(X0,a574)
| ~ c6_1(X0) ) ).
cnf(u1269,negated_conjecture,
( ~ c8_1(X0)
| c6_2(X0,a574)
| ~ c6_1(X0) ) ).
cnf(u1314,negated_conjecture,
( c9_2(X0,a450)
| ~ c5_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1332,negated_conjecture,
( ~ c2_1(X0)
| ndr1_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1344,negated_conjecture,
( ~ c8_1(X0)
| ndr1_1(X0)
| ~ c6_1(X0) ) ).
cnf(u1369,negated_conjecture,
ssSkC16 ).
cnf(u1380,negated_conjecture,
ssSkC20 ).
cnf(u1426,negated_conjecture,
ssSkC8 ).
cnf(u1436,negated_conjecture,
ssSkC13 ).
cnf(u1446,negated_conjecture,
( ~ c5_1(X0)
| ndr1_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1458,negated_conjecture,
( c2_1(X0)
| ~ c10_2(X0,a545)
| c7_1(X0) ) ).
cnf(u1584,negated_conjecture,
ssSkC19 ).
cnf(u1465,negated_conjecture,
( c2_1(X0)
| ~ c4_2(X0,a545)
| c7_1(X0) ) ).
cnf(u1790,negated_conjecture,
~ ssSkC5 ).
cnf(u1478,negated_conjecture,
( c10_1(X0)
| c9_1(X0)
| ~ c6_2(X0,a474) ) ).
cnf(u1491,negated_conjecture,
( c2_1(X0)
| c6_1(X0)
| ~ c3_2(X0,a536) ) ).
cnf(u1495,negated_conjecture,
( c2_1(X0)
| c6_1(X0)
| ~ c4_2(X0,a536) ) ).
cnf(u1531,negated_conjecture,
( c7_1(X0)
| ~ c6_1(X0)
| c5_1(X0) ) ).
cnf(u1543,negated_conjecture,
( c10_1(X0)
| c9_1(X0)
| c7_2(X0,a474) ) ).
cnf(u1547,negated_conjecture,
( c10_1(X0)
| c9_1(X0)
| c8_2(X0,a474) ) ).
cnf(u1555,negated_conjecture,
( c2_1(X0)
| c6_1(X0)
| c9_2(X0,a536) ) ).
cnf(u1591,negated_conjecture,
( c2_1(X0)
| ndr1_1(X0)
| c7_1(X0) ) ).
cnf(u1599,negated_conjecture,
( c10_1(X0)
| c9_1(X0)
| ndr1_1(X0) ) ).
cnf(u1603,negated_conjecture,
( c2_1(X0)
| c6_1(X0)
| ndr1_1(X0) ) ).
cnf(u1683,negated_conjecture,
~ c6_2(a494,a495) ).
cnf(u1688,negated_conjecture,
~ c9_2(a494,a495) ).
cnf(u1806,negated_conjecture,
~ c7_2(a481,a483) ).
cnf(u1822,negated_conjecture,
~ c5_2(a489,a490) ).
cnf(u2332,negated_conjecture,
ssSkC7 ).
cnf(u1829,negated_conjecture,
~ c1_2(a489,a490) ).
cnf(u1833,negated_conjecture,
~ c2_2(a489,a490) ).
cnf(u1837,negated_conjecture,
~ c1_1(a494) ).
cnf(u1841,negated_conjecture,
~ c4_1(a494) ).
cnf(u1845,negated_conjecture,
c10_2(a494,a495) ).
cnf(u1875,negated_conjecture,
~ c7_2(a519,a520) ).
cnf(u1880,negated_conjecture,
~ c5_2(a519,a520) ).
cnf(u1944,negated_conjecture,
~ c8_2(a578,a579) ).
cnf(u1955,negated_conjecture,
~ ssSkC26 ).
cnf(u2014,negated_conjecture,
ssSkC14 ).
cnf(u2021,negated_conjecture,
ssSkC25 ).
cnf(u2077,negated_conjecture,
~ c2_1(a470) ).
cnf(u2093,negated_conjecture,
c6_2(a481,a482) ).
cnf(u2097,negated_conjecture,
c10_2(a481,a482) ).
cnf(u2101,negated_conjecture,
c4_2(a481,a482) ).
cnf(u2105,negated_conjecture,
c10_2(a481,a483) ).
cnf(u2109,negated_conjecture,
c5_2(a481,a483) ).
cnf(u2113,negated_conjecture,
~ c10_1(a489) ).
cnf(u2117,negated_conjecture,
~ c6_1(a489) ).
cnf(u2121,negated_conjecture,
ndr1_1(a494) ).
cnf(u2139,negated_conjecture,
~ c8_1(a519) ).
cnf(u2143,negated_conjecture,
c9_2(a519,a520) ).
cnf(u2184,negated_conjecture,
~ c1_1(a541) ).
cnf(u2188,negated_conjecture,
~ c9_1(a541) ).
cnf(u2244,negated_conjecture,
~ c6_1(a577) ).
cnf(u2249,negated_conjecture,
~ c8_1(a577) ).
cnf(u2253,negated_conjecture,
~ c1_1(a577) ).
cnf(u2257,negated_conjecture,
~ c8_1(a578) ).
cnf(u2261,negated_conjecture,
c2_2(a578,a579) ).
cnf(u2265,negated_conjecture,
c7_2(a578,a579) ).
cnf(u2377,negated_conjecture,
~ c5_1(a585) ).
cnf(u2382,negated_conjecture,
~ c8_1(a592) ).
cnf(u2404,negated_conjecture,
c8_1(a470) ).
cnf(u2417,negated_conjecture,
ndr1_1(a489) ).
cnf(u2431,negated_conjecture,
c9_1(a519) ).
cnf(u2435,negated_conjecture,
ndr1_1(a519) ).
cnf(u2453,negated_conjecture,
c10_1(a541) ).
cnf(u2462,negated_conjecture,
c9_1(a550) ).
cnf(u2477,negated_conjecture,
c1_1(a578) ).
cnf(u2481,negated_conjecture,
ndr1_1(a578) ).
cnf(u2584,negated_conjecture,
c9_1(a585) ).
cnf(u2588,negated_conjecture,
c9_1(a592) ).
cnf(u2651,negated_conjecture,
~ c6_1(a470) ).
cnf(u2659,negated_conjecture,
c7_1(a470) ).
cnf(u2676,negated_conjecture,
~ c5_1(a577) ).
cnf(u2699,negated_conjecture,
~ c6_2(a489,a474) ).
cnf(u2702,negated_conjecture,
c9_1(a489) ).
cnf(u2711,negated_conjecture,
~ c3_2(a470,a536) ).
cnf(u2720,negated_conjecture,
~ c4_2(a470,a536) ).
cnf(u2735,negated_conjecture,
c9_2(a470,a536) ).
cnf(u2741,negated_conjecture,
~ c5_1(a470) ).
cnf(u2756,negated_conjecture,
~ c7_2(a489,a589) ).
cnf(u2764,negated_conjecture,
~ c10_2(a489,a589) ).
cnf(u2769,negated_conjecture,
~ c2_2(a489,a589) ).
cnf(u2796,negated_conjecture,
~ c5_1(a489) ).
cnf(u2859,negated_conjecture,
~ c9_2(a489,a459) ).
cnf(u2873,negated_conjecture,
c8_2(a489,a459) ).
cnf(u2882,negated_conjecture,
c2_2(a489,a459) ).
cnf(u2896,negated_conjecture,
c3_2(a481,a529) ).
cnf(u2899,negated_conjecture,
c1_2(a481,a483) ).
cnf(u2906,negated_conjecture,
c1_2(a481,a482) ).
cnf(u2917,negated_conjecture,
c6_2(a494,a530) ).
cnf(u2929,negated_conjecture,
~ c1_2(a494,a530) ).
cnf(u2988,negated_conjecture,
~ c6_2(a489,a589) ).
cnf(u3037,negated_conjecture,
~ c6_2(a489,a490) ).
cnf(u3065,negated_conjecture,
~ c3_2(a502,a503) ).
cnf(u2967,negated_conjecture,
( c10_2(X0,X1)
| c6_2(X0,a507)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511) ) ).
cnf(u2973,negated_conjecture,
( c3_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c1_2(X0,X1)
| c6_2(X0,a507) ) ).
cnf(u2954,negated_conjecture,
( c4_2(X0,X1)
| c2_2(X0,a508)
| c6_2(X0,a507)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u2864,negated_conjecture,
( c9_2(X0,a536)
| ~ c3_2(X0,a528)
| ~ c5_1(X0)
| c3_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u2886,negated_conjecture,
( ~ c10_2(X0,X1)
| c6_2(X0,a530)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| c3_2(X0,a529) ) ).
cnf(clause75,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(u3159,negated_conjecture,
( ~ c4_2(X0,a507)
| c3_2(X0,a508)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c10_2(X0,X1)
| c6_2(X0,a511) ) ).
cnf(clause138,negated_conjecture,
( ssSkP5(X0)
| c6_2(X0,a511) ) ).
cnf(u2844,negated_conjecture,
( c9_2(X0,a536)
| ~ c4_2(X0,a528)
| ~ c5_1(X0)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c6_2(X0,a604)
| ~ ndr1_1(X0) ) ).
cnf(u2692,negated_conjecture,
( c7_1(X0)
| ~ c4_2(X0,a545)
| ~ c4_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(u3144,negated_conjecture,
( ~ c5_2(X0,a511)
| c7_2(X0,a512)
| c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(clause153,negated_conjecture,
( ssSkP0(X0)
| c4_2(X0,a451) ) ).
cnf(u2842,negated_conjecture,
( c9_2(X0,a536)
| ~ c4_2(X0,a528)
| ~ c5_1(X0)
| c3_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u3020,negated_conjecture,
( c3_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c6_2(X0,a507) ) ).
cnf(u3002,negated_conjecture,
( c3_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c6_2(X0,a507) ) ).
cnf(u2961,negated_conjecture,
( c10_2(X0,X1)
| c6_2(X0,a507)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511) ) ).
cnf(clause62,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(u2813,negated_conjecture,
( ~ c5_1(X0)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,a536)
| ~ c4_2(X0,a528)
| c3_2(X0,a604) ) ).
cnf(u3068,negated_conjecture,
( c7_2(X0,a508)
| c3_2(X0,a507)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(clause151,negated_conjecture,
( ssSkP1(X0)
| c1_2(X0,a452) ) ).
cnf(u3154,negated_conjecture,
( ~ c4_2(X0,a507)
| c2_2(X0,a508)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c10_2(X0,X1)
| c6_2(X0,a511) ) ).
cnf(u3107,negated_conjecture,
( c2_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c3_2(X0,a507) ) ).
cnf(clause142,negated_conjecture,
( ssSkP3(X0)
| c9_2(X0,a497) ) ).
cnf(clause237,negated_conjecture,
( ssSkP7(X0)
| ~ c10_2(X0,a531) ) ).
cnf(u2808,negated_conjecture,
( ~ c5_1(X0)
| ~ c2_2(X0,a528)
| ~ c3_2(X0,a536)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c6_2(X0,a604)
| ~ ndr1_1(X0) ) ).
cnf(clause243,negated_conjecture,
( ssSkP3(X0)
| ~ c4_2(X0,a497) ) ).
cnf(u2866,negated_conjecture,
( c9_2(X0,a536)
| ~ c3_2(X0,a528)
| ~ c5_1(X0)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c6_2(X0,a604)
| ~ ndr1_1(X0) ) ).
cnf(clause129,negated_conjecture,
( ssSkP7(X0)
| c5_2(X0,a531) ) ).
cnf(u3145,negated_conjecture,
( ~ c5_2(X0,a511)
| c1_2(X0,a512)
| c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u2714,negated_conjecture,
( c6_1(X0)
| ~ c4_2(X0,a536)
| ~ c4_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(u2850,negated_conjecture,
( c9_2(X0,a536)
| ~ c2_2(X0,a528)
| ~ c5_1(X0)
| c3_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u2950,negated_conjecture,
( c7_2(X0,a512)
| c6_2(X0,a511)
| c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u3021,negated_conjecture,
( c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c6_2(X0,a507)
| c2_2(X0,a529) ) ).
cnf(clause51,negated_conjecture,
( ssSkP9(X0)
| ndr1_1(X0) ) ).
cnf(u3104,negated_conjecture,
( c3_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c1_2(X0,X1)
| c3_2(X0,a507) ) ).
cnf(clause242,negated_conjecture,
( ssSkP4(X0)
| ~ c4_2(X0,a507) ) ).
cnf(u2807,negated_conjecture,
( ~ c5_1(X0)
| ~ c2_2(X0,a528)
| ~ c3_2(X0,a536)
| c10_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(clause246,negated_conjecture,
( ssSkP2(X0)
| ~ c9_2(X0,a486) ) ).
cnf(u2888,negated_conjecture,
( c9_2(X0,a530)
| c2_2(X0,a529)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u2831,negated_conjecture,
( ~ c5_1(X0)
| ~ c2_2(X0,a528)
| ~ c4_2(X0,a536)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c6_2(X0,a604)
| ~ ndr1_1(X0) ) ).
cnf(u2822,negated_conjecture,
( ~ c5_1(X0)
| ~ c4_2(X0,a528)
| ~ c4_2(X0,a536)
| c3_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u2974,negated_conjecture,
( c3_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c6_2(X0,a507) ) ).
cnf(clause55,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(u3069,negated_conjecture,
( c4_2(X0,X1)
| c2_2(X0,a508)
| c3_2(X0,a507)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(clause235,negated_conjecture,
( ssSkP9(X0)
| ~ c2_2(X0,a564) ) ).
cnf(u3141,negated_conjecture,
( c9_2(X0,a568)
| ~ c3_2(X0,a567)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u2829,negated_conjecture,
( ~ c5_1(X0)
| ~ c2_2(X0,a528)
| ~ c4_2(X0,a536)
| c3_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u3079,negated_conjecture,
( c10_2(X0,X1)
| c3_2(X0,a507)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511) ) ).
cnf(clause241,negated_conjecture,
( ssSkP5(X0)
| ~ c5_2(X0,a511) ) ).
cnf(clause60,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u2786,negated_conjecture,
( c7_1(X0)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c4_2(X0,a545) ) ).
cnf(u2715,negated_conjecture,
( c6_1(X0)
| ~ c4_2(X0,a536)
| ~ c2_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(clause126,negated_conjecture,
( ssSkP8(X0)
| c5_2(X0,a542) ) ).
cnf(u3022,negated_conjecture,
( c2_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c6_2(X0,a507) ) ).
cnf(u2729,negated_conjecture,
( c6_1(X0)
| c9_2(X0,a536)
| ~ c4_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(u2781,negated_conjecture,
( c7_1(X0)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1)
| c6_1(X0)
| ~ c4_2(X0,a536) ) ).
cnf(u3139,negated_conjecture,
( ~ c5_2(X0,X1)
| ~ c10_2(X0,a568)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c2_2(X0,a567) ) ).
cnf(u2836,negated_conjecture,
( ~ c5_1(X0)
| ~ c3_2(X0,a528)
| ~ c4_2(X0,a536)
| c3_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(clause238,negated_conjecture,
( ssSkP7(X0)
| ~ c6_2(X0,a531) ) ).
cnf(u2812,negated_conjecture,
( ~ c5_1(X0)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,a536)
| ~ c2_2(X0,a528)
| c3_2(X0,a604) ) ).
cnf(u3012,negated_conjecture,
( c2_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c1_2(X0,X1)
| c6_2(X0,a507) ) ).
cnf(u2837,negated_conjecture,
( ~ c5_1(X0)
| ~ c3_2(X0,a528)
| ~ c4_2(X0,a536)
| c10_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u3010,negated_conjecture,
( c3_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c1_2(X0,X1)
| c6_2(X0,a507) ) ).
cnf(u2953,negated_conjecture,
( c7_2(X0,a508)
| c6_2(X0,a507)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u2805,negated_conjecture,
( ~ c5_1(X0)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,a536)
| ~ c4_2(X0,a528)
| c10_2(X0,a604) ) ).
cnf(u2851,negated_conjecture,
( c9_2(X0,a536)
| ~ c2_2(X0,a528)
| ~ c5_1(X0)
| c10_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u3097,negated_conjecture,
( c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c3_2(X0,a507)
| c2_2(X0,a529) ) ).
cnf(u3106,negated_conjecture,
( c2_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c1_2(X0,X1)
| c3_2(X0,a507) ) ).
cnf(u3003,negated_conjecture,
( c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c6_2(X0,a507)
| c2_2(X0,a529) ) ).
cnf(u3089,negated_conjecture,
( c2_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c3_2(X0,a507) ) ).
cnf(clause154,negated_conjecture,
( ssSkP0(X0)
| c7_2(X0,a451) ) ).
cnf(clause125,negated_conjecture,
( ssSkP8(X0)
| c1_2(X0,a542) ) ).
cnf(u2976,negated_conjecture,
( c2_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c6_2(X0,a507) ) ).
cnf(u3113,negated_conjecture,
( c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c3_2(X0,a507)
| c3_2(X0,a529) ) ).
cnf(u2706,negated_conjecture,
( c6_1(X0)
| ~ c3_2(X0,a536)
| ~ c2_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(u2955,negated_conjecture,
( c4_2(X0,X1)
| c3_2(X0,a508)
| c6_2(X0,a507)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u3070,negated_conjecture,
( c4_2(X0,X1)
| c3_2(X0,a508)
| c3_2(X0,a507)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u2885,negated_conjecture,
( c9_2(X0,a530)
| c3_2(X0,a529)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u3013,negated_conjecture,
( c2_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c6_2(X0,a507) ) ).
cnf(u3142,negated_conjecture,
( ~ c5_2(X0,X1)
| ~ c10_2(X0,a568)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,a567) ) ).
cnf(u2962,negated_conjecture,
( c10_2(X0,X1)
| c6_2(X0,a507)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511) ) ).
cnf(clause130,negated_conjecture,
( ssSkP6(X0)
| c3_2(X0,a529) ) ).
cnf(u2848,negated_conjecture,
( c9_2(X0,a568)
| c6_2(X0,a567)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u2823,negated_conjecture,
( ~ c5_1(X0)
| ~ c4_2(X0,a528)
| ~ c4_2(X0,a536)
| c10_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u2730,negated_conjecture,
( c6_1(X0)
| c9_2(X0,a536)
| ~ c2_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(u2849,negated_conjecture,
( ~ c5_2(X0,X1)
| ~ c10_2(X0,a568)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| c6_2(X0,a567) ) ).
cnf(u3019,negated_conjecture,
( c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c6_2(X0,a507)
| c3_2(X0,a529) ) ).
cnf(u3001,negated_conjecture,
( c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c6_2(X0,a507)
| c3_2(X0,a529) ) ).
cnf(u3098,negated_conjecture,
( c2_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c3_2(X0,a507) ) ).
cnf(clause236,negated_conjecture,
( ssSkP8(X0)
| ~ c6_2(X0,a542) ) ).
cnf(u3147,negated_conjecture,
( c7_2(X0,a508)
| ~ c4_2(X0,a507)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u2689,negated_conjecture,
( c7_1(X0)
| ~ c10_2(X0,a545)
| ~ c3_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(clause74,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u2664,negated_conjecture,
( c6_1(X0)
| ndr1_1(X0)
| ~ c5_1(X0) ) ).
cnf(u2947,negated_conjecture,
( c9_2(X0,a530)
| c7_2(X0,a529)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u3080,negated_conjecture,
( c10_2(X0,X1)
| c3_2(X0,a507)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511) ) ).
cnf(u2780,negated_conjecture,
( c7_1(X0)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1)
| c6_1(X0)
| ~ c3_2(X0,a536) ) ).
cnf(u2838,negated_conjecture,
( ~ c5_1(X0)
| ~ c3_2(X0,a528)
| ~ c4_2(X0,a536)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c6_2(X0,a604)
| ~ ndr1_1(X0) ) ).
cnf(u2707,negated_conjecture,
( c6_1(X0)
| ~ c3_2(X0,a536)
| ~ c3_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(clause251,negated_conjecture,
( ssSkP1(X0)
| ~ c2_2(X0,a452) ) ).
cnf(u3116,negated_conjecture,
( c2_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c3_2(X0,a507) ) ).
cnf(u2815,negated_conjecture,
( ~ c5_1(X0)
| ~ c3_2(X0,a528)
| ~ c3_2(X0,a536)
| c3_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(clause232,negated_conjecture,
( ssSkP10(X0)
| ~ c2_2(X0,a567) ) ).
cnf(clause65,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u3115,negated_conjecture,
( c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c3_2(X0,a507)
| c2_2(X0,a529) ) ).
cnf(u3095,negated_conjecture,
( c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c3_2(X0,a507)
| c3_2(X0,a529) ) ).
cnf(u2687,negated_conjecture,
( c7_1(X0)
| ~ c10_2(X0,a545)
| ~ c4_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(clause52,negated_conjecture,
( ssSkP8(X0)
| ndr1_1(X0) ) ).
cnf(u2975,negated_conjecture,
( c2_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c1_2(X0,X1)
| c6_2(X0,a507) ) ).
cnf(u3105,negated_conjecture,
( c3_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c3_2(X0,a507) ) ).
cnf(u2966,negated_conjecture,
( c10_2(X0,X1)
| c6_2(X0,a507)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511) ) ).
cnf(u3146,negated_conjecture,
( ~ c5_2(X0,a511)
| c2_2(X0,a512)
| c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(clause50,negated_conjecture,
( ssSkP10(X0)
| ndr1_1(X0) ) ).
cnf(clause152,negated_conjecture,
( ssSkP1(X0)
| c9_2(X0,a452) ) ).
cnf(u2852,negated_conjecture,
( c9_2(X0,a536)
| ~ c2_2(X0,a528)
| ~ c5_1(X0)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c6_2(X0,a604)
| ~ ndr1_1(X0) ) ).
cnf(u2816,negated_conjecture,
( ~ c5_1(X0)
| ~ c3_2(X0,a528)
| ~ c3_2(X0,a536)
| c10_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u3004,negated_conjecture,
( c2_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c6_2(X0,a507) ) ).
cnf(u2790,negated_conjecture,
( ~ c5_1(X0)
| ~ c4_2(X0,a528)
| ~ c3_2(X0,a536)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c6_2(X0,a604)
| ~ ndr1_1(X0) ) ).
cnf(u2951,negated_conjecture,
( ~ c4_2(X0,X1)
| c1_2(X0,a512)
| c10_2(X0,X1)
| ~ ndr1_1(X0)
| c6_2(X0,a511) ) ).
cnf(clause141,negated_conjecture,
( ssSkP3(X0)
| c2_2(X0,a497) ) ).
cnf(u2843,negated_conjecture,
( c9_2(X0,a536)
| ~ c4_2(X0,a528)
| ~ c5_1(X0)
| c10_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u2787,negated_conjecture,
( c7_1(X0)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c10_2(X0,a545) ) ).
cnf(u2817,negated_conjecture,
( ~ c5_1(X0)
| ~ c3_2(X0,a528)
| ~ c3_2(X0,a536)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c6_2(X0,a604)
| ~ ndr1_1(X0) ) ).
cnf(clause132,negated_conjecture,
( ssSkP6(X0)
| c7_2(X0,a529) ) ).
cnf(u2693,negated_conjecture,
( c7_1(X0)
| ~ c4_2(X0,a545)
| ~ c2_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(u2890,negated_conjecture,
( ~ c10_2(X0,X1)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| ~ ndr1_1(X0)
| c2_2(X0,a529) ) ).
cnf(clause54,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(u3158,negated_conjecture,
( ~ c4_2(X0,a507)
| c3_2(X0,a508)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c10_2(X0,X1)
| c6_2(X0,a511) ) ).
cnf(u3149,negated_conjecture,
( c4_2(X0,X1)
| c3_2(X0,a508)
| ~ c4_2(X0,a507)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(clause234,negated_conjecture,
( ssSkP9(X0)
| ~ c9_2(X0,a564) ) ).
cnf(u3148,negated_conjecture,
( c4_2(X0,X1)
| c2_2(X0,a508)
| ~ c4_2(X0,a507)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u2688,negated_conjecture,
( c7_1(X0)
| ~ c10_2(X0,a545)
| ~ c2_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(u2716,negated_conjecture,
( c6_1(X0)
| ~ c4_2(X0,a536)
| ~ c3_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(clause245,negated_conjecture,
( ssSkP2(X0)
| ~ c2_2(X0,a486) ) ).
cnf(u2782,negated_conjecture,
( c7_1(X0)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1)
| c6_1(X0)
| c9_2(X0,a536) ) ).
cnf(u3074,negated_conjecture,
( c10_2(X0,X1)
| c3_2(X0,a507)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511) ) ).
cnf(u3086,negated_conjecture,
( c3_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c1_2(X0,X1)
| c3_2(X0,a507) ) ).
cnf(u2952,negated_conjecture,
( ~ c4_2(X0,X1)
| c2_2(X0,a512)
| c10_2(X0,X1)
| ~ ndr1_1(X0)
| c6_2(X0,a511) ) ).
cnf(u3075,negated_conjecture,
( c10_2(X0,X1)
| c3_2(X0,a507)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511) ) ).
cnf(u2824,negated_conjecture,
( ~ c5_1(X0)
| ~ c4_2(X0,a528)
| ~ c4_2(X0,a536)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c6_2(X0,a604)
| ~ ndr1_1(X0) ) ).
cnf(u3153,negated_conjecture,
( ~ c4_2(X0,a507)
| c2_2(X0,a508)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c10_2(X0,X1)
| c6_2(X0,a511) ) ).
cnf(u3114,negated_conjecture,
( c3_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c3_2(X0,a507) ) ).
cnf(u2948,negated_conjecture,
( c7_2(X0,a529)
| c6_2(X0,a530)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u2656,negated_conjecture,
( c7_1(X0)
| ndr1_1(X0)
| ~ c5_1(X0) ) ).
cnf(u2830,negated_conjecture,
( ~ c5_1(X0)
| ~ c2_2(X0,a528)
| ~ c4_2(X0,a536)
| c10_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(clause244,negated_conjecture,
( ssSkP2(X0)
| ~ c1_2(X0,a486) ) ).
cnf(u2865,negated_conjecture,
( c9_2(X0,a536)
| ~ c3_2(X0,a528)
| ~ c5_1(X0)
| c10_2(X0,a604)
| c6_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u2889,negated_conjecture,
( ~ c10_2(X0,X1)
| c6_2(X0,a530)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| c2_2(X0,a529) ) ).
cnf(u3011,negated_conjecture,
( c3_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c3_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c6_2(X0,a507) ) ).
cnf(u2949,negated_conjecture,
( c7_2(X0,a529)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(clause140,negated_conjecture,
( ssSkP4(X0)
| c3_2(X0,a507) ) ).
cnf(u2705,negated_conjecture,
( c6_1(X0)
| ~ c3_2(X0,a536)
| ~ c4_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(clause139,negated_conjecture,
( ssSkP4(X0)
| c6_2(X0,a507) ) ).
cnf(u3087,negated_conjecture,
( c3_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c3_2(X0,a507) ) ).
cnf(clause131,negated_conjecture,
( ssSkP6(X0)
| c2_2(X0,a529) ) ).
cnf(u2731,negated_conjecture,
( c6_1(X0)
| c9_2(X0,a536)
| ~ c3_2(X0,a528)
| ~ c5_1(X0) ) ).
cnf(u3096,negated_conjecture,
( c3_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c2_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| c3_2(X0,a507) ) ).
cnf(clause61,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(u3088,negated_conjecture,
( c2_2(X0,a529)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,a512)
| c2_2(X0,a508)
| c6_2(X0,a511)
| c6_2(X0,a530)
| c1_2(X0,X1)
| c3_2(X0,a507) ) ).
cnf(u2887,negated_conjecture,
( ~ c10_2(X0,X1)
| c1_2(X0,X1)
| ~ c1_2(X0,a530)
| ~ ndr1_1(X0)
| c3_2(X0,a529) ) ).
cnf(u3138,negated_conjecture,
( c9_2(X0,a568)
| ~ c2_2(X0,a567)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(clause124,negated_conjecture,
( ssSkP10(X0)
| c6_2(X0,a567) ) ).
cnf(clause233,negated_conjecture,
( ssSkP10(X0)
| ~ c3_2(X0,a567) ) ).
cnf(u2694,negated_conjecture,
( c7_1(X0)
| ~ c4_2(X0,a545)
| ~ c3_2(X0,a528)
| ~ c5_1(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN421-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.25 % Computer : n004.cluster.edu
% 0.09/0.25 % Model : x86_64 x86_64
% 0.09/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.25 % Memory : 8046.5625MB
% 0.09/0.25 % OS : Linux 6.8.0-71-generic
% 0.09/0.25 % CPULimit : 300
% 0.09/0.25 % WCLimit : 300
% 0.09/0.25 % DateTime : Mon Sep 28 15:55:22 UTC 2026
% 0.09/0.25 % CPUTime :
% 0.09/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.24/0.30 Running first-order theorem proving
% 0.24/0.30 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
% 4.19/1.52 % (490146)Input is clausal, will run a generic CNF schedule.
% 4.19/1.52 % (490153)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=2195483758:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.19/1.52 % (490156)lrs+10_1_sil=8000:sp=occurrence:random_seed=3689736063:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.19/1.52 % (490159)dis-21_1_sil=8000:lcm=predicate:random_seed=216006874:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 4.19/1.52 % (490155)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=416630604:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.19/1.52 % (490157)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=798267287:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.19/1.52 % (490158)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1152491309:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.19/1.52 % (490154)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3260731681:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.19/1.52 % (490158)Refutation not found, incomplete strategy
% 4.19/1.52 % (490158)------------------------------
% 4.19/1.52 % (490158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.19/1.52 % (490158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/1.52 % (490158)CaDiCaL version: 2.1.3
% 4.19/1.52 % (490158)Termination reason: Refutation not found, incomplete strategy
% 4.19/1.52 % (490158)Time elapsed: 0.026 s
% 4.19/1.52 % (490158)Peak memory usage: 90 MB
% 4.19/1.52 % (490158)Instructions burned: 25 (million)
% 4.19/1.52 % (490159)First to succeed.
% 4.19/1.52 % (490159)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-490146"
% 4.19/1.52 % (490156)Instruction limit reached!
% 4.19/1.52 % (490156)------------------------------
% 4.19/1.52 % (490156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.19/1.52 % (490156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/1.52 % (490156)CaDiCaL version: 2.1.3
% 4.19/1.52 % (490156)Termination reason: Instruction limit
% 4.19/1.52 % (490156)Termination phase: Saturation
% 4.19/1.52 % (490156)Time elapsed: 0.095 s
% 4.19/1.52 % (490156)Peak memory usage: 90 MB
% 4.19/1.52 % (490156)Instructions burned: 108 (million)
% 4.19/1.52 % (490157)Instruction limit reached!
% 4.19/1.52 % (490157)------------------------------
% 4.19/1.52 % (490157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.19/1.52 % (490157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/1.52 % (490157)CaDiCaL version: 2.1.3
% 4.19/1.52 % (490157)Termination reason: Instruction limit
% 4.19/1.52 % (490157)Termination phase: Saturation
% 4.19/1.52 % (490157)Time elapsed: 0.097 s
% 4.19/1.52 % (490157)Peak memory usage: 90 MB
% 4.19/1.52 % (490157)Instructions burned: 114 (million)
% 4.19/1.52 % (490167)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=4066602665:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 4.19/1.52 % (490168)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3932923177:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 4.19/1.52 % (490168)Refutation not found, incomplete strategy
% 4.19/1.52 % (490168)------------------------------
% 4.19/1.52 % (490168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.19/1.52 % (490168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/1.52 % (490168)CaDiCaL version: 2.1.3
% 4.19/1.52 % (490168)Termination reason: Refutation not found, incomplete strategy
% 4.19/1.52 % (490168)Time elapsed: 0.049 s
% 4.19/1.52 % (490168)Peak memory usage: 90 MB
% 4.19/1.52 % (490168)Instructions burned: 53 (million)
% 4.19/1.52 % (490158)------------------------------
% 4.19/1.52 % (490158)------------------------------
% 4.19/1.52 % SZS status Satisfiable for theBenchmark
% 4.19/1.52 % SZS output start Saturation.
% See solution above
% 5.85/1.73 % SZS output start Definitions and Model Updates.
% 5.85/1.73 % SZS output end Definitions and Model Updates.
% 5.85/1.73 % (490159)------------------------------
% 5.85/1.73 % (490159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.85/1.73 % (490159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.73 % (490159)CaDiCaL version: 2.1.3
% 5.85/1.73 % (490159)Termination reason: Satisfiable
% 5.85/1.73 % (490159)Time elapsed: 0.042 s
% 5.85/1.73 % (490159)Peak memory usage: 90 MB
% 5.85/1.73 % (490159)Instructions burned: 43 (million)
% 5.85/1.73 % (490159)------------------------------
% 5.85/1.73 % (490159)------------------------------
% 5.85/1.73 % (490146)Success in time 0.724 s
% 5.85/1.73 % Vampire exiting
%------------------------------------------------------------------------------