%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : CSR106+7 : TPTP v8.1.0. Bugfixed 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:48:02 EDT 2022
% Result : Theorem 51.69s 11.10s
% Output : CNFRefutation 51.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 13
% Syntax : Number of clauses : 39 ( 15 unt; 6 nHn; 31 RR)
% Number of literals : 72 ( 9 equ; 36 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 9 con; 0-3 aty)
% Number of variables : 58 ( 17 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_2927,plain,
( s__instance(esk480_1(X1),s__TimePoint)
| ~ s__instance(X1,s__Object) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-irp4ea_j/input.p',i_0_2927) ).
cnf(i_0_2279,negated_conjecture,
~ s__instance(X1,s__TimePoint),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-irp4ea_j/input.p',i_0_2279) ).
cnf(i_0_2036,plain,
( s__instance(X1,X2)
| ~ s__instance(X1,X3)
| ~ s__subclass(X3,X2)
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-irp4ea_j/input.p',i_0_2036) ).
cnf(i_0_2034,plain,
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X2,X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-irp4ea_j/input.p',i_0_2034) ).
cnf(i_0_2035,plain,
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-irp4ea_j/input.p',i_0_2035) ).
cnf(i_0_2855,plain,
( X1 = s__UnionFn(X2,X3)
| s__instance(esk474_3(X3,X1,X2),X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-irp4ea_j/input.p',i_0_2855) ).
cnf(i_0_2170,plain,
( s__instance(esk448_1(X1),s__Object)
| ~ s__instance(X1,s__Physical) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-irp4ea_j/input.p',i_0_2170) ).
cnf(i_0_2210,plain,
s__subclass(s__Process,s__Physical),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-irp4ea_j/input.p',i_0_2210) ).
cnf(i_0_2293,plain,
( ~ s__earlier(X1,X1)
| ~ s__instance(X1,s__TimeInterval) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-irp4ea_j/input.p',i_0_2293) ).
cnf(i_0_2988,negated_conjecture,
( s__earlier(X1,X2)
| ~ s__instance(X2,s__TimeInterval)
| ~ s__instance(X1,s__TimeInterval) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-irp4ea_j/input.p',i_0_2988) ).
cnf(i_0_4461,plain,
( s__instance(esk839_1(X1),s__Process)
| ~ s__instance(X1,s__AboveTheLine) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-irp4ea_j/input.p',i_0_4461) ).
cnf(i_0_2856,plain,
( X1 = s__UnionFn(X2,X3)
| s__instance(esk473_3(X3,X1,X2),X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-irp4ea_j/input.p',i_0_2856) ).
cnf(i_0_163,plain,
s__instance(s__flows__m,s__TransitiveRelation),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-irp4ea_j/input.p',i_0_163) ).
cnf(c_0_4475,plain,
( s__instance(esk480_1(X1),s__TimePoint)
| ~ s__instance(X1,s__Object) ),
i_0_2927 ).
cnf(c_0_4476,negated_conjecture,
~ s__instance(X1,s__TimePoint),
i_0_2279 ).
cnf(c_0_4477,plain,
( s__instance(X1,X2)
| ~ s__instance(X1,X3)
| ~ s__subclass(X3,X2)
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass) ),
i_0_2036 ).
cnf(c_0_4478,plain,
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X2,X1) ),
i_0_2034 ).
cnf(c_0_4479,plain,
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X1,X2) ),
i_0_2035 ).
cnf(c_0_4480,plain,
( X1 = s__UnionFn(X2,X3)
| s__instance(esk474_3(X3,X1,X2),X1) ),
i_0_2855 ).
cnf(c_0_4481,plain,
~ s__instance(X1,s__Object),
inference(sr,[status(thm)],[c_0_4475,c_0_4476]) ).
cnf(c_0_4482,plain,
( s__instance(esk448_1(X1),s__Object)
| ~ s__instance(X1,s__Physical) ),
i_0_2170 ).
cnf(c_0_4483,plain,
( s__instance(X1,X2)
| ~ s__subclass(X3,X2)
| ~ s__instance(X1,X3) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_4477,c_0_4478]),c_0_4479]) ).
cnf(c_0_4484,plain,
s__subclass(s__Process,s__Physical),
i_0_2210 ).
cnf(c_0_4485,plain,
( ~ s__earlier(X1,X1)
| ~ s__instance(X1,s__TimeInterval) ),
i_0_2293 ).
cnf(c_0_4486,negated_conjecture,
( s__earlier(X1,X2)
| ~ s__instance(X2,s__TimeInterval)
| ~ s__instance(X1,s__TimeInterval) ),
i_0_2988 ).
cnf(c_0_4487,negated_conjecture,
s__UnionFn(X1,X2) = s__TimePoint,
inference(spm,[status(thm)],[c_0_4476,c_0_4480]) ).
cnf(c_0_4488,plain,
~ s__instance(X1,s__Physical),
inference(spm,[status(thm)],[c_0_4481,c_0_4482]) ).
cnf(c_0_4489,plain,
( s__instance(X1,s__Physical)
| ~ s__instance(X1,s__Process) ),
inference(spm,[status(thm)],[c_0_4483,c_0_4484]) ).
cnf(c_0_4490,plain,
~ s__instance(X1,s__TimeInterval),
inference(spm,[status(thm)],[c_0_4485,c_0_4486]) ).
cnf(c_0_4491,plain,
( X1 = s__TimePoint
| s__instance(esk474_3(X2,X1,X3),X1) ),
inference(rw,[status(thm)],[c_0_4480,c_0_4487]) ).
cnf(c_0_4492,plain,
~ s__instance(X1,s__Process),
inference(spm,[status(thm)],[c_0_4488,c_0_4489]) ).
cnf(c_0_4493,plain,
( s__instance(esk839_1(X1),s__Process)
| ~ s__instance(X1,s__AboveTheLine) ),
i_0_4461 ).
cnf(c_0_4494,plain,
( X1 = s__UnionFn(X2,X3)
| s__instance(esk473_3(X3,X1,X2),X3) ),
i_0_2856 ).
cnf(c_0_4495,plain,
s__TimePoint = s__TimeInterval,
inference(spm,[status(thm)],[c_0_4490,c_0_4491]) ).
cnf(c_0_4496,plain,
~ s__instance(X1,s__AboveTheLine),
inference(spm,[status(thm)],[c_0_4492,c_0_4493]) ).
cnf(c_0_4497,plain,
( X1 = s__TimeInterval
| s__instance(esk473_3(X2,X1,X3),X2) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_4494,c_0_4487]),c_0_4495]) ).
cnf(c_0_4498,plain,
s__instance(s__flows__m,s__TransitiveRelation),
i_0_163 ).
cnf(c_0_4499,plain,
X1 = s__TimeInterval,
inference(spm,[status(thm)],[c_0_4496,c_0_4497]) ).
cnf(c_0_4500,plain,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_4498,c_0_4499]),c_0_4499]),c_0_4490]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : CSR106+7 : TPTP v8.1.0. Bugfixed v7.3.0.
% 0.06/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.12/0.33 % Computer : n020.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Fri Jun 10 04:50:07 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.19/0.44 # ENIGMATIC: Selected SinE mode:
% 1.19/1.46 # Parsing /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.19/1.46 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 1.19/1.46 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 1.19/1.46 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 51.69/11.10 # ENIGMATIC: Solved by G_E___302_C18_F1_URBAN_S5PRR_RG_S04BN:
% 51.69/11.10 # Version: 2.1pre011
% 51.69/11.10 # Preprocessing time : 0.292 s
% 51.69/11.10
% 51.69/11.10 # Proof found!
% 51.69/11.10 # SZS status Theorem
% 51.69/11.10 # SZS output start CNFRefutation
% See solution above
% 51.69/11.10 # Proof object total steps : 39
% 51.69/11.10 # Proof object clause steps : 26
% 51.69/11.10 # Proof object formula steps : 13
% 51.69/11.10 # Proof object conjectures : 5
% 51.69/11.10 # Proof object clause conjectures : 3
% 51.69/11.10 # Proof object formula conjectures : 2
% 51.69/11.10 # Proof object initial clauses used : 13
% 51.69/11.10 # Proof object initial formulas used : 13
% 51.69/11.10 # Proof object generating inferences : 8
% 51.69/11.10 # Proof object simplifying inferences : 9
% 51.69/11.10 # Training examples: 0 positive, 0 negative
% 51.69/11.10 # Parsed axioms : 5372
% 51.69/11.10 # Removed by relevancy pruning/SinE : 0
% 51.69/11.10 # Initial clauses : 5372
% 51.69/11.10 # Removed in clause preprocessing : 0
% 51.69/11.10 # Initial clauses in saturation : 5372
% 51.69/11.10 # Processed clauses : 12057
% 51.69/11.10 # ...of these trivial : 162
% 51.69/11.10 # ...subsumed : 6054
% 51.69/11.10 # ...remaining for further processing : 5841
% 51.69/11.10 # Other redundant clauses eliminated : 15
% 51.69/11.10 # Clauses deleted for lack of memory : 0
% 51.69/11.10 # Backward-subsumed : 499
% 51.69/11.10 # Backward-rewritten : 5259
% 51.69/11.10 # Generated clauses : 52415
% 51.69/11.10 # ...of the previous two non-trivial : 52367
% 51.69/11.10 # Contextual simplify-reflections : 2094
% 51.69/11.10 # Paramodulations : 52356
% 51.69/11.10 # Factorizations : 26
% 51.69/11.10 # Equation resolutions : 25
% 51.69/11.10 # Propositional unsat checks : 1
% 51.69/11.10 # Propositional unsat check successes : 0
% 51.69/11.10 # Current number of processed clauses : 69
% 51.69/11.10 # Positive orientable unit clauses : 6
% 51.69/11.10 # Positive unorientable unit clauses: 1
% 51.69/11.10 # Negative unit clauses : 6
% 51.69/11.10 # Non-unit-clauses : 56
% 51.69/11.10 # Current number of unprocessed clauses: 89
% 51.69/11.10 # ...number of literals in the above : 630
% 51.69/11.10 # Current number of archived formulas : 0
% 51.69/11.10 # Current number of archived clauses : 5766
% 51.69/11.10 # Clause-clause subsumption calls (NU) : 10616750
% 51.69/11.10 # Rec. Clause-clause subsumption calls : 1317400
% 51.69/11.10 # Non-unit clause-clause subsumptions : 3586
% 51.69/11.10 # Unit Clause-clause subsumption calls : 929037
% 51.69/11.10 # Rewrite failures with RHS unbound : 0
% 51.69/11.10 # BW rewrite match attempts : 3194
% 51.69/11.10 # BW rewrite match successes : 2651
% 51.69/11.10 # Condensation attempts : 0
% 51.69/11.10 # Condensation successes : 0
% 51.69/11.10 # Termbank termtop insertions : 1436265
% 51.69/11.10
% 51.69/11.10 # -------------------------------------------------
% 51.69/11.10 # User time : 5.043 s
% 51.69/11.10 # System time : 0.061 s
% 51.69/11.10 # Total time : 5.104 s
% 51.69/11.10 # ...preprocessing : 0.292 s
% 51.69/11.10 # ...main loop : 4.813 s
% 51.69/11.10 # Maximum resident set size: 91092 pages
% 51.69/11.10
%------------------------------------------------------------------------------