%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG056+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 : n005.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:21 AM UTC 2026
% Result : Theorem 15.28s 4.23s
% Output : CNFRefutation 15.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 85
% Number of leaves : 21
% Syntax : Number of formulae : 434 ( 159 unt; 14 def)
% Number of atoms : 1962 (1660 equ)
% Maximal formula atoms : 250 ( 4 avg)
% Number of connectives : 1991 ( 463 ~;1132 |; 382 &)
% ( 14 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 4 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(e2,e2)
& e3 = op(e2,op(e2,e2))
& e1 = op(op(e2,op(e2,e2)),op(e2,e2))
& e0 = op(op(e2,e2),op(e2,e2)) ),
file('theBenchmark.p',ax6) ).
fof(co1,conjecture,
~ ( ( ( op(e4,e4) != e4
& op(e4,e4) = e4
& op(e4,e4) = e4 )
| ( op(e4,e3) != e4
& op(e3,e3) = e4
& op(e4,e4) = e3 )
| ( op(e4,e2) != e4
& op(e2,e2) = e4
& op(e4,e4) = e2 )
| ( op(e4,e1) != e4
& op(e1,e1) = e4
& op(e4,e4) = e1 )
| ( op(e4,e0) != e4
& op(e0,e0) = e4
& op(e4,e4) = e0 )
| ( op(e3,e4) != e3
& op(e4,e4) = e3
& op(e3,e3) = e4 )
| ( op(e3,e3) != e3
& op(e3,e3) = e3
& op(e3,e3) = e3 )
| ( op(e3,e2) != e3
& op(e2,e2) = e3
& op(e3,e3) = e2 )
| ( op(e3,e1) != e3
& op(e1,e1) = e3
& op(e3,e3) = e1 )
| ( op(e3,e0) != e3
& op(e0,e0) = e3
& op(e3,e3) = e0 )
| ( op(e2,e4) != e2
& op(e4,e4) = e2
& op(e2,e2) = e4 )
| ( op(e2,e3) != e2
& op(e3,e3) = e2
& op(e2,e2) = e3 )
| ( op(e2,e2) != e2
& op(e2,e2) = e2
& op(e2,e2) = e2 )
| ( op(e2,e1) != e2
& op(e1,e1) = e2
& op(e2,e2) = e1 )
| ( op(e2,e0) != e2
& op(e0,e0) = e2
& op(e2,e2) = e0 )
| ( op(e1,e4) != e1
& op(e4,e4) = e1
& op(e1,e1) = e4 )
| ( op(e1,e3) != e1
& op(e3,e3) = e1
& op(e1,e1) = e3 )
| ( op(e1,e2) != e1
& op(e2,e2) = e1
& op(e1,e1) = e2 )
| ( op(e1,e1) != e1
& op(e1,e1) = e1
& op(e1,e1) = e1 )
| ( op(e1,e0) != e1
& op(e0,e0) = e1
& op(e1,e1) = e0 )
| ( op(e0,e4) != e0
& op(e4,e4) = e0
& op(e0,e0) = e4 )
| ( op(e0,e3) != e0
& op(e3,e3) = e0
& op(e0,e0) = e3 )
| ( op(e0,e2) != e0
& op(e2,e2) = e0
& op(e0,e0) = e2 )
| ( op(e0,e1) != e0
& op(e1,e1) = e0
& op(e0,e0) = e1 )
| ( op(e0,e0) != e0
& op(e0,e0) = e0
& op(e0,e0) = e0 ) )
& ( ( op(e4,op(e4,e4)) = e4
& op(e4,op(e4,e4)) != e4 )
| ( op(e4,op(e3,e4)) = e3
& op(e3,op(e3,e4)) != e4 )
| ( op(e4,op(e2,e4)) = e2
& op(e2,op(e2,e4)) != e4 )
| ( op(e4,op(e1,e4)) = e1
& op(e1,op(e1,e4)) != e4 )
| ( op(e4,op(e0,e4)) = e0
& op(e0,op(e0,e4)) != e4 ) )
& ( ( op(e3,op(e4,e3)) = e4
& op(e4,op(e4,e3)) != e3 )
| ( op(e3,op(e3,e3)) = e3
& op(e3,op(e3,e3)) != e3 )
| ( op(e3,op(e2,e3)) = e2
& op(e2,op(e2,e3)) != e3 )
| ( op(e3,op(e1,e3)) = e1
& op(e1,op(e1,e3)) != e3 )
| ( op(e3,op(e0,e3)) = e0
& op(e0,op(e0,e3)) != e3 ) )
& ( ( op(e2,op(e4,e2)) = e4
& op(e4,op(e4,e2)) != e2 )
| ( op(e2,op(e3,e2)) = e3
& op(e3,op(e3,e2)) != e2 )
| ( op(e2,op(e2,e2)) = e2
& op(e2,op(e2,e2)) != e2 )
| ( op(e2,op(e1,e2)) = e1
& op(e1,op(e1,e2)) != e2 )
| ( op(e2,op(e0,e2)) = e0
& op(e0,op(e0,e2)) != e2 ) )
& ( ( op(e1,op(e4,e1)) = e4
& op(e4,op(e4,e1)) != e1 )
| ( op(e1,op(e3,e1)) = e3
& op(e3,op(e3,e1)) != e1 )
| ( op(e1,op(e2,e1)) = e2
& op(e2,op(e2,e1)) != e1 )
| ( op(e1,op(e1,e1)) = e1
& op(e1,op(e1,e1)) != e1 )
| ( op(e1,op(e0,e1)) = e0
& op(e0,op(e0,e1)) != e1 ) )
& ( ( op(e0,op(e4,e0)) = e4
& op(e4,op(e4,e0)) != e0 )
| ( op(e0,op(e3,e0)) = e3
& op(e3,op(e3,e0)) != e0 )
| ( op(e0,op(e2,e0)) = e2
& op(e2,op(e2,e0)) != e0 )
| ( op(e0,op(e1,e0)) = e1
& op(e1,op(e1,e0)) != e0 )
| ( op(e0,op(e0,e0)) = e0
& op(e0,op(e0,e0)) != e0 ) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ~ ( ( ( op(e4,e4) != e4
& op(e4,e4) = e4
& op(e4,e4) = e4 )
| ( op(e4,e3) != e4
& op(e3,e3) = e4
& op(e4,e4) = e3 )
| ( op(e4,e2) != e4
& op(e2,e2) = e4
& op(e4,e4) = e2 )
| ( op(e4,e1) != e4
& op(e1,e1) = e4
& op(e4,e4) = e1 )
| ( op(e4,e0) != e4
& op(e0,e0) = e4
& op(e4,e4) = e0 )
| ( op(e3,e4) != e3
& op(e4,e4) = e3
& op(e3,e3) = e4 )
| ( op(e3,e3) != e3
& op(e3,e3) = e3
& op(e3,e3) = e3 )
| ( op(e3,e2) != e3
& op(e2,e2) = e3
& op(e3,e3) = e2 )
| ( op(e3,e1) != e3
& op(e1,e1) = e3
& op(e3,e3) = e1 )
| ( op(e3,e0) != e3
& op(e0,e0) = e3
& op(e3,e3) = e0 )
| ( op(e2,e4) != e2
& op(e4,e4) = e2
& op(e2,e2) = e4 )
| ( op(e2,e3) != e2
& op(e3,e3) = e2
& op(e2,e2) = e3 )
| ( op(e2,e2) != e2
& op(e2,e2) = e2
& op(e2,e2) = e2 )
| ( op(e2,e1) != e2
& op(e1,e1) = e2
& op(e2,e2) = e1 )
| ( op(e2,e0) != e2
& op(e0,e0) = e2
& op(e2,e2) = e0 )
| ( op(e1,e4) != e1
& op(e4,e4) = e1
& op(e1,e1) = e4 )
| ( op(e1,e3) != e1
& op(e3,e3) = e1
& op(e1,e1) = e3 )
| ( op(e1,e2) != e1
& op(e2,e2) = e1
& op(e1,e1) = e2 )
| ( op(e1,e1) != e1
& op(e1,e1) = e1
& op(e1,e1) = e1 )
| ( op(e1,e0) != e1
& op(e0,e0) = e1
& op(e1,e1) = e0 )
| ( op(e0,e4) != e0
& op(e4,e4) = e0
& op(e0,e0) = e4 )
| ( op(e0,e3) != e0
& op(e3,e3) = e0
& op(e0,e0) = e3 )
| ( op(e0,e2) != e0
& op(e2,e2) = e0
& op(e0,e0) = e2 )
| ( op(e0,e1) != e0
& op(e1,e1) = e0
& op(e0,e0) = e1 )
| ( op(e0,e0) != e0
& op(e0,e0) = e0
& op(e0,e0) = e0 ) )
& ( ( op(e4,op(e4,e4)) = e4
& op(e4,op(e4,e4)) != e4 )
| ( op(e4,op(e3,e4)) = e3
& op(e3,op(e3,e4)) != e4 )
| ( op(e4,op(e2,e4)) = e2
& op(e2,op(e2,e4)) != e4 )
| ( op(e4,op(e1,e4)) = e1
& op(e1,op(e1,e4)) != e4 )
| ( op(e4,op(e0,e4)) = e0
& op(e0,op(e0,e4)) != e4 ) )
& ( ( op(e3,op(e4,e3)) = e4
& op(e4,op(e4,e3)) != e3 )
| ( op(e3,op(e3,e3)) = e3
& op(e3,op(e3,e3)) != e3 )
| ( op(e3,op(e2,e3)) = e2
& op(e2,op(e2,e3)) != e3 )
| ( op(e3,op(e1,e3)) = e1
& op(e1,op(e1,e3)) != e3 )
| ( op(e3,op(e0,e3)) = e0
& op(e0,op(e0,e3)) != e3 ) )
& ( ( op(e2,op(e4,e2)) = e4
& op(e4,op(e4,e2)) != e2 )
| ( op(e2,op(e3,e2)) = e3
& op(e3,op(e3,e2)) != e2 )
| ( op(e2,op(e2,e2)) = e2
& op(e2,op(e2,e2)) != e2 )
| ( op(e2,op(e1,e2)) = e1
& op(e1,op(e1,e2)) != e2 )
| ( op(e2,op(e0,e2)) = e0
& op(e0,op(e0,e2)) != e2 ) )
& ( ( op(e1,op(e4,e1)) = e4
& op(e4,op(e4,e1)) != e1 )
| ( op(e1,op(e3,e1)) = e3
& op(e3,op(e3,e1)) != e1 )
| ( op(e1,op(e2,e1)) = e2
& op(e2,op(e2,e1)) != e1 )
| ( op(e1,op(e1,e1)) = e1
& op(e1,op(e1,e1)) != e1 )
| ( op(e1,op(e0,e1)) = e0
& op(e0,op(e0,e1)) != e1 ) )
& ( ( op(e0,op(e4,e0)) = e4
& op(e4,op(e4,e0)) != e0 )
| ( op(e0,op(e3,e0)) = e3
& op(e3,op(e3,e0)) != e0 )
| ( op(e0,op(e2,e0)) = e2
& op(e2,op(e2,e0)) != e0 )
| ( op(e0,op(e1,e0)) = e1
& op(e1,op(e1,e0)) != e0 )
| ( op(e0,op(e0,e0)) = e0
& op(e0,op(e0,e0)) != e0 ) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_8,plain,
( op(e0,e0) = e4
| op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_10,plain,
( op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_11,plain,
( op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
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_18,plain,
( op(e2,e0) = e4
| op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = 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_26,plain,
( op(e3,e3) = e4
| op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_28,plain,
( op(e4,e0) = e4
| op(e4,e0) = e3
| op(e4,e0) = e2
| op(e4,e0) = e1
| op(e4,e0) = 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_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_89,plain,
( op(e4,e4) = e2
| op(e3,e4) = e2
| op(e2,e4) = e2
| op(e1,e4) = e2
| op(e0,e4) = e2 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_94,plain,
op(e1,e0) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_95,plain,
op(e2,e0) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_96,plain,
op(e0,e0) != op(e2,e0),
inference(copy,[status(thm)],[c_95]) ).
cnf(c_101,plain,
op(e2,e0) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_102,plain,
op(e1,e0) != op(e2,e0),
inference(copy,[status(thm)],[c_101]) ).
cnf(c_109,plain,
op(e4,e0) != op(e2,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_110,plain,
op(e2,e0) != op(e4,e0),
inference(copy,[status(thm)],[c_109]) ).
cnf(c_132,plain,
op(e1,e2) != op(e0,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_133,plain,
op(e2,e2) != op(e0,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_134,plain,
op(e0,e2) != op(e2,e2),
inference(copy,[status(thm)],[c_133]) ).
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_145,plain,
op(e3,e2) != op(e2,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_146,plain,
op(e2,e2) != op(e3,e2),
inference(copy,[status(thm)],[c_145]) ).
cnf(c_151,plain,
op(e1,e3) != op(e0,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_154,plain,
op(e3,e3) != op(e0,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_155,plain,
op(e0,e3) != op(e3,e3),
inference(copy,[status(thm)],[c_154]) ).
cnf(c_160,plain,
op(e3,e3) != op(e1,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_161,plain,
op(e1,e3) != op(e3,e3),
inference(copy,[status(thm)],[c_160]) ).
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_177,plain,
op(e2,e4) != op(e1,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_178,plain,
op(e1,e4) != op(e2,e4),
inference(copy,[status(thm)],[c_177]) ).
cnf(c_179,plain,
op(e3,e4) != op(e1,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_180,plain,
op(e1,e4) != op(e3,e4),
inference(copy,[status(thm)],[c_179]) ).
cnf(c_181,plain,
op(e4,e4) != op(e1,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_182,plain,
op(e1,e4) != op(e4,e4),
inference(copy,[status(thm)],[c_181]) ).
cnf(c_189,plain,
op(e0,e1) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_190,plain,
op(e0,e2) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_191,plain,
op(e0,e0) != op(e0,e2),
inference(copy,[status(thm)],[c_190]) ).
cnf(c_192,plain,
op(e0,e3) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_193,plain,
op(e0,e0) != op(e0,e3),
inference(copy,[status(thm)],[c_192]) ).
cnf(c_194,plain,
op(e0,e4) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_195,plain,
op(e0,e0) != op(e0,e4),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_196,plain,
op(e0,e2) != op(e0,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_197,plain,
op(e0,e1) != op(e0,e2),
inference(copy,[status(thm)],[c_196]) ).
cnf(c_198,plain,
op(e0,e3) != op(e0,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_199,plain,
op(e0,e1) != op(e0,e3),
inference(copy,[status(thm)],[c_198]) ).
cnf(c_202,plain,
op(e0,e3) != op(e0,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_203,plain,
op(e0,e2) != op(e0,e3),
inference(copy,[status(thm)],[c_202]) ).
cnf(c_206,plain,
op(e0,e4) != op(e0,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_207,plain,
op(e0,e3) != op(e0,e4),
inference(copy,[status(thm)],[c_206]) ).
cnf(c_227,plain,
op(e2,e1) != op(e2,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_228,plain,
op(e2,e2) != op(e2,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_229,plain,
op(e2,e0) != op(e2,e2),
inference(copy,[status(thm)],[c_228]) ).
cnf(c_232,plain,
op(e2,e4) != op(e2,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_233,plain,
op(e2,e0) != op(e2,e4),
inference(copy,[status(thm)],[c_232]) ).
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_257,plain,
op(e3,e4) != op(e3,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_258,plain,
op(e3,e1) != op(e3,e4),
inference(copy,[status(thm)],[c_257]) ).
cnf(c_259,plain,
op(e3,e3) != op(e3,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_260,plain,
op(e3,e2) != op(e3,e3),
inference(copy,[status(thm)],[c_259]) ).
cnf(c_261,plain,
op(e3,e4) != op(e3,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_262,plain,
op(e3,e2) != op(e3,e4),
inference(copy,[status(thm)],[c_261]) ).
cnf(c_263,plain,
op(e3,e4) != op(e3,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_264,plain,
op(e3,e3) != op(e3,e4),
inference(copy,[status(thm)],[c_263]) ).
cnf(c_265,plain,
op(e4,e1) != op(e4,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_268,plain,
op(e4,e3) != op(e4,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_269,plain,
op(e4,e0) != op(e4,e3),
inference(copy,[status(thm)],[c_268]) ).
cnf(c_270,plain,
op(e4,e4) != op(e4,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_271,plain,
op(e4,e0) != op(e4,e4),
inference(copy,[status(thm)],[c_270]) ).
cnf(c_280,plain,
op(e4,e4) != op(e4,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_281,plain,
op(e4,e2) != op(e4,e4),
inference(copy,[status(thm)],[c_280]) ).
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(e2,e2),op(e2,e2)) = e0,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_304,plain,
op(op(e2,op(e2,e2)),op(e2,e2)) = e1,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_305,plain,
op(e2,op(e2,e2)) = e3,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_306,plain,
op(e2,e2) = e4,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_320,negated_conjecture,
( op(e0,op(e4,e0)) = e4
| op(e3,op(e3,e0)) != e0
| op(e0,op(e2,e0)) = e2
| op(e0,op(e1,e0)) = e1 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_386,negated_conjecture,
( op(e4,op(e3,e4)) = e3
| op(e4,op(e2,e4)) = e2
| op(e4,op(e1,e4)) = e1
| op(e4,op(e0,e4)) = e0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
fof(def_defn_00,definition,
( defn_00
<=> ( op(e0,e1) != e0
& op(e1,e1) = e0
& op(e0,e0) = e1 ) ),
introduced(definition,[new_symbols(definition,[defn_00])],[]) ).
fof(def_defn_10,definition,
( defn_10
<=> ( op(e0,e2) != e0
& op(e2,e2) = e0
& op(e0,e0) = e2 ) ),
introduced(definition,[new_symbols(definition,[defn_10])],[]) ).
fof(def_defn_20,definition,
( defn_20
<=> ( op(e0,e3) != e0
& op(e3,e3) = e0
& op(e0,e0) = e3 ) ),
introduced(definition,[new_symbols(definition,[defn_20])],[]) ).
fof(def_defn_30,definition,
( defn_30
<=> ( op(e0,e4) != e0
& op(e4,e4) = e0
& op(e0,e0) = e4 ) ),
introduced(definition,[new_symbols(definition,[defn_30])],[]) ).
fof(def_defn_40,definition,
( defn_40
<=> ( op(e1,e0) != e1
& op(e0,e0) = e1
& op(e1,e1) = e0 ) ),
introduced(definition,[new_symbols(definition,[defn_40])],[]) ).
fof(def_defn_50,definition,
( defn_50
<=> ( op(e1,e2) != e1
& op(e2,e2) = e1
& op(e1,e1) = e2 ) ),
introduced(definition,[new_symbols(definition,[defn_50])],[]) ).
fof(def_defn_60,definition,
( defn_60
<=> ( op(e1,e3) != e1
& op(e3,e3) = e1
& op(e1,e1) = e3 ) ),
introduced(definition,[new_symbols(definition,[defn_60])],[]) ).
fof(def_defn_70,definition,
( defn_70
<=> ( op(e1,e4) != e1
& op(e4,e4) = e1
& op(e1,e1) = e4 ) ),
introduced(definition,[new_symbols(definition,[defn_70])],[]) ).
fof(def_defn_80,definition,
( defn_80
<=> ( op(e2,e0) != e2
& op(e0,e0) = e2
& op(e2,e2) = e0 ) ),
introduced(definition,[new_symbols(definition,[defn_80])],[]) ).
fof(def_defn_90,definition,
( defn_90
<=> ( op(e2,e1) != e2
& op(e1,e1) = e2
& op(e2,e2) = e1 ) ),
introduced(definition,[new_symbols(definition,[defn_90])],[]) ).
fof(def_defn_100,definition,
( defn_100
<=> ( op(e2,e3) != e2
& op(e3,e3) = e2
& op(e2,e2) = e3 ) ),
introduced(definition,[new_symbols(definition,[defn_100])],[]) ).
fof(def_defn_110,definition,
( defn_110
<=> ( op(e2,e4) != e2
& op(e4,e4) = e2
& op(e2,e2) = e4 ) ),
introduced(definition,[new_symbols(definition,[defn_110])],[]) ).
fof(def_defn_120,definition,
( defn_120
<=> ( op(e3,e0) != e3
& op(e0,e0) = e3
& op(e3,e3) = e0 ) ),
introduced(definition,[new_symbols(definition,[defn_120])],[]) ).
fof(def_defn_130,definition,
( defn_130
<=> ( op(e3,e1) != e3
& op(e1,e1) = e3
& op(e3,e3) = e1 ) ),
introduced(definition,[new_symbols(definition,[defn_130])],[]) ).
cnf(c_528,negated_conjecture,
( op(e4,e4) = e2
| op(e4,e4) = e1
| op(e0,e0) = e4
| op(e4,e4) = e3
| op(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_2952,negated_conjecture,
( op(e4,e4) = e2
| op(e4,e4) = e1
| op(e0,e0) = e4
| op(e4,e4) = e3
| e4 = 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_306,c_528]) ).
cnf(c_2953,negated_conjecture,
( op(e4,e4) = e2
| op(e4,e4) = e1
| op(e0,e0) = e4
| op(e4,e4) = e3
| e3 = e4
| 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_2952]) ).
cnf(c_529,negated_conjecture,
( op(e4,e4) = e2
| op(e4,e4) = e1
| op(e0,e0) = e4
| op(e4,e4) = 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(resolve,[status(thm)],[c_302,c_2953]) ).
cnf(c_632,negated_conjecture,
( op(e3,e3) = e1
| ~ defn_130 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_130]) ).
cnf(c_633,negated_conjecture,
( op(e3,e0) != e3
| ~ defn_120 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_120]) ).
cnf(c_637,negated_conjecture,
( op(e4,e4) = e2
| ~ defn_110 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_110]) ).
cnf(c_641,negated_conjecture,
( op(e2,e2) = e3
| ~ defn_100 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_100]) ).
cnf(c_2954,negated_conjecture,
( e4 = e3
| ~ defn_100 ),
inference(paramod,[status(thm)],[c_306,c_641]) ).
cnf(c_2955,negated_conjecture,
( e3 = e4
| ~ defn_100 ),
inference(copy,[status(thm)],[c_2954]) ).
cnf(c_642,negated_conjecture,
~ defn_100,
inference(resolve,[status(thm)],[c_302,c_2955]) ).
cnf(c_645,negated_conjecture,
( op(e2,e2) = e1
| ~ defn_90 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_90]) ).
cnf(c_2956,negated_conjecture,
( e4 = e1
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_306,c_645]) ).
cnf(c_2957,negated_conjecture,
( e1 = e4
| ~ defn_90 ),
inference(copy,[status(thm)],[c_2956]) ).
cnf(c_646,negated_conjecture,
~ defn_90,
inference(resolve,[status(thm)],[c_296,c_2957]) ).
cnf(c_649,negated_conjecture,
( op(e2,e2) = e0
| ~ defn_80 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_80]) ).
cnf(c_2958,negated_conjecture,
( e4 = e0
| ~ defn_80 ),
inference(paramod,[status(thm)],[c_306,c_649]) ).
cnf(c_2959,negated_conjecture,
( e0 = e4
| ~ defn_80 ),
inference(copy,[status(thm)],[c_2958]) ).
cnf(c_650,negated_conjecture,
~ defn_80,
inference(resolve,[status(thm)],[c_290,c_2959]) ).
cnf(c_652,negated_conjecture,
( op(e4,e4) = e1
| ~ defn_70 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_70]) ).
cnf(c_655,negated_conjecture,
( op(e3,e3) = e1
| ~ defn_60 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_60]) ).
cnf(c_658,negated_conjecture,
( op(e2,e2) = e1
| ~ defn_50 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_50]) ).
cnf(c_2960,negated_conjecture,
( e4 = e1
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_306,c_658]) ).
cnf(c_2961,negated_conjecture,
( e1 = e4
| ~ defn_50 ),
inference(copy,[status(thm)],[c_2960]) ).
cnf(c_659,negated_conjecture,
~ defn_50,
inference(resolve,[status(thm)],[c_296,c_2961]) ).
cnf(c_660,negated_conjecture,
( op(e1,e0) != e1
| ~ defn_40 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_40]) ).
cnf(c_665,negated_conjecture,
( op(e0,e0) = e4
| ~ defn_30 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_30]) ).
cnf(c_668,negated_conjecture,
( op(e0,e0) = e3
| ~ defn_20 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_20]) ).
cnf(c_670,negated_conjecture,
( op(e2,e2) = e0
| ~ defn_10 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_10]) ).
cnf(c_2962,negated_conjecture,
( e4 = e0
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_306,c_670]) ).
cnf(c_2963,negated_conjecture,
( e0 = e4
| ~ defn_10 ),
inference(copy,[status(thm)],[c_2962]) ).
cnf(c_671,negated_conjecture,
~ defn_10,
inference(resolve,[status(thm)],[c_290,c_2963]) ).
cnf(c_674,negated_conjecture,
( op(e0,e0) = e1
| ~ defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00]) ).
cnf(c_2964,plain,
op(op(e2,e4),op(e2,e2)) = e1,
inference(paramod,[status(thm)],[c_306,c_304]) ).
cnf(c_675,plain,
op(op(e2,e4),e4) = e1,
inference(paramod,[status(thm)],[c_306,c_2964]) ).
cnf(c_676,plain,
op(e2,e4) = e3,
inference(paramod,[status(thm)],[c_306,c_305]) ).
cnf(c_2965,plain,
op(e4,op(e2,e2)) = e0,
inference(paramod,[status(thm)],[c_306,c_303]) ).
cnf(c_677,plain,
op(e4,e4) = e0,
inference(paramod,[status(thm)],[c_306,c_2965]) ).
cnf(c_680,plain,
op(e2,e0) != e4,
inference(paramod,[status(thm)],[c_306,c_229]) ).
cnf(c_2966,plain,
e4 != op(e3,e2),
inference(paramod,[status(thm)],[c_306,c_146]) ).
cnf(c_682,plain,
op(e3,e2) != e4,
inference(copy,[status(thm)],[c_2966]) ).
cnf(c_684,plain,
op(e0,e2) != e4,
inference(paramod,[status(thm)],[c_306,c_134]) ).
cnf(c_2967,negated_conjecture,
( op(e4,e4) = e2
| op(e4,e4) = e1
| op(e0,e0) = e4
| e0 = 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_677,c_529]) ).
cnf(c_2968,negated_conjecture,
( op(e4,e4) = e2
| e0 = e1
| op(e0,e0) = e4
| e0 = 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_677,c_2967]) ).
cnf(c_2969,negated_conjecture,
( e0 = e2
| e0 = e1
| op(e0,e0) = e4
| e0 = 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_677,c_2968]) ).
cnf(c_2970,negated_conjecture,
( e0 = e2
| e1 = e0
| op(e0,e0) = e4
| e0 = 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_2969]) ).
cnf(c_2971,negated_conjecture,
( e0 = e2
| e1 = e0
| op(e0,e0) = e4
| e0 = 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_00 ),
inference(resolve,[status(thm)],[c_671,c_2970]) ).
cnf(c_2972,negated_conjecture,
( e0 = e2
| e1 = e0
| op(e0,e0) = e4
| e0 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_40
| defn_30
| defn_20
| defn_00 ),
inference(resolve,[status(thm)],[c_659,c_2971]) ).
cnf(c_2973,negated_conjecture,
( e0 = e2
| e1 = e0
| op(e0,e0) = e4
| e0 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_70
| defn_60
| defn_40
| defn_30
| defn_20
| defn_00 ),
inference(resolve,[status(thm)],[c_650,c_2972]) ).
cnf(c_2974,negated_conjecture,
( e0 = e2
| e1 = e0
| op(e0,e0) = e4
| e0 = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_70
| defn_60
| defn_40
| defn_30
| defn_20
| defn_00 ),
inference(resolve,[status(thm)],[c_646,c_2973]) ).
cnf(c_2975,negated_conjecture,
( e0 = e2
| e1 = e0
| op(e0,e0) = e4
| e0 = e3
| defn_130
| defn_120
| defn_110
| defn_70
| defn_60
| defn_40
| defn_30
| defn_20
| defn_00 ),
inference(resolve,[status(thm)],[c_642,c_2974]) ).
cnf(c_2976,negated_conjecture,
( e0 = e2
| e1 = e0
| op(e0,e0) = e4
| defn_130
| defn_120
| defn_110
| defn_70
| defn_60
| defn_40
| defn_30
| defn_20
| defn_00 ),
inference(resolve,[status(thm)],[c_288,c_2975]) ).
cnf(c_2977,negated_conjecture,
( e0 = e2
| op(e0,e0) = e4
| defn_130
| defn_120
| defn_110
| defn_70
| defn_60
| defn_40
| defn_30
| defn_20
| defn_00 ),
inference(resolve,[status(thm)],[c_284,c_2976]) ).
cnf(c_703,negated_conjecture,
( op(e0,e0) = e4
| defn_130
| defn_120
| defn_110
| defn_70
| defn_60
| defn_40
| defn_30
| defn_20
| defn_00 ),
inference(resolve,[status(thm)],[c_286,c_2977]) ).
cnf(c_704,plain,
op(e3,e4) = e1,
inference(paramod,[status(thm)],[c_676,c_675]) ).
cnf(c_2978,negated_conjecture,
( op(e4,op(e3,e4)) = e3
| op(e4,e3) = e2
| op(e4,op(e1,e4)) = e1
| op(e4,op(e0,e4)) = e0 ),
inference(paramod,[status(thm)],[c_676,c_386]) ).
cnf(c_705,negated_conjecture,
( op(e4,e1) = e3
| op(e4,e3) = e2
| op(e4,op(e1,e4)) = e1
| op(e4,op(e0,e4)) = e0 ),
inference(paramod,[status(thm)],[c_704,c_2978]) ).
cnf(c_715,plain,
op(e2,e0) != e3,
inference(paramod,[status(thm)],[c_676,c_233]) ).
cnf(c_716,plain,
op(e1,e4) != e3,
inference(paramod,[status(thm)],[c_676,c_178]) ).
cnf(c_2979,plain,
( op(e4,e4) = e2
| op(e3,e4) = e2
| e3 = e2
| op(e1,e4) = e2
| op(e0,e4) = e2 ),
inference(paramod,[status(thm)],[c_676,c_89]) ).
cnf(c_2980,plain,
( op(e4,e4) = e2
| e1 = e2
| e3 = e2
| op(e1,e4) = e2
| op(e0,e4) = e2 ),
inference(paramod,[status(thm)],[c_704,c_2979]) ).
cnf(c_2981,plain,
( e0 = e2
| e1 = e2
| e3 = e2
| op(e1,e4) = e2
| op(e0,e4) = e2 ),
inference(paramod,[status(thm)],[c_677,c_2980]) ).
cnf(c_2982,plain,
( e0 = e2
| e1 = e2
| e2 = e3
| op(e1,e4) = e2
| op(e0,e4) = e2 ),
inference(copy,[status(thm)],[c_2981]) ).
cnf(c_2983,plain,
( e0 = e2
| e1 = e2
| op(e1,e4) = e2
| op(e0,e4) = e2 ),
inference(resolve,[status(thm)],[c_298,c_2982]) ).
cnf(c_2984,plain,
( e0 = e2
| op(e1,e4) = e2
| op(e0,e4) = e2 ),
inference(resolve,[status(thm)],[c_292,c_2983]) ).
cnf(c_719,plain,
( op(e1,e4) = e2
| op(e0,e4) = e2 ),
inference(resolve,[status(thm)],[c_286,c_2984]) ).
cnf(c_2985,negated_conjecture,
( e0 = e1
| ~ defn_70 ),
inference(paramod,[status(thm)],[c_677,c_652]) ).
cnf(c_2986,negated_conjecture,
( e1 = e0
| ~ defn_70 ),
inference(copy,[status(thm)],[c_2985]) ).
cnf(c_720,negated_conjecture,
~ defn_70,
inference(resolve,[status(thm)],[c_284,c_2986]) ).
cnf(c_2987,negated_conjecture,
( e0 = e2
| ~ defn_110 ),
inference(paramod,[status(thm)],[c_677,c_637]) ).
cnf(c_721,negated_conjecture,
~ defn_110,
inference(resolve,[status(thm)],[c_286,c_2987]) ).
cnf(c_723,plain,
op(e4,e2) != e0,
inference(paramod,[status(thm)],[c_677,c_281]) ).
cnf(c_725,plain,
op(e4,e0) != e0,
inference(paramod,[status(thm)],[c_677,c_271]) ).
cnf(c_726,plain,
op(e1,e4) != e0,
inference(paramod,[status(thm)],[c_677,c_182]) ).
cnf(c_2988,plain,
( op(e2,e0) = e4
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 ),
inference(resolve,[status(thm)],[c_715,c_18]) ).
cnf(c_737,plain,
( op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 ),
inference(resolve,[status(thm)],[c_680,c_2988]) ).
cnf(c_740,plain,
( op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 ),
inference(resolve,[status(thm)],[c_682,c_25]) ).
cnf(c_744,plain,
( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 ),
inference(resolve,[status(thm)],[c_684,c_10]) ).
cnf(c_745,plain,
op(e3,e3) != e1,
inference(paramod,[status(thm)],[c_704,c_264]) ).
cnf(c_746,plain,
op(e3,e2) != e1,
inference(paramod,[status(thm)],[c_704,c_262]) ).
cnf(c_747,plain,
op(e3,e1) != e1,
inference(paramod,[status(thm)],[c_704,c_258]) ).
cnf(c_749,plain,
op(e1,e4) != e1,
inference(paramod,[status(thm)],[c_704,c_180]) ).
cnf(c_2989,plain,
( e1 = e2
| op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 ),
inference(paramod,[status(thm)],[c_704,c_78]) ).
cnf(c_752,plain,
( op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 ),
inference(resolve,[status(thm)],[c_292,c_2989]) ).
cnf(c_2990,plain,
( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2
| op(e1,e4) = e1 ),
inference(resolve,[status(thm)],[c_726,c_17]) ).
cnf(c_2991,plain,
( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2 ),
inference(resolve,[status(thm)],[c_749,c_2990]) ).
cnf(c_758,plain,
( op(e1,e4) = e4
| op(e1,e4) = e2 ),
inference(resolve,[status(thm)],[c_716,c_2991]) ).
cnf(c_2992,negated_conjecture,
( op(e0,e0) = e4
| defn_130
| defn_120
| defn_110
| defn_60
| defn_40
| defn_30
| defn_20
| defn_00 ),
inference(resolve,[status(thm)],[c_720,c_703]) ).
cnf(c_761,negated_conjecture,
( op(e0,e0) = e4
| defn_130
| defn_120
| defn_60
| defn_40
| defn_30
| defn_20
| defn_00 ),
inference(resolve,[status(thm)],[c_721,c_2992]) ).
cnf(c_769,plain,
( op(e4,e0) = e4
| op(e4,e0) = e3
| op(e4,e0) = e2
| op(e4,e0) = e1 ),
inference(resolve,[status(thm)],[c_725,c_28]) ).
cnf(c_772,negated_conjecture,
~ defn_60,
inference(resolve,[status(thm)],[c_745,c_655]) ).
cnf(c_773,negated_conjecture,
~ defn_130,
inference(resolve,[status(thm)],[c_745,c_632]) ).
cnf(c_775,plain,
( op(e3,e3) = e4
| op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e0 ),
inference(resolve,[status(thm)],[c_745,c_26]) ).
cnf(c_776,plain,
( op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e0 ),
inference(resolve,[status(thm)],[c_746,c_740]) ).
cnf(c_2993,negated_conjecture,
( op(e0,e0) = e4
| defn_130
| defn_120
| defn_40
| defn_30
| defn_20
| defn_00 ),
inference(resolve,[status(thm)],[c_772,c_761]) ).
cnf(c_785,negated_conjecture,
( op(e0,e0) = e4
| defn_120
| defn_40
| defn_30
| defn_20
| defn_00 ),
inference(resolve,[status(thm)],[c_773,c_2993]) ).
cnf(c_2994,plain,
( op(e4,e0) = e0
| unit = e3
| unit = e2
| unit = e1
| unit = e0 ),
inference(paramod,[status(thm)],[c_43,c_33]) ).
cnf(c_790,plain,
( unit = e3
| unit = e2
| unit = e1
| unit = e0 ),
inference(resolve,[status(thm)],[c_725,c_2994]) ).
cnf(c_1290,plain,
( op(e0,e0) != e1
| op(e2,e0) = e2
| op(e2,e0) = e0 ),
inference(paramod,[status(thm)],[c_737,c_96]) ).
cnf(c_2995,plain,
( e1 != op(e4,e0)
| op(e2,e0) = e2
| op(e2,e0) = e0 ),
inference(paramod,[status(thm)],[c_737,c_110]) ).
cnf(c_1297,plain,
( op(e4,e0) != e1
| op(e2,e0) = e2
| op(e2,e0) = e0 ),
inference(copy,[status(thm)],[c_2995]) ).
cnf(c_1383,plain,
( op(e0,e0) != e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 ),
inference(paramod,[status(thm)],[c_744,c_191]) ).
cnf(c_2996,plain,
( e1 != op(e0,e3)
| op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e0 ),
inference(paramod,[status(thm)],[c_744,c_203]) ).
cnf(c_1389,plain,
( op(e0,e3) != e1
| op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e0 ),
inference(copy,[status(thm)],[c_2996]) ).
cnf(c_2997,plain,
( op(e4,e1) = e3
| op(e4,e3) = e2
| op(e4,e4) = e1
| op(e4,op(e0,e4)) = e0
| op(e1,e4) = e2 ),
inference(paramod,[status(thm)],[c_758,c_705]) ).
cnf(c_2998,plain,
( op(e4,e1) = e3
| op(e4,e3) = e2
| e0 = e1
| op(e4,op(e0,e4)) = e0
| op(e1,e4) = e2 ),
inference(paramod,[status(thm)],[c_677,c_2997]) ).
cnf(c_2999,plain,
( op(e4,e1) = e3
| op(e4,e3) = e2
| e1 = e0
| op(e4,op(e0,e4)) = e0
| op(e1,e4) = e2 ),
inference(copy,[status(thm)],[c_2998]) ).
cnf(c_1504,plain,
( op(e4,e1) = e3
| op(e4,e3) = e2
| op(e4,op(e0,e4)) = e0
| op(e1,e4) = e2 ),
inference(resolve,[status(thm)],[c_284,c_2999]) ).
cnf(c_3000,plain,
( e2 != op(e4,e3)
| op(e4,e0) = e4
| op(e4,e0) = e3
| op(e4,e0) = e1 ),
inference(paramod,[status(thm)],[c_769,c_269]) ).
cnf(c_1657,plain,
( op(e4,e3) != e2
| op(e4,e0) = e4
| op(e4,e0) = e3
| op(e4,e0) = e1 ),
inference(copy,[status(thm)],[c_3000]) ).
cnf(c_1701,plain,
( op(e0,e3) != e4
| op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e0 ),
inference(paramod,[status(thm)],[c_775,c_155]) ).
cnf(c_3001,plain,
( e2 != op(e4,e3)
| op(e3,e3) = e4
| op(e3,e3) = e3
| op(e3,e3) = e0 ),
inference(paramod,[status(thm)],[c_775,c_169]) ).
cnf(c_1708,plain,
( op(e4,e3) != e2
| op(e3,e3) = e4
| op(e3,e3) = e3
| op(e3,e3) = e0 ),
inference(copy,[status(thm)],[c_3001]) ).
cnf(c_3002,plain,
( e0 != op(e3,e3)
| op(e3,e2) = e3
| op(e3,e2) = e2 ),
inference(paramod,[status(thm)],[c_776,c_260]) ).
cnf(c_1736,plain,
( op(e3,e3) != e0
| op(e3,e2) = e3
| op(e3,e2) = e2 ),
inference(copy,[status(thm)],[c_3002]) ).
cnf(c_3003,negated_conjecture,
( op(e0,e0) = e4
| op(e0,e0) = e4
| defn_120
| defn_40
| defn_20
| defn_00 ),
inference(resolve,[status(thm)],[c_785,c_665]) ).
cnf(c_1872,negated_conjecture,
( op(e0,e0) = e4
| defn_120
| defn_40
| defn_20
| defn_00 ),
inference(copy,[status(thm)],[c_3003]) ).
cnf(c_3004,plain,
( op(e3,e1) = e1
| unit = e2
| unit = e1
| unit = e0 ),
inference(paramod,[status(thm)],[c_790,c_35]) ).
cnf(c_1981,plain,
( unit = e2
| unit = e1
| unit = e0 ),
inference(resolve,[status(thm)],[c_747,c_3004]) ).
cnf(c_3005,plain,
( op(e2,e2) = e2
| unit = e1
| unit = e0 ),
inference(paramod,[status(thm)],[c_1981,c_37]) ).
cnf(c_3006,plain,
( e4 = e2
| unit = e1
| unit = e0 ),
inference(paramod,[status(thm)],[c_306,c_3005]) ).
cnf(c_3007,plain,
( e2 = e4
| unit = e1
| unit = e0 ),
inference(copy,[status(thm)],[c_3006]) ).
cnf(c_2009,plain,
( unit = e1
| unit = e0 ),
inference(resolve,[status(thm)],[c_300,c_3007]) ).
cnf(c_2020,plain,
( op(e0,e0) = e0
| unit = e1 ),
inference(paramod,[status(thm)],[c_2009,c_33]) ).
cnf(c_2021,plain,
( op(e1,e0) = e0
| unit = e0 ),
inference(paramod,[status(thm)],[c_2009,c_33]) ).
cnf(c_2022,plain,
( op(e0,e1) = e0
| unit = e0 ),
inference(paramod,[status(thm)],[c_2009,c_34]) ).
cnf(c_2023,plain,
( op(e0,e1) = e1
| unit = e1 ),
inference(paramod,[status(thm)],[c_2009,c_35]) ).
cnf(c_2025,plain,
( op(e1,e0) = e1
| unit = e1 ),
inference(paramod,[status(thm)],[c_2009,c_36]) ).
cnf(c_2027,plain,
( op(e1,e2) = e2
| unit = e0 ),
inference(paramod,[status(thm)],[c_2009,c_37]) ).
cnf(c_2029,plain,
( op(e2,e1) = e2
| unit = e0 ),
inference(paramod,[status(thm)],[c_2009,c_38]) ).
cnf(c_2030,plain,
( op(e0,e3) = e3
| unit = e1 ),
inference(paramod,[status(thm)],[c_2009,c_39]) ).
cnf(c_2031,plain,
( op(e1,e3) = e3
| unit = e0 ),
inference(paramod,[status(thm)],[c_2009,c_39]) ).
cnf(c_2032,plain,
( op(e3,e0) = e3
| unit = e1 ),
inference(paramod,[status(thm)],[c_2009,c_40]) ).
cnf(c_2033,plain,
( op(e3,e1) = e3
| unit = e0 ),
inference(paramod,[status(thm)],[c_2009,c_40]) ).
cnf(c_2035,plain,
( op(e1,e4) = e4
| unit = e0 ),
inference(paramod,[status(thm)],[c_2009,c_41]) ).
cnf(c_2037,plain,
( op(e4,e1) = e4
| unit = e0 ),
inference(paramod,[status(thm)],[c_2009,c_42]) ).
cnf(c_3008,plain,
( e0 = e4
| defn_120
| defn_40
| defn_20
| defn_00
| unit = e1 ),
inference(paramod,[status(thm)],[c_2020,c_1872]) ).
cnf(c_2053,plain,
( defn_120
| defn_40
| defn_20
| defn_00
| unit = e1 ),
inference(resolve,[status(thm)],[c_290,c_3008]) ).
cnf(c_3009,plain,
( e0 != op(e0,e0)
| unit = e0 ),
inference(paramod,[status(thm)],[c_2021,c_94]) ).
cnf(c_2083,plain,
( op(e0,e0) != e0
| unit = e0 ),
inference(copy,[status(thm)],[c_3009]) ).
cnf(c_3010,plain,
( e0 != op(e2,e0)
| unit = e0 ),
inference(paramod,[status(thm)],[c_2021,c_102]) ).
cnf(c_2084,plain,
( op(e2,e0) != e0
| unit = e0 ),
inference(copy,[status(thm)],[c_3010]) ).
cnf(c_3011,plain,
( e0 != op(e0,e2)
| unit = e0 ),
inference(paramod,[status(thm)],[c_2022,c_197]) ).
cnf(c_2104,plain,
( op(e0,e2) != e0
| unit = e0 ),
inference(copy,[status(thm)],[c_3011]) ).
cnf(c_3012,plain,
( e0 != op(e0,e3)
| unit = e0 ),
inference(paramod,[status(thm)],[c_2022,c_199]) ).
cnf(c_2105,plain,
( op(e0,e3) != e0
| unit = e0 ),
inference(copy,[status(thm)],[c_3012]) ).
cnf(c_3013,plain,
( e1 != op(e0,e0)
| unit = e1 ),
inference(paramod,[status(thm)],[c_2023,c_189]) ).
cnf(c_2121,plain,
( op(e0,e0) != e1
| unit = e1 ),
inference(copy,[status(thm)],[c_3013]) ).
cnf(c_2140,plain,
( ~ defn_40
| unit = e1 ),
inference(resolve,[status(thm)],[c_2025,c_660]) ).
cnf(c_3014,plain,
( defn_120
| defn_20
| defn_00
| unit = e1
| unit = e1 ),
inference(resolve,[status(thm)],[c_2140,c_2053]) ).
cnf(c_2155,plain,
( defn_120
| defn_20
| defn_00
| unit = e1 ),
inference(copy,[status(thm)],[c_3014]) ).
cnf(c_3015,plain,
( e2 != op(e0,e2)
| unit = e0 ),
inference(paramod,[status(thm)],[c_2027,c_132]) ).
cnf(c_2193,plain,
( op(e0,e2) != e2
| unit = e0 ),
inference(copy,[status(thm)],[c_3015]) ).
cnf(c_3016,plain,
( e2 != op(e3,e2)
| unit = e0 ),
inference(paramod,[status(thm)],[c_2027,c_142]) ).
cnf(c_2194,plain,
( op(e3,e2) != e2
| unit = e0 ),
inference(copy,[status(thm)],[c_3016]) ).
cnf(c_3017,plain,
( e2 != op(e2,e0)
| unit = e0 ),
inference(paramod,[status(thm)],[c_2029,c_227]) ).
cnf(c_2222,plain,
( op(e2,e0) != e2
| unit = e0 ),
inference(copy,[status(thm)],[c_3017]) ).
cnf(c_2234,plain,
( op(e0,e0) != e3
| unit = e1 ),
inference(paramod,[status(thm)],[c_2030,c_193]) ).
cnf(c_3018,plain,
( e3 != op(e0,e3)
| unit = e0 ),
inference(paramod,[status(thm)],[c_2031,c_151]) ).
cnf(c_2244,plain,
( op(e0,e3) != e3
| unit = e0 ),
inference(copy,[status(thm)],[c_3018]) ).
cnf(c_3019,plain,
( e3 != op(e3,e3)
| unit = e0 ),
inference(paramod,[status(thm)],[c_2031,c_161]) ).
cnf(c_2245,plain,
( op(e3,e3) != e3
| unit = e0 ),
inference(copy,[status(thm)],[c_3019]) ).
cnf(c_2253,plain,
( ~ defn_120
| unit = e1 ),
inference(resolve,[status(thm)],[c_2032,c_633]) ).
cnf(c_3020,plain,
( defn_20
| defn_00
| unit = e1
| unit = e1 ),
inference(resolve,[status(thm)],[c_2253,c_2155]) ).
cnf(c_2264,plain,
( defn_20
| defn_00
| unit = e1 ),
inference(copy,[status(thm)],[c_3020]) ).
cnf(c_2265,plain,
( op(e0,e0) = e1
| defn_20
| unit = e1 ),
inference(resolve,[status(thm)],[c_2264,c_674]) ).
cnf(c_3021,plain,
( e3 != op(e3,e2)
| unit = e0 ),
inference(paramod,[status(thm)],[c_2033,c_254]) ).
cnf(c_2453,plain,
( op(e3,e2) != e3
| unit = e0 ),
inference(copy,[status(thm)],[c_3021]) ).
cnf(c_3022,plain,
( e4 = e2
| op(e0,e4) = e2
| unit = e0 ),
inference(paramod,[status(thm)],[c_2035,c_719]) ).
cnf(c_3023,plain,
( e2 = e4
| op(e0,e4) = e2
| unit = e0 ),
inference(copy,[status(thm)],[c_3022]) ).
cnf(c_2470,plain,
( op(e0,e4) = e2
| unit = e0 ),
inference(resolve,[status(thm)],[c_300,c_3023]) ).
cnf(c_3024,plain,
( e4 != op(e4,e0)
| unit = e0 ),
inference(paramod,[status(thm)],[c_2037,c_265]) ).
cnf(c_2481,plain,
( op(e4,e0) != e4
| unit = e0 ),
inference(copy,[status(thm)],[c_3024]) ).
cnf(c_2486,plain,
( op(e2,e0) = e2
| op(e2,e0) = e1
| unit = e0 ),
inference(resolve,[status(thm)],[c_2084,c_737]) ).
cnf(c_2493,plain,
( op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| unit = e0 ),
inference(resolve,[status(thm)],[c_2105,c_11]) ).
cnf(c_2508,plain,
( op(e3,e2) = e3
| op(e3,e2) = e0
| unit = e0 ),
inference(resolve,[status(thm)],[c_2194,c_776]) ).
cnf(c_2509,plain,
( op(e3,e3) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2
| unit = e0 ),
inference(resolve,[status(thm)],[c_2194,c_752]) ).
cnf(c_2558,plain,
( op(e0,e0) != e2
| unit = e0 ),
inference(paramod,[status(thm)],[c_2470,c_195]) ).
cnf(c_2559,plain,
( op(e0,e3) != e2
| unit = e0 ),
inference(paramod,[status(thm)],[c_2470,c_207]) ).
cnf(c_2574,plain,
( op(e0,e0) = e4
| op(e0,e0) = e3
| op(e0,e0) = e1
| op(e0,e0) = e0
| unit = e0 ),
inference(resolve,[status(thm)],[c_2558,c_8]) ).
cnf(c_3025,plain,
( unit = e1
| defn_20
| unit = e1 ),
inference(resolve,[status(thm)],[c_2265,c_2121]) ).
cnf(c_2581,plain,
( defn_20
| unit = e1 ),
inference(copy,[status(thm)],[c_3025]) ).
cnf(c_2582,plain,
( op(e0,e0) = e3
| unit = e1 ),
inference(resolve,[status(thm)],[c_2581,c_668]) ).
cnf(c_3026,plain,
( unit = e1
| unit = e1 ),
inference(resolve,[status(thm)],[c_2582,c_2234]) ).
cnf(c_2735,plain,
unit = e1,
inference(copy,[status(thm)],[c_3026]) ).
cnf(c_3027,plain,
( op(e0,e0) = e4
| op(e0,e0) = e3
| op(e0,e0) = e1
| op(e0,e0) = e0
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2574]) ).
cnf(c_2738,plain,
( op(e0,e0) = e4
| op(e0,e0) = e3
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(resolve,[status(thm)],[c_284,c_3027]) ).
cnf(c_3028,plain,
( op(e0,e3) != e2
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2559]) ).
cnf(c_2745,plain,
op(e0,e3) != e2,
inference(resolve,[status(thm)],[c_284,c_3028]) ).
cnf(c_3029,plain,
( op(e3,e3) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2509]) ).
cnf(c_2763,plain,
( op(e3,e3) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 ),
inference(resolve,[status(thm)],[c_284,c_3029]) ).
cnf(c_3030,plain,
( op(e3,e2) = e3
| op(e3,e2) = e0
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2508]) ).
cnf(c_2764,plain,
( op(e3,e2) = e3
| op(e3,e2) = e0 ),
inference(resolve,[status(thm)],[c_284,c_3030]) ).
cnf(c_3031,plain,
( op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2493]) ).
cnf(c_3032,plain,
( op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1 ),
inference(resolve,[status(thm)],[c_284,c_3031]) ).
cnf(c_2766,plain,
( op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e3) = e1 ),
inference(resolve,[status(thm)],[c_2745,c_3032]) ).
cnf(c_3033,plain,
( op(e2,e0) = e2
| op(e2,e0) = e1
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2486]) ).
cnf(c_2773,plain,
( op(e2,e0) = e2
| op(e2,e0) = e1 ),
inference(resolve,[status(thm)],[c_284,c_3033]) ).
cnf(c_3034,plain,
( op(e4,e0) != e4
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2481]) ).
cnf(c_2778,plain,
op(e4,e0) != e4,
inference(resolve,[status(thm)],[c_284,c_3034]) ).
cnf(c_3035,plain,
( op(e0,e4) = e2
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2470]) ).
cnf(c_2781,plain,
op(e0,e4) = e2,
inference(resolve,[status(thm)],[c_284,c_3035]) ).
cnf(c_3036,plain,
( op(e3,e2) != e3
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2453]) ).
cnf(c_2789,plain,
op(e3,e2) != e3,
inference(resolve,[status(thm)],[c_284,c_3036]) ).
cnf(c_3037,plain,
( op(e3,e3) != e3
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2245]) ).
cnf(c_2800,plain,
op(e3,e3) != e3,
inference(resolve,[status(thm)],[c_284,c_3037]) ).
cnf(c_3038,plain,
( op(e0,e3) != e3
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2244]) ).
cnf(c_2801,plain,
op(e0,e3) != e3,
inference(resolve,[status(thm)],[c_284,c_3038]) ).
cnf(c_3039,plain,
( op(e2,e0) != e2
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2222]) ).
cnf(c_2806,plain,
op(e2,e0) != e2,
inference(resolve,[status(thm)],[c_284,c_3039]) ).
cnf(c_3040,plain,
( op(e0,e2) != e2
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2193]) ).
cnf(c_2819,plain,
op(e0,e2) != e2,
inference(resolve,[status(thm)],[c_284,c_3040]) ).
cnf(c_3041,plain,
( op(e0,e2) != e0
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2104]) ).
cnf(c_2830,plain,
op(e0,e2) != e0,
inference(resolve,[status(thm)],[c_284,c_3041]) ).
cnf(c_3042,plain,
( op(e0,e0) != e0
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2083]) ).
cnf(c_2842,plain,
op(e0,e0) != e0,
inference(resolve,[status(thm)],[c_284,c_3042]) ).
cnf(c_3043,plain,
( op(e4,e1) = e4
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2037]) ).
cnf(c_2845,plain,
op(e4,e1) = e4,
inference(resolve,[status(thm)],[c_284,c_3043]) ).
cnf(c_3044,plain,
( op(e1,e4) = e4
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2035]) ).
cnf(c_2846,plain,
op(e1,e4) = e4,
inference(resolve,[status(thm)],[c_284,c_3044]) ).
cnf(c_3045,plain,
( op(e3,e1) = e3
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2033]) ).
cnf(c_2847,plain,
op(e3,e1) = e3,
inference(resolve,[status(thm)],[c_284,c_3045]) ).
cnf(c_3046,plain,
( op(e0,e1) = e0
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2022]) ).
cnf(c_2852,plain,
op(e0,e1) = e0,
inference(resolve,[status(thm)],[c_284,c_3046]) ).
cnf(c_3047,plain,
( op(e1,e0) = e0
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2735,c_2021]) ).
cnf(c_2853,plain,
op(e1,e0) = e0,
inference(resolve,[status(thm)],[c_284,c_3047]) ).
cnf(c_2889,plain,
( op(e4,e3) != e2
| op(e4,e0) = e3
| op(e4,e0) = e1 ),
inference(resolve,[status(thm)],[c_2778,c_1657]) ).
cnf(c_3048,plain,
( op(e4,e1) = e3
| op(e4,e3) = e2
| op(e4,op(e0,e4)) = e0
| e4 = e2 ),
inference(paramod,[status(thm)],[c_2846,c_1504]) ).
cnf(c_3049,plain,
( op(e4,e1) = e3
| op(e4,e3) = e2
| op(e4,e2) = e0
| e4 = e2 ),
inference(paramod,[status(thm)],[c_2781,c_3048]) ).
cnf(c_3050,plain,
( e4 = e3
| op(e4,e3) = e2
| op(e4,e2) = e0
| e4 = e2 ),
inference(paramod,[status(thm)],[c_2845,c_3049]) ).
cnf(c_3051,plain,
( e4 = e3
| op(e4,e3) = e2
| op(e4,e2) = e0
| e2 = e4 ),
inference(copy,[status(thm)],[c_3050]) ).
cnf(c_3052,plain,
( e3 = e4
| op(e4,e3) = e2
| op(e4,e2) = e0
| e2 = e4 ),
inference(copy,[status(thm)],[c_3051]) ).
cnf(c_3053,plain,
( e3 = e4
| op(e4,e3) = e2
| op(e4,e2) = e0 ),
inference(resolve,[status(thm)],[c_300,c_3052]) ).
cnf(c_3054,plain,
( e3 = e4
| op(e4,e3) = e2 ),
inference(resolve,[status(thm)],[c_723,c_3053]) ).
cnf(c_2904,plain,
op(e4,e3) = e2,
inference(resolve,[status(thm)],[c_302,c_3054]) ).
cnf(c_2905,plain,
op(e3,e2) = e0,
inference(resolve,[status(thm)],[c_2789,c_2764]) ).
cnf(c_3055,plain,
( op(e3,e3) != e0
| op(e3,e2) = e3
| e0 = e2 ),
inference(paramod,[status(thm)],[c_2905,c_1736]) ).
cnf(c_3056,plain,
( op(e3,e3) != e0
| e0 = e3
| e0 = e2 ),
inference(paramod,[status(thm)],[c_2905,c_3055]) ).
cnf(c_3057,plain,
( op(e3,e3) != e0
| e0 = e3 ),
inference(resolve,[status(thm)],[c_286,c_3056]) ).
cnf(c_2907,plain,
op(e3,e3) != e0,
inference(resolve,[status(thm)],[c_288,c_3057]) ).
cnf(c_3058,plain,
( e2 != e2
| op(e3,e3) = e4
| op(e3,e3) = e3
| op(e3,e3) = e0 ),
inference(paramod,[status(thm)],[c_2904,c_1708]) ).
cnf(c_3059,plain,
( op(e3,e3) = e4
| op(e3,e3) = e3
| op(e3,e3) = e0 ),
inference(copy,[status(thm)],[c_3058]) ).
cnf(c_3060,plain,
( op(e3,e3) = e4
| op(e3,e3) = e3 ),
inference(resolve,[status(thm)],[c_2907,c_3059]) ).
cnf(c_2924,plain,
op(e3,e3) = e4,
inference(resolve,[status(thm)],[c_2800,c_3060]) ).
cnf(c_3061,plain,
( op(e0,e3) != e4
| op(e3,e3) = e3
| op(e3,e3) = e2
| e4 = e0 ),
inference(paramod,[status(thm)],[c_2924,c_1701]) ).
cnf(c_3062,plain,
( op(e0,e3) != e4
| op(e3,e3) = e3
| e4 = e2
| e4 = e0 ),
inference(paramod,[status(thm)],[c_2924,c_3061]) ).
cnf(c_3063,plain,
( op(e0,e3) != e4
| e4 = e3
| e4 = e2
| e4 = e0 ),
inference(paramod,[status(thm)],[c_2924,c_3062]) ).
cnf(c_3064,plain,
( op(e0,e3) != e4
| e4 = e3
| e4 = e2
| e0 = e4 ),
inference(copy,[status(thm)],[c_3063]) ).
cnf(c_3065,plain,
( op(e0,e3) != e4
| e4 = e3
| e2 = e4
| e0 = e4 ),
inference(copy,[status(thm)],[c_3064]) ).
cnf(c_3066,plain,
( op(e0,e3) != e4
| e3 = e4
| e2 = e4
| e0 = e4 ),
inference(copy,[status(thm)],[c_3065]) ).
cnf(c_3067,plain,
( op(e0,e3) != e4
| e3 = e4
| e2 = e4 ),
inference(resolve,[status(thm)],[c_290,c_3066]) ).
cnf(c_3068,plain,
( op(e0,e3) != e4
| e3 = e4 ),
inference(resolve,[status(thm)],[c_300,c_3067]) ).
cnf(c_2925,plain,
op(e0,e3) != e4,
inference(resolve,[status(thm)],[c_302,c_3068]) ).
cnf(c_3069,plain,
( op(e0,e3) = e4
| op(e0,e3) = e1 ),
inference(resolve,[status(thm)],[c_2801,c_2766]) ).
cnf(c_2926,plain,
op(e0,e3) = e1,
inference(resolve,[status(thm)],[c_2925,c_3069]) ).
cnf(c_2929,plain,
op(e2,e0) = e1,
inference(resolve,[status(thm)],[c_2806,c_2773]) ).
cnf(c_3070,plain,
( op(e4,e0) != e1
| op(e2,e0) = e2
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2929,c_1297]) ).
cnf(c_3071,plain,
( op(e4,e0) != e1
| e1 = e2
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2929,c_3070]) ).
cnf(c_3072,plain,
( op(e4,e0) != e1
| e1 = e2 ),
inference(resolve,[status(thm)],[c_284,c_3071]) ).
cnf(c_2930,plain,
op(e4,e0) != e1,
inference(resolve,[status(thm)],[c_292,c_3072]) ).
cnf(c_3073,plain,
( op(e0,e0) != e1
| op(e2,e0) = e2
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2929,c_1290]) ).
cnf(c_3074,plain,
( op(e0,e0) != e1
| e1 = e2
| e1 = e0 ),
inference(paramod,[status(thm)],[c_2929,c_3073]) ).
cnf(c_3075,plain,
( op(e0,e0) != e1
| e1 = e2 ),
inference(resolve,[status(thm)],[c_284,c_3074]) ).
cnf(c_2931,plain,
op(e0,e0) != e1,
inference(resolve,[status(thm)],[c_292,c_3075]) ).
cnf(c_3076,plain,
( op(e3,e3) = e2
| e3 = e2
| op(e3,e0) = e2 ),
inference(paramod,[status(thm)],[c_2847,c_2763]) ).
cnf(c_3077,plain,
( e4 = e2
| e3 = e2
| op(e3,e0) = e2 ),
inference(paramod,[status(thm)],[c_2924,c_3076]) ).
cnf(c_3078,plain,
( e4 = e2
| e2 = e3
| op(e3,e0) = e2 ),
inference(copy,[status(thm)],[c_3077]) ).
cnf(c_3079,plain,
( e2 = e4
| e2 = e3
| op(e3,e0) = e2 ),
inference(copy,[status(thm)],[c_3078]) ).
cnf(c_3080,plain,
( e2 = e4
| op(e3,e0) = e2 ),
inference(resolve,[status(thm)],[c_298,c_3079]) ).
cnf(c_2932,plain,
op(e3,e0) = e2,
inference(resolve,[status(thm)],[c_300,c_3080]) ).
cnf(c_3081,plain,
( e1 != e1
| op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e0 ),
inference(paramod,[status(thm)],[c_2926,c_1389]) ).
cnf(c_3082,plain,
( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e0 ),
inference(copy,[status(thm)],[c_3081]) ).
cnf(c_3083,plain,
( op(e0,e2) = e3
| op(e0,e2) = e2 ),
inference(resolve,[status(thm)],[c_2830,c_3082]) ).
cnf(c_2937,plain,
op(e0,e2) = e3,
inference(resolve,[status(thm)],[c_2819,c_3083]) ).
cnf(c_3084,plain,
( op(e0,e0) != e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| e3 = e0 ),
inference(paramod,[status(thm)],[c_2937,c_1383]) ).
cnf(c_3085,plain,
( op(e0,e0) != e3
| op(e0,e2) = e2
| e3 = e1
| e3 = e0 ),
inference(paramod,[status(thm)],[c_2937,c_3084]) ).
cnf(c_3086,plain,
( op(e0,e0) != e3
| e3 = e2
| e3 = e1
| e3 = e0 ),
inference(paramod,[status(thm)],[c_2937,c_3085]) ).
cnf(c_3087,plain,
( op(e0,e0) != e3
| e3 = e2
| e3 = e1
| e0 = e3 ),
inference(copy,[status(thm)],[c_3086]) ).
cnf(c_3088,plain,
( op(e0,e0) != e3
| e3 = e2
| e1 = e3
| e0 = e3 ),
inference(copy,[status(thm)],[c_3087]) ).
cnf(c_3089,plain,
( op(e0,e0) != e3
| e2 = e3
| e1 = e3
| e0 = e3 ),
inference(copy,[status(thm)],[c_3088]) ).
cnf(c_3090,plain,
( op(e0,e0) != e3
| e2 = e3
| e1 = e3 ),
inference(resolve,[status(thm)],[c_288,c_3089]) ).
cnf(c_3091,plain,
( op(e0,e0) != e3
| e2 = e3 ),
inference(resolve,[status(thm)],[c_294,c_3090]) ).
cnf(c_2938,plain,
op(e0,e0) != e3,
inference(resolve,[status(thm)],[c_298,c_3091]) ).
cnf(c_3092,plain,
( op(e0,e0) = e4
| op(e0,e0) = e3
| op(e0,e0) = e1 ),
inference(resolve,[status(thm)],[c_2842,c_2738]) ).
cnf(c_3093,plain,
( op(e0,e0) = e4
| op(e0,e0) = e3 ),
inference(resolve,[status(thm)],[c_2931,c_3092]) ).
cnf(c_2945,plain,
op(e0,e0) = e4,
inference(resolve,[status(thm)],[c_2938,c_3093]) ).
cnf(c_3094,negated_conjecture,
( op(e0,op(e4,e0)) = e4
| op(e3,op(e3,e0)) != e0
| op(e0,op(e2,e0)) = e2
| op(e0,e0) = e1 ),
inference(paramod,[status(thm)],[c_2853,c_320]) ).
cnf(c_3095,negated_conjecture,
( op(e0,op(e4,e0)) = e4
| op(e3,op(e3,e0)) != e0
| op(e0,op(e2,e0)) = e2
| e4 = e1 ),
inference(paramod,[status(thm)],[c_2945,c_3094]) ).
cnf(c_3096,negated_conjecture,
( op(e0,op(e4,e0)) = e4
| op(e3,op(e3,e0)) != e0
| op(e0,e1) = e2
| e4 = e1 ),
inference(paramod,[status(thm)],[c_2929,c_3095]) ).
cnf(c_3097,negated_conjecture,
( op(e0,op(e4,e0)) = e4
| op(e3,op(e3,e0)) != e0
| e0 = e2
| e4 = e1 ),
inference(paramod,[status(thm)],[c_2852,c_3096]) ).
cnf(c_3098,negated_conjecture,
( op(e0,op(e4,e0)) = e4
| op(e3,e2) != e0
| e0 = e2
| e4 = e1 ),
inference(paramod,[status(thm)],[c_2932,c_3097]) ).
cnf(c_3099,negated_conjecture,
( op(e0,op(e4,e0)) = e4
| e0 != e0
| e0 = e2
| e4 = e1 ),
inference(paramod,[status(thm)],[c_2905,c_3098]) ).
cnf(c_3100,negated_conjecture,
( op(e0,op(e4,e0)) = e4
| e0 != e0
| e0 = e2
| e1 = e4 ),
inference(copy,[status(thm)],[c_3099]) ).
cnf(c_3101,negated_conjecture,
( op(e0,op(e4,e0)) = e4
| e0 = e2
| e1 = e4 ),
inference(copy,[status(thm)],[c_3100]) ).
cnf(c_3102,negated_conjecture,
( op(e0,op(e4,e0)) = e4
| e0 = e2 ),
inference(resolve,[status(thm)],[c_296,c_3101]) ).
cnf(c_2946,negated_conjecture,
op(e0,op(e4,e0)) = e4,
inference(resolve,[status(thm)],[c_286,c_3102]) ).
cnf(c_3103,plain,
( e2 != e2
| op(e4,e0) = e3
| op(e4,e0) = e1 ),
inference(paramod,[status(thm)],[c_2904,c_2889]) ).
cnf(c_3104,plain,
( op(e4,e0) = e3
| op(e4,e0) = e1 ),
inference(copy,[status(thm)],[c_3103]) ).
cnf(c_2948,plain,
op(e4,e0) = e3,
inference(resolve,[status(thm)],[c_2930,c_3104]) ).
cnf(c_3105,negated_conjecture,
op(e0,e3) = e4,
inference(paramod,[status(thm)],[c_2948,c_2946]) ).
cnf(c_3106,negated_conjecture,
e1 = e4,
inference(paramod,[status(thm)],[c_2926,c_3105]) ).
cnf(c_2951,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_296,c_3106]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG056+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n005.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sat Sep 26 21:02:01 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.45 % Process 3098878 was started by sandbox on n005,
% 0.17/0.45 % Sat Sep 26 21:02:01 2026
% 0.17/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 2.27/2.53
% 2.27/2.53 % From the command line: assign(max_seconds, 300).
% 15.28/4.23
% 15.28/4.23 % given #500 (T,wt=12): 2248 unit = e0 | op(e1,e1) != e3. [para(2031(b,1),218(a,2))].
% 15.28/4.23
% 15.28/4.23 % SZS status Theorem for theBenchmark
% 15.28/4.23
% 15.28/4.23 % Proof 1 at 1.31 (+ 0.31) seconds.
% 15.28/4.23 % Length of proof is 264.
% 15.28/4.23 % Level of proof is 25.
% 15.28/4.23 % Maximum clause weight is 42.000.
% 15.28/4.23 % Given clauses 630.
% 15.28/4.23
% 15.28/4.23 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------