%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR219+1 : TPTP v7.3.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sine.py -e eprover -t %d %s
% Computer : n192.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:20 EST 2019
% Result : Theorem 77.32s
% Output : CNFRefutation 77.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 9
% Syntax : Number of formulae : 55 ( 19 unt; 0 def)
% Number of atoms : 649 ( 1 equ)
% Maximal formula atoms : 110 ( 11 avg)
% Number of connectives : 894 ( 300 ~; 289 |; 286 &)
% ( 12 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 68 ( 9 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 1 prp; 0-7 aty)
% Number of functors : 11 ( 11 usr; 10 con; 0-2 aty)
% Number of variables : 317 ( 2 sgn 286 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(607,axiom,
p__d__subclass(c__Number,c__Quantity),
file('/export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_5',mergeA354) ).
fof(640,axiom,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
file('/export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_5',mergeA173) ).
fof(1533,axiom,
! [X142,X141] :
( p__d__disjoint(X142,X141)
<=> ! [X240] :
( ~ p__d__instance(X240,X142)
| ~ p__d__instance(X240,X141) ) ),
file('/export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_5',predefinitionsA15) ).
fof(1765,axiom,
p__d__subclass(c__Object,c__Physical),
file('/export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_5',mergeA181) ).
fof(1958,axiom,
p__d__subclass(c__Quantity,c__Abstract),
file('/export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_5',mergeA332) ).
fof(3063,axiom,
( ! [X163,X658,X659] :
( p__d__partition3(X163,X658,X659)
<=> ( p__d__exhaustiveDecomposition3(X163,X658,X659)
& p__d__disjointDecomposition3(X163,X658,X659) ) )
& ! [X163,X658,X659,X660] :
( p__d__partition4(X163,X658,X659,X660)
<=> ( p__d__exhaustiveDecomposition4(X163,X658,X659,X660)
& p__d__disjointDecomposition4(X163,X658,X659,X660) ) )
& ! [X163,X658,X659,X660,X661] :
( p__d__partition5(X163,X658,X659,X660,X661)
<=> ( p__d__exhaustiveDecomposition5(X163,X658,X659,X660,X661)
& p__d__disjointDecomposition5(X163,X658,X659,X660,X661) ) )
& ! [X163,X658,X659,X660,X661,X662] :
( p__d__partition6(X163,X658,X659,X660,X661,X662)
<=> ( p__d__exhaustiveDecomposition6(X163,X658,X659,X660,X661,X662)
& p__d__disjointDecomposition6(X163,X658,X659,X660,X661,X662) ) )
& ! [X163,X658,X659,X660,X661,X662,X663] :
( p__d__partition7(X163,X658,X659,X660,X661,X662,X663)
<=> ( p__d__exhaustiveDecomposition7(X163,X658,X659,X660,X661,X662,X663)
& p__d__disjointDecomposition7(X163,X658,X659,X660,X661,X662,X663) ) ) ),
file('/export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_5',predefinitionsA18) ).
fof(3066,axiom,
! [X49,X176,X177] :
( ( p__d__instance(X49,X176)
& p__d__subclass(X176,X177) )
=> p__d__instance(X49,X177) ),
file('/export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_5',predefinitionsA12) ).
fof(3318,axiom,
( ! [X163,X658,X659] :
( p__d__disjointDecomposition3(X163,X658,X659)
<=> p__d__disjoint(X658,X659) )
& ! [X163,X658,X659,X660] :
( p__d__disjointDecomposition4(X163,X658,X659,X660)
<=> ( p__d__disjoint(X658,X659)
& p__d__disjoint(X658,X660)
& p__d__disjoint(X659,X660) ) )
& ! [X163,X658,X659,X660,X661] :
( p__d__disjointDecomposition5(X163,X658,X659,X660,X661)
<=> ( p__d__disjoint(X658,X659)
& p__d__disjoint(X658,X660)
& p__d__disjoint(X658,X661)
& p__d__disjoint(X659,X660)
& p__d__disjoint(X659,X661)
& p__d__disjoint(X660,X661) ) )
& ! [X163,X658,X659,X660,X661,X662] :
( p__d__disjointDecomposition6(X163,X658,X659,X660,X661,X662)
<=> ( p__d__disjoint(X658,X659)
& p__d__disjoint(X658,X660)
& p__d__disjoint(X658,X661)
& p__d__disjoint(X658,X662)
& p__d__disjoint(X659,X660)
& p__d__disjoint(X659,X661)
& p__d__disjoint(X659,X662)
& p__d__disjoint(X660,X661)
& p__d__disjoint(X660,X662)
& p__d__disjoint(X661,X662) ) )
& ! [X163,X658,X659,X660,X661,X662,X663] :
( p__d__disjointDecomposition7(X163,X658,X659,X660,X661,X662,X663)
<=> ( p__d__disjoint(X658,X659)
& p__d__disjoint(X658,X660)
& p__d__disjoint(X658,X661)
& p__d__disjoint(X658,X662)
& p__d__disjoint(X658,X663)
& p__d__disjoint(X659,X660)
& p__d__disjoint(X659,X661)
& p__d__disjoint(X659,X662)
& p__d__disjoint(X659,X663)
& p__d__disjoint(X660,X661)
& p__d__disjoint(X660,X662)
& p__d__disjoint(X660,X663)
& p__d__disjoint(X661,X662)
& p__d__disjoint(X661,X663)
& p__d__disjoint(X662,X663) ) ) ),
file('/export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_5',predefinitionsA24) ).
fof(3405,conjecture,
! [X49,X176] :
( p__d__instance(X176,c__Object)
=> ( ( p__d__instance(X49,c__Number)
& ? [X177] :
( p__d__instance(X177,c__Attribute)
& p__d__instance(X177,c__Attribute)
& p__attribute(X176,X177) ) )
=> ~ equal(X49,X176) ) ),
file('/export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_5',antonymPattern10066) ).
fof(3406,negated_conjecture,
~ ! [X49,X176] :
( p__d__instance(X176,c__Object)
=> ( ( p__d__instance(X49,c__Number)
& ? [X177] :
( p__d__instance(X177,c__Attribute)
& p__d__instance(X177,c__Attribute)
& p__attribute(X176,X177) ) )
=> ~ equal(X49,X176) ) ),
inference(assume_negation,[status(cth)],[3405]) ).
fof(3435,plain,
! [X142,X141] :
( p__d__disjoint(X142,X141)
<=> ! [X240] :
( ~ p__d__instance(X240,X142)
| ~ p__d__instance(X240,X141) ) ),
inference(fof_simplification,[status(thm)],[1533,theory(equality)]) ).
fof(3496,negated_conjecture,
~ ! [X49,X176] :
( p__d__instance(X176,c__Object)
=> ( ( p__d__instance(X49,c__Number)
& ? [X177] :
( p__d__instance(X177,c__Attribute)
& p__attribute(X176,X177) ) )
=> ~ equal(X49,X176) ) ),
inference(fof_simplification,[status(thm)],[3406,theory(equality)]) ).
cnf(5100,plain,
p__d__subclass(c__Number,c__Quantity),
inference(split_conjunct,[status(thm)],[607]) ).
cnf(5177,plain,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
inference(split_conjunct,[status(thm)],[640]) ).
fof(7650,plain,
! [X142,X141] :
( ( ~ p__d__disjoint(X142,X141)
| ! [X240] :
( ~ p__d__instance(X240,X142)
| ~ p__d__instance(X240,X141) ) )
& ( ? [X240] :
( p__d__instance(X240,X142)
& p__d__instance(X240,X141) )
| p__d__disjoint(X142,X141) ) ),
inference(fof_nnf,[status(thm)],[3435]) ).
fof(7651,plain,
! [X241,X242] :
( ( ~ p__d__disjoint(X241,X242)
| ! [X243] :
( ~ p__d__instance(X243,X241)
| ~ p__d__instance(X243,X242) ) )
& ( ? [X244] :
( p__d__instance(X244,X241)
& p__d__instance(X244,X242) )
| p__d__disjoint(X241,X242) ) ),
inference(variable_rename,[status(thm)],[7650]) ).
fof(7652,plain,
! [X241,X242] :
( ( ~ p__d__disjoint(X241,X242)
| ! [X243] :
( ~ p__d__instance(X243,X241)
| ~ p__d__instance(X243,X242) ) )
& ( ( p__d__instance(esk282_2(X241,X242),X241)
& p__d__instance(esk282_2(X241,X242),X242) )
| p__d__disjoint(X241,X242) ) ),
inference(skolemize,[status(esa)],[7651]) ).
fof(7653,plain,
! [X241,X242,X243] :
( ( ~ p__d__instance(X243,X241)
| ~ p__d__instance(X243,X242)
| ~ p__d__disjoint(X241,X242) )
& ( ( p__d__instance(esk282_2(X241,X242),X241)
& p__d__instance(esk282_2(X241,X242),X242) )
| p__d__disjoint(X241,X242) ) ),
inference(shift_quantors,[status(thm)],[7652]) ).
fof(7654,plain,
! [X241,X242,X243] :
( ( ~ p__d__instance(X243,X241)
| ~ p__d__instance(X243,X242)
| ~ p__d__disjoint(X241,X242) )
& ( p__d__instance(esk282_2(X241,X242),X241)
| p__d__disjoint(X241,X242) )
& ( p__d__instance(esk282_2(X241,X242),X242)
| p__d__disjoint(X241,X242) ) ),
inference(distribute,[status(thm)],[7653]) ).
cnf(7657,plain,
( ~ p__d__disjoint(X1,X2)
| ~ p__d__instance(X3,X2)
| ~ p__d__instance(X3,X1) ),
inference(split_conjunct,[status(thm)],[7654]) ).
cnf(8326,plain,
p__d__subclass(c__Object,c__Physical),
inference(split_conjunct,[status(thm)],[1765]) ).
cnf(8850,plain,
p__d__subclass(c__Quantity,c__Abstract),
inference(split_conjunct,[status(thm)],[1958]) ).
fof(12068,plain,
( ! [X163,X658,X659] :
( ( ~ p__d__partition3(X163,X658,X659)
| ( p__d__exhaustiveDecomposition3(X163,X658,X659)
& p__d__disjointDecomposition3(X163,X658,X659) ) )
& ( ~ p__d__exhaustiveDecomposition3(X163,X658,X659)
| ~ p__d__disjointDecomposition3(X163,X658,X659)
| p__d__partition3(X163,X658,X659) ) )
& ! [X163,X658,X659,X660] :
( ( ~ p__d__partition4(X163,X658,X659,X660)
| ( p__d__exhaustiveDecomposition4(X163,X658,X659,X660)
& p__d__disjointDecomposition4(X163,X658,X659,X660) ) )
& ( ~ p__d__exhaustiveDecomposition4(X163,X658,X659,X660)
| ~ p__d__disjointDecomposition4(X163,X658,X659,X660)
| p__d__partition4(X163,X658,X659,X660) ) )
& ! [X163,X658,X659,X660,X661] :
( ( ~ p__d__partition5(X163,X658,X659,X660,X661)
| ( p__d__exhaustiveDecomposition5(X163,X658,X659,X660,X661)
& p__d__disjointDecomposition5(X163,X658,X659,X660,X661) ) )
& ( ~ p__d__exhaustiveDecomposition5(X163,X658,X659,X660,X661)
| ~ p__d__disjointDecomposition5(X163,X658,X659,X660,X661)
| p__d__partition5(X163,X658,X659,X660,X661) ) )
& ! [X163,X658,X659,X660,X661,X662] :
( ( ~ p__d__partition6(X163,X658,X659,X660,X661,X662)
| ( p__d__exhaustiveDecomposition6(X163,X658,X659,X660,X661,X662)
& p__d__disjointDecomposition6(X163,X658,X659,X660,X661,X662) ) )
& ( ~ p__d__exhaustiveDecomposition6(X163,X658,X659,X660,X661,X662)
| ~ p__d__disjointDecomposition6(X163,X658,X659,X660,X661,X662)
| p__d__partition6(X163,X658,X659,X660,X661,X662) ) )
& ! [X163,X658,X659,X660,X661,X662,X663] :
( ( ~ p__d__partition7(X163,X658,X659,X660,X661,X662,X663)
| ( p__d__exhaustiveDecomposition7(X163,X658,X659,X660,X661,X662,X663)
& p__d__disjointDecomposition7(X163,X658,X659,X660,X661,X662,X663) ) )
& ( ~ p__d__exhaustiveDecomposition7(X163,X658,X659,X660,X661,X662,X663)
| ~ p__d__disjointDecomposition7(X163,X658,X659,X660,X661,X662,X663)
| p__d__partition7(X163,X658,X659,X660,X661,X662,X663) ) ) ),
inference(fof_nnf,[status(thm)],[3063]) ).
fof(12069,plain,
( ! [X664,X665,X666] :
( ( ~ p__d__partition3(X664,X665,X666)
| ( p__d__exhaustiveDecomposition3(X664,X665,X666)
& p__d__disjointDecomposition3(X664,X665,X666) ) )
& ( ~ p__d__exhaustiveDecomposition3(X664,X665,X666)
| ~ p__d__disjointDecomposition3(X664,X665,X666)
| p__d__partition3(X664,X665,X666) ) )
& ! [X667,X668,X669,X670] :
( ( ~ p__d__partition4(X667,X668,X669,X670)
| ( p__d__exhaustiveDecomposition4(X667,X668,X669,X670)
& p__d__disjointDecomposition4(X667,X668,X669,X670) ) )
& ( ~ p__d__exhaustiveDecomposition4(X667,X668,X669,X670)
| ~ p__d__disjointDecomposition4(X667,X668,X669,X670)
| p__d__partition4(X667,X668,X669,X670) ) )
& ! [X671,X672,X673,X674,X675] :
( ( ~ p__d__partition5(X671,X672,X673,X674,X675)
| ( p__d__exhaustiveDecomposition5(X671,X672,X673,X674,X675)
& p__d__disjointDecomposition5(X671,X672,X673,X674,X675) ) )
& ( ~ p__d__exhaustiveDecomposition5(X671,X672,X673,X674,X675)
| ~ p__d__disjointDecomposition5(X671,X672,X673,X674,X675)
| p__d__partition5(X671,X672,X673,X674,X675) ) )
& ! [X676,X677,X678,X679,X680,X681] :
( ( ~ p__d__partition6(X676,X677,X678,X679,X680,X681)
| ( p__d__exhaustiveDecomposition6(X676,X677,X678,X679,X680,X681)
& p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681) ) )
& ( ~ p__d__exhaustiveDecomposition6(X676,X677,X678,X679,X680,X681)
| ~ p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681)
| p__d__partition6(X676,X677,X678,X679,X680,X681) ) )
& ! [X682,X683,X684,X685,X686,X687,X688] :
( ( ~ p__d__partition7(X682,X683,X684,X685,X686,X687,X688)
| ( p__d__exhaustiveDecomposition7(X682,X683,X684,X685,X686,X687,X688)
& p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) ) )
& ( ~ p__d__exhaustiveDecomposition7(X682,X683,X684,X685,X686,X687,X688)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688)
| p__d__partition7(X682,X683,X684,X685,X686,X687,X688) ) ) ),
inference(variable_rename,[status(thm)],[12068]) ).
fof(12070,plain,
! [X664,X665,X666,X667,X668,X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687,X688] :
( ( ~ p__d__partition7(X682,X683,X684,X685,X686,X687,X688)
| ( p__d__exhaustiveDecomposition7(X682,X683,X684,X685,X686,X687,X688)
& p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) ) )
& ( ~ p__d__exhaustiveDecomposition7(X682,X683,X684,X685,X686,X687,X688)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688)
| p__d__partition7(X682,X683,X684,X685,X686,X687,X688) )
& ( ~ p__d__partition6(X676,X677,X678,X679,X680,X681)
| ( p__d__exhaustiveDecomposition6(X676,X677,X678,X679,X680,X681)
& p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681) ) )
& ( ~ p__d__exhaustiveDecomposition6(X676,X677,X678,X679,X680,X681)
| ~ p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681)
| p__d__partition6(X676,X677,X678,X679,X680,X681) )
& ( ~ p__d__partition5(X671,X672,X673,X674,X675)
| ( p__d__exhaustiveDecomposition5(X671,X672,X673,X674,X675)
& p__d__disjointDecomposition5(X671,X672,X673,X674,X675) ) )
& ( ~ p__d__exhaustiveDecomposition5(X671,X672,X673,X674,X675)
| ~ p__d__disjointDecomposition5(X671,X672,X673,X674,X675)
| p__d__partition5(X671,X672,X673,X674,X675) )
& ( ~ p__d__partition4(X667,X668,X669,X670)
| ( p__d__exhaustiveDecomposition4(X667,X668,X669,X670)
& p__d__disjointDecomposition4(X667,X668,X669,X670) ) )
& ( ~ p__d__exhaustiveDecomposition4(X667,X668,X669,X670)
| ~ p__d__disjointDecomposition4(X667,X668,X669,X670)
| p__d__partition4(X667,X668,X669,X670) )
& ( ~ p__d__partition3(X664,X665,X666)
| ( p__d__exhaustiveDecomposition3(X664,X665,X666)
& p__d__disjointDecomposition3(X664,X665,X666) ) )
& ( ~ p__d__exhaustiveDecomposition3(X664,X665,X666)
| ~ p__d__disjointDecomposition3(X664,X665,X666)
| p__d__partition3(X664,X665,X666) ) ),
inference(shift_quantors,[status(thm)],[12069]) ).
fof(12071,plain,
! [X664,X665,X666,X667,X668,X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687,X688] :
( ( p__d__exhaustiveDecomposition7(X682,X683,X684,X685,X686,X687,X688)
| ~ p__d__partition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688)
| ~ p__d__partition7(X682,X683,X684,X685,X686,X687,X688) )
& ( ~ p__d__exhaustiveDecomposition7(X682,X683,X684,X685,X686,X687,X688)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688)
| p__d__partition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__exhaustiveDecomposition6(X676,X677,X678,X679,X680,X681)
| ~ p__d__partition6(X676,X677,X678,X679,X680,X681) )
& ( p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681)
| ~ p__d__partition6(X676,X677,X678,X679,X680,X681) )
& ( ~ p__d__exhaustiveDecomposition6(X676,X677,X678,X679,X680,X681)
| ~ p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681)
| p__d__partition6(X676,X677,X678,X679,X680,X681) )
& ( p__d__exhaustiveDecomposition5(X671,X672,X673,X674,X675)
| ~ p__d__partition5(X671,X672,X673,X674,X675) )
& ( p__d__disjointDecomposition5(X671,X672,X673,X674,X675)
| ~ p__d__partition5(X671,X672,X673,X674,X675) )
& ( ~ p__d__exhaustiveDecomposition5(X671,X672,X673,X674,X675)
| ~ p__d__disjointDecomposition5(X671,X672,X673,X674,X675)
| p__d__partition5(X671,X672,X673,X674,X675) )
& ( p__d__exhaustiveDecomposition4(X667,X668,X669,X670)
| ~ p__d__partition4(X667,X668,X669,X670) )
& ( p__d__disjointDecomposition4(X667,X668,X669,X670)
| ~ p__d__partition4(X667,X668,X669,X670) )
& ( ~ p__d__exhaustiveDecomposition4(X667,X668,X669,X670)
| ~ p__d__disjointDecomposition4(X667,X668,X669,X670)
| p__d__partition4(X667,X668,X669,X670) )
& ( p__d__exhaustiveDecomposition3(X664,X665,X666)
| ~ p__d__partition3(X664,X665,X666) )
& ( p__d__disjointDecomposition3(X664,X665,X666)
| ~ p__d__partition3(X664,X665,X666) )
& ( ~ p__d__exhaustiveDecomposition3(X664,X665,X666)
| ~ p__d__disjointDecomposition3(X664,X665,X666)
| p__d__partition3(X664,X665,X666) ) ),
inference(distribute,[status(thm)],[12070]) ).
cnf(12073,plain,
( p__d__disjointDecomposition3(X1,X2,X3)
| ~ p__d__partition3(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[12071]) ).
fof(12094,plain,
! [X49,X176,X177] :
( ~ p__d__instance(X49,X176)
| ~ p__d__subclass(X176,X177)
| p__d__instance(X49,X177) ),
inference(fof_nnf,[status(thm)],[3066]) ).
fof(12095,plain,
! [X178,X179,X180] :
( ~ p__d__instance(X178,X179)
| ~ p__d__subclass(X179,X180)
| p__d__instance(X178,X180) ),
inference(variable_rename,[status(thm)],[12094]) ).
cnf(12096,plain,
( p__d__instance(X1,X2)
| ~ p__d__subclass(X3,X2)
| ~ p__d__instance(X1,X3) ),
inference(split_conjunct,[status(thm)],[12095]) ).
fof(12856,plain,
( ! [X163,X658,X659] :
( ( ~ p__d__disjointDecomposition3(X163,X658,X659)
| p__d__disjoint(X658,X659) )
& ( ~ p__d__disjoint(X658,X659)
| p__d__disjointDecomposition3(X163,X658,X659) ) )
& ! [X163,X658,X659,X660] :
( ( ~ p__d__disjointDecomposition4(X163,X658,X659,X660)
| ( p__d__disjoint(X658,X659)
& p__d__disjoint(X658,X660)
& p__d__disjoint(X659,X660) ) )
& ( ~ p__d__disjoint(X658,X659)
| ~ p__d__disjoint(X658,X660)
| ~ p__d__disjoint(X659,X660)
| p__d__disjointDecomposition4(X163,X658,X659,X660) ) )
& ! [X163,X658,X659,X660,X661] :
( ( ~ p__d__disjointDecomposition5(X163,X658,X659,X660,X661)
| ( p__d__disjoint(X658,X659)
& p__d__disjoint(X658,X660)
& p__d__disjoint(X658,X661)
& p__d__disjoint(X659,X660)
& p__d__disjoint(X659,X661)
& p__d__disjoint(X660,X661) ) )
& ( ~ p__d__disjoint(X658,X659)
| ~ p__d__disjoint(X658,X660)
| ~ p__d__disjoint(X658,X661)
| ~ p__d__disjoint(X659,X660)
| ~ p__d__disjoint(X659,X661)
| ~ p__d__disjoint(X660,X661)
| p__d__disjointDecomposition5(X163,X658,X659,X660,X661) ) )
& ! [X163,X658,X659,X660,X661,X662] :
( ( ~ p__d__disjointDecomposition6(X163,X658,X659,X660,X661,X662)
| ( p__d__disjoint(X658,X659)
& p__d__disjoint(X658,X660)
& p__d__disjoint(X658,X661)
& p__d__disjoint(X658,X662)
& p__d__disjoint(X659,X660)
& p__d__disjoint(X659,X661)
& p__d__disjoint(X659,X662)
& p__d__disjoint(X660,X661)
& p__d__disjoint(X660,X662)
& p__d__disjoint(X661,X662) ) )
& ( ~ p__d__disjoint(X658,X659)
| ~ p__d__disjoint(X658,X660)
| ~ p__d__disjoint(X658,X661)
| ~ p__d__disjoint(X658,X662)
| ~ p__d__disjoint(X659,X660)
| ~ p__d__disjoint(X659,X661)
| ~ p__d__disjoint(X659,X662)
| ~ p__d__disjoint(X660,X661)
| ~ p__d__disjoint(X660,X662)
| ~ p__d__disjoint(X661,X662)
| p__d__disjointDecomposition6(X163,X658,X659,X660,X661,X662) ) )
& ! [X163,X658,X659,X660,X661,X662,X663] :
( ( ~ p__d__disjointDecomposition7(X163,X658,X659,X660,X661,X662,X663)
| ( p__d__disjoint(X658,X659)
& p__d__disjoint(X658,X660)
& p__d__disjoint(X658,X661)
& p__d__disjoint(X658,X662)
& p__d__disjoint(X658,X663)
& p__d__disjoint(X659,X660)
& p__d__disjoint(X659,X661)
& p__d__disjoint(X659,X662)
& p__d__disjoint(X659,X663)
& p__d__disjoint(X660,X661)
& p__d__disjoint(X660,X662)
& p__d__disjoint(X660,X663)
& p__d__disjoint(X661,X662)
& p__d__disjoint(X661,X663)
& p__d__disjoint(X662,X663) ) )
& ( ~ p__d__disjoint(X658,X659)
| ~ p__d__disjoint(X658,X660)
| ~ p__d__disjoint(X658,X661)
| ~ p__d__disjoint(X658,X662)
| ~ p__d__disjoint(X658,X663)
| ~ p__d__disjoint(X659,X660)
| ~ p__d__disjoint(X659,X661)
| ~ p__d__disjoint(X659,X662)
| ~ p__d__disjoint(X659,X663)
| ~ p__d__disjoint(X660,X661)
| ~ p__d__disjoint(X660,X662)
| ~ p__d__disjoint(X660,X663)
| ~ p__d__disjoint(X661,X662)
| ~ p__d__disjoint(X661,X663)
| ~ p__d__disjoint(X662,X663)
| p__d__disjointDecomposition7(X163,X658,X659,X660,X661,X662,X663) ) ) ),
inference(fof_nnf,[status(thm)],[3318]) ).
fof(12857,plain,
( ! [X664,X665,X666] :
( ( ~ p__d__disjointDecomposition3(X664,X665,X666)
| p__d__disjoint(X665,X666) )
& ( ~ p__d__disjoint(X665,X666)
| p__d__disjointDecomposition3(X664,X665,X666) ) )
& ! [X667,X668,X669,X670] :
( ( ~ p__d__disjointDecomposition4(X667,X668,X669,X670)
| ( p__d__disjoint(X668,X669)
& p__d__disjoint(X668,X670)
& p__d__disjoint(X669,X670) ) )
& ( ~ p__d__disjoint(X668,X669)
| ~ p__d__disjoint(X668,X670)
| ~ p__d__disjoint(X669,X670)
| p__d__disjointDecomposition4(X667,X668,X669,X670) ) )
& ! [X671,X672,X673,X674,X675] :
( ( ~ p__d__disjointDecomposition5(X671,X672,X673,X674,X675)
| ( p__d__disjoint(X672,X673)
& p__d__disjoint(X672,X674)
& p__d__disjoint(X672,X675)
& p__d__disjoint(X673,X674)
& p__d__disjoint(X673,X675)
& p__d__disjoint(X674,X675) ) )
& ( ~ p__d__disjoint(X672,X673)
| ~ p__d__disjoint(X672,X674)
| ~ p__d__disjoint(X672,X675)
| ~ p__d__disjoint(X673,X674)
| ~ p__d__disjoint(X673,X675)
| ~ p__d__disjoint(X674,X675)
| p__d__disjointDecomposition5(X671,X672,X673,X674,X675) ) )
& ! [X676,X677,X678,X679,X680,X681] :
( ( ~ p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681)
| ( p__d__disjoint(X677,X678)
& p__d__disjoint(X677,X679)
& p__d__disjoint(X677,X680)
& p__d__disjoint(X677,X681)
& p__d__disjoint(X678,X679)
& p__d__disjoint(X678,X680)
& p__d__disjoint(X678,X681)
& p__d__disjoint(X679,X680)
& p__d__disjoint(X679,X681)
& p__d__disjoint(X680,X681) ) )
& ( ~ p__d__disjoint(X677,X678)
| ~ p__d__disjoint(X677,X679)
| ~ p__d__disjoint(X677,X680)
| ~ p__d__disjoint(X677,X681)
| ~ p__d__disjoint(X678,X679)
| ~ p__d__disjoint(X678,X680)
| ~ p__d__disjoint(X678,X681)
| ~ p__d__disjoint(X679,X680)
| ~ p__d__disjoint(X679,X681)
| ~ p__d__disjoint(X680,X681)
| p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681) ) )
& ! [X682,X683,X684,X685,X686,X687,X688] :
( ( ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688)
| ( p__d__disjoint(X683,X684)
& p__d__disjoint(X683,X685)
& p__d__disjoint(X683,X686)
& p__d__disjoint(X683,X687)
& p__d__disjoint(X683,X688)
& p__d__disjoint(X684,X685)
& p__d__disjoint(X684,X686)
& p__d__disjoint(X684,X687)
& p__d__disjoint(X684,X688)
& p__d__disjoint(X685,X686)
& p__d__disjoint(X685,X687)
& p__d__disjoint(X685,X688)
& p__d__disjoint(X686,X687)
& p__d__disjoint(X686,X688)
& p__d__disjoint(X687,X688) ) )
& ( ~ p__d__disjoint(X683,X684)
| ~ p__d__disjoint(X683,X685)
| ~ p__d__disjoint(X683,X686)
| ~ p__d__disjoint(X683,X687)
| ~ p__d__disjoint(X683,X688)
| ~ p__d__disjoint(X684,X685)
| ~ p__d__disjoint(X684,X686)
| ~ p__d__disjoint(X684,X687)
| ~ p__d__disjoint(X684,X688)
| ~ p__d__disjoint(X685,X686)
| ~ p__d__disjoint(X685,X687)
| ~ p__d__disjoint(X685,X688)
| ~ p__d__disjoint(X686,X687)
| ~ p__d__disjoint(X686,X688)
| ~ p__d__disjoint(X687,X688)
| p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) ) ) ),
inference(variable_rename,[status(thm)],[12856]) ).
fof(12858,plain,
! [X664,X665,X666,X667,X668,X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687,X688] :
( ( ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688)
| ( p__d__disjoint(X683,X684)
& p__d__disjoint(X683,X685)
& p__d__disjoint(X683,X686)
& p__d__disjoint(X683,X687)
& p__d__disjoint(X683,X688)
& p__d__disjoint(X684,X685)
& p__d__disjoint(X684,X686)
& p__d__disjoint(X684,X687)
& p__d__disjoint(X684,X688)
& p__d__disjoint(X685,X686)
& p__d__disjoint(X685,X687)
& p__d__disjoint(X685,X688)
& p__d__disjoint(X686,X687)
& p__d__disjoint(X686,X688)
& p__d__disjoint(X687,X688) ) )
& ( ~ p__d__disjoint(X683,X684)
| ~ p__d__disjoint(X683,X685)
| ~ p__d__disjoint(X683,X686)
| ~ p__d__disjoint(X683,X687)
| ~ p__d__disjoint(X683,X688)
| ~ p__d__disjoint(X684,X685)
| ~ p__d__disjoint(X684,X686)
| ~ p__d__disjoint(X684,X687)
| ~ p__d__disjoint(X684,X688)
| ~ p__d__disjoint(X685,X686)
| ~ p__d__disjoint(X685,X687)
| ~ p__d__disjoint(X685,X688)
| ~ p__d__disjoint(X686,X687)
| ~ p__d__disjoint(X686,X688)
| ~ p__d__disjoint(X687,X688)
| p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( ~ p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681)
| ( p__d__disjoint(X677,X678)
& p__d__disjoint(X677,X679)
& p__d__disjoint(X677,X680)
& p__d__disjoint(X677,X681)
& p__d__disjoint(X678,X679)
& p__d__disjoint(X678,X680)
& p__d__disjoint(X678,X681)
& p__d__disjoint(X679,X680)
& p__d__disjoint(X679,X681)
& p__d__disjoint(X680,X681) ) )
& ( ~ p__d__disjoint(X677,X678)
| ~ p__d__disjoint(X677,X679)
| ~ p__d__disjoint(X677,X680)
| ~ p__d__disjoint(X677,X681)
| ~ p__d__disjoint(X678,X679)
| ~ p__d__disjoint(X678,X680)
| ~ p__d__disjoint(X678,X681)
| ~ p__d__disjoint(X679,X680)
| ~ p__d__disjoint(X679,X681)
| ~ p__d__disjoint(X680,X681)
| p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681) )
& ( ~ p__d__disjointDecomposition5(X671,X672,X673,X674,X675)
| ( p__d__disjoint(X672,X673)
& p__d__disjoint(X672,X674)
& p__d__disjoint(X672,X675)
& p__d__disjoint(X673,X674)
& p__d__disjoint(X673,X675)
& p__d__disjoint(X674,X675) ) )
& ( ~ p__d__disjoint(X672,X673)
| ~ p__d__disjoint(X672,X674)
| ~ p__d__disjoint(X672,X675)
| ~ p__d__disjoint(X673,X674)
| ~ p__d__disjoint(X673,X675)
| ~ p__d__disjoint(X674,X675)
| p__d__disjointDecomposition5(X671,X672,X673,X674,X675) )
& ( ~ p__d__disjointDecomposition4(X667,X668,X669,X670)
| ( p__d__disjoint(X668,X669)
& p__d__disjoint(X668,X670)
& p__d__disjoint(X669,X670) ) )
& ( ~ p__d__disjoint(X668,X669)
| ~ p__d__disjoint(X668,X670)
| ~ p__d__disjoint(X669,X670)
| p__d__disjointDecomposition4(X667,X668,X669,X670) )
& ( ~ p__d__disjointDecomposition3(X664,X665,X666)
| p__d__disjoint(X665,X666) )
& ( ~ p__d__disjoint(X665,X666)
| p__d__disjointDecomposition3(X664,X665,X666) ) ),
inference(shift_quantors,[status(thm)],[12857]) ).
fof(12859,plain,
! [X664,X665,X666,X667,X668,X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687,X688] :
( ( p__d__disjoint(X683,X684)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjoint(X683,X685)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjoint(X683,X686)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjoint(X683,X687)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjoint(X683,X688)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjoint(X684,X685)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjoint(X684,X686)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjoint(X684,X687)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjoint(X684,X688)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjoint(X685,X686)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjoint(X685,X687)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjoint(X685,X688)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjoint(X686,X687)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjoint(X686,X688)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjoint(X687,X688)
| ~ p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( ~ p__d__disjoint(X683,X684)
| ~ p__d__disjoint(X683,X685)
| ~ p__d__disjoint(X683,X686)
| ~ p__d__disjoint(X683,X687)
| ~ p__d__disjoint(X683,X688)
| ~ p__d__disjoint(X684,X685)
| ~ p__d__disjoint(X684,X686)
| ~ p__d__disjoint(X684,X687)
| ~ p__d__disjoint(X684,X688)
| ~ p__d__disjoint(X685,X686)
| ~ p__d__disjoint(X685,X687)
| ~ p__d__disjoint(X685,X688)
| ~ p__d__disjoint(X686,X687)
| ~ p__d__disjoint(X686,X688)
| ~ p__d__disjoint(X687,X688)
| p__d__disjointDecomposition7(X682,X683,X684,X685,X686,X687,X688) )
& ( p__d__disjoint(X677,X678)
| ~ p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681) )
& ( p__d__disjoint(X677,X679)
| ~ p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681) )
& ( p__d__disjoint(X677,X680)
| ~ p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681) )
& ( p__d__disjoint(X677,X681)
| ~ p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681) )
& ( p__d__disjoint(X678,X679)
| ~ p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681) )
& ( p__d__disjoint(X678,X680)
| ~ p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681) )
& ( p__d__disjoint(X678,X681)
| ~ p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681) )
& ( p__d__disjoint(X679,X680)
| ~ p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681) )
& ( p__d__disjoint(X679,X681)
| ~ p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681) )
& ( p__d__disjoint(X680,X681)
| ~ p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681) )
& ( ~ p__d__disjoint(X677,X678)
| ~ p__d__disjoint(X677,X679)
| ~ p__d__disjoint(X677,X680)
| ~ p__d__disjoint(X677,X681)
| ~ p__d__disjoint(X678,X679)
| ~ p__d__disjoint(X678,X680)
| ~ p__d__disjoint(X678,X681)
| ~ p__d__disjoint(X679,X680)
| ~ p__d__disjoint(X679,X681)
| ~ p__d__disjoint(X680,X681)
| p__d__disjointDecomposition6(X676,X677,X678,X679,X680,X681) )
& ( p__d__disjoint(X672,X673)
| ~ p__d__disjointDecomposition5(X671,X672,X673,X674,X675) )
& ( p__d__disjoint(X672,X674)
| ~ p__d__disjointDecomposition5(X671,X672,X673,X674,X675) )
& ( p__d__disjoint(X672,X675)
| ~ p__d__disjointDecomposition5(X671,X672,X673,X674,X675) )
& ( p__d__disjoint(X673,X674)
| ~ p__d__disjointDecomposition5(X671,X672,X673,X674,X675) )
& ( p__d__disjoint(X673,X675)
| ~ p__d__disjointDecomposition5(X671,X672,X673,X674,X675) )
& ( p__d__disjoint(X674,X675)
| ~ p__d__disjointDecomposition5(X671,X672,X673,X674,X675) )
& ( ~ p__d__disjoint(X672,X673)
| ~ p__d__disjoint(X672,X674)
| ~ p__d__disjoint(X672,X675)
| ~ p__d__disjoint(X673,X674)
| ~ p__d__disjoint(X673,X675)
| ~ p__d__disjoint(X674,X675)
| p__d__disjointDecomposition5(X671,X672,X673,X674,X675) )
& ( p__d__disjoint(X668,X669)
| ~ p__d__disjointDecomposition4(X667,X668,X669,X670) )
& ( p__d__disjoint(X668,X670)
| ~ p__d__disjointDecomposition4(X667,X668,X669,X670) )
& ( p__d__disjoint(X669,X670)
| ~ p__d__disjointDecomposition4(X667,X668,X669,X670) )
& ( ~ p__d__disjoint(X668,X669)
| ~ p__d__disjoint(X668,X670)
| ~ p__d__disjoint(X669,X670)
| p__d__disjointDecomposition4(X667,X668,X669,X670) )
& ( ~ p__d__disjointDecomposition3(X664,X665,X666)
| p__d__disjoint(X665,X666) )
& ( ~ p__d__disjoint(X665,X666)
| p__d__disjointDecomposition3(X664,X665,X666) ) ),
inference(distribute,[status(thm)],[12858]) ).
cnf(12861,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__disjointDecomposition3(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[12859]) ).
fof(13152,negated_conjecture,
? [X49,X176] :
( p__d__instance(X176,c__Object)
& p__d__instance(X49,c__Number)
& ? [X177] :
( p__d__instance(X177,c__Attribute)
& p__attribute(X176,X177) )
& equal(X49,X176) ),
inference(fof_nnf,[status(thm)],[3496]) ).
fof(13153,negated_conjecture,
? [X178,X179] :
( p__d__instance(X179,c__Object)
& p__d__instance(X178,c__Number)
& ? [X180] :
( p__d__instance(X180,c__Attribute)
& p__attribute(X179,X180) )
& equal(X178,X179) ),
inference(variable_rename,[status(thm)],[13152]) ).
fof(13154,negated_conjecture,
( p__d__instance(esk707_0,c__Object)
& p__d__instance(esk706_0,c__Number)
& p__d__instance(esk708_0,c__Attribute)
& p__attribute(esk707_0,esk708_0)
& equal(esk706_0,esk707_0) ),
inference(skolemize,[status(esa)],[13153]) ).
cnf(13155,negated_conjecture,
esk706_0 = esk707_0,
inference(split_conjunct,[status(thm)],[13154]) ).
cnf(13158,negated_conjecture,
p__d__instance(esk706_0,c__Number),
inference(split_conjunct,[status(thm)],[13154]) ).
cnf(13159,negated_conjecture,
p__d__instance(esk707_0,c__Object),
inference(split_conjunct,[status(thm)],[13154]) ).
cnf(13160,negated_conjecture,
p__d__instance(esk707_0,c__Number),
inference(rw,[status(thm)],[13158,13155,theory(equality)]) ).
cnf(13685,plain,
( p__d__instance(X1,c__Physical)
| ~ p__d__instance(X1,c__Object) ),
inference(spm,[status(thm)],[12096,8326,theory(equality)]) ).
cnf(13695,plain,
( p__d__instance(X1,c__Quantity)
| ~ p__d__instance(X1,c__Number) ),
inference(spm,[status(thm)],[12096,5100,theory(equality)]) ).
cnf(13738,plain,
( p__d__instance(X1,c__Abstract)
| ~ p__d__instance(X1,c__Quantity) ),
inference(spm,[status(thm)],[12096,8850,theory(equality)]) ).
cnf(17005,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__partition3(X3,X1,X2) ),
inference(spm,[status(thm)],[12861,12073,theory(equality)]) ).
cnf(34171,negated_conjecture,
p__d__instance(esk707_0,c__Quantity),
inference(spm,[status(thm)],[13695,13160,theory(equality)]) ).
cnf(99596,plain,
p__d__disjoint(c__Physical,c__Abstract),
inference(spm,[status(thm)],[17005,5177,theory(equality)]) ).
cnf(100169,plain,
( ~ p__d__instance(X1,c__Abstract)
| ~ p__d__instance(X1,c__Physical) ),
inference(spm,[status(thm)],[7657,99596,theory(equality)]) ).
cnf(100687,plain,
( ~ p__d__instance(X1,c__Physical)
| ~ p__d__instance(X1,c__Quantity) ),
inference(spm,[status(thm)],[100169,13738,theory(equality)]) ).
cnf(114619,negated_conjecture,
~ p__d__instance(esk707_0,c__Physical),
inference(spm,[status(thm)],[100687,34171,theory(equality)]) ).
cnf(114661,negated_conjecture,
~ p__d__instance(esk707_0,c__Object),
inference(spm,[status(thm)],[114619,13685,theory(equality)]) ).
cnf(114663,negated_conjecture,
$false,
inference(rw,[status(thm)],[114661,13159,theory(equality)]) ).
cnf(114664,negated_conjecture,
$false,
inference(cn,[status(thm)],[114663,theory(equality)]) ).
cnf(114665,negated_conjecture,
$false,
114664,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR219+1 : TPTP v7.3.0. Released v7.3.0.
% 0.00/0.05 % Command : sine.py -e eprover -t %d %s
% 0.04/0.25 % Computer : n192.star.cs.uiowa.edu
% 0.04/0.25 % Model : x86_64 x86_64
% 0.04/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.04/0.25 % Memory : 32218.5MB
% 0.04/0.25 % OS : Linux 3.10.0-862.11.6.el7.x86_64
% 0.04/0.25 % CPULimit : 300
% 0.04/0.25 % DateTime : Tue Feb 19 22:58:40 CST 2019
% 0.04/0.25 % CPUTime :
% 0.04/0.30 % SZS status Started for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/0.30 --creating new selector for [CSR006+0.ax]
% 0.55/0.82 -running prover on /export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_1 with time limit 29
% 0.55/0.82 -running prover with command ['/export/starexec/sandbox/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=29', '/export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_1']
% 0.55/0.82 -prover status CounterSatisfiable
% 0.55/0.82 -running prover on /export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_2 with time limit 89
% 0.55/0.82 -running prover with command ['/export/starexec/sandbox/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=89', '/export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_2']
% 0.55/0.82 -prover status CounterSatisfiable
% 0.55/0.82 --creating new selector for [CSR006+0.ax]
% 0.71/1.01 -running prover on /export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_3 with time limit 119
% 0.71/1.01 -running prover with command ['/export/starexec/sandbox/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=119', '/export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_3']
% 0.71/1.01 -prover status CounterSatisfiable
% 0.71/1.01 --creating new selector for [CSR006+0.ax]
% 1.51/1.77 -running prover on /export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_4 with time limit 149
% 1.51/1.77 -running prover with command ['/export/starexec/sandbox/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=149', '/export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_4']
% 1.51/1.77 -prover status CounterSatisfiable
% 1.51/1.77 --creating new selector for [CSR006+0.ax]
% 77.32/77.64 -running prover on /export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_5 with time limit 298
% 77.32/77.64 -running prover with command ['/export/starexec/sandbox/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=298', '/export/starexec/sandbox/tmp/tmpCrlesm/sel_theBenchmark.p_5']
% 77.32/77.64 -prover status Theorem
% 77.32/77.64 Problem theBenchmark.p solved in phase 4.
% 77.32/77.64 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 77.32/77.64 % SZS status Ended for /export/starexec/sandbox/benchmark/theBenchmark.p
% 77.32/77.64 Solved 1 out of 1.
% 77.32/77.64 # Problem is unsatisfiable (or provable), constructing proof object
% 77.32/77.64 # SZS status Theorem
% 77.32/77.64 # SZS output start CNFRefutation.
% See solution above
% 77.41/77.68 # SZS output end CNFRefutation
%------------------------------------------------------------------------------