%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : CSR182+1 : TPTP v8.1.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n020.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:49:55 EDT 2022
% Result : Theorem 161.57s 23.65s
% Output : CNFRefutation 161.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 18
% Syntax : Number of clauses : 64 ( 33 unt; 0 nHn; 64 RR)
% Number of literals : 101 ( 0 equ; 42 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-7 aty)
% Number of functors : 17 ( 17 usr; 16 con; 0-1 aty)
% Number of variables : 63 ( 10 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_3280,plain,
( p__d__disjointDecomposition7(X1,X2,X3,X4,X5,X6,X7)
| ~ p__d__partition7(X1,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_3280) ).
cnf(i_0_847,plain,
p__d__partition7(c__Communication,c__Stating,c__Supposing,c__Directing,c__Committing,c__Expressing,c__Declaring),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_847) ).
cnf(i_0_3275,plain,
( p__d__instance(X1,X2)
| ~ p__d__instance(X1,X3)
| ~ p__d__subclass(X3,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_3275) ).
cnf(i_0_3274,negated_conjecture,
p__d__subclass(esk699_0,c__Confirming),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_3274) ).
cnf(i_0_3273,negated_conjecture,
p__d__subclass(esk699_0,c__Accrediting),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_3273) ).
cnf(i_0_3365,plain,
( p__d__subclass(X1,X2)
| ~ p__d__subclass(X3,X2)
| ~ p__d__subclass(X1,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_3365) ).
cnf(i_0_869,plain,
p__d__subclass(c__LinguisticCommunication,c__Communication),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_869) ).
cnf(i_0_877,plain,
p__d__subclass(c__Stating,c__LinguisticCommunication),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_877) ).
cnf(i_0_3073,plain,
p__d__subclass(c__Confirming,c__Stating),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_3073) ).
cnf(i_0_3335,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__disjointDecomposition7(X3,X1,X4,X5,X6,X7,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_3335) ).
cnf(i_0_205,plain,
( p__d__instance(esk29_1(X1),X1)
| ~ p__d__subclass(X1,c__Entity) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_205) ).
cnf(i_0_1886,plain,
p__d__subclass(c__Accrediting,c__Declaring),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_1886) ).
cnf(i_0_845,plain,
p__d__subclass(c__SocialInteraction,c__IntentionalProcess),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_845) ).
cnf(i_0_846,plain,
p__d__subclass(c__Communication,c__SocialInteraction),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_846) ).
cnf(i_0_3278,plain,
( ~ p__d__instance(X1,X2)
| ~ p__d__instance(X1,X3)
| ~ p__d__disjoint(X3,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_3278) ).
cnf(i_0_213,plain,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_213) ).
cnf(i_0_580,plain,
p__d__subclass(c__IntentionalProcess,c__Process),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_580) ).
cnf(i_0_1277,plain,
p__d__subclass(c__Process,c__Physical),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-xsuukzs5/input.p',i_0_1277) ).
cnf(c_0_3384,plain,
( p__d__disjointDecomposition7(X1,X2,X3,X4,X5,X6,X7)
| ~ p__d__partition7(X1,X2,X3,X4,X5,X6,X7) ),
i_0_3280 ).
cnf(c_0_3385,plain,
p__d__partition7(c__Communication,c__Stating,c__Supposing,c__Directing,c__Committing,c__Expressing,c__Declaring),
i_0_847 ).
cnf(c_0_3386,plain,
( p__d__instance(X1,X2)
| ~ p__d__instance(X1,X3)
| ~ p__d__subclass(X3,X2) ),
i_0_3275 ).
cnf(c_0_3387,negated_conjecture,
p__d__subclass(esk699_0,c__Confirming),
i_0_3274 ).
cnf(c_0_3388,negated_conjecture,
p__d__subclass(esk699_0,c__Accrediting),
i_0_3273 ).
cnf(c_0_3389,plain,
( p__d__subclass(X1,X2)
| ~ p__d__subclass(X3,X2)
| ~ p__d__subclass(X1,X3) ),
i_0_3365 ).
cnf(c_0_3390,plain,
p__d__subclass(c__LinguisticCommunication,c__Communication),
i_0_869 ).
cnf(c_0_3391,plain,
p__d__subclass(c__Stating,c__LinguisticCommunication),
i_0_877 ).
cnf(c_0_3392,plain,
p__d__subclass(c__Confirming,c__Stating),
i_0_3073 ).
cnf(c_0_3393,plain,
( p__d__disjoint(X1,X2)
| ~ p__d__disjointDecomposition7(X3,X1,X4,X5,X6,X7,X2) ),
i_0_3335 ).
cnf(c_0_3394,plain,
p__d__disjointDecomposition7(c__Communication,c__Stating,c__Supposing,c__Directing,c__Committing,c__Expressing,c__Declaring),
inference(spm,[status(thm)],[c_0_3384,c_0_3385]) ).
cnf(c_0_3395,negated_conjecture,
( p__d__instance(X1,c__Confirming)
| ~ p__d__instance(X1,esk699_0) ),
inference(spm,[status(thm)],[c_0_3386,c_0_3387]) ).
cnf(c_0_3396,plain,
( p__d__instance(esk29_1(X1),X1)
| ~ p__d__subclass(X1,c__Entity) ),
i_0_205 ).
cnf(c_0_3397,plain,
p__d__subclass(c__Accrediting,c__Declaring),
i_0_1886 ).
cnf(c_0_3398,negated_conjecture,
( p__d__instance(X1,c__Accrediting)
| ~ p__d__instance(X1,esk699_0) ),
inference(spm,[status(thm)],[c_0_3386,c_0_3388]) ).
cnf(c_0_3399,plain,
p__d__subclass(c__SocialInteraction,c__IntentionalProcess),
i_0_845 ).
cnf(c_0_3400,plain,
p__d__subclass(c__Communication,c__SocialInteraction),
i_0_846 ).
cnf(c_0_3401,plain,
( p__d__subclass(X1,c__Communication)
| ~ p__d__subclass(X1,c__LinguisticCommunication) ),
inference(spm,[status(thm)],[c_0_3389,c_0_3390]) ).
cnf(c_0_3402,plain,
( p__d__subclass(X1,c__LinguisticCommunication)
| ~ p__d__subclass(X1,c__Stating) ),
inference(spm,[status(thm)],[c_0_3389,c_0_3391]) ).
cnf(c_0_3403,plain,
( p__d__subclass(X1,c__Stating)
| ~ p__d__subclass(X1,c__Confirming) ),
inference(spm,[status(thm)],[c_0_3389,c_0_3392]) ).
cnf(c_0_3404,plain,
( ~ p__d__instance(X1,X2)
| ~ p__d__instance(X1,X3)
| ~ p__d__disjoint(X3,X2) ),
i_0_3278 ).
cnf(c_0_3405,plain,
p__d__disjoint(c__Stating,c__Declaring),
inference(spm,[status(thm)],[c_0_3393,c_0_3394]) ).
cnf(c_0_3406,plain,
( p__d__instance(X1,c__Stating)
| ~ p__d__instance(X1,c__Confirming) ),
inference(spm,[status(thm)],[c_0_3386,c_0_3392]) ).
cnf(c_0_3407,plain,
( p__d__instance(esk29_1(esk699_0),c__Confirming)
| ~ p__d__subclass(esk699_0,c__Entity) ),
inference(spm,[status(thm)],[c_0_3395,c_0_3396]) ).
cnf(c_0_3408,plain,
( p__d__instance(X1,c__Declaring)
| ~ p__d__instance(X1,c__Accrediting) ),
inference(spm,[status(thm)],[c_0_3386,c_0_3397]) ).
cnf(c_0_3409,plain,
( p__d__instance(esk29_1(esk699_0),c__Accrediting)
| ~ p__d__subclass(esk699_0,c__Entity) ),
inference(spm,[status(thm)],[c_0_3398,c_0_3396]) ).
cnf(c_0_3410,plain,
( p__d__subclass(X1,c__IntentionalProcess)
| ~ p__d__subclass(X1,c__SocialInteraction) ),
inference(spm,[status(thm)],[c_0_3389,c_0_3399]) ).
cnf(c_0_3411,plain,
( p__d__subclass(X1,c__SocialInteraction)
| ~ p__d__subclass(X1,c__Communication) ),
inference(spm,[status(thm)],[c_0_3389,c_0_3400]) ).
cnf(c_0_3412,plain,
( p__d__subclass(X1,c__Communication)
| ~ p__d__subclass(X1,c__Stating) ),
inference(spm,[status(thm)],[c_0_3401,c_0_3402]) ).
cnf(c_0_3413,negated_conjecture,
p__d__subclass(esk699_0,c__Stating),
inference(spm,[status(thm)],[c_0_3403,c_0_3387]) ).
cnf(c_0_3414,plain,
( ~ p__d__instance(X1,c__Stating)
| ~ p__d__instance(X1,c__Declaring) ),
inference(spm,[status(thm)],[c_0_3404,c_0_3405]) ).
cnf(c_0_3415,plain,
( p__d__instance(esk29_1(esk699_0),c__Stating)
| ~ p__d__subclass(esk699_0,c__Entity) ),
inference(spm,[status(thm)],[c_0_3406,c_0_3407]) ).
cnf(c_0_3416,plain,
( p__d__instance(esk29_1(esk699_0),c__Declaring)
| ~ p__d__subclass(esk699_0,c__Entity) ),
inference(spm,[status(thm)],[c_0_3408,c_0_3409]) ).
cnf(c_0_3417,plain,
p__d__subclass(c__Physical,c__Entity),
i_0_213 ).
cnf(c_0_3418,plain,
p__d__subclass(c__IntentionalProcess,c__Process),
i_0_580 ).
cnf(c_0_3419,plain,
( p__d__subclass(X1,c__IntentionalProcess)
| ~ p__d__subclass(X1,c__Communication) ),
inference(spm,[status(thm)],[c_0_3410,c_0_3411]) ).
cnf(c_0_3420,negated_conjecture,
p__d__subclass(esk699_0,c__Communication),
inference(spm,[status(thm)],[c_0_3412,c_0_3413]) ).
cnf(c_0_3421,plain,
~ p__d__subclass(esk699_0,c__Entity),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3414,c_0_3415]),c_0_3416]) ).
cnf(c_0_3422,plain,
( p__d__subclass(X1,c__Entity)
| ~ p__d__subclass(X1,c__Physical) ),
inference(spm,[status(thm)],[c_0_3389,c_0_3417]) ).
cnf(c_0_3423,plain,
p__d__subclass(c__Process,c__Physical),
i_0_1277 ).
cnf(c_0_3424,plain,
( p__d__subclass(X1,c__Process)
| ~ p__d__subclass(X1,c__IntentionalProcess) ),
inference(spm,[status(thm)],[c_0_3389,c_0_3418]) ).
cnf(c_0_3425,plain,
p__d__subclass(esk699_0,c__IntentionalProcess),
inference(spm,[status(thm)],[c_0_3419,c_0_3420]) ).
cnf(c_0_3426,plain,
~ p__d__subclass(esk699_0,c__Physical),
inference(spm,[status(thm)],[c_0_3421,c_0_3422]) ).
cnf(c_0_3427,plain,
( p__d__subclass(X1,c__Physical)
| ~ p__d__subclass(X1,c__Process) ),
inference(spm,[status(thm)],[c_0_3389,c_0_3423]) ).
cnf(c_0_3428,plain,
p__d__subclass(esk699_0,c__Process),
inference(spm,[status(thm)],[c_0_3424,c_0_3425]) ).
cnf(c_0_3429,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3426,c_0_3427]),c_0_3428])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR182+1 : TPTP v8.1.0. Released v7.3.0.
% 0.07/0.13 % Command : enigmatic-eprover.py %s %d 1
% 0.12/0.34 % Computer : n020.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Sat Jun 11 12:10:37 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.19/0.45 # ENIGMATIC: Selected SinE mode:
% 0.45/0.63 # Parsing /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.45/0.63 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.45/0.63 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.45/0.63 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 161.57/23.65 # ENIGMATIC: Solved by G_E___302_C18_F1_URBAN_S5PRR_RG_S0Y:
% 161.57/23.65 # Version: 2.1pre011
% 161.57/23.65 # Preprocessing time : 0.163 s
% 161.57/23.65
% 161.57/23.65 # Proof found!
% 161.57/23.65 # SZS status Theorem
% 161.57/23.65 # SZS output start CNFRefutation
% See solution above
% 161.57/23.65 # Proof object total steps : 64
% 161.57/23.65 # Proof object clause steps : 46
% 161.57/23.65 # Proof object formula steps : 18
% 161.57/23.65 # Proof object conjectures : 8
% 161.57/23.65 # Proof object clause conjectures : 6
% 161.57/23.65 # Proof object formula conjectures : 2
% 161.57/23.65 # Proof object initial clauses used : 18
% 161.57/23.65 # Proof object initial formulas used : 18
% 161.57/23.65 # Proof object generating inferences : 28
% 161.57/23.65 # Proof object simplifying inferences : 3
% 161.57/23.65 # Training examples: 0 positive, 0 negative
% 161.57/23.65 # Parsed axioms : 4311
% 161.57/23.65 # Removed by relevancy pruning/SinE : 0
% 161.57/23.65 # Initial clauses : 4311
% 161.57/23.65 # Removed in clause preprocessing : 0
% 161.57/23.65 # Initial clauses in saturation : 4311
% 161.57/23.65 # Processed clauses : 17608
% 161.57/23.65 # ...of these trivial : 151
% 161.57/23.65 # ...subsumed : 2451
% 161.57/23.65 # ...remaining for further processing : 15006
% 161.57/23.65 # Other redundant clauses eliminated : 13
% 161.57/23.65 # Clauses deleted for lack of memory : 0
% 161.57/23.65 # Backward-subsumed : 102
% 161.57/23.65 # Backward-rewritten : 53
% 161.57/23.65 # Generated clauses : 72915
% 161.57/23.65 # ...of the previous two non-trivial : 70013
% 161.57/23.65 # Contextual simplify-reflections : 3269
% 161.57/23.65 # Paramodulations : 72840
% 161.57/23.65 # Factorizations : 0
% 161.57/23.65 # Equation resolutions : 75
% 161.57/23.65 # Propositional unsat checks : 3
% 161.57/23.65 # Propositional unsat check successes : 0
% 161.57/23.65 # Current number of processed clauses : 14847
% 161.57/23.65 # Positive orientable unit clauses : 2740
% 161.57/23.65 # Positive unorientable unit clauses: 0
% 161.57/23.65 # Negative unit clauses : 2754
% 161.57/23.65 # Non-unit-clauses : 9353
% 161.57/23.65 # Current number of unprocessed clauses: 56034
% 161.57/23.65 # ...number of literals in the above : 202534
% 161.57/23.65 # Current number of archived formulas : 0
% 161.57/23.65 # Current number of archived clauses : 155
% 161.57/23.65 # Clause-clause subsumption calls (NU) : 21225266
% 161.57/23.65 # Rec. Clause-clause subsumption calls : 6663606
% 161.57/23.65 # Non-unit clause-clause subsumptions : 4544
% 161.57/23.65 # Unit Clause-clause subsumption calls : 8581337
% 161.57/23.65 # Rewrite failures with RHS unbound : 0
% 161.57/23.65 # BW rewrite match attempts : 104
% 161.57/23.65 # BW rewrite match successes : 28
% 161.57/23.65 # Condensation attempts : 0
% 161.57/23.65 # Condensation successes : 0
% 161.57/23.65 # Termbank termtop insertions : 1477637
% 161.57/23.65
% 161.57/23.65 # -------------------------------------------------
% 161.57/23.65 # User time : 18.840 s
% 161.57/23.65 # System time : 0.130 s
% 161.57/23.65 # Total time : 18.970 s
% 161.57/23.65 # ...preprocessing : 0.163 s
% 161.57/23.65 # ...main loop : 18.808 s
% 161.57/23.65 # Maximum resident set size: 133396 pages
% 161.57/23.65
%------------------------------------------------------------------------------