%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : CSR229+1 : TPTP v8.1.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n021.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Fri Jul 15 02:50:01 EDT 2022
% Result : Theorem 153.10s 22.27s
% Output : CNFRefutation 153.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 23
% Syntax : Number of clauses : 76 ( 38 unt; 4 nHn; 72 RR)
% Number of literals : 125 ( 3 equ; 53 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 15 con; 0-1 aty)
% Number of variables : 69 ( 5 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_3546,plain,
( p__d__subclass(X1,X2)
| ~ p__d__subclass(X3,X2)
| ~ p__d__subclass(X1,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_3546) ).
cnf(i_0_981,plain,
p__d__subclass(c__AnatomicalStructure,c__OrganicObject),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_981) ).
cnf(i_0_3544,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__disjointDecomposition3(X3,X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_3544) ).
cnf(i_0_3503,plain,
( p__d__disjointDecomposition3(X1,X2,X3)
| ~ p__d__partition3(X1,X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_3503) ).
cnf(i_0_884,plain,
p__d__subclass(c__OrganicObject,c__CorpuscularObject),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_884) ).
cnf(i_0_990,plain,
p__d__subclass(c__BodyPart,c__AnatomicalStructure),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_990) ).
cnf(i_0_120,plain,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_120) ).
cnf(i_0_768,plain,
p__d__subclass(c__ContentBearingPhysical,c__Physical),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_768) ).
cnf(i_0_559,plain,
p__d__subclass(c__CorpuscularObject,c__SelfConnectedObject),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_559) ).
cnf(i_0_3489,plain,
( ~ p__d__instance(X1,X2)
| ~ p__d__instance(X1,X3)
| ~ p__d__disjoint(X3,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_3489) ).
cnf(i_0_3486,plain,
( p__d__instance(X1,X2)
| ~ p__d__instance(X1,X3)
| ~ p__d__subclass(X3,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_3486) ).
cnf(i_0_1204,plain,
p__d__subclass(c__Attribute,c__Abstract),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_1204) ).
cnf(i_0_128,plain,
( p__d__subclass(X1,c__Entity)
| ~ p__d__instance(X1,c__Class) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_128) ).
cnf(i_0_870,plain,
p__d__subclass(c__Icon,c__ContentBearingPhysical),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_870) ).
cnf(i_0_127,plain,
( p__d__instance(X1,c__Class)
| ~ p__d__subclass(X1,c__Entity) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_127) ).
cnf(i_0_129,plain,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_129) ).
cnf(i_0_152,plain,
p__d__subclass(c__SelfConnectedObject,c__Object),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_152) ).
cnf(i_0_3934,plain,
( p__d__instance(X1,c__Attribute)
| ~ p__subAttribute(X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_3934) ).
cnf(i_0_2613,plain,
p__subAttribute(c__Anxiety,c__Unhappiness),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_2613) ).
cnf(i_0_151,plain,
p__d__subclass(c__Object,c__Physical),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_151) ).
cnf(i_0_89,plain,
( p__d__instance(X1,X2)
| ~ p__d__instance(X3,X2)
| ~ p__subAttribute(X1,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_89) ).
cnf(i_0_1,negated_conjecture,
( X1 = X2
| p__d__instance(X2,c__BodyPart)
| ~ p__d__instance(X1,c__Icon) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_1) ).
cnf(i_0_126,plain,
( p__d__instance(esk15_1(X1),X1)
| ~ p__d__subclass(X1,c__Entity) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-c8xujcv7/input.p',i_0_126) ).
cnf(c_0_3958,plain,
( p__d__subclass(X1,X2)
| ~ p__d__subclass(X3,X2)
| ~ p__d__subclass(X1,X3) ),
i_0_3546 ).
cnf(c_0_3959,plain,
p__d__subclass(c__AnatomicalStructure,c__OrganicObject),
i_0_981 ).
cnf(c_0_3960,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__disjointDecomposition3(X3,X1,X2) ),
i_0_3544 ).
cnf(c_0_3961,plain,
( p__d__disjointDecomposition3(X1,X2,X3)
| ~ p__d__partition3(X1,X2,X3) ),
i_0_3503 ).
cnf(c_0_3962,plain,
p__d__subclass(c__OrganicObject,c__CorpuscularObject),
i_0_884 ).
cnf(c_0_3963,plain,
( p__d__subclass(X1,c__OrganicObject)
| ~ p__d__subclass(X1,c__AnatomicalStructure) ),
inference(spm,[status(thm)],[c_0_3958,c_0_3959]) ).
cnf(c_0_3964,plain,
p__d__subclass(c__BodyPart,c__AnatomicalStructure),
i_0_990 ).
cnf(c_0_3965,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__partition3(X3,X1,X2) ),
inference(spm,[status(thm)],[c_0_3960,c_0_3961]) ).
cnf(c_0_3966,plain,
p__d__partition3(c__Entity,c__Physical,c__Abstract),
i_0_120 ).
cnf(c_0_3967,plain,
p__d__subclass(c__ContentBearingPhysical,c__Physical),
i_0_768 ).
cnf(c_0_3968,plain,
p__d__subclass(c__CorpuscularObject,c__SelfConnectedObject),
i_0_559 ).
cnf(c_0_3969,plain,
( p__d__subclass(X1,c__CorpuscularObject)
| ~ p__d__subclass(X1,c__OrganicObject) ),
inference(spm,[status(thm)],[c_0_3958,c_0_3962]) ).
cnf(c_0_3970,plain,
p__d__subclass(c__BodyPart,c__OrganicObject),
inference(spm,[status(thm)],[c_0_3963,c_0_3964]) ).
cnf(c_0_3971,plain,
( ~ p__d__instance(X1,X2)
| ~ p__d__instance(X1,X3)
| ~ p__d__disjoint(X3,X2) ),
i_0_3489 ).
cnf(c_0_3972,plain,
p__d__disjoint(c__Physical,c__Abstract),
inference(spm,[status(thm)],[c_0_3965,c_0_3966]) ).
cnf(c_0_3973,plain,
( p__d__instance(X1,X2)
| ~ p__d__instance(X1,X3)
| ~ p__d__subclass(X3,X2) ),
i_0_3486 ).
cnf(c_0_3974,plain,
p__d__subclass(c__Attribute,c__Abstract),
i_0_1204 ).
cnf(c_0_3975,plain,
( p__d__subclass(X1,c__Entity)
| ~ p__d__instance(X1,c__Class) ),
i_0_128 ).
cnf(c_0_3976,plain,
( p__d__subclass(X1,c__Physical)
| ~ p__d__subclass(X1,c__ContentBearingPhysical) ),
inference(spm,[status(thm)],[c_0_3958,c_0_3967]) ).
cnf(c_0_3977,plain,
p__d__subclass(c__Icon,c__ContentBearingPhysical),
i_0_870 ).
cnf(c_0_3978,plain,
( p__d__instance(X1,c__Class)
| ~ p__d__subclass(X1,c__Entity) ),
i_0_127 ).
cnf(c_0_3979,plain,
p__d__subclass(c__Physical,c__Entity),
i_0_129 ).
cnf(c_0_3980,plain,
p__d__subclass(c__SelfConnectedObject,c__Object),
i_0_152 ).
cnf(c_0_3981,plain,
( p__d__subclass(X1,c__SelfConnectedObject)
| ~ p__d__subclass(X1,c__CorpuscularObject) ),
inference(spm,[status(thm)],[c_0_3958,c_0_3968]) ).
cnf(c_0_3982,plain,
p__d__subclass(c__BodyPart,c__CorpuscularObject),
inference(spm,[status(thm)],[c_0_3969,c_0_3970]) ).
cnf(c_0_3983,plain,
( ~ p__d__instance(X1,c__Physical)
| ~ p__d__instance(X1,c__Abstract) ),
inference(spm,[status(thm)],[c_0_3971,c_0_3972]) ).
cnf(c_0_3984,plain,
( p__d__instance(X1,c__Abstract)
| ~ p__d__instance(X1,c__Attribute) ),
inference(spm,[status(thm)],[c_0_3973,c_0_3974]) ).
cnf(c_0_3985,plain,
( p__d__instance(X1,c__Attribute)
| ~ p__subAttribute(X1,X2) ),
i_0_3934 ).
cnf(c_0_3986,plain,
p__subAttribute(c__Anxiety,c__Unhappiness),
i_0_2613 ).
cnf(c_0_3987,plain,
( p__d__subclass(X1,c__Entity)
| ~ p__d__subclass(X1,X2)
| ~ p__d__instance(X2,c__Class) ),
inference(spm,[status(thm)],[c_0_3958,c_0_3975]) ).
cnf(c_0_3988,plain,
p__d__subclass(c__Icon,c__Physical),
inference(spm,[status(thm)],[c_0_3976,c_0_3977]) ).
cnf(c_0_3989,plain,
p__d__instance(c__Physical,c__Class),
inference(spm,[status(thm)],[c_0_3978,c_0_3979]) ).
cnf(c_0_3990,plain,
( p__d__subclass(X1,c__Object)
| ~ p__d__subclass(X1,c__SelfConnectedObject) ),
inference(spm,[status(thm)],[c_0_3958,c_0_3980]) ).
cnf(c_0_3991,plain,
p__d__subclass(c__BodyPart,c__SelfConnectedObject),
inference(spm,[status(thm)],[c_0_3981,c_0_3982]) ).
cnf(c_0_3992,plain,
( ~ p__d__instance(X1,c__Physical)
| ~ p__d__instance(X1,c__Attribute) ),
inference(spm,[status(thm)],[c_0_3983,c_0_3984]) ).
cnf(c_0_3993,plain,
p__d__instance(c__Anxiety,c__Attribute),
inference(spm,[status(thm)],[c_0_3985,c_0_3986]) ).
cnf(c_0_3994,plain,
p__d__subclass(c__Object,c__Physical),
i_0_151 ).
cnf(c_0_3995,plain,
( p__d__instance(X1,X2)
| ~ p__d__instance(X3,X2)
| ~ p__subAttribute(X1,X3) ),
i_0_89 ).
cnf(c_0_3996,negated_conjecture,
( X1 = X2
| p__d__instance(X2,c__BodyPart)
| ~ p__d__instance(X1,c__Icon) ),
i_0_1 ).
cnf(c_0_3997,plain,
( p__d__instance(esk15_1(X1),X1)
| ~ p__d__subclass(X1,c__Entity) ),
i_0_126 ).
cnf(c_0_3998,plain,
p__d__subclass(c__Icon,c__Entity),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3987,c_0_3988]),c_0_3989])]) ).
cnf(c_0_3999,plain,
p__d__subclass(c__BodyPart,c__Object),
inference(spm,[status(thm)],[c_0_3990,c_0_3991]) ).
cnf(c_0_4000,plain,
~ p__d__instance(c__Anxiety,c__Physical),
inference(spm,[status(thm)],[c_0_3992,c_0_3993]) ).
cnf(c_0_4001,plain,
( p__d__instance(X1,c__Physical)
| ~ p__d__instance(X1,c__Object) ),
inference(spm,[status(thm)],[c_0_3973,c_0_3994]) ).
cnf(c_0_4002,plain,
( p__d__instance(X1,c__Physical)
| ~ p__d__instance(X1,c__Icon) ),
inference(spm,[status(thm)],[c_0_3973,c_0_3988]) ).
cnf(c_0_4003,plain,
( p__d__instance(c__Anxiety,X1)
| ~ p__d__instance(c__Unhappiness,X1) ),
inference(spm,[status(thm)],[c_0_3995,c_0_3986]) ).
cnf(c_0_4004,negated_conjecture,
( esk15_1(c__Icon) = X1
| p__d__instance(X1,c__BodyPart) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3996,c_0_3997]),c_0_3998])]) ).
cnf(c_0_4005,plain,
( p__d__instance(X1,c__Object)
| ~ p__d__instance(X1,c__BodyPart) ),
inference(spm,[status(thm)],[c_0_3973,c_0_3999]) ).
cnf(c_0_4006,plain,
~ p__d__instance(c__Anxiety,c__Object),
inference(spm,[status(thm)],[c_0_4000,c_0_4001]) ).
cnf(c_0_4007,plain,
~ p__d__instance(c__Unhappiness,c__Icon),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_4002,c_0_4003]),c_0_4000]) ).
cnf(c_0_4008,plain,
( p__d__instance(X1,c__BodyPart)
| p__d__instance(X1,c__Icon) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3997,c_0_4004]),c_0_3998])]) ).
cnf(c_0_4009,plain,
~ p__d__instance(c__Unhappiness,c__BodyPart),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_4005,c_0_4003]),c_0_4006]) ).
cnf(c_0_4010,plain,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_4007,c_0_4008]),c_0_4009]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : CSR229+1 : TPTP v8.1.0. Released v7.3.0.
% 0.03/0.13 % Command : enigmatic-eprover.py %s %d 1
% 0.14/0.34 % Computer : n021.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Fri Jun 10 02:29:25 EDT 2022
% 0.14/0.35 % CPUTime :
% 0.21/0.46 # ENIGMATIC: Selected SinE mode:
% 0.47/0.63 # Parsing /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.47/0.63 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.47/0.63 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.47/0.63 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 153.10/22.27 # ENIGMATIC: Solved by G_E___302_C18_F1_URBAN_S5PRR_S0Y:
% 153.10/22.27 # Version: 2.1pre011
% 153.10/22.27 # Preprocessing time : 0.122 s
% 153.10/22.27
% 153.10/22.27 # Proof found!
% 153.10/22.27 # SZS status Theorem
% 153.10/22.27 # SZS output start CNFRefutation
% See solution above
% 153.10/22.27 # Proof object total steps : 76
% 153.10/22.27 # Proof object clause steps : 53
% 153.10/22.27 # Proof object formula steps : 23
% 153.10/22.27 # Proof object conjectures : 3
% 153.10/22.27 # Proof object clause conjectures : 2
% 153.10/22.27 # Proof object formula conjectures : 1
% 153.10/22.27 # Proof object initial clauses used : 23
% 153.10/22.27 # Proof object initial formulas used : 23
% 153.10/22.27 # Proof object generating inferences : 30
% 153.10/22.27 # Proof object simplifying inferences : 9
% 153.10/22.27 # Training examples: 0 positive, 0 negative
% 153.10/22.27 # Parsed axioms : 4253
% 153.10/22.27 # Removed by relevancy pruning/SinE : 0
% 153.10/22.27 # Initial clauses : 4253
% 153.10/22.27 # Removed in clause preprocessing : 0
% 153.10/22.27 # Initial clauses in saturation : 4253
% 153.10/22.27 # Processed clauses : 15577
% 153.10/22.27 # ...of these trivial : 144
% 153.10/22.27 # ...subsumed : 2122
% 153.10/22.27 # ...remaining for further processing : 13311
% 153.10/22.27 # Other redundant clauses eliminated : 19
% 153.10/22.27 # Clauses deleted for lack of memory : 0
% 153.10/22.27 # Backward-subsumed : 134
% 153.10/22.27 # Backward-rewritten : 104
% 153.10/22.27 # Generated clauses : 76914
% 153.10/22.27 # ...of the previous two non-trivial : 75292
% 153.10/22.27 # Contextual simplify-reflections : 3506
% 153.10/22.27 # Paramodulations : 76800
% 153.10/22.27 # Factorizations : 2
% 153.10/22.27 # Equation resolutions : 112
% 153.10/22.27 # Propositional unsat checks : 2
% 153.10/22.27 # Propositional unsat check successes : 0
% 153.10/22.27 # Current number of processed clauses : 13069
% 153.10/22.27 # Positive orientable unit clauses : 2583
% 153.10/22.27 # Positive unorientable unit clauses: 0
% 153.10/22.27 # Negative unit clauses : 1271
% 153.10/22.27 # Non-unit-clauses : 9215
% 153.10/22.27 # Current number of unprocessed clauses: 63303
% 153.10/22.27 # ...number of literals in the above : 262522
% 153.10/22.27 # Current number of archived formulas : 0
% 153.10/22.27 # Current number of archived clauses : 238
% 153.10/22.27 # Clause-clause subsumption calls (NU) : 28505528
% 153.10/22.27 # Rec. Clause-clause subsumption calls : 7725163
% 153.10/22.27 # Non-unit clause-clause subsumptions : 5071
% 153.10/22.27 # Unit Clause-clause subsumption calls : 4004586
% 153.10/22.27 # Rewrite failures with RHS unbound : 0
% 153.10/22.27 # BW rewrite match attempts : 39
% 153.10/22.27 # BW rewrite match successes : 32
% 153.10/22.27 # Condensation attempts : 0
% 153.10/22.27 # Condensation successes : 0
% 153.10/22.27 # Termbank termtop insertions : 1376368
% 153.10/22.27
% 153.10/22.27 # -------------------------------------------------
% 153.10/22.27 # User time : 17.864 s
% 153.10/22.27 # System time : 0.107 s
% 153.10/22.27 # Total time : 17.971 s
% 153.10/22.27 # ...preprocessing : 0.122 s
% 153.10/22.27 # ...main loop : 17.849 s
% 153.10/22.27 # Maximum resident set size: 124564 pages
% 153.10/22.27
%------------------------------------------------------------------------------