↑ Up

CSE_E---1.7.UNS-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : CSE_E---1.7
% Problem  : SYO588-1 : TPTP v9.2.1. Bugfixed v5.5.1.
% Transfm  : none
% Format   : tptp:raw
% Command  : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d

% Computer : n018.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue May  5 05:53:49 PM UTC 2026

% Result   : Unsatisfiable 6.31s 4.21s
% Output   : CNFRefutation 6.31s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   75
%            Number of leaves      :  171
% Syntax   : Number of clauses     :  546 (  12 unt; 244 nHn; 328 RR)
%            Number of literals    : 1809 (   0 equ; 713 neg)
%            Maximal clause size   :   10 (   3 avg)
%            Maximal term depth    :    1 (   1 avg)
%            Number of predicates  :  151 ( 150 usr;   4 prp; 0-21 aty)
%            Number of functors    :    2 (   2 usr;   2 con; 0-0 aty)
%            Number of variables   : 7914 (2491 sgn)

% Comments : 
%------------------------------------------------------------------------------
cnf(i_0_635,axiom,
    ( esk2_0
    | ~ esk1_0 ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_635) ).

cnf(i_0_1703,axiom,
    esk1_0,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1703) ).

cnf(i_0_1842,axiom,
    ( esk3_0
    | ~ esk1_0 ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1842) ).

cnf(i_0_674,axiom,
    ( ~ esk4_1(X1)
    | ~ p(X1)
    | ~ esk2_0 ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_674) ).

cnf(i_0_1163,axiom,
    ( esk5_1(X1)
    | esk4_1(X1)
    | ~ esk3_0 ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1163) ).

cnf(i_0_2328,axiom,
    ( esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X1)
    | ~ esk45_1(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2328) ).

cnf(i_0_1254,axiom,
    ( esk45_1(X1)
    | ~ esk5_1(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1254) ).

cnf(i_0_2226,axiom,
    ( ~ esk21_1(X1)
    | ~ esk52_1(X1)
    | ~ esk11_1(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2226) ).

cnf(i_0_361,axiom,
    ( esk52_1(X1)
    | ~ esk5_1(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_361) ).

cnf(i_0_882,axiom,
    ( esk11_1(X1)
    | ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_882) ).

cnf(i_0_1127,axiom,
    ( esk12_1(X1)
    | esk21_1(X1)
    | esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk762_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1127) ).

cnf(i_0_2025,axiom,
    ( esk762_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2025) ).

cnf(rule_true,axiom,
    p(true),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_true) ).

cnf(i_0_590,axiom,
    ( esk58_5(X1,X2,X3,X4,X5)
    | esk57_5(X1,X2,X3,X4,X5)
    | ~ esk46_1(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_590) ).

cnf(i_0_2309,axiom,
    ( esk46_1(X1)
    | ~ esk5_1(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2309) ).

cnf(i_0_1147,axiom,
    ( ~ esk12_1(X1)
    | ~ esk22_1(X1)
    | ~ esk53_1(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1147) ).

cnf(i_0_1895,axiom,
    ( esk53_1(X1)
    | ~ esk5_1(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1895) ).

cnf(i_0_162,axiom,
    ( esk41_1(X1)
    | ~ esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_162) ).

cnf(i_0_267,axiom,
    ( esk37_1(X1)
    | ~ esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_267) ).

cnf(i_0_2216,axiom,
    ( esk22_1(X1)
    | ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2216) ).

cnf(i_0_1960,axiom,
    ( p(X1)
    | p(X4)
    | ~ esk41_1(X2)
    | ~ p(X3)
    | ~ esk746_21(X2,X4,X1,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1960) ).

cnf(i_0_884,axiom,
    ( esk746_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk57_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_884) ).

cnf(i_0_1173,axiom,
    ( p(X1)
    | p(X2)
    | p(X4)
    | ~ esk742_21(X3,X4,X1,X2,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X5)
    | ~ esk37_1(X3) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1173) ).

cnf(i_0_996,axiom,
    ( esk742_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk57_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_996) ).

cnf(i_0_2315,axiom,
    ( esk686_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk685_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk109_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2315) ).

cnf(i_0_1758,axiom,
    ( esk109_5(X1,X2,X3,X4,X5)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1758) ).

cnf(i_0_2128,axiom,
    ( esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk707_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk98_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2128) ).

cnf(i_0_497,axiom,
    ( esk98_5(X1,X2,X3,X4,X5)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_497) ).

cnf(i_0_1467,axiom,
    ( esk677_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk113_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1467) ).

cnf(i_0_957,axiom,
    ( esk113_5(X1,X2,X3,X4,X5)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_957) ).

cnf(i_0_1075,axiom,
    ( esk685_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X3) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1075) ).

cnf(i_0_749,axiom,
    ( esk685_21(X2,X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_749) ).

cnf(i_0_1364,axiom,
    ( esk677_21(X2,X3,X1,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1364) ).

cnf(i_0_2282,axiom,
    ( esk677_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X2) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2282) ).

cnf(i_0_1313,axiom,
    ( esk65_5(X1,X2,X3,X4,X5)
    | ~ esk686_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1313) ).

cnf(i_0_1555,axiom,
    ( esk741_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk26_1(X1)
    | ~ esk707_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1555) ).

cnf(i_0_1456,axiom,
    ( esk26_1(X1)
    | ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1456) ).

cnf(i_0_1956,axiom,
    ( esk65_5(X1,X2,X3,X4,X5)
    | ~ esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1956) ).

cnf(i_0_2337,axiom,
    ( p(X1)
    | p(X3)
    | p(X5)
    | ~ p(X2)
    | ~ esk685_21(X4,X3,X1,X5,X2,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2337) ).

cnf(i_0_478,axiom,
    ( ~ esk124_5(X1,X2,X3,X4,X5)
    | ~ esk65_5(X1,X2,X3,X4,X5)
    | ~ esk75_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_478) ).

cnf(i_0_835,axiom,
    ( esk124_5(X1,X2,X3,X4,X5)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_835) ).

cnf(i_0_1155,axiom,
    ( p(X3)
    | p(X2)
    | ~ esk677_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X5)
    | ~ p(X4) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1155) ).

cnf(i_0_1073,axiom,
    ( esk722_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk75_5(X1,X2,X3,X4,X5)
    | esk66_5(X1,X2,X3,X4,X5)
    | ~ esk721_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1073) ).

cnf(i_0_1809,axiom,
    ( esk721_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1809) ).

cnf(i_0_2561,axiom,
    ( ~ esk741_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk37_1(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2561) ).

cnf(i_0_432,axiom,
    ( esk76_5(X1,X2,X3,X4,X5)
    | ~ esk686_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_432) ).

cnf(i_0_945,axiom,
    ( esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | esk128_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk117_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_945) ).

cnf(i_0_1871,axiom,
    ( esk117_5(X1,X2,X3,X4,X5)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1871) ).

cnf(i_0_2311,axiom,
    ( esk76_5(X1,X2,X3,X4,X5)
    | ~ esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2311) ).

cnf(i_0_481,axiom,
    ( p(X7)
    | ~ esk668_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X8)
    | ~ esk95_5(X1,X2,X3,X4,X5)
    | ~ p(X9)
    | ~ p(X6) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_481) ).

cnf(i_0_1573,axiom,
    ( esk668_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk128_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1573) ).

cnf(i_0_27,axiom,
    ( ~ esk76_5(X1,X2,X3,X4,X5)
    | ~ esk125_5(X1,X2,X3,X4,X5)
    | ~ esk66_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_27) ).

cnf(i_0_2384,axiom,
    ( esk125_5(X1,X2,X3,X4,X5)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2384) ).

cnf(i_0_1499,axiom,
    ( esk95_5(X1,X2,X3,X4,X5)
    | ~ esk722_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1499) ).

cnf(i_0_2053,axiom,
    ( p(X7)
    | p(X8)
    | ~ esk664_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X6)
    | ~ p(X9)
    | ~ esk91_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2053) ).

cnf(i_0_1177,axiom,
    ( esk664_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk128_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1177) ).

cnf(i_0_756,axiom,
    ( esk91_5(X1,X2,X3,X4,X5)
    | ~ esk722_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_756) ).

cnf(i_0_43,axiom,
    ( esk605_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk604_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk181_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_43) ).

cnf(i_0_2429,axiom,
    ( esk181_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2429) ).

cnf(i_0_816,axiom,
    ( esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk596_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk185_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_816) ).

cnf(i_0_788,axiom,
    ( esk185_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_788) ).

cnf(i_0_1630,axiom,
    ( esk604_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X7) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1630) ).

cnf(i_0_538,axiom,
    ( esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk628_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk169_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_538) ).

cnf(i_0_2423,axiom,
    ( esk169_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2423) ).

cnf(i_0_2554,axiom,
    ( esk596_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X7) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2554) ).

cnf(i_0_1839,axiom,
    ( esk137_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk605_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1839) ).

cnf(i_0_2495,axiom,
    ( esk79_5(X1,X2,X3,X4,X5)
    | ~ esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2495) ).

cnf(i_0_1023,axiom,
    ( esk137_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1023) ).

cnf(i_0_1121,axiom,
    ( p(X8)
    | p(X7)
    | ~ esk604_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X6)
    | ~ p(X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1121) ).

cnf(i_0_1514,axiom,
    ( esk662_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk628_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk79_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1514) ).

cnf(i_0_1132,axiom,
    ( ~ esk137_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk196_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1132) ).

cnf(i_0_7,axiom,
    ( esk196_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_7) ).

cnf(i_0_2245,axiom,
    ( p(X4)
    | ~ p(X1)
    | ~ p(X2)
    | ~ p(X3)
    | ~ esk596_21(X5,X6,X7,X8,X9,X1,X4,X3,X2,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2245) ).

cnf(i_0_2351,axiom,
    ( esk138_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk640_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2351) ).

cnf(i_0_1544,axiom,
    ( esk640_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1544) ).

cnf(i_0_2170,axiom,
    ( ~ esk662_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk95_5(X1,X2,X3,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2170) ).

cnf(i_0_402,axiom,
    ( esk148_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk605_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_402) ).

cnf(i_0_2275,axiom,
    ( esk199_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk188_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2275) ).

cnf(i_0_87,axiom,
    ( esk188_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_87) ).

cnf(i_0_905,axiom,
    ( esk148_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_905) ).

cnf(i_0_1812,axiom,
    ( p(X2)
    | p(X13)
    | ~ p(X1)
    | ~ esk163_9(X3,X4,X5,X6,X7,X8,X9,X10,X11)
    | ~ p(X12)
    | ~ esk586_21(X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X12,X2,X1,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1812) ).

cnf(i_0_1422,axiom,
    ( esk586_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk199_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1422) ).

cnf(i_0_668,axiom,
    ( ~ esk197_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk148_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk138_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_668) ).

cnf(i_0_1057,axiom,
    ( esk197_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1057) ).

cnf(i_0_2369,axiom,
    ( esk163_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2369) ).

cnf(i_0_2486,axiom,
    ( p(X11)
    | ~ p(X1)
    | ~ esk590_21(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X12)
    | ~ p(X13)
    | ~ esk167_9(X2,X3,X4,X5,X6,X7,X8,X9,X10) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2486) ).

cnf(i_0_2487,axiom,
    ( esk590_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk199_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2487) ).

cnf(i_0_2329,axiom,
    ( esk167_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2329) ).

cnf(i_0_1941,axiom,
    ( esk524_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk523_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk253_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1941) ).

cnf(i_0_895,axiom,
    ( esk253_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_895) ).

cnf(i_0_476,axiom,
    ( esk515_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk257_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_476) ).

cnf(i_0_1118,axiom,
    ( esk257_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1118) ).

cnf(i_0_1666,axiom,
    ( esk523_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X10) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1666) ).

cnf(i_0_1945,axiom,
    ( esk549_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk240_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1945) ).

cnf(i_0_1098,axiom,
    ( esk240_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1098) ).

cnf(i_0_2442,axiom,
    ( esk515_21(X2,X3,X4,X5,X6,X7,X8,X9,X10,X1,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2442) ).

cnf(i_0_1383,axiom,
    ( esk209_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk524_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1383) ).

cnf(i_0_2297,axiom,
    ( esk150_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2297) ).

cnf(i_0_553,axiom,
    ( esk209_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_553) ).

cnf(i_0_2421,axiom,
    ( p(X2)
    | p(X13)
    | ~ p(X1)
    | ~ p(X3)
    | ~ esk523_21(X4,X5,X6,X7,X8,X9,X10,X11,X12,X2,X1,X13,X3,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2421) ).

cnf(i_0_2417,axiom,
    ( esk583_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk150_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk549_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2417) ).

cnf(i_0_1059,axiom,
    ( ~ esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk209_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk268_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1059) ).

cnf(i_0_2353,axiom,
    ( esk268_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2353) ).

cnf(i_0_921,axiom,
    ( p(X10)
    | ~ esk515_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X12)
    | ~ p(X11)
    | ~ p(X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_921) ).

cnf(i_0_260,axiom,
    ( esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk210_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk560_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_260) ).

cnf(i_0_2491,axiom,
    ( esk560_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2491) ).

cnf(i_0_81,axiom,
    ( ~ esk583_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk163_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_81) ).

cnf(i_0_853,axiom,
    ( esk220_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk524_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_853) ).

cnf(i_0_1342,axiom,
    ( esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk259_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1342) ).

cnf(i_0_2006,axiom,
    ( esk259_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2006) ).

cnf(i_0_22,axiom,
    ( esk220_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_22) ).

cnf(i_0_2011,axiom,
    ( p(X16)
    | ~ p(X1)
    | ~ p(X2)
    | ~ esk508_21(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X1,X2,X16,X17,X18,X19,X20,X21)
    | ~ p(X17)
    | ~ esk235_13(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2011) ).

cnf(i_0_21,axiom,
    ( esk508_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_21) ).

cnf(i_0_2272,axiom,
    ( ~ esk269_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk210_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk220_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2272) ).

cnf(i_0_1701,axiom,
    ( esk269_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1701) ).

cnf(i_0_1052,axiom,
    ( esk235_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1052) ).

cnf(i_0_1780,axiom,
    ( ~ p(X1)
    | ~ p(X2)
    | ~ esk512_21(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X2,X16,X1,X17,X18,X19,X20,X21)
    | ~ p(X17)
    | ~ esk239_13(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
    | ~ p(X16) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1780) ).

cnf(i_0_2511,axiom,
    ( esk512_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2511) ).

cnf(i_0_333,axiom,
    ( esk239_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_333) ).

cnf(i_0_289,axiom,
    ( esk443_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk442_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk324_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_289) ).

cnf(i_0_2126,axiom,
    ( esk324_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2126) ).

cnf(i_0_347,axiom,
    ( esk434_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk435_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk328_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_347) ).

cnf(i_0_327,axiom,
    ( esk328_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_327) ).

cnf(i_0_1900,axiom,
    ( esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk470_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk310_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1900) ).

cnf(i_0_2219,axiom,
    ( esk310_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2219) ).

cnf(i_0_2388,axiom,
    ( esk281_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk443_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2388) ).

cnf(i_0_117,axiom,
    ( esk221_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_117) ).

cnf(i_0_676,axiom,
    ( esk281_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk435_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_676) ).

cnf(i_0_304,axiom,
    ( p(X2)
    | ~ p(X1)
    | ~ p(X3)
    | ~ esk442_21(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X3,X2,X1,X18,X19,X20,X21)
    | ~ p(X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_304) ).

cnf(i_0_1736,axiom,
    ( esk504_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk221_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk470_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1736) ).

cnf(i_0_2503,axiom,
    ( ~ esk339_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk291_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk281_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2503) ).

cnf(i_0_2287,axiom,
    ( esk339_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2287) ).

cnf(i_0_1011,axiom,
    ( ~ p(X1)
    | ~ p(X2)
    | ~ p(X3)
    | ~ esk434_21(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X2,X3,X1,X18,X19,X20,X21)
    | ~ p(X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1011) ).

cnf(i_0_1677,axiom,
    ( esk280_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk291_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk472_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1677) ).

cnf(i_0_2180,axiom,
    ( esk472_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2180) ).

cnf(i_0_345,axiom,
    ( ~ esk504_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk235_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_345) ).

cnf(i_0_269,axiom,
    ( esk279_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk290_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk473_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_269) ).

cnf(i_0_1240,axiom,
    ( esk473_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1240) ).

cnf(i_0_1811,axiom,
    ( ~ esk290_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk338_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk280_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1811) ).

cnf(i_0_1766,axiom,
    ( esk338_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1766) ).

cnf(i_0_1181,axiom,
    ( ~ esk289_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk337_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk279_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1181) ).

cnf(i_0_1445,axiom,
    ( esk337_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1445) ).

cnf(i_0_1097,axiom,
    ( esk574_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk557_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1097) ).

cnf(i_0_2531,axiom,
    ( esk557_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2531) ).

cnf(i_0_170,axiom,
    ( esk458_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk284_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk289_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk316_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_170) ).

cnf(i_0_2360,axiom,
    ( esk316_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2360) ).

cnf(i_0_1228,axiom,
    ( esk576_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk574_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1228) ).

cnf(i_0_1319,axiom,
    ( esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | esk653_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk636_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1319) ).

cnf(i_0_149,axiom,
    ( esk636_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_149) ).

cnf(i_0_163,axiom,
    ( esk459_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk227_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk458_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_163) ).

cnf(i_0_1603,axiom,
    ( esk203_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk227_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk576_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1603) ).

cnf(i_0_138,axiom,
    ( esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk213_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk537_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk246_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_138) ).

cnf(i_0_346,axiom,
    ( esk246_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_346) ).

cnf(i_0_1464,axiom,
    ( esk655_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk653_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1464) ).

cnf(i_0_2339,axiom,
    ( ~ esk274_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk284_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk332_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2339) ).

cnf(i_0_455,axiom,
    ( esk332_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_455) ).

cnf(i_0_1920,axiom,
    ( ~ esk235_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk459_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1920) ).

cnf(i_0_1305,axiom,
    ( esk274_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1305) ).

cnf(i_0_601,axiom,
    ( esk538_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk156_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk537_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_601) ).

cnf(i_0_1522,axiom,
    ( esk132_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | esk156_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk655_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1522) ).

cnf(i_0_417,axiom,
    ( ~ esk203_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk213_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk262_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_417) ).

cnf(i_0_2187,axiom,
    ( esk262_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2187) ).

cnf(i_0_1318,axiom,
    ( ~ esk538_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk163_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1318) ).

cnf(i_0_1724,axiom,
    ( esk142_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1724) ).

cnf(i_0_684,axiom,
    ( esk208_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk552_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_684) ).

cnf(i_0_212,axiom,
    ( esk552_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_212) ).

cnf(i_0_2281,axiom,
    ( ~ esk191_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk132_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk142_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_2281) ).

cnf(i_0_3,axiom,
    ( esk191_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_3) ).

cnf(i_0_221,axiom,
    ( ~ esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk267_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk208_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_221) ).

cnf(i_0_1575,axiom,
    ( esk267_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_1575) ).

cnf(rule_false,axiom,
    ~ p(false),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_false) ).

cnf(c_0_2733,axiom,
    ( esk2_0
    | ~ esk1_0 ),
    i_0_635 ).

cnf(c_0_2734,axiom,
    esk1_0,
    i_0_1703 ).

cnf(c_0_2735,axiom,
    ( esk3_0
    | ~ esk1_0 ),
    i_0_1842 ).

cnf(c_0_2736,axiom,
    ( ~ esk4_1(X1)
    | ~ p(X1)
    | ~ esk2_0 ),
    i_0_674 ).

cnf(c_0_2737,plain,
    esk2_0,
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2733,c_0_2734])]) ).

cnf(c_0_2738,axiom,
    ( esk5_1(X1)
    | esk4_1(X1)
    | ~ esk3_0 ),
    i_0_1163 ).

cnf(c_0_2739,plain,
    esk3_0,
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2735,c_0_2734])]) ).

cnf(c_0_2740,plain,
    ( ~ esk4_1(X1)
    | ~ p(X1) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2736,c_0_2737])]) ).

cnf(c_0_2741,plain,
    ( esk4_1(X1)
    | esk5_1(X1) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2738,c_0_2739])]) ).

cnf(c_0_2742,axiom,
    ( esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X1)
    | ~ esk45_1(X1) ),
    i_0_2328 ).

cnf(c_0_2743,axiom,
    ( esk45_1(X1)
    | ~ esk5_1(X1) ),
    i_0_1254 ).

cnf(c_0_2744,plain,
    ( esk5_1(X1)
    | ~ p(X1) ),
    inference(spm,[status(thm)],[c_0_2740,c_0_2741]) ).

cnf(c_0_2745,axiom,
    ( ~ esk21_1(X1)
    | ~ esk52_1(X1)
    | ~ esk11_1(X1) ),
    i_0_2226 ).

cnf(c_0_2746,axiom,
    ( esk52_1(X1)
    | ~ esk5_1(X1) ),
    i_0_361 ).

cnf(c_0_2747,axiom,
    ( esk11_1(X1)
    | ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_882 ).

cnf(c_0_2748,plain,
    ( esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X1) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2742,c_0_2743]),c_0_2744]) ).

cnf(c_0_2749,axiom,
    ( esk12_1(X1)
    | esk21_1(X1)
    | esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk762_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1127 ).

cnf(c_0_2750,axiom,
    ( esk762_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2025 ).

cnf(c_0_2751,plain,
    ( ~ esk5_1(X1)
    | ~ esk11_1(X1)
    | ~ esk21_1(X1) ),
    inference(spm,[status(thm)],[c_0_2745,c_0_2746]) ).

cnf(c_0_2752,plain,
    ( esk11_1(X1)
    | ~ p(X1) ),
    inference(spm,[status(thm)],[c_0_2747,c_0_2748]) ).

cnf(c_0_2753,plain,
    ( esk12_1(X1)
    | esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk21_1(X1)
    | ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    inference(spm,[status(thm)],[c_0_2749,c_0_2750]) ).

cnf(c_0_2754,plain,
    ( ~ esk21_1(X1)
    | ~ p(X1) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2751,c_0_2752]),c_0_2744]) ).

cnf(c_0_2755,plain,
    ( esk12_1(X1)
    | esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X1) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2753,c_0_2748]),c_0_2754]) ).

cnf(c_0_2756,axiom,
    p(true),
    rule_true ).

cnf(c_0_2757,axiom,
    ( esk58_5(X1,X2,X3,X4,X5)
    | esk57_5(X1,X2,X3,X4,X5)
    | ~ esk46_1(X1) ),
    i_0_590 ).

cnf(c_0_2758,axiom,
    ( esk46_1(X1)
    | ~ esk5_1(X1) ),
    i_0_2309 ).

cnf(c_0_2759,axiom,
    ( ~ esk12_1(X1)
    | ~ esk22_1(X1)
    | ~ esk53_1(X1) ),
    i_0_1147 ).

cnf(c_0_2760,axiom,
    ( esk53_1(X1)
    | ~ esk5_1(X1) ),
    i_0_1895 ).

cnf(c_0_2761,axiom,
    ( esk41_1(X1)
    | ~ esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_162 ).

cnf(c_0_2762,plain,
    ( esk12_1(true)
    | esk765_21(true,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(spm,[status(thm)],[c_0_2755,c_0_2756]) ).

cnf(c_0_2763,axiom,
    ( esk37_1(X1)
    | ~ esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_267 ).

cnf(c_0_2764,plain,
    ( esk57_5(X1,X2,X3,X4,X5)
    | esk58_5(X1,X2,X3,X4,X5)
    | ~ esk5_1(X1) ),
    inference(spm,[status(thm)],[c_0_2757,c_0_2758]) ).

cnf(c_0_2765,plain,
    ( ~ esk22_1(X1)
    | ~ esk12_1(X1)
    | ~ esk5_1(X1) ),
    inference(spm,[status(thm)],[c_0_2759,c_0_2760]) ).

cnf(c_0_2766,plain,
    ( esk12_1(true)
    | esk41_1(true) ),
    inference(spm,[status(thm)],[c_0_2761,c_0_2762]) ).

cnf(c_0_2767,axiom,
    ( esk22_1(X1)
    | ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2216 ).

cnf(c_0_2768,plain,
    ( esk12_1(true)
    | esk37_1(true) ),
    inference(spm,[status(thm)],[c_0_2763,c_0_2762]) ).

cnf(c_0_2769,axiom,
    ( p(X1)
    | p(X4)
    | ~ esk41_1(X2)
    | ~ p(X3)
    | ~ esk746_21(X2,X4,X1,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X5) ),
    i_0_1960 ).

cnf(c_0_2770,axiom,
    ( esk746_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk57_5(X1,X2,X3,X4,X5) ),
    i_0_884 ).

cnf(c_0_2771,plain,
    ( esk57_5(X1,X2,X3,X4,X5)
    | esk58_5(X1,X2,X3,X4,X5)
    | ~ p(X1) ),
    inference(spm,[status(thm)],[c_0_2764,c_0_2744]) ).

cnf(c_0_2772,plain,
    ( esk41_1(true)
    | ~ esk22_1(true)
    | ~ esk5_1(true) ),
    inference(spm,[status(thm)],[c_0_2765,c_0_2766]) ).

cnf(c_0_2773,plain,
    ( esk22_1(X1)
    | ~ p(X1) ),
    inference(spm,[status(thm)],[c_0_2767,c_0_2748]) ).

cnf(c_0_2774,axiom,
    ( p(X1)
    | p(X2)
    | p(X4)
    | ~ esk742_21(X3,X4,X1,X2,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X5)
    | ~ esk37_1(X3) ),
    i_0_1173 ).

cnf(c_0_2775,axiom,
    ( esk742_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk57_5(X1,X2,X3,X4,X5) ),
    i_0_996 ).

cnf(c_0_2776,plain,
    ( esk37_1(true)
    | ~ esk22_1(true)
    | ~ esk5_1(true) ),
    inference(spm,[status(thm)],[c_0_2765,c_0_2768]) ).

cnf(c_0_2777,plain,
    ( p(X1)
    | p(X2)
    | ~ esk57_5(X3,X2,X1,X4,X5)
    | ~ esk41_1(X3)
    | ~ p(X5)
    | ~ p(X4) ),
    inference(spm,[status(thm)],[c_0_2769,c_0_2770]) ).

cnf(c_0_2778,plain,
    ( esk57_5(true,X1,X2,X3,X4)
    | esk58_5(true,X1,X2,X3,X4) ),
    inference(spm,[status(thm)],[c_0_2771,c_0_2756]) ).

cnf(c_0_2779,plain,
    ( esk41_1(true)
    | ~ esk5_1(true) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2772,c_0_2773]),c_0_2756])]) ).

cnf(c_0_2780,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | ~ esk57_5(X4,X3,X1,X2,X5)
    | ~ p(X5)
    | ~ esk37_1(X4) ),
    inference(spm,[status(thm)],[c_0_2774,c_0_2775]) ).

cnf(c_0_2781,plain,
    ( esk37_1(true)
    | ~ esk5_1(true) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2776,c_0_2773]),c_0_2756])]) ).

cnf(c_0_2782,plain,
    ( esk58_5(true,X1,X2,X3,X4)
    | p(X1)
    | p(X2)
    | ~ esk41_1(true)
    | ~ p(X4)
    | ~ p(X3) ),
    inference(spm,[status(thm)],[c_0_2777,c_0_2778]) ).

cnf(c_0_2783,plain,
    esk41_1(true),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2779,c_0_2744]),c_0_2756])]) ).

cnf(c_0_2784,plain,
    ( esk58_5(true,X1,X2,X3,X4)
    | p(X1)
    | p(X3)
    | p(X2)
    | ~ p(X4)
    | ~ esk37_1(true) ),
    inference(spm,[status(thm)],[c_0_2780,c_0_2778]) ).

cnf(c_0_2785,plain,
    esk37_1(true),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2781,c_0_2744]),c_0_2756])]) ).

cnf(c_0_2786,plain,
    ( esk58_5(true,X1,X2,X3,X4)
    | p(X2)
    | p(X1)
    | ~ p(X4)
    | ~ p(X3) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2782,c_0_2783])]) ).

cnf(c_0_2787,axiom,
    ( esk686_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk685_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk109_5(X1,X2,X3,X4,X5) ),
    i_0_2315 ).

cnf(c_0_2788,axiom,
    ( esk109_5(X1,X2,X3,X4,X5)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    i_0_1758 ).

cnf(c_0_2789,plain,
    ( esk58_5(true,X1,X2,X3,X4)
    | p(X2)
    | p(X1)
    | ~ p(X4) ),
    inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2784,c_0_2785])]),c_0_2786]) ).

cnf(c_0_2790,axiom,
    ( esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk707_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk98_5(X1,X2,X3,X4,X5) ),
    i_0_2128 ).

cnf(c_0_2791,axiom,
    ( esk98_5(X1,X2,X3,X4,X5)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    i_0_497 ).

cnf(c_0_2792,axiom,
    ( esk677_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk113_5(X1,X2,X3,X4,X5) ),
    i_0_1467 ).

cnf(c_0_2793,axiom,
    ( esk113_5(X1,X2,X3,X4,X5)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    i_0_957 ).

cnf(c_0_2794,plain,
    ( esk685_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk686_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    inference(spm,[status(thm)],[c_0_2787,c_0_2788]) ).

cnf(c_0_2795,plain,
    ( esk58_5(true,X1,X2,X3,true)
    | p(X1)
    | p(X2) ),
    inference(spm,[status(thm)],[c_0_2789,c_0_2756]) ).

cnf(c_0_2796,axiom,
    ( esk685_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X3) ),
    i_0_1075 ).

cnf(c_0_2797,axiom,
    ( esk685_21(X2,X1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X1) ),
    i_0_749 ).

cnf(c_0_2798,plain,
    ( esk707_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    inference(spm,[status(thm)],[c_0_2790,c_0_2791]) ).

cnf(c_0_2799,plain,
    ( esk677_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    inference(spm,[status(thm)],[c_0_2792,c_0_2793]) ).

cnf(c_0_2800,axiom,
    ( esk677_21(X2,X3,X1,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X1) ),
    i_0_1364 ).

cnf(c_0_2801,axiom,
    ( esk677_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X2) ),
    i_0_2282 ).

cnf(c_0_2802,axiom,
    ( esk65_5(X1,X2,X3,X4,X5)
    | ~ esk686_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1313 ).

cnf(c_0_2803,plain,
    ( esk685_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
    | esk686_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2794,c_0_2795]),c_0_2796]),c_0_2797]) ).

cnf(c_0_2804,axiom,
    ( esk741_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk26_1(X1)
    | ~ esk707_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1555 ).

cnf(c_0_2805,plain,
    ( esk707_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
    | esk708_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
    | p(X2)
    | p(X1) ),
    inference(spm,[status(thm)],[c_0_2798,c_0_2795]) ).

cnf(c_0_2806,axiom,
    ( esk26_1(X1)
    | ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1456 ).

cnf(c_0_2807,axiom,
    ( esk65_5(X1,X2,X3,X4,X5)
    | ~ esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1956 ).

cnf(c_0_2808,plain,
    ( esk677_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
    | esk678_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2799,c_0_2795]),c_0_2800]),c_0_2801]) ).

cnf(c_0_2809,axiom,
    ( p(X1)
    | p(X3)
    | p(X5)
    | ~ p(X2)
    | ~ esk685_21(X4,X3,X1,X5,X2,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2337 ).

cnf(c_0_2810,plain,
    ( esk685_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
    | esk65_5(true,X1,X2,X3,true) ),
    inference(spm,[status(thm)],[c_0_2802,c_0_2803]) ).

cnf(c_0_2811,plain,
    ( esk741_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
    | esk708_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
    | p(X1)
    | p(X2)
    | ~ esk26_1(true) ),
    inference(spm,[status(thm)],[c_0_2804,c_0_2805]) ).

cnf(c_0_2812,plain,
    ( esk26_1(X1)
    | ~ p(X1) ),
    inference(spm,[status(thm)],[c_0_2806,c_0_2748]) ).

cnf(c_0_2813,axiom,
    ( ~ esk124_5(X1,X2,X3,X4,X5)
    | ~ esk65_5(X1,X2,X3,X4,X5)
    | ~ esk75_5(X1,X2,X3,X4,X5) ),
    i_0_478 ).

cnf(c_0_2814,axiom,
    ( esk124_5(X1,X2,X3,X4,X5)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    i_0_835 ).

cnf(c_0_2815,axiom,
    ( p(X3)
    | p(X2)
    | ~ esk677_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X5)
    | ~ p(X4) ),
    i_0_1155 ).

cnf(c_0_2816,plain,
    ( esk677_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
    | esk65_5(true,X1,X2,X3,true) ),
    inference(spm,[status(thm)],[c_0_2807,c_0_2808]) ).

cnf(c_0_2817,plain,
    ( esk65_5(true,X1,X2,X3,true)
    | p(X2)
    | p(X1)
    | p(X3) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2809,c_0_2810]),c_0_2756])]) ).

cnf(c_0_2818,axiom,
    ( esk722_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk75_5(X1,X2,X3,X4,X5)
    | esk66_5(X1,X2,X3,X4,X5)
    | ~ esk721_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1073 ).

cnf(c_0_2819,axiom,
    ( esk721_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1809 ).

cnf(c_0_2820,axiom,
    ( ~ esk741_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk37_1(X1) ),
    i_0_2561 ).

cnf(c_0_2821,plain,
    ( esk741_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
    | esk708_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
    | p(X2)
    | p(X1) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2811,c_0_2812]),c_0_2756])]) ).

cnf(c_0_2822,plain,
    ( ~ esk58_5(X1,X2,X3,X4,X5)
    | ~ esk65_5(X1,X2,X3,X4,X5)
    | ~ esk75_5(X1,X2,X3,X4,X5) ),
    inference(spm,[status(thm)],[c_0_2813,c_0_2814]) ).

cnf(c_0_2823,plain,
    ( esk65_5(true,X1,X2,X3,true)
    | p(X1)
    | p(X2) ),
    inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2815,c_0_2816]),c_0_2756])]),c_0_2817]) ).

cnf(c_0_2824,axiom,
    ( esk76_5(X1,X2,X3,X4,X5)
    | ~ esk686_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_432 ).

cnf(c_0_2825,axiom,
    ( esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | esk128_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk117_5(X1,X2,X3,X4,X5) ),
    i_0_945 ).

cnf(c_0_2826,axiom,
    ( esk117_5(X1,X2,X3,X4,X5)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    i_0_1871 ).

cnf(c_0_2827,plain,
    ( esk75_5(X1,X2,X3,X4,X5)
    | esk66_5(X1,X2,X3,X4,X5)
    | esk722_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    inference(spm,[status(thm)],[c_0_2818,c_0_2819]) ).

cnf(c_0_2828,plain,
    ( esk708_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
    | p(X1)
    | p(X2) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2820,c_0_2821]),c_0_2785])]) ).

cnf(c_0_2829,plain,
    ( p(X1)
    | p(X2)
    | ~ esk75_5(true,X2,X1,X3,true) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2822,c_0_2823]),c_0_2795]) ).

cnf(c_0_2830,axiom,
    ( esk76_5(X1,X2,X3,X4,X5)
    | ~ esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2311 ).

cnf(c_0_2831,plain,
    ( esk685_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
    | esk76_5(true,X1,X2,X3,true) ),
    inference(spm,[status(thm)],[c_0_2824,c_0_2803]) ).

cnf(c_0_2832,axiom,
    ( p(X7)
    | ~ esk668_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X8)
    | ~ esk95_5(X1,X2,X3,X4,X5)
    | ~ p(X9)
    | ~ p(X6) ),
    i_0_481 ).

cnf(c_0_2833,axiom,
    ( esk668_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk128_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_1573 ).

cnf(c_0_2834,plain,
    ( esk128_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    inference(spm,[status(thm)],[c_0_2825,c_0_2826]) ).

cnf(c_0_2835,axiom,
    ( ~ esk76_5(X1,X2,X3,X4,X5)
    | ~ esk125_5(X1,X2,X3,X4,X5)
    | ~ esk66_5(X1,X2,X3,X4,X5) ),
    i_0_27 ).

cnf(c_0_2836,axiom,
    ( esk125_5(X1,X2,X3,X4,X5)
    | ~ esk58_5(X1,X2,X3,X4,X5) ),
    i_0_2384 ).

cnf(c_0_2837,axiom,
    ( esk95_5(X1,X2,X3,X4,X5)
    | ~ esk722_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1499 ).

cnf(c_0_2838,plain,
    ( esk66_5(true,X1,X2,X3,true)
    | esk722_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
    | p(X2)
    | p(X1) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2827,c_0_2828]),c_0_2829]) ).

cnf(c_0_2839,plain,
    ( esk677_21(true,X1,X2,X3,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
    | esk76_5(true,X1,X2,X3,true) ),
    inference(spm,[status(thm)],[c_0_2830,c_0_2808]) ).

cnf(c_0_2840,plain,
    ( esk76_5(true,X1,X2,X3,true)
    | p(X2)
    | p(X1)
    | p(X3) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2809,c_0_2831]),c_0_2756])]) ).

cnf(c_0_2841,axiom,
    ( p(X7)
    | p(X8)
    | ~ esk664_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X6)
    | ~ p(X9)
    | ~ esk91_5(X1,X2,X3,X4,X5) ),
    i_0_2053 ).

cnf(c_0_2842,axiom,
    ( esk664_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk128_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_1177 ).

cnf(c_0_2843,axiom,
    ( esk91_5(X1,X2,X3,X4,X5)
    | ~ esk722_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_756 ).

cnf(c_0_2844,plain,
    ( p(X1)
    | ~ esk128_9(X2,X3,X4,X5,X6,X7,X1,X8,X9)
    | ~ esk95_5(X2,X3,X4,X5,X6)
    | ~ p(X9)
    | ~ p(X8)
    | ~ p(X7) ),
    inference(spm,[status(thm)],[c_0_2832,c_0_2833]) ).

cnf(c_0_2845,plain,
    ( esk128_9(true,X1,X2,X3,true,X4,X5,X6,X7)
    | p(X2)
    | p(X1)
    | esk129_9(true,X1,X2,X3,true,X4,X5,X6,X7) ),
    inference(spm,[status(thm)],[c_0_2834,c_0_2795]) ).

cnf(c_0_2846,plain,
    ( ~ esk58_5(X1,X2,X3,X4,X5)
    | ~ esk66_5(X1,X2,X3,X4,X5)
    | ~ esk76_5(X1,X2,X3,X4,X5) ),
    inference(spm,[status(thm)],[c_0_2835,c_0_2836]) ).

cnf(c_0_2847,plain,
    ( esk66_5(true,X1,X2,X3,true)
    | esk95_5(true,X1,X2,X3,true)
    | p(X1)
    | p(X2) ),
    inference(spm,[status(thm)],[c_0_2837,c_0_2838]) ).

cnf(c_0_2848,plain,
    ( esk76_5(true,X1,X2,X3,true)
    | p(X1)
    | p(X2) ),
    inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2815,c_0_2839]),c_0_2756])]),c_0_2840]) ).

cnf(c_0_2849,plain,
    ( p(X1)
    | p(X2)
    | ~ esk128_9(X3,X4,X5,X6,X7,X8,X1,X2,X9)
    | ~ esk91_5(X3,X4,X5,X6,X7)
    | ~ p(X9)
    | ~ p(X8) ),
    inference(spm,[status(thm)],[c_0_2841,c_0_2842]) ).

cnf(c_0_2850,plain,
    ( esk66_5(true,X1,X2,X3,true)
    | esk91_5(true,X1,X2,X3,true)
    | p(X1)
    | p(X2) ),
    inference(spm,[status(thm)],[c_0_2843,c_0_2838]) ).

cnf(c_0_2851,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | esk129_9(true,X1,X2,X4,true,X5,X3,X6,X7)
    | ~ esk95_5(true,X1,X2,X4,true)
    | ~ p(X7)
    | ~ p(X6)
    | ~ p(X5) ),
    inference(spm,[status(thm)],[c_0_2844,c_0_2845]) ).

cnf(c_0_2852,plain,
    ( esk95_5(true,X1,X2,X3,true)
    | p(X2)
    | p(X1) ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2846,c_0_2847]),c_0_2848]),c_0_2795]) ).

cnf(c_0_2853,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | p(X4)
    | esk129_9(true,X1,X2,X5,true,X6,X4,X3,X7)
    | ~ esk91_5(true,X1,X2,X5,true)
    | ~ p(X7)
    | ~ p(X6) ),
    inference(spm,[status(thm)],[c_0_2849,c_0_2845]) ).

cnf(c_0_2854,plain,
    ( esk91_5(true,X1,X2,X3,true)
    | p(X2)
    | p(X1) ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2846,c_0_2850]),c_0_2848]),c_0_2795]) ).

cnf(c_0_2855,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | esk129_9(true,X3,X2,X4,true,X5,X1,X6,X7)
    | ~ p(X7)
    | ~ p(X6)
    | ~ p(X5) ),
    inference(spm,[status(thm)],[c_0_2851,c_0_2852]) ).

cnf(c_0_2856,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | esk129_9(true,X3,X2,X4,true,X5,X1,X6,X7)
    | ~ p(X7)
    | ~ p(X5) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2853,c_0_2854]),c_0_2855]) ).

cnf(c_0_2857,axiom,
    ( esk605_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk604_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk181_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_43 ).

cnf(c_0_2858,axiom,
    ( esk181_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_2429 ).

cnf(c_0_2859,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | esk129_9(true,X1,X2,X4,true,X5,X3,X6,true)
    | ~ p(X5) ),
    inference(spm,[status(thm)],[c_0_2856,c_0_2756]) ).

cnf(c_0_2860,axiom,
    ( esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk596_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk185_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_816 ).

cnf(c_0_2861,axiom,
    ( esk185_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_788 ).

cnf(c_0_2862,plain,
    ( esk604_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk605_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    inference(spm,[status(thm)],[c_0_2857,c_0_2858]) ).

cnf(c_0_2863,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | esk129_9(true,X3,X2,X4,true,true,X1,X5,true) ),
    inference(spm,[status(thm)],[c_0_2859,c_0_2756]) ).

cnf(c_0_2864,axiom,
    ( esk604_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X7) ),
    i_0_1630 ).

cnf(c_0_2865,axiom,
    ( esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk628_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk169_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_538 ).

cnf(c_0_2866,axiom,
    ( esk169_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_2423 ).

cnf(c_0_2867,plain,
    ( esk596_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    inference(spm,[status(thm)],[c_0_2860,c_0_2861]) ).

cnf(c_0_2868,axiom,
    ( esk596_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X7) ),
    i_0_2554 ).

cnf(c_0_2869,axiom,
    ( esk137_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk605_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1839 ).

cnf(c_0_2870,plain,
    ( esk604_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk605_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | p(X1)
    | p(X2) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2862,c_0_2863]),c_0_2864]) ).

cnf(c_0_2871,plain,
    ( esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk628_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    inference(spm,[status(thm)],[c_0_2865,c_0_2866]) ).

cnf(c_0_2872,axiom,
    ( esk79_5(X1,X2,X3,X4,X5)
    | ~ esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2495 ).

cnf(c_0_2873,axiom,
    ( esk137_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1023 ).

cnf(c_0_2874,plain,
    ( esk596_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk597_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | p(X1)
    | p(X2) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2867,c_0_2863]),c_0_2868]) ).

cnf(c_0_2875,axiom,
    ( p(X8)
    | p(X7)
    | ~ esk604_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X6)
    | ~ p(X9) ),
    i_0_1121 ).

cnf(c_0_2876,plain,
    ( esk137_9(true,X1,X2,X3,true,true,X4,X5,true)
    | esk604_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | p(X2)
    | p(X1) ),
    inference(spm,[status(thm)],[c_0_2869,c_0_2870]) ).

cnf(c_0_2877,axiom,
    ( esk662_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk628_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk79_5(X1,X2,X3,X4,X5) ),
    i_0_1514 ).

cnf(c_0_2878,plain,
    ( esk629_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk628_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_2871,c_0_2863]) ).

cnf(c_0_2879,plain,
    ( esk79_5(true,X1,X2,X3,true)
    | p(X2)
    | p(X1) ),
    inference(spm,[status(thm)],[c_0_2872,c_0_2828]) ).

cnf(c_0_2880,axiom,
    ( ~ esk137_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk196_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_1132 ).

cnf(c_0_2881,axiom,
    ( esk196_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_7 ).

cnf(c_0_2882,axiom,
    ( p(X4)
    | ~ p(X1)
    | ~ p(X2)
    | ~ p(X3)
    | ~ esk596_21(X5,X6,X7,X8,X9,X1,X4,X3,X2,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2245 ).

cnf(c_0_2883,plain,
    ( esk596_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk137_9(true,X1,X2,X3,true,true,X4,X5,true)
    | p(X2)
    | p(X1) ),
    inference(spm,[status(thm)],[c_0_2873,c_0_2874]) ).

cnf(c_0_2884,plain,
    ( esk137_9(true,X1,X2,X3,true,true,X4,X5,true)
    | p(X1)
    | p(X2)
    | p(X4)
    | p(X5) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2875,c_0_2876]),c_0_2756])]) ).

cnf(c_0_2885,axiom,
    ( esk138_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk640_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2351 ).

cnf(c_0_2886,axiom,
    ( esk640_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1544 ).

cnf(c_0_2887,axiom,
    ( ~ esk662_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk95_5(X1,X2,X3,X4,X5) ),
    i_0_2170 ).

cnf(c_0_2888,plain,
    ( esk629_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk662_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | p(X4)
    | p(X2)
    | p(X1) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2877,c_0_2878]),c_0_2879]) ).

cnf(c_0_2889,plain,
    ( ~ esk137_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    inference(spm,[status(thm)],[c_0_2880,c_0_2881]) ).

cnf(c_0_2890,plain,
    ( esk137_9(true,X1,X2,X3,true,true,X4,X5,true)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2882,c_0_2883]),c_0_2756])]),c_0_2884]) ).

cnf(c_0_2891,axiom,
    ( esk148_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk605_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_402 ).

cnf(c_0_2892,axiom,
    ( esk199_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk188_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_2275 ).

cnf(c_0_2893,axiom,
    ( esk188_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_87 ).

cnf(c_0_2894,plain,
    ( esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk138_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    inference(spm,[status(thm)],[c_0_2885,c_0_2886]) ).

cnf(c_0_2895,plain,
    ( esk629_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2887,c_0_2888]),c_0_2852]) ).

cnf(c_0_2896,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | ~ esk147_9(true,X3,X2,X4,true,true,X1,X5,true) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2889,c_0_2890]),c_0_2863]) ).

cnf(c_0_2897,axiom,
    ( esk148_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_905 ).

cnf(c_0_2898,plain,
    ( esk148_9(true,X1,X2,X3,true,true,X4,X5,true)
    | esk604_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | p(X2)
    | p(X1) ),
    inference(spm,[status(thm)],[c_0_2891,c_0_2870]) ).

cnf(c_0_2899,axiom,
    ( p(X2)
    | p(X13)
    | ~ p(X1)
    | ~ esk163_9(X3,X4,X5,X6,X7,X8,X9,X10,X11)
    | ~ p(X12)
    | ~ esk586_21(X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X12,X2,X1,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1812 ).

cnf(c_0_2900,axiom,
    ( esk586_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk199_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_1422 ).

cnf(c_0_2901,plain,
    ( esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk199_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    inference(spm,[status(thm)],[c_0_2892,c_0_2893]) ).

cnf(c_0_2902,axiom,
    ( ~ esk197_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk148_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk138_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_668 ).

cnf(c_0_2903,axiom,
    ( esk197_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_1057 ).

cnf(c_0_2904,axiom,
    ( esk163_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2369 ).

cnf(c_0_2905,plain,
    ( esk645_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk138_9(true,X1,X2,X3,true,true,X4,X5,true)
    | p(X4)
    | p(X2)
    | p(X1) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2894,c_0_2895]),c_0_2896]) ).

cnf(c_0_2906,plain,
    ( esk596_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk148_9(true,X1,X2,X3,true,true,X4,X5,true)
    | p(X2)
    | p(X1) ),
    inference(spm,[status(thm)],[c_0_2897,c_0_2874]) ).

cnf(c_0_2907,plain,
    ( esk148_9(true,X1,X2,X3,true,true,X4,X5,true)
    | p(X1)
    | p(X2)
    | p(X4)
    | p(X5) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2875,c_0_2898]),c_0_2756])]) ).

cnf(c_0_2908,axiom,
    ( p(X11)
    | ~ p(X1)
    | ~ esk590_21(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X12)
    | ~ p(X13)
    | ~ esk167_9(X2,X3,X4,X5,X6,X7,X8,X9,X10) ),
    i_0_2486 ).

cnf(c_0_2909,axiom,
    ( esk590_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk199_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_2487 ).

cnf(c_0_2910,axiom,
    ( esk167_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2329 ).

cnf(c_0_2911,plain,
    ( p(X1)
    | p(X2)
    | ~ esk199_13(X3,X4,X5,X6,X7,X8,X9,X10,X11,X2,X12,X1,X13)
    | ~ p(X12)
    | ~ p(X13)
    | ~ esk163_9(X3,X4,X5,X6,X7,X8,X9,X10,X11) ),
    inference(spm,[status(thm)],[c_0_2899,c_0_2900]) ).

cnf(c_0_2912,plain,
    ( esk200_13(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9)
    | esk199_13(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_2901,c_0_2863]) ).

cnf(c_0_2913,plain,
    ( ~ esk138_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk148_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    inference(spm,[status(thm)],[c_0_2902,c_0_2903]) ).

cnf(c_0_2914,plain,
    ( esk138_9(true,X1,X2,X3,true,true,X4,X5,true)
    | p(X1)
    | p(X2)
    | p(X4)
    | esk163_9(true,X1,X2,X3,true,true,X4,X5,true) ),
    inference(spm,[status(thm)],[c_0_2904,c_0_2905]) ).

cnf(c_0_2915,plain,
    ( esk148_9(true,X1,X2,X3,true,true,X4,X5,true)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2882,c_0_2906]),c_0_2756])]),c_0_2907]) ).

cnf(c_0_2916,plain,
    ( p(X1)
    | ~ esk199_13(X2,X3,X4,X5,X6,X7,X8,X9,X10,X1,X11,X12,X13)
    | ~ p(X13)
    | ~ p(X12)
    | ~ p(X11)
    | ~ esk167_9(X2,X3,X4,X5,X6,X7,X8,X9,X10) ),
    inference(spm,[status(thm)],[c_0_2908,c_0_2909]) ).

cnf(c_0_2917,plain,
    ( esk138_9(true,X1,X2,X3,true,true,X4,X5,true)
    | p(X1)
    | p(X2)
    | p(X4)
    | esk167_9(true,X1,X2,X3,true,true,X4,X5,true) ),
    inference(spm,[status(thm)],[c_0_2910,c_0_2905]) ).

cnf(c_0_2918,plain,
    ( esk200_13(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6)
    | p(X8)
    | ~ p(X7)
    | ~ p(X9)
    | ~ esk163_9(true,X1,X2,X3,true,true,X4,X5,true) ),
    inference(spm,[status(thm)],[c_0_2911,c_0_2912]) ).

cnf(c_0_2919,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | esk163_9(true,X3,X2,X4,true,true,X1,X5,true) ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2913,c_0_2914]),c_0_2863]),c_0_2915]) ).

cnf(c_0_2920,plain,
    ( esk200_13(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6)
    | ~ p(X9)
    | ~ p(X8)
    | ~ p(X7)
    | ~ esk167_9(true,X1,X2,X3,true,true,X4,X5,true) ),
    inference(spm,[status(thm)],[c_0_2916,c_0_2912]) ).

cnf(c_0_2921,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | esk167_9(true,X3,X2,X4,true,true,X1,X5,true) ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2913,c_0_2917]),c_0_2863]),c_0_2915]) ).

cnf(c_0_2922,plain,
    ( esk200_13(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9)
    | p(X8)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4)
    | ~ p(X7)
    | ~ p(X9) ),
    inference(spm,[status(thm)],[c_0_2918,c_0_2919]) ).

cnf(c_0_2923,plain,
    ( esk200_13(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4)
    | ~ p(X9)
    | ~ p(X7) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2920,c_0_2921]),c_0_2922]) ).

cnf(c_0_2924,axiom,
    ( esk524_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk523_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk253_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_1941 ).

cnf(c_0_2925,axiom,
    ( esk253_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_895 ).

cnf(c_0_2926,plain,
    ( esk200_13(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6)
    | ~ p(X7) ),
    inference(spm,[status(thm)],[c_0_2923,c_0_2756]) ).

cnf(c_0_2927,axiom,
    ( esk515_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk257_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_476 ).

cnf(c_0_2928,axiom,
    ( esk257_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_1118 ).

cnf(c_0_2929,plain,
    ( esk524_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk523_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    inference(spm,[status(thm)],[c_0_2924,c_0_2925]) ).

cnf(c_0_2930,plain,
    ( esk200_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_2926,c_0_2756]) ).

cnf(c_0_2931,axiom,
    ( esk523_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X10) ),
    i_0_1666 ).

cnf(c_0_2932,axiom,
    ( esk549_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk240_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_1945 ).

cnf(c_0_2933,axiom,
    ( esk240_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_1098 ).

cnf(c_0_2934,plain,
    ( esk515_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    inference(spm,[status(thm)],[c_0_2927,c_0_2928]) ).

cnf(c_0_2935,axiom,
    ( esk515_21(X2,X3,X4,X5,X6,X7,X8,X9,X10,X1,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X1) ),
    i_0_2442 ).

cnf(c_0_2936,axiom,
    ( esk209_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk524_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1383 ).

cnf(c_0_2937,plain,
    ( esk524_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | esk523_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | p(X4)
    | p(X2)
    | p(X1) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2929,c_0_2930]),c_0_2931]) ).

cnf(c_0_2938,plain,
    ( esk549_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    inference(spm,[status(thm)],[c_0_2932,c_0_2933]) ).

cnf(c_0_2939,axiom,
    ( esk150_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2297 ).

cnf(c_0_2940,axiom,
    ( esk209_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_553 ).

cnf(c_0_2941,plain,
    ( esk515_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | esk516_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | p(X4)
    | p(X2)
    | p(X1) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2934,c_0_2930]),c_0_2935]) ).

cnf(c_0_2942,axiom,
    ( p(X2)
    | p(X13)
    | ~ p(X1)
    | ~ p(X3)
    | ~ esk523_21(X4,X5,X6,X7,X8,X9,X10,X11,X12,X2,X1,X13,X3,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2421 ).

cnf(c_0_2943,plain,
    ( esk209_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | esk523_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_2936,c_0_2937]) ).

cnf(c_0_2944,axiom,
    ( esk583_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk150_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk549_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2417 ).

cnf(c_0_2945,plain,
    ( esk549_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6)
    | esk550_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15) ),
    inference(spm,[status(thm)],[c_0_2938,c_0_2930]) ).

cnf(c_0_2946,plain,
    ( esk150_9(true,X1,X2,X3,true,true,X4,X5,true)
    | p(X4)
    | p(X2)
    | p(X1) ),
    inference(spm,[status(thm)],[c_0_2939,c_0_2895]) ).

cnf(c_0_2947,axiom,
    ( ~ esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk209_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk268_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_1059 ).

cnf(c_0_2948,axiom,
    ( esk268_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_2353 ).

cnf(c_0_2949,axiom,
    ( p(X10)
    | ~ esk515_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ p(X12)
    | ~ p(X11)
    | ~ p(X13) ),
    i_0_921 ).

cnf(c_0_2950,plain,
    ( esk209_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | esk515_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_2940,c_0_2941]) ).

cnf(c_0_2951,plain,
    ( esk209_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6)
    | p(X7) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2942,c_0_2943]),c_0_2756])]) ).

cnf(c_0_2952,axiom,
    ( esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk210_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk560_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_260 ).

cnf(c_0_2953,axiom,
    ( esk560_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2491 ).

cnf(c_0_2954,axiom,
    ( ~ esk583_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk163_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_81 ).

cnf(c_0_2955,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | p(X4)
    | esk583_21(true,X2,X3,X5,true,true,X4,X6,true,X1,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | esk550_21(true,X2,X3,X5,true,true,X4,X6,true,X1,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2944,c_0_2945]),c_0_2946]) ).

cnf(c_0_2956,plain,
    ( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk209_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    inference(spm,[status(thm)],[c_0_2947,c_0_2948]) ).

cnf(c_0_2957,plain,
    ( esk209_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2949,c_0_2950]),c_0_2756])]),c_0_2951]) ).

cnf(c_0_2958,axiom,
    ( esk220_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk524_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_853 ).

cnf(c_0_2959,axiom,
    ( esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk259_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_1342 ).

cnf(c_0_2960,axiom,
    ( esk259_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_2006 ).

cnf(c_0_2961,plain,
    ( esk210_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    inference(spm,[status(thm)],[c_0_2952,c_0_2953]) ).

cnf(c_0_2962,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | p(X4)
    | esk550_21(true,X3,X2,X5,true,true,X1,X6,true,X4,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2954,c_0_2955]),c_0_2919]) ).

cnf(c_0_2963,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | p(X4)
    | ~ esk219_13(true,X2,X3,X5,true,true,X4,X6,true,X1,true,X7,true) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2956,c_0_2957]),c_0_2930]) ).

cnf(c_0_2964,axiom,
    ( esk220_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_22 ).

cnf(c_0_2965,plain,
    ( esk523_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | esk220_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_2958,c_0_2937]) ).

cnf(c_0_2966,axiom,
    ( p(X16)
    | ~ p(X1)
    | ~ p(X2)
    | ~ esk508_21(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X1,X2,X16,X17,X18,X19,X20,X21)
    | ~ p(X17)
    | ~ esk235_13(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
    i_0_2011 ).

cnf(c_0_2967,axiom,
    ( esk508_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_21 ).

cnf(c_0_2968,plain,
    ( esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    inference(spm,[status(thm)],[c_0_2959,c_0_2960]) ).

cnf(c_0_2969,axiom,
    ( ~ esk269_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk210_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk220_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_2272 ).

cnf(c_0_2970,axiom,
    ( esk269_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_1701 ).

cnf(c_0_2971,axiom,
    ( esk235_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1052 ).

cnf(c_0_2972,plain,
    ( esk210_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | esk567_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2961,c_0_2962]),c_0_2963]) ).

cnf(c_0_2973,plain,
    ( esk515_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | esk220_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_2964,c_0_2941]) ).

cnf(c_0_2974,plain,
    ( esk220_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6)
    | p(X7) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2942,c_0_2965]),c_0_2756])]) ).

cnf(c_0_2975,axiom,
    ( ~ p(X1)
    | ~ p(X2)
    | ~ esk512_21(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X2,X16,X1,X17,X18,X19,X20,X21)
    | ~ p(X17)
    | ~ esk239_13(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
    | ~ p(X16) ),
    i_0_1780 ).

cnf(c_0_2976,axiom,
    ( esk512_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_2511 ).

cnf(c_0_2977,axiom,
    ( esk239_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_333 ).

cnf(c_0_2978,plain,
    ( p(X1)
    | ~ esk235_13(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
    | ~ esk270_17(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X1,X17)
    | ~ p(X17)
    | ~ p(X16)
    | ~ p(X15) ),
    inference(spm,[status(thm)],[c_0_2966,c_0_2967]) ).

cnf(c_0_2979,plain,
    ( esk270_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11)
    | esk271_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(spm,[status(thm)],[c_0_2968,c_0_2930]) ).

cnf(c_0_2980,plain,
    ( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk210_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk220_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    inference(spm,[status(thm)],[c_0_2969,c_0_2970]) ).

cnf(c_0_2981,plain,
    ( esk210_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | esk235_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(spm,[status(thm)],[c_0_2971,c_0_2972]) ).

cnf(c_0_2982,plain,
    ( esk220_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2949,c_0_2973]),c_0_2756])]),c_0_2974]) ).

cnf(c_0_2983,plain,
    ( ~ esk239_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ p(X17)
    | ~ p(X15)
    | ~ p(X14)
    | ~ p(X16) ),
    inference(spm,[status(thm)],[c_0_2975,c_0_2976]) ).

cnf(c_0_2984,plain,
    ( esk210_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | esk239_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(spm,[status(thm)],[c_0_2977,c_0_2972]) ).

cnf(c_0_2985,plain,
    ( esk271_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4)
    | p(X10)
    | ~ esk235_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | ~ p(X11)
    | ~ p(X9)
    | ~ p(X8) ),
    inference(spm,[status(thm)],[c_0_2978,c_0_2979]) ).

cnf(c_0_2986,plain,
    ( esk235_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2980,c_0_2981]),c_0_2982]),c_0_2930]) ).

cnf(c_0_2987,plain,
    ( esk271_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4)
    | ~ esk239_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | ~ p(X11)
    | ~ p(X9)
    | ~ p(X8)
    | ~ p(X10) ),
    inference(spm,[status(thm)],[c_0_2983,c_0_2979]) ).

cnf(c_0_2988,plain,
    ( esk239_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2980,c_0_2984]),c_0_2982]),c_0_2930]) ).

cnf(c_0_2989,plain,
    ( esk271_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11)
    | p(X10)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6)
    | ~ p(X11)
    | ~ p(X9)
    | ~ p(X8) ),
    inference(spm,[status(thm)],[c_0_2985,c_0_2986]) ).

cnf(c_0_2990,plain,
    ( esk271_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6)
    | ~ p(X11)
    | ~ p(X9)
    | ~ p(X8) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2987,c_0_2988]),c_0_2989]) ).

cnf(c_0_2991,plain,
    ( esk271_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4)
    | ~ p(X9)
    | ~ p(X8) ),
    inference(spm,[status(thm)],[c_0_2990,c_0_2756]) ).

cnf(c_0_2992,axiom,
    ( esk443_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk442_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk324_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_289 ).

cnf(c_0_2993,axiom,
    ( esk324_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_2126 ).

cnf(c_0_2994,plain,
    ( esk271_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,true,X9,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6)
    | ~ p(X8) ),
    inference(spm,[status(thm)],[c_0_2991,c_0_2756]) ).

cnf(c_0_2995,axiom,
    ( esk434_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk435_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk328_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_347 ).

cnf(c_0_2996,axiom,
    ( esk328_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_327 ).

cnf(c_0_2997,plain,
    ( esk443_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk442_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    inference(spm,[status(thm)],[c_0_2992,c_0_2993]) ).

cnf(c_0_2998,plain,
    ( esk271_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_2994,c_0_2756]) ).

cnf(c_0_2999,axiom,
    ( esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk470_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk310_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_1900 ).

cnf(c_0_3000,axiom,
    ( esk310_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_2219 ).

cnf(c_0_3001,plain,
    ( esk434_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk435_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    inference(spm,[status(thm)],[c_0_2995,c_0_2996]) ).

cnf(c_0_3002,axiom,
    ( esk281_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk443_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2388 ).

cnf(c_0_3003,plain,
    ( esk443_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true,X9,X10,X11,X12)
    | esk442_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true,X9,X10,X11,X12)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(spm,[status(thm)],[c_0_2997,c_0_2998]) ).

cnf(c_0_3004,plain,
    ( esk470_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    inference(spm,[status(thm)],[c_0_2999,c_0_3000]) ).

cnf(c_0_3005,axiom,
    ( esk221_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_117 ).

cnf(c_0_3006,axiom,
    ( esk281_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk435_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_676 ).

cnf(c_0_3007,plain,
    ( esk434_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true,X9,X10,X11,X12)
    | esk435_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true,X9,X10,X11,X12)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(spm,[status(thm)],[c_0_3001,c_0_2998]) ).

cnf(c_0_3008,axiom,
    ( p(X2)
    | ~ p(X1)
    | ~ p(X3)
    | ~ esk442_21(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X3,X2,X1,X18,X19,X20,X21)
    | ~ p(X17) ),
    i_0_304 ).

cnf(c_0_3009,plain,
    ( esk442_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true,X9,X10,X11,X12)
    | esk281_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_3002,c_0_3003]) ).

cnf(c_0_3010,axiom,
    ( esk504_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk221_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk470_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1736 ).

cnf(c_0_3011,plain,
    ( esk470_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true,X9,X10,X11,X12)
    | esk471_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true,X9,X10,X11,X12)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(spm,[status(thm)],[c_0_3004,c_0_2998]) ).

cnf(c_0_3012,plain,
    ( esk221_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_3005,c_0_2962]) ).

cnf(c_0_3013,axiom,
    ( ~ esk339_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk291_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk281_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_2503 ).

cnf(c_0_3014,axiom,
    ( esk339_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_2287 ).

cnf(c_0_3015,axiom,
    ( ~ p(X1)
    | ~ p(X2)
    | ~ p(X3)
    | ~ esk434_21(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X2,X3,X1,X18,X19,X20,X21)
    | ~ p(X17) ),
    i_0_1011 ).

cnf(c_0_3016,plain,
    ( esk434_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true,X9,X10,X11,X12)
    | esk281_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_3006,c_0_3007]) ).

cnf(c_0_3017,plain,
    ( esk281_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6)
    | p(X8) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3008,c_0_3009]),c_0_2756])]) ).

cnf(c_0_3018,axiom,
    ( esk280_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk291_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk472_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1677 ).

cnf(c_0_3019,axiom,
    ( esk472_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2180 ).

cnf(c_0_3020,axiom,
    ( ~ esk504_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk235_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_345 ).

cnf(c_0_3021,plain,
    ( esk504_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true,X9,X10,X11,X12)
    | esk471_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true,X9,X10,X11,X12)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3010,c_0_3011]),c_0_3012]) ).

cnf(c_0_3022,plain,
    ( ~ esk291_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk281_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    inference(spm,[status(thm)],[c_0_3013,c_0_3014]) ).

cnf(c_0_3023,plain,
    ( esk281_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3015,c_0_3016]),c_0_2756])]),c_0_3017]) ).

cnf(c_0_3024,axiom,
    ( esk279_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk290_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk473_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_269 ).

cnf(c_0_3025,axiom,
    ( esk473_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1240 ).

cnf(c_0_3026,axiom,
    ( ~ esk290_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk338_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk280_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_1811 ).

cnf(c_0_3027,axiom,
    ( esk338_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_1766 ).

cnf(c_0_3028,plain,
    ( esk280_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk291_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    inference(spm,[status(thm)],[c_0_3018,c_0_3019]) ).

cnf(c_0_3029,plain,
    ( esk471_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true,X9,X10,X11,X12)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3020,c_0_3021]),c_0_2986]) ).

cnf(c_0_3030,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | p(X4)
    | ~ esk291_17(true,X2,X3,X5,true,true,X4,X6,true,X1,true,X7,true,true,true,X8,true) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3022,c_0_3023]),c_0_2998]) ).

cnf(c_0_3031,axiom,
    ( ~ esk289_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk337_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk279_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_1181 ).

cnf(c_0_3032,axiom,
    ( esk337_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_1445 ).

cnf(c_0_3033,plain,
    ( esk290_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk279_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    inference(spm,[status(thm)],[c_0_3024,c_0_3025]) ).

cnf(c_0_3034,plain,
    ( ~ esk280_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk290_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    inference(spm,[status(thm)],[c_0_3026,c_0_3027]) ).

cnf(c_0_3035,plain,
    ( esk280_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3028,c_0_3029]),c_0_3030]) ).

cnf(c_0_3036,axiom,
    ( esk574_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk557_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1097 ).

cnf(c_0_3037,axiom,
    ( esk557_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_2531 ).

cnf(c_0_3038,axiom,
    ( esk458_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk284_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk289_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk316_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_170 ).

cnf(c_0_3039,axiom,
    ( esk316_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_2360 ).

cnf(c_0_3040,plain,
    ( ~ esk279_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk289_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    inference(spm,[status(thm)],[c_0_3031,c_0_3032]) ).

cnf(c_0_3041,plain,
    ( esk290_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true)
    | esk279_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_3033,c_0_3029]) ).

cnf(c_0_3042,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | p(X4)
    | ~ esk290_17(true,X3,X2,X5,true,true,X1,X6,true,X4,true,X7,true,true,true,X8,true) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3034,c_0_3035]),c_0_2998]) ).

cnf(c_0_3043,plain,
    ( esk574_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    inference(spm,[status(thm)],[c_0_3036,c_0_3037]) ).

cnf(c_0_3044,plain,
    ( esk458_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk289_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk284_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    inference(spm,[status(thm)],[c_0_3038,c_0_3039]) ).

cnf(c_0_3045,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | p(X4)
    | ~ esk289_17(true,X3,X2,X5,true,true,X1,X6,true,X4,true,X7,true,true,true,X8,true) ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3040,c_0_3041]),c_0_2998]),c_0_3042]) ).

cnf(c_0_3046,axiom,
    ( esk576_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk574_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1228 ).

cnf(c_0_3047,plain,
    ( esk574_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | esk218_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_3043,c_0_2962]) ).

cnf(c_0_3048,axiom,
    ( esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | esk653_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk636_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1319 ).

cnf(c_0_3049,axiom,
    ( esk636_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_149 ).

cnf(c_0_3050,axiom,
    ( esk459_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk227_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk458_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_163 ).

cnf(c_0_3051,plain,
    ( esk458_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true,X9,X10,X11,X12)
    | esk284_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3044,c_0_2998]),c_0_3045]) ).

cnf(c_0_3052,axiom,
    ( esk203_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk227_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk576_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1603 ).

cnf(c_0_3053,plain,
    ( esk576_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | esk218_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(spm,[status(thm)],[c_0_3046,c_0_3047]) ).

cnf(c_0_3054,axiom,
    ( esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk213_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk537_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk246_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_138 ).

cnf(c_0_3055,axiom,
    ( esk246_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_346 ).

cnf(c_0_3056,plain,
    ( esk653_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    inference(spm,[status(thm)],[c_0_3048,c_0_3049]) ).

cnf(c_0_3057,plain,
    ( esk284_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true)
    | esk459_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true,X9,X10,X11,X12)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4)
    | ~ esk227_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true) ),
    inference(spm,[status(thm)],[c_0_3050,c_0_3051]) ).

cnf(c_0_3058,plain,
    ( esk203_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | esk227_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | esk218_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_3052,c_0_3053]) ).

cnf(c_0_3059,plain,
    ( esk537_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | esk213_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    inference(spm,[status(thm)],[c_0_3054,c_0_3055]) ).

cnf(c_0_3060,axiom,
    ( esk655_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk653_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1464 ).

cnf(c_0_3061,plain,
    ( esk653_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk147_9(true,X1,X2,X3,true,true,X4,X5,true)
    | p(X4)
    | p(X2)
    | p(X1) ),
    inference(spm,[status(thm)],[c_0_3056,c_0_2895]) ).

cnf(c_0_3062,axiom,
    ( ~ esk274_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk284_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk332_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_2339 ).

cnf(c_0_3063,axiom,
    ( esk332_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    i_0_455 ).

cnf(c_0_3064,axiom,
    ( ~ esk235_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk459_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1920 ).

cnf(c_0_3065,plain,
    ( esk203_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | esk284_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true)
    | esk459_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true,X9,X10,X11,X12)
    | esk218_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(spm,[status(thm)],[c_0_3057,c_0_3058]) ).

cnf(c_0_3066,axiom,
    ( esk274_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1305 ).

cnf(c_0_3067,axiom,
    ( esk538_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk156_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk537_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_601 ).

cnf(c_0_3068,plain,
    ( esk537_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | esk213_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | esk218_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(spm,[status(thm)],[c_0_3059,c_0_2930]) ).

cnf(c_0_3069,axiom,
    ( esk132_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | esk156_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk655_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1522 ).

cnf(c_0_3070,plain,
    ( esk655_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk147_9(true,X1,X2,X3,true,true,X4,X5,true)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_3060,c_0_3061]) ).

cnf(c_0_3071,axiom,
    ( ~ esk203_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk213_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk262_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_417 ).

cnf(c_0_3072,axiom,
    ( esk262_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_2187 ).

cnf(c_0_3073,plain,
    ( ~ esk284_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk274_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    inference(spm,[status(thm)],[c_0_3062,c_0_3063]) ).

cnf(c_0_3074,plain,
    ( esk203_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | esk284_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true)
    | esk218_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3064,c_0_3065]),c_0_2986]) ).

cnf(c_0_3075,plain,
    ( esk274_17(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,true,true,X8,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_3066,c_0_3029]) ).

cnf(c_0_3076,plain,
    ( esk538_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | esk213_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | esk218_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4)
    | ~ esk156_9(true,X1,X2,X3,true,true,X4,X5,true) ),
    inference(spm,[status(thm)],[c_0_3067,c_0_3068]) ).

cnf(c_0_3077,plain,
    ( esk156_9(true,X1,X2,X3,true,true,X4,X5,true)
    | esk147_9(true,X1,X2,X3,true,true,X4,X5,true)
    | esk132_9(true,X1,X2,X3,true,true,X4,X5,true)
    | p(X4)
    | p(X2)
    | p(X1) ),
    inference(spm,[status(thm)],[c_0_3069,c_0_3070]) ).

cnf(c_0_3078,plain,
    ( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk203_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk213_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    inference(spm,[status(thm)],[c_0_3071,c_0_3072]) ).

cnf(c_0_3079,plain,
    ( esk203_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | esk218_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3073,c_0_3074]),c_0_2998]),c_0_3075]) ).

cnf(c_0_3080,axiom,
    ( ~ esk538_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk163_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_1318 ).

cnf(c_0_3081,plain,
    ( esk132_9(true,X1,X2,X3,true,true,X4,X5,true)
    | esk538_21(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true,X8,X9,X10,X11,X12,X13,X14,X15)
    | esk213_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | esk218_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3076,c_0_3077]),c_0_2896]) ).

cnf(c_0_3082,axiom,
    ( esk142_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_1724 ).

cnf(c_0_3083,axiom,
    ( esk208_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk552_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_684 ).

cnf(c_0_3084,axiom,
    ( esk552_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
    | ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    i_0_212 ).

cnf(c_0_3085,axiom,
    ( ~ esk191_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk132_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk142_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_2281 ).

cnf(c_0_3086,axiom,
    ( esk191_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    i_0_3 ).

cnf(c_0_3087,plain,
    ( esk218_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4)
    | ~ esk213_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3078,c_0_3079]),c_0_2930]) ).

cnf(c_0_3088,plain,
    ( esk132_9(true,X1,X2,X3,true,true,X4,X5,true)
    | esk213_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | esk218_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3080,c_0_3081]),c_0_2919]) ).

cnf(c_0_3089,plain,
    ( esk596_21(true,X1,X2,X3,true,true,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
    | esk142_9(true,X1,X2,X3,true,true,X4,X5,true)
    | p(X2)
    | p(X1) ),
    inference(spm,[status(thm)],[c_0_3082,c_0_2874]) ).

cnf(c_0_3090,axiom,
    ( ~ esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk267_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk208_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_221 ).

cnf(c_0_3091,axiom,
    ( esk267_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    i_0_1575 ).

cnf(c_0_3092,plain,
    ( esk208_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
    inference(spm,[status(thm)],[c_0_3083,c_0_3084]) ).

cnf(c_0_3093,plain,
    ( ~ esk132_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk142_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
    | ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
    inference(spm,[status(thm)],[c_0_3085,c_0_3086]) ).

cnf(c_0_3094,plain,
    ( esk132_9(true,X1,X2,X3,true,true,X4,X5,true)
    | esk218_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6) ),
    inference(spm,[status(thm)],[c_0_3087,c_0_3088]) ).

cnf(c_0_3095,plain,
    ( esk142_9(true,X1,X2,X3,true,true,X4,X5,true)
    | p(X1)
    | p(X2)
    | p(X4)
    | ~ p(X5) ),
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2882,c_0_3089]),c_0_2756])]) ).

cnf(c_0_3096,plain,
    ( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk208_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
    | ~ esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
    inference(spm,[status(thm)],[c_0_3090,c_0_3091]) ).

cnf(c_0_3097,plain,
    ( esk208_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | esk219_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4) ),
    inference(spm,[status(thm)],[c_0_3092,c_0_2962]) ).

cnf(c_0_3098,plain,
    ( esk218_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X6)
    | p(X1)
    | p(X2)
    | p(X4)
    | ~ esk142_9(true,X1,X2,X3,true,true,X4,X5,true) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3093,c_0_3094]),c_0_2863]) ).

cnf(c_0_3099,plain,
    ( esk142_9(true,X1,X2,X3,true,true,X4,true,true)
    | p(X4)
    | p(X2)
    | p(X1) ),
    inference(spm,[status(thm)],[c_0_3095,c_0_2756]) ).

cnf(c_0_3100,plain,
    ( esk219_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X6)
    | ~ esk218_13(true,X1,X2,X3,true,true,X4,X5,true,X6,true,X7,true) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3096,c_0_3097]),c_0_2930]) ).

cnf(c_0_3101,plain,
    ( esk218_13(true,X1,X2,X3,true,true,X4,true,true,X5,true,X6,true)
    | p(X4)
    | p(X2)
    | p(X1)
    | p(X5) ),
    inference(spm,[status(thm)],[c_0_3098,c_0_3099]) ).

cnf(c_0_3102,plain,
    ( p(X1)
    | p(X2)
    | p(X3)
    | p(X4) ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3100,c_0_3101]),c_0_2963]) ).

cnf(c_0_3103,plain,
    ( p(X1)
    | p(X2)
    | p(X3) ),
    inference(ef,[status(thm)],[c_0_3102]) ).

cnf(c_0_3104,plain,
    ( p(X1)
    | p(X2) ),
    inference(ef,[status(thm)],[c_0_3103]) ).

cnf(c_0_3105,axiom,
    ~ p(false),
    rule_false ).

cnf(c_0_3106,plain,
    p(X1),
    inference(ef,[status(thm)],[c_0_3104]) ).

cnf(c_0_3107,plain,
    $false,
    inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3105,c_0_3106])]),
    [proof] ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13  % Problem    : SYO588-1 : TPTP v9.2.1. Bugfixed v5.5.1.
% 0.12/0.13  % Command    : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.34  % Computer : n018.cluster.edu
% 0.16/0.34  % Model    : x86_64 x86_64
% 0.16/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34  % Memory   : 8042.1875MB
% 0.16/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34  % CPULimit   : 300
% 0.16/0.34  % WCLimit    : 300
% 0.16/0.34  % DateTime   : Tue May  5 09:14:32 EDT 2026
% 0.16/0.35  % CPUTime    : 
% 0.19/0.36  % start to proof: theBenchmark
% 6.31/4.21  % Version  : CSE_E---1.7
% 6.31/4.21  % Problem  : theBenchmark.p
% 6.31/4.21  % SZS status Unsatisfiable for theBenchmark.p
% 6.31/4.21  % SZS output start CNFRefutation
% See solution above
% 6.31/4.22  % Total time : 3.592s
%------------------------------------------------------------------------------