%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : ALG058+1 : TPTP v5.0.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Sat Dec 25 03:49:21 EST 2010
% Result : Theorem 0.54s
% Output : CNFRefutation 0.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 17
% Syntax : Number of formulae : 177 ( 46 unt; 0 def)
% Number of atoms : 4494 (3827 equ)
% Maximal formula atoms : 450 ( 25 avg)
% Number of connectives : 6399 (2082 ~;2495 |;1806 &)
% ( 0 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 8 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 12 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(1,axiom,
( op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& op(unit,e4) = e4
& op(e4,unit) = e4
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3
| unit = e4 ) ),
file('/tmp/tmpugQHcx/sel_ALG058+1.p_1',ax2) ).
fof(2,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0
| op(e0,e4) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0
| op(e4,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| op(e0,e4) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e4,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| op(e0,e4) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2
| op(e4,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3
| op(e0,e4) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3
| op(e4,e0) = e3 )
& ( op(e0,e0) = e4
| op(e0,e1) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e4) = e4 )
& ( op(e0,e0) = e4
| op(e1,e0) = e4
| op(e2,e0) = e4
| op(e3,e0) = e4
| op(e4,e0) = e4 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0
| op(e1,e4) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0
| op(e4,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1
| op(e1,e4) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1
| op(e4,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2
| op(e1,e4) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2
| op(e4,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3
| op(e1,e4) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3
| op(e4,e1) = e3 )
& ( op(e1,e0) = e4
| op(e1,e1) = e4
| op(e1,e2) = e4
| op(e1,e3) = e4
| op(e1,e4) = e4 )
& ( op(e0,e1) = e4
| op(e1,e1) = e4
| op(e2,e1) = e4
| op(e3,e1) = e4
| op(e4,e1) = e4 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0
| op(e2,e4) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0
| op(e4,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1
| op(e2,e4) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1
| op(e4,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2
| op(e2,e4) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2
| op(e4,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| op(e2,e4) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3
| op(e4,e2) = e3 )
& ( op(e2,e0) = e4
| op(e2,e1) = e4
| op(e2,e2) = e4
| op(e2,e3) = e4
| op(e2,e4) = e4 )
& ( op(e0,e2) = e4
| op(e1,e2) = e4
| op(e2,e2) = e4
| op(e3,e2) = e4
| op(e4,e2) = e4 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0
| op(e3,e4) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0
| op(e4,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1
| op(e3,e4) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1
| op(e4,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| op(e3,e4) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2
| op(e4,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3
| op(e3,e4) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3
| op(e4,e3) = e3 )
& ( op(e3,e0) = e4
| op(e3,e1) = e4
| op(e3,e2) = e4
| op(e3,e3) = e4
| op(e3,e4) = e4 )
& ( op(e0,e3) = e4
| op(e1,e3) = e4
| op(e2,e3) = e4
| op(e3,e3) = e4
| op(e4,e3) = e4 )
& ( op(e4,e0) = e0
| op(e4,e1) = e0
| op(e4,e2) = e0
| op(e4,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e4) = e0
| op(e1,e4) = e0
| op(e2,e4) = e0
| op(e3,e4) = e0
| op(e4,e4) = e0 )
& ( op(e4,e0) = e1
| op(e4,e1) = e1
| op(e4,e2) = e1
| op(e4,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e4) = e1
| op(e1,e4) = e1
| op(e2,e4) = e1
| op(e3,e4) = e1
| op(e4,e4) = e1 )
& ( op(e4,e0) = e2
| op(e4,e1) = e2
| op(e4,e2) = e2
| op(e4,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e4) = e2
| op(e1,e4) = e2
| op(e2,e4) = e2
| op(e3,e4) = e2
| op(e4,e4) = e2 )
& ( op(e4,e0) = e3
| op(e4,e1) = e3
| op(e4,e2) = e3
| op(e4,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e4) = e3
| op(e1,e4) = e3
| op(e2,e4) = e3
| op(e3,e4) = e3
| op(e4,e4) = e3 )
& ( op(e4,e0) = e4
| op(e4,e1) = e4
| op(e4,e2) = e4
| op(e4,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e4) = e4
| op(e1,e4) = e4
| op(e2,e4) = e4
| op(e3,e4) = e4
| op(e4,e4) = e4 ) ),
file('/tmp/tmpugQHcx/sel_ALG058+1.p_1',ax3) ).
fof(4,axiom,
( e0 = op(op(op(e2,e2),e2),op(op(e2,e2),e2))
& e1 = op(op(e2,e2),e2)
& e3 = op(e2,e2)
& e4 = op(op(e2,e2),op(e2,e2)) ),
file('/tmp/tmpugQHcx/sel_ALG058+1.p_1',ax6) ).
fof(5,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e4,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e4,e0)
& op(e2,e0) != op(e3,e0)
& op(e2,e0) != op(e4,e0)
& op(e3,e0) != op(e4,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e4,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e4,e1)
& op(e2,e1) != op(e3,e1)
& op(e2,e1) != op(e4,e1)
& op(e3,e1) != op(e4,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e4,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e4,e2)
& op(e2,e2) != op(e3,e2)
& op(e2,e2) != op(e4,e2)
& op(e3,e2) != op(e4,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e4,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e4,e3)
& op(e2,e3) != op(e3,e3)
& op(e2,e3) != op(e4,e3)
& op(e3,e3) != op(e4,e3)
& op(e0,e4) != op(e1,e4)
& op(e0,e4) != op(e2,e4)
& op(e0,e4) != op(e3,e4)
& op(e0,e4) != op(e4,e4)
& op(e1,e4) != op(e2,e4)
& op(e1,e4) != op(e3,e4)
& op(e1,e4) != op(e4,e4)
& op(e2,e4) != op(e3,e4)
& op(e2,e4) != op(e4,e4)
& op(e3,e4) != op(e4,e4)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e4)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e4)
& op(e0,e2) != op(e0,e3)
& op(e0,e2) != op(e0,e4)
& op(e0,e3) != op(e0,e4)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e4)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e4)
& op(e1,e2) != op(e1,e3)
& op(e1,e2) != op(e1,e4)
& op(e1,e3) != op(e1,e4)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e4)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e4)
& op(e2,e2) != op(e2,e3)
& op(e2,e2) != op(e2,e4)
& op(e2,e3) != op(e2,e4)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e4)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e4)
& op(e3,e2) != op(e3,e3)
& op(e3,e2) != op(e3,e4)
& op(e3,e3) != op(e3,e4)
& op(e4,e0) != op(e4,e1)
& op(e4,e0) != op(e4,e2)
& op(e4,e0) != op(e4,e3)
& op(e4,e0) != op(e4,e4)
& op(e4,e1) != op(e4,e2)
& op(e4,e1) != op(e4,e3)
& op(e4,e1) != op(e4,e4)
& op(e4,e2) != op(e4,e3)
& op(e4,e2) != op(e4,e4)
& op(e4,e3) != op(e4,e4) ),
file('/tmp/tmpugQHcx/sel_ALG058+1.p_1',ax4) ).
fof(6,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e0 != e4
& e1 != e2
& e1 != e3
& e1 != e4
& e2 != e3
& e2 != e4
& e3 != e4 ),
file('/tmp/tmpugQHcx/sel_ALG058+1.p_1',ax5) ).
fof(7,conjecture,
~ ( ( ( ( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit ) )
& ( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit ) )
& ( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit ) )
& ( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit ) )
& ( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit ) )
& ( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit ) )
& ( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit ) )
& ( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit ) )
& ( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit ) )
& ( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit ) )
& ( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit ) )
& ( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit ) )
& ( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit ) )
& ( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit ) )
& ( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit ) )
& ( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit ) )
& ( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit ) )
& ( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit ) )
& ( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit ) )
& ( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit ) )
& ( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit ) )
& ( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit ) )
& ( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit ) )
& ( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit ) )
& ( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit ) ) )
| ( ( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit ) )
& ( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit ) )
& ( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit ) )
& ( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit ) )
& ( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit ) )
& ( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit ) )
& ( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit ) )
& ( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit ) )
& ( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit ) )
& ( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit ) )
& ( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit ) )
& ( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit ) )
& ( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit ) )
& ( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit ) )
& ( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit ) )
& ( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit ) )
& ( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit ) )
& ( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit ) )
& ( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit ) )
& ( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit ) )
& ( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit ) )
& ( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit ) )
& ( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit ) )
& ( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit ) )
& ( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit ) ) )
| ( ( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit ) )
& ( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit ) )
& ( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit ) )
& ( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit ) )
& ( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit ) )
& ( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit ) )
& ( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit ) )
& ( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit ) )
& ( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit ) )
& ( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit ) )
& ( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit ) )
& ( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit ) )
& ( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit ) )
& ( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit ) )
& ( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit ) )
& ( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit ) )
& ( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit ) )
& ( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit ) )
& ( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit ) )
& ( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit ) )
& ( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit ) )
& ( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit ) )
& ( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit ) )
& ( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit ) )
& ( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit ) ) )
| ( ( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit ) )
& ( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit ) )
& ( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit ) )
& ( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit ) )
& ( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit ) )
& ( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit ) )
& ( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit ) )
& ( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit ) )
& ( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit ) )
& ( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit ) )
& ( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit ) )
& ( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit ) )
& ( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit ) )
& ( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit ) )
& ( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit ) )
& ( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit ) )
& ( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit ) )
& ( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit ) )
& ( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit ) )
& ( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit ) )
& ( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit ) )
& ( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit ) )
& ( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit ) )
& ( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit ) )
& ( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit ) ) )
| ( ( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit ) )
& ( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit ) )
& ( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit ) )
& ( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit ) )
& ( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit ) )
& ( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit ) )
& ( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit ) )
& ( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit ) )
& ( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit ) )
& ( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit ) )
& ( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit ) )
& ( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit ) )
& ( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit ) )
& ( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit ) )
& ( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit ) )
& ( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit ) )
& ( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit ) )
& ( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit ) )
& ( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit ) )
& ( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit ) )
& ( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit ) )
& ( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit ) )
& ( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit ) )
& ( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit ) )
& ( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit ) ) ) )
& ( ( op(e0,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 ) ) ),
file('/tmp/tmpugQHcx/sel_ALG058+1.p_1',co1) ).
fof(8,negated_conjecture,
~ ~ ( ( ( ( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit ) )
& ( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit ) )
& ( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit ) )
& ( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit ) )
& ( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit ) )
& ( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit ) )
& ( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit ) )
& ( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit ) )
& ( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit ) )
& ( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit ) )
& ( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit ) )
& ( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit ) )
& ( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit ) )
& ( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit ) )
& ( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit ) )
& ( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit ) )
& ( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit ) )
& ( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit ) )
& ( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit ) )
& ( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit ) )
& ( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit ) )
& ( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit ) )
& ( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit ) )
& ( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit ) )
& ( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit ) ) )
| ( ( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit ) )
& ( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit ) )
& ( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit ) )
& ( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit ) )
& ( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit ) )
& ( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit ) )
& ( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit ) )
& ( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit ) )
& ( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit ) )
& ( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit ) )
& ( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit ) )
& ( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit ) )
& ( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit ) )
& ( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit ) )
& ( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit ) )
& ( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit ) )
& ( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit ) )
& ( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit ) )
& ( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit ) )
& ( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit ) )
& ( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit ) )
& ( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit ) )
& ( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit ) )
& ( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit ) )
& ( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit ) ) )
| ( ( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit ) )
& ( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit ) )
& ( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit ) )
& ( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit ) )
& ( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit ) )
& ( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit ) )
& ( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit ) )
& ( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit ) )
& ( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit ) )
& ( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit ) )
& ( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit ) )
& ( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit ) )
& ( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit ) )
& ( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit ) )
& ( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit ) )
& ( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit ) )
& ( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit ) )
& ( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit ) )
& ( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit ) )
& ( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit ) )
& ( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit ) )
& ( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit ) )
& ( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit ) )
& ( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit ) )
& ( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit ) ) )
| ( ( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit ) )
& ( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit ) )
& ( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit ) )
& ( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit ) )
& ( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit ) )
& ( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit ) )
& ( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit ) )
& ( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit ) )
& ( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit ) )
& ( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit ) )
& ( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit ) )
& ( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit ) )
& ( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit ) )
& ( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit ) )
& ( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit ) )
& ( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit ) )
& ( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit ) )
& ( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit ) )
& ( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit ) )
& ( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit ) )
& ( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit ) )
& ( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit ) )
& ( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit ) )
& ( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit ) )
& ( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit ) ) )
| ( ( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit ) )
& ( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit ) )
& ( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit ) )
& ( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit ) )
& ( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit ) )
& ( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit ) )
& ( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit ) )
& ( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit ) )
& ( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit ) )
& ( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit ) )
& ( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit ) )
& ( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit ) )
& ( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit ) )
& ( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit ) )
& ( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit ) )
& ( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit ) )
& ( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit ) )
& ( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit ) )
& ( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit ) )
& ( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit ) )
& ( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit ) )
& ( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit ) )
& ( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit ) )
& ( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit ) )
& ( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit ) ) ) )
& ( ( 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(assume_negation,[status(cth)],[7]) ).
fof(9,negated_conjecture,
~ ~ ( ( ( ( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit ) )
& ( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit ) )
& ( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit ) )
& ( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit ) )
& ( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit ) )
& ( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit ) )
& ( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit ) )
& ( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit ) )
& ( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit ) )
& ( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit ) )
& ( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit ) )
& ( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit ) )
& ( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit ) )
& ( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit ) )
& ( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit ) )
& ( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit ) )
& ( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit ) )
& ( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit ) )
& ( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit ) )
& ( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit ) )
& ( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit ) )
& ( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit ) )
& ( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit ) )
& ( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit ) )
& ( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit ) ) )
| ( ( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit ) )
& ( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit ) )
& ( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit ) )
& ( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit ) )
& ( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit ) )
& ( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit ) )
& ( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit ) )
& ( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit ) )
& ( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit ) )
& ( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit ) )
& ( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit ) )
& ( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit ) )
& ( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit ) )
& ( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit ) )
& ( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit ) )
& ( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit ) )
& ( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit ) )
& ( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit ) )
& ( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit ) )
& ( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit ) )
& ( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit ) )
& ( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit ) )
& ( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit ) )
& ( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit ) )
& ( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit ) ) )
| ( ( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit ) )
& ( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit ) )
& ( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit ) )
& ( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit ) )
& ( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit ) )
& ( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit ) )
& ( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit ) )
& ( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit ) )
& ( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit ) )
& ( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit ) )
& ( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit ) )
& ( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit ) )
& ( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit ) )
& ( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit ) )
& ( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit ) )
& ( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit ) )
& ( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit ) )
& ( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit ) )
& ( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit ) )
& ( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit ) )
& ( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit ) )
& ( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit ) )
& ( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit ) )
& ( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit ) )
& ( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit ) ) )
| ( ( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit ) )
& ( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit ) )
& ( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit ) )
& ( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit ) )
& ( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit ) )
& ( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit ) )
& ( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit ) )
& ( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit ) )
& ( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit ) )
& ( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit ) )
& ( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit ) )
& ( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit ) )
& ( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit ) )
& ( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit ) )
& ( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit ) )
& ( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit ) )
& ( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit ) )
& ( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit ) )
& ( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit ) )
& ( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit ) )
& ( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit ) )
& ( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit ) )
& ( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit ) )
& ( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit ) )
& ( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit ) ) )
| ( ( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit ) )
& ( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit ) )
& ( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit ) )
& ( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit ) )
& ( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit ) )
& ( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit ) )
& ( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit ) )
& ( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit ) )
& ( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit ) )
& ( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit ) )
& ( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit ) )
& ( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit ) )
& ( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit ) )
& ( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit ) )
& ( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit ) )
& ( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit ) )
& ( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit ) )
& ( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit ) )
& ( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit ) )
& ( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit ) )
& ( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit ) )
& ( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit ) )
& ( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit ) )
& ( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit ) )
& ( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit ) ) ) )
& ( ( 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) = 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) = 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) = 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 ) ) ),
inference(fof_simplification,[status(thm)],[8,theory(equality)]) ).
fof(10,plain,
( epred1_0
=> ( ( op(e0,e0) != e0
| ( op(e0,e0) = e0
& e0 != unit ) )
& ( op(e0,e1) != e0
| ( op(e0,e0) = e1
& e0 != unit ) )
& ( op(e0,e2) != e0
| ( op(e0,e0) = e2
& e0 != unit ) )
& ( op(e0,e3) != e0
| ( op(e0,e0) = e3
& e0 != unit ) )
& ( op(e0,e4) != e0
| ( op(e0,e0) = e4
& e0 != unit ) )
& ( op(e1,e0) != e0
| ( op(e1,e0) = e0
& e0 != unit ) )
& ( op(e1,e1) != e0
| ( op(e1,e0) = e1
& e0 != unit ) )
& ( op(e1,e2) != e0
| ( op(e1,e0) = e2
& e0 != unit ) )
& ( op(e1,e3) != e0
| ( op(e1,e0) = e3
& e0 != unit ) )
& ( op(e1,e4) != e0
| ( op(e1,e0) = e4
& e0 != unit ) )
& ( op(e2,e0) != e0
| ( op(e2,e0) = e0
& e0 != unit ) )
& ( op(e2,e1) != e0
| ( op(e2,e0) = e1
& e0 != unit ) )
& ( op(e2,e2) != e0
| ( op(e2,e0) = e2
& e0 != unit ) )
& ( op(e2,e3) != e0
| ( op(e2,e0) = e3
& e0 != unit ) )
& ( op(e2,e4) != e0
| ( op(e2,e0) = e4
& e0 != unit ) )
& ( op(e3,e0) != e0
| ( op(e3,e0) = e0
& e0 != unit ) )
& ( op(e3,e1) != e0
| ( op(e3,e0) = e1
& e0 != unit ) )
& ( op(e3,e2) != e0
| ( op(e3,e0) = e2
& e0 != unit ) )
& ( op(e3,e3) != e0
| ( op(e3,e0) = e3
& e0 != unit ) )
& ( op(e3,e4) != e0
| ( op(e3,e0) = e4
& e0 != unit ) )
& ( op(e4,e0) != e0
| ( op(e4,e0) = e0
& e0 != unit ) )
& ( op(e4,e1) != e0
| ( op(e4,e0) = e1
& e0 != unit ) )
& ( op(e4,e2) != e0
| ( op(e4,e0) = e2
& e0 != unit ) )
& ( op(e4,e3) != e0
| ( op(e4,e0) = e3
& e0 != unit ) )
& ( op(e4,e4) != e0
| ( op(e4,e0) = e4
& e0 != unit ) ) ) ),
introduced(definition) ).
fof(11,plain,
( epred2_0
=> ( ( op(e0,e0) != e1
| ( op(e0,e1) = e0
& e1 != unit ) )
& ( op(e0,e1) != e1
| ( op(e0,e1) = e1
& e1 != unit ) )
& ( op(e0,e2) != e1
| ( op(e0,e1) = e2
& e1 != unit ) )
& ( op(e0,e3) != e1
| ( op(e0,e1) = e3
& e1 != unit ) )
& ( op(e0,e4) != e1
| ( op(e0,e1) = e4
& e1 != unit ) )
& ( op(e1,e0) != e1
| ( op(e1,e1) = e0
& e1 != unit ) )
& ( op(e1,e1) != e1
| ( op(e1,e1) = e1
& e1 != unit ) )
& ( op(e1,e2) != e1
| ( op(e1,e1) = e2
& e1 != unit ) )
& ( op(e1,e3) != e1
| ( op(e1,e1) = e3
& e1 != unit ) )
& ( op(e1,e4) != e1
| ( op(e1,e1) = e4
& e1 != unit ) )
& ( op(e2,e0) != e1
| ( op(e2,e1) = e0
& e1 != unit ) )
& ( op(e2,e1) != e1
| ( op(e2,e1) = e1
& e1 != unit ) )
& ( op(e2,e2) != e1
| ( op(e2,e1) = e2
& e1 != unit ) )
& ( op(e2,e3) != e1
| ( op(e2,e1) = e3
& e1 != unit ) )
& ( op(e2,e4) != e1
| ( op(e2,e1) = e4
& e1 != unit ) )
& ( op(e3,e0) != e1
| ( op(e3,e1) = e0
& e1 != unit ) )
& ( op(e3,e1) != e1
| ( op(e3,e1) = e1
& e1 != unit ) )
& ( op(e3,e2) != e1
| ( op(e3,e1) = e2
& e1 != unit ) )
& ( op(e3,e3) != e1
| ( op(e3,e1) = e3
& e1 != unit ) )
& ( op(e3,e4) != e1
| ( op(e3,e1) = e4
& e1 != unit ) )
& ( op(e4,e0) != e1
| ( op(e4,e1) = e0
& e1 != unit ) )
& ( op(e4,e1) != e1
| ( op(e4,e1) = e1
& e1 != unit ) )
& ( op(e4,e2) != e1
| ( op(e4,e1) = e2
& e1 != unit ) )
& ( op(e4,e3) != e1
| ( op(e4,e1) = e3
& e1 != unit ) )
& ( op(e4,e4) != e1
| ( op(e4,e1) = e4
& e1 != unit ) ) ) ),
introduced(definition) ).
fof(12,plain,
( epred3_0
=> ( ( op(e0,e0) != e2
| ( op(e0,e2) = e0
& e2 != unit ) )
& ( op(e0,e1) != e2
| ( op(e0,e2) = e1
& e2 != unit ) )
& ( op(e0,e2) != e2
| ( op(e0,e2) = e2
& e2 != unit ) )
& ( op(e0,e3) != e2
| ( op(e0,e2) = e3
& e2 != unit ) )
& ( op(e0,e4) != e2
| ( op(e0,e2) = e4
& e2 != unit ) )
& ( op(e1,e0) != e2
| ( op(e1,e2) = e0
& e2 != unit ) )
& ( op(e1,e1) != e2
| ( op(e1,e2) = e1
& e2 != unit ) )
& ( op(e1,e2) != e2
| ( op(e1,e2) = e2
& e2 != unit ) )
& ( op(e1,e3) != e2
| ( op(e1,e2) = e3
& e2 != unit ) )
& ( op(e1,e4) != e2
| ( op(e1,e2) = e4
& e2 != unit ) )
& ( op(e2,e0) != e2
| ( op(e2,e2) = e0
& e2 != unit ) )
& ( op(e2,e1) != e2
| ( op(e2,e2) = e1
& e2 != unit ) )
& ( op(e2,e2) != e2
| ( op(e2,e2) = e2
& e2 != unit ) )
& ( op(e2,e3) != e2
| ( op(e2,e2) = e3
& e2 != unit ) )
& ( op(e2,e4) != e2
| ( op(e2,e2) = e4
& e2 != unit ) )
& ( op(e3,e0) != e2
| ( op(e3,e2) = e0
& e2 != unit ) )
& ( op(e3,e1) != e2
| ( op(e3,e2) = e1
& e2 != unit ) )
& ( op(e3,e2) != e2
| ( op(e3,e2) = e2
& e2 != unit ) )
& ( op(e3,e3) != e2
| ( op(e3,e2) = e3
& e2 != unit ) )
& ( op(e3,e4) != e2
| ( op(e3,e2) = e4
& e2 != unit ) )
& ( op(e4,e0) != e2
| ( op(e4,e2) = e0
& e2 != unit ) )
& ( op(e4,e1) != e2
| ( op(e4,e2) = e1
& e2 != unit ) )
& ( op(e4,e2) != e2
| ( op(e4,e2) = e2
& e2 != unit ) )
& ( op(e4,e3) != e2
| ( op(e4,e2) = e3
& e2 != unit ) )
& ( op(e4,e4) != e2
| ( op(e4,e2) = e4
& e2 != unit ) ) ) ),
introduced(definition) ).
fof(13,plain,
( epred4_0
=> ( ( op(e0,e0) != e3
| ( op(e0,e3) = e0
& e3 != unit ) )
& ( op(e0,e1) != e3
| ( op(e0,e3) = e1
& e3 != unit ) )
& ( op(e0,e2) != e3
| ( op(e0,e3) = e2
& e3 != unit ) )
& ( op(e0,e3) != e3
| ( op(e0,e3) = e3
& e3 != unit ) )
& ( op(e0,e4) != e3
| ( op(e0,e3) = e4
& e3 != unit ) )
& ( op(e1,e0) != e3
| ( op(e1,e3) = e0
& e3 != unit ) )
& ( op(e1,e1) != e3
| ( op(e1,e3) = e1
& e3 != unit ) )
& ( op(e1,e2) != e3
| ( op(e1,e3) = e2
& e3 != unit ) )
& ( op(e1,e3) != e3
| ( op(e1,e3) = e3
& e3 != unit ) )
& ( op(e1,e4) != e3
| ( op(e1,e3) = e4
& e3 != unit ) )
& ( op(e2,e0) != e3
| ( op(e2,e3) = e0
& e3 != unit ) )
& ( op(e2,e1) != e3
| ( op(e2,e3) = e1
& e3 != unit ) )
& ( op(e2,e2) != e3
| ( op(e2,e3) = e2
& e3 != unit ) )
& ( op(e2,e3) != e3
| ( op(e2,e3) = e3
& e3 != unit ) )
& ( op(e2,e4) != e3
| ( op(e2,e3) = e4
& e3 != unit ) )
& ( op(e3,e0) != e3
| ( op(e3,e3) = e0
& e3 != unit ) )
& ( op(e3,e1) != e3
| ( op(e3,e3) = e1
& e3 != unit ) )
& ( op(e3,e2) != e3
| ( op(e3,e3) = e2
& e3 != unit ) )
& ( op(e3,e3) != e3
| ( op(e3,e3) = e3
& e3 != unit ) )
& ( op(e3,e4) != e3
| ( op(e3,e3) = e4
& e3 != unit ) )
& ( op(e4,e0) != e3
| ( op(e4,e3) = e0
& e3 != unit ) )
& ( op(e4,e1) != e3
| ( op(e4,e3) = e1
& e3 != unit ) )
& ( op(e4,e2) != e3
| ( op(e4,e3) = e2
& e3 != unit ) )
& ( op(e4,e3) != e3
| ( op(e4,e3) = e3
& e3 != unit ) )
& ( op(e4,e4) != e3
| ( op(e4,e3) = e4
& e3 != unit ) ) ) ),
introduced(definition) ).
fof(14,plain,
( epred5_0
=> ( ( op(e0,e0) != e4
| ( op(e0,e4) = e0
& e4 != unit ) )
& ( op(e0,e1) != e4
| ( op(e0,e4) = e1
& e4 != unit ) )
& ( op(e0,e2) != e4
| ( op(e0,e4) = e2
& e4 != unit ) )
& ( op(e0,e3) != e4
| ( op(e0,e4) = e3
& e4 != unit ) )
& ( op(e0,e4) != e4
| ( op(e0,e4) = e4
& e4 != unit ) )
& ( op(e1,e0) != e4
| ( op(e1,e4) = e0
& e4 != unit ) )
& ( op(e1,e1) != e4
| ( op(e1,e4) = e1
& e4 != unit ) )
& ( op(e1,e2) != e4
| ( op(e1,e4) = e2
& e4 != unit ) )
& ( op(e1,e3) != e4
| ( op(e1,e4) = e3
& e4 != unit ) )
& ( op(e1,e4) != e4
| ( op(e1,e4) = e4
& e4 != unit ) )
& ( op(e2,e0) != e4
| ( op(e2,e4) = e0
& e4 != unit ) )
& ( op(e2,e1) != e4
| ( op(e2,e4) = e1
& e4 != unit ) )
& ( op(e2,e2) != e4
| ( op(e2,e4) = e2
& e4 != unit ) )
& ( op(e2,e3) != e4
| ( op(e2,e4) = e3
& e4 != unit ) )
& ( op(e2,e4) != e4
| ( op(e2,e4) = e4
& e4 != unit ) )
& ( op(e3,e0) != e4
| ( op(e3,e4) = e0
& e4 != unit ) )
& ( op(e3,e1) != e4
| ( op(e3,e4) = e1
& e4 != unit ) )
& ( op(e3,e2) != e4
| ( op(e3,e4) = e2
& e4 != unit ) )
& ( op(e3,e3) != e4
| ( op(e3,e4) = e3
& e4 != unit ) )
& ( op(e3,e4) != e4
| ( op(e3,e4) = e4
& e4 != unit ) )
& ( op(e4,e0) != e4
| ( op(e4,e4) = e0
& e4 != unit ) )
& ( op(e4,e1) != e4
| ( op(e4,e4) = e1
& e4 != unit ) )
& ( op(e4,e2) != e4
| ( op(e4,e4) = e2
& e4 != unit ) )
& ( op(e4,e3) != e4
| ( op(e4,e4) = e3
& e4 != unit ) )
& ( op(e4,e4) != e4
| ( op(e4,e4) = e4
& e4 != unit ) ) ) ),
introduced(definition) ).
fof(15,plain,
( epred6_0
=> ( ( 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 ) ) ),
introduced(definition) ).
fof(16,plain,
( epred7_0
=> ( ( 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) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 ) ) ),
introduced(definition) ).
fof(17,plain,
( epred8_0
=> ( ( 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) = 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 ) ) ),
introduced(definition) ).
fof(18,plain,
( epred9_0
=> ( ( 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) = 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) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 ) ) ),
introduced(definition) ).
fof(19,plain,
( epred10_0
=> ( ( 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) = 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) = 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 ) ) ),
introduced(definition) ).
fof(20,plain,
( epred11_0
=> ( ( 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) = 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) = 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) = 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 ) ) ),
introduced(definition) ).
fof(21,negated_conjecture,
~ ~ ( ( epred1_0
| epred2_0
| epred3_0
| epred4_0
| epred5_0 )
& ( epred11_0
| ( 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 ) ) ),
inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[9,10,theory(equality)]),11,theory(equality)]),12,theory(equality)]),13,theory(equality)]),14,theory(equality)]),20,theory(equality)]) ).
fof(22,plain,
( epred7_0
=> ( epred6_0
| ( 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) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 ) ) ),
inference(apply_def,[status(esa)],[16,15,theory(equality)]) ).
fof(23,plain,
( epred8_0
=> ( epred7_0
| ( 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(apply_def,[status(esa)],[17,22,theory(equality)]) ).
fof(24,plain,
( epred9_0
=> ( epred8_0
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != 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(apply_def,[status(esa)],[18,23,theory(equality)]) ).
fof(25,plain,
( epred10_0
=> ( epred9_0
| ( 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(apply_def,[status(esa)],[19,24,theory(equality)]) ).
fof(26,plain,
( epred11_0
=> ( epred10_0
| ( 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(apply_def,[status(esa)],[20,25,theory(equality)]) ).
cnf(27,plain,
( unit = e4
| unit = e3
| unit = e2
| unit = e1
| unit = e0 ),
inference(split_conjunct,[status(thm)],[1]) ).
cnf(31,plain,
op(unit,e3) = e3,
inference(split_conjunct,[status(thm)],[1]) ).
cnf(33,plain,
op(unit,e2) = e2,
inference(split_conjunct,[status(thm)],[1]) ).
cnf(34,plain,
op(e1,unit) = e1,
inference(split_conjunct,[status(thm)],[1]) ).
cnf(35,plain,
op(unit,e1) = e1,
inference(split_conjunct,[status(thm)],[1]) ).
cnf(36,plain,
op(e0,unit) = e0,
inference(split_conjunct,[status(thm)],[1]) ).
cnf(37,plain,
op(unit,e0) = e0,
inference(split_conjunct,[status(thm)],[1]) ).
cnf(57,plain,
( op(e3,e4) = e0
| op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(split_conjunct,[status(thm)],[2]) ).
cnf(71,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 ),
inference(split_conjunct,[status(thm)],[2]) ).
cnf(113,plain,
e4 = op(op(e2,e2),op(e2,e2)),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(114,plain,
e3 = op(e2,e2),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(115,plain,
e1 = op(op(e2,e2),e2),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(116,plain,
e0 = op(op(op(e2,e2),e2),op(op(e2,e2),e2)),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(132,plain,
op(e3,e1) != op(e3,e2),
inference(split_conjunct,[status(thm)],[5]) ).
cnf(156,plain,
op(e1,e0) != op(e1,e1),
inference(split_conjunct,[status(thm)],[5]) ).
cnf(170,plain,
op(e1,e4) != op(e4,e4),
inference(split_conjunct,[status(thm)],[5]) ).
cnf(174,plain,
op(e0,e4) != op(e3,e4),
inference(split_conjunct,[status(thm)],[5]) ).
cnf(186,plain,
op(e0,e3) != op(e1,e3),
inference(split_conjunct,[status(thm)],[5]) ).
cnf(192,plain,
op(e1,e2) != op(e2,e2),
inference(split_conjunct,[status(thm)],[5]) ).
cnf(201,plain,
op(e1,e1) != op(e3,e1),
inference(split_conjunct,[status(thm)],[5]) ).
cnf(207,plain,
op(e3,e0) != op(e4,e0),
inference(split_conjunct,[status(thm)],[5]) ).
cnf(217,plain,
e3 != e4,
inference(split_conjunct,[status(thm)],[6]) ).
cnf(218,plain,
e2 != e4,
inference(split_conjunct,[status(thm)],[6]) ).
cnf(219,plain,
e2 != e3,
inference(split_conjunct,[status(thm)],[6]) ).
cnf(220,plain,
e1 != e4,
inference(split_conjunct,[status(thm)],[6]) ).
cnf(221,plain,
e1 != e3,
inference(split_conjunct,[status(thm)],[6]) ).
cnf(223,plain,
e0 != e4,
inference(split_conjunct,[status(thm)],[6]) ).
cnf(224,plain,
e0 != e3,
inference(split_conjunct,[status(thm)],[6]) ).
cnf(225,plain,
e0 != e2,
inference(split_conjunct,[status(thm)],[6]) ).
cnf(226,plain,
e0 != e1,
inference(split_conjunct,[status(thm)],[6]) ).
fof(227,negated_conjecture,
( ( epred1_0
| epred2_0
| epred3_0
| epred4_0
| epred5_0 )
& ( epred11_0
| ( 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 ) ) ),
inference(fof_nnf,[status(thm)],[21]) ).
fof(228,negated_conjecture,
( ( epred1_0
| epred2_0
| epred3_0
| epred4_0
| epred5_0 )
& ( op(e4,e4) = e4
| op(e4,e4) = e3
| op(e4,e4) = e2
| epred11_0 )
& ( op(e4,e4) != e4
| op(e4,e4) = e3
| op(e4,e4) = e2
| epred11_0 )
& ( op(e4,e4) = e4
| op(e3,e3) = e4
| op(e4,e4) = e2
| epred11_0 )
& ( op(e4,e4) != e4
| op(e3,e3) = e4
| op(e4,e4) = e2
| epred11_0 )
& ( op(e4,e4) = e4
| op(e4,e3) != e4
| op(e4,e4) = e2
| epred11_0 )
& ( op(e4,e4) != e4
| op(e4,e3) != e4
| op(e4,e4) = e2
| epred11_0 )
& ( op(e4,e4) = e4
| op(e4,e4) = e3
| op(e2,e2) = e4
| epred11_0 )
& ( op(e4,e4) != e4
| op(e4,e4) = e3
| op(e2,e2) = e4
| epred11_0 )
& ( op(e4,e4) = e4
| op(e3,e3) = e4
| op(e2,e2) = e4
| epred11_0 )
& ( op(e4,e4) != e4
| op(e3,e3) = e4
| op(e2,e2) = e4
| epred11_0 )
& ( op(e4,e4) = e4
| op(e4,e3) != e4
| op(e2,e2) = e4
| epred11_0 )
& ( op(e4,e4) != e4
| op(e4,e3) != e4
| op(e2,e2) = e4
| epred11_0 )
& ( op(e4,e4) = e4
| op(e4,e4) = e3
| op(e4,e2) != e4
| epred11_0 )
& ( op(e4,e4) != e4
| op(e4,e4) = e3
| op(e4,e2) != e4
| epred11_0 )
& ( op(e4,e4) = e4
| op(e3,e3) = e4
| op(e4,e2) != e4
| epred11_0 )
& ( op(e4,e4) != e4
| op(e3,e3) = e4
| op(e4,e2) != e4
| epred11_0 )
& ( op(e4,e4) = e4
| op(e4,e3) != e4
| op(e4,e2) != e4
| epred11_0 )
& ( op(e4,e4) != e4
| op(e4,e3) != e4
| op(e4,e2) != e4
| epred11_0 ) ),
inference(distribute,[status(thm)],[227]) ).
cnf(239,negated_conjecture,
( epred11_0
| op(e2,e2) = e4
| op(e4,e4) = e3
| op(e4,e4) != e4 ),
inference(split_conjunct,[status(thm)],[228]) ).
cnf(240,negated_conjecture,
( epred11_0
| op(e2,e2) = e4
| op(e4,e4) = e3
| op(e4,e4) = e4 ),
inference(split_conjunct,[status(thm)],[228]) ).
fof(508,plain,
( ~ epred6_0
| ( 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(fof_nnf,[status(thm)],[15]) ).
fof(509,plain,
( ( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e2,e2) = e0
| op(e0,e0) = e1
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e0,e0) = e1
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e2,e2) = e0
| op(e0,e0) = e1
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e0,e2) != e0
| op(e0,e0) = e1
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e0,e2) != e0
| op(e0,e0) = e1
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e0,e2) != e0
| op(e0,e0) = e1
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e1,e1) = e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e0,e0) = e2
| op(e1,e1) = e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e0,e0) = e2
| op(e1,e1) = e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e0,e2) != e0
| op(e1,e1) = e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e0,e2) != e0
| op(e1,e1) = e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e0,e2) != e0
| op(e1,e1) = e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e1) != e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e0,e0) = e2
| op(e0,e1) != e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e0,e0) = e2
| op(e0,e1) != e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e2,e2) = e0
| op(e0,e1) != e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e0,e1) != e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e2,e2) = e0
| op(e0,e1) != e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e0,e2) != e0
| op(e0,e1) != e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e0,e2) != e0
| op(e0,e1) != e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e0,e2) != e0
| op(e0,e1) != e0
| op(e0,e0) = e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e2,e2) = e0
| op(e0,e0) = e1
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e0,e0) = e1
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e2,e2) = e0
| op(e0,e0) = e1
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e0,e2) != e0
| op(e0,e0) = e1
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e0,e2) != e0
| op(e0,e0) = e1
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e0,e2) != e0
| op(e0,e0) = e1
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e1,e1) = e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e0,e0) = e2
| op(e1,e1) = e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e0,e0) = e2
| op(e1,e1) = e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e0,e2) != e0
| op(e1,e1) = e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e0,e2) != e0
| op(e1,e1) = e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e0,e2) != e0
| op(e1,e1) = e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e1) != e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e0,e0) = e2
| op(e0,e1) != e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e0,e0) = e2
| op(e0,e1) != e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e2,e2) = e0
| op(e0,e1) != e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e0,e1) != e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e2,e2) = e0
| op(e0,e1) != e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e0) = e3
| op(e0,e2) != e0
| op(e0,e1) != e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e3,e3) = e0
| op(e0,e2) != e0
| op(e0,e1) != e0
| op(e0,e0) != e0
| ~ epred6_0 )
& ( op(e0,e3) != e0
| op(e0,e2) != e0
| op(e0,e1) != e0
| op(e0,e0) != e0
| ~ epred6_0 ) ),
inference(distribute,[status(thm)],[508]) ).
cnf(532,plain,
( op(e0,e0) = e1
| op(e2,e2) = e0
| op(e3,e3) = e0
| ~ epred6_0
| op(e0,e0) != e0 ),
inference(split_conjunct,[status(thm)],[509]) ).
cnf(559,plain,
( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e2,e2) = e0
| op(e3,e3) = e0
| ~ epred6_0 ),
inference(split_conjunct,[status(thm)],[509]) ).
fof(564,plain,
( ~ epred7_0
| epred6_0
| ( 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) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 ) ),
inference(fof_nnf,[status(thm)],[22]) ).
fof(565,plain,
( ( op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) = e1
| op(e1,e1) = e0
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) = e1
| op(e1,e1) = e0
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) != e1
| op(e1,e1) = e0
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) != e1
| op(e1,e1) = e0
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) != e1
| op(e1,e1) = e0
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) = e1
| op(e0,e0) = e1
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) = e1
| op(e0,e0) = e1
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) = e1
| op(e0,e0) = e1
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) != e1
| op(e0,e0) = e1
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) != e1
| op(e0,e0) = e1
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) != e1
| op(e0,e0) = e1
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e0) != e1
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) != e1
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) = e1
| op(e1,e0) != e1
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) != e1
| op(e1,e0) != e1
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) != e1
| op(e1,e0) != e1
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) != e1
| op(e1,e0) != e1
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) = e1
| op(e1,e1) = e0
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) = e1
| op(e1,e1) = e0
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) != e1
| op(e1,e1) = e0
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) != e1
| op(e1,e1) = e0
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) != e1
| op(e1,e1) = e0
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) = e1
| op(e0,e0) = e1
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) = e1
| op(e0,e0) = e1
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) = e1
| op(e0,e0) = e1
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) != e1
| op(e0,e0) = e1
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) != e1
| op(e0,e0) = e1
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) != e1
| op(e0,e0) = e1
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e0) != e1
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) != e1
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) = e1
| op(e1,e0) != e1
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) != e1
| op(e1,e0) != e1
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) != e1
| op(e1,e0) != e1
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) != e1
| op(e1,e0) != e1
| op(e4,e4) = e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) = e1
| op(e1,e1) = e0
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) = e1
| op(e1,e1) = e0
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) != e1
| op(e1,e1) = e0
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) != e1
| op(e1,e1) = e0
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) != e1
| op(e1,e1) = e0
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) = e1
| op(e0,e0) = e1
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) = e1
| op(e0,e0) = e1
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) = e1
| op(e0,e0) = e1
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) != e1
| op(e0,e0) = e1
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) != e1
| op(e0,e0) = e1
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) != e1
| op(e0,e0) = e1
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e0) != e1
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) != e1
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) = e1
| op(e1,e0) != e1
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e1) = e2
| op(e1,e1) != e1
| op(e1,e0) != e1
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e2,e2) = e1
| op(e1,e1) != e1
| op(e1,e0) != e1
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 )
& ( op(e1,e2) != e1
| op(e1,e1) != e1
| op(e1,e0) != e1
| op(e0,e4) != e0
| epred6_0
| ~ epred7_0 ) ),
inference(distribute,[status(thm)],[564]) ).
cnf(611,plain,
( epred6_0
| op(e0,e0) = e4
| op(e0,e0) = e1
| op(e1,e1) = e1
| ~ epred7_0
| op(e1,e2) != e1 ),
inference(split_conjunct,[status(thm)],[565]) ).
cnf(613,plain,
( epred6_0
| op(e0,e0) = e4
| op(e0,e0) = e1
| op(e1,e1) = e1
| op(e1,e1) = e2
| ~ epred7_0 ),
inference(split_conjunct,[status(thm)],[565]) ).
fof(620,plain,
( ~ epred8_0
| epred7_0
| ( 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(fof_nnf,[status(thm)],[23]) ).
fof(621,plain,
( ( op(e2,e2) = e0
| op(e1,e1) = e4
| op(e1,e1) = e3
| epred7_0
| ~ epred8_0 )
& ( op(e0,e0) = e2
| op(e1,e1) = e4
| op(e1,e1) = e3
| epred7_0
| ~ epred8_0 )
& ( op(e2,e0) != e2
| op(e1,e1) = e4
| op(e1,e1) = e3
| epred7_0
| ~ epred8_0 )
& ( op(e2,e2) = e0
| op(e4,e4) = e1
| op(e1,e1) = e3
| epred7_0
| ~ epred8_0 )
& ( op(e0,e0) = e2
| op(e4,e4) = e1
| op(e1,e1) = e3
| epred7_0
| ~ epred8_0 )
& ( op(e2,e0) != e2
| op(e4,e4) = e1
| op(e1,e1) = e3
| epred7_0
| ~ epred8_0 )
& ( op(e2,e2) = e0
| op(e1,e4) != e1
| op(e1,e1) = e3
| epred7_0
| ~ epred8_0 )
& ( op(e0,e0) = e2
| op(e1,e4) != e1
| op(e1,e1) = e3
| epred7_0
| ~ epred8_0 )
& ( op(e2,e0) != e2
| op(e1,e4) != e1
| op(e1,e1) = e3
| epred7_0
| ~ epred8_0 )
& ( op(e2,e2) = e0
| op(e1,e1) = e4
| op(e3,e3) = e1
| epred7_0
| ~ epred8_0 )
& ( op(e0,e0) = e2
| op(e1,e1) = e4
| op(e3,e3) = e1
| epred7_0
| ~ epred8_0 )
& ( op(e2,e0) != e2
| op(e1,e1) = e4
| op(e3,e3) = e1
| epred7_0
| ~ epred8_0 )
& ( op(e2,e2) = e0
| op(e4,e4) = e1
| op(e3,e3) = e1
| epred7_0
| ~ epred8_0 )
& ( op(e0,e0) = e2
| op(e4,e4) = e1
| op(e3,e3) = e1
| epred7_0
| ~ epred8_0 )
& ( op(e2,e0) != e2
| op(e4,e4) = e1
| op(e3,e3) = e1
| epred7_0
| ~ epred8_0 )
& ( op(e2,e2) = e0
| op(e1,e4) != e1
| op(e3,e3) = e1
| epred7_0
| ~ epred8_0 )
& ( op(e0,e0) = e2
| op(e1,e4) != e1
| op(e3,e3) = e1
| epred7_0
| ~ epred8_0 )
& ( op(e2,e0) != e2
| op(e1,e4) != e1
| op(e3,e3) = e1
| epred7_0
| ~ epred8_0 )
& ( op(e2,e2) = e0
| op(e1,e1) = e4
| op(e1,e3) != e1
| epred7_0
| ~ epred8_0 )
& ( op(e0,e0) = e2
| op(e1,e1) = e4
| op(e1,e3) != e1
| epred7_0
| ~ epred8_0 )
& ( op(e2,e0) != e2
| op(e1,e1) = e4
| op(e1,e3) != e1
| epred7_0
| ~ epred8_0 )
& ( op(e2,e2) = e0
| op(e4,e4) = e1
| op(e1,e3) != e1
| epred7_0
| ~ epred8_0 )
& ( op(e0,e0) = e2
| op(e4,e4) = e1
| op(e1,e3) != e1
| epred7_0
| ~ epred8_0 )
& ( op(e2,e0) != e2
| op(e4,e4) = e1
| op(e1,e3) != e1
| epred7_0
| ~ epred8_0 )
& ( op(e2,e2) = e0
| op(e1,e4) != e1
| op(e1,e3) != e1
| epred7_0
| ~ epred8_0 )
& ( op(e0,e0) = e2
| op(e1,e4) != e1
| op(e1,e3) != e1
| epred7_0
| ~ epred8_0 )
& ( op(e2,e0) != e2
| op(e1,e4) != e1
| op(e1,e3) != e1
| epred7_0
| ~ epred8_0 ) ),
inference(distribute,[status(thm)],[620]) ).
cnf(639,plain,
( epred7_0
| op(e3,e3) = e1
| op(e1,e1) = e4
| op(e2,e2) = e0
| ~ epred8_0 ),
inference(split_conjunct,[status(thm)],[621]) ).
fof(649,plain,
( ~ epred9_0
| epred8_0
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != 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(fof_nnf,[status(thm)],[24]) ).
fof(650,plain,
( ( op(e2,e2) = e4
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e3,e3) = e2
| op(e2,e2) = e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e3,e3) = e2
| op(e2,e2) = e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e3,e3) = e2
| op(e2,e2) = e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e2,e3) != e2
| op(e2,e2) = e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e2,e3) != e2
| op(e2,e2) = e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e2,e3) != e2
| op(e2,e2) = e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e2,e2) = e3
| op(e2,e2) != e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e2,e2) = e3
| op(e2,e2) != e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e2,e2) = e3
| op(e2,e2) != e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e3,e3) = e2
| op(e2,e2) != e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e3,e3) = e2
| op(e2,e2) != e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e3,e3) = e2
| op(e2,e2) != e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e2,e3) != e2
| op(e2,e2) != e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e2,e3) != e2
| op(e2,e2) != e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e2,e3) != e2
| op(e2,e2) != e2
| op(e2,e2) = e1
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e3,e3) = e2
| op(e2,e2) = e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e3,e3) = e2
| op(e2,e2) = e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e3,e3) = e2
| op(e2,e2) = e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e2,e3) != e2
| op(e2,e2) = e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e2,e3) != e2
| op(e2,e2) = e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e2,e3) != e2
| op(e2,e2) = e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e2,e2) = e3
| op(e2,e2) != e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e2,e2) = e3
| op(e2,e2) != e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e2,e2) = e3
| op(e2,e2) != e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e3,e3) = e2
| op(e2,e2) != e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e3,e3) = e2
| op(e2,e2) != e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e3,e3) = e2
| op(e2,e2) != e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e2,e3) != e2
| op(e2,e2) != e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e2,e3) != e2
| op(e2,e2) != e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e2,e3) != e2
| op(e2,e2) != e2
| op(e1,e1) = e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e3,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e3,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e3,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e2,e3) != e2
| op(e2,e2) = e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e2,e3) != e2
| op(e2,e2) = e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e2,e3) != e2
| op(e2,e2) = e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e2,e2) = e3
| op(e2,e2) != e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e2,e2) = e3
| op(e2,e2) != e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e2,e2) = e3
| op(e2,e2) != e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e3,e3) = e2
| op(e2,e2) != e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e3,e3) = e2
| op(e2,e2) != e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e3,e3) = e2
| op(e2,e2) != e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e2) = e4
| op(e2,e3) != e2
| op(e2,e2) != e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e4,e4) = e2
| op(e2,e3) != e2
| op(e2,e2) != e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 )
& ( op(e2,e4) != e2
| op(e2,e3) != e2
| op(e2,e2) != e2
| op(e2,e1) != e2
| epred8_0
| ~ epred9_0 ) ),
inference(distribute,[status(thm)],[649]) ).
cnf(683,plain,
( epred8_0
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e2,e2) = e4
| ~ epred9_0 ),
inference(split_conjunct,[status(thm)],[650]) ).
fof(705,plain,
( ~ epred10_0
| epred9_0
| ( 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(fof_nnf,[status(thm)],[25]) ).
fof(706,plain,
( ( op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0
| epred9_0
| ~ epred10_0 )
& ( op(e2,e2) = e3
| op(e3,e3) = e1
| op(e3,e3) = e0
| epred9_0
| ~ epred10_0 )
& ( op(e3,e2) != e3
| op(e3,e3) = e1
| op(e3,e3) = e0
| epred9_0
| ~ epred10_0 )
& ( op(e3,e3) = e2
| op(e1,e1) = e3
| op(e3,e3) = e0
| epred9_0
| ~ epred10_0 )
& ( op(e2,e2) = e3
| op(e1,e1) = e3
| op(e3,e3) = e0
| epred9_0
| ~ epred10_0 )
& ( op(e3,e2) != e3
| op(e1,e1) = e3
| op(e3,e3) = e0
| epred9_0
| ~ epred10_0 )
& ( op(e3,e3) = e2
| op(e3,e1) != e3
| op(e3,e3) = e0
| epred9_0
| ~ epred10_0 )
& ( op(e2,e2) = e3
| op(e3,e1) != e3
| op(e3,e3) = e0
| epred9_0
| ~ epred10_0 )
& ( op(e3,e2) != e3
| op(e3,e1) != e3
| op(e3,e3) = e0
| epred9_0
| ~ epred10_0 )
& ( op(e3,e3) = e2
| op(e3,e3) = e1
| op(e0,e0) = e3
| epred9_0
| ~ epred10_0 )
& ( op(e2,e2) = e3
| op(e3,e3) = e1
| op(e0,e0) = e3
| epred9_0
| ~ epred10_0 )
& ( op(e3,e2) != e3
| op(e3,e3) = e1
| op(e0,e0) = e3
| epred9_0
| ~ epred10_0 )
& ( op(e3,e3) = e2
| op(e1,e1) = e3
| op(e0,e0) = e3
| epred9_0
| ~ epred10_0 )
& ( op(e2,e2) = e3
| op(e1,e1) = e3
| op(e0,e0) = e3
| epred9_0
| ~ epred10_0 )
& ( op(e3,e2) != e3
| op(e1,e1) = e3
| op(e0,e0) = e3
| epred9_0
| ~ epred10_0 )
& ( op(e3,e3) = e2
| op(e3,e1) != e3
| op(e0,e0) = e3
| epred9_0
| ~ epred10_0 )
& ( op(e2,e2) = e3
| op(e3,e1) != e3
| op(e0,e0) = e3
| epred9_0
| ~ epred10_0 )
& ( op(e3,e2) != e3
| op(e3,e1) != e3
| op(e0,e0) = e3
| epred9_0
| ~ epred10_0 )
& ( op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e0) != e3
| epred9_0
| ~ epred10_0 )
& ( op(e2,e2) = e3
| op(e3,e3) = e1
| op(e3,e0) != e3
| epred9_0
| ~ epred10_0 )
& ( op(e3,e2) != e3
| op(e3,e3) = e1
| op(e3,e0) != e3
| epred9_0
| ~ epred10_0 )
& ( op(e3,e3) = e2
| op(e1,e1) = e3
| op(e3,e0) != e3
| epred9_0
| ~ epred10_0 )
& ( op(e2,e2) = e3
| op(e1,e1) = e3
| op(e3,e0) != e3
| epred9_0
| ~ epred10_0 )
& ( op(e3,e2) != e3
| op(e1,e1) = e3
| op(e3,e0) != e3
| epred9_0
| ~ epred10_0 )
& ( op(e3,e3) = e2
| op(e3,e1) != e3
| op(e3,e0) != e3
| epred9_0
| ~ epred10_0 )
& ( op(e2,e2) = e3
| op(e3,e1) != e3
| op(e3,e0) != e3
| epred9_0
| ~ epred10_0 )
& ( op(e3,e2) != e3
| op(e3,e1) != e3
| op(e3,e0) != e3
| epred9_0
| ~ epred10_0 ) ),
inference(distribute,[status(thm)],[705]) ).
cnf(733,plain,
( epred9_0
| op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| ~ epred10_0 ),
inference(split_conjunct,[status(thm)],[706]) ).
fof(734,plain,
( ~ epred11_0
| epred10_0
| ( 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(fof_nnf,[status(thm)],[26]) ).
fof(735,plain,
( ( op(e4,e4) = e1
| op(e4,e4) = e0
| op(e3,e3) = e4
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e4,e4) = e0
| op(e3,e3) = e4
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e4,e4) = e0
| op(e3,e3) = e4
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e0,e0) = e4
| op(e3,e3) = e4
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e3,e3) = e4
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e0,e0) = e4
| op(e3,e3) = e4
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e4,e0) != e4
| op(e3,e3) = e4
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e4,e0) != e4
| op(e3,e3) = e4
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e4,e0) != e4
| op(e3,e3) = e4
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e4,e4) = e0
| op(e4,e4) = e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e4,e4) = e0
| op(e4,e4) = e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e4,e4) = e0
| op(e4,e4) = e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e0,e0) = e4
| op(e4,e4) = e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e4,e0) != e4
| op(e4,e4) = e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e4,e0) != e4
| op(e4,e4) = e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e4,e0) != e4
| op(e4,e4) = e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e4,e4) = e0
| op(e3,e4) != e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e4,e4) = e0
| op(e3,e4) != e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e4,e4) = e0
| op(e3,e4) != e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e0,e0) = e4
| op(e3,e4) != e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e3,e4) != e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e0,e0) = e4
| op(e3,e4) != e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e4,e0) != e4
| op(e3,e4) != e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e4,e0) != e4
| op(e3,e4) != e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e4,e0) != e4
| op(e3,e4) != e3
| op(e3,e3) = e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e4,e4) = e0
| op(e3,e3) = e4
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e4,e4) = e0
| op(e3,e3) = e4
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e4,e4) = e0
| op(e3,e3) = e4
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e0,e0) = e4
| op(e3,e3) = e4
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e3,e3) = e4
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e0,e0) = e4
| op(e3,e3) = e4
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e4,e0) != e4
| op(e3,e3) = e4
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e4,e0) != e4
| op(e3,e3) = e4
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e4,e0) != e4
| op(e3,e3) = e4
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e4,e4) = e0
| op(e4,e4) = e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e4,e4) = e0
| op(e4,e4) = e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e4,e4) = e0
| op(e4,e4) = e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e0,e0) = e4
| op(e4,e4) = e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e0,e0) = e4
| op(e4,e4) = e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e4,e0) != e4
| op(e4,e4) = e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e4,e0) != e4
| op(e4,e4) = e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e4,e0) != e4
| op(e4,e4) = e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e4,e4) = e0
| op(e3,e4) != e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e4,e4) = e0
| op(e3,e4) != e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e4,e4) = e0
| op(e3,e4) != e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e0,e0) = e4
| op(e3,e4) != e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e0,e0) = e4
| op(e3,e4) != e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e0,e0) = e4
| op(e3,e4) != e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e4) = e1
| op(e4,e0) != e4
| op(e3,e4) != e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e1,e1) = e4
| op(e4,e0) != e4
| op(e3,e4) != e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 )
& ( op(e4,e1) != e4
| op(e4,e0) != e4
| op(e3,e4) != e3
| op(e3,e3) != e3
| epred10_0
| ~ epred11_0 ) ),
inference(distribute,[status(thm)],[734]) ).
cnf(776,plain,
( epred10_0
| op(e3,e3) = e3
| op(e4,e4) = e3
| op(e0,e0) = e4
| op(e1,e1) = e4
| ~ epred11_0 ),
inference(split_conjunct,[status(thm)],[735]) ).
cnf(794,plain,
( op(e4,e0) = e0
| unit = e3
| unit = e2
| unit = e1
| unit = e0 ),
inference(spm,[status(thm)],[37,27,theory(equality)]) ).
cnf(799,plain,
( op(e0,e4) = e0
| unit = e3
| unit = e2
| unit = e1
| unit = e0 ),
inference(spm,[status(thm)],[36,27,theory(equality)]) ).
cnf(807,plain,
op(e1,e2) != e3,
inference(rw,[status(thm)],[192,114,theory(equality)]) ).
cnf(960,negated_conjecture,
( e3 = e4
| op(e4,e4) = e3
| epred11_0
| op(e4,e4) != e4 ),
inference(rw,[status(thm)],[239,114,theory(equality)]) ).
cnf(961,negated_conjecture,
( op(e4,e4) = e3
| epred11_0
| op(e4,e4) != e4 ),
inference(sr,[status(thm)],[960,217,theory(equality)]) ).
cnf(1001,plain,
op(e3,e2) = e1,
inference(rw,[status(thm)],[115,114,theory(equality)]) ).
cnf(1005,plain,
op(e3,e1) != e1,
inference(rw,[status(thm)],[132,1001,theory(equality)]) ).
cnf(1027,plain,
op(e3,e3) = e4,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[113,114,theory(equality)]),114,theory(equality)]) ).
cnf(1065,negated_conjecture,
( e3 = e4
| op(e4,e4) = e3
| op(e4,e4) = e4
| epred11_0 ),
inference(rw,[status(thm)],[240,114,theory(equality)]) ).
cnf(1066,negated_conjecture,
( op(e4,e4) = e3
| op(e4,e4) = e4
| epred11_0 ),
inference(sr,[status(thm)],[1065,217,theory(equality)]) ).
cnf(1067,negated_conjecture,
( op(e4,e4) = e3
| epred11_0 ),
inference(csr,[status(thm)],[1066,961]) ).
cnf(1121,plain,
( op(e1,e1) = e4
| e3 = e0
| op(e3,e3) = e1
| epred7_0
| ~ epred8_0 ),
inference(rw,[status(thm)],[639,114,theory(equality)]) ).
cnf(1122,plain,
( op(e1,e1) = e4
| e3 = e0
| e4 = e1
| epred7_0
| ~ epred8_0 ),
inference(rw,[status(thm)],[1121,1027,theory(equality)]) ).
cnf(1123,plain,
( op(e1,e1) = e4
| e4 = e1
| epred7_0
| ~ epred8_0 ),
inference(sr,[status(thm)],[1122,224,theory(equality)]) ).
cnf(1124,plain,
( op(e1,e1) = e4
| epred7_0
| ~ epred8_0 ),
inference(sr,[status(thm)],[1123,220,theory(equality)]) ).
cnf(1132,plain,
( e4 = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| epred9_0
| ~ epred10_0 ),
inference(rw,[status(thm)],[733,1027,theory(equality)]) ).
cnf(1133,plain,
( e4 = e0
| e4 = e1
| op(e3,e3) = e2
| epred9_0
| ~ epred10_0 ),
inference(rw,[status(thm)],[1132,1027,theory(equality)]) ).
cnf(1134,plain,
( e4 = e0
| e4 = e1
| e4 = e2
| epred9_0
| ~ epred10_0 ),
inference(rw,[status(thm)],[1133,1027,theory(equality)]) ).
cnf(1135,plain,
( e4 = e1
| e4 = e2
| epred9_0
| ~ epred10_0 ),
inference(sr,[status(thm)],[1134,223,theory(equality)]) ).
cnf(1136,plain,
( e4 = e2
| epred9_0
| ~ epred10_0 ),
inference(sr,[status(thm)],[1135,220,theory(equality)]) ).
cnf(1137,plain,
( epred9_0
| ~ epred10_0 ),
inference(sr,[status(thm)],[1136,218,theory(equality)]) ).
cnf(1142,plain,
( op(e0,e0) = e0
| op(e0,e0) = e1
| e3 = e0
| op(e3,e3) = e0
| ~ epred6_0 ),
inference(rw,[status(thm)],[559,114,theory(equality)]) ).
cnf(1143,plain,
( op(e0,e0) = e0
| op(e0,e0) = e1
| e3 = e0
| e4 = e0
| ~ epred6_0 ),
inference(rw,[status(thm)],[1142,1027,theory(equality)]) ).
cnf(1144,plain,
( op(e0,e0) = e0
| op(e0,e0) = e1
| e4 = e0
| ~ epred6_0 ),
inference(sr,[status(thm)],[1143,224,theory(equality)]) ).
cnf(1145,plain,
( op(e0,e0) = e0
| op(e0,e0) = e1
| ~ epred6_0 ),
inference(sr,[status(thm)],[1144,223,theory(equality)]) ).
cnf(1256,plain,
op(e1,e1) = e0,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[116,114,theory(equality)]),1001,theory(equality)]),114,theory(equality)]),1001,theory(equality)]) ).
cnf(1258,plain,
op(e3,e1) != e0,
inference(rw,[status(thm)],[201,1256,theory(equality)]) ).
cnf(1263,plain,
e0 != op(e1,e0),
inference(rw,[status(thm)],[156,1256,theory(equality)]) ).
cnf(1271,plain,
( e0 = e4
| epred7_0
| ~ epred8_0 ),
inference(rw,[status(thm)],[1124,1256,theory(equality)]) ).
cnf(1272,plain,
( epred7_0
| ~ epred8_0 ),
inference(sr,[status(thm)],[1271,223,theory(equality)]) ).
cnf(1307,plain,
( op(e0,e0) = e1
| op(e0,e0) = e4
| e0 = e1
| op(e1,e1) = e2
| epred6_0
| ~ epred7_0 ),
inference(rw,[status(thm)],[613,1256,theory(equality)]) ).
cnf(1308,plain,
( op(e0,e0) = e1
| op(e0,e0) = e4
| e0 = e1
| e0 = e2
| epred6_0
| ~ epred7_0 ),
inference(rw,[status(thm)],[1307,1256,theory(equality)]) ).
cnf(1309,plain,
( op(e0,e0) = e1
| op(e0,e0) = e4
| e2 = e0
| epred6_0
| ~ epred7_0 ),
inference(sr,[status(thm)],[1308,226,theory(equality)]) ).
cnf(1310,plain,
( op(e0,e0) = e1
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 ),
inference(sr,[status(thm)],[1309,225,theory(equality)]) ).
cnf(1332,plain,
( op(e0,e0) = e4
| e0 = e4
| op(e3,e3) = e3
| op(e4,e4) = e3
| epred10_0
| ~ epred11_0 ),
inference(rw,[status(thm)],[776,1256,theory(equality)]) ).
cnf(1333,plain,
( op(e0,e0) = e4
| e0 = e4
| e4 = e3
| op(e4,e4) = e3
| epred10_0
| ~ epred11_0 ),
inference(rw,[status(thm)],[1332,1027,theory(equality)]) ).
cnf(1334,plain,
( op(e0,e0) = e4
| e4 = e3
| op(e4,e4) = e3
| epred10_0
| ~ epred11_0 ),
inference(sr,[status(thm)],[1333,223,theory(equality)]) ).
cnf(1335,plain,
( op(e0,e0) = e4
| op(e4,e4) = e3
| epred10_0
| ~ epred11_0 ),
inference(sr,[status(thm)],[1334,217,theory(equality)]) ).
cnf(1336,plain,
( op(e0,e0) = e4
| op(e4,e4) = e3
| epred10_0 ),
inference(csr,[status(thm)],[1335,1067]) ).
cnf(1338,plain,
( op(e0,e0) = e4
| epred10_0
| e3 != op(e1,e4) ),
inference(spm,[status(thm)],[170,1336,theory(equality)]) ).
cnf(1392,plain,
( e0 = e2
| op(e2,e2) = e2
| op(e2,e2) = e4
| op(e3,e3) = e2
| epred8_0
| ~ epred9_0 ),
inference(rw,[status(thm)],[683,1256,theory(equality)]) ).
cnf(1393,plain,
( e0 = e2
| e3 = e2
| op(e2,e2) = e4
| op(e3,e3) = e2
| epred8_0
| ~ epred9_0 ),
inference(rw,[status(thm)],[1392,114,theory(equality)]) ).
cnf(1394,plain,
( e0 = e2
| e3 = e2
| e3 = e4
| op(e3,e3) = e2
| epred8_0
| ~ epred9_0 ),
inference(rw,[status(thm)],[1393,114,theory(equality)]) ).
cnf(1395,plain,
( e0 = e2
| e3 = e2
| e3 = e4
| e4 = e2
| epred8_0
| ~ epred9_0 ),
inference(rw,[status(thm)],[1394,1027,theory(equality)]) ).
cnf(1396,plain,
( e3 = e2
| e4 = e3
| e4 = e2
| epred8_0
| ~ epred9_0 ),
inference(sr,[status(thm)],[1395,225,theory(equality)]) ).
cnf(1397,plain,
( e4 = e3
| e4 = e2
| epred8_0
| ~ epred9_0 ),
inference(sr,[status(thm)],[1396,219,theory(equality)]) ).
cnf(1398,plain,
( e4 = e2
| epred8_0
| ~ epred9_0 ),
inference(sr,[status(thm)],[1397,217,theory(equality)]) ).
cnf(1399,plain,
( epred8_0
| ~ epred9_0 ),
inference(sr,[status(thm)],[1398,218,theory(equality)]) ).
cnf(1491,plain,
( op(e0,e0) = e1
| e3 = e0
| op(e3,e3) = e0
| op(e0,e0) != e0
| ~ epred6_0 ),
inference(rw,[status(thm)],[532,114,theory(equality)]) ).
cnf(1492,plain,
( op(e0,e0) = e1
| e3 = e0
| e4 = e0
| op(e0,e0) != e0
| ~ epred6_0 ),
inference(rw,[status(thm)],[1491,1027,theory(equality)]) ).
cnf(1493,plain,
( op(e0,e0) = e1
| e4 = e0
| op(e0,e0) != e0
| ~ epred6_0 ),
inference(sr,[status(thm)],[1492,224,theory(equality)]) ).
cnf(1494,plain,
( op(e0,e0) = e1
| op(e0,e0) != e0
| ~ epred6_0 ),
inference(sr,[status(thm)],[1493,223,theory(equality)]) ).
cnf(1495,plain,
( op(e0,e0) = e1
| ~ epred6_0 ),
inference(csr,[status(thm)],[1494,1145]) ).
cnf(1606,plain,
( op(e0,e0) = e1
| op(e0,e0) = e4
| e0 = e1
| epred6_0
| op(e1,e2) != e1
| ~ epred7_0 ),
inference(rw,[status(thm)],[611,1256,theory(equality)]) ).
cnf(1607,plain,
( op(e0,e0) = e1
| op(e0,e0) = e4
| epred6_0
| op(e1,e2) != e1
| ~ epred7_0 ),
inference(sr,[status(thm)],[1606,226,theory(equality)]) ).
cnf(1608,plain,
( op(e0,e0) = e1
| op(e0,e0) = e4
| epred6_0
| ~ epred7_0 ),
inference(csr,[status(thm)],[1607,1310]) ).
cnf(1609,plain,
( op(e0,e0) = e1
| op(e0,e0) = e4
| ~ epred7_0 ),
inference(csr,[status(thm)],[1608,1495]) ).
cnf(2096,plain,
( op(e1,e0) = e3
| e0 = e3
| op(e1,e2) = e3
| op(e1,e3) = e3
| op(e1,e4) = e3 ),
inference(rw,[status(thm)],[71,1256,theory(equality)]) ).
cnf(2097,plain,
( op(e1,e0) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3
| op(e1,e4) = e3 ),
inference(sr,[status(thm)],[2096,224,theory(equality)]) ).
cnf(2098,plain,
( op(e1,e0) = e3
| op(e1,e3) = e3
| op(e1,e4) = e3 ),
inference(sr,[status(thm)],[2097,807,theory(equality)]) ).
cnf(2332,plain,
( op(e3,e0) = e0
| op(e3,e1) = e0
| e1 = e0
| op(e3,e3) = e0
| op(e3,e4) = e0 ),
inference(rw,[status(thm)],[57,1001,theory(equality)]) ).
cnf(2333,plain,
( op(e3,e0) = e0
| op(e3,e1) = e0
| e1 = e0
| e4 = e0
| op(e3,e4) = e0 ),
inference(rw,[status(thm)],[2332,1027,theory(equality)]) ).
cnf(2334,plain,
( op(e3,e0) = e0
| op(e3,e1) = e0
| e4 = e0
| op(e3,e4) = e0 ),
inference(sr,[status(thm)],[2333,226,theory(equality)]) ).
cnf(2335,plain,
( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e4) = e0 ),
inference(sr,[status(thm)],[2334,223,theory(equality)]) ).
cnf(2781,plain,
( op(e3,e4) = e0
| op(e3,e0) = e0 ),
inference(sr,[status(thm)],[2335,1258,theory(equality)]) ).
cnf(2839,plain,
( op(e3,e0) = e0
| e0 != op(e0,e4) ),
inference(spm,[status(thm)],[174,2781,theory(equality)]) ).
cnf(2857,plain,
( unit = e0
| unit = e1
| unit = e2
| unit = e3
| e0 != op(e3,e0) ),
inference(spm,[status(thm)],[207,794,theory(equality)]) ).
cnf(3114,plain,
( op(e3,e0) = e0
| unit = e0
| unit = e1
| unit = e2
| unit = e3 ),
inference(spm,[status(thm)],[2839,799,theory(equality)]) ).
cnf(3695,plain,
( unit = e3
| unit = e2
| unit = e1
| unit = e0 ),
inference(csr,[status(thm)],[3114,2857]) ).
cnf(3700,plain,
( op(e3,e1) = e1
| unit = e2
| unit = e1
| unit = e0 ),
inference(spm,[status(thm)],[35,3695,theory(equality)]) ).
cnf(3729,plain,
( unit = e2
| unit = e1
| unit = e0 ),
inference(sr,[status(thm)],[3700,1005,theory(equality)]) ).
cnf(3740,plain,
( op(e1,e0) = e0
| unit = e0
| unit = e2 ),
inference(spm,[status(thm)],[37,3729,theory(equality)]) ).
cnf(3770,plain,
( unit = e0
| unit = e2 ),
inference(sr,[status(thm)],[3740,1263,theory(equality)]) ).
cnf(3779,plain,
( op(e2,e2) = e2
| unit = e0 ),
inference(spm,[status(thm)],[33,3770,theory(equality)]) ).
cnf(3807,plain,
( e3 = e2
| unit = e0 ),
inference(rw,[status(thm)],[3779,114,theory(equality)]) ).
cnf(3808,plain,
unit = e0,
inference(sr,[status(thm)],[3807,219,theory(equality)]) ).
cnf(3818,plain,
op(e1,e0) = e1,
inference(rw,[status(thm)],[34,3808,theory(equality)]) ).
cnf(3819,plain,
op(e0,e0) = e0,
inference(rw,[status(thm)],[36,3808,theory(equality)]) ).
cnf(3821,plain,
op(e0,e3) = e3,
inference(rw,[status(thm)],[31,3808,theory(equality)]) ).
cnf(4143,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| e1 = e3 ),
inference(rw,[status(thm)],[2098,3818,theory(equality)]) ).
cnf(4144,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3 ),
inference(sr,[status(thm)],[4143,221,theory(equality)]) ).
cnf(4192,plain,
( e0 = e4
| epred10_0
| op(e1,e4) != e3 ),
inference(rw,[status(thm)],[1338,3819,theory(equality)]) ).
cnf(4193,plain,
( epred10_0
| op(e1,e4) != e3 ),
inference(sr,[status(thm)],[4192,223,theory(equality)]) ).
cnf(4198,plain,
( e0 = e4
| op(e0,e0) = e1
| ~ epred7_0 ),
inference(rw,[status(thm)],[1609,3819,theory(equality)]) ).
cnf(4199,plain,
( e0 = e4
| e0 = e1
| ~ epred7_0 ),
inference(rw,[status(thm)],[4198,3819,theory(equality)]) ).
cnf(4200,plain,
( e1 = e0
| ~ epred7_0 ),
inference(sr,[status(thm)],[4199,223,theory(equality)]) ).
cnf(4201,plain,
~ epred7_0,
inference(sr,[status(thm)],[4200,226,theory(equality)]) ).
cnf(4254,plain,
op(e1,e3) != e3,
inference(rw,[status(thm)],[186,3821,theory(equality)]) ).
cnf(4542,plain,
( epred10_0
| op(e1,e3) = e3 ),
inference(spm,[status(thm)],[4193,4144,theory(equality)]) ).
cnf(4553,plain,
epred10_0,
inference(sr,[status(thm)],[4542,4254,theory(equality)]) ).
cnf(4559,plain,
( epred9_0
| $false ),
inference(rw,[status(thm)],[1137,4553,theory(equality)]) ).
cnf(4560,plain,
epred9_0,
inference(cn,[status(thm)],[4559,theory(equality)]) ).
cnf(4561,plain,
( epred8_0
| $false ),
inference(rw,[status(thm)],[1399,4560,theory(equality)]) ).
cnf(4562,plain,
epred8_0,
inference(cn,[status(thm)],[4561,theory(equality)]) ).
cnf(4563,plain,
( epred7_0
| $false ),
inference(rw,[status(thm)],[1272,4562,theory(equality)]) ).
cnf(4564,plain,
epred7_0,
inference(cn,[status(thm)],[4563,theory(equality)]) ).
cnf(4565,plain,
$false,
inference(sr,[status(thm)],[4564,4201,theory(equality)]) ).
cnf(4566,plain,
$false,
4565,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% /home/graph/tptp/Systems/SInE---0.4/Source/sine.py:10: DeprecationWarning: the sets module is deprecated
% from sets import Set
% % SZS status Started for /home/graph/tptp/TPTP/Problems/ALG/ALG058+1.p
% --creating new selector for []
% -running prover on /tmp/tmpugQHcx/sel_ALG058+1.p_1 with time limit 29
% -prover status Theorem
% Problem ALG058+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/ALG/ALG058+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/ALG/ALG058+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------