%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : ALG105+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n026.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 : Thu Jul 14 14:57:48 EDT 2022
% Result : Theorem 9.69s 3.07s
% Output : CNFRefutation 9.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 61
% Syntax : Number of clauses : 177 ( 128 unt; 43 nHn; 177 RR)
% Number of literals : 332 ( 316 equ; 105 neg)
% Maximal clause size : 20 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_262,plain,
op1(op1(e12,e11),op1(e12,e11)) = e10,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_262) ).
cnf(i_0_261,plain,
op1(e12,e11) = e13,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_261) ).
cnf(i_0_231,plain,
op1(op1(e12,e11),e12) = e11,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_231) ).
cnf(i_0_225,plain,
op1(op1(e13,e13),e13) = e13,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_225) ).
cnf(i_0_226,plain,
op1(op1(e13,e12),e13) = e12,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_226) ).
cnf(i_0_264,plain,
op2(op2(e22,e21),op2(e22,e21)) = e20,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_264) ).
cnf(i_0_263,plain,
op2(e22,e21) = e23,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_263) ).
cnf(i_0_21,plain,
( op1(e10,e13) = e11
| op1(e11,e13) = e11
| op1(e12,e13) = e11
| op1(e13,e13) = e11 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_21) ).
cnf(i_0_198,plain,
e10 != e11,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_198) ).
cnf(i_0_194,plain,
e13 != e11,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_194) ).
cnf(i_0_195,plain,
e11 != e12,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_195) ).
cnf(i_0_245,plain,
op2(op2(e23,e23),e23) = e23,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_245) ).
cnf(i_0_229,plain,
op1(op1(e12,e13),e12) = e13,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_229) ).
cnf(i_0_251,plain,
op2(op2(e22,e21),e22) = e21,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_251) ).
cnf(i_0_153,plain,
op2(e22,e22) != op2(e22,e21),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_153) ).
cnf(i_0_163,plain,
op2(e20,e23) != op2(e20,e22),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_163) ).
cnf(i_0_234,plain,
op1(op1(e11,e12),e11) = e12,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_234) ).
cnf(i_0_73,plain,
( op2(e20,e22) = e23
| op2(e21,e22) = e23
| op2(e22,e22) = e23
| op2(e23,e22) = e23 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_73) ).
cnf(i_0_200,plain,
e23 != e21,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_200) ).
cnf(i_0_223,plain,
( op1(e13,op1(e11,e13)) = op1(e11,e13)
| epred1_0 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_223) ).
cnf(i_0_136,plain,
op1(e10,e11) != op1(e13,e11),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_136) ).
cnf(i_0_130,plain,
op1(e10,e12) != op1(e13,e12),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_130) ).
cnf(i_0_246,plain,
op2(op2(e23,e22),e23) = e22,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_246) ).
cnf(i_0_254,plain,
op2(op2(e21,e22),e21) = e22,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_254) ).
cnf(i_0_409,plain,
( op1(e10,op1(e10,e10)) = op1(e10,e10)
| op1(e11,op1(e13,e11)) = op1(e13,e11)
| op1(e12,op1(e13,e12)) = op1(e13,e12)
| ~ epred1_0 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_409) ).
cnf(i_0_193,plain,
e13 != e12,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_193) ).
cnf(i_0_44,plain,
( op1(e10,e10) = e12
| op1(e10,e11) = e12
| op1(e10,e12) = e12
| op1(e10,e13) = e12 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_44) ).
cnf(i_0_46,plain,
( op1(e10,e10) = e11
| op1(e10,e11) = e11
| op1(e10,e12) = e11
| op1(e10,e13) = e11 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_46) ).
cnf(i_0_243,plain,
( op2(e23,op2(e21,e23)) = op2(e21,e23)
| epred2_0 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_243) ).
cnf(i_0_201,plain,
e22 != e21,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_201) ).
cnf(i_0_184,plain,
op2(e23,e21) != op2(e20,e21),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_184) ).
cnf(i_0_237,plain,
op1(op1(e10,e13),e10) = e13,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_237) ).
cnf(i_0_477,plain,
( op2(e20,op2(e20,e20)) = op2(e20,e20)
| op2(e21,op2(e22,e21)) = op2(e22,e21)
| op2(e22,op2(e23,e22)) = op2(e23,e22)
| ~ epred2_0 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_477) ).
cnf(i_0_199,plain,
e23 != e22,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_199) ).
cnf(i_0_92,plain,
( op2(e20,e20) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_92) ).
cnf(i_0_178,plain,
op2(e23,e22) != op2(e20,e22),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_178) ).
cnf(i_0_247,plain,
op2(op2(e23,e21),e23) = e21,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_247) ).
cnf(i_0_315,negated_conjecture,
( h12(e11) != e23
| ~ epred14_0 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_315) ).
cnf(i_0_312,plain,
h12(e11) = e23,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_312) ).
cnf(i_0_47,plain,
( op1(e10,e10) = e10
| op1(e11,e10) = e10
| op1(e12,e10) = e10
| op1(e13,e10) = e10 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_47) ).
cnf(i_0_196,plain,
e10 != e13,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_196) ).
cnf(i_0_238,plain,
op1(op1(e10,e12),e10) = e12,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_238) ).
cnf(i_0_239,plain,
op1(op1(e10,e11),e10) = e11,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_239) ).
cnf(i_0_31,plain,
( op1(e10,e12) = e10
| op1(e11,e12) = e10
| op1(e12,e12) = e10
| op1(e13,e12) = e10 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_31) ).
cnf(i_0_79,plain,
( op2(e20,e22) = e20
| op2(e21,e22) = e20
| op2(e22,e22) = e20
| op2(e23,e22) = e20 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_79) ).
cnf(i_0_204,plain,
e21 != e20,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_204) ).
cnf(i_0_202,plain,
e23 != e20,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_202) ).
cnf(i_0_39,plain,
( op1(e10,e11) = e10
| op1(e11,e11) = e10
| op1(e12,e11) = e10
| op1(e13,e11) = e10 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_39) ).
cnf(i_0_197,plain,
e10 != e12,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_197) ).
cnf(i_0_94,plain,
( op2(e20,e20) = e21
| op2(e20,e21) = e21
| op2(e20,e22) = e21
| op2(e20,e23) = e21 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_94) ).
cnf(i_0_96,plain,
( op2(e20,e20) = e20
| op2(e20,e21) = e20
| op2(e20,e22) = e20
| op2(e20,e23) = e20 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_96) ).
cnf(i_0_1242,plain,
( epred14_0
| h12(e10) != e20
| h12(e12) != e22
| h12(e13) != e21
| h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),h12(e11))
| h12(op1(e10,e12)) != op2(h12(e10),h12(e12))
| h12(op1(e10,e13)) != op2(h12(e10),h12(e13))
| h12(op1(e11,e10)) != op2(h12(e11),h12(e10))
| h12(op1(e11,e11)) != op2(h12(e11),h12(e11))
| h12(op1(e11,e12)) != op2(h12(e11),h12(e12))
| h12(op1(e11,e13)) != op2(h12(e11),h12(e13))
| h12(op1(e12,e10)) != op2(h12(e12),h12(e10))
| h12(op1(e12,e11)) != op2(h12(e12),h12(e11))
| h12(op1(e12,e12)) != op2(h12(e12),h12(e12))
| h12(op1(e12,e13)) != op2(h12(e12),h12(e13))
| h12(op1(e13,e10)) != op2(h12(e13),h12(e10))
| h12(op1(e13,e11)) != op2(h12(e13),h12(e11))
| h12(op1(e13,e12)) != op2(h12(e13),h12(e12))
| h12(op1(e13,e13)) != op2(h12(e13),h12(e13)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_1242) ).
cnf(i_0_309,plain,
op2(e22,e23) = h12(e13),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_309) ).
cnf(i_0_310,plain,
op2(op2(e22,e23),op2(e22,e23)) = h12(e10),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_310) ).
cnf(i_0_311,plain,
h12(e12) = e22,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_311) ).
cnf(i_0_255,plain,
op2(op2(e21,e21),e21) = e21,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_255) ).
cnf(i_0_203,plain,
e22 != e20,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_203) ).
cnf(i_0_87,plain,
( op2(e20,e21) = e20
| op2(e21,e21) = e20
| op2(e22,e21) = e20
| op2(e23,e21) = e20 ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_87) ).
cnf(i_0_257,plain,
op2(op2(e20,e23),e20) = e23,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_257) ).
cnf(i_0_258,plain,
op2(op2(e20,e22),e20) = e22,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_258) ).
cnf(i_0_259,plain,
op2(op2(e20,e21),e20) = e21,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-6n45qha7/lgb.p',i_0_259) ).
cnf(c_0_1304,plain,
op1(op1(e12,e11),op1(e12,e11)) = e10,
i_0_262 ).
cnf(c_0_1305,plain,
op1(e12,e11) = e13,
i_0_261 ).
cnf(c_0_1306,plain,
op1(op1(e12,e11),e12) = e11,
i_0_231 ).
cnf(c_0_1307,plain,
op1(op1(e13,e13),e13) = e13,
i_0_225 ).
cnf(c_0_1308,plain,
op1(e13,e13) = e10,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1304,c_0_1305]),c_0_1305]) ).
cnf(c_0_1309,plain,
op1(op1(e13,e12),e13) = e12,
i_0_226 ).
cnf(c_0_1310,plain,
op1(e13,e12) = e11,
inference(rw,[status(thm)],[c_0_1306,c_0_1305]) ).
cnf(c_0_1311,plain,
op2(op2(e22,e21),op2(e22,e21)) = e20,
i_0_264 ).
cnf(c_0_1312,plain,
op2(e22,e21) = e23,
i_0_263 ).
cnf(c_0_1313,plain,
( op1(e10,e13) = e11
| op1(e11,e13) = e11
| op1(e12,e13) = e11
| op1(e13,e13) = e11 ),
i_0_21 ).
cnf(c_0_1314,plain,
op1(e10,e13) = e13,
inference(rw,[status(thm)],[c_0_1307,c_0_1308]) ).
cnf(c_0_1315,plain,
op1(e11,e13) = e12,
inference(rw,[status(thm)],[c_0_1309,c_0_1310]) ).
cnf(c_0_1316,plain,
e10 != e11,
i_0_198 ).
cnf(c_0_1317,plain,
e13 != e11,
i_0_194 ).
cnf(c_0_1318,plain,
e11 != e12,
i_0_195 ).
cnf(c_0_1319,plain,
op2(op2(e23,e23),e23) = e23,
i_0_245 ).
cnf(c_0_1320,plain,
op2(e23,e23) = e20,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1311,c_0_1312]),c_0_1312]) ).
cnf(c_0_1321,plain,
op1(op1(e12,e13),e12) = e13,
i_0_229 ).
cnf(c_0_1322,plain,
op1(e12,e13) = e11,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1313,c_0_1308]),c_0_1314]),c_0_1315]),c_0_1316]),c_0_1317]),c_0_1318]) ).
cnf(c_0_1323,plain,
op2(op2(e22,e21),e22) = e21,
i_0_251 ).
cnf(c_0_1324,plain,
op2(e22,e22) != op2(e22,e21),
i_0_153 ).
cnf(c_0_1325,plain,
op2(e20,e23) != op2(e20,e22),
i_0_163 ).
cnf(c_0_1326,plain,
op2(e20,e23) = e23,
inference(rw,[status(thm)],[c_0_1319,c_0_1320]) ).
cnf(c_0_1327,plain,
op1(op1(e11,e12),e11) = e12,
i_0_234 ).
cnf(c_0_1328,plain,
op1(e11,e12) = e13,
inference(rw,[status(thm)],[c_0_1321,c_0_1322]) ).
cnf(c_0_1329,plain,
( op2(e20,e22) = e23
| op2(e21,e22) = e23
| op2(e22,e22) = e23
| op2(e23,e22) = e23 ),
i_0_73 ).
cnf(c_0_1330,plain,
op2(e23,e22) = e21,
inference(rw,[status(thm)],[c_0_1323,c_0_1312]) ).
cnf(c_0_1331,plain,
op2(e22,e22) != e23,
inference(rw,[status(thm)],[c_0_1324,c_0_1312]) ).
cnf(c_0_1332,plain,
e23 != e21,
i_0_200 ).
cnf(c_0_1333,plain,
op2(e20,e22) != e23,
inference(rw,[status(thm)],[c_0_1325,c_0_1326]) ).
cnf(c_0_1334,plain,
( op1(e13,op1(e11,e13)) = op1(e11,e13)
| epred1_0 ),
i_0_223 ).
cnf(c_0_1335,plain,
op1(e10,e11) != op1(e13,e11),
i_0_136 ).
cnf(c_0_1336,plain,
op1(e13,e11) = e12,
inference(rw,[status(thm)],[c_0_1327,c_0_1328]) ).
cnf(c_0_1337,plain,
op1(e10,e12) != op1(e13,e12),
i_0_130 ).
cnf(c_0_1338,plain,
op2(op2(e23,e22),e23) = e22,
i_0_246 ).
cnf(c_0_1339,plain,
op2(op2(e21,e22),e21) = e22,
i_0_254 ).
cnf(c_0_1340,plain,
op2(e21,e22) = e23,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1329,c_0_1330]),c_0_1331]),c_0_1332]),c_0_1333]) ).
cnf(c_0_1341,plain,
( op1(e10,op1(e10,e10)) = op1(e10,e10)
| op1(e11,op1(e13,e11)) = op1(e13,e11)
| op1(e12,op1(e13,e12)) = op1(e13,e12)
| ~ epred1_0 ),
i_0_409 ).
cnf(c_0_1342,plain,
epred1_0,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1334,c_0_1315]),c_0_1310]),c_0_1315]),c_0_1318]) ).
cnf(c_0_1343,plain,
e13 != e12,
i_0_193 ).
cnf(c_0_1344,plain,
( op1(e10,e10) = e12
| op1(e10,e11) = e12
| op1(e10,e12) = e12
| op1(e10,e13) = e12 ),
i_0_44 ).
cnf(c_0_1345,plain,
op1(e10,e11) != e12,
inference(rw,[status(thm)],[c_0_1335,c_0_1336]) ).
cnf(c_0_1346,plain,
( op1(e10,e10) = e11
| op1(e10,e11) = e11
| op1(e10,e12) = e11
| op1(e10,e13) = e11 ),
i_0_46 ).
cnf(c_0_1347,plain,
op1(e10,e12) != e11,
inference(rw,[status(thm)],[c_0_1337,c_0_1310]) ).
cnf(c_0_1348,plain,
( op2(e23,op2(e21,e23)) = op2(e21,e23)
| epred2_0 ),
i_0_243 ).
cnf(c_0_1349,plain,
op2(e21,e23) = e22,
inference(rw,[status(thm)],[c_0_1338,c_0_1330]) ).
cnf(c_0_1350,plain,
e22 != e21,
i_0_201 ).
cnf(c_0_1351,plain,
op2(e23,e21) != op2(e20,e21),
i_0_184 ).
cnf(c_0_1352,plain,
op2(e23,e21) = e22,
inference(rw,[status(thm)],[c_0_1339,c_0_1340]) ).
cnf(c_0_1353,plain,
op1(op1(e10,e13),e10) = e13,
i_0_237 ).
cnf(c_0_1354,plain,
op1(e10,op1(e10,e10)) = op1(e10,e10),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[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(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1341,c_0_1336]),c_0_1328]),c_0_1336]),c_0_1310]),c_0_1305]),c_0_1310]),c_0_1342])]),c_0_1343]),c_0_1317]) ).
cnf(c_0_1355,plain,
( op1(e10,e12) = e12
| op1(e10,e10) = e12 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1344,c_0_1314]),c_0_1343]),c_0_1345]) ).
cnf(c_0_1356,plain,
( op1(e10,e11) = e11
| op1(e10,e10) = e11 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1346,c_0_1314]),c_0_1317]),c_0_1347]) ).
cnf(c_0_1357,plain,
( op2(e20,op2(e20,e20)) = op2(e20,e20)
| op2(e21,op2(e22,e21)) = op2(e22,e21)
| op2(e22,op2(e23,e22)) = op2(e23,e22)
| ~ epred2_0 ),
i_0_477 ).
cnf(c_0_1358,plain,
epred2_0,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1348,c_0_1349]),c_0_1330]),c_0_1349]),c_0_1350]) ).
cnf(c_0_1359,plain,
e23 != e22,
i_0_199 ).
cnf(c_0_1360,plain,
( op2(e20,e20) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 ),
i_0_92 ).
cnf(c_0_1361,plain,
op2(e20,e21) != e22,
inference(rw,[status(thm)],[c_0_1351,c_0_1352]) ).
cnf(c_0_1362,plain,
op2(e23,e22) != op2(e20,e22),
i_0_178 ).
cnf(c_0_1363,plain,
op2(op2(e23,e21),e23) = e21,
i_0_247 ).
cnf(c_0_1364,negated_conjecture,
( h12(e11) != e23
| ~ epred14_0 ),
i_0_315 ).
cnf(c_0_1365,plain,
h12(e11) = e23,
i_0_312 ).
cnf(c_0_1366,plain,
( op1(e10,e10) = e10
| op1(e11,e10) = e10
| op1(e12,e10) = e10
| op1(e13,e10) = e10 ),
i_0_47 ).
cnf(c_0_1367,plain,
op1(e13,e10) = e13,
inference(rw,[status(thm)],[c_0_1353,c_0_1314]) ).
cnf(c_0_1368,plain,
e10 != e13,
i_0_196 ).
cnf(c_0_1369,plain,
op1(op1(e10,e12),e10) = e12,
i_0_238 ).
cnf(c_0_1370,plain,
op1(e10,e12) = e12,
inference(spm,[status(thm)],[c_0_1354,c_0_1355]) ).
cnf(c_0_1371,plain,
op1(op1(e10,e11),e10) = e11,
i_0_239 ).
cnf(c_0_1372,plain,
op1(e10,e11) = e11,
inference(spm,[status(thm)],[c_0_1354,c_0_1356]) ).
cnf(c_0_1373,plain,
( op1(e10,e12) = e10
| op1(e11,e12) = e10
| op1(e12,e12) = e10
| op1(e13,e12) = e10 ),
i_0_31 ).
cnf(c_0_1374,plain,
( op2(e20,e22) = e20
| op2(e21,e22) = e20
| op2(e22,e22) = e20
| op2(e23,e22) = e20 ),
i_0_79 ).
cnf(c_0_1375,plain,
e21 != e20,
i_0_204 ).
cnf(c_0_1376,plain,
e23 != e20,
i_0_202 ).
cnf(c_0_1377,plain,
op2(e20,op2(e20,e20)) = op2(e20,e20),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[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(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1357,c_0_1330]),c_0_1312]),c_0_1330]),c_0_1312]),c_0_1349]),c_0_1312]),c_0_1358])]),c_0_1332]),c_0_1359]) ).
cnf(c_0_1378,plain,
( op2(e20,e20) = e22
| op2(e20,e22) = e22 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1360,c_0_1326]),c_0_1359]),c_0_1361]) ).
cnf(c_0_1379,plain,
( op1(e10,e11) = e10
| op1(e11,e11) = e10
| op1(e12,e11) = e10
| op1(e13,e11) = e10 ),
i_0_39 ).
cnf(c_0_1380,plain,
e10 != e12,
i_0_197 ).
cnf(c_0_1381,plain,
( op2(e20,e20) = e21
| op2(e20,e21) = e21
| op2(e20,e22) = e21
| op2(e20,e23) = e21 ),
i_0_94 ).
cnf(c_0_1382,plain,
op2(e20,e22) != e21,
inference(rw,[status(thm)],[c_0_1362,c_0_1330]) ).
cnf(c_0_1383,plain,
( op2(e20,e20) = e20
| op2(e20,e21) = e20
| op2(e20,e22) = e20
| op2(e20,e23) = e20 ),
i_0_96 ).
cnf(c_0_1384,plain,
( epred14_0
| h12(e10) != e20
| h12(e12) != e22
| h12(e13) != e21
| h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),h12(e11))
| h12(op1(e10,e12)) != op2(h12(e10),h12(e12))
| h12(op1(e10,e13)) != op2(h12(e10),h12(e13))
| h12(op1(e11,e10)) != op2(h12(e11),h12(e10))
| h12(op1(e11,e11)) != op2(h12(e11),h12(e11))
| h12(op1(e11,e12)) != op2(h12(e11),h12(e12))
| h12(op1(e11,e13)) != op2(h12(e11),h12(e13))
| h12(op1(e12,e10)) != op2(h12(e12),h12(e10))
| h12(op1(e12,e11)) != op2(h12(e12),h12(e11))
| h12(op1(e12,e12)) != op2(h12(e12),h12(e12))
| h12(op1(e12,e13)) != op2(h12(e12),h12(e13))
| h12(op1(e13,e10)) != op2(h12(e13),h12(e10))
| h12(op1(e13,e11)) != op2(h12(e13),h12(e11))
| h12(op1(e13,e12)) != op2(h12(e13),h12(e12))
| h12(op1(e13,e13)) != op2(h12(e13),h12(e13)) ),
i_0_1242 ).
cnf(c_0_1385,plain,
op2(e22,e23) = h12(e13),
i_0_309 ).
cnf(c_0_1386,plain,
op2(e22,e23) = e21,
inference(rw,[status(thm)],[c_0_1363,c_0_1352]) ).
cnf(c_0_1387,plain,
op2(op2(e22,e23),op2(e22,e23)) = h12(e10),
i_0_310 ).
cnf(c_0_1388,plain,
h12(e12) = e22,
i_0_311 ).
cnf(c_0_1389,plain,
op2(op2(e21,e21),e21) = e21,
i_0_255 ).
cnf(c_0_1390,negated_conjecture,
~ epred14_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1364,c_0_1365])]) ).
cnf(c_0_1391,plain,
( op1(e12,e10) = e10
| op1(e11,e10) = e10
| op1(e10,e10) = e10 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1366,c_0_1367]),c_0_1368]) ).
cnf(c_0_1392,plain,
op1(e12,e10) = e12,
inference(rw,[status(thm)],[c_0_1369,c_0_1370]) ).
cnf(c_0_1393,plain,
op1(e11,e10) = e11,
inference(rw,[status(thm)],[c_0_1371,c_0_1372]) ).
cnf(c_0_1394,plain,
( op1(e12,e12) = e10
| op1(e10,e12) = e10 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1373,c_0_1310]),c_0_1328]),c_0_1316]),c_0_1368]) ).
cnf(c_0_1395,plain,
( op2(e20,e22) = e20
| op2(e22,e22) = e20 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1374,c_0_1330]),c_0_1340]),c_0_1375]),c_0_1376]) ).
cnf(c_0_1396,plain,
op2(e20,e22) = e22,
inference(spm,[status(thm)],[c_0_1377,c_0_1378]) ).
cnf(c_0_1397,plain,
e22 != e20,
i_0_203 ).
cnf(c_0_1398,plain,
( op1(e11,e11) = e10
| op1(e10,e11) = e10 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1379,c_0_1336]),c_0_1305]),c_0_1380]),c_0_1368]) ).
cnf(c_0_1399,plain,
( op2(e20,e21) = e20
| op2(e21,e21) = e20
| op2(e22,e21) = e20
| op2(e23,e21) = e20 ),
i_0_87 ).
cnf(c_0_1400,plain,
( op2(e20,e20) = e21
| op2(e20,e21) = e21 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1381,c_0_1326]),c_0_1382]),c_0_1332]) ).
cnf(c_0_1401,plain,
( op2(e20,e20) = e20
| op2(e20,e21) = e20
| op2(e20,e22) = e20 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1383,c_0_1326]),c_0_1376]) ).
cnf(c_0_1402,plain,
( h12(op1(e10,e10)) != op2(op2(e21,e21),op2(e21,e21))
| h12(op1(e10,e11)) != op2(op2(e21,e21),e23)
| h12(op1(e10,e12)) != op2(op2(e21,e21),e22)
| h12(op1(e11,e10)) != op2(e23,op2(e21,e21))
| h12(op1(e12,e10)) != op2(e22,op2(e21,e21))
| h12(op1(e12,e12)) != op2(e22,e22)
| op2(e21,op2(e21,e21)) != e21
| h12(op1(e11,e11)) != e20
| op2(e21,e21) != e20 ),
inference(sr,[status(thm)],[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(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1384,c_0_1385]),c_0_1386]),c_0_1387]),c_0_1386]),c_0_1386]),c_0_1388]),c_0_1385]),c_0_1386]),c_0_1385]),c_0_1386]),c_0_1308]),c_0_1387]),c_0_1386]),c_0_1386]),c_0_1385]),c_0_1386]),c_0_1387]),c_0_1386]),c_0_1386]),c_0_1367]),c_0_1385]),c_0_1386]),c_0_1385]),c_0_1386]),c_0_1365]),c_0_1349]),c_0_1336]),c_0_1388]),c_0_1385]),c_0_1386]),c_0_1388]),c_0_1340]),c_0_1310]),c_0_1365]),c_0_1387]),c_0_1386]),c_0_1386]),c_0_1385]),c_0_1386]),c_0_1389]),c_0_1314]),c_0_1385]),c_0_1386]),c_0_1387]),c_0_1386]),c_0_1386]),c_0_1387]),c_0_1386]),c_0_1386]),c_0_1387]),c_0_1386]),c_0_1386]),c_0_1365]),c_0_1387]),c_0_1386]),c_0_1386]),c_0_1388]),c_0_1365]),c_0_1385]),c_0_1386]),c_0_1352]),c_0_1315]),c_0_1388]),c_0_1365]),c_0_1387]),c_0_1386]),c_0_1386]),c_0_1365]),c_0_1365]),c_0_1320]),c_0_1365]),c_0_1388]),c_0_1330]),c_0_1328]),c_0_1385]),c_0_1386]),c_0_1388]),c_0_1385]),c_0_1386]),c_0_1312]),c_0_1322]),c_0_1365]),c_0_1388]),c_0_1387]),c_0_1386]),c_0_1386]),c_0_1388]),c_0_1365]),c_0_1386]),c_0_1305]),c_0_1385]),c_0_1386]),c_0_1388]),c_0_1388])]),c_0_1390]) ).
cnf(c_0_1403,plain,
op1(e10,e10) = e10,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1391,c_0_1392]),c_0_1393]),c_0_1380]),c_0_1316]) ).
cnf(c_0_1404,plain,
op1(e12,e12) = e10,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1394,c_0_1370]),c_0_1380]) ).
cnf(c_0_1405,plain,
op2(e22,e22) = e20,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1395,c_0_1396]),c_0_1397]) ).
cnf(c_0_1406,plain,
op1(e11,e11) = e10,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1398,c_0_1372]),c_0_1316]) ).
cnf(c_0_1407,plain,
( op2(e20,e21) = e20
| op2(e21,e21) = e20 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1399,c_0_1312]),c_0_1352]),c_0_1376]),c_0_1397]) ).
cnf(c_0_1408,plain,
op2(e20,e21) = e21,
inference(spm,[status(thm)],[c_0_1377,c_0_1400]) ).
cnf(c_0_1409,plain,
( op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1401,c_0_1396]),c_0_1397]) ).
cnf(c_0_1410,plain,
op2(op2(e20,e23),e20) = e23,
i_0_257 ).
cnf(c_0_1411,plain,
op2(op2(e20,e22),e20) = e22,
i_0_258 ).
cnf(c_0_1412,plain,
op2(op2(e20,e21),e20) = e21,
i_0_259 ).
cnf(c_0_1413,plain,
( op2(op2(e21,e21),op2(e21,e21)) != op2(e21,e21)
| op2(op2(e21,e21),e23) != e23
| op2(op2(e21,e21),e22) != e22
| op2(e23,op2(e21,e21)) != e23
| op2(e22,op2(e21,e21)) != e22
| op2(e21,op2(e21,e21)) != e21
| op2(e21,e21) != e20 ),
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(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1402,c_0_1403]),c_0_1387]),c_0_1386]),c_0_1386]),c_0_1372]),c_0_1365]),c_0_1370]),c_0_1388]),c_0_1393]),c_0_1365]),c_0_1392]),c_0_1388]),c_0_1404]),c_0_1387]),c_0_1386]),c_0_1386]),c_0_1405]),c_0_1406]),c_0_1387]),c_0_1386]),c_0_1386])]) ).
cnf(c_0_1414,plain,
op2(e21,e21) = e20,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1407,c_0_1408]),c_0_1375]) ).
cnf(c_0_1415,plain,
op2(e20,e20) = e20,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1409,c_0_1408]),c_0_1375]) ).
cnf(c_0_1416,plain,
op2(e23,e20) = e23,
inference(rw,[status(thm)],[c_0_1410,c_0_1326]) ).
cnf(c_0_1417,plain,
op2(e22,e20) = e22,
inference(rw,[status(thm)],[c_0_1411,c_0_1396]) ).
cnf(c_0_1418,plain,
op2(e21,e20) = e21,
inference(rw,[status(thm)],[c_0_1412,c_0_1408]) ).
cnf(c_0_1419,plain,
$false,
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(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1413,c_0_1414]),c_0_1414]),c_0_1415]),c_0_1414]),c_0_1414]),c_0_1326]),c_0_1414]),c_0_1396]),c_0_1414]),c_0_1416]),c_0_1414]),c_0_1417]),c_0_1414]),c_0_1418]),c_0_1414])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : ALG105+1 : TPTP v8.1.0. Released v2.7.0.
% 0.06/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.11/0.33 % Computer : n026.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Thu Jun 9 06:45:49 EDT 2022
% 0.11/0.33 % CPUTime :
% 0.18/0.44 # ENIGMATIC: Selected complete mode:
% 9.69/3.07 # ENIGMATIC: Solved by autoschedule-lgb:
% 9.69/3.07 # No SInE strategy applied
% 9.69/3.07 # Trying AutoSched0 for 150 seconds
% 9.69/3.07 # AutoSched0-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S003I
% 9.69/3.07 # and selection function PSelectNegativeLiterals.
% 9.69/3.07 #
% 9.69/3.07 # Preprocessing time : 0.070 s
% 9.69/3.07 # Presaturation interreduction done
% 9.69/3.07
% 9.69/3.07 # Proof found!
% 9.69/3.07 # SZS status Theorem
% 9.69/3.07 # SZS output start CNFRefutation
% See solution above
% 9.69/3.07 # Training examples: 0 positive, 0 negative
% 9.69/3.07
% 9.69/3.07 # -------------------------------------------------
% 9.69/3.07 # User time : 0.131 s
% 9.69/3.07 # System time : 0.008 s
% 9.69/3.07 # Total time : 0.139 s
% 9.69/3.07 # Maximum resident set size: 7120 pages
% 9.69/3.07
%------------------------------------------------------------------------------