%------------------------------------------------------------------------------
% File : Vampire-SAT---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 SAT
% Computer : n018.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:31:45 PM UTC 2026
% Result : Unsatisfiable 16.09s 2.68s
% Output : Refutation 16.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 145
% Syntax : Number of formulae : 375 ( 24 unt; 14 def)
% Number of atoms : 1564 ( 0 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 2465 (1276 ~;1175 |; 0 &)
% ( 14 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 18 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 136 ( 135 usr; 18 prp; 0-23 aty)
% Number of functors : 2 ( 2 usr; 2 con; 0-0 aty)
% Number of variables : 4920 ( 0 sgn4920 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( esk165_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) ),
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] :
( esk112_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk111_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] :
( esk162_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) ),
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] :
( esk197_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) ),
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] :
( esk150_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ 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) ),
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] :
( esk185_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ 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_29) ).
fof(f41,axiom,
! [X2,X3,X0,X1,X4] :
( esk28_5(X0,X1,X2,X3,X4)
| esk27_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] :
( p(X17)
| ~ esk152_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ 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)
| ~ 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] :
( 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)
| 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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_58) ).
fof(f61,axiom,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( esk81_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk83_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_61) ).
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] :
( esk168_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| 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) ),
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] :
( esk176_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ 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_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] :
( 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)
| ~ 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) ),
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] :
( ~ esk185_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)
| ~ esk170_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] :
( esk141_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk140_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] :
( esk137_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) ),
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] :
( esk196_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) ),
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] :
( p(X17)
| ~ 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(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] :
( 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)
| ~ esk32_5(X0,X1,X2,X3,X4)
| ~ 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) ),
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] :
( 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)
| ~ 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) ),
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] :
( esk58_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_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(f170,axiom,
! [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)
| ~ 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_170) ).
fof(f172,axiom,
! [X0,X1] :
( esk10_2(X0,X1)
| esk7_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_172) ).
fof(f175,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( esk81_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk54_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] :
( esk110_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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_194) ).
fof(f205,axiom,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( esk108_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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_205) ).
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] :
( 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)
| ~ 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) ),
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] :
( esk14_2(X0,X1)
| ~ 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) ),
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] :
( ~ esk165_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk142_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] :
( esk22_2(X0,X1)
| ~ p(X1)
| ~ esk23_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_257) ).
fof(f272,axiom,
! [X2,X3,X0,X1,X4] :
( esk43_5(X0,X1,X2,X3,X4)
| ~ esk28_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] :
( esk188_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| 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_277) ).
fof(f279,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( esk70_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk54_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] :
( esk32_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_288) ).
fof(f289,axiom,
! [X2,X3,X0,X1,X4] :
( esk26_2(X0,X1)
| ~ esk28_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_289) ).
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] :
( ~ 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)
| ~ esk189_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(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] :
( esk79_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk54_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] :
( esk54_8(X0,X1,X2,X3,X4,X5,X6,X7)
| esk53_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] :
( 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)
| ~ esk14_2(X0,X1)
| ~ 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) ),
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] :
( esk128_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) ),
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] :
( esk116_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_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,X16,X14,X4,X7,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( p(X15)
| ~ p(X14)
| ~ p(X16)
| ~ 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) ),
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] :
( 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)
| 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) ),
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] :
( esk166_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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_505) ).
fof(f517,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X19,X6,X7,X9,X4,X14,X16,X18,X17,X15,X5,X12,X22,X13,X20] :
( p(X19)
| ~ p(X1)
| ~ esk150_17(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18)
| ~ 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(X0) ),
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] :
( 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)
| ~ 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) ),
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] :
( 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)
| ~ 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_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] :
( 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)
| ~ 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) ),
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] :
( esk178_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ 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_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] :
( esk144_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ 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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_649) ).
fof(f660,axiom,
! [X0,X1] :
( esk23_2(X0,X1)
| ~ esk11_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] :
( esk99_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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_672) ).
fof(f674,axiom,
! [X0] :
( ~ p(X0)
| ~ esk2_0
| ~ esk4_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_674) ).
fof(f675,axiom,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X16,X7,X4,X14,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( p(X16)
| ~ esk124_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ p(X15)
| ~ 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)
| ~ p(X0) ),
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] :
( 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)
| ~ 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) ),
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(f712,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( esk52_5(X0,X1,X2,X3,X4)
| ~ esk54_8(X0,X1,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_712) ).
fof(f722,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( esk139_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk141_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_722) ).
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] :
( esk139_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) ),
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] :
( esk155_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) ),
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] :
( esk143_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ 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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_771) ).
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] :
( esk192_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) ),
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] :
( 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)
| ~ 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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_809) ).
fof(f826,axiom,
! [X0,X1] :
( esk24_2(X0,X1)
| ~ esk11_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] :
( esk8_1(X0)
| ~ esk5_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] :
( esk11_2(X0,X1)
| esk10_2(X0,X1)
| ~ esk9_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_904) ).
fof(f908,axiom,
! [X2,X3,X0,X1,X4] :
( esk50_5(X0,X1,X2,X3,X4)
| ~ esk28_5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_908) ).
fof(f920,axiom,
! [X0,X1] :
( esk26_2(X0,X1)
| ~ esk11_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] :
( esk7_1(X0)
| ~ 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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_934) ).
fof(f948,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)
| ~ 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_948) ).
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] :
( 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)
| ~ 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) ),
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] :
( esk52_5(X0,X1,X2,X3,X4)
| ~ esk28_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(f1004,axiom,
! [X0,X1] :
( esk9_1(X0)
| ~ esk11_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1004) ).
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] :
( 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)
| ~ 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)
| ~ 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] :
( esk183_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ 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_1017) ).
fof(f1022,axiom,
! [X0] :
( esk9_1(X0)
| ~ esk5_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(f1025,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( esk110_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk112_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1025) ).
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] :
( esk6_1(X0)
| ~ 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) ),
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] :
( esk87_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_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] :
( esk181_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ 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_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] :
( 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)
| 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) ),
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] :
( 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)
| 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)
| ~ 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] :
( esk149_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk142_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ 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_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(f1141,definition,
( spl0_1
<=> esk3_0 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f1149,definition,
( spl0_3
<=> ! [X0] :
( esk5_1(X0)
| esk4_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f1150,plain,
( ! [X0] :
( esk4_1(X0)
| esk5_1(X0) )
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f1149]) ).
fof(f1151,plain,
( ~ spl0_1
| spl0_3 ),
inference(avatar_split_clause,[],[f850,f1149,f1141]) ).
fof(f1153,definition,
( spl0_4
<=> esk2_0 ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f1157,definition,
( spl0_5
<=> ! [X0] :
( ~ p(X0)
| ~ esk4_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f1158,plain,
( ! [X0] :
( ~ esk4_1(X0)
| ~ p(X0) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f1157]) ).
fof(f1159,plain,
( ~ spl0_4
| spl0_5 ),
inference(avatar_split_clause,[],[f674,f1157,f1153]) ).
fof(f1160,plain,
esk2_0,
inference(forward_subsumption_resolution,[],[f635,f873]) ).
fof(f1169,plain,
esk3_0,
inference(forward_subsumption_resolution,[],[f14,f873]) ).
fof(f1170,plain,
spl0_4,
inference(avatar_split_clause,[],[f1160,f1153]) ).
fof(f1171,plain,
spl0_1,
inference(avatar_split_clause,[],[f1169,f1141]) ).
fof(f1172,plain,
( ! [X0] :
( esk5_1(X0)
| ~ p(X0) )
| ~ spl0_3
| ~ spl0_5 ),
inference(resolution,[],[f1158,f1150]) ).
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] :
( ~ esk213_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,X17,X18,X19,X20,X21)
| ~ p(X18)
| ~ p(X17) ),
inference(resolution,[],[f152,f1138]) ).
fof(f1213,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk233_23(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X0,false,X1,X16,X17,X18,X19,X20,X21)
| ~ p(X1)
| ~ p(X0) ),
inference(resolution,[],[f456,f1138]) ).
fof(f1291,plain,
! [X2,X3,X0,X1,X4] :
( ~ esk27_5(X3,X4,X0,X2,X1)
| ~ p(X1)
| ~ p(X2)
| ~ esk22_2(X3,X4)
| ~ p(X0) ),
inference(resolution,[],[f1011,f570]) ).
fof(f1317,plain,
! [X2,X3,X0,X1,X4] :
( esk42_5(X0,X1,X2,X3,X4)
| ~ esk50_5(X0,X1,X2,X3,X4)
| ~ p(X3)
| ~ p(X4)
| ~ p(X2) ),
inference(resolution,[],[f438,f711]) ).
fof(f1318,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ esk53_8(X1,X2,X3,X4,X5,X6,X0,X7)
| ~ esk42_5(X1,X2,X3,X4,X5)
| ~ p(X6)
| ~ p(X7)
| ~ p(X0) ),
inference(resolution,[],[f476,f984]) ).
fof(f1352,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ esk82_11(X1,X2,X3,X4,X5,X6,X7,X8,X0,X10,X9)
| ~ esk68_8(X1,X2,X3,X4,X5,X6,X7,X8)
| ~ p(X9)
| ~ p(X10)
| ~ p(X0) ),
inference(resolution,[],[f169,f221]) ).
fof(f1357,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( esk83_11(X0,X1,X2,X3,X4,X5,X6,X7,X10,X9,X8)
| ~ p(X8)
| ~ p(X9)
| ~ p(X10)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk81_8(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(resolution,[],[f1352,f734]) ).
fof(f1395,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ esk111_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X13,X12,X0)
| ~ esk97_11(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11)
| ~ p(X12)
| ~ p(X13)
| ~ p(X0) ),
inference(resolution,[],[f303,f967]) ).
fof(f1412,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk79_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ p(X6)
| ~ p(X5)
| ~ p(X7) ),
inference(resolution,[],[f847,f595]) ).
fof(f1431,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk257_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15,X16,X17,X18,X19,X20,X21)
| ~ p(X14)
| ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ p(X15) ),
inference(resolution,[],[f675,f1138]) ).
fof(f1432,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ esk140_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X0,false,X15)
| ~ esk124_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ p(X15)
| ~ p(X0) ),
inference(resolution,[],[f1431,f667]) ).
fof(f1459,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk229_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,X17,X18,X19,X20,X21)
| ~ esk152_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ p(X17)
| ~ p(X18) ),
inference(resolution,[],[f44,f1138]) ).
fof(f1460,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X17,X15,X5,X12,X13] :
( ~ esk167_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,X17,X18)
| ~ p(X17)
| ~ p(X18)
| ~ esk152_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
inference(resolution,[],[f1459,f498]) ).
fof(f1465,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( 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)
| ~ p(X9)
| ~ p(X10)
| ~ p(X8) ),
inference(resolution,[],[f69,f1060]) ).
fof(f1484,plain,
! [X2,X21,X3,X10,X0,X11,X18,X1,X6,X8,X7,X9,X4,X14,X16,X19,X17,X15,X5,X12,X13,X20] :
( p(X18)
| ~ esk150_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
| ~ esk227_23(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,false,X18,X0,X19,X20,X21)
| ~ p(X0) ),
inference(resolution,[],[f517,f1138]) ).
fof(f1485,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk227_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,false,X17,X18,X19,X20)
| ~ esk150_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ p(X17) ),
inference(resolution,[],[f1484,f1138]) ).
fof(f1486,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X17,X15,X5,X12,X13] :
( ~ esk167_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,false,X17)
| ~ p(X17)
| ~ esk150_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
inference(resolution,[],[f1485,f284]) ).
fof(f1492,plain,
! [X2,X21,X3,X10,X0,X11,X18,X8,X6,X9,X7,X14,X4,X16,X19,X1,X17,X15,X5,X12,X13,X20] :
( ~ esk187_22(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X0,X1)
| ~ p(X1)
| ~ esk175_20(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ p(X0) ),
inference(resolution,[],[f414,f1023]) ).
fof(f1521,plain,
! [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)
| ~ esk22_2(X0,X1) ),
inference(resolution,[],[f384,f559]) ).
fof(f1579,plain,
! [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)
| ~ esk24_2(X0,X1)
| ~ esk6_1(X0)
| ~ esk7_1(X0) ),
inference(resolution,[],[f1136,f1029]) ).
fof(f1582,plain,
! [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)
| ~ esk42_5(X0,X1,X2,X3,X4) ),
inference(resolution,[],[f153,f484]) ).
fof(f1586,plain,
! [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)
| ~ esk143_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) ),
inference(resolution,[],[f251,f11]) ).
fof(f1627,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( esk124_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)
| ~ p(X13)
| ~ p(X11)
| ~ p(X12) ),
inference(resolution,[],[f346,f1135]) ).
fof(f1689,definition,
( spl0_8
<=> ! [X6] : ~ p(X6) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f1690,plain,
( ! [X6] : ~ p(X6)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f1689]) ).
fof(f1695,plain,
( $false
| ~ spl0_8 ),
inference(resolution,[],[f1690,f1137]) ).
fof(f1747,plain,
~ spl0_8,
inference(avatar_contradiction_clause,[],[f1695]) ).
fof(f2887,plain,
! [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)
| ~ esk58_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(resolution,[],[f90,f668]) ).
fof(f5805,plain,
! [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)
| ~ esk87_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) ),
inference(resolution,[],[f710,f109]) ).
fof(f7640,plain,
! [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)
| ~ esk168_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
inference(resolution,[],[f94,f29]) ).
fof(f7701,plain,
! [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)
| ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ),
inference(resolution,[],[f641,f1112]) ).
fof(f7736,plain,
! [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)
| ~ esk128_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk87_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) ),
inference(resolution,[],[f999,f5805]) ).
fof(f8210,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X17,X15,X5,X12,X13] :
( esk170_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,X17,X18)
| ~ esk183_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,X17,X18)
| ~ p(X18)
| ~ p(X17) ),
inference(resolution,[],[f626,f1194]) ).
fof(f8211,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X17,X15,X5,X12,X13] :
( ~ esk183_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,X17,X18)
| ~ p(X18)
| ~ p(X17)
| ~ esk169_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,X17,X18)
| ~ esk168_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,X17,X18) ),
inference(resolution,[],[f8210,f7640]) ).
fof(f8212,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X17,X15,X5,X12,X13] :
( ~ esk169_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,X17,X18)
| ~ p(X17)
| ~ p(X18)
| ~ esk168_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,X17,X18) ),
inference(forward_subsumption_resolution,[],[f8211,f1017]) ).
fof(f8249,plain,
! [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)
| ~ esk152_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
inference(resolution,[],[f809,f948]) ).
fof(f8253,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( esk169_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk152_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk144_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk176_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
inference(resolution,[],[f8249,f726]) ).
fof(f8363,plain,
! [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)
| ~ esk150_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
inference(resolution,[],[f966,f856]) ).
fof(f9441,plain,
! [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)
| ~ esk146_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk150_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
inference(resolution,[],[f1009,f137]) ).
fof(f10622,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( 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)
| ~ esk149_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk150_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
inference(resolution,[],[f1035,f8363]) ).
fof(f10720,plain,
! [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)
| ~ esk155_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk116_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) ),
inference(resolution,[],[f1050,f7701]) ).
fof(f10722,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk234_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15,X16,X17,X18,X19,X20,X21)
| ~ esk162_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ p(X15)
| ~ p(X14) ),
inference(resolution,[],[f1086,f1213]) ).
fof(f10725,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( 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)
| ~ esk146_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk150_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
inference(resolution,[],[f1094,f9441]) ).
fof(f12653,plain,
! [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)
| ~ esk171_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
inference(resolution,[],[f215,f150]) ).
fof(f12884,plain,
! [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)
| ~ esk190_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) ),
inference(resolution,[],[f295,f18]) ).
fof(f12924,plain,
! [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)
| ~ esk192_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk171_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
inference(resolution,[],[f744,f12653]) ).
fof(f12926,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( 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)
| ~ p(X20)
| ~ p(X21) ),
inference(resolution,[],[f1026,f545]) ).
fof(f13714,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X17,X15,X5,X12,X13] :
( ~ esk152_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk144_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk176_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,X17,X18)
| ~ p(X17)
| ~ p(X18)
| ~ esk168_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,X17,X18) ),
inference(resolution,[],[f8253,f8212]) ).
fof(f13715,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X17,X15,X5,X12,X13] :
( ~ esk168_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,X17,X18)
| ~ esk144_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ p(X17)
| ~ p(X18)
| ~ esk152_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
inference(forward_subsumption_resolution,[],[f13714,f85]) ).
fof(f13716,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X17,X15,X5,X12,X13] :
( ~ esk144_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ p(X17)
| ~ p(X18)
| ~ esk152_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| esk167_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,false,X17,X18)
| ~ esk166_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
inference(resolution,[],[f13715,f81]) ).
fof(f13717,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X17,X15,X5,X12,X13] :
( ~ esk144_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ p(X17)
| ~ p(X18)
| ~ esk152_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) ),
inference(forward_subsumption_resolution,[],[f13716,f1460]) ).
fof(f13719,definition,
( spl0_90
<=> ! [X7,X2,X3,X10,X0,X11,X1,X8,X6,X9,X16,X14,X4,X15,X5,X12,X13] :
( ~ esk144_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)
| ~ esk152_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f13720,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk166_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk144_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) )
| ~ spl0_90 ),
inference(avatar_component_clause,[],[f13719]) ).
fof(f13721,plain,
( spl0_8
| spl0_8
| spl0_90 ),
inference(avatar_split_clause,[],[f13717,f13719,f1689,f1689]) ).
fof(f13724,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk144_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)
| ~ esk141_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
| ~ spl0_90 ),
inference(resolution,[],[f13720,f505]) ).
fof(f13730,plain,
( ! [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)
| ~ esk141_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) )
| ~ spl0_90 ),
inference(resolution,[],[f13724,f649]) ).
fof(f13738,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ esk141_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk152_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk162_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ p(X15)
| ~ p(X14) )
| ~ spl0_90 ),
inference(resolution,[],[f13730,f10722]) ).
fof(f13739,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ esk141_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk152_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ p(X15)
| ~ p(X14) )
| ~ spl0_90 ),
inference(forward_subsumption_resolution,[],[f13738,f16]) ).
fof(f13740,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( esk140_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ p(X15)
| ~ p(X14)
| ~ esk152_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk139_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
| ~ spl0_90 ),
inference(resolution,[],[f13739,f97]) ).
fof(f13741,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ p(X0)
| ~ p(X1)
| ~ esk152_17(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X1,false,X0)
| ~ esk139_14(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| ~ esk124_14(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| ~ p(X0)
| ~ p(X1) )
| ~ spl0_90 ),
inference(resolution,[],[f13740,f1432]) ).
fof(f13760,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ esk152_17(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X1,false,X0)
| ~ p(X1)
| ~ p(X0)
| ~ esk139_14(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| ~ esk124_14(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) )
| ~ spl0_90 ),
inference(duplicate_literal_removal,[],[f13741]) ).
fof(f16222,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk192_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk171_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk190_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) ),
inference(resolution,[],[f12924,f12884]) ).
fof(f16223,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk190_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21)
| ~ esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk171_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk188_22(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21) ),
inference(forward_subsumption_resolution,[],[f16222,f794]) ).
fof(f16228,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk171_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ 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)
| ~ p(X20)
| ~ p(X21) ),
inference(resolution,[],[f16223,f12926]) ).
fof(f16230,plain,
! [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)
| ~ esk171_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ p(X20)
| ~ p(X21) ),
inference(forward_subsumption_resolution,[],[f16228,f131]) ).
fof(f16233,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk171_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ p(X20)
| ~ p(X21)
| 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) ),
inference(resolution,[],[f16230,f277]) ).
fof(f16234,plain,
! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk171_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ p(X20)
| ~ p(X21)
| ~ esk186_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
inference(forward_subsumption_resolution,[],[f16233,f1492]) ).
fof(f16236,definition,
( spl0_109
<=> ! [X7,X2,X3,X10,X0,X11,X18,X8,X19,X9,X16,X14,X4,X1,X6,X17,X15,X5,X12,X13] :
( ~ esk171_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk186_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f16237,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( ~ esk171_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk186_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) )
| ~ spl0_109 ),
inference(avatar_component_clause,[],[f16236]) ).
fof(f16238,plain,
( spl0_8
| spl0_8
| spl0_109 ),
inference(avatar_split_clause,[],[f16234,f16236,f1689,f1689]) ).
fof(f16242,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( ~ esk178_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk186_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk146_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk150_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
| ~ spl0_109 ),
inference(resolution,[],[f16237,f10725]) ).
fof(f16356,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( ~ esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk186_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk146_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk150_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) )
| ~ spl0_109 ),
inference(resolution,[],[f16242,f643]) ).
fof(f16358,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( ~ esk175_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk146_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk150_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) )
| ~ spl0_109 ),
inference(forward_subsumption_resolution,[],[f16356,f170]) ).
fof(f16359,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( ~ esk146_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk150_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)
| ~ esk181_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk149_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk150_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
| ~ spl0_109 ),
inference(resolution,[],[f16358,f10622]) ).
fof(f16363,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( ~ esk146_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk150_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)
| ~ esk181_20(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
| ~ esk149_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
| ~ spl0_109 ),
inference(duplicate_literal_removal,[],[f16359]) ).
fof(f16364,plain,
( ! [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)
| ~ esk150_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk146_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) )
| ~ spl0_109 ),
inference(forward_subsumption_resolution,[],[f16363,f1072]) ).
fof(f16365,plain,
( ! [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)
| ~ esk146_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)
| ~ esk150_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) )
| ~ spl0_109 ),
inference(resolution,[],[f16364,f81]) ).
fof(f16391,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X17,X15,X5,X12,X13] :
( ~ esk146_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)
| ~ esk150_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)
| ~ p(X17)
| ~ esk150_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) )
| ~ spl0_109 ),
inference(resolution,[],[f16365,f1486]) ).
fof(f16392,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X17,X15,X5,X12,X13] :
( ~ esk146_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)
| ~ esk150_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)
| ~ p(X17) )
| ~ spl0_109 ),
inference(duplicate_literal_removal,[],[f16391]) ).
fof(f16394,definition,
( spl0_119
<=> ! [X7,X2,X3,X10,X0,X11,X1,X8,X6,X9,X16,X14,X4,X15,X5,X12,X13] :
( ~ esk146_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)
| ~ esk150_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) ) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f16395,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X15,X5,X12,X13] :
( ~ esk146_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)
| ~ esk150_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) )
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f16394]) ).
fof(f16396,plain,
( spl0_8
| spl0_119
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f16392,f16236,f16394,f1689]) ).
fof(f16397,plain,
( ! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( esk152_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ esk150_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)
| ~ esk166_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ 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) )
| ~ spl0_119 ),
inference(resolution,[],[f16395,f619]) ).
fof(f16416,plain,
( ! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk251_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15,X16,X17,X18,X19,X20,X21)
| ~ esk149_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk166_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk150_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ p(X14)
| ~ p(X15)
| ~ esk139_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) )
| ~ spl0_90
| ~ spl0_119 ),
inference(resolution,[],[f16397,f13760]) ).
fof(f16430,plain,
( ! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk149_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk166_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk150_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ p(X14)
| ~ p(X15)
| ~ esk139_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)
| ~ esk247_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15,X16,X17,X18,X19,X20,X21) )
| ~ spl0_90
| ~ spl0_119 ),
inference(resolution,[],[f16416,f533]) ).
fof(f16433,plain,
( ! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk247_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15,X16,X17,X18,X19,X20,X21)
| ~ esk166_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ p(X14)
| ~ p(X15)
| ~ esk139_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)
| ~ esk149_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15) )
| ~ spl0_90
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f16430,f22]) ).
fof(f16434,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ esk166_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ p(X14)
| ~ p(X15)
| ~ esk139_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)
| ~ esk149_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk155_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk116_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) )
| ~ spl0_90
| ~ spl0_119 ),
inference(resolution,[],[f16433,f10720]) ).
fof(f16439,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ esk149_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ p(X14)
| ~ p(X15)
| ~ esk139_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)
| ~ esk166_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk155_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk116_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
| ~ spl0_90
| ~ spl0_119 ),
inference(duplicate_literal_removal,[],[f16434]) ).
fof(f16441,plain,
( ! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( esk142_17(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X0,false,X1)
| ~ p(X1)
| ~ esk139_14(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| ~ esk124_14(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| ~ esk166_17(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X0,false,X1)
| ~ esk155_17(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X0,false,X1)
| ~ esk116_14(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| ~ p(X0)
| ~ esk248_23(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X0,false,X1,X16,X17,X18,X19,X20,X21) )
| ~ spl0_90
| ~ spl0_119 ),
inference(resolution,[],[f16439,f1134]) ).
fof(f16546,plain,
( ! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ p(X0)
| ~ esk139_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ esk124_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ esk166_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0)
| ~ esk155_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0)
| ~ esk116_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ p(X15)
| ~ esk248_23(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0,X16,X17,X18,X19,X20,X21)
| ~ esk143_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0)
| ~ esk141_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0) )
| ~ spl0_90
| ~ spl0_119 ),
inference(resolution,[],[f16441,f1586]) ).
fof(f16547,plain,
( ! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ p(X0)
| ~ esk124_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ esk166_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0)
| ~ esk155_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0)
| ~ esk116_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ p(X15)
| ~ esk248_23(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0,X16,X17,X18,X19,X20,X21)
| ~ esk143_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0)
| ~ esk141_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0) )
| ~ spl0_90
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f16546,f722]) ).
fof(f16548,plain,
( ! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ p(X0)
| ~ esk124_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ esk155_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0)
| ~ esk116_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ p(X15)
| ~ esk248_23(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0,X16,X17,X18,X19,X20,X21)
| ~ esk143_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0)
| ~ esk141_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0) )
| ~ spl0_90
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f16547,f505]) ).
fof(f16549,plain,
( ! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk248_23(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0,X16,X17,X18,X19,X20,X21)
| ~ esk124_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ esk116_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ p(X15)
| ~ p(X0)
| ~ esk143_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0)
| ~ esk141_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0) )
| ~ spl0_90
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f16548,f769]) ).
fof(f16550,plain,
( ! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk247_23(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15,X16,X17,X18,X19,X20,X21)
| ~ esk116_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ p(X14)
| ~ p(X15)
| ~ esk143_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk141_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
| ~ spl0_90
| ~ spl0_119 ),
inference(resolution,[],[f16549,f158]) ).
fof(f16554,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ esk116_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ p(X14)
| ~ p(X15)
| ~ esk143_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk141_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk155_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk116_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) )
| ~ spl0_90
| ~ spl0_119 ),
inference(resolution,[],[f16550,f10720]) ).
fof(f16563,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ esk116_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ p(X14)
| ~ p(X15)
| ~ esk143_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk141_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk155_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15) )
| ~ spl0_90
| ~ spl0_119 ),
inference(duplicate_literal_removal,[],[f16554]) ).
fof(f16568,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ esk143_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ p(X14)
| ~ p(X15)
| ~ esk116_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk141_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,false,X15)
| ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
| ~ spl0_90
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f16563,f769]) ).
fof(f16573,plain,
( ! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13,X20] :
( ~ esk234_23(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X0,false,X1,X16,X17,X18,X19,X20,X21)
| ~ p(X1)
| ~ esk116_14(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| ~ esk141_17(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X0,false,X1)
| ~ esk124_14(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
| ~ p(X0) )
| ~ spl0_90
| ~ spl0_119 ),
inference(resolution,[],[f16568,f771]) ).
fof(f16603,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ p(X0)
| ~ esk116_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ esk141_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0)
| ~ esk124_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ p(X15)
| ~ esk162_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0)
| ~ p(X0)
| ~ p(X15) )
| ~ spl0_90
| ~ spl0_119 ),
inference(resolution,[],[f16573,f10722]) ).
fof(f16605,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ p(X0)
| ~ esk116_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ esk141_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0)
| ~ esk124_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ p(X15)
| ~ esk162_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0) )
| ~ spl0_90
| ~ spl0_119 ),
inference(duplicate_literal_removal,[],[f16603]) ).
fof(f16606,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ esk141_17(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,false,X0)
| ~ esk116_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ p(X0)
| ~ esk124_14(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)
| ~ p(X15) )
| ~ spl0_90
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f16605,f16]) ).
fof(f16607,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ esk116_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ p(X14)
| ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ p(X15)
| esk140_17(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X15,false,X14)
| ~ esk139_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
| ~ spl0_90
| ~ spl0_119 ),
inference(resolution,[],[f16606,f97]) ).
fof(f16608,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X15,X5,X12,X13] :
( ~ esk116_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ p(X14)
| ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ p(X15)
| ~ esk139_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
| ~ spl0_90
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f16607,f1432]) ).
fof(f16610,definition,
( spl0_121
<=> ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ esk116_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)
| ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f16611,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ esk116_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)
| ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
| ~ spl0_121 ),
inference(avatar_component_clause,[],[f16610]) ).
fof(f16612,plain,
( spl0_8
| spl0_8
| spl0_121
| ~ spl0_90
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f16608,f16394,f13719,f16610,f1689,f1689]) ).
fof(f16613,plain,
( ! [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)
| ~ esk124_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) )
| ~ spl0_121 ),
inference(resolution,[],[f16611,f411]) ).
fof(f16618,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ esk128_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)
| ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk87_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) )
| ~ spl0_121 ),
inference(resolution,[],[f16613,f7736]) ).
fof(f16713,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ esk139_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)
| ~ esk87_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk112_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
| ~ spl0_121 ),
inference(resolution,[],[f16618,f394]) ).
fof(f16714,plain,
( ! [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)
| ~ esk87_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
| ~ spl0_121 ),
inference(forward_subsumption_resolution,[],[f16713,f766]) ).
fof(f16715,plain,
( ! [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)
| ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk87_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) )
| ~ spl0_121 ),
inference(resolution,[],[f16714,f15]) ).
fof(f16719,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk87_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)
| ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ p(X12)
| ~ p(X11)
| ~ p(X13) )
| ~ spl0_121 ),
inference(resolution,[],[f16715,f1395]) ).
fof(f16730,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ esk124_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk87_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)
| ~ p(X12)
| ~ p(X11)
| ~ p(X13) )
| ~ spl0_121 ),
inference(duplicate_literal_removal,[],[f16719]) ).
fof(f16731,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk87_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)
| ~ p(X11)
| ~ p(X12)
| ~ p(X13)
| ~ esk137_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X11,X13)
| ~ p(X13)
| ~ p(X12)
| ~ p(X11) )
| ~ spl0_121 ),
inference(resolution,[],[f16730,f1627]) ).
fof(f16732,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ esk137_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X11,X13)
| ~ esk87_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)
| ~ p(X11)
| ~ p(X12)
| ~ p(X13)
| ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) )
| ~ spl0_121 ),
inference(duplicate_literal_removal,[],[f16731]) ).
fof(f16736,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ esk87_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)
| ~ p(X11)
| ~ p(X12)
| ~ p(X13)
| ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk112_14(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X12,X11,X13) )
| ~ spl0_121 ),
inference(resolution,[],[f16732,f128]) ).
fof(f16737,plain,
( ! [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,X12,X11,X13)
| ~ p(X11)
| ~ p(X12)
| ~ p(X13)
| ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk87_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) )
| ~ spl0_121 ),
inference(forward_subsumption_resolution,[],[f16736,f1025]) ).
fof(f16738,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ esk97_11(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk87_11(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| esk111_14(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X1,X0,X2)
| ~ esk110_11(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
| ~ spl0_121 ),
inference(resolution,[],[f16737,f15]) ).
fof(f16739,plain,
( ! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ esk97_11(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk87_11(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk110_11(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
| ~ spl0_121 ),
inference(forward_subsumption_resolution,[],[f16738,f1395]) ).
fof(f16741,definition,
( spl0_122
<=> ! [X3,X10,X11,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ esk97_11(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk110_11(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk87_11(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) ) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f16742,plain,
( ! [X3,X10,X11,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ esk87_11(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk110_11(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| ~ esk97_11(X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) )
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f16741]) ).
fof(f16743,plain,
( spl0_122
| spl0_8
| spl0_8
| spl0_8
| ~ spl0_121 ),
inference(avatar_split_clause,[],[f16739,f16610,f1689,f1689,f1689,f16741]) ).
fof(f16744,plain,
( ! [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)
| ~ esk97_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) )
| ~ spl0_122 ),
inference(resolution,[],[f16742,f1047]) ).
fof(f16745,plain,
( ! [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)
| ~ esk110_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk97_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) )
| ~ spl0_122 ),
inference(resolution,[],[f16744,f1085]) ).
fof(f16749,plain,
( ! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ esk99_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk97_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)
| ~ esk58_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7) )
| ~ spl0_122 ),
inference(resolution,[],[f16745,f2887]) ).
fof(f16814,plain,
( ! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ esk97_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)
| ~ esk58_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk83_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) )
| ~ spl0_122 ),
inference(resolution,[],[f16749,f672]) ).
fof(f16815,plain,
( ! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ esk83_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk58_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10) )
| ~ spl0_122 ),
inference(forward_subsumption_resolution,[],[f16814,f194]) ).
fof(f16816,plain,
( ! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ esk58_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ p(X10)
| ~ p(X9)
| ~ p(X8)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk81_8(X0,X1,X2,X3,X4,X5,X6,X7) )
| ~ spl0_122 ),
inference(resolution,[],[f16815,f1357]) ).
fof(f16821,plain,
( ! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ esk97_11(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk58_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ p(X10)
| ~ p(X9)
| ~ p(X8)
| ~ esk81_8(X0,X1,X2,X3,X4,X5,X6,X7) )
| ~ spl0_122 ),
inference(duplicate_literal_removal,[],[f16816]) ).
fof(f16822,plain,
( ! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk58_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ p(X8)
| ~ p(X9)
| ~ p(X10)
| ~ esk81_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk108_11(X0,X1,X2,X3,X4,X5,X6,X7,X10,X9,X8)
| ~ p(X9)
| ~ p(X8)
| ~ p(X10) )
| ~ spl0_122 ),
inference(resolution,[],[f16821,f1465]) ).
fof(f16823,plain,
( ! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ esk108_11(X0,X1,X2,X3,X4,X5,X6,X7,X10,X9,X8)
| ~ esk58_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ p(X8)
| ~ p(X9)
| ~ p(X10)
| ~ esk81_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7) )
| ~ spl0_122 ),
inference(duplicate_literal_removal,[],[f16822]) ).
fof(f16827,plain,
( ! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ esk58_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ p(X8)
| ~ p(X9)
| ~ p(X10)
| ~ esk81_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk83_11(X0,X1,X2,X3,X4,X5,X6,X7,X10,X9,X8) )
| ~ spl0_122 ),
inference(resolution,[],[f16823,f205]) ).
fof(f16828,plain,
( ! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ esk83_11(X0,X1,X2,X3,X4,X5,X6,X7,X10,X9,X8)
| ~ p(X8)
| ~ p(X9)
| ~ p(X10)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk58_8(X0,X1,X2,X3,X4,X5,X6,X7) )
| ~ spl0_122 ),
inference(forward_subsumption_resolution,[],[f16827,f61]) ).
fof(f16829,plain,
( ! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ esk68_8(X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk58_8(X3,X4,X5,X6,X7,X8,X9,X10)
| ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ esk68_8(X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk81_8(X3,X4,X5,X6,X7,X8,X9,X10) )
| ~ spl0_122 ),
inference(resolution,[],[f16828,f1357]) ).
fof(f16838,plain,
( ! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ esk68_8(X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk58_8(X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk81_8(X3,X4,X5,X6,X7,X8,X9,X10) )
| ~ spl0_122 ),
inference(duplicate_literal_removal,[],[f16829]) ).
fof(f16840,definition,
( spl0_125
<=> ! [X5,X6,X10,X3,X7,X4,X9,X8] :
( ~ esk68_8(X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk81_8(X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk58_8(X3,X4,X5,X6,X7,X8,X9,X10) ) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f16841,plain,
( ! [X3,X10,X8,X6,X9,X7,X4,X5] :
( ~ esk58_8(X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk81_8(X3,X4,X5,X6,X7,X8,X9,X10)
| ~ esk68_8(X3,X4,X5,X6,X7,X8,X9,X10) )
| ~ spl0_125 ),
inference(avatar_component_clause,[],[f16840]) ).
fof(f16842,plain,
( spl0_125
| spl0_8
| spl0_8
| spl0_8
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f16838,f16741,f1689,f1689,f1689,f16840]) ).
fof(f16843,plain,
( ! [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)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk81_8(X0,X1,X2,X3,X4,X5,X6,X7) )
| ~ spl0_125 ),
inference(resolution,[],[f16841,f167]) ).
fof(f16844,plain,
( ! [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)
| ~ esk81_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk70_8(X0,X1,X2,X3,X4,X5,X6,X7) )
| ~ spl0_125 ),
inference(resolution,[],[f16843,f485]) ).
fof(f16848,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ esk70_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk81_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk32_5(X0,X1,X2,X3,X4)
| ~ esk42_5(X0,X1,X2,X3,X4) )
| ~ spl0_125 ),
inference(resolution,[],[f16844,f1582]) ).
fof(f17148,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk81_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk32_5(X0,X1,X2,X3,X4)
| ~ esk42_5(X0,X1,X2,X3,X4)
| ~ esk54_8(X0,X1,X2,X3,X4,X5,X6,X7) )
| ~ spl0_125 ),
inference(resolution,[],[f16848,f279]) ).
fof(f17149,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ esk54_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk32_5(X0,X1,X2,X3,X4)
| ~ esk42_5(X0,X1,X2,X3,X4)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7) )
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f17148,f175]) ).
fof(f17150,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( esk53_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk42_5(X0,X1,X2,X3,X4)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk32_5(X0,X1,X2,X3,X4)
| ~ esk52_5(X0,X1,X2,X3,X4) )
| ~ spl0_125 ),
inference(resolution,[],[f17149,f335]) ).
fof(f17153,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ esk42_5(X0,X1,X2,X3,X4)
| ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk32_5(X0,X1,X2,X3,X4)
| ~ esk52_5(X0,X1,X2,X3,X4)
| ~ esk42_5(X0,X1,X2,X3,X4)
| ~ p(X5)
| ~ p(X7)
| ~ p(X6) )
| ~ spl0_125 ),
inference(resolution,[],[f17150,f1318]) ).
fof(f17238,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ esk68_8(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ esk42_5(X0,X1,X2,X3,X4)
| ~ esk32_5(X0,X1,X2,X3,X4)
| ~ esk52_5(X0,X1,X2,X3,X4)
| ~ p(X5)
| ~ p(X7)
| ~ p(X6) )
| ~ spl0_125 ),
inference(duplicate_literal_removal,[],[f17153]) ).
fof(f17243,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ esk42_5(X0,X1,X2,X3,X4)
| ~ esk32_5(X0,X1,X2,X3,X4)
| ~ esk52_5(X0,X1,X2,X3,X4)
| ~ p(X5)
| ~ p(X6)
| ~ p(X7)
| ~ esk79_8(X0,X1,X2,X3,X4,X5,X7,X6)
| ~ p(X7)
| ~ p(X5)
| ~ p(X6) )
| ~ spl0_125 ),
inference(resolution,[],[f17238,f1412]) ).
fof(f17244,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ esk79_8(X0,X1,X2,X3,X4,X5,X7,X6)
| ~ esk32_5(X0,X1,X2,X3,X4)
| ~ esk52_5(X0,X1,X2,X3,X4)
| ~ p(X5)
| ~ p(X6)
| ~ p(X7)
| ~ esk42_5(X0,X1,X2,X3,X4) )
| ~ spl0_125 ),
inference(duplicate_literal_removal,[],[f17243]) ).
fof(f17247,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ esk32_5(X0,X1,X2,X3,X4)
| ~ esk52_5(X0,X1,X2,X3,X4)
| ~ p(X5)
| ~ p(X6)
| ~ p(X7)
| ~ esk42_5(X0,X1,X2,X3,X4)
| ~ esk54_8(X0,X1,X2,X3,X4,X5,X7,X6) )
| ~ spl0_125 ),
inference(resolution,[],[f17244,f332]) ).
fof(f17248,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ esk54_8(X0,X1,X2,X3,X4,X5,X7,X6)
| ~ p(X5)
| ~ p(X6)
| ~ p(X7)
| ~ esk42_5(X0,X1,X2,X3,X4)
| ~ esk32_5(X0,X1,X2,X3,X4) )
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f17247,f712]) ).
fof(f17249,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ esk42_5(X3,X4,X5,X6,X7)
| ~ esk32_5(X3,X4,X5,X6,X7)
| esk53_8(X3,X4,X5,X6,X7,X0,X2,X1)
| ~ esk52_5(X3,X4,X5,X6,X7) )
| ~ spl0_125 ),
inference(resolution,[],[f17248,f335]) ).
fof(f17250,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ esk42_5(X3,X4,X5,X6,X7)
| ~ esk32_5(X3,X4,X5,X6,X7)
| ~ esk52_5(X3,X4,X5,X6,X7) )
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f17249,f1318]) ).
fof(f17252,definition,
( spl0_127
<=> ! [X5,X4,X7,X6,X3] :
( ~ esk42_5(X3,X4,X5,X6,X7)
| ~ esk52_5(X3,X4,X5,X6,X7)
| ~ esk32_5(X3,X4,X5,X6,X7) ) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f17253,plain,
( ! [X3,X6,X7,X4,X5] :
( ~ esk32_5(X3,X4,X5,X6,X7)
| ~ esk52_5(X3,X4,X5,X6,X7)
| ~ esk42_5(X3,X4,X5,X6,X7) )
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f17252]) ).
fof(f17254,plain,
( spl0_127
| spl0_8
| spl0_8
| spl0_8
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f17250,f16840,f1689,f1689,f1689,f17252]) ).
fof(f17255,plain,
( ! [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)
| ~ esk42_5(X0,X1,X2,X3,X4)
| ~ esk52_5(X0,X1,X2,X3,X4) )
| ~ spl0_127 ),
inference(resolution,[],[f17253,f288]) ).
fof(f17256,plain,
( ! [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)
| ~ esk52_5(X0,X1,X2,X3,X4)
| ~ esk42_5(X0,X1,X2,X3,X4)
| ~ esk43_5(X0,X1,X2,X3,X4) )
| ~ spl0_127 ),
inference(resolution,[],[f17255,f58]) ).
fof(f17393,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ esk52_5(X0,X1,X2,X3,X4)
| ~ esk42_5(X0,X1,X2,X3,X4)
| ~ esk43_5(X0,X1,X2,X3,X4)
| ~ esk14_2(X0,X1)
| ~ esk22_2(X0,X1) )
| ~ spl0_127 ),
inference(resolution,[],[f17256,f1521]) ).
fof(f17419,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ esk42_5(X0,X1,X2,X3,X4)
| ~ esk43_5(X0,X1,X2,X3,X4)
| ~ esk14_2(X0,X1)
| ~ esk22_2(X0,X1)
| ~ esk28_5(X0,X1,X2,X3,X4) )
| ~ spl0_127 ),
inference(resolution,[],[f17393,f972]) ).
fof(f17420,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ esk28_5(X0,X1,X2,X3,X4)
| ~ esk14_2(X0,X1)
| ~ esk22_2(X0,X1)
| ~ esk42_5(X0,X1,X2,X3,X4) )
| ~ spl0_127 ),
inference(forward_subsumption_resolution,[],[f17419,f272]) ).
fof(f17422,plain,
( ! [X2,X3,X0,X1,X4] :
( esk27_5(X0,X1,X2,X3,X4)
| ~ esk22_2(X0,X1)
| ~ esk42_5(X0,X1,X2,X3,X4)
| ~ esk14_2(X0,X1)
| ~ esk26_2(X0,X1) )
| ~ spl0_127 ),
inference(resolution,[],[f17420,f41]) ).
fof(f17426,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ esk22_2(X0,X1)
| ~ esk42_5(X0,X1,X2,X3,X4)
| ~ esk14_2(X0,X1)
| ~ esk26_2(X0,X1)
| ~ p(X4)
| ~ p(X3)
| ~ esk22_2(X0,X1)
| ~ p(X2) )
| ~ spl0_127 ),
inference(resolution,[],[f17422,f1291]) ).
fof(f17427,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ esk42_5(X0,X1,X2,X3,X4)
| ~ esk22_2(X0,X1)
| ~ esk14_2(X0,X1)
| ~ esk26_2(X0,X1)
| ~ p(X4)
| ~ p(X3)
| ~ p(X2) )
| ~ spl0_127 ),
inference(duplicate_literal_removal,[],[f17426]) ).
fof(f17430,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ esk22_2(X0,X1)
| ~ esk14_2(X0,X1)
| ~ esk26_2(X0,X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ esk50_5(X0,X1,X4,X3,X2)
| ~ p(X3)
| ~ p(X2)
| ~ p(X4) )
| ~ spl0_127 ),
inference(resolution,[],[f17427,f1317]) ).
fof(f17431,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ esk50_5(X0,X1,X4,X3,X2)
| ~ esk14_2(X0,X1)
| ~ esk26_2(X0,X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ esk22_2(X0,X1) )
| ~ spl0_127 ),
inference(duplicate_literal_removal,[],[f17430]) ).
fof(f17434,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ esk14_2(X0,X1)
| ~ esk26_2(X0,X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ esk22_2(X0,X1)
| ~ esk28_5(X0,X1,X4,X3,X2) )
| ~ spl0_127 ),
inference(resolution,[],[f17431,f908]) ).
fof(f17435,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ esk28_5(X0,X1,X4,X3,X2)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ esk22_2(X0,X1)
| ~ esk14_2(X0,X1) )
| ~ spl0_127 ),
inference(forward_subsumption_resolution,[],[f17434,f289]) ).
fof(f17437,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ esk22_2(X3,X4)
| ~ esk14_2(X3,X4)
| esk27_5(X3,X4,X2,X1,X0)
| ~ esk26_2(X3,X4) )
| ~ spl0_127 ),
inference(resolution,[],[f17435,f41]) ).
fof(f17438,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ esk22_2(X3,X4)
| ~ esk14_2(X3,X4)
| ~ esk26_2(X3,X4) )
| ~ spl0_127 ),
inference(forward_subsumption_resolution,[],[f17437,f1291]) ).
fof(f17440,definition,
( spl0_128
<=> ! [X4,X3] :
( ~ esk22_2(X3,X4)
| ~ esk26_2(X3,X4)
| ~ esk14_2(X3,X4) ) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f17441,plain,
( ! [X3,X4] :
( ~ esk14_2(X3,X4)
| ~ esk26_2(X3,X4)
| ~ esk22_2(X3,X4) )
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f17440]) ).
fof(f17442,plain,
( spl0_128
| spl0_8
| spl0_8
| spl0_8
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f17438,f17252,f1689,f1689,f1689,f17440]) ).
fof(f17443,plain,
( ! [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)
| ~ esk22_2(X0,X1)
| ~ esk26_2(X0,X1) )
| ~ spl0_128 ),
inference(resolution,[],[f17441,f218]) ).
fof(f17736,plain,
( ! [X0,X1] :
( ~ esk24_2(X0,X1)
| ~ esk26_2(X0,X1)
| ~ esk22_2(X0,X1)
| ~ esk6_1(X0)
| ~ esk7_1(X0) )
| ~ spl0_128 ),
inference(resolution,[],[f17443,f1579]) ).
fof(f17739,plain,
( ! [X0,X1] :
( ~ esk26_2(X0,X1)
| ~ esk22_2(X0,X1)
| ~ esk6_1(X0)
| ~ esk7_1(X0)
| ~ esk11_2(X0,X1) )
| ~ spl0_128 ),
inference(resolution,[],[f17736,f826]) ).
fof(f17740,plain,
( ! [X0,X1] :
( ~ esk11_2(X0,X1)
| ~ esk6_1(X0)
| ~ esk7_1(X0)
| ~ esk22_2(X0,X1) )
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f17739,f920]) ).
fof(f17742,plain,
( ! [X0,X1] :
( ~ esk6_1(X0)
| ~ esk7_1(X0)
| ~ esk22_2(X0,X1)
| esk10_2(X0,X1)
| ~ esk9_1(X0) )
| ~ spl0_128 ),
inference(resolution,[],[f17740,f904]) ).
fof(f17743,plain,
( ! [X0,X1] :
( esk10_2(X0,X1)
| ~ esk22_2(X0,X1)
| ~ esk6_1(X0)
| ~ esk9_1(X0) )
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f17742,f172]) ).
fof(f17744,plain,
( ! [X0,X1] :
( ~ esk22_2(X0,X1)
| ~ esk6_1(X0)
| ~ esk9_1(X0)
| ~ esk7_1(X0)
| ~ p(X1) )
| ~ spl0_128 ),
inference(resolution,[],[f17743,f552]) ).
fof(f17745,plain,
( ! [X0,X1] :
( ~ esk6_1(X0)
| ~ esk9_1(X0)
| ~ esk7_1(X0)
| ~ p(X1)
| ~ p(X1)
| ~ esk23_2(X0,X1) )
| ~ spl0_128 ),
inference(resolution,[],[f17744,f257]) ).
fof(f17746,plain,
( ! [X0,X1] :
( ~ esk23_2(X0,X1)
| ~ esk9_1(X0)
| ~ esk7_1(X0)
| ~ p(X1)
| ~ esk6_1(X0) )
| ~ spl0_128 ),
inference(duplicate_literal_removal,[],[f17745]) ).
fof(f17747,plain,
( ! [X0,X1] :
( ~ esk9_1(X0)
| ~ esk7_1(X0)
| ~ p(X1)
| ~ esk6_1(X0)
| ~ esk11_2(X0,X1) )
| ~ spl0_128 ),
inference(resolution,[],[f17746,f660]) ).
fof(f17750,plain,
( ! [X0,X1] :
( ~ esk11_2(X0,X1)
| ~ p(X1)
| ~ esk6_1(X0)
| ~ esk7_1(X0) )
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f17747,f1004]) ).
fof(f17752,plain,
( ! [X0,X1] :
( ~ p(X0)
| ~ esk6_1(X1)
| ~ esk7_1(X1)
| esk10_2(X1,X0)
| ~ esk9_1(X1) )
| ~ spl0_128 ),
inference(resolution,[],[f17750,f904]) ).
fof(f17753,plain,
( ! [X0,X1] :
( ~ p(X0)
| ~ esk6_1(X1)
| ~ esk7_1(X1)
| ~ esk9_1(X1) )
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f17752,f552]) ).
fof(f17755,definition,
( spl0_129
<=> ! [X1] :
( ~ esk6_1(X1)
| ~ esk9_1(X1)
| ~ esk7_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f17756,plain,
( ! [X1] :
( ~ esk6_1(X1)
| ~ esk9_1(X1)
| ~ esk7_1(X1) )
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f17755]) ).
fof(f17757,plain,
( spl0_129
| spl0_8
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f17753,f17440,f1689,f17755]) ).
fof(f17758,plain,
( ! [X2,X21,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X22,X13,X20] :
( ~ esk9_1(X0)
| ~ esk7_1(X0)
| ~ 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) )
| ~ spl0_129 ),
inference(resolution,[],[f17756,f1041]) ).
fof(f17759,plain,
( ! [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)
| ~ esk9_1(X0) )
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f17758,f934]) ).
fof(f17763,plain,
( ! [X0] :
( ~ esk8_1(X0)
| ~ esk9_1(X0)
| ~ p(X0) )
| ~ spl0_129 ),
inference(resolution,[],[f17759,f1048]) ).
fof(f17767,plain,
( ! [X0] :
( ~ esk9_1(X0)
| ~ p(X0)
| ~ esk5_1(X0) )
| ~ spl0_129 ),
inference(resolution,[],[f17763,f855]) ).
fof(f17768,plain,
( ! [X0] :
( ~ esk9_1(X0)
| ~ p(X0) )
| ~ spl0_3
| ~ spl0_5
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f17767,f1172]) ).
fof(f17771,plain,
( ! [X0] :
( ~ p(X0)
| ~ esk5_1(X0) )
| ~ spl0_3
| ~ spl0_5
| ~ spl0_129 ),
inference(resolution,[],[f17768,f1022]) ).
fof(f17772,plain,
( ! [X0] : ~ p(X0)
| ~ spl0_3
| ~ spl0_5
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f17771,f1172]) ).
fof(f17773,plain,
( spl0_8
| ~ spl0_3
| ~ spl0_5
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f17772,f17755,f1157,f1149,f1689]) ).
cnf(s2,plain,
( ~ spl0_1
| spl0_3 ),
inference(sat_conversion,[],[f1151]) ).
cnf(s3,plain,
( ~ spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f1159]) ).
cnf(s6,plain,
spl0_4,
inference(sat_conversion,[],[f1170]) ).
cnf(s7,plain,
spl0_1,
inference(sat_conversion,[],[f1171]) ).
cnf(s10,plain,
~ spl0_8,
inference(sat_conversion,[],[f1747]) ).
cnf(s151,plain,
( spl0_8
| spl0_8
| spl0_90 ),
inference(sat_conversion,[],[f13721]) ).
cnf(s152,plain,
( spl0_8
| spl0_90 ),
inference(rat,[],[s151]) ).
cnf(s187,plain,
( spl0_8
| spl0_8
| spl0_109 ),
inference(sat_conversion,[],[f16238]) ).
cnf(s188,plain,
( spl0_8
| spl0_109 ),
inference(rat,[],[s187]) ).
cnf(s204,plain,
( spl0_8
| ~ spl0_109
| spl0_119 ),
inference(sat_conversion,[],[f16396]) ).
cnf(s207,plain,
( spl0_8
| spl0_8
| ~ spl0_90
| ~ spl0_119
| spl0_121 ),
inference(sat_conversion,[],[f16612]) ).
cnf(s208,plain,
( spl0_8
| ~ spl0_90
| ~ spl0_119
| spl0_121 ),
inference(rat,[],[s207]) ).
cnf(s209,plain,
( spl0_8
| spl0_8
| spl0_8
| ~ spl0_121
| spl0_122 ),
inference(sat_conversion,[],[f16743]) ).
cnf(s210,plain,
( spl0_8
| ~ spl0_121
| spl0_122 ),
inference(rat,[],[s209]) ).
cnf(s214,plain,
( spl0_8
| spl0_8
| spl0_8
| ~ spl0_122
| spl0_125 ),
inference(sat_conversion,[],[f16842]) ).
cnf(s215,plain,
( spl0_8
| ~ spl0_122
| spl0_125 ),
inference(rat,[],[s214]) ).
cnf(s218,plain,
( spl0_8
| spl0_8
| spl0_8
| ~ spl0_125
| spl0_127 ),
inference(sat_conversion,[],[f17254]) ).
cnf(s219,plain,
( spl0_8
| ~ spl0_125
| spl0_127 ),
inference(rat,[],[s218]) ).
cnf(s220,plain,
( spl0_8
| spl0_8
| spl0_8
| ~ spl0_127
| spl0_128 ),
inference(sat_conversion,[],[f17442]) ).
cnf(s221,plain,
( spl0_8
| ~ spl0_127
| spl0_128 ),
inference(rat,[],[s220]) ).
cnf(s222,plain,
( spl0_8
| ~ spl0_128
| spl0_129 ),
inference(sat_conversion,[],[f17757]) ).
cnf(s223,plain,
( ~ spl0_3
| ~ spl0_5
| spl0_8
| ~ spl0_129 ),
inference(sat_conversion,[],[f17773]) ).
cnf(s227,plain,
spl0_109,
inference(rat,[],[s188,s10]) ).
cnf(s233,plain,
spl0_90,
inference(rat,[],[s152,s10]) ).
cnf(s271,plain,
spl0_119,
inference(rat,[],[s204,s10,s227]) ).
cnf(s318,plain,
spl0_121,
inference(rat,[],[s208,s233,s10,s271]) ).
cnf(s331,plain,
spl0_122,
inference(rat,[],[s210,s10,s318]) ).
cnf(s333,plain,
spl0_125,
inference(rat,[],[s215,s10,s331]) ).
cnf(s334,plain,
spl0_127,
inference(rat,[],[s219,s10,s333]) ).
cnf(s335,plain,
spl0_128,
inference(rat,[],[s221,s10,s334]) ).
cnf(s336,plain,
spl0_129,
inference(rat,[],[s222,s10,s335]) ).
cnf(s345,plain,
spl0_5,
inference(rat,[],[s3,s6]) ).
cnf(s346,plain,
~ spl0_3,
inference(rat,[],[s223,s336,s10,s345]) ).
cnf(s347,plain,
$false,
inference(rat,[],[s2,s346,s7]) ).
fof(f17774,plain,
$false,
inference(avatar_sat_refutation,[],[s347]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO591-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n018.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 17:53:56 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.89/0.94 % (3625087)Will run a generic schedule for satisfiability detection.
% 3.89/0.94 % (3625096)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=140538468:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.89/0.94 % (3625093)% WARNING: option uhcvi not known.
% 3.89/0.94 % (3625092)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4090039466_2999 on theBenchmark for (2999ds/0Mi)
% 3.89/0.94 % (3625093)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2107205894:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.89/0.94 % (3625094)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4184367072:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.89/0.94 % (3625095)dis+10_1_sil=32000:sp=arity:random_seed=838911618:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.89/0.94 % (3625097)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3907846101:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.89/0.94 % (3625098)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3230992176:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.89/0.94 % (3625096)Instruction limit reached!
% 3.89/0.94 % (3625096)------------------------------
% 3.89/0.94 % (3625096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.89/0.94 % (3625096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.89/0.94 % (3625096)CaDiCaL version: 2.1.3
% 3.89/0.94 % (3625096)Termination reason: Instruction limit
% 3.89/0.94 % (3625096)Termination phase: Blocked clause elimination
% 3.89/0.94 % (3625096)Time elapsed: 0.026 s
% 3.89/0.94 % (3625096)Peak memory usage: 11 MB
% 3.89/0.94 % (3625096)Instructions burned: 119 (million)
% 3.89/0.94 % (3625106)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=334913799:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.89/0.94 % (3625095)Instruction limit reached!
% 3.89/0.94 % (3625095)------------------------------
% 3.89/0.94 % (3625095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.89/0.94 % (3625095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.89/0.94 % (3625095)CaDiCaL version: 2.1.3
% 3.89/0.94 % (3625095)Termination reason: Instruction limit
% 3.89/0.94 % (3625095)Termination phase: Saturation
% 3.89/0.94 % (3625095)Time elapsed: 0.058 s
% 3.89/0.94 % (3625095)Peak memory usage: 13 MB
% 3.89/0.94 % (3625095)Instructions burned: 104 (million)
% 3.89/0.94 % (3625097)Instruction limit reached!
% 3.89/0.94 % (3625097)------------------------------
% 3.89/0.94 % (3625097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.89/0.94 % (3625097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.89/0.94 % (3625097)CaDiCaL version: 2.1.3
% 3.89/0.94 % (3625097)Termination reason: Instruction limit
% 3.89/0.94 % (3625097)Termination phase: Saturation
% 3.89/0.94 % (3625097)Time elapsed: 0.064 s
% 3.89/0.94 % (3625097)Peak memory usage: 14 MB
% 3.89/0.94 % (3625097)Instructions burned: 132 (million)
% 3.89/0.94 % (3625108)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1336813676:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 3.89/0.94 % (3625098)Instruction limit reached!
% 3.89/0.94 % (3625098)------------------------------
% 3.89/0.94 % (3625098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.89/0.94 % (3625098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.89/0.94 % (3625098)CaDiCaL version: 2.1.3
% 3.89/0.94 % (3625098)Termination reason: Instruction limit
% 3.89/0.94 % (3625098)Termination phase: Saturation
% 3.89/0.94 % (3625098)Time elapsed: 0.083 s
% 3.89/0.94 % (3625098)Peak memory usage: 16 MB
% 3.89/0.94 % (3625098)Instructions burned: 161 (million)
% 3.89/0.94 % (3625109)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1387002958:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 3.89/0.94 % (3625112)ott-21_1_sil=16000:fs=off:random_seed=2263165529:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 3.89/0.94 % (3625108)Instruction limit reached!
% 3.89/0.94 % (3625108)------------------------------
% 3.89/0.94 % (3625108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.89/0.94 % (3625108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.24 % (3625108)CaDiCaL version: 2.1.3
% 6.37/1.24 % (3625108)Termination reason: Instruction limit
% 6.37/1.24 % (3625108)Termination phase: Blocked clause elimination
% 6.37/1.24 % (3625108)Time elapsed: 0.054 s
% 6.37/1.24 % (3625108)Peak memory usage: 11 MB
% 6.37/1.24 % (3625108)Instructions burned: 133 (million)
% 6.37/1.24 % Detected minimum model sizes of [1]
% 6.37/1.24 % Detected maximum model sizes of [2]
% 6.37/1.24 % TRYING [1]
% 6.37/1.24 % (3625106)Cannot represent all propositional literals internally
% 6.37/1.24 % (3625106)Refutation not found, incomplete strategy
% 6.37/1.24 % (3625106)------------------------------
% 6.37/1.24 % (3625106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.24 % (3625106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.24 % (3625106)CaDiCaL version: 2.1.3
% 6.37/1.24 % (3625106)Termination reason: Refutation not found, incomplete strategy
% 6.37/1.24 % (3625106)Time elapsed: 0.108 s
% 6.37/1.24 % (3625106)Peak memory usage: 15 MB
% 6.37/1.24 % (3625106)Instructions burned: 473 (million)
% 6.37/1.24 % (3625106)------------------------------
% 6.37/1.24 % (3625106)------------------------------
% 6.37/1.24 % (3625115)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=438551325:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 6.37/1.24 % (3625114)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=954391350:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 6.37/1.24 % (3625112)Instruction limit reached!
% 6.37/1.24 % (3625112)------------------------------
% 6.37/1.24 % (3625112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.24 % (3625112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.24 % (3625112)CaDiCaL version: 2.1.3
% 6.37/1.24 % (3625112)Termination reason: Instruction limit
% 6.37/1.24 % (3625112)Termination phase: Saturation
% 6.37/1.24 % (3625112)Time elapsed: 0.088 s
% 6.37/1.24 % (3625112)Peak memory usage: 13 MB
% 6.37/1.24 % (3625112)Instructions burned: 181 (million)
% 6.37/1.24 % Detected minimum model sizes of [1]
% 6.37/1.24 % Detected maximum model sizes of [2]
% 6.37/1.24 % TRYING [1]
% 6.37/1.24 % (3625092)Cannot represent all propositional literals internally
% 6.37/1.24 % (3625092)Refutation not found, incomplete strategy
% 6.37/1.24 % (3625092)------------------------------
% 6.37/1.24 % (3625092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.24 % (3625092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.24 % (3625092)CaDiCaL version: 2.1.3
% 6.37/1.24 % (3625092)Termination reason: Refutation not found, incomplete strategy
% 6.37/1.24 % (3625092)Time elapsed: 0.200 s
% 6.37/1.24 % (3625092)Peak memory usage: 15 MB
% 6.37/1.24 % (3625092)Instructions burned: 467 (million)
% 6.37/1.24 % (3625092)------------------------------
% 6.37/1.24 % (3625092)------------------------------
% 6.37/1.24 % (3625118)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3281884161:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 6.37/1.24 % (3625119)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2141685872:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 6.37/1.24 % Detected minimum model sizes of [1]
% 6.37/1.24 % Detected maximum model sizes of [2]
% 6.37/1.24 % TRYING [1]
% 6.37/1.24 % (3625115)Cannot represent all propositional literals internally
% 6.37/1.24 % (3625115)Refutation not found, incomplete strategy
% 6.37/1.24 % (3625115)------------------------------
% 6.37/1.24 % (3625115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.37/1.24 % (3625115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.37/1.24 % (3625115)CaDiCaL version: 2.1.3
% 6.37/1.24 % (3625115)Termination reason: Refutation not found, incomplete strategy
% 6.37/1.24 % (3625115)Time elapsed: 0.085 s
% 6.37/1.24 % (3625115)Peak memory usage: 14 MB
% 6.37/1.24 % (3625115)Instructions burned: 357 (million)
% 6.37/1.24 % (3625115)------------------------------
% 6.37/1.24 % (3625115)------------------------------
% 6.37/1.24 % (3625122)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2901808788:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 6.37/1.24 % Detected minimum model sizes of [1]
% 6.37/1.24 % Detected maximum model sizes of [2]
% 6.37/1.24 % fmb_start_size (= 14) larger than a detected sort maximum size!
% 6.37/1.24 % (3625119)Refutation not found, incomplete strategy
% 6.37/1.24 % (3625119)------------------------------
% 6.37/1.24 % (3625119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.67 % (3625119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.67 % (3625119)CaDiCaL version: 2.1.3
% 16.09/2.67 % (3625119)Termination reason: Refutation not found, incomplete strategy
% 16.09/2.67 % (3625119)Time elapsed: 0.162 s
% 16.09/2.67 % (3625119)Peak memory usage: 14 MB
% 16.09/2.67 % (3625119)Instructions burned: 369 (million)
% 16.09/2.67 % (3625119)------------------------------
% 16.09/2.67 % (3625119)------------------------------
% 16.09/2.67 % (3625114)Instruction limit reached!
% 16.09/2.67 % (3625114)------------------------------
% 16.09/2.67 % (3625114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.67 % (3625114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.67 % (3625114)CaDiCaL version: 2.1.3
% 16.09/2.67 % (3625114)Termination reason: Instruction limit
% 16.09/2.67 % (3625114)Termination phase: Saturation
% 16.09/2.67 % (3625114)Time elapsed: 0.238 s
% 16.09/2.67 % (3625114)Peak memory usage: 14 MB
% 16.09/2.67 % (3625114)Instructions burned: 479 (million)
% 16.09/2.67 % (3625124)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4188242948:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 16.09/2.67 % (3625125)fmb+10_1_sil=64000:random_seed=835136872:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 16.09/2.67 % (3625122)Instruction limit reached!
% 16.09/2.67 % (3625122)------------------------------
% 16.09/2.67 % (3625122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.67 % (3625122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.67 % (3625122)CaDiCaL version: 2.1.3
% 16.09/2.67 % (3625122)Termination reason: Instruction limit
% 16.09/2.67 % (3625122)Termination phase: Saturation
% 16.09/2.67 % (3625122)Time elapsed: 0.186 s
% 16.09/2.67 % (3625122)Peak memory usage: 19 MB
% 16.09/2.67 % (3625122)Instructions burned: 695 (million)
% 16.09/2.67 % (3625128)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4048312655:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 16.09/2.67 % (3625109)Instruction limit reached!
% 16.09/2.67 % (3625109)------------------------------
% 16.09/2.67 % (3625109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.67 % (3625109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.67 % (3625109)CaDiCaL version: 2.1.3
% 16.09/2.67 % (3625109)Termination reason: Instruction limit
% 16.09/2.67 % (3625109)Termination phase: Saturation
% 16.09/2.67 % (3625109)Time elapsed: 0.370 s
% 16.09/2.67 % (3625109)Peak memory usage: 19 MB
% 16.09/2.67 % (3625109)Instructions burned: 685 (million)
% 16.09/2.67 % (3625130)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=744679416:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 16.09/2.67 % Detected minimum model sizes of [1]
% 16.09/2.67 % Detected maximum model sizes of [2]
% 16.09/2.67 % fmb_start_size (= 20) larger than a detected sort maximum size!
% 16.09/2.67 % (3625128)Refutation not found, incomplete strategy
% 16.09/2.67 % (3625128)------------------------------
% 16.09/2.67 % (3625128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.67 % (3625128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.67 % (3625128)CaDiCaL version: 2.1.3
% 16.09/2.67 % (3625128)Termination reason: Refutation not found, incomplete strategy
% 16.09/2.67 % (3625128)Time elapsed: 0.082 s
% 16.09/2.67 % (3625128)Peak memory usage: 14 MB
% 16.09/2.67 % (3625128)Instructions burned: 347 (million)
% 16.09/2.67 % (3625128)------------------------------
% 16.09/2.67 % (3625128)------------------------------
% 16.09/2.67 % (3625132)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1928850292:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 16.09/2.67 % Detected minimum model sizes of [1]
% 16.09/2.67 % Detected maximum model sizes of [2]
% 16.09/2.67 % TRYING [1]
% 16.09/2.67 % (3625125)Cannot represent all propositional literals internally
% 16.09/2.67 % (3625125)Refutation not found, incomplete strategy
% 16.09/2.67 % (3625125)------------------------------
% 16.09/2.67 % (3625125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.67 % (3625125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.67 % (3625125)CaDiCaL version: 2.1.3
% 16.09/2.67 % (3625125)Termination reason: Refutation not found, incomplete strategy
% 16.09/2.67 % (3625125)Time elapsed: 0.211 s
% 16.09/2.67 % (3625125)Peak memory usage: 14 MB
% 16.09/2.67 % (3625125)Instructions burned: 448 (million)
% 16.09/2.67 % (3625125)------------------------------
% 16.09/2.67 % (3625125)------------------------------
% 16.09/2.67 % Detected minimum model sizes of [1]
% 16.09/2.67 % Detected maximum model sizes of [2]
% 16.09/2.67 % fmb_start_size (= 8) larger than a detected sort maximum size!
% 16.09/2.67 % (3625130)Refutation not found, incomplete strategy
% 16.09/2.67 % (3625130)------------------------------
% 16.09/2.67 % (3625130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.67 % (3625130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.67 % (3625130)CaDiCaL version: 2.1.3
% 16.09/2.67 % (3625130)Termination reason: Refutation not found, incomplete strategy
% 16.09/2.67 % (3625130)Time elapsed: 0.155 s
% 16.09/2.67 % (3625130)Peak memory usage: 14 MB
% 16.09/2.67 % (3625130)Instructions burned: 347 (million)
% 16.09/2.67 % (3625130)------------------------------
% 16.09/2.67 % (3625130)------------------------------
% 16.09/2.67 % (3625134)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3033528:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi)
% 16.09/2.67 % (3625135)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3712347099:i=6324_2992 on theBenchmark for (2992ds/6324Mi)
% 16.09/2.67 % (3625118)Instruction limit reached!
% 16.09/2.67 % (3625118)------------------------------
% 16.09/2.67 % (3625118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.67 % (3625118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.67 % (3625118)CaDiCaL version: 2.1.3
% 16.09/2.67 % (3625118)Termination reason: Instruction limit
% 16.09/2.67 % (3625118)Termination phase: Saturation
% 16.09/2.67 % (3625118)Time elapsed: 0.529 s
% 16.09/2.67 % (3625118)Peak memory usage: 25 MB
% 16.09/2.67 % (3625118)Instructions burned: 1179 (million)
% 16.09/2.67 % (3625138)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=642285987:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi)
% 16.09/2.67 % (3625124)Instruction limit reached!
% 16.09/2.67 % (3625124)------------------------------
% 16.09/2.67 % (3625124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.67 % (3625124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.67 % (3625124)CaDiCaL version: 2.1.3
% 16.09/2.67 % (3625124)Termination reason: Instruction limit
% 16.09/2.67 % (3625124)Termination phase: Saturation
% 16.09/2.67 % (3625124)Time elapsed: 0.424 s
% 16.09/2.67 % (3625124)Peak memory usage: 17 MB
% 16.09/2.67 % (3625124)Instructions burned: 880 (million)
% 16.09/2.67 % Detected minimum model sizes of [1]
% 16.09/2.67 % Detected maximum model sizes of [2]
% 16.09/2.67 % fmb_start_size (= 77) larger than a detected sort maximum size!
% 16.09/2.67 % (3625135)Refutation not found, incomplete strategy
% 16.09/2.67 % (3625135)------------------------------
% 16.09/2.67 % (3625135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.67 % (3625135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.67 % (3625135)CaDiCaL version: 2.1.3
% 16.09/2.67 % (3625135)Termination reason: Refutation not found, incomplete strategy
% 16.09/2.67 % (3625135)Time elapsed: 0.196 s
% 16.09/2.67 % (3625135)Peak memory usage: 15 MB
% 16.09/2.67 % (3625135)Instructions burned: 457 (million)
% 16.09/2.67 % (3625135)------------------------------
% 16.09/2.67 % (3625135)------------------------------
% 16.09/2.67 % (3625140)ott-2_1_sil=16000:newcnf=on:random_seed=2067634645:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi)
% 16.09/2.67 % (3625142)ott+10_1_sil=32000:tgt=ground:random_seed=3228275361:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi)
% 16.09/2.67 % Detected minimum model sizes of [1]
% 16.09/2.67 % Detected maximum model sizes of [2]
% 16.09/2.67 % fmb_start_size (= 16) larger than a detected sort maximum size!
% 16.09/2.67 % (3625138)Refutation not found, incomplete strategy
% 16.09/2.67 % (3625138)------------------------------
% 16.09/2.67 % (3625138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.67 % (3625138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.67 % (3625138)CaDiCaL version: 2.1.3
% 16.09/2.67 % (3625138)Termination reason: Refutation not found, incomplete strategy
% 16.09/2.67 % (3625138)Time elapsed: 0.162 s
% 16.09/2.67 % (3625138)Peak memory usage: 14 MB
% 16.09/2.67 % (3625138)Instructions burned: 373 (million)
% 16.09/2.67 % (3625138)------------------------------
% 16.09/2.67 % (3625138)------------------------------
% 16.09/2.67 % (3625144)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3444311093:i=54282_2989 on theBenchmark for (2989ds/54282Mi)
% 16.09/2.67 % Detected minimum model sizes of [1]
% 16.09/2.67 % Detected maximum model sizes of [2]
% 16.09/2.67 % TRYING [1]
% 16.09/2.67 % (3625144)Cannot represent all propositional literals internally
% 16.09/2.67 % (3625144)Refutation not found, incomplete strategy
% 16.09/2.67 % (3625144)------------------------------
% 16.09/2.67 % (3625144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.67 % (3625144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.67 % (3625144)CaDiCaL version: 2.1.3
% 16.09/2.67 % (3625144)Termination reason: Refutation not found, incomplete strategy
% 16.09/2.67 % (3625144)Time elapsed: 0.200 s
% 16.09/2.67 % (3625144)Peak memory usage: 15 MB
% 16.09/2.67 % (3625144)Instructions burned: 466 (million)
% 16.09/2.67 % (3625144)------------------------------
% 16.09/2.67 % (3625144)------------------------------
% 16.09/2.67 % (3625146)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1267636158:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi)
% 16.09/2.68 % (3625140)Instruction limit reached!
% 16.09/2.68 % (3625140)------------------------------
% 16.09/2.68 % (3625140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.68 % (3625140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.68 % (3625140)CaDiCaL version: 2.1.3
% 16.09/2.68 % (3625140)Termination reason: Instruction limit
% 16.09/2.68 % (3625140)Termination phase: Saturation
% 16.09/2.68 % (3625140)Time elapsed: 0.425 s
% 16.09/2.68 % (3625140)Peak memory usage: 19 MB
% 16.09/2.68 % (3625140)Instructions burned: 870 (million)
% 16.09/2.68 % (3625148)dis+21_1_sil=32000:sas=cadical:random_seed=2754344748:i=3773:amm=off_2986 on theBenchmark for (2986ds/3773Mi)
% 16.09/2.68 % (3625134)Instruction limit reached!
% 16.09/2.68 % (3625134)------------------------------
% 16.09/2.68 % (3625134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.68 % (3625134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.68 % (3625134)CaDiCaL version: 2.1.3
% 16.09/2.68 % (3625134)Termination reason: Instruction limit
% 16.09/2.68 % (3625134)Termination phase: Saturation
% 16.09/2.68 % (3625134)Time elapsed: 0.758 s
% 16.09/2.68 % (3625134)Peak memory usage: 28 MB
% 16.09/2.68 % (3625134)Instructions burned: 1474 (million)
% 16.09/2.68 % (3625150)ott+11_1_sil=16000:gs=on:random_seed=2174290987:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2985 on theBenchmark for (2985ds/2251Mi)
% 16.09/2.68 % (3625132)Instruction limit reached!
% 16.09/2.68 % (3625132)------------------------------
% 16.09/2.68 % (3625132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.68 % (3625132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.68 % (3625132)CaDiCaL version: 2.1.3
% 16.09/2.68 % (3625132)Termination reason: Instruction limit
% 16.09/2.68 % (3625132)Termination phase: Saturation
% 16.09/2.68 % (3625132)Time elapsed: 1.214 s
% 16.09/2.68 % (3625132)Peak memory usage: 28 MB
% 16.09/2.68 % (3625132)Instructions burned: 5132 (million)
% 16.09/2.68 % (3625152)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2989056129:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi)
% 16.09/2.68 % Detected minimum model sizes of [1]
% 16.09/2.68 % Detected maximum model sizes of [2]
% 16.09/2.68 % fmb_start_size (= 7) larger than a detected sort maximum size!
% 16.09/2.68 % (3625152)Refutation not found, incomplete strategy
% 16.09/2.68 % (3625152)------------------------------
% 16.09/2.68 % (3625152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.68 % (3625152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.68 % (3625152)CaDiCaL version: 2.1.3
% 16.09/2.68 % (3625152)Termination reason: Refutation not found, incomplete strategy
% 16.09/2.68 % (3625152)Time elapsed: 0.105 s
% 16.09/2.68 % (3625152)Peak memory usage: 14 MB
% 16.09/2.68 % (3625152)Instructions burned: 464 (million)
% 16.09/2.68 % (3625152)------------------------------
% 16.09/2.68 % (3625152)------------------------------
% 16.09/2.68 % (3625154)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=373532045:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi)
% 16.09/2.68 % (3625154) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3625087-3625154"...
% 16.09/2.68 % (3625154)...printing done.
% 16.09/2.68 % (3625154)Refutation found. Thanks to Tanya!
% 16.09/2.68 % SZS status Unsatisfiable for theBenchmark
% 16.09/2.68 % SZS output start Proof for theBenchmark
% See solution above
% 16.09/2.68 % (3625154)------------------------------
% 16.09/2.68 % (3625154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.09/2.68 % (3625154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.09/2.68 % (3625154)CaDiCaL version: 2.1.3
% 16.09/2.68 % (3625154)Termination reason: Refutation
% 16.09/2.68 % (3625154)Time elapsed: 0.464 s
% 16.09/2.68 % (3625154)Peak memory usage: 23 MB
% 16.09/2.68 % (3625154)Instructions burned: 1815 (million)
% 16.09/2.68 % (3625087)Success in time 2.436 s
% 16.09/2.68 % Vampire exiting
%------------------------------------------------------------------------------