%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL645+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : 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 8.57s 2.70s
% Output : Saturation 13.46s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1968,negated_conjecture,
( ~ p1(X753)
| ~ p1(X754)
| ~ r1(X751,X754)
| ~ r1(sK300,X751)
| ~ r1(sK602(X751),X753)
| p2(X751) ) ).
cnf(u1971,negated_conjecture,
( ~ p2(sK601(X748))
| ~ p2(X748)
| ~ r1(sK300,X748)
| p1(sK600(X748)) ) ).
cnf(u1975,negated_conjecture,
( ~ p1(X754)
| ~ r1(sK300,X751)
| ~ r1(X751,X754)
| r1(X751,sK602(X751))
| p2(X751) ) ).
cnf(u1984,negated_conjecture,
( ~ p2(sK601(X748))
| ~ p2(X748)
| ~ r1(sK300,X748)
| r1(X748,sK600(X748)) ) ).
cnf(u1997,negated_conjecture,
( ~ p2(sK599(X745))
| ~ p2(X745)
| ~ r1(sK300,X745)
| ~ p1(X745)
| p2(X746)
| ~ r1(X745,X746) ) ).
cnf(u2001,negated_conjecture,
( ~ p1(X745)
| ~ p2(X745)
| r1(X745,sK599(X745))
| ~ r1(sK300,X745)
| p2(X746)
| ~ r1(X745,X746) ) ).
cnf(u2005,negated_conjecture,
( ~ p2(X743)
| ~ p2(X744)
| ~ r1(X741,X744)
| ~ r1(sK300,X741)
| ~ r1(sK598(X741),X743)
| p3(X741) ) ).
cnf(u2012,negated_conjecture,
( ~ p2(X744)
| ~ r1(sK300,X741)
| ~ r1(X741,X744)
| r1(X741,sK598(X741))
| p3(X741) ) ).
cnf(u2031,negated_conjecture,
sP1(sK300) ).
cnf(u2042,negated_conjecture,
( ~ p3(X733)
| ~ p3(X734)
| ~ r1(X731,X734)
| ~ r1(sK300,X731)
| ~ r1(sK594(X731),X733)
| p4(X731) ) ).
cnf(u2049,negated_conjecture,
( ~ p3(X734)
| ~ r1(sK300,X731)
| ~ r1(X731,X734)
| r1(X731,sK594(X731))
| p4(X731) ) ).
cnf(u2071,negated_conjecture,
( ~ p4(sK591(X725))
| ~ p4(X725)
| ~ r1(sK300,X725)
| ~ p3(X725)
| p4(X726)
| ~ r1(X725,X726) ) ).
cnf(u2075,negated_conjecture,
( ~ p3(X725)
| ~ p4(X725)
| r1(X725,sK591(X725))
| ~ r1(sK300,X725)
| p4(X726)
| ~ r1(X725,X726) ) ).
cnf(u2079,negated_conjecture,
( ~ p4(X723)
| ~ p4(X724)
| ~ r1(X721,X724)
| ~ r1(sK300,X721)
| ~ r1(sK590(X721),X723)
| p5(X721) ) ).
cnf(u2086,negated_conjecture,
( ~ p4(X724)
| ~ r1(sK300,X721)
| ~ r1(X721,X724)
| r1(X721,sK590(X721))
| p5(X721) ) ).
cnf(u2108,negated_conjecture,
( ~ p5(sK587(X715))
| ~ p5(X715)
| ~ r1(sK300,X715)
| ~ p4(X715)
| p5(X716)
| ~ r1(X715,X716) ) ).
cnf(u2112,negated_conjecture,
( ~ p4(X715)
| ~ p5(X715)
| r1(X715,sK587(X715))
| ~ r1(sK300,X715)
| p5(X716)
| ~ r1(X715,X716) ) ).
cnf(u2116,negated_conjecture,
( ~ p5(X713)
| ~ p5(X714)
| ~ r1(X711,X714)
| ~ r1(sK300,X711)
| ~ r1(sK586(X711),X713)
| p6(X711) ) ).
cnf(u2123,negated_conjecture,
( ~ p5(X714)
| ~ r1(sK300,X711)
| ~ r1(X711,X714)
| r1(X711,sK586(X711))
| p6(X711) ) ).
cnf(u2145,negated_conjecture,
( ~ p6(sK583(X705))
| ~ p6(X705)
| ~ r1(sK300,X705)
| ~ p5(X705)
| p6(X706)
| ~ r1(X705,X706) ) ).
cnf(u2149,negated_conjecture,
( ~ p5(X705)
| ~ p6(X705)
| r1(X705,sK583(X705))
| ~ r1(sK300,X705)
| p6(X706)
| ~ r1(X705,X706) ) ).
cnf(u2153,negated_conjecture,
( ~ p6(X703)
| ~ p6(X704)
| ~ r1(X701,X704)
| ~ r1(sK300,X701)
| ~ r1(sK582(X701),X703)
| p7(X701) ) ).
cnf(u2160,negated_conjecture,
( ~ p6(X704)
| ~ r1(sK300,X701)
| ~ r1(X701,X704)
| r1(X701,sK582(X701))
| p7(X701) ) ).
cnf(u2182,negated_conjecture,
( ~ p7(sK579(X695))
| ~ p7(X695)
| ~ r1(sK300,X695)
| ~ p6(X695)
| p7(X696)
| ~ r1(X695,X696) ) ).
cnf(u2186,negated_conjecture,
( ~ p6(X695)
| ~ p7(X695)
| r1(X695,sK579(X695))
| ~ r1(sK300,X695)
| p7(X696)
| ~ r1(X695,X696) ) ).
cnf(u2190,negated_conjecture,
( ~ p7(X693)
| ~ p7(X694)
| ~ r1(X691,X694)
| ~ r1(sK300,X691)
| ~ r1(sK578(X691),X693)
| p8(X691) ) ).
cnf(u2197,negated_conjecture,
( ~ p7(X694)
| ~ r1(sK300,X691)
| ~ r1(X691,X694)
| r1(X691,sK578(X691))
| p8(X691) ) ).
cnf(u2219,negated_conjecture,
( ~ p8(sK575(X685))
| ~ p8(X685)
| ~ r1(sK300,X685)
| ~ p7(X685)
| p8(X686)
| ~ r1(X685,X686) ) ).
cnf(u2223,negated_conjecture,
( ~ p7(X685)
| ~ p8(X685)
| r1(X685,sK575(X685))
| ~ r1(sK300,X685)
| p8(X686)
| ~ r1(X685,X686) ) ).
cnf(u2227,negated_conjecture,
( ~ p8(X683)
| ~ p8(X684)
| ~ r1(X681,X684)
| ~ r1(sK300,X681)
| ~ r1(sK574(X681),X683)
| p9(X681) ) ).
cnf(u2234,negated_conjecture,
( ~ p8(X684)
| ~ r1(sK300,X681)
| ~ r1(X681,X684)
| r1(X681,sK574(X681))
| p9(X681) ) ).
cnf(u2256,negated_conjecture,
( ~ p9(sK571(X675))
| ~ p9(X675)
| ~ r1(sK300,X675)
| ~ p8(X675)
| p9(X676)
| ~ r1(X675,X676) ) ).
cnf(u2260,negated_conjecture,
( ~ p8(X675)
| ~ p9(X675)
| r1(X675,sK571(X675))
| ~ r1(sK300,X675)
| p9(X676)
| ~ r1(X675,X676) ) ).
cnf(u2264,negated_conjecture,
( ~ p9(X673)
| ~ p9(X674)
| ~ r1(X671,X674)
| ~ r1(sK300,X671)
| ~ r1(sK570(X671),X673)
| p10(X671) ) ).
cnf(u2271,negated_conjecture,
( ~ p9(X674)
| ~ r1(sK300,X671)
| ~ r1(X671,X674)
| r1(X671,sK570(X671))
| p10(X671) ) ).
cnf(u2293,negated_conjecture,
( ~ p10(sK567(X665))
| ~ p10(X665)
| ~ r1(sK300,X665)
| ~ p9(X665)
| p10(X666)
| ~ r1(X665,X666) ) ).
cnf(u2297,negated_conjecture,
( ~ p9(X665)
| ~ p10(X665)
| r1(X665,sK567(X665))
| ~ r1(sK300,X665)
| p10(X666)
| ~ r1(X665,X666) ) ).
cnf(u2301,negated_conjecture,
( ~ p10(X663)
| ~ p10(X664)
| ~ r1(X661,X664)
| ~ r1(sK300,X661)
| ~ r1(sK566(X661),X663)
| p11(X661) ) ).
cnf(u2308,negated_conjecture,
( ~ p10(X664)
| ~ r1(sK300,X661)
| ~ r1(X661,X664)
| r1(X661,sK566(X661))
| p11(X661) ) ).
cnf(u2330,negated_conjecture,
( ~ p11(sK563(X655))
| ~ p11(X655)
| ~ r1(sK300,X655)
| ~ p10(X655)
| p11(X656)
| ~ r1(X655,X656) ) ).
cnf(u2334,negated_conjecture,
( ~ p10(X655)
| ~ p11(X655)
| r1(X655,sK563(X655))
| ~ r1(sK300,X655)
| p11(X656)
| ~ r1(X655,X656) ) ).
cnf(u2338,negated_conjecture,
( ~ p11(X653)
| ~ p11(X654)
| ~ r1(X651,X654)
| ~ r1(sK300,X651)
| ~ r1(sK562(X651),X653)
| p12(X651) ) ).
cnf(u2345,negated_conjecture,
( ~ p11(X654)
| ~ r1(sK300,X651)
| ~ r1(X651,X654)
| r1(X651,sK562(X651))
| p12(X651) ) ).
cnf(u2364,negated_conjecture,
sP10(sK300) ).
cnf(u2375,negated_conjecture,
( ~ p12(X643)
| ~ p12(X644)
| ~ r1(X641,X644)
| ~ r1(sK300,X641)
| ~ r1(sK558(X641),X643)
| p13(X641) ) ).
cnf(u2382,negated_conjecture,
( ~ p12(X644)
| ~ r1(sK300,X641)
| ~ r1(X641,X644)
| r1(X641,sK558(X641))
| p13(X641) ) ).
cnf(u2404,negated_conjecture,
( ~ p13(sK555(X635))
| ~ p13(X635)
| ~ r1(sK300,X635)
| ~ p12(X635)
| p13(X636)
| ~ r1(X635,X636) ) ).
cnf(u2408,negated_conjecture,
( ~ p12(X635)
| ~ p13(X635)
| r1(X635,sK555(X635))
| ~ r1(sK300,X635)
| p13(X636)
| ~ r1(X635,X636) ) ).
cnf(u2412,negated_conjecture,
( ~ p13(X633)
| ~ p13(X634)
| ~ r1(X631,X634)
| ~ r1(sK300,X631)
| ~ r1(sK554(X631),X633)
| p14(X631) ) ).
cnf(u2419,negated_conjecture,
( ~ p13(X634)
| ~ r1(sK300,X631)
| ~ r1(X631,X634)
| r1(X631,sK554(X631))
| p14(X631) ) ).
cnf(u2441,negated_conjecture,
( ~ p14(sK551(X625))
| ~ p14(X625)
| ~ r1(sK300,X625)
| ~ p13(X625)
| p14(X626)
| ~ r1(X625,X626) ) ).
cnf(u2445,negated_conjecture,
( ~ p13(X625)
| ~ p14(X625)
| r1(X625,sK551(X625))
| ~ r1(sK300,X625)
| p14(X626)
| ~ r1(X625,X626) ) ).
cnf(u2449,negated_conjecture,
( ~ p14(X623)
| ~ p14(X624)
| ~ r1(X621,X624)
| ~ r1(sK300,X621)
| ~ r1(sK550(X621),X623)
| p15(X621) ) ).
cnf(u2456,negated_conjecture,
( ~ p14(X624)
| ~ r1(sK300,X621)
| ~ r1(X621,X624)
| r1(X621,sK550(X621))
| p15(X621) ) ).
cnf(u2478,negated_conjecture,
( ~ p15(sK547(X615))
| ~ p15(X615)
| ~ r1(sK300,X615)
| ~ p14(X615)
| p15(X616)
| ~ r1(X615,X616) ) ).
cnf(u2482,negated_conjecture,
( ~ p14(X615)
| ~ p15(X615)
| r1(X615,sK547(X615))
| ~ r1(sK300,X615)
| p15(X616)
| ~ r1(X615,X616) ) ).
cnf(u2486,negated_conjecture,
( ~ p15(X613)
| ~ p15(X614)
| ~ r1(X611,X614)
| ~ r1(sK300,X611)
| ~ r1(sK546(X611),X613)
| p16(X611) ) ).
cnf(u2493,negated_conjecture,
( ~ p15(X614)
| ~ r1(sK300,X611)
| ~ r1(X611,X614)
| r1(X611,sK546(X611))
| p16(X611) ) ).
cnf(u2515,negated_conjecture,
( ~ p16(sK543(X605))
| ~ p16(X605)
| ~ r1(sK300,X605)
| ~ p15(X605)
| p16(X606)
| ~ r1(X605,X606) ) ).
cnf(u2519,negated_conjecture,
( ~ p15(X605)
| ~ p16(X605)
| r1(X605,sK543(X605))
| ~ r1(sK300,X605)
| p16(X606)
| ~ r1(X605,X606) ) ).
cnf(u2523,negated_conjecture,
( ~ p16(X603)
| ~ p16(X604)
| ~ r1(X601,X604)
| ~ r1(sK300,X601)
| ~ r1(sK542(X601),X603)
| p17(X601) ) ).
cnf(u2530,negated_conjecture,
( ~ p16(X604)
| ~ r1(sK300,X601)
| ~ r1(X601,X604)
| r1(X601,sK542(X601))
| p17(X601) ) ).
cnf(u2552,negated_conjecture,
( ~ p17(sK539(X595))
| ~ p17(X595)
| ~ r1(sK300,X595)
| ~ p16(X595)
| p17(X596)
| ~ r1(X595,X596) ) ).
cnf(u2556,negated_conjecture,
( ~ p16(X595)
| ~ p17(X595)
| r1(X595,sK539(X595))
| ~ r1(sK300,X595)
| p17(X596)
| ~ r1(X595,X596) ) ).
cnf(u2560,negated_conjecture,
( ~ p17(X593)
| ~ p17(X594)
| ~ r1(X591,X594)
| ~ r1(sK300,X591)
| ~ r1(sK538(X591),X593)
| p18(X591) ) ).
cnf(u2567,negated_conjecture,
( ~ p17(X594)
| ~ r1(sK300,X591)
| ~ r1(X591,X594)
| r1(X591,sK538(X591))
| p18(X591) ) ).
cnf(u2589,negated_conjecture,
( ~ p18(sK535(X585))
| ~ p18(X585)
| ~ r1(sK300,X585)
| ~ p17(X585)
| p18(X586)
| ~ r1(X585,X586) ) ).
cnf(u2593,negated_conjecture,
( ~ p17(X585)
| ~ p18(X585)
| r1(X585,sK535(X585))
| ~ r1(sK300,X585)
| p18(X586)
| ~ r1(X585,X586) ) ).
cnf(u2597,negated_conjecture,
( ~ p18(X583)
| ~ p18(X584)
| ~ r1(X581,X584)
| ~ r1(sK300,X581)
| ~ r1(sK534(X581),X583)
| p19(X581) ) ).
cnf(u2604,negated_conjecture,
( ~ p18(X584)
| ~ r1(sK300,X581)
| ~ r1(X581,X584)
| r1(X581,sK534(X581))
| p19(X581) ) ).
cnf(u2626,negated_conjecture,
( ~ p19(sK531(X575))
| ~ p19(X575)
| ~ r1(sK300,X575)
| ~ p18(X575)
| p19(X576)
| ~ r1(X575,X576) ) ).
cnf(u2630,negated_conjecture,
( ~ p18(X575)
| ~ p19(X575)
| r1(X575,sK531(X575))
| ~ r1(sK300,X575)
| p19(X576)
| ~ r1(X575,X576) ) ).
cnf(u2634,negated_conjecture,
( ~ p19(X573)
| ~ p19(X574)
| ~ r1(X571,X574)
| ~ r1(sK300,X571)
| ~ r1(sK530(X571),X573)
| p20(X571) ) ).
cnf(u2641,negated_conjecture,
( ~ p19(X574)
| ~ r1(sK300,X571)
| ~ r1(X571,X574)
| r1(X571,sK530(X571))
| p20(X571) ) ).
cnf(u2663,negated_conjecture,
( ~ p20(sK527(X565))
| ~ p20(X565)
| ~ r1(sK300,X565)
| ~ p19(X565)
| p20(X566)
| ~ r1(X565,X566) ) ).
cnf(u2667,negated_conjecture,
( ~ p19(X565)
| ~ p20(X565)
| r1(X565,sK527(X565))
| ~ r1(sK300,X565)
| p20(X566)
| ~ r1(X565,X566) ) ).
cnf(u2671,negated_conjecture,
( ~ r1(sK526(X561),X563)
| ~ p20(X564)
| ~ r1(X561,X564)
| ~ p20(X563)
| ~ r1(sK300,X561)
| p21(X561) ) ).
cnf(u2674,negated_conjecture,
( ~ p21(sK525(X558))
| ~ p21(X558)
| ~ r1(sK300,X558)
| p20(sK524(X558)) ) ).
cnf(u2682,negated_conjecture,
( ~ p21(X558)
| ~ r1(sK300,X558)
| r1(X558,sK525(X558))
| p20(sK524(X558)) ) ).
cnf(u2687,negated_conjecture,
( ~ p21(sK525(X558))
| ~ p21(X558)
| ~ r1(sK300,X558)
| r1(X558,sK524(X558)) ) ).
cnf(u2692,negated_conjecture,
( ~ p21(X558)
| ~ r1(sK300,X558)
| r1(X558,sK525(X558))
| r1(X558,sK524(X558)) ) ).
cnf(u2700,negated_conjecture,
( ~ p21(sK523(X555))
| ~ p21(X555)
| ~ r1(sK300,X555)
| ~ p20(X555)
| p21(X556)
| ~ r1(X555,X556) ) ).
cnf(u2704,negated_conjecture,
( ~ p21(X555)
| ~ r1(sK300,X555)
| r1(X555,sK523(X555))
| ~ p20(X555)
| p21(X556)
| ~ r1(X555,X556) ) ).
cnf(u2708,negated_conjecture,
( ~ p21(X553)
| ~ p21(X554)
| ~ r1(X551,X554)
| ~ r1(sK300,X551)
| ~ r1(sK522(X551),X553)
| p22(X551) ) ).
cnf(u2715,negated_conjecture,
( ~ p21(X554)
| ~ r1(sK300,X551)
| ~ r1(X551,X554)
| r1(X551,sK522(X551))
| p22(X551) ) ).
cnf(u2737,negated_conjecture,
( ~ p22(sK519(X545))
| ~ p22(X545)
| ~ r1(sK300,X545)
| ~ p21(X545)
| p22(X546)
| ~ r1(X545,X546) ) ).
cnf(u2741,negated_conjecture,
( ~ p21(X545)
| ~ p22(X545)
| r1(X545,sK519(X545))
| ~ r1(sK300,X545)
| p22(X546)
| ~ r1(X545,X546) ) ).
cnf(u2745,negated_conjecture,
( ~ p22(X543)
| ~ p22(X544)
| ~ r1(X541,X544)
| ~ r1(sK300,X541)
| ~ r1(sK518(X541),X543)
| p23(X541) ) ).
cnf(u2752,negated_conjecture,
( ~ p22(X544)
| ~ r1(sK300,X541)
| ~ r1(X541,X544)
| r1(X541,sK518(X541))
| p23(X541) ) ).
cnf(u2774,negated_conjecture,
( ~ p23(sK515(X535))
| ~ p23(X535)
| ~ r1(sK300,X535)
| ~ p22(X535)
| p23(X536)
| ~ r1(X535,X536) ) ).
cnf(u2778,negated_conjecture,
( ~ p22(X535)
| ~ p23(X535)
| r1(X535,sK515(X535))
| ~ r1(sK300,X535)
| p23(X536)
| ~ r1(X535,X536) ) ).
cnf(u2782,negated_conjecture,
( ~ p23(X533)
| ~ p23(X534)
| ~ r1(X531,X534)
| ~ r1(sK300,X531)
| ~ r1(sK514(X531),X533)
| p24(X531) ) ).
cnf(u2789,negated_conjecture,
( ~ p23(X534)
| ~ r1(sK300,X531)
| ~ r1(X531,X534)
| r1(X531,sK514(X531))
| p24(X531) ) ).
cnf(u2811,negated_conjecture,
( ~ p24(sK511(X525))
| ~ p24(X525)
| ~ r1(sK300,X525)
| ~ p23(X525)
| p24(X526)
| ~ r1(X525,X526) ) ).
cnf(u2815,negated_conjecture,
( ~ p23(X525)
| ~ p24(X525)
| r1(X525,sK511(X525))
| ~ r1(sK300,X525)
| p24(X526)
| ~ r1(X525,X526) ) ).
cnf(u2819,negated_conjecture,
( ~ p24(X523)
| ~ p24(X524)
| ~ r1(X521,X524)
| ~ r1(sK300,X521)
| ~ r1(sK510(X521),X523)
| p25(X521) ) ).
cnf(u2826,negated_conjecture,
( ~ p24(X524)
| ~ r1(sK300,X521)
| ~ r1(X521,X524)
| r1(X521,sK510(X521))
| p25(X521) ) ).
cnf(u2848,negated_conjecture,
( ~ p25(sK507(X515))
| ~ p25(X515)
| ~ r1(sK300,X515)
| ~ p24(X515)
| p25(X516)
| ~ r1(X515,X516) ) ).
cnf(u2852,negated_conjecture,
( ~ p24(X515)
| ~ p25(X515)
| r1(X515,sK507(X515))
| ~ r1(sK300,X515)
| p25(X516)
| ~ r1(X515,X516) ) ).
cnf(u2856,negated_conjecture,
( ~ p25(X513)
| ~ p25(X514)
| ~ r1(X511,X514)
| ~ r1(sK300,X511)
| ~ r1(sK506(X511),X513)
| p26(X511) ) ).
cnf(u2863,negated_conjecture,
( ~ p25(X514)
| ~ r1(sK300,X511)
| ~ r1(X511,X514)
| r1(X511,sK506(X511))
| p26(X511) ) ).
cnf(u2885,negated_conjecture,
( ~ p26(sK503(X505))
| ~ p26(X505)
| ~ r1(sK300,X505)
| ~ p25(X505)
| p26(X506)
| ~ r1(X505,X506) ) ).
cnf(u2889,negated_conjecture,
( ~ p25(X505)
| ~ p26(X505)
| r1(X505,sK503(X505))
| ~ r1(sK300,X505)
| p26(X506)
| ~ r1(X505,X506) ) ).
cnf(u2893,negated_conjecture,
( ~ p26(X503)
| ~ p26(X504)
| ~ r1(X501,X504)
| ~ r1(sK300,X501)
| ~ r1(sK502(X501),X503)
| p27(X501) ) ).
cnf(u2900,negated_conjecture,
( ~ p26(X504)
| ~ r1(sK300,X501)
| ~ r1(X501,X504)
| r1(X501,sK502(X501))
| p27(X501) ) ).
cnf(u2922,negated_conjecture,
( ~ p27(sK499(X495))
| ~ p27(X495)
| ~ r1(sK300,X495)
| ~ p26(X495)
| p27(X496)
| ~ r1(X495,X496) ) ).
cnf(u2926,negated_conjecture,
( ~ p26(X495)
| ~ p27(X495)
| r1(X495,sK499(X495))
| ~ r1(sK300,X495)
| p27(X496)
| ~ r1(X495,X496) ) ).
cnf(u2930,negated_conjecture,
( ~ p27(X493)
| ~ p27(X494)
| ~ r1(X491,X494)
| ~ r1(sK300,X491)
| ~ r1(sK498(X491),X493)
| p28(X491) ) ).
cnf(u2937,negated_conjecture,
( ~ p27(X494)
| ~ r1(sK300,X491)
| ~ r1(X491,X494)
| r1(X491,sK498(X491))
| p28(X491) ) ).
cnf(u2959,negated_conjecture,
( ~ p28(sK495(X485))
| ~ p28(X485)
| ~ r1(sK300,X485)
| ~ p27(X485)
| p28(X486)
| ~ r1(X485,X486) ) ).
cnf(u2963,negated_conjecture,
( ~ p27(X485)
| ~ p28(X485)
| r1(X485,sK495(X485))
| ~ r1(sK300,X485)
| p28(X486)
| ~ r1(X485,X486) ) ).
cnf(u2967,negated_conjecture,
( ~ p28(X483)
| ~ p28(X484)
| ~ r1(X481,X484)
| ~ r1(sK300,X481)
| ~ r1(sK494(X481),X483)
| p29(X481) ) ).
cnf(u2974,negated_conjecture,
( ~ p28(X484)
| ~ r1(sK300,X481)
| ~ r1(X481,X484)
| r1(X481,sK494(X481))
| p29(X481) ) ).
cnf(u2996,negated_conjecture,
( ~ p29(sK491(X475))
| ~ p29(X475)
| ~ r1(sK300,X475)
| ~ p28(X475)
| p29(X476)
| ~ r1(X475,X476) ) ).
cnf(u3000,negated_conjecture,
( ~ p28(X475)
| ~ p29(X475)
| r1(X475,sK491(X475))
| ~ r1(sK300,X475)
| p29(X476)
| ~ r1(X475,X476) ) ).
cnf(u3004,negated_conjecture,
( ~ p29(X473)
| ~ p29(X474)
| ~ r1(X471,X474)
| ~ r1(sK300,X471)
| ~ r1(sK490(X471),X473)
| p30(X471) ) ).
cnf(u3011,negated_conjecture,
( ~ p29(X474)
| ~ r1(sK300,X471)
| ~ r1(X471,X474)
| r1(X471,sK490(X471))
| p30(X471) ) ).
cnf(u3033,negated_conjecture,
( ~ p30(sK487(X465))
| ~ p30(X465)
| ~ r1(sK300,X465)
| ~ p29(X465)
| p30(X466)
| ~ r1(X465,X466) ) ).
cnf(u3037,negated_conjecture,
( ~ p29(X465)
| ~ p30(X465)
| r1(X465,sK487(X465))
| ~ r1(sK300,X465)
| p30(X466)
| ~ r1(X465,X466) ) ).
cnf(u3041,negated_conjecture,
( ~ p30(X463)
| ~ p30(X464)
| ~ r1(X461,X464)
| ~ r1(sK300,X461)
| ~ r1(sK486(X461),X463)
| p31(X461) ) ).
cnf(u3048,negated_conjecture,
( ~ p30(X464)
| ~ r1(sK300,X461)
| ~ r1(X461,X464)
| r1(X461,sK486(X461))
| p31(X461) ) ).
cnf(u3070,negated_conjecture,
( ~ p31(sK483(X455))
| ~ p31(X455)
| ~ r1(sK300,X455)
| ~ p30(X455)
| p31(X456)
| ~ r1(X455,X456) ) ).
cnf(u3074,negated_conjecture,
( ~ p30(X455)
| ~ p31(X455)
| r1(X455,sK483(X455))
| ~ r1(sK300,X455)
| p31(X456)
| ~ r1(X455,X456) ) ).
cnf(u3078,negated_conjecture,
( ~ p31(X453)
| ~ p31(X454)
| ~ r1(X451,X454)
| ~ r1(sK300,X451)
| ~ r1(sK482(X451),X453)
| p32(X451) ) ).
cnf(u3085,negated_conjecture,
( ~ p31(X454)
| ~ r1(sK300,X451)
| ~ r1(X451,X454)
| r1(X451,sK482(X451))
| p32(X451) ) ).
cnf(u3107,negated_conjecture,
( ~ p32(sK479(X445))
| ~ p32(X445)
| ~ r1(sK300,X445)
| ~ p31(X445)
| p32(X446)
| ~ r1(X445,X446) ) ).
cnf(u3111,negated_conjecture,
( ~ p31(X445)
| ~ p32(X445)
| r1(X445,sK479(X445))
| ~ r1(sK300,X445)
| p32(X446)
| ~ r1(X445,X446) ) ).
cnf(u3115,negated_conjecture,
( ~ p32(X443)
| ~ p32(X444)
| ~ r1(X441,X444)
| ~ r1(sK300,X441)
| ~ r1(sK478(X441),X443)
| p33(X441) ) ).
cnf(u3122,negated_conjecture,
( ~ p32(X444)
| ~ r1(sK300,X441)
| ~ r1(X441,X444)
| r1(X441,sK478(X441))
| p33(X441) ) ).
cnf(u3144,negated_conjecture,
( ~ p33(sK475(X435))
| ~ p33(X435)
| ~ r1(sK300,X435)
| ~ p32(X435)
| p33(X436)
| ~ r1(X435,X436) ) ).
cnf(u3148,negated_conjecture,
( ~ p32(X435)
| ~ p33(X435)
| r1(X435,sK475(X435))
| ~ r1(sK300,X435)
| p33(X436)
| ~ r1(X435,X436) ) ).
cnf(u3152,negated_conjecture,
( ~ p33(X433)
| ~ p33(X434)
| ~ r1(X431,X434)
| ~ r1(sK300,X431)
| ~ r1(sK474(X431),X433)
| p34(X431) ) ).
cnf(u3159,negated_conjecture,
( ~ p33(X434)
| ~ r1(sK300,X431)
| ~ r1(X431,X434)
| r1(X431,sK474(X431))
| p34(X431) ) ).
cnf(u3181,negated_conjecture,
( ~ p34(sK471(X425))
| ~ p34(X425)
| ~ r1(sK300,X425)
| ~ p33(X425)
| p34(X426)
| ~ r1(X425,X426) ) ).
cnf(u3185,negated_conjecture,
( ~ p33(X425)
| ~ p34(X425)
| r1(X425,sK471(X425))
| ~ r1(sK300,X425)
| p34(X426)
| ~ r1(X425,X426) ) ).
cnf(u3189,negated_conjecture,
( ~ p34(X423)
| ~ p34(X424)
| ~ r1(X421,X424)
| ~ r1(sK300,X421)
| ~ r1(sK470(X421),X423)
| p35(X421) ) ).
cnf(u3196,negated_conjecture,
( ~ p34(X424)
| ~ r1(sK300,X421)
| ~ r1(X421,X424)
| r1(X421,sK470(X421))
| p35(X421) ) ).
cnf(u3218,negated_conjecture,
( ~ p35(sK467(X415))
| ~ p35(X415)
| ~ r1(sK300,X415)
| ~ p34(X415)
| p35(X416)
| ~ r1(X415,X416) ) ).
cnf(u3222,negated_conjecture,
( ~ p34(X415)
| ~ p35(X415)
| r1(X415,sK467(X415))
| ~ r1(sK300,X415)
| p35(X416)
| ~ r1(X415,X416) ) ).
cnf(u3226,negated_conjecture,
( ~ p35(X413)
| ~ p35(X414)
| ~ r1(X411,X414)
| ~ r1(sK300,X411)
| ~ r1(sK466(X411),X413)
| p36(X411) ) ).
cnf(u3233,negated_conjecture,
( ~ p35(X414)
| ~ r1(sK300,X411)
| ~ r1(X411,X414)
| r1(X411,sK466(X411))
| p36(X411) ) ).
cnf(u3255,negated_conjecture,
( ~ p36(sK463(X405))
| ~ p36(X405)
| ~ r1(sK300,X405)
| ~ p35(X405)
| p36(X406)
| ~ r1(X405,X406) ) ).
cnf(u3259,negated_conjecture,
( ~ p35(X405)
| ~ p36(X405)
| r1(X405,sK463(X405))
| ~ r1(sK300,X405)
| p36(X406)
| ~ r1(X405,X406) ) ).
cnf(u3263,negated_conjecture,
( ~ p36(X403)
| ~ p36(X404)
| ~ r1(X401,X404)
| ~ r1(sK300,X401)
| ~ r1(sK462(X401),X403)
| p37(X401) ) ).
cnf(u3270,negated_conjecture,
( ~ p36(X404)
| ~ r1(sK300,X401)
| ~ r1(X401,X404)
| r1(X401,sK462(X401))
| p37(X401) ) ).
cnf(u3292,negated_conjecture,
( ~ p37(sK459(X395))
| ~ p37(X395)
| ~ r1(sK300,X395)
| ~ p36(X395)
| p37(X396)
| ~ r1(X395,X396) ) ).
cnf(u3296,negated_conjecture,
( ~ p36(X395)
| ~ p37(X395)
| r1(X395,sK459(X395))
| ~ r1(sK300,X395)
| p37(X396)
| ~ r1(X395,X396) ) ).
cnf(u3300,negated_conjecture,
( ~ p37(X393)
| ~ p37(X394)
| ~ r1(X391,X394)
| ~ r1(sK300,X391)
| ~ r1(sK458(X391),X393)
| p38(X391) ) ).
cnf(u3307,negated_conjecture,
( ~ p37(X394)
| ~ r1(sK300,X391)
| ~ r1(X391,X394)
| r1(X391,sK458(X391))
| p38(X391) ) ).
cnf(u3329,negated_conjecture,
( ~ p38(sK455(X385))
| ~ p38(X385)
| ~ r1(sK300,X385)
| ~ p37(X385)
| p38(X386)
| ~ r1(X385,X386) ) ).
cnf(u3333,negated_conjecture,
( ~ p37(X385)
| ~ p38(X385)
| r1(X385,sK455(X385))
| ~ r1(sK300,X385)
| p38(X386)
| ~ r1(X385,X386) ) ).
cnf(u3337,negated_conjecture,
( ~ p38(X383)
| ~ p38(X384)
| ~ r1(X381,X384)
| ~ r1(sK300,X381)
| ~ r1(sK454(X381),X383)
| p39(X381) ) ).
cnf(u3344,negated_conjecture,
( ~ p38(X384)
| ~ r1(sK300,X381)
| ~ r1(X381,X384)
| r1(X381,sK454(X381))
| p39(X381) ) ).
cnf(u3366,negated_conjecture,
( ~ p39(sK451(X375))
| ~ p39(X375)
| ~ r1(sK300,X375)
| ~ p38(X375)
| p39(X376)
| ~ r1(X375,X376) ) ).
cnf(u3370,negated_conjecture,
( ~ p38(X375)
| ~ p39(X375)
| r1(X375,sK451(X375))
| ~ r1(sK300,X375)
| p39(X376)
| ~ r1(X375,X376) ) ).
cnf(u3374,negated_conjecture,
( ~ p40(X369)
| ~ p40(X370)
| ~ r1(X367,X370)
| ~ r1(sK300,X367)
| ~ r1(sK448(X367),X369)
| p41(X367) ) ).
cnf(u3381,negated_conjecture,
( ~ p40(X370)
| ~ r1(sK300,X367)
| ~ r1(X367,X370)
| r1(X367,sK448(X367))
| p41(X367) ) ).
cnf(u3403,negated_conjecture,
( ~ p41(sK445(X361))
| ~ p41(X361)
| ~ r1(sK300,X361)
| ~ p40(X361)
| p41(X362)
| ~ r1(X361,X362) ) ).
cnf(u3407,negated_conjecture,
( ~ p40(X361)
| ~ p41(X361)
| r1(X361,sK445(X361))
| ~ r1(sK300,X361)
| p41(X362)
| ~ r1(X361,X362) ) ).
cnf(u3411,negated_conjecture,
( ~ p41(X359)
| ~ p41(X360)
| ~ r1(X357,X360)
| ~ r1(sK300,X357)
| ~ r1(sK444(X357),X359)
| p42(X357) ) ).
cnf(u3418,negated_conjecture,
( ~ p41(X360)
| ~ r1(sK300,X357)
| ~ r1(X357,X360)
| r1(X357,sK444(X357))
| p42(X357) ) ).
cnf(u3440,negated_conjecture,
( ~ p42(sK441(X351))
| ~ p42(X351)
| ~ r1(sK300,X351)
| ~ p41(X351)
| p42(X352)
| ~ r1(X351,X352) ) ).
cnf(u3444,negated_conjecture,
( ~ p41(X351)
| ~ p42(X351)
| r1(X351,sK441(X351))
| ~ r1(sK300,X351)
| p42(X352)
| ~ r1(X351,X352) ) ).
cnf(u3448,negated_conjecture,
( ~ p42(X349)
| ~ p42(X350)
| ~ r1(X347,X350)
| ~ r1(sK300,X347)
| ~ r1(sK440(X347),X349)
| p43(X347) ) ).
cnf(u3455,negated_conjecture,
( ~ p42(X350)
| ~ r1(sK300,X347)
| ~ r1(X347,X350)
| r1(X347,sK440(X347))
| p43(X347) ) ).
cnf(u3477,negated_conjecture,
( ~ p43(sK437(X341))
| ~ p43(X341)
| ~ r1(sK300,X341)
| ~ p42(X341)
| p43(X342)
| ~ r1(X341,X342) ) ).
cnf(u3481,negated_conjecture,
( ~ p42(X341)
| ~ p43(X341)
| r1(X341,sK437(X341))
| ~ r1(sK300,X341)
| p43(X342)
| ~ r1(X341,X342) ) ).
cnf(u3485,negated_conjecture,
( ~ p43(X339)
| ~ p43(X340)
| ~ r1(X337,X340)
| ~ r1(sK300,X337)
| ~ r1(sK436(X337),X339)
| p44(X337) ) ).
cnf(u3492,negated_conjecture,
( ~ p43(X340)
| ~ r1(sK300,X337)
| ~ r1(X337,X340)
| r1(X337,sK436(X337))
| p44(X337) ) ).
cnf(u3514,negated_conjecture,
( ~ p44(sK433(X331))
| ~ p44(X331)
| ~ r1(sK300,X331)
| ~ p43(X331)
| p44(X332)
| ~ r1(X331,X332) ) ).
cnf(u3518,negated_conjecture,
( ~ p43(X331)
| ~ p44(X331)
| r1(X331,sK433(X331))
| ~ r1(sK300,X331)
| p44(X332)
| ~ r1(X331,X332) ) ).
cnf(u3522,negated_conjecture,
( ~ p44(X329)
| ~ p44(X330)
| ~ r1(X327,X330)
| ~ r1(sK300,X327)
| ~ r1(sK432(X327),X329)
| p45(X327) ) ).
cnf(u3529,negated_conjecture,
( ~ p44(X330)
| ~ r1(sK300,X327)
| ~ r1(X327,X330)
| r1(X327,sK432(X327))
| p45(X327) ) ).
cnf(u3551,negated_conjecture,
( ~ p45(sK429(X321))
| ~ p45(X321)
| ~ r1(sK300,X321)
| ~ p44(X321)
| p45(X322)
| ~ r1(X321,X322) ) ).
cnf(u3555,negated_conjecture,
( ~ p44(X321)
| ~ p45(X321)
| r1(X321,sK429(X321))
| ~ r1(sK300,X321)
| p45(X322)
| ~ r1(X321,X322) ) ).
cnf(u3559,negated_conjecture,
( ~ p45(X319)
| ~ p45(X320)
| ~ r1(X317,X320)
| ~ r1(sK300,X317)
| ~ r1(sK428(X317),X319)
| p46(X317) ) ).
cnf(u3566,negated_conjecture,
( ~ p45(X320)
| ~ r1(sK300,X317)
| ~ r1(X317,X320)
| r1(X317,sK428(X317))
| p46(X317) ) ).
cnf(u3588,negated_conjecture,
( ~ p46(sK425(X311))
| ~ p46(X311)
| ~ r1(sK300,X311)
| ~ p45(X311)
| p46(X312)
| ~ r1(X311,X312) ) ).
cnf(u3592,negated_conjecture,
( ~ p45(X311)
| ~ p46(X311)
| r1(X311,sK425(X311))
| ~ r1(sK300,X311)
| p46(X312)
| ~ r1(X311,X312) ) ).
cnf(u3596,negated_conjecture,
( ~ p46(X309)
| ~ p46(X310)
| ~ r1(X307,X310)
| ~ r1(sK300,X307)
| ~ r1(sK424(X307),X309)
| p47(X307) ) ).
cnf(u3603,negated_conjecture,
( ~ p46(X310)
| ~ r1(sK300,X307)
| ~ r1(X307,X310)
| r1(X307,sK424(X307))
| p47(X307) ) ).
cnf(u3625,negated_conjecture,
( ~ p47(sK421(X301))
| ~ p47(X301)
| ~ r1(sK300,X301)
| ~ p46(X301)
| p47(X302)
| ~ r1(X301,X302) ) ).
cnf(u3629,negated_conjecture,
( ~ p46(X301)
| ~ p47(X301)
| r1(X301,sK421(X301))
| ~ r1(sK300,X301)
| p47(X302)
| ~ r1(X301,X302) ) ).
cnf(u3633,negated_conjecture,
( ~ p47(X299)
| ~ p47(X300)
| ~ r1(X297,X300)
| ~ r1(sK300,X297)
| ~ r1(sK420(X297),X299)
| p48(X297) ) ).
cnf(u3640,negated_conjecture,
( ~ p47(X300)
| ~ r1(sK300,X297)
| ~ r1(X297,X300)
| r1(X297,sK420(X297))
| p48(X297) ) ).
cnf(u3662,negated_conjecture,
( ~ p48(sK417(X291))
| ~ p48(X291)
| ~ r1(sK300,X291)
| ~ p47(X291)
| p48(X292)
| ~ r1(X291,X292) ) ).
cnf(u3666,negated_conjecture,
( ~ p47(X291)
| ~ p48(X291)
| r1(X291,sK417(X291))
| ~ r1(sK300,X291)
| p48(X292)
| ~ r1(X291,X292) ) ).
cnf(u3670,negated_conjecture,
( ~ p48(X289)
| ~ p48(X290)
| ~ r1(X287,X290)
| ~ r1(sK300,X287)
| ~ r1(sK416(X287),X289)
| p49(X287) ) ).
cnf(u3677,negated_conjecture,
( ~ p48(X290)
| ~ r1(sK300,X287)
| ~ r1(X287,X290)
| r1(X287,sK416(X287))
| p49(X287) ) ).
cnf(u3699,negated_conjecture,
( ~ p49(sK413(X281))
| ~ p49(X281)
| ~ r1(sK300,X281)
| ~ p48(X281)
| p49(X282)
| ~ r1(X281,X282) ) ).
cnf(u3703,negated_conjecture,
( ~ p48(X281)
| ~ p49(X281)
| r1(X281,sK413(X281))
| ~ r1(sK300,X281)
| p49(X282)
| ~ r1(X281,X282) ) ).
cnf(u3707,negated_conjecture,
( ~ p49(X279)
| ~ p49(X280)
| ~ r1(X277,X280)
| ~ r1(sK300,X277)
| ~ r1(sK412(X277),X279)
| p50(X277) ) ).
cnf(u3714,negated_conjecture,
( ~ p49(X280)
| ~ r1(sK300,X277)
| ~ r1(X277,X280)
| r1(X277,sK412(X277))
| p50(X277) ) ).
cnf(u3736,negated_conjecture,
( ~ p50(sK409(X271))
| ~ p50(X271)
| ~ r1(sK300,X271)
| ~ p49(X271)
| p50(X272)
| ~ r1(X271,X272) ) ).
cnf(u3740,negated_conjecture,
( ~ p49(X271)
| ~ p50(X271)
| r1(X271,sK409(X271))
| ~ r1(sK300,X271)
| p50(X272)
| ~ r1(X271,X272) ) ).
cnf(u3744,negated_conjecture,
( ~ p50(X269)
| ~ p50(X270)
| ~ r1(X267,X270)
| ~ r1(sK300,X267)
| ~ r1(sK408(X267),X269)
| p51(X267) ) ).
cnf(u3751,negated_conjecture,
( ~ p50(X270)
| ~ r1(sK300,X267)
| ~ r1(X267,X270)
| r1(X267,sK408(X267))
| p51(X267) ) ).
cnf(u3773,negated_conjecture,
( ~ p51(sK405(X261))
| ~ p51(X261)
| ~ r1(sK300,X261)
| ~ p50(X261)
| p51(X262)
| ~ r1(X261,X262) ) ).
cnf(u3777,negated_conjecture,
( ~ p50(X261)
| ~ p51(X261)
| r1(X261,sK405(X261))
| ~ r1(sK300,X261)
| p51(X262)
| ~ r1(X261,X262) ) ).
cnf(u3781,negated_conjecture,
( ~ p51(X259)
| ~ p51(X260)
| ~ r1(X257,X260)
| ~ r1(sK300,X257)
| ~ r1(sK404(X257),X259)
| p52(X257) ) ).
cnf(u3788,negated_conjecture,
( ~ p51(X260)
| ~ r1(sK300,X257)
| ~ r1(X257,X260)
| r1(X257,sK404(X257))
| p52(X257) ) ).
cnf(u3810,negated_conjecture,
( ~ p52(sK401(X251))
| ~ p52(X251)
| ~ r1(sK300,X251)
| ~ p51(X251)
| p52(X252)
| ~ r1(X251,X252) ) ).
cnf(u3814,negated_conjecture,
( ~ p51(X251)
| ~ p52(X251)
| r1(X251,sK401(X251))
| ~ r1(sK300,X251)
| p52(X252)
| ~ r1(X251,X252) ) ).
cnf(u3818,negated_conjecture,
( ~ p52(X249)
| ~ p52(X250)
| ~ r1(X247,X250)
| ~ r1(sK300,X247)
| ~ r1(sK400(X247),X249)
| p53(X247) ) ).
cnf(u3825,negated_conjecture,
( ~ p52(X250)
| ~ r1(sK300,X247)
| ~ r1(X247,X250)
| r1(X247,sK400(X247))
| p53(X247) ) ).
cnf(u3847,negated_conjecture,
( ~ p53(sK397(X241))
| ~ p53(X241)
| ~ r1(sK300,X241)
| ~ p52(X241)
| p53(X242)
| ~ r1(X241,X242) ) ).
cnf(u3851,negated_conjecture,
( ~ p52(X241)
| ~ p53(X241)
| r1(X241,sK397(X241))
| ~ r1(sK300,X241)
| p53(X242)
| ~ r1(X241,X242) ) ).
cnf(u3855,negated_conjecture,
( ~ p53(X239)
| ~ p53(X240)
| ~ r1(X237,X240)
| ~ r1(sK300,X237)
| ~ r1(sK396(X237),X239)
| p54(X237) ) ).
cnf(u3862,negated_conjecture,
( ~ p53(X240)
| ~ r1(sK300,X237)
| ~ r1(X237,X240)
| r1(X237,sK396(X237))
| p54(X237) ) ).
cnf(u3884,negated_conjecture,
( ~ p54(sK393(X231))
| ~ p54(X231)
| ~ r1(sK300,X231)
| ~ p53(X231)
| p54(X232)
| ~ r1(X231,X232) ) ).
cnf(u3888,negated_conjecture,
( ~ p53(X231)
| ~ p54(X231)
| r1(X231,sK393(X231))
| ~ r1(sK300,X231)
| p54(X232)
| ~ r1(X231,X232) ) ).
cnf(u3892,negated_conjecture,
( ~ p54(X229)
| ~ p54(X230)
| ~ r1(X227,X230)
| ~ r1(sK300,X227)
| ~ r1(sK392(X227),X229)
| p55(X227) ) ).
cnf(u3899,negated_conjecture,
( ~ p54(X230)
| ~ r1(sK300,X227)
| ~ r1(X227,X230)
| r1(X227,sK392(X227))
| p55(X227) ) ).
cnf(u3921,negated_conjecture,
( ~ p55(sK389(X221))
| ~ p55(X221)
| ~ r1(sK300,X221)
| ~ p54(X221)
| p55(X222)
| ~ r1(X221,X222) ) ).
cnf(u3925,negated_conjecture,
( ~ p54(X221)
| ~ p55(X221)
| r1(X221,sK389(X221))
| ~ r1(sK300,X221)
| p55(X222)
| ~ r1(X221,X222) ) ).
cnf(u3929,negated_conjecture,
( ~ p55(X219)
| ~ p55(X220)
| ~ r1(X217,X220)
| ~ r1(sK300,X217)
| ~ r1(sK388(X217),X219)
| p56(X217) ) ).
cnf(u3936,negated_conjecture,
( ~ p55(X220)
| ~ r1(sK300,X217)
| ~ r1(X217,X220)
| r1(X217,sK388(X217))
| p56(X217) ) ).
cnf(u3958,negated_conjecture,
( ~ p56(sK385(X211))
| ~ p56(X211)
| ~ r1(sK300,X211)
| ~ p55(X211)
| p56(X212)
| ~ r1(X211,X212) ) ).
cnf(u3962,negated_conjecture,
( ~ p55(X211)
| ~ p56(X211)
| r1(X211,sK385(X211))
| ~ r1(sK300,X211)
| p56(X212)
| ~ r1(X211,X212) ) ).
cnf(u3966,negated_conjecture,
( ~ p56(X209)
| ~ p56(X210)
| ~ r1(X207,X210)
| ~ r1(sK300,X207)
| ~ r1(sK384(X207),X209)
| p57(X207) ) ).
cnf(u3973,negated_conjecture,
( ~ p56(X210)
| ~ r1(sK300,X207)
| ~ r1(X207,X210)
| r1(X207,sK384(X207))
| p57(X207) ) ).
cnf(u3995,negated_conjecture,
( ~ p57(sK381(X201))
| ~ p57(X201)
| ~ r1(sK300,X201)
| ~ p56(X201)
| p57(X202)
| ~ r1(X201,X202) ) ).
cnf(u3999,negated_conjecture,
( ~ p56(X201)
| ~ p57(X201)
| r1(X201,sK381(X201))
| ~ r1(sK300,X201)
| p57(X202)
| ~ r1(X201,X202) ) ).
cnf(u4003,negated_conjecture,
( ~ p57(X199)
| ~ p57(X200)
| ~ r1(X197,X200)
| ~ r1(sK300,X197)
| ~ r1(sK380(X197),X199)
| p58(X197) ) ).
cnf(u4010,negated_conjecture,
( ~ p57(X200)
| ~ r1(sK300,X197)
| ~ r1(X197,X200)
| r1(X197,sK380(X197))
| p58(X197) ) ).
cnf(u4032,negated_conjecture,
( ~ p58(sK377(X191))
| ~ p58(X191)
| ~ r1(sK300,X191)
| ~ p57(X191)
| p58(X192)
| ~ r1(X191,X192) ) ).
cnf(u4036,negated_conjecture,
( ~ p57(X191)
| ~ p58(X191)
| r1(X191,sK377(X191))
| ~ r1(sK300,X191)
| p58(X192)
| ~ r1(X191,X192) ) ).
cnf(u4040,negated_conjecture,
( ~ p58(X189)
| ~ p58(X190)
| ~ r1(X187,X190)
| ~ r1(sK300,X187)
| ~ r1(sK376(X187),X189)
| p59(X187) ) ).
cnf(u4047,negated_conjecture,
( ~ p58(X190)
| ~ r1(sK300,X187)
| ~ r1(X187,X190)
| r1(X187,sK376(X187))
| p59(X187) ) ).
cnf(u4069,negated_conjecture,
( ~ p59(sK373(X181))
| ~ p59(X181)
| ~ r1(sK300,X181)
| ~ p58(X181)
| p59(X182)
| ~ r1(X181,X182) ) ).
cnf(u4073,negated_conjecture,
( ~ p58(X181)
| ~ p59(X181)
| r1(X181,sK373(X181))
| ~ r1(sK300,X181)
| p59(X182)
| ~ r1(X181,X182) ) ).
cnf(u4077,negated_conjecture,
( ~ p59(X179)
| ~ p59(X180)
| ~ r1(X177,X180)
| ~ r1(sK300,X177)
| ~ r1(sK372(X177),X179)
| p60(X177) ) ).
cnf(u4084,negated_conjecture,
( ~ p59(X180)
| ~ r1(sK300,X177)
| ~ r1(X177,X180)
| r1(X177,sK372(X177))
| p60(X177) ) ).
cnf(u4106,negated_conjecture,
( ~ p60(sK369(X171))
| ~ p60(X171)
| ~ r1(sK300,X171)
| ~ p59(X171)
| p60(X172)
| ~ r1(X171,X172) ) ).
cnf(u4110,negated_conjecture,
( ~ p59(X171)
| ~ p60(X171)
| r1(X171,sK369(X171))
| ~ r1(sK300,X171)
| p60(X172)
| ~ r1(X171,X172) ) ).
cnf(u4114,negated_conjecture,
( ~ p60(X169)
| ~ p60(X170)
| ~ r1(X167,X170)
| ~ r1(sK300,X167)
| ~ r1(sK368(X167),X169)
| p61(X167) ) ).
cnf(u4121,negated_conjecture,
( ~ p60(X170)
| ~ r1(sK300,X167)
| ~ r1(X167,X170)
| r1(X167,sK368(X167))
| p61(X167) ) ).
cnf(u4143,negated_conjecture,
( ~ p61(sK365(X161))
| ~ p61(X161)
| ~ r1(sK300,X161)
| ~ p60(X161)
| p61(X162)
| ~ r1(X161,X162) ) ).
cnf(u4147,negated_conjecture,
( ~ p60(X161)
| ~ p61(X161)
| r1(X161,sK365(X161))
| ~ r1(sK300,X161)
| p61(X162)
| ~ r1(X161,X162) ) ).
cnf(u4151,negated_conjecture,
( ~ p61(X159)
| ~ p61(X160)
| ~ r1(X157,X160)
| ~ r1(sK300,X157)
| ~ r1(sK364(X157),X159)
| p62(X157) ) ).
cnf(u4158,negated_conjecture,
( ~ p61(X160)
| ~ r1(sK300,X157)
| ~ r1(X157,X160)
| r1(X157,sK364(X157))
| p62(X157) ) ).
cnf(u4180,negated_conjecture,
( ~ p62(sK361(X151))
| ~ p62(X151)
| ~ r1(sK300,X151)
| ~ p61(X151)
| p62(X152)
| ~ r1(X151,X152) ) ).
cnf(u4184,negated_conjecture,
( ~ p61(X151)
| ~ p62(X151)
| r1(X151,sK361(X151))
| ~ r1(sK300,X151)
| p62(X152)
| ~ r1(X151,X152) ) ).
cnf(u4188,negated_conjecture,
( ~ p62(X149)
| ~ p62(X150)
| ~ r1(X147,X150)
| ~ r1(sK300,X147)
| ~ r1(sK360(X147),X149)
| p63(X147) ) ).
cnf(u4195,negated_conjecture,
( ~ p62(X150)
| ~ r1(sK300,X147)
| ~ r1(X147,X150)
| r1(X147,sK360(X147))
| p63(X147) ) ).
cnf(u4217,negated_conjecture,
( ~ p63(sK357(X141))
| ~ p63(X141)
| ~ r1(sK300,X141)
| ~ p62(X141)
| p63(X142)
| ~ r1(X141,X142) ) ).
cnf(u4221,negated_conjecture,
( ~ p62(X141)
| ~ p63(X141)
| r1(X141,sK357(X141))
| ~ r1(sK300,X141)
| p63(X142)
| ~ r1(X141,X142) ) ).
cnf(u4225,negated_conjecture,
( ~ p63(X139)
| ~ p63(X140)
| ~ r1(X137,X140)
| ~ r1(sK300,X137)
| ~ r1(sK356(X137),X139)
| p64(X137) ) ).
cnf(u4232,negated_conjecture,
( ~ p63(X140)
| ~ r1(sK300,X137)
| ~ r1(X137,X140)
| r1(X137,sK356(X137))
| p64(X137) ) ).
cnf(u4254,negated_conjecture,
( ~ p64(sK353(X131))
| ~ p64(X131)
| ~ r1(sK300,X131)
| ~ p63(X131)
| p64(X132)
| ~ r1(X131,X132) ) ).
cnf(u4258,negated_conjecture,
( ~ p63(X131)
| ~ p64(X131)
| r1(X131,sK353(X131))
| ~ r1(sK300,X131)
| p64(X132)
| ~ r1(X131,X132) ) ).
cnf(u4262,negated_conjecture,
( ~ p64(X129)
| ~ p64(X130)
| ~ r1(X127,X130)
| ~ r1(sK300,X127)
| ~ r1(sK352(X127),X129)
| p65(X127) ) ).
cnf(u4269,negated_conjecture,
( ~ p64(X130)
| ~ r1(sK300,X127)
| ~ r1(X127,X130)
| r1(X127,sK352(X127))
| p65(X127) ) ).
cnf(u4291,negated_conjecture,
( ~ p65(sK349(X121))
| ~ p65(X121)
| ~ r1(sK300,X121)
| ~ p64(X121)
| p65(X122)
| ~ r1(X121,X122) ) ).
cnf(u4295,negated_conjecture,
( ~ p64(X121)
| ~ p65(X121)
| r1(X121,sK349(X121))
| ~ r1(sK300,X121)
| p65(X122)
| ~ r1(X121,X122) ) ).
cnf(u4299,negated_conjecture,
( ~ p65(X119)
| ~ p65(X120)
| ~ r1(X117,X120)
| ~ r1(sK300,X117)
| ~ r1(sK348(X117),X119)
| p66(X117) ) ).
cnf(u4306,negated_conjecture,
( ~ p65(X120)
| ~ r1(sK300,X117)
| ~ r1(X117,X120)
| r1(X117,sK348(X117))
| p66(X117) ) ).
cnf(u4328,negated_conjecture,
( ~ p66(sK345(X111))
| ~ p66(X111)
| ~ r1(sK300,X111)
| ~ p65(X111)
| p66(X112)
| ~ r1(X111,X112) ) ).
cnf(u4332,negated_conjecture,
( ~ p65(X111)
| ~ p66(X111)
| r1(X111,sK345(X111))
| ~ r1(sK300,X111)
| p66(X112)
| ~ r1(X111,X112) ) ).
cnf(u4336,negated_conjecture,
( ~ p66(X109)
| ~ p66(X110)
| ~ r1(X107,X110)
| ~ r1(sK300,X107)
| ~ r1(sK344(X107),X109)
| p67(X107) ) ).
cnf(u4343,negated_conjecture,
( ~ p66(X110)
| ~ r1(sK300,X107)
| ~ r1(X107,X110)
| r1(X107,sK344(X107))
| p67(X107) ) ).
cnf(u4365,negated_conjecture,
( ~ p67(sK341(X101))
| ~ p67(X101)
| ~ r1(sK300,X101)
| ~ p66(X101)
| p67(X102)
| ~ r1(X101,X102) ) ).
cnf(u4369,negated_conjecture,
( ~ p66(X101)
| ~ p67(X101)
| r1(X101,sK341(X101))
| ~ r1(sK300,X101)
| p67(X102)
| ~ r1(X101,X102) ) ).
cnf(u4373,negated_conjecture,
( ~ p67(X99)
| ~ p67(X100)
| ~ r1(X97,X100)
| ~ r1(sK300,X97)
| ~ r1(sK340(X97),X99)
| p68(X97) ) ).
cnf(u4380,negated_conjecture,
( ~ p67(X100)
| ~ r1(sK300,X97)
| ~ r1(X97,X100)
| r1(X97,sK340(X97))
| p68(X97) ) ).
cnf(u4402,negated_conjecture,
( ~ p68(sK337(X91))
| ~ p68(X91)
| ~ r1(sK300,X91)
| ~ p67(X91)
| p68(X92)
| ~ r1(X91,X92) ) ).
cnf(u4406,negated_conjecture,
( ~ p67(X91)
| ~ p68(X91)
| r1(X91,sK337(X91))
| ~ r1(sK300,X91)
| p68(X92)
| ~ r1(X91,X92) ) ).
cnf(u4410,negated_conjecture,
( ~ p68(X89)
| ~ p68(X90)
| ~ r1(X87,X90)
| ~ r1(sK300,X87)
| ~ r1(sK336(X87),X89)
| p69(X87) ) ).
cnf(u4417,negated_conjecture,
( ~ p68(X90)
| ~ r1(sK300,X87)
| ~ r1(X87,X90)
| r1(X87,sK336(X87))
| p69(X87) ) ).
cnf(u4439,negated_conjecture,
( ~ p69(sK333(X81))
| ~ p69(X81)
| ~ r1(sK300,X81)
| ~ p68(X81)
| p69(X82)
| ~ r1(X81,X82) ) ).
cnf(u4443,negated_conjecture,
( ~ p68(X81)
| ~ p69(X81)
| r1(X81,sK333(X81))
| ~ r1(sK300,X81)
| p69(X82)
| ~ r1(X81,X82) ) ).
cnf(u4447,negated_conjecture,
( ~ p69(X79)
| ~ p69(X80)
| ~ r1(X77,X80)
| ~ r1(sK300,X77)
| ~ r1(sK332(X77),X79)
| p70(X77) ) ).
cnf(u4454,negated_conjecture,
( ~ p69(X80)
| ~ r1(sK300,X77)
| ~ r1(X77,X80)
| r1(X77,sK332(X77))
| p70(X77) ) ).
cnf(u4476,negated_conjecture,
( ~ p70(sK329(X71))
| ~ p70(X71)
| ~ r1(sK300,X71)
| ~ p69(X71)
| p70(X72)
| ~ r1(X71,X72) ) ).
cnf(u4480,negated_conjecture,
( ~ p69(X71)
| ~ p70(X71)
| r1(X71,sK329(X71))
| ~ r1(sK300,X71)
| p70(X72)
| ~ r1(X71,X72) ) ).
cnf(u4484,negated_conjecture,
( ~ p70(X69)
| ~ p70(X70)
| ~ r1(X67,X70)
| ~ r1(sK300,X67)
| ~ r1(sK328(X67),X69)
| p71(X67) ) ).
cnf(u4491,negated_conjecture,
( ~ p70(X70)
| ~ r1(sK300,X67)
| ~ r1(X67,X70)
| r1(X67,sK328(X67))
| p71(X67) ) ).
cnf(u4513,negated_conjecture,
( ~ p71(sK325(X61))
| ~ p71(X61)
| ~ r1(sK300,X61)
| ~ p70(X61)
| p71(X62)
| ~ r1(X61,X62) ) ).
cnf(u4517,negated_conjecture,
( ~ p70(X61)
| ~ p71(X61)
| r1(X61,sK325(X61))
| ~ r1(sK300,X61)
| p71(X62)
| ~ r1(X61,X62) ) ).
cnf(u4521,negated_conjecture,
( ~ p71(X59)
| ~ p71(X60)
| ~ r1(X57,X60)
| ~ r1(sK300,X57)
| ~ r1(sK324(X57),X59)
| p72(X57) ) ).
cnf(u4528,negated_conjecture,
( ~ p71(X60)
| ~ r1(sK300,X57)
| ~ r1(X57,X60)
| r1(X57,sK324(X57))
| p72(X57) ) ).
cnf(u4550,negated_conjecture,
( ~ p72(sK321(X51))
| ~ p72(X51)
| ~ r1(sK300,X51)
| ~ p71(X51)
| p72(X52)
| ~ r1(X51,X52) ) ).
cnf(u4554,negated_conjecture,
( ~ p71(X51)
| ~ p72(X51)
| r1(X51,sK321(X51))
| ~ r1(sK300,X51)
| p72(X52)
| ~ r1(X51,X52) ) ).
cnf(u4558,negated_conjecture,
( ~ p72(X49)
| ~ p72(X50)
| ~ r1(X47,X50)
| ~ r1(sK300,X47)
| ~ r1(sK320(X47),X49)
| p73(X47) ) ).
cnf(u4565,negated_conjecture,
( ~ p72(X50)
| ~ r1(sK300,X47)
| ~ r1(X47,X50)
| r1(X47,sK320(X47))
| p73(X47) ) ).
cnf(u4587,negated_conjecture,
( ~ p73(sK317(X41))
| ~ p73(X41)
| ~ r1(sK300,X41)
| ~ p72(X41)
| p73(X42)
| ~ r1(X41,X42) ) ).
cnf(u4591,negated_conjecture,
( ~ p72(X41)
| ~ p73(X41)
| r1(X41,sK317(X41))
| ~ r1(sK300,X41)
| p73(X42)
| ~ r1(X41,X42) ) ).
cnf(u4595,negated_conjecture,
( ~ p73(X39)
| ~ p73(X40)
| ~ r1(X37,X40)
| ~ r1(sK300,X37)
| ~ r1(sK316(X37),X39)
| p74(X37) ) ).
cnf(u4602,negated_conjecture,
( ~ p73(X40)
| ~ r1(sK300,X37)
| ~ r1(X37,X40)
| r1(X37,sK316(X37))
| p74(X37) ) ).
cnf(u4624,negated_conjecture,
( ~ p74(sK313(X31))
| ~ p74(X31)
| ~ r1(sK300,X31)
| ~ p73(X31)
| p74(X32)
| ~ r1(X31,X32) ) ).
cnf(u4628,negated_conjecture,
( ~ p73(X31)
| ~ p74(X31)
| r1(X31,sK313(X31))
| ~ r1(sK300,X31)
| p74(X32)
| ~ r1(X31,X32) ) ).
cnf(u4632,negated_conjecture,
( ~ p74(X29)
| ~ p74(X30)
| ~ r1(X27,X30)
| ~ r1(sK300,X27)
| ~ r1(sK312(X27),X29)
| p75(X27) ) ).
cnf(u4639,negated_conjecture,
( ~ p74(X30)
| ~ r1(sK300,X27)
| ~ r1(X27,X30)
| r1(X27,sK312(X27))
| p75(X27) ) ).
cnf(u4661,negated_conjecture,
( ~ p75(sK309(X21))
| ~ p75(X21)
| ~ r1(sK300,X21)
| ~ p74(X21)
| p75(X22)
| ~ r1(X21,X22) ) ).
cnf(u4665,negated_conjecture,
( ~ p74(X21)
| ~ p75(X21)
| r1(X21,sK309(X21))
| ~ r1(sK300,X21)
| p75(X22)
| ~ r1(X21,X22) ) ).
cnf(u4669,negated_conjecture,
( ~ p75(X19)
| ~ p75(X20)
| ~ r1(X17,X20)
| ~ r1(sK300,X17)
| ~ r1(sK308(X17),X19)
| p76(X17) ) ).
cnf(u4676,negated_conjecture,
( ~ p75(X20)
| ~ r1(sK300,X17)
| ~ r1(X17,X20)
| r1(X17,sK308(X17))
| p76(X17) ) ).
cnf(u4698,negated_conjecture,
( ~ p76(sK305(X11))
| ~ p76(X11)
| ~ r1(sK300,X11)
| ~ p75(X11)
| p76(X12)
| ~ r1(X11,X12) ) ).
cnf(u4702,negated_conjecture,
( ~ p75(X11)
| ~ p76(X11)
| r1(X11,sK305(X11))
| ~ r1(sK300,X11)
| p76(X12)
| ~ r1(X11,X12) ) ).
cnf(u4706,negated_conjecture,
( ~ p76(X9)
| ~ p76(X10)
| ~ r1(X7,X10)
| ~ r1(sK300,X7)
| ~ r1(sK304(X7),X9)
| p77(X7) ) ).
cnf(u4713,negated_conjecture,
( ~ p76(X10)
| ~ r1(sK300,X7)
| ~ r1(X7,X10)
| r1(X7,sK304(X7))
| p77(X7) ) ).
cnf(u4735,negated_conjecture,
( ~ p77(sK301(X1))
| ~ p77(X1)
| ~ r1(sK300,X1)
| ~ p76(X1)
| p77(X2)
| ~ r1(X1,X2) ) ).
cnf(u4739,negated_conjecture,
( ~ p76(X1)
| ~ p77(X1)
| r1(X1,sK301(X1))
| ~ r1(sK300,X1)
| p77(X2)
| ~ r1(X1,X2) ) ).
cnf(u5266,negated_conjecture,
p2(sK449) ).
cnf(u5276,negated_conjecture,
p2(sK450) ).
cnf(u5359,negated_conjecture,
p20(sK296(sK449)) ).
cnf(u5369,negated_conjecture,
p20(sK296(sK450)) ).
cnf(u7070,negated_conjecture,
~ p13(sK449) ).
cnf(u7058,negated_conjecture,
~ p13(sK450) ).
cnf(u6616,negated_conjecture,
p20(sK269(sK449)) ).
cnf(u6619,negated_conjecture,
p12(sK449) ).
cnf(u6626,negated_conjecture,
p20(sK269(sK450)) ).
cnf(u6629,negated_conjecture,
p12(sK450) ).
cnf(u7032,negated_conjecture,
~ r1(sK300,sK300) ).
cnf(u661,axiom,
( ~ p48(sK163(X1))
| p48(X1)
| ~ r1(X0,X1)
| p47(X1)
| ~ sP45(X0) ) ).
cnf(u1021,axiom,
( ~ p17(sK253(X1))
| p17(X1)
| ~ r1(X0,X1)
| p16(X1)
| ~ sP15(X0) ) ).
cnf(u778,axiom,
( ~ sP35(X0)
| p37(X1)
| p36(sK192(X1))
| p36(X1)
| ~ r1(X0,X1) ) ).
cnf(u1158,axiom,
( ~ sP4(X0)
| p6(X1)
| r1(sK285(X1),sK286(X1))
| r1(X1,sK287(X1))
| ~ r1(X0,X1) ) ).
cnf(u550,axiom,
( ~ sP54(X0)
| p57(X1)
| p56(sK135(X1))
| p56(X1)
| ~ r1(X0,X1) ) ).
cnf(u1019,axiom,
( ~ p17(sK254(X1))
| p17(X1)
| p16(sK252(X1))
| ~ r1(X0,X1)
| ~ sP15(X0) ) ).
cnf(u784,axiom,
( ~ sP35(X0)
| p37(X1)
| r1(sK192(X1),sK193(X1))
| p36(X1)
| ~ r1(X0,X1) ) ).
cnf(u1070,axiom,
( ~ p13(sK266(X1))
| p13(X1)
| ~ p13(sK265(X1))
| ~ r1(X0,X1)
| ~ sP11(X0) ) ).
cnf(u556,axiom,
( ~ sP54(X0)
| p57(X1)
| r1(sK135(X1),sK136(X1))
| p56(X1)
| ~ r1(X0,X1) ) ).
cnf(u521,axiom,
( ~ p60(sK128(X1))
| p60(X1)
| r1(sK126(X1),sK127(X1))
| ~ r1(X0,X1)
| ~ sP57(X0) ) ).
cnf(u406,axiom,
( ~ sP66(X0)
| p69(X1)
| p68(sK99(X1))
| p68(X1)
| ~ r1(X0,X1) ) ).
cnf(u805,axiom,
( ~ p35(sK199(X1))
| p35(X1)
| ~ r1(X0,X1)
| p34(X1)
| ~ sP33(X0) ) ).
cnf(u1193,axiom,
( ~ p3(sK296(X1))
| p3(X1)
| r1(sK294(X1),sK295(X1))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u535,axiom,
( ~ sP56(X0)
| p59(X1)
| r1(X1,sK129(X1))
| p58(X1)
| ~ r1(X0,X1) ) ).
cnf(u906,axiom,
( ~ sP25(X0)
| p27(X1)
| r1(sK222(X1),sK223(X1))
| r1(X1,sK224(X1))
| ~ r1(X0,X1) ) ).
cnf(u803,axiom,
( ~ p35(sK200(X1))
| p35(X1)
| p34(sK198(X1))
| ~ r1(X0,X1)
| ~ sP33(X0) ) ).
cnf(u678,axiom,
( ~ sP44(X0)
| p47(X1)
| r1(sK165(X1),sK166(X1))
| r1(X1,sK167(X1))
| ~ r1(X0,X1) ) ).
cnf(u912,axiom,
( ~ sP24(X0)
| p26(X1)
| p25(sK225(X1))
| r1(X1,sK227(X1))
| ~ r1(X0,X1) ) ).
cnf(u1196,axiom,
( ~ p3(sK296(X1))
| p3(X1)
| r1(X1,sK294(X1))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u417,axiom,
( ~ sP66(X0)
| p69(X1)
| r1(X1,sK99(X1))
| r1(X1,sK101(X1))
| ~ r1(X0,X1) ) ).
cnf(u649,axiom,
( ~ p49(sK160(X1))
| p49(X1)
| ~ r1(X0,X1)
| p48(X1)
| ~ sP46(X0) ) ).
cnf(u404,axiom,
( ~ p70(sK98(X1))
| p70(X1)
| r1(X1,sK96(X1))
| ~ r1(X0,X1)
| ~ sP67(X0) ) ).
cnf(u933,axiom,
( ~ sP23(X0)
| p25(X1)
| r1(X1,sK228(X1))
| r1(X1,sK230(X1))
| ~ r1(X0,X1) ) ).
cnf(u818,axiom,
( ~ p34(sK203(X1))
| p34(X1)
| ~ p34(sK202(X1))
| ~ r1(X0,X1)
| ~ sP32(X0) ) ).
cnf(u1593,negated_conjecture,
( ~ r1(sK449,X372)
| p20(X372) ) ).
cnf(u663,axiom,
( ~ p48(sK163(X1))
| p48(X1)
| ~ r1(X0,X1)
| r1(X1,sK164(X1))
| ~ sP45(X0) ) ).
cnf(u538,axiom,
( ~ sP55(X0)
| p58(X1)
| p57(sK132(X1))
| p57(X1)
| ~ r1(X0,X1) ) ).
cnf(u931,axiom,
( ~ sP23(X0)
| p25(X1)
| r1(X1,sK228(X1))
| p24(X1)
| ~ r1(X0,X1) ) ).
cnf(u824,axiom,
( ~ p34(sK203(X1))
| p34(X1)
| r1(X1,sK201(X1))
| ~ r1(X0,X1)
| ~ sP32(X0) ) ).
cnf(u544,axiom,
( ~ sP55(X0)
| p58(X1)
| r1(sK132(X1),sK133(X1))
| p57(X1)
| ~ r1(X0,X1) ) ).
cnf(u423,axiom,
( ~ p68(sK103(X1))
| p68(X1)
| ~ r1(X0,X1)
| r1(X1,sK104(X1))
| ~ sP65(X0) ) ).
cnf(u561,axiom,
( ~ sP54(X0)
| p57(X1)
| r1(X1,sK135(X1))
| r1(X1,sK137(X1))
| ~ r1(X0,X1) ) ).
cnf(u316,axiom,
( ~ sP74(X0)
| p77(X1)
| r1(sK75(X1),sK76(X1))
| p76(X1)
| ~ r1(X0,X1) ) ).
cnf(u4746,negated_conjecture,
( r1(X0,sK296(X0))
| r1(X0,sK294(X0))
| p3(X0)
| ~ r1(sK300,X0) ) ).
cnf(u1169,axiom,
( ~ p5(sK290(X1))
| p5(X1)
| r1(sK288(X1),sK289(X1))
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u1077,axiom,
( ~ sP11(X0)
| p13(X1)
| r1(X1,sK264(X1))
| r1(X1,sK266(X1))
| ~ r1(X0,X1) ) ).
cnf(u575,axiom,
( ~ p55(sK143(X1))
| p55(X1)
| p54(sK141(X1))
| ~ r1(X0,X1)
| ~ sP52(X0) ) ).
cnf(u946,axiom,
( ~ sP21(X0)
| p23(X1)
| p22(sK234(X1))
| p22(X1)
| ~ r1(X0,X1) ) ).
cnf(u666,axiom,
( ~ sP45(X0)
| p48(X1)
| r1(sK162(X1),sK163(X1))
| r1(X1,sK164(X1))
| ~ r1(X0,X1) ) ).
cnf(u4876,negated_conjecture,
( r1(X0,sK267(X0))
| p12(X0)
| p11(X0)
| ~ r1(sK300,X0) ) ).
cnf(u952,axiom,
( ~ sP21(X0)
| p23(X1)
| r1(sK234(X1),sK235(X1))
| p22(X1)
| ~ r1(X0,X1) ) ).
cnf(u421,axiom,
( ~ p68(sK103(X1))
| p68(X1)
| ~ r1(X0,X1)
| p67(X1)
| ~ sP65(X0) ) ).
cnf(u672,axiom,
( ~ sP44(X0)
| p47(X1)
| p46(sK165(X1))
| r1(X1,sK167(X1))
| ~ r1(X0,X1) ) ).
cnf(u1081,axiom,
( ~ p12(sK268(X1))
| p12(X1)
| ~ r1(X0,X1)
| p11(X1)
| ~ sP10(X0) ) ).
cnf(u444,axiom,
( ~ sP63(X0)
| p66(X1)
| p65(sK108(X1))
| r1(X1,sK110(X1))
| ~ r1(X0,X1) ) ).
cnf(u995,axiom,
( ~ p19(sK248(X1))
| p19(X1)
| p18(sK246(X1))
| ~ r1(X0,X1)
| ~ sP17(X0) ) ).
cnf(u822,axiom,
( ~ sP32(X0)
| p34(X1)
| r1(sK201(X1),sK202(X1))
| r1(X1,sK203(X1))
| ~ r1(X0,X1) ) ).
cnf(u1010,axiom,
( ~ p18(sK251(X1))
| p18(X1)
| ~ p18(sK250(X1))
| ~ r1(X0,X1)
| ~ sP16(X0) ) ).
cnf(u703,axiom,
( ~ sP42(X0)
| p45(X1)
| r1(X1,sK171(X1))
| p44(X1)
| ~ r1(X0,X1) ) ).
cnf(u6996,negated_conjecture,
( ~ p20(sK269(sK526(X1)))
| ~ r1(X1,X0)
| ~ p20(X0)
| ~ r1(sK300,X1)
| p21(X1)
| r1(sK526(X1),sK267(sK526(X1)))
| p12(sK526(X1))
| ~ r1(sK300,sK526(X1)) ) ).
cnf(u1186,axiom,
( ~ sP1(X0)
| p3(X1)
| p2(sK294(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u785,axiom,
( ~ p37(sK194(X1))
| p37(X1)
| r1(sK192(X1),sK193(X1))
| ~ r1(X0,X1)
| ~ sP35(X0) ) ).
cnf(u828,axiom,
( ~ sP31(X0)
| p33(X1)
| p32(sK204(X1))
| r1(X1,sK206(X1))
| ~ r1(X0,X1) ) ).
cnf(u746,axiom,
( ~ p41(sK185(X1))
| p41(X1)
| ~ p41(sK184(X1))
| ~ r1(X0,X1)
| ~ sP38(X0) ) ).
cnf(u335,axiom,
( ~ p75(sK83(X1))
| p75(X1)
| p74(sK81(X1))
| ~ r1(X0,X1)
| ~ sP72(X0) ) ).
cnf(u571,axiom,
( ~ sP53(X0)
| p56(X1)
| r1(X1,sK138(X1))
| p55(X1)
| ~ r1(X0,X1) ) ).
cnf(u1087,axiom,
( ~ sP10(X0)
| p12(X1)
| r1(X1,sK267(X1))
| p11(X1)
| ~ r1(X0,X1) ) ).
cnf(u1209,axiom,
( ~ sP0(X0)
| p2(X1)
| r1(X1,sK297(X1))
| r1(X1,sK299(X1))
| ~ r1(X0,X1) ) ).
cnf(u7022,negated_conjecture,
( ~ r1(X0,sK449)
| ~ r1(sK300,X0)
| r1(X0,sK598(X0))
| p3(X0) ) ).
cnf(u1034,axiom,
( ~ p16(sK257(X1))
| p16(X1)
| ~ p16(sK256(X1))
| ~ r1(X0,X1)
| ~ sP14(X0) ) ).
cnf(u578,axiom,
( ~ p55(sK143(X1))
| p55(X1)
| ~ p55(sK142(X1))
| ~ r1(X0,X1)
| ~ sP52(X0) ) ).
cnf(u956,axiom,
( ~ p23(sK236(X1))
| p23(X1)
| r1(X1,sK234(X1))
| ~ r1(X0,X1)
| ~ sP21(X0) ) ).
cnf(u1094,axiom,
( ~ p11(sK272(X1))
| p11(X1)
| ~ p11(sK271(X1))
| ~ r1(X0,X1)
| ~ sP9(X0) ) ).
cnf(u333,axiom,
( ~ sP73(X0)
| p76(X1)
| r1(X1,sK78(X1))
| r1(X1,sK80(X1))
| ~ r1(X0,X1) ) ).
cnf(u584,axiom,
( ~ p55(sK143(X1))
| p55(X1)
| r1(X1,sK141(X1))
| ~ r1(X0,X1)
| ~ sP52(X0) ) ).
cnf(u432,axiom,
( ~ sP64(X0)
| p67(X1)
| p66(sK105(X1))
| r1(X1,sK107(X1))
| ~ r1(X0,X1) ) ).
cnf(u833,axiom,
( ~ p33(sK206(X1))
| p33(X1)
| r1(sK204(X1),sK205(X1))
| ~ r1(X0,X1)
| ~ sP31(X0) ) ).
cnf(u1068,axiom,
( ~ sP11(X0)
| p13(X1)
| p12(sK264(X1))
| r1(X1,sK266(X1))
| ~ r1(X0,X1) ) ).
cnf(u1117,axiom,
( ~ p9(sK277(X1))
| p9(X1)
| ~ r1(X0,X1)
| p8(X1)
| ~ sP7(X0) ) ).
cnf(u948,axiom,
( ~ sP21(X0)
| p23(X1)
| p22(sK234(X1))
| r1(X1,sK236(X1))
| ~ r1(X0,X1) ) ).
cnf(u847,axiom,
( ~ sP30(X0)
| p32(X1)
| r1(X1,sK207(X1))
| p31(X1)
| ~ r1(X0,X1) ) ).
cnf(u1098,axiom,
( ~ sP9(X0)
| p11(X1)
| r1(sK270(X1),sK271(X1))
| r1(X1,sK272(X1))
| ~ r1(X0,X1) ) ).
cnf(u636,axiom,
( ~ sP47(X0)
| p50(X1)
| p49(sK156(X1))
| r1(X1,sK158(X1))
| ~ r1(X0,X1) ) ).
cnf(u1092,axiom,
( ~ sP9(X0)
| p11(X1)
| p10(sK270(X1))
| r1(X1,sK272(X1))
| ~ r1(X0,X1) ) ).
cnf(u323,axiom,
( ~ p76(sK80(X1))
| p76(X1)
| p75(sK78(X1))
| ~ r1(X0,X1)
| ~ sP73(X0) ) ).
cnf(u1115,axiom,
( ~ p9(sK278(X1))
| p9(X1)
| p8(sK276(X1))
| ~ r1(X0,X1)
| ~ sP7(X0) ) ).
cnf(u461,axiom,
( ~ p65(sK113(X1))
| p65(X1)
| r1(sK111(X1),sK112(X1))
| ~ r1(X0,X1)
| ~ sP62(X0) ) ).
cnf(u712,axiom,
( ~ sP41(X0)
| p44(X1)
| r1(sK174(X1),sK175(X1))
| p43(X1)
| ~ r1(X0,X1) ) ).
cnf(u7011,negated_conjecture,
( ~ r1(sK598(X1),sK450)
| ~ r1(X1,X0)
| ~ r1(sK300,X1)
| ~ p2(X0)
| p3(X1) ) ).
cnf(u346,axiom,
( ~ sP71(X0)
| p74(X1)
| p73(sK84(X1))
| p73(X1)
| ~ r1(X0,X1) ) ).
cnf(u961,axiom,
( ~ p22(sK238(X1))
| p22(X1)
| ~ r1(X0,X1)
| p21(X1)
| ~ sP20(X0) ) ).
cnf(u1107,axiom,
( ~ p10(sK274(X1))
| p10(X1)
| ~ r1(X0,X1)
| r1(X1,sK275(X1))
| ~ sP8(X0) ) ).
cnf(u862,axiom,
( ~ sP28(X0)
| p30(X1)
| p29(sK213(X1))
| p29(X1)
| ~ r1(X0,X1) ) ).
cnf(u975,axiom,
( ~ p21(sK241(X1))
| p21(X1)
| ~ r1(X0,X1)
| r1(X1,sK242(X1))
| ~ sP19(X0) ) ).
cnf(u479,axiom,
( ~ p63(sK119(X1))
| p63(X1)
| p62(sK117(X1))
| ~ r1(X0,X1)
| ~ sP60(X0) ) ).
cnf(u868,axiom,
( ~ sP28(X0)
| p30(X1)
| r1(sK213(X1),sK214(X1))
| p29(X1)
| ~ r1(X0,X1) ) ).
cnf(u1134,axiom,
( ~ sP6(X0)
| p8(X1)
| r1(sK279(X1),sK280(X1))
| r1(X1,sK281(X1))
| ~ r1(X0,X1) ) ).
cnf(u451,axiom,
( ~ sP63(X0)
| p66(X1)
| r1(X1,sK108(X1))
| p65(X1)
| ~ r1(X0,X1) ) ).
cnf(u344,axiom,
( ~ p75(sK83(X1))
| p75(X1)
| r1(X1,sK81(X1))
| ~ r1(X0,X1)
| ~ sP72(X0) ) ).
cnf(u1127,axiom,
( ~ p8(sK281(X1))
| p8(X1)
| p7(sK279(X1))
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u474,axiom,
( ~ sP61(X0)
| p64(X1)
| r1(sK114(X1),sK115(X1))
| r1(X1,sK116(X1))
| ~ r1(X0,X1) ) ).
cnf(u873,axiom,
( ~ sP28(X0)
| p30(X1)
| r1(X1,sK213(X1))
| r1(X1,sK215(X1))
| ~ r1(X0,X1) ) ).
cnf(u889,axiom,
( ~ p28(sK220(X1))
| p28(X1)
| ~ r1(X0,X1)
| p27(X1)
| ~ sP26(X0) ) ).
cnf(u603,axiom,
( ~ p53(sK148(X1))
| p53(X1)
| ~ r1(X0,X1)
| r1(X1,sK149(X1))
| ~ sP50(X0) ) ).
cnf(u990,axiom,
( ~ sP18(X0)
| p20(X1)
| r1(sK243(X1),sK244(X1))
| r1(X1,sK245(X1))
| ~ r1(X0,X1) ) ).
cnf(u744,axiom,
( ~ sP38(X0)
| p41(X1)
| p40(sK183(X1))
| r1(X1,sK185(X1))
| ~ r1(X0,X1) ) ).
cnf(u887,axiom,
( ~ p28(sK221(X1))
| p28(X1)
| p27(sK219(X1))
| ~ r1(X0,X1)
| ~ sP26(X0) ) ).
cnf(u1132,axiom,
( ~ sP6(X0)
| p8(X1)
| r1(sK279(X1),sK280(X1))
| p7(X1)
| ~ r1(X0,X1) ) ).
cnf(u363,axiom,
( ~ p73(sK88(X1))
| p73(X1)
| ~ r1(X0,X1)
| r1(X1,sK89(X1))
| ~ sP70(X0) ) ).
cnf(u716,axiom,
( ~ p44(sK176(X1))
| p44(X1)
| r1(X1,sK174(X1))
| ~ r1(X0,X1)
| ~ sP41(X0) ) ).
cnf(u350,axiom,
( ~ p74(sK86(X1))
| p74(X1)
| ~ p74(sK85(X1))
| ~ r1(X0,X1)
| ~ sP71(X0) ) ).
cnf(u733,axiom,
( ~ p42(sK181(X1))
| p42(X1)
| ~ r1(X0,X1)
| p41(X1)
| ~ sP39(X0) ) ).
cnf(u472,axiom,
( ~ sP61(X0)
| p64(X1)
| r1(sK114(X1),sK115(X1))
| p63(X1)
| ~ r1(X0,X1) ) ).
cnf(u1001,axiom,
( ~ p19(sK248(X1))
| p19(X1)
| r1(sK246(X1),sK247(X1))
| ~ r1(X0,X1)
| ~ sP17(X0) ) ).
cnf(u389,axiom,
( ~ p71(sK95(X1))
| p71(X1)
| r1(sK93(X1),sK94(X1))
| ~ r1(X0,X1)
| ~ sP68(X0) ) ).
cnf(u1147,axiom,
( ~ sP5(X0)
| p7(X1)
| r1(X1,sK282(X1))
| p6(X1)
| ~ r1(X0,X1) ) ).
cnf(u731,axiom,
( ~ p42(sK182(X1))
| p42(X1)
| p41(sK180(X1))
| ~ r1(X0,X1)
| ~ sP39(X0) ) ).
cnf(u655,axiom,
( ~ sP46(X0)
| p49(X1)
| r1(X1,sK159(X1))
| p48(X1)
| ~ r1(X0,X1) ) ).
cnf(u1136,axiom,
( ~ p8(sK281(X1))
| p8(X1)
| r1(X1,sK279(X1))
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u1015,axiom,
( ~ sP16(X0)
| p18(X1)
| r1(X1,sK249(X1))
| p17(X1)
| ~ r1(X0,X1) ) ).
cnf(u866,axiom,
( ~ p30(sK215(X1))
| p30(X1)
| ~ p30(sK214(X1))
| ~ r1(X0,X1)
| ~ sP28(X0) ) ).
cnf(u361,axiom,
( ~ p73(sK88(X1))
| p73(X1)
| ~ r1(X0,X1)
| p72(X1)
| ~ sP70(X0) ) ).
cnf(u628,axiom,
( ~ sP48(X0)
| p51(X1)
| r1(sK153(X1),sK154(X1))
| p50(X1)
| ~ r1(X0,X1) ) ).
cnf(u893,axiom,
( ~ p28(sK221(X1))
| p28(X1)
| r1(sK219(X1),sK220(X1))
| ~ r1(X0,X1)
| ~ sP26(X0) ) ).
cnf(u517,axiom,
( ~ p60(sK127(X1))
| p60(X1)
| ~ r1(X0,X1)
| p59(X1)
| ~ sP57(X0) ) ).
cnf(u478,axiom,
( ~ sP60(X0)
| p63(X1)
| p62(sK117(X1))
| p62(X1)
| ~ r1(X0,X1) ) ).
cnf(u877,axiom,
( ~ p29(sK217(X1))
| p29(X1)
| ~ r1(X0,X1)
| p28(X1)
| ~ sP27(X0) ) ).
cnf(u515,axiom,
( ~ p60(sK128(X1))
| p60(X1)
| p59(sK126(X1))
| ~ r1(X0,X1)
| ~ sP57(X0) ) ).
cnf(u658,axiom,
( ~ sP45(X0)
| p48(X1)
| p47(sK162(X1))
| p47(X1)
| ~ r1(X0,X1) ) ).
cnf(u875,axiom,
( ~ p29(sK218(X1))
| p29(X1)
| p28(sK216(X1))
| ~ r1(X0,X1)
| ~ sP27(X0) ) ).
cnf(u750,axiom,
( ~ sP38(X0)
| p41(X1)
| r1(sK183(X1),sK184(X1))
| r1(X1,sK185(X1))
| ~ r1(X0,X1) ) ).
cnf(u455,axiom,
( ~ p65(sK113(X1))
| p65(X1)
| p64(sK111(X1))
| ~ r1(X0,X1)
| ~ sP62(X0) ) ).
cnf(u1061,axiom,
( ~ p14(sK263(X1))
| p14(X1)
| r1(sK261(X1),sK262(X1))
| ~ r1(X0,X1)
| ~ sP12(X0) ) ).
cnf(u984,axiom,
( ~ sP18(X0)
| p20(X1)
| p19(sK243(X1))
| r1(X1,sK245(X1))
| ~ r1(X0,X1) ) ).
cnf(u1044,axiom,
( ~ sP13(X0)
| p15(X1)
| p14(sK258(X1))
| r1(X1,sK260(X1))
| ~ r1(X0,X1) ) ).
cnf(u489,axiom,
( ~ sP60(X0)
| p63(X1)
| r1(X1,sK117(X1))
| r1(X1,sK119(X1))
| ~ r1(X0,X1) ) ).
cnf(u756,axiom,
( ~ sP37(X0)
| p39(X1)
| p38(sK186(X1))
| r1(X1,sK188(X1))
| ~ r1(X0,X1) ) ).
cnf(u645,axiom,
( ~ sP47(X0)
| p50(X1)
| r1(X1,sK156(X1))
| r1(X1,sK158(X1))
| ~ r1(X0,X1) ) ).
cnf(u1005,axiom,
( ~ sP17(X0)
| p19(X1)
| r1(X1,sK246(X1))
| r1(X1,sK248(X1))
| ~ r1(X0,X1) ) ).
cnf(u890,axiom,
( ~ p28(sK221(X1))
| p28(X1)
| ~ p28(sK220(X1))
| ~ r1(X0,X1)
| ~ sP26(X0) ) ).
cnf(u1106,axiom,
( ~ p10(sK275(X1))
| p10(X1)
| ~ p10(sK274(X1))
| ~ r1(X0,X1)
| ~ sP8(X0) ) ).
cnf(u643,axiom,
( ~ sP47(X0)
| p50(X1)
| r1(X1,sK156(X1))
| p49(X1)
| ~ r1(X0,X1) ) ).
cnf(u534,axiom,
( ~ sP56(X0)
| p59(X1)
| r1(sK129(X1),sK130(X1))
| r1(X1,sK131(X1))
| ~ r1(X0,X1) ) ).
cnf(u1003,axiom,
( ~ sP17(X0)
| p19(X1)
| r1(X1,sK246(X1))
| p18(X1)
| ~ r1(X0,X1) ) ).
cnf(u1146,axiom,
( ~ sP5(X0)
| p7(X1)
| r1(sK282(X1),sK283(X1))
| r1(X1,sK284(X1))
| ~ r1(X0,X1) ) ).
cnf(u768,axiom,
( ~ sP36(X0)
| p38(X1)
| p37(sK189(X1))
| r1(X1,sK191(X1))
| ~ r1(X0,X1) ) ).
cnf(u1187,axiom,
( ~ p3(sK296(X1))
| p3(X1)
| p2(sK294(X1))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u495,axiom,
( ~ p62(sK121(X1))
| p62(X1)
| ~ r1(X0,X1)
| r1(X1,sK122(X1))
| ~ sP59(X0) ) ).
cnf(u633,axiom,
( ~ sP48(X0)
| p51(X1)
| r1(X1,sK153(X1))
| r1(X1,sK155(X1))
| ~ r1(X0,X1) ) ).
cnf(u390,axiom,
( ~ sP68(X0)
| p71(X1)
| r1(sK93(X1),sK94(X1))
| r1(X1,sK95(X1))
| ~ r1(X0,X1) ) ).
cnf(u789,axiom,
( ~ sP35(X0)
| p37(X1)
| r1(X1,sK192(X1))
| r1(X1,sK194(X1))
| ~ r1(X0,X1) ) ).
cnf(u1091,axiom,
( ~ p11(sK272(X1))
| p11(X1)
| p10(sK270(X1))
| ~ r1(X0,X1)
| ~ sP9(X0) ) ).
cnf(u519,axiom,
( ~ p60(sK127(X1))
| p60(X1)
| ~ r1(X0,X1)
| r1(X1,sK128(X1))
| ~ sP57(X0) ) ).
cnf(u1018,axiom,
( ~ sP15(X0)
| p17(X1)
| p16(sK252(X1))
| p16(X1)
| ~ r1(X0,X1) ) ).
cnf(u1182,axiom,
( ~ sP2(X0)
| p4(X1)
| r1(sK291(X1),sK292(X1))
| r1(X1,sK293(X1))
| ~ r1(X0,X1) ) ).
cnf(u787,axiom,
( ~ sP35(X0)
| p37(X1)
| r1(X1,sK192(X1))
| p36(X1)
| ~ r1(X0,X1) ) ).
cnf(u662,axiom,
( ~ p48(sK164(X1))
| p48(X1)
| ~ p48(sK163(X1))
| ~ r1(X0,X1)
| ~ sP45(X0) ) ).
cnf(u896,axiom,
( ~ p28(sK221(X1))
| p28(X1)
| r1(X1,sK219(X1))
| ~ r1(X0,X1)
| ~ sP26(X0) ) ).
cnf(u761,axiom,
( ~ p39(sK188(X1))
| p39(X1)
| r1(sK186(X1),sK187(X1))
| ~ r1(X0,X1)
| ~ sP37(X0) ) ).
cnf(u388,axiom,
( ~ sP68(X0)
| p71(X1)
| r1(sK93(X1),sK94(X1))
| p70(X1)
| ~ r1(X0,X1) ) ).
cnf(u398,axiom,
( ~ p70(sK98(X1))
| p70(X1)
| ~ p70(sK97(X1))
| ~ r1(X0,X1)
| ~ sP67(X0) ) ).
cnf(u917,axiom,
( ~ p26(sK227(X1))
| p26(X1)
| r1(sK225(X1),sK226(X1))
| ~ r1(X0,X1)
| ~ sP24(X0) ) ).
cnf(u802,axiom,
( ~ sP33(X0)
| p35(X1)
| p34(sK198(X1))
| p34(X1)
| ~ r1(X0,X1) ) ).
cnf(u647,axiom,
( ~ p49(sK161(X1))
| p49(X1)
| p48(sK159(X1))
| ~ r1(X0,X1)
| ~ sP46(X0) ) ).
cnf(u522,axiom,
( ~ sP57(X0)
| p60(X1)
| r1(sK126(X1),sK127(X1))
| r1(X1,sK128(X1))
| ~ r1(X0,X1) ) ).
cnf(u1180,axiom,
( ~ sP2(X0)
| p4(X1)
| r1(sK291(X1),sK292(X1))
| p3(X1)
| ~ r1(X0,X1) ) ).
cnf(u915,axiom,
( ~ p26(sK226(X1))
| p26(X1)
| ~ r1(X0,X1)
| r1(X1,sK227(X1))
| ~ sP24(X0) ) ).
cnf(u808,axiom,
( ~ sP33(X0)
| p35(X1)
| r1(sK198(X1),sK199(X1))
| p34(X1)
| ~ r1(X0,X1) ) ).
cnf(u528,axiom,
( ~ sP56(X0)
| p59(X1)
| p58(sK129(X1))
| r1(X1,sK131(X1))
| ~ r1(X0,X1) ) ).
cnf(u407,axiom,
( ~ p69(sK101(X1))
| p69(X1)
| p68(sK99(X1))
| ~ r1(X0,X1)
| ~ sP66(X0) ) ).
cnf(u1130,axiom,
( ~ p8(sK281(X1))
| p8(X1)
| ~ p8(sK280(X1))
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u545,axiom,
( ~ p58(sK134(X1))
| p58(X1)
| r1(sK132(X1),sK133(X1))
| ~ r1(X0,X1)
| ~ sP55(X0) ) ).
cnf(u1153,axiom,
( ~ p6(sK286(X1))
| p6(X1)
| ~ r1(X0,X1)
| p5(X1)
| ~ sP4(X0) ) ).
cnf(u829,axiom,
( ~ p33(sK205(X1))
| p33(X1)
| ~ r1(X0,X1)
| p32(X1)
| ~ sP31(X0) ) ).
cnf(u930,axiom,
( ~ sP23(X0)
| p25(X1)
| r1(sK228(X1),sK229(X1))
| r1(X1,sK230(X1))
| ~ r1(X0,X1) ) ).
cnf(u503,axiom,
( ~ p61(sK125(X1))
| p61(X1)
| p60(sK123(X1))
| ~ r1(X0,X1)
| ~ sP58(X0) ) ).
cnf(u1042,axiom,
( ~ sP13(X0)
| p15(X1)
| p14(sK258(X1))
| p14(X1)
| ~ r1(X0,X1) ) ).
cnf(u7091,negated_conjecture,
( ~ p20(sK269(sK526(X0)))
| p12(sK526(X0))
| ~ r1(sK300,sK526(X0))
| ~ p20(X1)
| ~ r1(X0,X1)
| p11(sK267(sK526(X0)))
| ~ r1(sK300,X0)
| p21(X0) ) ).
cnf(u319,axiom,
( ~ sP74(X0)
| p77(X1)
| r1(X1,sK75(X1))
| p76(X1)
| ~ r1(X0,X1) ) ).
cnf(u405,axiom,
( ~ sP67(X0)
| p70(X1)
| r1(X1,sK96(X1))
| r1(X1,sK98(X1))
| ~ r1(X0,X1) ) ).
cnf(u656,axiom,
( ~ p49(sK161(X1))
| p49(X1)
| r1(X1,sK159(X1))
| ~ r1(X0,X1)
| ~ sP46(X0) ) ).
cnf(u673,axiom,
( ~ p47(sK166(X1))
| p47(X1)
| ~ r1(X0,X1)
| p46(X1)
| ~ sP44(X0) ) ).
cnf(u428,axiom,
( ~ p68(sK104(X1))
| p68(X1)
| r1(X1,sK102(X1))
| ~ r1(X0,X1)
| ~ sP65(X0) ) ).
cnf(u1189,axiom,
( ~ p3(sK295(X1))
| p3(X1)
| ~ r1(X0,X1)
| p2(X1)
| ~ sP1(X0) ) ).
cnf(u687,axiom,
( ~ p46(sK169(X1))
| p46(X1)
| ~ r1(X0,X1)
| r1(X1,sK170(X1))
| ~ sP43(X0) ) ).
cnf(u562,axiom,
( ~ sP53(X0)
| p56(X1)
| p55(sK138(X1))
| p55(X1)
| ~ r1(X0,X1) ) ).
cnf(u1170,axiom,
( ~ sP3(X0)
| p5(X1)
| r1(sK288(X1),sK289(X1))
| r1(X1,sK290(X1))
| ~ r1(X0,X1) ) ).
cnf(u713,axiom,
( ~ p44(sK176(X1))
| p44(X1)
| r1(sK174(X1),sK175(X1))
| ~ r1(X0,X1)
| ~ sP41(X0) ) ).
cnf(u812,axiom,
( ~ p35(sK200(X1))
| p35(X1)
| r1(X1,sK198(X1))
| ~ r1(X0,X1)
| ~ sP33(X0) ) ).
cnf(u1078,axiom,
( ~ sP10(X0)
| p12(X1)
| p11(sK267(X1))
| p11(X1)
| ~ r1(X0,X1) ) ).
cnf(u317,axiom,
( ~ p77(sK77(X1))
| p77(X1)
| r1(sK75(X1),sK76(X1))
| ~ r1(X0,X1)
| ~ sP74(X0) ) ).
cnf(u568,axiom,
( ~ sP53(X0)
| p56(X1)
| r1(sK138(X1),sK139(X1))
| p55(X1)
| ~ r1(X0,X1) ) ).
cnf(u447,axiom,
( ~ p66(sK109(X1))
| p66(X1)
| ~ r1(X0,X1)
| r1(X1,sK110(X1))
| ~ sP63(X0) ) ).
cnf(u1071,axiom,
( ~ p13(sK265(X1))
| p13(X1)
| ~ r1(X0,X1)
| r1(X1,sK266(X1))
| ~ sP11(X0) ) ).
cnf(u418,axiom,
( ~ sP65(X0)
| p68(X1)
| p67(sK102(X1))
| p67(X1)
| ~ r1(X0,X1) ) ).
cnf(u817,axiom,
( ~ p34(sK202(X1))
| p34(X1)
| ~ r1(X0,X1)
| p33(X1)
| ~ sP32(X0) ) ).
cnf(u769,axiom,
( ~ p38(sK190(X1))
| p38(X1)
| ~ r1(X0,X1)
| p37(X1)
| ~ sP36(X0) ) ).
cnf(u934,axiom,
( ~ sP22(X0)
| p24(X1)
| p23(sK231(X1))
| p23(X1)
| ~ r1(X0,X1) ) ).
cnf(u730,axiom,
( ~ sP39(X0)
| p42(X1)
| p41(sK180(X1))
| p41(X1)
| ~ r1(X0,X1) ) ).
cnf(u831,axiom,
( ~ p33(sK205(X1))
| p33(X1)
| ~ r1(X0,X1)
| r1(X1,sK206(X1))
| ~ sP31(X0) ) ).
cnf(u690,axiom,
( ~ sP43(X0)
| p46(X1)
| r1(sK168(X1),sK169(X1))
| r1(X1,sK170(X1))
| ~ r1(X0,X1) ) ).
cnf(u809,axiom,
( ~ p35(sK200(X1))
| p35(X1)
| r1(sK198(X1),sK199(X1))
| ~ r1(X0,X1)
| ~ sP33(X0) ) ).
cnf(u1041,axiom,
( ~ sP14(X0)
| p16(X1)
| r1(X1,sK255(X1))
| r1(X1,sK257(X1))
| ~ r1(X0,X1) ) ).
cnf(u940,axiom,
( ~ sP22(X0)
| p24(X1)
| r1(sK231(X1),sK232(X1))
| p23(X1)
| ~ r1(X0,X1) ) ).
cnf(u1206,axiom,
( ~ sP0(X0)
| p2(X1)
| r1(sK297(X1),sK298(X1))
| r1(X1,sK299(X1))
| ~ r1(X0,X1) ) ).
cnf(u445,axiom,
( ~ p66(sK109(X1))
| p66(X1)
| ~ r1(X0,X1)
| p65(X1)
| ~ sP63(X0) ) ).
cnf(u696,axiom,
( ~ sP42(X0)
| p45(X1)
| p44(sK171(X1))
| r1(X1,sK173(X1))
| ~ r1(X0,X1) ) ).
cnf(u416,axiom,
( ~ p69(sK101(X1))
| p69(X1)
| r1(X1,sK99(X1))
| ~ r1(X0,X1)
| ~ sP66(X0) ) ).
cnf(u1199,axiom,
( ~ p2(sK299(X1))
| p2(X1)
| p1(sK297(X1))
| ~ r1(X0,X1)
| ~ sP0(X0) ) ).
cnf(u945,axiom,
( ~ sP22(X0)
| p24(X1)
| r1(X1,sK231(X1))
| r1(X1,sK233(X1))
| ~ r1(X0,X1) ) ).
cnf(u542,axiom,
( ~ p58(sK134(X1))
| p58(X1)
| ~ p58(sK133(X1))
| ~ r1(X0,X1)
| ~ sP55(X0) ) ).
cnf(u1101,axiom,
( ~ sP9(X0)
| p11(X1)
| r1(X1,sK270(X1))
| r1(X1,sK272(X1))
| ~ r1(X0,X1) ) ).
cnf(u1080,axiom,
( ~ sP10(X0)
| p12(X1)
| p11(sK267(X1))
| r1(X1,sK269(X1))
| ~ r1(X0,X1) ) ).
cnf(u959,axiom,
( ~ p22(sK239(X1))
| p22(X1)
| p21(sK237(X1))
| ~ r1(X0,X1)
| ~ sP20(X0) ) ).
cnf(u983,axiom,
( ~ p20(sK245(X1))
| p20(X1)
| p19(sK243(X1))
| ~ r1(X0,X1)
| ~ sP18(X0) ) ).
cnf(u1204,axiom,
( ~ sP0(X0)
| p2(X1)
| r1(sK297(X1),sK298(X1))
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u435,axiom,
( ~ p67(sK106(X1))
| p67(X1)
| ~ r1(X0,X1)
| r1(X1,sK107(X1))
| ~ sP64(X0) ) ).
cnf(u1052,axiom,
( ~ p15(sK260(X1))
| p15(X1)
| r1(X1,sK258(X1))
| ~ r1(X0,X1)
| ~ sP13(X0) ) ).
cnf(u7012,negated_conjecture,
( ~ r1(X0,sK450)
| ~ r1(sK300,X0)
| r1(X0,sK598(X0))
| p3(X0) ) ).
cnf(u330,axiom,
( ~ sP73(X0)
| p76(X1)
| r1(sK78(X1),sK79(X1))
| r1(X1,sK80(X1))
| ~ r1(X0,X1) ) ).
cnf(u650,axiom,
( ~ p49(sK161(X1))
| p49(X1)
| ~ p49(sK160(X1))
| ~ r1(X0,X1)
| ~ sP46(X0) ) ).
cnf(u846,axiom,
( ~ sP30(X0)
| p32(X1)
| r1(sK207(X1),sK208(X1))
| r1(X1,sK209(X1))
| ~ r1(X0,X1) ) ).
cnf(u1208,axiom,
( ~ p2(sK299(X1))
| p2(X1)
| r1(X1,sK297(X1))
| ~ r1(X0,X1)
| ~ sP0(X0) ) ).
cnf(u852,axiom,
( ~ sP29(X0)
| p31(X1)
| p30(sK210(X1))
| r1(X1,sK212(X1))
| ~ r1(X0,X1) ) ).
cnf(u1118,axiom,
( ~ p9(sK278(X1))
| p9(X1)
| ~ p9(sK277(X1))
| ~ r1(X0,X1)
| ~ sP7(X0) ) ).
cnf(u589,axiom,
( ~ p54(sK145(X1))
| p54(X1)
| ~ r1(X0,X1)
| p53(X1)
| ~ sP51(X0) ) ).
cnf(u328,axiom,
( ~ sP73(X0)
| p76(X1)
| r1(sK78(X1),sK79(X1))
| p75(X1)
| ~ r1(X0,X1) ) ).
cnf(u1111,axiom,
( ~ sP8(X0)
| p10(X1)
| r1(X1,sK273(X1))
| p9(X1)
| ~ r1(X0,X1) ) ).
cnf(u458,axiom,
( ~ p65(sK113(X1))
| p65(X1)
| ~ p65(sK112(X1))
| ~ r1(X0,X1)
| ~ sP62(X0) ) ).
cnf(u857,axiom,
( ~ p31(sK212(X1))
| p31(X1)
| r1(sK210(X1),sK211(X1))
| ~ r1(X0,X1)
| ~ sP29(X0) ) ).
cnf(u499,axiom,
( ~ sP59(X0)
| p62(X1)
| r1(X1,sK120(X1))
| p61(X1)
| ~ r1(X0,X1) ) ).
cnf(u5060,negated_conjecture,
( ~ r1(sK300,X0)
| p11(sK267(X0))
| p11(X0)
| p12(X0) ) ).
cnf(u587,axiom,
( ~ p54(sK146(X1))
| p54(X1)
| p53(sK144(X1))
| ~ r1(X0,X1)
| ~ sP51(X0) ) ).
cnf(u974,axiom,
( ~ p21(sK242(X1))
| p21(X1)
| ~ p21(sK241(X1))
| ~ r1(X0,X1)
| ~ sP19(X0) ) ).
cnf(u5034,negated_conjecture,
( r1(X0,sK269(X0))
| p11(sK267(X0))
| p12(X0)
| ~ r1(sK300,X0) ) ).
cnf(u871,axiom,
( ~ sP28(X0)
| p30(X1)
| r1(X1,sK213(X1))
| p29(X1)
| ~ r1(X0,X1) ) ).
cnf(u853,axiom,
( ~ p31(sK211(X1))
| p31(X1)
| ~ r1(X0,X1)
| p30(X1)
| ~ sP29(X0) ) ).
cnf(u1116,axiom,
( ~ sP7(X0)
| p9(X1)
| p8(sK276(X1))
| r1(X1,sK278(X1))
| ~ r1(X0,X1) ) ).
cnf(u347,axiom,
( ~ p74(sK86(X1))
| p74(X1)
| p73(sK84(X1))
| ~ r1(X0,X1)
| ~ sP71(X0) ) ).
cnf(u373,axiom,
( ~ p72(sK91(X1))
| p72(X1)
| ~ r1(X0,X1)
| p71(X1)
| ~ sP69(X0) ) ).
cnf(u334,axiom,
( ~ sP72(X0)
| p75(X1)
| p74(sK81(X1))
| p74(X1)
| ~ r1(X0,X1) ) ).
cnf(u717,axiom,
( ~ sP41(X0)
| p44(X1)
| r1(X1,sK174(X1))
| r1(X1,sK176(X1))
| ~ r1(X0,X1) ) ).
cnf(u456,axiom,
( ~ sP62(X0)
| p65(X1)
| p64(sK111(X1))
| r1(X1,sK113(X1))
| ~ r1(X0,X1) ) ).
cnf(u985,axiom,
( ~ p20(sK244(X1))
| p20(X1)
| ~ r1(X0,X1)
| p19(X1)
| ~ sP18(X0) ) ).
cnf(u1131,axiom,
( ~ p8(sK280(X1))
| p8(X1)
| ~ r1(X0,X1)
| r1(X1,sK281(X1))
| ~ sP6(X0) ) ).
cnf(u715,axiom,
( ~ sP41(X0)
| p44(X1)
| r1(X1,sK174(X1))
| p43(X1)
| ~ r1(X0,X1) ) ).
cnf(u606,axiom,
( ~ sP50(X0)
| p53(X1)
| r1(sK147(X1),sK148(X1))
| r1(X1,sK149(X1))
| ~ r1(X0,X1) ) ).
cnf(u1120,axiom,
( ~ sP7(X0)
| p9(X1)
| r1(sK276(X1),sK277(X1))
| p8(X1)
| ~ r1(X0,X1) ) ).
cnf(u999,axiom,
( ~ p19(sK247(X1))
| p19(X1)
| ~ r1(X0,X1)
| r1(X1,sK248(X1))
| ~ sP17(X0) ) ).
cnf(u345,axiom,
( ~ sP72(X0)
| p75(X1)
| r1(X1,sK81(X1))
| r1(X1,sK83(X1))
| ~ r1(X0,X1) ) ).
cnf(u612,axiom,
( ~ sP49(X0)
| p52(X1)
| p51(sK150(X1))
| r1(X1,sK152(X1))
| ~ r1(X0,X1) ) ).
cnf(u475,axiom,
( ~ sP61(X0)
| p64(X1)
| r1(X1,sK114(X1))
| p63(X1)
| ~ r1(X0,X1) ) ).
cnf(u722,axiom,
( ~ p43(sK179(X1))
| p43(X1)
| ~ p43(sK178(X1))
| ~ r1(X0,X1)
| ~ sP40(X0) ) ).
cnf(u629,axiom,
( ~ p51(sK155(X1))
| p51(X1)
| r1(sK153(X1),sK154(X1))
| ~ r1(X0,X1)
| ~ sP48(X0) ) ).
cnf(u368,axiom,
( ~ p73(sK89(X1))
| p73(X1)
| r1(X1,sK87(X1))
| ~ r1(X0,X1)
| ~ sP70(X0) ) ).
cnf(u462,axiom,
( ~ sP62(X0)
| p65(X1)
| r1(sK111(X1),sK112(X1))
| r1(X1,sK113(X1))
| ~ r1(X0,X1) ) ).
cnf(u861,axiom,
( ~ sP29(X0)
| p31(X1)
| r1(X1,sK210(X1))
| r1(X1,sK212(X1))
| ~ r1(X0,X1) ) ).
cnf(u859,axiom,
( ~ sP29(X0)
| p31(X1)
| r1(X1,sK210(X1))
| p30(X1)
| ~ r1(X0,X1) ) ).
cnf(u386,axiom,
( ~ p71(sK95(X1))
| p71(X1)
| ~ p71(sK94(X1))
| ~ r1(X0,X1)
| ~ sP68(X0) ) ).
cnf(u968,axiom,
( ~ p22(sK239(X1))
| p22(X1)
| r1(X1,sK237(X1))
| ~ r1(X0,X1)
| ~ sP20(X0) ) ).
cnf(u1028,axiom,
( ~ p17(sK254(X1))
| p17(X1)
| r1(X1,sK252(X1))
| ~ r1(X0,X1)
| ~ sP15(X0) ) ).
cnf(u473,axiom,
( ~ p64(sK116(X1))
| p64(X1)
| r1(sK114(X1),sK115(X1))
| ~ r1(X0,X1)
| ~ sP61(X0) ) ).
cnf(u740,axiom,
( ~ p42(sK182(X1))
| p42(X1)
| r1(X1,sK180(X1))
| ~ r1(X0,X1)
| ~ sP39(X0) ) ).
cnf(u374,axiom,
( ~ p72(sK92(X1))
| p72(X1)
| ~ p72(sK91(X1))
| ~ r1(X0,X1)
| ~ sP69(X0) ) ).
cnf(u757,axiom,
( ~ p39(sK187(X1))
| p39(X1)
| ~ r1(X0,X1)
| p38(X1)
| ~ sP37(X0) ) ).
cnf(u989,axiom,
( ~ p20(sK245(X1))
| p20(X1)
| r1(sK243(X1),sK244(X1))
| ~ r1(X0,X1)
| ~ sP18(X0) ) ).
cnf(u755,axiom,
( ~ p39(sK188(X1))
| p39(X1)
| p38(sK186(X1))
| ~ r1(X0,X1)
| ~ sP37(X0) ) ).
cnf(u518,axiom,
( ~ p60(sK128(X1))
| p60(X1)
| ~ p60(sK127(X1))
| ~ r1(X0,X1)
| ~ sP57(X0) ) ).
cnf(u1113,axiom,
( ~ sP8(X0)
| p10(X1)
| r1(X1,sK273(X1))
| r1(X1,sK275(X1))
| ~ r1(X0,X1) ) ).
cnf(u880,axiom,
( ~ sP27(X0)
| p29(X1)
| r1(sK216(X1),sK217(X1))
| p28(X1)
| ~ r1(X0,X1) ) ).
cnf(u524,axiom,
( ~ p60(sK128(X1))
| p60(X1)
| r1(X1,sK126(X1))
| ~ r1(X0,X1)
| ~ sP57(X0) ) ).
cnf(u372,axiom,
( ~ sP69(X0)
| p72(X1)
| p71(sK90(X1))
| r1(X1,sK92(X1))
| ~ r1(X0,X1) ) ).
cnf(u502,axiom,
( ~ sP58(X0)
| p61(X1)
| p60(sK123(X1))
| p60(X1)
| ~ r1(X0,X1) ) ).
cnf(u773,axiom,
( ~ p38(sK191(X1))
| p38(X1)
| r1(sK189(X1),sK190(X1))
| ~ r1(X0,X1)
| ~ sP36(X0) ) ).
cnf(u631,axiom,
( ~ sP48(X0)
| p51(X1)
| r1(X1,sK153(X1))
| p50(X1)
| ~ r1(X0,X1) ) ).
cnf(u1002,axiom,
( ~ sP17(X0)
| p19(X1)
| r1(sK246(X1),sK247(X1))
| r1(X1,sK248(X1))
| ~ r1(X0,X1) ) ).
cnf(u771,axiom,
( ~ p38(sK190(X1))
| p38(X1)
| ~ r1(X0,X1)
| r1(X1,sK191(X1))
| ~ sP36(X0) ) ).
cnf(u646,axiom,
( ~ sP46(X0)
| p49(X1)
| p48(sK159(X1))
| p48(X1)
| ~ r1(X0,X1) ) ).
cnf(u1008,axiom,
( ~ sP16(X0)
| p18(X1)
| p17(sK249(X1))
| r1(X1,sK251(X1))
| ~ r1(X0,X1) ) ).
cnf(u385,axiom,
( ~ p71(sK94(X1))
| p71(X1)
| ~ r1(X0,X1)
| p70(X1)
| ~ sP68(X0) ) ).
cnf(u1100,axiom,
( ~ p11(sK272(X1))
| p11(X1)
| r1(X1,sK270(X1))
| ~ r1(X0,X1)
| ~ sP9(X0) ) ).
cnf(u1055,axiom,
( ~ p14(sK263(X1))
| p14(X1)
| p13(sK261(X1))
| ~ r1(X0,X1)
| ~ sP12(X0) ) ).
cnf(u1137,axiom,
( ~ sP6(X0)
| p8(X1)
| r1(X1,sK279(X1))
| r1(X1,sK281(X1))
| ~ r1(X0,X1) ) ).
cnf(u500,axiom,
( ~ p62(sK122(X1))
| p62(X1)
| r1(X1,sK120(X1))
| ~ r1(X0,X1)
| ~ sP59(X0) ) ).
cnf(u901,axiom,
( ~ p27(sK223(X1))
| p27(X1)
| ~ r1(X0,X1)
| p26(X1)
| ~ sP25(X0) ) ).
cnf(u786,axiom,
( ~ sP35(X0)
| p37(X1)
| r1(sK192(X1),sK193(X1))
| r1(X1,sK194(X1))
| ~ r1(X0,X1) ) ).
cnf(u759,axiom,
( ~ p39(sK187(X1))
| p39(X1)
| ~ r1(X0,X1)
| r1(X1,sK188(X1))
| ~ sP37(X0) ) ).
cnf(u634,axiom,
( ~ sP47(X0)
| p50(X1)
| p49(sK156(X1))
| p49(X1)
| ~ r1(X0,X1) ) ).
cnf(u899,axiom,
( ~ p27(sK224(X1))
| p27(X1)
| p26(sK222(X1))
| ~ r1(X0,X1)
| ~ sP25(X0) ) ).
cnf(u792,axiom,
( ~ sP34(X0)
| p36(X1)
| p35(sK195(X1))
| r1(X1,sK197(X1))
| ~ r1(X0,X1) ) ).
cnf(u512,axiom,
( ~ p61(sK125(X1))
| p61(X1)
| r1(X1,sK123(X1))
| ~ r1(X0,X1)
| ~ sP58(X0) ) ).
cnf(u391,axiom,
( ~ sP68(X0)
| p71(X1)
| r1(X1,sK93(X1))
| p70(X1)
| ~ r1(X0,X1) ) ).
cnf(u529,axiom,
( ~ p59(sK130(X1))
| p59(X1)
| ~ r1(X0,X1)
| p58(X1)
| ~ sP56(X0) ) ).
cnf(u1179,axiom,
( ~ p4(sK292(X1))
| p4(X1)
| ~ r1(X0,X1)
| r1(X1,sK293(X1))
| ~ sP2(X0) ) ).
cnf(u1164,axiom,
( ~ sP3(X0)
| p5(X1)
| p4(sK288(X1))
| r1(X1,sK290(X1))
| ~ r1(X0,X1) ) ).
cnf(u1045,axiom,
( ~ p15(sK259(X1))
| p15(X1)
| ~ r1(X0,X1)
| p14(X1)
| ~ sP13(X0) ) ).
cnf(u310,axiom,
( ~ sP74(X0)
| p77(X1)
| p76(sK75(X1))
| p76(X1)
| ~ r1(X0,X1) ) ).
cnf(u543,axiom,
( ~ p58(sK133(X1))
| p58(X1)
| ~ r1(X0,X1)
| r1(X1,sK134(X1))
| ~ sP55(X0) ) ).
cnf(u914,axiom,
( ~ p26(sK227(X1))
| p26(X1)
| ~ p26(sK226(X1))
| ~ r1(X0,X1)
| ~ sP24(X0) ) ).
cnf(u1026,axiom,
( ~ sP15(X0)
| p17(X1)
| r1(sK252(X1),sK253(X1))
| r1(X1,sK254(X1))
| ~ r1(X0,X1) ) ).
cnf(u726,axiom,
( ~ sP40(X0)
| p43(X1)
| r1(sK177(X1),sK178(X1))
| r1(X1,sK179(X1))
| ~ r1(X0,X1) ) ).
cnf(u640,axiom,
( ~ sP47(X0)
| p50(X1)
| r1(sK156(X1),sK157(X1))
| p49(X1)
| ~ r1(X0,X1) ) ).
cnf(u657,axiom,
( ~ sP46(X0)
| p49(X1)
| r1(X1,sK159(X1))
| r1(X1,sK161(X1))
| ~ r1(X0,X1) ) ).
cnf(u412,axiom,
( ~ sP66(X0)
| p69(X1)
| r1(sK99(X1),sK100(X1))
| p68(X1)
| ~ r1(X0,X1) ) ).
cnf(u1031,axiom,
( ~ p16(sK257(X1))
| p16(X1)
| p15(sK255(X1))
| ~ r1(X0,X1)
| ~ sP14(X0) ) ).
cnf(u923,axiom,
( ~ p25(sK230(X1))
| p25(X1)
| p24(sK228(X1))
| ~ r1(X0,X1)
| ~ sP23(X0) ) ).
cnf(u790,axiom,
( ~ sP34(X0)
| p36(X1)
| p35(sK195(X1))
| p35(X1)
| ~ r1(X0,X1) ) ).
cnf(u1173,axiom,
( ~ sP3(X0)
| p5(X1)
| r1(X1,sK288(X1))
| r1(X1,sK290(X1))
| ~ r1(X0,X1) ) ).
cnf(u671,axiom,
( ~ p47(sK167(X1))
| p47(X1)
| p46(sK165(X1))
| ~ r1(X0,X1)
| ~ sP44(X0) ) ).
cnf(u546,axiom,
( ~ sP55(X0)
| p58(X1)
| r1(sK132(X1),sK133(X1))
| r1(X1,sK134(X1))
| ~ r1(X0,X1) ) ).
cnf(u1154,axiom,
( ~ p6(sK287(X1))
| p6(X1)
| ~ p6(sK286(X1))
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u796,axiom,
( ~ sP34(X0)
| p36(X1)
| r1(sK195(X1),sK196(X1))
| p35(X1)
| ~ r1(X0,X1) ) ).
cnf(u1062,axiom,
( ~ sP12(X0)
| p14(X1)
| r1(sK261(X1),sK262(X1))
| r1(X1,sK263(X1))
| ~ r1(X0,X1) ) ).
cnf(u552,axiom,
( ~ sP54(X0)
| p57(X1)
| p56(sK135(X1))
| r1(X1,sK137(X1))
| ~ r1(X0,X1) ) ).
cnf(u431,axiom,
( ~ p67(sK107(X1))
| p67(X1)
| p66(sK105(X1))
| ~ r1(X0,X1)
| ~ sP64(X0) ) ).
cnf(u569,axiom,
( ~ p56(sK140(X1))
| p56(X1)
| r1(sK138(X1),sK139(X1))
| ~ r1(X0,X1)
| ~ sP53(X0) ) ).
cnf(u402,axiom,
( ~ sP67(X0)
| p70(X1)
| r1(sK96(X1),sK97(X1))
| r1(X1,sK98(X1))
| ~ r1(X0,X1) ) ).
cnf(u1177,axiom,
( ~ p4(sK292(X1))
| p4(X1)
| ~ r1(X0,X1)
| p3(X1)
| ~ sP2(X0) ) ).
cnf(u1085,axiom,
( ~ p12(sK269(X1))
| p12(X1)
| r1(sK267(X1),sK268(X1))
| ~ r1(X0,X1)
| ~ sP10(X0) ) ).
cnf(u918,axiom,
( ~ sP24(X0)
| p26(X1)
| r1(sK225(X1),sK226(X1))
| r1(X1,sK227(X1))
| ~ r1(X0,X1) ) ).
cnf(u815,axiom,
( ~ p34(sK203(X1))
| p34(X1)
| p33(sK201(X1))
| ~ r1(X0,X1)
| ~ sP32(X0) ) ).
cnf(u1066,axiom,
( ~ sP11(X0)
| p13(X1)
| p12(sK264(X1))
| p12(X1)
| ~ r1(X0,X1) ) ).
cnf(u737,axiom,
( ~ p42(sK182(X1))
| p42(X1)
| r1(sK180(X1),sK181(X1))
| ~ r1(X0,X1)
| ~ sP39(X0) ) ).
cnf(u7050,negated_conjecture,
( ~ r1(X0,sK450)
| ~ r1(sK300,X0)
| r1(X0,sK558(X0))
| p13(X0) ) ).
cnf(u924,axiom,
( ~ sP23(X0)
| p25(X1)
| p24(sK228(X1))
| r1(X1,sK230(X1))
| ~ r1(X0,X1) ) ).
cnf(u429,axiom,
( ~ sP65(X0)
| p68(X1)
| r1(X1,sK102(X1))
| r1(X1,sK104(X1))
| ~ r1(X0,X1) ) ).
cnf(u680,axiom,
( ~ p47(sK167(X1))
| p47(X1)
| r1(X1,sK165(X1))
| ~ r1(X0,X1)
| ~ sP44(X0) ) ).
cnf(u314,axiom,
( ~ p77(sK77(X1))
| p77(X1)
| ~ p77(sK76(X1))
| ~ r1(X0,X1)
| ~ sP74(X0) ) ).
cnf(u400,axiom,
( ~ sP67(X0)
| p70(X1)
| r1(sK96(X1),sK97(X1))
| p69(X1)
| ~ r1(X0,X1) ) ).
cnf(u1183,axiom,
( ~ sP2(X0)
| p4(X1)
| r1(X1,sK291(X1))
| p3(X1)
| ~ r1(X0,X1) ) ).
cnf(u929,axiom,
( ~ p25(sK230(X1))
| p25(X1)
| r1(sK228(X1),sK229(X1))
| ~ r1(X0,X1)
| ~ sP23(X0) ) ).
cnf(u1075,axiom,
( ~ sP11(X0)
| p13(X1)
| r1(X1,sK264(X1))
| p12(X1)
| ~ r1(X0,X1) ) ).
cnf(u830,axiom,
( ~ p33(sK206(X1))
| p33(X1)
| ~ p33(sK205(X1))
| ~ r1(X0,X1)
| ~ sP31(X0) ) ).
cnf(u539,axiom,
( ~ p58(sK134(X1))
| p58(X1)
| p57(sK132(X1))
| ~ r1(X0,X1)
| ~ sP55(X0) ) ).
cnf(u324,axiom,
( ~ sP73(X0)
| p76(X1)
| p75(sK78(X1))
| r1(X1,sK80(X1))
| ~ r1(X0,X1) ) ).
cnf(u1064,axiom,
( ~ p14(sK263(X1))
| p14(X1)
| r1(X1,sK261(X1))
| ~ r1(X0,X1)
| ~ sP12(X0) ) ).
cnf(u943,axiom,
( ~ sP22(X0)
| p24(X1)
| r1(X1,sK231(X1))
| p23(X1)
| ~ r1(X0,X1) ) ).
cnf(u1194,axiom,
( ~ sP1(X0)
| p3(X1)
| r1(sK294(X1),sK295(X1))
| r1(X1,sK296(X1))
| ~ r1(X0,X1) ) ).
cnf(u341,axiom,
( ~ p75(sK83(X1))
| p75(X1)
| r1(sK81(X1),sK82(X1))
| ~ r1(X0,X1)
| ~ sP72(X0) ) ).
cnf(u1188,axiom,
( ~ sP1(X0)
| p3(X1)
| p2(sK294(X1))
| r1(X1,sK296(X1))
| ~ r1(X0,X1) ) ).
cnf(u419,axiom,
( ~ p68(sK104(X1))
| p68(X1)
| p67(sK102(X1))
| ~ r1(X0,X1)
| ~ sP65(X0) ) ).
cnf(u573,axiom,
( ~ sP53(X0)
| p56(X1)
| r1(X1,sK138(X1))
| r1(X1,sK140(X1))
| ~ r1(X0,X1) ) ).
cnf(u312,axiom,
( ~ sP74(X0)
| p77(X1)
| p76(sK75(X1))
| r1(X1,sK77(X1))
| ~ r1(X0,X1) ) ).
cnf(u442,axiom,
( ~ sP63(X0)
| p66(X1)
| p65(sK108(X1))
| p65(X1)
| ~ r1(X0,X1) ) ).
cnf(u1203,axiom,
( ~ p2(sK298(X1))
| p2(X1)
| ~ r1(X0,X1)
| r1(X1,sK299(X1))
| ~ sP0(X0) ) ).
cnf(u958,axiom,
( ~ sP20(X0)
| p22(X1)
| p21(sK237(X1))
| p21(X1)
| ~ r1(X0,X1) ) ).
cnf(u1192,axiom,
( ~ sP1(X0)
| p3(X1)
| r1(sK294(X1),sK295(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u836,axiom,
( ~ p33(sK206(X1))
| p33(X1)
| r1(X1,sK204(X1))
| ~ r1(X0,X1)
| ~ sP31(X0) ) ).
cnf(u1102,axiom,
( ~ sP8(X0)
| p10(X1)
| p9(sK273(X1))
| p9(X1)
| ~ r1(X0,X1) ) ).
cnf(u684,axiom,
( ~ sP43(X0)
| p46(X1)
| p45(sK168(X1))
| r1(X1,sK170(X1))
| ~ r1(X0,X1) ) ).
cnf(u506,axiom,
( ~ p61(sK125(X1))
| p61(X1)
| ~ p61(sK124(X1))
| ~ r1(X0,X1)
| ~ sP58(X0) ) ).
cnf(u318,axiom,
( ~ sP74(X0)
| p77(X1)
| r1(sK75(X1),sK76(X1))
| r1(X1,sK77(X1))
| ~ r1(X0,X1) ) ).
cnf(u701,axiom,
( ~ p45(sK173(X1))
| p45(X1)
| r1(sK171(X1),sK172(X1))
| ~ r1(X0,X1)
| ~ sP42(X0) ) ).
cnf(u440,axiom,
( ~ p67(sK107(X1))
| p67(X1)
| r1(X1,sK105(X1))
| ~ r1(X0,X1)
| ~ sP64(X0) ) ).
cnf(u1095,axiom,
( ~ p11(sK271(X1))
| p11(X1)
| ~ r1(X0,X1)
| r1(X1,sK272(X1))
| ~ sP9(X0) ) ).
cnf(u841,axiom,
( ~ p32(sK208(X1))
| p32(X1)
| ~ r1(X0,X1)
| p31(X1)
| ~ sP30(X0) ) ).
cnf(u6995,negated_conjecture,
( ~ p20(sK296(sK526(X1)))
| ~ r1(X1,X0)
| ~ p20(X0)
| ~ r1(sK300,X1)
| p21(X1)
| r1(sK526(X1),sK294(sK526(X1)))
| p3(sK526(X1))
| ~ r1(sK300,sK526(X1)) ) ).
cnf(u699,axiom,
( ~ p45(sK172(X1))
| p45(X1)
| ~ r1(X0,X1)
| r1(X1,sK173(X1))
| ~ sP42(X0) ) ).
cnf(u855,axiom,
( ~ p31(sK211(X1))
| p31(X1)
| ~ r1(X0,X1)
| r1(X1,sK212(X1))
| ~ sP29(X0) ) ).
cnf(u6999,negated_conjecture,
( ~ p20(sK294(sK526(X0)))
| p2(sK526(X0))
| ~ r1(sK300,sK526(X0))
| ~ p20(X1)
| ~ r1(X0,X1)
| p3(sK526(X0))
| ~ r1(sK300,X0)
| p21(X0) ) ).
cnf(u964,axiom,
( ~ sP20(X0)
| p22(X1)
| r1(sK237(X1),sK238(X1))
| p21(X1)
| ~ r1(X0,X1) ) ).
cnf(u331,axiom,
( ~ sP73(X0)
| p76(X1)
| r1(X1,sK78(X1))
| p75(X1)
| ~ r1(X0,X1) ) ).
cnf(u446,axiom,
( ~ p66(sK110(X1))
| p66(X1)
| ~ p66(sK109(X1))
| ~ r1(X0,X1)
| ~ sP63(X0) ) ).
cnf(u659,axiom,
( ~ p48(sK164(X1))
| p48(X1)
| p47(sK162(X1))
| ~ r1(X0,X1)
| ~ sP45(X0) ) ).
cnf(u969,axiom,
( ~ sP20(X0)
| p22(X1)
| r1(X1,sK237(X1))
| r1(X1,sK239(X1))
| ~ r1(X0,X1) ) ).
cnf(u590,axiom,
( ~ p54(sK146(X1))
| p54(X1)
| ~ p54(sK145(X1))
| ~ r1(X0,X1)
| ~ sP51(X0) ) ).
cnf(u1104,axiom,
( ~ sP8(X0)
| p10(X1)
| p9(sK273(X1))
| r1(X1,sK275(X1))
| ~ r1(X0,X1) ) ).
cnf(u329,axiom,
( ~ p76(sK80(X1))
| p76(X1)
| r1(sK78(X1),sK79(X1))
| ~ r1(X0,X1)
| ~ sP73(X0) ) ).
cnf(u596,axiom,
( ~ p54(sK146(X1))
| p54(X1)
| r1(X1,sK144(X1))
| ~ r1(X0,X1)
| ~ sP51(X0) ) ).
cnf(u459,axiom,
( ~ p65(sK112(X1))
| p65(X1)
| ~ r1(X0,X1)
| r1(X1,sK113(X1))
| ~ sP62(X0) ) ).
cnf(u613,axiom,
( ~ p52(sK151(X1))
| p52(X1)
| ~ r1(X0,X1)
| p51(X1)
| ~ sP49(X0) ) ).
cnf(u352,axiom,
( ~ sP71(X0)
| p74(X1)
| r1(sK84(X1),sK85(X1))
| p73(X1)
| ~ r1(X0,X1) ) ).
cnf(u611,axiom,
( ~ p52(sK152(X1))
| p52(X1)
| p51(sK150(X1))
| ~ r1(X0,X1)
| ~ sP49(X0) ) ).
cnf(u4804,negated_conjecture,
( r1(X0,sK269(X0))
| r1(X0,sK267(X0))
| p12(X0)
| ~ r1(sK300,X0) ) ).
cnf(u843,axiom,
( ~ p32(sK208(X1))
| p32(X1)
| ~ r1(X0,X1)
| r1(X1,sK209(X1))
| ~ sP30(X0) ) ).
cnf(u718,axiom,
( ~ sP40(X0)
| p43(X1)
| p42(sK177(X1))
| p42(X1)
| ~ r1(X0,X1) ) ).
cnf(u4821,negated_conjecture,
( r1(X0,sK294(X0))
| p3(X0)
| p2(X0)
| ~ r1(sK300,X0) ) ).
cnf(u1140,axiom,
( ~ sP5(X0)
| p7(X1)
| p6(sK282(X1))
| r1(X1,sK284(X1))
| ~ r1(X0,X1) ) ).
cnf(u457,axiom,
( ~ p65(sK112(X1))
| p65(X1)
| ~ r1(X0,X1)
| p64(X1)
| ~ sP62(X0) ) ).
cnf(u724,axiom,
( ~ sP40(X0)
| p43(X1)
| r1(sK177(X1),sK178(X1))
| p42(X1)
| ~ r1(X0,X1) ) ).
cnf(u358,axiom,
( ~ sP70(X0)
| p73(X1)
| p72(sK87(X1))
| p72(X1)
| ~ r1(X0,X1) ) ).
cnf(u741,axiom,
( ~ sP39(X0)
| p42(X1)
| r1(X1,sK180(X1))
| r1(X1,sK182(X1))
| ~ r1(X0,X1) ) ).
cnf(u973,axiom,
( ~ p21(sK241(X1))
| p21(X1)
| ~ r1(X0,X1)
| p20(X1)
| ~ sP19(X0) ) ).
cnf(u1590,negated_conjecture,
( ~ r1(sK450,X374)
| p20(X374) ) ).
cnf(u858,axiom,
( ~ sP29(X0)
| p31(X1)
| r1(sK210(X1),sK211(X1))
| r1(X1,sK212(X1))
| ~ r1(X0,X1) ) ).
cnf(u739,axiom,
( ~ sP39(X0)
| p42(X1)
| r1(X1,sK180(X1))
| p41(X1)
| ~ r1(X0,X1) ) ).
cnf(u630,axiom,
( ~ sP48(X0)
| p51(X1)
| r1(sK153(X1),sK154(X1))
| r1(X1,sK155(X1))
| ~ r1(X0,X1) ) ).
cnf(u971,axiom,
( ~ p21(sK242(X1))
| p21(X1)
| p20(sK240(X1))
| ~ r1(X0,X1)
| ~ sP19(X0) ) ).
cnf(u864,axiom,
( ~ sP28(X0)
| p30(X1)
| p29(sK213(X1))
| r1(X1,sK215(X1))
| ~ r1(X0,X1) ) ).
cnf(u369,axiom,
( ~ sP70(X0)
| p73(X1)
| r1(X1,sK87(X1))
| r1(X1,sK89(X1))
| ~ r1(X0,X1) ) ).
cnf(u463,axiom,
( ~ sP62(X0)
| p65(X1)
| r1(X1,sK111(X1))
| p64(X1)
| ~ r1(X0,X1) ) ).
cnf(u5066,negated_conjecture,
( r1(sK267(X0),sK268(X0))
| p12(X0)
| p11(X0)
| ~ r1(sK300,X0) ) ).
cnf(u601,axiom,
( ~ p53(sK148(X1))
| p53(X1)
| ~ r1(X0,X1)
| p52(X1)
| ~ sP50(X0) ) ).
cnf(u356,axiom,
( ~ p74(sK86(X1))
| p74(X1)
| r1(X1,sK84(X1))
| ~ r1(X0,X1)
| ~ sP71(X0) ) ).
cnf(u486,axiom,
( ~ sP60(X0)
| p63(X1)
| r1(sK117(X1),sK118(X1))
| r1(X1,sK119(X1))
| ~ r1(X0,X1) ) ).
cnf(u885,axiom,
( ~ sP27(X0)
| p29(X1)
| r1(X1,sK216(X1))
| r1(X1,sK218(X1))
| ~ r1(X0,X1) ) ).
cnf(u1097,axiom,
( ~ p11(sK272(X1))
| p11(X1)
| r1(sK270(X1),sK271(X1))
| ~ r1(X0,X1)
| ~ sP9(X0) ) ).
cnf(u615,axiom,
( ~ p52(sK151(X1))
| p52(X1)
| ~ r1(X0,X1)
| r1(X1,sK152(X1))
| ~ sP49(X0) ) ).
cnf(u986,axiom,
( ~ p20(sK245(X1))
| p20(X1)
| ~ p20(sK244(X1))
| ~ r1(X0,X1)
| ~ sP18(X0) ) ).
cnf(u883,axiom,
( ~ sP27(X0)
| p29(X1)
| r1(X1,sK216(X1))
| p28(X1)
| ~ r1(X0,X1) ) ).
cnf(u758,axiom,
( ~ p39(sK188(X1))
| p39(X1)
| ~ p39(sK187(X1))
| ~ r1(X0,X1)
| ~ sP37(X0) ) ).
cnf(u874,axiom,
( ~ sP27(X0)
| p29(X1)
| p28(sK216(X1))
| p28(X1)
| ~ r1(X0,X1) ) ).
cnf(u992,axiom,
( ~ p20(sK245(X1))
| p20(X1)
| r1(X1,sK243(X1))
| ~ r1(X0,X1)
| ~ sP18(X0) ) ).
cnf(u375,axiom,
( ~ p72(sK91(X1))
| p72(X1)
| ~ r1(X0,X1)
| r1(X1,sK92(X1))
| ~ sP69(X0) ) ).
cnf(u4978,negated_conjecture,
( ~ r1(sK300,X0)
| p2(sK294(X0))
| p2(X0)
| p3(X0) ) ).
cnf(u497,axiom,
( ~ p62(sK122(X1))
| p62(X1)
| r1(sK120(X1),sK121(X1))
| ~ r1(X0,X1)
| ~ sP59(X0) ) ).
cnf(u1103,axiom,
( ~ p10(sK275(X1))
| p10(X1)
| p9(sK273(X1))
| ~ r1(X0,X1)
| ~ sP8(X0) ) ).
cnf(u729,axiom,
( ~ sP40(X0)
| p43(X1)
| r1(X1,sK177(X1))
| r1(X1,sK179(X1))
| ~ r1(X0,X1) ) ).
cnf(u484,axiom,
( ~ sP60(X0)
| p63(X1)
| r1(sK117(X1),sK118(X1))
| p62(X1)
| ~ r1(X0,X1) ) ).
cnf(u1013,axiom,
( ~ p18(sK251(X1))
| p18(X1)
| r1(sK249(X1),sK250(X1))
| ~ r1(X0,X1)
| ~ sP16(X0) ) ).
cnf(u770,axiom,
( ~ p38(sK191(X1))
| p38(X1)
| ~ p38(sK190(X1))
| ~ r1(X0,X1)
| ~ sP36(X0) ) ).
cnf(u900,axiom,
( ~ sP25(X0)
| p27(X1)
| p26(sK222(X1))
| r1(X1,sK224(X1))
| ~ r1(X0,X1) ) ).
cnf(u618,axiom,
( ~ sP49(X0)
| p52(X1)
| r1(sK150(X1),sK151(X1))
| r1(X1,sK152(X1))
| ~ r1(X0,X1) ) ).
cnf(u1011,axiom,
( ~ p18(sK250(X1))
| p18(X1)
| ~ r1(X0,X1)
| r1(X1,sK251(X1))
| ~ sP16(X0) ) ).
cnf(u776,axiom,
( ~ p38(sK191(X1))
| p38(X1)
| r1(X1,sK189(X1))
| ~ r1(X0,X1)
| ~ sP36(X0) ) ).
cnf(u1148,axiom,
( ~ p7(sK284(X1))
| p7(X1)
| r1(X1,sK282(X1))
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u624,axiom,
( ~ sP48(X0)
| p51(X1)
| p50(sK153(X1))
| r1(X1,sK155(X1))
| ~ r1(X0,X1) ) ).
cnf(u1059,axiom,
( ~ p14(sK262(X1))
| p14(X1)
| ~ r1(X0,X1)
| r1(X1,sK263(X1))
| ~ sP12(X0) ) ).
cnf(u670,axiom,
( ~ sP44(X0)
| p47(X1)
| p46(sK165(X1))
| p46(X1)
| ~ r1(X0,X1) ) ).
cnf(u513,axiom,
( ~ sP58(X0)
| p61(X1)
| r1(X1,sK123(X1))
| r1(X1,sK125(X1))
| ~ r1(X0,X1) ) ).
cnf(u1029,axiom,
( ~ sP15(X0)
| p17(X1)
| r1(X1,sK252(X1))
| r1(X1,sK254(X1))
| ~ r1(X0,X1) ) ).
cnf(u527,axiom,
( ~ p59(sK131(X1))
| p59(X1)
| p58(sK129(X1))
| ~ r1(X0,X1)
| ~ sP56(X0) ) ).
cnf(u898,axiom,
( ~ sP25(X0)
| p27(X1)
| p26(sK222(X1))
| p26(X1)
| ~ r1(X0,X1) ) ).
cnf(u1138,axiom,
( ~ sP5(X0)
| p7(X1)
| p6(sK282(X1))
| p6(X1)
| ~ r1(X0,X1) ) ).
cnf(u1163,axiom,
( ~ p5(sK290(X1))
| p5(X1)
| p4(sK288(X1))
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u501,axiom,
( ~ sP59(X0)
| p62(X1)
| r1(X1,sK120(X1))
| r1(X1,sK122(X1))
| ~ r1(X0,X1) ) ).
cnf(u752,axiom,
( ~ p41(sK185(X1))
| p41(X1)
| r1(X1,sK183(X1))
| ~ r1(X0,X1)
| ~ sP38(X0) ) ).
cnf(u1033,axiom,
( ~ p16(sK256(X1))
| p16(X1)
| ~ r1(X0,X1)
| p15(X1)
| ~ sP14(X0) ) ).
cnf(u396,axiom,
( ~ sP67(X0)
| p70(X1)
| p69(sK96(X1))
| r1(X1,sK98(X1))
| ~ r1(X0,X1) ) ).
cnf(u774,axiom,
( ~ sP36(X0)
| p38(X1)
| r1(sK189(X1),sK190(X1))
| r1(X1,sK191(X1))
| ~ r1(X0,X1) ) ).
cnf(u780,axiom,
( ~ sP35(X0)
| p37(X1)
| p36(sK192(X1))
| r1(X1,sK194(X1))
| ~ r1(X0,X1) ) ).
cnf(u1046,axiom,
( ~ p15(sK260(X1))
| p15(X1)
| ~ p15(sK259(X1))
| ~ r1(X0,X1)
| ~ sP13(X0) ) ).
cnf(u536,axiom,
( ~ p59(sK131(X1))
| p59(X1)
| r1(X1,sK129(X1))
| ~ r1(X0,X1)
| ~ sP56(X0) ) ).
cnf(u415,axiom,
( ~ sP66(X0)
| p69(X1)
| r1(X1,sK99(X1))
| p68(X1)
| ~ r1(X0,X1) ) ).
cnf(u553,axiom,
( ~ p57(sK136(X1))
| p57(X1)
| ~ r1(X0,X1)
| p56(X1)
| ~ sP54(X0) ) ).
cnf(u1039,axiom,
( ~ sP14(X0)
| p16(X1)
| r1(X1,sK255(X1))
| p15(X1)
| ~ r1(X0,X1) ) ).
cnf(u1161,axiom,
( ~ sP4(X0)
| p6(X1)
| r1(X1,sK285(X1))
| r1(X1,sK287(X1))
| ~ r1(X0,X1) ) ).
cnf(u1069,axiom,
( ~ p13(sK265(X1))
| p13(X1)
| ~ r1(X0,X1)
| p12(X1)
| ~ sP11(X0) ) ).
cnf(u902,axiom,
( ~ p27(sK224(X1))
| p27(X1)
| ~ p27(sK223(X1))
| ~ r1(X0,X1)
| ~ sP25(X0) ) ).
cnf(u799,axiom,
( ~ sP34(X0)
| p36(X1)
| r1(X1,sK195(X1))
| p35(X1)
| ~ r1(X0,X1) ) ).
cnf(u1050,axiom,
( ~ sP13(X0)
| p15(X1)
| r1(sK258(X1),sK259(X1))
| r1(X1,sK260(X1))
| ~ r1(X0,X1) ) ).
cnf(u4897,negated_conjecture,
( r1(sK294(X0),sK295(X0))
| p3(X0)
| r1(X0,sK296(X0))
| ~ r1(sK300,X0) ) ).
cnf(u908,axiom,
( ~ p27(sK224(X1))
| p27(X1)
| r1(X1,sK222(X1))
| ~ r1(X0,X1)
| ~ sP25(X0) ) ).
cnf(u4903,negated_conjecture,
( r1(sK267(X0),sK268(X0))
| p12(X0)
| r1(X0,sK269(X0))
| ~ r1(sK300,X0) ) ).
cnf(u1174,axiom,
( ~ sP2(X0)
| p4(X1)
| p3(sK291(X1))
| p3(X1)
| ~ r1(X0,X1) ) ).
cnf(u413,axiom,
( ~ p69(sK101(X1))
| p69(X1)
| r1(sK99(X1),sK100(X1))
| ~ r1(X0,X1)
| ~ sP66(X0) ) ).
cnf(u664,axiom,
( ~ sP45(X0)
| p48(X1)
| r1(sK162(X1),sK163(X1))
| p47(X1)
| ~ r1(X0,X1) ) ).
cnf(u384,axiom,
( ~ sP68(X0)
| p71(X1)
| p70(sK93(X1))
| r1(X1,sK95(X1))
| ~ r1(X0,X1) ) ).
cnf(u1167,axiom,
( ~ p5(sK289(X1))
| p5(X1)
| ~ r1(X0,X1)
| r1(X1,sK290(X1))
| ~ sP3(X0) ) ).
cnf(u913,axiom,
( ~ p26(sK226(X1))
| p26(X1)
| ~ r1(X0,X1)
| p25(X1)
| ~ sP24(X0) ) ).
cnf(u814,axiom,
( ~ sP32(X0)
| p34(X1)
| p33(sK201(X1))
| p33(X1)
| ~ r1(X0,X1) ) ).
cnf(u1197,axiom,
( ~ sP1(X0)
| p3(X1)
| r1(X1,sK294(X1))
| r1(X1,sK296(X1))
| ~ r1(X0,X1) ) ).
cnf(u1048,axiom,
( ~ sP13(X0)
| p15(X1)
| r1(sK258(X1),sK259(X1))
| p14(X1)
| ~ r1(X0,X1) ) ).
cnf(u927,axiom,
( ~ p25(sK229(X1))
| p25(X1)
| ~ r1(X0,X1)
| r1(X1,sK230(X1))
| ~ sP23(X0) ) ).
cnf(u1178,axiom,
( ~ p4(sK293(X1))
| p4(X1)
| ~ p4(sK292(X1))
| ~ r1(X0,X1)
| ~ sP2(X0) ) ).
cnf(u820,axiom,
( ~ sP32(X0)
| p34(X1)
| r1(sK201(X1),sK202(X1))
| p33(X1)
| ~ r1(X0,X1) ) ).
cnf(u1086,axiom,
( ~ sP10(X0)
| p12(X1)
| r1(sK267(X1),sK268(X1))
| r1(X1,sK269(X1))
| ~ r1(X0,X1) ) ).
cnf(u1172,axiom,
( ~ p5(sK290(X1))
| p5(X1)
| r1(X1,sK288(X1))
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u403,axiom,
( ~ sP67(X0)
| p70(X1)
| r1(X1,sK96(X1))
| p69(X1)
| ~ r1(X0,X1) ) ).
cnf(u704,axiom,
( ~ p45(sK173(X1))
| p45(X1)
| r1(X1,sK171(X1))
| ~ r1(X0,X1)
| ~ sP42(X0) ) ).
cnf(u557,axiom,
( ~ p57(sK137(X1))
| p57(X1)
| r1(sK135(X1),sK136(X1))
| ~ r1(X0,X1)
| ~ sP54(X0) ) ).
cnf(u1079,axiom,
( ~ p12(sK269(X1))
| p12(X1)
| p11(sK267(X1))
| ~ r1(X0,X1)
| ~ sP10(X0) ) ).
cnf(u426,axiom,
( ~ sP65(X0)
| p68(X1)
| r1(sK102(X1),sK103(X1))
| r1(X1,sK104(X1))
| ~ r1(X0,X1) ) ).
cnf(u825,axiom,
( ~ sP32(X0)
| p34(X1)
| r1(X1,sK201(X1))
| r1(X1,sK203(X1))
| ~ r1(X0,X1) ) ).
cnf(u555,axiom,
( ~ p57(sK136(X1))
| p57(X1)
| ~ r1(X0,X1)
| r1(X1,sK137(X1))
| ~ sP54(X0) ) ).
cnf(u942,axiom,
( ~ sP22(X0)
| p24(X1)
| r1(sK231(X1),sK232(X1))
| r1(X1,sK233(X1))
| ~ r1(X0,X1) ) ).
cnf(u533,axiom,
( ~ p59(sK131(X1))
| p59(X1)
| r1(sK129(X1),sK130(X1))
| ~ r1(X0,X1)
| ~ sP56(X0) ) ).
cnf(u1176,axiom,
( ~ sP2(X0)
| p4(X1)
| p3(sK291(X1))
| r1(X1,sK293(X1))
| ~ r1(X0,X1) ) ).
cnf(u315,axiom,
( ~ p77(sK76(X1))
| p77(X1)
| ~ r1(X0,X1)
| r1(X1,sK77(X1))
| ~ sP74(X0) ) ).
cnf(u668,axiom,
( ~ p48(sK164(X1))
| p48(X1)
| r1(X1,sK162(X1))
| ~ r1(X0,X1)
| ~ sP45(X0) ) ).
cnf(u685,axiom,
( ~ p46(sK169(X1))
| p46(X1)
| ~ r1(X0,X1)
| p45(X1)
| ~ sP43(X0) ) ).
cnf(u424,axiom,
( ~ sP65(X0)
| p68(X1)
| r1(sK102(X1),sK103(X1))
| p67(X1)
| ~ r1(X0,X1) ) ).
cnf(u1207,axiom,
( ~ sP0(X0)
| p2(X1)
| r1(X1,sK297(X1))
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u953,axiom,
( ~ p23(sK236(X1))
| p23(X1)
| r1(sK234(X1),sK235(X1))
| ~ r1(X0,X1)
| ~ sP21(X0) ) ).
cnf(u991,axiom,
( ~ sP18(X0)
| p20(X1)
| r1(X1,sK243(X1))
| p19(X1)
| ~ r1(X0,X1) ) ).
cnf(u683,axiom,
( ~ p46(sK170(X1))
| p46(X1)
| p45(sK168(X1))
| ~ r1(X0,X1)
| ~ sP43(X0) ) ).
cnf(u574,axiom,
( ~ sP52(X0)
| p55(X1)
| p54(sK141(X1))
| p54(X1)
| ~ r1(X0,X1) ) ).
cnf(u839,axiom,
( ~ p32(sK209(X1))
| p32(X1)
| p31(sK207(X1))
| ~ r1(X0,X1)
| ~ sP30(X0) ) ).
cnf(u1591,negated_conjecture,
~ p20(sK450) ).
cnf(u313,axiom,
( ~ p77(sK76(X1))
| p77(X1)
| ~ r1(X0,X1)
| p76(X1)
| ~ sP74(X0) ) ).
cnf(u443,axiom,
( ~ p66(sK110(X1))
| p66(X1)
| p65(sK108(X1))
| ~ r1(X0,X1)
| ~ sP63(X0) ) ).
cnf(u748,axiom,
( ~ sP38(X0)
| p41(X1)
| r1(sK183(X1),sK184(X1))
| p40(X1)
| ~ r1(X0,X1) ) ).
cnf(u430,axiom,
( ~ sP64(X0)
| p67(X1)
| p66(sK105(X1))
| p66(X1)
| ~ r1(X0,X1) ) ).
cnf(u779,axiom,
( ~ p37(sK194(X1))
| p37(X1)
| p36(sK192(X1))
| ~ r1(X0,X1)
| ~ sP35(X0) ) ).
cnf(u1099,axiom,
( ~ sP9(X0)
| p11(X1)
| r1(X1,sK270(X1))
| p10(X1)
| ~ r1(X0,X1) ) ).
cnf(u827,axiom,
( ~ p33(sK206(X1))
| p33(X1)
| p32(sK204(X1))
| ~ r1(X0,X1)
| ~ sP31(X0) ) ).
cnf(u702,axiom,
( ~ sP42(X0)
| p45(X1)
| r1(sK171(X1),sK172(X1))
| r1(X1,sK173(X1))
| ~ r1(X0,X1) ) ).
cnf(u1088,axiom,
( ~ p12(sK269(X1))
| p12(X1)
| r1(X1,sK267(X1))
| ~ r1(X0,X1)
| ~ sP10(X0) ) ).
cnf(u7062,negated_conjecture,
( ~ r1(X0,sK449)
| ~ r1(sK300,X0)
| r1(X0,sK558(X0))
| p13(X0) ) ).
cnf(u936,axiom,
( ~ sP22(X0)
| p24(X1)
| p23(sK231(X1))
| r1(X1,sK233(X1))
| ~ r1(X0,X1) ) ).
cnf(u1594,negated_conjecture,
~ p20(sK449) ).
cnf(u441,axiom,
( ~ sP64(X0)
| p67(X1)
| r1(X1,sK105(X1))
| r1(X1,sK107(X1))
| ~ r1(X0,X1) ) ).
cnf(u580,axiom,
( ~ sP52(X0)
| p55(X1)
| r1(sK141(X1),sK142(X1))
| p54(X1)
| ~ r1(X0,X1) ) ).
cnf(u597,axiom,
( ~ sP51(X0)
| p54(X1)
| r1(X1,sK144(X1))
| r1(X1,sK146(X1))
| ~ r1(X0,X1) ) ).
cnf(u336,axiom,
( ~ sP72(X0)
| p75(X1)
| p74(sK81(X1))
| r1(X1,sK83(X1))
| ~ r1(X0,X1) ) ).
cnf(u957,axiom,
( ~ sP21(X0)
| p23(X1)
| r1(X1,sK234(X1))
| r1(X1,sK236(X1))
| ~ r1(X0,X1) ) ).
cnf(u595,axiom,
( ~ sP51(X0)
| p54(X1)
| r1(X1,sK144(X1))
| p53(X1)
| ~ r1(X0,X1) ) ).
cnf(u955,axiom,
( ~ sP21(X0)
| p23(X1)
| r1(X1,sK234(X1))
| p22(X1)
| ~ r1(X0,X1) ) ).
cnf(u1124,axiom,
( ~ p9(sK278(X1))
| p9(X1)
| r1(X1,sK276(X1))
| ~ r1(X0,X1)
| ~ sP7(X0) ) ).
cnf(u708,axiom,
( ~ sP41(X0)
| p44(X1)
| p43(sK174(X1))
| r1(X1,sK176(X1))
| ~ r1(X0,X1) ) ).
cnf(u342,axiom,
( ~ sP72(X0)
| p75(X1)
| r1(sK81(X1),sK82(X1))
| r1(X1,sK83(X1))
| ~ r1(X0,X1) ) ).
cnf(u725,axiom,
( ~ p43(sK179(X1))
| p43(X1)
| r1(sK177(X1),sK178(X1))
| ~ r1(X0,X1)
| ~ sP40(X0) ) ).
cnf(u848,axiom,
( ~ p32(sK209(X1))
| p32(X1)
| r1(X1,sK207(X1))
| ~ r1(X0,X1)
| ~ sP30(X0) ) ).
cnf(u353,axiom,
( ~ p74(sK86(X1))
| p74(X1)
| r1(sK84(X1),sK85(X1))
| ~ r1(X0,X1)
| ~ sP71(X0) ) ).
cnf(u620,axiom,
( ~ p52(sK152(X1))
| p52(X1)
| r1(X1,sK150(X1))
| ~ r1(X0,X1)
| ~ sP49(X0) ) ).
cnf(u585,axiom,
( ~ sP52(X0)
| p55(X1)
| r1(X1,sK141(X1))
| r1(X1,sK143(X1))
| ~ r1(X0,X1) ) ).
cnf(u340,axiom,
( ~ sP72(X0)
| p75(X1)
| r1(sK81(X1),sK82(X1))
| p74(X1)
| ~ r1(X0,X1) ) ).
cnf(u470,axiom,
( ~ p64(sK116(X1))
| p64(X1)
| ~ p64(sK115(X1))
| ~ r1(X0,X1)
| ~ sP61(X0) ) ).
cnf(u869,axiom,
( ~ p30(sK215(X1))
| p30(X1)
| r1(sK213(X1),sK214(X1))
| ~ r1(X0,X1)
| ~ sP28(X0) ) ).
cnf(u1058,axiom,
( ~ p14(sK263(X1))
| p14(X1)
| ~ p14(sK262(X1))
| ~ r1(X0,X1)
| ~ sP12(X0) ) ).
cnf(u970,axiom,
( ~ sP19(X0)
| p21(X1)
| p20(sK240(X1))
| p20(X1)
| ~ r1(X0,X1) ) ).
cnf(u867,axiom,
( ~ p30(sK214(X1))
| p30(X1)
| ~ r1(X0,X1)
| r1(X1,sK215(X1))
| ~ sP28(X0) ) ).
cnf(u742,axiom,
( ~ sP38(X0)
| p41(X1)
| p40(sK183(X1))
| p40(X1)
| ~ r1(X0,X1) ) ).
cnf(u976,axiom,
( ~ sP19(X0)
| p21(X1)
| r1(sK240(X1),sK241(X1))
| p20(X1)
| ~ r1(X0,X1) ) ).
cnf(u359,axiom,
( ~ p73(sK89(X1))
| p73(X1)
| p72(sK87(X1))
| ~ r1(X0,X1)
| ~ sP70(X0) ) ).
cnf(u481,axiom,
( ~ p63(sK118(X1))
| p63(X1)
| ~ r1(X0,X1)
| p62(X1)
| ~ sP60(X0) ) ).
cnf(u1105,axiom,
( ~ p10(sK274(X1))
| p10(X1)
| ~ r1(X0,X1)
| p9(X1)
| ~ sP8(X0) ) ).
cnf(u468,axiom,
( ~ sP61(X0)
| p64(X1)
| p63(sK114(X1))
| r1(X1,sK116(X1))
| ~ r1(X0,X1) ) ).
cnf(u997,axiom,
( ~ p19(sK247(X1))
| p19(X1)
| ~ r1(X0,X1)
| p18(X1)
| ~ sP17(X0) ) ).
cnf(u635,axiom,
( ~ p50(sK158(X1))
| p50(X1)
| p49(sK156(X1))
| ~ r1(X0,X1)
| ~ sP47(X0) ) ).
cnf(u882,axiom,
( ~ sP27(X0)
| p29(X1)
| r1(sK216(X1),sK217(X1))
| r1(X1,sK218(X1))
| ~ r1(X0,X1) ) ).
cnf(u727,axiom,
( ~ sP40(X0)
| p43(X1)
| r1(X1,sK177(X1))
| p42(X1)
| ~ r1(X0,X1) ) ).
cnf(u888,axiom,
( ~ sP26(X0)
| p28(X1)
| p27(sK219(X1))
| r1(X1,sK221(X1))
| ~ r1(X0,X1) ) ).
cnf(u357,axiom,
( ~ sP71(X0)
| p74(X1)
| r1(X1,sK84(X1))
| r1(X1,sK86(X1))
| ~ r1(X0,X1) ) ).
cnf(u1057,axiom,
( ~ p14(sK262(X1))
| p14(X1)
| ~ r1(X0,X1)
| p13(X1)
| ~ sP12(X0) ) ).
cnf(u487,axiom,
( ~ sP60(X0)
| p63(X1)
| r1(X1,sK117(X1))
| p62(X1)
| ~ r1(X0,X1) ) ).
cnf(u641,axiom,
( ~ p50(sK158(X1))
| p50(X1)
| r1(sK156(X1),sK157(X1))
| ~ r1(X0,X1)
| ~ sP47(X0) ) ).
cnf(u625,axiom,
( ~ p51(sK154(X1))
| p51(X1)
| ~ r1(X0,X1)
| p50(X1)
| ~ sP48(X0) ) ).
cnf(u380,axiom,
( ~ p72(sK92(X1))
| p72(X1)
| r1(X1,sK90(X1))
| ~ r1(X0,X1)
| ~ sP69(X0) ) ).
cnf(u1141,axiom,
( ~ p7(sK283(X1))
| p7(X1)
| ~ r1(X0,X1)
| p6(X1)
| ~ sP5(X0) ) ).
cnf(u639,axiom,
( ~ p50(sK157(X1))
| p50(X1)
| ~ r1(X0,X1)
| r1(X1,sK158(X1))
| ~ sP47(X0) ) ).
cnf(u762,axiom,
( ~ sP37(X0)
| p39(X1)
| r1(sK186(X1),sK187(X1))
| r1(X1,sK188(X1))
| ~ r1(X0,X1) ) ).
cnf(u1122,axiom,
( ~ sP7(X0)
| p9(X1)
| r1(sK276(X1),sK277(X1))
| r1(X1,sK278(X1))
| ~ r1(X0,X1) ) ).
cnf(u1096,axiom,
( ~ sP9(X0)
| p11(X1)
| r1(sK270(X1),sK271(X1))
| p10(X1)
| ~ r1(X0,X1) ) ).
cnf(u485,axiom,
( ~ p63(sK119(X1))
| p63(X1)
| r1(sK117(X1),sK118(X1))
| ~ r1(X0,X1)
| ~ sP60(X0) ) ).
cnf(u736,axiom,
( ~ sP39(X0)
| p42(X1)
| r1(sK180(X1),sK181(X1))
| p41(X1)
| ~ r1(X0,X1) ) ).
cnf(u370,axiom,
( ~ sP69(X0)
| p72(X1)
| p71(sK90(X1))
| p71(X1)
| ~ r1(X0,X1) ) ).
cnf(u753,axiom,
( ~ sP38(X0)
| p41(X1)
| r1(X1,sK183(X1))
| r1(X1,sK185(X1))
| ~ r1(X0,X1) ) ).
cnf(u508,axiom,
( ~ sP58(X0)
| p61(X1)
| r1(sK123(X1),sK124(X1))
| p60(X1)
| ~ r1(X0,X1) ) ).
cnf(u886,axiom,
( ~ sP26(X0)
| p28(X1)
| p27(sK219(X1))
| p27(X1)
| ~ r1(X0,X1) ) ).
cnf(u7037,negated_conjecture,
( ~ p20(sK267(sK526(X0)))
| p11(sK526(X0))
| ~ r1(sK300,sK526(X0))
| ~ p20(X1)
| ~ r1(X0,X1)
| p12(sK526(X0))
| ~ r1(sK300,X0)
| p21(X0) ) ).
cnf(u767,axiom,
( ~ p38(sK191(X1))
| p38(X1)
| p37(sK189(X1))
| ~ r1(X0,X1)
| ~ sP36(X0) ) ).
cnf(u514,axiom,
( ~ sP57(X0)
| p60(X1)
| p59(sK126(X1))
| p59(X1)
| ~ r1(X0,X1) ) ).
cnf(u401,axiom,
( ~ p70(sK98(X1))
| p70(X1)
| r1(sK96(X1),sK97(X1))
| ~ r1(X0,X1)
| ~ sP67(X0) ) ).
cnf(u892,axiom,
( ~ sP26(X0)
| p28(X1)
| r1(sK219(X1),sK220(X1))
| p27(X1)
| ~ r1(X0,X1) ) ).
cnf(u1030,axiom,
( ~ sP14(X0)
| p16(X1)
| p15(sK255(X1))
| p15(X1)
| ~ r1(X0,X1) ) ).
cnf(u520,axiom,
( ~ sP57(X0)
| p60(X1)
| r1(sK126(X1),sK127(X1))
| p59(X1)
| ~ r1(X0,X1) ) ).
cnf(u399,axiom,
( ~ p70(sK97(X1))
| p70(X1)
| ~ r1(X0,X1)
| r1(X1,sK98(X1))
| ~ sP67(X0) ) ).
cnf(u1151,axiom,
( ~ p6(sK287(X1))
| p6(X1)
| p5(sK285(X1))
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u498,axiom,
( ~ sP59(X0)
| p62(X1)
| r1(sK120(X1),sK121(X1))
| r1(X1,sK122(X1))
| ~ r1(X0,X1) ) ).
cnf(u1053,axiom,
( ~ sP13(X0)
| p15(X1)
| r1(X1,sK258(X1))
| r1(X1,sK260(X1))
| ~ r1(X0,X1) ) ).
cnf(u1014,axiom,
( ~ sP16(X0)
| p18(X1)
| r1(sK249(X1),sK250(X1))
| r1(X1,sK251(X1))
| ~ r1(X0,X1) ) ).
cnf(u783,axiom,
( ~ p37(sK193(X1))
| p37(X1)
| ~ r1(X0,X1)
| r1(X1,sK194(X1))
| ~ sP35(X0) ) ).
cnf(u642,axiom,
( ~ sP47(X0)
| p50(X1)
| r1(sK156(X1),sK157(X1))
| r1(X1,sK158(X1))
| ~ r1(X0,X1) ) ).
cnf(u1020,axiom,
( ~ sP15(X0)
| p17(X1)
| p16(sK252(X1))
| r1(X1,sK254(X1))
| ~ r1(X0,X1) ) ).
cnf(u397,axiom,
( ~ p70(sK97(X1))
| p70(X1)
| ~ r1(X0,X1)
| p69(X1)
| ~ sP67(X0) ) ).
cnf(u648,axiom,
( ~ sP46(X0)
| p49(X1)
| p48(sK159(X1))
| r1(X1,sK161(X1))
| ~ r1(X0,X1) ) ).
cnf(u496,axiom,
( ~ sP59(X0)
| p62(X1)
| r1(sK120(X1),sK121(X1))
| p61(X1)
| ~ r1(X0,X1) ) ).
cnf(u897,axiom,
( ~ sP26(X0)
| p28(X1)
| r1(X1,sK219(X1))
| r1(X1,sK221(X1))
| ~ r1(X0,X1) ) ).
cnf(u1043,axiom,
( ~ p15(sK260(X1))
| p15(X1)
| p14(sK258(X1))
| ~ r1(X0,X1)
| ~ sP13(X0) ) ).
cnf(u798,axiom,
( ~ sP34(X0)
| p36(X1)
| r1(sK195(X1),sK196(X1))
| r1(X1,sK197(X1))
| ~ r1(X0,X1) ) ).
cnf(u1181,axiom,
( ~ p4(sK293(X1))
| p4(X1)
| r1(sK291(X1),sK292(X1))
| ~ r1(X0,X1)
| ~ sP2(X0) ) ).
cnf(u682,axiom,
( ~ sP43(X0)
| p46(X1)
| p45(sK168(X1))
| p45(X1)
| ~ r1(X0,X1) ) ).
cnf(u1032,axiom,
( ~ sP14(X0)
| p16(X1)
| p15(sK255(X1))
| r1(X1,sK257(X1))
| ~ r1(X0,X1) ) ).
cnf(u911,axiom,
( ~ p26(sK227(X1))
| p26(X1)
| p25(sK225(X1))
| ~ r1(X0,X1)
| ~ sP24(X0) ) ).
cnf(u1162,axiom,
( ~ sP3(X0)
| p5(X1)
| p4(sK288(X1))
| p4(X1)
| ~ r1(X0,X1) ) ).
cnf(u804,axiom,
( ~ sP33(X0)
| p35(X1)
| p34(sK198(X1))
| r1(X1,sK200(X1))
| ~ r1(X0,X1) ) ).
cnf(u1155,axiom,
( ~ p6(sK286(X1))
| p6(X1)
| ~ r1(X0,X1)
| r1(X1,sK287(X1))
| ~ sP4(X0) ) ).
cnf(u1156,axiom,
( ~ sP4(X0)
| p6(X1)
| r1(sK285(X1),sK286(X1))
| p5(X1)
| ~ r1(X0,X1) ) ).
cnf(u387,axiom,
( ~ p71(sK94(X1))
| p71(X1)
| ~ r1(X0,X1)
| r1(X1,sK95(X1))
| ~ sP68(X0) ) ).
cnf(u743,axiom,
( ~ p41(sK185(X1))
| p41(X1)
| p40(sK183(X1))
| ~ r1(X0,X1)
| ~ sP38(X0) ) ).
cnf(u541,axiom,
( ~ p58(sK133(X1))
| p58(X1)
| ~ r1(X0,X1)
| p57(X1)
| ~ sP55(X0) ) ).
cnf(u1063,axiom,
( ~ sP12(X0)
| p14(X1)
| r1(X1,sK261(X1))
| p13(X1)
| ~ r1(X0,X1) ) ).
cnf(u410,axiom,
( ~ p69(sK101(X1))
| p69(X1)
| ~ p69(sK100(X1))
| ~ r1(X0,X1)
| ~ sP66(X0) ) ).
cnf(u1171,axiom,
( ~ sP3(X0)
| p5(X1)
| r1(X1,sK288(X1))
| p4(X1)
| ~ r1(X0,X1) ) ).
cnf(u926,axiom,
( ~ p25(sK230(X1))
| p25(X1)
| ~ p25(sK229(X1))
| ~ r1(X0,X1)
| ~ sP23(X0) ) ).
cnf(u823,axiom,
( ~ sP32(X0)
| p34(X1)
| r1(X1,sK201(X1))
| p33(X1)
| ~ r1(X0,X1) ) ).
cnf(u1160,axiom,
( ~ p6(sK287(X1))
| p6(X1)
| r1(X1,sK285(X1))
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u932,axiom,
( ~ p25(sK230(X1))
| p25(X1)
| r1(X1,sK228(X1))
| ~ r1(X0,X1)
| ~ sP23(X0) ) ).
cnf(u950,axiom,
( ~ p23(sK236(X1))
| p23(X1)
| ~ p23(sK235(X1))
| ~ r1(X0,X1)
| ~ sP21(X0) ) ).
cnf(u1198,axiom,
( ~ sP0(X0)
| p2(X1)
| p1(sK297(X1))
| p1(X1)
| ~ r1(X0,X1) ) ).
cnf(u652,axiom,
( ~ sP46(X0)
| p49(X1)
| r1(sK159(X1),sK160(X1))
| p48(X1)
| ~ r1(X0,X1) ) ).
cnf(u669,axiom,
( ~ sP45(X0)
| p48(X1)
| r1(X1,sK162(X1))
| r1(X1,sK164(X1))
| ~ r1(X0,X1) ) ).
cnf(u408,axiom,
( ~ sP66(X0)
| p69(X1)
| p68(sK99(X1))
| r1(X1,sK101(X1))
| ~ r1(X0,X1) ) ).
cnf(u1191,axiom,
( ~ p3(sK295(X1))
| p3(X1)
| ~ r1(X0,X1)
| r1(X1,sK296(X1))
| ~ sP1(X0) ) ).
cnf(u362,axiom,
( ~ p73(sK89(X1))
| p73(X1)
| ~ p73(sK88(X1))
| ~ r1(X0,X1)
| ~ sP70(X0) ) ).
cnf(u937,axiom,
( ~ p24(sK232(X1))
| p24(X1)
| ~ r1(X0,X1)
| p23(X1)
| ~ sP22(X0) ) ).
cnf(u1083,axiom,
( ~ p12(sK268(X1))
| p12(X1)
| ~ r1(X0,X1)
| r1(X1,sK269(X1))
| ~ sP10(X0) ) ).
cnf(u667,axiom,
( ~ sP45(X0)
| p48(X1)
| r1(X1,sK162(X1))
| p47(X1)
| ~ r1(X0,X1) ) ).
cnf(u558,axiom,
( ~ sP54(X0)
| p57(X1)
| r1(sK135(X1),sK136(X1))
| r1(X1,sK137(X1))
| ~ r1(X0,X1) ) ).
cnf(u1072,axiom,
( ~ sP11(X0)
| p13(X1)
| r1(sK264(X1),sK265(X1))
| p12(X1)
| ~ r1(X0,X1) ) ).
cnf(u951,axiom,
( ~ p23(sK235(X1))
| p23(X1)
| ~ r1(X0,X1)
| r1(X1,sK236(X1))
| ~ sP21(X0) ) ).
cnf(u564,axiom,
( ~ sP53(X0)
| p56(X1)
| p55(sK138(X1))
| r1(X1,sK140(X1))
| ~ r1(X0,X1) ) ).
cnf(u427,axiom,
( ~ sP65(X0)
| p68(X1)
| r1(X1,sK102(X1))
| p67(X1)
| ~ r1(X0,X1) ) ).
cnf(u7049,negated_conjecture,
( ~ r1(sK558(X1),sK450)
| ~ r1(X1,X0)
| ~ r1(sK300,X1)
| ~ p12(X0)
| p13(X1) ) ).
cnf(u414,axiom,
( ~ sP66(X0)
| p69(X1)
| r1(sK99(X1),sK100(X1))
| r1(X1,sK101(X1))
| ~ r1(X0,X1) ) ).
cnf(u813,axiom,
( ~ sP33(X0)
| p35(X1)
| r1(X1,sK198(X1))
| r1(X1,sK200(X1))
| ~ r1(X0,X1) ) ).
cnf(u707,axiom,
( ~ p44(sK176(X1))
| p44(X1)
| p43(sK174(X1))
| ~ r1(X0,X1)
| ~ sP41(X0) ) ).
cnf(u996,axiom,
( ~ sP17(X0)
| p19(X1)
| p18(sK246(X1))
| r1(X1,sK248(X1))
| ~ r1(X0,X1) ) ).
cnf(u811,axiom,
( ~ sP33(X0)
| p35(X1)
| r1(X1,sK198(X1))
| p34(X1)
| ~ r1(X0,X1) ) ).
cnf(u686,axiom,
( ~ p46(sK170(X1))
| p46(X1)
| ~ p46(sK169(X1))
| ~ r1(X0,X1)
| ~ sP43(X0) ) ).
cnf(u1200,axiom,
( ~ sP0(X0)
| p2(X1)
| p1(sK297(X1))
| r1(X1,sK299(X1))
| ~ r1(X0,X1) ) ).
cnf(u559,axiom,
( ~ sP54(X0)
| p57(X1)
| r1(X1,sK135(X1))
| p56(X1)
| ~ r1(X0,X1) ) ).
cnf(u920,axiom,
( ~ p26(sK227(X1))
| p26(X1)
| r1(X1,sK225(X1))
| ~ r1(X0,X1)
| ~ sP24(X0) ) ).
cnf(u425,axiom,
( ~ p68(sK104(X1))
| p68(X1)
| r1(sK102(X1),sK103(X1))
| ~ r1(X0,X1)
| ~ sP65(X0) ) ).
cnf(u692,axiom,
( ~ p46(sK170(X1))
| p46(X1)
| r1(X1,sK168(X1))
| ~ r1(X0,X1)
| ~ sP43(X0) ) ).
cnf(u1595,negated_conjecture,
r1(sK300,sK449) ).
cnf(u581,axiom,
( ~ p55(sK143(X1))
| p55(X1)
| r1(sK141(X1),sK142(X1))
| ~ r1(X0,X1)
| ~ sP52(X0) ) ).
cnf(u320,axiom,
( ~ p77(sK77(X1))
| p77(X1)
| r1(X1,sK75(X1))
| ~ r1(X0,X1)
| ~ sP74(X0) ) ).
cnf(u941,axiom,
( ~ p24(sK233(X1))
| p24(X1)
| r1(sK231(X1),sK232(X1))
| ~ r1(X0,X1)
| ~ sP22(X0) ) ).
cnf(u826,axiom,
( ~ sP31(X0)
| p33(X1)
| p32(sK204(X1))
| p32(X1)
| ~ r1(X0,X1) ) ).
cnf(u579,axiom,
( ~ p55(sK142(X1))
| p55(X1)
| ~ r1(X0,X1)
| r1(X1,sK143(X1))
| ~ sP52(X0) ) ).
cnf(u939,axiom,
( ~ p24(sK232(X1))
| p24(X1)
| ~ r1(X0,X1)
| r1(X1,sK233(X1))
| ~ sP22(X0) ) ).
cnf(u7094,negated_conjecture,
( ~ p20(sK296(sK526(X0)))
| p3(sK526(X0))
| ~ r1(sK300,sK526(X0))
| ~ p20(X1)
| ~ r1(X0,X1)
| p2(sK294(sK526(X0)))
| ~ r1(sK300,X0)
| p21(X0) ) ).
cnf(u627,axiom,
( ~ p51(sK154(X1))
| p51(X1)
| ~ r1(X0,X1)
| r1(X1,sK155(X1))
| ~ sP48(X0) ) ).
cnf(u326,axiom,
( ~ p76(sK80(X1))
| p76(X1)
| ~ p76(sK79(X1))
| ~ r1(X0,X1)
| ~ sP73(X0) ) ).
cnf(u709,axiom,
( ~ p44(sK175(X1))
| p44(X1)
| ~ r1(X0,X1)
| p43(X1)
| ~ sP41(X0) ) ).
cnf(u954,axiom,
( ~ sP21(X0)
| p23(X1)
| r1(sK234(X1),sK235(X1))
| r1(X1,sK236(X1))
| ~ r1(X0,X1) ) ).
cnf(u598,axiom,
( ~ sP50(X0)
| p53(X1)
| p52(sK147(X1))
| p52(X1)
| ~ r1(X0,X1) ) ).
cnf(u832,axiom,
( ~ sP31(X0)
| p33(X1)
| r1(sK204(X1),sK205(X1))
| p32(X1)
| ~ r1(X0,X1) ) ).
cnf(u337,axiom,
( ~ p75(sK82(X1))
| p75(X1)
| ~ r1(X0,X1)
| p74(X1)
| ~ sP72(X0) ) ).
cnf(u604,axiom,
( ~ sP50(X0)
| p53(X1)
| r1(sK147(X1),sK148(X1))
| p52(X1)
| ~ r1(X0,X1) ) ).
cnf(u697,axiom,
( ~ p45(sK172(X1))
| p45(X1)
| ~ r1(X0,X1)
| p44(X1)
| ~ sP42(X0) ) ).
cnf(u608,axiom,
( ~ p53(sK149(X1))
| p53(X1)
| r1(X1,sK147(X1))
| ~ r1(X0,X1)
| ~ sP50(X0) ) ).
cnf(u454,axiom,
( ~ sP62(X0)
| p65(X1)
| p64(sK111(X1))
| p64(X1)
| ~ r1(X0,X1) ) ).
cnf(u594,axiom,
( ~ sP51(X0)
| p54(X1)
| r1(sK144(X1),sK145(X1))
| r1(X1,sK146(X1))
| ~ r1(X0,X1) ) ).
cnf(u1025,axiom,
( ~ p17(sK254(X1))
| p17(X1)
| r1(sK252(X1),sK253(X1))
| ~ r1(X0,X1)
| ~ sP15(X0) ) ).
cnf(u583,axiom,
( ~ sP52(X0)
| p55(X1)
| r1(X1,sK141(X1))
| p54(X1)
| ~ r1(X0,X1) ) ).
cnf(u602,axiom,
( ~ p53(sK149(X1))
| p53(X1)
| ~ p53(sK148(X1))
| ~ r1(X0,X1)
| ~ sP50(X0) ) ).
cnf(u851,axiom,
( ~ p31(sK212(X1))
| p31(X1)
| p30(sK210(X1))
| ~ r1(X0,X1)
| ~ sP29(X0) ) ).
cnf(u1065,axiom,
( ~ sP12(X0)
| p14(X1)
| r1(X1,sK261(X1))
| r1(X1,sK263(X1))
| ~ r1(X0,X1) ) ).
cnf(u530,axiom,
( ~ p59(sK131(X1))
| p59(X1)
| ~ p59(sK130(X1))
| ~ r1(X0,X1)
| ~ sP56(X0) ) ).
cnf(u343,axiom,
( ~ sP72(X0)
| p75(X1)
| r1(X1,sK81(X1))
| p74(X1)
| ~ r1(X0,X1) ) ).
cnf(u465,axiom,
( ~ sP62(X0)
| p65(X1)
| r1(X1,sK111(X1))
| r1(X1,sK113(X1))
| ~ r1(X0,X1) ) ).
cnf(u1089,axiom,
( ~ sP10(X0)
| p12(X1)
| r1(X1,sK267(X1))
| r1(X1,sK269(X1))
| ~ r1(X0,X1) ) ).
cnf(u452,axiom,
( ~ p66(sK110(X1))
| p66(X1)
| r1(X1,sK108(X1))
| ~ r1(X0,X1)
| ~ sP63(X0) ) ).
cnf(u981,axiom,
( ~ sP19(X0)
| p21(X1)
| r1(X1,sK240(X1))
| r1(X1,sK242(X1))
| ~ r1(X0,X1) ) ).
cnf(u1082,axiom,
( ~ p12(sK269(X1))
| p12(X1)
| ~ p12(sK268(X1))
| ~ r1(X0,X1)
| ~ sP10(X0) ) ).
cnf(u7061,negated_conjecture,
( ~ r1(sK558(X1),sK449)
| ~ r1(X1,X0)
| ~ r1(sK300,X1)
| ~ p12(X0)
| p13(X1) ) ).
cnf(u711,axiom,
( ~ p44(sK175(X1))
| p44(X1)
| ~ r1(X0,X1)
| r1(X1,sK176(X1))
| ~ sP41(X0) ) ).
cnf(u586,axiom,
( ~ sP51(X0)
| p54(X1)
| p53(sK144(X1))
| p53(X1)
| ~ r1(X0,X1) ) ).
cnf(u979,axiom,
( ~ sP19(X0)
| p21(X1)
| r1(X1,sK240(X1))
| p20(X1)
| ~ r1(X0,X1) ) ).
cnf(u4973,negated_conjecture,
( r1(sK294(X0),sK295(X0))
| p3(X0)
| p2(X0)
| ~ r1(sK300,X0) ) ).
cnf(u872,axiom,
( ~ p30(sK215(X1))
| p30(X1)
| r1(X1,sK213(X1))
| ~ r1(X0,X1)
| ~ sP28(X0) ) ).
cnf(u592,axiom,
( ~ sP51(X0)
| p54(X1)
| r1(sK144(X1),sK145(X1))
| p53(X1)
| ~ r1(X0,X1) ) ).
cnf(u471,axiom,
( ~ p64(sK115(X1))
| p64(X1)
| ~ r1(X0,X1)
| r1(X1,sK116(X1))
| ~ sP61(X0) ) ).
cnf(u609,axiom,
( ~ sP50(X0)
| p53(X1)
| r1(X1,sK147(X1))
| r1(X1,sK149(X1))
| ~ r1(X0,X1) ) ).
cnf(u364,axiom,
( ~ sP70(X0)
| p73(X1)
| r1(sK87(X1),sK88(X1))
| p72(X1)
| ~ r1(X0,X1) ) ).
cnf(u1125,axiom,
( ~ sP7(X0)
| p9(X1)
| r1(X1,sK276(X1))
| r1(X1,sK278(X1))
| ~ r1(X0,X1) ) ).
cnf(u623,axiom,
( ~ p51(sK155(X1))
| p51(X1)
| p50(sK153(X1))
| ~ r1(X0,X1)
| ~ sP48(X0) ) ).
cnf(u994,axiom,
( ~ sP17(X0)
| p19(X1)
| p18(sK246(X1))
| p18(X1)
| ~ r1(X0,X1) ) ).
cnf(u714,axiom,
( ~ sP41(X0)
| p44(X1)
| r1(sK174(X1),sK175(X1))
| r1(X1,sK176(X1))
| ~ r1(X0,X1) ) ).
cnf(u383,axiom,
( ~ p71(sK95(X1))
| p71(X1)
| p70(sK93(X1))
| ~ r1(X0,X1)
| ~ sP68(X0) ) ).
cnf(u469,axiom,
( ~ p64(sK115(X1))
| p64(X1)
| ~ r1(X0,X1)
| p63(X1)
| ~ sP61(X0) ) ).
cnf(u720,axiom,
( ~ sP40(X0)
| p43(X1)
| p42(sK177(X1))
| r1(X1,sK179(X1))
| ~ r1(X0,X1) ) ).
cnf(u354,axiom,
( ~ sP71(X0)
| p74(X1)
| r1(sK84(X1),sK85(X1))
| r1(X1,sK86(X1))
| ~ r1(X0,X1) ) ).
cnf(u1129,axiom,
( ~ p8(sK280(X1))
| p8(X1)
| ~ r1(X0,X1)
| p7(X1)
| ~ sP6(X0) ) ).
cnf(u492,axiom,
( ~ sP59(X0)
| p62(X1)
| p61(sK120(X1))
| r1(X1,sK122(X1))
| ~ r1(X0,X1) ) ).
cnf(u791,axiom,
( ~ p36(sK197(X1))
| p36(X1)
| p35(sK195(X1))
| ~ r1(X0,X1)
| ~ sP34(X0) ) ).
cnf(u870,axiom,
( ~ sP28(X0)
| p30(X1)
| r1(sK213(X1),sK214(X1))
| r1(X1,sK215(X1))
| ~ r1(X0,X1) ) ).
cnf(u433,axiom,
( ~ p67(sK106(X1))
| p67(X1)
| ~ r1(X0,X1)
| p66(X1)
| ~ sP64(X0) ) ).
cnf(u751,axiom,
( ~ sP38(X0)
| p41(X1)
| r1(X1,sK183(X1))
| p40(X1)
| ~ r1(X0,X1) ) ).
cnf(u626,axiom,
( ~ p51(sK155(X1))
| p51(X1)
| ~ p51(sK154(X1))
| ~ r1(X0,X1)
| ~ sP48(X0) ) ).
cnf(u876,axiom,
( ~ sP27(X0)
| p29(X1)
| p28(sK216(X1))
| r1(X1,sK218(X1))
| ~ r1(X0,X1) ) ).
cnf(u1142,axiom,
( ~ p7(sK284(X1))
| p7(X1)
| ~ p7(sK283(X1))
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u381,axiom,
( ~ sP69(X0)
| p72(X1)
| r1(X1,sK90(X1))
| r1(X1,sK92(X1))
| ~ r1(X0,X1) ) ).
cnf(u632,axiom,
( ~ p51(sK155(X1))
| p51(X1)
| r1(X1,sK153(X1))
| ~ r1(X0,X1)
| ~ sP48(X0) ) ).
cnf(u511,axiom,
( ~ sP58(X0)
| p61(X1)
| r1(X1,sK123(X1))
| p60(X1)
| ~ r1(X0,X1) ) ).
cnf(u1135,axiom,
( ~ sP6(X0)
| p8(X1)
| r1(X1,sK279(X1))
| p7(X1)
| ~ r1(X0,X1) ) ).
cnf(u482,axiom,
( ~ p63(sK119(X1))
| p63(X1)
| ~ p63(sK118(X1))
| ~ r1(X0,X1)
| ~ sP60(X0) ) ).
cnf(u1037,axiom,
( ~ p16(sK257(X1))
| p16(X1)
| r1(sK255(X1),sK256(X1))
| ~ r1(X0,X1)
| ~ sP14(X0) ) ).
cnf(u998,axiom,
( ~ p19(sK248(X1))
| p19(X1)
| ~ p19(sK247(X1))
| ~ r1(X0,X1)
| ~ sP17(X0) ) ).
cnf(u895,axiom,
( ~ sP26(X0)
| p28(X1)
| r1(X1,sK219(X1))
| p27(X1)
| ~ r1(X0,X1) ) ).
cnf(u754,axiom,
( ~ sP37(X0)
| p39(X1)
| p38(sK186(X1))
| p38(X1)
| ~ r1(X0,X1) ) ).
cnf(u1004,axiom,
( ~ p19(sK248(X1))
| p19(X1)
| r1(X1,sK246(X1))
| ~ r1(X0,X1)
| ~ sP17(X0) ) ).
cnf(u371,axiom,
( ~ p72(sK92(X1))
| p72(X1)
| p71(sK90(X1))
| ~ r1(X0,X1)
| ~ sP69(X0) ) ).
cnf(u509,axiom,
( ~ p61(sK125(X1))
| p61(X1)
| r1(sK123(X1),sK124(X1))
| ~ r1(X0,X1)
| ~ sP58(X0) ) ).
cnf(u760,axiom,
( ~ sP37(X0)
| p39(X1)
| r1(sK186(X1),sK187(X1))
| p38(X1)
| ~ r1(X0,X1) ) ).
cnf(u480,axiom,
( ~ sP60(X0)
| p63(X1)
| p62(sK117(X1))
| r1(X1,sK119(X1))
| ~ r1(X0,X1) ) ).
cnf(u1009,axiom,
( ~ p18(sK250(X1))
| p18(X1)
| ~ r1(X0,X1)
| p17(X1)
| ~ sP16(X0) ) ).
cnf(u1027,axiom,
( ~ sP15(X0)
| p17(X1)
| r1(X1,sK252(X1))
| p16(X1)
| ~ r1(X0,X1) ) ).
cnf(u782,axiom,
( ~ p37(sK194(X1))
| p37(X1)
| ~ p37(sK193(X1))
| ~ r1(X0,X1)
| ~ sP35(X0) ) ).
cnf(u1165,axiom,
( ~ p5(sK289(X1))
| p5(X1)
| ~ r1(X0,X1)
| p4(X1)
| ~ sP3(X0) ) ).
cnf(u1144,axiom,
( ~ sP5(X0)
| p7(X1)
| r1(sK282(X1),sK283(X1))
| p6(X1)
| ~ r1(X0,X1) ) ).
cnf(u1023,axiom,
( ~ p17(sK253(X1))
| p17(X1)
| ~ r1(X0,X1)
| r1(X1,sK254(X1))
| ~ sP15(X0) ) ).
cnf(u689,axiom,
( ~ p46(sK170(X1))
| p46(X1)
| r1(sK168(X1),sK169(X1))
| ~ r1(X0,X1)
| ~ sP43(X0) ) ).
cnf(u788,axiom,
( ~ p37(sK194(X1))
| p37(X1)
| r1(X1,sK192(X1))
| ~ r1(X0,X1)
| ~ sP35(X0) ) ).
cnf(u1054,axiom,
( ~ sP12(X0)
| p14(X1)
| p13(sK261(X1))
| p13(X1)
| ~ r1(X0,X1) ) ).
cnf(u960,axiom,
( ~ sP20(X0)
| p22(X1)
| p21(sK237(X1))
| r1(X1,sK239(X1))
| ~ r1(X0,X1) ) ).
cnf(u845,axiom,
( ~ p32(sK209(X1))
| p32(X1)
| r1(sK207(X1),sK208(X1))
| ~ r1(X0,X1)
| ~ sP30(X0) ) ).
cnf(u525,axiom,
( ~ sP57(X0)
| p60(X1)
| r1(X1,sK126(X1))
| r1(X1,sK128(X1))
| ~ r1(X0,X1) ) ).
cnf(u1047,axiom,
( ~ p15(sK259(X1))
| p15(X1)
| ~ r1(X0,X1)
| r1(X1,sK260(X1))
| ~ sP13(X0) ) ).
cnf(u394,axiom,
( ~ sP67(X0)
| p70(X1)
| p69(sK96(X1))
| p69(X1)
| ~ r1(X0,X1) ) ).
cnf(u793,axiom,
( ~ p36(sK196(X1))
| p36(X1)
| ~ r1(X0,X1)
| p35(X1)
| ~ sP34(X0) ) ).
cnf(u523,axiom,
( ~ sP57(X0)
| p60(X1)
| r1(X1,sK126(X1))
| p59(X1)
| ~ r1(X0,X1) ) ).
cnf(u910,axiom,
( ~ sP24(X0)
| p26(X1)
| p25(sK225(X1))
| p25(X1)
| ~ r1(X0,X1) ) ).
cnf(u807,axiom,
( ~ p35(sK199(X1))
| p35(X1)
| ~ r1(X0,X1)
| r1(X1,sK200(X1))
| ~ sP33(X0) ) ).
cnf(u916,axiom,
( ~ sP24(X0)
| p26(X1)
| r1(sK225(X1),sK226(X1))
| p25(X1)
| ~ r1(X0,X1) ) ).
cnf(u764,axiom,
( ~ p39(sK188(X1))
| p39(X1)
| r1(X1,sK186(X1))
| ~ r1(X0,X1)
| ~ sP37(X0) ) ).
cnf(u653,axiom,
( ~ p49(sK161(X1))
| p49(X1)
| r1(sK159(X1),sK160(X1))
| ~ r1(X0,X1)
| ~ sP46(X0) ) ).
cnf(u392,axiom,
( ~ p71(sK95(X1))
| p71(X1)
| r1(X1,sK93(X1))
| ~ r1(X0,X1)
| ~ sP68(X0) ) ).
cnf(u1175,axiom,
( ~ p4(sK293(X1))
| p4(X1)
| p3(sK291(X1))
| ~ r1(X0,X1)
| ~ sP2(X0) ) ).
cnf(u921,axiom,
( ~ sP24(X0)
| p26(X1)
| r1(X1,sK225(X1))
| r1(X1,sK227(X1))
| ~ r1(X0,X1) ) ).
cnf(u1157,axiom,
( ~ p6(sK287(X1))
| p6(X1)
| r1(sK285(X1),sK286(X1))
| ~ r1(X0,X1)
| ~ sP4(X0) ) ).
cnf(u1067,axiom,
( ~ p13(sK266(X1))
| p13(X1)
| p12(sK264(X1))
| ~ r1(X0,X1)
| ~ sP11(X0) ) ).
cnf(u651,axiom,
( ~ p49(sK160(X1))
| p49(X1)
| ~ r1(X0,X1)
| r1(X1,sK161(X1))
| ~ sP46(X0) ) ).
cnf(u706,axiom,
( ~ sP41(X0)
| p44(X1)
| p43(sK174(X1))
| p43(X1)
| ~ r1(X0,X1) ) ).
cnf(u1056,axiom,
( ~ sP12(X0)
| p14(X1)
| p13(sK261(X1))
| r1(X1,sK263(X1))
| ~ r1(X0,X1) ) ).
cnf(u935,axiom,
( ~ p24(sK233(X1))
| p24(X1)
| p23(sK231(X1))
| ~ r1(X0,X1)
| ~ sP22(X0) ) ).
cnf(u548,axiom,
( ~ p58(sK134(X1))
| p58(X1)
| r1(X1,sK132(X1))
| ~ r1(X0,X1)
| ~ sP55(X0) ) ).
cnf(u411,axiom,
( ~ p69(sK100(X1))
| p69(X1)
| ~ r1(X0,X1)
| r1(X1,sK101(X1))
| ~ sP66(X0) ) ).
cnf(u565,axiom,
( ~ p56(sK139(X1))
| p56(X1)
| ~ r1(X0,X1)
| p55(X1)
| ~ sP53(X0) ) ).
cnf(u1190,axiom,
( ~ p3(sK296(X1))
| p3(X1)
| ~ p3(sK295(X1))
| ~ r1(X0,X1)
| ~ sP1(X0) ) ).
cnf(u797,axiom,
( ~ p36(sK197(X1))
| p36(X1)
| r1(sK195(X1),sK196(X1))
| ~ r1(X0,X1)
| ~ sP34(X0) ) ).
cnf(u1195,axiom,
( ~ sP1(X0)
| p3(X1)
| r1(X1,sK294(X1))
| p2(X1)
| ~ r1(X0,X1) ) ).
cnf(u795,axiom,
( ~ p36(sK196(X1))
| p36(X1)
| ~ r1(X0,X1)
| r1(X1,sK197(X1))
| ~ sP34(X0) ) ).
cnf(u1184,axiom,
( ~ p4(sK293(X1))
| p4(X1)
| r1(X1,sK291(X1))
| ~ r1(X0,X1)
| ~ sP2(X0) ) ).
cnf(u904,axiom,
( ~ sP25(X0)
| p27(X1)
| r1(sK222(X1),sK223(X1))
| p26(X1)
| ~ r1(X0,X1) ) ).
cnf(u409,axiom,
( ~ p69(sK100(X1))
| p69(X1)
| ~ r1(X0,X1)
| p68(X1)
| ~ sP66(X0) ) ).
cnf(u676,axiom,
( ~ sP44(X0)
| p47(X1)
| r1(sK165(X1),sK166(X1))
| p46(X1)
| ~ r1(X0,X1) ) ).
cnf(u980,axiom,
( ~ p21(sK242(X1))
| p21(X1)
| r1(X1,sK240(X1))
| ~ r1(X0,X1)
| ~ sP19(X0) ) ).
cnf(u693,axiom,
( ~ sP43(X0)
| p46(X1)
| r1(X1,sK168(X1))
| r1(X1,sK170(X1))
| ~ r1(X0,X1) ) ).
cnf(u925,axiom,
( ~ p25(sK229(X1))
| p25(X1)
| ~ r1(X0,X1)
| p24(X1)
| ~ sP23(X0) ) ).
cnf(u810,axiom,
( ~ sP33(X0)
| p35(X1)
| r1(sK198(X1),sK199(X1))
| r1(X1,sK200(X1))
| ~ r1(X0,X1) ) ).
cnf(u691,axiom,
( ~ sP43(X0)
| p46(X1)
| r1(X1,sK168(X1))
| p45(X1)
| ~ r1(X0,X1) ) ).
cnf(u1121,axiom,
( ~ p9(sK278(X1))
| p9(X1)
| r1(sK276(X1),sK277(X1))
| ~ r1(X0,X1)
| ~ sP7(X0) ) ).
cnf(u816,axiom,
( ~ sP32(X0)
| p34(X1)
| p33(sK201(X1))
| r1(X1,sK203(X1))
| ~ r1(X0,X1) ) ).
cnf(u1049,axiom,
( ~ p15(sK260(X1))
| p15(X1)
| r1(sK258(X1),sK259(X1))
| ~ r1(X0,X1)
| ~ sP13(X0) ) ).
cnf(u438,axiom,
( ~ sP64(X0)
| p67(X1)
| r1(sK105(X1),sK106(X1))
| r1(X1,sK107(X1))
| ~ r1(X0,X1) ) ).
cnf(u572,axiom,
( ~ p56(sK140(X1))
| p56(X1)
| r1(X1,sK138(X1))
| ~ r1(X0,X1)
| ~ sP53(X0) ) ).
cnf(u567,axiom,
( ~ p56(sK139(X1))
| p56(X1)
| ~ r1(X0,X1)
| r1(X1,sK140(X1))
| ~ sP53(X0) ) ).
cnf(u938,axiom,
( ~ p24(sK233(X1))
| p24(X1)
| ~ p24(sK232(X1))
| ~ r1(X0,X1)
| ~ sP22(X0) ) ).
cnf(u582,axiom,
( ~ sP52(X0)
| p55(X1)
| r1(sK141(X1),sK142(X1))
| r1(X1,sK143(X1))
| ~ r1(X0,X1) ) ).
cnf(u944,axiom,
( ~ p24(sK233(X1))
| p24(X1)
| r1(X1,sK231(X1))
| ~ r1(X0,X1)
| ~ sP22(X0) ) ).
cnf(u321,axiom,
( ~ sP74(X0)
| p77(X1)
| r1(X1,sK75(X1))
| r1(X1,sK77(X1))
| ~ r1(X0,X1) ) ).
cnf(u588,axiom,
( ~ sP51(X0)
| p54(X1)
| p53(sK144(X1))
| r1(X1,sK146(X1))
| ~ r1(X0,X1) ) ).
cnf(u681,axiom,
( ~ sP44(X0)
| p47(X1)
| r1(X1,sK165(X1))
| r1(X1,sK167(X1))
| ~ r1(X0,X1) ) ).
cnf(u436,axiom,
( ~ sP64(X0)
| p67(X1)
| r1(sK105(X1),sK106(X1))
| p66(X1)
| ~ r1(X0,X1) ) ).
cnf(u837,axiom,
( ~ sP31(X0)
| p33(X1)
| r1(X1,sK204(X1))
| r1(X1,sK206(X1))
| ~ r1(X0,X1) ) ).
cnf(u695,axiom,
( ~ p45(sK173(X1))
| p45(X1)
| p44(sK171(X1))
| ~ r1(X0,X1)
| ~ sP42(X0) ) ).
cnf(u570,axiom,
( ~ sP53(X0)
| p56(X1)
| r1(sK138(X1),sK139(X1))
| r1(X1,sK140(X1))
| ~ r1(X0,X1) ) ).
cnf(u987,axiom,
( ~ p20(sK244(X1))
| p20(X1)
| ~ r1(X0,X1)
| r1(X1,sK245(X1))
| ~ sP18(X0) ) ).
cnf(u835,axiom,
( ~ sP31(X0)
| p33(X1)
| r1(X1,sK204(X1))
| p32(X1)
| ~ r1(X0,X1) ) ).
cnf(u710,axiom,
( ~ p44(sK176(X1))
| p44(X1)
| ~ p44(sK175(X1))
| ~ r1(X0,X1)
| ~ sP41(X0) ) ).
cnf(u327,axiom,
( ~ p76(sK79(X1))
| p76(X1)
| ~ r1(X0,X1)
| r1(X1,sK80(X1))
| ~ sP73(X0) ) ).
cnf(u806,axiom,
( ~ p35(sK200(X1))
| p35(X1)
| ~ p35(sK199(X1))
| ~ r1(X0,X1)
| ~ sP33(X0) ) ).
cnf(u449,axiom,
( ~ p66(sK110(X1))
| p66(X1)
| r1(sK108(X1),sK109(X1))
| ~ r1(X0,X1)
| ~ sP63(X0) ) ).
cnf(u1201,axiom,
( ~ p2(sK298(X1))
| p2(X1)
| ~ r1(X0,X1)
| p1(X1)
| ~ sP0(X0) ) ).
cnf(u965,axiom,
( ~ p22(sK239(X1))
| p22(X1)
| r1(sK237(X1),sK238(X1))
| ~ r1(X0,X1)
| ~ sP20(X0) ) ).
cnf(u850,axiom,
( ~ sP29(X0)
| p31(X1)
| p30(sK210(X1))
| p30(X1)
| ~ r1(X0,X1) ) ).
cnf(u698,axiom,
( ~ p45(sK173(X1))
| p45(X1)
| ~ p45(sK172(X1))
| ~ r1(X0,X1)
| ~ sP42(X0) ) ).
cnf(u963,axiom,
( ~ p22(sK238(X1))
| p22(X1)
| ~ r1(X0,X1)
| r1(X1,sK239(X1))
| ~ sP20(X0) ) ).
cnf(u856,axiom,
( ~ sP29(X0)
| p31(X1)
| r1(sK210(X1),sK211(X1))
| p30(X1)
| ~ r1(X0,X1) ) ).
cnf(u325,axiom,
( ~ p76(sK79(X1))
| p76(X1)
| ~ r1(X0,X1)
| p75(X1)
| ~ sP73(X0) ) ).
cnf(u576,axiom,
( ~ sP52(X0)
| p55(X1)
| p54(sK141(X1))
| r1(X1,sK143(X1))
| ~ r1(X0,X1) ) ).
cnf(u593,axiom,
( ~ p54(sK146(X1))
| p54(X1)
| r1(sK144(X1),sK145(X1))
| ~ r1(X0,X1)
| ~ sP51(X0) ) ).
cnf(u348,axiom,
( ~ sP71(X0)
| p74(X1)
| p73(sK84(X1))
| r1(X1,sK86(X1))
| ~ r1(X0,X1) ) ).
cnf(u605,axiom,
( ~ p53(sK149(X1))
| p53(X1)
| r1(sK147(X1),sK148(X1))
| ~ r1(X0,X1)
| ~ sP50(X0) ) ).
cnf(u1109,axiom,
( ~ p10(sK275(X1))
| p10(X1)
| r1(sK273(X1),sK274(X1))
| ~ r1(X0,X1)
| ~ sP8(X0) ) ).
cnf(u607,axiom,
( ~ sP50(X0)
| p53(X1)
| r1(X1,sK147(X1))
| p52(X1)
| ~ r1(X0,X1) ) ).
cnf(u978,axiom,
( ~ sP19(X0)
| p21(X1)
| r1(sK240(X1),sK241(X1))
| r1(X1,sK242(X1))
| ~ r1(X0,X1) ) ).
cnf(u1090,axiom,
( ~ sP9(X0)
| p11(X1)
| p10(sK270(X1))
| p10(X1)
| ~ r1(X0,X1) ) ).
cnf(u367,axiom,
( ~ sP70(X0)
| p73(X1)
| r1(X1,sK87(X1))
| p72(X1)
| ~ r1(X0,X1) ) ).
cnf(u453,axiom,
( ~ sP63(X0)
| p66(X1)
| r1(X1,sK108(X1))
| r1(X1,sK110(X1))
| ~ r1(X0,X1) ) ).
cnf(u622,axiom,
( ~ sP48(X0)
| p51(X1)
| p50(sK153(X1))
| p50(X1)
| ~ r1(X0,X1) ) ).
cnf(u338,axiom,
( ~ p75(sK83(X1))
| p75(X1)
| ~ p75(sK82(X1))
| ~ r1(X0,X1)
| ~ sP72(X0) ) ).
cnf(u721,axiom,
( ~ p43(sK178(X1))
| p43(X1)
| ~ r1(X0,X1)
| p42(X1)
| ~ sP40(X0) ) ).
cnf(u476,axiom,
( ~ p64(sK116(X1))
| p64(X1)
| r1(X1,sK114(X1))
| ~ r1(X0,X1)
| ~ sP61(X0) ) ).
cnf(u854,axiom,
( ~ p31(sK212(X1))
| p31(X1)
| ~ p31(sK211(X1))
| ~ r1(X0,X1)
| ~ sP29(X0) ) ).
cnf(u735,axiom,
( ~ p42(sK181(X1))
| p42(X1)
| ~ r1(X0,X1)
| r1(X1,sK182(X1))
| ~ sP39(X0) ) ).
cnf(u610,axiom,
( ~ sP49(X0)
| p52(X1)
| p51(sK150(X1))
| p51(X1)
| ~ r1(X0,X1) ) ).
cnf(u967,axiom,
( ~ sP20(X0)
| p22(X1)
| r1(X1,sK237(X1))
| p21(X1)
| ~ r1(X0,X1) ) ).
cnf(u860,axiom,
( ~ p31(sK212(X1))
| p31(X1)
| r1(X1,sK210(X1))
| ~ r1(X0,X1)
| ~ sP29(X0) ) ).
cnf(u1126,axiom,
( ~ sP6(X0)
| p8(X1)
| p7(sK279(X1))
| p7(X1)
| ~ r1(X0,X1) ) ).
cnf(u365,axiom,
( ~ p73(sK89(X1))
| p73(X1)
| r1(sK87(X1),sK88(X1))
| ~ r1(X0,X1)
| ~ sP70(X0) ) ).
cnf(u616,axiom,
( ~ sP49(X0)
| p52(X1)
| r1(sK150(X1),sK151(X1))
| p51(X1)
| ~ r1(X0,X1) ) ).
cnf(u422,axiom,
( ~ p68(sK104(X1))
| p68(X1)
| ~ p68(sK103(X1))
| ~ r1(X0,X1)
| ~ sP65(X0) ) ).
cnf(u1119,axiom,
( ~ p9(sK277(X1))
| p9(X1)
| ~ r1(X0,X1)
| r1(X1,sK278(X1))
| ~ sP7(X0) ) ).
cnf(u466,axiom,
( ~ sP61(X0)
| p64(X1)
| p63(sK114(X1))
| p63(X1)
| ~ r1(X0,X1) ) ).
cnf(u865,axiom,
( ~ p30(sK214(X1))
| p30(X1)
| ~ r1(X0,X1)
| p29(X1)
| ~ sP28(X0) ) ).
cnf(u1149,axiom,
( ~ sP5(X0)
| p7(X1)
| r1(X1,sK282(X1))
| r1(X1,sK284(X1))
| ~ r1(X0,X1) ) ).
cnf(u982,axiom,
( ~ sP18(X0)
| p20(X1)
| p19(sK243(X1))
| p19(X1)
| ~ r1(X0,X1) ) ).
cnf(u879,axiom,
( ~ p29(sK217(X1))
| p29(X1)
| ~ r1(X0,X1)
| r1(X1,sK218(X1))
| ~ sP27(X0) ) ).
cnf(u738,axiom,
( ~ sP39(X0)
| p42(X1)
| r1(sK180(X1),sK181(X1))
| r1(X1,sK182(X1))
| ~ r1(X0,X1) ) ).
cnf(u988,axiom,
( ~ sP18(X0)
| p20(X1)
| r1(sK243(X1),sK244(X1))
| p19(X1)
| ~ r1(X0,X1) ) ).
cnf(u355,axiom,
( ~ sP71(X0)
| p74(X1)
| r1(X1,sK84(X1))
| p73(X1)
| ~ r1(X0,X1) ) ).
cnf(u493,axiom,
( ~ p62(sK121(X1))
| p62(X1)
| ~ r1(X0,X1)
| p61(X1)
| ~ sP59(X0) ) ).
cnf(u378,axiom,
( ~ sP69(X0)
| p72(X1)
| r1(sK90(X1),sK91(X1))
| r1(X1,sK92(X1))
| ~ r1(X0,X1) ) ).
cnf(u464,axiom,
( ~ p65(sK113(X1))
| p65(X1)
| r1(X1,sK111(X1))
| ~ r1(X0,X1)
| ~ sP62(X0) ) ).
cnf(u993,axiom,
( ~ sP18(X0)
| p20(X1)
| r1(X1,sK243(X1))
| r1(X1,sK245(X1))
| ~ r1(X0,X1) ) ).
cnf(u1139,axiom,
( ~ p7(sK284(X1))
| p7(X1)
| p6(sK282(X1))
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u894,axiom,
( ~ sP26(X0)
| p28(X1)
| r1(sK219(X1),sK220(X1))
| r1(X1,sK221(X1))
| ~ r1(X0,X1) ) ).
cnf(u723,axiom,
( ~ p43(sK178(X1))
| p43(X1)
| ~ r1(X0,X1)
| r1(X1,sK179(X1))
| ~ sP40(X0) ) ).
cnf(u1128,axiom,
( ~ sP6(X0)
| p8(X1)
| p7(sK279(X1))
| r1(X1,sK281(X1))
| ~ r1(X0,X1) ) ).
cnf(u1007,axiom,
( ~ p18(sK251(X1))
| p18(X1)
| p17(sK249(X1))
| ~ r1(X0,X1)
| ~ sP16(X0) ) ).
cnf(u1133,axiom,
( ~ p8(sK281(X1))
| p8(X1)
| r1(sK279(X1),sK280(X1))
| ~ r1(X0,X1)
| ~ sP6(X0) ) ).
cnf(u772,axiom,
( ~ sP36(X0)
| p38(X1)
| r1(sK189(X1),sK190(X1))
| p37(X1)
| ~ r1(X0,X1) ) ).
cnf(u1038,axiom,
( ~ sP14(X0)
| p16(X1)
| r1(sK255(X1),sK256(X1))
| r1(X1,sK257(X1))
| ~ r1(X0,X1) ) ).
cnf(u483,axiom,
( ~ p63(sK118(X1))
| p63(X1)
| ~ r1(X0,X1)
| r1(X1,sK119(X1))
| ~ sP60(X0) ) ).
cnf(u637,axiom,
( ~ p50(sK157(X1))
| p50(X1)
| ~ r1(X0,X1)
| p49(X1)
| ~ sP47(X0) ) ).
cnf(u376,axiom,
( ~ sP69(X0)
| p72(X1)
| r1(sK90(X1),sK91(X1))
| p71(X1)
| ~ r1(X0,X1) ) ).
cnf(u777,axiom,
( ~ sP36(X0)
| p38(X1)
| r1(X1,sK189(X1))
| r1(X1,sK191(X1))
| ~ r1(X0,X1) ) ).
cnf(u1022,axiom,
( ~ p17(sK254(X1))
| p17(X1)
| ~ p17(sK253(X1))
| ~ r1(X0,X1)
| ~ sP15(X0) ) ).
cnf(u434,axiom,
( ~ p67(sK107(X1))
| p67(X1)
| ~ p67(sK106(X1))
| ~ r1(X0,X1)
| ~ sP64(X0) ) ).
cnf(u1036,axiom,
( ~ sP14(X0)
| p16(X1)
| r1(sK255(X1),sK256(X1))
| p15(X1)
| ~ r1(X0,X1) ) ).
cnf(u1166,axiom,
( ~ p5(sK290(X1))
| p5(X1)
| ~ p5(sK289(X1))
| ~ r1(X0,X1)
| ~ sP3(X0) ) ).
cnf(u382,axiom,
( ~ sP68(X0)
| p71(X1)
| p70(sK93(X1))
| p70(X1)
| ~ r1(X0,X1) ) ).
cnf(u765,axiom,
( ~ sP37(X0)
| p39(X1)
| r1(X1,sK186(X1))
| r1(X1,sK188(X1))
| ~ r1(X0,X1) ) ).
cnf(u504,axiom,
( ~ sP58(X0)
| p61(X1)
| p60(sK123(X1))
| r1(X1,sK125(X1))
| ~ r1(X0,X1) ) ).
cnf(u1159,axiom,
( ~ sP4(X0)
| p6(X1)
| r1(X1,sK285(X1))
| p5(X1)
| ~ r1(X0,X1) ) ).
cnf(u905,axiom,
( ~ p27(sK224(X1))
| p27(X1)
| r1(sK222(X1),sK223(X1))
| ~ r1(X0,X1)
| ~ sP25(X0) ) ).
cnf(u1051,axiom,
( ~ sP13(X0)
| p15(X1)
| r1(X1,sK258(X1))
| p14(X1)
| ~ r1(X0,X1) ) ).
cnf(u763,axiom,
( ~ sP37(X0)
| p39(X1)
| r1(X1,sK186(X1))
| p38(X1)
| ~ r1(X0,X1) ) ).
cnf(u526,axiom,
( ~ sP56(X0)
| p59(X1)
| p58(sK129(X1))
| p58(X1)
| ~ r1(X0,X1) ) ).
cnf(u1040,axiom,
( ~ p16(sK257(X1))
| p16(X1)
| r1(X1,sK255(X1))
| ~ r1(X0,X1)
| ~ sP14(X0) ) ).
cnf(u919,axiom,
( ~ sP24(X0)
| p26(X1)
| r1(X1,sK225(X1))
| p25(X1)
| ~ r1(X0,X1) ) ).
cnf(u842,axiom,
( ~ p32(sK209(X1))
| p32(X1)
| ~ p32(sK208(X1))
| ~ r1(X0,X1)
| ~ sP30(X0) ) ).
cnf(u532,axiom,
( ~ sP56(X0)
| p59(X1)
| r1(sK129(X1),sK130(X1))
| p58(X1)
| ~ r1(X0,X1) ) ).
cnf(u395,axiom,
( ~ p70(sK98(X1))
| p70(X1)
| p69(sK96(X1))
| ~ r1(X0,X1)
| ~ sP67(X0) ) ).
cnf(u549,axiom,
( ~ sP55(X0)
| p58(X1)
| r1(X1,sK132(X1))
| r1(X1,sK134(X1))
| ~ r1(X0,X1) ) ).
cnf(u510,axiom,
( ~ sP58(X0)
| p61(X1)
| r1(sK123(X1),sK124(X1))
| r1(X1,sK125(X1))
| ~ r1(X0,X1) ) ).
cnf(u781,axiom,
( ~ p37(sK193(X1))
| p37(X1)
| ~ r1(X0,X1)
| p36(X1)
| ~ sP35(X0) ) ).
cnf(u547,axiom,
( ~ sP55(X0)
| p58(X1)
| r1(X1,sK132(X1))
| p57(X1)
| ~ r1(X0,X1) ) ).
cnf(u1205,axiom,
( ~ p2(sK299(X1))
| p2(X1)
| r1(sK297(X1),sK298(X1))
| ~ r1(X0,X1)
| ~ sP0(X0) ) ).
cnf(u654,axiom,
( ~ sP46(X0)
| p49(X1)
| r1(sK159(X1),sK160(X1))
| r1(X1,sK161(X1))
| ~ r1(X0,X1) ) ).
cnf(u1168,axiom,
( ~ sP3(X0)
| p5(X1)
| r1(sK288(X1),sK289(X1))
| p4(X1)
| ~ r1(X0,X1) ) ).
cnf(u1016,axiom,
( ~ p18(sK251(X1))
| p18(X1)
| r1(X1,sK249(X1))
| ~ r1(X0,X1)
| ~ sP16(X0) ) ).
cnf(u1076,axiom,
( ~ p13(sK266(X1))
| p13(X1)
| r1(X1,sK264(X1))
| ~ r1(X0,X1)
| ~ sP11(X0) ) ).
cnf(u540,axiom,
( ~ sP55(X0)
| p58(X1)
| p57(sK132(X1))
| r1(X1,sK134(X1))
| ~ r1(X0,X1) ) ).
cnf(u393,axiom,
( ~ sP68(X0)
| p71(X1)
| r1(X1,sK93(X1))
| r1(X1,sK95(X1))
| ~ r1(X0,X1) ) ).
cnf(u660,axiom,
( ~ sP45(X0)
| p48(X1)
| p47(sK162(X1))
| r1(X1,sK164(X1))
| ~ r1(X0,X1) ) ).
cnf(u491,axiom,
( ~ p62(sK122(X1))
| p62(X1)
| p61(sK120(X1))
| ~ r1(X0,X1)
| ~ sP59(X0) ) ).
cnf(u677,axiom,
( ~ p47(sK167(X1))
| p47(X1)
| r1(sK165(X1),sK166(X1))
| ~ r1(X0,X1)
| ~ sP44(X0) ) ).
cnf(u909,axiom,
( ~ sP25(X0)
| p27(X1)
| r1(X1,sK222(X1))
| r1(X1,sK224(X1))
| ~ r1(X0,X1) ) ).
cnf(u794,axiom,
( ~ p36(sK197(X1))
| p36(X1)
| ~ p36(sK196(X1))
| ~ r1(X0,X1)
| ~ sP34(X0) ) ).
cnf(u675,axiom,
( ~ p47(sK166(X1))
| p47(X1)
| ~ r1(X0,X1)
| r1(X1,sK167(X1))
| ~ sP44(X0) ) ).
cnf(u566,axiom,
( ~ p56(sK140(X1))
| p56(X1)
| ~ p56(sK139(X1))
| ~ r1(X0,X1)
| ~ sP53(X0) ) ).
cnf(u907,axiom,
( ~ sP25(X0)
| p27(X1)
| r1(X1,sK222(X1))
| p26(X1)
| ~ r1(X0,X1) ) ).
cnf(u800,axiom,
( ~ p36(sK197(X1))
| p36(X1)
| r1(X1,sK195(X1))
| ~ r1(X0,X1)
| ~ sP34(X0) ) ).
cnf(u537,axiom,
( ~ sP56(X0)
| p59(X1)
| r1(X1,sK129(X1))
| r1(X1,sK131(X1))
| ~ r1(X0,X1) ) ).
cnf(u821,axiom,
( ~ p34(sK203(X1))
| p34(X1)
| r1(sK201(X1),sK202(X1))
| ~ r1(X0,X1)
| ~ sP32(X0) ) ).
cnf(u734,axiom,
( ~ p42(sK182(X1))
| p42(X1)
| ~ p42(sK181(X1))
| ~ r1(X0,X1)
| ~ sP39(X0) ) ).
cnf(u551,axiom,
( ~ p57(sK137(X1))
| p57(X1)
| p56(sK135(X1))
| ~ r1(X0,X1)
| ~ sP54(X0) ) ).
cnf(u922,axiom,
( ~ sP23(X0)
| p25(X1)
| p24(sK228(X1))
| p24(X1)
| ~ r1(X0,X1) ) ).
cnf(u819,axiom,
( ~ p34(sK202(X1))
| p34(X1)
| ~ r1(X0,X1)
| r1(X1,sK203(X1))
| ~ sP32(X0) ) ).
cnf(u694,axiom,
( ~ sP42(X0)
| p45(X1)
| p44(sK171(X1))
| p44(X1)
| ~ r1(X0,X1) ) ).
cnf(u928,axiom,
( ~ sP23(X0)
| p25(X1)
| r1(sK228(X1),sK229(X1))
| p24(X1)
| ~ r1(X0,X1) ) ).
cnf(u311,axiom,
( ~ p77(sK77(X1))
| p77(X1)
| p76(sK75(X1))
| ~ r1(X0,X1)
| ~ sP74(X0) ) ).
cnf(u700,axiom,
( ~ sP42(X0)
| p45(X1)
| r1(sK171(X1),sK172(X1))
| p44(X1)
| ~ r1(X0,X1) ) ).
cnf(u665,axiom,
( ~ p48(sK164(X1))
| p48(X1)
| r1(sK162(X1),sK163(X1))
| ~ r1(X0,X1)
| ~ sP45(X0) ) ).
cnf(u420,axiom,
( ~ sP65(X0)
| p68(X1)
| p67(sK102(X1))
| r1(X1,sK104(X1))
| ~ r1(X0,X1) ) ).
cnf(u949,axiom,
( ~ p23(sK235(X1))
| p23(X1)
| ~ r1(X0,X1)
| p22(X1)
| ~ sP21(X0) ) ).
cnf(u1592,negated_conjecture,
r1(sK300,sK450) ).
cnf(u679,axiom,
( ~ sP44(X0)
| p47(X1)
| r1(X1,sK165(X1))
| p46(X1)
| ~ r1(X0,X1) ) ).
cnf(u554,axiom,
( ~ p57(sK137(X1))
| p57(X1)
| ~ p57(sK136(X1))
| ~ r1(X0,X1)
| ~ sP54(X0) ) ).
cnf(u947,axiom,
( ~ p23(sK236(X1))
| p23(X1)
| p22(sK234(X1))
| ~ r1(X0,X1)
| ~ sP21(X0) ) ).
cnf(u560,axiom,
( ~ p57(sK137(X1))
| p57(X1)
| r1(X1,sK135(X1))
| ~ r1(X0,X1)
| ~ sP54(X0) ) ).
cnf(u439,axiom,
( ~ sP64(X0)
| p67(X1)
| r1(X1,sK105(X1))
| p66(X1)
| ~ r1(X0,X1) ) ).
cnf(u1185,axiom,
( ~ sP2(X0)
| p4(X1)
| r1(X1,sK291(X1))
| r1(X1,sK293(X1))
| ~ r1(X0,X1) ) ).
cnf(u614,axiom,
( ~ p52(sK152(X1))
| p52(X1)
| ~ p52(sK151(X1))
| ~ r1(X0,X1)
| ~ sP49(X0) ) ).
cnf(u745,axiom,
( ~ p41(sK184(X1))
| p41(X1)
| ~ r1(X0,X1)
| p40(X1)
| ~ sP38(X0) ) ).
cnf(u563,axiom,
( ~ p56(sK140(X1))
| p56(X1)
| p55(sK138(X1))
| ~ r1(X0,X1)
| ~ sP53(X0) ) ).
cnf(u834,axiom,
( ~ sP31(X0)
| p33(X1)
| r1(sK204(X1),sK205(X1))
| r1(X1,sK206(X1))
| ~ r1(X0,X1) ) ).
cnf(u1074,axiom,
( ~ sP11(X0)
| p13(X1)
| r1(sK264(X1),sK265(X1))
| r1(X1,sK266(X1))
| ~ r1(X0,X1) ) ).
cnf(u840,axiom,
( ~ sP30(X0)
| p32(X1)
| p31(sK207(X1))
| r1(X1,sK209(X1))
| ~ r1(X0,X1) ) ).
cnf(u437,axiom,
( ~ p67(sK107(X1))
| p67(X1)
| r1(sK105(X1),sK106(X1))
| ~ r1(X0,X1)
| ~ sP64(X0) ) ).
cnf(u688,axiom,
( ~ sP43(X0)
| p46(X1)
| r1(sK168(X1),sK169(X1))
| p45(X1)
| ~ r1(X0,X1) ) ).
cnf(u801,axiom,
( ~ sP34(X0)
| p36(X1)
| r1(X1,sK195(X1))
| r1(X1,sK197(X1))
| ~ r1(X0,X1) ) ).
cnf(u577,axiom,
( ~ p55(sK142(X1))
| p55(X1)
| ~ r1(X0,X1)
| p54(X1)
| ~ sP52(X0) ) ).
cnf(u332,axiom,
( ~ p76(sK80(X1))
| p76(X1)
| r1(X1,sK78(X1))
| ~ r1(X0,X1)
| ~ sP73(X0) ) ).
cnf(u1073,axiom,
( ~ p13(sK266(X1))
| p13(X1)
| r1(sK264(X1),sK265(X1))
| ~ r1(X0,X1)
| ~ sP11(X0) ) ).
cnf(u1093,axiom,
( ~ p11(sK271(X1))
| p11(X1)
| ~ r1(X0,X1)
| p10(X1)
| ~ sP9(X0) ) ).
cnf(u591,axiom,
( ~ p54(sK145(X1))
| p54(X1)
| ~ r1(X0,X1)
| r1(X1,sK146(X1))
| ~ sP51(X0) ) ).
cnf(u962,axiom,
( ~ p22(sK239(X1))
| p22(X1)
| ~ p22(sK238(X1))
| ~ r1(X0,X1)
| ~ sP20(X0) ) ).
cnf(u1202,axiom,
( ~ p2(sK299(X1))
| p2(X1)
| ~ p2(sK298(X1))
| ~ r1(X0,X1)
| ~ sP0(X0) ) ).
cnf(u351,axiom,
( ~ p74(sK85(X1))
| p74(X1)
| ~ r1(X0,X1)
| r1(X1,sK86(X1))
| ~ sP71(X0) ) ).
cnf(u322,axiom,
( ~ sP73(X0)
| p76(X1)
| p75(sK78(X1))
| p75(X1)
| ~ r1(X0,X1) ) ).
cnf(u705,axiom,
( ~ sP42(X0)
| p45(X1)
| r1(X1,sK171(X1))
| r1(X1,sK173(X1))
| ~ r1(X0,X1) ) ).
cnf(u460,axiom,
( ~ sP62(X0)
| p65(X1)
| r1(sK111(X1),sK112(X1))
| p64(X1)
| ~ r1(X0,X1) ) ).
cnf(u599,axiom,
( ~ p53(sK149(X1))
| p53(X1)
| p52(sK147(X1))
| ~ r1(X0,X1)
| ~ sP50(X0) ) ).
cnf(u838,axiom,
( ~ sP30(X0)
| p32(X1)
| p31(sK207(X1))
| p31(X1)
| ~ r1(X0,X1) ) ).
cnf(u719,axiom,
( ~ p43(sK179(X1))
| p43(X1)
| p42(sK177(X1))
| ~ r1(X0,X1)
| ~ sP40(X0) ) ).
cnf(u1084,axiom,
( ~ sP10(X0)
| p12(X1)
| r1(sK267(X1),sK268(X1))
| p11(X1)
| ~ r1(X0,X1) ) ).
cnf(u844,axiom,
( ~ sP30(X0)
| p32(X1)
| r1(sK207(X1),sK208(X1))
| p31(X1)
| ~ r1(X0,X1) ) ).
cnf(u1110,axiom,
( ~ sP8(X0)
| p10(X1)
| r1(sK273(X1),sK274(X1))
| r1(X1,sK275(X1))
| ~ r1(X0,X1) ) ).
cnf(u349,axiom,
( ~ p74(sK85(X1))
| p74(X1)
| ~ r1(X0,X1)
| p73(X1)
| ~ sP71(X0) ) ).
cnf(u600,axiom,
( ~ sP50(X0)
| p53(X1)
| p52(sK147(X1))
| r1(X1,sK149(X1))
| ~ r1(X0,X1) ) ).
cnf(u450,axiom,
( ~ sP63(X0)
| p66(X1)
| r1(sK108(X1),sK109(X1))
| r1(X1,sK110(X1))
| ~ r1(X0,X1) ) ).
cnf(u849,axiom,
( ~ sP30(X0)
| p32(X1)
| r1(X1,sK207(X1))
| r1(X1,sK209(X1))
| ~ r1(X0,X1) ) ).
cnf(u966,axiom,
( ~ sP20(X0)
| p22(X1)
| r1(sK237(X1),sK238(X1))
| r1(X1,sK239(X1))
| ~ r1(X0,X1) ) ).
cnf(u863,axiom,
( ~ p30(sK215(X1))
| p30(X1)
| p29(sK213(X1))
| ~ r1(X0,X1)
| ~ sP28(X0) ) ).
cnf(u1114,axiom,
( ~ sP7(X0)
| p9(X1)
| p8(sK276(X1))
| p8(X1)
| ~ r1(X0,X1) ) ).
cnf(u1108,axiom,
( ~ sP8(X0)
| p10(X1)
| r1(sK273(X1),sK274(X1))
| p9(X1)
| ~ r1(X0,X1) ) ).
cnf(u339,axiom,
( ~ p75(sK82(X1))
| p75(X1)
| ~ r1(X0,X1)
| r1(X1,sK83(X1))
| ~ sP72(X0) ) ).
cnf(u4976,negated_conjecture,
( r1(X0,sK296(X0))
| p2(sK294(X0))
| p3(X0)
| ~ r1(sK300,X0) ) ).
cnf(u477,axiom,
( ~ sP61(X0)
| p64(X1)
| r1(X1,sK114(X1))
| r1(X1,sK116(X1))
| ~ r1(X0,X1) ) ).
cnf(u728,axiom,
( ~ p43(sK179(X1))
| p43(X1)
| r1(X1,sK177(X1))
| ~ r1(X0,X1)
| ~ sP40(X0) ) ).
cnf(u448,axiom,
( ~ sP63(X0)
| p66(X1)
| r1(sK108(X1),sK109(X1))
| p65(X1)
| ~ r1(X0,X1) ) ).
cnf(u977,axiom,
( ~ p21(sK242(X1))
| p21(X1)
| r1(sK240(X1),sK241(X1))
| ~ r1(X0,X1)
| ~ sP19(X0) ) ).
cnf(u1123,axiom,
( ~ sP7(X0)
| p9(X1)
| r1(X1,sK276(X1))
| p8(X1)
| ~ r1(X0,X1) ) ).
cnf(u878,axiom,
( ~ p29(sK218(X1))
| p29(X1)
| ~ p29(sK217(X1))
| ~ r1(X0,X1)
| ~ sP27(X0) ) ).
cnf(u1112,axiom,
( ~ p10(sK275(X1))
| p10(X1)
| r1(X1,sK273(X1))
| ~ r1(X0,X1)
| ~ sP8(X0) ) ).
cnf(u617,axiom,
( ~ p52(sK152(X1))
| p52(X1)
| r1(sK150(X1),sK151(X1))
| ~ r1(X0,X1)
| ~ sP49(X0) ) ).
cnf(u884,axiom,
( ~ p29(sK218(X1))
| p29(X1)
| r1(X1,sK216(X1))
| ~ r1(X0,X1)
| ~ sP27(X0) ) ).
cnf(u881,axiom,
( ~ p29(sK218(X1))
| p29(X1)
| r1(sK216(X1),sK217(X1))
| ~ r1(X0,X1)
| ~ sP27(X0) ) ).
cnf(u1150,axiom,
( ~ sP4(X0)
| p6(X1)
| p5(sK285(X1))
| p5(X1)
| ~ r1(X0,X1) ) ).
cnf(u467,axiom,
( ~ p64(sK116(X1))
| p64(X1)
| p63(sK114(X1))
| ~ r1(X0,X1)
| ~ sP61(X0) ) ).
cnf(u621,axiom,
( ~ sP49(X0)
| p52(X1)
| r1(X1,sK150(X1))
| r1(X1,sK152(X1))
| ~ r1(X0,X1) ) ).
cnf(u360,axiom,
( ~ sP70(X0)
| p73(X1)
| p72(sK87(X1))
| r1(X1,sK89(X1))
| ~ r1(X0,X1) ) ).
cnf(u1143,axiom,
( ~ p7(sK283(X1))
| p7(X1)
| ~ r1(X0,X1)
| r1(X1,sK284(X1))
| ~ sP5(X0) ) ).
cnf(u490,axiom,
( ~ sP59(X0)
| p62(X1)
| p61(sK120(X1))
| p61(X1)
| ~ r1(X0,X1) ) ).
cnf(u619,axiom,
( ~ sP49(X0)
| p52(X1)
| r1(X1,sK150(X1))
| p51(X1)
| ~ r1(X0,X1) ) ).
cnf(u1006,axiom,
( ~ sP16(X0)
| p18(X1)
| p17(sK249(X1))
| p17(X1)
| ~ r1(X0,X1) ) ).
cnf(u775,axiom,
( ~ sP36(X0)
| p38(X1)
| r1(X1,sK189(X1))
| p37(X1)
| ~ r1(X0,X1) ) ).
cnf(u1012,axiom,
( ~ sP16(X0)
| p18(X1)
| r1(sK249(X1),sK250(X1))
| p17(X1)
| ~ r1(X0,X1) ) ).
cnf(u379,axiom,
( ~ sP69(X0)
| p72(X1)
| r1(X1,sK90(X1))
| p71(X1)
| ~ r1(X0,X1) ) ).
cnf(u732,axiom,
( ~ sP39(X0)
| p42(X1)
| p41(sK180(X1))
| r1(X1,sK182(X1))
| ~ r1(X0,X1) ) ).
cnf(u366,axiom,
( ~ sP70(X0)
| p73(X1)
| r1(sK87(X1),sK88(X1))
| r1(X1,sK89(X1))
| ~ r1(X0,X1) ) ).
cnf(u749,axiom,
( ~ p41(sK185(X1))
| p41(X1)
| r1(sK183(X1),sK184(X1))
| ~ r1(X0,X1)
| ~ sP38(X0) ) ).
cnf(u488,axiom,
( ~ p63(sK119(X1))
| p63(X1)
| r1(X1,sK117(X1))
| ~ r1(X0,X1)
| ~ sP60(X0) ) ).
cnf(u1017,axiom,
( ~ sP16(X0)
| p18(X1)
| r1(X1,sK249(X1))
| r1(X1,sK251(X1))
| ~ r1(X0,X1) ) ).
cnf(u1035,axiom,
( ~ p16(sK256(X1))
| p16(X1)
| ~ r1(X0,X1)
| r1(X1,sK257(X1))
| ~ sP14(X0) ) ).
cnf(u747,axiom,
( ~ p41(sK184(X1))
| p41(X1)
| ~ r1(X0,X1)
| r1(X1,sK185(X1))
| ~ sP38(X0) ) ).
cnf(u638,axiom,
( ~ p50(sK158(X1))
| p50(X1)
| ~ p50(sK157(X1))
| ~ r1(X0,X1)
| ~ sP47(X0) ) ).
cnf(u1024,axiom,
( ~ sP15(X0)
| p17(X1)
| r1(sK252(X1),sK253(X1))
| p16(X1)
| ~ r1(X0,X1) ) ).
cnf(u903,axiom,
( ~ p27(sK223(X1))
| p27(X1)
| ~ r1(X0,X1)
| r1(X1,sK224(X1))
| ~ sP25(X0) ) ).
cnf(u674,axiom,
( ~ p47(sK167(X1))
| p47(X1)
| ~ p47(sK166(X1))
| ~ r1(X0,X1)
| ~ sP44(X0) ) ).
cnf(u377,axiom,
( ~ p72(sK92(X1))
| p72(X1)
| r1(sK90(X1),sK91(X1))
| ~ r1(X0,X1)
| ~ sP69(X0) ) ).
cnf(u516,axiom,
( ~ sP57(X0)
| p60(X1)
| p59(sK126(X1))
| r1(X1,sK128(X1))
| ~ r1(X0,X1) ) ).
cnf(u507,axiom,
( ~ p61(sK124(X1))
| p61(X1)
| ~ r1(X0,X1)
| r1(X1,sK125(X1))
| ~ sP58(X0) ) ).
cnf(u494,axiom,
( ~ p62(sK122(X1))
| p62(X1)
| ~ p62(sK121(X1))
| ~ r1(X0,X1)
| ~ sP59(X0) ) ).
cnf(u1145,axiom,
( ~ p7(sK284(X1))
| p7(X1)
| r1(sK282(X1),sK283(X1))
| ~ r1(X0,X1)
| ~ sP5(X0) ) ).
cnf(u531,axiom,
( ~ p59(sK130(X1))
| p59(X1)
| ~ r1(X0,X1)
| r1(X1,sK131(X1))
| ~ sP56(X0) ) ).
cnf(u7021,negated_conjecture,
( ~ r1(sK598(X1),sK449)
| ~ r1(X1,X0)
| ~ r1(sK300,X1)
| ~ p2(X0)
| p3(X1) ) ).
cnf(u891,axiom,
( ~ p28(sK220(X1))
| p28(X1)
| ~ r1(X0,X1)
| r1(X1,sK221(X1))
| ~ sP26(X0) ) ).
cnf(u766,axiom,
( ~ sP36(X0)
| p38(X1)
| p37(sK189(X1))
| p37(X1)
| ~ r1(X0,X1) ) ).
cnf(u1152,axiom,
( ~ sP4(X0)
| p6(X1)
| p5(sK285(X1))
| r1(X1,sK287(X1))
| ~ r1(X0,X1) ) ).
cnf(u1000,axiom,
( ~ sP17(X0)
| p19(X1)
| r1(sK246(X1),sK247(X1))
| p18(X1)
| ~ r1(X0,X1) ) ).
cnf(u1060,axiom,
( ~ sP12(X0)
| p14(X1)
| r1(sK261(X1),sK262(X1))
| p13(X1)
| ~ r1(X0,X1) ) ).
cnf(u972,axiom,
( ~ sP19(X0)
| p21(X1)
| p20(sK240(X1))
| r1(X1,sK242(X1))
| ~ r1(X0,X1) ) ).
cnf(u505,axiom,
( ~ p61(sK124(X1))
| p61(X1)
| ~ r1(X0,X1)
| p60(X1)
| ~ sP58(X0) ) ).
cnf(u644,axiom,
( ~ p50(sK158(X1))
| p50(X1)
| r1(X1,sK156(X1))
| ~ r1(X0,X1)
| ~ sP47(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL645+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n014.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 16:12:31 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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
% 8.57/2.70 % (980335)Detected formulas, will run a generic FOF schedule.
% 8.57/2.70 % (980342)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=1453464365:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.57/2.70 % (980343)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2014331185:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.57/2.70 % (980346)dis-21_1_sil=8000:lcm=predicate:random_seed=811741342: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)
% 8.57/2.70 % (980340)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=627167756:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.57/2.70 % (980344)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3708361609:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.57/2.70 % (980341)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=289078783:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.57/2.70 % (980345)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2341188222:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.57/2.70 % (980343)Instruction limit reached!
% 8.57/2.70 % (980343)------------------------------
% 8.57/2.70 % (980343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980343)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980343)Termination reason: Instruction limit
% 8.57/2.70 % (980343)Termination phase: Blocked clause elimination
% 8.57/2.70 % (980343)Time elapsed: 0.056 s
% 8.57/2.70 % (980343)Peak memory usage: 91 MB
% 8.57/2.70 % (980343)Instructions burned: 109 (million)
% 8.57/2.70 % (980344)Instruction limit reached!
% 8.57/2.70 % (980344)------------------------------
% 8.57/2.70 % (980344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980344)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980344)Termination reason: Instruction limit
% 8.57/2.70 % (980344)Termination phase: Saturation
% 8.57/2.70 % (980344)Time elapsed: 0.067 s
% 8.57/2.70 % (980344)Peak memory usage: 91 MB
% 8.57/2.70 % (980344)Instructions burned: 121 (million)
% 8.57/2.70 % (980346)Instruction limit reached!
% 8.57/2.70 % (980346)------------------------------
% 8.57/2.70 % (980346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980346)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980346)Termination reason: Instruction limit
% 8.57/2.70 % (980346)Termination phase: Saturation
% 8.57/2.70 % (980346)Time elapsed: 0.071 s
% 8.57/2.70 % (980346)Peak memory usage: 93 MB
% 8.57/2.70 % (980346)Instructions burned: 130 (million)
% 8.57/2.70 % (980345)Instruction limit reached!
% 8.57/2.70 % (980345)------------------------------
% 8.57/2.70 % (980345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980345)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980345)Termination reason: Instruction limit
% 8.57/2.70 % (980345)Termination phase: Saturation
% 8.57/2.70 % (980345)Time elapsed: 0.074 s
% 8.57/2.70 % (980345)Peak memory usage: 94 MB
% 8.57/2.70 % (980345)Instructions burned: 141 (million)
% 8.57/2.70 % (980354)lrs+10_1_sil=8000:sp=occurrence:random_seed=3158685001:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 8.57/2.70 % (980357)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=335139812:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 8.57/2.70 % (980356)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2798859441:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 8.57/2.70 % (980355)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3033907822:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.57/2.70 % (980357)Refutation not found, incomplete strategy
% 8.57/2.70 % (980357)------------------------------
% 8.57/2.70 % (980357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980357)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980357)Termination reason: Refutation not found, incomplete strategy
% 8.57/2.70 % (980357)Time elapsed: 0.064 s
% 8.57/2.70 % (980357)Peak memory usage: 94 MB
% 8.57/2.70 % (980357)Instructions burned: 119 (million)
% 8.57/2.70 % (980355)Refutation not found, incomplete strategy
% 8.57/2.70 % (980355)------------------------------
% 8.57/2.70 % (980355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980355)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980355)Termination reason: Refutation not found, incomplete strategy
% 8.57/2.70 % (980355)Time elapsed: 0.065 s
% 8.57/2.70 % (980355)Peak memory usage: 94 MB
% 8.57/2.70 % (980355)Instructions burned: 122 (million)
% 8.57/2.70 % (980354)Instruction limit reached!
% 8.57/2.70 % (980354)------------------------------
% 8.57/2.70 % (980354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980354)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980354)Termination reason: Instruction limit
% 8.57/2.70 % (980354)Termination phase: Saturation
% 8.57/2.70 % (980354)Time elapsed: 0.137 s
% 8.57/2.70 % (980354)Peak memory usage: 96 MB
% 8.57/2.70 % (980354)Instructions burned: 285 (million)
% 8.57/2.70 % (980356)Refutation not found, incomplete strategy
% 8.57/2.70 % (980356)------------------------------
% 8.57/2.70 % (980356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980356)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980356)Termination reason: Refutation not found, incomplete strategy
% 8.57/2.70 % (980356)Time elapsed: 0.144 s
% 8.57/2.70 % (980356)Peak memory usage: 96 MB
% 8.57/2.70 % (980356)Instructions burned: 276 (million)
% 8.57/2.70 % (980362)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2743901633:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 8.57/2.70 % (980357)------------------------------
% 8.57/2.70 % (980357)------------------------------
% 8.57/2.70 % (980355)------------------------------
% 8.57/2.70 % (980355)------------------------------
% 8.57/2.70 % (980362)Instruction limit reached!
% 8.57/2.70 % (980362)------------------------------
% 8.57/2.70 % (980362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980362)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980362)Termination reason: Instruction limit
% 8.57/2.70 % (980362)Termination phase: Saturation
% 8.57/2.70 % (980362)Time elapsed: 0.084 s
% 8.57/2.70 % (980362)Peak memory usage: 98 MB
% 8.57/2.70 % (980362)Instructions burned: 295 (million)
% 8.57/2.70 % (980356)------------------------------
% 8.57/2.70 % (980356)------------------------------
% 8.57/2.70 % (980366)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3770707022:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 8.57/2.70 % (980364)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3832499509:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 8.57/2.70 % (980365)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2122084640:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 8.57/2.70 % (980366)Instruction limit reached!
% 8.57/2.70 % (980366)------------------------------
% 8.57/2.70 % (980366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980366)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980366)Termination reason: Instruction limit
% 8.57/2.70 % (980366)Termination phase: Blocked clause elimination
% 8.57/2.70 % (980366)Time elapsed: 0.038 s
% 8.57/2.70 % (980366)Peak memory usage: 90 MB
% 8.57/2.70 % (980366)Instructions burned: 128 (million)
% 8.57/2.70 % (980365)Instruction limit reached!
% 8.57/2.70 % (980365)------------------------------
% 8.57/2.70 % (980365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980365)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980365)Termination reason: Instruction limit
% 8.57/2.70 % (980365)Termination phase: Saturation
% 8.57/2.70 % (980365)Time elapsed: 0.062 s
% 8.57/2.70 % (980365)Peak memory usage: 93 MB
% 8.57/2.70 % (980365)Instructions burned: 115 (million)
% 8.57/2.70 % (980367)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1495792180:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 8.57/2.70 % (980367)Instruction limit reached!
% 8.57/2.70 % (980367)------------------------------
% 8.57/2.70 % (980367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980367)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980367)Termination reason: Instruction limit
% 8.57/2.70 % (980367)Termination phase: Saturation
% 8.57/2.70 % (980367)Time elapsed: 0.061 s
% 8.57/2.70 % (980367)Peak memory usage: 91 MB
% 8.57/2.70 % (980367)Instructions burned: 116 (million)
% 8.57/2.70 % (980371)lrs+10_1_sil=8000:sp=occurrence:random_seed=203706580:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 8.57/2.70 % (980372)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=32219742:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 8.57/2.70 % (980375)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3003901934:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 8.57/2.70 % (980371)Instruction limit reached!
% 8.57/2.70 % (980371)------------------------------
% 8.57/2.70 % (980371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980371)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980371)Termination reason: Instruction limit
% 8.57/2.70 % (980371)Termination phase: Saturation
% 8.57/2.70 % (980371)Time elapsed: 0.226 s
% 8.57/2.70 % (980371)Peak memory usage: 104 MB
% 8.57/2.70 % (980371)Instructions burned: 908 (million)
% 8.57/2.70 % (980372)Instruction limit reached!
% 8.57/2.70 % (980372)------------------------------
% 8.57/2.70 % (980372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980372)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980372)Termination reason: Instruction limit
% 8.57/2.70 % (980372)Termination phase: Saturation
% 8.57/2.70 % (980372)Time elapsed: 0.220 s
% 8.57/2.70 % (980372)Peak memory usage: 110 MB
% 8.57/2.70 % (980372)Instructions burned: 437 (million)
% 8.57/2.70 % (980378)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4220962185:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 8.57/2.70 % (980378)Instruction limit reached!
% 8.57/2.70 % (980378)------------------------------
% 8.57/2.70 % (980378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980378)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980378)Termination reason: Instruction limit
% 8.57/2.70 % (980378)Termination phase: Saturation
% 8.57/2.70 % (980378)Time elapsed: 0.040 s
% 8.57/2.70 % (980378)Peak memory usage: 92 MB
% 8.57/2.70 % (980378)Instructions burned: 137 (million)
% 8.57/2.70 % (980379)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3332864684:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 8.57/2.70 % (980381)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3747179436:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 8.57/2.70 % (980341)First to succeed.
% 8.57/2.70 % (980341)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-980335"
% 8.57/2.70 % (980379)Instruction limit reached!
% 8.57/2.70 % (980379)------------------------------
% 8.57/2.70 % (980379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.70 % (980379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.70 % (980379)CaDiCaL version: 2.1.3
% 8.57/2.70 % (980379)Termination reason: Instruction limit
% 8.57/2.70 % (980379)Termination phase: Saturation
% 8.57/2.70 % (980379)Time elapsed: 0.265 s
% 8.57/2.70 % (980379)Peak memory usage: 101 MB
% 8.57/2.70 % (980379)Instructions burned: 593 (million)
% 8.57/2.70 % SZS status CounterSatisfiable for theBenchmark
% 8.57/2.70 % SZS output start Saturation.
% See solution above
% 13.46/2.90 % SZS output start Definitions and Model Updates.
% 13.46/2.90 % SZS output end Definitions and Model Updates.
% 13.46/2.90 % (980341)------------------------------
% 13.46/2.90 % (980341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.46/2.90 % (980341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.46/2.90 % (980341)CaDiCaL version: 2.1.3
% 13.46/2.90 % (980341)Termination reason: Satisfiable
% 13.46/2.90 % (980341)Time elapsed: 1.391 s
% 13.46/2.90 % (980341)Peak memory usage: 154 MB
% 13.46/2.90 % (980341)Instructions burned: 2098 (million)
% 13.46/2.90 % (980341)------------------------------
% 13.46/2.90 % (980341)------------------------------
% 13.46/2.90 % (980335)Success in time 1.844 s
% 13.46/2.90 % Vampire exiting
%------------------------------------------------------------------------------