%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n007.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:35 PM UTC 2026
% Result : CounterSatisfiable 5.25s 1.48s
% Output : Saturation 6.25s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1104,negated_conjecture,
ndr1_0 ).
cnf(u1112,negated_conjecture,
c1_0 ).
cnf(u1115,negated_conjecture,
c6_0 ).
cnf(u1129,negated_conjecture,
c2_0 ).
cnf(u1164,negated_conjecture,
( c8_2(X184,X185)
| ~ ndr1_1(X184)
| c1_2(X184,X185)
| ~ c10_1(X184) ) ).
cnf(u1167,negated_conjecture,
~ sP1 ).
cnf(u1184,negated_conjecture,
sP4 ).
cnf(u1187,negated_conjecture,
~ sP5 ).
cnf(u1191,negated_conjecture,
( ~ c1_2(X180,a1176)
| c3_2(X180,X181)
| c9_1(X180)
| ~ ndr1_1(X180)
| c7_2(X180,X181)
| c4_2(X180,X181) ) ).
cnf(u1199,negated_conjecture,
( c6_2(X180,a1176)
| c4_2(X180,X181)
| c9_1(X180)
| ~ ndr1_1(X180)
| c7_2(X180,X181)
| c3_2(X180,X181) ) ).
cnf(u1203,negated_conjecture,
c7_0 ).
cnf(u1211,negated_conjecture,
c3_0 ).
cnf(u1216,negated_conjecture,
~ sP6 ).
cnf(u1220,negated_conjecture,
( c10_2(X177,a1172)
| ~ c7_1(X177)
| c4_1(X177) ) ).
cnf(u1224,negated_conjecture,
( c1_2(X177,a1172)
| ~ c7_1(X177)
| c4_1(X177) ) ).
cnf(u1228,negated_conjecture,
( c4_2(X177,a1172)
| ~ c7_1(X177)
| c4_1(X177) ) ).
cnf(u1232,negated_conjecture,
( ~ c7_1(X177)
| ndr1_1(X177)
| c4_1(X177) ) ).
cnf(u1236,negated_conjecture,
c5_0 ).
cnf(u1240,negated_conjecture,
~ c8_0 ).
cnf(u1244,negated_conjecture,
( ~ c7_1(X176)
| c3_1(X176)
| c10_1(X176) ) ).
cnf(u1249,negated_conjecture,
c4_0 ).
cnf(u1253,negated_conjecture,
c10_2(a1170,a1171) ).
cnf(u1258,negated_conjecture,
~ c9_2(a1170,a1171) ).
cnf(u1263,negated_conjecture,
c6_2(a1170,a1171) ).
cnf(u1267,negated_conjecture,
~ ndr1_1(a1170) ).
cnf(u1272,negated_conjecture,
( ~ c6_2(a1170,X175)
| c10_2(a1170,X175)
| c8_2(a1170,X175) ) ).
cnf(u1277,negated_conjecture,
c2_1(a1170) ).
cnf(u1301,negated_conjecture,
~ sP7 ).
cnf(u1332,negated_conjecture,
sP8 ).
cnf(u1336,negated_conjecture,
~ sP9 ).
cnf(u1340,negated_conjecture,
( ~ c8_2(X165,X166)
| c9_1(X165)
| c10_2(X165,a1159)
| ~ ndr1_1(X165)
| ~ c5_2(X165,X166)
| c9_2(X165,X166) ) ).
cnf(u1344,negated_conjecture,
( ~ c8_2(X165,X166)
| c9_1(X165)
| ~ c9_2(X165,a1159)
| ~ ndr1_1(X165)
| ~ c5_2(X165,X166)
| c9_2(X165,X166) ) ).
cnf(u1348,negated_conjecture,
( ~ c8_2(X165,X166)
| c9_1(X165)
| c2_2(X165,a1159)
| ~ ndr1_1(X165)
| ~ c5_2(X165,X166)
| c9_2(X165,X166) ) ).
cnf(u1352,negated_conjecture,
~ sP12 ).
cnf(u1357,negated_conjecture,
~ c10_0 ).
cnf(u1378,negated_conjecture,
~ sP13 ).
cnf(u1382,negated_conjecture,
c9_1(a1153) ).
cnf(u1387,negated_conjecture,
ndr1_1(a1153) ).
cnf(u1391,negated_conjecture,
( ~ c10_2(a1153,X162)
| c9_2(a1153,X162)
| c6_2(a1153,X162) ) ).
cnf(u1396,negated_conjecture,
c4_1(a1153) ).
cnf(u1401,negated_conjecture,
( ~ c6_2(X160,X161)
| ~ ndr1_1(X160)
| ~ c3_2(X160,X161)
| ~ c2_2(X160,X161)
| ~ c5_1(X160)
| ~ c7_1(X160) ) ).
cnf(u1404,negated_conjecture,
~ c9_0 ).
cnf(u1443,negated_conjecture,
( c6_2(X155,X156)
| ~ ndr1_1(X155)
| ~ c5_1(X155)
| c9_2(X155,X156)
| c7_2(X155,X156)
| c9_2(X155,a1149) ) ).
cnf(u1447,negated_conjecture,
( ~ c7_2(X155,a1149)
| ~ ndr1_1(X155)
| c6_2(X155,X156)
| c9_2(X155,X156)
| c7_2(X155,X156)
| ~ c5_1(X155) ) ).
cnf(u1451,negated_conjecture,
( ~ c8_2(X153,X154)
| c10_1(X153)
| ~ ndr1_1(X153)
| c2_2(X153,X154)
| ~ c5_1(X153) ) ).
cnf(u1466,negated_conjecture,
~ sP15 ).
cnf(u1489,negated_conjecture,
( ~ c6_2(X148,X150)
| ~ c1_2(X148,X150)
| ~ c5_1(X148)
| ~ c2_2(X148,X150)
| ~ ndr1_1(X148)
| ~ c8_2(X148,X149)
| ~ c1_2(X148,X149) ) ).
cnf(u1494,negated_conjecture,
~ c10_1(a1144) ).
cnf(u1499,negated_conjecture,
~ c5_1(a1144) ).
cnf(u1504,negated_conjecture,
c3_2(a1144,a1145) ).
cnf(u1509,negated_conjecture,
~ c1_2(a1144,a1145) ).
cnf(u1514,negated_conjecture,
c4_2(a1144,a1145) ).
cnf(u1519,negated_conjecture,
ndr1_1(a1144) ).
cnf(u1525,negated_conjecture,
~ c7_1(a1143) ).
cnf(u1528,negated_conjecture,
~ sP16 ).
cnf(u1534,negated_conjecture,
c8_1(a1143) ).
cnf(u1539,negated_conjecture,
~ sP17 ).
cnf(u1544,negated_conjecture,
~ c10_1(a1139) ).
cnf(u1548,negated_conjecture,
ndr1_1(a1139) ).
cnf(u1552,negated_conjecture,
( ~ c6_2(a1139,X147)
| c5_2(a1139,X147)
| c7_2(a1139,X147) ) ).
cnf(u1557,negated_conjecture,
~ c1_1(a1139) ).
cnf(u1562,negated_conjecture,
( ~ c9_2(X145,X146)
| ~ ndr1_1(X145)
| ~ c8_2(X145,X146)
| ~ c10_1(X145)
| ~ c10_2(X145,X146) ) ).
cnf(u1566,negated_conjecture,
( c9_2(X144,a1138)
| c3_1(X144) ) ).
cnf(u1570,negated_conjecture,
( c2_2(X144,a1138)
| c3_1(X144) ) ).
cnf(u1578,negated_conjecture,
( c3_1(X144)
| ndr1_1(X144) ) ).
cnf(u1582,negated_conjecture,
~ sP18 ).
cnf(u1587,negated_conjecture,
~ c3_1(a1135) ).
cnf(u1592,negated_conjecture,
c4_1(a1135) ).
cnf(u1597,negated_conjecture,
c9_1(a1135) ).
cnf(u1602,negated_conjecture,
~ sP19 ).
cnf(u1606,negated_conjecture,
ndr1_1(a1131) ).
cnf(u1610,negated_conjecture,
( ~ c3_2(a1131,X143)
| ~ c1_2(a1131,X143)
| c4_2(a1131,X143) ) ).
cnf(u1615,negated_conjecture,
c2_2(a1131,a1132) ).
cnf(u1620,negated_conjecture,
~ c4_2(a1131,a1132) ).
cnf(u1630,negated_conjecture,
~ sP21 ).
cnf(u1634,negated_conjecture,
( ~ c3_2(X140,X141)
| sP20(X140)
| ~ c10_2(X140,a1128)
| ~ ndr1_1(X140)
| ~ c1_2(X140,X141)
| ~ c7_2(X140,X141) ) ).
cnf(u1638,negated_conjecture,
( ~ c3_2(X140,X141)
| sP20(X140)
| ~ c7_2(X140,a1128)
| ~ ndr1_1(X140)
| ~ c1_2(X140,X141)
| ~ c7_2(X140,X141) ) ).
cnf(u1644,negated_conjecture,
sP22 ).
cnf(u1652,negated_conjecture,
( ~ c7_1(X138)
| c10_1(X138)
| c6_1(X138) ) ).
cnf(u1669,negated_conjecture,
~ sP23 ).
cnf(u1673,negated_conjecture,
( c10_2(X137,a1122)
| c8_1(X137)
| c10_1(X137) ) ).
cnf(u1677,negated_conjecture,
( ~ c2_2(X137,a1122)
| c8_1(X137)
| c10_1(X137) ) ).
cnf(u1681,negated_conjecture,
( ~ c9_2(X137,a1122)
| c8_1(X137)
| c10_1(X137) ) ).
cnf(u1685,negated_conjecture,
( c10_1(X137)
| c8_1(X137)
| ndr1_1(X137) ) ).
cnf(u1689,negated_conjecture,
~ sP24 ).
cnf(u1694,negated_conjecture,
~ c2_2(a1118,a1119) ).
cnf(u1699,negated_conjecture,
c4_2(a1118,a1119) ).
cnf(u1704,negated_conjecture,
~ c5_2(a1118,a1119) ).
cnf(u1709,negated_conjecture,
ndr1_1(a1118) ).
cnf(u1714,negated_conjecture,
c6_1(a1118) ).
cnf(u1719,negated_conjecture,
c7_1(a1118) ).
cnf(u1727,negated_conjecture,
~ sP25 ).
cnf(u1736,negated_conjecture,
( c6_1(X136)
| ndr1_1(X136)
| c3_1(X136) ) ).
cnf(u1741,negated_conjecture,
( ~ c1_1(X135)
| c4_1(X135)
| ~ c5_1(X135) ) ).
cnf(u1759,negated_conjecture,
~ sP27 ).
cnf(u1763,negated_conjecture,
~ sP28 ).
cnf(u1767,negated_conjecture,
( ~ c2_2(X134,a1110)
| c10_1(X134) ) ).
cnf(u1771,negated_conjecture,
( ~ c7_2(X134,a1110)
| c10_1(X134) ) ).
cnf(u1775,negated_conjecture,
( ~ c10_2(X134,a1110)
| c10_1(X134) ) ).
cnf(u1779,negated_conjecture,
( c10_1(X134)
| ndr1_1(X134) ) ).
cnf(u1795,negated_conjecture,
~ sP29 ).
cnf(u1799,negated_conjecture,
( ~ c8_1(X130)
| ~ c3_1(X130) ) ).
cnf(u1805,negated_conjecture,
sP30 ).
cnf(u1808,negated_conjecture,
( ~ c2_2(X129,a1104)
| c3_1(X129)
| ~ c2_1(X129) ) ).
cnf(u1812,negated_conjecture,
( c9_2(X129,a1104)
| c3_1(X129)
| ~ c2_1(X129) ) ).
cnf(u1816,negated_conjecture,
( ~ c3_2(X129,a1104)
| c3_1(X129)
| ~ c2_1(X129) ) ).
cnf(u1836,negated_conjecture,
~ sP31 ).
cnf(u1844,negated_conjecture,
( c5_2(X127,a1101)
| c8_1(X127)
| c1_1(X127) ) ).
cnf(u1848,negated_conjecture,
( c4_2(X127,a1101)
| c8_1(X127)
| c1_1(X127) ) ).
cnf(u1852,negated_conjecture,
( c8_1(X127)
| ndr1_1(X127)
| c1_1(X127) ) ).
cnf(u1856,negated_conjecture,
( c2_2(X125,X126)
| ~ ndr1_1(X125)
| ~ c10_1(X125)
| c3_2(X125,X126)
| ~ c2_1(X125) ) ).
cnf(u1860,negated_conjecture,
( c8_2(X124,a1100)
| ~ c5_1(X124)
| ~ c2_1(X124) ) ).
cnf(u1864,negated_conjecture,
( ~ c10_2(X124,a1100)
| ~ c5_1(X124)
| ~ c2_1(X124) ) ).
cnf(u1873,negated_conjecture,
~ c8_1(a1099) ).
cnf(u1878,negated_conjecture,
c5_1(a1099) ).
cnf(u1882,negated_conjecture,
ndr1_1(a1099) ).
cnf(u1892,negated_conjecture,
~ c5_1(a1098) ).
cnf(u1895,negated_conjecture,
( ~ c4_2(X120,X121)
| ~ ndr1_1(X120)
| c7_2(X120,X121)
| ~ c1_1(X120)
| c8_2(X120,X121)
| ~ c2_1(X120) ) ).
cnf(u1899,negated_conjecture,
ndr1_1(a1098) ).
cnf(u1908,negated_conjecture,
~ c8_1(a1098) ).
cnf(u1917,negated_conjecture,
( ~ c9_2(X116,X117)
| ~ c4_1(X116)
| c9_2(X116,a1097)
| ~ ndr1_1(X116)
| c6_2(X116,X117)
| ~ c1_2(X116,X117) ) ).
cnf(u1924,negated_conjecture,
( ~ c6_2(X116,a1097)
| ~ c4_1(X116)
| ~ c1_2(X116,X117)
| ~ ndr1_1(X116)
| c6_2(X116,X117)
| ~ c9_2(X116,X117) ) ).
cnf(u1940,negated_conjecture,
ndr1_1(a1095) ).
cnf(u1944,negated_conjecture,
( ~ c9_2(a1095,X111)
| c8_2(a1095,X111)
| c2_2(a1095,X111) ) ).
cnf(u1949,negated_conjecture,
~ c9_1(a1095) ).
cnf(u1953,negated_conjecture,
( ~ c9_2(a1095,X110)
| c2_2(a1095,X110)
| ~ c5_2(a1095,X110) ) ).
cnf(u1958,negated_conjecture,
~ sP32 ).
cnf(u1962,negated_conjecture,
( ~ c2_1(X109)
| c10_1(X109)
| c7_1(X109) ) ).
cnf(u1965,negated_conjecture,
~ sP33 ).
cnf(u1970,negated_conjecture,
ndr1_1(a1087) ).
cnf(u1974,negated_conjecture,
( c6_2(a1087,X108)
| c9_2(a1087,X108)
| c5_2(a1087,X108) ) ).
cnf(u1979,negated_conjecture,
~ c10_2(a1087,a1088) ).
cnf(u1984,negated_conjecture,
~ c4_2(a1087,a1088) ).
cnf(u1989,negated_conjecture,
~ c5_2(a1087,a1088) ).
cnf(u1994,negated_conjecture,
( ~ c3_2(a1087,X107)
| c6_2(a1087,X107)
| ~ c8_2(a1087,X107) ) ).
cnf(u1999,negated_conjecture,
~ sP35 ).
cnf(u2003,negated_conjecture,
( ~ c5_2(X105,a1084)
| ~ ndr1_1(X105)
| c6_2(X105,X106)
| ~ c1_2(X105,X106)
| ~ c2_1(X105) ) ).
cnf(u2007,negated_conjecture,
( ~ c9_2(X105,a1084)
| ~ ndr1_1(X105)
| c6_2(X105,X106)
| ~ c1_2(X105,X106)
| ~ c2_1(X105) ) ).
cnf(u2011,negated_conjecture,
( ~ c2_2(X105,a1084)
| ~ ndr1_1(X105)
| c6_2(X105,X106)
| ~ c1_2(X105,X106)
| ~ c2_1(X105) ) ).
cnf(u2015,negated_conjecture,
~ sP36 ).
cnf(u2020,negated_conjecture,
~ sP37 ).
cnf(u2025,negated_conjecture,
~ c8_1(a1079) ).
cnf(u2033,negated_conjecture,
~ c9_1(a1079) ).
cnf(u2038,negated_conjecture,
c1_1(a1079) ).
cnf(u2047,negated_conjecture,
sP39 ).
cnf(u2067,negated_conjecture,
~ c6_2(a1074,a1075) ).
cnf(u2072,negated_conjecture,
~ c3_2(a1074,a1075) ).
cnf(u2077,negated_conjecture,
~ c4_2(a1074,a1075) ).
cnf(u2082,negated_conjecture,
ndr1_1(a1074) ).
cnf(u2086,negated_conjecture,
( c8_2(a1074,X98)
| c5_2(a1074,X98) ) ).
cnf(u2091,negated_conjecture,
c7_1(a1074) ).
cnf(u2096,negated_conjecture,
( ~ c5_2(X96,X97)
| c3_1(X96)
| ~ ndr1_1(X96)
| c2_2(X96,X97)
| c10_1(X96)
| ~ c1_2(X96,X97) ) ).
cnf(u2107,negated_conjecture,
~ sP40 ).
cnf(u2123,negated_conjecture,
~ sP41 ).
cnf(u2128,negated_conjecture,
~ c4_2(a1066,a1067) ).
cnf(u2133,negated_conjecture,
c1_2(a1066,a1067) ).
cnf(u2138,negated_conjecture,
c6_2(a1066,a1067) ).
cnf(u2143,negated_conjecture,
ndr1_1(a1066) ).
cnf(u2148,negated_conjecture,
~ c8_1(a1066) ).
cnf(u2153,negated_conjecture,
c7_1(a1066) ).
cnf(u2190,negated_conjecture,
~ sP42 ).
cnf(u2195,negated_conjecture,
~ c5_1(a1062) ).
cnf(u2200,negated_conjecture,
c10_1(a1062) ).
cnf(u2205,negated_conjecture,
~ sP44 ).
cnf(u2209,negated_conjecture,
~ sP43 ).
cnf(u2214,negated_conjecture,
~ c5_1(a1058) ).
cnf(u2219,negated_conjecture,
~ c10_1(a1058) ).
cnf(u2224,negated_conjecture,
~ c1_1(a1058) ).
cnf(u2229,negated_conjecture,
~ sP45 ).
cnf(u2234,negated_conjecture,
( ~ c3_2(X86,X87)
| ~ ndr1_1(X86)
| c5_1(X86)
| ~ c1_2(X86,X87)
| c1_1(X86) ) ).
cnf(u2297,negated_conjecture,
~ sP47 ).
cnf(u2301,negated_conjecture,
( ~ c7_2(X83,X84)
| c8_1(X83)
| c8_2(X83,a1049)
| ~ ndr1_1(X83)
| c3_2(X83,X84)
| c4_2(X83,X84) ) ).
cnf(u2304,negated_conjecture,
~ sP46 ).
cnf(u2309,negated_conjecture,
( ~ c9_2(X83,a1049)
| c8_1(X83)
| ~ c7_2(X83,X84)
| ~ ndr1_1(X83)
| c3_2(X83,X84)
| c4_2(X83,X84) ) ).
cnf(u2313,negated_conjecture,
( ~ c7_2(X83,X84)
| c8_1(X83)
| ~ c10_2(X83,a1049)
| ~ ndr1_1(X83)
| c3_2(X83,X84)
| c4_2(X83,X84) ) ).
cnf(u2318,negated_conjecture,
~ c9_1(a1046) ).
cnf(u2321,negated_conjecture,
~ sP48 ).
cnf(u2326,negated_conjecture,
ndr1_1(a1046) ).
cnf(u2330,negated_conjecture,
( ~ c3_2(a1046,X82)
| c10_2(a1046,X82)
| ~ c8_2(a1046,X82) ) ).
cnf(u2336,negated_conjecture,
c5_1(a1043) ).
cnf(u2344,negated_conjecture,
c8_1(a1043) ).
cnf(u2349,negated_conjecture,
~ c1_2(a1043,a1044) ).
cnf(u2354,negated_conjecture,
~ c6_2(a1043,a1044) ).
cnf(u2359,negated_conjecture,
c4_2(a1043,a1044) ).
cnf(u2364,negated_conjecture,
ndr1_1(a1043) ).
cnf(u2369,negated_conjecture,
~ c9_1(a1042) ).
cnf(u2373,negated_conjecture,
ndr1_1(a1042) ).
cnf(u2377,negated_conjecture,
( ~ c3_2(a1042,X79)
| c6_2(a1042,X79)
| c4_2(a1042,X79) ) ).
cnf(u2381,negated_conjecture,
( ~ c7_2(a1042,X78)
| c3_2(a1042,X78)
| ~ c10_2(a1042,X78) ) ).
cnf(u2386,negated_conjecture,
~ sP49 ).
cnf(u2390,negated_conjecture,
( ~ c1_1(X77)
| c10_1(X77)
| ~ c7_1(X77) ) ).
cnf(u2407,negated_conjecture,
( ~ c8_2(X74,X75)
| c1_1(X74)
| c6_2(X74,a1039)
| ~ ndr1_1(X74)
| ~ c5_2(X74,X75)
| c4_2(X74,X75) ) ).
cnf(u2410,negated_conjecture,
~ sP50 ).
cnf(u2415,negated_conjecture,
( ~ c8_2(X74,a1039)
| c1_1(X74)
| ~ c5_2(X74,X75)
| ~ ndr1_1(X74)
| ~ c8_2(X74,X75)
| c4_2(X74,X75) ) ).
cnf(u2419,negated_conjecture,
( ~ c8_2(X74,X75)
| c1_1(X74)
| ~ c5_2(X74,a1039)
| ~ ndr1_1(X74)
| ~ c5_2(X74,X75)
| c4_2(X74,X75) ) ).
cnf(u2453,negated_conjecture,
ndr1_1(a1031) ).
cnf(u2457,negated_conjecture,
( ~ c6_2(a1031,X72)
| c4_2(a1031,X72)
| ~ c2_2(a1031,X72) ) ).
cnf(u2460,negated_conjecture,
~ sP51 ).
cnf(u2466,negated_conjecture,
~ c7_2(a1031,a1032) ).
cnf(u2471,negated_conjecture,
~ c8_2(a1031,a1032) ).
cnf(u2476,negated_conjecture,
c6_2(a1031,a1032) ).
cnf(u2482,negated_conjecture,
( ~ c4_2(X70,X71)
| ~ ndr1_1(X70)
| c6_2(X70,X71)
| c5_1(X70)
| c10_2(X70,X71)
| c8_1(X70) ) ).
cnf(u2538,negated_conjecture,
~ sP52 ).
cnf(u2572,negated_conjecture,
c9_1(a1020) ).
cnf(u2575,negated_conjecture,
~ sP53 ).
cnf(u2581,negated_conjecture,
~ ndr1_1(a1020) ).
cnf(u2589,negated_conjecture,
c3_1(a1020) ).
cnf(u2594,negated_conjecture,
~ sP55 ).
cnf(u2598,negated_conjecture,
~ sP56 ).
cnf(u2602,negated_conjecture,
( ~ c7_2(X64,a1011)
| c4_1(X64)
| sP54(X64) ) ).
cnf(u2606,negated_conjecture,
( c3_2(X64,a1011)
| c4_1(X64)
| sP54(X64) ) ).
cnf(u2610,negated_conjecture,
( ~ c1_2(X64,a1011)
| c4_1(X64)
| sP54(X64) ) ).
cnf(u2614,negated_conjecture,
( ndr1_1(X64)
| c4_1(X64)
| sP54(X64) ) ).
cnf(u2618,negated_conjecture,
( c4_2(X62,X63)
| ~ c3_1(X62)
| ~ c5_1(X62)
| ~ ndr1_1(X62)
| c8_2(X62,X63)
| c1_2(X62,X63) ) ).
cnf(u2631,negated_conjecture,
sP57 ).
cnf(u2637,negated_conjecture,
c10_1(a1007) ).
cnf(u2640,negated_conjecture,
~ sP58 ).
cnf(u2644,negated_conjecture,
~ sP59 ).
cnf(u2650,negated_conjecture,
( ~ c1_1(X56)
| c3_1(X56) ) ).
cnf(u2669,negated_conjecture,
~ sP60 ).
cnf(u2684,negated_conjecture,
~ sP61 ).
cnf(u2688,negated_conjecture,
( ~ c7_1(X50)
| c4_1(X50)
| ~ c2_1(X50) ) ).
cnf(u2705,negated_conjecture,
~ ndr1_1(a995) ).
cnf(u2711,negated_conjecture,
~ sP62 ).
cnf(u2715,negated_conjecture,
~ sP63 ).
cnf(u2736,negated_conjecture,
( ~ c7_2(X37,X38)
| c4_1(X37)
| c5_1(X37)
| ~ ndr1_1(X37)
| c5_2(X37,X38)
| ~ c6_2(X37,X38) ) ).
cnf(u2740,negated_conjecture,
( ~ c8_2(X35,X36)
| c3_1(X35)
| ~ c9_1(X35)
| ~ ndr1_1(X35)
| c2_2(X35,X36)
| ~ c7_2(X35,X36) ) ).
cnf(u2744,negated_conjecture,
( c6_2(X33,X34)
| ~ ndr1_1(X33)
| c10_2(X33,X34)
| c1_2(X33,X34)
| ~ c10_1(X33)
| ~ c3_1(X33) ) ).
cnf(u2748,negated_conjecture,
( ~ c8_2(X30,X31)
| ~ c8_1(X30)
| c1_2(X30,X32)
| c7_2(X30,X32)
| c3_2(X30,X32)
| ~ ndr1_1(X30)
| c3_2(X30,X31)
| ~ c1_2(X30,X31) ) ).
cnf(u2763,negated_conjecture,
( c1_2(X27,a988)
| ~ c6_1(X27)
| sP64(X27) ) ).
cnf(u2767,negated_conjecture,
( c10_2(X27,a988)
| ~ c6_1(X27)
| sP64(X27) ) ).
cnf(u2771,negated_conjecture,
( ~ c5_2(X27,a988)
| ~ c6_1(X27)
| sP64(X27) ) ).
cnf(u2775,negated_conjecture,
( ndr1_1(X27)
| ~ c6_1(X27)
| sP64(X27) ) ).
cnf(u2826,negated_conjecture,
( ~ c5_2(X21,X22)
| ~ ndr1_1(X21)
| c6_2(X21,X22)
| ~ c6_1(X21)
| c2_2(X21,X22) ) ).
cnf(u2843,negated_conjecture,
( c10_2(X19,a983)
| ~ c2_1(X19)
| c1_1(X19) ) ).
cnf(u2847,negated_conjecture,
( ~ c4_2(X19,a983)
| ~ c2_1(X19)
| c1_1(X19) ) ).
cnf(u2851,negated_conjecture,
( ~ c2_2(X19,a983)
| ~ c2_1(X19)
| c1_1(X19) ) ).
cnf(u2855,negated_conjecture,
( ~ c2_1(X19)
| ndr1_1(X19)
| c1_1(X19) ) ).
cnf(u2871,negated_conjecture,
ndr1_1(a980) ).
cnf(u2875,negated_conjecture,
( c3_2(a980,X16)
| c1_2(a980,X16) ) ).
cnf(u2880,negated_conjecture,
~ c7_1(a980) ).
cnf(u2885,negated_conjecture,
c5_2(a980,a981) ).
cnf(u2890,negated_conjecture,
~ c4_2(a980,a981) ).
cnf(u2895,negated_conjecture,
c6_2(a980,a981) ).
cnf(u2901,negated_conjecture,
( ~ c2_2(X15,a979)
| c2_1(X15)
| ~ c3_1(X15) ) ).
cnf(u2909,negated_conjecture,
( ~ c5_2(X15,a979)
| c2_1(X15)
| ~ c3_1(X15) ) ).
cnf(u2936,negated_conjecture,
~ sP65 ).
cnf(u2940,negated_conjecture,
( ~ c6_2(X13,a976)
| c7_1(X13)
| c2_1(X13) ) ).
cnf(u2944,negated_conjecture,
( c8_2(X13,a976)
| c7_1(X13)
| c2_1(X13) ) ).
cnf(u2948,negated_conjecture,
( ~ c1_2(X13,a976)
| c7_1(X13)
| c2_1(X13) ) ).
cnf(u2952,negated_conjecture,
( c7_1(X13)
| ndr1_1(X13)
| c2_1(X13) ) ).
cnf(u2956,negated_conjecture,
~ sP66 ).
cnf(u2976,negated_conjecture,
~ sP67 ).
cnf(u2981,negated_conjecture,
~ ndr1_1(a972) ).
cnf(u2989,negated_conjecture,
c7_1(a972) ).
cnf(u2997,negated_conjecture,
~ sP68 ).
cnf(u3002,negated_conjecture,
~ c2_1(a970) ).
cnf(u3007,negated_conjecture,
c5_1(a970) ).
cnf(u3012,negated_conjecture,
~ ndr1_1(a970) ).
cnf(u3019,negated_conjecture,
( c10_2(X7,a969)
| c9_1(X7)
| ~ c3_1(X7) ) ).
cnf(u3023,negated_conjecture,
( c8_2(X7,a969)
| c9_1(X7)
| ~ c3_1(X7) ) ).
cnf(u3027,negated_conjecture,
( ~ c5_2(X7,a969)
| c9_1(X7)
| ~ c3_1(X7) ) ).
cnf(u3031,negated_conjecture,
( ~ c3_1(X7)
| ndr1_1(X7)
| c9_1(X7) ) ).
cnf(u3035,negated_conjecture,
~ sP69 ).
cnf(u3040,negated_conjecture,
c6_1(a966) ).
cnf(u3045,negated_conjecture,
~ c4_1(a966) ).
cnf(u3050,negated_conjecture,
~ c9_1(a966) ).
cnf(u3068,negated_conjecture,
~ c5_2(a963,a964) ).
cnf(u3073,negated_conjecture,
c4_2(a963,a964) ).
cnf(u3078,negated_conjecture,
c1_2(a963,a964) ).
cnf(u3083,negated_conjecture,
ndr1_1(a963) ).
cnf(u3087,negated_conjecture,
( c9_2(a963,X3)
| c3_2(a963,X3)
| c10_2(a963,X3) ) ).
cnf(u3092,negated_conjecture,
~ c6_1(a963) ).
cnf(u3098,negated_conjecture,
~ ndr1_1(a962) ).
cnf(u3104,negated_conjecture,
~ sP70 ).
cnf(u3160,axiom,
( ~ c1_2(X0,a1179)
| c5_1(X0)
| sP2(X0) ) ).
cnf(u3164,axiom,
( c8_2(X0,a1179)
| c5_1(X0)
| sP2(X0) ) ).
cnf(u3168,axiom,
( ~ c2_2(X0,a1179)
| c5_1(X0)
| sP2(X0) ) ).
cnf(u3243,axiom,
c8_2(a1162,a1164) ).
cnf(u3248,axiom,
c4_2(a1162,a1164) ).
cnf(u3253,axiom,
~ c5_2(a1162,a1164) ).
cnf(u3258,axiom,
ndr1_1(a1162) ).
cnf(u3263,axiom,
~ c6_1(a1162) ).
cnf(u3268,axiom,
~ c3_2(a1162,a1163) ).
cnf(u3273,axiom,
~ c10_2(a1162,a1163) ).
cnf(u3278,axiom,
~ c8_2(a1162,a1163) ).
cnf(u3467,axiom,
~ c8_1(a1130) ).
cnf(u3471,axiom,
ndr1_1(a1130) ).
cnf(u3480,axiom,
~ c10_1(a1130) ).
cnf(u3486,axiom,
c4_2(a1125,a1127) ).
cnf(u3491,axiom,
~ c1_2(a1125,a1127) ).
cnf(u3496,axiom,
c5_2(a1125,a1127) ).
cnf(u3501,axiom,
ndr1_1(a1125) ).
cnf(u3506,axiom,
~ c4_1(a1125) ).
cnf(u3511,axiom,
~ c10_2(a1125,a1126) ).
cnf(u3516,axiom,
~ c3_2(a1125,a1126) ).
cnf(u3521,axiom,
c8_2(a1125,a1126) ).
cnf(u3609,axiom,
( c3_2(X0,a1113)
| ~ c7_1(X0) ) ).
cnf(u3671,axiom,
( ~ c8_2(X0,a1105)
| c6_1(X0)
| c3_1(X0) ) ).
cnf(u3675,axiom,
( ~ c5_2(X0,a1105)
| c6_1(X0)
| c3_1(X0) ) ).
cnf(u3679,axiom,
( c1_2(X0,a1105)
| c6_1(X0)
| c3_1(X0) ) ).
cnf(u3847,axiom,
ndr1_1(a1078) ).
cnf(u3851,axiom,
( ~ c6_2(a1078,X1)
| c2_2(a1078,X1)
| ~ c10_2(a1078,X1) ) ).
cnf(u3855,axiom,
( ~ c6_2(a1078,X0)
| c1_2(a1078,X0)
| c10_2(a1078,X0) ) ).
cnf(u3860,axiom,
~ c10_1(a1078) ).
cnf(u4078,axiom,
c3_1(a1041) ).
cnf(u4084,axiom,
~ ndr1_1(a1041) ).
cnf(u4305,axiom,
ndr1_1(a1008) ).
cnf(u4309,axiom,
( ~ c4_2(a1008,X0)
| c10_2(a1008,X0)
| c7_2(a1008,X0) ) ).
cnf(u4314,axiom,
~ c2_2(a1008,a1010) ).
cnf(u4319,axiom,
~ c6_2(a1008,a1010) ).
cnf(u4324,axiom,
~ c1_2(a1008,a1010) ).
cnf(u4330,axiom,
c8_2(a1008,a1009) ).
cnf(u4335,axiom,
c3_2(a1008,a1009) ).
cnf(u4617,axiom,
( c5_1(X0)
| ndr1_1(X0) ) ).
cnf(u4626,axiom,
( ~ c6_1(X0)
| ndr1_1(X0) ) ).
cnf(u4678,negated_conjecture,
c3_1(a1118) ).
cnf(u4683,negated_conjecture,
c10_1(a1074) ).
cnf(u4686,negated_conjecture,
~ c3_1(a1074) ).
cnf(u4696,negated_conjecture,
c3_1(a1066) ).
cnf(u4701,negated_conjecture,
c10_1(a972) ).
cnf(u4715,negated_conjecture,
c6_1(a1074) ).
cnf(u4720,negated_conjecture,
c6_1(a1066) ).
cnf(u4745,negated_conjecture,
c7_1(a1170) ).
cnf(u4749,negated_conjecture,
c10_1(a1170) ).
cnf(u4755,negated_conjecture,
~ c6_1(a1170) ).
cnf(u4767,negated_conjecture,
~ c2_1(a1118) ).
cnf(u4776,negated_conjecture,
~ c2_1(a1074) ).
cnf(u4785,negated_conjecture,
~ c2_1(a1066) ).
cnf(u4794,negated_conjecture,
~ c2_1(a972) ).
cnf(u4812,negated_conjecture,
~ c2_1(a980) ).
cnf(u4815,negated_conjecture,
~ c3_1(a980) ).
cnf(u4860,negated_conjecture,
~ c7_1(a1098) ).
cnf(u4880,negated_conjecture,
~ c6_1(a1153) ).
cnf(u4894,negated_conjecture,
~ c3_1(a1153) ).
cnf(u4910,negated_conjecture,
~ sP54(a1087) ).
cnf(u4915,negated_conjecture,
c4_1(a1087) ).
cnf(u4919,negated_conjecture,
~ c8_2(a1087,a1011) ).
cnf(u4928,negated_conjecture,
c1_1(a1087) ).
cnf(u4931,negated_conjecture,
~ c8_1(a1087) ).
cnf(u4935,negated_conjecture,
c8_2(a1087,a1101) ).
cnf(u4955,negated_conjecture,
~ c8_2(a1046,a1011) ).
cnf(u4963,negated_conjecture,
~ c1_1(a1046) ).
cnf(u4972,negated_conjecture,
~ c8_2(a1046,a1101) ).
cnf(u4983,negated_conjecture,
sP54(a1042) ).
cnf(u5001,negated_conjecture,
~ c3_1(a1042) ).
cnf(u5004,negated_conjecture,
~ c2_1(a1042) ).
cnf(u5018,negated_conjecture,
c2_2(a1031,a1032) ).
cnf(u5023,negated_conjecture,
c4_2(a1031,a1032) ).
cnf(u5038,negated_conjecture,
~ c10_1(a1046) ).
cnf(u5051,negated_conjecture,
c10_1(a1087) ).
cnf(u5061,negated_conjecture,
c1_2(a1087,a1011) ).
cnf(u5066,negated_conjecture,
~ c10_1(a1031) ).
cnf(u5081,negated_conjecture,
~ c5_1(a1074) ).
cnf(u5112,negated_conjecture,
~ c2_1(a963) ).
cnf(u5126,negated_conjecture,
~ c2_1(a1095) ).
cnf(u5156,negated_conjecture,
~ c2_1(a1062) ).
cnf(u5165,negated_conjecture,
~ c2_1(a1007) ).
cnf(u5186,negated_conjecture,
~ c1_2(a980,a981) ).
cnf(u5189,negated_conjecture,
~ c10_1(a980) ).
cnf(u5227,negated_conjecture,
~ c3_1(a1131) ).
cnf(u5231,negated_conjecture,
~ c7_1(a1131) ).
cnf(u5240,negated_conjecture,
c3_1(a1087) ).
cnf(u5243,negated_conjecture,
~ c7_1(a1087) ).
cnf(u5261,negated_conjecture,
~ c9_2(a1031,a1032) ).
cnf(u5284,negated_conjecture,
c8_1(a963) ).
cnf(u5309,negated_conjecture,
c6_2(a1118,a1119) ).
cnf(u5339,negated_conjecture,
~ c5_1(a1131) ).
cnf(u5352,negated_conjecture,
~ c5_1(a1087) ).
cnf(u5363,negated_conjecture,
~ c5_1(a980) ).
cnf(u5378,negated_conjecture,
~ c9_1(a1074) ).
cnf(u5424,negated_conjecture,
c9_1(a1087) ).
cnf(u5433,negated_conjecture,
~ c3_2(a1066,a1067) ).
cnf(u5437,negated_conjecture,
~ c7_2(a1066,a1067) ).
cnf(u5502,negated_conjecture,
~ c7_2(a1139,a1176) ).
cnf(u5511,negated_conjecture,
c9_1(a1139) ).
cnf(u5519,negated_conjecture,
~ c2_2(a1031,a1176) ).
cnf(u5527,negated_conjecture,
c9_1(a1031) ).
cnf(u5549,negated_conjecture,
c5_1(a1170) ).
cnf(u5562,negated_conjecture,
~ c5_1(a1139) ).
cnf(u5574,negated_conjecture,
~ c5_1(a1031) ).
cnf(u5591,negated_conjecture,
~ c4_1(a963) ).
cnf(u5612,negated_conjecture,
~ c4_1(a1131) ).
cnf(u5662,negated_conjecture,
( ~ c8_2(a1074,X0)
| c4_2(a1074,X0)
| ~ c5_2(a1074,X0) ) ).
cnf(u5682,negated_conjecture,
~ c5_1(a1130) ).
cnf(u5721,negated_conjecture,
c1_1(a1170) ).
cnf(u5724,negated_conjecture,
~ c8_1(a1170) ).
cnf(u5776,negated_conjecture,
c9_2(a1043,a1149) ).
cnf(u5792,negated_conjecture,
~ c2_1(a1043) ).
cnf(u5853,negated_conjecture,
( c2_2(a1131,X1)
| c4_2(a1131,X1)
| c3_2(a1131,X1)
| c8_2(a1131,X1) ) ).
cnf(u5870,negated_conjecture,
( ~ c9_2(a980,X0)
| ~ c7_2(a980,X0)
| ~ c3_2(a980,X0) ) ).
cnf(u5896,negated_conjecture,
~ c9_2(a1131,a1132) ).
cnf(u5904,negated_conjecture,
c2_1(a1087) ).
cnf(u5923,negated_conjecture,
~ c8_1(a1074) ).
cnf(u5937,negated_conjecture,
~ c7_2(a1162,a1164) ).
cnf(u5948,negated_conjecture,
~ c3_1(a1162) ).
cnf(u5954,negated_conjecture,
~ c5_1(a1162) ).
cnf(u5957,negated_conjecture,
~ c10_1(a1162) ).
cnf(u5963,negated_conjecture,
~ c1_2(a1162,a1164) ).
cnf(u5973,negated_conjecture,
c8_1(a1162) ).
cnf(u6008,negated_conjecture,
~ c2_1(a1125) ).
cnf(u6025,negated_conjecture,
c8_1(a1125) ).
cnf(u6032,negated_conjecture,
~ c5_1(a1125) ).
cnf(u6050,negated_conjecture,
~ c6_1(a1125) ).
cnf(u6071,negated_conjecture,
~ c5_2(a1125,a1126) ).
cnf(u6088,negated_conjecture,
~ c10_1(a1125) ).
cnf(u6099,negated_conjecture,
~ c9_1(a1125) ).
cnf(u6105,negated_conjecture,
~ c1_2(a1125,a1126) ).
cnf(u6134,negated_conjecture,
~ c2_1(a1031) ).
cnf(u6147,negated_conjecture,
~ c10_2(a1043,a1149) ).
cnf(u6172,negated_conjecture,
~ c4_1(a1043) ).
cnf(u6262,negated_conjecture,
~ c2_1(a1144) ).
cnf(u6284,negated_conjecture,
c10_2(a1144,a1145) ).
cnf(u6312,negated_conjecture,
c6_2(a1153,a1122) ).
cnf(u6316,negated_conjecture,
c10_1(a1153) ).
cnf(u6319,negated_conjecture,
~ c8_1(a1153) ).
cnf(u6345,negated_conjecture,
~ c2_1(a1153) ).
cnf(u6356,negated_conjecture,
~ c2_2(a1153,a1122) ).
cnf(u6361,negated_conjecture,
c8_2(a1153,a1122) ).
cnf(u6382,negated_conjecture,
c3_2(a1131,a976) ).
cnf(u6385,negated_conjecture,
~ c2_1(a1131) ).
cnf(u6394,negated_conjecture,
c5_2(a1087,a976) ).
cnf(u6425,negated_conjecture,
~ c1_2(a1131,a976) ).
cnf(u6446,negated_conjecture,
~ c6_1(a1087) ).
cnf(u6456,negated_conjecture,
~ c1_2(a1087,a976) ).
cnf(u6481,negated_conjecture,
~ c5_1(a1066) ).
cnf(u6492,negated_conjecture,
~ c7_2(a1118,a1119) ).
cnf(u6496,negated_conjecture,
( ~ c7_2(a1087,X0)
| c9_2(a1087,X0)
| c5_2(a1087,X0) ) ).
cnf(u6596,negated_conjecture,
~ c2_1(a1008) ).
cnf(u6604,negated_conjecture,
~ c10_1(a1008) ).
cnf(u6625,negated_conjecture,
~ c5_1(a1008) ).
cnf(u6631,negated_conjecture,
~ c3_1(a1008) ).
cnf(u6654,negated_conjecture,
~ c5_2(a1008,a1009) ).
cnf(u6662,negated_conjecture,
c9_1(a1008) ).
cnf(u6675,negated_conjecture,
~ c7_2(a1008,a1009) ).
cnf(u6706,negated_conjecture,
~ c1_2(a1008,a1009) ).
cnf(u6728,negated_conjecture,
~ sP64(a1095) ).
cnf(u6742,negated_conjecture,
~ sP64(a1074) ).
cnf(u6766,negated_conjecture,
~ c10_2(a1042,a1012) ).
cnf(u6790,negated_conjecture,
~ sP54(a1170) ).
cnf(u6801,negated_conjecture,
~ sP64(a980) ).
cnf(u6819,negated_conjecture,
~ c7_2(a980,a1138) ).
cnf(u6839,negated_conjecture,
~ sP38(a1087) ).
cnf(u6855,negated_conjecture,
~ c3_2(a980,a1086) ).
cnf(u6863,negated_conjecture,
~ sP34(a980) ).
cnf(u6874,negated_conjecture,
~ sP34(a1095) ).
cnf(u6895,negated_conjecture,
~ c10_2(a1042,a1112) ).
cnf(u6919,negated_conjecture,
~ sP26(a963) ).
cnf(u6935,negated_conjecture,
~ sP20(a1087) ).
cnf(u6957,negated_conjecture,
c10_1(a1131) ).
cnf(u6991,negated_conjecture,
~ c5_2(a1074,a1152) ).
cnf(u7020,negated_conjecture,
~ sP11(a1139) ).
cnf(u7032,negated_conjecture,
~ sP11(a1170) ).
cnf(u7046,negated_conjecture,
~ sP10(a1074) ).
cnf(u7061,negated_conjecture,
~ c2_2(a1031,a1158) ).
cnf(u7081,negated_conjecture,
~ sP10(a1170) ).
cnf(u7090,negated_conjecture,
~ sP10(a1139) ).
cnf(u7129,negated_conjecture,
~ sP2(a1153) ).
cnf(u7150,negated_conjecture,
~ sP0(a963) ).
cnf(u7171,negated_conjecture,
~ c5_2(a1074,a1182) ).
cnf(u7202,negated_conjecture,
~ c7_1(a1046) ).
cnf(u7265,negated_conjecture,
~ c7_1(a1042) ).
cnf(u7285,negated_conjecture,
~ c5_2(a1074,a1179) ).
cnf(u7333,negated_conjecture,
~ sP38(a1153) ).
cnf(u7336,negated_conjecture,
~ c5_1(a1153) ).
cnf(u7452,axiom,
~ sP10(a1078) ).
cnf(u7467,negated_conjecture,
c9_1(a1078) ).
cnf(u7474,negated_conjecture,
~ c10_2(a1078,a1176) ).
cnf(u7483,axiom,
~ sP54(a1078) ).
cnf(u7487,axiom,
~ c10_2(a1078,a1012) ).
cnf(u7496,negated_conjecture,
~ c5_1(a1078) ).
cnf(u7516,axiom,
~ sP11(a1078) ).
cnf(u7541,negated_conjecture,
c8_1(a1008) ).
cnf(u7554,axiom,
~ sP34(a1008) ).
cnf(u7567,axiom,
~ sP38(a1008) ).
cnf(u7581,axiom,
~ sP11(a1008) ).
cnf(u7606,negated_conjecture,
~ sP26(a1074) ).
cnf(u7619,negated_conjecture,
~ sP54(a1074) ).
cnf(u7638,negated_conjecture,
~ c10_2(a1074,a1138) ).
cnf(u7654,negated_conjecture,
~ c10_2(a1074,a1086) ).
cnf(u7686,negated_conjecture,
~ sP26(a1170) ).
cnf(u7699,negated_conjecture,
~ c6_1(a1078) ).
cnf(u7785,negated_conjecture,
~ c5_2(a1153,a1122) ).
cnf(u7839,negated_conjecture,
c8_1(a1078) ).
cnf(u7890,negated_conjecture,
~ sP54(a1131) ).
cnf(u7918,negated_conjecture,
~ c5_1(a1079) ).
cnf(u7927,negated_conjecture,
~ c7_1(a1079) ).
cnf(u8023,negated_conjecture,
~ sP34(a1139) ).
cnf(u8063,negated_conjecture,
~ sP38(a1095) ).
cnf(u8075,negated_conjecture,
~ c5_1(a1095) ).
cnf(u8250,negated_conjecture,
c10_2(a1087,a1159) ).
cnf(u8279,negated_conjecture,
~ c8_2(a1087,a1086) ).
cnf(u8287,negated_conjecture,
~ sP34(a1087) ).
cnf(u8293,negated_conjecture,
~ c8_2(a1087,a1084) ).
cnf(u8301,negated_conjecture,
~ sP64(a1087) ).
cnf(u8305,negated_conjecture,
c8_2(a1087,a1179) ).
cnf(u8310,negated_conjecture,
c6_2(a1087,a1179) ).
cnf(u8332,negated_conjecture,
~ c5_2(a1087,a1101) ).
cnf(u8355,negated_conjecture,
c3_2(a1087,a1084) ).
cnf(u8404,negated_conjecture,
~ c8_2(a1087,a983) ).
cnf(u8431,negated_conjecture,
~ c5_2(a1087,a1179) ).
cnf(u8499,negated_conjecture,
~ c7_2(a1087,a1084) ).
cnf(u8502,negated_conjecture,
c1_2(a1087,a1084) ).
cnf(u8731,negated_conjecture,
~ sP3(a1170) ).
cnf(u8998,negated_conjecture,
~ c10_1(a1095) ).
cnf(u6410,negated_conjecture,
( ~ c5_2(X0,a1039)
| c2_1(X0)
| c1_1(X0)
| c7_1(X0)
| ~ c5_2(X0,a976)
| c4_2(X0,a976) ) ).
cnf(u4636,negated_conjecture,
( ~ c5_2(X96,X97)
| c3_1(X96)
| c2_2(X96,X97)
| c10_1(X96)
| ~ c1_2(X96,X97) ) ).
cnf(u8838,negated_conjecture,
( ~ c2_2(X0,a988)
| ~ c10_1(X0)
| c3_2(X0,a1084)
| ~ c6_1(X0)
| ~ c3_2(X0,a988)
| ~ c2_1(X0)
| ~ c5_1(X0)
| ~ c7_1(X0) ) ).
cnf(u289,axiom,
( ~ c2_2(X0,a1012)
| ~ sP54(X0) ) ).
cnf(u8885,negated_conjecture,
( ~ c1_2(X0,a1149)
| c1_2(X0,a1097)
| ~ c10_1(X0)
| ~ c3_1(X0)
| ~ c4_1(X0)
| c10_2(X0,a1097)
| c6_2(X0,a1149)
| ~ c5_1(X0)
| c9_2(X0,a1077)
| c7_2(X0,a1077)
| ~ sP38(X0) ) ).
cnf(u8978,negated_conjecture,
( ~ c8_2(X0,a1101)
| c10_2(X0,a1159)
| c1_2(X0,a1101)
| ~ c10_1(X0)
| c8_1(X0)
| c1_1(X0)
| c9_1(X0)
| ~ c10_2(X0,a1101) ) ).
cnf(u8951,negated_conjecture,
( c4_2(X0,a1112)
| c1_1(X0)
| c1_2(X0,a1039)
| ~ c10_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0) ) ).
cnf(u9424,negated_conjecture,
( c6_2(X0,a988)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c10_1(X0)
| ~ c5_1(X0)
| c7_2(X0,a1084)
| c1_2(X0,a1084)
| ~ c6_1(X0)
| sP64(X0) ) ).
cnf(u4647,negated_conjecture,
~ c3_1(a1143) ).
cnf(u9905,negated_conjecture,
( ~ c1_2(X0,a1176)
| ~ c1_1(X0)
| c8_2(X0,X1)
| ~ c2_1(X0)
| c9_1(X0)
| ~ c5_1(X0)
| c3_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_2(X0,a969)
| ~ c10_1(X0)
| c3_2(X0,a1176) ) ).
cnf(u529,axiom,
( c8_2(X0,a1152)
| ~ sP14(X0) ) ).
cnf(u9919,negated_conjecture,
( c6_2(X0,a1178)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c9_2(X0,a1097)
| ~ c5_1(X0) ) ).
cnf(u544,axiom,
( ~ c8_2(X0,a1158)
| ~ sP10(X0) ) ).
cnf(u5751,negated_conjecture,
( c2_2(X0,a969)
| c10_1(X0)
| ~ c5_1(X0)
| c9_1(X0)
| ~ c3_1(X0) ) ).
cnf(u10128,negated_conjecture,
( ~ c5_2(X0,a1182)
| c1_2(X0,a1159)
| c7_2(X0,a1159)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| ~ sP0(X0) ) ).
cnf(u5769,negated_conjecture,
~ c3_1(a1043) ).
cnf(u9273,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ sP11(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,a1077)
| ~ c10_1(X0)
| c3_2(X0,a1157)
| ~ c2_1(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0) ) ).
cnf(u7431,negated_conjecture,
( ~ c7_2(X0,a1128)
| sP20(X0)
| ~ ndr1_1(X0)
| ~ c1_2(X0,a1113)
| ~ c7_2(X0,a1113)
| ~ c7_1(X0) ) ).
cnf(u6985,negated_conjecture,
( ~ c7_2(X0,a1152)
| c3_1(X0)
| ~ c9_1(X0)
| c2_2(X0,a1152)
| ~ sP14(X0) ) ).
cnf(u9898,negated_conjecture,
( ~ c1_2(X0,a1176)
| ~ c1_1(X0)
| c8_2(X0,X1)
| ~ c2_1(X0)
| c9_1(X0)
| ~ c5_1(X0)
| c3_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_2(X0,a1077)
| ~ c10_1(X0)
| c3_2(X0,a1176)
| c7_2(X0,a1077)
| ~ sP38(X0) ) ).
cnf(u8594,negated_conjecture,
( c2_2(X0,X1)
| c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c10_1(X0)
| ~ c5_1(X0) ) ).
cnf(u6830,negated_conjecture,
( c9_2(X0,a1149)
| ~ c5_1(X0)
| c9_2(X0,a1077)
| c7_2(X0,a1077)
| ~ sP38(X0) ) ).
cnf(u4649,negated_conjecture,
ndr1_1(a966) ).
cnf(u9924,negated_conjecture,
( ~ c1_2(X0,X1)
| ~ c5_1(X0)
| c9_2(X0,X1)
| c7_2(X0,X1)
| c9_2(X0,a1149)
| ~ c10_1(X0)
| c3_2(X0,X1)
| ~ c2_1(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| c10_2(X0,a1077) ) ).
cnf(u6732,negated_conjecture,
( ~ c1_2(X0,a989)
| ~ c4_1(X0)
| c9_2(X0,a1097)
| ~ sP64(X0) ) ).
cnf(u8260,negated_conjecture,
( ~ c7_2(X0,a1084)
| ~ c2_1(X0)
| ~ sP64(X0)
| sP20(X0)
| ~ c10_2(X0,a1128)
| ~ c1_2(X0,a1084)
| ~ c10_1(X0) ) ).
cnf(u9405,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ c5_1(X0)
| ~ c1_2(X0,a976)
| c9_2(X0,a976)
| c7_2(X0,a976)
| c9_2(X0,a1149)
| c10_1(X0)
| c7_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0) ) ).
cnf(u9386,negated_conjecture,
( ~ c1_2(X0,a1152)
| ~ c5_1(X0)
| ~ c1_2(X0,a976)
| c9_2(X0,a976)
| c7_2(X0,a976)
| c9_2(X0,a1149)
| c10_1(X0)
| c7_1(X0)
| ~ sP14(X0) ) ).
cnf(u9660,negated_conjecture,
( ~ c1_2(X0,a1182)
| c10_1(X0)
| ~ c5_1(X0)
| c7_2(X0,a1084)
| c1_2(X0,a1084)
| ~ sP3(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ sP0(X0) ) ).
cnf(u8034,negated_conjecture,
( ~ c5_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0)
| ~ c2_1(X0)
| c9_1(X0)
| c2_2(X0,a1159)
| c7_2(X0,a1157)
| c9_2(X0,a1157) ) ).
cnf(u10101,negated_conjecture,
( c9_2(X0,a1149)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c9_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| ~ sP3(X0) ) ).
cnf(u461,axiom,
( c7_2(X0,a1112)
| ~ sP26(X0) ) ).
cnf(u9071,negated_conjecture,
( c7_2(X0,a1122)
| c1_2(X0,a1122)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c10_1(X0)
| ~ c5_1(X0)
| c8_1(X0) ) ).
cnf(u10034,negated_conjecture,
( ~ c1_2(X0,a1149)
| c7_2(X0,a988)
| ~ c5_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a988)
| ~ c2_1(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| c10_2(X0,a1077)
| ~ c6_1(X0)
| sP64(X0)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| c9_2(X0,a988)
| c6_2(X0,a1149) ) ).
cnf(u605,axiom,
( ~ c9_2(X0,a1182)
| ~ sP0(X0) ) ).
cnf(u7646,negated_conjecture,
( ~ c10_2(X0,a1086)
| ~ c10_1(X0)
| ~ sP34(X0)
| c1_2(X0,a1086) ) ).
cnf(u8521,negated_conjecture,
( c2_2(X0,a1159)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0) ) ).
cnf(u9271,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ sP11(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,a1100)
| ~ c10_1(X0)
| c3_2(X0,a1157)
| ~ c2_1(X0) ) ).
cnf(u8157,negated_conjecture,
( ~ c5_2(X0,a983)
| ~ c3_1(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| c1_2(X0,a983)
| c9_1(X0)
| c2_2(X0,a1159)
| c1_1(X0)
| c9_2(X0,a983) ) ).
cnf(u6887,negated_conjecture,
( c6_2(X0,a1112)
| ~ sP26(X0)
| ~ c6_1(X0)
| c2_2(X0,a1112) ) ).
cnf(u6865,negated_conjecture,
( ~ c8_2(X0,a1086)
| ~ sP34(X0)
| ~ c10_1(X0)
| ~ c10_2(X0,a1086) ) ).
cnf(u6243,negated_conjecture,
( ~ c8_2(X0,a1138)
| ~ c10_1(X0)
| ~ c10_2(X0,a1138)
| c3_1(X0) ) ).
cnf(u4734,negated_conjecture,
( c1_1(X0)
| ndr1_1(X0) ) ).
cnf(u7003,negated_conjecture,
( ~ c7_2(X0,a1157)
| c4_1(X0)
| c5_1(X0)
| c5_2(X0,a1157)
| ~ sP11(X0) ) ).
cnf(u8718,negated_conjecture,
( ~ c3_2(X0,a1178)
| ~ c10_1(X0)
| c3_2(X0,a1084)
| ~ sP3(X0)
| ~ c2_1(X0)
| ~ c5_1(X0)
| ~ c7_1(X0) ) ).
cnf(u9080,negated_conjecture,
( ~ c1_2(X0,X1)
| c7_2(X0,a1084)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c10_1(X0)
| ~ c5_1(X0)
| c6_2(X0,X1)
| c1_2(X0,a1084) ) ).
cnf(u7177,negated_conjecture,
( ~ c5_2(X0,a1182)
| c1_1(X0)
| ~ c5_2(X0,a1039)
| ~ sP0(X0) ) ).
cnf(u9990,negated_conjecture,
( c9_2(X0,a1149)
| c9_2(X0,a988)
| c7_2(X0,a988)
| ~ c5_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a988)
| ~ c2_1(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| c10_2(X0,a1077)
| ~ c6_1(X0)
| sP64(X0) ) ).
cnf(u9364,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ c5_1(X0)
| ~ c1_2(X0,a1100)
| c9_2(X0,a1100)
| c7_2(X0,a1100)
| c9_2(X0,a1149)
| c10_1(X0)
| ~ c2_1(X0)
| ~ sP0(X0) ) ).
cnf(u7295,negated_conjecture,
( ~ c7_2(X0,a1179)
| sP2(X0)
| c3_1(X0)
| ~ c9_1(X0)
| c5_1(X0) ) ).
cnf(u9707,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ c6_1(X0)
| ~ c1_2(X0,a988)
| ~ c5_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a1084)
| c3_2(X0,a988)
| c7_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0) ) ).
cnf(u8231,negated_conjecture,
( c6_2(X0,a988)
| ~ c2_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a1084)
| ~ c6_1(X0)
| sP64(X0) ) ).
cnf(u8463,negated_conjecture,
( c9_2(X0,a1012)
| c9_1(X0)
| c10_2(X0,a1159)
| c1_2(X0,a1012)
| ~ c10_1(X0)
| c4_1(X0)
| c5_1(X0)
| ~ sP54(X0) ) ).
cnf(u540,axiom,
( ~ c10_2(X0,a1157)
| ~ sP11(X0) ) ).
cnf(u10142,negated_conjecture,
( ~ c8_2(X0,a1149)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c9_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c10_2(X0,a1149) ) ).
cnf(u390,axiom,
( ~ c5_2(X0,a1077)
| ~ sP38(X0) ) ).
cnf(u8235,negated_conjecture,
( c3_2(X0,a1084)
| ~ c10_1(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ sP38(X0) ) ).
cnf(u9138,negated_conjecture,
( ~ c1_2(X0,a1077)
| c3_2(X0,a1084)
| ~ sP3(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c10_1(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0) ) ).
cnf(u6408,negated_conjecture,
( ~ c7_2(X0,a976)
| c2_1(X0)
| c3_1(X0)
| ~ c9_1(X0)
| c2_2(X0,a976)
| c7_1(X0) ) ).
cnf(u9866,negated_conjecture,
( ~ c1_2(X0,a969)
| c9_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a1084)
| ~ c5_1(X0)
| c10_2(X0,a1159)
| ~ c10_1(X0)
| ~ sP26(X0)
| c3_2(X0,a1112)
| ~ c3_1(X0) ) ).
cnf(u5657,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| c1_1(X0)
| c4_2(X0,X1)
| c1_2(X0,a1039)
| ~ c10_1(X0) ) ).
cnf(u8614,negated_conjecture,
( c1_2(X0,a1158)
| ~ c5_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ sP10(X0) ) ).
cnf(u8460,negated_conjecture,
c1_2(a1087,a983) ).
cnf(u10219,negated_conjecture,
( ~ c1_2(X0,a1149)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| ~ sP3(X0)
| c7_2(X0,a1077)
| c6_2(X0,a1149) ) ).
cnf(u6554,negated_conjecture,
( c10_2(X0,a976)
| ~ c10_1(X0)
| ~ c3_1(X0)
| c7_1(X0)
| c2_1(X0) ) ).
cnf(u6185,negated_conjecture,
( c2_2(X0,a1100)
| c10_1(X0)
| ~ c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u8817,negated_conjecture,
( ~ c3_2(X0,a1182)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c7_2(X0,a1182)
| c9_2(X0,a1149)
| c10_1(X0)
| ~ sP0(X0) ) ).
cnf(u6950,negated_conjecture,
( ~ c1_2(X0,a983)
| ~ c10_1(X0)
| ~ c2_1(X0)
| c5_1(X0)
| c1_1(X0) ) ).
cnf(u528,axiom,
( ~ c4_2(X0,a1152)
| ~ sP14(X0) ) ).
cnf(u9466,negated_conjecture,
( ~ c10_2(X0,a1049)
| ~ c2_1(X0)
| ~ c5_1(X0)
| c1_2(X0,a1084)
| ~ sP20(X0)
| c8_1(X0)
| ~ c1_1(X0)
| c3_2(X0,a1084)
| c4_2(X0,a1084) ) ).
cnf(u545,axiom,
( c6_2(X0,a1158)
| ~ sP10(X0) ) ).
cnf(u8033,negated_conjecture,
( ~ c5_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0)
| ~ c2_1(X0)
| c9_1(X0)
| c10_2(X0,a1159)
| c7_2(X0,a1157)
| c9_2(X0,a1157) ) ).
cnf(u8921,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c1_2(X0,a1182)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| c7_2(X0,a1182)
| c9_2(X0,a1149)
| c10_1(X0)
| ~ sP0(X0) ) ).
cnf(u9884,negated_conjecture,
( ~ c1_2(X0,a1176)
| ~ c1_1(X0)
| c8_2(X0,X1)
| ~ c2_1(X0)
| c9_1(X0)
| ~ c5_1(X0)
| c3_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_2(X0,a1152)
| ~ c10_1(X0)
| c3_2(X0,a1176)
| ~ sP14(X0) ) ).
cnf(u290,axiom,
( c7_2(X0,a1012)
| ~ sP54(X0) ) ).
cnf(u4648,negated_conjecture,
ndr1_1(a1143) ).
cnf(u7977,negated_conjecture,
( c2_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_1(X0)
| c7_2(X0,a1077)
| ~ c5_1(X0) ) ).
cnf(u4728,negated_conjecture,
( ~ c3_1(X0)
| c1_1(X0)
| ndr1_1(X0) ) ).
cnf(u9389,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ c5_1(X0)
| ~ c1_2(X0,a976)
| c9_2(X0,a976)
| c7_2(X0,a976)
| c9_2(X0,a1149)
| c10_1(X0)
| c7_1(X0)
| ~ sP0(X0) ) ).
cnf(u10173,negated_conjecture,
( ~ c1_2(X0,a1152)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP14(X0) ) ).
cnf(u9914,negated_conjecture,
( ~ c8_2(X0,a1178)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| ~ c5_1(X0)
| ~ c10_2(X0,a1178) ) ).
cnf(u8514,negated_conjecture,
( c2_2(X0,a1159)
| c9_1(X0)
| c9_2(X0,a1101)
| c1_2(X0,a1101)
| ~ c10_1(X0)
| c8_1(X0)
| c1_1(X0) ) ).
cnf(u7072,negated_conjecture,
( ~ c2_2(X0,a1158)
| ~ c3_2(X0,a1158)
| ~ sP10(X0)
| ~ c5_1(X0)
| ~ c7_1(X0) ) ).
cnf(u6844,negated_conjecture,
( c6_2(X0,a1086)
| ~ sP34(X0)
| c5_1(X0)
| c10_2(X0,a1086)
| c8_1(X0) ) ).
cnf(u6325,negated_conjecture,
c3_1(a1170) ).
cnf(u5311,negated_conjecture,
~ c3_1(a963) ).
cnf(u9406,negated_conjecture,
( ~ c1_2(X0,a1086)
| ~ c5_1(X0)
| ~ c1_2(X0,a976)
| c9_2(X0,a976)
| c7_2(X0,a976)
| c9_2(X0,a1149)
| c10_1(X0)
| c7_2(X0,a1086)
| ~ c1_1(X0)
| ~ sP34(X0) ) ).
cnf(u10131,negated_conjecture,
( ~ c5_2(X0,X1)
| c1_2(X0,a1159)
| c7_2(X0,a1159)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c9_2(X0,X1)
| c1_2(X0,X1)
| c7_2(X0,X1) ) ).
cnf(u6979,negated_conjecture,
( c2_2(X0,a1152)
| c10_1(X0)
| ~ sP14(X0)
| ~ c5_1(X0) ) ).
cnf(u5327,negated_conjecture,
( c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u6484,negated_conjecture,
( ~ c7_2(X0,a1176)
| c5_1(X0)
| c5_2(X0,a1176)
| c4_1(X0)
| c4_2(X0,X1)
| c9_1(X0)
| c7_2(X0,X1)
| c3_2(X0,X1) ) ).
cnf(u7183,negated_conjecture,
( ~ c1_2(X0,a1012)
| c5_1(X0)
| ~ sP54(X0)
| c3_1(X0)
| c10_1(X0)
| c4_1(X0) ) ).
cnf(u8669,negated_conjecture,
( ~ c5_2(X0,a983)
| c1_1(X0)
| c1_2(X0,a1039)
| ~ c3_1(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| c1_2(X0,a983) ) ).
cnf(u589,axiom,
( ~ sP3(X0)
| ndr1_1(X0) ) ).
cnf(u9984,negated_conjecture,
( ~ c8_2(X0,X1)
| c9_2(X0,a1149)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c9_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| ~ c1_2(X0,X1) ) ).
cnf(u587,axiom,
( c2_2(X0,a1178)
| ~ sP3(X0) ) ).
cnf(u9749,negated_conjecture,
( ~ c1_2(X0,a1152)
| ~ c10_1(X0)
| ~ sP26(X0)
| ~ c5_1(X0)
| c1_1(X0)
| c4_2(X0,a1112)
| c1_2(X0,a1112)
| c3_2(X0,a1039)
| ~ c2_1(X0)
| ~ sP14(X0) ) ).
cnf(u5908,negated_conjecture,
( ~ c1_2(X0,a1100)
| c1_2(X0,X1)
| c7_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0)
| c3_2(X0,a1100)
| ~ c8_1(X0)
| ~ c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u5577,negated_conjecture,
( ~ c1_2(X0,a1104)
| c9_2(X0,a1097)
| ~ ndr1_1(X0)
| c6_2(X0,a1104)
| ~ c4_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u8633,negated_conjecture,
( c6_2(X0,a1039)
| c1_1(X0)
| c4_2(X0,a1012)
| c1_2(X0,a1012)
| ~ c10_1(X0)
| c4_1(X0)
| c5_1(X0)
| ~ sP54(X0) ) ).
cnf(u415,axiom,
( ~ sP34(X0)
| ndr1_1(X0) ) ).
cnf(u9689,negated_conjecture,
( ~ c1_2(X0,a1152)
| ~ c6_1(X0)
| ~ c1_2(X0,a988)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a1084)
| c3_2(X0,a988)
| ~ sP14(X0) ) ).
cnf(u606,axiom,
( c8_2(X0,a1182)
| ~ sP0(X0) ) ).
cnf(u6501,negated_conjecture,
( ~ c5_2(X0,a1100)
| c10_2(X0,a1159)
| c9_1(X0)
| c9_2(X0,a1100)
| ~ c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u8680,negated_conjecture,
( ~ c10_2(X0,a1128)
| ~ c9_1(X0)
| ~ c10_1(X0)
| ~ sP54(X0)
| c3_1(X0)
| sP20(X0)
| ~ c2_1(X0) ) ).
cnf(u462,axiom,
( ~ c9_2(X0,a1112)
| ~ sP26(X0) ) ).
cnf(u8917,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c1_2(X0,a1152)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| c9_2(X0,a1152)
| c7_2(X0,a1152)
| c9_2(X0,a1149)
| c10_1(X0)
| ~ sP14(X0) ) ).
cnf(u10072,negated_conjecture,
( ~ c1_2(X0,a1100)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c9_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| c9_2(X0,a1149) ) ).
cnf(u9833,negated_conjecture,
( ~ c1_2(X0,a1159)
| ~ c5_1(X0)
| ~ c1_2(X0,a969)
| c9_2(X0,a1159)
| c7_2(X0,a1159)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0)
| ~ c3_1(X0) ) ).
cnf(u8163,negated_conjecture,
( c1_2(X0,a983)
| ~ c3_1(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| c1_1(X0)
| c10_1(X0) ) ).
cnf(u6236,negated_conjecture,
( ~ c9_2(X165,a1159)
| c9_1(X165)
| ~ c8_2(X165,X166)
| ~ c5_2(X165,X166)
| c9_2(X165,X166) ) ).
cnf(u9216,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ c5_1(X0)
| c9_2(X0,a1178)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP3(X0)
| ~ sP0(X0) ) ).
cnf(u9436,negated_conjecture,
( c6_2(X0,a1178)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c10_1(X0)
| ~ c5_1(X0)
| c7_2(X0,a1084)
| c1_2(X0,a1084)
| ~ sP3(X0) ) ).
cnf(u6823,negated_conjecture,
( c8_2(X0,a1077)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0) ) ).
cnf(u6506,negated_conjecture,
( ~ c5_2(X0,X1)
| c10_2(X0,a1159)
| c9_1(X0)
| c9_2(X0,X1)
| c1_2(X0,X1)
| ~ c10_1(X0) ) ).
cnf(u7281,negated_conjecture,
( ~ c5_2(X0,a1179)
| sP2(X0)
| c1_1(X0)
| c6_2(X0,a1039)
| c5_1(X0)
| c4_2(X0,a1179) ) ).
cnf(u9554,negated_conjecture,
( ~ c1_2(X0,a1086)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| c9_2(X0,X1)
| c7_2(X0,X1)
| c9_2(X0,a1149)
| c3_2(X0,X1)
| ~ c2_1(X0)
| c7_2(X0,a1086)
| ~ c1_1(X0)
| ~ sP34(X0) ) ).
cnf(u8234,negated_conjecture,
( c3_2(X0,a1084)
| ~ c10_1(X0)
| ~ c2_1(X0)
| ~ sP64(X0) ) ).
cnf(u9095,negated_conjecture,
( ~ c10_2(X0,a1049)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c10_1(X0)
| ~ c5_1(X0)
| c8_1(X0)
| c1_2(X0,a1122)
| c3_2(X0,a1122)
| c4_2(X0,a1122) ) ).
cnf(u10132,negated_conjecture,
( ~ c5_2(X0,X1)
| c1_2(X0,a1159)
| c7_2(X0,a1159)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c9_2(X0,X1)
| c1_2(X0,X1) ) ).
cnf(u9224,negated_conjecture,
( ~ c1_2(X0,a1100)
| ~ c5_1(X0)
| c9_2(X0,a1178)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP3(X0)
| ~ c2_1(X0) ) ).
cnf(u9211,negated_conjecture,
( ~ c1_2(X0,a1086)
| ~ c5_1(X0)
| c9_2(X0,a1178)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP3(X0)
| c7_2(X0,a1086)
| ~ c1_1(X0)
| ~ sP34(X0)
| ~ c2_1(X0) ) ).
cnf(u7440,negated_conjecture,
( ~ c7_2(X0,a1128)
| sP20(X0)
| ~ c1_2(X0,a1012)
| ~ c10_1(X0)
| ~ sP54(X0)
| ~ c2_1(X0) ) ).
cnf(u8703,negated_conjecture,
( ~ c2_2(X0,a1176)
| c7_2(X0,X1)
| c9_1(X0)
| ~ c1_1(X0)
| c8_2(X0,X1)
| ~ c2_1(X0)
| ~ c3_2(X0,a1176)
| c3_2(X0,X1)
| ~ c5_1(X0)
| ~ c7_1(X0) ) ).
cnf(u8042,negated_conjecture,
( ~ c10_2(X0,a1097)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ sP64(X0)
| c1_2(X0,a1097) ) ).
cnf(u8704,negated_conjecture,
( ~ c2_2(X0,a1176)
| c7_2(X0,X1)
| c9_1(X0)
| ~ c1_1(X0)
| c8_2(X0,X1)
| ~ c2_1(X0)
| ~ c1_2(X0,a1176)
| ~ c5_1(X0)
| c3_2(X0,X1)
| ~ c8_2(X0,X2)
| ~ c1_2(X0,X2) ) ).
cnf(u9740,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ sP26(X0)
| c9_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a1084)
| ~ c5_1(X0)
| c10_2(X0,a1159)
| ~ c10_1(X0)
| ~ c1_2(X0,X1)
| c3_2(X0,a1112) ) ).
cnf(u391,axiom,
( c4_2(X0,a1077)
| ~ sP38(X0) ) ).
cnf(u229,axiom,
( ~ sP64(X0)
| ndr1_1(X0) ) ).
cnf(u9602,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ c2_1(X0)
| c10_1(X0)
| c7_2(X0,a1157)
| ~ c5_1(X0)
| ~ c1_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0)
| ~ sP0(X0) ) ).
cnf(u543,axiom,
( ~ sP11(X0)
| ndr1_1(X0) ) ).
cnf(u4641,negated_conjecture,
( c9_1(X7)
| ndr1_1(X7) ) ).
cnf(u6552,negated_conjecture,
( ~ c7_2(X0,X1)
| c1_2(X0,X1)
| ~ c10_1(X0)
| ~ c3_1(X0)
| c4_1(X0)
| c5_1(X0)
| c5_2(X0,X1)
| c10_2(X0,X1) ) ).
cnf(u8615,negated_conjecture,
( ~ c10_2(X0,a1086)
| c1_2(X0,a1086)
| c7_2(X0,a1086)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ sP34(X0)
| ~ c5_1(X0) ) ).
cnf(u8591,negated_conjecture,
( c7_2(X0,a989)
| c1_2(X0,a989)
| ~ c5_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ sP64(X0) ) ).
cnf(u412,axiom,
( c4_2(X0,a1086)
| ~ sP34(X0) ) ).
cnf(u9465,negated_conjecture,
( c4_2(X0,a1084)
| ~ c2_1(X0)
| ~ c5_1(X0)
| c1_2(X0,a1084)
| ~ sP20(X0)
| c8_1(X0)
| c8_2(X0,a1049)
| c3_2(X0,a1084)
| ~ c1_1(X0) ) ).
cnf(u9903,negated_conjecture,
( ~ c1_2(X0,a1176)
| ~ c1_1(X0)
| c8_2(X0,X1)
| ~ c2_1(X0)
| c9_1(X0)
| ~ c5_1(X0)
| c3_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_2(X0,a1157)
| c3_2(X0,a1176)
| c7_2(X0,a1157)
| ~ sP11(X0) ) ).
cnf(u9896,negated_conjecture,
( ~ c1_2(X0,a1176)
| ~ c1_1(X0)
| c8_2(X0,X1)
| ~ c2_1(X0)
| c9_1(X0)
| ~ c5_1(X0)
| c3_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_2(X0,a1100)
| ~ c10_1(X0)
| c3_2(X0,a1176) ) ).
cnf(u9610,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ c2_1(X0)
| c10_1(X0)
| c7_2(X0,a1157)
| ~ c5_1(X0)
| ~ sP11(X0)
| ~ c1_1(X0) ) ).
cnf(u546,axiom,
( ~ c7_2(X0,a1158)
| ~ sP10(X0) ) ).
cnf(u8243,negated_conjecture,
( ~ c1_2(X0,a1084)
| ~ c2_1(X0)
| ~ sP20(X0)
| c5_1(X0)
| ~ c10_1(X0)
| c1_1(X0) ) ).
cnf(u10121,negated_conjecture,
( ~ c5_2(X0,a1157)
| c1_2(X0,a1159)
| c7_2(X0,a1159)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c9_2(X0,a1157)
| c7_2(X0,a1157)
| ~ sP11(X0) ) ).
cnf(u7163,negated_conjecture,
( ~ c5_2(X0,a1182)
| c9_1(X0)
| c10_2(X0,a1159)
| ~ sP0(X0) ) ).
cnf(u9014,negated_conjecture,
( ~ c3_2(X0,a1159)
| c9_2(X0,a1101)
| c1_2(X0,a1101)
| ~ c10_1(X0)
| c8_1(X0)
| c1_1(X0)
| c9_1(X0)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c9_2(X0,a1159)
| c7_2(X0,a1159)
| c9_2(X0,a1149) ) ).
cnf(u9191,negated_conjecture,
( ~ c8_2(X0,a1012)
| c10_2(X0,a1159)
| c1_2(X0,a1012)
| ~ c10_1(X0)
| c4_1(X0)
| c5_1(X0)
| ~ sP54(X0)
| c9_1(X0)
| ~ c10_2(X0,a1012) ) ).
cnf(u9127,negated_conjecture,
( ~ c1_2(X0,a1182)
| c3_2(X0,a1084)
| ~ sP3(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c10_1(X0)
| ~ sP0(X0) ) ).
cnf(u5169,negated_conjecture,
( c6_2(X0,a1101)
| ~ c6_1(X0)
| c2_2(X0,a1101)
| c8_1(X0)
| c1_1(X0) ) ).
cnf(u9103,negated_conjecture,
( ~ c10_2(X0,a1149)
| c7_2(X0,a1077)
| ~ sP38(X0)
| ~ c5_1(X0)
| ~ c10_1(X0)
| c9_2(X0,a1077)
| c1_2(X0,a1149) ) ).
cnf(u291,axiom,
( c6_2(X0,a1012)
| ~ sP54(X0) ) ).
cnf(u10033,negated_conjecture,
( ~ c1_2(X0,a1149)
| c7_2(X0,a988)
| ~ c5_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a988)
| ~ c2_1(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| c10_2(X0,a1077)
| ~ c6_1(X0)
| c9_2(X0,a1097)
| c6_2(X0,a1149)
| c9_2(X0,a988) ) ).
cnf(u9142,negated_conjecture,
( ~ c1_2(X0,a1086)
| ~ sP3(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a1084)
| c7_2(X0,a1086)
| ~ c1_1(X0)
| ~ sP34(X0) ) ).
cnf(u9015,negated_conjecture,
( ~ c8_2(X0,X1)
| c9_2(X0,a1101)
| c1_2(X0,a1101)
| ~ c10_1(X0)
| c8_1(X0)
| c1_1(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,a1159)
| c9_1(X0)
| ~ c1_2(X0,X1)
| c9_2(X0,a1159)
| c7_2(X0,a1159)
| c9_2(X0,a1149) ) ).
cnf(u9019,negated_conjecture,
( ~ c1_2(X0,a969)
| ~ c5_1(X0)
| ~ sP10(X0)
| ~ c10_1(X0)
| c3_2(X0,a1158)
| ~ c2_1(X0)
| c9_1(X0)
| ~ c3_1(X0) ) ).
cnf(u9124,negated_conjecture,
( ~ c1_2(X0,a1152)
| c3_2(X0,a1084)
| ~ sP3(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c10_1(X0)
| ~ sP14(X0) ) ).
cnf(u9407,negated_conjecture,
( ~ c1_2(X0,a1077)
| ~ c5_1(X0)
| ~ c1_2(X0,a976)
| c9_2(X0,a976)
| c7_2(X0,a976)
| c9_2(X0,a1149)
| c10_1(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0) ) ).
cnf(u9025,negated_conjecture,
( ~ c1_2(X0,a1152)
| ~ c5_1(X0)
| ~ sP10(X0)
| ~ c10_1(X0)
| c3_2(X0,a1158)
| ~ c2_1(X0)
| ~ sP14(X0) ) ).
cnf(u8750,negated_conjecture,
( ~ c7_2(X0,a1128)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ sP38(X0)
| sP20(X0)
| ~ c10_1(X0)
| ~ c1_2(X0,a1084)
| ~ c7_2(X0,a1084) ) ).
cnf(u8104,negated_conjecture,
( ~ c1_2(X0,a1149)
| c9_2(X0,a1077)
| c7_2(X0,a1077)
| ~ sP38(X0)
| ~ c4_1(X0)
| c9_2(X0,a1097)
| c6_2(X0,a1149)
| ~ c5_1(X0) ) ).
cnf(u6984,negated_conjecture,
( ~ c1_2(X0,a1152)
| ~ c8_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| c3_2(X0,X1)
| c3_2(X0,a1152)
| ~ sP14(X0) ) ).
cnf(u9864,negated_conjecture,
( ~ c1_2(X0,a1077)
| c9_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a1084)
| ~ c5_1(X0)
| c10_2(X0,a1159)
| ~ c10_1(X0)
| ~ sP26(X0)
| c3_2(X0,a1112)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0) ) ).
cnf(u9692,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ c6_1(X0)
| ~ c1_2(X0,a988)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a1084)
| c3_2(X0,a988)
| ~ sP0(X0) ) ).
cnf(u6237,negated_conjecture,
( ~ c8_2(X165,X166)
| c9_1(X165)
| c2_2(X165,a1159)
| ~ c5_2(X165,X166)
| c9_2(X165,X166) ) ).
cnf(u9210,negated_conjecture,
( ~ c1_2(X0,a1077)
| ~ c5_1(X0)
| c9_2(X0,a1178)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0) ) ).
cnf(u590,axiom,
( ~ c1_2(X0,a1180)
| ~ sP2(X0) ) ).
cnf(u10074,negated_conjecture,
( ~ c1_2(X0,a1077)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c9_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| c9_2(X0,a1149) ) ).
cnf(u8634,negated_conjecture,
( c6_2(X0,a1039)
| c1_1(X0)
| c4_2(X0,a1112)
| c1_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0) ) ).
cnf(u8925,negated_conjecture,
( ~ c7_2(X0,a1039)
| c4_2(X0,a1112)
| c1_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0)
| c4_1(X0)
| c5_1(X0)
| c5_2(X0,a1039)
| c1_1(X0) ) ).
cnf(u9447,negated_conjecture,
( c7_2(X0,a1084)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c10_1(X0)
| ~ c5_1(X0)
| c1_2(X0,a1084)
| ~ sP20(X0) ) ).
cnf(u6998,negated_conjecture,
( ~ c5_2(X0,a1152)
| c1_1(X0)
| c6_2(X0,a1039)
| ~ sP14(X0) ) ).
cnf(u9831,negated_conjecture,
( ~ c1_2(X0,a1159)
| ~ c5_1(X0)
| ~ c1_2(X0,a1100)
| c9_2(X0,a1159)
| c7_2(X0,a1159)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0)
| ~ c2_1(X0) ) ).
cnf(u6235,negated_conjecture,
( ~ c8_2(X165,X166)
| c9_1(X165)
| c10_2(X165,a1159)
| ~ c5_2(X165,X166)
| c9_2(X165,X166) ) ).
cnf(u8888,negated_conjecture,
( ~ c1_2(X0,a1086)
| c1_2(X0,a1097)
| ~ c10_1(X0)
| ~ c3_1(X0)
| ~ c4_1(X0)
| c10_2(X0,a1097)
| c6_2(X0,a1086)
| ~ sP34(X0) ) ).
cnf(u9669,negated_conjecture,
( ~ c1_2(X0,a1100)
| c10_1(X0)
| ~ c5_1(X0)
| c7_2(X0,a1084)
| c1_2(X0,a1084)
| ~ sP3(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u9118,negated_conjecture,
( ~ c1_2(X0,a969)
| c3_2(X0,a1084)
| ~ sP3(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c10_1(X0)
| c9_1(X0)
| ~ c3_1(X0) ) ).
cnf(u6866,negated_conjecture,
( ~ c1_2(X0,a1086)
| ~ c4_1(X0)
| c9_2(X0,a1097)
| c6_2(X0,a1086)
| ~ sP34(X0) ) ).
cnf(u8918,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c1_2(X0,a1100)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| c9_2(X0,a1100)
| c7_2(X0,a1100)
| c9_2(X0,a1149)
| c10_1(X0)
| ~ c2_1(X0) ) ).
cnf(u8681,negated_conjecture,
( ~ sP54(X0)
| ~ c9_1(X0)
| ~ c10_1(X0)
| c3_1(X0)
| ~ c2_1(X0)
| c5_1(X0) ) ).
cnf(u463,axiom,
( ~ sP26(X0)
| ndr1_1(X0) ) ).
cnf(u7137,negated_conjecture,
( ~ c1_2(X0,a1012)
| ~ sP54(X0)
| ~ c2_1(X0)
| c5_1(X0)
| ~ c10_1(X0)
| c1_1(X0) ) ).
cnf(u7421,negated_conjecture,
( ~ c7_2(X0,a983)
| ~ c10_2(X0,a1128)
| ~ c1_2(X0,a983)
| sP20(X0)
| c1_1(X0)
| ~ c10_1(X0)
| ~ c2_1(X0) ) ).
cnf(u497,axiom,
( c1_2(X0,a1129)
| ~ sP20(X0) ) ).
cnf(u10079,negated_conjecture,
( ~ c1_2(X0,a1086)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| c9_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| c7_2(X0,a1086)
| ~ sP34(X0) ) ).
cnf(u7641,negated_conjecture,
( c9_2(X0,a1097)
| ~ c4_1(X0)
| ~ sP64(X0)
| ~ c10_1(X0) ) ).
cnf(u9312,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ c5_1(X0)
| c7_2(X0,a1182)
| c9_2(X0,a1149)
| c10_1(X0)
| ~ sP0(X0) ) ).
cnf(u8032,negated_conjecture,
( c2_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0)
| ~ c2_1(X0)
| c10_1(X0)
| c7_2(X0,a1157)
| ~ c5_1(X0) ) ).
cnf(u9578,negated_conjecture,
( ~ c2_2(X0,a988)
| ~ c2_1(X0)
| c10_1(X0)
| ~ c5_1(X0)
| c7_2(X0,a1084)
| c1_2(X0,a1084)
| ~ c6_1(X0)
| sP64(X0)
| ~ c1_1(X0)
| ~ c8_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u10207,negated_conjecture,
( c9_2(X0,a1149)
| c7_2(X0,a1159)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c1_2(X0,a1159)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c8_1(X0) ) ).
cnf(u8156,negated_conjecture,
( ~ c5_2(X0,a983)
| ~ c3_1(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| c1_2(X0,a983)
| c9_1(X0)
| c10_2(X0,a1159)
| c1_1(X0)
| c9_2(X0,a983) ) ).
cnf(u10193,negated_conjecture,
( ~ c1_2(X0,a969)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| c9_1(X0) ) ).
cnf(u6510,negated_conjecture,
( ~ c5_2(X0,a976)
| c2_2(X0,a1159)
| c9_1(X0)
| c9_2(X0,a976)
| c7_1(X0)
| c2_1(X0) ) ).
cnf(u9850,negated_conjecture,
( ~ c1_2(X0,a1152)
| c9_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a1084)
| ~ c5_1(X0)
| c10_2(X0,a1159)
| ~ c10_1(X0)
| ~ sP26(X0)
| c3_2(X0,a1112)
| ~ sP14(X0) ) ).
cnf(u8755,negated_conjecture,
( c6_2(X0,a1112)
| c10_2(X0,a1159)
| ~ c10_1(X0)
| ~ sP26(X0)
| c9_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a1084) ) ).
cnf(u9213,negated_conjecture,
( ~ c1_2(X0,a1152)
| ~ c5_1(X0)
| c9_2(X0,a1178)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP3(X0)
| ~ sP14(X0) ) ).
cnf(u8867,negated_conjecture,
( c4_2(X0,a989)
| ~ c5_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ sP64(X0)
| c8_1(X0)
| c8_2(X0,a1049)
| c3_2(X0,a989)
| c1_2(X0,a989) ) ).
cnf(u9445,negated_conjecture,
( c6_2(X0,a1110)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c10_1(X0)
| ~ c5_1(X0)
| c7_2(X0,a1084)
| c1_2(X0,a1084) ) ).
cnf(u7799,negated_conjecture,
~ c7_2(a1153,a1122) ).
cnf(u8469,negated_conjecture,
( c1_2(X0,a1112)
| c9_1(X0)
| c10_2(X0,a1159)
| ~ c10_1(X0)
| ~ sP26(X0) ) ).
cnf(u7419,negated_conjecture,
( ~ c7_2(X0,a1086)
| ~ c10_2(X0,a1128)
| ~ c1_2(X0,a1086)
| sP20(X0)
| ~ c10_1(X0)
| ~ sP34(X0)
| ~ c2_1(X0) ) ).
cnf(u5766,negated_conjecture,
( ~ c10_1(X0)
| ~ ndr1_1(X0)
| ~ c2_1(X0)
| c3_1(X0) ) ).
cnf(u8919,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c1_2(X0,a976)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| c9_2(X0,a976)
| c7_2(X0,a976)
| c9_2(X0,a1149)
| c10_1(X0)
| c7_1(X0) ) ).
cnf(u8960,negated_conjecture,
( c6_2(X0,a1112)
| c1_2(X0,a1039)
| ~ c10_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| c1_1(X0)
| c5_1(X0)
| c10_2(X0,a1112)
| c8_1(X0) ) ).
cnf(u530,axiom,
( ~ c10_2(X0,a1152)
| ~ sP14(X0) ) ).
cnf(u9869,negated_conjecture,
( ~ c1_2(X0,a1157)
| c9_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a1084)
| ~ c5_1(X0)
| c10_2(X0,a1159)
| ~ sP26(X0)
| c3_2(X0,a1112)
| c7_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0) ) ).
cnf(u8227,negated_conjecture,
( c6_2(X0,a1178)
| ~ c2_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a1084)
| ~ sP3(X0) ) ).
cnf(u5369,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ c9_1(X0)
| ~ ndr1_1(X0)
| c2_2(X0,X1)
| c3_1(X0)
| c1_2(X0,X1)
| ~ c10_1(X0) ) ).
cnf(u9823,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ c5_1(X0)
| ~ c1_2(X0,a1159)
| c9_2(X0,a1159)
| c7_2(X0,a1159)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0)
| ~ sP0(X0) ) ).
cnf(u4642,negated_conjecture,
ndr1_1(a1135) ).
cnf(u8620,negated_conjecture,
( c2_2(X0,a1112)
| ~ c9_1(X0)
| c3_1(X0)
| c1_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0) ) ).
cnf(u7914,negated_conjecture,
c3_1(a1079) ).
cnf(u9512,negated_conjecture,
( ~ c1_2(X0,a969)
| ~ c5_1(X0)
| c9_2(X0,a969)
| c7_2(X0,a969)
| c9_2(X0,a1149)
| c10_1(X0)
| c9_1(X0)
| ~ c3_1(X0) ) ).
cnf(u6039,negated_conjecture,
~ c3_1(a1125) ).
cnf(u4637,negated_conjecture,
( c4_1(X64)
| ndr1_1(X64) ) ).
cnf(u9270,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ sP11(X0)
| ~ c5_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a1157)
| ~ c2_1(X0)
| c7_2(X0,a1157)
| ~ c1_1(X0) ) ).
cnf(u7992,negated_conjecture,
( ~ c10_2(X0,a1086)
| ~ c1_1(X0)
| ~ sP34(X0)
| ~ c2_1(X0)
| ~ c10_1(X0)
| c7_2(X0,a1086) ) ).
cnf(u413,axiom,
( c9_2(X0,a1086)
| ~ sP34(X0) ) ).
cnf(u10246,negated_conjecture,
( ~ c1_2(X0,a1149)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c1_2(X0,a1159)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c9_2(X0,a1097)
| c6_2(X0,a1149)
| c7_2(X0,a1159) ) ).
cnf(u10163,negated_conjecture,
( ~ c10_2(X0,a1149)
| ~ c5_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a988)
| ~ c2_1(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| c10_2(X0,a1077)
| ~ c6_1(X0)
| sP64(X0)
| c9_2(X0,a988)
| c7_2(X0,a988)
| c1_2(X0,a1149) ) ).
cnf(u9361,negated_conjecture,
( ~ c1_2(X0,a1152)
| ~ c5_1(X0)
| ~ c1_2(X0,a1100)
| c9_2(X0,a1100)
| c7_2(X0,a1100)
| c9_2(X0,a1149)
| c10_1(X0)
| ~ c2_1(X0)
| ~ sP14(X0) ) ).
cnf(u9250,negated_conjecture,
( ~ c10_2(X0,a1149)
| c9_2(X0,a976)
| c7_2(X0,a976)
| c7_1(X0)
| c2_1(X0)
| ~ c10_1(X0)
| ~ c5_1(X0)
| c1_2(X0,a1149) ) ).
cnf(u9708,negated_conjecture,
( ~ c1_2(X0,a1086)
| ~ c6_1(X0)
| ~ c1_2(X0,a988)
| ~ c5_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a1084)
| c3_2(X0,a988)
| c7_2(X0,a1086)
| ~ c1_1(X0)
| ~ sP34(X0) ) ).
cnf(u6242,negated_conjecture,
( ~ c7_2(X0,a1100)
| ~ c9_1(X0)
| c2_2(X0,a1100)
| c3_1(X0)
| ~ c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u8103,negated_conjecture,
( ~ c8_2(X0,a1149)
| c9_2(X0,a1077)
| c7_2(X0,a1077)
| ~ sP38(X0)
| ~ c5_1(X0)
| ~ c10_1(X0)
| ~ c10_2(X0,a1149) ) ).
cnf(u6825,negated_conjecture,
( c10_2(X0,a1077)
| c5_1(X0)
| ~ sP38(X0)
| c8_1(X0) ) ).
cnf(u6981,negated_conjecture,
( ~ c5_2(X0,a1152)
| c9_1(X0)
| c2_2(X0,a1159)
| ~ sP14(X0)
| c9_2(X0,a1152) ) ).
cnf(u4763,negated_conjecture,
c4_1(a1170) ).
cnf(u8948,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ sP11(X0)
| ~ c2_1(X0)
| c10_1(X0)
| c7_2(X0,a1157)
| ~ c5_1(X0)
| ~ c1_2(X0,a1157)
| ~ c1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u8886,negated_conjecture,
( ~ c1_2(X0,a1149)
| c1_2(X0,a1097)
| ~ c10_1(X0)
| ~ c3_1(X0)
| ~ c4_1(X0)
| c10_2(X0,a1097)
| c6_2(X0,a1149)
| ~ c5_1(X0)
| c9_2(X0,a1129)
| c7_2(X0,a1129)
| ~ sP20(X0) ) ).
cnf(u6831,negated_conjecture,
( c1_2(X0,a1077)
| c10_2(X0,a1077)
| ~ sP38(X0)
| ~ c10_1(X0)
| ~ c3_1(X0) ) ).
cnf(u460,axiom,
( c5_2(X0,a1112)
| ~ sP26(X0) ) ).
cnf(u8868,negated_conjecture,
( ~ c10_2(X0,a1049)
| ~ c5_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ sP64(X0)
| c8_1(X0)
| c1_2(X0,a989)
| c3_2(X0,a989)
| c4_2(X0,a989) ) ).
cnf(u9502,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ c5_1(X0)
| ~ c1_2(X0,a969)
| c9_2(X0,a969)
| c7_2(X0,a969)
| c9_2(X0,a1149)
| c10_1(X0)
| c9_1(X0)
| ~ c3_1(X0)
| ~ sP0(X0) ) ).
cnf(u8526,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c5_1(X0)
| ~ sP11(X0)
| ~ c1_2(X0,a1157)
| ~ c1_2(X0,X1)
| ~ c10_1(X0)
| c3_2(X0,a1157)
| ~ c2_1(X0) ) ).
cnf(u7437,negated_conjecture,
( ~ c7_2(X0,a1128)
| sP20(X0)
| ~ c1_2(X0,a1086)
| ~ c7_2(X0,a1086)
| ~ c10_1(X0)
| ~ sP34(X0)
| ~ c2_1(X0) ) ).
cnf(u9277,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ sP11(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,a1086)
| c3_2(X0,a1157)
| ~ c2_1(X0)
| c7_2(X0,a1086)
| ~ c1_1(X0)
| ~ sP34(X0) ) ).
cnf(u9136,negated_conjecture,
( ~ c1_2(X0,a1100)
| c3_2(X0,a1084)
| ~ sP3(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c10_1(X0) ) ).
cnf(u8887,negated_conjecture,
( ~ c1_2(X0,a1149)
| c1_2(X0,a1097)
| ~ c10_1(X0)
| ~ c3_1(X0)
| ~ c4_1(X0)
| c10_2(X0,a1097)
| c6_2(X0,a1149)
| c2_1(X0)
| ~ c5_1(X0)
| c9_2(X0,a976)
| c7_2(X0,a976)
| c7_1(X0) ) ).
cnf(u10192,negated_conjecture,
( ~ c1_2(X0,a1086)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| c7_2(X0,a1086)
| ~ sP34(X0) ) ).
cnf(u9954,negated_conjecture,
( ~ c1_2(X0,a1159)
| c1_2(X0,a1101)
| ~ c10_1(X0)
| c1_1(X0)
| ~ c5_1(X0)
| c9_2(X0,a1101)
| c9_1(X0)
| ~ c1_2(X0,a969)
| c9_2(X0,a1159)
| c7_2(X0,a1159)
| c9_2(X0,a1149)
| ~ c3_1(X0) ) ).
cnf(u8665,negated_conjecture,
( ~ c5_2(X0,X1)
| c1_1(X0)
| c4_2(X0,X1)
| c1_2(X0,a1039)
| ~ c10_1(X0)
| c1_2(X0,X1) ) ).
cnf(u6882,negated_conjecture,
( c3_2(X0,a1086)
| ~ c10_1(X0)
| ~ sP34(X0)
| ~ c2_1(X0) ) ).
cnf(u9674,negated_conjecture,
( ~ c1_2(X0,a969)
| c10_1(X0)
| ~ c5_1(X0)
| c7_2(X0,a1084)
| c1_2(X0,a1084)
| ~ sP3(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c9_1(X0) ) ).
cnf(u9558,negated_conjecture,
( c3_2(X0,a1158)
| ~ sP10(X0)
| ~ c10_1(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| c10_2(X0,a1077) ) ).
cnf(u9941,negated_conjecture,
( ~ c1_2(X0,a1182)
| c1_2(X0,a1101)
| ~ c10_1(X0)
| c8_1(X0)
| c1_1(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,a1159)
| c9_1(X0)
| c9_2(X0,a1101)
| c9_2(X0,a1159)
| c7_2(X0,a1159)
| c9_2(X0,a1149)
| ~ sP0(X0) ) ).
cnf(u9938,negated_conjecture,
( ~ c1_2(X0,a1159)
| c1_2(X0,a1101)
| ~ c10_1(X0)
| c8_1(X0)
| c1_1(X0)
| ~ c5_1(X0)
| c9_2(X0,a1101)
| c9_1(X0)
| ~ c1_2(X0,a1152)
| c9_2(X0,a1159)
| c7_2(X0,a1159)
| c9_2(X0,a1149)
| ~ sP14(X0) ) ).
cnf(u5478,negated_conjecture,
( c6_2(X0,a1176)
| c3_2(X0,X1)
| ~ ndr1_1(X0)
| c7_2(X0,X1)
| c9_1(X0)
| ~ c1_1(X0)
| c8_2(X0,X1)
| ~ c2_1(X0) ) ).
cnf(u9723,negated_conjecture,
( ~ c8_2(X0,X1)
| c1_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0)
| ~ c5_1(X0)
| c1_1(X0)
| c4_2(X0,a1112)
| ~ c1_2(X0,X1)
| c3_2(X0,a1039)
| ~ c2_1(X0) ) ).
cnf(u5140,negated_conjecture,
( ~ c8_2(X0,a1104)
| ~ ndr1_1(X0)
| ~ c10_1(X0)
| ~ c10_2(X0,a1104)
| c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u9743,negated_conjecture,
( ~ c1_2(X0,a969)
| ~ c10_1(X0)
| ~ sP26(X0)
| ~ c5_1(X0)
| c1_1(X0)
| c4_2(X0,a1112)
| c1_2(X0,a1112)
| c3_2(X0,a1039)
| ~ c2_1(X0)
| c9_1(X0)
| ~ c3_1(X0) ) ).
cnf(u9983,negated_conjecture,
( ~ c3_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| c9_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| ~ c7_1(X0) ) ).
cnf(u9176,negated_conjecture,
( ~ c2_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0)
| c9_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a1084)
| ~ c5_1(X0)
| c10_2(X0,a1159)
| ~ c8_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u10255,negated_conjecture,
( ~ c10_2(X0,a1149)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c1_2(X0,a1159)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c7_2(X0,a1159)
| ~ sP38(X0)
| c1_2(X0,a1149)
| c7_2(X0,a1149) ) ).
cnf(u7165,negated_conjecture,
( ~ c7_2(X0,a1182)
| c3_1(X0)
| ~ c9_1(X0)
| c2_2(X0,a1182)
| ~ sP0(X0) ) ).
cnf(u6351,negated_conjecture,
( c3_2(X0,a983)
| c1_1(X0)
| ~ c10_1(X0)
| ~ c2_1(X0) ) ).
cnf(u8913,negated_conjecture,
( ~ c8_2(X0,X2)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,X2)
| c9_2(X0,X1)
| c7_2(X0,X1)
| c9_2(X0,a1149)
| ~ c10_1(X0)
| c3_2(X0,X1)
| ~ c2_1(X0) ) ).
cnf(u10191,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| c7_2(X0,a1157)
| ~ sP11(X0) ) ).
cnf(u9380,negated_conjecture,
( ~ c1_2(X0,a976)
| ~ c5_1(X0)
| ~ c1_2(X0,a969)
| c9_2(X0,a976)
| c7_2(X0,a976)
| c9_2(X0,a1149)
| c10_1(X0)
| c7_1(X0)
| c9_1(X0)
| ~ c3_1(X0) ) ).
cnf(u8660,negated_conjecture,
( ~ c5_2(X0,a1179)
| c1_1(X0)
| c4_2(X0,a1179)
| c1_2(X0,a1039)
| ~ c10_1(X0)
| c5_1(X0)
| sP2(X0) ) ).
cnf(u6526,negated_conjecture,
( ~ c2_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c9_2(X0,X1)
| c7_2(X0,X1)
| c9_2(X0,a1149) ) ).
cnf(u9678,negated_conjecture,
( c9_2(X0,a1178)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0) ) ).
cnf(u5480,negated_conjecture,
( c6_2(X0,a1176)
| c6_2(X0,X1)
| c7_2(X0,X1)
| c3_2(X0,X1)
| c9_1(X0)
| c5_1(X0)
| c10_2(X0,X1)
| c8_1(X0) ) ).
cnf(u228,axiom,
( ~ c6_2(X0,a989)
| ~ sP64(X0) ) ).
cnf(u8839,negated_conjecture,
( ~ c2_2(X0,a988)
| ~ c10_1(X0)
| c3_2(X0,a1084)
| ~ c6_1(X0)
| ~ c1_2(X0,a988)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c8_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u9341,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ c5_1(X0)
| ~ c1_2(X0,a1152)
| c9_2(X0,a1152)
| c7_2(X0,a1152)
| c9_2(X0,a1149)
| c10_1(X0)
| ~ sP14(X0)
| ~ sP0(X0) ) ).
cnf(u9817,negated_conjecture,
( ~ c1_2(X0,a1159)
| ~ c5_1(X0)
| ~ c1_2(X0,a1077)
| c9_2(X0,a1159)
| c7_2(X0,a1159)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0) ) ).
cnf(u6409,negated_conjecture,
( ~ c5_2(X0,a976)
| c2_1(X0)
| c1_1(X0)
| c6_2(X0,a1039)
| c7_1(X0)
| c4_2(X0,a976) ) ).
cnf(u9836,negated_conjecture,
( ~ c1_2(X0,a1159)
| ~ c5_1(X0)
| ~ c1_2(X0,a1157)
| c9_2(X0,a1159)
| c7_2(X0,a1159)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| c7_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0)
| ~ c2_1(X0) ) ).
cnf(u498,axiom,
( ~ c4_2(X0,a1129)
| ~ sP20(X0) ) ).
cnf(u7439,negated_conjecture,
( ~ c7_2(X0,a1128)
| sP20(X0)
| ~ c1_2(X0,a983)
| ~ c7_2(X0,a983)
| c1_1(X0)
| ~ c10_1(X0)
| ~ c2_1(X0) ) ).
cnf(u9701,negated_conjecture,
( ~ c1_2(X0,a1100)
| ~ c6_1(X0)
| ~ c1_2(X0,a988)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a1084)
| c3_2(X0,a988) ) ).
cnf(u8952,negated_conjecture,
( c4_2(X0,a1012)
| c1_1(X0)
| c1_2(X0,a1039)
| ~ c10_1(X0)
| c1_2(X0,a1012)
| c4_1(X0)
| c5_1(X0)
| ~ sP54(X0) ) ).
cnf(u9870,negated_conjecture,
( ~ c1_2(X0,a1086)
| c9_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a1084)
| ~ c5_1(X0)
| c10_2(X0,a1159)
| ~ sP26(X0)
| c3_2(X0,a1112)
| c7_2(X0,a1086)
| ~ c1_1(X0)
| ~ sP34(X0) ) ).
cnf(u496,axiom,
( ~ c6_2(X0,a1129)
| ~ sP20(X0) ) ).
cnf(u9214,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ c5_1(X0)
| c9_2(X0,a1178)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP3(X0)
| c7_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0)
| ~ c2_1(X0) ) ).
cnf(u8773,negated_conjecture,
( c6_2(X0,a1176)
| c7_2(X0,a1176)
| c3_2(X0,a1176)
| c9_1(X0)
| c5_1(X0)
| c10_2(X0,a1176)
| c8_1(X0) ) ).
cnf(u6905,negated_conjecture,
( c4_2(X0,a1112)
| c8_1(X0)
| c8_2(X0,a1049)
| c3_2(X0,a1112)
| ~ sP26(X0) ) ).
cnf(u541,axiom,
( c6_2(X0,a1157)
| ~ sP11(X0) ) ).
cnf(u8592,negated_conjecture,
( ~ c5_2(X0,X1)
| c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c9_1(X0)
| c2_2(X0,a1159)
| ~ c5_1(X0)
| c9_2(X0,X1) ) ).
cnf(u7718,negated_conjecture,
( ~ c8_2(X0,a1097)
| ~ sP64(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c10_2(X0,a1097) ) ).
cnf(u8664,negated_conjecture,
( ~ c5_2(X0,a976)
| c1_1(X0)
| c4_2(X0,a976)
| c1_2(X0,a1039)
| ~ c10_1(X0)
| c7_1(X0)
| c2_1(X0) ) ).
cnf(u9135,negated_conjecture,
( ~ c1_2(X0,a1157)
| c3_2(X0,a1084)
| ~ sP3(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c10_1(X0)
| c7_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0) ) ).
cnf(u10063,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c9_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP0(X0) ) ).
cnf(u8748,negated_conjecture,
( ~ c1_2(X0,a1084)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ sP38(X0)
| c5_1(X0)
| ~ c10_1(X0)
| c1_1(X0) ) ).
cnf(u6549,negated_conjecture,
( ~ c9_2(X0,X1)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| ~ c10_1(X0)
| ~ c3_1(X0)
| ~ c4_1(X0)
| ~ c1_2(X0,X1)
| c6_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u9028,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ c5_1(X0)
| ~ sP10(X0)
| ~ c10_1(X0)
| c3_2(X0,a1158)
| ~ c2_1(X0)
| ~ sP0(X0) ) ).
cnf(u414,axiom,
( ~ c2_2(X0,a1086)
| ~ sP34(X0) ) ).
cnf(u6575,negated_conjecture,
( ~ c2_2(X0,X1)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X2)
| ~ c1_2(X0,X2)
| c9_2(X0,X1)
| c7_2(X0,X1)
| c9_2(X0,a1149) ) ).
cnf(u7993,negated_conjecture,
( c7_2(X0,a1086)
| ~ c1_1(X0)
| ~ sP34(X0)
| ~ c2_1(X0)
| c10_1(X0)
| ~ c5_1(X0) ) ).
cnf(u9549,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| c9_2(X0,X1)
| c7_2(X0,X1)
| c9_2(X0,a1149)
| ~ c10_1(X0)
| c3_2(X0,X1)
| ~ c2_1(X0)
| c7_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0) ) ).
cnf(u9862,negated_conjecture,
( ~ c1_2(X0,a1100)
| c9_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a1084)
| ~ c5_1(X0)
| c10_2(X0,a1159)
| ~ c10_1(X0)
| ~ sP26(X0)
| c3_2(X0,a1112) ) ).
cnf(u5627,negated_conjecture,
( ~ c5_2(X0,X1)
| c6_2(X0,a1039)
| ~ ndr1_1(X0)
| c1_1(X0)
| c4_2(X0,X1)
| c1_2(X0,X1)
| ~ c10_1(X0) ) ).
cnf(u8778,negated_conjecture,
( ~ c7_2(X0,a1176)
| c7_2(X0,X1)
| c3_2(X0,X1)
| c9_1(X0)
| c5_1(X0)
| c10_2(X0,X1)
| c8_1(X0)
| c4_1(X0)
| c5_2(X0,a1176)
| c6_2(X0,X1) ) ).
cnf(u6238,negated_conjecture,
( ~ c6_2(X37,X38)
| c4_1(X37)
| c5_1(X37)
| c5_2(X37,X38)
| ~ c7_2(X37,X38) ) ).
cnf(u8892,negated_conjecture,
( c1_2(X0,a1097)
| ~ c10_1(X0)
| ~ c3_1(X0)
| ~ c4_1(X0)
| ~ sP64(X0) ) ).
cnf(u9037,negated_conjecture,
( ~ c1_2(X0,a1100)
| ~ c5_1(X0)
| ~ sP10(X0)
| ~ c10_1(X0)
| c3_2(X0,a1158)
| ~ c2_1(X0) ) ).
cnf(u6744,negated_conjecture,
( c1_2(X0,a989)
| ~ sP64(X0)
| ~ c10_1(X0) ) ).
cnf(u604,axiom,
( ~ c4_2(X0,a1182)
| ~ sP0(X0) ) ).
cnf(u10176,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP0(X0) ) ).
cnf(u6997,negated_conjecture,
( ~ c5_2(X0,a1152)
| c1_1(X0)
| ~ c5_2(X0,a1039)
| ~ sP14(X0) ) ).
cnf(u9801,negated_conjecture,
( c9_2(X0,a1159)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c1_2(X0,a1159)
| c7_2(X0,a1159)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0) ) ).
cnf(u6348,negated_conjecture,
( c8_2(X0,a983)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| c1_2(X0,a983) ) ).
cnf(u8124,negated_conjecture,
( c6_2(X0,a1112)
| c8_2(X0,a1049)
| c3_2(X0,a1112)
| ~ sP26(X0)
| c8_1(X0)
| c5_1(X0)
| c10_2(X0,a1112) ) ).
cnf(u6843,negated_conjecture,
( c8_2(X0,a1086)
| c7_2(X0,a1086)
| ~ c1_1(X0)
| ~ sP34(X0)
| ~ c2_1(X0) ) ).
cnf(u9542,negated_conjecture,
( ~ c1_2(X0,a1100)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| c9_2(X0,X1)
| c7_2(X0,X1)
| c9_2(X0,a1149)
| ~ c10_1(X0)
| c3_2(X0,X1)
| ~ c2_1(X0) ) ).
cnf(u10199,negated_conjecture,
( c9_2(X0,a1149)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| ~ sP3(X0) ) ).
cnf(u9904,negated_conjecture,
( ~ c1_2(X0,a1176)
| ~ c1_1(X0)
| c8_2(X0,X1)
| ~ c2_1(X0)
| c9_1(X0)
| ~ c5_1(X0)
| c3_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_2(X0,a1086)
| c3_2(X0,a1176)
| c7_2(X0,a1086)
| ~ sP34(X0) ) ).
cnf(u6749,negated_conjecture,
( c3_2(X0,a1012)
| ~ c10_1(X0)
| ~ sP54(X0)
| ~ c2_1(X0) ) ).
cnf(u586,axiom,
( c1_2(X0,a1178)
| ~ sP3(X0) ) ).
cnf(u8259,negated_conjecture,
( ~ c1_2(X0,a1084)
| ~ c2_1(X0)
| ~ sP64(X0)
| c5_1(X0)
| ~ c10_1(X0)
| c1_1(X0) ) ).
cnf(u592,axiom,
( c10_2(X0,a1180)
| ~ sP2(X0) ) ).
cnf(u6239,negated_conjecture,
( ~ c5_2(X0,a1100)
| c6_2(X0,a1039)
| c1_1(X0)
| c4_2(X0,a1100)
| ~ c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u7276,negated_conjecture,
( ~ c5_2(X0,a1179)
| sP2(X0)
| c9_1(X0)
| c2_2(X0,a1159)
| c5_1(X0)
| c9_2(X0,a1179) ) ).
cnf(u10097,negated_conjecture,
( ~ c10_2(X0,a1159)
| c1_2(X0,a1159)
| c7_2(X0,a1159)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c8_1(X0) ) ).
cnf(u7633,negated_conjecture,
( ~ c10_2(X0,a1138)
| ~ c10_1(X0)
| c3_1(X0)
| c1_2(X0,a1138) ) ).
cnf(u6756,negated_conjecture,
( ~ c5_2(a1074,X0)
| c4_2(a1074,X0)
| c1_2(a1074,X0) ) ).
cnf(u8461,negated_conjecture,
( c9_2(X0,a1101)
| c9_1(X0)
| c10_2(X0,a1159)
| c1_2(X0,a1101)
| ~ c10_1(X0)
| c8_1(X0)
| c1_1(X0) ) ).
cnf(u7280,negated_conjecture,
( ~ c5_2(X0,a1179)
| sP2(X0)
| c1_1(X0)
| ~ c5_2(X0,a1039)
| c5_1(X0)
| c4_2(X0,a1179) ) ).
cnf(u8705,negated_conjecture,
( ~ c7_2(X0,a1176)
| c7_2(X0,X1)
| c9_1(X0)
| ~ c1_1(X0)
| c8_2(X0,X1)
| ~ c2_1(X0)
| c4_1(X0)
| c5_2(X0,a1176)
| c3_2(X0,X1) ) ).
cnf(u8666,negated_conjecture,
( ~ c5_2(X0,a1182)
| c1_1(X0)
| c1_2(X0,a1039)
| ~ c10_1(X0)
| ~ sP0(X0) ) ).
cnf(u7023,negated_conjecture,
( ~ c2_2(X0,a1157)
| ~ c3_2(X0,a1157)
| ~ sP11(X0)
| ~ c5_1(X0)
| ~ c7_1(X0) ) ).
cnf(u10225,negated_conjecture,
( ~ c10_2(X0,a1149)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| c1_2(X0,a1149) ) ).
cnf(u6884,negated_conjecture,
( ~ c1_2(X0,a1112)
| c3_1(X0)
| c2_2(X0,a1112)
| c10_1(X0)
| ~ sP26(X0) ) ).
cnf(u227,axiom,
( ~ c8_2(X0,a989)
| ~ sP64(X0) ) ).
cnf(u8920,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c1_2(X0,a969)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| c9_2(X0,a969)
| c7_2(X0,a969)
| c9_2(X0,a1149)
| c10_1(X0)
| c9_1(X0)
| ~ c3_1(X0) ) ).
cnf(u9339,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ c5_1(X0)
| ~ c1_2(X0,a1152)
| c9_2(X0,a1152)
| c7_2(X0,a1152)
| c9_2(X0,a1149)
| c10_1(X0)
| ~ sP14(X0)
| c7_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0)
| ~ c2_1(X0) ) ).
cnf(u9349,negated_conjecture,
( ~ c1_2(X0,a1152)
| ~ c5_1(X0)
| c9_2(X0,a1152)
| c7_2(X0,a1152)
| c9_2(X0,a1149)
| c10_1(X0)
| ~ sP14(X0) ) ).
cnf(u9820,negated_conjecture,
( ~ c1_2(X0,a1159)
| ~ c5_1(X0)
| ~ c1_2(X0,a1152)
| c9_2(X0,a1159)
| c7_2(X0,a1159)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0)
| ~ sP14(X0) ) ).
cnf(u9422,negated_conjecture,
( c3_2(X0,a1077)
| c3_2(X0,X1)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c10_1(X0) ) ).
cnf(u8813,negated_conjecture,
( ~ c3_2(X0,a1159)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c9_2(X0,a1159)
| c7_2(X0,a1159)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0) ) ).
cnf(u6389,negated_conjecture,
( c9_2(X0,a1149)
| c2_1(X0)
| ~ c5_1(X0)
| c9_2(X0,a976)
| c7_2(X0,a976)
| c7_1(X0) ) ).
cnf(u7162,negated_conjecture,
( ~ c5_2(X0,a1182)
| c9_1(X0)
| c2_2(X0,a1159)
| ~ sP0(X0) ) ).
cnf(u8708,negated_conjecture,
( ~ c7_2(X0,a1178)
| ~ c10_1(X0)
| c3_2(X0,a1084)
| ~ sP3(X0)
| c4_1(X0)
| c5_1(X0)
| c5_2(X0,a1178)
| ~ c2_1(X0) ) ).
cnf(u6762,negated_conjecture,
( ~ c10_2(X0,a1049)
| c8_1(X0)
| ~ sP54(X0)
| c3_2(X0,a1012)
| c4_2(X0,a1012) ) ).
cnf(u9204,negated_conjecture,
( ~ c7_2(X0,a1039)
| c4_2(X0,a1012)
| c1_2(X0,a1012)
| ~ c10_1(X0)
| c4_1(X0)
| c5_1(X0)
| ~ sP54(X0)
| c5_2(X0,a1039)
| c1_1(X0) ) ).
cnf(u499,axiom,
( ~ sP20(X0)
| ndr1_1(X0) ) ).
cnf(u9094,negated_conjecture,
( c4_2(X0,a1122)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c10_1(X0)
| ~ c5_1(X0)
| c8_1(X0)
| c8_2(X0,a1049)
| c3_2(X0,a1122)
| c1_2(X0,a1122) ) ).
cnf(u6793,negated_conjecture,
( c5_2(X0,a1012)
| c4_1(X0)
| c5_1(X0)
| ~ sP54(X0) ) ).
cnf(u6548,negated_conjecture,
( ~ c2_2(X0,X1)
| c10_2(X0,X1)
| c1_2(X0,X1)
| ~ c10_1(X0)
| ~ c3_1(X0)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_1(X0)
| ~ c7_1(X0) ) ).
cnf(u392,axiom,
( ~ c6_2(X0,a1077)
| ~ sP38(X0) ) ).
cnf(u9703,negated_conjecture,
( ~ c1_2(X0,a1077)
| ~ c6_1(X0)
| ~ c1_2(X0,a988)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a1084)
| c3_2(X0,a988)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0) ) ).
cnf(u10028,negated_conjecture,
( ~ c8_2(X0,a1149)
| c7_2(X0,a988)
| ~ c5_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a988)
| ~ c2_1(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| c10_2(X0,a1077)
| ~ c6_1(X0)
| sP64(X0)
| c9_2(X0,a988)
| ~ c10_2(X0,a1149) ) ).
cnf(u7297,negated_conjecture,
( c3_2(X0,a1179)
| sP2(X0)
| ~ c10_1(X0)
| c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u542,axiom,
( c4_2(X0,a1157)
| ~ sP11(X0) ) ).
cnf(u8361,negated_conjecture,
c1_2(a1087,a1086) ).
cnf(u531,axiom,
( ~ sP14(X0)
| ndr1_1(X0) ) ).
cnf(u9499,negated_conjecture,
( ~ c1_2(X0,a1152)
| ~ c5_1(X0)
| ~ c1_2(X0,a969)
| c9_2(X0,a969)
| c7_2(X0,a969)
| c9_2(X0,a1149)
| c10_1(X0)
| c9_1(X0)
| ~ c3_1(X0)
| ~ sP14(X0) ) ).
cnf(u6937,negated_conjecture,
( c9_2(X0,a1149)
| ~ c5_1(X0)
| c9_2(X0,a1129)
| c7_2(X0,a1129)
| ~ sP20(X0) ) ).
cnf(u9627,negated_conjecture,
( ~ c8_2(X0,X1)
| c3_2(X0,a1084)
| ~ c6_1(X0)
| ~ c1_2(X0,a988)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c10_1(X0)
| ~ c1_2(X0,X1)
| c3_2(X0,a988) ) ).
cnf(u9510,negated_conjecture,
( ~ c1_2(X0,a1100)
| ~ c5_1(X0)
| ~ c1_2(X0,a969)
| c9_2(X0,a969)
| c7_2(X0,a969)
| c9_2(X0,a1149)
| c10_1(X0)
| c9_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u9887,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ c1_1(X0)
| c8_2(X0,X1)
| ~ c2_1(X0)
| ~ c1_2(X0,a1176)
| ~ c5_1(X0)
| c3_2(X0,X1)
| c7_2(X0,X1)
| c9_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a1176)
| ~ sP0(X0) ) ).
cnf(u8662,negated_conjecture,
( ~ c5_2(X0,a1100)
| c1_1(X0)
| c4_2(X0,a1100)
| c1_2(X0,a1039)
| ~ c10_1(X0)
| ~ c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u9671,negated_conjecture,
( ~ c1_2(X0,a1077)
| c10_1(X0)
| ~ c5_1(X0)
| c7_2(X0,a1084)
| c1_2(X0,a1084)
| ~ sP3(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c7_2(X0,a1077)
| ~ sP38(X0) ) ).
cnf(u7345,negated_conjecture,
( ~ c1_2(X0,a1086)
| ~ sP34(X0)
| ~ c2_1(X0)
| c5_1(X0)
| ~ c10_1(X0)
| c1_1(X0) ) ).
cnf(u588,axiom,
( ~ c4_2(X0,a1178)
| ~ sP3(X0) ) ).
cnf(u9949,negated_conjecture,
( ~ c1_2(X0,a1159)
| c1_2(X0,a1101)
| ~ c10_1(X0)
| c8_1(X0)
| c1_1(X0)
| ~ c5_1(X0)
| c9_2(X0,a1101)
| c9_1(X0)
| ~ c1_2(X0,a1100)
| c9_2(X0,a1159)
| c7_2(X0,a1159)
| c9_2(X0,a1149)
| ~ c2_1(X0) ) ).
cnf(u9792,negated_conjecture,
( c3_2(X0,a1077)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c1_2(X0,a1077)
| c7_2(X0,a1077)
| ~ sP38(X0)
| ~ c1_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0) ) ).
cnf(u6980,negated_conjecture,
( ~ c5_2(X0,a1152)
| c9_1(X0)
| c10_2(X0,a1159)
| ~ sP14(X0)
| c9_2(X0,a1152) ) ).
cnf(u9550,negated_conjecture,
( ~ c1_2(X0,a1152)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| c9_2(X0,X1)
| c7_2(X0,X1)
| c9_2(X0,a1149)
| ~ c10_1(X0)
| c3_2(X0,X1)
| ~ c2_1(X0)
| ~ sP14(X0) ) ).
cnf(u9262,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ sP11(X0)
| ~ c1_2(X0,a1157)
| ~ c5_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a1157)
| ~ c2_1(X0)
| ~ sP0(X0) ) ).
cnf(u8812,negated_conjecture,
( ~ c3_2(X0,a1178)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c9_2(X0,a1178)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP3(X0) ) ).
cnf(u9490,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c2_1(X0)
| c10_1(X0)
| ~ c5_1(X0)
| c7_2(X0,a1084)
| c1_2(X0,a1084)
| ~ sP3(X0)
| ~ c1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u593,axiom,
( ~ sP2(X0)
| ndr1_1(X0) ) ).
cnf(u10051,negated_conjecture,
( ~ c8_2(X0,X1)
| c9_2(X0,a1149)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| ~ c1_2(X0,X1) ) ).
cnf(u9552,negated_conjecture,
( ~ c1_2(X0,a1077)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| c9_2(X0,X1)
| c7_2(X0,X1)
| c9_2(X0,a1149)
| ~ c10_1(X0)
| c3_2(X0,X1)
| ~ c2_1(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0) ) ).
cnf(u607,axiom,
( ~ sP0(X0)
| ndr1_1(X0) ) ).
cnf(u7275,negated_conjecture,
( ~ c5_2(X0,a1179)
| sP2(X0)
| c9_1(X0)
| c10_2(X0,a1159)
| c5_1(X0)
| c9_2(X0,a1179) ) ).
cnf(u9148,negated_conjecture,
( ~ c10_2(X0,a1149)
| c7_2(X0,a1129)
| ~ sP20(X0)
| ~ c5_1(X0)
| ~ c10_1(X0)
| c9_2(X0,a1129)
| c1_2(X0,a1149) ) ).
cnf(u10078,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| c9_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| c7_2(X0,a1157)
| ~ sP11(X0) ) ).
cnf(u6216,negated_conjecture,
ndr1_1(a1062) ).
cnf(u8036,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| c3_2(X0,X1)
| c3_2(X0,a1157)
| c7_2(X0,a1157) ) ).
cnf(u8144,negated_conjecture,
( ~ c8_2(X0,a1149)
| c9_2(X0,a1129)
| c7_2(X0,a1129)
| ~ sP20(X0)
| ~ c5_1(X0)
| ~ c10_1(X0)
| ~ c10_2(X0,a1149) ) ).
cnf(u8922,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| c9_2(X0,a1178)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP3(X0) ) ).
cnf(u9039,negated_conjecture,
( ~ c1_2(X0,a1077)
| ~ c5_1(X0)
| ~ sP10(X0)
| ~ c10_1(X0)
| c3_2(X0,a1158)
| ~ c2_1(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0) ) ).
cnf(u9036,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ c5_1(X0)
| ~ sP10(X0)
| ~ c10_1(X0)
| c3_2(X0,a1158)
| ~ c2_1(X0)
| c7_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0) ) ).
cnf(u10090,negated_conjecture,
( ~ c8_2(X0,a1159)
| ~ c8_1(X0)
| c1_2(X0,a1159)
| c7_2(X0,a1159)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c10_2(X0,a1159) ) ).
cnf(u8006,negated_conjecture,
( ~ c7_2(X0,a1086)
| c5_1(X0)
| c10_2(X0,a1086)
| c8_1(X0)
| c4_1(X0)
| c5_2(X0,a1086)
| ~ sP34(X0) ) ).
cnf(u9414,negated_conjecture,
( ~ c10_2(X0,a1101)
| c1_2(X0,a1101)
| ~ c10_1(X0)
| c8_1(X0)
| c1_1(X0)
| c9_1(X0)
| c10_2(X0,a1159) ) ).
cnf(u10156,negated_conjecture,
( ~ c10_2(X0,a1149)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c9_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| c1_2(X0,a1149) ) ).
cnf(u5576,negated_conjecture,
( ~ c1_2(X0,a1138)
| c9_2(X0,a1097)
| ~ ndr1_1(X0)
| c6_2(X0,a1138)
| ~ c4_1(X0)
| c3_1(X0) ) ).
cnf(u10185,negated_conjecture,
( ~ c1_2(X0,a1100)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| c9_2(X0,a1149) ) ).
cnf(u6883,negated_conjecture,
c1_2(a980,a1086) ).
cnf(u8168,negated_conjecture,
( ~ c5_2(X0,a983)
| ~ c3_1(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| c1_2(X0,a983)
| c6_2(X0,a1039)
| c1_1(X0) ) ).
cnf(u6240,negated_conjecture,
( ~ c5_2(X0,a1100)
| ~ c5_2(X0,a1039)
| c1_1(X0)
| c4_2(X0,a1100)
| ~ c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u7911,negated_conjecture,
ndr1_1(a1079) ).
cnf(u8190,negated_conjecture,
( ~ c8_2(X0,a1149)
| ~ c5_1(X0)
| c9_2(X0,a976)
| c7_2(X0,a976)
| c7_1(X0)
| c2_1(X0)
| ~ c10_1(X0)
| ~ c10_2(X0,a1149) ) ).
cnf(u6500,negated_conjecture,
( ~ c5_2(X0,a976)
| c10_2(X0,a1159)
| c9_1(X0)
| c9_2(X0,a976)
| c7_1(X0)
| c2_1(X0) ) ).
cnf(u10145,negated_conjecture,
( ~ c1_2(X0,a1149)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c9_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| ~ sP3(X0)
| c6_2(X0,a1149)
| c7_2(X0,a1077) ) ).
cnf(u9761,negated_conjecture,
( ~ c1_2(X0,a1100)
| ~ c10_1(X0)
| ~ sP26(X0)
| ~ c5_1(X0)
| c1_1(X0)
| c4_2(X0,a1112)
| c1_2(X0,a1112)
| c3_2(X0,a1039)
| ~ c2_1(X0) ) ).
cnf(u7024,negated_conjecture,
( ~ c2_2(X0,a1157)
| ~ c1_2(X0,a1157)
| ~ c5_1(X0)
| ~ sP11(X0)
| ~ c8_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u8536,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ sP10(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| ~ c10_1(X0)
| c3_2(X0,a1158)
| ~ c2_1(X0) ) ).
cnf(u8819,negated_conjecture,
( ~ c3_2(X0,a969)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c9_2(X0,a969)
| c7_2(X0,a969)
| c9_2(X0,a1149)
| c10_1(X0)
| c9_1(X0) ) ).
cnf(u9079,negated_conjecture,
( c1_2(X0,a1110)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c10_1(X0)
| ~ c5_1(X0) ) ).
cnf(u10256,negated_conjecture,
( ~ c10_2(X0,a1149)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c1_2(X0,a1159)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c7_2(X0,a1159)
| ~ sP38(X0)
| c1_2(X0,a1149) ) ).
cnf(u7157,negated_conjecture,
( c2_2(X0,a1182)
| c10_1(X0)
| ~ sP0(X0)
| ~ c5_1(X0) ) ).
cnf(u6529,negated_conjecture,
( ~ c2_2(X0,a1176)
| ~ c3_2(X0,a1176)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c4_2(X0,X1)
| c9_1(X0)
| c7_2(X0,X1)
| c3_2(X0,X1) ) ).
cnf(u226,axiom,
( c9_2(X0,a989)
| ~ sP64(X0) ) ).
cnf(u9373,negated_conjecture,
( ~ c1_2(X0,a1100)
| ~ c5_1(X0)
| c9_2(X0,a1100)
| c7_2(X0,a1100)
| c9_2(X0,a1149)
| c10_1(X0)
| ~ c2_1(X0) ) ).
cnf(u8814,negated_conjecture,
( ~ c3_2(X0,a1152)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c9_2(X0,a1152)
| c7_2(X0,a1152)
| c9_2(X0,a1149)
| c10_1(X0)
| ~ sP14(X0) ) ).
cnf(u9207,negated_conjecture,
( ~ c1_2(X0,a969)
| ~ c5_1(X0)
| c9_2(X0,a1178)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP3(X0)
| c9_1(X0)
| ~ c3_1(X0) ) ).
cnf(u5278,negated_conjecture,
( c6_2(X0,a1101)
| c5_1(X0)
| c10_2(X0,a1101)
| c8_1(X0)
| c1_1(X0) ) ).
cnf(u7845,negated_conjecture,
~ c3_1(a1078) ).
cnf(u7048,negated_conjecture,
( c1_2(X0,a1158)
| ~ sP10(X0)
| ~ c10_1(X0) ) ).
cnf(u9853,negated_conjecture,
( ~ c1_2(X0,a1182)
| c9_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a1084)
| ~ c5_1(X0)
| c10_2(X0,a1159)
| ~ c10_1(X0)
| ~ sP26(X0)
| c3_2(X0,a1112)
| ~ sP0(X0) ) ).
cnf(u6906,negated_conjecture,
( ~ c10_2(X0,a1049)
| c8_1(X0)
| ~ sP26(X0)
| c3_2(X0,a1112)
| c4_2(X0,a1112) ) ).
cnf(u7036,negated_conjecture,
( c8_2(X0,a1157)
| c7_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0)
| ~ c2_1(X0) ) ).
cnf(u9521,negated_conjecture,
( ~ c8_2(X0,X2)
| c9_1(X0)
| ~ c1_1(X0)
| c8_2(X0,X1)
| ~ c2_1(X0)
| ~ c1_2(X0,a1176)
| ~ c5_1(X0)
| c3_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_2(X0,X2)
| ~ c10_1(X0)
| c3_2(X0,a1176) ) ).
cnf(u547,axiom,
( ~ sP10(X0)
| ndr1_1(X0) ) ).
cnf(u8835,negated_conjecture,
( ~ c7_2(X0,a988)
| ~ c10_1(X0)
| c3_2(X0,a1084)
| ~ c6_1(X0)
| c4_1(X0)
| c5_1(X0)
| c5_2(X0,a988)
| ~ c2_1(X0) ) ).
cnf(u9621,negated_conjecture,
( ~ c10_2(X0,a1012)
| c1_2(X0,a1012)
| ~ c10_1(X0)
| c4_1(X0)
| c5_1(X0)
| ~ sP54(X0)
| c9_1(X0)
| c10_2(X0,a1159) ) ).
cnf(u7178,negated_conjecture,
( ~ c5_2(X0,a1182)
| c1_1(X0)
| c6_2(X0,a1039)
| ~ sP0(X0) ) ).
cnf(u393,axiom,
( ~ sP38(X0)
| ndr1_1(X0) ) ).
cnf(u7164,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ c8_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| c3_2(X0,X1)
| c3_2(X0,a1182)
| ~ sP0(X0) ) ).
cnf(u8232,negated_conjecture,
( c3_2(X0,a1084)
| ~ c10_1(X0)
| ~ c2_1(X0)
| ~ sP20(X0) ) ).
cnf(u9726,negated_conjecture,
( ~ c1_2(X0,a969)
| c3_2(X0,a1084)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c10_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a988)
| c9_1(X0)
| ~ c3_1(X0) ) ).
cnf(u8593,negated_conjecture,
( ~ c5_2(X0,X1)
| c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c9_1(X0)
| c10_2(X0,a1159)
| ~ c5_1(X0)
| c9_2(X0,X1) ) ).
cnf(u292,axiom,
( ~ sP54(X0)
| ndr1_1(X0) ) ).
cnf(u9752,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ c10_1(X0)
| ~ sP26(X0)
| ~ c5_1(X0)
| c1_1(X0)
| c4_2(X0,a1112)
| c1_2(X0,a1112)
| c3_2(X0,a1039)
| ~ c2_1(X0)
| ~ sP0(X0) ) ).
cnf(u7073,negated_conjecture,
( ~ c2_2(X0,a1158)
| ~ c1_2(X0,a1158)
| ~ c5_1(X0)
| ~ sP10(X0)
| ~ c8_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u10110,negated_conjecture,
( ~ c5_2(X0,a1152)
| c1_2(X0,a1159)
| c7_2(X0,a1159)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c9_2(X0,a1152)
| ~ sP14(X0) ) ).
cnf(u10050,negated_conjecture,
( ~ c3_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| ~ c7_1(X0) ) ).
cnf(u5672,negated_conjecture,
( ~ c5_2(X0,a1039)
| c1_1(X0)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,X1)
| ~ c10_1(X0) ) ).
cnf(u5756,negated_conjecture,
( ~ c1_2(X0,a1101)
| c2_2(X0,a1101)
| c10_1(X0)
| c3_1(X0)
| c8_1(X0) ) ).
cnf(u9173,negated_conjecture,
( ~ c2_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0)
| c9_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a1084)
| ~ c3_2(X0,a1112)
| c10_2(X0,a1159)
| ~ c5_1(X0)
| ~ c7_1(X0) ) ).
cnf(u8737,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c10_1(X0)
| c3_2(X0,a1084)
| ~ sP3(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u8916,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c1_2(X0,a1159)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| c9_2(X0,a1159)
| c7_2(X0,a1159)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0) ) ).
cnf(u8622,negated_conjecture,
( c1_2(X0,a1012)
| c3_1(X0)
| ~ c9_1(X0)
| ~ c10_1(X0)
| ~ sP54(X0) ) ).
cnf(u7204,negated_conjecture,
( ~ c1_2(X0,a1113)
| c5_1(X0)
| ~ c7_1(X0)
| c1_1(X0) ) ).
cnf(u9253,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ sP11(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,a969)
| ~ c10_1(X0)
| c3_2(X0,a1157)
| ~ c2_1(X0)
| c9_1(X0)
| ~ c3_1(X0) ) ).
cnf(u4640,negated_conjecture,
( ~ c8_2(X153,X154)
| c10_1(X153)
| c2_2(X153,X154)
| ~ c5_1(X153) ) ).
cnf(u9514,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ c5_1(X0)
| ~ c1_2(X0,a969)
| c9_2(X0,a969)
| c7_2(X0,a969)
| c9_2(X0,a1149)
| c10_1(X0)
| c9_1(X0)
| c7_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0)
| ~ c2_1(X0) ) ).
cnf(u10129,negated_conjecture,
( ~ c5_2(X0,a969)
| c1_2(X0,a1159)
| c7_2(X0,a1159)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c9_2(X0,a969) ) ).
cnf(u8261,negated_conjecture,
( ~ c7_2(X0,a1128)
| ~ c2_1(X0)
| ~ sP64(X0)
| sP20(X0)
| ~ c10_1(X0)
| ~ c1_2(X0,a1084)
| ~ c7_2(X0,a1084) ) ).
cnf(u8749,negated_conjecture,
( ~ c7_2(X0,a1084)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ sP38(X0)
| sP20(X0)
| ~ c10_2(X0,a1128)
| ~ c1_2(X0,a1084)
| ~ c10_1(X0) ) ).
cnf(u8516,negated_conjecture,
( c2_2(X0,a1159)
| c9_1(X0)
| c9_2(X0,a1012)
| c1_2(X0,a1012)
| ~ c10_1(X0)
| c4_1(X0)
| c5_1(X0)
| ~ sP54(X0) ) ).
cnf(u6511,negated_conjecture,
( ~ c5_2(X0,a1100)
| c2_2(X0,a1159)
| c9_1(X0)
| c9_2(X0,a1100)
| ~ c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u9921,negated_conjecture,
( c6_2(X0,a1178)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| ~ c5_1(X0) ) ).
cnf(u10245,negated_conjecture,
( ~ c8_2(X0,a1149)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c1_2(X0,a1159)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c7_2(X0,a1159)
| ~ c10_2(X0,a1149) ) ).
cnf(u9259,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ sP11(X0)
| ~ c5_1(X0)
| ~ c1_2(X0,a1152)
| ~ c10_1(X0)
| c3_2(X0,a1157)
| ~ c2_1(X0)
| ~ sP14(X0) ) ).
cnf(u591,axiom,
( ~ c5_2(X0,a1180)
| ~ sP2(X0) ) ).
cnf(u10187,negated_conjecture,
( ~ c1_2(X0,a1077)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| c9_2(X0,a1149) ) ).
cnf(u9402,negated_conjecture,
( ~ c1_2(X0,a1100)
| ~ c5_1(X0)
| ~ c1_2(X0,a976)
| c9_2(X0,a976)
| c7_2(X0,a976)
| c9_2(X0,a1149)
| c10_1(X0)
| c7_1(X0) ) ).
cnf(u9548,negated_conjecture,
( ~ c1_2(X0,a1182)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| c9_2(X0,X1)
| c7_2(X0,X1)
| c9_2(X0,a1149)
| ~ c10_1(X0)
| c3_2(X0,X1)
| ~ c2_1(X0)
| ~ sP0(X0) ) ).
cnf(u9657,negated_conjecture,
( ~ c1_2(X0,a1152)
| c10_1(X0)
| ~ c5_1(X0)
| c7_2(X0,a1084)
| c1_2(X0,a1084)
| ~ sP3(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ sP14(X0) ) ).
cnf(u8818,negated_conjecture,
( ~ c3_2(X0,a1100)
| ~ c5_1(X0)
| c9_2(X0,a1100)
| c7_2(X0,a1100)
| c9_2(X0,a1149)
| c10_1(X0)
| ~ c2_1(X0) ) ).
cnf(u9515,negated_conjecture,
( ~ c1_2(X0,a1077)
| ~ c5_1(X0)
| ~ c1_2(X0,a969)
| c9_2(X0,a969)
| c7_2(X0,a969)
| c9_2(X0,a1149)
| c10_1(X0)
| c9_1(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0) ) ).
cnf(u9043,negated_conjecture,
( ~ c1_2(X0,a1086)
| ~ c5_1(X0)
| ~ sP10(X0)
| c3_2(X0,a1158)
| ~ c2_1(X0)
| c7_2(X0,a1086)
| ~ c1_1(X0)
| ~ sP34(X0) ) ).
cnf(u10080,negated_conjecture,
( ~ c1_2(X0,a969)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c9_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| c9_1(X0) ) ).
cnf(u10249,negated_conjecture,
( ~ c1_2(X0,a1149)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c1_2(X0,a1159)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| c7_2(X0,a1159)
| c6_2(X0,a1149) ) ).
cnf(u10060,negated_conjecture,
( ~ c1_2(X0,a1152)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c9_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| c9_2(X0,a1149)
| ~ sP14(X0) ) ).
cnf(u7981,negated_conjecture,
( ~ c1_2(X0,a1077)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| c3_2(X0,X1)
| c3_2(X0,a1077)
| c7_2(X0,a1077) ) ).
cnf(u6761,negated_conjecture,
( c4_2(X0,a1012)
| c8_1(X0)
| c8_2(X0,a1049)
| c3_2(X0,a1012)
| ~ sP54(X0) ) ).
cnf(u6516,negated_conjecture,
( ~ c5_2(X0,X1)
| c2_2(X0,a1159)
| c9_1(X0)
| c9_2(X0,X1)
| c1_2(X0,X1)
| ~ c10_1(X0) ) ).
cnf(u4819,negated_conjecture,
ndr1_1(a1058) ).
cnf(u10088,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c8_1(X0)
| c1_2(X0,a1159)
| c7_2(X0,a1159)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c5_2(X0,X1)
| c9_2(X0,X1) ) ).
cnf(u8931,negated_conjecture,
( ~ c2_2(X0,a1039)
| c4_2(X0,a1112)
| c1_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0)
| ~ c3_2(X0,a1039)
| c1_1(X0)
| ~ c5_1(X0)
| ~ c7_1(X0) ) ).
cnf(u9555,negated_conjecture,
( ~ c1_2(X0,a969)
| ~ c5_1(X0)
| ~ c1_2(X0,X1)
| c9_2(X0,X1)
| c7_2(X0,X1)
| c9_2(X0,a1149)
| ~ c10_1(X0)
| c3_2(X0,X1)
| ~ c2_1(X0)
| c9_1(X0) ) ).
cnf(u8167,negated_conjecture,
( ~ c5_2(X0,a1039)
| ~ c3_1(X0)
| ~ c5_1(X0)
| ~ c2_1(X0)
| c1_2(X0,a983)
| c1_1(X0)
| ~ c5_2(X0,a983) ) ).
cnf(u8145,negated_conjecture,
( ~ c1_2(X0,a1149)
| c9_2(X0,a1129)
| c7_2(X0,a1129)
| ~ sP20(X0)
| ~ c4_1(X0)
| c9_2(X0,a1097)
| c6_2(X0,a1149)
| ~ c5_1(X0) ) ).
cnf(u8667,negated_conjecture,
( ~ c5_2(X0,a1152)
| c1_1(X0)
| c1_2(X0,a1039)
| ~ c10_1(X0)
| ~ sP14(X0) ) ).
cnf(u10216,negated_conjecture,
( ~ c8_2(X0,a1149)
| ~ c1_1(X0)
| ~ sP38(X0)
| ~ c2_1(X0)
| c10_2(X0,a1077)
| ~ c10_1(X0)
| c10_2(X0,a1097)
| c1_2(X0,a1097)
| ~ c5_1(X0)
| c7_2(X0,a1178)
| ~ sP3(X0)
| c7_2(X0,a1077)
| ~ c10_2(X0,a1149) ) ).
cnf(u6412,negated_conjecture,
( c2_2(X0,a976)
| c10_1(X0)
| c7_1(X0)
| ~ c5_1(X0) ) ).
cnf(u9683,negated_conjecture,
( ~ c1_2(X0,a988)
| ~ c6_1(X0)
| c3_2(X0,a1084)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c10_1(X0)
| ~ c1_2(X0,a969)
| c3_2(X0,a988)
| c9_1(X0)
| ~ c3_1(X0) ) ).
cnf(u9837,negated_conjecture,
( ~ c1_2(X0,a1159)
| ~ c5_1(X0)
| ~ c1_2(X0,a1086)
| c9_2(X0,a1159)
| c7_2(X0,a1159)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| c7_2(X0,a1086)
| ~ c1_1(X0)
| ~ sP34(X0)
| ~ c2_1(X0) ) ).
cnf(u7994,negated_conjecture,
( ~ c1_2(X0,a1086)
| ~ c1_1(X0)
| ~ sP34(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| c3_2(X0,X1)
| c3_2(X0,a1086)
| c7_2(X0,a1086) ) ).
cnf(u8932,negated_conjecture,
( ~ c2_2(X0,a1039)
| c4_2(X0,a1112)
| c1_2(X0,a1112)
| ~ c10_1(X0)
| ~ sP26(X0)
| ~ c1_2(X0,a1039)
| ~ c5_1(X0)
| c1_1(X0)
| ~ c8_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u7413,negated_conjecture,
( ~ c7_2(X0,a1113)
| ~ c10_2(X0,a1128)
| ~ ndr1_1(X0)
| ~ c1_2(X0,a1113)
| sP20(X0)
| ~ c7_1(X0) ) ).
cnf(u8191,negated_conjecture,
( ~ c1_2(X0,a1149)
| ~ c5_1(X0)
| c9_2(X0,a976)
| c7_2(X0,a976)
| c7_1(X0)
| ~ c4_1(X0)
| c9_2(X0,a1097)
| c6_2(X0,a1149)
| c2_1(X0) ) ).
cnf(u7422,negated_conjecture,
( ~ c1_2(X0,a1012)
| ~ c10_2(X0,a1128)
| sP20(X0)
| ~ c10_1(X0)
| ~ sP54(X0)
| ~ c2_1(X0) ) ).
cnf(u10122,negated_conjecture,
( ~ c5_2(X0,a1100)
| c1_2(X0,a1159)
| c7_2(X0,a1159)
| ~ sP38(X0)
| ~ c1_1(X0)
| c7_2(X0,a1077)
| c10_2(X0,a1077)
| ~ c5_1(X0)
| ~ c7_1(X0)
| c3_2(X0,a1077)
| c9_2(X0,a1149)
| c9_1(X0)
| c1_2(X0,a1112)
| ~ sP26(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c9_2(X0,a1100) ) ).
cnf(u9372,negated_conjecture,
( ~ c1_2(X0,a1157)
| ~ c5_1(X0)
| ~ c1_2(X0,a1100)
| c9_2(X0,a1100)
| c7_2(X0,a1100)
| c9_2(X0,a1149)
| c10_1(X0)
| ~ c2_1(X0)
| c7_2(X0,a1157)
| ~ c1_1(X0)
| ~ sP11(X0) ) ).
cnf(u6460,negated_conjecture,
( ~ c1_2(X0,X1)
| c6_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a1084) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN424+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n007.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 15:53:55 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.25/1.48 % (2522980)Detected formulas, will run a generic FOF schedule.
% 5.25/1.48 % (2522986)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=113772666:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.25/1.48 % (2522985)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=1703077886:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.25/1.48 % (2522987)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2902157967:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.25/1.48 % (2522990)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1478768390:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.25/1.48 % (2522991)dis-21_1_sil=8000:lcm=predicate:random_seed=2282523573:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 5.25/1.48 % (2522989)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4059644333:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.25/1.48 % (2522988)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1319555599:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.25/1.48 % (2522990)Refutation not found, incomplete strategy
% 5.25/1.48 % (2522990)------------------------------
% 5.25/1.48 % (2522990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.25/1.48 % (2522990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.48 % (2522990)CaDiCaL version: 2.1.3
% 5.25/1.48 % (2522990)Termination reason: Refutation not found, incomplete strategy
% 5.25/1.48 % (2522990)Time elapsed: 0.032 s
% 5.25/1.48 % (2522990)Peak memory usage: 91 MB
% 5.25/1.48 % (2522990)Instructions burned: 52 (million)
% 5.25/1.48 % (2522988)Instruction limit reached!
% 5.25/1.48 % (2522988)------------------------------
% 5.25/1.48 % (2522988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.25/1.48 % (2522988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.48 % (2522988)CaDiCaL version: 2.1.3
% 5.25/1.48 % (2522988)Termination reason: Instruction limit
% 5.25/1.48 % (2522988)Termination phase: Saturation
% 5.25/1.48 % (2522988)Time elapsed: 0.063 s
% 5.25/1.48 % (2522988)Peak memory usage: 91 MB
% 5.25/1.48 % (2522988)Instructions burned: 111 (million)
% 5.25/1.48 % (2522989)Instruction limit reached!
% 5.25/1.48 % (2522989)------------------------------
% 5.25/1.48 % (2522989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.25/1.48 % (2522989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.48 % (2522989)CaDiCaL version: 2.1.3
% 5.25/1.48 % (2522989)Termination reason: Instruction limit
% 5.25/1.48 % (2522989)Termination phase: Saturation
% 5.25/1.48 % (2522989)Time elapsed: 0.066 s
% 5.25/1.48 % (2522989)Peak memory usage: 89 MB
% 5.25/1.48 % (2522989)Instructions burned: 120 (million)
% 5.25/1.48 % (2522991)Instruction limit reached!
% 5.25/1.48 % (2522991)------------------------------
% 5.25/1.48 % (2522991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.25/1.48 % (2522991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.48 % (2522991)CaDiCaL version: 2.1.3
% 5.25/1.48 % (2522991)Termination reason: Instruction limit
% 5.25/1.48 % (2522991)Termination phase: Saturation
% 5.25/1.48 % (2522991)Time elapsed: 0.072 s
% 5.25/1.48 % (2522991)Peak memory usage: 92 MB
% 5.25/1.48 % (2522991)Instructions burned: 129 (million)
% 5.25/1.48 % (2523000)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1817469006:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.25/1.48 % (2522999)lrs+10_1_sil=8000:sp=occurrence:random_seed=261909014:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.25/1.48 % (2523001)lrs+1011_1_sil=32000:sp=occurrence:random_seed=109124052:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.25/1.48 % (2523000)Refutation not found, incomplete strategy
% 5.25/1.48 % (2523000)------------------------------
% 5.25/1.48 % (2523000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.25/1.48 % (2523000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.48 % (2523000)CaDiCaL version: 2.1.3
% 5.25/1.48 % (2523000)Termination reason: Refutation not found, incomplete strategy
% 5.25/1.48 % (2523000)Time elapsed: 0.036 s
% 5.25/1.48 % (2523000)Peak memory usage: 91 MB
% 5.25/1.48 % (2523000)Instructions burned: 58 (million)
% 5.25/1.48 % (2522990)------------------------------
% 5.25/1.48 % (2522990)------------------------------
% 5.25/1.48 % (2523001)Refutation not found, incomplete strategy
% 5.25/1.48 % (2523001)------------------------------
% 5.25/1.48 % (2523001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.25/1.48 % (2523001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.48 % (2523001)CaDiCaL version: 2.1.3
% 5.25/1.48 % (2523001)Termination reason: Refutation not found, incomplete strategy
% 5.25/1.48 % (2523001)Time elapsed: 0.052 s
% 5.25/1.48 % (2523001)Peak memory usage: 92 MB
% 5.25/1.48 % (2523001)Instructions burned: 88 (million)
% 5.25/1.48 % (2522999)First to succeed.
% 5.25/1.48 % (2522999)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2522980"
% 5.25/1.48 % (2523005)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1462228916:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 5.25/1.48 % (2523005)Refutation not found, incomplete strategy
% 5.25/1.48 % (2523005)------------------------------
% 5.25/1.48 % (2523005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.25/1.48 % (2523005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.25/1.48 % (2523005)CaDiCaL version: 2.1.3
% 5.25/1.48 % (2523005)Termination reason: Refutation not found, incomplete strategy
% 5.25/1.48 % (2523005)Time elapsed: 0.030 s
% 5.25/1.48 % (2523005)Peak memory usage: 91 MB
% 5.25/1.48 % (2523005)Instructions burned: 48 (million)
% 5.25/1.48 % (2523000)------------------------------
% 5.25/1.48 % (2523000)------------------------------
% 5.25/1.48 % (2523001)------------------------------
% 5.25/1.48 % (2523001)------------------------------
% 5.25/1.48 % (2522986)Also succeeded, but the first one will report.
% 5.25/1.48 % SZS status CounterSatisfiable for theBenchmark
% 5.25/1.48 % SZS output start Saturation.
% See solution above
% 6.25/1.67 % SZS output start Definitions and Model Updates.
% 6.25/1.67 % SZS output end Definitions and Model Updates.
% 6.25/1.67 % (2522999)------------------------------
% 6.25/1.67 % (2522999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/1.67 % (2522999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.67 % (2522999)CaDiCaL version: 2.1.3
% 6.25/1.67 % (2522999)Termination reason: Satisfiable
% 6.25/1.67 % (2522999)Time elapsed: 0.146 s
% 6.25/1.67 % (2522999)Peak memory usage: 94 MB
% 6.25/1.67 % (2522999)Instructions burned: 255 (million)
% 6.25/1.67 % (2522999)------------------------------
% 6.25/1.67 % (2522999)------------------------------
% 6.25/1.67 % (2522980)Success in time 0.805 s
% 6.25/1.67 % Vampire exiting
%------------------------------------------------------------------------------