%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG064+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:23 AM UTC 2026
% Result : Theorem 32.48s 8.23s
% Output : CNFRefutation 32.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 74
% Number of leaves : 21
% Syntax : Number of formulae : 558 ( 145 unt; 14 def)
% Number of atoms : 2751 (2201 equ)
% Maximal formula atoms : 250 ( 4 avg)
% Number of connectives : 2851 ( 658 ~;1847 |; 332 &)
% ( 14 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 15 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(e1,e1)
& e3 = op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1)))
& e2 = op(op(e1,e1),op(e1,e1))
& e0 = op(e1,op(op(e1,e1),op(e1,e1))) ),
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) ) )
& ( op(e4,e4) = e4
| op(e3,e3) = e4
| op(e2,e2) = e4
| op(e1,e1) = e4
| op(e0,e0) = e4 )
& ( op(e4,e4) = e3
| op(e3,e3) = e3
| op(e2,e2) = e3
| op(e1,e1) = e3
| op(e0,e0) = e3 )
& ( op(e4,e4) = e2
| op(e3,e3) = e2
| op(e2,e2) = e2
| op(e1,e1) = e2
| op(e0,e0) = e2 )
& ( op(e4,e4) = e1
| op(e3,e3) = e1
| op(e2,e2) = e1
| op(e1,e1) = e1
| op(e0,e0) = e1 )
& ( op(e4,e4) = e0
| op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e1) = 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) ) )
& ( op(e4,e4) = e4
| op(e3,e3) = e4
| op(e2,e2) = e4
| op(e1,e1) = e4
| op(e0,e0) = e4 )
& ( op(e4,e4) = e3
| op(e3,e3) = e3
| op(e2,e2) = e3
| op(e1,e1) = e3
| op(e0,e0) = e3 )
& ( op(e4,e4) = e2
| op(e3,e3) = e2
| op(e2,e2) = e2
| op(e1,e1) = e2
| op(e0,e0) = e2 )
& ( op(e4,e4) = e1
| op(e3,e3) = e1
| op(e2,e2) = e1
| op(e1,e1) = e1
| op(e0,e0) = e1 )
& ( op(e4,e4) = e0
| op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) = e0 ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_17,plain,
( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2
| op(e1,e4) = e1
| op(e1,e4) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_25,plain,
( op(e3,e2) = e4
| op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = 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_47,plain,
( op(e4,e0) = e1
| op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_48,plain,
( op(e0,e4) = e2
| op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_50,plain,
( op(e0,e4) = e3
| op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_52,plain,
( op(e0,e4) = e4
| op(e0,e3) = e4
| op(e0,e2) = e4
| op(e0,e1) = e4
| op(e0,e0) = e4 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_53,plain,
( op(e4,e0) = e4
| op(e3,e0) = e4
| op(e2,e0) = e4
| op(e1,e0) = e4
| op(e0,e0) = e4 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_58,plain,
( op(e1,e4) = e2
| op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_59,plain,
( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 ),
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_64,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_67,plain,
( op(e4,e2) = e1
| op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_72,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| op(e2,e2) = e4
| op(e2,e1) = e4
| op(e2,e0) = e4 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_73,plain,
( op(e4,e2) = e4
| op(e3,e2) = e4
| op(e2,e2) = e4
| op(e1,e2) = e4
| op(e0,e2) = e4 ),
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_78,plain,
( op(e3,e4) = e2
| op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_84,plain,
( op(e4,e4) = e0
| op(e4,e3) = e0
| op(e4,e2) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_87,plain,
( op(e4,e4) = e1
| op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| op(e0,e4) = e1 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_98,plain,
op(e3,e0) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_99,plain,
op(e0,e0) != op(e3,e0),
inference(copy,[status(thm)],[c_98]) ).
cnf(c_114,plain,
op(e1,e1) != op(e0,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_115,plain,
op(e0,e1) != op(e1,e1),
inference(copy,[status(thm)],[c_114]) ).
cnf(c_122,plain,
op(e2,e1) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_123,plain,
op(e1,e1) != op(e2,e1),
inference(copy,[status(thm)],[c_122]) ).
cnf(c_134,plain,
op(e1,e2) != op(e0,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_135,plain,
op(e0,e2) != op(e1,e2),
inference(copy,[status(thm)],[c_134]) ).
cnf(c_136,plain,
op(e2,e2) != op(e0,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_137,plain,
op(e0,e2) != op(e2,e2),
inference(copy,[status(thm)],[c_136]) ).
cnf(c_144,plain,
op(e3,e2) != op(e1,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_145,plain,
op(e1,e2) != op(e3,e2),
inference(copy,[status(thm)],[c_144]) ).
cnf(c_146,plain,
op(e4,e2) != op(e1,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_147,plain,
op(e1,e2) != op(e4,e2),
inference(copy,[status(thm)],[c_146]) ).
cnf(c_148,plain,
op(e3,e2) != op(e2,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_149,plain,
op(e2,e2) != op(e3,e2),
inference(copy,[status(thm)],[c_148]) ).
cnf(c_180,plain,
op(e4,e4) != op(e0,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_181,plain,
op(e0,e4) != op(e4,e4),
inference(copy,[status(thm)],[c_180]) ).
cnf(c_186,plain,
op(e4,e4) != op(e1,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_187,plain,
op(e1,e4) != op(e4,e4),
inference(copy,[status(thm)],[c_186]) ).
cnf(c_192,plain,
op(e4,e4) != op(e3,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_193,plain,
op(e3,e4) != op(e4,e4),
inference(copy,[status(thm)],[c_192]) ).
cnf(c_214,plain,
op(e1,e1) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_215,plain,
op(e1,e0) != op(e1,e1),
inference(copy,[status(thm)],[c_214]) ).
cnf(c_216,plain,
op(e1,e2) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_217,plain,
op(e1,e0) != op(e1,e2),
inference(copy,[status(thm)],[c_216]) ).
cnf(c_220,plain,
op(e1,e4) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_221,plain,
op(e1,e0) != op(e1,e4),
inference(copy,[status(thm)],[c_220]) ).
cnf(c_226,plain,
op(e1,e4) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_227,plain,
op(e1,e1) != op(e1,e4),
inference(copy,[status(thm)],[c_226]) ).
cnf(c_230,plain,
op(e1,e4) != op(e1,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_231,plain,
op(e1,e2) != op(e1,e4),
inference(copy,[status(thm)],[c_230]) ).
cnf(c_242,plain,
op(e2,e2) != op(e2,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_243,plain,
op(e2,e1) != op(e2,e2),
inference(copy,[status(thm)],[c_242]) ).
cnf(c_268,plain,
op(e3,e3) != op(e3,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_269,plain,
op(e3,e2) != op(e3,e3),
inference(copy,[status(thm)],[c_268]) ).
cnf(c_272,plain,
op(e3,e4) != op(e3,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_273,plain,
op(e3,e3) != op(e3,e4),
inference(copy,[status(thm)],[c_272]) ).
cnf(c_286,plain,
op(e4,e4) != op(e4,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_287,plain,
op(e4,e1) != op(e4,e4),
inference(copy,[status(thm)],[c_286]) ).
cnf(c_290,plain,
op(e4,e4) != op(e4,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_291,plain,
op(e4,e2) != op(e4,e4),
inference(copy,[status(thm)],[c_290]) ).
cnf(c_294,plain,
e1 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_295,plain,
e0 != e1,
inference(copy,[status(thm)],[c_294]) ).
cnf(c_296,plain,
e2 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_297,plain,
e0 != e2,
inference(copy,[status(thm)],[c_296]) ).
cnf(c_298,plain,
e3 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_299,plain,
e0 != e3,
inference(copy,[status(thm)],[c_298]) ).
cnf(c_300,plain,
e4 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_301,plain,
e0 != e4,
inference(copy,[status(thm)],[c_300]) ).
cnf(c_302,plain,
e2 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_303,plain,
e1 != e2,
inference(copy,[status(thm)],[c_302]) ).
cnf(c_304,plain,
e3 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_305,plain,
e1 != e3,
inference(copy,[status(thm)],[c_304]) ).
cnf(c_306,plain,
e4 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_307,plain,
e1 != e4,
inference(copy,[status(thm)],[c_306]) ).
cnf(c_308,plain,
e3 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_309,plain,
e2 != e3,
inference(copy,[status(thm)],[c_308]) ).
cnf(c_310,plain,
e4 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_311,plain,
e2 != e4,
inference(copy,[status(thm)],[c_310]) ).
cnf(c_312,plain,
e4 != e3,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_313,plain,
e3 != e4,
inference(copy,[status(thm)],[c_312]) ).
cnf(c_314,plain,
op(e1,op(op(e1,e1),op(e1,e1))) = e0,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_315,plain,
op(op(e1,e1),op(e1,e1)) = e2,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_316,plain,
op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1))) = e3,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_3162,plain,
op(e2,op(op(e1,e1),op(e1,e1))) = e3,
inference(paramod,[status(thm)],[c_315,c_316]) ).
cnf(c_317,plain,
op(e2,e2) = e3,
inference(paramod,[status(thm)],[c_315,c_3162]) ).
cnf(c_318,plain,
op(e1,e1) = e4,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_319,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) = e0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_3163,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| op(e2,e2) = e0
| e4 = e0
| op(e0,e0) = e0 ),
inference(paramod,[status(thm)],[c_318,c_319]) ).
cnf(c_3164,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| e3 = e0
| e4 = e0
| op(e0,e0) = e0 ),
inference(paramod,[status(thm)],[c_317,c_3163]) ).
cnf(c_3165,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| e3 = e0
| e0 = e4
| op(e0,e0) = e0 ),
inference(copy,[status(thm)],[c_3164]) ).
cnf(c_3166,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| e0 = e3
| e0 = e4
| op(e0,e0) = e0 ),
inference(copy,[status(thm)],[c_3165]) ).
cnf(c_3167,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| e0 = e3
| op(e0,e0) = e0 ),
inference(resolve,[status(thm)],[c_301,c_3166]) ).
cnf(c_320,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| op(e0,e0) = e0 ),
inference(resolve,[status(thm)],[c_299,c_3167]) ).
cnf(c_321,negated_conjecture,
( op(e4,e4) = e1
| op(e3,e3) = e1
| op(e2,e2) = e1
| op(e1,e1) = e1
| op(e0,e0) = e1 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_3168,negated_conjecture,
( op(e4,e4) = e1
| op(e3,e3) = e1
| op(e2,e2) = e1
| e4 = e1
| op(e0,e0) = e1 ),
inference(paramod,[status(thm)],[c_318,c_321]) ).
cnf(c_3169,negated_conjecture,
( op(e4,e4) = e1
| op(e3,e3) = e1
| e3 = e1
| e4 = e1
| op(e0,e0) = e1 ),
inference(paramod,[status(thm)],[c_317,c_3168]) ).
cnf(c_3170,negated_conjecture,
( op(e4,e4) = e1
| op(e3,e3) = e1
| e3 = e1
| e1 = e4
| op(e0,e0) = e1 ),
inference(copy,[status(thm)],[c_3169]) ).
cnf(c_3171,negated_conjecture,
( op(e4,e4) = e1
| op(e3,e3) = e1
| e1 = e3
| e1 = e4
| op(e0,e0) = e1 ),
inference(copy,[status(thm)],[c_3170]) ).
cnf(c_3172,negated_conjecture,
( op(e4,e4) = e1
| op(e3,e3) = e1
| e1 = e3
| op(e0,e0) = e1 ),
inference(resolve,[status(thm)],[c_307,c_3171]) ).
cnf(c_322,negated_conjecture,
( op(e4,e4) = e1
| op(e3,e3) = e1
| op(e0,e0) = e1 ),
inference(resolve,[status(thm)],[c_305,c_3172]) ).
fof(def_defn_00,definition,
( defn_00
<=> ( op(op(e0,e1),e0) != e1
& op(op(e0,e1),e1) = e0
& op(e1,e0) != op(e0,e1) ) ),
introduced(definition,[new_symbols(definition,[defn_00])],[]) ).
fof(def_defn_10,definition,
( defn_10
<=> ( op(op(e0,e2),e0) != e2
& op(op(e0,e2),e2) = e0
& op(e2,e0) != op(e0,e2) ) ),
introduced(definition,[new_symbols(definition,[defn_10])],[]) ).
fof(def_defn_20,definition,
( defn_20
<=> ( op(op(e0,e3),e0) != e3
& op(op(e0,e3),e3) = e0
& op(e3,e0) != op(e0,e3) ) ),
introduced(definition,[new_symbols(definition,[defn_20])],[]) ).
fof(def_defn_30,definition,
( defn_30
<=> ( op(op(e0,e4),e0) != e4
& op(op(e0,e4),e4) = e0
& op(e4,e0) != op(e0,e4) ) ),
introduced(definition,[new_symbols(definition,[defn_30])],[]) ).
fof(def_defn_40,definition,
( defn_40
<=> ( op(op(e1,e0),e1) != e0
& op(op(e1,e0),e0) = e1
& op(e1,e0) != op(e0,e1) ) ),
introduced(definition,[new_symbols(definition,[defn_40])],[]) ).
fof(def_defn_50,definition,
( defn_50
<=> ( op(op(e1,e2),e1) != e2
& op(op(e1,e2),e2) = e1
& op(e2,e1) != op(e1,e2) ) ),
introduced(definition,[new_symbols(definition,[defn_50])],[]) ).
fof(def_defn_60,definition,
( defn_60
<=> ( op(op(e1,e3),e1) != e3
& op(op(e1,e3),e3) = e1
& op(e3,e1) != op(e1,e3) ) ),
introduced(definition,[new_symbols(definition,[defn_60])],[]) ).
fof(def_defn_70,definition,
( defn_70
<=> ( op(op(e1,e4),e1) != e4
& op(op(e1,e4),e4) = e1
& op(e4,e1) != op(e1,e4) ) ),
introduced(definition,[new_symbols(definition,[defn_70])],[]) ).
fof(def_defn_80,definition,
( defn_80
<=> ( op(op(e2,e0),e2) != e0
& op(op(e2,e0),e0) = e2
& op(e2,e0) != op(e0,e2) ) ),
introduced(definition,[new_symbols(definition,[defn_80])],[]) ).
fof(def_defn_90,definition,
( defn_90
<=> ( op(op(e2,e1),e2) != e1
& op(op(e2,e1),e1) = e2
& op(e2,e1) != op(e1,e2) ) ),
introduced(definition,[new_symbols(definition,[defn_90])],[]) ).
fof(def_defn_100,definition,
( defn_100
<=> ( op(op(e2,e3),e2) != e3
& op(op(e2,e3),e3) = e2
& op(e3,e2) != op(e2,e3) ) ),
introduced(definition,[new_symbols(definition,[defn_100])],[]) ).
fof(def_defn_110,definition,
( defn_110
<=> ( op(op(e2,e4),e2) != e4
& op(op(e2,e4),e4) = e2
& op(e4,e2) != op(e2,e4) ) ),
introduced(definition,[new_symbols(definition,[defn_110])],[]) ).
fof(def_defn_120,definition,
( defn_120
<=> ( op(op(e3,e0),e3) != e0
& op(op(e3,e0),e0) = e3
& op(e3,e0) != op(e0,e3) ) ),
introduced(definition,[new_symbols(definition,[defn_120])],[]) ).
fof(def_defn_130,definition,
( defn_130
<=> ( op(op(e3,e1),e3) != e1
& op(op(e3,e1),e1) = e3
& op(e3,e1) != op(e1,e3) ) ),
introduced(definition,[new_symbols(definition,[defn_130])],[]) ).
cnf(c_663,negated_conjecture,
( op(op(e4,e3),e3) = e4
| op(e4,e2) != op(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_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| 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,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]) ).
cnf(c_3173,negated_conjecture,
( op(op(e4,e3),e3) = e4
| op(e4,e2) != op(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_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_663]) ).
cnf(c_664,negated_conjecture,
( op(op(e4,e3),e3) = e4
| op(e2,e4) != op(e4,e2)
| 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_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_3173]) ).
cnf(c_1075,negated_conjecture,
( op(e3,e1) != op(e1,e3)
| ~ defn_130 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_130]) ).
cnf(c_1076,negated_conjecture,
( op(e1,e3) != op(e3,e1)
| ~ defn_130 ),
inference(copy,[status(thm)],[c_1075]) ).
cnf(c_1079,negated_conjecture,
( op(e3,e0) != op(e0,e3)
| ~ defn_120 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_120]) ).
cnf(c_1080,negated_conjecture,
( op(e0,e3) != op(e3,e0)
| ~ defn_120 ),
inference(copy,[status(thm)],[c_1079]) ).
cnf(c_1083,negated_conjecture,
( op(e4,e2) != op(e2,e4)
| ~ defn_110 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_110]) ).
cnf(c_1084,negated_conjecture,
( op(e2,e4) != op(e4,e2)
| ~ defn_110 ),
inference(copy,[status(thm)],[c_1083]) ).
cnf(c_1087,negated_conjecture,
( op(e3,e2) != op(e2,e3)
| ~ defn_100 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_100]) ).
cnf(c_1088,negated_conjecture,
( op(e2,e3) != op(e3,e2)
| ~ defn_100 ),
inference(copy,[status(thm)],[c_1087]) ).
cnf(c_1091,negated_conjecture,
( op(e2,e1) != op(e1,e2)
| ~ defn_90 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_90]) ).
cnf(c_1092,negated_conjecture,
( op(e1,e2) != op(e2,e1)
| ~ defn_90 ),
inference(copy,[status(thm)],[c_1091]) ).
cnf(c_1095,negated_conjecture,
( op(e2,e0) != op(e0,e2)
| ~ defn_80 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_80]) ).
cnf(c_1096,negated_conjecture,
( op(e0,e2) != op(e2,e0)
| ~ defn_80 ),
inference(copy,[status(thm)],[c_1095]) ).
cnf(c_1099,negated_conjecture,
( op(e4,e1) != op(e1,e4)
| ~ defn_70 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_70]) ).
cnf(c_1100,negated_conjecture,
( op(e1,e4) != op(e4,e1)
| ~ defn_70 ),
inference(copy,[status(thm)],[c_1099]) ).
cnf(c_1103,negated_conjecture,
( op(e3,e1) != op(e1,e3)
| ~ defn_60 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_60]) ).
cnf(c_1104,negated_conjecture,
( op(e1,e3) != op(e3,e1)
| ~ defn_60 ),
inference(copy,[status(thm)],[c_1103]) ).
cnf(c_1107,negated_conjecture,
( op(e2,e1) != op(e1,e2)
| ~ defn_50 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_50]) ).
cnf(c_1108,negated_conjecture,
( op(e1,e2) != op(e2,e1)
| ~ defn_50 ),
inference(copy,[status(thm)],[c_1107]) ).
cnf(c_1111,negated_conjecture,
( op(e1,e0) != op(e0,e1)
| ~ defn_40 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_40]) ).
cnf(c_1112,negated_conjecture,
( op(e0,e1) != op(e1,e0)
| ~ defn_40 ),
inference(copy,[status(thm)],[c_1111]) ).
cnf(c_1113,negated_conjecture,
( op(op(e0,e4),e0) != e4
| ~ defn_30 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_30]) ).
cnf(c_1117,negated_conjecture,
( op(op(e0,e3),e0) != e3
| ~ defn_20 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_20]) ).
cnf(c_1121,negated_conjecture,
( op(op(e0,e2),e0) != e2
| ~ defn_10 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_10]) ).
cnf(c_1127,negated_conjecture,
( op(e1,e0) != op(e0,e1)
| ~ defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00]) ).
cnf(c_1128,negated_conjecture,
( op(e0,e1) != op(e1,e0)
| ~ defn_00 ),
inference(copy,[status(thm)],[c_1127]) ).
cnf(c_3174,plain,
op(e1,op(e4,op(e1,e1))) = e0,
inference(paramod,[status(thm)],[c_318,c_314]) ).
cnf(c_1129,plain,
op(e1,op(e4,e4)) = e0,
inference(paramod,[status(thm)],[c_318,c_3174]) ).
cnf(c_1132,plain,
op(e2,e1) != e3,
inference(paramod,[status(thm)],[c_317,c_243]) ).
cnf(c_3175,plain,
e3 != op(e3,e2),
inference(paramod,[status(thm)],[c_317,c_149]) ).
cnf(c_1135,plain,
op(e3,e2) != e3,
inference(copy,[status(thm)],[c_3175]) ).
cnf(c_1137,plain,
op(e0,e2) != e3,
inference(paramod,[status(thm)],[c_317,c_137]) ).
cnf(c_3176,plain,
( op(e4,e2) = e4
| op(e3,e2) = e4
| e3 = e4
| op(e1,e2) = e4
| op(e0,e2) = e4 ),
inference(paramod,[status(thm)],[c_317,c_73]) ).
cnf(c_1138,plain,
( op(e4,e2) = e4
| op(e3,e2) = e4
| op(e1,e2) = e4
| op(e0,e2) = e4 ),
inference(resolve,[status(thm)],[c_313,c_3176]) ).
cnf(c_3177,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| e3 = e4
| op(e2,e1) = e4
| op(e2,e0) = e4 ),
inference(paramod,[status(thm)],[c_317,c_72]) ).
cnf(c_1139,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| op(e2,e1) = e4
| op(e2,e0) = e4 ),
inference(resolve,[status(thm)],[c_313,c_3177]) ).
cnf(c_3178,plain,
( op(e4,e2) = e1
| op(e3,e2) = e1
| e3 = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 ),
inference(paramod,[status(thm)],[c_317,c_67]) ).
cnf(c_3179,plain,
( op(e4,e2) = e1
| op(e3,e2) = e1
| e1 = e3
| op(e1,e2) = e1
| op(e0,e2) = e1 ),
inference(copy,[status(thm)],[c_3178]) ).
cnf(c_1142,plain,
( op(e4,e2) = e1
| op(e3,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 ),
inference(resolve,[status(thm)],[c_305,c_3179]) ).
cnf(c_3180,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| e3 = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 ),
inference(paramod,[status(thm)],[c_317,c_64]) ).
cnf(c_3181,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| e0 = e3
| op(e2,e1) = e0
| op(e2,e0) = e0 ),
inference(copy,[status(thm)],[c_3180]) ).
cnf(c_1145,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 ),
inference(resolve,[status(thm)],[c_299,c_3181]) ).
cnf(c_3182,plain,
op(e4,op(e1,e1)) = e2,
inference(paramod,[status(thm)],[c_318,c_315]) ).
cnf(c_1146,plain,
op(e4,e4) = e2,
inference(paramod,[status(thm)],[c_318,c_3182]) ).
cnf(c_3183,plain,
e4 != op(e1,e4),
inference(paramod,[status(thm)],[c_318,c_227]) ).
cnf(c_1147,plain,
op(e1,e4) != e4,
inference(copy,[status(thm)],[c_3183]) ).
cnf(c_1150,plain,
op(e1,e0) != e4,
inference(paramod,[status(thm)],[c_318,c_215]) ).
cnf(c_3184,plain,
e4 != op(e2,e1),
inference(paramod,[status(thm)],[c_318,c_123]) ).
cnf(c_1153,plain,
op(e2,e1) != e4,
inference(copy,[status(thm)],[c_3184]) ).
cnf(c_1154,plain,
op(e0,e1) != e4,
inference(paramod,[status(thm)],[c_318,c_115]) ).
cnf(c_3185,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| e4 = e3
| op(e0,e1) = e3 ),
inference(paramod,[status(thm)],[c_318,c_61]) ).
cnf(c_3186,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| e3 = e4
| op(e0,e1) = e3 ),
inference(copy,[status(thm)],[c_3185]) ).
cnf(c_3187,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e0,e1) = e3 ),
inference(resolve,[status(thm)],[c_313,c_3186]) ).
cnf(c_1155,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e0,e1) = e3 ),
inference(resolve,[status(thm)],[c_1132,c_3187]) ).
cnf(c_3188,plain,
( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| e4 = e2
| op(e0,e1) = e2 ),
inference(paramod,[status(thm)],[c_318,c_59]) ).
cnf(c_3189,plain,
( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| e2 = e4
| op(e0,e1) = e2 ),
inference(copy,[status(thm)],[c_3188]) ).
cnf(c_1157,plain,
( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| op(e0,e1) = e2 ),
inference(resolve,[status(thm)],[c_311,c_3189]) ).
cnf(c_3190,plain,
( op(e1,e4) = e2
| op(e1,e3) = e2
| op(e1,e2) = e2
| e4 = e2
| op(e1,e0) = e2 ),
inference(paramod,[status(thm)],[c_318,c_58]) ).
cnf(c_3191,plain,
( op(e1,e4) = e2
| op(e1,e3) = e2
| op(e1,e2) = e2
| e2 = e4
| op(e1,e0) = e2 ),
inference(copy,[status(thm)],[c_3190]) ).
cnf(c_1158,plain,
( op(e1,e4) = e2
| op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e0) = e2 ),
inference(resolve,[status(thm)],[c_311,c_3191]) ).
cnf(c_1173,plain,
( op(e3,e2) = e4
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 ),
inference(resolve,[status(thm)],[c_1135,c_25]) ).
cnf(c_1175,plain,
( op(e0,e4) = e3
| op(e0,e3) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 ),
inference(resolve,[status(thm)],[c_1137,c_50]) ).
cnf(c_1177,plain,
op(e1,e2) = e0,
inference(paramod,[status(thm)],[c_1146,c_1129]) ).
cnf(c_3192,negated_conjecture,
( e2 = e1
| op(e3,e3) = e1
| op(e0,e0) = e1 ),
inference(paramod,[status(thm)],[c_1146,c_322]) ).
cnf(c_3193,negated_conjecture,
( e1 = e2
| op(e3,e3) = e1
| op(e0,e0) = e1 ),
inference(copy,[status(thm)],[c_3192]) ).
cnf(c_1178,negated_conjecture,
( op(e3,e3) = e1
| op(e0,e0) = e1 ),
inference(resolve,[status(thm)],[c_303,c_3193]) ).
cnf(c_3194,negated_conjecture,
( e2 = e0
| op(e3,e3) = e0
| op(e0,e0) = e0 ),
inference(paramod,[status(thm)],[c_1146,c_320]) ).
cnf(c_3195,negated_conjecture,
( e0 = e2
| op(e3,e3) = e0
| op(e0,e0) = e0 ),
inference(copy,[status(thm)],[c_3194]) ).
cnf(c_1179,negated_conjecture,
( op(e3,e3) = e0
| op(e0,e0) = e0 ),
inference(resolve,[status(thm)],[c_297,c_3195]) ).
cnf(c_1181,plain,
op(e4,e2) != e2,
inference(paramod,[status(thm)],[c_1146,c_291]) ).
cnf(c_1182,plain,
op(e4,e1) != e2,
inference(paramod,[status(thm)],[c_1146,c_287]) ).
cnf(c_1184,plain,
op(e3,e4) != e2,
inference(paramod,[status(thm)],[c_1146,c_193]) ).
cnf(c_1186,plain,
op(e1,e4) != e2,
inference(paramod,[status(thm)],[c_1146,c_187]) ).
cnf(c_1187,plain,
op(e0,e4) != e2,
inference(paramod,[status(thm)],[c_1146,c_181]) ).
cnf(c_3196,plain,
( e2 = e1
| op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| op(e0,e4) = e1 ),
inference(paramod,[status(thm)],[c_1146,c_87]) ).
cnf(c_3197,plain,
( e1 = e2
| op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| op(e0,e4) = e1 ),
inference(copy,[status(thm)],[c_3196]) ).
cnf(c_1190,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| op(e0,e4) = e1 ),
inference(resolve,[status(thm)],[c_303,c_3197]) ).
cnf(c_3198,plain,
( e2 = e0
| op(e4,e3) = e0
| op(e4,e2) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 ),
inference(paramod,[status(thm)],[c_1146,c_84]) ).
cnf(c_3199,plain,
( e0 = e2
| op(e4,e3) = e0
| op(e4,e2) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 ),
inference(copy,[status(thm)],[c_3198]) ).
cnf(c_1193,plain,
( op(e4,e3) = e0
| op(e4,e2) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 ),
inference(resolve,[status(thm)],[c_297,c_3199]) ).
cnf(c_3200,plain,
( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e1
| op(e1,e4) = e0 ),
inference(resolve,[status(thm)],[c_1186,c_17]) ).
cnf(c_1194,plain,
( op(e1,e4) = e3
| op(e1,e4) = e1
| op(e1,e4) = e0 ),
inference(resolve,[status(thm)],[c_1147,c_3200]) ).
cnf(c_3201,plain,
( op(e4,e2) = e4
| op(e3,e2) = e4
| e0 = e4
| op(e0,e2) = e4 ),
inference(paramod,[status(thm)],[c_1177,c_1138]) ).
cnf(c_1197,plain,
( op(e4,e2) = e4
| op(e3,e2) = e4
| op(e0,e2) = e4 ),
inference(resolve,[status(thm)],[c_301,c_3201]) ).
cnf(c_1198,plain,
( op(e4,e0) = e4
| op(e3,e0) = e4
| op(e2,e0) = e4
| op(e0,e0) = e4 ),
inference(resolve,[status(thm)],[c_1150,c_53]) ).
cnf(c_1203,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| op(e2,e0) = e4 ),
inference(resolve,[status(thm)],[c_1153,c_1139]) ).
cnf(c_1204,plain,
( op(e0,e4) = e4
| op(e0,e3) = e4
| op(e0,e2) = e4
| op(e0,e0) = e4 ),
inference(resolve,[status(thm)],[c_1154,c_52]) ).
cnf(c_3202,plain,
( op(e1,e4) = e2
| op(e1,e3) = e2
| e0 = e2
| op(e1,e0) = e2 ),
inference(paramod,[status(thm)],[c_1177,c_1158]) ).
cnf(c_3203,plain,
( op(e1,e4) = e2
| op(e1,e3) = e2
| op(e1,e0) = e2 ),
inference(resolve,[status(thm)],[c_297,c_3202]) ).
cnf(c_1207,plain,
( op(e1,e3) = e2
| op(e1,e0) = e2 ),
inference(resolve,[status(thm)],[c_1186,c_3203]) ).
cnf(c_3204,plain,
( op(e4,e2) = e1
| op(e3,e2) = e1
| e0 = e1
| op(e0,e2) = e1 ),
inference(paramod,[status(thm)],[c_1177,c_1142]) ).
cnf(c_1208,plain,
( op(e4,e2) = e1
| op(e3,e2) = e1
| op(e0,e2) = e1 ),
inference(resolve,[status(thm)],[c_295,c_3204]) ).
cnf(c_3205,negated_conjecture,
( e0 != op(e2,e1)
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_1177,c_1108]) ).
cnf(c_1210,negated_conjecture,
( op(e2,e1) != e0
| ~ defn_50 ),
inference(copy,[status(thm)],[c_3205]) ).
cnf(c_3206,negated_conjecture,
( e0 != op(e2,e1)
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_1177,c_1092]) ).
cnf(c_1213,negated_conjecture,
( op(e2,e1) != e0
| ~ defn_90 ),
inference(copy,[status(thm)],[c_3206]) ).
cnf(c_3207,plain,
e0 != op(e1,e4),
inference(paramod,[status(thm)],[c_1177,c_231]) ).
cnf(c_1214,plain,
op(e1,e4) != e0,
inference(copy,[status(thm)],[c_3207]) ).
cnf(c_1216,plain,
op(e1,e0) != e0,
inference(paramod,[status(thm)],[c_1177,c_217]) ).
cnf(c_3208,plain,
e0 != op(e4,e2),
inference(paramod,[status(thm)],[c_1177,c_147]) ).
cnf(c_1217,plain,
op(e4,e2) != e0,
inference(copy,[status(thm)],[c_3208]) ).
cnf(c_3209,plain,
e0 != op(e3,e2),
inference(paramod,[status(thm)],[c_1177,c_145]) ).
cnf(c_1218,plain,
op(e3,e2) != e0,
inference(copy,[status(thm)],[c_3209]) ).
cnf(c_1219,plain,
op(e0,e2) != e0,
inference(paramod,[status(thm)],[c_1177,c_135]) ).
cnf(c_1223,plain,
( op(e3,e1) = e2
| op(e2,e1) = e2
| op(e0,e1) = e2 ),
inference(resolve,[status(thm)],[c_1182,c_1157]) ).
cnf(c_1226,plain,
( op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 ),
inference(resolve,[status(thm)],[c_1184,c_78]) ).
cnf(c_1230,plain,
( op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 ),
inference(resolve,[status(thm)],[c_1187,c_48]) ).
cnf(c_1232,plain,
( op(e1,e4) = e3
| op(e1,e4) = e1 ),
inference(resolve,[status(thm)],[c_1214,c_1194]) ).
cnf(c_1238,plain,
( op(e4,e3) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 ),
inference(resolve,[status(thm)],[c_1217,c_1193]) ).
cnf(c_1239,plain,
( op(e3,e2) = e4
| op(e3,e2) = e2
| op(e3,e2) = e1 ),
inference(resolve,[status(thm)],[c_1218,c_1173]) ).
cnf(c_1240,plain,
( op(e3,e4) = e0
| op(e3,e3) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(resolve,[status(thm)],[c_1218,c_74]) ).
cnf(c_3210,plain,
( op(e1,e0) = e0
| unit = e4
| unit = e3
| unit = e2
| unit = e0 ),
inference(paramod,[status(thm)],[c_43,c_33]) ).
cnf(c_1244,plain,
( unit = e4
| unit = e3
| unit = e2
| unit = e0 ),
inference(resolve,[status(thm)],[c_1216,c_3210]) ).
cnf(c_1487,plain,
( op(e0,e1) != e1
| ~ defn_40
| op(e4,e0) = e1
| op(e3,e0) = e1
| op(e2,e0) = e1
| op(e0,e0) = e1 ),
inference(paramod,[status(thm)],[c_47,c_1112]) ).
cnf(c_1513,plain,
( op(e0,e1) != e1
| ~ defn_00
| op(e4,e0) = e1
| op(e3,e0) = e1
| op(e2,e0) = e1
| op(e0,e0) = e1 ),
inference(paramod,[status(thm)],[c_47,c_1128]) ).
cnf(c_3211,plain,
( e3 != op(e3,e0)
| ~ defn_120
| op(e0,e4) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 ),
inference(paramod,[status(thm)],[c_1175,c_1080]) ).
cnf(c_1765,plain,
( op(e3,e0) != e3
| ~ defn_120
| op(e0,e4) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 ),
inference(copy,[status(thm)],[c_3211]) ).
cnf(c_1769,plain,
( op(e3,e0) != e3
| ~ defn_20
| op(e0,e4) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 ),
inference(paramod,[status(thm)],[c_1175,c_1117]) ).
cnf(c_3212,plain,
( e1 != op(e4,e2)
| ~ defn_110
| op(e3,e4) = e1
| op(e1,e4) = e1
| op(e0,e4) = e1 ),
inference(paramod,[status(thm)],[c_1190,c_1084]) ).
cnf(c_1857,plain,
( op(e4,e2) != e1
| ~ defn_110
| op(e3,e4) = e1
| op(e1,e4) = e1
| op(e0,e4) = e1 ),
inference(copy,[status(thm)],[c_3212]) ).
cnf(c_2032,plain,
( op(e4,e0) != e4
| ~ defn_30
| op(e0,e3) = e4
| op(e0,e2) = e4
| op(e0,e0) = e4 ),
inference(paramod,[status(thm)],[c_1204,c_1113]) ).
cnf(c_2149,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e0) = e0
| ~ defn_50 ),
inference(resolve,[status(thm)],[c_1210,c_1145]) ).
cnf(c_2153,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e0) = e0
| ~ defn_90 ),
inference(resolve,[status(thm)],[c_1213,c_1145]) ).
cnf(c_2278,plain,
( op(e1,e3) != e2
| ~ defn_130
| op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e0) = e2 ),
inference(paramod,[status(thm)],[c_1226,c_1076]) ).
cnf(c_2281,plain,
( op(e1,e3) != e2
| ~ defn_60
| op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e0) = e2 ),
inference(paramod,[status(thm)],[c_1226,c_1104]) ).
cnf(c_3213,plain,
( e2 != op(e2,e0)
| ~ defn_80
| op(e0,e3) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 ),
inference(paramod,[status(thm)],[c_1230,c_1096]) ).
cnf(c_2357,plain,
( op(e2,e0) != e2
| ~ defn_80
| op(e0,e3) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 ),
inference(copy,[status(thm)],[c_3213]) ).
cnf(c_2359,plain,
( op(e2,e0) != e2
| ~ defn_10
| op(e0,e3) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 ),
inference(paramod,[status(thm)],[c_1230,c_1121]) ).
cnf(c_3214,plain,
( e3 != op(e4,e1)
| ~ defn_70
| op(e1,e4) = e1 ),
inference(paramod,[status(thm)],[c_1232,c_1100]) ).
cnf(c_2405,plain,
( op(e4,e1) != e3
| ~ defn_70
| op(e1,e4) = e1 ),
inference(copy,[status(thm)],[c_3214]) ).
cnf(c_3215,plain,
( e0 = e4
| op(e3,e0) = e4
| op(e2,e0) = e4
| op(e0,e0) = e4
| op(e4,e3) = e0
| op(e4,e1) = e0 ),
inference(paramod,[status(thm)],[c_1238,c_1198]) ).
cnf(c_2525,plain,
( op(e3,e0) = e4
| op(e2,e0) = e4
| op(e0,e0) = e4
| op(e4,e3) = e0
| op(e4,e1) = e0 ),
inference(resolve,[status(thm)],[c_301,c_3215]) ).
cnf(c_2543,plain,
( op(e2,e3) != e4
| ~ defn_100
| op(e3,e2) = e2
| op(e3,e2) = e1 ),
inference(paramod,[status(thm)],[c_1239,c_1088]) ).
cnf(c_3216,plain,
( e0 = e1
| op(e0,e0) = e1
| op(e3,e4) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(paramod,[status(thm)],[c_1240,c_1178]) ).
cnf(c_2554,plain,
( op(e0,e0) = e1
| op(e3,e4) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(resolve,[status(thm)],[c_295,c_3216]) ).
cnf(c_3217,plain,
( op(e0,e2) = e0
| unit = e4
| unit = e3
| unit = e0 ),
inference(paramod,[status(thm)],[c_1244,c_34]) ).
cnf(c_2622,plain,
( unit = e4
| unit = e3
| unit = e0 ),
inference(resolve,[status(thm)],[c_1219,c_3217]) ).
cnf(c_3218,plain,
( op(e4,e2) = e2
| unit = e3
| unit = e0 ),
inference(paramod,[status(thm)],[c_2622,c_37]) ).
cnf(c_2656,plain,
( unit = e3
| unit = e0 ),
inference(resolve,[status(thm)],[c_1181,c_3218]) ).
cnf(c_2666,plain,
( op(e0,e0) = e0
| unit = e3 ),
inference(paramod,[status(thm)],[c_2656,c_33]) ).
cnf(c_2667,plain,
( op(e3,e0) = e0
| unit = e0 ),
inference(paramod,[status(thm)],[c_2656,c_33]) ).
cnf(c_2669,plain,
( op(e0,e1) = e1
| unit = e3 ),
inference(paramod,[status(thm)],[c_2656,c_35]) ).
cnf(c_2671,plain,
( op(e1,e0) = e1
| unit = e3 ),
inference(paramod,[status(thm)],[c_2656,c_36]) ).
cnf(c_2673,plain,
( op(e0,e2) = e2
| unit = e3 ),
inference(paramod,[status(thm)],[c_2656,c_37]) ).
cnf(c_2675,plain,
( op(e2,e0) = e2
| unit = e3 ),
inference(paramod,[status(thm)],[c_2656,c_38]) ).
cnf(c_2677,plain,
( op(e0,e3) = e3
| unit = e3 ),
inference(paramod,[status(thm)],[c_2656,c_39]) ).
cnf(c_2678,plain,
( op(e3,e3) = e3
| unit = e0 ),
inference(paramod,[status(thm)],[c_2656,c_39]) ).
cnf(c_2679,plain,
( op(e3,e0) = e3
| unit = e3 ),
inference(paramod,[status(thm)],[c_2656,c_40]) ).
cnf(c_2680,plain,
( op(e0,e4) = e4
| unit = e3 ),
inference(paramod,[status(thm)],[c_2656,c_41]) ).
cnf(c_2682,plain,
( op(e4,e0) = e4
| unit = e3 ),
inference(paramod,[status(thm)],[c_2656,c_42]) ).
cnf(c_3219,plain,
( op(e3,e3) = e1
| e0 = e1
| unit = e3 ),
inference(paramod,[status(thm)],[c_2666,c_1178]) ).
cnf(c_2699,plain,
( op(e3,e3) = e1
| unit = e3 ),
inference(resolve,[status(thm)],[c_295,c_3219]) ).
cnf(c_2725,plain,
( op(e0,e0) != e0
| unit = e0 ),
inference(paramod,[status(thm)],[c_2667,c_99]) ).
cnf(c_3220,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| e1 = e3
| unit = e3 ),
inference(paramod,[status(thm)],[c_2669,c_1155]) ).
cnf(c_2771,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| unit = e3 ),
inference(resolve,[status(thm)],[c_305,c_3220]) ).
cnf(c_3221,plain,
( op(e3,e1) = e2
| op(e2,e1) = e2
| e1 = e2
| unit = e3 ),
inference(paramod,[status(thm)],[c_2669,c_1223]) ).
cnf(c_2773,plain,
( op(e3,e1) = e2
| op(e2,e1) = e2
| unit = e3 ),
inference(resolve,[status(thm)],[c_303,c_3221]) ).
cnf(c_3222,plain,
( e1 != op(e1,e4)
| unit = e3 ),
inference(paramod,[status(thm)],[c_2671,c_221]) ).
cnf(c_2803,plain,
( op(e1,e4) != e1
| unit = e3 ),
inference(copy,[status(thm)],[c_3222]) ).
cnf(c_3223,plain,
( op(e1,e3) = e2
| e1 = e2
| unit = e3 ),
inference(paramod,[status(thm)],[c_2671,c_1207]) ).
cnf(c_2807,plain,
( op(e1,e3) = e2
| unit = e3 ),
inference(resolve,[status(thm)],[c_303,c_3223]) ).
cnf(c_3224,plain,
( op(e4,e2) = e4
| op(e3,e2) = e4
| e2 = e4
| unit = e3 ),
inference(paramod,[status(thm)],[c_2673,c_1197]) ).
cnf(c_2833,plain,
( op(e4,e2) = e4
| op(e3,e2) = e4
| unit = e3 ),
inference(resolve,[status(thm)],[c_311,c_3224]) ).
cnf(c_3225,plain,
( op(e4,e2) = e1
| op(e3,e2) = e1
| e2 = e1
| unit = e3 ),
inference(paramod,[status(thm)],[c_2673,c_1208]) ).
cnf(c_3226,plain,
( op(e4,e2) = e1
| op(e3,e2) = e1
| e1 = e2
| unit = e3 ),
inference(copy,[status(thm)],[c_3225]) ).
cnf(c_2834,plain,
( op(e4,e2) = e1
| op(e3,e2) = e1
| unit = e3 ),
inference(resolve,[status(thm)],[c_303,c_3226]) ).
cnf(c_3227,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e1) = e0
| e2 = e0
| unit = e3 ),
inference(paramod,[status(thm)],[c_2675,c_1145]) ).
cnf(c_3228,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e1) = e0
| e0 = e2
| unit = e3 ),
inference(copy,[status(thm)],[c_3227]) ).
cnf(c_2858,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e1) = e0
| unit = e3 ),
inference(resolve,[status(thm)],[c_297,c_3228]) ).
cnf(c_3229,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| e2 = e4
| unit = e3 ),
inference(paramod,[status(thm)],[c_2675,c_1203]) ).
cnf(c_2859,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| unit = e3 ),
inference(resolve,[status(thm)],[c_311,c_3229]) ).
cnf(c_3230,plain,
( e3 = e0
| op(e0,e0) = e0
| unit = e0 ),
inference(paramod,[status(thm)],[c_2678,c_1179]) ).
cnf(c_3231,plain,
( e0 = e3
| op(e0,e0) = e0
| unit = e0 ),
inference(copy,[status(thm)],[c_3230]) ).
cnf(c_2895,plain,
( op(e0,e0) = e0
| unit = e0 ),
inference(resolve,[status(thm)],[c_299,c_3231]) ).
cnf(c_3232,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| e4 = e1
| unit = e3 ),
inference(paramod,[status(thm)],[c_2680,c_1190]) ).
cnf(c_3233,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| e1 = e4
| unit = e3 ),
inference(copy,[status(thm)],[c_3232]) ).
cnf(c_2917,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| unit = e3 ),
inference(resolve,[status(thm)],[c_307,c_3233]) ).
cnf(c_2955,plain,
( op(e3,e2) != e1
| unit = e3 ),
inference(paramod,[status(thm)],[c_2699,c_269]) ).
cnf(c_3234,plain,
( e1 != op(e3,e4)
| unit = e3 ),
inference(paramod,[status(thm)],[c_2699,c_273]) ).
cnf(c_2956,plain,
( op(e3,e4) != e1
| unit = e3 ),
inference(copy,[status(thm)],[c_3234]) ).
cnf(c_2981,plain,
( op(e1,e4) = e3
| unit = e3 ),
inference(resolve,[status(thm)],[c_2803,c_1232]) ).
cnf(c_3235,plain,
( unit = e0
| unit = e0 ),
inference(resolve,[status(thm)],[c_2895,c_2725]) ).
cnf(c_3043,plain,
unit = e0,
inference(copy,[status(thm)],[c_3235]) ).
cnf(c_3236,plain,
( op(e0,e0) = e0
| op(e0,e0) = e0 ),
inference(paramod,[status(thm)],[c_2895,c_33]) ).
cnf(c_3044,plain,
op(e0,e0) = e0,
inference(copy,[status(thm)],[c_3236]) ).
cnf(c_3237,plain,
( op(e1,e4) = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2981]) ).
cnf(c_3056,plain,
op(e1,e4) = e3,
inference(resolve,[status(thm)],[c_299,c_3237]) ).
cnf(c_3238,plain,
( op(e3,e4) != e1
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2956]) ).
cnf(c_3067,plain,
op(e3,e4) != e1,
inference(resolve,[status(thm)],[c_299,c_3238]) ).
cnf(c_3239,plain,
( op(e3,e2) != e1
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2955]) ).
cnf(c_3068,plain,
op(e3,e2) != e1,
inference(resolve,[status(thm)],[c_299,c_3239]) ).
cnf(c_3240,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2917]) ).
cnf(c_3241,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1
| e3 = e1
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3056,c_3240]) ).
cnf(c_3242,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1
| e1 = e3
| e0 = e3 ),
inference(copy,[status(thm)],[c_3241]) ).
cnf(c_3243,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1
| e1 = e3 ),
inference(resolve,[status(thm)],[c_299,c_3242]) ).
cnf(c_3244,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1 ),
inference(resolve,[status(thm)],[c_305,c_3243]) ).
cnf(c_3080,plain,
op(e2,e4) = e1,
inference(resolve,[status(thm)],[c_3067,c_3244]) ).
cnf(c_3245,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2859]) ).
cnf(c_3246,plain,
( e1 = e4
| op(e2,e3) = e4
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3080,c_3245]) ).
cnf(c_3247,plain,
( e1 = e4
| op(e2,e3) = e4 ),
inference(resolve,[status(thm)],[c_299,c_3246]) ).
cnf(c_3104,plain,
op(e2,e3) = e4,
inference(resolve,[status(thm)],[c_307,c_3247]) ).
cnf(c_3248,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e1) = e0
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2858]) ).
cnf(c_3249,plain,
( op(e2,e4) = e0
| e4 = e0
| op(e2,e1) = e0
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3104,c_3248]) ).
cnf(c_3250,plain,
( e1 = e0
| e4 = e0
| op(e2,e1) = e0
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3080,c_3249]) ).
cnf(c_3251,plain,
( e1 = e0
| e0 = e4
| op(e2,e1) = e0
| e0 = e3 ),
inference(copy,[status(thm)],[c_3250]) ).
cnf(c_3252,plain,
( e0 = e1
| e0 = e4
| op(e2,e1) = e0
| e0 = e3 ),
inference(copy,[status(thm)],[c_3251]) ).
cnf(c_3253,plain,
( e0 = e1
| e0 = e4
| op(e2,e1) = e0 ),
inference(resolve,[status(thm)],[c_299,c_3252]) ).
cnf(c_3254,plain,
( e0 = e1
| op(e2,e1) = e0 ),
inference(resolve,[status(thm)],[c_301,c_3253]) ).
cnf(c_3105,plain,
op(e2,e1) = e0,
inference(resolve,[status(thm)],[c_295,c_3254]) ).
cnf(c_3255,plain,
( op(e4,e2) = e1
| op(e3,e2) = e1
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2834]) ).
cnf(c_3256,plain,
( op(e4,e2) = e1
| op(e3,e2) = e1 ),
inference(resolve,[status(thm)],[c_299,c_3255]) ).
cnf(c_3110,plain,
op(e4,e2) = e1,
inference(resolve,[status(thm)],[c_3068,c_3256]) ).
cnf(c_3257,plain,
( op(e4,e2) = e4
| op(e3,e2) = e4
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2833]) ).
cnf(c_3258,plain,
( e1 = e4
| op(e3,e2) = e4
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3110,c_3257]) ).
cnf(c_3259,plain,
( e1 = e4
| op(e3,e2) = e4 ),
inference(resolve,[status(thm)],[c_299,c_3258]) ).
cnf(c_3111,plain,
op(e3,e2) = e4,
inference(resolve,[status(thm)],[c_307,c_3259]) ).
cnf(c_3260,plain,
( op(e1,e3) = e2
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2807]) ).
cnf(c_3116,plain,
op(e1,e3) = e2,
inference(resolve,[status(thm)],[c_299,c_3260]) ).
cnf(c_3261,plain,
( op(e3,e1) = e2
| op(e2,e1) = e2
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2773]) ).
cnf(c_3262,plain,
( op(e3,e1) = e2
| e0 = e2
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3105,c_3261]) ).
cnf(c_3263,plain,
( op(e3,e1) = e2
| e0 = e2 ),
inference(resolve,[status(thm)],[c_299,c_3262]) ).
cnf(c_3122,plain,
op(e3,e1) = e2,
inference(resolve,[status(thm)],[c_297,c_3263]) ).
cnf(c_3264,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2771]) ).
cnf(c_3265,plain,
( op(e4,e1) = e3
| e2 = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3122,c_3264]) ).
cnf(c_3266,plain,
( op(e4,e1) = e3
| e2 = e3 ),
inference(resolve,[status(thm)],[c_299,c_3265]) ).
cnf(c_3123,plain,
op(e4,e1) = e3,
inference(resolve,[status(thm)],[c_309,c_3266]) ).
cnf(c_3267,plain,
( op(e3,e3) = e1
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2699]) ).
cnf(c_3129,plain,
op(e3,e3) = e1,
inference(resolve,[status(thm)],[c_299,c_3267]) ).
cnf(c_3268,plain,
( op(e4,e0) = e4
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2682]) ).
cnf(c_3136,plain,
op(e4,e0) = e4,
inference(resolve,[status(thm)],[c_299,c_3268]) ).
cnf(c_3269,plain,
( op(e0,e4) = e4
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2680]) ).
cnf(c_3137,plain,
op(e0,e4) = e4,
inference(resolve,[status(thm)],[c_299,c_3269]) ).
cnf(c_3270,plain,
( op(e3,e0) = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2679]) ).
cnf(c_3138,plain,
op(e3,e0) = e3,
inference(resolve,[status(thm)],[c_299,c_3270]) ).
cnf(c_3271,plain,
( op(e0,e3) = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2677]) ).
cnf(c_3139,plain,
op(e0,e3) = e3,
inference(resolve,[status(thm)],[c_299,c_3271]) ).
cnf(c_3272,plain,
( op(e2,e0) = e2
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2675]) ).
cnf(c_3140,plain,
op(e2,e0) = e2,
inference(resolve,[status(thm)],[c_299,c_3272]) ).
cnf(c_3273,plain,
( op(e0,e2) = e2
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2673]) ).
cnf(c_3141,plain,
op(e0,e2) = e2,
inference(resolve,[status(thm)],[c_299,c_3273]) ).
cnf(c_3274,plain,
( op(e0,e1) = e1
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3043,c_2669]) ).
cnf(c_3143,plain,
op(e0,e1) = e1,
inference(resolve,[status(thm)],[c_299,c_3274]) ).
cnf(c_3275,plain,
( op(e0,e0) = e1
| op(e3,e4) = e0
| op(e3,e1) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_3138,c_2554]) ).
cnf(c_3276,plain,
( op(e0,e0) = e1
| op(e3,e4) = e0
| e2 = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_3122,c_3275]) ).
cnf(c_3277,plain,
( e0 = e1
| op(e3,e4) = e0
| e2 = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_3044,c_3276]) ).
cnf(c_3278,plain,
( e0 = e1
| op(e3,e4) = e0
| e2 = e0
| e0 = e3 ),
inference(copy,[status(thm)],[c_3277]) ).
cnf(c_3279,plain,
( e0 = e1
| op(e3,e4) = e0
| e0 = e2
| e0 = e3 ),
inference(copy,[status(thm)],[c_3278]) ).
cnf(c_3280,plain,
( e0 = e1
| op(e3,e4) = e0
| e0 = e2 ),
inference(resolve,[status(thm)],[c_299,c_3279]) ).
cnf(c_3281,plain,
( e0 = e1
| op(e3,e4) = e0 ),
inference(resolve,[status(thm)],[c_297,c_3280]) ).
cnf(c_3144,plain,
op(e3,e4) = e0,
inference(resolve,[status(thm)],[c_295,c_3281]) ).
cnf(c_3282,plain,
( op(e3,e0) = e4
| op(e2,e0) = e4
| op(e0,e0) = e4
| op(e4,e3) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_3123,c_2525]) ).
cnf(c_3283,plain,
( op(e3,e0) = e4
| op(e2,e0) = e4
| e0 = e4
| op(e4,e3) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_3044,c_3282]) ).
cnf(c_3284,plain,
( op(e3,e0) = e4
| e2 = e4
| e0 = e4
| op(e4,e3) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_3140,c_3283]) ).
cnf(c_3285,plain,
( e3 = e4
| e2 = e4
| e0 = e4
| op(e4,e3) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_3138,c_3284]) ).
cnf(c_3286,plain,
( e3 = e4
| e2 = e4
| e0 = e4
| op(e4,e3) = e0
| e0 = e3 ),
inference(copy,[status(thm)],[c_3285]) ).
cnf(c_3287,plain,
( e3 = e4
| e2 = e4
| e0 = e4
| op(e4,e3) = e0 ),
inference(resolve,[status(thm)],[c_299,c_3286]) ).
cnf(c_3288,plain,
( e3 = e4
| e2 = e4
| op(e4,e3) = e0 ),
inference(resolve,[status(thm)],[c_301,c_3287]) ).
cnf(c_3289,plain,
( e3 = e4
| op(e4,e3) = e0 ),
inference(resolve,[status(thm)],[c_311,c_3288]) ).
cnf(c_3145,plain,
op(e4,e3) = e0,
inference(resolve,[status(thm)],[c_313,c_3289]) ).
cnf(c_3290,plain,
( op(e2,e0) != e2
| ~ defn_10
| op(e0,e3) = e2
| op(e0,e1) = e2
| e0 = e2 ),
inference(paramod,[status(thm)],[c_3044,c_2359]) ).
cnf(c_3291,plain,
( op(e2,e0) != e2
| ~ defn_10
| op(e0,e3) = e2
| e1 = e2
| e0 = e2 ),
inference(paramod,[status(thm)],[c_3143,c_3290]) ).
cnf(c_3292,plain,
( op(e2,e0) != e2
| ~ defn_10
| e3 = e2
| e1 = e2
| e0 = e2 ),
inference(paramod,[status(thm)],[c_3139,c_3291]) ).
cnf(c_3293,plain,
( e2 != e2
| ~ defn_10
| e3 = e2
| e1 = e2
| e0 = e2 ),
inference(paramod,[status(thm)],[c_3140,c_3292]) ).
cnf(c_3294,plain,
( e2 != e2
| ~ defn_10
| e2 = e3
| e1 = e2
| e0 = e2 ),
inference(copy,[status(thm)],[c_3293]) ).
cnf(c_3295,plain,
( ~ defn_10
| e2 = e3
| e1 = e2
| e0 = e2 ),
inference(copy,[status(thm)],[c_3294]) ).
cnf(c_3296,plain,
( ~ defn_10
| e2 = e3
| e1 = e2 ),
inference(resolve,[status(thm)],[c_297,c_3295]) ).
cnf(c_3297,plain,
( ~ defn_10
| e2 = e3 ),
inference(resolve,[status(thm)],[c_303,c_3296]) ).
cnf(c_3146,plain,
~ defn_10,
inference(resolve,[status(thm)],[c_309,c_3297]) ).
cnf(c_3298,plain,
( op(e2,e0) != e2
| ~ defn_80
| op(e0,e3) = e2
| op(e0,e1) = e2
| e0 = e2 ),
inference(paramod,[status(thm)],[c_3044,c_2357]) ).
cnf(c_3299,plain,
( op(e2,e0) != e2
| ~ defn_80
| op(e0,e3) = e2
| e1 = e2
| e0 = e2 ),
inference(paramod,[status(thm)],[c_3143,c_3298]) ).
cnf(c_3300,plain,
( op(e2,e0) != e2
| ~ defn_80
| e3 = e2
| e1 = e2
| e0 = e2 ),
inference(paramod,[status(thm)],[c_3139,c_3299]) ).
cnf(c_3301,plain,
( e2 != e2
| ~ defn_80
| e3 = e2
| e1 = e2
| e0 = e2 ),
inference(paramod,[status(thm)],[c_3140,c_3300]) ).
cnf(c_3302,plain,
( e2 != e2
| ~ defn_80
| e2 = e3
| e1 = e2
| e0 = e2 ),
inference(copy,[status(thm)],[c_3301]) ).
cnf(c_3303,plain,
( ~ defn_80
| e2 = e3
| e1 = e2
| e0 = e2 ),
inference(copy,[status(thm)],[c_3302]) ).
cnf(c_3304,plain,
( ~ defn_80
| e2 = e3
| e1 = e2 ),
inference(resolve,[status(thm)],[c_297,c_3303]) ).
cnf(c_3305,plain,
( ~ defn_80
| e2 = e3 ),
inference(resolve,[status(thm)],[c_303,c_3304]) ).
cnf(c_3147,plain,
~ defn_80,
inference(resolve,[status(thm)],[c_309,c_3305]) ).
cnf(c_3306,plain,
( op(e4,e0) != e4
| ~ defn_30
| op(e0,e3) = e4
| op(e0,e2) = e4
| e0 = e4 ),
inference(paramod,[status(thm)],[c_3044,c_2032]) ).
cnf(c_3307,plain,
( op(e4,e0) != e4
| ~ defn_30
| op(e0,e3) = e4
| e2 = e4
| e0 = e4 ),
inference(paramod,[status(thm)],[c_3141,c_3306]) ).
cnf(c_3308,plain,
( op(e4,e0) != e4
| ~ defn_30
| e3 = e4
| e2 = e4
| e0 = e4 ),
inference(paramod,[status(thm)],[c_3139,c_3307]) ).
cnf(c_3309,plain,
( e4 != e4
| ~ defn_30
| e3 = e4
| e2 = e4
| e0 = e4 ),
inference(paramod,[status(thm)],[c_3136,c_3308]) ).
cnf(c_3310,plain,
( ~ defn_30
| e3 = e4
| e2 = e4
| e0 = e4 ),
inference(copy,[status(thm)],[c_3309]) ).
cnf(c_3311,plain,
( ~ defn_30
| e3 = e4
| e2 = e4 ),
inference(resolve,[status(thm)],[c_301,c_3310]) ).
cnf(c_3312,plain,
( ~ defn_30
| e3 = e4 ),
inference(resolve,[status(thm)],[c_311,c_3311]) ).
cnf(c_3148,plain,
~ defn_30,
inference(resolve,[status(thm)],[c_313,c_3312]) ).
cnf(c_3313,plain,
( op(e3,e0) != e3
| ~ defn_20
| op(e0,e4) = e3
| op(e0,e1) = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3044,c_1769]) ).
cnf(c_3314,plain,
( op(e3,e0) != e3
| ~ defn_20
| op(e0,e4) = e3
| e1 = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3143,c_3313]) ).
cnf(c_3315,plain,
( op(e3,e0) != e3
| ~ defn_20
| e4 = e3
| e1 = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3137,c_3314]) ).
cnf(c_3316,plain,
( e3 != e3
| ~ defn_20
| e4 = e3
| e1 = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3138,c_3315]) ).
cnf(c_3317,plain,
( e3 != e3
| ~ defn_20
| e3 = e4
| e1 = e3
| e0 = e3 ),
inference(copy,[status(thm)],[c_3316]) ).
cnf(c_3318,plain,
( ~ defn_20
| e3 = e4
| e1 = e3
| e0 = e3 ),
inference(copy,[status(thm)],[c_3317]) ).
cnf(c_3319,plain,
( ~ defn_20
| e3 = e4
| e1 = e3 ),
inference(resolve,[status(thm)],[c_299,c_3318]) ).
cnf(c_3320,plain,
( ~ defn_20
| e3 = e4 ),
inference(resolve,[status(thm)],[c_305,c_3319]) ).
cnf(c_3149,plain,
~ defn_20,
inference(resolve,[status(thm)],[c_313,c_3320]) ).
cnf(c_3321,plain,
( op(e3,e0) != e3
| ~ defn_120
| op(e0,e4) = e3
| op(e0,e1) = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3044,c_1765]) ).
cnf(c_3322,plain,
( op(e3,e0) != e3
| ~ defn_120
| op(e0,e4) = e3
| e1 = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3143,c_3321]) ).
cnf(c_3323,plain,
( op(e3,e0) != e3
| ~ defn_120
| e4 = e3
| e1 = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3137,c_3322]) ).
cnf(c_3324,plain,
( e3 != e3
| ~ defn_120
| e4 = e3
| e1 = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_3138,c_3323]) ).
cnf(c_3325,plain,
( e3 != e3
| ~ defn_120
| e3 = e4
| e1 = e3
| e0 = e3 ),
inference(copy,[status(thm)],[c_3324]) ).
cnf(c_3326,plain,
( ~ defn_120
| e3 = e4
| e1 = e3
| e0 = e3 ),
inference(copy,[status(thm)],[c_3325]) ).
cnf(c_3327,plain,
( ~ defn_120
| e3 = e4
| e1 = e3 ),
inference(resolve,[status(thm)],[c_299,c_3326]) ).
cnf(c_3328,plain,
( ~ defn_120
| e3 = e4 ),
inference(resolve,[status(thm)],[c_305,c_3327]) ).
cnf(c_3150,plain,
~ defn_120,
inference(resolve,[status(thm)],[c_313,c_3328]) ).
cnf(c_3329,plain,
( op(e0,e1) != e1
| ~ defn_00
| op(e4,e0) = e1
| op(e3,e0) = e1
| op(e2,e0) = e1
| e0 = e1 ),
inference(paramod,[status(thm)],[c_3044,c_1513]) ).
cnf(c_3330,plain,
( op(e0,e1) != e1
| ~ defn_00
| op(e4,e0) = e1
| op(e3,e0) = e1
| e2 = e1
| e0 = e1 ),
inference(paramod,[status(thm)],[c_3140,c_3329]) ).
cnf(c_3331,plain,
( op(e0,e1) != e1
| ~ defn_00
| op(e4,e0) = e1
| e3 = e1
| e2 = e1
| e0 = e1 ),
inference(paramod,[status(thm)],[c_3138,c_3330]) ).
cnf(c_3332,plain,
( op(e0,e1) != e1
| ~ defn_00
| e4 = e1
| e3 = e1
| e2 = e1
| e0 = e1 ),
inference(paramod,[status(thm)],[c_3136,c_3331]) ).
cnf(c_3333,plain,
( e1 != e1
| ~ defn_00
| e4 = e1
| e3 = e1
| e2 = e1
| e0 = e1 ),
inference(paramod,[status(thm)],[c_3143,c_3332]) ).
cnf(c_3334,plain,
( e1 != e1
| ~ defn_00
| e4 = e1
| e3 = e1
| e1 = e2
| e0 = e1 ),
inference(copy,[status(thm)],[c_3333]) ).
cnf(c_3335,plain,
( e1 != e1
| ~ defn_00
| e4 = e1
| e1 = e3
| e1 = e2
| e0 = e1 ),
inference(copy,[status(thm)],[c_3334]) ).
cnf(c_3336,plain,
( e1 != e1
| ~ defn_00
| e1 = e4
| e1 = e3
| e1 = e2
| e0 = e1 ),
inference(copy,[status(thm)],[c_3335]) ).
cnf(c_3337,plain,
( ~ defn_00
| e1 = e4
| e1 = e3
| e1 = e2
| e0 = e1 ),
inference(copy,[status(thm)],[c_3336]) ).
cnf(c_3338,plain,
( ~ defn_00
| e1 = e4
| e1 = e3
| e1 = e2 ),
inference(resolve,[status(thm)],[c_295,c_3337]) ).
cnf(c_3339,plain,
( ~ defn_00
| e1 = e4
| e1 = e3 ),
inference(resolve,[status(thm)],[c_303,c_3338]) ).
cnf(c_3340,plain,
( ~ defn_00
| e1 = e4 ),
inference(resolve,[status(thm)],[c_305,c_3339]) ).
cnf(c_3151,plain,
~ defn_00,
inference(resolve,[status(thm)],[c_307,c_3340]) ).
cnf(c_3341,plain,
( op(e0,e1) != e1
| ~ defn_40
| op(e4,e0) = e1
| op(e3,e0) = e1
| op(e2,e0) = e1
| e0 = e1 ),
inference(paramod,[status(thm)],[c_3044,c_1487]) ).
cnf(c_3342,plain,
( op(e0,e1) != e1
| ~ defn_40
| op(e4,e0) = e1
| op(e3,e0) = e1
| e2 = e1
| e0 = e1 ),
inference(paramod,[status(thm)],[c_3140,c_3341]) ).
cnf(c_3343,plain,
( op(e0,e1) != e1
| ~ defn_40
| op(e4,e0) = e1
| e3 = e1
| e2 = e1
| e0 = e1 ),
inference(paramod,[status(thm)],[c_3138,c_3342]) ).
cnf(c_3344,plain,
( op(e0,e1) != e1
| ~ defn_40
| e4 = e1
| e3 = e1
| e2 = e1
| e0 = e1 ),
inference(paramod,[status(thm)],[c_3136,c_3343]) ).
cnf(c_3345,plain,
( e1 != e1
| ~ defn_40
| e4 = e1
| e3 = e1
| e2 = e1
| e0 = e1 ),
inference(paramod,[status(thm)],[c_3143,c_3344]) ).
cnf(c_3346,plain,
( e1 != e1
| ~ defn_40
| e4 = e1
| e3 = e1
| e1 = e2
| e0 = e1 ),
inference(copy,[status(thm)],[c_3345]) ).
cnf(c_3347,plain,
( e1 != e1
| ~ defn_40
| e4 = e1
| e1 = e3
| e1 = e2
| e0 = e1 ),
inference(copy,[status(thm)],[c_3346]) ).
cnf(c_3348,plain,
( e1 != e1
| ~ defn_40
| e1 = e4
| e1 = e3
| e1 = e2
| e0 = e1 ),
inference(copy,[status(thm)],[c_3347]) ).
cnf(c_3349,plain,
( ~ defn_40
| e1 = e4
| e1 = e3
| e1 = e2
| e0 = e1 ),
inference(copy,[status(thm)],[c_3348]) ).
cnf(c_3350,plain,
( ~ defn_40
| e1 = e4
| e1 = e3
| e1 = e2 ),
inference(resolve,[status(thm)],[c_295,c_3349]) ).
cnf(c_3351,plain,
( ~ defn_40
| e1 = e4
| e1 = e3 ),
inference(resolve,[status(thm)],[c_303,c_3350]) ).
cnf(c_3352,plain,
( ~ defn_40
| e1 = e4 ),
inference(resolve,[status(thm)],[c_305,c_3351]) ).
cnf(c_3152,plain,
~ defn_40,
inference(resolve,[status(thm)],[c_307,c_3352]) ).
cnf(c_3353,plain,
( op(e1,e3) != e2
| ~ defn_60
| op(e3,e3) = e2
| op(e3,e2) = e2
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3138,c_2281]) ).
cnf(c_3354,plain,
( op(e1,e3) != e2
| ~ defn_60
| op(e3,e3) = e2
| e4 = e2
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3111,c_3353]) ).
cnf(c_3355,plain,
( op(e1,e3) != e2
| ~ defn_60
| e1 = e2
| e4 = e2
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3129,c_3354]) ).
cnf(c_3356,plain,
( e2 != e2
| ~ defn_60
| e1 = e2
| e4 = e2
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3116,c_3355]) ).
cnf(c_3357,plain,
( e2 != e2
| ~ defn_60
| e1 = e2
| e4 = e2
| e2 = e3 ),
inference(copy,[status(thm)],[c_3356]) ).
cnf(c_3358,plain,
( e2 != e2
| ~ defn_60
| e1 = e2
| e2 = e4
| e2 = e3 ),
inference(copy,[status(thm)],[c_3357]) ).
cnf(c_3359,plain,
( ~ defn_60
| e1 = e2
| e2 = e4
| e2 = e3 ),
inference(copy,[status(thm)],[c_3358]) ).
cnf(c_3360,plain,
( ~ defn_60
| e1 = e2
| e2 = e4 ),
inference(resolve,[status(thm)],[c_309,c_3359]) ).
cnf(c_3361,plain,
( ~ defn_60
| e1 = e2 ),
inference(resolve,[status(thm)],[c_311,c_3360]) ).
cnf(c_3153,plain,
~ defn_60,
inference(resolve,[status(thm)],[c_303,c_3361]) ).
cnf(c_3362,plain,
( op(e1,e3) != e2
| ~ defn_130
| op(e3,e3) = e2
| op(e3,e2) = e2
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3138,c_2278]) ).
cnf(c_3363,plain,
( op(e1,e3) != e2
| ~ defn_130
| op(e3,e3) = e2
| e4 = e2
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3111,c_3362]) ).
cnf(c_3364,plain,
( op(e1,e3) != e2
| ~ defn_130
| e1 = e2
| e4 = e2
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3129,c_3363]) ).
cnf(c_3365,plain,
( e2 != e2
| ~ defn_130
| e1 = e2
| e4 = e2
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3116,c_3364]) ).
cnf(c_3366,plain,
( e2 != e2
| ~ defn_130
| e1 = e2
| e4 = e2
| e2 = e3 ),
inference(copy,[status(thm)],[c_3365]) ).
cnf(c_3367,plain,
( e2 != e2
| ~ defn_130
| e1 = e2
| e2 = e4
| e2 = e3 ),
inference(copy,[status(thm)],[c_3366]) ).
cnf(c_3368,plain,
( ~ defn_130
| e1 = e2
| e2 = e4
| e2 = e3 ),
inference(copy,[status(thm)],[c_3367]) ).
cnf(c_3369,plain,
( ~ defn_130
| e1 = e2
| e2 = e4 ),
inference(resolve,[status(thm)],[c_309,c_3368]) ).
cnf(c_3370,plain,
( ~ defn_130
| e1 = e2 ),
inference(resolve,[status(thm)],[c_311,c_3369]) ).
cnf(c_3154,plain,
~ defn_130,
inference(resolve,[status(thm)],[c_303,c_3370]) ).
cnf(c_3371,plain,
( op(e4,e1) != e3
| ~ defn_70
| e3 = e1 ),
inference(paramod,[status(thm)],[c_3056,c_2405]) ).
cnf(c_3372,plain,
( e3 != e3
| ~ defn_70
| e3 = e1 ),
inference(paramod,[status(thm)],[c_3123,c_3371]) ).
cnf(c_3373,plain,
( e3 != e3
| ~ defn_70
| e1 = e3 ),
inference(copy,[status(thm)],[c_3372]) ).
cnf(c_3374,plain,
( ~ defn_70
| e1 = e3 ),
inference(copy,[status(thm)],[c_3373]) ).
cnf(c_3155,plain,
~ defn_70,
inference(resolve,[status(thm)],[c_305,c_3374]) ).
cnf(c_3375,plain,
( op(e4,e2) != e1
| ~ defn_110
| op(e3,e4) = e1
| op(e1,e4) = e1
| e4 = e1 ),
inference(paramod,[status(thm)],[c_3137,c_1857]) ).
cnf(c_3376,plain,
( op(e4,e2) != e1
| ~ defn_110
| op(e3,e4) = e1
| e3 = e1
| e4 = e1 ),
inference(paramod,[status(thm)],[c_3056,c_3375]) ).
cnf(c_3377,plain,
( op(e4,e2) != e1
| ~ defn_110
| e0 = e1
| e3 = e1
| e4 = e1 ),
inference(paramod,[status(thm)],[c_3144,c_3376]) ).
cnf(c_3378,plain,
( e1 != e1
| ~ defn_110
| e0 = e1
| e3 = e1
| e4 = e1 ),
inference(paramod,[status(thm)],[c_3110,c_3377]) ).
cnf(c_3379,plain,
( e1 != e1
| ~ defn_110
| e0 = e1
| e3 = e1
| e1 = e4 ),
inference(copy,[status(thm)],[c_3378]) ).
cnf(c_3380,plain,
( e1 != e1
| ~ defn_110
| e0 = e1
| e1 = e3
| e1 = e4 ),
inference(copy,[status(thm)],[c_3379]) ).
cnf(c_3381,plain,
( ~ defn_110
| e0 = e1
| e1 = e3
| e1 = e4 ),
inference(copy,[status(thm)],[c_3380]) ).
cnf(c_3382,plain,
( ~ defn_110
| e0 = e1
| e1 = e3 ),
inference(resolve,[status(thm)],[c_307,c_3381]) ).
cnf(c_3383,plain,
( ~ defn_110
| e0 = e1 ),
inference(resolve,[status(thm)],[c_305,c_3382]) ).
cnf(c_3156,plain,
~ defn_110,
inference(resolve,[status(thm)],[c_295,c_3383]) ).
cnf(c_3384,plain,
( op(e2,e3) != e4
| ~ defn_100
| op(e3,e2) = e2
| e4 = e1 ),
inference(paramod,[status(thm)],[c_3111,c_2543]) ).
cnf(c_3385,plain,
( op(e2,e3) != e4
| ~ defn_100
| e4 = e2
| e4 = e1 ),
inference(paramod,[status(thm)],[c_3111,c_3384]) ).
cnf(c_3386,plain,
( e4 != e4
| ~ defn_100
| e4 = e2
| e4 = e1 ),
inference(paramod,[status(thm)],[c_3104,c_3385]) ).
cnf(c_3387,plain,
( e4 != e4
| ~ defn_100
| e4 = e2
| e1 = e4 ),
inference(copy,[status(thm)],[c_3386]) ).
cnf(c_3388,plain,
( e4 != e4
| ~ defn_100
| e2 = e4
| e1 = e4 ),
inference(copy,[status(thm)],[c_3387]) ).
cnf(c_3389,plain,
( ~ defn_100
| e2 = e4
| e1 = e4 ),
inference(copy,[status(thm)],[c_3388]) ).
cnf(c_3390,plain,
( ~ defn_100
| e2 = e4 ),
inference(resolve,[status(thm)],[c_307,c_3389]) ).
cnf(c_3158,plain,
~ defn_100,
inference(resolve,[status(thm)],[c_311,c_3390]) ).
cnf(c_3391,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| e2 = e0
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_3140,c_2153]) ).
cnf(c_3392,plain,
( op(e2,e4) = e0
| e4 = e0
| e2 = e0
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_3104,c_3391]) ).
cnf(c_3393,plain,
( e1 = e0
| e4 = e0
| e2 = e0
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_3080,c_3392]) ).
cnf(c_3394,plain,
( e1 = e0
| e4 = e0
| e0 = e2
| ~ defn_90 ),
inference(copy,[status(thm)],[c_3393]) ).
cnf(c_3395,plain,
( e1 = e0
| e0 = e4
| e0 = e2
| ~ defn_90 ),
inference(copy,[status(thm)],[c_3394]) ).
cnf(c_3396,plain,
( e0 = e1
| e0 = e4
| e0 = e2
| ~ defn_90 ),
inference(copy,[status(thm)],[c_3395]) ).
cnf(c_3397,plain,
( e0 = e1
| e0 = e4
| ~ defn_90 ),
inference(resolve,[status(thm)],[c_297,c_3396]) ).
cnf(c_3398,plain,
( e0 = e1
| ~ defn_90 ),
inference(resolve,[status(thm)],[c_301,c_3397]) ).
cnf(c_3159,plain,
~ defn_90,
inference(resolve,[status(thm)],[c_295,c_3398]) ).
cnf(c_3399,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| e2 = e0
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_3140,c_2149]) ).
cnf(c_3400,plain,
( op(e2,e4) = e0
| e4 = e0
| e2 = e0
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_3104,c_3399]) ).
cnf(c_3401,plain,
( e1 = e0
| e4 = e0
| e2 = e0
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_3080,c_3400]) ).
cnf(c_3402,plain,
( e1 = e0
| e4 = e0
| e0 = e2
| ~ defn_50 ),
inference(copy,[status(thm)],[c_3401]) ).
cnf(c_3403,plain,
( e1 = e0
| e0 = e4
| e0 = e2
| ~ defn_50 ),
inference(copy,[status(thm)],[c_3402]) ).
cnf(c_3404,plain,
( e0 = e1
| e0 = e4
| e0 = e2
| ~ defn_50 ),
inference(copy,[status(thm)],[c_3403]) ).
cnf(c_3405,plain,
( e0 = e1
| e0 = e4
| ~ defn_50 ),
inference(resolve,[status(thm)],[c_297,c_3404]) ).
cnf(c_3406,plain,
( e0 = e1
| ~ defn_50 ),
inference(resolve,[status(thm)],[c_301,c_3405]) ).
cnf(c_3160,plain,
~ defn_50,
inference(resolve,[status(thm)],[c_295,c_3406]) ).
cnf(c_3407,negated_conjecture,
( op(op(e4,e3),e3) = e4
| op(e2,e4) != op(e4,e2)
| op(op(e4,e1),e1) = e4
| op(e0,e4) != op(e4,e0)
| op(op(e3,e4),e4) = e3
| op(e4,e2) = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3111,c_664]) ).
cnf(c_3408,negated_conjecture,
( op(op(e4,e3),e3) = e4
| op(e2,e4) != op(e4,e2)
| op(op(e4,e1),e1) = e4
| op(e0,e4) != op(e4,e0)
| op(op(e3,e4),e4) = e3
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3110,c_3407]) ).
cnf(c_3409,negated_conjecture,
( op(op(e4,e3),e3) = e4
| op(e2,e4) != op(e4,e2)
| op(op(e4,e1),e1) = e4
| op(e0,e4) != op(e4,e0)
| op(e0,e4) = e3
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3144,c_3408]) ).
cnf(c_3410,negated_conjecture,
( op(op(e4,e3),e3) = e4
| op(e2,e4) != op(e4,e2)
| op(op(e4,e1),e1) = e4
| op(e0,e4) != op(e4,e0)
| e4 = e3
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3137,c_3409]) ).
cnf(c_3411,negated_conjecture,
( op(op(e4,e3),e3) = e4
| op(e2,e4) != op(e4,e2)
| op(op(e4,e1),e1) = e4
| e4 != op(e4,e0)
| e4 = e3
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3137,c_3410]) ).
cnf(c_3412,negated_conjecture,
( op(op(e4,e3),e3) = e4
| op(e2,e4) != op(e4,e2)
| op(op(e4,e1),e1) = e4
| e4 != e4
| e4 = e3
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3136,c_3411]) ).
cnf(c_3413,negated_conjecture,
( op(op(e4,e3),e3) = e4
| op(e2,e4) != op(e4,e2)
| op(e3,e1) = e4
| e4 != e4
| e4 = e3
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3123,c_3412]) ).
cnf(c_3414,negated_conjecture,
( op(op(e4,e3),e3) = e4
| op(e2,e4) != op(e4,e2)
| e2 = e4
| e4 != e4
| e4 = e3
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3122,c_3413]) ).
cnf(c_3415,negated_conjecture,
( op(op(e4,e3),e3) = e4
| e1 != op(e4,e2)
| e2 = e4
| e4 != e4
| e4 = e3
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3080,c_3414]) ).
cnf(c_3416,negated_conjecture,
( op(op(e4,e3),e3) = e4
| e1 != e1
| e2 = e4
| e4 != e4
| e4 = e3
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3110,c_3415]) ).
cnf(c_3417,negated_conjecture,
( op(e0,e3) = e4
| e1 != e1
| e2 = e4
| e4 != e4
| e4 = e3
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3145,c_3416]) ).
cnf(c_3418,negated_conjecture,
( e3 = e4
| e1 != e1
| e2 = e4
| e4 != e4
| e4 = e3
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3139,c_3417]) ).
cnf(c_3419,negated_conjecture,
( e3 = e4
| e1 != e1
| e2 = e4
| e4 != e4
| e3 = e4
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_3418]) ).
cnf(c_3420,negated_conjecture,
( e3 = e4
| e1 != e1
| e2 = e4
| e3 = e4
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_3419]) ).
cnf(c_3421,negated_conjecture,
( e3 = e4
| e2 = e4
| e3 = e4
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_3420]) ).
cnf(c_3422,negated_conjecture,
( e2 = e4
| e3 = e4
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_3421]) ).
cnf(c_3423,negated_conjecture,
( e2 = e4
| e3 = e4
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10 ),
inference(resolve,[status(thm)],[c_3151,c_3422]) ).
cnf(c_3424,negated_conjecture,
( e2 = e4
| e3 = e4
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20 ),
inference(resolve,[status(thm)],[c_3146,c_3423]) ).
cnf(c_3425,negated_conjecture,
( e2 = e4
| e3 = e4
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30 ),
inference(resolve,[status(thm)],[c_3149,c_3424]) ).
cnf(c_3426,negated_conjecture,
( e2 = e4
| e3 = e4
| e1 = e3
| 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_3148,c_3425]) ).
cnf(c_3427,negated_conjecture,
( e2 = e4
| e3 = e4
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50 ),
inference(resolve,[status(thm)],[c_3152,c_3426]) ).
cnf(c_3428,negated_conjecture,
( e2 = e4
| e3 = e4
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60 ),
inference(resolve,[status(thm)],[c_3160,c_3427]) ).
cnf(c_3429,negated_conjecture,
( e2 = e4
| e3 = e4
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70 ),
inference(resolve,[status(thm)],[c_3153,c_3428]) ).
cnf(c_3430,negated_conjecture,
( e2 = e4
| e3 = e4
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80 ),
inference(resolve,[status(thm)],[c_3155,c_3429]) ).
cnf(c_3431,negated_conjecture,
( e2 = e4
| e3 = e4
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90 ),
inference(resolve,[status(thm)],[c_3147,c_3430]) ).
cnf(c_3432,negated_conjecture,
( e2 = e4
| e3 = e4
| e1 = e3
| defn_130
| defn_120
| defn_110
| defn_100 ),
inference(resolve,[status(thm)],[c_3159,c_3431]) ).
cnf(c_3433,negated_conjecture,
( e2 = e4
| e3 = e4
| e1 = e3
| defn_130
| defn_120
| defn_110 ),
inference(resolve,[status(thm)],[c_3158,c_3432]) ).
cnf(c_3434,negated_conjecture,
( e2 = e4
| e3 = e4
| e1 = e3
| defn_130
| defn_120 ),
inference(resolve,[status(thm)],[c_3156,c_3433]) ).
cnf(c_3435,negated_conjecture,
( e2 = e4
| e3 = e4
| e1 = e3
| defn_130 ),
inference(resolve,[status(thm)],[c_3150,c_3434]) ).
cnf(c_3436,negated_conjecture,
( e2 = e4
| e3 = e4
| e1 = e3 ),
inference(resolve,[status(thm)],[c_3154,c_3435]) ).
cnf(c_3437,negated_conjecture,
( e2 = e4
| e3 = e4 ),
inference(resolve,[status(thm)],[c_305,c_3436]) ).
cnf(c_3438,negated_conjecture,
e2 = e4,
inference(resolve,[status(thm)],[c_313,c_3437]) ).
cnf(c_3161,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_311,c_3438]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG064+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 21:05:17 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 23863 was started by sandbox on n010,
% 0.09/0.37 % Sat Sep 26 21:05:17 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 4.35/4.64
% 4.35/4.64 % From the command line: assign(max_seconds, 300).
% 32.48/8.23
% 32.48/8.23 % given #500 (I,wt=74): 1064 defn_00 | defn_10 | defn_20 | defn_30 | defn_40 | defn_50 | defn_60 | defn_70 | defn_80 | defn_90 | defn_100 | defn_110 | defn_120 | defn_130 | op(op(e3,e2),e3) != e2 | op(op(e3,e4),e3) != e4 | op(op(e4,e0),e4) != e0 | op(op(e4,e1),e1) = e4 | op(op(e4,e2),e4) != e2 | op(op(e4,e3),e4) != e3 # tptp_name(co1). [deny(7)].
% 32.48/8.23
% 32.48/8.23 % SZS status Theorem for theBenchmark
% 32.48/8.23
% 32.48/8.23 % Proof 1 at 3.06 (+ 0.48) seconds.
% 32.48/8.23 % Length of proof is 266.
% 32.48/8.23 % Level of proof is 18.
% 32.48/8.23 % Maximum clause weight is 70.000.
% 32.48/8.23 % Given clauses 771.
% 32.48/8.23
% 32.48/8.23 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------