%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO588-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:28:03 PM UTC 2026
% Result : Unsatisfiable 27.61s 5.38s
% Output : Refutation 32.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 144
% Syntax : Number of formulae : 286 ( 145 unt; 0 def)
% Number of atoms : 517 ( 0 equ)
% Maximal formula atoms : 9 ( 1 avg)
% Number of connectives : 490 ( 259 ~; 231 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 13 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 140 ( 139 usr; 4 prp; 0-21 aty)
% Number of functors : 2 ( 2 usr; 2 con; 0-0 aty)
% Number of variables : 3062 (3062 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk191_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3) ).
fof(f7,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk196_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_7) ).
fof(f22,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk516_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk220_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_22) ).
fof(f27,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk66_5(X0,X1,X2,X3,X4)
| ~ esk125_5(X0,X1,X2,X3,X4)
| ~ esk76_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_27) ).
fof(f37,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk664_21(X1,X2,X3,X4,X5,X6,X0,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_37) ).
fof(f81,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk583_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk163_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_81) ).
fof(f87,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk188_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_87) ).
fof(f117,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk221_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_117) ).
fof(f138,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk537_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk213_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk246_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk218_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_138) ).
fof(f149,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk629_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk636_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_149) ).
fof(f162,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk765_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk41_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_162) ).
fof(f163,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk458_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk459_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk227_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_163) ).
fof(f170,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk458_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk316_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk284_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk289_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_170) ).
fof(f212,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk552_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_212) ).
fof(f221,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk208_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk267_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk218_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_221) ).
fof(f260,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk560_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk219_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk567_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk210_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_260) ).
fof(f266,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk670_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| p(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_266) ).
fof(f267,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk765_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk37_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_267) ).
fof(f269,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk473_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk290_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk279_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_269) ).
fof(f327,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk328_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_327) ).
fof(f333,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk567_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk239_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_333) ).
fof(f346,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk246_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_346) ).
fof(f347,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk435_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk328_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk434_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_347) ).
fof(f361,axiom,
! [X0] :
( ~ esk5_1(X0)
| esk52_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_361) ).
fof(f417,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk262_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk213_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk203_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_417) ).
fof(f449,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk667_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk666_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk128_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ esk668_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk663_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk669_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk670_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk665_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk664_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_449) ).
fof(f455,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk332_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_455) ).
fof(f476,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk516_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk257_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk515_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_476) ).
fof(f478,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk124_5(X0,X1,X2,X3,X4)
| ~ esk65_5(X0,X1,X2,X3,X4)
| ~ esk75_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_478) ).
fof(f481,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk668_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ p(X7)
| p(X6)
| ~ esk95_5(X0,X1,X2,X3,X4)
| ~ p(X8)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_481) ).
fof(f497,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk58_5(X0,X1,X2,X3,X4)
| esk98_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_497) ).
fof(f538,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk628_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk629_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk169_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_538) ).
fof(f553,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk516_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk209_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_553) ).
fof(f590,axiom,
! [X2,X3,X0,X1,X4] :
( esk57_5(X0,X1,X2,X3,X4)
| ~ esk46_1(X0)
| esk58_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_590) ).
fof(f601,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk537_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk156_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk538_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_601) ).
fof(f635,axiom,
( ~ esk1_0
| esk2_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_635) ).
fof(f668,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk197_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ esk148_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ esk138_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_668) ).
fof(f674,axiom,
! [X0] :
( ~ esk4_1(X0)
| ~ p(X0)
| ~ esk2_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_674) ).
fof(f676,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk435_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk281_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_676) ).
fof(f684,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk552_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk208_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk219_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_684) ).
fof(f718,axiom,
! [X0] :
( esk4_1(X0)
| p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_718) ).
fof(f788,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk185_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_788) ).
fof(f816,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk597_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk185_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk596_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_816) ).
fof(f835,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk58_5(X0,X1,X2,X3,X4)
| esk124_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_835) ).
fof(f882,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk750_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk11_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_882) ).
fof(f884,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk746_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk57_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_884) ).
fof(f894,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk668_21(X1,X2,X3,X4,X5,X6,X0,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_894) ).
fof(f905,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk597_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk148_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_905) ).
fof(f921,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk515_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| p(X9)
| ~ p(X11)
| ~ p(X10)
| ~ p(X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_921) ).
fof(f945,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( esk128_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ esk117_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_945) ).
fof(f957,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk58_5(X0,X1,X2,X3,X4)
| esk113_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_957) ).
fof(f1011,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk434_21(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X1,X2,X0,X17,X18,X19,X20)
| ~ p(X1)
| ~ p(X2)
| ~ p(X0)
| ~ p(X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1011) ).
fof(f1023,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk597_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk137_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1023) ).
fof(f1057,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk197_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1057) ).
fof(f1059,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk209_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk219_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk268_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1059) ).
fof(f1073,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk721_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk75_5(X0,X1,X2,X3,X4)
| esk66_5(X0,X1,X2,X3,X4)
| esk722_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1073) ).
fof(f1079,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk665_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1079) ).
fof(f1097,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk557_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk218_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk574_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1097) ).
fof(f1098,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk240_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1098) ).
fof(f1118,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk257_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1118) ).
fof(f1127,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk762_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk21_1(X0)
| esk12_1(X0)
| esk765_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1127) ).
fof(f1132,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk137_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ esk196_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ esk147_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1132) ).
fof(f1147,axiom,
! [X0] :
( ~ esk22_1(X0)
| ~ esk12_1(X0)
| ~ esk53_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1147) ).
fof(f1155,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk677_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| p(X2)
| p(X1)
| ~ p(X4)
| ~ p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1155) ).
fof(f1163,axiom,
! [X0] :
( esk4_1(X0)
| ~ esk3_0
| esk5_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1163) ).
fof(f1165,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk504_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk239_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1165) ).
fof(f1181,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk337_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk289_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk279_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1181) ).
fof(f1228,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk574_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk576_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1228) ).
fof(f1240,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk471_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk473_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1240) ).
fof(f1254,axiom,
! [X0] :
( ~ esk5_1(X0)
| esk45_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1254) ).
fof(f1305,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk471_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk274_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1305) ).
fof(f1318,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk538_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk163_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1318) ).
fof(f1319,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk636_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk147_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk653_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1319) ).
fof(f1342,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( esk270_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk259_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1342) ).
fof(f1431,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk459_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk239_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1431) ).
fof(f1445,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk337_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1445) ).
fof(f1456,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk750_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk26_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1456) ).
fof(f1464,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk653_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk655_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1464) ).
fof(f1467,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk678_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk113_5(X0,X1,X2,X3,X4)
| esk677_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1467) ).
fof(f1499,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk722_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk95_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1499) ).
fof(f1514,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk628_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk662_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk79_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1514) ).
fof(f1522,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk655_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk156_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk132_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1522) ).
fof(f1544,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk629_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk640_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1544) ).
fof(f1555,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk707_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk26_1(X0)
| esk741_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1555) ).
fof(f1573,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk668_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk128_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1573) ).
fof(f1575,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk267_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1575) ).
fof(f1603,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk576_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk203_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk227_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1603) ).
fof(f1677,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk472_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk291_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk280_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1677) ).
fof(f1701,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk269_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1701) ).
fof(f1703,axiom,
esk1_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1703) ).
fof(f1724,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk597_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk142_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1724) ).
fof(f1736,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk470_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk504_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk221_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1736) ).
fof(f1766,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk338_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1766) ).
fof(f1780,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk512_21(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X1,X15,X0,X16,X17,X18,X19,X20)
| ~ p(X1)
| ~ p(X0)
| ~ p(X16)
| ~ esk239_13(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ p(X15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1780) ).
fof(f1809,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk708_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk721_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1809) ).
fof(f1811,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk280_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk338_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk290_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1811) ).
fof(f1895,axiom,
! [X0] :
( ~ esk5_1(X0)
| esk53_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1895) ).
fof(f1900,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk470_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk471_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk310_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1900) ).
fof(f1945,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk549_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk240_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1945) ).
fof(f1956,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk678_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk65_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1956) ).
fof(f1960,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk746_21(X1,X3,X0,X2,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk41_1(X1)
| ~ p(X2)
| p(X0)
| p(X3)
| ~ p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1960) ).
fof(f1964,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk669_21(X1,X2,X3,X4,X5,X0,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1964) ).
fof(f2006,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk259_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2006) ).
fof(f2025,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk750_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk762_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2025) ).
fof(f2128,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk707_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk98_5(X0,X1,X2,X3,X4)
| esk708_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2128) ).
fof(f2143,axiom,
! [X0] :
( ~ esk4_1(X0)
| esk3_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2143) ).
fof(f2151,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk128_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk117_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2151) ).
fof(f2170,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk662_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk95_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2170) ).
fof(f2180,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk471_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk472_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2180) ).
fof(f2187,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk262_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2187) ).
fof(f2216,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk750_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk22_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2216) ).
fof(f2219,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk310_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2219) ).
fof(f2226,axiom,
! [X0] :
( ~ esk11_1(X0)
| ~ esk52_1(X0)
| ~ esk21_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2226) ).
fof(f2229,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk663_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2229) ).
fof(f2245,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk596_21(X4,X5,X6,X7,X8,X0,X3,X2,X1,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2245) ).
fof(f2272,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk269_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk210_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk220_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2272) ).
fof(f2275,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( esk199_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk188_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2275) ).
fof(f2281,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk132_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ esk191_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ esk142_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2281) ).
fof(f2287,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk339_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2287) ).
fof(f2297,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk629_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk150_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2297) ).
fof(f2309,axiom,
! [X0] :
( ~ esk5_1(X0)
| esk46_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2309) ).
fof(f2311,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk678_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk76_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2311) ).
fof(f2328,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk750_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ p(X0)
| ~ esk45_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2328) ).
fof(f2329,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk645_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk167_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2329) ).
fof(f2339,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk332_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk284_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk274_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2339) ).
fof(f2351,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk640_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk645_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk138_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk147_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2351) ).
fof(f2353,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk200_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk268_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2353) ).
fof(f2360,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk271_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk316_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2360) ).
fof(f2369,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk645_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk163_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2369) ).
fof(f2384,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk58_5(X0,X1,X2,X3,X4)
| esk125_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2384) ).
fof(f2402,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk666_21(X1,X2,X3,X4,X5,X6,X7,X0,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2402) ).
fof(f2417,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk549_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk150_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk583_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2417) ).
fof(f2423,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk129_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk169_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2423) ).
fof(f2424,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk667_21(X1,X2,X3,X4,X5,X0,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2424) ).
fof(f2486,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk590_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X0,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ p(X0)
| p(X10)
| ~ p(X11)
| ~ p(X12)
| ~ esk167_9(X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2486) ).
fof(f2487,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk590_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk199_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2487) ).
fof(f2491,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk560_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2491) ).
fof(f2495,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk708_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk79_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2495) ).
fof(f2503,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk291_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk339_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk281_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2503) ).
fof(f2511,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk512_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk270_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2511) ).
fof(f2531,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk550_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk557_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2531) ).
fof(f2561,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk741_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk37_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2561) ).
fof(f2567,axiom,
p(true),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_true) ).
fof(f2568,axiom,
~ p(false),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_false) ).
fof(f2571,plain,
esk2_0,
inference(forward_subsumption_resolution,[],[f635,f1703]) ).
fof(f2578,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk664_21(X0,X1,X2,X3,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f37,f2567]) ).
fof(f2611,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk668_21(X0,X1,X2,X3,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f894,f2567]) ).
fof(f2618,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] : ~ esk434_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,true,true,true,true,X13,X14,X15,X16),
inference(unit_resulting_resolution,[],[f1011,f2567,f2567,f2567,f2567]) ).
fof(f2626,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk665_21(X0,X1,X2,X3,X4,true,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f1079,f2567]) ).
fof(f2670,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk669_21(X0,X1,X2,X3,X4,true,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f1964,f2567]) ).
fof(f2684,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk663_21(X0,X1,X2,X3,X4,X5,true,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f2229,f2567]) ).
fof(f2691,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk666_21(X0,X1,X2,X3,X4,X5,X6,true,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f2402,f2567]) ).
fof(f2693,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk667_21(X0,X1,X2,X3,X4,true,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f2424,f2567]) ).
fof(f2803,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk670_21(X0,X1,X2,X3,X4,X5,X6,X7,false,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f266,f2568]) ).
fof(f2840,plain,
esk4_1(false),
inference(unit_resulting_resolution,[],[f718,f2568]) ).
fof(f2858,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] : ~ esk515_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,false,true,true,true,X9,X10,X11,X12,X13,X14,X15,X16),
inference(unit_resulting_resolution,[],[f921,f2567,f2567,f2567,f2568]) ).
fof(f2881,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] : ~ esk677_21(X0,false,false,true,true,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16),
inference(unit_resulting_resolution,[],[f1155,f2567,f2567,f2568,f2568]) ).
fof(f3006,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] : ~ esk596_21(X0,X1,X2,X3,X4,true,false,true,true,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16),
inference(unit_resulting_resolution,[],[f2245,f2567,f2567,f2567,f2568]) ).
fof(f3045,plain,
esk3_0,
inference(unit_resulting_resolution,[],[f2143,f2840]) ).
fof(f3238,plain,
~ esk4_1(true),
inference(unit_resulting_resolution,[],[f674,f2567,f2571]) ).
fof(f3239,plain,
esk5_1(true),
inference(unit_resulting_resolution,[],[f1163,f3045,f3238]) ).
fof(f3242,plain,
esk52_1(true),
inference(unit_resulting_resolution,[],[f361,f3239]) ).
fof(f3247,plain,
esk45_1(true),
inference(unit_resulting_resolution,[],[f1254,f3239]) ).
fof(f3251,plain,
esk53_1(true),
inference(unit_resulting_resolution,[],[f1895,f3239]) ).
fof(f3252,plain,
esk46_1(true),
inference(unit_resulting_resolution,[],[f2309,f3239]) ).
fof(f3255,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk750_21(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f2328,f2567,f3247]) ).
fof(f3261,plain,
esk11_1(true),
inference(unit_resulting_resolution,[],[f882,f3255]) ).
fof(f3265,plain,
esk26_1(true),
inference(unit_resulting_resolution,[],[f1456,f3255]) ).
fof(f3270,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk762_21(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f2025,f3255]) ).
fof(f3272,plain,
esk22_1(true),
inference(unit_resulting_resolution,[],[f2216,f3255]) ).
fof(f3277,plain,
~ esk21_1(true),
inference(unit_resulting_resolution,[],[f2226,f3261,f3242]) ).
fof(f3279,plain,
~ esk12_1(true),
inference(unit_resulting_resolution,[],[f1147,f3272,f3251]) ).
fof(f3282,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk765_21(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f1127,f3279,f3277,f3270]) ).
fof(f3309,plain,
! [X2,X3,X0,X1,X4] : esk128_9(X0,X1,X2,X3,X4,true,true,true,false),
inference(unit_resulting_resolution,[],[f449,f2578,f2626,f2693,f2670,f2684,f2611,f2691,f2803]) ).
fof(f3364,plain,
! [X2,X3,X0,X1,X4] : esk117_5(X0,X1,X2,X3,X4),
inference(unit_resulting_resolution,[],[f2151,f3309]) ).
fof(f3496,plain,
esk37_1(true),
inference(unit_resulting_resolution,[],[f267,f3282]) ).
fof(f3497,plain,
esk41_1(true),
inference(unit_resulting_resolution,[],[f162,f3282]) ).
fof(f3513,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : ~ esk741_21(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f2561,f3496]) ).
fof(f3522,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : ~ esk746_21(true,false,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15),
inference(unit_resulting_resolution,[],[f1960,f2567,f2568,f2568,f2567,f3497]) ).
fof(f3530,plain,
~ esk57_5(true,false,false,true,true),
inference(unit_resulting_resolution,[],[f884,f3522]) ).
fof(f3535,plain,
esk58_5(true,false,false,true,true),
inference(unit_resulting_resolution,[],[f590,f3252,f3530]) ).
fof(f3537,plain,
esk98_5(true,false,false,true,true),
inference(unit_resulting_resolution,[],[f497,f3535]) ).
fof(f3543,plain,
esk124_5(true,false,false,true,true),
inference(unit_resulting_resolution,[],[f835,f3535]) ).
fof(f3546,plain,
esk113_5(true,false,false,true,true),
inference(unit_resulting_resolution,[],[f957,f3535]) ).
fof(f3564,plain,
esk125_5(true,false,false,true,true),
inference(unit_resulting_resolution,[],[f2384,f3535]) ).
fof(f3567,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : esk678_21(true,false,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15),
inference(unit_resulting_resolution,[],[f1467,f2881,f3546]) ).
fof(f3569,plain,
esk76_5(true,false,false,true,true),
inference(unit_resulting_resolution,[],[f2311,f3567]) ).
fof(f3570,plain,
esk65_5(true,false,false,true,true),
inference(unit_resulting_resolution,[],[f1956,f3567]) ).
fof(f3572,plain,
~ esk75_5(true,false,false,true,true),
inference(unit_resulting_resolution,[],[f478,f3543,f3570]) ).
fof(f3575,plain,
~ esk66_5(true,false,false,true,true),
inference(unit_resulting_resolution,[],[f27,f3564,f3569]) ).
fof(f3667,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : ~ esk707_21(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f1555,f3265,f3513]) ).
fof(f3668,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : esk708_21(true,false,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15),
inference(unit_resulting_resolution,[],[f2128,f3537,f3667]) ).
fof(f3682,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : esk721_21(true,false,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15),
inference(unit_resulting_resolution,[],[f1809,f3668]) ).
fof(f3686,plain,
esk79_5(true,false,false,true,true),
inference(unit_resulting_resolution,[],[f2495,f3668]) ).
fof(f3702,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : esk722_21(true,false,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15),
inference(unit_resulting_resolution,[],[f1073,f3575,f3572,f3682]) ).
fof(f3738,plain,
esk95_5(true,false,false,true,true),
inference(unit_resulting_resolution,[],[f1499,f3702]) ).
fof(f3741,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ~ esk668_21(true,false,false,true,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f481,f2567,f2567,f2567,f2568,f3738]) ).
fof(f3754,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : ~ esk662_21(true,false,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15),
inference(unit_resulting_resolution,[],[f2170,f3738]) ).
fof(f3774,plain,
~ esk128_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f1573,f3741]) ).
fof(f3776,plain,
esk129_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f945,f3364,f3774]) ).
fof(f3777,plain,
esk191_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f3,f3776]) ).
fof(f3778,plain,
esk196_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f7,f3776]) ).
fof(f3779,plain,
esk188_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f87,f3776]) ).
fof(f3787,plain,
esk185_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f788,f3776]) ).
fof(f3790,plain,
esk197_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f1057,f3776]) ).
fof(f3805,plain,
esk169_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f2423,f3776]) ).
fof(f3874,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk597_21(true,false,false,true,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f816,f3006,f3787]) ).
fof(f3875,plain,
esk137_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f1023,f3874]) ).
fof(f3876,plain,
esk142_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f1724,f3874]) ).
fof(f3877,plain,
esk148_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f905,f3874]) ).
fof(f3882,plain,
~ esk138_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f668,f3790,f3877]) ).
fof(f3887,plain,
~ esk147_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f1132,f3778,f3875]) ).
fof(f3891,plain,
~ esk132_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f2281,f3777,f3876]) ).
fof(f4114,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : ~ esk628_21(true,false,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15),
inference(unit_resulting_resolution,[],[f1514,f3686,f3754]) ).
fof(f4118,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk629_21(true,false,false,true,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f538,f3805,f4114]) ).
fof(f4134,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk636_21(true,false,false,true,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f149,f4118]) ).
fof(f4144,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk640_21(true,false,false,true,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f1544,f4118]) ).
fof(f4147,plain,
esk150_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f2297,f4118]) ).
fof(f4240,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk653_21(true,false,false,true,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f1319,f3887,f4134]) ).
fof(f4241,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk655_21(true,false,false,true,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f1464,f4240]) ).
fof(f4244,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk645_21(true,false,false,true,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f2351,f3887,f3882,f4144]) ).
fof(f4246,plain,
esk163_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f2369,f4244]) ).
fof(f4247,plain,
esk167_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f2329,f4244]) ).
fof(f4248,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ~ esk583_21(true,false,false,true,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f81,f4246]) ).
fof(f4255,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ~ esk538_21(true,false,false,true,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f1318,f4246]) ).
fof(f4273,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : ~ esk590_21(true,false,false,true,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f2486,f2567,f2567,f2567,f2568,f4247]) ).
fof(f4279,plain,
~ esk199_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f2487,f4273]) ).
fof(f4282,plain,
esk200_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f2275,f3779,f4279]) ).
fof(f4285,plain,
esk246_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f346,f4282]) ).
fof(f4296,plain,
esk240_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f1098,f4282]) ).
fof(f4297,plain,
esk257_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f1118,f4282]) ).
fof(f4300,plain,
esk267_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f1575,f4282]) ).
fof(f4303,plain,
esk269_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f1701,f4282]) ).
fof(f4308,plain,
esk259_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f2006,f4282]) ).
fof(f4311,plain,
esk262_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f2187,f4282]) ).
fof(f4312,plain,
esk268_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f2353,f4282]) ).
fof(f4377,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk516_21(true,false,false,true,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f476,f2858,f4297]) ).
fof(f4379,plain,
esk220_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f22,f4377]) ).
fof(f4381,plain,
esk209_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f553,f4377]) ).
fof(f4384,plain,
~ esk219_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f1059,f4312,f4381]) ).
fof(f4392,plain,
~ esk210_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f2272,f4303,f4379]) ).
fof(f4467,plain,
esk156_9(true,false,false,true,true,true,false,true,true),
inference(unit_resulting_resolution,[],[f1522,f3891,f4241]) ).
fof(f5512,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ~ esk549_21(true,false,false,true,true,true,false,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f2417,f4147,f4248]) ).
fof(f5515,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk550_21(true,false,false,true,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f1945,f4296,f5512]) ).
fof(f5534,plain,
esk221_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f117,f5515]) ).
fof(f5536,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk552_21(true,false,false,true,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f212,f5515]) ).
fof(f5545,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk560_21(true,false,false,true,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f2491,f5515]) ).
fof(f5546,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk557_21(true,false,false,true,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f2531,f5515]) ).
fof(f5587,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk567_21(true,false,false,true,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f260,f4392,f4384,f5545]) ).
fof(f5589,plain,
esk239_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f333,f5587]) ).
fof(f5593,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : ~ esk504_21(true,false,false,true,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f1165,f5589]) ).
fof(f5596,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : ~ esk459_21(true,false,false,true,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f1431,f5589]) ).
fof(f5601,plain,
! [X2,X3,X0,X1] : ~ esk512_21(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f1780,f2567,f2567,f2567,f2567,f5589]) ).
fof(f5649,plain,
esk208_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f684,f4384,f5536]) ).
fof(f5652,plain,
~ esk218_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f221,f4300,f5649]) ).
fof(f5655,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk574_21(true,false,false,true,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f1097,f5546,f5652]) ).
fof(f5658,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk576_21(true,false,false,true,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f1228,f5655]) ).
fof(f5665,plain,
~ esk270_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f2511,f5601]) ).
fof(f5691,plain,
esk271_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f1342,f4308,f5665]) ).
fof(f5696,plain,
esk328_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f327,f5691]) ).
fof(f5697,plain,
esk332_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f455,f5691]) ).
fof(f5709,plain,
esk337_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f1445,f5691]) ).
fof(f5713,plain,
esk338_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f1766,f5691]) ).
fof(f5717,plain,
esk310_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f2219,f5691]) ).
fof(f5718,plain,
esk339_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f2287,f5691]) ).
fof(f5720,plain,
esk316_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f2360,f5691]) ).
fof(f5723,plain,
! [X2,X3,X0,X1] : esk435_21(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f347,f2618,f5696]) ).
fof(f5725,plain,
esk281_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f676,f5723]) ).
fof(f5736,plain,
~ esk291_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f2503,f5718,f5725]) ).
fof(f5996,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : ~ esk470_21(true,false,false,true,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f1736,f5534,f5593]) ).
fof(f5999,plain,
! [X2,X3,X0,X1] : esk471_21(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f1900,f5717,f5996]) ).
fof(f6006,plain,
! [X2,X3,X0,X1] : esk473_21(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f1240,f5999]) ).
fof(f6007,plain,
esk274_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f1305,f5999]) ).
fof(f6010,plain,
! [X2,X3,X0,X1] : esk472_21(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f2180,f5999]) ).
fof(f6033,plain,
~ esk284_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f2339,f5697,f6007]) ).
fof(f6049,plain,
esk280_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f1677,f5736,f6010]) ).
fof(f6052,plain,
~ esk290_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f1811,f5713,f6049]) ).
fof(f6075,plain,
esk279_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f269,f6052,f6006]) ).
fof(f6079,plain,
~ esk289_17(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f1181,f5709,f6075]) ).
fof(f6081,plain,
! [X2,X3,X0,X1] : esk458_21(true,false,false,true,true,true,false,true,true,false,true,true,true,true,true,true,true,X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f170,f6033,f5720,f6079]) ).
fof(f6084,plain,
~ esk227_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f163,f5596,f6081]) ).
fof(f6087,plain,
esk203_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f1603,f5658,f6084]) ).
fof(f6091,plain,
~ esk213_13(true,false,false,true,true,true,false,true,true,false,true,true,true),
inference(unit_resulting_resolution,[],[f417,f4311,f6087]) ).
fof(f6096,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk537_21(true,false,false,true,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f138,f5652,f4285,f6091]) ).
fof(f6106,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk538_21(true,false,false,true,true,true,false,true,true,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f601,f4467,f6096]) ).
fof(f6107,plain,
$false,
inference(forward_subsumption_resolution,[],[f6106,f4255]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO588-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.21 % Computer : n016.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Mon Sep 28 17:56:03 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.26 Running first-order theorem proving
% 0.10/0.26 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.23/3.24 % (3841441)Input is clausal, will run a generic CNF schedule.
% 17.23/3.24 % (3841561)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3383629633:i=140167_2998 on theBenchmark for (2998ds/140167Mi)
% 17.23/3.24 % (3841564)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1687744868:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2998 on theBenchmark for (2998ds/137899Mi)
% 17.23/3.24 % (3841562)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2884223807:i=132376:av=off_2998 on theBenchmark for (2998ds/132376Mi)
% 17.23/3.24 % (3841570)dis-21_1_sil=8000:lcm=predicate:random_seed=1771467468:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/117Mi)
% 17.23/3.24 % (3841567)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1498833176:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2998 on theBenchmark for (2998ds/114Mi)
% 17.23/3.24 % (3841568)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3247470958:s2a=on:i=180:gtg=position_2998 on theBenchmark for (2998ds/180Mi)
% 17.23/3.24 % (3841565)lrs+10_1_sil=8000:sp=occurrence:random_seed=409413430:i=107:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/107Mi)
% 17.23/3.24 % (3841565)Refutation not found, incomplete strategy
% 17.23/3.24 % (3841565)------------------------------
% 17.23/3.24 % (3841565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.23/3.24 % (3841565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.23/3.24 % (3841565)CaDiCaL version: 2.1.3
% 17.23/3.24 % (3841565)Termination reason: Refutation not found, incomplete strategy
% 17.23/3.24 % (3841565)Time elapsed: 0.009 s
% 17.23/3.24 % (3841565)Peak memory usage: 88 MB
% 17.23/3.24 % (3841565)Instructions burned: 7 (million)
% 17.23/3.24 % (3841567)Refutation not found, incomplete strategy
% 17.23/3.24 % (3841567)------------------------------
% 17.23/3.24 % (3841567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.23/3.24 % (3841567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.23/3.24 % (3841567)CaDiCaL version: 2.1.3
% 17.23/3.24 % (3841567)Termination reason: Refutation not found, incomplete strategy
% 17.23/3.24 % (3841567)Time elapsed: 0.012 s
% 17.23/3.24 % (3841567)Peak memory usage: 88 MB
% 17.23/3.24 % (3841567)Instructions burned: 11 (million)
% 17.23/3.24 % (3841570)Instruction limit reached!
% 17.23/3.24 % (3841570)------------------------------
% 17.23/3.24 % (3841570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.23/3.24 % (3841570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.23/3.24 % (3841570)CaDiCaL version: 2.1.3
% 17.23/3.24 % (3841570)Termination reason: Instruction limit
% 17.23/3.24 % (3841570)Termination phase: Saturation
% 17.23/3.24 % (3841570)Time elapsed: 0.084 s
% 17.23/3.24 % (3841570)Peak memory usage: 89 MB
% 17.23/3.24 % (3841570)Instructions burned: 117 (million)
% 17.23/3.24 % (3841568)Instruction limit reached!
% 17.23/3.24 % (3841568)------------------------------
% 17.23/3.24 % (3841568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.23/3.24 % (3841568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.23/3.24 % (3841568)CaDiCaL version: 2.1.3
% 17.23/3.24 % (3841568)Termination reason: Instruction limit
% 17.23/3.24 % (3841568)Termination phase: Saturation
% 17.23/3.24 % (3841568)Time elapsed: 0.141 s
% 17.23/3.24 % (3841568)Peak memory usage: 90 MB
% 17.23/3.24 % (3841568)Instructions burned: 181 (million)
% 17.23/3.24 % (3841612)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1496320213:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi)
% 17.23/3.24 % (3841612)Refutation not found, incomplete strategy
% 17.23/3.24 % (3841612)------------------------------
% 17.23/3.24 % (3841612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.23/3.24 % (3841612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.23/3.24 % (3841612)CaDiCaL version: 2.1.3
% 17.23/3.24 % (3841612)Termination reason: Refutation not found, incomplete strategy
% 17.23/3.24 % (3841612)Time elapsed: 0.008 s
% 17.23/3.24 % (3841612)Peak memory usage: 88 MB
% 17.23/3.24 % (3841612)Instructions burned: 8 (million)
% 17.23/3.24 % (3841567)------------------------------
% 27.61/5.38 % (3841567)------------------------------
% 27.61/5.38 % (3841565)------------------------------
% 27.61/5.38 % (3841565)------------------------------
% 27.61/5.38 % (3841614)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3178466659:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 27.61/5.38 % (3841614)Refutation not found, incomplete strategy
% 27.61/5.38 % (3841614)------------------------------
% 27.61/5.38 % (3841614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.61/5.38 % (3841614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.61/5.38 % (3841614)CaDiCaL version: 2.1.3
% 27.61/5.38 % (3841614)Termination reason: Refutation not found, incomplete strategy
% 27.61/5.38 % (3841614)Time elapsed: 0.018 s
% 27.61/5.38 % (3841614)Peak memory usage: 88 MB
% 27.61/5.38 % (3841614)Instructions burned: 19 (million)
% 27.61/5.38 % (3841619)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=591099250:st=4:i=219:sd=3:ss=axioms_2992 on theBenchmark for (2992ds/219Mi)
% 27.61/5.38 % (3841619)Refutation not found, incomplete strategy
% 27.61/5.38 % (3841619)------------------------------
% 27.61/5.38 % (3841619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.61/5.38 % (3841619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.61/5.38 % (3841619)CaDiCaL version: 2.1.3
% 27.61/5.38 % (3841619)Termination reason: Refutation not found, incomplete strategy
% 27.61/5.38 % (3841619)Time elapsed: 0.006 s
% 27.61/5.38 % (3841619)Peak memory usage: 88 MB
% 27.61/5.38 % (3841619)Instructions burned: 11 (million)
% 27.61/5.38 % (3841620)lrs+10_64_to=lpo:sil=8000:random_seed=1445117473:i=126:bd=preordered_2992 on theBenchmark for (2992ds/126Mi)
% 27.61/5.38 % (3841612)------------------------------
% 27.61/5.38 % (3841612)------------------------------
% 27.61/5.38 % (3841620)Instruction limit reached!
% 27.61/5.38 % (3841620)------------------------------
% 27.61/5.38 % (3841620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.61/5.38 % (3841620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.61/5.38 % (3841620)CaDiCaL version: 2.1.3
% 27.61/5.38 % (3841620)Termination reason: Instruction limit
% 27.61/5.38 % (3841620)Termination phase: Saturation
% 27.61/5.38 % (3841620)Time elapsed: 0.112 s
% 27.61/5.38 % (3841620)Peak memory usage: 91 MB
% 27.61/5.38 % (3841620)Instructions burned: 126 (million)
% 27.61/5.38 % (3841614)------------------------------
% 27.61/5.38 % (3841614)------------------------------
% 27.61/5.38 % (3841619)------------------------------
% 27.61/5.38 % (3841619)------------------------------
% 27.61/5.38 % (3841632)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3904718761:avsq=on:i=194:fgj=on:bd=preordered_2989 on theBenchmark for (2989ds/194Mi)
% 27.61/5.38 % (3841635)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1483132528:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 27.61/5.38 % (3841633)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2067550295:i=157:gtg=all_2988 on theBenchmark for (2988ds/157Mi)
% 27.61/5.38 % (3841635)Refutation not found, incomplete strategy
% 27.61/5.38 % (3841635)------------------------------
% 27.61/5.38 % (3841635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.61/5.38 % (3841635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.61/5.38 % (3841635)CaDiCaL version: 2.1.3
% 27.61/5.38 % (3841635)Termination reason: Refutation not found, incomplete strategy
% 27.61/5.38 % (3841635)Time elapsed: 0.008 s
% 27.61/5.38 % (3841635)Peak memory usage: 88 MB
% 27.61/5.38 % (3841635)Instructions burned: 14 (million)
% 27.61/5.38 % (3841634)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2471626948:i=3394:sd=4:ss=included:sgt=64_2988 on theBenchmark for (2988ds/3394Mi)
% 27.61/5.38 % (3841633)Instruction limit reached!
% 27.61/5.38 % (3841633)------------------------------
% 27.61/5.38 % (3841633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.61/5.38 % (3841633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.61/5.38 % (3841633)CaDiCaL version: 2.1.3
% 27.61/5.38 % (3841633)Termination reason: Instruction limit
% 27.61/5.38 % (3841633)Termination phase: Saturation
% 27.61/5.38 % (3841633)Time elapsed: 0.129 s
% 27.61/5.38 % (3841633)Peak memory usage: 91 MB
% 27.61/5.38 % (3841633)Instructions burned: 157 (million)
% 27.61/5.38 % (3841632)Instruction limit reached!
% 27.61/5.38 % (3841632)------------------------------
% 27.61/5.38 % (3841632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.61/5.38 % (3841632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.61/5.38 % (3841632)CaDiCaL version: 2.1.3
% 27.61/5.38 % (3841632)Termination reason: Instruction limit
% 27.61/5.38 % (3841632)Termination phase: Saturation
% 27.61/5.38 % (3841632)Time elapsed: 0.179 s
% 27.61/5.38 % (3841632)Peak memory usage: 93 MB
% 27.61/5.38 % (3841632)Instructions burned: 194 (million)
% 27.61/5.38 % (3841645)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1773726242:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2984 on theBenchmark for (2984ds/242Mi)
% 27.61/5.38 % (3841644)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=47456459:i=107_2984 on theBenchmark for (2984ds/107Mi)
% 27.61/5.38 % (3841635)------------------------------
% 27.61/5.38 % (3841635)------------------------------
% 27.61/5.38 % (3841644)Instruction limit reached!
% 27.61/5.38 % (3841644)------------------------------
% 27.61/5.38 % (3841644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.61/5.38 % (3841644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.61/5.38 % (3841644)CaDiCaL version: 2.1.3
% 27.61/5.38 % (3841644)Termination reason: Instruction limit
% 27.61/5.38 % (3841644)Termination phase: Saturation
% 27.61/5.38 % (3841644)Time elapsed: 0.076 s
% 27.61/5.38 % (3841644)Peak memory usage: 91 MB
% 27.61/5.38 % (3841644)Instructions burned: 108 (million)
% 27.61/5.38 % (3841645)Instruction limit reached!
% 27.61/5.38 % (3841645)------------------------------
% 27.61/5.38 % (3841645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.61/5.38 % (3841645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.61/5.38 % (3841645)CaDiCaL version: 2.1.3
% 27.61/5.38 % (3841645)Termination reason: Instruction limit
% 27.61/5.38 % (3841645)Termination phase: Saturation
% 27.61/5.38 % (3841645)Time elapsed: 0.099 s
% 27.61/5.38 % (3841645)Peak memory usage: 91 MB
% 27.61/5.38 % (3841645)Instructions burned: 244 (million)
% 27.61/5.38 % (3841656)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=444031923:i=499:bd=all_2981 on theBenchmark for (2981ds/499Mi)
% 27.61/5.38 % (3841652)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4215085938:cond=fast:i=5208:av=off_2982 on theBenchmark for (2982ds/5208Mi)
% 27.61/5.38 % (3841654)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3988439796:i=134:sd=2:doe=on:ss=axioms:sgt=14_2982 on theBenchmark for (2982ds/134Mi)
% 27.61/5.38 % (3841654)Refutation not found, incomplete strategy
% 27.61/5.38 % (3841654)------------------------------
% 27.61/5.38 % (3841654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.61/5.38 % (3841654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.61/5.38 % (3841654)CaDiCaL version: 2.1.3
% 27.61/5.38 % (3841654)Termination reason: Refutation not found, incomplete strategy
% 27.61/5.38 % (3841654)Time elapsed: 0.009 s
% 27.61/5.38 % (3841654)Peak memory usage: 88 MB
% 27.61/5.38 % (3841654)Instructions burned: 8 (million)
% 27.61/5.38 % (3841656)Instruction limit reached!
% 27.61/5.38 % (3841656)------------------------------
% 27.61/5.38 % (3841656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.61/5.38 % (3841656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.61/5.38 % (3841656)CaDiCaL version: 2.1.3
% 27.61/5.38 % (3841656)Termination reason: Instruction limit
% 27.61/5.38 % (3841656)Termination phase: Saturation
% 27.61/5.38 % (3841656)Time elapsed: 0.232 s
% 27.61/5.38 % (3841656)Peak memory usage: 97 MB
% 27.61/5.38 % (3841656)Instructions burned: 500 (million)
% 27.61/5.38 % (3841662)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1795102242:i=191:fgj=on:bd=all_2978 on theBenchmark for (2978ds/191Mi)
% 27.61/5.38 % (3841654)------------------------------
% 27.61/5.38 % (3841654)------------------------------
% 27.61/5.38 % (3841662)Instruction limit reached!
% 27.61/5.38 % (3841662)------------------------------
% 27.61/5.38 % (3841662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.61/5.38 % (3841662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.61/5.38 % (3841662)CaDiCaL version: 2.1.3
% 27.61/5.38 % (3841662)Termination reason: Instruction limit
% 27.61/5.38 % (3841662)Termination phase: Saturation
% 27.61/5.38 % (3841662)Time elapsed: 0.090 s
% 27.61/5.38 % (3841662)Peak memory usage: 93 MB
% 27.61/5.38 % (3841662)Instructions burned: 191 (million)
% 27.61/5.38 % (3841668)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3621823772:i=264:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/264Mi)
% 27.61/5.38 % (3841671)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4191401496:cond=on:i=156:bs=on:gtg=exists_all:er=known_2974 on theBenchmark for (2974ds/156Mi)
% 27.61/5.38 % (3841671)Instruction limit reached!
% 27.61/5.38 % (3841671)------------------------------
% 27.61/5.38 % (3841671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.61/5.38 % (3841671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.61/5.38 % (3841671)CaDiCaL version: 2.1.3
% 27.61/5.38 % (3841671)Termination reason: Instruction limit
% 27.61/5.38 % (3841671)Termination phase: Saturation
% 27.61/5.38 % (3841671)Time elapsed: 0.069 s
% 27.61/5.38 % (3841671)Peak memory usage: 92 MB
% 27.61/5.38 % (3841671)Instructions burned: 157 (million)
% 27.61/5.38 % (3841668)Instruction limit reached!
% 27.61/5.38 % (3841668)------------------------------
% 27.61/5.38 % (3841668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.61/5.38 % (3841668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.61/5.38 % (3841668)CaDiCaL version: 2.1.3
% 27.61/5.38 % (3841668)Termination reason: Instruction limit
% 27.61/5.38 % (3841668)Termination phase: Saturation
% 27.61/5.38 % (3841668)Time elapsed: 0.215 s
% 27.61/5.38 % (3841668)Peak memory usage: 94 MB
% 27.61/5.38 % (3841668)Instructions burned: 264 (million)
% 27.61/5.38 % (3841674)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1131983908:i=3256:kws=precedence:bd=preordered:av=off_2971 on theBenchmark for (2971ds/3256Mi)
% 27.61/5.38 % (3841677)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2078145847:i=537:av=off:ss=included_2970 on theBenchmark for (2970ds/537Mi)
% 27.61/5.38 % (3841677)Instruction limit reached!
% 27.61/5.38 % (3841677)------------------------------
% 27.61/5.38 % (3841677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.61/5.38 % (3841677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.61/5.38 % (3841677)CaDiCaL version: 2.1.3
% 27.61/5.38 % (3841677)Termination reason: Instruction limit
% 27.61/5.38 % (3841677)Termination phase: Saturation
% 27.61/5.38 % (3841677)Time elapsed: 0.409 s
% 27.61/5.38 % (3841677)Peak memory usage: 94 MB
% 27.61/5.38 % (3841677)Instructions burned: 538 (million)
% 27.61/5.38 % (3841684)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2632108977:i=180:bd=preordered:av=off_2964 on theBenchmark for (2964ds/180Mi)
% 27.61/5.38 % (3841684)Instruction limit reached!
% 27.61/5.38 % (3841684)------------------------------
% 27.61/5.38 % (3841684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.61/5.38 % (3841684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.61/5.38 % (3841684)CaDiCaL version: 2.1.3
% 27.61/5.38 % (3841684)Termination reason: Instruction limit
% 27.61/5.38 % (3841684)Termination phase: Saturation
% 27.61/5.38 % (3841684)Time elapsed: 0.156 s
% 27.61/5.38 % (3841684)Peak memory usage: 93 MB
% 27.61/5.38 % (3841684)Instructions burned: 180 (million)
% 27.61/5.38 % (3841562)First to succeed.
% 27.61/5.38 % (3841562)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3841441"
% 27.61/5.38 % (3841688)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2697310342:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2960 on theBenchmark for (2960ds/10307Mi)
% 27.61/5.38 % (3841562)Refutation found. Thanks to Tanya!
% 27.61/5.38 % SZS status Unsatisfiable for theBenchmark
% 27.61/5.38 % SZS output start Proof for theBenchmark
% See solution above
% 32.43/5.50 % (3841562)------------------------------
% 32.43/5.50 % (3841562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.43/5.50 % (3841562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.43/5.50 % (3841562)CaDiCaL version: 2.1.3
% 32.43/5.50 % (3841562)Termination reason: Refutation
% 32.43/5.50 % (3841562)Time elapsed: 3.799 s
% 32.43/5.50 % (3841562)Peak memory usage: 282 MB
% 32.43/5.50 % (3841562)Instructions burned: 3539 (million)
% 32.43/5.50 % (3841562)------------------------------
% 32.43/5.50 % (3841562)------------------------------
% 32.43/5.50 % (3841441)Success in time 4.653 s
% 32.43/5.50 % Vampire exiting
%------------------------------------------------------------------------------