%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : GEO572+1 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n012.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 : Sat Jul 16 03:46:21 EDT 2022
% Result : Theorem 10.75s 2.74s
% Output : CNFRefutation 10.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 23
% Syntax : Number of clauses : 74 ( 23 unt; 0 nHn; 59 RR)
% Number of literals : 137 ( 0 equ; 66 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-8 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-4 aty)
% Number of variables : 267 ( 14 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_83,plain,
( para(X1,X2,X3,X4)
| ~ perp(X5,X6,X3,X4)
| ~ perp(X1,X2,X5,X6) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_83) ).
cnf(i_0_88,plain,
( perp(esk10_4(X1,X2,X3,X4),X1,X1,X4)
| ~ circle(X4,X1,X2,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_88) ).
cnf(i_0_82,plain,
( perp(X1,X2,X3,X4)
| ~ perp(X3,X4,X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_82) ).
cnf(i_0_16,plain,
( eqangle(X1,X2,X3,X4,X5,X6,X7,X8)
| ~ eqangle(X2,X1,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_16) ).
cnf(i_0_41,plain,
( eqangle(X1,X2,X3,X4,X5,X6,X3,X4)
| ~ para(X1,X2,X5,X6) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_41) ).
cnf(i_0_3,negated_conjecture,
circle(esk5_0,esk4_0,esk2_0,esk3_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_3) ).
cnf(i_0_17,plain,
( eqangle(X1,X2,X3,X4,X5,X6,X7,X8)
| ~ eqangle(X3,X4,X1,X2,X7,X8,X5,X6) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_17) ).
cnf(i_0_39,plain,
( para(X1,X2,X3,X4)
| ~ eqangle(X1,X2,X5,X6,X3,X4,X5,X6) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_39) ).
cnf(i_0_52,plain,
( para(X1,X2,X3,X4)
| ~ para(X1,X2,X4,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_52) ).
cnf(i_0_70,plain,
( coll(X1,X2,X3)
| ~ para(X1,X2,X1,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_70) ).
cnf(i_0_29,plain,
( coll(X1,X2,X3)
| ~ coll(X2,X1,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_29) ).
cnf(i_0_18,plain,
( coll(X1,X2,X3)
| ~ coll(X1,X3,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_18) ).
cnf(i_0_40,plain,
( coll(X1,X2,X3)
| ~ coll(X3,X4,X2)
| ~ coll(X3,X4,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_40) ).
cnf(i_0_44,plain,
( cyclic(X1,X2,X3,X4)
| ~ coll(X3,X4,X2)
| ~ eqangle(X3,X1,X3,X2,X4,X1,X4,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_44) ).
cnf(i_0_20,plain,
( eqangle(X1,X2,X3,X4,X5,X6,X7,X8)
| ~ eqangle(X1,X2,X5,X6,X3,X4,X7,X8) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_20) ).
cnf(i_0_5,negated_conjecture,
perp(esk2_0,esk3_0,esk1_0,esk4_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_5) ).
cnf(i_0_79,plain,
( perp(X1,X2,X3,X4)
| ~ perp(X5,X6,X7,X8)
| ~ eqangle(X1,X2,X3,X4,X5,X6,X7,X8) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_79) ).
cnf(i_0_42,plain,
( eqangle(X1,X2,X1,X3,X4,X2,X4,X3)
| ~ cyclic(X2,X3,X1,X4) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_42) ).
cnf(i_0_15,plain,
( cyclic(X1,X2,X3,X4)
| ~ cyclic(X5,X1,X2,X4)
| ~ cyclic(X5,X1,X2,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_15) ).
cnf(i_0_4,negated_conjecture,
perp(esk3_0,esk4_0,esk4_0,esk6_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_4) ).
cnf(i_0_63,plain,
( para(X1,X2,X3,X4)
| ~ para(X3,X4,X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_63) ).
cnf(i_0_81,plain,
( perp(X1,X2,X3,X4)
| ~ perp(X1,X2,X4,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_81) ).
cnf(i_0_1,negated_conjecture,
~ para(esk1_0,esk4_0,esk2_0,esk6_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-vskhyjc5/input.p',i_0_1) ).
cnf(c_0_112,plain,
( para(X1,X2,X3,X4)
| ~ perp(X5,X6,X3,X4)
| ~ perp(X1,X2,X5,X6) ),
i_0_83 ).
cnf(c_0_113,plain,
( perp(esk10_4(X1,X2,X3,X4),X1,X1,X4)
| ~ circle(X4,X1,X2,X3) ),
i_0_88 ).
cnf(c_0_114,plain,
( perp(X1,X2,X3,X4)
| ~ perp(X3,X4,X1,X2) ),
i_0_82 ).
cnf(c_0_115,plain,
( para(X1,X2,X3,X4)
| ~ circle(X4,X3,X5,X6)
| ~ perp(X1,X2,esk10_4(X3,X5,X6,X4),X3) ),
inference(spm,[status(thm)],[c_0_112,c_0_113]) ).
cnf(c_0_116,plain,
( perp(X1,X2,esk10_4(X1,X3,X4,X2),X1)
| ~ circle(X2,X1,X3,X4) ),
inference(spm,[status(thm)],[c_0_114,c_0_113]) ).
cnf(c_0_117,plain,
( eqangle(X1,X2,X3,X4,X5,X6,X7,X8)
| ~ eqangle(X2,X1,X3,X4,X5,X6,X7,X8) ),
i_0_16 ).
cnf(c_0_118,plain,
( eqangle(X1,X2,X3,X4,X5,X6,X3,X4)
| ~ para(X1,X2,X5,X6) ),
i_0_41 ).
cnf(c_0_119,plain,
( para(X1,X2,X1,X2)
| ~ circle(X2,X1,X3,X4) ),
inference(spm,[status(thm)],[c_0_115,c_0_116]) ).
cnf(c_0_120,negated_conjecture,
circle(esk5_0,esk4_0,esk2_0,esk3_0),
i_0_3 ).
cnf(c_0_121,plain,
( eqangle(X1,X2,X3,X4,X5,X6,X7,X8)
| ~ eqangle(X3,X4,X1,X2,X7,X8,X5,X6) ),
i_0_17 ).
cnf(c_0_122,plain,
( para(X1,X2,X3,X4)
| ~ eqangle(X1,X2,X5,X6,X3,X4,X5,X6) ),
i_0_39 ).
cnf(c_0_123,plain,
( eqangle(X1,X2,X3,X4,X5,X6,X3,X4)
| ~ para(X2,X1,X5,X6) ),
inference(spm,[status(thm)],[c_0_117,c_0_118]) ).
cnf(c_0_124,plain,
( para(X1,X2,X3,X4)
| ~ para(X1,X2,X4,X3) ),
i_0_52 ).
cnf(c_0_125,negated_conjecture,
para(esk4_0,esk5_0,esk4_0,esk5_0),
inference(spm,[status(thm)],[c_0_119,c_0_120]) ).
cnf(c_0_126,plain,
( eqangle(X1,X2,X3,X4,X1,X2,X5,X6)
| ~ para(X3,X4,X5,X6) ),
inference(spm,[status(thm)],[c_0_121,c_0_118]) ).
cnf(c_0_127,plain,
( para(X1,X2,X3,X4)
| ~ para(X2,X1,X3,X4) ),
inference(spm,[status(thm)],[c_0_122,c_0_123]) ).
cnf(c_0_128,plain,
para(esk4_0,esk5_0,esk5_0,esk4_0),
inference(spm,[status(thm)],[c_0_124,c_0_125]) ).
cnf(c_0_129,plain,
( para(X1,X2,X1,X2)
| ~ para(X3,X4,X3,X4) ),
inference(spm,[status(thm)],[c_0_122,c_0_126]) ).
cnf(c_0_130,plain,
para(esk5_0,esk4_0,esk5_0,esk4_0),
inference(spm,[status(thm)],[c_0_127,c_0_128]) ).
cnf(c_0_131,plain,
( coll(X1,X2,X3)
| ~ para(X1,X2,X1,X3) ),
i_0_70 ).
cnf(c_0_132,plain,
para(X1,X2,X1,X2),
inference(spm,[status(thm)],[c_0_129,c_0_130]) ).
cnf(c_0_133,plain,
( coll(X1,X2,X3)
| ~ coll(X2,X1,X3) ),
i_0_29 ).
cnf(c_0_134,plain,
coll(X1,X2,X2),
inference(spm,[status(thm)],[c_0_131,c_0_132]) ).
cnf(c_0_135,plain,
( coll(X1,X2,X3)
| ~ coll(X1,X3,X2) ),
i_0_18 ).
cnf(c_0_136,plain,
coll(X1,X2,X1),
inference(spm,[status(thm)],[c_0_133,c_0_134]) ).
cnf(c_0_137,plain,
( coll(X1,X2,X3)
| ~ coll(X3,X4,X2)
| ~ coll(X3,X4,X1) ),
i_0_40 ).
cnf(c_0_138,plain,
coll(X1,X1,X2),
inference(spm,[status(thm)],[c_0_135,c_0_136]) ).
cnf(c_0_139,plain,
( cyclic(X1,X2,X3,X4)
| ~ coll(X3,X4,X2)
| ~ eqangle(X3,X1,X3,X2,X4,X1,X4,X2) ),
i_0_44 ).
cnf(c_0_140,plain,
coll(X1,X2,X3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_137,c_0_138]),c_0_138])]) ).
cnf(c_0_141,plain,
( eqangle(X1,X2,X3,X4,X5,X6,X7,X8)
| ~ eqangle(X1,X2,X5,X6,X3,X4,X7,X8) ),
i_0_20 ).
cnf(c_0_142,plain,
( cyclic(X1,X2,X3,X4)
| ~ eqangle(X3,X1,X3,X2,X4,X1,X4,X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_139,c_0_140])]) ).
cnf(c_0_143,plain,
( eqangle(X1,X2,X3,X4,X5,X6,X5,X6)
| ~ para(X1,X2,X3,X4) ),
inference(spm,[status(thm)],[c_0_141,c_0_118]) ).
cnf(c_0_144,negated_conjecture,
perp(esk2_0,esk3_0,esk1_0,esk4_0),
i_0_5 ).
cnf(c_0_145,plain,
( perp(X1,X2,X3,X4)
| ~ perp(X5,X6,X7,X8)
| ~ eqangle(X1,X2,X3,X4,X5,X6,X7,X8) ),
i_0_79 ).
cnf(c_0_146,plain,
( eqangle(X1,X2,X1,X3,X4,X2,X4,X3)
| ~ cyclic(X2,X3,X1,X4) ),
i_0_42 ).
cnf(c_0_147,plain,
( cyclic(X1,X2,X3,X4)
| ~ cyclic(X5,X1,X2,X4)
| ~ cyclic(X5,X1,X2,X3) ),
i_0_15 ).
cnf(c_0_148,plain,
cyclic(X1,X1,X2,X3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_142,c_0_143]),c_0_132])]) ).
cnf(c_0_149,negated_conjecture,
perp(esk3_0,esk4_0,esk4_0,esk6_0),
i_0_4 ).
cnf(c_0_150,plain,
( para(X1,X2,X3,X4)
| ~ para(X3,X4,X1,X2) ),
i_0_63 ).
cnf(c_0_151,negated_conjecture,
( para(X1,X2,esk1_0,esk4_0)
| ~ perp(X1,X2,esk2_0,esk3_0) ),
inference(spm,[status(thm)],[c_0_112,c_0_144]) ).
cnf(c_0_152,plain,
( perp(X1,X2,X1,X3)
| ~ cyclic(X2,X3,X1,X4)
| ~ perp(X4,X2,X4,X3) ),
inference(spm,[status(thm)],[c_0_145,c_0_146]) ).
cnf(c_0_153,plain,
cyclic(X1,X2,X3,X4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_147,c_0_148]),c_0_148])]) ).
cnf(c_0_154,plain,
( perp(X1,X2,X3,X4)
| ~ perp(X1,X2,X4,X3) ),
i_0_81 ).
cnf(c_0_155,negated_conjecture,
perp(esk4_0,esk6_0,esk3_0,esk4_0),
inference(spm,[status(thm)],[c_0_114,c_0_149]) ).
cnf(c_0_156,negated_conjecture,
~ para(esk1_0,esk4_0,esk2_0,esk6_0),
i_0_1 ).
cnf(c_0_157,plain,
( para(esk1_0,esk4_0,X1,X2)
| ~ perp(X1,X2,esk2_0,esk3_0) ),
inference(spm,[status(thm)],[c_0_150,c_0_151]) ).
cnf(c_0_158,plain,
( perp(X1,X2,X1,X3)
| ~ perp(X4,X2,X4,X3) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_152,c_0_153])]) ).
cnf(c_0_159,plain,
perp(esk4_0,esk6_0,esk4_0,esk3_0),
inference(spm,[status(thm)],[c_0_154,c_0_155]) ).
cnf(c_0_160,negated_conjecture,
~ perp(esk2_0,esk6_0,esk2_0,esk3_0),
inference(spm,[status(thm)],[c_0_156,c_0_157]) ).
cnf(c_0_161,plain,
perp(X1,esk6_0,X1,esk3_0),
inference(spm,[status(thm)],[c_0_158,c_0_159]) ).
cnf(c_0_162,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_160,c_0_161])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO572+1 : TPTP v8.1.0. Released v7.5.0.
% 0.03/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.12/0.33 % Computer : n012.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 17 15:12:55 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.19/0.44 # ENIGMATIC: Selected SinE mode:
% 0.19/0.45 # Parsing /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.19/0.45 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.19/0.45 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 10.75/2.74 # ENIGMATIC: Solved by G_E___302_C18_F1_URBAN_S5PRR_RG_S04BN:
% 10.75/2.74 # Version: 2.1pre011
% 10.75/2.74 # Preprocessing time : 0.013 s
% 10.75/2.74
% 10.75/2.74 # Proof found!
% 10.75/2.74 # SZS status Theorem
% 10.75/2.74 # SZS output start CNFRefutation
% See solution above
% 10.75/2.74 # Proof object total steps : 74
% 10.75/2.74 # Proof object clause steps : 51
% 10.75/2.74 # Proof object formula steps : 23
% 10.75/2.74 # Proof object conjectures : 13
% 10.75/2.74 # Proof object clause conjectures : 9
% 10.75/2.74 # Proof object formula conjectures : 4
% 10.75/2.74 # Proof object initial clauses used : 23
% 10.75/2.74 # Proof object initial formulas used : 23
% 10.75/2.74 # Proof object generating inferences : 25
% 10.75/2.74 # Proof object simplifying inferences : 12
% 10.75/2.74 # Training examples: 0 positive, 0 negative
% 10.75/2.74 # Parsed axioms : 120
% 10.75/2.74 # Removed by relevancy pruning/SinE : 0
% 10.75/2.74 # Initial clauses : 120
% 10.75/2.74 # Removed in clause preprocessing : 0
% 10.75/2.74 # Initial clauses in saturation : 120
% 10.75/2.74 # Processed clauses : 1558
% 10.75/2.74 # ...of these trivial : 52
% 10.75/2.74 # ...subsumed : 318
% 10.75/2.74 # ...remaining for further processing : 1188
% 10.75/2.74 # Other redundant clauses eliminated : 0
% 10.75/2.74 # Clauses deleted for lack of memory : 0
% 10.75/2.74 # Backward-subsumed : 39
% 10.75/2.74 # Backward-rewritten : 443
% 10.75/2.74 # Generated clauses : 8997
% 10.75/2.74 # ...of the previous two non-trivial : 8547
% 10.75/2.74 # Contextual simplify-reflections : 35
% 10.75/2.74 # Paramodulations : 8997
% 10.75/2.74 # Factorizations : 0
% 10.75/2.74 # Equation resolutions : 0
% 10.75/2.74 # Propositional unsat checks : 0
% 10.75/2.74 # Propositional unsat check successes : 0
% 10.75/2.74 # Current number of processed clauses : 706
% 10.75/2.74 # Positive orientable unit clauses : 129
% 10.75/2.74 # Positive unorientable unit clauses: 0
% 10.75/2.74 # Negative unit clauses : 6
% 10.75/2.74 # Non-unit-clauses : 571
% 10.75/2.74 # Current number of unprocessed clauses: 4111
% 10.75/2.74 # ...number of literals in the above : 13455
% 10.75/2.74 # Current number of archived formulas : 0
% 10.75/2.74 # Current number of archived clauses : 482
% 10.75/2.74 # Clause-clause subsumption calls (NU) : 71626
% 10.75/2.74 # Rec. Clause-clause subsumption calls : 42408
% 10.75/2.74 # Non-unit clause-clause subsumptions : 375
% 10.75/2.74 # Unit Clause-clause subsumption calls : 7811
% 10.75/2.74 # Rewrite failures with RHS unbound : 0
% 10.75/2.74 # BW rewrite match attempts : 1803
% 10.75/2.74 # BW rewrite match successes : 338
% 10.75/2.74 # Condensation attempts : 0
% 10.75/2.74 # Condensation successes : 0
% 10.75/2.74 # Termbank termtop insertions : 114530
% 10.75/2.74
% 10.75/2.74 # -------------------------------------------------
% 10.75/2.74 # User time : 0.192 s
% 10.75/2.74 # System time : 0.007 s
% 10.75/2.74 # Total time : 0.199 s
% 10.75/2.74 # ...preprocessing : 0.013 s
% 10.75/2.74 # ...main loop : 0.186 s
% 10.75/2.74 # Maximum resident set size: 9996 pages
% 10.75/2.74
%------------------------------------------------------------------------------