%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR229+1 : TPTP v7.3.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sine.py -e eprover -t %d %s
% Computer : n183.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:21 EST 2019
% Result : Theorem 55.87s
% Output : CNFRefutation 55.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 26
% Syntax : Number of formulae : 158 ( 59 unt; 0 def)
% Number of atoms : 844 ( 14 equ)
% Maximal formula atoms : 110 ( 5 avg)
% Number of connectives : 1056 ( 370 ~; 364 |; 304 &)
% ( 13 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 68 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 1 prp; 0-7 aty)
% Number of functors : 28 ( 28 usr; 24 con; 0-2 aty)
% Number of variables : 395 ( 9 sgn 317 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(215,axiom,
p__subAttribute(c__Liquid,c__Fluid),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',mergeA3566) ).
fof(608,axiom,
p__d__subclass(c__SetOrClass,c__Abstract),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',mergeA573) ).
fof(612,axiom,
p__d__subclass(c__Class,c__SetOrClass),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',mergeA575) ).
fof(633,axiom,
! [X149] :
( p__d__instance(X149,c__Class)
<=> p__d__subclass(X149,c__Entity) ),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',mergeA177) ).
fof(636,axiom,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',mergeA173) ).
fof(837,axiom,
! [X149,X284,X285] :
( ( p__subAttribute(X284,X285)
& p__d__instance(X285,X149) )
=> p__d__instance(X284,X149) ),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',mergeA141) ).
fof(862,axiom,
p__subAttribute(c__Headache,c__Pain),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',miloA2799) ).
fof(863,axiom,
p__subAttribute(c__Pain,c__Unhappiness),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',miloA2798) ).
fof(1081,axiom,
! [X12,X13] :
( p__subAttribute(X12,X13)
=> ( p__d__instance(X13,c__Attribute)
& p__d__instance(X12,c__Attribute) ) ),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',typeA2) ).
fof(1142,axiom,
! [X37] : p__d__subclass(X37,X37),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',predefinitionsA7) ).
fof(1336,axiom,
p__subAttribute(c__Promise,c__Obligation),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',mergeA3551) ).
fof(1525,axiom,
! [X138,X137] :
( p__d__disjoint(X138,X137)
<=> ! [X240] :
( ~ p__d__instance(X240,X138)
| ~ p__d__instance(X240,X137) ) ),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',predefinitionsA15) ).
fof(1738,axiom,
p__d__subclass(c__Process,c__Physical),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',mergeA324) ).
fof(1785,axiom,
! [X141] :
( p__d__instance(X141,c__Translocation)
=> ? [X9,X54,X55] :
( p__d__instance(X9,c__Object)
& p__d__instance(X54,c__Object)
& p__d__instance(X55,c__Object)
& p__path(X141,X55)
& p__origin(X141,X9)
& p__destination(X141,X54) ) ),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',mergeA2507) ).
fof(1946,axiom,
p__d__disjointDecomposition6(c__Abstract,c__Quantity,c__Attribute,c__SetOrClass,c__Relation,c__Proposition),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',mergeA331) ).
fof(1948,axiom,
p__d__subclass(c__Attribute,c__Abstract),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',mergeA333) ).
fof(2415,axiom,
! [X12,X13] :
( p__destination(X12,X13)
=> p__d__instance(X12,c__Process) ),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',typeA31) ).
fof(2560,axiom,
p__d__subclass(c__Transfer,c__Translocation),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',mergeA2472) ).
fof(2728,axiom,
p__subAttribute(c__ServiceContract,c__Contract),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',miloA1957) ).
fof(2732,axiom,
p__subAttribute(c__Contract,c__Promise),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',miloA1950) ).
fof(2758,axiom,
p__d__subclass(c__Removing,c__Transfer),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',mergeA2477) ).
fof(3063,axiom,
( ! [X149,X663,X664] :
( p__d__partition3(X149,X663,X664)
<=> ( p__d__exhaustiveDecomposition3(X149,X663,X664)
& p__d__disjointDecomposition3(X149,X663,X664) ) )
& ! [X149,X663,X664,X665] :
( p__d__partition4(X149,X663,X664,X665)
<=> ( p__d__exhaustiveDecomposition4(X149,X663,X664,X665)
& p__d__disjointDecomposition4(X149,X663,X664,X665) ) )
& ! [X149,X663,X664,X665,X666] :
( p__d__partition5(X149,X663,X664,X665,X666)
<=> ( p__d__exhaustiveDecomposition5(X149,X663,X664,X665,X666)
& p__d__disjointDecomposition5(X149,X663,X664,X665,X666) ) )
& ! [X149,X663,X664,X665,X666,X667] :
( p__d__partition6(X149,X663,X664,X665,X666,X667)
<=> ( p__d__exhaustiveDecomposition6(X149,X663,X664,X665,X666,X667)
& p__d__disjointDecomposition6(X149,X663,X664,X665,X666,X667) ) )
& ! [X149,X663,X664,X665,X666,X667,X668] :
( p__d__partition7(X149,X663,X664,X665,X666,X667,X668)
<=> ( p__d__exhaustiveDecomposition7(X149,X663,X664,X665,X666,X667,X668)
& p__d__disjointDecomposition7(X149,X663,X664,X665,X666,X667,X668) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',predefinitionsA18) ).
fof(3067,axiom,
! [X37,X176,X177] :
( ( p__d__instance(X37,X176)
& p__d__subclass(X176,X177) )
=> p__d__instance(X37,X177) ),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',predefinitionsA12) ).
fof(3316,axiom,
( ! [X149,X663,X664] :
( p__d__disjointDecomposition3(X149,X663,X664)
<=> p__d__disjoint(X663,X664) )
& ! [X149,X663,X664,X665] :
( p__d__disjointDecomposition4(X149,X663,X664,X665)
<=> ( p__d__disjoint(X663,X664)
& p__d__disjoint(X663,X665)
& p__d__disjoint(X664,X665) ) )
& ! [X149,X663,X664,X665,X666] :
( p__d__disjointDecomposition5(X149,X663,X664,X665,X666)
<=> ( p__d__disjoint(X663,X664)
& p__d__disjoint(X663,X665)
& p__d__disjoint(X663,X666)
& p__d__disjoint(X664,X665)
& p__d__disjoint(X664,X666)
& p__d__disjoint(X665,X666) ) )
& ! [X149,X663,X664,X665,X666,X667] :
( p__d__disjointDecomposition6(X149,X663,X664,X665,X666,X667)
<=> ( p__d__disjoint(X663,X664)
& p__d__disjoint(X663,X665)
& p__d__disjoint(X663,X666)
& p__d__disjoint(X663,X667)
& p__d__disjoint(X664,X665)
& p__d__disjoint(X664,X666)
& p__d__disjoint(X664,X667)
& p__d__disjoint(X665,X666)
& p__d__disjoint(X665,X667)
& p__d__disjoint(X666,X667) ) )
& ! [X149,X663,X664,X665,X666,X667,X668] :
( p__d__disjointDecomposition7(X149,X663,X664,X665,X666,X667,X668)
<=> ( p__d__disjoint(X663,X664)
& p__d__disjoint(X663,X665)
& p__d__disjoint(X663,X666)
& p__d__disjoint(X663,X667)
& p__d__disjoint(X663,X668)
& p__d__disjoint(X664,X665)
& p__d__disjoint(X664,X666)
& p__d__disjoint(X664,X667)
& p__d__disjoint(X664,X668)
& p__d__disjoint(X665,X666)
& p__d__disjoint(X665,X667)
& p__d__disjoint(X665,X668)
& p__d__disjoint(X666,X667)
& p__d__disjoint(X666,X668)
& p__d__disjoint(X667,X668) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',predefinitionsA24) ).
fof(3317,axiom,
p__d__subclass(c__Putting,c__Transfer),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',mergeA2481) ).
fof(3403,conjecture,
? [X37,X176] :
( ~ p__d__instance(X176,c__Putting)
& ~ p__d__instance(X37,c__Removing)
& ~ equal(X37,X176) ),
file('/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5',antonymPattern31444) ).
fof(3404,negated_conjecture,
~ ? [X37,X176] :
( ~ p__d__instance(X176,c__Putting)
& ~ p__d__instance(X37,c__Removing)
& ~ equal(X37,X176) ),
inference(assume_negation,[status(cth)],[3403]) ).
fof(3432,plain,
! [X138,X137] :
( p__d__disjoint(X138,X137)
<=> ! [X240] :
( ~ p__d__instance(X240,X138)
| ~ p__d__instance(X240,X137) ) ),
inference(fof_simplification,[status(thm)],[1525,theory(equality)]) ).
fof(3494,negated_conjecture,
~ ? [X37,X176] :
( ~ p__d__instance(X176,c__Putting)
& ~ p__d__instance(X37,c__Removing)
& ~ equal(X37,X176) ),
inference(fof_simplification,[status(thm)],[3404,theory(equality)]) ).
cnf(4065,plain,
p__subAttribute(c__Liquid,c__Fluid),
inference(split_conjunct,[status(thm)],[215]) ).
cnf(5079,plain,
p__d__subclass(c__SetOrClass,c__Abstract),
inference(split_conjunct,[status(thm)],[608]) ).
cnf(5083,plain,
p__d__subclass(c__Class,c__SetOrClass),
inference(split_conjunct,[status(thm)],[612]) ).
fof(5138,plain,
! [X149] :
( ( ~ p__d__instance(X149,c__Class)
| p__d__subclass(X149,c__Entity) )
& ( ~ p__d__subclass(X149,c__Entity)
| p__d__instance(X149,c__Class) ) ),
inference(fof_nnf,[status(thm)],[633]) ).
fof(5139,plain,
! [X150] :
( ( ~ p__d__instance(X150,c__Class)
| p__d__subclass(X150,c__Entity) )
& ( ~ p__d__subclass(X150,c__Entity)
| p__d__instance(X150,c__Class) ) ),
inference(variable_rename,[status(thm)],[5138]) ).
cnf(5140,plain,
( p__d__instance(X1,c__Class)
| ~ p__d__subclass(X1,c__Entity) ),
inference(split_conjunct,[status(thm)],[5139]) ).
cnf(5147,plain,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
inference(split_conjunct,[status(thm)],[636]) ).
fof(5646,plain,
! [X149,X284,X285] :
( ~ p__subAttribute(X284,X285)
| ~ p__d__instance(X285,X149)
| p__d__instance(X284,X149) ),
inference(fof_nnf,[status(thm)],[837]) ).
fof(5647,plain,
! [X286,X287,X288] :
( ~ p__subAttribute(X287,X288)
| ~ p__d__instance(X288,X286)
| p__d__instance(X287,X286) ),
inference(variable_rename,[status(thm)],[5646]) ).
cnf(5648,plain,
( p__d__instance(X1,X2)
| ~ p__d__instance(X3,X2)
| ~ p__subAttribute(X1,X3) ),
inference(split_conjunct,[status(thm)],[5647]) ).
cnf(5713,plain,
p__subAttribute(c__Headache,c__Pain),
inference(split_conjunct,[status(thm)],[862]) ).
cnf(5714,plain,
p__subAttribute(c__Pain,c__Unhappiness),
inference(split_conjunct,[status(thm)],[863]) ).
fof(6356,plain,
! [X12,X13] :
( ~ p__subAttribute(X12,X13)
| ( p__d__instance(X13,c__Attribute)
& p__d__instance(X12,c__Attribute) ) ),
inference(fof_nnf,[status(thm)],[1081]) ).
fof(6357,plain,
! [X14,X15] :
( ~ p__subAttribute(X14,X15)
| ( p__d__instance(X15,c__Attribute)
& p__d__instance(X14,c__Attribute) ) ),
inference(variable_rename,[status(thm)],[6356]) ).
fof(6358,plain,
! [X14,X15] :
( ( p__d__instance(X15,c__Attribute)
| ~ p__subAttribute(X14,X15) )
& ( p__d__instance(X14,c__Attribute)
| ~ p__subAttribute(X14,X15) ) ),
inference(distribute,[status(thm)],[6357]) ).
cnf(6359,plain,
( p__d__instance(X1,c__Attribute)
| ~ p__subAttribute(X1,X2) ),
inference(split_conjunct,[status(thm)],[6358]) ).
cnf(6360,plain,
( p__d__instance(X2,c__Attribute)
| ~ p__subAttribute(X1,X2) ),
inference(split_conjunct,[status(thm)],[6358]) ).
fof(6531,plain,
! [X38] : p__d__subclass(X38,X38),
inference(variable_rename,[status(thm)],[1142]) ).
cnf(6532,plain,
p__d__subclass(X1,X1),
inference(split_conjunct,[status(thm)],[6531]) ).
cnf(7050,plain,
p__subAttribute(c__Promise,c__Obligation),
inference(split_conjunct,[status(thm)],[1336]) ).
fof(7615,plain,
! [X138,X137] :
( ( ~ p__d__disjoint(X138,X137)
| ! [X240] :
( ~ p__d__instance(X240,X138)
| ~ p__d__instance(X240,X137) ) )
& ( ? [X240] :
( p__d__instance(X240,X138)
& p__d__instance(X240,X137) )
| p__d__disjoint(X138,X137) ) ),
inference(fof_nnf,[status(thm)],[3432]) ).
fof(7616,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)],[7615]) ).
fof(7617,plain,
! [X241,X242] :
( ( ~ p__d__disjoint(X241,X242)
| ! [X243] :
( ~ p__d__instance(X243,X241)
| ~ p__d__instance(X243,X242) ) )
& ( ( p__d__instance(esk280_2(X241,X242),X241)
& p__d__instance(esk280_2(X241,X242),X242) )
| p__d__disjoint(X241,X242) ) ),
inference(skolemize,[status(esa)],[7616]) ).
fof(7618,plain,
! [X241,X242,X243] :
( ( ~ p__d__instance(X243,X241)
| ~ p__d__instance(X243,X242)
| ~ p__d__disjoint(X241,X242) )
& ( ( p__d__instance(esk280_2(X241,X242),X241)
& p__d__instance(esk280_2(X241,X242),X242) )
| p__d__disjoint(X241,X242) ) ),
inference(shift_quantors,[status(thm)],[7617]) ).
fof(7619,plain,
! [X241,X242,X243] :
( ( ~ p__d__instance(X243,X241)
| ~ p__d__instance(X243,X242)
| ~ p__d__disjoint(X241,X242) )
& ( p__d__instance(esk280_2(X241,X242),X241)
| p__d__disjoint(X241,X242) )
& ( p__d__instance(esk280_2(X241,X242),X242)
| p__d__disjoint(X241,X242) ) ),
inference(distribute,[status(thm)],[7618]) ).
cnf(7622,plain,
( ~ p__d__disjoint(X1,X2)
| ~ p__d__instance(X3,X2)
| ~ p__d__instance(X3,X1) ),
inference(split_conjunct,[status(thm)],[7619]) ).
cnf(8268,plain,
p__d__subclass(c__Process,c__Physical),
inference(split_conjunct,[status(thm)],[1738]) ).
fof(8371,plain,
! [X141] :
( ~ p__d__instance(X141,c__Translocation)
| ? [X9,X54,X55] :
( p__d__instance(X9,c__Object)
& p__d__instance(X54,c__Object)
& p__d__instance(X55,c__Object)
& p__path(X141,X55)
& p__origin(X141,X9)
& p__destination(X141,X54) ) ),
inference(fof_nnf,[status(thm)],[1785]) ).
fof(8372,plain,
! [X142] :
( ~ p__d__instance(X142,c__Translocation)
| ? [X143,X144,X145] :
( p__d__instance(X143,c__Object)
& p__d__instance(X144,c__Object)
& p__d__instance(X145,c__Object)
& p__path(X142,X145)
& p__origin(X142,X143)
& p__destination(X142,X144) ) ),
inference(variable_rename,[status(thm)],[8371]) ).
fof(8373,plain,
! [X142] :
( ~ p__d__instance(X142,c__Translocation)
| ( p__d__instance(esk348_1(X142),c__Object)
& p__d__instance(esk349_1(X142),c__Object)
& p__d__instance(esk350_1(X142),c__Object)
& p__path(X142,esk350_1(X142))
& p__origin(X142,esk348_1(X142))
& p__destination(X142,esk349_1(X142)) ) ),
inference(skolemize,[status(esa)],[8372]) ).
fof(8374,plain,
! [X142] :
( ( p__d__instance(esk348_1(X142),c__Object)
| ~ p__d__instance(X142,c__Translocation) )
& ( p__d__instance(esk349_1(X142),c__Object)
| ~ p__d__instance(X142,c__Translocation) )
& ( p__d__instance(esk350_1(X142),c__Object)
| ~ p__d__instance(X142,c__Translocation) )
& ( p__path(X142,esk350_1(X142))
| ~ p__d__instance(X142,c__Translocation) )
& ( p__origin(X142,esk348_1(X142))
| ~ p__d__instance(X142,c__Translocation) )
& ( p__destination(X142,esk349_1(X142))
| ~ p__d__instance(X142,c__Translocation) ) ),
inference(distribute,[status(thm)],[8373]) ).
cnf(8375,plain,
( p__destination(X1,esk349_1(X1))
| ~ p__d__instance(X1,c__Translocation) ),
inference(split_conjunct,[status(thm)],[8374]) ).
cnf(8839,plain,
p__d__disjointDecomposition6(c__Abstract,c__Quantity,c__Attribute,c__SetOrClass,c__Relation,c__Proposition),
inference(split_conjunct,[status(thm)],[1946]) ).
cnf(8841,plain,
p__d__subclass(c__Attribute,c__Abstract),
inference(split_conjunct,[status(thm)],[1948]) ).
fof(10195,plain,
! [X12,X13] :
( ~ p__destination(X12,X13)
| p__d__instance(X12,c__Process) ),
inference(fof_nnf,[status(thm)],[2415]) ).
fof(10196,plain,
! [X14,X15] :
( ~ p__destination(X14,X15)
| p__d__instance(X14,c__Process) ),
inference(variable_rename,[status(thm)],[10195]) ).
cnf(10197,plain,
( p__d__instance(X1,c__Process)
| ~ p__destination(X1,X2) ),
inference(split_conjunct,[status(thm)],[10196]) ).
cnf(10603,plain,
p__d__subclass(c__Transfer,c__Translocation),
inference(split_conjunct,[status(thm)],[2560]) ).
cnf(11100,plain,
p__subAttribute(c__ServiceContract,c__Contract),
inference(split_conjunct,[status(thm)],[2728]) ).
cnf(11106,plain,
p__subAttribute(c__Contract,c__Promise),
inference(split_conjunct,[status(thm)],[2732]) ).
cnf(11197,plain,
p__d__subclass(c__Removing,c__Transfer),
inference(split_conjunct,[status(thm)],[2758]) ).
fof(12084,plain,
( ! [X149,X663,X664] :
( ( ~ p__d__partition3(X149,X663,X664)
| ( p__d__exhaustiveDecomposition3(X149,X663,X664)
& p__d__disjointDecomposition3(X149,X663,X664) ) )
& ( ~ p__d__exhaustiveDecomposition3(X149,X663,X664)
| ~ p__d__disjointDecomposition3(X149,X663,X664)
| p__d__partition3(X149,X663,X664) ) )
& ! [X149,X663,X664,X665] :
( ( ~ p__d__partition4(X149,X663,X664,X665)
| ( p__d__exhaustiveDecomposition4(X149,X663,X664,X665)
& p__d__disjointDecomposition4(X149,X663,X664,X665) ) )
& ( ~ p__d__exhaustiveDecomposition4(X149,X663,X664,X665)
| ~ p__d__disjointDecomposition4(X149,X663,X664,X665)
| p__d__partition4(X149,X663,X664,X665) ) )
& ! [X149,X663,X664,X665,X666] :
( ( ~ p__d__partition5(X149,X663,X664,X665,X666)
| ( p__d__exhaustiveDecomposition5(X149,X663,X664,X665,X666)
& p__d__disjointDecomposition5(X149,X663,X664,X665,X666) ) )
& ( ~ p__d__exhaustiveDecomposition5(X149,X663,X664,X665,X666)
| ~ p__d__disjointDecomposition5(X149,X663,X664,X665,X666)
| p__d__partition5(X149,X663,X664,X665,X666) ) )
& ! [X149,X663,X664,X665,X666,X667] :
( ( ~ p__d__partition6(X149,X663,X664,X665,X666,X667)
| ( p__d__exhaustiveDecomposition6(X149,X663,X664,X665,X666,X667)
& p__d__disjointDecomposition6(X149,X663,X664,X665,X666,X667) ) )
& ( ~ p__d__exhaustiveDecomposition6(X149,X663,X664,X665,X666,X667)
| ~ p__d__disjointDecomposition6(X149,X663,X664,X665,X666,X667)
| p__d__partition6(X149,X663,X664,X665,X666,X667) ) )
& ! [X149,X663,X664,X665,X666,X667,X668] :
( ( ~ p__d__partition7(X149,X663,X664,X665,X666,X667,X668)
| ( p__d__exhaustiveDecomposition7(X149,X663,X664,X665,X666,X667,X668)
& p__d__disjointDecomposition7(X149,X663,X664,X665,X666,X667,X668) ) )
& ( ~ p__d__exhaustiveDecomposition7(X149,X663,X664,X665,X666,X667,X668)
| ~ p__d__disjointDecomposition7(X149,X663,X664,X665,X666,X667,X668)
| p__d__partition7(X149,X663,X664,X665,X666,X667,X668) ) ) ),
inference(fof_nnf,[status(thm)],[3063]) ).
fof(12085,plain,
( ! [X669,X670,X671] :
( ( ~ p__d__partition3(X669,X670,X671)
| ( p__d__exhaustiveDecomposition3(X669,X670,X671)
& p__d__disjointDecomposition3(X669,X670,X671) ) )
& ( ~ p__d__exhaustiveDecomposition3(X669,X670,X671)
| ~ p__d__disjointDecomposition3(X669,X670,X671)
| p__d__partition3(X669,X670,X671) ) )
& ! [X672,X673,X674,X675] :
( ( ~ p__d__partition4(X672,X673,X674,X675)
| ( p__d__exhaustiveDecomposition4(X672,X673,X674,X675)
& p__d__disjointDecomposition4(X672,X673,X674,X675) ) )
& ( ~ p__d__exhaustiveDecomposition4(X672,X673,X674,X675)
| ~ p__d__disjointDecomposition4(X672,X673,X674,X675)
| p__d__partition4(X672,X673,X674,X675) ) )
& ! [X676,X677,X678,X679,X680] :
( ( ~ p__d__partition5(X676,X677,X678,X679,X680)
| ( p__d__exhaustiveDecomposition5(X676,X677,X678,X679,X680)
& p__d__disjointDecomposition5(X676,X677,X678,X679,X680) ) )
& ( ~ p__d__exhaustiveDecomposition5(X676,X677,X678,X679,X680)
| ~ p__d__disjointDecomposition5(X676,X677,X678,X679,X680)
| p__d__partition5(X676,X677,X678,X679,X680) ) )
& ! [X681,X682,X683,X684,X685,X686] :
( ( ~ p__d__partition6(X681,X682,X683,X684,X685,X686)
| ( p__d__exhaustiveDecomposition6(X681,X682,X683,X684,X685,X686)
& p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686) ) )
& ( ~ p__d__exhaustiveDecomposition6(X681,X682,X683,X684,X685,X686)
| ~ p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686)
| p__d__partition6(X681,X682,X683,X684,X685,X686) ) )
& ! [X687,X688,X689,X690,X691,X692,X693] :
( ( ~ p__d__partition7(X687,X688,X689,X690,X691,X692,X693)
| ( p__d__exhaustiveDecomposition7(X687,X688,X689,X690,X691,X692,X693)
& p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) ) )
& ( ~ p__d__exhaustiveDecomposition7(X687,X688,X689,X690,X691,X692,X693)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693)
| p__d__partition7(X687,X688,X689,X690,X691,X692,X693) ) ) ),
inference(variable_rename,[status(thm)],[12084]) ).
fof(12086,plain,
! [X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687,X688,X689,X690,X691,X692,X693] :
( ( ~ p__d__partition7(X687,X688,X689,X690,X691,X692,X693)
| ( p__d__exhaustiveDecomposition7(X687,X688,X689,X690,X691,X692,X693)
& p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) ) )
& ( ~ p__d__exhaustiveDecomposition7(X687,X688,X689,X690,X691,X692,X693)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693)
| p__d__partition7(X687,X688,X689,X690,X691,X692,X693) )
& ( ~ p__d__partition6(X681,X682,X683,X684,X685,X686)
| ( p__d__exhaustiveDecomposition6(X681,X682,X683,X684,X685,X686)
& p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686) ) )
& ( ~ p__d__exhaustiveDecomposition6(X681,X682,X683,X684,X685,X686)
| ~ p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686)
| p__d__partition6(X681,X682,X683,X684,X685,X686) )
& ( ~ p__d__partition5(X676,X677,X678,X679,X680)
| ( p__d__exhaustiveDecomposition5(X676,X677,X678,X679,X680)
& p__d__disjointDecomposition5(X676,X677,X678,X679,X680) ) )
& ( ~ p__d__exhaustiveDecomposition5(X676,X677,X678,X679,X680)
| ~ p__d__disjointDecomposition5(X676,X677,X678,X679,X680)
| p__d__partition5(X676,X677,X678,X679,X680) )
& ( ~ p__d__partition4(X672,X673,X674,X675)
| ( p__d__exhaustiveDecomposition4(X672,X673,X674,X675)
& p__d__disjointDecomposition4(X672,X673,X674,X675) ) )
& ( ~ p__d__exhaustiveDecomposition4(X672,X673,X674,X675)
| ~ p__d__disjointDecomposition4(X672,X673,X674,X675)
| p__d__partition4(X672,X673,X674,X675) )
& ( ~ p__d__partition3(X669,X670,X671)
| ( p__d__exhaustiveDecomposition3(X669,X670,X671)
& p__d__disjointDecomposition3(X669,X670,X671) ) )
& ( ~ p__d__exhaustiveDecomposition3(X669,X670,X671)
| ~ p__d__disjointDecomposition3(X669,X670,X671)
| p__d__partition3(X669,X670,X671) ) ),
inference(shift_quantors,[status(thm)],[12085]) ).
fof(12087,plain,
! [X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687,X688,X689,X690,X691,X692,X693] :
( ( p__d__exhaustiveDecomposition7(X687,X688,X689,X690,X691,X692,X693)
| ~ p__d__partition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693)
| ~ p__d__partition7(X687,X688,X689,X690,X691,X692,X693) )
& ( ~ p__d__exhaustiveDecomposition7(X687,X688,X689,X690,X691,X692,X693)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693)
| p__d__partition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__exhaustiveDecomposition6(X681,X682,X683,X684,X685,X686)
| ~ p__d__partition6(X681,X682,X683,X684,X685,X686) )
& ( p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686)
| ~ p__d__partition6(X681,X682,X683,X684,X685,X686) )
& ( ~ p__d__exhaustiveDecomposition6(X681,X682,X683,X684,X685,X686)
| ~ p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686)
| p__d__partition6(X681,X682,X683,X684,X685,X686) )
& ( p__d__exhaustiveDecomposition5(X676,X677,X678,X679,X680)
| ~ p__d__partition5(X676,X677,X678,X679,X680) )
& ( p__d__disjointDecomposition5(X676,X677,X678,X679,X680)
| ~ p__d__partition5(X676,X677,X678,X679,X680) )
& ( ~ p__d__exhaustiveDecomposition5(X676,X677,X678,X679,X680)
| ~ p__d__disjointDecomposition5(X676,X677,X678,X679,X680)
| p__d__partition5(X676,X677,X678,X679,X680) )
& ( p__d__exhaustiveDecomposition4(X672,X673,X674,X675)
| ~ p__d__partition4(X672,X673,X674,X675) )
& ( p__d__disjointDecomposition4(X672,X673,X674,X675)
| ~ p__d__partition4(X672,X673,X674,X675) )
& ( ~ p__d__exhaustiveDecomposition4(X672,X673,X674,X675)
| ~ p__d__disjointDecomposition4(X672,X673,X674,X675)
| p__d__partition4(X672,X673,X674,X675) )
& ( p__d__exhaustiveDecomposition3(X669,X670,X671)
| ~ p__d__partition3(X669,X670,X671) )
& ( p__d__disjointDecomposition3(X669,X670,X671)
| ~ p__d__partition3(X669,X670,X671) )
& ( ~ p__d__exhaustiveDecomposition3(X669,X670,X671)
| ~ p__d__disjointDecomposition3(X669,X670,X671)
| p__d__partition3(X669,X670,X671) ) ),
inference(distribute,[status(thm)],[12086]) ).
cnf(12089,plain,
( p__d__disjointDecomposition3(X1,X2,X3)
| ~ p__d__partition3(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[12087]) ).
fof(12111,plain,
! [X37,X176,X177] :
( ~ p__d__instance(X37,X176)
| ~ p__d__subclass(X176,X177)
| p__d__instance(X37,X177) ),
inference(fof_nnf,[status(thm)],[3067]) ).
fof(12112,plain,
! [X178,X179,X180] :
( ~ p__d__instance(X178,X179)
| ~ p__d__subclass(X179,X180)
| p__d__instance(X178,X180) ),
inference(variable_rename,[status(thm)],[12111]) ).
cnf(12113,plain,
( p__d__instance(X1,X2)
| ~ p__d__subclass(X3,X2)
| ~ p__d__instance(X1,X3) ),
inference(split_conjunct,[status(thm)],[12112]) ).
fof(12847,plain,
( ! [X149,X663,X664] :
( ( ~ p__d__disjointDecomposition3(X149,X663,X664)
| p__d__disjoint(X663,X664) )
& ( ~ p__d__disjoint(X663,X664)
| p__d__disjointDecomposition3(X149,X663,X664) ) )
& ! [X149,X663,X664,X665] :
( ( ~ p__d__disjointDecomposition4(X149,X663,X664,X665)
| ( p__d__disjoint(X663,X664)
& p__d__disjoint(X663,X665)
& p__d__disjoint(X664,X665) ) )
& ( ~ p__d__disjoint(X663,X664)
| ~ p__d__disjoint(X663,X665)
| ~ p__d__disjoint(X664,X665)
| p__d__disjointDecomposition4(X149,X663,X664,X665) ) )
& ! [X149,X663,X664,X665,X666] :
( ( ~ p__d__disjointDecomposition5(X149,X663,X664,X665,X666)
| ( p__d__disjoint(X663,X664)
& p__d__disjoint(X663,X665)
& p__d__disjoint(X663,X666)
& p__d__disjoint(X664,X665)
& p__d__disjoint(X664,X666)
& p__d__disjoint(X665,X666) ) )
& ( ~ p__d__disjoint(X663,X664)
| ~ p__d__disjoint(X663,X665)
| ~ p__d__disjoint(X663,X666)
| ~ p__d__disjoint(X664,X665)
| ~ p__d__disjoint(X664,X666)
| ~ p__d__disjoint(X665,X666)
| p__d__disjointDecomposition5(X149,X663,X664,X665,X666) ) )
& ! [X149,X663,X664,X665,X666,X667] :
( ( ~ p__d__disjointDecomposition6(X149,X663,X664,X665,X666,X667)
| ( p__d__disjoint(X663,X664)
& p__d__disjoint(X663,X665)
& p__d__disjoint(X663,X666)
& p__d__disjoint(X663,X667)
& p__d__disjoint(X664,X665)
& p__d__disjoint(X664,X666)
& p__d__disjoint(X664,X667)
& p__d__disjoint(X665,X666)
& p__d__disjoint(X665,X667)
& p__d__disjoint(X666,X667) ) )
& ( ~ p__d__disjoint(X663,X664)
| ~ p__d__disjoint(X663,X665)
| ~ p__d__disjoint(X663,X666)
| ~ p__d__disjoint(X663,X667)
| ~ p__d__disjoint(X664,X665)
| ~ p__d__disjoint(X664,X666)
| ~ p__d__disjoint(X664,X667)
| ~ p__d__disjoint(X665,X666)
| ~ p__d__disjoint(X665,X667)
| ~ p__d__disjoint(X666,X667)
| p__d__disjointDecomposition6(X149,X663,X664,X665,X666,X667) ) )
& ! [X149,X663,X664,X665,X666,X667,X668] :
( ( ~ p__d__disjointDecomposition7(X149,X663,X664,X665,X666,X667,X668)
| ( p__d__disjoint(X663,X664)
& p__d__disjoint(X663,X665)
& p__d__disjoint(X663,X666)
& p__d__disjoint(X663,X667)
& p__d__disjoint(X663,X668)
& p__d__disjoint(X664,X665)
& p__d__disjoint(X664,X666)
& p__d__disjoint(X664,X667)
& p__d__disjoint(X664,X668)
& p__d__disjoint(X665,X666)
& p__d__disjoint(X665,X667)
& p__d__disjoint(X665,X668)
& p__d__disjoint(X666,X667)
& p__d__disjoint(X666,X668)
& p__d__disjoint(X667,X668) ) )
& ( ~ p__d__disjoint(X663,X664)
| ~ p__d__disjoint(X663,X665)
| ~ p__d__disjoint(X663,X666)
| ~ p__d__disjoint(X663,X667)
| ~ p__d__disjoint(X663,X668)
| ~ p__d__disjoint(X664,X665)
| ~ p__d__disjoint(X664,X666)
| ~ p__d__disjoint(X664,X667)
| ~ p__d__disjoint(X664,X668)
| ~ p__d__disjoint(X665,X666)
| ~ p__d__disjoint(X665,X667)
| ~ p__d__disjoint(X665,X668)
| ~ p__d__disjoint(X666,X667)
| ~ p__d__disjoint(X666,X668)
| ~ p__d__disjoint(X667,X668)
| p__d__disjointDecomposition7(X149,X663,X664,X665,X666,X667,X668) ) ) ),
inference(fof_nnf,[status(thm)],[3316]) ).
fof(12848,plain,
( ! [X669,X670,X671] :
( ( ~ p__d__disjointDecomposition3(X669,X670,X671)
| p__d__disjoint(X670,X671) )
& ( ~ p__d__disjoint(X670,X671)
| p__d__disjointDecomposition3(X669,X670,X671) ) )
& ! [X672,X673,X674,X675] :
( ( ~ p__d__disjointDecomposition4(X672,X673,X674,X675)
| ( p__d__disjoint(X673,X674)
& p__d__disjoint(X673,X675)
& p__d__disjoint(X674,X675) ) )
& ( ~ p__d__disjoint(X673,X674)
| ~ p__d__disjoint(X673,X675)
| ~ p__d__disjoint(X674,X675)
| p__d__disjointDecomposition4(X672,X673,X674,X675) ) )
& ! [X676,X677,X678,X679,X680] :
( ( ~ p__d__disjointDecomposition5(X676,X677,X678,X679,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(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__disjointDecomposition5(X676,X677,X678,X679,X680) ) )
& ! [X681,X682,X683,X684,X685,X686] :
( ( ~ p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686)
| ( p__d__disjoint(X682,X683)
& p__d__disjoint(X682,X684)
& p__d__disjoint(X682,X685)
& p__d__disjoint(X682,X686)
& p__d__disjoint(X683,X684)
& p__d__disjoint(X683,X685)
& p__d__disjoint(X683,X686)
& p__d__disjoint(X684,X685)
& p__d__disjoint(X684,X686)
& p__d__disjoint(X685,X686) ) )
& ( ~ p__d__disjoint(X682,X683)
| ~ p__d__disjoint(X682,X684)
| ~ p__d__disjoint(X682,X685)
| ~ p__d__disjoint(X682,X686)
| ~ p__d__disjoint(X683,X684)
| ~ p__d__disjoint(X683,X685)
| ~ p__d__disjoint(X683,X686)
| ~ p__d__disjoint(X684,X685)
| ~ p__d__disjoint(X684,X686)
| ~ p__d__disjoint(X685,X686)
| p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686) ) )
& ! [X687,X688,X689,X690,X691,X692,X693] :
( ( ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693)
| ( p__d__disjoint(X688,X689)
& p__d__disjoint(X688,X690)
& p__d__disjoint(X688,X691)
& p__d__disjoint(X688,X692)
& p__d__disjoint(X688,X693)
& p__d__disjoint(X689,X690)
& p__d__disjoint(X689,X691)
& p__d__disjoint(X689,X692)
& p__d__disjoint(X689,X693)
& p__d__disjoint(X690,X691)
& p__d__disjoint(X690,X692)
& p__d__disjoint(X690,X693)
& p__d__disjoint(X691,X692)
& p__d__disjoint(X691,X693)
& p__d__disjoint(X692,X693) ) )
& ( ~ p__d__disjoint(X688,X689)
| ~ p__d__disjoint(X688,X690)
| ~ p__d__disjoint(X688,X691)
| ~ p__d__disjoint(X688,X692)
| ~ p__d__disjoint(X688,X693)
| ~ p__d__disjoint(X689,X690)
| ~ p__d__disjoint(X689,X691)
| ~ p__d__disjoint(X689,X692)
| ~ p__d__disjoint(X689,X693)
| ~ p__d__disjoint(X690,X691)
| ~ p__d__disjoint(X690,X692)
| ~ p__d__disjoint(X690,X693)
| ~ p__d__disjoint(X691,X692)
| ~ p__d__disjoint(X691,X693)
| ~ p__d__disjoint(X692,X693)
| p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) ) ) ),
inference(variable_rename,[status(thm)],[12847]) ).
fof(12849,plain,
! [X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687,X688,X689,X690,X691,X692,X693] :
( ( ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693)
| ( p__d__disjoint(X688,X689)
& p__d__disjoint(X688,X690)
& p__d__disjoint(X688,X691)
& p__d__disjoint(X688,X692)
& p__d__disjoint(X688,X693)
& p__d__disjoint(X689,X690)
& p__d__disjoint(X689,X691)
& p__d__disjoint(X689,X692)
& p__d__disjoint(X689,X693)
& p__d__disjoint(X690,X691)
& p__d__disjoint(X690,X692)
& p__d__disjoint(X690,X693)
& p__d__disjoint(X691,X692)
& p__d__disjoint(X691,X693)
& p__d__disjoint(X692,X693) ) )
& ( ~ p__d__disjoint(X688,X689)
| ~ p__d__disjoint(X688,X690)
| ~ p__d__disjoint(X688,X691)
| ~ p__d__disjoint(X688,X692)
| ~ p__d__disjoint(X688,X693)
| ~ p__d__disjoint(X689,X690)
| ~ p__d__disjoint(X689,X691)
| ~ p__d__disjoint(X689,X692)
| ~ p__d__disjoint(X689,X693)
| ~ p__d__disjoint(X690,X691)
| ~ p__d__disjoint(X690,X692)
| ~ p__d__disjoint(X690,X693)
| ~ p__d__disjoint(X691,X692)
| ~ p__d__disjoint(X691,X693)
| ~ p__d__disjoint(X692,X693)
| p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( ~ p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686)
| ( p__d__disjoint(X682,X683)
& p__d__disjoint(X682,X684)
& p__d__disjoint(X682,X685)
& p__d__disjoint(X682,X686)
& p__d__disjoint(X683,X684)
& p__d__disjoint(X683,X685)
& p__d__disjoint(X683,X686)
& p__d__disjoint(X684,X685)
& p__d__disjoint(X684,X686)
& p__d__disjoint(X685,X686) ) )
& ( ~ p__d__disjoint(X682,X683)
| ~ p__d__disjoint(X682,X684)
| ~ p__d__disjoint(X682,X685)
| ~ p__d__disjoint(X682,X686)
| ~ p__d__disjoint(X683,X684)
| ~ p__d__disjoint(X683,X685)
| ~ p__d__disjoint(X683,X686)
| ~ p__d__disjoint(X684,X685)
| ~ p__d__disjoint(X684,X686)
| ~ p__d__disjoint(X685,X686)
| p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686) )
& ( ~ p__d__disjointDecomposition5(X676,X677,X678,X679,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(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__disjointDecomposition5(X676,X677,X678,X679,X680) )
& ( ~ p__d__disjointDecomposition4(X672,X673,X674,X675)
| ( p__d__disjoint(X673,X674)
& p__d__disjoint(X673,X675)
& p__d__disjoint(X674,X675) ) )
& ( ~ p__d__disjoint(X673,X674)
| ~ p__d__disjoint(X673,X675)
| ~ p__d__disjoint(X674,X675)
| p__d__disjointDecomposition4(X672,X673,X674,X675) )
& ( ~ p__d__disjointDecomposition3(X669,X670,X671)
| p__d__disjoint(X670,X671) )
& ( ~ p__d__disjoint(X670,X671)
| p__d__disjointDecomposition3(X669,X670,X671) ) ),
inference(shift_quantors,[status(thm)],[12848]) ).
fof(12850,plain,
! [X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687,X688,X689,X690,X691,X692,X693] :
( ( p__d__disjoint(X688,X689)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjoint(X688,X690)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjoint(X688,X691)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjoint(X688,X692)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjoint(X688,X693)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjoint(X689,X690)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjoint(X689,X691)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjoint(X689,X692)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjoint(X689,X693)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjoint(X690,X691)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjoint(X690,X692)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjoint(X690,X693)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjoint(X691,X692)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjoint(X691,X693)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjoint(X692,X693)
| ~ p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( ~ p__d__disjoint(X688,X689)
| ~ p__d__disjoint(X688,X690)
| ~ p__d__disjoint(X688,X691)
| ~ p__d__disjoint(X688,X692)
| ~ p__d__disjoint(X688,X693)
| ~ p__d__disjoint(X689,X690)
| ~ p__d__disjoint(X689,X691)
| ~ p__d__disjoint(X689,X692)
| ~ p__d__disjoint(X689,X693)
| ~ p__d__disjoint(X690,X691)
| ~ p__d__disjoint(X690,X692)
| ~ p__d__disjoint(X690,X693)
| ~ p__d__disjoint(X691,X692)
| ~ p__d__disjoint(X691,X693)
| ~ p__d__disjoint(X692,X693)
| p__d__disjointDecomposition7(X687,X688,X689,X690,X691,X692,X693) )
& ( p__d__disjoint(X682,X683)
| ~ p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686) )
& ( p__d__disjoint(X682,X684)
| ~ p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686) )
& ( p__d__disjoint(X682,X685)
| ~ p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686) )
& ( p__d__disjoint(X682,X686)
| ~ p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686) )
& ( p__d__disjoint(X683,X684)
| ~ p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686) )
& ( p__d__disjoint(X683,X685)
| ~ p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686) )
& ( p__d__disjoint(X683,X686)
| ~ p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686) )
& ( p__d__disjoint(X684,X685)
| ~ p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686) )
& ( p__d__disjoint(X684,X686)
| ~ p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686) )
& ( p__d__disjoint(X685,X686)
| ~ p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686) )
& ( ~ p__d__disjoint(X682,X683)
| ~ p__d__disjoint(X682,X684)
| ~ p__d__disjoint(X682,X685)
| ~ p__d__disjoint(X682,X686)
| ~ p__d__disjoint(X683,X684)
| ~ p__d__disjoint(X683,X685)
| ~ p__d__disjoint(X683,X686)
| ~ p__d__disjoint(X684,X685)
| ~ p__d__disjoint(X684,X686)
| ~ p__d__disjoint(X685,X686)
| p__d__disjointDecomposition6(X681,X682,X683,X684,X685,X686) )
& ( p__d__disjoint(X677,X678)
| ~ p__d__disjointDecomposition5(X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X677,X679)
| ~ p__d__disjointDecomposition5(X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X677,X680)
| ~ p__d__disjointDecomposition5(X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X678,X679)
| ~ p__d__disjointDecomposition5(X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X678,X680)
| ~ p__d__disjointDecomposition5(X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X679,X680)
| ~ p__d__disjointDecomposition5(X676,X677,X678,X679,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__disjointDecomposition5(X676,X677,X678,X679,X680) )
& ( p__d__disjoint(X673,X674)
| ~ p__d__disjointDecomposition4(X672,X673,X674,X675) )
& ( p__d__disjoint(X673,X675)
| ~ p__d__disjointDecomposition4(X672,X673,X674,X675) )
& ( p__d__disjoint(X674,X675)
| ~ p__d__disjointDecomposition4(X672,X673,X674,X675) )
& ( ~ p__d__disjoint(X673,X674)
| ~ p__d__disjoint(X673,X675)
| ~ p__d__disjoint(X674,X675)
| p__d__disjointDecomposition4(X672,X673,X674,X675) )
& ( ~ p__d__disjointDecomposition3(X669,X670,X671)
| p__d__disjoint(X670,X671) )
& ( ~ p__d__disjoint(X670,X671)
| p__d__disjointDecomposition3(X669,X670,X671) ) ),
inference(distribute,[status(thm)],[12849]) ).
cnf(12852,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__disjointDecomposition3(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[12850]) ).
cnf(12870,plain,
( p__d__disjoint(X3,X4)
| ~ p__d__disjointDecomposition6(X1,X2,X3,X4,X5,X6) ),
inference(split_conjunct,[status(thm)],[12850]) ).
cnf(12891,plain,
p__d__subclass(c__Putting,c__Transfer),
inference(split_conjunct,[status(thm)],[3317]) ).
fof(13148,negated_conjecture,
! [X37,X176] :
( p__d__instance(X176,c__Putting)
| p__d__instance(X37,c__Removing)
| equal(X37,X176) ),
inference(fof_nnf,[status(thm)],[3494]) ).
fof(13149,negated_conjecture,
! [X177,X178] :
( p__d__instance(X178,c__Putting)
| p__d__instance(X177,c__Removing)
| equal(X177,X178) ),
inference(variable_rename,[status(thm)],[13148]) ).
cnf(13150,negated_conjecture,
( X1 = X2
| p__d__instance(X1,c__Removing)
| p__d__instance(X2,c__Putting) ),
inference(split_conjunct,[status(thm)],[13149]) ).
cnf(13166,plain,
p__d__instance(c__Entity,c__Class),
inference(spm,[status(thm)],[5140,6532,theory(equality)]) ).
cnf(13202,plain,
p__d__instance(c__Fluid,c__Attribute),
inference(spm,[status(thm)],[6360,4065,theory(equality)]) ).
cnf(13205,plain,
p__d__instance(c__Pain,c__Attribute),
inference(spm,[status(thm)],[6360,5713,theory(equality)]) ).
cnf(13216,plain,
p__d__instance(c__Contract,c__Attribute),
inference(spm,[status(thm)],[6360,11100,theory(equality)]) ).
cnf(13471,plain,
p__d__instance(c__Liquid,c__Attribute),
inference(spm,[status(thm)],[6359,4065,theory(equality)]) ).
cnf(14541,plain,
( p__d__instance(c__Liquid,X1)
| ~ p__d__instance(c__Fluid,X1) ),
inference(spm,[status(thm)],[5648,4065,theory(equality)]) ).
cnf(14543,plain,
( p__d__instance(c__Promise,X1)
| ~ p__d__instance(c__Obligation,X1) ),
inference(spm,[status(thm)],[5648,7050,theory(equality)]) ).
cnf(14544,plain,
( p__d__instance(c__Headache,X1)
| ~ p__d__instance(c__Pain,X1) ),
inference(spm,[status(thm)],[5648,5713,theory(equality)]) ).
cnf(14545,plain,
( p__d__instance(c__Pain,X1)
| ~ p__d__instance(c__Unhappiness,X1) ),
inference(spm,[status(thm)],[5648,5714,theory(equality)]) ).
cnf(14553,plain,
( p__d__instance(c__Contract,X1)
| ~ p__d__instance(c__Promise,X1) ),
inference(spm,[status(thm)],[5648,11106,theory(equality)]) ).
cnf(14555,plain,
( p__d__instance(c__ServiceContract,X1)
| ~ p__d__instance(c__Contract,X1) ),
inference(spm,[status(thm)],[5648,11100,theory(equality)]) ).
cnf(14558,plain,
( p__d__instance(X1,c__Transfer)
| ~ p__d__instance(X1,c__Removing) ),
inference(spm,[status(thm)],[12113,11197,theory(equality)]) ).
cnf(14561,plain,
( p__d__instance(X1,c__Transfer)
| ~ p__d__instance(X1,c__Putting) ),
inference(spm,[status(thm)],[12113,12891,theory(equality)]) ).
cnf(14568,plain,
( p__d__instance(X1,c__Physical)
| ~ p__d__instance(X1,c__Process) ),
inference(spm,[status(thm)],[12113,8268,theory(equality)]) ).
cnf(14599,plain,
( p__d__instance(X1,c__Abstract)
| ~ p__d__instance(X1,c__SetOrClass) ),
inference(spm,[status(thm)],[12113,5079,theory(equality)]) ).
cnf(14685,plain,
( p__d__instance(X1,c__Abstract)
| ~ p__d__instance(X1,c__Attribute) ),
inference(spm,[status(thm)],[12113,8841,theory(equality)]) ).
cnf(14835,plain,
( p__d__instance(X1,c__Translocation)
| ~ p__d__instance(X1,c__Transfer) ),
inference(spm,[status(thm)],[12113,10603,theory(equality)]) ).
cnf(15050,plain,
( p__d__instance(X1,c__SetOrClass)
| ~ p__d__instance(X1,c__Class) ),
inference(spm,[status(thm)],[12113,5083,theory(equality)]) ).
cnf(16231,plain,
( p__d__instance(X1,c__Process)
| ~ p__d__instance(X1,c__Translocation) ),
inference(spm,[status(thm)],[10197,8375,theory(equality)]) ).
cnf(18346,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__partition3(X3,X1,X2) ),
inference(spm,[status(thm)],[12852,12089,theory(equality)]) ).
cnf(20078,plain,
p__d__disjoint(c__Attribute,c__SetOrClass),
inference(spm,[status(thm)],[12870,8839,theory(equality)]) ).
cnf(39817,plain,
( ~ p__d__instance(X1,c__SetOrClass)
| ~ p__d__instance(X1,c__Attribute) ),
inference(spm,[status(thm)],[7622,20078,theory(equality)]) ).
cnf(42010,plain,
( p__d__instance(c__Pain,c__Transfer)
| ~ p__d__instance(c__Unhappiness,c__Removing) ),
inference(spm,[status(thm)],[14558,14545,theory(equality)]) ).
cnf(45244,plain,
( p__d__instance(c__Contract,c__Transfer)
| ~ p__d__instance(c__Promise,c__Putting) ),
inference(spm,[status(thm)],[14561,14553,theory(equality)]) ).
cnf(46754,plain,
( p__d__instance(c__Headache,c__Physical)
| ~ p__d__instance(c__Pain,c__Process) ),
inference(spm,[status(thm)],[14544,14568,theory(equality)]) ).
cnf(51129,plain,
~ p__d__instance(c__Liquid,c__SetOrClass),
inference(spm,[status(thm)],[39817,13471,theory(equality)]) ).
cnf(52139,plain,
( p__d__instance(c__Liquid,c__Abstract)
| ~ p__d__instance(c__Fluid,c__Attribute) ),
inference(spm,[status(thm)],[14541,14685,theory(equality)]) ).
cnf(52141,plain,
( p__d__instance(c__Headache,c__Abstract)
| ~ p__d__instance(c__Pain,c__Attribute) ),
inference(spm,[status(thm)],[14544,14685,theory(equality)]) ).
cnf(52142,plain,
( p__d__instance(c__ServiceContract,c__Abstract)
| ~ p__d__instance(c__Contract,c__Attribute) ),
inference(spm,[status(thm)],[14555,14685,theory(equality)]) ).
cnf(52143,plain,
( p__d__instance(c__Liquid,c__Abstract)
| $false ),
inference(rw,[status(thm)],[52139,13202,theory(equality)]) ).
cnf(52144,plain,
p__d__instance(c__Liquid,c__Abstract),
inference(cn,[status(thm)],[52143,theory(equality)]) ).
cnf(52147,plain,
( p__d__instance(c__Headache,c__Abstract)
| $false ),
inference(rw,[status(thm)],[52141,13205,theory(equality)]) ).
cnf(52148,plain,
p__d__instance(c__Headache,c__Abstract),
inference(cn,[status(thm)],[52147,theory(equality)]) ).
cnf(52149,plain,
( p__d__instance(c__ServiceContract,c__Abstract)
| $false ),
inference(rw,[status(thm)],[52142,13216,theory(equality)]) ).
cnf(52150,plain,
p__d__instance(c__ServiceContract,c__Abstract),
inference(cn,[status(thm)],[52149,theory(equality)]) ).
cnf(60854,plain,
( p__d__instance(c__Pain,c__Translocation)
| ~ p__d__instance(c__Unhappiness,c__Removing) ),
inference(spm,[status(thm)],[14835,42010,theory(equality)]) ).
cnf(60881,plain,
( p__d__instance(c__Contract,c__Translocation)
| ~ p__d__instance(c__Promise,c__Putting) ),
inference(spm,[status(thm)],[14835,45244,theory(equality)]) ).
cnf(72880,plain,
p__d__instance(c__Entity,c__SetOrClass),
inference(spm,[status(thm)],[15050,13166,theory(equality)]) ).
cnf(107668,plain,
( p__d__instance(c__Pain,c__Process)
| ~ p__d__instance(c__Unhappiness,c__Removing) ),
inference(spm,[status(thm)],[16231,60854,theory(equality)]) ).
cnf(107687,plain,
( p__d__instance(c__Contract,c__Process)
| ~ p__d__instance(c__Promise,c__Putting) ),
inference(spm,[status(thm)],[16231,60881,theory(equality)]) ).
cnf(108087,plain,
( p__d__instance(c__ServiceContract,c__Process)
| ~ p__d__instance(c__Promise,c__Putting) ),
inference(spm,[status(thm)],[14555,107687,theory(equality)]) ).
cnf(108089,plain,
( p__d__instance(c__ServiceContract,c__Process)
| ~ p__d__instance(c__Obligation,c__Putting) ),
inference(spm,[status(thm)],[108087,14543,theory(equality)]) ).
cnf(132590,plain,
( p__d__instance(c__Headache,c__Physical)
| ~ p__d__instance(c__Unhappiness,c__Removing) ),
inference(spm,[status(thm)],[46754,107668,theory(equality)]) ).
cnf(181312,plain,
p__d__disjoint(c__Physical,c__Abstract),
inference(spm,[status(thm)],[18346,5147,theory(equality)]) ).
cnf(181987,plain,
( ~ p__d__instance(X1,c__Abstract)
| ~ p__d__instance(X1,c__Physical) ),
inference(spm,[status(thm)],[7622,181312,theory(equality)]) ).
cnf(182488,plain,
~ p__d__instance(c__Liquid,c__Physical),
inference(spm,[status(thm)],[181987,52144,theory(equality)]) ).
cnf(182490,plain,
~ p__d__instance(c__Headache,c__Physical),
inference(spm,[status(thm)],[181987,52148,theory(equality)]) ).
cnf(182491,plain,
~ p__d__instance(c__ServiceContract,c__Physical),
inference(spm,[status(thm)],[181987,52150,theory(equality)]) ).
cnf(182525,plain,
( ~ p__d__instance(X1,c__Physical)
| ~ p__d__instance(X1,c__SetOrClass) ),
inference(spm,[status(thm)],[181987,14599,theory(equality)]) ).
cnf(182549,plain,
~ p__d__instance(c__Liquid,c__Process),
inference(spm,[status(thm)],[182488,14568,theory(equality)]) ).
cnf(182560,plain,
~ p__d__instance(c__Unhappiness,c__Removing),
inference(spm,[status(thm)],[182490,132590,theory(equality)]) ).
cnf(182562,negated_conjecture,
( c__Unhappiness = X1
| p__d__instance(X1,c__Putting) ),
inference(spm,[status(thm)],[182560,13150,theory(equality)]) ).
cnf(182580,plain,
~ p__d__instance(c__ServiceContract,c__Process),
inference(spm,[status(thm)],[182491,14568,theory(equality)]) ).
cnf(182646,negated_conjecture,
( p__d__instance(c__ServiceContract,c__Process)
| c__Unhappiness = c__Obligation ),
inference(spm,[status(thm)],[108089,182562,theory(equality)]) ).
cnf(182651,negated_conjecture,
c__Unhappiness = c__Obligation,
inference(sr,[status(thm)],[182646,182580,theory(equality)]) ).
cnf(184318,negated_conjecture,
( c__Obligation = X1
| p__d__instance(X1,c__Putting) ),
inference(rw,[status(thm)],[182562,182651,theory(equality)]) ).
cnf(186003,negated_conjecture,
( p__d__instance(X1,c__Transfer)
| c__Obligation = X1 ),
inference(spm,[status(thm)],[14561,184318,theory(equality)]) ).
cnf(186100,negated_conjecture,
( p__d__instance(X1,c__Translocation)
| c__Obligation = X1 ),
inference(spm,[status(thm)],[14835,186003,theory(equality)]) ).
cnf(186131,negated_conjecture,
( p__d__instance(X1,c__Process)
| c__Obligation = X1 ),
inference(spm,[status(thm)],[16231,186100,theory(equality)]) ).
cnf(186138,negated_conjecture,
c__Obligation = c__Liquid,
inference(spm,[status(thm)],[182549,186131,theory(equality)]) ).
cnf(186276,negated_conjecture,
( c__Liquid = X1
| p__d__instance(X1,c__Putting) ),
inference(rw,[status(thm)],[184318,186138,theory(equality)]) ).
cnf(187505,negated_conjecture,
( p__d__instance(X1,c__Transfer)
| c__Liquid = X1 ),
inference(spm,[status(thm)],[14561,186276,theory(equality)]) ).
cnf(187526,negated_conjecture,
( p__d__instance(X1,c__Translocation)
| c__Liquid = X1 ),
inference(spm,[status(thm)],[14835,187505,theory(equality)]) ).
cnf(187555,negated_conjecture,
( p__d__instance(X1,c__Process)
| c__Liquid = X1 ),
inference(spm,[status(thm)],[16231,187526,theory(equality)]) ).
cnf(189166,plain,
~ p__d__instance(c__Entity,c__Physical),
inference(spm,[status(thm)],[182525,72880,theory(equality)]) ).
cnf(189199,plain,
~ p__d__instance(c__Entity,c__Process),
inference(spm,[status(thm)],[189166,14568,theory(equality)]) ).
cnf(189205,negated_conjecture,
c__Liquid = c__Entity,
inference(spm,[status(thm)],[189199,187555,theory(equality)]) ).
cnf(189206,plain,
p__d__instance(c__Liquid,c__SetOrClass),
inference(rw,[status(thm)],[72880,189205,theory(equality)]) ).
cnf(189207,plain,
$false,
inference(sr,[status(thm)],[189206,51129,theory(equality)]) ).
cnf(189208,plain,
$false,
189207,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR229+1 : TPTP v7.3.0. Released v7.3.0.
% 0.00/0.05 % Command : sine.py -e eprover -t %d %s
% 0.05/0.25 % Computer : n183.star.cs.uiowa.edu
% 0.05/0.25 % Model : x86_64 x86_64
% 0.05/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.05/0.25 % Memory : 32218.5MB
% 0.05/0.25 % OS : Linux 3.10.0-862.11.6.el7.x86_64
% 0.05/0.25 % CPULimit : 300
% 0.05/0.25 % DateTime : Wed Feb 20 02:46:48 CST 2019
% 0.05/0.25 % CPUTime :
% 0.09/0.30 % SZS status Started for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.30 --creating new selector for [CSR006+0.ax]
% 0.66/11.05 -running prover on /export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_1 with time limit 29
% 0.66/11.05 -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/tmp618XP7/sel_theBenchmark.p_1']
% 0.66/11.05 -prover status CounterSatisfiable
% 0.66/11.05 -running prover on /export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_2 with time limit 88
% 0.66/11.05 -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=88', '/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_2']
% 0.66/11.05 -prover status CounterSatisfiable
% 0.66/11.05 --creating new selector for [CSR006+0.ax]
% 0.89/17.02 -running prover on /export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_3 with time limit 115
% 0.89/17.02 -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=115', '/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_3']
% 0.89/17.02 -prover status CounterSatisfiable
% 0.89/17.02 --creating new selector for [CSR006+0.ax]
% 0.99/17.36 -running prover on /export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_4 with time limit 141
% 0.99/17.36 -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=141', '/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_4']
% 0.99/17.36 -prover status CounterSatisfiable
% 0.99/17.36 --creating new selector for [CSR006+0.ax]
% 55.87/72.10 -running prover on /export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5 with time limit 282
% 55.87/72.10 -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=282', '/export/starexec/sandbox2/tmp/tmp618XP7/sel_theBenchmark.p_5']
% 55.87/72.10 -prover status Theorem
% 55.87/72.10 Problem theBenchmark.p solved in phase 4.
% 55.87/72.10 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 55.87/72.10 % SZS status Ended for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 55.87/72.10 Solved 1 out of 1.
% 55.87/72.10 # Problem is unsatisfiable (or provable), constructing proof object
% 55.87/72.10 # SZS status Theorem
% 55.87/72.10 # SZS output start CNFRefutation.
% See solution above
% 55.87/72.13 # SZS output end CNFRefutation
%------------------------------------------------------------------------------