%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO588-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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 : Thu Sep 24 03:47:50 PM UTC 2026
% Result : Unsatisfiable 244.79s 245.00s
% Output : CNFRefutation 244.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 94
% Number of leaves : 135
% Syntax : Number of clauses : 624 ( 13 unt; 277 nHn; 423 RR)
% Number of literals : 2157 ( 0 equ; 832 neg)
% Maximal clause size : 10 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 134 ( 133 usr; 4 prp; 0-21 aty)
% Number of functors : 2 ( 2 usr; 2 con; 0-0 aty)
% Number of variables : 8214 (2117 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_1127,axiom,
( ~ esk762_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk21_1(X1)
| esk12_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1127) ).
cnf(i_0_2025,axiom,
( ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk762_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2025) ).
cnf(i_0_635,axiom,
( ~ esk1_0
| esk2_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_635) ).
cnf(i_0_1842,axiom,
( ~ esk1_0
| esk3_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1842) ).
cnf(i_0_2328,axiom,
( ~ esk45_1(X1)
| ~ p(X1)
| esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2328) ).
cnf(i_0_674,axiom,
( ~ esk2_0
| ~ p(X1)
| ~ esk4_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_674) ).
cnf(i_0_1703,axiom,
esk1_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1703) ).
cnf(i_0_1163,axiom,
( ~ esk3_0
| esk4_1(X1)
| esk5_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1163) ).
cnf(i_0_882,axiom,
( ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk11_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_882) ).
cnf(i_0_2216,axiom,
( ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk22_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2216) ).
cnf(i_0_1254,axiom,
( ~ esk5_1(X1)
| esk45_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1254) ).
cnf(i_0_2226,axiom,
( ~ esk11_1(X1)
| ~ esk52_1(X1)
| ~ esk21_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2226) ).
cnf(i_0_1147,axiom,
( ~ esk53_1(X1)
| ~ esk22_1(X1)
| ~ esk12_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1147) ).
cnf(i_0_590,axiom,
( ~ esk46_1(X1)
| esk57_5(X1,X2,X3,X4,X5)
| esk58_5(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_590) ).
cnf(i_0_2309,axiom,
( ~ esk5_1(X1)
| esk46_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2309) ).
cnf(i_0_1895,axiom,
( ~ esk5_1(X1)
| esk53_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1895) ).
cnf(i_0_162,axiom,
( ~ esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk41_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_162) ).
cnf(rule_true,axiom,
p(true),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_true) ).
cnf(i_0_361,axiom,
( ~ esk5_1(X1)
| esk52_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_361) ).
cnf(i_0_1960,axiom,
( ~ p(X5)
| ~ esk746_21(X2,X4,X1,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ p(X3)
| ~ esk41_1(X2)
| p(X4)
| p(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1960) ).
cnf(i_0_884,axiom,
( ~ esk57_5(X1,X2,X3,X4,X5)
| esk746_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_884) ).
cnf(i_0_2128,axiom,
( ~ esk98_5(X1,X2,X3,X4,X5)
| esk707_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2128) ).
cnf(i_0_497,axiom,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk98_5(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_497) ).
cnf(i_0_1555,axiom,
( ~ esk707_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk26_1(X1)
| esk741_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1555) ).
cnf(i_0_1456,axiom,
( ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk26_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1456) ).
cnf(i_0_267,axiom,
( ~ esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk37_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_267) ).
cnf(i_0_1073,axiom,
( ~ esk721_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk66_5(X1,X2,X3,X4,X5)
| esk75_5(X1,X2,X3,X4,X5)
| esk722_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1073) ).
cnf(i_0_1809,axiom,
( ~ esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk721_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1809) ).
cnf(i_0_2561,axiom,
( ~ esk37_1(X1)
| ~ esk741_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2561) ).
cnf(i_0_1467,axiom,
( ~ esk113_5(X1,X2,X3,X4,X5)
| esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk677_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1467) ).
cnf(i_0_957,axiom,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk113_5(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_957) ).
cnf(i_0_1499,axiom,
( ~ esk722_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk95_5(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1499) ).
cnf(i_0_27,axiom,
( ~ esk66_5(X1,X2,X3,X4,X5)
| ~ esk125_5(X1,X2,X3,X4,X5)
| ~ esk76_5(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_27) ).
cnf(i_0_478,axiom,
( ~ esk75_5(X1,X2,X3,X4,X5)
| ~ esk65_5(X1,X2,X3,X4,X5)
| ~ esk124_5(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_478) ).
cnf(i_0_835,axiom,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk124_5(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_835) ).
cnf(i_0_1956,axiom,
( ~ esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk65_5(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1956) ).
cnf(i_0_2384,axiom,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk125_5(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2384) ).
cnf(i_0_2311,axiom,
( ~ esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk76_5(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2311) ).
cnf(i_0_945,axiom,
( ~ esk117_5(X1,X2,X3,X4,X5)
| esk128_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_945) ).
cnf(i_0_1871,axiom,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk117_5(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1871) ).
cnf(i_0_1155,axiom,
( ~ p(X4)
| ~ p(X5)
| ~ esk677_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| p(X2)
| p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1155) ).
cnf(i_0_481,axiom,
( ~ p(X6)
| ~ p(X9)
| ~ esk95_5(X1,X2,X3,X4,X5)
| ~ p(X8)
| ~ esk668_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| p(X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_481) ).
cnf(i_0_1573,axiom,
( ~ esk128_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk668_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1573) ).
cnf(i_0_538,axiom,
( ~ esk169_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk628_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_538) ).
cnf(i_0_2423,axiom,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk169_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2423) ).
cnf(i_0_1514,axiom,
( ~ esk79_5(X1,X2,X3,X4,X5)
| ~ esk628_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk662_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1514) ).
cnf(i_0_2495,axiom,
( ~ esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk79_5(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2495) ).
cnf(i_0_2170,axiom,
( ~ esk95_5(X1,X2,X3,X4,X5)
| ~ esk662_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2170) ).
cnf(i_0_2351,axiom,
( ~ esk640_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk138_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2351) ).
cnf(i_0_1544,axiom,
( ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk640_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1544) ).
cnf(i_0_816,axiom,
( ~ esk185_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk596_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_816) ).
cnf(i_0_788,axiom,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk185_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_788) ).
cnf(i_0_668,axiom,
( ~ esk138_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk148_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk197_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_668) ).
cnf(i_0_1057,axiom,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk197_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1057) ).
cnf(i_0_2329,axiom,
( ~ esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk167_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2329) ).
cnf(i_0_905,axiom,
( ~ esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk148_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_905) ).
cnf(i_0_1023,axiom,
( ~ esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk137_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1023) ).
cnf(i_0_2245,axiom,
( ~ esk596_21(X5,X6,X7,X8,X9,X1,X4,X3,X2,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2245) ).
cnf(i_0_1132,axiom,
( ~ esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk196_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk137_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1132) ).
cnf(i_0_2275,axiom,
( ~ esk188_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk199_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2275) ).
cnf(i_0_87,axiom,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk188_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_87) ).
cnf(i_0_2486,axiom,
( ~ esk167_9(X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ p(X13)
| ~ p(X12)
| ~ esk590_21(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ p(X1)
| p(X11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2486) ).
cnf(i_0_2487,axiom,
( ~ esk199_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk590_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2487) ).
cnf(i_0_7,axiom,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk196_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_7) ).
cnf(i_0_2369,axiom,
( ~ esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk163_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2369) ).
cnf(i_0_1945,axiom,
( ~ esk240_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk549_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1945) ).
cnf(i_0_1098,axiom,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk240_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1098) ).
cnf(i_0_2417,axiom,
( ~ esk549_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk150_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk583_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2417) ).
cnf(i_0_2297,axiom,
( ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk150_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2297) ).
cnf(i_0_476,axiom,
( ~ esk257_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk515_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_476) ).
cnf(i_0_1118,axiom,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk257_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1118) ).
cnf(i_0_81,axiom,
( ~ esk163_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk583_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_81) ).
cnf(i_0_553,axiom,
( ~ esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk209_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_553) ).
cnf(i_0_260,axiom,
( ~ esk560_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk210_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_260) ).
cnf(i_0_2491,axiom,
( ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk560_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2491) ).
cnf(i_0_921,axiom,
( ~ p(X13)
| ~ p(X11)
| ~ p(X12)
| ~ esk515_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| p(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_921) ).
cnf(i_0_2272,axiom,
( ~ esk220_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk210_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk269_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2272) ).
cnf(i_0_1701,axiom,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk269_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1701) ).
cnf(i_0_1059,axiom,
( ~ esk268_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk209_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1059) ).
cnf(i_0_333,axiom,
( ~ esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk239_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_333) ).
cnf(i_0_22,axiom,
( ~ esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk220_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_22) ).
cnf(i_0_1342,axiom,
( ~ esk259_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1342) ).
cnf(i_0_2006,axiom,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk259_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2006) ).
cnf(i_0_2353,axiom,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk268_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2353) ).
cnf(i_0_1780,axiom,
( ~ p(X16)
| ~ esk239_13(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| ~ p(X17)
| ~ esk512_21(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X2,X16,X1,X17,X18,X19,X20,X21)
| ~ p(X2)
| ~ p(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1780) ).
cnf(i_0_2511,axiom,
( ~ esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk512_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2511) ).
cnf(i_0_1097,axiom,
( ~ esk557_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk574_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1097) ).
cnf(i_0_2531,axiom,
( ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk557_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2531) ).
cnf(i_0_170,axiom,
( ~ esk316_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk289_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk284_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk458_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_170) ).
cnf(i_0_2360,axiom,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk316_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2360) ).
cnf(i_0_1900,axiom,
( ~ esk310_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk470_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1900) ).
cnf(i_0_2219,axiom,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk310_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2219) ).
cnf(i_0_1228,axiom,
( ~ esk574_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk576_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1228) ).
cnf(i_0_1052,axiom,
( ~ esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk235_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1052) ).
cnf(i_0_163,axiom,
( ~ esk458_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk227_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk459_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_163) ).
cnf(i_0_1603,axiom,
( ~ esk576_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk227_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk203_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1603) ).
cnf(i_0_1736,axiom,
( ~ esk470_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk221_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk504_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1736) ).
cnf(i_0_117,axiom,
( ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk221_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_117) ).
cnf(i_0_1920,axiom,
( ~ esk459_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk235_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1920) ).
cnf(i_0_345,axiom,
( ~ esk235_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk504_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_345) ).
cnf(i_0_2339,axiom,
( ~ esk332_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk284_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk274_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2339) ).
cnf(i_0_455,axiom,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk332_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_455) ).
cnf(i_0_269,axiom,
( ~ esk473_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk290_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk279_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_269) ).
cnf(i_0_1240,axiom,
( ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk473_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1240) ).
cnf(i_0_1305,axiom,
( ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk274_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1305) ).
cnf(i_0_1677,axiom,
( ~ esk472_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk291_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk280_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1677) ).
cnf(i_0_2180,axiom,
( ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk472_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2180) ).
cnf(i_0_1181,axiom,
( ~ esk279_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk337_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk289_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1181) ).
cnf(i_0_1445,axiom,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk337_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1445) ).
cnf(i_0_1811,axiom,
( ~ esk280_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk338_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk290_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1811) ).
cnf(i_0_1766,axiom,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk338_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1766) ).
cnf(i_0_347,axiom,
( ~ esk328_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk435_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk434_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_347) ).
cnf(i_0_327,axiom,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk328_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_327) ).
cnf(i_0_1319,axiom,
( ~ esk636_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk653_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1319) ).
cnf(i_0_149,axiom,
( ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk636_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_149) ).
cnf(i_0_138,axiom,
( ~ esk246_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk537_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk213_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_138) ).
cnf(i_0_346,axiom,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk246_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_346) ).
cnf(i_0_2503,axiom,
( ~ esk281_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk291_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk339_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2503) ).
cnf(i_0_676,axiom,
( ~ esk435_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk281_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_676) ).
cnf(i_0_1464,axiom,
( ~ esk653_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk655_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1464) ).
cnf(i_0_684,axiom,
( ~ esk552_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk208_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_684) ).
cnf(i_0_212,axiom,
( ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk552_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_212) ).
cnf(i_0_2287,axiom,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk339_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2287) ).
cnf(i_0_1011,axiom,
( ~ p(X17)
| ~ esk434_21(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X2,X3,X1,X18,X19,X20,X21)
| ~ p(X3)
| ~ p(X2)
| ~ p(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1011) ).
cnf(i_0_601,axiom,
( ~ esk537_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk156_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk538_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_601) ).
cnf(i_0_1522,axiom,
( ~ esk655_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk156_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk132_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1522) ).
cnf(i_0_417,axiom,
( ~ esk262_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk213_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk203_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_417) ).
cnf(i_0_2187,axiom,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk262_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2187) ).
cnf(i_0_221,axiom,
( ~ esk208_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk267_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_221) ).
cnf(i_0_1318,axiom,
( ~ esk163_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk538_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1318) ).
cnf(i_0_1575,axiom,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk267_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1575) ).
cnf(i_0_1724,axiom,
( ~ esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk142_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1724) ).
cnf(i_0_2281,axiom,
( ~ esk142_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk132_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk191_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2281) ).
cnf(i_0_3,axiom,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk191_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3) ).
cnf(rule_false,axiom,
~ p(false),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_false) ).
cnf(c_0_2697,plain,
( ~ esk762_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk21_1(X1)
| esk12_1(X1) ),
inference(fof_simplification,[status(thm)],[i_0_1127]) ).
cnf(c_0_2698,plain,
( ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk762_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_2025]) ).
cnf(c_0_2699,plain,
( ~ esk1_0
| esk2_0 ),
inference(fof_simplification,[status(thm)],[i_0_635]) ).
cnf(c_0_2700,plain,
( ~ esk1_0
| esk3_0 ),
inference(fof_simplification,[status(thm)],[i_0_1842]) ).
cnf(c_0_2701,plain,
( ~ esk762_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk21_1(X1)
| esk12_1(X1) ),
c_0_2697 ).
cnf(c_0_2702,plain,
( ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk762_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2698 ).
cnf(c_0_2703,plain,
( ~ esk45_1(X1)
| ~ p(X1)
| esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_2328]) ).
cnf(c_0_2704,plain,
( ~ esk2_0
| ~ p(X1)
| ~ esk4_1(X1) ),
inference(fof_simplification,[status(thm)],[i_0_674]) ).
cnf(c_0_2705,plain,
( ~ esk1_0
| esk2_0 ),
c_0_2699 ).
cnf(c_0_2706,axiom,
esk1_0,
i_0_1703 ).
cnf(c_0_2707,plain,
( ~ esk3_0
| esk4_1(X1)
| esk5_1(X1) ),
inference(fof_simplification,[status(thm)],[i_0_1163]) ).
cnf(c_0_2708,plain,
( ~ esk1_0
| esk3_0 ),
c_0_2700 ).
cnf(c_0_2709,plain,
( ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk11_1(X1) ),
inference(fof_simplification,[status(thm)],[i_0_882]) ).
cnf(c_0_2710,plain,
( ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk22_1(X1) ),
inference(fof_simplification,[status(thm)],[i_0_2216]) ).
cnf(c_0_2711,plain,
( ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk21_1(X1)
| esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk12_1(X1) ),
inference(spm,[status(thm)],[c_0_2701,c_0_2702]) ).
cnf(c_0_2712,plain,
( ~ esk45_1(X1)
| ~ p(X1)
| esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2703 ).
cnf(c_0_2713,plain,
( ~ esk5_1(X1)
| esk45_1(X1) ),
inference(fof_simplification,[status(thm)],[i_0_1254]) ).
cnf(c_0_2714,plain,
( ~ esk2_0
| ~ p(X1)
| ~ esk4_1(X1) ),
c_0_2704 ).
cnf(c_0_2715,plain,
esk2_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2705,c_0_2706])]) ).
cnf(c_0_2716,plain,
( ~ esk3_0
| esk4_1(X1)
| esk5_1(X1) ),
c_0_2707 ).
cnf(c_0_2717,plain,
esk3_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2708,c_0_2706])]) ).
cnf(c_0_2718,plain,
( ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk11_1(X1) ),
c_0_2709 ).
cnf(c_0_2719,plain,
( ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk22_1(X1) ),
c_0_2710 ).
cnf(c_0_2720,plain,
( ~ p(X1)
| ~ esk45_1(X1)
| esk21_1(X1)
| esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk12_1(X1) ),
inference(spm,[status(thm)],[c_0_2711,c_0_2712]) ).
cnf(c_0_2721,plain,
( ~ esk5_1(X1)
| esk45_1(X1) ),
c_0_2713 ).
cnf(c_0_2722,plain,
( ~ p(X1)
| ~ esk4_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2714,c_0_2715])]) ).
cnf(c_0_2723,plain,
( esk5_1(X1)
| esk4_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2716,c_0_2717])]) ).
cnf(c_0_2724,plain,
( ~ esk11_1(X1)
| ~ esk52_1(X1)
| ~ esk21_1(X1) ),
inference(fof_simplification,[status(thm)],[i_0_2226]) ).
cnf(c_0_2725,plain,
( ~ p(X1)
| ~ esk45_1(X1)
| esk11_1(X1) ),
inference(spm,[status(thm)],[c_0_2718,c_0_2712]) ).
cnf(c_0_2726,plain,
( ~ esk53_1(X1)
| ~ esk22_1(X1)
| ~ esk12_1(X1) ),
inference(fof_simplification,[status(thm)],[i_0_1147]) ).
cnf(c_0_2727,plain,
( ~ p(X1)
| ~ esk45_1(X1)
| esk22_1(X1) ),
inference(spm,[status(thm)],[c_0_2719,c_0_2712]) ).
cnf(c_0_2728,plain,
( ~ p(X1)
| ~ esk5_1(X1)
| esk21_1(X1)
| esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk12_1(X1) ),
inference(spm,[status(thm)],[c_0_2720,c_0_2721]) ).
cnf(c_0_2729,plain,
( ~ p(X1)
| esk5_1(X1) ),
inference(spm,[status(thm)],[c_0_2722,c_0_2723]) ).
cnf(c_0_2730,plain,
( ~ esk46_1(X1)
| esk57_5(X1,X2,X3,X4,X5)
| esk58_5(X1,X2,X3,X4,X5) ),
inference(fof_simplification,[status(thm)],[i_0_590]) ).
cnf(c_0_2731,plain,
( ~ esk5_1(X1)
| esk46_1(X1) ),
inference(fof_simplification,[status(thm)],[i_0_2309]) ).
cnf(c_0_2732,plain,
( ~ esk11_1(X1)
| ~ esk52_1(X1)
| ~ esk21_1(X1) ),
c_0_2724 ).
cnf(c_0_2733,plain,
( ~ p(X1)
| ~ esk5_1(X1)
| esk11_1(X1) ),
inference(spm,[status(thm)],[c_0_2725,c_0_2721]) ).
cnf(c_0_2734,plain,
( ~ esk53_1(X1)
| ~ esk22_1(X1)
| ~ esk12_1(X1) ),
c_0_2726 ).
cnf(c_0_2735,plain,
( ~ p(X1)
| ~ esk5_1(X1)
| esk22_1(X1) ),
inference(spm,[status(thm)],[c_0_2727,c_0_2721]) ).
cnf(c_0_2736,plain,
( ~ esk5_1(X1)
| esk53_1(X1) ),
inference(fof_simplification,[status(thm)],[i_0_1895]) ).
cnf(c_0_2737,plain,
( ~ esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk41_1(X1) ),
inference(fof_simplification,[status(thm)],[i_0_162]) ).
cnf(c_0_2738,plain,
( ~ p(X1)
| esk21_1(X1)
| esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk12_1(X1) ),
inference(spm,[status(thm)],[c_0_2728,c_0_2729]) ).
cnf(c_0_2739,axiom,
p(true),
rule_true ).
cnf(c_0_2740,plain,
( ~ esk46_1(X1)
| esk57_5(X1,X2,X3,X4,X5)
| esk58_5(X1,X2,X3,X4,X5) ),
c_0_2730 ).
cnf(c_0_2741,plain,
( ~ esk5_1(X1)
| esk46_1(X1) ),
c_0_2731 ).
cnf(c_0_2742,plain,
( ~ p(X1)
| ~ esk21_1(X1)
| ~ esk52_1(X1)
| ~ esk5_1(X1) ),
inference(spm,[status(thm)],[c_0_2732,c_0_2733]) ).
cnf(c_0_2743,plain,
( ~ esk5_1(X1)
| esk52_1(X1) ),
inference(fof_simplification,[status(thm)],[i_0_361]) ).
cnf(c_0_2744,plain,
( ~ p(X1)
| ~ esk5_1(X1)
| ~ esk12_1(X1)
| ~ esk53_1(X1) ),
inference(spm,[status(thm)],[c_0_2734,c_0_2735]) ).
cnf(c_0_2745,plain,
( ~ esk5_1(X1)
| esk53_1(X1) ),
c_0_2736 ).
cnf(c_0_2746,plain,
( ~ esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk41_1(X1) ),
c_0_2737 ).
cnf(c_0_2747,plain,
( esk21_1(true)
| esk765_21(true,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk12_1(true) ),
inference(spm,[status(thm)],[c_0_2738,c_0_2739]) ).
cnf(c_0_2748,plain,
( ~ p(X5)
| ~ esk746_21(X2,X4,X1,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ p(X3)
| ~ esk41_1(X2)
| p(X4)
| p(X1) ),
inference(fof_simplification,[status(thm)],[i_0_1960]) ).
cnf(c_0_2749,plain,
( ~ esk57_5(X1,X2,X3,X4,X5)
| esk746_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_884]) ).
cnf(c_0_2750,plain,
( ~ esk5_1(X1)
| esk58_5(X1,X2,X3,X4,X5)
| esk57_5(X1,X2,X3,X4,X5) ),
inference(spm,[status(thm)],[c_0_2740,c_0_2741]) ).
cnf(c_0_2751,plain,
( ~ p(X1)
| ~ esk21_1(X1)
| ~ esk52_1(X1) ),
inference(spm,[status(thm)],[c_0_2742,c_0_2729]) ).
cnf(c_0_2752,plain,
( ~ esk5_1(X1)
| esk52_1(X1) ),
c_0_2743 ).
cnf(c_0_2753,plain,
( ~ p(X1)
| ~ esk5_1(X1)
| ~ esk12_1(X1) ),
inference(spm,[status(thm)],[c_0_2744,c_0_2745]) ).
cnf(c_0_2754,plain,
( esk41_1(true)
| esk21_1(true)
| esk12_1(true) ),
inference(spm,[status(thm)],[c_0_2746,c_0_2747]) ).
cnf(c_0_2755,plain,
( ~ p(X5)
| ~ esk746_21(X2,X4,X1,X3,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ p(X3)
| ~ esk41_1(X2)
| p(X4)
| p(X1) ),
c_0_2748 ).
cnf(c_0_2756,plain,
( ~ esk57_5(X1,X2,X3,X4,X5)
| esk746_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2749 ).
cnf(c_0_2757,plain,
( ~ p(X1)
| esk58_5(X1,X2,X3,X4,X5)
| esk57_5(X1,X2,X3,X4,X5) ),
inference(spm,[status(thm)],[c_0_2750,c_0_2729]) ).
cnf(c_0_2758,plain,
( ~ p(X1)
| ~ esk21_1(X1)
| ~ esk5_1(X1) ),
inference(spm,[status(thm)],[c_0_2751,c_0_2752]) ).
cnf(c_0_2759,plain,
( ~ esk5_1(true)
| esk41_1(true)
| esk21_1(true) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2753,c_0_2754]),c_0_2739])]) ).
cnf(c_0_2760,plain,
( ~ p(X4)
| ~ p(X5)
| ~ esk41_1(X3)
| ~ esk57_5(X3,X1,X2,X4,X5)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2755,c_0_2756]) ).
cnf(c_0_2761,plain,
( esk58_5(true,X1,X2,X3,X4)
| esk57_5(true,X1,X2,X3,X4) ),
inference(spm,[status(thm)],[c_0_2757,c_0_2739]) ).
cnf(c_0_2762,plain,
( ~ p(X1)
| ~ esk21_1(X1) ),
inference(spm,[status(thm)],[c_0_2758,c_0_2729]) ).
cnf(c_0_2763,plain,
( esk41_1(true)
| esk21_1(true) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2759,c_0_2729]),c_0_2739])]) ).
cnf(c_0_2764,plain,
( ~ p(X3)
| ~ p(X4)
| ~ esk41_1(true)
| p(X2)
| p(X1)
| esk58_5(true,X1,X2,X3,X4) ),
inference(spm,[status(thm)],[c_0_2760,c_0_2761]) ).
cnf(c_0_2765,plain,
esk41_1(true),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2762,c_0_2763]),c_0_2739])]) ).
cnf(c_0_2766,plain,
( ~ esk98_5(X1,X2,X3,X4,X5)
| esk707_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_2128]) ).
cnf(c_0_2767,plain,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk98_5(X1,X2,X3,X4,X5) ),
inference(fof_simplification,[status(thm)],[i_0_497]) ).
cnf(c_0_2768,plain,
( ~ p(X3)
| ~ p(X4)
| p(X2)
| p(X1)
| esk58_5(true,X1,X2,X3,X4) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2764,c_0_2765])]) ).
cnf(c_0_2769,plain,
( ~ esk98_5(X1,X2,X3,X4,X5)
| esk707_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2766 ).
cnf(c_0_2770,plain,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk98_5(X1,X2,X3,X4,X5) ),
c_0_2767 ).
cnf(c_0_2771,plain,
( ~ p(X3)
| p(X2)
| p(X1)
| esk58_5(true,X1,X2,X3,true) ),
inference(spm,[status(thm)],[c_0_2768,c_0_2739]) ).
cnf(c_0_2772,plain,
( ~ esk707_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk26_1(X1)
| esk741_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_1555]) ).
cnf(c_0_2773,plain,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk707_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(spm,[status(thm)],[c_0_2769,c_0_2770]) ).
cnf(c_0_2774,plain,
( p(X2)
| p(X1)
| esk58_5(true,X1,X2,true,true) ),
inference(spm,[status(thm)],[c_0_2771,c_0_2739]) ).
cnf(c_0_2775,plain,
( ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk26_1(X1) ),
inference(fof_simplification,[status(thm)],[i_0_1456]) ).
cnf(c_0_2776,plain,
( ~ esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk37_1(X1) ),
inference(fof_simplification,[status(thm)],[i_0_267]) ).
cnf(c_0_2777,plain,
( ~ esk707_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk26_1(X1)
| esk741_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2772 ).
cnf(c_0_2778,plain,
( p(X2)
| p(X1)
| esk708_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
| esk707_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) ),
inference(spm,[status(thm)],[c_0_2773,c_0_2774]) ).
cnf(c_0_2779,plain,
( ~ esk750_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk26_1(X1) ),
c_0_2775 ).
cnf(c_0_2780,plain,
( ~ esk765_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk37_1(X1) ),
c_0_2776 ).
cnf(c_0_2781,plain,
( ~ esk26_1(true)
| p(X2)
| p(X1)
| esk708_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
| esk741_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) ),
inference(spm,[status(thm)],[c_0_2777,c_0_2778]) ).
cnf(c_0_2782,plain,
( ~ p(X1)
| ~ esk45_1(X1)
| esk26_1(X1) ),
inference(spm,[status(thm)],[c_0_2779,c_0_2712]) ).
cnf(c_0_2783,plain,
( esk37_1(true)
| esk21_1(true)
| esk12_1(true) ),
inference(spm,[status(thm)],[c_0_2780,c_0_2747]) ).
cnf(c_0_2784,plain,
( ~ esk45_1(true)
| p(X2)
| p(X1)
| esk708_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
| esk741_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2781,c_0_2782]),c_0_2739])]) ).
cnf(c_0_2785,plain,
( ~ esk5_1(true)
| esk37_1(true)
| esk21_1(true) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2753,c_0_2783]),c_0_2739])]) ).
cnf(c_0_2786,plain,
( ~ esk721_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk66_5(X1,X2,X3,X4,X5)
| esk75_5(X1,X2,X3,X4,X5)
| esk722_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_1073]) ).
cnf(c_0_2787,plain,
( ~ esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk721_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_1809]) ).
cnf(c_0_2788,plain,
( ~ esk37_1(X1)
| ~ esk741_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_2561]) ).
cnf(c_0_2789,plain,
( ~ esk5_1(true)
| p(X2)
| p(X1)
| esk708_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
| esk741_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) ),
inference(spm,[status(thm)],[c_0_2784,c_0_2721]) ).
cnf(c_0_2790,plain,
( esk37_1(true)
| esk21_1(true) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2785,c_0_2729]),c_0_2739])]) ).
cnf(c_0_2791,plain,
( ~ esk721_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk66_5(X1,X2,X3,X4,X5)
| esk75_5(X1,X2,X3,X4,X5)
| esk722_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2786 ).
cnf(c_0_2792,plain,
( ~ esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk721_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2787 ).
cnf(c_0_2793,plain,
( ~ esk37_1(X1)
| ~ esk741_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2788 ).
cnf(c_0_2794,plain,
( p(X2)
| p(X1)
| esk708_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
| esk741_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2789,c_0_2729]),c_0_2739])]) ).
cnf(c_0_2795,plain,
esk37_1(true),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2762,c_0_2790]),c_0_2739])]) ).
cnf(c_0_2796,plain,
( ~ esk113_5(X1,X2,X3,X4,X5)
| esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk677_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_1467]) ).
cnf(c_0_2797,plain,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk113_5(X1,X2,X3,X4,X5) ),
inference(fof_simplification,[status(thm)],[i_0_957]) ).
cnf(c_0_2798,plain,
( ~ esk722_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk95_5(X1,X2,X3,X4,X5) ),
inference(fof_simplification,[status(thm)],[i_0_1499]) ).
cnf(c_0_2799,plain,
( ~ esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk722_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk66_5(X1,X2,X3,X4,X5)
| esk75_5(X1,X2,X3,X4,X5) ),
inference(spm,[status(thm)],[c_0_2791,c_0_2792]) ).
cnf(c_0_2800,plain,
( p(X2)
| p(X1)
| esk708_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2793,c_0_2794]),c_0_2795])]) ).
cnf(c_0_2801,plain,
( ~ esk113_5(X1,X2,X3,X4,X5)
| esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk677_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2796 ).
cnf(c_0_2802,plain,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk113_5(X1,X2,X3,X4,X5) ),
c_0_2797 ).
cnf(c_0_2803,plain,
( ~ esk66_5(X1,X2,X3,X4,X5)
| ~ esk125_5(X1,X2,X3,X4,X5)
| ~ esk76_5(X1,X2,X3,X4,X5) ),
inference(fof_simplification,[status(thm)],[i_0_27]) ).
cnf(c_0_2804,plain,
( ~ esk722_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk95_5(X1,X2,X3,X4,X5) ),
c_0_2798 ).
cnf(c_0_2805,plain,
( p(X2)
| p(X1)
| esk722_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
| esk66_5(true,X1,X2,true,true)
| esk75_5(true,X1,X2,true,true) ),
inference(spm,[status(thm)],[c_0_2799,c_0_2800]) ).
cnf(c_0_2806,plain,
( ~ esk75_5(X1,X2,X3,X4,X5)
| ~ esk65_5(X1,X2,X3,X4,X5)
| ~ esk124_5(X1,X2,X3,X4,X5) ),
inference(fof_simplification,[status(thm)],[i_0_478]) ).
cnf(c_0_2807,plain,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk124_5(X1,X2,X3,X4,X5) ),
inference(fof_simplification,[status(thm)],[i_0_835]) ).
cnf(c_0_2808,plain,
( ~ esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk65_5(X1,X2,X3,X4,X5) ),
inference(fof_simplification,[status(thm)],[i_0_1956]) ).
cnf(c_0_2809,plain,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk677_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(spm,[status(thm)],[c_0_2801,c_0_2802]) ).
cnf(c_0_2810,plain,
( ~ esk66_5(X1,X2,X3,X4,X5)
| ~ esk125_5(X1,X2,X3,X4,X5)
| ~ esk76_5(X1,X2,X3,X4,X5) ),
c_0_2803 ).
cnf(c_0_2811,plain,
( p(X2)
| p(X1)
| esk95_5(true,X1,X2,true,true)
| esk66_5(true,X1,X2,true,true)
| esk75_5(true,X1,X2,true,true) ),
inference(spm,[status(thm)],[c_0_2804,c_0_2805]) ).
cnf(c_0_2812,plain,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk125_5(X1,X2,X3,X4,X5) ),
inference(fof_simplification,[status(thm)],[i_0_2384]) ).
cnf(c_0_2813,plain,
( ~ esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk76_5(X1,X2,X3,X4,X5) ),
inference(fof_simplification,[status(thm)],[i_0_2311]) ).
cnf(c_0_2814,plain,
( ~ esk117_5(X1,X2,X3,X4,X5)
| esk128_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_945]) ).
cnf(c_0_2815,plain,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk117_5(X1,X2,X3,X4,X5) ),
inference(fof_simplification,[status(thm)],[i_0_1871]) ).
cnf(c_0_2816,plain,
( ~ esk75_5(X1,X2,X3,X4,X5)
| ~ esk65_5(X1,X2,X3,X4,X5)
| ~ esk124_5(X1,X2,X3,X4,X5) ),
c_0_2806 ).
cnf(c_0_2817,plain,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk124_5(X1,X2,X3,X4,X5) ),
c_0_2807 ).
cnf(c_0_2818,plain,
( ~ p(X4)
| ~ p(X5)
| ~ esk677_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| p(X2)
| p(X3) ),
inference(fof_simplification,[status(thm)],[i_0_1155]) ).
cnf(c_0_2819,plain,
( ~ esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk65_5(X1,X2,X3,X4,X5) ),
c_0_2808 ).
cnf(c_0_2820,plain,
( p(X2)
| p(X1)
| esk678_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
| esk677_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) ),
inference(spm,[status(thm)],[c_0_2809,c_0_2774]) ).
cnf(c_0_2821,plain,
( ~ esk76_5(true,X1,X2,true,true)
| ~ esk125_5(true,X1,X2,true,true)
| p(X2)
| p(X1)
| esk95_5(true,X1,X2,true,true)
| esk75_5(true,X1,X2,true,true) ),
inference(spm,[status(thm)],[c_0_2810,c_0_2811]) ).
cnf(c_0_2822,plain,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk125_5(X1,X2,X3,X4,X5) ),
c_0_2812 ).
cnf(c_0_2823,plain,
( ~ esk678_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk76_5(X1,X2,X3,X4,X5) ),
c_0_2813 ).
cnf(c_0_2824,plain,
( ~ p(X6)
| ~ p(X9)
| ~ esk95_5(X1,X2,X3,X4,X5)
| ~ p(X8)
| ~ esk668_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| p(X7) ),
inference(fof_simplification,[status(thm)],[i_0_481]) ).
cnf(c_0_2825,plain,
( ~ esk128_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk668_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_1573]) ).
cnf(c_0_2826,plain,
( ~ esk117_5(X1,X2,X3,X4,X5)
| esk128_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_2814 ).
cnf(c_0_2827,plain,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk117_5(X1,X2,X3,X4,X5) ),
c_0_2815 ).
cnf(c_0_2828,plain,
( ~ esk75_5(X1,X2,X3,X4,X5)
| ~ esk65_5(X1,X2,X3,X4,X5)
| ~ esk58_5(X1,X2,X3,X4,X5) ),
inference(spm,[status(thm)],[c_0_2816,c_0_2817]) ).
cnf(c_0_2829,plain,
( ~ p(X4)
| ~ p(X5)
| ~ esk677_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| p(X2)
| p(X3) ),
c_0_2818 ).
cnf(c_0_2830,plain,
( p(X2)
| p(X1)
| esk65_5(true,X1,X2,true,true)
| esk677_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) ),
inference(spm,[status(thm)],[c_0_2819,c_0_2820]) ).
cnf(c_0_2831,plain,
( ~ esk76_5(true,X1,X2,true,true)
| ~ esk58_5(true,X1,X2,true,true)
| p(X2)
| p(X1)
| esk95_5(true,X1,X2,true,true)
| esk75_5(true,X1,X2,true,true) ),
inference(spm,[status(thm)],[c_0_2821,c_0_2822]) ).
cnf(c_0_2832,plain,
( p(X2)
| p(X1)
| esk76_5(true,X1,X2,true,true)
| esk677_21(true,X1,X2,true,true,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) ),
inference(spm,[status(thm)],[c_0_2823,c_0_2820]) ).
cnf(c_0_2833,plain,
( ~ p(X6)
| ~ p(X9)
| ~ esk95_5(X1,X2,X3,X4,X5)
| ~ p(X8)
| ~ esk668_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| p(X7) ),
c_0_2824 ).
cnf(c_0_2834,plain,
( ~ esk128_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk668_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2825 ).
cnf(c_0_2835,plain,
( ~ esk58_5(X1,X2,X3,X4,X5)
| esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk128_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(spm,[status(thm)],[c_0_2826,c_0_2827]) ).
cnf(c_0_2836,plain,
( ~ esk75_5(true,X1,X2,true,true)
| ~ esk65_5(true,X1,X2,true,true)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2828,c_0_2774]) ).
cnf(c_0_2837,plain,
( p(X1)
| p(X2)
| esk65_5(true,X1,X2,true,true) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2829,c_0_2830]),c_0_2739])]) ).
cnf(c_0_2838,plain,
( ~ esk76_5(true,X1,X2,true,true)
| p(X2)
| p(X1)
| esk95_5(true,X1,X2,true,true)
| esk75_5(true,X1,X2,true,true) ),
inference(spm,[status(thm)],[c_0_2831,c_0_2774]) ).
cnf(c_0_2839,plain,
( p(X1)
| p(X2)
| esk76_5(true,X1,X2,true,true) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2829,c_0_2832]),c_0_2739])]) ).
cnf(c_0_2840,plain,
( ~ p(X7)
| ~ p(X8)
| ~ p(X9)
| ~ esk95_5(X2,X3,X4,X5,X6)
| ~ esk128_9(X2,X3,X4,X5,X6,X7,X1,X8,X9)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2833,c_0_2834]) ).
cnf(c_0_2841,plain,
( esk129_9(true,X1,X2,true,true,X3,X4,X5,X6)
| p(X2)
| p(X1)
| esk128_9(true,X1,X2,true,true,X3,X4,X5,X6) ),
inference(spm,[status(thm)],[c_0_2835,c_0_2774]) ).
cnf(c_0_2842,plain,
( ~ esk75_5(true,X1,X2,true,true)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2836,c_0_2837]) ).
cnf(c_0_2843,plain,
( p(X2)
| p(X1)
| esk95_5(true,X1,X2,true,true)
| esk75_5(true,X1,X2,true,true) ),
inference(spm,[status(thm)],[c_0_2838,c_0_2839]) ).
cnf(c_0_2844,plain,
( ~ p(X4)
| ~ p(X5)
| ~ p(X6)
| ~ esk95_5(true,X2,X3,true,true)
| esk129_9(true,X2,X3,true,true,X4,X1,X5,X6)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2840,c_0_2841]) ).
cnf(c_0_2845,plain,
( p(X2)
| p(X1)
| esk95_5(true,X1,X2,true,true) ),
inference(spm,[status(thm)],[c_0_2842,c_0_2843]) ).
cnf(c_0_2846,plain,
( ~ p(X4)
| ~ p(X5)
| ~ p(X6)
| esk129_9(true,X2,X3,true,true,X4,X1,X5,X6)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2844,c_0_2845]) ).
cnf(c_0_2847,plain,
( ~ esk169_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk628_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_538]) ).
cnf(c_0_2848,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk169_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_2423]) ).
cnf(c_0_2849,plain,
( ~ p(X4)
| ~ p(X5)
| esk129_9(true,X2,X3,true,true,X4,X1,X5,true)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2846,c_0_2739]) ).
cnf(c_0_2850,plain,
( ~ esk169_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk628_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2847 ).
cnf(c_0_2851,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk169_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_2848 ).
cnf(c_0_2852,plain,
( ~ p(X4)
| esk129_9(true,X2,X3,true,true,X4,X1,true,true)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2849,c_0_2739]) ).
cnf(c_0_2853,plain,
( ~ esk79_5(X1,X2,X3,X4,X5)
| ~ esk628_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk662_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_1514]) ).
cnf(c_0_2854,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk628_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(spm,[status(thm)],[c_0_2850,c_0_2851]) ).
cnf(c_0_2855,plain,
( esk129_9(true,X2,X3,true,true,true,X1,true,true)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2852,c_0_2739]) ).
cnf(c_0_2856,plain,
( ~ esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk79_5(X1,X2,X3,X4,X5) ),
inference(fof_simplification,[status(thm)],[i_0_2495]) ).
cnf(c_0_2857,plain,
( ~ esk79_5(X1,X2,X3,X4,X5)
| ~ esk628_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk662_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2853 ).
cnf(c_0_2858,plain,
( p(X2)
| p(X1)
| p(X3)
| esk628_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| esk629_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
inference(spm,[status(thm)],[c_0_2854,c_0_2855]) ).
cnf(c_0_2859,plain,
( ~ esk708_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk79_5(X1,X2,X3,X4,X5) ),
c_0_2856 ).
cnf(c_0_2860,plain,
( ~ esk95_5(X1,X2,X3,X4,X5)
| ~ esk662_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_2170]) ).
cnf(c_0_2861,plain,
( ~ esk79_5(true,X1,X2,true,true)
| p(X2)
| p(X1)
| p(X3)
| esk662_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| esk629_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
inference(spm,[status(thm)],[c_0_2857,c_0_2858]) ).
cnf(c_0_2862,plain,
( p(X2)
| p(X1)
| esk79_5(true,X1,X2,true,true) ),
inference(spm,[status(thm)],[c_0_2859,c_0_2800]) ).
cnf(c_0_2863,plain,
( ~ esk640_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk138_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_2351]) ).
cnf(c_0_2864,plain,
( ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk640_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_1544]) ).
cnf(c_0_2865,plain,
( ~ esk95_5(X1,X2,X3,X4,X5)
| ~ esk662_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2860 ).
cnf(c_0_2866,plain,
( p(X2)
| p(X1)
| p(X3)
| esk662_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| esk629_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
inference(spm,[status(thm)],[c_0_2861,c_0_2862]) ).
cnf(c_0_2867,plain,
( ~ esk185_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk596_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_816]) ).
cnf(c_0_2868,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk185_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_788]) ).
cnf(c_0_2869,plain,
( ~ esk640_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk138_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_2863 ).
cnf(c_0_2870,plain,
( ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk640_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2864 ).
cnf(c_0_2871,plain,
( ~ esk95_5(true,X1,X2,true,true)
| p(X2)
| p(X1)
| p(X3)
| esk629_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
inference(spm,[status(thm)],[c_0_2865,c_0_2866]) ).
cnf(c_0_2872,plain,
( ~ esk185_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk596_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2867 ).
cnf(c_0_2873,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk185_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_2868 ).
cnf(c_0_2874,plain,
( ~ esk138_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk148_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk197_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_668]) ).
cnf(c_0_2875,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk197_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_1057]) ).
cnf(c_0_2876,plain,
( ~ esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk167_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_2329]) ).
cnf(c_0_2877,plain,
( ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk138_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(spm,[status(thm)],[c_0_2869,c_0_2870]) ).
cnf(c_0_2878,plain,
( p(X2)
| p(X1)
| p(X3)
| esk629_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
inference(spm,[status(thm)],[c_0_2871,c_0_2845]) ).
cnf(c_0_2879,plain,
( ~ esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk148_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_905]) ).
cnf(c_0_2880,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk596_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(spm,[status(thm)],[c_0_2872,c_0_2873]) ).
cnf(c_0_2881,plain,
( ~ esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk137_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_1023]) ).
cnf(c_0_2882,plain,
( ~ esk138_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk148_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk197_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_2874 ).
cnf(c_0_2883,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk197_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_2875 ).
cnf(c_0_2884,plain,
( ~ esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk167_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_2876 ).
cnf(c_0_2885,plain,
( p(X2)
| p(X1)
| p(X3)
| esk147_9(true,X1,X2,true,true,true,X3,true,true)
| esk138_9(true,X1,X2,true,true,true,X3,true,true)
| esk645_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
inference(spm,[status(thm)],[c_0_2877,c_0_2878]) ).
cnf(c_0_2886,plain,
( ~ esk596_21(X5,X6,X7,X8,X9,X1,X4,X3,X2,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| p(X4) ),
inference(fof_simplification,[status(thm)],[i_0_2245]) ).
cnf(c_0_2887,plain,
( ~ esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk148_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_2879 ).
cnf(c_0_2888,plain,
( p(X2)
| p(X1)
| p(X3)
| esk597_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| esk596_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
inference(spm,[status(thm)],[c_0_2880,c_0_2855]) ).
cnf(c_0_2889,plain,
( ~ esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk137_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_2881 ).
cnf(c_0_2890,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk148_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk138_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(spm,[status(thm)],[c_0_2882,c_0_2883]) ).
cnf(c_0_2891,plain,
( esk167_9(true,X1,X2,true,true,true,X3,true,true)
| p(X2)
| p(X1)
| p(X3)
| esk147_9(true,X1,X2,true,true,true,X3,true,true)
| esk138_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_2884,c_0_2885]) ).
cnf(c_0_2892,plain,
( ~ esk596_21(X5,X6,X7,X8,X9,X1,X4,X3,X2,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| p(X4) ),
c_0_2886 ).
cnf(c_0_2893,plain,
( p(X2)
| p(X1)
| p(X3)
| esk148_9(true,X1,X2,true,true,true,X3,true,true)
| esk596_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
inference(spm,[status(thm)],[c_0_2887,c_0_2888]) ).
cnf(c_0_2894,plain,
( ~ esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk196_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk137_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_1132]) ).
cnf(c_0_2895,plain,
( p(X2)
| p(X1)
| p(X3)
| esk137_9(true,X1,X2,true,true,true,X3,true,true)
| esk596_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
inference(spm,[status(thm)],[c_0_2889,c_0_2888]) ).
cnf(c_0_2896,plain,
( ~ esk129_9(true,X1,X2,true,true,true,X3,true,true)
| ~ esk148_9(true,X1,X2,true,true,true,X3,true,true)
| esk167_9(true,X1,X2,true,true,true,X3,true,true)
| p(X2)
| p(X1)
| p(X3)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_2890,c_0_2891]) ).
cnf(c_0_2897,plain,
( p(X2)
| p(X1)
| p(X3)
| esk148_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2892,c_0_2893]),c_0_2739])]) ).
cnf(c_0_2898,plain,
( ~ esk188_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk199_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_2275]) ).
cnf(c_0_2899,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk188_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_87]) ).
cnf(c_0_2900,plain,
( ~ esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk196_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk137_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_2894 ).
cnf(c_0_2901,plain,
( p(X2)
| p(X1)
| p(X3)
| esk137_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2892,c_0_2895]),c_0_2739])]) ).
cnf(c_0_2902,plain,
( ~ esk129_9(true,X1,X2,true,true,true,X3,true,true)
| esk167_9(true,X1,X2,true,true,true,X3,true,true)
| p(X2)
| p(X1)
| p(X3)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_2896,c_0_2897]) ).
cnf(c_0_2903,plain,
( ~ esk167_9(X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ p(X13)
| ~ p(X12)
| ~ esk590_21(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ p(X1)
| p(X11) ),
inference(fof_simplification,[status(thm)],[i_0_2486]) ).
cnf(c_0_2904,plain,
( ~ esk199_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk590_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_2487]) ).
cnf(c_0_2905,plain,
( ~ esk188_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk199_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_2898 ).
cnf(c_0_2906,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk188_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_2899 ).
cnf(c_0_2907,plain,
( ~ esk196_9(true,X2,X3,true,true,true,X1,true,true)
| ~ esk147_9(true,X2,X3,true,true,true,X1,true,true)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2900,c_0_2901]) ).
cnf(c_0_2908,plain,
( esk167_9(true,X1,X2,true,true,true,X3,true,true)
| p(X2)
| p(X1)
| p(X3)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_2902,c_0_2855]) ).
cnf(c_0_2909,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk196_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_7]) ).
cnf(c_0_2910,plain,
( ~ esk167_9(X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ p(X13)
| ~ p(X12)
| ~ esk590_21(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ p(X1)
| p(X11) ),
c_0_2903 ).
cnf(c_0_2911,plain,
( ~ esk199_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk590_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2904 ).
cnf(c_0_2912,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk199_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(spm,[status(thm)],[c_0_2905,c_0_2906]) ).
cnf(c_0_2913,plain,
( ~ esk196_9(true,X2,X3,true,true,true,X1,true,true)
| esk167_9(true,X2,X3,true,true,true,X1,true,true)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2907,c_0_2908]) ).
cnf(c_0_2914,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk196_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_2909 ).
cnf(c_0_2915,plain,
( ~ esk167_9(X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ p(X11)
| ~ p(X12)
| ~ p(X13)
| ~ esk199_13(X2,X3,X4,X5,X6,X7,X8,X9,X10,X1,X11,X12,X13)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2910,c_0_2911]) ).
cnf(c_0_2916,plain,
( p(X2)
| p(X1)
| p(X3)
| esk199_13(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7)
| esk200_13(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7) ),
inference(spm,[status(thm)],[c_0_2912,c_0_2855]) ).
cnf(c_0_2917,plain,
( ~ esk129_9(true,X2,X3,true,true,true,X1,true,true)
| esk167_9(true,X2,X3,true,true,true,X1,true,true)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2913,c_0_2914]) ).
cnf(c_0_2918,plain,
( ~ esk167_9(true,X1,X2,true,true,true,X3,true,true)
| ~ p(X5)
| ~ p(X6)
| ~ p(X7)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk200_13(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7) ),
inference(spm,[status(thm)],[c_0_2915,c_0_2916]) ).
cnf(c_0_2919,plain,
( esk167_9(true,X2,X3,true,true,true,X1,true,true)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2917,c_0_2855]) ).
cnf(c_0_2920,plain,
( ~ esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk163_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_2369]) ).
cnf(c_0_2921,plain,
( ~ p(X5)
| ~ p(X6)
| ~ p(X7)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk200_13(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7) ),
inference(spm,[status(thm)],[c_0_2918,c_0_2919]) ).
cnf(c_0_2922,plain,
( ~ esk645_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk163_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_2920 ).
cnf(c_0_2923,plain,
( ~ esk240_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk549_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_1945]) ).
cnf(c_0_2924,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk240_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_1098]) ).
cnf(c_0_2925,plain,
( ~ p(X5)
| ~ p(X6)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk200_13(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,true) ),
inference(spm,[status(thm)],[c_0_2921,c_0_2739]) ).
cnf(c_0_2926,plain,
( esk163_9(true,X1,X2,true,true,true,X3,true,true)
| p(X2)
| p(X1)
| p(X3)
| esk147_9(true,X1,X2,true,true,true,X3,true,true)
| esk138_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_2922,c_0_2885]) ).
cnf(c_0_2927,plain,
( ~ esk240_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk549_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2923 ).
cnf(c_0_2928,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk240_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_2924 ).
cnf(c_0_2929,plain,
( ~ p(X5)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk200_13(true,X1,X2,true,true,true,X3,true,true,X4,X5,true,true) ),
inference(spm,[status(thm)],[c_0_2925,c_0_2739]) ).
cnf(c_0_2930,plain,
( ~ esk129_9(true,X1,X2,true,true,true,X3,true,true)
| ~ esk148_9(true,X1,X2,true,true,true,X3,true,true)
| esk163_9(true,X1,X2,true,true,true,X3,true,true)
| p(X2)
| p(X1)
| p(X3)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_2890,c_0_2926]) ).
cnf(c_0_2931,plain,
( ~ esk549_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk150_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk583_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_2417]) ).
cnf(c_0_2932,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk549_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(spm,[status(thm)],[c_0_2927,c_0_2928]) ).
cnf(c_0_2933,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk200_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_2929,c_0_2739]) ).
cnf(c_0_2934,plain,
( ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk150_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_2297]) ).
cnf(c_0_2935,plain,
( ~ esk129_9(true,X1,X2,true,true,true,X3,true,true)
| esk163_9(true,X1,X2,true,true,true,X3,true,true)
| p(X2)
| p(X1)
| p(X3)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_2930,c_0_2897]) ).
cnf(c_0_2936,plain,
( ~ esk257_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk515_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_476]) ).
cnf(c_0_2937,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk257_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_1118]) ).
cnf(c_0_2938,plain,
( ~ esk549_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk150_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk583_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2931 ).
cnf(c_0_2939,plain,
( esk550_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk549_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12) ),
inference(spm,[status(thm)],[c_0_2932,c_0_2933]) ).
cnf(c_0_2940,plain,
( ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk150_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_2934 ).
cnf(c_0_2941,plain,
( esk163_9(true,X1,X2,true,true,true,X3,true,true)
| p(X2)
| p(X1)
| p(X3)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_2935,c_0_2855]) ).
cnf(c_0_2942,plain,
( ~ esk257_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk515_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2936 ).
cnf(c_0_2943,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk257_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_2937 ).
cnf(c_0_2944,plain,
( ~ esk163_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk583_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_81]) ).
cnf(c_0_2945,plain,
( ~ esk150_9(true,X3,X4,true,true,true,X2,true,true)
| esk550_21(true,X3,X4,true,true,true,X2,true,true,X1,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12)
| esk583_21(true,X3,X4,true,true,true,X2,true,true,X1,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12)
| p(X4)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2938,c_0_2939]) ).
cnf(c_0_2946,plain,
( p(X2)
| p(X1)
| p(X3)
| esk150_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_2940,c_0_2878]) ).
cnf(c_0_2947,plain,
( ~ esk196_9(true,X2,X3,true,true,true,X1,true,true)
| esk163_9(true,X2,X3,true,true,true,X1,true,true)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2907,c_0_2941]) ).
cnf(c_0_2948,plain,
( ~ esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk209_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_553]) ).
cnf(c_0_2949,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk515_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(spm,[status(thm)],[c_0_2942,c_0_2943]) ).
cnf(c_0_2950,plain,
( ~ esk560_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk210_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_260]) ).
cnf(c_0_2951,plain,
( ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk560_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_2491]) ).
cnf(c_0_2952,plain,
( ~ esk163_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk583_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2944 ).
cnf(c_0_2953,plain,
( esk550_21(true,X3,X4,true,true,true,X2,true,true,X1,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12)
| esk583_21(true,X3,X4,true,true,true,X2,true,true,X1,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12)
| p(X4)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2945,c_0_2946]) ).
cnf(c_0_2954,plain,
( ~ esk129_9(true,X2,X3,true,true,true,X1,true,true)
| esk163_9(true,X2,X3,true,true,true,X1,true,true)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2947,c_0_2914]) ).
cnf(c_0_2955,plain,
( ~ p(X13)
| ~ p(X11)
| ~ p(X12)
| ~ esk515_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| p(X10) ),
inference(fof_simplification,[status(thm)],[i_0_921]) ).
cnf(c_0_2956,plain,
( ~ esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk209_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_2948 ).
cnf(c_0_2957,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk516_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12)
| esk515_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12) ),
inference(spm,[status(thm)],[c_0_2949,c_0_2933]) ).
cnf(c_0_2958,plain,
( ~ esk220_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk210_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk269_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_2272]) ).
cnf(c_0_2959,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk269_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_1701]) ).
cnf(c_0_2960,plain,
( ~ esk560_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk210_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_2950 ).
cnf(c_0_2961,plain,
( ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk560_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2951 ).
cnf(c_0_2962,plain,
( ~ esk163_9(true,X3,X4,true,true,true,X2,true,true)
| esk550_21(true,X3,X4,true,true,true,X2,true,true,X1,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12)
| p(X4)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2952,c_0_2953]) ).
cnf(c_0_2963,plain,
( esk163_9(true,X2,X3,true,true,true,X1,true,true)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2954,c_0_2855]) ).
cnf(c_0_2964,plain,
( ~ esk268_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk209_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_1059]) ).
cnf(c_0_2965,plain,
( ~ p(X13)
| ~ p(X11)
| ~ p(X12)
| ~ esk515_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| p(X10) ),
c_0_2955 ).
cnf(c_0_2966,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk515_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12)
| esk209_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_2956,c_0_2957]) ).
cnf(c_0_2967,plain,
( ~ esk220_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk210_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk269_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_2958 ).
cnf(c_0_2968,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk269_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_2959 ).
cnf(c_0_2969,plain,
( ~ esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk239_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_333]) ).
cnf(c_0_2970,plain,
( ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk210_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(spm,[status(thm)],[c_0_2960,c_0_2961]) ).
cnf(c_0_2971,plain,
( esk550_21(true,X3,X4,true,true,true,X2,true,true,X1,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12)
| p(X4)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2962,c_0_2963]) ).
cnf(c_0_2972,plain,
( ~ esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk220_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_22]) ).
cnf(c_0_2973,plain,
( ~ esk259_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_1342]) ).
cnf(c_0_2974,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk259_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_2006]) ).
cnf(c_0_2975,plain,
( ~ esk268_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk209_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_2964 ).
cnf(c_0_2976,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk209_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2965,c_0_2966]),c_0_2739])]) ).
cnf(c_0_2977,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk268_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_2353]) ).
cnf(c_0_2978,plain,
( ~ esk220_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk210_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(spm,[status(thm)],[c_0_2967,c_0_2968]) ).
cnf(c_0_2979,plain,
( ~ esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk239_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_2969 ).
cnf(c_0_2980,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk219_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk567_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12)
| esk210_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_2970,c_0_2971]) ).
cnf(c_0_2981,plain,
( ~ esk516_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk220_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_2972 ).
cnf(c_0_2982,plain,
( ~ p(X16)
| ~ esk239_13(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| ~ p(X17)
| ~ esk512_21(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X2,X16,X1,X17,X18,X19,X20,X21)
| ~ p(X2)
| ~ p(X1) ),
inference(fof_simplification,[status(thm)],[i_0_1780]) ).
cnf(c_0_2983,plain,
( ~ esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk512_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_2511]) ).
cnf(c_0_2984,plain,
( ~ esk259_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_2973 ).
cnf(c_0_2985,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk259_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_2974 ).
cnf(c_0_2986,plain,
( ~ esk219_13(true,X3,X4,true,true,true,X2,true,true,X1,true,true,true)
| ~ esk268_13(true,X3,X4,true,true,true,X2,true,true,X1,true,true,true)
| p(X4)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2975,c_0_2976]) ).
cnf(c_0_2987,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk268_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_2977 ).
cnf(c_0_2988,plain,
( ~ esk220_13(true,X3,X4,true,true,true,X2,true,true,X1,true,true,true)
| ~ esk210_13(true,X3,X4,true,true,true,X2,true,true,X1,true,true,true)
| p(X4)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2978,c_0_2933]) ).
cnf(c_0_2989,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk219_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk239_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk210_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_2979,c_0_2980]) ).
cnf(c_0_2990,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk220_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk515_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12) ),
inference(spm,[status(thm)],[c_0_2981,c_0_2957]) ).
cnf(c_0_2991,plain,
( ~ p(X16)
| ~ esk239_13(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| ~ p(X17)
| ~ esk512_21(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X2,X16,X1,X17,X18,X19,X20,X21)
| ~ p(X2)
| ~ p(X1) ),
c_0_2982 ).
cnf(c_0_2992,plain,
( ~ esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk512_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_2983 ).
cnf(c_0_2993,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(spm,[status(thm)],[c_0_2984,c_0_2985]) ).
cnf(c_0_2994,plain,
( ~ esk219_13(true,X3,X4,true,true,true,X2,true,true,X1,true,true,true)
| ~ esk200_13(true,X3,X4,true,true,true,X2,true,true,X1,true,true,true)
| p(X4)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2986,c_0_2987]) ).
cnf(c_0_2995,plain,
( ~ esk220_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk219_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk239_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_2988,c_0_2989]) ).
cnf(c_0_2996,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk220_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2965,c_0_2990]),c_0_2739])]) ).
cnf(c_0_2997,plain,
( ~ p(X16)
| ~ p(X14)
| ~ p(X15)
| ~ p(X17)
| ~ esk270_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk239_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(spm,[status(thm)],[c_0_2991,c_0_2992]) ).
cnf(c_0_2998,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk271_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8)
| esk270_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8) ),
inference(spm,[status(thm)],[c_0_2993,c_0_2933]) ).
cnf(c_0_2999,plain,
( ~ esk219_13(true,X3,X4,true,true,true,X2,true,true,X1,true,true,true)
| p(X4)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2994,c_0_2933]) ).
cnf(c_0_3000,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk219_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk239_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_2995,c_0_2996]) ).
cnf(c_0_3001,plain,
( ~ p(X7)
| ~ p(X5)
| ~ p(X6)
| ~ p(X8)
| ~ esk239_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk271_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8) ),
inference(spm,[status(thm)],[c_0_2997,c_0_2998]) ).
cnf(c_0_3002,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk239_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_2999,c_0_3000]) ).
cnf(c_0_3003,plain,
( ~ p(X7)
| ~ p(X5)
| ~ p(X6)
| ~ p(X8)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk271_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8) ),
inference(spm,[status(thm)],[c_0_3001,c_0_3002]) ).
cnf(c_0_3004,plain,
( ~ p(X7)
| ~ p(X5)
| ~ p(X6)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk271_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,true) ),
inference(spm,[status(thm)],[c_0_3003,c_0_2739]) ).
cnf(c_0_3005,plain,
( ~ esk557_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk574_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_1097]) ).
cnf(c_0_3006,plain,
( ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk557_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_2531]) ).
cnf(c_0_3007,plain,
( ~ esk316_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk289_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk284_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk458_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_170]) ).
cnf(c_0_3008,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk316_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_2360]) ).
cnf(c_0_3009,plain,
( ~ p(X6)
| ~ p(X5)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk271_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,true,X6,true) ),
inference(spm,[status(thm)],[c_0_3004,c_0_2739]) ).
cnf(c_0_3010,plain,
( ~ esk557_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk574_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3005 ).
cnf(c_0_3011,plain,
( ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk557_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3006 ).
cnf(c_0_3012,plain,
( ~ esk310_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk470_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_1900]) ).
cnf(c_0_3013,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk310_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_2219]) ).
cnf(c_0_3014,plain,
( ~ esk316_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk289_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk284_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk458_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3007 ).
cnf(c_0_3015,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk316_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_3008 ).
cnf(c_0_3016,plain,
( ~ p(X5)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk271_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,X5,true) ),
inference(spm,[status(thm)],[c_0_3009,c_0_2739]) ).
cnf(c_0_3017,plain,
( ~ esk574_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk576_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_1228]) ).
cnf(c_0_3018,plain,
( ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk574_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(spm,[status(thm)],[c_0_3010,c_0_3011]) ).
cnf(c_0_3019,plain,
( ~ esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk235_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_1052]) ).
cnf(c_0_3020,plain,
( ~ esk310_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk470_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3012 ).
cnf(c_0_3021,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk310_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_3013 ).
cnf(c_0_3022,plain,
( ~ esk458_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk227_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk459_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_163]) ).
cnf(c_0_3023,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk284_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk289_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk458_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(spm,[status(thm)],[c_0_3014,c_0_3015]) ).
cnf(c_0_3024,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk271_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true) ),
inference(spm,[status(thm)],[c_0_3016,c_0_2739]) ).
cnf(c_0_3025,plain,
( ~ esk576_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk227_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk203_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_1603]) ).
cnf(c_0_3026,plain,
( ~ esk574_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk576_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3017 ).
cnf(c_0_3027,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk574_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12) ),
inference(spm,[status(thm)],[c_0_3018,c_0_2971]) ).
cnf(c_0_3028,plain,
( ~ esk567_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk235_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_3019 ).
cnf(c_0_3029,plain,
( ~ esk470_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk221_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk504_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_1736]) ).
cnf(c_0_3030,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk470_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(spm,[status(thm)],[c_0_3020,c_0_3021]) ).
cnf(c_0_3031,plain,
( ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk221_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_117]) ).
cnf(c_0_3032,plain,
( ~ esk458_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk227_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk459_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3022 ).
cnf(c_0_3033,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk284_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| esk289_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| esk458_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true,X5,X6,X7,X8) ),
inference(spm,[status(thm)],[c_0_3023,c_0_3024]) ).
cnf(c_0_3034,plain,
( ~ esk576_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk227_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk203_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_3025 ).
cnf(c_0_3035,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk576_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12) ),
inference(spm,[status(thm)],[c_0_3026,c_0_3027]) ).
cnf(c_0_3036,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk219_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk235_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk210_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3028,c_0_2980]) ).
cnf(c_0_3037,plain,
( ~ esk470_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk221_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk504_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3029 ).
cnf(c_0_3038,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk471_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true,X5,X6,X7,X8)
| esk470_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true,X5,X6,X7,X8) ),
inference(spm,[status(thm)],[c_0_3030,c_0_3024]) ).
cnf(c_0_3039,plain,
( ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk221_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_3031 ).
cnf(c_0_3040,plain,
( ~ esk459_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk235_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_1920]) ).
cnf(c_0_3041,plain,
( ~ esk227_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk459_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true,X5,X6,X7,X8)
| esk284_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| esk289_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true) ),
inference(spm,[status(thm)],[c_0_3032,c_0_3033]) ).
cnf(c_0_3042,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk227_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk203_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3034,c_0_3035]) ).
cnf(c_0_3043,plain,
( ~ esk220_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk219_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk235_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_2988,c_0_3036]) ).
cnf(c_0_3044,plain,
( ~ esk235_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk504_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_345]) ).
cnf(c_0_3045,plain,
( ~ esk221_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk471_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true,X5,X6,X7,X8)
| esk504_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true,X5,X6,X7,X8) ),
inference(spm,[status(thm)],[c_0_3037,c_0_3038]) ).
cnf(c_0_3046,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk221_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3039,c_0_2971]) ).
cnf(c_0_3047,plain,
( ~ esk332_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk284_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk274_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_2339]) ).
cnf(c_0_3048,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk332_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_455]) ).
cnf(c_0_3049,plain,
( ~ esk459_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk235_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_3040 ).
cnf(c_0_3050,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk459_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true,X5,X6,X7,X8)
| esk284_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| esk289_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| esk203_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3041,c_0_3042]) ).
cnf(c_0_3051,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk219_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk235_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3043,c_0_2996]) ).
cnf(c_0_3052,plain,
( ~ esk235_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk504_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3044 ).
cnf(c_0_3053,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk471_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true,X5,X6,X7,X8)
| esk504_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true,X5,X6,X7,X8) ),
inference(spm,[status(thm)],[c_0_3045,c_0_3046]) ).
cnf(c_0_3054,plain,
( ~ esk473_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk290_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk279_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_269]) ).
cnf(c_0_3055,plain,
( ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk473_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_1240]) ).
cnf(c_0_3056,plain,
( ~ esk332_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk284_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk274_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_3047 ).
cnf(c_0_3057,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk332_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_3048 ).
cnf(c_0_3058,plain,
( ~ esk235_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk284_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| esk289_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| esk203_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3049,c_0_3050]) ).
cnf(c_0_3059,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk235_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_2999,c_0_3051]) ).
cnf(c_0_3060,plain,
( ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk274_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_1305]) ).
cnf(c_0_3061,plain,
( ~ esk235_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk471_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true,X5,X6,X7,X8) ),
inference(spm,[status(thm)],[c_0_3052,c_0_3053]) ).
cnf(c_0_3062,plain,
( ~ esk472_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk291_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk280_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_1677]) ).
cnf(c_0_3063,plain,
( ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk472_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_2180]) ).
cnf(c_0_3064,plain,
( ~ esk279_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk337_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk289_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_1181]) ).
cnf(c_0_3065,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk337_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_1445]) ).
cnf(c_0_3066,plain,
( ~ esk473_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk290_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk279_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_3054 ).
cnf(c_0_3067,plain,
( ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk473_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3055 ).
cnf(c_0_3068,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk274_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk284_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(spm,[status(thm)],[c_0_3056,c_0_3057]) ).
cnf(c_0_3069,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk284_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| esk289_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| esk203_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3058,c_0_3059]) ).
cnf(c_0_3070,plain,
( ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk274_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_3060 ).
cnf(c_0_3071,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk471_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true,X5,X6,X7,X8) ),
inference(spm,[status(thm)],[c_0_3061,c_0_3059]) ).
cnf(c_0_3072,plain,
( ~ esk472_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk291_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk280_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_3062 ).
cnf(c_0_3073,plain,
( ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk472_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3063 ).
cnf(c_0_3074,plain,
( ~ esk279_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk337_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk289_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_3064 ).
cnf(c_0_3075,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk337_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_3065 ).
cnf(c_0_3076,plain,
( ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk279_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk290_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(spm,[status(thm)],[c_0_3066,c_0_3067]) ).
cnf(c_0_3077,plain,
( ~ esk271_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| ~ esk274_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk289_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| esk203_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3068,c_0_3069]) ).
cnf(c_0_3078,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk274_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true) ),
inference(spm,[status(thm)],[c_0_3070,c_0_3071]) ).
cnf(c_0_3079,plain,
( ~ esk280_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk338_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk290_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_1811]) ).
cnf(c_0_3080,plain,
( ~ esk471_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk291_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk280_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(spm,[status(thm)],[c_0_3072,c_0_3073]) ).
cnf(c_0_3081,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk289_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk279_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(spm,[status(thm)],[c_0_3074,c_0_3075]) ).
cnf(c_0_3082,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk279_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| esk290_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true) ),
inference(spm,[status(thm)],[c_0_3076,c_0_3071]) ).
cnf(c_0_3083,plain,
( ~ esk271_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk289_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| esk203_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3077,c_0_3078]) ).
cnf(c_0_3084,plain,
( ~ esk280_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk338_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk290_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_3079 ).
cnf(c_0_3085,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk291_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| esk280_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true) ),
inference(spm,[status(thm)],[c_0_3080,c_0_3071]) ).
cnf(c_0_3086,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk338_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_1766]) ).
cnf(c_0_3087,plain,
( ~ esk271_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| ~ esk289_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk290_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true) ),
inference(spm,[status(thm)],[c_0_3081,c_0_3082]) ).
cnf(c_0_3088,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk289_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| esk203_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3083,c_0_3024]) ).
cnf(c_0_3089,plain,
( ~ esk290_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| ~ esk338_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk291_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true) ),
inference(spm,[status(thm)],[c_0_3084,c_0_3085]) ).
cnf(c_0_3090,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk338_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_3086 ).
cnf(c_0_3091,plain,
( ~ esk271_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk203_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk290_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true) ),
inference(spm,[status(thm)],[c_0_3087,c_0_3088]) ).
cnf(c_0_3092,plain,
( ~ esk328_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk435_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk434_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_347]) ).
cnf(c_0_3093,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk328_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_327]) ).
cnf(c_0_3094,plain,
( ~ esk636_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk653_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_1319]) ).
cnf(c_0_3095,plain,
( ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk636_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_149]) ).
cnf(c_0_3096,plain,
( ~ esk271_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| ~ esk290_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk291_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true) ),
inference(spm,[status(thm)],[c_0_3089,c_0_3090]) ).
cnf(c_0_3097,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk203_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk290_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true) ),
inference(spm,[status(thm)],[c_0_3091,c_0_3024]) ).
cnf(c_0_3098,plain,
( ~ esk328_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk435_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk434_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3092 ).
cnf(c_0_3099,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk328_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_3093 ).
cnf(c_0_3100,plain,
( ~ esk246_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk537_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk213_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_138]) ).
cnf(c_0_3101,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk246_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_346]) ).
cnf(c_0_3102,plain,
( ~ esk636_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk653_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_3094 ).
cnf(c_0_3103,plain,
( ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk636_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3095 ).
cnf(c_0_3104,plain,
( ~ esk281_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk291_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk339_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_2503]) ).
cnf(c_0_3105,plain,
( ~ esk271_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk203_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk291_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true) ),
inference(spm,[status(thm)],[c_0_3096,c_0_3097]) ).
cnf(c_0_3106,plain,
( ~ esk435_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk281_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_676]) ).
cnf(c_0_3107,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk435_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk434_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(spm,[status(thm)],[c_0_3098,c_0_3099]) ).
cnf(c_0_3108,plain,
( ~ esk246_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk537_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk213_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_3100 ).
cnf(c_0_3109,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk246_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_3101 ).
cnf(c_0_3110,plain,
( ~ esk653_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk655_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_1464]) ).
cnf(c_0_3111,plain,
( ~ esk629_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk147_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk653_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(spm,[status(thm)],[c_0_3102,c_0_3103]) ).
cnf(c_0_3112,plain,
( ~ esk552_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk208_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_684]) ).
cnf(c_0_3113,plain,
( ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk552_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_212]) ).
cnf(c_0_3114,plain,
( ~ esk281_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk291_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk339_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_3104 ).
cnf(c_0_3115,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk203_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk291_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true) ),
inference(spm,[status(thm)],[c_0_3105,c_0_3024]) ).
cnf(c_0_3116,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk339_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
inference(fof_simplification,[status(thm)],[i_0_2287]) ).
cnf(c_0_3117,plain,
( ~ p(X17)
| ~ esk434_21(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X2,X3,X1,X18,X19,X20,X21)
| ~ p(X3)
| ~ p(X2)
| ~ p(X1) ),
inference(fof_simplification,[status(thm)],[i_0_1011]) ).
cnf(c_0_3118,plain,
( ~ esk435_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk281_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_3106 ).
cnf(c_0_3119,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk435_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true,X5,X6,X7,X8)
| esk434_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true,X5,X6,X7,X8) ),
inference(spm,[status(thm)],[c_0_3107,c_0_3024]) ).
cnf(c_0_3120,plain,
( ~ esk537_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk156_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk538_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_601]) ).
cnf(c_0_3121,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk213_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk537_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(spm,[status(thm)],[c_0_3108,c_0_3109]) ).
cnf(c_0_3122,plain,
( ~ esk655_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk156_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk132_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_1522]) ).
cnf(c_0_3123,plain,
( ~ esk653_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk655_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3110 ).
cnf(c_0_3124,plain,
( p(X2)
| p(X1)
| p(X3)
| esk147_9(true,X1,X2,true,true,true,X3,true,true)
| esk653_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
inference(spm,[status(thm)],[c_0_3111,c_0_2878]) ).
cnf(c_0_3125,plain,
( ~ esk552_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk208_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_3112 ).
cnf(c_0_3126,plain,
( ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk552_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3113 ).
cnf(c_0_3127,plain,
( ~ esk262_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk213_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk203_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_417]) ).
cnf(c_0_3128,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk262_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_2187]) ).
cnf(c_0_3129,plain,
( ~ esk281_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| ~ esk339_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk203_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3114,c_0_3115]) ).
cnf(c_0_3130,plain,
( ~ esk271_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| esk339_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
c_0_3116 ).
cnf(c_0_3131,plain,
( ~ p(X17)
| ~ esk434_21(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X2,X3,X1,X18,X19,X20,X21)
| ~ p(X3)
| ~ p(X2)
| ~ p(X1) ),
c_0_3117 ).
cnf(c_0_3132,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk281_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| esk434_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true,X5,X6,X7,X8) ),
inference(spm,[status(thm)],[c_0_3118,c_0_3119]) ).
cnf(c_0_3133,plain,
( ~ esk537_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk156_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk538_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3120 ).
cnf(c_0_3134,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk213_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk537_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12) ),
inference(spm,[status(thm)],[c_0_3121,c_0_2933]) ).
cnf(c_0_3135,plain,
( ~ esk655_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk156_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk132_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_3122 ).
cnf(c_0_3136,plain,
( p(X2)
| p(X1)
| p(X3)
| esk147_9(true,X1,X2,true,true,true,X3,true,true)
| esk655_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
inference(spm,[status(thm)],[c_0_3123,c_0_3124]) ).
cnf(c_0_3137,plain,
( ~ esk208_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk267_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_221]) ).
cnf(c_0_3138,plain,
( ~ esk550_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk219_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk208_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(spm,[status(thm)],[c_0_3125,c_0_3126]) ).
cnf(c_0_3139,plain,
( ~ esk262_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk213_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk203_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_3127 ).
cnf(c_0_3140,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk262_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_3128 ).
cnf(c_0_3141,plain,
( ~ esk271_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| ~ esk281_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk203_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3129,c_0_3130]) ).
cnf(c_0_3142,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk281_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3131,c_0_3132]),c_0_2739])]) ).
cnf(c_0_3143,plain,
( ~ esk163_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk538_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(fof_simplification,[status(thm)],[i_0_1318]) ).
cnf(c_0_3144,plain,
( ~ esk156_9(true,X1,X2,true,true,true,X3,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk213_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk538_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12) ),
inference(spm,[status(thm)],[c_0_3133,c_0_3134]) ).
cnf(c_0_3145,plain,
( p(X2)
| p(X1)
| p(X3)
| esk132_9(true,X1,X2,true,true,true,X3,true,true)
| esk147_9(true,X1,X2,true,true,true,X3,true,true)
| esk156_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_3135,c_0_3136]) ).
cnf(c_0_3146,plain,
( ~ esk208_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk267_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk218_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_3137 ).
cnf(c_0_3147,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk219_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk208_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3138,c_0_2971]) ).
cnf(c_0_3148,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk267_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(fof_simplification,[status(thm)],[i_0_1575]) ).
cnf(c_0_3149,plain,
( ~ esk213_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk203_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(spm,[status(thm)],[c_0_3139,c_0_3140]) ).
cnf(c_0_3150,plain,
( ~ esk271_17(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,true,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk203_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3141,c_0_3142]) ).
cnf(c_0_3151,plain,
( ~ esk163_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk538_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
c_0_3143 ).
cnf(c_0_3152,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk213_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk538_21(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12)
| esk132_9(true,X1,X2,true,true,true,X3,true,true)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_3144,c_0_3145]) ).
cnf(c_0_3153,plain,
( ~ esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| ~ esk267_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk219_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3146,c_0_3147]) ).
cnf(c_0_3154,plain,
( ~ esk200_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk267_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
c_0_3148 ).
cnf(c_0_3155,plain,
( ~ esk213_13(true,X3,X4,true,true,true,X2,true,true,X1,true,true,true)
| ~ esk203_13(true,X3,X4,true,true,true,X2,true,true,X1,true,true,true)
| p(X4)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_3149,c_0_2933]) ).
cnf(c_0_3156,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk203_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3150,c_0_3024]) ).
cnf(c_0_3157,plain,
( ~ esk163_9(true,X1,X2,true,true,true,X3,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk213_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk132_9(true,X1,X2,true,true,true,X3,true,true)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_3151,c_0_3152]) ).
cnf(c_0_3158,plain,
( ~ esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| ~ esk200_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk219_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3153,c_0_3154]) ).
cnf(c_0_3159,plain,
( ~ esk213_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3155,c_0_3156]) ).
cnf(c_0_3160,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk213_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk132_9(true,X1,X2,true,true,true,X3,true,true)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_3157,c_0_2963]) ).
cnf(c_0_3161,plain,
( ~ esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk219_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true) ),
inference(spm,[status(thm)],[c_0_3158,c_0_2933]) ).
cnf(c_0_3162,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk218_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk132_9(true,X1,X2,true,true,true,X3,true,true)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_3159,c_0_3160]) ).
cnf(c_0_3163,plain,
( ~ esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk142_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_1724]) ).
cnf(c_0_3164,plain,
( ~ esk142_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk132_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk191_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_2281]) ).
cnf(c_0_3165,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk219_13(true,X1,X2,true,true,true,X3,true,true,X4,true,true,true)
| esk132_9(true,X1,X2,true,true,true,X3,true,true)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_3161,c_0_3162]) ).
cnf(c_0_3166,plain,
( ~ esk597_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk142_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_3163 ).
cnf(c_0_3167,plain,
( ~ esk142_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk132_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| ~ esk191_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_3164 ).
cnf(c_0_3168,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk132_9(true,X1,X2,true,true,true,X3,true,true)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_2999,c_0_3165]) ).
cnf(c_0_3169,plain,
( p(X2)
| p(X1)
| p(X3)
| esk142_9(true,X1,X2,true,true,true,X3,true,true)
| esk596_21(true,X1,X2,true,true,true,X3,true,true,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
inference(spm,[status(thm)],[c_0_3166,c_0_2888]) ).
cnf(c_0_3170,plain,
( ~ esk191_9(true,X1,X2,true,true,true,X3,true,true)
| ~ esk142_9(true,X1,X2,true,true,true,X3,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_3167,c_0_3168]) ).
cnf(c_0_3171,plain,
( p(X2)
| p(X1)
| p(X3)
| esk142_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2892,c_0_3169]),c_0_2739])]) ).
cnf(c_0_3172,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk191_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(fof_simplification,[status(thm)],[i_0_3]) ).
cnf(c_0_3173,plain,
( ~ esk191_9(true,X1,X2,true,true,true,X3,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_3170,c_0_3171]) ).
cnf(c_0_3174,plain,
( ~ esk129_9(X1,X2,X3,X4,X5,X6,X7,X8,X9)
| esk191_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
c_0_3172 ).
cnf(c_0_3175,plain,
( ~ esk129_9(true,X1,X2,true,true,true,X3,true,true)
| p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_3173,c_0_3174]) ).
cnf(c_0_3176,plain,
( p(X2)
| p(X1)
| p(X3)
| p(X4)
| esk147_9(true,X1,X2,true,true,true,X3,true,true) ),
inference(spm,[status(thm)],[c_0_3175,c_0_2855]) ).
cnf(c_0_3177,plain,
( ~ esk196_9(true,X2,X3,true,true,true,X1,true,true)
| p(X4)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_2907,c_0_3176]) ).
cnf(c_0_3178,plain,
( ~ esk129_9(true,X2,X3,true,true,true,X1,true,true)
| p(X4)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_3177,c_0_2914]) ).
cnf(c_0_3179,plain,
( p(X4)
| p(X3)
| p(X2)
| p(X1) ),
inference(spm,[status(thm)],[c_0_3178,c_0_2855]) ).
cnf(c_0_3180,plain,
( p(X3)
| p(X2)
| p(X1) ),
inference(ef,[status(thm)],[c_0_3179]) ).
cnf(c_0_3181,plain,
~ p(false),
inference(fof_simplification,[status(thm)],[rule_false]) ).
cnf(c_0_3182,plain,
( p(X2)
| p(X1) ),
inference(ef,[status(thm)],[c_0_3180]) ).
cnf(c_0_3183,plain,
~ p(false),
c_0_3181 ).
cnf(c_0_3184,plain,
p(X1),
inference(ef,[status(thm)],[c_0_3182]) ).
cnf(c_0_3185,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3183,c_0_3184])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO588-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n008.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 11:58:24 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.42 Running first-order theorem proving
% 0.14/0.42 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 244.79/245.00 % Version: 3.5.1
% 244.79/245.00 % Preprocessing class: FMLMSLSSSSSNFFN.
% 244.79/245.00 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 244.79/245.00 % Starting new_bool_3 with 900s (3) cores
% 244.79/245.00 % Starting new_bool_1 with 900s (3) cores
% 244.79/245.00 % Starting sh5l with 300s (1) cores
% 244.79/245.00 % Starting G-E--_208_C47_F1_SE_CS_SP_PS_S0Y with 300s (1) cores
% 244.79/245.00 % new_bool_1 with pid 930972 completed with status 9
% 244.79/245.00 % new_bool_3 with pid 930971 completed with status 9
% 244.79/245.00 % sh5l with pid 930973 completed with status 9
% 244.79/245.00 % G-E--_208_C47_F1_SE_CS_SP_PS_S0Y with pid 930974 completed with status 0
% 244.79/245.00 % Result found by G-E--_208_C47_F1_SE_CS_SP_PS_S0Y
% 244.79/245.00 % Preprocessing class: FMLMSLSSSSSNFFN.
% 244.79/245.00 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 244.79/245.00 % Starting new_bool_3 with 900s (3) cores
% 244.79/245.00 % Starting new_bool_1 with 900s (3) cores
% 244.79/245.00 % Starting sh5l with 300s (1) cores
% 244.79/245.00 % Starting G-E--_208_C47_F1_SE_CS_SP_PS_S0Y with 300s (1) cores
% 244.79/245.00 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 244.79/245.00 % No SInE strategy applied
% 244.79/245.00 % Search class: FGHSF-SMLF00-SFFFFFNN
% 244.79/245.00 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 244.79/245.00 % Starting SubtermCWHack with 28s (1) cores
% 244.79/245.00 % SubtermCWHack with pid 931014 completed with status 8
% 244.79/245.00 % Starting G-E--_208_C47_F1_SE_CS_SP_PS_S0Y with 31s (1) cores
% 244.79/245.00 % G-E--_208_C47_F1_SE_CS_SP_PS_S0Y with pid 931047 completed with status 8
% 244.79/245.00 % Starting new_bool_3 with 72s (1) cores
% 244.79/245.00 % new_bool_3 with pid 931297 completed with status 8
% 244.79/245.00 % Starting new_bool_1 with 71s (1) cores
% 244.79/245.00 % new_bool_1 with pid 931879 completed with status 8
% 244.79/245.00 % Starting G-E--_208_B07_F1_S5PRR_SE_CS_SP_PS_S0Y with 34s (1) cores
% 244.79/245.00 % G-E--_208_B07_F1_S5PRR_SE_CS_SP_PS_S0Y with pid 932297 completed with status 8
% 244.79/245.00 % Starting H----_011_C07_F1_PI_AE_OS_S1U with 28s (1) cores
% 244.79/245.00 % H----_011_C07_F1_PI_AE_OS_S1U with pid 932452 completed with status 0
% 244.79/245.00 % Result found by H----_011_C07_F1_PI_AE_OS_S1U
% 244.79/245.00 % Preprocessing class: FMLMSLSSSSSNFFN.
% 244.79/245.00 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 244.79/245.00 % Starting new_bool_3 with 900s (3) cores
% 244.79/245.00 % Starting new_bool_1 with 900s (3) cores
% 244.79/245.00 % Starting sh5l with 300s (1) cores
% 244.79/245.00 % Starting G-E--_208_C47_F1_SE_CS_SP_PS_S0Y with 300s (1) cores
% 244.79/245.00 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 244.79/245.00 % No SInE strategy applied
% 244.79/245.00 % Search class: FGHSF-SMLF00-SFFFFFNN
% 244.79/245.00 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 244.79/245.00 % Starting SubtermCWHack with 28s (1) cores
% 244.79/245.00 % SubtermCWHack with pid 931014 completed with status 8
% 244.79/245.00 % Starting G-E--_208_C47_F1_SE_CS_SP_PS_S0Y with 31s (1) cores
% 244.79/245.00 % G-E--_208_C47_F1_SE_CS_SP_PS_S0Y with pid 931047 completed with status 8
% 244.79/245.00 % Starting new_bool_3 with 72s (1) cores
% 244.79/245.00 % new_bool_3 with pid 931297 completed with status 8
% 244.79/245.00 % Starting new_bool_1 with 71s (1) cores
% 244.79/245.00 % new_bool_1 with pid 931879 completed with status 8
% 244.79/245.00 % Starting G-E--_208_B07_F1_S5PRR_SE_CS_SP_PS_S0Y with 34s (1) cores
% 244.79/245.00 % G-E--_208_B07_F1_S5PRR_SE_CS_SP_PS_S0Y with pid 932297 completed with status 8
% 244.79/245.00 % Starting H----_011_C07_F1_PI_AE_OS_S1U with 28s (1) cores
% 244.79/245.00 % Preprocessing time : 0.027 s
% 244.79/245.00
% 244.79/245.00 % Proof found!
% 244.79/245.00 % SZS status Unsatisfiable
% 244.79/245.00 % SZS output start CNFRefutation
% See solution above
% 244.79/245.00 % Parsed axioms : 2569
% 244.79/245.00 % Removed by relevancy pruning/SinE : 0
% 244.79/245.00 % Initial clauses : 2569
% 244.79/245.00 % Removed in clause preprocessing : 0
% 244.79/245.00 % Initial clauses in saturation : 2569
% 244.79/245.00 % Processed clauses : 21864
% 244.79/245.00 % ...of these trivial : 98
% 244.79/245.00 % ...subsumed : 10435
% 244.79/245.00 % ...remaining for further processing : 11331
% 244.79/245.00 % Other redundant clauses eliminated : 0
% 244.79/245.00 % Clauses deleted for lack of memory : 0
% 244.79/245.00 % Backward-subsumed : 7341
% 244.79/245.00 % Backward-rewritten : 962
% 244.79/245.00 % Generated clauses : 45716
% 244.79/245.00 % ...of the previous two non-redundant : 34674
% 244.79/245.00 % ...aggressively subsumed : 0
% 244.79/245.00 % Contextual simplify-reflections : 0
% 244.79/245.00 % Paramodulations : 45456
% 244.79/245.00 % Factorizations : 260
% 244.79/245.00 % NegExts : 0
% 244.79/245.00 % Equation resolutions : 0
% 244.79/245.00 % Disequality decompositions : 0
% 244.79/245.00 % Total rewrite steps : 11327
% 244.79/245.00 % ...of those cached : 11275
% 244.79/245.00 % Propositional unsat checks : 0
% 244.79/245.00 % Propositional check models : 0
% 244.79/245.00 % Propositional check unsatisfiable : 0
% 244.79/245.00 % Propositional clauses : 0
% 244.79/245.00 % Propositional clauses after purity: 0
% 244.79/245.00 % Propositional unsat core size : 0
% 244.79/245.00 % Propositional preprocessing time : 0.000
% 244.79/245.00 % Propositional encoding time : 0.000
% 244.79/245.00 % Propositional solver time : 0.000
% 244.79/245.00 % Success case prop preproc time : 0.000
% 244.79/245.00 % Success case prop encoding time : 0.000
% 244.79/245.00 % Success case prop solver time : 0.000
% 244.79/245.00 % Current number of processed clauses : 3028
% 244.79/245.00 % Positive orientable unit clauses : 9
% 244.79/245.00 % Positive unorientable unit clauses: 0
% 244.79/245.00 % Negative unit clauses : 1
% 244.79/245.00 % Non-unit-clauses : 3018
% 244.79/245.00 % Current number of unprocessed clauses: 5772
% 244.79/245.00 % ...number of literals in the above : 80053
% 244.79/245.00 % Current number of archived formulas : 0
% 244.79/245.00 % Current number of archived clauses : 8303
% 244.79/245.00 % Clause-clause subsumption calls (NU) : 28681373
% 244.79/245.00 % Rec. Clause-clause subsumption calls : 817556
% 244.79/245.00 % Non-unit clause-clause subsumptions : 17753
% 244.79/245.00 % Unit Clause-clause subsumption calls : 22990
% 244.79/245.00 % Rewrite failures with RHS unbound : 0
% 244.79/245.00 % BW rewrite match attempts : 49
% 244.79/245.00 % BW rewrite match successes : 49
% 244.79/245.00 % Condensation attempts : 0
% 244.79/245.00 % Condensation successes : 0
% 244.79/245.00 % Termbank termtop insertions : 1690356
% 244.79/245.00 % Search garbage collected termcells : 3777
% 244.79/245.00
% 244.79/245.00 % -------------------------------------------------
% 244.79/245.00 % User time : 243.180 s
% 244.79/245.00 % System time : 1.273 s
% 244.79/245.00 % Total time : 244.453 s
% 244.79/245.00 % Maximum resident set size: 8388 pages
% 244.79/245.00
% 244.79/245.00 % -------------------------------------------------
% 244.79/245.00 % User time : 243.369 s
% 244.79/245.00 % System time : 1.376 s
% 244.79/245.00 % Total time : 244.745 s
% 244.79/245.00 % Maximum resident set size: 6144 pages
% 244.79/245.00 % E exiting
%------------------------------------------------------------------------------