%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO591-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:04 PM UTC 2026
% Result : Unsatisfiable 10.54s 3.61s
% Output : Refutation 20.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 61
% Number of leaves : 127
% Syntax : Number of formulae : 253 ( 129 unt; 0 def)
% Number of atoms : 459 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 454 ( 248 ~; 206 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 14 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 123 ( 122 usr; 4 prp; 0-23 aty)
% Number of functors : 2 ( 2 usr; 2 con; 0-0 aty)
% Number of variables : 2935 (2935 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk141_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk165_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_11) ).
fof(f14,axiom,
( ~ esk1_0
| esk3_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_14) ).
fof(f15,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( esk111_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk112_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk110_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_15) ).
fof(f16,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk141_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk162_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_16) ).
fof(f18,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk188_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk197_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_18) ).
fof(f22,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk247_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk150_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_22) ).
fof(f29,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( ~ esk168_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| esk185_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_29) ).
fof(f41,axiom,
! [X2,X3,X0,X1,X4] :
( esk27_5(X0,X1,X2,X3,X4)
| esk28_5(X0,X1,X2,X3,X4)
| ~ esk26_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_41) ).
fof(f44,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk229_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk152_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| p(X17)
| ~ p(X18)
| ~ p(X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_44) ).
fof(f58,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk355_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk43_5(X0,X1,X2,X3,X4)
| esk356_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_58) ).
fof(f69,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk288_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk108_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_69) ).
fof(f81,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( esk167_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk166_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk168_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_81) ).
fof(f85,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( ~ esk168_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| esk176_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_85) ).
fof(f90,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk302_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk308_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk58_8(X0,X1,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_90) ).
fof(f94,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( ~ esk170_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk169_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk185_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_94) ).
fof(f97,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( esk140_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk141_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk139_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_97) ).
fof(f109,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk280_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_109) ).
fof(f128,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ esk112_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk137_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_128) ).
fof(f131,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk188_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk196_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_131) ).
fof(f137,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk222_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk150_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_137) ).
fof(f150,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk209_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_150) ).
fof(f152,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk213_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| p(X17)
| ~ p(X19)
| ~ p(X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_152) ).
fof(f153,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk330_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk32_5(X0,X1,X2,X3,X4)
| esk336_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_153) ).
fof(f158,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk247_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk248_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_158) ).
fof(f167,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk331_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk58_8(X0,X1,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_167) ).
fof(f169,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk315_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ p(X8)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ p(X10)
| ~ p(X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_169) ).
fof(f175,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ esk54_8(X0,X1,X2,X3,X4,X5,X6,X7)
| esk81_8(X0,X1,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_175) ).
fof(f194,axiom,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ esk83_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| esk110_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_194) ).
fof(f205,axiom,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ esk83_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| esk108_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_205) ).
fof(f210,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk226_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk150_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_210) ).
fof(f215,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk208_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk209_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk171_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_215) ).
fof(f218,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk367_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk14_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_218) ).
fof(f221,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk315_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk82_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_221) ).
fof(f251,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk142_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk165_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk143_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_251) ).
fof(f257,axiom,
! [X0,X1] :
( ~ esk23_2(X0,X1)
| ~ p(X1)
| esk22_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_257) ).
fof(f272,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk28_5(X0,X1,X2,X3,X4)
| esk43_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_272) ).
fof(f277,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk187_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk188_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk186_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_277) ).
fof(f279,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ esk54_8(X0,X1,X2,X3,X4,X5,X6,X7)
| esk70_8(X0,X1,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_279) ).
fof(f284,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk227_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk167_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_284) ).
fof(f288,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk356_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk32_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_288) ).
fof(f295,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk189_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk197_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk190_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_295) ).
fof(f297,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk211_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk187_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk210_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_297) ).
fof(f303,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk287_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X13,X11,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ p(X11)
| ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ p(X13)
| ~ p(X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_303) ).
fof(f332,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ esk54_8(X0,X1,X2,X3,X4,X5,X6,X7)
| esk79_8(X0,X1,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_332) ).
fof(f335,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( esk53_8(X0,X1,X2,X3,X4,X5,X6,X7)
| esk54_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk52_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_335) ).
fof(f346,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk260_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk137_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_346) ).
fof(f384,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk355_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk14_2(X0,X1)
| esk361_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_384) ).
fof(f394,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ esk112_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk128_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_394) ).
fof(f411,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk275_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk116_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_411) ).
fof(f414,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk211_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ p(X20)
| ~ p(X21)
| ~ esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_414) ).
fof(f438,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk344_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk50_5(X0,X1,X2,X3,X4)
| esk42_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_438) ).
fof(f456,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk233_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ p(X14)
| ~ p(X16)
| p(X15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_456) ).
fof(f476,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk343_23(X1,X2,X3,X4,X5,X6,X0,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ p(X0)
| ~ esk42_5(X1,X2,X3,X4,X5)
| ~ p(X6)
| ~ p(X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_476) ).
fof(f484,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk336_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk42_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_484) ).
fof(f485,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk330_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk70_8(X0,X1,X2,X3,X4,X5,X6,X7)
| esk331_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_485) ).
fof(f498,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk229_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk167_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_498) ).
fof(f505,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk141_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk166_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_505) ).
fof(f513,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk211_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| p(X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_513) ).
fof(f517,axiom,
! [X2,X21,X3,X10,X0,X11,X18,X8,X6,X9,X7,X14,X4,X16,X19,X1,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk227_23(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X0,X1,X20,X21,X22)
| ~ p(X1)
| ~ esk150_17(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
| p(X0)
| p(X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_517) ).
fof(f533,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk247_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk251_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_533) ).
fof(f545,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk202_23(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X0,X21,X22)
| ~ p(X0)
| ~ p(X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_545) ).
fof(f552,axiom,
! [X0,X1] :
( ~ esk10_2(X1,X0)
| ~ esk7_1(X1)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_552) ).
fof(f559,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk361_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk22_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_559) ).
fof(f570,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk365_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk27_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_570) ).
fof(f595,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk316_23(X2,X3,X4,X5,X6,X0,X1,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ p(X1)
| ~ p(X0)
| ~ p(X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_595) ).
fof(f619,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk251_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk146_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk152_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_619) ).
fof(f626,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk213_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk170_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk183_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_626) ).
fof(f635,axiom,
( ~ esk1_0
| esk2_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_635) ).
fof(f641,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk246_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk116_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk252_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_641) ).
fof(f643,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( ~ esk168_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| esk178_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_643) ).
fof(f649,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk234_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk144_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_649) ).
fof(f660,axiom,
! [X0,X1] :
( ~ esk11_2(X0,X1)
| esk23_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_660) ).
fof(f667,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk257_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk140_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_667) ).
fof(f668,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk308_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_668) ).
fof(f672,axiom,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ esk83_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| esk99_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_672) ).
fof(f674,axiom,
! [X0] :
( ~ esk4_1(X0)
| ~ esk2_0
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_674) ).
fof(f675,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk257_23(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X0,X17,X18,X19,X20,X21,X22)
| ~ esk124_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ p(X15)
| ~ p(X0)
| p(X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_675) ).
fof(f710,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk274_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk280_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk87_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_710) ).
fof(f711,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk344_23(X3,X4,X0,X1,X2,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ p(X1)
| ~ p(X2)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_711) ).
fof(f726,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk225_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk169_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk176_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_726) ).
fof(f734,axiom,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( esk82_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| esk83_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk81_8(X0,X1,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_734) ).
fof(f744,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk208_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk189_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk192_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_744) ).
fof(f766,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ esk112_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk139_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_766) ).
fof(f769,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk141_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk155_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_769) ).
fof(f771,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk234_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk143_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_771) ).
fof(f774,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk187_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk186_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_774) ).
fof(f794,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk188_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| esk192_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_794) ).
fof(f809,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk225_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk144_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk226_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_809) ).
fof(f826,axiom,
! [X0,X1] :
( ~ esk11_2(X0,X1)
| esk24_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_826) ).
fof(f847,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk316_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk79_8(X0,X1,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_847) ).
fof(f850,axiom,
! [X0] :
( esk5_1(X0)
| esk4_1(X0)
| ~ esk3_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_850) ).
fof(f855,axiom,
! [X0] :
( ~ esk5_1(X0)
| esk8_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_855) ).
fof(f856,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk216_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk150_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_856) ).
fof(f873,axiom,
esk1_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_873) ).
fof(f904,axiom,
! [X0,X1] :
( esk10_2(X0,X1)
| ~ esk9_1(X0)
| esk11_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_904) ).
fof(f908,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk28_5(X0,X1,X2,X3,X4)
| esk50_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_908) ).
fof(f920,axiom,
! [X0,X1] :
( ~ esk11_2(X0,X1)
| esk26_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_920) ).
fof(f934,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk372_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk7_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_934) ).
fof(f938,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk210_23(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X0,X21,X22)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_938) ).
fof(f966,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk215_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk149_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk216_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_966) ).
fof(f967,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk287_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk111_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_967) ).
fof(f972,axiom,
! [X2,X3,X0,X1,X4] :
( ~ esk28_5(X0,X1,X2,X3,X4)
| esk52_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_972) ).
fof(f984,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk343_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk53_8(X0,X1,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_984) ).
fof(f999,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk274_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk128_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk275_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_999) ).
fof(f1009,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk221_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk222_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk146_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_1009) ).
fof(f1011,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk365_23(X2,X3,X1,X4,X0,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ p(X1)
| ~ p(X0)
| ~ p(X4)
| ~ esk22_2(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1011) ).
fof(f1017,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( ~ esk168_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| esk183_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1017) ).
fof(f1022,axiom,
! [X0] :
( ~ esk5_1(X0)
| esk9_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1022) ).
fof(f1023,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk211_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk187_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1023) ).
fof(f1026,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk202_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk190_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk196_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1026) ).
fof(f1029,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk366_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk6_1(X0)
| ~ esk7_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1029) ).
fof(f1035,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk215_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk181_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1035) ).
fof(f1041,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk372_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk6_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1041) ).
fof(f1047,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk303_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk87_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1047) ).
fof(f1048,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk372_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk8_1(X0)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1048) ).
fof(f1050,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk246_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk247_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk155_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_1050) ).
fof(f1060,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk288_23(X2,X3,X4,X5,X6,X7,X8,X9,X10,X1,X0,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ p(X1)
| ~ p(X0)
| ~ p(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1060) ).
fof(f1072,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( ~ esk168_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| esk181_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1072) ).
fof(f1085,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk302_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk99_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| esk303_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1085) ).
fof(f1086,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk234_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk233_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk162_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(f1094,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk221_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk171_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk178_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1094) ).
fof(f1112,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk252_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1112) ).
fof(f1134,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk248_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk142_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk149_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_1134) ).
fof(f1135,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk260_23(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X2,X0,X1,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ p(X1)
| ~ p(X2)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1135) ).
fof(f1136,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk366_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| esk367_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ esk24_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1136) ).
fof(f1137,axiom,
p(true),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_true) ).
fof(f1138,axiom,
~ p(false),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_false) ).
fof(f1140,plain,
esk2_0,
inference(forward_subsumption_resolution,[],[f635,f873]) ).
fof(f1141,plain,
esk3_0,
inference(forward_subsumption_resolution,[],[f14,f873]) ).
fof(f1170,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] : ~ esk202_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,true,true,X20),
inference(unit_resulting_resolution,[],[f545,f1137,f1137]) ).
fof(f1173,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : ~ esk316_23(X0,X1,X2,X3,X4,true,true,true,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f595,f1137,f1137,f1137]) ).
fof(f1180,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : ~ esk344_23(X0,X1,true,true,true,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f711,f1137,f1137,f1137]) ).
fof(f1194,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] : esk210_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,true,X20,X21),
inference(unit_resulting_resolution,[],[f938,f1137]) ).
fof(f1200,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : ~ esk288_23(X0,X1,X2,X3,X4,X5,X6,X7,true,true,true,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f1060,f1137,f1137,f1137]) ).
fof(f1209,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : ~ esk260_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,true,true,true,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f1135,f1137,f1137,f1137]) ).
fof(f1285,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : ~ esk213_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,true,true,X17,X18,X19),
inference(unit_resulting_resolution,[],[f152,f1137,f1137,f1138]) ).
fof(f1318,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : ~ esk233_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,true,false,true,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f456,f1137,f1137,f1138]) ).
fof(f1325,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] : esk211_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,false,X21),
inference(unit_resulting_resolution,[],[f513,f1138]) ).
fof(f1460,plain,
~ esk4_1(true),
inference(unit_resulting_resolution,[],[f674,f1137,f1140]) ).
fof(f1462,plain,
esk5_1(true),
inference(unit_resulting_resolution,[],[f850,f1141,f1460]) ).
fof(f1465,plain,
esk9_1(true),
inference(unit_resulting_resolution,[],[f1022,f1462]) ).
fof(f1466,plain,
esk8_1(true),
inference(unit_resulting_resolution,[],[f855,f1462]) ).
fof(f1468,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] : esk372_23(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21),
inference(unit_resulting_resolution,[],[f1048,f1137,f1466]) ).
fof(f1470,plain,
esk7_1(true),
inference(unit_resulting_resolution,[],[f934,f1468]) ).
fof(f1471,plain,
esk6_1(true),
inference(unit_resulting_resolution,[],[f1041,f1468]) ).
fof(f1472,plain,
~ esk10_2(true,true),
inference(unit_resulting_resolution,[],[f552,f1137,f1470]) ).
fof(f1475,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] : ~ esk366_23(true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21),
inference(unit_resulting_resolution,[],[f1029,f1471,f1470]) ).
fof(f1478,plain,
esk11_2(true,true),
inference(unit_resulting_resolution,[],[f904,f1465,f1472]) ).
fof(f1481,plain,
esk23_2(true,true),
inference(unit_resulting_resolution,[],[f660,f1478]) ).
fof(f1482,plain,
esk24_2(true,true),
inference(unit_resulting_resolution,[],[f826,f1478]) ).
fof(f1484,plain,
esk26_2(true,true),
inference(unit_resulting_resolution,[],[f920,f1478]) ).
fof(f1485,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] : esk367_23(true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20),
inference(unit_resulting_resolution,[],[f1136,f1475,f1482]) ).
fof(f1489,plain,
esk14_2(true,true),
inference(unit_resulting_resolution,[],[f218,f1485]) ).
fof(f1493,plain,
esk22_2(true,true),
inference(unit_resulting_resolution,[],[f257,f1137,f1481]) ).
fof(f1495,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] : ~ esk361_23(true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20),
inference(unit_resulting_resolution,[],[f559,f1493]) ).
fof(f1498,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X17,X15,X5,X12,X13] : ~ esk365_23(true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17),
inference(unit_resulting_resolution,[],[f1011,f1137,f1137,f1137,f1493]) ).
fof(f1509,plain,
~ esk27_5(true,true,true,true,true),
inference(unit_resulting_resolution,[],[f570,f1498]) ).
fof(f1521,plain,
esk28_5(true,true,true,true,true),
inference(unit_resulting_resolution,[],[f41,f1484,f1509]) ).
fof(f1524,plain,
esk43_5(true,true,true,true,true),
inference(unit_resulting_resolution,[],[f272,f1521]) ).
fof(f1529,plain,
esk50_5(true,true,true,true,true),
inference(unit_resulting_resolution,[],[f908,f1521]) ).
fof(f1530,plain,
esk52_5(true,true,true,true,true),
inference(unit_resulting_resolution,[],[f972,f1521]) ).
fof(f1541,plain,
esk42_5(true,true,true,true,true),
inference(unit_resulting_resolution,[],[f438,f1180,f1529]) ).
fof(f1545,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] : ~ esk343_23(true,true,true,true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14),
inference(unit_resulting_resolution,[],[f476,f1137,f1137,f1137,f1541]) ).
fof(f1546,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X17,X15,X5,X12,X13] : ~ esk336_23(true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17),
inference(unit_resulting_resolution,[],[f484,f1541]) ).
fof(f1553,plain,
~ esk53_8(true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f984,f1545]) ).
fof(f1556,plain,
esk54_8(true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f335,f1530,f1553]) ).
fof(f1561,plain,
esk81_8(true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f175,f1556]) ).
fof(f1562,plain,
esk70_8(true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f279,f1556]) ).
fof(f1564,plain,
esk79_8(true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f332,f1556]) ).
fof(f1573,plain,
esk68_8(true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f847,f1173,f1564]) ).
fof(f1574,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ~ esk315_23(true,true,true,true,true,true,true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f169,f1137,f1137,f1137,f1573]) ).
fof(f1579,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] : ~ esk308_23(true,true,true,true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14),
inference(unit_resulting_resolution,[],[f668,f1573]) ).
fof(f1587,plain,
~ esk82_11(true,true,true,true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f221,f1574]) ).
fof(f1588,plain,
esk83_11(true,true,true,true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f734,f1561,f1587]) ).
fof(f1593,plain,
esk110_11(true,true,true,true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f194,f1588]) ).
fof(f1594,plain,
esk108_11(true,true,true,true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f205,f1588]) ).
fof(f1598,plain,
esk99_11(true,true,true,true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f672,f1588]) ).
fof(f1605,plain,
esk97_11(true,true,true,true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f69,f1200,f1594]) ).
fof(f1607,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ~ esk280_23(true,true,true,true,true,true,true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f109,f1605]) ).
fof(f1608,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : ~ esk287_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8),
inference(unit_resulting_resolution,[],[f303,f1137,f1137,f1137,f1605]) ).
fof(f1619,plain,
~ esk111_14(true,true,true,true,true,true,true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f967,f1608]) ).
fof(f1622,plain,
esk112_14(true,true,true,true,true,true,true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f15,f1593,f1619]) ).
fof(f1624,plain,
esk137_14(true,true,true,true,true,true,true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f128,f1622]) ).
fof(f1628,plain,
esk128_14(true,true,true,true,true,true,true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f394,f1622]) ).
fof(f1632,plain,
esk139_14(true,true,true,true,true,true,true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f766,f1622]) ).
fof(f1637,plain,
esk124_14(true,true,true,true,true,true,true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f346,f1209,f1624]) ).
fof(f1639,plain,
! [X2,X3,X0,X1,X4,X5] : ~ esk257_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,X0,X1,X2,X3,X4,X5),
inference(unit_resulting_resolution,[],[f675,f1138,f1137,f1137,f1637]) ).
fof(f1646,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : ~ esk252_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8),
inference(unit_resulting_resolution,[],[f1112,f1637]) ).
fof(f1651,plain,
~ esk140_17(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f667,f1639]) ).
fof(f1653,plain,
esk141_17(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f97,f1632,f1651]) ).
fof(f1654,plain,
esk165_17(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f11,f1653]) ).
fof(f1655,plain,
esk162_17(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f16,f1653]) ).
fof(f1659,plain,
esk166_17(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f505,f1653]) ).
fof(f1666,plain,
esk155_17(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f769,f1653]) ).
fof(f1668,plain,
! [X2,X3,X0,X1,X4,X5] : esk234_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,X0,X1,X2,X3,X4,X5),
inference(unit_resulting_resolution,[],[f1086,f1318,f1655]) ).
fof(f1669,plain,
esk144_17(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f649,f1668]) ).
fof(f1670,plain,
esk143_17(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f771,f1668]) ).
fof(f1675,plain,
~ esk142_17(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f251,f1654,f1670]) ).
fof(f1711,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk187_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,true,false),
inference(unit_resulting_resolution,[],[f297,f1194,f1325]) ).
fof(f1712,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] : esk186_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19),
inference(unit_resulting_resolution,[],[f774,f1711]) ).
fof(f2222,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] : ~ esk355_23(true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20),
inference(unit_resulting_resolution,[],[f384,f1489,f1495]) ).
fof(f2223,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X17,X15,X5,X12,X13] : esk356_23(true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17),
inference(unit_resulting_resolution,[],[f58,f1524,f2222]) ).
fof(f2228,plain,
esk32_5(true,true,true,true,true),
inference(unit_resulting_resolution,[],[f288,f2223]) ).
fof(f2245,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X17,X15,X5,X12,X13] : ~ esk330_23(true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17),
inference(unit_resulting_resolution,[],[f153,f1546,f2228]) ).
fof(f2332,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] : esk331_23(true,true,true,true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14),
inference(unit_resulting_resolution,[],[f485,f1562,f2245]) ).
fof(f2353,plain,
esk58_8(true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f167,f2332]) ).
fof(f2359,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] : ~ esk302_23(true,true,true,true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14),
inference(unit_resulting_resolution,[],[f90,f1579,f2353]) ).
fof(f2373,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : esk303_23(true,true,true,true,true,true,true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f1085,f1598,f2359]) ).
fof(f2380,plain,
esk87_11(true,true,true,true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f1047,f2373]) ).
fof(f2392,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ~ esk274_23(true,true,true,true,true,true,true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),
inference(unit_resulting_resolution,[],[f710,f1607,f2380]) ).
fof(f2632,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : esk275_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8),
inference(unit_resulting_resolution,[],[f999,f1628,f2392]) ).
fof(f2654,plain,
esk116_14(true,true,true,true,true,true,true,true,true,true,true,true,true,true),
inference(unit_resulting_resolution,[],[f411,f2632]) ).
fof(f2670,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : ~ esk246_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,X0,X1,X2,X3,X4,X5,X6,X7,X8),
inference(unit_resulting_resolution,[],[f641,f1646,f2654]) ).
fof(f2673,plain,
! [X2,X3,X0,X1,X4,X5] : esk247_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,X0,X1,X2,X3,X4,X5),
inference(unit_resulting_resolution,[],[f1050,f1666,f2670]) ).
fof(f2674,plain,
! [X2,X3,X0,X1,X4,X5] : esk251_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,X0,X1,X2,X3,X4,X5),
inference(unit_resulting_resolution,[],[f533,f2673]) ).
fof(f2677,plain,
! [X2,X3,X0,X1,X4,X5] : esk248_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,X0,X1,X2,X3,X4,X5),
inference(unit_resulting_resolution,[],[f158,f2673]) ).
fof(f2679,plain,
esk150_17(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f22,f2673]) ).
fof(f2680,plain,
! [X2,X3,X0,X1,X4,X5] : ~ esk222_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,X0,X1,X2,X3,X4,X5),
inference(unit_resulting_resolution,[],[f137,f2679]) ).
fof(f2681,plain,
! [X2,X3,X0,X1,X4,X5] : ~ esk226_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,X0,X1,X2,X3,X4,X5),
inference(unit_resulting_resolution,[],[f210,f2679]) ).
fof(f2683,plain,
! [X2,X0,X1] : ~ esk227_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true,X0,X1,X2),
inference(unit_resulting_resolution,[],[f517,f1138,f1138,f1137,f2679]) ).
fof(f2689,plain,
! [X2,X3,X0,X1,X4,X5] : ~ esk216_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,X0,X1,X2,X3,X4,X5),
inference(unit_resulting_resolution,[],[f856,f2679]) ).
fof(f2690,plain,
esk149_17(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f1134,f1675,f2677]) ).
fof(f3224,plain,
~ esk167_20(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true),
inference(unit_resulting_resolution,[],[f284,f2683]) ).
fof(f3231,plain,
esk168_20(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true),
inference(unit_resulting_resolution,[],[f81,f1659,f3224]) ).
fof(f3239,plain,
esk178_20(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true),
inference(unit_resulting_resolution,[],[f643,f3231]) ).
fof(f3242,plain,
esk181_20(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true),
inference(unit_resulting_resolution,[],[f1072,f3231]) ).
fof(f3439,plain,
! [X2,X3,X0,X1,X4,X5] : ~ esk215_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,X0,X1,X2,X3,X4,X5),
inference(unit_resulting_resolution,[],[f966,f2690,f2689]) ).
fof(f3442,plain,
esk175_20(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true),
inference(unit_resulting_resolution,[],[f1035,f3242,f3439]) ).
fof(f3444,plain,
! [X2,X0,X1] : ~ esk209_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true,X0,X1,X2),
inference(unit_resulting_resolution,[],[f150,f3442]) ).
fof(f3447,plain,
! [X0] : ~ esk211_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true,true,true,X0),
inference(unit_resulting_resolution,[],[f414,f1137,f1137,f3442]) ).
fof(f3450,plain,
~ esk187_22(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f1023,f3447]) ).
fof(f3455,plain,
esk188_22(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f277,f1712,f3450]) ).
fof(f3456,plain,
esk197_22(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f18,f3455]) ).
fof(f3457,plain,
esk196_22(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f131,f3455]) ).
fof(f3461,plain,
esk192_22(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f794,f3455]) ).
fof(f3464,plain,
esk190_22(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f1026,f1170,f3457]) ).
fof(f3467,plain,
~ esk189_22(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true,true,true),
inference(unit_resulting_resolution,[],[f295,f3456,f3464]) ).
fof(f3470,plain,
! [X0] : esk208_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true,true,true,X0),
inference(unit_resulting_resolution,[],[f744,f3467,f3461]) ).
fof(f3473,plain,
~ esk171_20(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true),
inference(unit_resulting_resolution,[],[f215,f3470,f3444]) ).
fof(f3475,plain,
! [X2,X0,X1] : esk221_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,false,true,X0,X1,X2),
inference(unit_resulting_resolution,[],[f1094,f3239,f3473]) ).
fof(f3477,plain,
~ esk146_17(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f1009,f2680,f3475]) ).
fof(f3479,plain,
esk152_17(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true),
inference(unit_resulting_resolution,[],[f619,f2674,f3477]) ).
fof(f3480,plain,
! [X2,X0,X1] : ~ esk229_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,true,true,X0,X1,X2),
inference(unit_resulting_resolution,[],[f44,f1137,f1137,f1138,f3479]) ).
fof(f3494,plain,
~ esk167_20(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,true,true),
inference(unit_resulting_resolution,[],[f498,f3480]) ).
fof(f3499,plain,
esk168_20(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,true,true),
inference(unit_resulting_resolution,[],[f81,f1659,f3494]) ).
fof(f3500,plain,
esk185_20(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,true,true),
inference(unit_resulting_resolution,[],[f29,f3499]) ).
fof(f3502,plain,
esk176_20(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,true,true),
inference(unit_resulting_resolution,[],[f85,f3499]) ).
fof(f3509,plain,
esk183_20(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,true,true),
inference(unit_resulting_resolution,[],[f1017,f3499]) ).
fof(f3516,plain,
esk170_20(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,true,true),
inference(unit_resulting_resolution,[],[f626,f1285,f3509]) ).
fof(f3519,plain,
~ esk169_20(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,true,true),
inference(unit_resulting_resolution,[],[f94,f3516,f3500]) ).
fof(f3522,plain,
! [X2,X0,X1] : esk225_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,true,true,X0,X1,X2),
inference(unit_resulting_resolution,[],[f726,f3519,f3502]) ).
fof(f3524,plain,
! [X2,X0,X1] : esk226_23(true,true,true,true,true,true,true,true,true,true,true,true,true,true,true,false,true,false,true,true,X0,X1,X2),
inference(unit_resulting_resolution,[],[f809,f1669,f3522]) ).
fof(f3525,plain,
$false,
inference(forward_subsumption_resolution,[],[f3524,f2681]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO591-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.11/0.27 % Computer : n001.cluster.edu
% 0.11/0.27 % Model : x86_64 x86_64
% 0.11/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.27 % Memory : 8046.5625MB
% 0.11/0.27 % OS : Linux 6.8.0-71-generic
% 0.11/0.27 % CPULimit : 300
% 0.11/0.27 % WCLimit : 300
% 0.11/0.27 % DateTime : Mon Sep 28 17:57:33 UTC 2026
% 0.11/0.27 % CPUTime :
% 0.11/0.27 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.26/0.33 Running first-order theorem proving
% 0.26/0.33 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
% 10.54/3.61 % (573175)Input is clausal, will run a generic CNF schedule.
% 10.54/3.61 % (573183)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2781254917:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.54/3.61 % (573188)dis-21_1_sil=8000:lcm=predicate:random_seed=3373030318:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.54/3.61 % (573186)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3239189753:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.54/3.61 % (573182)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=4019896735:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.54/3.61 % (573186)Refutation not found, incomplete strategy
% 10.54/3.61 % (573186)------------------------------
% 10.54/3.61 % (573186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/3.61 % (573186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/3.61 % (573186)CaDiCaL version: 2.1.3
% 10.54/3.61 % (573186)Termination reason: Refutation not found, incomplete strategy
% 10.54/3.61 % (573186)Time elapsed: 0.005 s
% 10.54/3.61 % (573186)Peak memory usage: 87 MB
% 10.54/3.61 % (573186)Instructions burned: 4 (million)
% 10.54/3.61 % (573184)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=506460201:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.54/3.61 % (573187)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1830500376:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.54/3.61 % (573185)lrs+10_1_sil=8000:sp=occurrence:random_seed=3668220738:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.54/3.61 % (573185)Refutation not found, incomplete strategy
% 10.54/3.61 % (573185)------------------------------
% 10.54/3.61 % (573185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/3.61 % (573185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/3.61 % (573185)CaDiCaL version: 2.1.3
% 10.54/3.61 % (573185)Termination reason: Refutation not found, incomplete strategy
% 10.54/3.61 % (573185)Time elapsed: 0.004 s
% 10.54/3.61 % (573185)Peak memory usage: 87 MB
% 10.54/3.61 % (573185)Instructions burned: 3 (million)
% 10.54/3.61 % (573188)Instruction limit reached!
% 10.54/3.61 % (573188)------------------------------
% 10.54/3.61 % (573188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/3.61 % (573188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/3.61 % (573188)CaDiCaL version: 2.1.3
% 10.54/3.61 % (573188)Termination reason: Instruction limit
% 10.54/3.61 % (573188)Termination phase: Saturation
% 10.54/3.61 % (573188)Time elapsed: 0.097 s
% 10.54/3.61 % (573188)Peak memory usage: 90 MB
% 10.54/3.61 % (573188)Instructions burned: 117 (million)
% 10.54/3.61 % (573187)Instruction limit reached!
% 10.54/3.61 % (573187)------------------------------
% 10.54/3.61 % (573187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/3.61 % (573187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/3.61 % (573187)CaDiCaL version: 2.1.3
% 10.54/3.61 % (573187)Termination reason: Instruction limit
% 10.54/3.61 % (573187)Termination phase: Saturation
% 10.54/3.61 % (573187)Time elapsed: 0.140 s
% 10.54/3.61 % (573187)Peak memory usage: 91 MB
% 10.54/3.61 % (573187)Instructions burned: 181 (million)
% 10.54/3.61 % (573197)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=1581442080:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi)
% 10.54/3.61 % (573198)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1831364988:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2994 on theBenchmark for (2994ds/189Mi)
% 10.54/3.61 % (573197)Refutation not found, incomplete strategy
% 10.54/3.61 % (573197)------------------------------
% 10.54/3.61 % (573197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/3.61 % (573197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/3.61 % (573197)CaDiCaL version: 2.1.3
% 10.54/3.61 % (573197)Termination reason: Refutation not found, incomplete strategy
% 10.54/3.61 % (573197)Time elapsed: 0.004 s
% 10.54/3.61 % (573197)Peak memory usage: 87 MB
% 10.54/3.61 % (573197)Instructions burned: 3 (million)
% 10.54/3.61 % (573198)Refutation not found, incomplete strategy
% 10.54/3.61 % (573198)------------------------------
% 10.54/3.61 % (573198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/3.61 % (573198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/3.61 % (573198)CaDiCaL version: 2.1.3
% 10.54/3.61 % (573198)Termination reason: Refutation not found, incomplete strategy
% 10.54/3.61 % (573198)Time elapsed: 0.008 s
% 10.54/3.61 % (573198)Peak memory usage: 87 MB
% 10.54/3.61 % (573198)Instructions burned: 7 (million)
% 10.54/3.61 % (573186)------------------------------
% 10.54/3.61 % (573186)------------------------------
% 10.54/3.61 % (573185)------------------------------
% 10.54/3.61 % (573185)------------------------------
% 10.54/3.61 % (573202)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=373831108:st=4:i=219:sd=3:ss=axioms_2992 on theBenchmark for (2992ds/219Mi)
% 10.54/3.61 % (573202)Refutation not found, incomplete strategy
% 10.54/3.61 % (573202)------------------------------
% 10.54/3.61 % (573202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/3.61 % (573202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/3.61 % (573202)CaDiCaL version: 2.1.3
% 10.54/3.61 % (573202)Termination reason: Refutation not found, incomplete strategy
% 10.54/3.61 % (573202)Time elapsed: 0.003 s
% 10.54/3.61 % (573202)Peak memory usage: 87 MB
% 10.54/3.61 % (573202)Instructions burned: 4 (million)
% 10.54/3.61 % (573203)lrs+10_64_to=lpo:sil=8000:random_seed=910843050:i=126:bd=preordered_2992 on theBenchmark for (2992ds/126Mi)
% 10.54/3.61 % (573197)------------------------------
% 10.54/3.61 % (573197)------------------------------
% 10.54/3.61 % (573198)------------------------------
% 10.54/3.61 % (573198)------------------------------
% 10.54/3.61 % (573203)Instruction limit reached!
% 10.54/3.61 % (573203)------------------------------
% 10.54/3.61 % (573203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/3.61 % (573203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/3.61 % (573203)CaDiCaL version: 2.1.3
% 10.54/3.61 % (573203)Termination reason: Instruction limit
% 10.54/3.61 % (573203)Termination phase: Saturation
% 10.54/3.61 % (573203)Time elapsed: 0.117 s
% 10.54/3.61 % (573203)Peak memory usage: 90 MB
% 10.54/3.61 % (573203)Instructions burned: 126 (million)
% 10.54/3.61 % (573202)------------------------------
% 10.54/3.61 % (573202)------------------------------
% 10.54/3.61 % (573207)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1932558247:avsq=on:i=194:fgj=on:bd=preordered_2988 on theBenchmark for (2988ds/194Mi)
% 10.54/3.61 % (573210)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=4044409916:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2987 on theBenchmark for (2987ds/106Mi)
% 10.54/3.61 % (573210)Refutation not found, incomplete strategy
% 10.54/3.61 % (573210)------------------------------
% 10.54/3.61 % (573210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/3.61 % (573210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/3.61 % (573210)CaDiCaL version: 2.1.3
% 10.54/3.61 % (573210)Termination reason: Refutation not found, incomplete strategy
% 10.54/3.61 % (573210)Time elapsed: 0.004 s
% 10.54/3.61 % (573210)Peak memory usage: 87 MB
% 10.54/3.61 % (573210)Instructions burned: 5 (million)
% 10.54/3.61 % (573209)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1275447916:i=3394:sd=4:ss=included:sgt=64_2988 on theBenchmark for (2988ds/3394Mi)
% 10.54/3.61 % (573208)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1661313549:i=157:gtg=all_2988 on theBenchmark for (2988ds/157Mi)
% 10.54/3.61 % (573207)Instruction limit reached!
% 10.54/3.61 % (573207)------------------------------
% 10.54/3.61 % (573207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/3.61 % (573207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/3.61 % (573207)CaDiCaL version: 2.1.3
% 10.54/3.61 % (573207)Termination reason: Instruction limit
% 10.54/3.61 % (573207)Termination phase: Saturation
% 10.54/3.61 % (573207)Time elapsed: 0.169 s
% 10.54/3.61 % (573207)Peak memory usage: 92 MB
% 10.54/3.61 % (573207)Instructions burned: 195 (million)
% 10.54/3.61 % (573208)Instruction limit reached!
% 10.54/3.61 % (573208)------------------------------
% 10.54/3.61 % (573208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/3.61 % (573208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/3.61 % (573208)CaDiCaL version: 2.1.3
% 10.54/3.61 % (573208)Termination reason: Instruction limit
% 10.54/3.61 % (573208)Termination phase: Saturation
% 10.54/3.61 % (573208)Time elapsed: 0.144 s
% 10.54/3.61 % (573208)Peak memory usage: 91 MB
% 10.54/3.61 % (573208)Instructions burned: 157 (million)
% 10.54/3.61 % (573210)------------------------------
% 10.54/3.61 % (573210)------------------------------
% 10.54/3.61 % (573217)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2764882466:i=107_2984 on theBenchmark for (2984ds/107Mi)
% 10.54/3.61 % (573217)Refutation not found, incomplete strategy
% 10.54/3.61 % (573217)------------------------------
% 10.54/3.61 % (573217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/3.61 % (573217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/3.61 % (573217)CaDiCaL version: 2.1.3
% 10.54/3.61 % (573217)Termination reason: Refutation not found, incomplete strategy
% 10.54/3.61 % (573217)Time elapsed: 0.057 s
% 10.54/3.61 % (573217)Peak memory usage: 90 MB
% 10.54/3.61 % (573217)Instructions burned: 64 (million)
% 10.54/3.61 % (573219)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=653011152:cond=fast:i=5208:av=off_2983 on theBenchmark for (2983ds/5208Mi)
% 10.54/3.61 % (573218)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4228924067:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2983 on theBenchmark for (2983ds/242Mi)
% 10.54/3.61 % (573218)Instruction limit reached!
% 10.54/3.61 % (573218)------------------------------
% 10.54/3.61 % (573218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/3.61 % (573218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/3.61 % (573218)CaDiCaL version: 2.1.3
% 10.54/3.61 % (573218)Termination reason: Instruction limit
% 10.54/3.61 % (573218)Termination phase: Saturation
% 10.54/3.61 % (573218)Time elapsed: 0.215 s
% 10.54/3.61 % (573218)Peak memory usage: 91 MB
% 10.54/3.61 % (573218)Instructions burned: 242 (million)
% 10.54/3.61 % (573217)------------------------------
% 10.54/3.61 % (573217)------------------------------
% 10.54/3.61 % (573183)First to succeed.
% 10.54/3.61 % (573183)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-573175"
% 10.54/3.61 % (573223)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1596843414:i=134:sd=2:doe=on:ss=axioms:sgt=14_2978 on theBenchmark for (2978ds/134Mi)
% 10.54/3.61 % (573223)Refutation not found, incomplete strategy
% 10.54/3.61 % (573223)------------------------------
% 10.54/3.61 % (573223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.54/3.61 % (573223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.54/3.61 % (573223)CaDiCaL version: 2.1.3
% 10.54/3.61 % (573223)Termination reason: Refutation not found, incomplete strategy
% 10.54/3.61 % (573223)Time elapsed: 0.005 s
% 10.54/3.61 % (573223)Peak memory usage: 87 MB
% 10.54/3.61 % (573223)Instructions burned: 3 (million)
% 10.54/3.61 % (573225)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1471404543:i=499:bd=all_2976 on theBenchmark for (2976ds/499Mi)
% 10.54/3.61 % (573183)Refutation found. Thanks to Tanya!
% 10.54/3.61 % SZS status Unsatisfiable for theBenchmark
% 10.54/3.61 % SZS output start Proof for theBenchmark
% See solution above
% 20.15/3.83 % (573183)------------------------------
% 20.15/3.83 % (573183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.15/3.83 % (573183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.15/3.83 % (573183)CaDiCaL version: 2.1.3
% 20.15/3.83 % (573183)Termination reason: Refutation
% 20.15/3.83 % (573183)Time elapsed: 2.046 s
% 20.15/3.83 % (573183)Peak memory usage: 152 MB
% 20.15/3.83 % (573183)Instructions burned: 2381 (million)
% 20.15/3.83 % (573183)------------------------------
% 20.15/3.83 % (573183)------------------------------
% 20.15/3.83 % (573175)Success in time 2.827 s
% 20.15/3.83 % Vampire exiting
%------------------------------------------------------------------------------