%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : HWV078-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 : n003.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 11:20:10 AM UTC 2026
% Result : Unsatisfiable 14.43s 2.63s
% Output : Refutation 14.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 1
% Number of leaves : 449
% Syntax : Number of formulae : 450 ( 4 unt; 0 def)
% Number of atoms : 2809 ( 1 equ)
% Maximal formula atoms : 8 ( 6 avg)
% Number of connectives : 3686 (1327 ~;2359 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 11 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 66 ( 64 usr; 54 prp; 0-7 aty)
% Number of functors : 2 ( 2 usr; 2 con; 0-0 aty)
% Number of variables : 2044 (2044 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| ~ p(X5)
| ~ p(X6)
| esk54_7(X1,X3,X0,X2,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_1) ).
fof(f2,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| esk33_0
| esk34_0
| ~ esk55_7(X1,X2,X3,X4,X0,X5,X6)
| ~ esk35_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2) ).
fof(f3,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| ~ p(X5)
| p(X6)
| ~ esk54_7(X3,X2,X4,X5,X1,X6,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_3) ).
fof(f4,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| p(X3)
| ~ esk54_7(X0,X4,X5,X6,X1,X3,X2)
| p(X4)
| ~ p(X5)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4) ).
fof(f5,axiom,
( ~ esk46_0
| ~ esk49_0
| esk47_0
| ~ esk45_0
| ~ esk48_0
| esk50_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_5) ).
fof(f6,axiom,
( esk40_0
| esk53_0
| esk41_0
| esk52_0
| esk39_0
| esk51_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_6) ).
fof(f7,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| p(X2)
| p(X3)
| p(X4)
| ~ p(X5)
| ~ p(X6)
| ~ esk54_7(X5,X0,X3,X4,X6,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_7) ).
fof(f8,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk33_0
| esk34_0
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X5)
| ~ esk35_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_8) ).
fof(f9,axiom,
( esk46_0
| esk43_0
| ~ esk45_0
| esk44_0
| esk47_0
| ~ esk42_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_9) ).
fof(f10,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk46_0
| p(X0)
| ~ esk59_7(X1,X2,X3,X4,X5,X6,X0)
| esk45_0
| ~ esk47_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_10) ).
fof(f11,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| esk54_7(X0,X5,X4,X6,X3,X2,X1)
| ~ p(X5)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_11) ).
fof(f12,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk40_0
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk39_0
| p(X6)
| ~ esk41_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_12) ).
fof(f13,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| esk49_0
| ~ esk50_0
| esk60_7(X1,X2,X3,X4,X0,X5,X6)
| esk48_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_13) ).
fof(f14,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| p(X2)
| p(X3)
| p(X4)
| p(X5)
| ~ esk54_7(X5,X0,X6,X3,X1,X4,X2)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_14) ).
fof(f15,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| p(X3)
| ~ esk54_7(X4,X1,X5,X0,X3,X6,X2)
| ~ p(X4)
| p(X5)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_15) ).
fof(f16,axiom,
( ~ esk53_0
| ~ esk51_0
| ~ esk52_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_16) ).
fof(f17,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk11_0
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk56_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_17) ).
fof(f18,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk61_7(X0,X1,X2,X3,X4,X5,X6)
| esk52_0
| esk51_0
| ~ p(X4)
| ~ esk53_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_18) ).
fof(f19,axiom,
( ~ esk48_0
| ~ esk33_0
| esk35_0
| esk34_0
| esk49_0
| esk50_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_19) ).
fof(f20,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| esk54_7(X0,X4,X2,X5,X3,X6,X1)
| ~ p(X6)
| p(X5)
| p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_20) ).
fof(f21,axiom,
( esk42_0
| esk46_0
| esk47_0
| esk45_0
| esk43_0
| esk44_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_21) ).
fof(f22,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk43_0
| esk44_0
| esk42_0
| ~ p(X0)
| esk58_7(X1,X2,X0,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_22) ).
fof(f23,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk21_0
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| esk61_7(X0,X1,X2,X3,X4,X5,X6)
| esk59_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_23) ).
fof(f24,axiom,
( esk34_0
| esk51_0
| esk52_0
| esk53_0
| esk33_0
| esk35_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_24) ).
fof(f25,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| esk60_7(X1,X2,X3,X4,X5,X0,X6)
| ~ esk50_0
| ~ esk48_0
| esk49_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_25) ).
fof(f26,axiom,
( esk35_0
| ~ esk33_0
| ~ esk34_0
| ~ esk39_0
| esk41_0
| ~ esk40_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_26) ).
fof(f27,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| p(X2)
| ~ p(X3)
| esk54_7(X4,X3,X0,X5,X6,X2,X1)
| ~ p(X4)
| ~ p(X5)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_27) ).
fof(f28,axiom,
( ~ esk35_0
| ~ esk34_0
| ~ esk33_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_28) ).
fof(f29,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| p(X2)
| ~ p(X3)
| p(X4)
| esk54_7(X4,X5,X6,X0,X2,X3,X1)
| p(X6)
| p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_29) ).
fof(f30,axiom,
( esk33_0
| esk40_0
| esk34_0
| ~ esk35_0
| ~ esk41_0
| esk39_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_30) ).
fof(f31,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| esk49_0
| esk48_0
| esk50_0
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_31) ).
fof(f32,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk63_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk24_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_32) ).
fof(f33,axiom,
( ~ esk52_0
| ~ esk46_0
| ~ esk53_0
| esk51_0
| esk45_0
| ~ esk47_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_33) ).
fof(f34,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk35_0
| ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk33_0
| ~ esk34_0
| p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_34) ).
fof(f35,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk9_0
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| esk56_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_35) ).
fof(f36,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| esk54_7(X1,X2,X3,X4,X0,X5,X6)
| ~ p(X6)
| p(X4)
| p(X1)
| ~ p(X2)
| ~ p(X5)
| p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_36) ).
fof(f37,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ esk45_0
| esk47_0
| esk46_0
| esk59_7(X1,X0,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_37) ).
fof(f38,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk60_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk17_0
| esk63_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_38) ).
fof(f39,axiom,
( ~ esk52_0
| ~ esk51_0
| ~ esk37_0
| esk38_0
| ~ esk36_0
| esk53_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_39) ).
fof(f40,axiom,
( ~ esk49_0
| ~ esk50_0
| ~ esk48_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_40) ).
fof(f41,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| ~ esk54_7(X3,X0,X4,X5,X6,X1,X2)
| p(X6)
| p(X5)
| p(X3)
| p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_41) ).
fof(f42,axiom,
( esk42_0
| esk46_0
| esk43_0
| ~ esk47_0
| ~ esk44_0
| esk45_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_42) ).
fof(f43,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk14_0
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk56_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_43) ).
fof(f44,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ p(X5)
| ~ p(X6)
| esk54_7(X6,X4,X2,X3,X1,X0,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_44) ).
fof(f45,axiom,
( ~ esk53_0
| ~ esk34_0
| esk33_0
| ~ esk35_0
| esk51_0
| ~ esk52_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_45) ).
fof(f46,axiom,
( esk36_0
| esk41_0
| esk38_0
| ~ esk40_0
| esk39_0
| ~ esk37_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_46) ).
fof(f47,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ p(X2)
| ~ p(X3)
| esk54_7(X1,X4,X0,X2,X5,X3,X6)
| ~ p(X4)
| ~ p(X6)
| p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_47) ).
fof(f48,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| p(X2)
| p(X3)
| p(X4)
| p(X5)
| ~ esk54_7(X4,X0,X6,X2,X3,X5,X1)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_48) ).
fof(f49,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk42_0
| ~ esk43_0
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk44_0
| p(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_49) ).
fof(f50,axiom,
( ~ esk49_0
| esk48_0
| ~ esk50_0
| ~ esk44_0
| esk42_0
| ~ esk43_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_50) ).
fof(f51,axiom,
( ~ esk40_0
| ~ esk46_0
| esk47_0
| esk45_0
| esk41_0
| esk39_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_51) ).
fof(f52,axiom,
( esk43_0
| esk49_0
| ~ esk48_0
| ~ esk42_0
| esk50_0
| esk44_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_52) ).
fof(f53,axiom,
( esk40_0
| ~ esk51_0
| esk53_0
| ~ esk39_0
| esk41_0
| esk52_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_53) ).
fof(f54,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk54_7(X0,X1,X2,X3,X4,X5,X6)
| p(X2)
| ~ p(X3)
| ~ p(X0)
| p(X4)
| ~ p(X5)
| p(X6)
| ~ p(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_54) ).
fof(f55,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk6_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_55) ).
fof(f56,axiom,
( ~ esk42_0
| esk44_0
| esk41_0
| ~ esk40_0
| ~ esk43_0
| ~ esk39_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_56) ).
fof(f57,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| p(X2)
| ~ p(X3)
| p(X4)
| ~ esk54_7(X1,X5,X6,X2,X3,X0,X4)
| p(X6)
| p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_57) ).
fof(f58,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| esk54_7(X2,X3,X0,X4,X1,X5,X6)
| ~ p(X4)
| p(X3)
| ~ p(X6)
| ~ p(X5)
| ~ p(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_58) ).
fof(f59,axiom,
( ~ esk36_0
| esk35_0
| esk34_0
| esk37_0
| esk38_0
| ~ esk33_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_59) ).
fof(f60,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| esk39_0
| ~ esk57_7(X1,X2,X3,X4,X0,X5,X6)
| esk40_0
| ~ esk41_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_60) ).
fof(f61,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk4_0
| ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk57_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_61) ).
fof(f62,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk5_0
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk58_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_62) ).
fof(f63,axiom,
( esk40_0
| esk41_0
| esk48_0
| esk49_0
| esk39_0
| esk50_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_63) ).
fof(f64,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| esk15_0
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_64) ).
fof(f65,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk25_0
| ~ esk63_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk60_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_65) ).
fof(f66,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk49_0
| esk50_0
| ~ esk48_0
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| p(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_66) ).
fof(f67,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| p(X2)
| p(X3)
| p(X4)
| p(X5)
| ~ esk54_7(X5,X2,X4,X0,X6,X3,X1)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_67) ).
fof(f68,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ esk54_7(X2,X3,X1,X4,X0,X5,X6)
| p(X6)
| p(X3)
| ~ p(X5)
| p(X4)
| ~ p(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_68) ).
fof(f69,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk61_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk21_0
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk63_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_69) ).
fof(f70,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk3_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_70) ).
fof(f71,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| p(X2)
| esk54_7(X3,X4,X2,X5,X0,X6,X1)
| p(X6)
| ~ p(X3)
| ~ p(X5)
| p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_71) ).
fof(f72,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk41_0
| esk39_0
| esk40_0
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_72) ).
fof(f73,axiom,
( ~ esk52_0
| ~ esk51_0
| ~ esk34_0
| esk53_0
| esk35_0
| ~ esk33_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_73) ).
fof(f74,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| p(X5)
| ~ p(X6)
| esk54_7(X0,X1,X3,X6,X2,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_74) ).
fof(f75,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ esk54_7(X2,X3,X4,X1,X5,X0,X6)
| ~ p(X6)
| ~ p(X3)
| p(X4)
| ~ p(X5)
| p(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_75) ).
fof(f76,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk28_0
| esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk63_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_76) ).
fof(f77,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk22_0
| esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk59_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_77) ).
fof(f78,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk49_0
| p(X0)
| ~ esk60_7(X1,X2,X3,X0,X4,X5,X6)
| esk50_0
| ~ esk48_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_78) ).
fof(f79,axiom,
( ~ esk34_0
| esk39_0
| ~ esk41_0
| esk33_0
| ~ esk40_0
| ~ esk35_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_79) ).
fof(f80,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk55_7(X0,X1,X2,X3,X4,X5,X6)
| esk33_0
| esk35_0
| ~ p(X2)
| ~ esk34_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_80) ).
fof(f81,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| p(X2)
| ~ p(X3)
| esk54_7(X4,X5,X3,X0,X1,X6,X2)
| p(X6)
| ~ p(X5)
| ~ p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_81) ).
fof(f82,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| esk54_7(X1,X2,X3,X0,X4,X5,X6)
| ~ p(X2)
| ~ p(X6)
| p(X3)
| ~ p(X5)
| ~ p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_82) ).
fof(f83,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk59_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk45_0
| ~ p(X3)
| ~ esk46_0
| esk47_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_83) ).
fof(f84,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| p(X2)
| p(X3)
| ~ esk54_7(X4,X1,X3,X2,X5,X0,X6)
| ~ p(X4)
| p(X6)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_84) ).
fof(f85,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| esk54_7(X0,X1,X4,X5,X6,X3,X2)
| ~ p(X6)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_85) ).
fof(f86,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ esk54_7(X0,X2,X3,X4,X1,X5,X6)
| p(X6)
| ~ p(X5)
| ~ p(X3)
| p(X2)
| ~ p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_86) ).
fof(f87,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| esk54_7(X0,X2,X3,X4,X5,X1,X6)
| p(X2)
| p(X3)
| ~ p(X6)
| ~ p(X5)
| ~ p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_87) ).
fof(f88,axiom,
( esk35_0
| esk33_0
| esk34_0
| esk45_0
| esk47_0
| esk46_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_88) ).
fof(f89,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| p(X4)
| esk42_0
| esk43_0
| ~ esk44_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_89) ).
fof(f90,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ esk54_7(X2,X3,X4,X5,X1,X0,X6)
| p(X5)
| p(X4)
| ~ p(X2)
| p(X3)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_90) ).
fof(f91,axiom,
( ~ esk35_0
| esk52_0
| ~ esk51_0
| ~ esk53_0
| ~ esk33_0
| esk34_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_91) ).
fof(f92,axiom,
( ~ esk52_0
| ~ esk37_0
| esk36_0
| esk51_0
| ~ esk38_0
| ~ esk53_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_92) ).
fof(f93,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk51_0
| ~ esk53_0
| p(X0)
| ~ esk61_7(X1,X2,X3,X4,X5,X0,X6)
| esk52_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_93) ).
fof(f94,axiom,
( esk39_0
| esk36_0
| ~ esk38_0
| ~ esk41_0
| esk40_0
| esk37_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_94) ).
fof(f95,axiom,
( esk46_0
| ~ esk36_0
| esk37_0
| ~ esk45_0
| esk47_0
| esk38_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_95) ).
fof(f96,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk59_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| esk29_0
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_96) ).
fof(f97,axiom,
( ~ esk50_0
| esk49_0
| ~ esk41_0
| esk48_0
| esk39_0
| esk40_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_97) ).
fof(f98,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk29_0
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk61_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_98) ).
fof(f99,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk63_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk32_0
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_99) ).
fof(f100,axiom,
( esk36_0
| esk38_0
| ~ esk49_0
| ~ esk37_0
| esk50_0
| esk48_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_100) ).
fof(f101,axiom,
( ~ esk43_0
| esk39_0
| esk42_0
| ~ esk40_0
| ~ esk44_0
| ~ esk41_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_101) ).
fof(f102,axiom,
( esk52_0
| esk48_0
| esk51_0
| ~ esk50_0
| esk49_0
| ~ esk53_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_102) ).
fof(f103,axiom,
( ~ esk52_0
| esk36_0
| ~ esk37_0
| esk53_0
| esk38_0
| esk51_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_103) ).
fof(f104,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk44_0
| ~ esk43_0
| ~ p(X0)
| esk58_7(X1,X2,X3,X0,X4,X5,X6)
| ~ esk42_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_104) ).
fof(f105,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk45_0
| esk47_0
| ~ p(X0)
| esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk46_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_105) ).
fof(f106,axiom,
( esk46_0
| esk49_0
| ~ esk47_0
| ~ esk45_0
| ~ esk50_0
| ~ esk48_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_106) ).
fof(f107,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk8_0
| ~ esk56_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_107) ).
fof(f108,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk47_0
| ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk46_0
| p(X0)
| esk45_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_108) ).
fof(f109,axiom,
( esk42_0
| esk39_0
| ~ esk44_0
| esk40_0
| esk43_0
| ~ esk41_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_109) ).
fof(f110,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| esk54_7(X2,X3,X1,X4,X5,X0,X6)
| ~ p(X6)
| p(X3)
| ~ p(X2)
| p(X4)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_110) ).
fof(f111,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| ~ p(X2)
| esk54_7(X3,X0,X4,X5,X2,X6,X1)
| p(X3)
| p(X6)
| ~ p(X5)
| ~ p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_111) ).
fof(f112,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| p(X2)
| ~ p(X3)
| p(X4)
| p(X5)
| ~ esk54_7(X4,X2,X6,X5,X3,X1,X0)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_112) ).
fof(f113,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| p(X2)
| esk54_7(X3,X2,X0,X1,X4,X5,X6)
| ~ p(X3)
| ~ p(X5)
| p(X6)
| ~ p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_113) ).
fof(f114,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk54_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X0)
| ~ p(X5)
| ~ p(X2)
| ~ p(X1)
| ~ p(X3)
| ~ p(X6)
| ~ p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_114) ).
fof(f115,axiom,
( esk51_0
| esk53_0
| ~ esk52_0
| esk50_0
| esk48_0
| ~ esk49_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_115) ).
fof(f116,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ esk54_7(X1,X2,X3,X4,X0,X5,X6)
| ~ p(X2)
| ~ p(X6)
| p(X3)
| p(X4)
| p(X5)
| ~ p(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_116) ).
fof(f117,axiom,
( ~ esk50_0
| esk36_0
| ~ esk37_0
| esk48_0
| ~ esk49_0
| ~ esk38_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_117) ).
fof(f118,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| esk59_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk30_0
| ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| esk63_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_118) ).
fof(f119,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk50_0
| esk49_0
| esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X1)
| ~ esk48_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_119) ).
fof(f120,axiom,
( ~ esk53_0
| ~ esk38_0
| esk37_0
| ~ esk51_0
| esk52_0
| ~ esk36_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_120) ).
fof(f121,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk7_0
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk58_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_121) ).
fof(f122,axiom,
( esk37_0
| esk52_0
| ~ esk36_0
| esk53_0
| esk38_0
| ~ esk51_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_122) ).
fof(f123,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| p(X3)
| ~ esk54_7(X4,X0,X3,X5,X6,X1,X2)
| ~ p(X5)
| p(X6)
| p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_123) ).
fof(f124,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk44_0
| esk42_0
| ~ p(X6)
| ~ esk43_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_124) ).
fof(f125,axiom,
( esk43_0
| esk34_0
| ~ esk33_0
| esk35_0
| ~ esk42_0
| esk44_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_125) ).
fof(f126,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ esk50_0
| esk48_0
| esk60_7(X1,X2,X3,X4,X5,X6,X0)
| ~ esk49_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_126) ).
fof(f127,axiom,
( ~ esk37_0
| ~ esk36_0
| esk50_0
| ~ esk49_0
| ~ esk48_0
| esk38_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_127) ).
fof(f128,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk44_0
| ~ esk42_0
| esk43_0
| p(X0)
| ~ esk58_7(X1,X2,X3,X4,X5,X0,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_128) ).
fof(f129,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk20_0
| esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk63_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk61_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_129) ).
fof(f130,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk37_0
| esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk36_0
| ~ esk38_0
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_130) ).
fof(f131,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk37_0
| ~ p(X0)
| esk56_7(X1,X2,X0,X3,X4,X5,X6)
| esk36_0
| esk38_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_131) ).
fof(f132,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| p(X3)
| esk54_7(X4,X3,X2,X1,X5,X6,X0)
| ~ p(X5)
| ~ p(X4)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_132) ).
fof(f133,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk14_0
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk56_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_133) ).
fof(f134,axiom,
( esk50_0
| ~ esk48_0
| ~ esk40_0
| ~ esk39_0
| esk41_0
| ~ esk49_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_134) ).
fof(f135,axiom,
( esk53_0
| esk51_0
| esk44_0
| ~ esk43_0
| esk42_0
| ~ esk52_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_135) ).
fof(f136,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| p(X3)
| p(X4)
| ~ esk54_7(X3,X5,X4,X6,X0,X2,X1)
| ~ p(X5)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_136) ).
fof(f137,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| esk52_0
| ~ esk51_0
| esk53_0
| p(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_137) ).
fof(f138,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| esk35_0
| esk34_0
| esk33_0
| esk55_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_138) ).
fof(f139,axiom,
( ~ esk39_0
| esk40_0
| esk43_0
| ~ esk42_0
| ~ esk44_0
| ~ esk41_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_139) ).
fof(f140,axiom,
( ~ esk34_0
| esk36_0
| esk33_0
| esk38_0
| esk35_0
| ~ esk37_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_140) ).
fof(f141,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X4)
| ~ p(X5)
| p(X6)
| esk54_7(X6,X0,X1,X3,X5,X2,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_141) ).
fof(f142,axiom,
( esk53_0
| ~ esk39_0
| ~ esk51_0
| esk41_0
| ~ esk40_0
| ~ esk52_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_142) ).
fof(f143,axiom,
( ~ esk43_0
| esk41_0
| esk39_0
| esk42_0
| esk44_0
| ~ esk40_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_143) ).
fof(f144,axiom,
( ~ esk33_0
| esk52_0
| esk53_0
| ~ esk51_0
| esk34_0
| esk35_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_144) ).
fof(f145,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk11_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_145) ).
fof(f146,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ esk54_7(X1,X2,X0,X3,X4,X5,X6)
| p(X2)
| p(X6)
| ~ p(X3)
| p(X5)
| p(X1)
| p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_146) ).
fof(f147,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| esk54_7(X2,X0,X3,X4,X5,X1,X6)
| ~ p(X2)
| p(X5)
| p(X4)
| p(X3)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_147) ).
fof(f148,axiom,
( ~ esk33_0
| esk46_0
| ~ esk35_0
| esk34_0
| ~ esk45_0
| ~ esk47_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_148) ).
fof(f149,axiom,
( ~ esk38_0
| esk43_0
| ~ esk42_0
| esk37_0
| ~ esk44_0
| ~ esk36_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_149) ).
fof(f150,axiom,
( esk53_0
| esk51_0
| esk45_0
| esk47_0
| esk46_0
| esk52_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_150) ).
fof(f151,axiom,
( ~ esk33_0
| esk37_0
| ~ esk35_0
| ~ esk36_0
| esk34_0
| ~ esk38_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_151) ).
fof(f152,axiom,
( esk42_0
| esk44_0
| esk35_0
| ~ esk43_0
| esk33_0
| ~ esk34_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_152) ).
fof(f153,axiom,
( ~ esk41_0
| ~ esk47_0
| esk39_0
| esk45_0
| ~ esk46_0
| ~ esk40_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_153) ).
fof(f154,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ esk54_7(X1,X2,X3,X4,X5,X6,X0)
| p(X4)
| p(X5)
| p(X2)
| p(X1)
| p(X3)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_154) ).
fof(f155,axiom,
( ~ esk45_0
| ~ esk52_0
| esk53_0
| ~ esk46_0
| ~ esk51_0
| esk47_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_155) ).
fof(f156,axiom,
( esk40_0
| ~ esk45_0
| esk46_0
| ~ esk39_0
| esk47_0
| esk41_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_156) ).
fof(f157,axiom,
( ~ esk42_0
| esk37_0
| ~ esk36_0
| esk43_0
| esk44_0
| esk38_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_157) ).
fof(f158,axiom,
( ~ esk37_0
| esk47_0
| ~ esk46_0
| esk38_0
| esk45_0
| esk36_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_158) ).
fof(f159,axiom,
( esk36_0
| esk49_0
| esk37_0
| ~ esk38_0
| ~ esk50_0
| esk48_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_159) ).
fof(f160,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| esk54_7(X2,X0,X3,X4,X5,X6,X1)
| p(X6)
| p(X5)
| ~ p(X3)
| p(X2)
| ~ p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_160) ).
fof(f161,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| p(X2)
| ~ esk54_7(X3,X1,X0,X4,X5,X2,X6)
| p(X4)
| ~ p(X5)
| ~ p(X6)
| ~ p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_161) ).
fof(f162,axiom,
( esk38_0
| esk44_0
| esk36_0
| esk37_0
| esk42_0
| esk43_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_162) ).
fof(f163,axiom,
( esk53_0
| esk52_0
| esk51_0
| esk44_0
| esk42_0
| esk43_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_163) ).
fof(f164,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk48_0
| ~ esk49_0
| p(X0)
| esk50_0
| ~ esk60_7(X1,X2,X0,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_164) ).
fof(f165,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk9_0
| esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_165) ).
fof(f166,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| esk54_7(X3,X4,X5,X2,X0,X6,X1)
| p(X3)
| p(X6)
| ~ p(X5)
| p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_166) ).
fof(f167,axiom,
( ~ esk38_0
| ~ esk37_0
| ~ esk36_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_167) ).
fof(f168,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| p(X2)
| ~ esk54_7(X3,X4,X5,X1,X2,X6,X0)
| p(X4)
| p(X5)
| ~ p(X3)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_168) ).
fof(f169,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk18_0
| esk60_7(X0,X1,X2,X3,X4,X5,X6)
| esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk63_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_169) ).
fof(f170,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| p(X2)
| p(X3)
| ~ p(X4)
| p(X5)
| ~ p(X6)
| ~ esk54_7(X3,X6,X4,X1,X5,X2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_170) ).
fof(f171,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ p(X2)
| p(X3)
| ~ esk54_7(X4,X5,X6,X0,X2,X3,X1)
| p(X4)
| ~ p(X5)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_171) ).
fof(f172,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk54_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X2)
| p(X1)
| ~ p(X4)
| ~ p(X3)
| p(X6)
| p(X5)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_172) ).
fof(f173,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| p(X2)
| p(X3)
| p(X4)
| ~ p(X5)
| p(X6)
| ~ esk54_7(X1,X5,X3,X2,X4,X0,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_173) ).
fof(f174,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk20_0
| esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_174) ).
fof(f175,axiom,
( esk52_0
| esk43_0
| ~ esk42_0
| ~ esk51_0
| ~ esk44_0
| ~ esk53_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_175) ).
fof(f176,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| p(X2)
| p(X3)
| ~ p(X4)
| p(X5)
| p(X6)
| ~ esk54_7(X6,X0,X4,X5,X2,X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_176) ).
fof(f177,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk41_0
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk40_0
| p(X5)
| ~ esk39_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_177) ).
fof(f178,axiom,
( ~ esk40_0
| ~ esk52_0
| ~ esk53_0
| esk39_0
| ~ esk41_0
| esk51_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_178) ).
fof(f179,axiom,
( ~ esk33_0
| esk50_0
| ~ esk34_0
| esk35_0
| ~ esk48_0
| ~ esk49_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_179) ).
fof(f180,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk2_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_180) ).
fof(f181,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk63_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk31_0
| ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_181) ).
fof(f182,axiom,
( esk43_0
| ~ esk33_0
| ~ esk35_0
| ~ esk44_0
| esk34_0
| ~ esk42_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_182) ).
fof(f183,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk45_0
| esk46_0
| ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| p(X4)
| ~ esk47_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_183) ).
fof(f184,axiom,
( ~ esk48_0
| ~ esk50_0
| ~ esk36_0
| ~ esk38_0
| esk49_0
| esk37_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_184) ).
fof(f185,axiom,
( esk51_0
| esk34_0
| ~ esk35_0
| ~ esk53_0
| esk52_0
| esk33_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_185) ).
fof(f186,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| esk58_7(X1,X2,X3,X4,X5,X0,X6)
| ~ esk42_0
| esk43_0
| ~ esk44_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_186) ).
fof(f187,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| esk54_7(X3,X1,X4,X5,X2,X6,X0)
| ~ p(X5)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_187) ).
fof(f188,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| esk54_7(X1,X3,X0,X2,X4,X5,X6)
| ~ p(X6)
| p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_188) ).
fof(f189,axiom,
( ~ esk44_0
| ~ esk42_0
| ~ esk43_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_189) ).
fof(f190,axiom,
( ~ esk49_0
| ~ esk50_0
| ~ esk46_0
| ~ esk47_0
| esk45_0
| esk48_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_190) ).
fof(f191,axiom,
( esk50_0
| ~ esk42_0
| ~ esk48_0
| esk44_0
| ~ esk43_0
| ~ esk49_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_191) ).
fof(f192,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| ~ p(X5)
| ~ p(X6)
| esk54_7(X0,X3,X4,X6,X2,X5,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_192) ).
fof(f193,axiom,
( esk34_0
| esk41_0
| esk35_0
| ~ esk39_0
| esk40_0
| ~ esk33_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_193) ).
fof(f194,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk27_0
| ~ esk59_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_194) ).
fof(f195,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk16_0
| ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_195) ).
fof(f196,axiom,
( ~ esk51_0
| esk44_0
| esk53_0
| ~ esk42_0
| ~ esk52_0
| ~ esk43_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_196) ).
fof(f197,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| esk54_7(X3,X0,X1,X4,X5,X6,X2)
| p(X4)
| p(X6)
| p(X3)
| p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_197) ).
fof(f198,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk54_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X2)
| p(X5)
| p(X1)
| ~ p(X4)
| p(X3)
| p(X0)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_198) ).
fof(f199,axiom,
( esk44_0
| esk48_0
| ~ esk43_0
| esk42_0
| ~ esk49_0
| esk50_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_199) ).
fof(f200,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| p(X2)
| p(X3)
| p(X4)
| ~ esk54_7(X3,X0,X5,X4,X2,X6,X1)
| p(X6)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_200) ).
fof(f201,axiom,
( esk45_0
| esk46_0
| ~ esk41_0
| esk39_0
| esk40_0
| ~ esk47_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_201) ).
fof(f202,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| p(X2)
| p(X3)
| p(X4)
| ~ esk54_7(X5,X6,X1,X0,X2,X4,X3)
| p(X6)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_202) ).
fof(f203,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| esk54_7(X1,X3,X0,X2,X4,X5,X6)
| p(X6)
| ~ p(X5)
| ~ p(X4)
| p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_203) ).
fof(f204,axiom,
( ~ esk34_0
| esk35_0
| esk51_0
| ~ esk52_0
| esk33_0
| esk53_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_204) ).
fof(f205,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk60_7(X0,X1,X2,X3,X4,X5,X6)
| esk26_0
| esk59_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_205) ).
fof(f206,axiom,
( esk34_0
| esk38_0
| esk35_0
| esk37_0
| esk33_0
| esk36_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_206) ).
fof(f207,axiom,
( esk40_0
| esk35_0
| esk39_0
| esk41_0
| esk34_0
| esk33_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_207) ).
fof(f208,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk31_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_208) ).
fof(f209,axiom,
( esk37_0
| esk48_0
| esk49_0
| esk38_0
| esk36_0
| esk50_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_209) ).
fof(f210,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk33_0
| esk35_0
| ~ p(X3)
| ~ esk34_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_210) ).
fof(f211,axiom,
( ~ esk37_0
| esk36_0
| ~ esk44_0
| ~ esk43_0
| ~ esk38_0
| esk42_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_211) ).
fof(f212,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X4)
| p(X5)
| ~ p(X6)
| esk54_7(X1,X6,X5,X3,X4,X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_212) ).
fof(f213,axiom,
( esk37_0
| esk46_0
| ~ esk45_0
| ~ esk38_0
| ~ esk47_0
| ~ esk36_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_213) ).
fof(f214,axiom,
( ~ esk46_0
| ~ esk45_0
| ~ esk47_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_214) ).
fof(f215,axiom,
( ~ esk39_0
| ~ esk41_0
| esk46_0
| esk40_0
| ~ esk45_0
| ~ esk47_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_215) ).
fof(f216,axiom,
( esk51_0
| esk36_0
| esk38_0
| esk52_0
| esk53_0
| esk37_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_216) ).
fof(f217,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk12_0
| ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| esk57_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_217) ).
fof(f218,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk54_7(X0,X1,X2,X3,X4,X5,X6)
| p(X4)
| ~ p(X0)
| p(X1)
| ~ p(X3)
| ~ p(X2)
| ~ p(X5)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_218) ).
fof(f219,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ esk48_0
| ~ esk49_0
| esk50_0
| esk60_7(X1,X2,X3,X0,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_219) ).
fof(f220,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X1)
| esk43_0
| ~ esk42_0
| esk44_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_220) ).
fof(f221,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk7_0
| ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_221) ).
fof(f222,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ esk51_0
| esk53_0
| ~ esk52_0
| esk61_7(X1,X2,X3,X0,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_222) ).
fof(f223,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk38_0
| p(X0)
| esk37_0
| ~ esk56_7(X1,X2,X3,X4,X0,X5,X6)
| esk36_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_223) ).
fof(f224,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ p(X2)
| ~ esk54_7(X3,X4,X0,X5,X2,X1,X6)
| ~ p(X6)
| ~ p(X4)
| ~ p(X3)
| p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_224) ).
fof(f225,axiom,
( ~ esk39_0
| esk40_0
| esk41_0
| esk43_0
| esk44_0
| ~ esk42_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_225) ).
fof(f226,axiom,
( ~ esk42_0
| ~ esk43_0
| ~ esk37_0
| ~ esk36_0
| esk44_0
| esk38_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_226) ).
fof(f227,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| esk54_7(X0,X1,X2,X3,X4,X5,X6)
| p(X4)
| ~ p(X2)
| ~ p(X5)
| p(X3)
| ~ p(X6)
| ~ p(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_227) ).
fof(f228,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk52_0
| esk53_0
| esk51_0
| ~ p(X0)
| esk61_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_228) ).
fof(f229,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk54_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X6)
| p(X1)
| ~ p(X2)
| p(X5)
| ~ p(X3)
| p(X0)
| p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_229) ).
fof(f230,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X4)
| p(X5)
| ~ esk54_7(X4,X0,X5,X1,X6,X3,X2)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_230) ).
fof(f231,axiom,
( ~ esk48_0
| esk49_0
| ~ esk45_0
| esk46_0
| esk50_0
| esk47_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_231) ).
fof(f232,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk33_0
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| esk34_0
| ~ p(X4)
| ~ esk35_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_232) ).
fof(f233,axiom,
( esk46_0
| esk34_0
| esk33_0
| ~ esk35_0
| esk45_0
| ~ esk47_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_233) ).
fof(f234,axiom,
( esk36_0
| ~ esk38_0
| esk43_0
| esk42_0
| esk37_0
| ~ esk44_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_234) ).
fof(f235,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| esk54_7(X0,X4,X3,X5,X6,X2,X1)
| ~ p(X4)
| ~ p(X6)
| p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_235) ).
fof(f236,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk63_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk24_0
| esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_236) ).
fof(f237,axiom,
( ~ esk37_0
| esk38_0
| esk41_0
| ~ esk40_0
| ~ esk39_0
| ~ esk36_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_237) ).
fof(f238,axiom,
( esk53_0
| ~ esk52_0
| ~ esk40_0
| esk39_0
| esk51_0
| esk41_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_238) ).
fof(f239,axiom,
( ~ esk38_0
| esk51_0
| ~ esk53_0
| esk37_0
| esk36_0
| esk52_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_239) ).
fof(f240,axiom,
( esk33_0
| ~ esk34_0
| esk48_0
| ~ esk49_0
| esk35_0
| esk50_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_240) ).
fof(f241,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk50_0
| ~ esk49_0
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| p(X6)
| esk48_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_241) ).
fof(f242,axiom,
( esk43_0
| esk42_0
| ~ esk35_0
| ~ esk44_0
| esk33_0
| esk34_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_242) ).
fof(f243,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| esk54_7(X2,X3,X4,X5,X1,X0,X6)
| p(X3)
| p(X5)
| p(X2)
| ~ p(X6)
| p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_243) ).
fof(f244,axiom,
( ~ esk46_0
| esk44_0
| ~ esk45_0
| ~ esk42_0
| ~ esk43_0
| esk47_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_244) ).
fof(f245,axiom,
( ~ esk46_0
| ~ esk47_0
| esk36_0
| ~ esk37_0
| esk45_0
| ~ esk38_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_245) ).
fof(f246,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| p(X5)
| esk54_7(X6,X2,X4,X1,X5,X3,X0)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_246) ).
fof(f247,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk47_0
| esk46_0
| ~ p(X0)
| esk45_0
| esk59_7(X1,X2,X3,X4,X0,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_247) ).
fof(f248,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X4)
| ~ p(X5)
| esk54_7(X6,X5,X0,X2,X3,X4,X1)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_248) ).
fof(f249,axiom,
( esk48_0
| esk49_0
| esk50_0
| esk51_0
| esk52_0
| esk53_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_249) ).
fof(f250,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk37_0
| p(X0)
| esk36_0
| ~ esk38_0
| ~ esk56_7(X1,X2,X3,X4,X5,X6,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_250) ).
fof(f251,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk47_0
| ~ esk45_0
| p(X1)
| esk46_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_251) ).
fof(f252,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| esk54_7(X2,X0,X3,X1,X4,X5,X6)
| p(X4)
| ~ p(X3)
| p(X2)
| ~ p(X6)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_252) ).
fof(f253,axiom,
( esk33_0
| esk44_0
| esk42_0
| esk43_0
| esk35_0
| esk34_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_253) ).
fof(f254,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk40_0
| ~ esk41_0
| esk57_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X6)
| esk39_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_254) ).
fof(f255,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk41_0
| esk40_0
| p(X1)
| ~ esk39_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_255) ).
fof(f256,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk35_0
| ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| p(X5)
| esk34_0
| ~ esk33_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_256) ).
fof(f257,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk54_7(X0,X1,X2,X3,X4,X5,X6)
| p(X3)
| ~ p(X5)
| p(X2)
| p(X6)
| p(X4)
| ~ p(X1)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_257) ).
fof(f258,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| esk37_0
| ~ esk36_0
| ~ esk38_0
| ~ esk56_7(X1,X2,X3,X4,X5,X0,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_258) ).
fof(f259,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ p(X2)
| p(X3)
| esk54_7(X1,X4,X0,X5,X6,X2,X3)
| ~ p(X4)
| ~ p(X5)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_259) ).
fof(f260,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk49_0
| esk48_0
| esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X0)
| esk50_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_260) ).
fof(f261,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| p(X2)
| p(X3)
| ~ p(X4)
| p(X5)
| ~ p(X6)
| ~ esk54_7(X3,X1,X5,X4,X2,X6,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_261) ).
fof(f262,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X4)
| esk54_7(X2,X5,X3,X1,X0,X6,X4)
| p(X6)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_262) ).
fof(f263,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk41_0
| ~ p(X0)
| esk57_7(X1,X2,X3,X4,X0,X5,X6)
| esk39_0
| esk40_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_263) ).
fof(f264,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk42_0
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk44_0
| p(X3)
| ~ esk43_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_264) ).
fof(f265,axiom,
( ~ esk52_0
| ~ esk44_0
| esk51_0
| ~ esk53_0
| ~ esk43_0
| esk42_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_265) ).
fof(f266,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| p(X2)
| p(X3)
| ~ p(X4)
| p(X5)
| ~ p(X6)
| esk54_7(X4,X0,X6,X2,X1,X5,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_266) ).
fof(f267,axiom,
( esk39_0
| esk41_0
| esk40_0
| esk38_0
| esk36_0
| esk37_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_267) ).
fof(f268,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk41_0
| ~ esk40_0
| ~ p(X0)
| esk39_0
| esk57_7(X1,X2,X0,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_268) ).
fof(f269,axiom,
( ~ esk53_0
| ~ esk50_0
| ~ esk48_0
| esk52_0
| ~ esk51_0
| esk49_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_269) ).
fof(f270,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| p(X4)
| ~ esk53_0
| esk51_0
| esk52_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_270) ).
fof(f271,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk3_0
| esk57_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk56_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_271) ).
fof(f272,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| esk54_7(X1,X2,X3,X4,X0,X5,X6)
| p(X5)
| ~ p(X2)
| ~ p(X4)
| ~ p(X6)
| ~ p(X3)
| ~ p(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_272) ).
fof(f273,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| esk51_0
| ~ esk52_0
| esk53_0
| p(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_273) ).
fof(f274,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| p(X2)
| ~ p(X3)
| p(X4)
| ~ p(X5)
| ~ esk54_7(X3,X4,X5,X0,X6,X2,X1)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_274) ).
fof(f275,axiom,
( ~ esk40_0
| esk39_0
| esk41_0
| esk50_0
| ~ esk49_0
| esk48_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_275) ).
fof(f276,axiom,
( esk38_0
| esk36_0
| esk47_0
| esk37_0
| esk45_0
| esk46_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_276) ).
fof(f277,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk41_0
| ~ p(X0)
| esk40_0
| ~ esk39_0
| esk57_7(X1,X0,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_277) ).
fof(f278,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk38_0
| esk37_0
| ~ esk36_0
| esk56_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_278) ).
fof(f279,axiom,
( ~ esk38_0
| ~ esk41_0
| ~ esk39_0
| esk40_0
| ~ esk36_0
| esk37_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_279) ).
fof(f280,axiom,
( esk33_0
| ~ esk34_0
| ~ esk49_0
| ~ esk35_0
| ~ esk50_0
| esk48_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_280) ).
fof(f281,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk13_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_281) ).
fof(f282,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| p(X2)
| ~ p(X3)
| p(X4)
| p(X5)
| esk54_7(X2,X4,X5,X3,X1,X0,X6)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_282) ).
fof(f283,axiom,
( ~ esk50_0
| esk48_0
| ~ esk44_0
| esk42_0
| esk49_0
| esk43_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_283) ).
fof(f284,axiom,
( esk49_0
| esk48_0
| esk47_0
| esk50_0
| esk46_0
| esk45_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_284) ).
fof(f285,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk41_0
| ~ p(X3)
| ~ esk39_0
| ~ esk40_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_285) ).
fof(f286,axiom,
( esk45_0
| ~ esk46_0
| ~ esk34_0
| ~ esk47_0
| ~ esk35_0
| esk33_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_286) ).
fof(f287,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| esk54_7(X0,X1,X2,X3,X4,X5,X6)
| p(X4)
| ~ p(X5)
| ~ p(X2)
| ~ p(X1)
| ~ p(X6)
| p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_287) ).
fof(f288,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| esk54_7(X3,X1,X4,X5,X2,X0,X6)
| p(X5)
| ~ p(X4)
| ~ p(X3)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_288) ).
fof(f289,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X4)
| p(X5)
| ~ esk54_7(X0,X2,X4,X1,X6,X5,X3)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_289) ).
fof(f290,axiom,
( ~ esk33_0
| ~ esk41_0
| esk40_0
| ~ esk35_0
| esk34_0
| ~ esk39_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_290) ).
fof(f291,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X4)
| ~ esk54_7(X4,X5,X6,X1,X0,X2,X3)
| ~ p(X5)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_291) ).
fof(f292,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| esk54_7(X2,X5,X4,X1,X6,X3,X0)
| p(X6)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_292) ).
fof(f293,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk46_0
| esk59_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk47_0
| ~ p(X5)
| ~ esk45_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_293) ).
fof(f294,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| esk46_0
| ~ esk47_0
| ~ esk45_0
| ~ esk59_7(X1,X2,X3,X4,X5,X0,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_294) ).
fof(f295,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk60_7(X0,X1,X2,X3,X4,X5,X6)
| esk61_7(X0,X1,X2,X3,X4,X5,X6)
| esk19_0
| ~ esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_295) ).
fof(f296,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| esk54_7(X0,X1,X4,X3,X2,X5,X6)
| ~ p(X6)
| p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_296) ).
fof(f297,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| p(X3)
| p(X4)
| p(X5)
| esk54_7(X2,X4,X5,X0,X1,X3,X6)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_297) ).
fof(f298,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| p(X0)
| esk53_0
| esk52_0
| esk51_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_298) ).
fof(f299,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| esk54_7(X1,X2,X3,X4,X5,X6,X0)
| ~ p(X1)
| ~ p(X6)
| p(X2)
| p(X5)
| ~ p(X4)
| ~ p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_299) ).
fof(f300,axiom,
( esk47_0
| esk53_0
| ~ esk46_0
| esk45_0
| ~ esk52_0
| esk51_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_300) ).
fof(f301,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk44_0
| esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk43_0
| esk42_0
| ~ p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_301) ).
fof(f302,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| p(X2)
| p(X3)
| ~ esk54_7(X1,X4,X5,X2,X6,X3,X0)
| ~ p(X4)
| p(X6)
| p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_302) ).
fof(f303,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk8_0
| ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_303) ).
fof(f304,axiom,
( esk48_0
| ~ esk41_0
| esk39_0
| ~ esk40_0
| ~ esk49_0
| ~ esk50_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_304) ).
fof(f305,axiom,
( ~ esk44_0
| ~ esk47_0
| ~ esk46_0
| esk45_0
| esk42_0
| ~ esk43_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_305) ).
fof(f306,axiom,
( ~ esk39_0
| ~ esk50_0
| ~ esk48_0
| esk49_0
| ~ esk41_0
| esk40_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_306) ).
fof(f307,axiom,
( ~ esk33_0
| esk46_0
| esk35_0
| esk47_0
| ~ esk45_0
| esk34_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_307) ).
fof(f308,axiom,
( ~ esk46_0
| esk33_0
| esk35_0
| esk47_0
| ~ esk34_0
| esk45_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_308) ).
fof(f309,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk59_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk63_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| esk30_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_309) ).
fof(f310,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X4)
| p(X5)
| esk54_7(X0,X6,X5,X4,X2,X3,X1)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_310) ).
fof(f311,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X4)
| p(X5)
| ~ p(X6)
| esk54_7(X4,X3,X0,X6,X5,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_311) ).
fof(f312,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk6_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_312) ).
fof(f313,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ esk55_7(X1,X0,X2,X3,X4,X5,X6)
| esk35_0
| esk34_0
| ~ esk33_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_313) ).
fof(f314,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk50_0
| p(X0)
| esk48_0
| ~ esk60_7(X1,X2,X3,X4,X0,X5,X6)
| esk49_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_314) ).
fof(f315,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk53_0
| esk51_0
| ~ esk52_0
| ~ p(X0)
| esk61_7(X1,X2,X0,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_315) ).
fof(f316,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ esk54_7(X1,X2,X0,X3,X4,X5,X6)
| p(X2)
| p(X3)
| ~ p(X6)
| ~ p(X1)
| p(X5)
| ~ p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_316) ).
fof(f317,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| p(X2)
| ~ p(X3)
| p(X4)
| ~ p(X5)
| ~ esk54_7(X5,X6,X0,X1,X4,X2,X3)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_317) ).
fof(f318,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk56_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X1)
| ~ esk36_0
| esk38_0
| esk37_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_318) ).
fof(f319,axiom,
( esk33_0
| esk49_0
| esk48_0
| esk35_0
| esk50_0
| esk34_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_319) ).
fof(f320,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| p(X2)
| esk54_7(X3,X1,X0,X4,X2,X5,X6)
| ~ p(X6)
| p(X3)
| p(X4)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_320) ).
fof(f321,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk38_0
| esk56_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk37_0
| ~ esk36_0
| ~ p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_321) ).
fof(f322,axiom,
( esk39_0
| esk44_0
| esk43_0
| esk42_0
| esk40_0
| esk41_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_322) ).
fof(f323,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| p(X5)
| esk54_7(X3,X2,X4,X0,X1,X6,X5)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_323) ).
fof(f324,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| esk12_0
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk57_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_324) ).
fof(f325,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| p(X2)
| p(X3)
| p(X4)
| p(X5)
| ~ p(X6)
| ~ esk54_7(X4,X1,X0,X5,X6,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_325) ).
fof(f326,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| p(X2)
| ~ esk54_7(X3,X4,X1,X2,X5,X6,X0)
| p(X3)
| ~ p(X4)
| ~ p(X5)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_326) ).
fof(f327,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| esk39_0
| ~ esk40_0
| esk41_0
| ~ esk57_7(X1,X2,X0,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_327) ).
fof(f328,axiom,
( ~ esk41_0
| esk36_0
| ~ esk38_0
| ~ esk37_0
| ~ esk40_0
| esk39_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_328) ).
fof(f329,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk34_0
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk33_0
| esk35_0
| ~ p(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_329) ).
fof(f330,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk1_0
| esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk56_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_330) ).
fof(f331,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk50_0
| esk48_0
| esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X2)
| ~ esk49_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_331) ).
fof(f332,axiom,
( ~ esk45_0
| ~ esk47_0
| esk43_0
| ~ esk42_0
| esk46_0
| ~ esk44_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_332) ).
fof(f333,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| esk49_0
| ~ esk50_0
| ~ esk48_0
| ~ esk60_7(X1,X2,X3,X4,X5,X0,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_333) ).
fof(f334,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X4)
| esk54_7(X5,X3,X1,X0,X6,X4,X2)
| ~ p(X6)
| p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_334) ).
fof(f335,axiom,
( ~ esk46_0
| esk41_0
| ~ esk39_0
| ~ esk45_0
| ~ esk40_0
| esk47_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_335) ).
fof(f336,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk16_0
| ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk55_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_336) ).
fof(f337,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk63_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk54_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_337) ).
fof(f338,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk5_0
| esk56_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| esk58_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_338) ).
fof(f339,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| p(X2)
| ~ esk54_7(X3,X1,X0,X4,X2,X5,X6)
| p(X5)
| p(X3)
| p(X6)
| ~ p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_339) ).
fof(f340,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ esk59_7(X1,X2,X0,X3,X4,X5,X6)
| esk47_0
| ~ esk46_0
| esk45_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_340) ).
fof(f341,axiom,
( esk43_0
| esk42_0
| esk51_0
| ~ esk53_0
| esk52_0
| ~ esk44_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_341) ).
fof(f342,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk54_7(X0,X1,X2,X3,X4,X5,X6)
| p(X4)
| ~ p(X6)
| p(X5)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_342) ).
fof(f343,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X1)
| esk52_0
| esk53_0
| ~ esk51_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_343) ).
fof(f344,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk52_0
| esk51_0
| p(X6)
| ~ esk53_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_344) ).
fof(f345,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ esk54_7(X3,X1,X2,X4,X0,X5,X6)
| p(X4)
| p(X6)
| ~ p(X5)
| p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_345) ).
fof(f346,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| ~ esk54_7(X3,X4,X5,X0,X6,X1,X2)
| p(X4)
| p(X6)
| ~ p(X3)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_346) ).
fof(f347,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk18_0
| esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk61_7(X0,X1,X2,X3,X4,X5,X6)
| esk59_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_347) ).
fof(f348,axiom,
( esk33_0
| ~ esk35_0
| esk34_0
| esk49_0
| esk48_0
| ~ esk50_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_348) ).
fof(f349,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk56_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk13_0
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_349) ).
fof(f350,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| p(X3)
| ~ p(X4)
| p(X5)
| esk54_7(X1,X4,X3,X0,X6,X5,X2)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_350) ).
fof(f351,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| ~ p(X2)
| p(X3)
| esk54_7(X4,X5,X6,X0,X3,X1,X2)
| ~ p(X4)
| p(X5)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_351) ).
fof(f352,axiom,
( ~ esk48_0
| esk52_0
| esk50_0
| ~ esk51_0
| esk53_0
| esk49_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_352) ).
fof(f353,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk28_0
| ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk60_7(X0,X1,X2,X3,X4,X5,X6)
| esk63_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk61_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_353) ).
fof(f354,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| esk36_0
| esk38_0
| ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk37_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_354) ).
fof(f355,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| esk33_0
| esk34_0
| p(X0)
| esk35_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_355) ).
fof(f356,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| ~ p(X3)
| esk54_7(X4,X5,X3,X0,X2,X6,X1)
| ~ p(X5)
| ~ p(X6)
| ~ p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_356) ).
fof(f357,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| p(X2)
| ~ p(X3)
| p(X4)
| ~ p(X5)
| p(X6)
| ~ esk54_7(X6,X0,X5,X4,X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_357) ).
fof(f358,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| p(X2)
| ~ p(X3)
| ~ p(X4)
| ~ esk54_7(X2,X5,X6,X4,X1,X3,X0)
| p(X5)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_358) ).
fof(f359,axiom,
( esk46_0
| ~ esk53_0
| esk52_0
| ~ esk47_0
| esk45_0
| esk51_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_359) ).
fof(f360,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk37_0
| esk38_0
| ~ esk36_0
| ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_360) ).
fof(f361,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ esk54_7(X1,X2,X0,X3,X4,X5,X6)
| p(X1)
| p(X6)
| p(X5)
| p(X3)
| ~ p(X4)
| ~ p(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_361) ).
fof(f362,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk56_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk2_0
| esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk55_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_362) ).
fof(f363,axiom,
( esk35_0
| esk47_0
| ~ esk46_0
| ~ esk34_0
| ~ esk45_0
| ~ esk33_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_363) ).
fof(f364,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk46_0
| esk45_0
| ~ p(X0)
| esk59_7(X1,X2,X3,X4,X5,X6,X0)
| ~ esk47_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_364) ).
fof(f365,axiom,
( ~ esk35_0
| ~ esk34_0
| ~ esk38_0
| ~ esk37_0
| esk36_0
| esk33_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_365) ).
fof(f366,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk63_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk26_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_366) ).
fof(f367,axiom,
( ~ esk37_0
| esk47_0
| ~ esk46_0
| ~ esk45_0
| ~ esk36_0
| esk38_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_367) ).
fof(f368,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| p(X2)
| ~ p(X3)
| ~ esk54_7(X4,X5,X1,X2,X3,X6,X0)
| p(X5)
| p(X6)
| p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_368) ).
fof(f369,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk38_0
| p(X0)
| esk36_0
| ~ esk56_7(X1,X2,X0,X3,X4,X5,X6)
| ~ esk37_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_369) ).
fof(f370,axiom,
( esk46_0
| esk39_0
| esk45_0
| esk47_0
| esk40_0
| esk41_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_370) ).
fof(f371,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk42_0
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk43_0
| p(X0)
| esk44_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_371) ).
fof(f372,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ esk34_0
| esk33_0
| esk35_0
| ~ esk55_7(X1,X2,X0,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_372) ).
fof(f373,axiom,
( esk47_0
| esk45_0
| ~ esk49_0
| esk48_0
| ~ esk46_0
| esk50_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_373) ).
fof(f374,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk4_0
| ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk57_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_374) ).
fof(f375,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| esk47_0
| ~ esk45_0
| ~ esk59_7(X1,X2,X3,X0,X4,X5,X6)
| ~ esk46_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_375) ).
fof(f376,axiom,
( esk52_0
| esk43_0
| esk53_0
| ~ esk51_0
| ~ esk42_0
| esk44_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_376) ).
fof(f377,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ p(X2)
| p(X3)
| ~ esk54_7(X4,X0,X2,X3,X5,X1,X6)
| p(X6)
| p(X4)
| p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_377) ).
fof(f378,axiom,
( esk40_0
| ~ esk53_0
| esk39_0
| esk52_0
| ~ esk41_0
| esk51_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_378) ).
fof(f379,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk41_0
| ~ esk40_0
| p(X0)
| ~ esk39_0
| ~ esk57_7(X1,X2,X3,X0,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_379) ).
fof(f380,axiom,
( ~ esk36_0
| esk38_0
| ~ esk48_0
| esk50_0
| esk49_0
| esk37_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_380) ).
fof(f381,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X0)
| esk43_0
| esk42_0
| esk44_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_381) ).
fof(f382,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| esk54_7(X2,X3,X0,X4,X1,X5,X6)
| ~ p(X6)
| ~ p(X3)
| p(X4)
| p(X2)
| p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_382) ).
fof(f383,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk10_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_383) ).
fof(f384,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| esk54_7(X5,X4,X6,X2,X0,X3,X1)
| p(X5)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_384) ).
fof(f385,axiom,
( esk45_0
| esk46_0
| ~ esk47_0
| ~ esk50_0
| esk49_0
| esk48_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_385) ).
fof(f386,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| esk41_0
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk40_0
| esk39_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_386) ).
fof(f387,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| esk54_7(X2,X3,X0,X4,X1,X5,X6)
| p(X5)
| ~ p(X6)
| p(X3)
| ~ p(X4)
| ~ p(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_387) ).
fof(f388,axiom,
( esk39_0
| ~ esk34_0
| esk33_0
| esk41_0
| ~ esk40_0
| esk35_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_388) ).
fof(f389,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| esk1_0
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk56_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_389) ).
fof(f390,axiom,
( ~ esk50_0
| esk43_0
| ~ esk48_0
| ~ esk44_0
| ~ esk42_0
| esk49_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_390) ).
fof(f391,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk27_0
| ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk59_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_391) ).
fof(f392,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ esk54_7(X1,X2,X3,X4,X5,X6,X0)
| p(X1)
| p(X2)
| p(X3)
| p(X4)
| p(X6)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_392) ).
fof(f393,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk53_0
| esk51_0
| esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X6)
| ~ esk52_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_393) ).
fof(f394,axiom,
( ~ esk41_0
| ~ esk39_0
| ~ esk40_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_394) ).
fof(f395,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| p(X2)
| p(X3)
| ~ p(X4)
| ~ esk54_7(X4,X3,X1,X5,X0,X6,X2)
| p(X5)
| p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_395) ).
fof(f396,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk52_0
| ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk51_0
| esk53_0
| p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_396) ).
fof(f397,axiom,
( ~ esk51_0
| ~ esk53_0
| esk46_0
| ~ esk45_0
| esk52_0
| ~ esk47_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_397) ).
fof(f398,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk23_0
| esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk63_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_398) ).
fof(f399,axiom,
( esk48_0
| esk49_0
| esk44_0
| esk42_0
| esk50_0
| esk43_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_399) ).
fof(f400,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk53_0
| ~ esk51_0
| esk61_7(X0,X1,X2,X3,X4,X5,X6)
| esk52_0
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_400) ).
fof(f401,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| esk54_7(X1,X2,X3,X4,X5,X0,X6)
| p(X6)
| ~ p(X1)
| ~ p(X5)
| p(X3)
| ~ p(X2)
| ~ p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_401) ).
fof(f402,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| p(X3)
| ~ esk54_7(X4,X0,X5,X2,X1,X6,X3)
| p(X4)
| ~ p(X6)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_402) ).
fof(f403,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| esk54_7(X1,X2,X3,X4,X0,X5,X6)
| p(X6)
| ~ p(X2)
| ~ p(X1)
| ~ p(X5)
| p(X4)
| ~ p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_403) ).
fof(f404,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk25_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_404) ).
fof(f405,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk37_0
| p(X1)
| ~ esk36_0
| esk38_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_405) ).
fof(f406,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk57_7(X0,X1,X2,X3,X4,X5,X6)
| esk40_0
| ~ esk41_0
| ~ p(X5)
| ~ esk39_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_406) ).
fof(f407,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk10_0
| esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| esk57_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_407) ).
fof(f408,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk38_0
| esk36_0
| esk37_0
| esk56_7(X0,X1,X2,X3,X4,X5,X6)
| ~ p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_408) ).
fof(f409,axiom,
( ~ esk35_0
| esk34_0
| ~ esk48_0
| ~ esk50_0
| esk49_0
| ~ esk33_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_409) ).
fof(f410,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk32_0
| ~ esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_410) ).
fof(f411,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ p(X2)
| ~ p(X3)
| p(X4)
| p(X5)
| esk54_7(X2,X1,X4,X0,X5,X6,X3)
| ~ p(X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_411) ).
fof(f412,axiom,
( esk37_0
| esk45_0
| ~ esk47_0
| ~ esk38_0
| esk46_0
| esk36_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_412) ).
fof(f413,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk54_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_413) ).
fof(f414,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk42_0
| esk43_0
| p(X0)
| esk44_0
| ~ esk58_7(X1,X0,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_414) ).
fof(f415,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| p(X2)
| ~ esk54_7(X3,X4,X5,X0,X6,X1,X2)
| p(X4)
| ~ p(X5)
| p(X6)
| ~ p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_415) ).
fof(f416,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk42_0
| p(X0)
| ~ esk44_0
| ~ esk58_7(X1,X2,X3,X4,X5,X6,X0)
| ~ esk43_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_416) ).
fof(f417,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk46_0
| esk45_0
| esk47_0
| ~ p(X0)
| esk59_7(X1,X2,X0,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_417) ).
fof(f418,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk17_0
| esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk60_7(X0,X1,X2,X3,X4,X5,X6)
| esk62_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_418) ).
fof(f419,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk15_0
| esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk55_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk58_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk57_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_419) ).
fof(f420,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk56_7(X0,X1,X2,X3,X4,X5,X6)
| esk37_0
| esk36_0
| ~ p(X0)
| esk38_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_420) ).
fof(f421,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk54_7(X0,X1,X2,X3,X4,X5,X6)
| p(X2)
| p(X6)
| ~ p(X0)
| ~ p(X5)
| ~ p(X4)
| p(X1)
| ~ p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_421) ).
fof(f422,axiom,
( esk47_0
| ~ esk45_0
| ~ esk51_0
| esk53_0
| esk52_0
| esk46_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_422) ).
fof(f423,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk35_0
| ~ p(X0)
| esk33_0
| esk55_7(X1,X2,X3,X4,X5,X6,X0)
| ~ esk34_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_423) ).
fof(f424,axiom,
( esk52_0
| ~ esk41_0
| ~ esk53_0
| esk40_0
| ~ esk51_0
| ~ esk39_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_424) ).
fof(f425,axiom,
( ~ esk49_0
| esk50_0
| ~ esk48_0
| ~ esk52_0
| ~ esk51_0
| esk53_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_425) ).
fof(f426,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk23_0
| ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk61_7(X0,X1,X2,X3,X4,X5,X6)
| esk63_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_426) ).
fof(f427,axiom,
( ~ esk34_0
| ~ esk43_0
| ~ esk44_0
| esk33_0
| ~ esk35_0
| esk42_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_427) ).
fof(f428,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| esk54_7(X1,X0,X2,X3,X4,X5,X6)
| ~ p(X6)
| p(X4)
| p(X3)
| ~ p(X5)
| p(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_428) ).
fof(f429,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk54_7(X0,X1,X2,X3,X4,X5,X6)
| p(X1)
| ~ p(X4)
| ~ p(X0)
| p(X3)
| p(X6)
| ~ p(X2)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_429) ).
fof(f430,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| p(X2)
| p(X3)
| p(X4)
| ~ p(X5)
| p(X6)
| ~ esk54_7(X0,X6,X3,X1,X2,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_430) ).
fof(f431,axiom,
( esk49_0
| esk41_0
| esk50_0
| ~ esk39_0
| esk40_0
| ~ esk48_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_431) ).
fof(f432,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk19_0
| esk61_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk60_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_432) ).
fof(f433,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk34_0
| p(X0)
| esk33_0
| ~ esk55_7(X1,X2,X3,X4,X5,X6,X0)
| ~ esk35_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_433) ).
fof(f434,axiom,
( esk36_0
| esk42_0
| esk44_0
| ~ esk43_0
| esk38_0
| ~ esk37_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_434) ).
fof(f435,axiom,
( esk36_0
| ~ esk35_0
| ~ esk38_0
| esk33_0
| esk34_0
| esk37_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_435) ).
fof(f436,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| ~ p(X1)
| ~ p(X2)
| p(X3)
| esk54_7(X4,X1,X5,X2,X6,X3,X0)
| ~ p(X6)
| ~ p(X5)
| p(X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_436) ).
fof(f437,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| ~ p(X1)
| ~ esk54_7(X1,X2,X0,X3,X4,X5,X6)
| p(X5)
| p(X4)
| p(X6)
| p(X3)
| p(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_437) ).
fof(f438,axiom,
( ~ esk33_0
| ~ esk42_0
| esk35_0
| ~ esk34_0
| ~ esk43_0
| esk44_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_438) ).
fof(f439,axiom,
( ~ esk53_0
| ~ esk52_0
| esk51_0
| ~ esk49_0
| ~ esk50_0
| esk48_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_439) ).
fof(f440,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| esk54_7(X1,X2,X3,X4,X0,X5,X6)
| ~ p(X6)
| ~ p(X4)
| p(X2)
| ~ p(X5)
| p(X1)
| ~ p(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_440) ).
fof(f441,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( p(X0)
| p(X1)
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| esk54_7(X3,X5,X4,X0,X2,X1,X6)
| ~ p(X6)
| ~ p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_441) ).
fof(f442,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(X0)
| p(X1)
| p(X2)
| p(X3)
| p(X4)
| ~ esk54_7(X5,X6,X4,X1,X3,X2,X0)
| p(X6)
| p(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_442) ).
fof(f443,axiom,
( esk47_0
| esk42_0
| ~ esk43_0
| esk44_0
| ~ esk46_0
| esk45_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_443) ).
fof(f444,axiom,
( esk40_0
| ~ esk39_0
| esk37_0
| esk38_0
| esk41_0
| ~ esk36_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_444) ).
fof(f445,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ esk60_7(X0,X1,X2,X3,X4,X5,X6)
| esk22_0
| ~ esk62_7(X0,X1,X2,X3,X4,X5,X6)
| ~ esk63_7(X0,X1,X2,X3,X4,X5,X6)
| esk59_7(X0,X1,X2,X3,X4,X5,X6)
| esk61_7(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_445) ).
fof(f446,axiom,
( ~ esk36_0
| ~ esk37_0
| ~ esk33_0
| esk38_0
| esk35_0
| ~ esk34_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_446) ).
fof(f447,axiom,
p(true),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_true) ).
fof(f448,axiom,
~ p(false),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_false) ).
fof(f449,axiom,
true != false,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',true_not_false) ).
fof(f453,plain,
$false,
inference(finite_model_not_found_(exhaustively_excluded_all_possible_domain_size_assignments),[],[f1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13,f14,f15,f16,f17,f18,f19,f20,f21,f22,f23,f24,f25,f26,f27,f28,f29,f30,f31,f32,f33,f34,f35,f36,f37,f38,f39,f40,f41,f42,f43,f44,f45,f46,f47,f48,f49,f50,f51,f52,f53,f54,f55,f56,f57,f58,f59,f60,f61,f62,f63,f64,f65,f66,f67,f68,f69,f70,f71,f72,f73,f74,f75,f76,f77,f78,f79,f80,f81,f82,f83,f84,f85,f86,f87,f88,f89,f90,f91,f92,f93,f94,f95,f96,f97,f98,f99,f100,f101,f102,f103,f104,f105,f106,f107,f108,f109,f110,f111,f112,f113,f114,f115,f116,f117,f118,f119,f120,f121,f122,f123,f124,f125,f126,f127,f128,f129,f130,f131,f132,f133,f134,f135,f136,f137,f138,f139,f140,f141,f142,f143,f144,f145,f146,f147,f148,f149,f150,f151,f152,f153,f154,f155,f156,f157,f158,f159,f160,f161,f162,f163,f164,f165,f166,f167,f168,f169,f170,f171,f172,f173,f174,f175,f176,f177,f178,f179,f180,f181,f182,f183,f184,f185,f186,f187,f188,f189,f190,f191,f192,f193,f194,f195,f196,f197,f198,f199,f200,f201,f202,f203,f204,f205,f206,f207,f208,f209,f210,f211,f212,f213,f214,f215,f216,f217,f218,f219,f220,f221,f222,f223,f224,f225,f226,f227,f228,f229,f230,f231,f232,f233,f234,f235,f236,f237,f238,f239,f240,f241,f242,f243,f244,f245,f246,f247,f248,f249,f250,f251,f252,f253,f254,f255,f256,f257,f258,f259,f260,f261,f262,f263,f264,f265,f266,f267,f268,f269,f270,f271,f272,f273,f274,f275,f276,f277,f278,f279,f280,f281,f282,f283,f284,f285,f286,f287,f288,f289,f290,f291,f292,f293,f294,f295,f296,f297,f298,f299,f300,f301,f302,f303,f304,f305,f306,f307,f308,f309,f310,f311,f312,f313,f314,f315,f316,f317,f318,f319,f320,f321,f322,f323,f324,f325,f326,f327,f328,f329,f330,f331,f332,f333,f334,f335,f336,f337,f338,f339,f340,f341,f342,f343,f344,f345,f346,f347,f348,f349,f350,f351,f352,f353,f354,f355,f356,f357,f358,f359,f360,f361,f362,f363,f364,f365,f366,f367,f368,f369,f370,f371,f372,f373,f374,f375,f376,f377,f378,f379,f380,f381,f382,f383,f384,f385,f386,f387,f388,f389,f390,f391,f392,f393,f394,f395,f396,f397,f398,f399,f400,f401,f402,f403,f404,f405,f406,f407,f408,f409,f410,f411,f412,f413,f414,f415,f416,f417,f418,f419,f420,f421,f422,f423,f424,f425,f426,f427,f428,f429,f430,f431,f432,f433,f434,f435,f436,f437,f438,f439,f440,f441,f442,f443,f444,f445,f446,f447,f448,f449]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : HWV078-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.17/0.44 % Computer : n003.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sun Sep 27 11:23:55 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.24/0.49 Running first-order model finding
% 0.24/0.49 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
% 7.60/1.88 % (361448)Will run a generic schedule for satisfiability detection.
% 7.60/1.88 % (361458)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3361568801:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.60/1.88 % (361455)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1657371447:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.60/1.88 % (361454)% WARNING: option uhcvi not known.
% 7.60/1.88 % (361459)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1227849252:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.60/1.88 % (361453)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2878084600_2999 on theBenchmark for (2999ds/0Mi)
% 7.60/1.88 % (361456)dis+10_1_sil=32000:sp=arity:random_seed=3246339107:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.60/1.88 % (361457)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3165847712:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.60/1.88 % (361454)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2771227770:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.60/1.88 % (361458)Instruction limit reached!
% 7.60/1.88 % (361458)------------------------------
% 7.60/1.88 % (361458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.60/1.88 % (361458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.88 % (361458)CaDiCaL version: 2.1.3
% 7.60/1.88 % (361458)Termination reason: Instruction limit
% 7.60/1.88 % (361458)Termination phase: Saturation
% 7.60/1.88 % (361458)Time elapsed: 0.054 s
% 7.60/1.88 % (361458)Peak memory usage: 12 MB
% 7.60/1.88 % (361458)Instructions burned: 133 (million)
% 7.60/1.88 % (361468)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2124307381:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.60/1.88 % Detected minimum model sizes of [1]
% 7.60/1.88 % Detected maximum model sizes of [2]
% 7.60/1.88 % TRYING [1]
% 7.60/1.88 % TRYING [2]
% 7.60/1.88 % (361457)Instruction limit reached!
% 7.60/1.88 % (361457)------------------------------
% 7.60/1.88 % (361457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.60/1.88 % (361457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.88 % (361457)CaDiCaL version: 2.1.3
% 7.60/1.88 % (361457)Termination reason: Instruction limit
% 7.60/1.88 % (361457)Termination phase: Blocked clause elimination
% 7.60/1.88 % (361457)Time elapsed: 0.086 s
% 7.60/1.88 % (361457)Peak memory usage: 10 MB
% 7.60/1.88 % (361457)Instructions burned: 117 (million)
% 7.60/1.88 % (361456)Instruction limit reached!
% 7.60/1.88 % (361456)------------------------------
% 7.60/1.88 % (361456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.60/1.88 % (361456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.88 % (361456)CaDiCaL version: 2.1.3
% 7.60/1.88 % (361456)Termination reason: Instruction limit
% 7.60/1.88 % (361456)Termination phase: Saturation
% 7.60/1.88 % (361456)Time elapsed: 0.086 s
% 7.60/1.88 % (361456)Peak memory usage: 12 MB
% 7.60/1.88 % (361456)Instructions burned: 103 (million)
% 7.60/1.88 % (361470)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2740387087:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.60/1.88 % (361471)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=161405881:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.60/1.88 % (361459)Instruction limit reached!
% 7.60/1.88 % (361459)------------------------------
% 7.60/1.88 % (361459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.60/1.88 % (361459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.88 % (361459)CaDiCaL version: 2.1.3
% 7.60/1.88 % (361459)Termination reason: Instruction limit
% 7.60/1.88 % (361459)Termination phase: Saturation
% 7.60/1.88 % (361459)Time elapsed: 0.126 s
% 7.60/1.88 % (361459)Peak memory usage: 12 MB
% 7.60/1.88 % (361459)Instructions burned: 159 (million)
% 7.60/1.88 % Detected minimum model sizes of [1]
% 7.60/1.88 % Detected maximum model sizes of [2]
% 7.60/1.88 % TRYING [1]
% 7.60/1.88 % TRYING [2]
% 7.60/1.88 % (361474)ott-21_1_sil=16000:fs=off:random_seed=2727947988:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.60/1.88 % (361470)Instruction limit reached!
% 7.60/1.88 % (361470)------------------------------
% 7.60/1.88 % (361470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.43/2.62 % (361470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.62 % (361470)CaDiCaL version: 2.1.3
% 14.43/2.62 % (361470)Termination reason: Instruction limit
% 14.43/2.62 % (361470)Termination phase: Blocked clause elimination
% 14.43/2.62 % (361470)Time elapsed: 0.069 s
% 14.43/2.62 % (361470)Peak memory usage: 10 MB
% 14.43/2.62 % (361470)Instructions burned: 131 (million)
% 14.43/2.62 % (361476)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1744766375:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 14.43/2.62 % (361474)Instruction limit reached!
% 14.43/2.62 % (361474)------------------------------
% 14.43/2.62 % (361474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.43/2.62 % (361474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.62 % (361474)CaDiCaL version: 2.1.3
% 14.43/2.62 % (361474)Termination reason: Instruction limit
% 14.43/2.62 % (361474)Termination phase: Saturation
% 14.43/2.62 % (361474)Time elapsed: 0.153 s
% 14.43/2.62 % (361474)Peak memory usage: 11 MB
% 14.43/2.62 % (361474)Instructions burned: 181 (million)
% 14.43/2.62 % (361478)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4105704511:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 14.43/2.62 % (361468)Instruction limit reached!
% 14.43/2.62 % (361468)------------------------------
% 14.43/2.62 % (361468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.43/2.62 % (361468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.62 % (361468)CaDiCaL version: 2.1.3
% 14.43/2.62 % (361468)Termination reason: Instruction limit
% 14.43/2.62 % (361468)Termination phase: Finite model building SAT solving
% 14.43/2.62 % (361468)Time elapsed: 0.299 s
% 14.43/2.62 % (361468)Peak memory usage: 17 MB
% 14.43/2.62 % (361468)Instructions burned: 716 (million)
% 14.43/2.62 % Detected minimum model sizes of [1]
% 14.43/2.62 % Detected maximum model sizes of [2]
% 14.43/2.62 % TRYING [1]
% 14.43/2.62 % TRYING [2]
% 14.43/2.62 % (361480)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2656256487:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 14.43/2.62 % (361476)Instruction limit reached!
% 14.43/2.62 % (361476)------------------------------
% 14.43/2.62 % (361476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.43/2.62 % (361476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.62 % (361476)CaDiCaL version: 2.1.3
% 14.43/2.62 % (361476)Termination reason: Instruction limit
% 14.43/2.62 % (361476)Termination phase: Saturation
% 14.43/2.62 % (361476)Time elapsed: 0.357 s
% 14.43/2.62 % (361476)Peak memory usage: 12 MB
% 14.43/2.62 % (361476)Instructions burned: 477 (million)
% 14.43/2.62 % (361482)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2163484431:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 14.43/2.62 % Detected minimum model sizes of [1]
% 14.43/2.62 % Detected maximum model sizes of [2]
% 14.43/2.62 % fmb_start_size (= 14) larger than a detected sort maximum size!
% 14.43/2.62 % (361482)Refutation not found, incomplete strategy
% 14.43/2.62 % (361482)------------------------------
% 14.43/2.62 % (361482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.43/2.62 % (361482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.62 % (361482)CaDiCaL version: 2.1.3
% 14.43/2.62 % (361482)Termination reason: Refutation not found, incomplete strategy
% 14.43/2.63 % (361482)Time elapsed: 0.032 s
% 14.43/2.63 % (361482)Peak memory usage: 11 MB
% 14.43/2.63 % (361482)Instructions burned: 36 (million)
% 14.43/2.63 % (361482)------------------------------
% 14.43/2.63 % (361482)------------------------------
% 14.43/2.63 % (361484)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=3563792619:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 14.43/2.63 % (361471)Instruction limit reached!
% 14.43/2.63 % (361471)------------------------------
% 14.43/2.63 % (361471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.43/2.63 % (361471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.63 % (361471)CaDiCaL version: 2.1.3
% 14.43/2.63 % (361471)Termination reason: Instruction limit
% 14.43/2.63 % (361471)Termination phase: Saturation
% 14.43/2.63 % (361471)Time elapsed: 0.614 s
% 14.43/2.63 % (361471)Peak memory usage: 15 MB
% 14.43/2.63 % (361471)Instructions burned: 684 (million)
% 14.43/2.63 % (361486)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1686942976:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 14.43/2.63 % (361480)Instruction limit reached!
% 14.43/2.63 % (361480)------------------------------
% 14.43/2.63 % (361480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.43/2.63 % (361480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.63 % (361480)CaDiCaL version: 2.1.3
% 14.43/2.63 % (361480)Termination reason: Instruction limit
% 14.43/2.63 % (361480)Termination phase: Saturation
% 14.43/2.63 % (361480)Time elapsed: 0.495 s
% 14.43/2.63 % (361480)Peak memory usage: 15 MB
% 14.43/2.63 % (361480)Instructions burned: 1180 (million)
% 14.43/2.63 % (361488)fmb+10_1_sil=64000:random_seed=1708225599:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 14.43/2.63 % Detected minimum model sizes of [1]
% 14.43/2.63 % Detected maximum model sizes of [2]
% 14.43/2.63 % TRYING [1]
% 14.43/2.63 % TRYING [2]
% 14.43/2.63 % (361478)Instruction limit reached!
% 14.43/2.63 % (361478)------------------------------
% 14.43/2.63 % (361478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.43/2.63 % (361478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.63 % (361478)CaDiCaL version: 2.1.3
% 14.43/2.63 % (361478)Termination reason: Instruction limit
% 14.43/2.63 % (361478)Termination phase: Finite model building SAT solving
% 14.43/2.63 % (361478)Time elapsed: 0.623 s
% 14.43/2.63 % (361478)Peak memory usage: 15 MB
% 14.43/2.63 % (361478)Instructions burned: 870 (million)
% 14.43/2.63 % (361490)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=159408933:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 14.43/2.63 % Detected minimum model sizes of [1]
% 14.43/2.63 % Detected maximum model sizes of [2]
% 14.43/2.63 % fmb_start_size (= 20) larger than a detected sort maximum size!
% 14.43/2.63 % (361490)Refutation not found, incomplete strategy
% 14.43/2.63 % (361490)------------------------------
% 14.43/2.63 % (361490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.43/2.63 % (361490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.63 % (361490)CaDiCaL version: 2.1.3
% 14.43/2.63 % (361490)Termination reason: Refutation not found, incomplete strategy
% 14.43/2.63 % (361490)Time elapsed: 0.028 s
% 14.43/2.63 % (361490)Peak memory usage: 11 MB
% 14.43/2.63 % (361490)Instructions burned: 33 (million)
% 14.43/2.63 % (361490)------------------------------
% 14.43/2.63 % (361490)------------------------------
% 14.43/2.63 % (361493)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2095331323:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 14.43/2.63 % Detected minimum model sizes of [1]
% 14.43/2.63 % Detected maximum model sizes of [2]
% 14.43/2.63 % fmb_start_size (= 8) larger than a detected sort maximum size!
% 14.43/2.63 % (361493)Refutation not found, incomplete strategy
% 14.43/2.63 % (361493)------------------------------
% 14.43/2.63 % (361493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.43/2.63 % (361493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.63 % (361493)CaDiCaL version: 2.1.3
% 14.43/2.63 % (361493)Termination reason: Refutation not found, incomplete strategy
% 14.43/2.63 % (361493)Time elapsed: 0.017 s
% 14.43/2.63 % (361493)Peak memory usage: 11 MB
% 14.43/2.63 % (361493)Instructions burned: 33 (million)
% 14.43/2.63 % (361493)------------------------------
% 14.43/2.63 % (361493)------------------------------
% 14.43/2.63 % (361495)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1692685865:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 14.43/2.63 % (361484)Instruction limit reached!
% 14.43/2.63 % (361484)------------------------------
% 14.43/2.63 % (361484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.43/2.63 % (361484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.63 % (361484)CaDiCaL version: 2.1.3
% 14.43/2.63 % (361484)Termination reason: Instruction limit
% 14.43/2.63 % (361484)Termination phase: Saturation
% 14.43/2.63 % (361484)Time elapsed: 0.619 s
% 14.43/2.63 % (361484)Peak memory usage: 15 MB
% 14.43/2.63 % (361484)Instructions burned: 692 (million)
% 14.43/2.63 % (361498)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3790009395:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 14.43/2.63 % (361486)Instruction limit reached!
% 14.43/2.63 % (361486)------------------------------
% 14.43/2.63 % (361486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.43/2.63 % (361486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.63 % (361486)CaDiCaL version: 2.1.3
% 14.43/2.63 % (361486)Termination reason: Instruction limit
% 14.43/2.63 % (361486)Termination phase: Saturation
% 14.43/2.63 % (361486)Time elapsed: 0.572 s
% 14.43/2.63 % (361486)Peak memory usage: 20 MB
% 14.43/2.63 % (361486)Instructions burned: 879 (million)
% 14.43/2.63 % (361501)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3706797280:i=6324_2986 on theBenchmark for (2986ds/6324Mi)
% 14.43/2.63 % Detected minimum model sizes of [1]
% 14.43/2.63 % Detected maximum model sizes of [2]
% 14.43/2.63 % fmb_start_size (= 77) larger than a detected sort maximum size!
% 14.43/2.63 % (361501)Refutation not found, incomplete strategy
% 14.43/2.63 % (361501)------------------------------
% 14.43/2.63 % (361501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.43/2.63 % (361501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.63 % (361501)CaDiCaL version: 2.1.3
% 14.43/2.63 % (361501)Termination reason: Refutation not found, incomplete strategy
% 14.43/2.63 % (361501)Time elapsed: 0.128 s
% 14.43/2.63 % (361501)Peak memory usage: 11 MB
% 14.43/2.63 % (361501)Instructions burned: 163 (million)
% 14.43/2.63 % (361501)------------------------------
% 14.43/2.63 % (361501)------------------------------
% 14.43/2.63 % (361504)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1190225773:fmbsr=2.30978:i=2174_2984 on theBenchmark for (2984ds/2174Mi)
% 14.43/2.63 % Detected minimum model sizes of [1]
% 14.43/2.63 % Detected maximum model sizes of [2]
% 14.43/2.63 % fmb_start_size (= 16) larger than a detected sort maximum size!
% 14.43/2.63 % (361504)Refutation not found, incomplete strategy
% 14.43/2.63 % (361504)------------------------------
% 14.43/2.63 % (361504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.43/2.63 % (361504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.63 % (361504)CaDiCaL version: 2.1.3
% 14.43/2.63 % (361504)Termination reason: Refutation not found, incomplete strategy
% 14.43/2.63 % (361504)Time elapsed: 0.029 s
% 14.43/2.63 % (361504)Peak memory usage: 11 MB
% 14.43/2.63 % (361504)Instructions burned: 36 (million)
% 14.43/2.63 % (361504)------------------------------
% 14.43/2.63 % (361504)------------------------------
% 14.43/2.63 % (361508)ott-2_1_sil=16000:newcnf=on:random_seed=1033043443:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2983 on theBenchmark for (2983ds/869Mi)
% 14.43/2.63 % (361488) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-361448-361488"...
% 14.43/2.63 % (361488)...printing done.
% 14.43/2.63 % (361488)Refutation found. Thanks to Tanya!
% 14.43/2.63 % SZS status Unsatisfiable for theBenchmark
% 14.43/2.63 % SZS output start Proof for theBenchmark
% See solution above
% 14.43/2.64 % (361488)------------------------------
% 14.43/2.64 % (361488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.43/2.64 % (361488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.64 % (361488)CaDiCaL version: 2.1.3
% 14.43/2.64 % (361488)Termination reason: Refutation
% 14.43/2.64 % (361488)Time elapsed: 1.168 s
% 14.43/2.64 % (361488)Peak memory usage: 16 MB
% 14.43/2.64 % (361488)Instructions burned: 2728 (million)
% 14.43/2.64 % (361448)Success in time 2.123 s
% 14.43/2.64 % Vampire exiting
%------------------------------------------------------------------------------