%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG059+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:49:22 AM UTC 2026
% Result : Theorem 90.37s 16.69s
% Output : CNFRefutation 90.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 66
% Number of leaves : 25
% Syntax : Number of formulae : 460 ( 136 unt; 18 def)
% Number of atoms : 3307 (2737 equ)
% Maximal formula atoms : 450 ( 7 avg)
% Number of connectives : 4161 (1314 ~;1839 |; 990 &)
% ( 18 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 19 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(ax1,axiom,
( ( op(e4,e4) = e4
| op(e4,e4) = e3
| op(e4,e4) = e2
| op(e4,e4) = e1
| op(e4,e4) = e0 )
& ( op(e4,e3) = e4
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e1
| op(e4,e3) = e0 )
& ( op(e4,e2) = e4
| op(e4,e2) = e3
| op(e4,e2) = e2
| op(e4,e2) = e1
| op(e4,e2) = e0 )
& ( op(e4,e1) = e4
| op(e4,e1) = e3
| op(e4,e1) = e2
| op(e4,e1) = e1
| op(e4,e1) = e0 )
& ( op(e4,e0) = e4
| op(e4,e0) = e3
| op(e4,e0) = e2
| op(e4,e0) = e1
| op(e4,e0) = e0 )
& ( op(e3,e4) = e4
| op(e3,e4) = e3
| op(e3,e4) = e2
| op(e3,e4) = e1
| op(e3,e4) = e0 )
& ( op(e3,e3) = e4
| op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 )
& ( op(e3,e2) = e4
| op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 )
& ( op(e3,e1) = e4
| op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 )
& ( op(e3,e0) = e4
| op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 )
& ( op(e2,e4) = e4
| op(e2,e4) = e3
| op(e2,e4) = e2
| op(e2,e4) = e1
| op(e2,e4) = e0 )
& ( op(e2,e3) = e4
| op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 )
& ( op(e2,e2) = e4
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 )
& ( op(e2,e1) = e4
| op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 )
& ( op(e2,e0) = e4
| op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 )
& ( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2
| op(e1,e4) = e1
| op(e1,e4) = e0 )
& ( op(e1,e3) = e4
| op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 )
& ( op(e1,e2) = e4
| op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 )
& ( op(e1,e1) = e4
| op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 )
& ( op(e1,e0) = e4
| op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 )
& ( op(e0,e4) = e4
| op(e0,e4) = e3
| op(e0,e4) = e2
| op(e0,e4) = e1
| op(e0,e4) = e0 )
& ( op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 )
& ( op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 )
& ( op(e0,e1) = e4
| op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 )
& ( op(e0,e0) = e4
| op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ) ),
file('theBenchmark.p',ax1) ).
fof(ax2,axiom,
( ( unit = e4
| unit = e3
| unit = e2
| unit = e1
| unit = e0 )
& op(e4,unit) = e4
& op(unit,e4) = e4
& op(e3,unit) = e3
& op(unit,e3) = e3
& op(e2,unit) = e2
& op(unit,e2) = e2
& op(e1,unit) = e1
& op(unit,e1) = e1
& op(e0,unit) = e0
& op(unit,e0) = e0 ),
file('theBenchmark.p',ax2) ).
fof(ax3,axiom,
( ( op(e4,e4) = e4
| op(e3,e4) = e4
| op(e2,e4) = e4
| op(e1,e4) = e4
| op(e0,e4) = e4 )
& ( op(e4,e4) = e4
| op(e4,e3) = e4
| op(e4,e2) = e4
| op(e4,e1) = e4
| op(e4,e0) = e4 )
& ( op(e4,e4) = e3
| op(e3,e4) = e3
| op(e2,e4) = e3
| op(e1,e4) = e3
| op(e0,e4) = e3 )
& ( op(e4,e4) = e3
| op(e4,e3) = e3
| op(e4,e2) = e3
| op(e4,e1) = e3
| op(e4,e0) = e3 )
& ( op(e4,e4) = e2
| op(e3,e4) = e2
| op(e2,e4) = e2
| op(e1,e4) = e2
| op(e0,e4) = e2 )
& ( op(e4,e4) = e2
| op(e4,e3) = e2
| op(e4,e2) = e2
| op(e4,e1) = e2
| op(e4,e0) = e2 )
& ( op(e4,e4) = e1
| op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| op(e0,e4) = e1 )
& ( op(e4,e4) = e1
| op(e4,e3) = e1
| op(e4,e2) = e1
| op(e4,e1) = e1
| op(e4,e0) = e1 )
& ( op(e4,e4) = e0
| op(e3,e4) = e0
| op(e2,e4) = e0
| op(e1,e4) = e0
| op(e0,e4) = e0 )
& ( op(e4,e4) = e0
| op(e4,e3) = e0
| op(e4,e2) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 )
& ( op(e4,e3) = e4
| op(e3,e3) = e4
| op(e2,e3) = e4
| op(e1,e3) = e4
| op(e0,e3) = e4 )
& ( op(e3,e4) = e4
| op(e3,e3) = e4
| op(e3,e2) = e4
| op(e3,e1) = e4
| op(e3,e0) = e4 )
& ( op(e4,e3) = e3
| op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 )
& ( op(e3,e4) = e3
| op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 )
& ( op(e4,e3) = e2
| op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 )
& ( op(e3,e4) = e2
| op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 )
& ( op(e4,e3) = e1
| op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 )
& ( op(e3,e4) = e1
| op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 )
& ( op(e4,e3) = e0
| op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 )
& ( op(e3,e4) = e0
| op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 )
& ( op(e4,e2) = e4
| op(e3,e2) = e4
| op(e2,e2) = e4
| op(e1,e2) = e4
| op(e0,e2) = e4 )
& ( op(e2,e4) = e4
| op(e2,e3) = e4
| op(e2,e2) = e4
| op(e2,e1) = e4
| op(e2,e0) = e4 )
& ( op(e4,e2) = e3
| op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 )
& ( op(e2,e4) = e3
| op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 )
& ( op(e4,e2) = e2
| op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 )
& ( op(e2,e4) = e2
| op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 )
& ( op(e4,e2) = e1
| op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 )
& ( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 )
& ( op(e4,e2) = e0
| op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 )
& ( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 )
& ( op(e4,e1) = e4
| op(e3,e1) = e4
| op(e2,e1) = e4
| op(e1,e1) = e4
| op(e0,e1) = e4 )
& ( op(e1,e4) = e4
| op(e1,e3) = e4
| op(e1,e2) = e4
| op(e1,e1) = e4
| op(e1,e0) = e4 )
& ( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 )
& ( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 )
& ( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 )
& ( op(e1,e4) = e2
| op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 )
& ( op(e4,e1) = e1
| op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 )
& ( op(e1,e4) = e1
| op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 )
& ( op(e4,e1) = e0
| op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 )
& ( op(e1,e4) = e0
| op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 )
& ( op(e4,e0) = e4
| op(e3,e0) = e4
| op(e2,e0) = e4
| op(e1,e0) = e4
| op(e0,e0) = e4 )
& ( op(e0,e4) = e4
| op(e0,e3) = e4
| op(e0,e2) = e4
| op(e0,e1) = e4
| op(e0,e0) = e4 )
& ( op(e4,e0) = e3
| op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 )
& ( op(e0,e4) = e3
| op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 )
& ( op(e4,e0) = e2
| op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 )
& ( op(e0,e4) = e2
| op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 )
& ( op(e4,e0) = e1
| op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 )
& ( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 )
& ( op(e4,e0) = e0
| op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 )
& ( op(e0,e4) = e0
| op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ) ),
file('theBenchmark.p',ax3) ).
fof(ax4,axiom,
( op(e4,e3) != op(e4,e4)
& op(e4,e2) != op(e4,e4)
& op(e4,e2) != op(e4,e3)
& op(e4,e1) != op(e4,e4)
& op(e4,e1) != op(e4,e3)
& op(e4,e1) != op(e4,e2)
& op(e4,e0) != op(e4,e4)
& op(e4,e0) != op(e4,e3)
& op(e4,e0) != op(e4,e2)
& op(e4,e0) != op(e4,e1)
& op(e3,e3) != op(e3,e4)
& op(e3,e2) != op(e3,e4)
& op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e4)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e4)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e3) != op(e2,e4)
& op(e2,e2) != op(e2,e4)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e4)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e4)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e3) != op(e1,e4)
& op(e1,e2) != op(e1,e4)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e4)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e4)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e3) != op(e0,e4)
& op(e0,e2) != op(e0,e4)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e4)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e4)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e3,e4) != op(e4,e4)
& op(e2,e4) != op(e4,e4)
& op(e2,e4) != op(e3,e4)
& op(e1,e4) != op(e4,e4)
& op(e1,e4) != op(e3,e4)
& op(e1,e4) != op(e2,e4)
& op(e0,e4) != op(e4,e4)
& op(e0,e4) != op(e3,e4)
& op(e0,e4) != op(e2,e4)
& op(e0,e4) != op(e1,e4)
& op(e3,e3) != op(e4,e3)
& op(e2,e3) != op(e4,e3)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e4,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e4,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e3,e2) != op(e4,e2)
& op(e2,e2) != op(e4,e2)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e4,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e4,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e3,e1) != op(e4,e1)
& op(e2,e1) != op(e4,e1)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e4,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e4,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e3,e0) != op(e4,e0)
& op(e2,e0) != op(e4,e0)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e4,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e4,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ),
file('theBenchmark.p',ax4) ).
fof(ax5,axiom,
( e3 != e4
& e2 != e4
& e2 != e3
& e1 != e4
& e1 != e3
& e1 != e2
& e0 != e4
& e0 != e3
& e0 != e2
& e0 != e1 ),
file('theBenchmark.p',ax5) ).
fof(ax6,axiom,
( e4 = op(op(e2,e2),op(e2,e2))
& e3 = op(e2,e2)
& e1 = op(op(e2,e2),e2)
& e0 = op(op(op(e2,e2),e2),op(op(e2,e2),e2)) ),
file('theBenchmark.p',ax6) ).
fof(co1,conjecture,
~ ( ( ( op(op(e4,e4),e4) != e4
& op(op(e4,e4),e4) = e4
& op(e4,e4) != op(e4,e4) )
| ( op(op(e4,e3),e4) != e3
& op(op(e4,e3),e3) = e4
& op(e3,e4) != op(e4,e3) )
| ( op(op(e4,e2),e4) != e2
& op(op(e4,e2),e2) = e4
& op(e2,e4) != op(e4,e2) )
| ( op(op(e4,e1),e4) != e1
& op(op(e4,e1),e1) = e4
& op(e1,e4) != op(e4,e1) )
| ( op(op(e4,e0),e4) != e0
& op(op(e4,e0),e0) = e4
& op(e0,e4) != op(e4,e0) )
| ( op(op(e3,e4),e3) != e4
& op(op(e3,e4),e4) = e3
& op(e4,e3) != op(e3,e4) )
| ( op(op(e3,e3),e3) != e3
& op(op(e3,e3),e3) = e3
& op(e3,e3) != op(e3,e3) )
| ( op(op(e3,e2),e3) != e2
& op(op(e3,e2),e2) = e3
& op(e2,e3) != op(e3,e2) )
| ( op(op(e3,e1),e3) != e1
& op(op(e3,e1),e1) = e3
& op(e1,e3) != op(e3,e1) )
| ( op(op(e3,e0),e3) != e0
& op(op(e3,e0),e0) = e3
& op(e0,e3) != op(e3,e0) )
| ( op(op(e2,e4),e2) != e4
& op(op(e2,e4),e4) = e2
& op(e4,e2) != op(e2,e4) )
| ( op(op(e2,e3),e2) != e3
& op(op(e2,e3),e3) = e2
& op(e3,e2) != op(e2,e3) )
| ( op(op(e2,e2),e2) != e2
& op(op(e2,e2),e2) = e2
& op(e2,e2) != op(e2,e2) )
| ( op(op(e2,e1),e2) != e1
& op(op(e2,e1),e1) = e2
& op(e1,e2) != op(e2,e1) )
| ( op(op(e2,e0),e2) != e0
& op(op(e2,e0),e0) = e2
& op(e0,e2) != op(e2,e0) )
| ( op(op(e1,e4),e1) != e4
& op(op(e1,e4),e4) = e1
& op(e4,e1) != op(e1,e4) )
| ( op(op(e1,e3),e1) != e3
& op(op(e1,e3),e3) = e1
& op(e3,e1) != op(e1,e3) )
| ( op(op(e1,e2),e1) != e2
& op(op(e1,e2),e2) = e1
& op(e2,e1) != op(e1,e2) )
| ( op(op(e1,e1),e1) != e1
& op(op(e1,e1),e1) = e1
& op(e1,e1) != op(e1,e1) )
| ( op(op(e1,e0),e1) != e0
& op(op(e1,e0),e0) = e1
& op(e0,e1) != op(e1,e0) )
| ( op(op(e0,e4),e0) != e4
& op(op(e0,e4),e4) = e0
& op(e4,e0) != op(e0,e4) )
| ( op(op(e0,e3),e0) != e3
& op(op(e0,e3),e3) = e0
& op(e3,e0) != op(e0,e3) )
| ( op(op(e0,e2),e0) != e2
& op(op(e0,e2),e2) = e0
& op(e2,e0) != op(e0,e2) )
| ( op(op(e0,e1),e0) != e1
& op(op(e0,e1),e1) = e0
& op(e1,e0) != op(e0,e1) )
| ( op(op(e0,e0),e0) != e0
& op(op(e0,e0),e0) = e0
& op(e0,e0) != op(e0,e0) ) )
& ( ( ( ( e4 != unit
& op(e4,e4) = e4 )
| op(e4,e4) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e3 )
| op(e4,e3) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e2 )
| op(e4,e2) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e1 )
| op(e4,e1) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e0 )
| op(e4,e0) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e4 )
| op(e3,e4) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e3 )
| op(e3,e3) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e2 )
| op(e3,e2) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e1 )
| op(e3,e1) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e0 )
| op(e3,e0) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e4 )
| op(e2,e4) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e3 )
| op(e2,e3) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e2 )
| op(e2,e2) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e1 )
| op(e2,e1) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e0 )
| op(e2,e0) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e4 )
| op(e1,e4) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e3 )
| op(e1,e3) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e2 )
| op(e1,e2) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e1 )
| op(e1,e1) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e0 )
| op(e1,e0) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e4 )
| op(e0,e4) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e3 )
| op(e0,e3) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e2 )
| op(e0,e2) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e1 )
| op(e0,e1) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e0 )
| op(e0,e0) != e4 ) )
| ( ( ( e3 != unit
& op(e4,e3) = e4 )
| op(e4,e4) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e3 )
| op(e4,e3) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e2 )
| op(e4,e2) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e1 )
| op(e4,e1) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e0 )
| op(e4,e0) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e4 )
| op(e3,e4) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e3 )
| op(e3,e3) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e2 )
| op(e3,e2) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e1 )
| op(e3,e1) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e0 )
| op(e3,e0) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e4 )
| op(e2,e4) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e3 )
| op(e2,e3) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e2 )
| op(e2,e2) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e1 )
| op(e2,e1) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e0 )
| op(e2,e0) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e4 )
| op(e1,e4) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e3 )
| op(e1,e3) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e2 )
| op(e1,e2) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e1 )
| op(e1,e1) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e0 )
| op(e1,e0) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e4 )
| op(e0,e4) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e3 )
| op(e0,e3) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e2 )
| op(e0,e2) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e1 )
| op(e0,e1) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e0 )
| op(e0,e0) != e3 ) )
| ( ( ( e2 != unit
& op(e4,e2) = e4 )
| op(e4,e4) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e3 )
| op(e4,e3) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e2 )
| op(e4,e2) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e1 )
| op(e4,e1) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e0 )
| op(e4,e0) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e4 )
| op(e3,e4) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e3 )
| op(e3,e3) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e2 )
| op(e3,e2) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e1 )
| op(e3,e1) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e0 )
| op(e3,e0) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e4 )
| op(e2,e4) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e3 )
| op(e2,e3) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e2 )
| op(e2,e2) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e1 )
| op(e2,e1) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e0 )
| op(e2,e0) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e4 )
| op(e1,e4) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e3 )
| op(e1,e3) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e2 )
| op(e1,e2) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e1 )
| op(e1,e1) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e0 )
| op(e1,e0) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e4 )
| op(e0,e4) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e3 )
| op(e0,e3) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e2 )
| op(e0,e2) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e1 )
| op(e0,e1) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e0 )
| op(e0,e0) != e2 ) )
| ( ( ( e1 != unit
& op(e4,e1) = e4 )
| op(e4,e4) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e3 )
| op(e4,e3) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e2 )
| op(e4,e2) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e1 )
| op(e4,e1) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e0 )
| op(e4,e0) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e4 )
| op(e3,e4) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e3 )
| op(e3,e3) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e2 )
| op(e3,e2) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e1 )
| op(e3,e1) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e0 )
| op(e3,e0) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e4 )
| op(e2,e4) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e3 )
| op(e2,e3) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e2 )
| op(e2,e2) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e1 )
| op(e2,e1) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e0 )
| op(e2,e0) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e4 )
| op(e1,e4) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e3 )
| op(e1,e3) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e2 )
| op(e1,e2) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e1 )
| op(e1,e1) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e0 )
| op(e1,e0) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e4 )
| op(e0,e4) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e3 )
| op(e0,e3) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e2 )
| op(e0,e2) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e1 )
| op(e0,e1) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e0 )
| op(e0,e0) != e1 ) )
| ( ( ( e0 != unit
& op(e4,e0) = e4 )
| op(e4,e4) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e3 )
| op(e4,e3) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e2 )
| op(e4,e2) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e1 )
| op(e4,e1) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e0 )
| op(e4,e0) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e4 )
| op(e3,e4) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e3 )
| op(e3,e3) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e2 )
| op(e3,e2) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e1 )
| op(e3,e1) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e0 )
| op(e3,e0) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e4 )
| op(e2,e4) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e3 )
| op(e2,e3) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e2 )
| op(e2,e2) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e1 )
| op(e2,e1) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e0 )
| op(e2,e0) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e4 )
| op(e1,e4) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e3 )
| op(e1,e3) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e2 )
| op(e1,e2) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e1 )
| op(e1,e1) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e0 )
| op(e1,e0) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e4 )
| op(e0,e4) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e3 )
| op(e0,e3) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e2 )
| op(e0,e2) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e1 )
| op(e0,e1) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e0 )
| op(e0,e0) != e0 ) ) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ~ ( ( ( op(op(e4,e4),e4) != e4
& op(op(e4,e4),e4) = e4
& op(e4,e4) != op(e4,e4) )
| ( op(op(e4,e3),e4) != e3
& op(op(e4,e3),e3) = e4
& op(e3,e4) != op(e4,e3) )
| ( op(op(e4,e2),e4) != e2
& op(op(e4,e2),e2) = e4
& op(e2,e4) != op(e4,e2) )
| ( op(op(e4,e1),e4) != e1
& op(op(e4,e1),e1) = e4
& op(e1,e4) != op(e4,e1) )
| ( op(op(e4,e0),e4) != e0
& op(op(e4,e0),e0) = e4
& op(e0,e4) != op(e4,e0) )
| ( op(op(e3,e4),e3) != e4
& op(op(e3,e4),e4) = e3
& op(e4,e3) != op(e3,e4) )
| ( op(op(e3,e3),e3) != e3
& op(op(e3,e3),e3) = e3
& op(e3,e3) != op(e3,e3) )
| ( op(op(e3,e2),e3) != e2
& op(op(e3,e2),e2) = e3
& op(e2,e3) != op(e3,e2) )
| ( op(op(e3,e1),e3) != e1
& op(op(e3,e1),e1) = e3
& op(e1,e3) != op(e3,e1) )
| ( op(op(e3,e0),e3) != e0
& op(op(e3,e0),e0) = e3
& op(e0,e3) != op(e3,e0) )
| ( op(op(e2,e4),e2) != e4
& op(op(e2,e4),e4) = e2
& op(e4,e2) != op(e2,e4) )
| ( op(op(e2,e3),e2) != e3
& op(op(e2,e3),e3) = e2
& op(e3,e2) != op(e2,e3) )
| ( op(op(e2,e2),e2) != e2
& op(op(e2,e2),e2) = e2
& op(e2,e2) != op(e2,e2) )
| ( op(op(e2,e1),e2) != e1
& op(op(e2,e1),e1) = e2
& op(e1,e2) != op(e2,e1) )
| ( op(op(e2,e0),e2) != e0
& op(op(e2,e0),e0) = e2
& op(e0,e2) != op(e2,e0) )
| ( op(op(e1,e4),e1) != e4
& op(op(e1,e4),e4) = e1
& op(e4,e1) != op(e1,e4) )
| ( op(op(e1,e3),e1) != e3
& op(op(e1,e3),e3) = e1
& op(e3,e1) != op(e1,e3) )
| ( op(op(e1,e2),e1) != e2
& op(op(e1,e2),e2) = e1
& op(e2,e1) != op(e1,e2) )
| ( op(op(e1,e1),e1) != e1
& op(op(e1,e1),e1) = e1
& op(e1,e1) != op(e1,e1) )
| ( op(op(e1,e0),e1) != e0
& op(op(e1,e0),e0) = e1
& op(e0,e1) != op(e1,e0) )
| ( op(op(e0,e4),e0) != e4
& op(op(e0,e4),e4) = e0
& op(e4,e0) != op(e0,e4) )
| ( op(op(e0,e3),e0) != e3
& op(op(e0,e3),e3) = e0
& op(e3,e0) != op(e0,e3) )
| ( op(op(e0,e2),e0) != e2
& op(op(e0,e2),e2) = e0
& op(e2,e0) != op(e0,e2) )
| ( op(op(e0,e1),e0) != e1
& op(op(e0,e1),e1) = e0
& op(e1,e0) != op(e0,e1) )
| ( op(op(e0,e0),e0) != e0
& op(op(e0,e0),e0) = e0
& op(e0,e0) != op(e0,e0) ) )
& ( ( ( ( e4 != unit
& op(e4,e4) = e4 )
| op(e4,e4) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e3 )
| op(e4,e3) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e2 )
| op(e4,e2) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e1 )
| op(e4,e1) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e0 )
| op(e4,e0) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e4 )
| op(e3,e4) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e3 )
| op(e3,e3) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e2 )
| op(e3,e2) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e1 )
| op(e3,e1) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e0 )
| op(e3,e0) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e4 )
| op(e2,e4) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e3 )
| op(e2,e3) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e2 )
| op(e2,e2) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e1 )
| op(e2,e1) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e0 )
| op(e2,e0) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e4 )
| op(e1,e4) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e3 )
| op(e1,e3) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e2 )
| op(e1,e2) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e1 )
| op(e1,e1) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e0 )
| op(e1,e0) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e4 )
| op(e0,e4) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e3 )
| op(e0,e3) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e2 )
| op(e0,e2) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e1 )
| op(e0,e1) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e0 )
| op(e0,e0) != e4 ) )
| ( ( ( e3 != unit
& op(e4,e3) = e4 )
| op(e4,e4) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e3 )
| op(e4,e3) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e2 )
| op(e4,e2) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e1 )
| op(e4,e1) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e0 )
| op(e4,e0) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e4 )
| op(e3,e4) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e3 )
| op(e3,e3) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e2 )
| op(e3,e2) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e1 )
| op(e3,e1) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e0 )
| op(e3,e0) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e4 )
| op(e2,e4) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e3 )
| op(e2,e3) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e2 )
| op(e2,e2) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e1 )
| op(e2,e1) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e0 )
| op(e2,e0) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e4 )
| op(e1,e4) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e3 )
| op(e1,e3) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e2 )
| op(e1,e2) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e1 )
| op(e1,e1) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e0 )
| op(e1,e0) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e4 )
| op(e0,e4) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e3 )
| op(e0,e3) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e2 )
| op(e0,e2) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e1 )
| op(e0,e1) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e0 )
| op(e0,e0) != e3 ) )
| ( ( ( e2 != unit
& op(e4,e2) = e4 )
| op(e4,e4) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e3 )
| op(e4,e3) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e2 )
| op(e4,e2) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e1 )
| op(e4,e1) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e0 )
| op(e4,e0) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e4 )
| op(e3,e4) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e3 )
| op(e3,e3) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e2 )
| op(e3,e2) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e1 )
| op(e3,e1) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e0 )
| op(e3,e0) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e4 )
| op(e2,e4) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e3 )
| op(e2,e3) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e2 )
| op(e2,e2) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e1 )
| op(e2,e1) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e0 )
| op(e2,e0) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e4 )
| op(e1,e4) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e3 )
| op(e1,e3) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e2 )
| op(e1,e2) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e1 )
| op(e1,e1) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e0 )
| op(e1,e0) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e4 )
| op(e0,e4) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e3 )
| op(e0,e3) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e2 )
| op(e0,e2) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e1 )
| op(e0,e1) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e0 )
| op(e0,e0) != e2 ) )
| ( ( ( e1 != unit
& op(e4,e1) = e4 )
| op(e4,e4) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e3 )
| op(e4,e3) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e2 )
| op(e4,e2) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e1 )
| op(e4,e1) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e0 )
| op(e4,e0) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e4 )
| op(e3,e4) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e3 )
| op(e3,e3) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e2 )
| op(e3,e2) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e1 )
| op(e3,e1) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e0 )
| op(e3,e0) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e4 )
| op(e2,e4) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e3 )
| op(e2,e3) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e2 )
| op(e2,e2) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e1 )
| op(e2,e1) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e0 )
| op(e2,e0) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e4 )
| op(e1,e4) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e3 )
| op(e1,e3) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e2 )
| op(e1,e2) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e1 )
| op(e1,e1) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e0 )
| op(e1,e0) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e4 )
| op(e0,e4) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e3 )
| op(e0,e3) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e2 )
| op(e0,e2) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e1 )
| op(e0,e1) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e0 )
| op(e0,e0) != e1 ) )
| ( ( ( e0 != unit
& op(e4,e0) = e4 )
| op(e4,e4) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e3 )
| op(e4,e3) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e2 )
| op(e4,e2) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e1 )
| op(e4,e1) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e0 )
| op(e4,e0) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e4 )
| op(e3,e4) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e3 )
| op(e3,e3) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e2 )
| op(e3,e2) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e1 )
| op(e3,e1) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e0 )
| op(e3,e0) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e4 )
| op(e2,e4) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e3 )
| op(e2,e3) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e2 )
| op(e2,e2) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e1 )
| op(e2,e1) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e0 )
| op(e2,e0) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e4 )
| op(e1,e4) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e3 )
| op(e1,e3) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e2 )
| op(e1,e2) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e1 )
| op(e1,e1) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e0 )
| op(e1,e0) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e4 )
| op(e0,e4) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e3 )
| op(e0,e3) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e2 )
| op(e0,e2) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e1 )
| op(e0,e1) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e0 )
| op(e0,e0) != e0 ) ) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_15,plain,
( op(e1,e2) = e4
| op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_19,plain,
( op(e2,e1) = e4
| op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_24,plain,
( op(e3,e1) = e4
| op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_31,plain,
( op(e4,e3) = e4
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e1
| op(e4,e3) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_33,plain,
op(unit,e0) = e0,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_34,plain,
op(e0,unit) = e0,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_35,plain,
op(unit,e1) = e1,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_36,plain,
op(e1,unit) = e1,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_37,plain,
op(unit,e2) = e2,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_38,plain,
op(e2,unit) = e2,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_39,plain,
op(unit,e3) = e3,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_40,plain,
op(e3,unit) = e3,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_41,plain,
op(unit,e4) = e4,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_42,plain,
op(e4,unit) = e4,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_43,plain,
( unit = e4
| unit = e3
| unit = e2
| unit = e1
| unit = e0 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_60,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_61,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_65,plain,
( op(e4,e2) = e0
| op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_66,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_74,plain,
( op(e3,e4) = e0
| op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_75,plain,
( op(e4,e3) = e0
| op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_77,plain,
( op(e4,e3) = e1
| op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_79,plain,
( op(e4,e3) = e2
| op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_114,plain,
op(e2,e1) != op(e0,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_115,plain,
op(e0,e1) != op(e2,e1),
inference(copy,[status(thm)],[c_114]) ).
cnf(c_120,plain,
op(e2,e1) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_121,plain,
op(e1,e1) != op(e2,e1),
inference(copy,[status(thm)],[c_120]) ).
cnf(c_122,plain,
op(e3,e1) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_123,plain,
op(e1,e1) != op(e3,e1),
inference(copy,[status(thm)],[c_122]) ).
cnf(c_126,plain,
op(e3,e1) != op(e2,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_127,plain,
op(e2,e1) != op(e3,e1),
inference(copy,[status(thm)],[c_126]) ).
cnf(c_132,plain,
op(e1,e2) != op(e0,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_139,plain,
op(e2,e2) != op(e1,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_140,plain,
op(e1,e2) != op(e2,e2),
inference(copy,[status(thm)],[c_139]) ).
cnf(c_141,plain,
op(e3,e2) != op(e1,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_142,plain,
op(e1,e2) != op(e3,e2),
inference(copy,[status(thm)],[c_141]) ).
cnf(c_151,plain,
op(e1,e3) != op(e0,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_156,plain,
op(e4,e3) != op(e0,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_157,plain,
op(e0,e3) != op(e4,e3),
inference(copy,[status(thm)],[c_156]) ).
cnf(c_168,plain,
op(e4,e3) != op(e3,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_169,plain,
op(e3,e3) != op(e4,e3),
inference(copy,[status(thm)],[c_168]) ).
cnf(c_204,plain,
op(e0,e4) != op(e0,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_205,plain,
op(e0,e2) != op(e0,e4),
inference(copy,[status(thm)],[c_204]) ).
cnf(c_208,plain,
op(e1,e1) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_211,plain,
op(e1,e3) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_212,plain,
op(e1,e0) != op(e1,e3),
inference(copy,[status(thm)],[c_211]) ).
cnf(c_213,plain,
op(e1,e4) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_214,plain,
op(e1,e0) != op(e1,e4),
inference(copy,[status(thm)],[c_213]) ).
cnf(c_215,plain,
op(e1,e2) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_216,plain,
op(e1,e1) != op(e1,e2),
inference(copy,[status(thm)],[c_215]) ).
cnf(c_217,plain,
op(e1,e3) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_218,plain,
op(e1,e1) != op(e1,e3),
inference(copy,[status(thm)],[c_217]) ).
cnf(c_234,plain,
op(e2,e2) != op(e2,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_235,plain,
op(e2,e1) != op(e2,e2),
inference(copy,[status(thm)],[c_234]) ).
cnf(c_246,plain,
op(e3,e1) != op(e3,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_253,plain,
op(e3,e2) != op(e3,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_254,plain,
op(e3,e1) != op(e3,e2),
inference(copy,[status(thm)],[c_253]) ).
cnf(c_255,plain,
op(e3,e3) != op(e3,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_256,plain,
op(e3,e1) != op(e3,e3),
inference(copy,[status(thm)],[c_255]) ).
cnf(c_278,plain,
op(e4,e3) != op(e4,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_279,plain,
op(e4,e2) != op(e4,e3),
inference(copy,[status(thm)],[c_278]) ).
cnf(c_284,plain,
e1 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_285,plain,
e2 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_286,plain,
e0 != e2,
inference(copy,[status(thm)],[c_285]) ).
cnf(c_287,plain,
e3 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_288,plain,
e0 != e3,
inference(copy,[status(thm)],[c_287]) ).
cnf(c_289,plain,
e4 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_290,plain,
e0 != e4,
inference(copy,[status(thm)],[c_289]) ).
cnf(c_291,plain,
e2 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_292,plain,
e1 != e2,
inference(copy,[status(thm)],[c_291]) ).
cnf(c_293,plain,
e3 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_294,plain,
e1 != e3,
inference(copy,[status(thm)],[c_293]) ).
cnf(c_295,plain,
e4 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_296,plain,
e1 != e4,
inference(copy,[status(thm)],[c_295]) ).
cnf(c_297,plain,
e3 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_298,plain,
e2 != e3,
inference(copy,[status(thm)],[c_297]) ).
cnf(c_299,plain,
e4 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_300,plain,
e2 != e4,
inference(copy,[status(thm)],[c_299]) ).
cnf(c_301,plain,
e4 != e3,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_302,plain,
e3 != e4,
inference(copy,[status(thm)],[c_301]) ).
cnf(c_303,plain,
op(op(op(e2,e2),e2),op(op(e2,e2),e2)) = e0,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_304,plain,
op(op(e2,e2),e2) = e1,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_305,plain,
op(e2,e2) = e3,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_306,plain,
op(op(e2,e2),op(e2,e2)) = e4,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_7600,plain,
op(e3,op(e2,e2)) = e4,
inference(paramod,[status(thm)],[c_305,c_306]) ).
cnf(c_307,plain,
op(e3,e3) = e4,
inference(paramod,[status(thm)],[c_305,c_7600]) ).
fof(def_defn_00,definition,
( defn_00
<=> ( ( unit != e0
| op(e4,e4) != e0 )
& ( op(e4,e0) = e4
| op(e4,e4) != e0 )
& ( unit != e0
| op(e4,e3) != e0 )
& ( op(e4,e0) = e3
| op(e4,e3) != e0 )
& ( unit != e0
| op(e4,e2) != e0 )
& ( op(e4,e0) = e2
| op(e4,e2) != e0 )
& ( unit != e0
| op(e4,e1) != e0 )
& ( op(e4,e0) = e1
| op(e4,e1) != e0 )
& ( unit != e0
| op(e4,e0) != e0 )
& ( unit != e0
| op(e3,e4) != e0 )
& ( op(e3,e0) = e4
| op(e3,e4) != e0 )
& ( unit != e0
| op(e3,e3) != e0 )
& ( op(e3,e0) = e3
| op(e3,e3) != e0 )
& ( unit != e0
| op(e3,e2) != e0 )
& ( op(e3,e0) = e2
| op(e3,e2) != e0 )
& ( unit != e0
| op(e3,e1) != e0 )
& ( op(e3,e0) = e1
| op(e3,e1) != e0 )
& ( unit != e0
| op(e3,e0) != e0 )
& ( unit != e0
| op(e2,e4) != e0 )
& ( op(e2,e0) = e4
| op(e2,e4) != e0 )
& ( unit != e0
| op(e2,e3) != e0 )
& ( op(e2,e0) = e3
| op(e2,e3) != e0 )
& ( unit != e0
| op(e2,e2) != e0 )
& ( op(e2,e0) = e2
| op(e2,e2) != e0 )
& ( unit != e0
| op(e2,e1) != e0 )
& ( op(e2,e0) = e1
| op(e2,e1) != e0 )
& ( unit != e0
| op(e2,e0) != e0 )
& ( unit != e0
| op(e1,e4) != e0 )
& ( op(e1,e0) = e4
| op(e1,e4) != e0 )
& ( unit != e0
| op(e1,e3) != e0 )
& ( op(e1,e0) = e3
| op(e1,e3) != e0 )
& ( unit != e0
| op(e1,e2) != e0 )
& ( op(e1,e0) = e2
| op(e1,e2) != e0 )
& ( unit != e0
| op(e1,e1) != e0 )
& ( op(e1,e0) = e1
| op(e1,e1) != e0 )
& ( unit != e0
| op(e1,e0) != e0 )
& ( unit != e0
| op(e0,e4) != e0 )
& ( op(e0,e0) = e4
| op(e0,e4) != e0 )
& ( unit != e0
| op(e0,e3) != e0 )
& ( op(e0,e0) = e3
| op(e0,e3) != e0 )
& ( unit != e0
| op(e0,e2) != e0 )
& ( op(e0,e0) = e2
| op(e0,e2) != e0 )
& ( unit != e0
| op(e0,e1) != e0 )
& ( op(e0,e0) = e1
| op(e0,e1) != e0 )
& ( unit != e0
| op(e0,e0) != e0 ) ) ),
introduced(definition,[new_symbols(definition,[defn_00])],[]) ).
fof(def_defn_10,definition,
( defn_10
<=> ( ( unit != e1
| op(e4,e4) != e1 )
& ( op(e4,e1) = e4
| op(e4,e4) != e1 )
& ( unit != e1
| op(e4,e3) != e1 )
& ( op(e4,e1) = e3
| op(e4,e3) != e1 )
& ( unit != e1
| op(e4,e2) != e1 )
& ( op(e4,e1) = e2
| op(e4,e2) != e1 )
& ( unit != e1
| op(e4,e1) != e1 )
& ( unit != e1
| op(e4,e0) != e1 )
& ( op(e4,e1) = e0
| op(e4,e0) != e1 )
& ( unit != e1
| op(e3,e4) != e1 )
& ( op(e3,e1) = e4
| op(e3,e4) != e1 )
& ( unit != e1
| op(e3,e3) != e1 )
& ( op(e3,e1) = e3
| op(e3,e3) != e1 )
& ( unit != e1
| op(e3,e2) != e1 )
& ( op(e3,e1) = e2
| op(e3,e2) != e1 )
& ( unit != e1
| op(e3,e1) != e1 )
& ( unit != e1
| op(e3,e0) != e1 )
& ( op(e3,e1) = e0
| op(e3,e0) != e1 )
& ( unit != e1
| op(e2,e4) != e1 )
& ( op(e2,e1) = e4
| op(e2,e4) != e1 )
& ( unit != e1
| op(e2,e3) != e1 )
& ( op(e2,e1) = e3
| op(e2,e3) != e1 )
& ( unit != e1
| op(e2,e2) != e1 )
& ( op(e2,e1) = e2
| op(e2,e2) != e1 )
& ( unit != e1
| op(e2,e1) != e1 )
& ( unit != e1
| op(e2,e0) != e1 )
& ( op(e2,e1) = e0
| op(e2,e0) != e1 )
& ( unit != e1
| op(e1,e4) != e1 )
& ( op(e1,e1) = e4
| op(e1,e4) != e1 )
& ( unit != e1
| op(e1,e3) != e1 )
& ( op(e1,e1) = e3
| op(e1,e3) != e1 )
& ( unit != e1
| op(e1,e2) != e1 )
& ( op(e1,e1) = e2
| op(e1,e2) != e1 )
& ( unit != e1
| op(e1,e1) != e1 )
& ( unit != e1
| op(e1,e0) != e1 )
& ( op(e1,e1) = e0
| op(e1,e0) != e1 )
& ( unit != e1
| op(e0,e4) != e1 )
& ( op(e0,e1) = e4
| op(e0,e4) != e1 )
& ( unit != e1
| op(e0,e3) != e1 )
& ( op(e0,e1) = e3
| op(e0,e3) != e1 )
& ( unit != e1
| op(e0,e2) != e1 )
& ( op(e0,e1) = e2
| op(e0,e2) != e1 )
& ( unit != e1
| op(e0,e1) != e1 )
& ( unit != e1
| op(e0,e0) != e1 )
& ( op(e0,e1) = e0
| op(e0,e0) != e1 ) ) ),
introduced(definition,[new_symbols(definition,[defn_10])],[]) ).
fof(def_defn_20,definition,
( defn_20
<=> ( ( unit != e2
| op(e4,e4) != e2 )
& ( op(e4,e2) = e4
| op(e4,e4) != e2 )
& ( unit != e2
| op(e4,e3) != e2 )
& ( op(e4,e2) = e3
| op(e4,e3) != e2 )
& ( unit != e2
| op(e4,e2) != e2 )
& ( unit != e2
| op(e4,e1) != e2 )
& ( op(e4,e2) = e1
| op(e4,e1) != e2 )
& ( unit != e2
| op(e4,e0) != e2 )
& ( op(e4,e2) = e0
| op(e4,e0) != e2 )
& ( unit != e2
| op(e3,e4) != e2 )
& ( op(e3,e2) = e4
| op(e3,e4) != e2 )
& ( unit != e2
| op(e3,e3) != e2 )
& ( op(e3,e2) = e3
| op(e3,e3) != e2 )
& ( unit != e2
| op(e3,e2) != e2 )
& ( unit != e2
| op(e3,e1) != e2 )
& ( op(e3,e2) = e1
| op(e3,e1) != e2 )
& ( unit != e2
| op(e3,e0) != e2 )
& ( op(e3,e2) = e0
| op(e3,e0) != e2 )
& ( unit != e2
| op(e2,e4) != e2 )
& ( op(e2,e2) = e4
| op(e2,e4) != e2 )
& ( unit != e2
| op(e2,e3) != e2 )
& ( op(e2,e2) = e3
| op(e2,e3) != e2 )
& ( unit != e2
| op(e2,e2) != e2 )
& ( unit != e2
| op(e2,e1) != e2 )
& ( op(e2,e2) = e1
| op(e2,e1) != e2 )
& ( unit != e2
| op(e2,e0) != e2 )
& ( op(e2,e2) = e0
| op(e2,e0) != e2 )
& ( unit != e2
| op(e1,e4) != e2 )
& ( op(e1,e2) = e4
| op(e1,e4) != e2 )
& ( unit != e2
| op(e1,e3) != e2 )
& ( op(e1,e2) = e3
| op(e1,e3) != e2 )
& ( unit != e2
| op(e1,e2) != e2 )
& ( unit != e2
| op(e1,e1) != e2 )
& ( op(e1,e2) = e1
| op(e1,e1) != e2 )
& ( unit != e2
| op(e1,e0) != e2 )
& ( op(e1,e2) = e0
| op(e1,e0) != e2 )
& ( unit != e2
| op(e0,e4) != e2 )
& ( op(e0,e2) = e4
| op(e0,e4) != e2 )
& ( unit != e2
| op(e0,e3) != e2 )
& ( op(e0,e2) = e3
| op(e0,e3) != e2 )
& ( unit != e2
| op(e0,e2) != e2 )
& ( unit != e2
| op(e0,e1) != e2 )
& ( op(e0,e2) = e1
| op(e0,e1) != e2 )
& ( unit != e2
| op(e0,e0) != e2 )
& ( op(e0,e2) = e0
| op(e0,e0) != e2 ) ) ),
introduced(definition,[new_symbols(definition,[defn_20])],[]) ).
fof(def_defn_30,definition,
( defn_30
<=> ( ( unit != e3
| op(e4,e4) != e3 )
& ( op(e4,e3) = e4
| op(e4,e4) != e3 )
& ( unit != e3
| op(e4,e3) != e3 )
& ( unit != e3
| op(e4,e2) != e3 )
& ( op(e4,e3) = e2
| op(e4,e2) != e3 )
& ( unit != e3
| op(e4,e1) != e3 )
& ( op(e4,e3) = e1
| op(e4,e1) != e3 )
& ( unit != e3
| op(e4,e0) != e3 )
& ( op(e4,e3) = e0
| op(e4,e0) != e3 )
& ( unit != e3
| op(e3,e4) != e3 )
& ( op(e3,e3) = e4
| op(e3,e4) != e3 )
& ( unit != e3
| op(e3,e3) != e3 )
& ( unit != e3
| op(e3,e2) != e3 )
& ( op(e3,e3) = e2
| op(e3,e2) != e3 )
& ( unit != e3
| op(e3,e1) != e3 )
& ( op(e3,e3) = e1
| op(e3,e1) != e3 )
& ( unit != e3
| op(e3,e0) != e3 )
& ( op(e3,e3) = e0
| op(e3,e0) != e3 )
& ( unit != e3
| op(e2,e4) != e3 )
& ( op(e2,e3) = e4
| op(e2,e4) != e3 )
& ( unit != e3
| op(e2,e3) != e3 )
& ( unit != e3
| op(e2,e2) != e3 )
& ( op(e2,e3) = e2
| op(e2,e2) != e3 )
& ( unit != e3
| op(e2,e1) != e3 )
& ( op(e2,e3) = e1
| op(e2,e1) != e3 )
& ( unit != e3
| op(e2,e0) != e3 )
& ( op(e2,e3) = e0
| op(e2,e0) != e3 )
& ( unit != e3
| op(e1,e4) != e3 )
& ( op(e1,e3) = e4
| op(e1,e4) != e3 )
& ( unit != e3
| op(e1,e3) != e3 )
& ( unit != e3
| op(e1,e2) != e3 )
& ( op(e1,e3) = e2
| op(e1,e2) != e3 )
& ( unit != e3
| op(e1,e1) != e3 )
& ( op(e1,e3) = e1
| op(e1,e1) != e3 )
& ( unit != e3
| op(e1,e0) != e3 )
& ( op(e1,e3) = e0
| op(e1,e0) != e3 )
& ( unit != e3
| op(e0,e4) != e3 )
& ( op(e0,e3) = e4
| op(e0,e4) != e3 )
& ( unit != e3
| op(e0,e3) != e3 )
& ( unit != e3
| op(e0,e2) != e3 )
& ( op(e0,e3) = e2
| op(e0,e2) != e3 )
& ( unit != e3
| op(e0,e1) != e3 )
& ( op(e0,e3) = e1
| op(e0,e1) != e3 )
& ( unit != e3
| op(e0,e0) != e3 )
& ( op(e0,e3) = e0
| op(e0,e0) != e3 ) ) ),
introduced(definition,[new_symbols(definition,[defn_30])],[]) ).
cnf(c_343,negated_conjecture,
( unit != e4
| op(e3,e3) != e4
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00,def_defn_10,def_defn_20,def_defn_30]) ).
cnf(c_7601,negated_conjecture,
( unit != e4
| e4 != e4
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_307,c_343]) ).
cnf(c_344,negated_conjecture,
( unit != e4
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_7601]) ).
fof(def_defn_40,definition,
( defn_40
<=> ( op(op(e0,e1),e0) != e1
& op(op(e0,e1),e1) = e0
& op(e1,e0) != op(e0,e1) ) ),
introduced(definition,[new_symbols(definition,[defn_40])],[]) ).
fof(def_defn_50,definition,
( defn_50
<=> ( op(op(e0,e2),e0) != e2
& op(op(e0,e2),e2) = e0
& op(e2,e0) != op(e0,e2) ) ),
introduced(definition,[new_symbols(definition,[defn_50])],[]) ).
fof(def_defn_60,definition,
( defn_60
<=> ( op(op(e0,e3),e0) != e3
& op(op(e0,e3),e3) = e0
& op(e3,e0) != op(e0,e3) ) ),
introduced(definition,[new_symbols(definition,[defn_60])],[]) ).
fof(def_defn_70,definition,
( defn_70
<=> ( op(op(e0,e4),e0) != e4
& op(op(e0,e4),e4) = e0
& op(e4,e0) != op(e0,e4) ) ),
introduced(definition,[new_symbols(definition,[defn_70])],[]) ).
fof(def_defn_80,definition,
( defn_80
<=> ( op(op(e1,e0),e1) != e0
& op(op(e1,e0),e0) = e1
& op(e1,e0) != op(e0,e1) ) ),
introduced(definition,[new_symbols(definition,[defn_80])],[]) ).
fof(def_defn_90,definition,
( defn_90
<=> ( op(op(e1,e2),e1) != e2
& op(op(e1,e2),e2) = e1
& op(e2,e1) != op(e1,e2) ) ),
introduced(definition,[new_symbols(definition,[defn_90])],[]) ).
fof(def_defn_100,definition,
( defn_100
<=> ( op(op(e1,e3),e1) != e3
& op(op(e1,e3),e3) = e1
& op(e3,e1) != op(e1,e3) ) ),
introduced(definition,[new_symbols(definition,[defn_100])],[]) ).
fof(def_defn_110,definition,
( defn_110
<=> ( op(op(e1,e4),e1) != e4
& op(op(e1,e4),e4) = e1
& op(e4,e1) != op(e1,e4) ) ),
introduced(definition,[new_symbols(definition,[defn_110])],[]) ).
fof(def_defn_120,definition,
( defn_120
<=> ( op(op(e2,e0),e2) != e0
& op(op(e2,e0),e0) = e2
& op(e2,e0) != op(e0,e2) ) ),
introduced(definition,[new_symbols(definition,[defn_120])],[]) ).
fof(def_defn_130,definition,
( defn_130
<=> ( op(op(e2,e1),e2) != e1
& op(op(e2,e1),e1) = e2
& op(e2,e1) != op(e1,e2) ) ),
introduced(definition,[new_symbols(definition,[defn_130])],[]) ).
fof(def_defn_140,definition,
( defn_140
<=> ( op(op(e2,e3),e2) != e3
& op(op(e2,e3),e3) = e2
& op(e3,e2) != op(e2,e3) ) ),
introduced(definition,[new_symbols(definition,[defn_140])],[]) ).
fof(def_defn_150,definition,
( defn_150
<=> ( op(op(e2,e4),e2) != e4
& op(op(e2,e4),e4) = e2
& op(e4,e2) != op(e2,e4) ) ),
introduced(definition,[new_symbols(definition,[defn_150])],[]) ).
fof(def_defn_160,definition,
( defn_160
<=> ( op(op(e3,e0),e3) != e0
& op(op(e3,e0),e0) = e3
& op(e3,e0) != op(e0,e3) ) ),
introduced(definition,[new_symbols(definition,[defn_160])],[]) ).
fof(def_defn_170,definition,
( defn_170
<=> ( op(op(e3,e1),e3) != e1
& op(op(e3,e1),e1) = e3
& op(e3,e1) != op(e1,e3) ) ),
introduced(definition,[new_symbols(definition,[defn_170])],[]) ).
cnf(c_691,negated_conjecture,
( op(op(e4,e3),e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| op(e4,e0) != op(e0,e4)
| op(op(e3,e4),e4) = e3
| op(op(e3,e2),e2) = e3
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_40,def_defn_50,def_defn_60,def_defn_70,def_defn_80,def_defn_90,def_defn_100,def_defn_110,def_defn_120,def_defn_130,def_defn_140,def_defn_150,def_defn_160,def_defn_170]) ).
cnf(c_692,negated_conjecture,
( op(op(e4,e3),e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| op(e0,e4) != op(e4,e0)
| op(op(e3,e4),e4) = e3
| op(op(e3,e2),e2) = e3
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40 ),
inference(copy,[status(thm)],[c_691]) ).
cnf(c_1096,negated_conjecture,
( op(op(e3,e1),e1) = e3
| ~ defn_170 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_170]) ).
cnf(c_1101,negated_conjecture,
( op(e3,e0) != op(e0,e3)
| ~ defn_160 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_160]) ).
cnf(c_1102,negated_conjecture,
( op(e0,e3) != op(e3,e0)
| ~ defn_160 ),
inference(copy,[status(thm)],[c_1101]) ).
cnf(c_1104,negated_conjecture,
( op(op(e2,e4),e4) = e2
| ~ defn_150 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_150]) ).
cnf(c_1108,negated_conjecture,
( op(op(e2,e3),e3) = e2
| ~ defn_140 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_140]) ).
cnf(c_1113,negated_conjecture,
( op(e2,e1) != op(e1,e2)
| ~ defn_130 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_130]) ).
cnf(c_1114,negated_conjecture,
( op(e1,e2) != op(e2,e1)
| ~ defn_130 ),
inference(copy,[status(thm)],[c_1113]) ).
cnf(c_1117,negated_conjecture,
( op(e2,e0) != op(e0,e2)
| ~ defn_120 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_120]) ).
cnf(c_1118,negated_conjecture,
( op(e0,e2) != op(e2,e0)
| ~ defn_120 ),
inference(copy,[status(thm)],[c_1117]) ).
cnf(c_1121,negated_conjecture,
( op(e4,e1) != op(e1,e4)
| ~ defn_110 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_110]) ).
cnf(c_1122,negated_conjecture,
( op(e1,e4) != op(e4,e1)
| ~ defn_110 ),
inference(copy,[status(thm)],[c_1121]) ).
cnf(c_1125,negated_conjecture,
( op(e3,e1) != op(e1,e3)
| ~ defn_100 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_100]) ).
cnf(c_1126,negated_conjecture,
( op(e1,e3) != op(e3,e1)
| ~ defn_100 ),
inference(copy,[status(thm)],[c_1125]) ).
cnf(c_1129,negated_conjecture,
( op(e2,e1) != op(e1,e2)
| ~ defn_90 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_90]) ).
cnf(c_1130,negated_conjecture,
( op(e1,e2) != op(e2,e1)
| ~ defn_90 ),
inference(copy,[status(thm)],[c_1129]) ).
cnf(c_1133,negated_conjecture,
( op(e1,e0) != op(e0,e1)
| ~ defn_80 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_80]) ).
cnf(c_1136,negated_conjecture,
( op(e4,e0) != op(e0,e4)
| ~ defn_70 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_70]) ).
cnf(c_1137,negated_conjecture,
( op(e0,e4) != op(e4,e0)
| ~ defn_70 ),
inference(copy,[status(thm)],[c_1136]) ).
cnf(c_1140,negated_conjecture,
( op(e3,e0) != op(e0,e3)
| ~ defn_60 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_60]) ).
cnf(c_1141,negated_conjecture,
( op(e0,e3) != op(e3,e0)
| ~ defn_60 ),
inference(copy,[status(thm)],[c_1140]) ).
cnf(c_1144,negated_conjecture,
( op(e2,e0) != op(e0,e2)
| ~ defn_50 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_50]) ).
cnf(c_1145,negated_conjecture,
( op(e0,e2) != op(e2,e0)
| ~ defn_50 ),
inference(copy,[status(thm)],[c_1144]) ).
cnf(c_1148,negated_conjecture,
( op(e1,e0) != op(e0,e1)
| ~ defn_40 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_40]) ).
cnf(c_1165,negated_conjecture,
( op(e3,e3) = e1
| op(e3,e1) != e3
| ~ defn_30 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_30]) ).
cnf(c_7602,negated_conjecture,
( e4 = e1
| op(e3,e1) != e3
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_307,c_1165]) ).
cnf(c_7603,negated_conjecture,
( e1 = e4
| op(e3,e1) != e3
| ~ defn_30 ),
inference(copy,[status(thm)],[c_7602]) ).
cnf(c_1166,negated_conjecture,
( op(e3,e1) != e3
| ~ defn_30 ),
inference(resolve,[status(thm)],[c_296,c_7603]) ).
cnf(c_1168,negated_conjecture,
( op(e3,e3) = e0
| op(e3,e0) != e3
| ~ defn_30 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_30]) ).
cnf(c_7604,negated_conjecture,
( e4 = e0
| op(e3,e0) != e3
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_307,c_1168]) ).
cnf(c_7605,negated_conjecture,
( e0 = e4
| op(e3,e0) != e3
| ~ defn_30 ),
inference(copy,[status(thm)],[c_7604]) ).
cnf(c_1169,negated_conjecture,
( op(e3,e0) != e3
| ~ defn_30 ),
inference(resolve,[status(thm)],[c_290,c_7605]) ).
cnf(c_1206,negated_conjecture,
( op(e2,e2) = e4
| op(e2,e4) != e2
| ~ defn_20 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_20]) ).
cnf(c_7606,negated_conjecture,
( e3 = e4
| op(e2,e4) != e2
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_305,c_1206]) ).
cnf(c_1207,negated_conjecture,
( op(e2,e4) != e2
| ~ defn_20 ),
inference(resolve,[status(thm)],[c_302,c_7606]) ).
cnf(c_1263,negated_conjecture,
( op(e1,e1) = e4
| op(e1,e4) != e1
| ~ defn_10 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_10]) ).
cnf(c_1313,negated_conjecture,
( unit != e0
| op(e1,e1) != e0
| ~ defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00]) ).
cnf(c_1314,negated_conjecture,
( op(e1,e0) = e1
| op(e1,e1) != e0
| ~ defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00]) ).
cnf(c_7607,plain,
op(op(e3,e2),op(op(e2,e2),e2)) = e0,
inference(paramod,[status(thm)],[c_305,c_303]) ).
cnf(c_1325,plain,
op(op(e3,e2),op(e3,e2)) = e0,
inference(paramod,[status(thm)],[c_305,c_7607]) ).
cnf(c_1326,plain,
op(e3,e2) = e1,
inference(paramod,[status(thm)],[c_305,c_304]) ).
cnf(c_1329,plain,
op(e2,e1) != e3,
inference(paramod,[status(thm)],[c_305,c_235]) ).
cnf(c_1332,plain,
op(e1,e2) != e3,
inference(paramod,[status(thm)],[c_305,c_140]) ).
cnf(c_7608,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| e3 = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 ),
inference(paramod,[status(thm)],[c_305,c_66]) ).
cnf(c_7609,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| e1 = e3
| op(e2,e1) = e1
| op(e2,e0) = e1 ),
inference(copy,[status(thm)],[c_7608]) ).
cnf(c_1338,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 ),
inference(resolve,[status(thm)],[c_294,c_7609]) ).
cnf(c_7610,plain,
( op(e4,e2) = e0
| op(e3,e2) = e0
| e3 = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 ),
inference(paramod,[status(thm)],[c_305,c_65]) ).
cnf(c_7611,plain,
( op(e4,e2) = e0
| e1 = e0
| e3 = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 ),
inference(paramod,[status(thm)],[c_1326,c_7610]) ).
cnf(c_7612,plain,
( op(e4,e2) = e0
| e1 = e0
| e0 = e3
| op(e1,e2) = e0
| op(e0,e2) = e0 ),
inference(copy,[status(thm)],[c_7611]) ).
cnf(c_7613,plain,
( op(e4,e2) = e0
| e1 = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 ),
inference(resolve,[status(thm)],[c_288,c_7612]) ).
cnf(c_1339,plain,
( op(e4,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 ),
inference(resolve,[status(thm)],[c_284,c_7613]) ).
cnf(c_1342,plain,
op(e3,e1) != e4,
inference(paramod,[status(thm)],[c_307,c_256]) ).
cnf(c_7614,plain,
e4 != op(e4,e3),
inference(paramod,[status(thm)],[c_307,c_169]) ).
cnf(c_1344,plain,
op(e4,e3) != e4,
inference(copy,[status(thm)],[c_7614]) ).
cnf(c_7615,plain,
( op(e4,e3) = e2
| e4 = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 ),
inference(paramod,[status(thm)],[c_307,c_79]) ).
cnf(c_7616,plain,
( op(e4,e3) = e2
| e2 = e4
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 ),
inference(copy,[status(thm)],[c_7615]) ).
cnf(c_1350,plain,
( op(e4,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 ),
inference(resolve,[status(thm)],[c_300,c_7616]) ).
cnf(c_7617,plain,
( op(e4,e3) = e1
| e4 = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 ),
inference(paramod,[status(thm)],[c_307,c_77]) ).
cnf(c_7618,plain,
( op(e4,e3) = e1
| e1 = e4
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 ),
inference(copy,[status(thm)],[c_7617]) ).
cnf(c_1352,plain,
( op(e4,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 ),
inference(resolve,[status(thm)],[c_296,c_7618]) ).
cnf(c_7619,plain,
( op(e4,e3) = e0
| e4 = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 ),
inference(paramod,[status(thm)],[c_307,c_75]) ).
cnf(c_7620,plain,
( op(e4,e3) = e0
| e0 = e4
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 ),
inference(copy,[status(thm)],[c_7619]) ).
cnf(c_1353,plain,
( op(e4,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 ),
inference(resolve,[status(thm)],[c_290,c_7620]) ).
cnf(c_7621,plain,
( op(e3,e4) = e0
| op(e3,e3) = e0
| e1 = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(paramod,[status(thm)],[c_1326,c_74]) ).
cnf(c_7622,plain,
( op(e3,e4) = e0
| e4 = e0
| e1 = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(paramod,[status(thm)],[c_307,c_7621]) ).
cnf(c_7623,plain,
( op(e3,e4) = e0
| e0 = e4
| e1 = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(copy,[status(thm)],[c_7622]) ).
cnf(c_7624,plain,
( op(e3,e4) = e0
| e0 = e4
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(resolve,[status(thm)],[c_284,c_7623]) ).
cnf(c_1354,plain,
( op(e3,e4) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(resolve,[status(thm)],[c_290,c_7624]) ).
cnf(c_7625,plain,
op(e1,op(e3,e2)) = e0,
inference(paramod,[status(thm)],[c_1326,c_1325]) ).
cnf(c_1355,plain,
op(e1,e1) = e0,
inference(paramod,[status(thm)],[c_1326,c_7625]) ).
cnf(c_7626,negated_conjecture,
( op(op(e4,e3),e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| op(e0,e4) != op(e4,e0)
| op(op(e3,e4),e4) = e3
| op(e1,e2) = e3
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40 ),
inference(paramod,[status(thm)],[c_1326,c_692]) ).
cnf(c_1594,negated_conjecture,
( op(op(e4,e3),e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| op(e0,e4) != op(e4,e0)
| op(op(e3,e4),e4) = e3
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40 ),
inference(resolve,[status(thm)],[c_1332,c_7626]) ).
cnf(c_1632,plain,
op(e3,e1) != e1,
inference(paramod,[status(thm)],[c_1326,c_254]) ).
cnf(c_1635,plain,
op(e1,e2) != e1,
inference(paramod,[status(thm)],[c_1326,c_142]) ).
cnf(c_7627,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| e0 = e3
| op(e0,e1) = e3 ),
inference(paramod,[status(thm)],[c_1355,c_61]) ).
cnf(c_7628,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e0,e1) = e3 ),
inference(resolve,[status(thm)],[c_288,c_7627]) ).
cnf(c_1641,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e0,e1) = e3 ),
inference(resolve,[status(thm)],[c_1329,c_7628]) ).
cnf(c_1642,plain,
( op(e2,e1) = e4
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 ),
inference(resolve,[status(thm)],[c_1329,c_19]) ).
cnf(c_7629,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| e0 = e3
| op(e1,e0) = e3 ),
inference(paramod,[status(thm)],[c_1355,c_60]) ).
cnf(c_7630,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e0) = e3 ),
inference(resolve,[status(thm)],[c_288,c_7629]) ).
cnf(c_1650,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e0) = e3 ),
inference(resolve,[status(thm)],[c_1332,c_7630]) ).
cnf(c_7631,plain,
( op(e1,e2) = e4
| op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e0 ),
inference(resolve,[status(thm)],[c_1635,c_15]) ).
cnf(c_1651,plain,
( op(e1,e2) = e4
| op(e1,e2) = e2
| op(e1,e2) = e0 ),
inference(resolve,[status(thm)],[c_1332,c_7631]) ).
cnf(c_7632,plain,
( op(e3,e1) = e4
| op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e0 ),
inference(resolve,[status(thm)],[c_1632,c_24]) ).
cnf(c_1658,plain,
( op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e0 ),
inference(resolve,[status(thm)],[c_1342,c_7632]) ).
cnf(c_1664,plain,
( op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e1
| op(e4,e3) = e0 ),
inference(resolve,[status(thm)],[c_1344,c_31]) ).
cnf(c_7633,negated_conjecture,
( op(e1,e0) = e1
| e0 != e0
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_1355,c_1314]) ).
cnf(c_1672,negated_conjecture,
( op(e1,e0) = e1
| ~ defn_00 ),
inference(copy,[status(thm)],[c_7633]) ).
cnf(c_7634,negated_conjecture,
( unit != e0
| e0 != e0
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_1355,c_1313]) ).
cnf(c_1673,negated_conjecture,
( unit != e0
| ~ defn_00 ),
inference(copy,[status(thm)],[c_7634]) ).
cnf(c_7635,negated_conjecture,
( e0 = e4
| op(e1,e4) != e1
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_1355,c_1263]) ).
cnf(c_1675,negated_conjecture,
( op(e1,e4) != e1
| ~ defn_10 ),
inference(resolve,[status(thm)],[c_290,c_7635]) ).
cnf(c_7636,plain,
e0 != op(e1,e3),
inference(paramod,[status(thm)],[c_1355,c_218]) ).
cnf(c_1677,plain,
op(e1,e3) != e0,
inference(copy,[status(thm)],[c_7636]) ).
cnf(c_7637,plain,
e0 != op(e1,e2),
inference(paramod,[status(thm)],[c_1355,c_216]) ).
cnf(c_1678,plain,
op(e1,e2) != e0,
inference(copy,[status(thm)],[c_7637]) ).
cnf(c_7638,plain,
e0 != op(e1,e0),
inference(paramod,[status(thm)],[c_1355,c_208]) ).
cnf(c_1679,plain,
op(e1,e0) != e0,
inference(copy,[status(thm)],[c_7638]) ).
cnf(c_7639,plain,
e0 != op(e3,e1),
inference(paramod,[status(thm)],[c_1355,c_123]) ).
cnf(c_1681,plain,
op(e3,e1) != e0,
inference(copy,[status(thm)],[c_7639]) ).
cnf(c_7640,plain,
e0 != op(e2,e1),
inference(paramod,[status(thm)],[c_1355,c_121]) ).
cnf(c_1682,plain,
op(e2,e1) != e0,
inference(copy,[status(thm)],[c_7640]) ).
cnf(c_1698,plain,
( op(e4,e3) = e0
| op(e2,e3) = e0
| op(e0,e3) = e0 ),
inference(resolve,[status(thm)],[c_1677,c_1353]) ).
cnf(c_1700,plain,
( op(e1,e2) = e4
| op(e1,e2) = e2 ),
inference(resolve,[status(thm)],[c_1678,c_1651]) ).
cnf(c_1701,plain,
( op(e4,e2) = e0
| op(e0,e2) = e0 ),
inference(resolve,[status(thm)],[c_1678,c_1339]) ).
cnf(c_1708,plain,
( op(e3,e1) = e3
| op(e3,e1) = e2 ),
inference(resolve,[status(thm)],[c_1681,c_1658]) ).
cnf(c_1709,plain,
( op(e3,e4) = e0
| op(e3,e0) = e0 ),
inference(resolve,[status(thm)],[c_1681,c_1354]) ).
cnf(c_1710,plain,
( op(e2,e1) = e4
| op(e2,e1) = e2
| op(e2,e1) = e1 ),
inference(resolve,[status(thm)],[c_1682,c_1642]) ).
cnf(c_7641,plain,
( op(e1,e0) = e0
| unit = e4
| unit = e3
| unit = e2
| unit = e0 ),
inference(paramod,[status(thm)],[c_43,c_33]) ).
cnf(c_1717,plain,
( unit = e4
| unit = e3
| unit = e2
| unit = e0 ),
inference(resolve,[status(thm)],[c_1679,c_7641]) ).
cnf(c_3310,plain,
( op(e1,e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| op(e0,e4) != op(e4,e0)
| op(op(e3,e4),e4) = e3
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e0 ),
inference(paramod,[status(thm)],[c_1664,c_1594]) ).
cnf(c_7642,plain,
( op(e4,e3) = e2
| e0 = e2
| op(e1,e3) = e2
| op(e0,e3) = e2
| op(e4,e3) = e0
| op(e0,e3) = e0 ),
inference(paramod,[status(thm)],[c_1698,c_1350]) ).
cnf(c_3969,plain,
( op(e4,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2
| op(e4,e3) = e0
| op(e0,e3) = e0 ),
inference(resolve,[status(thm)],[c_286,c_7642]) ).
cnf(c_7643,plain,
( op(e4,e3) = e1
| e0 = e1
| op(e1,e3) = e1
| op(e0,e3) = e1
| op(e4,e3) = e0
| op(e0,e3) = e0 ),
inference(paramod,[status(thm)],[c_1698,c_1352]) ).
cnf(c_7644,plain,
( op(e4,e3) = e1
| e1 = e0
| op(e1,e3) = e1
| op(e0,e3) = e1
| op(e4,e3) = e0
| op(e0,e3) = e0 ),
inference(copy,[status(thm)],[c_7643]) ).
cnf(c_3972,plain,
( op(e4,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1
| op(e4,e3) = e0
| op(e0,e3) = e0 ),
inference(resolve,[status(thm)],[c_284,c_7644]) ).
cnf(c_4313,plain,
( op(e2,e1) != e2
| op(e3,e1) = e3 ),
inference(paramod,[status(thm)],[c_1708,c_127]) ).
cnf(c_7645,plain,
( op(e3,e1) = e1
| unit = e4
| unit = e2
| unit = e0 ),
inference(paramod,[status(thm)],[c_1717,c_35]) ).
cnf(c_4548,plain,
( unit = e4
| unit = e2
| unit = e0 ),
inference(resolve,[status(thm)],[c_1632,c_7645]) ).
cnf(c_7646,plain,
( op(e1,e2) = e1
| unit = e4
| unit = e0 ),
inference(paramod,[status(thm)],[c_4548,c_36]) ).
cnf(c_4605,plain,
( unit = e4
| unit = e0 ),
inference(resolve,[status(thm)],[c_1635,c_7646]) ).
cnf(c_4618,plain,
( defn_30
| defn_20
| defn_10
| defn_00
| unit = e0 ),
inference(resolve,[status(thm)],[c_4605,c_344]) ).
cnf(c_4622,plain,
( op(e0,e4) = e0
| unit = e0 ),
inference(paramod,[status(thm)],[c_4605,c_34]) ).
cnf(c_4623,plain,
( op(e0,e1) = e1
| unit = e4 ),
inference(paramod,[status(thm)],[c_4605,c_35]) ).
cnf(c_4625,plain,
( op(e1,e0) = e1
| unit = e4 ),
inference(paramod,[status(thm)],[c_4605,c_36]) ).
cnf(c_4626,plain,
( op(e1,e4) = e1
| unit = e0 ),
inference(paramod,[status(thm)],[c_4605,c_36]) ).
cnf(c_4627,plain,
( op(e0,e2) = e2
| unit = e4 ),
inference(paramod,[status(thm)],[c_4605,c_37]) ).
cnf(c_4628,plain,
( op(e4,e2) = e2
| unit = e0 ),
inference(paramod,[status(thm)],[c_4605,c_37]) ).
cnf(c_4629,plain,
( op(e2,e0) = e2
| unit = e4 ),
inference(paramod,[status(thm)],[c_4605,c_38]) ).
cnf(c_4630,plain,
( op(e2,e4) = e2
| unit = e0 ),
inference(paramod,[status(thm)],[c_4605,c_38]) ).
cnf(c_4631,plain,
( op(e0,e3) = e3
| unit = e4 ),
inference(paramod,[status(thm)],[c_4605,c_39]) ).
cnf(c_4633,plain,
( op(e3,e0) = e3
| unit = e4 ),
inference(paramod,[status(thm)],[c_4605,c_40]) ).
cnf(c_4635,plain,
( op(e0,e4) = e4
| unit = e4 ),
inference(paramod,[status(thm)],[c_4605,c_41]) ).
cnf(c_4637,plain,
( op(e4,e0) = e4
| unit = e4 ),
inference(paramod,[status(thm)],[c_4605,c_42]) ).
cnf(c_4857,plain,
( op(e0,e2) != e0
| unit = e0 ),
inference(paramod,[status(thm)],[c_4622,c_205]) ).
cnf(c_7647,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| e1 = e3
| unit = e4 ),
inference(paramod,[status(thm)],[c_4623,c_1641]) ).
cnf(c_4878,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| unit = e4 ),
inference(resolve,[status(thm)],[c_294,c_7647]) ).
cnf(c_7648,plain,
( e1 != op(e1,e3)
| unit = e4 ),
inference(paramod,[status(thm)],[c_4625,c_212]) ).
cnf(c_4933,plain,
( op(e1,e3) != e1
| unit = e4 ),
inference(copy,[status(thm)],[c_7648]) ).
cnf(c_7649,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| e1 = e3
| unit = e4 ),
inference(paramod,[status(thm)],[c_4625,c_1650]) ).
cnf(c_4935,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| unit = e4 ),
inference(resolve,[status(thm)],[c_294,c_7649]) ).
cnf(c_7650,negated_conjecture,
( defn_30
| defn_20
| defn_00
| unit = e0
| op(e1,e4) != e1 ),
inference(resolve,[status(thm)],[c_1675,c_4618]) ).
cnf(c_7651,negated_conjecture,
( unit = e0
| defn_30
| defn_20
| defn_00
| unit = e0 ),
inference(resolve,[status(thm)],[c_7650,c_4626]) ).
cnf(c_4941,negated_conjecture,
( defn_30
| defn_20
| defn_00
| unit = e0 ),
inference(copy,[status(thm)],[c_7651]) ).
cnf(c_7652,plain,
( op(e4,e2) = e0
| e2 = e0
| unit = e4 ),
inference(paramod,[status(thm)],[c_4627,c_1701]) ).
cnf(c_7653,plain,
( op(e4,e2) = e0
| e0 = e2
| unit = e4 ),
inference(copy,[status(thm)],[c_7652]) ).
cnf(c_5075,plain,
( op(e4,e2) = e0
| unit = e4 ),
inference(resolve,[status(thm)],[c_286,c_7653]) ).
cnf(c_7654,plain,
( e2 = e0
| op(e0,e2) = e0
| unit = e0 ),
inference(paramod,[status(thm)],[c_4628,c_1701]) ).
cnf(c_7655,plain,
( e0 = e2
| op(e0,e2) = e0
| unit = e0 ),
inference(copy,[status(thm)],[c_7654]) ).
cnf(c_5102,plain,
( op(e0,e2) = e0
| unit = e0 ),
inference(resolve,[status(thm)],[c_286,c_7655]) ).
cnf(c_7656,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e1) = e1
| e2 = e1
| unit = e4 ),
inference(paramod,[status(thm)],[c_4629,c_1338]) ).
cnf(c_7657,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e1) = e1
| e1 = e2
| unit = e4 ),
inference(copy,[status(thm)],[c_7656]) ).
cnf(c_5114,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e1) = e1
| unit = e4 ),
inference(resolve,[status(thm)],[c_292,c_7657]) ).
cnf(c_7658,negated_conjecture,
( defn_30
| defn_00
| unit = e0
| op(e2,e4) != e2 ),
inference(resolve,[status(thm)],[c_1207,c_4941]) ).
cnf(c_7659,negated_conjecture,
( unit = e0
| defn_30
| defn_00
| unit = e0 ),
inference(resolve,[status(thm)],[c_7658,c_4630]) ).
cnf(c_5120,negated_conjecture,
( defn_30
| defn_00
| unit = e0 ),
inference(copy,[status(thm)],[c_7659]) ).
cnf(c_5174,plain,
( op(e0,e1) = e1
| defn_30
| defn_00 ),
inference(paramod,[status(thm)],[c_5120,c_35]) ).
cnf(c_5175,plain,
( op(e1,e0) = e1
| defn_30
| defn_00 ),
inference(paramod,[status(thm)],[c_5120,c_36]) ).
cnf(c_7660,negated_conjecture,
( op(e1,e0) = e1
| op(e1,e0) = e1
| defn_30 ),
inference(resolve,[status(thm)],[c_5175,c_1672]) ).
cnf(c_5300,negated_conjecture,
( op(e1,e0) = e1
| defn_30 ),
inference(copy,[status(thm)],[c_7660]) ).
cnf(c_7661,plain,
( e1 != op(e1,e4)
| defn_30 ),
inference(paramod,[status(thm)],[c_5300,c_214]) ).
cnf(c_5372,plain,
( op(e1,e4) != e1
| defn_30 ),
inference(copy,[status(thm)],[c_7661]) ).
cnf(c_5384,plain,
( unit = e0
| defn_30 ),
inference(resolve,[status(thm)],[c_5372,c_4626]) ).
cnf(c_7662,negated_conjecture,
( op(e0,e1) = e1
| defn_30
| unit != e0 ),
inference(resolve,[status(thm)],[c_1673,c_5174]) ).
cnf(c_7663,negated_conjecture,
( defn_30
| op(e0,e1) = e1
| defn_30 ),
inference(resolve,[status(thm)],[c_7662,c_5384]) ).
cnf(c_5412,negated_conjecture,
( op(e0,e1) = e1
| defn_30 ),
inference(copy,[status(thm)],[c_7663]) ).
cnf(c_5415,plain,
( op(e0,e2) = e2
| defn_30 ),
inference(paramod,[status(thm)],[c_5384,c_37]) ).
cnf(c_5418,plain,
( op(e3,e0) = e3
| defn_30 ),
inference(paramod,[status(thm)],[c_5384,c_40]) ).
cnf(c_7664,plain,
( e1 != op(e2,e1)
| defn_30 ),
inference(paramod,[status(thm)],[c_5412,c_115]) ).
cnf(c_5449,plain,
( op(e2,e1) != e1
| defn_30 ),
inference(copy,[status(thm)],[c_7664]) ).
cnf(c_5515,plain,
( op(e1,e2) != e2
| defn_30 ),
inference(paramod,[status(thm)],[c_5415,c_132]) ).
cnf(c_5632,plain,
( op(e3,e1) != e3
| defn_30 ),
inference(paramod,[status(thm)],[c_5418,c_246]) ).
cnf(c_7665,plain,
( op(e3,e4) = e0
| e3 = e0
| defn_30 ),
inference(paramod,[status(thm)],[c_5418,c_1709]) ).
cnf(c_7666,plain,
( op(e3,e4) = e0
| e0 = e3
| defn_30 ),
inference(copy,[status(thm)],[c_7665]) ).
cnf(c_5635,plain,
( op(e3,e4) = e0
| defn_30 ),
inference(resolve,[status(thm)],[c_288,c_7666]) ).
cnf(c_5730,plain,
( op(e2,e1) = e4
| op(e2,e1) = e2
| defn_30 ),
inference(resolve,[status(thm)],[c_5449,c_1710]) ).
cnf(c_5737,plain,
( op(e1,e2) = e4
| defn_30 ),
inference(resolve,[status(thm)],[c_5515,c_1700]) ).
cnf(c_5788,plain,
( op(e3,e1) = e2
| defn_30 ),
inference(resolve,[status(thm)],[c_5632,c_1708]) ).
cnf(c_7667,negated_conjecture,
( op(e3,e1) = e2
| op(e3,e1) != e3 ),
inference(resolve,[status(thm)],[c_1166,c_5788]) ).
cnf(c_7668,negated_conjecture,
( op(e3,e1) = e2
| op(e3,e1) = e2 ),
inference(resolve,[status(thm)],[c_7667,c_1708]) ).
cnf(c_5880,negated_conjecture,
op(e3,e1) = e2,
inference(copy,[status(thm)],[c_7668]) ).
cnf(c_7669,plain,
( op(e4,e1) = e3
| e2 = e3
| unit = e4 ),
inference(paramod,[status(thm)],[c_5880,c_4878]) ).
cnf(c_5911,plain,
( op(e4,e1) = e3
| unit = e4 ),
inference(resolve,[status(thm)],[c_298,c_7669]) ).
cnf(c_7670,plain,
( op(e2,e1) != e2
| e2 = e3 ),
inference(paramod,[status(thm)],[c_5880,c_4313]) ).
cnf(c_5919,plain,
op(e2,e1) != e2,
inference(resolve,[status(thm)],[c_298,c_7670]) ).
cnf(c_6015,negated_conjecture,
( op(e1,e3) != e2
| ~ defn_100 ),
inference(paramod,[status(thm)],[c_5880,c_1126]) ).
cnf(c_7671,negated_conjecture,
( op(e2,e1) = e3
| ~ defn_170 ),
inference(paramod,[status(thm)],[c_5880,c_1096]) ).
cnf(c_6017,negated_conjecture,
~ defn_170,
inference(resolve,[status(thm)],[c_1329,c_7671]) ).
cnf(c_6337,plain,
( op(e2,e1) = e4
| defn_30 ),
inference(resolve,[status(thm)],[c_5919,c_5730]) ).
cnf(c_6743,negated_conjecture,
( op(e1,e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| op(e0,e4) != op(e4,e0)
| op(op(e3,e4),e4) = e3
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e0 ),
inference(resolve,[status(thm)],[c_6017,c_3310]) ).
cnf(c_7402,plain,
( op(e1,e3) != e3
| unit = e4 ),
inference(paramod,[status(thm)],[c_4631,c_151]) ).
cnf(c_7672,plain,
( e3 != op(e4,e3)
| unit = e4 ),
inference(paramod,[status(thm)],[c_4631,c_157]) ).
cnf(c_7403,plain,
( op(e4,e3) != e3
| unit = e4 ),
inference(copy,[status(thm)],[c_7672]) ).
cnf(c_7673,plain,
( op(e4,e3) = e0
| op(e2,e3) = e0
| e3 = e0
| unit = e4 ),
inference(paramod,[status(thm)],[c_4631,c_1698]) ).
cnf(c_7674,plain,
( op(e4,e3) = e0
| op(e2,e3) = e0
| e0 = e3
| unit = e4 ),
inference(copy,[status(thm)],[c_7673]) ).
cnf(c_7409,plain,
( op(e4,e3) = e0
| op(e2,e3) = e0
| unit = e4 ),
inference(resolve,[status(thm)],[c_288,c_7674]) ).
cnf(c_7675,negated_conjecture,
( op(e2,e1) = e4
| op(e3,e0) != e3 ),
inference(resolve,[status(thm)],[c_1169,c_6337]) ).
cnf(c_7419,negated_conjecture,
( unit = e4
| op(e2,e1) = e4 ),
inference(resolve,[status(thm)],[c_7675,c_4633]) ).
cnf(c_7676,negated_conjecture,
( op(e1,e2) = e4
| op(e3,e0) != e3 ),
inference(resolve,[status(thm)],[c_1169,c_5737]) ).
cnf(c_7420,negated_conjecture,
( unit = e4
| op(e1,e2) = e4 ),
inference(resolve,[status(thm)],[c_7676,c_4633]) ).
cnf(c_7677,negated_conjecture,
( op(e3,e4) = e0
| op(e3,e0) != e3 ),
inference(resolve,[status(thm)],[c_1169,c_5635]) ).
cnf(c_7421,negated_conjecture,
( unit = e4
| op(e3,e4) = e0 ),
inference(resolve,[status(thm)],[c_7677,c_4633]) ).
cnf(c_7678,plain,
( e0 != op(e4,e3)
| unit = e4 ),
inference(paramod,[status(thm)],[c_5075,c_279]) ).
cnf(c_7482,plain,
( op(e4,e3) != e0
| unit = e4 ),
inference(copy,[status(thm)],[c_7678]) ).
cnf(c_7679,plain,
( unit = e0
| unit = e0 ),
inference(resolve,[status(thm)],[c_5102,c_4857]) ).
cnf(c_7487,plain,
unit = e0,
inference(copy,[status(thm)],[c_7679]) ).
cnf(c_7680,plain,
( op(e4,e3) != e0
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_7482]) ).
cnf(c_7498,plain,
op(e4,e3) != e0,
inference(resolve,[status(thm)],[c_290,c_7680]) ).
cnf(c_7681,negated_conjecture,
( e0 = e4
| op(e3,e4) = e0 ),
inference(paramod,[status(thm)],[c_7487,c_7421]) ).
cnf(c_7522,negated_conjecture,
op(e3,e4) = e0,
inference(resolve,[status(thm)],[c_290,c_7681]) ).
cnf(c_7682,negated_conjecture,
( e0 = e4
| op(e1,e2) = e4 ),
inference(paramod,[status(thm)],[c_7487,c_7420]) ).
cnf(c_7523,negated_conjecture,
op(e1,e2) = e4,
inference(resolve,[status(thm)],[c_290,c_7682]) ).
cnf(c_7683,negated_conjecture,
( e0 = e4
| op(e2,e1) = e4 ),
inference(paramod,[status(thm)],[c_7487,c_7419]) ).
cnf(c_7524,negated_conjecture,
op(e2,e1) = e4,
inference(resolve,[status(thm)],[c_290,c_7683]) ).
cnf(c_7684,plain,
( op(e4,e3) = e0
| op(e2,e3) = e0
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_7409]) ).
cnf(c_7685,plain,
( op(e4,e3) = e0
| op(e2,e3) = e0 ),
inference(resolve,[status(thm)],[c_290,c_7684]) ).
cnf(c_7525,plain,
op(e2,e3) = e0,
inference(resolve,[status(thm)],[c_7498,c_7685]) ).
cnf(c_7686,plain,
( op(e4,e3) != e3
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_7403]) ).
cnf(c_7531,plain,
op(e4,e3) != e3,
inference(resolve,[status(thm)],[c_290,c_7686]) ).
cnf(c_7687,plain,
( op(e1,e3) != e3
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_7402]) ).
cnf(c_7532,plain,
op(e1,e3) != e3,
inference(resolve,[status(thm)],[c_290,c_7687]) ).
cnf(c_7688,plain,
( op(e4,e1) = e3
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_5911]) ).
cnf(c_7533,plain,
op(e4,e1) = e3,
inference(resolve,[status(thm)],[c_290,c_7688]) ).
cnf(c_7689,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e1) = e1
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_5114]) ).
cnf(c_7690,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| e4 = e1
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7524,c_7689]) ).
cnf(c_7691,plain,
( op(e2,e4) = e1
| e0 = e1
| e4 = e1
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7525,c_7690]) ).
cnf(c_7692,plain,
( op(e2,e4) = e1
| e0 = e1
| e1 = e4
| e0 = e4 ),
inference(copy,[status(thm)],[c_7691]) ).
cnf(c_7693,plain,
( op(e2,e4) = e1
| e1 = e0
| e1 = e4
| e0 = e4 ),
inference(copy,[status(thm)],[c_7692]) ).
cnf(c_7694,plain,
( op(e2,e4) = e1
| e1 = e0
| e1 = e4 ),
inference(resolve,[status(thm)],[c_290,c_7693]) ).
cnf(c_7695,plain,
( op(e2,e4) = e1
| e1 = e0 ),
inference(resolve,[status(thm)],[c_296,c_7694]) ).
cnf(c_7534,plain,
op(e2,e4) = e1,
inference(resolve,[status(thm)],[c_284,c_7695]) ).
cnf(c_7696,plain,
( op(e4,e2) = e0
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_5075]) ).
cnf(c_7538,plain,
op(e4,e2) = e0,
inference(resolve,[status(thm)],[c_290,c_7696]) ).
cnf(c_7697,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_4935]) ).
cnf(c_7698,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3 ),
inference(resolve,[status(thm)],[c_290,c_7697]) ).
cnf(c_7543,plain,
op(e1,e4) = e3,
inference(resolve,[status(thm)],[c_7532,c_7698]) ).
cnf(c_7699,plain,
( op(e1,e3) != e1
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_4933]) ).
cnf(c_7544,plain,
op(e1,e3) != e1,
inference(resolve,[status(thm)],[c_290,c_7699]) ).
cnf(c_7700,plain,
( op(e4,e0) = e4
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_4637]) ).
cnf(c_7556,plain,
op(e4,e0) = e4,
inference(resolve,[status(thm)],[c_290,c_7700]) ).
cnf(c_7701,plain,
( op(e0,e4) = e4
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_4635]) ).
cnf(c_7557,plain,
op(e0,e4) = e4,
inference(resolve,[status(thm)],[c_290,c_7701]) ).
cnf(c_7702,plain,
( op(e3,e0) = e3
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_4633]) ).
cnf(c_7558,plain,
op(e3,e0) = e3,
inference(resolve,[status(thm)],[c_290,c_7702]) ).
cnf(c_7703,plain,
( op(e0,e3) = e3
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_4631]) ).
cnf(c_7559,plain,
op(e0,e3) = e3,
inference(resolve,[status(thm)],[c_290,c_7703]) ).
cnf(c_7704,plain,
( op(e2,e0) = e2
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_4629]) ).
cnf(c_7560,plain,
op(e2,e0) = e2,
inference(resolve,[status(thm)],[c_290,c_7704]) ).
cnf(c_7705,plain,
( op(e0,e2) = e2
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_4627]) ).
cnf(c_7561,plain,
op(e0,e2) = e2,
inference(resolve,[status(thm)],[c_290,c_7705]) ).
cnf(c_7706,plain,
( op(e1,e0) = e1
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_4625]) ).
cnf(c_7562,plain,
op(e1,e0) = e1,
inference(resolve,[status(thm)],[c_290,c_7706]) ).
cnf(c_7707,plain,
( op(e0,e1) = e1
| e0 = e4 ),
inference(paramod,[status(thm)],[c_7487,c_4623]) ).
cnf(c_7563,plain,
op(e0,e1) = e1,
inference(resolve,[status(thm)],[c_290,c_7707]) ).
cnf(c_7708,negated_conjecture,
( op(e1,e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| op(e0,e4) != op(e4,e0)
| op(e0,e4) = e3
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e0 ),
inference(paramod,[status(thm)],[c_7522,c_6743]) ).
cnf(c_7709,negated_conjecture,
( op(e1,e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| op(e0,e4) != op(e4,e0)
| e4 = e3
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e0 ),
inference(paramod,[status(thm)],[c_7557,c_7708]) ).
cnf(c_7710,negated_conjecture,
( op(e1,e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| e4 != op(e4,e0)
| e4 = e3
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e0 ),
inference(paramod,[status(thm)],[c_7557,c_7709]) ).
cnf(c_7711,negated_conjecture,
( op(e1,e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| e4 != e4
| e4 = e3
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e0 ),
inference(paramod,[status(thm)],[c_7556,c_7710]) ).
cnf(c_7712,negated_conjecture,
( op(e1,e4) != e3
| op(op(e4,e2),e2) = e4
| op(e3,e1) = e4
| e4 != e4
| e4 = e3
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e0 ),
inference(paramod,[status(thm)],[c_7533,c_7711]) ).
cnf(c_7713,negated_conjecture,
( op(e1,e4) != e3
| op(op(e4,e2),e2) = e4
| e2 = e4
| e4 != e4
| e4 = e3
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e0 ),
inference(paramod,[status(thm)],[c_5880,c_7712]) ).
cnf(c_7714,negated_conjecture,
( op(e1,e4) != e3
| op(e0,e2) = e4
| e2 = e4
| e4 != e4
| e4 = e3
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e0 ),
inference(paramod,[status(thm)],[c_7538,c_7713]) ).
cnf(c_7715,negated_conjecture,
( op(e1,e4) != e3
| e2 = e4
| e2 = e4
| e4 != e4
| e4 = e3
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e0 ),
inference(paramod,[status(thm)],[c_7561,c_7714]) ).
cnf(c_7716,negated_conjecture,
( e3 != e3
| e2 = e4
| e2 = e4
| e4 != e4
| e4 = e3
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e0 ),
inference(paramod,[status(thm)],[c_7543,c_7715]) ).
cnf(c_7717,negated_conjecture,
( e3 != e3
| e2 = e4
| e2 = e4
| e4 != e4
| e3 = e4
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e0 ),
inference(copy,[status(thm)],[c_7716]) ).
cnf(c_7718,negated_conjecture,
( e3 != e3
| e2 = e4
| e2 = e4
| e3 = e4
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e0 ),
inference(copy,[status(thm)],[c_7717]) ).
cnf(c_7719,negated_conjecture,
( e2 = e4
| e2 = e4
| e3 = e4
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e0 ),
inference(copy,[status(thm)],[c_7718]) ).
cnf(c_7720,negated_conjecture,
( e2 = e4
| e3 = e4
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e0 ),
inference(copy,[status(thm)],[c_7719]) ).
cnf(c_7721,negated_conjecture,
( e2 = e4
| e3 = e4
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e3
| op(e4,e3) = e2 ),
inference(resolve,[status(thm)],[c_7498,c_7720]) ).
cnf(c_7722,negated_conjecture,
( e2 = e4
| e3 = e4
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e2 ),
inference(resolve,[status(thm)],[c_7531,c_7721]) ).
cnf(c_7723,negated_conjecture,
( e2 = e4
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e2 ),
inference(resolve,[status(thm)],[c_302,c_7722]) ).
cnf(c_7575,negated_conjecture,
( defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| op(e4,e3) = e2 ),
inference(resolve,[status(thm)],[c_300,c_7723]) ).
cnf(c_7724,plain,
( op(e4,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1
| op(e4,e3) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_7559,c_3972]) ).
cnf(c_7725,plain,
( op(e4,e3) = e1
| op(e1,e3) = e1
| e3 = e1
| op(e4,e3) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_7559,c_7724]) ).
cnf(c_7726,plain,
( op(e4,e3) = e1
| op(e1,e3) = e1
| e3 = e1
| op(e4,e3) = e0
| e0 = e3 ),
inference(copy,[status(thm)],[c_7725]) ).
cnf(c_7727,plain,
( op(e4,e3) = e1
| op(e1,e3) = e1
| e1 = e3
| op(e4,e3) = e0
| e0 = e3 ),
inference(copy,[status(thm)],[c_7726]) ).
cnf(c_7728,plain,
( op(e4,e3) = e1
| op(e1,e3) = e1
| e1 = e3
| op(e4,e3) = e0 ),
inference(resolve,[status(thm)],[c_288,c_7727]) ).
cnf(c_7729,plain,
( op(e4,e3) = e1
| op(e1,e3) = e1
| e1 = e3 ),
inference(resolve,[status(thm)],[c_7498,c_7728]) ).
cnf(c_7730,plain,
( op(e4,e3) = e1
| op(e1,e3) = e1 ),
inference(resolve,[status(thm)],[c_294,c_7729]) ).
cnf(c_7577,plain,
op(e4,e3) = e1,
inference(resolve,[status(thm)],[c_7544,c_7730]) ).
cnf(c_7731,plain,
( op(e4,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2
| op(e4,e3) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_7559,c_3969]) ).
cnf(c_7732,plain,
( op(e4,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2
| e1 = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_7577,c_7731]) ).
cnf(c_7733,plain,
( op(e4,e3) = e2
| op(e1,e3) = e2
| e3 = e2
| e1 = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_7559,c_7732]) ).
cnf(c_7734,plain,
( e1 = e2
| op(e1,e3) = e2
| e3 = e2
| e1 = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_7577,c_7733]) ).
cnf(c_7735,plain,
( e1 = e2
| op(e1,e3) = e2
| e3 = e2
| e1 = e0
| e0 = e3 ),
inference(copy,[status(thm)],[c_7734]) ).
cnf(c_7736,plain,
( e1 = e2
| op(e1,e3) = e2
| e2 = e3
| e1 = e0
| e0 = e3 ),
inference(copy,[status(thm)],[c_7735]) ).
cnf(c_7737,plain,
( e1 = e2
| op(e1,e3) = e2
| e2 = e3
| e1 = e0 ),
inference(resolve,[status(thm)],[c_288,c_7736]) ).
cnf(c_7738,plain,
( e1 = e2
| op(e1,e3) = e2
| e2 = e3 ),
inference(resolve,[status(thm)],[c_284,c_7737]) ).
cnf(c_7739,plain,
( e1 = e2
| op(e1,e3) = e2 ),
inference(resolve,[status(thm)],[c_298,c_7738]) ).
cnf(c_7578,plain,
op(e1,e3) = e2,
inference(resolve,[status(thm)],[c_292,c_7739]) ).
cnf(c_7740,negated_conjecture,
( e4 != op(e2,e1)
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_7523,c_1130]) ).
cnf(c_7741,negated_conjecture,
( e4 != e4
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_7524,c_7740]) ).
cnf(c_7585,negated_conjecture,
~ defn_90,
inference(copy,[status(thm)],[c_7741]) ).
cnf(c_7742,negated_conjecture,
( e4 != op(e2,e1)
| ~ defn_130 ),
inference(paramod,[status(thm)],[c_7523,c_1114]) ).
cnf(c_7743,negated_conjecture,
( e4 != e4
| ~ defn_130 ),
inference(paramod,[status(thm)],[c_7524,c_7742]) ).
cnf(c_7586,negated_conjecture,
~ defn_130,
inference(copy,[status(thm)],[c_7743]) ).
cnf(c_7744,negated_conjecture,
( op(e0,e3) = e2
| ~ defn_140 ),
inference(paramod,[status(thm)],[c_7525,c_1108]) ).
cnf(c_7745,negated_conjecture,
( e3 = e2
| ~ defn_140 ),
inference(paramod,[status(thm)],[c_7559,c_7744]) ).
cnf(c_7746,negated_conjecture,
( e2 = e3
| ~ defn_140 ),
inference(copy,[status(thm)],[c_7745]) ).
cnf(c_7588,negated_conjecture,
~ defn_140,
inference(resolve,[status(thm)],[c_298,c_7746]) ).
cnf(c_7747,negated_conjecture,
( e3 != op(e4,e1)
| ~ defn_110 ),
inference(paramod,[status(thm)],[c_7543,c_1122]) ).
cnf(c_7748,negated_conjecture,
( e3 != e3
| ~ defn_110 ),
inference(paramod,[status(thm)],[c_7533,c_7747]) ).
cnf(c_7589,negated_conjecture,
~ defn_110,
inference(copy,[status(thm)],[c_7748]) ).
cnf(c_7749,negated_conjecture,
( op(e1,e4) = e2
| ~ defn_150 ),
inference(paramod,[status(thm)],[c_7534,c_1104]) ).
cnf(c_7750,negated_conjecture,
( e3 = e2
| ~ defn_150 ),
inference(paramod,[status(thm)],[c_7543,c_7749]) ).
cnf(c_7751,negated_conjecture,
( e2 = e3
| ~ defn_150 ),
inference(copy,[status(thm)],[c_7750]) ).
cnf(c_7590,negated_conjecture,
~ defn_150,
inference(resolve,[status(thm)],[c_298,c_7751]) ).
cnf(c_7752,negated_conjecture,
( e4 != op(e4,e0)
| ~ defn_70 ),
inference(paramod,[status(thm)],[c_7557,c_1137]) ).
cnf(c_7753,negated_conjecture,
( e4 != e4
| ~ defn_70 ),
inference(paramod,[status(thm)],[c_7556,c_7752]) ).
cnf(c_7591,negated_conjecture,
~ defn_70,
inference(copy,[status(thm)],[c_7753]) ).
cnf(c_7754,negated_conjecture,
( e3 != op(e3,e0)
| ~ defn_60 ),
inference(paramod,[status(thm)],[c_7559,c_1141]) ).
cnf(c_7755,negated_conjecture,
( e3 != e3
| ~ defn_60 ),
inference(paramod,[status(thm)],[c_7558,c_7754]) ).
cnf(c_7592,negated_conjecture,
~ defn_60,
inference(copy,[status(thm)],[c_7755]) ).
cnf(c_7756,negated_conjecture,
( e3 != op(e3,e0)
| ~ defn_160 ),
inference(paramod,[status(thm)],[c_7559,c_1102]) ).
cnf(c_7757,negated_conjecture,
( e3 != e3
| ~ defn_160 ),
inference(paramod,[status(thm)],[c_7558,c_7756]) ).
cnf(c_7593,negated_conjecture,
~ defn_160,
inference(copy,[status(thm)],[c_7757]) ).
cnf(c_7758,negated_conjecture,
( e2 != op(e2,e0)
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_7561,c_1145]) ).
cnf(c_7759,negated_conjecture,
( e2 != e2
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_7560,c_7758]) ).
cnf(c_7594,negated_conjecture,
~ defn_50,
inference(copy,[status(thm)],[c_7759]) ).
cnf(c_7760,negated_conjecture,
( e2 != op(e2,e0)
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_7561,c_1118]) ).
cnf(c_7761,negated_conjecture,
( e2 != e2
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_7560,c_7760]) ).
cnf(c_7595,negated_conjecture,
~ defn_120,
inference(copy,[status(thm)],[c_7761]) ).
cnf(c_7762,negated_conjecture,
( e1 != op(e0,e1)
| ~ defn_40 ),
inference(paramod,[status(thm)],[c_7562,c_1148]) ).
cnf(c_7763,negated_conjecture,
( e1 != e1
| ~ defn_40 ),
inference(paramod,[status(thm)],[c_7563,c_7762]) ).
cnf(c_7596,negated_conjecture,
~ defn_40,
inference(copy,[status(thm)],[c_7763]) ).
cnf(c_7764,negated_conjecture,
( e1 != op(e0,e1)
| ~ defn_80 ),
inference(paramod,[status(thm)],[c_7562,c_1133]) ).
cnf(c_7765,negated_conjecture,
( e1 != e1
| ~ defn_80 ),
inference(paramod,[status(thm)],[c_7563,c_7764]) ).
cnf(c_7597,negated_conjecture,
~ defn_80,
inference(copy,[status(thm)],[c_7765]) ).
cnf(c_7766,negated_conjecture,
( defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| e1 = e2 ),
inference(paramod,[status(thm)],[c_7577,c_7575]) ).
cnf(c_7767,negated_conjecture,
( defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40 ),
inference(resolve,[status(thm)],[c_292,c_7766]) ).
cnf(c_7768,negated_conjecture,
( defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50 ),
inference(resolve,[status(thm)],[c_7596,c_7767]) ).
cnf(c_7769,negated_conjecture,
( defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60 ),
inference(resolve,[status(thm)],[c_7594,c_7768]) ).
cnf(c_7770,negated_conjecture,
( defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70 ),
inference(resolve,[status(thm)],[c_7592,c_7769]) ).
cnf(c_7771,negated_conjecture,
( defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80 ),
inference(resolve,[status(thm)],[c_7591,c_7770]) ).
cnf(c_7772,negated_conjecture,
( defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90 ),
inference(resolve,[status(thm)],[c_7597,c_7771]) ).
cnf(c_7773,negated_conjecture,
( defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100 ),
inference(resolve,[status(thm)],[c_7585,c_7772]) ).
cnf(c_7774,negated_conjecture,
( defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_100 ),
inference(resolve,[status(thm)],[c_7589,c_7773]) ).
cnf(c_7775,negated_conjecture,
( defn_160
| defn_150
| defn_140
| defn_130
| defn_100 ),
inference(resolve,[status(thm)],[c_7595,c_7774]) ).
cnf(c_7776,negated_conjecture,
( defn_160
| defn_150
| defn_140
| defn_100 ),
inference(resolve,[status(thm)],[c_7586,c_7775]) ).
cnf(c_7777,negated_conjecture,
( defn_160
| defn_150
| defn_100 ),
inference(resolve,[status(thm)],[c_7588,c_7776]) ).
cnf(c_7778,negated_conjecture,
( defn_160
| defn_100 ),
inference(resolve,[status(thm)],[c_7590,c_7777]) ).
cnf(c_7598,negated_conjecture,
defn_100,
inference(resolve,[status(thm)],[c_7593,c_7778]) ).
cnf(c_7779,negated_conjecture,
( e2 != e2
| ~ defn_100 ),
inference(paramod,[status(thm)],[c_7578,c_6015]) ).
cnf(c_7780,negated_conjecture,
~ defn_100,
inference(copy,[status(thm)],[c_7779]) ).
cnf(c_7599,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_7598,c_7780]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG059+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n006.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 21:04:11 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 2114863 was started by sandbox2 on n006,
% 0.10/0.36 % Sat Sep 26 21:04:11 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 5.45/5.76
% 5.45/5.76 % From the command line: assign(max_seconds, 300).
% 90.37/16.69
% 90.37/16.69 % given #500 (W,wt=16): 5518 defn_30 | op(e0,e1) != e2. [para(5415(b,1),197(a,2))].
% 90.37/16.69
% 90.37/16.69 % SZS status Theorem for theBenchmark
% 90.37/16.69
% 90.37/16.69 % Proof 1 at 2.49 (+ 0.31) seconds.
% 90.37/16.69 % Length of proof is 260.
% 90.37/16.69 % Level of proof is 26.
% 90.37/16.69 % Maximum clause weight is 96.000.
% 90.37/16.69 % Given clauses 615.
% 90.37/16.69
% 90.37/16.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------