%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : ALG067+1 : TPTP v9.0.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 09:45:47 AM UTC 2025
% Result : Theorem 59.61s 7.84s
% Output : CNFRefutation 59.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 1
% Syntax : Number of formulae : 342 ( 1 unt; 0 def)
% Number of atoms : 1090 ( 684 equ)
% Maximal formula atoms : 125 ( 3 avg)
% Number of connectives : 1301 ( 553 ~; 598 |; 150 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 55 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 25 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co1,plain,
~ ( ( op(e0,e0) != e0
| op(e0,e0) = e0 )
& ( op(e0,e0) != e1
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e0,e2) = e0 )
& ( op(e0,e0) != e3
| op(e0,e3) = e0 )
& ( op(e0,e0) != e4
| op(e0,e4) = e0 )
& ( op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e1,e1) != e1
| op(e1,e1) = e1 )
& ( op(e1,e1) != e2
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e1,e3) = e1 )
& ( op(e1,e1) != e4
| op(e1,e4) = e1 )
& ( op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e2,e2) != e2
| op(e2,e2) = e2 )
& ( op(e2,e2) != e3
| op(e2,e3) = e2 )
& ( op(e2,e2) != e4
| op(e2,e4) = e2 )
& ( op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e3,e3) != e3
| op(e3,e3) = e3 )
& ( op(e3,e3) != e4
| op(e3,e4) = e3 )
& ( op(e4,e4) != e0
| op(e4,e0) = e4 )
& ( op(e4,e4) != e1
| op(e4,e1) = e4 )
& ( op(e4,e4) != e2
| op(e4,e2) = e4 )
& ( op(e4,e4) != e3
| op(e4,e3) = e4 )
& ( op(e4,e4) != e4
| op(e4,e4) = e4 )
& ( ( op(e0,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(co1_negated,plain,
~ ~ ( ( op(e0,e0) != e0
| op(e0,e0) = e0 )
& ( op(e0,e0) != e1
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e0,e2) = e0 )
& ( op(e0,e0) != e3
| op(e0,e3) = e0 )
& ( op(e0,e0) != e4
| op(e0,e4) = e0 )
& ( op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e1,e1) != e1
| op(e1,e1) = e1 )
& ( op(e1,e1) != e2
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e1,e3) = e1 )
& ( op(e1,e1) != e4
| op(e1,e4) = e1 )
& ( op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e2,e2) != e2
| op(e2,e2) = e2 )
& ( op(e2,e2) != e3
| op(e2,e3) = e2 )
& ( op(e2,e2) != e4
| op(e2,e4) = e2 )
& ( op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e3,e3) != e3
| op(e3,e3) = e3 )
& ( op(e3,e3) != e4
| op(e3,e4) = e3 )
& ( op(e4,e4) != e0
| op(e4,e0) = e4 )
& ( op(e4,e4) != e1
| op(e4,e1) = e4 )
& ( op(e4,e4) != e2
| op(e4,e2) = e4 )
& ( op(e4,e4) != e3
| op(e4,e3) = e4 )
& ( op(e4,e4) != e4
| op(e4,e4) = e4 )
& ( ( op(e0,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 ) ) ),
inference(negate_conjecture,[status(cth)],[co1]) ).
cnf(199,plain,
( op(e0,e0) != e1
| op(e0,e1) = e0 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l0,plain,
( op(e0,e0) != e1
| op(e0,e1) = e0 ),
inference(instantiation,[status(thm)],[199]) ).
cnf(280,plain,
( op(e0,e0) = e1
| ~ sP4 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1,plain,
( op(e0,e0) = e1
| ~ sP4 ),
inference(instantiation,[status(thm)],[280]) ).
cnf(291,plain,
( op(e0,e1) != e0
| ~ sP0 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l2,plain,
( op(e0,e1) != e0
| ~ sP0 ),
inference(instantiation,[status(thm)],[291]) ).
cnf(221,plain,
( op(e0,e0) != e0
| sP10
| sP11
| sP12
| sP13
| sP4
| sP5
| sP6
| sP14
| sP15
| sP16
| sP7
| sP17
| sP8
| sP9
| sP1
| sP2
| sP3
| sP0
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l3,plain,
( op(e0,e0) != e0
| sP10
| sP11
| sP12
| sP13
| sP4
| sP5
| sP6
| sP14
| sP15
| sP16
| sP7
| sP17
| sP8
| sP9
| sP1
| sP2
| sP3
| sP0
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23 ),
inference(instantiation,[status(thm)],[221]) ).
cnf(264,plain,
( op(e2,e0) != e2
| ~ sP9 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l48,plain,
( op(e2,e0) != e2
| ~ sP9 ),
inference(instantiation,[status(thm)],[264]) ).
cnf(248,plain,
( op(e3,e3) = e1
| ~ sP15 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l84,plain,
( op(e3,e3) = e1
| ~ sP15 ),
inference(instantiation,[status(thm)],[248]) ).
cnf(230,plain,
( op(e4,e4) = e2
| ~ sP21 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l61,plain,
( op(e4,e4) = e2
| ~ sP21 ),
inference(instantiation,[status(thm)],[230]) ).
cnf(224,plain,
( op(e4,e4) = e4
| ~ sP23 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l62,plain,
( op(e4,e4) = e4
| ~ sP23 ),
inference(instantiation,[status(thm)],[224]) ).
cnf(270,plain,
( op(e1,e3) != e1
| ~ sP7 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l132,plain,
( op(e1,e3) != e1
| ~ sP7 ),
inference(instantiation,[status(thm)],[270]) ).
cnf(217,plain,
( op(e4,e4) != e2
| op(e4,e2) = e4 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l79,plain,
( op(e4,e4) != e2
| op(e4,e2) = e4 ),
inference(instantiation,[status(thm)],[217]) ).
cnf(231,plain,
( op(e4,e1) != e4
| ~ sP20 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l60,plain,
( op(e4,e1) != e4
| ~ sP20 ),
inference(instantiation,[status(thm)],[231]) ).
cnf(225,plain,
( op(e4,e3) != e4
| ~ sP22 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l57,plain,
( op(e4,e3) != e4
| ~ sP22 ),
inference(instantiation,[status(thm)],[225]) ).
cnf(236,plain,
( op(e4,e4) = e0
| ~ sP19 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l54,plain,
( op(e4,e4) = e0
| ~ sP19 ),
inference(instantiation,[status(thm)],[236]) ).
cnf(273,plain,
( op(e1,e2) != e1
| ~ sP6 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l67,plain,
( op(e1,e2) != e1
| ~ sP6 ),
inference(instantiation,[status(thm)],[273]) ).
cnf(249,plain,
( op(e3,e0) != e3
| ~ sP14 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l90,plain,
( op(e3,e0) != e3
| ~ sP14 ),
inference(instantiation,[status(thm)],[249]) ).
cnf(220,plain,
( sP10
| op(e0,e0) = e0
| sP11
| sP12
| sP13
| sP4
| sP5
| sP6
| sP14
| sP15
| sP16
| sP7
| sP17
| sP8
| sP9
| sP1
| sP2
| sP3
| sP0
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l196,plain,
( sP10
| op(e0,e0) = e0
| sP11
| sP12
| sP13
| sP4
| sP5
| sP6
| sP14
| sP15
| sP16
| sP7
| sP17
| sP8
| sP9
| sP1
| sP2
| sP3
| sP0
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23 ),
inference(instantiation,[status(thm)],[220]) ).
cnf(276,plain,
( op(e1,e1) != e1
| ~ sP5 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l52,plain,
( op(e1,e1) != e1
| ~ sP5 ),
inference(instantiation,[status(thm)],[276]) ).
cnf(266,plain,
( op(e2,e2) = e0
| ~ sP9 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l221,plain,
( op(e2,e2) = e0
| ~ sP9 ),
inference(instantiation,[status(thm)],[266]) ).
cnf(242,plain,
( op(e3,e3) = e3
| ~ sP17 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l53,plain,
( op(e3,e3) = e3
| ~ sP17 ),
inference(instantiation,[status(thm)],[242]) ).
cnf(281,plain,
( op(e1,e1) = e0
| ~ sP4 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l101,plain,
( op(e1,e1) = e0
| ~ sP4 ),
inference(instantiation,[status(thm)],[281]) ).
cnf(284,plain,
( op(e0,e0) = e4
| ~ sP3 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l95,plain,
( op(e0,e0) = e4
| ~ sP3 ),
inference(instantiation,[status(thm)],[284]) ).
cnf(261,plain,
( op(e2,e1) != e2
| ~ sP10 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1160,plain,
( op(e2,e1) != e2
| ~ sP10 ),
inference(instantiation,[status(thm)],[261]) ).
cnf(259,plain,
( op(e2,e2) = e2
| ~ sP11 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l209,plain,
( op(e2,e2) = e2
| ~ sP11 ),
inference(instantiation,[status(thm)],[259]) ).
cnf(243,plain,
( op(e3,e2) != e3
| ~ sP16 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l223,plain,
( op(e3,e2) != e3
| ~ sP16 ),
inference(instantiation,[status(thm)],[243]) ).
cnf(252,plain,
( op(e2,e4) != e2
| ~ sP13 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l78,plain,
( op(e2,e4) != e2
| ~ sP13 ),
inference(instantiation,[status(thm)],[252]) ).
cnf(219,plain,
( sP10
| op(e0,e0) = e0
| sP11
| sP12
| sP13
| sP4
| sP5
| sP6
| sP14
| sP15
| sP16
| sP7
| sP17
| sP8
| sP9
| sP1
| sP2
| sP3
| sP0
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l89,plain,
( sP10
| op(e0,e0) = e0
| sP11
| sP12
| sP13
| sP4
| sP5
| sP6
| sP14
| sP15
| sP16
| sP7
| sP17
| sP8
| sP9
| sP1
| sP2
| sP3
| sP0
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23 ),
inference(instantiation,[status(thm)],[219]) ).
cnf(260,plain,
( op(e2,e2) = e2
| ~ sP11 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l70,plain,
( op(e2,e2) = e2
| ~ sP11 ),
inference(instantiation,[status(thm)],[260]) ).
cnf(240,plain,
( op(e3,e3) != e3
| ~ sP17 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l244,plain,
( op(e3,e3) != e3
| ~ sP17 ),
inference(instantiation,[status(thm)],[240]) ).
cnf(l214,plain,
( op(e1,e3) != e1
| ~ sP7 ),
inference(instantiation,[status(thm)],[270]) ).
cnf(216,plain,
( op(e4,e4) != e1
| op(e4,e1) = e4 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l271,plain,
( op(e4,e4) != e1
| op(e4,e1) = e4 ),
inference(instantiation,[status(thm)],[216]) ).
cnf(282,plain,
( op(e0,e4) != e0
| ~ sP3 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1180,plain,
( op(e0,e4) != e0
| ~ sP3 ),
inference(instantiation,[status(thm)],[282]) ).
cnf(l1173,plain,
( op(e3,e3) = e1
| ~ sP15 ),
inference(instantiation,[status(thm)],[248]) ).
cnf(239,plain,
( op(e3,e3) = e4
| ~ sP18 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l82,plain,
( op(e3,e3) = e4
| ~ sP18 ),
inference(instantiation,[status(thm)],[239]) ).
cnf(234,plain,
( op(e4,e0) != e4
| ~ sP19 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l250,plain,
( op(e4,e0) != e4
| ~ sP19 ),
inference(instantiation,[status(thm)],[234]) ).
cnf(207,plain,
( op(e2,e2) != e0
| op(e2,e0) = e2 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l68,plain,
( op(e2,e2) != e0
| op(e2,e0) = e2 ),
inference(instantiation,[status(thm)],[207]) ).
cnf(290,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1453,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[290]) ).
cnf(245,plain,
( op(e3,e3) = e2
| ~ sP16 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1338,plain,
( op(e3,e3) = e2
| ~ sP16 ),
inference(instantiation,[status(thm)],[245]) ).
cnf(l237,plain,
( op(e0,e0) = e4
| ~ sP3 ),
inference(instantiation,[status(thm)],[284]) ).
cnf(215,plain,
( op(e4,e4) != e0
| op(e4,e0) = e4 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l337,plain,
( op(e4,e4) != e0
| op(e4,e0) = e4 ),
inference(instantiation,[status(thm)],[215]) ).
cnf(212,plain,
( op(e3,e3) != e1
| op(e3,e1) = e3 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1456,plain,
( op(e3,e3) != e1
| op(e3,e1) = e3 ),
inference(instantiation,[status(thm)],[212]) ).
cnf(l1168,plain,
( op(e1,e2) != e1
| ~ sP6 ),
inference(instantiation,[status(thm)],[273]) ).
cnf(263,plain,
( op(e2,e2) = e1
| ~ sP10 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l94,plain,
( op(e2,e2) = e1
| ~ sP10 ),
inference(instantiation,[status(thm)],[263]) ).
cnf(l1243,plain,
( op(e4,e0) != e4
| ~ sP19 ),
inference(instantiation,[status(thm)],[234]) ).
cnf(204,plain,
( op(e1,e1) != e2
| op(e1,e2) = e1 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1409,plain,
( op(e1,e1) != e2
| op(e1,e2) = e1 ),
inference(instantiation,[status(thm)],[204]) ).
cnf(214,plain,
( op(e3,e3) != e4
| op(e3,e4) = e3 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l108,plain,
( op(e3,e3) != e4
| op(e3,e4) = e3 ),
inference(instantiation,[status(thm)],[214]) ).
cnf(202,plain,
( op(e0,e0) != e4
| op(e0,e4) = e0 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l114,plain,
( op(e0,e0) != e4
| op(e0,e4) = e0 ),
inference(instantiation,[status(thm)],[202]) ).
cnf(208,plain,
( op(e2,e2) != e1
| op(e2,e1) = e2 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1467,plain,
( op(e2,e2) != e1
| op(e2,e1) = e2 ),
inference(instantiation,[status(thm)],[208]) ).
cnf(l73,plain,
( op(e1,e1) != e2
| op(e1,e2) = e1 ),
inference(instantiation,[status(thm)],[204]) ).
cnf(l224,plain,
( op(e2,e2) != e0
| op(e2,e0) = e2 ),
inference(instantiation,[status(thm)],[207]) ).
cnf(l1176,plain,
( op(e4,e3) != e4
| ~ sP22 ),
inference(instantiation,[status(thm)],[225]) ).
cnf(275,plain,
( op(e1,e1) = e2
| ~ sP6 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l145,plain,
( op(e1,e1) = e2
| ~ sP6 ),
inference(instantiation,[status(thm)],[275]) ).
cnf(l50,plain,
( op(e2,e2) = e1
| ~ sP10 ),
inference(instantiation,[status(thm)],[263]) ).
cnf(278,plain,
( op(e1,e1) = e1
| ~ sP5 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l217,plain,
( op(e1,e1) = e1
| ~ sP5 ),
inference(instantiation,[status(thm)],[278]) ).
cnf(l1455,plain,
( op(e0,e0) != e4
| op(e0,e4) = e0 ),
inference(instantiation,[status(thm)],[202]) ).
cnf(227,plain,
( op(e4,e4) = e3
| ~ sP22 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l239,plain,
( op(e4,e4) = e3
| ~ sP22 ),
inference(instantiation,[status(thm)],[227]) ).
cnf(l1177,plain,
( op(e2,e4) != e2
| ~ sP13 ),
inference(instantiation,[status(thm)],[252]) ).
cnf(223,plain,
( op(e4,e4) = e4
| ~ sP23 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1340,plain,
( op(e4,e4) = e4
| ~ sP23 ),
inference(instantiation,[status(thm)],[223]) ).
cnf(l218,plain,
( op(e4,e4) = e2
| ~ sP21 ),
inference(instantiation,[status(thm)],[230]) ).
cnf(254,plain,
( op(e2,e2) = e4
| ~ sP13 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l216,plain,
( op(e2,e2) = e4
| ~ sP13 ),
inference(instantiation,[status(thm)],[254]) ).
cnf(218,plain,
( op(e4,e4) != e3
| op(e4,e3) = e4 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l240,plain,
( op(e4,e4) != e3
| op(e4,e3) = e4 ),
inference(instantiation,[status(thm)],[218]) ).
cnf(267,plain,
( op(e1,e4) != e1
| ~ sP8 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1411,plain,
( op(e1,e4) != e1
| ~ sP8 ),
inference(instantiation,[status(thm)],[267]) ).
cnf(205,plain,
( op(e1,e1) != e3
| op(e1,e3) = e1 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l251,plain,
( op(e1,e1) != e3
| op(e1,e3) = e1 ),
inference(instantiation,[status(thm)],[205]) ).
cnf(288,plain,
( op(e0,e2) != e0
| ~ sP1 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l49,plain,
( op(e0,e2) != e0
| ~ sP1 ),
inference(instantiation,[status(thm)],[288]) ).
cnf(233,plain,
( op(e4,e4) = e1
| ~ sP20 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1169,plain,
( op(e4,e4) = e1
| ~ sP20 ),
inference(instantiation,[status(thm)],[233]) ).
cnf(l1162,plain,
( op(e2,e2) != e1
| op(e2,e1) = e2 ),
inference(instantiation,[status(thm)],[208]) ).
cnf(246,plain,
( op(e3,e1) != e3
| ~ sP15 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l2104,plain,
( op(e3,e1) != e3
| ~ sP15 ),
inference(instantiation,[status(thm)],[246]) ).
cnf(228,plain,
( op(e4,e2) != e4
| ~ sP21 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l148,plain,
( op(e4,e2) != e4
| ~ sP21 ),
inference(instantiation,[status(thm)],[228]) ).
cnf(200,plain,
( op(e0,e0) != e2
| op(e0,e2) = e0 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1583,plain,
( op(e0,e0) != e2
| op(e0,e2) = e0 ),
inference(instantiation,[status(thm)],[200]) ).
cnf(l105,plain,
( op(e1,e4) != e1
| ~ sP8 ),
inference(instantiation,[status(thm)],[267]) ).
cnf(258,plain,
( op(e2,e2) != e2
| ~ sP11 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l265,plain,
( op(e2,e2) != e2
| ~ sP11 ),
inference(instantiation,[status(thm)],[258]) ).
cnf(257,plain,
( op(e2,e2) = e3
| ~ sP12 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1175,plain,
( op(e2,e2) = e3
| ~ sP12 ),
inference(instantiation,[status(thm)],[257]) ).
cnf(210,plain,
( op(e2,e2) != e4
| op(e2,e4) = e2 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l100,plain,
( op(e2,e2) != e4
| op(e2,e4) = e2 ),
inference(instantiation,[status(thm)],[210]) ).
cnf(l140,plain,
( op(e4,e4) != e3
| op(e4,e3) = e4 ),
inference(instantiation,[status(thm)],[218]) ).
cnf(285,plain,
( op(e0,e3) != e0
| ~ sP2 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1255,plain,
( op(e0,e3) != e0
| ~ sP2 ),
inference(instantiation,[status(thm)],[285]) ).
cnf(237,plain,
( op(e3,e4) != e3
| ~ sP18 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l319,plain,
( op(e3,e4) != e3
| ~ sP18 ),
inference(instantiation,[status(thm)],[237]) ).
cnf(211,plain,
( op(e3,e3) != e0
| op(e3,e0) = e3 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l118,plain,
( op(e3,e3) != e0
| op(e3,e0) = e3 ),
inference(instantiation,[status(thm)],[211]) ).
cnf(203,plain,
( op(e1,e1) != e0
| op(e1,e0) = e1 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l115,plain,
( op(e1,e1) != e0
| op(e1,e0) = e1 ),
inference(instantiation,[status(thm)],[203]) ).
cnf(l1546,plain,
( op(e2,e2) != e4
| op(e2,e4) = e2 ),
inference(instantiation,[status(thm)],[210]) ).
cnf(l1552,plain,
( op(e4,e4) != e3
| op(e4,e3) = e4 ),
inference(instantiation,[status(thm)],[218]) ).
cnf(l1178,plain,
( op(e2,e2) = e2
| ~ sP11 ),
inference(instantiation,[status(thm)],[260]) ).
cnf(l1174,plain,
( op(e3,e4) != e3
| ~ sP18 ),
inference(instantiation,[status(thm)],[237]) ).
cnf(l1167,plain,
( op(e1,e1) = e1
| ~ sP5 ),
inference(instantiation,[status(thm)],[278]) ).
cnf(201,plain,
( op(e0,e0) != e3
| op(e0,e3) = e0 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1906,plain,
( op(e0,e0) != e3
| op(e0,e3) = e0 ),
inference(instantiation,[status(thm)],[201]) ).
cnf(287,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l213,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[287]) ).
cnf(222,plain,
( op(e4,e4) != e4
| ~ sP23 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l313,plain,
( op(e4,e4) != e4
| ~ sP23 ),
inference(instantiation,[status(thm)],[222]) ).
cnf(l1463,plain,
( op(e2,e2) != e2
| ~ sP11 ),
inference(instantiation,[status(thm)],[258]) ).
cnf(l226,plain,
( op(e1,e1) != e1
| ~ sP5 ),
inference(instantiation,[status(thm)],[276]) ).
cnf(l80,plain,
( op(e3,e3) != e3
| ~ sP17 ),
inference(instantiation,[status(thm)],[240]) ).
cnf(l77,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[287]) ).
cnf(l153,plain,
( op(e0,e4) != e0
| ~ sP3 ),
inference(instantiation,[status(thm)],[282]) ).
cnf(l1311,plain,
( op(e4,e4) = e0
| ~ sP19 ),
inference(instantiation,[status(thm)],[236]) ).
cnf(l1237,plain,
( op(e2,e1) != e2
| ~ sP10 ),
inference(instantiation,[status(thm)],[261]) ).
cnf(l219,plain,
( op(e1,e1) = e2
| ~ sP6 ),
inference(instantiation,[status(thm)],[275]) ).
cnf(l212,plain,
( op(e4,e4) = e4
| ~ sP23 ),
inference(instantiation,[status(thm)],[224]) ).
cnf(l210,plain,
( op(e0,e2) != e0
| ~ sP1 ),
inference(instantiation,[status(thm)],[288]) ).
cnf(251,plain,
( op(e3,e3) = e0
| ~ sP14 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1932,plain,
( op(e3,e3) = e0
| ~ sP14 ),
inference(instantiation,[status(thm)],[251]) ).
cnf(l245,plain,
( op(e3,e4) != e3
| ~ sP18 ),
inference(instantiation,[status(thm)],[237]) ).
cnf(l86,plain,
( op(e0,e0) != e3
| op(e0,e3) = e0 ),
inference(instantiation,[status(thm)],[201]) ).
cnf(l141,plain,
( op(e2,e2) = e0
| ~ sP9 ),
inference(instantiation,[status(thm)],[266]) ).
cnf(l162,plain,
( op(e2,e2) != e2
| ~ sP11 ),
inference(instantiation,[status(thm)],[258]) ).
cnf(l222,plain,
( op(e3,e3) = e0
| ~ sP14 ),
inference(instantiation,[status(thm)],[251]) ).
cnf(293,plain,
( op(e0,e0) = e1
| ~ sP0 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l220,plain,
( op(e0,e0) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[293]) ).
cnf(l1166,plain,
( op(e4,e2) != e4
| ~ sP21 ),
inference(instantiation,[status(thm)],[228]) ).
cnf(206,plain,
( op(e1,e1) != e4
| op(e1,e4) = e1 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l125,plain,
( op(e1,e1) != e4
| op(e1,e4) = e1 ),
inference(instantiation,[status(thm)],[206]) ).
cnf(l231,plain,
( op(e3,e3) != e0
| op(e3,e0) = e3 ),
inference(instantiation,[status(thm)],[211]) ).
cnf(l211,plain,
( op(e2,e2) = e3
| ~ sP12 ),
inference(instantiation,[status(thm)],[257]) ).
cnf(l1407,plain,
( op(e3,e3) = e0
| ~ sP14 ),
inference(instantiation,[status(thm)],[251]) ).
cnf(l1335,plain,
( op(e1,e1) = e0
| ~ sP4 ),
inference(instantiation,[status(thm)],[281]) ).
cnf(l87,plain,
( op(e2,e2) = e3
| ~ sP12 ),
inference(instantiation,[status(thm)],[257]) ).
cnf(l254,plain,
( op(e0,e0) != e4
| op(e0,e4) = e0 ),
inference(instantiation,[status(thm)],[202]) ).
cnf(l1181,plain,
( op(e1,e3) != e1
| ~ sP7 ),
inference(instantiation,[status(thm)],[270]) ).
cnf(279,plain,
( op(e1,e0) != e1
| ~ sP4 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l968,plain,
( op(e1,e0) != e1
| ~ sP4 ),
inference(instantiation,[status(thm)],[279]) ).
cnf(l1585,plain,
( op(e2,e2) = e4
| ~ sP13 ),
inference(instantiation,[status(thm)],[254]) ).
cnf(l1339,plain,
( op(e1,e1) != e0
| op(e1,e0) = e1 ),
inference(instantiation,[status(thm)],[203]) ).
cnf(l2161,plain,
( op(e4,e4) = e3
| ~ sP22 ),
inference(instantiation,[status(thm)],[227]) ).
cnf(l249,plain,
( op(e3,e3) != e4
| op(e3,e4) = e3 ),
inference(instantiation,[status(thm)],[214]) ).
cnf(l81,plain,
( op(e4,e4) != e0
| op(e4,e0) = e4 ),
inference(instantiation,[status(thm)],[215]) ).
cnf(l107,plain,
( op(e3,e3) = e2
| ~ sP16 ),
inference(instantiation,[status(thm)],[245]) ).
cnf(l55,plain,
( op(e0,e0) != e2
| op(e0,e2) = e0 ),
inference(instantiation,[status(thm)],[200]) ).
cnf(l232,plain,
( op(e4,e4) != e2
| op(e4,e2) = e4 ),
inference(instantiation,[status(thm)],[217]) ).
cnf(l1830,plain,
( op(e4,e4) != e4
| ~ sP23 ),
inference(instantiation,[status(thm)],[222]) ).
cnf(l235,plain,
( op(e0,e0) != e2
| op(e0,e2) = e0 ),
inference(instantiation,[status(thm)],[200]) ).
cnf(213,plain,
( op(e3,e3) != e2
| op(e3,e2) = e3 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l147,plain,
( op(e3,e3) != e2
| op(e3,e2) = e3 ),
inference(instantiation,[status(thm)],[213]) ).
cnf(l965,plain,
( op(e4,e2) != e4
| ~ sP21 ),
inference(instantiation,[status(thm)],[228]) ).
cnf(l1163,plain,
( op(e2,e2) != e1
| op(e2,e1) = e2 ),
inference(instantiation,[status(thm)],[208]) ).
cnf(l242,plain,
( op(e4,e3) != e4
| ~ sP22 ),
inference(instantiation,[status(thm)],[225]) ).
cnf(l135,plain,
( op(e1,e1) != e3
| op(e1,e3) = e1 ),
inference(instantiation,[status(thm)],[205]) ).
cnf(l233,plain,
( op(e1,e4) != e1
| ~ sP8 ),
inference(instantiation,[status(thm)],[267]) ).
cnf(l236,plain,
( op(e4,e4) != e4
| ~ sP23 ),
inference(instantiation,[status(thm)],[222]) ).
cnf(l2298,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[287]) ).
cnf(l215,plain,
( op(e0,e0) != e3
| op(e0,e3) = e0 ),
inference(instantiation,[status(thm)],[201]) ).
cnf(l1194,plain,
( op(e4,e4) = e1
| ~ sP20 ),
inference(instantiation,[status(thm)],[233]) ).
cnf(l1405,plain,
( op(e4,e4) != e0
| op(e4,e0) = e4 ),
inference(instantiation,[status(thm)],[215]) ).
cnf(l327,plain,
( op(e4,e4) = e3
| ~ sP22 ),
inference(instantiation,[status(thm)],[227]) ).
cnf(l253,plain,
( op(e1,e1) != e4
| op(e1,e4) = e1 ),
inference(instantiation,[status(thm)],[206]) ).
cnf(l331,plain,
( op(e3,e2) != e3
| ~ sP16 ),
inference(instantiation,[status(thm)],[243]) ).
cnf(l121,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[290]) ).
cnf(l1975,plain,
( op(e1,e0) != e1
| ~ sP4 ),
inference(instantiation,[status(thm)],[279]) ).
cnf(209,plain,
( op(e2,e2) != e3
| op(e2,e3) = e2 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1341,plain,
( op(e2,e2) != e3
| op(e2,e3) = e2 ),
inference(instantiation,[status(thm)],[209]) ).
cnf(l238,plain,
( op(e0,e0) != e0
| sP10
| sP11
| sP12
| sP13
| sP4
| sP5
| sP6
| sP14
| sP15
| sP16
| sP7
| sP17
| sP8
| sP9
| sP1
| sP2
| sP3
| sP0
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23 ),
inference(instantiation,[status(thm)],[221]) ).
cnf(l1537,plain,
( op(e3,e0) != e3
| ~ sP14 ),
inference(instantiation,[status(thm)],[249]) ).
cnf(l1188,plain,
( op(e2,e2) = e2
| ~ sP11 ),
inference(instantiation,[status(thm)],[260]) ).
cnf(l1189,plain,
( op(e4,e4) != e4
| ~ sP23 ),
inference(instantiation,[status(thm)],[222]) ).
cnf(l248,plain,
( op(e4,e4) = e1
| ~ sP20 ),
inference(instantiation,[status(thm)],[233]) ).
cnf(l247,plain,
( op(e3,e3) = e1
| ~ sP15 ),
inference(instantiation,[status(thm)],[248]) ).
cnf(277,plain,
( op(e1,e1) = e1
| ~ sP5 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l92,plain,
( op(e1,e1) = e1
| ~ sP5 ),
inference(instantiation,[status(thm)],[277]) ).
cnf(l1209,plain,
( op(e3,e3) = e3
| ~ sP17 ),
inference(instantiation,[status(thm)],[242]) ).
cnf(l98,plain,
( op(e2,e2) != e3
| op(e2,e3) = e2 ),
inference(instantiation,[status(thm)],[209]) ).
cnf(l1412,plain,
( op(e4,e4) != e2
| op(e4,e2) = e4 ),
inference(instantiation,[status(thm)],[217]) ).
cnf(l2230,plain,
( op(e0,e2) != e0
| ~ sP1 ),
inference(instantiation,[status(thm)],[288]) ).
cnf(l1184,plain,
( op(e4,e4) = e1
| ~ sP20 ),
inference(instantiation,[status(thm)],[233]) ).
cnf(272,plain,
( op(e1,e1) = e3
| ~ sP7 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1161,plain,
( op(e1,e1) = e3
| ~ sP7 ),
inference(instantiation,[status(thm)],[272]) ).
cnf(l1040,plain,
( op(e1,e1) = e3
| ~ sP7 ),
inference(instantiation,[status(thm)],[272]) ).
cnf(l278,plain,
( op(e0,e3) != e0
| ~ sP2 ),
inference(instantiation,[status(thm)],[285]) ).
cnf(l1193,plain,
( op(e4,e4) = e3
| ~ sP22 ),
inference(instantiation,[status(thm)],[227]) ).
cnf(l1337,plain,
( op(e3,e3) != e4
| op(e3,e4) = e3 ),
inference(instantiation,[status(thm)],[214]) ).
cnf(l1197,plain,
( op(e4,e4) != e3
| op(e4,e3) = e4 ),
inference(instantiation,[status(thm)],[218]) ).
cnf(l1211,plain,
( op(e4,e4) = e2
| ~ sP21 ),
inference(instantiation,[status(thm)],[230]) ).
cnf(l228,plain,
( op(e2,e0) != e2
| ~ sP9 ),
inference(instantiation,[status(thm)],[264]) ).
cnf(l1457,plain,
( op(e4,e3) != e4
| ~ sP22 ),
inference(instantiation,[status(thm)],[225]) ).
cnf(269,plain,
( op(e1,e1) = e4
| ~ sP8 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1196,plain,
( op(e1,e1) = e4
| ~ sP8 ),
inference(instantiation,[status(thm)],[269]) ).
cnf(l229,plain,
( op(e1,e1) != e2
| op(e1,e2) = e1 ),
inference(instantiation,[status(thm)],[204]) ).
cnf(l1216,plain,
( op(e1,e1) != e4
| op(e1,e4) = e1 ),
inference(instantiation,[status(thm)],[206]) ).
cnf(l1187,plain,
( op(e2,e4) != e2
| ~ sP13 ),
inference(instantiation,[status(thm)],[252]) ).
cnf(l567,plain,
( op(e1,e1) = e4
| ~ sP8 ),
inference(instantiation,[status(thm)],[269]) ).
cnf(l1233,plain,
( op(e1,e2) != e1
| ~ sP6 ),
inference(instantiation,[status(thm)],[273]) ).
cnf(l1416,plain,
( op(e1,e4) != e1
| ~ sP8 ),
inference(instantiation,[status(thm)],[267]) ).
cnf(l1542,plain,
( op(e1,e1) != e1
| ~ sP5 ),
inference(instantiation,[status(thm)],[276]) ).
cnf(l1207,plain,
( op(e2,e2) != e2
| ~ sP11 ),
inference(instantiation,[status(thm)],[258]) ).
cnf(l1222,plain,
( op(e0,e4) != e0
| ~ sP3 ),
inference(instantiation,[status(thm)],[282]) ).
cnf(l1185,plain,
( op(e3,e2) != e3
| ~ sP16 ),
inference(instantiation,[status(thm)],[243]) ).
cnf(l356,plain,
( op(e3,e3) != e2
| op(e3,e2) = e3 ),
inference(instantiation,[status(thm)],[213]) ).
cnf(l1215,plain,
( op(e3,e3) = e4
| ~ sP18 ),
inference(instantiation,[status(thm)],[239]) ).
cnf(l1200,plain,
( op(e4,e4) = e0
| ~ sP19 ),
inference(instantiation,[status(thm)],[236]) ).
cnf(l1999,plain,
( op(e0,e0) = e4
| ~ sP3 ),
inference(instantiation,[status(thm)],[284]) ).
cnf(l1220,plain,
( op(e1,e3) != e1
| ~ sP7 ),
inference(instantiation,[status(thm)],[270]) ).
cnf(255,plain,
( op(e2,e3) != e2
| ~ sP12 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1240,plain,
( op(e2,e3) != e2
| ~ sP12 ),
inference(instantiation,[status(thm)],[255]) ).
cnf(241,plain,
( op(e3,e3) = e3
| ~ sP17 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1182,plain,
( op(e3,e3) = e3
| ~ sP17 ),
inference(instantiation,[status(thm)],[241]) ).
cnf(l1524,plain,
( op(e3,e3) != e3
| ~ sP17 ),
inference(instantiation,[status(thm)],[240]) ).
cnf(l1513,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[290]) ).
cnf(l1785,plain,
( op(e1,e1) != e3
| op(e1,e3) = e1 ),
inference(instantiation,[status(thm)],[205]) ).
cnf(l1217,plain,
( op(e1,e1) = e1
| ~ sP5 ),
inference(instantiation,[status(thm)],[277]) ).
cnf(l1250,plain,
( op(e4,e4) != e0
| op(e4,e0) = e4 ),
inference(instantiation,[status(thm)],[215]) ).
cnf(l1164,plain,
( op(e0,e3) != e0
| ~ sP2 ),
inference(instantiation,[status(thm)],[285]) ).
cnf(l1202,plain,
( op(e3,e3) = e1
| ~ sP15 ),
inference(instantiation,[status(thm)],[248]) ).
cnf(l1183,plain,
( op(e2,e2) = e1
| ~ sP10 ),
inference(instantiation,[status(thm)],[263]) ).
cnf(l104,plain,
( op(e4,e0) != e4
| ~ sP19 ),
inference(instantiation,[status(thm)],[234]) ).
cnf(l1272,plain,
( op(e0,e4) != e0
| ~ sP3 ),
inference(instantiation,[status(thm)],[282]) ).
cnf(l1191,plain,
( op(e1,e2) != e1
| ~ sP6 ),
inference(instantiation,[status(thm)],[273]) ).
cnf(l619,plain,
( op(e2,e2) = e4
| ~ sP13 ),
inference(instantiation,[status(thm)],[254]) ).
cnf(l487,plain,
( op(e3,e3) = e2
| ~ sP16 ),
inference(instantiation,[status(thm)],[245]) ).
cnf(l2109,plain,
( op(e1,e1) = e3
| ~ sP7 ),
inference(instantiation,[status(thm)],[272]) ).
cnf(l1226,plain,
( op(e2,e2) = e0
| ~ sP9 ),
inference(instantiation,[status(thm)],[266]) ).
cnf(l263,plain,
( op(e1,e1) = e4
| ~ sP8 ),
inference(instantiation,[status(thm)],[269]) ).
cnf(l1245,plain,
( op(e1,e1) != e1
| ~ sP5 ),
inference(instantiation,[status(thm)],[276]) ).
cnf(l246,plain,
( op(e3,e3) = e3
| ~ sP17 ),
inference(instantiation,[status(thm)],[241]) ).
cnf(l1224,plain,
( op(e0,e0) != e4
| op(e0,e4) = e0 ),
inference(instantiation,[status(thm)],[202]) ).
cnf(l2113,plain,
( op(e4,e4) = e0
| ~ sP19 ),
inference(instantiation,[status(thm)],[236]) ).
cnf(l2673,plain,
( op(e1,e1) = e2
| ~ sP6 ),
inference(instantiation,[status(thm)],[275]) ).
cnf(l1242,plain,
( op(e4,e4) != e1
| op(e4,e1) = e4 ),
inference(instantiation,[status(thm)],[216]) ).
cnf(l1186,plain,
( op(e3,e3) != e2
| op(e3,e2) = e3 ),
inference(instantiation,[status(thm)],[213]) ).
cnf(l1172,plain,
( op(e2,e2) = e1
| ~ sP10 ),
inference(instantiation,[status(thm)],[263]) ).
cnf(l1228,plain,
( op(e1,e1) != e3
| op(e1,e3) = e1 ),
inference(instantiation,[status(thm)],[205]) ).
cnf(l1521,plain,
( op(e1,e1) != e4
| op(e1,e4) = e1 ),
inference(instantiation,[status(thm)],[206]) ).
cnf(l2829,plain,
( op(e0,e0) = e4
| ~ sP3 ),
inference(instantiation,[status(thm)],[284]) ).
cnf(l2288,plain,
( op(e3,e3) = e4
| ~ sP18 ),
inference(instantiation,[status(thm)],[239]) ).
cnf(l1201,plain,
( op(e2,e2) != e4
| op(e2,e4) = e2 ),
inference(instantiation,[status(thm)],[210]) ).
cnf(l1229,plain,
( op(e1,e1) = e3
| ~ sP7 ),
inference(instantiation,[status(thm)],[272]) ).
cnf(l1225,plain,
( op(e3,e3) != e4
| op(e3,e4) = e3 ),
inference(instantiation,[status(thm)],[214]) ).
cnf(l1964,plain,
( op(e4,e1) != e4
| ~ sP20 ),
inference(instantiation,[status(thm)],[231]) ).
cnf(l1342,plain,
( op(e2,e2) = e0
| ~ sP9 ),
inference(instantiation,[status(thm)],[266]) ).
cnf(l1238,plain,
( op(e3,e3) != e1
| op(e3,e1) = e3 ),
inference(instantiation,[status(thm)],[212]) ).
cnf(l2272,plain,
( op(e1,e1) = e4
| ~ sP8 ),
inference(instantiation,[status(thm)],[269]) ).
cnf(l124,plain,
( op(e3,e3) != e1
| op(e3,e1) = e3 ),
inference(instantiation,[status(thm)],[212]) ).
cnf(l1824,plain,
( op(e2,e3) != e2
| ~ sP12 ),
inference(instantiation,[status(thm)],[255]) ).
cnf(l1190,plain,
( op(e4,e4) != e1
| op(e4,e1) = e4 ),
inference(instantiation,[status(thm)],[216]) ).
cnf(l1221,plain,
( op(e4,e4) != e2
| op(e4,e2) = e4 ),
inference(instantiation,[status(thm)],[217]) ).
cnf(l1473,plain,
( op(e4,e0) != e4
| ~ sP19 ),
inference(instantiation,[status(thm)],[234]) ).
cnf(l270,plain,
( op(e3,e1) != e3
| ~ sP15 ),
inference(instantiation,[status(thm)],[246]) ).
cnf(l1817,plain,
( op(e2,e1) != e2
| ~ sP10 ),
inference(instantiation,[status(thm)],[261]) ).
cnf(l959,plain,
( op(e3,e3) = e4
| ~ sP18 ),
inference(instantiation,[status(thm)],[239]) ).
cnf(l243,plain,
( op(e2,e2) != e4
| op(e2,e4) = e2 ),
inference(instantiation,[status(thm)],[210]) ).
cnf(l1933,plain,
( op(e4,e4) = e2
| ~ sP21 ),
inference(instantiation,[status(thm)],[230]) ).
cnf(l372,plain,
( op(e3,e3) != e1
| op(e3,e1) = e3 ),
inference(instantiation,[status(thm)],[212]) ).
cnf(l1294,plain,
( op(e3,e1) != e3
| ~ sP15 ),
inference(instantiation,[status(thm)],[246]) ).
cnf(l1271,plain,
( op(e4,e2) != e4
| ~ sP21 ),
inference(instantiation,[status(thm)],[228]) ).
cnf(l1204,plain,
( op(e1,e1) != e2
| op(e1,e2) = e1 ),
inference(instantiation,[status(thm)],[204]) ).
cnf(l1293,plain,
( op(e4,e1) != e4
| ~ sP20 ),
inference(instantiation,[status(thm)],[231]) ).
cnf(l1203,plain,
( op(e3,e3) = e0
| ~ sP14 ),
inference(instantiation,[status(thm)],[251]) ).
cnf(l1239,plain,
( op(e3,e3) != e3
| ~ sP17 ),
inference(instantiation,[status(thm)],[240]) ).
cnf(l1558,plain,
( op(e3,e4) != e3
| ~ sP18 ),
inference(instantiation,[status(thm)],[237]) ).
cnf(l1198,plain,
( op(e0,e3) != e0
| ~ sP2 ),
inference(instantiation,[status(thm)],[285]) ).
cnf(l335,plain,
( op(e4,e4) != e1
| op(e4,e1) = e4 ),
inference(instantiation,[status(thm)],[216]) ).
cnf(l373,plain,
( op(e3,e1) != e3
| ~ sP15 ),
inference(instantiation,[status(thm)],[246]) ).
cnf(l1195,plain,
( op(e4,e4) = e4
| ~ sP23 ),
inference(instantiation,[status(thm)],[223]) ).
cnf(l1231,plain,
( op(e2,e2) != e0
| op(e2,e0) = e2 ),
inference(instantiation,[status(thm)],[207]) ).
cnf(l418,plain,
( op(e4,e1) != e4
| ~ sP20 ),
inference(instantiation,[status(thm)],[231]) ).
cnf(l1305,plain,
( op(e3,e3) != e0
| op(e3,e0) = e3 ),
inference(instantiation,[status(thm)],[211]) ).
cnf(l1462,plain,
( op(e2,e2) != e0
| op(e2,e0) = e2 ),
inference(instantiation,[status(thm)],[207]) ).
cnf(l3012,plain,
( op(e3,e3) = e2
| ~ sP16 ),
inference(instantiation,[status(thm)],[245]) ).
cnf(l1466,plain,
( op(e3,e3) != e0
| op(e3,e0) = e3 ),
inference(instantiation,[status(thm)],[211]) ).
cnf(l1219,plain,
( op(e0,e0) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[293]) ).
cnf(l1199,plain,
( op(e0,e0) != e3
| op(e0,e3) = e0 ),
inference(instantiation,[status(thm)],[201]) ).
cnf(l1205,plain,
( op(e2,e2) != e1
| op(e2,e1) = e2 ),
inference(instantiation,[status(thm)],[208]) ).
cnf(l1398,plain,
( op(e3,e0) != e3
| ~ sP14 ),
inference(instantiation,[status(thm)],[249]) ).
cnf(l1668,plain,
( op(e2,e0) != e2
| ~ sP9 ),
inference(instantiation,[status(thm)],[264]) ).
cnf(l252,plain,
( op(e2,e2) != e3
| op(e2,e3) = e2 ),
inference(instantiation,[status(thm)],[209]) ).
cnf(l1210,plain,
( op(e0,e2) != e0
| ~ sP1 ),
inference(instantiation,[status(thm)],[288]) ).
cnf(l257,plain,
( op(e2,e3) != e2
| ~ sP12 ),
inference(instantiation,[status(thm)],[255]) ).
cnf(l1581,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[287]) ).
cnf(l1257,plain,
( op(e0,e0) != e2
| op(e0,e2) = e0 ),
inference(instantiation,[status(thm)],[200]) ).
cnf(l1241,plain,
( op(e2,e2) != e3
| op(e2,e3) = e2 ),
inference(instantiation,[status(thm)],[209]) ).
cnf(l1580,plain,
( op(e3,e3) != e2
| op(e3,e2) = e3 ),
inference(instantiation,[status(thm)],[213]) ).
cnf(l1995,plain,
( op(e2,e0) != e2
| ~ sP9 ),
inference(instantiation,[status(thm)],[264]) ).
cnf(l1706,plain,
( op(e2,e2) = e3
| ~ sP12 ),
inference(instantiation,[status(thm)],[257]) ).
cnf(l1777,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[290]) ).
cnf(l1356,plain,
( op(e2,e2) = e4
| ~ sP13 ),
inference(instantiation,[status(thm)],[254]) ).
cnf(l256,plain,
( op(e2,e4) != e2
| ~ sP13 ),
inference(instantiation,[status(thm)],[252]) ).
cnf(l417,plain,
( op(e2,e3) != e2
| ~ sP12 ),
inference(instantiation,[status(thm)],[255]) ).
cnf(l1992,plain,
( op(e3,e0) != e3
| ~ sP14 ),
inference(instantiation,[status(thm)],[249]) ).
cnf(l1676,plain,
( op(e1,e1) = e2
| ~ sP6 ),
inference(instantiation,[status(thm)],[275]) ).
cnf(l1270,plain,
( op(e2,e1) != e2
| ~ sP10 ),
inference(instantiation,[status(thm)],[261]) ).
cnf(l1968,plain,
( op(e3,e2) != e3
| ~ sP16 ),
inference(instantiation,[status(thm)],[243]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l3,l48,l84,l61,l62,l132,l79,l60,l57,l54,l67,l90,l196,l52,l221,l53,l101,l95,l1160,l209,l223,l78,l89,l70,l244,l214,l271,l1180,l1173,l82,l250,l68,l1453,l1338,l237,l337,l1456,l1168,l94,l1243,l1409,l108,l114,l1467,l73,l224,l1176,l145,l50,l217,l1455,l239,l1177,l1340,l218,l216,l240,l1411,l251,l49,l1169,l1162,l2104,l148,l1583,l105,l265,l1175,l100,l140,l1255,l319,l118,l115,l1546,l1552,l1178,l1174,l1167,l1906,l213,l313,l1463,l226,l80,l77,l153,l1311,l1237,l219,l212,l210,l1932,l245,l86,l141,l162,l222,l220,l1166,l125,l231,l211,l1407,l1335,l87,l254,l1181,l968,l1585,l1339,l2161,l249,l81,l107,l55,l232,l1830,l235,l147,l965,l1163,l242,l135,l233,l236,l2298,l215,l1194,l1405,l327,l253,l331,l121,l1975,l1341,l238,l1537,l1188,l1189,l248,l247,l92,l1209,l98,l1412,l2230,l1184,l1161,l1040,l278,l1193,l1337,l1197,l1211,l228,l1457,l1196,l229,l1216,l1187,l567,l1233,l1416,l1542,l1207,l1222,l1185,l356,l1215,l1200,l1999,l1220,l1240,l1182,l1524,l1513,l1785,l1217,l1250,l1164,l1202,l1183,l104,l1272,l1191,l619,l487,l2109,l1226,l263,l1245,l246,l1224,l2113,l2673,l1242,l1186,l1172,l1228,l1521,l2829,l2288,l1201,l1229,l1225,l1964,l1342,l1238,l2272,l124,l1824,l1190,l1221,l1473,l270,l1817,l959,l243,l1933,l372,l1294,l1271,l1204,l1293,l1203,l1239,l1558,l1198,l335,l373,l1195,l1231,l418,l1305,l1462,l3012,l1466,l1219,l1199,l1205,l1398,l1668,l252,l1210,l257,l1581,l1257,l1241,l1580,l1995,l1706,l1777,l1356,l256,l417,l1992,l1676,l1270,l1968]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.08 % Problem : ALG067+1 : TPTP v9.0.0. Released v2.7.0.
% 0.06/0.09 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.28 % Computer : n020.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 300
% 0.08/0.28 % DateTime : Sun Jul 20 02:08:49 EDT 2025
% 0.08/0.28 % CPUTime :
% 0.08/0.29 % launching worker at depth: 4
% 0.08/0.29 % launching worker at depth: 6
% 0.08/0.29 % launching worker at depth: 1
% 0.08/0.29 % launching worker at depth: 2
% 0.08/0.29 % launching worker at depth: 5
% 0.08/0.29 % launching worker at depth: 3
% 0.08/0.29 % launching worker at depth: 7
% 0.08/0.29 % launching worker at depth: 8
% 59.61/7.84 % SZS status Theorem for theBenchmark
% 59.61/7.84 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------