%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : LCL652+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:47:11 AM UTC 2026
% Result : Theorem 35.50s 7.14s
% Output : CNFRefutation 35.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 39
% Syntax : Number of clauses : 136 ( 46 unt; 42 nHn; 136 RR)
% Number of literals : 398 ( 0 equ; 222 neg)
% Maximal clause size : 8 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 16 con; 0-3 aty)
% Number of variables : 183 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_237,plain,
( epred3_1(X1)
| ~ epred4_1(X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_237) ).
cnf(i_0_81,negated_conjecture,
r1(esk34_0,esk38_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_81) ).
cnf(i_0_129,negated_conjecture,
( epred4_1(X1)
| ~ r1(X2,X3)
| ~ r1(X3,X1)
| ~ r1(esk1_0,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_129) ).
cnf(i_0_117,negated_conjecture,
r1(esk1_0,esk14_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_117) ).
cnf(i_0_187,plain,
( epred1_1(X1)
| ~ epred2_1(X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_187) ).
cnf(i_0_33,negated_conjecture,
r1(esk66_0,esk70_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_33) ).
cnf(i_0_212,plain,
( epred2_1(X1)
| ~ epred3_1(X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_212) ).
cnf(i_0_57,negated_conjecture,
r1(esk50_0,esk54_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_57) ).
cnf(i_0_87,negated_conjecture,
r1(esk30_0,esk34_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_87) ).
cnf(i_0_111,negated_conjecture,
r1(esk14_0,esk18_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_111) ).
cnf(i_0_39,negated_conjecture,
r1(esk62_0,esk66_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_39) ).
cnf(i_0_63,negated_conjecture,
r1(esk46_0,esk50_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_63) ).
cnf(i_0_93,negated_conjecture,
r1(esk26_0,esk30_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_93) ).
cnf(i_0_105,negated_conjecture,
r1(esk18_0,esk22_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_105) ).
cnf(i_0_45,negated_conjecture,
r1(esk58_0,esk62_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_45) ).
cnf(i_0_69,negated_conjecture,
r1(esk42_0,esk46_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_69) ).
cnf(i_0_99,negated_conjecture,
r1(esk22_0,esk26_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_99) ).
cnf(i_0_51,negated_conjecture,
r1(esk54_0,esk58_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_51) ).
cnf(i_0_75,negated_conjecture,
r1(esk38_0,esk42_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_75) ).
cnf(i_0_150,plain,
( r1(X1,esk98_1(X1))
| r1(X1,esk100_1(X1))
| ~ epred1_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_150) ).
cnf(i_0_178,plain,
( r1(X1,esk87_2(X2,X1))
| ~ epred1_1(X2)
| ~ r1(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_178) ).
cnf(i_0_175,plain,
( p2(esk87_2(X1,X2))
| ~ epred1_1(X1)
| ~ r1(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_175) ).
cnf(i_0_144,plain,
( p2(esk98_1(X1))
| r1(X1,esk100_1(X1))
| ~ epred1_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_144) ).
cnf(i_0_149,plain,
( r1(X1,esk98_1(X1))
| ~ p2(X2)
| ~ epred1_1(X1)
| ~ r1(esk100_1(X1),X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_149) ).
cnf(i_0_160,plain,
( r1(X1,esk94_2(X2,X1))
| r1(X1,esk95_2(X2,X1))
| ~ epred1_1(X2)
| ~ r1(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_160) ).
cnf(i_0_143,plain,
( p2(esk98_1(X1))
| ~ p2(X2)
| ~ epred1_1(X1)
| ~ r1(esk100_1(X1),X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_143) ).
cnf(i_0_170,plain,
( p2(X1)
| r1(X2,esk90_3(X3,X4,X2))
| ~ p2(X4)
| ~ epred1_1(X3)
| ~ r1(X4,X1)
| ~ r1(X4,X2)
| ~ r1(X3,X4) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_170) ).
cnf(i_0_32,negated_conjecture,
( r1(X1,esk71_1(X1))
| ~ r1(esk70_0,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_32) ).
cnf(i_0_31,negated_conjecture,
( ~ p2(esk71_1(X1))
| ~ r1(esk70_0,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_31) ).
cnf(i_0_159,plain,
( r1(X1,esk94_2(X2,X1))
| r1(X3,esk96_3(X2,X1,X3))
| ~ epred1_1(X2)
| ~ r1(X2,X1)
| ~ r1(esk95_2(X2,X1),X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_159) ).
cnf(i_0_156,plain,
( p2(esk96_3(X1,X2,X3))
| r1(X2,esk94_2(X1,X2))
| ~ epred1_1(X1)
| ~ r1(X1,X2)
| ~ r1(esk95_2(X1,X2),X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_156) ).
cnf(i_0_169,plain,
( p2(X1)
| ~ p2(X2)
| ~ p2(X3)
| ~ epred1_1(X4)
| ~ r1(X3,X1)
| ~ r1(X3,X5)
| ~ r1(X4,X3)
| ~ r1(esk90_3(X4,X3,X5),X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_169) ).
cnf(i_0_168,plain,
( r1(X1,esk93_1(X1))
| r1(X2,esk91_3(X1,X3,X2))
| ~ epred1_1(X1)
| ~ r1(X3,X2)
| ~ r1(X1,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_168) ).
cnf(i_0_162,plain,
( r1(X1,esk93_1(X1))
| p2(esk91_3(X1,X2,X3))
| ~ epred1_1(X1)
| ~ r1(X2,X3)
| ~ r1(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_162) ).
cnf(i_0_167,plain,
( r1(X1,esk91_3(X2,X3,X1))
| ~ p2(X4)
| ~ epred1_1(X2)
| ~ r1(X3,X1)
| ~ r1(X2,X3)
| ~ r1(esk93_1(X2),X4) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_167) ).
cnf(i_0_161,plain,
( p2(esk91_3(X1,X2,X3))
| ~ p2(X4)
| ~ epred1_1(X1)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(esk93_1(X1),X4) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_161) ).
cnf(i_0_155,plain,
( r1(X1,esk95_2(X2,X1))
| ~ p2(X3)
| ~ epred1_1(X2)
| ~ r1(X2,X1)
| ~ r1(esk94_2(X2,X1),X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_155) ).
cnf(i_0_154,plain,
( r1(X1,esk96_3(X2,X3,X1))
| ~ p2(X4)
| ~ epred1_1(X2)
| ~ r1(X2,X3)
| ~ r1(esk94_2(X2,X3),X4)
| ~ r1(esk95_2(X2,X3),X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_154) ).
cnf(i_0_151,plain,
( p2(esk96_3(X1,X2,X3))
| ~ p2(X4)
| ~ epred1_1(X1)
| ~ r1(X1,X2)
| ~ r1(esk94_2(X1,X2),X4)
| ~ r1(esk95_2(X1,X2),X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-9v_wwmet/lgb.p',i_0_151) ).
cnf(c_0_277,plain,
( epred3_1(X1)
| ~ epred4_1(X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X1) ),
i_0_237 ).
cnf(c_0_278,negated_conjecture,
r1(esk34_0,esk38_0),
i_0_81 ).
cnf(c_0_279,negated_conjecture,
( epred4_1(X1)
| ~ r1(X2,X3)
| ~ r1(X3,X1)
| ~ r1(esk1_0,X2) ),
i_0_129 ).
cnf(c_0_280,negated_conjecture,
r1(esk1_0,esk14_0),
i_0_117 ).
cnf(c_0_281,plain,
( epred1_1(X1)
| ~ epred2_1(X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X1) ),
i_0_187 ).
cnf(c_0_282,negated_conjecture,
r1(esk66_0,esk70_0),
i_0_33 ).
cnf(c_0_283,plain,
( epred2_1(X1)
| ~ epred3_1(X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X1) ),
i_0_212 ).
cnf(c_0_284,negated_conjecture,
r1(esk50_0,esk54_0),
i_0_57 ).
cnf(c_0_285,negated_conjecture,
( epred3_1(esk38_0)
| ~ epred4_1(X1)
| ~ r1(X2,esk34_0)
| ~ r1(X3,X2)
| ~ r1(X1,X3) ),
inference(spm,[status(thm)],[c_0_277,c_0_278]) ).
cnf(c_0_286,negated_conjecture,
r1(esk30_0,esk34_0),
i_0_87 ).
cnf(c_0_287,negated_conjecture,
( epred4_1(X1)
| ~ r1(esk14_0,X2)
| ~ r1(X2,X1) ),
inference(spm,[status(thm)],[c_0_279,c_0_280]) ).
cnf(c_0_288,negated_conjecture,
r1(esk14_0,esk18_0),
i_0_111 ).
cnf(c_0_289,negated_conjecture,
( epred1_1(esk70_0)
| ~ epred2_1(X1)
| ~ r1(X2,esk66_0)
| ~ r1(X3,X2)
| ~ r1(X1,X3) ),
inference(spm,[status(thm)],[c_0_281,c_0_282]) ).
cnf(c_0_290,negated_conjecture,
r1(esk62_0,esk66_0),
i_0_39 ).
cnf(c_0_291,negated_conjecture,
( epred2_1(esk54_0)
| ~ epred3_1(X1)
| ~ r1(X2,esk50_0)
| ~ r1(X3,X2)
| ~ r1(X1,X3) ),
inference(spm,[status(thm)],[c_0_283,c_0_284]) ).
cnf(c_0_292,negated_conjecture,
r1(esk46_0,esk50_0),
i_0_63 ).
cnf(c_0_293,negated_conjecture,
( epred3_1(esk38_0)
| ~ epred4_1(X1)
| ~ r1(X2,esk30_0)
| ~ r1(X1,X2) ),
inference(spm,[status(thm)],[c_0_285,c_0_286]) ).
cnf(c_0_294,negated_conjecture,
r1(esk26_0,esk30_0),
i_0_93 ).
cnf(c_0_295,negated_conjecture,
( epred4_1(X1)
| ~ r1(esk18_0,X1) ),
inference(spm,[status(thm)],[c_0_287,c_0_288]) ).
cnf(c_0_296,negated_conjecture,
r1(esk18_0,esk22_0),
i_0_105 ).
cnf(c_0_297,negated_conjecture,
( epred1_1(esk70_0)
| ~ epred2_1(X1)
| ~ r1(X2,esk62_0)
| ~ r1(X1,X2) ),
inference(spm,[status(thm)],[c_0_289,c_0_290]) ).
cnf(c_0_298,negated_conjecture,
r1(esk58_0,esk62_0),
i_0_45 ).
cnf(c_0_299,negated_conjecture,
( epred2_1(esk54_0)
| ~ epred3_1(X1)
| ~ r1(X2,esk46_0)
| ~ r1(X1,X2) ),
inference(spm,[status(thm)],[c_0_291,c_0_292]) ).
cnf(c_0_300,negated_conjecture,
r1(esk42_0,esk46_0),
i_0_69 ).
cnf(c_0_301,negated_conjecture,
( epred3_1(esk38_0)
| ~ epred4_1(X1)
| ~ r1(X1,esk26_0) ),
inference(spm,[status(thm)],[c_0_293,c_0_294]) ).
cnf(c_0_302,negated_conjecture,
r1(esk22_0,esk26_0),
i_0_99 ).
cnf(c_0_303,negated_conjecture,
epred4_1(esk22_0),
inference(spm,[status(thm)],[c_0_295,c_0_296]) ).
cnf(c_0_304,negated_conjecture,
( epred1_1(esk70_0)
| ~ epred2_1(X1)
| ~ r1(X1,esk58_0) ),
inference(spm,[status(thm)],[c_0_297,c_0_298]) ).
cnf(c_0_305,negated_conjecture,
r1(esk54_0,esk58_0),
i_0_51 ).
cnf(c_0_306,negated_conjecture,
( epred2_1(esk54_0)
| ~ epred3_1(X1)
| ~ r1(X1,esk42_0) ),
inference(spm,[status(thm)],[c_0_299,c_0_300]) ).
cnf(c_0_307,negated_conjecture,
r1(esk38_0,esk42_0),
i_0_75 ).
cnf(c_0_308,negated_conjecture,
epred3_1(esk38_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_301,c_0_302]),c_0_303])]) ).
cnf(c_0_309,negated_conjecture,
( epred1_1(esk70_0)
| ~ epred2_1(esk54_0) ),
inference(spm,[status(thm)],[c_0_304,c_0_305]) ).
cnf(c_0_310,negated_conjecture,
epred2_1(esk54_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_306,c_0_307]),c_0_308])]) ).
cnf(c_0_311,plain,
( r1(X1,esk98_1(X1))
| r1(X1,esk100_1(X1))
| ~ epred1_1(X1) ),
i_0_150 ).
cnf(c_0_312,negated_conjecture,
epred1_1(esk70_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_309,c_0_310])]) ).
cnf(c_0_313,plain,
( r1(X1,esk87_2(X2,X1))
| ~ epred1_1(X2)
| ~ r1(X2,X1) ),
i_0_178 ).
cnf(c_0_314,plain,
( r1(esk70_0,esk98_1(esk70_0))
| r1(esk70_0,esk100_1(esk70_0)) ),
inference(spm,[status(thm)],[c_0_311,c_0_312]) ).
cnf(c_0_315,plain,
( p2(esk87_2(X1,X2))
| ~ epred1_1(X1)
| ~ r1(X1,X2) ),
i_0_175 ).
cnf(c_0_316,plain,
( p2(esk98_1(X1))
| r1(X1,esk100_1(X1))
| ~ epred1_1(X1) ),
i_0_144 ).
cnf(c_0_317,plain,
( r1(X1,esk98_1(X1))
| ~ p2(X2)
| ~ epred1_1(X1)
| ~ r1(esk100_1(X1),X2) ),
i_0_149 ).
cnf(c_0_318,plain,
( r1(esk100_1(esk70_0),esk87_2(esk70_0,esk100_1(esk70_0)))
| r1(esk70_0,esk98_1(esk70_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_313,c_0_314]),c_0_312])]) ).
cnf(c_0_319,plain,
( r1(esk70_0,esk98_1(esk70_0))
| p2(esk87_2(esk70_0,esk100_1(esk70_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_315,c_0_314]),c_0_312])]) ).
cnf(c_0_320,plain,
( r1(esk70_0,esk100_1(esk70_0))
| p2(esk98_1(esk70_0)) ),
inference(spm,[status(thm)],[c_0_316,c_0_312]) ).
cnf(c_0_321,plain,
( r1(X1,esk94_2(X2,X1))
| r1(X1,esk95_2(X2,X1))
| ~ epred1_1(X2)
| ~ r1(X2,X1) ),
i_0_160 ).
cnf(c_0_322,plain,
r1(esk70_0,esk98_1(esk70_0)),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_317,c_0_318]),c_0_312])]),c_0_319]) ).
cnf(c_0_323,plain,
( p2(esk98_1(X1))
| ~ p2(X2)
| ~ epred1_1(X1)
| ~ r1(esk100_1(X1),X2) ),
i_0_143 ).
cnf(c_0_324,plain,
( r1(esk100_1(esk70_0),esk87_2(esk70_0,esk100_1(esk70_0)))
| p2(esk98_1(esk70_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_313,c_0_320]),c_0_312])]) ).
cnf(c_0_325,plain,
( p2(esk87_2(esk70_0,esk100_1(esk70_0)))
| p2(esk98_1(esk70_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_315,c_0_320]),c_0_312])]) ).
cnf(c_0_326,plain,
( p2(X1)
| r1(X2,esk90_3(X3,X4,X2))
| ~ p2(X4)
| ~ epred1_1(X3)
| ~ r1(X4,X1)
| ~ r1(X4,X2)
| ~ r1(X3,X4) ),
i_0_170 ).
cnf(c_0_327,plain,
( r1(esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0)))
| r1(esk98_1(esk70_0),esk95_2(esk70_0,esk98_1(esk70_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_321,c_0_322]),c_0_312])]) ).
cnf(c_0_328,plain,
p2(esk98_1(esk70_0)),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_323,c_0_324]),c_0_312])]),c_0_325]) ).
cnf(c_0_329,negated_conjecture,
( r1(X1,esk71_1(X1))
| ~ r1(esk70_0,X1) ),
i_0_32 ).
cnf(c_0_330,negated_conjecture,
( ~ p2(esk71_1(X1))
| ~ r1(esk70_0,X1) ),
i_0_31 ).
cnf(c_0_331,plain,
( r1(esk95_2(esk70_0,esk98_1(esk70_0)),esk90_3(X1,esk98_1(esk70_0),esk95_2(esk70_0,esk98_1(esk70_0))))
| r1(esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0)))
| p2(X2)
| ~ r1(esk98_1(esk70_0),X2)
| ~ r1(X1,esk98_1(esk70_0))
| ~ epred1_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_326,c_0_327]),c_0_328])]) ).
cnf(c_0_332,negated_conjecture,
r1(esk98_1(esk70_0),esk71_1(esk98_1(esk70_0))),
inference(spm,[status(thm)],[c_0_329,c_0_322]) ).
cnf(c_0_333,negated_conjecture,
~ p2(esk71_1(esk98_1(esk70_0))),
inference(spm,[status(thm)],[c_0_330,c_0_322]) ).
cnf(c_0_334,negated_conjecture,
( r1(esk95_2(esk70_0,esk98_1(esk70_0)),esk90_3(X1,esk98_1(esk70_0),esk95_2(esk70_0,esk98_1(esk70_0))))
| r1(esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0)))
| ~ r1(X1,esk98_1(esk70_0))
| ~ epred1_1(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_331,c_0_332]),c_0_333]) ).
cnf(c_0_335,plain,
( r1(X1,esk94_2(X2,X1))
| r1(X3,esk96_3(X2,X1,X3))
| ~ epred1_1(X2)
| ~ r1(X2,X1)
| ~ r1(esk95_2(X2,X1),X3) ),
i_0_159 ).
cnf(c_0_336,plain,
( r1(esk95_2(esk70_0,esk98_1(esk70_0)),esk90_3(esk70_0,esk98_1(esk70_0),esk95_2(esk70_0,esk98_1(esk70_0))))
| r1(esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_334,c_0_322]),c_0_312])]) ).
cnf(c_0_337,plain,
( p2(esk96_3(X1,X2,X3))
| r1(X2,esk94_2(X1,X2))
| ~ epred1_1(X1)
| ~ r1(X1,X2)
| ~ r1(esk95_2(X1,X2),X3) ),
i_0_156 ).
cnf(c_0_338,plain,
( p2(X1)
| ~ p2(X2)
| ~ p2(X3)
| ~ epred1_1(X4)
| ~ r1(X3,X1)
| ~ r1(X3,X5)
| ~ r1(X4,X3)
| ~ r1(esk90_3(X4,X3,X5),X2) ),
i_0_169 ).
cnf(c_0_339,plain,
( r1(esk90_3(esk70_0,esk98_1(esk70_0),esk95_2(esk70_0,esk98_1(esk70_0))),esk96_3(esk70_0,esk98_1(esk70_0),esk90_3(esk70_0,esk98_1(esk70_0),esk95_2(esk70_0,esk98_1(esk70_0)))))
| r1(esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_335,c_0_336]),c_0_322]),c_0_312])]) ).
cnf(c_0_340,plain,
( r1(esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0)))
| p2(esk96_3(esk70_0,esk98_1(esk70_0),esk90_3(esk70_0,esk98_1(esk70_0),esk95_2(esk70_0,esk98_1(esk70_0))))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_337,c_0_336]),c_0_322]),c_0_312])]) ).
cnf(c_0_341,plain,
( r1(esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0)))
| p2(X1)
| ~ r1(esk98_1(esk70_0),X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_338,c_0_339]),c_0_322]),c_0_312]),c_0_328])]),c_0_340]),c_0_327]) ).
cnf(c_0_342,plain,
( r1(X1,esk93_1(X1))
| r1(X2,esk91_3(X1,X3,X2))
| ~ epred1_1(X1)
| ~ r1(X3,X2)
| ~ r1(X1,X3) ),
i_0_168 ).
cnf(c_0_343,negated_conjecture,
r1(esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0))),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_341,c_0_332]),c_0_333]) ).
cnf(c_0_344,plain,
( r1(X1,esk93_1(X1))
| p2(esk91_3(X1,X2,X3))
| ~ epred1_1(X1)
| ~ r1(X2,X3)
| ~ r1(X1,X2) ),
i_0_162 ).
cnf(c_0_345,plain,
( r1(esk94_2(esk70_0,esk98_1(esk70_0)),esk91_3(X1,esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0))))
| r1(X1,esk93_1(X1))
| ~ r1(X1,esk98_1(esk70_0))
| ~ epred1_1(X1) ),
inference(spm,[status(thm)],[c_0_342,c_0_343]) ).
cnf(c_0_346,plain,
( r1(X1,esk93_1(X1))
| p2(esk91_3(X1,esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0))))
| ~ r1(X1,esk98_1(esk70_0))
| ~ epred1_1(X1) ),
inference(spm,[status(thm)],[c_0_344,c_0_343]) ).
cnf(c_0_347,plain,
( r1(esk94_2(esk70_0,esk98_1(esk70_0)),esk91_3(esk70_0,esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0))))
| r1(esk70_0,esk93_1(esk70_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_345,c_0_322]),c_0_312])]) ).
cnf(c_0_348,plain,
( r1(esk70_0,esk93_1(esk70_0))
| p2(esk91_3(esk70_0,esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_346,c_0_322]),c_0_312])]) ).
cnf(c_0_349,plain,
( r1(X1,esk91_3(X2,X3,X1))
| ~ p2(X4)
| ~ epred1_1(X2)
| ~ r1(X3,X1)
| ~ r1(X2,X3)
| ~ r1(esk93_1(X2),X4) ),
i_0_167 ).
cnf(c_0_350,plain,
( r1(esk94_2(esk70_0,esk98_1(esk70_0)),esk91_3(esk70_0,esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0))))
| r1(esk93_1(esk70_0),esk87_2(esk70_0,esk93_1(esk70_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_313,c_0_347]),c_0_312])]) ).
cnf(c_0_351,plain,
( r1(esk94_2(esk70_0,esk98_1(esk70_0)),esk91_3(esk70_0,esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0))))
| p2(esk87_2(esk70_0,esk93_1(esk70_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_315,c_0_347]),c_0_312])]) ).
cnf(c_0_352,plain,
( p2(esk91_3(X1,X2,X3))
| ~ p2(X4)
| ~ epred1_1(X1)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(esk93_1(X1),X4) ),
i_0_161 ).
cnf(c_0_353,plain,
( r1(esk93_1(esk70_0),esk87_2(esk70_0,esk93_1(esk70_0)))
| p2(esk91_3(esk70_0,esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_313,c_0_348]),c_0_312])]) ).
cnf(c_0_354,plain,
( p2(esk91_3(esk70_0,esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0))))
| p2(esk87_2(esk70_0,esk93_1(esk70_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_315,c_0_348]),c_0_312])]) ).
cnf(c_0_355,plain,
( r1(esk94_2(esk70_0,esk98_1(esk70_0)),esk91_3(esk70_0,esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0))))
| r1(X1,esk91_3(esk70_0,X2,X1))
| ~ r1(esk70_0,X2)
| ~ r1(X2,X1) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_349,c_0_350]),c_0_312])]),c_0_351]) ).
cnf(c_0_356,plain,
( p2(esk91_3(esk70_0,esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0))))
| p2(esk91_3(esk70_0,X1,X2))
| ~ r1(esk70_0,X1)
| ~ r1(X1,X2) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_352,c_0_353]),c_0_312])]),c_0_354]) ).
cnf(c_0_357,plain,
( r1(esk94_2(esk70_0,esk98_1(esk70_0)),esk91_3(esk70_0,esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0))))
| r1(X1,esk91_3(esk70_0,esk98_1(esk70_0),X1))
| ~ r1(esk98_1(esk70_0),X1) ),
inference(spm,[status(thm)],[c_0_355,c_0_322]) ).
cnf(c_0_358,plain,
( p2(esk91_3(esk70_0,esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0))))
| p2(esk91_3(esk70_0,esk98_1(esk70_0),X1))
| ~ r1(esk98_1(esk70_0),X1) ),
inference(spm,[status(thm)],[c_0_356,c_0_322]) ).
cnf(c_0_359,plain,
( r1(X1,esk95_2(X2,X1))
| ~ p2(X3)
| ~ epred1_1(X2)
| ~ r1(X2,X1)
| ~ r1(esk94_2(X2,X1),X3) ),
i_0_155 ).
cnf(c_0_360,negated_conjecture,
r1(esk94_2(esk70_0,esk98_1(esk70_0)),esk91_3(esk70_0,esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0)))),
inference(spm,[status(thm)],[c_0_357,c_0_343]) ).
cnf(c_0_361,negated_conjecture,
p2(esk91_3(esk70_0,esk98_1(esk70_0),esk94_2(esk70_0,esk98_1(esk70_0)))),
inference(spm,[status(thm)],[c_0_358,c_0_343]) ).
cnf(c_0_362,plain,
r1(esk98_1(esk70_0),esk95_2(esk70_0,esk98_1(esk70_0))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_359,c_0_360]),c_0_322]),c_0_312]),c_0_361])]) ).
cnf(c_0_363,plain,
( r1(esk95_2(esk70_0,esk98_1(esk70_0)),esk90_3(X1,esk98_1(esk70_0),esk95_2(esk70_0,esk98_1(esk70_0))))
| p2(X2)
| ~ r1(esk98_1(esk70_0),X2)
| ~ r1(X1,esk98_1(esk70_0))
| ~ epred1_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_326,c_0_362]),c_0_328])]) ).
cnf(c_0_364,plain,
( r1(X1,esk96_3(X2,X3,X1))
| ~ p2(X4)
| ~ epred1_1(X2)
| ~ r1(X2,X3)
| ~ r1(esk94_2(X2,X3),X4)
| ~ r1(esk95_2(X2,X3),X1) ),
i_0_154 ).
cnf(c_0_365,negated_conjecture,
( r1(esk95_2(esk70_0,esk98_1(esk70_0)),esk90_3(X1,esk98_1(esk70_0),esk95_2(esk70_0,esk98_1(esk70_0))))
| ~ r1(X1,esk98_1(esk70_0))
| ~ epred1_1(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_363,c_0_332]),c_0_333]) ).
cnf(c_0_366,plain,
( p2(esk96_3(X1,X2,X3))
| ~ p2(X4)
| ~ epred1_1(X1)
| ~ r1(X1,X2)
| ~ r1(esk94_2(X1,X2),X4)
| ~ r1(esk95_2(X1,X2),X3) ),
i_0_151 ).
cnf(c_0_367,plain,
( r1(X1,esk96_3(esk70_0,esk98_1(esk70_0),X1))
| ~ r1(esk95_2(esk70_0,esk98_1(esk70_0)),X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_364,c_0_360]),c_0_322]),c_0_312]),c_0_361])]) ).
cnf(c_0_368,plain,
r1(esk95_2(esk70_0,esk98_1(esk70_0)),esk90_3(esk70_0,esk98_1(esk70_0),esk95_2(esk70_0,esk98_1(esk70_0)))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_365,c_0_322]),c_0_312])]) ).
cnf(c_0_369,plain,
( p2(esk96_3(esk70_0,esk98_1(esk70_0),X1))
| ~ r1(esk95_2(esk70_0,esk98_1(esk70_0)),X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_366,c_0_360]),c_0_322]),c_0_312]),c_0_361])]) ).
cnf(c_0_370,plain,
r1(esk90_3(esk70_0,esk98_1(esk70_0),esk95_2(esk70_0,esk98_1(esk70_0))),esk96_3(esk70_0,esk98_1(esk70_0),esk90_3(esk70_0,esk98_1(esk70_0),esk95_2(esk70_0,esk98_1(esk70_0))))),
inference(spm,[status(thm)],[c_0_367,c_0_368]) ).
cnf(c_0_371,plain,
p2(esk96_3(esk70_0,esk98_1(esk70_0),esk90_3(esk70_0,esk98_1(esk70_0),esk95_2(esk70_0,esk98_1(esk70_0))))),
inference(spm,[status(thm)],[c_0_369,c_0_368]) ).
cnf(c_0_372,plain,
( p2(X1)
| ~ r1(esk98_1(esk70_0),X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_338,c_0_370]),c_0_322]),c_0_362]),c_0_312]),c_0_328]),c_0_371])]) ).
cnf(c_0_373,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_372,c_0_332]),c_0_333]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL652+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : enigmatic-eprover.py %s %d 1
% 0.09/0.36 % Computer : n027.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 5 00:05:14 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.22/0.46 # ENIGMATIC: Selected complete mode:
% 35.50/7.14 # ENIGMATIC: Solved by autoschedule-lgb:
% 35.50/7.14 # No SInE strategy applied
% 35.50/7.14 # Trying AutoSched0 for 150 seconds
% 35.50/7.14 # AutoSched0-Mode selected heuristic U_____043_B31_F1_PI_AE_CS_SP_S2S
% 35.50/7.14 # and selection function SelectNewComplexAHP.
% 35.50/7.14 #
% 35.50/7.14 # Preprocessing time : 0.029 s
% 35.50/7.14
% 35.50/7.14 # Proof found!
% 35.50/7.14 # SZS status Theorem
% 35.50/7.14 # SZS output start CNFRefutation
% See solution above
% 35.50/7.15 # Training examples: 0 positive, 0 negative
% 35.50/7.15
% 35.50/7.15 # -------------------------------------------------
% 35.50/7.15 # User time : 2.865 s
% 35.50/7.15 # System time : 0.032 s
% 35.50/7.15 # Total time : 2.898 s
% 35.50/7.15 # Maximum resident set size: 3328 pages
% 35.50/7.15
%------------------------------------------------------------------------------