%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG092+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 : n019.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:28 AM UTC 2026
% Result : Theorem 2.72s 17.05s
% Output : CNFRefutation 2.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 130
% Number of leaves : 81
% Syntax : Number of formulae : 559 ( 131 unt; 77 def)
% Number of atoms : 9601 (2296 equ)
% Maximal formula atoms : 440 ( 17 avg)
% Number of connectives : 10547 (1505 ~;8395 |; 570 &)
% ( 77 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 96 ( 17 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 79 ( 77 usr; 78 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,
( e3 != e4
& e2 != e4
& e2 != e3
& e1 != e4
& e1 != e3
& e1 != e2
& e0 != e4
& e0 != e3
& e0 != e2
& e0 != e1 ),
file('theBenchmark.p',ax1) ).
fof(ax2,axiom,
( op(e4,e4) = e0
& op(e4,e3) = e2
& op(e4,e2) = e1
& op(e4,e1) = e3
& op(e4,e0) = e4
& op(e3,e4) = e1
& op(e3,e3) = e4
& op(e3,e2) = e0
& op(e3,e1) = e2
& op(e3,e0) = e3
& op(e2,e4) = e3
& op(e2,e3) = e1
& op(e2,e2) = e4
& op(e2,e1) = e0
& op(e2,e0) = e2
& op(e1,e4) = e2
& op(e1,e3) = e0
& op(e1,e2) = e3
& op(e1,e1) = e4
& op(e1,e0) = e1
& op(e0,e4) = e4
& op(e0,e3) = e3
& op(e0,e2) = e2
& op(e0,e1) = e1
& op(e0,e0) = e0 ),
file('theBenchmark.p',ax2) ).
fof(co1,conjecture,
( ( 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 )
& ( 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
& ( 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 )
& ( ( op(e4,op(e4,e4)) = e4
& op(e4,op(e4,e4)) != e4 )
| ( op(e4,op(e3,e4)) = e3
& op(e3,op(e3,e4)) != e4 )
| ( op(e4,op(e2,e4)) = e2
& op(e2,op(e2,e4)) != e4 )
| ( op(e4,op(e1,e4)) = e1
& op(e1,op(e1,e4)) != e4 )
| ( op(e4,op(e0,e4)) = e0
& op(e0,op(e0,e4)) != e4 ) )
& ( ( op(e3,op(e4,e3)) = e4
& op(e4,op(e4,e3)) != e3 )
| ( op(e3,op(e3,e3)) = e3
& op(e3,op(e3,e3)) != e3 )
| ( op(e3,op(e2,e3)) = e2
& op(e2,op(e2,e3)) != e3 )
| ( op(e3,op(e1,e3)) = e1
& op(e1,op(e1,e3)) != e3 )
| ( op(e3,op(e0,e3)) = e0
& op(e0,op(e0,e3)) != e3 ) )
& ( ( op(e2,op(e4,e2)) = e4
& op(e4,op(e4,e2)) != e2 )
| ( op(e2,op(e3,e2)) = e3
& op(e3,op(e3,e2)) != e2 )
| ( op(e2,op(e2,e2)) = e2
& op(e2,op(e2,e2)) != e2 )
| ( op(e2,op(e1,e2)) = e1
& op(e1,op(e1,e2)) != e2 )
| ( op(e2,op(e0,e2)) = e0
& op(e0,op(e0,e2)) != e2 ) )
& ( ( op(e1,op(e4,e1)) = e4
& op(e4,op(e4,e1)) != e1 )
| ( op(e1,op(e3,e1)) = e3
& op(e3,op(e3,e1)) != e1 )
| ( op(e1,op(e2,e1)) = e2
& op(e2,op(e2,e1)) != e1 )
| ( op(e1,op(e1,e1)) = e1
& op(e1,op(e1,e1)) != e1 )
| ( op(e1,op(e0,e1)) = e0
& op(e0,op(e0,e1)) != e1 ) )
& ( ( op(e0,op(e4,e0)) = e4
& op(e4,op(e4,e0)) != e0 )
| ( op(e0,op(e3,e0)) = e3
& op(e3,op(e3,e0)) != e0 )
| ( op(e0,op(e2,e0)) = e2
& op(e2,op(e2,e0)) != e0 )
| ( op(e0,op(e1,e0)) = e1
& op(e1,op(e1,e0)) != e0 )
| ( op(e0,op(e0,e0)) = e0
& op(e0,op(e0,e0)) != e0 ) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ( ( op(e4,e4) = e4
| op(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 )
& ( 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
& ( 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 )
& ( ( op(e4,op(e4,e4)) = e4
& op(e4,op(e4,e4)) != e4 )
| ( op(e4,op(e3,e4)) = e3
& op(e3,op(e3,e4)) != e4 )
| ( op(e4,op(e2,e4)) = e2
& op(e2,op(e2,e4)) != e4 )
| ( op(e4,op(e1,e4)) = e1
& op(e1,op(e1,e4)) != e4 )
| ( op(e4,op(e0,e4)) = e0
& op(e0,op(e0,e4)) != e4 ) )
& ( ( op(e3,op(e4,e3)) = e4
& op(e4,op(e4,e3)) != e3 )
| ( op(e3,op(e3,e3)) = e3
& op(e3,op(e3,e3)) != e3 )
| ( op(e3,op(e2,e3)) = e2
& op(e2,op(e2,e3)) != e3 )
| ( op(e3,op(e1,e3)) = e1
& op(e1,op(e1,e3)) != e3 )
| ( op(e3,op(e0,e3)) = e0
& op(e0,op(e0,e3)) != e3 ) )
& ( ( op(e2,op(e4,e2)) = e4
& op(e4,op(e4,e2)) != e2 )
| ( op(e2,op(e3,e2)) = e3
& op(e3,op(e3,e2)) != e2 )
| ( op(e2,op(e2,e2)) = e2
& op(e2,op(e2,e2)) != e2 )
| ( op(e2,op(e1,e2)) = e1
& op(e1,op(e1,e2)) != e2 )
| ( op(e2,op(e0,e2)) = e0
& op(e0,op(e0,e2)) != e2 ) )
& ( ( op(e1,op(e4,e1)) = e4
& op(e4,op(e4,e1)) != e1 )
| ( op(e1,op(e3,e1)) = e3
& op(e3,op(e3,e1)) != e1 )
| ( op(e1,op(e2,e1)) = e2
& op(e2,op(e2,e1)) != e1 )
| ( op(e1,op(e1,e1)) = e1
& op(e1,op(e1,e1)) != e1 )
| ( op(e1,op(e0,e1)) = e0
& op(e0,op(e0,e1)) != e1 ) )
& ( ( op(e0,op(e4,e0)) = e4
& op(e4,op(e4,e0)) != e0 )
| ( op(e0,op(e3,e0)) = e3
& op(e3,op(e3,e0)) != e0 )
| ( op(e0,op(e2,e0)) = e2
& op(e2,op(e2,e0)) != e0 )
| ( op(e0,op(e1,e0)) = e1
& op(e1,op(e1,e0)) != e0 )
| ( op(e0,op(e0,e0)) = e0
& op(e0,op(e0,e0)) != e0 ) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_4,plain,
e1 != e0,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_5,plain,
e0 != e1,
inference(copy,[status(thm)],[c_4]) ).
cnf(c_6,plain,
e2 != e0,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_7,plain,
e0 != e2,
inference(copy,[status(thm)],[c_6]) ).
cnf(c_8,plain,
e3 != e0,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_9,plain,
e0 != e3,
inference(copy,[status(thm)],[c_8]) ).
cnf(c_10,plain,
e4 != e0,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_11,plain,
e0 != e4,
inference(copy,[status(thm)],[c_10]) ).
cnf(c_17,plain,
e4 != e3,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_18,plain,
op(e0,e0) = e0,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_19,plain,
op(e0,e1) = e1,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_20,plain,
op(e0,e2) = e2,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_21,plain,
op(e0,e3) = e3,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_22,plain,
op(e0,e4) = e4,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_23,plain,
op(e1,e0) = e1,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_24,plain,
op(e1,e1) = e4,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_25,plain,
op(e1,e2) = e3,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_26,plain,
op(e1,e3) = e0,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_27,plain,
op(e1,e4) = e2,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_28,plain,
op(e2,e0) = e2,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_29,plain,
op(e2,e1) = e0,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_30,plain,
op(e2,e2) = e4,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_31,plain,
op(e2,e3) = e1,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_32,plain,
op(e2,e4) = e3,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_33,plain,
op(e3,e0) = e3,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_34,plain,
op(e3,e1) = e2,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_35,plain,
op(e3,e2) = e0,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_36,plain,
op(e3,e3) = e4,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_37,plain,
op(e3,e4) = e1,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_38,plain,
op(e4,e0) = e4,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_39,plain,
op(e4,e1) = e3,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_40,plain,
op(e4,e2) = e1,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_41,plain,
op(e4,e3) = e2,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_42,plain,
op(e4,e4) = e0,
inference(clausify,[status(thm)],[ax2]) ).
fof(ax3,axiom,
unit = e0,
file('theBenchmark.p',ax3) ).
cnf(c_43,plain,
unit = e0,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_44,plain,
e0 = unit,
inference(copy,[status(thm)],[c_43]) ).
fof(def_defn_00,definition,
( defn_00
<=> ( ( op(e0,op(e4,e0)) != e4
| op(e4,op(e4,e0)) = e0 )
& ( op(e0,op(e3,e0)) != e3
| op(e3,op(e3,e0)) = e0 )
& ( op(e0,op(e2,e0)) != e2
| op(e2,op(e2,e0)) = e0 )
& ( op(e0,op(e1,e0)) != e1
| op(e1,op(e1,e0)) = e0 ) ) ),
introduced(definition,[new_symbols(definition,[defn_00])],[]) ).
fof(def_defn_10,definition,
( defn_10
<=> ( op(e0,e0) != e4
& op(e0,e0) != e3
& op(e0,e0) != e2
& op(e0,e0) != e1
& op(e0,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_10])],[]) ).
fof(def_defn_20,definition,
( defn_20
<=> ( op(e0,e1) != e4
& op(e0,e1) != e3
& op(e0,e1) != e2
& op(e0,e1) != e1
& op(e0,e1) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_20])],[]) ).
fof(def_defn_30,definition,
( defn_30
<=> ( op(e0,e2) != e4
& op(e0,e2) != e3
& op(e0,e2) != e2
& op(e0,e2) != e1
& op(e0,e2) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_30])],[]) ).
fof(def_defn_40,definition,
( defn_40
<=> ( op(e0,e3) != e4
& op(e0,e3) != e3
& op(e0,e3) != e2
& op(e0,e3) != e1
& op(e0,e3) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_40])],[]) ).
fof(def_defn_50,definition,
( defn_50
<=> ( op(e0,e4) != e4
& op(e0,e4) != e3
& op(e0,e4) != e2
& op(e0,e4) != e1
& op(e0,e4) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_50])],[]) ).
fof(def_defn_60,definition,
( defn_60
<=> ( op(e1,e0) != e4
& op(e1,e0) != e3
& op(e1,e0) != e2
& op(e1,e0) != e1
& op(e1,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_60])],[]) ).
fof(def_defn_70,definition,
( defn_70
<=> ( op(e1,e1) != e4
& op(e1,e1) != e3
& op(e1,e1) != e2
& op(e1,e1) != e1
& op(e1,e1) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_70])],[]) ).
fof(def_defn_80,definition,
( defn_80
<=> ( op(e1,e2) != e4
& op(e1,e2) != e3
& op(e1,e2) != e2
& op(e1,e2) != e1
& op(e1,e2) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_80])],[]) ).
fof(def_defn_90,definition,
( defn_90
<=> ( op(e1,e3) != e4
& op(e1,e3) != e3
& op(e1,e3) != e2
& op(e1,e3) != e1
& op(e1,e3) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_90])],[]) ).
fof(def_defn_100,definition,
( defn_100
<=> ( op(e1,e4) != e4
& op(e1,e4) != e3
& op(e1,e4) != e2
& op(e1,e4) != e1
& op(e1,e4) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_100])],[]) ).
fof(def_defn_110,definition,
( defn_110
<=> ( op(e2,e0) != e4
& op(e2,e0) != e3
& op(e2,e0) != e2
& op(e2,e0) != e1
& op(e2,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_110])],[]) ).
fof(def_defn_120,definition,
( defn_120
<=> ( op(e2,e1) != e4
& op(e2,e1) != e3
& op(e2,e1) != e2
& op(e2,e1) != e1
& op(e2,e1) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_120])],[]) ).
fof(def_defn_130,definition,
( defn_130
<=> ( op(e2,e2) != e4
& op(e2,e2) != e3
& op(e2,e2) != e2
& op(e2,e2) != e1
& op(e2,e2) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_130])],[]) ).
fof(def_defn_140,definition,
( defn_140
<=> ( op(e2,e3) != e4
& op(e2,e3) != e3
& op(e2,e3) != e2
& op(e2,e3) != e1
& op(e2,e3) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_140])],[]) ).
fof(def_defn_150,definition,
( defn_150
<=> ( op(e2,e4) != e4
& op(e2,e4) != e3
& op(e2,e4) != e2
& op(e2,e4) != e1
& op(e2,e4) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_150])],[]) ).
fof(def_defn_160,definition,
( defn_160
<=> ( op(e3,e0) != e4
& op(e3,e0) != e3
& op(e3,e0) != e2
& op(e3,e0) != e1
& op(e3,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_160])],[]) ).
fof(def_defn_170,definition,
( defn_170
<=> ( op(e3,e1) != e4
& op(e3,e1) != e3
& op(e3,e1) != e2
& op(e3,e1) != e1
& op(e3,e1) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_170])],[]) ).
fof(def_defn_180,definition,
( defn_180
<=> ( op(e3,e2) != e4
& op(e3,e2) != e3
& op(e3,e2) != e2
& op(e3,e2) != e1
& op(e3,e2) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_180])],[]) ).
fof(def_defn_190,definition,
( defn_190
<=> ( op(e3,e3) != e4
& op(e3,e3) != e3
& op(e3,e3) != e2
& op(e3,e3) != e1
& op(e3,e3) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_190])],[]) ).
fof(def_defn_200,definition,
( defn_200
<=> ( op(e3,e4) != e4
& op(e3,e4) != e3
& op(e3,e4) != e2
& op(e3,e4) != e1
& op(e3,e4) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_200])],[]) ).
fof(def_defn_210,definition,
( defn_210
<=> ( op(e4,e0) != e4
& op(e4,e0) != e3
& op(e4,e0) != e2
& op(e4,e0) != e1
& op(e4,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_210])],[]) ).
fof(def_defn_220,definition,
( defn_220
<=> ( op(e4,e1) != e4
& op(e4,e1) != e3
& op(e4,e1) != e2
& op(e4,e1) != e1
& op(e4,e1) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_220])],[]) ).
fof(def_defn_230,definition,
( defn_230
<=> ( op(e4,e2) != e4
& op(e4,e2) != e3
& op(e4,e2) != e2
& op(e4,e2) != e1
& op(e4,e2) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_230])],[]) ).
fof(def_defn_240,definition,
( defn_240
<=> ( op(e4,e3) != e4
& op(e4,e3) != e3
& op(e4,e3) != e2
& op(e4,e3) != e1
& op(e4,e3) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_240])],[]) ).
fof(def_defn_250,definition,
( defn_250
<=> ( op(e4,e4) != e4
& op(e4,e4) != e3
& op(e4,e4) != e2
& op(e4,e4) != e1
& op(e4,e4) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_250])],[]) ).
fof(def_defn_260,definition,
( defn_260
<=> ( unit != e4
& unit != e3
& unit != e2
& unit != e1
& unit != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_260])],[]) ).
fof(def_defn_270,definition,
( defn_270
<=> ( op(e0,e4) != e0
& op(e0,e3) != e0
& op(e0,e2) != e0
& op(e0,e1) != e0
& op(e0,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_270])],[]) ).
fof(def_defn_280,definition,
( defn_280
<=> ( op(e4,e0) != e0
& op(e3,e0) != e0
& op(e2,e0) != e0
& op(e1,e0) != e0
& op(e0,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_280])],[]) ).
fof(def_defn_290,definition,
( defn_290
<=> ( op(e0,e4) != e1
& op(e0,e3) != e1
& op(e0,e2) != e1
& op(e0,e1) != e1
& op(e0,e0) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_290])],[]) ).
fof(def_defn_300,definition,
( defn_300
<=> ( op(e4,e0) != e1
& op(e3,e0) != e1
& op(e2,e0) != e1
& op(e1,e0) != e1
& op(e0,e0) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_300])],[]) ).
fof(def_defn_310,definition,
( defn_310
<=> ( op(e0,e4) != e2
& op(e0,e3) != e2
& op(e0,e2) != e2
& op(e0,e1) != e2
& op(e0,e0) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_310])],[]) ).
fof(def_defn_320,definition,
( defn_320
<=> ( op(e4,e0) != e2
& op(e3,e0) != e2
& op(e2,e0) != e2
& op(e1,e0) != e2
& op(e0,e0) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_320])],[]) ).
fof(def_defn_330,definition,
( defn_330
<=> ( op(e0,e4) != e3
& op(e0,e3) != e3
& op(e0,e2) != e3
& op(e0,e1) != e3
& op(e0,e0) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_330])],[]) ).
fof(def_defn_340,definition,
( defn_340
<=> ( op(e4,e0) != e3
& op(e3,e0) != e3
& op(e2,e0) != e3
& op(e1,e0) != e3
& op(e0,e0) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_340])],[]) ).
fof(def_defn_350,definition,
( defn_350
<=> ( op(e0,e4) != e4
& op(e0,e3) != e4
& op(e0,e2) != e4
& op(e0,e1) != e4
& op(e0,e0) != e4 ) ),
introduced(definition,[new_symbols(definition,[defn_350])],[]) ).
fof(def_defn_360,definition,
( defn_360
<=> ( op(e4,e0) != e4
& op(e3,e0) != e4
& op(e2,e0) != e4
& op(e1,e0) != e4
& op(e0,e0) != e4 ) ),
introduced(definition,[new_symbols(definition,[defn_360])],[]) ).
fof(def_defn_370,definition,
( defn_370
<=> ( op(e1,e4) != e0
& op(e1,e3) != e0
& op(e1,e2) != e0
& op(e1,e1) != e0
& op(e1,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_370])],[]) ).
fof(def_defn_380,definition,
( defn_380
<=> ( op(e4,e1) != e0
& op(e3,e1) != e0
& op(e2,e1) != e0
& op(e1,e1) != e0
& op(e0,e1) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_380])],[]) ).
fof(def_defn_390,definition,
( defn_390
<=> ( op(e1,e4) != e1
& op(e1,e3) != e1
& op(e1,e2) != e1
& op(e1,e1) != e1
& op(e1,e0) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_390])],[]) ).
fof(def_defn_400,definition,
( defn_400
<=> ( op(e4,e1) != e1
& op(e3,e1) != e1
& op(e2,e1) != e1
& op(e1,e1) != e1
& op(e0,e1) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_400])],[]) ).
fof(def_defn_410,definition,
( defn_410
<=> ( op(e1,e4) != e2
& op(e1,e3) != e2
& op(e1,e2) != e2
& op(e1,e1) != e2
& op(e1,e0) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_410])],[]) ).
fof(def_defn_420,definition,
( defn_420
<=> ( op(e4,e1) != e2
& op(e3,e1) != e2
& op(e2,e1) != e2
& op(e1,e1) != e2
& op(e0,e1) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_420])],[]) ).
fof(def_defn_430,definition,
( defn_430
<=> ( op(e1,e4) != e3
& op(e1,e3) != e3
& op(e1,e2) != e3
& op(e1,e1) != e3
& op(e1,e0) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_430])],[]) ).
fof(def_defn_440,definition,
( defn_440
<=> ( op(e4,e1) != e3
& op(e3,e1) != e3
& op(e2,e1) != e3
& op(e1,e1) != e3
& op(e0,e1) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_440])],[]) ).
fof(def_defn_450,definition,
( defn_450
<=> ( op(e1,e4) != e4
& op(e1,e3) != e4
& op(e1,e2) != e4
& op(e1,e1) != e4
& op(e1,e0) != e4 ) ),
introduced(definition,[new_symbols(definition,[defn_450])],[]) ).
fof(def_defn_460,definition,
( defn_460
<=> ( op(e4,e1) != e4
& op(e3,e1) != e4
& op(e2,e1) != e4
& op(e1,e1) != e4
& op(e0,e1) != e4 ) ),
introduced(definition,[new_symbols(definition,[defn_460])],[]) ).
fof(def_defn_470,definition,
( defn_470
<=> ( op(e2,e4) != e0
& op(e2,e3) != e0
& op(e2,e2) != e0
& op(e2,e1) != e0
& op(e2,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_470])],[]) ).
fof(def_defn_480,definition,
( defn_480
<=> ( op(e4,e2) != e0
& op(e3,e2) != e0
& op(e2,e2) != e0
& op(e1,e2) != e0
& op(e0,e2) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_480])],[]) ).
fof(def_defn_490,definition,
( defn_490
<=> ( op(e2,e4) != e1
& op(e2,e3) != e1
& op(e2,e2) != e1
& op(e2,e1) != e1
& op(e2,e0) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_490])],[]) ).
fof(def_defn_500,definition,
( defn_500
<=> ( op(e4,e2) != e1
& op(e3,e2) != e1
& op(e2,e2) != e1
& op(e1,e2) != e1
& op(e0,e2) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_500])],[]) ).
fof(def_defn_510,definition,
( defn_510
<=> ( op(e2,e4) != e2
& op(e2,e3) != e2
& op(e2,e2) != e2
& op(e2,e1) != e2
& op(e2,e0) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_510])],[]) ).
fof(def_defn_520,definition,
( defn_520
<=> ( op(e4,e2) != e2
& op(e3,e2) != e2
& op(e2,e2) != e2
& op(e1,e2) != e2
& op(e0,e2) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_520])],[]) ).
fof(def_defn_530,definition,
( defn_530
<=> ( op(e2,e4) != e3
& op(e2,e3) != e3
& op(e2,e2) != e3
& op(e2,e1) != e3
& op(e2,e0) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_530])],[]) ).
fof(def_defn_540,definition,
( defn_540
<=> ( op(e4,e2) != e3
& op(e3,e2) != e3
& op(e2,e2) != e3
& op(e1,e2) != e3
& op(e0,e2) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_540])],[]) ).
fof(def_defn_550,definition,
( defn_550
<=> ( op(e2,e4) != e4
& op(e2,e3) != e4
& op(e2,e2) != e4
& op(e2,e1) != e4
& op(e2,e0) != e4 ) ),
introduced(definition,[new_symbols(definition,[defn_550])],[]) ).
fof(def_defn_560,definition,
( defn_560
<=> ( op(e4,e2) != e4
& op(e3,e2) != e4
& op(e2,e2) != e4
& op(e1,e2) != e4
& op(e0,e2) != e4 ) ),
introduced(definition,[new_symbols(definition,[defn_560])],[]) ).
fof(def_defn_570,definition,
( defn_570
<=> ( op(e3,e4) != e0
& op(e3,e3) != e0
& op(e3,e2) != e0
& op(e3,e1) != e0
& op(e3,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_570])],[]) ).
fof(def_defn_580,definition,
( defn_580
<=> ( op(e4,e3) != e0
& op(e3,e3) != e0
& op(e2,e3) != e0
& op(e1,e3) != e0
& op(e0,e3) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_580])],[]) ).
fof(def_defn_590,definition,
( defn_590
<=> ( op(e3,e4) != e1
& op(e3,e3) != e1
& op(e3,e2) != e1
& op(e3,e1) != e1
& op(e3,e0) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_590])],[]) ).
fof(def_defn_600,definition,
( defn_600
<=> ( op(e4,e3) != e1
& op(e3,e3) != e1
& op(e2,e3) != e1
& op(e1,e3) != e1
& op(e0,e3) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_600])],[]) ).
fof(def_defn_610,definition,
( defn_610
<=> ( op(e3,e4) != e2
& op(e3,e3) != e2
& op(e3,e2) != e2
& op(e3,e1) != e2
& op(e3,e0) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_610])],[]) ).
fof(def_defn_620,definition,
( defn_620
<=> ( op(e4,e3) != e2
& op(e3,e3) != e2
& op(e2,e3) != e2
& op(e1,e3) != e2
& op(e0,e3) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_620])],[]) ).
fof(def_defn_630,definition,
( defn_630
<=> ( op(e3,e4) != e3
& op(e3,e3) != e3
& op(e3,e2) != e3
& op(e3,e1) != e3
& op(e3,e0) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_630])],[]) ).
fof(def_defn_640,definition,
( defn_640
<=> ( op(e4,e3) != e3
& op(e3,e3) != e3
& op(e2,e3) != e3
& op(e1,e3) != e3
& op(e0,e3) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_640])],[]) ).
fof(def_defn_650,definition,
( defn_650
<=> ( op(e3,e4) != e4
& op(e3,e3) != e4
& op(e3,e2) != e4
& op(e3,e1) != e4
& op(e3,e0) != e4 ) ),
introduced(definition,[new_symbols(definition,[defn_650])],[]) ).
fof(def_defn_660,definition,
( defn_660
<=> ( op(e4,e3) != e4
& op(e3,e3) != e4
& op(e2,e3) != e4
& op(e1,e3) != e4
& op(e0,e3) != e4 ) ),
introduced(definition,[new_symbols(definition,[defn_660])],[]) ).
fof(def_defn_670,definition,
( defn_670
<=> ( op(e4,e4) != e0
& op(e4,e3) != e0
& op(e4,e2) != e0
& op(e4,e1) != e0
& op(e4,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_670])],[]) ).
fof(def_defn_680,definition,
( defn_680
<=> ( op(e4,e4) != e0
& op(e3,e4) != e0
& op(e2,e4) != e0
& op(e1,e4) != e0
& op(e0,e4) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_680])],[]) ).
fof(def_defn_690,definition,
( defn_690
<=> ( op(e4,e4) != e1
& op(e4,e3) != e1
& op(e4,e2) != e1
& op(e4,e1) != e1
& op(e4,e0) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_690])],[]) ).
fof(def_defn_700,definition,
( defn_700
<=> ( op(e4,e4) != e1
& op(e3,e4) != e1
& op(e2,e4) != e1
& op(e1,e4) != e1
& op(e0,e4) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_700])],[]) ).
fof(def_defn_710,definition,
( defn_710
<=> ( op(e4,e4) != e2
& op(e4,e3) != e2
& op(e4,e2) != e2
& op(e4,e1) != e2
& op(e4,e0) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_710])],[]) ).
fof(def_defn_720,definition,
( defn_720
<=> ( op(e4,e4) != e2
& op(e3,e4) != e2
& op(e2,e4) != e2
& op(e1,e4) != e2
& op(e0,e4) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_720])],[]) ).
fof(def_defn_730,definition,
( defn_730
<=> ( op(e4,e4) != e3
& op(e4,e3) != e3
& op(e4,e2) != e3
& op(e4,e1) != e3
& op(e4,e0) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_730])],[]) ).
fof(def_defn_740,definition,
( defn_740
<=> ( op(e4,e4) != e3
& op(e3,e4) != e3
& op(e2,e4) != e3
& op(e1,e4) != e3
& op(e0,e4) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_740])],[]) ).
fof(def_defn_750,definition,
( defn_750
<=> ( op(e4,e4) != e4
& op(e4,e3) != e4
& op(e4,e2) != e4
& op(e4,e1) != e4
& op(e4,e0) != e4 ) ),
introduced(definition,[new_symbols(definition,[defn_750])],[]) ).
fof(def_defn_760,definition,
( defn_760
<=> ( op(e4,e4) != e4
& op(e3,e4) != e4
& op(e2,e4) != e4
& op(e1,e4) != e4
& op(e0,e4) != e4 ) ),
introduced(definition,[new_symbols(definition,[defn_760])],[]) ).
cnf(c_275,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| op(e3,op(e2,e3)) != e2
| op(e2,op(e2,e3)) = e3
| op(e2,op(e1,e2)) != e1
| op(e1,op(e1,e2)) = e2
| op(e1,op(e3,e1)) != e3
| op(e3,op(e3,e1)) = e1
| 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,def_defn_140,def_defn_150,def_defn_160,def_defn_170,def_defn_180,def_defn_190,def_defn_200,def_defn_210,def_defn_220,def_defn_230,def_defn_240,def_defn_250,def_defn_260,def_defn_270,def_defn_280,def_defn_290,def_defn_300,def_defn_310,def_defn_320,def_defn_330,def_defn_340,def_defn_350,def_defn_360,def_defn_370,def_defn_380,def_defn_390,def_defn_400,def_defn_410,def_defn_420,def_defn_430,def_defn_440,def_defn_450,def_defn_460,def_defn_470,def_defn_480,def_defn_490,def_defn_500,def_defn_510,def_defn_520,def_defn_530,def_defn_540,def_defn_550,def_defn_560,def_defn_570,def_defn_580,def_defn_590,def_defn_600,def_defn_610,def_defn_620,def_defn_630,def_defn_640,def_defn_650,def_defn_660,def_defn_670,def_defn_680,def_defn_690,def_defn_700,def_defn_710,def_defn_720,def_defn_730,def_defn_740,def_defn_750,def_defn_760]) ).
cnf(c_1064,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| op(e3,op(e2,e3)) != e2
| op(e2,op(e2,e3)) = e3
| op(e2,op(e1,e2)) != e1
| op(e1,op(e1,e2)) = e2
| op(e1,op(e3,e1)) != e3
| op(e3,e2) = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_34,c_275]) ).
cnf(c_1065,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| op(e3,op(e2,e3)) != e2
| op(e2,op(e2,e3)) = e3
| op(e2,op(e1,e2)) != e1
| op(e1,op(e1,e2)) = e2
| op(e1,op(e3,e1)) != e3
| e0 = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_35,c_1064]) ).
cnf(c_1066,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| op(e3,op(e2,e3)) != e2
| op(e2,op(e2,e3)) = e3
| op(e2,op(e1,e2)) != e1
| op(e1,op(e1,e2)) = e2
| op(e1,op(e3,e1)) != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_44,c_1065]) ).
cnf(c_1067,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| op(e3,op(e2,e3)) != e2
| op(e2,op(e2,e3)) = e3
| op(e2,op(e1,e2)) != e1
| op(e1,op(e1,e2)) = e2
| op(e1,e2) != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_34,c_1066]) ).
cnf(c_1068,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| op(e3,op(e2,e3)) != e2
| op(e2,op(e2,e3)) = e3
| op(e2,op(e1,e2)) != e1
| op(e1,op(e1,e2)) = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_25,c_1067]) ).
cnf(c_1069,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| op(e3,op(e2,e3)) != e2
| op(e2,op(e2,e3)) = e3
| op(e2,op(e1,e2)) != e1
| op(e1,e3) = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_25,c_1068]) ).
cnf(c_1070,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| op(e3,op(e2,e3)) != e2
| op(e2,op(e2,e3)) = e3
| op(e2,op(e1,e2)) != e1
| e0 = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_26,c_1069]) ).
cnf(c_1071,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| op(e3,op(e2,e3)) != e2
| op(e2,op(e2,e3)) = e3
| op(e2,op(e1,e2)) != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_44,c_1070]) ).
cnf(c_1072,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| op(e3,op(e2,e3)) != e2
| op(e2,op(e2,e3)) = e3
| op(e2,e3) != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_25,c_1071]) ).
cnf(c_1073,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| op(e3,op(e2,e3)) != e2
| op(e2,op(e2,e3)) = e3
| e1 != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_31,c_1072]) ).
cnf(c_1074,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| op(e3,op(e2,e3)) != e2
| op(e2,e1) = e3
| e1 != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_31,c_1073]) ).
cnf(c_1075,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| op(e3,op(e2,e3)) != e2
| e0 = e3
| e1 != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_29,c_1074]) ).
cnf(c_1076,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| op(e3,op(e2,e3)) != e2
| unit = e3
| e1 != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_44,c_1075]) ).
cnf(c_1077,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| op(e3,e1) != e2
| unit = e3
| e1 != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_31,c_1076]) ).
cnf(c_1078,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,op(e1,e4)) = e4
| e2 != e2
| unit = e3
| e1 != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_34,c_1077]) ).
cnf(c_1079,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| op(e1,e2) = e4
| e2 != e2
| unit = e3
| e1 != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_27,c_1078]) ).
cnf(c_1080,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,op(e1,e4)) != e1
| e3 = e4
| e2 != e2
| unit = e3
| e1 != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_25,c_1079]) ).
cnf(c_1081,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| op(e4,e2) != e1
| e3 = e4
| e2 != e2
| unit = e3
| e1 != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_27,c_1080]) ).
cnf(c_1082,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| e1 != e1
| e3 = e4
| e2 != e2
| unit = e3
| e1 != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_40,c_1081]) ).
cnf(c_1083,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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,unit) != e0
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| e1 != e1
| e3 = e4
| e2 != e2
| unit = e3
| e1 != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_44,c_1082]) ).
cnf(c_1084,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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,unit) != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| e1 != e1
| e3 = e4
| e2 != e2
| unit = e3
| e1 != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_44,c_1083]) ).
cnf(c_1085,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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(unit,unit) != e0
| op(unit,unit) != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| e1 != e1
| e3 = e4
| e2 != e2
| unit = e3
| e1 != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_44,c_1084]) ).
cnf(c_1086,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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(unit,unit) != unit
| op(unit,unit) != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| e1 != e1
| e3 = e4
| e2 != e2
| unit = e3
| e1 != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_44,c_1085]) ).
cnf(c_1087,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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(unit,unit) != unit
| op(unit,unit) != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| e1 != e1
| e4 = e3
| e2 != e2
| unit = e3
| e1 != e1
| unit = e2
| e3 != e3
| unit = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1086]) ).
cnf(c_1088,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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(unit,unit) != unit
| op(unit,unit) != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| e1 != e1
| e4 = e3
| e2 != e2
| unit = e3
| e1 != e1
| unit = e2
| unit = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1087]) ).
cnf(c_1089,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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(unit,unit) != unit
| op(unit,unit) != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| e1 != e1
| e4 = e3
| e2 != e2
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1088]) ).
cnf(c_1090,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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(unit,unit) != unit
| op(unit,unit) != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| e1 != e1
| e4 = e3
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1089]) ).
cnf(c_1091,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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(unit,unit) != unit
| op(unit,unit) != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| e4 = e3
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1090]) ).
cnf(c_1092,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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(unit,unit) != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| e4 = e3
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1091]) ).
cnf(c_276,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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(unit,unit) != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(resolve,[status(thm)],[c_17,c_1092]) ).
cnf(c_434,negated_conjecture,
( op(e0,e4) != e4
| ~ defn_760 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_760]) ).
cnf(c_435,negated_conjecture,
( op(unit,e4) != e4
| ~ defn_760 ),
inference(paramod,[status(thm)],[c_44,c_434]) ).
cnf(c_441,negated_conjecture,
( op(e4,e0) != e4
| ~ defn_750 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_750]) ).
cnf(c_442,negated_conjecture,
( op(e4,unit) != e4
| ~ defn_750 ),
inference(paramod,[status(thm)],[c_44,c_441]) ).
cnf(c_446,negated_conjecture,
( op(e2,e4) != e3
| ~ defn_740 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_740]) ).
cnf(c_1093,negated_conjecture,
( e3 != e3
| ~ defn_740 ),
inference(paramod,[status(thm)],[c_32,c_446]) ).
cnf(c_447,negated_conjecture,
~ defn_740,
inference(copy,[status(thm)],[c_1093]) ).
cnf(c_454,negated_conjecture,
( op(e4,e1) != e3
| ~ defn_730 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_730]) ).
cnf(c_1094,negated_conjecture,
( e3 != e3
| ~ defn_730 ),
inference(paramod,[status(thm)],[c_39,c_454]) ).
cnf(c_455,negated_conjecture,
~ defn_730,
inference(copy,[status(thm)],[c_1094]) ).
cnf(c_461,negated_conjecture,
( op(e1,e4) != e2
| ~ defn_720 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_720]) ).
cnf(c_1095,negated_conjecture,
( e2 != e2
| ~ defn_720 ),
inference(paramod,[status(thm)],[c_27,c_461]) ).
cnf(c_462,negated_conjecture,
~ defn_720,
inference(copy,[status(thm)],[c_1095]) ).
cnf(c_466,negated_conjecture,
( op(e4,e3) != e2
| ~ defn_710 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_710]) ).
cnf(c_1096,negated_conjecture,
( e2 != e2
| ~ defn_710 ),
inference(paramod,[status(thm)],[c_41,c_466]) ).
cnf(c_467,negated_conjecture,
~ defn_710,
inference(copy,[status(thm)],[c_1096]) ).
cnf(c_473,negated_conjecture,
( op(e3,e4) != e1
| ~ defn_700 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_700]) ).
cnf(c_1097,negated_conjecture,
( e1 != e1
| ~ defn_700 ),
inference(paramod,[status(thm)],[c_37,c_473]) ).
cnf(c_474,negated_conjecture,
~ defn_700,
inference(copy,[status(thm)],[c_1097]) ).
cnf(c_481,negated_conjecture,
( op(e4,e2) != e1
| ~ defn_690 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_690]) ).
cnf(c_1098,negated_conjecture,
( e1 != e1
| ~ defn_690 ),
inference(paramod,[status(thm)],[c_40,c_481]) ).
cnf(c_482,negated_conjecture,
~ defn_690,
inference(copy,[status(thm)],[c_1098]) ).
cnf(c_485,negated_conjecture,
( op(e4,e4) != e0
| ~ defn_680 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_680]) ).
cnf(c_1099,negated_conjecture,
( e0 != e0
| ~ defn_680 ),
inference(paramod,[status(thm)],[c_42,c_485]) ).
cnf(c_1100,negated_conjecture,
( unit != e0
| ~ defn_680 ),
inference(paramod,[status(thm)],[c_44,c_1099]) ).
cnf(c_1101,negated_conjecture,
( unit != unit
| ~ defn_680 ),
inference(paramod,[status(thm)],[c_44,c_1100]) ).
cnf(c_486,negated_conjecture,
~ defn_680,
inference(copy,[status(thm)],[c_1101]) ).
cnf(c_491,negated_conjecture,
( op(e4,e4) != e0
| ~ defn_670 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_670]) ).
cnf(c_1102,negated_conjecture,
( e0 != e0
| ~ defn_670 ),
inference(paramod,[status(thm)],[c_42,c_491]) ).
cnf(c_1103,negated_conjecture,
( unit != e0
| ~ defn_670 ),
inference(paramod,[status(thm)],[c_44,c_1102]) ).
cnf(c_1104,negated_conjecture,
( unit != unit
| ~ defn_670 ),
inference(paramod,[status(thm)],[c_44,c_1103]) ).
cnf(c_492,negated_conjecture,
~ defn_670,
inference(copy,[status(thm)],[c_1104]) ).
cnf(c_498,negated_conjecture,
( op(e3,e3) != e4
| ~ defn_660 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_660]) ).
cnf(c_1105,negated_conjecture,
( e4 != e4
| ~ defn_660 ),
inference(paramod,[status(thm)],[c_36,c_498]) ).
cnf(c_499,negated_conjecture,
~ defn_660,
inference(copy,[status(thm)],[c_1105]) ).
cnf(c_504,negated_conjecture,
( op(e3,e3) != e4
| ~ defn_650 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_650]) ).
cnf(c_1106,negated_conjecture,
( e4 != e4
| ~ defn_650 ),
inference(paramod,[status(thm)],[c_36,c_504]) ).
cnf(c_505,negated_conjecture,
~ defn_650,
inference(copy,[status(thm)],[c_1106]) ).
cnf(c_514,negated_conjecture,
( op(e0,e3) != e3
| ~ defn_640 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_640]) ).
cnf(c_515,negated_conjecture,
( op(unit,e3) != e3
| ~ defn_640 ),
inference(paramod,[status(thm)],[c_44,c_514]) ).
cnf(c_521,negated_conjecture,
( op(e3,e0) != e3
| ~ defn_630 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_630]) ).
cnf(c_522,negated_conjecture,
( op(e3,unit) != e3
| ~ defn_630 ),
inference(paramod,[status(thm)],[c_44,c_521]) ).
cnf(c_523,negated_conjecture,
( op(e4,e3) != e2
| ~ defn_620 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_620]) ).
cnf(c_1107,negated_conjecture,
( e2 != e2
| ~ defn_620 ),
inference(paramod,[status(thm)],[c_41,c_523]) ).
cnf(c_524,negated_conjecture,
~ defn_620,
inference(copy,[status(thm)],[c_1107]) ).
cnf(c_533,negated_conjecture,
( op(e3,e1) != e2
| ~ defn_610 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_610]) ).
cnf(c_1108,negated_conjecture,
( e2 != e2
| ~ defn_610 ),
inference(paramod,[status(thm)],[c_34,c_533]) ).
cnf(c_534,negated_conjecture,
~ defn_610,
inference(copy,[status(thm)],[c_1108]) ).
cnf(c_538,negated_conjecture,
( op(e2,e3) != e1
| ~ defn_600 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_600]) ).
cnf(c_1109,negated_conjecture,
( e1 != e1
| ~ defn_600 ),
inference(paramod,[status(thm)],[c_31,c_538]) ).
cnf(c_539,negated_conjecture,
~ defn_600,
inference(copy,[status(thm)],[c_1109]) ).
cnf(c_542,negated_conjecture,
( op(e3,e4) != e1
| ~ defn_590 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_590]) ).
cnf(c_1110,negated_conjecture,
( e1 != e1
| ~ defn_590 ),
inference(paramod,[status(thm)],[c_37,c_542]) ).
cnf(c_543,negated_conjecture,
~ defn_590,
inference(copy,[status(thm)],[c_1110]) ).
cnf(c_554,negated_conjecture,
( op(e1,e3) != e0
| ~ defn_580 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_580]) ).
cnf(c_1111,negated_conjecture,
( e0 != e0
| ~ defn_580 ),
inference(paramod,[status(thm)],[c_26,c_554]) ).
cnf(c_1112,negated_conjecture,
( unit != e0
| ~ defn_580 ),
inference(paramod,[status(thm)],[c_44,c_1111]) ).
cnf(c_1113,negated_conjecture,
( unit != unit
| ~ defn_580 ),
inference(paramod,[status(thm)],[c_44,c_1112]) ).
cnf(c_555,negated_conjecture,
~ defn_580,
inference(copy,[status(thm)],[c_1113]) ).
cnf(c_561,negated_conjecture,
( op(e3,e2) != e0
| ~ defn_570 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_570]) ).
cnf(c_1114,negated_conjecture,
( e0 != e0
| ~ defn_570 ),
inference(paramod,[status(thm)],[c_35,c_561]) ).
cnf(c_1115,negated_conjecture,
( unit != e0
| ~ defn_570 ),
inference(paramod,[status(thm)],[c_44,c_1114]) ).
cnf(c_1116,negated_conjecture,
( unit != unit
| ~ defn_570 ),
inference(paramod,[status(thm)],[c_44,c_1115]) ).
cnf(c_562,negated_conjecture,
~ defn_570,
inference(copy,[status(thm)],[c_1116]) ).
cnf(c_568,negated_conjecture,
( op(e2,e2) != e4
| ~ defn_560 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_560]) ).
cnf(c_1117,negated_conjecture,
( e4 != e4
| ~ defn_560 ),
inference(paramod,[status(thm)],[c_30,c_568]) ).
cnf(c_569,negated_conjecture,
~ defn_560,
inference(copy,[status(thm)],[c_1117]) ).
cnf(c_574,negated_conjecture,
( op(e2,e2) != e4
| ~ defn_550 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_550]) ).
cnf(c_1118,negated_conjecture,
( e4 != e4
| ~ defn_550 ),
inference(paramod,[status(thm)],[c_30,c_574]) ).
cnf(c_575,negated_conjecture,
~ defn_550,
inference(copy,[status(thm)],[c_1118]) ).
cnf(c_582,negated_conjecture,
( op(e1,e2) != e3
| ~ defn_540 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_540]) ).
cnf(c_1119,negated_conjecture,
( e3 != e3
| ~ defn_540 ),
inference(paramod,[status(thm)],[c_25,c_582]) ).
cnf(c_583,negated_conjecture,
~ defn_540,
inference(copy,[status(thm)],[c_1119]) ).
cnf(c_585,negated_conjecture,
( op(e2,e4) != e3
| ~ defn_530 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_530]) ).
cnf(c_1120,negated_conjecture,
( e3 != e3
| ~ defn_530 ),
inference(paramod,[status(thm)],[c_32,c_585]) ).
cnf(c_586,negated_conjecture,
~ defn_530,
inference(copy,[status(thm)],[c_1120]) ).
cnf(c_596,negated_conjecture,
( op(e0,e2) != e2
| ~ defn_520 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_520]) ).
cnf(c_597,negated_conjecture,
( op(unit,e2) != e2
| ~ defn_520 ),
inference(paramod,[status(thm)],[c_44,c_596]) ).
cnf(c_603,negated_conjecture,
( op(e2,e0) != e2
| ~ defn_510 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_510]) ).
cnf(c_604,negated_conjecture,
( op(e2,unit) != e2
| ~ defn_510 ),
inference(paramod,[status(thm)],[c_44,c_603]) ).
cnf(c_605,negated_conjecture,
( op(e4,e2) != e1
| ~ defn_500 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_500]) ).
cnf(c_1121,negated_conjecture,
( e1 != e1
| ~ defn_500 ),
inference(paramod,[status(thm)],[c_40,c_605]) ).
cnf(c_606,negated_conjecture,
~ defn_500,
inference(copy,[status(thm)],[c_1121]) ).
cnf(c_612,negated_conjecture,
( op(e2,e3) != e1
| ~ defn_490 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_490]) ).
cnf(c_1122,negated_conjecture,
( e1 != e1
| ~ defn_490 ),
inference(paramod,[status(thm)],[c_31,c_612]) ).
cnf(c_613,negated_conjecture,
~ defn_490,
inference(copy,[status(thm)],[c_1122]) ).
cnf(c_619,negated_conjecture,
( op(e3,e2) != e0
| ~ defn_480 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_480]) ).
cnf(c_1123,negated_conjecture,
( e0 != e0
| ~ defn_480 ),
inference(paramod,[status(thm)],[c_35,c_619]) ).
cnf(c_1124,negated_conjecture,
( unit != e0
| ~ defn_480 ),
inference(paramod,[status(thm)],[c_44,c_1123]) ).
cnf(c_1125,negated_conjecture,
( unit != unit
| ~ defn_480 ),
inference(paramod,[status(thm)],[c_44,c_1124]) ).
cnf(c_620,negated_conjecture,
~ defn_480,
inference(copy,[status(thm)],[c_1125]) ).
cnf(c_630,negated_conjecture,
( op(e2,e1) != e0
| ~ defn_470 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_470]) ).
cnf(c_1126,negated_conjecture,
( e0 != e0
| ~ defn_470 ),
inference(paramod,[status(thm)],[c_29,c_630]) ).
cnf(c_1127,negated_conjecture,
( unit != e0
| ~ defn_470 ),
inference(paramod,[status(thm)],[c_44,c_1126]) ).
cnf(c_1128,negated_conjecture,
( unit != unit
| ~ defn_470 ),
inference(paramod,[status(thm)],[c_44,c_1127]) ).
cnf(c_631,negated_conjecture,
~ defn_470,
inference(copy,[status(thm)],[c_1128]) ).
cnf(c_637,negated_conjecture,
( op(e1,e1) != e4
| ~ defn_460 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_460]) ).
cnf(c_1129,negated_conjecture,
( e4 != e4
| ~ defn_460 ),
inference(paramod,[status(thm)],[c_24,c_637]) ).
cnf(c_638,negated_conjecture,
~ defn_460,
inference(copy,[status(thm)],[c_1129]) ).
cnf(c_644,negated_conjecture,
( op(e1,e1) != e4
| ~ defn_450 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_450]) ).
cnf(c_1130,negated_conjecture,
( e4 != e4
| ~ defn_450 ),
inference(paramod,[status(thm)],[c_24,c_644]) ).
cnf(c_645,negated_conjecture,
~ defn_450,
inference(copy,[status(thm)],[c_1130]) ).
cnf(c_647,negated_conjecture,
( op(e4,e1) != e3
| ~ defn_440 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_440]) ).
cnf(c_1131,negated_conjecture,
( e3 != e3
| ~ defn_440 ),
inference(paramod,[status(thm)],[c_39,c_647]) ).
cnf(c_648,negated_conjecture,
~ defn_440,
inference(copy,[status(thm)],[c_1131]) ).
cnf(c_656,negated_conjecture,
( op(e1,e2) != e3
| ~ defn_430 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_430]) ).
cnf(c_1132,negated_conjecture,
( e3 != e3
| ~ defn_430 ),
inference(paramod,[status(thm)],[c_25,c_656]) ).
cnf(c_657,negated_conjecture,
~ defn_430,
inference(copy,[status(thm)],[c_1132]) ).
cnf(c_661,negated_conjecture,
( op(e3,e1) != e2
| ~ defn_420 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_420]) ).
cnf(c_1133,negated_conjecture,
( e2 != e2
| ~ defn_420 ),
inference(paramod,[status(thm)],[c_34,c_661]) ).
cnf(c_662,negated_conjecture,
~ defn_420,
inference(copy,[status(thm)],[c_1133]) ).
cnf(c_666,negated_conjecture,
( op(e1,e4) != e2
| ~ defn_410 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_410]) ).
cnf(c_1134,negated_conjecture,
( e2 != e2
| ~ defn_410 ),
inference(paramod,[status(thm)],[c_27,c_666]) ).
cnf(c_667,negated_conjecture,
~ defn_410,
inference(copy,[status(thm)],[c_1134]) ).
cnf(c_677,negated_conjecture,
( op(e0,e1) != e1
| ~ defn_400 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_400]) ).
cnf(c_678,negated_conjecture,
( op(unit,e1) != e1
| ~ defn_400 ),
inference(paramod,[status(thm)],[c_44,c_677]) ).
cnf(c_684,negated_conjecture,
( op(e1,e0) != e1
| ~ defn_390 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_390]) ).
cnf(c_685,negated_conjecture,
( op(e1,unit) != e1
| ~ defn_390 ),
inference(paramod,[status(thm)],[c_44,c_684]) ).
cnf(c_690,negated_conjecture,
( op(e2,e1) != e0
| ~ defn_380 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_380]) ).
cnf(c_1135,negated_conjecture,
( e0 != e0
| ~ defn_380 ),
inference(paramod,[status(thm)],[c_29,c_690]) ).
cnf(c_1136,negated_conjecture,
( unit != e0
| ~ defn_380 ),
inference(paramod,[status(thm)],[c_44,c_1135]) ).
cnf(c_1137,negated_conjecture,
( unit != unit
| ~ defn_380 ),
inference(paramod,[status(thm)],[c_44,c_1136]) ).
cnf(c_691,negated_conjecture,
~ defn_380,
inference(copy,[status(thm)],[c_1137]) ).
cnf(c_696,negated_conjecture,
( op(e1,e3) != e0
| ~ defn_370 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_370]) ).
cnf(c_1138,negated_conjecture,
( e0 != e0
| ~ defn_370 ),
inference(paramod,[status(thm)],[c_26,c_696]) ).
cnf(c_1139,negated_conjecture,
( unit != e0
| ~ defn_370 ),
inference(paramod,[status(thm)],[c_44,c_1138]) ).
cnf(c_1140,negated_conjecture,
( unit != unit
| ~ defn_370 ),
inference(paramod,[status(thm)],[c_44,c_1139]) ).
cnf(c_697,negated_conjecture,
~ defn_370,
inference(copy,[status(thm)],[c_1140]) ).
cnf(c_701,negated_conjecture,
( op(e4,e0) != e4
| ~ defn_360 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_360]) ).
cnf(c_702,negated_conjecture,
( op(e4,unit) != e4
| ~ defn_360 ),
inference(paramod,[status(thm)],[c_44,c_701]) ).
cnf(c_711,negated_conjecture,
( op(e0,e4) != e4
| ~ defn_350 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_350]) ).
cnf(c_712,negated_conjecture,
( op(unit,e4) != e4
| ~ defn_350 ),
inference(paramod,[status(thm)],[c_44,c_711]) ).
cnf(c_723,negated_conjecture,
( op(e3,e0) != e3
| ~ defn_340 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_340]) ).
cnf(c_724,negated_conjecture,
( op(e3,unit) != e3
| ~ defn_340 ),
inference(paramod,[status(thm)],[c_44,c_723]) ).
cnf(c_733,negated_conjecture,
( op(e0,e3) != e3
| ~ defn_330 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_330]) ).
cnf(c_734,negated_conjecture,
( op(unit,e3) != e3
| ~ defn_330 ),
inference(paramod,[status(thm)],[c_44,c_733]) ).
cnf(c_745,negated_conjecture,
( op(e2,e0) != e2
| ~ defn_320 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_320]) ).
cnf(c_746,negated_conjecture,
( op(e2,unit) != e2
| ~ defn_320 ),
inference(paramod,[status(thm)],[c_44,c_745]) ).
cnf(c_755,negated_conjecture,
( op(e0,e2) != e2
| ~ defn_310 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_310]) ).
cnf(c_756,negated_conjecture,
( op(unit,e2) != e2
| ~ defn_310 ),
inference(paramod,[status(thm)],[c_44,c_755]) ).
cnf(c_767,negated_conjecture,
( op(e1,e0) != e1
| ~ defn_300 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_300]) ).
cnf(c_768,negated_conjecture,
( op(e1,unit) != e1
| ~ defn_300 ),
inference(paramod,[status(thm)],[c_44,c_767]) ).
cnf(c_777,negated_conjecture,
( op(e0,e1) != e1
| ~ defn_290 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_290]) ).
cnf(c_778,negated_conjecture,
( op(unit,e1) != e1
| ~ defn_290 ),
inference(paramod,[status(thm)],[c_44,c_777]) ).
cnf(c_789,negated_conjecture,
( op(e0,e0) != e0
| ~ defn_280 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_280]) ).
cnf(c_1141,negated_conjecture,
( op(unit,e0) != e0
| ~ defn_280 ),
inference(paramod,[status(thm)],[c_44,c_789]) ).
cnf(c_1142,negated_conjecture,
( op(unit,unit) != e0
| ~ defn_280 ),
inference(paramod,[status(thm)],[c_44,c_1141]) ).
cnf(c_790,negated_conjecture,
( op(unit,unit) != unit
| ~ defn_280 ),
inference(paramod,[status(thm)],[c_44,c_1142]) ).
cnf(c_799,negated_conjecture,
( op(e0,e0) != e0
| ~ defn_270 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_270]) ).
cnf(c_1143,negated_conjecture,
( op(unit,e0) != e0
| ~ defn_270 ),
inference(paramod,[status(thm)],[c_44,c_799]) ).
cnf(c_1144,negated_conjecture,
( op(unit,unit) != e0
| ~ defn_270 ),
inference(paramod,[status(thm)],[c_44,c_1143]) ).
cnf(c_800,negated_conjecture,
( op(unit,unit) != unit
| ~ defn_270 ),
inference(paramod,[status(thm)],[c_44,c_1144]) ).
cnf(c_805,negated_conjecture,
( unit != e0
| ~ defn_260 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_260]) ).
cnf(c_1145,negated_conjecture,
( unit != unit
| ~ defn_260 ),
inference(paramod,[status(thm)],[c_44,c_805]) ).
cnf(c_806,negated_conjecture,
~ defn_260,
inference(copy,[status(thm)],[c_1145]) ).
cnf(c_815,negated_conjecture,
( op(e4,e4) != e0
| ~ defn_250 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_250]) ).
cnf(c_1146,negated_conjecture,
( e0 != e0
| ~ defn_250 ),
inference(paramod,[status(thm)],[c_42,c_815]) ).
cnf(c_1147,negated_conjecture,
( unit != e0
| ~ defn_250 ),
inference(paramod,[status(thm)],[c_44,c_1146]) ).
cnf(c_1148,negated_conjecture,
( unit != unit
| ~ defn_250 ),
inference(paramod,[status(thm)],[c_44,c_1147]) ).
cnf(c_816,negated_conjecture,
~ defn_250,
inference(copy,[status(thm)],[c_1148]) ).
cnf(c_819,negated_conjecture,
( op(e4,e3) != e2
| ~ defn_240 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_240]) ).
cnf(c_1149,negated_conjecture,
( e2 != e2
| ~ defn_240 ),
inference(paramod,[status(thm)],[c_41,c_819]) ).
cnf(c_820,negated_conjecture,
~ defn_240,
inference(copy,[status(thm)],[c_1149]) ).
cnf(c_826,negated_conjecture,
( op(e4,e2) != e1
| ~ defn_230 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_230]) ).
cnf(c_1150,negated_conjecture,
( e1 != e1
| ~ defn_230 ),
inference(paramod,[status(thm)],[c_40,c_826]) ).
cnf(c_827,negated_conjecture,
~ defn_230,
inference(copy,[status(thm)],[c_1150]) ).
cnf(c_830,negated_conjecture,
( op(e4,e1) != e3
| ~ defn_220 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_220]) ).
cnf(c_1151,negated_conjecture,
( e3 != e3
| ~ defn_220 ),
inference(paramod,[status(thm)],[c_39,c_830]) ).
cnf(c_831,negated_conjecture,
~ defn_220,
inference(copy,[status(thm)],[c_1151]) ).
cnf(c_835,negated_conjecture,
( op(e4,e0) != e4
| ~ defn_210 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_210]) ).
cnf(c_836,negated_conjecture,
( op(e4,unit) != e4
| ~ defn_210 ),
inference(paramod,[status(thm)],[c_44,c_835]) ).
cnf(c_848,negated_conjecture,
( op(e3,e4) != e1
| ~ defn_200 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_200]) ).
cnf(c_1152,negated_conjecture,
( e1 != e1
| ~ defn_200 ),
inference(paramod,[status(thm)],[c_37,c_848]) ).
cnf(c_849,negated_conjecture,
~ defn_200,
inference(copy,[status(thm)],[c_1152]) ).
cnf(c_851,negated_conjecture,
( op(e3,e3) != e4
| ~ defn_190 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_190]) ).
cnf(c_1153,negated_conjecture,
( e4 != e4
| ~ defn_190 ),
inference(paramod,[status(thm)],[c_36,c_851]) ).
cnf(c_852,negated_conjecture,
~ defn_190,
inference(copy,[status(thm)],[c_1153]) ).
cnf(c_865,negated_conjecture,
( op(e3,e2) != e0
| ~ defn_180 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_180]) ).
cnf(c_1154,negated_conjecture,
( e0 != e0
| ~ defn_180 ),
inference(paramod,[status(thm)],[c_35,c_865]) ).
cnf(c_1155,negated_conjecture,
( unit != e0
| ~ defn_180 ),
inference(paramod,[status(thm)],[c_44,c_1154]) ).
cnf(c_1156,negated_conjecture,
( unit != unit
| ~ defn_180 ),
inference(paramod,[status(thm)],[c_44,c_1155]) ).
cnf(c_866,negated_conjecture,
~ defn_180,
inference(copy,[status(thm)],[c_1156]) ).
cnf(c_869,negated_conjecture,
( op(e3,e1) != e2
| ~ defn_170 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_170]) ).
cnf(c_1157,negated_conjecture,
( e2 != e2
| ~ defn_170 ),
inference(paramod,[status(thm)],[c_34,c_869]) ).
cnf(c_870,negated_conjecture,
~ defn_170,
inference(copy,[status(thm)],[c_1157]) ).
cnf(c_875,negated_conjecture,
( op(e3,e0) != e3
| ~ defn_160 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_160]) ).
cnf(c_876,negated_conjecture,
( op(e3,unit) != e3
| ~ defn_160 ),
inference(paramod,[status(thm)],[c_44,c_875]) ).
cnf(c_884,negated_conjecture,
( op(e2,e4) != e3
| ~ defn_150 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_150]) ).
cnf(c_1158,negated_conjecture,
( e3 != e3
| ~ defn_150 ),
inference(paramod,[status(thm)],[c_32,c_884]) ).
cnf(c_885,negated_conjecture,
~ defn_150,
inference(copy,[status(thm)],[c_1158]) ).
cnf(c_892,negated_conjecture,
( op(e2,e3) != e1
| ~ defn_140 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_140]) ).
cnf(c_1159,negated_conjecture,
( e1 != e1
| ~ defn_140 ),
inference(paramod,[status(thm)],[c_31,c_892]) ).
cnf(c_893,negated_conjecture,
~ defn_140,
inference(copy,[status(thm)],[c_1159]) ).
cnf(c_895,negated_conjecture,
( op(e2,e2) != e4
| ~ defn_130 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_130]) ).
cnf(c_1160,negated_conjecture,
( e4 != e4
| ~ defn_130 ),
inference(paramod,[status(thm)],[c_30,c_895]) ).
cnf(c_896,negated_conjecture,
~ defn_130,
inference(copy,[status(thm)],[c_1160]) ).
cnf(c_909,negated_conjecture,
( op(e2,e1) != e0
| ~ defn_120 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_120]) ).
cnf(c_1161,negated_conjecture,
( e0 != e0
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_29,c_909]) ).
cnf(c_1162,negated_conjecture,
( unit != e0
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_44,c_1161]) ).
cnf(c_1163,negated_conjecture,
( unit != unit
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_44,c_1162]) ).
cnf(c_910,negated_conjecture,
~ defn_120,
inference(copy,[status(thm)],[c_1163]) ).
cnf(c_915,negated_conjecture,
( op(e2,e0) != e2
| ~ defn_110 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_110]) ).
cnf(c_916,negated_conjecture,
( op(e2,unit) != e2
| ~ defn_110 ),
inference(paramod,[status(thm)],[c_44,c_915]) ).
cnf(c_923,negated_conjecture,
( op(e1,e4) != e2
| ~ defn_100 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_100]) ).
cnf(c_1164,negated_conjecture,
( e2 != e2
| ~ defn_100 ),
inference(paramod,[status(thm)],[c_27,c_923]) ).
cnf(c_924,negated_conjecture,
~ defn_100,
inference(copy,[status(thm)],[c_1164]) ).
cnf(c_935,negated_conjecture,
( op(e1,e3) != e0
| ~ defn_90 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_90]) ).
cnf(c_1165,negated_conjecture,
( e0 != e0
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_26,c_935]) ).
cnf(c_1166,negated_conjecture,
( unit != e0
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_44,c_1165]) ).
cnf(c_1167,negated_conjecture,
( unit != unit
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_44,c_1166]) ).
cnf(c_936,negated_conjecture,
~ defn_90,
inference(copy,[status(thm)],[c_1167]) ).
cnf(c_938,negated_conjecture,
( op(e1,e2) != e3
| ~ defn_80 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_80]) ).
cnf(c_1168,negated_conjecture,
( e3 != e3
| ~ defn_80 ),
inference(paramod,[status(thm)],[c_25,c_938]) ).
cnf(c_939,negated_conjecture,
~ defn_80,
inference(copy,[status(thm)],[c_1168]) ).
cnf(c_943,negated_conjecture,
( op(e1,e1) != e4
| ~ defn_70 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_70]) ).
cnf(c_1169,negated_conjecture,
( e4 != e4
| ~ defn_70 ),
inference(paramod,[status(thm)],[c_24,c_943]) ).
cnf(c_944,negated_conjecture,
~ defn_70,
inference(copy,[status(thm)],[c_1169]) ).
cnf(c_955,negated_conjecture,
( op(e1,e0) != e1
| ~ defn_60 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_60]) ).
cnf(c_956,negated_conjecture,
( op(e1,unit) != e1
| ~ defn_60 ),
inference(paramod,[status(thm)],[c_44,c_955]) ).
cnf(c_959,negated_conjecture,
( op(e0,e4) != e4
| ~ defn_50 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_50]) ).
cnf(c_960,negated_conjecture,
( op(unit,e4) != e4
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_44,c_959]) ).
cnf(c_971,negated_conjecture,
( op(e0,e3) != e3
| ~ defn_40 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_40]) ).
cnf(c_972,negated_conjecture,
( op(unit,e3) != e3
| ~ defn_40 ),
inference(paramod,[status(thm)],[c_44,c_971]) ).
cnf(c_983,negated_conjecture,
( op(e0,e2) != e2
| ~ defn_30 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_30]) ).
cnf(c_984,negated_conjecture,
( op(unit,e2) != e2
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_44,c_983]) ).
cnf(c_995,negated_conjecture,
( op(e0,e1) != e1
| ~ defn_20 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_20]) ).
cnf(c_996,negated_conjecture,
( op(unit,e1) != e1
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_44,c_995]) ).
cnf(c_1007,negated_conjecture,
( op(e0,e0) != e0
| ~ defn_10 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_10]) ).
cnf(c_1170,negated_conjecture,
( op(unit,e0) != e0
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_44,c_1007]) ).
cnf(c_1171,negated_conjecture,
( op(unit,unit) != e0
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_44,c_1170]) ).
cnf(c_1008,negated_conjecture,
( op(unit,unit) != unit
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_44,c_1171]) ).
cnf(c_1011,negated_conjecture,
( op(e0,op(e3,e0)) != e3
| op(e3,op(e3,e0)) = e0
| ~ defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00]) ).
cnf(c_1172,negated_conjecture,
( op(e0,op(e3,e0)) != e3
| op(e3,op(e3,unit)) = e0
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_44,c_1011]) ).
cnf(c_1173,negated_conjecture,
( op(e0,op(e3,e0)) != e3
| op(e3,op(e3,unit)) = unit
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_44,c_1172]) ).
cnf(c_1174,negated_conjecture,
( op(unit,op(e3,e0)) != e3
| op(e3,op(e3,unit)) = unit
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_44,c_1173]) ).
cnf(c_1012,negated_conjecture,
( op(unit,op(e3,unit)) != e3
| op(e3,op(e3,unit)) = unit
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_44,c_1174]) ).
cnf(c_1018,plain,
op(e4,unit) = e4,
inference(paramod,[status(thm)],[c_44,c_38]) ).
cnf(c_1020,plain,
op(e3,unit) = e3,
inference(paramod,[status(thm)],[c_44,c_33]) ).
cnf(c_1022,plain,
op(e2,unit) = e2,
inference(paramod,[status(thm)],[c_44,c_28]) ).
cnf(c_1024,plain,
op(e1,unit) = e1,
inference(paramod,[status(thm)],[c_44,c_23]) ).
cnf(c_1025,plain,
op(unit,e4) = e4,
inference(paramod,[status(thm)],[c_44,c_22]) ).
cnf(c_1026,plain,
op(unit,e3) = e3,
inference(paramod,[status(thm)],[c_44,c_21]) ).
cnf(c_1027,plain,
op(unit,e2) = e2,
inference(paramod,[status(thm)],[c_44,c_20]) ).
cnf(c_1028,plain,
op(unit,e1) = e1,
inference(paramod,[status(thm)],[c_44,c_19]) ).
cnf(c_1175,plain,
op(unit,e0) = e0,
inference(paramod,[status(thm)],[c_44,c_18]) ).
cnf(c_1176,plain,
op(unit,unit) = e0,
inference(paramod,[status(thm)],[c_44,c_1175]) ).
cnf(c_1029,plain,
op(unit,unit) = unit,
inference(paramod,[status(thm)],[c_44,c_1176]) ).
cnf(c_1030,plain,
unit != e4,
inference(paramod,[status(thm)],[c_44,c_11]) ).
cnf(c_1031,plain,
unit != e3,
inference(paramod,[status(thm)],[c_44,c_9]) ).
cnf(c_1032,plain,
unit != e2,
inference(paramod,[status(thm)],[c_44,c_7]) ).
cnf(c_1033,plain,
unit != e1,
inference(paramod,[status(thm)],[c_44,c_5]) ).
cnf(c_1177,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| unit != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_1029,c_276]) ).
cnf(c_1178,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| 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
| e1 != e1
| unit != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_1028,c_1177]) ).
cnf(c_1179,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| op(e4,unit) != e4
| op(unit,e4) != e4
| op(e3,unit) != e3
| op(unit,e3) != e3
| op(e2,unit) != e2
| op(unit,e2) != e2
| e1 != e1
| e1 != e1
| unit != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_1024,c_1178]) ).
cnf(c_1180,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| op(e4,unit) != e4
| op(unit,e4) != e4
| op(e3,unit) != e3
| op(unit,e3) != e3
| op(e2,unit) != e2
| e2 != e2
| e1 != e1
| e1 != e1
| unit != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_1027,c_1179]) ).
cnf(c_1181,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| op(e4,unit) != e4
| op(unit,e4) != e4
| op(e3,unit) != e3
| op(unit,e3) != e3
| e2 != e2
| e2 != e2
| e1 != e1
| e1 != e1
| unit != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_1022,c_1180]) ).
cnf(c_1182,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| op(e4,unit) != e4
| op(unit,e4) != e4
| op(e3,unit) != e3
| e3 != e3
| e2 != e2
| e2 != e2
| e1 != e1
| e1 != e1
| unit != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_1026,c_1181]) ).
cnf(c_1183,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| op(e4,unit) != e4
| op(unit,e4) != e4
| e3 != e3
| e3 != e3
| e2 != e2
| e2 != e2
| e1 != e1
| e1 != e1
| unit != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_1020,c_1182]) ).
cnf(c_1184,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| op(e4,unit) != e4
| e4 != e4
| e3 != e3
| e3 != e3
| e2 != e2
| e2 != e2
| e1 != e1
| e1 != e1
| unit != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_1025,c_1183]) ).
cnf(c_1185,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| e4 != e4
| e4 != e4
| e3 != e3
| e3 != e3
| e2 != e2
| e2 != e2
| e1 != e1
| e1 != e1
| unit != unit
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(paramod,[status(thm)],[c_1018,c_1184]) ).
cnf(c_1186,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| e4 != e4
| e4 != e4
| e3 != e3
| e3 != e3
| e2 != e2
| e2 != e2
| e1 != e1
| e1 != e1
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1185]) ).
cnf(c_1187,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| e4 != e4
| e4 != e4
| e3 != e3
| e3 != e3
| e2 != e2
| e2 != e2
| e1 != e1
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1186]) ).
cnf(c_1188,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| e4 != e4
| e4 != e4
| e3 != e3
| e3 != e3
| e2 != e2
| e2 != e2
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1187]) ).
cnf(c_1189,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| e4 != e4
| e4 != e4
| e3 != e3
| e3 != e3
| e2 != e2
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1188]) ).
cnf(c_1190,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| e4 != e4
| e4 != e4
| e3 != e3
| e3 != e3
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1189]) ).
cnf(c_1191,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| e4 != e4
| e4 != e4
| e3 != e3
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1190]) ).
cnf(c_1192,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| e4 != e4
| e4 != e4
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1191]) ).
cnf(c_1193,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| e4 != e4
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1192]) ).
cnf(c_1194,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| unit = e1
| defn_00 ),
inference(copy,[status(thm)],[c_1193]) ).
cnf(c_1195,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| unit = e2
| defn_00 ),
inference(resolve,[status(thm)],[c_1033,c_1194]) ).
cnf(c_1196,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| 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
| unit = e3
| defn_00 ),
inference(resolve,[status(thm)],[c_1032,c_1195]) ).
cnf(c_1197,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_1031,c_1196]) ).
cnf(c_1198,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_80
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_944,c_1197]) ).
cnf(c_1199,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_90
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_939,c_1198]) ).
cnf(c_1200,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_100
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_936,c_1199]) ).
cnf(c_1201,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_120
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_924,c_1200]) ).
cnf(c_1202,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| defn_130
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_910,c_1201]) ).
cnf(c_1203,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_140
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_896,c_1202]) ).
cnf(c_1204,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_150
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_893,c_1203]) ).
cnf(c_1205,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_170
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_885,c_1204]) ).
cnf(c_1206,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_180
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_870,c_1205]) ).
cnf(c_1207,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_190
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_866,c_1206]) ).
cnf(c_1208,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_200
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_852,c_1207]) ).
cnf(c_1209,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_849,c_1208]) ).
cnf(c_1210,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_831,c_1209]) ).
cnf(c_1211,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_827,c_1210]) ).
cnf(c_1212,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_250
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_820,c_1211]) ).
cnf(c_1213,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_260
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_816,c_1212]) ).
cnf(c_1214,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_370
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_806,c_1213]) ).
cnf(c_1215,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_697,c_1214]) ).
cnf(c_1216,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_691,c_1215]) ).
cnf(c_1217,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_667,c_1216]) ).
cnf(c_1218,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_662,c_1217]) ).
cnf(c_1219,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_657,c_1218]) ).
cnf(c_1220,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_450
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_648,c_1219]) ).
cnf(c_1221,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_460
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_645,c_1220]) ).
cnf(c_1222,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_470
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_638,c_1221]) ).
cnf(c_1223,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_480
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_631,c_1222]) ).
cnf(c_1224,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_490
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_620,c_1223]) ).
cnf(c_1225,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_500
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_613,c_1224]) ).
cnf(c_1226,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_530
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_606,c_1225]) ).
cnf(c_1227,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_540
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_586,c_1226]) ).
cnf(c_1228,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_550
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_583,c_1227]) ).
cnf(c_1229,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_560
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_575,c_1228]) ).
cnf(c_1230,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_570
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_569,c_1229]) ).
cnf(c_1231,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_580
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_562,c_1230]) ).
cnf(c_1232,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_590
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_555,c_1231]) ).
cnf(c_1233,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_600
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_543,c_1232]) ).
cnf(c_1234,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_610
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_539,c_1233]) ).
cnf(c_1235,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_620
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_534,c_1234]) ).
cnf(c_1236,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_650
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_524,c_1235]) ).
cnf(c_1237,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_660
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_505,c_1236]) ).
cnf(c_1238,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_670
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_499,c_1237]) ).
cnf(c_1239,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_680
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_492,c_1238]) ).
cnf(c_1240,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_690
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_486,c_1239]) ).
cnf(c_1241,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_700
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_482,c_1240]) ).
cnf(c_1242,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_710
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_474,c_1241]) ).
cnf(c_1243,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_720
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_467,c_1242]) ).
cnf(c_1244,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_730
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_462,c_1243]) ).
cnf(c_1245,negated_conjecture,
( defn_760
| defn_750
| defn_740
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_455,c_1244]) ).
cnf(c_1034,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10
| defn_00 ),
inference(resolve,[status(thm)],[c_447,c_1245]) ).
cnf(c_1246,negated_conjecture,
( e4 != e4
| ~ defn_210 ),
inference(paramod,[status(thm)],[c_1018,c_836]) ).
cnf(c_1035,negated_conjecture,
~ defn_210,
inference(copy,[status(thm)],[c_1246]) ).
cnf(c_1247,negated_conjecture,
( e4 != e4
| ~ defn_360 ),
inference(paramod,[status(thm)],[c_1018,c_702]) ).
cnf(c_1036,negated_conjecture,
~ defn_360,
inference(copy,[status(thm)],[c_1247]) ).
cnf(c_1248,negated_conjecture,
( e4 != e4
| ~ defn_750 ),
inference(paramod,[status(thm)],[c_1018,c_442]) ).
cnf(c_1037,negated_conjecture,
~ defn_750,
inference(copy,[status(thm)],[c_1248]) ).
cnf(c_1249,negated_conjecture,
( op(unit,op(e3,unit)) != e3
| op(e3,e3) = unit
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_1020,c_1012]) ).
cnf(c_1250,negated_conjecture,
( op(unit,op(e3,unit)) != e3
| e4 = unit
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_36,c_1249]) ).
cnf(c_1251,negated_conjecture,
( op(unit,e3) != e3
| e4 = unit
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_1020,c_1250]) ).
cnf(c_1252,negated_conjecture,
( e3 != e3
| e4 = unit
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_1026,c_1251]) ).
cnf(c_1253,negated_conjecture,
( e3 != e3
| unit = e4
| ~ defn_00 ),
inference(copy,[status(thm)],[c_1252]) ).
cnf(c_1254,negated_conjecture,
( unit = e4
| ~ defn_00 ),
inference(copy,[status(thm)],[c_1253]) ).
cnf(c_1038,negated_conjecture,
~ defn_00,
inference(resolve,[status(thm)],[c_1030,c_1254]) ).
cnf(c_1255,negated_conjecture,
( e3 != e3
| ~ defn_160 ),
inference(paramod,[status(thm)],[c_1020,c_876]) ).
cnf(c_1039,negated_conjecture,
~ defn_160,
inference(copy,[status(thm)],[c_1255]) ).
cnf(c_1256,negated_conjecture,
( e3 != e3
| ~ defn_340 ),
inference(paramod,[status(thm)],[c_1020,c_724]) ).
cnf(c_1040,negated_conjecture,
~ defn_340,
inference(copy,[status(thm)],[c_1256]) ).
cnf(c_1257,negated_conjecture,
( e3 != e3
| ~ defn_630 ),
inference(paramod,[status(thm)],[c_1020,c_522]) ).
cnf(c_1041,negated_conjecture,
~ defn_630,
inference(copy,[status(thm)],[c_1257]) ).
cnf(c_1258,negated_conjecture,
( e2 != e2
| ~ defn_110 ),
inference(paramod,[status(thm)],[c_1022,c_916]) ).
cnf(c_1042,negated_conjecture,
~ defn_110,
inference(copy,[status(thm)],[c_1258]) ).
cnf(c_1259,negated_conjecture,
( e2 != e2
| ~ defn_320 ),
inference(paramod,[status(thm)],[c_1022,c_746]) ).
cnf(c_1043,negated_conjecture,
~ defn_320,
inference(copy,[status(thm)],[c_1259]) ).
cnf(c_1260,negated_conjecture,
( e2 != e2
| ~ defn_510 ),
inference(paramod,[status(thm)],[c_1022,c_604]) ).
cnf(c_1044,negated_conjecture,
~ defn_510,
inference(copy,[status(thm)],[c_1260]) ).
cnf(c_1261,negated_conjecture,
( e1 != e1
| ~ defn_60 ),
inference(paramod,[status(thm)],[c_1024,c_956]) ).
cnf(c_1045,negated_conjecture,
~ defn_60,
inference(copy,[status(thm)],[c_1261]) ).
cnf(c_1262,negated_conjecture,
( e1 != e1
| ~ defn_300 ),
inference(paramod,[status(thm)],[c_1024,c_768]) ).
cnf(c_1046,negated_conjecture,
~ defn_300,
inference(copy,[status(thm)],[c_1262]) ).
cnf(c_1263,negated_conjecture,
( e1 != e1
| ~ defn_390 ),
inference(paramod,[status(thm)],[c_1024,c_685]) ).
cnf(c_1047,negated_conjecture,
~ defn_390,
inference(copy,[status(thm)],[c_1263]) ).
cnf(c_1264,negated_conjecture,
( e4 != e4
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_1025,c_960]) ).
cnf(c_1048,negated_conjecture,
~ defn_50,
inference(copy,[status(thm)],[c_1264]) ).
cnf(c_1265,negated_conjecture,
( e4 != e4
| ~ defn_350 ),
inference(paramod,[status(thm)],[c_1025,c_712]) ).
cnf(c_1049,negated_conjecture,
~ defn_350,
inference(copy,[status(thm)],[c_1265]) ).
cnf(c_1266,negated_conjecture,
( e4 != e4
| ~ defn_760 ),
inference(paramod,[status(thm)],[c_1025,c_435]) ).
cnf(c_1050,negated_conjecture,
~ defn_760,
inference(copy,[status(thm)],[c_1266]) ).
cnf(c_1267,negated_conjecture,
( e3 != e3
| ~ defn_40 ),
inference(paramod,[status(thm)],[c_1026,c_972]) ).
cnf(c_1051,negated_conjecture,
~ defn_40,
inference(copy,[status(thm)],[c_1267]) ).
cnf(c_1268,negated_conjecture,
( e3 != e3
| ~ defn_330 ),
inference(paramod,[status(thm)],[c_1026,c_734]) ).
cnf(c_1052,negated_conjecture,
~ defn_330,
inference(copy,[status(thm)],[c_1268]) ).
cnf(c_1269,negated_conjecture,
( e3 != e3
| ~ defn_640 ),
inference(paramod,[status(thm)],[c_1026,c_515]) ).
cnf(c_1053,negated_conjecture,
~ defn_640,
inference(copy,[status(thm)],[c_1269]) ).
cnf(c_1270,negated_conjecture,
( e2 != e2
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_1027,c_984]) ).
cnf(c_1054,negated_conjecture,
~ defn_30,
inference(copy,[status(thm)],[c_1270]) ).
cnf(c_1271,negated_conjecture,
( e2 != e2
| ~ defn_310 ),
inference(paramod,[status(thm)],[c_1027,c_756]) ).
cnf(c_1055,negated_conjecture,
~ defn_310,
inference(copy,[status(thm)],[c_1271]) ).
cnf(c_1272,negated_conjecture,
( e2 != e2
| ~ defn_520 ),
inference(paramod,[status(thm)],[c_1027,c_597]) ).
cnf(c_1056,negated_conjecture,
~ defn_520,
inference(copy,[status(thm)],[c_1272]) ).
cnf(c_1273,negated_conjecture,
( e1 != e1
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_1028,c_996]) ).
cnf(c_1057,negated_conjecture,
~ defn_20,
inference(copy,[status(thm)],[c_1273]) ).
cnf(c_1274,negated_conjecture,
( e1 != e1
| ~ defn_290 ),
inference(paramod,[status(thm)],[c_1028,c_778]) ).
cnf(c_1058,negated_conjecture,
~ defn_290,
inference(copy,[status(thm)],[c_1274]) ).
cnf(c_1275,negated_conjecture,
( e1 != e1
| ~ defn_400 ),
inference(paramod,[status(thm)],[c_1028,c_678]) ).
cnf(c_1059,negated_conjecture,
~ defn_400,
inference(copy,[status(thm)],[c_1275]) ).
cnf(c_1276,negated_conjecture,
( unit != unit
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_1029,c_1008]) ).
cnf(c_1060,negated_conjecture,
~ defn_10,
inference(copy,[status(thm)],[c_1276]) ).
cnf(c_1277,negated_conjecture,
( unit != unit
| ~ defn_270 ),
inference(paramod,[status(thm)],[c_1029,c_800]) ).
cnf(c_1061,negated_conjecture,
~ defn_270,
inference(copy,[status(thm)],[c_1277]) ).
cnf(c_1278,negated_conjecture,
( unit != unit
| ~ defn_280 ),
inference(paramod,[status(thm)],[c_1029,c_790]) ).
cnf(c_1062,negated_conjecture,
~ defn_280,
inference(copy,[status(thm)],[c_1278]) ).
cnf(c_1279,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20
| defn_10 ),
inference(resolve,[status(thm)],[c_1038,c_1034]) ).
cnf(c_1280,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30
| defn_20 ),
inference(resolve,[status(thm)],[c_1060,c_1279]) ).
cnf(c_1281,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40
| defn_30 ),
inference(resolve,[status(thm)],[c_1057,c_1280]) ).
cnf(c_1282,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50
| defn_40 ),
inference(resolve,[status(thm)],[c_1054,c_1281]) ).
cnf(c_1283,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60
| defn_50 ),
inference(resolve,[status(thm)],[c_1051,c_1282]) ).
cnf(c_1284,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110
| defn_60 ),
inference(resolve,[status(thm)],[c_1048,c_1283]) ).
cnf(c_1285,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160
| defn_110 ),
inference(resolve,[status(thm)],[c_1045,c_1284]) ).
cnf(c_1286,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210
| defn_160 ),
inference(resolve,[status(thm)],[c_1042,c_1285]) ).
cnf(c_1287,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270
| defn_210 ),
inference(resolve,[status(thm)],[c_1039,c_1286]) ).
cnf(c_1288,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280
| defn_270 ),
inference(resolve,[status(thm)],[c_1035,c_1287]) ).
cnf(c_1289,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290
| defn_280 ),
inference(resolve,[status(thm)],[c_1061,c_1288]) ).
cnf(c_1290,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300
| defn_290 ),
inference(resolve,[status(thm)],[c_1062,c_1289]) ).
cnf(c_1291,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310
| defn_300 ),
inference(resolve,[status(thm)],[c_1058,c_1290]) ).
cnf(c_1292,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320
| defn_310 ),
inference(resolve,[status(thm)],[c_1046,c_1291]) ).
cnf(c_1293,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330
| defn_320 ),
inference(resolve,[status(thm)],[c_1055,c_1292]) ).
cnf(c_1294,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340
| defn_330 ),
inference(resolve,[status(thm)],[c_1043,c_1293]) ).
cnf(c_1295,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350
| defn_340 ),
inference(resolve,[status(thm)],[c_1052,c_1294]) ).
cnf(c_1296,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360
| defn_350 ),
inference(resolve,[status(thm)],[c_1040,c_1295]) ).
cnf(c_1297,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390
| defn_360 ),
inference(resolve,[status(thm)],[c_1049,c_1296]) ).
cnf(c_1298,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400
| defn_390 ),
inference(resolve,[status(thm)],[c_1036,c_1297]) ).
cnf(c_1299,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510
| defn_400 ),
inference(resolve,[status(thm)],[c_1047,c_1298]) ).
cnf(c_1300,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520
| defn_510 ),
inference(resolve,[status(thm)],[c_1059,c_1299]) ).
cnf(c_1301,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630
| defn_520 ),
inference(resolve,[status(thm)],[c_1044,c_1300]) ).
cnf(c_1302,negated_conjecture,
( defn_760
| defn_750
| defn_640
| defn_630 ),
inference(resolve,[status(thm)],[c_1056,c_1301]) ).
cnf(c_1303,negated_conjecture,
( defn_760
| defn_750
| defn_640 ),
inference(resolve,[status(thm)],[c_1041,c_1302]) ).
cnf(c_1304,negated_conjecture,
( defn_760
| defn_750 ),
inference(resolve,[status(thm)],[c_1053,c_1303]) ).
cnf(c_1305,negated_conjecture,
defn_760,
inference(resolve,[status(thm)],[c_1037,c_1304]) ).
cnf(c_1063,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1050,c_1305]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG092+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/15.39 % Computer : n019.cluster.edu
% 0.09/15.39 % Model : x86_64 x86_64
% 0.09/15.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/15.39 % Memory : 8046.5625MB
% 0.09/15.39 % OS : Linux 6.8.0-71-generic
% 0.09/15.39 % CPULimit : 300
% 0.09/15.39 % WCLimit : 300
% 0.09/15.39 % DateTime : Sat Sep 26 21:08:07 UTC 2026
% 0.09/15.39 % CPUTime :
% 0.09/15.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/15.39 % Process 2195530 was started by sandbox on n019,
% 0.09/15.39 % Sat Sep 26 21:08:07 2026
% 0.09/15.39 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 1.54/16.86
% 1.54/16.86 % From the command line: assign(max_seconds, 300).
% 2.72/17.05
% 2.72/17.05 % SZS status Theorem for theBenchmark
% 2.72/17.05
% 2.72/17.05 % Proof 1 at 0.16 (+ 0.01) seconds.
% 2.72/17.05 % Length of proof is 238.
% 2.72/17.05 % Level of proof is 5.
% 2.72/17.05 % Maximum clause weight is 141.000.
% 2.72/17.05 % Given clauses 0.
% 2.72/17.05
% 2.72/17.05 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------