%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : ALG067+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n021.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 17:34:56 EDT 2022
% Result : Theorem 2.12s 2.31s
% Output : CNFRefutation 2.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 1
% Syntax : Number of formulae : 181 ( 90 unt; 0 def)
% Number of atoms : 6135 (6085 equ)
% Maximal formula atoms : 125 ( 33 avg)
% Number of connectives : 9320 (3366 ~;2099 |;3805 &)
% ( 0 <=>; 50 =>; 0 <=; 0 <~>)
% Maximal formula depth : 56 ( 17 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 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,conjecture,
~ ( ( 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 ) ) ) ).
fof(subgoal_0,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_1,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_2,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_3,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_4,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_5,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_6,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_7,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_8,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_9,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_10,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_11,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_12,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_13,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_14,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_15,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_16,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_17,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_18,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_19,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_20,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_21,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_22,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_23,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 ),
inference(strip,[],[co1]) ).
fof(subgoal_24,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(strip,[],[co1]) ).
fof(negate_0_0,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 ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
$false,
inference(canonicalize,[],[negate_0_0]) ).
cnf(refute_0_0,plain,
$false,
inference(canonicalize,[],[normalize_0_0]) ).
fof(negate_1_0,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 ),
inference(negate,[],[subgoal_1]) ).
fof(normalize_1_0,plain,
( op(e0,e1) != e0
& op(e0,e0) = e1
& op(e1,e1) = 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) != 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) != 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) != 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 ) ),
inference(canonicalize,[],[negate_1_0]) ).
fof(normalize_1_1,plain,
( op(e0,e0) != e1
| op(e0,e1) = e0 ),
inference(conjunct,[],[normalize_1_0]) ).
fof(normalize_1_2,plain,
op(e0,e0) = e1,
inference(conjunct,[],[normalize_1_0]) ).
fof(normalize_1_3,plain,
op(e0,e1) != e0,
inference(conjunct,[],[normalize_1_0]) ).
fof(normalize_1_4,plain,
$false,
inference(simplify,[],[normalize_1_1,normalize_1_2,normalize_1_3]) ).
cnf(refute_1_0,plain,
$false,
inference(canonicalize,[],[normalize_1_4]) ).
fof(negate_2_0,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 ),
inference(negate,[],[subgoal_2]) ).
fof(normalize_2_0,plain,
( op(e0,e2) != e0
& op(e0,e0) = e2
& op(e2,e2) = 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 ) ),
inference(canonicalize,[],[negate_2_0]) ).
fof(normalize_2_1,plain,
( op(e0,e0) != e2
| op(e0,e2) = e0 ),
inference(conjunct,[],[normalize_2_0]) ).
fof(normalize_2_2,plain,
op(e0,e0) = e2,
inference(conjunct,[],[normalize_2_0]) ).
fof(normalize_2_3,plain,
op(e0,e2) != e0,
inference(conjunct,[],[normalize_2_0]) ).
fof(normalize_2_4,plain,
$false,
inference(simplify,[],[normalize_2_1,normalize_2_2,normalize_2_3]) ).
cnf(refute_2_0,plain,
$false,
inference(canonicalize,[],[normalize_2_4]) ).
fof(negate_3_0,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 ),
inference(negate,[],[subgoal_3]) ).
fof(normalize_3_0,plain,
( op(e0,e3) != e0
& op(e0,e0) = e3
& op(e3,e3) = 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e0,e2) = e0 ) ),
inference(canonicalize,[],[negate_3_0]) ).
fof(normalize_3_1,plain,
( op(e0,e0) != e3
| op(e0,e3) = e0 ),
inference(conjunct,[],[normalize_3_0]) ).
fof(normalize_3_2,plain,
op(e0,e0) = e3,
inference(conjunct,[],[normalize_3_0]) ).
fof(normalize_3_3,plain,
op(e0,e3) != e0,
inference(conjunct,[],[normalize_3_0]) ).
fof(normalize_3_4,plain,
$false,
inference(simplify,[],[normalize_3_1,normalize_3_2,normalize_3_3]) ).
cnf(refute_3_0,plain,
$false,
inference(canonicalize,[],[normalize_3_4]) ).
fof(negate_4_0,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 ),
inference(negate,[],[subgoal_4]) ).
fof(normalize_4_0,plain,
( op(e0,e4) != e0
& op(e0,e0) = e4
& op(e4,e4) = 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) != 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) != 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) != 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(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 ) ),
inference(canonicalize,[],[negate_4_0]) ).
fof(normalize_4_1,plain,
( op(e0,e0) != e4
| op(e0,e4) = e0 ),
inference(conjunct,[],[normalize_4_0]) ).
fof(normalize_4_2,plain,
op(e0,e0) = e4,
inference(conjunct,[],[normalize_4_0]) ).
fof(normalize_4_3,plain,
op(e0,e4) != e0,
inference(conjunct,[],[normalize_4_0]) ).
fof(normalize_4_4,plain,
$false,
inference(simplify,[],[normalize_4_1,normalize_4_2,normalize_4_3]) ).
cnf(refute_4_0,plain,
$false,
inference(canonicalize,[],[normalize_4_4]) ).
fof(negate_5_0,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 ),
inference(negate,[],[subgoal_5]) ).
fof(normalize_5_0,plain,
( op(e1,e0) != e1
& op(e0,e0) = e1
& op(e1,e1) = 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) != 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) != 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) != 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(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 ) ),
inference(canonicalize,[],[negate_5_0]) ).
fof(normalize_5_1,plain,
( op(e1,e1) != e0
| op(e1,e0) = e1 ),
inference(conjunct,[],[normalize_5_0]) ).
fof(normalize_5_2,plain,
op(e1,e1) = e0,
inference(conjunct,[],[normalize_5_0]) ).
fof(normalize_5_3,plain,
op(e1,e0) != e1,
inference(conjunct,[],[normalize_5_0]) ).
fof(normalize_5_4,plain,
$false,
inference(simplify,[],[normalize_5_1,normalize_5_2,normalize_5_3]) ).
cnf(refute_5_0,plain,
$false,
inference(canonicalize,[],[normalize_5_4]) ).
fof(negate_6_0,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 ),
inference(negate,[],[subgoal_6]) ).
fof(normalize_6_0,plain,
$false,
inference(canonicalize,[],[negate_6_0]) ).
cnf(refute_6_0,plain,
$false,
inference(canonicalize,[],[normalize_6_0]) ).
fof(negate_7_0,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 ),
inference(negate,[],[subgoal_7]) ).
fof(normalize_7_0,plain,
( op(e1,e2) != e1
& op(e1,e1) = e2
& op(e2,e2) = e1
& ( 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( 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 ) ),
inference(canonicalize,[],[negate_7_0]) ).
fof(normalize_7_1,plain,
( op(e1,e1) != e2
| op(e1,e2) = e1 ),
inference(conjunct,[],[normalize_7_0]) ).
fof(normalize_7_2,plain,
op(e1,e1) = e2,
inference(conjunct,[],[normalize_7_0]) ).
fof(normalize_7_3,plain,
op(e1,e2) != e1,
inference(conjunct,[],[normalize_7_0]) ).
fof(normalize_7_4,plain,
$false,
inference(simplify,[],[normalize_7_1,normalize_7_2,normalize_7_3]) ).
cnf(refute_7_0,plain,
$false,
inference(canonicalize,[],[normalize_7_4]) ).
fof(negate_8_0,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 ),
inference(negate,[],[subgoal_8]) ).
fof(normalize_8_0,plain,
( op(e1,e3) != e1
& op(e1,e1) = e3
& op(e3,e3) = e1
& ( 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( 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) != e2
| op(e2,e2) != e1
| op(e1,e2) = e1 ) ),
inference(canonicalize,[],[negate_8_0]) ).
fof(normalize_8_1,plain,
( op(e1,e1) != e3
| op(e1,e3) = e1 ),
inference(conjunct,[],[normalize_8_0]) ).
fof(normalize_8_2,plain,
op(e1,e1) = e3,
inference(conjunct,[],[normalize_8_0]) ).
fof(normalize_8_3,plain,
op(e1,e3) != e1,
inference(conjunct,[],[normalize_8_0]) ).
fof(normalize_8_4,plain,
$false,
inference(simplify,[],[normalize_8_1,normalize_8_2,normalize_8_3]) ).
cnf(refute_8_0,plain,
$false,
inference(canonicalize,[],[normalize_8_4]) ).
fof(negate_9_0,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 ),
inference(negate,[],[subgoal_9]) ).
fof(normalize_9_0,plain,
( op(e1,e4) != e1
& op(e1,e1) = e4
& op(e4,e4) = e1
& ( 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( 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) != e2
| op(e2,e2) != e1
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e3,e3) != e1
| op(e1,e3) = e1 ) ),
inference(canonicalize,[],[negate_9_0]) ).
fof(normalize_9_1,plain,
( op(e1,e1) != e4
| op(e1,e4) = e1 ),
inference(conjunct,[],[normalize_9_0]) ).
fof(normalize_9_2,plain,
op(e1,e1) = e4,
inference(conjunct,[],[normalize_9_0]) ).
fof(normalize_9_3,plain,
op(e1,e4) != e1,
inference(conjunct,[],[normalize_9_0]) ).
fof(normalize_9_4,plain,
$false,
inference(simplify,[],[normalize_9_1,normalize_9_2,normalize_9_3]) ).
cnf(refute_9_0,plain,
$false,
inference(canonicalize,[],[normalize_9_4]) ).
fof(negate_10_0,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 ),
inference(negate,[],[subgoal_10]) ).
fof(normalize_10_0,plain,
( op(e2,e0) != e2
& op(e0,e0) = e2
& op(e2,e2) = 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( 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) != 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 ) ),
inference(canonicalize,[],[negate_10_0]) ).
fof(normalize_10_1,plain,
( op(e2,e2) != e0
| op(e2,e0) = e2 ),
inference(conjunct,[],[normalize_10_0]) ).
fof(normalize_10_2,plain,
op(e2,e2) = e0,
inference(conjunct,[],[normalize_10_0]) ).
fof(normalize_10_3,plain,
op(e2,e0) != e2,
inference(conjunct,[],[normalize_10_0]) ).
fof(normalize_10_4,plain,
$false,
inference(simplify,[],[normalize_10_1,normalize_10_2,normalize_10_3]) ).
cnf(refute_10_0,plain,
$false,
inference(canonicalize,[],[normalize_10_4]) ).
fof(negate_11_0,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 ),
inference(negate,[],[subgoal_11]) ).
fof(normalize_11_0,plain,
( op(e2,e1) != e2
& op(e1,e1) = e2
& op(e2,e2) = e1
& ( 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e0,e2) = e0 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( 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) != 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 ) ),
inference(canonicalize,[],[negate_11_0]) ).
fof(normalize_11_1,plain,
( op(e2,e2) != e1
| op(e2,e1) = e2 ),
inference(conjunct,[],[normalize_11_0]) ).
fof(normalize_11_2,plain,
op(e2,e2) = e1,
inference(conjunct,[],[normalize_11_0]) ).
fof(normalize_11_3,plain,
op(e2,e1) != e2,
inference(conjunct,[],[normalize_11_0]) ).
fof(normalize_11_4,plain,
$false,
inference(simplify,[],[normalize_11_1,normalize_11_2,normalize_11_3]) ).
cnf(refute_11_0,plain,
$false,
inference(canonicalize,[],[normalize_11_4]) ).
fof(negate_12_0,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 ),
inference(negate,[],[subgoal_12]) ).
fof(normalize_12_0,plain,
$false,
inference(canonicalize,[],[negate_12_0]) ).
cnf(refute_12_0,plain,
$false,
inference(canonicalize,[],[normalize_12_0]) ).
fof(negate_13_0,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 ),
inference(negate,[],[subgoal_13]) ).
fof(normalize_13_0,plain,
( op(e2,e3) != e2
& op(e2,e2) = e3
& op(e3,e3) = e2
& ( 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e0,e2) = e0 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( 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) != e2
| op(e2,e2) != e1
| op(e1,e2) = e1 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e1,e1) != e3
| op(e3,e3) != e1
| op(e1,e3) = e1 )
& ( op(e1,e1) != e4
| op(e4,e4) != e1
| op(e1,e4) = e1 ) ),
inference(canonicalize,[],[negate_13_0]) ).
fof(normalize_13_1,plain,
( op(e2,e2) != e3
| op(e2,e3) = e2 ),
inference(conjunct,[],[normalize_13_0]) ).
fof(normalize_13_2,plain,
op(e2,e2) = e3,
inference(conjunct,[],[normalize_13_0]) ).
fof(normalize_13_3,plain,
op(e2,e3) != e2,
inference(conjunct,[],[normalize_13_0]) ).
fof(normalize_13_4,plain,
$false,
inference(simplify,[],[normalize_13_1,normalize_13_2,normalize_13_3]) ).
cnf(refute_13_0,plain,
$false,
inference(canonicalize,[],[normalize_13_4]) ).
fof(negate_14_0,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 ),
inference(negate,[],[subgoal_14]) ).
fof(normalize_14_0,plain,
( op(e2,e4) != e2
& op(e2,e2) = e4
& op(e4,e4) = e2
& ( 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e0,e2) = e0 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( 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) != e2
| op(e2,e2) != e1
| op(e1,e2) = e1 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( 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) != e3
| op(e3,e3) != e2
| op(e2,e3) = e2 ) ),
inference(canonicalize,[],[negate_14_0]) ).
fof(normalize_14_1,plain,
( op(e2,e2) != e4
| op(e2,e4) = e2 ),
inference(conjunct,[],[normalize_14_0]) ).
fof(normalize_14_2,plain,
op(e2,e2) = e4,
inference(conjunct,[],[normalize_14_0]) ).
fof(normalize_14_3,plain,
op(e2,e4) != e2,
inference(conjunct,[],[normalize_14_0]) ).
fof(normalize_14_4,plain,
$false,
inference(simplify,[],[normalize_14_1,normalize_14_2,normalize_14_3]) ).
cnf(refute_14_0,plain,
$false,
inference(canonicalize,[],[normalize_14_4]) ).
fof(negate_15_0,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 ),
inference(negate,[],[subgoal_15]) ).
fof(normalize_15_0,plain,
( op(e3,e0) != e3
& op(e0,e0) = e3
& op(e3,e3) = 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e0,e2) = e0 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( 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) != e2
| op(e2,e2) != e1
| op(e1,e2) = e1 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( 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) != e3
| op(e3,e3) != e2
| op(e2,e3) = e2 )
& ( op(e2,e2) != e4
| op(e4,e4) != e2
| op(e2,e4) = e2 ) ),
inference(canonicalize,[],[negate_15_0]) ).
fof(normalize_15_1,plain,
( op(e3,e3) != e0
| op(e3,e0) = e3 ),
inference(conjunct,[],[normalize_15_0]) ).
fof(normalize_15_2,plain,
op(e3,e3) = e0,
inference(conjunct,[],[normalize_15_0]) ).
fof(normalize_15_3,plain,
op(e3,e0) != e3,
inference(conjunct,[],[normalize_15_0]) ).
fof(normalize_15_4,plain,
$false,
inference(simplify,[],[normalize_15_1,normalize_15_2,normalize_15_3]) ).
cnf(refute_15_0,plain,
$false,
inference(canonicalize,[],[normalize_15_4]) ).
fof(negate_16_0,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 ),
inference(negate,[],[subgoal_16]) ).
fof(normalize_16_0,plain,
( op(e3,e1) != e3
& op(e1,e1) = e3
& op(e3,e3) = e1
& ( 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e0,e2) = e0 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e0,e0) != e3
| op(e3,e3) != e0
| op(e0,e3) = e0 )
& ( op(e0,e0) != e3
| op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e0,e0) != e4
| op(e4,e4) != e0
| op(e0,e4) = e0 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e1,e2) = e1 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( 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) != e3
| op(e3,e3) != e2
| op(e2,e3) = e2 )
& ( op(e2,e2) != e4
| op(e4,e4) != e2
| op(e2,e4) = e2 ) ),
inference(canonicalize,[],[negate_16_0]) ).
fof(normalize_16_1,plain,
( op(e3,e3) != e1
| op(e3,e1) = e3 ),
inference(conjunct,[],[normalize_16_0]) ).
fof(normalize_16_2,plain,
op(e3,e3) = e1,
inference(conjunct,[],[normalize_16_0]) ).
fof(normalize_16_3,plain,
op(e3,e1) != e3,
inference(conjunct,[],[normalize_16_0]) ).
fof(normalize_16_4,plain,
$false,
inference(simplify,[],[normalize_16_1,normalize_16_2,normalize_16_3]) ).
cnf(refute_16_0,plain,
$false,
inference(canonicalize,[],[normalize_16_4]) ).
fof(negate_17_0,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 ),
inference(negate,[],[subgoal_17]) ).
fof(normalize_17_0,plain,
( op(e3,e2) != e3
& op(e2,e2) = e3
& op(e3,e3) = e2
& ( 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e0,e2) = e0 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e0,e0) != e3
| op(e3,e3) != e0
| op(e0,e3) = e0 )
& ( op(e0,e0) != e3
| op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e0,e0) != e4
| op(e4,e4) != e0
| op(e0,e4) = e0 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e1,e2) = e1 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e1,e1) != e3
| op(e3,e3) != e1
| op(e1,e3) = e1 )
& ( op(e1,e1) != e3
| op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e1,e1) != e4
| op(e4,e4) != e1
| op(e1,e4) = e1 )
& ( op(e2,e2) != e3
| op(e3,e3) != e2
| op(e2,e3) = e2 )
& ( op(e2,e2) != e4
| op(e4,e4) != e2
| op(e2,e4) = e2 ) ),
inference(canonicalize,[],[negate_17_0]) ).
fof(normalize_17_1,plain,
( op(e3,e3) != e2
| op(e3,e2) = e3 ),
inference(conjunct,[],[normalize_17_0]) ).
fof(normalize_17_2,plain,
op(e3,e3) = e2,
inference(conjunct,[],[normalize_17_0]) ).
fof(normalize_17_3,plain,
op(e3,e2) != e3,
inference(conjunct,[],[normalize_17_0]) ).
fof(normalize_17_4,plain,
$false,
inference(simplify,[],[normalize_17_1,normalize_17_2,normalize_17_3]) ).
cnf(refute_17_0,plain,
$false,
inference(canonicalize,[],[normalize_17_4]) ).
fof(negate_18_0,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 ),
inference(negate,[],[subgoal_18]) ).
fof(normalize_18_0,plain,
$false,
inference(canonicalize,[],[negate_18_0]) ).
cnf(refute_18_0,plain,
$false,
inference(canonicalize,[],[normalize_18_0]) ).
fof(negate_19_0,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 ),
inference(negate,[],[subgoal_19]) ).
fof(normalize_19_0,plain,
( op(e3,e4) != e3
& op(e3,e3) = e4
& op(e4,e4) = e3
& ( 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e0,e2) = e0 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e0,e0) != e3
| op(e3,e3) != e0
| op(e0,e3) = e0 )
& ( op(e0,e0) != e3
| op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e0,e0) != e4
| op(e4,e4) != e0
| op(e0,e4) = e0 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e1,e2) = e1 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e1,e1) != e3
| op(e3,e3) != e1
| op(e1,e3) = e1 )
& ( op(e1,e1) != e3
| op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e1,e1) != e4
| op(e4,e4) != e1
| op(e1,e4) = e1 )
& ( op(e2,e2) != e3
| op(e3,e3) != e2
| op(e2,e3) = e2 )
& ( op(e2,e2) != e3
| op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e2,e2) != e4
| op(e4,e4) != e2
| op(e2,e4) = e2 ) ),
inference(canonicalize,[],[negate_19_0]) ).
fof(normalize_19_1,plain,
( op(e3,e3) != e4
| op(e3,e4) = e3 ),
inference(conjunct,[],[normalize_19_0]) ).
fof(normalize_19_2,plain,
op(e3,e3) = e4,
inference(conjunct,[],[normalize_19_0]) ).
fof(normalize_19_3,plain,
op(e3,e4) != e3,
inference(conjunct,[],[normalize_19_0]) ).
fof(normalize_19_4,plain,
$false,
inference(simplify,[],[normalize_19_1,normalize_19_2,normalize_19_3]) ).
cnf(refute_19_0,plain,
$false,
inference(canonicalize,[],[normalize_19_4]) ).
fof(negate_20_0,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 ),
inference(negate,[],[subgoal_20]) ).
fof(normalize_20_0,plain,
( op(e4,e0) != e4
& op(e0,e0) = e4
& op(e4,e4) = 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e0,e2) = e0 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e0,e0) != e3
| op(e3,e3) != e0
| op(e0,e3) = e0 )
& ( op(e0,e0) != e3
| op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e0,e0) != e4
| op(e4,e4) != e0
| op(e0,e4) = e0 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e1,e2) = e1 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e1,e1) != e3
| op(e3,e3) != e1
| op(e1,e3) = e1 )
& ( op(e1,e1) != e3
| op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e1,e1) != e4
| op(e4,e4) != e1
| op(e1,e4) = e1 )
& ( op(e2,e2) != e3
| op(e3,e3) != e2
| op(e2,e3) = e2 )
& ( op(e2,e2) != e3
| op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e2,e2) != e4
| op(e4,e4) != e2
| op(e2,e4) = e2 )
& ( op(e3,e3) != e4
| op(e4,e4) != e3
| op(e3,e4) = e3 ) ),
inference(canonicalize,[],[negate_20_0]) ).
fof(normalize_20_1,plain,
( op(e4,e4) != e0
| op(e4,e0) = e4 ),
inference(conjunct,[],[normalize_20_0]) ).
fof(normalize_20_2,plain,
op(e4,e4) = e0,
inference(conjunct,[],[normalize_20_0]) ).
fof(normalize_20_3,plain,
op(e4,e0) != e4,
inference(conjunct,[],[normalize_20_0]) ).
fof(normalize_20_4,plain,
$false,
inference(simplify,[],[normalize_20_1,normalize_20_2,normalize_20_3]) ).
cnf(refute_20_0,plain,
$false,
inference(canonicalize,[],[normalize_20_4]) ).
fof(negate_21_0,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 ),
inference(negate,[],[subgoal_21]) ).
fof(normalize_21_0,plain,
( op(e4,e1) != e4
& op(e1,e1) = e4
& op(e4,e4) = e1
& ( 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e0,e2) = e0 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e0,e0) != e3
| op(e3,e3) != e0
| op(e0,e3) = e0 )
& ( op(e0,e0) != e3
| op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e0,e0) != e4
| op(e4,e4) != e0
| op(e0,e4) = e0 )
& ( op(e0,e0) != e4
| op(e4,e4) != e0
| op(e4,e0) = e4 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e1,e2) = e1 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e1,e1) != e3
| op(e3,e3) != e1
| op(e1,e3) = e1 )
& ( op(e1,e1) != e3
| op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e1,e1) != e4
| op(e4,e4) != e1
| op(e1,e4) = e1 )
& ( op(e2,e2) != e3
| op(e3,e3) != e2
| op(e2,e3) = e2 )
& ( op(e2,e2) != e3
| op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e2,e2) != e4
| op(e4,e4) != e2
| op(e2,e4) = e2 )
& ( op(e3,e3) != e4
| op(e4,e4) != e3
| op(e3,e4) = e3 ) ),
inference(canonicalize,[],[negate_21_0]) ).
fof(normalize_21_1,plain,
( op(e4,e4) != e1
| op(e4,e1) = e4 ),
inference(conjunct,[],[normalize_21_0]) ).
fof(normalize_21_2,plain,
op(e4,e4) = e1,
inference(conjunct,[],[normalize_21_0]) ).
fof(normalize_21_3,plain,
op(e4,e1) != e4,
inference(conjunct,[],[normalize_21_0]) ).
fof(normalize_21_4,plain,
$false,
inference(simplify,[],[normalize_21_1,normalize_21_2,normalize_21_3]) ).
cnf(refute_21_0,plain,
$false,
inference(canonicalize,[],[normalize_21_4]) ).
fof(negate_22_0,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 ),
inference(negate,[],[subgoal_22]) ).
fof(normalize_22_0,plain,
( op(e4,e2) != e4
& op(e2,e2) = e4
& op(e4,e4) = e2
& ( 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e0,e2) = e0 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e0,e0) != e3
| op(e3,e3) != e0
| op(e0,e3) = e0 )
& ( op(e0,e0) != e3
| op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e0,e0) != e4
| op(e4,e4) != e0
| op(e0,e4) = e0 )
& ( op(e0,e0) != e4
| op(e4,e4) != e0
| op(e4,e0) = e4 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e1,e2) = e1 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e1,e1) != e3
| op(e3,e3) != e1
| op(e1,e3) = e1 )
& ( op(e1,e1) != e3
| op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e1,e1) != e4
| op(e4,e4) != e1
| op(e1,e4) = e1 )
& ( op(e1,e1) != e4
| op(e4,e4) != e1
| op(e4,e1) = e4 )
& ( op(e2,e2) != e3
| op(e3,e3) != e2
| op(e2,e3) = e2 )
& ( op(e2,e2) != e3
| op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e2,e2) != e4
| op(e4,e4) != e2
| op(e2,e4) = e2 )
& ( op(e3,e3) != e4
| op(e4,e4) != e3
| op(e3,e4) = e3 ) ),
inference(canonicalize,[],[negate_22_0]) ).
fof(normalize_22_1,plain,
( op(e4,e4) != e2
| op(e4,e2) = e4 ),
inference(conjunct,[],[normalize_22_0]) ).
fof(normalize_22_2,plain,
op(e4,e4) = e2,
inference(conjunct,[],[normalize_22_0]) ).
fof(normalize_22_3,plain,
op(e4,e2) != e4,
inference(conjunct,[],[normalize_22_0]) ).
fof(normalize_22_4,plain,
$false,
inference(simplify,[],[normalize_22_1,normalize_22_2,normalize_22_3]) ).
cnf(refute_22_0,plain,
$false,
inference(canonicalize,[],[normalize_22_4]) ).
fof(negate_23_0,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 ),
inference(negate,[],[subgoal_23]) ).
fof(normalize_23_0,plain,
( op(e4,e3) != e4
& op(e3,e3) = e4
& op(e4,e4) = e3
& ( 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) != 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) != 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) != 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(e0,e0) != e1
| op(e1,e1) != e0
| op(e0,e1) = e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e0,e2) = e0 )
& ( op(e0,e0) != e2
| op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e0,e0) != e3
| op(e3,e3) != e0
| op(e0,e3) = e0 )
& ( op(e0,e0) != e3
| op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e0,e0) != e4
| op(e4,e4) != e0
| op(e0,e4) = e0 )
& ( op(e0,e0) != e4
| op(e4,e4) != e0
| op(e4,e0) = e4 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e1,e2) = e1 )
& ( op(e1,e1) != e2
| op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e1,e1) != e3
| op(e3,e3) != e1
| op(e1,e3) = e1 )
& ( op(e1,e1) != e3
| op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e1,e1) != e4
| op(e4,e4) != e1
| op(e1,e4) = e1 )
& ( op(e1,e1) != e4
| op(e4,e4) != e1
| op(e4,e1) = e4 )
& ( op(e2,e2) != e3
| op(e3,e3) != e2
| op(e2,e3) = e2 )
& ( op(e2,e2) != e3
| op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e2,e2) != e4
| op(e4,e4) != e2
| op(e2,e4) = e2 )
& ( op(e2,e2) != e4
| op(e4,e4) != e2
| op(e4,e2) = e4 )
& ( op(e3,e3) != e4
| op(e4,e4) != e3
| op(e3,e4) = e3 ) ),
inference(canonicalize,[],[negate_23_0]) ).
fof(normalize_23_1,plain,
( op(e4,e4) != e3
| op(e4,e3) = e4 ),
inference(conjunct,[],[normalize_23_0]) ).
fof(normalize_23_2,plain,
op(e4,e4) = e3,
inference(conjunct,[],[normalize_23_0]) ).
fof(normalize_23_3,plain,
op(e4,e3) != e4,
inference(conjunct,[],[normalize_23_0]) ).
fof(normalize_23_4,plain,
$false,
inference(simplify,[],[normalize_23_1,normalize_23_2,normalize_23_3]) ).
cnf(refute_23_0,plain,
$false,
inference(canonicalize,[],[normalize_23_4]) ).
fof(negate_24_0,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,[],[subgoal_24]) ).
fof(normalize_24_0,plain,
$false,
inference(canonicalize,[],[negate_24_0]) ).
cnf(refute_24_0,plain,
$false,
inference(canonicalize,[],[normalize_24_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ALG067+1 : TPTP v8.1.0. Released v2.7.0.
% 0.03/0.13 % Command : metis --show proof --show saturation %s
% 0.12/0.34 % Computer : n021.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Wed Jun 8 00:33:06 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 2.12/2.31 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.12/2.31
% 2.12/2.31 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 2.20/2.37
%------------------------------------------------------------------------------