%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG068+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:49:23 AM UTC 2026
% Result : Theorem 178.00s 28.07s
% Output : CNFRefutation 178.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 81
% Number of leaves : 21
% Syntax : Number of formulae : 688 ( 188 unt; 14 def)
% Number of atoms : 3277 (2656 equ)
% Maximal formula atoms : 250 ( 4 avg)
% Number of connectives : 3307 ( 718 ~;2204 |; 371 &)
% ( 14 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 15 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax1,axiom,
( ( op(e4,e4) = e4
| op(e4,e4) = e3
| op(e4,e4) = e2
| op(e4,e4) = e1
| op(e4,e4) = e0 )
& ( op(e4,e3) = e4
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e1
| op(e4,e3) = e0 )
& ( op(e4,e2) = e4
| op(e4,e2) = e3
| op(e4,e2) = e2
| op(e4,e2) = e1
| op(e4,e2) = e0 )
& ( op(e4,e1) = e4
| op(e4,e1) = e3
| op(e4,e1) = e2
| op(e4,e1) = e1
| op(e4,e1) = e0 )
& ( op(e4,e0) = e4
| op(e4,e0) = e3
| op(e4,e0) = e2
| op(e4,e0) = e1
| op(e4,e0) = e0 )
& ( op(e3,e4) = e4
| op(e3,e4) = e3
| op(e3,e4) = e2
| op(e3,e4) = e1
| op(e3,e4) = e0 )
& ( op(e3,e3) = e4
| op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 )
& ( op(e3,e2) = e4
| op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 )
& ( op(e3,e1) = e4
| op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 )
& ( op(e3,e0) = e4
| op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 )
& ( op(e2,e4) = e4
| op(e2,e4) = e3
| op(e2,e4) = e2
| op(e2,e4) = e1
| op(e2,e4) = e0 )
& ( op(e2,e3) = e4
| op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 )
& ( op(e2,e2) = e4
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 )
& ( op(e2,e1) = e4
| op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 )
& ( op(e2,e0) = e4
| op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 )
& ( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2
| op(e1,e4) = e1
| op(e1,e4) = e0 )
& ( op(e1,e3) = e4
| op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 )
& ( op(e1,e2) = e4
| op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 )
& ( op(e1,e1) = e4
| op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 )
& ( op(e1,e0) = e4
| op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 )
& ( op(e0,e4) = e4
| op(e0,e4) = e3
| op(e0,e4) = e2
| op(e0,e4) = e1
| op(e0,e4) = e0 )
& ( op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 )
& ( op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 )
& ( op(e0,e1) = e4
| op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 )
& ( op(e0,e0) = e4
| op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ) ),
file('theBenchmark.p',ax1) ).
fof(ax2,axiom,
( ( unit = e4
| unit = e3
| unit = e2
| unit = e1
| unit = e0 )
& op(e4,unit) = e4
& op(unit,e4) = e4
& op(e3,unit) = e3
& op(unit,e3) = e3
& op(e2,unit) = e2
& op(unit,e2) = e2
& op(e1,unit) = e1
& op(unit,e1) = e1
& op(e0,unit) = e0
& op(unit,e0) = e0 ),
file('theBenchmark.p',ax2) ).
fof(ax3,axiom,
( ( op(e4,e4) = e4
| op(e3,e4) = e4
| op(e2,e4) = e4
| op(e1,e4) = e4
| op(e0,e4) = e4 )
& ( op(e4,e4) = e4
| op(e4,e3) = e4
| op(e4,e2) = e4
| op(e4,e1) = e4
| op(e4,e0) = e4 )
& ( op(e4,e4) = e3
| op(e3,e4) = e3
| op(e2,e4) = e3
| op(e1,e4) = e3
| op(e0,e4) = e3 )
& ( op(e4,e4) = e3
| op(e4,e3) = e3
| op(e4,e2) = e3
| op(e4,e1) = e3
| op(e4,e0) = e3 )
& ( op(e4,e4) = e2
| op(e3,e4) = e2
| op(e2,e4) = e2
| op(e1,e4) = e2
| op(e0,e4) = e2 )
& ( op(e4,e4) = e2
| op(e4,e3) = e2
| op(e4,e2) = e2
| op(e4,e1) = e2
| op(e4,e0) = e2 )
& ( op(e4,e4) = e1
| op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| op(e0,e4) = e1 )
& ( op(e4,e4) = e1
| op(e4,e3) = e1
| op(e4,e2) = e1
| op(e4,e1) = e1
| op(e4,e0) = e1 )
& ( op(e4,e4) = e0
| op(e3,e4) = e0
| op(e2,e4) = e0
| op(e1,e4) = e0
| op(e0,e4) = e0 )
& ( op(e4,e4) = e0
| op(e4,e3) = e0
| op(e4,e2) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 )
& ( op(e4,e3) = e4
| op(e3,e3) = e4
| op(e2,e3) = e4
| op(e1,e3) = e4
| op(e0,e3) = e4 )
& ( op(e3,e4) = e4
| op(e3,e3) = e4
| op(e3,e2) = e4
| op(e3,e1) = e4
| op(e3,e0) = e4 )
& ( op(e4,e3) = e3
| op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 )
& ( op(e3,e4) = e3
| op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 )
& ( op(e4,e3) = e2
| op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 )
& ( op(e3,e4) = e2
| op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 )
& ( op(e4,e3) = e1
| op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 )
& ( op(e3,e4) = e1
| op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 )
& ( op(e4,e3) = e0
| op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 )
& ( op(e3,e4) = e0
| op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 )
& ( op(e4,e2) = e4
| op(e3,e2) = e4
| op(e2,e2) = e4
| op(e1,e2) = e4
| op(e0,e2) = e4 )
& ( op(e2,e4) = e4
| op(e2,e3) = e4
| op(e2,e2) = e4
| op(e2,e1) = e4
| op(e2,e0) = e4 )
& ( op(e4,e2) = e3
| op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 )
& ( op(e2,e4) = e3
| op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 )
& ( op(e4,e2) = e2
| op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 )
& ( op(e2,e4) = e2
| op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 )
& ( op(e4,e2) = e1
| op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 )
& ( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 )
& ( op(e4,e2) = e0
| op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 )
& ( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 )
& ( op(e4,e1) = e4
| op(e3,e1) = e4
| op(e2,e1) = e4
| op(e1,e1) = e4
| op(e0,e1) = e4 )
& ( op(e1,e4) = e4
| op(e1,e3) = e4
| op(e1,e2) = e4
| op(e1,e1) = e4
| op(e1,e0) = e4 )
& ( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 )
& ( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 )
& ( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 )
& ( op(e1,e4) = e2
| op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 )
& ( op(e4,e1) = e1
| op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 )
& ( op(e1,e4) = e1
| op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 )
& ( op(e4,e1) = e0
| op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 )
& ( op(e1,e4) = e0
| op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 )
& ( op(e4,e0) = e4
| op(e3,e0) = e4
| op(e2,e0) = e4
| op(e1,e0) = e4
| op(e0,e0) = e4 )
& ( op(e0,e4) = e4
| op(e0,e3) = e4
| op(e0,e2) = e4
| op(e0,e1) = e4
| op(e0,e0) = e4 )
& ( op(e4,e0) = e3
| op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 )
& ( op(e0,e4) = e3
| op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 )
& ( op(e4,e0) = e2
| op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 )
& ( op(e0,e4) = e2
| op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 )
& ( op(e4,e0) = e1
| op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 )
& ( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 )
& ( op(e4,e0) = e0
| op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 )
& ( op(e0,e4) = e0
| op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ) ),
file('theBenchmark.p',ax3) ).
fof(ax4,axiom,
( op(e4,e3) != op(e4,e4)
& op(e4,e2) != op(e4,e4)
& op(e4,e2) != op(e4,e3)
& op(e4,e1) != op(e4,e4)
& op(e4,e1) != op(e4,e3)
& op(e4,e1) != op(e4,e2)
& op(e4,e0) != op(e4,e4)
& op(e4,e0) != op(e4,e3)
& op(e4,e0) != op(e4,e2)
& op(e4,e0) != op(e4,e1)
& op(e3,e3) != op(e3,e4)
& op(e3,e2) != op(e3,e4)
& op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e4)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e4)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e3) != op(e2,e4)
& op(e2,e2) != op(e2,e4)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e4)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e4)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e3) != op(e1,e4)
& op(e1,e2) != op(e1,e4)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e4)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e4)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e3) != op(e0,e4)
& op(e0,e2) != op(e0,e4)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e4)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e4)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e3,e4) != op(e4,e4)
& op(e2,e4) != op(e4,e4)
& op(e2,e4) != op(e3,e4)
& op(e1,e4) != op(e4,e4)
& op(e1,e4) != op(e3,e4)
& op(e1,e4) != op(e2,e4)
& op(e0,e4) != op(e4,e4)
& op(e0,e4) != op(e3,e4)
& op(e0,e4) != op(e2,e4)
& op(e0,e4) != op(e1,e4)
& op(e3,e3) != op(e4,e3)
& op(e2,e3) != op(e4,e3)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e4,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e4,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e3,e2) != op(e4,e2)
& op(e2,e2) != op(e4,e2)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e4,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e4,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e3,e1) != op(e4,e1)
& op(e2,e1) != op(e4,e1)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e4,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e4,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e3,e0) != op(e4,e0)
& op(e2,e0) != op(e4,e0)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e4,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e4,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ),
file('theBenchmark.p',ax4) ).
fof(ax5,axiom,
( e3 != e4
& e2 != e4
& e2 != e3
& e1 != e4
& e1 != e3
& e1 != e2
& e0 != e4
& e0 != e3
& e0 != e2
& e0 != e1 ),
file('theBenchmark.p',ax5) ).
fof(ax6,axiom,
( e3 = op(e2,e4)
& e1 = op(e4,e2)
& e0 = op(op(e4,e2),op(e4,e2)) ),
file('theBenchmark.p',ax6) ).
fof(co1,conjecture,
~ ( ( ( op(op(e4,e4),e4) != e4
& op(op(e4,e4),e4) = e4
& op(e4,e4) != op(e4,e4) )
| ( op(op(e4,e3),e4) != e3
& op(op(e4,e3),e3) = e4
& op(e3,e4) != op(e4,e3) )
| ( op(op(e4,e2),e4) != e2
& op(op(e4,e2),e2) = e4
& op(e2,e4) != op(e4,e2) )
| ( op(op(e4,e1),e4) != e1
& op(op(e4,e1),e1) = e4
& op(e1,e4) != op(e4,e1) )
| ( op(op(e4,e0),e4) != e0
& op(op(e4,e0),e0) = e4
& op(e0,e4) != op(e4,e0) )
| ( op(op(e3,e4),e3) != e4
& op(op(e3,e4),e4) = e3
& op(e4,e3) != op(e3,e4) )
| ( op(op(e3,e3),e3) != e3
& op(op(e3,e3),e3) = e3
& op(e3,e3) != op(e3,e3) )
| ( op(op(e3,e2),e3) != e2
& op(op(e3,e2),e2) = e3
& op(e2,e3) != op(e3,e2) )
| ( op(op(e3,e1),e3) != e1
& op(op(e3,e1),e1) = e3
& op(e1,e3) != op(e3,e1) )
| ( op(op(e3,e0),e3) != e0
& op(op(e3,e0),e0) = e3
& op(e0,e3) != op(e3,e0) )
| ( op(op(e2,e4),e2) != e4
& op(op(e2,e4),e4) = e2
& op(e4,e2) != op(e2,e4) )
| ( op(op(e2,e3),e2) != e3
& op(op(e2,e3),e3) = e2
& op(e3,e2) != op(e2,e3) )
| ( op(op(e2,e2),e2) != e2
& op(op(e2,e2),e2) = e2
& op(e2,e2) != op(e2,e2) )
| ( op(op(e2,e1),e2) != e1
& op(op(e2,e1),e1) = e2
& op(e1,e2) != op(e2,e1) )
| ( op(op(e2,e0),e2) != e0
& op(op(e2,e0),e0) = e2
& op(e0,e2) != op(e2,e0) )
| ( op(op(e1,e4),e1) != e4
& op(op(e1,e4),e4) = e1
& op(e4,e1) != op(e1,e4) )
| ( op(op(e1,e3),e1) != e3
& op(op(e1,e3),e3) = e1
& op(e3,e1) != op(e1,e3) )
| ( op(op(e1,e2),e1) != e2
& op(op(e1,e2),e2) = e1
& op(e2,e1) != op(e1,e2) )
| ( op(op(e1,e1),e1) != e1
& op(op(e1,e1),e1) = e1
& op(e1,e1) != op(e1,e1) )
| ( op(op(e1,e0),e1) != e0
& op(op(e1,e0),e0) = e1
& op(e0,e1) != op(e1,e0) )
| ( op(op(e0,e4),e0) != e4
& op(op(e0,e4),e4) = e0
& op(e4,e0) != op(e0,e4) )
| ( op(op(e0,e3),e0) != e3
& op(op(e0,e3),e3) = e0
& op(e3,e0) != op(e0,e3) )
| ( op(op(e0,e2),e0) != e2
& op(op(e0,e2),e2) = e0
& op(e2,e0) != op(e0,e2) )
| ( op(op(e0,e1),e0) != e1
& op(op(e0,e1),e1) = e0
& op(e1,e0) != op(e0,e1) )
| ( op(op(e0,e0),e0) != e0
& op(op(e0,e0),e0) = e0
& op(e0,e0) != op(e0,e0) ) )
& ( op(e4,e4) = e4
| op(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,
~ ~ ( ( ( op(op(e4,e4),e4) != e4
& op(op(e4,e4),e4) = e4
& op(e4,e4) != op(e4,e4) )
| ( op(op(e4,e3),e4) != e3
& op(op(e4,e3),e3) = e4
& op(e3,e4) != op(e4,e3) )
| ( op(op(e4,e2),e4) != e2
& op(op(e4,e2),e2) = e4
& op(e2,e4) != op(e4,e2) )
| ( op(op(e4,e1),e4) != e1
& op(op(e4,e1),e1) = e4
& op(e1,e4) != op(e4,e1) )
| ( op(op(e4,e0),e4) != e0
& op(op(e4,e0),e0) = e4
& op(e0,e4) != op(e4,e0) )
| ( op(op(e3,e4),e3) != e4
& op(op(e3,e4),e4) = e3
& op(e4,e3) != op(e3,e4) )
| ( op(op(e3,e3),e3) != e3
& op(op(e3,e3),e3) = e3
& op(e3,e3) != op(e3,e3) )
| ( op(op(e3,e2),e3) != e2
& op(op(e3,e2),e2) = e3
& op(e2,e3) != op(e3,e2) )
| ( op(op(e3,e1),e3) != e1
& op(op(e3,e1),e1) = e3
& op(e1,e3) != op(e3,e1) )
| ( op(op(e3,e0),e3) != e0
& op(op(e3,e0),e0) = e3
& op(e0,e3) != op(e3,e0) )
| ( op(op(e2,e4),e2) != e4
& op(op(e2,e4),e4) = e2
& op(e4,e2) != op(e2,e4) )
| ( op(op(e2,e3),e2) != e3
& op(op(e2,e3),e3) = e2
& op(e3,e2) != op(e2,e3) )
| ( op(op(e2,e2),e2) != e2
& op(op(e2,e2),e2) = e2
& op(e2,e2) != op(e2,e2) )
| ( op(op(e2,e1),e2) != e1
& op(op(e2,e1),e1) = e2
& op(e1,e2) != op(e2,e1) )
| ( op(op(e2,e0),e2) != e0
& op(op(e2,e0),e0) = e2
& op(e0,e2) != op(e2,e0) )
| ( op(op(e1,e4),e1) != e4
& op(op(e1,e4),e4) = e1
& op(e4,e1) != op(e1,e4) )
| ( op(op(e1,e3),e1) != e3
& op(op(e1,e3),e3) = e1
& op(e3,e1) != op(e1,e3) )
| ( op(op(e1,e2),e1) != e2
& op(op(e1,e2),e2) = e1
& op(e2,e1) != op(e1,e2) )
| ( op(op(e1,e1),e1) != e1
& op(op(e1,e1),e1) = e1
& op(e1,e1) != op(e1,e1) )
| ( op(op(e1,e0),e1) != e0
& op(op(e1,e0),e0) = e1
& op(e0,e1) != op(e1,e0) )
| ( op(op(e0,e4),e0) != e4
& op(op(e0,e4),e4) = e0
& op(e4,e0) != op(e0,e4) )
| ( op(op(e0,e3),e0) != e3
& op(op(e0,e3),e3) = e0
& op(e3,e0) != op(e0,e3) )
| ( op(op(e0,e2),e0) != e2
& op(op(e0,e2),e2) = e0
& op(e2,e0) != op(e0,e2) )
| ( op(op(e0,e1),e0) != e1
& op(op(e0,e1),e1) = e0
& op(e1,e0) != op(e0,e1) )
| ( op(op(e0,e0),e0) != e0
& op(op(e0,e0),e0) = e0
& op(e0,e0) != op(e0,e0) ) )
& ( op(e4,e4) = e4
| op(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_20,plain,
( op(e2,e2) = e4
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_31,plain,
( op(e4,e3) = e4
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e1
| op(e4,e3) = 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_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_46,plain,
( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 ),
inference(clausify,[status(thm)],[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_63,plain,
( op(e4,e1) = e4
| op(e3,e1) = e4
| op(e2,e1) = e4
| op(e1,e1) = e4
| op(e0,e1) = 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_71,plain,
( op(e4,e2) = e3
| op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_82,plain,
( op(e3,e4) = e4
| op(e3,e3) = e4
| op(e3,e2) = e4
| op(e3,e1) = e4
| op(e3,e0) = e4 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_83,plain,
( op(e4,e3) = e4
| op(e3,e3) = e4
| op(e2,e3) = e4
| op(e1,e3) = e4
| op(e0,e3) = e4 ),
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_94,plain,
op(e1,e0) != op(e0,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_101,plain,
op(e2,e0) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_102,plain,
op(e1,e0) != op(e2,e0),
inference(copy,[status(thm)],[c_101]) ).
cnf(c_114,plain,
op(e2,e1) != op(e0,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_115,plain,
op(e0,e1) != op(e2,e1),
inference(copy,[status(thm)],[c_114]) ).
cnf(c_137,plain,
op(e4,e2) != op(e0,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_138,plain,
op(e0,e2) != op(e4,e2),
inference(copy,[status(thm)],[c_137]) ).
cnf(c_147,plain,
op(e4,e2) != op(e2,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_148,plain,
op(e2,e2) != op(e4,e2),
inference(copy,[status(thm)],[c_147]) ).
cnf(c_156,plain,
op(e4,e3) != op(e0,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_157,plain,
op(e0,e3) != op(e4,e3),
inference(copy,[status(thm)],[c_156]) ).
cnf(c_183,plain,
op(e3,e4) != op(e2,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_184,plain,
op(e2,e4) != op(e3,e4),
inference(copy,[status(thm)],[c_183]) ).
cnf(c_185,plain,
op(e4,e4) != op(e2,e4),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_186,plain,
op(e2,e4) != op(e4,e4),
inference(copy,[status(thm)],[c_185]) ).
cnf(c_211,plain,
op(e1,e3) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_212,plain,
op(e1,e0) != op(e1,e3),
inference(copy,[status(thm)],[c_211]) ).
cnf(c_213,plain,
op(e1,e4) != op(e1,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_214,plain,
op(e1,e0) != op(e1,e4),
inference(copy,[status(thm)],[c_213]) ).
cnf(c_227,plain,
op(e2,e1) != op(e2,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_228,plain,
op(e2,e2) != op(e2,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_229,plain,
op(e2,e0) != op(e2,e2),
inference(copy,[status(thm)],[c_228]) ).
cnf(c_238,plain,
op(e2,e4) != op(e2,e1),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_239,plain,
op(e2,e1) != op(e2,e4),
inference(copy,[status(thm)],[c_238]) ).
cnf(c_242,plain,
op(e2,e4) != op(e2,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_243,plain,
op(e2,e2) != op(e2,e4),
inference(copy,[status(thm)],[c_242]) ).
cnf(c_246,plain,
op(e3,e1) != op(e3,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_247,plain,
op(e3,e2) != op(e3,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_248,plain,
op(e3,e0) != op(e3,e2),
inference(copy,[status(thm)],[c_247]) ).
cnf(c_268,plain,
op(e4,e3) != op(e4,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_269,plain,
op(e4,e0) != op(e4,e3),
inference(copy,[status(thm)],[c_268]) ).
cnf(c_270,plain,
op(e4,e4) != op(e4,e0),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_271,plain,
op(e4,e0) != op(e4,e4),
inference(copy,[status(thm)],[c_270]) ).
cnf(c_278,plain,
op(e4,e3) != op(e4,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_279,plain,
op(e4,e2) != op(e4,e3),
inference(copy,[status(thm)],[c_278]) ).
cnf(c_280,plain,
op(e4,e4) != op(e4,e2),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_281,plain,
op(e4,e2) != op(e4,e4),
inference(copy,[status(thm)],[c_280]) ).
cnf(c_282,plain,
op(e4,e4) != op(e4,e3),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_283,plain,
op(e4,e3) != op(e4,e4),
inference(copy,[status(thm)],[c_282]) ).
cnf(c_284,plain,
e1 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_285,plain,
e2 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_286,plain,
e0 != e2,
inference(copy,[status(thm)],[c_285]) ).
cnf(c_287,plain,
e3 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_288,plain,
e0 != e3,
inference(copy,[status(thm)],[c_287]) ).
cnf(c_289,plain,
e4 != e0,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_290,plain,
e0 != e4,
inference(copy,[status(thm)],[c_289]) ).
cnf(c_291,plain,
e2 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_292,plain,
e1 != e2,
inference(copy,[status(thm)],[c_291]) ).
cnf(c_293,plain,
e3 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_294,plain,
e1 != e3,
inference(copy,[status(thm)],[c_293]) ).
cnf(c_295,plain,
e4 != e1,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_296,plain,
e1 != e4,
inference(copy,[status(thm)],[c_295]) ).
cnf(c_297,plain,
e3 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_298,plain,
e2 != e3,
inference(copy,[status(thm)],[c_297]) ).
cnf(c_299,plain,
e4 != e2,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_300,plain,
e2 != e4,
inference(copy,[status(thm)],[c_299]) ).
cnf(c_301,plain,
e4 != e3,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_302,plain,
e3 != e4,
inference(copy,[status(thm)],[c_301]) ).
cnf(c_303,plain,
op(op(e4,e2),op(e4,e2)) = e0,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_304,plain,
e0 = op(op(e4,e2),op(e4,e2)),
inference(copy,[status(thm)],[c_303]) ).
cnf(c_305,plain,
op(e4,e2) = e1,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_306,plain,
e1 = op(e4,e2),
inference(copy,[status(thm)],[c_305]) ).
cnf(c_307,plain,
op(e2,e4) = e3,
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_308,plain,
e3 = op(e2,e4),
inference(copy,[status(thm)],[c_307]) ).
cnf(c_317,negated_conjecture,
( op(e1,e0) = e1
| op(e1,e1) != e0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_3474,negated_conjecture,
( op(e1,e0) = e1
| op(op(e4,e2),e1) != e0 ),
inference(paramod,[status(thm)],[c_306,c_317]) ).
cnf(c_3475,negated_conjecture,
( op(e1,e0) = e1
| op(op(e4,e2),op(e4,e2)) != e0 ),
inference(paramod,[status(thm)],[c_306,c_3474]) ).
cnf(c_3476,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_304,c_3475]) ).
cnf(c_3477,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_306,c_3476]) ).
cnf(c_3478,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_304,c_3477]) ).
cnf(c_3479,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_306,c_3478]) ).
cnf(c_318,negated_conjecture,
op(op(e4,e2),op(op(e4,e2),op(e4,e2))) = op(e4,e2),
inference(copy,[status(thm)],[c_3479]) ).
cnf(c_329,negated_conjecture,
( op(e2,e4) = e2
| op(e2,e2) != e4 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_336,negated_conjecture,
( op(e3,e4) = e3
| op(e3,e3) != e4 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_3480,negated_conjecture,
( op(e3,e4) = e3
| op(op(e2,e4),e3) != e4 ),
inference(paramod,[status(thm)],[c_308,c_336]) ).
cnf(c_3481,negated_conjecture,
( op(e3,e4) = e3
| op(op(e2,e4),op(e2,e4)) != e4 ),
inference(paramod,[status(thm)],[c_308,c_3480]) ).
cnf(c_3482,negated_conjecture,
( op(op(e2,e4),e4) = e3
| op(op(e2,e4),op(e2,e4)) != e4 ),
inference(paramod,[status(thm)],[c_308,c_3481]) ).
cnf(c_337,negated_conjecture,
( op(op(e2,e4),e4) = op(e2,e4)
| op(op(e2,e4),op(e2,e4)) != e4 ),
inference(paramod,[status(thm)],[c_308,c_3482]) ).
cnf(c_338,negated_conjecture,
( op(e4,e0) = e4
| op(e4,e4) != e0 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_3483,negated_conjecture,
( op(e4,e0) = e4
| op(e4,e4) != op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_304,c_338]) ).
cnf(c_3484,negated_conjecture,
( op(e4,op(op(e4,e2),op(e4,e2))) = e4
| op(e4,e4) != op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_304,c_3483]) ).
cnf(c_339,negated_conjecture,
( op(e4,op(op(e4,e2),op(e4,e2))) = e4
| op(op(e4,e2),op(e4,e2)) != op(e4,e4) ),
inference(copy,[status(thm)],[c_3484]) ).
cnf(c_341,negated_conjecture,
( op(e4,e2) = e4
| op(e4,e4) != e2 ),
inference(clausify,[status(thm)],[co1_neg]) ).
fof(def_defn_00,definition,
( defn_00
<=> ( op(op(e0,e1),e0) != e1
& op(op(e0,e1),e1) = e0
& op(e1,e0) != op(e0,e1) ) ),
introduced(definition,[new_symbols(definition,[defn_00])],[]) ).
fof(def_defn_10,definition,
( defn_10
<=> ( op(op(e0,e2),e0) != e2
& op(op(e0,e2),e2) = e0
& op(e2,e0) != op(e0,e2) ) ),
introduced(definition,[new_symbols(definition,[defn_10])],[]) ).
fof(def_defn_20,definition,
( defn_20
<=> ( op(op(e0,e3),e0) != e3
& op(op(e0,e3),e3) = e0
& op(e3,e0) != op(e0,e3) ) ),
introduced(definition,[new_symbols(definition,[defn_20])],[]) ).
fof(def_defn_30,definition,
( defn_30
<=> ( op(op(e0,e4),e0) != e4
& op(op(e0,e4),e4) = e0
& op(e4,e0) != op(e0,e4) ) ),
introduced(definition,[new_symbols(definition,[defn_30])],[]) ).
fof(def_defn_40,definition,
( defn_40
<=> ( op(op(e1,e0),e1) != e0
& op(op(e1,e0),e0) = e1
& op(e1,e0) != op(e0,e1) ) ),
introduced(definition,[new_symbols(definition,[defn_40])],[]) ).
fof(def_defn_50,definition,
( defn_50
<=> ( op(op(e1,e2),e1) != e2
& op(op(e1,e2),e2) = e1
& op(e2,e1) != op(e1,e2) ) ),
introduced(definition,[new_symbols(definition,[defn_50])],[]) ).
fof(def_defn_60,definition,
( defn_60
<=> ( op(op(e1,e3),e1) != e3
& op(op(e1,e3),e3) = e1
& op(e3,e1) != op(e1,e3) ) ),
introduced(definition,[new_symbols(definition,[defn_60])],[]) ).
fof(def_defn_70,definition,
( defn_70
<=> ( op(op(e1,e4),e1) != e4
& op(op(e1,e4),e4) = e1
& op(e4,e1) != op(e1,e4) ) ),
introduced(definition,[new_symbols(definition,[defn_70])],[]) ).
fof(def_defn_80,definition,
( defn_80
<=> ( op(op(e2,e0),e2) != e0
& op(op(e2,e0),e0) = e2
& op(e2,e0) != op(e0,e2) ) ),
introduced(definition,[new_symbols(definition,[defn_80])],[]) ).
fof(def_defn_90,definition,
( defn_90
<=> ( op(op(e2,e1),e2) != e1
& op(op(e2,e1),e1) = e2
& op(e2,e1) != op(e1,e2) ) ),
introduced(definition,[new_symbols(definition,[defn_90])],[]) ).
fof(def_defn_100,definition,
( defn_100
<=> ( op(op(e2,e3),e2) != e3
& op(op(e2,e3),e3) = e2
& op(e3,e2) != op(e2,e3) ) ),
introduced(definition,[new_symbols(definition,[defn_100])],[]) ).
fof(def_defn_110,definition,
( defn_110
<=> ( op(op(e2,e4),e2) != e4
& op(op(e2,e4),e4) = e2
& op(e4,e2) != op(e2,e4) ) ),
introduced(definition,[new_symbols(definition,[defn_110])],[]) ).
fof(def_defn_120,definition,
( defn_120
<=> ( op(op(e3,e0),e3) != e0
& op(op(e3,e0),e0) = e3
& op(e3,e0) != op(e0,e3) ) ),
introduced(definition,[new_symbols(definition,[defn_120])],[]) ).
fof(def_defn_130,definition,
( defn_130
<=> ( op(op(e3,e1),e3) != e1
& op(op(e3,e1),e1) = e3
& op(e3,e1) != op(e1,e3) ) ),
introduced(definition,[new_symbols(definition,[defn_130])],[]) ).
cnf(c_685,negated_conjecture,
( op(op(e4,e3),e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| op(e4,e0) != op(e0,e4)
| op(op(e3,e4),e4) = e3
| op(op(e3,e2),e2) = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00,def_defn_10,def_defn_20,def_defn_30,def_defn_40,def_defn_50,def_defn_60,def_defn_70,def_defn_80,def_defn_90,def_defn_100,def_defn_110,def_defn_120,def_defn_130]) ).
cnf(c_3485,negated_conjecture,
( op(op(e4,e3),e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| op(e4,e0) != op(e0,e4)
| op(op(e3,e4),e4) = e3
| op(op(op(e2,e4),e2),e2) = e3
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_308,c_685]) ).
cnf(c_3486,negated_conjecture,
( op(op(e4,e3),e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| op(e4,e0) != op(e0,e4)
| op(op(e3,e4),e4) = e3
| op(op(op(e2,e4),e2),e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_308,c_3485]) ).
cnf(c_3487,negated_conjecture,
( op(op(e4,e3),e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| op(e4,e0) != op(e0,e4)
| op(op(op(e2,e4),e4),e4) = e3
| op(op(op(e2,e4),e2),e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_308,c_3486]) ).
cnf(c_3488,negated_conjecture,
( op(op(e4,e3),e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| op(e4,e0) != op(e0,e4)
| op(op(op(e2,e4),e4),e4) = op(e2,e4)
| op(op(op(e2,e4),e2),e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_308,c_3487]) ).
cnf(c_3489,negated_conjecture,
( op(op(e4,e3),e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| op(e4,op(op(e4,e2),op(e4,e2))) != op(e0,e4)
| op(op(op(e2,e4),e4),e4) = op(e2,e4)
| op(op(op(e2,e4),e2),e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_304,c_3488]) ).
cnf(c_3490,negated_conjecture,
( op(op(e4,e3),e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,e1),e1) = e4
| op(e4,op(op(e4,e2),op(e4,e2))) != op(op(op(e4,e2),op(e4,e2)),e4)
| op(op(op(e2,e4),e4),e4) = op(e2,e4)
| op(op(op(e2,e4),e2),e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_304,c_3489]) ).
cnf(c_3491,negated_conjecture,
( op(op(e4,e3),e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,op(e4,e2)),e1) = e4
| op(e4,op(op(e4,e2),op(e4,e2))) != op(op(op(e4,e2),op(e4,e2)),e4)
| op(op(op(e2,e4),e4),e4) = op(e2,e4)
| op(op(op(e2,e4),e2),e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_306,c_3490]) ).
cnf(c_3492,negated_conjecture,
( op(op(e4,e3),e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,op(e4,e2)),op(e4,e2)) = e4
| op(e4,op(op(e4,e2),op(e4,e2))) != op(op(op(e4,e2),op(e4,e2)),e4)
| op(op(op(e2,e4),e4),e4) = op(e2,e4)
| op(op(op(e2,e4),e2),e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_306,c_3491]) ).
cnf(c_3493,negated_conjecture,
( op(op(e4,op(e2,e4)),e4) != e3
| op(op(e4,e2),e2) = e4
| op(op(e4,op(e4,e2)),op(e4,e2)) = e4
| op(e4,op(op(e4,e2),op(e4,e2))) != op(op(op(e4,e2),op(e4,e2)),e4)
| op(op(op(e2,e4),e4),e4) = op(e2,e4)
| op(op(op(e2,e4),e2),e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_308,c_3492]) ).
cnf(c_3494,negated_conjecture,
( op(op(e4,op(e2,e4)),e4) != op(e2,e4)
| op(op(e4,e2),e2) = e4
| op(op(e4,op(e4,e2)),op(e4,e2)) = e4
| op(e4,op(op(e4,e2),op(e4,e2))) != op(op(op(e4,e2),op(e4,e2)),e4)
| op(op(op(e2,e4),e4),e4) = op(e2,e4)
| op(op(op(e2,e4),e2),e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_308,c_3493]) ).
cnf(c_686,negated_conjecture,
( op(op(e4,op(e2,e4)),e4) != op(e2,e4)
| op(op(e4,e2),e2) = e4
| op(op(e4,op(e4,e2)),op(e4,e2)) = e4
| op(op(op(e4,e2),op(e4,e2)),e4) != op(e4,op(op(e4,e2),op(e4,e2)))
| op(op(op(e2,e4),e4),e4) = op(e2,e4)
| op(op(op(e2,e4),e2),e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_3494]) ).
cnf(c_1155,negated_conjecture,
( op(op(e3,e1),e1) = e3
| ~ defn_130 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_130]) ).
cnf(c_3495,negated_conjecture,
( op(op(op(e2,e4),e1),e1) = e3
| ~ defn_130 ),
inference(paramod,[status(thm)],[c_308,c_1155]) ).
cnf(c_3496,negated_conjecture,
( op(op(op(e2,e4),op(e4,e2)),e1) = e3
| ~ defn_130 ),
inference(paramod,[status(thm)],[c_306,c_3495]) ).
cnf(c_3497,negated_conjecture,
( op(op(op(e2,e4),op(e4,e2)),op(e4,e2)) = e3
| ~ defn_130 ),
inference(paramod,[status(thm)],[c_306,c_3496]) ).
cnf(c_1156,negated_conjecture,
( op(op(op(e2,e4),op(e4,e2)),op(e4,e2)) = op(e2,e4)
| ~ defn_130 ),
inference(paramod,[status(thm)],[c_308,c_3497]) ).
cnf(c_1163,negated_conjecture,
( op(e3,e0) != op(e0,e3)
| ~ defn_120 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_120]) ).
cnf(c_3498,negated_conjecture,
( op(op(e2,e4),e0) != op(e0,e3)
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_308,c_1163]) ).
cnf(c_3499,negated_conjecture,
( op(op(e2,e4),op(op(e4,e2),op(e4,e2))) != op(e0,e3)
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_304,c_3498]) ).
cnf(c_3500,negated_conjecture,
( op(op(e2,e4),op(op(e4,e2),op(e4,e2))) != op(op(op(e4,e2),op(e4,e2)),e3)
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_304,c_3499]) ).
cnf(c_3501,negated_conjecture,
( op(op(e2,e4),op(op(e4,e2),op(e4,e2))) != op(op(op(e4,e2),op(e4,e2)),op(e2,e4))
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_308,c_3500]) ).
cnf(c_1164,negated_conjecture,
( op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) != op(op(e2,e4),op(op(e4,e2),op(e4,e2)))
| ~ defn_120 ),
inference(copy,[status(thm)],[c_3501]) ).
cnf(c_1166,negated_conjecture,
( op(op(e2,e4),e4) = e2
| ~ defn_110 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_110]) ).
cnf(c_1170,negated_conjecture,
( op(op(e2,e3),e3) = e2
| ~ defn_100 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_100]) ).
cnf(c_3502,negated_conjecture,
( op(op(e2,op(e2,e4)),e3) = e2
| ~ defn_100 ),
inference(paramod,[status(thm)],[c_308,c_1170]) ).
cnf(c_1171,negated_conjecture,
( op(op(e2,op(e2,e4)),op(e2,e4)) = e2
| ~ defn_100 ),
inference(paramod,[status(thm)],[c_308,c_3502]) ).
cnf(c_1176,negated_conjecture,
( op(op(e2,e1),e1) = e2
| ~ defn_90 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_90]) ).
cnf(c_3503,negated_conjecture,
( op(op(e2,op(e4,e2)),e1) = e2
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_306,c_1176]) ).
cnf(c_1177,negated_conjecture,
( op(op(e2,op(e4,e2)),op(e4,e2)) = e2
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_306,c_3503]) ).
cnf(c_1184,negated_conjecture,
( op(e2,e0) != op(e0,e2)
| ~ defn_80 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_80]) ).
cnf(c_3504,negated_conjecture,
( op(e2,op(op(e4,e2),op(e4,e2))) != op(e0,e2)
| ~ defn_80 ),
inference(paramod,[status(thm)],[c_304,c_1184]) ).
cnf(c_3505,negated_conjecture,
( op(e2,op(op(e4,e2),op(e4,e2))) != op(op(op(e4,e2),op(e4,e2)),e2)
| ~ defn_80 ),
inference(paramod,[status(thm)],[c_304,c_3504]) ).
cnf(c_1185,negated_conjecture,
( op(op(op(e4,e2),op(e4,e2)),e2) != op(e2,op(op(e4,e2),op(e4,e2)))
| ~ defn_80 ),
inference(copy,[status(thm)],[c_3505]) ).
cnf(c_1188,negated_conjecture,
( op(op(e1,e4),e4) = e1
| ~ defn_70 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_70]) ).
cnf(c_3506,negated_conjecture,
( op(op(op(e4,e2),e4),e4) = e1
| ~ defn_70 ),
inference(paramod,[status(thm)],[c_306,c_1188]) ).
cnf(c_1189,negated_conjecture,
( op(op(op(e4,e2),e4),e4) = op(e4,e2)
| ~ defn_70 ),
inference(paramod,[status(thm)],[c_306,c_3506]) ).
cnf(c_1194,negated_conjecture,
( op(op(e1,e3),e3) = e1
| ~ defn_60 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_60]) ).
cnf(c_3507,negated_conjecture,
( op(op(op(e4,e2),e3),e3) = e1
| ~ defn_60 ),
inference(paramod,[status(thm)],[c_306,c_1194]) ).
cnf(c_3508,negated_conjecture,
( op(op(op(e4,e2),op(e2,e4)),e3) = e1
| ~ defn_60 ),
inference(paramod,[status(thm)],[c_308,c_3507]) ).
cnf(c_3509,negated_conjecture,
( op(op(op(e4,e2),op(e2,e4)),op(e2,e4)) = e1
| ~ defn_60 ),
inference(paramod,[status(thm)],[c_308,c_3508]) ).
cnf(c_1195,negated_conjecture,
( op(op(op(e4,e2),op(e2,e4)),op(e2,e4)) = op(e4,e2)
| ~ defn_60 ),
inference(paramod,[status(thm)],[c_306,c_3509]) ).
cnf(c_1200,negated_conjecture,
( op(op(e1,e2),e2) = e1
| ~ defn_50 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_50]) ).
cnf(c_3510,negated_conjecture,
( op(op(op(e4,e2),e2),e2) = e1
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_306,c_1200]) ).
cnf(c_1201,negated_conjecture,
( op(op(op(e4,e2),e2),e2) = op(e4,e2)
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_306,c_3510]) ).
cnf(c_1204,negated_conjecture,
( op(op(e1,e0),e1) != e0
| ~ defn_40 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_40]) ).
cnf(c_3511,negated_conjecture,
( op(op(op(e4,e2),e0),e1) != e0
| ~ defn_40 ),
inference(paramod,[status(thm)],[c_306,c_1204]) ).
cnf(c_3512,negated_conjecture,
( op(op(op(e4,e2),op(op(e4,e2),op(e4,e2))),e1) != e0
| ~ defn_40 ),
inference(paramod,[status(thm)],[c_304,c_3511]) ).
cnf(c_3513,negated_conjecture,
( op(op(e4,e2),e1) != e0
| ~ defn_40 ),
inference(paramod,[status(thm)],[c_318,c_3512]) ).
cnf(c_3514,negated_conjecture,
( op(op(e4,e2),op(e4,e2)) != e0
| ~ defn_40 ),
inference(paramod,[status(thm)],[c_306,c_3513]) ).
cnf(c_3515,negated_conjecture,
( op(op(e4,e2),op(e4,e2)) != op(op(e4,e2),op(e4,e2))
| ~ defn_40 ),
inference(paramod,[status(thm)],[c_304,c_3514]) ).
cnf(c_1205,negated_conjecture,
~ defn_40,
inference(copy,[status(thm)],[c_3515]) ).
cnf(c_1212,negated_conjecture,
( op(e4,e0) != op(e0,e4)
| ~ defn_30 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_30]) ).
cnf(c_3516,negated_conjecture,
( op(e4,op(op(e4,e2),op(e4,e2))) != op(e0,e4)
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_304,c_1212]) ).
cnf(c_3517,negated_conjecture,
( op(e4,op(op(e4,e2),op(e4,e2))) != op(op(op(e4,e2),op(e4,e2)),e4)
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_304,c_3516]) ).
cnf(c_1213,negated_conjecture,
( op(op(op(e4,e2),op(e4,e2)),e4) != op(e4,op(op(e4,e2),op(e4,e2)))
| ~ defn_30 ),
inference(copy,[status(thm)],[c_3517]) ).
cnf(c_1218,negated_conjecture,
( op(e3,e0) != op(e0,e3)
| ~ defn_20 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_20]) ).
cnf(c_3518,negated_conjecture,
( op(op(e2,e4),e0) != op(e0,e3)
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_308,c_1218]) ).
cnf(c_3519,negated_conjecture,
( op(op(e2,e4),op(op(e4,e2),op(e4,e2))) != op(e0,e3)
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_304,c_3518]) ).
cnf(c_3520,negated_conjecture,
( op(op(e2,e4),op(op(e4,e2),op(e4,e2))) != op(op(op(e4,e2),op(e4,e2)),e3)
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_304,c_3519]) ).
cnf(c_3521,negated_conjecture,
( op(op(e2,e4),op(op(e4,e2),op(e4,e2))) != op(op(op(e4,e2),op(e4,e2)),op(e2,e4))
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_308,c_3520]) ).
cnf(c_1219,negated_conjecture,
( op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) != op(op(e2,e4),op(op(e4,e2),op(e4,e2)))
| ~ defn_20 ),
inference(copy,[status(thm)],[c_3521]) ).
cnf(c_1224,negated_conjecture,
( op(e2,e0) != op(e0,e2)
| ~ defn_10 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_10]) ).
cnf(c_3522,negated_conjecture,
( op(e2,op(op(e4,e2),op(e4,e2))) != op(e0,e2)
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_304,c_1224]) ).
cnf(c_3523,negated_conjecture,
( op(e2,op(op(e4,e2),op(e4,e2))) != op(op(op(e4,e2),op(e4,e2)),e2)
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_304,c_3522]) ).
cnf(c_1225,negated_conjecture,
( op(op(op(e4,e2),op(e4,e2)),e2) != op(e2,op(op(e4,e2),op(e4,e2)))
| ~ defn_10 ),
inference(copy,[status(thm)],[c_3523]) ).
cnf(c_1230,negated_conjecture,
( op(e1,e0) != op(e0,e1)
| ~ defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00]) ).
cnf(c_3524,negated_conjecture,
( op(op(e4,e2),e0) != op(e0,e1)
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_306,c_1230]) ).
cnf(c_3525,negated_conjecture,
( op(op(e4,e2),op(op(e4,e2),op(e4,e2))) != op(e0,e1)
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_304,c_3524]) ).
cnf(c_3526,negated_conjecture,
( op(e4,e2) != op(e0,e1)
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_318,c_3525]) ).
cnf(c_3527,negated_conjecture,
( op(e4,e2) != op(op(op(e4,e2),op(e4,e2)),e1)
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_304,c_3526]) ).
cnf(c_3528,negated_conjecture,
( op(e4,e2) != op(op(op(e4,e2),op(e4,e2)),op(e4,e2))
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_306,c_3527]) ).
cnf(c_1231,negated_conjecture,
( op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) != op(e4,e2)
| ~ defn_00 ),
inference(copy,[status(thm)],[c_3528]) ).
cnf(c_1232,plain,
op(op(e4,e2),op(e4,e2)) != e4,
inference(paramod,[status(thm)],[c_304,c_290]) ).
cnf(c_3529,plain,
op(op(e4,e2),op(e4,e2)) != e3,
inference(paramod,[status(thm)],[c_304,c_288]) ).
cnf(c_1233,plain,
op(op(e4,e2),op(e4,e2)) != op(e2,e4),
inference(paramod,[status(thm)],[c_308,c_3529]) ).
cnf(c_1234,plain,
op(op(e4,e2),op(e4,e2)) != e2,
inference(paramod,[status(thm)],[c_304,c_286]) ).
cnf(c_3530,plain,
op(e4,e2) != e0,
inference(paramod,[status(thm)],[c_306,c_284]) ).
cnf(c_3531,plain,
op(e4,e2) != op(op(e4,e2),op(e4,e2)),
inference(paramod,[status(thm)],[c_304,c_3530]) ).
cnf(c_1235,plain,
op(op(e4,e2),op(e4,e2)) != op(e4,e2),
inference(copy,[status(thm)],[c_3531]) ).
cnf(c_1236,plain,
op(e4,op(op(e4,e2),op(e4,e2))) != op(e4,e4),
inference(paramod,[status(thm)],[c_304,c_271]) ).
cnf(c_3532,plain,
op(e4,op(op(e4,e2),op(e4,e2))) != op(e4,e3),
inference(paramod,[status(thm)],[c_304,c_269]) ).
cnf(c_1237,plain,
op(e4,op(op(e4,e2),op(e4,e2))) != op(e4,op(e2,e4)),
inference(paramod,[status(thm)],[c_308,c_3532]) ).
cnf(c_3533,plain,
op(op(e2,e4),e0) != op(e3,e2),
inference(paramod,[status(thm)],[c_308,c_248]) ).
cnf(c_3534,plain,
op(op(e2,e4),op(op(e4,e2),op(e4,e2))) != op(e3,e2),
inference(paramod,[status(thm)],[c_304,c_3533]) ).
cnf(c_1242,plain,
op(op(e2,e4),op(op(e4,e2),op(e4,e2))) != op(op(e2,e4),e2),
inference(paramod,[status(thm)],[c_308,c_3534]) ).
cnf(c_3535,plain,
op(op(e2,e4),e1) != op(e3,e0),
inference(paramod,[status(thm)],[c_308,c_246]) ).
cnf(c_3536,plain,
op(op(e2,e4),op(e4,e2)) != op(e3,e0),
inference(paramod,[status(thm)],[c_306,c_3535]) ).
cnf(c_3537,plain,
op(op(e2,e4),op(e4,e2)) != op(op(e2,e4),e0),
inference(paramod,[status(thm)],[c_308,c_3536]) ).
cnf(c_3538,plain,
op(op(e2,e4),op(e4,e2)) != op(op(e2,e4),op(op(e4,e2),op(e4,e2))),
inference(paramod,[status(thm)],[c_304,c_3537]) ).
cnf(c_1243,plain,
op(op(e2,e4),op(op(e4,e2),op(e4,e2))) != op(op(e2,e4),op(e4,e2)),
inference(copy,[status(thm)],[c_3538]) ).
cnf(c_1246,plain,
op(e2,op(op(e4,e2),op(e4,e2))) != op(e2,e2),
inference(paramod,[status(thm)],[c_304,c_229]) ).
cnf(c_3539,plain,
op(e2,op(e4,e2)) != op(e2,e0),
inference(paramod,[status(thm)],[c_306,c_227]) ).
cnf(c_3540,plain,
op(e2,op(e4,e2)) != op(e2,op(op(e4,e2),op(e4,e2))),
inference(paramod,[status(thm)],[c_304,c_3539]) ).
cnf(c_1247,plain,
op(e2,op(op(e4,e2),op(e4,e2))) != op(e2,op(e4,e2)),
inference(copy,[status(thm)],[c_3540]) ).
cnf(c_3541,plain,
op(op(e4,e2),e0) != op(e1,e4),
inference(paramod,[status(thm)],[c_306,c_214]) ).
cnf(c_3542,plain,
op(op(e4,e2),op(op(e4,e2),op(e4,e2))) != op(e1,e4),
inference(paramod,[status(thm)],[c_304,c_3541]) ).
cnf(c_3543,plain,
op(e4,e2) != op(e1,e4),
inference(paramod,[status(thm)],[c_318,c_3542]) ).
cnf(c_3544,plain,
op(e4,e2) != op(op(e4,e2),e4),
inference(paramod,[status(thm)],[c_306,c_3543]) ).
cnf(c_1248,plain,
op(op(e4,e2),e4) != op(e4,e2),
inference(copy,[status(thm)],[c_3544]) ).
cnf(c_3545,plain,
op(op(e4,e2),e0) != op(e1,e3),
inference(paramod,[status(thm)],[c_306,c_212]) ).
cnf(c_3546,plain,
op(op(e4,e2),op(op(e4,e2),op(e4,e2))) != op(e1,e3),
inference(paramod,[status(thm)],[c_304,c_3545]) ).
cnf(c_3547,plain,
op(e4,e2) != op(e1,e3),
inference(paramod,[status(thm)],[c_318,c_3546]) ).
cnf(c_3548,plain,
op(e4,e2) != op(op(e4,e2),e3),
inference(paramod,[status(thm)],[c_306,c_3547]) ).
cnf(c_3549,plain,
op(e4,e2) != op(op(e4,e2),op(e2,e4)),
inference(paramod,[status(thm)],[c_308,c_3548]) ).
cnf(c_1249,plain,
op(op(e4,e2),op(e2,e4)) != op(e4,e2),
inference(copy,[status(thm)],[c_3549]) ).
cnf(c_3550,plain,
op(op(op(e4,e2),op(e4,e2)),e3) != op(e4,e3),
inference(paramod,[status(thm)],[c_304,c_157]) ).
cnf(c_3551,plain,
op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) != op(e4,e3),
inference(paramod,[status(thm)],[c_308,c_3550]) ).
cnf(c_1265,plain,
op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) != op(e4,op(e2,e4)),
inference(paramod,[status(thm)],[c_308,c_3551]) ).
cnf(c_1269,plain,
op(op(op(e4,e2),op(e4,e2)),e2) != op(e4,e2),
inference(paramod,[status(thm)],[c_304,c_138]) ).
cnf(c_3552,plain,
op(op(op(e4,e2),op(e4,e2)),e1) != op(e2,e1),
inference(paramod,[status(thm)],[c_304,c_115]) ).
cnf(c_3553,plain,
op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) != op(e2,e1),
inference(paramod,[status(thm)],[c_306,c_3552]) ).
cnf(c_1275,plain,
op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) != op(e2,op(e4,e2)),
inference(paramod,[status(thm)],[c_306,c_3553]) ).
cnf(c_3554,plain,
op(op(e4,e2),e0) != op(e2,e0),
inference(paramod,[status(thm)],[c_306,c_102]) ).
cnf(c_3555,plain,
op(op(e4,e2),op(op(e4,e2),op(e4,e2))) != op(e2,e0),
inference(paramod,[status(thm)],[c_304,c_3554]) ).
cnf(c_3556,plain,
op(e4,e2) != op(e2,e0),
inference(paramod,[status(thm)],[c_318,c_3555]) ).
cnf(c_3557,plain,
op(e4,e2) != op(e2,op(op(e4,e2),op(e4,e2))),
inference(paramod,[status(thm)],[c_304,c_3556]) ).
cnf(c_1281,plain,
op(e2,op(op(e4,e2),op(e4,e2))) != op(e4,e2),
inference(copy,[status(thm)],[c_3557]) ).
cnf(c_3558,plain,
op(op(e4,e2),e0) != op(e0,e0),
inference(paramod,[status(thm)],[c_306,c_94]) ).
cnf(c_3559,plain,
op(op(e4,e2),op(op(e4,e2),op(e4,e2))) != op(e0,e0),
inference(paramod,[status(thm)],[c_304,c_3558]) ).
cnf(c_3560,plain,
op(e4,e2) != op(e0,e0),
inference(paramod,[status(thm)],[c_318,c_3559]) ).
cnf(c_3561,plain,
op(e4,e2) != op(op(op(e4,e2),op(e4,e2)),e0),
inference(paramod,[status(thm)],[c_304,c_3560]) ).
cnf(c_3562,plain,
op(e4,e2) != op(op(op(e4,e2),op(e4,e2)),op(op(e4,e2),op(e4,e2))),
inference(paramod,[status(thm)],[c_304,c_3561]) ).
cnf(c_1285,plain,
op(op(op(e4,e2),op(e4,e2)),op(op(e4,e2),op(e4,e2))) != op(e4,e2),
inference(copy,[status(thm)],[c_3562]) ).
cnf(c_3563,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_304,c_89]) ).
cnf(c_3564,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_306,c_3563]) ).
cnf(c_1289,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_308,c_3564]) ).
cnf(c_3565,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_304,c_87]) ).
cnf(c_3566,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_306,c_3565]) ).
cnf(c_3567,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_306,c_3566]) ).
cnf(c_3568,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_306,c_3567]) ).
cnf(c_3569,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_306,c_3568]) ).
cnf(c_3570,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_308,c_3569]) ).
cnf(c_3571,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_306,c_3570]) ).
cnf(c_3572,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_306,c_3571]) ).
cnf(c_3573,plain,
( op(e4,e4) = op(e4,e2)
| op(op(e2,e4),e4) = op(e4,e2)
| op(e4,e2) = op(e2,e4)
| 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_3572]) ).
cnf(c_3574,plain,
( op(e4,e2) = op(e4,e4)
| op(op(e2,e4),e4) = op(e4,e2)
| op(e4,e2) = op(e2,e4)
| 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_3573]) ).
cnf(c_3575,plain,
( op(e4,e2) = op(e4,e4)
| op(op(e2,e4),e4) = op(e4,e2)
| op(e4,e2) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2) ),
inference(resolve,[status(thm)],[c_1248,c_3574]) ).
cnf(c_1291,plain,
( op(op(e2,e4),e4) = op(e4,e2)
| op(e4,e2) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2) ),
inference(resolve,[status(thm)],[c_281,c_3575]) ).
cnf(c_3576,plain,
( op(e4,e3) = e4
| op(e3,e3) = e4
| op(e2,e3) = e4
| op(e1,e3) = e4
| op(op(op(e4,e2),op(e4,e2)),e3) = e4 ),
inference(paramod,[status(thm)],[c_304,c_83]) ).
cnf(c_3577,plain,
( op(e4,e3) = e4
| op(e3,e3) = e4
| op(e2,e3) = e4
| op(e1,e3) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = e4 ),
inference(paramod,[status(thm)],[c_308,c_3576]) ).
cnf(c_3578,plain,
( op(e4,e3) = e4
| op(e3,e3) = e4
| op(e2,e3) = e4
| op(op(e4,e2),e3) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = e4 ),
inference(paramod,[status(thm)],[c_306,c_3577]) ).
cnf(c_3579,plain,
( op(e4,e3) = e4
| op(e3,e3) = e4
| op(e2,e3) = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = e4 ),
inference(paramod,[status(thm)],[c_308,c_3578]) ).
cnf(c_3580,plain,
( op(e4,e3) = e4
| op(e3,e3) = e4
| op(e2,op(e2,e4)) = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = e4 ),
inference(paramod,[status(thm)],[c_308,c_3579]) ).
cnf(c_3581,plain,
( op(e4,e3) = e4
| op(op(e2,e4),e3) = e4
| op(e2,op(e2,e4)) = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = e4 ),
inference(paramod,[status(thm)],[c_308,c_3580]) ).
cnf(c_3582,plain,
( op(e4,e3) = e4
| op(op(e2,e4),op(e2,e4)) = e4
| op(e2,op(e2,e4)) = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = e4 ),
inference(paramod,[status(thm)],[c_308,c_3581]) ).
cnf(c_1294,plain,
( op(e4,op(e2,e4)) = e4
| op(op(e2,e4),op(e2,e4)) = e4
| op(e2,op(e2,e4)) = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = e4 ),
inference(paramod,[status(thm)],[c_308,c_3582]) ).
cnf(c_3583,plain,
( op(e3,e4) = e4
| op(e3,e3) = e4
| op(e3,e2) = e4
| op(e3,e1) = e4
| op(op(e2,e4),e0) = e4 ),
inference(paramod,[status(thm)],[c_308,c_82]) ).
cnf(c_3584,plain,
( op(e3,e4) = e4
| op(e3,e3) = e4
| op(e3,e2) = e4
| op(e3,e1) = e4
| op(op(e2,e4),op(op(e4,e2),op(e4,e2))) = e4 ),
inference(paramod,[status(thm)],[c_304,c_3583]) ).
cnf(c_3585,plain,
( op(e3,e4) = e4
| op(e3,e3) = e4
| op(e3,e2) = e4
| op(op(e2,e4),e1) = e4
| op(op(e2,e4),op(op(e4,e2),op(e4,e2))) = e4 ),
inference(paramod,[status(thm)],[c_308,c_3584]) ).
cnf(c_3586,plain,
( op(e3,e4) = e4
| op(e3,e3) = e4
| op(e3,e2) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| op(op(e2,e4),op(op(e4,e2),op(e4,e2))) = e4 ),
inference(paramod,[status(thm)],[c_306,c_3585]) ).
cnf(c_3587,plain,
( op(e3,e4) = e4
| op(e3,e3) = e4
| op(op(e2,e4),e2) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| op(op(e2,e4),op(op(e4,e2),op(e4,e2))) = e4 ),
inference(paramod,[status(thm)],[c_308,c_3586]) ).
cnf(c_3588,plain,
( op(e3,e4) = e4
| op(op(e2,e4),e3) = e4
| op(op(e2,e4),e2) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| op(op(e2,e4),op(op(e4,e2),op(e4,e2))) = e4 ),
inference(paramod,[status(thm)],[c_308,c_3587]) ).
cnf(c_3589,plain,
( op(e3,e4) = e4
| op(op(e2,e4),op(e2,e4)) = e4
| op(op(e2,e4),e2) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| op(op(e2,e4),op(op(e4,e2),op(e4,e2))) = e4 ),
inference(paramod,[status(thm)],[c_308,c_3588]) ).
cnf(c_1295,plain,
( op(op(e2,e4),e4) = e4
| op(op(e2,e4),op(e2,e4)) = e4
| op(op(e2,e4),e2) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| op(op(e2,e4),op(op(e4,e2),op(e4,e2))) = e4 ),
inference(paramod,[status(thm)],[c_308,c_3589]) ).
cnf(c_3590,plain,
( op(e4,e2) = e3
| op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(op(op(e4,e2),op(e4,e2)),e2) = e3 ),
inference(paramod,[status(thm)],[c_304,c_71]) ).
cnf(c_3591,plain,
( op(e4,e2) = e3
| op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_308,c_3590]) ).
cnf(c_3592,plain,
( op(e4,e2) = e3
| op(e3,e2) = e3
| op(e2,e2) = e3
| op(op(e4,e2),e2) = e3
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_306,c_3591]) ).
cnf(c_3593,plain,
( op(e4,e2) = e3
| op(e3,e2) = e3
| op(e2,e2) = e3
| op(op(e4,e2),e2) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_308,c_3592]) ).
cnf(c_3594,plain,
( op(e4,e2) = e3
| op(e3,e2) = e3
| op(e2,e2) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_308,c_3593]) ).
cnf(c_3595,plain,
( op(e4,e2) = e3
| op(op(e2,e4),e2) = e3
| op(e2,e2) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_308,c_3594]) ).
cnf(c_3596,plain,
( op(e4,e2) = e3
| op(op(e2,e4),e2) = op(e2,e4)
| op(e2,e2) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_308,c_3595]) ).
cnf(c_3597,plain,
( op(e4,e2) = op(e2,e4)
| op(op(e2,e4),e2) = op(e2,e4)
| op(e2,e2) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_308,c_3596]) ).
cnf(c_1306,plain,
( op(e4,e2) = op(e2,e4)
| op(op(e2,e4),e2) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e2,e4) ),
inference(resolve,[status(thm)],[c_243,c_3597]) ).
cnf(c_3598,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_304,c_66]) ).
cnf(c_3599,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_306,c_3598]) ).
cnf(c_3600,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_306,c_3599]) ).
cnf(c_3601,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_306,c_3600]) ).
cnf(c_3602,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_306,c_3601]) ).
cnf(c_3603,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_308,c_3602]) ).
cnf(c_3604,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_306,c_3603]) ).
cnf(c_3605,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_306,c_3604]) ).
cnf(c_3606,plain,
( op(e4,e2) = op(e2,e4)
| 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(copy,[status(thm)],[c_3605]) ).
cnf(c_3607,plain,
( op(e4,e2) = op(e2,e4)
| 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_1281,c_3606]) ).
cnf(c_1309,plain,
( op(e4,e2) = op(e2,e4)
| op(e2,op(e2,e4)) = op(e4,e2)
| op(e2,op(e4,e2)) = op(e4,e2) ),
inference(resolve,[status(thm)],[c_148,c_3607]) ).
cnf(c_3608,plain,
( op(e4,e1) = e4
| op(e3,e1) = e4
| op(e2,e1) = e4
| op(e1,e1) = e4
| op(op(op(e4,e2),op(e4,e2)),e1) = e4 ),
inference(paramod,[status(thm)],[c_304,c_63]) ).
cnf(c_3609,plain,
( op(e4,e1) = e4
| op(e3,e1) = e4
| op(e2,e1) = e4
| op(e1,e1) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e4 ),
inference(paramod,[status(thm)],[c_306,c_3608]) ).
cnf(c_3610,plain,
( op(e4,e1) = e4
| op(e3,e1) = e4
| op(e2,e1) = e4
| op(op(e4,e2),e1) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e4 ),
inference(paramod,[status(thm)],[c_306,c_3609]) ).
cnf(c_3611,plain,
( op(e4,e1) = e4
| op(e3,e1) = e4
| op(e2,e1) = e4
| op(op(e4,e2),op(e4,e2)) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e4 ),
inference(paramod,[status(thm)],[c_306,c_3610]) ).
cnf(c_3612,plain,
( op(e4,e1) = e4
| op(e3,e1) = e4
| op(e2,op(e4,e2)) = e4
| op(op(e4,e2),op(e4,e2)) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e4 ),
inference(paramod,[status(thm)],[c_306,c_3611]) ).
cnf(c_3613,plain,
( op(e4,e1) = e4
| op(op(e2,e4),e1) = e4
| op(e2,op(e4,e2)) = e4
| op(op(e4,e2),op(e4,e2)) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e4 ),
inference(paramod,[status(thm)],[c_308,c_3612]) ).
cnf(c_3614,plain,
( op(e4,e1) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| op(e2,op(e4,e2)) = e4
| op(op(e4,e2),op(e4,e2)) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e4 ),
inference(paramod,[status(thm)],[c_306,c_3613]) ).
cnf(c_3615,plain,
( op(e4,op(e4,e2)) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| op(e2,op(e4,e2)) = e4
| op(op(e4,e2),op(e4,e2)) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e4 ),
inference(paramod,[status(thm)],[c_306,c_3614]) ).
cnf(c_1312,plain,
( op(e4,op(e4,e2)) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| op(e2,op(e4,e2)) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e4 ),
inference(resolve,[status(thm)],[c_1232,c_3615]) ).
cnf(c_3616,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(op(op(e4,e2),op(e4,e2)),e1) = e3 ),
inference(paramod,[status(thm)],[c_304,c_61]) ).
cnf(c_3617,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e3 ),
inference(paramod,[status(thm)],[c_306,c_3616]) ).
cnf(c_3618,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_308,c_3617]) ).
cnf(c_3619,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(op(e4,e2),e1) = e3
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_306,c_3618]) ).
cnf(c_3620,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(op(e4,e2),op(e4,e2)) = e3
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_306,c_3619]) ).
cnf(c_3621,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_308,c_3620]) ).
cnf(c_3622,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,op(e4,e2)) = e3
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_306,c_3621]) ).
cnf(c_3623,plain,
( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,op(e4,e2)) = op(e2,e4)
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_308,c_3622]) ).
cnf(c_3624,plain,
( op(e4,e1) = e3
| op(op(e2,e4),e1) = e3
| op(e2,op(e4,e2)) = op(e2,e4)
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_308,c_3623]) ).
cnf(c_3625,plain,
( op(e4,e1) = e3
| op(op(e2,e4),op(e4,e2)) = e3
| op(e2,op(e4,e2)) = op(e2,e4)
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_306,c_3624]) ).
cnf(c_3626,plain,
( op(e4,e1) = e3
| op(op(e2,e4),op(e4,e2)) = op(e2,e4)
| op(e2,op(e4,e2)) = op(e2,e4)
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_308,c_3625]) ).
cnf(c_3627,plain,
( op(e4,op(e4,e2)) = e3
| op(op(e2,e4),op(e4,e2)) = op(e2,e4)
| op(e2,op(e4,e2)) = op(e2,e4)
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_306,c_3626]) ).
cnf(c_3628,plain,
( op(e4,op(e4,e2)) = op(e2,e4)
| op(op(e2,e4),op(e4,e2)) = op(e2,e4)
| op(e2,op(e4,e2)) = op(e2,e4)
| op(op(e4,e2),op(e4,e2)) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e2,e4) ),
inference(paramod,[status(thm)],[c_308,c_3627]) ).
cnf(c_1314,plain,
( op(e4,op(e4,e2)) = op(e2,e4)
| op(op(e2,e4),op(e4,e2)) = op(e2,e4)
| op(e2,op(e4,e2)) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e2,e4) ),
inference(resolve,[status(thm)],[c_1233,c_3628]) ).
cnf(c_3629,plain,
( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(op(op(e4,e2),op(e4,e2)),e1) = e2 ),
inference(paramod,[status(thm)],[c_304,c_59]) ).
cnf(c_3630,plain,
( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e2 ),
inference(paramod,[status(thm)],[c_306,c_3629]) ).
cnf(c_3631,plain,
( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| op(op(e4,e2),e1) = e2
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e2 ),
inference(paramod,[status(thm)],[c_306,c_3630]) ).
cnf(c_3632,plain,
( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| op(op(e4,e2),op(e4,e2)) = e2
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e2 ),
inference(paramod,[status(thm)],[c_306,c_3631]) ).
cnf(c_3633,plain,
( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,op(e4,e2)) = e2
| op(op(e4,e2),op(e4,e2)) = e2
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e2 ),
inference(paramod,[status(thm)],[c_306,c_3632]) ).
cnf(c_3634,plain,
( op(e4,e1) = e2
| op(op(e2,e4),e1) = e2
| op(e2,op(e4,e2)) = e2
| op(op(e4,e2),op(e4,e2)) = e2
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e2 ),
inference(paramod,[status(thm)],[c_308,c_3633]) ).
cnf(c_3635,plain,
( op(e4,e1) = e2
| op(op(e2,e4),op(e4,e2)) = e2
| op(e2,op(e4,e2)) = e2
| op(op(e4,e2),op(e4,e2)) = e2
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e2 ),
inference(paramod,[status(thm)],[c_306,c_3634]) ).
cnf(c_3636,plain,
( op(e4,op(e4,e2)) = e2
| op(op(e2,e4),op(e4,e2)) = e2
| op(e2,op(e4,e2)) = e2
| op(op(e4,e2),op(e4,e2)) = e2
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e2 ),
inference(paramod,[status(thm)],[c_306,c_3635]) ).
cnf(c_1316,plain,
( op(e4,op(e4,e2)) = e2
| op(op(e2,e4),op(e4,e2)) = e2
| op(e2,op(e4,e2)) = e2
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e2 ),
inference(resolve,[status(thm)],[c_1234,c_3636]) ).
cnf(c_3637,plain,
( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(op(op(e4,e2),op(e4,e2)),e0) = e1 ),
inference(paramod,[status(thm)],[c_304,c_46]) ).
cnf(c_3638,plain,
( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(op(op(e4,e2),op(e4,e2)),op(op(e4,e2),op(e4,e2))) = e1 ),
inference(paramod,[status(thm)],[c_304,c_3637]) ).
cnf(c_3639,plain,
( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(op(op(e4,e2),op(e4,e2)),op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_306,c_3638]) ).
cnf(c_3640,plain,
( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(op(op(e4,e2),op(e4,e2)),e1) = e1
| op(op(op(e4,e2),op(e4,e2)),op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_304,c_3639]) ).
cnf(c_3641,plain,
( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = e1
| op(op(op(e4,e2),op(e4,e2)),op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_306,c_3640]) ).
cnf(c_3642,plain,
( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_306,c_3641]) ).
cnf(c_3643,plain,
( op(e0,e4) = e1
| op(e0,e3) = e1
| op(op(op(e4,e2),op(e4,e2)),e2) = e1
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_304,c_3642]) ).
cnf(c_3644,plain,
( op(e0,e4) = e1
| op(e0,e3) = e1
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_306,c_3643]) ).
cnf(c_3645,plain,
( op(e0,e4) = e1
| op(op(op(e4,e2),op(e4,e2)),e3) = e1
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_304,c_3644]) ).
cnf(c_3646,plain,
( op(e0,e4) = e1
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = e1
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_308,c_3645]) ).
cnf(c_3647,plain,
( op(e0,e4) = e1
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_306,c_3646]) ).
cnf(c_3648,plain,
( op(op(op(e4,e2),op(e4,e2)),e4) = e1
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_304,c_3647]) ).
cnf(c_3649,plain,
( op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(op(e4,e2),op(e4,e2))) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_306,c_3648]) ).
cnf(c_3650,plain,
( op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e4,e2) ),
inference(resolve,[status(thm)],[c_1285,c_3649]) ).
cnf(c_1325,plain,
( op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e4,e2) ),
inference(resolve,[status(thm)],[c_1269,c_3650]) ).
cnf(c_3651,plain,
( unit = e4
| unit = e3
| unit = e2
| unit = e1
| unit = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_304,c_43]) ).
cnf(c_3652,plain,
( unit = e4
| unit = e3
| unit = e2
| unit = op(e4,e2)
| unit = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_306,c_3651]) ).
cnf(c_3653,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_308,c_3652]) ).
cnf(c_3654,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_3653]) ).
cnf(c_3655,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_3654]) ).
cnf(c_1328,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_3655]) ).
cnf(c_3656,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_304,c_32]) ).
cnf(c_3657,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_306,c_3656]) ).
cnf(c_3658,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_308,c_3657]) ).
cnf(c_3659,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_3658]) ).
cnf(c_3660,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_3659]) ).
cnf(c_3661,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_3660]) ).
cnf(c_3662,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_281,c_3661]) ).
cnf(c_1331,plain,
( op(e4,e4) = e4
| op(e4,e4) = e2
| op(op(e4,e2),op(e4,e2)) = op(e4,e4) ),
inference(resolve,[status(thm)],[c_186,c_3662]) ).
cnf(c_3663,plain,
( op(e4,e3) = e4
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e1
| op(e4,op(e2,e4)) = e0 ),
inference(paramod,[status(thm)],[c_308,c_31]) ).
cnf(c_3664,plain,
( op(e4,e3) = e4
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e1
| op(e4,op(e2,e4)) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_304,c_3663]) ).
cnf(c_3665,plain,
( op(e4,e3) = e4
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,op(e2,e4)) = e1
| op(e4,op(e2,e4)) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_308,c_3664]) ).
cnf(c_3666,plain,
( op(e4,e3) = e4
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,op(e2,e4)) = op(e4,e2)
| op(e4,op(e2,e4)) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_306,c_3665]) ).
cnf(c_3667,plain,
( op(e4,e3) = e4
| op(e4,e3) = e3
| op(e4,op(e2,e4)) = e2
| op(e4,op(e2,e4)) = op(e4,e2)
| op(e4,op(e2,e4)) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_308,c_3666]) ).
cnf(c_3668,plain,
( op(e4,e3) = e4
| op(e4,op(e2,e4)) = e3
| op(e4,op(e2,e4)) = e2
| op(e4,op(e2,e4)) = op(e4,e2)
| op(e4,op(e2,e4)) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_308,c_3667]) ).
cnf(c_3669,plain,
( op(e4,e3) = e4
| op(e4,op(e2,e4)) = op(e2,e4)
| op(e4,op(e2,e4)) = e2
| op(e4,op(e2,e4)) = op(e4,e2)
| op(e4,op(e2,e4)) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_308,c_3668]) ).
cnf(c_3670,plain,
( op(e4,op(e2,e4)) = e4
| op(e4,op(e2,e4)) = op(e2,e4)
| op(e4,op(e2,e4)) = e2
| op(e4,op(e2,e4)) = op(e4,e2)
| op(e4,op(e2,e4)) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_308,c_3669]) ).
cnf(c_1332,plain,
( op(e4,op(e2,e4)) = e4
| op(e4,op(e2,e4)) = op(e2,e4)
| op(e4,op(e2,e4)) = e2
| op(e4,op(e2,e4)) = op(e4,e2)
| op(op(e4,e2),op(e4,e2)) = op(e4,op(e2,e4)) ),
inference(copy,[status(thm)],[c_3670]) ).
cnf(c_3671,plain,
( op(e2,e2) = e4
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_304,c_20]) ).
cnf(c_3672,plain,
( op(e2,e2) = e4
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = op(e4,e2)
| op(e2,e2) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_306,c_3671]) ).
cnf(c_3673,plain,
( op(e2,e2) = e4
| op(e2,e2) = op(e2,e4)
| op(e2,e2) = e2
| op(e2,e2) = op(e4,e2)
| op(e2,e2) = op(op(e4,e2),op(e4,e2)) ),
inference(paramod,[status(thm)],[c_308,c_3672]) ).
cnf(c_3674,plain,
( op(e2,e2) = e4
| op(e2,e2) = op(e2,e4)
| op(e2,e2) = e2
| op(e2,e2) = op(e4,e2)
| op(op(e4,e2),op(e4,e2)) = op(e2,e2) ),
inference(copy,[status(thm)],[c_3673]) ).
cnf(c_3675,plain,
( op(e2,e2) = e4
| op(e2,e2) = op(e2,e4)
| op(e2,e2) = e2
| op(op(e4,e2),op(e4,e2)) = op(e2,e2) ),
inference(resolve,[status(thm)],[c_148,c_3674]) ).
cnf(c_1341,plain,
( op(e2,e2) = e4
| op(e2,e2) = e2
| op(op(e4,e2),op(e4,e2)) = op(e2,e2) ),
inference(resolve,[status(thm)],[c_243,c_3675]) ).
cnf(c_1352,plain,
op(e4,e2) != e4,
inference(paramod,[status(thm)],[c_306,c_296]) ).
cnf(c_3676,plain,
op(e4,e2) != e3,
inference(paramod,[status(thm)],[c_306,c_294]) ).
cnf(c_1353,plain,
op(e4,e2) != op(e2,e4),
inference(paramod,[status(thm)],[c_308,c_3676]) ).
cnf(c_1354,plain,
op(e4,e2) != e2,
inference(paramod,[status(thm)],[c_306,c_292]) ).
cnf(c_1361,plain,
op(e2,op(e4,e2)) != op(e2,e4),
inference(paramod,[status(thm)],[c_306,c_239]) ).
cnf(c_3677,plain,
op(op(e4,e2),unit) = e1,
inference(paramod,[status(thm)],[c_306,c_36]) ).
cnf(c_1384,plain,
op(op(e4,e2),unit) = op(e4,e2),
inference(paramod,[status(thm)],[c_306,c_3677]) ).
cnf(c_3678,plain,
op(unit,op(e4,e2)) = e1,
inference(paramod,[status(thm)],[c_306,c_35]) ).
cnf(c_1385,plain,
op(unit,op(e4,e2)) = op(e4,e2),
inference(paramod,[status(thm)],[c_306,c_3678]) ).
cnf(c_1386,plain,
op(e2,e4) != e4,
inference(paramod,[status(thm)],[c_308,c_302]) ).
cnf(c_3679,plain,
e2 != op(e2,e4),
inference(paramod,[status(thm)],[c_308,c_298]) ).
cnf(c_1387,plain,
op(e2,e4) != e2,
inference(copy,[status(thm)],[c_3679]) ).
cnf(c_1388,plain,
op(e4,op(e2,e4)) != op(e4,e4),
inference(paramod,[status(thm)],[c_308,c_283]) ).
cnf(c_3680,plain,
op(e4,e2) != op(e4,op(e2,e4)),
inference(paramod,[status(thm)],[c_308,c_279]) ).
cnf(c_1389,plain,
op(e4,op(e2,e4)) != op(e4,e2),
inference(copy,[status(thm)],[c_3680]) ).
cnf(c_3681,plain,
op(e2,e4) != op(op(e2,e4),e4),
inference(paramod,[status(thm)],[c_308,c_184]) ).
cnf(c_1396,plain,
op(op(e2,e4),e4) != op(e2,e4),
inference(copy,[status(thm)],[c_3681]) ).
cnf(c_3682,plain,
op(op(e2,e4),unit) = e3,
inference(paramod,[status(thm)],[c_308,c_40]) ).
cnf(c_1402,plain,
op(op(e2,e4),unit) = op(e2,e4),
inference(paramod,[status(thm)],[c_308,c_3682]) ).
cnf(c_3683,plain,
op(unit,op(e2,e4)) = e3,
inference(paramod,[status(thm)],[c_308,c_39]) ).
cnf(c_1403,plain,
op(unit,op(e2,e4)) = op(e2,e4),
inference(paramod,[status(thm)],[c_308,c_3683]) ).
cnf(c_1560,negated_conjecture,
( op(op(e4,op(e2,e4)),e4) != op(e2,e4)
| op(op(e4,e2),e2) = e4
| op(op(e4,op(e4,e2)),op(e4,e2)) = e4
| op(op(op(e4,e2),op(e4,e2)),e4) != op(e4,op(op(e4,e2),op(e4,e2)))
| op(op(op(e2,e4),e4),e4) = op(e2,e4)
| op(op(op(e2,e4),e2),e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_1205,c_686]) ).
cnf(c_1678,negated_conjecture,
op(e4,e4) != e2,
inference(resolve,[status(thm)],[c_1352,c_341]) ).
cnf(c_1681,plain,
( op(e2,op(e2,e4)) = op(e4,e2)
| op(e2,op(e4,e2)) = op(e4,e2) ),
inference(resolve,[status(thm)],[c_1353,c_1309]) ).
cnf(c_1682,plain,
( op(op(e2,e4),e2) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),e2) = op(e2,e4) ),
inference(resolve,[status(thm)],[c_1353,c_1306]) ).
cnf(c_1683,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_1353,c_1291]) ).
cnf(c_1692,plain,
( op(e4,op(e4,e2)) = op(e2,e4)
| op(op(e2,e4),op(e4,e2)) = op(e2,e4)
| op(op(op(e4,e2),op(e4,e2)),op(e4,e2)) = op(e2,e4) ),
inference(resolve,[status(thm)],[c_1361,c_1314]) ).
cnf(c_3684,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_1387,c_1289]) ).
cnf(c_1706,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_1678,c_3684]) ).
cnf(c_1707,negated_conjecture,
op(e2,e2) != e4,
inference(resolve,[status(thm)],[c_1387,c_329]) ).
cnf(c_1708,plain,
( op(e4,op(e2,e4)) = e4
| op(e4,op(e2,e4)) = op(e2,e4)
| op(e4,op(e2,e4)) = e2
| op(op(e4,e2),op(e4,e2)) = op(e4,op(e2,e4)) ),
inference(resolve,[status(thm)],[c_1389,c_1332]) ).
cnf(c_1714,negated_conjecture,
op(op(e2,e4),op(e2,e4)) != e4,
inference(resolve,[status(thm)],[c_1396,c_337]) ).
cnf(c_1717,negated_conjecture,
( op(e4,e4) = e4
| op(op(e4,e2),op(e4,e2)) = op(e4,e4) ),
inference(resolve,[status(thm)],[c_1678,c_1331]) ).
cnf(c_1720,negated_conjecture,
( op(e2,e2) = e2
| op(op(e4,e2),op(e4,e2)) = op(e2,e2) ),
inference(resolve,[status(thm)],[c_1707,c_1341]) ).
cnf(c_1722,negated_conjecture,
( op(op(e2,e4),e4) = e4
| op(op(e2,e4),e2) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| op(op(e2,e4),op(op(e4,e2),op(e4,e2))) = e4 ),
inference(resolve,[status(thm)],[c_1714,c_1295]) ).
cnf(c_1723,negated_conjecture,
( op(e4,op(e2,e4)) = e4
| op(e2,op(e2,e4)) = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = e4 ),
inference(resolve,[status(thm)],[c_1714,c_1294]) ).
cnf(c_3685,plain,
( op(e4,e2) != op(e2,op(e4,e2))
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_1325,c_1275]) ).
cnf(c_1731,plain,
( op(e2,op(e4,e2)) != op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = op(e4,e2) ),
inference(copy,[status(thm)],[c_3685]) ).
cnf(c_3686,plain,
( op(e4,e2) = e2
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(paramod,[status(thm)],[c_1328,c_37]) ).
cnf(c_1733,plain,
( op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(resolve,[status(thm)],[c_1354,c_3686]) ).
cnf(c_3687,plain,
( op(e2,e4) = e4
| unit = e4
| op(e2,e4) = unit
| op(e4,e2) = unit
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(paramod,[status(thm)],[c_1328,c_41]) ).
cnf(c_1734,plain,
( unit = e4
| op(e2,e4) = unit
| op(e4,e2) = unit
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(resolve,[status(thm)],[c_1386,c_3687]) ).
cnf(c_3688,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_1328,c_304]) ).
cnf(c_3689,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_304,c_3688]) ).
cnf(c_3690,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_1385,c_3689]) ).
cnf(c_1739,plain,
( unit = e4
| op(e2,e4) = unit
| unit = e2
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(resolve,[status(thm)],[c_1235,c_3690]) ).
cnf(c_2356,plain,
( op(e2,op(e4,e4)) != op(e2,e2)
| op(e4,e4) = e4 ),
inference(paramod,[status(thm)],[c_1717,c_1246]) ).
cnf(c_2597,plain,
( op(e4,e4) = e4
| op(e2,e2) = op(e4,e4)
| op(e2,e2) = e2 ),
inference(paramod,[status(thm)],[c_1720,c_1717]) ).
cnf(c_3691,plain,
( e4 = op(e4,e2)
| op(e2,op(e4,e2)) = op(e4,e2)
| op(e4,op(e2,e4)) = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = e4 ),
inference(paramod,[status(thm)],[c_1723,c_1681]) ).
cnf(c_3692,plain,
( op(e4,e2) = e4
| op(e2,op(e4,e2)) = op(e4,e2)
| op(e4,op(e2,e4)) = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = e4 ),
inference(copy,[status(thm)],[c_3691]) ).
cnf(c_2618,plain,
( op(e2,op(e4,e2)) = op(e4,e2)
| op(e4,op(e2,e4)) = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = e4 ),
inference(resolve,[status(thm)],[c_1352,c_3692]) ).
cnf(c_2674,plain,
( op(e2,op(e2,e4)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),op(e2,e4)) = op(e4,e2) ),
inference(resolve,[status(thm)],[c_1731,c_1681]) ).
cnf(c_3693,plain,
( op(e4,op(op(e4,e2),op(e4,e2))) = e4
| unit != op(e4,e4)
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_1733,c_339]) ).
cnf(c_2691,plain,
( op(e4,op(op(e4,e2),op(e4,e2))) = e4
| op(e4,e4) != unit
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(copy,[status(thm)],[c_3693]) ).
cnf(c_3694,plain,
( op(e4,op(e4,e2)) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| op(e2,op(e4,e2)) = e4
| op(unit,op(e4,e2)) = e4
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_1733,c_1312]) ).
cnf(c_3695,plain,
( op(e4,op(e4,e2)) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| op(e2,op(e4,e2)) = e4
| op(e4,e2) = e4
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_1385,c_3694]) ).
cnf(c_2747,plain,
( op(e4,op(e4,e2)) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| op(e2,op(e4,e2)) = e4
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(resolve,[status(thm)],[c_1352,c_3695]) ).
cnf(c_3696,plain,
( op(e4,op(e4,e2)) = e2
| op(op(e2,e4),op(e4,e2)) = e2
| op(e2,op(e4,e2)) = e2
| op(unit,op(e4,e2)) = e2
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_1733,c_1316]) ).
cnf(c_3697,plain,
( op(e4,op(e4,e2)) = e2
| op(op(e2,e4),op(e4,e2)) = e2
| op(e2,op(e4,e2)) = e2
| op(e4,e2) = e2
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_1385,c_3696]) ).
cnf(c_2748,plain,
( op(e4,op(e4,e2)) = e2
| op(op(e2,e4),op(e4,e2)) = e2
| op(e2,op(e4,e2)) = e2
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(resolve,[status(thm)],[c_1354,c_3697]) ).
cnf(c_3698,plain,
( op(op(e2,e4),e2) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(unit,e2) = op(e2,e4)
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_1733,c_1682]) ).
cnf(c_3699,plain,
( op(op(e2,e4),e2) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| e2 = op(e2,e4)
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_37,c_3698]) ).
cnf(c_3700,plain,
( op(op(e2,e4),e2) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(e2,e4) = e2
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(copy,[status(thm)],[c_3699]) ).
cnf(c_2759,plain,
( op(op(e2,e4),e2) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(resolve,[status(thm)],[c_1387,c_3700]) ).
cnf(c_3701,plain,
( op(e4,op(e4,e2)) = op(e2,e4)
| op(op(e2,e4),op(e4,e2)) = op(e2,e4)
| op(unit,op(e4,e2)) = op(e2,e4)
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_1733,c_1692]) ).
cnf(c_3702,plain,
( op(e4,op(e4,e2)) = op(e2,e4)
| op(op(e2,e4),op(e4,e2)) = op(e2,e4)
| op(e4,e2) = op(e2,e4)
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_1385,c_3701]) ).
cnf(c_2763,plain,
( op(e4,op(e4,e2)) = op(e2,e4)
| op(op(e2,e4),op(e4,e2)) = op(e2,e4)
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(resolve,[status(thm)],[c_1353,c_3702]) ).
cnf(c_3703,plain,
( op(op(e2,e4),e4) = e2
| op(op(e4,e2),e4) = e2
| op(unit,e4) = e2
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_1733,c_1706]) ).
cnf(c_3704,plain,
( op(op(e2,e4),e4) = e2
| op(op(e4,e2),e4) = e2
| e4 = e2
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_41,c_3703]) ).
cnf(c_3705,plain,
( op(op(e2,e4),e4) = e2
| op(op(e4,e2),e4) = e2
| e2 = e4
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(copy,[status(thm)],[c_3704]) ).
cnf(c_2768,plain,
( op(op(e2,e4),e4) = e2
| op(op(e4,e2),e4) = e2
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(resolve,[status(thm)],[c_300,c_3705]) ).
cnf(c_3706,plain,
( op(e4,op(e2,e4)) = e4
| op(e4,op(e2,e4)) = op(e2,e4)
| op(e4,op(e2,e4)) = e2
| unit = op(e4,op(e2,e4))
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_1733,c_1708]) ).
cnf(c_2769,plain,
( op(e4,op(e2,e4)) = e4
| op(e4,op(e2,e4)) = op(e2,e4)
| op(e4,op(e2,e4)) = e2
| op(e4,op(e2,e4)) = unit
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(copy,[status(thm)],[c_3706]) ).
cnf(c_3707,plain,
( op(op(e2,e4),e4) = e4
| op(op(e2,e4),e2) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| op(op(e2,e4),unit) = e4
| unit = e4
| op(e2,e4) = unit
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_1734,c_1722]) ).
cnf(c_3708,plain,
( op(op(e2,e4),e4) = e4
| op(op(e2,e4),e2) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| op(e2,e4) = e4
| unit = e4
| op(e2,e4) = unit
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_1402,c_3707]) ).
cnf(c_2872,plain,
( op(op(e2,e4),e4) = e4
| op(op(e2,e4),e2) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| unit = e4
| op(e2,e4) = unit
| op(e4,e2) = unit ),
inference(resolve,[status(thm)],[c_1386,c_3708]) ).
cnf(c_3709,plain,
( op(e4,unit) != op(e4,e4)
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_1739,c_1236]) ).
cnf(c_3710,plain,
( e4 != op(e4,e4)
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_42,c_3709]) ).
cnf(c_2890,plain,
( op(e4,e4) != e4
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(copy,[status(thm)],[c_3710]) ).
cnf(c_3711,plain,
( op(e4,unit) != op(e4,op(e2,e4))
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_1739,c_1237]) ).
cnf(c_3712,plain,
( e4 != op(e4,op(e2,e4))
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_42,c_3711]) ).
cnf(c_2891,plain,
( op(e4,op(e2,e4)) != e4
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(copy,[status(thm)],[c_3712]) ).
cnf(c_3713,plain,
( op(op(e2,e4),unit) != op(op(e2,e4),e2)
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_1739,c_1242]) ).
cnf(c_3714,plain,
( op(e2,e4) != op(op(e2,e4),e2)
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_1402,c_3713]) ).
cnf(c_2899,plain,
( op(op(e2,e4),e2) != op(e2,e4)
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(copy,[status(thm)],[c_3714]) ).
cnf(c_3715,plain,
( op(op(e2,e4),unit) != op(op(e2,e4),op(e4,e2))
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_1739,c_1243]) ).
cnf(c_3716,plain,
( op(e2,e4) != op(op(e2,e4),op(e4,e2))
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_1402,c_3715]) ).
cnf(c_2902,plain,
( op(op(e2,e4),op(e4,e2)) != op(e2,e4)
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(copy,[status(thm)],[c_3716]) ).
cnf(c_3717,plain,
( op(e2,unit) != op(e2,e2)
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_1739,c_1246]) ).
cnf(c_3718,plain,
( e2 != op(e2,e2)
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_38,c_3717]) ).
cnf(c_2906,plain,
( op(e2,e2) != e2
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(copy,[status(thm)],[c_3718]) ).
cnf(c_3719,plain,
( op(e2,unit) != op(e2,op(e4,e2))
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_1739,c_1247]) ).
cnf(c_3720,plain,
( e2 != op(e2,op(e4,e2))
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_38,c_3719]) ).
cnf(c_2907,plain,
( op(e2,op(e4,e2)) != e2
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(copy,[status(thm)],[c_3720]) ).
cnf(c_3721,plain,
( op(unit,op(e2,e4)) != op(e4,op(e2,e4))
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_1739,c_1265]) ).
cnf(c_3722,plain,
( op(e2,e4) != op(e4,op(e2,e4))
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_1403,c_3721]) ).
cnf(c_2927,plain,
( op(e4,op(e2,e4)) != op(e2,e4)
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(copy,[status(thm)],[c_3722]) ).
cnf(c_3723,plain,
( op(op(e2,e4),e4) = op(e4,e2)
| op(unit,e4) = op(e4,e2)
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_1739,c_1683]) ).
cnf(c_3724,plain,
( op(op(e2,e4),e4) = op(e4,e2)
| e4 = op(e4,e2)
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_41,c_3723]) ).
cnf(c_3725,plain,
( op(op(e2,e4),e4) = op(e4,e2)
| op(e4,e2) = e4
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(copy,[status(thm)],[c_3724]) ).
cnf(c_2958,plain,
( op(op(e2,e4),e4) = op(e4,e2)
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(resolve,[status(thm)],[c_1352,c_3725]) ).
cnf(c_3726,plain,
( op(e4,e4) = e4
| unit = op(e4,e4)
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_1739,c_1717]) ).
cnf(c_2971,plain,
( op(e4,e4) = e4
| op(e4,e4) = unit
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(copy,[status(thm)],[c_3726]) ).
cnf(c_3727,plain,
( e2 != e2
| unit = e4
| op(e2,e4) = unit
| unit = e2
| op(op(e4,e2),op(e4,e2)) = op(e2,e2) ),
inference(paramod,[status(thm)],[c_1720,c_2906]) ).
cnf(c_2982,plain,
( unit = e4
| op(e2,e4) = unit
| unit = e2
| op(op(e4,e2),op(e4,e2)) = op(e2,e2) ),
inference(copy,[status(thm)],[c_3727]) ).
cnf(c_3728,plain,
( op(op(e4,e2),unit) != op(e4,e2)
| op(e4,e4) = e4
| op(e4,e4) = unit
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_2971,c_1249]) ).
cnf(c_3729,plain,
( op(e4,e2) != op(e4,e2)
| op(e4,e4) = e4
| op(e4,e4) = unit
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_1384,c_3728]) ).
cnf(c_3004,plain,
( op(e4,e4) = e4
| op(e4,e4) = unit
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_3729]) ).
cnf(c_3730,plain,
( e4 != e4
| unit = e4
| op(e2,e4) = unit
| unit = e2
| op(e4,e4) = unit
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_2971,c_2890]) ).
cnf(c_3731,plain,
( unit = e4
| op(e2,e4) = unit
| unit = e2
| op(e4,e4) = unit
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(copy,[status(thm)],[c_3730]) ).
cnf(c_3732,plain,
( unit = e4
| op(e2,e4) = unit
| op(e4,e4) = unit
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(copy,[status(thm)],[c_3731]) ).
cnf(c_3733,plain,
( unit = e4
| op(e4,e4) = unit
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(copy,[status(thm)],[c_3732]) ).
cnf(c_3017,plain,
( op(e4,e4) = unit
| unit = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(copy,[status(thm)],[c_3733]) ).
cnf(c_3734,plain,
( op(e4,e2) = e2
| op(e4,e4) = e4
| op(e4,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_3004,c_37]) ).
cnf(c_3019,plain,
( op(e4,e4) = e4
| op(e4,e4) = unit
| unit = e2 ),
inference(resolve,[status(thm)],[c_1354,c_3734]) ).
cnf(c_3735,plain,
( op(e2,e4) = e4
| op(e4,e4) = e4
| op(e4,e4) = unit ),
inference(paramod,[status(thm)],[c_3019,c_41]) ).
cnf(c_3047,plain,
( op(e4,e4) = e4
| op(e4,e4) = unit ),
inference(resolve,[status(thm)],[c_1386,c_3735]) ).
cnf(c_3736,plain,
( op(e2,unit) != op(e2,e2)
| op(e4,e4) = e4
| op(e4,e4) = e4 ),
inference(paramod,[status(thm)],[c_3047,c_2356]) ).
cnf(c_3737,plain,
( e2 != op(e2,e2)
| op(e4,e4) = e4
| op(e4,e4) = e4 ),
inference(paramod,[status(thm)],[c_38,c_3736]) ).
cnf(c_3738,plain,
( op(e2,e2) != e2
| op(e4,e4) = e4
| op(e4,e4) = e4 ),
inference(copy,[status(thm)],[c_3737]) ).
cnf(c_3100,plain,
( op(e2,e2) != e2
| op(e4,e4) = e4 ),
inference(copy,[status(thm)],[c_3738]) ).
cnf(c_3739,plain,
( e2 != e2
| op(e4,e4) = e4
| op(e4,e4) = e4
| op(e2,e2) = op(e4,e4) ),
inference(paramod,[status(thm)],[c_2597,c_3100]) ).
cnf(c_3740,plain,
( op(e4,e4) = e4
| op(e4,e4) = e4
| op(e2,e2) = op(e4,e4) ),
inference(copy,[status(thm)],[c_3739]) ).
cnf(c_3116,plain,
( op(e4,e4) = e4
| op(e2,e2) = op(e4,e4) ),
inference(copy,[status(thm)],[c_3740]) ).
cnf(c_3741,plain,
( op(e4,e4) = e4
| op(e2,e2) = unit
| op(e4,e4) = e4 ),
inference(paramod,[status(thm)],[c_3047,c_3116]) ).
cnf(c_3141,plain,
( op(e2,e2) = unit
| op(e4,e4) = e4 ),
inference(copy,[status(thm)],[c_3741]) ).
cnf(c_3742,plain,
( op(op(e4,e2),unit) != op(e4,e2)
| op(e4,e4) = unit
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_3017,c_1249]) ).
cnf(c_3743,plain,
( op(e4,e2) != op(e4,e2)
| op(e4,e4) = unit
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_1384,c_3742]) ).
cnf(c_3187,plain,
( op(e4,e4) = unit
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_3743]) ).
cnf(c_3744,plain,
( op(e4,e2) = e2
| op(e4,e4) = unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_3187,c_37]) ).
cnf(c_3195,plain,
( op(e4,e4) = unit
| unit = e2 ),
inference(resolve,[status(thm)],[c_1354,c_3744]) ).
cnf(c_3745,plain,
( op(e2,e2) = unit
| unit = e4
| unit = e4
| unit = e2 ),
inference(paramod,[status(thm)],[c_3187,c_3141]) ).
cnf(c_3212,plain,
( op(e2,e2) = unit
| unit = e4
| unit = e2 ),
inference(copy,[status(thm)],[c_3745]) ).
cnf(c_3746,plain,
( op(e2,e4) = e4
| op(e4,e4) = unit ),
inference(paramod,[status(thm)],[c_3195,c_41]) ).
cnf(c_3214,plain,
op(e4,e4) = unit,
inference(resolve,[status(thm)],[c_1386,c_3746]) ).
cnf(c_3218,plain,
( op(e4,op(op(e4,e2),op(e4,e2))) != unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_3195,c_1236]) ).
cnf(c_3747,plain,
( op(e4,op(op(e4,e2),op(e4,e2))) = e4
| unit != unit
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_3214,c_2691]) ).
cnf(c_3258,plain,
( op(e4,op(op(e4,e2),op(e4,e2))) = e4
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(copy,[status(thm)],[c_3747]) ).
cnf(c_3373,negated_conjecture,
unit != e2,
inference(paramod,[status(thm)],[c_3214,c_1678]) ).
cnf(c_3375,plain,
op(e4,op(e2,e4)) != unit,
inference(paramod,[status(thm)],[c_3214,c_1388]) ).
cnf(c_3381,plain,
op(e4,e2) != unit,
inference(paramod,[status(thm)],[c_3214,c_281]) ).
cnf(c_3382,plain,
op(e2,e4) != unit,
inference(paramod,[status(thm)],[c_3214,c_186]) ).
cnf(c_3748,plain,
( op(e4,op(op(e4,e2),op(e4,e2))) = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(resolve,[status(thm)],[c_3381,c_3258]) ).
cnf(c_3749,negated_conjecture,
( op(e4,op(op(e4,e2),op(e4,e2))) = e4
| op(e2,e4) = unit ),
inference(resolve,[status(thm)],[c_3373,c_3748]) ).
cnf(c_3383,negated_conjecture,
op(e4,op(op(e4,e2),op(e4,e2))) = e4,
inference(resolve,[status(thm)],[c_3382,c_3749]) ).
cnf(c_3750,plain,
( e4 != unit
| unit = e2 ),
inference(paramod,[status(thm)],[c_3383,c_3218]) ).
cnf(c_3751,plain,
( unit != e4
| unit = e2 ),
inference(copy,[status(thm)],[c_3750]) ).
cnf(c_3385,negated_conjecture,
unit != e4,
inference(resolve,[status(thm)],[c_3373,c_3751]) ).
cnf(c_3752,negated_conjecture,
( op(e2,e2) = unit
| unit = e4 ),
inference(resolve,[status(thm)],[c_3373,c_3212]) ).
cnf(c_3386,negated_conjecture,
op(e2,e2) = unit,
inference(resolve,[status(thm)],[c_3385,c_3752]) ).
cnf(c_3753,plain,
( unit = e4
| op(e2,e4) = unit
| unit = e2
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(paramod,[status(thm)],[c_3386,c_2982]) ).
cnf(c_3754,negated_conjecture,
( unit = e4
| op(e2,e4) = unit
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(resolve,[status(thm)],[c_3373,c_3753]) ).
cnf(c_3755,negated_conjecture,
( unit = e4
| op(op(e4,e2),op(e4,e2)) = unit ),
inference(resolve,[status(thm)],[c_3382,c_3754]) ).
cnf(c_3397,negated_conjecture,
op(op(e4,e2),op(e4,e2)) = unit,
inference(resolve,[status(thm)],[c_3385,c_3755]) ).
cnf(c_3756,negated_conjecture,
( op(op(e2,e4),e4) = op(e4,e2)
| unit = e4
| op(e2,e4) = unit ),
inference(resolve,[status(thm)],[c_3373,c_2958]) ).
cnf(c_3757,negated_conjecture,
( op(op(e2,e4),e4) = op(e4,e2)
| unit = e4 ),
inference(resolve,[status(thm)],[c_3382,c_3756]) ).
cnf(c_3410,negated_conjecture,
op(op(e2,e4),e4) = op(e4,e2),
inference(resolve,[status(thm)],[c_3385,c_3757]) ).
cnf(c_3758,negated_conjecture,
( op(e4,op(e2,e4)) != op(e2,e4)
| unit = e4
| op(e2,e4) = unit ),
inference(resolve,[status(thm)],[c_3373,c_2927]) ).
cnf(c_3759,negated_conjecture,
( op(e4,op(e2,e4)) != op(e2,e4)
| unit = e4 ),
inference(resolve,[status(thm)],[c_3382,c_3758]) ).
cnf(c_3426,negated_conjecture,
op(e4,op(e2,e4)) != op(e2,e4),
inference(resolve,[status(thm)],[c_3385,c_3759]) ).
cnf(c_3760,negated_conjecture,
( op(e2,op(e4,e2)) != e2
| unit = e4
| op(e2,e4) = unit ),
inference(resolve,[status(thm)],[c_3373,c_2907]) ).
cnf(c_3761,negated_conjecture,
( op(e2,op(e4,e2)) != e2
| unit = e4 ),
inference(resolve,[status(thm)],[c_3382,c_3760]) ).
cnf(c_3428,negated_conjecture,
op(e2,op(e4,e2)) != e2,
inference(resolve,[status(thm)],[c_3385,c_3761]) ).
cnf(c_3762,negated_conjecture,
( op(op(e2,e4),op(e4,e2)) != op(e2,e4)
| unit = e4
| op(e2,e4) = unit ),
inference(resolve,[status(thm)],[c_3373,c_2902]) ).
cnf(c_3763,negated_conjecture,
( op(op(e2,e4),op(e4,e2)) != op(e2,e4)
| unit = e4 ),
inference(resolve,[status(thm)],[c_3382,c_3762]) ).
cnf(c_3430,negated_conjecture,
op(op(e2,e4),op(e4,e2)) != op(e2,e4),
inference(resolve,[status(thm)],[c_3385,c_3763]) ).
cnf(c_3764,negated_conjecture,
( op(op(e2,e4),e2) != op(e2,e4)
| unit = e4
| op(e2,e4) = unit ),
inference(resolve,[status(thm)],[c_3373,c_2899]) ).
cnf(c_3765,negated_conjecture,
( op(op(e2,e4),e2) != op(e2,e4)
| unit = e4 ),
inference(resolve,[status(thm)],[c_3382,c_3764]) ).
cnf(c_3431,negated_conjecture,
op(op(e2,e4),e2) != op(e2,e4),
inference(resolve,[status(thm)],[c_3385,c_3765]) ).
cnf(c_3766,negated_conjecture,
( op(e4,op(e2,e4)) != e4
| unit = e4
| op(e2,e4) = unit ),
inference(resolve,[status(thm)],[c_3373,c_2891]) ).
cnf(c_3767,negated_conjecture,
( op(e4,op(e2,e4)) != e4
| unit = e4 ),
inference(resolve,[status(thm)],[c_3382,c_3766]) ).
cnf(c_3434,negated_conjecture,
op(e4,op(e2,e4)) != e4,
inference(resolve,[status(thm)],[c_3385,c_3767]) ).
cnf(c_3768,plain,
( op(e4,op(e2,e4)) = e4
| op(e4,op(e2,e4)) = op(e2,e4)
| op(e4,op(e2,e4)) = e2
| op(e4,op(e2,e4)) = unit
| op(e2,e4) = unit
| unit = e2 ),
inference(resolve,[status(thm)],[c_3381,c_2769]) ).
cnf(c_3769,negated_conjecture,
( op(e4,op(e2,e4)) = e4
| op(e4,op(e2,e4)) = op(e2,e4)
| op(e4,op(e2,e4)) = e2
| op(e4,op(e2,e4)) = unit
| op(e2,e4) = unit ),
inference(resolve,[status(thm)],[c_3373,c_3768]) ).
cnf(c_3770,negated_conjecture,
( op(e4,op(e2,e4)) = e4
| op(e4,op(e2,e4)) = op(e2,e4)
| op(e4,op(e2,e4)) = e2
| op(e4,op(e2,e4)) = unit ),
inference(resolve,[status(thm)],[c_3382,c_3769]) ).
cnf(c_3771,negated_conjecture,
( op(e4,op(e2,e4)) = e4
| op(e4,op(e2,e4)) = op(e2,e4)
| op(e4,op(e2,e4)) = e2 ),
inference(resolve,[status(thm)],[c_3375,c_3770]) ).
cnf(c_3772,negated_conjecture,
( op(e4,op(e2,e4)) = e4
| op(e4,op(e2,e4)) = e2 ),
inference(resolve,[status(thm)],[c_3426,c_3771]) ).
cnf(c_3439,negated_conjecture,
op(e4,op(e2,e4)) = e2,
inference(resolve,[status(thm)],[c_3434,c_3772]) ).
cnf(c_3773,plain,
( op(e4,e2) = e2
| op(op(e4,e2),e4) = e2
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_3410,c_2768]) ).
cnf(c_3774,plain,
( op(e4,e2) = e2
| op(op(e4,e2),e4) = e2
| op(e2,e4) = unit
| unit = e2 ),
inference(resolve,[status(thm)],[c_3381,c_3773]) ).
cnf(c_3775,negated_conjecture,
( op(e4,e2) = e2
| op(op(e4,e2),e4) = e2
| op(e2,e4) = unit ),
inference(resolve,[status(thm)],[c_3373,c_3774]) ).
cnf(c_3776,negated_conjecture,
( op(e4,e2) = e2
| op(op(e4,e2),e4) = e2 ),
inference(resolve,[status(thm)],[c_3382,c_3775]) ).
cnf(c_3440,negated_conjecture,
op(op(e4,e2),e4) = e2,
inference(resolve,[status(thm)],[c_1354,c_3776]) ).
cnf(c_3777,plain,
( op(e4,op(e4,e2)) = op(e2,e4)
| op(op(e2,e4),op(e4,e2)) = op(e2,e4)
| op(e2,e4) = unit
| unit = e2 ),
inference(resolve,[status(thm)],[c_3381,c_2763]) ).
cnf(c_3778,negated_conjecture,
( op(e4,op(e4,e2)) = op(e2,e4)
| op(op(e2,e4),op(e4,e2)) = op(e2,e4)
| op(e2,e4) = unit ),
inference(resolve,[status(thm)],[c_3373,c_3777]) ).
cnf(c_3779,negated_conjecture,
( op(e4,op(e4,e2)) = op(e2,e4)
| op(op(e2,e4),op(e4,e2)) = op(e2,e4) ),
inference(resolve,[status(thm)],[c_3382,c_3778]) ).
cnf(c_3441,negated_conjecture,
op(e4,op(e4,e2)) = op(e2,e4),
inference(resolve,[status(thm)],[c_3430,c_3779]) ).
cnf(c_3780,plain,
( op(op(e2,e4),e2) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(e2,e4) = unit
| unit = e2 ),
inference(resolve,[status(thm)],[c_3381,c_2759]) ).
cnf(c_3781,negated_conjecture,
( op(op(e2,e4),e2) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4)
| op(e2,e4) = unit ),
inference(resolve,[status(thm)],[c_3373,c_3780]) ).
cnf(c_3782,negated_conjecture,
( op(op(e2,e4),e2) = op(e2,e4)
| op(op(e4,e2),e2) = op(e2,e4) ),
inference(resolve,[status(thm)],[c_3382,c_3781]) ).
cnf(c_3442,negated_conjecture,
op(op(e4,e2),e2) = op(e2,e4),
inference(resolve,[status(thm)],[c_3431,c_3782]) ).
cnf(c_3783,plain,
( op(e2,e4) = e2
| op(op(e2,e4),op(e4,e2)) = e2
| op(e2,op(e4,e2)) = e2
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_3441,c_2748]) ).
cnf(c_3784,plain,
( op(e2,e4) = e2
| op(op(e2,e4),op(e4,e2)) = e2
| op(e2,op(e4,e2)) = e2
| op(e2,e4) = unit
| unit = e2 ),
inference(resolve,[status(thm)],[c_3381,c_3783]) ).
cnf(c_3785,negated_conjecture,
( op(e2,e4) = e2
| op(op(e2,e4),op(e4,e2)) = e2
| op(e2,op(e4,e2)) = e2
| op(e2,e4) = unit ),
inference(resolve,[status(thm)],[c_3373,c_3784]) ).
cnf(c_3786,negated_conjecture,
( op(e2,e4) = e2
| op(op(e2,e4),op(e4,e2)) = e2
| op(e2,op(e4,e2)) = e2 ),
inference(resolve,[status(thm)],[c_3382,c_3785]) ).
cnf(c_3787,negated_conjecture,
( op(e2,e4) = e2
| op(op(e2,e4),op(e4,e2)) = e2 ),
inference(resolve,[status(thm)],[c_3428,c_3786]) ).
cnf(c_3443,negated_conjecture,
op(op(e2,e4),op(e4,e2)) = e2,
inference(resolve,[status(thm)],[c_1387,c_3787]) ).
cnf(c_3788,plain,
( op(e4,op(e4,e2)) = e4
| e2 = e4
| op(e2,op(e4,e2)) = e4
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_3443,c_2747]) ).
cnf(c_3789,plain,
( op(e2,e4) = e4
| e2 = e4
| op(e2,op(e4,e2)) = e4
| op(e2,e4) = unit
| unit = e2
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_3441,c_3788]) ).
cnf(c_3790,plain,
( op(e2,e4) = e4
| e2 = e4
| op(e2,op(e4,e2)) = e4
| op(e2,e4) = unit
| unit = e2 ),
inference(resolve,[status(thm)],[c_3381,c_3789]) ).
cnf(c_3791,negated_conjecture,
( op(e2,e4) = e4
| e2 = e4
| op(e2,op(e4,e2)) = e4
| op(e2,e4) = unit ),
inference(resolve,[status(thm)],[c_3373,c_3790]) ).
cnf(c_3792,negated_conjecture,
( op(e2,e4) = e4
| e2 = e4
| op(e2,op(e4,e2)) = e4 ),
inference(resolve,[status(thm)],[c_3382,c_3791]) ).
cnf(c_3793,negated_conjecture,
( op(e2,e4) = e4
| op(e2,op(e4,e2)) = e4 ),
inference(resolve,[status(thm)],[c_300,c_3792]) ).
cnf(c_3444,negated_conjecture,
op(e2,op(e4,e2)) = e4,
inference(resolve,[status(thm)],[c_1386,c_3793]) ).
cnf(c_3794,plain,
( op(op(e2,e4),e4) = e4
| op(op(e2,e4),e2) = e4
| e2 = e4
| unit = e4
| op(e2,e4) = unit
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_3443,c_2872]) ).
cnf(c_3795,plain,
( op(e4,e2) = e4
| op(op(e2,e4),e2) = e4
| e2 = e4
| unit = e4
| op(e2,e4) = unit
| op(e4,e2) = unit ),
inference(paramod,[status(thm)],[c_3410,c_3794]) ).
cnf(c_3796,plain,
( op(e4,e2) = e4
| op(op(e2,e4),e2) = e4
| e2 = e4
| unit = e4
| op(e2,e4) = unit ),
inference(resolve,[status(thm)],[c_3381,c_3795]) ).
cnf(c_3797,plain,
( op(e4,e2) = e4
| op(op(e2,e4),e2) = e4
| e2 = e4
| unit = e4 ),
inference(resolve,[status(thm)],[c_3382,c_3796]) ).
cnf(c_3798,plain,
( op(e4,e2) = e4
| op(op(e2,e4),e2) = e4
| e2 = e4 ),
inference(resolve,[status(thm)],[c_3385,c_3797]) ).
cnf(c_3799,plain,
( op(e4,e2) = e4
| op(op(e2,e4),e2) = e4 ),
inference(resolve,[status(thm)],[c_300,c_3798]) ).
cnf(c_3445,plain,
op(op(e2,e4),e2) = e4,
inference(resolve,[status(thm)],[c_1352,c_3799]) ).
cnf(c_3800,negated_conjecture,
( op(op(e4,op(e2,e4)),e4) != op(e2,e4)
| op(op(e4,e2),e2) = e4
| op(op(e4,op(e4,e2)),op(e4,e2)) = e4
| op(op(op(e4,e2),op(e4,e2)),e4) != op(e4,op(op(e4,e2),op(e4,e2)))
| op(op(op(e2,e4),e4),e4) = op(e2,e4)
| op(e4,e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3445,c_1560]) ).
cnf(c_3801,negated_conjecture,
( op(op(e4,op(e2,e4)),e4) != op(e2,e4)
| op(op(e4,e2),e2) = e4
| op(op(e4,op(e4,e2)),op(e4,e2)) = e4
| op(op(op(e4,e2),op(e4,e2)),e4) != op(e4,op(op(e4,e2),op(e4,e2)))
| op(op(e4,e2),e4) = op(e2,e4)
| op(e4,e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3410,c_3800]) ).
cnf(c_3802,negated_conjecture,
( op(op(e4,op(e2,e4)),e4) != op(e2,e4)
| op(op(e4,e2),e2) = e4
| op(op(e4,op(e4,e2)),op(e4,e2)) = e4
| op(op(op(e4,e2),op(e4,e2)),e4) != op(e4,op(op(e4,e2),op(e4,e2)))
| e2 = op(e2,e4)
| op(e4,e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3440,c_3801]) ).
cnf(c_3803,negated_conjecture,
( op(op(e4,op(e2,e4)),e4) != op(e2,e4)
| op(op(e4,e2),e2) = e4
| op(op(e4,op(e4,e2)),op(e4,e2)) = e4
| op(unit,e4) != op(e4,op(op(e4,e2),op(e4,e2)))
| e2 = op(e2,e4)
| op(e4,e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3397,c_3802]) ).
cnf(c_3804,negated_conjecture,
( op(op(e4,op(e2,e4)),e4) != op(e2,e4)
| op(op(e4,e2),e2) = e4
| op(op(e4,op(e4,e2)),op(e4,e2)) = e4
| e4 != op(e4,op(op(e4,e2),op(e4,e2)))
| e2 = op(e2,e4)
| op(e4,e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_41,c_3803]) ).
cnf(c_3805,negated_conjecture,
( op(op(e4,op(e2,e4)),e4) != op(e2,e4)
| op(op(e4,e2),e2) = e4
| op(op(e4,op(e4,e2)),op(e4,e2)) = e4
| e4 != op(e4,unit)
| e2 = op(e2,e4)
| op(e4,e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3397,c_3804]) ).
cnf(c_3806,negated_conjecture,
( op(op(e4,op(e2,e4)),e4) != op(e2,e4)
| op(op(e4,e2),e2) = e4
| op(op(e4,op(e4,e2)),op(e4,e2)) = e4
| e4 != e4
| e2 = op(e2,e4)
| op(e4,e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_42,c_3805]) ).
cnf(c_3807,negated_conjecture,
( op(op(e4,op(e2,e4)),e4) != op(e2,e4)
| op(op(e4,e2),e2) = e4
| op(op(e2,e4),op(e4,e2)) = e4
| e4 != e4
| e2 = op(e2,e4)
| op(e4,e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3441,c_3806]) ).
cnf(c_3808,negated_conjecture,
( op(op(e4,op(e2,e4)),e4) != op(e2,e4)
| op(op(e4,e2),e2) = e4
| e2 = e4
| e4 != e4
| e2 = op(e2,e4)
| op(e4,e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3443,c_3807]) ).
cnf(c_3809,negated_conjecture,
( op(op(e4,op(e2,e4)),e4) != op(e2,e4)
| op(e2,e4) = e4
| e2 = e4
| e4 != e4
| e2 = op(e2,e4)
| op(e4,e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3442,c_3808]) ).
cnf(c_3810,negated_conjecture,
( op(e2,e4) != op(e2,e4)
| op(e2,e4) = e4
| e2 = e4
| e4 != e4
| e2 = op(e2,e4)
| op(e4,e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(paramod,[status(thm)],[c_3439,c_3809]) ).
cnf(c_3811,negated_conjecture,
( op(e2,e4) != op(e2,e4)
| op(e2,e4) = e4
| e2 = e4
| e4 != e4
| op(e2,e4) = e2
| op(e4,e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_3810]) ).
cnf(c_3812,negated_conjecture,
( op(e2,e4) != op(e2,e4)
| op(e2,e4) = e4
| e2 = e4
| op(e2,e4) = e2
| op(e4,e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_3811]) ).
cnf(c_3813,negated_conjecture,
( op(e2,e4) = e4
| e2 = e4
| op(e2,e4) = e2
| op(e4,e2) = op(e2,e4)
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(copy,[status(thm)],[c_3812]) ).
cnf(c_3814,negated_conjecture,
( op(e2,e4) = e4
| e2 = e4
| op(e2,e4) = e2
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_1353,c_3813]) ).
cnf(c_3815,negated_conjecture,
( op(e2,e4) = e4
| e2 = e4
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_1387,c_3814]) ).
cnf(c_3816,negated_conjecture,
( op(e2,e4) = e4
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_300,c_3815]) ).
cnf(c_3451,negated_conjecture,
( defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_1386,c_3816]) ).
cnf(c_3817,negated_conjecture,
( op(unit,e4) != op(e4,op(op(e4,e2),op(e4,e2)))
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_3397,c_1213]) ).
cnf(c_3818,negated_conjecture,
( e4 != op(e4,op(op(e4,e2),op(e4,e2)))
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_41,c_3817]) ).
cnf(c_3819,negated_conjecture,
( e4 != op(e4,unit)
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_3397,c_3818]) ).
cnf(c_3820,negated_conjecture,
( e4 != e4
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_42,c_3819]) ).
cnf(c_3452,negated_conjecture,
~ defn_30,
inference(copy,[status(thm)],[c_3820]) ).
cnf(c_3821,plain,
( op(e2,op(e2,e4)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2)
| op(unit,op(e2,e4)) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_3397,c_2674]) ).
cnf(c_3822,plain,
( op(e2,op(e2,e4)) = op(e4,e2)
| op(op(op(e4,e2),op(e4,e2)),e4) = op(e4,e2)
| op(e2,e4) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_1403,c_3821]) ).
cnf(c_3823,plain,
( op(e2,op(e2,e4)) = op(e4,e2)
| op(unit,e4) = op(e4,e2)
| op(e2,e4) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_3397,c_3822]) ).
cnf(c_3824,plain,
( op(e2,op(e2,e4)) = op(e4,e2)
| e4 = op(e4,e2)
| op(e2,e4) = op(e4,e2) ),
inference(paramod,[status(thm)],[c_41,c_3823]) ).
cnf(c_3825,plain,
( op(e2,op(e2,e4)) = op(e4,e2)
| e4 = op(e4,e2)
| op(e4,e2) = op(e2,e4) ),
inference(copy,[status(thm)],[c_3824]) ).
cnf(c_3826,plain,
( op(e2,op(e2,e4)) = op(e4,e2)
| op(e4,e2) = e4
| op(e4,e2) = op(e2,e4) ),
inference(copy,[status(thm)],[c_3825]) ).
cnf(c_3827,plain,
( op(e2,op(e2,e4)) = op(e4,e2)
| op(e4,e2) = e4 ),
inference(resolve,[status(thm)],[c_1353,c_3826]) ).
cnf(c_3455,plain,
op(e2,op(e2,e4)) = op(e4,e2),
inference(resolve,[status(thm)],[c_1352,c_3827]) ).
cnf(c_3828,plain,
( op(e2,op(e4,e2)) = op(e4,e2)
| op(e4,op(e2,e4)) = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(unit,op(e2,e4)) = e4 ),
inference(paramod,[status(thm)],[c_3397,c_2618]) ).
cnf(c_3829,plain,
( op(e2,op(e4,e2)) = op(e4,e2)
| op(e4,op(e2,e4)) = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(e2,e4) = e4 ),
inference(paramod,[status(thm)],[c_1403,c_3828]) ).
cnf(c_3830,plain,
( op(e2,op(e4,e2)) = op(e4,e2)
| e2 = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(e2,e4) = e4 ),
inference(paramod,[status(thm)],[c_3439,c_3829]) ).
cnf(c_3831,plain,
( e4 = op(e4,e2)
| e2 = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(e2,e4) = e4 ),
inference(paramod,[status(thm)],[c_3444,c_3830]) ).
cnf(c_3832,plain,
( op(e4,e2) = e4
| e2 = e4
| op(op(e4,e2),op(e2,e4)) = e4
| op(e2,e4) = e4 ),
inference(copy,[status(thm)],[c_3831]) ).
cnf(c_3833,plain,
( op(e4,e2) = e4
| e2 = e4
| op(op(e4,e2),op(e2,e4)) = e4 ),
inference(resolve,[status(thm)],[c_1386,c_3832]) ).
cnf(c_3834,plain,
( op(e4,e2) = e4
| op(op(e4,e2),op(e2,e4)) = e4 ),
inference(resolve,[status(thm)],[c_300,c_3833]) ).
cnf(c_3456,plain,
op(op(e4,e2),op(e2,e4)) = e4,
inference(resolve,[status(thm)],[c_1352,c_3834]) ).
cnf(c_3835,negated_conjecture,
( op(unit,op(e4,e2)) != op(e4,e2)
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_3397,c_1231]) ).
cnf(c_3836,negated_conjecture,
( op(e4,e2) != op(e4,e2)
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_1385,c_3835]) ).
cnf(c_3459,negated_conjecture,
~ defn_00,
inference(copy,[status(thm)],[c_3836]) ).
cnf(c_3837,negated_conjecture,
( op(unit,e2) != op(e2,op(op(e4,e2),op(e4,e2)))
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_3397,c_1225]) ).
cnf(c_3838,negated_conjecture,
( e2 != op(e2,op(op(e4,e2),op(e4,e2)))
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_37,c_3837]) ).
cnf(c_3839,negated_conjecture,
( e2 != op(e2,unit)
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_3397,c_3838]) ).
cnf(c_3840,negated_conjecture,
( e2 != e2
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_38,c_3839]) ).
cnf(c_3460,negated_conjecture,
~ defn_10,
inference(copy,[status(thm)],[c_3840]) ).
cnf(c_3841,negated_conjecture,
( op(unit,op(e2,e4)) != op(op(e2,e4),op(op(e4,e2),op(e4,e2)))
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_3397,c_1219]) ).
cnf(c_3842,negated_conjecture,
( op(e2,e4) != op(op(e2,e4),op(op(e4,e2),op(e4,e2)))
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_1403,c_3841]) ).
cnf(c_3843,negated_conjecture,
( op(e2,e4) != op(op(e2,e4),unit)
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_3397,c_3842]) ).
cnf(c_3844,negated_conjecture,
( op(e2,e4) != op(e2,e4)
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_1402,c_3843]) ).
cnf(c_3461,negated_conjecture,
~ defn_20,
inference(copy,[status(thm)],[c_3844]) ).
cnf(c_3845,negated_conjecture,
( op(unit,e2) != op(e2,op(op(e4,e2),op(e4,e2)))
| ~ defn_80 ),
inference(paramod,[status(thm)],[c_3397,c_1185]) ).
cnf(c_3846,negated_conjecture,
( e2 != op(e2,op(op(e4,e2),op(e4,e2)))
| ~ defn_80 ),
inference(paramod,[status(thm)],[c_37,c_3845]) ).
cnf(c_3847,negated_conjecture,
( e2 != op(e2,unit)
| ~ defn_80 ),
inference(paramod,[status(thm)],[c_3397,c_3846]) ).
cnf(c_3848,negated_conjecture,
( e2 != e2
| ~ defn_80 ),
inference(paramod,[status(thm)],[c_38,c_3847]) ).
cnf(c_3462,negated_conjecture,
~ defn_80,
inference(copy,[status(thm)],[c_3848]) ).
cnf(c_3849,negated_conjecture,
( op(unit,op(e2,e4)) != op(op(e2,e4),op(op(e4,e2),op(e4,e2)))
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_3397,c_1164]) ).
cnf(c_3850,negated_conjecture,
( op(e2,e4) != op(op(e2,e4),op(op(e4,e2),op(e4,e2)))
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_1403,c_3849]) ).
cnf(c_3851,negated_conjecture,
( op(e2,e4) != op(op(e2,e4),unit)
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_3397,c_3850]) ).
cnf(c_3852,negated_conjecture,
( op(e2,e4) != op(e2,e4)
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_1402,c_3851]) ).
cnf(c_3463,negated_conjecture,
~ defn_120,
inference(copy,[status(thm)],[c_3852]) ).
cnf(c_3853,negated_conjecture,
( op(e4,e2) = e2
| ~ defn_110 ),
inference(paramod,[status(thm)],[c_3410,c_1166]) ).
cnf(c_3465,negated_conjecture,
~ defn_110,
inference(resolve,[status(thm)],[c_1354,c_3853]) ).
cnf(c_3854,negated_conjecture,
( op(e2,e4) = op(e4,e2)
| ~ defn_70 ),
inference(paramod,[status(thm)],[c_3440,c_1189]) ).
cnf(c_3855,negated_conjecture,
( op(e4,e2) = op(e2,e4)
| ~ defn_70 ),
inference(copy,[status(thm)],[c_3854]) ).
cnf(c_3466,negated_conjecture,
~ defn_70,
inference(resolve,[status(thm)],[c_1353,c_3855]) ).
cnf(c_3856,negated_conjecture,
( op(op(e2,e4),e2) = op(e4,e2)
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_3442,c_1201]) ).
cnf(c_3857,negated_conjecture,
( e4 = op(e4,e2)
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_3445,c_3856]) ).
cnf(c_3858,negated_conjecture,
( op(e4,e2) = e4
| ~ defn_50 ),
inference(copy,[status(thm)],[c_3857]) ).
cnf(c_3467,negated_conjecture,
~ defn_50,
inference(resolve,[status(thm)],[c_1352,c_3858]) ).
cnf(c_3859,negated_conjecture,
( op(e2,op(e4,e2)) = op(e2,e4)
| ~ defn_130 ),
inference(paramod,[status(thm)],[c_3443,c_1156]) ).
cnf(c_3860,negated_conjecture,
( e4 = op(e2,e4)
| ~ defn_130 ),
inference(paramod,[status(thm)],[c_3444,c_3859]) ).
cnf(c_3861,negated_conjecture,
( op(e2,e4) = e4
| ~ defn_130 ),
inference(copy,[status(thm)],[c_3860]) ).
cnf(c_3468,negated_conjecture,
~ defn_130,
inference(resolve,[status(thm)],[c_1386,c_3861]) ).
cnf(c_3862,negated_conjecture,
( op(e4,op(e4,e2)) = e2
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_3444,c_1177]) ).
cnf(c_3863,negated_conjecture,
( op(e2,e4) = e2
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_3441,c_3862]) ).
cnf(c_3469,negated_conjecture,
~ defn_90,
inference(resolve,[status(thm)],[c_1387,c_3863]) ).
cnf(c_3864,negated_conjecture,
( defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20
| defn_10 ),
inference(resolve,[status(thm)],[c_3459,c_3451]) ).
cnf(c_3865,negated_conjecture,
( defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30
| defn_20 ),
inference(resolve,[status(thm)],[c_3460,c_3864]) ).
cnf(c_3866,negated_conjecture,
( defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_30 ),
inference(resolve,[status(thm)],[c_3461,c_3865]) ).
cnf(c_3867,negated_conjecture,
( defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50 ),
inference(resolve,[status(thm)],[c_3452,c_3866]) ).
cnf(c_3868,negated_conjecture,
( defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60 ),
inference(resolve,[status(thm)],[c_3467,c_3867]) ).
cnf(c_3869,negated_conjecture,
( defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_60 ),
inference(resolve,[status(thm)],[c_3466,c_3868]) ).
cnf(c_3870,negated_conjecture,
( defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_60 ),
inference(resolve,[status(thm)],[c_3462,c_3869]) ).
cnf(c_3871,negated_conjecture,
( defn_130
| defn_120
| defn_110
| defn_100
| defn_60 ),
inference(resolve,[status(thm)],[c_3469,c_3870]) ).
cnf(c_3872,negated_conjecture,
( defn_130
| defn_120
| defn_100
| defn_60 ),
inference(resolve,[status(thm)],[c_3465,c_3871]) ).
cnf(c_3873,negated_conjecture,
( defn_130
| defn_100
| defn_60 ),
inference(resolve,[status(thm)],[c_3463,c_3872]) ).
cnf(c_3470,negated_conjecture,
( defn_100
| defn_60 ),
inference(resolve,[status(thm)],[c_3468,c_3873]) ).
cnf(c_3874,negated_conjecture,
( op(op(e4,e2),op(e2,e4)) = e2
| ~ defn_100 ),
inference(paramod,[status(thm)],[c_3455,c_1171]) ).
cnf(c_3875,negated_conjecture,
( e4 = e2
| ~ defn_100 ),
inference(paramod,[status(thm)],[c_3456,c_3874]) ).
cnf(c_3876,negated_conjecture,
( e2 = e4
| ~ defn_100 ),
inference(copy,[status(thm)],[c_3875]) ).
cnf(c_3471,negated_conjecture,
~ defn_100,
inference(resolve,[status(thm)],[c_300,c_3876]) ).
cnf(c_3877,negated_conjecture,
( op(e4,op(e2,e4)) = op(e4,e2)
| ~ defn_60 ),
inference(paramod,[status(thm)],[c_3456,c_1195]) ).
cnf(c_3878,negated_conjecture,
( e2 = op(e4,e2)
| ~ defn_60 ),
inference(paramod,[status(thm)],[c_3439,c_3877]) ).
cnf(c_3879,negated_conjecture,
( op(e4,e2) = e2
| ~ defn_60 ),
inference(copy,[status(thm)],[c_3878]) ).
cnf(c_3472,negated_conjecture,
~ defn_60,
inference(resolve,[status(thm)],[c_1354,c_3879]) ).
cnf(c_3880,negated_conjecture,
defn_100,
inference(resolve,[status(thm)],[c_3472,c_3470]) ).
cnf(c_3473,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_3471,c_3880]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG068+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 21:05:17 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.36 % Process 3102928 was started by sandbox on n005,
% 0.12/0.36 % Sat Sep 26 21:05:17 2026
% 0.12/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 4.78/5.10
% 4.78/5.10 % From the command line: assign(max_seconds, 300).
% 178.00/28.07
% 178.00/28.07 % given #500 (I,wt=70): 1718 op(e2,op(op(e4,e2),op(e4,e2))) = e4 | op(e2,op(e4,e2)) = e4 | op(e2,op(e2,e4)) = e4. [back_unit_del(1703),unit_del(c,1707)].
% 178.00/28.07
% 178.00/28.07 % SZS status Theorem for theBenchmark
% 178.00/28.07
% 178.00/28.07 % Proof 1 at 3.42 (+ 0.47) seconds.
% 178.00/28.07 % Length of proof is 266.
% 178.00/28.07 % Level of proof is 20.
% 178.00/28.07 % Maximum clause weight is 184.000.
% 178.00/28.07 % Given clauses 575.
% 178.00/28.07
% 178.00/28.07 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------