%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL661+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:26 AM UTC 2026
% Result : CounterSatisfiable 13.52s 2.88s
% Output : Saturation 14.91s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u742,negated_conjecture,
( ~ r1(sK180,X178)
| r1(X178,sK182(X178))
| ~ r1(X179,X180)
| p1(X179)
| ~ r1(X178,X179) ) ).
cnf(u749,negated_conjecture,
( ~ p1(X178)
| ~ r1(sK180,X178)
| ~ r1(X179,X180)
| p1(X179)
| ~ r1(X178,X179) ) ).
cnf(u753,negated_conjecture,
r1(sK180,sK181) ).
cnf(u757,negated_conjecture,
~ p1(sK180) ).
cnf(u761,negated_conjecture,
r1(sK125,sK180) ).
cnf(u768,negated_conjecture,
( ~ r1(sK125,X166)
| ~ r1(X166,X167)
| p1(X166)
| p2(X166) ) ).
cnf(u799,negated_conjecture,
( ~ r1(sK125,X158)
| ~ r1(X158,X159)
| p1(X158)
| p2(X158)
| p3(X158) ) ).
cnf(u838,negated_conjecture,
( ~ r1(sK125,X150)
| ~ r1(X150,X151)
| p1(X150)
| p2(X150)
| p3(X150)
| p4(X150) ) ).
cnf(u885,negated_conjecture,
( ~ r1(sK125,X138)
| ~ r1(X139,X140)
| p1(X139)
| p2(X139)
| p3(X139)
| p4(X139)
| ~ r1(X138,X139)
| p1(X138) ) ).
cnf(u889,negated_conjecture,
( ~ p1(sK169(X144))
| ~ r1(sK166,X144)
| ~ r1(X146,X147)
| p1(X146)
| p2(X146)
| p3(X146)
| p4(X146)
| ~ r1(X145,X146)
| p1(X145)
| ~ r1(X144,X145) ) ).
cnf(u893,negated_conjecture,
( ~ p2(sK169(X144))
| ~ r1(sK166,X144)
| ~ r1(X146,X147)
| p1(X146)
| p2(X146)
| p3(X146)
| p4(X146)
| ~ r1(X145,X146)
| p1(X145)
| ~ r1(X144,X145) ) ).
cnf(u897,negated_conjecture,
( ~ p3(sK169(X144))
| ~ r1(sK166,X144)
| ~ r1(X146,X147)
| p1(X146)
| p2(X146)
| p3(X146)
| p4(X146)
| ~ r1(X145,X146)
| p1(X145)
| ~ r1(X144,X145) ) ).
cnf(u901,negated_conjecture,
( ~ p4(sK169(X144))
| ~ r1(sK166,X144)
| ~ r1(X146,X147)
| p1(X146)
| p2(X146)
| p3(X146)
| p4(X146)
| ~ r1(X145,X146)
| p1(X145)
| ~ r1(X144,X145) ) ).
cnf(u909,negated_conjecture,
( ~ r1(sK166,X144)
| ~ p1(X144)
| ~ r1(X146,X147)
| p1(X146)
| p2(X146)
| p3(X146)
| p4(X146)
| ~ r1(X145,X146)
| p1(X145)
| ~ r1(X144,X145) ) ).
cnf(u913,negated_conjecture,
r1(sK167,sK168) ).
cnf(u917,negated_conjecture,
~ p1(sK167) ).
cnf(u921,negated_conjecture,
~ p2(sK167) ).
cnf(u925,negated_conjecture,
~ p3(sK167) ).
cnf(u929,negated_conjecture,
~ p4(sK167) ).
cnf(u933,negated_conjecture,
r1(sK166,sK167) ).
cnf(u937,negated_conjecture,
~ p1(sK166) ).
cnf(u948,negated_conjecture,
( ~ r1(sK125,X132)
| ~ r1(X133,X134)
| p1(X133)
| p2(X133)
| p3(X133)
| p4(X133)
| ~ r1(X132,X133)
| p1(X132)
| p2(X132) ) ).
cnf(u991,negated_conjecture,
( ~ r1(sK125,X126)
| ~ r1(X127,X128)
| p1(X127)
| p2(X127)
| p3(X127)
| p4(X127)
| ~ r1(X126,X127)
| p1(X126)
| p2(X126)
| p3(X126) ) ).
cnf(u1038,negated_conjecture,
( ~ r1(sK125,X120)
| ~ r1(X121,X122)
| p1(X121)
| p2(X121)
| p3(X121)
| p4(X121)
| ~ r1(X120,X121)
| p1(X120)
| p2(X120)
| p3(X120)
| p4(X120) ) ).
cnf(u1089,negated_conjecture,
( ~ r1(sK125,X112)
| ~ r1(X114,X115)
| p1(X114)
| p2(X114)
| p3(X114)
| p4(X114)
| ~ r1(X113,X114)
| p1(X113)
| p2(X113)
| p3(X113)
| p4(X113)
| ~ r1(X112,X113)
| p1(X112) ) ).
cnf(u1148,negated_conjecture,
( ~ r1(sK125,X104)
| ~ r1(X106,X107)
| p1(X106)
| p2(X106)
| p3(X106)
| p4(X106)
| ~ r1(X105,X106)
| p1(X105)
| p2(X105)
| p3(X105)
| p4(X105)
| ~ r1(X104,X105)
| p1(X104)
| p2(X104) ) ).
cnf(u1211,negated_conjecture,
( ~ r1(sK125,X96)
| ~ r1(X98,X99)
| p1(X98)
| p2(X98)
| p3(X98)
| p4(X98)
| ~ r1(X97,X98)
| p1(X97)
| p2(X97)
| p3(X97)
| p4(X97)
| ~ r1(X96,X97)
| p1(X96)
| p2(X96)
| p3(X96) ) ).
cnf(u1278,negated_conjecture,
( ~ r1(sK125,X91)
| ~ r1(X93,X94)
| p1(X93)
| p2(X93)
| p3(X93)
| p4(X93)
| ~ r1(X92,X93)
| p1(X92)
| p2(X92)
| p3(X92)
| p4(X92)
| ~ r1(X91,X92)
| p1(X91)
| p2(X91)
| p3(X91)
| p4(X91) ) ).
cnf(u1309,negated_conjecture,
( ~ r1(sK125,X79)
| ~ r1(X82,X83)
| p1(X82)
| p2(X82)
| p3(X82)
| p4(X82)
| ~ r1(X81,X82)
| p1(X81)
| p2(X81)
| p3(X81)
| p4(X81)
| ~ r1(X80,X81)
| p1(X80)
| p2(X80)
| p3(X80)
| p4(X80)
| ~ r1(X79,X80)
| p1(X79) ) ).
cnf(u1332,negated_conjecture,
( ~ r1(sK125,X67)
| ~ r1(X70,X71)
| p1(X70)
| p2(X70)
| p3(X70)
| p4(X70)
| ~ r1(X69,X70)
| p1(X69)
| p2(X69)
| p3(X69)
| p4(X69)
| ~ r1(X68,X69)
| p1(X68)
| p2(X68)
| p3(X68)
| p4(X68)
| ~ r1(X67,X68)
| p1(X67)
| p2(X67) ) ).
cnf(u1363,negated_conjecture,
( ~ r1(sK125,X55)
| ~ r1(X58,X59)
| p1(X58)
| p2(X58)
| p3(X58)
| p4(X58)
| ~ r1(X57,X58)
| p1(X57)
| p2(X57)
| p3(X57)
| p4(X57)
| ~ r1(X56,X57)
| p1(X56)
| p2(X56)
| p3(X56)
| p4(X56)
| ~ r1(X55,X56)
| p1(X55)
| p2(X55)
| p3(X55) ) ).
cnf(u1402,negated_conjecture,
( ~ r1(sK125,X43)
| ~ r1(X46,X47)
| p1(X46)
| p2(X46)
| p3(X46)
| p4(X46)
| ~ r1(X45,X46)
| p1(X45)
| p2(X45)
| p3(X45)
| p4(X45)
| ~ r1(X44,X45)
| p1(X44)
| p2(X44)
| p3(X44)
| p4(X44)
| ~ r1(X43,X44)
| p1(X43)
| p2(X43)
| p3(X43)
| p4(X43) ) ).
cnf(u1449,negated_conjecture,
( ~ r1(sK125,X27)
| ~ r1(X31,X32)
| p1(X31)
| p2(X31)
| p3(X31)
| p4(X31)
| ~ r1(X30,X31)
| p1(X30)
| p2(X30)
| p3(X30)
| p4(X30)
| ~ r1(X29,X30)
| p1(X29)
| p2(X29)
| p3(X29)
| p4(X29)
| ~ r1(X28,X29)
| p1(X28)
| p2(X28)
| p3(X28)
| p4(X28)
| ~ r1(X27,X28)
| p1(X27) ) ).
cnf(u1512,negated_conjecture,
( ~ r1(sK125,X19)
| ~ r1(X23,X24)
| p1(X23)
| p2(X23)
| p3(X23)
| p4(X23)
| ~ r1(X22,X23)
| p1(X22)
| p2(X22)
| p3(X22)
| p4(X22)
| ~ r1(X21,X22)
| p1(X21)
| p2(X21)
| p3(X21)
| p4(X21)
| ~ r1(X20,X21)
| p1(X20)
| p2(X20)
| p3(X20)
| p4(X20)
| ~ r1(X19,X20)
| p1(X19)
| p2(X19) ) ).
cnf(u1555,negated_conjecture,
( ~ r1(sK125,X11)
| ~ r1(X15,X16)
| p1(X15)
| p2(X15)
| p3(X15)
| p4(X15)
| ~ r1(X14,X15)
| p1(X14)
| p2(X14)
| p3(X14)
| p4(X14)
| ~ r1(X13,X14)
| p1(X13)
| p2(X13)
| p3(X13)
| p4(X13)
| ~ r1(X12,X13)
| p1(X12)
| p2(X12)
| p3(X12)
| p4(X12)
| ~ r1(X11,X12)
| p1(X11)
| p2(X11)
| p3(X11) ) ).
cnf(u1599,negated_conjecture,
sP25(sK132) ).
cnf(u1606,negated_conjecture,
sP26(sK132) ).
cnf(u1610,negated_conjecture,
r1(sK125,sK132) ).
cnf(u1617,negated_conjecture,
p1(sK127) ).
cnf(u1624,negated_conjecture,
p1(sK129) ).
cnf(u1633,negated_conjecture,
p1(sK126) ).
cnf(u1641,negated_conjecture,
p1(sK130) ).
cnf(u1655,negated_conjecture,
p2(sK130) ).
cnf(u1659,negated_conjecture,
p2(sK128) ).
cnf(u1662,negated_conjecture,
p1(sK128) ).
cnf(u1669,negated_conjecture,
p2(sK131) ).
cnf(u1682,negated_conjecture,
r1(sK131,sK183(sK131)) ).
cnf(u1685,negated_conjecture,
( ~ r1(sK131,X0)
| p2(X0) ) ).
cnf(u1689,negated_conjecture,
r1(sK130,sK183(sK130)) ).
cnf(u1692,negated_conjecture,
( ~ r1(sK130,X0)
| p2(X0) ) ).
cnf(u1696,negated_conjecture,
r1(sK129,sK183(sK129)) ).
cnf(u1706,negated_conjecture,
( ~ r1(sK127,X0)
| p2(X0) ) ).
cnf(u1710,negated_conjecture,
r1(sK126,sK183(sK126)) ).
cnf(u1713,negated_conjecture,
( ~ r1(sK126,X0)
| p2(X0) ) ).
cnf(u1723,negated_conjecture,
( ~ r1(sK180,X0)
| p2(X0) ) ).
cnf(u1727,negated_conjecture,
p2(sK180) ).
cnf(u1743,negated_conjecture,
( ~ r1(sK181,X0)
| ~ r1(X0,X1)
| p1(X0) ) ).
cnf(u1764,negated_conjecture,
r1(sK180,sK182(sK180)) ).
cnf(u1768,negated_conjecture,
p2(sK125) ).
cnf(u1778,negated_conjecture,
r1(sK125,sK183(sK125)) ).
cnf(u1796,negated_conjecture,
r1(sK183(sK180),sK182(sK183(sK180))) ).
cnf(u1803,negated_conjecture,
p1(sK181) ).
cnf(u1844,negated_conjecture,
p2(sK127) ).
cnf(u1851,negated_conjecture,
p2(sK126) ).
cnf(u1894,negated_conjecture,
~ p2(sK132) ).
cnf(u1864,negated_conjecture,
p1(sK132) ).
cnf(u1871,negated_conjecture,
r1(sK132,sK183(sK132)) ).
cnf(u1898,negated_conjecture,
( ~ p2(X0)
| ~ r1(sK132,X0)
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u1906,negated_conjecture,
( ~ r1(sK34(sK132),X0)
| ~ r1(X0,X1)
| ~ p2(X0)
| p2(X1) ) ).
cnf(u1936,negated_conjecture,
~ r1(sK180,sK126) ).
cnf(u1958,negated_conjecture,
~ r1(sK180,sK129) ).
cnf(u1966,negated_conjecture,
~ r1(sK180,sK127) ).
cnf(u3292,negated_conjecture,
~ r1(sK125,sK30(sK125)) ).
cnf(u1991,negated_conjecture,
( ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(sK28(X1))
| p2(X1) ) ).
cnf(u1995,negated_conjecture,
r1(sK180,sK30(sK180)) ).
cnf(u1998,negated_conjecture,
( ~ r1(sK180,X0)
| ~ r1(X0,X1)
| p2(sK28(X1))
| p2(X1) ) ).
cnf(u2002,negated_conjecture,
r1(sK131,sK30(sK131)) ).
cnf(u2005,negated_conjecture,
( ~ r1(sK131,X0)
| ~ r1(X0,X1)
| p2(sK28(X1))
| p2(X1) ) ).
cnf(u2009,negated_conjecture,
r1(sK130,sK30(sK130)) ).
cnf(u2012,negated_conjecture,
( ~ r1(sK130,X0)
| ~ r1(X0,X1)
| p2(sK28(X1))
| p2(X1) ) ).
cnf(u2016,negated_conjecture,
r1(sK129,sK30(sK129)) ).
cnf(u2019,negated_conjecture,
( ~ r1(sK129,X0)
| ~ r1(X0,X1)
| p2(sK28(X1))
| p2(X1) ) ).
cnf(u2023,negated_conjecture,
r1(sK128,sK30(sK128)) ).
cnf(u2026,negated_conjecture,
( ~ r1(sK128,X0)
| ~ r1(X0,X1)
| p2(sK28(X1))
| p2(X1) ) ).
cnf(u2030,negated_conjecture,
r1(sK127,sK30(sK127)) ).
cnf(u2033,negated_conjecture,
( ~ r1(sK127,X0)
| ~ r1(X0,X1)
| p2(sK28(X1))
| p2(X1) ) ).
cnf(u2040,negated_conjecture,
( ~ r1(sK126,X0)
| ~ r1(X0,X1)
| p2(sK28(X1))
| p2(X1) ) ).
cnf(u2065,negated_conjecture,
~ r1(sK180,sK132) ).
cnf(u2079,negated_conjecture,
~ r1(sK180,sK128) ).
cnf(u2108,negated_conjecture,
~ p2(sK183(sK132)) ).
cnf(u2111,negated_conjecture,
r1(sK183(sK132),sK37(sK183(sK132))) ).
cnf(u2145,negated_conjecture,
p1(sK183(sK125)) ).
cnf(u2152,negated_conjecture,
r1(sK183(sK125),sK183(sK183(sK125))) ).
cnf(u2260,negated_conjecture,
~ r1(sK180,sK183(sK130)) ).
cnf(u2268,negated_conjecture,
~ r1(sK180,sK183(sK125)) ).
cnf(u2275,negated_conjecture,
( ~ r1(sK183(sK132),X1)
| ~ p2(X1)
| p2(X2)
| ~ r1(X1,X2) ) ).
cnf(u2278,negated_conjecture,
( ~ r1(sK183(sK132),X0)
| r1(X0,sK39(X0))
| p2(X0) ) ).
cnf(u2328,negated_conjecture,
r1(sK30(sK180),sK182(sK30(sK180))) ).
cnf(u2343,negated_conjecture,
r1(sK183(sK125),sK31(sK183(sK125))) ).
cnf(u2357,negated_conjecture,
( ~ r1(sK183(X0),sK30(sK128))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u2361,negated_conjecture,
~ r1(sK132,sK30(sK128)) ).
cnf(u2368,negated_conjecture,
( ~ r1(sK128,X0)
| r1(X1,sK28(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u2372,negated_conjecture,
( ~ p2(sK29(X1))
| ~ r1(sK128,X0)
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u2377,negated_conjecture,
( ~ r1(sK128,X0)
| r1(sK28(X1),sK29(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u2394,negated_conjecture,
~ r1(sK180,sK30(sK130)) ).
cnf(u2399,negated_conjecture,
~ p2(sK34(sK132)) ).
cnf(u2419,negated_conjecture,
( ~ r1(sK183(X0),sK30(sK180))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u2423,negated_conjecture,
~ r1(sK132,sK30(sK180)) ).
cnf(u2430,negated_conjecture,
( ~ r1(sK180,X0)
| r1(X1,sK28(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u2434,negated_conjecture,
( ~ p2(sK29(X1))
| ~ r1(sK180,X0)
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u2439,negated_conjecture,
( ~ r1(sK180,X0)
| r1(sK28(X1),sK29(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u2444,negated_conjecture,
( ~ r1(sK183(X0),sK180)
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u2448,negated_conjecture,
~ r1(sK132,sK180) ).
cnf(u2472,negated_conjecture,
( ~ r1(sK183(X0),sK30(sK131))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u2476,negated_conjecture,
~ r1(sK132,sK30(sK131)) ).
cnf(u2483,negated_conjecture,
( ~ r1(sK131,X0)
| r1(X1,sK28(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u2487,negated_conjecture,
( ~ p2(sK29(X1))
| ~ r1(sK131,X0)
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u2492,negated_conjecture,
( ~ r1(sK131,X0)
| r1(sK28(X1),sK29(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u2507,negated_conjecture,
( ~ r1(sK30(sK127),X2)
| p2(X2) ) ).
cnf(u2521,negated_conjecture,
( ~ r1(sK127,X0)
| r1(X1,sK28(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u2525,negated_conjecture,
( ~ p2(sK29(X1))
| ~ r1(sK127,X0)
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u2530,negated_conjecture,
( ~ r1(sK127,X0)
| r1(sK28(X1),sK29(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u2548,negated_conjecture,
( ~ r1(sK183(X0),sK30(sK130))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u2552,negated_conjecture,
~ r1(sK132,sK30(sK130)) ).
cnf(u2556,negated_conjecture,
( ~ sP27(X2)
| ~ r1(X2,sK130) ) ).
cnf(u2559,negated_conjecture,
( ~ r1(sK130,X0)
| r1(X1,sK28(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u2568,negated_conjecture,
( ~ r1(sK130,X0)
| r1(sK28(X1),sK29(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u2579,negated_conjecture,
sP24(sK35(sK132)) ).
cnf(u2603,negated_conjecture,
~ r1(sK180,sK31(sK130)) ).
cnf(u2617,negated_conjecture,
r1(sK183(sK125),sK30(sK183(sK125))) ).
cnf(u2624,negated_conjecture,
( ~ r1(sK126,X0)
| ~ r1(X0,X1)
| r1(X1,sK28(X1))
| p2(X1) ) ).
cnf(u2644,negated_conjecture,
p1(sK30(sK125)) ).
cnf(u2651,negated_conjecture,
r1(sK30(sK125),sK183(sK30(sK125))) ).
cnf(u2662,negated_conjecture,
r1(sK30(sK125),sK31(sK30(sK125))) ).
cnf(u2673,negated_conjecture,
( ~ r1(sK125,X0)
| ~ r1(X0,X1)
| r1(X1,sK28(X1))
| p2(X1) ) ).
cnf(u2697,negated_conjecture,
p2(sK30(sK180)) ).
cnf(u2704,negated_conjecture,
p2(sK181) ).
cnf(u2707,negated_conjecture,
r1(sK181,sK28(sK181)) ).
cnf(u2731,negated_conjecture,
( ~ r1(sK183(X0),sK30(sK125))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u2735,negated_conjecture,
~ r1(sK132,sK30(sK125)) ).
cnf(u2747,negated_conjecture,
( ~ r1(sK125,X0)
| r1(sK28(X1),sK29(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u2786,negated_conjecture,
~ r1(sK180,sK30(sK125)) ).
cnf(u2888,negated_conjecture,
~ p2(sK183(sK30(sK125))) ).
cnf(u2847,negated_conjecture,
( ~ r1(sK126,X0)
| ~ r1(X0,X1)
| r1(sK28(X1),sK29(X1))
| p2(X1) ) ).
cnf(u2861,negated_conjecture,
r1(sK182(sK180),sK182(sK182(sK180))) ).
cnf(u3255,negated_conjecture,
p2(sK31(sK30(sK125))) ).
cnf(u2886,negated_conjecture,
( ~ r1(sK31(sK30(sK125)),X2)
| p2(X2) ) ).
cnf(u4008,negated_conjecture,
p2(sK182(sK30(sK180))) ).
cnf(u2898,negated_conjecture,
( ~ r1(sK182(sK30(sK180)),X2)
| p2(X2) ) ).
cnf(u2910,negated_conjecture,
p3(sK183(sK180)) ).
cnf(u2924,negated_conjecture,
p4(sK30(sK180)) ).
cnf(u2945,negated_conjecture,
( ~ r1(sK183(X0),sK181)
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u2949,negated_conjecture,
~ r1(sK132,sK181) ).
cnf(u2963,negated_conjecture,
( ~ r1(sK183(X0),sK125)
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u2967,negated_conjecture,
~ r1(sK132,sK125) ).
cnf(u2975,negated_conjecture,
p4(sK182(sK180)) ).
cnf(u2981,negated_conjecture,
p2(sK182(sK180)) ).
cnf(u3043,negated_conjecture,
( ~ r1(sK35(sK132),X2)
| p2(X2) ) ).
cnf(u3085,negated_conjecture,
( ~ r1(sK183(X0),sK183(sK126))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u3089,negated_conjecture,
~ r1(sK132,sK183(sK126)) ).
cnf(u3104,negated_conjecture,
( ~ r1(sK183(X0),sK183(sK131))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u3108,negated_conjecture,
~ r1(sK132,sK183(sK131)) ).
cnf(u3147,negated_conjecture,
r1(sK32(sK30(sK125)),sK28(sK32(sK30(sK125)))) ).
cnf(u3180,negated_conjecture,
( ~ r1(sK35(sK132),X0)
| ~ r1(X0,X1)
| r1(X1,sK41(X1))
| p2(X1) ) ).
cnf(u3203,negated_conjecture,
p2(sK41(sK132)) ).
cnf(u3247,negated_conjecture,
( ~ r1(sK183(X0),sK41(sK132))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u3358,negated_conjecture,
r1(sK31(sK130),sK28(sK31(sK130))) ).
cnf(u3362,negated_conjecture,
p2(sK30(sK130)) ).
cnf(u3369,negated_conjecture,
p2(sK183(sK130)) ).
cnf(u3418,negated_conjecture,
p2(sK31(sK129)) ).
cnf(u3421,negated_conjecture,
r1(sK31(sK129),sK28(sK31(sK129))) ).
cnf(u3425,negated_conjecture,
p2(sK30(sK129)) ).
cnf(u3428,negated_conjecture,
r1(sK30(sK129),sK28(sK30(sK129))) ).
cnf(u3435,negated_conjecture,
r1(sK183(sK129),sK28(sK183(sK129))) ).
cnf(u3440,negated_conjecture,
p2(sK28(sK129)) ).
cnf(u3468,negated_conjecture,
( ~ r1(sK183(sK130),X2)
| p2(X2) ) ).
cnf(u3505,negated_conjecture,
r1(sK28(sK30(sK180)),sK28(sK28(sK30(sK180)))) ).
cnf(u3514,negated_conjecture,
( ~ r1(sK182(sK180),X2)
| p2(X2) ) ).
cnf(u3541,negated_conjecture,
( ~ r1(sK28(sK30(sK129)),X2)
| p2(X2) ) ).
cnf(u3544,negated_conjecture,
( ~ r1(sK129,X0)
| ~ r1(X0,X1)
| r1(X1,sK28(X1))
| p2(X1) ) ).
cnf(u3548,negated_conjecture,
( ~ r1(sK129,X0)
| ~ r1(X0,X1)
| r1(sK28(X1),sK29(X1))
| p2(X1) ) ).
cnf(u3564,negated_conjecture,
( ~ r1(sK30(sK129),X2)
| p2(X2) ) ).
cnf(u3575,negated_conjecture,
( ~ sP27(X2)
| ~ r1(X2,sK129) ) ).
cnf(u3683,negated_conjecture,
p2(sK28(sK31(sK129))) ).
cnf(u3686,negated_conjecture,
r1(sK28(sK31(sK129)),sK28(sK28(sK31(sK129)))) ).
cnf(u3695,negated_conjecture,
r1(sK32(sK129),sK28(sK32(sK129))) ).
cnf(u3715,negated_conjecture,
r1(sK29(sK129),sK28(sK29(sK129))) ).
cnf(u3773,negated_conjecture,
p2(sK28(sK28(sK31(sK129)))) ).
cnf(u3779,negated_conjecture,
p2(sK28(sK32(sK129))) ).
cnf(u3806,negated_conjecture,
( ~ r1(sK183(X0),sK28(sK32(sK129)))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u3810,negated_conjecture,
~ r1(sK132,sK28(sK32(sK129))) ).
cnf(u3819,negated_conjecture,
( ~ r1(sK183(X0),sK31(sK129))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u3823,negated_conjecture,
~ r1(sK132,sK31(sK129)) ).
cnf(u3836,negated_conjecture,
( ~ r1(sK28(sK28(sK31(sK129))),X2)
| p2(X2) ) ).
cnf(u3853,negated_conjecture,
~ r1(sK30(sK128),sK28(sK31(sK129))) ).
cnf(u3860,negated_conjecture,
~ r1(sK181,sK28(sK31(sK129))) ).
cnf(u3864,negated_conjecture,
~ r1(sK129,sK28(sK31(sK129))) ).
cnf(u3868,negated_conjecture,
~ r1(sK125,sK28(sK31(sK129))) ).
cnf(u3879,negated_conjecture,
( ~ r1(sK28(sK31(sK129)),X2)
| p2(X2) ) ).
cnf(u3908,negated_conjecture,
r1(sK28(sK28(sK30(sK180))),sK29(sK28(sK30(sK180)))) ).
cnf(u3921,negated_conjecture,
r1(sK183(sK125),sK28(sK183(sK125))) ).
cnf(u3967,negated_conjecture,
~ r1(sK31(sK129),sK28(sK30(sK180))) ).
cnf(u3974,negated_conjecture,
~ r1(sK28(sK129),sK28(sK30(sK180))) ).
cnf(u3978,negated_conjecture,
~ r1(sK181,sK28(sK30(sK180))) ).
cnf(u3982,negated_conjecture,
~ r1(sK125,sK28(sK30(sK180))) ).
cnf(u3986,negated_conjecture,
~ r1(sK129,sK28(sK30(sK180))) ).
cnf(u3990,negated_conjecture,
~ r1(sK30(sK128),sK28(sK30(sK180))) ).
cnf(u4056,negated_conjecture,
r1(sK28(sK28(sK129)),sK28(sK28(sK28(sK129)))) ).
cnf(u4085,negated_conjecture,
p2(sK28(sK29(sK129))) ).
cnf(u4104,negated_conjecture,
( ~ r1(sK183(X0),sK28(sK129))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u4108,negated_conjecture,
~ r1(sK132,sK28(sK129)) ).
cnf(u4117,negated_conjecture,
( ~ r1(sK183(X0),sK28(sK29(sK129)))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u4121,negated_conjecture,
~ r1(sK132,sK28(sK29(sK129))) ).
cnf(u4144,negated_conjecture,
( ~ r1(sK28(sK183(sK30(sK125))),X2)
| p2(X2) ) ).
cnf(u4180,negated_conjecture,
~ r1(sK31(sK129),sK183(sK30(sK125))) ).
cnf(u4187,negated_conjecture,
~ r1(sK28(sK129),sK183(sK30(sK125))) ).
cnf(u4191,negated_conjecture,
~ r1(sK181,sK183(sK30(sK125))) ).
cnf(u4195,negated_conjecture,
~ r1(sK125,sK183(sK30(sK125))) ).
cnf(u4199,negated_conjecture,
~ r1(sK129,sK183(sK30(sK125))) ).
cnf(u4203,negated_conjecture,
~ r1(sK30(sK128),sK183(sK30(sK125))) ).
cnf(u4213,negated_conjecture,
r1(sK28(sK183(sK129)),sK29(sK183(sK129))) ).
cnf(u4233,negated_conjecture,
p2(sK28(sK181)) ).
cnf(u4237,negated_conjecture,
p1(sK28(sK181)) ).
cnf(u4252,negated_conjecture,
~ r1(sK180,sK28(sK181)) ).
cnf(u4258,negated_conjecture,
( ~ r1(sK28(sK181),X2)
| p2(X2) ) ).
cnf(u4280,negated_conjecture,
r1(sK28(sK183(sK125)),sK29(sK183(sK125))) ).
cnf(u4284,negated_conjecture,
r1(sK28(sK183(sK183(sK125))),sK29(sK183(sK183(sK125)))) ).
cnf(u4291,negated_conjecture,
r1(sK28(sK30(sK183(sK125))),sK29(sK30(sK183(sK125)))) ).
cnf(u4325,negated_conjecture,
r1(sK28(sK31(sK183(sK125))),sK29(sK31(sK183(sK125)))) ).
cnf(u4328,negated_conjecture,
p2(sK31(sK183(sK125))) ).
cnf(u4335,negated_conjecture,
( ~ r1(sK31(sK183(sK125)),X1)
| p2(X1) ) ).
cnf(u4353,negated_conjecture,
( ~ r1(sK183(X0),sK32(sK183(sK125)))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u4357,negated_conjecture,
~ r1(sK132,sK32(sK183(sK125))) ).
cnf(u4389,negated_conjecture,
( ~ r1(sK183(sK132),X0)
| p2(sK39(X0))
| p2(X0) ) ).
cnf(u4393,negated_conjecture,
( r1(sK39(X0),sK40(X0))
| ~ r1(sK183(sK132),X0)
| p2(X0) ) ).
cnf(u4398,negated_conjecture,
r1(sK37(sK183(sK132)),sK38(sK183(sK132))) ).
cnf(u4416,negated_conjecture,
p2(sK28(sK132)) ).
cnf(u4429,negated_conjecture,
( ~ r1(sK28(sK132),X0)
| p2(sK39(X0))
| p2(X0) ) ).
cnf(u4433,negated_conjecture,
( ~ r1(sK28(sK132),X0)
| r1(sK39(X0),sK40(X0))
| p2(X0) ) ).
cnf(u4437,negated_conjecture,
( ~ r1(sK28(sK132),X0)
| r1(X0,sK39(X0))
| p2(X0) ) ).
cnf(u4442,negated_conjecture,
r1(sK28(sK132),sK37(sK28(sK132))) ).
cnf(u4447,negated_conjecture,
r1(sK37(sK28(sK132)),sK38(sK28(sK132))) ).
cnf(u4457,negated_conjecture,
( ~ r1(sK28(sK132),X0)
| p2(X0) ) ).
cnf(u4460,negated_conjecture,
~ r1(sK129,sK132) ).
cnf(u4481,negated_conjecture,
p2(sK29(sK132)) ).
cnf(u4491,negated_conjecture,
~ r1(sK30(sK128),sK132) ).
cnf(u4511,negated_conjecture,
( ~ r1(sK29(sK132),X2)
| p2(X2) ) ).
cnf(u5795,negated_conjecture,
~ p2(sK37(sK183(sK132))) ).
cnf(u4589,negated_conjecture,
~ r1(sK132,sK37(sK183(sK132))) ).
cnf(u4603,negated_conjecture,
p2(sK28(sK183(sK132))) ).
cnf(u4622,negated_conjecture,
( ~ r1(sK28(sK183(sK132)),X1)
| p2(X1) ) ).
cnf(u4625,negated_conjecture,
~ r1(sK129,sK183(sK132)) ).
cnf(u4629,negated_conjecture,
~ r1(sK125,sK183(sK132)) ).
cnf(u4659,negated_conjecture,
( ~ r1(sK29(sK183(sK132)),X2)
| p2(X2) ) ).
cnf(u4696,negated_conjecture,
( ~ r1(sK183(X0),sK35(sK183(sK132)))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u4700,negated_conjecture,
~ r1(sK132,sK35(sK183(sK132))) ).
cnf(u4728,negated_conjecture,
( ~ r1(sK28(sK132),X0)
| ~ r1(X0,X1)
| r1(X1,sK41(X1))
| p2(X1) ) ).
cnf(u4735,negated_conjecture,
r1(sK29(sK132),sK43(sK29(sK132))) ).
cnf(u4738,negated_conjecture,
( ~ r1(sK29(sK132),X0)
| ~ r1(X0,X1)
| r1(X1,sK41(X1))
| p2(X1) ) ).
cnf(u4793,negated_conjecture,
( ~ r1(sK28(sK132),X0)
| ~ r1(X0,X1)
| r1(sK41(X1),sK42(X1))
| p2(X1) ) ).
cnf(u4806,negated_conjecture,
( ~ r1(sK183(X0),sK43(sK29(sK132)))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u4810,negated_conjecture,
~ r1(sK132,sK43(sK29(sK132))) ).
cnf(u4814,negated_conjecture,
( ~ sP24(X2)
| ~ r1(X2,sK29(sK132)) ) ).
cnf(u4903,negated_conjecture,
( ~ r1(sK183(X0),sK38(sK28(sK132)))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u4907,negated_conjecture,
~ r1(sK132,sK38(sK28(sK132))) ).
cnf(u4925,negated_conjecture,
( ~ r1(sK183(X0),sK37(sK28(sK132)))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u4929,negated_conjecture,
~ r1(sK132,sK37(sK28(sK132))) ).
cnf(u4937,negated_conjecture,
r1(sK38(sK28(sK132)),sK41(sK38(sK28(sK132)))) ).
cnf(u4952,negated_conjecture,
~ p2(sK41(sK38(sK28(sK132)))) ).
cnf(u4991,negated_conjecture,
r1(sK183(sK183(sK125)),sK28(sK183(sK183(sK125)))) ).
cnf(u4995,negated_conjecture,
r1(sK30(sK183(sK125)),sK28(sK30(sK183(sK125)))) ).
cnf(u5005,negated_conjecture,
r1(sK30(sK125),sK28(sK30(sK125))) ).
cnf(u5011,negated_conjecture,
p2(sK28(sK183(sK129))) ).
cnf(u5030,negated_conjecture,
r1(sK36(sK132),sK43(sK36(sK132))) ).
cnf(u5074,negated_conjecture,
( ~ r1(sK35(sK132),X0)
| ~ r1(X0,X1)
| p2(sK41(X1))
| p2(X1) ) ).
cnf(u5080,negated_conjecture,
( ~ r1(sK35(sK132),X0)
| ~ r1(X0,X1)
| r1(sK41(X1),sK42(X1))
| p2(X1) ) ).
cnf(u5093,negated_conjecture,
( ~ r1(sK183(X0),sK38(sK183(sK132)))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u5097,negated_conjecture,
~ r1(sK132,sK38(sK183(sK132))) ).
cnf(u5117,negated_conjecture,
r1(sK37(sK183(sK132)),sK39(sK37(sK183(sK132)))) ).
cnf(u5121,negated_conjecture,
p2(sK39(sK37(sK183(sK132)))) ).
cnf(u5130,negated_conjecture,
( ~ r1(sK183(X0),sK39(sK37(sK183(sK132))))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u5134,negated_conjecture,
~ r1(sK132,sK39(sK37(sK183(sK132)))) ).
cnf(u5172,negated_conjecture,
r1(sK41(sK38(sK28(sK132))),sK42(sK38(sK28(sK132)))) ).
cnf(u5180,negated_conjecture,
( ~ r1(sK28(sK183(sK129)),X2)
| p2(X2) ) ).
cnf(u5187,negated_conjecture,
~ r1(sK132,sK28(sK183(sK129))) ).
cnf(u5201,negated_conjecture,
p2(sK29(sK183(sK129))) ).
cnf(u5214,negated_conjecture,
~ r1(sK30(sK128),sK183(sK129)) ).
cnf(u5272,negated_conjecture,
( ~ r1(sK29(sK183(sK129)),X2)
| p2(X2) ) ).
cnf(u5287,negated_conjecture,
( ~ r1(X0,sK183(sK129))
| ~ r1(sK130,X0) ) ).
cnf(u5291,negated_conjecture,
( ~ r1(sK127,X0)
| ~ r1(X0,sK183(sK129)) ) ).
cnf(u5295,negated_conjecture,
( ~ r1(X0,sK183(sK129))
| ~ r1(sK131,X0) ) ).
cnf(u5299,negated_conjecture,
( ~ r1(X0,sK183(sK129))
| ~ r1(sK180,X0) ) ).
cnf(u5303,negated_conjecture,
( ~ r1(sK128,X0)
| ~ r1(X0,sK183(sK129)) ) ).
cnf(u5307,negated_conjecture,
( ~ sP27(X2)
| ~ r1(X0,X1)
| r1(X0,sK30(X0))
| ~ r1(X2,X0)
| ~ r1(X1,sK183(sK129)) ) ).
cnf(u5311,negated_conjecture,
( ~ sP27(X2)
| ~ r1(X0,X1)
| ~ p2(X3)
| p2(X4)
| ~ r1(X3,X4)
| ~ r1(sK30(X0),X3)
| ~ r1(X2,X0)
| ~ r1(X1,sK183(sK129)) ) ).
cnf(u5357,negated_conjecture,
( ~ r1(sK39(sK183(sK132)),X2)
| p2(X2) ) ).
cnf(u5364,negated_conjecture,
~ r1(sK132,sK39(sK183(sK132))) ).
cnf(u5384,negated_conjecture,
( ~ r1(sK183(X0),sK182(sK182(sK180)))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u5388,negated_conjecture,
~ r1(sK132,sK182(sK182(sK180))) ).
cnf(u5406,negated_conjecture,
p2(sK28(sK183(sK125))) ).
cnf(u5410,negated_conjecture,
p2(sK28(sK183(sK183(sK125)))) ).
cnf(u5414,negated_conjecture,
p2(sK28(sK30(sK183(sK125)))) ).
cnf(u5423,negated_conjecture,
( ~ r1(sK183(X0),sK28(sK30(sK183(sK125))))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u5427,negated_conjecture,
~ r1(sK132,sK28(sK30(sK183(sK125)))) ).
cnf(u5438,negated_conjecture,
~ r1(sK28(sK129),sK30(sK183(sK125))) ).
cnf(u5445,negated_conjecture,
~ r1(sK181,sK30(sK183(sK125))) ).
cnf(u5449,negated_conjecture,
~ r1(sK125,sK30(sK183(sK125))) ).
cnf(u5453,negated_conjecture,
~ r1(sK129,sK30(sK183(sK125))) ).
cnf(u5457,negated_conjecture,
~ r1(sK30(sK128),sK30(sK183(sK125))) ).
cnf(u5463,negated_conjecture,
( ~ r1(sK28(sK183(sK183(sK125))),X2)
| p2(X2) ) ).
cnf(u5481,negated_conjecture,
~ r1(sK28(sK129),sK183(sK183(sK125))) ).
cnf(u5484,negated_conjecture,
p2(sK29(sK183(sK183(sK125)))) ).
cnf(u5488,negated_conjecture,
~ r1(sK181,sK183(sK183(sK125))) ).
cnf(u5492,negated_conjecture,
~ r1(sK125,sK183(sK183(sK125))) ).
cnf(u5496,negated_conjecture,
~ r1(sK129,sK183(sK183(sK125))) ).
cnf(u5500,negated_conjecture,
~ r1(sK30(sK128),sK183(sK183(sK125))) ).
cnf(u5506,negated_conjecture,
( ~ r1(sK28(sK183(sK125)),X2)
| p2(X2) ) ).
cnf(u5513,negated_conjecture,
~ r1(sK132,sK28(sK183(sK125))) ).
cnf(u5527,negated_conjecture,
p2(sK29(sK183(sK125))) ).
cnf(u5540,negated_conjecture,
~ r1(sK30(sK128),sK183(sK125)) ).
cnf(u5556,negated_conjecture,
r1(sK41(sK132),sK43(sK41(sK132))) ).
cnf(u5568,negated_conjecture,
( ~ r1(sK43(sK41(sK132)),X0)
| ~ r1(X0,X1)
| r1(X1,sK41(X1))
| p2(X1) ) ).
cnf(u5581,negated_conjecture,
( ~ r1(sK183(X0),sK43(sK41(sK132)))
| ~ r1(sK125,X0)
| ~ r1(X0,X1)
| p2(X1) ) ).
cnf(u5585,negated_conjecture,
~ r1(sK132,sK43(sK41(sK132))) ).
cnf(u5610,negated_conjecture,
~ r1(sK132,sK41(sK132)) ).
cnf(u5619,negated_conjecture,
r1(sK43(sK41(sK132)),sK44(sK43(sK41(sK132)))) ).
cnf(u5635,negated_conjecture,
p2(sK44(sK43(sK41(sK132)))) ).
cnf(u5641,negated_conjecture,
( ~ r1(sK44(sK43(sK41(sK132))),X2)
| p2(X2) ) ).
cnf(u5675,negated_conjecture,
r1(sK183(sK132),sK28(sK183(sK132))) ).
cnf(u5679,negated_conjecture,
r1(sK28(sK183(sK132)),sK29(sK183(sK132))) ).
cnf(u5683,negated_conjecture,
r1(sK183(sK132),sK39(sK183(sK132))) ).
cnf(u5687,negated_conjecture,
p2(sK39(sK183(sK132))) ).
cnf(u5694,negated_conjecture,
p2(sK29(sK183(sK132))) ).
cnf(u5702,negated_conjecture,
~ r1(sK30(sK128),sK183(sK132)) ).
cnf(u5770,negated_conjecture,
( ~ r1(sK40(sK183(sK132)),X2)
| p2(X2) ) ).
cnf(u5801,negated_conjecture,
r1(sK43(sK41(sK132)),sK41(sK43(sK41(sK132)))) ).
cnf(u5848,negated_conjecture,
( ~ r1(sK29(sK183(sK183(sK125))),X2)
| p2(X2) ) ).
cnf(u5863,negated_conjecture,
( ~ r1(sK127,X0)
| ~ r1(X0,sK183(sK183(sK125))) ) ).
cnf(u5867,negated_conjecture,
( ~ r1(X0,sK183(sK183(sK125)))
| ~ r1(sK131,X0) ) ).
cnf(u5871,negated_conjecture,
( ~ r1(X0,sK183(sK183(sK125)))
| ~ r1(sK180,X0) ) ).
cnf(u5875,negated_conjecture,
( ~ r1(sK128,X0)
| ~ r1(X0,sK183(sK183(sK125))) ) ).
cnf(u5879,negated_conjecture,
( ~ sP27(X2)
| ~ r1(X0,X1)
| r1(X0,sK30(X0))
| ~ r1(X2,X0)
| ~ r1(X1,sK183(sK183(sK125))) ) ).
cnf(u5883,negated_conjecture,
( ~ sP27(X2)
| ~ r1(X0,X1)
| ~ p2(X3)
| p2(X4)
| ~ r1(X3,X4)
| ~ r1(sK30(X0),X3)
| ~ r1(X2,X0)
| ~ r1(X1,sK183(sK183(sK125))) ) ).
cnf(u5904,negated_conjecture,
r1(sK41(sK43(sK41(sK132))),sK41(sK41(sK43(sK41(sK132))))) ).
cnf(u5948,negated_conjecture,
( ~ r1(sK29(sK183(sK125)),X2)
| p2(X2) ) ).
cnf(u5959,negated_conjecture,
( ~ r1(sK127,X0)
| ~ r1(X0,sK183(sK125)) ) ).
cnf(u5963,negated_conjecture,
( ~ r1(X0,sK183(sK125))
| ~ r1(sK131,X0) ) ).
cnf(u5967,negated_conjecture,
( ~ r1(X0,sK183(sK125))
| ~ r1(sK180,X0) ) ).
cnf(u5971,negated_conjecture,
( ~ r1(sK128,X0)
| ~ r1(X0,sK183(sK125)) ) ).
cnf(u5975,negated_conjecture,
( ~ sP27(X2)
| ~ r1(X0,X1)
| r1(X0,sK30(X0))
| ~ r1(X2,X0)
| ~ r1(X1,sK183(sK125)) ) ).
cnf(u5979,negated_conjecture,
( ~ sP27(X2)
| ~ r1(X0,X1)
| ~ p2(X3)
| p2(X4)
| ~ r1(X3,X4)
| ~ r1(sK30(X0),X3)
| ~ r1(X2,X0)
| ~ r1(X1,sK183(sK125)) ) ).
cnf(u6010,negated_conjecture,
p2(sK41(sK41(sK43(sK41(sK132))))) ).
cnf(u6019,negated_conjecture,
( ~ r1(sK41(sK41(sK43(sK41(sK132)))),X2)
| p2(X2) ) ).
cnf(u248,axiom,
( r1(sK56(X0),sK57(X0))
| ~ sP19(X0) ) ).
cnf(u2831,negated_conjecture,
( ~ r1(sK30(sK128),X0)
| p2(sK28(X0))
| p2(X0) ) ).
cnf(u524,negated_conjecture,
( ~ r1(sK125,X182)
| ~ r1(X182,X183)
| p2(X183)
| r1(X182,sK183(X182)) ) ).
cnf(u151,axiom,
( ~ p2(sK34(X0))
| ~ r1(X0,X8)
| ~ r1(X8,X9)
| p2(X9)
| ~ p2(X8)
| ~ sP26(X0) ) ).
cnf(u2330,negated_conjecture,
p2(sK30(sK131)) ).
cnf(u289,axiom,
( ~ p3(sK70(X0))
| ~ sP16(X0) ) ).
cnf(u3327,negated_conjecture,
( ~ r1(sK183(sK125),X0)
| p2(X0)
| r1(sK28(X0),sK29(X0)) ) ).
cnf(u276,axiom,
( ~ p1(sK65(X0))
| ~ sP17(X0) ) ).
cnf(u406,axiom,
( ~ p3(sK97(X0))
| ~ sP9(X0) ) ).
cnf(u300,axiom,
( ~ p4(sK68(X0))
| ~ sP16(X0) ) ).
cnf(u4375,negated_conjecture,
( ~ r1(sK132,X0)
| p2(X0)
| r1(sK28(X0),sK29(X0)) ) ).
cnf(u502,axiom,
( ~ sP2(X0)
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u149,axiom,
( ~ sP26(X0)
| ~ r1(X3,X4)
| p2(X4)
| ~ p2(X3)
| ~ r1(X0,X8)
| ~ r1(X8,X9)
| p2(X9)
| ~ p2(X8)
| ~ r1(sK34(X0),X3) ) ).
cnf(u295,axiom,
( ~ p4(sK69(X0))
| ~ sP16(X0) ) ).
cnf(u5018,negated_conjecture,
( ~ r1(sK35(sK132),X0)
| ~ r1(X1,X2)
| p2(X2)
| r1(sK41(X2),sK42(X2))
| ~ r1(sK43(X0),X3)
| ~ r1(X3,X4)
| p2(X4)
| ~ p2(X3)
| ~ r1(X0,X1) ) ).
cnf(u417,axiom,
( ~ p3(sK102(X0))
| ~ sP8(X0) ) ).
cnf(u404,axiom,
( ~ p1(sK97(X0))
| ~ sP9(X0) ) ).
cnf(u160,axiom,
( ~ p2(sK40(X6))
| sP24(X1)
| ~ r1(X1,X6)
| p2(X6)
| ~ r1(X0,X1)
| ~ p2(X1)
| ~ sP25(X0) ) ).
cnf(u2873,negated_conjecture,
( ~ p2(sK38(X0))
| ~ r1(sK38(X0),X1)
| p2(X1)
| sP24(X0)
| ~ p2(X0)
| ~ r1(sK132,X0) ) ).
cnf(u479,axiom,
( ~ p4(sK113(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u1825,negated_conjecture,
p1(sK183(sK130)) ).
cnf(u293,axiom,
( ~ p2(sK69(X0))
| ~ sP16(X0) ) ).
cnf(u423,axiom,
( ~ p4(sK101(X0))
| ~ sP8(X0) ) ).
cnf(u316,axiom,
( ~ p4(sK72(X0))
| ~ sP15(X0) ) ).
cnf(u166,axiom,
( ~ sP25(X0)
| sP24(X1)
| ~ r1(sK38(X1),X4)
| ~ r1(X4,X5)
| p2(X5)
| ~ p2(X4)
| ~ p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u307,axiom,
( r1(sK73(X0),sK74(X0))
| ~ sP15(X0) ) ).
cnf(u189,axiom,
( ~ sP23(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| sP21(sK46(X1))
| ~ r1(X0,X1) ) ).
cnf(u216,axiom,
( ~ p2(sK53(X0))
| ~ sP21(X0) ) ).
cnf(u421,axiom,
( ~ p2(sK101(X0))
| ~ sP8(X0) ) ).
cnf(u306,axiom,
( ~ p4(sK74(X0))
| ~ sP15(X0) ) ).
cnf(u444,axiom,
( ~ p3(sK108(X1))
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u164,axiom,
( ~ sP25(X0)
| sP24(X1)
| ~ r1(X1,X6)
| p2(X6)
| r1(X6,sK39(X6))
| ~ p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u4673,negated_conjecture,
( ~ r1(sK128,X0)
| ~ r1(X0,sK183(sK132)) ) ).
cnf(u179,axiom,
( ~ sP24(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| p2(sK41(X3))
| r1(X1,sK43(X1))
| ~ r1(X0,X1) ) ).
cnf(u2989,negated_conjecture,
( ~ r1(sK132,X0)
| ~ r1(X0,X1)
| p2(X1)
| r1(sK39(X1),sK40(X1))
| ~ r1(X0,X2)
| ~ r1(X2,X3)
| p2(X3)
| ~ p2(X2)
| sP24(X0) ) ).
cnf(u434,axiom,
( ~ p4(sK105(X0))
| ~ sP7(X0) ) ).
cnf(u2628,negated_conjecture,
( ~ r1(sK183(sK131),X0)
| p2(X0)
| r1(X0,sK28(X0)) ) ).
cnf(u2987,negated_conjecture,
( ~ r1(sK30(sK131),X0)
| p2(X0)
| r1(sK28(X0),sK29(X0)) ) ).
cnf(u177,axiom,
( ~ sP24(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| p2(sK41(X3))
| ~ r1(sK43(X1),X7)
| ~ r1(X7,X8)
| p2(X8)
| ~ p2(X7)
| ~ r1(X0,X1) ) ).
cnf(u334,axiom,
( r1(sK82(X0),sK83(X0))
| ~ sP13(X0) ) ).
cnf(u333,axiom,
( ~ sP14(X0)
| r1(X0,sK76(X0)) ) ).
cnf(u432,axiom,
( ~ p2(sK105(X0))
| ~ sP7(X0) ) ).
cnf(u206,axiom,
( ~ p3(sK48(X0))
| ~ sP22(X0) ) ).
cnf(u323,axiom,
( r1(sK77(X0),sK78(X0))
| ~ sP14(X0) ) ).
cnf(u461,axiom,
( ~ sP5(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| r1(sK110(X1),sK111(X1))
| ~ r1(X0,X1) ) ).
cnf(u346,axiom,
( ~ p2(sK80(X0))
| ~ sP13(X0) ) ).
cnf(u204,axiom,
( ~ p1(sK48(X0))
| ~ sP22(X0) ) ).
cnf(u2682,negated_conjecture,
( ~ r1(sK183(sK125),X0)
| r1(X0,sK28(X0))
| p2(X0) ) ).
cnf(u3008,negated_conjecture,
( ~ r1(sK180,X2)
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0)
| ~ r1(X2,X0)
| p2(X2)
| p3(X2)
| p4(X2)
| ~ r1(X0,X1) ) ).
cnf(u451,axiom,
( ~ sP6(X0)
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| r1(X1,sK107(X1))
| ~ r1(X0,X1) ) ).
cnf(u344,axiom,
( r1(sK80(X0),sK81(X0))
| ~ sP13(X0) ) ).
cnf(u194,axiom,
( ~ sP23(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| r1(X1,sK46(X1))
| ~ r1(X0,X1) ) ).
cnf(u5332,negated_conjecture,
~ r1(sK127,sK183(sK129)) ).
cnf(u5892,negated_conjecture,
~ r1(sK180,sK183(sK183(sK125))) ).
cnf(u4552,negated_conjecture,
( ~ r1(sK132,sK28(X0))
| p2(X0)
| ~ r1(sK132,X0)
| p2(X1)
| ~ r1(sK28(X0),X1) ) ).
cnf(u217,axiom,
( ~ p3(sK53(X0))
| ~ sP21(X0) ) ).
cnf(u363,axiom,
( ~ p3(sK84(X0))
| ~ sP12(X0) ) ).
cnf(u350,axiom,
( r1(sK86(X0),sK87(X0))
| ~ sP12(X0) ) ).
cnf(u733,negated_conjecture,
r1(sK125,sK129) ).
cnf(u472,axiom,
( ~ p2(sK114(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u731,negated_conjecture,
r1(sK125,sK130) ).
cnf(u223,axiom,
( ~ p4(sK52(X0))
| ~ sP21(X0) ) ).
cnf(u361,axiom,
( ~ p1(sK84(X0))
| ~ sP12(X0) ) ).
cnf(u402,axiom,
( ~ p4(sK98(X0))
| ~ sP9(X0) ) ).
cnf(u517,axiom,
( ~ p3(sK123(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ r1(X0,X1)
| ~ sP0(X0) ) ).
cnf(u256,axiom,
( ~ p2(sK62(X0))
| ~ sP18(X0) ) ).
cnf(u478,axiom,
( ~ p3(sK113(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u234,axiom,
( ~ p4(sK55(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| ~ r1(X0,X1)
| ~ sP20(X0) ) ).
cnf(u515,axiom,
( ~ p1(sK123(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ r1(X0,X1)
| ~ sP0(X0) ) ).
cnf(u5745,negated_conjecture,
( ~ sP27(X2)
| ~ r1(X1,sK183(sK132))
| ~ r1(X2,X0)
| r1(X0,sK30(X0))
| ~ r1(X0,X1) ) ).
cnf(u262,axiom,
( ~ p3(sK61(X0))
| ~ sP18(X0) ) ).
cnf(u232,axiom,
( ~ p2(sK55(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| ~ r1(X0,X1)
| ~ sP20(X0) ) ).
cnf(u135,axiom,
( ~ sP27(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| r1(sK28(X3),sK29(X3))
| ~ r1(sK30(X1),X7)
| ~ r1(X7,X8)
| p2(X8)
| ~ p2(X7)
| ~ r1(X0,X1) ) ).
cnf(u273,axiom,
( ~ p3(sK66(X0))
| ~ sP17(X0) ) ).
cnf(u495,axiom,
( ~ sP2(X0)
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| r1(sK119(X1),sK120(X1))
| ~ r1(X0,X1) ) ).
cnf(u218,axiom,
( ~ p4(sK53(X0))
| ~ sP21(X0) ) ).
cnf(u390,axiom,
( ~ p3(sK93(X0))
| ~ sP10(X0) ) ).
cnf(u519,axiom,
( ~ sP0(X0)
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| r1(X1,sK123(X1))
| ~ r1(X0,X1) ) ).
cnf(u4372,negated_conjecture,
( p2(sK28(X0))
| ~ r1(sK132,X0)
| p2(X0) ) ).
cnf(u133,axiom,
( ~ p2(sK30(X1))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| ~ p2(sK29(X3))
| ~ r1(X0,X1)
| ~ sP27(X0) ) ).
cnf(u279,axiom,
( ~ p4(sK65(X0))
| ~ sP17(X0) ) ).
cnf(u401,axiom,
( ~ p3(sK98(X0))
| ~ sP9(X0) ) ).
cnf(u388,axiom,
( ~ p1(sK93(X0))
| ~ sP10(X0) ) ).
cnf(u144,axiom,
( ~ p2(sK36(X5))
| p2(X5)
| ~ r1(X0,X5)
| ~ p2(X0)
| ~ sP26(X0) ) ).
cnf(u326,axiom,
( ~ p3(sK77(X0))
| ~ sP14(X0) ) ).
cnf(u522,negated_conjecture,
( ~ p2(X185)
| ~ r1(X182,X183)
| p2(X183)
| ~ r1(sK183(X182),X185)
| ~ r1(X185,X186)
| p2(X186)
| ~ r1(sK125,X182) ) ).
cnf(u2331,negated_conjecture,
p2(sK30(sK127)) ).
cnf(u277,axiom,
( ~ p2(sK65(X0))
| ~ sP17(X0) ) ).
cnf(u407,axiom,
( ~ p4(sK97(X0))
| ~ sP9(X0) ) ).
cnf(u513,axiom,
( ~ sP1(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ p3(X1)
| ~ r1(X0,X1) ) ).
cnf(u150,axiom,
( ~ sP26(X0)
| ~ r1(X3,X4)
| p2(X4)
| ~ p2(X3)
| ~ p2(X0)
| ~ r1(sK34(X0),X3) ) ).
cnf(u173,axiom,
( ~ sP24(X0)
| p2(X1)
| p2(sK44(X1))
| ~ r1(X0,X1) ) ).
cnf(u4671,negated_conjecture,
( ~ r1(X0,sK183(sK132))
| ~ r1(sK131,X0) ) ).
cnf(u405,axiom,
( ~ p2(sK97(X0))
| ~ sP9(X0) ) ).
cnf(u290,axiom,
( ~ p4(sK70(X0))
| ~ sP16(X0) ) ).
cnf(u428,axiom,
( ~ p4(sK100(X0))
| ~ sP8(X0) ) ).
cnf(u148,axiom,
( ~ sP26(X0)
| p2(X5)
| r1(X5,sK35(X5))
| ~ p2(X0)
| ~ r1(X0,X5) ) ).
cnf(u246,axiom,
( ~ p3(sK57(X0))
| ~ sP19(X0) ) ).
cnf(u275,axiom,
( r1(sK65(X0),sK66(X0))
| ~ sP17(X0) ) ).
cnf(u4527,negated_conjecture,
( ~ sP27(X2)
| ~ r1(X1,sK132)
| ~ r1(X2,X0)
| ~ r1(sK30(X0),X3)
| ~ r1(X3,X4)
| p2(X4)
| ~ p2(X3)
| ~ r1(X0,X1) ) ).
cnf(u163,axiom,
( ~ sP25(X0)
| sP24(X1)
| ~ r1(X1,X6)
| p2(X6)
| r1(X6,sK39(X6))
| ~ r1(X1,X9)
| ~ r1(X9,X10)
| p2(X10)
| ~ p2(X9)
| ~ r1(X0,X1) ) ).
cnf(u317,axiom,
( ~ sP15(X0)
| r1(X0,sK72(X0)) ) ).
cnf(u447,axiom,
( ~ p1(sK107(X1))
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u418,axiom,
( ~ p4(sK102(X0))
| ~ sP8(X0) ) ).
cnf(u3387,negated_conjecture,
( ~ r1(sK30(sK130),X0)
| p2(X0)
| r1(X0,sK28(X0)) ) ).
cnf(u190,axiom,
( ~ p1(sK46(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| ~ r1(X0,X1)
| ~ sP23(X0) ) ).
cnf(u2629,negated_conjecture,
( ~ r1(sK30(sK131),X0)
| p2(X0)
| r1(X0,sK28(X0)) ) ).
cnf(u4525,negated_conjecture,
( ~ r1(sK128,X0)
| ~ r1(X0,sK132) ) ).
cnf(u161,axiom,
( ~ sP25(X0)
| sP24(X1)
| ~ r1(X1,X6)
| p2(X6)
| r1(sK39(X6),sK40(X6))
| ~ r1(X1,X9)
| ~ r1(X9,X10)
| p2(X10)
| ~ p2(X9)
| ~ r1(X0,X1) ) ).
cnf(u331,axiom,
( ~ p3(sK76(X0))
| ~ sP14(X0) ) ).
cnf(u445,axiom,
( ~ p4(sK108(X1))
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u416,axiom,
( ~ p2(sK102(X0))
| ~ sP8(X0) ) ).
cnf(u2986,negated_conjecture,
( ~ r1(sK183(sK131),X0)
| p2(X0)
| r1(sK28(X0),sK29(X0)) ) ).
cnf(u188,axiom,
( ~ sP24(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| r1(X3,sK41(X3))
| r1(X1,sK43(X1))
| ~ r1(X0,X1) ) ).
cnf(u454,axiom,
( ~ sP6(X0)
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ p3(X1)
| ~ r1(X0,X1) ) ).
cnf(u435,axiom,
( r1(sK104(X0),sK105(X0))
| ~ sP7(X0) ) ).
cnf(u330,axiom,
( ~ p2(sK76(X0))
| ~ sP14(X0) ) ).
cnf(u178,axiom,
( ~ p2(sK43(X1))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| p2(sK41(X3))
| ~ r1(X0,X1)
| ~ sP24(X0) ) ).
cnf(u3662,negated_conjecture,
( ~ r1(sK28(sK129),X0)
| r1(X0,sK28(X0))
| p2(X0) ) ).
cnf(u469,axiom,
( ~ sP5(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ p3(X1)
| ~ r1(X0,X1) ) ).
cnf(u328,axiom,
( r1(sK76(X0),sK77(X0))
| ~ sP14(X0) ) ).
cnf(u458,axiom,
( ~ p2(sK111(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u201,axiom,
( ~ p3(sK49(X0))
| ~ sP22(X0) ) ).
cnf(u347,axiom,
( ~ p3(sK80(X0))
| ~ sP13(X0) ) ).
cnf(u4686,negated_conjecture,
~ r1(sK180,sK183(sK132)) ).
cnf(u456,axiom,
( ~ sP5(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| r1(sK111(X1),sK112(X1))
| ~ r1(X0,X1) ) ).
cnf(u207,axiom,
( ~ p4(sK48(X0))
| ~ sP22(X0) ) ).
cnf(u345,axiom,
( ~ p1(sK80(X0))
| ~ sP13(X0) ) ).
cnf(u475,axiom,
( ~ sP4(X0)
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| r1(sK113(X1),sK114(X1))
| ~ r1(X0,X1) ) ).
cnf(u368,axiom,
( ~ p2(sK90(X0))
| ~ sP11(X0) ) ).
cnf(u4319,negated_conjecture,
( ~ r1(sK132,sK28(X0))
| p2(X0)
| ~ r1(sK125,X0)
| p2(X1)
| ~ r1(sK28(X0),X1) ) ).
cnf(u4171,negated_conjecture,
p2(sK28(sK183(sK30(sK125)))) ).
cnf(u734,negated_conjecture,
( ~ r1(sK128,X5)
| p2(X5) ) ).
cnf(u386,axiom,
( ~ p4(sK94(X0))
| ~ sP10(X0) ) ).
cnf(u473,axiom,
( ~ p3(sK114(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u4971,negated_conjecture,
( ~ r1(sK37(sK28(sK132)),X0)
| r1(sK41(X0),sK42(X0))
| p2(X0) ) ).
cnf(u374,axiom,
( ~ p3(sK89(X0))
| ~ sP11(X0) ) ).
cnf(u5890,negated_conjecture,
~ r1(sK30(sK127),sK183(sK183(sK125))) ).
cnf(u518,axiom,
( ~ p4(sK123(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ r1(X0,X1)
| ~ sP0(X0) ) ).
cnf(u3036,negated_conjecture,
( ~ r1(sK132,X0)
| ~ r1(X0,X1)
| p2(X1)
| p2(sK39(X1))
| ~ r1(X0,X2)
| ~ r1(X2,X3)
| p2(X3)
| ~ p2(X2)
| sP24(X0) ) ).
cnf(u247,axiom,
( ~ p4(sK57(X0))
| ~ sP19(X0) ) ).
cnf(u257,axiom,
( ~ p3(sK62(X0))
| ~ sP18(X0) ) ).
cnf(u5020,negated_conjecture,
( ~ r1(sK35(sK132),X0)
| ~ r1(X1,X2)
| p2(X2)
| r1(X2,sK41(X2))
| ~ r1(sK43(X0),X3)
| ~ r1(X3,X4)
| p2(X4)
| ~ p2(X3)
| ~ r1(X0,X1) ) ).
cnf(u443,axiom,
( ~ p2(sK108(X1))
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u372,axiom,
( ~ p1(sK89(X0))
| ~ sP11(X0) ) ).
cnf(u3328,negated_conjecture,
( r1(sK28(X0),sK29(X0))
| p2(X0)
| ~ r1(sK125,X0) ) ).
cnf(u5746,negated_conjecture,
( ~ sP27(X2)
| ~ r1(X1,sK183(sK132))
| ~ r1(X2,X0)
| ~ r1(sK30(X0),X3)
| ~ r1(X3,X4)
| p2(X4)
| ~ p2(X3)
| ~ r1(X0,X1) ) ).
cnf(u202,axiom,
( ~ p4(sK49(X0))
| ~ sP22(X0) ) ).
cnf(u245,axiom,
( ~ p2(sK57(X0))
| ~ sP19(X0) ) ).
cnf(u263,axiom,
( ~ p4(sK61(X0))
| ~ sP18(X0) ) ).
cnf(u385,axiom,
( ~ p3(sK94(X0))
| ~ sP10(X0) ) ).
cnf(u500,axiom,
( ~ sP2(X0)
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| r1(X1,sK119(X1))
| ~ r1(X0,X1) ) ).
cnf(u2683,negated_conjecture,
( ~ r1(sK125,X0)
| r1(X0,sK28(X0))
| p2(X0) ) ).
cnf(u128,axiom,
( ~ sP27(X0)
| p2(X1)
| r1(X1,sK31(X1))
| ~ r1(X0,X1) ) ).
cnf(u261,axiom,
( ~ p2(sK61(X0))
| ~ sP18(X0) ) ).
cnf(u512,axiom,
( ~ sP1(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u391,axiom,
( ~ p4(sK93(X0))
| ~ sP10(X0) ) ).
cnf(u284,axiom,
( ~ p4(sK64(X0))
| ~ sP17(X0) ) ).
cnf(u5016,negated_conjecture,
( ~ r1(sK35(sK132),X0)
| ~ r1(X1,X2)
| p2(X2)
| p2(sK41(X2))
| ~ r1(sK43(X0),X3)
| ~ r1(X3,X4)
| p2(X4)
| ~ p2(X3)
| ~ r1(X0,X1) ) ).
cnf(u134,axiom,
( ~ p2(sK29(X3))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| ~ r1(X0,X1)
| r1(X1,sK30(X1))
| ~ sP27(X0) ) ).
cnf(u3323,negated_conjecture,
( r1(sK28(X0),sK29(X0))
| p2(X0)
| ~ r1(sK129,X0) ) ).
cnf(u157,axiom,
( ~ sP25(X0)
| sP24(X1)
| ~ r1(X1,X6)
| p2(X6)
| p2(sK39(X6))
| ~ r1(X1,X9)
| ~ r1(X9,X10)
| p2(X10)
| ~ p2(X9)
| ~ r1(X0,X1) ) ).
cnf(u303,axiom,
( ~ p1(sK74(X0))
| ~ sP15(X0) ) ).
cnf(u389,axiom,
( ~ p2(sK93(X0))
| ~ sP10(X0) ) ).
cnf(u274,axiom,
( ~ p4(sK66(X0))
| ~ sP17(X0) ) ).
cnf(u412,axiom,
( ~ p4(sK96(X0))
| ~ sP9(X0) ) ).
cnf(u1827,negated_conjecture,
p2(sK183(sK131)) ).
cnf(u383,axiom,
( ~ p1(sK94(X0))
| ~ sP10(X0) ) ).
cnf(u132,axiom,
( ~ p2(sK29(X3))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| ~ r1(X0,X1)
| ~ r1(sK30(X1),X7)
| ~ r1(X7,X8)
| p2(X8)
| ~ p2(X7)
| ~ sP27(X0) ) ).
cnf(u2072,negated_conjecture,
( ~ r1(sK132,X0)
| r1(X0,sK37(X0))
| ~ p2(X0)
| sP24(X0) ) ).
cnf(u4524,negated_conjecture,
( ~ r1(X0,sK132)
| ~ r1(sK180,X0) ) ).
cnf(u147,axiom,
( ~ sP26(X0)
| p2(X5)
| r1(X5,sK35(X5))
| ~ r1(X0,X8)
| ~ r1(X8,X9)
| p2(X9)
| ~ p2(X8)
| ~ r1(X0,X5) ) ).
cnf(u320,axiom,
( ~ p2(sK78(X0))
| ~ sP14(X0) ) ).
cnf(u301,axiom,
( ~ sP16(X0)
| r1(X0,sK68(X0)) ) ).
cnf(u431,axiom,
( ~ p1(sK105(X0))
| ~ sP7(X0) ) ).
cnf(u2957,negated_conjecture,
( ~ r1(sK30(sK131),X0)
| p2(sK28(X0))
| p2(X0) ) ).
cnf(u4754,negated_conjecture,
p2(sK43(sK29(sK132))) ).
cnf(u174,axiom,
( ~ p2(sK45(X1))
| p2(X1)
| ~ r1(X0,X1)
| ~ sP24(X0) ) ).
cnf(u343,axiom,
( ~ p4(sK81(X0))
| ~ sP13(X0) ) ).
cnf(u145,axiom,
( ~ sP26(X0)
| p2(X5)
| r1(sK35(X5),sK36(X5))
| ~ r1(X0,X8)
| ~ r1(X8,X9)
| p2(X9)
| ~ p2(X8)
| ~ r1(X0,X5) ) ).
cnf(u291,axiom,
( r1(sK69(X0),sK70(X0))
| ~ sP16(X0) ) ).
cnf(u429,axiom,
( ~ sP8(X0)
| r1(X0,sK100(X0)) ) ).
cnf(u314,axiom,
( ~ p2(sK72(X0))
| ~ sP15(X0) ) ).
cnf(u400,axiom,
( ~ p2(sK98(X0))
| ~ sP9(X0) ) ).
cnf(u172,axiom,
( ~ sP25(X0)
| sP24(X1)
| r1(X1,sK37(X1))
| ~ p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u4522,negated_conjecture,
( ~ r1(sK127,X0)
| ~ r1(X0,sK132) ) ).
cnf(u187,axiom,
( ~ p2(sK43(X1))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| r1(X3,sK41(X3))
| ~ r1(X0,X1)
| ~ sP24(X0) ) ).
cnf(u419,axiom,
( r1(sK101(X0),sK102(X0))
| ~ sP8(X0) ) ).
cnf(u312,axiom,
( r1(sK72(X0),sK73(X0))
| ~ sP15(X0) ) ).
cnf(u442,axiom,
( ~ p1(sK108(X1))
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u162,axiom,
( ~ sP25(X0)
| sP24(X1)
| ~ r1(X1,X6)
| p2(X6)
| r1(sK39(X6),sK40(X6))
| ~ p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u185,axiom,
( ~ sP24(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| r1(sK41(X3),sK42(X3))
| r1(X1,sK43(X1))
| ~ r1(X0,X1) ) ).
cnf(u493,axiom,
( ~ sP3(X0)
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| r1(X1,sK116(X1))
| ~ r1(X0,X1) ) ).
cnf(u318,axiom,
( r1(sK78(X0),sK79(X0))
| ~ sP14(X0) ) ).
cnf(u440,axiom,
( ~ sP7(X0)
| r1(X0,sK104(X0)) ) ).
cnf(u4539,negated_conjecture,
~ r1(sK30(sK127),sK132) ).
cnf(u3013,negated_conjecture,
( p2(sK28(X0))
| ~ r1(sK129,X0)
| p2(X0) ) ).
cnf(u4526,negated_conjecture,
( ~ sP27(X2)
| ~ r1(X1,sK132)
| ~ r1(X2,X0)
| r1(X0,sK30(X0))
| ~ r1(X0,X1) ) ).
cnf(u191,axiom,
( ~ p2(sK46(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| ~ r1(X0,X1)
| ~ sP23(X0) ) ).
cnf(u4683,negated_conjecture,
~ r1(sK127,sK183(sK132)) ).
cnf(u446,axiom,
( ~ sP6(X0)
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| r1(sK107(X1),sK108(X1))
| ~ r1(X0,X1) ) ).
cnf(u3676,negated_conjecture,
( ~ r1(sK183(sK129),X0)
| r1(sK28(X0),sK29(X0))
| p2(X0) ) ).
cnf(u4537,negated_conjecture,
~ r1(sK131,sK132) ).
cnf(u329,axiom,
( ~ p1(sK76(X0))
| ~ sP14(X0) ) ).
cnf(u399,axiom,
( ~ p1(sK98(X0))
| ~ sP9(X0) ) ).
cnf(u459,axiom,
( ~ p3(sK111(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u352,axiom,
( ~ p2(sK86(X0))
| ~ sP12(X0) ) ).
cnf(u2386,negated_conjecture,
( r1(sK28(X0),sK29(X0))
| p2(X0)
| ~ r1(sK30(sK128),X0) ) ).
cnf(u5657,negated_conjecture,
( ~ r1(sK43(sK41(sK132)),X0)
| r1(X0,sK41(X0))
| p2(X0) ) ).
cnf(u457,axiom,
( ~ p1(sK111(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u397,axiom,
( ~ sP10(X0)
| r1(X0,sK92(X0)) ) ).
cnf(u358,axiom,
( ~ p3(sK85(X0))
| ~ sP12(X0) ) ).
cnf(u3014,negated_conjecture,
( p2(sK28(X0))
| ~ r1(sK130,X0)
| p2(X0) ) ).
cnf(u200,axiom,
( ~ p2(sK49(X0))
| ~ sP22(X0) ) ).
cnf(u739,negated_conjecture,
r1(sK125,sK126) ).
cnf(u3020,negated_conjecture,
( ~ r1(sK183(X1),sK28(X0))
| p2(X0)
| ~ r1(X1,X2)
| p2(X2)
| ~ r1(sK130,X0)
| ~ r1(sK28(X0),X3)
| p2(X3)
| ~ r1(sK125,X1) ) ).
cnf(u231,axiom,
( ~ p1(sK55(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| ~ r1(X0,X1)
| ~ sP20(X0) ) ).
cnf(u369,axiom,
( ~ p3(sK90(X0))
| ~ sP11(X0) ) ).
cnf(u463,axiom,
( ~ p2(sK110(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u356,axiom,
( ~ p1(sK85(X0))
| ~ sP12(X0) ) ).
cnf(u486,axiom,
( ~ p3(sK117(X1))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u186,axiom,
( ~ sP24(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| r1(X3,sK41(X3))
| ~ r1(sK43(X1),X7)
| ~ r1(X7,X8)
| p2(X8)
| ~ p2(X7)
| ~ r1(X0,X1) ) ).
cnf(u474,axiom,
( ~ p4(sK114(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u408,axiom,
( r1(sK96(X0),sK97(X0))
| ~ sP9(X0) ) ).
cnf(u229,axiom,
( ~ sP21(X0)
| r1(X0,sK51(X0)) ) ).
cnf(u4320,negated_conjecture,
( ~ r1(sK183(X1),sK28(X0))
| p2(X0)
| ~ r1(X1,X2)
| p2(X2)
| ~ r1(sK125,X0)
| ~ r1(sK28(X0),X3)
| p2(X3)
| ~ r1(sK125,X1) ) ).
cnf(u375,axiom,
( ~ p4(sK89(X0))
| ~ sP11(X0) ) ).
cnf(u497,axiom,
( ~ p2(sK119(X1))
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ r1(X0,X1)
| ~ sP2(X0) ) ).
cnf(u729,negated_conjecture,
r1(sK125,sK131) ).
cnf(u484,axiom,
( ~ p1(sK117(X1))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u240,axiom,
( ~ p2(sK58(X0))
| ~ sP19(X0) ) ).
cnf(u5887,negated_conjecture,
~ r1(sK128,sK183(sK183(sK125))) ).
cnf(u5329,negated_conjecture,
~ r1(sK131,sK183(sK129)) ).
cnf(u219,axiom,
( r1(sK52(X0),sK53(X0))
| ~ sP21(X0) ) ).
cnf(u373,axiom,
( ~ p2(sK89(X0))
| ~ sP11(X0) ) ).
cnf(u503,axiom,
( ~ sP2(X0)
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ p3(X1)
| ~ r1(X0,X1) ) ).
cnf(u3329,negated_conjecture,
( ~ r1(sK30(sK180),X0)
| p2(X0)
| r1(X0,sK28(X0)) ) ).
cnf(u268,axiom,
( ~ p4(sK60(X0))
| ~ sP18(X0) ) ).
cnf(u3324,negated_conjecture,
( r1(sK28(X0),sK29(X0))
| p2(X0)
| ~ r1(sK130,X0) ) ).
cnf(u5891,negated_conjecture,
~ r1(sK127,sK183(sK183(sK125))) ).
cnf(u141,axiom,
( ~ sP26(X0)
| p2(X5)
| p2(sK35(X5))
| ~ r1(X0,X8)
| ~ r1(X8,X9)
| p2(X9)
| ~ p2(X8)
| ~ r1(X0,X5) ) ).
cnf(u2320,negated_conjecture,
p2(sK30(sK128)) ).
cnf(u287,axiom,
( ~ p1(sK70(X0))
| ~ sP16(X0) ) ).
cnf(u501,axiom,
( ~ sP2(X0)
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u3457,negated_conjecture,
( ~ r1(sK182(sK180),X0)
| p2(X0)
| r1(sK28(X0),sK29(X0)) ) ).
cnf(u396,axiom,
( ~ p4(sK92(X0))
| ~ sP10(X0) ) ).
cnf(u244,axiom,
( ~ p1(sK57(X0))
| ~ sP19(X0) ) ).
cnf(u131,axiom,
( ~ sP27(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| p2(sK28(X3))
| r1(X1,sK30(X1))
| ~ r1(X0,X1) ) ).
cnf(u285,axiom,
( ~ sP17(X0)
| r1(X0,sK64(X0)) ) ).
cnf(u415,axiom,
( ~ p1(sK102(X0))
| ~ sP8(X0) ) ).
cnf(u4879,negated_conjecture,
( ~ r1(sK37(sK28(sK132)),X0)
| r1(X0,sK41(X0))
| p2(X0) ) ).
cnf(u492,axiom,
( ~ p4(sK116(X1))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u158,axiom,
( ~ sP25(X0)
| sP24(X1)
| ~ r1(X1,X6)
| p2(X6)
| p2(sK39(X6))
| ~ p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u266,axiom,
( ~ p2(sK60(X0))
| ~ sP18(X0) ) ).
cnf(u283,axiom,
( ~ p3(sK64(X0))
| ~ sP17(X0) ) ).
cnf(u129,axiom,
( ~ sP27(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| p2(sK28(X3))
| ~ r1(sK30(X1),X7)
| ~ r1(X7,X8)
| p2(X8)
| ~ p2(X7)
| ~ r1(X0,X1) ) ).
cnf(u413,axiom,
( ~ sP9(X0)
| r1(X0,sK96(X0)) ) ).
cnf(u298,axiom,
( ~ p2(sK68(X0))
| ~ sP16(X0) ) ).
cnf(u384,axiom,
( ~ p2(sK94(X0))
| ~ sP10(X0) ) ).
cnf(u5761,negated_conjecture,
p2(sK40(sK183(sK132))) ).
cnf(u156,axiom,
( ~ sP26(X0)
| ~ p2(X0)
| r1(X0,sK33(X0)) ) ).
cnf(u5780,negated_conjecture,
( ~ sP25(X1)
| ~ r1(X0,sK183(sK132))
| ~ r1(X1,X0)
| ~ r1(X0,X2)
| ~ r1(X2,X3)
| p2(X3)
| ~ p2(X2)
| sP24(X0) ) ).
cnf(u171,axiom,
( ~ sP25(X0)
| sP24(X1)
| r1(X1,sK37(X1))
| ~ r1(X1,X9)
| ~ r1(X9,X10)
| p2(X10)
| ~ p2(X9)
| ~ r1(X0,X1) ) ).
cnf(u403,axiom,
( r1(sK97(X0),sK98(X0))
| ~ sP9(X0) ) ).
cnf(u296,axiom,
( r1(sK68(X0),sK69(X0))
| ~ sP16(X0) ) ).
cnf(u426,axiom,
( ~ p2(sK100(X0))
| ~ sP8(X0) ) ).
cnf(u146,axiom,
( ~ sP26(X0)
| p2(X5)
| r1(sK35(X5),sK36(X5))
| ~ p2(X0)
| ~ r1(X0,X5) ) ).
cnf(u4538,negated_conjecture,
~ r1(sK131,sK125) ).
cnf(u169,axiom,
( ~ sP25(X0)
| sP24(X1)
| r1(sK37(X1),sK38(X1))
| ~ r1(X1,X9)
| ~ r1(X9,X10)
| p2(X10)
| ~ p2(X9)
| ~ r1(X0,X1) ) ).
cnf(u315,axiom,
( ~ p3(sK72(X0))
| ~ sP15(X0) ) ).
cnf(u302,axiom,
( r1(sK74(X0),sK75(X0))
| ~ sP15(X0) ) ).
cnf(u424,axiom,
( r1(sK100(X0),sK101(X0))
| ~ sP8(X0) ) ).
cnf(u3762,negated_conjecture,
( ~ r1(sK28(sK129),X0)
| p2(sK28(X0))
| p2(X0) ) ).
cnf(u395,axiom,
( ~ p3(sK92(X0))
| ~ sP10(X0) ) ).
cnf(u175,axiom,
( ~ sP24(X0)
| p2(X1)
| r1(sK44(X1),sK45(X1))
| ~ r1(X0,X1) ) ).
cnf(u313,axiom,
( ~ p1(sK72(X0))
| ~ sP15(X0) ) ).
cnf(u2833,negated_conjecture,
( ~ r1(sK183(sK126),X0)
| p2(sK28(X0))
| p2(X0) ) ).
cnf(u430,axiom,
( r1(sK105(X0),sK106(X0))
| ~ sP7(X0) ) ).
cnf(u4542,negated_conjecture,
~ r1(sK180,sK125) ).
cnf(u441,axiom,
( ~ sP6(X0)
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| r1(sK108(X1),sK109(X1))
| ~ r1(X0,X1) ) ).
cnf(u5988,negated_conjecture,
~ r1(sK127,sK183(sK125)) ).
cnf(u336,axiom,
( ~ p2(sK82(X0))
| ~ sP13(X0) ) ).
cnf(u184,axiom,
( ~ p2(sK43(X1))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| r1(sK41(X3),sK42(X3))
| ~ r1(X0,X1)
| ~ sP24(X0) ) ).
cnf(u5982,negated_conjecture,
~ r1(sK128,sK183(sK125)) ).
cnf(u521,axiom,
( ~ sP0(X0)
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u450,axiom,
( ~ p4(sK107(X1))
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u3524,negated_conjecture,
( ~ r1(sK30(sK180),X0)
| p2(sK28(X0))
| p2(X0) ) ).
cnf(u2678,negated_conjecture,
( ~ r1(sK129,X0)
| r1(X0,sK28(X0))
| p2(X0) ) ).
cnf(u342,axiom,
( ~ p3(sK81(X0))
| ~ sP13(X0) ) ).
cnf(u5328,negated_conjecture,
~ r1(sK130,sK129) ).
cnf(u4553,negated_conjecture,
( ~ r1(sK183(X1),sK28(X0))
| p2(X0)
| ~ r1(X1,X2)
| p2(X2)
| ~ r1(sK132,X0)
| ~ r1(sK28(X0),X3)
| p2(X3)
| ~ r1(sK125,X1) ) ).
cnf(u2270,negated_conjecture,
( ~ r1(sK132,X0)
| ~ r1(X0,X1)
| p2(X1)
| r1(X1,sK39(X1))
| ~ r1(X0,X2)
| ~ r1(X2,X3)
| p2(X3)
| ~ p2(X2)
| sP24(X0) ) ).
cnf(u215,axiom,
( ~ p1(sK53(X0))
| ~ sP21(X0) ) ).
cnf(u353,axiom,
( ~ p3(sK86(X0))
| ~ sP12(X0) ) ).
cnf(u371,axiom,
( r1(sK89(X0),sK90(X0))
| ~ sP11(X0) ) ).
cnf(u340,axiom,
( ~ p1(sK81(X0))
| ~ sP13(X0) ) ).
cnf(u470,axiom,
( ~ sP4(X0)
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| r1(sK114(X1),sK115(X1))
| ~ r1(X0,X1) ) ).
cnf(u153,axiom,
( ~ sP26(X0)
| ~ r1(X0,X8)
| ~ r1(X8,X9)
| p2(X9)
| ~ p2(X8)
| r1(sK33(X0),sK34(X0)) ) ).
cnf(u3023,negated_conjecture,
( ~ r1(sK132,sK28(X0))
| p2(X0)
| ~ r1(sK129,X0)
| p2(X1)
| ~ r1(sK28(X0),X1) ) ).
cnf(u5889,negated_conjecture,
~ r1(sK131,sK183(sK125)) ).
cnf(u213,axiom,
( ~ sP22(X0)
| r1(X0,sK47(X0)) ) ).
cnf(u359,axiom,
( ~ p4(sK85(X0))
| ~ sP12(X0) ) ).
cnf(u481,axiom,
( ~ sP4(X0)
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u4682,negated_conjecture,
~ r1(sK30(sK127),sK183(sK132)) ).
cnf(u468,axiom,
( ~ sP5(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u224,axiom,
( r1(sK51(X0),sK52(X0))
| ~ sP21(X0) ) ).
cnf(u4999,negated_conjecture,
p2(sK182(sK182(sK180))) ).
cnf(u125,axiom,
( ~ sP27(X0)
| p2(X1)
| p2(sK31(X1))
| ~ r1(X0,X1) ) ).
cnf(u203,axiom,
( r1(sK48(X0),sK49(X0))
| ~ sP22(X0) ) ).
cnf(u357,axiom,
( ~ p2(sK85(X0))
| ~ sP12(X0) ) ).
cnf(u487,axiom,
( ~ p4(sK117(X1))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u380,axiom,
( ~ p4(sK88(X0))
| ~ sP11(X0) ) ).
cnf(u230,axiom,
( ~ sP20(X0)
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| sP18(sK55(X1))
| ~ r1(X0,X1) ) ).
cnf(u730,negated_conjecture,
( ~ r1(sK130,X8)
| p1(X8) ) ).
cnf(u253,axiom,
( ~ sP19(X0)
| r1(X0,sK56(X0)) ) ).
cnf(u271,axiom,
( ~ p1(sK66(X0))
| ~ sP17(X0) ) ).
cnf(u485,axiom,
( ~ p2(sK117(X1))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u736,negated_conjecture,
~ p3(sK127) ).
cnf(u370,axiom,
( ~ p4(sK90(X0))
| ~ sP11(X0) ) ).
cnf(u508,axiom,
( ~ p3(sK121(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u228,axiom,
( ~ p4(sK51(X0))
| ~ sP21(X0) ) ).
cnf(u197,axiom,
( ~ sP23(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| ~ p3(X1)
| ~ r1(X0,X1) ) ).
cnf(u208,axiom,
( r1(sK47(X0),sK48(X0))
| ~ sP22(X0) ) ).
cnf(u514,axiom,
( ~ sP0(X0)
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| r1(sK123(X1),sK124(X1))
| ~ r1(X0,X1) ) ).
cnf(u243,axiom,
( r1(sK57(X0),sK58(X0))
| ~ sP19(X0) ) ).
cnf(u269,axiom,
( ~ sP18(X0)
| r1(X0,sK60(X0)) ) ).
cnf(u520,axiom,
( ~ sP0(X0)
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u2071,negated_conjecture,
( r1(sK37(X0),sK38(X0))
| sP24(X0)
| ~ p2(X0)
| ~ r1(sK132,X0) ) ).
cnf(u462,axiom,
( ~ p1(sK110(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u498,axiom,
( ~ p3(sK119(X1))
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ r1(X0,X1)
| ~ sP2(X0) ) ).
cnf(u142,axiom,
( ~ sP26(X0)
| p2(X5)
| p2(sK35(X5))
| ~ p2(X0)
| ~ r1(X0,X5) ) ).
cnf(u3051,negated_conjecture,
p2(sK35(sK132)) ).
cnf(u455,axiom,
( ~ sP6(X0)
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ p4(X1)
| ~ r1(X0,X1) ) ).
cnf(u241,axiom,
( ~ p3(sK58(X0))
| ~ sP19(X0) ) ).
cnf(u259,axiom,
( r1(sK61(X0),sK62(X0))
| ~ sP18(X0) ) ).
cnf(u4878,negated_conjecture,
p2(sK37(sK28(sK132))) ).
cnf(u2069,negated_conjecture,
( ~ r1(sK132,X0)
| r1(X0,sK37(X0))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p2(X2)
| ~ p2(X1)
| sP24(X0) ) ).
cnf(u282,axiom,
( ~ p2(sK64(X0))
| ~ sP17(X0) ) ).
cnf(u496,axiom,
( ~ p1(sK119(X1))
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ r1(X0,X1)
| ~ sP2(X0) ) ).
cnf(u140,axiom,
( ~ sP27(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| r1(X3,sK28(X3))
| r1(X1,sK30(X1))
| ~ r1(X0,X1) ) ).
cnf(u2099,negated_conjecture,
( ~ p2(sK38(X0))
| ~ r1(sK38(X0),X1)
| p2(X1)
| sP24(X0)
| ~ r1(X0,X2)
| ~ r1(X2,X3)
| p2(X3)
| ~ p2(X2)
| ~ r1(sK132,X0) ) ).
cnf(u2853,negated_conjecture,
( ~ r1(sK183(sK126),X0)
| r1(sK28(X0),sK29(X0))
| p2(X0) ) ).
cnf(u155,axiom,
( ~ sP26(X0)
| ~ r1(X0,X8)
| ~ r1(X8,X9)
| p2(X9)
| ~ p2(X8)
| r1(X0,sK33(X0)) ) ).
cnf(u309,axiom,
( ~ p2(sK73(X0))
| ~ sP15(X0) ) ).
cnf(u387,axiom,
( r1(sK93(X0),sK94(X0))
| ~ sP10(X0) ) ).
cnf(u2070,negated_conjecture,
( ~ r1(sK38(X0),X1)
| sP24(X0)
| ~ r1(X1,X2)
| p2(X2)
| ~ p2(X1)
| ~ p2(X0)
| ~ r1(sK132,X0) ) ).
cnf(u280,axiom,
( r1(sK64(X0),sK65(X0))
| ~ sP17(X0) ) ).
cnf(u410,axiom,
( ~ p2(sK96(X0))
| ~ sP9(X0) ) ).
cnf(u130,axiom,
( ~ p2(sK30(X1))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| p2(sK28(X3))
| ~ r1(X0,X1)
| ~ sP27(X0) ) ).
cnf(u270,axiom,
( r1(sK66(X0),sK67(X0))
| ~ sP17(X0) ) ).
cnf(u5017,negated_conjecture,
( ~ r1(sK35(sK132),X0)
| ~ r1(X1,X2)
| p2(X2)
| p2(sK41(X2))
| r1(X0,sK43(X0))
| ~ r1(X0,X1) ) ).
cnf(u310,axiom,
( ~ p3(sK73(X0))
| ~ sP15(X0) ) ).
cnf(u299,axiom,
( ~ p3(sK68(X0))
| ~ sP16(X0) ) ).
cnf(u3765,negated_conjecture,
( ~ r1(sK183(sK129),X0)
| p2(sK28(X0))
| p2(X0) ) ).
cnf(u286,axiom,
( r1(sK70(X0),sK71(X0))
| ~ sP16(X0) ) ).
cnf(u159,axiom,
( ~ p2(sK40(X6))
| sP24(X1)
| ~ r1(X1,X6)
| p2(X6)
| ~ r1(X0,X1)
| ~ r1(X1,X9)
| ~ r1(X9,X10)
| p2(X10)
| ~ p2(X9)
| ~ sP25(X0) ) ).
cnf(u297,axiom,
( ~ p1(sK68(X0))
| ~ sP16(X0) ) ).
cnf(u427,axiom,
( ~ p3(sK100(X0))
| ~ sP8(X0) ) ).
cnf(u4670,negated_conjecture,
( ~ r1(sK127,X0)
| ~ r1(X0,sK183(sK132)) ) ).
cnf(u414,axiom,
( r1(sK102(X0),sK103(X0))
| ~ sP8(X0) ) ).
cnf(u170,axiom,
( ~ sP25(X0)
| sP24(X1)
| r1(sK37(X1),sK38(X1))
| ~ p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u732,negated_conjecture,
~ p2(sK129) ).
cnf(u425,axiom,
( ~ p1(sK100(X0))
| ~ sP8(X0) ) ).
cnf(u5019,negated_conjecture,
( ~ r1(sK35(sK132),X0)
| ~ r1(X1,X2)
| p2(X2)
| r1(sK41(X2),sK42(X2))
| r1(X0,sK43(X0))
| ~ r1(X0,X1) ) ).
cnf(u168,axiom,
( ~ p2(sK38(X1))
| sP24(X1)
| ~ r1(X0,X1)
| ~ p2(X1)
| ~ sP25(X0) ) ).
cnf(u260,axiom,
( ~ p1(sK61(X0))
| ~ sP18(X0) ) ).
cnf(u2626,negated_conjecture,
( ~ r1(sK183(sK126),X0)
| r1(X0,sK28(X0))
| p2(X0) ) ).
cnf(u233,axiom,
( ~ p3(sK55(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| ~ r1(X0,X1)
| ~ sP20(X0) ) ).
cnf(u2123,negated_conjecture,
p2(sK183(sK126)) ).
cnf(u199,axiom,
( ~ p1(sK49(X0))
| ~ sP22(X0) ) ).
cnf(u337,axiom,
( ~ p3(sK82(X0))
| ~ sP13(X0) ) ).
cnf(u324,axiom,
( ~ p1(sK77(X0))
| ~ sP14(X0) ) ).
cnf(u3408,negated_conjecture,
( ~ r1(sK30(sK180),X0)
| p2(X0)
| r1(sK28(X0),sK29(X0)) ) ).
cnf(u3525,negated_conjecture,
( ~ r1(sK181,X0)
| p2(sK28(X0))
| p2(X0) ) ).
cnf(u465,axiom,
( ~ p4(sK110(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u452,axiom,
( ~ sP6(X0)
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u4672,negated_conjecture,
( ~ r1(X0,sK183(sK132))
| ~ r1(sK180,X0) ) ).
cnf(u341,axiom,
( ~ p2(sK81(X0))
| ~ sP13(X0) ) ).
cnf(u471,axiom,
( ~ p1(sK114(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u364,axiom,
( ~ p4(sK84(X0))
| ~ sP12(X0) ) ).
cnf(u214,axiom,
( r1(sK53(X0),sK54(X0))
| ~ sP21(X0) ) ).
cnf(u1752,negated_conjecture,
p3(sK126) ).
cnf(u3673,negated_conjecture,
( r1(sK28(X0),sK29(X0))
| ~ r1(sK28(sK129),X0)
| p2(X0) ) ).
cnf(u5987,negated_conjecture,
~ r1(sK30(sK127),sK183(sK125)) ).
cnf(u237,axiom,
( ~ sP20(X0)
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| ~ p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u5333,negated_conjecture,
~ r1(sK180,sK183(sK129)) ).
cnf(u354,axiom,
( ~ p4(sK86(X0))
| ~ sP12(X0) ) ).
cnf(u737,negated_conjecture,
r1(sK125,sK127) ).
cnf(u126,axiom,
( ~ p2(sK32(X1))
| p2(X1)
| ~ r1(X0,X1)
| ~ sP27(X0) ) ).
cnf(u212,axiom,
( ~ p4(sK47(X0))
| ~ sP22(X0) ) ).
cnf(u227,axiom,
( ~ p3(sK51(X0))
| ~ sP21(X0) ) ).
cnf(u381,axiom,
( ~ sP11(X0)
| r1(X0,sK88(X0)) ) ).
cnf(u511,axiom,
( ~ sP1(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u482,axiom,
( ~ sP4(X0)
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u124,axiom,
r1(X0,X0) ).
cnf(u254,axiom,
( r1(sK62(X0),sK63(X0))
| ~ sP18(X0) ) ).
cnf(u5898,negated_conjecture,
( ~ r1(sK41(sK43(sK41(sK132))),X0)
| r1(X0,sK41(X0))
| p2(X0) ) ).
cnf(u225,axiom,
( ~ p1(sK51(X0))
| ~ sP21(X0) ) ).
cnf(u3454,negated_conjecture,
( ~ r1(sK30(sK130),X0)
| p2(sK28(X0))
| p2(X0) ) ).
cnf(u509,axiom,
( ~ p4(sK121(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u480,axiom,
( ~ sP4(X0)
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| r1(X1,sK113(X1))
| ~ r1(X0,X1) ) ).
cnf(u252,axiom,
( ~ p4(sK56(X0))
| ~ sP19(X0) ) ).
cnf(u4373,negated_conjecture,
( ~ r1(sK132,X0)
| r1(X0,sK28(X0))
| p2(X0) ) ).
cnf(u460,axiom,
( ~ p4(sK111(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u3330,negated_conjecture,
( ~ r1(sK181,X0)
| p2(X0)
| r1(X0,sK28(X0)) ) ).
cnf(u139,axiom,
( ~ p2(sK30(X1))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| r1(X3,sK28(X3))
| ~ r1(X0,X1)
| ~ sP27(X0) ) ).
cnf(u499,axiom,
( ~ p4(sK119(X1))
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ r1(X0,X1)
| ~ sP2(X0) ) ).
cnf(u264,axiom,
( r1(sK60(X0),sK61(X0))
| ~ sP18(X0) ) ).
cnf(u394,axiom,
( ~ p2(sK92(X0))
| ~ sP10(X0) ) ).
cnf(u242,axiom,
( ~ p4(sK58(X0))
| ~ sP19(X0) ) ).
cnf(u523,negated_conjecture,
( ~ p2(sK183(X182))
| ~ r1(X182,X183)
| p2(X183)
| ~ r1(sK125,X182) ) ).
cnf(u4376,negated_conjecture,
r1(sK132,sK28(sK132)) ).
cnf(u5888,negated_conjecture,
~ r1(sK131,sK183(sK183(sK125))) ).
cnf(u3458,negated_conjecture,
( ~ r1(sK182(sK180),X0)
| p2(X0)
| r1(X0,sK28(X0)) ) ).
cnf(u137,axiom,
( ~ sP27(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| r1(sK28(X3),sK29(X3))
| r1(X1,sK30(X1))
| ~ r1(X0,X1) ) ).
cnf(u5022,negated_conjecture,
~ r1(sK35(sK132),sK29(sK132)) ).
cnf(u392,axiom,
( r1(sK92(X0),sK93(X0))
| ~ sP10(X0) ) ).
cnf(u265,axiom,
( ~ p1(sK60(X0))
| ~ sP18(X0) ) ).
cnf(u143,axiom,
( ~ p2(sK36(X5))
| p2(X5)
| ~ r1(X0,X5)
| ~ r1(X0,X8)
| ~ r1(X8,X9)
| p2(X9)
| ~ p2(X8)
| ~ sP26(X0) ) ).
cnf(u281,axiom,
( ~ p1(sK64(X0))
| ~ sP17(X0) ) ).
cnf(u516,axiom,
( ~ p2(sK123(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ r1(X0,X1)
| ~ sP0(X0) ) ).
cnf(u411,axiom,
( ~ p3(sK96(X0))
| ~ sP9(X0) ) ).
cnf(u304,axiom,
( ~ p2(sK74(X0))
| ~ sP15(X0) ) ).
cnf(u398,axiom,
( r1(sK98(X0),sK99(X0))
| ~ sP9(X0) ) ).
cnf(u154,axiom,
( r1(sK33(X0),sK34(X0))
| ~ p2(X0)
| ~ sP26(X0) ) ).
cnf(u4523,negated_conjecture,
( ~ r1(X0,sK132)
| ~ r1(sK131,X0) ) ).
cnf(u5779,negated_conjecture,
( ~ sP25(X1)
| ~ r1(X0,sK183(sK132))
| ~ r1(X1,X0)
| ~ p2(X0)
| sP24(X0) ) ).
cnf(u409,axiom,
( ~ p1(sK96(X0))
| ~ sP9(X0) ) ).
cnf(u152,axiom,
( ~ p2(sK34(X0))
| ~ p2(X0)
| ~ sP26(X0) ) ).
cnf(u4677,negated_conjecture,
~ r1(sK128,sK183(sK132)) ).
cnf(u5787,negated_conjecture,
( ~ r1(X0,sK183(sK132))
| ~ r1(sK132,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p2(X2)
| ~ p2(X1)
| sP24(X0) ) ).
cnf(u3496,negated_conjecture,
( ~ r1(sK30(sK130),X0)
| p2(X0)
| r1(sK28(X0),sK29(X0)) ) ).
cnf(u183,axiom,
( ~ sP24(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| r1(sK41(X3),sK42(X3))
| ~ r1(sK43(X1),X7)
| ~ r1(X7,X8)
| p2(X8)
| ~ p2(X7)
| ~ r1(X0,X1) ) ).
cnf(u308,axiom,
( ~ p1(sK73(X0))
| ~ sP15(X0) ) ).
cnf(u438,axiom,
( ~ p3(sK104(X0))
| ~ sP7(X0) ) ).
cnf(u2098,negated_conjecture,
( ~ r1(sK38(X0),X1)
| sP24(X0)
| ~ r1(X1,X2)
| p2(X2)
| ~ p2(X1)
| ~ r1(X0,X3)
| ~ r1(X3,X4)
| p2(X4)
| ~ p2(X3)
| ~ r1(sK132,X0) ) ).
cnf(u4529,negated_conjecture,
~ r1(sK128,sK132) ).
cnf(u181,axiom,
( ~ p2(sK43(X1))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| ~ p2(sK42(X3))
| ~ r1(X0,X1)
| ~ sP24(X0) ) ).
cnf(u321,axiom,
( ~ p3(sK78(X0))
| ~ sP14(X0) ) ).
cnf(u349,axiom,
( ~ sP13(X0)
| r1(X0,sK80(X0)) ) ).
cnf(u436,axiom,
( ~ p1(sK104(X0))
| ~ sP7(X0) ) ).
cnf(u327,axiom,
( ~ p4(sK77(X0))
| ~ sP14(X0) ) ).
cnf(u449,axiom,
( ~ p3(sK107(X1))
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u127,axiom,
( ~ sP27(X0)
| p2(X1)
| r1(sK31(X1),sK32(X1))
| ~ r1(X0,X1) ) ).
cnf(u192,axiom,
( ~ p3(sK46(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| ~ r1(X0,X1)
| ~ sP23(X0) ) ).
cnf(u325,axiom,
( ~ p2(sK77(X0))
| ~ sP14(X0) ) ).
cnf(u3409,negated_conjecture,
( r1(sK28(X0),sK29(X0))
| p2(X0)
| ~ r1(sK181,X0) ) ).
cnf(u348,axiom,
( ~ p4(sK80(X0))
| ~ sP13(X0) ) ).
cnf(u198,axiom,
( r1(sK49(X0),sK50(X0))
| ~ sP22(X0) ) ).
cnf(u221,axiom,
( ~ p2(sK52(X0))
| ~ sP21(X0) ) ).
cnf(u367,axiom,
( ~ p1(sK90(X0))
| ~ sP11(X0) ) ).
cnf(u453,axiom,
( ~ sP6(X0)
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u338,axiom,
( ~ p4(sK82(X0))
| ~ sP13(X0) ) ).
cnf(u476,axiom,
( ~ p1(sK113(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u196,axiom,
( ~ sP23(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| ~ p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u735,negated_conjecture,
r1(sK125,sK128) ).
cnf(u3386,negated_conjecture,
( ~ r1(sK183(sK130),X0)
| p2(X0)
| r1(X0,sK28(X0)) ) ).
cnf(u211,axiom,
( ~ p3(sK47(X0))
| ~ sP22(X0) ) ).
cnf(u365,axiom,
( ~ sP12(X0)
| r1(X0,sK84(X0)) ) ).
cnf(u3021,negated_conjecture,
( ~ r1(sK132,sK28(X0))
| p2(X0)
| ~ r1(sK180,X0)
| p2(X1)
| ~ r1(sK28(X0),X1) ) ).
cnf(u3016,negated_conjecture,
( p2(sK28(X0))
| ~ r1(sK180,X0)
| p2(X0) ) ).
cnf(u466,axiom,
( ~ sP5(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| r1(X1,sK110(X1))
| ~ r1(X0,X1) ) ).
cnf(u238,axiom,
( r1(sK58(X0),sK59(X0))
| ~ sP19(X0) ) ).
cnf(u3019,negated_conjecture,
( ~ r1(sK132,sK28(X0))
| p2(X0)
| ~ r1(sK130,X0)
| p2(X1)
| ~ r1(sK28(X0),X1) ) ).
cnf(u738,negated_conjecture,
( ~ r1(sK126,X2)
| p3(X2) ) ).
cnf(u5327,negated_conjecture,
~ r1(sK130,sK183(sK129)) ).
cnf(u209,axiom,
( ~ p1(sK47(X0))
| ~ sP22(X0) ) ).
cnf(u3022,negated_conjecture,
( ~ r1(sK183(X1),sK28(X0))
| p2(X0)
| ~ r1(X1,X2)
| p2(X2)
| ~ r1(sK180,X0)
| ~ r1(sK28(X0),X3)
| p2(X3)
| ~ r1(sK125,X1) ) ).
cnf(u355,axiom,
( r1(sK85(X0),sK86(X0))
| ~ sP12(X0) ) ).
cnf(u3455,negated_conjecture,
( ~ r1(sK183(sK130),X0)
| p2(sK28(X0))
| p2(X0) ) ).
cnf(u378,axiom,
( ~ p2(sK88(X0))
| ~ sP11(X0) ) ).
cnf(u464,axiom,
( ~ p3(sK110(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u236,axiom,
( ~ sP20(X0)
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| ~ p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u2679,negated_conjecture,
( ~ r1(sK130,X0)
| r1(X0,sK28(X0))
| p2(X0) ) ).
cnf(u3588,negated_conjecture,
p2(sK28(sK30(sK129))) ).
cnf(u251,axiom,
( ~ p3(sK56(X0))
| ~ sP19(X0) ) ).
cnf(u222,axiom,
( ~ p3(sK52(X0))
| ~ sP21(X0) ) ).
cnf(u483,axiom,
( ~ sP3(X0)
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| r1(sK117(X1),sK118(X1))
| ~ r1(X0,X1) ) ).
cnf(u376,axiom,
( r1(sK88(X0),sK89(X0))
| ~ sP11(X0) ) ).
cnf(u506,axiom,
( ~ p1(sK121(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u226,axiom,
( ~ p2(sK51(X0))
| ~ sP21(X0) ) ).
cnf(u4845,negated_conjecture,
( ~ r1(sK43(sK29(sK132)),X0)
| r1(X0,sK41(X0))
| p2(X0) ) ).
cnf(u249,axiom,
( ~ p1(sK56(X0))
| ~ sP19(X0) ) ).
cnf(u267,axiom,
( ~ p3(sK60(X0))
| ~ sP18(X0) ) ).
cnf(u382,axiom,
( r1(sK94(X0),sK95(X0))
| ~ sP10(X0) ) ).
cnf(u504,axiom,
( ~ sP2(X0)
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ p4(X1)
| ~ r1(X0,X1) ) ).
cnf(u319,axiom,
( ~ p1(sK78(X0))
| ~ sP14(X0) ) ).
cnf(u255,axiom,
( ~ p1(sK62(X0))
| ~ sP18(X0) ) ).
cnf(u2067,negated_conjecture,
( ~ r1(sK132,X0)
| r1(sK37(X0),sK38(X0))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p2(X2)
| ~ p2(X1)
| sP24(X0) ) ).
cnf(u288,axiom,
( ~ p2(sK70(X0))
| ~ sP16(X0) ) ).
cnf(u510,axiom,
( ~ sP1(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| r1(X1,sK121(X1))
| ~ r1(X0,X1) ) ).
cnf(u138,axiom,
( ~ sP27(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| r1(X3,sK28(X3))
| ~ r1(sK30(X1),X7)
| ~ r1(X7,X8)
| p2(X8)
| ~ p2(X7)
| ~ r1(X0,X1) ) ).
cnf(u393,axiom,
( ~ p1(sK92(X0))
| ~ sP10(X0) ) ).
cnf(u491,axiom,
( ~ p3(sK116(X1))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u294,axiom,
( ~ p3(sK69(X0))
| ~ sP16(X0) ) ).
cnf(u136,axiom,
( ~ p2(sK30(X1))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| r1(sK28(X3),sK29(X3))
| ~ r1(X0,X1)
| ~ sP27(X0) ) ).
cnf(u2450,negated_conjecture,
( ~ r1(sK180,X0)
| p1(X0)
| p2(X0)
| p3(X0)
| p4(X0)
| ~ r1(X0,X1) ) ).
cnf(u2956,negated_conjecture,
( ~ r1(sK183(sK131),X0)
| p2(sK28(X0))
| p2(X0) ) ).
cnf(u5782,negated_conjecture,
( ~ r1(X0,sK183(sK132))
| ~ r1(sK132,X0)
| ~ p2(X0)
| sP24(X0) ) ).
cnf(u5021,negated_conjecture,
( ~ r1(sK35(sK132),X0)
| ~ r1(X1,X2)
| p2(X2)
| r1(X2,sK41(X2))
| r1(X0,sK43(X0))
| ~ r1(X0,X1) ) ).
cnf(u167,axiom,
( ~ p2(sK38(X1))
| sP24(X1)
| ~ r1(X0,X1)
| ~ r1(X1,X9)
| ~ r1(X9,X10)
| p2(X10)
| ~ p2(X9)
| ~ sP25(X0) ) ).
cnf(u305,axiom,
( ~ p3(sK74(X0))
| ~ sP15(X0) ) ).
cnf(u292,axiom,
( ~ p1(sK69(X0))
| ~ sP16(X0) ) ).
cnf(u489,axiom,
( ~ p1(sK116(X1))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u422,axiom,
( ~ p3(sK101(X0))
| ~ sP8(X0) ) ).
cnf(u335,axiom,
( ~ p1(sK82(X0))
| ~ sP13(X0) ) ).
cnf(u165,axiom,
( ~ sP25(X0)
| sP24(X1)
| ~ r1(sK38(X1),X4)
| ~ r1(X4,X5)
| p2(X5)
| ~ p2(X4)
| ~ r1(X1,X9)
| ~ r1(X9,X10)
| p2(X10)
| ~ p2(X9)
| ~ r1(X0,X1) ) ).
cnf(u311,axiom,
( ~ p4(sK73(X0))
| ~ sP15(X0) ) ).
cnf(u433,axiom,
( ~ p3(sK105(X0))
| ~ sP7(X0) ) ).
cnf(u420,axiom,
( ~ p1(sK101(X0))
| ~ sP8(X0) ) ).
cnf(u176,axiom,
( ~ sP24(X0)
| p2(X1)
| r1(X1,sK44(X1))
| ~ r1(X0,X1) ) ).
cnf(u439,axiom,
( ~ p4(sK104(X0))
| ~ sP7(X0) ) ).
cnf(u182,axiom,
( ~ p2(sK42(X3))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| ~ r1(X0,X1)
| r1(X1,sK43(X1))
| ~ sP24(X0) ) ).
cnf(u4540,negated_conjecture,
~ r1(sK127,sK132) ).
cnf(u437,axiom,
( ~ p2(sK104(X0))
| ~ sP7(X0) ) ).
cnf(u258,axiom,
( ~ p4(sK62(X0))
| ~ sP18(X0) ) ).
cnf(u332,axiom,
( ~ p4(sK76(X0))
| ~ sP14(X0) ) ).
cnf(u180,axiom,
( ~ p2(sK42(X3))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(X3)
| ~ r1(X0,X1)
| ~ r1(sK43(X1),X7)
| ~ r1(X7,X8)
| p2(X8)
| ~ p2(X7)
| ~ sP24(X0) ) ).
cnf(u3017,negated_conjecture,
( ~ r1(sK183(sK125),X0)
| p2(sK28(X0))
| p2(X0) ) ).
cnf(u205,axiom,
( ~ p2(sK48(X0))
| ~ sP22(X0) ) ).
cnf(u2384,negated_conjecture,
( ~ r1(sK30(sK128),X0)
| p2(X0)
| r1(X0,sK28(X0)) ) ).
cnf(u351,axiom,
( ~ p1(sK86(X0))
| ~ sP12(X0) ) ).
cnf(u322,axiom,
( ~ p4(sK78(X0))
| ~ sP14(X0) ) ).
cnf(u4680,negated_conjecture,
~ r1(sK131,sK183(sK132)) ).
cnf(u3415,negated_conjecture,
r1(sK129,sK28(sK129)) ).
cnf(u5330,negated_conjecture,
~ r1(sK131,sK129) ).
cnf(u195,axiom,
( ~ sP23(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| ~ p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u5314,negated_conjecture,
~ r1(sK128,sK183(sK129)) ).
cnf(u3665,negated_conjecture,
( ~ r1(sK183(sK129),X0)
| r1(X0,sK28(X0))
| p2(X0) ) ).
cnf(u193,axiom,
( ~ p4(sK46(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| ~ r1(X0,X1)
| ~ sP23(X0) ) ).
cnf(u339,axiom,
( r1(sK81(X0),sK82(X0))
| ~ sP13(X0) ) ).
cnf(u477,axiom,
( ~ p2(sK113(X1))
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u728,negated_conjecture,
~ p1(sK131) ).
cnf(u362,axiom,
( ~ p2(sK84(X0))
| ~ sP12(X0) ) ).
cnf(u448,axiom,
( ~ p2(sK107(X1))
| ~ r1(X1,X2)
| p4(X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u3018,negated_conjecture,
( p2(sK28(X0))
| ~ r1(sK125,X0)
| p2(X0) ) ).
cnf(u220,axiom,
( ~ p1(sK52(X0))
| ~ sP21(X0) ) ).
cnf(u4547,negated_conjecture,
r1(sK28(sK132),sK29(sK132)) ).
cnf(u3024,negated_conjecture,
( ~ r1(sK183(X1),sK28(X0))
| p2(X0)
| ~ r1(X1,X2)
| p2(X2)
| ~ r1(sK129,X0)
| ~ r1(sK28(X0),X3)
| p2(X3)
| ~ r1(sK125,X1) ) ).
cnf(u235,axiom,
( ~ sP20(X0)
| ~ r1(X1,X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| p4(X5)
| p3(X5)
| p2(X5)
| p1(X5)
| ~ r1(X5,X6)
| p4(X6)
| p3(X6)
| p2(X6)
| p1(X6)
| ~ r1(X6,X7)
| r1(X1,sK55(X1))
| ~ r1(X0,X1) ) ).
cnf(u467,axiom,
( ~ sP5(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u360,axiom,
( r1(sK84(X0),sK85(X0))
| ~ sP12(X0) ) ).
cnf(u490,axiom,
( ~ p2(sK116(X1))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u210,axiom,
( ~ p2(sK47(X0))
| ~ sP22(X0) ) ).
cnf(u1826,negated_conjecture,
p3(sK183(sK126)) ).
cnf(u379,axiom,
( ~ p3(sK88(X0))
| ~ sP11(X0) ) ).
cnf(u366,axiom,
( r1(sK90(X0),sK91(X0))
| ~ sP11(X0) ) ).
cnf(u488,axiom,
( ~ sP3(X0)
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| r1(sK116(X1),sK117(X1))
| ~ r1(X0,X1) ) ).
cnf(u239,axiom,
( ~ p1(sK58(X0))
| ~ sP19(X0) ) ).
cnf(u377,axiom,
( ~ p1(sK88(X0))
| ~ sP11(X0) ) ).
cnf(u507,axiom,
( ~ p2(sK121(X1))
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u272,axiom,
( ~ p2(sK66(X0))
| ~ sP17(X0) ) ).
cnf(u494,axiom,
( ~ sP3(X0)
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| p4(X4)
| p3(X4)
| p2(X4)
| p1(X4)
| ~ r1(X4,X5)
| ~ p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u250,axiom,
( ~ p2(sK56(X0))
| ~ sP19(X0) ) ).
cnf(u2317,negated_conjecture,
p1(sK30(sK130)) ).
cnf(u505,axiom,
( ~ sP1(X0)
| ~ r1(X1,X2)
| p3(X2)
| p2(X2)
| p1(X2)
| ~ r1(X2,X3)
| p4(X3)
| p3(X3)
| p2(X3)
| p1(X3)
| ~ r1(X3,X4)
| r1(sK121(X1),sK122(X1))
| ~ r1(X0,X1) ) ).
cnf(u5331,negated_conjecture,
~ r1(sK30(sK127),sK183(sK129)) ).
cnf(u278,axiom,
( ~ p3(sK65(X0))
| ~ sP17(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL661+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n005.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 16:23:32 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.47/2.38 % (4182960)Detected formulas, will run a generic FOF schedule.
% 10.47/2.38 % (4182969)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1161714186:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.47/2.38 % (4182965)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=98867401:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.47/2.38 % (4182966)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=468934685:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.47/2.38 % (4182967)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=4186701542:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.47/2.38 % (4182969)Instruction limit reached!
% 10.47/2.38 % (4182969)------------------------------
% 10.47/2.38 % (4182969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.38 % (4182969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.38 % (4182969)CaDiCaL version: 2.1.3
% 10.47/2.38 % (4182969)Termination reason: Instruction limit
% 10.47/2.38 % (4182969)Termination phase: Saturation
% 10.47/2.38 % (4182969)Time elapsed: 0.031 s
% 10.47/2.38 % (4182969)Peak memory usage: 89 MB
% 10.47/2.38 % (4182969)Instructions burned: 119 (million)
% 10.47/2.38 % (4182968)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2954532574:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.47/2.38 % (4182970)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1976387921:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.47/2.38 % (4182971)dis-21_1_sil=8000:lcm=predicate:random_seed=3820543916: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)
% 10.47/2.38 % (4182970)Instruction limit reached!
% 10.47/2.38 % (4182970)------------------------------
% 10.47/2.38 % (4182970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.38 % (4182970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.38 % (4182970)CaDiCaL version: 2.1.3
% 10.47/2.38 % (4182970)Termination reason: Instruction limit
% 10.47/2.38 % (4182970)Termination phase: Saturation
% 10.47/2.38 % (4182970)Time elapsed: 0.041 s
% 10.47/2.38 % (4182970)Peak memory usage: 91 MB
% 10.47/2.38 % (4182970)Instructions burned: 141 (million)
% 10.47/2.38 % (4182968)Instruction limit reached!
% 10.47/2.38 % (4182968)------------------------------
% 10.47/2.38 % (4182968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.38 % (4182968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.38 % (4182968)CaDiCaL version: 2.1.3
% 10.47/2.38 % (4182968)Termination reason: Instruction limit
% 10.47/2.38 % (4182968)Termination phase: Blocked clause elimination
% 10.47/2.38 % (4182968)Time elapsed: 0.056 s
% 10.47/2.38 % (4182968)Peak memory usage: 88 MB
% 10.47/2.38 % (4182968)Instructions burned: 110 (million)
% 10.47/2.38 % (4182971)Instruction limit reached!
% 10.47/2.38 % (4182971)------------------------------
% 10.47/2.38 % (4182971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.38 % (4182971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.38 % (4182971)CaDiCaL version: 2.1.3
% 10.47/2.38 % (4182971)Termination reason: Instruction limit
% 10.47/2.38 % (4182971)Termination phase: Saturation
% 10.47/2.38 % (4182971)Time elapsed: 0.064 s
% 10.47/2.38 % (4182971)Peak memory usage: 90 MB
% 10.47/2.38 % (4182971)Instructions burned: 131 (million)
% 10.47/2.38 % (4182977)lrs+10_1_sil=8000:sp=occurrence:random_seed=511688701:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 10.47/2.38 % (4182980)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3143539256:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.47/2.38 % (4182981)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3011687534:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 10.47/2.38 % (4182980)Instruction limit reached!
% 10.47/2.38 % (4182980)------------------------------
% 10.47/2.38 % (4182980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.38 % (4182980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.88 % (4182980)CaDiCaL version: 2.1.3
% 13.52/2.88 % (4182980)Termination reason: Instruction limit
% 13.52/2.88 % (4182980)Termination phase: Saturation
% 13.52/2.88 % (4182980)Time elapsed: 0.036 s
% 13.52/2.88 % (4182980)Peak memory usage: 90 MB
% 13.52/2.88 % (4182980)Instructions burned: 158 (million)
% 13.52/2.88 % (4182982)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=1699710234:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 13.52/2.88 % (4182977)Instruction limit reached!
% 13.52/2.88 % (4182977)------------------------------
% 13.52/2.88 % (4182977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.88 % (4182977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.88 % (4182977)CaDiCaL version: 2.1.3
% 13.52/2.88 % (4182977)Termination reason: Instruction limit
% 13.52/2.88 % (4182977)Termination phase: Saturation
% 13.52/2.88 % (4182977)Time elapsed: 0.140 s
% 13.52/2.88 % (4182977)Peak memory usage: 95 MB
% 13.52/2.88 % (4182977)Instructions burned: 287 (million)
% 13.52/2.88 % (4182981)Refutation not found, incomplete strategy
% 13.52/2.88 % (4182981)------------------------------
% 13.52/2.88 % (4182981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.88 % (4182981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.88 % (4182981)CaDiCaL version: 2.1.3
% 13.52/2.88 % (4182981)Termination reason: Refutation not found, incomplete strategy
% 13.52/2.88 % (4182981)Time elapsed: 0.108 s
% 13.52/2.88 % (4182981)Peak memory usage: 92 MB
% 13.52/2.88 % (4182981)Instructions burned: 211 (million)
% 13.52/2.88 % (4182986)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1519278253:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 13.52/2.88 % (4182982)Instruction limit reached!
% 13.52/2.88 % (4182982)------------------------------
% 13.52/2.88 % (4182982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.88 % (4182982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.88 % (4182982)CaDiCaL version: 2.1.3
% 13.52/2.88 % (4182982)Termination reason: Instruction limit
% 13.52/2.88 % (4182982)Termination phase: Saturation
% 13.52/2.88 % (4182982)Time elapsed: 0.116 s
% 13.52/2.88 % (4182982)Peak memory usage: 90 MB
% 13.52/2.88 % (4182982)Instructions burned: 249 (million)
% 13.52/2.88 % (4182986)Instruction limit reached!
% 13.52/2.88 % (4182986)------------------------------
% 13.52/2.88 % (4182986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.88 % (4182986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.88 % (4182986)CaDiCaL version: 2.1.3
% 13.52/2.88 % (4182986)Termination reason: Instruction limit
% 13.52/2.88 % (4182986)Termination phase: Saturation
% 13.52/2.88 % (4182986)Time elapsed: 0.079 s
% 13.52/2.88 % (4182986)Peak memory usage: 92 MB
% 13.52/2.88 % (4182986)Instructions burned: 299 (million)
% 13.52/2.88 % (4182988)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1215629112:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 13.52/2.88 % (4182990)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2561566246:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 13.52/2.88 % (4182981)------------------------------
% 13.52/2.88 % (4182981)------------------------------
% 13.52/2.88 % (4182991)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4081712506:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 13.52/2.88 % (4182990)Instruction limit reached!
% 13.52/2.88 % (4182990)------------------------------
% 13.52/2.88 % (4182990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.88 % (4182990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.88 % (4182990)CaDiCaL version: 2.1.3
% 13.52/2.88 % (4182990)Termination reason: Instruction limit
% 13.52/2.88 % (4182990)Termination phase: Saturation
% 13.52/2.88 % (4182990)Time elapsed: 0.058 s
% 13.52/2.88 % (4182990)Peak memory usage: 92 MB
% 13.52/2.88 % (4182990)Instructions burned: 113 (million)
% 13.52/2.88 % (4182991)Instruction limit reached!
% 13.52/2.88 % (4182991)------------------------------
% 13.52/2.88 % (4182991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.88 % (4182991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.88 % (4182991)CaDiCaL version: 2.1.3
% 13.52/2.88 % (4182991)Termination reason: Instruction limit
% 13.52/2.88 % (4182991)Termination phase: Blocked clause elimination
% 13.52/2.88 % (4182991)Time elapsed: 0.036 s
% 13.52/2.88 % (4182991)Peak memory usage: 87 MB
% 13.52/2.88 % (4182991)Instructions burned: 130 (million)
% 13.52/2.88 % (4182995)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2319370036:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 13.52/2.88 % (4182997)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3849456699:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 13.52/2.88 % (4182996)lrs+10_1_sil=8000:sp=occurrence:random_seed=1727164021:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 13.52/2.88 % (4182995)Instruction limit reached!
% 13.52/2.88 % (4182995)------------------------------
% 13.52/2.88 % (4182995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.88 % (4182995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.88 % (4182995)CaDiCaL version: 2.1.3
% 13.52/2.88 % (4182995)Termination reason: Instruction limit
% 13.52/2.88 % (4182995)Termination phase: Property scanning
% 13.52/2.88 % (4182995)Time elapsed: 0.042 s
% 13.52/2.88 % (4182995)Peak memory usage: 87 MB
% 13.52/2.88 % (4182995)Instructions burned: 115 (million)
% 13.52/2.88 % (4182997)Instruction limit reached!
% 13.52/2.88 % (4182997)------------------------------
% 13.52/2.88 % (4182997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.88 % (4182997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.88 % (4182997)CaDiCaL version: 2.1.3
% 13.52/2.88 % (4182997)Termination reason: Instruction limit
% 13.52/2.88 % (4182997)Termination phase: Saturation
% 13.52/2.88 % (4182997)Time elapsed: 0.090 s
% 13.52/2.88 % (4182997)Peak memory usage: 91 MB
% 13.52/2.88 % (4182997)Instructions burned: 440 (million)
% 13.52/2.88 % (4183001)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2807702656:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 13.52/2.88 % (4183002)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2433767842:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2990 on theBenchmark for (2990ds/134Mi)
% 13.52/2.88 % (4183002)Instruction limit reached!
% 13.52/2.88 % (4183002)------------------------------
% 13.52/2.88 % (4183002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.88 % (4183002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.88 % (4183002)CaDiCaL version: 2.1.3
% 13.52/2.88 % (4183002)Termination reason: Instruction limit
% 13.52/2.88 % (4183002)Termination phase: Saturation
% 13.52/2.88 % (4183002)Time elapsed: 0.039 s
% 13.52/2.88 % (4183002)Peak memory usage: 90 MB
% 13.52/2.88 % (4183002)Instructions burned: 148 (million)
% 13.52/2.88 % (4183005)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=459257330:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 13.52/2.88 % (4182996)Instruction limit reached!
% 13.52/2.88 % (4182996)------------------------------
% 13.52/2.88 % (4182996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.88 % (4182996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.88 % (4182996)CaDiCaL version: 2.1.3
% 13.52/2.88 % (4182996)Termination reason: Instruction limit
% 13.52/2.88 % (4182996)Termination phase: Saturation
% 13.52/2.88 % (4182996)Time elapsed: 0.414 s
% 13.52/2.88 % (4182996)Peak memory usage: 99 MB
% 13.52/2.88 % (4182996)Instructions burned: 909 (million)
% 13.52/2.88 % (4183005)Instruction limit reached!
% 13.52/2.88 % (4183005)------------------------------
% 13.52/2.88 % (4183005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.88 % (4183005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.88 % (4183005)CaDiCaL version: 2.1.3
% 13.52/2.88 % (4183005)Termination reason: Instruction limit
% 13.52/2.88 % (4183005)Termination phase: Saturation
% 13.52/2.88 % (4183005)Time elapsed: 0.119 s
% 13.52/2.88 % (4183005)Peak memory usage: 90 MB
% 13.52/2.88 % (4183005)Instructions burned: 595 (million)
% 13.52/2.88 % (4183007)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4064094101:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 13.52/2.88 % (4183008)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=502966899:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 13.52/2.88 % (4183008)Instruction limit reached!
% 13.52/2.88 % (4183008)------------------------------
% 13.52/2.88 % (4183008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.88 % (4183008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.88 % (4183008)CaDiCaL version: 2.1.3
% 13.52/2.88 % (4183008)Termination reason: Instruction limit
% 13.52/2.88 % (4183008)Termination phase: Saturation
% 13.52/2.88 % (4183008)Time elapsed: 0.032 s
% 13.52/2.88 % (4183008)Peak memory usage: 92 MB
% 13.52/2.88 % (4183008)Instructions burned: 128 (million)
% 13.52/2.88 % (4183011)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1612155752:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi)
% 13.52/2.88 % (4183011)Instruction limit reached!
% 13.52/2.88 % (4183011)------------------------------
% 13.52/2.88 % (4183011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.88 % (4183011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.88 % (4183011)CaDiCaL version: 2.1.3
% 13.52/2.88 % (4183011)Termination reason: Instruction limit
% 13.52/2.88 % (4183011)Termination phase: Saturation
% 13.52/2.88 % (4183011)Time elapsed: 0.028 s
% 13.52/2.88 % (4183011)Peak memory usage: 90 MB
% 13.52/2.88 % (4183011)Instructions burned: 137 (million)
% 13.52/2.88 % (4182966)First to succeed.
% 13.52/2.88 % (4182966)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4182960"
% 13.52/2.88 % (4183013)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4255920707:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi)
% 13.52/2.88 % (4183013)Instruction limit reached!
% 13.52/2.88 % (4183013)------------------------------
% 13.52/2.88 % (4183013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.88 % (4183013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.88 % (4183013)CaDiCaL version: 2.1.3
% 13.52/2.88 % (4183013)Termination reason: Instruction limit
% 13.52/2.88 % (4183013)Termination phase: Saturation
% 13.52/2.88 % (4183013)Time elapsed: 0.040 s
% 13.52/2.88 % (4183013)Peak memory usage: 93 MB
% 13.52/2.88 % (4183013)Instructions burned: 144 (million)
% 13.52/2.88 % SZS status CounterSatisfiable for theBenchmark
% 13.52/2.88 % SZS output start Saturation.
% See solution above
% 14.91/3.07 % SZS output start Definitions and Model Updates.
% 14.91/3.07 % SZS output end Definitions and Model Updates.
% 14.91/3.07 % (4182966)------------------------------
% 14.91/3.07 % (4182966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.91/3.07 % (4182966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.91/3.07 % (4182966)CaDiCaL version: 2.1.3
% 14.91/3.07 % (4182966)Termination reason: Satisfiable
% 14.91/3.07 % (4182966)Time elapsed: 1.593 s
% 14.91/3.07 % (4182966)Peak memory usage: 141 MB
% 14.91/3.07 % (4182966)Instructions burned: 2545 (million)
% 14.91/3.07 % (4182966)------------------------------
% 14.91/3.07 % (4182966)------------------------------
% 14.91/3.07 % (4182960)Success in time 2.031 s
% 14.91/3.07 % Vampire exiting
%------------------------------------------------------------------------------