%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR193+1 : TPTP v7.3.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sine.py -e eprover -t %d %s
% Computer : n188.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.5MB
% OS : Linux 3.10.0-862.11.6.el7.x86_64
% CPULimit : 300s
% DateTime : Wed Feb 27 12:29:18 EST 2019
% Result : Theorem 134.86s
% Output : CNFRefutation 134.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 16
% Syntax : Number of formulae : 93 ( 29 unt; 0 def)
% Number of atoms : 737 ( 0 equ)
% Maximal formula atoms : 110 ( 7 avg)
% Number of connectives : 991 ( 347 ~; 336 |; 289 &)
% ( 12 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 68 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 22 ( 21 usr; 1 prp; 0-7 aty)
% Number of functors : 18 ( 18 usr; 16 con; 0-2 aty)
% Number of variables : 348 ( 3 sgn 307 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(11,axiom,
p__d__subclass(c__PetroleumProduct,c__Oil),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',miloA258) ).
fof(68,axiom,
p__d__subclass(c__Oil,c__Solution),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',miloA1360) ).
fof(220,axiom,
! [X1,X2] :
( p__part(X1,X2)
=> ( p__d__instance(X2,c__Object)
& p__d__instance(X1,c__Object) ) ),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',typeA5) ).
fof(249,axiom,
p__d__partition3(c__Substance,c__PureSubstance,c__Mixture),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',mergeA227) ).
fof(297,axiom,
p__d__subclass(c__FossilFuel,c__PetroleumProduct),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',miloA261) ).
fof(543,axiom,
! [X20,X123] :
( ( p__d__instance(X123,c__Object)
& p__d__instance(X20,c__ChemicalProcess)
& ( p__resource(X20,X123)
| p__result(X20,X123) ) )
=> p__d__instance(X123,c__PureSubstance) ),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',mergeA2632) ).
fof(548,axiom,
p__d__subclass(c__ChemicalDecomposition,c__ChemicalProcess),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',mergeA2637) ).
fof(619,axiom,
! [X52] :
( p__d__instance(X52,c__PetroleumProduct)
=> ? [X41] :
( p__d__instance(X41,c__OrganicCompound)
& p__part(X41,X52) ) ),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',miloA259) ).
fof(697,axiom,
( ! [X29,X245,X246] :
( p__d__partition3(X29,X245,X246)
<=> ( p__d__exhaustiveDecomposition3(X29,X245,X246)
& p__d__disjointDecomposition3(X29,X245,X246) ) )
& ! [X29,X245,X246,X247] :
( p__d__partition4(X29,X245,X246,X247)
<=> ( p__d__exhaustiveDecomposition4(X29,X245,X246,X247)
& p__d__disjointDecomposition4(X29,X245,X246,X247) ) )
& ! [X29,X245,X246,X247,X248] :
( p__d__partition5(X29,X245,X246,X247,X248)
<=> ( p__d__exhaustiveDecomposition5(X29,X245,X246,X247,X248)
& p__d__disjointDecomposition5(X29,X245,X246,X247,X248) ) )
& ! [X29,X245,X246,X247,X248,X249] :
( p__d__partition6(X29,X245,X246,X247,X248,X249)
<=> ( p__d__exhaustiveDecomposition6(X29,X245,X246,X247,X248,X249)
& p__d__disjointDecomposition6(X29,X245,X246,X247,X248,X249) ) )
& ! [X29,X245,X246,X247,X248,X249,X250] :
( p__d__partition7(X29,X245,X246,X247,X248,X249,X250)
<=> ( p__d__exhaustiveDecomposition7(X29,X245,X246,X247,X248,X249,X250)
& p__d__disjointDecomposition7(X29,X245,X246,X247,X248,X249,X250) ) ) ),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',predefinitionsA18) ).
fof(698,axiom,
! [X251,X252] :
( p__d__disjoint(X251,X252)
<=> ! [X186] :
( ~ p__d__instance(X186,X251)
| ~ p__d__instance(X186,X252) ) ),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',predefinitionsA15) ).
fof(699,axiom,
! [X18,X19,X185] :
( ( p__d__instance(X18,X19)
& p__d__subclass(X19,X185) )
=> p__d__instance(X18,X185) ),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',predefinitionsA12) ).
fof(898,axiom,
p__d__subclass(c__Combustion,c__ChemicalDecomposition),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',mergeA2640) ).
fof(908,axiom,
p__d__subclass(c__LiquidMixture,c__Mixture),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',mergeA2993) ).
fof(911,axiom,
p__d__subclass(c__Solution,c__LiquidMixture),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',mergeA2996) ).
fof(1033,axiom,
( ! [X29,X245,X246] :
( p__d__disjointDecomposition3(X29,X245,X246)
<=> p__d__disjoint(X245,X246) )
& ! [X29,X245,X246,X247] :
( p__d__disjointDecomposition4(X29,X245,X246,X247)
<=> ( p__d__disjoint(X245,X246)
& p__d__disjoint(X245,X247)
& p__d__disjoint(X246,X247) ) )
& ! [X29,X245,X246,X247,X248] :
( p__d__disjointDecomposition5(X29,X245,X246,X247,X248)
<=> ( p__d__disjoint(X245,X246)
& p__d__disjoint(X245,X247)
& p__d__disjoint(X245,X248)
& p__d__disjoint(X246,X247)
& p__d__disjoint(X246,X248)
& p__d__disjoint(X247,X248) ) )
& ! [X29,X245,X246,X247,X248,X249] :
( p__d__disjointDecomposition6(X29,X245,X246,X247,X248,X249)
<=> ( p__d__disjoint(X245,X246)
& p__d__disjoint(X245,X247)
& p__d__disjoint(X245,X248)
& p__d__disjoint(X245,X249)
& p__d__disjoint(X246,X247)
& p__d__disjoint(X246,X248)
& p__d__disjoint(X246,X249)
& p__d__disjoint(X247,X248)
& p__d__disjoint(X247,X249)
& p__d__disjoint(X248,X249) ) )
& ! [X29,X245,X246,X247,X248,X249,X250] :
( p__d__disjointDecomposition7(X29,X245,X246,X247,X248,X249,X250)
<=> ( p__d__disjoint(X245,X246)
& p__d__disjoint(X245,X247)
& p__d__disjoint(X245,X248)
& p__d__disjoint(X245,X249)
& p__d__disjoint(X245,X250)
& p__d__disjoint(X246,X247)
& p__d__disjoint(X246,X248)
& p__d__disjoint(X246,X249)
& p__d__disjoint(X246,X250)
& p__d__disjoint(X247,X248)
& p__d__disjoint(X247,X249)
& p__d__disjoint(X247,X250)
& p__d__disjoint(X248,X249)
& p__d__disjoint(X248,X250)
& p__d__disjoint(X249,X250) ) ) ),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',predefinitionsA24) ).
fof(1102,conjecture,
! [X18,X19] :
( p__d__instance(X18,c__Process)
=> ( ~ p__d__instance(X18,c__Combustion)
| ~ p__d__instance(X19,c__FossilFuel)
| ~ p__result(X18,X19) ) ),
file('/export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4',negatedResultRelation0009) ).
fof(1103,negated_conjecture,
~ ! [X18,X19] :
( p__d__instance(X18,c__Process)
=> ( ~ p__d__instance(X18,c__Combustion)
| ~ p__d__instance(X19,c__FossilFuel)
| ~ p__result(X18,X19) ) ),
inference(assume_negation,[status(cth)],[1102]) ).
fof(1124,plain,
! [X251,X252] :
( p__d__disjoint(X251,X252)
<=> ! [X186] :
( ~ p__d__instance(X186,X251)
| ~ p__d__instance(X186,X252) ) ),
inference(fof_simplification,[status(thm)],[698,theory(equality)]) ).
fof(1136,negated_conjecture,
~ ! [X18,X19] :
( p__d__instance(X18,c__Process)
=> ( ~ p__d__instance(X18,c__Combustion)
| ~ p__d__instance(X19,c__FossilFuel)
| ~ p__result(X18,X19) ) ),
inference(fof_simplification,[status(thm)],[1103,theory(equality)]) ).
cnf(1176,plain,
p__d__subclass(c__PetroleumProduct,c__Oil),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(1325,plain,
p__d__subclass(c__Oil,c__Solution),
inference(split_conjunct,[status(thm)],[68]) ).
fof(1781,plain,
! [X1,X2] :
( ~ p__part(X1,X2)
| ( p__d__instance(X2,c__Object)
& p__d__instance(X1,c__Object) ) ),
inference(fof_nnf,[status(thm)],[220]) ).
fof(1782,plain,
! [X3,X4] :
( ~ p__part(X3,X4)
| ( p__d__instance(X4,c__Object)
& p__d__instance(X3,c__Object) ) ),
inference(variable_rename,[status(thm)],[1781]) ).
fof(1783,plain,
! [X3,X4] :
( ( p__d__instance(X4,c__Object)
| ~ p__part(X3,X4) )
& ( p__d__instance(X3,c__Object)
| ~ p__part(X3,X4) ) ),
inference(distribute,[status(thm)],[1782]) ).
cnf(1785,plain,
( p__d__instance(X2,c__Object)
| ~ p__part(X1,X2) ),
inference(split_conjunct,[status(thm)],[1783]) ).
cnf(1872,plain,
p__d__partition3(c__Substance,c__PureSubstance,c__Mixture),
inference(split_conjunct,[status(thm)],[249]) ).
cnf(2025,plain,
p__d__subclass(c__FossilFuel,c__PetroleumProduct),
inference(split_conjunct,[status(thm)],[297]) ).
fof(2690,plain,
! [X20,X123] :
( ~ p__d__instance(X123,c__Object)
| ~ p__d__instance(X20,c__ChemicalProcess)
| ( ~ p__resource(X20,X123)
& ~ p__result(X20,X123) )
| p__d__instance(X123,c__PureSubstance) ),
inference(fof_nnf,[status(thm)],[543]) ).
fof(2691,plain,
! [X124,X125] :
( ~ p__d__instance(X125,c__Object)
| ~ p__d__instance(X124,c__ChemicalProcess)
| ( ~ p__resource(X124,X125)
& ~ p__result(X124,X125) )
| p__d__instance(X125,c__PureSubstance) ),
inference(variable_rename,[status(thm)],[2690]) ).
fof(2692,plain,
! [X124,X125] :
( ( ~ p__resource(X124,X125)
| ~ p__d__instance(X125,c__Object)
| ~ p__d__instance(X124,c__ChemicalProcess)
| p__d__instance(X125,c__PureSubstance) )
& ( ~ p__result(X124,X125)
| ~ p__d__instance(X125,c__Object)
| ~ p__d__instance(X124,c__ChemicalProcess)
| p__d__instance(X125,c__PureSubstance) ) ),
inference(distribute,[status(thm)],[2691]) ).
cnf(2693,plain,
( p__d__instance(X1,c__PureSubstance)
| ~ p__d__instance(X2,c__ChemicalProcess)
| ~ p__d__instance(X1,c__Object)
| ~ p__result(X2,X1) ),
inference(split_conjunct,[status(thm)],[2692]) ).
cnf(2711,plain,
p__d__subclass(c__ChemicalDecomposition,c__ChemicalProcess),
inference(split_conjunct,[status(thm)],[548]) ).
fof(2872,plain,
! [X52] :
( ~ p__d__instance(X52,c__PetroleumProduct)
| ? [X41] :
( p__d__instance(X41,c__OrganicCompound)
& p__part(X41,X52) ) ),
inference(fof_nnf,[status(thm)],[619]) ).
fof(2873,plain,
! [X53] :
( ~ p__d__instance(X53,c__PetroleumProduct)
| ? [X54] :
( p__d__instance(X54,c__OrganicCompound)
& p__part(X54,X53) ) ),
inference(variable_rename,[status(thm)],[2872]) ).
fof(2874,plain,
! [X53] :
( ~ p__d__instance(X53,c__PetroleumProduct)
| ( p__d__instance(esk149_1(X53),c__OrganicCompound)
& p__part(esk149_1(X53),X53) ) ),
inference(skolemize,[status(esa)],[2873]) ).
fof(2875,plain,
! [X53] :
( ( p__d__instance(esk149_1(X53),c__OrganicCompound)
| ~ p__d__instance(X53,c__PetroleumProduct) )
& ( p__part(esk149_1(X53),X53)
| ~ p__d__instance(X53,c__PetroleumProduct) ) ),
inference(distribute,[status(thm)],[2874]) ).
cnf(2876,plain,
( p__part(esk149_1(X1),X1)
| ~ p__d__instance(X1,c__PetroleumProduct) ),
inference(split_conjunct,[status(thm)],[2875]) ).
fof(3069,plain,
( ! [X29,X245,X246] :
( ( ~ p__d__partition3(X29,X245,X246)
| ( p__d__exhaustiveDecomposition3(X29,X245,X246)
& p__d__disjointDecomposition3(X29,X245,X246) ) )
& ( ~ p__d__exhaustiveDecomposition3(X29,X245,X246)
| ~ p__d__disjointDecomposition3(X29,X245,X246)
| p__d__partition3(X29,X245,X246) ) )
& ! [X29,X245,X246,X247] :
( ( ~ p__d__partition4(X29,X245,X246,X247)
| ( p__d__exhaustiveDecomposition4(X29,X245,X246,X247)
& p__d__disjointDecomposition4(X29,X245,X246,X247) ) )
& ( ~ p__d__exhaustiveDecomposition4(X29,X245,X246,X247)
| ~ p__d__disjointDecomposition4(X29,X245,X246,X247)
| p__d__partition4(X29,X245,X246,X247) ) )
& ! [X29,X245,X246,X247,X248] :
( ( ~ p__d__partition5(X29,X245,X246,X247,X248)
| ( p__d__exhaustiveDecomposition5(X29,X245,X246,X247,X248)
& p__d__disjointDecomposition5(X29,X245,X246,X247,X248) ) )
& ( ~ p__d__exhaustiveDecomposition5(X29,X245,X246,X247,X248)
| ~ p__d__disjointDecomposition5(X29,X245,X246,X247,X248)
| p__d__partition5(X29,X245,X246,X247,X248) ) )
& ! [X29,X245,X246,X247,X248,X249] :
( ( ~ p__d__partition6(X29,X245,X246,X247,X248,X249)
| ( p__d__exhaustiveDecomposition6(X29,X245,X246,X247,X248,X249)
& p__d__disjointDecomposition6(X29,X245,X246,X247,X248,X249) ) )
& ( ~ p__d__exhaustiveDecomposition6(X29,X245,X246,X247,X248,X249)
| ~ p__d__disjointDecomposition6(X29,X245,X246,X247,X248,X249)
| p__d__partition6(X29,X245,X246,X247,X248,X249) ) )
& ! [X29,X245,X246,X247,X248,X249,X250] :
( ( ~ p__d__partition7(X29,X245,X246,X247,X248,X249,X250)
| ( p__d__exhaustiveDecomposition7(X29,X245,X246,X247,X248,X249,X250)
& p__d__disjointDecomposition7(X29,X245,X246,X247,X248,X249,X250) ) )
& ( ~ p__d__exhaustiveDecomposition7(X29,X245,X246,X247,X248,X249,X250)
| ~ p__d__disjointDecomposition7(X29,X245,X246,X247,X248,X249,X250)
| p__d__partition7(X29,X245,X246,X247,X248,X249,X250) ) ) ),
inference(fof_nnf,[status(thm)],[697]) ).
fof(3070,plain,
( ! [X251,X252,X253] :
( ( ~ p__d__partition3(X251,X252,X253)
| ( p__d__exhaustiveDecomposition3(X251,X252,X253)
& p__d__disjointDecomposition3(X251,X252,X253) ) )
& ( ~ p__d__exhaustiveDecomposition3(X251,X252,X253)
| ~ p__d__disjointDecomposition3(X251,X252,X253)
| p__d__partition3(X251,X252,X253) ) )
& ! [X254,X255,X256,X257] :
( ( ~ p__d__partition4(X254,X255,X256,X257)
| ( p__d__exhaustiveDecomposition4(X254,X255,X256,X257)
& p__d__disjointDecomposition4(X254,X255,X256,X257) ) )
& ( ~ p__d__exhaustiveDecomposition4(X254,X255,X256,X257)
| ~ p__d__disjointDecomposition4(X254,X255,X256,X257)
| p__d__partition4(X254,X255,X256,X257) ) )
& ! [X258,X259,X260,X261,X262] :
( ( ~ p__d__partition5(X258,X259,X260,X261,X262)
| ( p__d__exhaustiveDecomposition5(X258,X259,X260,X261,X262)
& p__d__disjointDecomposition5(X258,X259,X260,X261,X262) ) )
& ( ~ p__d__exhaustiveDecomposition5(X258,X259,X260,X261,X262)
| ~ p__d__disjointDecomposition5(X258,X259,X260,X261,X262)
| p__d__partition5(X258,X259,X260,X261,X262) ) )
& ! [X263,X264,X265,X266,X267,X268] :
( ( ~ p__d__partition6(X263,X264,X265,X266,X267,X268)
| ( p__d__exhaustiveDecomposition6(X263,X264,X265,X266,X267,X268)
& p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268) ) )
& ( ~ p__d__exhaustiveDecomposition6(X263,X264,X265,X266,X267,X268)
| ~ p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268)
| p__d__partition6(X263,X264,X265,X266,X267,X268) ) )
& ! [X269,X270,X271,X272,X273,X274,X275] :
( ( ~ p__d__partition7(X269,X270,X271,X272,X273,X274,X275)
| ( p__d__exhaustiveDecomposition7(X269,X270,X271,X272,X273,X274,X275)
& p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) ) )
& ( ~ p__d__exhaustiveDecomposition7(X269,X270,X271,X272,X273,X274,X275)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275)
| p__d__partition7(X269,X270,X271,X272,X273,X274,X275) ) ) ),
inference(variable_rename,[status(thm)],[3069]) ).
fof(3071,plain,
! [X251,X252,X253,X254,X255,X256,X257,X258,X259,X260,X261,X262,X263,X264,X265,X266,X267,X268,X269,X270,X271,X272,X273,X274,X275] :
( ( ~ p__d__partition7(X269,X270,X271,X272,X273,X274,X275)
| ( p__d__exhaustiveDecomposition7(X269,X270,X271,X272,X273,X274,X275)
& p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) ) )
& ( ~ p__d__exhaustiveDecomposition7(X269,X270,X271,X272,X273,X274,X275)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275)
| p__d__partition7(X269,X270,X271,X272,X273,X274,X275) )
& ( ~ p__d__partition6(X263,X264,X265,X266,X267,X268)
| ( p__d__exhaustiveDecomposition6(X263,X264,X265,X266,X267,X268)
& p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268) ) )
& ( ~ p__d__exhaustiveDecomposition6(X263,X264,X265,X266,X267,X268)
| ~ p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268)
| p__d__partition6(X263,X264,X265,X266,X267,X268) )
& ( ~ p__d__partition5(X258,X259,X260,X261,X262)
| ( p__d__exhaustiveDecomposition5(X258,X259,X260,X261,X262)
& p__d__disjointDecomposition5(X258,X259,X260,X261,X262) ) )
& ( ~ p__d__exhaustiveDecomposition5(X258,X259,X260,X261,X262)
| ~ p__d__disjointDecomposition5(X258,X259,X260,X261,X262)
| p__d__partition5(X258,X259,X260,X261,X262) )
& ( ~ p__d__partition4(X254,X255,X256,X257)
| ( p__d__exhaustiveDecomposition4(X254,X255,X256,X257)
& p__d__disjointDecomposition4(X254,X255,X256,X257) ) )
& ( ~ p__d__exhaustiveDecomposition4(X254,X255,X256,X257)
| ~ p__d__disjointDecomposition4(X254,X255,X256,X257)
| p__d__partition4(X254,X255,X256,X257) )
& ( ~ p__d__partition3(X251,X252,X253)
| ( p__d__exhaustiveDecomposition3(X251,X252,X253)
& p__d__disjointDecomposition3(X251,X252,X253) ) )
& ( ~ p__d__exhaustiveDecomposition3(X251,X252,X253)
| ~ p__d__disjointDecomposition3(X251,X252,X253)
| p__d__partition3(X251,X252,X253) ) ),
inference(shift_quantors,[status(thm)],[3070]) ).
fof(3072,plain,
! [X251,X252,X253,X254,X255,X256,X257,X258,X259,X260,X261,X262,X263,X264,X265,X266,X267,X268,X269,X270,X271,X272,X273,X274,X275] :
( ( p__d__exhaustiveDecomposition7(X269,X270,X271,X272,X273,X274,X275)
| ~ p__d__partition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275)
| ~ p__d__partition7(X269,X270,X271,X272,X273,X274,X275) )
& ( ~ p__d__exhaustiveDecomposition7(X269,X270,X271,X272,X273,X274,X275)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275)
| p__d__partition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__exhaustiveDecomposition6(X263,X264,X265,X266,X267,X268)
| ~ p__d__partition6(X263,X264,X265,X266,X267,X268) )
& ( p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268)
| ~ p__d__partition6(X263,X264,X265,X266,X267,X268) )
& ( ~ p__d__exhaustiveDecomposition6(X263,X264,X265,X266,X267,X268)
| ~ p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268)
| p__d__partition6(X263,X264,X265,X266,X267,X268) )
& ( p__d__exhaustiveDecomposition5(X258,X259,X260,X261,X262)
| ~ p__d__partition5(X258,X259,X260,X261,X262) )
& ( p__d__disjointDecomposition5(X258,X259,X260,X261,X262)
| ~ p__d__partition5(X258,X259,X260,X261,X262) )
& ( ~ p__d__exhaustiveDecomposition5(X258,X259,X260,X261,X262)
| ~ p__d__disjointDecomposition5(X258,X259,X260,X261,X262)
| p__d__partition5(X258,X259,X260,X261,X262) )
& ( p__d__exhaustiveDecomposition4(X254,X255,X256,X257)
| ~ p__d__partition4(X254,X255,X256,X257) )
& ( p__d__disjointDecomposition4(X254,X255,X256,X257)
| ~ p__d__partition4(X254,X255,X256,X257) )
& ( ~ p__d__exhaustiveDecomposition4(X254,X255,X256,X257)
| ~ p__d__disjointDecomposition4(X254,X255,X256,X257)
| p__d__partition4(X254,X255,X256,X257) )
& ( p__d__exhaustiveDecomposition3(X251,X252,X253)
| ~ p__d__partition3(X251,X252,X253) )
& ( p__d__disjointDecomposition3(X251,X252,X253)
| ~ p__d__partition3(X251,X252,X253) )
& ( ~ p__d__exhaustiveDecomposition3(X251,X252,X253)
| ~ p__d__disjointDecomposition3(X251,X252,X253)
| p__d__partition3(X251,X252,X253) ) ),
inference(distribute,[status(thm)],[3071]) ).
cnf(3074,plain,
( p__d__disjointDecomposition3(X1,X2,X3)
| ~ p__d__partition3(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[3072]) ).
fof(3088,plain,
! [X251,X252] :
( ( ~ p__d__disjoint(X251,X252)
| ! [X186] :
( ~ p__d__instance(X186,X251)
| ~ p__d__instance(X186,X252) ) )
& ( ? [X186] :
( p__d__instance(X186,X251)
& p__d__instance(X186,X252) )
| p__d__disjoint(X251,X252) ) ),
inference(fof_nnf,[status(thm)],[1124]) ).
fof(3089,plain,
! [X253,X254] :
( ( ~ p__d__disjoint(X253,X254)
| ! [X255] :
( ~ p__d__instance(X255,X253)
| ~ p__d__instance(X255,X254) ) )
& ( ? [X256] :
( p__d__instance(X256,X253)
& p__d__instance(X256,X254) )
| p__d__disjoint(X253,X254) ) ),
inference(variable_rename,[status(thm)],[3088]) ).
fof(3090,plain,
! [X253,X254] :
( ( ~ p__d__disjoint(X253,X254)
| ! [X255] :
( ~ p__d__instance(X255,X253)
| ~ p__d__instance(X255,X254) ) )
& ( ( p__d__instance(esk167_2(X253,X254),X253)
& p__d__instance(esk167_2(X253,X254),X254) )
| p__d__disjoint(X253,X254) ) ),
inference(skolemize,[status(esa)],[3089]) ).
fof(3091,plain,
! [X253,X254,X255] :
( ( ~ p__d__instance(X255,X253)
| ~ p__d__instance(X255,X254)
| ~ p__d__disjoint(X253,X254) )
& ( ( p__d__instance(esk167_2(X253,X254),X253)
& p__d__instance(esk167_2(X253,X254),X254) )
| p__d__disjoint(X253,X254) ) ),
inference(shift_quantors,[status(thm)],[3090]) ).
fof(3092,plain,
! [X253,X254,X255] :
( ( ~ p__d__instance(X255,X253)
| ~ p__d__instance(X255,X254)
| ~ p__d__disjoint(X253,X254) )
& ( p__d__instance(esk167_2(X253,X254),X253)
| p__d__disjoint(X253,X254) )
& ( p__d__instance(esk167_2(X253,X254),X254)
| p__d__disjoint(X253,X254) ) ),
inference(distribute,[status(thm)],[3091]) ).
cnf(3095,plain,
( ~ p__d__disjoint(X1,X2)
| ~ p__d__instance(X3,X2)
| ~ p__d__instance(X3,X1) ),
inference(split_conjunct,[status(thm)],[3092]) ).
fof(3096,plain,
! [X18,X19,X185] :
( ~ p__d__instance(X18,X19)
| ~ p__d__subclass(X19,X185)
| p__d__instance(X18,X185) ),
inference(fof_nnf,[status(thm)],[699]) ).
fof(3097,plain,
! [X186,X187,X188] :
( ~ p__d__instance(X186,X187)
| ~ p__d__subclass(X187,X188)
| p__d__instance(X186,X188) ),
inference(variable_rename,[status(thm)],[3096]) ).
cnf(3098,plain,
( p__d__instance(X1,X2)
| ~ p__d__subclass(X3,X2)
| ~ p__d__instance(X1,X3) ),
inference(split_conjunct,[status(thm)],[3097]) ).
cnf(3567,plain,
p__d__subclass(c__Combustion,c__ChemicalDecomposition),
inference(split_conjunct,[status(thm)],[898]) ).
cnf(3577,plain,
p__d__subclass(c__LiquidMixture,c__Mixture),
inference(split_conjunct,[status(thm)],[908]) ).
cnf(3584,plain,
p__d__subclass(c__Solution,c__LiquidMixture),
inference(split_conjunct,[status(thm)],[911]) ).
fof(3967,plain,
( ! [X29,X245,X246] :
( ( ~ p__d__disjointDecomposition3(X29,X245,X246)
| p__d__disjoint(X245,X246) )
& ( ~ p__d__disjoint(X245,X246)
| p__d__disjointDecomposition3(X29,X245,X246) ) )
& ! [X29,X245,X246,X247] :
( ( ~ p__d__disjointDecomposition4(X29,X245,X246,X247)
| ( p__d__disjoint(X245,X246)
& p__d__disjoint(X245,X247)
& p__d__disjoint(X246,X247) ) )
& ( ~ p__d__disjoint(X245,X246)
| ~ p__d__disjoint(X245,X247)
| ~ p__d__disjoint(X246,X247)
| p__d__disjointDecomposition4(X29,X245,X246,X247) ) )
& ! [X29,X245,X246,X247,X248] :
( ( ~ p__d__disjointDecomposition5(X29,X245,X246,X247,X248)
| ( p__d__disjoint(X245,X246)
& p__d__disjoint(X245,X247)
& p__d__disjoint(X245,X248)
& p__d__disjoint(X246,X247)
& p__d__disjoint(X246,X248)
& p__d__disjoint(X247,X248) ) )
& ( ~ p__d__disjoint(X245,X246)
| ~ p__d__disjoint(X245,X247)
| ~ p__d__disjoint(X245,X248)
| ~ p__d__disjoint(X246,X247)
| ~ p__d__disjoint(X246,X248)
| ~ p__d__disjoint(X247,X248)
| p__d__disjointDecomposition5(X29,X245,X246,X247,X248) ) )
& ! [X29,X245,X246,X247,X248,X249] :
( ( ~ p__d__disjointDecomposition6(X29,X245,X246,X247,X248,X249)
| ( p__d__disjoint(X245,X246)
& p__d__disjoint(X245,X247)
& p__d__disjoint(X245,X248)
& p__d__disjoint(X245,X249)
& p__d__disjoint(X246,X247)
& p__d__disjoint(X246,X248)
& p__d__disjoint(X246,X249)
& p__d__disjoint(X247,X248)
& p__d__disjoint(X247,X249)
& p__d__disjoint(X248,X249) ) )
& ( ~ p__d__disjoint(X245,X246)
| ~ p__d__disjoint(X245,X247)
| ~ p__d__disjoint(X245,X248)
| ~ p__d__disjoint(X245,X249)
| ~ p__d__disjoint(X246,X247)
| ~ p__d__disjoint(X246,X248)
| ~ p__d__disjoint(X246,X249)
| ~ p__d__disjoint(X247,X248)
| ~ p__d__disjoint(X247,X249)
| ~ p__d__disjoint(X248,X249)
| p__d__disjointDecomposition6(X29,X245,X246,X247,X248,X249) ) )
& ! [X29,X245,X246,X247,X248,X249,X250] :
( ( ~ p__d__disjointDecomposition7(X29,X245,X246,X247,X248,X249,X250)
| ( p__d__disjoint(X245,X246)
& p__d__disjoint(X245,X247)
& p__d__disjoint(X245,X248)
& p__d__disjoint(X245,X249)
& p__d__disjoint(X245,X250)
& p__d__disjoint(X246,X247)
& p__d__disjoint(X246,X248)
& p__d__disjoint(X246,X249)
& p__d__disjoint(X246,X250)
& p__d__disjoint(X247,X248)
& p__d__disjoint(X247,X249)
& p__d__disjoint(X247,X250)
& p__d__disjoint(X248,X249)
& p__d__disjoint(X248,X250)
& p__d__disjoint(X249,X250) ) )
& ( ~ p__d__disjoint(X245,X246)
| ~ p__d__disjoint(X245,X247)
| ~ p__d__disjoint(X245,X248)
| ~ p__d__disjoint(X245,X249)
| ~ p__d__disjoint(X245,X250)
| ~ p__d__disjoint(X246,X247)
| ~ p__d__disjoint(X246,X248)
| ~ p__d__disjoint(X246,X249)
| ~ p__d__disjoint(X246,X250)
| ~ p__d__disjoint(X247,X248)
| ~ p__d__disjoint(X247,X249)
| ~ p__d__disjoint(X247,X250)
| ~ p__d__disjoint(X248,X249)
| ~ p__d__disjoint(X248,X250)
| ~ p__d__disjoint(X249,X250)
| p__d__disjointDecomposition7(X29,X245,X246,X247,X248,X249,X250) ) ) ),
inference(fof_nnf,[status(thm)],[1033]) ).
fof(3968,plain,
( ! [X251,X252,X253] :
( ( ~ p__d__disjointDecomposition3(X251,X252,X253)
| p__d__disjoint(X252,X253) )
& ( ~ p__d__disjoint(X252,X253)
| p__d__disjointDecomposition3(X251,X252,X253) ) )
& ! [X254,X255,X256,X257] :
( ( ~ p__d__disjointDecomposition4(X254,X255,X256,X257)
| ( p__d__disjoint(X255,X256)
& p__d__disjoint(X255,X257)
& p__d__disjoint(X256,X257) ) )
& ( ~ p__d__disjoint(X255,X256)
| ~ p__d__disjoint(X255,X257)
| ~ p__d__disjoint(X256,X257)
| p__d__disjointDecomposition4(X254,X255,X256,X257) ) )
& ! [X258,X259,X260,X261,X262] :
( ( ~ p__d__disjointDecomposition5(X258,X259,X260,X261,X262)
| ( p__d__disjoint(X259,X260)
& p__d__disjoint(X259,X261)
& p__d__disjoint(X259,X262)
& p__d__disjoint(X260,X261)
& p__d__disjoint(X260,X262)
& p__d__disjoint(X261,X262) ) )
& ( ~ p__d__disjoint(X259,X260)
| ~ p__d__disjoint(X259,X261)
| ~ p__d__disjoint(X259,X262)
| ~ p__d__disjoint(X260,X261)
| ~ p__d__disjoint(X260,X262)
| ~ p__d__disjoint(X261,X262)
| p__d__disjointDecomposition5(X258,X259,X260,X261,X262) ) )
& ! [X263,X264,X265,X266,X267,X268] :
( ( ~ p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268)
| ( p__d__disjoint(X264,X265)
& p__d__disjoint(X264,X266)
& p__d__disjoint(X264,X267)
& p__d__disjoint(X264,X268)
& p__d__disjoint(X265,X266)
& p__d__disjoint(X265,X267)
& p__d__disjoint(X265,X268)
& p__d__disjoint(X266,X267)
& p__d__disjoint(X266,X268)
& p__d__disjoint(X267,X268) ) )
& ( ~ p__d__disjoint(X264,X265)
| ~ p__d__disjoint(X264,X266)
| ~ p__d__disjoint(X264,X267)
| ~ p__d__disjoint(X264,X268)
| ~ p__d__disjoint(X265,X266)
| ~ p__d__disjoint(X265,X267)
| ~ p__d__disjoint(X265,X268)
| ~ p__d__disjoint(X266,X267)
| ~ p__d__disjoint(X266,X268)
| ~ p__d__disjoint(X267,X268)
| p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268) ) )
& ! [X269,X270,X271,X272,X273,X274,X275] :
( ( ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275)
| ( p__d__disjoint(X270,X271)
& p__d__disjoint(X270,X272)
& p__d__disjoint(X270,X273)
& p__d__disjoint(X270,X274)
& p__d__disjoint(X270,X275)
& p__d__disjoint(X271,X272)
& p__d__disjoint(X271,X273)
& p__d__disjoint(X271,X274)
& p__d__disjoint(X271,X275)
& p__d__disjoint(X272,X273)
& p__d__disjoint(X272,X274)
& p__d__disjoint(X272,X275)
& p__d__disjoint(X273,X274)
& p__d__disjoint(X273,X275)
& p__d__disjoint(X274,X275) ) )
& ( ~ p__d__disjoint(X270,X271)
| ~ p__d__disjoint(X270,X272)
| ~ p__d__disjoint(X270,X273)
| ~ p__d__disjoint(X270,X274)
| ~ p__d__disjoint(X270,X275)
| ~ p__d__disjoint(X271,X272)
| ~ p__d__disjoint(X271,X273)
| ~ p__d__disjoint(X271,X274)
| ~ p__d__disjoint(X271,X275)
| ~ p__d__disjoint(X272,X273)
| ~ p__d__disjoint(X272,X274)
| ~ p__d__disjoint(X272,X275)
| ~ p__d__disjoint(X273,X274)
| ~ p__d__disjoint(X273,X275)
| ~ p__d__disjoint(X274,X275)
| p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) ) ) ),
inference(variable_rename,[status(thm)],[3967]) ).
fof(3969,plain,
! [X251,X252,X253,X254,X255,X256,X257,X258,X259,X260,X261,X262,X263,X264,X265,X266,X267,X268,X269,X270,X271,X272,X273,X274,X275] :
( ( ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275)
| ( p__d__disjoint(X270,X271)
& p__d__disjoint(X270,X272)
& p__d__disjoint(X270,X273)
& p__d__disjoint(X270,X274)
& p__d__disjoint(X270,X275)
& p__d__disjoint(X271,X272)
& p__d__disjoint(X271,X273)
& p__d__disjoint(X271,X274)
& p__d__disjoint(X271,X275)
& p__d__disjoint(X272,X273)
& p__d__disjoint(X272,X274)
& p__d__disjoint(X272,X275)
& p__d__disjoint(X273,X274)
& p__d__disjoint(X273,X275)
& p__d__disjoint(X274,X275) ) )
& ( ~ p__d__disjoint(X270,X271)
| ~ p__d__disjoint(X270,X272)
| ~ p__d__disjoint(X270,X273)
| ~ p__d__disjoint(X270,X274)
| ~ p__d__disjoint(X270,X275)
| ~ p__d__disjoint(X271,X272)
| ~ p__d__disjoint(X271,X273)
| ~ p__d__disjoint(X271,X274)
| ~ p__d__disjoint(X271,X275)
| ~ p__d__disjoint(X272,X273)
| ~ p__d__disjoint(X272,X274)
| ~ p__d__disjoint(X272,X275)
| ~ p__d__disjoint(X273,X274)
| ~ p__d__disjoint(X273,X275)
| ~ p__d__disjoint(X274,X275)
| p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( ~ p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268)
| ( p__d__disjoint(X264,X265)
& p__d__disjoint(X264,X266)
& p__d__disjoint(X264,X267)
& p__d__disjoint(X264,X268)
& p__d__disjoint(X265,X266)
& p__d__disjoint(X265,X267)
& p__d__disjoint(X265,X268)
& p__d__disjoint(X266,X267)
& p__d__disjoint(X266,X268)
& p__d__disjoint(X267,X268) ) )
& ( ~ p__d__disjoint(X264,X265)
| ~ p__d__disjoint(X264,X266)
| ~ p__d__disjoint(X264,X267)
| ~ p__d__disjoint(X264,X268)
| ~ p__d__disjoint(X265,X266)
| ~ p__d__disjoint(X265,X267)
| ~ p__d__disjoint(X265,X268)
| ~ p__d__disjoint(X266,X267)
| ~ p__d__disjoint(X266,X268)
| ~ p__d__disjoint(X267,X268)
| p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268) )
& ( ~ p__d__disjointDecomposition5(X258,X259,X260,X261,X262)
| ( p__d__disjoint(X259,X260)
& p__d__disjoint(X259,X261)
& p__d__disjoint(X259,X262)
& p__d__disjoint(X260,X261)
& p__d__disjoint(X260,X262)
& p__d__disjoint(X261,X262) ) )
& ( ~ p__d__disjoint(X259,X260)
| ~ p__d__disjoint(X259,X261)
| ~ p__d__disjoint(X259,X262)
| ~ p__d__disjoint(X260,X261)
| ~ p__d__disjoint(X260,X262)
| ~ p__d__disjoint(X261,X262)
| p__d__disjointDecomposition5(X258,X259,X260,X261,X262) )
& ( ~ p__d__disjointDecomposition4(X254,X255,X256,X257)
| ( p__d__disjoint(X255,X256)
& p__d__disjoint(X255,X257)
& p__d__disjoint(X256,X257) ) )
& ( ~ p__d__disjoint(X255,X256)
| ~ p__d__disjoint(X255,X257)
| ~ p__d__disjoint(X256,X257)
| p__d__disjointDecomposition4(X254,X255,X256,X257) )
& ( ~ p__d__disjointDecomposition3(X251,X252,X253)
| p__d__disjoint(X252,X253) )
& ( ~ p__d__disjoint(X252,X253)
| p__d__disjointDecomposition3(X251,X252,X253) ) ),
inference(shift_quantors,[status(thm)],[3968]) ).
fof(3970,plain,
! [X251,X252,X253,X254,X255,X256,X257,X258,X259,X260,X261,X262,X263,X264,X265,X266,X267,X268,X269,X270,X271,X272,X273,X274,X275] :
( ( p__d__disjoint(X270,X271)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjoint(X270,X272)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjoint(X270,X273)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjoint(X270,X274)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjoint(X270,X275)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjoint(X271,X272)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjoint(X271,X273)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjoint(X271,X274)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjoint(X271,X275)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjoint(X272,X273)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjoint(X272,X274)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjoint(X272,X275)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjoint(X273,X274)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjoint(X273,X275)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjoint(X274,X275)
| ~ p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( ~ p__d__disjoint(X270,X271)
| ~ p__d__disjoint(X270,X272)
| ~ p__d__disjoint(X270,X273)
| ~ p__d__disjoint(X270,X274)
| ~ p__d__disjoint(X270,X275)
| ~ p__d__disjoint(X271,X272)
| ~ p__d__disjoint(X271,X273)
| ~ p__d__disjoint(X271,X274)
| ~ p__d__disjoint(X271,X275)
| ~ p__d__disjoint(X272,X273)
| ~ p__d__disjoint(X272,X274)
| ~ p__d__disjoint(X272,X275)
| ~ p__d__disjoint(X273,X274)
| ~ p__d__disjoint(X273,X275)
| ~ p__d__disjoint(X274,X275)
| p__d__disjointDecomposition7(X269,X270,X271,X272,X273,X274,X275) )
& ( p__d__disjoint(X264,X265)
| ~ p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268) )
& ( p__d__disjoint(X264,X266)
| ~ p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268) )
& ( p__d__disjoint(X264,X267)
| ~ p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268) )
& ( p__d__disjoint(X264,X268)
| ~ p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268) )
& ( p__d__disjoint(X265,X266)
| ~ p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268) )
& ( p__d__disjoint(X265,X267)
| ~ p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268) )
& ( p__d__disjoint(X265,X268)
| ~ p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268) )
& ( p__d__disjoint(X266,X267)
| ~ p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268) )
& ( p__d__disjoint(X266,X268)
| ~ p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268) )
& ( p__d__disjoint(X267,X268)
| ~ p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268) )
& ( ~ p__d__disjoint(X264,X265)
| ~ p__d__disjoint(X264,X266)
| ~ p__d__disjoint(X264,X267)
| ~ p__d__disjoint(X264,X268)
| ~ p__d__disjoint(X265,X266)
| ~ p__d__disjoint(X265,X267)
| ~ p__d__disjoint(X265,X268)
| ~ p__d__disjoint(X266,X267)
| ~ p__d__disjoint(X266,X268)
| ~ p__d__disjoint(X267,X268)
| p__d__disjointDecomposition6(X263,X264,X265,X266,X267,X268) )
& ( p__d__disjoint(X259,X260)
| ~ p__d__disjointDecomposition5(X258,X259,X260,X261,X262) )
& ( p__d__disjoint(X259,X261)
| ~ p__d__disjointDecomposition5(X258,X259,X260,X261,X262) )
& ( p__d__disjoint(X259,X262)
| ~ p__d__disjointDecomposition5(X258,X259,X260,X261,X262) )
& ( p__d__disjoint(X260,X261)
| ~ p__d__disjointDecomposition5(X258,X259,X260,X261,X262) )
& ( p__d__disjoint(X260,X262)
| ~ p__d__disjointDecomposition5(X258,X259,X260,X261,X262) )
& ( p__d__disjoint(X261,X262)
| ~ p__d__disjointDecomposition5(X258,X259,X260,X261,X262) )
& ( ~ p__d__disjoint(X259,X260)
| ~ p__d__disjoint(X259,X261)
| ~ p__d__disjoint(X259,X262)
| ~ p__d__disjoint(X260,X261)
| ~ p__d__disjoint(X260,X262)
| ~ p__d__disjoint(X261,X262)
| p__d__disjointDecomposition5(X258,X259,X260,X261,X262) )
& ( p__d__disjoint(X255,X256)
| ~ p__d__disjointDecomposition4(X254,X255,X256,X257) )
& ( p__d__disjoint(X255,X257)
| ~ p__d__disjointDecomposition4(X254,X255,X256,X257) )
& ( p__d__disjoint(X256,X257)
| ~ p__d__disjointDecomposition4(X254,X255,X256,X257) )
& ( ~ p__d__disjoint(X255,X256)
| ~ p__d__disjoint(X255,X257)
| ~ p__d__disjoint(X256,X257)
| p__d__disjointDecomposition4(X254,X255,X256,X257) )
& ( ~ p__d__disjointDecomposition3(X251,X252,X253)
| p__d__disjoint(X252,X253) )
& ( ~ p__d__disjoint(X252,X253)
| p__d__disjointDecomposition3(X251,X252,X253) ) ),
inference(distribute,[status(thm)],[3969]) ).
cnf(3972,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__disjointDecomposition3(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[3970]) ).
fof(4163,negated_conjecture,
? [X18,X19] :
( p__d__instance(X18,c__Process)
& p__d__instance(X18,c__Combustion)
& p__d__instance(X19,c__FossilFuel)
& p__result(X18,X19) ),
inference(fof_nnf,[status(thm)],[1136]) ).
fof(4164,negated_conjecture,
? [X20,X21] :
( p__d__instance(X20,c__Process)
& p__d__instance(X20,c__Combustion)
& p__d__instance(X21,c__FossilFuel)
& p__result(X20,X21) ),
inference(variable_rename,[status(thm)],[4163]) ).
fof(4165,negated_conjecture,
( p__d__instance(esk241_0,c__Process)
& p__d__instance(esk241_0,c__Combustion)
& p__d__instance(esk242_0,c__FossilFuel)
& p__result(esk241_0,esk242_0) ),
inference(skolemize,[status(esa)],[4164]) ).
cnf(4166,negated_conjecture,
p__result(esk241_0,esk242_0),
inference(split_conjunct,[status(thm)],[4165]) ).
cnf(4167,negated_conjecture,
p__d__instance(esk242_0,c__FossilFuel),
inference(split_conjunct,[status(thm)],[4165]) ).
cnf(4168,negated_conjecture,
p__d__instance(esk241_0,c__Combustion),
inference(split_conjunct,[status(thm)],[4165]) ).
cnf(4339,plain,
( p__d__instance(X1,c__PetroleumProduct)
| ~ p__d__instance(X1,c__FossilFuel) ),
inference(spm,[status(thm)],[3098,2025,theory(equality)]) ).
cnf(4340,plain,
( p__d__instance(X1,c__ChemicalDecomposition)
| ~ p__d__instance(X1,c__Combustion) ),
inference(spm,[status(thm)],[3098,3567,theory(equality)]) ).
cnf(4350,plain,
( p__d__instance(X1,c__Oil)
| ~ p__d__instance(X1,c__PetroleumProduct) ),
inference(spm,[status(thm)],[3098,1176,theory(equality)]) ).
cnf(4351,plain,
( p__d__instance(X1,c__Solution)
| ~ p__d__instance(X1,c__Oil) ),
inference(spm,[status(thm)],[3098,1325,theory(equality)]) ).
cnf(4418,plain,
( p__d__instance(X1,c__ChemicalProcess)
| ~ p__d__instance(X1,c__ChemicalDecomposition) ),
inference(spm,[status(thm)],[3098,2711,theory(equality)]) ).
cnf(4445,plain,
( p__d__instance(X1,c__LiquidMixture)
| ~ p__d__instance(X1,c__Solution) ),
inference(spm,[status(thm)],[3098,3584,theory(equality)]) ).
cnf(4769,plain,
( p__d__instance(X1,c__Mixture)
| ~ p__d__instance(X1,c__LiquidMixture) ),
inference(spm,[status(thm)],[3098,3577,theory(equality)]) ).
cnf(5019,plain,
( p__d__instance(X1,c__Object)
| ~ p__d__instance(X1,c__PetroleumProduct) ),
inference(spm,[status(thm)],[1785,2876,theory(equality)]) ).
cnf(5618,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__partition3(X3,X1,X2) ),
inference(spm,[status(thm)],[3972,3074,theory(equality)]) ).
cnf(5764,negated_conjecture,
( p__d__instance(esk242_0,c__PureSubstance)
| ~ p__d__instance(esk241_0,c__ChemicalProcess)
| ~ p__d__instance(esk242_0,c__Object) ),
inference(spm,[status(thm)],[2693,4166,theory(equality)]) ).
cnf(11003,negated_conjecture,
p__d__instance(esk242_0,c__PetroleumProduct),
inference(spm,[status(thm)],[4339,4167,theory(equality)]) ).
cnf(14480,plain,
( p__d__instance(X1,c__ChemicalProcess)
| ~ p__d__instance(X1,c__Combustion) ),
inference(spm,[status(thm)],[4418,4340,theory(equality)]) ).
cnf(15331,plain,
( p__d__instance(X1,c__LiquidMixture)
| ~ p__d__instance(X1,c__Oil) ),
inference(spm,[status(thm)],[4445,4351,theory(equality)]) ).
cnf(24849,negated_conjecture,
p__d__instance(esk242_0,c__Object),
inference(spm,[status(thm)],[5019,11003,theory(equality)]) ).
cnf(26786,plain,
( p__d__instance(X1,c__LiquidMixture)
| ~ p__d__instance(X1,c__PetroleumProduct) ),
inference(spm,[status(thm)],[15331,4350,theory(equality)]) ).
cnf(28127,plain,
p__d__disjoint(c__PureSubstance,c__Mixture),
inference(spm,[status(thm)],[5618,1872,theory(equality)]) ).
cnf(28156,plain,
( ~ p__d__instance(X1,c__Mixture)
| ~ p__d__instance(X1,c__PureSubstance) ),
inference(spm,[status(thm)],[3095,28127,theory(equality)]) ).
cnf(32073,negated_conjecture,
( p__d__instance(esk242_0,c__PureSubstance)
| ~ p__d__instance(esk241_0,c__ChemicalProcess)
| $false ),
inference(rw,[status(thm)],[5764,24849,theory(equality)]) ).
cnf(32074,negated_conjecture,
( p__d__instance(esk242_0,c__PureSubstance)
| ~ p__d__instance(esk241_0,c__ChemicalProcess) ),
inference(cn,[status(thm)],[32073,theory(equality)]) ).
cnf(32076,negated_conjecture,
( ~ p__d__instance(esk242_0,c__Mixture)
| ~ p__d__instance(esk241_0,c__ChemicalProcess) ),
inference(spm,[status(thm)],[28156,32074,theory(equality)]) ).
cnf(71431,negated_conjecture,
p__d__instance(esk242_0,c__LiquidMixture),
inference(spm,[status(thm)],[26786,11003,theory(equality)]) ).
cnf(71460,negated_conjecture,
p__d__instance(esk242_0,c__Mixture),
inference(spm,[status(thm)],[4769,71431,theory(equality)]) ).
cnf(71468,negated_conjecture,
( $false
| ~ p__d__instance(esk241_0,c__ChemicalProcess) ),
inference(rw,[status(thm)],[32076,71460,theory(equality)]) ).
cnf(71469,negated_conjecture,
~ p__d__instance(esk241_0,c__ChemicalProcess),
inference(cn,[status(thm)],[71468,theory(equality)]) ).
cnf(71474,negated_conjecture,
~ p__d__instance(esk241_0,c__Combustion),
inference(spm,[status(thm)],[71469,14480,theory(equality)]) ).
cnf(71475,negated_conjecture,
$false,
inference(rw,[status(thm)],[71474,4168,theory(equality)]) ).
cnf(71476,negated_conjecture,
$false,
inference(cn,[status(thm)],[71475,theory(equality)]) ).
cnf(71477,negated_conjecture,
$false,
71476,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR193+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 : n188.star.cs.uiowa.edu
% 0.03/0.25 % Model : x86_64 x86_64
% 0.03/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.25 % Memory : 32218.5MB
% 0.03/0.25 % OS : Linux 3.10.0-862.11.6.el7.x86_64
% 0.03/0.25 % CPULimit : 300
% 0.03/0.25 % DateTime : Tue Feb 19 18:47:29 CST 2019
% 0.03/0.25 % CPUTime :
% 0.03/0.30 % SZS status Started for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.30 --creating new selector for [CSR006+0.ax]
% 0.64/0.97 -running prover on /export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_1 with time limit 29
% 0.64/0.97 -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/tmpkLDyUw/sel_theBenchmark.p_1']
% 0.64/0.97 -prover status CounterSatisfiable
% 0.64/0.97 -running prover on /export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_2 with time limit 89
% 0.64/0.97 -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/tmpkLDyUw/sel_theBenchmark.p_2']
% 0.64/0.97 -prover status CounterSatisfiable
% 0.64/0.97 --creating new selector for [CSR006+0.ax]
% 119.86/121.05 eprover: CPU time limit exceeded, terminating
% 120.04/121.83 -running prover on /export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_3 with time limit 119
% 120.04/121.83 -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/tmpkLDyUw/sel_theBenchmark.p_3']
% 120.04/121.83 -prover status ResourceOut
% 120.04/121.83 --creating new selector for [CSR006+0.ax]
% 134.86/136.65 -running prover on /export/starexec/sandbox/tmp/tmpkLDyUw/sel_theBenchmark.p_4 with time limit 89
% 134.86/136.65 -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/tmpkLDyUw/sel_theBenchmark.p_4']
% 134.86/136.65 -prover status Theorem
% 134.86/136.65 Problem theBenchmark.p solved in phase 3.
% 134.86/136.65 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 134.86/136.65 % SZS status Ended for /export/starexec/sandbox/benchmark/theBenchmark.p
% 134.86/136.65 Solved 1 out of 1.
% 134.86/136.65 # Problem is unsatisfiable (or provable), constructing proof object
% 134.86/136.65 # SZS status Theorem
% 134.86/136.65 # SZS output start CNFRefutation.
% See solution above
% 134.86/136.67 # SZS output end CNFRefutation
%------------------------------------------------------------------------------