%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN422+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:50:34 PM UTC 2026
% Result : CounterSatisfiable 5.28s 1.47s
% Output : Saturation 6.35s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u790,negated_conjecture,
~ c8_1(a759) ).
cnf(u794,negated_conjecture,
c7_0 ).
cnf(u803,negated_conjecture,
~ c5_2(a759,a760) ).
cnf(u808,negated_conjecture,
c2_2(a759,a760) ).
cnf(u813,negated_conjecture,
~ c1_2(a759,a760) ).
cnf(u818,negated_conjecture,
ndr1_1(a759) ).
cnf(u822,negated_conjecture,
( ~ c6_2(a759,X125)
| c8_2(a759,X125)
| c7_2(a759,X125) ) ).
cnf(u827,negated_conjecture,
ndr1_0 ).
cnf(u832,negated_conjecture,
sP0 ).
cnf(u851,negated_conjecture,
ndr1_1(a756) ).
cnf(u860,negated_conjecture,
c6_1(a756) ).
cnf(u865,negated_conjecture,
ndr1_1(a755) ).
cnf(u873,negated_conjecture,
~ c10_0 ).
cnf(u876,negated_conjecture,
( ~ c10_2(X121,X122)
| ~ c5_1(X121)
| c10_1(X121)
| ~ ndr1_1(X121)
| c3_2(X121,X122)
| c1_2(X121,X122) ) ).
cnf(u881,negated_conjecture,
~ c6_1(a755) ).
cnf(u886,negated_conjecture,
~ c7_1(a755) ).
cnf(u890,negated_conjecture,
~ sP1 ).
cnf(u894,negated_conjecture,
~ sP2 ).
cnf(u898,negated_conjecture,
( ~ c8_2(X119,X120)
| c2_2(X119,a751)
| ~ ndr1_1(X119)
| c7_1(X119)
| c9_2(X119,X120)
| ~ c6_2(X119,X120) ) ).
cnf(u902,negated_conjecture,
( ~ c8_2(X119,X120)
| c3_2(X119,a751)
| ~ ndr1_1(X119)
| c7_1(X119)
| c9_2(X119,X120)
| ~ c6_2(X119,X120) ) ).
cnf(u907,negated_conjecture,
c6_0 ).
cnf(u910,negated_conjecture,
~ c2_0 ).
cnf(u914,negated_conjecture,
~ c4_0 ).
cnf(u919,negated_conjecture,
( ~ c2_1(X118)
| c9_1(X118) ) ).
cnf(u923,negated_conjecture,
~ sP4 ).
cnf(u927,negated_conjecture,
( c10_2(X116,a748)
| c10_2(X116,X117)
| ~ ndr1_1(X116)
| c5_2(X116,X117)
| c3_2(X116,X117)
| c8_1(X116) ) ).
cnf(u935,negated_conjecture,
( ~ c4_2(X116,a748)
| ~ ndr1_1(X116)
| c10_2(X116,X117)
| c5_2(X116,X117)
| c3_2(X116,X117)
| c8_1(X116) ) ).
cnf(u939,negated_conjecture,
( ~ c1_2(X114,X115)
| ~ c2_1(X114)
| ~ ndr1_1(X114)
| c5_2(X114,X115)
| c3_2(X114,X115)
| c9_2(X114,a747) ) ).
cnf(u943,negated_conjecture,
( ~ c1_2(X114,a747)
| ~ c2_1(X114)
| ~ ndr1_1(X114)
| c5_2(X114,X115)
| c3_2(X114,X115)
| ~ c1_2(X114,X115) ) ).
cnf(u947,negated_conjecture,
( ~ c1_2(X114,X115)
| ~ c2_1(X114)
| ~ ndr1_1(X114)
| c5_2(X114,X115)
| c3_2(X114,X115)
| c5_2(X114,a747) ) ).
cnf(u952,negated_conjecture,
c8_0 ).
cnf(u985,negated_conjecture,
( ~ c10_2(X111,a743)
| sP5(X111)
| c6_2(X111,X112)
| ~ ndr1_1(X111)
| ~ c3_2(X111,X112)
| ~ c1_2(X111,X112) ) ).
cnf(u988,negated_conjecture,
~ sP6 ).
cnf(u993,negated_conjecture,
( ~ c1_2(X111,X112)
| sP5(X111)
| ~ c9_2(X111,a743)
| ~ ndr1_1(X111)
| ~ c3_2(X111,X112)
| c6_2(X111,X112) ) ).
cnf(u1001,negated_conjecture,
c9_0 ).
cnf(u1005,negated_conjecture,
~ sP7 ).
cnf(u1010,negated_conjecture,
~ c7_1(a739) ).
cnf(u1015,negated_conjecture,
~ c5_1(a739) ).
cnf(u1020,negated_conjecture,
~ c2_1(a739) ).
cnf(u1026,negated_conjecture,
~ c4_1(a737) ).
cnf(u1029,negated_conjecture,
~ sP8 ).
cnf(u1035,negated_conjecture,
c9_1(a737) ).
cnf(u1040,negated_conjecture,
c1_2(a737,a738) ).
cnf(u1045,negated_conjecture,
~ c4_2(a737,a738) ).
cnf(u1050,negated_conjecture,
c9_2(a737,a738) ).
cnf(u1055,negated_conjecture,
ndr1_1(a737) ).
cnf(u1060,negated_conjecture,
~ sP10 ).
cnf(u1076,negated_conjecture,
~ sP11 ).
cnf(u1081,negated_conjecture,
c1_1(a728) ).
cnf(u1086,negated_conjecture,
c6_1(a728) ).
cnf(u1091,negated_conjecture,
( ~ c8_2(X105,X106)
| ~ c10_1(X105)
| ~ c4_1(X105)
| ~ ndr1_1(X105)
| c3_2(X105,X106)
| ~ c4_2(X105,X106) ) ).
cnf(u1094,negated_conjecture,
~ sP12 ).
cnf(u1134,negated_conjecture,
~ sP13 ).
cnf(u1150,negated_conjecture,
~ sP15 ).
cnf(u1154,negated_conjecture,
~ sP16 ).
cnf(u1158,negated_conjecture,
( ~ c7_2(X96,a718)
| sP14(X96)
| ~ c10_1(X96) ) ).
cnf(u1162,negated_conjecture,
( ~ c8_2(X96,a718)
| sP14(X96)
| ~ c10_1(X96) ) ).
cnf(u1166,negated_conjecture,
( ~ c10_1(X96)
| sP14(X96)
| ndr1_1(X96) ) ).
cnf(u1182,negated_conjecture,
( ~ c5_2(X92,X93)
| ~ c6_1(X92)
| ~ ndr1_1(X92)
| ~ c1_1(X92)
| c7_2(X92,X93) ) ).
cnf(u1194,negated_conjecture,
sP19 ).
cnf(u1197,negated_conjecture,
( ~ c9_2(X89,a712)
| sP18(X89) ) ).
cnf(u1201,negated_conjecture,
( c8_2(X89,a712)
| sP18(X89) ) ).
cnf(u1205,negated_conjecture,
( ~ c4_2(X89,a712)
| sP18(X89) ) ).
cnf(u1218,negated_conjecture,
~ c5_0 ).
cnf(u1237,negated_conjecture,
( ~ c7_2(X82,X84)
| ~ c8_1(X82)
| ~ c5_2(X82,X84)
| ~ c2_2(X82,X83)
| c4_2(X82,X84)
| ~ ndr1_1(X82)
| ~ c9_2(X82,X83)
| c1_2(X82,X83) ) ).
cnf(u1272,negated_conjecture,
~ c5_1(a708) ).
cnf(u1275,negated_conjecture,
~ sP20 ).
cnf(u1280,negated_conjecture,
ndr1_1(a708) ).
cnf(u1284,negated_conjecture,
( ~ c5_2(a708,X81)
| c7_2(a708,X81)
| c10_2(a708,X81) ) ).
cnf(u1289,negated_conjecture,
~ sP21 ).
cnf(u1294,negated_conjecture,
~ c3_1(a705) ).
cnf(u1298,negated_conjecture,
ndr1_1(a705) ).
cnf(u1307,negated_conjecture,
~ c9_1(a705) ).
cnf(u1312,negated_conjecture,
( ~ c8_2(X77,X78)
| c10_2(X77,X79)
| ~ c1_2(X77,X79)
| c4_2(X77,X79)
| c1_1(X77)
| ~ ndr1_1(X77)
| c6_2(X77,X78)
| c4_2(X77,X78) ) ).
cnf(u1315,negated_conjecture,
~ sP22 ).
cnf(u1334,negated_conjecture,
~ sP23 ).
cnf(u1339,negated_conjecture,
~ c10_1(a700) ).
cnf(u1344,negated_conjecture,
~ c9_1(a700) ).
cnf(u1349,negated_conjecture,
~ c7_1(a700) ).
cnf(u1355,negated_conjecture,
c9_1(a698) ).
cnf(u1360,negated_conjecture,
c2_1(a698) ).
cnf(u1364,negated_conjecture,
~ c1_2(a698,a699) ).
cnf(u1370,negated_conjecture,
~ c5_2(a698,a699) ).
cnf(u1375,negated_conjecture,
ndr1_1(a698) ).
cnf(u1380,negated_conjecture,
~ sP24 ).
cnf(u1389,negated_conjecture,
c3_0 ).
cnf(u1406,negated_conjecture,
~ sP25 ).
cnf(u1422,negated_conjecture,
ndr1_1(a690) ).
cnf(u1426,negated_conjecture,
( c7_2(a690,X75)
| c4_2(a690,X75)
| c2_2(a690,X75) ) ).
cnf(u1434,negated_conjecture,
c2_1(a690) ).
cnf(u1439,negated_conjecture,
~ c10_2(a690,a691) ).
cnf(u1444,negated_conjecture,
~ c9_2(a690,a691) ).
cnf(u1449,negated_conjecture,
~ c5_2(a690,a691) ).
cnf(u1473,negated_conjecture,
( ~ c10_2(X71,X72)
| ~ c3_1(X71)
| ~ c8_1(X71)
| ~ ndr1_1(X71)
| ~ c9_2(X71,X72)
| c6_2(X71,X72) ) ).
cnf(u1477,negated_conjecture,
( ~ c10_1(X69)
| ~ ndr1_1(X69)
| ~ c3_2(X69,X70)
| c5_2(X69,X70)
| ~ c8_2(X69,X70)
| ~ c8_1(X69) ) ).
cnf(u1483,negated_conjecture,
sP26 ).
cnf(u1487,negated_conjecture,
( c7_2(X68,a684)
| ~ c8_1(X68)
| sP27(X68) ) ).
cnf(u1491,negated_conjecture,
( c1_2(X68,a684)
| ~ c8_1(X68)
| sP27(X68) ) ).
cnf(u1495,negated_conjecture,
( c6_2(X68,a684)
| ~ c8_1(X68)
| sP27(X68) ) ).
cnf(u1526,negated_conjecture,
~ sP29 ).
cnf(u1548,negated_conjecture,
( ~ c6_1(X62)
| c3_1(X62)
| ~ c2_1(X62) ) ).
cnf(u1552,negated_conjecture,
( c8_2(X61,a675)
| sP30(X61)
| sP31(X61) ) ).
cnf(u1556,negated_conjecture,
( ~ c1_2(X61,a675)
| sP30(X61)
| sP31(X61) ) ).
cnf(u1560,negated_conjecture,
( c5_2(X61,a675)
| sP30(X61)
| sP31(X61) ) ).
cnf(u1564,negated_conjecture,
( ndr1_1(X61)
| sP30(X61)
| sP31(X61) ) ).
cnf(u1611,negated_conjecture,
~ sP32 ).
cnf(u1616,negated_conjecture,
c8_1(a670) ).
cnf(u1621,negated_conjecture,
c9_1(a670) ).
cnf(u1626,negated_conjecture,
~ c3_1(a670) ).
cnf(u1632,negated_conjecture,
~ sP33 ).
cnf(u1637,negated_conjecture,
~ c9_1(a668) ).
cnf(u1641,negated_conjecture,
ndr1_1(a668) ).
cnf(u1645,negated_conjecture,
( ~ c8_2(a668,X57)
| ~ c3_2(a668,X57)
| c2_2(a668,X57) ) ).
cnf(u1649,negated_conjecture,
( ~ c4_2(a668,X56)
| c1_2(a668,X56) ) ).
cnf(u1666,negated_conjecture,
~ sP34 ).
cnf(u1670,negated_conjecture,
ndr1_1(a665) ).
cnf(u1679,negated_conjecture,
~ c2_1(a665) ).
cnf(u1688,negated_conjecture,
( ~ c10_2(X49,X50)
| ~ c6_1(X49)
| ~ ndr1_1(X49)
| ~ c1_2(X49,X50)
| c2_1(X49)
| ~ c9_2(X49,X50) ) ).
cnf(u1693,negated_conjecture,
~ sP35 ).
cnf(u1697,negated_conjecture,
( ~ c7_2(X47,X48)
| ~ c9_1(X47)
| ~ ndr1_1(X47)
| ~ c8_2(X47,X48)
| ~ c10_1(X47)
| c1_2(X47,X48) ) ).
cnf(u1718,negated_conjecture,
~ sP37 ).
cnf(u1723,negated_conjecture,
~ c6_1(a660) ).
cnf(u1728,negated_conjecture,
~ c10_1(a660) ).
cnf(u1733,negated_conjecture,
c5_1(a660) ).
cnf(u1742,negated_conjecture,
( c8_2(X42,X43)
| ~ ndr1_1(X42)
| c4_2(X42,X43)
| c6_2(X42,X43)
| ~ c1_1(X42)
| c5_1(X42) ) ).
cnf(u1761,negated_conjecture,
ndr1_1(a658) ).
cnf(u1765,negated_conjecture,
( ~ c3_2(a658,X40)
| ~ c4_2(a658,X40)
| ~ c5_2(a658,X40) ) ).
cnf(u1770,negated_conjecture,
c7_1(a658) ).
cnf(u1776,negated_conjecture,
~ sP38 ).
cnf(u1780,negated_conjecture,
ndr1_1(a655) ).
cnf(u1784,negated_conjecture,
( c6_2(a655,X39)
| c3_2(a655,X39)
| c9_2(a655,X39) ) ).
cnf(u1788,negated_conjecture,
( ~ c10_2(a655,X38)
| c3_2(a655,X38)
| ~ c2_2(a655,X38) ) ).
cnf(u1793,negated_conjecture,
c2_1(a655) ).
cnf(u1813,negated_conjecture,
~ sP39 ).
cnf(u1818,negated_conjecture,
~ c7_1(a651) ).
cnf(u1823,negated_conjecture,
~ c9_1(a651) ).
cnf(u1828,negated_conjecture,
~ c5_1(a651) ).
cnf(u1832,negated_conjecture,
~ sP40 ).
cnf(u1852,negated_conjecture,
( ~ c10_2(X31,X32)
| ~ ndr1_1(X31)
| c2_2(X31,X32)
| c5_2(X31,X32)
| ~ c9_1(X31)
| c2_1(X31) ) ).
cnf(u1874,negated_conjecture,
sP41 ).
cnf(u1877,negated_conjecture,
~ sP42 ).
cnf(u1886,negated_conjecture,
( ~ c10_2(X27,X29)
| ~ c9_2(X27,X29)
| ~ c3_2(X27,X29)
| c10_1(X27)
| ~ ndr1_1(X27)
| ~ c8_2(X27,X28)
| ~ c6_2(X27,X28)
| ~ c3_2(X27,X28) ) ).
cnf(u1961,negated_conjecture,
( ~ c8_2(X15,X16)
| ~ c8_1(X15)
| ~ c6_1(X15)
| ~ ndr1_1(X15)
| c1_2(X15,X16)
| c4_2(X15,X16) ) ).
cnf(u1968,negated_conjecture,
~ sP44 ).
cnf(u1993,negated_conjecture,
( ~ c6_2(X13,X14)
| c3_1(X13)
| ~ ndr1_1(X13)
| c10_1(X13)
| c5_2(X13,X14)
| ~ c3_2(X13,X14) ) ).
cnf(u2014,negated_conjecture,
~ sP45 ).
cnf(u2018,negated_conjecture,
( ~ c2_2(X12,a627)
| ~ c7_1(X12)
| ~ c8_1(X12) ) ).
cnf(u2022,negated_conjecture,
( ~ c5_2(X12,a627)
| ~ c7_1(X12)
| ~ c8_1(X12) ) ).
cnf(u2026,negated_conjecture,
( ~ c10_2(X12,a627)
| ~ c7_1(X12)
| ~ c8_1(X12) ) ).
cnf(u2030,negated_conjecture,
( ~ c7_1(X12)
| ~ c8_1(X12)
| ndr1_1(X12) ) ).
cnf(u2034,negated_conjecture,
~ sP46 ).
cnf(u2050,negated_conjecture,
~ sP47 ).
cnf(u2054,negated_conjecture,
ndr1_1(a621) ).
cnf(u2058,negated_conjecture,
( ~ c2_2(a621,X10)
| c6_2(a621,X10)
| c1_2(a621,X10) ) ).
cnf(u2063,negated_conjecture,
c1_1(a621) ).
cnf(u2068,negated_conjecture,
~ c3_1(a621) ).
cnf(u2103,negated_conjecture,
~ sP48 ).
cnf(u2108,negated_conjecture,
~ c10_1(a617) ).
cnf(u2113,negated_conjecture,
c9_1(a617) ).
cnf(u2118,negated_conjecture,
c5_1(a617) ).
cnf(u2123,negated_conjecture,
~ sP49 ).
cnf(u2131,negated_conjecture,
~ sP50 ).
cnf(u2144,negated_conjecture,
~ sP51 ).
cnf(u2149,negated_conjecture,
~ c8_1(a609) ).
cnf(u2154,negated_conjecture,
~ c10_1(a609) ).
cnf(u2159,negated_conjecture,
~ c5_1(a609) ).
cnf(u2181,axiom,
c4_1(a758) ).
cnf(u2186,axiom,
c8_1(a758) ).
cnf(u2191,axiom,
c1_1(a758) ).
cnf(u2337,axiom,
ndr1_1(a733) ).
cnf(u2350,axiom,
~ c4_1(a733) ).
cnf(u2446,axiom,
( ~ c7_2(X0,X1)
| ~ c8_1(X0)
| ~ c5_2(X0,a714)
| ~ ndr1_1(X0)
| c8_2(X0,X1)
| c6_2(X0,X1) ) ).
cnf(u2450,axiom,
( ~ c7_2(X0,X1)
| ~ c8_1(X0)
| c7_2(X0,a714)
| ~ ndr1_1(X0)
| c8_2(X0,X1)
| c6_2(X0,X1) ) ).
cnf(u2454,axiom,
( ~ c7_2(X0,X1)
| ~ c8_1(X0)
| c3_2(X0,a714)
| ~ ndr1_1(X0)
| c8_2(X0,X1)
| c6_2(X0,X1) ) ).
cnf(u2596,axiom,
c2_2(a686,a688) ).
cnf(u2601,axiom,
c4_2(a686,a688) ).
cnf(u2606,axiom,
ndr1_1(a686) ).
cnf(u2611,axiom,
c8_1(a686) ).
cnf(u2616,axiom,
~ c8_2(a686,a687) ).
cnf(u2621,axiom,
c4_2(a686,a687) ).
cnf(u2626,axiom,
~ c1_2(a686,a687) ).
cnf(u2685,axiom,
ndr1_1(a669) ).
cnf(u2694,axiom,
~ c2_1(a669) ).
cnf(u2822,axiom,
c5_2(a645,a647) ).
cnf(u2827,axiom,
~ c3_2(a645,a647) ).
cnf(u2832,axiom,
~ c9_2(a645,a647) ).
cnf(u2837,axiom,
ndr1_1(a645) ).
cnf(u2842,axiom,
~ c5_2(a645,a646) ).
cnf(u2847,axiom,
~ c3_2(a645,a646) ).
cnf(u2852,axiom,
~ c9_2(a645,a646) ).
cnf(u2857,axiom,
( ~ c9_2(a645,X0)
| ~ c2_2(a645,X0)
| ~ c5_2(a645,X0) ) ).
cnf(u3161,negated_conjecture,
~ c2_1(a756) ).
cnf(u3180,negated_conjecture,
~ c10_1(a759) ).
cnf(u3187,negated_conjecture,
~ c5_1(a759) ).
cnf(u3192,negated_conjecture,
~ c1_1(a759) ).
cnf(u3261,negated_conjecture,
~ c2_1(a728) ).
cnf(u3297,negated_conjecture,
~ c3_2(a737,a738) ).
cnf(u3306,negated_conjecture,
~ c2_1(a737) ).
cnf(u3313,negated_conjecture,
~ c8_1(a690) ).
cnf(u3339,negated_conjecture,
sP31(a708) ).
cnf(u3342,negated_conjecture,
~ sP30(a708) ).
cnf(u3359,negated_conjecture,
~ c10_1(a690) ).
cnf(u3383,negated_conjecture,
~ sP31(a668) ).
cnf(u3396,negated_conjecture,
~ c3_2(a668,a675) ).
cnf(u3410,negated_conjecture,
~ c3_2(a668,a712) ).
cnf(u3414,negated_conjecture,
~ c5_1(a668) ).
cnf(u3419,negated_conjecture,
~ c1_1(a668) ).
cnf(u3446,negated_conjecture,
c3_2(a655,a712) ).
cnf(u3466,negated_conjecture,
~ c8_1(a655) ).
cnf(u3474,negated_conjecture,
( ~ c2_2(a655,X0)
| c5_2(a655,X0)
| c3_2(a655,X0) ) ).
cnf(u3487,negated_conjecture,
~ c2_2(a655,a748) ).
cnf(u3519,negated_conjecture,
~ c6_1(a668) ).
cnf(u3573,negated_conjecture,
~ c10_1(a756) ).
cnf(u3598,negated_conjecture,
~ c9_1(a728) ).
cnf(u3625,negated_conjecture,
c9_2(a655,a675) ).
cnf(u3628,negated_conjecture,
~ sP31(a655) ).
cnf(u3679,negated_conjecture,
~ c6_1(a658) ).
cnf(u3723,negated_conjecture,
c1_1(a737) ).
cnf(u3739,negated_conjecture,
~ c1_1(a645) ).
cnf(u3743,negated_conjecture,
~ c6_1(a645) ).
cnf(u3772,negated_conjecture,
~ c2_1(a708) ).
cnf(u3865,negated_conjecture,
~ c1_1(a698) ).
cnf(u3905,negated_conjecture,
~ c3_2(a668,a636) ).
cnf(u3926,negated_conjecture,
~ c2_2(a655,a636) ).
cnf(u3934,negated_conjecture,
~ sP43(a655) ).
cnf(u3971,negated_conjecture,
~ sP36(a655) ).
cnf(u4013,negated_conjecture,
~ sP30(a621) ).
cnf(u4047,negated_conjecture,
~ sP28(a708) ).
cnf(u4063,negated_conjecture,
~ sP28(a759) ).
cnf(u4075,negated_conjecture,
~ c5_2(a658,a685) ).
cnf(u4124,negated_conjecture,
~ c5_2(a658,a716) ).
cnf(u4149,negated_conjecture,
~ sP14(a655) ).
cnf(u4162,negated_conjecture,
~ sP14(a621) ).
cnf(u4180,negated_conjecture,
~ sP9(a668) ).
cnf(u4196,negated_conjecture,
~ c3_2(a668,a744) ).
cnf(u4226,negated_conjecture,
~ c9_1(a621) ).
cnf(u4268,negated_conjecture,
~ sP3(a655) ).
cnf(u4281,negated_conjecture,
~ sP3(a621) ).
cnf(u4299,axiom,
~ c2_2(a645,a744) ).
cnf(u4304,axiom,
~ sP18(a645) ).
cnf(u4325,negated_conjecture,
~ c2_1(a645) ).
cnf(u4617,negated_conjecture,
~ c5_1(a690) ).
cnf(u4671,negated_conjecture,
~ c6_1(a737) ).
cnf(u5271,negated_conjecture,
c2_2(a737,a748) ).
cnf(u5284,negated_conjecture,
~ c9_1(a645) ).
cnf(u6508,negated_conjecture,
~ sP17(a759) ).
cnf(u7044,negated_conjecture,
~ c6_1(a655) ).
cnf(u3989,negated_conjecture,
( ~ c4_2(X0,a676)
| ~ c10_1(X0)
| ~ c4_1(X0)
| c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u9351,negated_conjecture,
( c4_2(X0,a744)
| ~ c6_1(X0)
| ~ sP5(X0)
| ~ c8_1(X0)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c4_2(X0,a676)
| sP18(X0)
| c1_1(X0)
| c7_1(X0)
| c2_2(X0,a751) ) ).
cnf(u248,axiom,
( c10_2(X0,a662)
| ~ sP36(X0) ) ).
cnf(u4489,negated_conjecture,
( ~ c9_2(X0,X1)
| c2_1(X0)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c8_1(X0)
| ~ c2_2(X0,X1)
| c4_2(X0,a662)
| ~ c9_1(X0)
| c1_2(X0,X1) ) ).
cnf(u7407,negated_conjecture,
( ~ c6_2(X0,a676)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c9_2(X0,a747)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u8862,negated_conjecture,
( ~ c9_2(X0,a748)
| c5_2(X0,a743)
| c3_2(X0,a743)
| c8_1(X0)
| sP5(X0)
| c6_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| c3_2(X0,a748)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c6_1(X0)
| c2_1(X0)
| ~ c5_1(X0) ) ).
cnf(u5646,negated_conjecture,
( ~ c9_2(X0,X1)
| c8_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c6_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0) ) ).
cnf(u4399,negated_conjecture,
( c8_2(X0,a677)
| c3_2(X0,a714)
| ~ c8_1(X0)
| c6_2(X0,a677)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP30(X0) ) ).
cnf(u8223,negated_conjecture,
( ~ c3_2(X0,a636)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| c10_1(X0)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c2_2(X0,a751)
| c7_1(X0)
| c1_1(X0)
| ~ c8_1(X0) ) ).
cnf(u3993,negated_conjecture,
( ~ c3_2(X0,a676)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c8_1(X0) ) ).
cnf(u7176,negated_conjecture,
( ~ c9_2(X0,a662)
| c1_1(X0)
| c4_2(X0,a744)
| sP18(X0)
| ~ sP5(X0)
| c10_1(X0)
| ~ c6_1(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| ~ c3_2(X0,a662)
| ~ sP36(X0)
| ~ c8_1(X0)
| ~ c3_2(X0,a712) ) ).
cnf(u4497,negated_conjecture,
( ~ c6_2(X0,a712)
| c10_1(X0)
| ~ sP27(X0)
| ~ c9_2(X0,a685)
| ~ c3_2(X0,a712)
| sP18(X0) ) ).
cnf(u4398,negated_conjecture,
( c8_2(X0,a747)
| c3_2(X0,a714)
| ~ c8_1(X0)
| c6_2(X0,a747)
| c5_2(X0,a712)
| ~ c6_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u4484,negated_conjecture,
( ~ c8_2(X0,a662)
| c2_1(X0)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c9_1(X0)
| ~ c10_1(X0)
| c1_2(X0,a662) ) ).
cnf(u4838,negated_conjecture,
( c7_2(X0,a747)
| ~ c2_1(X0)
| ~ c8_1(X0)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0) ) ).
cnf(u6178,negated_conjecture,
( ~ c9_2(X0,a636)
| c4_2(X0,a684)
| sP18(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c3_2(X0,a636)
| c10_1(X0)
| ~ sP43(X0)
| c1_1(X0)
| ~ c3_2(X0,a712) ) ).
cnf(u8745,negated_conjecture,
( ~ c9_2(X0,a636)
| sP18(X0)
| c4_2(X0,a744)
| ~ c6_1(X0)
| ~ sP5(X0)
| ~ c8_1(X0)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c5_2(X0,a636)
| ~ c3_2(X0,a636)
| c1_1(X0)
| ~ c3_2(X0,a712) ) ).
cnf(u3220,negated_conjecture,
( ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c8_1(X0)
| ~ c6_1(X0)
| c10_2(X0,a748)
| c2_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u4503,negated_conjecture,
( ~ c6_2(X0,a676)
| ~ c3_2(X0,a636)
| c10_1(X0)
| ~ sP43(X0)
| ~ c9_2(X0,a636)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u5795,negated_conjecture,
( c3_2(X0,a751)
| c1_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_1(X0)
| c4_2(X0,a744)
| c7_1(X0) ) ).
cnf(u3990,negated_conjecture,
( c1_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676) ) ).
cnf(u3224,negated_conjecture,
( c10_2(X0,X1)
| ~ ndr1_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c8_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u4775,negated_conjecture,
( ~ c2_2(X0,a747)
| c3_2(X0,a662)
| ~ sP36(X0)
| ~ c2_1(X0)
| c5_2(X0,a662)
| ~ c5_1(X0)
| ~ c5_2(X0,a684)
| c10_1(X0)
| c4_2(X0,a684)
| ~ c8_1(X0)
| c1_2(X0,a747)
| sP27(X0) ) ).
cnf(u5538,negated_conjecture,
( c3_2(X0,a713)
| c4_2(X0,a713)
| ~ c6_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a713)
| ~ c8_1(X0)
| c5_2(X0,a747)
| ~ sP18(X0) ) ).
cnf(u4746,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP28(X0)
| ~ c8_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c1_2(X0,a747)
| c5_2(X0,a684)
| c3_2(X0,a684)
| ~ c2_1(X0)
| sP27(X0) ) ).
cnf(u7102,negated_conjecture,
( ~ c6_2(X0,a675)
| c4_2(X0,a744)
| ~ c8_1(X0)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c3_2(X0,a744)
| c10_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u3996,negated_conjecture,
( ~ c6_2(X0,a676)
| c3_2(X0,a751)
| c7_1(X0)
| ~ sP31(X0) ) ).
cnf(u6555,negated_conjecture,
( ~ c6_2(X0,a712)
| c1_1(X0)
| c6_2(X0,a636)
| ~ sP17(X0)
| ~ c9_2(X0,a716)
| c10_1(X0)
| ~ sP43(X0)
| c4_2(X0,a716)
| ~ c3_2(X0,a712)
| sP18(X0) ) ).
cnf(u5032,negated_conjecture,
( ~ c9_2(X0,X1)
| c5_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| ~ c2_2(X0,X1)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,X1) ) ).
cnf(u3994,negated_conjecture,
( ~ c1_2(X0,X1)
| c10_2(X0,X1)
| ~ sP31(X0)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676) ) ).
cnf(u6059,negated_conjecture,
( ~ c9_2(X0,a685)
| ~ sP43(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| c2_2(X0,a712)
| c5_2(X0,a712)
| ~ c9_1(X0)
| c2_1(X0)
| c10_1(X0)
| ~ sP27(X0)
| c1_1(X0)
| ~ c3_2(X0,a636) ) ).
cnf(u9267,negated_conjecture,
( c6_2(X0,a712)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c4_2(X0,a676)
| sP18(X0)
| c1_1(X0) ) ).
cnf(u7725,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| c5_2(X0,a636)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747) ) ).
cnf(u6184,negated_conjecture,
( ~ c3_2(X0,a712)
| c4_2(X0,a684)
| sP18(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c3_1(X0)
| c5_2(X0,a712)
| c1_1(X0) ) ).
cnf(u3639,negated_conjecture,
( ~ c9_2(X0,X1)
| ~ c5_2(X0,a684)
| ~ c2_2(X0,X1)
| c4_2(X0,a684)
| ~ c8_1(X0)
| c1_2(X0,X1)
| sP27(X0) ) ).
cnf(u5579,negated_conjecture,
( c1_2(X0,a748)
| c3_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a744)
| c3_2(X0,a744)
| c8_1(X0)
| ~ c6_1(X0)
| c2_1(X0)
| c10_1(X0)
| ~ sP5(X0) ) ).
cnf(u5945,negated_conjecture,
( ~ c6_2(X0,a712)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c3_2(X0,a712)
| sP18(X0) ) ).
cnf(u6079,negated_conjecture,
( ~ c9_2(X0,a662)
| c4_2(X0,a676)
| ~ c8_1(X0)
| c1_1(X0)
| ~ c6_1(X0)
| sP18(X0)
| c2_2(X0,a676)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c3_2(X0,a662)
| c10_1(X0)
| ~ sP36(X0)
| ~ sP31(X0)
| ~ c3_2(X0,a712) ) ).
cnf(u6330,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c6_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a662)
| c3_2(X0,a662)
| ~ c8_1(X0)
| ~ sP36(X0)
| ~ sP30(X0)
| c4_2(X0,a662)
| c4_2(X0,a677)
| c1_2(X0,a747) ) ).
cnf(u7712,negated_conjecture,
( ~ c2_2(X0,a744)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| c5_2(X0,a636)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u5167,negated_conjecture,
( ~ c9_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ sP17(X0)
| ~ c6_1(X0)
| c2_1(X0)
| c4_2(X0,a716) ) ).
cnf(u5718,negated_conjecture,
( ~ c9_2(X0,a743)
| c6_2(X0,a677)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP30(X0)
| ~ c9_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a714)
| sP5(X0)
| ~ c8_1(X0)
| ~ c3_2(X0,a677) ) ).
cnf(u5030,negated_conjecture,
( c8_2(X0,a747)
| c5_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| c6_2(X0,a747) ) ).
cnf(u3918,negated_conjecture,
( c1_2(X0,a636)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u4702,negated_conjecture,
( ~ c6_2(X0,a636)
| c10_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| ~ c3_2(X0,a636)
| c10_2(X0,X1)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c8_1(X0)
| ~ sP43(X0) ) ).
cnf(u3754,negated_conjecture,
( c6_2(X0,a712)
| c1_1(X0)
| sP18(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c2_2(X0,a712)
| c5_2(X0,a712)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u3649,negated_conjecture,
( c10_2(X0,X1)
| c10_1(X0)
| c3_2(X0,a748)
| c1_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c8_1(X0) ) ).
cnf(u8388,negated_conjecture,
( c2_2(X0,a751)
| ~ c6_1(X0)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| ~ sP5(X0)
| c7_1(X0)
| c1_1(X0)
| ~ c8_1(X0)
| c5_2(X0,a636)
| ~ c10_1(X0)
| ~ c4_1(X0) ) ).
cnf(u4696,negated_conjecture,
( c3_2(X0,a713)
| c5_2(X0,a713)
| c8_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0)
| ~ sP18(X0) ) ).
cnf(u4426,negated_conjecture,
( ~ c3_2(X0,a750)
| ~ sP3(X0)
| ~ c1_1(X0)
| c5_1(X0)
| c3_1(X0)
| c10_1(X0)
| c5_2(X0,a750)
| c4_2(X0,a750) ) ).
cnf(u7643,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c8_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c6_1(X0)
| c4_2(X0,a747)
| c5_2(X0,a712)
| c1_2(X0,a747)
| ~ sP43(X0)
| c5_2(X0,a636) ) ).
cnf(u5561,negated_conjecture,
( ~ c9_2(X0,a748)
| c8_1(X0)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a748)
| c5_2(X0,X1)
| c5_2(X0,X2)
| c3_2(X0,X2)
| ~ c6_1(X0)
| c10_2(X0,X2)
| c3_2(X0,X1) ) ).
cnf(u7678,negated_conjecture,
( ~ c9_2(X0,a748)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a748)
| c5_2(X0,X1)
| c8_1(X0)
| ~ sP43(X0)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c6_1(X0)
| c3_2(X0,X1) ) ).
cnf(u6992,negated_conjecture,
( c9_2(X0,a675)
| c4_2(X0,a684)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c3_2(X0,a751)
| c7_1(X0)
| c1_1(X0) ) ).
cnf(u5805,negated_conjecture,
( ~ c3_2(X0,a676)
| c1_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c3_1(X0)
| c4_2(X0,a744) ) ).
cnf(u5484,negated_conjecture,
( c7_2(X0,a714)
| c5_2(X0,a744)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c2_1(X0)
| c8_2(X0,a747)
| c6_2(X0,a747) ) ).
cnf(u4203,negated_conjecture,
( c1_2(X0,a744)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744) ) ).
cnf(u5068,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP30(X0)
| ~ c8_1(X0)
| ~ c1_1(X0)
| c4_2(X0,a677)
| ~ c6_1(X0)
| c1_2(X0,a747)
| c10_1(X0)
| c3_2(X0,a636)
| ~ sP43(X0)
| ~ c2_1(X0)
| c5_2(X0,a636)
| ~ c5_1(X0) ) ).
cnf(u3915,negated_conjecture,
( c1_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP43(X0) ) ).
cnf(u3534,negated_conjecture,
( ~ c6_1(X0)
| ~ c1_1(X0)
| sP30(X0)
| sP31(X0)
| ~ c9_1(X0)
| ~ c10_1(X0) ) ).
cnf(u344,axiom,
( c2_2(X0,a716)
| ~ sP17(X0) ) ).
cnf(u7522,negated_conjecture,
( ~ c6_2(X0,a636)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ c8_1(X0)
| sP27(X0)
| ~ c9_2(X0,a684)
| ~ c3_2(X0,a684)
| c10_1(X0)
| ~ sP31(X0)
| c4_2(X0,a684)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u4980,negated_conjecture,
( ~ c9_2(X0,a662)
| c4_2(X0,a744)
| ~ c8_1(X0)
| c1_1(X0)
| ~ c6_1(X0)
| sP18(X0)
| c2_1(X0)
| ~ c3_2(X0,a662)
| c10_1(X0)
| ~ sP36(X0)
| ~ sP5(X0)
| ~ c3_2(X0,a712) ) ).
cnf(u7685,negated_conjecture,
( ~ c6_2(X0,a712)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ c8_1(X0)
| sP27(X0)
| ~ c9_2(X0,a684)
| ~ c3_2(X0,a684)
| c10_1(X0)
| c4_2(X0,a684)
| c1_1(X0)
| ~ c3_2(X0,a712)
| sP18(X0) ) ).
cnf(u7646,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c8_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c6_1(X0)
| c4_2(X0,a747)
| c5_2(X0,a712)
| c1_2(X0,a747) ) ).
cnf(u6342,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c6_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a713)
| c3_2(X0,a713)
| ~ c8_1(X0)
| ~ sP18(X0)
| ~ sP28(X0)
| c4_2(X0,a713)
| c1_2(X0,a747) ) ).
cnf(u6746,negated_conjecture,
( c2_2(X0,a751)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_1(X0)
| ~ sP43(X0)
| c7_1(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| c1_1(X0)
| c5_2(X0,a744) ) ).
cnf(u8033,negated_conjecture,
( ~ c2_2(X0,a713)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c5_2(X0,a744)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a713)
| ~ sP18(X0) ) ).
cnf(u3829,negated_conjecture,
( c1_2(X0,X1)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u6838,negated_conjecture,
( ~ c3_2(X0,a676)
| c1_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c3_1(X0)
| c4_2(X0,a684) ) ).
cnf(u8157,negated_conjecture,
( ~ c3_2(X0,a636)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| c10_1(X0)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c3_2(X0,a751)
| c7_1(X0)
| c1_1(X0)
| ~ c8_1(X0) ) ).
cnf(u3810,negated_conjecture,
( ~ c9_2(X0,a684)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c8_1(X0)
| sP27(X0)
| ~ c6_1(X0)
| c2_1(X0)
| c4_2(X0,a684) ) ).
cnf(u4049,negated_conjecture,
( c7_2(X0,a683)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP28(X0) ) ).
cnf(u7632,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c8_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c6_1(X0)
| c4_2(X0,a747)
| c5_2(X0,a712)
| c1_2(X0,a747)
| c4_2(X0,a662)
| c5_1(X0)
| c5_2(X0,a662)
| c3_2(X0,a662)
| ~ sP36(X0) ) ).
cnf(u4723,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP43(X0)
| ~ c2_1(X0)
| c5_2(X0,a636)
| c3_2(X0,a636)
| ~ c8_1(X0)
| ~ c5_2(X0,a684)
| ~ c6_1(X0)
| c4_2(X0,a684)
| c1_2(X0,a747)
| sP27(X0) ) ).
cnf(u3830,negated_conjecture,
( ~ c8_2(X0,X2)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c1_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c3_2(X0,X2) ) ).
cnf(u4955,negated_conjecture,
( c1_2(X0,a662)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c8_1(X0)
| c3_2(X0,a714)
| ~ c9_1(X0)
| c2_1(X0)
| c4_2(X0,a662) ) ).
cnf(u5344,negated_conjecture,
( c10_2(X0,a748)
| c8_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a713)
| c2_1(X0)
| c5_2(X0,a713)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP18(X0) ) ).
cnf(u4569,negated_conjecture,
( ~ c8_2(X0,X2)
| c5_2(X0,X1)
| c8_1(X0)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c10_1(X0)
| c3_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c3_2(X0,X2) ) ).
cnf(u7177,negated_conjecture,
( ~ c9_2(X0,a636)
| c1_1(X0)
| c4_2(X0,a744)
| sP18(X0)
| ~ sP5(X0)
| c10_1(X0)
| ~ c6_1(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| ~ c3_2(X0,a636)
| ~ sP43(X0)
| ~ c8_1(X0)
| ~ c3_2(X0,a712) ) ).
cnf(u7274,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747)
| c4_2(X0,a713)
| c5_1(X0)
| c5_2(X0,a713)
| c3_2(X0,a713)
| ~ sP18(X0) ) ).
cnf(u7132,negated_conjecture,
( ~ c6_2(X0,a675)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| ~ c3_2(X0,a744)
| c10_1(X0)
| ~ sP43(X0)
| c4_2(X0,a744)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u5083,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ c2_1(X0)
| c5_2(X0,a744)
| c3_2(X0,a744)
| ~ c8_1(X0)
| ~ c5_2(X0,a684)
| ~ c6_1(X0)
| c4_2(X0,a684)
| c1_2(X0,a747)
| sP27(X0) ) ).
cnf(u5486,negated_conjecture,
( ~ c8_2(X0,a747)
| c5_2(X0,a744)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c2_1(X0)
| c1_2(X0,a747) ) ).
cnf(u5754,negated_conjecture,
( c4_2(X0,a676)
| c1_1(X0)
| ~ sP31(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| c2_2(X0,a676)
| ~ c9_1(X0)
| c2_1(X0)
| c2_2(X0,a751)
| c7_1(X0) ) ).
cnf(u3333,negated_conjecture,
( c4_2(X0,a675)
| sP31(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| sP30(X0) ) ).
cnf(u4096,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c9_2(X0,a685)
| c10_1(X0)
| ~ sP27(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u5391,negated_conjecture,
( ~ c9_2(X0,a748)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c6_1(X0)
| c1_2(X0,X1)
| c2_1(X0)
| c3_2(X0,X1)
| c1_2(X0,X2)
| c5_2(X0,X2)
| c3_2(X0,a748)
| c3_2(X0,X2) ) ).
cnf(u273,axiom,
( c5_2(X0,a677)
| ~ sP30(X0) ) ).
cnf(u4867,negated_conjecture,
( ~ c9_2(X0,X1)
| ~ c8_1(X0)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c2_2(X0,X1)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,X1) ) ).
cnf(u4742,negated_conjecture,
( ~ c2_2(X0,a744)
| ~ sP28(X0)
| ~ c8_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c1_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u6813,negated_conjecture,
( ~ c1_2(X0,X1)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| c6_2(X0,a747)
| c5_2(X0,a636)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c8_1(X0) ) ).
cnf(u5663,negated_conjecture,
( ~ c9_2(X0,a685)
| sP18(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c2_2(X0,a712)
| c5_2(X0,a712)
| ~ c9_1(X0)
| c2_1(X0)
| ~ sP27(X0)
| c1_1(X0)
| ~ c3_2(X0,a712) ) ).
cnf(u4502,negated_conjecture,
( ~ c6_2(X0,a675)
| ~ c3_2(X0,a636)
| c10_1(X0)
| ~ sP43(X0)
| ~ c9_2(X0,a636)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u4102,negated_conjecture,
( ~ c9_2(X0,X1)
| ~ c1_1(X0)
| ~ sP28(X0)
| ~ c8_1(X0)
| ~ c2_2(X0,X1)
| ~ c6_1(X0)
| c1_2(X0,X1) ) ).
cnf(u6408,negated_conjecture,
( ~ c9_2(X0,a748)
| c3_2(X0,a713)
| c2_1(X0)
| c5_2(X0,a713)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP18(X0)
| c8_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a748)
| c5_2(X0,a744)
| c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u4882,negated_conjecture,
( ~ c9_2(X0,a716)
| c4_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ sP17(X0)
| ~ c6_1(X0)
| c2_1(X0)
| ~ sP31(X0) ) ).
cnf(u401,axiom,
( c9_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u4995,negated_conjecture,
( c6_2(X0,a676)
| c1_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| c2_2(X0,a712)
| c5_2(X0,a712)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u4513,negated_conjecture,
( ~ c6_2(X0,a712)
| ~ c3_2(X0,a662)
| c10_1(X0)
| ~ sP36(X0)
| ~ c9_2(X0,a662)
| ~ c3_2(X0,a712)
| sP18(X0) ) ).
cnf(u3704,negated_conjecture,
( c5_2(X0,a747)
| c5_2(X0,a684)
| c3_1(X0)
| ~ c8_1(X0)
| sP27(X0)
| ~ c2_1(X0)
| c10_1(X0) ) ).
cnf(u4745,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP28(X0)
| ~ c8_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c1_2(X0,a747)
| ~ sP43(X0)
| ~ c2_1(X0)
| c5_2(X0,a636)
| c3_2(X0,a636) ) ).
cnf(u5029,negated_conjecture,
( c7_2(X0,a714)
| c5_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| ~ c2_1(X0)
| c8_2(X0,a747)
| c6_2(X0,a747) ) ).
cnf(u3856,negated_conjecture,
( c6_2(X0,X1)
| ~ c8_1(X0)
| c4_2(X0,X1)
| ~ c6_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c5_2(X0,a747) ) ).
cnf(u407,axiom,
( ~ c10_2(X0,a750)
| ~ sP3(X0) ) ).
cnf(u5010,negated_conjecture,
( c3_2(X0,a751)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_1(X0)
| c4_2(X0,a744)
| c7_1(X0) ) ).
cnf(u8944,negated_conjecture,
( c6_2(X0,a747)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| ~ c6_1(X0)
| c5_2(X0,a636)
| c5_2(X0,a744)
| ~ c8_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744) ) ).
cnf(u7212,negated_conjecture,
( c9_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| c10_1(X0)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c2_2(X0,a751)
| c7_1(X0)
| c1_1(X0) ) ).
cnf(u5365,negated_conjecture,
( ~ c9_2(X0,a743)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c8_1(X0)
| c3_2(X0,a714)
| ~ c9_1(X0)
| ~ c10_1(X0)
| c2_1(X0)
| sP5(X0)
| ~ c6_1(X0)
| ~ c3_2(X0,a662) ) ).
cnf(u4389,negated_conjecture,
( c7_2(X0,a714)
| ~ c8_1(X0)
| c8_2(X0,a677)
| c6_2(X0,a677)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP30(X0) ) ).
cnf(u3239,negated_conjecture,
( c9_2(X0,a747)
| ~ ndr1_1(X0)
| c5_2(X0,a684)
| c3_2(X0,a684)
| ~ c2_1(X0)
| ~ c8_1(X0)
| sP27(X0) ) ).
cnf(u5674,negated_conjecture,
( ~ c6_2(X0,a712)
| c3_2(X0,a750)
| c8_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c10_1(X0)
| ~ sP3(X0)
| c5_2(X0,a750)
| ~ c3_2(X0,a712)
| sP18(X0) ) ).
cnf(u6313,negated_conjecture,
( ~ c9_2(X0,a743)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| c6_2(X0,a747)
| ~ c8_1(X0)
| sP5(X0)
| ~ sP31(X0)
| ~ c3_2(X0,a747) ) ).
cnf(u6460,negated_conjecture,
( c10_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a743)
| c3_2(X0,a743)
| c8_1(X0)
| sP5(X0)
| c6_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| c3_2(X0,a748)
| ~ sP43(X0)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a636) ) ).
cnf(u6709,negated_conjecture,
( ~ c4_2(X0,a747)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| c6_2(X0,a747)
| ~ c4_1(X0)
| c3_2(X0,a747)
| c5_2(X0,a636) ) ).
cnf(u6542,negated_conjecture,
( ~ c6_2(X0,a676)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c9_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| c4_2(X0,a716)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u290,axiom,
( c3_2(X0,a685)
| ~ sP27(X0) ) ).
cnf(u202,axiom,
( ~ c4_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u3500,negated_conjecture,
( ~ c3_2(X0,a712)
| c5_2(X0,a712)
| ~ c10_1(X0)
| ~ c8_1(X0)
| sP18(X0) ) ).
cnf(u6438,negated_conjecture,
( ~ c9_2(X0,a748)
| c3_2(X0,a744)
| c2_1(X0)
| c5_2(X0,a744)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP5(X0)
| c8_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a748) ) ).
cnf(u291,axiom,
( c10_2(X0,a685)
| ~ sP27(X0) ) ).
cnf(u5943,negated_conjecture,
( ~ c6_2(X0,a676)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u4490,negated_conjecture,
( ~ c5_2(X0,a714)
| c2_1(X0)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c8_1(X0)
| ~ c9_1(X0)
| c8_2(X0,a662) ) ).
cnf(u6553,negated_conjecture,
( ~ c6_2(X0,a676)
| c1_1(X0)
| c6_2(X0,a636)
| ~ sP17(X0)
| ~ c9_2(X0,a716)
| c10_1(X0)
| ~ sP43(X0)
| c4_2(X0,a716)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u6944,negated_conjecture,
( ~ c6_2(X0,a712)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ sP17(X0)
| ~ c9_2(X0,a716)
| c10_1(X0)
| ~ sP31(X0)
| c4_2(X0,a716)
| ~ c3_2(X0,a712)
| sP18(X0) ) ).
cnf(u5031,negated_conjecture,
( ~ c8_2(X0,a747)
| c5_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| ~ c2_1(X0)
| c1_2(X0,a747) ) ).
cnf(u6197,negated_conjecture,
( ~ c2_2(X0,a713)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c8_1(X0)
| c2_1(X0)
| c4_2(X0,a662)
| ~ c9_1(X0)
| c1_2(X0,a713)
| ~ sP18(X0) ) ).
cnf(u3511,negated_conjecture,
( c10_2(X0,a748)
| c1_2(X0,X1)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0) ) ).
cnf(u5164,negated_conjecture,
( ~ c9_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ sP17(X0)
| ~ c3_1(X0)
| ~ c8_1(X0)
| c4_2(X0,a716)
| c6_2(X0,a716) ) ).
cnf(u7474,negated_conjecture,
( ~ c3_2(X0,a744)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| c10_1(X0)
| ~ sP31(X0) ) ).
cnf(u5564,negated_conjecture,
( ~ c9_2(X0,a748)
| c8_1(X0)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a748)
| c5_2(X0,X1)
| c5_2(X0,X2)
| c2_2(X0,X2)
| ~ c6_1(X0)
| c3_2(X0,X2)
| c3_2(X0,X1) ) ).
cnf(u7426,negated_conjecture,
( ~ c6_2(X0,a675)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a747)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u3912,negated_conjecture,
( ~ c6_2(X0,a636)
| c2_2(X0,a751)
| c7_1(X0)
| c9_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u4528,negated_conjecture,
( c10_2(X0,a748)
| c10_2(X0,X1)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ sP31(X0)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0) ) ).
cnf(u9368,negated_conjecture,
( c4_2(X0,a676)
| ~ sP5(X0)
| ~ c8_1(X0)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| ~ c6_1(X0)
| sP18(X0)
| c1_1(X0)
| c7_1(X0)
| c2_2(X0,a751)
| ~ c10_1(X0)
| ~ c4_1(X0) ) ).
cnf(u9309,negated_conjecture,
( c9_2(X0,a636)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c4_2(X0,a676)
| c1_1(X0)
| ~ sP43(X0)
| c2_2(X0,a751)
| c7_1(X0)
| ~ c8_1(X0) ) ).
cnf(u8599,negated_conjecture,
( c6_2(X0,a747)
| c6_2(X0,X1)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| ~ c4_1(X0)
| ~ c8_1(X0)
| c5_2(X0,X1)
| ~ sP31(X0)
| c4_2(X0,X1)
| ~ c10_1(X0)
| c5_1(X0) ) ).
cnf(u9050,negated_conjecture,
( ~ c9_2(X0,a748)
| c5_2(X0,a743)
| c3_2(X0,a743)
| c8_1(X0)
| sP5(X0)
| c6_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| c3_2(X0,a748)
| ~ sP31(X0)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ c6_1(X0)
| c2_1(X0)
| ~ c5_1(X0) ) ).
cnf(u6274,negated_conjecture,
( c1_2(X0,a747)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| c6_2(X0,a747)
| ~ c8_1(X0) ) ).
cnf(u7217,negated_conjecture,
( ~ c6_2(X0,a675)
| c6_2(X0,a712)
| sP18(X0)
| ~ c8_1(X0)
| sP27(X0)
| ~ c9_2(X0,a684)
| ~ c3_2(X0,a684)
| c10_1(X0)
| c4_2(X0,a684)
| c1_1(X0)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u6729,negated_conjecture,
( c2_2(X0,a751)
| c1_1(X0)
| ~ c6_1(X0)
| sP18(X0)
| c2_1(X0)
| c7_1(X0)
| ~ c8_1(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ sP5(X0)
| c5_2(X0,a744) ) ).
cnf(u6221,negated_conjecture,
( c3_2(X0,a744)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_1(X0)
| c2_2(X0,a751)
| c7_1(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| c1_1(X0) ) ).
cnf(u7752,negated_conjecture,
( c4_2(X0,a676)
| ~ sP31(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_1(X0)
| c2_2(X0,a751)
| c7_1(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| c1_1(X0)
| c5_2(X0,a744) ) ).
cnf(u7211,negated_conjecture,
( c9_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| c10_1(X0)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c3_2(X0,a751)
| c7_1(X0)
| c1_1(X0) ) ).
cnf(u8412,negated_conjecture,
( ~ c6_2(X0,a636)
| c3_2(X0,a713)
| c2_1(X0)
| c5_2(X0,a713)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP18(X0)
| ~ c9_2(X0,a748)
| c8_1(X0)
| ~ c6_1(X0)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u5661,negated_conjecture,
( c2_2(X0,a751)
| sP18(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c2_2(X0,a712)
| c5_2(X0,a712)
| ~ c9_1(X0)
| c2_1(X0)
| c7_1(X0)
| c1_1(X0) ) ).
cnf(u4170,negated_conjecture,
( ~ c9_2(X0,a636)
| ~ sP43(X0)
| c2_1(X0)
| ~ c6_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a636) ) ).
cnf(u201,axiom,
( c10_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u7772,negated_conjecture,
( ~ c9_2(X0,a748)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a748)
| c5_2(X0,X1)
| c8_1(X0)
| ~ sP31(X0)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ c6_1(X0)
| c3_2(X0,X1) ) ).
cnf(u5331,negated_conjecture,
( ~ c9_2(X0,a662)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c9_1(X0)
| ~ c10_1(X0)
| c2_1(X0)
| c4_2(X0,a662)
| c5_1(X0)
| ~ c6_1(X0) ) ).
cnf(u5665,negated_conjecture,
( ~ c9_2(X0,a662)
| sP18(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c2_2(X0,a712)
| c5_2(X0,a712)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c3_2(X0,a662)
| ~ sP36(X0)
| c1_1(X0)
| ~ c3_2(X0,a712) ) ).
cnf(u3794,negated_conjecture,
( c5_2(X0,a747)
| ~ c2_1(X0)
| c5_2(X0,a712)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| ~ c10_1(X0) ) ).
cnf(u4033,negated_conjecture,
( c7_2(X0,a677)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP30(X0) ) ).
cnf(u4812,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c2_1(X0)
| c3_2(X0,a676)
| ~ c8_1(X0)
| ~ c1_1(X0)
| ~ sP28(X0)
| ~ c6_1(X0)
| c1_2(X0,a747) ) ).
cnf(u6102,negated_conjecture,
( ~ c3_2(X0,a636)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP31(X0)
| c2_2(X0,a676)
| ~ c9_1(X0)
| c3_1(X0)
| c5_2(X0,a636)
| c4_2(X0,a676) ) ).
cnf(u4829,negated_conjecture,
( ~ c9_2(X0,a684)
| c4_2(X0,a684)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c8_1(X0)
| sP27(X0)
| ~ c6_1(X0)
| c2_1(X0)
| ~ sP43(X0) ) ).
cnf(u4568,negated_conjecture,
( c1_2(X0,a748)
| c3_2(X0,X1)
| c8_1(X0)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a748)
| c5_2(X0,X1) ) ).
cnf(u6787,negated_conjecture,
( ~ c1_2(X0,X1)
| c6_2(X0,a747)
| c5_2(X0,a712)
| ~ c6_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a714)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c8_1(X0) ) ).
cnf(u5667,negated_conjecture,
( ~ c3_2(X0,a712)
| sP18(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c2_2(X0,a712)
| c5_2(X0,a712)
| ~ c9_1(X0)
| c3_1(X0)
| c1_1(X0) ) ).
cnf(u345,axiom,
( ~ sP17(X0)
| ndr1_1(X0) ) ).
cnf(u5988,negated_conjecture,
( ~ c9_2(X0,a748)
| c8_1(X0)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| c5_2(X0,X1)
| ~ c3_2(X0,a748)
| c10_1(X0)
| c3_2(X0,X1)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u4707,negated_conjecture,
( ~ c9_2(X0,a748)
| c10_1(X0)
| ~ c3_2(X0,a748)
| ~ c3_2(X0,a744)
| c10_2(X0,X1)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c8_1(X0)
| ~ sP5(X0) ) ).
cnf(u3957,negated_conjecture,
( ~ c9_2(X0,a662)
| ~ c3_1(X0)
| ~ c8_1(X0)
| ~ sP36(X0) ) ).
cnf(u7015,negated_conjecture,
( c2_2(X0,a748)
| c8_1(X0)
| c5_2(X0,a744)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP5(X0)
| ~ c6_1(X0)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c3_1(X0) ) ).
cnf(u4457,negated_conjecture,
( c3_2(X0,a750)
| c5_2(X0,a750)
| ~ sP3(X0)
| c8_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u7540,negated_conjecture,
( ~ c9_2(X0,a684)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ c8_1(X0)
| sP27(X0)
| c4_2(X0,a684)
| ~ c3_2(X0,a684)
| c10_1(X0)
| ~ sP31(X0)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u6993,negated_conjecture,
( c9_2(X0,a675)
| c4_2(X0,a684)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c2_2(X0,a751)
| c7_1(X0)
| c1_1(X0) ) ).
cnf(u8055,negated_conjecture,
( ~ c2_2(X0,a744)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c5_2(X0,a744)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a744) ) ).
cnf(u5069,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP30(X0)
| ~ c8_1(X0)
| ~ c1_1(X0)
| c4_2(X0,a677)
| ~ c6_1(X0)
| c1_2(X0,a747)
| c10_1(X0)
| c3_2(X0,a662)
| ~ sP36(X0)
| ~ c2_1(X0)
| c5_2(X0,a662)
| ~ c5_1(X0) ) ).
cnf(u7284,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747)
| ~ sP5(X0)
| c4_2(X0,a744)
| c5_2(X0,a744) ) ).
cnf(u7982,negated_conjecture,
( c3_2(X0,a751)
| ~ sP43(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c1_1(X0)
| c7_1(X0)
| c4_2(X0,a684)
| ~ c6_1(X0) ) ).
cnf(u4103,negated_conjecture,
( ~ c2_2(X0,a713)
| ~ c5_2(X0,a684)
| ~ sP18(X0)
| c4_2(X0,a684)
| ~ c8_1(X0)
| c1_2(X0,a713)
| sP27(X0) ) ).
cnf(u4465,negated_conjecture,
( c10_2(X0,a684)
| ~ sP43(X0)
| c4_2(X0,a684)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c8_1(X0)
| sP27(X0) ) ).
cnf(u4741,negated_conjecture,
( ~ c2_2(X0,a713)
| ~ sP28(X0)
| ~ c8_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c1_2(X0,a713)
| ~ sP18(X0) ) ).
cnf(u9095,negated_conjecture,
( ~ c1_2(X0,a748)
| c5_2(X0,a743)
| c3_2(X0,a743)
| sP5(X0)
| c6_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| c3_2(X0,a748)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ c6_1(X0)
| ~ c5_1(X0)
| c2_1(X0)
| ~ c9_2(X0,a748) ) ).
cnf(u8413,negated_conjecture,
( ~ c9_2(X0,a748)
| c3_2(X0,a713)
| c2_1(X0)
| c5_2(X0,a713)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP18(X0)
| ~ c6_1(X0)
| c8_1(X0)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u247,axiom,
( ~ c2_2(X0,a662)
| ~ sP36(X0) ) ).
cnf(u5856,negated_conjecture,
( ~ c1_2(X0,a748)
| ~ c6_1(X0)
| c3_2(X0,a713)
| c2_1(X0)
| c5_2(X0,a713)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP18(X0)
| c8_1(X0)
| ~ c9_2(X0,a748) ) ).
cnf(u7429,negated_conjecture,
( ~ c6_2(X0,a712)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a747)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c3_2(X0,a712)
| sP18(X0) ) ).
cnf(u6786,negated_conjecture,
( ~ c9_2(X0,a743)
| c6_2(X0,a747)
| c5_2(X0,a712)
| ~ c6_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a714)
| sP5(X0)
| ~ c8_1(X0)
| ~ c3_2(X0,a747) ) ).
cnf(u7272,negated_conjecture,
( ~ c2_2(X0,a713)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a713)
| ~ sP18(X0) ) ).
cnf(u4471,negated_conjecture,
( c10_2(X0,a744)
| ~ sP43(X0)
| c4_2(X0,a744)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0) ) ).
cnf(u7409,negated_conjecture,
( ~ c6_2(X0,a712)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c9_2(X0,a747)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c3_2(X0,a712)
| sP18(X0) ) ).
cnf(u7178,negated_conjecture,
( ~ c9_2(X0,a685)
| c1_1(X0)
| c4_2(X0,a744)
| sP18(X0)
| ~ sP5(X0)
| c10_1(X0)
| ~ c6_1(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| ~ sP27(X0)
| ~ c8_1(X0)
| ~ c3_2(X0,a712) ) ).
cnf(u7182,negated_conjecture,
( c4_2(X0,a744)
| c1_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| ~ sP5(X0)
| c10_1(X0)
| ~ c6_1(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c7_1(X0)
| c2_2(X0,a751) ) ).
cnf(u4112,negated_conjecture,
( c9_2(X0,a747)
| c10_1(X0)
| c3_2(X0,a636)
| ~ sP43(X0)
| ~ c2_1(X0)
| c5_2(X0,a636)
| ~ c5_1(X0) ) ).
cnf(u3958,negated_conjecture,
( c5_2(X0,a662)
| ~ sP36(X0)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u5378,negated_conjecture,
( c3_2(X0,a744)
| ~ c8_1(X0)
| c1_1(X0)
| ~ c6_1(X0)
| sP18(X0)
| c2_1(X0)
| c7_1(X0)
| c2_2(X0,a751)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ sP5(X0) ) ).
cnf(u5761,negated_conjecture,
( ~ c9_2(X0,a685)
| c1_1(X0)
| ~ sP31(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| c2_2(X0,a676)
| ~ c9_1(X0)
| c2_1(X0)
| ~ sP27(X0)
| c4_2(X0,a676)
| ~ c3_2(X0,a676) ) ).
cnf(u4883,negated_conjecture,
( ~ c8_2(X0,X1)
| c4_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ sP17(X0)
| ~ c9_2(X0,a716)
| c10_1(X0)
| ~ sP31(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u5669,negated_conjecture,
( ~ c6_2(X0,a636)
| c3_2(X0,a750)
| c8_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c10_1(X0)
| ~ sP3(X0)
| c5_2(X0,a750)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u6350,negated_conjecture,
( c4_2(X0,a662)
| ~ c6_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a662)
| ~ c8_1(X0)
| c5_2(X0,a747)
| ~ sP36(X0)
| ~ c10_1(X0) ) ).
cnf(u7400,negated_conjecture,
( c1_2(X0,a747)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| c6_2(X0,a747)
| c5_2(X0,a744) ) ).
cnf(u4599,negated_conjecture,
( c1_2(X0,a748)
| c3_2(X0,a748)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,a713)
| c3_2(X0,a713)
| c8_1(X0)
| ~ sP18(X0) ) ).
cnf(u7724,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| c5_2(X0,a636)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747)
| ~ sP31(X0)
| c4_2(X0,a676) ) ).
cnf(u6383,negated_conjecture,
( ~ c9_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a744)
| c3_2(X0,a744)
| c8_1(X0)
| ~ c6_1(X0)
| c2_1(X0)
| c10_1(X0)
| ~ sP5(X0)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c3_2(X0,X1)
| c3_2(X0,a748) ) ).
cnf(u3230,negated_conjecture,
( ~ c1_2(X0,a748)
| c5_2(X0,a748)
| c3_2(X0,a748)
| c8_1(X0)
| ~ c6_1(X0)
| ~ ndr1_1(X0)
| c2_1(X0)
| ~ c9_2(X0,a748) ) ).
cnf(u4092,negated_conjecture,
( ~ c1_2(X0,a685)
| ~ c6_1(X0)
| ~ sP27(X0)
| c2_1(X0)
| ~ c9_2(X0,a685) ) ).
cnf(u4099,negated_conjecture,
( ~ c8_2(X0,a683)
| ~ c1_1(X0)
| ~ sP28(X0)
| ~ c9_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| c1_2(X0,a683) ) ).
cnf(u5495,negated_conjecture,
( c9_2(X0,a747)
| c4_2(X0,a662)
| ~ c6_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a662)
| c3_2(X0,a662)
| ~ c8_1(X0)
| ~ sP36(X0) ) ).
cnf(u4624,negated_conjecture,
( c10_2(X0,a748)
| c10_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| c4_2(X0,X1)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0) ) ).
cnf(u9162,negated_conjecture,
( ~ c9_2(X0,a748)
| c3_2(X0,a743)
| sP5(X0)
| c6_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| c3_2(X0,a748)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ c6_1(X0)
| ~ c5_1(X0)
| c2_1(X0)
| c5_2(X0,a743) ) ).
cnf(u7302,negated_conjecture,
( ~ c9_2(X0,a716)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ sP17(X0)
| c1_1(X0)
| c10_1(X0)
| c4_2(X0,a716)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u4379,negated_conjecture,
( ~ c5_2(X0,a714)
| ~ c8_1(X0)
| c8_2(X0,a677)
| c6_2(X0,a677)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP30(X0) ) ).
cnf(u4246,negated_conjecture,
( c3_2(X0,a662)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP36(X0)
| ~ c2_1(X0)
| c5_2(X0,a662)
| c5_2(X0,a747) ) ).
cnf(u6552,negated_conjecture,
( ~ c6_2(X0,a675)
| c1_1(X0)
| c6_2(X0,a636)
| ~ sP17(X0)
| ~ c9_2(X0,a716)
| c10_1(X0)
| ~ sP43(X0)
| c4_2(X0,a716)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u6237,negated_conjecture,
( ~ c9_2(X0,a662)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c3_2(X0,a662)
| c10_1(X0)
| ~ sP36(X0)
| c4_2(X0,a684)
| ~ c3_2(X0,a636) ) ).
cnf(u7296,negated_conjecture,
( ~ c6_2(X0,a712)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ sP17(X0)
| ~ c9_2(X0,a716)
| c10_1(X0)
| c4_2(X0,a716)
| c1_1(X0)
| ~ c3_2(X0,a712)
| sP18(X0) ) ).
cnf(u274,axiom,
( ~ sP30(X0)
| ndr1_1(X0) ) ).
cnf(u7680,negated_conjecture,
( ~ c6_2(X0,a636)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ c8_1(X0)
| sP27(X0)
| ~ c9_2(X0,a684)
| ~ c3_2(X0,a684)
| c10_1(X0)
| c4_2(X0,a684)
| c1_1(X0)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u3892,negated_conjecture,
( ~ c3_2(X0,a636)
| ~ sP43(X0)
| c5_2(X0,a636)
| ~ c10_1(X0)
| ~ c8_1(X0) ) ).
cnf(u3611,negated_conjecture,
( c3_2(X0,a675)
| ~ c10_1(X0)
| ~ c4_1(X0)
| sP31(X0)
| sP30(X0)
| ~ c8_1(X0)
| ~ c6_1(X0) ) ).
cnf(u3890,negated_conjecture,
( ~ c2_2(X0,a747)
| c3_2(X0,a712)
| ~ c2_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| ~ c5_2(X0,a684)
| c5_2(X0,a712)
| c4_2(X0,a684)
| c1_2(X0,a747)
| sP27(X0) ) ).
cnf(u5512,negated_conjecture,
( c9_2(X0,a747)
| c4_2(X0,a713)
| ~ c6_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a713)
| c3_2(X0,a713)
| ~ c8_1(X0)
| ~ sP18(X0) ) ).
cnf(u402,axiom,
( ~ sP5(X0)
| ndr1_1(X0) ) ).
cnf(u7723,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| c5_2(X0,a636)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747)
| ~ sP5(X0)
| c4_2(X0,a744)
| c5_2(X0,a744) ) ).
cnf(u9014,negated_conjecture,
( ~ c3_2(X0,a636)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c3_2(X0,a751)
| c7_1(X0)
| c1_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0) ) ).
cnf(u4413,negated_conjecture,
( ~ c9_2(X0,a685)
| ~ sP27(X0)
| c2_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c4_2(X0,a685)
| ~ c1_1(X0)
| c5_1(X0) ) ).
cnf(u9235,negated_conjecture,
( c6_2(X0,a747)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| ~ sP5(X0)
| c5_2(X0,a744)
| ~ c8_1(X0) ) ).
cnf(u6930,negated_conjecture,
( c6_2(X0,a747)
| c4_2(X0,a747)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a747)
| c3_2(X0,a747)
| ~ c6_1(X0)
| ~ c8_1(X0) ) ).
cnf(u6673,negated_conjecture,
( ~ c9_2(X0,a685)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| c2_2(X0,a712)
| c5_2(X0,a712)
| ~ c9_1(X0)
| c2_1(X0)
| ~ sP27(X0)
| c1_1(X0)
| ~ c3_2(X0,a676) ) ).
cnf(u6836,negated_conjecture,
( ~ c9_2(X0,a636)
| c1_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c3_2(X0,a636)
| ~ sP43(X0)
| c4_2(X0,a684)
| ~ c3_2(X0,a676) ) ).
cnf(u5401,negated_conjecture,
( c10_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0)
| c3_2(X0,X1)
| ~ sP43(X0)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a636) ) ).
cnf(u4252,negated_conjecture,
( ~ c9_2(X0,a662)
| ~ sP36(X0)
| c2_1(X0)
| ~ c6_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a662) ) ).
cnf(u5155,negated_conjecture,
( ~ c9_2(X0,a748)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,a713)
| c3_2(X0,a713)
| c8_1(X0)
| ~ sP18(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c6_1(X0)
| c10_2(X0,X1)
| c2_1(X0)
| c3_2(X0,a748) ) ).
cnf(u7804,negated_conjecture,
( ~ c3_2(X0,a744)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c6_2(X0,a712)
| sP18(X0)
| c1_1(X0)
| ~ c3_2(X0,a676) ) ).
cnf(u400,axiom,
( c6_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u6706,negated_conjecture,
( c1_2(X0,a747)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| c6_2(X0,a747)
| c5_2(X0,a636) ) ).
cnf(u3499,negated_conjecture,
( c7_2(X0,a675)
| ~ c1_1(X0)
| ~ c6_1(X0)
| sP30(X0)
| sP31(X0) ) ).
cnf(u5302,negated_conjecture,
( ~ c8_2(X0,X1)
| c4_2(X0,a744)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| ~ c3_2(X0,a744)
| c10_1(X0)
| ~ sP31(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u6182,negated_conjecture,
( c4_2(X0,a684)
| c1_1(X0)
| sP18(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c7_1(X0)
| c2_2(X0,a751) ) ).
cnf(u4522,negated_conjecture,
( ~ c9_2(X0,a716)
| c4_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c3_1(X0)
| ~ c8_1(X0)
| ~ sP17(X0)
| c6_2(X0,a716) ) ).
cnf(u7983,negated_conjecture,
( ~ c3_2(X0,a744)
| ~ sP43(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c3_2(X0,a751)
| c7_1(X0)
| c4_2(X0,a684)
| ~ c3_2(X0,a636)
| c10_1(X0)
| c1_1(X0)
| ~ sP5(X0) ) ).
cnf(u6213,negated_conjecture,
( c2_2(X0,a751)
| ~ sP31(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| c2_2(X0,a676)
| ~ c9_1(X0)
| c2_1(X0)
| c1_1(X0)
| c7_1(X0)
| ~ c10_1(X0)
| ~ c4_1(X0) ) ).
cnf(u6343,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c6_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a713)
| c3_2(X0,a713)
| ~ c8_1(X0)
| ~ sP18(X0)
| ~ sP30(X0)
| c4_2(X0,a713)
| c4_2(X0,a677)
| c1_2(X0,a747) ) ).
cnf(u5303,negated_conjecture,
( c6_2(X0,a676)
| c4_2(X0,a744)
| c1_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_1(X0) ) ).
cnf(u5049,negated_conjecture,
( ~ c8_2(X0,X2)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c9_2(X0,a747)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c3_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c3_2(X0,X2) ) ).
cnf(u4169,negated_conjecture,
( ~ c9_2(X0,a636)
| ~ sP43(X0)
| c2_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0) ) ).
cnf(u4409,negated_conjecture,
( c3_2(X0,a676)
| ~ c6_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c5_2(X0,a747) ) ).
cnf(u4539,negated_conjecture,
( c10_2(X0,a744)
| ~ sP31(X0)
| c4_2(X0,a744)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0) ) ).
cnf(u6341,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c6_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a713)
| c3_2(X0,a713)
| ~ c8_1(X0)
| ~ sP18(X0)
| ~ c5_2(X0,a684)
| c4_2(X0,a713)
| c4_2(X0,a684)
| c1_2(X0,a747)
| sP27(X0) ) ).
cnf(u3656,negated_conjecture,
( ~ c1_2(X0,X1)
| c10_2(X0,X1)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0) ) ).
cnf(u4526,negated_conjecture,
( ~ c8_2(X0,X1)
| c4_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c9_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u3670,negated_conjecture,
( c9_2(X0,a747)
| c3_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a748)
| c8_1(X0)
| ~ c2_1(X0)
| c10_1(X0) ) ).
cnf(u5469,negated_conjecture,
( c6_2(X0,a747)
| c4_2(X0,a747)
| ~ c8_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a676)
| ~ c6_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676) ) ).
cnf(u4537,negated_conjecture,
( c10_2(X0,a748)
| ~ sP31(X0)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| c10_1(X0)
| c3_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a748)
| c8_1(X0) ) ).
cnf(u4811,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c2_1(X0)
| c3_2(X0,a676)
| ~ c8_1(X0)
| ~ c5_2(X0,a684)
| ~ c6_1(X0)
| c4_2(X0,a684)
| c1_2(X0,a747)
| sP27(X0) ) ).
cnf(u3798,negated_conjecture,
( c7_2(X0,a747)
| c5_2(X0,a712)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u7100,negated_conjecture,
( ~ c6_2(X0,a636)
| c4_2(X0,a744)
| ~ c8_1(X0)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c3_2(X0,a744)
| c10_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u6477,negated_conjecture,
( ~ c9_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a743)
| c3_2(X0,a743)
| c8_1(X0)
| sP5(X0)
| c6_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ c6_1(X0)
| c1_2(X0,X1)
| c2_1(X0)
| c3_2(X0,a748) ) ).
cnf(u4183,negated_conjecture,
( ~ c3_2(X0,a744)
| ~ sP5(X0)
| c5_2(X0,a744)
| ~ c10_1(X0)
| ~ c8_1(X0) ) ).
cnf(u3530,negated_conjecture,
( c3_2(X0,a684)
| c5_2(X0,a684)
| ~ c2_1(X0)
| c5_2(X0,a747)
| ~ c8_1(X0)
| sP27(X0) ) ).
cnf(u3939,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c9_2(X0,a636)
| ~ c3_2(X0,a636)
| c10_1(X0)
| ~ sP43(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u6096,negated_conjecture,
( ~ c9_2(X0,a662)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP31(X0)
| c2_2(X0,a676)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c3_2(X0,a662)
| c10_1(X0)
| ~ sP36(X0)
| c4_2(X0,a676)
| ~ c3_2(X0,a636) ) ).
cnf(u7642,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c8_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c6_1(X0)
| c4_2(X0,a747)
| c5_2(X0,a712)
| c1_2(X0,a747)
| ~ sP31(X0)
| c4_2(X0,a676) ) ).
cnf(u7273,negated_conjecture,
( ~ c2_2(X0,a744)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u4938,negated_conjecture,
( c6_2(X0,a636)
| c4_2(X0,a744)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_1(X0) ) ).
cnf(u6235,negated_conjecture,
( ~ c9_2(X0,a636)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c3_2(X0,a636)
| c10_1(X0)
| c4_2(X0,a684) ) ).
cnf(u8045,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c5_2(X0,a744)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747)
| c4_2(X0,a713)
| c5_1(X0)
| c5_2(X0,a713)
| c3_2(X0,a713)
| ~ sP18(X0) ) ).
cnf(u5454,negated_conjecture,
( c6_2(X0,a747)
| c4_2(X0,a747)
| ~ c8_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a744)
| c3_2(X0,a744)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744) ) ).
cnf(u200,axiom,
( c8_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u4934,negated_conjecture,
( c6_2(X0,a636)
| c4_2(X0,a744)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_2(X0,a744)
| c5_2(X0,a744)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u6252,negated_conjecture,
( ~ c8_2(X0,a714)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c2_1(X0)
| c8_2(X0,a747)
| c6_2(X0,a747)
| ~ c8_1(X0)
| c1_2(X0,a714) ) ).
cnf(u3286,negated_conjecture,
( ~ c10_2(X121,X122)
| ~ c5_1(X121)
| c10_1(X121)
| c3_2(X121,X122)
| c1_2(X121,X122) ) ).
cnf(u5085,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ c2_1(X0)
| c5_2(X0,a744)
| c3_2(X0,a744)
| ~ c8_1(X0)
| ~ c1_1(X0)
| ~ sP30(X0)
| ~ c6_1(X0)
| c4_2(X0,a677)
| c1_2(X0,a747) ) ).
cnf(u5487,negated_conjecture,
( ~ c9_2(X0,X1)
| c5_2(X0,a744)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c2_2(X0,X1)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,X1) ) ).
cnf(u4695,negated_conjecture,
( ~ c1_2(X0,X1)
| c3_2(X0,a743)
| c8_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0)
| sP5(X0)
| c6_2(X0,X1)
| ~ c3_2(X0,X1)
| c5_2(X0,a743) ) ).
cnf(u5151,negated_conjecture,
( c10_2(X0,a748)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,a713)
| c3_2(X0,a713)
| c8_1(X0)
| ~ sP18(X0)
| c3_2(X0,a748)
| ~ sP31(X0)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676) ) ).
cnf(u356,axiom,
( ~ sP14(X0)
| ndr1_1(X0) ) ).
cnf(u4507,negated_conjecture,
( ~ c9_2(X0,a636)
| ~ c3_2(X0,a636)
| c10_1(X0)
| ~ sP43(X0)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u5909,negated_conjecture,
( ~ c1_2(X0,a748)
| ~ c6_1(X0)
| c3_2(X0,a744)
| c2_1(X0)
| c5_2(X0,a744)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP5(X0)
| c8_1(X0)
| ~ c9_2(X0,a748) ) ).
cnf(u6380,negated_conjecture,
( ~ c9_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a744)
| c3_2(X0,a744)
| c8_1(X0)
| ~ c6_1(X0)
| c2_1(X0)
| c10_1(X0)
| ~ sP5(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,X1)
| c3_2(X0,a748) ) ).
cnf(u8028,negated_conjecture,
( ~ c3_2(X0,a744)
| ~ c8_1(X0)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| c4_2(X0,a744)
| ~ c6_1(X0)
| ~ sP5(X0)
| ~ c3_2(X0,a636)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747) ) ).
cnf(u4978,negated_conjecture,
( ~ c9_2(X0,a685)
| c4_2(X0,a744)
| ~ c8_1(X0)
| c1_1(X0)
| ~ c6_1(X0)
| sP18(X0)
| c2_1(X0)
| c10_1(X0)
| ~ sP27(X0)
| ~ sP5(X0)
| ~ c3_2(X0,a712) ) ).
cnf(u9372,negated_conjecture,
( c2_2(X0,a751)
| ~ c8_1(X0)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| ~ c6_1(X0)
| sP18(X0)
| c1_1(X0)
| c7_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0) ) ).
cnf(u6354,negated_conjecture,
( c4_2(X0,a713)
| ~ c6_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a713)
| ~ c8_1(X0)
| c5_2(X0,a747)
| ~ sP18(X0)
| ~ c10_1(X0) ) ).
cnf(u7641,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c8_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c6_1(X0)
| c4_2(X0,a747)
| c5_2(X0,a712)
| c1_2(X0,a747)
| ~ sP5(X0)
| c4_2(X0,a744)
| c5_2(X0,a744) ) ).
cnf(u3948,negated_conjecture,
( c1_2(X0,a662)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a662)
| ~ sP36(X0) ) ).
cnf(u7288,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747)
| c5_2(X0,a684)
| c3_2(X0,a684)
| sP27(X0) ) ).
cnf(u4704,negated_conjecture,
( ~ c6_2(X0,a676)
| c10_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| ~ c3_2(X0,a676)
| c10_2(X0,X1)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c8_1(X0)
| ~ sP31(X0) ) ).
cnf(u3946,negated_conjecture,
( ~ c9_2(X0,a743)
| ~ c6_1(X0)
| ~ sP43(X0)
| sP5(X0)
| ~ c8_1(X0)
| ~ c3_2(X0,a636)
| c6_2(X0,a636) ) ).
cnf(u7291,negated_conjecture,
( ~ c6_2(X0,a636)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ sP17(X0)
| ~ c9_2(X0,a716)
| c10_1(X0)
| c4_2(X0,a716)
| c1_1(X0)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u4070,negated_conjecture,
( ~ c9_2(X0,X1)
| ~ c1_1(X0)
| ~ sP30(X0)
| ~ c8_1(X0)
| ~ c2_2(X0,X1)
| c4_2(X0,a677)
| ~ c6_1(X0)
| c1_2(X0,X1) ) ).
cnf(u7289,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747)
| c5_2(X0,a712)
| sP18(X0) ) ).
cnf(u8058,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c5_2(X0,a744)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747)
| c4_2(X0,a744) ) ).
cnf(u3329,negated_conjecture,
( ~ c4_2(X0,a675)
| sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| c3_2(X0,a675)
| sP30(X0) ) ).
cnf(u268,axiom,
( ~ c9_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u6411,negated_conjecture,
( ~ c9_2(X0,a748)
| c3_2(X0,a713)
| c2_1(X0)
| c5_2(X0,a713)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP18(X0)
| c8_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a748) ) ).
cnf(u8929,negated_conjecture,
( c6_2(X0,a747)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| ~ c6_1(X0)
| c5_2(X0,a636)
| c5_2(X0,a684)
| c3_2(X0,a684)
| ~ c8_1(X0)
| sP27(X0) ) ).
cnf(u6951,negated_conjecture,
( ~ c9_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ sP17(X0)
| c4_2(X0,a716)
| c10_1(X0)
| ~ sP31(X0)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u3207,negated_conjecture,
( ~ c6_2(X0,a712)
| ~ ndr1_1(X0)
| c7_1(X0)
| c2_2(X0,a751)
| sP18(X0) ) ).
cnf(u8160,negated_conjecture,
( ~ c3_2(X0,a744)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c3_2(X0,a751)
| c7_1(X0)
| c1_1(X0)
| ~ c3_2(X0,a636)
| ~ c8_1(X0) ) ).
cnf(u7240,negated_conjecture,
( ~ c6_2(X0,a712)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c8_1(X0)
| sP27(X0)
| ~ c9_2(X0,a684)
| ~ c3_2(X0,a684)
| c10_1(X0)
| ~ sP43(X0)
| c4_2(X0,a684)
| ~ c3_2(X0,a712)
| sP18(X0) ) ).
cnf(u5241,negated_conjecture,
( c2_2(X0,a748)
| c8_1(X0)
| c2_2(X0,a732)
| ~ c9_1(X0)
| c2_1(X0)
| c5_2(X0,a732)
| c5_2(X0,a748)
| ~ sP9(X0) ) ).
cnf(u3331,negated_conjecture,
( ~ c6_2(X0,a675)
| sP31(X0)
| c2_2(X0,a751)
| c7_1(X0)
| c9_2(X0,a675)
| sP30(X0) ) ).
cnf(u7950,negated_conjecture,
( c4_2(X0,a684)
| ~ sP43(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c2_2(X0,a751)
| c7_1(X0)
| c1_1(X0)
| ~ c6_1(X0) ) ).
cnf(u287,axiom,
( c6_2(X0,a683)
| ~ sP28(X0) ) ).
cnf(u5402,negated_conjecture,
( c10_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0)
| c3_2(X0,X1)
| ~ sP31(X0)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676) ) ).
cnf(u6198,negated_conjecture,
( ~ c2_2(X0,a744)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c8_1(X0)
| c2_1(X0)
| c4_2(X0,a662)
| ~ c9_1(X0)
| c1_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u5122,negated_conjecture,
( c7_2(X0,a747)
| ~ c2_1(X0)
| c5_2(X0,a744)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0) ) ).
cnf(u6539,negated_conjecture,
( ~ c6_2(X0,a636)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c9_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| c4_2(X0,a716)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u3827,negated_conjecture,
( c10_2(X0,a748)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a747) ) ).
cnf(u5374,negated_conjecture,
( ~ c9_2(X0,a748)
| c8_1(X0)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c6_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| c3_2(X0,a748)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,a713)
| c3_2(X0,a713)
| ~ sP18(X0) ) ).
cnf(u3200,negated_conjecture,
( c1_2(X0,X1)
| ~ c6_1(X0)
| ~ ndr1_1(X0)
| ~ c8_1(X0)
| c4_2(X0,X1)
| c6_2(X0,X1)
| ~ c1_1(X0)
| c5_1(X0) ) ).
cnf(u4495,negated_conjecture,
( ~ c6_2(X0,a675)
| c10_1(X0)
| ~ sP27(X0)
| ~ c9_2(X0,a685)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u7149,negated_conjecture,
( ~ c6_2(X0,a676)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| ~ c3_2(X0,a744)
| ~ sP43(X0)
| c4_2(X0,a744)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u4633,negated_conjecture,
( c10_2(X0,a748)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| c10_1(X0)
| c3_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a748)
| c8_1(X0) ) ).
cnf(u7347,negated_conjecture,
( ~ c8_2(X0,a714)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c2_1(X0)
| c8_2(X0,a747)
| c6_2(X0,a747)
| c5_2(X0,a744)
| c1_2(X0,a714) ) ).
cnf(u6832,negated_conjecture,
( c3_2(X0,a751)
| c1_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c4_2(X0,a684)
| c7_1(X0) ) ).
cnf(u4238,negated_conjecture,
( c10_2(X0,a748)
| ~ sP3(X0)
| c5_2(X0,a750)
| c3_2(X0,a750)
| c8_1(X0) ) ).
cnf(u285,axiom,
( c5_2(X0,a683)
| ~ sP28(X0) ) ).
cnf(u5400,negated_conjecture,
( c10_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0)
| c3_2(X0,X1)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0) ) ).
cnf(u4879,negated_conjecture,
( ~ c9_2(X0,a716)
| c4_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ sP17(X0)
| ~ c3_1(X0)
| ~ c8_1(X0)
| ~ sP31(X0)
| c6_2(X0,a716) ) ).
cnf(u8841,negated_conjecture,
( c6_2(X0,a747)
| c5_2(X0,a712)
| ~ c6_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a714)
| c5_2(X0,a636)
| ~ c8_1(X0)
| ~ sP43(X0) ) ).
cnf(u7713,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| c5_2(X0,a636)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747)
| c4_2(X0,a713)
| c5_1(X0)
| c5_2(X0,a713)
| c3_2(X0,a713)
| ~ sP18(X0) ) ).
cnf(u5007,negated_conjecture,
( ~ c9_2(X0,a662)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_1(X0)
| ~ c3_2(X0,a662)
| c10_1(X0)
| ~ sP36(X0)
| c4_2(X0,a744)
| ~ c3_2(X0,a636) ) ).
cnf(u3729,negated_conjecture,
( c10_2(X0,a712)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c6_1(X0)
| ~ c8_1(X0) ) ).
cnf(u6812,negated_conjecture,
( ~ c9_2(X0,a743)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| c6_2(X0,a747)
| c5_2(X0,a636)
| sP5(X0)
| ~ c8_1(X0)
| ~ c3_2(X0,a747) ) ).
cnf(u4496,negated_conjecture,
( ~ c6_2(X0,a676)
| c10_1(X0)
| ~ sP27(X0)
| ~ c9_2(X0,a685)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u3503,negated_conjecture,
( ~ c3_2(X0,X1)
| c5_2(X0,X1)
| ~ c10_1(X0)
| ~ c8_1(X0)
| c4_2(X0,X1)
| c6_2(X0,X1)
| ~ c1_1(X0)
| c5_1(X0) ) ).
cnf(u5028,negated_conjecture,
( ~ c5_2(X0,a714)
| c5_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| ~ c2_1(X0)
| c8_2(X0,a747)
| c6_2(X0,a747) ) ).
cnf(u5942,negated_conjecture,
( ~ c6_2(X0,a675)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u4408,negated_conjecture,
( c9_2(X0,a747)
| ~ c6_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c2_1(X0)
| c3_2(X0,a676)
| ~ c8_1(X0) ) ).
cnf(u5299,negated_conjecture,
( c6_2(X0,a676)
| c4_2(X0,a744)
| c1_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_2(X0,a744)
| c5_2(X0,a744)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u3995,negated_conjecture,
( ~ c6_2(X0,a676)
| c2_2(X0,a751)
| c7_1(X0)
| ~ sP31(X0) ) ).
cnf(u4734,negated_conjecture,
( c7_2(X0,a747)
| ~ c2_1(X0)
| c5_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0) ) ).
cnf(u5549,negated_conjecture,
( c10_2(X0,a748)
| c3_2(X0,X1)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a748)
| c5_2(X0,X1)
| c8_1(X0)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u5047,negated_conjecture,
( c1_2(X0,a748)
| c3_2(X0,X1)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c9_2(X0,a747)
| c3_2(X0,a748)
| c10_1(X0) ) ).
cnf(u7806,negated_conjecture,
( ~ c9_2(X0,a716)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c6_2(X0,a712)
| sP18(X0)
| c1_1(X0)
| ~ sP17(X0)
| c4_2(X0,a716)
| ~ c3_2(X0,a676) ) ).
cnf(u4937,negated_conjecture,
( ~ c8_2(X0,X1)
| c4_2(X0,a744)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| ~ c3_2(X0,a744)
| c10_1(X0)
| ~ sP43(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u5553,negated_conjecture,
( c10_2(X0,a748)
| c3_2(X0,X1)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a748)
| c5_2(X0,X1)
| c8_1(X0)
| ~ sP31(X0)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676) ) ).
cnf(u3654,negated_conjecture,
( ~ c1_2(X0,X1)
| c10_2(X0,X1)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u5794,negated_conjecture,
( c4_2(X0,a744)
| c1_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_1(X0)
| c2_2(X0,a751)
| c7_1(X0) ) ).
cnf(u5037,negated_conjecture,
( ~ c9_2(X0,a748)
| c3_2(X0,a748)
| c8_1(X0)
| ~ c6_1(X0)
| c2_1(X0)
| c5_2(X0,a748)
| c10_1(X0)
| ~ c5_1(X0) ) ).
cnf(u9308,negated_conjecture,
( c9_2(X0,a636)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c4_2(X0,a676)
| c1_1(X0)
| ~ sP43(X0)
| c3_2(X0,a751)
| c7_1(X0)
| ~ c8_1(X0) ) ).
cnf(u7424,negated_conjecture,
( ~ c6_2(X0,a636)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a747)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u5112,negated_conjecture,
( c5_2(X0,a747)
| ~ c6_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a744)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0) ) ).
cnf(u6604,negated_conjecture,
( ~ c4_2(X0,a747)
| ~ c8_1(X0)
| c6_2(X0,a747)
| c5_2(X0,a712)
| ~ c6_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c4_1(X0)
| c3_2(X0,a747)
| c3_2(X0,a714) ) ).
cnf(u5802,negated_conjecture,
( ~ c9_2(X0,a662)
| c1_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_1(X0)
| ~ c3_2(X0,a662)
| ~ sP36(X0)
| c4_2(X0,a744)
| ~ c3_2(X0,a676) ) ).
cnf(u5982,negated_conjecture,
( ~ c6_2(X0,a675)
| c8_1(X0)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c10_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u4422,negated_conjecture,
( c9_2(X0,a747)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ c2_1(X0)
| c5_2(X0,a744)
| c3_2(X0,a744)
| ~ c8_1(X0) ) ).
cnf(u342,axiom,
( c1_2(X0,a716)
| ~ sP17(X0) ) ).
cnf(u7402,negated_conjecture,
( ~ c4_2(X0,a747)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| c6_2(X0,a747)
| c3_2(X0,a747)
| c5_2(X0,a744) ) ).
cnf(u3945,negated_conjecture,
( c3_2(X0,a636)
| ~ c6_1(X0)
| ~ sP43(X0)
| ~ c2_1(X0)
| c5_2(X0,a636)
| ~ c8_1(X0)
| c5_2(X0,a747) ) ).
cnf(u8410,negated_conjecture,
( ~ c6_2(X0,a676)
| c3_2(X0,a713)
| c2_1(X0)
| c5_2(X0,a713)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP18(X0)
| ~ c9_2(X0,a748)
| c8_1(X0)
| ~ c6_1(X0)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u4553,negated_conjecture,
( ~ c9_2(X0,a716)
| c4_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a636)
| ~ sP17(X0)
| ~ c6_1(X0)
| c2_1(X0)
| ~ sP43(X0) ) ).
cnf(u4700,negated_conjecture,
( c1_2(X0,a677)
| ~ sP30(X0)
| ~ c9_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| c4_2(X0,a677)
| c6_2(X0,a677)
| c5_1(X0) ) ).
cnf(u4550,negated_conjecture,
( ~ c9_2(X0,a716)
| c4_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a636)
| ~ sP17(X0)
| ~ c3_1(X0)
| ~ c8_1(X0)
| ~ sP43(X0)
| c6_2(X0,a716) ) ).
cnf(u4954,negated_conjecture,
( c1_2(X0,a662)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c8_1(X0)
| c3_2(X0,a714)
| ~ c9_1(X0)
| ~ c10_1(X0)
| c2_1(X0) ) ).
cnf(u353,axiom,
( c2_2(X0,a719)
| ~ sP14(X0) ) ).
cnf(u5483,negated_conjecture,
( ~ c5_2(X0,a714)
| c5_2(X0,a744)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c2_1(X0)
| c8_2(X0,a747)
| c6_2(X0,a747) ) ).
cnf(u340,axiom,
( ~ c6_2(X0,a713)
| ~ sP18(X0) ) ).
cnf(u5470,negated_conjecture,
( c6_2(X0,a747)
| c6_2(X0,X1)
| c4_2(X0,a747)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c6_1(X0)
| c4_2(X0,X1)
| ~ c8_1(X0) ) ).
cnf(u6233,negated_conjecture,
( c9_2(X0,a636)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c2_2(X0,a751)
| c7_1(X0)
| c4_2(X0,a684) ) ).
cnf(u4828,negated_conjecture,
( ~ c8_2(X0,X1)
| c4_2(X0,a684)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c8_1(X0)
| sP27(X0)
| ~ c9_2(X0,a684)
| ~ c3_2(X0,a684)
| c10_1(X0)
| ~ sP43(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u5077,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP30(X0)
| ~ c8_1(X0)
| ~ c1_1(X0)
| c4_2(X0,a677)
| ~ c6_1(X0)
| c1_2(X0,a747)
| c5_2(X0,a712)
| c3_2(X0,a712)
| ~ c2_1(X0)
| sP18(X0) ) ).
cnf(u7992,negated_conjecture,
( ~ c3_2(X0,a636)
| ~ sP43(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c1_1(X0)
| c10_1(X0)
| c4_2(X0,a684)
| c3_2(X0,a751)
| c7_1(X0) ) ).
cnf(u4711,negated_conjecture,
( c1_2(X0,a712)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a712)
| ~ sP43(X0) ) ).
cnf(u5857,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c6_1(X0)
| c3_2(X0,a713)
| c2_1(X0)
| c5_2(X0,a713)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP18(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c8_1(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u6491,negated_conjecture,
( ~ c8_2(X0,a714)
| c8_2(X0,a747)
| c6_2(X0,a747)
| c5_2(X0,a712)
| ~ c6_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c1_2(X0,a714) ) ).
cnf(u8357,negated_conjecture,
( c3_2(X0,a751)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| ~ c6_1(X0)
| c7_1(X0)
| c1_1(X0)
| ~ c8_1(X0)
| c5_2(X0,a636) ) ).
cnf(u4968,negated_conjecture,
( c6_2(X0,a636)
| c4_2(X0,a676)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP31(X0)
| c2_2(X0,a676)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u7286,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747)
| ~ sP43(X0)
| c5_2(X0,a636) ) ).
cnf(u4567,negated_conjecture,
( c3_2(X0,X1)
| c5_2(X0,X1)
| c8_1(X0)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748) ) ).
cnf(u7406,negated_conjecture,
( ~ c6_2(X0,a675)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c9_2(X0,a747)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u203,axiom,
( ~ sP43(X0)
| ndr1_1(X0) ) ).
cnf(u4866,negated_conjecture,
( ~ c8_2(X0,a747)
| ~ c8_1(X0)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c2_1(X0)
| c1_2(X0,a747) ) ).
cnf(u3936,negated_conjecture,
( ~ c9_2(X0,a636)
| ~ c3_1(X0)
| ~ c8_1(X0)
| ~ sP43(X0)
| c6_2(X0,a636) ) ).
cnf(u4719,negated_conjecture,
( c6_2(X0,a636)
| c1_1(X0)
| ~ sP43(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| c2_2(X0,a712)
| c5_2(X0,a712)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u5107,negated_conjecture,
( ~ c9_2(X0,a748)
| c3_2(X0,a750)
| c8_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a748)
| ~ sP3(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c6_1(X0)
| c10_2(X0,X1)
| c2_1(X0)
| c5_2(X0,a750) ) ).
cnf(u6179,negated_conjecture,
( ~ c9_2(X0,a662)
| c4_2(X0,a684)
| sP18(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c3_2(X0,a662)
| c10_1(X0)
| ~ sP36(X0)
| c1_1(X0)
| ~ c3_2(X0,a712) ) ).
cnf(u5765,negated_conjecture,
( ~ c3_2(X0,a676)
| c1_1(X0)
| ~ sP31(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| c2_2(X0,a676)
| ~ c9_1(X0)
| c3_1(X0)
| c4_2(X0,a676) ) ).
cnf(u7159,negated_conjecture,
( c6_2(X0,a636)
| c1_1(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| c10_1(X0)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747) ) ).
cnf(u4609,negated_conjecture,
( ~ c1_2(X0,X1)
| c3_2(X0,a748)
| c1_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a743)
| c3_2(X0,a743)
| c8_1(X0)
| sP5(X0)
| c6_2(X0,X1)
| ~ c3_2(X0,X1)
| c10_1(X0) ) ).
cnf(u5345,negated_conjecture,
( c10_2(X0,a748)
| c8_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a744)
| c2_1(X0)
| c5_2(X0,a744)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP5(X0) ) ).
cnf(u271,axiom,
( c2_2(X0,a677)
| ~ sP30(X0) ) ).
cnf(u8435,negated_conjecture,
( ~ c6_2(X0,a675)
| c3_2(X0,a744)
| c2_1(X0)
| c5_2(X0,a744)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP5(X0)
| ~ c9_2(X0,a748)
| c8_1(X0)
| ~ c6_1(X0)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u6458,negated_conjecture,
( c10_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a743)
| c3_2(X0,a743)
| c8_1(X0)
| sP5(X0)
| c6_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| c3_2(X0,a748)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0) ) ).
cnf(u3854,negated_conjecture,
( ~ c1_2(X0,X1)
| ~ c8_1(X0)
| c4_2(X0,a747)
| c6_2(X0,a747)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c6_1(X0) ) ).
cnf(u4492,negated_conjecture,
( c8_2(X0,a662)
| c2_1(X0)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c8_1(X0)
| c3_2(X0,a714)
| ~ c9_1(X0) ) ).
cnf(u3707,negated_conjecture,
( c10_2(X0,a748)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| c10_1(X0)
| c3_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a748)
| c8_1(X0) ) ).
cnf(u269,axiom,
( ~ c5_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u399,axiom,
( c8_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u7917,negated_conjecture,
( ~ c9_2(X0,a684)
| c6_2(X0,a636)
| ~ c8_1(X0)
| sP27(X0)
| c1_1(X0)
| ~ c3_2(X0,a684)
| ~ sP43(X0)
| c4_2(X0,a684)
| ~ c3_2(X0,a676)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| c5_2(X0,a744)
| c5_2(X0,a747) ) ).
cnf(u4850,negated_conjecture,
( c6_2(X0,a676)
| c4_2(X0,a676)
| c1_1(X0)
| ~ sP31(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| c2_2(X0,a676)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u6183,negated_conjecture,
( c3_2(X0,a751)
| c4_2(X0,a684)
| sP18(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c7_1(X0)
| c1_1(X0) ) ).
cnf(u3837,negated_conjecture,
( ~ c8_2(X0,a747)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a712)
| c1_2(X0,a747) ) ).
cnf(u7439,negated_conjecture,
( ~ c9_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a747)
| c10_1(X0)
| ~ c3_2(X0,a748)
| c3_2(X0,X1)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u3818,negated_conjecture,
( c10_2(X0,a748)
| c10_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| c3_2(X0,X1)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0) ) ).
cnf(u4254,negated_conjecture,
( ~ c9_2(X0,a662)
| ~ sP36(X0)
| c2_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c4_2(X0,a662)
| ~ c1_1(X0)
| c5_1(X0) ) ).
cnf(u4895,negated_conjecture,
( c6_2(X0,a712)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| c1_1(X0)
| ~ c6_1(X0)
| sP18(X0)
| c2_2(X0,a676)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u3824,negated_conjecture,
( c1_2(X0,a748)
| c1_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| c3_2(X0,a748)
| c3_2(X0,X1) ) ).
cnf(u5140,negated_conjecture,
( ~ c9_2(X0,a684)
| c4_2(X0,a684)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ c8_1(X0)
| sP27(X0)
| ~ c6_1(X0)
| c2_1(X0)
| ~ sP31(X0) ) ).
cnf(u5006,negated_conjecture,
( ~ c9_2(X0,a685)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_1(X0)
| c10_1(X0)
| ~ sP27(X0)
| c4_2(X0,a744)
| ~ c3_2(X0,a636) ) ).
cnf(u8597,negated_conjecture,
( c6_2(X0,a747)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| ~ c10_1(X0)
| ~ c8_1(X0)
| c5_2(X0,a712)
| ~ sP31(X0)
| sP18(X0) ) ).
cnf(u410,axiom,
( ~ sP3(X0)
| ndr1_1(X0) ) ).
cnf(u7951,negated_conjecture,
( ~ c3_2(X0,a744)
| ~ sP43(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c2_2(X0,a751)
| c7_1(X0)
| c4_2(X0,a684)
| ~ c3_2(X0,a636)
| c10_1(X0)
| c1_1(X0)
| ~ sP5(X0) ) ).
cnf(u5898,negated_conjecture,
( ~ c3_2(X0,a662)
| c8_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0)
| sP5(X0)
| c3_2(X0,a743)
| c5_2(X0,a743)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c10_1(X0)
| c4_2(X0,a662)
| c5_1(X0) ) ).
cnf(u3857,negated_conjecture,
( ~ c9_2(X0,a743)
| ~ c8_1(X0)
| c4_2(X0,X1)
| c6_2(X0,X1)
| ~ c1_1(X0)
| c5_1(X0)
| sP5(X0)
| ~ c6_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u5148,negated_conjecture,
( c10_2(X0,a748)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,a713)
| c3_2(X0,a713)
| c8_1(X0)
| ~ sP18(X0)
| c3_2(X0,a748)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u4499,negated_conjecture,
( ~ c9_2(X0,a685)
| c10_1(X0)
| ~ sP27(X0)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u5662,negated_conjecture,
( c3_2(X0,a751)
| sP18(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c2_2(X0,a712)
| c5_2(X0,a712)
| ~ c9_1(X0)
| c2_1(X0)
| c7_1(X0)
| c1_1(X0) ) ).
cnf(u6674,negated_conjecture,
( ~ c9_2(X0,a662)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| c2_2(X0,a712)
| c5_2(X0,a712)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c3_2(X0,a662)
| ~ sP36(X0)
| c1_1(X0)
| ~ c3_2(X0,a676) ) ).
cnf(u6278,negated_conjecture,
( ~ c4_2(X0,a747)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| c6_2(X0,a747)
| c3_2(X0,a747)
| ~ c8_1(X0) ) ).
cnf(u4749,negated_conjecture,
( ~ c2_2(X0,a747)
| c3_2(X0,a636)
| ~ sP43(X0)
| ~ c2_1(X0)
| c5_2(X0,a636)
| ~ c5_1(X0)
| ~ c5_2(X0,a684)
| c10_1(X0)
| c4_2(X0,a684)
| ~ c8_1(X0)
| c1_2(X0,a747)
| sP27(X0) ) ).
cnf(u8225,negated_conjecture,
( ~ c3_2(X0,a744)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c2_2(X0,a751)
| c7_1(X0)
| c1_1(X0)
| ~ c3_2(X0,a636)
| ~ c8_1(X0) ) ).
cnf(u3201,negated_conjecture,
( c1_2(X0,a712)
| ~ c6_1(X0)
| ~ ndr1_1(X0)
| ~ c8_1(X0)
| sP18(X0) ) ).
cnf(u286,axiom,
( ~ c4_2(X0,a683)
| ~ sP28(X0) ) ).
cnf(u408,axiom,
( ~ c8_2(X0,a750)
| ~ sP3(X0) ) ).
cnf(u3746,negated_conjecture,
( c1_2(X0,a712)
| c6_2(X0,a712)
| sP18(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a712)
| c1_1(X0) ) ).
cnf(u7803,negated_conjecture,
( ~ c3_2(X0,a744)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c6_2(X0,a636)
| c1_1(X0)
| ~ sP43(X0)
| ~ c3_2(X0,a676) ) ).
cnf(u3705,negated_conjecture,
( c10_2(X0,a684)
| c4_2(X0,a684)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c8_1(X0)
| sP27(X0) ) ).
cnf(u5936,negated_conjecture,
( ~ c9_2(X0,a662)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c8_1(X0)
| c3_2(X0,a714)
| ~ c9_1(X0)
| c2_1(X0)
| c4_2(X0,a662)
| ~ c6_1(X0) ) ).
cnf(u4494,negated_conjecture,
( ~ c6_2(X0,a636)
| c10_1(X0)
| ~ sP27(X0)
| ~ c9_2(X0,a685)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u3999,negated_conjecture,
( c7_2(X0,a662)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP36(X0) ) ).
cnf(u6060,negated_conjecture,
( ~ c9_2(X0,a662)
| ~ sP43(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| c2_2(X0,a712)
| c5_2(X0,a712)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c3_2(X0,a662)
| c10_1(X0)
| ~ sP36(X0)
| c1_1(X0)
| ~ c3_2(X0,a636) ) ).
cnf(u5938,negated_conjecture,
( ~ c9_2(X0,a743)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c8_1(X0)
| c3_2(X0,a714)
| ~ c9_1(X0)
| c2_1(X0)
| c4_2(X0,a662)
| sP5(X0)
| ~ c6_1(X0)
| ~ c3_2(X0,a662) ) ).
cnf(u3126,negated_conjecture,
( ~ c10_1(X96)
| ndr1_1(X96) ) ).
cnf(u4789,negated_conjecture,
( ~ c8_2(X0,a714)
| c8_2(X0,a677)
| c6_2(X0,a677)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP30(X0)
| ~ c9_1(X0)
| ~ c8_1(X0)
| ~ c10_1(X0)
| c1_2(X0,a714) ) ).
cnf(u7844,negated_conjecture,
( ~ c9_2(X0,a748)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a748)
| c5_2(X0,X1)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ c6_1(X0)
| c3_2(X0,X1) ) ).
cnf(u4864,negated_conjecture,
( c7_2(X0,a714)
| ~ c8_1(X0)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c2_1(X0)
| c8_2(X0,a747)
| c6_2(X0,a747) ) ).
cnf(u7210,negated_conjecture,
( ~ c9_2(X0,a685)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| c10_1(X0)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| ~ sP27(X0)
| c1_1(X0)
| ~ c3_2(X0,a636) ) ).
cnf(u5801,negated_conjecture,
( ~ c9_2(X0,a685)
| c1_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_1(X0)
| ~ sP27(X0)
| c4_2(X0,a744)
| ~ c3_2(X0,a676) ) ).
cnf(u7237,negated_conjecture,
( ~ c6_2(X0,a675)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c8_1(X0)
| sP27(X0)
| ~ c9_2(X0,a684)
| ~ c3_2(X0,a684)
| c10_1(X0)
| ~ sP43(X0)
| c4_2(X0,a684)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u7231,negated_conjecture,
( ~ c9_2(X0,a684)
| c6_2(X0,a712)
| sP18(X0)
| ~ c8_1(X0)
| sP27(X0)
| c1_1(X0)
| ~ c3_2(X0,a684)
| c10_1(X0)
| c4_2(X0,a684)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u6066,negated_conjecture,
( ~ c3_2(X0,a636)
| ~ sP43(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| c2_2(X0,a712)
| c5_2(X0,a712)
| ~ c9_1(X0)
| c3_1(X0)
| c5_2(X0,a636)
| c1_1(X0) ) ).
cnf(u7215,negated_conjecture,
( ~ c6_2(X0,a636)
| c6_2(X0,a712)
| sP18(X0)
| ~ c8_1(X0)
| sP27(X0)
| ~ c9_2(X0,a684)
| ~ c3_2(X0,a684)
| c10_1(X0)
| c4_2(X0,a684)
| c1_1(X0)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u3254,negated_conjecture,
( ~ c8_2(X69,X70)
| ~ c3_2(X69,X70)
| c5_2(X69,X70)
| ~ c10_1(X69)
| ~ c8_1(X69) ) ).
cnf(u3913,negated_conjecture,
( ~ c6_2(X0,a636)
| c3_2(X0,a751)
| c7_1(X0)
| c9_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u5550,negated_conjecture,
( c10_2(X0,a748)
| c3_2(X0,X1)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a748)
| c5_2(X0,X1)
| c8_1(X0)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0) ) ).
cnf(u4543,negated_conjecture,
( c10_2(X0,a712)
| ~ sP31(X0)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0) ) ).
cnf(u5889,negated_conjecture,
( ~ c3_2(X0,a677)
| c8_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0)
| sP5(X0)
| c6_2(X0,a677)
| c3_2(X0,a743)
| c5_2(X0,a743)
| ~ sP30(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| c4_2(X0,a677)
| c5_1(X0) ) ).
cnf(u5947,negated_conjecture,
( ~ c9_2(X0,a748)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| c3_2(X0,X1)
| ~ c3_2(X0,a748)
| c1_2(X0,X1)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u6939,negated_conjecture,
( ~ c6_2(X0,a636)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ sP17(X0)
| ~ c9_2(X0,a716)
| c10_1(X0)
| ~ sP31(X0)
| c4_2(X0,a716)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u4913,negated_conjecture,
( c6_2(X0,a712)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ c8_1(X0)
| c1_1(X0)
| ~ c6_1(X0)
| sP18(X0)
| c2_1(X0) ) ).
cnf(u5700,negated_conjecture,
( ~ c9_2(X0,a743)
| ~ c9_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| c4_2(X0,a677)
| c6_2(X0,a677)
| c5_1(X0)
| sP5(X0)
| ~ sP30(X0)
| ~ c3_2(X0,a677) ) ).
cnf(u4806,negated_conjecture,
( c1_2(X0,a677)
| ~ c8_1(X0)
| c6_2(X0,a677)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP30(X0)
| c3_2(X0,a714)
| c4_2(X0,a677) ) ).
cnf(u6833,negated_conjecture,
( c4_2(X0,a684)
| c1_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c2_2(X0,a751)
| c7_1(X0) ) ).
cnf(u7427,negated_conjecture,
( ~ c6_2(X0,a676)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a747)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u8822,negated_conjecture,
( c6_2(X0,a747)
| c5_2(X0,a712)
| ~ c6_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a714)
| c5_2(X0,a684)
| c3_2(X0,a684)
| ~ c8_1(X0)
| sP27(X0) ) ).
cnf(u7252,negated_conjecture,
( ~ c6_2(X0,a676)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c8_1(X0)
| sP27(X0)
| ~ c9_2(X0,a684)
| ~ c3_2(X0,a684)
| ~ sP43(X0)
| c4_2(X0,a684)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u4566,negated_conjecture,
( ~ c1_2(X0,a748)
| c5_2(X0,X1)
| c8_1(X0)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c6_1(X0)
| c3_2(X0,X1)
| ~ c9_2(X0,a748) ) ).
cnf(u3144,negated_conjecture,
c9_1(a655) ).
cnf(u343,axiom,
( c3_2(X0,a716)
| ~ sP17(X0) ) ).
cnf(u7486,negated_conjecture,
( c6_2(X0,a676)
| c1_1(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| c10_1(X0)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747) ) ).
cnf(u8678,negated_conjecture,
( ~ c3_2(X0,a636)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| c4_2(X0,a744)
| ~ c6_1(X0)
| ~ sP5(X0)
| ~ c8_1(X0)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747) ) ).
cnf(u3916,negated_conjecture,
( ~ c1_2(X0,X1)
| c10_2(X0,X1)
| ~ sP43(X0)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a636) ) ).
cnf(u5059,negated_conjecture,
( c1_2(X0,a748)
| c3_2(X0,X1)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a747)
| c3_2(X0,a748)
| c10_1(X0) ) ).
cnf(u7118,negated_conjecture,
( ~ c6_2(X0,a676)
| c4_2(X0,a744)
| ~ c8_1(X0)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c3_2(X0,a744)
| ~ c6_1(X0)
| ~ sP5(X0)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u5845,negated_conjecture,
( c1_2(X0,a748)
| c3_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a743)
| c3_2(X0,a743)
| c8_1(X0)
| sP5(X0)
| c6_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0) ) ).
cnf(u5072,negated_conjecture,
( ~ c2_2(X0,a744)
| ~ sP30(X0)
| ~ c8_1(X0)
| ~ c1_1(X0)
| c4_2(X0,a677)
| ~ c6_1(X0)
| c1_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u4577,negated_conjecture,
( c6_2(X0,a716)
| ~ c10_1(X0)
| ~ c8_1(X0)
| c4_2(X0,a716)
| c5_2(X0,a716)
| ~ c1_1(X0)
| c5_1(X0)
| ~ sP17(X0) ) ).
cnf(u3529,negated_conjecture,
( c3_2(X0,a712)
| c5_2(X0,a712)
| ~ c2_1(X0)
| c5_2(X0,a747)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0) ) ).
cnf(u6478,negated_conjecture,
( ~ c9_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a743)
| c3_2(X0,a743)
| c8_1(X0)
| sP5(X0)
| c6_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c6_1(X0)
| c10_2(X0,X1)
| c2_1(X0)
| c3_2(X0,a748) ) ).
cnf(u341,axiom,
( ~ sP18(X0)
| ndr1_1(X0) ) ).
cnf(u6600,negated_conjecture,
( c1_2(X0,a747)
| ~ c8_1(X0)
| c6_2(X0,a747)
| c5_2(X0,a712)
| ~ c6_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a714) ) ).
cnf(u5074,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP30(X0)
| ~ c8_1(X0)
| ~ c1_1(X0)
| c4_2(X0,a677)
| ~ c6_1(X0)
| c1_2(X0,a747)
| ~ sP43(X0)
| ~ c2_1(X0)
| c5_2(X0,a636)
| c3_2(X0,a636) ) ).
cnf(u5985,negated_conjecture,
( ~ c6_2(X0,a712)
| c8_1(X0)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c10_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ c3_2(X0,a712)
| sP18(X0) ) ).
cnf(u6496,negated_conjecture,
( c3_2(X0,a743)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0)
| sP5(X0)
| c8_1(X0)
| c5_2(X0,a743)
| ~ sP17(X0)
| c3_1(X0)
| c10_1(X0)
| c5_2(X0,a716) ) ).
cnf(u6329,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c6_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a662)
| c3_2(X0,a662)
| ~ c8_1(X0)
| ~ sP36(X0)
| ~ sP28(X0)
| c4_2(X0,a662)
| c1_2(X0,a747) ) ).
cnf(u7510,negated_conjecture,
( ~ c1_2(X0,X1)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| c6_2(X0,a747)
| c5_2(X0,a744)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c8_1(X0) ) ).
cnf(u6095,negated_conjecture,
( ~ c9_2(X0,a685)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP31(X0)
| c2_2(X0,a676)
| ~ c9_1(X0)
| c2_1(X0)
| c10_1(X0)
| ~ sP27(X0)
| c4_2(X0,a676)
| ~ c3_2(X0,a636) ) ).
cnf(u4817,negated_conjecture,
( c4_2(X0,a676)
| ~ sP31(X0)
| ~ c6_1(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| c5_2(X0,a747)
| ~ c10_1(X0) ) ).
cnf(u8059,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c5_2(X0,a744)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747)
| c5_2(X0,a684)
| c3_2(X0,a684)
| sP27(X0) ) ).
cnf(u4206,negated_conjecture,
( ~ c3_2(X0,a744)
| c3_1(X0)
| c10_1(X0)
| c5_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u9036,negated_conjecture,
( ~ c3_2(X0,a636)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c2_2(X0,a751)
| c7_1(X0)
| c1_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0) ) ).
cnf(u5333,negated_conjecture,
( ~ c9_2(X0,a743)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c9_1(X0)
| ~ c10_1(X0)
| c2_1(X0)
| c4_2(X0,a662)
| c5_1(X0)
| sP5(X0)
| ~ c6_1(X0)
| ~ c3_2(X0,a662) ) ).
cnf(u354,axiom,
( ~ c4_2(X0,a719)
| ~ sP14(X0) ) ).
cnf(u3553,negated_conjecture,
( ~ c9_2(X0,a743)
| sP5(X0)
| ~ c3_2(X0,a712)
| c6_2(X0,a712)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0) ) ).
cnf(u7404,negated_conjecture,
( ~ c6_2(X0,a636)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c9_2(X0,a747)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u3173,negated_conjecture,
( c6_2(X0,a718)
| c4_2(X0,a718)
| ~ c1_1(X0)
| c5_1(X0)
| sP14(X0)
| ~ c10_1(X0) ) ).
cnf(u4956,negated_conjecture,
( ~ c4_2(X0,a662)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c8_1(X0)
| c3_2(X0,a714)
| ~ c9_1(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| c3_2(X0,a662)
| c2_1(X0) ) ).
cnf(u7117,negated_conjecture,
( ~ c3_2(X0,a744)
| c4_2(X0,a744)
| ~ c8_1(X0)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ sP5(X0)
| c10_1(X0)
| ~ c6_1(X0) ) ).
cnf(u4729,negated_conjecture,
( c5_2(X0,a747)
| ~ sP43(X0)
| ~ c2_1(X0)
| c5_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0) ) ).
cnf(u4982,negated_conjecture,
( c4_2(X0,a744)
| ~ sP5(X0)
| ~ c8_1(X0)
| c1_1(X0)
| ~ c6_1(X0)
| sP18(X0)
| c2_1(X0)
| c7_1(X0)
| c2_2(X0,a751) ) ).
cnf(u7805,negated_conjecture,
( ~ c9_2(X0,a716)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c6_2(X0,a636)
| ~ sP17(X0)
| c1_1(X0)
| ~ sP43(X0)
| c4_2(X0,a716)
| ~ c3_2(X0,a676) ) ).
cnf(u4863,negated_conjecture,
( ~ c5_2(X0,a714)
| ~ c8_1(X0)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c2_1(X0)
| c8_2(X0,a747)
| c6_2(X0,a747) ) ).
cnf(u5897,negated_conjecture,
( c6_2(X0,a716)
| c8_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0)
| sP5(X0)
| c3_2(X0,a743)
| c5_2(X0,a743)
| ~ sP17(X0) ) ).
cnf(u5084,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ c2_1(X0)
| c5_2(X0,a744)
| c3_2(X0,a744)
| ~ c8_1(X0)
| ~ c1_1(X0)
| ~ sP28(X0)
| ~ c6_1(X0)
| c1_2(X0,a747) ) ).
cnf(u4451,negated_conjecture,
( c1_2(X0,a748)
| c5_2(X0,a750)
| c3_2(X0,a750)
| c8_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a748)
| ~ sP3(X0) ) ).
cnf(u4865,negated_conjecture,
( c8_2(X0,a747)
| ~ c8_1(X0)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| c6_2(X0,a747) ) ).
cnf(u7147,negated_conjecture,
( ~ c3_2(X0,a744)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| c10_1(X0)
| ~ sP43(X0) ) ).
cnf(u8433,negated_conjecture,
( ~ c6_2(X0,a712)
| c3_2(X0,a744)
| c2_1(X0)
| c5_2(X0,a744)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP5(X0)
| ~ c9_2(X0,a748)
| c8_1(X0)
| ~ c6_1(X0)
| ~ c3_2(X0,a712)
| sP18(X0) ) ).
cnf(u8411,negated_conjecture,
( ~ c6_2(X0,a675)
| c3_2(X0,a713)
| c2_1(X0)
| c5_2(X0,a713)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP18(X0)
| ~ c9_2(X0,a748)
| c8_1(X0)
| ~ c6_1(X0)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u3808,negated_conjecture,
( c6_2(X0,a712)
| c1_1(X0)
| c4_2(X0,a684)
| sP18(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u8436,negated_conjecture,
( ~ c6_2(X0,a636)
| c3_2(X0,a744)
| c2_1(X0)
| c5_2(X0,a744)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP5(X0)
| ~ c9_2(X0,a748)
| c8_1(X0)
| ~ c6_1(X0)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u7662,negated_conjecture,
( ~ c9_2(X0,a748)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a748)
| c5_2(X0,X1)
| c8_1(X0)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c6_1(X0)
| c3_2(X0,X1) ) ).
cnf(u4378,negated_conjecture,
( ~ c5_2(X0,a714)
| ~ c8_1(X0)
| c8_2(X0,a747)
| c6_2(X0,a747)
| c5_2(X0,a712)
| ~ c6_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u4592,negated_conjecture,
( ~ c9_2(X0,a748)
| c3_2(X0,X1)
| c8_1(X0)
| ~ c6_1(X0)
| c10_2(X0,X1)
| c2_1(X0)
| c5_2(X0,X1)
| c10_1(X0)
| c3_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a748) ) ).
cnf(u5375,negated_conjecture,
( ~ c9_2(X0,a748)
| c8_1(X0)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c6_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| c1_2(X0,X2)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X2)
| c3_2(X0,a748)
| c3_2(X0,X2) ) ).
cnf(u7809,negated_conjecture,
( ~ c9_2(X0,a685)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| ~ sP27(X0)
| c1_1(X0)
| ~ c3_2(X0,a676) ) ).
cnf(u4236,negated_conjecture,
( ~ c2_2(X0,a744)
| ~ c5_2(X0,a684)
| ~ sP5(X0)
| c4_2(X0,a684)
| ~ c8_1(X0)
| c1_2(X0,a744)
| sP27(X0) ) ).
cnf(u5139,negated_conjecture,
( ~ c8_2(X0,X1)
| c4_2(X0,a684)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ c8_1(X0)
| sP27(X0)
| ~ c9_2(X0,a684)
| ~ c3_2(X0,a684)
| c10_1(X0)
| ~ sP31(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u8837,negated_conjecture,
( c6_2(X0,a747)
| c5_2(X0,a712)
| ~ c6_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a714)
| c5_2(X0,a744)
| ~ c8_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744) ) ).
cnf(u4093,negated_conjecture,
( c2_2(X0,a685)
| ~ sP27(X0)
| c5_2(X0,a685)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u5138,negated_conjecture,
( c6_2(X0,a676)
| c4_2(X0,a684)
| c1_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u9251,negated_conjecture,
( c6_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c4_2(X0,a676)
| c1_1(X0)
| ~ sP43(X0) ) ).
cnf(u5910,negated_conjecture,
( c3_2(X0,a744)
| ~ c6_1(X0)
| c8_1(X0)
| c2_1(X0)
| c5_2(X0,a744)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP5(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0) ) ).
cnf(u4506,negated_conjecture,
( ~ c6_2(X0,a636)
| ~ c3_2(X0,a636)
| c10_1(X0)
| ~ sP43(X0)
| ~ c9_2(X0,a636) ) ).
cnf(u3855,negated_conjecture,
( c6_2(X0,X1)
| ~ c8_1(X0)
| c4_2(X0,X1)
| ~ c6_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c9_2(X0,a747) ) ).
cnf(u288,axiom,
( ~ sP28(X0)
| ndr1_1(X0) ) ).
cnf(u6548,negated_conjecture,
( ~ c9_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| c4_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u9350,negated_conjecture,
( c3_2(X0,a751)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c4_2(X0,a676)
| sP18(X0)
| c1_1(X0)
| c7_1(X0)
| ~ c8_1(X0) ) ).
cnf(u270,axiom,
( ~ sP31(X0)
| ndr1_1(X0) ) ).
cnf(u9216,negated_conjecture,
( c6_2(X0,a747)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| ~ sP5(X0)
| c5_2(X0,a744)
| c5_2(X0,a684)
| c3_2(X0,a684)
| ~ c8_1(X0)
| sP27(X0) ) ).
cnf(u8046,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c5_2(X0,a744)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747)
| c4_2(X0,a662)
| c5_1(X0)
| c5_2(X0,a662)
| c3_2(X0,a662)
| ~ sP36(X0) ) ).
cnf(u4504,negated_conjecture,
( ~ c6_2(X0,a712)
| ~ c3_2(X0,a636)
| c10_1(X0)
| ~ sP43(X0)
| ~ c9_2(X0,a636)
| ~ c3_2(X0,a712)
| sP18(X0) ) ).
cnf(u5399,negated_conjecture,
( c10_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0)
| c3_2(X0,X1)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u5521,negated_conjecture,
( c3_2(X0,a662)
| c4_2(X0,a662)
| ~ c6_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a662)
| ~ c8_1(X0)
| c5_2(X0,a747)
| ~ sP36(X0) ) ).
cnf(u5168,negated_conjecture,
( ~ c8_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ sP17(X0)
| ~ c9_2(X0,a716)
| c10_1(X0)
| c4_2(X0,a716)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u5671,negated_conjecture,
( ~ c6_2(X0,a675)
| c3_2(X0,a750)
| c8_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c10_1(X0)
| ~ sP3(X0)
| c5_2(X0,a750)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u4660,negated_conjecture,
( ~ c9_2(X0,X1)
| c3_2(X0,X1)
| c8_1(X0)
| ~ c6_1(X0)
| c10_2(X0,a748)
| c2_1(X0)
| c5_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0) ) ).
cnf(u6234,negated_conjecture,
( c9_2(X0,a636)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c3_2(X0,a751)
| c7_1(X0)
| c4_2(X0,a684) ) ).
cnf(u4510,negated_conjecture,
( ~ c6_2(X0,a636)
| ~ c3_2(X0,a662)
| c10_1(X0)
| ~ sP36(X0)
| ~ c9_2(X0,a662)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u4512,negated_conjecture,
( ~ c6_2(X0,a676)
| ~ c3_2(X0,a662)
| c10_1(X0)
| ~ sP36(X0)
| ~ c9_2(X0,a662)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u3218,negated_conjecture,
( c10_2(X0,a748)
| ~ ndr1_1(X0)
| c5_2(X0,a748)
| c3_2(X0,a748)
| c8_1(X0) ) ).
cnf(u409,axiom,
( c2_2(X0,a750)
| ~ sP3(X0) ) ).
cnf(u5676,negated_conjecture,
( ~ c9_2(X0,a748)
| c3_2(X0,a750)
| c8_1(X0)
| c5_2(X0,a750)
| ~ c3_2(X0,a748)
| c10_1(X0)
| ~ sP3(X0)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u6461,negated_conjecture,
( c10_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a743)
| c3_2(X0,a743)
| c8_1(X0)
| sP5(X0)
| c6_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| c3_2(X0,a748)
| ~ sP31(X0)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676) ) ).
cnf(u8598,negated_conjecture,
( c6_2(X0,a747)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| ~ c10_1(X0)
| ~ c8_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676) ) ).
cnf(u4909,negated_conjecture,
( c6_2(X0,a712)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ c8_1(X0)
| c1_1(X0)
| ~ c6_1(X0)
| sP18(X0)
| c2_2(X0,a744)
| c5_2(X0,a744)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u4525,negated_conjecture,
( ~ c9_2(X0,a716)
| c4_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c6_1(X0)
| c2_1(X0)
| ~ sP17(X0) ) ).
cnf(u3241,negated_conjecture,
( c9_2(X0,a747)
| ~ ndr1_1(X0)
| c5_2(X0,a712)
| c3_2(X0,a712)
| ~ c2_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0) ) ).
cnf(u4388,negated_conjecture,
( c7_2(X0,a714)
| ~ c8_1(X0)
| c8_2(X0,a747)
| c6_2(X0,a747)
| c5_2(X0,a712)
| ~ c6_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u3231,negated_conjecture,
( c3_2(X0,a748)
| c5_2(X0,a748)
| ~ ndr1_1(X0)
| c8_1(X0)
| c2_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u8376,negated_conjecture,
( c4_2(X0,a744)
| ~ sP5(X0)
| ~ c6_1(X0)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c2_2(X0,a751)
| c7_1(X0)
| c1_1(X0)
| ~ c8_1(X0)
| c5_2(X0,a636) ) ).
cnf(u6240,negated_conjecture,
( ~ c3_2(X0,a636)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c3_1(X0)
| c5_2(X0,a636)
| c4_2(X0,a684) ) ).
cnf(u7208,negated_conjecture,
( ~ c9_2(X0,a662)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| c10_1(X0)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| ~ c3_2(X0,a662)
| ~ sP36(X0)
| c1_1(X0)
| ~ c3_2(X0,a636) ) ).
cnf(u4407,negated_conjecture,
( ~ c9_2(X0,a743)
| ~ c6_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| sP5(X0)
| ~ c8_1(X0)
| ~ c3_2(X0,a676)
| c6_2(X0,a676) ) ).
cnf(u8595,negated_conjecture,
( c6_2(X0,a747)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| ~ c10_1(X0)
| ~ c8_1(X0)
| c5_2(X0,a636)
| ~ sP31(X0)
| ~ sP43(X0) ) ).
cnf(u4805,negated_conjecture,
( c1_2(X0,a677)
| ~ c8_1(X0)
| c6_2(X0,a677)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP30(X0)
| ~ c9_1(X0)
| ~ c10_1(X0)
| c3_2(X0,a714) ) ).
cnf(u4469,negated_conjecture,
( c10_2(X0,a748)
| ~ sP43(X0)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a636)
| c10_1(X0)
| c3_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a748)
| c8_1(X0) ) ).
cnf(u6835,negated_conjecture,
( ~ c9_2(X0,a662)
| c1_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c3_2(X0,a662)
| ~ sP36(X0)
| c4_2(X0,a684)
| ~ c3_2(X0,a676) ) ).
cnf(u4535,negated_conjecture,
( c10_2(X0,a716)
| ~ sP31(X0)
| c4_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ sP17(X0) ) ).
cnf(u3513,negated_conjecture,
( c1_2(X0,a748)
| c10_1(X0)
| c3_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a748)
| c8_1(X0) ) ).
cnf(u3256,negated_conjecture,
ndr1_1(X61) ).
cnf(u7251,negated_conjecture,
( ~ c9_2(X0,a684)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c8_1(X0)
| sP27(X0)
| c4_2(X0,a684)
| ~ c3_2(X0,a684)
| c10_1(X0)
| ~ sP43(X0)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u7419,negated_conjecture,
( ~ c9_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c9_2(X0,a747)
| c10_1(X0)
| ~ c3_2(X0,a748)
| c3_2(X0,X1)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u4533,negated_conjecture,
( c10_2(X0,a684)
| ~ sP31(X0)
| c4_2(X0,a684)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ c8_1(X0)
| sP27(X0) ) ).
cnf(u3267,negated_conjecture,
c9_1(a690) ).
cnf(u7232,negated_conjecture,
( ~ c6_2(X0,a676)
| c6_2(X0,a712)
| sP18(X0)
| ~ c8_1(X0)
| sP27(X0)
| ~ c9_2(X0,a684)
| ~ c3_2(X0,a684)
| c4_2(X0,a684)
| c1_1(X0)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u4807,negated_conjecture,
( ~ c4_2(X0,a677)
| ~ c8_1(X0)
| c6_2(X0,a677)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP30(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| c3_2(X0,a677)
| c3_2(X0,a714) ) ).
cnf(u7711,negated_conjecture,
( ~ c2_2(X0,a713)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| c5_2(X0,a636)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a713)
| ~ sP18(X0) ) ).
cnf(u5983,negated_conjecture,
( ~ c6_2(X0,a676)
| c8_1(X0)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c10_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u4705,negated_conjecture,
( ~ c6_2(X0,a712)
| c10_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| ~ c3_2(X0,a712)
| c10_2(X0,X1)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c8_1(X0)
| sP18(X0) ) ).
cnf(u4460,negated_conjecture,
( c10_2(X0,a748)
| c10_2(X0,X1)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a636)
| ~ sP43(X0)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0) ) ).
cnf(u7275,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747)
| c4_2(X0,a662)
| c5_1(X0)
| c5_2(X0,a662)
| c3_2(X0,a662)
| ~ sP36(X0) ) ).
cnf(u7800,negated_conjecture,
( c3_2(X0,a751)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| c10_1(X0)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c1_1(X0)
| c7_1(X0) ) ).
cnf(u7645,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c8_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c6_1(X0)
| c4_2(X0,a747)
| c5_2(X0,a712)
| c1_2(X0,a747)
| c5_2(X0,a684)
| c3_2(X0,a684)
| sP27(X0) ) ).
cnf(u3671,negated_conjecture,
( c3_2(X0,a748)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,a748)
| c8_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a747) ) ).
cnf(u338,axiom,
( c9_2(X0,a713)
| ~ sP18(X0) ) ).
cnf(u7698,negated_conjecture,
( ~ c9_2(X0,a684)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ c8_1(X0)
| sP27(X0)
| c1_1(X0)
| ~ c3_2(X0,a684)
| c10_1(X0)
| c4_2(X0,a684)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u4833,negated_conjecture,
( c5_2(X0,a747)
| ~ c6_1(X0)
| ~ c2_1(X0)
| ~ c8_1(X0)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0) ) ).
cnf(u3956,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c9_2(X0,a662)
| ~ c3_2(X0,a662)
| c10_1(X0)
| ~ sP36(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u3954,negated_conjecture,
( ~ c1_2(X0,a662)
| ~ c6_1(X0)
| ~ sP36(X0)
| c2_1(X0)
| ~ c9_2(X0,a662) ) ).
cnf(u3664,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c3_2(X0,a748)
| c10_1(X0)
| ~ c9_2(X0,a748)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1)
| c10_2(X0,X2)
| c5_2(X0,X2)
| c3_2(X0,X2)
| c8_1(X0) ) ).
cnf(u4477,negated_conjecture,
( c10_2(X0,a712)
| ~ sP43(X0)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0) ) ).
cnf(u7128,negated_conjecture,
( c6_2(X0,a712)
| ~ c8_1(X0)
| c1_1(X0)
| c4_2(X0,a744)
| sP18(X0)
| ~ sP5(X0)
| c10_1(X0)
| ~ c6_1(X0)
| c5_2(X0,a744)
| c5_2(X0,a747) ) ).
cnf(u4458,negated_conjecture,
( ~ c8_2(X0,X1)
| c5_2(X0,a750)
| c3_2(X0,a750)
| c8_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c10_1(X0)
| ~ sP3(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u7991,negated_conjecture,
( ~ c3_2(X0,a636)
| ~ sP43(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| c1_1(X0)
| c10_1(X0)
| c4_2(X0,a684)
| c2_2(X0,a751)
| c7_1(X0) ) ).
cnf(u5073,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP30(X0)
| ~ c8_1(X0)
| ~ c1_1(X0)
| c4_2(X0,a677)
| ~ c6_1(X0)
| c1_2(X0,a747)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c2_1(X0)
| c3_2(X0,a676) ) ).
cnf(u355,axiom,
( ~ c7_2(X0,a719)
| ~ sP14(X0) ) ).
cnf(u7807,negated_conjecture,
( ~ c9_2(X0,a662)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| ~ c3_2(X0,a662)
| ~ sP36(X0)
| c1_1(X0)
| ~ c3_2(X0,a676) ) ).
cnf(u378,axiom,
( ~ sP9(X0)
| ndr1_1(X0) ) ).
cnf(u7808,negated_conjecture,
( ~ c9_2(X0,a636)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| ~ c3_2(X0,a636)
| ~ sP43(X0)
| c1_1(X0)
| ~ c3_2(X0,a676) ) ).
cnf(u4467,negated_conjecture,
( c10_2(X0,a716)
| ~ sP43(X0)
| c4_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a636)
| ~ sP17(X0) ) ).
cnf(u4456,negated_conjecture,
( ~ c1_2(X0,a748)
| c5_2(X0,a750)
| c3_2(X0,a750)
| c8_1(X0)
| ~ c6_1(X0)
| ~ sP3(X0)
| c2_1(X0)
| ~ c9_2(X0,a748) ) ).
cnf(u5911,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c6_1(X0)
| c3_2(X0,a744)
| c2_1(X0)
| c5_2(X0,a744)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP5(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c8_1(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u4586,negated_conjecture,
( c4_2(X0,a685)
| ~ c10_1(X0)
| ~ c8_1(X0)
| c5_2(X0,a685)
| ~ c1_1(X0)
| c5_1(X0)
| ~ sP27(X0) ) ).
cnf(u4985,negated_conjecture,
( ~ c3_2(X0,a712)
| c4_2(X0,a744)
| ~ c8_1(X0)
| c1_1(X0)
| ~ c6_1(X0)
| sP18(X0)
| c3_1(X0)
| c5_2(X0,a712)
| ~ sP5(X0) ) ).
cnf(u376,axiom,
( c4_2(X0,a732)
| ~ sP9(X0) ) ).
cnf(u6384,negated_conjecture,
( ~ c9_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a744)
| c3_2(X0,a744)
| c8_1(X0)
| ~ c6_1(X0)
| c2_1(X0)
| c10_1(X0)
| ~ sP5(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| c1_2(X0,X1)
| c3_2(X0,a748) ) ).
cnf(u5150,negated_conjecture,
( c10_2(X0,a748)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,a713)
| c3_2(X0,a713)
| c8_1(X0)
| ~ sP18(X0)
| c3_2(X0,a748)
| ~ sP43(X0)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a636) ) ).
cnf(u8434,negated_conjecture,
( ~ c6_2(X0,a676)
| c3_2(X0,a744)
| c2_1(X0)
| c5_2(X0,a744)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP5(X0)
| ~ c9_2(X0,a748)
| c8_1(X0)
| ~ c6_1(X0)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u8947,negated_conjecture,
( c6_2(X0,a747)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| ~ c6_1(X0)
| c5_2(X0,a636)
| ~ c8_1(X0) ) ).
cnf(u3838,negated_conjecture,
( ~ c9_2(X0,X1)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c2_2(X0,X1)
| c4_2(X0,a747)
| c5_2(X0,a712)
| c1_2(X0,X1) ) ).
cnf(u249,axiom,
( ~ c6_2(X0,a662)
| ~ sP36(X0) ) ).
cnf(u267,axiom,
( c8_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u8575,negated_conjecture,
( c6_2(X0,a747)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| ~ c10_1(X0)
| ~ c8_1(X0)
| c5_2(X0,a684)
| c3_2(X0,a684)
| ~ sP31(X0)
| sP27(X0) ) ).
cnf(u3211,negated_conjecture,
( ~ c6_2(X0,a712)
| ~ ndr1_1(X0)
| c7_1(X0)
| c3_2(X0,a751)
| sP18(X0) ) ).
cnf(u4113,negated_conjecture,
( c3_2(X0,a636)
| c10_1(X0)
| ~ c5_1(X0)
| ~ sP43(X0)
| ~ c2_1(X0)
| c5_2(X0,a636)
| c5_2(X0,a747) ) ).
cnf(u5012,negated_conjecture,
( ~ c3_2(X0,a636)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c3_1(X0)
| c5_2(X0,a636)
| c4_2(X0,a744) ) ).
cnf(u4554,negated_conjecture,
( ~ c8_2(X0,X1)
| c4_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a636)
| ~ sP17(X0)
| ~ c9_2(X0,a716)
| c10_1(X0)
| ~ sP43(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u4612,negated_conjecture,
( ~ c9_2(X0,X1)
| c3_2(X0,a748)
| c1_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c8_1(X0)
| ~ c6_1(X0)
| c2_1(X0)
| c10_1(X0) ) ).
cnf(u4629,negated_conjecture,
( c10_2(X0,a684)
| c4_2(X0,a684)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ c8_1(X0)
| sP27(X0) ) ).
cnf(u4095,negated_conjecture,
( ~ c9_2(X0,a685)
| ~ c3_1(X0)
| ~ c8_1(X0)
| ~ sP27(X0) ) ).
cnf(u8875,negated_conjecture,
( ~ c9_2(X0,a748)
| c5_2(X0,a743)
| c3_2(X0,a743)
| c8_1(X0)
| sP5(X0)
| c6_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| c3_2(X0,a748)
| ~ sP43(X0)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c6_1(X0)
| c2_1(X0)
| ~ c5_1(X0) ) ).
cnf(u4747,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP28(X0)
| ~ c8_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c1_2(X0,a747)
| c5_2(X0,a712)
| c3_2(X0,a712)
| ~ c2_1(X0)
| sP18(X0) ) ).
cnf(u5009,negated_conjecture,
( c4_2(X0,a744)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_1(X0)
| c2_2(X0,a751)
| c7_1(X0) ) ).
cnf(u4987,negated_conjecture,
( c1_2(X0,a712)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a712)
| ~ sP31(X0) ) ).
cnf(u4119,negated_conjecture,
( ~ c9_2(X0,a743)
| sP5(X0)
| ~ sP17(X0)
| c6_2(X0,a716) ) ).
cnf(u289,axiom,
( ~ c6_2(X0,a685)
| ~ sP27(X0) ) ).
cnf(u3221,negated_conjecture,
( c10_2(X0,a748)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ ndr1_1(X0)
| c8_1(X0)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u7209,negated_conjecture,
( ~ c9_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| c10_1(X0)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| ~ c3_2(X0,a636)
| c1_1(X0) ) ).
cnf(u3202,negated_conjecture,
( ~ c3_2(X0,a684)
| ~ ndr1_1(X0)
| c10_1(X0)
| c5_2(X0,a684)
| c3_1(X0)
| ~ c8_1(X0)
| sP27(X0) ) ).
cnf(u6677,negated_conjecture,
( ~ c3_2(X0,a676)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c6_1(X0)
| ~ c8_1(X0)
| sP18(X0)
| c2_2(X0,a712)
| c5_2(X0,a712)
| ~ c9_1(X0)
| c3_1(X0)
| c1_1(X0) ) ).
cnf(u5390,negated_conjecture,
( ~ c9_2(X0,a748)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c6_1(X0)
| c1_2(X0,X1)
| c2_1(X0)
| c3_2(X0,X1)
| c3_2(X0,a748)
| c5_2(X0,a713)
| c3_2(X0,a713)
| ~ sP18(X0) ) ).
cnf(u6541,negated_conjecture,
( ~ c6_2(X0,a675)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c9_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| c4_2(X0,a716)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u5315,negated_conjecture,
( c6_2(X0,a675)
| c1_1(X0)
| c4_2(X0,a684)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u4248,negated_conjecture,
( c6_2(X0,a750)
| c4_2(X0,a750)
| ~ sP3(X0)
| ~ c1_1(X0)
| c5_1(X0) ) ).
cnf(u4631,negated_conjecture,
( c10_2(X0,a716)
| c4_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ sP17(X0) ) ).
cnf(u5394,negated_conjecture,
( c3_2(X0,a744)
| ~ sP43(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_1(X0)
| c2_2(X0,a751)
| c7_1(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| c1_1(X0) ) ).
cnf(u292,axiom,
( ~ sP27(X0)
| ndr1_1(X0) ) ).
cnf(u4899,negated_conjecture,
( c1_2(X0,a662)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c9_1(X0)
| ~ c10_1(X0)
| c2_1(X0)
| c4_2(X0,a662)
| c5_1(X0) ) ).
cnf(u4774,negated_conjecture,
( ~ c2_2(X0,a747)
| c3_2(X0,a662)
| ~ sP36(X0)
| ~ c2_1(X0)
| c5_2(X0,a662)
| ~ c5_1(X0)
| ~ c1_1(X0)
| ~ sP28(X0)
| ~ c8_1(X0)
| c10_1(X0)
| ~ c6_1(X0)
| c1_2(X0,a747) ) ).
cnf(u4912,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ c8_1(X0)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c3_2(X0,a744)
| c10_1(X0)
| ~ c6_1(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u4245,negated_conjecture,
( c9_2(X0,a747)
| c10_1(X0)
| c3_2(X0,a662)
| ~ sP36(X0)
| ~ c2_1(X0)
| c5_2(X0,a662)
| ~ c5_1(X0) ) ).
cnf(u4511,negated_conjecture,
( ~ c6_2(X0,a675)
| ~ c3_2(X0,a662)
| c10_1(X0)
| ~ sP36(X0)
| ~ c9_2(X0,a662)
| ~ c3_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u6559,negated_conjecture,
( ~ c9_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a636)
| ~ sP17(X0)
| c4_2(X0,a716)
| c10_1(X0)
| ~ sP43(X0)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u4404,negated_conjecture,
( c10_2(X0,a676)
| ~ c6_1(X0)
| ~ sP31(X0)
| c4_2(X0,a676)
| ~ c8_1(X0)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0) ) ).
cnf(u5672,negated_conjecture,
( ~ c6_2(X0,a676)
| c3_2(X0,a750)
| c8_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c10_1(X0)
| ~ sP3(X0)
| c5_2(X0,a750)
| ~ c3_2(X0,a676)
| ~ sP31(X0) ) ).
cnf(u6077,negated_conjecture,
( ~ c9_2(X0,a685)
| c4_2(X0,a676)
| ~ c8_1(X0)
| c1_1(X0)
| ~ c6_1(X0)
| sP18(X0)
| c2_2(X0,a676)
| ~ c9_1(X0)
| c2_1(X0)
| c10_1(X0)
| ~ sP27(X0)
| ~ sP31(X0)
| ~ c3_2(X0,a712) ) ).
cnf(u4423,negated_conjecture,
( c3_2(X0,a744)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ c2_1(X0)
| c5_2(X0,a744)
| ~ c8_1(X0)
| c5_2(X0,a747) ) ).
cnf(u6314,negated_conjecture,
( ~ c1_2(X0,X1)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| c6_2(X0,a747)
| ~ c8_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ sP31(X0) ) ).
cnf(u6457,negated_conjecture,
( c10_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a743)
| c3_2(X0,a743)
| c8_1(X0)
| sP5(X0)
| c6_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| c3_2(X0,a748)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0) ) ).
cnf(u4540,negated_conjecture,
( c10_2(X0,a676)
| ~ sP31(X0)
| c4_2(X0,a676)
| c1_1(X0)
| c6_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0) ) ).
cnf(u5061,negated_conjecture,
( ~ c8_2(X0,X2)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a747)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c3_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c3_2(X0,X2) ) ).
cnf(u5552,negated_conjecture,
( c10_2(X0,a748)
| c3_2(X0,X1)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a748)
| c5_2(X0,X1)
| c8_1(X0)
| ~ sP43(X0)
| c4_2(X0,a748)
| c1_1(X0)
| c6_2(X0,a636) ) ).
cnf(u6475,negated_conjecture,
( ~ c9_2(X0,a748)
| ~ c5_1(X0)
| c5_2(X0,a743)
| c3_2(X0,a743)
| c8_1(X0)
| sP5(X0)
| c6_2(X0,a716)
| c10_1(X0)
| ~ sP17(X0)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c6_1(X0)
| c3_2(X0,X1)
| c3_2(X0,a748) ) ).
cnf(u5462,negated_conjecture,
( c6_2(X0,a747)
| c4_2(X0,a747)
| ~ c8_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a636)
| c3_2(X0,a636)
| ~ c6_1(X0)
| ~ sP43(X0) ) ).
cnf(u4924,negated_conjecture,
( ~ c8_2(X0,a714)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c8_1(X0)
| ~ c9_1(X0)
| c8_2(X0,a662)
| c2_1(X0)
| ~ c10_1(X0)
| c1_2(X0,a714) ) ).
cnf(u6989,negated_conjecture,
( ~ c9_2(X0,a662)
| c4_2(X0,a684)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c3_2(X0,a662)
| c10_1(X0)
| ~ sP36(X0)
| c1_1(X0)
| ~ c3_2(X0,a675) ) ).
cnf(u4421,negated_conjecture,
( c10_2(X0,a744)
| ~ c6_1(X0)
| ~ sP5(X0)
| c4_2(X0,a744)
| ~ c8_1(X0)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0) ) ).
cnf(u4703,negated_conjecture,
( ~ c6_2(X0,a675)
| c10_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| ~ c3_2(X0,a675)
| c10_2(X0,X1)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c8_1(X0)
| sP30(X0)
| sP31(X0) ) ).
cnf(u5186,negated_conjecture,
( ~ c9_2(X0,a743)
| c6_2(X0,a677)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP30(X0)
| c3_2(X0,a714)
| c4_2(X0,a677)
| sP5(X0)
| ~ c8_1(X0)
| ~ c3_2(X0,a677) ) ).
cnf(u7850,negated_conjecture,
( c2_2(X0,a751)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c2_1(X0)
| ~ sP31(X0)
| c7_1(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| c1_1(X0)
| c5_2(X0,a744) ) ).
cnf(u7714,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| c5_2(X0,a636)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747)
| c4_2(X0,a662)
| c5_1(X0)
| c5_2(X0,a662)
| c3_2(X0,a662)
| ~ sP36(X0) ) ).
cnf(u4697,negated_conjecture,
( ~ c1_2(X0,X1)
| c3_2(X0,X1)
| c8_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c6_1(X0)
| c5_2(X0,X1)
| ~ c9_2(X0,X1) ) ).
cnf(u6083,negated_conjecture,
( ~ c3_2(X0,a712)
| c4_2(X0,a676)
| ~ c8_1(X0)
| c1_1(X0)
| ~ c6_1(X0)
| sP18(X0)
| c2_2(X0,a676)
| ~ c9_1(X0)
| c3_1(X0)
| c5_2(X0,a712)
| ~ sP31(X0) ) ).
cnf(u5762,negated_conjecture,
( ~ c9_2(X0,a662)
| c1_1(X0)
| ~ sP31(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| c2_2(X0,a676)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c3_2(X0,a662)
| ~ sP36(X0)
| c4_2(X0,a676)
| ~ c3_2(X0,a676) ) ).
cnf(u7527,negated_conjecture,
( ~ c6_2(X0,a712)
| c1_1(X0)
| c6_2(X0,a676)
| c4_2(X0,a676)
| ~ c8_1(X0)
| sP27(X0)
| ~ c9_2(X0,a684)
| ~ c3_2(X0,a684)
| c10_1(X0)
| ~ sP31(X0)
| c4_2(X0,a684)
| ~ c3_2(X0,a712)
| sP18(X0) ) ).
cnf(u3938,negated_conjecture,
( c2_2(X0,a636)
| ~ sP43(X0)
| c5_2(X0,a636)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u3648,negated_conjecture,
( ~ c1_2(X0,a748)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c8_1(X0)
| ~ c6_1(X0)
| c10_2(X0,X1)
| c2_1(X0)
| ~ c9_2(X0,a748) ) ).
cnf(u8684,negated_conjecture,
( c6_2(X0,a712)
| c1_1(X0)
| sP18(X0)
| c4_2(X0,a744)
| ~ c6_1(X0)
| ~ sP5(X0)
| ~ c8_1(X0)
| ~ sP43(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c5_2(X0,a636) ) ).
cnf(u5468,negated_conjecture,
( c6_2(X0,a747)
| c4_2(X0,a747)
| ~ c8_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a712)
| c3_2(X0,a712)
| ~ c6_1(X0)
| sP18(X0) ) ).
cnf(u3944,negated_conjecture,
( c9_2(X0,a747)
| ~ c6_1(X0)
| ~ sP43(X0)
| ~ c2_1(X0)
| c5_2(X0,a636)
| c3_2(X0,a636)
| ~ c8_1(X0) ) ).
cnf(u5215,negated_conjecture,
( ~ c9_2(X0,a748)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| c3_2(X0,a748)
| c3_2(X0,X1)
| c5_2(X0,X2)
| c3_2(X0,X2)
| ~ c6_1(X0)
| c10_2(X0,X2)
| c2_1(X0)
| c1_2(X0,X1) ) ).
cnf(u4068,negated_conjecture,
( ~ c8_2(X0,a677)
| ~ c1_1(X0)
| ~ sP30(X0)
| ~ c9_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| c1_2(X0,a677) ) ).
cnf(u339,axiom,
( ~ c10_2(X0,a713)
| ~ sP18(X0) ) ).
cnf(u5078,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP30(X0)
| ~ c8_1(X0)
| ~ c1_1(X0)
| c4_2(X0,a677)
| ~ c6_1(X0)
| c1_2(X0,a747)
| c5_2(X0,a684)
| c3_2(X0,a684)
| ~ c2_1(X0)
| sP27(X0) ) ).
cnf(u5071,negated_conjecture,
( ~ c2_2(X0,a713)
| ~ sP30(X0)
| ~ c8_1(X0)
| ~ c1_1(X0)
| c4_2(X0,a677)
| ~ c6_1(X0)
| c1_2(X0,a713)
| ~ sP18(X0) ) ).
cnf(u5940,negated_conjecture,
( ~ c6_2(X0,a636)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u5316,negated_conjecture,
( ~ c8_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a675)
| c4_2(X0,a675)
| sP30(X0)
| sP31(X0)
| ~ c8_1(X0)
| sP27(X0)
| ~ c9_2(X0,a684)
| ~ c3_2(X0,a684)
| c10_1(X0)
| c4_2(X0,a684)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u7630,negated_conjecture,
( ~ c2_2(X0,a744)
| ~ c8_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c6_1(X0)
| c4_2(X0,a747)
| c5_2(X0,a712)
| c1_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u3809,negated_conjecture,
( ~ c8_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0)
| ~ c8_1(X0)
| sP27(X0)
| ~ c9_2(X0,a684)
| ~ c3_2(X0,a684)
| c10_1(X0)
| c4_2(X0,a684)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u5980,negated_conjecture,
( ~ c6_2(X0,a636)
| c8_1(X0)
| c2_2(X0,X1)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c9_2(X0,a748)
| ~ c3_2(X0,a748)
| c10_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ c3_2(X0,a636)
| ~ sP43(X0) ) ).
cnf(u5485,negated_conjecture,
( c8_2(X0,a747)
| c5_2(X0,a744)
| ~ c8_1(X0)
| ~ sP5(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| c6_2(X0,a747) ) ).
cnf(u4983,negated_conjecture,
( c3_2(X0,a751)
| c4_2(X0,a744)
| ~ c8_1(X0)
| c1_1(X0)
| ~ c6_1(X0)
| sP18(X0)
| c2_1(X0)
| c7_1(X0)
| ~ sP5(X0) ) ).
cnf(u7801,negated_conjecture,
( c4_2(X0,a744)
| c4_2(X0,a676)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP5(X0)
| c1_1(X0)
| c10_1(X0)
| ~ sP31(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c2_2(X0,a751)
| c7_1(X0) ) ).
cnf(u3937,negated_conjecture,
( ~ c1_2(X0,a636)
| ~ c6_1(X0)
| ~ sP43(X0)
| c2_1(X0)
| ~ c9_2(X0,a636) ) ).
cnf(u5092,negated_conjecture,
( c4_2(X0,a744)
| ~ sP5(X0)
| ~ c6_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a744)
| ~ c8_1(X0)
| c5_2(X0,a747)
| ~ c10_1(X0) ) ).
cnf(u4472,negated_conjecture,
( c10_2(X0,a676)
| ~ sP43(X0)
| c4_2(X0,a676)
| c1_1(X0)
| c6_2(X0,a636)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ sP31(X0) ) ).
cnf(u5127,negated_conjecture,
( c4_2(X0,a750)
| ~ sP3(X0)
| c8_1(X0)
| c2_2(X0,a748)
| c5_2(X0,a748)
| ~ c9_1(X0)
| c2_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| c3_1(X0)
| c10_1(X0)
| c5_2(X0,a750) ) ).
cnf(u4202,negated_conjecture,
( ~ c4_2(X0,a744)
| ~ c10_1(X0)
| ~ c4_1(X0)
| c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u3828,negated_conjecture,
( ~ c1_2(X0,a748)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c6_1(X0)
| c1_2(X0,X1)
| c2_1(X0)
| ~ c9_2(X0,a748) ) ).
cnf(u5363,negated_conjecture,
( ~ c9_2(X0,a662)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c8_1(X0)
| c3_2(X0,a714)
| ~ c9_1(X0)
| ~ c10_1(X0)
| c2_1(X0)
| ~ c6_1(X0) ) ).
cnf(u5118,negated_conjecture,
( ~ c9_2(X0,a748)
| c3_2(X0,a750)
| c8_1(X0)
| ~ c6_1(X0)
| ~ sP3(X0)
| c2_1(X0)
| c5_2(X0,a750)
| ~ c5_1(X0)
| c10_1(X0)
| c3_2(X0,a748) ) ).
cnf(u4827,negated_conjecture,
( c6_2(X0,a636)
| c4_2(X0,a684)
| c1_1(X0)
| ~ sP43(X0)
| ~ c8_1(X0)
| sP27(X0)
| c2_2(X0,a684)
| c5_2(X0,a684)
| ~ c9_1(X0)
| c2_1(X0) ) ).
cnf(u7285,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ sP31(X0)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c8_1(X0)
| c4_2(X0,a747)
| ~ c2_1(X0)
| c1_2(X0,a747)
| c4_2(X0,a676) ) ).
cnf(u3826,negated_conjecture,
( c10_2(X0,a748)
| c3_2(X0,X1)
| c10_1(X0)
| ~ c5_1(X0)
| c5_2(X0,X1)
| c8_1(X0)
| ~ c2_1(X0)
| c9_2(X0,a747) ) ).
cnf(u6657,negated_conjecture,
( ~ c8_2(X0,a714)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ sP43(X0)
| ~ c2_1(X0)
| c8_2(X0,a747)
| c6_2(X0,a747)
| c5_2(X0,a636)
| c1_2(X0,a714) ) ).
cnf(u8843,negated_conjecture,
( c6_2(X0,a747)
| c5_2(X0,a712)
| ~ c6_1(X0)
| sP18(X0)
| ~ c10_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c3_2(X0,a714)
| ~ c8_1(X0) ) ).
cnf(u5255,negated_conjecture,
( c2_2(X0,a748)
| c8_1(X0)
| c2_2(X0,a744)
| ~ c9_1(X0)
| c2_1(X0)
| c5_2(X0,a744)
| c5_2(X0,a748)
| c3_1(X0)
| c10_1(X0)
| ~ sP5(X0) ) ).
cnf(u4515,negated_conjecture,
( ~ c9_2(X0,a662)
| ~ c3_2(X0,a662)
| c10_1(X0)
| ~ sP36(X0)
| ~ c3_2(X0,a744)
| ~ sP5(X0) ) ).
cnf(u377,axiom,
( ~ c3_2(X0,a732)
| ~ sP9(X0) ) ).
cnf(u3332,negated_conjecture,
( ~ c6_2(X0,a675)
| sP31(X0)
| c3_2(X0,a751)
| c7_1(X0)
| c9_2(X0,a675)
| sP30(X0) ) ).
cnf(u6328,negated_conjecture,
( ~ c2_2(X0,a747)
| ~ c6_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a662)
| c3_2(X0,a662)
| ~ c8_1(X0)
| ~ sP36(X0)
| ~ c5_2(X0,a684)
| c4_2(X0,a662)
| c4_2(X0,a684)
| c1_2(X0,a747)
| sP27(X0) ) ).
cnf(u272,axiom,
( ~ c9_2(X0,a677)
| ~ sP30(X0) ) ).
cnf(u5456,negated_conjecture,
( c6_2(X0,a747)
| c4_2(X0,a747)
| ~ c8_1(X0)
| ~ c1_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c5_2(X0,a684)
| c3_2(X0,a684)
| ~ c6_1(X0)
| sP27(X0) ) ).
cnf(u250,axiom,
( ~ sP36(X0)
| ndr1_1(X0) ) ).
cnf(u4491,negated_conjecture,
( c7_2(X0,a714)
| c2_1(X0)
| ~ c6_1(X0)
| ~ c1_1(X0)
| ~ sP36(X0)
| ~ c8_1(X0)
| ~ c9_1(X0)
| c8_2(X0,a662) ) ).
cnf(u5755,negated_conjecture,
( c3_2(X0,a751)
| c1_1(X0)
| ~ sP31(X0)
| ~ c8_1(X0)
| ~ c6_1(X0)
| c2_2(X0,a676)
| ~ c9_1(X0)
| c2_1(X0)
| c4_2(X0,a676)
| c7_1(X0) ) ).
cnf(u7181,negated_conjecture,
( c3_2(X0,a751)
| c1_1(X0)
| c4_2(X0,a744)
| sP18(X0)
| ~ sP5(X0)
| c10_1(X0)
| ~ c6_1(X0)
| c5_2(X0,a744)
| c5_2(X0,a747)
| c7_1(X0)
| ~ c8_1(X0) ) ).
cnf(u4114,negated_conjecture,
( c10_2(X0,a716)
| ~ sP17(X0)
| c4_2(X0,a716)
| c1_1(X0)
| c6_2(X0,a712)
| sP18(X0) ) ).
cnf(u8590,negated_conjecture,
( c6_2(X0,a747)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c6_1(X0)
| c3_2(X0,a714)
| ~ c2_1(X0)
| ~ c10_1(X0)
| ~ c8_1(X0)
| c5_2(X0,a744)
| ~ sP31(X0)
| ~ sP5(X0)
| c4_2(X0,a744) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN422+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n018.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 15:57:40 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 Running first-order theorem proving
% 0.09/0.20 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.28/1.47 % (3506778)Detected formulas, will run a generic FOF schedule.
% 5.28/1.47 % (3506783)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=3002141707:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.28/1.47 % (3506788)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=809238434:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.28/1.47 % (3506786)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2249981453:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.28/1.47 % (3506789)dis-21_1_sil=8000:lcm=predicate:random_seed=2333424842: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.28/1.47 % (3506785)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=209005918:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.28/1.47 % (3506787)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2293354557:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.28/1.47 % (3506784)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=2017228234:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.28/1.47 % (3506788)Refutation not found, incomplete strategy
% 5.28/1.47 % (3506788)------------------------------
% 5.28/1.47 % (3506788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.47 % (3506788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.47 % (3506788)CaDiCaL version: 2.1.3
% 5.28/1.47 % (3506788)Termination reason: Refutation not found, incomplete strategy
% 5.28/1.47 % (3506788)Time elapsed: 0.019 s
% 5.28/1.47 % (3506788)Peak memory usage: 90 MB
% 5.28/1.47 % (3506788)Instructions burned: 30 (million)
% 5.28/1.47 % (3506787)Instruction limit reached!
% 5.28/1.47 % (3506787)------------------------------
% 5.28/1.47 % (3506787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.47 % (3506787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.47 % (3506787)CaDiCaL version: 2.1.3
% 5.28/1.47 % (3506787)Termination reason: Instruction limit
% 5.28/1.47 % (3506787)Termination phase: Saturation
% 5.28/1.47 % (3506787)Time elapsed: 0.063 s
% 5.28/1.47 % (3506787)Peak memory usage: 89 MB
% 5.28/1.47 % (3506787)Instructions burned: 119 (million)
% 5.28/1.47 % (3506786)Instruction limit reached!
% 5.28/1.47 % (3506786)------------------------------
% 5.28/1.47 % (3506786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.47 % (3506786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.47 % (3506786)CaDiCaL version: 2.1.3
% 5.28/1.47 % (3506786)Termination reason: Instruction limit
% 5.28/1.47 % (3506786)Termination phase: Saturation
% 5.28/1.47 % (3506786)Time elapsed: 0.063 s
% 5.28/1.47 % (3506786)Peak memory usage: 91 MB
% 5.28/1.47 % (3506786)Instructions burned: 111 (million)
% 5.28/1.47 % (3506789)Instruction limit reached!
% 5.28/1.47 % (3506789)------------------------------
% 5.28/1.47 % (3506789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.47 % (3506789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.47 % (3506789)CaDiCaL version: 2.1.3
% 5.28/1.47 % (3506789)Termination reason: Instruction limit
% 5.28/1.47 % (3506789)Termination phase: Saturation
% 5.28/1.47 % (3506789)Time elapsed: 0.069 s
% 5.28/1.47 % (3506789)Peak memory usage: 91 MB
% 5.28/1.47 % (3506789)Instructions burned: 130 (million)
% 5.28/1.47 % (3506797)lrs+10_1_sil=8000:sp=occurrence:random_seed=3191069508:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.28/1.47 % (3506798)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3460066576:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.28/1.47 % (3506799)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2848748045:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.28/1.47 % (3506798)Refutation not found, incomplete strategy
% 5.28/1.47 % (3506798)------------------------------
% 5.28/1.47 % (3506798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.47 % (3506798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.47 % (3506798)CaDiCaL version: 2.1.3
% 5.28/1.47 % (3506798)Termination reason: Refutation not found, incomplete strategy
% 5.28/1.47 % (3506798)Time elapsed: 0.021 s
% 5.28/1.47 % (3506798)Peak memory usage: 90 MB
% 5.28/1.47 % (3506798)Instructions burned: 33 (million)
% 5.28/1.47 % (3506799)Refutation not found, incomplete strategy
% 5.28/1.47 % (3506799)------------------------------
% 5.28/1.47 % (3506799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.47 % (3506799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.47 % (3506799)CaDiCaL version: 2.1.3
% 5.28/1.47 % (3506799)Termination reason: Refutation not found, incomplete strategy
% 5.28/1.47 % (3506799)Time elapsed: 0.018 s
% 5.28/1.47 % (3506799)Peak memory usage: 90 MB
% 5.28/1.47 % (3506799)Instructions burned: 28 (million)
% 5.28/1.47 % (3506788)------------------------------
% 5.28/1.47 % (3506788)------------------------------
% 5.28/1.47 % (3506797)First to succeed.
% 5.28/1.47 % (3506797)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3506778"
% 5.28/1.47 % (3506783)Also succeeded, but the first one will report.
% 5.28/1.47 % (3506803)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=1958362189:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 5.28/1.47 % (3506803)Refutation not found, incomplete strategy
% 5.28/1.47 % (3506803)------------------------------
% 5.28/1.47 % (3506803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.47 % (3506803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.47 % (3506803)CaDiCaL version: 2.1.3
% 5.28/1.47 % (3506803)Termination reason: Refutation not found, incomplete strategy
% 5.28/1.47 % (3506803)Time elapsed: 0.023 s
% 5.28/1.47 % (3506803)Peak memory usage: 90 MB
% 5.28/1.47 % (3506803)Instructions burned: 35 (million)
% 5.28/1.47 % (3506798)------------------------------
% 5.28/1.47 % (3506798)------------------------------
% 5.28/1.47 % (3506799)------------------------------
% 5.28/1.47 % (3506799)------------------------------
% 5.28/1.47 % SZS status CounterSatisfiable for theBenchmark
% 5.28/1.47 % SZS output start Saturation.
% See solution above
% 6.35/1.66 % SZS output start Definitions and Model Updates.
% 6.35/1.66 % SZS output end Definitions and Model Updates.
% 6.35/1.66 % (3506797)------------------------------
% 6.35/1.66 % (3506797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.35/1.66 % (3506797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.35/1.66 % (3506797)CaDiCaL version: 2.1.3
% 6.35/1.66 % (3506797)Termination reason: Satisfiable
% 6.35/1.66 % (3506797)Time elapsed: 0.163 s
% 6.35/1.66 % (3506797)Peak memory usage: 94 MB
% 6.35/1.66 % (3506797)Instructions burned: 308 (million)
% 6.35/1.66 % (3506797)------------------------------
% 6.35/1.66 % (3506797)------------------------------
% 6.35/1.66 % (3506778)Success in time 0.823 s
% 6.35/1.66 % Vampire exiting
%------------------------------------------------------------------------------