%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG061+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:49:22 AM UTC 2026
% Result : Theorem 5.03s 1.15s
% Output : CNFRefutation 5.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 66
% Number of leaves : 7
% Syntax : Number of formulae : 246 ( 83 unt; 0 def)
% Number of atoms : 1279 (1278 equ)
% Maximal formula atoms : 250 ( 5 avg)
% Number of connectives : 1248 ( 215 ~; 771 |; 262 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax1,axiom,
( ( op(e4,e4) = e4
| op(e4,e4) = e3
| op(e4,e4) = e2
| op(e4,e4) = e1
| op(e4,e4) = e0 )
& ( op(e4,e3) = e4
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e1
| op(e4,e3) = e0 )
& ( op(e4,e2) = e4
| op(e4,e2) = e3
| op(e4,e2) = e2
| op(e4,e2) = e1
| op(e4,e2) = e0 )
& ( op(e4,e1) = e4
| op(e4,e1) = e3
| op(e4,e1) = e2
| op(e4,e1) = e1
| op(e4,e1) = e0 )
& ( op(e4,e0) = e4
| op(e4,e0) = e3
| op(e4,e0) = e2
| op(e4,e0) = e1
| op(e4,e0) = e0 )
& ( op(e3,e4) = e4
| op(e3,e4) = e3
| op(e3,e4) = e2
| op(e3,e4) = e1
| op(e3,e4) = e0 )
& ( op(e3,e3) = e4
| op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 )
& ( op(e3,e2) = e4
| op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 )
& ( op(e3,e1) = e4
| op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 )
& ( op(e3,e0) = e4
| op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 )
& ( op(e2,e4) = e4
| op(e2,e4) = e3
| op(e2,e4) = e2
| op(e2,e4) = e1
| op(e2,e4) = e0 )
& ( op(e2,e3) = e4
| op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 )
& ( op(e2,e2) = e4
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 )
& ( op(e2,e1) = e4
| op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 )
& ( op(e2,e0) = e4
| op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 )
& ( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2
| op(e1,e4) = e1
| op(e1,e4) = e0 )
& ( op(e1,e3) = e4
| op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 )
& ( op(e1,e2) = e4
| op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 )
& ( op(e1,e1) = e4
| op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 )
& ( op(e1,e0) = e4
| op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 )
& ( op(e0,e4) = e4
| op(e0,e4) = e3
| op(e0,e4) = e2
| op(e0,e4) = e1
| op(e0,e4) = e0 )
& ( op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 )
& ( op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 )
& ( op(e0,e1) = e4
| op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 )
& ( op(e0,e0) = e4
| op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ) ),
file('theBenchmark.p',ax1) ).
fof(ax2,axiom,
( ( unit = e4
| unit = e3
| unit = e2
| unit = e1
| unit = e0 )
& op(e4,unit) = e4
& op(unit,e4) = e4
& op(e3,unit) = e3
& op(unit,e3) = e3
& op(e2,unit) = e2
& op(unit,e2) = e2
& op(e1,unit) = e1
& op(unit,e1) = e1
& op(e0,unit) = e0
& op(unit,e0) = e0 ),
file('theBenchmark.p',ax2) ).
fof(ax3,axiom,
( ( op(e4,e4) = e4
| op(e3,e4) = e4
| op(e2,e4) = e4
| op(e1,e4) = e4
| op(e0,e4) = e4 )
& ( op(e4,e4) = e4
| op(e4,e3) = e4
| op(e4,e2) = e4
| op(e4,e1) = e4
| op(e4,e0) = e4 )
& ( op(e4,e4) = e3
| op(e3,e4) = e3
| op(e2,e4) = e3
| op(e1,e4) = e3
| op(e0,e4) = e3 )
& ( op(e4,e4) = e3
| op(e4,e3) = e3
| op(e4,e2) = e3
| op(e4,e1) = e3
| op(e4,e0) = e3 )
& ( op(e4,e4) = e2
| op(e3,e4) = e2
| op(e2,e4) = e2
| op(e1,e4) = e2
| op(e0,e4) = e2 )
& ( op(e4,e4) = e2
| op(e4,e3) = e2
| op(e4,e2) = e2
| op(e4,e1) = e2
| op(e4,e0) = e2 )
& ( op(e4,e4) = e1
| op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| op(e0,e4) = e1 )
& ( op(e4,e4) = e1
| op(e4,e3) = e1
| op(e4,e2) = e1
| op(e4,e1) = e1
| op(e4,e0) = e1 )
& ( op(e4,e4) = e0
| op(e3,e4) = e0
| op(e2,e4) = e0
| op(e1,e4) = e0
| op(e0,e4) = e0 )
& ( op(e4,e4) = e0
| op(e4,e3) = e0
| op(e4,e2) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 )
& ( op(e4,e3) = e4
| op(e3,e3) = e4
| op(e2,e3) = e4
| op(e1,e3) = e4
| op(e0,e3) = e4 )
& ( op(e3,e4) = e4
| op(e3,e3) = e4
| op(e3,e2) = e4
| op(e3,e1) = e4
| op(e3,e0) = e4 )
& ( op(e4,e3) = e3
| op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 )
& ( op(e3,e4) = e3
| op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 )
& ( op(e4,e3) = e2
| op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 )
& ( op(e3,e4) = e2
| op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 )
& ( op(e4,e3) = e1
| op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 )
& ( op(e3,e4) = e1
| op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 )
& ( op(e4,e3) = e0
| op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 )
& ( op(e3,e4) = e0
| op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 )
& ( op(e4,e2) = e4
| op(e3,e2) = e4
| op(e2,e2) = e4
| op(e1,e2) = e4
| op(e0,e2) = e4 )
& ( op(e2,e4) = e4
| op(e2,e3) = e4
| op(e2,e2) = e4
| op(e2,e1) = e4
| op(e2,e0) = e4 )
& ( op(e4,e2) = e3
| op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 )
& ( op(e2,e4) = e3
| op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 )
& ( op(e4,e2) = e2
| op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 )
& ( op(e2,e4) = e2
| op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 )
& ( op(e4,e2) = e1
| op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 )
& ( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 )
& ( op(e4,e2) = e0
| op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 )
& ( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 )
& ( op(e4,e1) = e4
| op(e3,e1) = e4
| op(e2,e1) = e4
| op(e1,e1) = e4
| op(e0,e1) = e4 )
& ( op(e1,e4) = e4
| op(e1,e3) = e4
| op(e1,e2) = e4
| op(e1,e1) = e4
| op(e1,e0) = e4 )
& ( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 )
& ( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 )
& ( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 )
& ( op(e1,e4) = e2
| op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 )
& ( op(e4,e1) = e1
| op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 )
& ( op(e1,e4) = e1
| op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 )
& ( op(e4,e1) = e0
| op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 )
& ( op(e1,e4) = e0
| op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 )
& ( op(e4,e0) = e4
| op(e3,e0) = e4
| op(e2,e0) = e4
| op(e1,e0) = e4
| op(e0,e0) = e4 )
& ( op(e0,e4) = e4
| op(e0,e3) = e4
| op(e0,e2) = e4
| op(e0,e1) = e4
| op(e0,e0) = e4 )
& ( op(e4,e0) = e3
| op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 )
& ( op(e0,e4) = e3
| op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 )
& ( op(e4,e0) = e2
| op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 )
& ( op(e0,e4) = e2
| op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 )
& ( op(e4,e0) = e1
| op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 )
& ( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 )
& ( op(e4,e0) = e0
| op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 )
& ( op(e0,e4) = e0
| op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ) ),
file('theBenchmark.p',ax3) ).
fof(ax4,axiom,
( op(e4,e3) != op(e4,e4)
& op(e4,e2) != op(e4,e4)
& op(e4,e2) != op(e4,e3)
& op(e4,e1) != op(e4,e4)
& op(e4,e1) != op(e4,e3)
& op(e4,e1) != op(e4,e2)
& op(e4,e0) != op(e4,e4)
& op(e4,e0) != op(e4,e3)
& op(e4,e0) != op(e4,e2)
& op(e4,e0) != op(e4,e1)
& op(e3,e3) != op(e3,e4)
& op(e3,e2) != op(e3,e4)
& op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e4)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e4)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e3) != op(e2,e4)
& op(e2,e2) != op(e2,e4)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e4)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e4)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e3) != op(e1,e4)
& op(e1,e2) != op(e1,e4)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e4)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e4)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e3) != op(e0,e4)
& op(e0,e2) != op(e0,e4)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e4)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e4)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e3,e4) != op(e4,e4)
& op(e2,e4) != op(e4,e4)
& op(e2,e4) != op(e3,e4)
& op(e1,e4) != op(e4,e4)
& op(e1,e4) != op(e3,e4)
& op(e1,e4) != op(e2,e4)
& op(e0,e4) != op(e4,e4)
& op(e0,e4) != op(e3,e4)
& op(e0,e4) != op(e2,e4)
& op(e0,e4) != op(e1,e4)
& op(e3,e3) != op(e4,e3)
& op(e2,e3) != op(e4,e3)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e4,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e4,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e3,e2) != op(e4,e2)
& op(e2,e2) != op(e4,e2)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e4,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e4,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e3,e1) != op(e4,e1)
& op(e2,e1) != op(e4,e1)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e4,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e4,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e3,e0) != op(e4,e0)
& op(e2,e0) != op(e4,e0)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e4,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e4,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ),
file('theBenchmark.p',ax4) ).
fof(ax5,axiom,
( e3 != e4
& e2 != e4
& e2 != e3
& e1 != e4
& e1 != e3
& e1 != e2
& e0 != e4
& e0 != e3
& e0 != e2
& e0 != e1 ),
file('theBenchmark.p',ax5) ).
fof(ax6,axiom,
( e4 = op(e1,e1)
& e3 = op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1)))
& e2 = op(op(e1,e1),op(e1,e1))
& e0 = op(e1,op(op(e1,e1),op(e1,e1))) ),
file('theBenchmark.p',ax6) ).
fof(co1,conjecture,
~ ( ( ( op(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 ) )
& ( op(e4,e4) = e4
| op(e3,e3) = e4
| op(e2,e2) = e4
| op(e1,e1) = e4
| op(e0,e0) = e4 )
& ( op(e4,e4) = e3
| op(e3,e3) = e3
| op(e2,e2) = e3
| op(e1,e1) = e3
| op(e0,e0) = e3 )
& ( op(e4,e4) = e2
| op(e3,e3) = e2
| op(e2,e2) = e2
| op(e1,e1) = e2
| op(e0,e0) = e2 )
& ( op(e4,e4) = e1
| op(e3,e3) = e1
| op(e2,e2) = e1
| op(e1,e1) = e1
| op(e0,e0) = e1 )
& ( op(e4,e4) = e0
| op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) = e0 ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ~ ( ( ( op(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 ) )
& ( op(e4,e4) = e4
| op(e3,e3) = e4
| op(e2,e2) = e4
| op(e1,e1) = e4
| op(e0,e0) = e4 )
& ( op(e4,e4) = e3
| op(e3,e3) = e3
| op(e2,e2) = e3
| op(e1,e1) = e3
| op(e0,e0) = e3 )
& ( op(e4,e4) = e2
| op(e3,e3) = e2
| op(e2,e2) = e2
| op(e1,e1) = e2
| op(e0,e0) = e2 )
& ( op(e4,e4) = e1
| op(e3,e3) = e1
| op(e2,e2) = e1
| op(e1,e1) = e1
| op(e0,e0) = e1 )
& ( op(e4,e4) = e0
| op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) = e0 ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_17,plain,
( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2
| op(e1,e4) = e1
| op(e1,e4) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_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_53,plain,
( op(e4,e0) = e4
| op(e3,e0) = e4
| op(e2,e0) = e4
| op(e1,e0) = e4
| op(e0,e0) = e4 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_59,plain,
( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_61,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_64,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_72,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| op(e2,e2) = e4
| op(e2,e1) = e4
| op(e2,e0) = e4 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_74,plain,
( op(e3,e4) = e0
| op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_84,plain,
( op(e4,e4) = e0
| op(e4,e3) = e0
| op(e4,e2) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_87,plain,
( op(e4,e4) = e1
| op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| op(e0,e4) = e1 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_97,plain,
op(e3,e0) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_110,plain,
op(e2,e1) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_116,plain,
op(e1,e2) != op(e0,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_117,plain,
op(e0,e2) != op(e1,e2),
inference(copy,[status(thm)],[c_116]) ).
cnf(c_122,plain,
op(e3,e2) != op(e1,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_123,plain,
op(e4,e2) != op(e1,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_145,plain,
op(e4,e4) != op(e1,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_160,plain,
op(e1,e1) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_161,plain,
op(e1,e0) != op(e1,e1),
inference(copy,[status(thm)],[c_160]) ).
cnf(c_162,plain,
op(e1,e2) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_164,plain,
op(e1,e4) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_167,plain,
op(e1,e4) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_169,plain,
op(e1,e4) != op(e1,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_176,plain,
op(e2,e2) != op(e2,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_192,plain,
op(e3,e4) != op(e3,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_200,plain,
op(e4,e4) != op(e4,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_202,plain,
op(e4,e4) != op(e4,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_204,plain,
e1 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_205,plain,
e0 != e1,
inference(copy,[status(thm)],[c_204]) ).
cnf(c_206,plain,
e2 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_207,plain,
e3 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_208,plain,
e4 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_209,plain,
e2 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_210,plain,
e3 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_211,plain,
e4 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_212,plain,
e3 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_213,plain,
e4 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_214,plain,
e4 != e3,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_215,plain,
op(e1,op(op(e1,e1),op(e1,e1))) = e0,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_216,plain,
op(op(e1,e1),op(e1,e1)) = e2,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_217,plain,
op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1))) = e3,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_1993,plain,
op(e2,op(op(e1,e1),op(e1,e1))) = e3,
inference(paramod,[status(thm)],[c_216,c_217]) ).
cnf(c_218,plain,
op(e2,e2) = e3,
inference(paramod,[status(thm)],[c_216,c_1993]) ).
cnf(c_219,plain,
op(e1,e1) = e4,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_220,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) = e0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1994,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| op(e2,e2) = e0
| e4 = e0
| op(e0,e0) = e0 ),
inference(paramod,[status(thm)],[c_219,c_220]) ).
cnf(c_1995,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| e3 = e0
| e4 = e0
| op(e0,e0) = e0 ),
inference(paramod,[status(thm)],[c_218,c_1994]) ).
cnf(c_1996,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| e3 = e0
| op(e0,e0) = e0 ),
inference(resolve,[status(thm)],[c_208,c_1995]) ).
cnf(c_221,negated_conjecture,
( op(e4,e4) = e0
| op(e3,e3) = e0
| op(e0,e0) = e0 ),
inference(resolve,[status(thm)],[c_207,c_1996]) ).
cnf(c_222,negated_conjecture,
( op(e4,e4) = e1
| op(e3,e3) = e1
| op(e2,e2) = e1
| op(e1,e1) = e1
| op(e0,e0) = e1 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1997,negated_conjecture,
( op(e4,e4) = e1
| op(e3,e3) = e1
| op(e2,e2) = e1
| e4 = e1
| op(e0,e0) = e1 ),
inference(paramod,[status(thm)],[c_219,c_222]) ).
cnf(c_1998,negated_conjecture,
( op(e4,e4) = e1
| op(e3,e3) = e1
| e3 = e1
| e4 = e1
| op(e0,e0) = e1 ),
inference(paramod,[status(thm)],[c_218,c_1997]) ).
cnf(c_1999,negated_conjecture,
( op(e4,e4) = e1
| op(e3,e3) = e1
| e3 = e1
| op(e0,e0) = e1 ),
inference(resolve,[status(thm)],[c_211,c_1998]) ).
cnf(c_223,negated_conjecture,
( op(e4,e4) = e1
| op(e3,e3) = e1
| op(e0,e0) = e1 ),
inference(resolve,[status(thm)],[c_210,c_1999]) ).
cnf(c_307,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]) ).
cnf(c_2000,plain,
op(e1,op(e4,op(e1,e1))) = e0,
inference(paramod,[status(thm)],[c_219,c_215]) ).
cnf(c_308,plain,
op(e1,op(e4,e4)) = e0,
inference(paramod,[status(thm)],[c_219,c_2000]) ).
cnf(c_2001,plain,
e3 != op(e2,e1),
inference(paramod,[status(thm)],[c_218,c_176]) ).
cnf(c_311,plain,
op(e2,e1) != e3,
inference(copy,[status(thm)],[c_2001]) ).
cnf(c_2002,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| e3 = e4
| op(e2,e1) = e4
| op(e2,e0) = e4 ),
inference(paramod,[status(thm)],[c_218,c_72]) ).
cnf(c_2003,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| e4 = e3
| op(e2,e1) = e4
| op(e2,e0) = e4 ),
inference(copy,[status(thm)],[c_2002]) ).
cnf(c_318,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| op(e2,e1) = e4
| op(e2,e0) = e4 ),
inference(resolve,[status(thm)],[c_214,c_2003]) ).
cnf(c_2004,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| e3 = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 ),
inference(paramod,[status(thm)],[c_218,c_64]) ).
cnf(c_324,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 ),
inference(resolve,[status(thm)],[c_207,c_2004]) ).
cnf(c_2005,plain,
op(e4,op(e1,e1)) = e2,
inference(paramod,[status(thm)],[c_219,c_216]) ).
cnf(c_325,plain,
op(e4,e4) = e2,
inference(paramod,[status(thm)],[c_219,c_2005]) ).
cnf(c_326,plain,
op(e1,e4) != e4,
inference(paramod,[status(thm)],[c_219,c_167]) ).
cnf(c_329,plain,
op(e1,e0) != e4,
inference(paramod,[status(thm)],[c_219,c_161]) ).
cnf(c_332,plain,
op(e2,e1) != e4,
inference(paramod,[status(thm)],[c_219,c_110]) ).
cnf(c_2006,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| e4 = e3
| op(e0,e1) = e3 ),
inference(paramod,[status(thm)],[c_219,c_61]) ).
cnf(c_2007,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e0,e1) = e3 ),
inference(resolve,[status(thm)],[c_214,c_2006]) ).
cnf(c_334,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e0,e1) = e3 ),
inference(resolve,[status(thm)],[c_311,c_2007]) ).
cnf(c_2008,plain,
( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| e4 = e2
| op(e0,e1) = e2 ),
inference(paramod,[status(thm)],[c_219,c_59]) ).
cnf(c_336,plain,
( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| op(e0,e1) = e2 ),
inference(resolve,[status(thm)],[c_213,c_2008]) ).
cnf(c_356,plain,
op(e1,e2) = e0,
inference(paramod,[status(thm)],[c_325,c_308]) ).
cnf(c_2009,negated_conjecture,
( e2 = e1
| op(e3,e3) = e1
| op(e0,e0) = e1 ),
inference(paramod,[status(thm)],[c_325,c_223]) ).
cnf(c_357,negated_conjecture,
( op(e3,e3) = e1
| op(e0,e0) = e1 ),
inference(resolve,[status(thm)],[c_209,c_2009]) ).
cnf(c_2010,negated_conjecture,
( e2 = e0
| op(e3,e3) = e0
| op(e0,e0) = e0 ),
inference(paramod,[status(thm)],[c_325,c_221]) ).
cnf(c_358,negated_conjecture,
( op(e3,e3) = e0
| op(e0,e0) = e0 ),
inference(resolve,[status(thm)],[c_206,c_2010]) ).
cnf(c_2011,plain,
e2 != op(e4,e2),
inference(paramod,[status(thm)],[c_325,c_202]) ).
cnf(c_360,plain,
op(e4,e2) != e2,
inference(copy,[status(thm)],[c_2011]) ).
cnf(c_2012,plain,
e2 != op(e4,e1),
inference(paramod,[status(thm)],[c_325,c_200]) ).
cnf(c_361,plain,
op(e4,e1) != e2,
inference(copy,[status(thm)],[c_2012]) ).
cnf(c_2013,plain,
e2 != op(e1,e4),
inference(paramod,[status(thm)],[c_325,c_145]) ).
cnf(c_365,plain,
op(e1,e4) != e2,
inference(copy,[status(thm)],[c_2013]) ).
cnf(c_2014,plain,
( e2 = e1
| op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| op(e0,e4) = e1 ),
inference(paramod,[status(thm)],[c_325,c_87]) ).
cnf(c_369,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| op(e0,e4) = e1 ),
inference(resolve,[status(thm)],[c_209,c_2014]) ).
cnf(c_2015,plain,
( e2 = e0
| op(e4,e3) = e0
| op(e4,e2) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 ),
inference(paramod,[status(thm)],[c_325,c_84]) ).
cnf(c_372,plain,
( op(e4,e3) = e0
| op(e4,e2) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 ),
inference(resolve,[status(thm)],[c_206,c_2015]) ).
cnf(c_2016,plain,
( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e1
| op(e1,e4) = e0 ),
inference(resolve,[status(thm)],[c_365,c_17]) ).
cnf(c_373,plain,
( op(e1,e4) = e3
| op(e1,e4) = e1
| op(e1,e4) = e0 ),
inference(resolve,[status(thm)],[c_326,c_2016]) ).
cnf(c_377,plain,
( op(e4,e0) = e4
| op(e3,e0) = e4
| op(e2,e0) = e4
| op(e0,e0) = e4 ),
inference(resolve,[status(thm)],[c_329,c_53]) ).
cnf(c_382,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| op(e2,e0) = e4 ),
inference(resolve,[status(thm)],[c_332,c_318]) ).
cnf(c_405,plain,
op(e1,e4) != e0,
inference(paramod,[status(thm)],[c_356,c_169]) ).
cnf(c_2017,plain,
e0 != op(e1,e0),
inference(paramod,[status(thm)],[c_356,c_162]) ).
cnf(c_407,plain,
op(e1,e0) != e0,
inference(copy,[status(thm)],[c_2017]) ).
cnf(c_408,plain,
op(e4,e2) != e0,
inference(paramod,[status(thm)],[c_356,c_123]) ).
cnf(c_409,plain,
op(e3,e2) != e0,
inference(paramod,[status(thm)],[c_356,c_122]) ).
cnf(c_410,plain,
op(e0,e2) != e0,
inference(paramod,[status(thm)],[c_356,c_117]) ).
cnf(c_414,plain,
( op(e3,e1) = e2
| op(e2,e1) = e2
| op(e0,e1) = e2 ),
inference(resolve,[status(thm)],[c_361,c_336]) ).
cnf(c_423,plain,
( op(e1,e4) = e3
| op(e1,e4) = e1 ),
inference(resolve,[status(thm)],[c_405,c_373]) ).
cnf(c_429,plain,
( op(e4,e3) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 ),
inference(resolve,[status(thm)],[c_408,c_372]) ).
cnf(c_431,plain,
( op(e3,e4) = e0
| op(e3,e3) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(resolve,[status(thm)],[c_409,c_74]) ).
cnf(c_2018,plain,
( op(e1,e0) = e0
| unit = e4
| unit = e3
| unit = e2
| unit = e0 ),
inference(paramod,[status(thm)],[c_43,c_33]) ).
cnf(c_435,plain,
( unit = e4
| unit = e3
| unit = e2
| unit = e0 ),
inference(resolve,[status(thm)],[c_407,c_2018]) ).
cnf(c_2019,plain,
( e0 = e4
| op(e3,e0) = e4
| op(e2,e0) = e4
| op(e0,e0) = e4
| op(e4,e3) = e0
| op(e4,e1) = e0 ),
inference(paramod,[status(thm)],[c_429,c_377]) ).
cnf(c_2020,plain,
( e4 = e0
| op(e3,e0) = e4
| op(e2,e0) = e4
| op(e0,e0) = e4
| op(e4,e3) = e0
| op(e4,e1) = e0 ),
inference(copy,[status(thm)],[c_2019]) ).
cnf(c_1447,plain,
( op(e3,e0) = e4
| op(e2,e0) = e4
| op(e0,e0) = e4
| op(e4,e3) = e0
| op(e4,e1) = e0 ),
inference(resolve,[status(thm)],[c_208,c_2020]) ).
cnf(c_2021,plain,
( e0 = e1
| op(e0,e0) = e1
| op(e3,e4) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(paramod,[status(thm)],[c_431,c_357]) ).
cnf(c_1472,plain,
( op(e0,e0) = e1
| op(e3,e4) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(resolve,[status(thm)],[c_205,c_2021]) ).
cnf(c_2022,plain,
( op(e0,e2) = e0
| unit = e4
| unit = e3
| unit = e0 ),
inference(paramod,[status(thm)],[c_435,c_34]) ).
cnf(c_1529,plain,
( unit = e4
| unit = e3
| unit = e0 ),
inference(resolve,[status(thm)],[c_410,c_2022]) ).
cnf(c_2023,plain,
( op(e4,e2) = e2
| unit = e3
| unit = e0 ),
inference(paramod,[status(thm)],[c_1529,c_37]) ).
cnf(c_1563,plain,
( unit = e3
| unit = e0 ),
inference(resolve,[status(thm)],[c_360,c_2023]) ).
cnf(c_1573,plain,
( op(e0,e0) = e0
| unit = e3 ),
inference(paramod,[status(thm)],[c_1563,c_33]) ).
cnf(c_1574,plain,
( op(e3,e0) = e0
| unit = e0 ),
inference(paramod,[status(thm)],[c_1563,c_33]) ).
cnf(c_1576,plain,
( op(e0,e1) = e1
| unit = e3 ),
inference(paramod,[status(thm)],[c_1563,c_35]) ).
cnf(c_1578,plain,
( op(e1,e0) = e1
| unit = e3 ),
inference(paramod,[status(thm)],[c_1563,c_36]) ).
cnf(c_1582,plain,
( op(e2,e0) = e2
| unit = e3 ),
inference(paramod,[status(thm)],[c_1563,c_38]) ).
cnf(c_1585,plain,
( op(e3,e3) = e3
| unit = e0 ),
inference(paramod,[status(thm)],[c_1563,c_39]) ).
cnf(c_1586,plain,
( op(e3,e0) = e3
| unit = e3 ),
inference(paramod,[status(thm)],[c_1563,c_40]) ).
cnf(c_1587,plain,
( op(e0,e4) = e4
| unit = e3 ),
inference(paramod,[status(thm)],[c_1563,c_41]) ).
cnf(c_1589,plain,
( op(e4,e0) = e4
| unit = e3 ),
inference(paramod,[status(thm)],[c_1563,c_42]) ).
cnf(c_2024,plain,
( op(e3,e3) = e1
| e0 = e1
| unit = e3 ),
inference(paramod,[status(thm)],[c_1573,c_357]) ).
cnf(c_1606,plain,
( op(e3,e3) = e1
| unit = e3 ),
inference(resolve,[status(thm)],[c_205,c_2024]) ).
cnf(c_2025,plain,
( e0 != op(e0,e0)
| unit = e0 ),
inference(paramod,[status(thm)],[c_1574,c_97]) ).
cnf(c_1616,plain,
( op(e0,e0) != e0
| unit = e0 ),
inference(copy,[status(thm)],[c_2025]) ).
cnf(c_2026,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| e1 = e3
| unit = e3 ),
inference(paramod,[status(thm)],[c_1576,c_334]) ).
cnf(c_2027,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| e3 = e1
| unit = e3 ),
inference(copy,[status(thm)],[c_2026]) ).
cnf(c_1655,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| unit = e3 ),
inference(resolve,[status(thm)],[c_210,c_2027]) ).
cnf(c_2028,plain,
( op(e3,e1) = e2
| op(e2,e1) = e2
| e1 = e2
| unit = e3 ),
inference(paramod,[status(thm)],[c_1576,c_414]) ).
cnf(c_2029,plain,
( op(e3,e1) = e2
| op(e2,e1) = e2
| e2 = e1
| unit = e3 ),
inference(copy,[status(thm)],[c_2028]) ).
cnf(c_1657,plain,
( op(e3,e1) = e2
| op(e2,e1) = e2
| unit = e3 ),
inference(resolve,[status(thm)],[c_209,c_2029]) ).
cnf(c_1685,plain,
( op(e1,e4) != e1
| unit = e3 ),
inference(paramod,[status(thm)],[c_1578,c_164]) ).
cnf(c_2030,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e1) = e0
| e2 = e0
| unit = e3 ),
inference(paramod,[status(thm)],[c_1582,c_324]) ).
cnf(c_1731,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e1) = e0
| unit = e3 ),
inference(resolve,[status(thm)],[c_206,c_2030]) ).
cnf(c_2031,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| e2 = e4
| unit = e3 ),
inference(paramod,[status(thm)],[c_1582,c_382]) ).
cnf(c_2032,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| e4 = e2
| unit = e3 ),
inference(copy,[status(thm)],[c_2031]) ).
cnf(c_1732,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| unit = e3 ),
inference(resolve,[status(thm)],[c_213,c_2032]) ).
cnf(c_2033,plain,
( e3 = e0
| op(e0,e0) = e0
| unit = e0 ),
inference(paramod,[status(thm)],[c_1585,c_358]) ).
cnf(c_1765,plain,
( op(e0,e0) = e0
| unit = e0 ),
inference(resolve,[status(thm)],[c_207,c_2033]) ).
cnf(c_2034,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| e4 = e1
| unit = e3 ),
inference(paramod,[status(thm)],[c_1587,c_369]) ).
cnf(c_1783,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| unit = e3 ),
inference(resolve,[status(thm)],[c_211,c_2034]) ).
cnf(c_1822,plain,
( op(e3,e4) != e1
| unit = e3 ),
inference(paramod,[status(thm)],[c_1606,c_192]) ).
cnf(c_1848,plain,
( op(e1,e4) = e3
| unit = e3 ),
inference(resolve,[status(thm)],[c_1685,c_423]) ).
cnf(c_2035,plain,
( unit = e0
| unit = e0 ),
inference(resolve,[status(thm)],[c_1765,c_1616]) ).
cnf(c_1906,plain,
unit = e0,
inference(copy,[status(thm)],[c_2035]) ).
cnf(c_2036,plain,
( op(e0,e0) = e0
| op(e0,e0) = e0 ),
inference(paramod,[status(thm)],[c_1765,c_33]) ).
cnf(c_1907,plain,
op(e0,e0) = e0,
inference(copy,[status(thm)],[c_2036]) ).
cnf(c_2037,plain,
( op(e1,e4) = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1906,c_1848]) ).
cnf(c_2038,plain,
( op(e1,e4) = e3
| e3 = e0 ),
inference(copy,[status(thm)],[c_2037]) ).
cnf(c_1917,plain,
op(e1,e4) = e3,
inference(resolve,[status(thm)],[c_207,c_2038]) ).
cnf(c_2039,plain,
( op(e3,e4) != e1
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1906,c_1822]) ).
cnf(c_2040,plain,
( op(e3,e4) != e1
| e3 = e0 ),
inference(copy,[status(thm)],[c_2039]) ).
cnf(c_1928,plain,
op(e3,e4) != e1,
inference(resolve,[status(thm)],[c_207,c_2040]) ).
cnf(c_2041,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1906,c_1783]) ).
cnf(c_2042,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1
| e3 = e1
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1917,c_2041]) ).
cnf(c_2043,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1
| e3 = e1
| e3 = e0 ),
inference(copy,[status(thm)],[c_2042]) ).
cnf(c_2044,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1
| e3 = e1 ),
inference(resolve,[status(thm)],[c_207,c_2043]) ).
cnf(c_2045,plain,
( op(e3,e4) = e1
| op(e2,e4) = e1 ),
inference(resolve,[status(thm)],[c_210,c_2044]) ).
cnf(c_1940,plain,
op(e2,e4) = e1,
inference(resolve,[status(thm)],[c_1928,c_2045]) ).
cnf(c_2046,plain,
( op(e2,e4) = e4
| op(e2,e3) = e4
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1906,c_1732]) ).
cnf(c_2047,plain,
( e1 = e4
| op(e2,e3) = e4
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1940,c_2046]) ).
cnf(c_2048,plain,
( e1 = e4
| op(e2,e3) = e4
| e3 = e0 ),
inference(copy,[status(thm)],[c_2047]) ).
cnf(c_2049,plain,
( e4 = e1
| op(e2,e3) = e4
| e3 = e0 ),
inference(copy,[status(thm)],[c_2048]) ).
cnf(c_2050,plain,
( e4 = e1
| op(e2,e3) = e4 ),
inference(resolve,[status(thm)],[c_207,c_2049]) ).
cnf(c_1958,plain,
op(e2,e3) = e4,
inference(resolve,[status(thm)],[c_211,c_2050]) ).
cnf(c_2051,plain,
( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e1) = e0
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1906,c_1731]) ).
cnf(c_2052,plain,
( op(e2,e4) = e0
| e4 = e0
| op(e2,e1) = e0
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1958,c_2051]) ).
cnf(c_2053,plain,
( e1 = e0
| e4 = e0
| op(e2,e1) = e0
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1940,c_2052]) ).
cnf(c_2054,plain,
( e1 = e0
| e4 = e0
| op(e2,e1) = e0
| e3 = e0 ),
inference(copy,[status(thm)],[c_2053]) ).
cnf(c_2055,plain,
( e0 = e1
| e4 = e0
| op(e2,e1) = e0
| e3 = e0 ),
inference(copy,[status(thm)],[c_2054]) ).
cnf(c_2056,plain,
( e0 = e1
| e4 = e0
| op(e2,e1) = e0 ),
inference(resolve,[status(thm)],[c_207,c_2055]) ).
cnf(c_2057,plain,
( e0 = e1
| op(e2,e1) = e0 ),
inference(resolve,[status(thm)],[c_208,c_2056]) ).
cnf(c_1959,plain,
op(e2,e1) = e0,
inference(resolve,[status(thm)],[c_205,c_2057]) ).
cnf(c_2058,plain,
( op(e3,e1) = e2
| op(e2,e1) = e2
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1906,c_1657]) ).
cnf(c_2059,plain,
( op(e3,e1) = e2
| e0 = e2
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1959,c_2058]) ).
cnf(c_2060,plain,
( op(e3,e1) = e2
| e0 = e2
| e3 = e0 ),
inference(copy,[status(thm)],[c_2059]) ).
cnf(c_2061,plain,
( op(e3,e1) = e2
| e2 = e0
| e3 = e0 ),
inference(copy,[status(thm)],[c_2060]) ).
cnf(c_2062,plain,
( op(e3,e1) = e2
| e2 = e0 ),
inference(resolve,[status(thm)],[c_207,c_2061]) ).
cnf(c_1970,plain,
op(e3,e1) = e2,
inference(resolve,[status(thm)],[c_206,c_2062]) ).
cnf(c_2063,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1906,c_1655]) ).
cnf(c_2064,plain,
( op(e4,e1) = e3
| e2 = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1970,c_2063]) ).
cnf(c_2065,plain,
( op(e4,e1) = e3
| e2 = e3
| e3 = e0 ),
inference(copy,[status(thm)],[c_2064]) ).
cnf(c_2066,plain,
( op(e4,e1) = e3
| e3 = e2
| e3 = e0 ),
inference(copy,[status(thm)],[c_2065]) ).
cnf(c_2067,plain,
( op(e4,e1) = e3
| e3 = e2 ),
inference(resolve,[status(thm)],[c_207,c_2066]) ).
cnf(c_1971,plain,
op(e4,e1) = e3,
inference(resolve,[status(thm)],[c_212,c_2067]) ).
cnf(c_2068,plain,
( op(e4,e0) = e4
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1906,c_1589]) ).
cnf(c_2069,plain,
( op(e4,e0) = e4
| e3 = e0 ),
inference(copy,[status(thm)],[c_2068]) ).
cnf(c_1982,plain,
op(e4,e0) = e4,
inference(resolve,[status(thm)],[c_207,c_2069]) ).
cnf(c_2070,plain,
( op(e0,e4) = e4
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1906,c_1587]) ).
cnf(c_2071,plain,
( op(e0,e4) = e4
| e3 = e0 ),
inference(copy,[status(thm)],[c_2070]) ).
cnf(c_1983,plain,
op(e0,e4) = e4,
inference(resolve,[status(thm)],[c_207,c_2071]) ).
cnf(c_2072,plain,
( op(e3,e0) = e3
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1906,c_1586]) ).
cnf(c_2073,plain,
( op(e3,e0) = e3
| e3 = e0 ),
inference(copy,[status(thm)],[c_2072]) ).
cnf(c_1984,plain,
op(e3,e0) = e3,
inference(resolve,[status(thm)],[c_207,c_2073]) ).
cnf(c_2074,plain,
( op(e2,e0) = e2
| e0 = e3 ),
inference(paramod,[status(thm)],[c_1906,c_1582]) ).
cnf(c_2075,plain,
( op(e2,e0) = e2
| e3 = e0 ),
inference(copy,[status(thm)],[c_2074]) ).
cnf(c_1986,plain,
op(e2,e0) = e2,
inference(resolve,[status(thm)],[c_207,c_2075]) ).
cnf(c_2076,plain,
( op(e0,e0) = e1
| op(e3,e4) = e0
| op(e3,e1) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_1984,c_1472]) ).
cnf(c_2077,plain,
( op(e0,e0) = e1
| op(e3,e4) = e0
| e2 = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_1970,c_2076]) ).
cnf(c_2078,plain,
( e0 = e1
| op(e3,e4) = e0
| e2 = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_1907,c_2077]) ).
cnf(c_2079,plain,
( e0 = e1
| op(e3,e4) = e0
| e2 = e0 ),
inference(resolve,[status(thm)],[c_207,c_2078]) ).
cnf(c_2080,plain,
( e0 = e1
| op(e3,e4) = e0 ),
inference(resolve,[status(thm)],[c_206,c_2079]) ).
cnf(c_1990,plain,
op(e3,e4) = e0,
inference(resolve,[status(thm)],[c_205,c_2080]) ).
cnf(c_2081,plain,
( op(e3,e0) = e4
| op(e2,e0) = e4
| op(e0,e0) = e4
| op(e4,e3) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_1971,c_1447]) ).
cnf(c_2082,plain,
( op(e3,e0) = e4
| op(e2,e0) = e4
| e0 = e4
| op(e4,e3) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_1907,c_2081]) ).
cnf(c_2083,plain,
( op(e3,e0) = e4
| e2 = e4
| e0 = e4
| op(e4,e3) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_1986,c_2082]) ).
cnf(c_2084,plain,
( e3 = e4
| e2 = e4
| e0 = e4
| op(e4,e3) = e0
| e3 = e0 ),
inference(paramod,[status(thm)],[c_1984,c_2083]) ).
cnf(c_2085,plain,
( e3 = e4
| e2 = e4
| e4 = e0
| op(e4,e3) = e0
| e3 = e0 ),
inference(copy,[status(thm)],[c_2084]) ).
cnf(c_2086,plain,
( e3 = e4
| e4 = e2
| e4 = e0
| op(e4,e3) = e0
| e3 = e0 ),
inference(copy,[status(thm)],[c_2085]) ).
cnf(c_2087,plain,
( e4 = e3
| e4 = e2
| e4 = e0
| op(e4,e3) = e0
| e3 = e0 ),
inference(copy,[status(thm)],[c_2086]) ).
cnf(c_2088,plain,
( e4 = e3
| e4 = e2
| e4 = e0
| op(e4,e3) = e0 ),
inference(resolve,[status(thm)],[c_207,c_2087]) ).
cnf(c_2089,plain,
( e4 = e3
| e4 = e2
| op(e4,e3) = e0 ),
inference(resolve,[status(thm)],[c_208,c_2088]) ).
cnf(c_2090,plain,
( e4 = e3
| op(e4,e3) = e0 ),
inference(resolve,[status(thm)],[c_213,c_2089]) ).
cnf(c_1991,plain,
op(e4,e3) = e0,
inference(resolve,[status(thm)],[c_214,c_2090]) ).
cnf(c_2091,negated_conjecture,
( op(e4,op(e3,e4)) = e3
| op(e4,op(e2,e4)) = e2
| op(e4,op(e1,e4)) = e1
| op(e4,e4) = e0 ),
inference(paramod,[status(thm)],[c_1983,c_307]) ).
cnf(c_2092,negated_conjecture,
( op(e4,op(e3,e4)) = e3
| op(e4,op(e2,e4)) = e2
| op(e4,op(e1,e4)) = e1
| e2 = e0 ),
inference(paramod,[status(thm)],[c_325,c_2091]) ).
cnf(c_2093,negated_conjecture,
( op(e4,op(e3,e4)) = e3
| op(e4,op(e2,e4)) = e2
| op(e4,e3) = e1
| e2 = e0 ),
inference(paramod,[status(thm)],[c_1917,c_2092]) ).
cnf(c_2094,negated_conjecture,
( op(e4,op(e3,e4)) = e3
| op(e4,op(e2,e4)) = e2
| e0 = e1
| e2 = e0 ),
inference(paramod,[status(thm)],[c_1991,c_2093]) ).
cnf(c_2095,negated_conjecture,
( op(e4,op(e3,e4)) = e3
| op(e4,e1) = e2
| e0 = e1
| e2 = e0 ),
inference(paramod,[status(thm)],[c_1940,c_2094]) ).
cnf(c_2096,negated_conjecture,
( op(e4,op(e3,e4)) = e3
| e3 = e2
| e0 = e1
| e2 = e0 ),
inference(paramod,[status(thm)],[c_1971,c_2095]) ).
cnf(c_2097,negated_conjecture,
( op(e4,e0) = e3
| e3 = e2
| e0 = e1
| e2 = e0 ),
inference(paramod,[status(thm)],[c_1990,c_2096]) ).
cnf(c_2098,negated_conjecture,
( e4 = e3
| e3 = e2
| e0 = e1
| e2 = e0 ),
inference(paramod,[status(thm)],[c_1982,c_2097]) ).
cnf(c_2099,negated_conjecture,
( e4 = e3
| e3 = e2
| e0 = e1 ),
inference(resolve,[status(thm)],[c_206,c_2098]) ).
cnf(c_2100,negated_conjecture,
( e4 = e3
| e3 = e2 ),
inference(resolve,[status(thm)],[c_205,c_2099]) ).
cnf(c_2101,negated_conjecture,
e4 = e3,
inference(resolve,[status(thm)],[c_212,c_2100]) ).
cnf(c_1992,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_214,c_2101]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG061+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.09/0.35 % Computer : n006.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 21:03:55 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 2114108 was started by sandbox2 on n006,
% 0.09/0.36 % Sat Sep 26 21:03:55 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.38
% 0.12/0.38 % From the command line: assign(max_seconds, 300).
% 5.03/1.15
% 5.03/1.15 % SZS status Theorem for theBenchmark
% 5.03/1.15
% 5.03/1.15 % Proof 1 at 0.57 (+ 0.13) seconds.
% 5.03/1.15 % Length of proof is 136.
% 5.03/1.15 % Level of proof is 18.
% 5.03/1.15 % Maximum clause weight is 42.000.
% 5.03/1.15 % Given clauses 399.
% 5.03/1.15
% 5.03/1.15 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------