%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR163+1 : TPTP v7.3.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sine.py -e eprover -t %d %s
% Computer : n189.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 174.66s
% Output : CNFRefutation 174.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 12
% Syntax : Number of formulae : 80 ( 19 unt; 0 def)
% Number of atoms : 727 ( 1 equ)
% Maximal formula atoms : 110 ( 9 avg)
% Number of connectives : 969 ( 322 ~; 322 |; 306 &)
% ( 12 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 68 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 1 prp; 0-7 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-2 aty)
% Number of variables : 365 ( 13 sgn 308 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(642,axiom,
p__d__subclass(c__Covering,c__Putting),
file('/export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_5',mergeA2483) ).
fof(643,axiom,
p__d__partition3(c__Physical,c__Object,c__Process),
file('/export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_5',mergeA179) ).
fof(1250,axiom,
! [X12,X13] :
( p__path(X12,X13)
=> ( p__d__instance(X13,c__Object)
& p__d__instance(X12,c__Motion) ) ),
file('/export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_5',typeA38) ).
fof(1790,axiom,
! [X26] :
( p__d__instance(X26,c__Translocation)
=> ? [X9,X60,X61] :
( p__d__instance(X9,c__Object)
& p__d__instance(X60,c__Object)
& p__d__instance(X61,c__Object)
& p__path(X26,X61)
& p__origin(X26,X9)
& p__destination(X26,X60) ) ),
file('/export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_5',mergeA2507) ).
fof(2420,axiom,
! [X12,X13] :
( p__origin(X12,X13)
=> ( p__d__instance(X13,c__Object)
& p__d__instance(X12,c__Process) ) ),
file('/export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_5',typeA33) ).
fof(2560,axiom,
p__d__subclass(c__Transfer,c__Translocation),
file('/export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_5',mergeA2472) ).
fof(3064,axiom,
( ! [X161,X657,X658] :
( p__d__partition3(X161,X657,X658)
<=> ( p__d__exhaustiveDecomposition3(X161,X657,X658)
& p__d__disjointDecomposition3(X161,X657,X658) ) )
& ! [X161,X657,X658,X659] :
( p__d__partition4(X161,X657,X658,X659)
<=> ( p__d__exhaustiveDecomposition4(X161,X657,X658,X659)
& p__d__disjointDecomposition4(X161,X657,X658,X659) ) )
& ! [X161,X657,X658,X659,X660] :
( p__d__partition5(X161,X657,X658,X659,X660)
<=> ( p__d__exhaustiveDecomposition5(X161,X657,X658,X659,X660)
& p__d__disjointDecomposition5(X161,X657,X658,X659,X660) ) )
& ! [X161,X657,X658,X659,X660,X661] :
( p__d__partition6(X161,X657,X658,X659,X660,X661)
<=> ( p__d__exhaustiveDecomposition6(X161,X657,X658,X659,X660,X661)
& p__d__disjointDecomposition6(X161,X657,X658,X659,X660,X661) ) )
& ! [X161,X657,X658,X659,X660,X661,X662] :
( p__d__partition7(X161,X657,X658,X659,X660,X661,X662)
<=> ( p__d__exhaustiveDecomposition7(X161,X657,X658,X659,X660,X661,X662)
& p__d__disjointDecomposition7(X161,X657,X658,X659,X660,X661,X662) ) ) ),
file('/export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_5',predefinitionsA18) ).
fof(3066,axiom,
! [X139,X138] :
( p__d__disjoint(X139,X138)
<=> ! [X143] :
( ~ p__d__instance(X143,X139)
| ~ p__d__instance(X143,X138) ) ),
file('/export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_5',predefinitionsA15) ).
fof(3067,axiom,
! [X50,X175,X176] :
( ( p__d__instance(X50,X175)
& p__d__subclass(X175,X176) )
=> p__d__instance(X50,X176) ),
file('/export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_5',predefinitionsA12) ).
fof(3316,axiom,
( ! [X161,X657,X658] :
( p__d__disjointDecomposition3(X161,X657,X658)
<=> p__d__disjoint(X657,X658) )
& ! [X161,X657,X658,X659] :
( p__d__disjointDecomposition4(X161,X657,X658,X659)
<=> ( p__d__disjoint(X657,X658)
& p__d__disjoint(X657,X659)
& p__d__disjoint(X658,X659) ) )
& ! [X161,X657,X658,X659,X660] :
( p__d__disjointDecomposition5(X161,X657,X658,X659,X660)
<=> ( p__d__disjoint(X657,X658)
& p__d__disjoint(X657,X659)
& p__d__disjoint(X657,X660)
& p__d__disjoint(X658,X659)
& p__d__disjoint(X658,X660)
& p__d__disjoint(X659,X660) ) )
& ! [X161,X657,X658,X659,X660,X661] :
( p__d__disjointDecomposition6(X161,X657,X658,X659,X660,X661)
<=> ( p__d__disjoint(X657,X658)
& p__d__disjoint(X657,X659)
& p__d__disjoint(X657,X660)
& p__d__disjoint(X657,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) ) )
& ! [X161,X657,X658,X659,X660,X661,X662] :
( p__d__disjointDecomposition7(X161,X657,X658,X659,X660,X661,X662)
<=> ( p__d__disjoint(X657,X658)
& p__d__disjoint(X657,X659)
& p__d__disjoint(X657,X660)
& p__d__disjoint(X657,X661)
& p__d__disjoint(X657,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) ) ) ),
file('/export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_5',predefinitionsA24) ).
fof(3317,axiom,
p__d__subclass(c__Putting,c__Transfer),
file('/export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_5',mergeA2481) ).
fof(3403,conjecture,
? [X50] :
( ~ p__d__instance(X50,c__Putting)
& ! [X175] :
( p__d__instance(X175,c__Covering)
=> ~ equal(X50,X175) ) ),
file('/export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_5',antonymPattern20302) ).
fof(3404,negated_conjecture,
~ ? [X50] :
( ~ p__d__instance(X50,c__Putting)
& ! [X175] :
( p__d__instance(X175,c__Covering)
=> ~ equal(X50,X175) ) ),
inference(assume_negation,[status(cth)],[3403]) ).
fof(3479,plain,
! [X139,X138] :
( p__d__disjoint(X139,X138)
<=> ! [X143] :
( ~ p__d__instance(X143,X139)
| ~ p__d__instance(X143,X138) ) ),
inference(fof_simplification,[status(thm)],[3066,theory(equality)]) ).
fof(3494,negated_conjecture,
~ ? [X50] :
( ~ p__d__instance(X50,c__Putting)
& ! [X175] :
( p__d__instance(X175,c__Covering)
=> ~ equal(X50,X175) ) ),
inference(fof_simplification,[status(thm)],[3404,theory(equality)]) ).
cnf(5206,plain,
p__d__subclass(c__Covering,c__Putting),
inference(split_conjunct,[status(thm)],[642]) ).
cnf(5207,plain,
p__d__partition3(c__Physical,c__Object,c__Process),
inference(split_conjunct,[status(thm)],[643]) ).
fof(6874,plain,
! [X12,X13] :
( ~ p__path(X12,X13)
| ( p__d__instance(X13,c__Object)
& p__d__instance(X12,c__Motion) ) ),
inference(fof_nnf,[status(thm)],[1250]) ).
fof(6875,plain,
! [X14,X15] :
( ~ p__path(X14,X15)
| ( p__d__instance(X15,c__Object)
& p__d__instance(X14,c__Motion) ) ),
inference(variable_rename,[status(thm)],[6874]) ).
fof(6876,plain,
! [X14,X15] :
( ( p__d__instance(X15,c__Object)
| ~ p__path(X14,X15) )
& ( p__d__instance(X14,c__Motion)
| ~ p__path(X14,X15) ) ),
inference(distribute,[status(thm)],[6875]) ).
cnf(6878,plain,
( p__d__instance(X2,c__Object)
| ~ p__path(X1,X2) ),
inference(split_conjunct,[status(thm)],[6876]) ).
fof(8404,plain,
! [X26] :
( ~ p__d__instance(X26,c__Translocation)
| ? [X9,X60,X61] :
( p__d__instance(X9,c__Object)
& p__d__instance(X60,c__Object)
& p__d__instance(X61,c__Object)
& p__path(X26,X61)
& p__origin(X26,X9)
& p__destination(X26,X60) ) ),
inference(fof_nnf,[status(thm)],[1790]) ).
fof(8405,plain,
! [X62] :
( ~ p__d__instance(X62,c__Translocation)
| ? [X63,X64,X65] :
( p__d__instance(X63,c__Object)
& p__d__instance(X64,c__Object)
& p__d__instance(X65,c__Object)
& p__path(X62,X65)
& p__origin(X62,X63)
& p__destination(X62,X64) ) ),
inference(variable_rename,[status(thm)],[8404]) ).
fof(8406,plain,
! [X62] :
( ~ p__d__instance(X62,c__Translocation)
| ( p__d__instance(esk351_1(X62),c__Object)
& p__d__instance(esk352_1(X62),c__Object)
& p__d__instance(esk353_1(X62),c__Object)
& p__path(X62,esk353_1(X62))
& p__origin(X62,esk351_1(X62))
& p__destination(X62,esk352_1(X62)) ) ),
inference(skolemize,[status(esa)],[8405]) ).
fof(8407,plain,
! [X62] :
( ( p__d__instance(esk351_1(X62),c__Object)
| ~ p__d__instance(X62,c__Translocation) )
& ( p__d__instance(esk352_1(X62),c__Object)
| ~ p__d__instance(X62,c__Translocation) )
& ( p__d__instance(esk353_1(X62),c__Object)
| ~ p__d__instance(X62,c__Translocation) )
& ( p__path(X62,esk353_1(X62))
| ~ p__d__instance(X62,c__Translocation) )
& ( p__origin(X62,esk351_1(X62))
| ~ p__d__instance(X62,c__Translocation) )
& ( p__destination(X62,esk352_1(X62))
| ~ p__d__instance(X62,c__Translocation) ) ),
inference(distribute,[status(thm)],[8406]) ).
cnf(8409,plain,
( p__origin(X1,esk351_1(X1))
| ~ p__d__instance(X1,c__Translocation) ),
inference(split_conjunct,[status(thm)],[8407]) ).
cnf(8410,plain,
( p__path(X1,esk353_1(X1))
| ~ p__d__instance(X1,c__Translocation) ),
inference(split_conjunct,[status(thm)],[8407]) ).
fof(10193,plain,
! [X12,X13] :
( ~ p__origin(X12,X13)
| ( p__d__instance(X13,c__Object)
& p__d__instance(X12,c__Process) ) ),
inference(fof_nnf,[status(thm)],[2420]) ).
fof(10194,plain,
! [X14,X15] :
( ~ p__origin(X14,X15)
| ( p__d__instance(X15,c__Object)
& p__d__instance(X14,c__Process) ) ),
inference(variable_rename,[status(thm)],[10193]) ).
fof(10195,plain,
! [X14,X15] :
( ( p__d__instance(X15,c__Object)
| ~ p__origin(X14,X15) )
& ( p__d__instance(X14,c__Process)
| ~ p__origin(X14,X15) ) ),
inference(distribute,[status(thm)],[10194]) ).
cnf(10196,plain,
( p__d__instance(X1,c__Process)
| ~ p__origin(X1,X2) ),
inference(split_conjunct,[status(thm)],[10195]) ).
cnf(10597,plain,
p__d__subclass(c__Transfer,c__Translocation),
inference(split_conjunct,[status(thm)],[2560]) ).
fof(12074,plain,
( ! [X161,X657,X658] :
( ( ~ p__d__partition3(X161,X657,X658)
| ( p__d__exhaustiveDecomposition3(X161,X657,X658)
& p__d__disjointDecomposition3(X161,X657,X658) ) )
& ( ~ p__d__exhaustiveDecomposition3(X161,X657,X658)
| ~ p__d__disjointDecomposition3(X161,X657,X658)
| p__d__partition3(X161,X657,X658) ) )
& ! [X161,X657,X658,X659] :
( ( ~ p__d__partition4(X161,X657,X658,X659)
| ( p__d__exhaustiveDecomposition4(X161,X657,X658,X659)
& p__d__disjointDecomposition4(X161,X657,X658,X659) ) )
& ( ~ p__d__exhaustiveDecomposition4(X161,X657,X658,X659)
| ~ p__d__disjointDecomposition4(X161,X657,X658,X659)
| p__d__partition4(X161,X657,X658,X659) ) )
& ! [X161,X657,X658,X659,X660] :
( ( ~ p__d__partition5(X161,X657,X658,X659,X660)
| ( p__d__exhaustiveDecomposition5(X161,X657,X658,X659,X660)
& p__d__disjointDecomposition5(X161,X657,X658,X659,X660) ) )
& ( ~ p__d__exhaustiveDecomposition5(X161,X657,X658,X659,X660)
| ~ p__d__disjointDecomposition5(X161,X657,X658,X659,X660)
| p__d__partition5(X161,X657,X658,X659,X660) ) )
& ! [X161,X657,X658,X659,X660,X661] :
( ( ~ p__d__partition6(X161,X657,X658,X659,X660,X661)
| ( p__d__exhaustiveDecomposition6(X161,X657,X658,X659,X660,X661)
& p__d__disjointDecomposition6(X161,X657,X658,X659,X660,X661) ) )
& ( ~ p__d__exhaustiveDecomposition6(X161,X657,X658,X659,X660,X661)
| ~ p__d__disjointDecomposition6(X161,X657,X658,X659,X660,X661)
| p__d__partition6(X161,X657,X658,X659,X660,X661) ) )
& ! [X161,X657,X658,X659,X660,X661,X662] :
( ( ~ p__d__partition7(X161,X657,X658,X659,X660,X661,X662)
| ( p__d__exhaustiveDecomposition7(X161,X657,X658,X659,X660,X661,X662)
& p__d__disjointDecomposition7(X161,X657,X658,X659,X660,X661,X662) ) )
& ( ~ p__d__exhaustiveDecomposition7(X161,X657,X658,X659,X660,X661,X662)
| ~ p__d__disjointDecomposition7(X161,X657,X658,X659,X660,X661,X662)
| p__d__partition7(X161,X657,X658,X659,X660,X661,X662) ) ) ),
inference(fof_nnf,[status(thm)],[3064]) ).
fof(12075,plain,
( ! [X663,X664,X665] :
( ( ~ p__d__partition3(X663,X664,X665)
| ( p__d__exhaustiveDecomposition3(X663,X664,X665)
& p__d__disjointDecomposition3(X663,X664,X665) ) )
& ( ~ p__d__exhaustiveDecomposition3(X663,X664,X665)
| ~ p__d__disjointDecomposition3(X663,X664,X665)
| p__d__partition3(X663,X664,X665) ) )
& ! [X666,X667,X668,X669] :
( ( ~ p__d__partition4(X666,X667,X668,X669)
| ( p__d__exhaustiveDecomposition4(X666,X667,X668,X669)
& p__d__disjointDecomposition4(X666,X667,X668,X669) ) )
& ( ~ p__d__exhaustiveDecomposition4(X666,X667,X668,X669)
| ~ p__d__disjointDecomposition4(X666,X667,X668,X669)
| p__d__partition4(X666,X667,X668,X669) ) )
& ! [X670,X671,X672,X673,X674] :
( ( ~ p__d__partition5(X670,X671,X672,X673,X674)
| ( p__d__exhaustiveDecomposition5(X670,X671,X672,X673,X674)
& p__d__disjointDecomposition5(X670,X671,X672,X673,X674) ) )
& ( ~ p__d__exhaustiveDecomposition5(X670,X671,X672,X673,X674)
| ~ p__d__disjointDecomposition5(X670,X671,X672,X673,X674)
| p__d__partition5(X670,X671,X672,X673,X674) ) )
& ! [X675,X676,X677,X678,X679,X680] :
( ( ~ p__d__partition6(X675,X676,X677,X678,X679,X680)
| ( p__d__exhaustiveDecomposition6(X675,X676,X677,X678,X679,X680)
& p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680) ) )
& ( ~ p__d__exhaustiveDecomposition6(X675,X676,X677,X678,X679,X680)
| ~ p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680)
| p__d__partition6(X675,X676,X677,X678,X679,X680) ) )
& ! [X681,X682,X683,X684,X685,X686,X687] :
( ( ~ p__d__partition7(X681,X682,X683,X684,X685,X686,X687)
| ( p__d__exhaustiveDecomposition7(X681,X682,X683,X684,X685,X686,X687)
& p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) ) )
& ( ~ p__d__exhaustiveDecomposition7(X681,X682,X683,X684,X685,X686,X687)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687)
| p__d__partition7(X681,X682,X683,X684,X685,X686,X687) ) ) ),
inference(variable_rename,[status(thm)],[12074]) ).
fof(12076,plain,
! [X663,X664,X665,X666,X667,X668,X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687] :
( ( ~ p__d__partition7(X681,X682,X683,X684,X685,X686,X687)
| ( p__d__exhaustiveDecomposition7(X681,X682,X683,X684,X685,X686,X687)
& p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) ) )
& ( ~ p__d__exhaustiveDecomposition7(X681,X682,X683,X684,X685,X686,X687)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687)
| p__d__partition7(X681,X682,X683,X684,X685,X686,X687) )
& ( ~ p__d__partition6(X675,X676,X677,X678,X679,X680)
| ( p__d__exhaustiveDecomposition6(X675,X676,X677,X678,X679,X680)
& p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680) ) )
& ( ~ p__d__exhaustiveDecomposition6(X675,X676,X677,X678,X679,X680)
| ~ p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680)
| p__d__partition6(X675,X676,X677,X678,X679,X680) )
& ( ~ p__d__partition5(X670,X671,X672,X673,X674)
| ( p__d__exhaustiveDecomposition5(X670,X671,X672,X673,X674)
& p__d__disjointDecomposition5(X670,X671,X672,X673,X674) ) )
& ( ~ p__d__exhaustiveDecomposition5(X670,X671,X672,X673,X674)
| ~ p__d__disjointDecomposition5(X670,X671,X672,X673,X674)
| p__d__partition5(X670,X671,X672,X673,X674) )
& ( ~ p__d__partition4(X666,X667,X668,X669)
| ( p__d__exhaustiveDecomposition4(X666,X667,X668,X669)
& p__d__disjointDecomposition4(X666,X667,X668,X669) ) )
& ( ~ p__d__exhaustiveDecomposition4(X666,X667,X668,X669)
| ~ p__d__disjointDecomposition4(X666,X667,X668,X669)
| p__d__partition4(X666,X667,X668,X669) )
& ( ~ p__d__partition3(X663,X664,X665)
| ( p__d__exhaustiveDecomposition3(X663,X664,X665)
& p__d__disjointDecomposition3(X663,X664,X665) ) )
& ( ~ p__d__exhaustiveDecomposition3(X663,X664,X665)
| ~ p__d__disjointDecomposition3(X663,X664,X665)
| p__d__partition3(X663,X664,X665) ) ),
inference(shift_quantors,[status(thm)],[12075]) ).
fof(12077,plain,
! [X663,X664,X665,X666,X667,X668,X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687] :
( ( p__d__exhaustiveDecomposition7(X681,X682,X683,X684,X685,X686,X687)
| ~ p__d__partition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687)
| ~ p__d__partition7(X681,X682,X683,X684,X685,X686,X687) )
& ( ~ p__d__exhaustiveDecomposition7(X681,X682,X683,X684,X685,X686,X687)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687)
| p__d__partition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__exhaustiveDecomposition6(X675,X676,X677,X678,X679,X680)
| ~ p__d__partition6(X675,X676,X677,X678,X679,X680) )
& ( p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680)
| ~ p__d__partition6(X675,X676,X677,X678,X679,X680) )
& ( ~ p__d__exhaustiveDecomposition6(X675,X676,X677,X678,X679,X680)
| ~ p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680)
| p__d__partition6(X675,X676,X677,X678,X679,X680) )
& ( p__d__exhaustiveDecomposition5(X670,X671,X672,X673,X674)
| ~ p__d__partition5(X670,X671,X672,X673,X674) )
& ( p__d__disjointDecomposition5(X670,X671,X672,X673,X674)
| ~ p__d__partition5(X670,X671,X672,X673,X674) )
& ( ~ p__d__exhaustiveDecomposition5(X670,X671,X672,X673,X674)
| ~ p__d__disjointDecomposition5(X670,X671,X672,X673,X674)
| p__d__partition5(X670,X671,X672,X673,X674) )
& ( p__d__exhaustiveDecomposition4(X666,X667,X668,X669)
| ~ p__d__partition4(X666,X667,X668,X669) )
& ( p__d__disjointDecomposition4(X666,X667,X668,X669)
| ~ p__d__partition4(X666,X667,X668,X669) )
& ( ~ p__d__exhaustiveDecomposition4(X666,X667,X668,X669)
| ~ p__d__disjointDecomposition4(X666,X667,X668,X669)
| p__d__partition4(X666,X667,X668,X669) )
& ( p__d__exhaustiveDecomposition3(X663,X664,X665)
| ~ p__d__partition3(X663,X664,X665) )
& ( p__d__disjointDecomposition3(X663,X664,X665)
| ~ p__d__partition3(X663,X664,X665) )
& ( ~ p__d__exhaustiveDecomposition3(X663,X664,X665)
| ~ p__d__disjointDecomposition3(X663,X664,X665)
| p__d__partition3(X663,X664,X665) ) ),
inference(distribute,[status(thm)],[12076]) ).
cnf(12079,plain,
( p__d__disjointDecomposition3(X1,X2,X3)
| ~ p__d__partition3(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[12077]) ).
fof(12094,plain,
! [X139,X138] :
( ( ~ p__d__disjoint(X139,X138)
| ! [X143] :
( ~ p__d__instance(X143,X139)
| ~ p__d__instance(X143,X138) ) )
& ( ? [X143] :
( p__d__instance(X143,X139)
& p__d__instance(X143,X138) )
| p__d__disjoint(X139,X138) ) ),
inference(fof_nnf,[status(thm)],[3479]) ).
fof(12095,plain,
! [X144,X145] :
( ( ~ p__d__disjoint(X144,X145)
| ! [X146] :
( ~ p__d__instance(X146,X144)
| ~ p__d__instance(X146,X145) ) )
& ( ? [X147] :
( p__d__instance(X147,X144)
& p__d__instance(X147,X145) )
| p__d__disjoint(X144,X145) ) ),
inference(variable_rename,[status(thm)],[12094]) ).
fof(12096,plain,
! [X144,X145] :
( ( ~ p__d__disjoint(X144,X145)
| ! [X146] :
( ~ p__d__instance(X146,X144)
| ~ p__d__instance(X146,X145) ) )
& ( ( p__d__instance(esk634_2(X144,X145),X144)
& p__d__instance(esk634_2(X144,X145),X145) )
| p__d__disjoint(X144,X145) ) ),
inference(skolemize,[status(esa)],[12095]) ).
fof(12097,plain,
! [X144,X145,X146] :
( ( ~ p__d__instance(X146,X144)
| ~ p__d__instance(X146,X145)
| ~ p__d__disjoint(X144,X145) )
& ( ( p__d__instance(esk634_2(X144,X145),X144)
& p__d__instance(esk634_2(X144,X145),X145) )
| p__d__disjoint(X144,X145) ) ),
inference(shift_quantors,[status(thm)],[12096]) ).
fof(12098,plain,
! [X144,X145,X146] :
( ( ~ p__d__instance(X146,X144)
| ~ p__d__instance(X146,X145)
| ~ p__d__disjoint(X144,X145) )
& ( p__d__instance(esk634_2(X144,X145),X144)
| p__d__disjoint(X144,X145) )
& ( p__d__instance(esk634_2(X144,X145),X145)
| p__d__disjoint(X144,X145) ) ),
inference(distribute,[status(thm)],[12097]) ).
cnf(12101,plain,
( ~ p__d__disjoint(X1,X2)
| ~ p__d__instance(X3,X2)
| ~ p__d__instance(X3,X1) ),
inference(split_conjunct,[status(thm)],[12098]) ).
fof(12102,plain,
! [X50,X175,X176] :
( ~ p__d__instance(X50,X175)
| ~ p__d__subclass(X175,X176)
| p__d__instance(X50,X176) ),
inference(fof_nnf,[status(thm)],[3067]) ).
fof(12103,plain,
! [X177,X178,X179] :
( ~ p__d__instance(X177,X178)
| ~ p__d__subclass(X178,X179)
| p__d__instance(X177,X179) ),
inference(variable_rename,[status(thm)],[12102]) ).
cnf(12104,plain,
( p__d__instance(X1,X2)
| ~ p__d__subclass(X3,X2)
| ~ p__d__instance(X1,X3) ),
inference(split_conjunct,[status(thm)],[12103]) ).
fof(12859,plain,
( ! [X161,X657,X658] :
( ( ~ p__d__disjointDecomposition3(X161,X657,X658)
| p__d__disjoint(X657,X658) )
& ( ~ p__d__disjoint(X657,X658)
| p__d__disjointDecomposition3(X161,X657,X658) ) )
& ! [X161,X657,X658,X659] :
( ( ~ p__d__disjointDecomposition4(X161,X657,X658,X659)
| ( p__d__disjoint(X657,X658)
& p__d__disjoint(X657,X659)
& p__d__disjoint(X658,X659) ) )
& ( ~ p__d__disjoint(X657,X658)
| ~ p__d__disjoint(X657,X659)
| ~ p__d__disjoint(X658,X659)
| p__d__disjointDecomposition4(X161,X657,X658,X659) ) )
& ! [X161,X657,X658,X659,X660] :
( ( ~ p__d__disjointDecomposition5(X161,X657,X658,X659,X660)
| ( p__d__disjoint(X657,X658)
& p__d__disjoint(X657,X659)
& p__d__disjoint(X657,X660)
& p__d__disjoint(X658,X659)
& p__d__disjoint(X658,X660)
& p__d__disjoint(X659,X660) ) )
& ( ~ p__d__disjoint(X657,X658)
| ~ p__d__disjoint(X657,X659)
| ~ p__d__disjoint(X657,X660)
| ~ p__d__disjoint(X658,X659)
| ~ p__d__disjoint(X658,X660)
| ~ p__d__disjoint(X659,X660)
| p__d__disjointDecomposition5(X161,X657,X658,X659,X660) ) )
& ! [X161,X657,X658,X659,X660,X661] :
( ( ~ p__d__disjointDecomposition6(X161,X657,X658,X659,X660,X661)
| ( p__d__disjoint(X657,X658)
& p__d__disjoint(X657,X659)
& p__d__disjoint(X657,X660)
& p__d__disjoint(X657,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(X657,X658)
| ~ p__d__disjoint(X657,X659)
| ~ p__d__disjoint(X657,X660)
| ~ p__d__disjoint(X657,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__disjointDecomposition6(X161,X657,X658,X659,X660,X661) ) )
& ! [X161,X657,X658,X659,X660,X661,X662] :
( ( ~ p__d__disjointDecomposition7(X161,X657,X658,X659,X660,X661,X662)
| ( p__d__disjoint(X657,X658)
& p__d__disjoint(X657,X659)
& p__d__disjoint(X657,X660)
& p__d__disjoint(X657,X661)
& p__d__disjoint(X657,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(X657,X658)
| ~ p__d__disjoint(X657,X659)
| ~ p__d__disjoint(X657,X660)
| ~ p__d__disjoint(X657,X661)
| ~ p__d__disjoint(X657,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__disjointDecomposition7(X161,X657,X658,X659,X660,X661,X662) ) ) ),
inference(fof_nnf,[status(thm)],[3316]) ).
fof(12860,plain,
( ! [X663,X664,X665] :
( ( ~ p__d__disjointDecomposition3(X663,X664,X665)
| p__d__disjoint(X664,X665) )
& ( ~ p__d__disjoint(X664,X665)
| p__d__disjointDecomposition3(X663,X664,X665) ) )
& ! [X666,X667,X668,X669] :
( ( ~ p__d__disjointDecomposition4(X666,X667,X668,X669)
| ( p__d__disjoint(X667,X668)
& p__d__disjoint(X667,X669)
& p__d__disjoint(X668,X669) ) )
& ( ~ p__d__disjoint(X667,X668)
| ~ p__d__disjoint(X667,X669)
| ~ p__d__disjoint(X668,X669)
| p__d__disjointDecomposition4(X666,X667,X668,X669) ) )
& ! [X670,X671,X672,X673,X674] :
( ( ~ p__d__disjointDecomposition5(X670,X671,X672,X673,X674)
| ( p__d__disjoint(X671,X672)
& p__d__disjoint(X671,X673)
& p__d__disjoint(X671,X674)
& p__d__disjoint(X672,X673)
& p__d__disjoint(X672,X674)
& p__d__disjoint(X673,X674) ) )
& ( ~ p__d__disjoint(X671,X672)
| ~ p__d__disjoint(X671,X673)
| ~ p__d__disjoint(X671,X674)
| ~ p__d__disjoint(X672,X673)
| ~ p__d__disjoint(X672,X674)
| ~ p__d__disjoint(X673,X674)
| p__d__disjointDecomposition5(X670,X671,X672,X673,X674) ) )
& ! [X675,X676,X677,X678,X679,X680] :
( ( ~ p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680)
| ( p__d__disjoint(X676,X677)
& p__d__disjoint(X676,X678)
& p__d__disjoint(X676,X679)
& p__d__disjoint(X676,X680)
& p__d__disjoint(X677,X678)
& p__d__disjoint(X677,X679)
& p__d__disjoint(X677,X680)
& p__d__disjoint(X678,X679)
& p__d__disjoint(X678,X680)
& p__d__disjoint(X679,X680) ) )
& ( ~ p__d__disjoint(X676,X677)
| ~ p__d__disjoint(X676,X678)
| ~ p__d__disjoint(X676,X679)
| ~ p__d__disjoint(X676,X680)
| ~ p__d__disjoint(X677,X678)
| ~ p__d__disjoint(X677,X679)
| ~ p__d__disjoint(X677,X680)
| ~ p__d__disjoint(X678,X679)
| ~ p__d__disjoint(X678,X680)
| ~ p__d__disjoint(X679,X680)
| p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680) ) )
& ! [X681,X682,X683,X684,X685,X686,X687] :
( ( ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687)
| ( p__d__disjoint(X682,X683)
& p__d__disjoint(X682,X684)
& p__d__disjoint(X682,X685)
& p__d__disjoint(X682,X686)
& p__d__disjoint(X682,X687)
& p__d__disjoint(X683,X684)
& p__d__disjoint(X683,X685)
& p__d__disjoint(X683,X686)
& p__d__disjoint(X683,X687)
& p__d__disjoint(X684,X685)
& p__d__disjoint(X684,X686)
& p__d__disjoint(X684,X687)
& p__d__disjoint(X685,X686)
& p__d__disjoint(X685,X687)
& p__d__disjoint(X686,X687) ) )
& ( ~ p__d__disjoint(X682,X683)
| ~ p__d__disjoint(X682,X684)
| ~ p__d__disjoint(X682,X685)
| ~ p__d__disjoint(X682,X686)
| ~ p__d__disjoint(X682,X687)
| ~ p__d__disjoint(X683,X684)
| ~ p__d__disjoint(X683,X685)
| ~ p__d__disjoint(X683,X686)
| ~ p__d__disjoint(X683,X687)
| ~ p__d__disjoint(X684,X685)
| ~ p__d__disjoint(X684,X686)
| ~ p__d__disjoint(X684,X687)
| ~ p__d__disjoint(X685,X686)
| ~ p__d__disjoint(X685,X687)
| ~ p__d__disjoint(X686,X687)
| p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) ) ) ),
inference(variable_rename,[status(thm)],[12859]) ).
fof(12861,plain,
! [X663,X664,X665,X666,X667,X668,X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687] :
( ( ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687)
| ( p__d__disjoint(X682,X683)
& p__d__disjoint(X682,X684)
& p__d__disjoint(X682,X685)
& p__d__disjoint(X682,X686)
& p__d__disjoint(X682,X687)
& p__d__disjoint(X683,X684)
& p__d__disjoint(X683,X685)
& p__d__disjoint(X683,X686)
& p__d__disjoint(X683,X687)
& p__d__disjoint(X684,X685)
& p__d__disjoint(X684,X686)
& p__d__disjoint(X684,X687)
& p__d__disjoint(X685,X686)
& p__d__disjoint(X685,X687)
& p__d__disjoint(X686,X687) ) )
& ( ~ p__d__disjoint(X682,X683)
| ~ p__d__disjoint(X682,X684)
| ~ p__d__disjoint(X682,X685)
| ~ p__d__disjoint(X682,X686)
| ~ p__d__disjoint(X682,X687)
| ~ p__d__disjoint(X683,X684)
| ~ p__d__disjoint(X683,X685)
| ~ p__d__disjoint(X683,X686)
| ~ p__d__disjoint(X683,X687)
| ~ p__d__disjoint(X684,X685)
| ~ p__d__disjoint(X684,X686)
| ~ p__d__disjoint(X684,X687)
| ~ p__d__disjoint(X685,X686)
| ~ p__d__disjoint(X685,X687)
| ~ p__d__disjoint(X686,X687)
| p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( ~ p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680)
| ( p__d__disjoint(X676,X677)
& p__d__disjoint(X676,X678)
& p__d__disjoint(X676,X679)
& p__d__disjoint(X676,X680)
& p__d__disjoint(X677,X678)
& p__d__disjoint(X677,X679)
& p__d__disjoint(X677,X680)
& p__d__disjoint(X678,X679)
& p__d__disjoint(X678,X680)
& p__d__disjoint(X679,X680) ) )
& ( ~ p__d__disjoint(X676,X677)
| ~ p__d__disjoint(X676,X678)
| ~ p__d__disjoint(X676,X679)
| ~ p__d__disjoint(X676,X680)
| ~ p__d__disjoint(X677,X678)
| ~ p__d__disjoint(X677,X679)
| ~ p__d__disjoint(X677,X680)
| ~ p__d__disjoint(X678,X679)
| ~ p__d__disjoint(X678,X680)
| ~ p__d__disjoint(X679,X680)
| p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680) )
& ( ~ p__d__disjointDecomposition5(X670,X671,X672,X673,X674)
| ( p__d__disjoint(X671,X672)
& p__d__disjoint(X671,X673)
& p__d__disjoint(X671,X674)
& p__d__disjoint(X672,X673)
& p__d__disjoint(X672,X674)
& p__d__disjoint(X673,X674) ) )
& ( ~ p__d__disjoint(X671,X672)
| ~ p__d__disjoint(X671,X673)
| ~ p__d__disjoint(X671,X674)
| ~ p__d__disjoint(X672,X673)
| ~ p__d__disjoint(X672,X674)
| ~ p__d__disjoint(X673,X674)
| p__d__disjointDecomposition5(X670,X671,X672,X673,X674) )
& ( ~ p__d__disjointDecomposition4(X666,X667,X668,X669)
| ( p__d__disjoint(X667,X668)
& p__d__disjoint(X667,X669)
& p__d__disjoint(X668,X669) ) )
& ( ~ p__d__disjoint(X667,X668)
| ~ p__d__disjoint(X667,X669)
| ~ p__d__disjoint(X668,X669)
| p__d__disjointDecomposition4(X666,X667,X668,X669) )
& ( ~ p__d__disjointDecomposition3(X663,X664,X665)
| p__d__disjoint(X664,X665) )
& ( ~ p__d__disjoint(X664,X665)
| p__d__disjointDecomposition3(X663,X664,X665) ) ),
inference(shift_quantors,[status(thm)],[12860]) ).
fof(12862,plain,
! [X663,X664,X665,X666,X667,X668,X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687] :
( ( p__d__disjoint(X682,X683)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjoint(X682,X684)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjoint(X682,X685)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjoint(X682,X686)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjoint(X682,X687)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjoint(X683,X684)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjoint(X683,X685)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjoint(X683,X686)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjoint(X683,X687)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjoint(X684,X685)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjoint(X684,X686)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjoint(X684,X687)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjoint(X685,X686)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjoint(X685,X687)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjoint(X686,X687)
| ~ p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( ~ p__d__disjoint(X682,X683)
| ~ p__d__disjoint(X682,X684)
| ~ p__d__disjoint(X682,X685)
| ~ p__d__disjoint(X682,X686)
| ~ p__d__disjoint(X682,X687)
| ~ p__d__disjoint(X683,X684)
| ~ p__d__disjoint(X683,X685)
| ~ p__d__disjoint(X683,X686)
| ~ p__d__disjoint(X683,X687)
| ~ p__d__disjoint(X684,X685)
| ~ p__d__disjoint(X684,X686)
| ~ p__d__disjoint(X684,X687)
| ~ p__d__disjoint(X685,X686)
| ~ p__d__disjoint(X685,X687)
| ~ p__d__disjoint(X686,X687)
| p__d__disjointDecomposition7(X681,X682,X683,X684,X685,X686,X687) )
& ( p__d__disjoint(X676,X677)
| ~ p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X676,X678)
| ~ p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X676,X679)
| ~ p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X676,X680)
| ~ p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X677,X678)
| ~ p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X677,X679)
| ~ p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X677,X680)
| ~ p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X678,X679)
| ~ p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X678,X680)
| ~ p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X679,X680)
| ~ p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680) )
& ( ~ p__d__disjoint(X676,X677)
| ~ p__d__disjoint(X676,X678)
| ~ p__d__disjoint(X676,X679)
| ~ p__d__disjoint(X676,X680)
| ~ p__d__disjoint(X677,X678)
| ~ p__d__disjoint(X677,X679)
| ~ p__d__disjoint(X677,X680)
| ~ p__d__disjoint(X678,X679)
| ~ p__d__disjoint(X678,X680)
| ~ p__d__disjoint(X679,X680)
| p__d__disjointDecomposition6(X675,X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X671,X672)
| ~ p__d__disjointDecomposition5(X670,X671,X672,X673,X674) )
& ( p__d__disjoint(X671,X673)
| ~ p__d__disjointDecomposition5(X670,X671,X672,X673,X674) )
& ( p__d__disjoint(X671,X674)
| ~ p__d__disjointDecomposition5(X670,X671,X672,X673,X674) )
& ( p__d__disjoint(X672,X673)
| ~ p__d__disjointDecomposition5(X670,X671,X672,X673,X674) )
& ( p__d__disjoint(X672,X674)
| ~ p__d__disjointDecomposition5(X670,X671,X672,X673,X674) )
& ( p__d__disjoint(X673,X674)
| ~ p__d__disjointDecomposition5(X670,X671,X672,X673,X674) )
& ( ~ p__d__disjoint(X671,X672)
| ~ p__d__disjoint(X671,X673)
| ~ p__d__disjoint(X671,X674)
| ~ p__d__disjoint(X672,X673)
| ~ p__d__disjoint(X672,X674)
| ~ p__d__disjoint(X673,X674)
| p__d__disjointDecomposition5(X670,X671,X672,X673,X674) )
& ( p__d__disjoint(X667,X668)
| ~ p__d__disjointDecomposition4(X666,X667,X668,X669) )
& ( p__d__disjoint(X667,X669)
| ~ p__d__disjointDecomposition4(X666,X667,X668,X669) )
& ( p__d__disjoint(X668,X669)
| ~ p__d__disjointDecomposition4(X666,X667,X668,X669) )
& ( ~ p__d__disjoint(X667,X668)
| ~ p__d__disjoint(X667,X669)
| ~ p__d__disjoint(X668,X669)
| p__d__disjointDecomposition4(X666,X667,X668,X669) )
& ( ~ p__d__disjointDecomposition3(X663,X664,X665)
| p__d__disjoint(X664,X665) )
& ( ~ p__d__disjoint(X664,X665)
| p__d__disjointDecomposition3(X663,X664,X665) ) ),
inference(distribute,[status(thm)],[12861]) ).
cnf(12864,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__disjointDecomposition3(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[12862]) ).
cnf(12903,plain,
p__d__subclass(c__Putting,c__Transfer),
inference(split_conjunct,[status(thm)],[3317]) ).
fof(13148,negated_conjecture,
! [X50] :
( p__d__instance(X50,c__Putting)
| ? [X175] :
( p__d__instance(X175,c__Covering)
& equal(X50,X175) ) ),
inference(fof_nnf,[status(thm)],[3494]) ).
fof(13149,negated_conjecture,
! [X176] :
( p__d__instance(X176,c__Putting)
| ? [X177] :
( p__d__instance(X177,c__Covering)
& equal(X176,X177) ) ),
inference(variable_rename,[status(thm)],[13148]) ).
fof(13150,negated_conjecture,
! [X176] :
( p__d__instance(X176,c__Putting)
| ( p__d__instance(esk706_1(X176),c__Covering)
& equal(X176,esk706_1(X176)) ) ),
inference(skolemize,[status(esa)],[13149]) ).
fof(13151,negated_conjecture,
! [X176] :
( ( p__d__instance(esk706_1(X176),c__Covering)
| p__d__instance(X176,c__Putting) )
& ( equal(X176,esk706_1(X176))
| p__d__instance(X176,c__Putting) ) ),
inference(distribute,[status(thm)],[13150]) ).
cnf(13152,negated_conjecture,
( p__d__instance(X1,c__Putting)
| X1 = esk706_1(X1) ),
inference(split_conjunct,[status(thm)],[13151]) ).
cnf(13153,negated_conjecture,
( p__d__instance(X1,c__Putting)
| p__d__instance(esk706_1(X1),c__Covering) ),
inference(split_conjunct,[status(thm)],[13151]) ).
cnf(13155,negated_conjecture,
( p__d__instance(X1,c__Covering)
| p__d__instance(X1,c__Putting) ),
inference(spm,[status(thm)],[13153,13152,theory(equality)]) ).
cnf(13648,plain,
( p__d__instance(X1,c__Putting)
| ~ p__d__instance(X1,c__Covering) ),
inference(spm,[status(thm)],[12104,5206,theory(equality)]) ).
cnf(13650,plain,
( p__d__instance(X1,c__Transfer)
| ~ p__d__instance(X1,c__Putting) ),
inference(spm,[status(thm)],[12104,12903,theory(equality)]) ).
cnf(13932,plain,
( p__d__instance(X1,c__Translocation)
| ~ p__d__instance(X1,c__Transfer) ),
inference(spm,[status(thm)],[12104,10597,theory(equality)]) ).
cnf(16698,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__partition3(X3,X1,X2) ),
inference(spm,[status(thm)],[12864,12079,theory(equality)]) ).
cnf(34053,plain,
p__d__instance(X1,c__Putting),
inference(csr,[status(thm)],[13648,13155]) ).
cnf(35542,plain,
( p__d__instance(X1,c__Transfer)
| $false ),
inference(rw,[status(thm)],[13650,34053,theory(equality)]) ).
cnf(35543,plain,
p__d__instance(X1,c__Transfer),
inference(cn,[status(thm)],[35542,theory(equality)]) ).
cnf(47080,plain,
( p__d__instance(X1,c__Translocation)
| $false ),
inference(rw,[status(thm)],[13932,35543,theory(equality)]) ).
cnf(47081,plain,
p__d__instance(X1,c__Translocation),
inference(cn,[status(thm)],[47080,theory(equality)]) ).
cnf(47141,plain,
( p__path(X1,esk353_1(X1))
| $false ),
inference(rw,[status(thm)],[8410,47081,theory(equality)]) ).
cnf(47142,plain,
p__path(X1,esk353_1(X1)),
inference(cn,[status(thm)],[47141,theory(equality)]) ).
cnf(47143,plain,
( p__origin(X1,esk351_1(X1))
| $false ),
inference(rw,[status(thm)],[8409,47081,theory(equality)]) ).
cnf(47144,plain,
p__origin(X1,esk351_1(X1)),
inference(cn,[status(thm)],[47143,theory(equality)]) ).
cnf(47160,plain,
p__d__instance(esk353_1(X1),c__Object),
inference(spm,[status(thm)],[6878,47142,theory(equality)]) ).
cnf(47207,plain,
p__d__instance(X1,c__Process),
inference(spm,[status(thm)],[10196,47144,theory(equality)]) ).
cnf(94056,plain,
p__d__disjoint(c__Object,c__Process),
inference(spm,[status(thm)],[16698,5207,theory(equality)]) ).
cnf(94190,plain,
( ~ p__d__instance(X1,c__Process)
| ~ p__d__instance(X1,c__Object) ),
inference(spm,[status(thm)],[12101,94056,theory(equality)]) ).
cnf(94191,plain,
( $false
| ~ p__d__instance(X1,c__Object) ),
inference(rw,[status(thm)],[94190,47207,theory(equality)]) ).
cnf(94192,plain,
~ p__d__instance(X1,c__Object),
inference(cn,[status(thm)],[94191,theory(equality)]) ).
cnf(94545,plain,
$false,
inference(sr,[status(thm)],[47160,94192,theory(equality)]) ).
cnf(94546,plain,
$false,
94545,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR163+1 : TPTP v7.3.0. Released v7.3.0.
% 0.00/0.05 % Command : sine.py -e eprover -t %d %s
% 0.03/0.25 % Computer : n189.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:43:11 CST 2019
% 0.03/0.25 % CPUTime :
% 0.03/0.30 % SZS status Started for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.30 --creating new selector for [CSR006+0.ax]
% 0.56/0.82 -running prover on /export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_1 with time limit 29
% 0.56/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/tmp2NJB09/sel_theBenchmark.p_1']
% 0.56/0.82 -prover status CounterSatisfiable
% 0.56/0.82 -running prover on /export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_2 with time limit 89
% 0.56/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/tmp2NJB09/sel_theBenchmark.p_2']
% 0.56/0.82 -prover status CounterSatisfiable
% 0.56/0.82 --creating new selector for [CSR006+0.ax]
% 0.71/0.98 -running prover on /export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_3 with time limit 119
% 0.71/0.98 -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/tmp2NJB09/sel_theBenchmark.p_3']
% 0.71/0.98 -prover status CounterSatisfiable
% 0.71/0.98 --creating new selector for [CSR006+0.ax]
% 149.89/150.46 eprover: CPU time limit exceeded, terminating
% 149.99/150.56 -running prover on /export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_4 with time limit 149
% 149.99/150.56 -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/tmp2NJB09/sel_theBenchmark.p_4']
% 149.99/150.56 -prover status ResourceOut
% 149.99/150.56 --creating new selector for [CSR006+0.ax]
% 174.66/175.35 -running prover on /export/starexec/sandbox/tmp/tmp2NJB09/sel_theBenchmark.p_5 with time limit 149
% 174.66/175.35 -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/tmp2NJB09/sel_theBenchmark.p_5']
% 174.66/175.35 -prover status Theorem
% 174.66/175.35 Problem theBenchmark.p solved in phase 4.
% 174.66/175.35 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 174.66/175.35 % SZS status Ended for /export/starexec/sandbox/benchmark/theBenchmark.p
% 174.66/175.35 Solved 1 out of 1.
% 174.66/175.35 # Problem is unsatisfiable (or provable), constructing proof object
% 174.66/175.35 # SZS status Theorem
% 174.66/175.35 # SZS output start CNFRefutation.
% See solution above
% 174.66/175.39 # SZS output end CNFRefutation
%------------------------------------------------------------------------------