%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG066+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:49:23 AM UTC 2026
% Result : Theorem 7.70s 21.79s
% Output : CNFRefutation 7.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 11
% Syntax : Number of formulae : 365 ( 148 unt; 4 def)
% Number of atoms : 2710 (2625 equ)
% Maximal formula atoms : 425 ( 7 avg)
% Number of connectives : 3484 (1139 ~;1432 |; 909 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 5 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,
( e3 = op(e2,e4)
& e1 = op(e4,e2)
& e0 = op(op(e4,e2),op(e4,e2)) ),
file('theBenchmark.p',ax6) ).
fof(co1,conjecture,
~ ( ( ( ( ( e4 != unit
& op(e4,e4) = e4 )
| op(e4,e4) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e3 )
| op(e4,e3) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e2 )
| op(e4,e2) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e1 )
| op(e4,e1) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e0 )
| op(e4,e0) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e4 )
| op(e3,e4) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e3 )
| op(e3,e3) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e2 )
| op(e3,e2) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e1 )
| op(e3,e1) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e0 )
| op(e3,e0) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e4 )
| op(e2,e4) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e3 )
| op(e2,e3) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e2 )
| op(e2,e2) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e1 )
| op(e2,e1) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e0 )
| op(e2,e0) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e4 )
| op(e1,e4) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e3 )
| op(e1,e3) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e2 )
| op(e1,e2) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e1 )
| op(e1,e1) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e0 )
| op(e1,e0) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e4 )
| op(e0,e4) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e3 )
| op(e0,e3) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e2 )
| op(e0,e2) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e1 )
| op(e0,e1) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e0 )
| op(e0,e0) != e4 ) )
| ( ( ( e3 != unit
& op(e4,e3) = e4 )
| op(e4,e4) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e3 )
| op(e4,e3) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e2 )
| op(e4,e2) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e1 )
| op(e4,e1) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e0 )
| op(e4,e0) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e4 )
| op(e3,e4) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e3 )
| op(e3,e3) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e2 )
| op(e3,e2) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e1 )
| op(e3,e1) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e0 )
| op(e3,e0) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e4 )
| op(e2,e4) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e3 )
| op(e2,e3) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e2 )
| op(e2,e2) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e1 )
| op(e2,e1) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e0 )
| op(e2,e0) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e4 )
| op(e1,e4) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e3 )
| op(e1,e3) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e2 )
| op(e1,e2) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e1 )
| op(e1,e1) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e0 )
| op(e1,e0) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e4 )
| op(e0,e4) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e3 )
| op(e0,e3) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e2 )
| op(e0,e2) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e1 )
| op(e0,e1) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e0 )
| op(e0,e0) != e3 ) )
| ( ( ( e2 != unit
& op(e4,e2) = e4 )
| op(e4,e4) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e3 )
| op(e4,e3) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e2 )
| op(e4,e2) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e1 )
| op(e4,e1) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e0 )
| op(e4,e0) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e4 )
| op(e3,e4) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e3 )
| op(e3,e3) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e2 )
| op(e3,e2) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e1 )
| op(e3,e1) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e0 )
| op(e3,e0) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e4 )
| op(e2,e4) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e3 )
| op(e2,e3) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e2 )
| op(e2,e2) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e1 )
| op(e2,e1) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e0 )
| op(e2,e0) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e4 )
| op(e1,e4) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e3 )
| op(e1,e3) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e2 )
| op(e1,e2) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e1 )
| op(e1,e1) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e0 )
| op(e1,e0) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e4 )
| op(e0,e4) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e3 )
| op(e0,e3) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e2 )
| op(e0,e2) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e1 )
| op(e0,e1) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e0 )
| op(e0,e0) != e2 ) )
| ( ( ( e1 != unit
& op(e4,e1) = e4 )
| op(e4,e4) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e3 )
| op(e4,e3) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e2 )
| op(e4,e2) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e1 )
| op(e4,e1) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e0 )
| op(e4,e0) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e4 )
| op(e3,e4) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e3 )
| op(e3,e3) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e2 )
| op(e3,e2) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e1 )
| op(e3,e1) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e0 )
| op(e3,e0) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e4 )
| op(e2,e4) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e3 )
| op(e2,e3) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e2 )
| op(e2,e2) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e1 )
| op(e2,e1) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e0 )
| op(e2,e0) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e4 )
| op(e1,e4) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e3 )
| op(e1,e3) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e2 )
| op(e1,e2) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e1 )
| op(e1,e1) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e0 )
| op(e1,e0) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e4 )
| op(e0,e4) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e3 )
| op(e0,e3) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e2 )
| op(e0,e2) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e1 )
| op(e0,e1) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e0 )
| op(e0,e0) != e1 ) )
| ( ( ( e0 != unit
& op(e4,e0) = e4 )
| op(e4,e4) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e3 )
| op(e4,e3) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e2 )
| op(e4,e2) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e1 )
| op(e4,e1) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e0 )
| op(e4,e0) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e4 )
| op(e3,e4) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e3 )
| op(e3,e3) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e2 )
| op(e3,e2) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e1 )
| op(e3,e1) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e0 )
| op(e3,e0) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e4 )
| op(e2,e4) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e3 )
| op(e2,e3) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e2 )
| op(e2,e2) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e1 )
| op(e2,e1) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e0 )
| op(e2,e0) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e4 )
| op(e1,e4) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e3 )
| op(e1,e3) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e2 )
| op(e1,e2) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e1 )
| op(e1,e1) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e0 )
| op(e1,e0) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e4 )
| op(e0,e4) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e3 )
| op(e0,e3) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e2 )
| op(e0,e2) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e1 )
| op(e0,e1) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e0 )
| op(e0,e0) != e0 ) ) )
& ( op(e4,e4) = e4
| op(e4,e4) != e4 )
& ( op(e4,e3) = e4
| op(e4,e4) != e3 )
& ( op(e4,e2) = e4
| op(e4,e4) != e2 )
& ( op(e4,e1) = e4
| op(e4,e4) != e1 )
& ( op(e4,e0) = e4
| op(e4,e4) != e0 )
& ( op(e3,e4) = e3
| op(e3,e3) != e4 )
& ( op(e3,e3) = e3
| op(e3,e3) != e3 )
& ( op(e3,e2) = e3
| op(e3,e3) != e2 )
& ( op(e3,e1) = e3
| op(e3,e3) != e1 )
& ( op(e3,e0) = e3
| op(e3,e3) != e0 )
& ( op(e2,e4) = e2
| op(e2,e2) != e4 )
& ( op(e2,e3) = e2
| op(e2,e2) != e3 )
& ( op(e2,e2) = e2
| op(e2,e2) != e2 )
& ( op(e2,e1) = e2
| op(e2,e2) != e1 )
& ( op(e2,e0) = e2
| op(e2,e2) != e0 )
& ( op(e1,e4) = e1
| op(e1,e1) != e4 )
& ( op(e1,e3) = e1
| op(e1,e1) != e3 )
& ( op(e1,e2) = e1
| op(e1,e1) != e2 )
& ( op(e1,e1) = e1
| op(e1,e1) != e1 )
& ( op(e1,e0) = e1
| op(e1,e1) != e0 )
& ( op(e0,e4) = e0
| op(e0,e0) != e4 )
& ( op(e0,e3) = e0
| op(e0,e0) != e3 )
& ( op(e0,e2) = e0
| op(e0,e0) != e2 )
& ( op(e0,e1) = e0
| op(e0,e0) != e1 )
& ( op(e0,e0) = e0
| op(e0,e0) != e0 ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ~ ( ( ( ( ( e4 != unit
& op(e4,e4) = e4 )
| op(e4,e4) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e3 )
| op(e4,e3) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e2 )
| op(e4,e2) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e1 )
| op(e4,e1) != e4 )
& ( ( e4 != unit
& op(e4,e4) = e0 )
| op(e4,e0) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e4 )
| op(e3,e4) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e3 )
| op(e3,e3) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e2 )
| op(e3,e2) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e1 )
| op(e3,e1) != e4 )
& ( ( e4 != unit
& op(e3,e4) = e0 )
| op(e3,e0) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e4 )
| op(e2,e4) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e3 )
| op(e2,e3) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e2 )
| op(e2,e2) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e1 )
| op(e2,e1) != e4 )
& ( ( e4 != unit
& op(e2,e4) = e0 )
| op(e2,e0) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e4 )
| op(e1,e4) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e3 )
| op(e1,e3) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e2 )
| op(e1,e2) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e1 )
| op(e1,e1) != e4 )
& ( ( e4 != unit
& op(e1,e4) = e0 )
| op(e1,e0) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e4 )
| op(e0,e4) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e3 )
| op(e0,e3) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e2 )
| op(e0,e2) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e1 )
| op(e0,e1) != e4 )
& ( ( e4 != unit
& op(e0,e4) = e0 )
| op(e0,e0) != e4 ) )
| ( ( ( e3 != unit
& op(e4,e3) = e4 )
| op(e4,e4) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e3 )
| op(e4,e3) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e2 )
| op(e4,e2) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e1 )
| op(e4,e1) != e3 )
& ( ( e3 != unit
& op(e4,e3) = e0 )
| op(e4,e0) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e4 )
| op(e3,e4) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e3 )
| op(e3,e3) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e2 )
| op(e3,e2) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e1 )
| op(e3,e1) != e3 )
& ( ( e3 != unit
& op(e3,e3) = e0 )
| op(e3,e0) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e4 )
| op(e2,e4) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e3 )
| op(e2,e3) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e2 )
| op(e2,e2) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e1 )
| op(e2,e1) != e3 )
& ( ( e3 != unit
& op(e2,e3) = e0 )
| op(e2,e0) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e4 )
| op(e1,e4) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e3 )
| op(e1,e3) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e2 )
| op(e1,e2) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e1 )
| op(e1,e1) != e3 )
& ( ( e3 != unit
& op(e1,e3) = e0 )
| op(e1,e0) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e4 )
| op(e0,e4) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e3 )
| op(e0,e3) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e2 )
| op(e0,e2) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e1 )
| op(e0,e1) != e3 )
& ( ( e3 != unit
& op(e0,e3) = e0 )
| op(e0,e0) != e3 ) )
| ( ( ( e2 != unit
& op(e4,e2) = e4 )
| op(e4,e4) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e3 )
| op(e4,e3) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e2 )
| op(e4,e2) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e1 )
| op(e4,e1) != e2 )
& ( ( e2 != unit
& op(e4,e2) = e0 )
| op(e4,e0) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e4 )
| op(e3,e4) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e3 )
| op(e3,e3) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e2 )
| op(e3,e2) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e1 )
| op(e3,e1) != e2 )
& ( ( e2 != unit
& op(e3,e2) = e0 )
| op(e3,e0) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e4 )
| op(e2,e4) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e3 )
| op(e2,e3) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e2 )
| op(e2,e2) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e1 )
| op(e2,e1) != e2 )
& ( ( e2 != unit
& op(e2,e2) = e0 )
| op(e2,e0) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e4 )
| op(e1,e4) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e3 )
| op(e1,e3) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e2 )
| op(e1,e2) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e1 )
| op(e1,e1) != e2 )
& ( ( e2 != unit
& op(e1,e2) = e0 )
| op(e1,e0) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e4 )
| op(e0,e4) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e3 )
| op(e0,e3) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e2 )
| op(e0,e2) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e1 )
| op(e0,e1) != e2 )
& ( ( e2 != unit
& op(e0,e2) = e0 )
| op(e0,e0) != e2 ) )
| ( ( ( e1 != unit
& op(e4,e1) = e4 )
| op(e4,e4) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e3 )
| op(e4,e3) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e2 )
| op(e4,e2) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e1 )
| op(e4,e1) != e1 )
& ( ( e1 != unit
& op(e4,e1) = e0 )
| op(e4,e0) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e4 )
| op(e3,e4) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e3 )
| op(e3,e3) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e2 )
| op(e3,e2) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e1 )
| op(e3,e1) != e1 )
& ( ( e1 != unit
& op(e3,e1) = e0 )
| op(e3,e0) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e4 )
| op(e2,e4) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e3 )
| op(e2,e3) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e2 )
| op(e2,e2) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e1 )
| op(e2,e1) != e1 )
& ( ( e1 != unit
& op(e2,e1) = e0 )
| op(e2,e0) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e4 )
| op(e1,e4) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e3 )
| op(e1,e3) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e2 )
| op(e1,e2) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e1 )
| op(e1,e1) != e1 )
& ( ( e1 != unit
& op(e1,e1) = e0 )
| op(e1,e0) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e4 )
| op(e0,e4) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e3 )
| op(e0,e3) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e2 )
| op(e0,e2) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e1 )
| op(e0,e1) != e1 )
& ( ( e1 != unit
& op(e0,e1) = e0 )
| op(e0,e0) != e1 ) )
| ( ( ( e0 != unit
& op(e4,e0) = e4 )
| op(e4,e4) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e3 )
| op(e4,e3) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e2 )
| op(e4,e2) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e1 )
| op(e4,e1) != e0 )
& ( ( e0 != unit
& op(e4,e0) = e0 )
| op(e4,e0) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e4 )
| op(e3,e4) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e3 )
| op(e3,e3) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e2 )
| op(e3,e2) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e1 )
| op(e3,e1) != e0 )
& ( ( e0 != unit
& op(e3,e0) = e0 )
| op(e3,e0) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e4 )
| op(e2,e4) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e3 )
| op(e2,e3) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e2 )
| op(e2,e2) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e1 )
| op(e2,e1) != e0 )
& ( ( e0 != unit
& op(e2,e0) = e0 )
| op(e2,e0) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e4 )
| op(e1,e4) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e3 )
| op(e1,e3) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e2 )
| op(e1,e2) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e1 )
| op(e1,e1) != e0 )
& ( ( e0 != unit
& op(e1,e0) = e0 )
| op(e1,e0) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e4 )
| op(e0,e4) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e3 )
| op(e0,e3) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e2 )
| op(e0,e2) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e1 )
| op(e0,e1) != e0 )
& ( ( e0 != unit
& op(e0,e0) = e0 )
| op(e0,e0) != e0 ) ) )
& ( op(e4,e4) = e4
| op(e4,e4) != e4 )
& ( op(e4,e3) = e4
| op(e4,e4) != e3 )
& ( op(e4,e2) = e4
| op(e4,e4) != e2 )
& ( op(e4,e1) = e4
| op(e4,e4) != e1 )
& ( op(e4,e0) = e4
| op(e4,e4) != e0 )
& ( op(e3,e4) = e3
| op(e3,e3) != e4 )
& ( op(e3,e3) = e3
| op(e3,e3) != e3 )
& ( op(e3,e2) = e3
| op(e3,e3) != e2 )
& ( op(e3,e1) = e3
| op(e3,e3) != e1 )
& ( op(e3,e0) = e3
| op(e3,e3) != e0 )
& ( op(e2,e4) = e2
| op(e2,e2) != e4 )
& ( op(e2,e3) = e2
| op(e2,e2) != e3 )
& ( op(e2,e2) = e2
| op(e2,e2) != e2 )
& ( op(e2,e1) = e2
| op(e2,e2) != e1 )
& ( op(e2,e0) = e2
| op(e2,e2) != e0 )
& ( op(e1,e4) = e1
| op(e1,e1) != e4 )
& ( op(e1,e3) = e1
| op(e1,e1) != e3 )
& ( op(e1,e2) = e1
| op(e1,e1) != e2 )
& ( op(e1,e1) = e1
| op(e1,e1) != e1 )
& ( op(e1,e0) = e1
| op(e1,e1) != e0 )
& ( op(e0,e4) = e0
| op(e0,e0) != e4 )
& ( op(e0,e3) = e0
| op(e0,e0) != e3 )
& ( op(e0,e2) = e0
| op(e0,e0) != e2 )
& ( op(e0,e1) = e0
| op(e0,e0) != e1 )
& ( op(e0,e0) = 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_29,plain,
( op(e4,e1) = e4
| op(e4,e1) = e3
| op(e4,e1) = e2
| op(e4,e1) = e1
| op(e4,e1) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_32,plain,
( op(e4,e4) = e4
| op(e4,e4) = e3
| op(e4,e4) = e2
| op(e4,e4) = e1
| op(e4,e4) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
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_39,plain,
op(unit,e3) = e3,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_41,plain,
op(unit,e4) = e4,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_42,plain,
op(e4,unit) = e4,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_43,plain,
( unit = e4
| unit = e3
| unit = e2
| unit = e1
| unit = e0 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_60,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_62,plain,
( op(e1,e4) = e4
| op(e1,e3) = e4
| op(e1,e2) = e4
| op(e1,e1) = e4
| op(e1,e0) = e4 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_66,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_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_89,plain,
( op(e4,e4) = e2
| op(e3,e4) = e2
| op(e2,e4) = e2
| op(e1,e4) = e2
| op(e0,e4) = e2 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_90,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)],[ax3]) ).
cnf(c_100,plain,
op(e2,e0) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_101,plain,
op(e1,e0) != op(e2,e0),
inference(copy,[status(thm)],[c_100]) ).
cnf(c_111,plain,
op(e2,e1) != op(e0,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_112,plain,
op(e0,e1) != op(e2,e1),
inference(copy,[status(thm)],[c_111]) ).
cnf(c_119,plain,
op(e4,e1) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_120,plain,
op(e1,e1) != op(e4,e1),
inference(copy,[status(thm)],[c_119]) ).
cnf(c_138,plain,
op(e4,e2) != op(e2,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_139,plain,
op(e2,e2) != op(e4,e2),
inference(copy,[status(thm)],[c_138]) ).
cnf(c_142,plain,
op(e1,e3) != op(e0,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_146,plain,
op(e4,e3) != op(e0,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_147,plain,
op(e0,e3) != op(e4,e3),
inference(copy,[status(thm)],[c_146]) ).
cnf(c_164,plain,
op(e2,e4) != op(e1,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_165,plain,
op(e1,e4) != op(e2,e4),
inference(copy,[status(thm)],[c_164]) ).
cnf(c_170,plain,
op(e4,e4) != op(e2,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_171,plain,
op(e2,e4) != op(e4,e4),
inference(copy,[status(thm)],[c_170]) ).
cnf(c_193,plain,
op(e1,e3) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_194,plain,
op(e1,e4) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_195,plain,
op(e1,e0) != op(e1,e4),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_199,plain,
op(e1,e4) != op(e1,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_200,plain,
op(e1,e1) != op(e1,e4),
inference(copy,[status(thm)],[c_199]) ).
cnf(c_215,plain,
op(e2,e4) != op(e2,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_216,plain,
op(e2,e1) != op(e2,e4),
inference(copy,[status(thm)],[c_215]) ).
cnf(c_238,plain,
op(e4,e1) != op(e4,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_242,plain,
op(e4,e4) != op(e4,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_243,plain,
op(e4,e0) != op(e4,e4),
inference(copy,[status(thm)],[c_242]) ).
cnf(c_244,plain,
op(e4,e2) != op(e4,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_245,plain,
op(e4,e1) != op(e4,e2),
inference(copy,[status(thm)],[c_244]) ).
cnf(c_249,plain,
op(e4,e3) != op(e4,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_250,plain,
op(e4,e4) != op(e4,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_251,plain,
op(e4,e2) != op(e4,e4),
inference(copy,[status(thm)],[c_250]) ).
cnf(c_254,plain,
e1 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_257,plain,
e3 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_258,plain,
e4 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_259,plain,
e0 != e4,
inference(copy,[status(thm)],[c_258]) ).
cnf(c_260,plain,
e2 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_261,plain,
e1 != e2,
inference(copy,[status(thm)],[c_260]) ).
cnf(c_262,plain,
e3 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_263,plain,
e4 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_264,plain,
e1 != e4,
inference(copy,[status(thm)],[c_263]) ).
cnf(c_265,plain,
e3 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_266,plain,
e4 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_267,plain,
e2 != e4,
inference(copy,[status(thm)],[c_266]) ).
cnf(c_268,plain,
e4 != e3,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_269,plain,
e3 != e4,
inference(copy,[status(thm)],[c_268]) ).
cnf(c_270,plain,
op(op(e4,e2),op(e4,e2)) = e0,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_271,plain,
e0 = op(op(e4,e2),op(e4,e2)),
inference(copy,[status(thm)],[c_270]) ).
cnf(c_272,plain,
op(e4,e2) = e1,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_273,plain,
e1 = op(e4,e2),
inference(copy,[status(thm)],[c_272]) ).
cnf(c_274,plain,
op(e2,e4) = e3,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_275,plain,
e3 = op(e2,e4),
inference(copy,[status(thm)],[c_274]) ).
cnf(c_284,negated_conjecture,
( op(e1,e0) = e1
| op(e1,e1) != e0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1405,negated_conjecture,
( op(e1,e0) = e1
| op(op(e4,e2),e1) != e0 ),
inference(paramod,[status(thm)],[c_273,c_284]) ).
cnf(c_1406,negated_conjecture,
( op(e1,e0) = e1
| op(op(e4,e2),op(e4,e2)) != e0 ),
inference(paramod,[status(thm)],[c_273,c_1405]) ).
cnf(c_1407,negated_conjecture,
( op(e1,e0) = e1
| op(op(e4,e2),op(e4,e2)) != op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_271,c_1406]) ).
cnf(c_1408,negated_conjecture,
( op(op(e4,e2),e0) = e1
| op(op(e4,e2),op(e4,e2)) != op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_273,c_1407]) ).
cnf(c_1409,negated_conjecture,
( op(op(e4,e2),op(op(e4,e2),op(e4,e2))) = e1
| op(op(e4,e2),op(e4,e2)) != op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_271,c_1408]) ).
cnf(c_1410,negated_conjecture,
( op(op(e4,e2),op(op(e4,e2),op(e4,e2))) = op(e4,e2)
| op(op(e4,e2),op(e4,e2)) != op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_273,c_1409]) ).
cnf(c_285,negated_conjecture,
op(op(e4,e2),op(op(e4,e2),op(e4,e2))) = op(e4,e2),
inference(copy,[status(thm)],[c_1410]) ).
cnf(c_308,negated_conjecture,
( op(e4,e2) = e4
| op(e4,e4) != e2 ),
inference(clausify,[status(thm)],[co1_neg]) ).
fof(def_defn_00,definition,
( defn_00
<=> ( ( unit != e0
| op(e4,e4) != e0 )
& ( op(e4,e0) = e4
| op(e4,e4) != e0 )
& ( unit != e0
| op(e4,e3) != e0 )
& ( op(e4,e0) = e3
| op(e4,e3) != e0 )
& ( unit != e0
| op(e4,e2) != e0 )
& ( op(e4,e0) = e2
| op(e4,e2) != e0 )
& ( unit != e0
| op(e4,e1) != e0 )
& ( op(e4,e0) = e1
| op(e4,e1) != e0 )
& ( unit != e0
| op(e4,e0) != e0 )
& ( unit != e0
| op(e3,e4) != e0 )
& ( op(e3,e0) = e4
| op(e3,e4) != e0 )
& ( unit != e0
| op(e3,e3) != e0 )
& ( op(e3,e0) = e3
| op(e3,e3) != e0 )
& ( unit != e0
| op(e3,e2) != e0 )
& ( op(e3,e0) = e2
| op(e3,e2) != e0 )
& ( unit != e0
| op(e3,e1) != e0 )
& ( op(e3,e0) = e1
| op(e3,e1) != e0 )
& ( unit != e0
| op(e3,e0) != e0 )
& ( unit != e0
| op(e2,e4) != e0 )
& ( op(e2,e0) = e4
| op(e2,e4) != e0 )
& ( unit != e0
| op(e2,e3) != e0 )
& ( op(e2,e0) = e3
| op(e2,e3) != e0 )
& ( unit != e0
| op(e2,e2) != e0 )
& ( op(e2,e0) = e2
| op(e2,e2) != e0 )
& ( unit != e0
| op(e2,e1) != e0 )
& ( op(e2,e0) = e1
| op(e2,e1) != e0 )
& ( unit != e0
| op(e2,e0) != e0 )
& ( unit != e0
| op(e1,e4) != e0 )
& ( op(e1,e0) = e4
| op(e1,e4) != e0 )
& ( unit != e0
| op(e1,e3) != e0 )
& ( op(e1,e0) = e3
| op(e1,e3) != e0 )
& ( unit != e0
| op(e1,e2) != e0 )
& ( op(e1,e0) = e2
| op(e1,e2) != e0 )
& ( unit != e0
| op(e1,e1) != e0 )
& ( op(e1,e0) = e1
| op(e1,e1) != e0 )
& ( unit != e0
| op(e1,e0) != e0 )
& ( unit != e0
| op(e0,e4) != e0 )
& ( op(e0,e0) = e4
| op(e0,e4) != e0 )
& ( unit != e0
| op(e0,e3) != e0 )
& ( op(e0,e0) = e3
| op(e0,e3) != e0 )
& ( unit != e0
| op(e0,e2) != e0 )
& ( op(e0,e0) = e2
| op(e0,e2) != e0 )
& ( unit != e0
| op(e0,e1) != e0 )
& ( op(e0,e0) = e1
| op(e0,e1) != e0 )
& ( unit != e0
| op(e0,e0) != e0 ) ) ),
introduced(definition,[new_symbols(definition,[defn_00])],[]) ).
fof(def_defn_10,definition,
( defn_10
<=> ( ( unit != e1
| op(e4,e4) != e1 )
& ( op(e4,e1) = e4
| op(e4,e4) != e1 )
& ( unit != e1
| op(e4,e3) != e1 )
& ( op(e4,e1) = e3
| op(e4,e3) != e1 )
& ( unit != e1
| op(e4,e2) != e1 )
& ( op(e4,e1) = e2
| op(e4,e2) != e1 )
& ( unit != e1
| op(e4,e1) != e1 )
& ( unit != e1
| op(e4,e0) != e1 )
& ( op(e4,e1) = e0
| op(e4,e0) != e1 )
& ( unit != e1
| op(e3,e4) != e1 )
& ( op(e3,e1) = e4
| op(e3,e4) != e1 )
& ( unit != e1
| op(e3,e3) != e1 )
& ( op(e3,e1) = e3
| op(e3,e3) != e1 )
& ( unit != e1
| op(e3,e2) != e1 )
& ( op(e3,e1) = e2
| op(e3,e2) != e1 )
& ( unit != e1
| op(e3,e1) != e1 )
& ( unit != e1
| op(e3,e0) != e1 )
& ( op(e3,e1) = e0
| op(e3,e0) != e1 )
& ( unit != e1
| op(e2,e4) != e1 )
& ( op(e2,e1) = e4
| op(e2,e4) != e1 )
& ( unit != e1
| op(e2,e3) != e1 )
& ( op(e2,e1) = e3
| op(e2,e3) != e1 )
& ( unit != e1
| op(e2,e2) != e1 )
& ( op(e2,e1) = e2
| op(e2,e2) != e1 )
& ( unit != e1
| op(e2,e1) != e1 )
& ( unit != e1
| op(e2,e0) != e1 )
& ( op(e2,e1) = e0
| op(e2,e0) != e1 )
& ( unit != e1
| op(e1,e4) != e1 )
& ( op(e1,e1) = e4
| op(e1,e4) != e1 )
& ( unit != e1
| op(e1,e3) != e1 )
& ( op(e1,e1) = e3
| op(e1,e3) != e1 )
& ( unit != e1
| op(e1,e2) != e1 )
& ( op(e1,e1) = e2
| op(e1,e2) != e1 )
& ( unit != e1
| op(e1,e1) != e1 )
& ( unit != e1
| op(e1,e0) != e1 )
& ( op(e1,e1) = e0
| op(e1,e0) != e1 )
& ( unit != e1
| op(e0,e4) != e1 )
& ( op(e0,e1) = e4
| op(e0,e4) != e1 )
& ( unit != e1
| op(e0,e3) != e1 )
& ( op(e0,e1) = e3
| op(e0,e3) != e1 )
& ( unit != e1
| op(e0,e2) != e1 )
& ( op(e0,e1) = e2
| op(e0,e2) != e1 )
& ( unit != e1
| op(e0,e1) != e1 )
& ( unit != e1
| op(e0,e0) != e1 )
& ( op(e0,e1) = e0
| op(e0,e0) != e1 ) ) ),
introduced(definition,[new_symbols(definition,[defn_10])],[]) ).
fof(def_defn_20,definition,
( defn_20
<=> ( ( unit != e2
| op(e4,e4) != e2 )
& ( op(e4,e2) = e4
| op(e4,e4) != e2 )
& ( unit != e2
| op(e4,e3) != e2 )
& ( op(e4,e2) = e3
| op(e4,e3) != e2 )
& ( unit != e2
| op(e4,e2) != e2 )
& ( unit != e2
| op(e4,e1) != e2 )
& ( op(e4,e2) = e1
| op(e4,e1) != e2 )
& ( unit != e2
| op(e4,e0) != e2 )
& ( op(e4,e2) = e0
| op(e4,e0) != e2 )
& ( unit != e2
| op(e3,e4) != e2 )
& ( op(e3,e2) = e4
| op(e3,e4) != e2 )
& ( unit != e2
| op(e3,e3) != e2 )
& ( op(e3,e2) = e3
| op(e3,e3) != e2 )
& ( unit != e2
| op(e3,e2) != e2 )
& ( unit != e2
| op(e3,e1) != e2 )
& ( op(e3,e2) = e1
| op(e3,e1) != e2 )
& ( unit != e2
| op(e3,e0) != e2 )
& ( op(e3,e2) = e0
| op(e3,e0) != e2 )
& ( unit != e2
| op(e2,e4) != e2 )
& ( op(e2,e2) = e4
| op(e2,e4) != e2 )
& ( unit != e2
| op(e2,e3) != e2 )
& ( op(e2,e2) = e3
| op(e2,e3) != e2 )
& ( unit != e2
| op(e2,e2) != e2 )
& ( unit != e2
| op(e2,e1) != e2 )
& ( op(e2,e2) = e1
| op(e2,e1) != e2 )
& ( unit != e2
| op(e2,e0) != e2 )
& ( op(e2,e2) = e0
| op(e2,e0) != e2 )
& ( unit != e2
| op(e1,e4) != e2 )
& ( op(e1,e2) = e4
| op(e1,e4) != e2 )
& ( unit != e2
| op(e1,e3) != e2 )
& ( op(e1,e2) = e3
| op(e1,e3) != e2 )
& ( unit != e2
| op(e1,e2) != e2 )
& ( unit != e2
| op(e1,e1) != e2 )
& ( op(e1,e2) = e1
| op(e1,e1) != e2 )
& ( unit != e2
| op(e1,e0) != e2 )
& ( op(e1,e2) = e0
| op(e1,e0) != e2 )
& ( unit != e2
| op(e0,e4) != e2 )
& ( op(e0,e2) = e4
| op(e0,e4) != e2 )
& ( unit != e2
| op(e0,e3) != e2 )
& ( op(e0,e2) = e3
| op(e0,e3) != e2 )
& ( unit != e2
| op(e0,e2) != e2 )
& ( unit != e2
| op(e0,e1) != e2 )
& ( op(e0,e2) = e1
| op(e0,e1) != e2 )
& ( unit != e2
| op(e0,e0) != e2 )
& ( op(e0,e2) = e0
| op(e0,e0) != e2 ) ) ),
introduced(definition,[new_symbols(definition,[defn_20])],[]) ).
fof(def_defn_30,definition,
( defn_30
<=> ( ( unit != e3
| op(e4,e4) != e3 )
& ( op(e4,e3) = e4
| op(e4,e4) != e3 )
& ( unit != e3
| op(e4,e3) != e3 )
& ( unit != e3
| op(e4,e2) != e3 )
& ( op(e4,e3) = e2
| op(e4,e2) != e3 )
& ( unit != e3
| op(e4,e1) != e3 )
& ( op(e4,e3) = e1
| op(e4,e1) != e3 )
& ( unit != e3
| op(e4,e0) != e3 )
& ( op(e4,e3) = e0
| op(e4,e0) != e3 )
& ( unit != e3
| op(e3,e4) != e3 )
& ( op(e3,e3) = e4
| op(e3,e4) != e3 )
& ( unit != e3
| op(e3,e3) != e3 )
& ( unit != e3
| op(e3,e2) != e3 )
& ( op(e3,e3) = e2
| op(e3,e2) != e3 )
& ( unit != e3
| op(e3,e1) != e3 )
& ( op(e3,e3) = e1
| op(e3,e1) != e3 )
& ( unit != e3
| op(e3,e0) != e3 )
& ( op(e3,e3) = e0
| op(e3,e0) != e3 )
& ( unit != e3
| op(e2,e4) != e3 )
& ( op(e2,e3) = e4
| op(e2,e4) != e3 )
& ( unit != e3
| op(e2,e3) != e3 )
& ( unit != e3
| op(e2,e2) != e3 )
& ( op(e2,e3) = e2
| op(e2,e2) != e3 )
& ( unit != e3
| op(e2,e1) != e3 )
& ( op(e2,e3) = e1
| op(e2,e1) != e3 )
& ( unit != e3
| op(e2,e0) != e3 )
& ( op(e2,e3) = e0
| op(e2,e0) != e3 )
& ( unit != e3
| op(e1,e4) != e3 )
& ( op(e1,e3) = e4
| op(e1,e4) != e3 )
& ( unit != e3
| op(e1,e3) != e3 )
& ( unit != e3
| op(e1,e2) != e3 )
& ( op(e1,e3) = e2
| op(e1,e2) != e3 )
& ( unit != e3
| op(e1,e1) != e3 )
& ( op(e1,e3) = e1
| op(e1,e1) != e3 )
& ( unit != e3
| op(e1,e0) != e3 )
& ( op(e1,e3) = e0
| op(e1,e0) != e3 )
& ( unit != e3
| op(e0,e4) != e3 )
& ( op(e0,e3) = e4
| op(e0,e4) != e3 )
& ( unit != e3
| op(e0,e3) != e3 )
& ( unit != e3
| op(e0,e2) != e3 )
& ( op(e0,e3) = e2
| op(e0,e2) != e3 )
& ( unit != e3
| op(e0,e1) != e3 )
& ( op(e0,e3) = e1
| op(e0,e1) != e3 )
& ( unit != e3
| op(e0,e0) != e3 )
& ( op(e0,e3) = e0
| op(e0,e0) != e3 ) ) ),
introduced(definition,[new_symbols(definition,[defn_30])],[]) ).
cnf(c_336,negated_conjecture,
( op(e1,e4) = e3
| op(e1,e3) != e4
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00,def_defn_10,def_defn_20,def_defn_30]) ).
cnf(c_1411,negated_conjecture,
( op(e1,e4) = e3
| op(op(e4,e2),e3) != e4
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_273,c_336]) ).
cnf(c_1412,negated_conjecture,
( op(e1,e4) = e3
| op(op(e4,e2),op(e2,e4)) != e4
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_275,c_1411]) ).
cnf(c_1413,negated_conjecture,
( op(op(e4,e2),e4) = e3
| op(op(e4,e2),op(e2,e4)) != e4
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_273,c_1412]) ).
cnf(c_337,negated_conjecture,
( op(op(e4,e2),e4) = op(e2,e4)
| op(op(e4,e2),op(e2,e4)) != e4
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_275,c_1413]) ).
cnf(c_393,negated_conjecture,
( op(e4,e3) = e1
| op(e4,e1) != e3
| ~ defn_30 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_30]) ).
cnf(c_1414,negated_conjecture,
( op(e4,e3) = e1
| op(e4,op(e4,e2)) != e3
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_273,c_393]) ).
cnf(c_1415,negated_conjecture,
( op(e4,e3) = e1
| op(e4,op(e4,e2)) != op(e2,e4)
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_275,c_1414]) ).
cnf(c_1416,negated_conjecture,
( op(e4,op(e2,e4)) = e1
| op(e4,op(e4,e2)) != op(e2,e4)
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_275,c_1415]) ).
cnf(c_1417,negated_conjecture,
( op(e4,op(e2,e4)) = op(e4,e2)
| op(e4,op(e4,e2)) != op(e2,e4)
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_273,c_1416]) ).
cnf(c_394,negated_conjecture,
( op(e4,op(e2,e4)) = op(e4,e2)
| op(e2,e4) != op(e4,op(e4,e2))
| ~ defn_30 ),
inference(copy,[status(thm)],[c_1417]) ).
cnf(c_501,negated_conjecture,
( op(e1,e2) = e4
| op(e1,e4) != e2
| ~ defn_20 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_20]) ).
cnf(c_1418,negated_conjecture,
( op(e1,e2) = e4
| op(op(e4,e2),e4) != e2
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_273,c_501]) ).
cnf(c_502,negated_conjecture,
( op(op(e4,e2),e2) = e4
| op(op(e4,e2),e4) != e2
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_273,c_1418]) ).
cnf(c_562,negated_conjecture,
( op(e2,e1) = e3
| op(e2,e3) != e1
| ~ defn_10 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_10]) ).
cnf(c_1419,negated_conjecture,
( op(e2,e1) = e3
| op(e2,op(e2,e4)) != e1
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_275,c_562]) ).
cnf(c_1420,negated_conjecture,
( op(e2,e1) = e3
| op(e2,op(e2,e4)) != op(e4,e2)
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_273,c_1419]) ).
cnf(c_1421,negated_conjecture,
( op(e2,op(e4,e2)) = e3
| op(e2,op(e2,e4)) != op(e4,e2)
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_273,c_1420]) ).
cnf(c_563,negated_conjecture,
( op(e2,op(e4,e2)) = op(e2,e4)
| op(e2,op(e2,e4)) != op(e4,e2)
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_275,c_1421]) ).
cnf(c_657,negated_conjecture,
( unit != e0
| op(e1,e1) != e0
| ~ defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00]) ).
cnf(c_1422,negated_conjecture,
( unit != e0
| op(op(e4,e2),e1) != e0
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_273,c_657]) ).
cnf(c_1423,negated_conjecture,
( unit != e0
| op(op(e4,e2),op(e4,e2)) != e0
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_273,c_1422]) ).
cnf(c_1424,negated_conjecture,
( unit != e0
| op(op(e4,e2),op(e4,e2)) != op(op(e4,e2),op(e4,e2))
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_271,c_1423]) ).
cnf(c_1425,negated_conjecture,
( unit != op(op(e4,e2),op(e4,e2))
| op(op(e4,e2),op(e4,e2)) != op(op(e4,e2),op(e4,e2))
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_271,c_1424]) ).
cnf(c_1426,negated_conjecture,
( op(op(e4,e2),op(e4,e2)) != unit
| op(op(e4,e2),op(e4,e2)) != op(op(e4,e2),op(e4,e2))
| ~ defn_00 ),
inference(copy,[status(thm)],[c_1425]) ).
cnf(c_658,negated_conjecture,
( op(op(e4,e2),op(e4,e2)) != unit
| ~ defn_00 ),
inference(copy,[status(thm)],[c_1426]) ).
cnf(c_674,plain,
op(op(e4,e2),op(e4,e2)) != e4,
inference(paramod,[status(thm)],[c_271,c_259]) ).
cnf(c_1427,plain,
op(e2,e4) != e0,
inference(paramod,[status(thm)],[c_275,c_257]) ).
cnf(c_1428,plain,
op(e2,e4) != op(op(e4,e2),op(e4,e2)),
inference(paramod,[status(thm)],[c_271,c_1427]) ).
cnf(c_675,plain,
op(op(e4,e2),op(e4,e2)) != op(e2,e4),
inference(copy,[status(thm)],[c_1428]) ).
cnf(c_1429,plain,
op(e4,e2) != e0,
inference(paramod,[status(thm)],[c_273,c_254]) ).
cnf(c_1430,plain,
op(e4,e2) != op(op(e4,e2),op(e4,e2)),
inference(paramod,[status(thm)],[c_271,c_1429]) ).
cnf(c_677,plain,
op(op(e4,e2),op(e4,e2)) != op(e4,e2),
inference(copy,[status(thm)],[c_1430]) ).
cnf(c_678,plain,
op(e4,op(op(e4,e2),op(e4,e2))) != op(e4,e4),
inference(paramod,[status(thm)],[c_271,c_243]) ).
cnf(c_1431,plain,
op(e4,op(e4,e2)) != op(e4,e0),
inference(paramod,[status(thm)],[c_273,c_238]) ).
cnf(c_1432,plain,
op(e4,op(e4,e2)) != op(e4,op(op(e4,e2),op(e4,e2))),
inference(paramod,[status(thm)],[c_271,c_1431]) ).
cnf(c_681,plain,
op(e4,op(op(e4,e2),op(e4,e2))) != op(e4,op(e4,e2)),
inference(copy,[status(thm)],[c_1432]) ).
cnf(c_1433,plain,
op(op(e4,e2),e0) != op(e1,e4),
inference(paramod,[status(thm)],[c_273,c_195]) ).
cnf(c_1434,plain,
op(op(e4,e2),op(op(e4,e2),op(e4,e2))) != op(e1,e4),
inference(paramod,[status(thm)],[c_271,c_1433]) ).
cnf(c_1435,plain,
op(e4,e2) != op(e1,e4),
inference(paramod,[status(thm)],[c_285,c_1434]) ).
cnf(c_1436,plain,
op(e4,e2) != op(op(e4,e2),e4),
inference(paramod,[status(thm)],[c_273,c_1435]) ).
cnf(c_690,plain,
op(op(e4,e2),e4) != op(e4,e2),
inference(copy,[status(thm)],[c_1436]) ).
cnf(c_1437,plain,
op(op(e4,e2),e3) != op(e1,e0),
inference(paramod,[status(thm)],[c_273,c_193]) ).
cnf(c_1438,plain,
op(op(e4,e2),op(e2,e4)) != op(e1,e0),
inference(paramod,[status(thm)],[c_275,c_1437]) ).
cnf(c_1439,plain,
op(op(e4,e2),op(e2,e4)) != op(op(e4,e2),e0),
inference(paramod,[status(thm)],[c_273,c_1438]) ).
cnf(c_1440,plain,
op(op(e4,e2),op(e2,e4)) != op(op(e4,e2),op(op(e4,e2),op(e4,e2))),
inference(paramod,[status(thm)],[c_271,c_1439]) ).
cnf(c_691,plain,
op(op(e4,e2),op(e2,e4)) != op(e4,e2),
inference(paramod,[status(thm)],[c_285,c_1440]) ).
cnf(c_1441,plain,
op(op(op(e4,e2),op(e4,e2)),e3) != op(e4,e3),
inference(paramod,[status(thm)],[c_271,c_147]) ).
cnf(c_1442,plain,
op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) != op(e4,e3),
inference(paramod,[status(thm)],[c_275,c_1441]) ).
cnf(c_707,plain,
op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) != op(e4,op(e2,e4)),
inference(paramod,[status(thm)],[c_275,c_1442]) ).
cnf(c_1443,plain,
op(op(e4,e2),e3) != op(e0,e3),
inference(paramod,[status(thm)],[c_273,c_142]) ).
cnf(c_1444,plain,
op(op(e4,e2),op(e2,e4)) != op(e0,e3),
inference(paramod,[status(thm)],[c_275,c_1443]) ).
cnf(c_1445,plain,
op(op(e4,e2),op(e2,e4)) != op(op(op(e4,e2),op(e4,e2)),e3),
inference(paramod,[status(thm)],[c_271,c_1444]) ).
cnf(c_1446,plain,
op(op(e4,e2),op(e2,e4)) != op(op(op(e4,e2),op(e4,e2)),op(e2,e4)),
inference(paramod,[status(thm)],[c_275,c_1445]) ).
cnf(c_710,plain,
op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) != op(op(e4,e2),op(e2,e4)),
inference(copy,[status(thm)],[c_1446]) ).
cnf(c_1447,plain,
op(op(op(e4,e2),op(e4,e2)),e1) != op(e2,e1),
inference(paramod,[status(thm)],[c_271,c_112]) ).
cnf(c_1448,plain,
op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) != op(e2,e1),
inference(paramod,[status(thm)],[c_273,c_1447]) ).
cnf(c_717,plain,
op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) != op(e2,op(e4,e2)),
inference(paramod,[status(thm)],[c_273,c_1448]) ).
cnf(c_1449,plain,
op(op(e4,e2),e0) != op(e2,e0),
inference(paramod,[status(thm)],[c_273,c_101]) ).
cnf(c_1450,plain,
op(op(e4,e2),op(op(e4,e2),op(e4,e2))) != op(e2,e0),
inference(paramod,[status(thm)],[c_271,c_1449]) ).
cnf(c_1451,plain,
op(e4,e2) != op(e2,e0),
inference(paramod,[status(thm)],[c_285,c_1450]) ).
cnf(c_1452,plain,
op(e4,e2) != op(e2,op(op(e4,e2),op(e4,e2))),
inference(paramod,[status(thm)],[c_271,c_1451]) ).
cnf(c_723,plain,
op(e2,op(op(e4,e2),op(e4,e2))) != op(e4,e2),
inference(copy,[status(thm)],[c_1452]) ).
cnf(c_1453,plain,
( op(e4,e4) = e3
| op(e4,e3) = e3
| op(e4,e2) = e3
| op(e4,e1) = e3
| op(e4,op(op(e4,e2),op(e4,e2))) = e3 ),
inference(paramod,[status(thm)],[c_271,c_90]) ).
cnf(c_1454,plain,
( op(e4,e4) = e3
| op(e4,e3) = e3
| op(e4,e2) = e3
| op(e4,e1) = e3
| op(e4,op(op(e4,e2),op(e4,e2))) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_275,c_1453]) ).
cnf(c_1455,plain,
( op(e4,e4) = e3
| op(e4,e3) = e3
| op(e4,e2) = e3
| op(e4,op(e4,e2)) = e3
| op(e4,op(op(e4,e2),op(e4,e2))) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_273,c_1454]) ).
cnf(c_1456,plain,
( op(e4,e4) = e3
| op(e4,e3) = e3
| op(e4,e2) = e3
| op(e4,op(e4,e2)) = op(e2,e4)
| op(e4,op(op(e4,e2),op(e4,e2))) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_275,c_1455]) ).
cnf(c_1457,plain,
( op(e4,e4) = e3
| op(e4,e3) = e3
| op(e4,e2) = op(e2,e4)
| op(e4,op(e4,e2)) = op(e2,e4)
| op(e4,op(op(e4,e2),op(e4,e2))) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_275,c_1456]) ).
cnf(c_1458,plain,
( op(e4,e4) = e3
| op(e4,op(e2,e4)) = e3
| op(e4,e2) = op(e2,e4)
| op(e4,op(e4,e2)) = op(e2,e4)
| op(e4,op(op(e4,e2),op(e4,e2))) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_275,c_1457]) ).
cnf(c_1459,plain,
( op(e4,e4) = e3
| op(e4,op(e2,e4)) = op(e2,e4)
| op(e4,e2) = op(e2,e4)
| op(e4,op(e4,e2)) = op(e2,e4)
| op(e4,op(op(e4,e2),op(e4,e2))) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_275,c_1458]) ).
cnf(c_1460,plain,
( op(e4,e4) = op(e2,e4)
| op(e4,op(e2,e4)) = op(e2,e4)
| op(e4,e2) = op(e2,e4)
| op(e4,op(e4,e2)) = op(e2,e4)
| op(e4,op(op(e4,e2),op(e4,e2))) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_275,c_1459]) ).
cnf(c_1461,plain,
( op(e4,e4) = op(e2,e4)
| op(e4,op(e2,e4)) = op(e2,e4)
| op(e4,e2) = op(e2,e4)
| op(e2,e4) = op(e4,op(e4,e2))
| op(e4,op(op(e4,e2),op(e4,e2))) = op(e2,e4) ),
inference(copy,[status(thm)],[c_1460]) ).
cnf(c_1462,plain,
( op(e4,e4) = op(e2,e4)
| op(e4,op(e2,e4)) = op(e2,e4)
| op(e2,e4) = op(e4,e2)
| op(e2,e4) = op(e4,op(e4,e2))
| op(e4,op(op(e4,e2),op(e4,e2))) = op(e2,e4) ),
inference(copy,[status(thm)],[c_1461]) ).
cnf(c_1463,plain,
( op(e2,e4) = op(e4,e4)
| op(e4,op(e2,e4)) = op(e2,e4)
| op(e2,e4) = op(e4,e2)
| op(e2,e4) = op(e4,op(e4,e2))
| op(e4,op(op(e4,e2),op(e4,e2))) = op(e2,e4) ),
inference(copy,[status(thm)],[c_1462]) ).
cnf(c_730,plain,
( op(e4,op(e2,e4)) = op(e2,e4)
| op(e2,e4) = op(e4,e2)
| op(e2,e4) = op(e4,op(e4,e2))
| op(e4,op(op(e4,e2),op(e4,e2))) = op(e2,e4) ),
inference(resolve,[status(thm)],[c_171,c_1463]) ).
cnf(c_1464,plain,
( op(e4,e4) = e2
| op(e3,e4) = e2
| op(e2,e4) = e2
| op(e1,e4) = e2
| op(op(op(e4,e2),op(e4,e2)),e4) = e2 ),
inference(paramod,[status(thm)],[c_271,c_89]) ).
cnf(c_1465,plain,
( op(e4,e4) = e2
| op(e3,e4) = e2
| op(e2,e4) = e2
| op(op(e4,e2),e4) = e2
| op(op(op(e4,e2),op(e4,e2)),e4) = e2 ),
inference(paramod,[status(thm)],[c_273,c_1464]) ).
cnf(c_731,plain,
( op(e4,e4) = e2
| op(op(e2,e4),e4) = e2
| op(e2,e4) = e2
| op(op(e4,e2),e4) = e2
| op(op(op(e4,e2),op(e4,e2)),e4) = e2 ),
inference(paramod,[status(thm)],[c_275,c_1465]) ).
cnf(c_1466,plain,
( op(e4,e4) = e1
| op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| op(op(op(e4,e2),op(e4,e2)),e4) = e1 ),
inference(paramod,[status(thm)],[c_271,c_87]) ).
cnf(c_1467,plain,
( op(e4,e4) = e1
| op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_273,c_1466]) ).
cnf(c_1468,plain,
( op(e4,e4) = e1
| op(e3,e4) = e1
| op(e2,e4) = e1
| op(op(e4,e2),e4) = e1
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_273,c_1467]) ).
cnf(c_1469,plain,
( op(e4,e4) = e1
| op(e3,e4) = e1
| op(e2,e4) = e1
| op(op(e4,e2),e4) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_273,c_1468]) ).
cnf(c_1470,plain,
( op(e4,e4) = e1
| op(e3,e4) = e1
| op(e2,e4) = op(e4,e2)
| op(op(e4,e2),e4) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_273,c_1469]) ).
cnf(c_1471,plain,
( op(e4,e4) = e1
| op(op(e2,e4),e4) = e1
| op(e2,e4) = op(e4,e2)
| op(op(e4,e2),e4) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_275,c_1470]) ).
cnf(c_1472,plain,
( op(e4,e4) = e1
| op(op(e2,e4),e4) = op(e4,e2)
| op(e2,e4) = op(e4,e2)
| op(op(e4,e2),e4) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_273,c_1471]) ).
cnf(c_1473,plain,
( op(e4,e4) = op(e4,e2)
| op(op(e2,e4),e4) = op(e4,e2)
| op(e2,e4) = op(e4,e2)
| op(op(e4,e2),e4) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_273,c_1472]) ).
cnf(c_1474,plain,
( op(e4,e2) = op(e4,e4)
| op(op(e2,e4),e4) = op(e4,e2)
| op(e2,e4) = op(e4,e2)
| op(op(e4,e2),e4) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2) ),
inference(copy,[status(thm)],[c_1473]) ).
cnf(c_1475,plain,
( op(e4,e2) = op(e4,e4)
| op(op(e2,e4),e4) = op(e4,e2)
| op(e2,e4) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2) ),
inference(resolve,[status(thm)],[c_690,c_1474]) ).
cnf(c_733,plain,
( op(op(e2,e4),e4) = op(e4,e2)
| op(e2,e4) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2) ),
inference(resolve,[status(thm)],[c_251,c_1475]) ).
cnf(c_1476,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,op(op(e4,e2),op(e4,e2))) = e1 ),
inference(paramod,[status(thm)],[c_271,c_66]) ).
cnf(c_1477,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_273,c_1476]) ).
cnf(c_1478,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,op(e4,e2)) = e1
| op(e2,op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_273,c_1477]) ).
cnf(c_1479,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,op(e4,e2)) = op(e4,e2)
| op(e2,op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_273,c_1478]) ).
cnf(c_1480,plain,
( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e2) = op(e4,e2)
| op(e2,op(e4,e2)) = op(e4,e2)
| op(e2,op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_273,c_1479]) ).
cnf(c_1481,plain,
( op(e2,e4) = e1
| op(e2,op(e2,e4)) = e1
| op(e2,e2) = op(e4,e2)
| op(e2,op(e4,e2)) = op(e4,e2)
| op(e2,op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_275,c_1480]) ).
cnf(c_1482,plain,
( op(e2,e4) = e1
| op(e2,op(e2,e4)) = op(e4,e2)
| op(e2,e2) = op(e4,e2)
| op(e2,op(e4,e2)) = op(e4,e2)
| op(e2,op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_273,c_1481]) ).
cnf(c_1483,plain,
( op(e2,e4) = op(e4,e2)
| op(e2,op(e2,e4)) = op(e4,e2)
| op(e2,e2) = op(e4,e2)
| op(e2,op(e4,e2)) = op(e4,e2)
| op(e2,op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_273,c_1482]) ).
cnf(c_1484,plain,
( op(e2,e4) = op(e4,e2)
| op(e2,op(e2,e4)) = op(e4,e2)
| op(e2,e2) = op(e4,e2)
| op(e2,op(e4,e2)) = op(e4,e2) ),
inference(resolve,[status(thm)],[c_723,c_1483]) ).
cnf(c_751,plain,
( op(e2,e4) = op(e4,e2)
| op(e2,op(e2,e4)) = op(e4,e2)
| op(e2,op(e4,e2)) = op(e4,e2) ),
inference(resolve,[status(thm)],[c_139,c_1484]) ).
cnf(c_1485,plain,
( op(e1,e4) = e4
| op(e1,e3) = e4
| op(e1,e2) = e4
| op(e1,e1) = e4
| op(op(e4,e2),e0) = e4 ),
inference(paramod,[status(thm)],[c_273,c_62]) ).
cnf(c_1486,plain,
( op(e1,e4) = e4
| op(e1,e3) = e4
| op(e1,e2) = e4
| op(e1,e1) = e4
| op(op(e4,e2),op(op(e4,e2),op(e4,e2))) = e4 ),
inference(paramod,[status(thm)],[c_271,c_1485]) ).
cnf(c_1487,plain,
( op(e1,e4) = e4
| op(e1,e3) = e4
| op(e1,e2) = e4
| op(e1,e1) = e4
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_285,c_1486]) ).
cnf(c_1488,plain,
( op(e1,e4) = e4
| op(e1,e3) = e4
| op(e1,e2) = e4
| op(op(e4,e2),e1) = e4
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_273,c_1487]) ).
cnf(c_1489,plain,
( op(e1,e4) = e4
| op(e1,e3) = e4
| op(e1,e2) = e4
| op(op(e4,e2),op(e4,e2)) = e4
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_273,c_1488]) ).
cnf(c_1490,plain,
( op(e1,e4) = e4
| op(e1,e3) = e4
| op(op(e4,e2),e2) = e4
| op(op(e4,e2),op(e4,e2)) = e4
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_273,c_1489]) ).
cnf(c_1491,plain,
( op(e1,e4) = e4
| op(op(e4,e2),e3) = e4
| op(op(e4,e2),e2) = e4
| op(op(e4,e2),op(e4,e2)) = e4
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_273,c_1490]) ).
cnf(c_1492,plain,
( op(e1,e4) = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(op(e4,e2),e2) = e4
| op(op(e4,e2),op(e4,e2)) = e4
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_275,c_1491]) ).
cnf(c_1493,plain,
( op(op(e4,e2),e4) = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(op(e4,e2),e2) = e4
| op(op(e4,e2),op(e4,e2)) = e4
| op(e4,e2) = e4 ),
inference(paramod,[status(thm)],[c_273,c_1492]) ).
cnf(c_755,plain,
( op(op(e4,e2),e4) = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(op(e4,e2),e2) = e4
| op(e4,e2) = e4 ),
inference(resolve,[status(thm)],[c_674,c_1493]) ).
cnf(c_1494,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(op(e4,e2),e0) = e3 ),
inference(paramod,[status(thm)],[c_273,c_60]) ).
cnf(c_1495,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(op(e4,e2),op(op(e4,e2),op(e4,e2))) = e3 ),
inference(paramod,[status(thm)],[c_271,c_1494]) ).
cnf(c_1496,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e4,e2) = e3 ),
inference(paramod,[status(thm)],[c_285,c_1495]) ).
cnf(c_1497,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e4,e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_275,c_1496]) ).
cnf(c_1498,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(op(e4,e2),e1) = e3
| op(e4,e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_273,c_1497]) ).
cnf(c_1499,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(op(e4,e2),op(e4,e2)) = e3
| op(e4,e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_273,c_1498]) ).
cnf(c_1500,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(e4,e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_275,c_1499]) ).
cnf(c_1501,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(op(e4,e2),e2) = e3
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(e4,e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_273,c_1500]) ).
cnf(c_1502,plain,
( op(e1,e4) = e3
| op(e1,e3) = e3
| op(op(e4,e2),e2) = op(e2,e4)
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(e4,e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_275,c_1501]) ).
cnf(c_1503,plain,
( op(e1,e4) = e3
| op(op(e4,e2),e3) = e3
| op(op(e4,e2),e2) = op(e2,e4)
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(e4,e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_273,c_1502]) ).
cnf(c_1504,plain,
( op(e1,e4) = e3
| op(op(e4,e2),op(e2,e4)) = e3
| op(op(e4,e2),e2) = op(e2,e4)
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(e4,e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_275,c_1503]) ).
cnf(c_1505,plain,
( op(e1,e4) = e3
| op(op(e4,e2),op(e2,e4)) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(e4,e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_275,c_1504]) ).
cnf(c_1506,plain,
( op(op(e4,e2),e4) = e3
| op(op(e4,e2),op(e2,e4)) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(e4,e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_273,c_1505]) ).
cnf(c_1507,plain,
( op(op(e4,e2),e4) = op(e2,e4)
| op(op(e4,e2),op(e2,e4)) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(e4,e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_275,c_1506]) ).
cnf(c_1508,plain,
( op(op(e4,e2),e4) = op(e2,e4)
| op(op(e4,e2),op(e2,e4)) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(e2,e4) = op(e4,e2) ),
inference(copy,[status(thm)],[c_1507]) ).
cnf(c_757,plain,
( op(op(e4,e2),e4) = op(e2,e4)
| op(op(e4,e2),op(e2,e4)) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(e2,e4) = op(e4,e2) ),
inference(resolve,[status(thm)],[c_675,c_1508]) ).
cnf(c_1509,plain,
( unit = e4
| unit = e3
| unit = e2
| unit = e1
| unit = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_271,c_43]) ).
cnf(c_1510,plain,
( unit = e4
| unit = e3
| unit = e2
| unit = op(e4,e2)
| unit = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_273,c_1509]) ).
cnf(c_1511,plain,
( unit = e4
| unit = op(e2,e4)
| unit = e2
| unit = op(e4,e2)
| unit = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_275,c_1510]) ).
cnf(c_1512,plain,
( unit = e4
| unit = op(e2,e4)
| unit = e2
| unit = op(e4,e2)
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(copy,[status(thm)],[c_1511]) ).
cnf(c_1513,plain,
( unit = e4
| unit = op(e2,e4)
| unit = e2
| op(e4,e2) = unit
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(copy,[status(thm)],[c_1512]) ).
cnf(c_770,plain,
( unit = e4
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(copy,[status(thm)],[c_1513]) ).
cnf(c_1514,plain,
( op(e4,e4) = e4
| op(e4,e4) = e3
| op(e4,e4) = e2
| op(e4,e4) = e1
| op(e4,e4) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_271,c_32]) ).
cnf(c_1515,plain,
( op(e4,e4) = e4
| op(e4,e4) = e3
| op(e4,e4) = e2
| op(e4,e4) = op(e4,e2)
| op(e4,e4) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_273,c_1514]) ).
cnf(c_1516,plain,
( op(e4,e4) = e4
| op(e4,e4) = op(e2,e4)
| op(e4,e4) = e2
| op(e4,e4) = op(e4,e2)
| op(e4,e4) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_275,c_1515]) ).
cnf(c_1517,plain,
( op(e4,e4) = e4
| op(e4,e4) = op(e2,e4)
| op(e4,e4) = e2
| op(e4,e4) = op(e4,e2)
| op(op(e4,e2),op(e4,e2)) = op(e4,e4) ),
inference(copy,[status(thm)],[c_1516]) ).
cnf(c_1518,plain,
( op(e4,e4) = e4
| op(e4,e4) = op(e2,e4)
| op(e4,e4) = e2
| op(e4,e2) = op(e4,e4)
| op(op(e4,e2),op(e4,e2)) = op(e4,e4) ),
inference(copy,[status(thm)],[c_1517]) ).
cnf(c_1519,plain,
( op(e4,e4) = e4
| op(e2,e4) = op(e4,e4)
| op(e4,e4) = e2
| op(e4,e2) = op(e4,e4)
| op(op(e4,e2),op(e4,e2)) = op(e4,e4) ),
inference(copy,[status(thm)],[c_1518]) ).
cnf(c_1520,plain,
( op(e4,e4) = e4
| op(e2,e4) = op(e4,e4)
| op(e4,e4) = e2
| op(op(e4,e2),op(e4,e2)) = op(e4,e4) ),
inference(resolve,[status(thm)],[c_251,c_1519]) ).
cnf(c_773,plain,
( op(e4,e4) = e4
| op(e4,e4) = e2
| op(op(e4,e2),op(e4,e2)) = op(e4,e4) ),
inference(resolve,[status(thm)],[c_171,c_1520]) ).
cnf(c_1521,plain,
( op(e4,e1) = e4
| op(e4,e1) = e3
| op(e4,e1) = e2
| op(e4,e1) = e1
| op(e4,op(e4,e2)) = e0 ),
inference(paramod,[status(thm)],[c_273,c_29]) ).
cnf(c_1522,plain,
( op(e4,e1) = e4
| op(e4,e1) = e3
| op(e4,e1) = e2
| op(e4,e1) = e1
| op(e4,op(e4,e2)) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_271,c_1521]) ).
cnf(c_1523,plain,
( op(e4,e1) = e4
| op(e4,e1) = e3
| op(e4,e1) = e2
| op(e4,op(e4,e2)) = e1
| op(e4,op(e4,e2)) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_273,c_1522]) ).
cnf(c_1524,plain,
( op(e4,e1) = e4
| op(e4,e1) = e3
| op(e4,e1) = e2
| op(e4,op(e4,e2)) = op(e4,e2)
| op(e4,op(e4,e2)) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_273,c_1523]) ).
cnf(c_1525,plain,
( op(e4,e1) = e4
| op(e4,e1) = e3
| op(e4,op(e4,e2)) = e2
| op(e4,op(e4,e2)) = op(e4,e2)
| op(e4,op(e4,e2)) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_273,c_1524]) ).
cnf(c_1526,plain,
( op(e4,e1) = e4
| op(e4,op(e4,e2)) = e3
| op(e4,op(e4,e2)) = e2
| op(e4,op(e4,e2)) = op(e4,e2)
| op(e4,op(e4,e2)) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_273,c_1525]) ).
cnf(c_1527,plain,
( op(e4,e1) = e4
| op(e4,op(e4,e2)) = op(e2,e4)
| op(e4,op(e4,e2)) = e2
| op(e4,op(e4,e2)) = op(e4,e2)
| op(e4,op(e4,e2)) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_275,c_1526]) ).
cnf(c_1528,plain,
( op(e4,op(e4,e2)) = e4
| op(e4,op(e4,e2)) = op(e2,e4)
| op(e4,op(e4,e2)) = e2
| op(e4,op(e4,e2)) = op(e4,e2)
| op(e4,op(e4,e2)) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_273,c_1527]) ).
cnf(c_1529,plain,
( op(e4,op(e4,e2)) = e4
| op(e4,op(e4,e2)) = op(e2,e4)
| op(e4,op(e4,e2)) = e2
| op(e4,op(e4,e2)) = op(e4,e2)
| op(op(e4,e2),op(e4,e2)) = op(e4,op(e4,e2)) ),
inference(copy,[status(thm)],[c_1528]) ).
cnf(c_775,plain,
( op(e4,op(e4,e2)) = e4
| op(e2,e4) = op(e4,op(e4,e2))
| op(e4,op(e4,e2)) = e2
| op(e4,op(e4,e2)) = op(e4,e2)
| op(op(e4,e2),op(e4,e2)) = op(e4,op(e4,e2)) ),
inference(copy,[status(thm)],[c_1529]) ).
cnf(c_1530,plain,
( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2
| op(e1,e4) = e1
| op(op(e4,e2),e4) = e0 ),
inference(paramod,[status(thm)],[c_273,c_17]) ).
cnf(c_1531,plain,
( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2
| op(e1,e4) = e1
| op(op(e4,e2),e4) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_271,c_1530]) ).
cnf(c_1532,plain,
( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2
| op(op(e4,e2),e4) = e1
| op(op(e4,e2),e4) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_273,c_1531]) ).
cnf(c_1533,plain,
( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2
| op(op(e4,e2),e4) = op(e4,e2)
| op(op(e4,e2),e4) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_273,c_1532]) ).
cnf(c_1534,plain,
( op(e1,e4) = e4
| op(e1,e4) = e3
| op(op(e4,e2),e4) = e2
| op(op(e4,e2),e4) = op(e4,e2)
| op(op(e4,e2),e4) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_273,c_1533]) ).
cnf(c_1535,plain,
( op(e1,e4) = e4
| op(op(e4,e2),e4) = e3
| op(op(e4,e2),e4) = e2
| op(op(e4,e2),e4) = op(e4,e2)
| op(op(e4,e2),e4) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_273,c_1534]) ).
cnf(c_1536,plain,
( op(e1,e4) = e4
| op(op(e4,e2),e4) = op(e2,e4)
| op(op(e4,e2),e4) = e2
| op(op(e4,e2),e4) = op(e4,e2)
| op(op(e4,e2),e4) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_275,c_1535]) ).
cnf(c_1537,plain,
( op(op(e4,e2),e4) = e4
| op(op(e4,e2),e4) = op(e2,e4)
| op(op(e4,e2),e4) = e2
| op(op(e4,e2),e4) = op(e4,e2)
| op(op(e4,e2),e4) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_273,c_1536]) ).
cnf(c_1538,plain,
( op(op(e4,e2),e4) = e4
| op(op(e4,e2),e4) = op(e2,e4)
| op(op(e4,e2),e4) = e2
| op(op(e4,e2),e4) = op(e4,e2)
| op(op(e4,e2),op(e4,e2)) = op(op(e4,e2),e4) ),
inference(copy,[status(thm)],[c_1537]) ).
cnf(c_786,plain,
( op(op(e4,e2),e4) = e4
| op(op(e4,e2),e4) = op(e2,e4)
| op(op(e4,e2),e4) = e2
| op(op(e4,e2),op(e4,e2)) = op(op(e4,e2),e4) ),
inference(resolve,[status(thm)],[c_690,c_1538]) ).
cnf(c_794,plain,
op(e4,e2) != e4,
inference(paramod,[status(thm)],[c_273,c_264]) ).
cnf(c_1539,plain,
op(e2,e4) != e1,
inference(paramod,[status(thm)],[c_275,c_262]) ).
cnf(c_795,plain,
op(e2,e4) != op(e4,e2),
inference(paramod,[status(thm)],[c_273,c_1539]) ).
cnf(c_796,plain,
op(e4,e2) != e2,
inference(paramod,[status(thm)],[c_273,c_261]) ).
cnf(c_799,plain,
op(e4,op(e4,e2)) != op(e4,e2),
inference(paramod,[status(thm)],[c_273,c_245]) ).
cnf(c_803,plain,
op(e2,op(e4,e2)) != op(e2,e4),
inference(paramod,[status(thm)],[c_273,c_216]) ).
cnf(c_1540,plain,
op(op(e4,e2),e1) != op(e1,e4),
inference(paramod,[status(thm)],[c_273,c_200]) ).
cnf(c_1541,plain,
op(op(e4,e2),op(e4,e2)) != op(e1,e4),
inference(paramod,[status(thm)],[c_273,c_1540]) ).
cnf(c_809,plain,
op(op(e4,e2),op(e4,e2)) != op(op(e4,e2),e4),
inference(paramod,[status(thm)],[c_273,c_1541]) ).
cnf(c_814,plain,
op(op(e4,e2),e4) != op(e2,e4),
inference(paramod,[status(thm)],[c_273,c_165]) ).
cnf(c_1542,plain,
op(op(e4,e2),e1) != op(e4,e1),
inference(paramod,[status(thm)],[c_273,c_120]) ).
cnf(c_1543,plain,
op(op(e4,e2),op(e4,e2)) != op(e4,e1),
inference(paramod,[status(thm)],[c_273,c_1542]) ).
cnf(c_823,plain,
op(op(e4,e2),op(e4,e2)) != op(e4,op(e4,e2)),
inference(paramod,[status(thm)],[c_273,c_1543]) ).
cnf(c_1544,plain,
op(op(e4,e2),unit) = e1,
inference(paramod,[status(thm)],[c_273,c_36]) ).
cnf(c_826,plain,
op(op(e4,e2),unit) = op(e4,e2),
inference(paramod,[status(thm)],[c_273,c_1544]) ).
cnf(c_1545,plain,
op(unit,op(e4,e2)) = e1,
inference(paramod,[status(thm)],[c_273,c_35]) ).
cnf(c_827,plain,
op(unit,op(e4,e2)) = op(e4,e2),
inference(paramod,[status(thm)],[c_273,c_1545]) ).
cnf(c_828,plain,
op(e2,e4) != e4,
inference(paramod,[status(thm)],[c_275,c_269]) ).
cnf(c_829,plain,
op(e2,e4) != e2,
inference(paramod,[status(thm)],[c_275,c_265]) ).
cnf(c_831,plain,
op(e4,op(e2,e4)) != op(e4,e2),
inference(paramod,[status(thm)],[c_275,c_249]) ).
cnf(c_1546,plain,
op(unit,op(e2,e4)) = e3,
inference(paramod,[status(thm)],[c_275,c_39]) ).
cnf(c_845,plain,
op(unit,op(e2,e4)) = op(e2,e4),
inference(paramod,[status(thm)],[c_275,c_1546]) ).
cnf(c_852,plain,
( op(op(e4,e2),e4) = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(op(e4,e2),e2) = e4 ),
inference(resolve,[status(thm)],[c_794,c_755]) ).
cnf(c_855,negated_conjecture,
op(e4,e4) != e2,
inference(resolve,[status(thm)],[c_794,c_308]) ).
cnf(c_1547,plain,
( op(op(e4,e2),e4) = op(e2,e4)
| op(op(e4,e2),op(e2,e4)) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4) ),
inference(resolve,[status(thm)],[c_795,c_757]) ).
cnf(c_857,plain,
( op(op(e4,e2),op(e2,e4)) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4) ),
inference(resolve,[status(thm)],[c_814,c_1547]) ).
cnf(c_858,plain,
( op(e2,op(e2,e4)) = op(e4,e2)
| op(e2,op(e4,e2)) = op(e4,e2) ),
inference(resolve,[status(thm)],[c_795,c_751]) ).
cnf(c_860,plain,
( op(op(e2,e4),e4) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2) ),
inference(resolve,[status(thm)],[c_795,c_733]) ).
cnf(c_861,plain,
( op(e4,op(e2,e4)) = op(e2,e4)
| op(e2,e4) = op(e4,op(e4,e2))
| op(e4,op(op(e4,e2),op(e4,e2))) = op(e2,e4) ),
inference(resolve,[status(thm)],[c_795,c_730]) ).
cnf(c_1548,plain,
( op(e4,op(e4,e2)) = e4
| op(e2,e4) = op(e4,op(e4,e2))
| op(e4,op(e4,e2)) = e2
| op(e4,op(e4,e2)) = op(e4,e2) ),
inference(resolve,[status(thm)],[c_823,c_775]) ).
cnf(c_868,plain,
( op(e4,op(e4,e2)) = e4
| op(e2,e4) = op(e4,op(e4,e2))
| op(e4,op(e4,e2)) = e2 ),
inference(resolve,[status(thm)],[c_799,c_1548]) ).
cnf(c_872,negated_conjecture,
( op(e2,op(e2,e4)) != op(e4,e2)
| ~ defn_10 ),
inference(resolve,[status(thm)],[c_803,c_563]) ).
cnf(c_1549,plain,
( op(op(e4,e2),e4) = e4
| op(op(e4,e2),e4) = op(e2,e4)
| op(op(e4,e2),e4) = e2 ),
inference(resolve,[status(thm)],[c_809,c_786]) ).
cnf(c_873,plain,
( op(op(e4,e2),e4) = e4
| op(op(e4,e2),e4) = e2 ),
inference(resolve,[status(thm)],[c_814,c_1549]) ).
cnf(c_879,negated_conjecture,
( op(op(e4,e2),op(e2,e4)) != e4
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_814,c_337]) ).
cnf(c_1550,plain,
( op(e4,e4) = e2
| op(op(e2,e4),e4) = e2
| op(op(e4,e2),e4) = e2
| op(op(op(e4,e2),op(e4,e2)),e4) = e2 ),
inference(resolve,[status(thm)],[c_829,c_731]) ).
cnf(c_887,negated_conjecture,
( op(op(e2,e4),e4) = e2
| op(op(e4,e2),e4) = e2
| op(op(op(e4,e2),op(e4,e2)),e4) = e2 ),
inference(resolve,[status(thm)],[c_855,c_1550]) ).
cnf(c_891,negated_conjecture,
( op(e2,e4) != op(e4,op(e4,e2))
| ~ defn_30 ),
inference(resolve,[status(thm)],[c_831,c_394]) ).
cnf(c_900,negated_conjecture,
( op(e4,e4) = e4
| op(op(e4,e2),op(e4,e2)) = op(e4,e4) ),
inference(resolve,[status(thm)],[c_855,c_773]) ).
cnf(c_1551,plain,
( e0 = op(unit,op(e4,e2))
| unit = e4
| op(e2,e4) = unit
| unit = e2
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(paramod,[status(thm)],[c_770,c_271]) ).
cnf(c_1552,plain,
( op(op(e4,e2),op(e4,e2)) = op(unit,op(e4,e2))
| unit = e4
| op(e2,e4) = unit
| unit = e2
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(paramod,[status(thm)],[c_271,c_1551]) ).
cnf(c_1553,plain,
( op(op(e4,e2),op(e4,e2)) = op(e4,e2)
| unit = e4
| op(e2,e4) = unit
| unit = e2
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(paramod,[status(thm)],[c_827,c_1552]) ).
cnf(c_908,plain,
( unit = e4
| op(e2,e4) = unit
| unit = e2
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(resolve,[status(thm)],[c_677,c_1553]) ).
cnf(c_919,plain,
( op(e2,op(e4,e2)) = op(e4,e2)
| ~ defn_10 ),
inference(resolve,[status(thm)],[c_872,c_858]) ).
cnf(c_920,plain,
( op(op(e4,e2),e2) = e4
| ~ defn_20
| op(op(e4,e2),e4) = e4 ),
inference(resolve,[status(thm)],[c_873,c_502]) ).
cnf(c_931,plain,
( op(op(e4,e2),e4) = e4
| op(op(e4,e2),e2) = e4
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_879,c_852]) ).
cnf(c_933,plain,
( op(e4,op(e4,e2)) = e4
| op(e4,op(e4,e2)) = e2
| ~ defn_30 ),
inference(resolve,[status(thm)],[c_891,c_868]) ).
cnf(c_1554,plain,
( op(op(e4,e2),unit) != op(e4,e2)
| unit = e4
| unit = e2
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(paramod,[status(thm)],[c_908,c_691]) ).
cnf(c_1555,plain,
( op(e4,e2) != op(e4,e2)
| unit = e4
| unit = e2
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(paramod,[status(thm)],[c_826,c_1554]) ).
cnf(c_1053,plain,
( unit = e4
| unit = e2
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(copy,[status(thm)],[c_1555]) ).
cnf(c_1556,plain,
( op(op(e4,e2),e2) = e4
| op(op(e4,e2),e4) = e4
| op(op(e4,e2),e4) = e4
| op(op(e4,e2),e2) = e4
| defn_30
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_931,c_920]) ).
cnf(c_1557,plain,
( op(op(e4,e2),e2) = e4
| op(op(e4,e2),e4) = e4
| op(op(e4,e2),e2) = e4
| defn_30
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_1556]) ).
cnf(c_1103,plain,
( op(op(e4,e2),e4) = e4
| op(op(e4,e2),e2) = e4
| defn_30
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_1557]) ).
cnf(c_1558,plain,
( op(e4,e2) = e2
| unit = e2
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(paramod,[status(thm)],[c_1053,c_37]) ).
cnf(c_1140,plain,
( unit = e2
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(resolve,[status(thm)],[c_796,c_1558]) ).
cnf(c_1559,plain,
( op(e4,unit) != op(e4,e4)
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_1053,c_678]) ).
cnf(c_1560,plain,
( e4 != op(e4,e4)
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_42,c_1559]) ).
cnf(c_1145,plain,
( op(e4,e4) != e4
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_1560]) ).
cnf(c_1561,plain,
( op(op(e2,e4),e4) = e2
| op(op(e4,e2),e4) = e2
| op(unit,e4) = e2
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_1053,c_887]) ).
cnf(c_1562,plain,
( op(op(e2,e4),e4) = e2
| op(op(e4,e2),e4) = e2
| e4 = e2
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_41,c_1561]) ).
cnf(c_1563,plain,
( op(op(e2,e4),e4) = e2
| op(op(e4,e2),e4) = e2
| e2 = e4
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_1562]) ).
cnf(c_1171,plain,
( op(op(e2,e4),e4) = e2
| op(op(e4,e2),e4) = e2
| unit = e4
| unit = e2 ),
inference(resolve,[status(thm)],[c_267,c_1563]) ).
cnf(c_1564,plain,
( op(e4,e4) = e4
| unit = op(e4,e4)
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_1053,c_900]) ).
cnf(c_1172,plain,
( op(e4,e4) = e4
| op(e4,e4) = unit
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_1564]) ).
cnf(c_1565,plain,
( unit = e4
| unit = e2
| op(e4,e4) = unit
| unit = e4
| unit = e2 ),
inference(resolve,[status(thm)],[c_1172,c_1145]) ).
cnf(c_1566,plain,
( unit = e4
| op(e4,e4) = unit
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_1565]) ).
cnf(c_1194,plain,
( op(e4,e4) = unit
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_1566]) ).
cnf(c_1567,plain,
( op(e4,e2) = e2
| op(e4,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_1194,c_37]) ).
cnf(c_1228,plain,
( op(e4,e4) = unit
| unit = e2 ),
inference(resolve,[status(thm)],[c_796,c_1567]) ).
cnf(c_1568,plain,
( op(e2,e4) = e4
| op(e4,e4) = unit ),
inference(paramod,[status(thm)],[c_1228,c_41]) ).
cnf(c_1258,plain,
op(e4,e4) = unit,
inference(resolve,[status(thm)],[c_828,c_1568]) ).
cnf(c_1319,negated_conjecture,
unit != e2,
inference(paramod,[status(thm)],[c_1258,c_855]) ).
cnf(c_1325,plain,
op(e4,op(op(e4,e2),op(e4,e2))) != unit,
inference(paramod,[status(thm)],[c_1258,c_678]) ).
cnf(c_1332,negated_conjecture,
( op(op(e2,e4),e4) = e2
| op(op(e4,e2),e4) = e2
| unit = e4 ),
inference(resolve,[status(thm)],[c_1319,c_1171]) ).
cnf(c_1338,negated_conjecture,
op(op(e4,e2),op(e4,e2)) = unit,
inference(resolve,[status(thm)],[c_1319,c_1140]) ).
cnf(c_1569,plain,
op(e4,unit) != unit,
inference(paramod,[status(thm)],[c_1338,c_1325]) ).
cnf(c_1570,plain,
e4 != unit,
inference(paramod,[status(thm)],[c_42,c_1569]) ).
cnf(c_1339,plain,
unit != e4,
inference(copy,[status(thm)],[c_1570]) ).
cnf(c_1571,plain,
( op(e4,op(e2,e4)) = op(e2,e4)
| op(e2,e4) = op(e4,op(e4,e2))
| op(e4,unit) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_1338,c_861]) ).
cnf(c_1572,plain,
( op(e4,op(e2,e4)) = op(e2,e4)
| op(e2,e4) = op(e4,op(e4,e2))
| e4 = op(e2,e4) ),
inference(paramod,[status(thm)],[c_42,c_1571]) ).
cnf(c_1573,plain,
( op(e4,op(e2,e4)) = op(e2,e4)
| op(e2,e4) = op(e4,op(e4,e2))
| op(e2,e4) = e4 ),
inference(copy,[status(thm)],[c_1572]) ).
cnf(c_1356,plain,
( op(e4,op(e2,e4)) = op(e2,e4)
| op(e2,e4) = op(e4,op(e4,e2)) ),
inference(resolve,[status(thm)],[c_828,c_1573]) ).
cnf(c_1574,plain,
( op(op(e2,e4),e4) = op(e4,e2)
| op(unit,e4) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_1338,c_860]) ).
cnf(c_1575,plain,
( op(op(e2,e4),e4) = op(e4,e2)
| e4 = op(e4,e2) ),
inference(paramod,[status(thm)],[c_41,c_1574]) ).
cnf(c_1576,plain,
( op(op(e2,e4),e4) = op(e4,e2)
| op(e4,e2) = e4 ),
inference(copy,[status(thm)],[c_1575]) ).
cnf(c_1357,plain,
op(op(e2,e4),e4) = op(e4,e2),
inference(resolve,[status(thm)],[c_794,c_1576]) ).
cnf(c_1577,plain,
op(unit,op(e4,e2)) != op(e2,op(e4,e2)),
inference(paramod,[status(thm)],[c_1338,c_717]) ).
cnf(c_1578,plain,
op(e4,e2) != op(e2,op(e4,e2)),
inference(paramod,[status(thm)],[c_827,c_1577]) ).
cnf(c_1364,plain,
op(e2,op(e4,e2)) != op(e4,e2),
inference(copy,[status(thm)],[c_1578]) ).
cnf(c_1579,plain,
op(unit,op(e2,e4)) != op(op(e4,e2),op(e2,e4)),
inference(paramod,[status(thm)],[c_1338,c_710]) ).
cnf(c_1580,plain,
op(e2,e4) != op(op(e4,e2),op(e2,e4)),
inference(paramod,[status(thm)],[c_845,c_1579]) ).
cnf(c_1369,plain,
op(op(e4,e2),op(e2,e4)) != op(e2,e4),
inference(copy,[status(thm)],[c_1580]) ).
cnf(c_1581,plain,
op(unit,op(e2,e4)) != op(e4,op(e2,e4)),
inference(paramod,[status(thm)],[c_1338,c_707]) ).
cnf(c_1582,plain,
op(e2,e4) != op(e4,op(e2,e4)),
inference(paramod,[status(thm)],[c_845,c_1581]) ).
cnf(c_1371,plain,
op(e4,op(e2,e4)) != op(e2,e4),
inference(copy,[status(thm)],[c_1582]) ).
cnf(c_1583,plain,
op(e4,unit) != op(e4,op(e4,e2)),
inference(paramod,[status(thm)],[c_1338,c_681]) ).
cnf(c_1584,plain,
e4 != op(e4,op(e4,e2)),
inference(paramod,[status(thm)],[c_42,c_1583]) ).
cnf(c_1377,plain,
op(e4,op(e4,e2)) != e4,
inference(copy,[status(thm)],[c_1584]) ).
cnf(c_1585,negated_conjecture,
( unit != unit
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_1338,c_658]) ).
cnf(c_1379,negated_conjecture,
~ defn_00,
inference(copy,[status(thm)],[c_1585]) ).
cnf(c_1586,negated_conjecture,
( op(e4,e2) = e2
| op(op(e4,e2),e4) = e2
| unit = e4 ),
inference(paramod,[status(thm)],[c_1357,c_1332]) ).
cnf(c_1587,negated_conjecture,
( op(e4,e2) = e2
| op(op(e4,e2),e4) = e2 ),
inference(resolve,[status(thm)],[c_1339,c_1586]) ).
cnf(c_1383,negated_conjecture,
op(op(e4,e2),e4) = e2,
inference(resolve,[status(thm)],[c_796,c_1587]) ).
cnf(c_1392,plain,
~ defn_10,
inference(resolve,[status(thm)],[c_1364,c_919]) ).
cnf(c_1397,plain,
op(op(e4,e2),e2) = op(e2,e4),
inference(resolve,[status(thm)],[c_1369,c_857]) ).
cnf(c_1398,plain,
op(e2,e4) = op(e4,op(e4,e2)),
inference(resolve,[status(thm)],[c_1371,c_1356]) ).
cnf(c_1588,plain,
( op(op(e4,e2),e4) = e4
| op(e2,e4) = e4
| defn_30
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_1397,c_1103]) ).
cnf(c_1589,plain,
( op(op(e4,e2),e4) = e4
| op(e4,op(e4,e2)) = e4
| defn_30
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_1398,c_1588]) ).
cnf(c_1590,plain,
( e2 = e4
| op(e4,op(e4,e2)) = e4
| defn_30
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_1383,c_1589]) ).
cnf(c_1591,negated_conjecture,
( e2 = e4
| op(e4,op(e4,e2)) = e4
| defn_30
| defn_10 ),
inference(resolve,[status(thm)],[c_1379,c_1590]) ).
cnf(c_1592,negated_conjecture,
( e2 = e4
| op(e4,op(e4,e2)) = e4
| defn_30 ),
inference(resolve,[status(thm)],[c_1392,c_1591]) ).
cnf(c_1593,negated_conjecture,
( e2 = e4
| defn_30 ),
inference(resolve,[status(thm)],[c_1377,c_1592]) ).
cnf(c_1399,negated_conjecture,
defn_30,
inference(resolve,[status(thm)],[c_267,c_1593]) ).
cnf(c_1594,plain,
( op(e4,op(e4,e2)) = e4
| op(e4,op(e4,e2)) = e2 ),
inference(resolve,[status(thm)],[c_1399,c_933]) ).
cnf(c_1403,plain,
op(e4,op(e4,e2)) = e2,
inference(resolve,[status(thm)],[c_1377,c_1594]) ).
cnf(c_1595,plain,
e2 != op(e2,e4),
inference(paramod,[status(thm)],[c_1383,c_814]) ).
cnf(c_1596,plain,
e2 != op(e4,op(e4,e2)),
inference(paramod,[status(thm)],[c_1398,c_1595]) ).
cnf(c_1597,plain,
e2 != e2,
inference(paramod,[status(thm)],[c_1403,c_1596]) ).
cnf(c_1404,plain,
$false,
inference(copy,[status(thm)],[c_1597]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG066+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.07/20.61 % CPULimit : 300
% 0.07/20.61 % WCLimit : 300
% 0.07/20.61 % DateTime : Sat Sep 26 21:10:52 UTC 2026
% 0.07/20.61 % CPUTime :
% 0.07/20.61 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/20.61 % Process 1723956 was started by sandbox on n016,
% 0.07/20.61 % Sat Sep 26 21:10:52 2026
% 0.07/20.61 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.07/20.65
% 0.07/20.65 % From the command line: assign(max_seconds, 300).
% 7.70/21.79
% 7.70/21.79 % SZS status Theorem for theBenchmark
% 7.70/21.79
% 7.70/21.79 % Proof 1 at 0.87 (+ 0.20) seconds.
% 7.70/21.79 % Length of proof is 167.
% 7.70/21.79 % Level of proof is 16.
% 7.70/21.79 % Maximum clause weight is 65.000.
% 7.70/21.79 % Given clauses 377.
% 7.70/21.79
% 7.70/21.79 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------