%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL645+1.015 : 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 : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:53:48 AM UTC 2026
% Result : CounterSatisfiable 10.96s 2.47s
% Output : Saturation 11.77s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1451,negated_conjecture,
( ~ p2(sK441(X548))
| ~ p2(X548)
| ~ r1(sK220,X548)
| p1(sK440(X548)) ) ).
cnf(u1459,negated_conjecture,
( ~ p2(X548)
| ~ r1(sK220,X548)
| r1(X548,sK441(X548))
| p1(sK440(X548)) ) ).
cnf(u1464,negated_conjecture,
( ~ p2(sK441(X548))
| ~ p2(X548)
| ~ r1(sK220,X548)
| r1(X548,sK440(X548)) ) ).
cnf(u1469,negated_conjecture,
( ~ p2(X548)
| ~ r1(sK220,X548)
| r1(X548,sK441(X548))
| r1(X548,sK440(X548)) ) ).
cnf(u1477,negated_conjecture,
( ~ p2(sK439(X545))
| ~ p2(X545)
| ~ r1(sK220,X545)
| ~ p1(X545)
| p2(X546)
| ~ r1(X545,X546) ) ).
cnf(u1481,negated_conjecture,
( ~ p1(X545)
| ~ p2(X545)
| r1(X545,sK439(X545))
| ~ r1(sK220,X545)
| p2(X546)
| ~ r1(X545,X546) ) ).
cnf(u1485,negated_conjecture,
( ~ p2(X543)
| ~ p2(X544)
| ~ r1(X541,X544)
| ~ r1(sK220,X541)
| ~ r1(sK438(X541),X543)
| p3(X541) ) ).
cnf(u1492,negated_conjecture,
( ~ p2(X544)
| ~ r1(sK220,X541)
| ~ r1(X541,X544)
| r1(X541,sK438(X541))
| p3(X541) ) ).
cnf(u1514,negated_conjecture,
( ~ p3(sK435(X535))
| ~ p3(X535)
| ~ r1(sK220,X535)
| ~ p2(X535)
| p3(X536)
| ~ r1(X535,X536) ) ).
cnf(u1518,negated_conjecture,
( ~ p2(X535)
| ~ p3(X535)
| r1(X535,sK435(X535))
| ~ r1(sK220,X535)
| p3(X536)
| ~ r1(X535,X536) ) ).
cnf(u1522,negated_conjecture,
( ~ p3(X533)
| ~ p3(X534)
| ~ r1(X531,X534)
| ~ r1(sK220,X531)
| ~ r1(sK434(X531),X533)
| p4(X531) ) ).
cnf(u1529,negated_conjecture,
( ~ p3(X534)
| ~ r1(sK220,X531)
| ~ r1(X531,X534)
| r1(X531,sK434(X531))
| p4(X531) ) ).
cnf(u1551,negated_conjecture,
( ~ p4(sK431(X525))
| ~ p4(X525)
| ~ r1(sK220,X525)
| ~ p3(X525)
| p4(X526)
| ~ r1(X525,X526) ) ).
cnf(u1555,negated_conjecture,
( ~ p3(X525)
| ~ p4(X525)
| r1(X525,sK431(X525))
| ~ r1(sK220,X525)
| p4(X526)
| ~ r1(X525,X526) ) ).
cnf(u1559,negated_conjecture,
( ~ p4(X523)
| ~ p4(X524)
| ~ r1(X521,X524)
| ~ r1(sK220,X521)
| ~ r1(sK430(X521),X523)
| p5(X521) ) ).
cnf(u1566,negated_conjecture,
( ~ p4(X524)
| ~ r1(sK220,X521)
| ~ r1(X521,X524)
| r1(X521,sK430(X521))
| p5(X521) ) ).
cnf(u1588,negated_conjecture,
( ~ p5(sK427(X515))
| ~ p5(X515)
| ~ r1(sK220,X515)
| ~ p4(X515)
| p5(X516)
| ~ r1(X515,X516) ) ).
cnf(u1592,negated_conjecture,
( ~ p4(X515)
| ~ p5(X515)
| r1(X515,sK427(X515))
| ~ r1(sK220,X515)
| p5(X516)
| ~ r1(X515,X516) ) ).
cnf(u1596,negated_conjecture,
( ~ p5(X513)
| ~ p5(X514)
| ~ r1(X511,X514)
| ~ r1(sK220,X511)
| ~ r1(sK426(X511),X513)
| p6(X511) ) ).
cnf(u1603,negated_conjecture,
( ~ p5(X514)
| ~ r1(sK220,X511)
| ~ r1(X511,X514)
| r1(X511,sK426(X511))
| p6(X511) ) ).
cnf(u1625,negated_conjecture,
( ~ p6(sK423(X505))
| ~ p6(X505)
| ~ r1(sK220,X505)
| ~ p5(X505)
| p6(X506)
| ~ r1(X505,X506) ) ).
cnf(u1629,negated_conjecture,
( ~ p5(X505)
| ~ p6(X505)
| r1(X505,sK423(X505))
| ~ r1(sK220,X505)
| p6(X506)
| ~ r1(X505,X506) ) ).
cnf(u1633,negated_conjecture,
( ~ p6(X503)
| ~ p6(X504)
| ~ r1(X501,X504)
| ~ r1(sK220,X501)
| ~ r1(sK422(X501),X503)
| p7(X501) ) ).
cnf(u1640,negated_conjecture,
( ~ p6(X504)
| ~ r1(sK220,X501)
| ~ r1(X501,X504)
| r1(X501,sK422(X501))
| p7(X501) ) ).
cnf(u1662,negated_conjecture,
( ~ p7(sK419(X495))
| ~ p7(X495)
| ~ r1(sK220,X495)
| ~ p6(X495)
| p7(X496)
| ~ r1(X495,X496) ) ).
cnf(u1666,negated_conjecture,
( ~ p6(X495)
| ~ p7(X495)
| r1(X495,sK419(X495))
| ~ r1(sK220,X495)
| p7(X496)
| ~ r1(X495,X496) ) ).
cnf(u1670,negated_conjecture,
( ~ p7(X493)
| ~ p7(X494)
| ~ r1(X491,X494)
| ~ r1(sK220,X491)
| ~ r1(sK418(X491),X493)
| p8(X491) ) ).
cnf(u1677,negated_conjecture,
( ~ p7(X494)
| ~ r1(sK220,X491)
| ~ r1(X491,X494)
| r1(X491,sK418(X491))
| p8(X491) ) ).
cnf(u1699,negated_conjecture,
( ~ p8(sK415(X485))
| ~ p8(X485)
| ~ r1(sK220,X485)
| ~ p7(X485)
| p8(X486)
| ~ r1(X485,X486) ) ).
cnf(u1703,negated_conjecture,
( ~ p7(X485)
| ~ p8(X485)
| r1(X485,sK415(X485))
| ~ r1(sK220,X485)
| p8(X486)
| ~ r1(X485,X486) ) ).
cnf(u1707,negated_conjecture,
( ~ p8(X483)
| ~ p8(X484)
| ~ r1(X481,X484)
| ~ r1(sK220,X481)
| ~ r1(sK414(X481),X483)
| p9(X481) ) ).
cnf(u1714,negated_conjecture,
( ~ p8(X484)
| ~ r1(sK220,X481)
| ~ r1(X481,X484)
| r1(X481,sK414(X481))
| p9(X481) ) ).
cnf(u1736,negated_conjecture,
( ~ p9(sK411(X475))
| ~ p9(X475)
| ~ r1(sK220,X475)
| ~ p8(X475)
| p9(X476)
| ~ r1(X475,X476) ) ).
cnf(u1740,negated_conjecture,
( ~ p8(X475)
| ~ p9(X475)
| r1(X475,sK411(X475))
| ~ r1(sK220,X475)
| p9(X476)
| ~ r1(X475,X476) ) ).
cnf(u1744,negated_conjecture,
( ~ p9(X473)
| ~ p9(X474)
| ~ r1(X471,X474)
| ~ r1(sK220,X471)
| ~ r1(sK410(X471),X473)
| p10(X471) ) ).
cnf(u1751,negated_conjecture,
( ~ p9(X474)
| ~ r1(sK220,X471)
| ~ r1(X471,X474)
| r1(X471,sK410(X471))
| p10(X471) ) ).
cnf(u1773,negated_conjecture,
( ~ p10(sK407(X465))
| ~ p10(X465)
| ~ r1(sK220,X465)
| ~ p9(X465)
| p10(X466)
| ~ r1(X465,X466) ) ).
cnf(u1777,negated_conjecture,
( ~ p9(X465)
| ~ p10(X465)
| r1(X465,sK407(X465))
| ~ r1(sK220,X465)
| p10(X466)
| ~ r1(X465,X466) ) ).
cnf(u1781,negated_conjecture,
( ~ p10(X463)
| ~ p10(X464)
| ~ r1(X461,X464)
| ~ r1(sK220,X461)
| ~ r1(sK406(X461),X463)
| p11(X461) ) ).
cnf(u1788,negated_conjecture,
( ~ p10(X464)
| ~ r1(sK220,X461)
| ~ r1(X461,X464)
| r1(X461,sK406(X461))
| p11(X461) ) ).
cnf(u1810,negated_conjecture,
( ~ p11(sK403(X455))
| ~ p11(X455)
| ~ r1(sK220,X455)
| ~ p10(X455)
| p11(X456)
| ~ r1(X455,X456) ) ).
cnf(u1814,negated_conjecture,
( ~ p10(X455)
| ~ p11(X455)
| r1(X455,sK403(X455))
| ~ r1(sK220,X455)
| p11(X456)
| ~ r1(X455,X456) ) ).
cnf(u1818,negated_conjecture,
( ~ p11(X453)
| ~ p11(X454)
| ~ r1(X451,X454)
| ~ r1(sK220,X451)
| ~ r1(sK402(X451),X453)
| p12(X451) ) ).
cnf(u1825,negated_conjecture,
( ~ p11(X454)
| ~ r1(sK220,X451)
| ~ r1(X451,X454)
| r1(X451,sK402(X451))
| p12(X451) ) ).
cnf(u1847,negated_conjecture,
( ~ p12(sK399(X445))
| ~ p12(X445)
| ~ r1(sK220,X445)
| ~ p11(X445)
| p12(X446)
| ~ r1(X445,X446) ) ).
cnf(u1851,negated_conjecture,
( ~ p11(X445)
| ~ p12(X445)
| r1(X445,sK399(X445))
| ~ r1(sK220,X445)
| p12(X446)
| ~ r1(X445,X446) ) ).
cnf(u1855,negated_conjecture,
( ~ p12(X443)
| ~ p12(X444)
| ~ r1(X441,X444)
| ~ r1(sK220,X441)
| ~ r1(sK398(X441),X443)
| p13(X441) ) ).
cnf(u1862,negated_conjecture,
( ~ p12(X444)
| ~ r1(sK220,X441)
| ~ r1(X441,X444)
| r1(X441,sK398(X441))
| p13(X441) ) ).
cnf(u1884,negated_conjecture,
( ~ p13(sK395(X435))
| ~ p13(X435)
| ~ r1(sK220,X435)
| ~ p12(X435)
| p13(X436)
| ~ r1(X435,X436) ) ).
cnf(u1888,negated_conjecture,
( ~ p12(X435)
| ~ p13(X435)
| r1(X435,sK395(X435))
| ~ r1(sK220,X435)
| p13(X436)
| ~ r1(X435,X436) ) ).
cnf(u1892,negated_conjecture,
( ~ p13(X433)
| ~ p13(X434)
| ~ r1(X431,X434)
| ~ r1(sK220,X431)
| ~ r1(sK394(X431),X433)
| p14(X431) ) ).
cnf(u1899,negated_conjecture,
( ~ p13(X434)
| ~ r1(sK220,X431)
| ~ r1(X431,X434)
| r1(X431,sK394(X431))
| p14(X431) ) ).
cnf(u1921,negated_conjecture,
( ~ p14(sK391(X425))
| ~ p14(X425)
| ~ r1(sK220,X425)
| ~ p13(X425)
| p14(X426)
| ~ r1(X425,X426) ) ).
cnf(u1925,negated_conjecture,
( ~ p13(X425)
| ~ p14(X425)
| r1(X425,sK391(X425))
| ~ r1(sK220,X425)
| p14(X426)
| ~ r1(X425,X426) ) ).
cnf(u1929,negated_conjecture,
( ~ p14(X423)
| ~ p14(X424)
| ~ r1(X421,X424)
| ~ r1(sK220,X421)
| ~ r1(sK390(X421),X423)
| p15(X421) ) ).
cnf(u1936,negated_conjecture,
( ~ p14(X424)
| ~ r1(sK220,X421)
| ~ r1(X421,X424)
| r1(X421,sK390(X421))
| p15(X421) ) ).
cnf(u1958,negated_conjecture,
( ~ p15(sK387(X415))
| ~ p15(X415)
| ~ r1(sK220,X415)
| ~ p14(X415)
| p15(X416)
| ~ r1(X415,X416) ) ).
cnf(u1962,negated_conjecture,
( ~ p14(X415)
| ~ p15(X415)
| r1(X415,sK387(X415))
| ~ r1(sK220,X415)
| p15(X416)
| ~ r1(X415,X416) ) ).
cnf(u1966,negated_conjecture,
( ~ p15(X413)
| ~ p15(X414)
| ~ r1(X411,X414)
| ~ r1(sK220,X411)
| ~ r1(sK386(X411),X413)
| p16(X411) ) ).
cnf(u1973,negated_conjecture,
( ~ p15(X414)
| ~ r1(sK220,X411)
| ~ r1(X411,X414)
| r1(X411,sK386(X411))
| p16(X411) ) ).
cnf(u1995,negated_conjecture,
( ~ p16(sK383(X405))
| ~ p16(X405)
| ~ r1(sK220,X405)
| ~ p15(X405)
| p16(X406)
| ~ r1(X405,X406) ) ).
cnf(u1999,negated_conjecture,
( ~ p16(X405)
| ~ r1(sK220,X405)
| r1(X405,sK383(X405))
| ~ p15(X405)
| p16(X406)
| ~ r1(X405,X406) ) ).
cnf(u2003,negated_conjecture,
( ~ p16(X403)
| ~ p16(X404)
| ~ r1(X401,X404)
| ~ r1(sK220,X401)
| ~ r1(sK382(X401),X403)
| p17(X401) ) ).
cnf(u2010,negated_conjecture,
( ~ p16(X404)
| ~ r1(sK220,X401)
| ~ r1(X401,X404)
| r1(X401,sK382(X401))
| p17(X401) ) ).
cnf(u2032,negated_conjecture,
( ~ p17(sK379(X395))
| ~ p17(X395)
| ~ r1(sK220,X395)
| ~ p16(X395)
| p17(X396)
| ~ r1(X395,X396) ) ).
cnf(u2036,negated_conjecture,
( ~ p16(X395)
| ~ p17(X395)
| r1(X395,sK379(X395))
| ~ r1(sK220,X395)
| p17(X396)
| ~ r1(X395,X396) ) ).
cnf(u2040,negated_conjecture,
( ~ p17(X393)
| ~ p17(X394)
| ~ r1(X391,X394)
| ~ r1(sK220,X391)
| ~ r1(sK378(X391),X393)
| p18(X391) ) ).
cnf(u2047,negated_conjecture,
( ~ p17(X394)
| ~ r1(sK220,X391)
| ~ r1(X391,X394)
| r1(X391,sK378(X391))
| p18(X391) ) ).
cnf(u2069,negated_conjecture,
( ~ p18(sK375(X385))
| ~ p18(X385)
| ~ r1(sK220,X385)
| ~ p17(X385)
| p18(X386)
| ~ r1(X385,X386) ) ).
cnf(u2073,negated_conjecture,
( ~ p17(X385)
| ~ p18(X385)
| r1(X385,sK375(X385))
| ~ r1(sK220,X385)
| p18(X386)
| ~ r1(X385,X386) ) ).
cnf(u2077,negated_conjecture,
( ~ p18(X383)
| ~ p18(X384)
| ~ r1(X381,X384)
| ~ r1(sK220,X381)
| ~ r1(sK374(X381),X383)
| p19(X381) ) ).
cnf(u2084,negated_conjecture,
( ~ p18(X384)
| ~ r1(sK220,X381)
| ~ r1(X381,X384)
| r1(X381,sK374(X381))
| p19(X381) ) ).
cnf(u2106,negated_conjecture,
( ~ p19(sK371(X375))
| ~ p19(X375)
| ~ r1(sK220,X375)
| ~ p18(X375)
| p19(X376)
| ~ r1(X375,X376) ) ).
cnf(u2110,negated_conjecture,
( ~ p18(X375)
| ~ p19(X375)
| r1(X375,sK371(X375))
| ~ r1(sK220,X375)
| p19(X376)
| ~ r1(X375,X376) ) ).
cnf(u2114,negated_conjecture,
( ~ p19(X373)
| ~ p19(X374)
| ~ r1(X371,X374)
| ~ r1(sK220,X371)
| ~ r1(sK370(X371),X373)
| p20(X371) ) ).
cnf(u2121,negated_conjecture,
( ~ p19(X374)
| ~ r1(sK220,X371)
| ~ r1(X371,X374)
| r1(X371,sK370(X371))
| p20(X371) ) ).
cnf(u2143,negated_conjecture,
( ~ p20(sK367(X365))
| ~ p20(X365)
| ~ r1(sK220,X365)
| ~ p19(X365)
| p20(X366)
| ~ r1(X365,X366) ) ).
cnf(u2147,negated_conjecture,
( ~ p19(X365)
| ~ p20(X365)
| r1(X365,sK367(X365))
| ~ r1(sK220,X365)
| p20(X366)
| ~ r1(X365,X366) ) ).
cnf(u2151,negated_conjecture,
( ~ p20(X363)
| ~ p20(X364)
| ~ r1(X361,X364)
| ~ r1(sK220,X361)
| ~ r1(sK366(X361),X363)
| p21(X361) ) ).
cnf(u2158,negated_conjecture,
( ~ p20(X364)
| ~ r1(sK220,X361)
| ~ r1(X361,X364)
| r1(X361,sK366(X361))
| p21(X361) ) ).
cnf(u2180,negated_conjecture,
( ~ p21(sK363(X355))
| ~ p21(X355)
| ~ r1(sK220,X355)
| ~ p20(X355)
| p21(X356)
| ~ r1(X355,X356) ) ).
cnf(u2184,negated_conjecture,
( ~ p20(X355)
| ~ p21(X355)
| r1(X355,sK363(X355))
| ~ r1(sK220,X355)
| p21(X356)
| ~ r1(X355,X356) ) ).
cnf(u2188,negated_conjecture,
( ~ p21(X353)
| ~ p21(X354)
| ~ r1(X351,X354)
| ~ r1(sK220,X351)
| ~ r1(sK362(X351),X353)
| p22(X351) ) ).
cnf(u2195,negated_conjecture,
( ~ p21(X354)
| ~ r1(sK220,X351)
| ~ r1(X351,X354)
| r1(X351,sK362(X351))
| p22(X351) ) ).
cnf(u2217,negated_conjecture,
( ~ p22(sK359(X345))
| ~ p22(X345)
| ~ r1(sK220,X345)
| ~ p21(X345)
| p22(X346)
| ~ r1(X345,X346) ) ).
cnf(u2221,negated_conjecture,
( ~ p21(X345)
| ~ p22(X345)
| r1(X345,sK359(X345))
| ~ r1(sK220,X345)
| p22(X346)
| ~ r1(X345,X346) ) ).
cnf(u2225,negated_conjecture,
( ~ p22(X343)
| ~ p22(X344)
| ~ r1(X341,X344)
| ~ r1(sK220,X341)
| ~ r1(sK358(X341),X343)
| p23(X341) ) ).
cnf(u2232,negated_conjecture,
( ~ p22(X344)
| ~ r1(sK220,X341)
| ~ r1(X341,X344)
| r1(X341,sK358(X341))
| p23(X341) ) ).
cnf(u2254,negated_conjecture,
( ~ p23(sK355(X335))
| ~ p23(X335)
| ~ r1(sK220,X335)
| ~ p22(X335)
| p23(X336)
| ~ r1(X335,X336) ) ).
cnf(u2258,negated_conjecture,
( ~ p22(X335)
| ~ p23(X335)
| r1(X335,sK355(X335))
| ~ r1(sK220,X335)
| p23(X336)
| ~ r1(X335,X336) ) ).
cnf(u2262,negated_conjecture,
( ~ p23(X333)
| ~ p23(X334)
| ~ r1(X331,X334)
| ~ r1(sK220,X331)
| ~ r1(sK354(X331),X333)
| p24(X331) ) ).
cnf(u2269,negated_conjecture,
( ~ p23(X334)
| ~ r1(sK220,X331)
| ~ r1(X331,X334)
| r1(X331,sK354(X331))
| p24(X331) ) ).
cnf(u2291,negated_conjecture,
( ~ p24(sK351(X325))
| ~ p24(X325)
| ~ r1(sK220,X325)
| ~ p23(X325)
| p24(X326)
| ~ r1(X325,X326) ) ).
cnf(u2295,negated_conjecture,
( ~ p23(X325)
| ~ p24(X325)
| r1(X325,sK351(X325))
| ~ r1(sK220,X325)
| p24(X326)
| ~ r1(X325,X326) ) ).
cnf(u2299,negated_conjecture,
( ~ p24(X323)
| ~ p24(X324)
| ~ r1(X321,X324)
| ~ r1(sK220,X321)
| ~ r1(sK350(X321),X323)
| p25(X321) ) ).
cnf(u2306,negated_conjecture,
( ~ p24(X324)
| ~ r1(sK220,X321)
| ~ r1(X321,X324)
| r1(X321,sK350(X321))
| p25(X321) ) ).
cnf(u2328,negated_conjecture,
( ~ p25(sK347(X315))
| ~ p25(X315)
| ~ r1(sK220,X315)
| ~ p24(X315)
| p25(X316)
| ~ r1(X315,X316) ) ).
cnf(u2332,negated_conjecture,
( ~ p24(X315)
| ~ p25(X315)
| r1(X315,sK347(X315))
| ~ r1(sK220,X315)
| p25(X316)
| ~ r1(X315,X316) ) ).
cnf(u2336,negated_conjecture,
( ~ p25(X313)
| ~ p25(X314)
| ~ r1(X311,X314)
| ~ r1(sK220,X311)
| ~ r1(sK346(X311),X313)
| p26(X311) ) ).
cnf(u2343,negated_conjecture,
( ~ p25(X314)
| ~ r1(sK220,X311)
| ~ r1(X311,X314)
| r1(X311,sK346(X311))
| p26(X311) ) ).
cnf(u2365,negated_conjecture,
( ~ p26(sK343(X305))
| ~ p26(X305)
| ~ r1(sK220,X305)
| ~ p25(X305)
| p26(X306)
| ~ r1(X305,X306) ) ).
cnf(u2369,negated_conjecture,
( ~ p25(X305)
| ~ p26(X305)
| r1(X305,sK343(X305))
| ~ r1(sK220,X305)
| p26(X306)
| ~ r1(X305,X306) ) ).
cnf(u2373,negated_conjecture,
( ~ p26(X303)
| ~ p26(X304)
| ~ r1(X301,X304)
| ~ r1(sK220,X301)
| ~ r1(sK342(X301),X303)
| p27(X301) ) ).
cnf(u2380,negated_conjecture,
( ~ p26(X304)
| ~ r1(sK220,X301)
| ~ r1(X301,X304)
| r1(X301,sK342(X301))
| p27(X301) ) ).
cnf(u2402,negated_conjecture,
( ~ p27(sK339(X295))
| ~ p27(X295)
| ~ r1(sK220,X295)
| ~ p26(X295)
| p27(X296)
| ~ r1(X295,X296) ) ).
cnf(u2406,negated_conjecture,
( ~ p26(X295)
| ~ p27(X295)
| r1(X295,sK339(X295))
| ~ r1(sK220,X295)
| p27(X296)
| ~ r1(X295,X296) ) ).
cnf(u2410,negated_conjecture,
( ~ p27(X293)
| ~ p27(X294)
| ~ r1(X291,X294)
| ~ r1(sK220,X291)
| ~ r1(sK338(X291),X293)
| p28(X291) ) ).
cnf(u2417,negated_conjecture,
( ~ p27(X294)
| ~ r1(sK220,X291)
| ~ r1(X291,X294)
| r1(X291,sK338(X291))
| p28(X291) ) ).
cnf(u2439,negated_conjecture,
( ~ p28(sK335(X285))
| ~ p28(X285)
| ~ r1(sK220,X285)
| ~ p27(X285)
| p28(X286)
| ~ r1(X285,X286) ) ).
cnf(u2443,negated_conjecture,
( ~ p27(X285)
| ~ p28(X285)
| r1(X285,sK335(X285))
| ~ r1(sK220,X285)
| p28(X286)
| ~ r1(X285,X286) ) ).
cnf(u2447,negated_conjecture,
( ~ p28(X283)
| ~ p28(X284)
| ~ r1(X281,X284)
| ~ r1(sK220,X281)
| ~ r1(sK334(X281),X283)
| p29(X281) ) ).
cnf(u2454,negated_conjecture,
( ~ p28(X284)
| ~ r1(sK220,X281)
| ~ r1(X281,X284)
| r1(X281,sK334(X281))
| p29(X281) ) ).
cnf(u2476,negated_conjecture,
( ~ p29(sK331(X275))
| ~ p29(X275)
| ~ r1(sK220,X275)
| ~ p28(X275)
| p29(X276)
| ~ r1(X275,X276) ) ).
cnf(u2480,negated_conjecture,
( ~ p28(X275)
| ~ p29(X275)
| r1(X275,sK331(X275))
| ~ r1(sK220,X275)
| p29(X276)
| ~ r1(X275,X276) ) ).
cnf(u2484,negated_conjecture,
( ~ p30(X269)
| ~ p30(X270)
| ~ r1(X267,X270)
| ~ r1(sK220,X267)
| ~ r1(sK328(X267),X269)
| p31(X267) ) ).
cnf(u2491,negated_conjecture,
( ~ p30(X270)
| ~ r1(sK220,X267)
| ~ r1(X267,X270)
| r1(X267,sK328(X267))
| p31(X267) ) ).
cnf(u2513,negated_conjecture,
( ~ p31(sK325(X261))
| ~ p31(X261)
| ~ r1(sK220,X261)
| ~ p30(X261)
| p31(X262)
| ~ r1(X261,X262) ) ).
cnf(u2517,negated_conjecture,
( ~ p30(X261)
| ~ p31(X261)
| r1(X261,sK325(X261))
| ~ r1(sK220,X261)
| p31(X262)
| ~ r1(X261,X262) ) ).
cnf(u2521,negated_conjecture,
( ~ p31(X259)
| ~ p31(X260)
| ~ r1(X257,X260)
| ~ r1(sK220,X257)
| ~ r1(sK324(X257),X259)
| p32(X257) ) ).
cnf(u2528,negated_conjecture,
( ~ p31(X260)
| ~ r1(sK220,X257)
| ~ r1(X257,X260)
| r1(X257,sK324(X257))
| p32(X257) ) ).
cnf(u2550,negated_conjecture,
( ~ p32(sK321(X251))
| ~ p32(X251)
| ~ r1(sK220,X251)
| ~ p31(X251)
| p32(X252)
| ~ r1(X251,X252) ) ).
cnf(u2554,negated_conjecture,
( ~ p31(X251)
| ~ p32(X251)
| r1(X251,sK321(X251))
| ~ r1(sK220,X251)
| p32(X252)
| ~ r1(X251,X252) ) ).
cnf(u2558,negated_conjecture,
( ~ p32(X249)
| ~ p32(X250)
| ~ r1(X247,X250)
| ~ r1(sK220,X247)
| ~ r1(sK320(X247),X249)
| p33(X247) ) ).
cnf(u2565,negated_conjecture,
( ~ p32(X250)
| ~ r1(sK220,X247)
| ~ r1(X247,X250)
| r1(X247,sK320(X247))
| p33(X247) ) ).
cnf(u2587,negated_conjecture,
( ~ p33(sK317(X241))
| ~ p33(X241)
| ~ r1(sK220,X241)
| ~ p32(X241)
| p33(X242)
| ~ r1(X241,X242) ) ).
cnf(u2591,negated_conjecture,
( ~ p32(X241)
| ~ p33(X241)
| r1(X241,sK317(X241))
| ~ r1(sK220,X241)
| p33(X242)
| ~ r1(X241,X242) ) ).
cnf(u2595,negated_conjecture,
( ~ p33(X239)
| ~ p33(X240)
| ~ r1(X237,X240)
| ~ r1(sK220,X237)
| ~ r1(sK316(X237),X239)
| p34(X237) ) ).
cnf(u2602,negated_conjecture,
( ~ p33(X240)
| ~ r1(sK220,X237)
| ~ r1(X237,X240)
| r1(X237,sK316(X237))
| p34(X237) ) ).
cnf(u2624,negated_conjecture,
( ~ p34(sK313(X231))
| ~ p34(X231)
| ~ r1(sK220,X231)
| ~ p33(X231)
| p34(X232)
| ~ r1(X231,X232) ) ).
cnf(u2628,negated_conjecture,
( ~ p33(X231)
| ~ p34(X231)
| r1(X231,sK313(X231))
| ~ r1(sK220,X231)
| p34(X232)
| ~ r1(X231,X232) ) ).
cnf(u2632,negated_conjecture,
( ~ p34(X229)
| ~ p34(X230)
| ~ r1(X227,X230)
| ~ r1(sK220,X227)
| ~ r1(sK312(X227),X229)
| p35(X227) ) ).
cnf(u2639,negated_conjecture,
( ~ p34(X230)
| ~ r1(sK220,X227)
| ~ r1(X227,X230)
| r1(X227,sK312(X227))
| p35(X227) ) ).
cnf(u2661,negated_conjecture,
( ~ p35(sK309(X221))
| ~ p35(X221)
| ~ r1(sK220,X221)
| ~ p34(X221)
| p35(X222)
| ~ r1(X221,X222) ) ).
cnf(u2665,negated_conjecture,
( ~ p34(X221)
| ~ p35(X221)
| r1(X221,sK309(X221))
| ~ r1(sK220,X221)
| p35(X222)
| ~ r1(X221,X222) ) ).
cnf(u2669,negated_conjecture,
( ~ p35(X219)
| ~ p35(X220)
| ~ r1(X217,X220)
| ~ r1(sK220,X217)
| ~ r1(sK308(X217),X219)
| p36(X217) ) ).
cnf(u2676,negated_conjecture,
( ~ p35(X220)
| ~ r1(sK220,X217)
| ~ r1(X217,X220)
| r1(X217,sK308(X217))
| p36(X217) ) ).
cnf(u2698,negated_conjecture,
( ~ p36(sK305(X211))
| ~ p36(X211)
| ~ r1(sK220,X211)
| ~ p35(X211)
| p36(X212)
| ~ r1(X211,X212) ) ).
cnf(u2702,negated_conjecture,
( ~ p35(X211)
| ~ p36(X211)
| r1(X211,sK305(X211))
| ~ r1(sK220,X211)
| p36(X212)
| ~ r1(X211,X212) ) ).
cnf(u2706,negated_conjecture,
( ~ p36(X209)
| ~ p36(X210)
| ~ r1(X207,X210)
| ~ r1(sK220,X207)
| ~ r1(sK304(X207),X209)
| p37(X207) ) ).
cnf(u2713,negated_conjecture,
( ~ p36(X210)
| ~ r1(sK220,X207)
| ~ r1(X207,X210)
| r1(X207,sK304(X207))
| p37(X207) ) ).
cnf(u2735,negated_conjecture,
( ~ p37(sK301(X201))
| ~ p37(X201)
| ~ r1(sK220,X201)
| ~ p36(X201)
| p37(X202)
| ~ r1(X201,X202) ) ).
cnf(u2739,negated_conjecture,
( ~ p36(X201)
| ~ p37(X201)
| r1(X201,sK301(X201))
| ~ r1(sK220,X201)
| p37(X202)
| ~ r1(X201,X202) ) ).
cnf(u2743,negated_conjecture,
( ~ p37(X199)
| ~ p37(X200)
| ~ r1(X197,X200)
| ~ r1(sK220,X197)
| ~ r1(sK300(X197),X199)
| p38(X197) ) ).
cnf(u2750,negated_conjecture,
( ~ p37(X200)
| ~ r1(sK220,X197)
| ~ r1(X197,X200)
| r1(X197,sK300(X197))
| p38(X197) ) ).
cnf(u2772,negated_conjecture,
( ~ p38(sK297(X191))
| ~ p38(X191)
| ~ r1(sK220,X191)
| ~ p37(X191)
| p38(X192)
| ~ r1(X191,X192) ) ).
cnf(u2776,negated_conjecture,
( ~ p37(X191)
| ~ p38(X191)
| r1(X191,sK297(X191))
| ~ r1(sK220,X191)
| p38(X192)
| ~ r1(X191,X192) ) ).
cnf(u2780,negated_conjecture,
( ~ p38(X189)
| ~ p38(X190)
| ~ r1(X187,X190)
| ~ r1(sK220,X187)
| ~ r1(sK296(X187),X189)
| p39(X187) ) ).
cnf(u2787,negated_conjecture,
( ~ p38(X190)
| ~ r1(sK220,X187)
| ~ r1(X187,X190)
| r1(X187,sK296(X187))
| p39(X187) ) ).
cnf(u2809,negated_conjecture,
( ~ p39(sK293(X181))
| ~ p39(X181)
| ~ r1(sK220,X181)
| ~ p38(X181)
| p39(X182)
| ~ r1(X181,X182) ) ).
cnf(u2813,negated_conjecture,
( ~ p38(X181)
| ~ p39(X181)
| r1(X181,sK293(X181))
| ~ r1(sK220,X181)
| p39(X182)
| ~ r1(X181,X182) ) ).
cnf(u2817,negated_conjecture,
( ~ p39(X179)
| ~ p39(X180)
| ~ r1(X177,X180)
| ~ r1(sK220,X177)
| ~ r1(sK292(X177),X179)
| p40(X177) ) ).
cnf(u2824,negated_conjecture,
( ~ p39(X180)
| ~ r1(sK220,X177)
| ~ r1(X177,X180)
| r1(X177,sK292(X177))
| p40(X177) ) ).
cnf(u2846,negated_conjecture,
( ~ p40(sK289(X171))
| ~ p40(X171)
| ~ r1(sK220,X171)
| ~ p39(X171)
| p40(X172)
| ~ r1(X171,X172) ) ).
cnf(u2850,negated_conjecture,
( ~ p39(X171)
| ~ p40(X171)
| r1(X171,sK289(X171))
| ~ r1(sK220,X171)
| p40(X172)
| ~ r1(X171,X172) ) ).
cnf(u2854,negated_conjecture,
( ~ p40(X169)
| ~ p40(X170)
| ~ r1(X167,X170)
| ~ r1(sK220,X167)
| ~ r1(sK288(X167),X169)
| p41(X167) ) ).
cnf(u2861,negated_conjecture,
( ~ p40(X170)
| ~ r1(sK220,X167)
| ~ r1(X167,X170)
| r1(X167,sK288(X167))
| p41(X167) ) ).
cnf(u2883,negated_conjecture,
( ~ p41(sK285(X161))
| ~ p41(X161)
| ~ r1(sK220,X161)
| ~ p40(X161)
| p41(X162)
| ~ r1(X161,X162) ) ).
cnf(u2887,negated_conjecture,
( ~ p40(X161)
| ~ p41(X161)
| r1(X161,sK285(X161))
| ~ r1(sK220,X161)
| p41(X162)
| ~ r1(X161,X162) ) ).
cnf(u2891,negated_conjecture,
( ~ p41(X159)
| ~ p41(X160)
| ~ r1(X157,X160)
| ~ r1(sK220,X157)
| ~ r1(sK284(X157),X159)
| p42(X157) ) ).
cnf(u2898,negated_conjecture,
( ~ p41(X160)
| ~ r1(sK220,X157)
| ~ r1(X157,X160)
| r1(X157,sK284(X157))
| p42(X157) ) ).
cnf(u2920,negated_conjecture,
( ~ p42(sK281(X151))
| ~ p42(X151)
| ~ r1(sK220,X151)
| ~ p41(X151)
| p42(X152)
| ~ r1(X151,X152) ) ).
cnf(u2924,negated_conjecture,
( ~ p41(X151)
| ~ p42(X151)
| r1(X151,sK281(X151))
| ~ r1(sK220,X151)
| p42(X152)
| ~ r1(X151,X152) ) ).
cnf(u2928,negated_conjecture,
( ~ p42(X149)
| ~ p42(X150)
| ~ r1(X147,X150)
| ~ r1(sK220,X147)
| ~ r1(sK280(X147),X149)
| p43(X147) ) ).
cnf(u2935,negated_conjecture,
( ~ p42(X150)
| ~ r1(sK220,X147)
| ~ r1(X147,X150)
| r1(X147,sK280(X147))
| p43(X147) ) ).
cnf(u2957,negated_conjecture,
( ~ p43(sK277(X141))
| ~ p43(X141)
| ~ r1(sK220,X141)
| ~ p42(X141)
| p43(X142)
| ~ r1(X141,X142) ) ).
cnf(u2961,negated_conjecture,
( ~ p42(X141)
| ~ p43(X141)
| r1(X141,sK277(X141))
| ~ r1(sK220,X141)
| p43(X142)
| ~ r1(X141,X142) ) ).
cnf(u2965,negated_conjecture,
( ~ p43(X139)
| ~ p43(X140)
| ~ r1(X137,X140)
| ~ r1(sK220,X137)
| ~ r1(sK276(X137),X139)
| p44(X137) ) ).
cnf(u2972,negated_conjecture,
( ~ p43(X140)
| ~ r1(sK220,X137)
| ~ r1(X137,X140)
| r1(X137,sK276(X137))
| p44(X137) ) ).
cnf(u2994,negated_conjecture,
( ~ p44(sK273(X131))
| ~ p44(X131)
| ~ r1(sK220,X131)
| ~ p43(X131)
| p44(X132)
| ~ r1(X131,X132) ) ).
cnf(u2998,negated_conjecture,
( ~ p43(X131)
| ~ p44(X131)
| r1(X131,sK273(X131))
| ~ r1(sK220,X131)
| p44(X132)
| ~ r1(X131,X132) ) ).
cnf(u3002,negated_conjecture,
( ~ p44(X129)
| ~ p44(X130)
| ~ r1(X127,X130)
| ~ r1(sK220,X127)
| ~ r1(sK272(X127),X129)
| p45(X127) ) ).
cnf(u3009,negated_conjecture,
( ~ p44(X130)
| ~ r1(sK220,X127)
| ~ r1(X127,X130)
| r1(X127,sK272(X127))
| p45(X127) ) ).
cnf(u3031,negated_conjecture,
( ~ p45(sK269(X121))
| ~ p45(X121)
| ~ r1(sK220,X121)
| ~ p44(X121)
| p45(X122)
| ~ r1(X121,X122) ) ).
cnf(u3035,negated_conjecture,
( ~ p44(X121)
| ~ p45(X121)
| r1(X121,sK269(X121))
| ~ r1(sK220,X121)
| p45(X122)
| ~ r1(X121,X122) ) ).
cnf(u3039,negated_conjecture,
( ~ p45(X119)
| ~ p45(X120)
| ~ r1(X117,X120)
| ~ r1(sK220,X117)
| ~ r1(sK268(X117),X119)
| p46(X117) ) ).
cnf(u3046,negated_conjecture,
( ~ p45(X120)
| ~ r1(sK220,X117)
| ~ r1(X117,X120)
| r1(X117,sK268(X117))
| p46(X117) ) ).
cnf(u3068,negated_conjecture,
( ~ p46(sK265(X111))
| ~ p46(X111)
| ~ r1(sK220,X111)
| ~ p45(X111)
| p46(X112)
| ~ r1(X111,X112) ) ).
cnf(u3072,negated_conjecture,
( ~ p45(X111)
| ~ p46(X111)
| r1(X111,sK265(X111))
| ~ r1(sK220,X111)
| p46(X112)
| ~ r1(X111,X112) ) ).
cnf(u3076,negated_conjecture,
( ~ p46(X109)
| ~ p46(X110)
| ~ r1(X107,X110)
| ~ r1(sK220,X107)
| ~ r1(sK264(X107),X109)
| p47(X107) ) ).
cnf(u3083,negated_conjecture,
( ~ p46(X110)
| ~ r1(sK220,X107)
| ~ r1(X107,X110)
| r1(X107,sK264(X107))
| p47(X107) ) ).
cnf(u3105,negated_conjecture,
( ~ p47(sK261(X101))
| ~ p47(X101)
| ~ r1(sK220,X101)
| ~ p46(X101)
| p47(X102)
| ~ r1(X101,X102) ) ).
cnf(u3109,negated_conjecture,
( ~ p46(X101)
| ~ p47(X101)
| r1(X101,sK261(X101))
| ~ r1(sK220,X101)
| p47(X102)
| ~ r1(X101,X102) ) ).
cnf(u3113,negated_conjecture,
( ~ p47(X99)
| ~ p47(X100)
| ~ r1(X97,X100)
| ~ r1(sK220,X97)
| ~ r1(sK260(X97),X99)
| p48(X97) ) ).
cnf(u3120,negated_conjecture,
( ~ p47(X100)
| ~ r1(sK220,X97)
| ~ r1(X97,X100)
| r1(X97,sK260(X97))
| p48(X97) ) ).
cnf(u3142,negated_conjecture,
( ~ p48(sK257(X91))
| ~ p48(X91)
| ~ r1(sK220,X91)
| ~ p47(X91)
| p48(X92)
| ~ r1(X91,X92) ) ).
cnf(u3146,negated_conjecture,
( ~ p47(X91)
| ~ p48(X91)
| r1(X91,sK257(X91))
| ~ r1(sK220,X91)
| p48(X92)
| ~ r1(X91,X92) ) ).
cnf(u3150,negated_conjecture,
( ~ p48(X89)
| ~ p48(X90)
| ~ r1(X87,X90)
| ~ r1(sK220,X87)
| ~ r1(sK256(X87),X89)
| p49(X87) ) ).
cnf(u3157,negated_conjecture,
( ~ p48(X90)
| ~ r1(sK220,X87)
| ~ r1(X87,X90)
| r1(X87,sK256(X87))
| p49(X87) ) ).
cnf(u3179,negated_conjecture,
( ~ p49(sK253(X81))
| ~ p49(X81)
| ~ r1(sK220,X81)
| ~ p48(X81)
| p49(X82)
| ~ r1(X81,X82) ) ).
cnf(u3183,negated_conjecture,
( ~ p48(X81)
| ~ p49(X81)
| r1(X81,sK253(X81))
| ~ r1(sK220,X81)
| p49(X82)
| ~ r1(X81,X82) ) ).
cnf(u3187,negated_conjecture,
( ~ p49(X79)
| ~ p49(X80)
| ~ r1(X77,X80)
| ~ r1(sK220,X77)
| ~ r1(sK252(X77),X79)
| p50(X77) ) ).
cnf(u3194,negated_conjecture,
( ~ p49(X80)
| ~ r1(sK220,X77)
| ~ r1(X77,X80)
| r1(X77,sK252(X77))
| p50(X77) ) ).
cnf(u3216,negated_conjecture,
( ~ p50(sK249(X71))
| ~ p50(X71)
| ~ r1(sK220,X71)
| ~ p49(X71)
| p50(X72)
| ~ r1(X71,X72) ) ).
cnf(u3220,negated_conjecture,
( ~ p49(X71)
| ~ p50(X71)
| r1(X71,sK249(X71))
| ~ r1(sK220,X71)
| p50(X72)
| ~ r1(X71,X72) ) ).
cnf(u3224,negated_conjecture,
( ~ p50(X69)
| ~ p50(X70)
| ~ r1(X67,X70)
| ~ r1(sK220,X67)
| ~ r1(sK248(X67),X69)
| p51(X67) ) ).
cnf(u3231,negated_conjecture,
( ~ p50(X70)
| ~ r1(sK220,X67)
| ~ r1(X67,X70)
| r1(X67,sK248(X67))
| p51(X67) ) ).
cnf(u3253,negated_conjecture,
( ~ p51(sK245(X61))
| ~ p51(X61)
| ~ r1(sK220,X61)
| ~ p50(X61)
| p51(X62)
| ~ r1(X61,X62) ) ).
cnf(u3257,negated_conjecture,
( ~ p50(X61)
| ~ p51(X61)
| r1(X61,sK245(X61))
| ~ r1(sK220,X61)
| p51(X62)
| ~ r1(X61,X62) ) ).
cnf(u3261,negated_conjecture,
( ~ p51(X59)
| ~ p51(X60)
| ~ r1(X57,X60)
| ~ r1(sK220,X57)
| ~ r1(sK244(X57),X59)
| p52(X57) ) ).
cnf(u3268,negated_conjecture,
( ~ p51(X60)
| ~ r1(sK220,X57)
| ~ r1(X57,X60)
| r1(X57,sK244(X57))
| p52(X57) ) ).
cnf(u3290,negated_conjecture,
( ~ p52(sK241(X51))
| ~ p52(X51)
| ~ r1(sK220,X51)
| ~ p51(X51)
| p52(X52)
| ~ r1(X51,X52) ) ).
cnf(u3294,negated_conjecture,
( ~ p51(X51)
| ~ p52(X51)
| r1(X51,sK241(X51))
| ~ r1(sK220,X51)
| p52(X52)
| ~ r1(X51,X52) ) ).
cnf(u3298,negated_conjecture,
( ~ p52(X49)
| ~ p52(X50)
| ~ r1(X47,X50)
| ~ r1(sK220,X47)
| ~ r1(sK240(X47),X49)
| p53(X47) ) ).
cnf(u3305,negated_conjecture,
( ~ p52(X50)
| ~ r1(sK220,X47)
| ~ r1(X47,X50)
| r1(X47,sK240(X47))
| p53(X47) ) ).
cnf(u3327,negated_conjecture,
( ~ p53(sK237(X41))
| ~ p53(X41)
| ~ r1(sK220,X41)
| ~ p52(X41)
| p53(X42)
| ~ r1(X41,X42) ) ).
cnf(u3331,negated_conjecture,
( ~ p52(X41)
| ~ p53(X41)
| r1(X41,sK237(X41))
| ~ r1(sK220,X41)
| p53(X42)
| ~ r1(X41,X42) ) ).
cnf(u3335,negated_conjecture,
( ~ p53(X39)
| ~ p53(X40)
| ~ r1(X37,X40)
| ~ r1(sK220,X37)
| ~ r1(sK236(X37),X39)
| p54(X37) ) ).
cnf(u3342,negated_conjecture,
( ~ p53(X40)
| ~ r1(sK220,X37)
| ~ r1(X37,X40)
| r1(X37,sK236(X37))
| p54(X37) ) ).
cnf(u3364,negated_conjecture,
( ~ p54(sK233(X31))
| ~ p54(X31)
| ~ r1(sK220,X31)
| ~ p53(X31)
| p54(X32)
| ~ r1(X31,X32) ) ).
cnf(u3368,negated_conjecture,
( ~ p53(X31)
| ~ p54(X31)
| r1(X31,sK233(X31))
| ~ r1(sK220,X31)
| p54(X32)
| ~ r1(X31,X32) ) ).
cnf(u3372,negated_conjecture,
( ~ p54(X29)
| ~ p54(X30)
| ~ r1(X27,X30)
| ~ r1(sK220,X27)
| ~ r1(sK232(X27),X29)
| p55(X27) ) ).
cnf(u3379,negated_conjecture,
( ~ p54(X30)
| ~ r1(sK220,X27)
| ~ r1(X27,X30)
| r1(X27,sK232(X27))
| p55(X27) ) ).
cnf(u3401,negated_conjecture,
( ~ p55(sK229(X21))
| ~ p55(X21)
| ~ r1(sK220,X21)
| ~ p54(X21)
| p55(X22)
| ~ r1(X21,X22) ) ).
cnf(u3405,negated_conjecture,
( ~ p54(X21)
| ~ p55(X21)
| r1(X21,sK229(X21))
| ~ r1(sK220,X21)
| p55(X22)
| ~ r1(X21,X22) ) ).
cnf(u3409,negated_conjecture,
( ~ p55(X19)
| ~ p55(X20)
| ~ r1(X17,X20)
| ~ r1(sK220,X17)
| ~ r1(sK228(X17),X19)
| p56(X17) ) ).
cnf(u3416,negated_conjecture,
( ~ p55(X20)
| ~ r1(sK220,X17)
| ~ r1(X17,X20)
| r1(X17,sK228(X17))
| p56(X17) ) ).
cnf(u3438,negated_conjecture,
( ~ p56(sK225(X11))
| ~ p56(X11)
| ~ r1(sK220,X11)
| ~ p55(X11)
| p56(X12)
| ~ r1(X11,X12) ) ).
cnf(u3442,negated_conjecture,
( ~ p55(X11)
| ~ p56(X11)
| r1(X11,sK225(X11))
| ~ r1(sK220,X11)
| p56(X12)
| ~ r1(X11,X12) ) ).
cnf(u3446,negated_conjecture,
( ~ p56(X9)
| ~ p56(X10)
| ~ r1(X7,X10)
| ~ r1(sK220,X7)
| ~ r1(sK224(X7),X9)
| p57(X7) ) ).
cnf(u3453,negated_conjecture,
( ~ p56(X10)
| ~ r1(sK220,X7)
| ~ r1(X7,X10)
| r1(X7,sK224(X7))
| p57(X7) ) ).
cnf(u3475,negated_conjecture,
( ~ p57(sK221(X1))
| ~ p57(X1)
| ~ r1(sK220,X1)
| ~ p56(X1)
| p57(X2)
| ~ r1(X1,X2) ) ).
cnf(u3479,negated_conjecture,
( ~ p56(X1)
| ~ p57(X1)
| r1(X1,sK221(X1))
| ~ r1(sK220,X1)
| p57(X2)
| ~ r1(X1,X2) ) ).
cnf(u661,axiom,
( ~ sP19(X0)
| p21(X1)
| r1(X1,sK160(X1))
| r1(X1,sK162(X1))
| ~ r1(X0,X1) ) ).
cnf(u273,axiom,
( ~ p54(sK66(X1))
| p54(X1)
| r1(sK64(X1),sK65(X1))
| ~ r1(X0,X1)
| ~ sP51(X0) ) ).
cnf(u248,axiom,
( ~ sP53(X0)
| p56(X1)
| r1(sK58(X1),sK59(X1))
| p55(X1)
| ~ r1(X0,X1) ) ).
cnf(u778,axiom,
( ~ sP9(X0)
| p11(X1)
| r1(sK190(X1),sK191(X1))
| r1(X1,sK192(X1))
| ~ r1(X0,X1) ) ).
cnf(u659,axiom,
( ~ sP19(X0)
| p21(X1)
| r1(X1,sK160(X1))
| p20(X1)
| ~ r1(X0,X1) ) ).
cnf(u550,axiom,
( ~ sP28(X0)
| p31(X1)
| r1(sK133(X1),sK134(X1))
| r1(X1,sK135(X1))
| ~ r1(X0,X1) ) ).
cnf(u524,axiom,
( ~ sP30(X0)
| p33(X1)
| r1(sK127(X1),sK128(X1))
| p32(X1)
| ~ r1(X0,X1) ) ).
cnf(u784,axiom,
( ~ sP8(X0)
| p10(X1)
| p9(sK193(X1))
| r1(X1,sK195(X1))
| ~ r1(X0,X1) ) ).
cnf(u289,axiom,
( ~ sP50(X0)
| p53(X1)
| r1(X1,sK67(X1))
| r1(X1,sK69(X1))
| ~ r1(X0,X1) ) ).
cnf(u556,axiom,
( ~ sP27(X0)
| p29(X1)
| p28(sK136(X1))
| r1(X1,sK138(X1))
| ~ r1(X0,X1) ) ).
cnf(u521,axiom,
( ~ p33(sK128(X1))
| p33(X1)
| ~ r1(X0,X1)
| p32(X1)
| ~ sP30(X0) ) ).
cnf(u276,axiom,
( ~ p54(sK66(X1))
| p54(X1)
| r1(X1,sK64(X1))
| ~ r1(X0,X1)
| ~ sP51(X0) ) ).
cnf(u805,axiom,
( ~ sP7(X0)
| p9(X1)
| r1(X1,sK196(X1))
| r1(X1,sK198(X1))
| ~ r1(X0,X1) ) ).
cnf(u535,axiom,
( ~ p32(sK131(X1))
| p32(X1)
| ~ r1(X0,X1)
| r1(X1,sK132(X1))
| ~ sP29(X0) ) ).
cnf(u803,axiom,
( ~ sP7(X0)
| p9(X1)
| r1(X1,sK196(X1))
| p8(X1)
| ~ r1(X0,X1) ) ).
cnf(u678,axiom,
( ~ p19(sK168(X1))
| p19(X1)
| ~ p19(sK167(X1))
| ~ r1(X0,X1)
| ~ sP17(X0) ) ).
cnf(u295,axiom,
( ~ p52(sK71(X1))
| p52(X1)
| ~ r1(X0,X1)
| r1(X1,sK72(X1))
| ~ sP49(X0) ) ).
cnf(u417,axiom,
( ~ p42(sK102(X1))
| p42(X1)
| r1(sK100(X1),sK101(X1))
| ~ r1(X0,X1)
| ~ sP39(X0) ) ).
cnf(u649,axiom,
( ~ sP20(X0)
| p22(X1)
| r1(X1,sK157(X1))
| r1(X1,sK159(X1))
| ~ r1(X0,X1) ) ).
cnf(u404,axiom,
( ~ sP40(X0)
| p43(X1)
| r1(sK97(X1),sK98(X1))
| p42(X1)
| ~ r1(X0,X1) ) ).
cnf(u818,axiom,
( ~ sP5(X0)
| p7(X1)
| p6(sK202(X1))
| p6(X1)
| ~ r1(X0,X1) ) ).
cnf(u663,axiom,
( ~ p20(sK165(X1))
| p20(X1)
| p19(sK163(X1))
| ~ r1(X0,X1)
| ~ sP18(X0) ) ).
cnf(u538,axiom,
( ~ sP29(X0)
| p32(X1)
| r1(sK130(X1),sK131(X1))
| r1(X1,sK132(X1))
| ~ r1(X0,X1) ) ).
cnf(u824,axiom,
( ~ sP5(X0)
| p7(X1)
| r1(sK202(X1),sK203(X1))
| p6(X1)
| ~ r1(X0,X1) ) ).
cnf(u293,axiom,
( ~ p52(sK71(X1))
| p52(X1)
| ~ r1(X0,X1)
| p51(X1)
| ~ sP49(X0) ) ).
cnf(u544,axiom,
( ~ sP28(X0)
| p31(X1)
| p30(sK133(X1))
| r1(X1,sK135(X1))
| ~ r1(X0,X1) ) ).
cnf(u423,axiom,
( ~ p41(sK105(X1))
| p41(X1)
| p40(sK103(X1))
| ~ r1(X0,X1)
| ~ sP38(X0) ) ).
cnf(u561,axiom,
( ~ p29(sK138(X1))
| p29(X1)
| r1(sK136(X1),sK137(X1))
| ~ r1(X0,X1)
| ~ sP27(X0) ) ).
cnf(u316,axiom,
( ~ sP47(X0)
| p50(X1)
| p49(sK76(X1))
| r1(X1,sK78(X1))
| ~ r1(X0,X1) ) ).
cnf(u575,axiom,
( ~ sP26(X0)
| p28(X1)
| r1(X1,sK139(X1))
| p27(X1)
| ~ r1(X0,X1) ) ).
cnf(u666,axiom,
( ~ p20(sK165(X1))
| p20(X1)
| ~ p20(sK164(X1))
| ~ r1(X0,X1)
| ~ sP18(X0) ) ).
cnf(u421,axiom,
( ~ sP39(X0)
| p42(X1)
| r1(X1,sK100(X1))
| r1(X1,sK102(X1))
| ~ r1(X0,X1) ) ).
cnf(u672,axiom,
( ~ p20(sK165(X1))
| p20(X1)
| r1(X1,sK163(X1))
| ~ r1(X0,X1)
| ~ sP18(X0) ) ).
cnf(u306,axiom,
( ~ p51(sK75(X1))
| p51(X1)
| ~ p51(sK74(X1))
| ~ r1(X0,X1)
| ~ sP48(X0) ) ).
cnf(u689,axiom,
( ~ p18(sK170(X1))
| p18(X1)
| ~ r1(X0,X1)
| p17(X1)
| ~ sP16(X0) ) ).
cnf(u444,axiom,
( ~ p40(sK108(X1))
| p40(X1)
| r1(X1,sK106(X1))
| ~ r1(X0,X1)
| ~ sP37(X0) ) ).
cnf(u774,axiom,
( ~ p11(sK192(X1))
| p11(X1)
| ~ p11(sK191(X1))
| ~ r1(X0,X1)
| ~ sP9(X0) ) ).
cnf(u703,axiom,
( ~ p17(sK173(X1))
| p17(X1)
| ~ r1(X0,X1)
| r1(X1,sK174(X1))
| ~ sP15(X0) ) ).
cnf(u335,axiom,
( ~ sP46(X0)
| p49(X1)
| r1(X1,sK79(X1))
| p48(X1)
| ~ r1(X0,X1) ) ).
cnf(u434,axiom,
( ~ sP37(X0)
| p40(X1)
| p39(sK106(X1))
| p39(X1)
| ~ r1(X0,X1) ) ).
cnf(u578,axiom,
( ~ sP25(X0)
| p27(X1)
| p26(sK142(X1))
| p26(X1)
| ~ r1(X0,X1) ) ).
cnf(u333,axiom,
( ~ p49(sK81(X1))
| p49(X1)
| r1(sK79(X1),sK80(X1))
| ~ r1(X0,X1)
| ~ sP46(X0) ) ).
cnf(u584,axiom,
( ~ sP25(X0)
| p27(X1)
| r1(sK142(X1),sK143(X1))
| p26(X1)
| ~ r1(X0,X1) ) ).
cnf(u432,axiom,
( ~ p41(sK105(X1))
| p41(X1)
| r1(X1,sK103(X1))
| ~ r1(X0,X1)
| ~ sP38(X0) ) ).
cnf(u833,axiom,
( ~ p6(sK206(X1))
| p6(X1)
| ~ r1(X0,X1)
| p5(X1)
| ~ sP4(X0) ) ).
cnf(u847,axiom,
( ~ p5(sK209(X1))
| p5(X1)
| ~ r1(X0,X1)
| r1(X1,sK210(X1))
| ~ sP3(X0) ) ).
cnf(u706,axiom,
( ~ sP15(X0)
| p17(X1)
| r1(sK172(X1),sK173(X1))
| r1(X1,sK174(X1))
| ~ r1(X0,X1) ) ).
cnf(u636,axiom,
( ~ p23(sK156(X1))
| p23(X1)
| r1(X1,sK154(X1))
| ~ r1(X0,X1)
| ~ sP21(X0) ) ).
cnf(u323,axiom,
( ~ sP47(X0)
| p50(X1)
| r1(X1,sK76(X1))
| p49(X1)
| ~ r1(X0,X1) ) ).
cnf(u461,axiom,
( ~ p38(sK113(X1))
| p38(X1)
| ~ r1(X0,X1)
| p37(X1)
| ~ sP35(X0) ) ).
cnf(u712,axiom,
( ~ sP14(X0)
| p16(X1)
| p15(sK175(X1))
| r1(X1,sK177(X1))
| ~ r1(X0,X1) ) ).
cnf(u346,axiom,
( ~ sP45(X0)
| p48(X1)
| r1(sK82(X1),sK83(X1))
| r1(X1,sK84(X1))
| ~ r1(X0,X1) ) ).
cnf(u862,axiom,
( ~ sP2(X0)
| p4(X1)
| r1(sK211(X1),sK212(X1))
| r1(X1,sK213(X1))
| ~ r1(X0,X1) ) ).
cnf(u868,axiom,
( ~ sP1(X0)
| p3(X1)
| p2(sK214(X1))
| r1(X1,sK216(X1))
| ~ r1(X0,X1) ) ).
cnf(u451,axiom,
( ~ p39(sK110(X1))
| p39(X1)
| ~ r1(X0,X1)
| r1(X1,sK111(X1))
| ~ sP36(X0) ) ).
cnf(u605,axiom,
( ~ p25(sK149(X1))
| p25(X1)
| ~ r1(X0,X1)
| p24(X1)
| ~ sP23(X0) ) ).
cnf(u344,axiom,
( ~ sP45(X0)
| p48(X1)
| r1(sK82(X1),sK83(X1))
| p47(X1)
| ~ r1(X0,X1) ) ).
cnf(u474,axiom,
( ~ p37(sK117(X1))
| p37(X1)
| ~ p37(sK116(X1))
| ~ r1(X0,X1)
| ~ sP34(X0) ) ).
cnf(u873,axiom,
( ~ p3(sK216(X1))
| p3(X1)
| r1(sK214(X1),sK215(X1))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u603,axiom,
( ~ p25(sK150(X1))
| p25(X1)
| p24(sK148(X1))
| ~ r1(X0,X1)
| ~ sP23(X0) ) ).
cnf(u887,axiom,
( ~ sP0(X0)
| p2(X1)
| r1(X1,sK217(X1))
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u363,axiom,
( ~ p46(sK90(X1))
| p46(X1)
| p45(sK88(X1))
| ~ r1(X0,X1)
| ~ sP43(X0) ) ).
cnf(u716,axiom,
( ~ sP14(X0)
| p16(X1)
| r1(sK175(X1),sK176(X1))
| p15(X1)
| ~ r1(X0,X1) ) ).
cnf(u350,axiom,
( ~ sP44(X0)
| p47(X1)
| p46(sK85(X1))
| p46(X1)
| ~ r1(X0,X1) ) ).
cnf(u733,axiom,
( ~ sP13(X0)
| p15(X1)
| r1(X1,sK178(X1))
| r1(X1,sK180(X1))
| ~ r1(X0,X1) ) ).
cnf(u472,axiom,
( ~ sP34(X0)
| p37(X1)
| p36(sK115(X1))
| r1(X1,sK117(X1))
| ~ r1(X0,X1) ) ).
cnf(u731,axiom,
( ~ sP13(X0)
| p15(X1)
| r1(X1,sK178(X1))
| p14(X1)
| ~ r1(X0,X1) ) ).
cnf(u622,axiom,
( ~ sP22(X0)
| p24(X1)
| r1(sK151(X1),sK152(X1))
| r1(X1,sK153(X1))
| ~ r1(X0,X1) ) ).
cnf(u361,axiom,
( ~ sP44(X0)
| p47(X1)
| r1(X1,sK85(X1))
| r1(X1,sK87(X1))
| ~ r1(X0,X1) ) ).
cnf(u628,axiom,
( ~ sP21(X0)
| p23(X1)
| p22(sK154(X1))
| r1(X1,sK156(X1))
| ~ r1(X0,X1) ) ).
cnf(u491,axiom,
( ~ sP33(X0)
| p36(X1)
| r1(X1,sK118(X1))
| p35(X1)
| ~ r1(X0,X1) ) ).
cnf(u517,axiom,
( ~ sP31(X0)
| p34(X1)
| r1(X1,sK124(X1))
| r1(X1,sK126(X1))
| ~ r1(X0,X1) ) ).
cnf(u256,axiom,
( ~ sP52(X0)
| p55(X1)
| p54(sK61(X1))
| r1(X1,sK63(X1))
| ~ r1(X0,X1) ) ).
cnf(u478,axiom,
( ~ sP34(X0)
| p37(X1)
| r1(sK115(X1),sK116(X1))
| r1(X1,sK117(X1))
| ~ r1(X0,X1) ) ).
cnf(u877,axiom,
( ~ sP1(X0)
| p3(X1)
| r1(X1,sK214(X1))
| r1(X1,sK216(X1))
| ~ r1(X0,X1) ) ).
cnf(u234,axiom,
( ~ p57(sK57(X1))
| p57(X1)
| ~ p57(sK56(X1))
| ~ r1(X0,X1)
| ~ sP54(X0) ) ).
cnf(u515,axiom,
( ~ sP31(X0)
| p34(X1)
| r1(X1,sK124(X1))
| p33(X1)
| ~ r1(X0,X1) ) ).
cnf(u875,axiom,
( ~ sP1(X0)
| p3(X1)
| r1(X1,sK214(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u489,axiom,
( ~ p36(sK120(X1))
| p36(X1)
| r1(sK118(X1),sK119(X1))
| ~ r1(X0,X1)
| ~ sP33(X0) ) ).
cnf(u756,axiom,
( ~ p13(sK186(X1))
| p13(X1)
| r1(X1,sK184(X1))
| ~ r1(X0,X1)
| ~ sP11(X0) ) ).
cnf(u262,axiom,
( ~ sP52(X0)
| p55(X1)
| r1(sK61(X1),sK62(X1))
| r1(X1,sK63(X1))
| ~ r1(X0,X1) ) ).
cnf(u645,axiom,
( ~ p22(sK159(X1))
| p22(X1)
| r1(sK157(X1),sK158(X1))
| ~ r1(X0,X1)
| ~ sP20(X0) ) ).
cnf(u643,axiom,
( ~ p22(sK158(X1))
| p22(X1)
| ~ r1(X0,X1)
| r1(X1,sK159(X1))
| ~ sP20(X0) ) ).
cnf(u534,axiom,
( ~ p32(sK132(X1))
| p32(X1)
| ~ p32(sK131(X1))
| ~ r1(X0,X1)
| ~ sP29(X0) ) ).
cnf(u768,axiom,
( ~ p12(sK189(X1))
| p12(X1)
| r1(X1,sK187(X1))
| ~ r1(X0,X1)
| ~ sP10(X0) ) ).
cnf(u540,axiom,
( ~ p32(sK132(X1))
| p32(X1)
| r1(X1,sK130(X1))
| ~ r1(X0,X1)
| ~ sP29(X0) ) ).
cnf(u633,axiom,
( ~ p23(sK156(X1))
| p23(X1)
| r1(sK154(X1),sK155(X1))
| ~ r1(X0,X1)
| ~ sP21(X0) ) ).
cnf(u260,axiom,
( ~ sP52(X0)
| p55(X1)
| r1(sK61(X1),sK62(X1))
| p54(X1)
| ~ r1(X0,X1) ) ).
cnf(u390,axiom,
( ~ p44(sK96(X1))
| p44(X1)
| ~ p44(sK95(X1))
| ~ r1(X0,X1)
| ~ sP41(X0) ) ).
cnf(u519,axiom,
( ~ p33(sK129(X1))
| p33(X1)
| p32(sK127(X1))
| ~ r1(X0,X1)
| ~ sP30(X0) ) ).
cnf(u787,axiom,
( ~ p10(sK194(X1))
| p10(X1)
| ~ r1(X0,X1)
| r1(X1,sK195(X1))
| ~ sP8(X0) ) ).
cnf(u662,axiom,
( ~ sP18(X0)
| p20(X1)
| p19(sK163(X1))
| p19(X1)
| ~ r1(X0,X1) ) ).
cnf(u279,axiom,
( ~ p53(sK69(X1))
| p53(X1)
| p52(sK67(X1))
| ~ r1(X0,X1)
| ~ sP50(X0) ) ).
cnf(u401,axiom,
( ~ p43(sK98(X1))
| p43(X1)
| ~ r1(X0,X1)
| p42(X1)
| ~ sP40(X0) ) ).
cnf(u761,axiom,
( ~ p12(sK188(X1))
| p12(X1)
| ~ r1(X0,X1)
| p11(X1)
| ~ sP10(X0) ) ).
cnf(u388,axiom,
( ~ sP41(X0)
| p44(X1)
| p43(sK94(X1))
| r1(X1,sK96(X1))
| ~ r1(X0,X1) ) ).
cnf(u802,axiom,
( ~ sP7(X0)
| p9(X1)
| r1(sK196(X1),sK197(X1))
| r1(X1,sK198(X1))
| ~ r1(X0,X1) ) ).
cnf(u647,axiom,
( ~ sP20(X0)
| p22(X1)
| r1(X1,sK157(X1))
| p21(X1)
| ~ r1(X0,X1) ) ).
cnf(u522,axiom,
( ~ p33(sK129(X1))
| p33(X1)
| ~ p33(sK128(X1))
| ~ r1(X0,X1)
| ~ sP30(X0) ) ).
cnf(u261,axiom,
( ~ p55(sK63(X1))
| p55(X1)
| r1(sK61(X1),sK62(X1))
| ~ r1(X0,X1)
| ~ sP52(X0) ) ).
cnf(u808,axiom,
( ~ sP6(X0)
| p8(X1)
| p7(sK199(X1))
| r1(X1,sK201(X1))
| ~ r1(X0,X1) ) ).
cnf(u277,axiom,
( ~ sP51(X0)
| p54(X1)
| r1(X1,sK64(X1))
| r1(X1,sK66(X1))
| ~ r1(X0,X1) ) ).
cnf(u528,axiom,
( ~ p33(sK129(X1))
| p33(X1)
| r1(X1,sK127(X1))
| ~ r1(X0,X1)
| ~ sP30(X0) ) ).
cnf(u407,axiom,
( ~ sP40(X0)
| p43(X1)
| r1(X1,sK97(X1))
| p42(X1)
| ~ r1(X0,X1) ) ).
cnf(u300,axiom,
( ~ p52(sK72(X1))
| p52(X1)
| r1(X1,sK70(X1))
| ~ r1(X0,X1)
| ~ sP49(X0) ) ).
cnf(u829,axiom,
( ~ sP5(X0)
| p7(X1)
| r1(X1,sK202(X1))
| r1(X1,sK204(X1))
| ~ r1(X0,X1) ) ).
cnf(u559,axiom,
( ~ p29(sK137(X1))
| p29(X1)
| ~ r1(X0,X1)
| r1(X1,sK138(X1))
| ~ sP27(X0) ) ).
cnf(u650,axiom,
( ~ sP19(X0)
| p21(X1)
| p20(sK160(X1))
| p20(X1)
| ~ r1(X0,X1) ) ).
cnf(u319,axiom,
( ~ p50(sK77(X1))
| p50(X1)
| ~ r1(X0,X1)
| r1(X1,sK78(X1))
| ~ sP47(X0) ) ).
cnf(u405,axiom,
( ~ p43(sK99(X1))
| p43(X1)
| r1(sK97(X1),sK98(X1))
| ~ r1(X0,X1)
| ~ sP40(X0) ) ).
cnf(u656,axiom,
( ~ sP19(X0)
| p21(X1)
| r1(sK160(X1),sK161(X1))
| p20(X1)
| ~ r1(X0,X1) ) ).
cnf(u290,axiom,
( ~ sP49(X0)
| p52(X1)
| p51(sK70(X1))
| p51(X1)
| ~ r1(X0,X1) ) ).
cnf(u673,axiom,
( ~ sP18(X0)
| p20(X1)
| r1(X1,sK163(X1))
| r1(X1,sK165(X1))
| ~ r1(X0,X1) ) ).
cnf(u428,axiom,
( ~ sP38(X0)
| p41(X1)
| r1(sK103(X1),sK104(X1))
| p40(X1)
| ~ r1(X0,X1) ) ).
cnf(u806,axiom,
( ~ sP6(X0)
| p8(X1)
| p7(sK199(X1))
| p7(X1)
| ~ r1(X0,X1) ) ).
cnf(u687,axiom,
( ~ p18(sK171(X1))
| p18(X1)
| p17(sK169(X1))
| ~ r1(X0,X1)
| ~ sP16(X0) ) ).
cnf(u562,axiom,
( ~ sP27(X0)
| p29(X1)
| r1(sK136(X1),sK137(X1))
| r1(X1,sK138(X1))
| ~ r1(X0,X1) ) ).
cnf(u1170,negated_conjecture,
( ~ r1(sK330,X274)
| p15(X274) ) ).
cnf(u812,axiom,
( ~ sP6(X0)
| p8(X1)
| r1(sK199(X1),sK200(X1))
| p7(X1)
| ~ r1(X0,X1) ) ).
cnf(u317,axiom,
( ~ p50(sK77(X1))
| p50(X1)
| ~ r1(X0,X1)
| p49(X1)
| ~ sP47(X0) ) ).
cnf(u568,axiom,
( ~ sP26(X0)
| p28(X1)
| p27(sK139(X1))
| r1(X1,sK141(X1))
| ~ r1(X0,X1) ) ).
cnf(u447,axiom,
( ~ p39(sK111(X1))
| p39(X1)
| p38(sK109(X1))
| ~ r1(X0,X1)
| ~ sP36(X0) ) ).
cnf(u418,axiom,
( ~ sP39(X0)
| p42(X1)
| r1(sK100(X1),sK101(X1))
| r1(X1,sK102(X1))
| ~ r1(X0,X1) ) ).
cnf(u817,axiom,
( ~ sP6(X0)
| p8(X1)
| r1(X1,sK199(X1))
| r1(X1,sK201(X1))
| ~ r1(X0,X1) ) ).
cnf(u831,axiom,
( ~ p6(sK207(X1))
| p6(X1)
| p5(sK205(X1))
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u690,axiom,
( ~ p18(sK171(X1))
| p18(X1)
| ~ p18(sK170(X1))
| ~ r1(X0,X1)
| ~ sP16(X0) ) ).
cnf(u307,axiom,
( ~ p51(sK74(X1))
| p51(X1)
| ~ r1(X0,X1)
| r1(X1,sK75(X1))
| ~ sP48(X0) ) ).
cnf(u445,axiom,
( ~ sP37(X0)
| p40(X1)
| r1(X1,sK106(X1))
| r1(X1,sK108(X1))
| ~ r1(X0,X1) ) ).
cnf(u696,axiom,
( ~ p18(sK171(X1))
| p18(X1)
| r1(X1,sK169(X1))
| ~ r1(X0,X1)
| ~ sP16(X0) ) ).
cnf(u416,axiom,
( ~ sP39(X0)
| p42(X1)
| r1(sK100(X1),sK101(X1))
| p41(X1)
| ~ r1(X0,X1) ) ).
cnf(u435,axiom,
( ~ p40(sK108(X1))
| p40(X1)
| p39(sK106(X1))
| ~ r1(X0,X1)
| ~ sP37(X0) ) ).
cnf(u330,axiom,
( ~ p49(sK81(X1))
| p49(X1)
| ~ p49(sK80(X1))
| ~ r1(X0,X1)
| ~ sP46(X0) ) ).
cnf(u846,axiom,
( ~ p5(sK210(X1))
| p5(X1)
| ~ p5(sK209(X1))
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u852,axiom,
( ~ p5(sK210(X1))
| p5(X1)
| r1(X1,sK208(X1))
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u589,axiom,
( ~ sP25(X0)
| p27(X1)
| r1(X1,sK142(X1))
| r1(X1,sK144(X1))
| ~ r1(X0,X1) ) ).
cnf(u328,axiom,
( ~ sP46(X0)
| p49(X1)
| p48(sK79(X1))
| r1(X1,sK81(X1))
| ~ r1(X0,X1) ) ).
cnf(u458,axiom,
( ~ sP35(X0)
| p38(X1)
| p37(sK112(X1))
| p37(X1)
| ~ r1(X0,X1) ) ).
cnf(u857,axiom,
( ~ p4(sK212(X1))
| p4(X1)
| ~ r1(X0,X1)
| p3(X1)
| ~ sP2(X0) ) ).
cnf(u587,axiom,
( ~ sP25(X0)
| p27(X1)
| r1(X1,sK142(X1))
| p26(X1)
| ~ r1(X0,X1) ) ).
cnf(u871,axiom,
( ~ p3(sK215(X1))
| p3(X1)
| ~ r1(X0,X1)
| r1(X1,sK216(X1))
| ~ sP1(X0) ) ).
cnf(u347,axiom,
( ~ sP45(X0)
| p48(X1)
| r1(X1,sK82(X1))
| p47(X1)
| ~ r1(X0,X1) ) ).
cnf(u334,axiom,
( ~ sP46(X0)
| p49(X1)
| r1(sK79(X1),sK80(X1))
| r1(X1,sK81(X1))
| ~ r1(X0,X1) ) ).
cnf(u717,axiom,
( ~ p16(sK177(X1))
| p16(X1)
| r1(sK175(X1),sK176(X1))
| ~ r1(X0,X1)
| ~ sP14(X0) ) ).
cnf(u456,axiom,
( ~ p39(sK111(X1))
| p39(X1)
| r1(X1,sK109(X1))
| ~ r1(X0,X1)
| ~ sP36(X0) ) ).
cnf(u851,axiom,
( ~ sP3(X0)
| p5(X1)
| r1(X1,sK208(X1))
| p4(X1)
| ~ r1(X0,X1) ) ).
cnf(u715,axiom,
( ~ p16(sK176(X1))
| p16(X1)
| ~ r1(X0,X1)
| r1(X1,sK177(X1))
| ~ sP14(X0) ) ).
cnf(u606,axiom,
( ~ p25(sK150(X1))
| p25(X1)
| ~ p25(sK149(X1))
| ~ r1(X0,X1)
| ~ sP23(X0) ) ).
cnf(u345,axiom,
( ~ p48(sK84(X1))
| p48(X1)
| r1(sK82(X1),sK83(X1))
| ~ r1(X0,X1)
| ~ sP45(X0) ) ).
cnf(u612,axiom,
( ~ p25(sK150(X1))
| p25(X1)
| r1(X1,sK148(X1))
| ~ r1(X0,X1)
| ~ sP23(X0) ) ).
cnf(u475,axiom,
( ~ p37(sK116(X1))
| p37(X1)
| ~ r1(X0,X1)
| r1(X1,sK117(X1))
| ~ sP34(X0) ) ).
cnf(u629,axiom,
( ~ p23(sK155(X1))
| p23(X1)
| ~ r1(X0,X1)
| p22(X1)
| ~ sP21(X0) ) ).
cnf(u368,axiom,
( ~ sP43(X0)
| p46(X1)
| r1(sK88(X1),sK89(X1))
| p45(X1)
| ~ r1(X0,X1) ) ).
cnf(u462,axiom,
( ~ p38(sK114(X1))
| p38(X1)
| ~ p38(sK113(X1))
| ~ r1(X0,X1)
| ~ sP35(X0) ) ).
cnf(u627,axiom,
( ~ p23(sK156(X1))
| p23(X1)
| p22(sK154(X1))
| ~ r1(X0,X1)
| ~ sP21(X0) ) ).
cnf(u859,axiom,
( ~ p4(sK212(X1))
| p4(X1)
| ~ r1(X0,X1)
| r1(X1,sK213(X1))
| ~ sP2(X0) ) ).
cnf(u734,axiom,
( ~ sP12(X0)
| p14(X1)
| p13(sK181(X1))
| p13(X1)
| ~ r1(X0,X1) ) ).
cnf(u473,axiom,
( ~ p37(sK116(X1))
| p37(X1)
| ~ r1(X0,X1)
| p36(X1)
| ~ sP34(X0) ) ).
cnf(u740,axiom,
( ~ sP12(X0)
| p14(X1)
| r1(sK181(X1),sK182(X1))
| p13(X1)
| ~ r1(X0,X1) ) ).
cnf(u374,axiom,
( ~ sP42(X0)
| p45(X1)
| p44(sK91(X1))
| p44(X1)
| ~ r1(X0,X1) ) ).
cnf(u757,axiom,
( ~ sP11(X0)
| p13(X1)
| r1(X1,sK184(X1))
| r1(X1,sK186(X1))
| ~ r1(X0,X1) ) ).
cnf(u874,axiom,
( ~ sP1(X0)
| p3(X1)
| r1(sK214(X1),sK215(X1))
| r1(X1,sK216(X1))
| ~ r1(X0,X1) ) ).
cnf(u755,axiom,
( ~ sP11(X0)
| p13(X1)
| r1(X1,sK184(X1))
| p12(X1)
| ~ r1(X0,X1) ) ).
cnf(u518,axiom,
( ~ sP30(X0)
| p33(X1)
| p32(sK127(X1))
| p32(X1)
| ~ r1(X0,X1) ) ).
cnf(u880,axiom,
( ~ sP0(X0)
| p2(X1)
| p1(sK217(X1))
| r1(X1,sK219(X1))
| ~ r1(X0,X1) ) ).
cnf(u247,axiom,
( ~ p56(sK59(X1))
| p56(X1)
| ~ r1(X0,X1)
| r1(X1,sK60(X1))
| ~ sP53(X0) ) ).
cnf(u257,axiom,
( ~ p55(sK62(X1))
| p55(X1)
| ~ r1(X0,X1)
| p54(X1)
| ~ sP52(X0) ) ).
cnf(u479,axiom,
( ~ sP34(X0)
| p37(X1)
| r1(X1,sK115(X1))
| p36(X1)
| ~ r1(X0,X1) ) ).
cnf(u617,axiom,
( ~ p24(sK152(X1))
| p24(X1)
| ~ r1(X0,X1)
| p23(X1)
| ~ sP22(X0) ) ).
cnf(u372,axiom,
( ~ p46(sK90(X1))
| p46(X1)
| r1(X1,sK88(X1))
| ~ r1(X0,X1)
| ~ sP43(X0) ) ).
cnf(u502,axiom,
( ~ sP32(X0)
| p35(X1)
| r1(sK121(X1),sK122(X1))
| r1(X1,sK123(X1))
| ~ r1(X0,X1) ) ).
cnf(u773,axiom,
( ~ p11(sK191(X1))
| p11(X1)
| ~ r1(X0,X1)
| p10(X1)
| ~ sP9(X0) ) ).
cnf(u631,axiom,
( ~ p23(sK155(X1))
| p23(X1)
| ~ r1(X0,X1)
| r1(X1,sK156(X1))
| ~ sP21(X0) ) ).
cnf(u646,axiom,
( ~ sP20(X0)
| p22(X1)
| r1(sK157(X1),sK158(X1))
| r1(X1,sK159(X1))
| ~ r1(X0,X1) ) ).
cnf(u245,axiom,
( ~ p56(sK59(X1))
| p56(X1)
| ~ r1(X0,X1)
| p55(X1)
| ~ sP53(X0) ) ).
cnf(u263,axiom,
( ~ sP52(X0)
| p55(X1)
| r1(X1,sK61(X1))
| p54(X1)
| ~ r1(X0,X1) ) ).
cnf(u385,axiom,
( ~ sP42(X0)
| p45(X1)
| r1(X1,sK91(X1))
| r1(X1,sK93(X1))
| ~ r1(X0,X1) ) ).
cnf(u745,axiom,
( ~ sP12(X0)
| p14(X1)
| r1(X1,sK181(X1))
| r1(X1,sK183(X1))
| ~ r1(X0,X1) ) ).
cnf(u500,axiom,
( ~ sP32(X0)
| p35(X1)
| r1(sK121(X1),sK122(X1))
| p34(X1)
| ~ r1(X0,X1) ) ).
cnf(u786,axiom,
( ~ p10(sK195(X1))
| p10(X1)
| ~ p10(sK194(X1))
| ~ r1(X0,X1)
| ~ sP8(X0) ) ).
cnf(u792,axiom,
( ~ p10(sK195(X1))
| p10(X1)
| r1(X1,sK193(X1))
| ~ r1(X0,X1)
| ~ sP8(X0) ) ).
cnf(u512,axiom,
( ~ sP31(X0)
| p34(X1)
| r1(sK124(X1),sK125(X1))
| p33(X1)
| ~ r1(X0,X1) ) ).
cnf(u391,axiom,
( ~ p44(sK95(X1))
| p44(X1)
| ~ r1(X0,X1)
| r1(X1,sK96(X1))
| ~ sP41(X0) ) ).
cnf(u529,axiom,
( ~ sP30(X0)
| p33(X1)
| r1(X1,sK127(X1))
| r1(X1,sK129(X1))
| ~ r1(X0,X1) ) ).
cnf(u284,axiom,
( ~ sP50(X0)
| p53(X1)
| r1(sK67(X1),sK68(X1))
| p52(X1)
| ~ r1(X0,X1) ) ).
cnf(u543,axiom,
( ~ p31(sK135(X1))
| p31(X1)
| p30(sK133(X1))
| ~ r1(X0,X1)
| ~ sP28(X0) ) ).
cnf(u762,axiom,
( ~ p12(sK189(X1))
| p12(X1)
| ~ p12(sK188(X1))
| ~ r1(X0,X1)
| ~ sP10(X0) ) ).
cnf(u303,axiom,
( ~ p51(sK75(X1))
| p51(X1)
| p50(sK73(X1))
| ~ r1(X0,X1)
| ~ sP48(X0) ) ).
cnf(u389,axiom,
( ~ p44(sK95(X1))
| p44(X1)
| ~ r1(X0,X1)
| p43(X1)
| ~ sP41(X0) ) ).
cnf(u640,axiom,
( ~ sP20(X0)
| p22(X1)
| p21(sK157(X1))
| r1(X1,sK159(X1))
| ~ r1(X0,X1) ) ).
cnf(u274,axiom,
( ~ sP51(X0)
| p54(X1)
| r1(sK64(X1),sK65(X1))
| r1(X1,sK66(X1))
| ~ r1(X0,X1) ) ).
cnf(u657,axiom,
( ~ p21(sK162(X1))
| p21(X1)
| r1(sK160(X1),sK161(X1))
| ~ r1(X0,X1)
| ~ sP19(X0) ) ).
cnf(u412,axiom,
( ~ sP39(X0)
| p42(X1)
| p41(sK100(X1))
| r1(X1,sK102(X1))
| ~ r1(X0,X1) ) ).
cnf(u790,axiom,
( ~ sP8(X0)
| p10(X1)
| r1(sK193(X1),sK194(X1))
| r1(X1,sK195(X1))
| ~ r1(X0,X1) ) ).
cnf(u1173,negated_conjecture,
( ~ r1(sK329,X272)
| p15(X272) ) ).
cnf(u671,axiom,
( ~ sP18(X0)
| p20(X1)
| r1(X1,sK163(X1))
| p19(X1)
| ~ r1(X0,X1) ) ).
cnf(u546,axiom,
( ~ p31(sK135(X1))
| p31(X1)
| ~ p31(sK134(X1))
| ~ r1(X0,X1)
| ~ sP28(X0) ) ).
cnf(u796,axiom,
( ~ sP7(X0)
| p9(X1)
| p8(sK196(X1))
| r1(X1,sK198(X1))
| ~ r1(X0,X1) ) ).
cnf(u301,axiom,
( ~ sP49(X0)
| p52(X1)
| r1(X1,sK70(X1))
| r1(X1,sK72(X1))
| ~ r1(X0,X1) ) ).
cnf(u552,axiom,
( ~ p31(sK135(X1))
| p31(X1)
| r1(X1,sK133(X1))
| ~ r1(X0,X1)
| ~ sP28(X0) ) ).
cnf(u431,axiom,
( ~ sP38(X0)
| p41(X1)
| r1(X1,sK103(X1))
| p40(X1)
| ~ r1(X0,X1) ) ).
cnf(u569,axiom,
( ~ p28(sK140(X1))
| p28(X1)
| ~ r1(X0,X1)
| p27(X1)
| ~ sP26(X0) ) ).
cnf(u402,axiom,
( ~ p43(sK99(X1))
| p43(X1)
| ~ p43(sK98(X1))
| ~ r1(X0,X1)
| ~ sP40(X0) ) ).
cnf(u801,axiom,
( ~ p9(sK198(X1))
| p9(X1)
| r1(sK196(X1),sK197(X1))
| ~ r1(X0,X1)
| ~ sP7(X0) ) ).
cnf(u815,axiom,
( ~ sP6(X0)
| p8(X1)
| r1(X1,sK199(X1))
| p7(X1)
| ~ r1(X0,X1) ) ).
cnf(u674,axiom,
( ~ sP17(X0)
| p19(X1)
| p18(sK166(X1))
| p18(X1)
| ~ r1(X0,X1) ) ).
cnf(u291,axiom,
( ~ p52(sK72(X1))
| p52(X1)
| p51(sK70(X1))
| ~ r1(X0,X1)
| ~ sP49(X0) ) ).
cnf(u429,axiom,
( ~ p41(sK105(X1))
| p41(X1)
| r1(sK103(X1),sK104(X1))
| ~ r1(X0,X1)
| ~ sP38(X0) ) ).
cnf(u680,axiom,
( ~ sP17(X0)
| p19(X1)
| r1(sK166(X1),sK167(X1))
| p18(X1)
| ~ r1(X0,X1) ) ).
cnf(u314,axiom,
( ~ sP47(X0)
| p50(X1)
| p49(sK76(X1))
| p49(X1)
| ~ r1(X0,X1) ) ).
cnf(u400,axiom,
( ~ sP40(X0)
| p43(X1)
| p42(sK97(X1))
| r1(X1,sK99(X1))
| ~ r1(X0,X1) ) ).
cnf(u830,axiom,
( ~ sP4(X0)
| p6(X1)
| p5(sK205(X1))
| p5(X1)
| ~ r1(X0,X1) ) ).
cnf(u539,axiom,
( ~ sP29(X0)
| p32(X1)
| r1(X1,sK130(X1))
| p31(X1)
| ~ r1(X0,X1) ) ).
cnf(u419,axiom,
( ~ sP39(X0)
| p42(X1)
| r1(X1,sK100(X1))
| p41(X1)
| ~ r1(X0,X1) ) ).
cnf(u573,axiom,
( ~ p28(sK141(X1))
| p28(X1)
| r1(sK139(X1),sK140(X1))
| ~ r1(X0,X1)
| ~ sP26(X0) ) ).
cnf(u312,axiom,
( ~ p51(sK75(X1))
| p51(X1)
| r1(X1,sK73(X1))
| ~ r1(X0,X1)
| ~ sP48(X0) ) ).
cnf(u442,axiom,
( ~ sP37(X0)
| p40(X1)
| r1(sK106(X1),sK107(X1))
| r1(X1,sK108(X1))
| ~ r1(X0,X1) ) ).
cnf(u571,axiom,
( ~ p28(sK140(X1))
| p28(X1)
| ~ r1(X0,X1)
| r1(X1,sK141(X1))
| ~ sP26(X0) ) ).
cnf(u836,axiom,
( ~ sP4(X0)
| p6(X1)
| r1(sK205(X1),sK206(X1))
| p5(X1)
| ~ r1(X0,X1) ) ).
cnf(u684,axiom,
( ~ p19(sK168(X1))
| p19(X1)
| r1(X1,sK166(X1))
| ~ r1(X0,X1)
| ~ sP17(X0) ) ).
cnf(u318,axiom,
( ~ p50(sK78(X1))
| p50(X1)
| ~ p50(sK77(X1))
| ~ r1(X0,X1)
| ~ sP47(X0) ) ).
cnf(u701,axiom,
( ~ p17(sK173(X1))
| p17(X1)
| ~ r1(X0,X1)
| p16(X1)
| ~ sP15(X0) ) ).
cnf(u440,axiom,
( ~ sP37(X0)
| p40(X1)
| r1(sK106(X1),sK107(X1))
| p39(X1)
| ~ r1(X0,X1) ) ).
cnf(u841,axiom,
( ~ sP4(X0)
| p6(X1)
| r1(X1,sK205(X1))
| r1(X1,sK207(X1))
| ~ r1(X0,X1) ) ).
cnf(u634,axiom,
( ~ sP21(X0)
| p23(X1)
| r1(sK154(X1),sK155(X1))
| r1(X1,sK156(X1))
| ~ r1(X0,X1) ) ).
cnf(u699,axiom,
( ~ p17(sK174(X1))
| p17(X1)
| p16(sK172(X1))
| ~ r1(X0,X1)
| ~ sP15(X0) ) ).
cnf(u855,axiom,
( ~ p4(sK213(X1))
| p4(X1)
| p3(sK211(X1))
| ~ r1(X0,X1)
| ~ sP2(X0) ) ).
cnf(u331,axiom,
( ~ p49(sK80(X1))
| p49(X1)
| ~ r1(X0,X1)
| r1(X1,sK81(X1))
| ~ sP46(X0) ) ).
cnf(u446,axiom,
( ~ sP36(X0)
| p39(X1)
| p38(sK109(X1))
| p38(X1)
| ~ r1(X0,X1) ) ).
cnf(u590,axiom,
( ~ sP24(X0)
| p26(X1)
| p25(sK145(X1))
| p25(X1)
| ~ r1(X0,X1) ) ).
cnf(u329,axiom,
( ~ p49(sK80(X1))
| p49(X1)
| ~ r1(X0,X1)
| p48(X1)
| ~ sP46(X0) ) ).
cnf(u596,axiom,
( ~ sP24(X0)
| p26(X1)
| r1(sK145(X1),sK146(X1))
| p25(X1)
| ~ r1(X0,X1) ) ).
cnf(u613,axiom,
( ~ sP23(X0)
| p25(X1)
| r1(X1,sK148(X1))
| r1(X1,sK150(X1))
| ~ r1(X0,X1) ) ).
cnf(u352,axiom,
( ~ sP44(X0)
| p47(X1)
| p46(sK85(X1))
| r1(X1,sK87(X1))
| ~ r1(X0,X1) ) ).
cnf(u845,axiom,
( ~ p5(sK209(X1))
| p5(X1)
| ~ r1(X0,X1)
| p4(X1)
| ~ sP3(X0) ) ).
cnf(u611,axiom,
( ~ sP23(X0)
| p25(X1)
| r1(X1,sK148(X1))
| p24(X1)
| ~ r1(X0,X1) ) ).
cnf(u843,axiom,
( ~ p5(sK210(X1))
| p5(X1)
| p4(sK208(X1))
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u718,axiom,
( ~ sP14(X0)
| p16(X1)
| r1(sK175(X1),sK176(X1))
| r1(X1,sK177(X1))
| ~ r1(X0,X1) ) ).
cnf(u457,axiom,
( ~ sP36(X0)
| p39(X1)
| r1(X1,sK109(X1))
| r1(X1,sK111(X1))
| ~ r1(X0,X1) ) ).
cnf(u724,axiom,
( ~ sP13(X0)
| p15(X1)
| p14(sK178(X1))
| r1(X1,sK180(X1))
| ~ r1(X0,X1) ) ).
cnf(u358,axiom,
( ~ sP44(X0)
| p47(X1)
| r1(sK85(X1),sK86(X1))
| r1(X1,sK87(X1))
| ~ r1(X0,X1) ) ).
cnf(u741,axiom,
( ~ p14(sK183(X1))
| p14(X1)
| r1(sK181(X1),sK182(X1))
| ~ r1(X0,X1)
| ~ sP12(X0) ) ).
cnf(u858,axiom,
( ~ p4(sK213(X1))
| p4(X1)
| ~ p4(sK212(X1))
| ~ r1(X0,X1)
| ~ sP2(X0) ) ).
cnf(u739,axiom,
( ~ p14(sK182(X1))
| p14(X1)
| ~ r1(X0,X1)
| r1(X1,sK183(X1))
| ~ sP12(X0) ) ).
cnf(u630,axiom,
( ~ p23(sK156(X1))
| p23(X1)
| ~ p23(sK155(X1))
| ~ r1(X0,X1)
| ~ sP21(X0) ) ).
cnf(u410,axiom,
( ~ sP39(X0)
| p42(X1)
| p41(sK100(X1))
| p41(X1)
| ~ r1(X0,X1) ) ).
cnf(u864,axiom,
( ~ p4(sK213(X1))
| p4(X1)
| r1(X1,sK211(X1))
| ~ r1(X0,X1)
| ~ sP2(X0) ) ).
cnf(u231,axiom,
( ~ p57(sK57(X1))
| p57(X1)
| p56(sK55(X1))
| ~ r1(X0,X1)
| ~ sP54(X0) ) ).
cnf(u369,axiom,
( ~ p46(sK90(X1))
| p46(X1)
| r1(sK88(X1),sK89(X1))
| ~ r1(X0,X1)
| ~ sP43(X0) ) ).
cnf(u463,axiom,
( ~ p38(sK113(X1))
| p38(X1)
| ~ r1(X0,X1)
| r1(X1,sK114(X1))
| ~ sP35(X0) ) ).
cnf(u601,axiom,
( ~ sP24(X0)
| p26(X1)
| r1(X1,sK145(X1))
| r1(X1,sK147(X1))
| ~ r1(X0,X1) ) ).
cnf(u356,axiom,
( ~ sP44(X0)
| p47(X1)
| r1(sK85(X1),sK86(X1))
| p46(X1)
| ~ r1(X0,X1) ) ).
cnf(u486,axiom,
( ~ p36(sK120(X1))
| p36(X1)
| ~ p36(sK119(X1))
| ~ r1(X0,X1)
| ~ sP33(X0) ) ).
cnf(u885,axiom,
( ~ p2(sK219(X1))
| p2(X1)
| r1(sK217(X1),sK218(X1))
| ~ r1(X0,X1)
| ~ sP0(X0) ) ).
cnf(u865,axiom,
( ~ sP2(X0)
| p4(X1)
| r1(X1,sK211(X1))
| r1(X1,sK213(X1))
| ~ r1(X0,X1) ) ).
cnf(u883,axiom,
( ~ p2(sK218(X1))
| p2(X1)
| ~ r1(X0,X1)
| r1(X1,sK219(X1))
| ~ sP0(X0) ) ).
cnf(u758,axiom,
( ~ sP10(X0)
| p12(X1)
| p11(sK187(X1))
| p11(X1)
| ~ r1(X0,X1) ) ).
cnf(u375,axiom,
( ~ p45(sK93(X1))
| p45(X1)
| p44(sK91(X1))
| ~ r1(X0,X1)
| ~ sP42(X0) ) ).
cnf(u497,axiom,
( ~ p35(sK122(X1))
| p35(X1)
| ~ r1(X0,X1)
| p34(X1)
| ~ sP32(X0) ) ).
cnf(u729,axiom,
( ~ p15(sK180(X1))
| p15(X1)
| r1(sK178(X1),sK179(X1))
| ~ r1(X0,X1)
| ~ sP13(X0) ) ).
cnf(u484,axiom,
( ~ sP33(X0)
| p36(X1)
| p35(sK118(X1))
| r1(X1,sK120(X1))
| ~ r1(X0,X1) ) ).
cnf(u240,axiom,
( ~ p57(sK57(X1))
| p57(X1)
| r1(X1,sK55(X1))
| ~ r1(X0,X1)
| ~ sP54(X0) ) ).
cnf(u770,axiom,
( ~ sP9(X0)
| p11(X1)
| p10(sK190(X1))
| p10(X1)
| ~ r1(X0,X1) ) ).
cnf(u414,axiom,
( ~ p42(sK102(X1))
| p42(X1)
| ~ p42(sK101(X1))
| ~ r1(X0,X1)
| ~ sP39(X0) ) ).
cnf(u743,axiom,
( ~ sP12(X0)
| p14(X1)
| r1(X1,sK181(X1))
| p13(X1)
| ~ r1(X0,X1) ) ).
cnf(u618,axiom,
( ~ p24(sK153(X1))
| p24(X1)
| ~ p24(sK152(X1))
| ~ r1(X0,X1)
| ~ sP22(X0) ) ).
cnf(u776,axiom,
( ~ sP9(X0)
| p11(X1)
| r1(sK190(X1),sK191(X1))
| p10(X1)
| ~ r1(X0,X1) ) ).
cnf(u373,axiom,
( ~ sP43(X0)
| p46(X1)
| r1(X1,sK88(X1))
| r1(X1,sK90(X1))
| ~ r1(X0,X1) ) ).
cnf(u624,axiom,
( ~ p24(sK153(X1))
| p24(X1)
| r1(X1,sK151(X1))
| ~ r1(X0,X1)
| ~ sP22(X0) ) ).
cnf(u503,axiom,
( ~ sP32(X0)
| p35(X1)
| r1(X1,sK121(X1))
| p34(X1)
| ~ r1(X0,X1) ) ).
cnf(u513,axiom,
( ~ p34(sK126(X1))
| p34(X1)
| r1(sK124(X1),sK125(X1))
| ~ r1(X0,X1)
| ~ sP31(X0) ) ).
cnf(u268,axiom,
( ~ sP51(X0)
| p54(X1)
| p53(sK64(X1))
| r1(X1,sK66(X1))
| ~ r1(X0,X1) ) ).
cnf(u246,axiom,
( ~ p56(sK60(X1))
| p56(X1)
| ~ p56(sK59(X1))
| ~ r1(X0,X1)
| ~ sP53(X0) ) ).
cnf(u527,axiom,
( ~ sP30(X0)
| p33(X1)
| r1(X1,sK127(X1))
| p32(X1)
| ~ r1(X0,X1) ) ).
cnf(u746,axiom,
( ~ sP11(X0)
| p13(X1)
| p12(sK184(X1))
| p12(X1)
| ~ r1(X0,X1) ) ).
cnf(u287,axiom,
( ~ sP50(X0)
| p53(X1)
| r1(X1,sK67(X1))
| p52(X1)
| ~ r1(X0,X1) ) ).
cnf(u501,axiom,
( ~ p35(sK123(X1))
| p35(X1)
| r1(sK121(X1),sK122(X1))
| ~ r1(X0,X1)
| ~ sP32(X0) ) ).
cnf(u752,axiom,
( ~ sP11(X0)
| p13(X1)
| r1(sK184(X1),sK185(X1))
| p12(X1)
| ~ r1(X0,X1) ) ).
cnf(u258,axiom,
( ~ p55(sK63(X1))
| p55(X1)
| ~ p55(sK62(X1))
| ~ r1(X0,X1)
| ~ sP52(X0) ) ).
cnf(u641,axiom,
( ~ p22(sK158(X1))
| p22(X1)
| ~ r1(X0,X1)
| p21(X1)
| ~ sP20(X0) ) ).
cnf(u396,axiom,
( ~ p44(sK96(X1))
| p44(X1)
| r1(X1,sK94(X1))
| ~ r1(X0,X1)
| ~ sP41(X0) ) ).
cnf(u244,axiom,
( ~ sP53(X0)
| p56(X1)
| p55(sK58(X1))
| r1(X1,sK60(X1))
| ~ r1(X0,X1) ) ).
cnf(u655,axiom,
( ~ p21(sK161(X1))
| p21(X1)
| ~ r1(X0,X1)
| r1(X1,sK162(X1))
| ~ sP19(X0) ) ).
cnf(u530,axiom,
( ~ sP29(X0)
| p32(X1)
| p31(sK130(X1))
| p31(X1)
| ~ r1(X0,X1) ) ).
cnf(u780,axiom,
( ~ p11(sK192(X1))
| p11(X1)
| r1(X1,sK190(X1))
| ~ r1(X0,X1)
| ~ sP9(X0) ) ).
cnf(u285,axiom,
( ~ p53(sK69(X1))
| p53(X1)
| r1(sK67(X1),sK68(X1))
| ~ r1(X0,X1)
| ~ sP50(X0) ) ).
cnf(u536,axiom,
( ~ sP29(X0)
| p32(X1)
| r1(sK130(X1),sK131(X1))
| p31(X1)
| ~ r1(X0,X1) ) ).
cnf(u415,axiom,
( ~ p42(sK101(X1))
| p42(X1)
| ~ r1(X0,X1)
| r1(X1,sK102(X1))
| ~ sP39(X0) ) ).
cnf(u553,axiom,
( ~ sP28(X0)
| p31(X1)
| r1(X1,sK133(X1))
| r1(X1,sK135(X1))
| ~ r1(X0,X1) ) ).
cnf(u386,axiom,
( ~ sP41(X0)
| p44(X1)
| p43(sK94(X1))
| p43(X1)
| ~ r1(X0,X1) ) ).
cnf(u785,axiom,
( ~ p10(sK194(X1))
| p10(X1)
| ~ r1(X0,X1)
| p9(X1)
| ~ sP8(X0) ) ).
cnf(u799,axiom,
( ~ p9(sK197(X1))
| p9(X1)
| ~ r1(X0,X1)
| r1(X1,sK198(X1))
| ~ sP7(X0) ) ).
cnf(u658,axiom,
( ~ sP19(X0)
| p21(X1)
| r1(sK160(X1),sK161(X1))
| r1(X1,sK162(X1))
| ~ r1(X0,X1) ) ).
cnf(u275,axiom,
( ~ sP51(X0)
| p54(X1)
| r1(X1,sK64(X1))
| p53(X1)
| ~ r1(X0,X1) ) ).
cnf(u1174,negated_conjecture,
~ p15(sK329) ).
cnf(u413,axiom,
( ~ p42(sK101(X1))
| p42(X1)
| ~ r1(X0,X1)
| p41(X1)
| ~ sP39(X0) ) ).
cnf(u664,axiom,
( ~ sP18(X0)
| p20(X1)
| p19(sK163(X1))
| r1(X1,sK165(X1))
| ~ r1(X0,X1) ) ).
cnf(u298,axiom,
( ~ sP49(X0)
| p52(X1)
| r1(sK70(X1),sK71(X1))
| r1(X1,sK72(X1))
| ~ r1(X0,X1) ) ).
cnf(u384,axiom,
( ~ p45(sK93(X1))
| p45(X1)
| r1(X1,sK91(X1))
| ~ r1(X0,X1)
| ~ sP42(X0) ) ).
cnf(u814,axiom,
( ~ sP6(X0)
| p8(X1)
| r1(sK199(X1),sK200(X1))
| r1(X1,sK201(X1))
| ~ r1(X0,X1) ) ).
cnf(u820,axiom,
( ~ sP5(X0)
| p7(X1)
| p6(sK202(X1))
| r1(X1,sK204(X1))
| ~ r1(X0,X1) ) ).
cnf(u1172,negated_conjecture,
r1(sK220,sK330) ).
cnf(u403,axiom,
( ~ p43(sK98(X1))
| p43(X1)
| ~ r1(X0,X1)
| r1(X1,sK99(X1))
| ~ sP40(X0) ) ).
cnf(u557,axiom,
( ~ p29(sK137(X1))
| p29(X1)
| ~ r1(X0,X1)
| p28(X1)
| ~ sP27(X0) ) ).
cnf(u296,axiom,
( ~ sP49(X0)
| p52(X1)
| r1(sK70(X1),sK71(X1))
| p51(X1)
| ~ r1(X0,X1) ) ).
cnf(u426,axiom,
( ~ p41(sK105(X1))
| p41(X1)
| ~ p41(sK104(X1))
| ~ r1(X0,X1)
| ~ sP38(X0) ) ).
cnf(u825,axiom,
( ~ p7(sK204(X1))
| p7(X1)
| r1(sK202(X1),sK203(X1))
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u555,axiom,
( ~ p29(sK138(X1))
| p29(X1)
| p28(sK136(X1))
| ~ r1(X0,X1)
| ~ sP27(X0) ) ).
cnf(u315,axiom,
( ~ p50(sK78(X1))
| p50(X1)
| p49(sK76(X1))
| ~ r1(X0,X1)
| ~ sP47(X0) ) ).
cnf(u668,axiom,
( ~ sP18(X0)
| p20(X1)
| r1(sK163(X1),sK164(X1))
| p19(X1)
| ~ r1(X0,X1) ) ).
cnf(u302,axiom,
( ~ sP48(X0)
| p51(X1)
| p50(sK73(X1))
| p50(X1)
| ~ r1(X0,X1) ) ).
cnf(u685,axiom,
( ~ sP17(X0)
| p19(X1)
| r1(X1,sK166(X1))
| r1(X1,sK168(X1))
| ~ r1(X0,X1) ) ).
cnf(u424,axiom,
( ~ sP38(X0)
| p41(X1)
| p40(sK103(X1))
| r1(X1,sK105(X1))
| ~ r1(X0,X1) ) ).
cnf(u683,axiom,
( ~ sP17(X0)
| p19(X1)
| r1(X1,sK166(X1))
| p18(X1)
| ~ r1(X0,X1) ) ).
cnf(u574,axiom,
( ~ sP26(X0)
| p28(X1)
| r1(sK139(X1),sK140(X1))
| r1(X1,sK141(X1))
| ~ r1(X0,X1) ) ).
cnf(u839,axiom,
( ~ sP4(X0)
| p6(X1)
| r1(X1,sK205(X1))
| p5(X1)
| ~ r1(X0,X1) ) ).
cnf(u313,axiom,
( ~ sP48(X0)
| p51(X1)
| r1(X1,sK73(X1))
| r1(X1,sK75(X1))
| ~ r1(X0,X1) ) ).
cnf(u443,axiom,
( ~ sP37(X0)
| p40(X1)
| r1(X1,sK106(X1))
| p39(X1)
| ~ r1(X0,X1) ) ).
cnf(u430,axiom,
( ~ sP38(X0)
| p41(X1)
| r1(sK103(X1),sK104(X1))
| r1(X1,sK105(X1))
| ~ r1(X0,X1) ) ).
cnf(u827,axiom,
( ~ sP5(X0)
| p7(X1)
| r1(X1,sK202(X1))
| p6(X1)
| ~ r1(X0,X1) ) ).
cnf(u702,axiom,
( ~ p17(sK174(X1))
| p17(X1)
| ~ p17(sK173(X1))
| ~ r1(X0,X1)
| ~ sP15(X0) ) ).
cnf(u615,axiom,
( ~ p24(sK153(X1))
| p24(X1)
| p23(sK151(X1))
| ~ r1(X0,X1)
| ~ sP22(X0) ) ).
cnf(u441,axiom,
( ~ p40(sK108(X1))
| p40(X1)
| r1(sK106(X1),sK107(X1))
| ~ r1(X0,X1)
| ~ sP37(X0) ) ).
cnf(u580,axiom,
( ~ sP25(X0)
| p27(X1)
| p26(sK142(X1))
| r1(X1,sK144(X1))
| ~ r1(X0,X1) ) ).
cnf(u597,axiom,
( ~ p26(sK147(X1))
| p26(X1)
| r1(sK145(X1),sK146(X1))
| ~ r1(X0,X1)
| ~ sP24(X0) ) ).
cnf(u336,axiom,
( ~ p49(sK81(X1))
| p49(X1)
| r1(X1,sK79(X1))
| ~ r1(X0,X1)
| ~ sP46(X0) ) ).
cnf(u595,axiom,
( ~ p26(sK146(X1))
| p26(X1)
| ~ r1(X0,X1)
| r1(X1,sK147(X1))
| ~ sP24(X0) ) ).
cnf(u708,axiom,
( ~ p17(sK174(X1))
| p17(X1)
| r1(X1,sK172(X1))
| ~ r1(X0,X1)
| ~ sP15(X0) ) ).
cnf(u342,axiom,
( ~ p48(sK84(X1))
| p48(X1)
| ~ p48(sK83(X1))
| ~ r1(X0,X1)
| ~ sP45(X0) ) ).
cnf(u725,axiom,
( ~ p15(sK179(X1))
| p15(X1)
| ~ r1(X0,X1)
| p14(X1)
| ~ sP13(X0) ) ).
cnf(u842,axiom,
( ~ sP3(X0)
| p5(X1)
| p4(sK208(X1))
| p4(X1)
| ~ r1(X0,X1) ) ).
cnf(u614,axiom,
( ~ sP22(X0)
| p24(X1)
| p23(sK151(X1))
| p23(X1)
| ~ r1(X0,X1) ) ).
cnf(u848,axiom,
( ~ sP3(X0)
| p5(X1)
| r1(sK208(X1),sK209(X1))
| p4(X1)
| ~ r1(X0,X1) ) ).
cnf(u353,axiom,
( ~ p47(sK86(X1))
| p47(X1)
| ~ r1(X0,X1)
| p46(X1)
| ~ sP44(X0) ) ).
cnf(u620,axiom,
( ~ sP22(X0)
| p24(X1)
| r1(sK151(X1),sK152(X1))
| p23(X1)
| ~ r1(X0,X1) ) ).
cnf(u340,axiom,
( ~ sP45(X0)
| p48(X1)
| p47(sK82(X1))
| r1(X1,sK84(X1))
| ~ r1(X0,X1) ) ).
cnf(u470,axiom,
( ~ sP34(X0)
| p37(X1)
| p36(sK115(X1))
| p36(X1)
| ~ r1(X0,X1) ) ).
cnf(u869,axiom,
( ~ p3(sK215(X1))
| p3(X1)
| ~ r1(X0,X1)
| p2(X1)
| ~ sP1(X0) ) ).
cnf(u599,axiom,
( ~ sP24(X0)
| p26(X1)
| r1(X1,sK145(X1))
| p25(X1)
| ~ r1(X0,X1) ) ).
cnf(u867,axiom,
( ~ p3(sK216(X1))
| p3(X1)
| p2(sK214(X1))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u742,axiom,
( ~ sP12(X0)
| p14(X1)
| r1(sK181(X1),sK182(X1))
| r1(X1,sK183(X1))
| ~ r1(X0,X1) ) ).
cnf(u359,axiom,
( ~ sP44(X0)
| p47(X1)
| r1(X1,sK85(X1))
| p46(X1)
| ~ r1(X0,X1) ) ).
cnf(u481,axiom,
( ~ sP34(X0)
| p37(X1)
| r1(X1,sK115(X1))
| r1(X1,sK117(X1))
| ~ r1(X0,X1) ) ).
cnf(u713,axiom,
( ~ p16(sK176(X1))
| p16(X1)
| ~ r1(X0,X1)
| p15(X1)
| ~ sP14(X0) ) ).
cnf(u468,axiom,
( ~ p38(sK114(X1))
| p38(X1)
| r1(X1,sK112(X1))
| ~ r1(X0,X1)
| ~ sP35(X0) ) ).
cnf(u882,axiom,
( ~ p2(sK219(X1))
| p2(X1)
| ~ p2(sK218(X1))
| ~ r1(X0,X1)
| ~ sP0(X0) ) ).
cnf(u727,axiom,
( ~ p15(sK179(X1))
| p15(X1)
| ~ r1(X0,X1)
| r1(X1,sK180(X1))
| ~ sP13(X0) ) ).
cnf(u602,axiom,
( ~ sP23(X0)
| p25(X1)
| p24(sK148(X1))
| p24(X1)
| ~ r1(X0,X1) ) ).
cnf(u759,axiom,
( ~ p12(sK189(X1))
| p12(X1)
| p11(sK187(X1))
| ~ r1(X0,X1)
| ~ sP10(X0) ) ).
cnf(u888,axiom,
( ~ p2(sK219(X1))
| p2(X1)
| r1(X1,sK217(X1))
| ~ r1(X0,X1)
| ~ sP0(X0) ) ).
cnf(u357,axiom,
( ~ p47(sK87(X1))
| p47(X1)
| r1(sK85(X1),sK86(X1))
| ~ r1(X0,X1)
| ~ sP44(X0) ) ).
cnf(u608,axiom,
( ~ sP23(X0)
| p25(X1)
| r1(sK148(X1),sK149(X1))
| p24(X1)
| ~ r1(X0,X1) ) ).
cnf(u487,axiom,
( ~ p36(sK119(X1))
| p36(X1)
| ~ r1(X0,X1)
| r1(X1,sK120(X1))
| ~ sP33(X0) ) ).
cnf(u625,axiom,
( ~ sP22(X0)
| p24(X1)
| r1(X1,sK151(X1))
| r1(X1,sK153(X1))
| ~ r1(X0,X1) ) ).
cnf(u380,axiom,
( ~ sP42(X0)
| p45(X1)
| r1(sK91(X1),sK92(X1))
| p44(X1)
| ~ r1(X0,X1) ) ).
cnf(u230,axiom,
( ~ sP54(X0)
| p57(X1)
| p56(sK55(X1))
| p56(X1)
| ~ r1(X0,X1) ) ).
cnf(u639,axiom,
( ~ p22(sK159(X1))
| p22(X1)
| p21(sK157(X1))
| ~ r1(X0,X1)
| ~ sP20(X0) ) ).
cnf(u730,axiom,
( ~ sP13(X0)
| p15(X1)
| r1(sK178(X1),sK179(X1))
| r1(X1,sK180(X1))
| ~ r1(X0,X1) ) ).
cnf(u253,axiom,
( ~ sP53(X0)
| p56(X1)
| r1(X1,sK58(X1))
| r1(X1,sK60(X1))
| ~ r1(X0,X1) ) ).
cnf(u271,axiom,
( ~ p54(sK65(X1))
| p54(X1)
| ~ r1(X0,X1)
| r1(X1,sK66(X1))
| ~ sP51(X0) ) ).
cnf(u485,axiom,
( ~ p36(sK119(X1))
| p36(X1)
| ~ r1(X0,X1)
| p35(X1)
| ~ sP33(X0) ) ).
cnf(u736,axiom,
( ~ sP12(X0)
| p14(X1)
| p13(sK181(X1))
| r1(X1,sK183(X1))
| ~ r1(X0,X1) ) ).
cnf(u370,axiom,
( ~ sP43(X0)
| p46(X1)
| r1(sK88(X1),sK89(X1))
| r1(X1,sK90(X1))
| ~ r1(X0,X1) ) ).
cnf(u753,axiom,
( ~ p13(sK186(X1))
| p13(X1)
| r1(sK184(X1),sK185(X1))
| ~ r1(X0,X1)
| ~ sP11(X0) ) ).
cnf(u508,axiom,
( ~ sP31(X0)
| p34(X1)
| p33(sK124(X1))
| r1(X1,sK126(X1))
| ~ r1(X0,X1) ) ).
cnf(u886,axiom,
( ~ sP0(X0)
| p2(X1)
| r1(sK217(X1),sK218(X1))
| r1(X1,sK219(X1))
| ~ r1(X0,X1) ) ).
cnf(u767,axiom,
( ~ sP10(X0)
| p12(X1)
| r1(X1,sK187(X1))
| p11(X1)
| ~ r1(X0,X1) ) ).
cnf(u514,axiom,
( ~ sP31(X0)
| p34(X1)
| r1(sK124(X1),sK125(X1))
| r1(X1,sK126(X1))
| ~ r1(X0,X1) ) ).
cnf(u243,axiom,
( ~ p56(sK60(X1))
| p56(X1)
| p55(sK58(X1))
| ~ r1(X0,X1)
| ~ sP53(X0) ) ).
cnf(u449,axiom,
( ~ p39(sK110(X1))
| p39(X1)
| ~ r1(X0,X1)
| p38(X1)
| ~ sP36(X0) ) ).
cnf(u269,axiom,
( ~ p54(sK65(X1))
| p54(X1)
| ~ r1(X0,X1)
| p53(X1)
| ~ sP51(X0) ) ).
cnf(u520,axiom,
( ~ sP30(X0)
| p33(X1)
| p32(sK127(X1))
| r1(X1,sK129(X1))
| ~ r1(X0,X1) ) ).
cnf(u399,axiom,
( ~ p43(sK99(X1))
| p43(X1)
| p42(sK97(X1))
| ~ r1(X0,X1)
| ~ sP40(X0) ) ).
cnf(u498,axiom,
( ~ p35(sK123(X1))
| p35(X1)
| ~ p35(sK122(X1))
| ~ r1(X0,X1)
| ~ sP32(X0) ) ).
cnf(u769,axiom,
( ~ sP10(X0)
| p12(X1)
| r1(X1,sK187(X1))
| r1(X1,sK189(X1))
| ~ r1(X0,X1) ) ).
cnf(u783,axiom,
( ~ p10(sK195(X1))
| p10(X1)
| p9(sK193(X1))
| ~ r1(X0,X1)
| ~ sP8(X0) ) ).
cnf(u642,axiom,
( ~ p22(sK159(X1))
| p22(X1)
| ~ p22(sK158(X1))
| ~ r1(X0,X1)
| ~ sP20(X0) ) ).
cnf(u241,axiom,
( ~ sP54(X0)
| p57(X1)
| r1(X1,sK55(X1))
| r1(X1,sK57(X1))
| ~ r1(X0,X1) ) ).
cnf(u259,axiom,
( ~ p55(sK62(X1))
| p55(X1)
| ~ r1(X0,X1)
| r1(X1,sK63(X1))
| ~ sP52(X0) ) ).
cnf(u397,axiom,
( ~ sP41(X0)
| p44(X1)
| r1(X1,sK94(X1))
| r1(X1,sK96(X1))
| ~ r1(X0,X1) ) ).
cnf(u648,axiom,
( ~ p22(sK159(X1))
| p22(X1)
| r1(X1,sK157(X1))
| ~ r1(X0,X1)
| ~ sP20(X0) ) ).
cnf(u282,axiom,
( ~ p53(sK69(X1))
| p53(X1)
| ~ p53(sK68(X1))
| ~ r1(X0,X1)
| ~ sP50(X0) ) ).
cnf(u496,axiom,
( ~ sP32(X0)
| p35(X1)
| p34(sK121(X1))
| r1(X1,sK123(X1))
| ~ r1(X0,X1) ) ).
cnf(u798,axiom,
( ~ p9(sK198(X1))
| p9(X1)
| ~ p9(sK197(X1))
| ~ r1(X0,X1)
| ~ sP7(X0) ) ).
cnf(u804,axiom,
( ~ p9(sK198(X1))
| p9(X1)
| r1(X1,sK196(X1))
| ~ r1(X0,X1)
| ~ sP7(X0) ) ).
cnf(u309,axiom,
( ~ p51(sK75(X1))
| p51(X1)
| r1(sK73(X1),sK74(X1))
| ~ r1(X0,X1)
| ~ sP48(X0) ) ).
cnf(u387,axiom,
( ~ p44(sK96(X1))
| p44(X1)
| p43(sK94(X1))
| ~ r1(X0,X1)
| ~ sP41(X0) ) ).
cnf(u541,axiom,
( ~ sP29(X0)
| p32(X1)
| r1(X1,sK130(X1))
| r1(X1,sK132(X1))
| ~ r1(X0,X1) ) ).
cnf(u280,axiom,
( ~ sP50(X0)
| p53(X1)
| p52(sK67(X1))
| r1(X1,sK69(X1))
| ~ r1(X0,X1) ) ).
cnf(u809,axiom,
( ~ p8(sK200(X1))
| p8(X1)
| ~ r1(X0,X1)
| p7(X1)
| ~ sP6(X0) ) ).
cnf(u1171,negated_conjecture,
~ p15(sK330) ).
cnf(u823,axiom,
( ~ p7(sK203(X1))
| p7(X1)
| ~ r1(X0,X1)
| r1(X1,sK204(X1))
| ~ sP5(X0) ) ).
cnf(u299,axiom,
( ~ sP49(X0)
| p52(X1)
| r1(X1,sK70(X1))
| p51(X1)
| ~ r1(X0,X1) ) ).
cnf(u652,axiom,
( ~ sP19(X0)
| p21(X1)
| p20(sK160(X1))
| r1(X1,sK162(X1))
| ~ r1(X0,X1) ) ).
cnf(u286,axiom,
( ~ sP50(X0)
| p53(X1)
| r1(sK67(X1),sK68(X1))
| r1(X1,sK69(X1))
| ~ r1(X0,X1) ) ).
cnf(u669,axiom,
( ~ p20(sK165(X1))
| p20(X1)
| r1(sK163(X1),sK164(X1))
| ~ r1(X0,X1)
| ~ sP18(X0) ) ).
cnf(u408,axiom,
( ~ p43(sK99(X1))
| p43(X1)
| r1(X1,sK97(X1))
| ~ r1(X0,X1)
| ~ sP40(X0) ) ).
cnf(u532,axiom,
( ~ sP29(X0)
| p32(X1)
| p31(sK130(X1))
| r1(X1,sK132(X1))
| ~ r1(X0,X1) ) ).
cnf(u667,axiom,
( ~ p20(sK164(X1))
| p20(X1)
| ~ r1(X0,X1)
| r1(X1,sK165(X1))
| ~ sP18(X0) ) ).
cnf(u558,axiom,
( ~ p29(sK138(X1))
| p29(X1)
| ~ p29(sK137(X1))
| ~ r1(X0,X1)
| ~ sP27(X0) ) ).
cnf(u297,axiom,
( ~ p52(sK72(X1))
| p52(X1)
| r1(sK70(X1),sK71(X1))
| ~ r1(X0,X1)
| ~ sP49(X0) ) ).
cnf(u564,axiom,
( ~ p29(sK138(X1))
| p29(X1)
| r1(X1,sK136(X1))
| ~ r1(X0,X1)
| ~ sP27(X0) ) ).
cnf(u427,axiom,
( ~ p41(sK104(X1))
| p41(X1)
| ~ r1(X0,X1)
| r1(X1,sK105(X1))
| ~ sP38(X0) ) ).
cnf(u813,axiom,
( ~ p8(sK201(X1))
| p8(X1)
| r1(sK199(X1),sK200(X1))
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u811,axiom,
( ~ p8(sK200(X1))
| p8(X1)
| ~ r1(X0,X1)
| r1(X1,sK201(X1))
| ~ sP6(X0) ) ).
cnf(u686,axiom,
( ~ sP16(X0)
| p18(X1)
| p17(sK169(X1))
| p17(X1)
| ~ r1(X0,X1) ) ).
cnf(u425,axiom,
( ~ p41(sK104(X1))
| p41(X1)
| ~ r1(X0,X1)
| p40(X1)
| ~ sP38(X0) ) ).
cnf(u692,axiom,
( ~ sP16(X0)
| p18(X1)
| r1(sK169(X1),sK170(X1))
| p17(X1)
| ~ r1(X0,X1) ) ).
cnf(u581,axiom,
( ~ p27(sK143(X1))
| p27(X1)
| ~ r1(X0,X1)
| p26(X1)
| ~ sP25(X0) ) ).
cnf(u320,axiom,
( ~ sP47(X0)
| p50(X1)
| r1(sK76(X1),sK77(X1))
| p49(X1)
| ~ r1(X0,X1) ) ).
cnf(u826,axiom,
( ~ sP5(X0)
| p7(X1)
| r1(sK202(X1),sK203(X1))
| r1(X1,sK204(X1))
| ~ r1(X0,X1) ) ).
cnf(u579,axiom,
( ~ p27(sK144(X1))
| p27(X1)
| p26(sK142(X1))
| ~ r1(X0,X1)
| ~ sP25(X0) ) ).
cnf(u326,axiom,
( ~ sP46(X0)
| p49(X1)
| p48(sK79(X1))
| p48(X1)
| ~ r1(X0,X1) ) ).
cnf(u709,axiom,
( ~ sP15(X0)
| p17(X1)
| r1(X1,sK172(X1))
| r1(X1,sK174(X1))
| ~ r1(X0,X1) ) ).
cnf(u598,axiom,
( ~ sP24(X0)
| p26(X1)
| r1(sK145(X1),sK146(X1))
| r1(X1,sK147(X1))
| ~ r1(X0,X1) ) ).
cnf(u832,axiom,
( ~ sP4(X0)
| p6(X1)
| p5(sK205(X1))
| r1(X1,sK207(X1))
| ~ r1(X0,X1) ) ).
cnf(u337,axiom,
( ~ sP46(X0)
| p49(X1)
| r1(X1,sK79(X1))
| r1(X1,sK81(X1))
| ~ r1(X0,X1) ) ).
cnf(u604,axiom,
( ~ sP23(X0)
| p25(X1)
| p24(sK148(X1))
| r1(X1,sK150(X1))
| ~ r1(X0,X1) ) ).
cnf(u697,axiom,
( ~ sP16(X0)
| p18(X1)
| r1(X1,sK169(X1))
| r1(X1,sK171(X1))
| ~ r1(X0,X1) ) ).
cnf(u324,axiom,
( ~ p50(sK78(X1))
| p50(X1)
| r1(X1,sK76(X1))
| ~ r1(X0,X1)
| ~ sP47(X0) ) ).
cnf(u454,axiom,
( ~ sP36(X0)
| p39(X1)
| r1(sK109(X1),sK110(X1))
| r1(X1,sK111(X1))
| ~ r1(X0,X1) ) ).
cnf(u853,axiom,
( ~ sP3(X0)
| p5(X1)
| r1(X1,sK208(X1))
| r1(X1,sK210(X1))
| ~ r1(X0,X1) ) ).
cnf(u822,axiom,
( ~ p7(sK204(X1))
| p7(X1)
| ~ p7(sK203(X1))
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u828,axiom,
( ~ p7(sK204(X1))
| p7(X1)
| r1(X1,sK202(X1))
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u583,axiom,
( ~ p27(sK143(X1))
| p27(X1)
| ~ r1(X0,X1)
| r1(X1,sK144(X1))
| ~ sP25(X0) ) ).
cnf(u726,axiom,
( ~ p15(sK180(X1))
| p15(X1)
| ~ p15(sK179(X1))
| ~ r1(X0,X1)
| ~ sP13(X0) ) ).
cnf(u343,axiom,
( ~ p48(sK83(X1))
| p48(X1)
| ~ r1(X0,X1)
| r1(X1,sK84(X1))
| ~ sP45(X0) ) ).
cnf(u465,axiom,
( ~ p38(sK114(X1))
| p38(X1)
| r1(sK112(X1),sK113(X1))
| ~ r1(X0,X1)
| ~ sP35(X0) ) ).
cnf(u452,axiom,
( ~ sP36(X0)
| p39(X1)
| r1(sK109(X1),sK110(X1))
| p38(X1)
| ~ r1(X0,X1) ) ).
cnf(u866,axiom,
( ~ sP1(X0)
| p3(X1)
| p2(sK214(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u711,axiom,
( ~ p16(sK177(X1))
| p16(X1)
| p15(sK175(X1))
| ~ r1(X0,X1)
| ~ sP14(X0) ) ).
cnf(u586,axiom,
( ~ sP25(X0)
| p27(X1)
| r1(sK142(X1),sK143(X1))
| r1(X1,sK144(X1))
| ~ r1(X0,X1) ) ).
cnf(u872,axiom,
( ~ sP1(X0)
| p3(X1)
| r1(sK214(X1),sK215(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u341,axiom,
( ~ p48(sK83(X1))
| p48(X1)
| ~ r1(X0,X1)
| p47(X1)
| ~ sP45(X0) ) ).
cnf(u592,axiom,
( ~ sP24(X0)
| p26(X1)
| p25(sK145(X1))
| r1(X1,sK147(X1))
| ~ r1(X0,X1) ) ).
cnf(u471,axiom,
( ~ p37(sK117(X1))
| p37(X1)
| p36(sK115(X1))
| ~ r1(X0,X1)
| ~ sP34(X0) ) ).
cnf(u609,axiom,
( ~ p25(sK150(X1))
| p25(X1)
| r1(sK148(X1),sK149(X1))
| ~ r1(X0,X1)
| ~ sP23(X0) ) ).
cnf(u364,axiom,
( ~ sP43(X0)
| p46(X1)
| p45(sK88(X1))
| r1(X1,sK90(X1))
| ~ r1(X0,X1) ) ).
cnf(u623,axiom,
( ~ sP22(X0)
| p24(X1)
| r1(X1,sK151(X1))
| p23(X1)
| ~ r1(X0,X1) ) ).
cnf(u714,axiom,
( ~ p16(sK177(X1))
| p16(X1)
| ~ p16(sK176(X1))
| ~ r1(X0,X1)
| ~ sP14(X0) ) ).
cnf(u237,axiom,
( ~ p57(sK57(X1))
| p57(X1)
| r1(sK55(X1),sK56(X1))
| ~ r1(X0,X1)
| ~ sP54(X0) ) ).
cnf(u383,axiom,
( ~ sP42(X0)
| p45(X1)
| r1(X1,sK91(X1))
| p44(X1)
| ~ r1(X0,X1) ) ).
cnf(u469,axiom,
( ~ sP35(X0)
| p38(X1)
| r1(X1,sK112(X1))
| r1(X1,sK114(X1))
| ~ r1(X0,X1) ) ).
cnf(u720,axiom,
( ~ p16(sK177(X1))
| p16(X1)
| r1(X1,sK175(X1))
| ~ r1(X0,X1)
| ~ sP14(X0) ) ).
cnf(u354,axiom,
( ~ p47(sK87(X1))
| p47(X1)
| ~ p47(sK86(X1))
| ~ r1(X0,X1)
| ~ sP44(X0) ) ).
cnf(u737,axiom,
( ~ p14(sK182(X1))
| p14(X1)
| ~ r1(X0,X1)
| p13(X1)
| ~ sP12(X0) ) ).
cnf(u492,axiom,
( ~ p36(sK120(X1))
| p36(X1)
| r1(X1,sK118(X1))
| ~ r1(X0,X1)
| ~ sP33(X0) ) ).
cnf(u870,axiom,
( ~ p3(sK216(X1))
| p3(X1)
| ~ p3(sK215(X1))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u751,axiom,
( ~ p13(sK185(X1))
| p13(X1)
| ~ r1(X0,X1)
| r1(X1,sK186(X1))
| ~ sP11(X0) ) ).
cnf(u626,axiom,
( ~ sP21(X0)
| p23(X1)
| p22(sK154(X1))
| p22(X1)
| ~ r1(X0,X1) ) ).
cnf(u876,axiom,
( ~ p3(sK216(X1))
| p3(X1)
| r1(X1,sK214(X1))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u381,axiom,
( ~ p45(sK93(X1))
| p45(X1)
| r1(sK91(X1),sK92(X1))
| ~ r1(X0,X1)
| ~ sP42(X0) ) ).
cnf(u632,axiom,
( ~ sP21(X0)
| p23(X1)
| r1(sK154(X1),sK155(X1))
| p22(X1)
| ~ r1(X0,X1) ) ).
cnf(u511,axiom,
( ~ p34(sK125(X1))
| p34(X1)
| ~ r1(X0,X1)
| r1(X1,sK126(X1))
| ~ sP31(X0) ) ).
cnf(u482,axiom,
( ~ sP33(X0)
| p36(X1)
| p35(sK118(X1))
| p35(X1)
| ~ r1(X0,X1) ) ).
cnf(u881,axiom,
( ~ p2(sK218(X1))
| p2(X1)
| ~ r1(X0,X1)
| p1(X1)
| ~ sP0(X0) ) ).
cnf(u459,axiom,
( ~ p38(sK114(X1))
| p38(X1)
| p37(sK112(X1))
| ~ r1(X0,X1)
| ~ sP35(X0) ) ).
cnf(u254,axiom,
( ~ sP52(X0)
| p55(X1)
| p54(sK61(X1))
| p54(X1)
| ~ r1(X0,X1) ) ).
cnf(u754,axiom,
( ~ sP11(X0)
| p13(X1)
| r1(sK184(X1),sK185(X1))
| r1(X1,sK186(X1))
| ~ r1(X0,X1) ) ).
cnf(u371,axiom,
( ~ sP43(X0)
| p46(X1)
| r1(X1,sK88(X1))
| p45(X1)
| ~ r1(X0,X1) ) ).
cnf(u509,axiom,
( ~ p34(sK125(X1))
| p34(X1)
| ~ r1(X0,X1)
| p33(X1)
| ~ sP31(X0) ) ).
cnf(u760,axiom,
( ~ sP10(X0)
| p12(X1)
| p11(sK187(X1))
| r1(X1,sK189(X1))
| ~ r1(X0,X1) ) ).
cnf(u266,axiom,
( ~ sP51(X0)
| p54(X1)
| p53(sK64(X1))
| p53(X1)
| ~ r1(X0,X1) ) ).
cnf(u480,axiom,
( ~ p37(sK117(X1))
| p37(X1)
| r1(X1,sK115(X1))
| ~ r1(X0,X1)
| ~ sP34(X0) ) ).
cnf(u252,axiom,
( ~ p56(sK60(X1))
| p56(X1)
| r1(X1,sK58(X1))
| ~ r1(X0,X1)
| ~ sP53(X0) ) ).
cnf(u782,axiom,
( ~ sP8(X0)
| p10(X1)
| p9(sK193(X1))
| p9(X1)
| ~ r1(X0,X1) ) ).
cnf(u788,axiom,
( ~ sP8(X0)
| p10(X1)
| r1(sK193(X1),sK194(X1))
| p9(X1)
| ~ r1(X0,X1) ) ).
cnf(u499,axiom,
( ~ p35(sK122(X1))
| p35(X1)
| ~ r1(X0,X1)
| r1(X1,sK123(X1))
| ~ sP32(X0) ) ).
cnf(u525,axiom,
( ~ p33(sK129(X1))
| p33(X1)
| r1(sK127(X1),sK128(X1))
| ~ r1(X0,X1)
| ~ sP30(X0) ) ).
cnf(u264,axiom,
( ~ p55(sK63(X1))
| p55(X1)
| r1(X1,sK61(X1))
| ~ r1(X0,X1)
| ~ sP52(X0) ) ).
cnf(u394,axiom,
( ~ sP41(X0)
| p44(X1)
| r1(sK94(X1),sK95(X1))
| r1(X1,sK96(X1))
| ~ r1(X0,X1) ) ).
cnf(u793,axiom,
( ~ sP8(X0)
| p10(X1)
| r1(X1,sK193(X1))
| r1(X1,sK195(X1))
| ~ r1(X0,X1) ) ).
cnf(u242,axiom,
( ~ sP53(X0)
| p56(X1)
| p55(sK58(X1))
| p55(X1)
| ~ r1(X0,X1) ) ).
cnf(u523,axiom,
( ~ p33(sK128(X1))
| p33(X1)
| ~ r1(X0,X1)
| r1(X1,sK129(X1))
| ~ sP30(X0) ) ).
cnf(u807,axiom,
( ~ p8(sK201(X1))
| p8(X1)
| p7(sK199(X1))
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u283,axiom,
( ~ p53(sK68(X1))
| p53(X1)
| ~ r1(X0,X1)
| r1(X1,sK69(X1))
| ~ sP50(X0) ) ).
cnf(u764,axiom,
( ~ sP10(X0)
| p12(X1)
| r1(sK187(X1),sK188(X1))
| p11(X1)
| ~ r1(X0,X1) ) ).
cnf(u270,axiom,
( ~ p54(sK66(X1))
| p54(X1)
| ~ p54(sK65(X1))
| ~ r1(X0,X1)
| ~ sP51(X0) ) ).
cnf(u653,axiom,
( ~ p21(sK161(X1))
| p21(X1)
| ~ r1(X0,X1)
| p20(X1)
| ~ sP19(X0) ) ).
cnf(u392,axiom,
( ~ sP41(X0)
| p44(X1)
| r1(sK94(X1),sK95(X1))
| p43(X1)
| ~ r1(X0,X1) ) ).
cnf(u1175,negated_conjecture,
r1(sK220,sK329) ).
cnf(u651,axiom,
( ~ p21(sK162(X1))
| p21(X1)
| p20(sK160(X1))
| ~ r1(X0,X1)
| ~ sP19(X0) ) ).
cnf(u542,axiom,
( ~ sP28(X0)
| p31(X1)
| p30(sK133(X1))
| p30(X1)
| ~ r1(X0,X1) ) ).
cnf(u281,axiom,
( ~ p53(sK68(X1))
| p53(X1)
| ~ r1(X0,X1)
| p52(X1)
| ~ sP50(X0) ) ).
cnf(u548,axiom,
( ~ sP28(X0)
| p31(X1)
| r1(sK133(X1),sK134(X1))
| p30(X1)
| ~ r1(X0,X1) ) ).
cnf(u411,axiom,
( ~ p42(sK102(X1))
| p42(X1)
| p41(sK100(X1))
| ~ r1(X0,X1)
| ~ sP39(X0) ) ).
cnf(u565,axiom,
( ~ sP27(X0)
| p29(X1)
| r1(X1,sK136(X1))
| r1(X1,sK138(X1))
| ~ r1(X0,X1) ) ).
cnf(u304,axiom,
( ~ sP48(X0)
| p51(X1)
| p50(sK73(X1))
| r1(X1,sK75(X1))
| ~ r1(X0,X1) ) ).
cnf(u398,axiom,
( ~ sP40(X0)
| p43(X1)
| p42(sK97(X1))
| p42(X1)
| ~ r1(X0,X1) ) ).
cnf(u797,axiom,
( ~ p9(sK197(X1))
| p9(X1)
| ~ r1(X0,X1)
| p8(X1)
| ~ sP7(X0) ) ).
cnf(u563,axiom,
( ~ sP27(X0)
| p29(X1)
| r1(X1,sK136(X1))
| p28(X1)
| ~ r1(X0,X1) ) ).
cnf(u795,axiom,
( ~ p9(sK198(X1))
| p9(X1)
| p8(sK196(X1))
| ~ r1(X0,X1)
| ~ sP7(X0) ) ).
cnf(u670,axiom,
( ~ sP18(X0)
| p20(X1)
| r1(sK163(X1),sK164(X1))
| r1(X1,sK165(X1))
| ~ r1(X0,X1) ) ).
cnf(u409,axiom,
( ~ sP40(X0)
| p43(X1)
| r1(X1,sK97(X1))
| r1(X1,sK99(X1))
| ~ r1(X0,X1) ) ).
cnf(u676,axiom,
( ~ sP17(X0)
| p19(X1)
| p18(sK166(X1))
| r1(X1,sK168(X1))
| ~ r1(X0,X1) ) ).
cnf(u310,axiom,
( ~ sP48(X0)
| p51(X1)
| r1(sK73(X1),sK74(X1))
| r1(X1,sK75(X1))
| ~ r1(X0,X1) ) ).
cnf(u693,axiom,
( ~ p18(sK171(X1))
| p18(X1)
| r1(sK169(X1),sK170(X1))
| ~ r1(X0,X1)
| ~ sP16(X0) ) ).
cnf(u810,axiom,
( ~ p8(sK201(X1))
| p8(X1)
| ~ p8(sK200(X1))
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u505,axiom,
( ~ sP32(X0)
| p35(X1)
| r1(X1,sK121(X1))
| r1(X1,sK123(X1))
| ~ r1(X0,X1) ) ).
cnf(u691,axiom,
( ~ p18(sK170(X1))
| p18(X1)
| ~ r1(X0,X1)
| r1(X1,sK171(X1))
| ~ sP16(X0) ) ).
cnf(u789,axiom,
( ~ p10(sK195(X1))
| p10(X1)
| r1(sK193(X1),sK194(X1))
| ~ r1(X0,X1)
| ~ sP8(X0) ) ).
cnf(u750,axiom,
( ~ p13(sK186(X1))
| p13(X1)
| ~ p13(sK185(X1))
| ~ r1(X0,X1)
| ~ sP11(X0) ) ).
cnf(u816,axiom,
( ~ p8(sK201(X1))
| p8(X1)
| r1(X1,sK199(X1))
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u308,axiom,
( ~ sP48(X0)
| p51(X1)
| r1(sK73(X1),sK74(X1))
| p50(X1)
| ~ r1(X0,X1) ) ).
cnf(u438,axiom,
( ~ p40(sK108(X1))
| p40(X1)
| ~ p40(sK107(X1))
| ~ r1(X0,X1)
| ~ sP37(X0) ) ).
cnf(u567,axiom,
( ~ p28(sK141(X1))
| p28(X1)
| p27(sK139(X1))
| ~ r1(X0,X1)
| ~ sP26(X0) ) ).
cnf(u582,axiom,
( ~ p27(sK144(X1))
| p27(X1)
| ~ p27(sK143(X1))
| ~ r1(X0,X1)
| ~ sP25(X0) ) ).
cnf(u321,axiom,
( ~ p50(sK78(X1))
| p50(X1)
| r1(sK76(X1),sK77(X1))
| ~ r1(X0,X1)
| ~ sP47(X0) ) ).
cnf(u588,axiom,
( ~ p27(sK144(X1))
| p27(X1)
| r1(X1,sK142(X1))
| ~ r1(X0,X1)
| ~ sP25(X0) ) ).
cnf(u681,axiom,
( ~ p19(sK168(X1))
| p19(X1)
| r1(sK166(X1),sK167(X1))
| ~ r1(X0,X1)
| ~ sP17(X0) ) ).
cnf(u436,axiom,
( ~ sP37(X0)
| p40(X1)
| p39(sK106(X1))
| r1(X1,sK108(X1))
| ~ r1(X0,X1) ) ).
cnf(u837,axiom,
( ~ p6(sK207(X1))
| p6(X1)
| r1(sK205(X1),sK206(X1))
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u695,axiom,
( ~ sP16(X0)
| p18(X1)
| r1(X1,sK169(X1))
| p17(X1)
| ~ r1(X0,X1) ) ).
cnf(u570,axiom,
( ~ p28(sK141(X1))
| p28(X1)
| ~ p28(sK140(X1))
| ~ r1(X0,X1)
| ~ sP26(X0) ) ).
cnf(u835,axiom,
( ~ p6(sK206(X1))
| p6(X1)
| ~ r1(X0,X1)
| r1(X1,sK207(X1))
| ~ sP4(X0) ) ).
cnf(u710,axiom,
( ~ sP14(X0)
| p16(X1)
| p15(sK175(X1))
| p15(X1)
| ~ r1(X0,X1) ) ).
cnf(u327,axiom,
( ~ p49(sK81(X1))
| p49(X1)
| p48(sK79(X1))
| ~ r1(X0,X1)
| ~ sP46(X0) ) ).
cnf(u850,axiom,
( ~ sP3(X0)
| p5(X1)
| r1(sK208(X1),sK209(X1))
| r1(X1,sK210(X1))
| ~ r1(X0,X1) ) ).
cnf(u698,axiom,
( ~ sP15(X0)
| p17(X1)
| p16(sK172(X1))
| p16(X1)
| ~ r1(X0,X1) ) ).
cnf(u232,axiom,
( ~ sP54(X0)
| p57(X1)
| p56(sK55(X1))
| r1(X1,sK57(X1))
| ~ r1(X0,X1) ) ).
cnf(u856,axiom,
( ~ sP2(X0)
| p4(X1)
| p3(sK211(X1))
| r1(X1,sK213(X1))
| ~ r1(X0,X1) ) ).
cnf(u325,axiom,
( ~ sP47(X0)
| p50(X1)
| r1(X1,sK76(X1))
| r1(X1,sK78(X1))
| ~ r1(X0,X1) ) ).
cnf(u576,axiom,
( ~ p28(sK141(X1))
| p28(X1)
| r1(X1,sK139(X1))
| ~ r1(X0,X1)
| ~ sP26(X0) ) ).
cnf(u455,axiom,
( ~ sP36(X0)
| p39(X1)
| r1(X1,sK109(X1))
| p38(X1)
| ~ r1(X0,X1) ) ).
cnf(u593,axiom,
( ~ p26(sK146(X1))
| p26(X1)
| ~ r1(X0,X1)
| p25(X1)
| ~ sP24(X0) ) ).
cnf(u348,axiom,
( ~ p48(sK84(X1))
| p48(X1)
| r1(X1,sK82(X1))
| ~ r1(X0,X1)
| ~ sP45(X0) ) ).
cnf(u607,axiom,
( ~ p25(sK149(X1))
| p25(X1)
| ~ r1(X0,X1)
| r1(X1,sK150(X1))
| ~ sP23(X0) ) ).
cnf(u367,axiom,
( ~ p46(sK89(X1))
| p46(X1)
| ~ r1(X0,X1)
| r1(X1,sK90(X1))
| ~ sP43(X0) ) ).
cnf(u453,axiom,
( ~ p39(sK111(X1))
| p39(X1)
| r1(sK109(X1),sK110(X1))
| ~ r1(X0,X1)
| ~ sP36(X0) ) ).
cnf(u704,axiom,
( ~ sP15(X0)
| p17(X1)
| r1(sK172(X1),sK173(X1))
| p16(X1)
| ~ r1(X0,X1) ) ).
cnf(u338,axiom,
( ~ sP45(X0)
| p48(X1)
| p47(sK82(X1))
| p47(X1)
| ~ r1(X0,X1) ) ).
cnf(u721,axiom,
( ~ sP14(X0)
| p16(X1)
| r1(X1,sK175(X1))
| r1(X1,sK177(X1))
| ~ r1(X0,X1) ) ).
cnf(u476,axiom,
( ~ sP34(X0)
| p37(X1)
| r1(sK115(X1),sK116(X1))
| p36(X1)
| ~ r1(X0,X1) ) ).
cnf(u854,axiom,
( ~ sP2(X0)
| p4(X1)
| p3(sK211(X1))
| p3(X1)
| ~ r1(X0,X1) ) ).
cnf(u735,axiom,
( ~ p14(sK183(X1))
| p14(X1)
| p13(sK181(X1))
| ~ r1(X0,X1)
| ~ sP12(X0) ) ).
cnf(u610,axiom,
( ~ sP23(X0)
| p25(X1)
| r1(sK148(X1),sK149(X1))
| r1(X1,sK150(X1))
| ~ r1(X0,X1) ) ).
cnf(u406,axiom,
( ~ sP40(X0)
| p43(X1)
| r1(sK97(X1),sK98(X1))
| r1(X1,sK99(X1))
| ~ r1(X0,X1) ) ).
cnf(u365,axiom,
( ~ p46(sK89(X1))
| p46(X1)
| ~ r1(X0,X1)
| p45(X1)
| ~ sP43(X0) ) ).
cnf(u616,axiom,
( ~ sP22(X0)
| p24(X1)
| p23(sK151(X1))
| r1(X1,sK153(X1))
| ~ r1(X0,X1) ) ).
cnf(u466,axiom,
( ~ sP35(X0)
| p38(X1)
| r1(sK112(X1),sK113(X1))
| r1(X1,sK114(X1))
| ~ r1(X0,X1) ) ).
cnf(u238,axiom,
( ~ sP54(X0)
| p57(X1)
| r1(sK55(X1),sK56(X1))
| r1(X1,sK57(X1))
| ~ r1(X0,X1) ) ).
cnf(u861,axiom,
( ~ p4(sK213(X1))
| p4(X1)
| r1(sK211(X1),sK212(X1))
| ~ r1(X0,X1)
| ~ sP2(X0) ) ).
cnf(u879,axiom,
( ~ p2(sK219(X1))
| p2(X1)
| p1(sK217(X1))
| ~ r1(X0,X1)
| ~ sP0(X0) ) ).
cnf(u738,axiom,
( ~ p14(sK183(X1))
| p14(X1)
| ~ p14(sK182(X1))
| ~ r1(X0,X1)
| ~ sP12(X0) ) ).
cnf(u355,axiom,
( ~ p47(sK86(X1))
| p47(X1)
| ~ r1(X0,X1)
| r1(X1,sK87(X1))
| ~ sP44(X0) ) ).
cnf(u493,axiom,
( ~ sP33(X0)
| p36(X1)
| r1(X1,sK118(X1))
| r1(X1,sK120(X1))
| ~ r1(X0,X1) ) ).
cnf(u744,axiom,
( ~ p14(sK183(X1))
| p14(X1)
| r1(X1,sK181(X1))
| ~ r1(X0,X1)
| ~ sP12(X0) ) ).
cnf(u378,axiom,
( ~ p45(sK93(X1))
| p45(X1)
| ~ p45(sK92(X1))
| ~ r1(X0,X1)
| ~ sP42(X0) ) ).
cnf(u464,axiom,
( ~ sP35(X0)
| p38(X1)
| r1(sK112(X1),sK113(X1))
| p37(X1)
| ~ r1(X0,X1) ) ).
cnf(u236,axiom,
( ~ sP54(X0)
| p57(X1)
| r1(sK55(X1),sK56(X1))
| p56(X1)
| ~ r1(X0,X1) ) ).
cnf(u723,axiom,
( ~ p15(sK180(X1))
| p15(X1)
| p14(sK178(X1))
| ~ r1(X0,X1)
| ~ sP13(X0) ) ).
cnf(u772,axiom,
( ~ sP9(X0)
| p11(X1)
| p10(sK190(X1))
| r1(X1,sK192(X1))
| ~ r1(X0,X1) ) ).
cnf(u251,axiom,
( ~ sP53(X0)
| p56(X1)
| r1(X1,sK58(X1))
| p55(X1)
| ~ r1(X0,X1) ) ).
cnf(u483,axiom,
( ~ p36(sK120(X1))
| p36(X1)
| p35(sK118(X1))
| ~ r1(X0,X1)
| ~ sP33(X0) ) ).
cnf(u637,axiom,
( ~ sP21(X0)
| p23(X1)
| r1(X1,sK154(X1))
| r1(X1,sK156(X1))
| ~ r1(X0,X1) ) ).
cnf(u376,axiom,
( ~ sP42(X0)
| p45(X1)
| p44(sK91(X1))
| r1(X1,sK93(X1))
| ~ r1(X0,X1) ) ).
cnf(u506,axiom,
( ~ sP31(X0)
| p34(X1)
| p33(sK124(X1))
| p33(X1)
| ~ r1(X0,X1) ) ).
cnf(u777,axiom,
( ~ p11(sK192(X1))
| p11(X1)
| r1(sK190(X1),sK191(X1))
| ~ r1(X0,X1)
| ~ sP9(X0) ) ).
cnf(u635,axiom,
( ~ sP21(X0)
| p23(X1)
| r1(X1,sK154(X1))
| p22(X1)
| ~ r1(X0,X1) ) ).
cnf(u791,axiom,
( ~ sP8(X0)
| p10(X1)
| r1(X1,sK193(X1))
| p9(X1)
| ~ r1(X0,X1) ) ).
cnf(u249,axiom,
( ~ p56(sK60(X1))
| p56(X1)
| r1(sK58(X1),sK59(X1))
| ~ r1(X0,X1)
| ~ sP53(X0) ) ).
cnf(u267,axiom,
( ~ p54(sK66(X1))
| p54(X1)
| p53(sK64(X1))
| ~ r1(X0,X1)
| ~ sP51(X0) ) ).
cnf(u748,axiom,
( ~ sP11(X0)
| p13(X1)
| p12(sK184(X1))
| r1(X1,sK186(X1))
| ~ r1(X0,X1) ) ).
cnf(u382,axiom,
( ~ sP42(X0)
| p45(X1)
| r1(sK91(X1),sK92(X1))
| r1(X1,sK93(X1))
| ~ r1(X0,X1) ) ).
cnf(u765,axiom,
( ~ p12(sK189(X1))
| p12(X1)
| r1(sK187(X1),sK188(X1))
| ~ r1(X0,X1)
| ~ sP10(X0) ) ).
cnf(u504,axiom,
( ~ p35(sK123(X1))
| p35(X1)
| r1(X1,sK121(X1))
| ~ r1(X0,X1)
| ~ sP32(X0) ) ).
cnf(u763,axiom,
( ~ p12(sK188(X1))
| p12(X1)
| ~ r1(X0,X1)
| r1(X1,sK189(X1))
| ~ sP10(X0) ) ).
cnf(u526,axiom,
( ~ sP30(X0)
| p33(X1)
| r1(sK127(X1),sK128(X1))
| r1(X1,sK129(X1))
| ~ r1(X0,X1) ) ).
cnf(u255,axiom,
( ~ p55(sK63(X1))
| p55(X1)
| p54(sK61(X1))
| ~ r1(X0,X1)
| ~ sP52(X0) ) ).
cnf(u265,axiom,
( ~ sP52(X0)
| p55(X1)
| r1(X1,sK61(X1))
| r1(X1,sK63(X1))
| ~ r1(X0,X1) ) ).
cnf(u395,axiom,
( ~ sP41(X0)
| p44(X1)
| r1(X1,sK94(X1))
| p43(X1)
| ~ r1(X0,X1) ) ).
cnf(u549,axiom,
( ~ p31(sK135(X1))
| p31(X1)
| r1(sK133(X1),sK134(X1))
| ~ r1(X0,X1)
| ~ sP28(X0) ) ).
cnf(u288,axiom,
( ~ p53(sK69(X1))
| p53(X1)
| r1(X1,sK67(X1))
| ~ r1(X0,X1)
| ~ sP50(X0) ) ).
cnf(u510,axiom,
( ~ p34(sK126(X1))
| p34(X1)
| ~ p34(sK125(X1))
| ~ r1(X0,X1)
| ~ sP31(X0) ) ).
cnf(u781,axiom,
( ~ sP9(X0)
| p11(X1)
| r1(X1,sK190(X1))
| r1(X1,sK192(X1))
| ~ r1(X0,X1) ) ).
cnf(u547,axiom,
( ~ p31(sK134(X1))
| p31(X1)
| ~ r1(X0,X1)
| r1(X1,sK135(X1))
| ~ sP28(X0) ) ).
cnf(u779,axiom,
( ~ sP9(X0)
| p11(X1)
| r1(X1,sK190(X1))
| p10(X1)
| ~ r1(X0,X1) ) ).
cnf(u654,axiom,
( ~ p21(sK162(X1))
| p21(X1)
| ~ p21(sK161(X1))
| ~ r1(X0,X1)
| ~ sP19(X0) ) ).
cnf(u393,axiom,
( ~ p44(sK96(X1))
| p44(X1)
| r1(sK94(X1),sK95(X1))
| ~ r1(X0,X1)
| ~ sP41(X0) ) ).
cnf(u660,axiom,
( ~ p21(sK162(X1))
| p21(X1)
| r1(X1,sK160(X1))
| ~ r1(X0,X1)
| ~ sP19(X0) ) ).
cnf(u294,axiom,
( ~ p52(sK72(X1))
| p52(X1)
| ~ p52(sK71(X1))
| ~ r1(X0,X1)
| ~ sP49(X0) ) ).
cnf(u677,axiom,
( ~ p19(sK167(X1))
| p19(X1)
| ~ r1(X0,X1)
| p18(X1)
| ~ sP17(X0) ) ).
cnf(u794,axiom,
( ~ sP7(X0)
| p9(X1)
| p8(sK196(X1))
| p8(X1)
| ~ r1(X0,X1) ) ).
cnf(u675,axiom,
( ~ p19(sK168(X1))
| p19(X1)
| p18(sK166(X1))
| ~ r1(X0,X1)
| ~ sP17(X0) ) ).
cnf(u566,axiom,
( ~ sP26(X0)
| p28(X1)
| p27(sK139(X1))
| p27(X1)
| ~ r1(X0,X1) ) ).
cnf(u800,axiom,
( ~ sP7(X0)
| p9(X1)
| r1(sK196(X1),sK197(X1))
| p8(X1)
| ~ r1(X0,X1) ) ).
cnf(u305,axiom,
( ~ p51(sK74(X1))
| p51(X1)
| ~ r1(X0,X1)
| p50(X1)
| ~ sP48(X0) ) ).
cnf(u572,axiom,
( ~ sP26(X0)
| p28(X1)
| r1(sK139(X1),sK140(X1))
| p27(X1)
| ~ r1(X0,X1) ) ).
cnf(u537,axiom,
( ~ p32(sK132(X1))
| p32(X1)
| r1(sK130(X1),sK131(X1))
| ~ r1(X0,X1)
| ~ sP29(X0) ) ).
cnf(u292,axiom,
( ~ sP49(X0)
| p52(X1)
| p51(sK70(X1))
| r1(X1,sK72(X1))
| ~ r1(X0,X1) ) ).
cnf(u422,axiom,
( ~ sP38(X0)
| p41(X1)
| p40(sK103(X1))
| p40(X1)
| ~ r1(X0,X1) ) ).
cnf(u821,axiom,
( ~ p7(sK203(X1))
| p7(X1)
| ~ r1(X0,X1)
| p6(X1)
| ~ sP5(X0) ) ).
cnf(u551,axiom,
( ~ sP28(X0)
| p31(X1)
| r1(X1,sK133(X1))
| p30(X1)
| ~ r1(X0,X1) ) ).
cnf(u819,axiom,
( ~ p7(sK204(X1))
| p7(X1)
| p6(sK202(X1))
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u694,axiom,
( ~ sP16(X0)
| p18(X1)
| r1(sK169(X1),sK170(X1))
| r1(X1,sK171(X1))
| ~ r1(X0,X1) ) ).
cnf(u771,axiom,
( ~ p11(sK192(X1))
| p11(X1)
| p10(sK190(X1))
| ~ r1(X0,X1)
| ~ sP9(X0) ) ).
cnf(u545,axiom,
( ~ p31(sK134(X1))
| p31(X1)
| ~ r1(X0,X1)
| p30(X1)
| ~ sP28(X0) ) ).
cnf(u495,axiom,
( ~ p35(sK123(X1))
| p35(X1)
| p34(sK121(X1))
| ~ r1(X0,X1)
| ~ sP32(X0) ) ).
cnf(u311,axiom,
( ~ sP48(X0)
| p51(X1)
| r1(X1,sK73(X1))
| p50(X1)
| ~ r1(X0,X1) ) ).
cnf(u433,axiom,
( ~ sP38(X0)
| p41(X1)
| r1(X1,sK103(X1))
| r1(X1,sK105(X1))
| ~ r1(X0,X1) ) ).
cnf(u700,axiom,
( ~ sP15(X0)
| p17(X1)
| p16(sK172(X1))
| r1(X1,sK174(X1))
| ~ r1(X0,X1) ) ).
cnf(u665,axiom,
( ~ p20(sK164(X1))
| p20(X1)
| ~ r1(X0,X1)
| p19(X1)
| ~ sP18(X0) ) ).
cnf(u420,axiom,
( ~ p42(sK102(X1))
| p42(X1)
| r1(X1,sK100(X1))
| ~ r1(X0,X1)
| ~ sP39(X0) ) ).
cnf(u679,axiom,
( ~ p19(sK167(X1))
| p19(X1)
| ~ r1(X0,X1)
| r1(X1,sK168(X1))
| ~ sP17(X0) ) ).
cnf(u554,axiom,
( ~ sP27(X0)
| p29(X1)
| p28(sK136(X1))
| p28(X1)
| ~ r1(X0,X1) ) ).
cnf(u560,axiom,
( ~ sP27(X0)
| p29(X1)
| r1(sK136(X1),sK137(X1))
| p28(X1)
| ~ r1(X0,X1) ) ).
cnf(u439,axiom,
( ~ p40(sK107(X1))
| p40(X1)
| ~ r1(X0,X1)
| r1(X1,sK108(X1))
| ~ sP37(X0) ) ).
cnf(u834,axiom,
( ~ p6(sK207(X1))
| p6(X1)
| ~ p6(sK206(X1))
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u682,axiom,
( ~ sP17(X0)
| p19(X1)
| r1(sK166(X1),sK167(X1))
| r1(X1,sK168(X1))
| ~ r1(X0,X1) ) ).
cnf(u840,axiom,
( ~ p6(sK207(X1))
| p6(X1)
| r1(X1,sK205(X1))
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u437,axiom,
( ~ p40(sK107(X1))
| p40(X1)
| ~ r1(X0,X1)
| p39(X1)
| ~ sP37(X0) ) ).
cnf(u688,axiom,
( ~ sP16(X0)
| p18(X1)
| p17(sK169(X1))
| r1(X1,sK171(X1))
| ~ r1(X0,X1) ) ).
cnf(u577,axiom,
( ~ sP26(X0)
| p28(X1)
| r1(X1,sK139(X1))
| r1(X1,sK141(X1))
| ~ r1(X0,X1) ) ).
cnf(u332,axiom,
( ~ sP46(X0)
| p49(X1)
| r1(sK79(X1),sK80(X1))
| p48(X1)
| ~ r1(X0,X1) ) ).
cnf(u591,axiom,
( ~ p26(sK147(X1))
| p26(X1)
| p25(sK145(X1))
| ~ r1(X0,X1)
| ~ sP24(X0) ) ).
cnf(u351,axiom,
( ~ p47(sK87(X1))
| p47(X1)
| p46(sK85(X1))
| ~ r1(X0,X1)
| ~ sP44(X0) ) ).
cnf(u322,axiom,
( ~ sP47(X0)
| p50(X1)
| r1(sK76(X1),sK77(X1))
| r1(X1,sK78(X1))
| ~ r1(X0,X1) ) ).
cnf(u705,axiom,
( ~ p17(sK174(X1))
| p17(X1)
| r1(sK172(X1),sK173(X1))
| ~ r1(X0,X1)
| ~ sP15(X0) ) ).
cnf(u460,axiom,
( ~ sP35(X0)
| p38(X1)
| p37(sK112(X1))
| r1(X1,sK114(X1))
| ~ r1(X0,X1) ) ).
cnf(u838,axiom,
( ~ sP4(X0)
| p6(X1)
| r1(sK205(X1),sK206(X1))
| r1(X1,sK207(X1))
| ~ r1(X0,X1) ) ).
cnf(u719,axiom,
( ~ sP14(X0)
| p16(X1)
| r1(X1,sK175(X1))
| p15(X1)
| ~ r1(X0,X1) ) ).
cnf(u594,axiom,
( ~ p26(sK147(X1))
| p26(X1)
| ~ p26(sK146(X1))
| ~ r1(X0,X1)
| ~ sP24(X0) ) ).
cnf(u844,axiom,
( ~ sP3(X0)
| p5(X1)
| p4(sK208(X1))
| r1(X1,sK210(X1))
| ~ r1(X0,X1) ) ).
cnf(u349,axiom,
( ~ sP45(X0)
| p48(X1)
| r1(X1,sK82(X1))
| r1(X1,sK84(X1))
| ~ r1(X0,X1) ) ).
cnf(u600,axiom,
( ~ p26(sK147(X1))
| p26(X1)
| r1(X1,sK145(X1))
| ~ r1(X0,X1)
| ~ sP24(X0) ) ).
cnf(u585,axiom,
( ~ p27(sK144(X1))
| p27(X1)
| r1(sK142(X1),sK143(X1))
| ~ r1(X0,X1)
| ~ sP25(X0) ) ).
cnf(u450,axiom,
( ~ p39(sK111(X1))
| p39(X1)
| ~ p39(sK110(X1))
| ~ r1(X0,X1)
| ~ sP36(X0) ) ).
cnf(u849,axiom,
( ~ p5(sK210(X1))
| p5(X1)
| r1(sK208(X1),sK209(X1))
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u863,axiom,
( ~ sP2(X0)
| p4(X1)
| r1(X1,sK211(X1))
| p3(X1)
| ~ r1(X0,X1) ) ).
cnf(u722,axiom,
( ~ sP13(X0)
| p15(X1)
| p14(sK178(X1))
| p14(X1)
| ~ r1(X0,X1) ) ).
cnf(u339,axiom,
( ~ p48(sK84(X1))
| p48(X1)
| p47(sK82(X1))
| ~ r1(X0,X1)
| ~ sP45(X0) ) ).
cnf(u477,axiom,
( ~ p37(sK117(X1))
| p37(X1)
| r1(sK115(X1),sK116(X1))
| ~ r1(X0,X1)
| ~ sP34(X0) ) ).
cnf(u728,axiom,
( ~ sP13(X0)
| p15(X1)
| r1(sK178(X1),sK179(X1))
| p14(X1)
| ~ r1(X0,X1) ) ).
cnf(u362,axiom,
( ~ sP43(X0)
| p46(X1)
| p45(sK88(X1))
| p45(X1)
| ~ r1(X0,X1) ) ).
cnf(u448,axiom,
( ~ sP36(X0)
| p39(X1)
| p38(sK109(X1))
| r1(X1,sK111(X1))
| ~ r1(X0,X1) ) ).
cnf(u878,axiom,
( ~ sP0(X0)
| p2(X1)
| p1(sK217(X1))
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u707,axiom,
( ~ sP15(X0)
| p17(X1)
| r1(X1,sK172(X1))
| p16(X1)
| ~ r1(X0,X1) ) ).
cnf(u884,axiom,
( ~ sP0(X0)
| p2(X1)
| r1(sK217(X1),sK218(X1))
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u235,axiom,
( ~ p57(sK56(X1))
| p57(X1)
| ~ r1(X0,X1)
| r1(X1,sK57(X1))
| ~ sP54(X0) ) ).
cnf(u467,axiom,
( ~ sP35(X0)
| p38(X1)
| r1(X1,sK112(X1))
| p37(X1)
| ~ r1(X0,X1) ) ).
cnf(u621,axiom,
( ~ p24(sK153(X1))
| p24(X1)
| r1(sK151(X1),sK152(X1))
| ~ r1(X0,X1)
| ~ sP22(X0) ) ).
cnf(u360,axiom,
( ~ p47(sK87(X1))
| p47(X1)
| r1(X1,sK85(X1))
| ~ r1(X0,X1)
| ~ sP44(X0) ) ).
cnf(u490,axiom,
( ~ sP33(X0)
| p36(X1)
| r1(sK118(X1),sK119(X1))
| r1(X1,sK120(X1))
| ~ r1(X0,X1) ) ).
cnf(u889,axiom,
( ~ sP0(X0)
| p2(X1)
| r1(X1,sK217(X1))
| r1(X1,sK219(X1))
| ~ r1(X0,X1) ) ).
cnf(u860,axiom,
( ~ sP2(X0)
| p4(X1)
| r1(sK211(X1),sK212(X1))
| p3(X1)
| ~ r1(X0,X1) ) ).
cnf(u619,axiom,
( ~ p24(sK152(X1))
| p24(X1)
| ~ r1(X0,X1)
| r1(X1,sK153(X1))
| ~ sP22(X0) ) ).
cnf(u775,axiom,
( ~ p11(sK191(X1))
| p11(X1)
| ~ r1(X0,X1)
| r1(X1,sK192(X1))
| ~ sP9(X0) ) ).
cnf(u233,axiom,
( ~ p57(sK56(X1))
| p57(X1)
| ~ r1(X0,X1)
| p56(X1)
| ~ sP54(X0) ) ).
cnf(u379,axiom,
( ~ p45(sK92(X1))
| p45(X1)
| ~ r1(X0,X1)
| r1(X1,sK93(X1))
| ~ sP42(X0) ) ).
cnf(u732,axiom,
( ~ p15(sK180(X1))
| p15(X1)
| r1(X1,sK178(X1))
| ~ r1(X0,X1)
| ~ sP13(X0) ) ).
cnf(u366,axiom,
( ~ p46(sK90(X1))
| p46(X1)
| ~ p46(sK89(X1))
| ~ r1(X0,X1)
| ~ sP43(X0) ) ).
cnf(u749,axiom,
( ~ p13(sK185(X1))
| p13(X1)
| ~ r1(X0,X1)
| p12(X1)
| ~ sP11(X0) ) ).
cnf(u488,axiom,
( ~ sP33(X0)
| p36(X1)
| r1(sK118(X1),sK119(X1))
| p35(X1)
| ~ r1(X0,X1) ) ).
cnf(u747,axiom,
( ~ p13(sK186(X1))
| p13(X1)
| p12(sK184(X1))
| ~ r1(X0,X1)
| ~ sP11(X0) ) ).
cnf(u638,axiom,
( ~ sP20(X0)
| p22(X1)
| p21(sK157(X1))
| p21(X1)
| ~ r1(X0,X1) ) ).
cnf(u239,axiom,
( ~ sP54(X0)
| p57(X1)
| r1(X1,sK55(X1))
| p56(X1)
| ~ r1(X0,X1) ) ).
cnf(u377,axiom,
( ~ p45(sK92(X1))
| p45(X1)
| ~ r1(X0,X1)
| p44(X1)
| ~ sP42(X0) ) ).
cnf(u516,axiom,
( ~ p34(sK126(X1))
| p34(X1)
| r1(X1,sK124(X1))
| ~ r1(X0,X1)
| ~ sP31(X0) ) ).
cnf(u507,axiom,
( ~ p34(sK126(X1))
| p34(X1)
| p33(sK124(X1))
| ~ r1(X0,X1)
| ~ sP31(X0) ) ).
cnf(u533,axiom,
( ~ p32(sK131(X1))
| p32(X1)
| ~ r1(X0,X1)
| p31(X1)
| ~ sP29(X0) ) ).
cnf(u272,axiom,
( ~ sP51(X0)
| p54(X1)
| r1(sK64(X1),sK65(X1))
| p53(X1)
| ~ r1(X0,X1) ) ).
cnf(u494,axiom,
( ~ sP32(X0)
| p35(X1)
| p34(sK121(X1))
| p34(X1)
| ~ r1(X0,X1) ) ).
cnf(u250,axiom,
( ~ sP53(X0)
| p56(X1)
| r1(sK58(X1),sK59(X1))
| r1(X1,sK60(X1))
| ~ r1(X0,X1) ) ).
cnf(u531,axiom,
( ~ p32(sK132(X1))
| p32(X1)
| p31(sK130(X1))
| ~ r1(X0,X1)
| ~ sP29(X0) ) ).
cnf(u766,axiom,
( ~ sP10(X0)
| p12(X1)
| r1(sK187(X1),sK188(X1))
| r1(X1,sK189(X1))
| ~ r1(X0,X1) ) ).
cnf(u644,axiom,
( ~ sP20(X0)
| p22(X1)
| r1(sK157(X1),sK158(X1))
| p21(X1)
| ~ r1(X0,X1) ) ).
cnf(u278,axiom,
( ~ sP50(X0)
| p53(X1)
| p52(sK67(X1))
| p52(X1)
| ~ r1(X0,X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL645+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n014.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 16:12:46 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 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.96/2.46 % (980765)Detected formulas, will run a generic FOF schedule.
% 10.96/2.46 % (980772)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=550156337:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.96/2.46 % (980776)dis-21_1_sil=8000:lcm=predicate:random_seed=606129817: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.96/2.46 % (980775)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3691846935:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.96/2.46 % (980771)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=521057349:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.96/2.46 % (980773)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2353762227:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.96/2.46 % (980774)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=628202824:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.96/2.46 % (980770)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=841430769:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.96/2.46 % (980773)Instruction limit reached!
% 10.96/2.46 % (980773)------------------------------
% 10.96/2.46 % (980773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.46 % (980773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.46 % (980773)CaDiCaL version: 2.1.3
% 10.96/2.46 % (980773)Termination reason: Instruction limit
% 10.96/2.46 % (980773)Termination phase: Blocked clause elimination
% 10.96/2.46 % (980773)Time elapsed: 0.057 s
% 10.96/2.46 % (980773)Peak memory usage: 90 MB
% 10.96/2.46 % (980773)Instructions burned: 109 (million)
% 10.96/2.46 % (980774)Instruction limit reached!
% 10.96/2.46 % (980774)------------------------------
% 10.96/2.46 % (980774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.46 % (980774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.46 % (980774)CaDiCaL version: 2.1.3
% 10.96/2.46 % (980774)Termination reason: Instruction limit
% 10.96/2.46 % (980774)Termination phase: Saturation
% 10.96/2.46 % (980774)Time elapsed: 0.066 s
% 10.96/2.46 % (980774)Peak memory usage: 91 MB
% 10.96/2.46 % (980774)Instructions burned: 120 (million)
% 10.96/2.46 % (980776)Instruction limit reached!
% 10.96/2.46 % (980776)------------------------------
% 10.96/2.46 % (980776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.46 % (980776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.46 % (980776)CaDiCaL version: 2.1.3
% 10.96/2.46 % (980776)Termination reason: Instruction limit
% 10.96/2.46 % (980776)Termination phase: Saturation
% 10.96/2.46 % (980776)Time elapsed: 0.072 s
% 10.96/2.46 % (980776)Peak memory usage: 92 MB
% 10.96/2.46 % (980776)Instructions burned: 129 (million)
% 10.96/2.46 % (980775)Instruction limit reached!
% 10.96/2.46 % (980775)------------------------------
% 10.96/2.46 % (980775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.47 % (980775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.47 % (980775)CaDiCaL version: 2.1.3
% 10.96/2.47 % (980775)Termination reason: Instruction limit
% 10.96/2.47 % (980775)Termination phase: Saturation
% 10.96/2.47 % (980775)Time elapsed: 0.074 s
% 10.96/2.47 % (980775)Peak memory usage: 93 MB
% 10.96/2.47 % (980775)Instructions burned: 139 (million)
% 10.96/2.47 % (980784)lrs+10_1_sil=8000:sp=occurrence:random_seed=3266291913:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.96/2.47 % (980787)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=2443338344:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 10.96/2.47 % (980786)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3550011914:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 10.96/2.47 % (980785)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1318633218:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.96/2.47 % (980787)Refutation not found, incomplete strategy
% 10.96/2.47 % (980787)------------------------------
% 10.96/2.47 % (980787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.47 % (980787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.47 % (980787)CaDiCaL version: 2.1.3
% 10.96/2.47 % (980787)Termination reason: Refutation not found, incomplete strategy
% 10.96/2.47 % (980787)Time elapsed: 0.047 s
% 10.96/2.47 % (980787)Peak memory usage: 92 MB
% 10.96/2.47 % (980787)Instructions burned: 86 (million)
% 10.96/2.47 % (980785)Refutation not found, incomplete strategy
% 10.96/2.47 % (980785)------------------------------
% 10.96/2.47 % (980785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.47 % (980785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.47 % (980785)CaDiCaL version: 2.1.3
% 10.96/2.47 % (980785)Termination reason: Refutation not found, incomplete strategy
% 10.96/2.47 % (980785)Time elapsed: 0.048 s
% 10.96/2.47 % (980785)Peak memory usage: 92 MB
% 10.96/2.47 % (980785)Instructions burned: 89 (million)
% 10.96/2.47 % (980786)Refutation not found, incomplete strategy
% 10.96/2.47 % (980786)------------------------------
% 10.96/2.47 % (980786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.47 % (980786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.47 % (980786)CaDiCaL version: 2.1.3
% 10.96/2.47 % (980786)Termination reason: Refutation not found, incomplete strategy
% 10.96/2.47 % (980786)Time elapsed: 0.096 s
% 10.96/2.47 % (980786)Peak memory usage: 94 MB
% 10.96/2.47 % (980786)Instructions burned: 180 (million)
% 10.96/2.47 % (980784)Instruction limit reached!
% 10.96/2.47 % (980784)------------------------------
% 10.96/2.47 % (980784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.47 % (980784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.47 % (980784)CaDiCaL version: 2.1.3
% 10.96/2.47 % (980784)Termination reason: Instruction limit
% 10.96/2.47 % (980784)Termination phase: Saturation
% 10.96/2.47 % (980784)Time elapsed: 0.140 s
% 10.96/2.47 % (980784)Peak memory usage: 95 MB
% 10.96/2.47 % (980784)Instructions burned: 286 (million)
% 10.96/2.47 % (980787)------------------------------
% 10.96/2.47 % (980787)------------------------------
% 10.96/2.47 % (980785)------------------------------
% 10.96/2.47 % (980785)------------------------------
% 10.96/2.47 % (980792)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=827614223:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 10.96/2.47 % (980786)------------------------------
% 10.96/2.47 % (980786)------------------------------
% 10.96/2.47 % (980794)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1306112957:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 10.96/2.47 % (980795)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2532345684:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 10.96/2.47 % (980792)Instruction limit reached!
% 10.96/2.47 % (980792)------------------------------
% 10.96/2.47 % (980792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.47 % (980792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.47 % (980792)CaDiCaL version: 2.1.3
% 10.96/2.47 % (980792)Termination reason: Instruction limit
% 10.96/2.47 % (980792)Termination phase: Saturation
% 10.96/2.47 % (980792)Time elapsed: 0.155 s
% 10.96/2.47 % (980792)Peak memory usage: 97 MB
% 10.96/2.47 % (980792)Instructions burned: 294 (million)
% 10.96/2.47 % (980796)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3236222215:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 10.96/2.47 % (980795)Instruction limit reached!
% 10.96/2.47 % (980795)------------------------------
% 10.96/2.47 % (980795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.47 % (980795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.47 % (980795)CaDiCaL version: 2.1.3
% 10.96/2.47 % (980795)Termination reason: Instruction limit
% 10.96/2.47 % (980795)Termination phase: Saturation
% 10.96/2.47 % (980795)Time elapsed: 0.062 s
% 10.96/2.47 % (980795)Peak memory usage: 92 MB
% 10.96/2.47 % (980795)Instructions burned: 114 (million)
% 10.96/2.47 % (980796)Instruction limit reached!
% 10.96/2.47 % (980796)------------------------------
% 10.96/2.47 % (980796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.47 % (980796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.47 % (980796)CaDiCaL version: 2.1.3
% 10.96/2.47 % (980796)Termination reason: Instruction limit
% 10.96/2.47 % (980796)Termination phase: Blocked clause elimination
% 10.96/2.47 % (980796)Time elapsed: 0.071 s
% 10.96/2.47 % (980796)Peak memory usage: 90 MB
% 10.96/2.47 % (980796)Instructions burned: 128 (million)
% 10.96/2.47 % (980799)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4104089019:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 10.96/2.47 % (980799)Instruction limit reached!
% 10.96/2.47 % (980799)------------------------------
% 10.96/2.47 % (980799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.47 % (980799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.47 % (980799)CaDiCaL version: 2.1.3
% 10.96/2.47 % (980799)Termination reason: Instruction limit
% 10.96/2.47 % (980799)Termination phase: Saturation
% 10.96/2.47 % (980799)Time elapsed: 0.060 s
% 10.96/2.47 % (980799)Peak memory usage: 91 MB
% 10.96/2.47 % (980799)Instructions burned: 114 (million)
% 10.96/2.47 % (980801)lrs+10_1_sil=8000:sp=occurrence:random_seed=3992316256:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 10.96/2.47 % (980802)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3488551005:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 10.96/2.47 % (980805)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2232970776:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 10.96/2.47 % (980771)First to succeed.
% 10.96/2.47 % (980771)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-980765"
% 10.96/2.47 % (980802)Instruction limit reached!
% 10.96/2.47 % (980802)------------------------------
% 10.96/2.47 % (980802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.47 % (980802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.47 % (980802)CaDiCaL version: 2.1.3
% 10.96/2.47 % (980802)Termination reason: Instruction limit
% 10.96/2.47 % (980802)Termination phase: Saturation
% 10.96/2.47 % (980802)Time elapsed: 0.195 s
% 10.96/2.47 % (980802)Peak memory usage: 104 MB
% 10.96/2.47 % (980802)Instructions burned: 438 (million)
% 10.96/2.47 % (980801)Instruction limit reached!
% 10.96/2.47 % (980801)------------------------------
% 10.96/2.47 % (980801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.47 % (980801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.47 % (980801)CaDiCaL version: 2.1.3
% 10.96/2.47 % (980801)Termination reason: Instruction limit
% 10.96/2.47 % (980801)Termination phase: Saturation
% 10.96/2.47 % (980801)Time elapsed: 0.429 s
% 10.96/2.47 % (980801)Peak memory usage: 104 MB
% 10.96/2.47 % (980801)Instructions burned: 907 (million)
% 10.96/2.47 % (980808)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2268589595:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 10.96/2.47 % (980808)Instruction limit reached!
% 10.96/2.47 % (980808)------------------------------
% 10.96/2.47 % (980808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.96/2.47 % (980808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/2.47 % (980808)CaDiCaL version: 2.1.3
% 10.96/2.47 % (980808)Termination reason: Instruction limit
% 10.96/2.47 % (980808)Termination phase: Saturation
% 10.96/2.47 % (980808)Time elapsed: 0.073 s
% 10.96/2.47 % (980808)Peak memory usage: 92 MB
% 10.96/2.47 % (980808)Instructions burned: 136 (million)
% 10.96/2.47 % SZS status CounterSatisfiable for theBenchmark
% 10.96/2.47 % SZS output start Saturation.
% See solution above
% 11.77/2.66 % SZS output start Definitions and Model Updates.
% 11.77/2.66 % SZS output end Definitions and Model Updates.
% 11.77/2.66 % (980771)------------------------------
% 11.77/2.66 % (980771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.77/2.66 % (980771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.77/2.66 % (980771)CaDiCaL version: 2.1.3
% 11.77/2.66 % (980771)Termination reason: Satisfiable
% 11.77/2.66 % (980771)Time elapsed: 1.150 s
% 11.77/2.66 % (980771)Peak memory usage: 147 MB
% 11.77/2.66 % (980771)Instructions burned: 1750 (million)
% 11.77/2.66 % (980771)------------------------------
% 11.77/2.66 % (980771)------------------------------
% 11.77/2.66 % (980765)Success in time 1.589 s
% 11.77/2.66 % Vampire exiting
%------------------------------------------------------------------------------