%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL657+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n011.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 11:54:22 AM UTC 2026
% Result : CounterSatisfiable 4.88s 6.55s
% Output : Saturation 5.56s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u245,negated_conjecture,
~ p104(sK21(sK22)) ).
cnf(u250,negated_conjecture,
~ p105(sK21(sK22)) ).
cnf(u254,negated_conjecture,
~ p103(sK21(sK22)) ).
cnf(u259,negated_conjecture,
~ p102(sK21(sK22)) ).
cnf(u265,negated_conjecture,
p101(sK21(sK22)) ).
cnf(u270,negated_conjecture,
p100(sK21(sK22)) ).
cnf(u302,negated_conjecture,
~ p104(sK20(sK22)) ).
cnf(u307,negated_conjecture,
~ p105(sK20(sK22)) ).
cnf(u311,negated_conjecture,
~ p103(sK20(sK22)) ).
cnf(u316,negated_conjecture,
~ p102(sK20(sK22)) ).
cnf(u322,negated_conjecture,
p101(sK20(sK22)) ).
cnf(u327,negated_conjecture,
p100(sK20(sK22)) ).
cnf(u546,negated_conjecture,
~ p1(sK22) ).
cnf(u549,negated_conjecture,
~ p1(sK21(sK22)) ).
cnf(u599,negated_conjecture,
~ p104(sK19(sK21(sK22))) ).
cnf(u604,negated_conjecture,
~ p105(sK19(sK21(sK22))) ).
cnf(u608,negated_conjecture,
~ p103(sK19(sK21(sK22))) ).
cnf(u614,negated_conjecture,
p102(sK19(sK21(sK22))) ).
cnf(u619,negated_conjecture,
p101(sK19(sK21(sK22))) ).
cnf(u624,negated_conjecture,
p100(sK19(sK21(sK22))) ).
cnf(u644,negated_conjecture,
~ p104(sK18(sK21(sK22))) ).
cnf(u649,negated_conjecture,
~ p105(sK18(sK21(sK22))) ).
cnf(u653,negated_conjecture,
~ p103(sK18(sK21(sK22))) ).
cnf(u659,negated_conjecture,
p102(sK18(sK21(sK22))) ).
cnf(u664,negated_conjecture,
p101(sK18(sK21(sK22))) ).
cnf(u669,negated_conjecture,
p100(sK18(sK21(sK22))) ).
cnf(u683,negated_conjecture,
p2(sK21(sK22)) ).
cnf(u688,negated_conjecture,
p2(sK19(sK21(sK22))) ).
cnf(u775,negated_conjecture,
~ p1(sK18(sK21(sK22))) ).
cnf(u833,negated_conjecture,
~ p104(sK19(sK20(sK22))) ).
cnf(u838,negated_conjecture,
~ p105(sK19(sK20(sK22))) ).
cnf(u842,negated_conjecture,
~ p103(sK19(sK20(sK22))) ).
cnf(u848,negated_conjecture,
p102(sK19(sK20(sK22))) ).
cnf(u853,negated_conjecture,
p101(sK19(sK20(sK22))) ).
cnf(u858,negated_conjecture,
p100(sK19(sK20(sK22))) ).
cnf(u895,negated_conjecture,
~ p104(sK18(sK20(sK22))) ).
cnf(u900,negated_conjecture,
~ p105(sK18(sK20(sK22))) ).
cnf(u904,negated_conjecture,
~ p103(sK18(sK20(sK22))) ).
cnf(u910,negated_conjecture,
p102(sK18(sK20(sK22))) ).
cnf(u915,negated_conjecture,
p101(sK18(sK20(sK22))) ).
cnf(u920,negated_conjecture,
p100(sK18(sK20(sK22))) ).
cnf(u1105,negated_conjecture,
sP0(sK17(sK19(sK21(sK22)))) ).
cnf(u1109,negated_conjecture,
p100(sK17(sK19(sK21(sK22)))) ).
cnf(u1114,negated_conjecture,
p101(sK17(sK19(sK21(sK22)))) ).
cnf(u1125,negated_conjecture,
sP1(sK17(sK19(sK21(sK22)))) ).
cnf(u1130,negated_conjecture,
p102(sK17(sK19(sK21(sK22)))) ).
cnf(u1141,negated_conjecture,
sP2(sK17(sK19(sK21(sK22)))) ).
cnf(u1146,negated_conjecture,
p103(sK17(sK19(sK21(sK22)))) ).
cnf(u1157,negated_conjecture,
sP3(sK17(sK19(sK21(sK22)))) ).
cnf(u1161,negated_conjecture,
~ p104(sK17(sK19(sK21(sK22)))) ).
cnf(u1165,negated_conjecture,
( ~ r1(sK15(sK17(sK19(sK21(sK22)))),X0)
| sP11(X0) ) ).
cnf(u1169,negated_conjecture,
( ~ r1(sK14(sK17(sK19(sK21(sK22)))),X0)
| sP11(X0) ) ).
cnf(u1173,negated_conjecture,
sP4(sK17(sK19(sK21(sK22)))) ).
cnf(u1177,negated_conjecture,
~ p105(sK17(sK19(sK21(sK22)))) ).
cnf(u1200,negated_conjecture,
sP0(sK16(sK19(sK21(sK22)))) ).
cnf(u1204,negated_conjecture,
p100(sK16(sK19(sK21(sK22)))) ).
cnf(u1209,negated_conjecture,
p101(sK16(sK19(sK21(sK22)))) ).
cnf(u1220,negated_conjecture,
sP1(sK16(sK19(sK21(sK22)))) ).
cnf(u1225,negated_conjecture,
p102(sK16(sK19(sK21(sK22)))) ).
cnf(u1236,negated_conjecture,
sP2(sK16(sK19(sK21(sK22)))) ).
cnf(u1241,negated_conjecture,
p103(sK16(sK19(sK21(sK22)))) ).
cnf(u1252,negated_conjecture,
sP3(sK16(sK19(sK21(sK22)))) ).
cnf(u1256,negated_conjecture,
~ p104(sK16(sK19(sK21(sK22)))) ).
cnf(u1260,negated_conjecture,
( ~ r1(sK15(sK16(sK19(sK21(sK22)))),X0)
| sP11(X0) ) ).
cnf(u1264,negated_conjecture,
( ~ r1(sK14(sK16(sK19(sK21(sK22)))),X0)
| sP11(X0) ) ).
cnf(u1268,negated_conjecture,
sP4(sK16(sK19(sK21(sK22)))) ).
cnf(u1272,negated_conjecture,
~ p105(sK16(sK19(sK21(sK22)))) ).
cnf(u1295,negated_conjecture,
sP0(sK17(sK18(sK21(sK22)))) ).
cnf(u1299,negated_conjecture,
p100(sK17(sK18(sK21(sK22)))) ).
cnf(u1304,negated_conjecture,
p101(sK17(sK18(sK21(sK22)))) ).
cnf(u1315,negated_conjecture,
sP1(sK17(sK18(sK21(sK22)))) ).
cnf(u1320,negated_conjecture,
p102(sK17(sK18(sK21(sK22)))) ).
cnf(u1331,negated_conjecture,
sP2(sK17(sK18(sK21(sK22)))) ).
cnf(u1336,negated_conjecture,
p103(sK17(sK18(sK21(sK22)))) ).
cnf(u1347,negated_conjecture,
sP3(sK17(sK18(sK21(sK22)))) ).
cnf(u1351,negated_conjecture,
~ p104(sK17(sK18(sK21(sK22)))) ).
cnf(u1355,negated_conjecture,
( ~ r1(sK15(sK17(sK18(sK21(sK22)))),X0)
| sP11(X0) ) ).
cnf(u1359,negated_conjecture,
( ~ r1(sK14(sK17(sK18(sK21(sK22)))),X0)
| sP11(X0) ) ).
cnf(u1363,negated_conjecture,
sP4(sK17(sK18(sK21(sK22)))) ).
cnf(u1367,negated_conjecture,
~ p105(sK17(sK18(sK21(sK22)))) ).
cnf(u1390,negated_conjecture,
sP0(sK16(sK18(sK21(sK22)))) ).
cnf(u1394,negated_conjecture,
p100(sK16(sK18(sK21(sK22)))) ).
cnf(u1399,negated_conjecture,
p101(sK16(sK18(sK21(sK22)))) ).
cnf(u1410,negated_conjecture,
sP1(sK16(sK18(sK21(sK22)))) ).
cnf(u1415,negated_conjecture,
p102(sK16(sK18(sK21(sK22)))) ).
cnf(u1426,negated_conjecture,
sP2(sK16(sK18(sK21(sK22)))) ).
cnf(u1431,negated_conjecture,
p103(sK16(sK18(sK21(sK22)))) ).
cnf(u1442,negated_conjecture,
sP3(sK16(sK18(sK21(sK22)))) ).
cnf(u1446,negated_conjecture,
~ p104(sK16(sK18(sK21(sK22)))) ).
cnf(u1450,negated_conjecture,
( ~ r1(sK15(sK16(sK18(sK21(sK22)))),X0)
| sP11(X0) ) ).
cnf(u1454,negated_conjecture,
( ~ r1(sK14(sK16(sK18(sK21(sK22)))),X0)
| sP11(X0) ) ).
cnf(u1458,negated_conjecture,
sP4(sK16(sK18(sK21(sK22)))) ).
cnf(u1462,negated_conjecture,
~ p105(sK16(sK18(sK21(sK22)))) ).
cnf(u1502,negated_conjecture,
sP0(sK17(sK19(sK20(sK22)))) ).
cnf(u1506,negated_conjecture,
p100(sK17(sK19(sK20(sK22)))) ).
cnf(u1511,negated_conjecture,
p101(sK17(sK19(sK20(sK22)))) ).
cnf(u1522,negated_conjecture,
sP1(sK17(sK19(sK20(sK22)))) ).
cnf(u1527,negated_conjecture,
p102(sK17(sK19(sK20(sK22)))) ).
cnf(u1538,negated_conjecture,
sP2(sK17(sK19(sK20(sK22)))) ).
cnf(u1543,negated_conjecture,
p103(sK17(sK19(sK20(sK22)))) ).
cnf(u1554,negated_conjecture,
sP3(sK17(sK19(sK20(sK22)))) ).
cnf(u1558,negated_conjecture,
~ p104(sK17(sK19(sK20(sK22)))) ).
cnf(u1562,negated_conjecture,
( ~ r1(sK15(sK17(sK19(sK20(sK22)))),X0)
| sP11(X0) ) ).
cnf(u1566,negated_conjecture,
( ~ r1(sK14(sK17(sK19(sK20(sK22)))),X0)
| sP11(X0) ) ).
cnf(u1570,negated_conjecture,
sP4(sK17(sK19(sK20(sK22)))) ).
cnf(u1574,negated_conjecture,
~ p105(sK17(sK19(sK20(sK22)))) ).
cnf(u1597,negated_conjecture,
sP0(sK16(sK19(sK20(sK22)))) ).
cnf(u1601,negated_conjecture,
p100(sK16(sK19(sK20(sK22)))) ).
cnf(u1606,negated_conjecture,
p101(sK16(sK19(sK20(sK22)))) ).
cnf(u1617,negated_conjecture,
sP1(sK16(sK19(sK20(sK22)))) ).
cnf(u1622,negated_conjecture,
p102(sK16(sK19(sK20(sK22)))) ).
cnf(u1633,negated_conjecture,
sP2(sK16(sK19(sK20(sK22)))) ).
cnf(u1638,negated_conjecture,
p103(sK16(sK19(sK20(sK22)))) ).
cnf(u1649,negated_conjecture,
sP3(sK16(sK19(sK20(sK22)))) ).
cnf(u1653,negated_conjecture,
~ p104(sK16(sK19(sK20(sK22)))) ).
cnf(u1657,negated_conjecture,
( ~ r1(sK15(sK16(sK19(sK20(sK22)))),X0)
| sP11(X0) ) ).
cnf(u1661,negated_conjecture,
( ~ r1(sK14(sK16(sK19(sK20(sK22)))),X0)
| sP11(X0) ) ).
cnf(u1665,negated_conjecture,
sP4(sK16(sK19(sK20(sK22)))) ).
cnf(u1669,negated_conjecture,
~ p105(sK16(sK19(sK20(sK22)))) ).
cnf(u1687,negated_conjecture,
~ p2(sK20(sK22)) ).
cnf(u1690,negated_conjecture,
~ p2(sK19(sK20(sK22))) ).
cnf(u1702,negated_conjecture,
~ p1(sK20(sK22)) ).
cnf(u1705,negated_conjecture,
~ p1(sK19(sK20(sK22))) ).
cnf(u1751,negated_conjecture,
~ sP0(sK17(sK20(sK22))) ).
cnf(u1771,negated_conjecture,
~ sP1(sK17(sK20(sK22))) ).
cnf(u1774,negated_conjecture,
~ p102(sK17(sK20(sK22))) ).
cnf(u1803,negated_conjecture,
~ sP3(sK17(sK20(sK22))) ).
cnf(u1819,negated_conjecture,
~ sP4(sK17(sK20(sK22))) ).
cnf(u1878,negated_conjecture,
sP2(sK19(sK20(sK22))) ).
cnf(u1882,negated_conjecture,
( ~ r1(sK17(sK19(sK20(sK22))),X0)
| sP11(X1)
| ~ r1(X0,X1) ) ).
cnf(u1886,negated_conjecture,
( ~ r1(sK16(sK19(sK20(sK22))),X0)
| sP11(X1)
| ~ r1(X0,X1) ) ).
cnf(u1905,negated_conjecture,
sP2(sK18(sK20(sK22))) ).
cnf(u1909,negated_conjecture,
( ~ r1(sK17(sK18(sK20(sK22))),X0)
| sP11(X1)
| ~ r1(X0,X1) ) ).
cnf(u1913,negated_conjecture,
( ~ r1(sK16(sK18(sK20(sK22))),X0)
| sP11(X1)
| ~ r1(X0,X1) ) ).
cnf(u2054,negated_conjecture,
sP0(sK17(sK18(sK20(sK22)))) ).
cnf(u2058,negated_conjecture,
p100(sK17(sK18(sK20(sK22)))) ).
cnf(u2063,negated_conjecture,
p101(sK17(sK18(sK20(sK22)))) ).
cnf(u2074,negated_conjecture,
sP1(sK17(sK18(sK20(sK22)))) ).
cnf(u2079,negated_conjecture,
p102(sK17(sK18(sK20(sK22)))) ).
cnf(u2090,negated_conjecture,
sP2(sK17(sK18(sK20(sK22)))) ).
cnf(u2095,negated_conjecture,
p103(sK17(sK18(sK20(sK22)))) ).
cnf(u2106,negated_conjecture,
sP3(sK17(sK18(sK20(sK22)))) ).
cnf(u2110,negated_conjecture,
~ p104(sK17(sK18(sK20(sK22)))) ).
cnf(u2114,negated_conjecture,
( ~ r1(sK15(sK17(sK18(sK20(sK22)))),X0)
| sP11(X0) ) ).
cnf(u2118,negated_conjecture,
( ~ r1(sK14(sK17(sK18(sK20(sK22)))),X0)
| sP11(X0) ) ).
cnf(u2122,negated_conjecture,
sP4(sK17(sK18(sK20(sK22)))) ).
cnf(u2126,negated_conjecture,
~ p105(sK17(sK18(sK20(sK22)))) ).
cnf(u2149,negated_conjecture,
sP0(sK16(sK18(sK20(sK22)))) ).
cnf(u2153,negated_conjecture,
p100(sK16(sK18(sK20(sK22)))) ).
cnf(u2158,negated_conjecture,
p101(sK16(sK18(sK20(sK22)))) ).
cnf(u2169,negated_conjecture,
sP1(sK16(sK18(sK20(sK22)))) ).
cnf(u2174,negated_conjecture,
p102(sK16(sK18(sK20(sK22)))) ).
cnf(u2185,negated_conjecture,
sP2(sK16(sK18(sK20(sK22)))) ).
cnf(u2190,negated_conjecture,
p103(sK16(sK18(sK20(sK22)))) ).
cnf(u2201,negated_conjecture,
sP3(sK16(sK18(sK20(sK22)))) ).
cnf(u2205,negated_conjecture,
~ p104(sK16(sK18(sK20(sK22)))) ).
cnf(u2209,negated_conjecture,
( ~ r1(sK15(sK16(sK18(sK20(sK22)))),X0)
| sP11(X0) ) ).
cnf(u2213,negated_conjecture,
( ~ r1(sK14(sK16(sK18(sK20(sK22)))),X0)
| sP11(X0) ) ).
cnf(u2217,negated_conjecture,
sP4(sK16(sK18(sK20(sK22)))) ).
cnf(u2221,negated_conjecture,
~ p105(sK16(sK18(sK20(sK22)))) ).
cnf(u2312,negated_conjecture,
~ sP0(sK15(sK19(sK21(sK22)))) ).
cnf(u2332,negated_conjecture,
~ sP1(sK15(sK19(sK21(sK22)))) ).
cnf(u2335,negated_conjecture,
~ p102(sK15(sK19(sK21(sK22)))) ).
cnf(u2364,negated_conjecture,
~ sP3(sK15(sK19(sK21(sK22)))) ).
cnf(u2380,negated_conjecture,
~ sP4(sK15(sK19(sK21(sK22)))) ).
cnf(u2450,negated_conjecture,
p3(sK19(sK21(sK22))) ).
cnf(u2455,negated_conjecture,
p3(sK17(sK19(sK21(sK22)))) ).
cnf(u2507,negated_conjecture,
~ p1(sK19(sK21(sK22))) ).
cnf(u2510,negated_conjecture,
~ p1(sK17(sK19(sK21(sK22)))) ).
cnf(u2669,negated_conjecture,
~ sP0(sK15(sK18(sK21(sK22)))) ).
cnf(u2689,negated_conjecture,
~ sP1(sK15(sK18(sK21(sK22)))) ).
cnf(u2692,negated_conjecture,
~ p102(sK15(sK18(sK21(sK22)))) ).
cnf(u2721,negated_conjecture,
~ sP3(sK15(sK18(sK21(sK22)))) ).
cnf(u2737,negated_conjecture,
~ sP4(sK15(sK18(sK21(sK22)))) ).
cnf(u2808,negated_conjecture,
~ p3(sK18(sK21(sK22))) ).
cnf(u2811,negated_conjecture,
~ p3(sK17(sK18(sK21(sK22)))) ).
cnf(u2902,negated_conjecture,
~ p1(sK17(sK19(sK20(sK22)))) ).
cnf(u2913,negated_conjecture,
~ p2(sK17(sK19(sK20(sK22)))) ).
cnf(u2923,negated_conjecture,
p3(sK19(sK20(sK22))) ).
cnf(u2928,negated_conjecture,
p3(sK17(sK19(sK20(sK22)))) ).
cnf(u3068,negated_conjecture,
~ p1(sK18(sK20(sK22))) ).
cnf(u3071,negated_conjecture,
~ p1(sK17(sK18(sK20(sK22)))) ).
cnf(u3083,negated_conjecture,
~ p2(sK18(sK20(sK22))) ).
cnf(u3086,negated_conjecture,
~ p2(sK17(sK18(sK20(sK22)))) ).
cnf(u3097,negated_conjecture,
~ p3(sK18(sK20(sK22))) ).
cnf(u3100,negated_conjecture,
~ p3(sK17(sK18(sK20(sK22)))) ).
cnf(u3194,negated_conjecture,
~ p1(sK17(sK18(sK21(sK22)))) ).
cnf(u3300,negated_conjecture,
sP0(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u3304,negated_conjecture,
p100(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u3309,negated_conjecture,
p101(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u3322,negated_conjecture,
sP1(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u3327,negated_conjecture,
p102(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u3340,negated_conjecture,
sP2(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u3345,negated_conjecture,
p103(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u3358,negated_conjecture,
sP3(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u3363,negated_conjecture,
p104(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u3376,negated_conjecture,
sP4(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u3380,negated_conjecture,
~ p105(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u3385,negated_conjecture,
sP11(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u3390,negated_conjecture,
sP11(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u3406,negated_conjecture,
sP0(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u3410,negated_conjecture,
p100(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u3415,negated_conjecture,
p101(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u3428,negated_conjecture,
sP1(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u3433,negated_conjecture,
p102(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u3446,negated_conjecture,
sP2(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u3451,negated_conjecture,
p103(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u3464,negated_conjecture,
sP3(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u3469,negated_conjecture,
p104(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u3482,negated_conjecture,
sP4(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u3486,negated_conjecture,
~ p105(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u3491,negated_conjecture,
sP11(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u3496,negated_conjecture,
sP11(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u3512,negated_conjecture,
sP0(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u3516,negated_conjecture,
p100(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u3521,negated_conjecture,
p101(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u3534,negated_conjecture,
sP1(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u3539,negated_conjecture,
p102(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u3552,negated_conjecture,
sP2(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u3557,negated_conjecture,
p103(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u3570,negated_conjecture,
sP3(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u3575,negated_conjecture,
p104(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u3588,negated_conjecture,
sP4(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u3592,negated_conjecture,
~ p105(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u3597,negated_conjecture,
sP11(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u3602,negated_conjecture,
sP11(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u3617,negated_conjecture,
sP0(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u3621,negated_conjecture,
p100(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u3626,negated_conjecture,
p101(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u3639,negated_conjecture,
sP1(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u3644,negated_conjecture,
p102(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u3657,negated_conjecture,
sP2(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u3662,negated_conjecture,
p103(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u3675,negated_conjecture,
sP3(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u3680,negated_conjecture,
p104(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u3693,negated_conjecture,
sP4(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u3697,negated_conjecture,
~ p105(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u3702,negated_conjecture,
sP11(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u3707,negated_conjecture,
sP11(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u3722,negated_conjecture,
sP0(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u3726,negated_conjecture,
p100(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u3731,negated_conjecture,
p101(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u3744,negated_conjecture,
sP1(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u3749,negated_conjecture,
p102(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u3762,negated_conjecture,
sP2(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u3767,negated_conjecture,
p103(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u3780,negated_conjecture,
sP3(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u3785,negated_conjecture,
p104(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u3798,negated_conjecture,
sP4(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u3802,negated_conjecture,
~ p105(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u3807,negated_conjecture,
sP11(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u3812,negated_conjecture,
sP11(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u3827,negated_conjecture,
sP0(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u3831,negated_conjecture,
p100(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u3836,negated_conjecture,
p101(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u3849,negated_conjecture,
sP1(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u3854,negated_conjecture,
p102(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u3867,negated_conjecture,
sP2(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u3872,negated_conjecture,
p103(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u3885,negated_conjecture,
sP3(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u3890,negated_conjecture,
p104(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u3903,negated_conjecture,
sP4(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u3907,negated_conjecture,
~ p105(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u3912,negated_conjecture,
sP11(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u3917,negated_conjecture,
sP11(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u3932,negated_conjecture,
sP0(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u3936,negated_conjecture,
p100(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u3941,negated_conjecture,
p101(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u3954,negated_conjecture,
sP1(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u3959,negated_conjecture,
p102(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u3972,negated_conjecture,
sP2(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u3977,negated_conjecture,
p103(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u3990,negated_conjecture,
sP3(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u3995,negated_conjecture,
p104(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u4008,negated_conjecture,
sP4(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u4012,negated_conjecture,
~ p105(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u4017,negated_conjecture,
sP11(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u4022,negated_conjecture,
sP11(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u4037,negated_conjecture,
sP0(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u4041,negated_conjecture,
p100(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u4046,negated_conjecture,
p101(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u4059,negated_conjecture,
sP1(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u4064,negated_conjecture,
p102(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u4077,negated_conjecture,
sP2(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u4082,negated_conjecture,
p103(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u4095,negated_conjecture,
sP3(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u4100,negated_conjecture,
p104(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u4113,negated_conjecture,
sP4(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u4117,negated_conjecture,
~ p105(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u4122,negated_conjecture,
sP11(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u4127,negated_conjecture,
sP11(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u4142,negated_conjecture,
sP0(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u4146,negated_conjecture,
p100(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u4151,negated_conjecture,
p101(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u4164,negated_conjecture,
sP1(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u4169,negated_conjecture,
p102(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u4182,negated_conjecture,
sP2(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u4187,negated_conjecture,
p103(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u4200,negated_conjecture,
sP3(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u4205,negated_conjecture,
p104(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u4218,negated_conjecture,
sP4(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u4222,negated_conjecture,
~ p105(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u4227,negated_conjecture,
sP11(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u4232,negated_conjecture,
sP11(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u4247,negated_conjecture,
sP0(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u4251,negated_conjecture,
p100(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u4256,negated_conjecture,
p101(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u4269,negated_conjecture,
sP1(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u4274,negated_conjecture,
p102(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u4287,negated_conjecture,
sP2(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u4292,negated_conjecture,
p103(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u4305,negated_conjecture,
sP3(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u4310,negated_conjecture,
p104(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u4323,negated_conjecture,
sP4(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u4327,negated_conjecture,
~ p105(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u4332,negated_conjecture,
sP11(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u4337,negated_conjecture,
sP11(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u4352,negated_conjecture,
sP0(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u4356,negated_conjecture,
p100(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u4361,negated_conjecture,
p101(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u4374,negated_conjecture,
sP1(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u4379,negated_conjecture,
p102(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u4392,negated_conjecture,
sP2(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u4397,negated_conjecture,
p103(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u4410,negated_conjecture,
sP3(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u4415,negated_conjecture,
p104(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u4428,negated_conjecture,
sP4(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u4432,negated_conjecture,
~ p105(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u4437,negated_conjecture,
sP11(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u4442,negated_conjecture,
sP11(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u4457,negated_conjecture,
sP0(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u4461,negated_conjecture,
p100(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u4466,negated_conjecture,
p101(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u4479,negated_conjecture,
sP1(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u4484,negated_conjecture,
p102(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u4497,negated_conjecture,
sP2(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u4502,negated_conjecture,
p103(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u4515,negated_conjecture,
sP3(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u4520,negated_conjecture,
p104(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u4533,negated_conjecture,
sP4(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u4537,negated_conjecture,
~ p105(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u4542,negated_conjecture,
sP11(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u4547,negated_conjecture,
sP11(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u4562,negated_conjecture,
sP0(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u4566,negated_conjecture,
p100(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u4571,negated_conjecture,
p101(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u4584,negated_conjecture,
sP1(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u4589,negated_conjecture,
p102(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u4602,negated_conjecture,
sP2(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u4607,negated_conjecture,
p103(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u4620,negated_conjecture,
sP3(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u4625,negated_conjecture,
p104(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u4638,negated_conjecture,
sP4(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u4642,negated_conjecture,
~ p105(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u4647,negated_conjecture,
sP11(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u4652,negated_conjecture,
sP11(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u4667,negated_conjecture,
sP0(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u4671,negated_conjecture,
p100(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u4676,negated_conjecture,
p101(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u4689,negated_conjecture,
sP1(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u4694,negated_conjecture,
p102(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u4707,negated_conjecture,
sP2(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u4712,negated_conjecture,
p103(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u4725,negated_conjecture,
sP3(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u4730,negated_conjecture,
p104(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u4743,negated_conjecture,
sP4(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u4747,negated_conjecture,
~ p105(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u4752,negated_conjecture,
sP11(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u4757,negated_conjecture,
sP11(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u4772,negated_conjecture,
sP0(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u4776,negated_conjecture,
p100(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u4781,negated_conjecture,
p101(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u4794,negated_conjecture,
sP1(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u4799,negated_conjecture,
p102(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u4812,negated_conjecture,
sP2(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u4817,negated_conjecture,
p103(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u4830,negated_conjecture,
sP3(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u4835,negated_conjecture,
p104(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u4848,negated_conjecture,
sP4(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u4852,negated_conjecture,
~ p105(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u4857,negated_conjecture,
sP11(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u4862,negated_conjecture,
sP11(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u4877,negated_conjecture,
sP0(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u4881,negated_conjecture,
p100(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u4886,negated_conjecture,
p101(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u4899,negated_conjecture,
sP1(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u4904,negated_conjecture,
p102(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u4917,negated_conjecture,
sP2(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u4922,negated_conjecture,
p103(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u4935,negated_conjecture,
sP3(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u4940,negated_conjecture,
p104(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u4953,negated_conjecture,
sP4(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u4957,negated_conjecture,
~ p105(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u4962,negated_conjecture,
sP11(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u4967,negated_conjecture,
sP11(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u5281,negated_conjecture,
~ p1(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u5305,negated_conjecture,
p4(sK17(sK19(sK21(sK22)))) ).
cnf(u5310,negated_conjecture,
p4(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u5419,negated_conjecture,
~ p1(sK16(sK19(sK21(sK22)))) ).
cnf(u5422,negated_conjecture,
~ p1(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u5447,negated_conjecture,
~ p4(sK16(sK19(sK21(sK22)))) ).
cnf(u5450,negated_conjecture,
~ p4(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u5549,negated_conjecture,
~ p1(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u5567,negated_conjecture,
~ p3(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u5577,negated_conjecture,
p4(sK17(sK18(sK21(sK22)))) ).
cnf(u5582,negated_conjecture,
p4(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u5685,negated_conjecture,
~ p1(sK16(sK18(sK21(sK22)))) ).
cnf(u5688,negated_conjecture,
~ p1(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u5707,negated_conjecture,
~ p3(sK16(sK18(sK21(sK22)))) ).
cnf(u5710,negated_conjecture,
~ p3(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u5721,negated_conjecture,
~ p4(sK16(sK18(sK21(sK22)))) ).
cnf(u5724,negated_conjecture,
~ p4(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u5817,negated_conjecture,
~ p1(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u5828,negated_conjecture,
~ p2(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u5845,negated_conjecture,
p4(sK17(sK19(sK20(sK22)))) ).
cnf(u5850,negated_conjecture,
p4(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u5953,negated_conjecture,
~ p1(sK16(sK19(sK20(sK22)))) ).
cnf(u5956,negated_conjecture,
~ p1(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u5968,negated_conjecture,
~ p2(sK16(sK19(sK20(sK22)))) ).
cnf(u5971,negated_conjecture,
~ p2(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u5989,negated_conjecture,
~ p4(sK16(sK19(sK20(sK22)))) ).
cnf(u5992,negated_conjecture,
~ p4(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u6085,negated_conjecture,
~ p1(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u6096,negated_conjecture,
~ p2(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u6107,negated_conjecture,
~ p3(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u6117,negated_conjecture,
p4(sK17(sK18(sK20(sK22)))) ).
cnf(u6122,negated_conjecture,
p4(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u6219,negated_conjecture,
~ p1(sK16(sK18(sK20(sK22)))) ).
cnf(u6222,negated_conjecture,
~ p1(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u6234,negated_conjecture,
~ p2(sK16(sK18(sK20(sK22)))) ).
cnf(u6237,negated_conjecture,
~ p2(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u6249,negated_conjecture,
~ p3(sK16(sK18(sK20(sK22)))) ).
cnf(u6252,negated_conjecture,
~ p3(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u6263,negated_conjecture,
~ p4(sK16(sK18(sK20(sK22)))) ).
cnf(u6266,negated_conjecture,
~ p4(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u6340,negated_conjecture,
p104(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6343,negated_conjecture,
p105(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6349,negated_conjecture,
p103(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6354,negated_conjecture,
p102(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6359,negated_conjecture,
p101(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6364,negated_conjecture,
p100(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6385,negated_conjecture,
p104(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6388,negated_conjecture,
p105(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6394,negated_conjecture,
p103(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6399,negated_conjecture,
p102(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6404,negated_conjecture,
p101(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6409,negated_conjecture,
p100(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6430,negated_conjecture,
p104(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6433,negated_conjecture,
p105(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6439,negated_conjecture,
p103(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6444,negated_conjecture,
p102(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6449,negated_conjecture,
p101(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6454,negated_conjecture,
p100(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6475,negated_conjecture,
p104(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6478,negated_conjecture,
p105(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6484,negated_conjecture,
p103(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6489,negated_conjecture,
p102(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6494,negated_conjecture,
p101(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6499,negated_conjecture,
p100(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6520,negated_conjecture,
p104(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6523,negated_conjecture,
p105(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6529,negated_conjecture,
p103(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6534,negated_conjecture,
p102(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6539,negated_conjecture,
p101(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6544,negated_conjecture,
p100(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6565,negated_conjecture,
p104(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6568,negated_conjecture,
p105(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6574,negated_conjecture,
p103(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6579,negated_conjecture,
p102(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6584,negated_conjecture,
p101(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6589,negated_conjecture,
p100(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6610,negated_conjecture,
p104(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6613,negated_conjecture,
p105(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6619,negated_conjecture,
p103(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6624,negated_conjecture,
p102(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6629,negated_conjecture,
p101(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6634,negated_conjecture,
p100(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6656,negated_conjecture,
p104(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6659,negated_conjecture,
p105(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6665,negated_conjecture,
p103(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6670,negated_conjecture,
p102(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6675,negated_conjecture,
p101(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6680,negated_conjecture,
p100(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6702,negated_conjecture,
p104(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6705,negated_conjecture,
p105(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6711,negated_conjecture,
p103(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6716,negated_conjecture,
p102(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6721,negated_conjecture,
p101(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6726,negated_conjecture,
p100(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6748,negated_conjecture,
p104(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6751,negated_conjecture,
p105(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6757,negated_conjecture,
p103(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6762,negated_conjecture,
p102(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6767,negated_conjecture,
p101(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6772,negated_conjecture,
p100(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6793,negated_conjecture,
p104(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6796,negated_conjecture,
p105(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6802,negated_conjecture,
p103(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6807,negated_conjecture,
p102(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6812,negated_conjecture,
p101(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6817,negated_conjecture,
p100(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6838,negated_conjecture,
p104(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6841,negated_conjecture,
p105(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6847,negated_conjecture,
p103(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6852,negated_conjecture,
p102(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6857,negated_conjecture,
p101(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6862,negated_conjecture,
p100(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6883,negated_conjecture,
p104(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6886,negated_conjecture,
p105(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6892,negated_conjecture,
p103(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6897,negated_conjecture,
p102(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6902,negated_conjecture,
p101(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6907,negated_conjecture,
p100(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6928,negated_conjecture,
p104(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6931,negated_conjecture,
p105(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6937,negated_conjecture,
p103(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6942,negated_conjecture,
p102(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6947,negated_conjecture,
p101(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6952,negated_conjecture,
p100(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6973,negated_conjecture,
p104(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u6976,negated_conjecture,
p105(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u6982,negated_conjecture,
p103(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u6987,negated_conjecture,
p102(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u6992,negated_conjecture,
p101(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u6997,negated_conjecture,
p100(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u7018,negated_conjecture,
p104(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u7021,negated_conjecture,
p105(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u7027,negated_conjecture,
p103(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u7032,negated_conjecture,
p102(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u7037,negated_conjecture,
p101(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u7042,negated_conjecture,
p100(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u7064,negated_conjecture,
p104(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7067,negated_conjecture,
p105(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7073,negated_conjecture,
p103(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7078,negated_conjecture,
p102(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7083,negated_conjecture,
p101(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7088,negated_conjecture,
p100(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7110,negated_conjecture,
p104(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7113,negated_conjecture,
p105(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7119,negated_conjecture,
p103(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7124,negated_conjecture,
p102(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7129,negated_conjecture,
p101(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7134,negated_conjecture,
p100(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7156,negated_conjecture,
p104(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7159,negated_conjecture,
p105(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7165,negated_conjecture,
p103(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7170,negated_conjecture,
p102(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7175,negated_conjecture,
p101(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7180,negated_conjecture,
p100(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7201,negated_conjecture,
p104(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7204,negated_conjecture,
p105(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7210,negated_conjecture,
p103(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7215,negated_conjecture,
p102(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7220,negated_conjecture,
p101(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7225,negated_conjecture,
p100(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7246,negated_conjecture,
p104(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u7249,negated_conjecture,
p105(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u7255,negated_conjecture,
p103(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u7260,negated_conjecture,
p102(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u7265,negated_conjecture,
p101(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u7270,negated_conjecture,
p100(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u7291,negated_conjecture,
p104(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u7294,negated_conjecture,
p105(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u7300,negated_conjecture,
p103(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u7305,negated_conjecture,
p102(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u7310,negated_conjecture,
p101(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u7315,negated_conjecture,
p100(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u7336,negated_conjecture,
p104(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7339,negated_conjecture,
p105(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7345,negated_conjecture,
p103(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7350,negated_conjecture,
p102(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7355,negated_conjecture,
p101(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7360,negated_conjecture,
p100(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7381,negated_conjecture,
p104(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7384,negated_conjecture,
p105(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7390,negated_conjecture,
p103(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7395,negated_conjecture,
p102(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7400,negated_conjecture,
p101(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7405,negated_conjecture,
p100(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7426,negated_conjecture,
p104(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7429,negated_conjecture,
p105(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7435,negated_conjecture,
p103(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7440,negated_conjecture,
p102(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7445,negated_conjecture,
p101(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7450,negated_conjecture,
p100(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7472,negated_conjecture,
p104(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7475,negated_conjecture,
p105(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7481,negated_conjecture,
p103(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7486,negated_conjecture,
p102(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7491,negated_conjecture,
p101(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7496,negated_conjecture,
p100(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7518,negated_conjecture,
p104(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7521,negated_conjecture,
p105(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7527,negated_conjecture,
p103(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7532,negated_conjecture,
p102(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7537,negated_conjecture,
p101(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7542,negated_conjecture,
p100(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7563,negated_conjecture,
p104(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7566,negated_conjecture,
p105(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7572,negated_conjecture,
p103(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7577,negated_conjecture,
p102(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7582,negated_conjecture,
p101(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7587,negated_conjecture,
p100(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7608,negated_conjecture,
p104(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7611,negated_conjecture,
p105(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7617,negated_conjecture,
p103(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7622,negated_conjecture,
p102(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7627,negated_conjecture,
p101(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7632,negated_conjecture,
p100(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7653,negated_conjecture,
p104(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7656,negated_conjecture,
p105(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7662,negated_conjecture,
p103(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7667,negated_conjecture,
p102(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7672,negated_conjecture,
p101(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7677,negated_conjecture,
p100(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7698,negated_conjecture,
p104(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7701,negated_conjecture,
p105(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7707,negated_conjecture,
p103(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7712,negated_conjecture,
p102(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7717,negated_conjecture,
p101(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7722,negated_conjecture,
p100(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7743,negated_conjecture,
p104(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7746,negated_conjecture,
p105(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7752,negated_conjecture,
p103(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7757,negated_conjecture,
p102(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7762,negated_conjecture,
p101(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7767,negated_conjecture,
p100(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7797,negated_conjecture,
p5(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u7802,negated_conjecture,
p5(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u7887,negated_conjecture,
~ p5(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u7923,negated_conjecture,
~ p1(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u7969,negated_conjecture,
p5(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u7974,negated_conjecture,
p5(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u8057,negated_conjecture,
~ p5(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u8072,negated_conjecture,
~ p4(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u8101,negated_conjecture,
~ p1(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u8141,negated_conjecture,
p5(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u8146,negated_conjecture,
p5(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u8229,negated_conjecture,
~ p5(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u8251,negated_conjecture,
~ p3(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u8273,negated_conjecture,
~ p1(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u8313,negated_conjecture,
p5(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u8318,negated_conjecture,
p5(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u8399,negated_conjecture,
~ p5(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u8414,negated_conjecture,
~ p4(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u8429,negated_conjecture,
~ p3(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u8451,negated_conjecture,
~ p1(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u8485,negated_conjecture,
p5(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u8490,negated_conjecture,
p5(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u8573,negated_conjecture,
~ p5(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u8602,negated_conjecture,
~ p2(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u8617,negated_conjecture,
~ p1(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u8657,negated_conjecture,
p5(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u8662,negated_conjecture,
p5(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u8743,negated_conjecture,
~ p5(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u8758,negated_conjecture,
~ p4(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u8780,negated_conjecture,
~ p2(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u8795,negated_conjecture,
~ p1(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u8829,negated_conjecture,
p5(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u8834,negated_conjecture,
p5(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u8915,negated_conjecture,
~ p5(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u8937,negated_conjecture,
~ p3(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u8952,negated_conjecture,
~ p2(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u8967,negated_conjecture,
~ p1(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u9001,negated_conjecture,
p5(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u9006,negated_conjecture,
p5(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u9085,negated_conjecture,
~ p5(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u9100,negated_conjecture,
~ p4(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u9115,negated_conjecture,
~ p3(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u9130,negated_conjecture,
~ p2(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u9145,negated_conjecture,
~ p1(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u6333,negated_conjecture,
sP1(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u7595,negated_conjecture,
sP6(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u6461,negated_conjecture,
sP5(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u749,negated_conjecture,
sP9(sK18(sK21(sK22))) ).
cnf(u6780,negated_conjecture,
sP6(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u7549,negated_conjecture,
sP5(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u6784,negated_conjecture,
sP10(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u8898,negated_conjecture,
p4(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u722,negated_conjecture,
sP11(sK19(sK21(sK22))) ).
cnf(u2519,negated_conjecture,
p2(sK17(sK19(sK21(sK22)))) ).
cnf(u281,axiom,
( ~ p105(sK20(X0))
| p6(sK20(X0))
| ~ p6(X0)
| ~ p105(X0)
| ~ sP10(X0)
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u142,negated_conjecture,
~ p103(sK22) ).
cnf(u1859,negated_conjecture,
( ~ r1(sK19(sK20(sK22)),X0)
| sP11(X0) ) ).
cnf(u7644,negated_conjecture,
sP10(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7648,negated_conjecture,
sP3(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7332,negated_conjecture,
sP4(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u5777,negated_conjecture,
p2(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u745,negated_conjecture,
sP5(sK18(sK21(sK22))) ).
cnf(u6824,negated_conjecture,
sP5(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u3604,negated_conjecture,
sP11(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u2859,negated_conjecture,
sP9(sK17(sK19(sK20(sK22)))) ).
cnf(u7640,negated_conjecture,
sP6(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u334,axiom,
( ~ p105(sK16(X0))
| ~ p6(sK16(X0))
| p6(X0)
| ~ p105(X0)
| ~ sP10(X0)
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u734,negated_conjecture,
sP10(sK19(sK21(sK22))) ).
cnf(u1967,negated_conjecture,
sP0(sK18(sK20(sK22))) ).
cnf(u2565,negated_conjecture,
p2(sK16(sK19(sK21(sK22)))) ).
cnf(u8510,negated_conjecture,
p3(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7196,negated_conjecture,
sP3(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u293,negated_conjecture,
sP9(sK20(sK22)) ).
cnf(u1989,negated_conjecture,
( ~ r1(sK17(sK19(sK20(sK22))),X0)
| sP11(X0) ) ).
cnf(u2414,negated_conjecture,
sP11(sK17(sK19(sK21(sK22)))) ).
cnf(u3172,negated_conjecture,
sP5(sK17(sK18(sK21(sK22)))) ).
cnf(u63,axiom,
( ~ sP11(X0)
| sP0(X0) ) ).
cnf(u6879,negated_conjecture,
sP4(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u428,axiom,
( ~ p101(sK14(X0))
| p2(sK14(X0))
| ~ p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u7322,negated_conjecture,
sP5(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7007,negated_conjecture,
sP8(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u6601,negated_conjecture,
sP10(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u379,axiom,
( ~ p103(sK21(X0))
| p4(sK21(X0))
| ~ p4(X0)
| ~ p103(X0)
| ~ sP8(X0)
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u730,negated_conjecture,
sP6(sK19(sK21(sK22))) ).
cnf(u8847,negated_conjecture,
p4(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u8206,negated_conjecture,
p4(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u7511,negated_conjecture,
sP1(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u6464,negated_conjecture,
sP8(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u7052,negated_conjecture,
sP7(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7467,negated_conjecture,
sP3(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u6834,negated_conjecture,
sP4(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u1931,negated_conjecture,
sP5(sK19(sK20(sK22))) ).
cnf(u135,negated_conjecture,
sP2(sK22) ).
cnf(u6193,negated_conjecture,
sP7(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u6326,negated_conjecture,
sP5(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u7734,negated_conjecture,
sP10(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u8585,negated_conjecture,
p4(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7865,negated_conjecture,
p3(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u5324,negated_conjecture,
sP7(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u5464,negated_conjecture,
sP6(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u3113,negated_conjecture,
sP10(sK16(sK18(sK20(sK22)))) ).
cnf(u8384,negated_conjecture,
p2(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u7690,negated_conjecture,
sP0(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u146,negated_conjecture,
~ p105(sK22) ).
cnf(u2952,negated_conjecture,
sP6(sK16(sK19(sK20(sK22)))) ).
cnf(u2606,negated_conjecture,
sP11(sK16(sK18(sK20(sK22)))) ).
cnf(u436,axiom,
( ~ p101(sK19(X0))
| p2(sK19(X0))
| ~ p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p102(X0)
| ~ sP1(X0) ) ).
cnf(u131,negated_conjecture,
sP9(sK22) ).
cnf(u6875,negated_conjecture,
sP0(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u8891,negated_conjecture,
p5(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7189,negated_conjecture,
sP7(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7236,negated_conjecture,
sP9(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u240,negated_conjecture,
sP2(sK21(sK22)) ).
cnf(u8120,negated_conjecture,
p3(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u394,axiom,
( ~ p4(sK15(X0))
| ~ p103(sK15(X0))
| p4(X0)
| ~ p103(X0)
| ~ sP8(X0)
| p104(X0)
| ~ sP3(X0) ) ).
cnf(u7238,negated_conjecture,
sP0(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u5396,negated_conjecture,
sP10(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u6921,negated_conjecture,
sP1(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u353,axiom,
( ~ p104(sK12(X0))
| p5(sK12(X0))
| ~ p5(X0)
| ~ p104(X0)
| ~ sP9(X0)
| p105(X0)
| ~ sP4(X0) ) ).
cnf(u223,negated_conjecture,
( ~ r1(sK20(sK22),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP11(X2) ) ).
cnf(u7059,negated_conjecture,
sP3(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7194,negated_conjecture,
sP1(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u123,negated_conjecture,
( ~ r1(sK22,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP11(X2) ) ).
cnf(u5431,negated_conjecture,
p2(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u6420,negated_conjecture,
sP9(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u7327,negated_conjecture,
sP10(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7102,negated_conjecture,
sP0(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u459,axiom,
( ~ p100(sK17(X0))
| p1(sK17(X0))
| ~ p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u7106,negated_conjecture,
sP4(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u7283,negated_conjecture,
sP0(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u237,negated_conjecture,
sP10(sK21(sK22)) ).
cnf(u7368,negated_conjecture,
sP6(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u6924,negated_conjecture,
sP4(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u365,axiom,
( ~ p5(sK21(X0))
| ~ p104(sK21(X0))
| p5(X0)
| ~ p104(X0)
| ~ sP9(X0)
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u296,negated_conjecture,
sP1(sK20(sK22)) ).
cnf(u1858,negated_conjecture,
( ~ r1(sK18(sK20(sK22)),X0)
| ~ r1(X0,X1)
| sP11(X1) ) ).
cnf(u7508,negated_conjecture,
sP9(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u6642,negated_conjecture,
sP5(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u7872,negated_conjecture,
p2(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6961,negated_conjecture,
sP7(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u7325,negated_conjecture,
sP8(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u116,axiom,
( ~ p2(sK20(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u471,axiom,
( ~ p1(sK15(X0))
| ~ p100(sK15(X0))
| p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u6062,negated_conjecture,
sP9(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u8214,negated_conjecture,
p2(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u8727,negated_conjecture,
p3(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u233,negated_conjecture,
sP6(sK21(sK22)) ).
cnf(u7460,negated_conjecture,
sP7(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u6877,negated_conjecture,
sP2(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u5325,negated_conjecture,
sP8(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u7374,negated_conjecture,
sP1(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7005,negated_conjecture,
sP6(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u6372,negated_conjecture,
sP6(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u222,negated_conjecture,
( ~ r1(sK20(sK22),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP11(X3) ) ).
cnf(u2410,negated_conjecture,
( ~ r1(sK17(sK19(sK21(sK22))),X0)
| ~ r1(X0,X1)
| sP11(X1) ) ).
cnf(u8199,negated_conjecture,
p5(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u112,axiom,
( p2(sK21(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u132,negated_conjecture,
sP10(sK22) ).
cnf(u731,negated_conjecture,
sP7(sK19(sK21(sK22))) ).
cnf(u335,axiom,
( ~ p105(sK17(X0))
| ~ p6(sK17(X0))
| p6(X0)
| ~ p105(X0)
| ~ sP10(X0)
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u414,axiom,
( ~ p3(sK14(X0))
| ~ p102(sK14(X0))
| p3(X0)
| ~ p102(X0)
| ~ sP7(X0)
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u3214,negated_conjecture,
sP10(sK16(sK18(sK21(sK22)))) ).
cnf(u6696,negated_conjecture,
sP2(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u7060,negated_conjecture,
sP4(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u2587,negated_conjecture,
sP11(sK17(sK19(sK20(sK22)))) ).
cnf(u6736,negated_conjecture,
sP7(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6334,negated_conjecture,
sP2(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u124,negated_conjecture,
( ~ r1(sK22,X0)
| ~ r1(X0,X1)
| sP11(X1) ) ).
cnf(u479,axiom,
( ~ p1(sK20(X0))
| ~ p100(sK20(X0))
| p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p101(X0)
| ~ sP0(X0) ) ).
cnf(u278,axiom,
( ~ p105(sK17(X0))
| p6(sK17(X0))
| ~ p6(X0)
| ~ p105(X0)
| ~ sP10(X0)
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u7552,negated_conjecture,
sP8(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u109,axiom,
( r1(X0,sK18(X0))
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u241,negated_conjecture,
sP3(sK21(sK22)) ).
cnf(u7240,negated_conjecture,
sP2(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u5601,negated_conjecture,
sP7(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u7596,negated_conjecture,
sP7(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u6507,negated_conjecture,
sP6(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u7375,negated_conjecture,
sP2(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u6514,negated_conjecture,
sP2(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6511,negated_conjecture,
sP10(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u2857,negated_conjecture,
sP7(sK17(sK19(sK20(sK22)))) ).
cnf(u7197,negated_conjecture,
sP4(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u120,negated_conjecture,
( ~ r1(sK22,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP11(X5) ) ).
cnf(u7011,negated_conjecture,
sP1(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u8042,negated_conjecture,
p2(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u105,axiom,
( r1(X0,sK19(X0))
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u1017,negated_conjecture,
( ~ r1(sK19(sK21(sK22)),X0)
| sP11(X0) ) ).
cnf(u6191,negated_conjecture,
sP5(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u1860,negated_conjecture,
( ~ r1(sK18(sK20(sK22)),X0)
| sP11(X0) ) ).
cnf(u6556,negated_conjecture,
sP10(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u5258,negated_conjecture,
sP9(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u5255,negated_conjecture,
sP6(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u94,axiom,
( p103(sK17(X0))
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u226,negated_conjecture,
sP11(sK20(sK22)) ).
cnf(u2860,negated_conjecture,
sP10(sK17(sK19(sK20(sK22)))) ).
cnf(u7419,negated_conjecture,
sP1(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u6470,negated_conjecture,
sP3(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6872,negated_conjecture,
sP8(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6373,negated_conjecture,
sP7(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u339,axiom,
( ~ p105(sK21(X0))
| ~ p6(sK21(X0))
| p6(X0)
| ~ p105(X0)
| ~ sP10(X0)
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u7242,negated_conjecture,
sP4(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u6416,negated_conjecture,
sP5(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u117,axiom,
( r1(X0,sK20(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u2528,negated_conjecture,
sP8(sK16(sK19(sK21(sK22)))) ).
cnf(u474,axiom,
( ~ p1(sK18(X0))
| ~ p100(sK18(X0))
| p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u7376,negated_conjecture,
sP3(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u3022,negated_conjecture,
sP7(sK17(sK18(sK20(sK22)))) ).
cnf(u1941,negated_conjecture,
sP4(sK19(sK20(sK22))) ).
cnf(u5737,negated_conjecture,
sP5(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u90,axiom,
( p104(sK14(X0))
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u6920,negated_conjecture,
sP0(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u380,axiom,
( ~ p103(sK15(X0))
| p4(sK15(X0))
| ~ p4(X0)
| ~ p103(X0)
| ~ sP8(X0)
| p104(X0)
| ~ sP3(X0) ) ).
cnf(u384,axiom,
( ~ p4(sK12(X0))
| ~ p103(sK12(X0))
| p4(X0)
| ~ p103(X0)
| ~ sP8(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u6650,negated_conjecture,
sP2(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u75,axiom,
( ~ r1(X0,X1)
| ~ p3(X1)
| ~ p102(X1)
| p3(X0)
| ~ p102(X0)
| ~ sP7(X0) ) ).
cnf(u3109,negated_conjecture,
sP6(sK16(sK18(sK20(sK22)))) ).
cnf(u7689,negated_conjecture,
sP10(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u6142,negated_conjecture,
sP8(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u95,axiom,
( ~ p104(sK17(X0))
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u204,negated_conjecture,
( ~ r1(sK21(sK22),X0)
| ~ r1(X0,X1)
| sP11(X1) ) ).
cnf(u113,axiom,
( r1(X0,sK21(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u7468,negated_conjecture,
sP4(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u6327,negated_conjecture,
sP6(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u102,axiom,
( p102(sK19(X0))
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u7013,negated_conjecture,
sP3(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u6380,negated_conjecture,
sP3(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u445,axiom,
( ~ p2(sK17(X0))
| ~ p101(sK17(X0))
| p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u6827,negated_conjecture,
sP8(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u1938,negated_conjecture,
sP1(sK19(sK20(sK22))) ).
cnf(u87,axiom,
( ~ p105(sK15(X0))
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u729,negated_conjecture,
sP5(sK19(sK21(sK22))) ).
cnf(u6831,negated_conjecture,
sP1(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u3175,negated_conjecture,
sP8(sK17(sK18(sK21(sK22)))) ).
cnf(u6959,negated_conjecture,
sP5(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u7190,negated_conjecture,
sP8(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u1990,negated_conjecture,
( ~ r1(sK16(sK19(sK20(sK22))),X0)
| sP11(X0) ) ).
cnf(u6279,negated_conjecture,
sP5(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u5558,negated_conjecture,
p2(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u7054,negated_conjecture,
sP9(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u98,axiom,
( p103(sK16(X0))
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u7235,negated_conjecture,
sP8(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u441,axiom,
( ~ p2(sK13(X0))
| ~ p101(sK13(X0))
| p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u83,axiom,
( p105(sK12(X0))
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u5929,negated_conjecture,
sP9(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u6606,negated_conjecture,
sP4(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u5525,negated_conjecture,
sP8(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u8550,negated_conjecture,
p4(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u64,axiom,
( ~ sP11(X0)
| sP1(X0) ) ).
cnf(u6914,negated_conjecture,
sP5(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u415,axiom,
( ~ p3(sK15(X0))
| ~ p102(sK15(X0))
| p3(X0)
| ~ p102(X0)
| ~ sP7(X0)
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u2954,negated_conjecture,
sP8(sK16(sK19(sK20(sK22)))) ).
cnf(u6466,negated_conjecture,
sP10(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u2856,negated_conjecture,
sP6(sK17(sK19(sK20(sK22)))) ).
cnf(u460,axiom,
( ~ p100(sK18(X0))
| p1(sK18(X0))
| ~ p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u6195,negated_conjecture,
sP9(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u76,axiom,
( ~ r1(X0,X2)
| p2(X2)
| ~ p101(X2)
| ~ p2(X0)
| ~ p101(X0)
| ~ sP6(X0) ) ).
cnf(u3814,negated_conjecture,
sP11(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u5522,negated_conjecture,
sP5(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u8719,negated_conjecture,
p5(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u6923,negated_conjecture,
sP3(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u8686,negated_conjecture,
p3(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u6180,negated_conjecture,
p4(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u7602,negated_conjecture,
sP2(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7599,negated_conjecture,
sP10(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u5599,negated_conjecture,
sP5(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u456,axiom,
( ~ p100(sK14(X0))
| p1(sK14(X0))
| ~ p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u6828,negated_conjecture,
sP9(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u291,negated_conjecture,
sP7(sK20(sK22)) ).
cnf(u72,axiom,
( ~ r1(X0,X2)
| p4(X2)
| ~ p103(X2)
| ~ p4(X0)
| ~ p103(X0)
| ~ sP8(X0) ) ).
cnf(u6425,negated_conjecture,
sP3(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u423,axiom,
( ~ p3(sK16(X0))
| ~ p102(sK16(X0))
| p3(X0)
| ~ p102(X0)
| ~ sP7(X0)
| p103(X0)
| ~ sP2(X0) ) ).
cnf(u7279,negated_conjecture,
sP7(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u754,negated_conjecture,
sP3(sK18(sK21(sK22))) ).
cnf(u1940,negated_conjecture,
sP3(sK19(sK20(sK22))) ).
cnf(u6509,negated_conjecture,
sP8(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6059,negated_conjecture,
sP6(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u814,negated_conjecture,
( ~ r1(sK18(sK21(sK22)),X0)
| ~ r1(X0,X1)
| sP11(X1) ) ).
cnf(u7414,negated_conjecture,
sP7(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u468,axiom,
( ~ p1(sK12(X0))
| ~ p100(sK12(X0))
| p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u5794,negated_conjecture,
sP9(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u2951,negated_conjecture,
sP5(sK16(sK19(sK20(sK22)))) ).
cnf(u1854,negated_conjecture,
( ~ r1(sK18(sK20(sK22)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP11(X2) ) ).
cnf(u7192,negated_conjecture,
sP10(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u366,axiom,
( ~ p5(sK13(X0))
| ~ p104(sK13(X0))
| p5(X0)
| ~ p104(X0)
| ~ sP9(X0)
| p105(X0)
| ~ sP4(X0) ) ).
cnf(u766,negated_conjecture,
p2(sK18(sK21(sK22))) ).
cnf(u2529,negated_conjecture,
sP9(sK16(sK19(sK21(sK22)))) ).
cnf(u69,axiom,
( ~ r1(X0,X1)
| ~ p6(X1)
| ~ p105(X1)
| p6(X0)
| ~ p105(X0)
| ~ sP10(X0) ) ).
cnf(u735,negated_conjecture,
sP0(sK19(sK21(sK22))) ).
cnf(u61,axiom,
( ~ sP11(X0)
| sP9(X0) ) ).
cnf(u5872,negated_conjecture,
sP10(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u7412,negated_conjecture,
sP5(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u6463,negated_conjecture,
sP7(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6829,negated_conjecture,
sP10(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u3211,negated_conjecture,
sP7(sK16(sK18(sK21(sK22)))) ).
cnf(u385,axiom,
( ~ p4(sK13(X0))
| ~ p103(sK13(X0))
| p4(X0)
| ~ p103(X0)
| ~ sP8(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u3020,negated_conjecture,
sP5(sK17(sK18(sK20(sK22)))) ).
cnf(u6963,negated_conjecture,
sP9(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u464,axiom,
( ~ p100(sK21(X0))
| p1(sK21(X0))
| ~ p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p101(X0)
| ~ sP0(X0) ) ).
cnf(u5254,negated_conjecture,
sP5(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u5463,negated_conjecture,
sP5(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u6967,negated_conjecture,
sP2(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u5394,negated_conjecture,
sP8(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u6561,negated_conjecture,
sP4(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6508,negated_conjecture,
sP7(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u5438,negated_conjecture,
p3(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u6196,negated_conjecture,
sP10(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u65,axiom,
( ~ sP11(X0)
| sP2(X0) ) ).
cnf(u6689,negated_conjecture,
sP6(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u8927,negated_conjecture,
p4(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u5795,negated_conjecture,
sP10(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u3709,negated_conjecture,
sP11(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u7012,negated_conjecture,
sP2(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u7466,negated_conjecture,
sP2(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u6738,negated_conjecture,
sP9(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u7144,negated_conjecture,
sP7(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u8005,negated_conjecture,
p2(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u7686,negated_conjecture,
sP7(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u295,negated_conjecture,
sP0(sK20(sK22)) ).
cnf(u6602,negated_conjecture,
sP0(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u57,axiom,
( ~ sP11(X0)
| sP5(X0) ) ).
cnf(u2029,negated_conjecture,
( ~ r1(sK16(sK18(sK20(sK22))),X0)
| sP11(X0) ) ).
cnf(u6331,negated_conjecture,
sP10(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6694,negated_conjecture,
sP0(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u393,axiom,
( ~ p4(sK21(X0))
| ~ p103(sK21(X0))
| p4(X0)
| ~ p103(X0)
| ~ sP8(X0)
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u5928,negated_conjecture,
sP8(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u5602,negated_conjecture,
sP8(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u5914,negated_conjecture,
p4(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u144,negated_conjecture,
~ p104(sK22) ).
cnf(u1934,negated_conjecture,
sP8(sK19(sK20(sK22))) ).
cnf(u6645,negated_conjecture,
sP8(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u426,axiom,
( ~ p101(sK12(X0))
| p2(sK12(X0))
| ~ p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u7554,negated_conjecture,
sP10(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u5980,negated_conjecture,
p3(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u137,negated_conjecture,
sP4(sK22) ).
cnf(u720,negated_conjecture,
( ~ r1(sK19(sK21(sK22)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP11(X2) ) ).
cnf(u6783,negated_conjecture,
sP9(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u5510,negated_conjecture,
p3(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u7416,negated_conjecture,
sP9(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u6377,negated_conjecture,
sP0(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u2526,negated_conjecture,
sP6(sK16(sK19(sK21(sK22)))) ).
cnf(u3212,negated_conjecture,
sP8(sK16(sK18(sK21(sK22)))) ).
cnf(u1018,negated_conjecture,
( ~ r1(sK18(sK21(sK22)),X0)
| sP11(X0) ) ).
cnf(u5466,negated_conjecture,
sP8(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u1857,negated_conjecture,
( ~ r1(sK19(sK20(sK22)),X0)
| ~ r1(X0,X1)
| sP11(X1) ) ).
cnf(u721,negated_conjecture,
( ~ r1(sK18(sK21(sK22)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP11(X2) ) ).
cnf(u2485,negated_conjecture,
sP6(sK17(sK19(sK21(sK22)))) ).
cnf(u6009,negated_conjecture,
sP9(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u7287,negated_conjecture,
sP4(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u2413,negated_conjecture,
( ~ r1(sK16(sK19(sK21(sK22))),X0)
| sP11(X0) ) ).
cnf(u6966,negated_conjecture,
sP1(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u7006,negated_conjecture,
sP7(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u3110,negated_conjecture,
sP7(sK16(sK18(sK20(sK22)))) ).
cnf(u5925,negated_conjecture,
sP5(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u7187,negated_conjecture,
sP5(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u3108,negated_conjecture,
sP5(sK16(sK18(sK20(sK22)))) ).
cnf(u54,axiom,
( ~ sP11(X0)
| ~ p103(X0)
| p102(X0) ) ).
cnf(u7738,negated_conjecture,
sP3(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u732,negated_conjecture,
sP8(sK19(sK21(sK22))) ).
cnf(u6061,negated_conjecture,
sP8(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u6558,negated_conjecture,
sP1(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u7691,negated_conjecture,
sP1(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7513,negated_conjecture,
sP3(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u733,negated_conjecture,
sP9(sK19(sK21(sK22))) ).
cnf(u5326,negated_conjecture,
sP9(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u5297,negated_conjecture,
p3(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u7281,negated_conjecture,
sP9(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u6604,negated_conjecture,
sP2(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6965,negated_conjecture,
sP0(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u6332,negated_conjecture,
sP0(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u5660,negated_conjecture,
sP8(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u6058,negated_conjecture,
sP5(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u6779,negated_conjecture,
sP5(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6919,negated_conjecture,
sP10(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u451,axiom,
( ~ p2(sK18(X0))
| ~ p101(sK18(X0))
| p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p102(X0)
| ~ sP1(X0) ) ).
cnf(u7598,negated_conjecture,
sP9(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u367,axiom,
( ~ p5(sK12(X0))
| ~ p104(sK12(X0))
| p5(X0)
| ~ p104(X0)
| ~ sP9(X0)
| p105(X0)
| ~ sP4(X0) ) ).
cnf(u298,negated_conjecture,
sP3(sK20(sK22)) ).
cnf(u2772,negated_conjecture,
sP11(sK16(sK18(sK21(sK22)))) ).
cnf(u6192,negated_conjecture,
sP6(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u277,axiom,
( ~ p105(sK16(X0))
| p6(sK16(X0))
| ~ p6(X0)
| ~ p105(X0)
| ~ sP10(X0)
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u6336,negated_conjecture,
sP4(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u7152,negated_conjecture,
sP4(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u8127,negated_conjecture,
p2(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u465,axiom,
( ~ p100(sK20(X0))
| p1(sK20(X0))
| ~ p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p101(X0)
| ~ sP0(X0) ) ).
cnf(u412,axiom,
( ~ p3(sK12(X0))
| ~ p102(sK12(X0))
| p3(X0)
| ~ p102(X0)
| ~ sP7(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u6139,negated_conjecture,
sP5(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u235,negated_conjecture,
sP8(sK21(sK22)) ).
cnf(u7649,negated_conjecture,
sP4(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u8770,negated_conjecture,
p3(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7955,negated_conjecture,
p2(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u2955,negated_conjecture,
sP9(sK16(sK19(sK20(sK22)))) ).
cnf(u363,axiom,
( ~ p5(sK19(X0))
| ~ p104(sK19(X0))
| p5(X0)
| ~ p104(X0)
| ~ sP9(X0)
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u5790,negated_conjecture,
sP5(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u7735,negated_conjecture,
sP0(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u2028,negated_conjecture,
( ~ r1(sK17(sK18(sK20(sK22))),X0)
| sP11(X0) ) ).
cnf(u7188,negated_conjecture,
sP6(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7329,negated_conjecture,
sP1(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u6555,negated_conjecture,
sP9(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6559,negated_conjecture,
sP2(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u134,negated_conjecture,
sP1(sK22) ).
cnf(u6378,negated_conjecture,
sP1(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u7420,negated_conjecture,
sP2(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u6418,negated_conjecture,
sP7(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u7105,negated_conjecture,
sP3(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u408,axiom,
( ~ p102(sK17(X0))
| p3(sK17(X0))
| ~ p3(X0)
| ~ p102(X0)
| ~ sP7(X0)
| p103(X0)
| ~ sP2(X0) ) ).
cnf(u6008,negated_conjecture,
sP8(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u6787,negated_conjecture,
sP2(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u1971,negated_conjecture,
sP4(sK18(sK20(sK22))) ).
cnf(u6915,negated_conjecture,
sP6(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6597,negated_conjecture,
sP6(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u7422,negated_conjecture,
sP4(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u3112,negated_conjecture,
sP9(sK16(sK18(sK20(sK22)))) ).
cnf(u2488,negated_conjecture,
sP9(sK17(sK19(sK21(sK22)))) ).
cnf(u6060,negated_conjecture,
sP7(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u6781,negated_conjecture,
sP7(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u7278,negated_conjecture,
sP6(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u203,negated_conjecture,
( ~ r1(sK21(sK22),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP11(X2) ) ).
cnf(u5290,negated_conjecture,
p2(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u126,negated_conjecture,
sP11(sK22) ).
cnf(u130,negated_conjecture,
sP5(sK22) ).
cnf(u5930,negated_conjecture,
sP10(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u473,axiom,
( ~ p1(sK17(X0))
| ~ p100(sK17(X0))
| p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u6830,negated_conjecture,
sP0(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u7323,negated_conjecture,
sP6(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u4444,negated_conjecture,
sP11(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u1856,negated_conjecture,
sP11(sK18(sK20(sK22))) ).
cnf(u7239,negated_conjecture,
sP1(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u5323,negated_conjecture,
sP6(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u458,axiom,
( ~ p100(sK16(X0))
| p1(sK16(X0))
| ~ p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u371,axiom,
( ~ p103(sK13(X0))
| p4(sK13(X0))
| ~ p4(X0)
| ~ p103(X0)
| ~ sP8(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u224,negated_conjecture,
( ~ r1(sK20(sK22),X0)
| ~ r1(X0,X1)
| sP11(X1) ) ).
cnf(u8027,negated_conjecture,
p5(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u7815,negated_conjecture,
p4(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6141,negated_conjecture,
sP7(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u6962,negated_conjecture,
sP8(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u6964,negated_conjecture,
sP10(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u6690,negated_conjecture,
sP7(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u7096,negated_conjecture,
sP5(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u122,negated_conjecture,
( ~ r1(sK22,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP11(X3) ) ).
cnf(u337,axiom,
( ~ p105(sK19(X0))
| ~ p6(sK19(X0))
| p6(X0)
| ~ p105(X0)
| ~ sP10(X0)
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u100,axiom,
( ~ p4(sK16(X0))
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u2771,negated_conjecture,
sP11(sK17(sK18(sK21(sK22)))) ).
cnf(u7693,negated_conjecture,
sP3(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u6554,negated_conjecture,
sP8(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u107,axiom,
( ~ p103(sK18(X0))
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u470,axiom,
( ~ p1(sK14(X0))
| ~ p100(sK14(X0))
| p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u7600,negated_conjecture,
sP0(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u8985,negated_conjecture,
p4(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u1964,negated_conjecture,
sP8(sK18(sK20(sK22))) ).
cnf(u1937,negated_conjecture,
sP0(sK19(sK20(sK22))) ).
cnf(u236,negated_conjecture,
sP9(sK21(sK22)) ).
cnf(u115,axiom,
( ~ p102(sK20(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u5662,negated_conjecture,
sP10(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u6789,negated_conjecture,
sP4(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6375,negated_conjecture,
sP9(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6917,negated_conjecture,
sP8(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6284,negated_conjecture,
sP10(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u349,axiom,
( ~ p104(sK19(X0))
| p5(sK19(X0))
| ~ p5(X0)
| ~ p104(X0)
| ~ sP9(X0)
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u280,axiom,
( ~ p105(sK19(X0))
| p6(sK19(X0))
| ~ p6(X0)
| ~ p105(X0)
| ~ sP10(X0)
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u1970,negated_conjecture,
sP3(sK18(sK20(sK22))) ).
cnf(u119,negated_conjecture,
~ p101(sK22) ).
cnf(u750,negated_conjecture,
sP10(sK18(sK21(sK22))) ).
cnf(u6735,negated_conjecture,
sP6(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6469,negated_conjecture,
sP2(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u7557,negated_conjecture,
sP2(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u8299,negated_conjecture,
p2(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6788,negated_conjecture,
sP3(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6786,negated_conjecture,
sP1(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u232,negated_conjecture,
sP5(sK21(sK22)) ).
cnf(u455,axiom,
( ~ p100(sK13(X0))
| p1(sK13(X0))
| ~ p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u6513,negated_conjecture,
sP1(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6005,negated_conjecture,
sP5(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u7146,negated_conjecture,
sP9(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u292,negated_conjecture,
sP8(sK20(sK22)) ).
cnf(u206,negated_conjecture,
sP11(sK21(sK22)) ).
cnf(u7829,negated_conjecture,
p2(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u8635,negated_conjecture,
p4(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7415,negated_conjecture,
sP8(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7324,negated_conjecture,
sP7(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u5257,negated_conjecture,
sP8(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u96,axiom,
( p4(sK17(X0))
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u7459,negated_conjecture,
sP6(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u6695,negated_conjecture,
sP1(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u5385,negated_conjecture,
p4(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u378,axiom,
( ~ p103(sK20(X0))
| p4(sK20(X0))
| ~ p4(X0)
| ~ p103(X0)
| ~ sP8(X0)
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u7280,negated_conjecture,
sP8(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u398,axiom,
( ~ p102(sK12(X0))
| p3(sK12(X0))
| ~ p3(X0)
| ~ p102(X0)
| ~ sP7(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u6968,negated_conjecture,
sP3(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u7509,negated_conjecture,
sP10(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7906,negated_conjecture,
p3(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u7739,negated_conjecture,
sP4(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7465,negated_conjecture,
sP1(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u6426,negated_conjecture,
sP4(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u202,negated_conjecture,
( ~ r1(sK21(sK22),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP11(X3) ) ).
cnf(u6371,negated_conjecture,
sP5(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u127,negated_conjecture,
sP8(sK22) ).
cnf(u8084,negated_conjecture,
p3(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u7277,negated_conjecture,
sP5(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u7143,negated_conjecture,
sP6(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u3499,negated_conjecture,
sP11(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u108,axiom,
( ~ p3(sK18(X0))
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u443,axiom,
( ~ p2(sK15(X0))
| ~ p101(sK15(X0))
| p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u7899,negated_conjecture,
p4(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u7372,negated_conjecture,
sP10(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7004,negated_conjecture,
sP5(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u5523,negated_conjecture,
sP6(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u93,axiom,
( r1(X0,sK14(X0))
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u7998,negated_conjecture,
p3(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u225,negated_conjecture,
( ~ r1(sK20(sK22),X0)
| sP11(X0) ) ).
cnf(u7647,negated_conjecture,
sP2(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u6600,negated_conjecture,
sP9(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6010,negated_conjecture,
sP10(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u6144,negated_conjecture,
sP10(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u7550,negated_conjecture,
sP6(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u6737,negated_conjecture,
sP8(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6329,negated_conjecture,
sP8(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u7104,negated_conjecture,
sP2(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u104,axiom,
( p3(sK19(X0))
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u813,negated_conjecture,
( ~ r1(sK19(sK21(sK22)),X0)
| ~ r1(X0,X1)
| sP11(X1) ) ).
cnf(u5927,negated_conjecture,
sP7(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u3287,negated_conjecture,
sP11(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u8035,negated_conjecture,
p3(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u7463,negated_conjecture,
sP10(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u89,axiom,
( r1(X0,sK15(X0))
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u1853,negated_conjecture,
( ~ r1(sK19(sK20(sK22)),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP11(X2) ) ).
cnf(u6063,negated_conjecture,
sP10(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u3177,negated_conjecture,
sP10(sK17(sK18(sK21(sK22)))) ).
cnf(u5870,negated_conjecture,
sP8(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u78,axiom,
( ~ r1(X0,X2)
| p1(X2)
| ~ p100(X2)
| ~ p1(X0)
| ~ p100(X0)
| ~ sP5(X0) ) ).
cnf(u4234,negated_conjecture,
sP11(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u6510,negated_conjecture,
sP9(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u2953,negated_conjecture,
sP7(sK16(sK19(sK20(sK22)))) ).
cnf(u352,axiom,
( ~ p104(sK13(X0))
| p5(sK13(X0))
| ~ p5(X0)
| ~ p104(X0)
| ~ sP9(X0)
| p105(X0)
| ~ sP4(X0) ) ).
cnf(u3919,negated_conjecture,
sP11(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u1936,negated_conjecture,
sP10(sK19(sK20(sK22))) ).
cnf(u7822,negated_conjecture,
p3(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u101,axiom,
( r1(X0,sK16(X0))
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u2858,negated_conjecture,
sP8(sK17(sK19(sK20(sK22)))) ).
cnf(u6605,negated_conjecture,
sP3(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6140,negated_conjecture,
sP6(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u74,axiom,
( ~ r1(X0,X2)
| p3(X2)
| ~ p102(X2)
| ~ p3(X0)
| ~ p102(X0)
| ~ sP7(X0) ) ).
cnf(u7642,negated_conjecture,
sP8(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u3249,negated_conjecture,
p2(sK16(sK18(sK21(sK22)))) ).
cnf(u7330,negated_conjecture,
sP2(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u2956,negated_conjecture,
sP10(sK16(sK19(sK20(sK22)))) ).
cnf(u364,axiom,
( ~ p5(sK20(X0))
| ~ p104(sK20(X0))
| p5(X0)
| ~ p104(X0)
| ~ sP9(X0)
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u3025,negated_conjecture,
sP10(sK17(sK18(sK20(sK22)))) ).
cnf(u5926,negated_conjecture,
sP6(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u6465,negated_conjecture,
sP9(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u5395,negated_conjecture,
sP9(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u97,axiom,
( r1(X0,sK17(X0))
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u297,negated_conjecture,
sP2(sK20(sK22)) ).
cnf(u6782,negated_conjecture,
sP8(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u7328,negated_conjecture,
sP0(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u86,axiom,
( p104(sK15(X0))
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u8814,negated_conjecture,
p3(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u429,axiom,
( ~ p101(sK15(X0))
| p2(sK15(X0))
| ~ p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u6916,negated_conjecture,
sP7(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u6878,negated_conjecture,
sP3(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u71,axiom,
( ~ r1(X0,X1)
| ~ p5(X1)
| ~ p104(X1)
| p5(X0)
| ~ p104(X0)
| ~ sP9(X0) ) ).
cnf(u6744,negated_conjecture,
sP4(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u7851,negated_conjecture,
p5(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u4129,negated_conjecture,
sP11(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u7601,negated_conjecture,
sP1(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7729,negated_conjecture,
sP5(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u6379,negated_conjecture,
sP2(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u4024,negated_conjecture,
sP11(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u7948,negated_conjecture,
p3(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u5742,negated_conjecture,
sP10(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u1933,negated_conjecture,
sP7(sK19(sK20(sK22))) ).
cnf(u82,axiom,
( r1(X0,sK13(X0))
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u6869,negated_conjecture,
sP5(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u7284,negated_conjecture,
sP1(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u67,axiom,
( ~ sP11(X0)
| sP4(X0) ) ).
cnf(u7694,negated_conjecture,
sP4(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7057,negated_conjecture,
sP1(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u8263,negated_conjecture,
p2(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u2768,negated_conjecture,
( ~ r1(sK16(sK18(sK21(sK22))),X0)
| ~ r1(X0,X1)
| sP11(X1) ) ).
cnf(u1966,negated_conjecture,
sP10(sK18(sK20(sK22))) ).
cnf(u399,axiom,
( ~ p102(sK13(X0))
| p3(sK13(X0))
| ~ p3(X0)
| ~ p102(X0)
| ~ sP7(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u478,axiom,
( ~ p1(sK21(X0))
| ~ p100(sK21(X0))
| p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p101(X0)
| ~ sP0(X0) ) ).
cnf(u7646,negated_conjecture,
sP1(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7514,negated_conjecture,
sP4(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u752,negated_conjecture,
sP1(sK18(sK21(sK22))) ).
cnf(u289,negated_conjecture,
sP5(sK20(sK22)) ).
cnf(u2769,negated_conjecture,
( ~ r1(sK17(sK18(sK21(sK22))),X0)
| sP11(X0) ) ).
cnf(u437,axiom,
( ~ p101(sK18(X0))
| p2(sK18(X0))
| ~ p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p102(X0)
| ~ sP1(X0) ) ).
cnf(u6281,negated_conjecture,
sP7(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u59,axiom,
( ~ sP11(X0)
| sP7(X0) ) ).
cnf(u79,axiom,
( ~ r1(X0,X1)
| ~ p1(X1)
| ~ p100(X1)
| p1(X0)
| ~ p100(X0)
| ~ sP5(X0) ) ).
cnf(u8159,negated_conjecture,
p4(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u2486,negated_conjecture,
sP7(sK17(sK19(sK21(sK22)))) ).
cnf(u6553,negated_conjecture,
sP7(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u753,negated_conjecture,
sP2(sK18(sK21(sK22))) ).
cnf(u395,axiom,
( ~ p4(sK14(X0))
| ~ p103(sK14(X0))
| p4(X0)
| ~ p103(X0)
| ~ sP8(X0)
| p104(X0)
| ~ sP3(X0) ) ).
cnf(u6143,negated_conjecture,
sP9(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u52,axiom,
( ~ sP11(X0)
| ~ p101(X0)
| p100(X0) ) ).
cnf(u7098,negated_conjecture,
sP7(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u3203,negated_conjecture,
p2(sK17(sK18(sK21(sK22)))) ).
cnf(u5837,negated_conjecture,
p3(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u5871,negated_conjecture,
sP9(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u5465,negated_conjecture,
sP7(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u6643,negated_conjecture,
sP6(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u7232,negated_conjecture,
sP5(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u8353,negated_conjecture,
p2(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u5793,negated_conjecture,
sP8(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u7417,negated_conjecture,
sP10(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u6647,negated_conjecture,
sP10(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u5600,negated_conjecture,
sP6(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u6506,negated_conjecture,
sP5(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6194,negated_conjecture,
sP8(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u7147,negated_conjecture,
sP10(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7461,negated_conjecture,
sP8(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u338,axiom,
( ~ p105(sK20(X0))
| ~ p6(sK20(X0))
| p6(X0)
| ~ p105(X0)
| ~ sP10(X0)
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u738,negated_conjecture,
sP3(sK19(sK21(sK22))) ).
cnf(u5792,negated_conjecture,
sP7(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u7736,negated_conjecture,
sP1(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u6741,negated_conjecture,
sP1(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u5603,negated_conjecture,
sP9(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u6873,negated_conjecture,
sP9(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u5322,negated_conjecture,
sP5(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u2487,negated_conjecture,
sP8(sK17(sK19(sK21(sK22)))) ).
cnf(u2415,negated_conjecture,
sP11(sK16(sK19(sK21(sK22)))) ).
cnf(u6421,negated_conjecture,
sP10(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u3024,negated_conjecture,
sP9(sK17(sK18(sK20(sK22)))) ).
cnf(u6006,negated_conjecture,
sP6(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u7555,negated_conjecture,
sP0(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u68,axiom,
( ~ r1(X0,X2)
| p6(X2)
| ~ p105(X2)
| ~ p6(X0)
| ~ p105(X0)
| ~ sP10(X0) ) ).
cnf(u290,negated_conjecture,
sP6(sK20(sK22)) ).
cnf(u6552,negated_conjecture,
sP6(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u350,axiom,
( ~ p104(sK20(X0))
| p5(sK20(X0))
| ~ p5(X0)
| ~ p104(X0)
| ~ sP9(X0)
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u7458,negated_conjecture,
sP5(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u6007,negated_conjecture,
sP7(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u5467,negated_conjecture,
sP9(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u7056,negated_conjecture,
sP0(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u2411,negated_conjecture,
( ~ r1(sK16(sK19(sK21(sK22))),X0)
| ~ r1(X0,X1)
| sP11(X1) ) ).
cnf(u5657,negated_conjecture,
sP5(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u444,axiom,
( ~ p2(sK16(X0))
| ~ p101(sK16(X0))
| p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u8471,negated_conjecture,
p2(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u5524,negated_conjecture,
sP7(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u7553,negated_conjecture,
sP9(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u3173,negated_conjecture,
sP6(sK17(sK18(sK21(sK22)))) ).
cnf(u60,axiom,
( ~ sP11(X0)
| sP8(X0) ) ).
cnf(u6330,negated_conjecture,
sP9(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u7737,negated_conjecture,
sP2(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u746,negated_conjecture,
sP6(sK18(sK21(sK22))) ).
cnf(u2525,negated_conjecture,
sP5(sK16(sK19(sK21(sK22)))) ).
cnf(u7604,negated_conjecture,
sP4(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7377,negated_conjecture,
sP4(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u6515,negated_conjecture,
sP3(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u1932,negated_conjecture,
sP6(sK19(sK20(sK22))) ).
cnf(u6462,negated_conjecture,
sP6(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u7858,negated_conjecture,
p4(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u4549,negated_conjecture,
sP11(sK15(sK17(sK18(sK20(sK22))))) ).
cnf(u5259,negated_conjecture,
sP10(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u440,axiom,
( ~ p2(sK12(X0))
| ~ p101(sK12(X0))
| p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u6688,negated_conjecture,
sP5(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u56,axiom,
( ~ sP11(X0)
| ~ p105(X0)
| p104(X0) ) ).
cnf(u7506,negated_conjecture,
sP7(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u279,axiom,
( ~ p105(sK18(X0))
| p6(sK18(X0))
| ~ p6(X0)
| ~ p105(X0)
| ~ sP10(X0)
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u1961,negated_conjecture,
sP5(sK18(sK20(sK22))) ).
cnf(u6557,negated_conjecture,
sP0(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6876,negated_conjecture,
sP1(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u7371,negated_conjecture,
sP9(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u6734,negated_conjecture,
sP5(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u5327,negated_conjecture,
sP10(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u8241,negated_conjecture,
p4(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u3393,negated_conjecture,
sP11(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u6424,negated_conjecture,
sP2(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6598,negated_conjecture,
sP7(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u128,negated_conjecture,
sP7(sK22) ).
cnf(u1855,negated_conjecture,
sP11(sK19(sK20(sK22))) ).
cnf(u53,axiom,
( ~ sP11(X0)
| ~ p102(X0)
| p101(X0) ) ).
cnf(u723,negated_conjecture,
sP11(sK18(sK21(sK22))) ).
cnf(u7597,negated_conjecture,
sP8(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7369,negated_conjecture,
sP7(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u6599,negated_conjecture,
sP8(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u7731,negated_conjecture,
sP7(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7641,negated_conjecture,
sP7(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u7504,negated_conjecture,
sP5(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7149,negated_conjecture,
sP1(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u140,negated_conjecture,
~ p102(sK22) ).
cnf(u475,axiom,
( ~ p1(sK19(X0))
| ~ p100(sK19(X0))
| p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u6335,negated_conjecture,
sP3(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u422,axiom,
( ~ p3(sK17(X0))
| ~ p102(sK17(X0))
| p3(X0)
| ~ p102(X0)
| ~ sP7(X0)
| p103(X0)
| ~ sP2(X0) ) ).
cnf(u4759,negated_conjecture,
sP11(sK15(sK16(sK18(sK20(sK22))))) ).
cnf(u7730,negated_conjecture,
sP6(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7195,negated_conjecture,
sP2(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u381,axiom,
( ~ p103(sK14(X0))
| p4(sK14(X0))
| ~ p4(X0)
| ~ p103(X0)
| ~ sP8(X0)
| p104(X0)
| ~ sP3(X0) ) ).
cnf(u7009,negated_conjecture,
sP10(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u6376,negated_conjecture,
sP10(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u6691,negated_conjecture,
sP8(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u7594,negated_conjecture,
sP5(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u6870,negated_conjecture,
sP6(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u7282,negated_conjecture,
sP10(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u751,negated_conjecture,
sP0(sK18(sK21(sK22))) ).
cnf(u3111,negated_conjecture,
sP8(sK16(sK18(sK20(sK22)))) ).
cnf(u136,negated_conjecture,
sP3(sK22) ).
cnf(u4654,negated_conjecture,
sP11(sK14(sK17(sK18(sK20(sK22))))) ).
cnf(u6417,negated_conjecture,
sP6(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u9067,negated_conjecture,
p5(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u6918,negated_conjecture,
sP9(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u7050,negated_conjecture,
sP5(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u3209,negated_conjecture,
sP5(sK16(sK18(sK21(sK22)))) ).
cnf(u238,negated_conjecture,
sP0(sK21(sK22)) ).
cnf(u2770,negated_conjecture,
( ~ r1(sK16(sK18(sK21(sK22))),X0)
| sP11(X0) ) ).
cnf(u5639,negated_conjecture,
p2(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u6651,negated_conjecture,
sP3(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u7558,negated_conjecture,
sP3(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u2588,negated_conjecture,
sP11(sK16(sK19(sK20(sK22)))) ).
cnf(u351,axiom,
( ~ p104(sK21(X0))
| p5(sK21(X0))
| ~ p5(X0)
| ~ p104(X0)
| ~ sP9(X0)
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u282,axiom,
( ~ p105(sK21(X0))
| p6(sK21(X0))
| ~ p6(X0)
| ~ p105(X0)
| ~ sP10(X0)
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u430,axiom,
( ~ p101(sK16(X0))
| p2(sK16(X0))
| ~ p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u1935,negated_conjecture,
sP9(sK19(sK20(sK22))) ).
cnf(u133,negated_conjecture,
sP0(sK22) ).
cnf(u2855,negated_conjecture,
sP5(sK17(sK19(sK20(sK22)))) ).
cnf(u7241,negated_conjecture,
sP3(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u5659,negated_conjecture,
sP7(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u6471,negated_conjecture,
sP4(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u6648,negated_conjecture,
sP0(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u8441,negated_conjecture,
p2(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u234,negated_conjecture,
sP7(sK21(sK22)) ).
cnf(u7145,negated_conjecture,
sP8(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u7688,negated_conjecture,
sP9(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7418,negated_conjecture,
sP0(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7732,negated_conjecture,
sP8(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7103,negated_conjecture,
sP1(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u5527,negated_conjecture,
sP10(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u6644,negated_conjecture,
sP7(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u294,negated_conjecture,
sP10(sK20(sK22)) ).
cnf(u6693,negated_conjecture,
sP10(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6825,negated_conjecture,
sP6(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u125,negated_conjecture,
( ~ r1(sK22,X0)
| sP11(X0) ) ).
cnf(u129,negated_conjecture,
sP6(sK22) ).
cnf(u8543,negated_conjecture,
p5(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u6560,negated_conjecture,
sP3(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6742,negated_conjecture,
sP2(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u7148,negated_conjecture,
sP0(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u6874,negated_conjecture,
sP10(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u1963,negated_conjecture,
sP7(sK18(sK20(sK22))) ).
cnf(u461,axiom,
( ~ p100(sK19(X0))
| p1(sK19(X0))
| ~ p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u392,axiom,
( ~ p4(sK20(X0))
| ~ p103(sK20(X0))
| p4(X0)
| ~ p103(X0)
| ~ sP8(X0)
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u6692,negated_conjecture,
sP9(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u5391,negated_conjecture,
sP5(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u5503,negated_conjecture,
p2(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u5604,negated_conjecture,
sP10(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u121,axiom,
r1(X0,X0) ).
cnf(u6282,negated_conjecture,
sP8(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u5393,negated_conjecture,
sP7(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u5867,negated_conjecture,
sP5(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u6922,negated_conjecture,
sP2(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u7645,negated_conjecture,
sP0(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u8592,negated_conjecture,
p3(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u110,axiom,
( p101(sK21(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u7556,negated_conjecture,
sP1(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u242,negated_conjecture,
sP4(sK21(sK22)) ).
cnf(u7733,negated_conjecture,
sP9(sK12(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u6467,negated_conjecture,
sP0(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u457,axiom,
( ~ p100(sK15(X0))
| p1(sK15(X0))
| ~ p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u7512,negated_conjecture,
sP2(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7603,negated_conjecture,
sP3(sK13(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u1968,negated_conjecture,
sP1(sK18(sK20(sK22))) ).
cnf(u5661,negated_conjecture,
sP9(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u7285,negated_conjecture,
sP2(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u5468,negated_conjecture,
sP10(sK14(sK16(sK19(sK21(sK22))))) ).
cnf(u7099,negated_conjecture,
sP8(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u2484,negated_conjecture,
sP5(sK17(sK19(sK21(sK22)))) ).
cnf(u5908,negated_conjecture,
p3(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u2412,negated_conjecture,
( ~ r1(sK17(sK19(sK21(sK22))),X0)
| sP11(X0) ) ).
cnf(u106,axiom,
( p102(sK18(X0))
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u7234,negated_conjecture,
sP7(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u469,axiom,
( ~ p1(sK13(X0))
| ~ p100(sK13(X0))
| p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u2997,negated_conjecture,
p3(sK16(sK19(sK20(sK22)))) ).
cnf(u400,axiom,
( ~ p102(sK14(X0))
| p3(sK14(X0))
| ~ p3(X0)
| ~ p102(X0)
| ~ sP7(X0)
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u91,axiom,
( ~ p105(sK14(X0))
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u239,negated_conjecture,
sP1(sK21(sK22)) ).
cnf(u6516,negated_conjecture,
sP4(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u6697,negated_conjecture,
sP3(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u3174,negated_conjecture,
sP7(sK17(sK18(sK21(sK22)))) ).
cnf(u2605,negated_conjecture,
sP11(sK17(sK18(sK20(sK22)))) ).
cnf(u205,negated_conjecture,
( ~ r1(sK21(sK22),X0)
| sP11(X0) ) ).
cnf(u7058,negated_conjecture,
sP2(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u118,negated_conjecture,
p100(sK22) ).
cnf(u8291,negated_conjecture,
p4(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6603,negated_conjecture,
sP1(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u7941,negated_conjecture,
p4(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u7008,negated_conjecture,
sP9(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u103,axiom,
( ~ p103(sK19(X0))
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u7505,negated_conjecture,
sP6(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7421,negated_conjecture,
sP3(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u84,axiom,
( ~ p6(sK12(X0))
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u4864,negated_conjecture,
sP11(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u6283,negated_conjecture,
sP9(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u5739,negated_conjecture,
sP7(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u8557,negated_conjecture,
p3(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u5646,negated_conjecture,
p4(sK14(sK17(sK18(sK21(sK22))))) ).
cnf(u1965,negated_conjecture,
sP9(sK18(sK20(sK22))) ).
cnf(u114,axiom,
( p101(sK20(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u5868,negated_conjecture,
sP6(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u7101,negated_conjecture,
sP10(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u99,axiom,
( ~ p104(sK16(X0))
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u7551,negated_conjecture,
sP7(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u299,negated_conjecture,
sP4(sK20(sK22)) ).
cnf(u7191,negated_conjecture,
sP9(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u5738,negated_conjecture,
sP6(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u80,axiom,
( p105(sK13(X0))
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u6381,negated_conjecture,
sP4(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u7643,negated_conjecture,
sP9(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u3023,negated_conjecture,
sP8(sK17(sK18(sK20(sK22)))) ).
cnf(u431,axiom,
( ~ p101(sK17(X0))
| p2(sK17(X0))
| ~ p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u362,axiom,
( ~ p5(sK18(X0))
| ~ p104(sK18(X0))
| p5(X0)
| ~ p104(X0)
| ~ sP9(X0)
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u7559,negated_conjecture,
sP4(sK12(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u6328,negated_conjecture,
sP7(sK13(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u7142,negated_conjecture,
sP5(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u1962,negated_conjecture,
sP6(sK18(sK20(sK22))) ).
cnf(u111,axiom,
( ~ p102(sK21(X0))
| p101(X0)
| ~ p100(X0)
| ~ sP0(X0) ) ).
cnf(u2571,negated_conjecture,
p3(sK16(sK19(sK21(sK22)))) ).
cnf(u6832,negated_conjecture,
sP2(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u5256,negated_conjecture,
sP7(sK15(sK17(sK19(sK21(sK22))))) ).
cnf(u92,axiom,
( ~ p5(sK14(X0))
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u7913,negated_conjecture,
p2(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u427,axiom,
( ~ p101(sK13(X0))
| p2(sK13(X0))
| ~ p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u5369,negated_conjecture,
p3(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u5869,negated_conjecture,
sP7(sK14(sK17(sK19(sK20(sK22))))) ).
cnf(u77,axiom,
( ~ r1(X0,X1)
| ~ p2(X1)
| ~ p101(X1)
| p2(X0)
| ~ p101(X0)
| ~ sP6(X0) ) ).
cnf(u7685,negated_conjecture,
sP6(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u5697,negated_conjecture,
p2(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u6422,negated_conjecture,
sP0(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u7151,negated_conjecture,
sP3(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u6551,negated_conjecture,
sP5(sK12(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u8503,negated_conjecture,
p4(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u472,axiom,
( ~ p1(sK16(X0))
| ~ p100(sK16(X0))
| p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p103(X0)
| ~ p102(X0)
| ~ sP2(X0) ) ).
cnf(u7237,negated_conjecture,
sP10(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u7051,negated_conjecture,
sP6(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u88,axiom,
( p5(sK15(X0))
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u7326,negated_conjecture,
sP9(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7370,negated_conjecture,
sP8(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u7684,negated_conjecture,
sP5(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u370,axiom,
( ~ p103(sK12(X0))
| p4(sK12(X0))
| ~ p4(X0)
| ~ p103(X0)
| ~ sP8(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u7055,negated_conjecture,
sP10(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u3176,negated_conjecture,
sP9(sK17(sK18(sK21(sK22)))) ).
cnf(u73,axiom,
( ~ r1(X0,X1)
| ~ p4(X1)
| ~ p103(X1)
| p4(X0)
| ~ p103(X0)
| ~ sP8(X0) ) ).
cnf(u739,negated_conjecture,
sP4(sK19(sK21(sK22))) ).
cnf(u7510,negated_conjecture,
sP0(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u6596,negated_conjecture,
sP5(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u5740,negated_conjecture,
sP8(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u6652,negated_conjecture,
sP4(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6833,negated_conjecture,
sP3(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u7233,negated_conjecture,
sP6(sK13(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u336,axiom,
( ~ p105(sK18(X0))
| ~ p6(sK18(X0))
| p6(X0)
| ~ p105(X0)
| ~ sP10(X0)
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u2767,negated_conjecture,
( ~ r1(sK17(sK18(sK21(sK22))),X0)
| ~ r1(X0,X1)
| sP11(X1) ) ).
cnf(u62,axiom,
( ~ sP11(X0)
| sP10(X0) ) ).
cnf(u3210,negated_conjecture,
sP6(sK16(sK18(sK21(sK22)))) ).
cnf(u7462,negated_conjecture,
sP9(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u6512,negated_conjecture,
sP0(sK13(sK15(sK16(sK19(sK21(sK22)))))) ).
cnf(u5392,negated_conjecture,
sP6(sK15(sK16(sK19(sK21(sK22))))) ).
cnf(u85,axiom,
( r1(X0,sK12(X0))
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u6374,negated_conjecture,
sP8(sK12(sK15(sK17(sK19(sK21(sK22)))))) ).
cnf(u8091,negated_conjecture,
p2(sK13(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u8375,negated_conjecture,
p5(sK12(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u7014,negated_conjecture,
sP4(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u401,axiom,
( ~ p102(sK15(X0))
| p3(sK15(X0))
| ~ p3(X0)
| ~ p102(X0)
| ~ sP7(X0)
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u348,axiom,
( ~ p104(sK18(X0))
| p5(sK18(X0))
| ~ p5(X0)
| ~ p104(X0)
| ~ sP9(X0)
| p102(X0)
| ~ p101(X0)
| ~ sP1(X0) ) ).
cnf(u4339,negated_conjecture,
sP11(sK15(sK16(sK19(sK20(sK22))))) ).
cnf(u5791,negated_conjecture,
sP6(sK15(sK17(sK19(sK20(sK22))))) ).
cnf(u8642,negated_conjecture,
p3(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u5741,negated_conjecture,
sP9(sK14(sK16(sK18(sK21(sK22))))) ).
cnf(u81,axiom,
( p6(sK13(X0))
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u747,negated_conjecture,
sP7(sK18(sK21(sK22))) ).
cnf(u6419,negated_conjecture,
sP8(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u454,axiom,
( ~ p100(sK12(X0))
| p1(sK12(X0))
| ~ p1(X0)
| ~ p100(X0)
| ~ sP5(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u5362,negated_conjecture,
p2(sK14(sK17(sK19(sK21(sK22))))) ).
cnf(u6698,negated_conjecture,
sP4(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u70,axiom,
( ~ r1(X0,X2)
| p5(X2)
| ~ p104(X2)
| ~ p5(X0)
| ~ p104(X0)
| ~ sP9(X0) ) ).
cnf(u7193,negated_conjecture,
sP0(sK12(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u6423,negated_conjecture,
sP1(sK13(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u413,axiom,
( ~ p3(sK13(X0))
| ~ p102(sK13(X0))
| p3(X0)
| ~ p102(X0)
| ~ sP7(X0)
| p105(X0)
| ~ p104(X0)
| ~ sP4(X0) ) ).
cnf(u7097,negated_conjecture,
sP6(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u6871,negated_conjecture,
sP7(sK13(sK15(sK16(sK18(sK21(sK22)))))) ).
cnf(u3021,negated_conjecture,
sP6(sK17(sK18(sK20(sK22)))) ).
cnf(u7413,negated_conjecture,
sP6(sK13(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u7507,negated_conjecture,
sP8(sK13(sK14(sK17(sK18(sK20(sK22)))))) ).
cnf(u7286,negated_conjecture,
sP3(sK12(sK15(sK16(sK19(sK20(sK22)))))) ).
cnf(u6649,negated_conjecture,
sP1(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6646,negated_conjecture,
sP9(sK12(sK14(sK16(sK19(sK21(sK22)))))) ).
cnf(u6468,negated_conjecture,
sP1(sK12(sK14(sK17(sK19(sK21(sK22)))))) ).
cnf(u450,axiom,
( ~ p2(sK19(X0))
| ~ p101(sK19(X0))
| p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p102(X0)
| ~ sP1(X0) ) ).
cnf(u5526,negated_conjecture,
sP9(sK15(sK17(sK18(sK21(sK22))))) ).
cnf(u7150,negated_conjecture,
sP2(sK13(sK14(sK17(sK19(sK20(sK22)))))) ).
cnf(u66,axiom,
( ~ sP11(X0)
| sP3(X0) ) ).
cnf(u7331,negated_conjecture,
sP3(sK13(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u409,axiom,
( ~ p102(sK16(X0))
| p3(sK16(X0))
| ~ p3(X0)
| ~ p102(X0)
| ~ sP7(X0)
| p103(X0)
| ~ sP2(X0) ) ).
cnf(u2530,negated_conjecture,
sP10(sK16(sK19(sK21(sK22)))) ).
cnf(u7100,negated_conjecture,
sP9(sK12(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u2527,negated_conjecture,
sP7(sK16(sK19(sK21(sK22)))) ).
cnf(u6826,negated_conjecture,
sP7(sK12(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u8177,negated_conjecture,
p2(sK13(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u6740,negated_conjecture,
sP0(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u2489,negated_conjecture,
sP10(sK17(sK19(sK21(sK22)))) ).
cnf(u5658,negated_conjecture,
sP6(sK15(sK16(sK18(sK21(sK22))))) ).
cnf(u7010,negated_conjecture,
sP0(sK12(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u442,axiom,
( ~ p2(sK14(X0))
| ~ p101(sK14(X0))
| p2(X0)
| ~ p101(X0)
| ~ sP6(X0)
| p104(X0)
| ~ p103(X0)
| ~ sP3(X0) ) ).
cnf(u7373,negated_conjecture,
sP0(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u58,axiom,
( ~ sP11(X0)
| sP6(X0) ) ).
cnf(u6960,negated_conjecture,
sP6(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u736,negated_conjecture,
sP1(sK19(sK21(sK22))) ).
cnf(u755,negated_conjecture,
sP4(sK18(sK21(sK22))) ).
cnf(u6046,negated_conjecture,
p3(sK14(sK16(sK19(sK20(sK22))))) ).
cnf(u7053,negated_conjecture,
sP8(sK13(sK15(sK17(sK19(sK20(sK22)))))) ).
cnf(u55,axiom,
( ~ sP11(X0)
| ~ p104(X0)
| p103(X0) ) ).
cnf(u7464,negated_conjecture,
sP0(sK12(sK15(sK17(sK18(sK20(sK22)))))) ).
cnf(u737,negated_conjecture,
sP2(sK19(sK21(sK22))) ).
cnf(u7687,negated_conjecture,
sP8(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u7692,negated_conjecture,
sP2(sK13(sK14(sK16(sK18(sK20(sK22)))))) ).
cnf(u3213,negated_conjecture,
sP9(sK16(sK18(sK21(sK22)))) ).
cnf(u7367,negated_conjecture,
sP5(sK12(sK14(sK16(sK19(sK20(sK22)))))) ).
cnf(u6785,negated_conjecture,
sP0(sK13(sK14(sK17(sK18(sK21(sK22)))))) ).
cnf(u6739,negated_conjecture,
sP10(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
cnf(u748,negated_conjecture,
sP8(sK18(sK21(sK22))) ).
cnf(u7639,negated_conjecture,
sP5(sK12(sK15(sK16(sK18(sK20(sK22)))))) ).
cnf(u6280,negated_conjecture,
sP6(sK14(sK16(sK18(sK20(sK22))))) ).
cnf(u6969,negated_conjecture,
sP4(sK13(sK14(sK16(sK18(sK21(sK22)))))) ).
cnf(u6743,negated_conjecture,
sP3(sK12(sK15(sK17(sK18(sK21(sK22)))))) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL657+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/5.37 % Computer : n011.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Sun Sep 27 16:20:52 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/5.41 Running first-order theorem proving
% 0.14/5.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.88/6.55 % (2596351)Detected formulas, will run a generic FOF schedule.
% 4.88/6.55 % (2596359)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=189921690:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.88/6.55 % (2596359)Refutation not found, incomplete strategy
% 4.88/6.55 % (2596359)------------------------------
% 4.88/6.55 % (2596359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.88/6.55 % (2596359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.88/6.55 % (2596359)CaDiCaL version: 2.1.3
% 4.88/6.55 % (2596359)Termination reason: Refutation not found, incomplete strategy
% 4.88/6.55 % (2596359)Time elapsed: 0.015 s
% 4.88/6.55 % (2596359)Peak memory usage: 89 MB
% 4.88/6.55 % (2596359)Instructions burned: 50 (million)
% 4.88/6.55 % (2596356)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=257571968:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.88/6.55 % (2596361)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2979990006:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.88/6.55 % (2596358)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=3466025546:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.88/6.55 % (2596357)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=1738764361:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.88/6.55 % (2596362)dis-21_1_sil=8000:lcm=predicate:random_seed=1216090715: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)
% 4.88/6.55 % (2596360)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3852715318:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.88/6.55 % (2596360)Instruction limit reached!
% 4.88/6.55 % (2596360)------------------------------
% 4.88/6.55 % (2596360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.88/6.55 % (2596360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.88/6.55 % (2596360)CaDiCaL version: 2.1.3
% 4.88/6.55 % (2596360)Termination reason: Instruction limit
% 4.88/6.55 % (2596360)Termination phase: Saturation
% 4.88/6.55 % (2596360)Time elapsed: 0.058 s
% 4.88/6.55 % (2596360)Peak memory usage: 89 MB
% 4.88/6.55 % (2596360)Instructions burned: 120 (million)
% 4.88/6.55 % (2596361)Instruction limit reached!
% 4.88/6.55 % (2596361)------------------------------
% 4.88/6.55 % (2596361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.88/6.55 % (2596361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.88/6.55 % (2596361)CaDiCaL version: 2.1.3
% 4.88/6.55 % (2596361)Termination reason: Instruction limit
% 4.88/6.55 % (2596361)Termination phase: Saturation
% 4.88/6.55 % (2596361)Time elapsed: 0.074 s
% 4.88/6.55 % (2596361)Peak memory usage: 89 MB
% 4.88/6.55 % (2596361)Instructions burned: 139 (million)
% 4.88/6.55 % (2596362)Instruction limit reached!
% 4.88/6.55 % (2596362)------------------------------
% 4.88/6.55 % (2596362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.88/6.55 % (2596362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.88/6.55 % (2596362)CaDiCaL version: 2.1.3
% 4.88/6.55 % (2596362)Termination reason: Instruction limit
% 4.88/6.55 % (2596362)Termination phase: Saturation
% 4.88/6.55 % (2596362)Time elapsed: 0.070 s
% 4.88/6.55 % (2596362)Peak memory usage: 90 MB
% 4.88/6.55 % (2596362)Instructions burned: 131 (million)
% 4.88/6.55 % (2596359)------------------------------
% 4.88/6.55 % (2596359)------------------------------
% 4.88/6.55 % (2596370)lrs+10_1_sil=8000:sp=occurrence:random_seed=3372254411:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 4.88/6.55 % (2596371)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3888183573:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.88/6.55 % (2596372)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2515115916:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 4.88/6.55 % (2596373)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=3861419245:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 4.88/6.55 % (2596373)Instruction limit reached!
% 4.88/6.55 % (2596373)------------------------------
% 4.88/6.55 % (2596373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.88/6.55 % (2596373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.88/6.55 % (2596373)CaDiCaL version: 2.1.3
% 4.88/6.55 % (2596373)Termination reason: Instruction limit
% 4.88/6.55 % (2596373)Termination phase: Saturation
% 4.88/6.55 % (2596373)Time elapsed: 0.064 s
% 4.88/6.55 % (2596373)Peak memory usage: 89 MB
% 4.88/6.55 % (2596373)Instructions burned: 249 (million)
% 4.88/6.55 % (2596371)Instruction limit reached!
% 4.88/6.55 % (2596371)------------------------------
% 4.88/6.55 % (2596371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.88/6.55 % (2596371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.88/6.55 % (2596371)CaDiCaL version: 2.1.3
% 4.88/6.55 % (2596371)Termination reason: Instruction limit
% 4.88/6.55 % (2596371)Termination phase: Saturation
% 4.88/6.55 % (2596371)Time elapsed: 0.078 s
% 4.88/6.55 % (2596371)Peak memory usage: 89 MB
% 4.88/6.55 % (2596371)Instructions burned: 157 (million)
% 4.88/6.55 % (2596370)First to succeed.
% 4.88/6.55 % (2596370)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2596351"
% 4.88/6.55 % (2596378)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3887008663:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 4.88/6.55 % (2596372)Instruction limit reached!
% 4.88/6.55 % (2596372)------------------------------
% 4.88/6.55 % (2596372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.88/6.55 % (2596372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.88/6.55 % (2596372)CaDiCaL version: 2.1.3
% 4.88/6.55 % (2596372)Termination reason: Instruction limit
% 4.88/6.55 % (2596372)Termination phase: Saturation
% 4.88/6.55 % (2596372)Time elapsed: 0.180 s
% 4.88/6.55 % (2596372)Peak memory usage: 92 MB
% 4.88/6.55 % (2596372)Instructions burned: 326 (million)
% 4.88/6.55 % (2596379)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=845371978:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 4.88/6.55 % (2596378)Refutation not found, incomplete strategy
% 4.88/6.55 % (2596378)------------------------------
% 4.88/6.55 % (2596378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.88/6.55 % (2596378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.88/6.55 % (2596378)CaDiCaL version: 2.1.3
% 4.88/6.55 % (2596378)Termination reason: Refutation not found, incomplete strategy
% 4.88/6.55 % (2596378)Time elapsed: 0.047 s
% 4.88/6.55 % (2596378)Peak memory usage: 91 MB
% 4.88/6.55 % (2596378)Instructions burned: 179 (million)
% 4.88/6.55 % (2596381)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=130965398:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 4.88/6.55 % SZS status CounterSatisfiable for theBenchmark
% 4.88/6.55 % SZS output start Saturation.
% See solution above
% 5.56/6.75 % SZS output start Definitions and Model Updates.
% 5.56/6.75 for all inputs,
% 5.56/6.75 define p106(X0) := $false
% 5.56/6.75 % SZS output end Definitions and Model Updates.
% 5.56/6.75 % (2596370)------------------------------
% 5.56/6.75 % (2596370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/6.75 % (2596370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/6.75 % (2596370)CaDiCaL version: 2.1.3
% 5.56/6.75 % (2596370)Termination reason: Satisfiable
% 5.56/6.75 % (2596370)Time elapsed: 0.113 s
% 5.56/6.75 % (2596370)Peak memory usage: 93 MB
% 5.56/6.75 % (2596370)Instructions burned: 212 (million)
% 5.56/6.75 % (2596370)------------------------------
% 5.56/6.75 % (2596370)------------------------------
% 5.56/6.75 % (2596351)Success in time 0.705 s
% 5.56/6.75 % Vampire exiting
%------------------------------------------------------------------------------