%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR161+1 : TPTP v7.3.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sine.py -e eprover -t %d %s
% Computer : n188.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.5MB
% OS : Linux 3.10.0-862.11.6.el7.x86_64
% CPULimit : 300s
% DateTime : Wed Feb 27 12:29:16 EST 2019
% Result : Theorem 123.49s
% Output : CNFRefutation 123.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 5
% Syntax : Number of formulae : 38 ( 11 unt; 0 def)
% Number of atoms : 604 ( 1 equ)
% Maximal formula atoms : 110 ( 15 avg)
% Number of connectives : 852 ( 286 ~; 279 |; 273 &)
% ( 12 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 68 ( 11 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 1 prp; 0-7 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 294 ( 2 sgn 275 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(20,axiom,
p__d__partition3(c__Animal,c__Vertebrate,c__Invertebrate),
file('/export/starexec/sandbox2/tmp/tmpjXLEVe/sel_theBenchmark.p_4',mergeA2934) ).
fof(689,axiom,
( ! [X28,X241,X242] :
( p__d__partition3(X28,X241,X242)
<=> ( p__d__exhaustiveDecomposition3(X28,X241,X242)
& p__d__disjointDecomposition3(X28,X241,X242) ) )
& ! [X28,X241,X242,X243] :
( p__d__partition4(X28,X241,X242,X243)
<=> ( p__d__exhaustiveDecomposition4(X28,X241,X242,X243)
& p__d__disjointDecomposition4(X28,X241,X242,X243) ) )
& ! [X28,X241,X242,X243,X244] :
( p__d__partition5(X28,X241,X242,X243,X244)
<=> ( p__d__exhaustiveDecomposition5(X28,X241,X242,X243,X244)
& p__d__disjointDecomposition5(X28,X241,X242,X243,X244) ) )
& ! [X28,X241,X242,X243,X244,X245] :
( p__d__partition6(X28,X241,X242,X243,X244,X245)
<=> ( p__d__exhaustiveDecomposition6(X28,X241,X242,X243,X244,X245)
& p__d__disjointDecomposition6(X28,X241,X242,X243,X244,X245) ) )
& ! [X28,X241,X242,X243,X244,X245,X246] :
( p__d__partition7(X28,X241,X242,X243,X244,X245,X246)
<=> ( p__d__exhaustiveDecomposition7(X28,X241,X242,X243,X244,X245,X246)
& p__d__disjointDecomposition7(X28,X241,X242,X243,X244,X245,X246) ) ) ),
file('/export/starexec/sandbox2/tmp/tmpjXLEVe/sel_theBenchmark.p_4',predefinitionsA18) ).
fof(690,axiom,
! [X247,X248] :
( p__d__disjoint(X247,X248)
<=> ! [X185] :
( ~ p__d__instance(X185,X247)
| ~ p__d__instance(X185,X248) ) ),
file('/export/starexec/sandbox2/tmp/tmpjXLEVe/sel_theBenchmark.p_4',predefinitionsA15) ).
fof(1032,axiom,
( ! [X28,X241,X242] :
( p__d__disjointDecomposition3(X28,X241,X242)
<=> p__d__disjoint(X241,X242) )
& ! [X28,X241,X242,X243] :
( p__d__disjointDecomposition4(X28,X241,X242,X243)
<=> ( p__d__disjoint(X241,X242)
& p__d__disjoint(X241,X243)
& p__d__disjoint(X242,X243) ) )
& ! [X28,X241,X242,X243,X244] :
( p__d__disjointDecomposition5(X28,X241,X242,X243,X244)
<=> ( p__d__disjoint(X241,X242)
& p__d__disjoint(X241,X243)
& p__d__disjoint(X241,X244)
& p__d__disjoint(X242,X243)
& p__d__disjoint(X242,X244)
& p__d__disjoint(X243,X244) ) )
& ! [X28,X241,X242,X243,X244,X245] :
( p__d__disjointDecomposition6(X28,X241,X242,X243,X244,X245)
<=> ( p__d__disjoint(X241,X242)
& p__d__disjoint(X241,X243)
& p__d__disjoint(X241,X244)
& p__d__disjoint(X241,X245)
& p__d__disjoint(X242,X243)
& p__d__disjoint(X242,X244)
& p__d__disjoint(X242,X245)
& p__d__disjoint(X243,X244)
& p__d__disjoint(X243,X245)
& p__d__disjoint(X244,X245) ) )
& ! [X28,X241,X242,X243,X244,X245,X246] :
( p__d__disjointDecomposition7(X28,X241,X242,X243,X244,X245,X246)
<=> ( p__d__disjoint(X241,X242)
& p__d__disjoint(X241,X243)
& p__d__disjoint(X241,X244)
& p__d__disjoint(X241,X245)
& p__d__disjoint(X241,X246)
& p__d__disjoint(X242,X243)
& p__d__disjoint(X242,X244)
& p__d__disjoint(X242,X245)
& p__d__disjoint(X242,X246)
& p__d__disjoint(X243,X244)
& p__d__disjoint(X243,X245)
& p__d__disjoint(X243,X246)
& p__d__disjoint(X244,X245)
& p__d__disjoint(X244,X246)
& p__d__disjoint(X245,X246) ) ) ),
file('/export/starexec/sandbox2/tmp/tmpjXLEVe/sel_theBenchmark.p_4',predefinitionsA24) ).
fof(1102,conjecture,
! [X18,X19] :
( ( p__d__instance(X19,c__Invertebrate)
& p__d__instance(X18,c__Vertebrate) )
=> ~ equal(X18,X19) ),
file('/export/starexec/sandbox2/tmp/tmpjXLEVe/sel_theBenchmark.p_4',antonymPattern10049) ).
fof(1103,negated_conjecture,
~ ! [X18,X19] :
( ( p__d__instance(X19,c__Invertebrate)
& p__d__instance(X18,c__Vertebrate) )
=> ~ equal(X18,X19) ),
inference(assume_negation,[status(cth)],[1102]) ).
fof(1125,plain,
! [X247,X248] :
( p__d__disjoint(X247,X248)
<=> ! [X185] :
( ~ p__d__instance(X185,X247)
| ~ p__d__instance(X185,X248) ) ),
inference(fof_simplification,[status(thm)],[690,theory(equality)]) ).
cnf(1197,plain,
p__d__partition3(c__Animal,c__Vertebrate,c__Invertebrate),
inference(split_conjunct,[status(thm)],[20]) ).
fof(3046,plain,
( ! [X28,X241,X242] :
( ( ~ p__d__partition3(X28,X241,X242)
| ( p__d__exhaustiveDecomposition3(X28,X241,X242)
& p__d__disjointDecomposition3(X28,X241,X242) ) )
& ( ~ p__d__exhaustiveDecomposition3(X28,X241,X242)
| ~ p__d__disjointDecomposition3(X28,X241,X242)
| p__d__partition3(X28,X241,X242) ) )
& ! [X28,X241,X242,X243] :
( ( ~ p__d__partition4(X28,X241,X242,X243)
| ( p__d__exhaustiveDecomposition4(X28,X241,X242,X243)
& p__d__disjointDecomposition4(X28,X241,X242,X243) ) )
& ( ~ p__d__exhaustiveDecomposition4(X28,X241,X242,X243)
| ~ p__d__disjointDecomposition4(X28,X241,X242,X243)
| p__d__partition4(X28,X241,X242,X243) ) )
& ! [X28,X241,X242,X243,X244] :
( ( ~ p__d__partition5(X28,X241,X242,X243,X244)
| ( p__d__exhaustiveDecomposition5(X28,X241,X242,X243,X244)
& p__d__disjointDecomposition5(X28,X241,X242,X243,X244) ) )
& ( ~ p__d__exhaustiveDecomposition5(X28,X241,X242,X243,X244)
| ~ p__d__disjointDecomposition5(X28,X241,X242,X243,X244)
| p__d__partition5(X28,X241,X242,X243,X244) ) )
& ! [X28,X241,X242,X243,X244,X245] :
( ( ~ p__d__partition6(X28,X241,X242,X243,X244,X245)
| ( p__d__exhaustiveDecomposition6(X28,X241,X242,X243,X244,X245)
& p__d__disjointDecomposition6(X28,X241,X242,X243,X244,X245) ) )
& ( ~ p__d__exhaustiveDecomposition6(X28,X241,X242,X243,X244,X245)
| ~ p__d__disjointDecomposition6(X28,X241,X242,X243,X244,X245)
| p__d__partition6(X28,X241,X242,X243,X244,X245) ) )
& ! [X28,X241,X242,X243,X244,X245,X246] :
( ( ~ p__d__partition7(X28,X241,X242,X243,X244,X245,X246)
| ( p__d__exhaustiveDecomposition7(X28,X241,X242,X243,X244,X245,X246)
& p__d__disjointDecomposition7(X28,X241,X242,X243,X244,X245,X246) ) )
& ( ~ p__d__exhaustiveDecomposition7(X28,X241,X242,X243,X244,X245,X246)
| ~ p__d__disjointDecomposition7(X28,X241,X242,X243,X244,X245,X246)
| p__d__partition7(X28,X241,X242,X243,X244,X245,X246) ) ) ),
inference(fof_nnf,[status(thm)],[689]) ).
fof(3047,plain,
( ! [X247,X248,X249] :
( ( ~ p__d__partition3(X247,X248,X249)
| ( p__d__exhaustiveDecomposition3(X247,X248,X249)
& p__d__disjointDecomposition3(X247,X248,X249) ) )
& ( ~ p__d__exhaustiveDecomposition3(X247,X248,X249)
| ~ p__d__disjointDecomposition3(X247,X248,X249)
| p__d__partition3(X247,X248,X249) ) )
& ! [X250,X251,X252,X253] :
( ( ~ p__d__partition4(X250,X251,X252,X253)
| ( p__d__exhaustiveDecomposition4(X250,X251,X252,X253)
& p__d__disjointDecomposition4(X250,X251,X252,X253) ) )
& ( ~ p__d__exhaustiveDecomposition4(X250,X251,X252,X253)
| ~ p__d__disjointDecomposition4(X250,X251,X252,X253)
| p__d__partition4(X250,X251,X252,X253) ) )
& ! [X254,X255,X256,X257,X258] :
( ( ~ p__d__partition5(X254,X255,X256,X257,X258)
| ( p__d__exhaustiveDecomposition5(X254,X255,X256,X257,X258)
& p__d__disjointDecomposition5(X254,X255,X256,X257,X258) ) )
& ( ~ p__d__exhaustiveDecomposition5(X254,X255,X256,X257,X258)
| ~ p__d__disjointDecomposition5(X254,X255,X256,X257,X258)
| p__d__partition5(X254,X255,X256,X257,X258) ) )
& ! [X259,X260,X261,X262,X263,X264] :
( ( ~ p__d__partition6(X259,X260,X261,X262,X263,X264)
| ( p__d__exhaustiveDecomposition6(X259,X260,X261,X262,X263,X264)
& p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264) ) )
& ( ~ p__d__exhaustiveDecomposition6(X259,X260,X261,X262,X263,X264)
| ~ p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264)
| p__d__partition6(X259,X260,X261,X262,X263,X264) ) )
& ! [X265,X266,X267,X268,X269,X270,X271] :
( ( ~ p__d__partition7(X265,X266,X267,X268,X269,X270,X271)
| ( p__d__exhaustiveDecomposition7(X265,X266,X267,X268,X269,X270,X271)
& p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) ) )
& ( ~ p__d__exhaustiveDecomposition7(X265,X266,X267,X268,X269,X270,X271)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271)
| p__d__partition7(X265,X266,X267,X268,X269,X270,X271) ) ) ),
inference(variable_rename,[status(thm)],[3046]) ).
fof(3048,plain,
! [X247,X248,X249,X250,X251,X252,X253,X254,X255,X256,X257,X258,X259,X260,X261,X262,X263,X264,X265,X266,X267,X268,X269,X270,X271] :
( ( ~ p__d__partition7(X265,X266,X267,X268,X269,X270,X271)
| ( p__d__exhaustiveDecomposition7(X265,X266,X267,X268,X269,X270,X271)
& p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) ) )
& ( ~ p__d__exhaustiveDecomposition7(X265,X266,X267,X268,X269,X270,X271)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271)
| p__d__partition7(X265,X266,X267,X268,X269,X270,X271) )
& ( ~ p__d__partition6(X259,X260,X261,X262,X263,X264)
| ( p__d__exhaustiveDecomposition6(X259,X260,X261,X262,X263,X264)
& p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264) ) )
& ( ~ p__d__exhaustiveDecomposition6(X259,X260,X261,X262,X263,X264)
| ~ p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264)
| p__d__partition6(X259,X260,X261,X262,X263,X264) )
& ( ~ p__d__partition5(X254,X255,X256,X257,X258)
| ( p__d__exhaustiveDecomposition5(X254,X255,X256,X257,X258)
& p__d__disjointDecomposition5(X254,X255,X256,X257,X258) ) )
& ( ~ p__d__exhaustiveDecomposition5(X254,X255,X256,X257,X258)
| ~ p__d__disjointDecomposition5(X254,X255,X256,X257,X258)
| p__d__partition5(X254,X255,X256,X257,X258) )
& ( ~ p__d__partition4(X250,X251,X252,X253)
| ( p__d__exhaustiveDecomposition4(X250,X251,X252,X253)
& p__d__disjointDecomposition4(X250,X251,X252,X253) ) )
& ( ~ p__d__exhaustiveDecomposition4(X250,X251,X252,X253)
| ~ p__d__disjointDecomposition4(X250,X251,X252,X253)
| p__d__partition4(X250,X251,X252,X253) )
& ( ~ p__d__partition3(X247,X248,X249)
| ( p__d__exhaustiveDecomposition3(X247,X248,X249)
& p__d__disjointDecomposition3(X247,X248,X249) ) )
& ( ~ p__d__exhaustiveDecomposition3(X247,X248,X249)
| ~ p__d__disjointDecomposition3(X247,X248,X249)
| p__d__partition3(X247,X248,X249) ) ),
inference(shift_quantors,[status(thm)],[3047]) ).
fof(3049,plain,
! [X247,X248,X249,X250,X251,X252,X253,X254,X255,X256,X257,X258,X259,X260,X261,X262,X263,X264,X265,X266,X267,X268,X269,X270,X271] :
( ( p__d__exhaustiveDecomposition7(X265,X266,X267,X268,X269,X270,X271)
| ~ p__d__partition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271)
| ~ p__d__partition7(X265,X266,X267,X268,X269,X270,X271) )
& ( ~ p__d__exhaustiveDecomposition7(X265,X266,X267,X268,X269,X270,X271)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271)
| p__d__partition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__exhaustiveDecomposition6(X259,X260,X261,X262,X263,X264)
| ~ p__d__partition6(X259,X260,X261,X262,X263,X264) )
& ( p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264)
| ~ p__d__partition6(X259,X260,X261,X262,X263,X264) )
& ( ~ p__d__exhaustiveDecomposition6(X259,X260,X261,X262,X263,X264)
| ~ p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264)
| p__d__partition6(X259,X260,X261,X262,X263,X264) )
& ( p__d__exhaustiveDecomposition5(X254,X255,X256,X257,X258)
| ~ p__d__partition5(X254,X255,X256,X257,X258) )
& ( p__d__disjointDecomposition5(X254,X255,X256,X257,X258)
| ~ p__d__partition5(X254,X255,X256,X257,X258) )
& ( ~ p__d__exhaustiveDecomposition5(X254,X255,X256,X257,X258)
| ~ p__d__disjointDecomposition5(X254,X255,X256,X257,X258)
| p__d__partition5(X254,X255,X256,X257,X258) )
& ( p__d__exhaustiveDecomposition4(X250,X251,X252,X253)
| ~ p__d__partition4(X250,X251,X252,X253) )
& ( p__d__disjointDecomposition4(X250,X251,X252,X253)
| ~ p__d__partition4(X250,X251,X252,X253) )
& ( ~ p__d__exhaustiveDecomposition4(X250,X251,X252,X253)
| ~ p__d__disjointDecomposition4(X250,X251,X252,X253)
| p__d__partition4(X250,X251,X252,X253) )
& ( p__d__exhaustiveDecomposition3(X247,X248,X249)
| ~ p__d__partition3(X247,X248,X249) )
& ( p__d__disjointDecomposition3(X247,X248,X249)
| ~ p__d__partition3(X247,X248,X249) )
& ( ~ p__d__exhaustiveDecomposition3(X247,X248,X249)
| ~ p__d__disjointDecomposition3(X247,X248,X249)
| p__d__partition3(X247,X248,X249) ) ),
inference(distribute,[status(thm)],[3048]) ).
cnf(3051,plain,
( p__d__disjointDecomposition3(X1,X2,X3)
| ~ p__d__partition3(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[3049]) ).
fof(3065,plain,
! [X247,X248] :
( ( ~ p__d__disjoint(X247,X248)
| ! [X185] :
( ~ p__d__instance(X185,X247)
| ~ p__d__instance(X185,X248) ) )
& ( ? [X185] :
( p__d__instance(X185,X247)
& p__d__instance(X185,X248) )
| p__d__disjoint(X247,X248) ) ),
inference(fof_nnf,[status(thm)],[1125]) ).
fof(3066,plain,
! [X249,X250] :
( ( ~ p__d__disjoint(X249,X250)
| ! [X251] :
( ~ p__d__instance(X251,X249)
| ~ p__d__instance(X251,X250) ) )
& ( ? [X252] :
( p__d__instance(X252,X249)
& p__d__instance(X252,X250) )
| p__d__disjoint(X249,X250) ) ),
inference(variable_rename,[status(thm)],[3065]) ).
fof(3067,plain,
! [X249,X250] :
( ( ~ p__d__disjoint(X249,X250)
| ! [X251] :
( ~ p__d__instance(X251,X249)
| ~ p__d__instance(X251,X250) ) )
& ( ( p__d__instance(esk163_2(X249,X250),X249)
& p__d__instance(esk163_2(X249,X250),X250) )
| p__d__disjoint(X249,X250) ) ),
inference(skolemize,[status(esa)],[3066]) ).
fof(3068,plain,
! [X249,X250,X251] :
( ( ~ p__d__instance(X251,X249)
| ~ p__d__instance(X251,X250)
| ~ p__d__disjoint(X249,X250) )
& ( ( p__d__instance(esk163_2(X249,X250),X249)
& p__d__instance(esk163_2(X249,X250),X250) )
| p__d__disjoint(X249,X250) ) ),
inference(shift_quantors,[status(thm)],[3067]) ).
fof(3069,plain,
! [X249,X250,X251] :
( ( ~ p__d__instance(X251,X249)
| ~ p__d__instance(X251,X250)
| ~ p__d__disjoint(X249,X250) )
& ( p__d__instance(esk163_2(X249,X250),X249)
| p__d__disjoint(X249,X250) )
& ( p__d__instance(esk163_2(X249,X250),X250)
| p__d__disjoint(X249,X250) ) ),
inference(distribute,[status(thm)],[3068]) ).
cnf(3072,plain,
( ~ p__d__disjoint(X1,X2)
| ~ p__d__instance(X3,X2)
| ~ p__d__instance(X3,X1) ),
inference(split_conjunct,[status(thm)],[3069]) ).
fof(3966,plain,
( ! [X28,X241,X242] :
( ( ~ p__d__disjointDecomposition3(X28,X241,X242)
| p__d__disjoint(X241,X242) )
& ( ~ p__d__disjoint(X241,X242)
| p__d__disjointDecomposition3(X28,X241,X242) ) )
& ! [X28,X241,X242,X243] :
( ( ~ p__d__disjointDecomposition4(X28,X241,X242,X243)
| ( p__d__disjoint(X241,X242)
& p__d__disjoint(X241,X243)
& p__d__disjoint(X242,X243) ) )
& ( ~ p__d__disjoint(X241,X242)
| ~ p__d__disjoint(X241,X243)
| ~ p__d__disjoint(X242,X243)
| p__d__disjointDecomposition4(X28,X241,X242,X243) ) )
& ! [X28,X241,X242,X243,X244] :
( ( ~ p__d__disjointDecomposition5(X28,X241,X242,X243,X244)
| ( p__d__disjoint(X241,X242)
& p__d__disjoint(X241,X243)
& p__d__disjoint(X241,X244)
& p__d__disjoint(X242,X243)
& p__d__disjoint(X242,X244)
& p__d__disjoint(X243,X244) ) )
& ( ~ p__d__disjoint(X241,X242)
| ~ p__d__disjoint(X241,X243)
| ~ p__d__disjoint(X241,X244)
| ~ p__d__disjoint(X242,X243)
| ~ p__d__disjoint(X242,X244)
| ~ p__d__disjoint(X243,X244)
| p__d__disjointDecomposition5(X28,X241,X242,X243,X244) ) )
& ! [X28,X241,X242,X243,X244,X245] :
( ( ~ p__d__disjointDecomposition6(X28,X241,X242,X243,X244,X245)
| ( p__d__disjoint(X241,X242)
& p__d__disjoint(X241,X243)
& p__d__disjoint(X241,X244)
& p__d__disjoint(X241,X245)
& p__d__disjoint(X242,X243)
& p__d__disjoint(X242,X244)
& p__d__disjoint(X242,X245)
& p__d__disjoint(X243,X244)
& p__d__disjoint(X243,X245)
& p__d__disjoint(X244,X245) ) )
& ( ~ p__d__disjoint(X241,X242)
| ~ p__d__disjoint(X241,X243)
| ~ p__d__disjoint(X241,X244)
| ~ p__d__disjoint(X241,X245)
| ~ p__d__disjoint(X242,X243)
| ~ p__d__disjoint(X242,X244)
| ~ p__d__disjoint(X242,X245)
| ~ p__d__disjoint(X243,X244)
| ~ p__d__disjoint(X243,X245)
| ~ p__d__disjoint(X244,X245)
| p__d__disjointDecomposition6(X28,X241,X242,X243,X244,X245) ) )
& ! [X28,X241,X242,X243,X244,X245,X246] :
( ( ~ p__d__disjointDecomposition7(X28,X241,X242,X243,X244,X245,X246)
| ( p__d__disjoint(X241,X242)
& p__d__disjoint(X241,X243)
& p__d__disjoint(X241,X244)
& p__d__disjoint(X241,X245)
& p__d__disjoint(X241,X246)
& p__d__disjoint(X242,X243)
& p__d__disjoint(X242,X244)
& p__d__disjoint(X242,X245)
& p__d__disjoint(X242,X246)
& p__d__disjoint(X243,X244)
& p__d__disjoint(X243,X245)
& p__d__disjoint(X243,X246)
& p__d__disjoint(X244,X245)
& p__d__disjoint(X244,X246)
& p__d__disjoint(X245,X246) ) )
& ( ~ p__d__disjoint(X241,X242)
| ~ p__d__disjoint(X241,X243)
| ~ p__d__disjoint(X241,X244)
| ~ p__d__disjoint(X241,X245)
| ~ p__d__disjoint(X241,X246)
| ~ p__d__disjoint(X242,X243)
| ~ p__d__disjoint(X242,X244)
| ~ p__d__disjoint(X242,X245)
| ~ p__d__disjoint(X242,X246)
| ~ p__d__disjoint(X243,X244)
| ~ p__d__disjoint(X243,X245)
| ~ p__d__disjoint(X243,X246)
| ~ p__d__disjoint(X244,X245)
| ~ p__d__disjoint(X244,X246)
| ~ p__d__disjoint(X245,X246)
| p__d__disjointDecomposition7(X28,X241,X242,X243,X244,X245,X246) ) ) ),
inference(fof_nnf,[status(thm)],[1032]) ).
fof(3967,plain,
( ! [X247,X248,X249] :
( ( ~ p__d__disjointDecomposition3(X247,X248,X249)
| p__d__disjoint(X248,X249) )
& ( ~ p__d__disjoint(X248,X249)
| p__d__disjointDecomposition3(X247,X248,X249) ) )
& ! [X250,X251,X252,X253] :
( ( ~ p__d__disjointDecomposition4(X250,X251,X252,X253)
| ( p__d__disjoint(X251,X252)
& p__d__disjoint(X251,X253)
& p__d__disjoint(X252,X253) ) )
& ( ~ p__d__disjoint(X251,X252)
| ~ p__d__disjoint(X251,X253)
| ~ p__d__disjoint(X252,X253)
| p__d__disjointDecomposition4(X250,X251,X252,X253) ) )
& ! [X254,X255,X256,X257,X258] :
( ( ~ p__d__disjointDecomposition5(X254,X255,X256,X257,X258)
| ( p__d__disjoint(X255,X256)
& p__d__disjoint(X255,X257)
& p__d__disjoint(X255,X258)
& p__d__disjoint(X256,X257)
& p__d__disjoint(X256,X258)
& p__d__disjoint(X257,X258) ) )
& ( ~ p__d__disjoint(X255,X256)
| ~ p__d__disjoint(X255,X257)
| ~ p__d__disjoint(X255,X258)
| ~ p__d__disjoint(X256,X257)
| ~ p__d__disjoint(X256,X258)
| ~ p__d__disjoint(X257,X258)
| p__d__disjointDecomposition5(X254,X255,X256,X257,X258) ) )
& ! [X259,X260,X261,X262,X263,X264] :
( ( ~ p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264)
| ( p__d__disjoint(X260,X261)
& p__d__disjoint(X260,X262)
& p__d__disjoint(X260,X263)
& p__d__disjoint(X260,X264)
& p__d__disjoint(X261,X262)
& p__d__disjoint(X261,X263)
& p__d__disjoint(X261,X264)
& p__d__disjoint(X262,X263)
& p__d__disjoint(X262,X264)
& p__d__disjoint(X263,X264) ) )
& ( ~ p__d__disjoint(X260,X261)
| ~ p__d__disjoint(X260,X262)
| ~ p__d__disjoint(X260,X263)
| ~ p__d__disjoint(X260,X264)
| ~ p__d__disjoint(X261,X262)
| ~ p__d__disjoint(X261,X263)
| ~ p__d__disjoint(X261,X264)
| ~ p__d__disjoint(X262,X263)
| ~ p__d__disjoint(X262,X264)
| ~ p__d__disjoint(X263,X264)
| p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264) ) )
& ! [X265,X266,X267,X268,X269,X270,X271] :
( ( ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271)
| ( p__d__disjoint(X266,X267)
& p__d__disjoint(X266,X268)
& p__d__disjoint(X266,X269)
& p__d__disjoint(X266,X270)
& p__d__disjoint(X266,X271)
& p__d__disjoint(X267,X268)
& p__d__disjoint(X267,X269)
& p__d__disjoint(X267,X270)
& p__d__disjoint(X267,X271)
& p__d__disjoint(X268,X269)
& p__d__disjoint(X268,X270)
& p__d__disjoint(X268,X271)
& p__d__disjoint(X269,X270)
& p__d__disjoint(X269,X271)
& p__d__disjoint(X270,X271) ) )
& ( ~ p__d__disjoint(X266,X267)
| ~ p__d__disjoint(X266,X268)
| ~ p__d__disjoint(X266,X269)
| ~ p__d__disjoint(X266,X270)
| ~ p__d__disjoint(X266,X271)
| ~ p__d__disjoint(X267,X268)
| ~ p__d__disjoint(X267,X269)
| ~ p__d__disjoint(X267,X270)
| ~ p__d__disjoint(X267,X271)
| ~ p__d__disjoint(X268,X269)
| ~ p__d__disjoint(X268,X270)
| ~ p__d__disjoint(X268,X271)
| ~ p__d__disjoint(X269,X270)
| ~ p__d__disjoint(X269,X271)
| ~ p__d__disjoint(X270,X271)
| p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) ) ) ),
inference(variable_rename,[status(thm)],[3966]) ).
fof(3968,plain,
! [X247,X248,X249,X250,X251,X252,X253,X254,X255,X256,X257,X258,X259,X260,X261,X262,X263,X264,X265,X266,X267,X268,X269,X270,X271] :
( ( ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271)
| ( p__d__disjoint(X266,X267)
& p__d__disjoint(X266,X268)
& p__d__disjoint(X266,X269)
& p__d__disjoint(X266,X270)
& p__d__disjoint(X266,X271)
& p__d__disjoint(X267,X268)
& p__d__disjoint(X267,X269)
& p__d__disjoint(X267,X270)
& p__d__disjoint(X267,X271)
& p__d__disjoint(X268,X269)
& p__d__disjoint(X268,X270)
& p__d__disjoint(X268,X271)
& p__d__disjoint(X269,X270)
& p__d__disjoint(X269,X271)
& p__d__disjoint(X270,X271) ) )
& ( ~ p__d__disjoint(X266,X267)
| ~ p__d__disjoint(X266,X268)
| ~ p__d__disjoint(X266,X269)
| ~ p__d__disjoint(X266,X270)
| ~ p__d__disjoint(X266,X271)
| ~ p__d__disjoint(X267,X268)
| ~ p__d__disjoint(X267,X269)
| ~ p__d__disjoint(X267,X270)
| ~ p__d__disjoint(X267,X271)
| ~ p__d__disjoint(X268,X269)
| ~ p__d__disjoint(X268,X270)
| ~ p__d__disjoint(X268,X271)
| ~ p__d__disjoint(X269,X270)
| ~ p__d__disjoint(X269,X271)
| ~ p__d__disjoint(X270,X271)
| p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( ~ p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264)
| ( p__d__disjoint(X260,X261)
& p__d__disjoint(X260,X262)
& p__d__disjoint(X260,X263)
& p__d__disjoint(X260,X264)
& p__d__disjoint(X261,X262)
& p__d__disjoint(X261,X263)
& p__d__disjoint(X261,X264)
& p__d__disjoint(X262,X263)
& p__d__disjoint(X262,X264)
& p__d__disjoint(X263,X264) ) )
& ( ~ p__d__disjoint(X260,X261)
| ~ p__d__disjoint(X260,X262)
| ~ p__d__disjoint(X260,X263)
| ~ p__d__disjoint(X260,X264)
| ~ p__d__disjoint(X261,X262)
| ~ p__d__disjoint(X261,X263)
| ~ p__d__disjoint(X261,X264)
| ~ p__d__disjoint(X262,X263)
| ~ p__d__disjoint(X262,X264)
| ~ p__d__disjoint(X263,X264)
| p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264) )
& ( ~ p__d__disjointDecomposition5(X254,X255,X256,X257,X258)
| ( p__d__disjoint(X255,X256)
& p__d__disjoint(X255,X257)
& p__d__disjoint(X255,X258)
& p__d__disjoint(X256,X257)
& p__d__disjoint(X256,X258)
& p__d__disjoint(X257,X258) ) )
& ( ~ p__d__disjoint(X255,X256)
| ~ p__d__disjoint(X255,X257)
| ~ p__d__disjoint(X255,X258)
| ~ p__d__disjoint(X256,X257)
| ~ p__d__disjoint(X256,X258)
| ~ p__d__disjoint(X257,X258)
| p__d__disjointDecomposition5(X254,X255,X256,X257,X258) )
& ( ~ p__d__disjointDecomposition4(X250,X251,X252,X253)
| ( p__d__disjoint(X251,X252)
& p__d__disjoint(X251,X253)
& p__d__disjoint(X252,X253) ) )
& ( ~ p__d__disjoint(X251,X252)
| ~ p__d__disjoint(X251,X253)
| ~ p__d__disjoint(X252,X253)
| p__d__disjointDecomposition4(X250,X251,X252,X253) )
& ( ~ p__d__disjointDecomposition3(X247,X248,X249)
| p__d__disjoint(X248,X249) )
& ( ~ p__d__disjoint(X248,X249)
| p__d__disjointDecomposition3(X247,X248,X249) ) ),
inference(shift_quantors,[status(thm)],[3967]) ).
fof(3969,plain,
! [X247,X248,X249,X250,X251,X252,X253,X254,X255,X256,X257,X258,X259,X260,X261,X262,X263,X264,X265,X266,X267,X268,X269,X270,X271] :
( ( p__d__disjoint(X266,X267)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjoint(X266,X268)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjoint(X266,X269)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjoint(X266,X270)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjoint(X266,X271)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjoint(X267,X268)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjoint(X267,X269)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjoint(X267,X270)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjoint(X267,X271)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjoint(X268,X269)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjoint(X268,X270)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjoint(X268,X271)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjoint(X269,X270)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjoint(X269,X271)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjoint(X270,X271)
| ~ p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( ~ p__d__disjoint(X266,X267)
| ~ p__d__disjoint(X266,X268)
| ~ p__d__disjoint(X266,X269)
| ~ p__d__disjoint(X266,X270)
| ~ p__d__disjoint(X266,X271)
| ~ p__d__disjoint(X267,X268)
| ~ p__d__disjoint(X267,X269)
| ~ p__d__disjoint(X267,X270)
| ~ p__d__disjoint(X267,X271)
| ~ p__d__disjoint(X268,X269)
| ~ p__d__disjoint(X268,X270)
| ~ p__d__disjoint(X268,X271)
| ~ p__d__disjoint(X269,X270)
| ~ p__d__disjoint(X269,X271)
| ~ p__d__disjoint(X270,X271)
| p__d__disjointDecomposition7(X265,X266,X267,X268,X269,X270,X271) )
& ( p__d__disjoint(X260,X261)
| ~ p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264) )
& ( p__d__disjoint(X260,X262)
| ~ p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264) )
& ( p__d__disjoint(X260,X263)
| ~ p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264) )
& ( p__d__disjoint(X260,X264)
| ~ p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264) )
& ( p__d__disjoint(X261,X262)
| ~ p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264) )
& ( p__d__disjoint(X261,X263)
| ~ p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264) )
& ( p__d__disjoint(X261,X264)
| ~ p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264) )
& ( p__d__disjoint(X262,X263)
| ~ p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264) )
& ( p__d__disjoint(X262,X264)
| ~ p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264) )
& ( p__d__disjoint(X263,X264)
| ~ p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264) )
& ( ~ p__d__disjoint(X260,X261)
| ~ p__d__disjoint(X260,X262)
| ~ p__d__disjoint(X260,X263)
| ~ p__d__disjoint(X260,X264)
| ~ p__d__disjoint(X261,X262)
| ~ p__d__disjoint(X261,X263)
| ~ p__d__disjoint(X261,X264)
| ~ p__d__disjoint(X262,X263)
| ~ p__d__disjoint(X262,X264)
| ~ p__d__disjoint(X263,X264)
| p__d__disjointDecomposition6(X259,X260,X261,X262,X263,X264) )
& ( p__d__disjoint(X255,X256)
| ~ p__d__disjointDecomposition5(X254,X255,X256,X257,X258) )
& ( p__d__disjoint(X255,X257)
| ~ p__d__disjointDecomposition5(X254,X255,X256,X257,X258) )
& ( p__d__disjoint(X255,X258)
| ~ p__d__disjointDecomposition5(X254,X255,X256,X257,X258) )
& ( p__d__disjoint(X256,X257)
| ~ p__d__disjointDecomposition5(X254,X255,X256,X257,X258) )
& ( p__d__disjoint(X256,X258)
| ~ p__d__disjointDecomposition5(X254,X255,X256,X257,X258) )
& ( p__d__disjoint(X257,X258)
| ~ p__d__disjointDecomposition5(X254,X255,X256,X257,X258) )
& ( ~ p__d__disjoint(X255,X256)
| ~ p__d__disjoint(X255,X257)
| ~ p__d__disjoint(X255,X258)
| ~ p__d__disjoint(X256,X257)
| ~ p__d__disjoint(X256,X258)
| ~ p__d__disjoint(X257,X258)
| p__d__disjointDecomposition5(X254,X255,X256,X257,X258) )
& ( p__d__disjoint(X251,X252)
| ~ p__d__disjointDecomposition4(X250,X251,X252,X253) )
& ( p__d__disjoint(X251,X253)
| ~ p__d__disjointDecomposition4(X250,X251,X252,X253) )
& ( p__d__disjoint(X252,X253)
| ~ p__d__disjointDecomposition4(X250,X251,X252,X253) )
& ( ~ p__d__disjoint(X251,X252)
| ~ p__d__disjoint(X251,X253)
| ~ p__d__disjoint(X252,X253)
| p__d__disjointDecomposition4(X250,X251,X252,X253) )
& ( ~ p__d__disjointDecomposition3(X247,X248,X249)
| p__d__disjoint(X248,X249) )
& ( ~ p__d__disjoint(X248,X249)
| p__d__disjointDecomposition3(X247,X248,X249) ) ),
inference(distribute,[status(thm)],[3968]) ).
cnf(3971,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__disjointDecomposition3(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[3969]) ).
fof(4162,negated_conjecture,
? [X18,X19] :
( p__d__instance(X19,c__Invertebrate)
& p__d__instance(X18,c__Vertebrate)
& equal(X18,X19) ),
inference(fof_nnf,[status(thm)],[1103]) ).
fof(4163,negated_conjecture,
? [X20,X21] :
( p__d__instance(X21,c__Invertebrate)
& p__d__instance(X20,c__Vertebrate)
& equal(X20,X21) ),
inference(variable_rename,[status(thm)],[4162]) ).
fof(4164,negated_conjecture,
( p__d__instance(esk242_0,c__Invertebrate)
& p__d__instance(esk241_0,c__Vertebrate)
& equal(esk241_0,esk242_0) ),
inference(skolemize,[status(esa)],[4163]) ).
cnf(4165,negated_conjecture,
esk241_0 = esk242_0,
inference(split_conjunct,[status(thm)],[4164]) ).
cnf(4166,negated_conjecture,
p__d__instance(esk241_0,c__Vertebrate),
inference(split_conjunct,[status(thm)],[4164]) ).
cnf(4167,negated_conjecture,
p__d__instance(esk242_0,c__Invertebrate),
inference(split_conjunct,[status(thm)],[4164]) ).
cnf(4168,negated_conjecture,
p__d__instance(esk241_0,c__Invertebrate),
inference(rw,[status(thm)],[4167,4165,theory(equality)]) ).
cnf(5639,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__partition3(X3,X1,X2) ),
inference(spm,[status(thm)],[3971,3051,theory(equality)]) ).
cnf(27984,plain,
p__d__disjoint(c__Vertebrate,c__Invertebrate),
inference(spm,[status(thm)],[5639,1197,theory(equality)]) ).
cnf(28008,plain,
( ~ p__d__instance(X1,c__Invertebrate)
| ~ p__d__instance(X1,c__Vertebrate) ),
inference(spm,[status(thm)],[3072,27984,theory(equality)]) ).
cnf(28012,negated_conjecture,
~ p__d__instance(esk241_0,c__Vertebrate),
inference(spm,[status(thm)],[28008,4168,theory(equality)]) ).
cnf(28034,negated_conjecture,
$false,
inference(rw,[status(thm)],[28012,4166,theory(equality)]) ).
cnf(28035,negated_conjecture,
$false,
inference(cn,[status(thm)],[28034,theory(equality)]) ).
cnf(28036,negated_conjecture,
$false,
28035,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.04 % Problem : CSR161+1 : TPTP v7.3.0. Released v7.3.0.
% 0.02/0.05 % Command : sine.py -e eprover -t %d %s
% 0.03/0.25 % Computer : n188.star.cs.uiowa.edu
% 0.03/0.25 % Model : x86_64 x86_64
% 0.03/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.25 % Memory : 32218.5MB
% 0.03/0.25 % OS : Linux 3.10.0-862.11.6.el7.x86_64
% 0.03/0.25 % CPULimit : 300
% 0.03/0.25 % DateTime : Tue Feb 19 13:20:41 CST 2019
% 0.07/0.25 % CPUTime :
% 0.07/0.30 % SZS status Started for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.30 --creating new selector for [CSR006+0.ax]
% 0.56/0.86 -running prover on /export/starexec/sandbox2/tmp/tmpjXLEVe/sel_theBenchmark.p_1 with time limit 29
% 0.56/0.86 -running prover with command ['/export/starexec/sandbox2/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=29', '/export/starexec/sandbox2/tmp/tmpjXLEVe/sel_theBenchmark.p_1']
% 0.56/0.86 -prover status CounterSatisfiable
% 0.56/0.86 -running prover on /export/starexec/sandbox2/tmp/tmpjXLEVe/sel_theBenchmark.p_2 with time limit 89
% 0.56/0.86 -running prover with command ['/export/starexec/sandbox2/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=89', '/export/starexec/sandbox2/tmp/tmpjXLEVe/sel_theBenchmark.p_2']
% 0.56/0.86 -prover status CounterSatisfiable
% 0.56/0.86 --creating new selector for [CSR006+0.ax]
% 119.71/120.44 eprover: CPU time limit exceeded, terminating
% 119.87/121.09 -running prover on /export/starexec/sandbox2/tmp/tmpjXLEVe/sel_theBenchmark.p_3 with time limit 119
% 119.87/121.09 -running prover with command ['/export/starexec/sandbox2/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=119', '/export/starexec/sandbox2/tmp/tmpjXLEVe/sel_theBenchmark.p_3']
% 119.87/121.09 -prover status ResourceOut
% 119.87/121.09 --creating new selector for [CSR006+0.ax]
% 123.49/124.94 -running prover on /export/starexec/sandbox2/tmp/tmpjXLEVe/sel_theBenchmark.p_4 with time limit 89
% 123.49/124.94 -running prover with command ['/export/starexec/sandbox2/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=89', '/export/starexec/sandbox2/tmp/tmpjXLEVe/sel_theBenchmark.p_4']
% 123.49/124.94 -prover status Theorem
% 123.49/124.94 Problem theBenchmark.p solved in phase 3.
% 123.49/124.94 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 123.49/124.94 % SZS status Ended for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 123.49/124.94 Solved 1 out of 1.
% 123.49/124.94 # Problem is unsatisfiable (or provable), constructing proof object
% 123.49/124.94 # SZS status Theorem
% 123.49/124.94 # SZS output start CNFRefutation.
% See solution above
% 123.49/124.96 # SZS output end CNFRefutation
%------------------------------------------------------------------------------