%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO589-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 : n001.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 78.14s 17.26s
% Output : Refutation 0.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 199
% Syntax : Number of formulae : 396 ( 200 unt; 0 def)
% Number of atoms : 717 ( 0 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 684 ( 363 ~; 321 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 36 ( 17 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 198 ( 197 usr; 4 prp; 0-29 aty)
% Number of functors : 2 ( 2 usr; 2 con; 0-0 aty)
% Number of variables : 5640 (5640 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f68,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1482_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk28_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_68) ).
fof(f200,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk840_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk598_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| esk591_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| ~ esk636_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_200) ).
fof(f245,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1442_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk129_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_245) ).
fof(f268,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1264_29(X1,X2,X3,X4,X5,X6,X0,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ p(X0)
| p(X7)
| ~ p(X8)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_268) ).
fof(f295,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk474_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| 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_295) ).
fof(f313,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk857_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk577_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_313) ).
fof(f323,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk202_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ esk188_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ esk271_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_323) ).
fof(f389,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1196_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1206_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_389) ).
fof(f400,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1005_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1007_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_400) ).
fof(f414,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1356_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk123_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_414) ).
fof(f454,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( esk374_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk375_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk359_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_454) ).
fof(f463,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1219_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk323_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_463) ).
fof(f478,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk375_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk458_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_478) ).
fof(f481,axiom,
! [X0] :
( ~ esk71_1(X0)
| ~ esk14_1(X0)
| ~ esk28_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_481) ).
fof(f485,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk953_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk538_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk492_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk499_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_485) ).
fof(f520,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk177_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk260_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_520) ).
fof(f535,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk1380_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1379_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk155_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_535) ).
fof(f563,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1422_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1441_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_563) ).
fof(f573,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1231_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1233_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_573) ).
fof(f576,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk487_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk570_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk501_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_576) ).
fof(f578,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk474_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk530_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_578) ).
fof(f601,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk171_5(X0,X1,X2,X3,X4)
| ~ esk102_5(X0,X1,X2,X3,X4)
| ~ esk88_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_601) ).
fof(f673,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1118_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1120_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_673) ).
fof(f687,axiom,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk659_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| ~ esk577_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| ~ esk591_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_687) ).
fof(f692,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1442_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk123_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_692) ).
fof(f705,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1007_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk478_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk511_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_705) ).
fof(f833,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk386_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk469_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk400_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_833) ).
fof(f883,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk1421_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1422_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk134_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_883) ).
fof(f963,axiom,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk585_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| ~ esk667_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| ~ esk599_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_963) ).
fof(f1014,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk970_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk972_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1014) ).
fof(f1023,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1308_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk107_5(X0,X1,X2,X3,X4)
| esk1356_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1023) ).
fof(f1031,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk954_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk429_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_1031) ).
fof(f1059,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk857_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk858_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1059) ).
fof(f1086,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1047_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk387_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_1086) ).
fof(f1126,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk1066_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk439_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk400_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk393_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_1126) ).
fof(f1176,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk804_29(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X0,X23,X24,X25,X26,X27,X28)
| ~ p(X0)
| ~ p(X24)
| ~ p(X23)
| ~ p(X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1176) ).
fof(f1228,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk474_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk568_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(f1302,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk970_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk973_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1302) ).
fof(f1307,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1083_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1086_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1307) ).
fof(f1318,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk916_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk572_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1318) ).
fof(f1326,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk375_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk439_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_1326) ).
fof(f1365,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk1082_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk431_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk1083_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1365) ).
fof(f1372,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1364_29(X1,X2,X3,X4,X5,X6,X0,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk129_5(X1,X2,X3,X4,X5)
| ~ p(X6)
| ~ p(X0)
| p(X7)
| ~ p(X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1372) ).
fof(f1399,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1046_29(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X0,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ p(X0)
| ~ p(X15)
| p(X16)
| ~ p(X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1399) ).
fof(f1424,axiom,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk669_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| ~ esk601_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| ~ esk587_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1424) ).
fof(f1463,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1379_29(X1,X2,X3,X0,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| p(X0)
| ~ p(X4)
| ~ p(X3)
| p(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1463) ).
fof(f1465,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1233_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk280_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk313_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1465) ).
fof(f1503,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk177_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk270_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1503) ).
fof(f1519,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1083_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1093_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1519) ).
fof(f1538,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1150_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk287_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1538) ).
fof(f1574,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1482_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk13_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1574) ).
fof(f1625,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk375_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk469_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_1625) ).
fof(f1687,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk280_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk294_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk363_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1687) ).
fof(f1695,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1195_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1243_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk206_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1695) ).
fof(f1720,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk995_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk529_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_1720) ).
fof(f1735,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk370_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk301_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk287_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1735) ).
fof(f1767,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk276_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk332_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1767) ).
fof(f1803,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1066_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1067_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk313_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1803) ).
fof(f1834,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1107_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk429_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_1834) ).
fof(f1842,axiom,
( esk3_0
| ~ esk1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1842) ).
fof(f1929,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk470_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk387_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk401_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_1929) ).
fof(f1963,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk78_5(X0,X1,X2,X3,X4)
| esk161_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1963) ).
fof(f1976,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk841_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk523_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_1976) ).
fof(f1990,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk970_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk503_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_1990) ).
fof(f2027,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1422_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk107_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2027) ).
fof(f2090,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1083_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk404_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_2090) ).
fof(f2100,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk78_5(X0,X1,X2,X3,X4)
| esk155_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2100) ).
fof(f2139,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1150_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk294_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2139) ).
fof(f2147,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk919_29(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X2,X3,X1,X0,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2147) ).
fof(f2169,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1309_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk206_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2169) ).
fof(f2205,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1441_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk101_5(X0,X1,X2,X3,X4)
| esk88_5(X0,X1,X2,X3,X4)
| esk1442_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2205) ).
fof(f2307,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk984_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk501_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk995_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk488_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_2307) ).
fof(f2309,axiom,
! [X0] :
( ~ esk5_1(X0)
| esk62_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2309) ).
fof(f2350,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1476_29(X1,X2,X3,X0,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| p(X0)
| p(X2)
| ~ p(X4)
| ~ p(X3)
| ~ esk55_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2350) ).
fof(f2357,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1500_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk14_1(X0)
| esk1503_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk27_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2357) ).
fof(f2411,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1130_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk323_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2411) ).
fof(f2430,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk276_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk371_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2430) ).
fof(f2453,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk388_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk402_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk471_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_2453) ).
fof(f2459,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1326_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk188_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk201_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk1331_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2459) ).
fof(f2485,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk840_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk511_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk841_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2485) ).
fof(f2486,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk187_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ esk201_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ esk270_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2486) ).
fof(f2491,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk857_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk859_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2491) ).
fof(f2508,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk920_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk487_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_2508) ).
fof(f2535,axiom,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk573_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| esk659_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2535) ).
fof(f2578,axiom,
! [X0] :
( ~ esk5_1(X0)
| esk61_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2578) ).
fof(f2579,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1503_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk49_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2579) ).
fof(f2642,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk474_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk570_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_2642) ).
fof(f2654,axiom,
! [X0] :
( ~ esk4_1(X0)
| ~ p(X0)
| ~ esk2_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2654) ).
fof(f2669,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1028_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X19,X18,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| p(X17)
| ~ p(X18)
| ~ p(X19)
| ~ esk429_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ p(X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2669) ).
fof(f2672,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk916_29(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X23,X22,X0,X24,X25,X26,X27,X28)
| ~ esk529_21(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ p(X22)
| ~ p(X0)
| ~ p(X23)
| ~ p(X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2672) ).
fof(f2774,axiom,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk666_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| ~ esk598_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| ~ esk584_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2774) ).
fof(f2779,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1150_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk302_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2779) ).
fof(f2787,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk1195_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1196_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk332_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2787) ).
fof(f2831,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1017_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk429_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_2831) ).
fof(f2832,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk276_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk363_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2832) ).
fof(f2848,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk1028_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ 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_2848) ).
fof(f2853,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk1482_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk61_1(X0)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2853) ).
fof(f2863,axiom,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk573_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| esk666_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2863) ).
fof(f2875,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1380_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk102_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2875) ).
fof(f2877,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1134_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X15,X16,X14,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ p(X13)
| p(X14)
| ~ p(X15)
| ~ p(X16)
| ~ esk323_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2877) ).
fof(f2948,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk995_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk523_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_2948) ).
fof(f2974,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)
| ~ esk458_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk474_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_2974) ).
fof(f2985,axiom,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk573_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| esk667_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2985) ).
fof(f3022,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk569_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk500_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk486_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_3022) ).
fof(f3098,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk1134_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk374_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_3098) ).
fof(f3124,axiom,
! [X2,X3,X0,X1,X4] :
( esk77_5(X0,X1,X2,X3,X4)
| esk78_5(X0,X1,X2,X3,X4)
| ~ esk62_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3124) ).
fof(f3180,axiom,
( ~ esk1_0
| esk2_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3180) ).
fof(f3189,axiom,
! [X0] :
( ~ esk70_1(X0)
| ~ esk13_1(X0)
| ~ esk27_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3189) ).
fof(f3246,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk474_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk555_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_3246) ).
fof(f3256,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk375_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk470_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_3256) ).
fof(f3257,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk474_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_3257) ).
fof(f3272,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk78_5(X0,X1,X2,X3,X4)
| esk170_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3272) ).
fof(f3273,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk568_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk485_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk499_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_3273) ).
fof(f3310,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1196_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk305_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3310) ).
fof(f3337,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk276_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk359_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3337) ).
fof(f3339,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk1047_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1046_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk449_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_3339) ).
fof(f3354,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1120_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk379_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk412_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_3354) ).
fof(f3355,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk904_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk523_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_3355) ).
fof(f3387,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk1476_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk77_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3387) ).
fof(f3405,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk859_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk600_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| esk585_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3405) ).
fof(f3417,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk972_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk501_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk486_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_3417) ).
fof(f3419,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1082_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1130_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk305_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3419) ).
fof(f3421,axiom,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk573_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| esk628_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3421) ).
fof(f3456,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk970_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk984_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3456) ).
fof(f3506,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk980_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk499_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk1005_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3506) ).
fof(f3511,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( esk176_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk177_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ esk161_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3511) ).
fof(f3609,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( esk275_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk276_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk260_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3609) ).
fof(f3620,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1331_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk229_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3620) ).
fof(f3649,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1206_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1231_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk301_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3649) ).
fof(f3666,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk1252_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk275_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3666) ).
fof(f3667,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk1265_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1264_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk255_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3667) ).
fof(f3723,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1380_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk87_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3723) ).
fof(f3761,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1083_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1098_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3761) ).
fof(f3836,axiom,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] :
( esk572_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| esk573_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| ~ 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_3836) ).
fof(f3845,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk474_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk561_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_3845) ).
fof(f3846,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk177_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk255_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3846) ).
fof(f3847,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk805_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk654_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| esk804_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3847) ).
fof(f3911,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk920_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk502_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_3911) ).
fof(f4005,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk474_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk571_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_4005) ).
fof(f4007,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk1150_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1149_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk355_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4007) ).
fof(f4013,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1309_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1326_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4013) ).
fof(f4023,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk371_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk288_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| ~ esk302_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4023) ).
fof(f4033,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1469_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk49_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4033) ).
fof(f4051,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1212_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1219_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk288_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk301_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4051) ).
fof(f4120,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk970_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk980_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4120) ).
fof(f4152,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk375_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk431_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_4152) ).
fof(f4153,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk858_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk601_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| esk586_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4153) ).
fof(f4161,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1482_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1500_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4161) ).
fof(f4169,axiom,
! [X0] :
( esk4_1(X0)
| ~ esk3_0
| esk5_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4169) ).
fof(f4236,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk969_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1017_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk404_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_4236) ).
fof(f4241,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk78_5(X0,X1,X2,X3,X4)
| esk134_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4241) ).
fof(f4308,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk561_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk492_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk478_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_4308) ).
fof(f4360,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1503_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk55_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4360) ).
fof(f4361,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1067_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk323_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4361) ).
fof(f4362,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1086_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk386_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk401_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_4362) ).
fof(f4378,axiom,
! [X0] :
( ~ esk5_1(X0)
| esk71_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4378) ).
fof(f4401,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk1364_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk176_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4401) ).
fof(f4412,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk973_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk500_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk485_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_4412) ).
fof(f4419,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk856_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk503_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk904_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4419) ).
fof(f4436,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1265_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk202_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4436) ).
fof(f4438,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1243_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk229_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4438) ).
fof(f4446,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk856_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk628_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| esk857_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4446) ).
fof(f4575,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk1308_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk233_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk1309_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4575) ).
fof(f4579,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk474_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk569_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_4579) ).
fof(f4596,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1421_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1469_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk34_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4596) ).
fof(f4614,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk857_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk860_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4614) ).
fof(f4632,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1149_29(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X0,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| p(X0)
| ~ p(X11)
| ~ p(X12)
| p(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4632) ).
fof(f4633,axiom,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk573_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| esk668_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4633) ).
fof(f4649,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1252_29(X3,X4,X5,X6,X7,X8,X9,X10,X11,X2,X12,X1,X0,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ p(X1)
| p(X2)
| ~ esk229_9(X3,X4,X5,X6,X7,X8,X9,X10,X11)
| p(X12)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4649) ).
fof(f4657,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1047_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk402_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_4657) ).
fof(f4772,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1482_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk34_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4772) ).
fof(f4786,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk170_5(X0,X1,X2,X3,X4)
| ~ esk101_5(X0,X1,X2,X3,X4)
| ~ esk87_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4786) ).
fof(f4798,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1265_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk187_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4798) ).
fof(f4813,axiom,
esk1_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4813) ).
fof(f4835,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk571_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk488_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| ~ esk502_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_4835) ).
fof(f4903,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1196_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk1212_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4903) ).
fof(f4938,axiom,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk573_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| esk636_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4938) ).
fof(f4939,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk375_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk449_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_4939) ).
fof(f4941,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk920_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk919_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk555_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_4941) ).
fof(f4981,axiom,
! [X0] :
( ~ esk5_1(X0)
| esk70_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4981) ).
fof(f4993,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk379_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk393_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk462_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_4993) ).
fof(f5058,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk375_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk462_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_5058) ).
fof(f5074,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( esk969_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk530_21(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20)
| esk970_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_5074) ).
fof(f5110,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk276_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk355_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_5110) ).
fof(f5120,axiom,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk573_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| esk654_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_5120) ).
fof(f5123,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1093_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk400_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk1118_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_5123) ).
fof(f5182,axiom,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk573_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| esk669_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_5182) ).
fof(f5200,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk375_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk471_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_5200) ).
fof(f5239,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk860_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk584_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| esk599_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_5239) ).
fof(f5258,axiom,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk668_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| ~ esk586_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)
| ~ esk600_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_5258) ).
fof(f5264,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk78_5(X0,X1,X2,X3,X4)
| esk171_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_5264) ).
fof(f5353,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk177_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk233_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_5353) ).
fof(f5393,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk953_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk954_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| ~ esk412_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_5393) ).
fof(f5394,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ esk177_9(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| esk271_9(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_5394) ).
fof(f5451,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk805_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk587_25(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_5451) ).
fof(f5458,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ esk276_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
| esk370_13(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_5458) ).
fof(f5484,axiom,
! [X2,X21,X28,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] :
( ~ esk1098_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk388_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk1107_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28)
| esk401_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_5484) ).
fof(f5507,axiom,
p(true),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_true) ).
fof(f5508,axiom,
~ p(false),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_false) ).
fof(f5510,plain,
esk2_0,
inference(forward_subsumption_resolution,[],[f3180,f4813]) ).
fof(f5511,plain,
esk3_0,
inference(forward_subsumption_resolution,[],[f1842,f4813]) ).
fof(f5858,plain,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] : ~ esk1264_29(X0,X1,X2,X3,X4,true,true,false,true,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24),
inference(unit_resulting_resolution,[],[f268,f5507,f5507,f5508,f5507]) ).
fof(f5917,plain,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] : ~ esk804_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,true,true,true,true,X21,X22,X23,X24),
inference(unit_resulting_resolution,[],[f1176,f5507,f5507,f5507,f5507]) ).
fof(f5938,plain,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] : ~ esk1046_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,true,true,true,false,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24),
inference(unit_resulting_resolution,[],[f1399,f5507,f5508,f5507,f5507]) ).
fof(f5944,plain,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] : ~ esk1379_29(X0,false,true,false,true,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24),
inference(unit_resulting_resolution,[],[f1463,f5508,f5507,f5508,f5507]) ).
fof(f6005,plain,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] : ~ esk919_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,true,true,true,X17,X18,X19,X20,X21,X22,X23,X24),
inference(unit_resulting_resolution,[],[f2147,f5507,f5507,f5508,f5507]) ).
fof(f6218,plain,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] : ~ esk1149_29(X0,X1,X2,X3,X4,X5,X6,X7,X8,false,false,true,true,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24),
inference(unit_resulting_resolution,[],[f4632,f5508,f5508,f5507,f5507]) ).
fof(f6856,plain,
~ esk4_1(true),
inference(unit_resulting_resolution,[],[f2654,f5507,f5510]) ).
fof(f6857,plain,
esk5_1(true),
inference(unit_resulting_resolution,[],[f4169,f5511,f6856]) ).
fof(f6866,plain,
esk62_1(true),
inference(unit_resulting_resolution,[],[f2309,f6857]) ).
fof(f6868,plain,
esk61_1(true),
inference(unit_resulting_resolution,[],[f2578,f6857]) ).
fof(f6873,plain,
esk71_1(true),
inference(unit_resulting_resolution,[],[f4378,f6857]) ).
fof(f6875,plain,
esk70_1(true),
inference(unit_resulting_resolution,[],[f4981,f6857]) ).
fof(f6877,plain,
! [X2,X21,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] : esk1482_29(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27),
inference(unit_resulting_resolution,[],[f2853,f5507,f6868]) ).
fof(f6878,plain,
esk28_1(true),
inference(unit_resulting_resolution,[],[f68,f6877]) ).
fof(f6885,plain,
esk13_1(true),
inference(unit_resulting_resolution,[],[f1574,f6877]) ).
fof(f6895,plain,
! [X2,X21,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] : esk1500_29(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27),
inference(unit_resulting_resolution,[],[f4161,f6877]) ).
fof(f6897,plain,
esk34_1(true),
inference(unit_resulting_resolution,[],[f4772,f6877]) ).
fof(f6901,plain,
~ esk14_1(true),
inference(unit_resulting_resolution,[],[f481,f6873,f6878]) ).
fof(f6906,plain,
~ esk27_1(true),
inference(unit_resulting_resolution,[],[f3189,f6875,f6885]) ).
fof(f6994,plain,
! [X2,X21,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] : esk1503_29(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27),
inference(unit_resulting_resolution,[],[f2357,f6906,f6901,f6895]) ).
fof(f7071,plain,
esk55_1(true),
inference(unit_resulting_resolution,[],[f4360,f6994]) ).
fof(f7072,plain,
esk49_1(true),
inference(unit_resulting_resolution,[],[f2579,f6994]) ).
fof(f7084,plain,
! [X2,X21,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] : ~ esk1469_29(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27),
inference(unit_resulting_resolution,[],[f4033,f7072]) ).
fof(f7097,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20,X23] : ~ esk1476_29(true,false,true,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23),
inference(unit_resulting_resolution,[],[f2350,f5508,f5507,f5507,f5508,f7071]) ).
fof(f7115,plain,
~ esk77_5(true,false,true,false,true),
inference(unit_resulting_resolution,[],[f3387,f7097]) ).
fof(f7118,plain,
esk78_5(true,false,true,false,true),
inference(unit_resulting_resolution,[],[f3124,f6866,f7115]) ).
fof(f7135,plain,
esk161_5(true,false,true,false,true),
inference(unit_resulting_resolution,[],[f1963,f7118]) ).
fof(f7136,plain,
esk155_5(true,false,true,false,true),
inference(unit_resulting_resolution,[],[f2100,f7118]) ).
fof(f7142,plain,
esk170_5(true,false,true,false,true),
inference(unit_resulting_resolution,[],[f3272,f7118]) ).
fof(f7150,plain,
esk134_5(true,false,true,false,true),
inference(unit_resulting_resolution,[],[f4241,f7118]) ).
fof(f7158,plain,
esk171_5(true,false,true,false,true),
inference(unit_resulting_resolution,[],[f5264,f7118]) ).
fof(f7162,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20,X23] : esk1380_29(true,false,true,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23),
inference(unit_resulting_resolution,[],[f535,f5944,f7136]) ).
fof(f7164,plain,
esk102_5(true,false,true,false,true),
inference(unit_resulting_resolution,[],[f2875,f7162]) ).
fof(f7165,plain,
esk87_5(true,false,true,false,true),
inference(unit_resulting_resolution,[],[f3723,f7162]) ).
fof(f7170,plain,
~ esk101_5(true,false,true,false,true),
inference(unit_resulting_resolution,[],[f4786,f7142,f7165]) ).
fof(f7173,plain,
~ esk88_5(true,false,true,false,true),
inference(unit_resulting_resolution,[],[f601,f7158,f7164]) ).
fof(f7274,plain,
! [X2,X21,X0,X11,X18,X6,X9,X16,X27,X4,X15,X22,X25,X13,X20,X3,X10,X1,X8,X19,X26,X7,X14,X17,X24,X5,X12,X23] : ~ esk1421_29(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27),
inference(unit_resulting_resolution,[],[f4596,f6897,f7084]) ).
fof(f7277,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20,X23] : esk1422_29(true,false,true,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23),
inference(unit_resulting_resolution,[],[f883,f7150,f7274]) ).
fof(f7280,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20,X23] : esk1441_29(true,false,true,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23),
inference(unit_resulting_resolution,[],[f563,f7277]) ).
fof(f7291,plain,
esk107_5(true,false,true,false,true),
inference(unit_resulting_resolution,[],[f2027,f7277]) ).
fof(f7345,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20,X23] : esk1442_29(true,false,true,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23),
inference(unit_resulting_resolution,[],[f2205,f7173,f7170,f7280]) ).
fof(f7426,plain,
esk123_5(true,false,true,false,true),
inference(unit_resulting_resolution,[],[f692,f7345]) ).
fof(f7427,plain,
esk129_5(true,false,true,false,true),
inference(unit_resulting_resolution,[],[f245,f7345]) ).
fof(f7428,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20,X23] : ~ esk1356_29(true,false,true,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23),
inference(unit_resulting_resolution,[],[f414,f7426]) ).
fof(f7449,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : ~ esk1364_29(true,false,true,false,true,true,true,false,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,[],[f1372,f5507,f5508,f5507,f5507,f7427]) ).
fof(f7468,plain,
~ esk176_9(true,false,true,false,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f4401,f7449]) ).
fof(f7470,plain,
esk177_9(true,false,true,false,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f3511,f7135,f7468]) ).
fof(f7473,plain,
esk260_9(true,false,true,false,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f520,f7470]) ).
fof(f7481,plain,
esk270_9(true,false,true,false,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f1503,f7470]) ).
fof(f7500,plain,
esk255_9(true,false,true,false,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f3846,f7470]) ).
fof(f7512,plain,
esk233_9(true,false,true,false,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f5353,f7470]) ).
fof(f7513,plain,
esk271_9(true,false,true,false,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f5394,f7470]) ).
fof(f7581,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk1265_29(true,false,true,false,true,true,true,false,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,[],[f3667,f5858,f7500]) ).
fof(f7584,plain,
esk187_9(true,false,true,false,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f4798,f7581]) ).
fof(f7585,plain,
esk202_9(true,false,true,false,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f4436,f7581]) ).
fof(f7586,plain,
~ esk188_9(true,false,true,false,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f323,f7513,f7585]) ).
fof(f7598,plain,
~ esk201_9(true,false,true,false,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f2486,f7584,f7481]) ).
fof(f7837,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20,X23] : ~ esk1308_29(true,false,true,false,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23),
inference(unit_resulting_resolution,[],[f1023,f7291,f7428]) ).
fof(f7840,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk1309_29(true,false,true,false,true,true,true,false,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,[],[f4575,f7512,f7837]) ).
fof(f7850,plain,
esk206_9(true,false,true,false,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f2169,f7840]) ).
fof(f7857,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk1326_29(true,false,true,false,true,true,true,false,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,[],[f4013,f7840]) ).
fof(f7888,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk1331_29(true,false,true,false,true,true,true,false,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,[],[f2459,f7598,f7586,f7857]) ).
fof(f7890,plain,
esk229_9(true,false,true,false,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f3620,f7888]) ).
fof(f7903,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : ~ esk1243_29(true,false,true,false,true,true,true,false,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,[],[f4438,f7890]) ).
fof(f7905,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : ~ esk1252_29(true,false,true,false,true,true,true,false,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,[],[f4649,f5507,f5508,f5507,f5508,f7890]) ).
fof(f8047,plain,
~ esk275_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f3666,f7905]) ).
fof(f8050,plain,
esk276_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f3609,f7473,f8047]) ).
fof(f8065,plain,
esk332_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f1767,f8050]) ).
fof(f8070,plain,
esk371_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f2430,f8050]) ).
fof(f8073,plain,
esk363_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f2832,f8050]) ).
fof(f8076,plain,
esk359_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f3337,f8050]) ).
fof(f8089,plain,
esk355_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f5110,f8050]) ).
fof(f8093,plain,
esk370_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f5458,f8050]) ).
fof(f8188,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : esk1150_29(true,false,true,false,true,true,true,false,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,[],[f4007,f6218,f8089]) ).
fof(f8189,plain,
esk294_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f2139,f8188]) ).
fof(f8190,plain,
esk287_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f1538,f8188]) ).
fof(f8191,plain,
esk302_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f2779,f8188]) ).
fof(f8197,plain,
~ esk288_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f4023,f8070,f8191]) ).
fof(f8201,plain,
~ esk280_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f1687,f8073,f8189]) ).
fof(f8205,plain,
~ esk301_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f1735,f8093,f8190]) ).
fof(f8400,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : ~ esk1195_29(true,false,true,false,true,true,true,false,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,[],[f1695,f7850,f7903]) ).
fof(f8403,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : esk1196_29(true,false,true,false,true,true,true,false,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,[],[f2787,f8065,f8400]) ).
fof(f8429,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : esk1206_29(true,false,true,false,true,true,true,false,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,[],[f389,f8403]) ).
fof(f8440,plain,
esk305_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f3310,f8403]) ).
fof(f8445,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : esk1212_29(true,false,true,false,true,true,true,false,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,[],[f4903,f8403]) ).
fof(f8536,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : esk1219_29(true,false,true,false,true,true,true,false,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,[],[f4051,f8205,f8197,f8445]) ).
fof(f8538,plain,
esk323_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f463,f8536]) ).
fof(f8545,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : ~ esk1130_29(true,false,true,false,true,true,true,false,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,[],[f2411,f8538]) ).
fof(f8546,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ~ esk1134_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f2877,f5507,f5507,f5507,f5508,f8538]) ).
fof(f8555,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : ~ esk1067_29(true,false,true,false,true,true,true,false,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,[],[f4361,f8538]) ).
fof(f8579,plain,
~ esk374_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f3098,f8546]) ).
fof(f8581,plain,
esk375_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f454,f8076,f8579]) ).
fof(f8584,plain,
esk458_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f478,f8581]) ).
fof(f8595,plain,
esk439_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f1326,f8581]) ).
fof(f8597,plain,
esk469_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f1625,f8581]) ).
fof(f8615,plain,
esk470_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f3256,f8581]) ).
fof(f8617,plain,
esk431_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f4152,f8581]) ).
fof(f8621,plain,
esk449_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f4939,f8581]) ).
fof(f8622,plain,
esk462_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f5058,f8581]) ).
fof(f8624,plain,
esk471_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f5200,f8581]) ).
fof(f8629,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : esk1231_29(true,false,true,false,true,true,true,false,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,[],[f3649,f8205,f8429]) ).
fof(f8630,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : esk1233_29(true,false,true,false,true,true,true,false,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,[],[f573,f8629]) ).
fof(f8833,plain,
esk313_13(true,false,true,false,true,true,true,false,true,false,false,true,true),
inference(unit_resulting_resolution,[],[f1465,f8201,f8630]) ).
fof(f8951,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk1047_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f3339,f5938,f8621]) ).
fof(f8953,plain,
esk387_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f1086,f8951]) ).
fof(f8955,plain,
esk402_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f4657,f8951]) ).
fof(f8960,plain,
~ esk388_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f2453,f8624,f8955]) ).
fof(f8967,plain,
~ esk401_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f1929,f8615,f8953]) ).
fof(f9762,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : ~ esk1082_29(true,false,true,false,true,true,true,false,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,[],[f3419,f8440,f8545]) ).
fof(f9765,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk1083_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f1365,f8617,f9762]) ).
fof(f9793,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk1086_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f1307,f9765]) ).
fof(f9795,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk1093_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f1519,f9765]) ).
fof(f9797,plain,
esk404_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f2090,f9765]) ).
fof(f9802,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk1098_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f3761,f9765]) ).
fof(f9910,plain,
esk386_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f4362,f8967,f9793]) ).
fof(f9913,plain,
~ esk400_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f833,f8597,f9910]) ).
fof(f9924,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk1107_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f5484,f8967,f8960,f9802]) ).
fof(f9927,plain,
esk429_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f1834,f9924]) ).
fof(f9931,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ~ esk954_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f1031,f9927]) ).
fof(f9936,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : ~ esk1028_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f2669,f5507,f5508,f5507,f5507,f9927]) ).
fof(f9939,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ~ esk1017_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f2831,f9927]) ).
fof(f9965,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk1118_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f5123,f9913,f9795]) ).
fof(f9966,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk1120_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f673,f9965]) ).
fof(f10030,plain,
~ esk473_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f2848,f9936]) ).
fof(f10077,plain,
esk474_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f2974,f8584,f10030]) ).
fof(f10080,plain,
esk538_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f295,f10077]) ).
fof(f10081,plain,
esk530_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f578,f10077]) ).
fof(f10088,plain,
esk568_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f1228,f10077]) ).
fof(f10100,plain,
esk570_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f2642,f10077]) ).
fof(f10101,plain,
esk555_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f3246,f10077]) ).
fof(f10102,plain,
esk557_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f3257,f10077]) ).
fof(f10105,plain,
esk561_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f3845,f10077]) ).
fof(f10109,plain,
esk571_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f4005,f10077]) ).
fof(f10111,plain,
esk569_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f4579,f10077]) ).
fof(f10146,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk920_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f4941,f6005,f10101]) ).
fof(f10148,plain,
esk502_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f3911,f10146]) ).
fof(f10150,plain,
esk487_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f2508,f10146]) ).
fof(f10153,plain,
~ esk488_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f4835,f10109,f10148]) ).
fof(f10162,plain,
~ esk501_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f576,f10100,f10150]) ).
fof(f10482,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] : ~ esk1066_29(true,false,true,false,true,true,true,false,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,[],[f1803,f8833,f8555]) ).
fof(f10484,plain,
esk393_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f1126,f9913,f8595,f10482]) ).
fof(f10494,plain,
~ esk379_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f4993,f8622,f10484]) ).
fof(f10505,plain,
esk412_17(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false),
inference(unit_resulting_resolution,[],[f3354,f9966,f10494]) ).
fof(f13153,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ~ esk969_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f4236,f9797,f9939]) ).
fof(f13156,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk970_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f5074,f10081,f13153]) ).
fof(f13158,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk972_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f1014,f13156]) ).
fof(f13159,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk973_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f1302,f13156]) ).
fof(f13162,plain,
esk503_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f1990,f13156]) ).
fof(f13169,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk984_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f3456,f13156]) ).
fof(f13172,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk980_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f4120,f13156]) ).
fof(f13178,plain,
esk486_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f3417,f10162,f13158]) ).
fof(f13181,plain,
~ esk500_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f3022,f10111,f13178]) ).
fof(f13186,plain,
esk485_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f4412,f13159,f13181]) ).
fof(f13189,plain,
~ esk499_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f3273,f10088,f13186]) ).
fof(f13197,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk1005_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f3506,f13189,f13172]) ).
fof(f13198,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk1007_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f400,f13197]) ).
fof(f13202,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : esk995_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f2307,f10153,f10162,f13169]) ).
fof(f13204,plain,
esk529_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f1720,f13202]) ).
fof(f13205,plain,
esk523_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f2948,f13202]) ).
fof(f13211,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : ~ esk841_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f1976,f13205]) ).
fof(f13216,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : ~ esk904_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f3355,f13205]) ).
fof(f13232,plain,
! [X2,X3,X0,X1] : ~ esk916_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true,X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f2672,f5507,f5507,f5507,f5507,f13204]) ).
fof(f13241,plain,
~ esk572_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f1318,f13232]) ).
fof(f13303,plain,
esk573_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f3836,f10102,f13241]) ).
fof(f13319,plain,
esk659_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f2535,f13303]) ).
fof(f13325,plain,
esk666_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f2863,f13303]) ).
fof(f13326,plain,
esk667_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f2985,f13303]) ).
fof(f13327,plain,
esk628_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f3421,f13303]) ).
fof(f13336,plain,
esk668_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f4633,f13303]) ).
fof(f13341,plain,
esk636_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f4938,f13303]) ).
fof(f13343,plain,
esk654_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f5120,f13303]) ).
fof(f13344,plain,
esk669_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f5182,f13303]) ).
fof(f13347,plain,
! [X2,X3,X0,X1] : esk805_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true,X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f3847,f5917,f13343]) ).
fof(f13349,plain,
esk587_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f5451,f13347]) ).
fof(f13356,plain,
~ esk601_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f1424,f13344,f13349]) ).
fof(f13449,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ~ esk953_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f5393,f10505,f9931]) ).
fof(f13450,plain,
esk492_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f485,f13189,f10080,f13449]) ).
fof(f13456,plain,
~ esk478_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f4308,f10105,f13450]) ).
fof(f13460,plain,
esk511_21(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f705,f13198,f13456]) ).
fof(f28432,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : ~ esk856_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7),
inference(unit_resulting_resolution,[],[f4419,f13162,f13216]) ).
fof(f28435,plain,
! [X2,X3,X0,X1] : esk857_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true,X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f4446,f13327,f28432]) ).
fof(f28439,plain,
esk577_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f313,f28435]) ).
fof(f28442,plain,
! [X2,X3,X0,X1] : esk858_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true,X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f1059,f28435]) ).
fof(f28448,plain,
! [X2,X3,X0,X1] : esk859_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true,X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f2491,f28435]) ).
fof(f28454,plain,
! [X2,X3,X0,X1] : esk860_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true,X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f4614,f28435]) ).
fof(f28481,plain,
~ esk591_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f687,f13319,f28439]) ).
fof(f28485,plain,
esk586_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f4153,f13356,f28442]) ).
fof(f28488,plain,
~ esk600_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f5258,f13336,f28485]) ).
fof(f28491,plain,
esk585_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f3405,f28448,f28488]) ).
fof(f28496,plain,
~ esk599_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f963,f13326,f28491]) ).
fof(f28513,plain,
esk584_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f5239,f28496,f28454]) ).
fof(f28516,plain,
~ esk598_25(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f2774,f13325,f28513]) ).
fof(f28517,plain,
! [X2,X3,X0,X1] : esk840_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true,X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f200,f13341,f28481,f28516]) ).
fof(f28530,plain,
! [X2,X3,X0,X1] : esk841_29(true,false,true,false,true,true,true,false,true,false,false,true,true,true,true,true,false,false,true,true,true,true,true,true,true,X0,X1,X2,X3),
inference(unit_resulting_resolution,[],[f2485,f13460,f28517]) ).
fof(f28531,plain,
$false,
inference(forward_subsumption_resolution,[],[f28530,f13211]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO589-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.26 % Computer : n001.cluster.edu
% 0.09/0.26 % Model : x86_64 x86_64
% 0.09/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.26 % Memory : 8046.5625MB
% 0.09/0.26 % OS : Linux 6.8.0-71-generic
% 0.09/0.26 % CPULimit : 300
% 0.09/0.26 % WCLimit : 300
% 0.09/0.26 % DateTime : Mon Sep 28 17:57:03 UTC 2026
% 0.09/0.27 % CPUTime :
% 0.09/0.27 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.32 Running first-order theorem proving
% 0.25/0.32 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
% 21.39/4.35 % (572586)Input is clausal, will run a generic CNF schedule.
% 21.39/4.35 % (572597)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3371259397:i=132376:av=off_2996 on theBenchmark for (2996ds/132376Mi)
% 21.39/4.35 % (572599)lrs+10_1_sil=8000:sp=occurrence:random_seed=3745521579:i=107:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/107Mi)
% 21.39/4.35 % (572599)Refutation not found, incomplete strategy
% 21.39/4.35 % (572599)------------------------------
% 21.39/4.35 % (572599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.39/4.35 % (572599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.39/4.35 % (572599)CaDiCaL version: 2.1.3
% 21.39/4.35 % (572599)Termination reason: Refutation not found, incomplete strategy
% 21.39/4.35 % (572599)Time elapsed: 0.021 s
% 21.39/4.35 % (572599)Peak memory usage: 91 MB
% 21.39/4.35 % (572599)Instructions burned: 21 (million)
% 21.39/4.35 % (572596)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=2944348416:i=140167_2996 on theBenchmark for (2996ds/140167Mi)
% 21.39/4.35 % (572600)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2529577042:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2996 on theBenchmark for (2996ds/114Mi)
% 21.39/4.35 % (572601)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=967222229:s2a=on:i=180:gtg=position_2996 on theBenchmark for (2996ds/180Mi)
% 21.39/4.35 % (572598)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2358507693:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2996 on theBenchmark for (2996ds/137899Mi)
% 21.39/4.35 % (572600)Refutation not found, incomplete strategy
% 21.39/4.35 % (572600)------------------------------
% 21.39/4.35 % (572600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.39/4.35 % (572600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.39/4.35 % (572600)CaDiCaL version: 2.1.3
% 21.39/4.35 % (572600)Termination reason: Refutation not found, incomplete strategy
% 21.39/4.35 % (572600)Time elapsed: 0.028 s
% 21.39/4.35 % (572600)Peak memory usage: 91 MB
% 21.39/4.35 % (572600)Instructions burned: 33 (million)
% 21.39/4.35 % (572602)dis-21_1_sil=8000:lcm=predicate:random_seed=1138928869:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2996 on theBenchmark for (2996ds/117Mi)
% 21.39/4.35 % (572601)Instruction limit reached!
% 21.39/4.35 % (572601)------------------------------
% 21.39/4.35 % (572601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.39/4.35 % (572601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.39/4.35 % (572601)CaDiCaL version: 2.1.3
% 21.39/4.35 % (572601)Termination reason: Instruction limit
% 21.39/4.35 % (572601)Termination phase: Property scanning
% 21.39/4.35 % (572601)Time elapsed: 0.123 s
% 21.39/4.35 % (572601)Peak memory usage: 89 MB
% 21.39/4.35 % (572601)Instructions burned: 182 (million)
% 21.39/4.35 % (572602)Instruction limit reached!
% 21.39/4.35 % (572602)------------------------------
% 21.39/4.35 % (572602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.39/4.35 % (572602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.39/4.35 % (572602)CaDiCaL version: 2.1.3
% 21.39/4.35 % (572602)Termination reason: Instruction limit
% 21.39/4.35 % (572602)Termination phase: Property scanning
% 21.39/4.35 % (572602)Time elapsed: 0.082 s
% 21.39/4.35 % (572602)Peak memory usage: 89 MB
% 21.39/4.35 % (572602)Instructions burned: 118 (million)
% 21.39/4.35 % (572599)------------------------------
% 21.39/4.35 % (572599)------------------------------
% 21.39/4.35 % (572610)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=3777099661:i=143:sd=2:aac=none:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/143Mi)
% 21.39/4.35 % (572610)Refutation not found, incomplete strategy
% 21.39/4.35 % (572610)------------------------------
% 21.39/4.35 % (572610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.39/4.35 % (572610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.39/4.35 % (572610)CaDiCaL version: 2.1.3
% 21.39/4.35 % (572610)Termination reason: Refutation not found, incomplete strategy
% 21.39/4.35 % (572610)Time elapsed: 0.013 s
% 21.39/4.35 % (572610)Peak memory usage: 91 MB
% 21.39/4.35 % (572610)Instructions burned: 23 (million)
% 39.36/6.90 % (572600)------------------------------
% 39.36/6.90 % (572600)------------------------------
% 39.36/6.90 % (572611)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=328046938:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2991 on theBenchmark for (2991ds/189Mi)
% 39.36/6.90 % (572611)Refutation not found, incomplete strategy
% 39.36/6.90 % (572611)------------------------------
% 39.36/6.90 % (572611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.36/6.90 % (572611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.36/6.90 % (572611)CaDiCaL version: 2.1.3
% 39.36/6.90 % (572611)Termination reason: Refutation not found, incomplete strategy
% 39.36/6.90 % (572611)Time elapsed: 0.048 s
% 39.36/6.90 % (572611)Peak memory usage: 91 MB
% 39.36/6.90 % (572611)Instructions burned: 57 (million)
% 39.36/6.90 % (572612)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4054141136:st=4:i=219:sd=3:ss=axioms_2989 on theBenchmark for (2989ds/219Mi)
% 39.36/6.90 % (572612)Refutation not found, incomplete strategy
% 39.36/6.90 % (572612)------------------------------
% 39.36/6.90 % (572612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.36/6.90 % (572612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.36/6.90 % (572612)CaDiCaL version: 2.1.3
% 39.36/6.90 % (572612)Termination reason: Refutation not found, incomplete strategy
% 39.36/6.90 % (572612)Time elapsed: 0.020 s
% 39.36/6.90 % (572612)Peak memory usage: 91 MB
% 39.36/6.90 % (572612)Instructions burned: 33 (million)
% 39.36/6.90 % (572610)------------------------------
% 39.36/6.90 % (572610)------------------------------
% 39.36/6.90 % (572614)lrs+10_64_to=lpo:sil=8000:random_seed=2159295296:i=126:bd=preordered_2988 on theBenchmark for (2988ds/126Mi)
% 39.36/6.90 % (572617)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=952945599:avsq=on:i=194:fgj=on:bd=preordered_2987 on theBenchmark for (2987ds/194Mi)
% 39.36/6.90 % (572614)Instruction limit reached!
% 39.36/6.90 % (572614)------------------------------
% 39.36/6.90 % (572614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.36/6.90 % (572614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.36/6.90 % (572614)CaDiCaL version: 2.1.3
% 39.36/6.90 % (572614)Termination reason: Instruction limit
% 39.36/6.90 % (572614)Termination phase: Saturation
% 39.36/6.90 % (572614)Time elapsed: 0.116 s
% 39.36/6.90 % (572614)Peak memory usage: 94 MB
% 39.36/6.90 % (572614)Instructions burned: 127 (million)
% 39.36/6.90 % (572611)------------------------------
% 39.36/6.90 % (572611)------------------------------
% 39.36/6.90 % (572617)Instruction limit reached!
% 39.36/6.90 % (572617)------------------------------
% 39.36/6.90 % (572617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.36/6.90 % (572617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.36/6.90 % (572617)CaDiCaL version: 2.1.3
% 39.36/6.90 % (572617)Termination reason: Instruction limit
% 39.36/6.90 % (572617)Termination phase: Saturation
% 39.36/6.90 % (572617)Time elapsed: 0.092 s
% 39.36/6.90 % (572617)Peak memory usage: 95 MB
% 39.36/6.90 % (572617)Instructions burned: 194 (million)
% 39.36/6.90 % (572612)------------------------------
% 39.36/6.90 % (572612)------------------------------
% 39.36/6.90 % (572621)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1996735299:i=157:gtg=all_2984 on theBenchmark for (2984ds/157Mi)
% 39.36/6.90 % (572623)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=674460986:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2983 on theBenchmark for (2983ds/106Mi)
% 39.36/6.90 % (572623)Refutation not found, incomplete strategy
% 39.36/6.90 % (572623)------------------------------
% 39.36/6.90 % (572623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.36/6.90 % (572623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.36/6.90 % (572623)CaDiCaL version: 2.1.3
% 39.36/6.90 % (572623)Termination reason: Refutation not found, incomplete strategy
% 39.36/6.90 % (572623)Time elapsed: 0.021 s
% 39.36/6.90 % (572623)Peak memory usage: 91 MB
% 39.36/6.90 % (572623)Instructions burned: 42 (million)
% 39.36/6.90 % (572622)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2707747416:i=3394:sd=4:ss=included:sgt=64_2984 on theBenchmark for (2984ds/3394Mi)
% 39.36/6.90 % (572621)Instruction limit reached!
% 53.84/9.03 % (572621)------------------------------
% 53.84/9.03 % (572621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.84/9.03 % (572621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.84/9.03 % (572621)CaDiCaL version: 2.1.3
% 53.84/9.03 % (572621)Termination reason: Instruction limit
% 53.84/9.03 % (572621)Termination phase: Saturation
% 53.84/9.03 % (572621)Time elapsed: 0.108 s
% 53.84/9.03 % (572621)Peak memory usage: 91 MB
% 53.84/9.03 % (572621)Instructions burned: 157 (million)
% 53.84/9.03 % (572624)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=144887246:i=107_2983 on theBenchmark for (2983ds/107Mi)
% 53.84/9.03 % (572624)Instruction limit reached!
% 53.84/9.03 % (572624)------------------------------
% 53.84/9.03 % (572624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.84/9.03 % (572624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.84/9.03 % (572624)CaDiCaL version: 2.1.3
% 53.84/9.03 % (572624)Termination reason: Instruction limit
% 53.84/9.03 % (572624)Termination phase: Saturation
% 53.84/9.03 % (572624)Time elapsed: 0.095 s
% 53.84/9.03 % (572624)Peak memory usage: 94 MB
% 53.84/9.03 % (572624)Instructions burned: 107 (million)
% 53.84/9.03 % (572623)------------------------------
% 53.84/9.03 % (572623)------------------------------
% 53.84/9.03 % (572631)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=22232154:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2980 on theBenchmark for (2980ds/242Mi)
% 53.84/9.03 % (572633)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3094504270:cond=fast:i=5208:av=off_2979 on theBenchmark for (2979ds/5208Mi)
% 53.84/9.03 % (572631)Instruction limit reached!
% 53.84/9.03 % (572631)------------------------------
% 53.84/9.03 % (572631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.84/9.03 % (572631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.84/9.03 % (572631)CaDiCaL version: 2.1.3
% 53.84/9.03 % (572631)Termination reason: Instruction limit
% 53.84/9.03 % (572631)Termination phase: Property scanning
% 53.84/9.03 % (572631)Time elapsed: 0.164 s
% 53.84/9.03 % (572631)Peak memory usage: 88 MB
% 53.84/9.03 % (572631)Instructions burned: 243 (million)
% 53.84/9.03 % (572634)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2778384223:i=134:sd=2:doe=on:ss=axioms:sgt=14_2979 on theBenchmark for (2979ds/134Mi)
% 53.84/9.03 % (572634)Refutation not found, incomplete strategy
% 53.84/9.03 % (572634)------------------------------
% 53.84/9.03 % (572634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.84/9.03 % (572634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.84/9.03 % (572634)CaDiCaL version: 2.1.3
% 53.84/9.03 % (572634)Termination reason: Refutation not found, incomplete strategy
% 53.84/9.03 % (572634)Time elapsed: 0.023 s
% 53.84/9.03 % (572634)Peak memory usage: 91 MB
% 53.84/9.03 % (572634)Instructions burned: 23 (million)
% 53.84/9.03 % (572639)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=632835714:i=499:bd=all_2976 on theBenchmark for (2976ds/499Mi)
% 53.84/9.03 % (572634)------------------------------
% 53.84/9.03 % (572634)------------------------------
% 53.84/9.03 % (572639)Instruction limit reached!
% 53.84/9.03 % (572639)------------------------------
% 53.84/9.03 % (572639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.84/9.03 % (572639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.84/9.03 % (572639)CaDiCaL version: 2.1.3
% 53.84/9.03 % (572639)Termination reason: Instruction limit
% 53.84/9.03 % (572639)Termination phase: Saturation
% 53.84/9.03 % (572639)Time elapsed: 0.402 s
% 53.84/9.03 % (572639)Peak memory usage: 101 MB
% 53.84/9.03 % (572639)Instructions burned: 500 (million)
% 53.84/9.03 % (572645)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1190246946:i=191:fgj=on:bd=all_2971 on theBenchmark for (2971ds/191Mi)
% 53.84/9.03 % (572646)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2634761126:i=264:kws=precedence:fsr=off_2969 on theBenchmark for (2969ds/264Mi)
% 53.84/9.03 % (572645)Instruction limit reached!
% 53.84/9.03 % (572645)------------------------------
% 53.84/9.03 % (572645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.84/9.03 % (572645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.94/9.69 % (572645)CaDiCaL version: 2.1.3
% 58.94/9.69 % (572645)Termination reason: Instruction limit
% 58.94/9.69 % (572645)Termination phase: Saturation
% 58.94/9.69 % (572645)Time elapsed: 0.176 s
% 58.94/9.69 % (572645)Peak memory usage: 96 MB
% 58.94/9.69 % (572645)Instructions burned: 192 (million)
% 58.94/9.69 % (572646)Instruction limit reached!
% 58.94/9.69 % (572646)------------------------------
% 58.94/9.69 % (572646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.94/9.69 % (572646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.94/9.69 % (572646)CaDiCaL version: 2.1.3
% 58.94/9.69 % (572646)Termination reason: Instruction limit
% 58.94/9.69 % (572646)Termination phase: Saturation
% 58.94/9.69 % (572646)Time elapsed: 0.231 s
% 58.94/9.69 % (572646)Peak memory usage: 97 MB
% 58.94/9.69 % (572646)Instructions burned: 265 (million)
% 58.94/9.69 % (572650)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3709984276:cond=on:i=156:bs=on:gtg=exists_all:er=known_2966 on theBenchmark for (2966ds/156Mi)
% 58.94/9.69 % (572650)Instruction limit reached!
% 58.94/9.70 % (572650)------------------------------
% 58.94/9.70 % (572650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.94/9.70 % (572650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.94/9.70 % (572650)CaDiCaL version: 2.1.3
% 58.94/9.70 % (572650)Termination reason: Instruction limit
% 58.94/9.70 % (572650)Termination phase: Saturation
% 58.94/9.70 % (572650)Time elapsed: 0.071 s
% 58.94/9.70 % (572650)Peak memory usage: 91 MB
% 58.94/9.70 % (572650)Instructions burned: 157 (million)
% 58.94/9.70 % (572651)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=718348244:i=3256:kws=precedence:bd=preordered:av=off_2964 on theBenchmark for (2964ds/3256Mi)
% 58.94/9.70 % (572653)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=999863223:i=537:av=off:ss=included_2963 on theBenchmark for (2963ds/537Mi)
% 58.94/9.70 % (572653)Instruction limit reached!
% 58.94/9.70 % (572653)------------------------------
% 58.94/9.70 % (572653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.94/9.70 % (572653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.94/9.70 % (572653)CaDiCaL version: 2.1.3
% 58.94/9.70 % (572653)Termination reason: Instruction limit
% 58.94/9.70 % (572653)Termination phase: Saturation
% 58.94/9.70 % (572653)Time elapsed: 0.382 s
% 58.94/9.70 % (572653)Peak memory usage: 96 MB
% 58.94/9.70 % (572653)Instructions burned: 537 (million)
% 58.94/9.70 % (572658)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3720032112:i=180:bd=preordered:av=off_2956 on theBenchmark for (2956ds/180Mi)
% 58.94/9.70 % (572658)Instruction limit reached!
% 58.94/9.70 % (572658)------------------------------
% 58.94/9.70 % (572658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.94/9.70 % (572658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.94/9.70 % (572658)CaDiCaL version: 2.1.3
% 58.94/9.70 % (572658)Termination reason: Instruction limit
% 58.94/9.70 % (572658)Termination phase: Saturation
% 58.94/9.70 % (572658)Time elapsed: 0.161 s
% 58.94/9.70 % (572658)Peak memory usage: 94 MB
% 58.94/9.70 % (572658)Instructions burned: 180 (million)
% 58.94/9.70 % (572660)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=2978629781:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2951 on theBenchmark for (2951ds/10307Mi)
% 58.94/9.70 % (572633)Instruction limit reached!
% 58.94/9.70 % (572633)------------------------------
% 58.94/9.70 % (572633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.94/9.70 % (572633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.94/9.70 % (572633)CaDiCaL version: 2.1.3
% 58.94/9.70 % (572633)Termination reason: Instruction limit
% 58.94/9.70 % (572633)Termination phase: Saturation
% 58.94/9.70 % (572633)Time elapsed: 3.561 s
% 58.94/9.70 % (572633)Peak memory usage: 327 MB
% 58.94/9.70 % (572633)Instructions burned: 5208 (million)
% 58.94/9.70 % (572622)Instruction limit reached!
% 58.94/9.70 % (572622)------------------------------
% 58.94/9.70 % (572622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.94/9.70 % (572622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.94/9.70 % (572622)CaDiCaL version: 2.1.3
% 83.59/13.14 % (572622)Termination reason: Instruction limit
% 83.59/13.14 % (572622)Termination phase: Saturation
% 83.59/13.14 % (572622)Time elapsed: 3.982 s
% 83.59/13.14 % (572622)Peak memory usage: 380 MB
% 83.59/13.14 % (572622)Instructions burned: 3394 (million)
% 83.59/13.14 % (572664)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=2200947302:i=412:gtgl=4:gtg=exists_all_2941 on theBenchmark for (2941ds/412Mi)
% 83.59/13.14 % (572665)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=372262286:s2pl=no:i=8478:s2at=4:nm=6_2940 on theBenchmark for (2940ds/8478Mi)
% 83.59/13.14 % (572664)Instruction limit reached!
% 83.59/13.14 % (572664)------------------------------
% 83.59/13.14 % (572664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/13.14 % (572664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/13.14 % (572664)CaDiCaL version: 2.1.3
% 83.59/13.14 % (572664)Termination reason: Instruction limit
% 83.59/13.14 % (572664)Termination phase: Blocked clause elimination
% 83.59/13.14 % (572664)Time elapsed: 0.289 s
% 83.59/13.14 % (572664)Peak memory usage: 90 MB
% 83.59/13.14 % (572664)Instructions burned: 413 (million)
% 83.59/13.14 % (572668)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3310382617:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2936 on theBenchmark for (2936ds/303Mi)
% 83.59/13.14 % (572668)Instruction limit reached!
% 83.59/13.14 % (572668)------------------------------
% 83.59/13.14 % (572668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/13.14 % (572668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/13.14 % (572668)CaDiCaL version: 2.1.3
% 83.59/13.14 % (572668)Termination reason: Instruction limit
% 83.59/13.14 % (572668)Termination phase: Saturation
% 83.59/13.14 % (572668)Time elapsed: 0.233 s
% 83.59/13.14 % (572668)Peak memory usage: 96 MB
% 83.59/13.14 % (572668)Instructions burned: 303 (million)
% 83.59/13.14 % (572673)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=4120708985:st=4:i=720:sd=3:fsr=off:ss=axioms_2931 on theBenchmark for (2931ds/720Mi)
% 83.59/13.14 % (572673)Refutation not found, incomplete strategy
% 83.59/13.14 % (572673)------------------------------
% 83.59/13.14 % (572673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/13.14 % (572673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/13.14 % (572673)CaDiCaL version: 2.1.3
% 83.59/13.14 % (572673)Termination reason: Refutation not found, incomplete strategy
% 83.59/13.14 % (572673)Time elapsed: 0.029 s
% 83.59/13.14 % (572673)Peak memory usage: 91 MB
% 83.59/13.14 % (572673)Instructions burned: 33 (million)
% 83.59/13.14 % (572673)------------------------------
% 83.59/13.14 % (572673)------------------------------
% 83.59/13.14 % (572651)Instruction limit reached!
% 83.59/13.14 % (572651)------------------------------
% 83.59/13.14 % (572651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/13.14 % (572651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/13.14 % (572651)CaDiCaL version: 2.1.3
% 83.59/13.14 % (572651)Termination reason: Instruction limit
% 83.59/13.14 % (572651)Termination phase: Saturation
% 83.59/13.14 % (572651)Time elapsed: 3.814 s
% 83.59/13.14 % (572651)Peak memory usage: 398 MB
% 83.59/13.14 % (572651)Instructions burned: 3256 (million)
% 83.59/13.14 % (572678)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3423911924:i=598:bs=on:bd=preordered:av=off:ss=axioms_2923 on theBenchmark for (2923ds/598Mi)
% 83.59/13.14 % (572678)Refutation not found, incomplete strategy
% 83.59/13.14 % (572678)------------------------------
% 83.59/13.14 % (572678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/13.14 % (572678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/13.14 % (572678)CaDiCaL version: 2.1.3
% 83.59/13.14 % (572678)Termination reason: Refutation not found, incomplete strategy
% 83.59/13.14 % (572678)Time elapsed: 0.022 s
% 83.59/13.14 % (572678)Peak memory usage: 91 MB
% 83.59/13.14 % (572678)Instructions burned: 23 (million)
% 83.59/13.14 % (572679)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1876342426:i=2989:sd=3:ss=axioms:sgt=60_2922 on theBenchmark for (2922ds/2989Mi)
% 85.92/13.42 % (572678)------------------------------
% 85.92/13.42 % (572678)------------------------------
% 85.92/13.42 % (572684)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=1097411461:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2917 on theBenchmark for (2917ds/1997Mi)
% 85.92/13.42 [W928 17:57:13.373904934 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.92/13.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.92/13.42 [W928 17:57:13.373971641 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.92/13.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.92/13.42 [W928 17:57:13.374047448 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.92/13.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.92/13.42 [W928 17:57:13.374069198 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.92/13.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.92/13.42 [W928 17:57:13.374114998 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.92/13.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.92/13.42 [W928 17:57:13.374134595 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.92/13.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.92/13.42 [W928 17:57:13.374180299 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.92/13.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.92/13.42 [W928 17:57:13.374199539 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.92/13.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.92/13.42 [W928 17:57:13.374246646 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.92/13.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.92/13.42 [W928 17:57:13.374265736 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.92/13.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.92/13.42 [W928 17:57:13.374310567 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.92/13.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.92/13.42 [W928 17:57:13.374330653 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.92/13.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 87.15/13.65 % (572679)Refutation not found, incomplete strategy
% 87.15/13.65 % (572679)------------------------------
% 87.15/13.65 % (572679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.15/13.65 % (572679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.15/13.65 % (572679)CaDiCaL version: 2.1.3
% 87.15/13.65 % (572679)Termination reason: Refutation not found, incomplete strategy
% 87.15/13.65 % (572679)Time elapsed: 0.952 s
% 87.15/13.65 % (572679)Peak memory usage: 136 MB
% 87.15/13.65 % (572679)Instructions burned: 901 (million)
% 87.15/13.65 % (572679)------------------------------
% 87.15/13.65 % (572679)------------------------------
% 87.15/13.65 % (572692)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=215748426:i=2088:bd=preordered:av=off_2907 on theBenchmark for (2907ds/2088Mi)
% 87.15/13.65 % (572684)Instruction limit reached!
% 87.15/13.65 % (572684)------------------------------
% 87.15/13.65 % (572684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.15/13.65 % (572684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.15/13.65 % (572684)CaDiCaL version: 2.1.3
% 87.15/13.65 % (572684)Termination reason: Instruction limit
% 87.15/13.65 % (572684)Termination phase: Saturation
% 87.15/13.65 % (572684)Time elapsed: 1.930 s
% 87.15/13.65 % (572684)Peak memory usage: 165 MB
% 87.15/13.65 % (572684)Instructions burned: 1997 (million)
% 87.15/13.65 % (572697)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3428425879:i=1098:nicw=on_2895 on theBenchmark for (2895ds/1098Mi)
% 87.15/13.65 % (572692)Instruction limit reached!
% 87.15/13.65 % (572692)------------------------------
% 87.15/13.65 % (572692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.15/13.65 % (572692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.15/13.65 % (572692)CaDiCaL version: 2.1.3
% 87.15/13.65 % (572692)Termination reason: Instruction limit
% 87.15/13.65 % (572692)Termination phase: Saturation
% 87.15/13.65 % (572692)Time elapsed: 1.913 s
% 87.15/13.65 % (572692)Peak memory usage: 345 MB
% 87.15/13.65 % (572692)Instructions burned: 2092 (million)
% 87.15/13.65 % (572665)Instruction limit reached!
% 87.15/13.65 % (572665)------------------------------
% 87.15/13.65 % (572665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.15/13.65 % (572665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.15/13.65 % (572665)CaDiCaL version: 2.1.3
% 87.15/13.65 % (572665)Termination reason: Instruction limit
% 87.15/13.65 % (572665)Termination phase: Saturation
% 87.15/13.65 % (572665)Time elapsed: 5.353 s
% 87.15/13.65 % (572665)Peak memory usage: 472 MB
% 87.15/13.65 % (572665)Instructions burned: 8478 (million)
% 87.15/13.65 % (572697)Instruction limit reached!
% 87.15/13.65 % (572697)------------------------------
% 87.15/13.65 % (572697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.15/13.65 % (572697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.15/13.65 % (572697)CaDiCaL version: 2.1.3
% 87.15/13.65 % (572697)Termination reason: Instruction limit
% 87.15/13.65 % (572697)Termination phase: Saturation
% 87.15/13.65 % (572697)Time elapsed: 0.841 s
% 87.15/13.65 % (572697)Peak memory usage: 108 MB
% 87.15/13.65 % (572697)Instructions burned: 1099 (million)
% 87.15/13.65 % (572702)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=984339655:i=433:bd=preordered_2884 on theBenchmark for (2884ds/433Mi)
% 87.15/13.65 % (572703)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=740428415:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2883 on theBenchmark for (2883ds/2942Mi)
% 87.15/13.65 % (572704)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3130056212:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2883 on theBenchmark for (2883ds/6922Mi)
% 87.15/13.65 % (572702)Instruction limit reached!
% 87.15/13.65 % (572702)------------------------------
% 87.15/13.65 % (572702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.15/13.65 % (572702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.15/13.65 % (572702)CaDiCaL version: 2.1.3
% 87.15/13.65 % (572702)Termination reason: Instruction limit
% 87.15/13.65 % (572702)Termination phase: Saturation
% 95.09/14.76 % (572702)Time elapsed: 0.383 s
% 95.09/14.76 % (572702)Peak memory usage: 103 MB
% 95.09/14.76 % (572702)Instructions burned: 434 (million)
% 95.09/14.76 [W928 17:57:16.972226470 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.09/14.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.09/14.76 [W928 17:57:16.972259026 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.09/14.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.09/14.76 [W928 17:57:16.972291031 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.09/14.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.09/14.76 [W928 17:57:16.972302061 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.09/14.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.09/14.76 [W928 17:57:16.972326345 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.09/14.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.09/14.76 [W928 17:57:16.972336601 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.09/14.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.09/14.76 [W928 17:57:16.972359184 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.09/14.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.09/14.76 [W928 17:57:16.972369640 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.09/14.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.09/14.76 [W928 17:57:16.972392554 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.09/14.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.09/14.76 [W928 17:57:16.972402124 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.09/14.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.09/14.76 [W928 17:57:16.972422707 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.09/14.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.09/14.76 [W928 17:57:16.972432530 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.09/14.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.09/14.76 % (572709)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=563097636:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2878 on theBenchmark for (2878ds/596Mi)
% 106.96/16.86 % (572703)Refutation not found, incomplete strategy
% 106.96/16.86 % (572703)------------------------------
% 106.96/16.86 % (572703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.96/16.86 % (572703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.96/16.86 % (572703)CaDiCaL version: 2.1.3
% 106.96/16.86 % (572703)Termination reason: Refutation not found, incomplete strategy
% 106.96/16.86 % (572703)Time elapsed: 0.582 s
% 106.96/16.86 % (572703)Peak memory usage: 131 MB
% 106.96/16.86 % (572703)Instructions burned: 1073 (million)
% 106.96/16.86 [W928 17:57:17.323173219 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 106.96/16.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 106.96/16.86 [W928 17:57:17.323223886 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 106.96/16.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 106.96/16.86 [W928 17:57:17.323286453 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 106.96/16.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 106.96/16.86 [W928 17:57:17.323308107 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 106.96/16.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 106.96/16.86 [W928 17:57:17.323356740 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 106.96/16.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 106.96/16.86 [W928 17:57:17.323389417 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 106.96/16.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 106.96/16.86 [W928 17:57:17.323436804 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 106.96/16.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 106.96/16.86 [W928 17:57:17.323516502 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 106.96/16.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 106.96/16.86 [W928 17:57:17.323570685 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 106.96/16.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 106.96/16.86 [W928 17:57:17.323586155 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 106.96/16.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 106.96/16.86 [W928 17:57:17.323623219 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 106.96/16.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 106.96/16.86 [W928 17:57:17.323638119 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.14/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.14/17.26 % (572703)------------------------------
% 78.14/17.26 % (572703)------------------------------
% 78.14/17.26 % (572709)Instruction limit reached!
% 78.14/17.26 % (572709)------------------------------
% 78.14/17.26 % (572709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.14/17.26 % (572709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.14/17.26 % (572709)CaDiCaL version: 2.1.3
% 78.14/17.26 % (572709)Termination reason: Instruction limit
% 78.14/17.26 % (572709)Termination phase: Saturation
% 78.14/17.26 % (572709)Time elapsed: 0.416 s
% 78.14/17.26 % (572709)Peak memory usage: 94 MB
% 78.14/17.26 % (572709)Instructions burned: 596 (million)
% 78.14/17.26 % (572712)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=3381866241:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2873 on theBenchmark for (2873ds/4123Mi)
% 78.14/17.26 % (572704)Refutation not found, incomplete strategy
% 78.14/17.26 % (572704)------------------------------
% 78.14/17.26 % (572704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.14/17.26 % (572704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.14/17.26 % (572704)CaDiCaL version: 2.1.3
% 78.14/17.26 % (572704)Termination reason: Refutation not found, incomplete strategy
% 78.14/17.26 % (572704)Time elapsed: 1.050 s
% 78.14/17.26 % (572704)Peak memory usage: 137 MB
% 78.14/17.26 % (572704)Instructions burned: 913 (million)
% 78.14/17.26 % (572713)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2414538724:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2871 on theBenchmark for (2871ds/16411Mi)
% 78.14/17.26 % (572704)------------------------------
% 78.14/17.26 % (572704)------------------------------
% 78.14/17.26 % (572718)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2097234234:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2865 on theBenchmark for (2865ds/1670Mi)
% 78.14/17.26 [W928 17:57:18.435339330 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.14/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.14/17.26 [W928 17:57:18.435401187 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.14/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.14/17.26 [W928 17:57:18.435459881 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.14/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.14/17.26 [W928 17:57:18.435477058 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.14/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.14/17.26 [W928 17:57:18.435517335 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.14/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.14/17.26 [W928 17:57:18.435533288 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.14/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.14/17.26 [W928 17:57:18.435573355 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.14/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.14/17.26 [W928 17:57:18.435589499 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.14/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.14/17.26 [W928 17:57:18.435644106 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.14/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.14/17.26 [W928 17:57:18.435660043 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.14/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.14/17.26 [W928 17:57:18.435763367 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.14/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.14/17.26 [W928 17:57:18.435786983 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.14/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.14/17.26 % (572713)Refutation not found, incomplete strategy
% 78.14/17.26 % (572713)------------------------------
% 78.14/17.26 % (572713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.14/17.26 % (572713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.14/17.26 % (572713)CaDiCaL version: 2.1.3
% 78.14/17.26 % (572713)Termination reason: Refutation not found, incomplete strategy
% 78.14/17.26 % (572713)Time elapsed: 0.950 s
% 78.14/17.26 % (572713)Peak memory usage: 135 MB
% 78.14/17.26 % (572713)Instructions burned: 902 (million)
% 78.14/17.26 % (572713)------------------------------
% 78.14/17.26 % (572713)------------------------------
% 78.14/17.26 % (572720)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=3206911240:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2855 on theBenchmark for (2855ds/1722Mi)
% 78.14/17.26 % (572718)Instruction limit reached!
% 78.14/17.26 % (572718)------------------------------
% 78.14/17.26 % (572718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.14/17.26 % (572718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.14/17.26 % (572718)CaDiCaL version: 2.1.3
% 78.14/17.26 % (572718)Termination reason: Instruction limit
% 78.14/17.26 % (572718)Termination phase: Saturation
% 78.14/17.26 % (572718)Time elapsed: 1.887 s
% 78.14/17.26 % (572718)Peak memory usage: 270 MB
% 78.14/17.26 % (572718)Instructions burned: 1670 (million)
% 78.14/17.26 % (572597)First to succeed.
% 78.14/17.26 % (572597)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-572586"
% 78.14/17.26 % (572712)Instruction limit reached!
% 78.14/17.26 % (572712)------------------------------
% 78.14/17.26 % (572712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.14/17.26 % (572712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.14/17.26 % (572712)CaDiCaL version: 2.1.3
% 78.14/17.26 % (572712)Termination reason: Instruction limit
% 78.14/17.26 % (572712)Termination phase: Saturation
% 78.14/17.26 % (572712)Time elapsed: 2.857 s
% 78.14/17.26 % (572712)Peak memory usage: 422 MB
% 78.14/17.26 % (572712)Instructions burned: 4124 (million)
% 78.14/17.26 % (572660)Instruction limit reached!
% 78.14/17.26 % (572660)------------------------------
% 78.14/17.26 % (572660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.14/17.26 % (572660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.14/17.26 % (572660)CaDiCaL version: 2.1.3
% 78.14/17.26 % (572660)Termination reason: Instruction limit
% 78.14/17.26 % (572660)Termination phase: Saturation
% 78.14/17.26 % (572660)Time elapsed: 10.767 s
% 78.14/17.26 % (572660)Peak memory usage: 490 MB
% 78.14/17.26 % (572660)Instructions burned: 10307 (million)
% 78.14/17.26 % (572724)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=3340580991:cts=off:cond=on:i=9530:bs=on:fsd=on_2844 on theBenchmark for (2844ds/9530Mi)
% 78.14/17.26 % (572725)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2039740275:st=2:i=4495:sd=10:ss=included_2842 on theBenchmark for (2842ds/4495Mi)
% 78.14/17.26 % (572597)Refutation found. Thanks to Tanya!
% 78.14/17.26 % SZS status Unsatisfiable for theBenchmark
% 78.14/17.26 % SZS output start Proof for theBenchmark
% See solution above
% 0.28/17.51 % (572597)------------------------------
% 0.28/17.51 % (572597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.28/17.51 % (572597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/17.51 % (572597)CaDiCaL version: 2.1.3
% 0.28/17.51 % (572597)Termination reason: Refutation
% 0.28/17.51 % (572597)Time elapsed: 15.088 s
% 0.28/17.51 % (572597)Peak memory usage: 473 MB
% 0.28/17.51 % (572597)Instructions burned: 13848 (million)
% 0.28/17.51 % (572597)------------------------------
% 0.28/17.51 % (572597)------------------------------
% 0.28/17.51 % (572586)Success in time 16.25 s
% 0.28/17.51 % Vampire exiting
%------------------------------------------------------------------------------