%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN424-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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:07:50 PM UTC 2026
% Result : Satisfiable 0.18s 0.32s
% Output : Saturation 0.18s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1438,negated_conjecture,
~ c2_0 ).
cnf(u1444,negated_conjecture,
~ ndr1_0 ).
cnf(u1459,negated_conjecture,
( ~ c8_1(X0)
| c3_2(X0,X1)
| c1_2(X0,X4)
| ~ c7_2(X0,X4)
| c3_2(X0,X4)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u1476,negated_conjecture,
~ c8_0 ).
cnf(u1493,negated_conjecture,
( c2_2(X0,X1)
| ~ c4_1(X0)
| c5_2(X0,X2)
| ~ c9_2(X0,X2)
| ~ c10_2(X0,X1)
| ~ c8_2(X0,X2)
| ~ ndr1_1(X0)
| c9_2(X0,X1) ) ).
cnf(u1496,negated_conjecture,
ssSkC28 ).
cnf(u1506,negated_conjecture,
~ c6_0 ).
cnf(u1516,negated_conjecture,
~ c10_0 ).
cnf(u1520,negated_conjecture,
( ~ c5_1(X1)
| ~ c6_2(X1,X2)
| ~ c9_2(X1,X2)
| ~ c2_1(X1)
| ~ c4_2(X1,X2)
| ~ ndr1_1(X1) ) ).
cnf(u1545,negated_conjecture,
~ c3_0 ).
cnf(u1552,negated_conjecture,
( ~ c5_2(X0,X1)
| c3_1(X0)
| c10_1(X0)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1577,negated_conjecture,
~ ndr1_1(a1098) ).
cnf(u1594,negated_conjecture,
( ~ c6_2(X0,X1)
| c8_1(X0)
| c5_1(X0)
| ~ c4_2(X0,X1)
| ~ c10_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1605,negated_conjecture,
( ~ c9_1(X0)
| ~ c5_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u1608,negated_conjecture,
ssSkC2 ).
cnf(u1616,negated_conjecture,
( ~ c2_1(X0)
| ~ c4_1(X0)
| c7_1(X0) ) ).
cnf(u1619,negated_conjecture,
ssSkC8 ).
cnf(u1624,negated_conjecture,
~ c7_0 ).
cnf(u1635,negated_conjecture,
( ~ c3_2(X0,X1)
| c1_1(X0)
| c5_1(X0)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1644,negated_conjecture,
c9_0 ).
cnf(u1655,negated_conjecture,
c5_0 ).
cnf(u1680,negated_conjecture,
( ~ c7_1(X0)
| c6_2(X0,X1)
| c8_2(X0,X1)
| ~ c2_2(X0,X1)
| c9_2(X0,X2)
| c7_2(X0,X2)
| ~ c3_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u1685,negated_conjecture,
c1_0 ).
cnf(u1692,negated_conjecture,
( ~ c8_2(X2,a1148)
| ~ c9_1(X2)
| ~ c2_1(X2) ) ).
cnf(u1709,negated_conjecture,
( c7_2(X1,X2)
| ~ c4_1(X1)
| c5_1(X1)
| c5_2(X1,X2)
| ~ ndr1_1(X1)
| c6_2(X1,X2) ) ).
cnf(u1717,negated_conjecture,
~ ndr1_1(a1041) ).
cnf(u1726,negated_conjecture,
~ ssSkC18 ).
cnf(u1732,negated_conjecture,
c4_0 ).
cnf(u1746,negated_conjecture,
( c4_2(X2,a1148)
| ~ c9_1(X2)
| ~ c2_1(X2) ) ).
cnf(u1755,negated_conjecture,
( ~ c3_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c10_2(X0,X2)
| c8_2(X0,X1)
| ~ c10_2(X0,X1)
| c2_2(X0,a1109)
| ~ ndr1_1(X0) ) ).
cnf(u1759,negated_conjecture,
( ~ c1_2(X0,a1109)
| ~ c2_2(X0,X2)
| ~ c10_2(X0,X2)
| c8_2(X0,X1)
| ~ c10_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1763,negated_conjecture,
( ~ c2_1(X2)
| ~ c9_1(X2)
| ndr1_1(X2) ) ).
cnf(u1767,negated_conjecture,
( ~ c5_1(X0)
| c7_1(X0)
| c6_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| c2_2(X0,X1) ) ).
cnf(u1774,negated_conjecture,
( ~ c5_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c6_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1788,negated_conjecture,
ssSkC26 ).
cnf(u1800,negated_conjecture,
ssSkC38 ).
cnf(u1815,negated_conjecture,
( ~ c3_2(X0,X1)
| c4_2(X0,a1109)
| ~ c2_2(X0,X2)
| ~ c10_2(X0,X2)
| c8_2(X0,X1)
| ~ c10_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1819,negated_conjecture,
( ~ c8_2(X0,X1)
| c3_1(X0)
| ~ c2_2(X0,X1)
| c9_1(X0)
| ~ ndr1_1(X0)
| c7_2(X0,X1) ) ).
cnf(u1834,negated_conjecture,
~ ssSkC9 ).
cnf(u1862,negated_conjecture,
( ~ c8_2(X0,a1039)
| c1_1(X0)
| c4_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1865,negated_conjecture,
ssSkC17 ).
cnf(u1870,negated_conjecture,
( ~ c5_2(X0,a1039)
| c1_1(X0)
| c4_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1883,negated_conjecture,
~ c5_1(a1098) ).
cnf(u1888,negated_conjecture,
~ c8_1(a1098) ).
cnf(u1892,negated_conjecture,
( ~ c5_2(X0,a1102)
| c3_1(X0)
| ~ c10_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1895,negated_conjecture,
~ ssSkC31 ).
cnf(u1900,negated_conjecture,
( ~ c4_2(X0,a1102)
| c3_1(X0)
| ~ c10_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1951,negated_conjecture,
ssSkC46 ).
cnf(u1966,negated_conjecture,
( ~ c6_2(X0,a1039)
| c1_1(X0)
| ~ c5_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1974,negated_conjecture,
( ~ c4_2(X0,X1)
| c5_1(X0)
| c2_1(X0)
| c5_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1992,negated_conjecture,
( c2_2(X0,X1)
| c3_1(X0)
| c8_2(X0,a1102)
| ~ c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1996,negated_conjecture,
ssSkC21 ).
cnf(u2000,negated_conjecture,
( c7_2(X0,X1)
| c8_1(X0)
| c3_2(X0,X1)
| c4_2(X0,X1)
| c9_2(X0,a1049)
| ~ ndr1_1(X0) ) ).
cnf(u2004,negated_conjecture,
( c7_2(X0,X1)
| c8_1(X0)
| c3_2(X0,X1)
| c4_2(X0,X1)
| c10_2(X0,a1049)
| ~ ndr1_1(X0) ) ).
cnf(u2016,negated_conjecture,
ssSkC51 ).
cnf(u2020,negated_conjecture,
( ~ c4_2(X0,a1182)
| c1_2(X0,X1)
| ~ c10_2(X0,X1)
| ssSkP11(X0)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u2024,negated_conjecture,
( ~ c10_2(X0,X1)
| c1_2(X0,X1)
| ssSkP11(X0)
| c9_2(X0,a1182)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u2072,negated_conjecture,
ssSkC19 ).
cnf(u2079,negated_conjecture,
( c7_2(X0,X1)
| c8_1(X0)
| c8_2(X0,a1049)
| c3_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u2084,negated_conjecture,
~ ssSkC29 ).
cnf(u2099,negated_conjecture,
~ ssSkC49 ).
cnf(u2103,negated_conjecture,
( ~ c1_2(X0,a1176)
| ~ c9_1(X0)
| ~ c7_2(X0,X1)
| c4_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u2107,negated_conjecture,
( ~ c10_2(X0,X1)
| c8_2(X0,a1182)
| c1_2(X0,X1)
| ssSkP11(X0)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u2114,negated_conjecture,
ssSkC24 ).
cnf(u2160,negated_conjecture,
( c2_2(X0,X1)
| c10_1(X0)
| c4_2(X0,a1045)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u2164,negated_conjecture,
( c2_2(X0,X1)
| c10_1(X0)
| c8_2(X0,a1045)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u2168,negated_conjecture,
( ~ c9_1(X0)
| ~ ndr1_1(X0)
| ~ c7_2(X0,a1176)
| ~ c7_2(X0,X1)
| c4_2(X0,X1)
| c3_2(X0,X1) ) ).
cnf(u2172,negated_conjecture,
( ~ c6_2(X0,a1176)
| ~ c9_1(X0)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| c4_2(X0,X1)
| c3_2(X0,X1) ) ).
cnf(u2194,negated_conjecture,
~ ndr1_1(a962) ).
cnf(u2200,negated_conjecture,
~ ssSkC0 ).
cnf(u2216,negated_conjecture,
~ ssSkC5 ).
cnf(u2222,negated_conjecture,
~ ndr1_1(a995) ).
cnf(u2228,negated_conjecture,
~ ssSkC7 ).
cnf(u2232,negated_conjecture,
ssSkC6 ).
cnf(u2240,negated_conjecture,
( ~ c1_1(X0)
| c3_1(X0) ) ).
cnf(u2253,negated_conjecture,
~ ndr1_1(a1042) ).
cnf(u2275,negated_conjecture,
ssSkC37 ).
cnf(u2320,negated_conjecture,
ssSkC16 ).
cnf(u2330,negated_conjecture,
~ ndr1_1(a1046) ).
cnf(u2344,negated_conjecture,
ssSkC20 ).
cnf(u2349,negated_conjecture,
ndr1_1(a1087) ).
cnf(u2353,negated_conjecture,
( ~ c6_2(a1087,X0)
| ~ c8_2(a1087,X0)
| ~ c3_2(a1087,X0) ) ).
cnf(u2373,negated_conjecture,
~ ssSkC48 ).
cnf(u2378,negated_conjecture,
ssSkC35 ).
cnf(u2390,negated_conjecture,
ssSkC39 ).
cnf(u2406,negated_conjecture,
( ~ c2_1(X0)
| ~ c2_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c10_1(X0) ) ).
cnf(u2433,negated_conjecture,
~ ssSkC15 ).
cnf(u2438,negated_conjecture,
ndr1_1(a1033) ).
cnf(u2442,negated_conjecture,
( ~ c7_2(a1033,X0)
| ~ c2_2(a1033,X0)
| ~ c4_2(a1033,X0) ) ).
cnf(u2451,negated_conjecture,
~ ndr1_1(a1078) ).
cnf(u2457,negated_conjecture,
~ ssSkC27 ).
cnf(u2482,negated_conjecture,
( ~ c1_1(X0)
| ~ c4_1(X0)
| ~ c5_1(X0) ) ).
cnf(u2491,negated_conjecture,
~ ndr1_1(a1154) ).
cnf(u2497,negated_conjecture,
~ ssSkC44 ).
cnf(u2502,negated_conjecture,
ndr1_1(a1170) ).
cnf(u2506,negated_conjecture,
( ~ c10_2(a1170,X0)
| c6_2(a1170,X0)
| c8_2(a1170,X0) ) ).
cnf(u2519,negated_conjecture,
~ ssSkC3 ).
cnf(u2563,negated_conjecture,
ssSkC23 ).
cnf(u2574,negated_conjecture,
ssSkC41 ).
cnf(u2579,negated_conjecture,
~ ndr1_1(a1139) ).
cnf(u2595,negated_conjecture,
ssSkC45 ).
cnf(u2607,negated_conjecture,
~ ndr1_1(a973) ).
cnf(u2621,negated_conjecture,
ssSkC14 ).
cnf(u2630,negated_conjecture,
( ~ c8_1(X0)
| ~ c3_1(X0) ) ).
cnf(u2649,negated_conjecture,
( ~ c10_2(a963,X0)
| c3_2(a963,X0)
| ~ c9_2(a963,X0) ) ).
cnf(u2652,negated_conjecture,
ndr1_1(a963) ).
cnf(u2657,negated_conjecture,
( ~ c5_2(X0,a969)
| ~ c9_1(X0)
| ~ c3_1(X0) ) ).
cnf(u2664,negated_conjecture,
~ ssSkC4 ).
cnf(u2681,negated_conjecture,
( ~ c4_2(X0,a983)
| c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2685,negated_conjecture,
( c2_2(X0,a983)
| c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2694,negated_conjecture,
~ c3_1(a1041) ).
cnf(u2702,negated_conjecture,
( ~ c6_2(a1087,X0)
| ~ c9_2(a1087,X0)
| c5_2(a1087,X0) ) ).
cnf(u2710,negated_conjecture,
( ~ c2_1(X0)
| c10_1(X0)
| ~ c7_1(X0) ) ).
cnf(u2713,negated_conjecture,
~ ssSkC30 ).
cnf(u2761,negated_conjecture,
~ ndr1_1(a1130) ).
cnf(u2782,negated_conjecture,
~ ssSkC43 ).
cnf(u2815,negated_conjecture,
( ~ c10_2(X0,a969)
| ~ c9_1(X0)
| ~ c3_1(X0) ) ).
cnf(u2819,negated_conjecture,
( c8_2(X0,a969)
| ~ c9_1(X0)
| ~ c3_1(X0) ) ).
cnf(u2831,negated_conjecture,
( ~ c10_2(X0,a983)
| c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2918,negated_conjecture,
ssSkC32 ).
cnf(u2922,negated_conjecture,
( c2_2(X0,a1104)
| c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2926,negated_conjecture,
( ~ c3_2(X0,a1104)
| c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2930,negated_conjecture,
~ ssSkC34 ).
cnf(u2934,negated_conjecture,
( c9_2(X0,a1112)
| ~ c6_1(X0)
| ssSkP4(X0) ) ).
cnf(u2938,negated_conjecture,
~ ssSkC42 ).
cnf(u2942,negated_conjecture,
( ~ c4_2(X0,a1142)
| c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2946,negated_conjecture,
( ~ c8_2(X0,a1142)
| c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2950,negated_conjecture,
( ~ c1_2(X0,a1142)
| c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2955,negated_conjecture,
~ ssSkC50 ).
cnf(u2979,negated_conjecture,
( c7_1(X0)
| c10_1(X0)
| c3_1(X0) ) ).
cnf(u2983,negated_conjecture,
( ~ c3_1(X0)
| ~ c9_1(X0)
| ndr1_1(X0) ) ).
cnf(u2995,negated_conjecture,
( ~ c2_1(X0)
| c1_1(X0)
| ndr1_1(X0) ) ).
cnf(u3060,negated_conjecture,
~ ssSkC12 ).
cnf(u3064,negated_conjecture,
( c2_2(X0,a1012)
| ~ c4_1(X0)
| ssSkP1(X0) ) ).
cnf(u3072,negated_conjecture,
( ~ c9_2(X0,a1104)
| c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u3076,negated_conjecture,
( c5_2(X0,a1112)
| ssSkP4(X0)
| ~ c6_1(X0) ) ).
cnf(u3080,negated_conjecture,
( ~ c7_2(X0,a1112)
| ssSkP4(X0)
| ~ c6_1(X0) ) ).
cnf(u3092,negated_conjecture,
( ~ c10_2(X0,a1172)
| ~ c4_1(X0)
| c7_1(X0) ) ).
cnf(u3096,negated_conjecture,
( c1_2(X0,a1172)
| ~ c4_1(X0)
| c7_1(X0) ) ).
cnf(u3100,negated_conjecture,
( c4_2(X0,a1172)
| ~ c4_1(X0)
| c7_1(X0) ) ).
cnf(u3112,negated_conjecture,
( c3_2(a980,X0)
| c1_2(a980,X0) ) ).
cnf(u3115,negated_conjecture,
ndr1_1(a980) ).
cnf(u3120,negated_conjecture,
( c5_2(a1074,X0)
| c8_2(a1074,X0) ) ).
cnf(u3123,negated_conjecture,
ndr1_1(a1074) ).
cnf(u3177,negated_conjecture,
( ~ c7_2(X0,a1012)
| ~ c4_1(X0)
| ssSkP1(X0) ) ).
cnf(u3181,negated_conjecture,
( ~ c6_2(X0,a1012)
| ~ c4_1(X0)
| ssSkP1(X0) ) ).
cnf(u3201,negated_conjecture,
( ~ c2_1(X0)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u3205,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0)
| ~ c6_1(X0) ) ).
cnf(u3213,negated_conjecture,
( ~ c2_1(X0)
| c5_1(X0)
| ndr1_1(X0) ) ).
cnf(u3217,negated_conjecture,
( ~ c4_1(X0)
| c7_1(X0)
| ndr1_1(X0) ) ).
cnf(u3228,negated_conjecture,
ssSkC33 ).
cnf(u3285,negated_conjecture,
( ssSkP1(X0)
| ~ c4_1(X0)
| ndr1_1(X0) ) ).
cnf(u3382,negated_conjecture,
~ c5_2(a1068,a1069) ).
cnf(u3385,negated_conjecture,
ssSkC25 ).
cnf(u3391,negated_conjecture,
c2_2(a1068,a1069) ).
cnf(u3396,negated_conjecture,
c2_2(a1068,a1070) ).
cnf(u3416,negated_conjecture,
c10_2(a1125,a1126) ).
cnf(u3421,negated_conjecture,
~ c3_2(a1125,a1126) ).
cnf(u3426,negated_conjecture,
~ c1_2(a1125,a1127) ).
cnf(u3461,negated_conjecture,
~ c3_2(a1162,a1163) ).
cnf(u3466,negated_conjecture,
c10_2(a1162,a1163) ).
cnf(u3471,negated_conjecture,
~ c8_2(a1162,a1163) ).
cnf(u3476,negated_conjecture,
~ c5_2(a1162,a1164) ).
cnf(u3490,negated_conjecture,
~ c5_2(a963,a964) ).
cnf(u3495,negated_conjecture,
~ c8_2(a967,a968) ).
cnf(u3498,negated_conjecture,
~ ssSkC1 ).
cnf(u3504,negated_conjecture,
~ c1_1(a973) ).
cnf(u3514,negated_conjecture,
~ c4_2(a980,a981) ).
cnf(u3528,negated_conjecture,
~ ssSkC13 ).
cnf(u3549,negated_conjecture,
c9_1(a1042) ).
cnf(u3574,negated_conjecture,
~ c3_1(a1068) ).
cnf(u3579,negated_conjecture,
c1_2(a1068,a1070) ).
cnf(u3584,negated_conjecture,
c8_2(a1068,a1070) ).
cnf(u3589,negated_conjecture,
c6_2(a1074,a1075) ).
cnf(u3594,negated_conjecture,
~ c3_2(a1074,a1075) ).
cnf(u3599,negated_conjecture,
~ c4_2(a1074,a1075) ).
cnf(u3605,negated_conjecture,
c10_2(a1087,a1088) ).
cnf(u3610,negated_conjecture,
~ c4_2(a1087,a1088) ).
cnf(u3615,negated_conjecture,
~ c5_2(a1087,a1088) ).
cnf(u3625,negated_conjecture,
c4_1(a1125) ).
cnf(u3630,negated_conjecture,
c8_2(a1125,a1126) ).
cnf(u3635,negated_conjecture,
c4_2(a1125,a1127) ).
cnf(u3640,negated_conjecture,
c5_2(a1125,a1127) ).
cnf(u3658,negated_conjecture,
~ ssSkC40 ).
cnf(u3709,negated_conjecture,
~ c6_1(a1162) ).
cnf(u3714,negated_conjecture,
c8_2(a1162,a1164) ).
cnf(u3719,negated_conjecture,
c4_2(a1162,a1164) ).
cnf(u3727,negated_conjecture,
ssSkC47 ).
cnf(u3743,negated_conjecture,
c9_2(a1170,a1171) ).
cnf(u3788,negated_conjecture,
ssSkC10 ).
cnf(u3917,negated_conjecture,
ssSkC36 ).
cnf(u3944,negated_conjecture,
~ c6_1(a963) ).
cnf(u3949,negated_conjecture,
c4_2(a963,a964) ).
cnf(u3954,negated_conjecture,
c1_2(a963,a964) ).
cnf(u3959,negated_conjecture,
~ c3_1(a967) ).
cnf(u3964,negated_conjecture,
~ c6_2(a967,a968) ).
cnf(u3969,negated_conjecture,
c1_2(a967,a968) ).
cnf(u3974,negated_conjecture,
~ c9_1(a973) ).
cnf(u3989,negated_conjecture,
c7_1(a980) ).
cnf(u3994,negated_conjecture,
c5_2(a980,a981) ).
cnf(u3999,negated_conjecture,
~ c6_2(a980,a981) ).
cnf(u4045,negated_conjecture,
c7_1(a1033) ).
cnf(u4050,negated_conjecture,
c8_2(a1033,a1034) ).
cnf(u4055,negated_conjecture,
c5_2(a1033,a1034) ).
cnf(u4060,negated_conjecture,
~ c10_2(a1033,a1034) ).
cnf(u4065,negated_conjecture,
c9_1(a1046) ).
cnf(u4075,negated_conjecture,
ssSkC22 ).
cnf(u4080,negated_conjecture,
ndr1_1(a1068) ).
cnf(u4100,negated_conjecture,
~ c1_1(a1120) ).
cnf(u4105,negated_conjecture,
~ c9_2(a1120,a1121) ).
cnf(u4110,negated_conjecture,
c1_2(a1120,a1121) ).
cnf(u4115,negated_conjecture,
~ c2_2(a1120,a1121) ).
cnf(u4125,negated_conjecture,
ndr1_1(a1125) ).
cnf(u4130,negated_conjecture,
~ c8_1(a1130) ).
cnf(u4135,negated_conjecture,
~ c10_1(a1130) ).
cnf(u4180,negated_conjecture,
~ c6_1(a1154) ).
cnf(u4186,negated_conjecture,
ndr1_1(a1162) ).
cnf(u4196,negated_conjecture,
~ c10_2(a1170,a1171) ).
cnf(u4201,negated_conjecture,
~ c6_2(a1170,a1171) ).
cnf(u4287,negated_conjecture,
ssSkC11 ).
cnf(u4366,negated_conjecture,
~ c5_1(a1058) ).
cnf(u4371,negated_conjecture,
~ c10_1(a1058) ).
cnf(u4376,negated_conjecture,
~ c1_1(a1058) ).
cnf(u4461,negated_conjecture,
~ c10_1(a1139) ).
cnf(u4466,negated_conjecture,
~ c1_1(a1139) ).
cnf(u4504,negated_conjecture,
~ c4_1(a967) ).
cnf(u4509,negated_conjecture,
ndr1_1(a967) ).
cnf(u4521,negated_conjecture,
c10_1(a1007) ).
cnf(u4562,negated_conjecture,
~ c7_1(a1074) ).
cnf(u4568,negated_conjecture,
~ c10_1(a1078) ).
cnf(u4575,negated_conjecture,
~ c4_1(a1120) ).
cnf(u4580,negated_conjecture,
ndr1_1(a1120) ).
cnf(u4605,negated_conjecture,
~ c9_1(a1154) ).
cnf(u4616,negated_conjecture,
c2_1(a1170) ).
cnf(u4872,negated_conjecture,
~ c7_1(a1170) ).
cnf(u4877,negated_conjecture,
~ c4_1(a1170) ).
cnf(u4882,negated_conjecture,
~ c10_1(a1170) ).
cnf(u4889,negated_conjecture,
c3_1(a1074) ).
cnf(u4893,negated_conjecture,
c10_1(a1074) ).
cnf(u4899,negated_conjecture,
c3_1(a1170) ).
cnf(u4908,negated_conjecture,
~ ssSkP4(a980) ).
cnf(u4917,negated_conjecture,
ssSkP6(a980) ).
cnf(u4928,negated_conjecture,
~ ssSkP0(a1074) ).
cnf(u4937,negated_conjecture,
ssSkP6(a1074) ).
cnf(u4957,negated_conjecture,
~ c9_1(a1074) ).
cnf(u4967,negated_conjecture,
~ c2_1(a980) ).
cnf(u4978,negated_conjecture,
~ ssSkP2(a1087) ).
cnf(u4989,negated_conjecture,
~ ssSkP1(a1033) ).
cnf(u5010,negated_conjecture,
~ c2_2(a1033,a1128) ).
cnf(u5018,negated_conjecture,
ssSkP5(a1170) ).
cnf(u5033,negated_conjecture,
~ ssSkP7(a1170) ).
cnf(u5042,negated_conjecture,
ssSkP8(a1170) ).
cnf(u5058,negated_conjecture,
~ c9_2(a963,a1128) ).
cnf(u5072,negated_conjecture,
~ c9_2(a963,a1157) ).
cnf(u5081,negated_conjecture,
~ ssSkP7(a963) ).
cnf(u5107,negated_conjecture,
~ c2_1(a1162) ).
cnf(u5112,negated_conjecture,
c5_1(a1162) ).
cnf(u5117,negated_conjecture,
c2_1(a963) ).
cnf(u5147,negated_conjecture,
~ c2_2(a1125,a1126) ).
cnf(u5151,negated_conjecture,
~ c2_2(a1125,a1045) ).
cnf(u5160,negated_conjecture,
~ c2_2(a1162,a1164) ).
cnf(u5164,negated_conjecture,
~ c2_2(a1162,a1045) ).
cnf(u5168,negated_conjecture,
~ c10_1(a1162) ).
cnf(u5173,negated_conjecture,
~ c2_2(a1033,a1034) ).
cnf(u5182,negated_conjecture,
c10_1(a1033) ).
cnf(u5194,negated_conjecture,
c7_1(a1162) ).
cnf(u5198,negated_conjecture,
~ c4_1(a1162) ).
cnf(u5213,negated_conjecture,
~ c8_2(a1120,a1121) ).
cnf(u5240,negated_conjecture,
~ c7_1(a963) ).
cnf(u5245,negated_conjecture,
~ c4_1(a963) ).
cnf(u5249,negated_conjecture,
~ c10_1(a963) ).
cnf(u5268,negated_conjecture,
~ c1_2(a980,a981) ).
cnf(u5295,negated_conjecture,
c5_1(a1125) ).
cnf(u5322,negated_conjecture,
~ c9_1(a1125) ).
cnf(u5356,negated_conjecture,
c7_2(a1068,a1070) ).
cnf(u5371,negated_conjecture,
c1_1(a1074) ).
cnf(u5379,negated_conjecture,
c8_2(a1074,a1102) ).
cnf(u5397,negated_conjecture,
~ c2_1(a1125) ).
cnf(u5408,negated_conjecture,
c7_1(a1125) ).
cnf(u5418,negated_conjecture,
~ c10_2(a1120,a1121) ).
cnf(u5453,negated_conjecture,
~ c8_2(a1087,a1088) ).
cnf(u5470,negated_conjecture,
c9_2(a1125,a1182) ).
cnf(u5474,negated_conjecture,
ssSkP11(a1125) ).
cnf(u5477,negated_conjecture,
~ c1_2(a1125,a1126) ).
cnf(u5520,negated_conjecture,
~ c4_1(a1074) ).
cnf(u5534,negated_conjecture,
c2_2(a980,a1109) ).
cnf(u5553,negated_conjecture,
c4_2(a980,a1109) ).
cnf(u5560,negated_conjecture,
( ~ c8_2(a1125,X1)
| c5_2(a1125,X1)
| ~ c9_2(a1125,X1) ) ).
cnf(u5572,negated_conjecture,
( c7_2(a1033,X1)
| ~ c3_2(a1033,X1)
| c9_2(a1033,X1) ) ).
cnf(u5579,negated_conjecture,
( c7_2(a980,X1)
| ~ c3_2(a980,X1)
| c9_2(a980,X1) ) ).
cnf(u5607,negated_conjecture,
~ c8_2(a1033,a1128) ).
cnf(u5621,negated_conjecture,
~ c1_2(a1033,a1128) ).
cnf(u5624,negated_conjecture,
c10_2(a1033,a1128) ).
cnf(u5635,negated_conjecture,
( c7_2(a1162,X1)
| ~ c3_2(a1162,X1)
| c9_2(a1162,X1) ) ).
cnf(u5652,negated_conjecture,
c4_2(a1125,a1045) ).
cnf(u5657,negated_conjecture,
c8_2(a1125,a1045) ).
cnf(u5675,negated_conjecture,
~ c1_2(a1162,a1164) ).
cnf(u5700,negated_conjecture,
c3_1(a963) ).
cnf(u5843,negated_conjecture,
c5_2(a980,a1109) ).
cnf(u5863,negated_conjecture,
~ c9_2(a1125,a1179) ).
cnf(u5872,negated_conjecture,
~ c9_2(a1125,a1126) ).
cnf(u5886,negated_conjecture,
~ ssSkP2(a1125) ).
cnf(u5896,negated_conjecture,
( c7_2(a1125,X1)
| ~ c3_2(a1125,X1)
| c9_2(a1125,X1) ) ).
cnf(u5899,negated_conjecture,
( ~ c2_2(a1125,X0)
| c6_2(a1125,X0)
| c8_2(a1125,X0) ) ).
cnf(u5908,negated_conjecture,
~ c4_1(a1033) ).
cnf(u5927,negated_conjecture,
~ c4_1(a980) ).
cnf(u5965,negated_conjecture,
~ c9_2(a1125,a1045) ).
cnf(u5984,negated_conjecture,
~ c1_2(a1125,a1045) ).
cnf(u6005,negated_conjecture,
~ c1_2(a1162,a1045) ).
cnf(u6019,negated_conjecture,
( c7_2(a980,X1)
| c1_2(a980,X1)
| c9_2(a980,X1) ) ).
cnf(u6028,negated_conjecture,
~ c1_2(a980,a1109) ).
cnf(u6039,negated_conjecture,
~ ssSkP11(a1033) ).
cnf(u6076,negated_conjecture,
ssSkP1(a1125) ).
cnf(u6084,negated_conjecture,
~ c3_2(a1125,a1012) ).
cnf(u6098,negated_conjecture,
~ ssSkP3(a1125) ).
cnf(u6112,negated_conjecture,
( ~ c10_2(a1125,X0)
| ~ c1_2(a1125,X0)
| c6_2(a1125,X0)
| c8_2(a1125,X0) ) ).
cnf(u6139,negated_conjecture,
~ c1_2(a1125,a1128) ).
cnf(u6154,negated_conjecture,
~ c1_2(a1125,a1156) ).
cnf(u6167,negated_conjecture,
~ c1_2(a1125,a1157) ).
cnf(u901,negated_conjecture,
( ~ c2_2(X0,a1151)
| ssSkP6(X0) ) ).
cnf(u890,negated_conjecture,
( ~ c9_2(X0,a1181)
| ~ ssSkP11(X0) ) ).
cnf(u6067,negated_conjecture,
( ~ c1_2(X0,a1012)
| c8_1(X0)
| ~ c4_1(X0)
| ssSkP1(X0)
| c5_1(X0)
| c2_1(X0)
| c8_2(X0,a1049)
| c3_1(X0)
| c10_1(X0)
| c3_2(X0,a1012) ) ).
cnf(u996,negated_conjecture,
( c9_2(X0,a1156)
| ~ ssSkP7(X0) ) ).
cnf(u5130,negated_conjecture,
( ~ c6_1(X0)
| ~ c6_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u1005,negated_conjecture,
( c9_2(X0,a1085)
| ~ ssSkP3(X0) ) ).
cnf(u848,negated_conjecture,
( ~ ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(u846,negated_conjecture,
( ~ ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u4944,negated_conjecture,
( ~ c6_1(X0)
| ndr1_1(X0) ) ).
cnf(u1007,negated_conjecture,
( c6_2(X0,a1076)
| ~ ssSkP2(X0) ) ).
cnf(u835,negated_conjecture,
( ~ ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(u5686,negated_conjecture,
c8_2(a1162,a1045) ).
cnf(u828,negated_conjecture,
( ~ ssSkP11(X0)
| ndr1_1(X0) ) ).
cnf(u5225,negated_conjecture,
( ~ c8_2(X0,a1151)
| c8_2(X0,a1045)
| c10_1(X0)
| ssSkP6(X0) ) ).
cnf(u5704,negated_conjecture,
( ~ c1_2(X0,a1157)
| c5_1(X0)
| ssSkP8(X0)
| c3_1(X0)
| c10_1(X0)
| ~ c2_2(X0,a1157)
| c2_1(X0) ) ).
cnf(u891,negated_conjecture,
( c3_2(X0,a1181)
| ~ ssSkP11(X0) ) ).
cnf(u5312,negated_conjecture,
( ~ ssSkP2(X0)
| ~ c2_2(X0,a1076)
| c9_1(X0)
| c7_2(X0,a1076)
| c3_1(X0) ) ).
cnf(u5530,negated_conjecture,
( ~ c10_2(X0,a1181)
| ~ c10_2(X0,X1)
| c8_2(X0,a1181)
| ~ c2_2(X0,X1)
| c2_2(X0,a1109)
| ~ ssSkP11(X0) ) ).
cnf(u838,negated_conjecture,
( ~ ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(u5943,negated_conjecture,
( ~ c1_2(X0,a1177)
| c9_1(X0)
| c7_2(X0,a1177)
| ssSkP9(X0)
| c8_2(X0,a1102)
| ~ c10_2(X0,a1177)
| c3_1(X0) ) ).
cnf(u5948,negated_conjecture,
( c5_2(X0,a1012)
| c8_1(X0)
| c9_2(X0,a1049)
| ~ c4_1(X0)
| ssSkP1(X0)
| c5_1(X0)
| c2_1(X0)
| c3_2(X0,a1012) ) ).
cnf(u5493,negated_conjecture,
( c1_2(X0,a1128)
| c8_2(X0,a1182)
| ssSkP11(X0)
| ~ c8_2(X0,a1128)
| ssSkP5(X0) ) ).
cnf(u5567,negated_conjecture,
( ~ c3_2(X0,X2)
| c8_2(X0,X1)
| ~ c2_2(X0,X1)
| c9_2(X0,X2)
| c7_2(X0,X2)
| c6_2(X0,X1)
| ~ ndr1_1(X0)
| c10_1(X0)
| c3_1(X0) ) ).
cnf(u909,negated_conjecture,
( ~ c10_2(X0,a1111)
| ~ ssSkP4(X0) ) ).
cnf(u1004,negated_conjecture,
( c2_2(X0,a1085)
| ~ ssSkP3(X0) ) ).
cnf(u935,negated_conjecture,
( ~ c10_2(X0,a988)
| ~ ssSkP0(X0) ) ).
cnf(u5483,negated_conjecture,
( c4_2(X0,a1012)
| c8_2(X0,a1049)
| c3_2(X0,a1012)
| c8_1(X0)
| ~ c4_1(X0)
| ssSkP1(X0) ) ).
cnf(u5208,negated_conjecture,
( ~ c8_2(X0,a1151)
| c4_2(X0,a1045)
| c10_1(X0)
| ssSkP6(X0) ) ).
cnf(u5901,negated_conjecture,
( ~ c3_2(a1033,X0)
| c9_2(a1033,X0)
| ~ c2_2(a1033,X0)
| ~ c4_2(a1033,X0) ) ).
cnf(u915,negated_conjecture,
( c3_2(X0,a1085)
| ~ ssSkP3(X0) ) ).
cnf(u5945,negated_conjecture,
( c7_2(X0,a1177)
| c9_1(X0)
| c3_1(X0)
| ssSkP9(X0)
| c10_1(X0)
| c8_2(X0,a1045) ) ).
cnf(u994,negated_conjecture,
( c10_2(X0,a1157)
| ssSkP8(X0) ) ).
cnf(u936,negated_conjecture,
( c1_2(X0,a988)
| ~ ssSkP0(X0) ) ).
cnf(u5437,negated_conjecture,
( ~ c6_1(X0)
| c3_2(X0,a1112)
| c4_2(X0,a1112)
| c10_2(X0,a1049)
| ssSkP4(X0)
| c8_1(X0) ) ).
cnf(u5351,negated_conjecture,
( ~ ssSkP10(X0)
| c9_1(X0)
| c7_2(X0,a1179)
| c3_1(X0) ) ).
cnf(u910,negated_conjecture,
( ~ c9_2(X0,a1111)
| ~ ssSkP4(X0) ) ).
cnf(clause75,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(u894,negated_conjecture,
( ~ c6_2(X0,a1177)
| ssSkP9(X0) ) ).
cnf(u829,negated_conjecture,
( ~ ssSkP10(X0)
| ndr1_1(X0) ) ).
cnf(u5548,negated_conjecture,
( ~ c10_2(X0,a1085)
| ~ c2_2(X0,X1)
| ~ c10_2(X0,X1)
| c8_2(X0,a1085)
| c4_2(X0,a1109)
| ~ ssSkP3(X0) ) ).
cnf(u993,negated_conjecture,
( ~ c1_2(X0,a1179)
| ~ ssSkP10(X0) ) ).
cnf(u5290,negated_conjecture,
( ~ c4_1(X1)
| c7_2(X1,X2)
| c5_1(X1)
| c5_2(X1,X2)
| c6_2(X1,X2) ) ).
cnf(u5547,negated_conjecture,
( ~ c10_2(X0,a1011)
| ~ c2_2(X0,X1)
| ~ c10_2(X0,X1)
| c8_2(X0,a1011)
| c4_2(X0,a1109)
| ~ ssSkP1(X0) ) ).
cnf(u5436,negated_conjecture,
( c4_2(X0,a1012)
| c3_2(X0,a1012)
| c8_1(X0)
| c10_2(X0,a1049)
| ~ c4_1(X0)
| ssSkP1(X0) ) ).
cnf(u5494,negated_conjecture,
( c1_2(X0,a1156)
| c8_2(X0,a1182)
| ssSkP11(X0)
| ~ c8_2(X0,a1156)
| ~ ssSkP7(X0) ) ).
cnf(u5104,negated_conjecture,
( c5_2(X0,a1172)
| c5_1(X0)
| ~ c4_1(X0)
| c7_1(X0) ) ).
cnf(u5549,negated_conjecture,
( ~ c10_2(X0,a1181)
| ~ c2_2(X0,X1)
| ~ c10_2(X0,X1)
| c8_2(X0,a1181)
| c4_2(X0,a1109)
| ~ ssSkP11(X0) ) ).
cnf(u5412,negated_conjecture,
( ~ c1_2(X0,a1151)
| c8_2(X0,a1102)
| ~ c10_2(X0,a1151)
| c3_1(X0)
| ssSkP6(X0) ) ).
cnf(u839,negated_conjecture,
( ~ ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u5950,negated_conjecture,
( c5_2(X0,a1012)
| c8_1(X0)
| c10_2(X0,a1049)
| ~ c4_1(X0)
| ssSkP1(X0)
| c5_1(X0)
| c2_1(X0)
| c3_2(X0,a1012) ) ).
cnf(u893,negated_conjecture,
( ~ c9_2(X0,a1177)
| ssSkP9(X0) ) ).
cnf(u5447,negated_conjecture,
( ~ c8_2(X0,a1156)
| ssSkP11(X0)
| c9_2(X0,a1182)
| c1_2(X0,a1156)
| ~ ssSkP7(X0) ) ).
cnf(u991,negated_conjecture,
( ~ c1_2(X0,a1181)
| ~ ssSkP11(X0) ) ).
cnf(u995,negated_conjecture,
( c10_2(X0,a1156)
| ~ ssSkP7(X0) ) ).
cnf(u6021,negated_conjecture,
( ~ ssSkP11(X0)
| ~ c2_2(X0,X1)
| c7_2(X0,a1181)
| c6_2(X0,X1)
| c10_1(X0)
| c3_1(X0)
| c8_2(X0,X1) ) ).
cnf(u898,negated_conjecture,
( ~ c6_2(X0,a1157)
| ssSkP8(X0) ) ).
cnf(clause71,negated_conjecture,
( ssSkP8(X0)
| ndr1_1(X0) ) ).
cnf(u6052,negated_conjecture,
( ~ c8_2(X0,a1157)
| ssSkP8(X0)
| c3_1(X0)
| c10_1(X0)
| ~ c2_2(X0,a1157)
| c2_1(X0)
| c8_2(X0,a1182)
| ssSkP11(X0)
| c5_1(X0) ) ).
cnf(u1022,negated_conjecture,
( c7_2(X0,a1011)
| ~ ssSkP1(X0) ) ).
cnf(u6061,negated_conjecture,
( ~ c1_2(X0,a1012)
| c9_2(X0,a1049)
| ~ c4_1(X0)
| ssSkP1(X0)
| c5_1(X0)
| c2_1(X0)
| c3_2(X0,a1012)
| c3_1(X0)
| c10_1(X0)
| c8_1(X0) ) ).
cnf(u1002,negated_conjecture,
( ~ c3_2(X0,a1111)
| ~ ssSkP4(X0) ) ).
cnf(u998,negated_conjecture,
( c10_2(X0,a1128)
| ssSkP5(X0) ) ).
cnf(clause164,negated_conjecture,
( c8_2(X0,a1177)
| ssSkP9(X0) ) ).
cnf(u917,negated_conjecture,
( c8_2(X0,a1076)
| ~ ssSkP2(X0) ) ).
cnf(u5264,negated_conjecture,
( ~ c1_2(X0,a1112)
| c10_1(X0)
| ~ c2_2(X0,a1112)
| c3_1(X0)
| ssSkP4(X0)
| ~ c6_1(X0) ) ).
cnf(u1021,negated_conjecture,
( ~ c1_2(X0,a1011)
| ~ ssSkP1(X0) ) ).
cnf(u5556,negated_conjecture,
( ~ c4_1(X0)
| c2_2(X0,X1)
| c5_2(X0,X2)
| ~ c9_2(X0,X2)
| ~ c10_2(X0,X1)
| ~ c8_2(X0,X2)
| c9_2(X0,X1) ) ).
cnf(u992,negated_conjecture,
( c2_2(X0,a1179)
| ~ ssSkP10(X0) ) ).
cnf(u899,negated_conjecture,
( ~ c6_2(X0,a1156)
| ~ ssSkP7(X0) ) ).
cnf(u6064,negated_conjecture,
( ~ c1_2(X0,a1012)
| c10_2(X0,a1049)
| ~ c4_1(X0)
| ssSkP1(X0)
| c5_1(X0)
| c2_1(X0)
| c3_2(X0,a1012)
| c3_1(X0)
| c10_1(X0)
| c8_1(X0) ) ).
cnf(u5685,negated_conjecture,
c4_2(a1162,a1045) ).
cnf(u892,negated_conjecture,
( c8_2(X0,a1179)
| ~ ssSkP10(X0) ) ).
cnf(clause300,negated_conjecture,
( ~ c3_2(X0,a1151)
| ssSkP6(X0) ) ).
cnf(u5944,negated_conjecture,
( c7_2(X0,a1177)
| c9_1(X0)
| c3_1(X0)
| ssSkP9(X0)
| c10_1(X0)
| c4_2(X0,a1045) ) ).
cnf(clause79,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u997,negated_conjecture,
( c7_2(X0,a1128)
| ssSkP5(X0) ) ).
cnf(clause68,negated_conjecture,
( ssSkP9(X0)
| ndr1_1(X0) ) ).
cnf(u830,negated_conjecture,
( ~ ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(u5092,negated_conjecture,
( ~ c1_2(X0,a1085)
| c5_1(X0)
| c1_1(X0)
| ~ ssSkP3(X0) ) ).
cnf(u5528,negated_conjecture,
( ~ c10_2(X0,a1011)
| ~ c10_2(X0,X1)
| c8_2(X0,a1011)
| ~ c2_2(X0,X1)
| c2_2(X0,a1109)
| ~ ssSkP1(X0) ) ).
cnf(u5484,negated_conjecture,
( ~ c6_1(X0)
| c8_2(X0,a1049)
| c3_2(X0,a1112)
| c4_2(X0,a1112)
| ssSkP4(X0)
| c8_1(X0) ) ).
cnf(u5101,negated_conjecture,
( c5_2(X0,a1157)
| c2_1(X0)
| c5_1(X0)
| ssSkP8(X0) ) ).
cnf(u5289,negated_conjecture,
( ~ c10_2(X0,a1076)
| c5_1(X0)
| ~ c4_2(X0,a1076)
| c8_1(X0)
| ~ ssSkP2(X0) ) ).
cnf(u5313,negated_conjecture,
( ~ c2_2(X0,a1177)
| c3_1(X0)
| c9_1(X0)
| c7_2(X0,a1177)
| ssSkP9(X0) ) ).
cnf(u5432,negated_conjecture,
( ~ c6_1(X0)
| c3_2(X0,a1112)
| c4_2(X0,a1112)
| c9_2(X0,a1049)
| ssSkP4(X0)
| c8_1(X0) ) ).
cnf(u5529,negated_conjecture,
( ~ c10_2(X0,a1085)
| ~ c10_2(X0,X1)
| c8_2(X0,a1085)
| ~ c2_2(X0,X1)
| c2_2(X0,a1109)
| ~ ssSkP3(X0) ) ).
cnf(u5446,negated_conjecture,
( ~ c8_2(X0,a1128)
| ssSkP11(X0)
| c9_2(X0,a1182)
| c1_2(X0,a1128)
| ssSkP5(X0) ) ).
cnf(u1027,negated_conjecture,
( ~ c5_2(X0,a988)
| ~ ssSkP0(X0) ) ).
cnf(u5448,negated_conjecture,
( ~ c8_2(X0,a1157)
| ssSkP11(X0)
| c9_2(X0,a1182)
| c1_2(X0,a1157)
| ssSkP8(X0) ) ).
cnf(u5495,negated_conjecture,
( c1_2(X0,a1157)
| c8_2(X0,a1182)
| ssSkP11(X0)
| ~ c8_2(X0,a1157)
| ssSkP8(X0) ) ).
cnf(clause301,negated_conjecture,
( ~ c5_2(X0,a1151)
| ssSkP6(X0) ) ).
cnf(u4947,negated_conjecture,
( ~ c4_1(X0)
| ndr1_1(X0) ) ).
cnf(u929,negated_conjecture,
( c3_2(X0,a1011)
| ~ ssSkP1(X0) ) ).
cnf(u5957,negated_conjecture,
( c5_2(X0,a1012)
| c3_2(X0,a1012)
| c8_1(X0)
| ~ c4_1(X0)
| ssSkP1(X0)
| c5_1(X0)
| c2_1(X0)
| c8_2(X0,a1049) ) ).
cnf(u1006,negated_conjecture,
( c9_2(X0,a1076)
| ~ ssSkP2(X0) ) ).
cnf(clause169,negated_conjecture,
( c4_2(X0,a1157)
| ssSkP8(X0) ) ).
cnf(u5431,negated_conjecture,
( c4_2(X0,a1012)
| c3_2(X0,a1012)
| c8_1(X0)
| c9_2(X0,a1049)
| ~ c4_1(X0)
| ssSkP1(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN424-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n001.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 16:01:48 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.32 % (457668)Will run a generic schedule for satisfiability detection.
% 0.18/0.32 % (457679)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=336851757:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.32 % (457674)% WARNING: option uhcvi not known.
% 0.18/0.32 % (457674)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2622077682:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.32 % (457673)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2137339717_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.32 % (457677)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2708831573:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.32 % (457675)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1816345143:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.32 % (457676)dis+10_1_sil=32000:sp=arity:random_seed=1022017425:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.32 % (457678)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=539850705:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.32 % Detected minimum model sizes of [1]
% 0.18/0.32 % Detected maximum model sizes of [227]
% 0.18/0.32 % TRYING [1]
% 0.18/0.32 % TRYING [2]
% 0.18/0.32 % (457679)Instruction limit reached!
% 0.18/0.32 % (457679)------------------------------
% 0.18/0.32 % (457679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.32 % (457679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.32 % (457679)CaDiCaL version: 2.1.3
% 0.18/0.32 % (457679)Termination reason: Instruction limit
% 0.18/0.32 % (457679)Termination phase: Saturation
% 0.18/0.32 % (457679)Time elapsed: 0.049 s
% 0.18/0.32 % (457679)Peak memory usage: 17 MB
% 0.18/0.32 % (457679)Instructions burned: 162 (million)
% 0.18/0.32 % (457674) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-457668-457674"...
% 0.18/0.32 % Finite Model Found!
% 0.18/0.32 % SZS status Satisfiable for theBenchmark
% 0.18/0.32 % (457673) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-457668-457673"...
% 0.18/0.32 % (457674)...printing done.
% 0.18/0.32 % SZS status Satisfiable for theBenchmark
% 0.18/0.32 % SZS output start Saturation.
% See solution above
% 0.18/0.32 % SZS output start Definitions and Model Updates.
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC9"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC51"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC29"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC50"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC4"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC31"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC32"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "c7_2"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "c10_2"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "c2_2"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "c6_2"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "c9_2"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC5"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkP0"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkP1"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkP2"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkP3"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkP4"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "c7_1"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "c9_1"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "c4_1"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkP7"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkP10"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkP11"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "c9_0"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC21"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "c6_0"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "c4_0"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC0"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC1"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC3"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC7"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC13"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC15"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC18"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC22"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC30"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC40"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC41"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC43"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC44"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ssSkC27"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "c2_0"
% 0.18/0.32 globally flip the polarity of every occurrence of predicate "ndr1_0"
% 0.18/0.32 % SZS output end Definitions and Model Updates.
% 0.18/0.32 % (457674)------------------------------
% 0.18/0.32 % (457674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.32 % (457674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.32 % (457674)CaDiCaL version: 2.1.3
% 0.18/0.32 % (457674)Termination reason: Satisfiable
% 0.18/0.32 % (457674)Time elapsed: 0.047 s
% 0.18/0.32 % (457674)Peak memory usage: 15 MB
% 0.18/0.32 % (457674)Instructions burned: 74 (million)
% 0.18/0.32 % (457668)Success in time 0.091 s
% 0.18/0.32 % Vampire exiting
%------------------------------------------------------------------------------