%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR230+1 : TPTP v7.3.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sine.py -e eprover -t %d %s
% Computer : n186.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 271.14s
% Output : CNFRefutation 271.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 21
% Syntax : Number of formulae : 123 ( 30 unt; 0 def)
% Number of atoms : 793 ( 4 equ)
% Maximal formula atoms : 110 ( 6 avg)
% Number of connectives : 1032 ( 362 ~; 361 |; 289 &)
% ( 13 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 68 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 1 prp; 0-7 aty)
% Number of functors : 17 ( 17 usr; 14 con; 0-2 aty)
% Number of variables : 394 ( 4 sgn 330 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(417,axiom,
! [X52,X189,X190] :
( ( p__d__subclass(X52,X189)
& p__d__subclass(X189,X190) )
=> p__d__subclass(X52,X190) ),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',predefinitionsA8) ).
fof(645,axiom,
! [X164] :
( p__d__subclass(X164,c__Entity)
=> ? [X249] : p__d__instance(X249,X164) ),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',mergeA176) ).
fof(646,axiom,
! [X164] :
( p__d__instance(X164,c__Class)
<=> p__d__subclass(X164,c__Entity) ),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',mergeA177) ).
fof(649,axiom,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',mergeA173) ).
fof(653,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',mergeA178) ).
fof(851,axiom,
! [X164,X291,X292] :
( ( p__subAttribute(X291,X292)
& p__d__instance(X292,X164) )
=> p__d__instance(X291,X164) ),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',mergeA141) ).
fof(875,axiom,
p__subAttribute(c__Headache,c__Pain),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',miloA2799) ).
fof(876,axiom,
p__subAttribute(c__Pain,c__Unhappiness),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',miloA2798) ).
fof(1076,axiom,
! [X12,X13] :
( p__part(X12,X13)
=> ( p__d__instance(X13,c__Object)
& p__d__instance(X12,c__Object) ) ),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',typeA5) ).
fof(1095,axiom,
! [X12,X13] :
( p__subAttribute(X12,X13)
=> ( p__d__instance(X13,c__Attribute)
& p__d__instance(X12,c__Attribute) ) ),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',typeA2) ).
fof(1755,axiom,
p__d__subclass(c__BodyPart,c__AnatomicalStructure),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',mergeA3031) ).
fof(1758,axiom,
p__d__subclass(c__Object,c__Physical),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',mergeA181) ).
fof(1953,axiom,
p__d__subclass(c__Attribute,c__Abstract),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',mergeA333) ).
fof(2478,axiom,
p__d__subclass(c__Icon,c__ContentBearingPhysical),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',mergeA287) ).
fof(2756,axiom,
p__d__subclass(c__ContentBearingPhysical,c__Physical),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',mergeA272) ).
fof(2869,axiom,
! [X176] :
( p__d__instance(X176,c__AnatomicalStructure)
=> ? [X271] :
( p__d__instance(X271,c__Cell)
& p__part(X271,X176) ) ),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',mergeA3028) ).
fof(3059,axiom,
( ! [X164,X659,X660] :
( p__d__partition3(X164,X659,X660)
<=> ( p__d__exhaustiveDecomposition3(X164,X659,X660)
& p__d__disjointDecomposition3(X164,X659,X660) ) )
& ! [X164,X659,X660,X661] :
( p__d__partition4(X164,X659,X660,X661)
<=> ( p__d__exhaustiveDecomposition4(X164,X659,X660,X661)
& p__d__disjointDecomposition4(X164,X659,X660,X661) ) )
& ! [X164,X659,X660,X661,X662] :
( p__d__partition5(X164,X659,X660,X661,X662)
<=> ( p__d__exhaustiveDecomposition5(X164,X659,X660,X661,X662)
& p__d__disjointDecomposition5(X164,X659,X660,X661,X662) ) )
& ! [X164,X659,X660,X661,X662,X663] :
( p__d__partition6(X164,X659,X660,X661,X662,X663)
<=> ( p__d__exhaustiveDecomposition6(X164,X659,X660,X661,X662,X663)
& p__d__disjointDecomposition6(X164,X659,X660,X661,X662,X663) ) )
& ! [X164,X659,X660,X661,X662,X663,X664] :
( p__d__partition7(X164,X659,X660,X661,X662,X663,X664)
<=> ( p__d__exhaustiveDecomposition7(X164,X659,X660,X661,X662,X663,X664)
& p__d__disjointDecomposition7(X164,X659,X660,X661,X662,X663,X664) ) ) ),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',predefinitionsA18) ).
fof(3062,axiom,
! [X145,X144] :
( p__d__disjoint(X145,X144)
<=> ! [X253] :
( ~ p__d__instance(X253,X145)
| ~ p__d__instance(X253,X144) ) ),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',predefinitionsA15) ).
fof(3063,axiom,
! [X52,X189,X190] :
( ( p__d__instance(X52,X189)
& p__d__subclass(X189,X190) )
=> p__d__instance(X52,X190) ),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',predefinitionsA12) ).
fof(3315,axiom,
( ! [X164,X659,X660] :
( p__d__disjointDecomposition3(X164,X659,X660)
<=> p__d__disjoint(X659,X660) )
& ! [X164,X659,X660,X661] :
( p__d__disjointDecomposition4(X164,X659,X660,X661)
<=> ( p__d__disjoint(X659,X660)
& p__d__disjoint(X659,X661)
& p__d__disjoint(X660,X661) ) )
& ! [X164,X659,X660,X661,X662] :
( p__d__disjointDecomposition5(X164,X659,X660,X661,X662)
<=> ( p__d__disjoint(X659,X660)
& p__d__disjoint(X659,X661)
& p__d__disjoint(X659,X662)
& p__d__disjoint(X660,X661)
& p__d__disjoint(X660,X662)
& p__d__disjoint(X661,X662) ) )
& ! [X164,X659,X660,X661,X662,X663] :
( p__d__disjointDecomposition6(X164,X659,X660,X661,X662,X663)
<=> ( p__d__disjoint(X659,X660)
& p__d__disjoint(X659,X661)
& p__d__disjoint(X659,X662)
& p__d__disjoint(X659,X663)
& p__d__disjoint(X660,X661)
& p__d__disjoint(X660,X662)
& p__d__disjoint(X660,X663)
& p__d__disjoint(X661,X662)
& p__d__disjoint(X661,X663)
& p__d__disjoint(X662,X663) ) )
& ! [X164,X659,X660,X661,X662,X663,X664] :
( p__d__disjointDecomposition7(X164,X659,X660,X661,X662,X663,X664)
<=> ( p__d__disjoint(X659,X660)
& p__d__disjoint(X659,X661)
& p__d__disjoint(X659,X662)
& p__d__disjoint(X659,X663)
& p__d__disjoint(X659,X664)
& p__d__disjoint(X660,X661)
& p__d__disjoint(X660,X662)
& p__d__disjoint(X660,X663)
& p__d__disjoint(X660,X664)
& p__d__disjoint(X661,X662)
& p__d__disjoint(X661,X663)
& p__d__disjoint(X661,X664)
& p__d__disjoint(X662,X663)
& p__d__disjoint(X662,X664)
& p__d__disjoint(X663,X664) ) ) ),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',predefinitionsA24) ).
fof(3403,conjecture,
? [X52,X189] :
( p__d__instance(X52,c__Icon)
& ~ p__d__instance(X189,c__BodyPart)
& ~ equal(X52,X189) ),
file('/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5',antonymPattern31567) ).
fof(3404,negated_conjecture,
~ ? [X52,X189] :
( p__d__instance(X52,c__Icon)
& ~ p__d__instance(X189,c__BodyPart)
& ~ equal(X52,X189) ),
inference(assume_negation,[status(cth)],[3403]) ).
fof(3478,plain,
! [X145,X144] :
( p__d__disjoint(X145,X144)
<=> ! [X253] :
( ~ p__d__instance(X253,X145)
| ~ p__d__instance(X253,X144) ) ),
inference(fof_simplification,[status(thm)],[3062,theory(equality)]) ).
fof(3494,negated_conjecture,
~ ? [X52,X189] :
( p__d__instance(X52,c__Icon)
& ~ p__d__instance(X189,c__BodyPart)
& ~ equal(X52,X189) ),
inference(fof_simplification,[status(thm)],[3404,theory(equality)]) ).
fof(4589,plain,
! [X52,X189,X190] :
( ~ p__d__subclass(X52,X189)
| ~ p__d__subclass(X189,X190)
| p__d__subclass(X52,X190) ),
inference(fof_nnf,[status(thm)],[417]) ).
fof(4590,plain,
! [X191,X192,X193] :
( ~ p__d__subclass(X191,X192)
| ~ p__d__subclass(X192,X193)
| p__d__subclass(X191,X193) ),
inference(variable_rename,[status(thm)],[4589]) ).
cnf(4591,plain,
( p__d__subclass(X1,X2)
| ~ p__d__subclass(X3,X2)
| ~ p__d__subclass(X1,X3) ),
inference(split_conjunct,[status(thm)],[4590]) ).
fof(5234,plain,
! [X164] :
( ~ p__d__subclass(X164,c__Entity)
| ? [X249] : p__d__instance(X249,X164) ),
inference(fof_nnf,[status(thm)],[645]) ).
fof(5235,plain,
! [X250] :
( ~ p__d__subclass(X250,c__Entity)
| ? [X251] : p__d__instance(X251,X250) ),
inference(variable_rename,[status(thm)],[5234]) ).
fof(5236,plain,
! [X250] :
( ~ p__d__subclass(X250,c__Entity)
| p__d__instance(esk116_1(X250),X250) ),
inference(skolemize,[status(esa)],[5235]) ).
cnf(5237,plain,
( p__d__instance(esk116_1(X1),X1)
| ~ p__d__subclass(X1,c__Entity) ),
inference(split_conjunct,[status(thm)],[5236]) ).
fof(5238,plain,
! [X164] :
( ( ~ p__d__instance(X164,c__Class)
| p__d__subclass(X164,c__Entity) )
& ( ~ p__d__subclass(X164,c__Entity)
| p__d__instance(X164,c__Class) ) ),
inference(fof_nnf,[status(thm)],[646]) ).
fof(5239,plain,
! [X165] :
( ( ~ p__d__instance(X165,c__Class)
| p__d__subclass(X165,c__Entity) )
& ( ~ p__d__subclass(X165,c__Entity)
| p__d__instance(X165,c__Class) ) ),
inference(variable_rename,[status(thm)],[5238]) ).
cnf(5240,plain,
( p__d__instance(X1,c__Class)
| ~ p__d__subclass(X1,c__Entity) ),
inference(split_conjunct,[status(thm)],[5239]) ).
cnf(5241,plain,
( p__d__subclass(X1,c__Entity)
| ~ p__d__instance(X1,c__Class) ),
inference(split_conjunct,[status(thm)],[5239]) ).
cnf(5247,plain,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
inference(split_conjunct,[status(thm)],[649]) ).
cnf(5254,plain,
p__d__subclass(c__Physical,c__Entity),
inference(split_conjunct,[status(thm)],[653]) ).
fof(5722,plain,
! [X164,X291,X292] :
( ~ p__subAttribute(X291,X292)
| ~ p__d__instance(X292,X164)
| p__d__instance(X291,X164) ),
inference(fof_nnf,[status(thm)],[851]) ).
fof(5723,plain,
! [X293,X294,X295] :
( ~ p__subAttribute(X294,X295)
| ~ p__d__instance(X295,X293)
| p__d__instance(X294,X293) ),
inference(variable_rename,[status(thm)],[5722]) ).
cnf(5724,plain,
( p__d__instance(X1,X2)
| ~ p__d__instance(X3,X2)
| ~ p__subAttribute(X1,X3) ),
inference(split_conjunct,[status(thm)],[5723]) ).
cnf(5788,plain,
p__subAttribute(c__Headache,c__Pain),
inference(split_conjunct,[status(thm)],[875]) ).
cnf(5789,plain,
p__subAttribute(c__Pain,c__Unhappiness),
inference(split_conjunct,[status(thm)],[876]) ).
fof(6369,plain,
! [X12,X13] :
( ~ p__part(X12,X13)
| ( p__d__instance(X13,c__Object)
& p__d__instance(X12,c__Object) ) ),
inference(fof_nnf,[status(thm)],[1076]) ).
fof(6370,plain,
! [X14,X15] :
( ~ p__part(X14,X15)
| ( p__d__instance(X15,c__Object)
& p__d__instance(X14,c__Object) ) ),
inference(variable_rename,[status(thm)],[6369]) ).
fof(6371,plain,
! [X14,X15] :
( ( p__d__instance(X15,c__Object)
| ~ p__part(X14,X15) )
& ( p__d__instance(X14,c__Object)
| ~ p__part(X14,X15) ) ),
inference(distribute,[status(thm)],[6370]) ).
cnf(6373,plain,
( p__d__instance(X2,c__Object)
| ~ p__part(X1,X2) ),
inference(split_conjunct,[status(thm)],[6371]) ).
fof(6447,plain,
! [X12,X13] :
( ~ p__subAttribute(X12,X13)
| ( p__d__instance(X13,c__Attribute)
& p__d__instance(X12,c__Attribute) ) ),
inference(fof_nnf,[status(thm)],[1095]) ).
fof(6448,plain,
! [X14,X15] :
( ~ p__subAttribute(X14,X15)
| ( p__d__instance(X15,c__Attribute)
& p__d__instance(X14,c__Attribute) ) ),
inference(variable_rename,[status(thm)],[6447]) ).
fof(6449,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)],[6448]) ).
cnf(6451,plain,
( p__d__instance(X2,c__Attribute)
| ~ p__subAttribute(X1,X2) ),
inference(split_conjunct,[status(thm)],[6449]) ).
cnf(8360,plain,
p__d__subclass(c__BodyPart,c__AnatomicalStructure),
inference(split_conjunct,[status(thm)],[1755]) ).
cnf(8363,plain,
p__d__subclass(c__Object,c__Physical),
inference(split_conjunct,[status(thm)],[1758]) ).
cnf(8885,plain,
p__d__subclass(c__Attribute,c__Abstract),
inference(split_conjunct,[status(thm)],[1953]) ).
cnf(10383,plain,
p__d__subclass(c__Icon,c__ContentBearingPhysical),
inference(split_conjunct,[status(thm)],[2478]) ).
cnf(11201,plain,
p__d__subclass(c__ContentBearingPhysical,c__Physical),
inference(split_conjunct,[status(thm)],[2756]) ).
fof(11500,plain,
! [X176] :
( ~ p__d__instance(X176,c__AnatomicalStructure)
| ? [X271] :
( p__d__instance(X271,c__Cell)
& p__part(X271,X176) ) ),
inference(fof_nnf,[status(thm)],[2869]) ).
fof(11501,plain,
! [X272] :
( ~ p__d__instance(X272,c__AnatomicalStructure)
| ? [X273] :
( p__d__instance(X273,c__Cell)
& p__part(X273,X272) ) ),
inference(variable_rename,[status(thm)],[11500]) ).
fof(11502,plain,
! [X272] :
( ~ p__d__instance(X272,c__AnatomicalStructure)
| ( p__d__instance(esk591_1(X272),c__Cell)
& p__part(esk591_1(X272),X272) ) ),
inference(skolemize,[status(esa)],[11501]) ).
fof(11503,plain,
! [X272] :
( ( p__d__instance(esk591_1(X272),c__Cell)
| ~ p__d__instance(X272,c__AnatomicalStructure) )
& ( p__part(esk591_1(X272),X272)
| ~ p__d__instance(X272,c__AnatomicalStructure) ) ),
inference(distribute,[status(thm)],[11502]) ).
cnf(11504,plain,
( p__part(esk591_1(X1),X1)
| ~ p__d__instance(X1,c__AnatomicalStructure) ),
inference(split_conjunct,[status(thm)],[11503]) ).
fof(12057,plain,
( ! [X164,X659,X660] :
( ( ~ p__d__partition3(X164,X659,X660)
| ( p__d__exhaustiveDecomposition3(X164,X659,X660)
& p__d__disjointDecomposition3(X164,X659,X660) ) )
& ( ~ p__d__exhaustiveDecomposition3(X164,X659,X660)
| ~ p__d__disjointDecomposition3(X164,X659,X660)
| p__d__partition3(X164,X659,X660) ) )
& ! [X164,X659,X660,X661] :
( ( ~ p__d__partition4(X164,X659,X660,X661)
| ( p__d__exhaustiveDecomposition4(X164,X659,X660,X661)
& p__d__disjointDecomposition4(X164,X659,X660,X661) ) )
& ( ~ p__d__exhaustiveDecomposition4(X164,X659,X660,X661)
| ~ p__d__disjointDecomposition4(X164,X659,X660,X661)
| p__d__partition4(X164,X659,X660,X661) ) )
& ! [X164,X659,X660,X661,X662] :
( ( ~ p__d__partition5(X164,X659,X660,X661,X662)
| ( p__d__exhaustiveDecomposition5(X164,X659,X660,X661,X662)
& p__d__disjointDecomposition5(X164,X659,X660,X661,X662) ) )
& ( ~ p__d__exhaustiveDecomposition5(X164,X659,X660,X661,X662)
| ~ p__d__disjointDecomposition5(X164,X659,X660,X661,X662)
| p__d__partition5(X164,X659,X660,X661,X662) ) )
& ! [X164,X659,X660,X661,X662,X663] :
( ( ~ p__d__partition6(X164,X659,X660,X661,X662,X663)
| ( p__d__exhaustiveDecomposition6(X164,X659,X660,X661,X662,X663)
& p__d__disjointDecomposition6(X164,X659,X660,X661,X662,X663) ) )
& ( ~ p__d__exhaustiveDecomposition6(X164,X659,X660,X661,X662,X663)
| ~ p__d__disjointDecomposition6(X164,X659,X660,X661,X662,X663)
| p__d__partition6(X164,X659,X660,X661,X662,X663) ) )
& ! [X164,X659,X660,X661,X662,X663,X664] :
( ( ~ p__d__partition7(X164,X659,X660,X661,X662,X663,X664)
| ( p__d__exhaustiveDecomposition7(X164,X659,X660,X661,X662,X663,X664)
& p__d__disjointDecomposition7(X164,X659,X660,X661,X662,X663,X664) ) )
& ( ~ p__d__exhaustiveDecomposition7(X164,X659,X660,X661,X662,X663,X664)
| ~ p__d__disjointDecomposition7(X164,X659,X660,X661,X662,X663,X664)
| p__d__partition7(X164,X659,X660,X661,X662,X663,X664) ) ) ),
inference(fof_nnf,[status(thm)],[3059]) ).
fof(12058,plain,
( ! [X665,X666,X667] :
( ( ~ p__d__partition3(X665,X666,X667)
| ( p__d__exhaustiveDecomposition3(X665,X666,X667)
& p__d__disjointDecomposition3(X665,X666,X667) ) )
& ( ~ p__d__exhaustiveDecomposition3(X665,X666,X667)
| ~ p__d__disjointDecomposition3(X665,X666,X667)
| p__d__partition3(X665,X666,X667) ) )
& ! [X668,X669,X670,X671] :
( ( ~ p__d__partition4(X668,X669,X670,X671)
| ( p__d__exhaustiveDecomposition4(X668,X669,X670,X671)
& p__d__disjointDecomposition4(X668,X669,X670,X671) ) )
& ( ~ p__d__exhaustiveDecomposition4(X668,X669,X670,X671)
| ~ p__d__disjointDecomposition4(X668,X669,X670,X671)
| p__d__partition4(X668,X669,X670,X671) ) )
& ! [X672,X673,X674,X675,X676] :
( ( ~ p__d__partition5(X672,X673,X674,X675,X676)
| ( p__d__exhaustiveDecomposition5(X672,X673,X674,X675,X676)
& p__d__disjointDecomposition5(X672,X673,X674,X675,X676) ) )
& ( ~ p__d__exhaustiveDecomposition5(X672,X673,X674,X675,X676)
| ~ p__d__disjointDecomposition5(X672,X673,X674,X675,X676)
| p__d__partition5(X672,X673,X674,X675,X676) ) )
& ! [X677,X678,X679,X680,X681,X682] :
( ( ~ p__d__partition6(X677,X678,X679,X680,X681,X682)
| ( p__d__exhaustiveDecomposition6(X677,X678,X679,X680,X681,X682)
& p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682) ) )
& ( ~ p__d__exhaustiveDecomposition6(X677,X678,X679,X680,X681,X682)
| ~ p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682)
| p__d__partition6(X677,X678,X679,X680,X681,X682) ) )
& ! [X683,X684,X685,X686,X687,X688,X689] :
( ( ~ p__d__partition7(X683,X684,X685,X686,X687,X688,X689)
| ( p__d__exhaustiveDecomposition7(X683,X684,X685,X686,X687,X688,X689)
& p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) ) )
& ( ~ p__d__exhaustiveDecomposition7(X683,X684,X685,X686,X687,X688,X689)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689)
| p__d__partition7(X683,X684,X685,X686,X687,X688,X689) ) ) ),
inference(variable_rename,[status(thm)],[12057]) ).
fof(12059,plain,
! [X665,X666,X667,X668,X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687,X688,X689] :
( ( ~ p__d__partition7(X683,X684,X685,X686,X687,X688,X689)
| ( p__d__exhaustiveDecomposition7(X683,X684,X685,X686,X687,X688,X689)
& p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) ) )
& ( ~ p__d__exhaustiveDecomposition7(X683,X684,X685,X686,X687,X688,X689)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689)
| p__d__partition7(X683,X684,X685,X686,X687,X688,X689) )
& ( ~ p__d__partition6(X677,X678,X679,X680,X681,X682)
| ( p__d__exhaustiveDecomposition6(X677,X678,X679,X680,X681,X682)
& p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682) ) )
& ( ~ p__d__exhaustiveDecomposition6(X677,X678,X679,X680,X681,X682)
| ~ p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682)
| p__d__partition6(X677,X678,X679,X680,X681,X682) )
& ( ~ p__d__partition5(X672,X673,X674,X675,X676)
| ( p__d__exhaustiveDecomposition5(X672,X673,X674,X675,X676)
& p__d__disjointDecomposition5(X672,X673,X674,X675,X676) ) )
& ( ~ p__d__exhaustiveDecomposition5(X672,X673,X674,X675,X676)
| ~ p__d__disjointDecomposition5(X672,X673,X674,X675,X676)
| p__d__partition5(X672,X673,X674,X675,X676) )
& ( ~ p__d__partition4(X668,X669,X670,X671)
| ( p__d__exhaustiveDecomposition4(X668,X669,X670,X671)
& p__d__disjointDecomposition4(X668,X669,X670,X671) ) )
& ( ~ p__d__exhaustiveDecomposition4(X668,X669,X670,X671)
| ~ p__d__disjointDecomposition4(X668,X669,X670,X671)
| p__d__partition4(X668,X669,X670,X671) )
& ( ~ p__d__partition3(X665,X666,X667)
| ( p__d__exhaustiveDecomposition3(X665,X666,X667)
& p__d__disjointDecomposition3(X665,X666,X667) ) )
& ( ~ p__d__exhaustiveDecomposition3(X665,X666,X667)
| ~ p__d__disjointDecomposition3(X665,X666,X667)
| p__d__partition3(X665,X666,X667) ) ),
inference(shift_quantors,[status(thm)],[12058]) ).
fof(12060,plain,
! [X665,X666,X667,X668,X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687,X688,X689] :
( ( p__d__exhaustiveDecomposition7(X683,X684,X685,X686,X687,X688,X689)
| ~ p__d__partition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689)
| ~ p__d__partition7(X683,X684,X685,X686,X687,X688,X689) )
& ( ~ p__d__exhaustiveDecomposition7(X683,X684,X685,X686,X687,X688,X689)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689)
| p__d__partition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__exhaustiveDecomposition6(X677,X678,X679,X680,X681,X682)
| ~ p__d__partition6(X677,X678,X679,X680,X681,X682) )
& ( p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682)
| ~ p__d__partition6(X677,X678,X679,X680,X681,X682) )
& ( ~ p__d__exhaustiveDecomposition6(X677,X678,X679,X680,X681,X682)
| ~ p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682)
| p__d__partition6(X677,X678,X679,X680,X681,X682) )
& ( p__d__exhaustiveDecomposition5(X672,X673,X674,X675,X676)
| ~ p__d__partition5(X672,X673,X674,X675,X676) )
& ( p__d__disjointDecomposition5(X672,X673,X674,X675,X676)
| ~ p__d__partition5(X672,X673,X674,X675,X676) )
& ( ~ p__d__exhaustiveDecomposition5(X672,X673,X674,X675,X676)
| ~ p__d__disjointDecomposition5(X672,X673,X674,X675,X676)
| p__d__partition5(X672,X673,X674,X675,X676) )
& ( p__d__exhaustiveDecomposition4(X668,X669,X670,X671)
| ~ p__d__partition4(X668,X669,X670,X671) )
& ( p__d__disjointDecomposition4(X668,X669,X670,X671)
| ~ p__d__partition4(X668,X669,X670,X671) )
& ( ~ p__d__exhaustiveDecomposition4(X668,X669,X670,X671)
| ~ p__d__disjointDecomposition4(X668,X669,X670,X671)
| p__d__partition4(X668,X669,X670,X671) )
& ( p__d__exhaustiveDecomposition3(X665,X666,X667)
| ~ p__d__partition3(X665,X666,X667) )
& ( p__d__disjointDecomposition3(X665,X666,X667)
| ~ p__d__partition3(X665,X666,X667) )
& ( ~ p__d__exhaustiveDecomposition3(X665,X666,X667)
| ~ p__d__disjointDecomposition3(X665,X666,X667)
| p__d__partition3(X665,X666,X667) ) ),
inference(distribute,[status(thm)],[12059]) ).
cnf(12062,plain,
( p__d__disjointDecomposition3(X1,X2,X3)
| ~ p__d__partition3(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[12060]) ).
fof(12078,plain,
! [X145,X144] :
( ( ~ p__d__disjoint(X145,X144)
| ! [X253] :
( ~ p__d__instance(X253,X145)
| ~ p__d__instance(X253,X144) ) )
& ( ? [X253] :
( p__d__instance(X253,X145)
& p__d__instance(X253,X144) )
| p__d__disjoint(X145,X144) ) ),
inference(fof_nnf,[status(thm)],[3478]) ).
fof(12079,plain,
! [X254,X255] :
( ( ~ p__d__disjoint(X254,X255)
| ! [X256] :
( ~ p__d__instance(X256,X254)
| ~ p__d__instance(X256,X255) ) )
& ( ? [X257] :
( p__d__instance(X257,X254)
& p__d__instance(X257,X255) )
| p__d__disjoint(X254,X255) ) ),
inference(variable_rename,[status(thm)],[12078]) ).
fof(12080,plain,
! [X254,X255] :
( ( ~ p__d__disjoint(X254,X255)
| ! [X256] :
( ~ p__d__instance(X256,X254)
| ~ p__d__instance(X256,X255) ) )
& ( ( p__d__instance(esk633_2(X254,X255),X254)
& p__d__instance(esk633_2(X254,X255),X255) )
| p__d__disjoint(X254,X255) ) ),
inference(skolemize,[status(esa)],[12079]) ).
fof(12081,plain,
! [X254,X255,X256] :
( ( ~ p__d__instance(X256,X254)
| ~ p__d__instance(X256,X255)
| ~ p__d__disjoint(X254,X255) )
& ( ( p__d__instance(esk633_2(X254,X255),X254)
& p__d__instance(esk633_2(X254,X255),X255) )
| p__d__disjoint(X254,X255) ) ),
inference(shift_quantors,[status(thm)],[12080]) ).
fof(12082,plain,
! [X254,X255,X256] :
( ( ~ p__d__instance(X256,X254)
| ~ p__d__instance(X256,X255)
| ~ p__d__disjoint(X254,X255) )
& ( p__d__instance(esk633_2(X254,X255),X254)
| p__d__disjoint(X254,X255) )
& ( p__d__instance(esk633_2(X254,X255),X255)
| p__d__disjoint(X254,X255) ) ),
inference(distribute,[status(thm)],[12081]) ).
cnf(12085,plain,
( ~ p__d__disjoint(X1,X2)
| ~ p__d__instance(X3,X2)
| ~ p__d__instance(X3,X1) ),
inference(split_conjunct,[status(thm)],[12082]) ).
fof(12086,plain,
! [X52,X189,X190] :
( ~ p__d__instance(X52,X189)
| ~ p__d__subclass(X189,X190)
| p__d__instance(X52,X190) ),
inference(fof_nnf,[status(thm)],[3063]) ).
fof(12087,plain,
! [X191,X192,X193] :
( ~ p__d__instance(X191,X192)
| ~ p__d__subclass(X192,X193)
| p__d__instance(X191,X193) ),
inference(variable_rename,[status(thm)],[12086]) ).
cnf(12088,plain,
( p__d__instance(X1,X2)
| ~ p__d__subclass(X3,X2)
| ~ p__d__instance(X1,X3) ),
inference(split_conjunct,[status(thm)],[12087]) ).
fof(12853,plain,
( ! [X164,X659,X660] :
( ( ~ p__d__disjointDecomposition3(X164,X659,X660)
| p__d__disjoint(X659,X660) )
& ( ~ p__d__disjoint(X659,X660)
| p__d__disjointDecomposition3(X164,X659,X660) ) )
& ! [X164,X659,X660,X661] :
( ( ~ p__d__disjointDecomposition4(X164,X659,X660,X661)
| ( p__d__disjoint(X659,X660)
& p__d__disjoint(X659,X661)
& p__d__disjoint(X660,X661) ) )
& ( ~ p__d__disjoint(X659,X660)
| ~ p__d__disjoint(X659,X661)
| ~ p__d__disjoint(X660,X661)
| p__d__disjointDecomposition4(X164,X659,X660,X661) ) )
& ! [X164,X659,X660,X661,X662] :
( ( ~ p__d__disjointDecomposition5(X164,X659,X660,X661,X662)
| ( p__d__disjoint(X659,X660)
& p__d__disjoint(X659,X661)
& p__d__disjoint(X659,X662)
& p__d__disjoint(X660,X661)
& p__d__disjoint(X660,X662)
& p__d__disjoint(X661,X662) ) )
& ( ~ p__d__disjoint(X659,X660)
| ~ p__d__disjoint(X659,X661)
| ~ p__d__disjoint(X659,X662)
| ~ p__d__disjoint(X660,X661)
| ~ p__d__disjoint(X660,X662)
| ~ p__d__disjoint(X661,X662)
| p__d__disjointDecomposition5(X164,X659,X660,X661,X662) ) )
& ! [X164,X659,X660,X661,X662,X663] :
( ( ~ p__d__disjointDecomposition6(X164,X659,X660,X661,X662,X663)
| ( p__d__disjoint(X659,X660)
& p__d__disjoint(X659,X661)
& p__d__disjoint(X659,X662)
& p__d__disjoint(X659,X663)
& p__d__disjoint(X660,X661)
& p__d__disjoint(X660,X662)
& p__d__disjoint(X660,X663)
& p__d__disjoint(X661,X662)
& p__d__disjoint(X661,X663)
& p__d__disjoint(X662,X663) ) )
& ( ~ p__d__disjoint(X659,X660)
| ~ p__d__disjoint(X659,X661)
| ~ p__d__disjoint(X659,X662)
| ~ p__d__disjoint(X659,X663)
| ~ p__d__disjoint(X660,X661)
| ~ p__d__disjoint(X660,X662)
| ~ p__d__disjoint(X660,X663)
| ~ p__d__disjoint(X661,X662)
| ~ p__d__disjoint(X661,X663)
| ~ p__d__disjoint(X662,X663)
| p__d__disjointDecomposition6(X164,X659,X660,X661,X662,X663) ) )
& ! [X164,X659,X660,X661,X662,X663,X664] :
( ( ~ p__d__disjointDecomposition7(X164,X659,X660,X661,X662,X663,X664)
| ( p__d__disjoint(X659,X660)
& p__d__disjoint(X659,X661)
& p__d__disjoint(X659,X662)
& p__d__disjoint(X659,X663)
& p__d__disjoint(X659,X664)
& p__d__disjoint(X660,X661)
& p__d__disjoint(X660,X662)
& p__d__disjoint(X660,X663)
& p__d__disjoint(X660,X664)
& p__d__disjoint(X661,X662)
& p__d__disjoint(X661,X663)
& p__d__disjoint(X661,X664)
& p__d__disjoint(X662,X663)
& p__d__disjoint(X662,X664)
& p__d__disjoint(X663,X664) ) )
& ( ~ p__d__disjoint(X659,X660)
| ~ p__d__disjoint(X659,X661)
| ~ p__d__disjoint(X659,X662)
| ~ p__d__disjoint(X659,X663)
| ~ p__d__disjoint(X659,X664)
| ~ p__d__disjoint(X660,X661)
| ~ p__d__disjoint(X660,X662)
| ~ p__d__disjoint(X660,X663)
| ~ p__d__disjoint(X660,X664)
| ~ p__d__disjoint(X661,X662)
| ~ p__d__disjoint(X661,X663)
| ~ p__d__disjoint(X661,X664)
| ~ p__d__disjoint(X662,X663)
| ~ p__d__disjoint(X662,X664)
| ~ p__d__disjoint(X663,X664)
| p__d__disjointDecomposition7(X164,X659,X660,X661,X662,X663,X664) ) ) ),
inference(fof_nnf,[status(thm)],[3315]) ).
fof(12854,plain,
( ! [X665,X666,X667] :
( ( ~ p__d__disjointDecomposition3(X665,X666,X667)
| p__d__disjoint(X666,X667) )
& ( ~ p__d__disjoint(X666,X667)
| p__d__disjointDecomposition3(X665,X666,X667) ) )
& ! [X668,X669,X670,X671] :
( ( ~ p__d__disjointDecomposition4(X668,X669,X670,X671)
| ( p__d__disjoint(X669,X670)
& p__d__disjoint(X669,X671)
& p__d__disjoint(X670,X671) ) )
& ( ~ p__d__disjoint(X669,X670)
| ~ p__d__disjoint(X669,X671)
| ~ p__d__disjoint(X670,X671)
| p__d__disjointDecomposition4(X668,X669,X670,X671) ) )
& ! [X672,X673,X674,X675,X676] :
( ( ~ p__d__disjointDecomposition5(X672,X673,X674,X675,X676)
| ( p__d__disjoint(X673,X674)
& p__d__disjoint(X673,X675)
& p__d__disjoint(X673,X676)
& p__d__disjoint(X674,X675)
& p__d__disjoint(X674,X676)
& p__d__disjoint(X675,X676) ) )
& ( ~ p__d__disjoint(X673,X674)
| ~ p__d__disjoint(X673,X675)
| ~ p__d__disjoint(X673,X676)
| ~ p__d__disjoint(X674,X675)
| ~ p__d__disjoint(X674,X676)
| ~ p__d__disjoint(X675,X676)
| p__d__disjointDecomposition5(X672,X673,X674,X675,X676) ) )
& ! [X677,X678,X679,X680,X681,X682] :
( ( ~ p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682)
| ( p__d__disjoint(X678,X679)
& p__d__disjoint(X678,X680)
& p__d__disjoint(X678,X681)
& p__d__disjoint(X678,X682)
& p__d__disjoint(X679,X680)
& p__d__disjoint(X679,X681)
& p__d__disjoint(X679,X682)
& p__d__disjoint(X680,X681)
& p__d__disjoint(X680,X682)
& p__d__disjoint(X681,X682) ) )
& ( ~ p__d__disjoint(X678,X679)
| ~ p__d__disjoint(X678,X680)
| ~ p__d__disjoint(X678,X681)
| ~ p__d__disjoint(X678,X682)
| ~ p__d__disjoint(X679,X680)
| ~ p__d__disjoint(X679,X681)
| ~ p__d__disjoint(X679,X682)
| ~ p__d__disjoint(X680,X681)
| ~ p__d__disjoint(X680,X682)
| ~ p__d__disjoint(X681,X682)
| p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682) ) )
& ! [X683,X684,X685,X686,X687,X688,X689] :
( ( ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689)
| ( p__d__disjoint(X684,X685)
& p__d__disjoint(X684,X686)
& p__d__disjoint(X684,X687)
& p__d__disjoint(X684,X688)
& p__d__disjoint(X684,X689)
& p__d__disjoint(X685,X686)
& p__d__disjoint(X685,X687)
& p__d__disjoint(X685,X688)
& p__d__disjoint(X685,X689)
& p__d__disjoint(X686,X687)
& p__d__disjoint(X686,X688)
& p__d__disjoint(X686,X689)
& p__d__disjoint(X687,X688)
& p__d__disjoint(X687,X689)
& p__d__disjoint(X688,X689) ) )
& ( ~ p__d__disjoint(X684,X685)
| ~ p__d__disjoint(X684,X686)
| ~ p__d__disjoint(X684,X687)
| ~ p__d__disjoint(X684,X688)
| ~ p__d__disjoint(X684,X689)
| ~ p__d__disjoint(X685,X686)
| ~ p__d__disjoint(X685,X687)
| ~ p__d__disjoint(X685,X688)
| ~ p__d__disjoint(X685,X689)
| ~ p__d__disjoint(X686,X687)
| ~ p__d__disjoint(X686,X688)
| ~ p__d__disjoint(X686,X689)
| ~ p__d__disjoint(X687,X688)
| ~ p__d__disjoint(X687,X689)
| ~ p__d__disjoint(X688,X689)
| p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) ) ) ),
inference(variable_rename,[status(thm)],[12853]) ).
fof(12855,plain,
! [X665,X666,X667,X668,X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687,X688,X689] :
( ( ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689)
| ( p__d__disjoint(X684,X685)
& p__d__disjoint(X684,X686)
& p__d__disjoint(X684,X687)
& p__d__disjoint(X684,X688)
& p__d__disjoint(X684,X689)
& p__d__disjoint(X685,X686)
& p__d__disjoint(X685,X687)
& p__d__disjoint(X685,X688)
& p__d__disjoint(X685,X689)
& p__d__disjoint(X686,X687)
& p__d__disjoint(X686,X688)
& p__d__disjoint(X686,X689)
& p__d__disjoint(X687,X688)
& p__d__disjoint(X687,X689)
& p__d__disjoint(X688,X689) ) )
& ( ~ p__d__disjoint(X684,X685)
| ~ p__d__disjoint(X684,X686)
| ~ p__d__disjoint(X684,X687)
| ~ p__d__disjoint(X684,X688)
| ~ p__d__disjoint(X684,X689)
| ~ p__d__disjoint(X685,X686)
| ~ p__d__disjoint(X685,X687)
| ~ p__d__disjoint(X685,X688)
| ~ p__d__disjoint(X685,X689)
| ~ p__d__disjoint(X686,X687)
| ~ p__d__disjoint(X686,X688)
| ~ p__d__disjoint(X686,X689)
| ~ p__d__disjoint(X687,X688)
| ~ p__d__disjoint(X687,X689)
| ~ p__d__disjoint(X688,X689)
| p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( ~ p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682)
| ( p__d__disjoint(X678,X679)
& p__d__disjoint(X678,X680)
& p__d__disjoint(X678,X681)
& p__d__disjoint(X678,X682)
& p__d__disjoint(X679,X680)
& p__d__disjoint(X679,X681)
& p__d__disjoint(X679,X682)
& p__d__disjoint(X680,X681)
& p__d__disjoint(X680,X682)
& p__d__disjoint(X681,X682) ) )
& ( ~ p__d__disjoint(X678,X679)
| ~ p__d__disjoint(X678,X680)
| ~ p__d__disjoint(X678,X681)
| ~ p__d__disjoint(X678,X682)
| ~ p__d__disjoint(X679,X680)
| ~ p__d__disjoint(X679,X681)
| ~ p__d__disjoint(X679,X682)
| ~ p__d__disjoint(X680,X681)
| ~ p__d__disjoint(X680,X682)
| ~ p__d__disjoint(X681,X682)
| p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682) )
& ( ~ p__d__disjointDecomposition5(X672,X673,X674,X675,X676)
| ( p__d__disjoint(X673,X674)
& p__d__disjoint(X673,X675)
& p__d__disjoint(X673,X676)
& p__d__disjoint(X674,X675)
& p__d__disjoint(X674,X676)
& p__d__disjoint(X675,X676) ) )
& ( ~ p__d__disjoint(X673,X674)
| ~ p__d__disjoint(X673,X675)
| ~ p__d__disjoint(X673,X676)
| ~ p__d__disjoint(X674,X675)
| ~ p__d__disjoint(X674,X676)
| ~ p__d__disjoint(X675,X676)
| p__d__disjointDecomposition5(X672,X673,X674,X675,X676) )
& ( ~ p__d__disjointDecomposition4(X668,X669,X670,X671)
| ( p__d__disjoint(X669,X670)
& p__d__disjoint(X669,X671)
& p__d__disjoint(X670,X671) ) )
& ( ~ p__d__disjoint(X669,X670)
| ~ p__d__disjoint(X669,X671)
| ~ p__d__disjoint(X670,X671)
| p__d__disjointDecomposition4(X668,X669,X670,X671) )
& ( ~ p__d__disjointDecomposition3(X665,X666,X667)
| p__d__disjoint(X666,X667) )
& ( ~ p__d__disjoint(X666,X667)
| p__d__disjointDecomposition3(X665,X666,X667) ) ),
inference(shift_quantors,[status(thm)],[12854]) ).
fof(12856,plain,
! [X665,X666,X667,X668,X669,X670,X671,X672,X673,X674,X675,X676,X677,X678,X679,X680,X681,X682,X683,X684,X685,X686,X687,X688,X689] :
( ( p__d__disjoint(X684,X685)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjoint(X684,X686)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjoint(X684,X687)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjoint(X684,X688)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjoint(X684,X689)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjoint(X685,X686)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjoint(X685,X687)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjoint(X685,X688)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjoint(X685,X689)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjoint(X686,X687)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjoint(X686,X688)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjoint(X686,X689)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjoint(X687,X688)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjoint(X687,X689)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjoint(X688,X689)
| ~ p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( ~ p__d__disjoint(X684,X685)
| ~ p__d__disjoint(X684,X686)
| ~ p__d__disjoint(X684,X687)
| ~ p__d__disjoint(X684,X688)
| ~ p__d__disjoint(X684,X689)
| ~ p__d__disjoint(X685,X686)
| ~ p__d__disjoint(X685,X687)
| ~ p__d__disjoint(X685,X688)
| ~ p__d__disjoint(X685,X689)
| ~ p__d__disjoint(X686,X687)
| ~ p__d__disjoint(X686,X688)
| ~ p__d__disjoint(X686,X689)
| ~ p__d__disjoint(X687,X688)
| ~ p__d__disjoint(X687,X689)
| ~ p__d__disjoint(X688,X689)
| p__d__disjointDecomposition7(X683,X684,X685,X686,X687,X688,X689) )
& ( p__d__disjoint(X678,X679)
| ~ p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682) )
& ( p__d__disjoint(X678,X680)
| ~ p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682) )
& ( p__d__disjoint(X678,X681)
| ~ p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682) )
& ( p__d__disjoint(X678,X682)
| ~ p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682) )
& ( p__d__disjoint(X679,X680)
| ~ p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682) )
& ( p__d__disjoint(X679,X681)
| ~ p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682) )
& ( p__d__disjoint(X679,X682)
| ~ p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682) )
& ( p__d__disjoint(X680,X681)
| ~ p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682) )
& ( p__d__disjoint(X680,X682)
| ~ p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682) )
& ( p__d__disjoint(X681,X682)
| ~ p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682) )
& ( ~ p__d__disjoint(X678,X679)
| ~ p__d__disjoint(X678,X680)
| ~ p__d__disjoint(X678,X681)
| ~ p__d__disjoint(X678,X682)
| ~ p__d__disjoint(X679,X680)
| ~ p__d__disjoint(X679,X681)
| ~ p__d__disjoint(X679,X682)
| ~ p__d__disjoint(X680,X681)
| ~ p__d__disjoint(X680,X682)
| ~ p__d__disjoint(X681,X682)
| p__d__disjointDecomposition6(X677,X678,X679,X680,X681,X682) )
& ( p__d__disjoint(X673,X674)
| ~ p__d__disjointDecomposition5(X672,X673,X674,X675,X676) )
& ( p__d__disjoint(X673,X675)
| ~ p__d__disjointDecomposition5(X672,X673,X674,X675,X676) )
& ( p__d__disjoint(X673,X676)
| ~ p__d__disjointDecomposition5(X672,X673,X674,X675,X676) )
& ( p__d__disjoint(X674,X675)
| ~ p__d__disjointDecomposition5(X672,X673,X674,X675,X676) )
& ( p__d__disjoint(X674,X676)
| ~ p__d__disjointDecomposition5(X672,X673,X674,X675,X676) )
& ( p__d__disjoint(X675,X676)
| ~ p__d__disjointDecomposition5(X672,X673,X674,X675,X676) )
& ( ~ p__d__disjoint(X673,X674)
| ~ p__d__disjoint(X673,X675)
| ~ p__d__disjoint(X673,X676)
| ~ p__d__disjoint(X674,X675)
| ~ p__d__disjoint(X674,X676)
| ~ p__d__disjoint(X675,X676)
| p__d__disjointDecomposition5(X672,X673,X674,X675,X676) )
& ( p__d__disjoint(X669,X670)
| ~ p__d__disjointDecomposition4(X668,X669,X670,X671) )
& ( p__d__disjoint(X669,X671)
| ~ p__d__disjointDecomposition4(X668,X669,X670,X671) )
& ( p__d__disjoint(X670,X671)
| ~ p__d__disjointDecomposition4(X668,X669,X670,X671) )
& ( ~ p__d__disjoint(X669,X670)
| ~ p__d__disjoint(X669,X671)
| ~ p__d__disjoint(X670,X671)
| p__d__disjointDecomposition4(X668,X669,X670,X671) )
& ( ~ p__d__disjointDecomposition3(X665,X666,X667)
| p__d__disjoint(X666,X667) )
& ( ~ p__d__disjoint(X666,X667)
| p__d__disjointDecomposition3(X665,X666,X667) ) ),
inference(distribute,[status(thm)],[12855]) ).
cnf(12858,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__disjointDecomposition3(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[12856]) ).
fof(13148,negated_conjecture,
! [X52,X189] :
( ~ p__d__instance(X52,c__Icon)
| p__d__instance(X189,c__BodyPart)
| equal(X52,X189) ),
inference(fof_nnf,[status(thm)],[3494]) ).
fof(13149,negated_conjecture,
! [X190,X191] :
( ~ p__d__instance(X190,c__Icon)
| p__d__instance(X191,c__BodyPart)
| equal(X190,X191) ),
inference(variable_rename,[status(thm)],[13148]) ).
cnf(13150,negated_conjecture,
( X1 = X2
| p__d__instance(X2,c__BodyPart)
| ~ p__d__instance(X1,c__Icon) ),
inference(split_conjunct,[status(thm)],[13149]) ).
cnf(13153,plain,
p__d__instance(c__Physical,c__Class),
inference(spm,[status(thm)],[5240,5254,theory(equality)]) ).
cnf(13173,plain,
p__d__instance(c__Pain,c__Attribute),
inference(spm,[status(thm)],[6451,5788,theory(equality)]) ).
cnf(13633,plain,
( p__d__instance(c__Headache,X1)
| ~ p__d__instance(c__Pain,X1) ),
inference(spm,[status(thm)],[5724,5788,theory(equality)]) ).
cnf(13634,plain,
( p__d__instance(c__Pain,X1)
| ~ p__d__instance(c__Unhappiness,X1) ),
inference(spm,[status(thm)],[5724,5789,theory(equality)]) ).
cnf(13648,plain,
( p__d__instance(X1,c__AnatomicalStructure)
| ~ p__d__instance(X1,c__BodyPart) ),
inference(spm,[status(thm)],[12088,8360,theory(equality)]) ).
cnf(13664,plain,
( p__d__instance(X1,c__ContentBearingPhysical)
| ~ p__d__instance(X1,c__Icon) ),
inference(spm,[status(thm)],[12088,10383,theory(equality)]) ).
cnf(13668,plain,
( p__d__instance(X1,c__Physical)
| ~ p__d__instance(X1,c__Object) ),
inference(spm,[status(thm)],[12088,8363,theory(equality)]) ).
cnf(13789,plain,
( p__d__instance(X1,c__Abstract)
| ~ p__d__instance(X1,c__Attribute) ),
inference(spm,[status(thm)],[12088,8885,theory(equality)]) ).
cnf(13794,plain,
( p__d__instance(X1,c__Physical)
| ~ p__d__instance(X1,c__ContentBearingPhysical) ),
inference(spm,[status(thm)],[12088,11201,theory(equality)]) ).
cnf(15253,negated_conjecture,
( esk116_1(c__Icon) = X1
| p__d__instance(X1,c__BodyPart)
| ~ p__d__subclass(c__Icon,c__Entity) ),
inference(spm,[status(thm)],[13150,5237,theory(equality)]) ).
cnf(15344,plain,
( p__d__instance(X1,c__Object)
| ~ p__d__instance(X1,c__AnatomicalStructure) ),
inference(spm,[status(thm)],[6373,11504,theory(equality)]) ).
cnf(16697,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__partition3(X3,X1,X2) ),
inference(spm,[status(thm)],[12858,12062,theory(equality)]) ).
cnf(18233,plain,
( p__d__subclass(X1,c__Physical)
| ~ p__d__subclass(X1,c__ContentBearingPhysical) ),
inference(spm,[status(thm)],[4591,11201,theory(equality)]) ).
cnf(19194,plain,
( p__d__subclass(X1,c__Entity)
| ~ p__d__subclass(X1,X2)
| ~ p__d__instance(X2,c__Class) ),
inference(spm,[status(thm)],[4591,5241,theory(equality)]) ).
cnf(35065,plain,
( p__d__instance(c__Pain,c__ContentBearingPhysical)
| ~ p__d__instance(c__Unhappiness,c__Icon) ),
inference(spm,[status(thm)],[13664,13634,theory(equality)]) ).
cnf(37153,plain,
( p__d__instance(c__Headache,c__Physical)
| ~ p__d__instance(c__Pain,c__Object) ),
inference(spm,[status(thm)],[13633,13668,theory(equality)]) ).
cnf(39237,plain,
( p__d__instance(c__Headache,c__ContentBearingPhysical)
| ~ p__d__instance(c__Unhappiness,c__Icon) ),
inference(spm,[status(thm)],[13633,35065,theory(equality)]) ).
cnf(42674,plain,
( p__d__instance(c__Headache,c__Abstract)
| ~ p__d__instance(c__Pain,c__Attribute) ),
inference(spm,[status(thm)],[13633,13789,theory(equality)]) ).
cnf(42680,plain,
( p__d__instance(c__Headache,c__Abstract)
| $false ),
inference(rw,[status(thm)],[42674,13173,theory(equality)]) ).
cnf(42681,plain,
p__d__instance(c__Headache,c__Abstract),
inference(cn,[status(thm)],[42680,theory(equality)]) ).
cnf(42868,plain,
( p__d__instance(c__Headache,c__Physical)
| ~ p__d__instance(c__Unhappiness,c__Icon) ),
inference(spm,[status(thm)],[13794,39237,theory(equality)]) ).
cnf(85430,plain,
( p__d__instance(X1,c__Object)
| ~ p__d__instance(X1,c__BodyPart) ),
inference(spm,[status(thm)],[15344,13648,theory(equality)]) ).
cnf(85462,plain,
( p__d__instance(c__Pain,c__Object)
| ~ p__d__instance(c__Unhappiness,c__BodyPart) ),
inference(spm,[status(thm)],[85430,13634,theory(equality)]) ).
cnf(97848,plain,
( p__d__instance(c__Headache,c__Physical)
| ~ p__d__instance(c__Unhappiness,c__BodyPart) ),
inference(spm,[status(thm)],[37153,85462,theory(equality)]) ).
cnf(102930,plain,
p__d__disjoint(c__Physical,c__Abstract),
inference(spm,[status(thm)],[16697,5247,theory(equality)]) ).
cnf(103451,plain,
( ~ p__d__instance(X1,c__Abstract)
| ~ p__d__instance(X1,c__Physical) ),
inference(spm,[status(thm)],[12085,102930,theory(equality)]) ).
cnf(104173,plain,
~ p__d__instance(c__Headache,c__Physical),
inference(spm,[status(thm)],[103451,42681,theory(equality)]) ).
cnf(104258,plain,
~ p__d__instance(c__Unhappiness,c__Icon),
inference(spm,[status(thm)],[104173,42868,theory(equality)]) ).
cnf(104260,plain,
~ p__d__instance(c__Unhappiness,c__BodyPart),
inference(spm,[status(thm)],[104173,97848,theory(equality)]) ).
cnf(123494,plain,
p__d__subclass(c__Icon,c__Physical),
inference(spm,[status(thm)],[18233,10383,theory(equality)]) ).
cnf(138259,plain,
( p__d__subclass(c__Icon,c__Entity)
| ~ p__d__instance(c__Physical,c__Class) ),
inference(spm,[status(thm)],[19194,123494,theory(equality)]) ).
cnf(139846,plain,
( p__d__subclass(c__Icon,c__Entity)
| $false ),
inference(rw,[status(thm)],[138259,13153,theory(equality)]) ).
cnf(139847,plain,
p__d__subclass(c__Icon,c__Entity),
inference(cn,[status(thm)],[139846,theory(equality)]) ).
cnf(139921,negated_conjecture,
( esk116_1(c__Icon) = X1
| p__d__instance(X1,c__BodyPart)
| $false ),
inference(rw,[status(thm)],[15253,139847,theory(equality)]) ).
cnf(139922,negated_conjecture,
( esk116_1(c__Icon) = X1
| p__d__instance(X1,c__BodyPart) ),
inference(cn,[status(thm)],[139921,theory(equality)]) ).
cnf(140173,negated_conjecture,
( p__d__instance(X1,c__Icon)
| p__d__instance(X1,c__BodyPart)
| ~ p__d__subclass(c__Icon,c__Entity) ),
inference(spm,[status(thm)],[5237,139922,theory(equality)]) ).
cnf(141026,negated_conjecture,
( p__d__instance(X1,c__Icon)
| p__d__instance(X1,c__BodyPart)
| $false ),
inference(rw,[status(thm)],[140173,139847,theory(equality)]) ).
cnf(141027,negated_conjecture,
( p__d__instance(X1,c__Icon)
| p__d__instance(X1,c__BodyPart) ),
inference(cn,[status(thm)],[141026,theory(equality)]) ).
cnf(142605,negated_conjecture,
p__d__instance(c__Unhappiness,c__BodyPart),
inference(spm,[status(thm)],[104258,141027,theory(equality)]) ).
cnf(142681,negated_conjecture,
$false,
inference(sr,[status(thm)],[142605,104260,theory(equality)]) ).
cnf(142682,negated_conjecture,
$false,
142681,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR230+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 : n186.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 : Wed Feb 20 02:54:28 CST 2019
% 0.03/0.25 % CPUTime :
% 0.08/0.30 % SZS status Started for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.30 --creating new selector for [CSR006+0.ax]
% 37.48/37.88 -running prover on /export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_1 with time limit 29
% 37.48/37.88 -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/tmpgKkcrQ/sel_theBenchmark.p_1']
% 37.48/37.88 -prover status CounterSatisfiable
% 37.48/37.88 -running prover on /export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_2 with time limit 84
% 37.48/37.88 -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=84', '/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_2']
% 37.48/37.88 -prover status CounterSatisfiable
% 37.48/37.88 --creating new selector for [CSR006+0.ax]
% 56.89/57.61 -running prover on /export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_3 with time limit 104
% 56.89/57.61 -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=104', '/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_3']
% 56.89/57.61 -prover status CounterSatisfiable
% 56.89/57.61 --creating new selector for [CSR006+0.ax]
% 177.96/178.96 eprover: CPU time limit exceeded, terminating
% 178.08/179.24 -running prover on /export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_4 with time limit 121
% 178.08/179.24 -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=121', '/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_4']
% 178.08/179.24 -prover status ResourceOut
% 178.08/179.24 --creating new selector for [CSR006+0.ax]
% 271.14/272.34 -running prover on /export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5 with time limit 121
% 271.14/272.34 -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=121', '/export/starexec/sandbox/tmp/tmpgKkcrQ/sel_theBenchmark.p_5']
% 271.14/272.34 -prover status Theorem
% 271.14/272.34 Problem theBenchmark.p solved in phase 4.
% 271.14/272.34 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 271.14/272.34 % SZS status Ended for /export/starexec/sandbox/benchmark/theBenchmark.p
% 271.14/272.34 Solved 1 out of 1.
% 271.14/272.34 # Problem is unsatisfiable (or provable), constructing proof object
% 271.14/272.34 # SZS status Theorem
% 271.14/272.34 # SZS output start CNFRefutation.
% See solution above
% 271.14/272.38 # SZS output end CNFRefutation
%------------------------------------------------------------------------------