%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG170+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:38 AM UTC 2026
% Result : Theorem 10.05s 3.31s
% Output : CNFRefutation 10.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 9
% Syntax : Number of formulae : 544 ( 200 unt; 2 def)
% Number of atoms : 1955 (1929 equ)
% Maximal formula atoms : 250 ( 3 avg)
% Number of connectives : 1895 ( 484 ~;1111 |; 298 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(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,
( ( 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',ax2) ).
fof(ax3,axiom,
( op(op(e4,e4),op(e4,e4)) = e4
& op(op(e3,e4),op(e4,e3)) = e4
& op(op(e2,e4),op(e4,e2)) = e4
& op(op(e1,e4),op(e4,e1)) = e4
& op(op(e0,e4),op(e4,e0)) = e4
& op(op(e4,e3),op(e3,e4)) = e3
& op(op(e3,e3),op(e3,e3)) = e3
& op(op(e2,e3),op(e3,e2)) = e3
& op(op(e1,e3),op(e3,e1)) = e3
& op(op(e0,e3),op(e3,e0)) = e3
& op(op(e4,e2),op(e2,e4)) = e2
& op(op(e3,e2),op(e2,e3)) = e2
& op(op(e2,e2),op(e2,e2)) = e2
& op(op(e1,e2),op(e2,e1)) = e2
& op(op(e0,e2),op(e2,e0)) = e2
& op(op(e4,e1),op(e1,e4)) = e1
& op(op(e3,e1),op(e1,e3)) = e1
& op(op(e2,e1),op(e1,e2)) = e1
& op(op(e1,e1),op(e1,e1)) = e1
& op(op(e0,e1),op(e1,e0)) = e1
& op(op(e4,e0),op(e0,e4)) = e0
& op(op(e3,e0),op(e0,e3)) = e0
& op(op(e2,e0),op(e0,e2)) = e0
& op(op(e1,e0),op(e0,e1)) = e0
& op(op(e0,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,
( e3 = op(op(e4,op(e4,e4)),op(e4,op(e4,e4)))
& e2 = op(op(e4,op(e4,e4)),op(e4,e4))
& e1 = op(e4,e4)
& e0 = op(e4,op(e4,e4)) ),
file('theBenchmark.p',ax6) ).
fof(co1,conjecture,
~ ( ( ( op(e4,e4) != e4
& op(e4,e3) != e3
& op(e4,e2) != e2
& op(e4,e1) != e1
& op(e4,e0) != e0 )
| ( op(e3,e4) != e4
& op(e3,e3) != e3
& op(e3,e2) != e2
& op(e3,e1) != e1
& op(e3,e0) != e0 )
| ( op(e2,e4) != e4
& op(e2,e3) != e3
& op(e2,e2) != e2
& op(e2,e1) != e1
& op(e2,e0) != e0 )
| ( op(e1,e4) != e4
& op(e1,e3) != e3
& op(e1,e2) != e2
& op(e1,e1) != e1
& op(e1,e0) != e0 )
| ( op(e0,e4) != e4
& op(e0,e3) != e3
& op(e0,e2) != e2
& op(e0,e1) != e1
& op(e0,e0) != e0 ) )
& ( ( op(e4,e4) != e4
& op(e3,e4) != e3
& op(e2,e4) != e2
& op(e1,e4) != e1
& op(e0,e4) != e0 )
| ( op(e4,e3) != e4
& op(e3,e3) != e3
& op(e2,e3) != e2
& op(e1,e3) != e1
& op(e0,e3) != e0 )
| ( op(e4,e2) != e4
& op(e3,e2) != e3
& op(e2,e2) != e2
& op(e1,e2) != e1
& op(e0,e2) != e0 )
| ( op(e4,e1) != e4
& op(e3,e1) != e3
& op(e2,e1) != e2
& op(e1,e1) != e1
& op(e0,e1) != e0 )
| ( op(e4,e0) != e4
& op(e3,e0) != e3
& op(e2,e0) != e2
& op(e1,e0) != e1
& op(e0,e0) != e0 ) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ~ ( ( ( op(e4,e4) != e4
& op(e4,e3) != e3
& op(e4,e2) != e2
& op(e4,e1) != e1
& op(e4,e0) != e0 )
| ( op(e3,e4) != e4
& op(e3,e3) != e3
& op(e3,e2) != e2
& op(e3,e1) != e1
& op(e3,e0) != e0 )
| ( op(e2,e4) != e4
& op(e2,e3) != e3
& op(e2,e2) != e2
& op(e2,e1) != e1
& op(e2,e0) != e0 )
| ( op(e1,e4) != e4
& op(e1,e3) != e3
& op(e1,e2) != e2
& op(e1,e1) != e1
& op(e1,e0) != e0 )
| ( op(e0,e4) != e4
& op(e0,e3) != e3
& op(e0,e2) != e2
& op(e0,e1) != e1
& op(e0,e0) != e0 ) )
& ( ( op(e4,e4) != e4
& op(e3,e4) != e3
& op(e2,e4) != e2
& op(e1,e4) != e1
& op(e0,e4) != e0 )
| ( op(e4,e3) != e4
& op(e3,e3) != e3
& op(e2,e3) != e2
& op(e1,e3) != e1
& op(e0,e3) != e0 )
| ( op(e4,e2) != e4
& op(e3,e2) != e3
& op(e2,e2) != e2
& op(e1,e2) != e1
& op(e0,e2) != e0 )
| ( op(e4,e1) != e4
& op(e3,e1) != e3
& op(e2,e1) != e2
& op(e1,e1) != e1
& op(e0,e1) != e0 )
| ( op(e4,e0) != e4
& op(e3,e0) != e3
& op(e2,e0) != e2
& op(e1,e0) != e1
& op(e0,e0) != e0 ) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
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_12,plain,
( op(e0,e4) = e4
| op(e0,e4) = e3
| op(e0,e4) = e2
| op(e0,e4) = e1
| op(e0,e4) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_16,plain,
( op(e1,e3) = e4
| op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,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_19,plain,
( op(e2,e1) = e4
| op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_22,plain,
( op(e2,e4) = e4
| op(e2,e4) = e3
| op(e2,e4) = e2
| op(e2,e4) = e1
| op(e2,e4) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_27,plain,
( op(e3,e4) = e4
| op(e3,e4) = e3
| op(e3,e4) = e2
| op(e3,e4) = e1
| op(e3,e4) = 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(e0,e4) = e0
| op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_34,plain,
( op(e4,e0) = e0
| op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_35,plain,
( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_36,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)],[ax2]) ).
cnf(c_45,plain,
( op(e1,e4) = e1
| op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_46,plain,
( op(e4,e1) = e1
| op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_49,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_50,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)],[ax2]) ).
cnf(c_53,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)],[ax2]) ).
cnf(c_54,plain,
( op(e4,e2) = e0
| op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_55,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_57,plain,
( op(e2,e4) = e2
| op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_69,plain,
( op(e3,e4) = e3
| op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_70,plain,
( op(e4,e3) = e3
| op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_74,plain,
( op(e4,e4) = e0
| op(e3,e4) = e0
| op(e2,e4) = e0
| op(e1,e4) = e0
| op(e0,e4) = e0 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_79,plain,
( op(e4,e4) = e3
| op(e4,e3) = e3
| op(e4,e2) = e3
| op(e4,e1) = e3
| op(e4,e0) = e3 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_81,plain,
( op(e4,e4) = e4
| op(e4,e3) = e4
| op(e4,e2) = e4
| op(e4,e1) = e4
| op(e4,e0) = e4 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_82,plain,
( op(e4,e4) = e4
| op(e3,e4) = e4
| op(e2,e4) = e4
| op(e1,e4) = e4
| op(e0,e4) = e4 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_83,plain,
op(op(e0,e0),op(e0,e0)) = e0,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_84,plain,
op(op(e1,e0),op(e0,e1)) = e0,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_85,plain,
op(op(e2,e0),op(e0,e2)) = e0,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_86,plain,
op(op(e3,e0),op(e0,e3)) = e0,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_87,plain,
op(op(e4,e0),op(e0,e4)) = e0,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_88,plain,
op(op(e0,e1),op(e1,e0)) = e1,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_90,plain,
op(op(e2,e1),op(e1,e2)) = e1,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_91,plain,
op(op(e3,e1),op(e1,e3)) = e1,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_92,plain,
op(op(e4,e1),op(e1,e4)) = e1,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_98,plain,
op(op(e0,e3),op(e3,e0)) = e3,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_99,plain,
op(op(e1,e3),op(e3,e1)) = e3,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_104,plain,
op(op(e1,e4),op(e4,e1)) = e4,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_105,plain,
op(op(e2,e4),op(e4,e2)) = e4,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_107,plain,
op(op(e4,e4),op(e4,e4)) = e4,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_108,plain,
op(e1,e0) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_109,plain,
op(e0,e0) != op(e1,e0),
inference(copy,[status(thm)],[c_108]) ).
cnf(c_110,plain,
op(e2,e0) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_111,plain,
op(e0,e0) != op(e2,e0),
inference(copy,[status(thm)],[c_110]) ).
cnf(c_112,plain,
op(e3,e0) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_113,plain,
op(e0,e0) != op(e3,e0),
inference(copy,[status(thm)],[c_112]) ).
cnf(c_114,plain,
op(e4,e0) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_115,plain,
op(e0,e0) != op(e4,e0),
inference(copy,[status(thm)],[c_114]) ).
cnf(c_120,plain,
op(e3,e0) != op(e2,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_121,plain,
op(e4,e0) != op(e2,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_122,plain,
op(e2,e0) != op(e4,e0),
inference(copy,[status(thm)],[c_121]) ).
cnf(c_123,plain,
op(e4,e0) != op(e3,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_124,plain,
op(e3,e0) != op(e4,e0),
inference(copy,[status(thm)],[c_123]) ).
cnf(c_127,plain,
op(e2,e1) != op(e0,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_128,plain,
op(e0,e1) != op(e2,e1),
inference(copy,[status(thm)],[c_127]) ).
cnf(c_133,plain,
op(e2,e1) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_137,plain,
op(e3,e1) != op(e2,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_138,plain,
op(e4,e1) != op(e2,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_139,plain,
op(e2,e1) != op(e4,e1),
inference(copy,[status(thm)],[c_138]) ).
cnf(c_142,plain,
op(e1,e2) != op(e0,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_143,plain,
op(e0,e2) != op(e1,e2),
inference(copy,[status(thm)],[c_142]) ).
cnf(c_148,plain,
op(e4,e2) != op(e0,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_149,plain,
op(e0,e2) != op(e4,e2),
inference(copy,[status(thm)],[c_148]) ).
cnf(c_152,plain,
op(e4,e2) != op(e1,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_153,plain,
op(e1,e2) != op(e4,e2),
inference(copy,[status(thm)],[c_152]) ).
cnf(c_157,plain,
op(e4,e2) != op(e3,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_158,plain,
op(e3,e2) != op(e4,e2),
inference(copy,[status(thm)],[c_157]) ).
cnf(c_159,plain,
op(e1,e3) != op(e0,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_160,plain,
op(e0,e3) != op(e1,e3),
inference(copy,[status(thm)],[c_159]) ).
cnf(c_161,plain,
op(e2,e3) != op(e0,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_162,plain,
op(e0,e3) != op(e2,e3),
inference(copy,[status(thm)],[c_161]) ).
cnf(c_163,plain,
op(e3,e3) != op(e0,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_164,plain,
op(e0,e3) != op(e3,e3),
inference(copy,[status(thm)],[c_163]) ).
cnf(c_167,plain,
op(e2,e3) != op(e1,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_168,plain,
op(e3,e3) != op(e1,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_171,plain,
op(e3,e3) != op(e2,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_172,plain,
op(e4,e3) != op(e2,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_173,plain,
op(e2,e3) != op(e4,e3),
inference(copy,[status(thm)],[c_172]) ).
cnf(c_178,plain,
op(e2,e4) != op(e0,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_179,plain,
op(e0,e4) != op(e2,e4),
inference(copy,[status(thm)],[c_178]) ).
cnf(c_182,plain,
op(e4,e4) != op(e0,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_183,plain,
op(e0,e4) != op(e4,e4),
inference(copy,[status(thm)],[c_182]) ).
cnf(c_184,plain,
op(e2,e4) != op(e1,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_185,plain,
op(e3,e4) != op(e1,e4),
inference(clausify,[status(thm)],[ax4]) ).
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_188,plain,
op(e3,e4) != op(e2,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_189,plain,
op(e4,e4) != op(e2,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_190,plain,
op(e2,e4) != op(e4,e4),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_191,plain,
op(e4,e4) != op(e3,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_192,plain,
op(e3,e4) != op(e4,e4),
inference(copy,[status(thm)],[c_191]) ).
cnf(c_195,plain,
op(e0,e2) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_196,plain,
op(e0,e0) != op(e0,e2),
inference(copy,[status(thm)],[c_195]) ).
cnf(c_197,plain,
op(e0,e3) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_198,plain,
op(e0,e0) != op(e0,e3),
inference(copy,[status(thm)],[c_197]) ).
cnf(c_199,plain,
op(e0,e4) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_200,plain,
op(e0,e0) != op(e0,e4),
inference(copy,[status(thm)],[c_199]) ).
cnf(c_201,plain,
op(e0,e2) != op(e0,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_202,plain,
op(e0,e3) != op(e0,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_203,plain,
op(e0,e4) != op(e0,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_204,plain,
op(e0,e1) != op(e0,e4),
inference(copy,[status(thm)],[c_203]) ).
cnf(c_205,plain,
op(e0,e3) != op(e0,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_219,plain,
op(e1,e3) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_220,plain,
op(e1,e4) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_221,plain,
op(e1,e1) != op(e1,e4),
inference(copy,[status(thm)],[c_220]) ).
cnf(c_227,plain,
op(e2,e1) != op(e2,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_228,plain,
op(e2,e0) != op(e2,e1),
inference(copy,[status(thm)],[c_227]) ).
cnf(c_229,plain,
op(e2,e2) != op(e2,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_230,plain,
op(e2,e0) != op(e2,e2),
inference(copy,[status(thm)],[c_229]) ).
cnf(c_233,plain,
op(e2,e4) != op(e2,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_234,plain,
op(e2,e0) != op(e2,e4),
inference(copy,[status(thm)],[c_233]) ).
cnf(c_236,plain,
op(e2,e3) != op(e2,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_248,plain,
op(e3,e3) != op(e3,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_249,plain,
op(e3,e0) != op(e3,e3),
inference(copy,[status(thm)],[c_248]) ).
cnf(c_250,plain,
op(e3,e4) != op(e3,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_251,plain,
op(e3,e0) != op(e3,e4),
inference(copy,[status(thm)],[c_250]) ).
cnf(c_256,plain,
op(e3,e3) != op(e3,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_259,plain,
op(e3,e4) != op(e3,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_260,plain,
op(e3,e3) != op(e3,e4),
inference(copy,[status(thm)],[c_259]) ).
cnf(c_261,plain,
op(e4,e1) != op(e4,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_262,plain,
op(e4,e0) != op(e4,e1),
inference(copy,[status(thm)],[c_261]) ).
cnf(c_267,plain,
op(e4,e4) != op(e4,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_268,plain,
op(e4,e0) != op(e4,e4),
inference(copy,[status(thm)],[c_267]) ).
cnf(c_269,plain,
op(e4,e2) != op(e4,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_278,plain,
e1 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_279,plain,
e0 != e1,
inference(copy,[status(thm)],[c_278]) ).
cnf(c_280,plain,
e2 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_281,plain,
e0 != e2,
inference(copy,[status(thm)],[c_280]) ).
cnf(c_282,plain,
e3 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_283,plain,
e0 != e3,
inference(copy,[status(thm)],[c_282]) ).
cnf(c_284,plain,
e4 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_285,plain,
e0 != e4,
inference(copy,[status(thm)],[c_284]) ).
cnf(c_286,plain,
e2 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_287,plain,
e3 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_288,plain,
e4 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_289,plain,
e1 != e4,
inference(copy,[status(thm)],[c_288]) ).
cnf(c_290,plain,
e3 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_291,plain,
e4 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_292,plain,
e2 != e4,
inference(copy,[status(thm)],[c_291]) ).
cnf(c_293,plain,
e4 != e3,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_294,plain,
e3 != e4,
inference(copy,[status(thm)],[c_293]) ).
cnf(c_295,plain,
op(e4,op(e4,e4)) = e0,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_296,plain,
op(e4,e4) = e1,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_297,plain,
op(op(e4,op(e4,e4)),op(e4,e4)) = e2,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_3731,plain,
op(op(e4,e1),op(e4,e4)) = e2,
inference(paramod,[status(thm)],[c_296,c_297]) ).
cnf(c_298,plain,
op(op(e4,e1),e1) = e2,
inference(paramod,[status(thm)],[c_296,c_3731]) ).
cnf(c_299,plain,
op(op(e4,op(e4,e4)),op(e4,op(e4,e4))) = e3,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_3732,plain,
op(op(e4,e1),op(e4,op(e4,e4))) = e3,
inference(paramod,[status(thm)],[c_296,c_299]) ).
cnf(c_300,plain,
op(op(e4,e1),op(e4,e1)) = e3,
inference(paramod,[status(thm)],[c_296,c_3732]) ).
fof(def_defn_00,definition,
( defn_00
<=> ( op(e4,e0) != e4
& op(e3,e0) != e3
& op(e2,e0) != e2
& op(e1,e0) != e1
& op(e0,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_00])],[]) ).
cnf(c_746,negated_conjecture,
( op(e0,e4) != e0
| op(e4,e3) != e4
| op(e2,e2) != e2
| op(e3,e1) != e3
| defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00]) ).
fof(def_defn_10,definition,
( defn_10
<=> ( op(e0,e4) != e4
& op(e0,e3) != e3
& op(e0,e2) != e2
& op(e0,e1) != e1
& op(e0,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_10])],[]) ).
cnf(c_984,negated_conjecture,
( op(e4,e3) != e3
| op(e3,e1) != e1
| op(e2,e2) != e2
| op(e1,e0) != e0
| defn_10 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_10]) ).
cnf(c_1551,negated_conjecture,
( op(e0,e4) != e4
| ~ defn_10 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_10]) ).
cnf(c_1559,negated_conjecture,
( op(e1,e0) != e1
| ~ defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00]) ).
cnf(c_1561,plain,
op(e4,e1) = e0,
inference(paramod,[status(thm)],[c_296,c_295]) ).
cnf(c_1564,plain,
op(e4,e0) != e1,
inference(paramod,[status(thm)],[c_296,c_268]) ).
cnf(c_1565,plain,
op(e3,e4) != e1,
inference(paramod,[status(thm)],[c_296,c_192]) ).
cnf(c_1566,plain,
op(e2,e4) != e1,
inference(paramod,[status(thm)],[c_296,c_190]) ).
cnf(c_1567,plain,
op(e1,e4) != e1,
inference(paramod,[status(thm)],[c_296,c_187]) ).
cnf(c_1568,plain,
op(e0,e4) != e1,
inference(paramod,[status(thm)],[c_296,c_183]) ).
cnf(c_3733,plain,
op(e1,op(e4,e4)) = e4,
inference(paramod,[status(thm)],[c_296,c_107]) ).
cnf(c_1569,plain,
op(e1,e1) = e4,
inference(paramod,[status(thm)],[c_296,c_3733]) ).
cnf(c_3734,plain,
( e1 = e4
| op(e3,e4) = e4
| op(e2,e4) = e4
| op(e1,e4) = e4
| op(e0,e4) = e4 ),
inference(paramod,[status(thm)],[c_296,c_82]) ).
cnf(c_1570,plain,
( op(e3,e4) = e4
| op(e2,e4) = e4
| op(e1,e4) = e4
| op(e0,e4) = e4 ),
inference(resolve,[status(thm)],[c_289,c_3734]) ).
cnf(c_3735,plain,
( op(e4,e4) = e4
| op(e4,e3) = e4
| op(e4,e2) = e4
| e0 = e4
| op(e4,e0) = e4 ),
inference(paramod,[status(thm)],[c_1561,c_81]) ).
cnf(c_3736,plain,
( e1 = e4
| op(e4,e3) = e4
| op(e4,e2) = e4
| e0 = e4
| op(e4,e0) = e4 ),
inference(paramod,[status(thm)],[c_296,c_3735]) ).
cnf(c_3737,plain,
( e1 = e4
| op(e4,e3) = e4
| op(e4,e2) = e4
| op(e4,e0) = e4 ),
inference(resolve,[status(thm)],[c_285,c_3736]) ).
cnf(c_1571,plain,
( op(e4,e3) = e4
| op(e4,e2) = e4
| op(e4,e0) = e4 ),
inference(resolve,[status(thm)],[c_289,c_3737]) ).
cnf(c_3738,plain,
( op(e4,e4) = e3
| op(e4,e3) = e3
| op(e4,e2) = e3
| e0 = e3
| op(e4,e0) = e3 ),
inference(paramod,[status(thm)],[c_1561,c_79]) ).
cnf(c_3739,plain,
( e1 = e3
| op(e4,e3) = e3
| op(e4,e2) = e3
| e0 = e3
| op(e4,e0) = e3 ),
inference(paramod,[status(thm)],[c_296,c_3738]) ).
cnf(c_3740,plain,
( e3 = e1
| op(e4,e3) = e3
| op(e4,e2) = e3
| e0 = e3
| op(e4,e0) = e3 ),
inference(copy,[status(thm)],[c_3739]) ).
cnf(c_3741,plain,
( e3 = e1
| op(e4,e3) = e3
| op(e4,e2) = e3
| op(e4,e0) = e3 ),
inference(resolve,[status(thm)],[c_283,c_3740]) ).
cnf(c_1573,plain,
( op(e4,e3) = e3
| op(e4,e2) = e3
| op(e4,e0) = e3 ),
inference(resolve,[status(thm)],[c_287,c_3741]) ).
cnf(c_3742,plain,
( e1 = e0
| op(e3,e4) = e0
| op(e2,e4) = e0
| op(e1,e4) = e0
| op(e0,e4) = e0 ),
inference(paramod,[status(thm)],[c_296,c_74]) ).
cnf(c_3743,plain,
( e0 = e1
| op(e3,e4) = e0
| op(e2,e4) = e0
| op(e1,e4) = e0
| op(e0,e4) = e0 ),
inference(copy,[status(thm)],[c_3742]) ).
cnf(c_1576,plain,
( op(e3,e4) = e0
| op(e2,e4) = e0
| op(e1,e4) = e0
| op(e0,e4) = e0 ),
inference(resolve,[status(thm)],[c_279,c_3743]) ).
cnf(c_3744,plain,
op(e0,op(e4,e1)) = e3,
inference(paramod,[status(thm)],[c_1561,c_300]) ).
cnf(c_1577,plain,
op(e0,e0) = e3,
inference(paramod,[status(thm)],[c_1561,c_3744]) ).
cnf(c_1578,plain,
op(e0,e1) = e2,
inference(paramod,[status(thm)],[c_1561,c_298]) ).
cnf(c_1580,plain,
op(e4,e2) != e0,
inference(paramod,[status(thm)],[c_1561,c_269]) ).
cnf(c_1581,plain,
op(e4,e0) != e0,
inference(paramod,[status(thm)],[c_1561,c_262]) ).
cnf(c_1583,plain,
op(e2,e1) != e0,
inference(paramod,[status(thm)],[c_1561,c_139]) ).
cnf(c_1584,plain,
op(op(e1,e4),e0) = e4,
inference(paramod,[status(thm)],[c_1561,c_104]) ).
cnf(c_1585,plain,
op(e0,op(e1,e4)) = e1,
inference(paramod,[status(thm)],[c_1561,c_92]) ).
cnf(c_3745,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| e2 = e3 ),
inference(paramod,[status(thm)],[c_1578,c_50]) ).
cnf(c_3746,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| e4 = e3
| e2 = e3 ),
inference(paramod,[status(thm)],[c_1569,c_3745]) ).
cnf(c_3747,plain,
( e0 = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| e4 = e3
| e2 = e3 ),
inference(paramod,[status(thm)],[c_1561,c_3746]) ).
cnf(c_3748,plain,
( e0 = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| e4 = e3
| e3 = e2 ),
inference(copy,[status(thm)],[c_3747]) ).
cnf(c_3749,plain,
( e0 = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| e3 = e4
| e3 = e2 ),
inference(copy,[status(thm)],[c_3748]) ).
cnf(c_3750,plain,
( e0 = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| e3 = e4 ),
inference(resolve,[status(thm)],[c_290,c_3749]) ).
cnf(c_3751,plain,
( e0 = e3
| op(e3,e1) = e3
| op(e2,e1) = e3 ),
inference(resolve,[status(thm)],[c_294,c_3750]) ).
cnf(c_1586,plain,
( op(e3,e1) = e3
| op(e2,e1) = e3 ),
inference(resolve,[status(thm)],[c_283,c_3751]) ).
cnf(c_3752,plain,
( op(e4,e1) = e1
| op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| e2 = e1 ),
inference(paramod,[status(thm)],[c_1578,c_46]) ).
cnf(c_3753,plain,
( op(e4,e1) = e1
| op(e3,e1) = e1
| op(e2,e1) = e1
| e4 = e1
| e2 = e1 ),
inference(paramod,[status(thm)],[c_1569,c_3752]) ).
cnf(c_3754,plain,
( e0 = e1
| op(e3,e1) = e1
| op(e2,e1) = e1
| e4 = e1
| e2 = e1 ),
inference(paramod,[status(thm)],[c_1561,c_3753]) ).
cnf(c_3755,plain,
( e0 = e1
| op(e3,e1) = e1
| op(e2,e1) = e1
| e1 = e4
| e2 = e1 ),
inference(copy,[status(thm)],[c_3754]) ).
cnf(c_3756,plain,
( e0 = e1
| op(e3,e1) = e1
| op(e2,e1) = e1
| e1 = e4 ),
inference(resolve,[status(thm)],[c_286,c_3755]) ).
cnf(c_3757,plain,
( e0 = e1
| op(e3,e1) = e1
| op(e2,e1) = e1 ),
inference(resolve,[status(thm)],[c_289,c_3756]) ).
cnf(c_1587,plain,
( op(e3,e1) = e1
| op(e2,e1) = e1 ),
inference(resolve,[status(thm)],[c_279,c_3757]) ).
cnf(c_3758,plain,
( op(e4,e0) = e1
| op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| e3 = e1 ),
inference(paramod,[status(thm)],[c_1577,c_36]) ).
cnf(c_3759,plain,
( op(e4,e0) = e1
| op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1 ),
inference(resolve,[status(thm)],[c_287,c_3758]) ).
cnf(c_1592,plain,
( op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1 ),
inference(resolve,[status(thm)],[c_1564,c_3759]) ).
cnf(c_3760,plain,
( op(e4,e0) = e4
| op(e4,e0) = e3
| op(e4,e0) = e2
| op(e4,e0) = e1 ),
inference(resolve,[status(thm)],[c_1581,c_28]) ).
cnf(c_1593,plain,
( op(e4,e0) = e4
| op(e4,e0) = e3
| op(e4,e0) = e2 ),
inference(resolve,[status(thm)],[c_1564,c_3760]) ).
cnf(c_1595,plain,
( op(e3,e4) = e4
| op(e3,e4) = e3
| op(e3,e4) = e2
| op(e3,e4) = e0 ),
inference(resolve,[status(thm)],[c_1565,c_27]) ).
cnf(c_1596,plain,
( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 ),
inference(resolve,[status(thm)],[c_1566,c_55]) ).
cnf(c_1597,plain,
( op(e2,e4) = e4
| op(e2,e4) = e3
| op(e2,e4) = e2
| op(e2,e4) = e0 ),
inference(resolve,[status(thm)],[c_1566,c_22]) ).
cnf(c_3761,plain,
( op(e1,e4) = e1
| op(e1,e3) = e1
| op(e1,e2) = e1
| e4 = e1
| op(e1,e0) = e1 ),
inference(paramod,[status(thm)],[c_1569,c_45]) ).
cnf(c_3762,plain,
( op(e1,e4) = e1
| op(e1,e3) = e1
| op(e1,e2) = e1
| e1 = e4
| op(e1,e0) = e1 ),
inference(copy,[status(thm)],[c_3761]) ).
cnf(c_3763,plain,
( op(e1,e4) = e1
| op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e0) = e1 ),
inference(resolve,[status(thm)],[c_289,c_3762]) ).
cnf(c_1598,plain,
( op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e0) = e1 ),
inference(resolve,[status(thm)],[c_1567,c_3763]) ).
cnf(c_1599,plain,
( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2
| op(e1,e4) = e0 ),
inference(resolve,[status(thm)],[c_1567,c_17]) ).
cnf(c_3764,plain,
( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| e3 = e1 ),
inference(paramod,[status(thm)],[c_1577,c_35]) ).
cnf(c_3765,plain,
( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| e2 = e1
| e3 = e1 ),
inference(paramod,[status(thm)],[c_1578,c_3764]) ).
cnf(c_3766,plain,
( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| e2 = e1 ),
inference(resolve,[status(thm)],[c_287,c_3765]) ).
cnf(c_3767,plain,
( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1 ),
inference(resolve,[status(thm)],[c_286,c_3766]) ).
cnf(c_1600,plain,
( op(e0,e3) = e1
| op(e0,e2) = e1 ),
inference(resolve,[status(thm)],[c_1568,c_3767]) ).
cnf(c_1601,plain,
( op(e0,e4) = e4
| op(e0,e4) = e3
| op(e0,e4) = e2
| op(e0,e4) = e0 ),
inference(resolve,[status(thm)],[c_1568,c_12]) ).
cnf(c_3768,plain,
e4 != op(e1,e4),
inference(paramod,[status(thm)],[c_1569,c_221]) ).
cnf(c_1602,plain,
op(e1,e4) != e4,
inference(copy,[status(thm)],[c_3768]) ).
cnf(c_1603,plain,
op(e1,e3) != e4,
inference(paramod,[status(thm)],[c_1569,c_219]) ).
cnf(c_1607,plain,
op(e2,e1) != e4,
inference(paramod,[status(thm)],[c_1569,c_133]) ).
cnf(c_3769,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| e4 = e3
| op(e1,e0) = e3 ),
inference(paramod,[status(thm)],[c_1569,c_49]) ).
cnf(c_3770,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| e3 = e4
| op(e1,e0) = e3 ),
inference(copy,[status(thm)],[c_3769]) ).
cnf(c_1608,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e0) = e3 ),
inference(resolve,[status(thm)],[c_294,c_3770]) ).
cnf(c_3771,plain,
e3 != op(e0,e4),
inference(paramod,[status(thm)],[c_1577,c_200]) ).
cnf(c_1611,plain,
op(e0,e4) != e3,
inference(copy,[status(thm)],[c_3771]) ).
cnf(c_3772,plain,
e3 != op(e0,e3),
inference(paramod,[status(thm)],[c_1577,c_198]) ).
cnf(c_1612,plain,
op(e0,e3) != e3,
inference(copy,[status(thm)],[c_3772]) ).
cnf(c_3773,plain,
e3 != op(e0,e2),
inference(paramod,[status(thm)],[c_1577,c_196]) ).
cnf(c_1613,plain,
op(e0,e2) != e3,
inference(copy,[status(thm)],[c_3773]) ).
cnf(c_3774,plain,
e3 != op(e4,e0),
inference(paramod,[status(thm)],[c_1577,c_115]) ).
cnf(c_1614,plain,
op(e4,e0) != e3,
inference(copy,[status(thm)],[c_3774]) ).
cnf(c_3775,plain,
e3 != op(e3,e0),
inference(paramod,[status(thm)],[c_1577,c_113]) ).
cnf(c_1615,plain,
op(e3,e0) != e3,
inference(copy,[status(thm)],[c_3775]) ).
cnf(c_3776,plain,
e3 != op(e2,e0),
inference(paramod,[status(thm)],[c_1577,c_111]) ).
cnf(c_1616,plain,
op(e2,e0) != e3,
inference(copy,[status(thm)],[c_3776]) ).
cnf(c_3777,plain,
e3 != op(e1,e0),
inference(paramod,[status(thm)],[c_1577,c_109]) ).
cnf(c_1617,plain,
op(e1,e0) != e3,
inference(copy,[status(thm)],[c_3777]) ).
cnf(c_3778,plain,
op(e3,op(e0,e0)) = e0,
inference(paramod,[status(thm)],[c_1577,c_83]) ).
cnf(c_1618,plain,
op(e3,e3) = e0,
inference(paramod,[status(thm)],[c_1577,c_3778]) ).
cnf(c_3779,plain,
( op(e4,e0) = e0
| op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_1577,c_34]) ).
cnf(c_3780,plain,
( op(e4,e0) = e0
| op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| e0 = e3 ),
inference(copy,[status(thm)],[c_3779]) ).
cnf(c_3781,plain,
( op(e4,e0) = e0
| op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0 ),
inference(resolve,[status(thm)],[c_283,c_3780]) ).
cnf(c_1622,plain,
( op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0 ),
inference(resolve,[status(thm)],[c_1581,c_3781]) ).
cnf(c_3782,plain,
( op(e0,e4) = e0
| op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_1577,c_33]) ).
cnf(c_3783,plain,
( op(e0,e4) = e0
| op(e0,e3) = e0
| op(e0,e2) = e0
| e2 = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_1578,c_3782]) ).
cnf(c_3784,plain,
( op(e0,e4) = e0
| op(e0,e3) = e0
| op(e0,e2) = e0
| e2 = e0
| e0 = e3 ),
inference(copy,[status(thm)],[c_3783]) ).
cnf(c_3785,plain,
( op(e0,e4) = e0
| op(e0,e3) = e0
| op(e0,e2) = e0
| e0 = e2
| e0 = e3 ),
inference(copy,[status(thm)],[c_3784]) ).
cnf(c_3786,plain,
( op(e0,e4) = e0
| op(e0,e3) = e0
| op(e0,e2) = e0
| e0 = e2 ),
inference(resolve,[status(thm)],[c_283,c_3785]) ).
cnf(c_1623,plain,
( op(e0,e4) = e0
| op(e0,e3) = e0
| op(e0,e2) = e0 ),
inference(resolve,[status(thm)],[c_281,c_3786]) ).
cnf(c_3787,plain,
e2 != op(e0,e4),
inference(paramod,[status(thm)],[c_1578,c_204]) ).
cnf(c_1624,plain,
op(e0,e4) != e2,
inference(copy,[status(thm)],[c_3787]) ).
cnf(c_1625,plain,
op(e0,e3) != e2,
inference(paramod,[status(thm)],[c_1578,c_202]) ).
cnf(c_1626,plain,
op(e0,e2) != e2,
inference(paramod,[status(thm)],[c_1578,c_201]) ).
cnf(c_3788,plain,
e2 != op(e2,e1),
inference(paramod,[status(thm)],[c_1578,c_128]) ).
cnf(c_1628,plain,
op(e2,e1) != e2,
inference(copy,[status(thm)],[c_3788]) ).
cnf(c_1629,plain,
op(e2,op(e1,e0)) = e1,
inference(paramod,[status(thm)],[c_1578,c_88]) ).
cnf(c_1630,plain,
op(op(e1,e0),e2) = e0,
inference(paramod,[status(thm)],[c_1578,c_84]) ).
cnf(c_1631,plain,
( op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 ),
inference(resolve,[status(thm)],[c_1580,c_54]) ).
cnf(c_1633,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e0) = e0 ),
inference(resolve,[status(thm)],[c_1583,c_53]) ).
cnf(c_3789,plain,
( op(e2,e1) = e4
| op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1 ),
inference(resolve,[status(thm)],[c_1583,c_19]) ).
cnf(c_3790,plain,
( op(e2,e1) = e4
| op(e2,e1) = e3
| op(e2,e1) = e1 ),
inference(resolve,[status(thm)],[c_1628,c_3789]) ).
cnf(c_1634,plain,
( op(e2,e1) = e3
| op(e2,e1) = e1 ),
inference(resolve,[status(thm)],[c_1607,c_3790]) ).
cnf(c_1635,plain,
( op(e1,e4) = e3
| op(e1,e4) = e2
| op(e1,e4) = e0 ),
inference(resolve,[status(thm)],[c_1602,c_1599]) ).
cnf(c_1636,plain,
( op(e3,e4) = e4
| op(e2,e4) = e4
| op(e0,e4) = e4 ),
inference(resolve,[status(thm)],[c_1602,c_1570]) ).
cnf(c_1638,plain,
( op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 ),
inference(resolve,[status(thm)],[c_1603,c_16]) ).
cnf(c_3791,plain,
( op(e0,e4) = e4
| op(e0,e4) = e3
| op(e0,e4) = e0 ),
inference(resolve,[status(thm)],[c_1624,c_1601]) ).
cnf(c_1644,plain,
( op(e0,e4) = e4
| op(e0,e4) = e0 ),
inference(resolve,[status(thm)],[c_1611,c_3791]) ).
cnf(c_3792,plain,
( op(e4,e3) = e3
| e0 = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 ),
inference(paramod,[status(thm)],[c_1618,c_70]) ).
cnf(c_3793,plain,
( op(e4,e3) = e3
| e0 = e3
| op(e2,e3) = e3
| op(e1,e3) = e3 ),
inference(resolve,[status(thm)],[c_1612,c_3792]) ).
cnf(c_1646,plain,
( op(e4,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3 ),
inference(resolve,[status(thm)],[c_283,c_3793]) ).
cnf(c_3794,plain,
( op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e3) = e1
| op(e0,e3) = e0 ),
inference(resolve,[status(thm)],[c_1625,c_11]) ).
cnf(c_1647,plain,
( op(e0,e3) = e4
| op(e0,e3) = e1
| op(e0,e3) = e0 ),
inference(resolve,[status(thm)],[c_1612,c_3794]) ).
cnf(c_3795,plain,
( op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e2) = e1
| op(e0,e2) = e0 ),
inference(resolve,[status(thm)],[c_1626,c_10]) ).
cnf(c_1649,plain,
( op(e0,e2) = e4
| op(e0,e2) = e1
| op(e0,e2) = e0 ),
inference(resolve,[status(thm)],[c_1613,c_3795]) ).
cnf(c_1650,plain,
( op(e4,e0) = e4
| op(e4,e0) = e2 ),
inference(resolve,[status(thm)],[c_1614,c_1593]) ).
cnf(c_1651,plain,
( op(e4,e3) = e3
| op(e4,e2) = e3 ),
inference(resolve,[status(thm)],[c_1614,c_1573]) ).
cnf(c_3796,plain,
( op(e3,e4) = e3
| e0 = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 ),
inference(paramod,[status(thm)],[c_1618,c_69]) ).
cnf(c_3797,plain,
( op(e3,e4) = e3
| e0 = e3
| op(e3,e2) = e3
| op(e3,e1) = e3 ),
inference(resolve,[status(thm)],[c_1615,c_3796]) ).
cnf(c_1652,plain,
( op(e3,e4) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3 ),
inference(resolve,[status(thm)],[c_283,c_3797]) ).
cnf(c_1655,plain,
( op(e2,e0) = e4
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 ),
inference(resolve,[status(thm)],[c_1616,c_18]) ).
cnf(c_1656,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3 ),
inference(resolve,[status(thm)],[c_1617,c_1608]) ).
cnf(c_3798,plain,
e0 != op(e3,e4),
inference(paramod,[status(thm)],[c_1618,c_260]) ).
cnf(c_1659,plain,
op(e3,e4) != e0,
inference(copy,[status(thm)],[c_3798]) ).
cnf(c_3799,plain,
e0 != op(e3,e2),
inference(paramod,[status(thm)],[c_1618,c_256]) ).
cnf(c_1660,plain,
op(e3,e2) != e0,
inference(copy,[status(thm)],[c_3799]) ).
cnf(c_1661,plain,
op(e3,e0) != e0,
inference(paramod,[status(thm)],[c_1618,c_249]) ).
cnf(c_3800,plain,
e0 != op(e2,e3),
inference(paramod,[status(thm)],[c_1618,c_171]) ).
cnf(c_1662,plain,
op(e2,e3) != e0,
inference(copy,[status(thm)],[c_3800]) ).
cnf(c_3801,plain,
e0 != op(e1,e3),
inference(paramod,[status(thm)],[c_1618,c_168]) ).
cnf(c_1663,plain,
op(e1,e3) != e0,
inference(copy,[status(thm)],[c_3801]) ).
cnf(c_1664,plain,
op(e0,e3) != e0,
inference(paramod,[status(thm)],[c_1618,c_164]) ).
cnf(c_1669,plain,
( op(e2,e4) = e2
| op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e0) = e2 ),
inference(resolve,[status(thm)],[c_1628,c_57]) ).
cnf(c_1670,plain,
( op(e3,e4) = e4
| op(e3,e4) = e3
| op(e3,e4) = e2 ),
inference(resolve,[status(thm)],[c_1659,c_1595]) ).
cnf(c_1671,plain,
( op(e2,e4) = e0
| op(e1,e4) = e0
| op(e0,e4) = e0 ),
inference(resolve,[status(thm)],[c_1659,c_1576]) ).
cnf(c_1672,plain,
( op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 ),
inference(resolve,[status(thm)],[c_1660,c_1631]) ).
cnf(c_1675,plain,
( op(e2,e0) = e0
| op(e1,e0) = e0 ),
inference(resolve,[status(thm)],[c_1661,c_1622]) ).
cnf(c_1676,plain,
( op(e2,e4) = e0
| op(e2,e2) = e0
| op(e2,e0) = e0 ),
inference(resolve,[status(thm)],[c_1662,c_1633]) ).
cnf(c_1678,plain,
( op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1 ),
inference(resolve,[status(thm)],[c_1663,c_1638]) ).
cnf(c_1680,plain,
( op(e0,e3) = e4
| op(e0,e3) = e1 ),
inference(resolve,[status(thm)],[c_1664,c_1647]) ).
cnf(c_1681,plain,
( op(e0,e4) = e0
| op(e0,e2) = e0 ),
inference(resolve,[status(thm)],[c_1664,c_1623]) ).
cnf(c_1688,plain,
( op(e4,op(e0,e4)) = e0
| op(e4,e3) = e4
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_1571,c_87]) ).
cnf(c_1716,plain,
( op(e3,op(e1,e3)) = e1
| op(e2,e1) = e3 ),
inference(paramod,[status(thm)],[c_1586,c_91]) ).
cnf(c_1717,plain,
( op(op(e1,e3),e3) = e3
| op(e2,e1) = e3 ),
inference(paramod,[status(thm)],[c_1586,c_99]) ).
cnf(c_1744,plain,
( op(e1,op(e1,e3)) = e1
| op(e2,e1) = e1 ),
inference(paramod,[status(thm)],[c_1587,c_91]) ).
cnf(c_1762,plain,
( op(e1,op(e0,e3)) = e0
| op(e2,e0) = e1
| op(e1,e0) = e1 ),
inference(paramod,[status(thm)],[c_1592,c_86]) ).
cnf(c_1763,plain,
( op(op(e0,e3),e1) = e3
| op(e2,e0) = e1
| op(e1,e0) = e1 ),
inference(paramod,[status(thm)],[c_1592,c_98]) ).
cnf(c_1773,plain,
( op(e2,e0) != e0
| op(e2,e4) = e4
| op(e2,e4) = e3
| op(e2,e4) = e2 ),
inference(paramod,[status(thm)],[c_1597,c_234]) ).
cnf(c_3802,plain,
( e1 != op(e1,e3)
| op(e0,e2) = e1 ),
inference(paramod,[status(thm)],[c_1600,c_160]) ).
cnf(c_1779,plain,
( op(e1,e3) != e1
| op(e0,e2) = e1 ),
inference(copy,[status(thm)],[c_3802]) ).
cnf(c_1802,plain,
( op(e1,e2) = e0
| op(e1,e3) = e1
| op(e1,e2) = e1 ),
inference(paramod,[status(thm)],[c_1598,c_1630]) ).
cnf(c_1829,plain,
( op(e3,e1) != e3
| op(e2,e1) = e1 ),
inference(paramod,[status(thm)],[c_1634,c_137]) ).
cnf(c_1831,plain,
( op(e2,e3) != e3
| op(e2,e1) = e1 ),
inference(paramod,[status(thm)],[c_1634,c_236]) ).
cnf(c_3803,plain,
( op(e0,e0) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2 ),
inference(paramod,[status(thm)],[c_1635,c_1584]) ).
cnf(c_3804,plain,
( e3 = e4
| op(e1,e4) = e3
| op(e1,e4) = e2 ),
inference(paramod,[status(thm)],[c_1577,c_3803]) ).
cnf(c_1837,plain,
( op(e1,e4) = e3
| op(e1,e4) = e2 ),
inference(resolve,[status(thm)],[c_294,c_3804]) ).
cnf(c_1924,plain,
( op(e2,e0) != e2
| op(e4,e0) = e4 ),
inference(paramod,[status(thm)],[c_1650,c_122]) ).
cnf(c_1931,plain,
( op(e2,e3) != e3
| op(e4,e2) = e3 ),
inference(paramod,[status(thm)],[c_1651,c_173]) ).
cnf(c_3805,plain,
( e3 != op(e4,e2)
| op(e3,e4) = e3
| op(e3,e1) = e3 ),
inference(paramod,[status(thm)],[c_1652,c_158]) ).
cnf(c_1936,plain,
( op(e4,e2) != e3
| op(e3,e4) = e3
| op(e3,e1) = e3 ),
inference(copy,[status(thm)],[c_3805]) ).
cnf(c_2033,plain,
( op(e4,e3) != e4
| op(e2,e2) != e2
| op(e3,e1) != e3
| defn_00
| op(e2,e4) = e0
| op(e1,e4) = e0 ),
inference(resolve,[status(thm)],[c_1671,c_746]) ).
cnf(c_2099,plain,
( op(e0,op(e0,e2)) = e0
| op(e1,e0) = e0 ),
inference(paramod,[status(thm)],[c_1675,c_85]) ).
cnf(c_3806,plain,
( e0 != op(e2,e2)
| op(e1,e0) = e0 ),
inference(paramod,[status(thm)],[c_1675,c_230]) ).
cnf(c_2101,plain,
( op(e2,e2) != e0
| op(e1,e0) = e0 ),
inference(copy,[status(thm)],[c_3806]) ).
cnf(c_3807,plain,
( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| e0 = e1
| op(e2,e4) = e0
| op(e2,e2) = e0 ),
inference(paramod,[status(thm)],[c_1676,c_1596]) ).
cnf(c_2117,plain,
( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e4) = e0
| op(e2,e2) = e0 ),
inference(resolve,[status(thm)],[c_279,c_3807]) ).
cnf(c_3808,plain,
( e0 != op(e1,e2)
| op(e0,e4) = e0 ),
inference(paramod,[status(thm)],[c_1681,c_143]) ).
cnf(c_2191,plain,
( op(e1,e2) != e0
| op(e0,e4) = e0 ),
inference(copy,[status(thm)],[c_3808]) ).
cnf(c_3809,plain,
( op(e4,e0) = e0
| op(e4,e3) = e4
| op(e4,e2) = e4
| op(e0,e4) = e4 ),
inference(paramod,[status(thm)],[c_1644,c_1688]) ).
cnf(c_2202,plain,
( op(e4,e3) = e4
| op(e4,e2) = e4
| op(e0,e4) = e4 ),
inference(resolve,[status(thm)],[c_1581,c_3809]) ).
cnf(c_2209,plain,
( op(e4,e3) = e3
| op(e1,e3) = e3
| op(e2,e1) = e1 ),
inference(resolve,[status(thm)],[c_1831,c_1646]) ).
cnf(c_2210,plain,
( op(e2,e4) != e3
| op(e1,e4) = e2 ),
inference(paramod,[status(thm)],[c_1837,c_184]) ).
cnf(c_2211,plain,
( op(e3,e4) != e3
| op(e1,e4) = e2 ),
inference(paramod,[status(thm)],[c_1837,c_185]) ).
cnf(c_2214,plain,
( op(e3,e0) = e4
| op(e1,e4) = e2 ),
inference(paramod,[status(thm)],[c_1837,c_1584]) ).
cnf(c_2215,plain,
( op(e0,e3) = e1
| op(e1,e4) = e2 ),
inference(paramod,[status(thm)],[c_1837,c_1585]) ).
cnf(c_2220,plain,
( op(e2,e4) = e2
| op(e2,e3) = e2
| op(e2,e2) = e2
| op(e4,e0) = e4 ),
inference(resolve,[status(thm)],[c_1924,c_1669]) ).
cnf(c_2234,plain,
( op(e3,e4) = e4
| op(e3,e4) = e2
| op(e1,e4) = e2 ),
inference(resolve,[status(thm)],[c_2211,c_1670]) ).
cnf(c_3810,plain,
( e4 != op(e2,e0)
| op(e1,e4) = e2 ),
inference(paramod,[status(thm)],[c_2214,c_120]) ).
cnf(c_2239,plain,
( op(e2,e0) != e4
| op(e1,e4) = e2 ),
inference(copy,[status(thm)],[c_3810]) ).
cnf(c_3811,plain,
( e4 != op(e4,e0)
| op(e1,e4) = e2 ),
inference(paramod,[status(thm)],[c_2214,c_124]) ).
cnf(c_2240,plain,
( op(e4,e0) != e4
| op(e1,e4) = e2 ),
inference(copy,[status(thm)],[c_3811]) ).
cnf(c_3812,plain,
( e4 != op(e3,e4)
| op(e1,e4) = e2 ),
inference(paramod,[status(thm)],[c_2214,c_251]) ).
cnf(c_2242,plain,
( op(e3,e4) != e4
| op(e1,e4) = e2 ),
inference(copy,[status(thm)],[c_3812]) ).
cnf(c_3813,plain,
( e1 != op(e1,e3)
| op(e1,e4) = e2 ),
inference(paramod,[status(thm)],[c_2215,c_160]) ).
cnf(c_2252,plain,
( op(e1,e3) != e1
| op(e1,e4) = e2 ),
inference(copy,[status(thm)],[c_3813]) ).
cnf(c_3814,plain,
( e1 != op(e2,e3)
| op(e1,e4) = e2 ),
inference(paramod,[status(thm)],[c_2215,c_162]) ).
cnf(c_2253,plain,
( op(e2,e3) != e1
| op(e1,e4) = e2 ),
inference(copy,[status(thm)],[c_3814]) ).
cnf(c_3815,plain,
( e1 != op(e0,e2)
| op(e1,e4) = e2 ),
inference(paramod,[status(thm)],[c_2215,c_205]) ).
cnf(c_2254,plain,
( op(e0,e2) != e1
| op(e1,e4) = e2 ),
inference(copy,[status(thm)],[c_3815]) ).
cnf(c_2288,plain,
( op(e0,e2) = e1
| op(e1,e2) = e0
| op(e1,e2) = e1 ),
inference(resolve,[status(thm)],[c_1802,c_1779]) ).
cnf(c_3816,plain,
( op(e3,e3) = e1
| op(e2,e1) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1 ),
inference(paramod,[status(thm)],[c_1678,c_1716]) ).
cnf(c_3817,plain,
( e0 = e1
| op(e2,e1) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1 ),
inference(paramod,[status(thm)],[c_1618,c_3816]) ).
cnf(c_2353,plain,
( op(e2,e1) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1 ),
inference(resolve,[status(thm)],[c_279,c_3817]) ).
cnf(c_3818,plain,
( op(e4,e4) = e0
| op(e4,e3) = e4
| op(e4,e2) = e4
| op(e4,e3) = e4
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_2202,c_1688]) ).
cnf(c_3819,plain,
( e1 = e0
| op(e4,e3) = e4
| op(e4,e2) = e4
| op(e4,e3) = e4
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_296,c_3818]) ).
cnf(c_3820,plain,
( e0 = e1
| op(e4,e3) = e4
| op(e4,e2) = e4
| op(e4,e3) = e4
| op(e4,e2) = e4 ),
inference(copy,[status(thm)],[c_3819]) ).
cnf(c_3821,plain,
( e0 = e1
| op(e4,e3) = e4
| op(e4,e3) = e4
| op(e4,e2) = e4 ),
inference(copy,[status(thm)],[c_3820]) ).
cnf(c_3822,plain,
( e0 = e1
| op(e4,e3) = e4
| op(e4,e2) = e4 ),
inference(copy,[status(thm)],[c_3821]) ).
cnf(c_2414,plain,
( op(e4,e3) = e4
| op(e4,e2) = e4 ),
inference(resolve,[status(thm)],[c_279,c_3822]) ).
cnf(c_3823,plain,
( e4 = e3
| op(e4,e2) = e3
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_2414,c_1651]) ).
cnf(c_3824,plain,
( e3 = e4
| op(e4,e2) = e3
| op(e4,e2) = e4 ),
inference(copy,[status(thm)],[c_3823]) ).
cnf(c_2421,plain,
( op(e4,e2) = e3
| op(e4,e2) = e4 ),
inference(resolve,[status(thm)],[c_294,c_3824]) ).
cnf(c_2422,plain,
( op(e3,e4) = e3
| op(e3,e1) = e3
| op(e4,e2) = e4 ),
inference(resolve,[status(thm)],[c_2421,c_1936]) ).
cnf(c_2425,plain,
( op(e1,e2) != e3
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_2421,c_153]) ).
cnf(c_2499,plain,
( op(e2,e0) != e1
| op(e4,e3) = e3
| op(e1,e3) = e3 ),
inference(paramod,[status(thm)],[c_2209,c_228]) ).
cnf(c_3825,plain,
( e2 != op(e2,e4)
| op(e3,e4) = e4
| op(e1,e4) = e2 ),
inference(paramod,[status(thm)],[c_2234,c_188]) ).
cnf(c_2555,plain,
( op(e2,e4) != e2
| op(e3,e4) = e4
| op(e1,e4) = e2 ),
inference(copy,[status(thm)],[c_3825]) ).
cnf(c_3826,plain,
( op(e2,e2) = e0
| op(e1,e2) = e0
| e1 = e0
| op(e1,e2) = e0
| op(e1,e2) = e1 ),
inference(paramod,[status(thm)],[c_2288,c_1672]) ).
cnf(c_3827,plain,
( op(e2,e2) = e0
| op(e1,e2) = e0
| e0 = e1
| op(e1,e2) = e0
| op(e1,e2) = e1 ),
inference(copy,[status(thm)],[c_3826]) ).
cnf(c_3828,plain,
( op(e2,e2) = e0
| e0 = e1
| op(e1,e2) = e0
| op(e1,e2) = e1 ),
inference(copy,[status(thm)],[c_3827]) ).
cnf(c_2651,plain,
( op(e2,e2) = e0
| op(e1,e2) = e0
| op(e1,e2) = e1 ),
inference(resolve,[status(thm)],[c_279,c_3828]) ).
cnf(c_2726,plain,
( op(e2,e1) = e1
| op(e3,e4) = e3
| op(e4,e2) = e4 ),
inference(resolve,[status(thm)],[c_2422,c_1829]) ).
cnf(c_3829,plain,
( op(e1,e3) = e1
| op(e2,e1) = e1
| op(e1,e3) = e2
| op(e1,e3) = e1 ),
inference(paramod,[status(thm)],[c_1678,c_1744]) ).
cnf(c_2749,plain,
( op(e2,e1) = e1
| op(e1,e3) = e2
| op(e1,e3) = e1 ),
inference(copy,[status(thm)],[c_3829]) ).
cnf(c_3830,plain,
( op(e1,e1) = e1
| op(e2,e1) = e1
| op(e1,e2) = e0
| op(e1,e2) = e1 ),
inference(paramod,[status(thm)],[c_1802,c_1744]) ).
cnf(c_3831,plain,
( e4 = e1
| op(e2,e1) = e1
| op(e1,e2) = e0
| op(e1,e2) = e1 ),
inference(paramod,[status(thm)],[c_1569,c_3830]) ).
cnf(c_3832,plain,
( e1 = e4
| op(e2,e1) = e1
| op(e1,e2) = e0
| op(e1,e2) = e1 ),
inference(copy,[status(thm)],[c_3831]) ).
cnf(c_2750,plain,
( op(e2,e1) = e1
| op(e1,e2) = e0
| op(e1,e2) = e1 ),
inference(resolve,[status(thm)],[c_289,c_3832]) ).
cnf(c_2800,plain,
( op(e1,e0) = e0
| op(e1,e2) = e0
| op(e1,e2) = e1 ),
inference(resolve,[status(thm)],[c_2651,c_2101]) ).
cnf(c_3833,plain,
( op(e1,e1) = e0
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e3) = e4 ),
inference(paramod,[status(thm)],[c_1680,c_1762]) ).
cnf(c_3834,plain,
( e4 = e0
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e3) = e4 ),
inference(paramod,[status(thm)],[c_1569,c_3833]) ).
cnf(c_3835,plain,
( e0 = e4
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e3) = e4 ),
inference(copy,[status(thm)],[c_3834]) ).
cnf(c_2851,plain,
( op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e3) = e4 ),
inference(resolve,[status(thm)],[c_285,c_3835]) ).
cnf(c_3836,plain,
( e3 != op(e1,e4)
| op(e2,e1) = e1
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_2726,c_185]) ).
cnf(c_2895,plain,
( op(e1,e4) != e3
| op(e2,e1) = e1
| op(e4,e2) = e4 ),
inference(copy,[status(thm)],[c_3836]) ).
cnf(c_3837,plain,
( e1 = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e1 ),
inference(paramod,[status(thm)],[c_2749,c_2353]) ).
cnf(c_3838,plain,
( e3 = e1
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e1 ),
inference(copy,[status(thm)],[c_3837]) ).
cnf(c_3839,plain,
( e3 = e1
| op(e1,e3) = e2
| op(e1,e3) = e2
| op(e1,e3) = e1 ),
inference(copy,[status(thm)],[c_3838]) ).
cnf(c_3840,plain,
( e3 = e1
| op(e1,e3) = e2
| op(e1,e3) = e1 ),
inference(copy,[status(thm)],[c_3839]) ).
cnf(c_2908,plain,
( op(e1,e3) = e2
| op(e1,e3) = e1 ),
inference(resolve,[status(thm)],[c_287,c_3840]) ).
cnf(c_2911,plain,
( op(e2,e3) != e2
| op(e1,e3) = e1 ),
inference(paramod,[status(thm)],[c_2908,c_167]) ).
cnf(c_3841,plain,
( op(e1,e4) = e3
| e2 = e3
| op(e1,e2) = e3
| op(e1,e3) = e1 ),
inference(paramod,[status(thm)],[c_2908,c_1656]) ).
cnf(c_3842,plain,
( op(e1,e4) = e3
| e3 = e2
| op(e1,e2) = e3
| op(e1,e3) = e1 ),
inference(copy,[status(thm)],[c_3841]) ).
cnf(c_2916,plain,
( op(e1,e4) = e3
| op(e1,e2) = e3
| op(e1,e3) = e1 ),
inference(resolve,[status(thm)],[c_290,c_3842]) ).
cnf(c_2918,plain,
( op(e2,e3) = e3
| op(e2,e1) = e3
| op(e1,e3) = e1 ),
inference(paramod,[status(thm)],[c_2908,c_1717]) ).
cnf(c_2925,plain,
( op(e2,e0) != e1
| op(e1,e2) = e0
| op(e1,e2) = e1 ),
inference(paramod,[status(thm)],[c_2750,c_228]) ).
cnf(c_2965,plain,
( op(e2,e0) = e1
| op(e1,e2) = e0
| op(e1,e2) = e1 ),
inference(paramod,[status(thm)],[c_2800,c_1629]) ).
cnf(c_2983,plain,
( op(e2,e0) = e4
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e4) = e4
| op(e2,e4) = e3
| op(e2,e4) = e2 ),
inference(resolve,[status(thm)],[c_1773,c_1655]) ).
cnf(c_3843,plain,
( op(e4,e1) = e3
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1 ),
inference(paramod,[status(thm)],[c_2851,c_1763]) ).
cnf(c_3844,plain,
( e0 = e3
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1 ),
inference(paramod,[status(thm)],[c_1561,c_3843]) ).
cnf(c_3845,plain,
( e0 = e3
| op(e2,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1 ),
inference(copy,[status(thm)],[c_3844]) ).
cnf(c_3846,plain,
( e0 = e3
| op(e2,e0) = e1
| op(e1,e0) = e1 ),
inference(copy,[status(thm)],[c_3845]) ).
cnf(c_3002,plain,
( op(e2,e0) = e1
| op(e1,e0) = e1 ),
inference(resolve,[status(thm)],[c_283,c_3846]) ).
cnf(c_3847,plain,
( e1 != op(e2,e1)
| op(e1,e0) = e1 ),
inference(paramod,[status(thm)],[c_3002,c_228]) ).
cnf(c_3010,plain,
( op(e2,e1) != e1
| op(e1,e0) = e1 ),
inference(copy,[status(thm)],[c_3847]) ).
cnf(c_3848,plain,
( op(e1,e4) = e3
| e1 = e3
| op(e1,e2) = e3
| op(e1,e4) = e3
| op(e1,e2) = e3 ),
inference(paramod,[status(thm)],[c_2916,c_1656]) ).
cnf(c_3849,plain,
( op(e1,e4) = e3
| e3 = e1
| op(e1,e2) = e3
| op(e1,e4) = e3
| op(e1,e2) = e3 ),
inference(copy,[status(thm)],[c_3848]) ).
cnf(c_3850,plain,
( op(e1,e4) = e3
| e3 = e1
| op(e1,e4) = e3
| op(e1,e2) = e3 ),
inference(copy,[status(thm)],[c_3849]) ).
cnf(c_3851,plain,
( e3 = e1
| op(e1,e4) = e3
| op(e1,e2) = e3 ),
inference(copy,[status(thm)],[c_3850]) ).
cnf(c_3075,plain,
( op(e1,e4) = e3
| op(e1,e2) = e3 ),
inference(resolve,[status(thm)],[c_287,c_3851]) ).
cnf(c_3076,plain,
( op(e4,e2) = e4
| op(e1,e4) = e3 ),
inference(resolve,[status(thm)],[c_3075,c_2425]) ).
cnf(c_3852,plain,
( op(e2,e1) = e1
| op(e4,e2) = e4
| op(e4,e2) = e4 ),
inference(resolve,[status(thm)],[c_3076,c_2895]) ).
cnf(c_3085,plain,
( op(e2,e1) = e1
| op(e4,e2) = e4 ),
inference(copy,[status(thm)],[c_3852]) ).
cnf(c_3093,plain,
( op(e1,e0) = e1
| op(e4,e2) = e4 ),
inference(resolve,[status(thm)],[c_3085,c_3010]) ).
cnf(c_3117,plain,
( op(e1,e2) = e0
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_3093,c_1630]) ).
cnf(c_3124,plain,
( op(e0,e4) = e0
| op(e4,e2) = e4 ),
inference(resolve,[status(thm)],[c_3117,c_2191]) ).
cnf(c_3853,plain,
( e0 != op(e2,e4)
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_3124,c_179]) ).
cnf(c_3137,plain,
( op(e2,e4) != e0
| op(e4,e2) = e4 ),
inference(copy,[status(thm)],[c_3853]) ).
cnf(c_3160,plain,
( op(e4,e2) = e3
| op(e2,e1) = e3
| op(e1,e3) = e1 ),
inference(resolve,[status(thm)],[c_2918,c_1931]) ).
cnf(c_3854,plain,
( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e0
| op(e1,e2) = e1 ),
inference(resolve,[status(thm)],[c_2965,c_2925]) ).
cnf(c_3855,plain,
( op(e1,e2) = e0
| op(e1,e2) = e0
| op(e1,e2) = e1 ),
inference(copy,[status(thm)],[c_3854]) ).
cnf(c_3184,plain,
( op(e1,e2) = e0
| op(e1,e2) = e1 ),
inference(copy,[status(thm)],[c_3855]) ).
cnf(c_3186,plain,
( op(e0,e4) = e0
| op(e1,e2) = e1 ),
inference(resolve,[status(thm)],[c_3184,c_2191]) ).
cnf(c_3856,plain,
( op(e1,e4) = e3
| e0 = e3
| op(e1,e2) = e1 ),
inference(paramod,[status(thm)],[c_3184,c_3075]) ).
cnf(c_3194,plain,
( op(e1,e4) = e3
| op(e1,e2) = e1 ),
inference(resolve,[status(thm)],[c_283,c_3856]) ).
cnf(c_3857,plain,
( op(e3,e4) = e4
| op(e2,e4) = e4
| e0 = e4
| op(e1,e2) = e1 ),
inference(paramod,[status(thm)],[c_3186,c_1636]) ).
cnf(c_3212,plain,
( op(e3,e4) = e4
| op(e2,e4) = e4
| op(e1,e2) = e1 ),
inference(resolve,[status(thm)],[c_285,c_3857]) ).
cnf(c_3858,plain,
( op(e1,e4) = e3
| e1 = e3
| op(e1,e4) = e3 ),
inference(paramod,[status(thm)],[c_3194,c_3075]) ).
cnf(c_3859,plain,
( op(e1,e4) = e3
| e3 = e1
| op(e1,e4) = e3 ),
inference(copy,[status(thm)],[c_3858]) ).
cnf(c_3860,plain,
( e3 = e1
| op(e1,e4) = e3 ),
inference(copy,[status(thm)],[c_3859]) ).
cnf(c_3229,plain,
op(e1,e4) = e3,
inference(resolve,[status(thm)],[c_287,c_3860]) ).
cnf(c_3861,plain,
( op(e2,e4) != e2
| op(e3,e4) = e4
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3229,c_2555]) ).
cnf(c_3303,plain,
( op(e2,e4) != e2
| op(e3,e4) = e4 ),
inference(resolve,[status(thm)],[c_290,c_3861]) ).
cnf(c_3862,plain,
( op(e0,e2) != e1
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3229,c_2254]) ).
cnf(c_3336,plain,
op(e0,e2) != e1,
inference(resolve,[status(thm)],[c_290,c_3862]) ).
cnf(c_3863,plain,
( op(e2,e3) != e1
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3229,c_2253]) ).
cnf(c_3337,plain,
op(e2,e3) != e1,
inference(resolve,[status(thm)],[c_290,c_3863]) ).
cnf(c_3864,plain,
( op(e1,e3) != e1
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3229,c_2252]) ).
cnf(c_3338,plain,
op(e1,e3) != e1,
inference(resolve,[status(thm)],[c_290,c_3864]) ).
cnf(c_3865,plain,
( op(e3,e4) != e4
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3229,c_2242]) ).
cnf(c_3345,plain,
op(e3,e4) != e4,
inference(resolve,[status(thm)],[c_290,c_3865]) ).
cnf(c_3866,plain,
( op(e4,e0) != e4
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3229,c_2240]) ).
cnf(c_3347,plain,
op(e4,e0) != e4,
inference(resolve,[status(thm)],[c_290,c_3866]) ).
cnf(c_3867,plain,
( op(e2,e0) != e4
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3229,c_2239]) ).
cnf(c_3348,plain,
op(e2,e0) != e4,
inference(resolve,[status(thm)],[c_290,c_3867]) ).
cnf(c_3868,plain,
( op(e3,e4) = e4
| op(e3,e4) = e2
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3229,c_2234]) ).
cnf(c_3869,plain,
( op(e3,e4) = e4
| op(e3,e4) = e2 ),
inference(resolve,[status(thm)],[c_290,c_3868]) ).
cnf(c_3351,plain,
op(e3,e4) = e2,
inference(resolve,[status(thm)],[c_3345,c_3869]) ).
cnf(c_3870,plain,
( op(e2,e4) != e3
| e3 = e2 ),
inference(paramod,[status(thm)],[c_3229,c_2210]) ).
cnf(c_3358,plain,
op(e2,e4) != e3,
inference(resolve,[status(thm)],[c_290,c_3870]) ).
cnf(c_3871,plain,
( op(e4,e3) != e4
| op(e2,e2) != e2
| op(e3,e1) != e3
| defn_00
| op(e2,e4) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_3229,c_2033]) ).
cnf(c_3872,plain,
( op(e4,e3) != e4
| op(e2,e2) != e2
| op(e3,e1) != e3
| defn_00
| op(e2,e4) = e0
| e0 = e3 ),
inference(copy,[status(thm)],[c_3871]) ).
cnf(c_3369,plain,
( op(e4,e3) != e4
| op(e2,e2) != e2
| op(e3,e1) != e3
| defn_00
| op(e2,e4) = e0 ),
inference(resolve,[status(thm)],[c_283,c_3872]) ).
cnf(c_3389,plain,
( op(e0,e2) = e4
| op(e0,e2) = e0 ),
inference(resolve,[status(thm)],[c_3336,c_1649]) ).
cnf(c_3398,plain,
( op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e4) = e0
| op(e2,e2) = e0 ),
inference(resolve,[status(thm)],[c_3337,c_2117]) ).
cnf(c_3411,plain,
( op(e4,e2) = e3
| op(e2,e1) = e3 ),
inference(resolve,[status(thm)],[c_3338,c_3160]) ).
cnf(c_3422,plain,
op(e2,e3) != e2,
inference(resolve,[status(thm)],[c_3338,c_2911]) ).
cnf(c_3425,plain,
op(e1,e3) = e2,
inference(resolve,[status(thm)],[c_3338,c_2908]) ).
cnf(c_3873,plain,
( op(e2,e4) != e2
| e2 = e4 ),
inference(paramod,[status(thm)],[c_3351,c_3303]) ).
cnf(c_3428,plain,
op(e2,e4) != e2,
inference(resolve,[status(thm)],[c_292,c_3873]) ).
cnf(c_3874,plain,
( e2 = e4
| op(e2,e4) = e4
| op(e1,e2) = e1 ),
inference(paramod,[status(thm)],[c_3351,c_3212]) ).
cnf(c_3432,plain,
( op(e2,e4) = e4
| op(e1,e2) = e1 ),
inference(resolve,[status(thm)],[c_292,c_3874]) ).
cnf(c_3875,plain,
( op(e2,e4) = e2
| op(e2,e3) = e2
| op(e2,e2) = e2 ),
inference(resolve,[status(thm)],[c_3347,c_2220]) ).
cnf(c_3876,plain,
( op(e2,e4) = e2
| op(e2,e2) = e2 ),
inference(resolve,[status(thm)],[c_3422,c_3875]) ).
cnf(c_3448,plain,
op(e2,e2) = e2,
inference(resolve,[status(thm)],[c_3428,c_3876]) ).
cnf(c_3450,plain,
op(e2,e0) != e2,
inference(resolve,[status(thm)],[c_3347,c_1924]) ).
cnf(c_3877,plain,
( op(e2,e0) = e4
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e4) = e4
| op(e2,e4) = e3 ),
inference(resolve,[status(thm)],[c_3428,c_2983]) ).
cnf(c_3878,plain,
( op(e2,e0) = e4
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e4) = e4 ),
inference(resolve,[status(thm)],[c_3358,c_3877]) ).
cnf(c_3879,plain,
( op(e2,e0) = e4
| op(e2,e0) = e1
| op(e2,e4) = e4 ),
inference(resolve,[status(thm)],[c_3450,c_3878]) ).
cnf(c_3454,plain,
( op(e2,e0) = e1
| op(e2,e4) = e4 ),
inference(resolve,[status(thm)],[c_3348,c_3879]) ).
cnf(c_3880,plain,
( e2 = e3
| op(e3,e1) = e3
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_3351,c_2422]) ).
cnf(c_3881,plain,
( e3 = e2
| op(e3,e1) = e3
| op(e4,e2) = e4 ),
inference(copy,[status(thm)],[c_3880]) ).
cnf(c_3462,plain,
( op(e3,e1) = e3
| op(e4,e2) = e4 ),
inference(resolve,[status(thm)],[c_290,c_3881]) ).
cnf(c_3882,plain,
( op(e2,e0) != e1
| op(e4,e3) = e3
| e2 = e3 ),
inference(paramod,[status(thm)],[c_3425,c_2499]) ).
cnf(c_3883,plain,
( op(e2,e0) != e1
| op(e4,e3) = e3
| e3 = e2 ),
inference(copy,[status(thm)],[c_3882]) ).
cnf(c_3472,plain,
( op(e2,e0) != e1
| op(e4,e3) = e3 ),
inference(resolve,[status(thm)],[c_290,c_3883]) ).
cnf(c_3884,plain,
( op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e4) = e0
| e2 = e0 ),
inference(paramod,[status(thm)],[c_3448,c_3398]) ).
cnf(c_3885,plain,
( e2 = e1
| op(e2,e1) = e1
| op(e2,e4) = e0
| e2 = e0 ),
inference(paramod,[status(thm)],[c_3448,c_3884]) ).
cnf(c_3886,plain,
( e2 = e1
| op(e2,e1) = e1
| op(e2,e4) = e0
| e0 = e2 ),
inference(copy,[status(thm)],[c_3885]) ).
cnf(c_3887,plain,
( e2 = e1
| op(e2,e1) = e1
| op(e2,e4) = e0 ),
inference(resolve,[status(thm)],[c_281,c_3886]) ).
cnf(c_3511,plain,
( op(e2,e1) = e1
| op(e2,e4) = e0 ),
inference(resolve,[status(thm)],[c_286,c_3887]) ).
cnf(c_3888,plain,
( op(e4,e3) != e4
| e2 != e2
| op(e3,e1) != e3
| defn_00
| op(e2,e4) = e0 ),
inference(paramod,[status(thm)],[c_3448,c_3369]) ).
cnf(c_3513,plain,
( op(e4,e3) != e4
| op(e3,e1) != e3
| defn_00
| op(e2,e4) = e0 ),
inference(copy,[status(thm)],[c_3888]) ).
cnf(c_3889,negated_conjecture,
( op(e4,e3) != e3
| op(e3,e1) != e1
| e2 != e2
| op(e1,e0) != e0
| defn_10 ),
inference(paramod,[status(thm)],[c_3448,c_984]) ).
cnf(c_3523,negated_conjecture,
( op(e4,e3) != e3
| op(e3,e1) != e1
| op(e1,e0) != e0
| defn_10 ),
inference(copy,[status(thm)],[c_3889]) ).
cnf(c_3890,plain,
( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e0,e2) = e4 ),
inference(paramod,[status(thm)],[c_3389,c_2099]) ).
cnf(c_3891,plain,
( e3 = e0
| op(e1,e0) = e0
| op(e0,e2) = e4 ),
inference(paramod,[status(thm)],[c_1577,c_3890]) ).
cnf(c_3892,plain,
( e0 = e3
| op(e1,e0) = e0
| op(e0,e2) = e4 ),
inference(copy,[status(thm)],[c_3891]) ).
cnf(c_3536,plain,
( op(e1,e0) = e0
| op(e0,e2) = e4 ),
inference(resolve,[status(thm)],[c_283,c_3892]) ).
cnf(c_3542,plain,
( op(e3,op(e1,e2)) = e1
| op(e4,e2) = e3 ),
inference(paramod,[status(thm)],[c_3411,c_90]) ).
cnf(c_3548,plain,
( op(e4,op(e4,e2)) = e4
| op(e1,e2) = e1 ),
inference(paramod,[status(thm)],[c_3432,c_105]) ).
cnf(c_3572,plain,
( op(e2,e4) = e4
| op(e4,e3) = e3 ),
inference(resolve,[status(thm)],[c_3472,c_3454]) ).
cnf(c_3893,plain,
( op(e4,e2) = e3
| e1 = e3
| op(e2,e4) = e0 ),
inference(paramod,[status(thm)],[c_3511,c_3411]) ).
cnf(c_3894,plain,
( op(e4,e2) = e3
| e3 = e1
| op(e2,e4) = e0 ),
inference(copy,[status(thm)],[c_3893]) ).
cnf(c_3603,plain,
( op(e4,e2) = e3
| op(e2,e4) = e0 ),
inference(resolve,[status(thm)],[c_287,c_3894]) ).
cnf(c_3895,plain,
( e4 != op(e4,e2)
| op(e1,e0) = e0 ),
inference(paramod,[status(thm)],[c_3536,c_149]) ).
cnf(c_3615,plain,
( op(e4,e2) != e4
| op(e1,e0) = e0 ),
inference(copy,[status(thm)],[c_3895]) ).
cnf(c_3633,plain,
( op(e4,op(e4,e2)) = e4
| op(e4,e3) = e3 ),
inference(paramod,[status(thm)],[c_3572,c_105]) ).
cnf(c_3655,plain,
( op(e0,op(e4,e2)) = e4
| op(e4,e2) = e3 ),
inference(paramod,[status(thm)],[c_3603,c_105]) ).
cnf(c_3896,plain,
( op(e4,e2) = e4
| op(e4,e3) != e4
| defn_00
| op(e2,e4) = e0 ),
inference(resolve,[status(thm)],[c_3513,c_3462]) ).
cnf(c_3897,plain,
( op(e4,e2) = e4
| op(e4,e2) = e4
| defn_00
| op(e2,e4) = e0 ),
inference(resolve,[status(thm)],[c_3896,c_2414]) ).
cnf(c_3693,plain,
( op(e4,e2) = e4
| defn_00
| op(e2,e4) = e0 ),
inference(copy,[status(thm)],[c_3897]) ).
cnf(c_3898,negated_conjecture,
( op(e4,e2) = e4
| op(e2,e4) = e0
| op(e1,e0) != e1 ),
inference(resolve,[status(thm)],[c_1559,c_3693]) ).
cnf(c_3899,negated_conjecture,
( op(e4,e2) = e4
| op(e4,e2) = e4
| op(e2,e4) = e0 ),
inference(resolve,[status(thm)],[c_3898,c_3093]) ).
cnf(c_3697,negated_conjecture,
( op(e4,e2) = e4
| op(e2,e4) = e0 ),
inference(copy,[status(thm)],[c_3899]) ).
cnf(c_3900,plain,
( op(e4,e2) = e4
| op(e4,e2) = e4 ),
inference(resolve,[status(thm)],[c_3697,c_3137]) ).
cnf(c_3701,plain,
op(e4,e2) = e4,
inference(copy,[status(thm)],[c_3900]) ).
cnf(c_3901,plain,
( op(e0,op(e4,e2)) = e4
| e4 = e3 ),
inference(paramod,[status(thm)],[c_3701,c_3655]) ).
cnf(c_3902,plain,
( op(e0,e4) = e4
| e4 = e3 ),
inference(paramod,[status(thm)],[c_3701,c_3901]) ).
cnf(c_3903,plain,
( op(e0,e4) = e4
| e3 = e4 ),
inference(copy,[status(thm)],[c_3902]) ).
cnf(c_3709,plain,
op(e0,e4) = e4,
inference(resolve,[status(thm)],[c_294,c_3903]) ).
cnf(c_3904,plain,
( op(e4,e4) = e4
| op(e4,e3) = e3 ),
inference(paramod,[status(thm)],[c_3701,c_3633]) ).
cnf(c_3905,plain,
( e1 = e4
| op(e4,e3) = e3 ),
inference(paramod,[status(thm)],[c_296,c_3904]) ).
cnf(c_3712,plain,
op(e4,e3) = e3,
inference(resolve,[status(thm)],[c_289,c_3905]) ).
cnf(c_3906,plain,
( e4 != e4
| op(e1,e0) = e0 ),
inference(paramod,[status(thm)],[c_3701,c_3615]) ).
cnf(c_3716,plain,
op(e1,e0) = e0,
inference(copy,[status(thm)],[c_3906]) ).
cnf(c_3907,plain,
( op(e4,e4) = e4
| op(e1,e2) = e1 ),
inference(paramod,[status(thm)],[c_3701,c_3548]) ).
cnf(c_3908,plain,
( e1 = e4
| op(e1,e2) = e1 ),
inference(paramod,[status(thm)],[c_296,c_3907]) ).
cnf(c_3722,plain,
op(e1,e2) = e1,
inference(resolve,[status(thm)],[c_289,c_3908]) ).
cnf(c_3909,plain,
( op(e3,op(e1,e2)) = e1
| e4 = e3 ),
inference(paramod,[status(thm)],[c_3701,c_3542]) ).
cnf(c_3910,plain,
( op(e3,e1) = e1
| e4 = e3 ),
inference(paramod,[status(thm)],[c_3722,c_3909]) ).
cnf(c_3911,plain,
( op(e3,e1) = e1
| e3 = e4 ),
inference(copy,[status(thm)],[c_3910]) ).
cnf(c_3723,plain,
op(e3,e1) = e1,
inference(resolve,[status(thm)],[c_294,c_3911]) ).
cnf(c_3912,negated_conjecture,
( e4 != e4
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_3709,c_1551]) ).
cnf(c_3729,negated_conjecture,
~ defn_10,
inference(copy,[status(thm)],[c_3912]) ).
cnf(c_3913,negated_conjecture,
( op(e4,e3) != e3
| op(e3,e1) != e1
| e0 != e0
| defn_10 ),
inference(paramod,[status(thm)],[c_3716,c_3523]) ).
cnf(c_3914,negated_conjecture,
( op(e4,e3) != e3
| e1 != e1
| e0 != e0
| defn_10 ),
inference(paramod,[status(thm)],[c_3723,c_3913]) ).
cnf(c_3915,negated_conjecture,
( e3 != e3
| e1 != e1
| e0 != e0
| defn_10 ),
inference(paramod,[status(thm)],[c_3712,c_3914]) ).
cnf(c_3916,negated_conjecture,
( e3 != e3
| e1 != e1
| defn_10 ),
inference(copy,[status(thm)],[c_3915]) ).
cnf(c_3917,negated_conjecture,
( e3 != e3
| defn_10 ),
inference(copy,[status(thm)],[c_3916]) ).
cnf(c_3918,negated_conjecture,
defn_10,
inference(copy,[status(thm)],[c_3917]) ).
cnf(c_3730,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_3729,c_3918]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG170+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n020.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 21:22:33 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 2529239 was started by sandbox2 on n020,
% 0.10/0.37 % Sat Sep 26 21:22:33 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 1.55/1.80
% 1.55/1.80 % From the command line: assign(max_seconds, 300).
% 10.05/3.31
% 10.05/3.31 % given #500 (W,wt=25): 2278 op(e0,e2) = e4 | op(e0,e4) = e4 | op(e2,e2) != e1. [para(1794(c,1),145(a,1)),flip(c)].
% 10.05/3.31
% 10.05/3.31 % given #1000 (W,wt=20): 3645 op(e4,e2) = e3 | op(e2,e0) = e1. [resolve(3597,a,3456,b)].
% 10.05/3.31
% 10.05/3.31 % SZS status Theorem for theBenchmark
% 10.05/3.31
% 10.05/3.31 % Proof 1 at 1.19 (+ 0.27) seconds.
% 10.05/3.31 % Length of proof is 353.
% 10.05/3.31 % Level of proof is 23.
% 10.05/3.31 % Maximum clause weight is 40.000.
% 10.05/3.31 % Given clauses 1027.
% 10.05/3.31
% 10.05/3.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------