↑ Up

iProver---3.9.4.UNS-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : iProver---3.9.4
% Problem  : SYO588-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM

% Computer : n005.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Fri Sep 25 03:51:28 PM UTC 2026

% Result   : Unsatisfiable 168.81s 34.47s
% Output   : CNFRefutation 168.81s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :    9
%            Number of leaves      :  131
% Syntax   : Number of formulae    :  431 (  16 unt;   0 def)
%            Number of atoms       : 4241 (   0 equ)
%            Maximal formula atoms :    6 (   9 avg)
%            Number of connectives : 1313 ( 636   ~; 677   |;   0   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   28 (  16 avg)
%            Maximal term depth    :    1 (   1 avg)
%            Number of types       :    1 (   0 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of predicates  :  134 ( 133 usr;   6 prp; 0-21 aty)
%            Number of functors    :    0 (   0 usr;   0 con; --- aty)
%            Number of variables   : 5536 (   0 sgn5536   !;   0   ?;3408   :)

% Comments : 
%------------------------------------------------------------------------------
fof(f3,axiom,
    ! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
      ( ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk191_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3) ).

fof(f7,axiom,
    ! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
      ( ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk196_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_7) ).

fof(f22,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk220_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk516_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_22) ).

fof(f27,axiom,
    ! [X2,X3,X0,X1,X4] :
      ( ~ esk66_5(X0,X1,X2,X3,X4)
      | ~ esk125_5(X0,X1,X2,X3,X4)
      | ~ esk76_5(X0,X1,X2,X3,X4) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_27) ).

fof(f67,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk91_5(X0,X1,X2,X3,X4)
      | ~ esk662_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_67) ).

fof(f87,axiom,
    ! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
      ( esk188_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_87) ).

fof(f117,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk221_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_117) ).

fof(f138,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk537_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk246_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk213_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk218_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_138) ).

fof(f149,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk636_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk629_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_149) ).

fof(f163,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk458_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk459_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk227_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_163) ).

fof(f170,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk289_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk284_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk458_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk316_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_170) ).

fof(f212,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk552_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_212) ).

fof(f221,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
      ( ~ esk208_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk267_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk218_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_221) ).

fof(f249,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk538_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk167_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_249) ).

fof(f260,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk210_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk567_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk560_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk219_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_260) ).

fof(f267,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk37_1(X0)
      | ~ esk765_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_267) ).

fof(f269,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk473_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk290_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk279_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_269) ).

fof(f327,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
      ( ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk328_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_327) ).

fof(f333,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk239_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk567_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_333) ).

fof(f346,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
      ( esk246_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_346) ).

fof(f347,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk435_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk328_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk434_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_347) ).

fof(f361,axiom,
    ! [X0] :
      ( esk52_1(X0)
      | ~ esk5_1(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_361) ).

fof(f417,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
      ( ~ esk262_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk213_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk203_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_417) ).

fof(f432,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk76_5(X0,X1,X2,X3,X4)
      | ~ esk686_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_432) ).

fof(f455,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
      ( ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk332_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_455) ).

fof(f476,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk516_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk257_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk515_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_476) ).

fof(f478,axiom,
    ! [X2,X3,X0,X1,X4] :
      ( ~ esk75_5(X0,X1,X2,X3,X4)
      | ~ esk65_5(X0,X1,X2,X3,X4)
      | ~ esk124_5(X0,X1,X2,X3,X4) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_478) ).

fof(f481,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ p(X5)
      | ~ p(X8)
      | ~ esk95_5(X0,X1,X2,X3,X4)
      | p(X6)
      | ~ p(X7)
      | ~ esk668_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_481) ).

fof(f497,axiom,
    ! [X2,X3,X0,X1,X4] :
      ( esk98_5(X0,X1,X2,X3,X4)
      | ~ esk58_5(X0,X1,X2,X3,X4) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_497) ).

fof(f538,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk169_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk628_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk629_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_538) ).

fof(f553,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk516_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk209_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_553) ).

fof(f590,axiom,
    ! [X2,X3,X0,X1,X4] :
      ( esk57_5(X0,X1,X2,X3,X4)
      | ~ esk46_1(X0)
      | esk58_5(X0,X1,X2,X3,X4) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_590) ).

fof(f601,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk538_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk537_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk156_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_601) ).

fof(f635,axiom,
    ( esk2_0
    | ~ esk1_0 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_635) ).

fof(f668,axiom,
    ! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
      ( ~ esk138_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk148_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk197_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_668) ).

fof(f674,axiom,
    ! [X0] :
      ( ~ esk2_0
      | ~ p(X0)
      | ~ esk4_1(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_674) ).

fof(f676,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk435_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk281_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_676) ).

fof(f684,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk219_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk208_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk552_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_684) ).

fof(f756,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk722_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk91_5(X0,X1,X2,X3,X4) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_756) ).

fof(f788,axiom,
    ! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
      ( ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk185_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_788) ).

fof(f816,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk596_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk597_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk185_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_816) ).

fof(f835,axiom,
    ! [X2,X3,X0,X1,X4] :
      ( ~ esk58_5(X0,X1,X2,X3,X4)
      | esk124_5(X0,X1,X2,X3,X4) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_835) ).

fof(f882,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk750_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk11_1(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_882) ).

fof(f905,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk148_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk597_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_905) ).

fof(f921,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ p(X12)
      | ~ p(X10)
      | ~ p(X11)
      | p(X9)
      | ~ esk515_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_921) ).

fof(f945,axiom,
    ! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
      ( ~ esk117_5(X0,X1,X2,X3,X4)
      | esk128_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_945) ).

fof(f996,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk742_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk57_5(X0,X1,X2,X3,X4) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_996) ).

fof(f1011,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ p(X16)
      | ~ esk434_21(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X1,X2,X0,X17,X18,X19,X20)
      | ~ p(X2)
      | ~ p(X1)
      | ~ p(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1011) ).

fof(f1023,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk597_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk137_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1023) ).

fof(f1057,axiom,
    ! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
      ( ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk197_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1057) ).

fof(f1059,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
      ( ~ esk268_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk209_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk219_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1059) ).

fof(f1073,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk721_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk66_5(X0,X1,X2,X3,X4)
      | esk75_5(X0,X1,X2,X3,X4)
      | esk722_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1073) ).

fof(f1097,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk557_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk218_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk574_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1097) ).

fof(f1098,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
      ( ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk240_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1098) ).

fof(f1118,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
      ( ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk257_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1118) ).

fof(f1127,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk765_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk762_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk21_1(X0)
      | esk12_1(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1127) ).

fof(f1132,axiom,
    ! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
      ( ~ esk147_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk196_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk137_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1132) ).

fof(f1147,axiom,
    ! [X0] :
      ( ~ esk53_1(X0)
      | ~ esk22_1(X0)
      | ~ esk12_1(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1147) ).

fof(f1163,axiom,
    ! [X0] :
      ( esk4_1(X0)
      | ~ esk3_0
      | esk5_1(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1163) ).

fof(f1165,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk239_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk504_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1165) ).

fof(f1173,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( p(X3)
      | ~ esk37_1(X2)
      | ~ p(X4)
      | ~ esk742_21(X2,X3,X0,X1,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | p(X1)
      | p(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1173) ).

fof(f1181,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
      ( ~ esk279_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk337_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk289_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1181) ).

fof(f1228,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk576_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk574_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1228) ).

fof(f1240,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk473_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk471_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1240) ).

fof(f1254,axiom,
    ! [X0] :
      ( esk45_1(X0)
      | ~ esk5_1(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1254) ).

fof(f1305,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk471_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk274_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1305) ).

fof(f1313,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk686_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk65_5(X0,X1,X2,X3,X4) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1313) ).

fof(f1319,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk653_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk636_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk147_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1319) ).

fof(f1342,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
      ( ~ esk259_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk270_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1342) ).

fof(f1431,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk459_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk239_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1431) ).

fof(f1445,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
      ( ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk337_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1445) ).

fof(f1456,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk750_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk26_1(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1456) ).

fof(f1464,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk655_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk653_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1464) ).

fof(f1499,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk95_5(X0,X1,X2,X3,X4)
      | ~ esk722_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1499) ).

fof(f1514,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk79_5(X0,X1,X2,X3,X4)
      | esk662_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk628_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1514) ).

fof(f1516,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk167_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk583_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1516) ).

fof(f1522,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk655_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk156_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk132_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1522) ).

fof(f1544,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk629_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk640_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1544) ).

fof(f1555,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk707_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk26_1(X0)
      | esk741_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1555) ).

fof(f1573,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk128_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk668_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1573) ).

fof(f1575,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
      ( ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk267_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1575) ).

fof(f1603,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk227_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk203_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk576_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1603) ).

fof(f1677,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk472_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk291_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk280_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1677) ).

fof(f1701,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
      ( esk269_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1701) ).

fof(f1703,axiom,
    esk1_0,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1703) ).

fof(f1724,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk597_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk142_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1724) ).

fof(f1736,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk470_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk504_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk221_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1736) ).

fof(f1758,axiom,
    ! [X2,X3,X0,X1,X4] :
      ( ~ esk58_5(X0,X1,X2,X3,X4)
      | esk109_5(X0,X1,X2,X3,X4) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1758) ).

fof(f1766,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
      ( esk338_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1766) ).

fof(f1780,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ p(X15)
      | ~ esk239_13(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
      | ~ p(X16)
      | ~ esk512_21(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X1,X15,X0,X16,X17,X18,X19,X20)
      | ~ p(X1)
      | ~ p(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1780) ).

fof(f1809,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk721_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk708_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1809) ).

fof(f1811,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
      ( ~ esk280_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk338_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk290_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1811) ).

fof(f1842,axiom,
    ( ~ esk1_0
    | esk3_0 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1842) ).

fof(f1871,axiom,
    ! [X2,X3,X0,X1,X4] :
      ( esk117_5(X0,X1,X2,X3,X4)
      | ~ esk58_5(X0,X1,X2,X3,X4) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1871) ).

fof(f1895,axiom,
    ! [X0] :
      ( esk53_1(X0)
      | ~ esk5_1(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1895) ).

fof(f1900,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk310_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk470_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk471_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1900) ).

fof(f1945,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk549_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk240_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1945) ).

fof(f2006,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
      ( esk259_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2006) ).

fof(f2025,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk750_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk762_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2025) ).

fof(f2128,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk707_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk98_5(X0,X1,X2,X3,X4)
      | esk708_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2128) ).

fof(f2180,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk471_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk472_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2180) ).

fof(f2187,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
      ( esk262_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2187) ).

fof(f2216,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk22_1(X0)
      | ~ esk750_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2216) ).

fof(f2219,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
      ( ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk310_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2219) ).

fof(f2226,axiom,
    ! [X0] :
      ( ~ esk11_1(X0)
      | ~ esk52_1(X0)
      | ~ esk21_1(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2226) ).

fof(f2245,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk596_21(X4,X5,X6,X7,X8,X0,X3,X2,X1,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | p(X3)
      | ~ p(X2)
      | ~ p(X1)
      | ~ p(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2245) ).

fof(f2272,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
      ( ~ esk220_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk210_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk269_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2272) ).

fof(f2275,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
      ( ~ esk188_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk199_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2275) ).

fof(f2281,axiom,
    ! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
      ( ~ esk142_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk132_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk191_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2281) ).

fof(f2287,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
      ( ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk339_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2287) ).

fof(f2297,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk629_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk150_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2297) ).

fof(f2309,axiom,
    ! [X0] :
      ( ~ esk5_1(X0)
      | esk46_1(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2309) ).

fof(f2315,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk685_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk109_5(X0,X1,X2,X3,X4)
      | esk686_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2315) ).

fof(f2328,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk45_1(X0)
      | esk750_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ p(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2328) ).

fof(f2329,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk167_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk645_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2329) ).

fof(f2337,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( p(X4)
      | ~ esk685_21(X3,X2,X0,X4,X1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | p(X2)
      | ~ p(X1)
      | p(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2337) ).

fof(f2339,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
      ( ~ esk332_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk284_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk274_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2339) ).

fof(f2351,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk147_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk640_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk645_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk138_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2351) ).

fof(f2353,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
      ( ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk268_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2353) ).

fof(f2360,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
      ( ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk316_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2360) ).

fof(f2384,axiom,
    ! [X2,X3,X0,X1,X4] :
      ( ~ esk58_5(X0,X1,X2,X3,X4)
      | esk125_5(X0,X1,X2,X3,X4) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2384) ).

fof(f2417,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk583_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk549_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk150_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2417) ).

fof(f2423,axiom,
    ! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
      ( ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk169_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2423) ).

fof(f2486,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk167_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
      | ~ p(X12)
      | ~ p(X11)
      | p(X10)
      | ~ esk590_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X0,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ p(X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2486) ).

fof(f2487,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk199_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk590_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2487) ).

fof(f2491,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk560_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2491) ).

fof(f2495,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk79_5(X0,X1,X2,X3,X4)
      | ~ esk708_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2495) ).

fof(f2503,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
      ( ~ esk281_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk291_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk339_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2503) ).

fof(f2511,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk270_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk512_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2511) ).

fof(f2531,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( esk557_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2531) ).

fof(f2561,axiom,
    ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
      ( ~ esk37_1(X0)
      | ~ esk741_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2561) ).

tcf(c_2620,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
      ( esk191_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    inference(cnf_transformation,[],[f3]) ).

tcf(c_2624,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
      ( esk196_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    inference(cnf_transformation,[],[f7]) ).

tcf(c_2639,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk220_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk516_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f22]) ).

tcf(c_2644,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
      ( ~ esk66_5(X0,X1,X2,X3,X4)
      | ~ esk125_5(X0,X1,X2,X3,X4)
      | ~ esk76_5(X0,X1,X2,X3,X4) ),
    inference(cnf_transformation,[],[f27]) ).

tcf(c_2684,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( ~ esk91_5(X0,X1,X2,X3,X4)
      | ~ esk662_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f67]) ).

tcf(c_2704,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
      ( esk188_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    inference(cnf_transformation,[],[f87]) ).

tcf(c_2734,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk221_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f117]) ).

tcf(c_2755,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk213_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk218_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk537_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk246_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f138]) ).

tcf(c_2766,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk636_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk629_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f149]) ).

tcf(c_2780,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk459_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk227_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk458_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f163]) ).

tcf(c_2787,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk289_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk284_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk458_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk316_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[],[f170]) ).

tcf(c_2829,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk552_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f212]) ).

tcf(c_2838,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i] :
      ( ~ esk208_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk267_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk218_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f221]) ).

tcf(c_2866,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( ~ esk167_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk538_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f249]) ).

tcf(c_2877,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk210_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk219_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk567_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk560_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f260]) ).

tcf(c_2884,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk37_1(X0)
      | ~ esk765_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f267]) ).

tcf(c_2886,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk290_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk279_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk473_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f269]) ).

tcf(c_2944,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( esk328_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[],[f327]) ).

tcf(c_2950,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk239_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk567_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f333]) ).

tcf(c_2963,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i] :
      ( esk246_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f346]) ).

tcf(c_2964,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk434_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk435_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk328_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[],[f347]) ).

tcf(c_2978,plain,
    ! [X0: $i] :
      ( esk52_1(X0)
      | ~ esk5_1(X0) ),
    inference(cnf_transformation,[],[f361]) ).

tcf(c_3034,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i] :
      ( ~ esk262_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk203_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk213_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f417]) ).

tcf(c_3049,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk76_5(X0,X1,X2,X3,X4)
      | ~ esk686_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f432]) ).

tcf(c_3072,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( esk332_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[],[f455]) ).

tcf(c_3093,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk515_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk516_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk257_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f476]) ).

tcf(c_3095,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
      ( ~ esk124_5(X0,X1,X2,X3,X4)
      | ~ esk65_5(X0,X1,X2,X3,X4)
      | ~ esk75_5(X0,X1,X2,X3,X4) ),
    inference(cnf_transformation,[],[f478]) ).

tcf(c_3098,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( p(X6)
      | ~ p(X8)
      | ~ p(X7)
      | ~ p(X5)
      | ~ esk95_5(X0,X1,X2,X3,X4)
      | ~ esk668_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f481]) ).

tcf(c_3114,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
      ( esk98_5(X0,X1,X2,X3,X4)
      | ~ esk58_5(X0,X1,X2,X3,X4) ),
    inference(cnf_transformation,[],[f497]) ).

tcf(c_3155,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk629_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk628_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk169_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    inference(cnf_transformation,[],[f538]) ).

tcf(c_3170,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk209_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk516_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f553]) ).

tcf(c_3207,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
      ( esk57_5(X0,X1,X2,X3,X4)
      | esk58_5(X0,X1,X2,X3,X4)
      | ~ esk46_1(X0) ),
    inference(cnf_transformation,[],[f590]) ).

tcf(c_3218,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk538_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk156_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk537_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f601]) ).

tcf(c_3252,plain,
    ( esk2_0
    | ~ esk1_0 ),
    inference(cnf_transformation,[],[f635]) ).

tcf(c_3285,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
      ( ~ esk197_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk138_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk148_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    inference(cnf_transformation,[],[f668]) ).

tcf(c_3291,plain,
    ! [X0: $i] :
      ( ~ esk2_0
      | ~ esk4_1(X0)
      | ~ p(X0) ),
    inference(cnf_transformation,[],[f674]) ).

tcf(c_3293,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk281_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk435_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f676]) ).

tcf(c_3301,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk208_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk219_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk552_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f684]) ).

tcf(c_3373,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk91_5(X0,X1,X2,X3,X4)
      | ~ esk722_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f756]) ).

tcf(c_3405,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
      ( esk185_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    inference(cnf_transformation,[],[f788]) ).

tcf(c_3433,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk596_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk597_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk185_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    inference(cnf_transformation,[],[f816]) ).

tcf(c_3452,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
      ( esk124_5(X0,X1,X2,X3,X4)
      | ~ esk58_5(X0,X1,X2,X3,X4) ),
    inference(cnf_transformation,[],[f835]) ).

tcf(c_3499,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk11_1(X0)
      | ~ esk750_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f882]) ).

tcf(c_3522,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk148_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk597_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f905]) ).

tcf(c_3538,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( p(X9)
      | ~ p(X12)
      | ~ p(X11)
      | ~ p(X10)
      | ~ esk515_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f921]) ).

tcf(c_3562,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
      ( esk128_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk117_5(X0,X1,X2,X3,X4) ),
    inference(cnf_transformation,[],[f945]) ).

tcf(c_3613,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk742_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk57_5(X0,X1,X2,X3,X4) ),
    inference(cnf_transformation,[],[f996]) ).

tcf(c_3628,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( ~ p(X16)
      | ~ p(X15)
      | ~ p(X14)
      | ~ p(X13)
      | ~ esk434_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1011]) ).

tcf(c_3640,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk137_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk597_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1023]) ).

tcf(c_3674,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
      ( esk197_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    inference(cnf_transformation,[],[f1057]) ).

tcf(c_3676,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i] :
      ( ~ esk209_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk268_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk219_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f1059]) ).

tcf(c_3690,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk75_5(X0,X1,X2,X3,X4)
      | esk66_5(X0,X1,X2,X3,X4)
      | esk722_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk721_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1073]) ).

tcf(c_3714,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk218_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk574_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk557_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1097]) ).

tcf(c_3715,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i] :
      ( esk240_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f1098]) ).

tcf(c_3735,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i] :
      ( esk257_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f1118]) ).

tcf(c_3744,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk12_1(X0)
      | esk21_1(X0)
      | esk765_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk762_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1127]) ).

tcf(c_3749,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
      ( ~ esk137_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk147_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk196_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    inference(cnf_transformation,[],[f1132]) ).

tcf(c_3764,plain,
    ! [X0: $i] :
      ( ~ esk22_1(X0)
      | ~ esk53_1(X0)
      | ~ esk12_1(X0) ),
    inference(cnf_transformation,[],[f1147]) ).

tcf(c_3780,plain,
    ! [X0: $i] :
      ( esk4_1(X0)
      | esk5_1(X0)
      | ~ esk3_0 ),
    inference(cnf_transformation,[],[f1163]) ).

tcf(c_3782,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( ~ esk239_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk504_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1165]) ).

tcf(c_3790,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( p(X3)
      | p(X2)
      | p(X1)
      | ~ p(X4)
      | ~ esk37_1(X0)
      | ~ esk742_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1173]) ).

tcf(c_3798,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( ~ esk337_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk279_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk289_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[],[f1181]) ).

tcf(c_3845,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk576_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk574_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1228]) ).

tcf(c_3857,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk473_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk471_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1240]) ).

tcf(c_3871,plain,
    ! [X0: $i] :
      ( esk45_1(X0)
      | ~ esk5_1(X0) ),
    inference(cnf_transformation,[],[f1254]) ).

tcf(c_3922,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk274_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk471_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1305]) ).

tcf(c_3930,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk65_5(X0,X1,X2,X3,X4)
      | ~ esk686_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1313]) ).

tcf(c_3936,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk147_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk653_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk636_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1319]) ).

tcf(c_3959,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( esk270_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk259_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f1342]) ).

tcf(c_4048,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( ~ esk239_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk459_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1431]) ).

tcf(c_4062,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( esk337_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[],[f1445]) ).

tcf(c_4073,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk26_1(X0)
      | ~ esk750_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1456]) ).

tcf(c_4081,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk655_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk653_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1464]) ).

tcf(c_4116,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk95_5(X0,X1,X2,X3,X4)
      | ~ esk722_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1499]) ).

tcf(c_4131,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk662_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk79_5(X0,X1,X2,X3,X4)
      | ~ esk628_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1514]) ).

tcf(c_4133,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( ~ esk167_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk583_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1516]) ).

tcf(c_4139,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk156_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk132_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk655_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1522]) ).

tcf(c_4161,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk640_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk629_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1544]) ).

tcf(c_4172,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk741_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk26_1(X0)
      | ~ esk707_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1555]) ).

tcf(c_4190,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk668_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk128_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    inference(cnf_transformation,[],[f1573]) ).

tcf(c_4192,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i] :
      ( esk267_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f1575]) ).

tcf(c_4220,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk203_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk227_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk576_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1603]) ).

tcf(c_4294,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk280_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk291_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk472_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1677]) ).

tcf(c_4318,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i] :
      ( esk269_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f1701]) ).

tcf(c_4320,plain,
    esk1_0,
    inference(cnf_transformation,[],[f1703]) ).

tcf(c_4341,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk142_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk597_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1724]) ).

tcf(c_4353,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk504_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk221_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk470_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1736]) ).

tcf(c_4375,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
      ( esk109_5(X0,X1,X2,X3,X4)
      | ~ esk58_5(X0,X1,X2,X3,X4) ),
    inference(cnf_transformation,[],[f1758]) ).

tcf(c_4383,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( esk338_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[],[f1766]) ).

tcf(c_4397,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( ~ p(X16)
      | ~ p(X15)
      | ~ p(X14)
      | ~ p(X13)
      | ~ esk239_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk512_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1780]) ).

tcf(c_4426,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk721_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk708_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f1809]) ).

tcf(c_4428,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( ~ esk280_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk338_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk290_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[],[f1811]) ).

tcf(c_4459,plain,
    ( esk3_0
    | ~ esk1_0 ),
    inference(cnf_transformation,[],[f1842]) ).

tcf(c_4488,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
      ( esk117_5(X0,X1,X2,X3,X4)
      | ~ esk58_5(X0,X1,X2,X3,X4) ),
    inference(cnf_transformation,[],[f1871]) ).

tcf(c_4512,plain,
    ! [X0: $i] :
      ( esk53_1(X0)
      | ~ esk5_1(X0) ),
    inference(cnf_transformation,[],[f1895]) ).

tcf(c_4517,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk470_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk471_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk310_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[],[f1900]) ).

tcf(c_4562,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk549_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk240_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f1945]) ).

tcf(c_4623,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i] :
      ( esk259_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f2006]) ).

tcf(c_4642,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk762_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk750_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f2025]) ).

tcf(c_4745,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk707_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk708_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk98_5(X0,X1,X2,X3,X4) ),
    inference(cnf_transformation,[],[f2128]) ).

tcf(c_4797,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk472_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk471_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f2180]) ).

tcf(c_4804,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i] :
      ( esk262_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f2187]) ).

tcf(c_4833,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk22_1(X0)
      | ~ esk750_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f2216]) ).

tcf(c_4836,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( esk310_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[],[f2219]) ).

tcf(c_4843,plain,
    ! [X0: $i] :
      ( ~ esk11_1(X0)
      | ~ esk52_1(X0)
      | ~ esk21_1(X0) ),
    inference(cnf_transformation,[],[f2226]) ).

tcf(c_4862,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( p(X6)
      | ~ p(X8)
      | ~ p(X7)
      | ~ p(X5)
      | ~ esk596_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f2245]) ).

tcf(c_4889,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i] :
      ( ~ esk269_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk210_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk220_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f2272]) ).

tcf(c_4892,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i] :
      ( esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk199_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk188_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    inference(cnf_transformation,[],[f2275]) ).

tcf(c_4898,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
      ( ~ esk132_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk142_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk191_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    inference(cnf_transformation,[],[f2281]) ).

tcf(c_4904,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( esk339_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[],[f2287]) ).

tcf(c_4914,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk150_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk629_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f2297]) ).

tcf(c_4926,plain,
    ! [X0: $i] :
      ( esk46_1(X0)
      | ~ esk5_1(X0) ),
    inference(cnf_transformation,[],[f2309]) ).

tcf(c_4932,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk685_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk686_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk109_5(X0,X1,X2,X3,X4) ),
    inference(cnf_transformation,[],[f2315]) ).

tcf(c_4945,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk750_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk45_1(X0)
      | ~ p(X0) ),
    inference(cnf_transformation,[],[f2328]) ).

tcf(c_4946,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk167_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk645_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f2329]) ).

tcf(c_4954,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( p(X3)
      | p(X2)
      | p(X1)
      | ~ p(X4)
      | ~ esk685_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f2337]) ).

tcf(c_4956,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( ~ esk332_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk284_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk274_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[],[f2339]) ).

tcf(c_4968,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk138_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk147_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk645_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk640_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f2351]) ).

tcf(c_4970,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i] :
      ( esk268_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f2353]) ).

tcf(c_4977,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( esk316_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[],[f2360]) ).

tcf(c_5001,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
      ( esk125_5(X0,X1,X2,X3,X4)
      | ~ esk58_5(X0,X1,X2,X3,X4) ),
    inference(cnf_transformation,[],[f2384]) ).

tcf(c_5034,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk583_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk150_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk549_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f2417]) ).

tcf(c_5040,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
      ( esk169_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    inference(cnf_transformation,[],[f2423]) ).

tcf(c_5103,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( p(X9)
      | ~ p(X12)
      | ~ p(X11)
      | ~ p(X10)
      | ~ esk167_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk590_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f2486]) ).

tcf(c_5104,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk590_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk199_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(cnf_transformation,[],[f2487]) ).

tcf(c_5108,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk560_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f2491]) ).

tcf(c_5112,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk79_5(X0,X1,X2,X3,X4)
      | ~ esk708_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f2495]) ).

tcf(c_5120,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( ~ esk291_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk339_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk281_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[],[f2503]) ).

tcf(c_5128,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk512_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk270_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[],[f2511]) ).

tcf(c_5148,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk557_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f2531]) ).

tcf(c_5178,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( ~ esk37_1(X0)
      | ~ esk741_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(cnf_transformation,[],[f2561]) ).

tcf(c_7437,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( ~ esk239_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk512_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,true,true,true,true,X13,X14,X15,X16) ),
    inference(domain_res,[status(esa)],[c_4397]) ).

tcf(c_7448,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( ~ esk167_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk590_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,false,true,true,true,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(domain_res,[status(esa)],[c_5103]) ).

tcf(c_7454,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( ~ esk95_5(X0,X1,X2,X3,X4)
      | ~ esk668_21(X0,X1,X2,X3,X4,true,false,true,true,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(domain_res,[status(esa)],[c_3098]) ).

tcf(c_7469,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] : ~ esk434_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,true,true,true,true,X13,X14,X15,X16),
    inference(domain_res,[status(esa)],[c_3628]) ).

tcf(c_7470,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( ~ esk37_1(X0)
      | ~ esk742_21(X0,false,false,false,true,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(domain_res,[status(esa)],[c_3790]) ).

tcf(c_7479,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] : ~ esk515_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,false,true,true,true,X9,X10,X11,X12,X13,X14,X15,X16),
    inference(domain_res,[status(esa)],[c_3538]) ).

tcf(c_7487,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] : ~ esk596_21(X0,X1,X2,X3,X4,true,false,true,true,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16),
    inference(domain_res,[status(esa)],[c_4862]) ).

tcf(c_7507,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] : ~ esk685_21(X0,false,false,false,true,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16),
    inference(domain_res,[status(esa)],[c_4954]) ).

tcf(c_7509,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i] :
      ( esk750_21(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
      | ~ esk45_1(true) ),
    inference(domain_res,[status(esa)],[c_4945]) ).

tcf(c_7830,plain,
    ( ~ esk2_0
    | ~ esk4_1(true) ),
    inference(domain_res,[status(esa)],[c_3291]) ).

tcf(c_8115,plain,
    esk2_0,
    inference(forward_subsumption_resolution,[status(thm)],[c_3252,c_4320]) ).

tcf(c_8116,plain,
    esk3_0,
    inference(forward_subsumption_resolution,[status(thm)],[c_4459,c_4320]) ).

tcf(c_8243,plain,
    ~ esk4_1(true),
    inference(forward_subsumption_resolution,[status(thm)],[c_7830,c_8115]) ).

tcf(c_8244,plain,
    ! [X0: $i] :
      ( esk4_1(X0)
      | esk5_1(X0) ),
    inference(forward_subsumption_resolution,[status(thm)],[c_3780,c_8116]) ).

tcf(c_19224,plain,
    esk5_1(true),
    inference(resolution,[status(thm)],[c_8244,c_8243]) ).

tcf(c_19367,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( esk516_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,false,true,true,true,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk257_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,false,true,true,true) ),
    inference(resolution,[status(thm)],[c_3093,c_7479]) ).

tcf(c_19703,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( esk435_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,true,true,true,true,X13,X14,X15,X16)
      | ~ esk328_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,true,true,true,true) ),
    inference(resolution,[status(thm)],[c_2964,c_7469]) ).

tcf(c_20440,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( esk686_21(X0,false,false,false,true,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk109_5(X0,false,false,false,true) ),
    inference(resolution,[status(thm)],[c_4932,c_7507]) ).

tcf(c_20475,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( esk597_21(X0,X1,X2,X3,X4,true,false,true,true,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk185_9(X0,X1,X2,X3,X4,true,false,true,true) ),
    inference(resolution,[status(thm)],[c_3433,c_7487]) ).

tcf(c_23739,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i] :
      ( esk750_21(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
      | ~ esk5_1(true) ),
    inference(resolution,[status(thm)],[c_3871,c_7509]) ).

tcf(c_23741,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i] : esk750_21(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
    inference(global_subsumption_just,[status(thm)],[c_23739,c_19224,c_23739]) ).

tcf(c_23829,plain,
    ! [X0: $i] :
      ( ~ esk5_1(X0)
      | ~ esk11_1(X0)
      | ~ esk21_1(X0) ),
    inference(resolution,[status(thm)],[c_2978,c_4843]) ).

tcf(c_24057,plain,
    ! [X0: $i] :
      ( ~ esk22_1(X0)
      | ~ esk12_1(X0)
      | ~ esk5_1(X0) ),
    inference(resolution,[status(thm)],[c_4512,c_3764]) ).

tcf(c_24276,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i] :
      ( esk281_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,true,true,true,true)
      | ~ esk328_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,true,true,true,true) ),
    inference(resolution,[status(thm)],[c_3293,c_19703]) ).

tcf(c_24663,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk583_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk150_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk240_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(resolution,[status(thm)],[c_4562,c_5034]) ).

tcf(c_24713,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk629_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk662_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk79_5(X0,X1,X2,X3,X4)
      | ~ esk169_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    inference(resolution,[status(thm)],[c_3155,c_4131]) ).

tcf(c_24807,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk741_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk708_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk26_1(X0)
      | ~ esk98_5(X0,X1,X2,X3,X4) ),
    inference(resolution,[status(thm)],[c_4745,c_4172]) ).

tcf(c_24839,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk504_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | esk471_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk221_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk310_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(resolution,[status(thm)],[c_4517,c_4353]) ).

tcf(c_28290,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk213_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk218_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk538_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk156_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk246_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
    inference(resolution,[status(thm)],[c_2755,c_3218]) ).

tcf(c_28406,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk289_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk284_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | esk459_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk227_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk316_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(resolution,[status(thm)],[c_2787,c_2780]) ).

tcf(c_30046,plain,
    ( ~ esk22_1(true)
    | ~ esk12_1(true) ),
    inference(resolution,[status(thm)],[c_24057,c_19224]) ).

tcf(c_30074,plain,
    ( ~ esk11_1(true)
    | ~ esk21_1(true) ),
    inference(resolution,[status(thm)],[c_23829,c_19224]) ).

tcf(c_30088,plain,
    esk46_1(true),
    inference(resolution,[status(thm)],[c_4926,c_19224]) ).

tcf(c_30468,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i] :
      ( ~ esk21_1(true)
      | ~ esk750_21(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(resolution,[status(thm)],[c_3499,c_30074]) ).

tcf(c_30554,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i] :
      ( ~ esk12_1(true)
      | ~ esk750_21(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(resolution,[status(thm)],[c_4833,c_30046]) ).

tcf(c_30556,plain,
    ~ esk12_1(true),
    inference(global_subsumption_just,[status(thm)],[c_30554,c_19224,c_23739,c_30554]) ).

tcf(c_34495,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk75_5(X0,X1,X2,X3,X4)
      | esk66_5(X0,X1,X2,X3,X4)
      | esk95_5(X0,X1,X2,X3,X4)
      | ~ esk721_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(resolution,[status(thm)],[c_3690,c_4116]) ).

tcf(c_34509,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk75_5(X0,X1,X2,X3,X4)
      | esk66_5(X0,X1,X2,X3,X4)
      | esk91_5(X0,X1,X2,X3,X4)
      | ~ esk721_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(resolution,[status(thm)],[c_3690,c_3373]) ).

tcf(c_34720,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk12_1(X0)
      | esk21_1(X0)
      | esk37_1(X0)
      | ~ esk762_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(resolution,[status(thm)],[c_3744,c_2884]) ).

tcf(c_35216,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk210_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk239_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk219_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk560_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(resolution,[status(thm)],[c_2877,c_2950]) ).

tcf(c_35520,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk138_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk147_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk167_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk640_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(resolution,[status(thm)],[c_4968,c_4946]) ).

tcf(c_35690,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
      ( esk209_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,false,true,true,true)
      | ~ esk257_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,false,true,true,true) ),
    inference(resolution,[status(thm)],[c_3170,c_19367]) ).

tcf(c_35698,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
      ( esk220_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,false,true,true,true)
      | ~ esk257_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,false,true,true,true) ),
    inference(resolution,[status(thm)],[c_2639,c_19367]) ).

tcf(c_36090,plain,
    ! [X0: $i] :
      ( esk65_5(X0,false,false,false,true)
      | ~ esk109_5(X0,false,false,false,true) ),
    inference(resolution,[status(thm)],[c_3930,c_20440]) ).

tcf(c_36106,plain,
    ! [X0: $i] :
      ( esk76_5(X0,false,false,false,true)
      | ~ esk109_5(X0,false,false,false,true) ),
    inference(resolution,[status(thm)],[c_3049,c_20440]) ).

tcf(c_36497,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
      ( esk142_9(X0,X1,X2,X3,X4,true,false,true,true)
      | ~ esk185_9(X0,X1,X2,X3,X4,true,false,true,true) ),
    inference(resolution,[status(thm)],[c_4341,c_20475]) ).

tcf(c_36506,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
      ( esk137_9(X0,X1,X2,X3,X4,true,false,true,true)
      | ~ esk185_9(X0,X1,X2,X3,X4,true,false,true,true) ),
    inference(resolution,[status(thm)],[c_3640,c_20475]) ).

tcf(c_36514,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
      ( esk148_9(X0,X1,X2,X3,X4,true,false,true,true)
      | ~ esk185_9(X0,X1,X2,X3,X4,true,false,true,true) ),
    inference(resolution,[status(thm)],[c_3522,c_20475]) ).

tcf(c_39303,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk203_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk227_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk574_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(resolution,[status(thm)],[c_3845,c_4220]) ).

tcf(c_40825,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk156_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk132_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk653_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(resolution,[status(thm)],[c_4081,c_4139]) ).

tcf(c_43503,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i] :
      ( esk21_1(true)
      | esk37_1(true)
      | ~ esk762_21(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(resolution,[status(thm)],[c_34720,c_30556]) ).

tcf(c_53768,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk203_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk227_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | esk218_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
      | ~ esk557_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(resolution,[status(thm)],[c_3714,c_39303]) ).

tcf(c_54767,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk156_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk147_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | esk132_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
      | ~ esk636_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
    inference(resolution,[status(thm)],[c_3936,c_40825]) ).

tcf(c_94501,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i] :
      ( esk708_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
      | ~ esk26_1(X0)
      | ~ esk37_1(X0)
      | ~ esk98_5(X0,X1,X2,X3,X4) ),
    inference(resolution,[status(thm)],[c_24807,c_5178]) ).

tcf(c_132177,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i] : esk762_21(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
    inference(resolution,[status(thm)],[c_4642,c_23741]) ).

tcf(c_132192,plain,
    esk26_1(true),
    inference(resolution,[status(thm)],[c_4073,c_23741]) ).

tcf(c_303697,plain,
    ! [X0: $i] :
      ( esk109_5(X0,false,false,false,true)
      | ~ esk58_5(X0,false,false,false,true) ),
    inference(instantiation,[status(thm)],[c_4375]) ).

tcf(c_303761,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
      ( esk742_21(X0,false,false,false,true,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ esk57_5(X0,false,false,false,true) ),
    inference(instantiation,[status(thm)],[c_3613]) ).

tcf(c_303787,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i] :
      ( esk708_21(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
      | ~ esk26_1(true)
      | ~ esk37_1(true)
      | ~ esk98_5(true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_94501]) ).

tcf(c_303928,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i] :
      ( ~ esk37_1(true)
      | ~ esk742_21(true,false,false,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
    inference(instantiation,[status(thm)],[c_7470]) ).

tcf(c_303989,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( esk98_5(true,X0,X1,X2,X3)
      | ~ esk58_5(true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_3114]) ).

tcf(c_304049,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i] :
      ( esk742_21(true,false,false,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      | ~ esk57_5(true,false,false,false,true) ),
    inference(instantiation,[status(thm)],[c_303761]) ).

tcf(c_304092,plain,
    ( esk57_5(true,false,false,false,true)
    | esk58_5(true,false,false,false,true)
    | ~ esk46_1(true) ),
    inference(instantiation,[status(thm)],[c_3207]) ).

tcf(c_304111,plain,
    ( esk98_5(true,false,false,false,true)
    | ~ esk58_5(true,false,false,false,true) ),
    inference(instantiation,[status(thm)],[c_303989]) ).

tcf(c_304113,plain,
    ( esk109_5(true,false,false,false,true)
    | ~ esk58_5(true,false,false,false,true) ),
    inference(instantiation,[status(thm)],[c_303697]) ).

tcf(c_304159,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i] :
      ( esk708_21(true,false,false,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      | ~ esk26_1(true)
      | ~ esk37_1(true)
      | ~ esk98_5(true,false,false,false,true) ),
    inference(instantiation,[status(thm)],[c_303787]) ).

tcf(c_304167,plain,
    ( esk76_5(true,false,false,false,true)
    | ~ esk109_5(true,false,false,false,true) ),
    inference(instantiation,[status(thm)],[c_36106]) ).

tcf(c_304169,plain,
    ( esk65_5(true,false,false,false,true)
    | ~ esk109_5(true,false,false,false,true) ),
    inference(instantiation,[status(thm)],[c_36090]) ).

tcf(c_304272,plain,
    ( ~ esk124_5(true,false,false,false,true)
    | ~ esk65_5(true,false,false,false,true)
    | ~ esk75_5(true,false,false,false,true) ),
    inference(instantiation,[status(thm)],[c_3095]) ).

tcf(c_304350,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i] :
      ( esk721_21(true,false,false,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      | ~ esk708_21(true,false,false,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
    inference(instantiation,[status(thm)],[c_4426]) ).

tcf(c_304361,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i] :
      ( esk79_5(true,false,false,false,true)
      | ~ esk708_21(true,false,false,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
    inference(instantiation,[status(thm)],[c_5112]) ).

tcf(c_304418,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( esk124_5(true,X0,X1,X2,X3)
      | ~ esk58_5(true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_3452]) ).

tcf(c_304651,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i] :
      ( esk75_5(true,false,false,false,true)
      | esk66_5(true,false,false,false,true)
      | esk91_5(true,false,false,false,true)
      | ~ esk721_21(true,false,false,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
    inference(instantiation,[status(thm)],[c_34509]) ).

tcf(c_304652,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i] :
      ( esk75_5(true,false,false,false,true)
      | esk66_5(true,false,false,false,true)
      | esk95_5(true,false,false,false,true)
      | ~ esk721_21(true,false,false,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
    inference(instantiation,[status(thm)],[c_34495]) ).

tcf(c_304948,plain,
    ( esk124_5(true,false,false,false,true)
    | ~ esk58_5(true,false,false,false,true) ),
    inference(instantiation,[status(thm)],[c_304418]) ).

tcf(c_305165,plain,
    ( ~ esk66_5(true,false,false,false,true)
    | ~ esk125_5(true,false,false,false,true)
    | ~ esk76_5(true,false,false,false,true) ),
    inference(instantiation,[status(thm)],[c_2644]) ).

tcf(c_305330,plain,
    ( esk117_5(true,false,false,false,true)
    | ~ esk58_5(true,false,false,false,true) ),
    inference(instantiation,[status(thm)],[c_4488]) ).

tcf(c_305333,plain,
    ( esk125_5(true,false,false,false,true)
    | ~ esk58_5(true,false,false,false,true) ),
    inference(instantiation,[status(thm)],[c_5001]) ).

tcf(c_305604,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
      ( ~ esk95_5(true,false,false,false,true)
      | ~ esk668_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11) ),
    inference(instantiation,[status(thm)],[c_7454]) ).

tcf(c_305727,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
      ( esk185_9(X0,X1,X2,X3,X4,true,false,true,true)
      | ~ esk129_9(X0,X1,X2,X3,X4,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_3405]) ).

tcf(c_305740,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
      ( esk257_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,false,true,true,true)
      | ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_3735]) ).

tcf(c_305785,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
      ( esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,false,true,true,true)
      | esk199_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,false,true,true,true)
      | ~ esk188_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
    inference(instantiation,[status(thm)],[c_4892]) ).

tcf(c_306040,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i] :
      ( esk629_21(true,false,false,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      | esk662_21(true,false,false,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      | ~ esk79_5(true,false,false,false,true)
      | ~ esk169_9(true,false,false,false,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_24713]) ).

tcf(c_306286,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( esk169_9(true,false,false,false,true,X0,X1,X2,X3)
      | ~ esk129_9(true,false,false,false,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_5040]) ).

tcf(c_306340,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
      ( esk668_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11)
      | ~ esk128_9(true,false,false,false,true,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_4190]) ).

tcf(c_306448,plain,
    ( esk128_9(true,false,false,false,true,true,false,true,true)
    | esk129_9(true,false,false,false,true,true,false,true,true)
    | ~ esk117_5(true,false,false,false,true) ),
    inference(instantiation,[status(thm)],[c_3562]) ).

tcf(c_306478,plain,
    ( esk185_9(true,false,false,false,true,true,false,true,true)
    | ~ esk129_9(true,false,false,false,true,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_305727]) ).

tcf(c_306482,plain,
    ( esk169_9(true,false,false,false,true,true,false,true,true)
    | ~ esk129_9(true,false,false,false,true,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_306286]) ).

tcf(c_306593,plain,
    ( esk148_9(true,false,false,false,true,true,false,true,true)
    | ~ esk185_9(true,false,false,false,true,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_36514]) ).

tcf(c_306594,plain,
    ( esk137_9(true,false,false,false,true,true,false,true,true)
    | ~ esk185_9(true,false,false,false,true,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_36506]) ).

tcf(c_306595,plain,
    ( esk142_9(true,false,false,false,true,true,false,true,true)
    | ~ esk185_9(true,false,false,false,true,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_36497]) ).

tcf(c_306603,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
      ( esk629_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11)
      | esk662_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11)
      | ~ esk79_5(true,false,false,false,true)
      | ~ esk169_9(true,false,false,false,true,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_306040]) ).

tcf(c_306768,plain,
    ( ~ esk137_9(true,false,false,false,true,true,false,true,true)
    | ~ esk147_9(true,false,false,false,true,true,false,true,true)
    | ~ esk196_9(true,false,false,false,true,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_3749]) ).

tcf(c_306917,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
      ( ~ esk91_5(true,false,false,false,true)
      | ~ esk662_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11) ),
    inference(instantiation,[status(thm)],[c_2684]) ).

tcf(c_306953,plain,
    ( esk196_9(true,false,false,false,true,true,false,true,true)
    | ~ esk129_9(true,false,false,false,true,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_2624]) ).

tcf(c_307173,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
      ( esk640_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11)
      | ~ esk629_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11) ),
    inference(instantiation,[status(thm)],[c_4161]) ).

tcf(c_307182,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
      ( esk636_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11)
      | ~ esk629_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11) ),
    inference(instantiation,[status(thm)],[c_2766]) ).

tcf(c_307183,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
      ( esk150_9(true,false,false,false,true,true,false,true,true)
      | ~ esk629_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11) ),
    inference(instantiation,[status(thm)],[c_4914]) ).

tcf(c_307230,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
      ( esk156_9(true,false,false,false,true,true,false,true,true)
      | esk147_9(true,false,false,false,true,true,false,true,true)
      | esk132_9(true,false,false,false,true,true,false,true,true)
      | ~ esk636_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11) ),
    inference(instantiation,[status(thm)],[c_54767]) ).

tcf(c_307231,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
      ( esk138_9(true,false,false,false,true,true,false,true,true)
      | esk147_9(true,false,false,false,true,true,false,true,true)
      | esk167_9(true,false,false,false,true,true,false,true,true)
      | ~ esk640_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11) ),
    inference(instantiation,[status(thm)],[c_35520]) ).

tcf(c_307609,plain,
    ( ~ esk132_9(true,false,false,false,true,true,false,true,true)
    | ~ esk142_9(true,false,false,false,true,true,false,true,true)
    | ~ esk191_9(true,false,false,false,true,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_4898]) ).

tcf(c_307616,plain,
    ( ~ esk197_9(true,false,false,false,true,true,false,true,true)
    | ~ esk138_9(true,false,false,false,true,true,false,true,true)
    | ~ esk148_9(true,false,false,false,true,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_3285]) ).

tcf(c_307905,plain,
    ( esk197_9(true,false,false,false,true,true,false,true,true)
    | ~ esk129_9(true,false,false,false,true,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_3674]) ).

tcf(c_308144,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
      ( ~ esk167_9(true,false,false,false,true,true,false,true,true)
      | ~ esk583_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11) ),
    inference(instantiation,[status(thm)],[c_4133]) ).

tcf(c_308151,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( ~ esk167_9(true,false,false,false,true,true,false,true,true)
      | ~ esk590_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7) ),
    inference(instantiation,[status(thm)],[c_7448]) ).

tcf(c_308353,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( esk590_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7)
      | ~ esk199_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_5104]) ).

tcf(c_308593,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
      ( esk583_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11)
      | esk550_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11)
      | ~ esk150_9(true,false,false,false,true,true,false,true,true)
      | ~ esk240_13(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_24663]) ).

tcf(c_308617,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
      ( esk213_13(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3)
      | esk218_13(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3)
      | esk538_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11)
      | ~ esk156_9(true,false,false,false,true,true,false,true,true)
      | ~ esk246_13(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_28290]) ).

tcf(c_308740,plain,
    ( esk200_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | esk199_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk188_9(true,false,false,false,true,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_305785]) ).

tcf(c_309294,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( esk240_13(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3)
      | ~ esk200_13(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_3715]) ).

tcf(c_309406,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( esk246_13(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3)
      | ~ esk200_13(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_2963]) ).

tcf(c_309437,plain,
    ( esk188_9(true,false,false,false,true,true,false,true,true)
    | ~ esk129_9(true,false,false,false,true,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_2704]) ).

tcf(c_310015,plain,
    ( esk257_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk200_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_305740]) ).

tcf(c_310016,plain,
    ( esk246_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk200_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_309406]) ).

tcf(c_310020,plain,
    ( esk240_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk200_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_309294]) ).

tcf(c_310251,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( esk259_13(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3)
      | ~ esk200_13(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_4623]) ).

tcf(c_310292,plain,
    ( esk220_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk257_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_35698]) ).

tcf(c_310293,plain,
    ( esk209_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk257_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_35690]) ).

tcf(c_310295,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( esk213_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | esk218_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | esk538_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7)
      | ~ esk156_9(true,false,false,false,true,true,false,true,true)
      | ~ esk246_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_308617]) ).

tcf(c_310301,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( esk583_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7)
      | esk550_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7)
      | ~ esk150_9(true,false,false,false,true,true,false,true,true)
      | ~ esk240_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_308593]) ).

tcf(c_310461,plain,
    ( esk259_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk200_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_310251]) ).

tcf(c_310803,plain,
    ( ~ esk209_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk268_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk219_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_3676]) ).

tcf(c_310911,plain,
    ( esk191_9(true,false,false,false,true,true,false,true,true)
    | ~ esk129_9(true,false,false,false,true,true,false,true,true) ),
    inference(instantiation,[status(thm)],[c_2620]) ).

tcf(c_310942,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( esk557_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7)
      | ~ esk550_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7) ),
    inference(instantiation,[status(thm)],[c_5148]) ).

tcf(c_310943,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( esk560_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7)
      | ~ esk550_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7) ),
    inference(instantiation,[status(thm)],[c_5108]) ).

tcf(c_310951,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( esk552_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7)
      | ~ esk550_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7) ),
    inference(instantiation,[status(thm)],[c_2829]) ).

tcf(c_310956,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( esk221_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | ~ esk550_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7) ),
    inference(instantiation,[status(thm)],[c_2734]) ).

tcf(c_311585,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( ~ esk167_9(true,false,false,false,true,true,false,true,true)
      | ~ esk583_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7) ),
    inference(instantiation,[status(thm)],[c_308144]) ).

tcf(c_312174,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( esk203_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | esk227_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | esk218_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | ~ esk557_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7) ),
    inference(instantiation,[status(thm)],[c_53768]) ).

tcf(c_312489,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( esk210_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | esk239_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | esk219_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | ~ esk560_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7) ),
    inference(instantiation,[status(thm)],[c_35216]) ).

tcf(c_312524,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( esk208_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | esk219_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | ~ esk552_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7) ),
    inference(instantiation,[status(thm)],[c_3301]) ).

tcf(c_313181,plain,
    ( esk268_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk200_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_4970]) ).

tcf(c_314539,plain,
    ( ~ esk269_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk210_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk220_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_4889]) ).

tcf(c_314548,plain,
    ( ~ esk208_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk267_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk218_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_2838]) ).

tcf(c_316379,plain,
    ( esk269_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk200_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_4318]) ).

tcf(c_316383,plain,
    ( esk267_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk200_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_4192]) ).

tcf(c_318086,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
      ( ~ esk167_9(true,false,false,false,true,true,false,true,true)
      | ~ esk538_21(true,false,false,false,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11) ),
    inference(instantiation,[status(thm)],[c_2866]) ).

tcf(c_321036,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( ~ esk239_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | ~ esk459_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7) ),
    inference(instantiation,[status(thm)],[c_4048]) ).

tcf(c_321039,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( ~ esk239_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | ~ esk504_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7) ),
    inference(instantiation,[status(thm)],[c_3782]) ).

tcf(c_321042,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( ~ esk239_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | ~ esk512_21(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_7437]) ).

tcf(c_321363,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( esk512_21(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3)
      | ~ esk270_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true) ),
    inference(instantiation,[status(thm)],[c_5128]) ).

tcf(c_321586,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( esk289_17(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3)
      | esk284_17(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3)
      | esk459_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7)
      | ~ esk227_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | ~ esk316_17(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_28406]) ).

tcf(c_321598,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( esk504_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7)
      | esk471_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7)
      | ~ esk221_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | ~ esk310_17(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_24839]) ).

tcf(c_321808,plain,
    ( esk270_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | esk271_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk259_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_3959]) ).

tcf(c_322642,plain,
    ( esk262_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk200_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_4804]) ).

tcf(c_322746,plain,
    ( esk316_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk271_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true) ),
    inference(instantiation,[status(thm)],[c_4977]) ).

tcf(c_322748,plain,
    ( esk339_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk271_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true) ),
    inference(instantiation,[status(thm)],[c_4904]) ).

tcf(c_322749,plain,
    ( esk310_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk271_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true) ),
    inference(instantiation,[status(thm)],[c_4836]) ).

tcf(c_322753,plain,
    ( esk338_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk271_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true) ),
    inference(instantiation,[status(thm)],[c_4383]) ).

tcf(c_322757,plain,
    ( esk337_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk271_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true) ),
    inference(instantiation,[status(thm)],[c_4062]) ).

tcf(c_322768,plain,
    ( esk332_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk271_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true) ),
    inference(instantiation,[status(thm)],[c_3072]) ).

tcf(c_322769,plain,
    ( esk328_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk271_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true) ),
    inference(instantiation,[status(thm)],[c_2944]) ).

tcf(c_323832,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( esk289_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
      | esk284_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
      | esk459_21(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3)
      | ~ esk227_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | ~ esk316_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true) ),
    inference(instantiation,[status(thm)],[c_321586]) ).

tcf(c_323834,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( esk504_21(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3)
      | esk471_21(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3)
      | ~ esk221_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | ~ esk310_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true) ),
    inference(instantiation,[status(thm)],[c_321598]) ).

tcf(c_323846,plain,
    ( esk281_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk328_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true) ),
    inference(instantiation,[status(thm)],[c_24276]) ).

tcf(c_325040,plain,
    ( ~ esk291_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk339_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk281_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true) ),
    inference(instantiation,[status(thm)],[c_5120]) ).

tcf(c_325592,plain,
    ( ~ esk262_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk203_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
    | ~ esk213_13(true,false,false,false,true,true,false,true,true,false,true,true,true) ),
    inference(instantiation,[status(thm)],[c_3034]) ).

tcf(c_325646,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( ~ esk239_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | ~ esk504_21(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_321039]) ).

tcf(c_326451,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( esk280_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
      | esk291_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
      | ~ esk472_21(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_4294]) ).

tcf(c_326924,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( esk472_21(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3)
      | ~ esk471_21(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_4797]) ).

tcf(c_326927,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( esk473_21(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3)
      | ~ esk471_21(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_3857]) ).

tcf(c_326932,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( esk274_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
      | ~ esk471_21(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_3922]) ).

tcf(c_328525,plain,
    ( ~ esk280_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk338_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk290_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true) ),
    inference(instantiation,[status(thm)],[c_4428]) ).

tcf(c_328728,plain,
    ( ~ esk332_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk284_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk274_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true) ),
    inference(instantiation,[status(thm)],[c_4956]) ).

tcf(c_329316,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
      ( ~ esk167_9(true,false,false,false,true,true,false,true,true)
      | ~ esk538_21(true,false,false,false,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7) ),
    inference(instantiation,[status(thm)],[c_318086]) ).

tcf(c_329446,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( esk290_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
      | esk279_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
      | ~ esk473_21(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_2886]) ).

tcf(c_331256,plain,
    ( ~ esk337_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk279_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true)
    | ~ esk289_17(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true) ),
    inference(instantiation,[status(thm)],[c_3798]) ).

tcf(c_331965,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( ~ esk239_13(true,false,false,false,true,true,false,true,true,false,true,true,true)
      | ~ esk459_21(true,false,false,false,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3) ),
    inference(instantiation,[status(thm)],[c_321036]) ).

tcf(c_331966,plain,
    $false,
    inference(prop_impl_just,[status(thm)],[c_331965,c_331256,c_329446,c_329316,c_328728,c_328525,c_326924,c_326927,c_326932,c_326451,c_325646,c_325592,c_325040,c_323846,c_323834,c_323832,c_322746,c_322748,c_322749,c_322753,c_322757,c_322768,c_322769,c_322642,c_321808,c_321363,c_321042,c_316383,c_316379,c_314548,c_314539,c_313181,c_312524,c_312489,c_312174,c_311585,c_310942,c_310943,c_310951,c_310956,c_310911,c_310803,c_310461,c_310301,c_310295,c_310292,c_310293,c_310016,c_310020,c_310015,c_309437,c_308740,c_308353,c_308151,c_307905,c_307616,c_307609,c_307230,c_307231,c_307173,c_307182,c_307183,c_306953,c_306917,c_306768,c_306603,c_306593,c_306594,c_306595,c_306482,c_306478,c_306448,c_306340,c_305604,c_305333,c_305330,c_305165,c_304948,c_304651,c_304652,c_304350,c_304361,c_304272,c_304167,c_304169,c_304159,c_304113,c_304111,c_304092,c_304049,c_303928,c_132192,c_132177,c_43503,c_30468,c_30088,c_23739,c_19224]) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05  % Problem  : SYO588-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 0.00/0.07  % Command  : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.20/0.45  % Computer : n005.cluster.edu
% 0.20/0.45  % Model    : x86_64 x86_64
% 0.20/0.45  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45  % Memory   : 8046.5625MB
% 0.20/0.45  % OS       : Linux 6.8.0-71-generic
% 0.20/0.45  % CPULimit : 300
% 0.20/0.45  % WCLimit  : 300
% 0.20/0.45  % DateTime : Fri Sep 25 03:07:17 UTC 2026
% 0.20/0.46  % CPUTime  : 
% 0.20/0.46  Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.24/0.51  Running EPR theorem proving
% 0.24/0.51  Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s epr_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.24/0.53  
% 0.24/0.53  % ======== iProver multi-core TPTP/SMT =========
% 0.24/0.53  
% 0.24/0.53  % Detected problem language: tptp
% 0.24/0.55  % Proving...
% 168.81/34.47  % SZS status Started for theBenchmark.p
% 168.81/34.47  % SZS status Unsatisfiable for theBenchmark.p
% 168.81/34.47  
% 168.81/34.47  %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 168.81/34.47  
% 168.81/34.47  % ------  iProver source info
% 168.81/34.47  
% 168.81/34.47  % git: date: 2026-07-19 20:42:38 +0200
% 168.81/34.47  % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 168.81/34.47  % git: non_committed_changes: false
% 168.81/34.47  
% 168.81/34.47  % ------ Parsing...% successful
% 168.81/34.47  
% 168.81/34.47  
% 168.81/34.47  % ------ Clausification by vclausify_rel  & Parsing by iProver...% ------  preprocesses with Option_epr_non_horn_eq
% 168.81/34.47  % 
% 168.81/34.47  
% 168.81/34.47  % ------ Preprocessing... sup_sim: 9  sf_s  rm: 6 0s  sf_e  pe_s  pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe:32:0s pe:64:0s pe:128:0s pe:256:2s pe_e  sf_s  rm: 0 0s  sf_e  pe_s  pe_e % 
% 168.81/34.47  
% 168.81/34.47  % ------ Preprocessing...% ------  preprocesses with Option_epr_non_horn_non_eq
% 168.81/34.47   gs_s  sp: 0 0s  gs_e  snvd_s sp: 0 0s snvd_e 
% 168.81/34.47  % ------ Proving...
% 168.81/34.47  % ------ Problem Properties 
% 168.81/34.47  
% 168.81/34.47  % 
% 168.81/34.47  % clauses                               1784
% 168.81/34.47  % conjectures                           0
% 168.81/34.47  % EPR                                   1784
% 168.81/34.47  % Horn                                  1363
% 168.81/34.47  % unary                                 292
% 168.81/34.47  % binary                                994
% 168.81/34.47  % lits                                  4549
% 168.81/34.47  % lits eq                               0
% 168.81/34.47  % fd_pure                               0
% 168.81/34.47  % fd_pseudo                             0
% 168.81/34.47  % fd_cond                               0
% 168.81/34.47  % fd_pseudo_cond                        0
% 168.81/34.47  % AC symbols                            0
% 168.81/34.47  
% 168.81/34.47  % ------ Schedule EPR non Horn non eq is on
% 168.81/34.47  
% 168.81/34.47  % ------ no conjectures: strip conj schedule 
% 168.81/34.47  
% 168.81/34.47  % ------ no equalities: superposition off 
% 168.81/34.47  
% 168.81/34.47  % ------ Input Options "--resolution_flag false" stripped conjectures Time Limit: 70.
% 168.81/34.47  
% 168.81/34.47  
% 168.81/34.47  % ------ 
% 168.81/34.47  % Current options:
% 168.81/34.47  % ------ 
% 168.81/34.47  
% 168.81/34.47  
% 168.81/34.47  % 
% 168.81/34.47  
% 168.81/34.47  % ------ Proving...
% 168.81/34.47  % 
% 168.81/34.47  
% 168.81/34.47  % SZS status Unsatisfiable for theBenchmark.p
% 168.81/34.47  
% 168.81/34.47  % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 168.81/34.48  
% 168.81/34.48  
%------------------------------------------------------------------------------