%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN429-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 : n014.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:37 PM UTC 2026
% Result : Satisfiable 11.04s 2.05s
% Output : Saturation 11.91s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u741,negated_conjecture,
c9_0 ).
cnf(u749,negated_conjecture,
ndr1_0 ).
cnf(u753,negated_conjecture,
( ~ c7_2(X0,X3)
| c4_2(X0,X3)
| c5_2(X0,X2)
| ~ c10_2(X0,X1)
| ~ c3_2(X0,X3)
| ~ c7_2(X0,X2)
| ~ c1_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u764,negated_conjecture,
( ~ c6_2(X0,X1)
| c5_2(X0,X4)
| c2_2(X0,X4)
| c2_2(X0,X1)
| ~ c9_1(X0)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u794,negated_conjecture,
~ c6_0 ).
cnf(u813,negated_conjecture,
c7_0 ).
cnf(u833,negated_conjecture,
~ c1_0 ).
cnf(u864,negated_conjecture,
c3_0 ).
cnf(u868,negated_conjecture,
( ~ c6_2(X1,X2)
| c8_1(X1)
| c8_2(X1,X3)
| c7_2(X1,X3)
| ~ c5_2(X1,X3)
| ~ ndr1_1(X1)
| ~ c9_2(X1,X2)
| ~ c2_2(X1,X2) ) ).
cnf(u879,negated_conjecture,
~ c10_0 ).
cnf(u886,negated_conjecture,
( ~ c2_1(X0)
| c10_1(X0)
| c9_2(X0,X3)
| c8_2(X0,X3)
| c4_2(X0,X3)
| ~ ndr1_1(X0) ) ).
cnf(u909,negated_conjecture,
( ~ c3_1(X3)
| ~ c10_1(X3) ) ).
cnf(u916,negated_conjecture,
ndr1_1(a188) ).
cnf(u920,negated_conjecture,
( ~ c2_2(a188,X2)
| c7_2(a188,X2)
| ~ c8_2(a188,X2) ) ).
cnf(u923,negated_conjecture,
( ~ c6_2(X0,X1)
| c5_1(X0)
| c3_1(X0)
| c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u926,negated_conjecture,
ssSkC26 ).
cnf(u950,negated_conjecture,
ndr1_1(a195) ).
cnf(u954,negated_conjecture,
( ~ c1_2(a195,X2)
| ~ c4_2(a195,X2)
| ~ c2_2(a195,X2) ) ).
cnf(u960,negated_conjecture,
ssSkC28 ).
cnf(u969,negated_conjecture,
c8_0 ).
cnf(u973,negated_conjecture,
( ~ c3_2(X0,X1)
| c6_1(X0)
| c6_2(X0,X2)
| c9_2(X0,X1)
| ~ c4_2(X0,X2)
| ~ c2_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u991,negated_conjecture,
( ~ c6_2(X0,X1)
| c3_1(X0)
| c5_2(X0,X2)
| c9_2(X0,X1)
| ~ c9_2(X0,X2)
| ~ c2_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u994,negated_conjecture,
ssSkC27 ).
cnf(u1007,negated_conjecture,
ndr1_1(a164) ).
cnf(u1011,negated_conjecture,
( ~ c4_2(X0,X1)
| c3_1(X0)
| c6_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u1041,negated_conjecture,
~ c4_0 ).
cnf(u1045,negated_conjecture,
( ~ c9_2(X0,X2)
| c10_2(X0,X3)
| c7_2(X0,X2)
| ~ c2_2(X0,X3)
| ~ c4_2(X0,X1)
| ~ c5_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u1050,negated_conjecture,
~ c5_1(a80) ).
cnf(u1060,negated_conjecture,
( ~ c1_2(X0,a26)
| ~ ssSkP3(X0)
| ~ ssSkP4(X0) ) ).
cnf(u1084,negated_conjecture,
c7_1(a80) ).
cnf(u1089,negated_conjecture,
c3_1(a80) ).
cnf(u1093,negated_conjecture,
( ~ c7_2(X1,X2)
| c2_1(X1)
| c1_2(X1,X2)
| ~ c3_1(X1)
| ~ ndr1_1(X1)
| ~ c3_2(X1,X2) ) ).
cnf(u1100,negated_conjecture,
( ~ ssSkP3(X0)
| c7_2(X0,a26)
| ~ ssSkP4(X0) ) ).
cnf(u1104,negated_conjecture,
( ~ ssSkP3(X0)
| c6_2(X0,a26)
| ~ ssSkP4(X0) ) ).
cnf(u1109,negated_conjecture,
~ c5_0 ).
cnf(u1112,negated_conjecture,
( ~ c3_2(X0,X1)
| c3_2(X0,X2)
| c7_2(X0,X1)
| ~ c8_2(X0,a144)
| ~ c1_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u1115,negated_conjecture,
ssSkC16 ).
cnf(u1124,negated_conjecture,
( ~ c10_2(X0,X1)
| c8_1(X0)
| c9_2(X0,X2)
| c4_2(X0,X2)
| c8_2(X0,X1)
| c5_2(X0,X1)
| ~ c8_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u1128,negated_conjecture,
( ~ ssSkP3(X0)
| ndr1_1(X0)
| ~ ssSkP4(X0) ) ).
cnf(u1132,negated_conjecture,
( ~ c3_2(X0,X1)
| c6_2(X0,a144)
| c3_2(X0,X2)
| c7_2(X0,X1)
| ~ c1_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u1136,negated_conjecture,
( ~ c3_2(X0,X1)
| c10_2(X0,a144)
| c3_2(X0,X2)
| c7_2(X0,X1)
| ~ c1_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u1140,negated_conjecture,
c2_0 ).
cnf(u1144,negated_conjecture,
( ~ c7_2(X0,X1)
| c2_2(X0,X1)
| ~ c9_1(X0)
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u1148,negated_conjecture,
( ~ c9_2(X0,a77)
| c7_2(X0,X1)
| ~ c6_1(X0)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u1153,negated_conjecture,
~ c8_1(a171) ).
cnf(u1161,negated_conjecture,
~ c4_1(a171) ).
cnf(u1166,negated_conjecture,
~ c1_1(a171) ).
cnf(u1186,negated_conjecture,
~ ssSkC25 ).
cnf(u1190,negated_conjecture,
( ~ c6_2(X0,a185)
| c1_2(X0,X1)
| c7_2(X0,X2)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u1194,negated_conjecture,
( ~ c5_2(X0,a185)
| c1_2(X0,X1)
| c7_2(X0,X2)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u1198,negated_conjecture,
( ~ c3_2(X0,a185)
| c1_2(X0,X1)
| c7_2(X0,X2)
| c5_2(X0,X2)
| c4_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u1214,negated_conjecture,
( ~ c1_2(X0,X1)
| c7_1(X0)
| c7_2(X0,X1)
| ~ c6_2(X0,a52)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u1218,negated_conjecture,
( ~ c2_2(X0,X1)
| c3_2(X0,a77)
| c7_2(X0,X1)
| ~ c6_1(X0)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u1222,negated_conjecture,
( ~ c2_2(X0,X1)
| c1_2(X0,a77)
| c7_2(X0,X1)
| ~ c6_1(X0)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u1226,negated_conjecture,
ssSkC22 ).
cnf(u1230,negated_conjecture,
( ~ c3_2(X0,a177)
| c1_2(X0,X1)
| ~ ssSkP16(X0)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u1234,negated_conjecture,
( ~ c2_2(X0,a177)
| c1_2(X0,X1)
| ~ ssSkP16(X0)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u1238,negated_conjecture,
~ ssSkC29 ).
cnf(u1242,negated_conjecture,
( ~ c7_2(X0,X1)
| c8_2(X0,X1)
| ~ c1_1(X0)
| ~ c2_2(X0,a198)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u1272,negated_conjecture,
( ~ c3_2(X0,X1)
| c8_1(X0)
| c9_2(X0,X1)
| ~ c2_1(X0)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u1280,negated_conjecture,
ssSkC0 ).
cnf(u1284,negated_conjecture,
( ~ c7_2(X0,a23)
| c5_2(X0,X1)
| ~ ssSkP2(X0)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1)
| ~ c4_2(X0,X1) ) ).
cnf(u1288,negated_conjecture,
( ~ c6_2(X0,X1)
| c5_2(X0,X1)
| ~ c2_2(X0,a23)
| ~ ndr1_1(X0)
| ~ ssSkP2(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u1292,negated_conjecture,
( ~ c1_2(X0,X1)
| c7_1(X0)
| c2_2(X0,a52)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u1296,negated_conjecture,
( ~ c6_2(X0,X1)
| c8_2(X0,X1)
| c2_2(X0,X1)
| ~ c4_1(X0)
| ~ c8_2(X0,a55)
| ~ ndr1_1(X0) ) ).
cnf(u1299,negated_conjecture,
ssSkC4 ).
cnf(u1304,negated_conjecture,
( ~ c7_2(X0,a55)
| c8_2(X0,X1)
| c2_2(X0,X1)
| ~ c4_1(X0)
| ~ c6_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1313,negated_conjecture,
( ~ c2_2(X0,X1)
| c8_2(X0,a177)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1)
| ~ ssSkP16(X0) ) ).
cnf(u1317,negated_conjecture,
c9_1(a188) ).
cnf(u1322,negated_conjecture,
c3_1(a188) ).
cnf(u1328,negated_conjecture,
ssSkC2 ).
cnf(u1335,negated_conjecture,
( ~ c7_2(X0,X1)
| c4_2(X0,a198)
| c8_2(X0,X1)
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u1339,negated_conjecture,
( ~ c7_2(X0,X1)
| c1_2(X0,a198)
| c8_2(X0,X1)
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u1343,negated_conjecture,
~ ssSkC31 ).
cnf(u1347,negated_conjecture,
( ~ c3_2(X0,X1)
| c8_2(X0,a204)
| c1_2(X0,X1)
| ~ c7_1(X0)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u1351,negated_conjecture,
( ~ c3_2(X0,X1)
| c4_2(X0,a204)
| c1_2(X0,X1)
| ~ c7_1(X0)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u1355,negated_conjecture,
~ ssSkC33 ).
cnf(u1359,negated_conjecture,
( ~ c6_2(X0,X1)
| c9_2(X0,X1)
| ~ c10_2(X0,a209)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1)
| ~ ssSkP17(X0) ) ).
cnf(u1369,negated_conjecture,
~ c3_1(a164) ).
cnf(u1373,negated_conjecture,
( ~ c1_2(X0,X1)
| c9_1(X0)
| c4_1(X0)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c10_2(X0,X1) ) ).
cnf(u1377,negated_conjecture,
( ~ c3_2(X0,X1)
| ~ c9_1(X0)
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u1381,negated_conjecture,
( ~ c6_2(X0,X1)
| c8_2(X0,a23)
| c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ssSkP2(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u1393,negated_conjecture,
~ ssSkC7 ).
cnf(u1397,negated_conjecture,
( ~ ndr1_1(X0)
| c9_2(X0,X1)
| c4_2(X0,X1)
| c10_2(X0,X1)
| ~ c9_1(X0)
| ~ c6_2(X0,a70) ) ).
cnf(u1401,negated_conjecture,
( ~ ndr1_1(X0)
| c9_2(X0,X1)
| c4_2(X0,X1)
| c10_2(X0,X1)
| ~ c9_1(X0)
| ~ c10_2(X0,a70) ) ).
cnf(u1405,negated_conjecture,
( ~ c6_2(X0,X1)
| c5_2(X0,a209)
| c9_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1)
| ~ ssSkP17(X0) ) ).
cnf(u1409,negated_conjecture,
( ~ c6_2(X0,X1)
| c3_2(X0,a209)
| c9_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1)
| ~ ssSkP17(X0) ) ).
cnf(u1422,negated_conjecture,
~ c8_2(a195,a196) ).
cnf(u1427,negated_conjecture,
~ c2_2(a195,a196) ).
cnf(u1432,negated_conjecture,
~ c9_2(a195,a197) ).
cnf(u1437,negated_conjecture,
~ c7_2(a195,a197) ).
cnf(u1442,negated_conjecture,
~ c4_2(a195,a197) ).
cnf(u1446,negated_conjecture,
( ~ ndr1_1(X0)
| c8_2(X0,a70)
| c9_2(X0,X1)
| c4_2(X0,X1)
| c10_2(X0,X1)
| ~ c9_1(X0) ) ).
cnf(u1450,negated_conjecture,
~ ssSkC9 ).
cnf(u1454,negated_conjecture,
( ~ c9_2(X0,X1)
| c2_2(X0,X1)
| ~ c6_1(X0)
| ~ c9_2(X0,a78)
| ~ ndr1_1(X0) ) ).
cnf(u1458,negated_conjecture,
( ~ c9_2(X0,X1)
| c2_2(X0,X1)
| ~ c6_1(X0)
| ~ c7_2(X0,a78)
| ~ ndr1_1(X0) ) ).
cnf(u1462,negated_conjecture,
( ~ c9_2(X0,X1)
| c2_2(X0,X1)
| ~ c6_1(X0)
| ~ c3_2(X0,a78)
| ~ ndr1_1(X0) ) ).
cnf(u1466,negated_conjecture,
~ ssSkC23 ).
cnf(u1470,negated_conjecture,
( ~ c2_2(X0,X1)
| c7_1(X0)
| c8_2(X0,a178)
| c9_2(X0,X1)
| c10_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1474,negated_conjecture,
( ~ c2_2(X0,X1)
| c7_1(X0)
| c5_2(X0,a178)
| c9_2(X0,X1)
| c10_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1481,negated_conjecture,
( ~ c7_2(X0,a65)
| ~ c6_1(X0)
| ~ ssSkP9(X0) ) ).
cnf(u1533,negated_conjecture,
ssSkC12 ).
cnf(u1538,negated_conjecture,
ndr1_1(a141) ).
cnf(u1542,negated_conjecture,
( ~ c8_2(a141,X0)
| c6_2(a141,X0)
| c10_2(a141,X0) ) ).
cnf(u1554,negated_conjecture,
~ ssSkC20 ).
cnf(u1566,negated_conjecture,
( ~ c6_1(X0)
| c4_2(X0,a65)
| ~ ssSkP9(X0) ) ).
cnf(u1570,negated_conjecture,
( ~ c6_1(X0)
| c2_2(X0,a65)
| ~ ssSkP9(X0) ) ).
cnf(u1574,negated_conjecture,
ndr1_1(a1) ).
cnf(u1578,negated_conjecture,
( ~ c3_2(a1,X0)
| c7_2(a1,X0)
| ~ c6_2(a1,X0) ) ).
cnf(u1582,negated_conjecture,
ndr1_1(a7) ).
cnf(u1586,negated_conjecture,
( ~ c1_2(a7,X0)
| c4_2(a7,X0)
| ~ c5_2(a7,X0) ) ).
cnf(u1618,negated_conjecture,
ndr1_1(a59) ).
cnf(u1622,negated_conjecture,
( ~ c10_2(a59,X0)
| c9_2(a59,X0)
| c3_2(a59,X0) ) ).
cnf(u1626,negated_conjecture,
ndr1_1(a71) ).
cnf(u1646,negated_conjecture,
ndr1_1(a160) ).
cnf(u1650,negated_conjecture,
( ~ c4_2(a160,X0)
| c6_2(a160,X0)
| c2_2(a160,X0) ) ).
cnf(u1653,negated_conjecture,
ssSkC19 ).
cnf(u1665,negated_conjecture,
ssSkC30 ).
cnf(u1671,negated_conjecture,
ssSkC14 ).
cnf(u1682,negated_conjecture,
ndr1_1(a194) ).
cnf(u1698,negated_conjecture,
~ ssSkC34 ).
cnf(u1702,negated_conjecture,
ndr1_1(a213) ).
cnf(u1706,negated_conjecture,
( ~ c2_2(a213,X0)
| c7_2(a213,X0)
| ~ c8_2(a213,X0) ) ).
cnf(u1710,negated_conjecture,
( ~ ssSkP9(X0)
| ndr1_1(X0)
| ~ c6_1(X0) ) ).
cnf(u1714,negated_conjecture,
( ~ c3_2(a7,X0)
| c7_2(a7,X0)
| c1_2(a7,X0) ) ).
cnf(u1718,negated_conjecture,
( c8_2(a19,X0)
| c10_2(a19,X0)
| c5_2(a19,X0) ) ).
cnf(u1721,negated_conjecture,
ndr1_1(a19) ).
cnf(u1733,negated_conjecture,
ssSkC3 ).
cnf(u1746,negated_conjecture,
~ ssSkC6 ).
cnf(u1754,negated_conjecture,
ndr1_1(a79) ).
cnf(u1790,negated_conjecture,
( c1_2(a160,X0)
| c9_2(a160,X0)
| c2_2(a160,X0) ) ).
cnf(u1809,negated_conjecture,
ssSkC32 ).
cnf(u1815,negated_conjecture,
ssSkC8 ).
cnf(u1827,negated_conjecture,
ssSkC17 ).
cnf(u1838,negated_conjecture,
( ~ c6_2(X0,a11)
| ~ c3_1(X0)
| ~ ssSkP0(X0) ) ).
cnf(u1842,negated_conjecture,
( ~ c4_2(X0,a11)
| ~ c3_1(X0)
| ~ ssSkP0(X0) ) ).
cnf(u1930,negated_conjecture,
ssSkC18 ).
cnf(u1934,negated_conjecture,
( ~ c1_2(X0,a157)
| ~ c6_1(X0)
| ~ ssSkP14(X0) ) ).
cnf(u1970,negated_conjecture,
~ ssSkC5 ).
cnf(u1981,negated_conjecture,
ssSkC10 ).
cnf(u1986,negated_conjecture,
( ~ c9_2(X0,a151)
| ~ c2_1(X0) ) ).
cnf(u1990,negated_conjecture,
( ~ c6_2(X0,a151)
| ~ c2_1(X0) ) ).
cnf(u1994,negated_conjecture,
ndr1_1(a183) ).
cnf(u1998,negated_conjecture,
( ~ c4_2(a183,X0)
| c1_2(a183,X0) ) ).
cnf(u2001,negated_conjecture,
ssSkC24 ).
cnf(u2006,negated_conjecture,
( ~ c9_1(X0)
| c3_1(X0)
| c2_1(X0) ) ).
cnf(u2010,negated_conjecture,
( ~ ssSkP0(X0)
| c1_2(X0,a11)
| ~ c3_1(X0) ) ).
cnf(u2064,negated_conjecture,
( ~ c6_1(X0)
| c8_2(X0,a157)
| ~ ssSkP14(X0) ) ).
cnf(u2068,negated_conjecture,
( ~ c6_1(X0)
| c6_2(X0,a157)
| ~ ssSkP14(X0) ) ).
cnf(u2081,negated_conjecture,
ssSkC11 ).
cnf(u2092,negated_conjecture,
( ~ c6_2(X0,a168)
| ~ c1_1(X0)
| ~ ssSkP15(X0) ) ).
cnf(u2104,negated_conjecture,
ndr1_1(a73) ).
cnf(u2108,negated_conjecture,
( ~ c10_2(a73,X0)
| c8_2(a73,X0) ) ).
cnf(u2112,negated_conjecture,
( ~ c2_1(X0)
| c4_2(X0,a151) ) ).
cnf(u2128,negated_conjecture,
( ~ ssSkP0(X0)
| ndr1_1(X0)
| ~ c3_1(X0) ) ).
cnf(u2168,negated_conjecture,
( ~ ssSkP14(X0)
| ndr1_1(X0)
| ~ c6_1(X0) ) ).
cnf(u2192,negated_conjecture,
( ~ c7_2(X0,a66)
| c6_1(X0)
| c2_1(X0) ) ).
cnf(u2196,negated_conjecture,
( ~ c5_2(X0,a66)
| c6_1(X0)
| c2_1(X0) ) ).
cnf(u2200,negated_conjecture,
( ~ c1_2(X0,a66)
| c6_1(X0)
| c2_1(X0) ) ).
cnf(u2204,negated_conjecture,
( ~ c10_1(X0)
| c5_1(X0)
| c7_2(X0,a68) ) ).
cnf(u2208,negated_conjecture,
( ~ c10_1(X0)
| c5_1(X0)
| c3_2(X0,a68) ) ).
cnf(u2212,negated_conjecture,
( ~ c10_1(X0)
| c5_1(X0)
| c10_2(X0,a68) ) ).
cnf(u2220,negated_conjecture,
~ ssSkC13 ).
cnf(u2224,negated_conjecture,
( ~ c10_2(X0,a126)
| c9_1(X0)
| ~ ssSkP13(X0) ) ).
cnf(u2232,negated_conjecture,
( ~ c1_1(X0)
| c5_2(X0,a168)
| ~ ssSkP15(X0) ) ).
cnf(u2236,negated_conjecture,
( ~ c1_1(X0)
| c1_2(X0,a168)
| ~ ssSkP15(X0) ) ).
cnf(u2244,negated_conjecture,
( ~ c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u2248,negated_conjecture,
( c10_1(X0)
| c6_2(X0,a161) ) ).
cnf(u2252,negated_conjecture,
( c10_1(X0)
| c5_2(X0,a161) ) ).
cnf(u2256,negated_conjecture,
( c10_1(X0)
| c4_2(X0,a161) ) ).
cnf(u2308,negated_conjecture,
( ~ c10_1(X0)
| c5_1(X0)
| ndr1_1(X0) ) ).
cnf(u2316,negated_conjecture,
( ~ ssSkP13(X0)
| c9_1(X0)
| c4_2(X0,a126) ) ).
cnf(u2320,negated_conjecture,
( ~ ssSkP15(X0)
| ndr1_1(X0)
| ~ c1_1(X0) ) ).
cnf(u2336,negated_conjecture,
( c3_1(X0)
| c3_2(X0,a9) ) ).
cnf(u2344,negated_conjecture,
( c10_1(X0)
| ndr1_1(X0) ) ).
cnf(u2382,negated_conjecture,
( ndr1_1(X0)
| c6_1(X0)
| c2_1(X0) ) ).
cnf(u2386,negated_conjecture,
( ~ ssSkP13(X0)
| c9_1(X0)
| ndr1_1(X0) ) ).
cnf(u2394,negated_conjecture,
( c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u2419,negated_conjecture,
~ c7_2(a141,a142) ).
cnf(u2424,negated_conjecture,
~ c3_2(a141,a142) ).
cnf(u2429,negated_conjecture,
~ c10_2(a141,a142) ).
cnf(u2434,negated_conjecture,
~ c1_2(a152,a154) ).
cnf(u2468,negated_conjecture,
~ c5_2(a59,a60) ).
cnf(u2473,negated_conjecture,
~ c3_2(a59,a60) ).
cnf(u2478,negated_conjecture,
~ c1_2(a61,a62) ).
cnf(u2483,negated_conjecture,
~ c5_2(a61,a63) ).
cnf(u2488,negated_conjecture,
~ c10_2(a61,a63) ).
cnf(u2586,negated_conjecture,
ssSkC15 ).
cnf(u2601,negated_conjecture,
c9_1(a141) ).
cnf(u2607,negated_conjecture,
~ c5_2(a146,a147) ).
cnf(u2612,negated_conjecture,
c7_2(a152,a153) ).
cnf(u2617,negated_conjecture,
c6_2(a152,a153) ).
cnf(u2622,negated_conjecture,
c10_2(a152,a153) ).
cnf(u2627,negated_conjecture,
c8_2(a152,a154) ).
cnf(u2632,negated_conjecture,
c3_2(a152,a154) ).
cnf(u2637,negated_conjecture,
~ c9_1(a162) ).
cnf(u2642,negated_conjecture,
~ c10_1(a162) ).
cnf(u2647,negated_conjecture,
c9_2(a162,a163) ).
cnf(u2652,negated_conjecture,
c5_2(a162,a163) ).
cnf(u2657,negated_conjecture,
c2_2(a162,a163) ).
cnf(u2667,negated_conjecture,
~ c8_2(a183,a184) ).
cnf(u2672,negated_conjecture,
~ c6_2(a183,a184) ).
cnf(u2680,negated_conjecture,
~ c4_2(a1,a2) ).
cnf(u2685,negated_conjecture,
~ c7_2(a1,a3) ).
cnf(u2690,negated_conjecture,
~ c10_2(a1,a3) ).
cnf(u2695,negated_conjecture,
~ c8_2(a4,a5) ).
cnf(u2700,negated_conjecture,
~ c9_2(a4,a6) ).
cnf(u2705,negated_conjecture,
~ c2_2(a4,a6) ).
cnf(u2710,negated_conjecture,
~ c3_2(a7,a8) ).
cnf(u2715,negated_conjecture,
~ c10_2(a7,a8) ).
cnf(u2750,negated_conjecture,
~ c6_1(a19) ).
cnf(u2755,negated_conjecture,
~ c8_2(a29,a30) ).
cnf(u2758,negated_conjecture,
ssSkC1 ).
cnf(u2834,negated_conjecture,
~ c4_1(a59) ).
cnf(u2839,negated_conjecture,
c1_2(a59,a60) ).
cnf(u2844,negated_conjecture,
~ c6_1(a61) ).
cnf(u2849,negated_conjecture,
c3_2(a61,a62) ).
cnf(u3002,negated_conjecture,
~ c4_1(a146) ).
cnf(u3007,negated_conjecture,
c3_2(a146,a147) ).
cnf(u3012,negated_conjecture,
c10_2(a146,a147) ).
cnf(u3017,negated_conjecture,
ndr1_1(a152) ).
cnf(u3022,negated_conjecture,
~ c10_1(a160) ).
cnf(u3027,negated_conjecture,
ndr1_1(a162) ).
cnf(u3042,negated_conjecture,
~ c5_1(a174) ).
cnf(u3045,negated_conjecture,
ssSkC21 ).
cnf(u3051,negated_conjecture,
~ c3_1(a174) ).
cnf(u3056,negated_conjecture,
~ c6_1(a183) ).
cnf(u3061,negated_conjecture,
c1_2(a183,a184) ).
cnf(u3136,negated_conjecture,
~ c8_2(a213,a214) ).
cnf(u3141,negated_conjecture,
~ c6_2(a213,a214) ).
cnf(u3146,negated_conjecture,
~ c1_2(a213,a214) ).
cnf(u3154,negated_conjecture,
c9_2(a1,a2) ).
cnf(u3159,negated_conjecture,
c6_2(a1,a2) ).
cnf(u3164,negated_conjecture,
c7_2(a4,a5) ).
cnf(u3169,negated_conjecture,
c6_2(a4,a5) ).
cnf(u3174,negated_conjecture,
c6_2(a4,a6) ).
cnf(u3179,negated_conjecture,
c7_2(a7,a8) ).
cnf(u3214,negated_conjecture,
c4_1(a19) ).
cnf(u3219,negated_conjecture,
~ c2_1(a29) ).
cnf(u3224,negated_conjecture,
c7_2(a29,a30) ).
cnf(u3229,negated_conjecture,
c2_2(a29,a30) ).
cnf(u3291,negated_conjecture,
ndr1_1(a61) ).
cnf(u3301,negated_conjecture,
~ c6_1(a73) ).
cnf(u3311,negated_conjecture,
~ c3_1(a79) ).
cnf(u3392,negated_conjecture,
ndr1_1(a146) ).
cnf(u3541,negated_conjecture,
~ c9_1(a194) ).
cnf(u3546,negated_conjecture,
~ c2_1(a194) ).
cnf(u3561,negated_conjecture,
c4_1(a4) ).
cnf(u3566,negated_conjecture,
ndr1_1(a4) ).
cnf(u3578,negated_conjecture,
ndr1_1(a29) ).
cnf(u3616,negated_conjecture,
c4_1(a73) ).
cnf(u3808,negated_conjecture,
c8_1(a213) ).
cnf(u3989,negated_conjecture,
c5_2(a19,a125) ).
cnf(u3998,negated_conjecture,
ssSkP16(a19) ).
cnf(u4015,negated_conjecture,
~ c8_2(a188,a9) ).
cnf(u4041,negated_conjecture,
c3_2(a183,a9) ).
cnf(u4048,negated_conjecture,
~ c6_2(a1,a9) ).
cnf(u4061,negated_conjecture,
c1_2(a7,a9) ).
cnf(u4087,negated_conjecture,
~ c5_2(a7,a9) ).
cnf(u4090,negated_conjecture,
~ c4_2(a7,a9) ).
cnf(u4100,negated_conjecture,
~ ssSkP14(a160) ).
cnf(u4103,negated_conjecture,
c6_1(a160) ).
cnf(u4116,negated_conjecture,
~ c2_1(a160) ).
cnf(u4130,negated_conjecture,
ssSkP5(a160) ).
cnf(u4134,negated_conjecture,
c2_2(a160,a40) ).
cnf(u4144,negated_conjecture,
ssSkP9(a160) ).
cnf(u4162,negated_conjecture,
~ c4_2(a162,a163) ).
cnf(u4203,negated_conjecture,
~ c10_2(a164,a9) ).
cnf(u4211,negated_conjecture,
~ c9_1(a164) ).
cnf(u4216,negated_conjecture,
~ c10_2(a152,a154) ).
cnf(u4220,negated_conjecture,
~ c1_1(a152) ).
cnf(u4223,negated_conjecture,
c9_1(a152) ).
cnf(u4229,negated_conjecture,
~ c10_2(a174,a9) ).
cnf(u4233,negated_conjecture,
~ c1_1(a174) ).
cnf(u4237,negated_conjecture,
~ c9_1(a174) ).
cnf(u4242,negated_conjecture,
~ c10_2(a61,a62) ).
cnf(u4263,negated_conjecture,
~ c9_1(a79) ).
cnf(u4273,negated_conjecture,
~ c1_1(a183) ).
cnf(u4277,negated_conjecture,
~ c9_1(a183) ).
cnf(u4286,negated_conjecture,
~ c9_1(a146) ).
cnf(u4305,negated_conjecture,
~ c3_2(a152,a153) ).
cnf(u4309,negated_conjecture,
~ c3_1(a152) ).
cnf(u4317,negated_conjecture,
c2_1(a152) ).
cnf(u4322,negated_conjecture,
~ c3_2(a4,a5) ).
cnf(u4325,negated_conjecture,
c3_1(a4) ).
cnf(u4329,negated_conjecture,
~ c1_2(a4,a5) ).
cnf(u4333,negated_conjecture,
~ c2_1(a4) ).
cnf(u4340,negated_conjecture,
~ c3_2(a29,a30) ).
cnf(u4343,negated_conjecture,
c3_1(a29) ).
cnf(u4366,negated_conjecture,
~ c10_2(a4,a5) ).
cnf(u4374,negated_conjecture,
~ c9_1(a4) ).
cnf(u4383,negated_conjecture,
~ c5_1(a152) ).
cnf(u4387,negated_conjecture,
c2_2(a152,a153) ).
cnf(u4409,negated_conjecture,
~ c10_2(a188,a9) ).
cnf(u4426,negated_conjecture,
~ c2_1(a174) ).
cnf(u4439,negated_conjecture,
~ c2_1(a79) ).
cnf(u4453,negated_conjecture,
~ c2_1(a183) ).
cnf(u4466,negated_conjecture,
~ c2_1(a146) ).
cnf(u4484,negated_conjecture,
( ~ c5_2(a160,X0)
| c2_2(a160,X0)
| c9_2(a160,X0)
| ~ c10_2(a160,X0) ) ).
cnf(u4487,negated_conjecture,
~ c4_1(a160) ).
cnf(u4492,negated_conjecture,
c9_1(a160) ).
cnf(u4502,negated_conjecture,
~ c5_2(a183,a184) ).
cnf(u4526,negated_conjecture,
~ c6_2(a160,a52) ).
cnf(u4529,negated_conjecture,
( ~ c4_2(a160,X0)
| c2_2(a160,X0)
| c9_2(a160,X0)
| c7_2(a160,X0) ) ).
cnf(u4532,negated_conjecture,
~ c7_1(a160) ).
cnf(u4538,negated_conjecture,
~ c4_2(a59,a60) ).
cnf(u4542,negated_conjecture,
~ c6_2(a59,a52) ).
cnf(u4555,negated_conjecture,
~ c4_2(a183,a184) ).
cnf(u4559,negated_conjecture,
~ c6_2(a183,a52) ).
cnf(u4583,negated_conjecture,
c3_1(a160) ).
cnf(u4591,negated_conjecture,
( c4_2(a160,X0)
| c10_2(a160,X0)
| c9_2(a160,X0) ) ).
cnf(u4609,negated_conjecture,
~ c5_2(a188,a9) ).
cnf(u4622,negated_conjecture,
~ c5_2(a164,a9) ).
cnf(u4626,negated_conjecture,
~ c6_1(a164) ).
cnf(u4629,negated_conjecture,
~ c7_2(a164,a9) ).
cnf(u4641,negated_conjecture,
~ c5_2(a174,a9) ).
cnf(u4658,negated_conjecture,
~ c5_2(a79,a9) ).
cnf(u4661,negated_conjecture,
c6_1(a79) ).
cnf(u4666,negated_conjecture,
c7_2(a79,a9) ).
cnf(u4675,negated_conjecture,
~ c5_2(a160,a40) ).
cnf(u4688,negated_conjecture,
~ c6_1(a162) ).
cnf(u4719,negated_conjecture,
~ c5_2(a152,a153) ).
cnf(u4726,negated_conjecture,
~ c8_2(a152,a153) ).
cnf(u4733,negated_conjecture,
~ c5_2(a7,a8) ).
cnf(u4751,negated_conjecture,
~ c5_2(a4,a5) ).
cnf(u4755,negated_conjecture,
~ c2_2(a4,a198) ).
cnf(u4772,negated_conjecture,
~ c1_1(a29) ).
cnf(u4787,negated_conjecture,
~ c4_2(a152,a153) ).
cnf(u4800,negated_conjecture,
~ c4_2(a4,a6) ).
cnf(u4804,negated_conjecture,
~ ssSkP2(a4) ).
cnf(u4817,negated_conjecture,
~ c4_2(a4,a5) ).
cnf(u4865,negated_conjecture,
~ c8_2(a80,a55) ).
cnf(u4872,negated_conjecture,
~ c2_2(a80,a161) ).
cnf(u4876,negated_conjecture,
~ c8_2(a80,a161) ).
cnf(u4886,negated_conjecture,
~ c4_1(a152) ).
cnf(u4894,negated_conjecture,
~ c2_2(a160,a161) ).
cnf(u4908,negated_conjecture,
~ c4_1(a162) ).
cnf(u4915,negated_conjecture,
~ c8_2(a162,a161) ).
cnf(u4925,negated_conjecture,
~ c4_1(a1) ).
cnf(u4928,negated_conjecture,
~ c2_2(a1,a2) ).
cnf(u4942,negated_conjecture,
~ c8_2(a4,a55) ).
cnf(u4964,negated_conjecture,
~ ssSkP16(a164) ).
cnf(u4981,negated_conjecture,
~ ssSkP16(a160) ).
cnf(u4984,negated_conjecture,
c8_2(a160,a40) ).
cnf(u4998,negated_conjecture,
~ ssSkP16(a162) ).
cnf(u5019,negated_conjecture,
~ c8_2(a174,a9) ).
cnf(u5036,negated_conjecture,
~ c8_2(a79,a9) ).
cnf(u5039,negated_conjecture,
~ c1_2(a79,a9) ).
cnf(u5087,negated_conjecture,
~ c4_2(a188,a9) ).
cnf(u5104,negated_conjecture,
~ c4_2(a164,a9) ).
cnf(u5108,negated_conjecture,
~ c7_1(a164) ).
cnf(u5118,negated_conjecture,
~ c4_2(a174,a9) ).
cnf(u5121,negated_conjecture,
c7_1(a174) ).
cnf(u5132,negated_conjecture,
~ c4_2(a79,a9) ).
cnf(u5135,negated_conjecture,
c7_1(a79) ).
cnf(u5149,negated_conjecture,
~ c7_1(a146) ).
cnf(u5162,negated_conjecture,
~ c4_2(a152,a154) ).
cnf(u5165,negated_conjecture,
c7_1(a152) ).
cnf(u5179,negated_conjecture,
~ c7_1(a61) ).
cnf(u5230,negated_conjecture,
~ c9_2(a152,a153) ).
cnf(u5236,negated_conjecture,
~ ssSkP17(a160) ).
cnf(u5244,negated_conjecture,
c9_2(a160,a161) ).
cnf(u5253,negated_conjecture,
~ c10_2(a162,a209) ).
cnf(u5256,negated_conjecture,
~ c9_2(a162,a161) ).
cnf(u5263,negated_conjecture,
~ ssSkP17(a4) ).
cnf(u5267,negated_conjecture,
~ c10_2(a4,a209) ).
cnf(u5331,negated_conjecture,
c10_2(a160,a40) ).
cnf(u5341,negated_conjecture,
~ c10_2(a29,a30) ).
cnf(u5354,negated_conjecture,
c7_1(a29) ).
cnf(u5359,negated_conjecture,
c8_2(a188,a178) ).
cnf(u5365,negated_conjecture,
c8_2(a174,a178) ).
cnf(u5375,negated_conjecture,
c9_2(a164,a9) ).
cnf(u5395,negated_conjecture,
c5_2(a188,a178) ).
cnf(u5418,negated_conjecture,
c5_2(a1,a2) ).
cnf(u5432,negated_conjecture,
~ c9_2(a4,a5) ).
cnf(u5447,negated_conjecture,
~ c10_2(a80,a161) ).
cnf(u5463,negated_conjecture,
~ c9_1(a1) ).
cnf(u5587,negated_conjecture,
~ ssSkP4(a160) ).
cnf(u5590,negated_conjecture,
ssSkP3(a160) ).
cnf(u5625,negated_conjecture,
~ c2_2(a152,a154) ).
cnf(u5638,negated_conjecture,
~ c2_2(a61,a62) ).
cnf(u5642,negated_conjecture,
~ c8_2(a61,a144) ).
cnf(u5651,negated_conjecture,
~ c2_2(a146,a147) ).
cnf(u5655,negated_conjecture,
~ c8_2(a146,a144) ).
cnf(u5663,negated_conjecture,
~ c2_2(a183,a9) ).
cnf(u5676,negated_conjecture,
~ c8_2(a164,a144) ).
cnf(u5684,negated_conjecture,
~ c8_2(a174,a144) ).
cnf(u5687,negated_conjecture,
( ~ c1_2(a174,X0)
| c3_2(a174,X0) ) ).
cnf(u5692,negated_conjecture,
~ c8_2(a79,a144) ).
cnf(u5722,negated_conjecture,
c6_2(a164,a144) ).
cnf(u5755,negated_conjecture,
c10_2(a164,a144) ).
cnf(u5782,negated_conjecture,
c8_1(a160) ).
cnf(u5825,negated_conjecture,
( ~ c4_2(a174,X0)
| ~ c2_2(a174,X0)
| c6_2(a174,X0) ) ).
cnf(u5840,negated_conjecture,
~ ssSkP14(a79) ).
cnf(u5854,negated_conjecture,
~ ssSkP9(a79) ).
cnf(u5890,negated_conjecture,
( ~ c9_2(a162,X0)
| ~ c2_2(a162,X0)
| c5_2(a162,X0) ) ).
cnf(u5908,negated_conjecture,
c8_2(a146,a147) ).
cnf(u5919,negated_conjecture,
c8_1(a152) ).
cnf(u5933,negated_conjecture,
c7_2(a1,a2) ).
cnf(u5940,negated_conjecture,
( ~ c9_2(a162,X1)
| ~ c4_2(a162,X1) ) ).
cnf(u5968,negated_conjecture,
( ~ c7_2(a4,X0)
| ~ c1_2(a4,X0)
| c5_2(a4,X0) ) ).
cnf(u6011,negated_conjecture,
~ c3_2(a1,a2) ).
cnf(u6032,negated_conjecture,
~ c1_1(a1) ).
cnf(u6067,negated_conjecture,
c1_2(a80,a11) ).
cnf(u6076,negated_conjecture,
c1_2(a188,a11) ).
cnf(u6081,negated_conjecture,
c9_2(a160,a10) ).
cnf(u6085,negated_conjecture,
c1_2(a160,a11) ).
cnf(u6155,negated_conjecture,
c2_2(a160,a10) ).
cnf(u6171,negated_conjecture,
~ c4_2(a160,a156) ).
cnf(u6255,negated_conjecture,
c4_2(a162,a126) ).
cnf(u6260,negated_conjecture,
c4_2(a79,a125) ).
cnf(u6264,negated_conjecture,
c4_2(a79,a126) ).
cnf(u6269,negated_conjecture,
c4_2(a146,a125) ).
cnf(u6277,negated_conjecture,
~ c4_2(a183,a125) ).
cnf(u6282,negated_conjecture,
c4_2(a183,a126) ).
cnf(u6291,negated_conjecture,
c4_2(a194,a126) ).
cnf(u6296,negated_conjecture,
c4_2(a1,a125) ).
cnf(u6305,negated_conjecture,
c4_2(a4,a125) ).
cnf(u6309,negated_conjecture,
c4_2(a4,a126) ).
cnf(u6314,negated_conjecture,
c4_2(a29,a125) ).
cnf(u6318,negated_conjecture,
c4_2(a29,a126) ).
cnf(u6330,negated_conjecture,
~ c10_2(a160,a161) ).
cnf(u6339,negated_conjecture,
( c2_2(a152,X0)
| c5_2(a152,X0) ) ).
cnf(u6346,negated_conjecture,
c8_2(a188,a70) ).
cnf(u6355,negated_conjecture,
~ c2_1(a141) ).
cnf(u6360,negated_conjecture,
c3_1(a141) ).
cnf(u6364,negated_conjecture,
~ c8_2(a141,a70) ).
cnf(u6368,negated_conjecture,
( c4_2(a141,X0)
| c10_2(a141,X0)
| c9_2(a141,X0) ) ).
cnf(u6379,negated_conjecture,
( c4_2(a152,X0)
| c10_2(a152,X0)
| c9_2(a152,X0) ) ).
cnf(u6405,negated_conjecture,
c1_2(a141,a11) ).
cnf(u6430,negated_conjecture,
~ c10_1(a141) ).
cnf(u6496,negated_conjecture,
~ ssSkP4(a152) ).
cnf(u6501,negated_conjecture,
c5_2(a152,a25) ).
cnf(u6510,negated_conjecture,
c5_2(a152,a156) ).
cnf(u6518,negated_conjecture,
~ ssSkP16(a152) ).
cnf(u6568,negated_conjecture,
c1_2(a146,a125) ).
cnf(u6578,negated_conjecture,
c1_2(a1,a125) ).
cnf(u6602,negated_conjecture,
c4_2(a174,a161) ).
cnf(u6605,negated_conjecture,
~ c7_2(a174,a68) ).
cnf(u6618,negated_conjecture,
c8_2(a160,a156) ).
cnf(u6636,negated_conjecture,
c3_2(a174,a68) ).
cnf(u6653,negated_conjecture,
~ c8_2(a160,a65) ).
cnf(u6670,negated_conjecture,
c9_2(a160,a65) ).
cnf(u6680,negated_conjecture,
~ c5_2(a160,a65) ).
cnf(u6707,negated_conjecture,
c5_2(a174,a161) ).
cnf(u6715,negated_conjecture,
c6_2(a174,a161) ).
cnf(u6730,negated_conjecture,
~ c5_2(a4,a9) ).
cnf(u6733,negated_conjecture,
c6_1(a4) ).
cnf(u6738,negated_conjecture,
c7_2(a4,a9) ).
cnf(u6752,negated_conjecture,
~ ssSkP16(a4) ).
cnf(u6756,negated_conjecture,
~ c8_2(a4,a9) ).
cnf(u6759,negated_conjecture,
~ c1_2(a4,a9) ).
cnf(u6768,negated_conjecture,
~ c10_2(a4,a9) ).
cnf(u6780,negated_conjecture,
~ c7_1(a4) ).
cnf(u6845,negated_conjecture,
c8_1(a4) ).
cnf(u6880,negated_conjecture,
ssSkP12(a141) ).
cnf(u6892,negated_conjecture,
ssSkP0(a141) ).
cnf(u6897,negated_conjecture,
c9_2(a141,a11) ).
cnf(u6906,negated_conjecture,
ssSkP3(a141) ).
cnf(u6919,negated_conjecture,
c10_2(a141,a41) ).
cnf(u6945,negated_conjecture,
c7_2(a160,a161) ).
cnf(u6957,negated_conjecture,
~ ssSkP4(a141) ).
cnf(u6977,negated_conjecture,
~ ssSkP14(a4) ).
cnf(u6991,negated_conjecture,
~ ssSkP9(a4) ).
cnf(u7013,negated_conjecture,
~ c5_2(a29,a9) ).
cnf(u7016,negated_conjecture,
c6_1(a29) ).
cnf(u7021,negated_conjecture,
c7_2(a29,a9) ).
cnf(u7039,negated_conjecture,
~ c8_2(a29,a9) ).
cnf(u7072,negated_conjecture,
~ c4_2(a29,a9) ).
cnf(u7124,negated_conjecture,
~ ssSkP14(a29) ).
cnf(u7138,negated_conjecture,
~ ssSkP9(a29) ).
cnf(u7170,negated_conjecture,
( ~ c7_2(a79,X0)
| ~ c1_2(a79,X0)
| c5_2(a79,X0) ) ).
cnf(u7193,negated_conjecture,
~ c4_2(a4,a22) ).
cnf(u7216,negated_conjecture,
~ c3_2(a4,a22) ).
cnf(u7232,negated_conjecture,
~ c9_2(a162,a176) ).
cnf(u7249,negated_conjecture,
~ c4_2(a162,a176) ).
cnf(u7291,negated_conjecture,
~ c5_2(a4,a208) ).
cnf(u7367,negated_conjecture,
~ ssSkP17(a188) ).
cnf(u7398,negated_conjecture,
~ c4_1(a188) ).
cnf(u7401,negated_conjecture,
~ c2_2(a188,a161) ).
cnf(u7412,negated_conjecture,
~ c10_2(a188,a161) ).
cnf(u7449,negated_conjecture,
~ c9_2(a164,a144) ).
cnf(u7453,negated_conjecture,
c5_2(a164,a144) ).
cnf(u7462,negated_conjecture,
~ c4_2(a164,a144) ).
cnf(u7495,negated_conjecture,
~ c8_2(a164,a55) ).
cnf(u7516,negated_conjecture,
c4_2(a164,a125) ).
cnf(u7525,negated_conjecture,
c1_2(a164,a125) ).
cnf(u7541,negated_conjecture,
~ c10_2(a80,a11) ).
cnf(u7555,negated_conjecture,
~ c4_2(a188,a11) ).
cnf(u7594,negated_conjecture,
~ c5_2(a146,a125) ).
cnf(u7603,negated_conjecture,
c7_2(a146,a125) ).
cnf(u7631,negated_conjecture,
c7_1(a1) ).
cnf(u7645,negated_conjecture,
~ c5_2(a1,a125) ).
cnf(u7663,negated_conjecture,
~ c4_2(a174,a68) ).
cnf(u7719,negated_conjecture,
c4_2(a174,a126) ).
cnf(u7749,negated_conjecture,
~ c8_2(a174,a161) ).
cnf(u7752,negated_conjecture,
~ c9_2(a174,a161) ).
cnf(u7772,negated_conjecture,
~ c8_2(a174,a55) ).
cnf(u7779,negated_conjecture,
~ c2_2(a174,a161) ).
cnf(u7790,negated_conjecture,
( ~ c9_2(a174,X0)
| ~ c2_2(a174,X0)
| c5_2(a174,X0) ) ).
cnf(u7798,negated_conjecture,
~ c5_2(a141,a11) ).
cnf(u7826,negated_conjecture,
c8_1(a141) ).
cnf(u7876,negated_conjecture,
ssSkP12(a160) ).
cnf(u7889,negated_conjecture,
~ ssSkP0(a160) ).
cnf(u7893,negated_conjecture,
c9_2(a160,a11) ).
cnf(u7911,negated_conjecture,
c10_2(a160,a41) ).
cnf(u8003,negated_conjecture,
c10_2(a152,a123) ).
cnf(u8009,negated_conjecture,
ssSkP3(a152) ).
cnf(u8013,negated_conjecture,
c9_2(a152,a24) ).
cnf(u8018,negated_conjecture,
ssSkP6(a152) ).
cnf(u8045,negated_conjecture,
~ c2_2(a195,a24) ).
cnf(u8062,negated_conjecture,
c3_2(a174,a24) ).
cnf(u8075,negated_conjecture,
~ c5_2(a7,a24) ).
cnf(u8130,negated_conjecture,
~ c9_2(a164,a176) ).
cnf(u8139,negated_conjecture,
~ c4_2(a164,a176) ).
cnf(u8169,negated_conjecture,
~ c5_2(a160,a208) ).
cnf(u8186,negated_conjecture,
~ c4_2(a160,a11) ).
cnf(u8204,negated_conjecture,
~ c5_2(a160,a10) ).
cnf(u8229,negated_conjecture,
~ c2_2(a152,a68) ).
cnf(u8245,negated_conjecture,
~ c4_2(a152,a68) ).
cnf(u8267,negated_conjecture,
( ~ c6_2(a152,X1)
| ~ c5_2(a152,X1)
| ~ c10_2(a152,X1) ) ).
cnf(u8291,negated_conjecture,
~ c2_2(a152,a9) ).
cnf(u8310,negated_conjecture,
c9_2(a152,a9) ).
cnf(u8315,negated_conjecture,
~ c4_2(a152,a9) ).
cnf(u8340,negated_conjecture,
~ ssSkP17(a141) ).
cnf(u8371,negated_conjecture,
~ c4_1(a141) ).
cnf(u8381,negated_conjecture,
~ c10_2(a141,a161) ).
cnf(u8412,negated_conjecture,
~ c4_2(a152,a176) ).
cnf(u8415,negated_conjecture,
~ c5_2(a152,a176) ).
cnf(u8427,negated_conjecture,
~ c9_2(a152,a176) ).
cnf(u8467,negated_conjecture,
~ c1_2(a4,a26) ).
cnf(u8510,negated_conjecture,
~ c5_1(a29) ).
cnf(u8514,negated_conjecture,
~ c9_1(a29) ).
cnf(u8523,negated_conjecture,
~ c3_2(a29,a9) ).
cnf(u8539,negated_conjecture,
c1_2(a29,a11) ).
cnf(u8566,negated_conjecture,
~ c10_2(a29,a11) ).
cnf(u8573,negated_conjecture,
~ c4_1(a29) ).
cnf(u8631,negated_conjecture,
c1_2(a4,a11) ).
cnf(u8662,negated_conjecture,
~ c4_2(a4,a11) ).
cnf(u8693,negated_conjecture,
c4_2(a160,a176) ).
cnf(u8698,negated_conjecture,
~ ssSkP2(a160) ).
cnf(u8701,negated_conjecture,
~ c5_2(a160,a176) ).
cnf(u8715,negated_conjecture,
c2_2(a160,a176) ).
cnf(u8719,negated_conjecture,
c9_2(a160,a176) ).
cnf(u8726,negated_conjecture,
~ c10_2(a160,a176) ).
cnf(u8732,negated_conjecture,
c9_2(a160,a25) ).
cnf(u8754,negated_conjecture,
~ c5_2(a164,a125) ).
cnf(u8765,negated_conjecture,
c7_2(a164,a125) ).
cnf(u8786,negated_conjecture,
~ c2_2(a174,a126) ).
cnf(u8796,negated_conjecture,
( ~ c9_2(a174,X1)
| ~ c4_2(a174,X1) ) ).
cnf(u8825,negated_conjecture,
( ~ c2_2(a152,X0)
| c10_2(a152,X0) ) ).
cnf(u8834,negated_conjecture,
~ c4_2(a152,a24) ).
cnf(u8855,negated_conjecture,
~ c4_2(a174,a24) ).
cnf(u8886,negated_conjecture,
~ c8_2(a29,a161) ).
cnf(u8912,negated_conjecture,
~ c2_2(a29,a161) ).
cnf(u8945,negated_conjecture,
~ c2_2(a4,a161) ).
cnf(u8998,negated_conjecture,
~ c3_2(a160,a161) ).
cnf(u9022,negated_conjecture,
~ c1_2(a79,a26) ).
cnf(u9048,negated_conjecture,
~ c4_2(a79,a156) ).
cnf(u9079,negated_conjecture,
ssSkP8(a160) ).
cnf(u9097,negated_conjecture,
c2_2(a160,a78) ).
cnf(u9105,negated_conjecture,
c10_2(a160,a78) ).
cnf(u9114,negated_conjecture,
( ~ c5_2(a160,X0)
| c10_2(a160,X0)
| c7_2(a160,X0)
| c2_2(a160,X0)
| c6_2(a160,X0) ) ).
cnf(u9122,negated_conjecture,
c2_2(a160,a77) ).
cnf(u9130,negated_conjecture,
c10_2(a160,a77) ).
cnf(u9181,negated_conjecture,
c5_2(a79,a156) ).
cnf(u9188,negated_conjecture,
( ~ c8_2(a79,X0)
| c9_2(a79,X0)
| c4_2(a79,X0) ) ).
cnf(u9231,negated_conjecture,
~ c4_2(a141,a25) ).
cnf(u9306,negated_conjecture,
~ c2_2(a4,a176) ).
cnf(u9346,negated_conjecture,
~ c5_2(a188,a208) ).
cnf(u9382,negated_conjecture,
~ c8_2(a188,a208) ).
cnf(u9405,negated_conjecture,
~ c4_2(a160,a10) ).
cnf(u9418,negated_conjecture,
~ c5_2(a160,a11) ).
cnf(u9476,negated_conjecture,
~ c2_2(a146,a9) ).
cnf(u9489,negated_conjecture,
~ c2_2(a1,a9) ).
cnf(u9497,negated_conjecture,
~ c8_2(a1,a144) ).
cnf(u9506,negated_conjecture,
~ c2_2(a59,a9) ).
cnf(u9510,negated_conjecture,
~ c8_2(a59,a144) ).
cnf(u9684,negated_conjecture,
~ c2_2(a194,a9) ).
cnf(u9881,negated_conjecture,
~ c5_2(a160,a25) ).
cnf(u10002,negated_conjecture,
~ c2_2(a162,a9) ).
cnf(u10111,negated_conjecture,
~ c3_2(a29,a26) ).
cnf(u10126,negated_conjecture,
~ c1_2(a7,a8) ).
cnf(u10151,negated_conjecture,
~ c3_2(a164,a26) ).
cnf(u10171,negated_conjecture,
~ c3_2(a146,a26) ).
cnf(u10204,negated_conjecture,
~ c5_2(a160,a78) ).
cnf(u10226,negated_conjecture,
~ c5_2(a160,a77) ).
cnf(u10482,negated_conjecture,
~ c4_2(a29,a156) ).
cnf(u10485,negated_conjecture,
~ c1_2(a29,a156) ).
cnf(u10496,negated_conjecture,
c5_2(a29,a156) ).
cnf(u10529,negated_conjecture,
c8_2(a29,a64) ).
cnf(u10569,negated_conjecture,
~ c5_2(a141,a208) ).
cnf(u10621,negated_conjecture,
~ ssSkP16(a141) ).
cnf(u10683,negated_conjecture,
~ c3_2(a160,a22) ).
cnf(u10702,negated_conjecture,
~ c5_1(a160) ).
cnf(u10732,negated_conjecture,
c10_2(a141,a25) ).
cnf(u10812,negated_conjecture,
c7_2(a183,a126) ).
cnf(u10917,negated_conjecture,
~ c4_2(a141,a176) ).
cnf(u10924,negated_conjecture,
~ c5_2(a141,a176) ).
cnf(u10940,negated_conjecture,
~ c10_2(a141,a176) ).
cnf(u10969,negated_conjecture,
~ c3_2(a183,a26) ).
cnf(u9854,negated_conjecture,
( ~ c2_2(X0,a9)
| c6_2(X0,a144)
| c3_2(X0,a24)
| c7_2(X0,a9)
| c2_2(X0,a10)
| c1_2(X0,a11)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(u7977,negated_conjecture,
( ~ c10_2(X0,a9)
| c1_2(X0,a11)
| c8_1(X0)
| c9_2(X0,a9)
| ~ c2_1(X0)
| c1_2(X0,a10) ) ).
cnf(u7185,negated_conjecture,
c10_2(a29,a156) ).
cnf(u10388,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_2(X0,a161)
| c4_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u7153,negated_conjecture,
c3_2(a4,a156) ).
cnf(u5975,negated_conjecture,
c10_2(a79,a156) ).
cnf(u10322,negated_conjecture,
( c4_2(X0,a126)
| c1_2(X0,a125)
| c4_2(X0,a161)
| c4_2(X0,a151) ) ).
cnf(clause289,negated_conjecture,
( ~ c4_2(X0,a41)
| ssSkP6(X0) ) ).
cnf(u8105,negated_conjecture,
( ~ c10_1(X0)
| c4_2(X0,a126)
| c2_1(X0)
| c1_2(X0,a125) ) ).
cnf(u7960,negated_conjecture,
( ~ c1_2(X0,X1)
| c1_2(X0,a11)
| c10_2(X0,a144)
| c3_2(X0,X1)
| c7_2(X0,a9)
| c2_2(X0,a10)
| ~ c2_2(X0,a9) ) ).
cnf(clause295,negated_conjecture,
( ~ c2_2(X0,a25)
| ssSkP4(X0) ) ).
cnf(u10551,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c4_2(X0,a125)
| c7_2(X0,a68) ) ).
cnf(u10377,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a151)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_1(X0)
| c4_2(X0,a125)
| ~ c2_2(X0,a9)
| c5_2(X0,a161) ) ).
cnf(u9905,negated_conjecture,
( ~ c2_2(X0,a9)
| c10_2(X0,a144)
| c3_2(X0,a24)
| c7_2(X0,a9)
| c1_2(X0,a10)
| c1_2(X0,a11)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(u7980,negated_conjecture,
( ~ c1_2(X0,X1)
| c1_2(X0,a11)
| c3_2(X0,X1)
| c7_2(X0,a9)
| ~ c8_2(X0,a144)
| c1_2(X0,a10)
| ~ c2_2(X0,a9) ) ).
cnf(u4150,negated_conjecture,
~ c2_2(a160,a156) ).
cnf(u4841,negated_conjecture,
~ c5_2(a4,a22) ).
cnf(u7324,negated_conjecture,
~ c8_2(a160,a176) ).
cnf(clause166,negated_conjecture,
( ssSkP13(X0)
| c4_2(X0,a125) ) ).
cnf(u9516,negated_conjecture,
( ~ c2_2(X0,a9)
| c7_2(X0,a9)
| c6_2(X0,a144)
| c3_2(X0,a24)
| c5_2(X0,a161)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(u9437,negated_conjecture,
c5_2(a152,a9) ).
cnf(clause189,negated_conjecture,
( ssSkP0(X0)
| c1_2(X0,a10) ) ).
cnf(u9277,negated_conjecture,
( c10_1(X0)
| c4_2(X0,a125)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1) ) ).
cnf(u10431,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_2(X0,a161)
| c1_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(clause179,negated_conjecture,
( ssSkP5(X0)
| c3_2(X0,a40) ) ).
cnf(u6590,negated_conjecture,
~ c8_2(a152,a176) ).
cnf(u10288,negated_conjecture,
( c4_2(X0,a126)
| c4_2(X0,a125)
| c5_2(X0,a161)
| c4_2(X0,a151) ) ).
cnf(clause78,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(u7840,negated_conjecture,
( ~ c4_2(X0,a9)
| c8_2(X0,a204)
| c1_2(X0,a9)
| ~ c7_1(X0)
| c6_2(X0,a161) ) ).
cnf(u3924,negated_conjecture,
c6_2(a160,a161) ).
cnf(clause177,negated_conjecture,
( ssSkP7(X0)
| c3_2(X0,a53) ) ).
cnf(clause76,negated_conjecture,
( ssSkP9(X0)
| ndr1_1(X0) ) ).
cnf(u9291,negated_conjecture,
( c10_1(X0)
| c4_2(X0,a125)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1) ) ).
cnf(u10534,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c4_2(X0,a125)
| c3_2(X0,a68) ) ).
cnf(u8034,negated_conjecture,
( ~ c5_2(X0,a26)
| c1_2(X0,a25)
| c1_2(X0,a198)
| c8_2(X0,a26)
| ~ c1_1(X0)
| c1_2(X0,a24) ) ).
cnf(u10598,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,a125)
| c10_2(X0,a68) ) ).
cnf(u7934,negated_conjecture,
( ~ c1_2(X0,X1)
| c1_2(X0,a11)
| c6_2(X0,a144)
| c3_2(X0,X1)
| c7_2(X0,a9)
| c9_2(X0,a10)
| ~ c2_2(X0,a9) ) ).
cnf(u9446,negated_conjecture,
c10_2(a152,a176) ).
cnf(u4845,negated_conjecture,
c9_2(a4,a22) ).
cnf(u10737,negated_conjecture,
~ c6_2(a152,a68) ).
cnf(u3935,negated_conjecture,
c4_2(a162,a161) ).
cnf(u10578,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,a125)
| c3_2(X0,a68) ) ).
cnf(u9786,negated_conjecture,
( ~ c2_2(X0,a9)
| c6_2(X0,a144)
| c3_2(X0,a24)
| c7_2(X0,a9)
| c9_2(X0,a10)
| c1_2(X0,a11)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(u3931,negated_conjecture,
c5_2(a80,a161) ).
cnf(u10350,negated_conjecture,
~ c10_2(a183,a126) ).
cnf(u9339,negated_conjecture,
( c10_1(X0)
| c1_2(X0,a125)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1) ) ).
cnf(u8649,negated_conjecture,
c5_2(a4,a161) ).
cnf(u7173,negated_conjecture,
~ c1_2(a4,a64) ).
cnf(u7270,negated_conjecture,
~ c7_2(a160,a78) ).
cnf(u8392,negated_conjecture,
c2_2(a141,a208) ).
cnf(u8587,negated_conjecture,
~ c5_2(a162,a66) ).
cnf(u8030,negated_conjecture,
( ~ c3_2(X0,a26)
| c1_2(X0,a25)
| c2_1(X0)
| c1_2(X0,a26)
| ~ c3_1(X0)
| c1_2(X0,a24) ) ).
cnf(u5083,negated_conjecture,
( ~ c4_2(X0,a9)
| c1_2(X0,a9)
| ~ c7_1(X0)
| c8_2(X0,a204)
| c5_2(X0,a161) ) ).
cnf(u3872,negated_conjecture,
ndr1_1(X0) ).
cnf(u10408,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_2(X0,a161)
| c4_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u7669,negated_conjecture,
~ c10_1(a174) ).
cnf(u7423,negated_conjecture,
c2_2(a188,a208) ).
cnf(clause73,negated_conjecture,
( ssSkP11(X0)
| ndr1_1(X0) ) ).
cnf(u7325,negated_conjecture,
~ c7_2(a160,a176) ).
cnf(u10272,negated_conjecture,
c2_2(a152,a176) ).
cnf(clause279,negated_conjecture,
( ~ c4_2(X0,a123)
| ssSkP12(X0) ) ).
cnf(clause284,negated_conjecture,
( ~ c1_2(X0,a64)
| ssSkP9(X0) ) ).
cnf(u10301,negated_conjecture,
( c4_2(X0,a126)
| c4_2(X0,a125)
| c6_2(X0,a161)
| c4_2(X0,a151) ) ).
cnf(u7958,negated_conjecture,
( ~ c4_2(X0,a9)
| c1_2(X0,a11)
| c8_2(X0,a204)
| c1_2(X0,a9)
| ~ c7_1(X0)
| c2_2(X0,a10) ) ).
cnf(u7936,negated_conjecture,
( ~ c4_2(X0,X1)
| c1_2(X0,a11)
| c6_1(X0)
| c6_2(X0,X1)
| c9_2(X0,a9)
| c9_2(X0,a10)
| ~ c2_2(X0,X1)
| ~ c2_2(X0,a9) ) ).
cnf(u10655,negated_conjecture,
c6_2(a141,a176) ).
cnf(u6950,negated_conjecture,
~ c6_2(a141,a11) ).
cnf(u7962,negated_conjecture,
( ~ c1_2(X0,X1)
| c1_2(X0,a11)
| c3_2(X0,X1)
| c7_2(X0,a9)
| ~ c8_2(X0,a144)
| c2_2(X0,a10)
| ~ c2_2(X0,a9) ) ).
cnf(u8033,negated_conjecture,
( ~ c5_2(X0,a26)
| c1_2(X0,a25)
| c4_2(X0,a198)
| c8_2(X0,a26)
| ~ c1_1(X0)
| c1_2(X0,a24) ) ).
cnf(u6443,negated_conjecture,
c10_2(a152,a68) ).
cnf(u8588,negated_conjecture,
~ c1_2(a162,a66) ).
cnf(clause150,negated_conjecture,
( ssSkP16(X0)
| c6_2(X0,a176) ) ).
cnf(clause274,negated_conjecture,
( ~ c2_2(X0,a156)
| ssSkP14(X0) ) ).
cnf(u7172,negated_conjecture,
~ c9_2(a4,a64) ).
cnf(u9804,negated_conjecture,
( ~ c2_2(X0,a9)
| c3_2(X0,a24)
| c7_2(X0,a9)
| ~ c8_2(X0,a144)
| c9_2(X0,a10)
| c1_2(X0,a11)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(u6594,negated_conjecture,
c6_2(a152,a176) ).
cnf(u6199,negated_conjecture,
( c3_1(X0)
| c4_2(X0,a125)
| c4_2(X0,a126)
| c2_1(X0) ) ).
cnf(u9028,negated_conjecture,
( c2_1(X0)
| c4_2(X0,a126)
| c4_2(X0,a125)
| c4_2(X0,a161) ) ).
cnf(clause60,negated_conjecture,
( ssSkP15(X0)
| ndr1_1(X0) ) ).
cnf(u4155,negated_conjecture,
c10_2(a160,a156) ).
cnf(clause190,negated_conjecture,
( ssSkP0(X0)
| c2_2(X0,a10) ) ).
cnf(u7869,negated_conjecture,
( c7_2(a160,X0)
| c9_2(a160,X0)
| c2_2(a160,X0)
| c10_2(a160,X0) ) ).
cnf(clause188,negated_conjecture,
( ssSkP1(X0)
| c6_2(X0,a17) ) ).
cnf(u7859,negated_conjecture,
( ~ c1_2(X0,X1)
| c10_2(X0,a144)
| c3_2(X0,X1)
| c7_2(X0,a9)
| c6_2(X0,a161)
| ~ c2_2(X0,a9) ) ).
cnf(u7856,negated_conjecture,
( ~ c1_2(X0,X1)
| c3_2(X0,X1)
| c7_2(X0,a9)
| c6_2(X0,a144)
| ~ c2_2(X0,a9)
| c5_2(X0,a161) ) ).
cnf(u9169,negated_conjecture,
~ c5_2(a160,a22) ).
cnf(u10784,negated_conjecture,
( ~ c2_2(X0,a126)
| c4_2(X0,a161)
| c4_2(X0,a151)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_1(X0)
| c4_2(X0,a125)
| ~ c2_2(X0,a9)
| c5_2(X0,a161) ) ).
cnf(u8090,negated_conjecture,
( ~ c6_2(X0,a52)
| c1_2(X0,a25)
| c7_1(X0)
| c7_2(X0,a24)
| c6_2(X0,a26)
| ~ c4_2(X0,a24) ) ).
cnf(clause178,negated_conjecture,
( ssSkP6(X0)
| c6_2(X0,a41) ) ).
cnf(u7857,negated_conjecture,
( ~ c1_2(X0,X1)
| c3_2(X0,X1)
| c7_2(X0,a9)
| c10_2(X0,a144)
| ~ c2_2(X0,a9)
| c5_2(X0,a161) ) ).
cnf(u9580,negated_conjecture,
( ~ c2_2(X0,a9)
| c3_2(X0,a24)
| c7_2(X0,a9)
| c6_2(X0,a161)
| c10_2(X0,a144)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(u6484,negated_conjecture,
c5_2(a152,a154) ).
cnf(u5573,negated_conjecture,
c6_2(a188,a161) ).
cnf(u5974,negated_conjecture,
c3_2(a79,a156) ).
cnf(u10855,negated_conjecture,
( ~ c2_2(X0,a126)
| c5_2(X0,a161)
| c4_2(X0,a151)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_1(X0)
| c1_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(clause79,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(u8031,negated_conjecture,
( ~ c10_2(X0,a26)
| c1_2(X0,a25)
| c2_2(X0,a26)
| ~ c9_1(X0)
| ~ c5_1(X0)
| c1_2(X0,a24) ) ).
cnf(u5978,negated_conjecture,
~ c1_2(a79,a64) ).
cnf(u10865,negated_conjecture,
( ~ c2_2(X0,a126)
| c6_2(X0,a161)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c1_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u8035,negated_conjecture,
( ~ c7_2(X0,X1)
| c1_2(X0,a25)
| c4_2(X0,a26)
| c5_2(X0,X1)
| ~ c10_2(X0,X2)
| ~ c3_2(X0,a26)
| c1_2(X0,a24)
| ~ c1_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c5_2(X0,X2) ) ).
cnf(u10394,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c9_2(X0,a10)
| c4_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u3957,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,a11)
| c9_2(X0,a10) ) ).
cnf(u5571,negated_conjecture,
c4_2(a188,a161) ).
cnf(u10840,negated_conjecture,
( ~ c2_2(X0,a126)
| c4_2(X0,a161)
| c4_2(X0,a151)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_1(X0)
| c1_2(X0,a125)
| ~ c2_2(X0,a9)
| c5_2(X0,a161) ) ).
cnf(u5735,negated_conjecture,
~ c7_2(a164,a176) ).
cnf(u7110,negated_conjecture,
~ c2_2(a141,a25) ).
cnf(u3961,negated_conjecture,
( c9_1(X0)
| c4_2(X0,a126)
| c4_2(X0,a125) ) ).
cnf(u10444,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a151)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_1(X0)
| c1_2(X0,a125)
| ~ c2_2(X0,a9)
| c5_2(X0,a161) ) ).
cnf(u10353,negated_conjecture,
( c4_2(X0,a126)
| c1_2(X0,a125)
| c6_2(X0,a161)
| c4_2(X0,a151) ) ).
cnf(u6387,negated_conjecture,
c4_2(a152,a151) ).
cnf(u8391,negated_conjecture,
c4_2(a141,a208) ).
cnf(u10450,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c1_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u10637,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,a125)
| c10_2(X0,a68) ) ).
cnf(u3958,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,a11)
| c2_2(X0,a10) ) ).
cnf(u4072,negated_conjecture,
( c5_1(X0)
| c7_2(X0,a68)
| c5_2(X0,a161) ) ).
cnf(u3962,negated_conjecture,
( c9_1(X0)
| c4_2(X0,a126)
| c1_2(X0,a125) ) ).
cnf(u6383,negated_conjecture,
~ c6_2(a152,a151) ).
cnf(u9768,negated_conjecture,
( ~ c2_2(X0,a9)
| c10_2(X0,a144)
| c3_2(X0,a24)
| c7_2(X0,a9)
| c9_2(X0,a10)
| c1_2(X0,a11)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(clause285,negated_conjecture,
( ~ c9_2(X0,a64)
| ssSkP9(X0) ) ).
cnf(u10409,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a151)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_1(X0)
| c4_2(X0,a125)
| ~ c2_2(X0,a9)
| c5_2(X0,a161) ) ).
cnf(clause298,negated_conjecture,
( ~ c4_2(X0,a24)
| ssSkP3(X0) ) ).
cnf(u10735,negated_conjecture,
~ c7_2(a4,a55) ).
cnf(u3892,negated_conjecture,
~ c10_1(a80) ).
cnf(clause84,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(u7976,negated_conjecture,
( ~ c4_2(X0,a9)
| c1_2(X0,a11)
| c8_2(X0,a204)
| c1_2(X0,a9)
| ~ c7_1(X0)
| c1_2(X0,a10) ) ).
cnf(u3890,negated_conjecture,
( ~ c3_2(X0,a78)
| c2_2(X0,X1)
| ~ c6_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u7975,negated_conjecture,
( ~ c4_2(X0,a9)
| c1_2(X0,a11)
| c4_2(X0,a204)
| c1_2(X0,a9)
| ~ c7_1(X0)
| c1_2(X0,a10) ) ).
cnf(clause174,negated_conjecture,
( ssSkP9(X0)
| c10_2(X0,a64) ) ).
cnf(clause296,negated_conjecture,
( ~ c6_2(X0,a25)
| ssSkP4(X0) ) ).
cnf(clause291,negated_conjecture,
( ~ c1_2(X0,a40)
| ssSkP5(X0) ) ).
cnf(u8104,negated_conjecture,
( c2_1(X0)
| c4_2(X0,a126)
| c1_2(X0,a125)
| c1_2(X0,a11)
| c9_2(X0,a10) ) ).
cnf(u9279,negated_conjecture,
( c4_2(X0,a126)
| c4_2(X0,a125)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a151) ) ).
cnf(u10389,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a151)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_1(X0)
| c4_2(X0,a125)
| ~ c2_2(X0,a9)
| c5_2(X0,a161) ) ).
cnf(clause172,negated_conjecture,
( ssSkP10(X0)
| c6_2(X0,a93) ) ).
cnf(u5302,negated_conjecture,
c2_2(a4,a208) ).
cnf(u7963,negated_conjecture,
( ~ c4_2(X0,X1)
| c1_2(X0,a11)
| c6_1(X0)
| c6_2(X0,X1)
| c9_2(X0,a9)
| c2_2(X0,a10)
| ~ c2_2(X0,X1)
| ~ c2_2(X0,a9) ) ).
cnf(clause57,negated_conjecture,
( ssSkP16(X0)
| ndr1_1(X0) ) ).
cnf(clause187,negated_conjecture,
( ssSkP1(X0)
| c2_2(X0,a17) ) ).
cnf(u7983,negated_conjecture,
c9_2(a152,a154) ).
cnf(u3889,negated_conjecture,
( ~ c7_2(X0,a78)
| c2_2(X0,X1)
| ~ c6_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u5300,negated_conjecture,
c9_2(a4,a208) ).
cnf(u8091,negated_conjecture,
( ~ c4_2(X0,a24)
| c1_2(X0,a25)
| c7_1(X0)
| c2_2(X0,a52)
| c7_2(X0,a24)
| c6_2(X0,a26) ) ).
cnf(clause63,negated_conjecture,
( ssSkP14(X0)
| ndr1_1(X0) ) ).
cnf(u7858,negated_conjecture,
( ~ c4_2(X0,X1)
| c6_2(X0,X1)
| c9_2(X0,a9)
| c6_1(X0)
| ~ c2_2(X0,X1)
| ~ c2_2(X0,a9)
| c5_2(X0,a161) ) ).
cnf(clause185,negated_conjecture,
( ssSkP2(X0)
| c9_2(X0,a22) ) ).
cnf(u7855,negated_conjecture,
( ~ c1_2(X0,X1)
| c7_2(X0,a9)
| ~ c8_2(X0,a144)
| c3_2(X0,X1)
| ~ c2_2(X0,a9)
| c5_2(X0,a161) ) ).
cnf(u9059,negated_conjecture,
( c2_1(X0)
| c4_2(X0,a126)
| c1_2(X0,a125)
| c4_2(X0,a161) ) ).
cnf(u9030,negated_conjecture,
( c2_1(X0)
| c4_2(X0,a126)
| c4_2(X0,a125)
| c6_2(X0,a161) ) ).
cnf(clause191,negated_conjecture,
( ssSkP0(X0)
| c9_2(X0,a10) ) ).
cnf(u9824,negated_conjecture,
( ~ c2_2(X0,a9)
| c10_2(X0,a144)
| c3_2(X0,a24)
| c7_2(X0,a9)
| c2_2(X0,a10)
| c1_2(X0,a11)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(u9428,negated_conjecture,
c5_2(a152,a68) ).
cnf(u10599,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,a125)
| c3_2(X0,a68) ) ).
cnf(clause74,negated_conjecture,
( ssSkP10(X0)
| ndr1_1(X0) ) ).
cnf(u10437,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c9_2(X0,a10)
| c1_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u6550,negated_conjecture,
( c8_2(X0,a70)
| c1_2(X0,a125)
| c9_2(X0,X1)
| c4_2(X0,X1)
| c10_2(X0,X1)
| c4_2(X0,a126) ) ).
cnf(u5597,negated_conjecture,
~ c6_2(a160,a25) ).
cnf(u10461,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c1_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u5970,negated_conjecture,
~ c2_2(a79,a156) ).
cnf(u3945,negated_conjecture,
c3_2(a164,a9) ).
cnf(u7113,negated_conjecture,
c1_2(a141,a25) ).
cnf(u6551,negated_conjecture,
( c3_1(X0)
| c1_2(X0,a125)
| c4_2(X0,a126)
| c2_1(X0) ) ).
cnf(u3959,negated_conjecture,
( ~ c3_1(X0)
| c1_2(X0,a11)
| c1_2(X0,a10) ) ).
cnf(u10254,negated_conjecture,
( c10_2(a152,X0)
| c5_2(a152,X0) ) ).
cnf(u7943,negated_conjecture,
c1_2(a160,a10) ).
cnf(u4073,negated_conjecture,
( c5_1(X0)
| c7_2(X0,a68)
| c6_2(X0,a161) ) ).
cnf(u5595,negated_conjecture,
( ~ ssSkP4(X0)
| c7_2(X0,a26)
| c1_2(X0,a24) ) ).
cnf(clause175,negated_conjecture,
( ssSkP8(X0)
| c4_2(X0,a57) ) ).
cnf(u7421,negated_conjecture,
c9_2(a188,a208) ).
cnf(u3942,negated_conjecture,
( ~ c10_1(X0)
| c3_2(X0,a9) ) ).
cnf(u10506,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c4_2(X0,a125)
| c10_2(X0,a68) ) ).
cnf(u8032,negated_conjecture,
( ~ c2_2(X0,a198)
| c1_2(X0,a25)
| c8_2(X0,a26)
| ~ c1_1(X0)
| c1_2(X0,a24)
| ~ c5_2(X0,a26) ) ).
cnf(u7929,negated_conjecture,
( ~ c10_2(X0,a9)
| c1_2(X0,a11)
| ~ c9_1(X0)
| ~ c1_1(X0)
| c9_2(X0,a10) ) ).
cnf(u7180,negated_conjecture,
~ c2_2(a29,a156) ).
cnf(u4076,negated_conjecture,
( c5_1(X0)
| c3_2(X0,a68)
| c5_2(X0,a161) ) ).
cnf(clause287,negated_conjecture,
( ~ c9_2(X0,a57)
| ssSkP8(X0) ) ).
cnf(u4080,negated_conjecture,
( c5_1(X0)
| c10_2(X0,a68)
| c5_2(X0,a161) ) ).
cnf(u3870,negated_conjecture,
( ~ c1_1(X0)
| ndr1_1(X0) ) ).
cnf(u8446,negated_conjecture,
~ c1_2(a4,a22) ).
cnf(u7149,negated_conjecture,
~ c2_2(a4,a156) ).
cnf(u6788,negated_conjecture,
( c7_2(X0,a26)
| c1_2(X0,a24)
| c1_2(X0,a25) ) ).
cnf(clause158,negated_conjecture,
( ssSkP14(X0)
| c10_2(X0,a156) ) ).
cnf(u7931,negated_conjecture,
( ~ c4_2(X0,a9)
| c1_2(X0,a11)
| c8_2(X0,a204)
| c1_2(X0,a9)
| ~ c7_1(X0)
| c9_2(X0,a10) ) ).
cnf(u10550,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c4_2(X0,a125)
| c3_2(X0,a68) ) ).
cnf(u9263,negated_conjecture,
( c10_1(X0)
| c4_2(X0,a125)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1) ) ).
cnf(u4199,negated_conjecture,
( ~ c10_2(X0,a9)
| ~ c1_1(X0)
| ~ c9_1(X0)
| c5_2(X0,a161) ) ).
cnf(u7328,negated_conjecture,
c6_2(a160,a176) ).
cnf(u4405,negated_conjecture,
( ~ c10_2(X0,a9)
| c9_2(X0,a9)
| ~ c2_1(X0)
| c8_1(X0)
| c5_2(X0,a161) ) ).
cnf(u3869,negated_conjecture,
( ~ c6_1(X0)
| ndr1_1(X0) ) ).
cnf(u7841,negated_conjecture,
( ~ c10_2(X0,a9)
| c8_1(X0)
| c9_2(X0,a9)
| ~ c2_1(X0)
| c6_2(X0,a161) ) ).
cnf(clause171,negated_conjecture,
( ssSkP10(X0)
| c1_2(X0,a93) ) ).
cnf(u10783,negated_conjecture,
( ~ c2_2(X0,a126)
| c4_2(X0,a161)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_2(X0,a161)
| c4_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u7979,negated_conjecture,
( ~ c1_2(X0,X1)
| c1_2(X0,a11)
| c6_2(X0,a144)
| c3_2(X0,X1)
| c7_2(X0,a9)
| c1_2(X0,a10)
| ~ c2_2(X0,a9) ) ).
cnf(u6198,negated_conjecture,
( c8_2(X0,a70)
| c4_2(X0,a125)
| c9_2(X0,X1)
| c4_2(X0,X1)
| c10_2(X0,X1)
| c4_2(X0,a126) ) ).
cnf(u7861,negated_conjecture,
( ~ c1_2(X0,X1)
| c3_2(X0,X1)
| c7_2(X0,a9)
| ~ c8_2(X0,a144)
| c6_2(X0,a161)
| ~ c2_2(X0,a9) ) ).
cnf(u3887,negated_conjecture,
( ~ c9_2(X0,X1)
| c3_1(X0)
| c6_2(X0,X1)
| ~ c4_2(X0,X1) ) ).
cnf(u7570,negated_conjecture,
~ c9_2(a162,a126) ).
cnf(u6471,negated_conjecture,
c6_2(a141,a161) ).
cnf(u7109,negated_conjecture,
~ c6_2(a141,a25) ).
cnf(u10432,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a151)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_1(X0)
| c1_2(X0,a125)
| ~ c2_2(X0,a9)
| c5_2(X0,a161) ) ).
cnf(clause186,negated_conjecture,
( ssSkP1(X0)
| c1_2(X0,a17) ) ).
cnf(u6469,negated_conjecture,
c4_2(a141,a161) ).
cnf(u9265,negated_conjecture,
( c4_2(X0,a126)
| c4_2(X0,a125)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a151) ) ).
cnf(u5065,negated_conjecture,
c6_2(a162,a176) ).
cnf(u8103,negated_conjecture,
( c2_1(X0)
| c4_2(X0,a126)
| c1_2(X0,a125)
| c1_2(X0,a11)
| c2_2(X0,a10) ) ).
cnf(u3925,negated_conjecture,
c6_2(a80,a161) ).
cnf(u7176,negated_conjecture,
c10_2(a4,a64) ).
cnf(clause184,negated_conjecture,
( ssSkP2(X0)
| c7_2(X0,a22) ) ).
cnf(u3923,negated_conjecture,
c6_2(a162,a161) ).
cnf(u7200,negated_conjecture,
~ c1_2(a29,a64) ).
cnf(clause87,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(u3929,negated_conjecture,
c5_2(a162,a161) ).
cnf(u3943,negated_conjecture,
c3_2(a79,a9) ).
cnf(clause85,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u7974,negated_conjecture,
( ~ c10_2(X0,a9)
| c1_2(X0,a11)
| ~ c9_1(X0)
| ~ c1_1(X0)
| c1_2(X0,a10) ) ).
cnf(u5598,negated_conjecture,
~ c2_2(a160,a25) ).
cnf(u8390,negated_conjecture,
c9_2(a141,a208) ).
cnf(u3930,negated_conjecture,
c5_2(a160,a161) ).
cnf(u10337,negated_conjecture,
( c4_2(X0,a126)
| c1_2(X0,a125)
| c5_2(X0,a161)
| c4_2(X0,a151) ) ).
cnf(u3936,negated_conjecture,
c4_2(a160,a161) ).
cnf(u10507,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c4_2(X0,a125)
| c3_2(X0,a68) ) ).
cnf(u10449,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c9_2(X0,a10)
| c1_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u8557,negated_conjecture,
c6_2(a29,a161) ).
cnf(u9174,negated_conjecture,
c7_2(a160,a22) ).
cnf(u10456,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a151)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_1(X0)
| c1_2(X0,a125)
| ~ c2_2(X0,a9)
| c5_2(X0,a161) ) ).
cnf(clause269,negated_conjecture,
( ~ c7_2(X0,a176)
| ssSkP16(X0) ) ).
cnf(u10549,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c4_2(X0,a125)
| c10_2(X0,a68) ) ).
cnf(u10638,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,a125)
| c3_2(X0,a68) ) ).
cnf(u6804,negated_conjecture,
c1_2(a152,a25) ).
cnf(u9450,negated_conjecture,
( ~ c2_2(X0,a9)
| ~ c8_2(X0,a144)
| c3_2(X0,a24)
| c7_2(X0,a9)
| c5_2(X0,a161)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(u8094,negated_conjecture,
( c2_1(X0)
| c4_2(X0,a126)
| c4_2(X0,a125)
| c1_2(X0,a11)
| c9_2(X0,a10) ) ).
cnf(clause282,negated_conjecture,
( ~ c10_2(X0,a109)
| ssSkP11(X0) ) ).
cnf(clause140,negated_conjecture,
( ssSkP17(X0)
| c9_2(X0,a208) ) ).
cnf(u10740,negated_conjecture,
~ c6_2(a160,a156) ).
cnf(u10508,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c4_2(X0,a125)
| c7_2(X0,a68) ) ).
cnf(u7839,negated_conjecture,
( ~ c4_2(X0,a9)
| c4_2(X0,a204)
| c1_2(X0,a9)
| ~ c7_1(X0)
| c6_2(X0,a161) ) ).
cnf(u3871,negated_conjecture,
( c9_1(X0)
| ndr1_1(X0) ) ).
cnf(clause153,negated_conjecture,
( ssSkP15(X0)
| c10_2(X0,a167) ) ).
cnf(clause299,negated_conjecture,
( ~ c5_2(X0,a22)
| ssSkP2(X0) ) ).
cnf(clause286,negated_conjecture,
( ~ c5_2(X0,a57)
| ssSkP8(X0) ) ).
cnf(u6801,negated_conjecture,
~ c2_2(a152,a25) ).
cnf(u9371,negated_conjecture,
( c10_1(X0)
| c1_2(X0,a125)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1) ) ).
cnf(u4154,negated_conjecture,
c3_2(a160,a156) ).
cnf(clause159,negated_conjecture,
( ssSkP14(X0)
| c3_2(X0,a156) ) ).
cnf(clause297,negated_conjecture,
( ~ c10_2(X0,a24)
| ssSkP3(X0) ) ).
cnf(u9029,negated_conjecture,
( c2_1(X0)
| c4_2(X0,a126)
| c4_2(X0,a125)
| c5_2(X0,a161) ) ).
cnf(u8585,negated_conjecture,
~ c2_1(a162) ).
cnf(u7864,negated_conjecture,
( c9_2(a160,X0)
| c10_2(a160,X0)
| c6_2(a160,X0)
| c2_2(a160,X0) ) ).
cnf(u6445,negated_conjecture,
c7_2(a152,a68) ).
cnf(clause170,negated_conjecture,
( ssSkP11(X0)
| c5_2(X0,a109) ) ).
cnf(u10414,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c4_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u7334,negated_conjecture,
c6_2(a4,a176) ).
cnf(u5805,negated_conjecture,
c9_2(a160,a208) ).
cnf(clause168,negated_conjecture,
( ssSkP12(X0)
| c7_2(X0,a123) ) ).
cnf(u10577,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,a125)
| c10_2(X0,a68) ) ).
cnf(u5601,negated_conjecture,
c1_2(a160,a25) ).
cnf(clause69,negated_conjecture,
( ssSkP12(X0)
| ndr1_1(X0) ) ).
cnf(clause80,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u4024,negated_conjecture,
( c4_2(X0,a161)
| c3_2(X0,a9) ) ).
cnf(u9949,negated_conjecture,
( ~ c2_2(X0,a9)
| c3_2(X0,a24)
| c7_2(X0,a9)
| ~ c8_2(X0,a144)
| c1_2(X0,a10)
| c1_2(X0,a11)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(u9923,negated_conjecture,
( ~ c2_2(X0,a9)
| c6_2(X0,a144)
| c3_2(X0,a24)
| c7_2(X0,a9)
| c1_2(X0,a10)
| c1_2(X0,a11)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(clause86,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u5981,negated_conjecture,
c10_2(a79,a64) ).
cnf(u8093,negated_conjecture,
( c2_1(X0)
| c4_2(X0,a126)
| c4_2(X0,a125)
| c1_2(X0,a11)
| c2_2(X0,a10) ) ).
cnf(u5985,negated_conjecture,
~ c7_2(a183,a66) ).
cnf(u10533,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c4_2(X0,a125)
| c10_2(X0,a68) ) ).
cnf(u9325,negated_conjecture,
( c10_1(X0)
| c1_2(X0,a125)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1) ) ).
cnf(u10535,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c4_2(X0,a125)
| c7_2(X0,a68) ) ).
cnf(u7930,negated_conjecture,
( ~ c4_2(X0,a9)
| c1_2(X0,a11)
| c4_2(X0,a204)
| c1_2(X0,a9)
| ~ c7_1(X0)
| c9_2(X0,a10) ) ).
cnf(u8531,negated_conjecture,
~ c10_1(a29) ).
cnf(u10579,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,a125)
| c7_2(X0,a68) ) ).
cnf(u7956,negated_conjecture,
( ~ c10_2(X0,a9)
| c1_2(X0,a11)
| ~ c9_1(X0)
| ~ c1_1(X0)
| c2_2(X0,a10) ) ).
cnf(u7933,negated_conjecture,
( ~ c1_2(X0,X1)
| c1_2(X0,a11)
| c10_2(X0,a144)
| c3_2(X0,X1)
| c7_2(X0,a9)
| c9_2(X0,a10)
| ~ c2_2(X0,a9) ) ).
cnf(clause139,negated_conjecture,
( ssSkP17(X0)
| c4_2(X0,a208) ) ).
cnf(u6806,negated_conjecture,
( c1_2(X0,a24)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(u6949,negated_conjecture,
~ c4_2(a141,a11) ).
cnf(u11016,negated_conjecture,
c9_2(a141,a176) ).
cnf(u9251,negated_conjecture,
( c4_2(X0,a126)
| c4_2(X0,a125)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a151) ) ).
cnf(u10382,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c9_2(X0,a10)
| c4_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u6381,negated_conjecture,
c10_1(a152) ).
cnf(clause283,negated_conjecture,
( ~ c3_2(X0,a109)
| ssSkP11(X0) ) ).
cnf(u7838,negated_conjecture,
( ~ c10_2(X0,a9)
| ~ c9_1(X0)
| ~ c1_1(X0)
| c6_2(X0,a161) ) ).
cnf(clause270,negated_conjecture,
( ~ c8_2(X0,a176)
| ssSkP16(X0) ) ).
cnf(u6444,negated_conjecture,
c3_2(a152,a68) ).
cnf(u10639,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,a125)
| c7_2(X0,a68) ) ).
cnf(u10252,negated_conjecture,
~ c4_2(a183,a66) ).
cnf(u8616,negated_conjecture,
~ c3_2(a4,a9) ).
cnf(u6800,negated_conjecture,
~ c6_2(a152,a25) ).
cnf(u8095,negated_conjecture,
( ~ c10_1(X0)
| c4_2(X0,a126)
| c2_1(X0)
| c4_2(X0,a125) ) ).
cnf(clause154,negated_conjecture,
( ssSkP15(X0)
| c8_2(X0,a167) ) ).
cnf(u7862,negated_conjecture,
( ~ c4_2(X0,X1)
| c6_1(X0)
| c6_2(X0,X1)
| c9_2(X0,a9)
| c6_2(X0,a161)
| ~ c2_2(X0,X1)
| ~ c2_2(X0,a9) ) ).
cnf(u9552,negated_conjecture,
( ~ c2_2(X0,a9)
| c7_2(X0,a9)
| c10_2(X0,a144)
| c3_2(X0,a24)
| c5_2(X0,a161)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(u4021,negated_conjecture,
( ~ c6_2(X0,a70)
| c4_2(X0,X1)
| c10_2(X0,X1)
| ~ c9_1(X0)
| c9_2(X0,X1) ) ).
cnf(u6591,negated_conjecture,
~ c7_2(a152,a176) ).
cnf(clause152,negated_conjecture,
( ssSkP15(X0)
| c1_2(X0,a167) ) ).
cnf(u7330,negated_conjecture,
~ c8_2(a4,a176) ).
cnf(u10395,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c4_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u9608,negated_conjecture,
( ~ c2_2(X0,a9)
| c3_2(X0,a24)
| c7_2(X0,a9)
| c6_2(X0,a161)
| c6_2(X0,a144)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(clause183,negated_conjecture,
( ssSkP3(X0)
| c1_2(X0,a24) ) ).
cnf(u4025,negated_conjecture,
( c3_2(X0,a9)
| c5_2(X0,a161) ) ).
cnf(u9887,negated_conjecture,
( ~ c2_2(X0,a9)
| c3_2(X0,a24)
| c7_2(X0,a9)
| ~ c8_2(X0,a144)
| c2_2(X0,a10)
| c1_2(X0,a11)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(u10384,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c4_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u5807,negated_conjecture,
c2_2(a160,a208) ).
cnf(u5806,negated_conjecture,
c4_2(a160,a208) ).
cnf(u7978,negated_conjecture,
( ~ c1_2(X0,X1)
| c1_2(X0,a11)
| c10_2(X0,a144)
| c3_2(X0,X1)
| c7_2(X0,a9)
| c1_2(X0,a10)
| ~ c2_2(X0,a9) ) ).
cnf(u10839,negated_conjecture,
( ~ c2_2(X0,a126)
| c4_2(X0,a161)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_2(X0,a161)
| c1_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u10652,negated_conjecture,
~ c7_2(a141,a176) ).
cnf(u5402,negated_conjecture,
( ~ c6_2(X0,X1)
| c5_1(X0)
| c3_1(X0)
| c5_2(X0,X1)
| ~ c9_2(X0,X1) ) ).
cnf(u4022,negated_conjecture,
( ~ c10_2(X0,a70)
| c4_2(X0,X1)
| c10_2(X0,X1)
| ~ c9_1(X0)
| c9_2(X0,X1) ) ).
cnf(u4026,negated_conjecture,
( c3_2(X0,a9)
| c6_2(X0,a161) ) ).
cnf(u5404,negated_conjecture,
~ c10_1(a188) ).
cnf(u4182,negated_conjecture,
~ c7_2(a160,a65) ).
cnf(u10845,negated_conjecture,
~ c7_2(a29,a156) ).
cnf(u7271,negated_conjecture,
~ c3_2(a160,a78) ).
cnf(clause68,negated_conjecture,
( ssSkP13(X0)
| ndr1_1(X0) ) ).
cnf(u10600,negated_conjecture,
( c5_1(X0)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a126)
| c9_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,a125)
| c7_2(X0,a68) ) ).
cnf(u5983,negated_conjecture,
~ c1_2(a183,a66) ).
cnf(u8102,negated_conjecture,
( c2_1(X0)
| c4_2(X0,a126)
| c1_2(X0,a125)
| c1_2(X0,a11)
| c1_2(X0,a10) ) ).
cnf(clause83,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(u7269,negated_conjecture,
~ c9_2(a160,a78) ).
cnf(u8650,negated_conjecture,
c6_2(a4,a161) ).
cnf(u5977,negated_conjecture,
~ c9_2(a79,a64) ).
cnf(u5572,negated_conjecture,
c5_2(a188,a161) ).
cnf(u10383,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c2_2(X0,a10)
| c4_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u9061,negated_conjecture,
( c2_1(X0)
| c4_2(X0,a126)
| c1_2(X0,a125)
| c6_2(X0,a161) ) ).
cnf(u5062,negated_conjecture,
~ c7_2(a162,a176) ).
cnf(u9313,negated_conjecture,
( c4_2(X0,a126)
| c1_2(X0,a125)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a151) ) ).
cnf(u8586,negated_conjecture,
~ c7_2(a162,a66) ).
cnf(u10439,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c1_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u4178,negated_conjecture,
c4_2(a160,a65) ).
cnf(u9060,negated_conjecture,
( c2_1(X0)
| c4_2(X0,a126)
| c1_2(X0,a125)
| c5_2(X0,a161) ) ).
cnf(u9359,negated_conjecture,
( c4_2(X0,a126)
| c1_2(X0,a125)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a151) ) ).
cnf(u8555,negated_conjecture,
c4_2(a29,a161) ).
cnf(u7935,negated_conjecture,
( ~ c1_2(X0,X1)
| c1_2(X0,a11)
| c3_2(X0,X1)
| c7_2(X0,a9)
| ~ c8_2(X0,a144)
| c9_2(X0,a10)
| ~ c2_2(X0,a9) ) ).
cnf(u4071,negated_conjecture,
( c5_1(X0)
| c7_2(X0,a68)
| c4_2(X0,a161) ) ).
cnf(u4077,negated_conjecture,
( c5_1(X0)
| c3_2(X0,a68)
| c6_2(X0,a161) ) ).
cnf(u4075,negated_conjecture,
( c5_1(X0)
| c3_2(X0,a68)
| c4_2(X0,a161) ) ).
cnf(u5734,negated_conjecture,
~ c8_2(a164,a176) ).
cnf(u4081,negated_conjecture,
( c5_1(X0)
| c10_2(X0,a68)
| c6_2(X0,a161) ) ).
cnf(u6453,negated_conjecture,
c3_2(a152,a9) ).
cnf(u6147,negated_conjecture,
( c3_2(X0,a9)
| c2_2(X0,a10)
| c1_2(X0,a11) ) ).
cnf(u7957,negated_conjecture,
( ~ c4_2(X0,a9)
| c1_2(X0,a11)
| c4_2(X0,a204)
| c1_2(X0,a9)
| ~ c7_1(X0)
| c2_2(X0,a10) ) ).
cnf(clause288,negated_conjecture,
( ~ c6_2(X0,a53)
| ssSkP7(X0) ) ).
cnf(clause278,negated_conjecture,
( ~ c8_2(X0,a125)
| ssSkP13(X0) ) ).
cnf(clause138,negated_conjecture,
( ssSkP17(X0)
| c2_2(X0,a208) ) ).
cnf(u7961,negated_conjecture,
( ~ c1_2(X0,X1)
| c1_2(X0,a11)
| c6_2(X0,a144)
| c3_2(X0,X1)
| c7_2(X0,a9)
| c2_2(X0,a10)
| ~ c2_2(X0,a9) ) ).
cnf(u10443,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_2(X0,a161)
| c1_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u7981,negated_conjecture,
( ~ c4_2(X0,X1)
| c1_2(X0,a11)
| c6_1(X0)
| c6_2(X0,X1)
| c9_2(X0,a9)
| c1_2(X0,a10)
| ~ c2_2(X0,X1)
| ~ c2_2(X0,a9) ) ).
cnf(u7199,negated_conjecture,
~ c9_2(a29,a64) ).
cnf(clause77,negated_conjecture,
( ssSkP8(X0)
| ndr1_1(X0) ) ).
cnf(u10334,negated_conjecture,
ssSkP13(a183) ).
cnf(clause167,negated_conjecture,
( ssSkP12(X0)
| c1_2(X0,a123) ) ).
cnf(u7203,negated_conjecture,
c10_2(a29,a64) ).
cnf(clause48,negated_conjecture,
( ssSkP17(X0)
| ndr1_1(X0) ) ).
cnf(clause290,negated_conjecture,
( ~ c9_2(X0,a41)
| ssSkP6(X0) ) ).
cnf(u9626,negated_conjecture,
( ~ c2_2(X0,a9)
| c7_2(X0,a9)
| ~ c8_2(X0,a144)
| c6_2(X0,a161)
| c3_2(X0,a24)
| c6_2(X0,a26)
| c1_2(X0,a25) ) ).
cnf(u7860,negated_conjecture,
( ~ c1_2(X0,X1)
| c6_2(X0,a144)
| c3_2(X0,X1)
| c7_2(X0,a9)
| c6_2(X0,a161)
| ~ c2_2(X0,a9) ) ).
cnf(clause165,negated_conjecture,
( ssSkP13(X0)
| c1_2(X0,a125) ) ).
cnf(u8623,negated_conjecture,
~ c10_1(a4) ).
cnf(u9173,negated_conjecture,
c9_2(a160,a22) ).
cnf(u7331,negated_conjecture,
~ c7_2(a4,a176) ).
cnf(u10240,negated_conjecture,
~ c9_2(a174,a126) ).
cnf(u10366,negated_conjecture,
c1_2(a183,a126) ).
cnf(clause176,negated_conjecture,
( ssSkP7(X0)
| c1_2(X0,a53) ) ).
cnf(u7184,negated_conjecture,
c3_2(a29,a156) ).
cnf(u6055,negated_conjecture,
( c3_2(X0,a9)
| c9_2(X0,a10)
| c1_2(X0,a11) ) ).
cnf(u7425,negated_conjecture,
~ c4_2(a160,a25) ).
cnf(u10651,negated_conjecture,
~ c8_2(a141,a176) ).
cnf(clause182,negated_conjecture,
( ssSkP4(X0)
| c1_2(X0,a25) ) ).
cnf(u10376,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_2(X0,a161)
| c4_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u4023,negated_conjecture,
( ~ c9_1(X0)
| c9_2(X0,X1)
| c4_2(X0,X1)
| c10_2(X0,X1)
| c8_2(X0,a70) ) ).
cnf(u5301,negated_conjecture,
c4_2(a4,a208) ).
cnf(u6335,negated_conjecture,
~ c1_1(a160) ).
cnf(clause180,negated_conjecture,
( ssSkP5(X0)
| c5_2(X0,a40) ) ).
cnf(u8556,negated_conjecture,
c5_2(a29,a161) ).
cnf(u4179,negated_conjecture,
c2_2(a160,a65) ).
cnf(u6470,negated_conjecture,
c5_2(a141,a161) ).
cnf(u8092,negated_conjecture,
( c2_1(X0)
| c4_2(X0,a126)
| c4_2(X0,a125)
| c1_2(X0,a11)
| c1_2(X0,a10) ) ).
cnf(u8089,negated_conjecture,
( ~ c5_2(X0,a24)
| c1_2(X0,a25)
| c9_1(X0)
| c4_1(X0)
| c6_2(X0,a26)
| ~ c10_2(X0,a24) ) ).
cnf(u5194,negated_conjecture,
( ~ c4_2(X0,a9)
| c1_2(X0,a9)
| ~ c7_1(X0)
| c4_2(X0,a204)
| c5_2(X0,a161) ) ).
cnf(u3944,negated_conjecture,
c3_2(a174,a9) ).
cnf(u10823,negated_conjecture,
( ~ c2_2(X0,a126)
| c5_2(X0,a161)
| c4_2(X0,a151)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_1(X0)
| c4_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u5061,negated_conjecture,
~ c8_2(a162,a176) ).
cnf(u9327,negated_conjecture,
( c4_2(X0,a126)
| c1_2(X0,a125)
| c1_2(X0,a11)
| c2_2(X0,a10)
| c4_2(X0,a151) ) ).
cnf(u10455,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c9_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c6_2(X0,a161)
| c1_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u10833,negated_conjecture,
( ~ c2_2(X0,a126)
| c6_2(X0,a161)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c4_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u10438,negated_conjecture,
( ~ c2_2(X0,a126)
| c1_2(X0,a11)
| c1_2(X0,a10)
| c4_2(X0,a151)
| c6_1(X0)
| c6_2(X0,a126)
| c9_2(X0,a9)
| c2_2(X0,a10)
| c1_2(X0,a125)
| ~ c2_2(X0,a9) ) ).
cnf(u8648,negated_conjecture,
c4_2(a4,a161) ).
cnf(u3937,negated_conjecture,
c4_2(a80,a161) ).
cnf(u6384,negated_conjecture,
~ c9_2(a152,a151) ).
cnf(u5984,negated_conjecture,
~ c5_2(a183,a66) ).
cnf(u7154,negated_conjecture,
c10_2(a4,a156) ).
cnf(u4079,negated_conjecture,
( c5_1(X0)
| c10_2(X0,a68)
| c4_2(X0,a161) ) ).
cnf(u7932,negated_conjecture,
( ~ c10_2(X0,a9)
| c1_2(X0,a11)
| c8_1(X0)
| c9_2(X0,a9)
| ~ c2_1(X0)
| c9_2(X0,a10) ) ).
cnf(u5603,negated_conjecture,
( ~ ssSkP4(X0)
| c6_2(X0,a26)
| c1_2(X0,a24) ) ).
cnf(u4846,negated_conjecture,
c7_2(a4,a22) ).
cnf(u10099,negated_conjecture,
( ~ c3_2(X0,a26)
| c4_2(X0,a26)
| c5_2(X0,a26)
| ~ c10_2(X0,X1)
| c1_2(X0,a25)
| c1_2(X0,a24)
| ~ c1_2(X0,a26)
| ~ c6_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u5738,negated_conjecture,
c6_2(a164,a176) ).
cnf(u7422,negated_conjecture,
c4_2(a188,a208) ).
cnf(u7959,negated_conjecture,
( ~ c10_2(X0,a9)
| c1_2(X0,a11)
| c8_1(X0)
| c9_2(X0,a9)
| ~ c2_1(X0)
| c2_2(X0,a10) ) ).
cnf(u6193,negated_conjecture,
( c3_2(X0,a9)
| c1_2(X0,a10)
| c1_2(X0,a11) ) ).
cnf(u10275,negated_conjecture,
( c4_2(X0,a126)
| c4_2(X0,a125)
| c4_2(X0,a161)
| c4_2(X0,a151) ) ).
cnf(u3888,negated_conjecture,
( ~ c9_2(X0,a78)
| c2_2(X0,X1)
| ~ c6_1(X0)
| ~ c9_2(X0,X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN429-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.19 % Computer : n014.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 15:57:01 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 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
% 7.99/1.68 % (1897322)Input is clausal, will run a generic CNF schedule.
% 7.99/1.68 % (1897333)dis-21_1_sil=8000:lcm=predicate:random_seed=3535335284:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 7.99/1.68 % (1897331)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2345797255:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.99/1.68 % (1897332)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1580866850:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.99/1.68 % (1897328)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=815281352:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.99/1.68 % (1897327)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=485402275:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.99/1.68 % (1897329)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1105687474:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.99/1.68 % (1897330)lrs+10_1_sil=8000:sp=occurrence:random_seed=3862451473:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.99/1.68 % (1897333)Instruction limit reached!
% 7.99/1.68 % (1897333)------------------------------
% 7.99/1.68 % (1897333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.99/1.68 % (1897333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.68 % (1897333)CaDiCaL version: 2.1.3
% 7.99/1.68 % (1897333)Termination reason: Instruction limit
% 7.99/1.68 % (1897333)Termination phase: Saturation
% 7.99/1.68 % (1897333)Time elapsed: 0.036 s
% 7.99/1.68 % (1897333)Peak memory usage: 92 MB
% 7.99/1.68 % (1897333)Instructions burned: 117 (million)
% 7.99/1.68 % (1897332)Refutation not found, incomplete strategy
% 7.99/1.68 % (1897332)------------------------------
% 7.99/1.68 % (1897332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.99/1.68 % (1897332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.68 % (1897332)CaDiCaL version: 2.1.3
% 7.99/1.68 % (1897332)Termination reason: Refutation not found, incomplete strategy
% 7.99/1.68 % (1897332)Time elapsed: 0.049 s
% 7.99/1.68 % (1897332)Peak memory usage: 91 MB
% 7.99/1.68 % (1897332)Instructions burned: 83 (million)
% 7.99/1.68 % (1897330)Instruction limit reached!
% 7.99/1.68 % (1897330)------------------------------
% 7.99/1.68 % (1897330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.99/1.68 % (1897330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.68 % (1897330)CaDiCaL version: 2.1.3
% 7.99/1.68 % (1897330)Termination reason: Instruction limit
% 7.99/1.68 % (1897330)Termination phase: Saturation
% 7.99/1.68 % (1897330)Time elapsed: 0.062 s
% 7.99/1.68 % (1897330)Peak memory usage: 91 MB
% 7.99/1.68 % (1897330)Instructions burned: 107 (million)
% 7.99/1.68 % (1897331)Instruction limit reached!
% 7.99/1.68 % (1897331)------------------------------
% 7.99/1.68 % (1897331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.99/1.68 % (1897331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.68 % (1897331)CaDiCaL version: 2.1.3
% 7.99/1.68 % (1897331)Termination reason: Instruction limit
% 7.99/1.68 % (1897331)Termination phase: Saturation
% 7.99/1.68 % (1897331)Time elapsed: 0.066 s
% 7.99/1.68 % (1897331)Peak memory usage: 91 MB
% 7.99/1.68 % (1897331)Instructions burned: 116 (million)
% 7.99/1.68 % (1897341)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=233180768:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 7.99/1.68 % (1897341)Instruction limit reached!
% 7.99/1.68 % (1897341)------------------------------
% 7.99/1.68 % (1897341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.99/1.68 % (1897341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.68 % (1897341)CaDiCaL version: 2.1.3
% 7.99/1.68 % (1897341)Termination reason: Instruction limit
% 7.99/1.68 % (1897341)Termination phase: Saturation
% 7.99/1.68 % (1897341)Time elapsed: 0.044 s
% 7.99/1.68 % (1897341)Peak memory usage: 92 MB
% 7.99/1.68 % (1897341)Instructions burned: 144 (million)
% 7.99/1.68 % (1897343)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1789617975:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.04/2.05 % (1897342)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=465487501:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 11.04/2.05 % (1897345)lrs+10_64_to=lpo:sil=8000:random_seed=2405820489:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 11.04/2.05 % (1897342)Refutation not found, incomplete strategy
% 11.04/2.05 % (1897342)------------------------------
% 11.04/2.05 % (1897342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.05 % (1897342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.05 % (1897342)CaDiCaL version: 2.1.3
% 11.04/2.05 % (1897342)Termination reason: Refutation not found, incomplete strategy
% 11.04/2.05 % (1897342)Time elapsed: 0.051 s
% 11.04/2.05 % (1897342)Peak memory usage: 91 MB
% 11.04/2.05 % (1897342)Instructions burned: 91 (million)
% 11.04/2.05 % (1897345)Instruction limit reached!
% 11.04/2.05 % (1897345)------------------------------
% 11.04/2.05 % (1897345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.05 % (1897345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.05 % (1897345)CaDiCaL version: 2.1.3
% 11.04/2.05 % (1897345)Termination reason: Instruction limit
% 11.04/2.05 % (1897345)Termination phase: Saturation
% 11.04/2.05 % (1897345)Time elapsed: 0.038 s
% 11.04/2.05 % (1897345)Peak memory usage: 92 MB
% 11.04/2.05 % (1897345)Instructions burned: 130 (million)
% 11.04/2.05 % (1897332)------------------------------
% 11.04/2.05 % (1897332)------------------------------
% 11.04/2.05 % (1897343)Instruction limit reached!
% 11.04/2.05 % (1897343)------------------------------
% 11.04/2.05 % (1897343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.05 % (1897343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.05 % (1897343)CaDiCaL version: 2.1.3
% 11.04/2.05 % (1897343)Termination reason: Instruction limit
% 11.04/2.05 % (1897343)Termination phase: Saturation
% 11.04/2.05 % (1897343)Time elapsed: 0.120 s
% 11.04/2.05 % (1897343)Peak memory usage: 93 MB
% 11.04/2.05 % (1897343)Instructions burned: 220 (million)
% 11.04/2.05 % (1897349)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=609318390:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 11.04/2.05 % (1897349)Refutation not found, incomplete strategy
% 11.04/2.05 % (1897349)------------------------------
% 11.04/2.05 % (1897349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.05 % (1897349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.05 % (1897349)CaDiCaL version: 2.1.3
% 11.04/2.05 % (1897349)Termination reason: Refutation not found, incomplete strategy
% 11.04/2.05 % (1897349)Time elapsed: 0.038 s
% 11.04/2.05 % (1897349)Peak memory usage: 92 MB
% 11.04/2.05 % (1897349)Instructions burned: 126 (million)
% 11.04/2.05 % (1897350)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=523481980:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 11.04/2.05 % (1897351)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1558714151:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 11.04/2.05 % (1897342)------------------------------
% 11.04/2.05 % (1897342)------------------------------
% 11.04/2.05 % (1897350)Instruction limit reached!
% 11.04/2.05 % (1897350)------------------------------
% 11.04/2.05 % (1897350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.05 % (1897350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.05 % (1897350)CaDiCaL version: 2.1.3
% 11.04/2.05 % (1897350)Termination reason: Instruction limit
% 11.04/2.05 % (1897350)Termination phase: Saturation
% 11.04/2.05 % (1897350)Time elapsed: 0.092 s
% 11.04/2.05 % (1897350)Peak memory usage: 92 MB
% 11.04/2.05 % (1897350)Instructions burned: 159 (million)
% 11.04/2.05 % (1897349)------------------------------
% 11.04/2.05 % (1897349)------------------------------
% 11.04/2.05 % (1897355)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1490196311:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 11.04/2.05 % (1897357)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1703844145:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 11.04/2.05 % (1897356)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3720634319:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 11.04/2.05 % (1897355)Refutation not found, incomplete strategy
% 11.04/2.05 % (1897355)------------------------------
% 11.04/2.05 % (1897355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.05 % (1897355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.05 % (1897355)CaDiCaL version: 2.1.3
% 11.04/2.05 % (1897355)Termination reason: Refutation not found, incomplete strategy
% 11.04/2.05 % (1897355)Time elapsed: 0.043 s
% 11.04/2.05 % (1897355)Peak memory usage: 91 MB
% 11.04/2.05 % (1897355)Instructions burned: 75 (million)
% 11.04/2.05 % (1897357)Refutation not found, incomplete strategy
% 11.04/2.05 % (1897357)------------------------------
% 11.04/2.05 % (1897357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.05 % (1897357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.05 % (1897357)CaDiCaL version: 2.1.3
% 11.04/2.05 % (1897357)Termination reason: Refutation not found, incomplete strategy
% 11.04/2.05 % (1897357)Time elapsed: 0.050 s
% 11.04/2.05 % (1897357)Peak memory usage: 90 MB
% 11.04/2.05 % (1897357)Instructions burned: 192 (million)
% 11.04/2.05 % (1897328)Refutation not found, incomplete strategy
% 11.04/2.05 % (1897328)------------------------------
% 11.04/2.05 % (1897328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.05 % (1897328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.05 % (1897328)CaDiCaL version: 2.1.3
% 11.04/2.05 % (1897328)Termination reason: Refutation not found, incomplete strategy
% 11.04/2.05 % (1897328)Time elapsed: 0.705 s
% 11.04/2.05 % (1897328)Peak memory usage: 136 MB
% 11.04/2.05 % (1897328)Instructions burned: 1080 (million)
% 11.04/2.05 % (1897356)Instruction limit reached!
% 11.04/2.05 % (1897356)------------------------------
% 11.04/2.05 % (1897356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.05 % (1897356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.05 % (1897356)CaDiCaL version: 2.1.3
% 11.04/2.05 % (1897356)Termination reason: Instruction limit
% 11.04/2.05 % (1897356)Termination phase: Saturation
% 11.04/2.05 % (1897356)Time elapsed: 0.062 s
% 11.04/2.05 % (1897356)Peak memory usage: 91 MB
% 11.04/2.05 % (1897356)Instructions burned: 109 (million)
% 11.04/2.05 % (1897357)------------------------------
% 11.04/2.05 % (1897357)------------------------------
% 11.04/2.05 % (1897361)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1279752262:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 11.04/2.05 % (1897355)------------------------------
% 11.04/2.05 % (1897355)------------------------------
% 11.04/2.05 % (1897362)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3701461291:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 11.04/2.05 % (1897328)------------------------------
% 11.04/2.05 % (1897328)------------------------------
% 11.04/2.05 % (1897362)Instruction limit reached!
% 11.04/2.05 % (1897362)------------------------------
% 11.04/2.05 % (1897362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.05 % (1897362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.05 % (1897362)CaDiCaL version: 2.1.3
% 11.04/2.05 % (1897362)Termination reason: Instruction limit
% 11.04/2.05 % (1897362)Termination phase: Saturation
% 11.04/2.05 % (1897362)Time elapsed: 0.040 s
% 11.04/2.05 % (1897362)Peak memory usage: 92 MB
% 11.04/2.05 % (1897362)Instructions burned: 136 (million)
% 11.04/2.05 % (1897364)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1255357085:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 11.04/2.05 % (1897367)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2238827450:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 11.04/2.05 % (1897366)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2970257217:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 11.04/2.05 % (1897367)Instruction limit reached!
% 11.04/2.05 % (1897367)------------------------------
% 11.04/2.05 % (1897367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.05 % (1897367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.05 % (1897367)CaDiCaL version: 2.1.3
% 11.04/2.05 % (1897367)Termination reason: Instruction limit
% 11.04/2.05 % (1897367)Termination phase: Saturation
% 11.04/2.05 % (1897367)Time elapsed: 0.065 s
% 11.04/2.05 % (1897367)Peak memory usage: 91 MB
% 11.04/2.05 % (1897367)Instructions burned: 266 (million)
% 11.04/2.05 % (1897366)Instruction limit reached!
% 11.04/2.05 % (1897366)------------------------------
% 11.04/2.05 % (1897366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.05 % (1897366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.05 % (1897366)CaDiCaL version: 2.1.3
% 11.04/2.05 % (1897366)Termination reason: Instruction limit
% 11.04/2.05 % (1897366)Termination phase: Saturation
% 11.04/2.05 % (1897366)Time elapsed: 0.106 s
% 11.04/2.05 % (1897366)Peak memory usage: 93 MB
% 11.04/2.05 % (1897366)Instructions burned: 191 (million)
% 11.04/2.05 % (1897371)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1869260443:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi)
% 11.04/2.05 % (1897364)First to succeed.
% 11.04/2.05 % (1897364)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1897322"
% 11.04/2.05 % (1897371)Instruction limit reached!
% 11.04/2.05 % (1897371)------------------------------
% 11.04/2.05 % (1897371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.05 % (1897371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.05 % (1897371)CaDiCaL version: 2.1.3
% 11.04/2.05 % (1897371)Termination reason: Instruction limit
% 11.04/2.05 % (1897371)Termination phase: Saturation
% 11.04/2.05 % (1897371)Time elapsed: 0.046 s
% 11.04/2.05 % (1897371)Peak memory usage: 92 MB
% 11.04/2.05 % (1897371)Instructions burned: 157 (million)
% 11.04/2.05 % (1897372)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3464590385:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi)
% 11.04/2.05 % (1897374)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1172149074:i=537:av=off:ss=included_2985 on theBenchmark for (2985ds/537Mi)
% 11.04/2.05 % SZS status Satisfiable for theBenchmark
% 11.04/2.05 % SZS output start Saturation.
% See solution above
% 11.91/2.25 % SZS output start Definitions and Model Updates.
% 11.91/2.25 % SZS output end Definitions and Model Updates.
% 11.91/2.25 % (1897364)------------------------------
% 11.91/2.25 % (1897364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.91/2.25 % (1897364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.91/2.25 % (1897364)CaDiCaL version: 2.1.3
% 11.91/2.25 % (1897364)Termination reason: Satisfiable
% 11.91/2.25 % (1897364)Time elapsed: 0.190 s
% 11.91/2.25 % (1897364)Peak memory usage: 94 MB
% 11.91/2.25 % (1897364)Instructions burned: 333 (million)
% 11.91/2.25 % (1897364)------------------------------
% 11.91/2.25 % (1897364)------------------------------
% 11.91/2.25 % (1897322)Success in time 1.636 s
% 11.91/2.25 % Vampire exiting
%------------------------------------------------------------------------------