%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : ALG118+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n023.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 15:00:21 EDT 2022
% Result : Theorem 13.82s 3.60s
% Output : CNFRefutation 13.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 139
% Syntax : Number of clauses : 564 ( 282 unt; 203 nHn; 564 RR)
% Number of literals : 1135 (1118 equ; 389 neg)
% Maximal clause size : 20 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_239,plain,
op1(op1(e11,e11),e11) = e13,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_239) ).
cnf(i_0_241,plain,
op1(e11,e11) = e10,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_241) ).
cnf(i_0_136,plain,
op1(e13,e11) != op1(e10,e11),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_136) ).
cnf(i_0_228,plain,
( op1(e10,e11) = e10
| op1(e11,e11) = e11
| op1(e12,e11) = e12
| op1(e13,e11) = e13 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_228) ).
cnf(i_0_198,plain,
e10 != e11,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_198) ).
cnf(i_0_196,plain,
e13 != e10,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_196) ).
cnf(i_0_37,plain,
( op1(e10,e11) = e11
| op1(e11,e11) = e11
| op1(e12,e11) = e11
| op1(e13,e11) = e11 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_37) ).
cnf(i_0_194,plain,
e13 != e11,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_194) ).
cnf(i_0_108,plain,
op1(e12,e10) != op1(e12,e11),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_108) ).
cnf(i_0_120,plain,
op1(e10,e10) != op1(e10,e11),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_120) ).
cnf(i_0_240,plain,
op1(op1(op1(e11,e11),e11),op1(e11,e11)) = e12,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_240) ).
cnf(i_0_195,plain,
e12 != e11,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_195) ).
cnf(i_0_229,plain,
( op1(e10,e10) = e10
| op1(e11,e10) = e11
| op1(e12,e10) = e12
| op1(e13,e10) = e13 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_229) ).
cnf(i_0_16,plain,
( op1(e10,e10) = e10
| op1(e10,e10) = e11
| op1(e10,e10) = e12
| op1(e10,e10) = e13 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_16) ).
cnf(i_0_142,plain,
op1(e13,e10) != op1(e10,e10),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_142) ).
cnf(i_0_98,plain,
op1(e13,e13) != op1(e13,e11),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_98) ).
cnf(i_0_193,plain,
e12 != e13,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_193) ).
cnf(i_0_114,plain,
op1(e11,e10) != op1(e11,e11),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_114) ).
cnf(i_0_242,plain,
op2(op2(e21,e21),e21) = e23,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_242) ).
cnf(i_0_244,plain,
op2(e21,e21) = e20,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_244) ).
cnf(i_0_1,plain,
( op1(e13,e13) = e10
| op1(e13,e13) = e11
| op1(e13,e13) = e12
| op1(e13,e13) = e13 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_1) ).
cnf(i_0_100,plain,
op1(e13,e13) != op1(e13,e10),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_100) ).
cnf(i_0_104,plain,
op1(e12,e13) != op1(e12,e11),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_104) ).
cnf(i_0_144,plain,
op1(e10,e10) != op1(e11,e10),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_144) ).
cnf(i_0_99,plain,
op1(e13,e12) != op1(e13,e11),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_99) ).
cnf(i_0_12,plain,
( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e12
| op1(e11,e10) = e13 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_12) ).
cnf(i_0_140,plain,
op1(e13,e10) != op1(e11,e10),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_140) ).
cnf(i_0_243,plain,
op2(op2(op2(e21,e21),e21),op2(e21,e21)) = e22,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_243) ).
cnf(i_0_226,plain,
( op1(e10,e13) = e10
| op1(e11,e13) = e11
| op1(e12,e13) = e12
| op1(e13,e13) = e13 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_226) ).
cnf(i_0_118,plain,
op1(e10,e13) != op1(e10,e10),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_118) ).
cnf(i_0_2,plain,
( op1(e13,e12) = e10
| op1(e13,e12) = e11
| op1(e13,e12) = e12
| op1(e13,e12) = e13 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_2) ).
cnf(i_0_101,plain,
op1(e13,e12) != op1(e13,e10),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_101) ).
cnf(i_0_105,plain,
op1(e12,e12) != op1(e12,e11),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_105) ).
cnf(i_0_182,plain,
op2(e23,e21) != op2(e21,e21),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_182) ).
cnf(i_0_150,plain,
op2(e23,e21) != op2(e23,e20),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_150) ).
cnf(i_0_184,plain,
op2(e23,e21) != op2(e20,e21),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_184) ).
cnf(i_0_190,plain,
op2(e23,e20) != op2(e20,e20),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_190) ).
cnf(i_0_247,plain,
op2(e20,e20) = h1(e10),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_247) ).
cnf(i_0_168,plain,
op2(e20,e21) != op2(e20,e20),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_168) ).
cnf(i_0_148,plain,
op2(e23,e23) != op2(e23,e20),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_148) ).
cnf(i_0_259,plain,
op2(e23,e23) = h4(e10),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_259) ).
cnf(i_0_122,plain,
op1(e13,e13) != op1(e11,e13),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_122) ).
cnf(i_0_227,plain,
( op1(e10,e12) = e10
| op1(e11,e12) = e11
| op1(e12,e12) = e12
| op1(e13,e12) = e13 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_227) ).
cnf(i_0_119,plain,
op1(e10,e12) != op1(e10,e10),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_119) ).
cnf(i_0_113,plain,
op1(e11,e12) != op1(e11,e10),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_113) ).
cnf(i_0_51,plain,
( op2(e23,e21) = e20
| op2(e23,e21) = e21
| op2(e23,e21) = e22
| op2(e23,e21) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_51) ).
cnf(i_0_187,plain,
op2(e23,e20) != op2(e22,e20),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_187) ).
cnf(i_0_146,plain,
op2(e23,e23) != op2(e23,e21),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_146) ).
cnf(i_0_34,plain,
( op1(e11,e10) = e13
| op1(e11,e11) = e13
| op1(e11,e12) = e13
| op1(e11,e13) = e13 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_34) ).
cnf(i_0_128,plain,
op1(e13,e12) != op1(e11,e12),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_128) ).
cnf(i_0_153,plain,
op2(e22,e22) != op2(e22,e21),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_153) ).
cnf(i_0_255,plain,
op2(e22,e22) = h3(e10),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_255) ).
cnf(i_0_237,plain,
( op2(e20,e21) = e20
| op2(e21,e21) = e21
| op2(e22,e21) = e22
| op2(e23,e21) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_237) ).
cnf(i_0_202,plain,
e23 != e20,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_202) ).
cnf(i_0_204,plain,
e21 != e20,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_204) ).
cnf(i_0_200,plain,
e23 != e21,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_200) ).
cnf(i_0_192,plain,
op2(e21,e20) != op2(e20,e20),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_192) ).
cnf(i_0_238,plain,
( op2(e20,e20) = e20
| op2(e21,e20) = e21
| op2(e22,e20) = e22
| op2(e23,e20) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_238) ).
cnf(i_0_199,plain,
e23 != e22,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_199) ).
cnf(i_0_64,plain,
( op2(e20,e20) = e20
| op2(e20,e20) = e21
| op2(e20,e20) = e22
| op2(e20,e20) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_64) ).
cnf(i_0_49,plain,
( op2(e23,e23) = e20
| op2(e23,e23) = e21
| op2(e23,e23) = e22
| op2(e23,e23) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_49) ).
cnf(i_0_24,plain,
( op1(e13,e10) = e10
| op1(e13,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_24) ).
cnf(i_0_236,plain,
( op2(e20,e22) = e20
| op2(e21,e22) = e21
| op2(e22,e22) = e22
| op2(e23,e22) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_236) ).
cnf(i_0_167,plain,
op2(e20,e22) != op2(e20,e20),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_167) ).
cnf(i_0_257,plain,
op2(op2(e23,e23),e23) = h4(e13),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_257) ).
cnf(i_0_36,plain,
( op1(e11,e10) = e12
| op1(e11,e11) = e12
| op1(e11,e12) = e12
| op1(e11,e13) = e12 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_36) ).
cnf(i_0_197,plain,
e12 != e10,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_197) ).
cnf(i_0_116,plain,
op1(e10,e13) != op1(e10,e11),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_116) ).
cnf(i_0_159,plain,
op2(e21,e22) != op2(e21,e21),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_159) ).
cnf(i_0_102,plain,
op1(e13,e10) != op1(e13,e11),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_102) ).
cnf(i_0_224,plain,
( epred1_0
| op1(e13,op1(e13,e11)) != e11 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_224) ).
cnf(i_0_17,plain,
( op1(e10,e13) = e13
| op1(e11,e13) = e13
| op1(e12,e13) = e13
| op1(e13,e13) = e13 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_17) ).
cnf(i_0_112,plain,
op1(e11,e13) != op1(e11,e10),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_112) ).
cnf(i_0_111,plain,
op1(e11,e12) != op1(e11,e11),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_111) ).
cnf(i_0_235,plain,
( op2(e20,e23) = e20
| op2(e21,e23) = e21
| op2(e22,e23) = e22
| op2(e23,e23) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_235) ).
cnf(i_0_152,plain,
op2(e22,e23) != op2(e22,e21),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_152) ).
cnf(i_0_166,plain,
op2(e20,e23) != op2(e20,e20),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_166) ).
cnf(i_0_145,plain,
op2(e23,e23) != op2(e23,e22),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_145) ).
cnf(i_0_79,plain,
( op2(e20,e22) = e20
| op2(e21,e22) = e20
| op2(e22,e22) = e20
| op2(e23,e22) = e20 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_79) ).
cnf(i_0_258,plain,
op2(op2(op2(e23,e23),e23),op2(e23,e23)) = h4(e12),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_258) ).
cnf(i_0_45,plain,
( op1(e10,e10) = e11
| op1(e11,e10) = e11
| op1(e12,e10) = e11
| op1(e13,e10) = e11 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_45) ).
cnf(i_0_329,plain,
( op1(e10,op1(e10,e10)) != e10
| op1(e11,op1(e11,e12)) != e12
| op1(e12,op1(e12,e13)) != e13
| ~ epred1_0 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_329) ).
cnf(i_0_121,plain,
op1(e12,e13) != op1(e13,e13),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_121) ).
cnf(i_0_31,plain,
( op1(e10,e12) = e10
| op1(e11,e12) = e10
| op1(e12,e12) = e10
| op1(e13,e12) = e10 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_31) ).
cnf(i_0_177,plain,
op2(e22,e22) != op2(e21,e22),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_177) ).
cnf(i_0_66,plain,
( op2(e23,e20) = e23
| op2(e23,e21) = e23
| op2(e23,e22) = e23
| op2(e23,e23) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_66) ).
cnf(i_0_175,plain,
op2(e23,e22) != op2(e22,e22),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_175) ).
cnf(i_0_127,plain,
op1(e12,e12) != op1(e13,e12),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_127) ).
cnf(i_0_97,plain,
op1(e13,e12) != op1(e13,e13),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_97) ).
cnf(i_0_93,plain,
( op2(e20,e20) = e21
| op2(e21,e20) = e21
| op2(e22,e20) = e21
| op2(e23,e20) = e21 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_93) ).
cnf(i_0_201,plain,
e22 != e21,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_201) ).
cnf(i_0_54,plain,
( op2(e22,e22) = e20
| op2(e22,e22) = e21
| op2(e22,e22) = e22
| op2(e22,e22) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_54) ).
cnf(i_0_26,plain,
( op1(e12,e10) = e13
| op1(e12,e11) = e13
| op1(e12,e12) = e13
| op1(e12,e13) = e13 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_26) ).
cnf(i_0_72,plain,
( op2(e23,e20) = e20
| op2(e23,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e23) = e20 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_72) ).
cnf(i_0_203,plain,
e22 != e20,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_203) ).
cnf(i_0_67,plain,
( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e22,e23) = e22
| op2(e23,e23) = e22 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_67) ).
cnf(i_0_160,plain,
op2(e21,e23) != op2(e21,e20),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_160) ).
cnf(i_0_149,plain,
op2(e23,e22) != op2(e23,e20),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_149) ).
cnf(i_0_94,plain,
( op2(e20,e20) = e21
| op2(e20,e21) = e21
| op2(e20,e22) = e21
| op2(e20,e23) = e21 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_94) ).
cnf(i_0_249,plain,
op2(op2(e21,e21),e21) = h2(e13),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_249) ).
cnf(i_0_27,plain,
( op1(e10,e12) = e12
| op1(e11,e12) = e12
| op1(e12,e12) = e12
| op1(e13,e12) = e12 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_27) ).
cnf(i_0_191,plain,
op2(e22,e20) != op2(e20,e20),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_191) ).
cnf(i_0_185,plain,
op2(e22,e21) != op2(e20,e21),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_185) ).
cnf(i_0_161,plain,
op2(e21,e22) != op2(e21,e20),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_161) ).
cnf(i_0_50,plain,
( op2(e23,e22) = e20
| op2(e23,e22) = e21
| op2(e23,e22) = e22
| op2(e23,e22) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_50) ).
cnf(i_0_147,plain,
op2(e23,e22) != op2(e23,e21),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_147) ).
cnf(i_0_253,plain,
op2(op2(e22,e22),e22) = h3(e13),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_253) ).
cnf(i_0_174,plain,
op2(e21,e23) != op2(e20,e23),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_174) ).
cnf(i_0_251,plain,
op2(e21,e21) = h2(e10),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_251) ).
cnf(i_0_250,plain,
op2(op2(op2(e21,e21),e21),op2(e21,e21)) = h2(e12),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_250) ).
cnf(i_0_269,negated_conjecture,
( h2(e13) != e23
| ~ epred46_0 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_269) ).
cnf(i_0_46,plain,
( op1(e10,e10) = e11
| op1(e10,e11) = e11
| op1(e10,e12) = e11
| op1(e10,e13) = e11 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_46) ).
cnf(i_0_132,plain,
op1(e10,e12) != op1(e11,e12),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_132) ).
cnf(i_0_5,plain,
( op1(e12,e13) = e10
| op1(e12,e13) = e11
| op1(e12,e13) = e12
| op1(e12,e13) = e13 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_5) ).
cnf(i_0_106,plain,
op1(e12,e13) != op1(e12,e10),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_106) ).
cnf(i_0_56,plain,
( op2(e22,e20) = e20
| op2(e22,e20) = e21
| op2(e22,e20) = e22
| op2(e22,e20) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_56) ).
cnf(i_0_158,plain,
op2(e21,e23) != op2(e21,e21),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_158) ).
cnf(i_0_74,plain,
( op2(e22,e20) = e23
| op2(e22,e21) = e23
| op2(e22,e22) = e23
| op2(e22,e23) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_74) ).
cnf(i_0_254,plain,
op2(op2(op2(e22,e22),e22),op2(e22,e22)) = h3(e12),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_254) ).
cnf(i_0_89,plain,
( op2(e20,e20) = e23
| op2(e21,e20) = e23
| op2(e22,e20) = e23
| op2(e23,e20) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_89) ).
cnf(i_0_164,plain,
op2(e20,e23) != op2(e20,e21),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_164) ).
cnf(i_0_2696,plain,
( epred46_0
| h2(e10) != e20
| h2(e11) != e21
| h2(e12) != e22
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e13)) != h2(op1(e10,e13))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e13)) != h2(op1(e12,e13))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e12)) != h2(op1(e13,e12))
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_2696) ).
cnf(i_0_252,plain,
h2(e11) = e21,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_252) ).
cnf(i_0_155,plain,
op2(e22,e22) != op2(e22,e20),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_155) ).
cnf(i_0_75,plain,
( op2(e20,e22) = e22
| op2(e21,e22) = e22
| op2(e22,e22) = e22
| op2(e23,e22) = e22 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_75) ).
cnf(i_0_71,plain,
( op2(e20,e23) = e20
| op2(e21,e23) = e20
| op2(e22,e23) = e20
| op2(e23,e23) = e20 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_71) ).
cnf(i_0_169,plain,
op2(e23,e23) != op2(e22,e23),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_169) ).
cnf(i_0_61,plain,
( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e22
| op2(e20,e23) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_61) ).
cnf(i_0_170,plain,
op2(e23,e23) != op2(e21,e23),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_170) ).
cnf(i_0_57,plain,
( op2(e21,e23) = e20
| op2(e21,e23) = e21
| op2(e21,e23) = e22
| op2(e21,e23) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_57) ).
cnf(i_0_53,plain,
( op2(e22,e23) = e20
| op2(e22,e23) = e21
| op2(e22,e23) = e22
| op2(e22,e23) = e23 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_53) ).
cnf(i_0_154,plain,
op2(e22,e23) != op2(e22,e20),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_154) ).
cnf(i_0_179,plain,
op2(e22,e22) != op2(e20,e22),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_179) ).
cnf(i_0_163,plain,
op2(e20,e23) != op2(e20,e22),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_163) ).
cnf(i_0_151,plain,
op2(e22,e23) != op2(e22,e22),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_151) ).
cnf(i_0_188,plain,
op2(e23,e20) != op2(e21,e20),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_188) ).
cnf(i_0_84,plain,
( op2(e21,e20) = e22
| op2(e21,e21) = e22
| op2(e21,e22) = e22
| op2(e21,e23) = e22 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_84) ).
cnf(i_0_1478,plain,
( op2(e20,op2(e20,e20)) != e20
| op2(e21,op2(e21,e22)) != e22
| op2(e22,op2(e22,e23)) != e23
| ~ epred23_0 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_1478) ).
cnf(i_0_233,plain,
( epred23_0
| op2(e23,op2(e23,e21)) != e21 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-341b9656/input.p',i_0_233) ).
cnf(c_0_2836,plain,
op1(op1(e11,e11),e11) = e13,
i_0_239 ).
cnf(c_0_2837,plain,
op1(e11,e11) = e10,
i_0_241 ).
cnf(c_0_2838,plain,
op1(e13,e11) != op1(e10,e11),
i_0_136 ).
cnf(c_0_2839,plain,
op1(e10,e11) = e13,
inference(rw,[status(thm)],[c_0_2836,c_0_2837]) ).
cnf(c_0_2840,plain,
( op1(e10,e11) = e10
| op1(e11,e11) = e11
| op1(e12,e11) = e12
| op1(e13,e11) = e13 ),
i_0_228 ).
cnf(c_0_2841,plain,
e10 != e11,
i_0_198 ).
cnf(c_0_2842,plain,
e13 != e10,
i_0_196 ).
cnf(c_0_2843,plain,
op1(e13,e11) != e13,
inference(rw,[status(thm)],[c_0_2838,c_0_2839]) ).
cnf(c_0_2844,plain,
( op1(e10,e11) = e11
| op1(e11,e11) = e11
| op1(e12,e11) = e11
| op1(e13,e11) = e11 ),
i_0_37 ).
cnf(c_0_2845,plain,
e13 != e11,
i_0_194 ).
cnf(c_0_2846,plain,
op1(e12,e10) != op1(e12,e11),
i_0_108 ).
cnf(c_0_2847,plain,
op1(e12,e11) = e12,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_2840,c_0_2837]),c_0_2839]),c_0_2841]),c_0_2842]),c_0_2843]) ).
cnf(c_0_2848,plain,
op1(e10,e10) != op1(e10,e11),
i_0_120 ).
cnf(c_0_2849,plain,
op1(op1(op1(e11,e11),e11),op1(e11,e11)) = e12,
i_0_240 ).
cnf(c_0_2850,plain,
( op1(e12,e11) = e11
| op1(e13,e11) = e11 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_2844,c_0_2837]),c_0_2839]),c_0_2841]),c_0_2845]) ).
cnf(c_0_2851,plain,
e12 != e11,
i_0_195 ).
cnf(c_0_2852,plain,
( op1(e10,e10) = e10
| op1(e11,e10) = e11
| op1(e12,e10) = e12
| op1(e13,e10) = e13 ),
i_0_229 ).
cnf(c_0_2853,plain,
op1(e12,e10) != e12,
inference(rw,[status(thm)],[c_0_2846,c_0_2847]) ).
cnf(c_0_2854,plain,
( op1(e10,e10) = e10
| op1(e10,e10) = e11
| op1(e10,e10) = e12
| op1(e10,e10) = e13 ),
i_0_16 ).
cnf(c_0_2855,plain,
op1(e10,e10) != e13,
inference(rw,[status(thm)],[c_0_2848,c_0_2839]) ).
cnf(c_0_2856,plain,
op1(e13,e10) != op1(e10,e10),
i_0_142 ).
cnf(c_0_2857,plain,
op1(e13,e10) = e12,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_2849,c_0_2837]),c_0_2839]),c_0_2837]) ).
cnf(c_0_2858,plain,
op1(e13,e13) != op1(e13,e11),
i_0_98 ).
cnf(c_0_2859,plain,
op1(e13,e11) = e11,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_2850,c_0_2847]),c_0_2851]) ).
cnf(c_0_2860,plain,
( op1(e13,e10) = e13
| op1(e10,e10) = e10
| op1(e11,e10) = e11 ),
inference(sr,[status(thm)],[c_0_2852,c_0_2853]) ).
cnf(c_0_2861,plain,
e12 != e13,
i_0_193 ).
cnf(c_0_2862,plain,
( op1(e10,e10) = e12
| op1(e10,e10) = e10
| op1(e10,e10) = e11 ),
inference(sr,[status(thm)],[c_0_2854,c_0_2855]) ).
cnf(c_0_2863,plain,
op1(e10,e10) != e12,
inference(rw,[status(thm)],[c_0_2856,c_0_2857]) ).
cnf(c_0_2864,plain,
op1(e11,e10) != op1(e11,e11),
i_0_114 ).
cnf(c_0_2865,plain,
op2(op2(e21,e21),e21) = e23,
i_0_242 ).
cnf(c_0_2866,plain,
op2(e21,e21) = e20,
i_0_244 ).
cnf(c_0_2867,plain,
( op1(e13,e13) = e10
| op1(e13,e13) = e11
| op1(e13,e13) = e12
| op1(e13,e13) = e13 ),
i_0_1 ).
cnf(c_0_2868,plain,
op1(e13,e13) != e11,
inference(rw,[status(thm)],[c_0_2858,c_0_2859]) ).
cnf(c_0_2869,plain,
op1(e13,e13) != op1(e13,e10),
i_0_100 ).
cnf(c_0_2870,plain,
op1(e12,e13) != op1(e12,e11),
i_0_104 ).
cnf(c_0_2871,plain,
op1(e10,e10) != op1(e11,e10),
i_0_144 ).
cnf(c_0_2872,plain,
( op1(e10,e10) = e10
| op1(e11,e10) = e11 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2857,c_0_2860]),c_0_2861]) ).
cnf(c_0_2873,plain,
( op1(e10,e10) = e11
| op1(e10,e10) = e10 ),
inference(sr,[status(thm)],[c_0_2862,c_0_2863]) ).
cnf(c_0_2874,plain,
op1(e13,e12) != op1(e13,e11),
i_0_99 ).
cnf(c_0_2875,plain,
( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e12
| op1(e11,e10) = e13 ),
i_0_12 ).
cnf(c_0_2876,plain,
op1(e11,e10) != e10,
inference(rw,[status(thm)],[c_0_2864,c_0_2837]) ).
cnf(c_0_2877,plain,
op1(e13,e10) != op1(e11,e10),
i_0_140 ).
cnf(c_0_2878,plain,
op2(op2(op2(e21,e21),e21),op2(e21,e21)) = e22,
i_0_243 ).
cnf(c_0_2879,plain,
op2(e20,e21) = e23,
inference(rw,[status(thm)],[c_0_2865,c_0_2866]) ).
cnf(c_0_2880,plain,
( op1(e13,e13) = e12
| op1(e13,e13) = e13
| op1(e13,e13) = e10 ),
inference(sr,[status(thm)],[c_0_2867,c_0_2868]) ).
cnf(c_0_2881,plain,
op1(e13,e13) != e12,
inference(rw,[status(thm)],[c_0_2869,c_0_2857]) ).
cnf(c_0_2882,plain,
( op1(e10,e13) = e10
| op1(e11,e13) = e11
| op1(e12,e13) = e12
| op1(e13,e13) = e13 ),
i_0_226 ).
cnf(c_0_2883,plain,
op1(e12,e13) != e12,
inference(rw,[status(thm)],[c_0_2870,c_0_2847]) ).
cnf(c_0_2884,plain,
op1(e10,e13) != op1(e10,e10),
i_0_118 ).
cnf(c_0_2885,plain,
op1(e10,e10) = e10,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2871,c_0_2872]),c_0_2873]) ).
cnf(c_0_2886,plain,
( op1(e13,e12) = e10
| op1(e13,e12) = e11
| op1(e13,e12) = e12
| op1(e13,e12) = e13 ),
i_0_2 ).
cnf(c_0_2887,plain,
op1(e13,e12) != e11,
inference(rw,[status(thm)],[c_0_2874,c_0_2859]) ).
cnf(c_0_2888,plain,
op1(e13,e12) != op1(e13,e10),
i_0_101 ).
cnf(c_0_2889,plain,
op1(e12,e12) != op1(e12,e11),
i_0_105 ).
cnf(c_0_2890,plain,
( op1(e11,e10) = e12
| op1(e11,e10) = e13
| op1(e11,e10) = e11 ),
inference(sr,[status(thm)],[c_0_2875,c_0_2876]) ).
cnf(c_0_2891,plain,
op1(e11,e10) != e12,
inference(rw,[status(thm)],[c_0_2877,c_0_2857]) ).
cnf(c_0_2892,plain,
op2(e23,e21) != op2(e21,e21),
i_0_182 ).
cnf(c_0_2893,plain,
op2(e23,e21) != op2(e23,e20),
i_0_150 ).
cnf(c_0_2894,plain,
op2(e23,e20) = e22,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_2878,c_0_2866]),c_0_2879]),c_0_2866]) ).
cnf(c_0_2895,plain,
op2(e23,e21) != op2(e20,e21),
i_0_184 ).
cnf(c_0_2896,plain,
op2(e23,e20) != op2(e20,e20),
i_0_190 ).
cnf(c_0_2897,plain,
op2(e20,e20) = h1(e10),
i_0_247 ).
cnf(c_0_2898,plain,
op2(e20,e21) != op2(e20,e20),
i_0_168 ).
cnf(c_0_2899,plain,
op2(e23,e23) != op2(e23,e20),
i_0_148 ).
cnf(c_0_2900,plain,
op2(e23,e23) = h4(e10),
i_0_259 ).
cnf(c_0_2901,plain,
op1(e13,e13) != op1(e11,e13),
i_0_122 ).
cnf(c_0_2902,plain,
( op1(e13,e13) = e10
| op1(e13,e13) = e13 ),
inference(sr,[status(thm)],[c_0_2880,c_0_2881]) ).
cnf(c_0_2903,plain,
( op1(e13,e13) = e13
| op1(e10,e13) = e10
| op1(e11,e13) = e11 ),
inference(sr,[status(thm)],[c_0_2882,c_0_2883]) ).
cnf(c_0_2904,plain,
op1(e10,e13) != e10,
inference(rw,[status(thm)],[c_0_2884,c_0_2885]) ).
cnf(c_0_2905,plain,
( op1(e13,e12) = e12
| op1(e13,e12) = e13
| op1(e13,e12) = e10 ),
inference(sr,[status(thm)],[c_0_2886,c_0_2887]) ).
cnf(c_0_2906,plain,
op1(e13,e12) != e12,
inference(rw,[status(thm)],[c_0_2888,c_0_2857]) ).
cnf(c_0_2907,plain,
( op1(e10,e12) = e10
| op1(e11,e12) = e11
| op1(e12,e12) = e12
| op1(e13,e12) = e13 ),
i_0_227 ).
cnf(c_0_2908,plain,
op1(e12,e12) != e12,
inference(rw,[status(thm)],[c_0_2889,c_0_2847]) ).
cnf(c_0_2909,plain,
op1(e10,e12) != op1(e10,e10),
i_0_119 ).
cnf(c_0_2910,plain,
op1(e11,e12) != op1(e11,e10),
i_0_113 ).
cnf(c_0_2911,plain,
( op1(e11,e10) = e11
| op1(e11,e10) = e13 ),
inference(sr,[status(thm)],[c_0_2890,c_0_2891]) ).
cnf(c_0_2912,plain,
( op2(e23,e21) = e20
| op2(e23,e21) = e21
| op2(e23,e21) = e22
| op2(e23,e21) = e23 ),
i_0_51 ).
cnf(c_0_2913,plain,
op2(e23,e21) != e20,
inference(rw,[status(thm)],[c_0_2892,c_0_2866]) ).
cnf(c_0_2914,plain,
op2(e23,e21) != e22,
inference(rw,[status(thm)],[c_0_2893,c_0_2894]) ).
cnf(c_0_2915,plain,
op2(e23,e21) != e23,
inference(rw,[status(thm)],[c_0_2895,c_0_2879]) ).
cnf(c_0_2916,plain,
op2(e23,e20) != op2(e22,e20),
i_0_187 ).
cnf(c_0_2917,plain,
op2(e23,e20) != h1(e10),
inference(rw,[status(thm)],[c_0_2896,c_0_2897]) ).
cnf(c_0_2918,plain,
op2(e20,e21) != h1(e10),
inference(rw,[status(thm)],[c_0_2898,c_0_2897]) ).
cnf(c_0_2919,plain,
op2(e23,e20) != h4(e10),
inference(rw,[status(thm)],[c_0_2899,c_0_2900]) ).
cnf(c_0_2920,plain,
op2(e23,e23) != op2(e23,e21),
i_0_146 ).
cnf(c_0_2921,plain,
( op1(e13,e13) = e10
| op1(e11,e13) != e13 ),
inference(spm,[status(thm)],[c_0_2901,c_0_2902]) ).
cnf(c_0_2922,plain,
( op1(e11,e13) = e11
| op1(e13,e13) = e13 ),
inference(sr,[status(thm)],[c_0_2903,c_0_2904]) ).
cnf(c_0_2923,plain,
( op1(e11,e10) = e13
| op1(e11,e11) = e13
| op1(e11,e12) = e13
| op1(e11,e13) = e13 ),
i_0_34 ).
cnf(c_0_2924,plain,
op1(e13,e12) != op1(e11,e12),
i_0_128 ).
cnf(c_0_2925,plain,
( op1(e13,e12) = e10
| op1(e13,e12) = e13 ),
inference(sr,[status(thm)],[c_0_2905,c_0_2906]) ).
cnf(c_0_2926,plain,
( op1(e13,e12) = e13
| op1(e10,e12) = e10
| op1(e11,e12) = e11 ),
inference(sr,[status(thm)],[c_0_2907,c_0_2908]) ).
cnf(c_0_2927,plain,
op1(e10,e12) != e10,
inference(rw,[status(thm)],[c_0_2909,c_0_2885]) ).
cnf(c_0_2928,plain,
( op1(e11,e10) = e11
| op1(e11,e12) != e13 ),
inference(spm,[status(thm)],[c_0_2910,c_0_2911]) ).
cnf(c_0_2929,plain,
op2(e22,e22) != op2(e22,e21),
i_0_153 ).
cnf(c_0_2930,plain,
op2(e22,e22) = h3(e10),
i_0_255 ).
cnf(c_0_2931,plain,
( op2(e20,e21) = e20
| op2(e21,e21) = e21
| op2(e22,e21) = e22
| op2(e23,e21) = e23 ),
i_0_237 ).
cnf(c_0_2932,plain,
op2(e23,e21) = e21,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_2912,c_0_2913]),c_0_2914]),c_0_2915]) ).
cnf(c_0_2933,plain,
e23 != e20,
i_0_202 ).
cnf(c_0_2934,plain,
e21 != e20,
i_0_204 ).
cnf(c_0_2935,plain,
e23 != e21,
i_0_200 ).
cnf(c_0_2936,plain,
op2(e21,e20) != op2(e20,e20),
i_0_192 ).
cnf(c_0_2937,plain,
( op2(e20,e20) = e20
| op2(e21,e20) = e21
| op2(e22,e20) = e22
| op2(e23,e20) = e23 ),
i_0_238 ).
cnf(c_0_2938,plain,
op2(e22,e20) != e22,
inference(rw,[status(thm)],[c_0_2916,c_0_2894]) ).
cnf(c_0_2939,plain,
e23 != e22,
i_0_199 ).
cnf(c_0_2940,plain,
( op2(e20,e20) = e20
| op2(e20,e20) = e21
| op2(e20,e20) = e22
| op2(e20,e20) = e23 ),
i_0_64 ).
cnf(c_0_2941,plain,
h1(e10) != e22,
inference(rw,[status(thm)],[c_0_2917,c_0_2894]) ).
cnf(c_0_2942,plain,
e23 != h1(e10),
inference(rw,[status(thm)],[c_0_2918,c_0_2879]) ).
cnf(c_0_2943,plain,
( op2(e23,e23) = e20
| op2(e23,e23) = e21
| op2(e23,e23) = e22
| op2(e23,e23) = e23 ),
i_0_49 ).
cnf(c_0_2944,plain,
h4(e10) != e22,
inference(rw,[status(thm)],[c_0_2919,c_0_2894]) ).
cnf(c_0_2945,plain,
op2(e23,e21) != h4(e10),
inference(rw,[status(thm)],[c_0_2920,c_0_2900]) ).
cnf(c_0_2946,plain,
( op1(e13,e10) = e10
| op1(e13,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10 ),
i_0_24 ).
cnf(c_0_2947,plain,
( op1(e11,e13) = e11
| op1(e11,e13) != e13 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2921,c_0_2922]),c_0_2842]) ).
cnf(c_0_2948,plain,
( op1(e11,e12) = e13
| op1(e11,e13) = e13
| op1(e11,e10) = e13 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_2923,c_0_2837]),c_0_2842]) ).
cnf(c_0_2949,plain,
( op1(e13,e12) = e10
| op1(e11,e12) != e13 ),
inference(spm,[status(thm)],[c_0_2924,c_0_2925]) ).
cnf(c_0_2950,plain,
( op1(e11,e12) = e11
| op1(e13,e12) = e13 ),
inference(sr,[status(thm)],[c_0_2926,c_0_2927]) ).
cnf(c_0_2951,plain,
( op1(e11,e12) != e11
| op1(e11,e12) != e13 ),
inference(spm,[status(thm)],[c_0_2910,c_0_2928]) ).
cnf(c_0_2952,plain,
( op2(e20,e22) = e20
| op2(e21,e22) = e21
| op2(e22,e22) = e22
| op2(e23,e22) = e23 ),
i_0_236 ).
cnf(c_0_2953,plain,
op2(e22,e21) != h3(e10),
inference(rw,[status(thm)],[c_0_2929,c_0_2930]) ).
cnf(c_0_2954,plain,
op2(e22,e21) = e22,
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_2931,c_0_2879]),c_0_2866]),c_0_2932]),c_0_2933]),c_0_2934]),c_0_2935]) ).
cnf(c_0_2955,plain,
op2(e20,e22) != op2(e20,e20),
i_0_167 ).
cnf(c_0_2956,plain,
op2(e21,e20) != h1(e10),
inference(rw,[status(thm)],[c_0_2936,c_0_2897]) ).
cnf(c_0_2957,plain,
( op2(e21,e20) = e21
| h1(e10) = e20 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_2937,c_0_2897]),c_0_2894]),c_0_2938]),c_0_2939]) ).
cnf(c_0_2958,plain,
( h1(e10) = e21
| h1(e10) = e20 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_2940,c_0_2897]),c_0_2897]),c_0_2897]),c_0_2897]),c_0_2941]),c_0_2942]) ).
cnf(c_0_2959,plain,
( e23 = h4(e10)
| h4(e10) = e21
| h4(e10) = e20 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_2943,c_0_2900]),c_0_2900]),c_0_2900]),c_0_2900]),c_0_2944]) ).
cnf(c_0_2960,plain,
h4(e10) != e21,
inference(rw,[status(thm)],[c_0_2945,c_0_2932]) ).
cnf(c_0_2961,plain,
op2(op2(e23,e23),e23) = h4(e13),
i_0_257 ).
cnf(c_0_2962,plain,
( op1(e11,e10) = e12
| op1(e11,e11) = e12
| op1(e11,e12) = e12
| op1(e11,e13) = e12 ),
i_0_36 ).
cnf(c_0_2963,plain,
e12 != e10,
i_0_197 ).
cnf(c_0_2964,plain,
( op1(e13,e12) = e10
| op1(e13,e13) = e10
| op1(e13,e10) = e10 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_2946,c_0_2859]),c_0_2841]) ).
cnf(c_0_2965,plain,
op1(e10,e13) != op1(e10,e11),
i_0_116 ).
cnf(c_0_2966,plain,
( op1(e11,e12) = e13
| op1(e11,e10) = e13 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2947,c_0_2948]),c_0_2845]) ).
cnf(c_0_2967,plain,
op1(e11,e12) != e13,
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2949,c_0_2950]),c_0_2842]),c_0_2951]) ).
cnf(c_0_2968,plain,
( op2(e23,e22) = e23
| op2(e21,e22) = e21
| op2(e20,e22) = e20
| h3(e10) = e22 ),
inference(rw,[status(thm)],[c_0_2952,c_0_2930]) ).
cnf(c_0_2969,plain,
h3(e10) != e22,
inference(rw,[status(thm)],[c_0_2953,c_0_2954]) ).
cnf(c_0_2970,plain,
op2(e20,e22) != h1(e10),
inference(rw,[status(thm)],[c_0_2955,c_0_2897]) ).
cnf(c_0_2971,plain,
h1(e10) = e20,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2956,c_0_2957]),c_0_2958]) ).
cnf(c_0_2972,plain,
op2(e21,e22) != op2(e21,e21),
i_0_159 ).
cnf(c_0_2973,plain,
( h4(e10) = e20
| e23 = h4(e10) ),
inference(sr,[status(thm)],[c_0_2959,c_0_2960]) ).
cnf(c_0_2974,plain,
op2(h4(e10),e23) = h4(e13),
inference(rw,[status(thm)],[c_0_2961,c_0_2900]) ).
cnf(c_0_2975,plain,
op1(e13,e10) != op1(e13,e11),
i_0_102 ).
cnf(c_0_2976,plain,
( epred1_0
| op1(e13,op1(e13,e11)) != e11 ),
i_0_224 ).
cnf(c_0_2977,plain,
( op1(e11,e12) = e12
| op1(e11,e13) = e12
| op1(e11,e10) = e12 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_2962,c_0_2837]),c_0_2963]) ).
cnf(c_0_2978,plain,
( op1(e13,e13) = e10
| op1(e13,e12) = e10 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_2964,c_0_2857]),c_0_2963]) ).
cnf(c_0_2979,plain,
( op1(e10,e13) = e13
| op1(e11,e13) = e13
| op1(e12,e13) = e13
| op1(e13,e13) = e13 ),
i_0_17 ).
cnf(c_0_2980,plain,
op1(e10,e13) != e13,
inference(rw,[status(thm)],[c_0_2965,c_0_2839]) ).
cnf(c_0_2981,plain,
op1(e11,e13) != op1(e11,e10),
i_0_112 ).
cnf(c_0_2982,plain,
op1(e11,e10) = e13,
inference(sr,[status(thm)],[c_0_2966,c_0_2967]) ).
cnf(c_0_2983,plain,
op1(e11,e12) != op1(e11,e11),
i_0_111 ).
cnf(c_0_2984,plain,
( op2(e20,e23) = e20
| op2(e21,e23) = e21
| op2(e22,e23) = e22
| op2(e23,e23) = e23 ),
i_0_235 ).
cnf(c_0_2985,plain,
op2(e22,e23) != op2(e22,e21),
i_0_152 ).
cnf(c_0_2986,plain,
op2(e20,e23) != op2(e20,e20),
i_0_166 ).
cnf(c_0_2987,plain,
op2(e23,e23) != op2(e23,e22),
i_0_145 ).
cnf(c_0_2988,plain,
( op2(e20,e22) = e20
| op2(e21,e22) = e21
| op2(e23,e22) = e23 ),
inference(sr,[status(thm)],[c_0_2968,c_0_2969]) ).
cnf(c_0_2989,plain,
op2(e20,e22) != e20,
inference(rw,[status(thm)],[c_0_2970,c_0_2971]) ).
cnf(c_0_2990,plain,
( op2(e20,e22) = e20
| op2(e21,e22) = e20
| op2(e22,e22) = e20
| op2(e23,e22) = e20 ),
i_0_79 ).
cnf(c_0_2991,plain,
op2(e21,e22) != e20,
inference(rw,[status(thm)],[c_0_2972,c_0_2866]) ).
cnf(c_0_2992,plain,
op2(op2(op2(e23,e23),e23),op2(e23,e23)) = h4(e12),
i_0_258 ).
cnf(c_0_2993,plain,
( op2(h4(e10),h4(e10)) = h4(e10)
| h4(e10) = e20 ),
inference(spm,[status(thm)],[c_0_2900,c_0_2973]) ).
cnf(c_0_2994,plain,
( op2(h4(e10),h4(e10)) = h4(e13)
| h4(e10) = e20 ),
inference(spm,[status(thm)],[c_0_2974,c_0_2973]) ).
cnf(c_0_2995,plain,
( op1(e10,e10) = e11
| op1(e11,e10) = e11
| op1(e12,e10) = e11
| op1(e13,e10) = e11 ),
i_0_45 ).
cnf(c_0_2996,plain,
op1(e13,e10) != e11,
inference(rw,[status(thm)],[c_0_2975,c_0_2859]) ).
cnf(c_0_2997,plain,
( op1(e10,op1(e10,e10)) != e10
| op1(e11,op1(e11,e12)) != e12
| op1(e12,op1(e12,e13)) != e13
| ~ epred1_0 ),
i_0_329 ).
cnf(c_0_2998,plain,
epred1_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_2976,c_0_2859]),c_0_2859])]) ).
cnf(c_0_2999,plain,
( op1(e11,e13) = e12
| op1(e11,e12) = e12 ),
inference(sr,[status(thm)],[c_0_2977,c_0_2891]) ).
cnf(c_0_3000,plain,
( op1(e11,e13) = e11
| op1(e13,e12) = e10 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2978,c_0_2922]),c_0_2842]) ).
cnf(c_0_3001,plain,
( op1(e12,e13) = e13
| op1(e13,e13) = e13
| op1(e11,e13) = e13 ),
inference(sr,[status(thm)],[c_0_2979,c_0_2980]) ).
cnf(c_0_3002,plain,
op1(e11,e13) != e13,
inference(rw,[status(thm)],[c_0_2981,c_0_2982]) ).
cnf(c_0_3003,plain,
op1(e12,e13) != op1(e13,e13),
i_0_121 ).
cnf(c_0_3004,plain,
( op1(e10,e12) = e10
| op1(e11,e12) = e10
| op1(e12,e12) = e10
| op1(e13,e12) = e10 ),
i_0_31 ).
cnf(c_0_3005,plain,
op1(e11,e12) != e10,
inference(rw,[status(thm)],[c_0_2983,c_0_2837]) ).
cnf(c_0_3006,plain,
( op2(e22,e23) = e22
| op2(e21,e23) = e21
| op2(e20,e23) = e20
| e23 = h4(e10) ),
inference(rw,[status(thm)],[c_0_2984,c_0_2900]) ).
cnf(c_0_3007,plain,
op2(e22,e23) != e22,
inference(rw,[status(thm)],[c_0_2985,c_0_2954]) ).
cnf(c_0_3008,plain,
op2(e20,e23) != h1(e10),
inference(rw,[status(thm)],[c_0_2986,c_0_2897]) ).
cnf(c_0_3009,plain,
op2(e22,e22) != op2(e21,e22),
i_0_177 ).
cnf(c_0_3010,plain,
op2(e23,e22) != h4(e10),
inference(rw,[status(thm)],[c_0_2987,c_0_2900]) ).
cnf(c_0_3011,plain,
( op2(e23,e22) = e23
| op2(e21,e22) = e21 ),
inference(sr,[status(thm)],[c_0_2988,c_0_2989]) ).
cnf(c_0_3012,plain,
( op2(e23,e20) = e23
| op2(e23,e21) = e23
| op2(e23,e22) = e23
| op2(e23,e23) = e23 ),
i_0_66 ).
cnf(c_0_3013,plain,
( op2(e23,e22) = e20
| op2(e20,e22) = e20
| h3(e10) = e20 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_2990,c_0_2930]),c_0_2991]) ).
cnf(c_0_3014,plain,
op2(e23,e22) != op2(e22,e22),
i_0_175 ).
cnf(c_0_3015,plain,
op2(h4(e13),h4(e10)) = h4(e12),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_2992,c_0_2900]),c_0_2974]),c_0_2900]) ).
cnf(c_0_3016,plain,
( h4(e13) = h4(e10)
| h4(e10) = e20 ),
inference(spm,[status(thm)],[c_0_2993,c_0_2994]) ).
cnf(c_0_3017,plain,
( op1(e12,e10) = e11
| op1(e10,e10) = e11
| op1(e11,e10) = e11 ),
inference(sr,[status(thm)],[c_0_2995,c_0_2996]) ).
cnf(c_0_3018,plain,
( op1(e11,op1(e11,e12)) != e12
| op1(e10,op1(e10,e10)) != e10
| op1(e12,op1(e12,e13)) != e13 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2997,c_0_2998])]) ).
cnf(c_0_3019,plain,
op1(e12,e12) != op1(e13,e12),
i_0_127 ).
cnf(c_0_3020,plain,
( op1(e13,e12) = e10
| op1(e11,e12) = e12 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2999,c_0_3000]),c_0_2851]) ).
cnf(c_0_3021,plain,
( op1(e12,e13) = e13
| op1(e13,e13) = e13 ),
inference(sr,[status(thm)],[c_0_3001,c_0_3002]) ).
cnf(c_0_3022,plain,
op1(e13,e12) != op1(e13,e13),
i_0_97 ).
cnf(c_0_3023,plain,
( op1(e13,e13) = e10
| op1(e12,e13) != e13 ),
inference(spm,[status(thm)],[c_0_3003,c_0_2902]) ).
cnf(c_0_3024,plain,
( op1(e12,e12) = e10
| op1(e13,e12) = e10
| op1(e10,e12) = e10 ),
inference(sr,[status(thm)],[c_0_3004,c_0_3005]) ).
cnf(c_0_3025,plain,
( op2(e20,e20) = e21
| op2(e21,e20) = e21
| op2(e22,e20) = e21
| op2(e23,e20) = e21 ),
i_0_93 ).
cnf(c_0_3026,plain,
e22 != e21,
i_0_201 ).
cnf(c_0_3027,plain,
( op2(e20,e23) = e20
| op2(e21,e23) = e21
| e23 = h4(e10) ),
inference(sr,[status(thm)],[c_0_3006,c_0_3007]) ).
cnf(c_0_3028,plain,
op2(e20,e23) != e20,
inference(rw,[status(thm)],[c_0_3008,c_0_2971]) ).
cnf(c_0_3029,plain,
op2(e21,e22) != h3(e10),
inference(rw,[status(thm)],[c_0_3009,c_0_2930]) ).
cnf(c_0_3030,plain,
( op2(e21,e22) = e21
| e23 != h4(e10) ),
inference(spm,[status(thm)],[c_0_3010,c_0_3011]) ).
cnf(c_0_3031,plain,
( op2(e23,e22) = e23
| e23 = h4(e10) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3012,c_0_2894]),c_0_2900]),c_0_2939]),c_0_2915]) ).
cnf(c_0_3032,plain,
( op2(e23,e22) = e20
| h3(e10) = e20 ),
inference(sr,[status(thm)],[c_0_3013,c_0_2989]) ).
cnf(c_0_3033,plain,
op2(e23,e22) != h3(e10),
inference(rw,[status(thm)],[c_0_3014,c_0_2930]) ).
cnf(c_0_3034,plain,
( op2(e22,e22) = e20
| op2(e22,e22) = e21
| op2(e22,e22) = e22
| op2(e22,e22) = e23 ),
i_0_54 ).
cnf(c_0_3035,plain,
( op2(h4(e10),h4(e10)) = h4(e12)
| h4(e10) = e20 ),
inference(spm,[status(thm)],[c_0_3015,c_0_3016]) ).
cnf(c_0_3036,plain,
( op1(e12,e10) = e13
| op1(e12,e11) = e13
| op1(e12,e12) = e13
| op1(e12,e13) = e13 ),
i_0_26 ).
cnf(c_0_3037,plain,
( op1(e12,e10) = e11
| op1(e11,e10) = e11 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3017,c_0_2885]),c_0_2841]) ).
cnf(c_0_3038,plain,
( op1(e11,op1(e11,e12)) != e12
| op1(e12,op1(e12,e13)) != e13 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3018,c_0_2885]),c_0_2885])]) ).
cnf(c_0_3039,plain,
( op1(e11,e12) = e12
| op1(e12,e12) != e10 ),
inference(spm,[status(thm)],[c_0_3019,c_0_3020]) ).
cnf(c_0_3040,plain,
( op1(e12,e13) = e13
| op1(e13,e12) = e10 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2978,c_0_3021]),c_0_2842]) ).
cnf(c_0_3041,plain,
( op1(e13,e12) != e10
| op1(e12,e13) != e13 ),
inference(spm,[status(thm)],[c_0_3022,c_0_3023]) ).
cnf(c_0_3042,plain,
( op1(e13,e12) = e10
| op1(e12,e12) = e10 ),
inference(sr,[status(thm)],[c_0_3024,c_0_2927]) ).
cnf(c_0_3043,plain,
( op2(e23,e20) = e20
| op2(e23,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e23) = e20 ),
i_0_72 ).
cnf(c_0_3044,plain,
e22 != e20,
i_0_203 ).
cnf(c_0_3045,plain,
( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e22,e23) = e22
| op2(e23,e23) = e22 ),
i_0_67 ).
cnf(c_0_3046,plain,
( op2(e22,e20) = e21
| op2(e21,e20) = e21
| h1(e10) = e21 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3025,c_0_2897]),c_0_2894]),c_0_3026]) ).
cnf(c_0_3047,plain,
op2(e21,e23) != op2(e21,e20),
i_0_160 ).
cnf(c_0_3048,plain,
( op2(e21,e23) = e21
| e23 = h4(e10) ),
inference(sr,[status(thm)],[c_0_3027,c_0_3028]) ).
cnf(c_0_3049,plain,
( h3(e10) != e21
| e23 != h4(e10) ),
inference(spm,[status(thm)],[c_0_3029,c_0_3030]) ).
cnf(c_0_3050,plain,
( h3(e10) = e20
| e23 = h4(e10) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_3031,c_0_3032]),c_0_2933]) ).
cnf(c_0_3051,plain,
( e23 = h4(e10)
| e23 != h3(e10) ),
inference(spm,[status(thm)],[c_0_3033,c_0_3031]) ).
cnf(c_0_3052,plain,
( e23 = h3(e10)
| h3(e10) = e21
| h3(e10) = e20 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3034,c_0_2930]),c_0_2930]),c_0_2930]),c_0_2930]),c_0_2969]) ).
cnf(c_0_3053,plain,
op2(e23,e22) != op2(e23,e20),
i_0_149 ).
cnf(c_0_3054,plain,
( op2(e20,e20) = e21
| op2(e20,e21) = e21
| op2(e20,e22) = e21
| op2(e20,e23) = e21 ),
i_0_94 ).
cnf(c_0_3055,plain,
( h4(e10) = h4(e12)
| h4(e10) = e20 ),
inference(spm,[status(thm)],[c_0_2993,c_0_3035]) ).
cnf(c_0_3056,plain,
op2(op2(e21,e21),e21) = h2(e13),
i_0_249 ).
cnf(c_0_3057,plain,
( op1(e13,e13) = e10
| op1(e13,e12) != e13 ),
inference(spm,[status(thm)],[c_0_3022,c_0_2902]) ).
cnf(c_0_3058,plain,
( op1(e12,e12) = e13
| op1(e12,e13) = e13
| op1(e12,e10) = e13 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3036,c_0_2847]),c_0_2861]) ).
cnf(c_0_3059,plain,
op1(e12,e10) = e11,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_3037,c_0_2982]),c_0_2845]) ).
cnf(c_0_3060,plain,
( op1(e12,op1(e12,e13)) != e13
| op1(e12,e12) != e10 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3038,c_0_3039]),c_0_3039]) ).
cnf(c_0_3061,plain,
( op1(e12,e13) = e13
| op1(e12,e12) != e10 ),
inference(spm,[status(thm)],[c_0_3019,c_0_3040]) ).
cnf(c_0_3062,plain,
( op1(e12,e12) = e10
| op1(e12,e13) != e13 ),
inference(spm,[status(thm)],[c_0_3041,c_0_3042]) ).
cnf(c_0_3063,plain,
( op1(e10,e12) = e12
| op1(e11,e12) = e12
| op1(e12,e12) = e12
| op1(e13,e12) = e12 ),
i_0_27 ).
cnf(c_0_3064,plain,
op2(e22,e20) != op2(e20,e20),
i_0_191 ).
cnf(c_0_3065,plain,
( op2(e23,e22) = e20
| h4(e10) = e20 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3043,c_0_2894]),c_0_2900]),c_0_3044]),c_0_2913]) ).
cnf(c_0_3066,plain,
( op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3045,c_0_2900]),c_0_2944]) ).
cnf(c_0_3067,plain,
op2(e22,e21) != op2(e20,e21),
i_0_185 ).
cnf(c_0_3068,plain,
op2(e21,e22) != op2(e21,e20),
i_0_161 ).
cnf(c_0_3069,plain,
( op2(e21,e20) = e21
| op2(e22,e20) = e21 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3046,c_0_2971]),c_0_2934]) ).
cnf(c_0_3070,plain,
( e23 = h4(e10)
| op2(e21,e20) != e21 ),
inference(spm,[status(thm)],[c_0_3047,c_0_3048]) ).
cnf(c_0_3071,plain,
( h3(e10) = e20
| h3(e10) != e21 ),
inference(spm,[status(thm)],[c_0_3049,c_0_3050]) ).
cnf(c_0_3072,plain,
( h4(e10) = h3(e10)
| h3(e10) = e21
| h3(e10) = e20 ),
inference(spm,[status(thm)],[c_0_3051,c_0_3052]) ).
cnf(c_0_3073,plain,
( op2(e23,e22) = e20
| op2(e23,e22) = e21
| op2(e23,e22) = e22
| op2(e23,e22) = e23 ),
i_0_50 ).
cnf(c_0_3074,plain,
op2(e23,e22) != e22,
inference(rw,[status(thm)],[c_0_3053,c_0_2894]) ).
cnf(c_0_3075,plain,
op2(e23,e22) != op2(e23,e21),
i_0_147 ).
cnf(c_0_3076,plain,
op2(op2(e22,e22),e22) = h3(e13),
i_0_253 ).
cnf(c_0_3077,plain,
op2(e21,e23) != op2(e20,e23),
i_0_174 ).
cnf(c_0_3078,plain,
( op2(e20,e23) = e21
| op2(e20,e22) = e21
| h1(e10) = e21 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3054,c_0_2897]),c_0_2879]),c_0_2935]) ).
cnf(c_0_3079,plain,
( h3(e10) = e20
| h4(e10) != e20 ),
inference(spm,[status(thm)],[c_0_3010,c_0_3032]) ).
cnf(c_0_3080,plain,
( h4(e10) = e20
| e21 != h4(e12) ),
inference(spm,[status(thm)],[c_0_2960,c_0_3055]) ).
cnf(c_0_3081,plain,
op2(e21,e21) = h2(e10),
i_0_251 ).
cnf(c_0_3082,plain,
op2(op2(op2(e21,e21),e21),op2(e21,e21)) = h2(e12),
i_0_250 ).
cnf(c_0_3083,negated_conjecture,
( h2(e13) != e23
| ~ epred46_0 ),
i_0_269 ).
cnf(c_0_3084,plain,
h2(e13) = e23,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3056,c_0_2866]),c_0_2879]) ).
cnf(c_0_3085,plain,
( op1(e12,e13) = e13
| op1(e13,e12) != e13 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_3057,c_0_3021]),c_0_2842]) ).
cnf(c_0_3086,plain,
( op1(e10,e10) = e11
| op1(e10,e11) = e11
| op1(e10,e12) = e11
| op1(e10,e13) = e11 ),
i_0_46 ).
cnf(c_0_3087,plain,
op1(e10,e12) != op1(e11,e12),
i_0_132 ).
cnf(c_0_3088,plain,
( op1(e12,e12) = e10
| op1(e11,e12) = e11 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2950,c_0_3042]),c_0_2842]) ).
cnf(c_0_3089,plain,
( op1(e12,e13) = e13
| op1(e12,e12) = e13 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3058,c_0_3059]),c_0_2845]) ).
cnf(c_0_3090,plain,
op1(e12,e13) != e13,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3060,c_0_3061]),c_0_3062]) ).
cnf(c_0_3091,plain,
( op1(e13,e12) = e12
| op1(e10,e12) = e12
| op1(e11,e12) = e12 ),
inference(sr,[status(thm)],[c_0_3063,c_0_2908]) ).
cnf(c_0_3092,plain,
( op1(e12,e13) = e10
| op1(e12,e13) = e11
| op1(e12,e13) = e12
| op1(e12,e13) = e13 ),
i_0_5 ).
cnf(c_0_3093,plain,
op1(e12,e13) != op1(e12,e10),
i_0_106 ).
cnf(c_0_3094,plain,
( op2(e22,e20) = e20
| op2(e22,e20) = e21
| op2(e22,e20) = e22
| op2(e22,e20) = e23 ),
i_0_56 ).
cnf(c_0_3095,plain,
op2(e22,e20) != h1(e10),
inference(rw,[status(thm)],[c_0_3064,c_0_2897]) ).
cnf(c_0_3096,plain,
op2(e21,e23) != op2(e21,e21),
i_0_158 ).
cnf(c_0_3097,plain,
( h4(e10) = e20
| h3(e10) != e20 ),
inference(spm,[status(thm)],[c_0_3033,c_0_3065]) ).
cnf(c_0_3098,plain,
( op2(e20,e23) = e22
| op2(e21,e23) = e22 ),
inference(sr,[status(thm)],[c_0_3066,c_0_3007]) ).
cnf(c_0_3099,plain,
( op2(e22,e20) = e23
| op2(e22,e21) = e23
| op2(e22,e22) = e23
| op2(e22,e23) = e23 ),
i_0_74 ).
cnf(c_0_3100,plain,
op2(e22,e21) != e23,
inference(rw,[status(thm)],[c_0_3067,c_0_2879]) ).
cnf(c_0_3101,plain,
( op2(e22,e20) = e21
| op2(e21,e22) != e21 ),
inference(spm,[status(thm)],[c_0_3068,c_0_3069]) ).
cnf(c_0_3102,plain,
( op2(e22,e20) = e21
| e23 = h4(e10) ),
inference(spm,[status(thm)],[c_0_3070,c_0_3069]) ).
cnf(c_0_3103,plain,
( op2(h3(e10),h3(e10)) = h4(e10)
| h3(e10) = e20 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2900,c_0_3052]),c_0_3071]) ).
cnf(c_0_3104,plain,
( op2(h3(e10),h3(e10)) = h3(e10)
| h3(e10) = e20 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2993,c_0_3072]),c_0_3071]) ).
cnf(c_0_3105,plain,
( op2(e23,e22) = e23
| op2(e23,e22) = e21
| op2(e23,e22) = e20 ),
inference(sr,[status(thm)],[c_0_3073,c_0_3074]) ).
cnf(c_0_3106,plain,
op2(e23,e22) != e21,
inference(rw,[status(thm)],[c_0_3075,c_0_2932]) ).
cnf(c_0_3107,plain,
op2(op2(op2(e22,e22),e22),op2(e22,e22)) = h3(e12),
i_0_254 ).
cnf(c_0_3108,plain,
op2(h3(e10),e22) = h3(e13),
inference(rw,[status(thm)],[c_0_3076,c_0_2930]) ).
cnf(c_0_3109,plain,
( e23 = h4(e10)
| op2(e20,e23) != e21 ),
inference(spm,[status(thm)],[c_0_3077,c_0_3048]) ).
cnf(c_0_3110,plain,
( op2(e20,e22) = e21
| op2(e20,e23) = e21 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3078,c_0_2971]),c_0_2934]) ).
cnf(c_0_3111,plain,
( h3(e10) = e20
| e21 != h4(e12) ),
inference(spm,[status(thm)],[c_0_3079,c_0_3080]) ).
cnf(c_0_3112,plain,
( op2(e20,e20) = e23
| op2(e21,e20) = e23
| op2(e22,e20) = e23
| op2(e23,e20) = e23 ),
i_0_89 ).
cnf(c_0_3113,plain,
op2(e20,e23) != op2(e20,e21),
i_0_164 ).
cnf(c_0_3114,plain,
( epred46_0
| h2(e10) != e20
| h2(e11) != e21
| h2(e12) != e22
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e13)) != h2(op1(e10,e13))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e13)) != h2(op1(e12,e13))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e12)) != h2(op1(e13,e12))
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) ),
i_0_2696 ).
cnf(c_0_3115,plain,
h2(e11) = e21,
i_0_252 ).
cnf(c_0_3116,plain,
h2(e10) = e20,
inference(rw,[status(thm)],[c_0_3081,c_0_2866]) ).
cnf(c_0_3117,plain,
h2(e12) = e22,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3082,c_0_2866]),c_0_2879]),c_0_2866]),c_0_2894]) ).
cnf(c_0_3118,negated_conjecture,
~ epred46_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3083,c_0_3084])]) ).
cnf(c_0_3119,plain,
( op1(e11,e12) = e11
| op1(e12,e13) = e13 ),
inference(spm,[status(thm)],[c_0_3085,c_0_2950]) ).
cnf(c_0_3120,plain,
( op1(e10,e12) = e11
| op1(e10,e13) = e11
| op1(e10,e10) = e11 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3086,c_0_2839]),c_0_2845]) ).
cnf(c_0_3121,plain,
( op1(e12,e12) = e10
| op1(e10,e12) != e11 ),
inference(spm,[status(thm)],[c_0_3087,c_0_3088]) ).
cnf(c_0_3122,plain,
op1(e12,e12) = e13,
inference(sr,[status(thm)],[c_0_3089,c_0_3090]) ).
cnf(c_0_3123,plain,
( op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(sr,[status(thm)],[c_0_3091,c_0_2906]) ).
cnf(c_0_3124,plain,
( op1(e12,e13) = e13
| op1(e12,e13) = e10
| op1(e12,e13) = e11 ),
inference(sr,[status(thm)],[c_0_3092,c_0_2883]) ).
cnf(c_0_3125,plain,
op1(e12,e13) != e11,
inference(rw,[status(thm)],[c_0_3093,c_0_3059]) ).
cnf(c_0_3126,plain,
op2(e22,e22) != op2(e22,e20),
i_0_155 ).
cnf(c_0_3127,plain,
( op2(e22,e20) = e23
| op2(e22,e20) = e21
| op2(e22,e20) = e20 ),
inference(sr,[status(thm)],[c_0_3094,c_0_2938]) ).
cnf(c_0_3128,plain,
op2(e22,e20) != e20,
inference(rw,[status(thm)],[c_0_3095,c_0_2971]) ).
cnf(c_0_3129,plain,
( op2(e20,e22) = e22
| op2(e21,e22) = e22
| op2(e22,e22) = e22
| op2(e23,e22) = e22 ),
i_0_75 ).
cnf(c_0_3130,plain,
( op2(e20,e23) = e20
| op2(e21,e23) = e20
| op2(e22,e23) = e20
| op2(e23,e23) = e20 ),
i_0_71 ).
cnf(c_0_3131,plain,
op2(e21,e23) != e20,
inference(rw,[status(thm)],[c_0_3096,c_0_2866]) ).
cnf(c_0_3132,plain,
( op2(e20,e23) = h4(e13)
| h3(e10) != e20 ),
inference(spm,[status(thm)],[c_0_2974,c_0_3097]) ).
cnf(c_0_3133,plain,
( op2(e20,e23) = e22
| e23 = h4(e10) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_3098,c_0_3048]),c_0_3026]) ).
cnf(c_0_3134,plain,
op2(e23,e23) != op2(e22,e23),
i_0_169 ).
cnf(c_0_3135,plain,
( op2(e22,e23) = e23
| op2(e22,e20) = e23
| e23 = h3(e10) ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3099,c_0_2930]),c_0_3100]) ).
cnf(c_0_3136,plain,
op2(e22,e20) = e21,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3101,c_0_3030]),c_0_3102]) ).
cnf(c_0_3137,plain,
( op2(h4(e10),e22) = e20
| h4(e10) = e20 ),
inference(spm,[status(thm)],[c_0_3065,c_0_2973]) ).
cnf(c_0_3138,plain,
( h4(e10) = h3(e10)
| h3(e10) = e20 ),
inference(spm,[status(thm)],[c_0_3103,c_0_3104]) ).
cnf(c_0_3139,plain,
( op2(e23,e22) = e20
| op2(e23,e22) = e23 ),
inference(sr,[status(thm)],[c_0_3105,c_0_3106]) ).
cnf(c_0_3140,plain,
op2(h3(e13),h3(e10)) = h3(e12),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3107,c_0_2930]),c_0_3108]),c_0_2930]) ).
cnf(c_0_3141,plain,
( op2(e20,e22) = e21
| e23 = h4(e10) ),
inference(spm,[status(thm)],[c_0_3109,c_0_3110]) ).
cnf(c_0_3142,plain,
( op2(e20,e22) = h3(e13)
| e21 != h4(e12) ),
inference(spm,[status(thm)],[c_0_3108,c_0_3111]) ).
cnf(c_0_3143,plain,
( op2(e22,e20) = e23
| op2(e21,e20) = e23 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3112,c_0_2897]),c_0_2894]),c_0_2942]),c_0_2939]) ).
cnf(c_0_3144,plain,
( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e22
| op2(e20,e23) = e23 ),
i_0_61 ).
cnf(c_0_3145,plain,
op2(e20,e23) != e23,
inference(rw,[status(thm)],[c_0_3113,c_0_2879]) ).
cnf(c_0_3146,plain,
( op2(e21,e20) != h2(op1(e11,e10))
| op2(e21,e23) != h2(op1(e11,e13))
| op2(e21,e22) != h2(op1(e11,e12))
| op2(e20,e23) != h2(op1(e10,e13))
| op2(e20,e22) != h2(op1(e10,e12))
| op2(e23,e22) != h2(op1(e13,e12))
| op2(e22,e20) != h2(op1(e12,e10))
| op2(e22,e23) != h2(op1(e12,e13))
| h2(op1(e10,e10)) != h1(e10)
| h2(op1(e13,e13)) != h4(e10)
| h2(op1(e12,e12)) != h3(e10) ),
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)],[c_0_3114,c_0_3115]),c_0_3116]),c_0_3117]),c_0_3115]),c_0_3115]),c_0_2866]),c_0_2837]),c_0_3116]),c_0_3115]),c_0_3116]),c_0_3115]),c_0_3084]),c_0_3115]),c_0_3117]),c_0_3116]),c_0_3115]),c_0_2879]),c_0_2839]),c_0_3084]),c_0_3116]),c_0_3116]),c_0_2897]),c_0_3116]),c_0_3084]),c_0_3116]),c_0_3117]),c_0_3084]),c_0_3115]),c_0_2932]),c_0_2859]),c_0_3115]),c_0_3084]),c_0_3116]),c_0_2894]),c_0_2857]),c_0_3117]),c_0_3084]),c_0_3084]),c_0_2900]),c_0_3084]),c_0_3117]),c_0_3117]),c_0_3115]),c_0_2954]),c_0_2847]),c_0_3117]),c_0_3117]),c_0_3116]),c_0_3117]),c_0_3084]),c_0_3117]),c_0_3117]),c_0_2930])]),c_0_3118]) ).
cnf(c_0_3147,plain,
op1(e11,e12) = e11,
inference(sr,[status(thm)],[c_0_3119,c_0_3090]) ).
cnf(c_0_3148,plain,
( op1(e10,e13) = e11
| op1(e10,e12) = e11 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3120,c_0_2885]),c_0_2841]) ).
cnf(c_0_3149,plain,
op1(e10,e12) != e11,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3121,c_0_3122]),c_0_2842]) ).
cnf(c_0_3150,plain,
( op1(e12,e12) = e10
| op1(e10,e12) = e12 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_3123,c_0_3088]),c_0_2851]) ).
cnf(c_0_3151,plain,
op1(e12,e12) != e10,
inference(spm,[status(thm)],[c_0_3090,c_0_3061]) ).
cnf(c_0_3152,plain,
( op1(e12,e13) = e10
| op1(e12,e13) = e13 ),
inference(sr,[status(thm)],[c_0_3124,c_0_3125]) ).
cnf(c_0_3153,plain,
op2(e22,e20) != h3(e10),
inference(rw,[status(thm)],[c_0_3126,c_0_2930]) ).
cnf(c_0_3154,plain,
( op2(e22,e20) = e21
| op2(e22,e20) = e23 ),
inference(sr,[status(thm)],[c_0_3127,c_0_3128]) ).
cnf(c_0_3155,plain,
( op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3129,c_0_2930]),c_0_2969]),c_0_3074]) ).
cnf(c_0_3156,plain,
( op2(e21,e22) = e21
| e23 != h3(e10) ),
inference(spm,[status(thm)],[c_0_3033,c_0_3011]) ).
cnf(c_0_3157,plain,
op2(e23,e23) != op2(e21,e23),
i_0_170 ).
cnf(c_0_3158,plain,
( op2(e21,e23) = e20
| op2(e21,e23) = e21
| op2(e21,e23) = e22
| op2(e21,e23) = e23 ),
i_0_57 ).
cnf(c_0_3159,plain,
( op2(e22,e23) = e20
| op2(e22,e23) = e21
| op2(e22,e23) = e22
| op2(e22,e23) = e23 ),
i_0_53 ).
cnf(c_0_3160,plain,
op2(e22,e23) != op2(e22,e20),
i_0_154 ).
cnf(c_0_3161,plain,
op2(e22,e22) != op2(e20,e22),
i_0_179 ).
cnf(c_0_3162,plain,
( op2(e22,e23) = e20
| op2(e20,e23) = e20
| h4(e10) = e20 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3130,c_0_2900]),c_0_3131]) ).
cnf(c_0_3163,plain,
( op2(h4(e13),e20) = h4(e12)
| h3(e10) != e20 ),
inference(spm,[status(thm)],[c_0_3015,c_0_3097]) ).
cnf(c_0_3164,plain,
( e23 = h4(e10)
| h4(e13) = e22 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3132,c_0_3133]),c_0_3050]) ).
cnf(c_0_3165,plain,
op2(e22,e23) != h4(e10),
inference(rw,[status(thm)],[c_0_3134,c_0_2900]) ).
cnf(c_0_3166,plain,
( op2(e22,e23) = e23
| e23 = h3(e10) ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3135,c_0_3136]),c_0_2935]) ).
cnf(c_0_3167,plain,
op2(e20,e23) != op2(e20,e22),
i_0_163 ).
cnf(c_0_3168,plain,
( h3(e10) = e20
| h3(e13) = e20 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3137,c_0_3138]),c_0_3108]) ).
cnf(c_0_3169,plain,
( op2(e23,e22) = e20
| e23 != h4(e10) ),
inference(spm,[status(thm)],[c_0_3010,c_0_3139]) ).
cnf(c_0_3170,plain,
( op2(h3(e13),e20) = h3(e12)
| e21 != h4(e12) ),
inference(spm,[status(thm)],[c_0_3140,c_0_3111]) ).
cnf(c_0_3171,plain,
( e23 = h4(e10)
| h3(e13) = e21
| e21 != h4(e12) ),
inference(spm,[status(thm)],[c_0_3141,c_0_3142]) ).
cnf(c_0_3172,plain,
op2(e21,e20) = e23,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3143,c_0_3136]),c_0_2935]) ).
cnf(c_0_3173,plain,
( h4(e10) = e20
| h4(e12) != e20 ),
inference(ef,[status(thm)],[c_0_3055]) ).
cnf(c_0_3174,plain,
( op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 ),
inference(sr,[status(thm)],[c_0_3144,c_0_3145]) ).
cnf(c_0_3175,plain,
( op2(e21,e23) != h2(op1(e11,e13))
| op2(e21,e22) != h2(op1(e11,e12))
| op2(e20,e23) != h2(op1(e10,e13))
| op2(e20,e22) != h2(op1(e10,e12))
| op2(e23,e22) != h2(op1(e13,e12))
| op2(e22,e23) != h2(op1(e12,e13))
| h2(op1(e13,e13)) != h4(e10)
| h2(op1(e12,e12)) != h3(e10)
| op2(e21,e20) != e23
| op2(e22,e20) != e21 ),
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_3146,c_0_2982]),c_0_3084]),c_0_3059]),c_0_3115]),c_0_2885]),c_0_3116]),c_0_2971])]) ).
cnf(c_0_3176,plain,
op1(e11,e13) = e12,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_2999,c_0_3147]),c_0_2851]) ).
cnf(c_0_3177,plain,
op1(e10,e13) = e11,
inference(sr,[status(thm)],[c_0_3148,c_0_3149]) ).
cnf(c_0_3178,plain,
op1(e10,e12) = e12,
inference(sr,[status(thm)],[c_0_3150,c_0_3151]) ).
cnf(c_0_3179,plain,
op1(e13,e12) = e10,
inference(sr,[status(thm)],[c_0_3040,c_0_3090]) ).
cnf(c_0_3180,plain,
op1(e12,e13) = e10,
inference(sr,[status(thm)],[c_0_3152,c_0_3090]) ).
cnf(c_0_3181,plain,
op1(e13,e13) = e13,
inference(sr,[status(thm)],[c_0_3021,c_0_3090]) ).
cnf(c_0_3182,plain,
( op2(e22,e20) = e21
| e23 != h3(e10) ),
inference(spm,[status(thm)],[c_0_3153,c_0_3154]) ).
cnf(c_0_3183,plain,
( op2(e23,e22) = e20
| e23 != h3(e10) ),
inference(spm,[status(thm)],[c_0_3033,c_0_3139]) ).
cnf(c_0_3184,plain,
( op2(e20,e22) = e22
| e23 != h3(e10) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_3155,c_0_3156]),c_0_3026]) ).
cnf(c_0_3185,plain,
op2(e21,e23) != h4(e10),
inference(rw,[status(thm)],[c_0_3157,c_0_2900]) ).
cnf(c_0_3186,plain,
( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21 ),
inference(sr,[status(thm)],[c_0_3158,c_0_3131]) ).
cnf(c_0_3187,plain,
op2(e22,e23) != op2(e22,e22),
i_0_151 ).
cnf(c_0_3188,plain,
( op2(e22,e23) = e20
| op2(e22,e23) = e21
| op2(e22,e23) = e23 ),
inference(sr,[status(thm)],[c_0_3159,c_0_3007]) ).
cnf(c_0_3189,plain,
op2(e22,e23) != e21,
inference(rw,[status(thm)],[c_0_3160,c_0_3136]) ).
cnf(c_0_3190,plain,
op2(e20,e22) != h3(e10),
inference(rw,[status(thm)],[c_0_3161,c_0_2930]) ).
cnf(c_0_3191,plain,
( op2(e22,e23) = e20
| h4(e10) = e20 ),
inference(sr,[status(thm)],[c_0_3162,c_0_3028]) ).
cnf(c_0_3192,plain,
( e23 = h4(e10)
| e21 = h4(e12) ),
inference(csr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3163,c_0_3164]),c_0_3136]),c_0_3050]) ).
cnf(c_0_3193,plain,
( e23 = h3(e10)
| e23 != h4(e10) ),
inference(spm,[status(thm)],[c_0_3165,c_0_3166]) ).
cnf(c_0_3194,plain,
( h3(e10) = e20
| op2(e20,h3(e10)) != op2(e20,e22) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3167,c_0_3052]),c_0_3071]) ).
cnf(c_0_3195,plain,
( op2(e20,h3(e10)) = h3(e12)
| h3(e10) = e20 ),
inference(spm,[status(thm)],[c_0_3140,c_0_3168]) ).
cnf(c_0_3196,plain,
( h3(e10) != e20
| e23 != h4(e10) ),
inference(spm,[status(thm)],[c_0_3033,c_0_3169]) ).
cnf(c_0_3197,plain,
( e23 = h4(e10)
| e23 = h3(e12)
| e21 != h4(e12) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3170,c_0_3171]),c_0_3172]) ).
cnf(c_0_3198,plain,
( op2(e20,e23) = h4(e13)
| h4(e12) != e20 ),
inference(spm,[status(thm)],[c_0_2974,c_0_3173]) ).
cnf(c_0_3199,plain,
( op2(e20,e23) = e21
| op2(e20,e23) = e22 ),
inference(sr,[status(thm)],[c_0_3174,c_0_3028]) ).
cnf(c_0_3200,plain,
( op2(e21,e23) != e22
| op2(e20,e23) != e21
| op2(e22,e23) != e20
| op2(e21,e20) != e23
| e23 != h3(e10) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[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_3175,c_0_3122]),c_0_3084]),c_0_3176]),c_0_3117]),c_0_3147]),c_0_3115]),c_0_3177]),c_0_3115]),c_0_3178]),c_0_3117]),c_0_3179]),c_0_3116]),c_0_3180]),c_0_3116]),c_0_3181]),c_0_3084]),c_0_3051]),c_0_3182]),c_0_3183]),c_0_3184]),c_0_3156]) ).
cnf(c_0_3201,plain,
( op2(e21,e23) = e22
| op2(e21,e23) = e21 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3185,c_0_3186]),c_0_3048]) ).
cnf(c_0_3202,plain,
op2(e22,e23) != h3(e10),
inference(rw,[status(thm)],[c_0_3187,c_0_2930]) ).
cnf(c_0_3203,plain,
( op2(e22,e23) = e20
| op2(e22,e23) = e23 ),
inference(sr,[status(thm)],[c_0_3188,c_0_3189]) ).
cnf(c_0_3204,plain,
h3(e10) != e21,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3190,c_0_3141]),c_0_3049]) ).
cnf(c_0_3205,plain,
( e23 = h3(e10)
| h4(e10) = e20 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_3191,c_0_3166]),c_0_2933]) ).
cnf(c_0_3206,plain,
( e21 = h4(e12)
| op2(e22,h4(e10)) != e21 ),
inference(spm,[status(thm)],[c_0_3189,c_0_3192]) ).
cnf(c_0_3207,plain,
( h4(e10) = h3(e10)
| e21 = h4(e12) ),
inference(spm,[status(thm)],[c_0_3193,c_0_3192]) ).
cnf(c_0_3208,plain,
( h3(e10) = e20
| op2(e20,e22) != h3(e12) ),
inference(spm,[status(thm)],[c_0_3194,c_0_3195]) ).
cnf(c_0_3209,plain,
( op2(e20,e22) = e22
| e23 != h4(e10) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_3155,c_0_3030]),c_0_3026]) ).
cnf(c_0_3210,plain,
( e23 = h3(e12)
| e21 != h4(e12) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3196,c_0_3197]),c_0_3111]) ).
cnf(c_0_3211,plain,
( h4(e10) = e20
| h3(e10) != e21 ),
inference(spm,[status(thm)],[c_0_3049,c_0_2973]) ).
cnf(c_0_3212,plain,
( op2(e20,e23) = e22
| h4(e13) = e21
| h4(e12) != e20 ),
inference(spm,[status(thm)],[c_0_3198,c_0_3199]) ).
cnf(c_0_3213,plain,
( op2(e21,e23) != e22
| op2(e20,e23) != e21
| op2(e22,e23) != e20
| e23 != h3(e10) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3200,c_0_3172])]) ).
cnf(c_0_3214,plain,
( op2(e21,e23) = e22
| op2(e20,e23) != e21 ),
inference(spm,[status(thm)],[c_0_3077,c_0_3201]) ).
cnf(c_0_3215,plain,
( op2(e22,e23) = e20
| e23 != h3(e10) ),
inference(spm,[status(thm)],[c_0_3202,c_0_3203]) ).
cnf(c_0_3216,plain,
( e23 = h3(e10)
| h3(e10) = e20 ),
inference(sr,[status(thm)],[c_0_3052,c_0_3204]) ).
cnf(c_0_3217,plain,
( h4(e10) = e20
| h3(e13) = e20 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3065,c_0_3205]),c_0_3108]) ).
cnf(c_0_3218,plain,
( e21 = h4(e12)
| op2(e22,h3(e10)) != e21 ),
inference(spm,[status(thm)],[c_0_3206,c_0_3207]) ).
cnf(c_0_3219,plain,
( h3(e10) = e20
| h3(e12) != e22 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3208,c_0_3209]),c_0_3050]) ).
cnf(c_0_3220,plain,
( h3(e12) != e22
| e21 != h4(e12) ),
inference(spm,[status(thm)],[c_0_2939,c_0_3210]) ).
cnf(c_0_3221,plain,
op2(e23,e20) != op2(e21,e20),
i_0_188 ).
cnf(c_0_3222,plain,
( h3(e10) = h4(e12)
| h4(e10) = e20
| h3(e10) = e21 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3072,c_0_3055]),c_0_3097]) ).
cnf(c_0_3223,plain,
( op2(e20,e23) = h4(e13)
| h3(e10) != e21 ),
inference(spm,[status(thm)],[c_0_2974,c_0_3211]) ).
cnf(c_0_3224,plain,
( op2(h4(e13),e20) = h4(e12)
| h4(e12) != e20 ),
inference(spm,[status(thm)],[c_0_3015,c_0_3173]) ).
cnf(c_0_3225,plain,
( h4(e13) = e21
| h4(e13) = e22
| h4(e12) != e20 ),
inference(spm,[status(thm)],[c_0_3198,c_0_3212]) ).
cnf(c_0_3226,plain,
( op2(e20,e23) != e21
| e23 != h3(e10) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3213,c_0_3214]),c_0_3215]) ).
cnf(c_0_3227,plain,
( op2(e20,h3(e10)) = e22
| op2(e20,h3(e10)) = e21
| h3(e10) = e20 ),
inference(spm,[status(thm)],[c_0_3199,c_0_3216]) ).
cnf(c_0_3228,plain,
( op2(e20,h3(e10)) = h3(e12)
| h4(e10) = e20 ),
inference(spm,[status(thm)],[c_0_3140,c_0_3217]) ).
cnf(c_0_3229,plain,
h3(e12) != e22,
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3218,c_0_3219]),c_0_3136])]),c_0_3220]) ).
cnf(c_0_3230,plain,
( op2(e21,e20) = e22
| op2(e21,e21) = e22
| op2(e21,e22) = e22
| op2(e21,e23) = e22 ),
i_0_84 ).
cnf(c_0_3231,plain,
op2(e21,e20) != e22,
inference(rw,[status(thm)],[c_0_3221,c_0_2894]) ).
cnf(c_0_3232,plain,
( op2(e20,e23) = h4(e13)
| h3(e10) = h4(e12) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2974,c_0_3222]),c_0_3223]) ).
cnf(c_0_3233,plain,
( h3(e10) = h4(e12)
| h3(e10) = e21
| h3(e10) = e20 ),
inference(spm,[status(thm)],[c_0_3072,c_0_3222]) ).
cnf(c_0_3234,plain,
( h4(e13) = e22
| e23 = h4(e12)
| h4(e12) != e20 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3224,c_0_3225]),c_0_3172]) ).
cnf(c_0_3235,plain,
( e21 = h4(e12)
| op2(e20,h4(e10)) != e20 ),
inference(spm,[status(thm)],[c_0_3028,c_0_3192]) ).
cnf(c_0_3236,plain,
( h3(e10) = e20
| op2(e20,h3(e10)) != e21 ),
inference(spm,[status(thm)],[c_0_3226,c_0_3216]) ).
cnf(c_0_3237,plain,
( h3(e10) = e20
| e21 = h3(e12) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_3227,c_0_3228]),c_0_3229]),c_0_3079]) ).
cnf(c_0_3238,plain,
( op2(e20,op2(e20,e20)) != e20
| op2(e21,op2(e21,e22)) != e22
| op2(e22,op2(e22,e23)) != e23
| ~ epred23_0 ),
i_0_1478 ).
cnf(c_0_3239,plain,
( epred23_0
| op2(e23,op2(e23,e21)) != e21 ),
i_0_233 ).
cnf(c_0_3240,plain,
( op2(e21,e23) = e22
| op2(e21,e22) = e22 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3230,c_0_2866]),c_0_3231]),c_0_3044]) ).
cnf(c_0_3241,plain,
( h4(e13) != e21
| h3(e10) != e20 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3109,c_0_3132]),c_0_3196]) ).
cnf(c_0_3242,plain,
( h3(e10) = h4(e12)
| h4(e13) = e22
| h4(e13) = e21 ),
inference(spm,[status(thm)],[c_0_3199,c_0_3232]) ).
cnf(c_0_3243,plain,
( h3(e10) = h4(e12)
| h3(e10) = e20 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_3071,c_0_3233]),c_0_2934]) ).
cnf(c_0_3244,plain,
( e23 = h4(e12)
| e21 = h4(e12)
| h4(e12) != e20 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3224,c_0_3234]),c_0_3136]) ).
cnf(c_0_3245,plain,
( e21 = h4(e12)
| op2(e20,h3(e10)) != e20 ),
inference(spm,[status(thm)],[c_0_3235,c_0_3207]) ).
cnf(c_0_3246,plain,
h3(e10) = e20,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3236,c_0_3195]),c_0_3237]) ).
cnf(c_0_3247,plain,
( op2(e21,op2(e21,e22)) != e22
| op2(e22,op2(e22,e23)) != e23
| op2(e20,h1(e10)) != e20
| ~ epred23_0 ),
inference(rw,[status(thm)],[c_0_3238,c_0_2897]) ).
cnf(c_0_3248,plain,
epred23_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3239,c_0_2932]),c_0_2932])]) ).
cnf(c_0_3249,plain,
( op2(e21,e22) = e22
| op2(e20,e23) != e22 ),
inference(spm,[status(thm)],[c_0_3077,c_0_3240]) ).
cnf(c_0_3250,plain,
( h3(e10) = h4(e12)
| h4(e13) = e22 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3241,c_0_3242]),c_0_3243]) ).
cnf(c_0_3251,plain,
( e21 = h4(e12)
| h4(e12) != e20 ),
inference(spm,[status(thm)],[c_0_2933,c_0_3244]) ).
cnf(c_0_3252,plain,
e21 = h4(e12),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3245,c_0_3246]),c_0_2897]),c_0_2971])]) ).
cnf(c_0_3253,plain,
( op2(e21,op2(e21,e22)) != e22
| op2(e22,op2(e22,e23)) != e23
| op2(e20,h1(e10)) != e20 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3247,c_0_3248])]) ).
cnf(c_0_3254,plain,
( h3(e10) = h4(e12)
| op2(e21,e22) = e22 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_3249,c_0_3232]),c_0_3250]) ).
cnf(c_0_3255,plain,
h4(e12) != e20,
inference(spm,[status(thm)],[c_0_2934,c_0_3251]) ).
cnf(c_0_3256,plain,
e23 = h3(e12),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3210,c_0_3252])]) ).
cnf(c_0_3257,plain,
( op2(e21,op2(e21,e22)) != e22
| op2(e22,op2(e22,e23)) != e23 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_3253,c_0_2971]),c_0_2897]),c_0_2971])]) ).
cnf(c_0_3258,plain,
op2(h4(e12),e22) = e22,
inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3254,c_0_3246]),c_0_3255]),c_0_3252]) ).
cnf(c_0_3259,plain,
op2(e22,h3(e12)) = h3(e12),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_3166,c_0_3246]),c_0_2933]),c_0_3256]),c_0_3256]) ).
cnf(c_0_3260,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)],[c_0_3257,c_0_3252]),c_0_3252]),c_0_3258]),c_0_3258]),c_0_3256]),c_0_3259]),c_0_3259]),c_0_3256])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ALG118+1 : TPTP v8.1.0. Released v2.7.0.
% 0.03/0.13 % Command : enigmatic-eprover.py %s %d 1
% 0.13/0.34 % Computer : n023.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Wed Jun 8 08:26:10 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.19/0.45 # ENIGMATIC: Selected complete mode:
% 13.82/3.60 # ENIGMATIC: Solved by autoschedule:
% 13.82/3.60 # No SInE strategy applied
% 13.82/3.60 # Trying AutoSched0 for 150 seconds
% 13.82/3.60 # AutoSched0-Mode selected heuristic C07_19_nc_SAT001_MinMin_rr
% 13.82/3.60 # and selection function SelectMaxLComplexAvoidPosPred.
% 13.82/3.60 #
% 13.82/3.60 # Preprocessing time : 0.110 s
% 13.82/3.60 # Presaturation interreduction done
% 13.82/3.60
% 13.82/3.60 # Proof found!
% 13.82/3.60 # SZS status Theorem
% 13.82/3.60 # SZS output start CNFRefutation
% See solution above
% 13.82/3.60 # Training examples: 0 positive, 0 negative
% 13.82/3.60
% 13.82/3.60 # -------------------------------------------------
% 13.82/3.60 # User time : 0.652 s
% 13.82/3.60 # System time : 0.016 s
% 13.82/3.60 # Total time : 0.668 s
% 13.82/3.60 # Maximum resident set size: 7124 pages
% 13.82/3.60
%------------------------------------------------------------------------------