%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG044+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 : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:49:20 AM UTC 2026
% Result : Theorem 1.02s 1.32s
% Output : CNFRefutation 1.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 78
% Number of leaves : 53
% Syntax : Number of formulae : 361 ( 86 unt; 49 def)
% Number of atoms : 3857 (1063 equ)
% Maximal formula atoms : 220 ( 10 avg)
% Number of connectives : 4244 ( 748 ~;3142 |; 305 &)
% ( 49 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 62 ( 11 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 51 ( 49 usr; 50 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax1,axiom,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ),
file('theBenchmark.p',ax1) ).
fof(ax2,axiom,
( op(e3,e3) = e0
& op(e3,e2) = e1
& op(e3,e1) = e2
& op(e3,e0) = e3
& op(e2,e3) = e1
& op(e2,e2) = e3
& op(e2,e1) = e0
& op(e2,e0) = e2
& op(e1,e3) = e2
& op(e1,e2) = e0
& op(e1,e1) = e3
& op(e1,e0) = e1
& op(e0,e3) = e3
& op(e0,e2) = e2
& op(e0,e1) = e1
& op(e0,e0) = e0 ),
file('theBenchmark.p',ax2) ).
fof(co1,conjecture,
( ( op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 )
& ( op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 )
& ( op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 )
& ( op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 )
& ( op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 )
& ( op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 )
& ( op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 )
& ( op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 )
& ( op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 )
& ( op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 )
& ( op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 )
& ( op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 )
& ( op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 )
& ( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 )
& ( op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 )
& ( op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 )
& ( op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 )
& ( op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 )
& ( op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 )
& ( op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 )
& ( op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 )
& ( op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 )
& ( op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 )
& ( op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 )
& ( op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 )
& ( op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 )
& ( op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 )
& ( op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 )
& ( op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 )
& ( op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 )
& ( op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 )
& ( op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 )
& ( unit = e3
| unit = e2
| unit = e1
| unit = e0 )
& 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(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 )
& ( op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 )
& ( op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 )
& ( op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 )
& ( op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 )
& ( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 )
& ( op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 )
& ( op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 )
& ( op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 )
& ( op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 )
& ( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 )
& ( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 )
& ( op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 )
& ( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 )
& ( op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 )
& ( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 )
& ~ ( ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ( ( op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 )
& ( op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 )
& ( op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 )
& ( op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 )
& ( op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 )
& ( op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 )
& ( op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 )
& ( op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 )
& ( op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 )
& ( op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 )
& ( op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 )
& ( op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 )
& ( op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 )
& ( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 )
& ( op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 )
& ( op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 )
& ( op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 )
& ( op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 )
& ( op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 )
& ( op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 )
& ( op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 )
& ( op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 )
& ( op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 )
& ( op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 )
& ( op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 )
& ( op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 )
& ( op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 )
& ( op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 )
& ( op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 )
& ( op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 )
& ( op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 )
& ( op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 )
& ( unit = e3
| unit = e2
| unit = e1
| unit = e0 )
& 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(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 )
& ( op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 )
& ( op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 )
& ( op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 )
& ( op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 )
& ( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 )
& ( op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 )
& ( op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 )
& ( op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 )
& ( op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 )
& ( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 )
& ( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 )
& ( op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 )
& ( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 )
& ( op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 )
& ( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 )
& ~ ( ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_7,plain,
e3 != e0,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_8,plain,
e0 != e3,
inference(copy,[status(thm)],[c_7]) ).
cnf(c_11,plain,
e3 != e1,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_12,plain,
e1 != e3,
inference(copy,[status(thm)],[c_11]) ).
cnf(c_13,plain,
e3 != e2,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_14,plain,
e2 != e3,
inference(copy,[status(thm)],[c_13]) ).
cnf(c_15,plain,
op(e0,e0) = e0,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_16,plain,
op(e0,e1) = e1,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_17,plain,
op(e0,e2) = e2,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_18,plain,
op(e0,e3) = e3,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_19,plain,
op(e1,e0) = e1,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_20,plain,
op(e1,e1) = e3,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_21,plain,
op(e1,e2) = e0,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_22,plain,
op(e1,e3) = e2,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_23,plain,
op(e2,e0) = e2,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_24,plain,
op(e2,e1) = e0,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_25,plain,
op(e2,e2) = e3,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_26,plain,
op(e2,e3) = e1,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_27,plain,
op(e3,e0) = e3,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_28,plain,
op(e3,e1) = e2,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_29,plain,
op(e3,e2) = e1,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_30,plain,
op(e3,e3) = e0,
inference(clausify,[status(thm)],[ax2]) ).
fof(ax3,axiom,
unit = e0,
file('theBenchmark.p',ax3) ).
cnf(c_31,plain,
unit = e0,
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_32,plain,
e0 = unit,
inference(copy,[status(thm)],[c_31]) ).
fof(def_defn_00,definition,
( defn_00
<=> ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) ),
introduced(definition,[new_symbols(definition,[defn_00])],[]) ).
fof(def_defn_10,definition,
( defn_10
<=> ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 ) ),
introduced(definition,[new_symbols(definition,[defn_10])],[]) ).
fof(def_defn_20,definition,
( defn_20
<=> ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 ) ),
introduced(definition,[new_symbols(definition,[defn_20])],[]) ).
fof(def_defn_30,definition,
( defn_30
<=> ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 ) ),
introduced(definition,[new_symbols(definition,[defn_30])],[]) ).
fof(def_defn_40,definition,
( defn_40
<=> ( op(e0,e0) != e3
& op(e0,e0) != e2
& op(e0,e0) != e1
& op(e0,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_40])],[]) ).
fof(def_defn_50,definition,
( defn_50
<=> ( op(e0,e1) != e3
& op(e0,e1) != e2
& op(e0,e1) != e1
& op(e0,e1) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_50])],[]) ).
fof(def_defn_60,definition,
( defn_60
<=> ( op(e0,e2) != e3
& op(e0,e2) != e2
& op(e0,e2) != e1
& op(e0,e2) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_60])],[]) ).
fof(def_defn_70,definition,
( defn_70
<=> ( op(e0,e3) != e3
& op(e0,e3) != e2
& op(e0,e3) != e1
& op(e0,e3) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_70])],[]) ).
fof(def_defn_80,definition,
( defn_80
<=> ( op(e1,e0) != e3
& op(e1,e0) != e2
& op(e1,e0) != e1
& op(e1,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_80])],[]) ).
fof(def_defn_90,definition,
( defn_90
<=> ( op(e1,e1) != e3
& op(e1,e1) != e2
& op(e1,e1) != e1
& op(e1,e1) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_90])],[]) ).
fof(def_defn_100,definition,
( defn_100
<=> ( op(e1,e2) != e3
& op(e1,e2) != e2
& op(e1,e2) != e1
& op(e1,e2) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_100])],[]) ).
fof(def_defn_110,definition,
( defn_110
<=> ( op(e1,e3) != e3
& op(e1,e3) != e2
& op(e1,e3) != e1
& op(e1,e3) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_110])],[]) ).
fof(def_defn_120,definition,
( defn_120
<=> ( op(e2,e0) != e3
& op(e2,e0) != e2
& op(e2,e0) != e1
& op(e2,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_120])],[]) ).
fof(def_defn_130,definition,
( defn_130
<=> ( op(e2,e1) != e3
& op(e2,e1) != e2
& op(e2,e1) != e1
& op(e2,e1) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_130])],[]) ).
fof(def_defn_140,definition,
( defn_140
<=> ( op(e2,e2) != e3
& op(e2,e2) != e2
& op(e2,e2) != e1
& op(e2,e2) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_140])],[]) ).
fof(def_defn_150,definition,
( defn_150
<=> ( op(e2,e3) != e3
& op(e2,e3) != e2
& op(e2,e3) != e1
& op(e2,e3) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_150])],[]) ).
fof(def_defn_160,definition,
( defn_160
<=> ( 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) != 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) != 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) != 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
<=> ( unit != e3
& unit != e2
& unit != e1
& unit != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_200])],[]) ).
fof(def_defn_210,definition,
( defn_210
<=> ( op(e0,e3) != e0
& op(e0,e2) != e0
& op(e0,e1) != e0
& op(e0,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_210])],[]) ).
fof(def_defn_220,definition,
( defn_220
<=> ( op(e3,e0) != e0
& op(e2,e0) != e0
& op(e1,e0) != e0
& op(e0,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_220])],[]) ).
fof(def_defn_230,definition,
( defn_230
<=> ( op(e0,e3) != e1
& op(e0,e2) != e1
& op(e0,e1) != e1
& op(e0,e0) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_230])],[]) ).
fof(def_defn_240,definition,
( defn_240
<=> ( op(e3,e0) != e1
& op(e2,e0) != e1
& op(e1,e0) != e1
& op(e0,e0) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_240])],[]) ).
fof(def_defn_250,definition,
( defn_250
<=> ( op(e0,e3) != e2
& op(e0,e2) != e2
& op(e0,e1) != e2
& op(e0,e0) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_250])],[]) ).
fof(def_defn_260,definition,
( defn_260
<=> ( op(e3,e0) != e2
& op(e2,e0) != e2
& op(e1,e0) != e2
& op(e0,e0) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_260])],[]) ).
fof(def_defn_270,definition,
( defn_270
<=> ( op(e0,e3) != e3
& op(e0,e2) != e3
& op(e0,e1) != e3
& op(e0,e0) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_270])],[]) ).
fof(def_defn_280,definition,
( defn_280
<=> ( op(e3,e0) != e3
& op(e2,e0) != e3
& op(e1,e0) != e3
& op(e0,e0) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_280])],[]) ).
fof(def_defn_290,definition,
( defn_290
<=> ( op(e1,e3) != e0
& op(e1,e2) != e0
& op(e1,e1) != e0
& op(e1,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_290])],[]) ).
fof(def_defn_300,definition,
( defn_300
<=> ( op(e3,e1) != e0
& op(e2,e1) != e0
& op(e1,e1) != e0
& op(e0,e1) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_300])],[]) ).
fof(def_defn_310,definition,
( defn_310
<=> ( op(e1,e3) != e1
& op(e1,e2) != e1
& op(e1,e1) != e1
& op(e1,e0) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_310])],[]) ).
fof(def_defn_320,definition,
( defn_320
<=> ( op(e3,e1) != e1
& op(e2,e1) != e1
& op(e1,e1) != e1
& op(e0,e1) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_320])],[]) ).
fof(def_defn_330,definition,
( defn_330
<=> ( op(e1,e3) != e2
& op(e1,e2) != e2
& op(e1,e1) != e2
& op(e1,e0) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_330])],[]) ).
fof(def_defn_340,definition,
( defn_340
<=> ( op(e3,e1) != e2
& op(e2,e1) != e2
& op(e1,e1) != e2
& op(e0,e1) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_340])],[]) ).
fof(def_defn_350,definition,
( defn_350
<=> ( op(e1,e3) != e3
& op(e1,e2) != e3
& op(e1,e1) != e3
& op(e1,e0) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_350])],[]) ).
fof(def_defn_360,definition,
( defn_360
<=> ( op(e3,e1) != e3
& op(e2,e1) != e3
& op(e1,e1) != e3
& op(e0,e1) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_360])],[]) ).
fof(def_defn_370,definition,
( defn_370
<=> ( op(e2,e3) != e0
& op(e2,e2) != e0
& op(e2,e1) != e0
& op(e2,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_370])],[]) ).
fof(def_defn_380,definition,
( defn_380
<=> ( op(e3,e2) != e0
& op(e2,e2) != e0
& op(e1,e2) != e0
& op(e0,e2) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_380])],[]) ).
fof(def_defn_390,definition,
( defn_390
<=> ( op(e2,e3) != e1
& op(e2,e2) != e1
& op(e2,e1) != e1
& op(e2,e0) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_390])],[]) ).
fof(def_defn_400,definition,
( defn_400
<=> ( op(e3,e2) != e1
& op(e2,e2) != e1
& op(e1,e2) != e1
& op(e0,e2) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_400])],[]) ).
fof(def_defn_410,definition,
( defn_410
<=> ( op(e2,e3) != e2
& op(e2,e2) != e2
& op(e2,e1) != e2
& op(e2,e0) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_410])],[]) ).
fof(def_defn_420,definition,
( defn_420
<=> ( op(e3,e2) != e2
& op(e2,e2) != e2
& op(e1,e2) != e2
& op(e0,e2) != e2 ) ),
introduced(definition,[new_symbols(definition,[defn_420])],[]) ).
fof(def_defn_430,definition,
( defn_430
<=> ( op(e2,e3) != e3
& op(e2,e2) != e3
& op(e2,e1) != e3
& op(e2,e0) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_430])],[]) ).
fof(def_defn_440,definition,
( defn_440
<=> ( op(e3,e2) != e3
& op(e2,e2) != e3
& op(e1,e2) != e3
& op(e0,e2) != e3 ) ),
introduced(definition,[new_symbols(definition,[defn_440])],[]) ).
fof(def_defn_450,definition,
( defn_450
<=> ( op(e3,e3) != e0
& op(e3,e2) != e0
& op(e3,e1) != e0
& op(e3,e0) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_450])],[]) ).
fof(def_defn_460,definition,
( defn_460
<=> ( op(e3,e3) != e0
& op(e2,e3) != e0
& op(e1,e3) != e0
& op(e0,e3) != e0 ) ),
introduced(definition,[new_symbols(definition,[defn_460])],[]) ).
fof(def_defn_470,definition,
( defn_470
<=> ( op(e3,e3) != e1
& op(e3,e2) != e1
& op(e3,e1) != e1
& op(e3,e0) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_470])],[]) ).
fof(def_defn_480,definition,
( defn_480
<=> ( op(e3,e3) != e1
& op(e2,e3) != e1
& op(e1,e3) != e1
& op(e0,e3) != e1 ) ),
introduced(definition,[new_symbols(definition,[defn_480])],[]) ).
cnf(c_76,negated_conjecture,
( op(e0,e3) != e3
| op(e3,e0) != e3
| op(e1,e3) != e2
| op(e3,e1) != e2
| 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
| 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_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(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]) ).
cnf(c_492,negated_conjecture,
( op(e0,e3) != e3
| op(e3,e0) != e3
| op(e1,e3) != e2
| op(e3,e1) != e2
| 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
| 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_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(paramod,[status(thm)],[c_32,c_76]) ).
cnf(c_493,negated_conjecture,
( op(e0,e3) != e3
| op(e3,e0) != e3
| op(e1,e3) != e2
| op(e3,e1) != e2
| 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
| 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_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(paramod,[status(thm)],[c_32,c_492]) ).
cnf(c_494,negated_conjecture,
( op(e0,e3) != e3
| op(e3,e0) != e3
| op(e1,e3) != e2
| op(e3,e1) != e2
| 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
| 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_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(paramod,[status(thm)],[c_32,c_493]) ).
cnf(c_495,negated_conjecture,
( op(e0,e3) != e3
| op(e3,e0) != e3
| op(e1,e3) != e2
| op(e3,e1) != e2
| 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
| 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_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(paramod,[status(thm)],[c_32,c_494]) ).
cnf(c_496,negated_conjecture,
( op(e0,e3) != e3
| op(e3,e0) != e3
| op(e1,e3) != e2
| e2 != e2
| 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
| 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_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(paramod,[status(thm)],[c_28,c_495]) ).
cnf(c_497,negated_conjecture,
( op(e0,e3) != e3
| op(e3,e0) != e3
| e2 != e2
| e2 != e2
| 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
| 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_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(paramod,[status(thm)],[c_22,c_496]) ).
cnf(c_498,negated_conjecture,
( op(e0,e3) != e3
| op(e3,unit) != e3
| e2 != e2
| e2 != e2
| 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
| 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_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(paramod,[status(thm)],[c_32,c_497]) ).
cnf(c_499,negated_conjecture,
( op(unit,e3) != e3
| op(e3,unit) != e3
| e2 != e2
| e2 != e2
| 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
| 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_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(paramod,[status(thm)],[c_32,c_498]) ).
cnf(c_500,negated_conjecture,
( op(unit,e3) != e3
| op(e3,unit) != e3
| e2 != e2
| 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
| 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_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(copy,[status(thm)],[c_499]) ).
cnf(c_501,negated_conjecture,
( op(unit,e3) != e3
| op(e3,unit) != e3
| 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
| 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_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(copy,[status(thm)],[c_500]) ).
cnf(c_502,negated_conjecture,
( op(unit,e3) != e3
| op(e3,unit) != e3
| 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
| 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_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(copy,[status(thm)],[c_501]) ).
cnf(c_503,negated_conjecture,
( op(unit,e3) != e3
| 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
| 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_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(copy,[status(thm)],[c_502]) ).
cnf(c_77,negated_conjecture,
( 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
| 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_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(copy,[status(thm)],[c_503]) ).
cnf(c_139,negated_conjecture,
( op(e2,e3) != e1
| ~ defn_480 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_480]) ).
cnf(c_504,negated_conjecture,
( e1 != e1
| ~ defn_480 ),
inference(paramod,[status(thm)],[c_26,c_139]) ).
cnf(c_140,negated_conjecture,
~ defn_480,
inference(copy,[status(thm)],[c_504]) ).
cnf(c_145,negated_conjecture,
( op(e3,e2) != e1
| ~ defn_470 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_470]) ).
cnf(c_505,negated_conjecture,
( e1 != e1
| ~ defn_470 ),
inference(paramod,[status(thm)],[c_29,c_145]) ).
cnf(c_146,negated_conjecture,
~ defn_470,
inference(copy,[status(thm)],[c_505]) ).
cnf(c_149,negated_conjecture,
( op(e3,e3) != e0
| ~ defn_460 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_460]) ).
cnf(c_506,negated_conjecture,
( e0 != e0
| ~ defn_460 ),
inference(paramod,[status(thm)],[c_30,c_149]) ).
cnf(c_507,negated_conjecture,
( unit != e0
| ~ defn_460 ),
inference(paramod,[status(thm)],[c_32,c_506]) ).
cnf(c_508,negated_conjecture,
( unit != unit
| ~ defn_460 ),
inference(paramod,[status(thm)],[c_32,c_507]) ).
cnf(c_150,negated_conjecture,
~ defn_460,
inference(copy,[status(thm)],[c_508]) ).
cnf(c_154,negated_conjecture,
( op(e3,e3) != e0
| ~ defn_450 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_450]) ).
cnf(c_509,negated_conjecture,
( e0 != e0
| ~ defn_450 ),
inference(paramod,[status(thm)],[c_30,c_154]) ).
cnf(c_510,negated_conjecture,
( unit != e0
| ~ defn_450 ),
inference(paramod,[status(thm)],[c_32,c_509]) ).
cnf(c_511,negated_conjecture,
( unit != unit
| ~ defn_450 ),
inference(paramod,[status(thm)],[c_32,c_510]) ).
cnf(c_155,negated_conjecture,
~ defn_450,
inference(copy,[status(thm)],[c_511]) ).
cnf(c_160,negated_conjecture,
( op(e2,e2) != e3
| ~ defn_440 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_440]) ).
cnf(c_512,negated_conjecture,
( e3 != e3
| ~ defn_440 ),
inference(paramod,[status(thm)],[c_25,c_160]) ).
cnf(c_161,negated_conjecture,
~ defn_440,
inference(copy,[status(thm)],[c_512]) ).
cnf(c_165,negated_conjecture,
( op(e2,e2) != e3
| ~ defn_430 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_430]) ).
cnf(c_513,negated_conjecture,
( e3 != e3
| ~ defn_430 ),
inference(paramod,[status(thm)],[c_25,c_165]) ).
cnf(c_166,negated_conjecture,
~ defn_430,
inference(copy,[status(thm)],[c_513]) ).
cnf(c_173,negated_conjecture,
( op(e0,e2) != e2
| ~ defn_420 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_420]) ).
cnf(c_174,negated_conjecture,
( op(unit,e2) != e2
| ~ defn_420 ),
inference(paramod,[status(thm)],[c_32,c_173]) ).
cnf(c_179,negated_conjecture,
( op(e2,e0) != e2
| ~ defn_410 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_410]) ).
cnf(c_180,negated_conjecture,
( op(e2,unit) != e2
| ~ defn_410 ),
inference(paramod,[status(thm)],[c_32,c_179]) ).
cnf(c_181,negated_conjecture,
( op(e3,e2) != e1
| ~ defn_400 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_400]) ).
cnf(c_514,negated_conjecture,
( e1 != e1
| ~ defn_400 ),
inference(paramod,[status(thm)],[c_29,c_181]) ).
cnf(c_182,negated_conjecture,
~ defn_400,
inference(copy,[status(thm)],[c_514]) ).
cnf(c_186,negated_conjecture,
( op(e2,e3) != e1
| ~ defn_390 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_390]) ).
cnf(c_515,negated_conjecture,
( e1 != e1
| ~ defn_390 ),
inference(paramod,[status(thm)],[c_26,c_186]) ).
cnf(c_187,negated_conjecture,
~ defn_390,
inference(copy,[status(thm)],[c_515]) ).
cnf(c_195,negated_conjecture,
( op(e1,e2) != e0
| ~ defn_380 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_380]) ).
cnf(c_516,negated_conjecture,
( e0 != e0
| ~ defn_380 ),
inference(paramod,[status(thm)],[c_21,c_195]) ).
cnf(c_517,negated_conjecture,
( unit != e0
| ~ defn_380 ),
inference(paramod,[status(thm)],[c_32,c_516]) ).
cnf(c_518,negated_conjecture,
( unit != unit
| ~ defn_380 ),
inference(paramod,[status(thm)],[c_32,c_517]) ).
cnf(c_196,negated_conjecture,
~ defn_380,
inference(copy,[status(thm)],[c_518]) ).
cnf(c_202,negated_conjecture,
( op(e2,e1) != e0
| ~ defn_370 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_370]) ).
cnf(c_519,negated_conjecture,
( e0 != e0
| ~ defn_370 ),
inference(paramod,[status(thm)],[c_24,c_202]) ).
cnf(c_520,negated_conjecture,
( unit != e0
| ~ defn_370 ),
inference(paramod,[status(thm)],[c_32,c_519]) ).
cnf(c_521,negated_conjecture,
( unit != unit
| ~ defn_370 ),
inference(paramod,[status(thm)],[c_32,c_520]) ).
cnf(c_203,negated_conjecture,
~ defn_370,
inference(copy,[status(thm)],[c_521]) ).
cnf(c_208,negated_conjecture,
( op(e1,e1) != e3
| ~ defn_360 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_360]) ).
cnf(c_522,negated_conjecture,
( e3 != e3
| ~ defn_360 ),
inference(paramod,[status(thm)],[c_20,c_208]) ).
cnf(c_209,negated_conjecture,
~ defn_360,
inference(copy,[status(thm)],[c_522]) ).
cnf(c_214,negated_conjecture,
( op(e1,e1) != e3
| ~ defn_350 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_350]) ).
cnf(c_523,negated_conjecture,
( e3 != e3
| ~ defn_350 ),
inference(paramod,[status(thm)],[c_20,c_214]) ).
cnf(c_215,negated_conjecture,
~ defn_350,
inference(copy,[status(thm)],[c_523]) ).
cnf(c_217,negated_conjecture,
( op(e3,e1) != e2
| ~ defn_340 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_340]) ).
cnf(c_524,negated_conjecture,
( e2 != e2
| ~ defn_340 ),
inference(paramod,[status(thm)],[c_28,c_217]) ).
cnf(c_218,negated_conjecture,
~ defn_340,
inference(copy,[status(thm)],[c_524]) ).
cnf(c_222,negated_conjecture,
( op(e1,e3) != e2
| ~ defn_330 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_330]) ).
cnf(c_525,negated_conjecture,
( e2 != e2
| ~ defn_330 ),
inference(paramod,[status(thm)],[c_22,c_222]) ).
cnf(c_223,negated_conjecture,
~ defn_330,
inference(copy,[status(thm)],[c_525]) ).
cnf(c_231,negated_conjecture,
( op(e0,e1) != e1
| ~ defn_320 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_320]) ).
cnf(c_232,negated_conjecture,
( op(unit,e1) != e1
| ~ defn_320 ),
inference(paramod,[status(thm)],[c_32,c_231]) ).
cnf(c_237,negated_conjecture,
( op(e1,e0) != e1
| ~ defn_310 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_310]) ).
cnf(c_238,negated_conjecture,
( op(e1,unit) != e1
| ~ defn_310 ),
inference(paramod,[status(thm)],[c_32,c_237]) ).
cnf(c_241,negated_conjecture,
( op(e2,e1) != e0
| ~ defn_300 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_300]) ).
cnf(c_526,negated_conjecture,
( e0 != e0
| ~ defn_300 ),
inference(paramod,[status(thm)],[c_24,c_241]) ).
cnf(c_527,negated_conjecture,
( unit != e0
| ~ defn_300 ),
inference(paramod,[status(thm)],[c_32,c_526]) ).
cnf(c_528,negated_conjecture,
( unit != unit
| ~ defn_300 ),
inference(paramod,[status(thm)],[c_32,c_527]) ).
cnf(c_242,negated_conjecture,
~ defn_300,
inference(copy,[status(thm)],[c_528]) ).
cnf(c_247,negated_conjecture,
( op(e1,e2) != e0
| ~ defn_290 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_290]) ).
cnf(c_529,negated_conjecture,
( e0 != e0
| ~ defn_290 ),
inference(paramod,[status(thm)],[c_21,c_247]) ).
cnf(c_530,negated_conjecture,
( unit != e0
| ~ defn_290 ),
inference(paramod,[status(thm)],[c_32,c_529]) ).
cnf(c_531,negated_conjecture,
( unit != unit
| ~ defn_290 ),
inference(paramod,[status(thm)],[c_32,c_530]) ).
cnf(c_248,negated_conjecture,
~ defn_290,
inference(copy,[status(thm)],[c_531]) ).
cnf(c_251,negated_conjecture,
( op(e3,e0) != e3
| ~ defn_280 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_280]) ).
cnf(c_252,negated_conjecture,
( op(e3,unit) != e3
| ~ defn_280 ),
inference(paramod,[status(thm)],[c_32,c_251]) ).
cnf(c_259,negated_conjecture,
( op(e0,e3) != e3
| ~ defn_270 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_270]) ).
cnf(c_260,negated_conjecture,
( op(unit,e3) != e3
| ~ defn_270 ),
inference(paramod,[status(thm)],[c_32,c_259]) ).
cnf(c_269,negated_conjecture,
( op(e2,e0) != e2
| ~ defn_260 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_260]) ).
cnf(c_270,negated_conjecture,
( op(e2,unit) != e2
| ~ defn_260 ),
inference(paramod,[status(thm)],[c_32,c_269]) ).
cnf(c_277,negated_conjecture,
( op(e0,e2) != e2
| ~ defn_250 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_250]) ).
cnf(c_278,negated_conjecture,
( op(unit,e2) != e2
| ~ defn_250 ),
inference(paramod,[status(thm)],[c_32,c_277]) ).
cnf(c_287,negated_conjecture,
( op(e1,e0) != e1
| ~ defn_240 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_240]) ).
cnf(c_288,negated_conjecture,
( op(e1,unit) != e1
| ~ defn_240 ),
inference(paramod,[status(thm)],[c_32,c_287]) ).
cnf(c_295,negated_conjecture,
( op(e0,e1) != e1
| ~ defn_230 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_230]) ).
cnf(c_296,negated_conjecture,
( op(unit,e1) != e1
| ~ defn_230 ),
inference(paramod,[status(thm)],[c_32,c_295]) ).
cnf(c_305,negated_conjecture,
( op(e0,e0) != e0
| ~ defn_220 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_220]) ).
cnf(c_532,negated_conjecture,
( op(unit,e0) != e0
| ~ defn_220 ),
inference(paramod,[status(thm)],[c_32,c_305]) ).
cnf(c_533,negated_conjecture,
( op(unit,unit) != e0
| ~ defn_220 ),
inference(paramod,[status(thm)],[c_32,c_532]) ).
cnf(c_306,negated_conjecture,
( op(unit,unit) != unit
| ~ defn_220 ),
inference(paramod,[status(thm)],[c_32,c_533]) ).
cnf(c_313,negated_conjecture,
( op(e0,e0) != e0
| ~ defn_210 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_210]) ).
cnf(c_534,negated_conjecture,
( op(unit,e0) != e0
| ~ defn_210 ),
inference(paramod,[status(thm)],[c_32,c_313]) ).
cnf(c_535,negated_conjecture,
( op(unit,unit) != e0
| ~ defn_210 ),
inference(paramod,[status(thm)],[c_32,c_534]) ).
cnf(c_314,negated_conjecture,
( op(unit,unit) != unit
| ~ defn_210 ),
inference(paramod,[status(thm)],[c_32,c_535]) ).
cnf(c_320,negated_conjecture,
( unit != e0
| ~ defn_200 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_200]) ).
cnf(c_536,negated_conjecture,
( unit != unit
| ~ defn_200 ),
inference(paramod,[status(thm)],[c_32,c_320]) ).
cnf(c_321,negated_conjecture,
~ defn_200,
inference(copy,[status(thm)],[c_536]) ).
cnf(c_328,negated_conjecture,
( op(e3,e3) != e0
| ~ defn_190 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_190]) ).
cnf(c_537,negated_conjecture,
( e0 != e0
| ~ defn_190 ),
inference(paramod,[status(thm)],[c_30,c_328]) ).
cnf(c_538,negated_conjecture,
( unit != e0
| ~ defn_190 ),
inference(paramod,[status(thm)],[c_32,c_537]) ).
cnf(c_539,negated_conjecture,
( unit != unit
| ~ defn_190 ),
inference(paramod,[status(thm)],[c_32,c_538]) ).
cnf(c_329,negated_conjecture,
~ defn_190,
inference(copy,[status(thm)],[c_539]) ).
cnf(c_332,negated_conjecture,
( op(e3,e2) != e1
| ~ defn_180 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_180]) ).
cnf(c_540,negated_conjecture,
( e1 != e1
| ~ defn_180 ),
inference(paramod,[status(thm)],[c_29,c_332]) ).
cnf(c_333,negated_conjecture,
~ defn_180,
inference(copy,[status(thm)],[c_540]) ).
cnf(c_336,negated_conjecture,
( op(e3,e1) != e2
| ~ defn_170 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_170]) ).
cnf(c_541,negated_conjecture,
( e2 != e2
| ~ defn_170 ),
inference(paramod,[status(thm)],[c_28,c_336]) ).
cnf(c_337,negated_conjecture,
~ defn_170,
inference(copy,[status(thm)],[c_541]) ).
cnf(c_340,negated_conjecture,
( op(e3,e0) != e3
| ~ defn_160 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_160]) ).
cnf(c_341,negated_conjecture,
( op(e3,unit) != e3
| ~ defn_160 ),
inference(paramod,[status(thm)],[c_32,c_340]) ).
cnf(c_350,negated_conjecture,
( op(e2,e3) != e1
| ~ defn_150 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_150]) ).
cnf(c_542,negated_conjecture,
( e1 != e1
| ~ defn_150 ),
inference(paramod,[status(thm)],[c_26,c_350]) ).
cnf(c_351,negated_conjecture,
~ defn_150,
inference(copy,[status(thm)],[c_542]) ).
cnf(c_353,negated_conjecture,
( op(e2,e2) != e3
| ~ defn_140 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_140]) ).
cnf(c_543,negated_conjecture,
( e3 != e3
| ~ defn_140 ),
inference(paramod,[status(thm)],[c_25,c_353]) ).
cnf(c_354,negated_conjecture,
~ defn_140,
inference(copy,[status(thm)],[c_543]) ).
cnf(c_364,negated_conjecture,
( op(e2,e1) != e0
| ~ defn_130 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_130]) ).
cnf(c_544,negated_conjecture,
( e0 != e0
| ~ defn_130 ),
inference(paramod,[status(thm)],[c_24,c_364]) ).
cnf(c_545,negated_conjecture,
( unit != e0
| ~ defn_130 ),
inference(paramod,[status(thm)],[c_32,c_544]) ).
cnf(c_546,negated_conjecture,
( unit != unit
| ~ defn_130 ),
inference(paramod,[status(thm)],[c_32,c_545]) ).
cnf(c_365,negated_conjecture,
~ defn_130,
inference(copy,[status(thm)],[c_546]) ).
cnf(c_368,negated_conjecture,
( op(e2,e0) != e2
| ~ defn_120 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_120]) ).
cnf(c_369,negated_conjecture,
( op(e2,unit) != e2
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_32,c_368]) ).
cnf(c_375,negated_conjecture,
( op(e1,e3) != e2
| ~ defn_110 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_110]) ).
cnf(c_547,negated_conjecture,
( e2 != e2
| ~ defn_110 ),
inference(paramod,[status(thm)],[c_22,c_375]) ).
cnf(c_376,negated_conjecture,
~ defn_110,
inference(copy,[status(thm)],[c_547]) ).
cnf(c_385,negated_conjecture,
( op(e1,e2) != e0
| ~ defn_100 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_100]) ).
cnf(c_548,negated_conjecture,
( e0 != e0
| ~ defn_100 ),
inference(paramod,[status(thm)],[c_21,c_385]) ).
cnf(c_549,negated_conjecture,
( unit != e0
| ~ defn_100 ),
inference(paramod,[status(thm)],[c_32,c_548]) ).
cnf(c_550,negated_conjecture,
( unit != unit
| ~ defn_100 ),
inference(paramod,[status(thm)],[c_32,c_549]) ).
cnf(c_386,negated_conjecture,
~ defn_100,
inference(copy,[status(thm)],[c_550]) ).
cnf(c_387,negated_conjecture,
( op(e1,e1) != e3
| ~ defn_90 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_90]) ).
cnf(c_551,negated_conjecture,
( e3 != e3
| ~ defn_90 ),
inference(paramod,[status(thm)],[c_20,c_387]) ).
cnf(c_388,negated_conjecture,
~ defn_90,
inference(copy,[status(thm)],[c_551]) ).
cnf(c_396,negated_conjecture,
( op(e1,e0) != e1
| ~ defn_80 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_80]) ).
cnf(c_397,negated_conjecture,
( op(e1,unit) != e1
| ~ defn_80 ),
inference(paramod,[status(thm)],[c_32,c_396]) ).
cnf(c_400,negated_conjecture,
( op(e0,e3) != e3
| ~ defn_70 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_70]) ).
cnf(c_401,negated_conjecture,
( op(unit,e3) != e3
| ~ defn_70 ),
inference(paramod,[status(thm)],[c_32,c_400]) ).
cnf(c_410,negated_conjecture,
( op(e0,e2) != e2
| ~ defn_60 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_60]) ).
cnf(c_411,negated_conjecture,
( op(unit,e2) != e2
| ~ defn_60 ),
inference(paramod,[status(thm)],[c_32,c_410]) ).
cnf(c_420,negated_conjecture,
( op(e0,e1) != e1
| ~ defn_50 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_50]) ).
cnf(c_421,negated_conjecture,
( op(unit,e1) != e1
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_32,c_420]) ).
cnf(c_430,negated_conjecture,
( op(e0,e0) != e0
| ~ defn_40 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_40]) ).
cnf(c_552,negated_conjecture,
( op(unit,e0) != e0
| ~ defn_40 ),
inference(paramod,[status(thm)],[c_32,c_430]) ).
cnf(c_553,negated_conjecture,
( op(unit,unit) != e0
| ~ defn_40 ),
inference(paramod,[status(thm)],[c_32,c_552]) ).
cnf(c_431,negated_conjecture,
( op(unit,unit) != unit
| ~ defn_40 ),
inference(paramod,[status(thm)],[c_32,c_553]) ).
cnf(c_436,negated_conjecture,
( op(e0,e0) = e3
| ~ defn_30 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_30]) ).
cnf(c_554,negated_conjecture,
( op(unit,e0) = e3
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_32,c_436]) ).
cnf(c_437,negated_conjecture,
( op(unit,unit) = e3
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_32,c_554]) ).
cnf(c_440,negated_conjecture,
( op(e2,e2) = e2
| ~ defn_20 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_20]) ).
cnf(c_555,negated_conjecture,
( e3 = e2
| ~ defn_20 ),
inference(paramod,[status(thm)],[c_25,c_440]) ).
cnf(c_556,negated_conjecture,
( e2 = e3
| ~ defn_20 ),
inference(copy,[status(thm)],[c_555]) ).
cnf(c_441,negated_conjecture,
~ defn_20,
inference(resolve,[status(thm)],[c_14,c_556]) ).
cnf(c_446,negated_conjecture,
( op(e2,e2) = e1
| ~ defn_10 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_10]) ).
cnf(c_557,negated_conjecture,
( e3 = e1
| ~ defn_10 ),
inference(paramod,[status(thm)],[c_25,c_446]) ).
cnf(c_558,negated_conjecture,
( e1 = e3
| ~ defn_10 ),
inference(copy,[status(thm)],[c_557]) ).
cnf(c_447,negated_conjecture,
~ defn_10,
inference(resolve,[status(thm)],[c_12,c_558]) ).
cnf(c_451,negated_conjecture,
( op(e2,e2) = e0
| ~ defn_00 ),
inference(clausify,[status(thm)],[co1_neg,def_defn_00]) ).
cnf(c_559,negated_conjecture,
( e3 = e0
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_25,c_451]) ).
cnf(c_560,negated_conjecture,
( e3 = unit
| ~ defn_00 ),
inference(paramod,[status(thm)],[c_32,c_559]) ).
cnf(c_452,negated_conjecture,
( unit = e3
| ~ defn_00 ),
inference(copy,[status(thm)],[c_560]) ).
cnf(c_457,plain,
op(e3,unit) = e3,
inference(paramod,[status(thm)],[c_32,c_27]) ).
cnf(c_459,plain,
op(e2,unit) = e2,
inference(paramod,[status(thm)],[c_32,c_23]) ).
cnf(c_461,plain,
op(e1,unit) = e1,
inference(paramod,[status(thm)],[c_32,c_19]) ).
cnf(c_462,plain,
op(unit,e3) = e3,
inference(paramod,[status(thm)],[c_32,c_18]) ).
cnf(c_463,plain,
op(unit,e2) = e2,
inference(paramod,[status(thm)],[c_32,c_17]) ).
cnf(c_464,plain,
op(unit,e1) = e1,
inference(paramod,[status(thm)],[c_32,c_16]) ).
cnf(c_561,plain,
op(unit,e0) = e0,
inference(paramod,[status(thm)],[c_32,c_15]) ).
cnf(c_562,plain,
op(unit,unit) = e0,
inference(paramod,[status(thm)],[c_32,c_561]) ).
cnf(c_465,plain,
op(unit,unit) = unit,
inference(paramod,[status(thm)],[c_32,c_562]) ).
cnf(c_466,plain,
unit != e3,
inference(paramod,[status(thm)],[c_32,c_8]) ).
cnf(c_563,negated_conjecture,
( 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
| 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_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(paramod,[status(thm)],[c_465,c_77]) ).
cnf(c_564,negated_conjecture,
( 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
| 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_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(paramod,[status(thm)],[c_464,c_563]) ).
cnf(c_565,negated_conjecture,
( 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
| op(e3,unit) != e3
| op(unit,e3) != e3
| op(e2,unit) != e2
| op(unit,e2) != e2
| e1 != e1
| e1 != e1
| unit != unit
| 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(paramod,[status(thm)],[c_461,c_564]) ).
cnf(c_566,negated_conjecture,
( 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
| op(e3,unit) != e3
| op(unit,e3) != e3
| op(e2,unit) != e2
| e2 != e2
| e1 != e1
| e1 != e1
| unit != unit
| 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(paramod,[status(thm)],[c_463,c_565]) ).
cnf(c_567,negated_conjecture,
( 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
| op(e3,unit) != e3
| op(unit,e3) != e3
| e2 != e2
| e2 != e2
| e1 != e1
| e1 != e1
| unit != unit
| 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(paramod,[status(thm)],[c_459,c_566]) ).
cnf(c_568,negated_conjecture,
( 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
| op(e3,unit) != e3
| e3 != e3
| e2 != e2
| e2 != e2
| e1 != e1
| e1 != e1
| unit != unit
| 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(paramod,[status(thm)],[c_462,c_567]) ).
cnf(c_569,negated_conjecture,
( 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
| e3 != e3
| e3 != e3
| e2 != e2
| e2 != e2
| e1 != e1
| e1 != e1
| unit != unit
| 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(paramod,[status(thm)],[c_457,c_568]) ).
cnf(c_570,negated_conjecture,
( 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
| e3 != e3
| e3 != e3
| e2 != e2
| e2 != e2
| e1 != e1
| e1 != e1
| 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(copy,[status(thm)],[c_569]) ).
cnf(c_571,negated_conjecture,
( 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
| e3 != e3
| e3 != e3
| e2 != e2
| e2 != e2
| e1 != e1
| 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(copy,[status(thm)],[c_570]) ).
cnf(c_572,negated_conjecture,
( 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
| e3 != e3
| e3 != e3
| e2 != e2
| e2 != e2
| 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(copy,[status(thm)],[c_571]) ).
cnf(c_573,negated_conjecture,
( 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
| e3 != e3
| e3 != e3
| e2 != e2
| 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(copy,[status(thm)],[c_572]) ).
cnf(c_574,negated_conjecture,
( 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
| e3 != e3
| e3 != e3
| 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(copy,[status(thm)],[c_573]) ).
cnf(c_575,negated_conjecture,
( 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
| e3 != e3
| 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(copy,[status(thm)],[c_574]) ).
cnf(c_576,negated_conjecture,
( 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(copy,[status(thm)],[c_575]) ).
cnf(c_577,negated_conjecture,
( 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_00 ),
inference(resolve,[status(thm)],[c_447,c_576]) ).
cnf(c_578,negated_conjecture,
( 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_00 ),
inference(resolve,[status(thm)],[c_441,c_577]) ).
cnf(c_579,negated_conjecture,
( 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_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_388,c_578]) ).
cnf(c_580,negated_conjecture,
( 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_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_386,c_579]) ).
cnf(c_581,negated_conjecture,
( 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_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_376,c_580]) ).
cnf(c_582,negated_conjecture,
( 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_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_365,c_581]) ).
cnf(c_583,negated_conjecture,
( 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_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_354,c_582]) ).
cnf(c_584,negated_conjecture,
( 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_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_351,c_583]) ).
cnf(c_585,negated_conjecture,
( 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_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_337,c_584]) ).
cnf(c_586,negated_conjecture,
( 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_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_333,c_585]) ).
cnf(c_587,negated_conjecture,
( 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_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_329,c_586]) ).
cnf(c_588,negated_conjecture,
( 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_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_321,c_587]) ).
cnf(c_589,negated_conjecture,
( 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_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_248,c_588]) ).
cnf(c_590,negated_conjecture,
( 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_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_242,c_589]) ).
cnf(c_591,negated_conjecture,
( 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_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_223,c_590]) ).
cnf(c_592,negated_conjecture,
( 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_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_218,c_591]) ).
cnf(c_593,negated_conjecture,
( 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_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_215,c_592]) ).
cnf(c_594,negated_conjecture,
( 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_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_209,c_593]) ).
cnf(c_595,negated_conjecture,
( defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_380
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_203,c_594]) ).
cnf(c_596,negated_conjecture,
( defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_390
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_196,c_595]) ).
cnf(c_597,negated_conjecture,
( defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_400
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_187,c_596]) ).
cnf(c_598,negated_conjecture,
( defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_430
| defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_182,c_597]) ).
cnf(c_599,negated_conjecture,
( defn_480
| defn_470
| defn_460
| defn_450
| defn_440
| defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_166,c_598]) ).
cnf(c_600,negated_conjecture,
( defn_480
| defn_470
| defn_460
| defn_450
| defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_161,c_599]) ).
cnf(c_601,negated_conjecture,
( defn_480
| defn_470
| defn_460
| defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_155,c_600]) ).
cnf(c_602,negated_conjecture,
( defn_480
| defn_470
| defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_150,c_601]) ).
cnf(c_603,negated_conjecture,
( defn_480
| defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_146,c_602]) ).
cnf(c_469,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30
| defn_00 ),
inference(resolve,[status(thm)],[c_140,c_603]) ).
cnf(c_604,negated_conjecture,
( e3 != e3
| ~ defn_160 ),
inference(paramod,[status(thm)],[c_457,c_341]) ).
cnf(c_470,negated_conjecture,
~ defn_160,
inference(copy,[status(thm)],[c_604]) ).
cnf(c_605,negated_conjecture,
( e3 != e3
| ~ defn_280 ),
inference(paramod,[status(thm)],[c_457,c_252]) ).
cnf(c_471,negated_conjecture,
~ defn_280,
inference(copy,[status(thm)],[c_605]) ).
cnf(c_606,negated_conjecture,
( e2 != e2
| ~ defn_120 ),
inference(paramod,[status(thm)],[c_459,c_369]) ).
cnf(c_472,negated_conjecture,
~ defn_120,
inference(copy,[status(thm)],[c_606]) ).
cnf(c_607,negated_conjecture,
( e2 != e2
| ~ defn_260 ),
inference(paramod,[status(thm)],[c_459,c_270]) ).
cnf(c_473,negated_conjecture,
~ defn_260,
inference(copy,[status(thm)],[c_607]) ).
cnf(c_608,negated_conjecture,
( e2 != e2
| ~ defn_410 ),
inference(paramod,[status(thm)],[c_459,c_180]) ).
cnf(c_474,negated_conjecture,
~ defn_410,
inference(copy,[status(thm)],[c_608]) ).
cnf(c_609,negated_conjecture,
( e1 != e1
| ~ defn_80 ),
inference(paramod,[status(thm)],[c_461,c_397]) ).
cnf(c_475,negated_conjecture,
~ defn_80,
inference(copy,[status(thm)],[c_609]) ).
cnf(c_610,negated_conjecture,
( e1 != e1
| ~ defn_240 ),
inference(paramod,[status(thm)],[c_461,c_288]) ).
cnf(c_476,negated_conjecture,
~ defn_240,
inference(copy,[status(thm)],[c_610]) ).
cnf(c_611,negated_conjecture,
( e1 != e1
| ~ defn_310 ),
inference(paramod,[status(thm)],[c_461,c_238]) ).
cnf(c_477,negated_conjecture,
~ defn_310,
inference(copy,[status(thm)],[c_611]) ).
cnf(c_612,negated_conjecture,
( e3 != e3
| ~ defn_70 ),
inference(paramod,[status(thm)],[c_462,c_401]) ).
cnf(c_478,negated_conjecture,
~ defn_70,
inference(copy,[status(thm)],[c_612]) ).
cnf(c_613,negated_conjecture,
( e3 != e3
| ~ defn_270 ),
inference(paramod,[status(thm)],[c_462,c_260]) ).
cnf(c_479,negated_conjecture,
~ defn_270,
inference(copy,[status(thm)],[c_613]) ).
cnf(c_614,negated_conjecture,
( e2 != e2
| ~ defn_60 ),
inference(paramod,[status(thm)],[c_463,c_411]) ).
cnf(c_480,negated_conjecture,
~ defn_60,
inference(copy,[status(thm)],[c_614]) ).
cnf(c_615,negated_conjecture,
( e2 != e2
| ~ defn_250 ),
inference(paramod,[status(thm)],[c_463,c_278]) ).
cnf(c_481,negated_conjecture,
~ defn_250,
inference(copy,[status(thm)],[c_615]) ).
cnf(c_616,negated_conjecture,
( e2 != e2
| ~ defn_420 ),
inference(paramod,[status(thm)],[c_463,c_174]) ).
cnf(c_482,negated_conjecture,
~ defn_420,
inference(copy,[status(thm)],[c_616]) ).
cnf(c_617,negated_conjecture,
( e1 != e1
| ~ defn_50 ),
inference(paramod,[status(thm)],[c_464,c_421]) ).
cnf(c_483,negated_conjecture,
~ defn_50,
inference(copy,[status(thm)],[c_617]) ).
cnf(c_618,negated_conjecture,
( e1 != e1
| ~ defn_230 ),
inference(paramod,[status(thm)],[c_464,c_296]) ).
cnf(c_484,negated_conjecture,
~ defn_230,
inference(copy,[status(thm)],[c_618]) ).
cnf(c_619,negated_conjecture,
( e1 != e1
| ~ defn_320 ),
inference(paramod,[status(thm)],[c_464,c_232]) ).
cnf(c_485,negated_conjecture,
~ defn_320,
inference(copy,[status(thm)],[c_619]) ).
cnf(c_620,negated_conjecture,
( unit = e3
| ~ defn_30 ),
inference(paramod,[status(thm)],[c_465,c_437]) ).
cnf(c_486,negated_conjecture,
~ defn_30,
inference(resolve,[status(thm)],[c_466,c_620]) ).
cnf(c_621,negated_conjecture,
( unit != unit
| ~ defn_40 ),
inference(paramod,[status(thm)],[c_465,c_431]) ).
cnf(c_487,negated_conjecture,
~ defn_40,
inference(copy,[status(thm)],[c_621]) ).
cnf(c_622,negated_conjecture,
( unit != unit
| ~ defn_210 ),
inference(paramod,[status(thm)],[c_465,c_314]) ).
cnf(c_488,negated_conjecture,
~ defn_210,
inference(copy,[status(thm)],[c_622]) ).
cnf(c_623,negated_conjecture,
( unit != unit
| ~ defn_220 ),
inference(paramod,[status(thm)],[c_465,c_306]) ).
cnf(c_489,negated_conjecture,
~ defn_220,
inference(copy,[status(thm)],[c_623]) ).
cnf(c_490,negated_conjecture,
~ defn_00,
inference(resolve,[status(thm)],[c_466,c_452]) ).
cnf(c_624,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40
| defn_30 ),
inference(resolve,[status(thm)],[c_490,c_469]) ).
cnf(c_625,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50
| defn_40 ),
inference(resolve,[status(thm)],[c_486,c_624]) ).
cnf(c_626,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60
| defn_50 ),
inference(resolve,[status(thm)],[c_487,c_625]) ).
cnf(c_627,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70
| defn_60 ),
inference(resolve,[status(thm)],[c_483,c_626]) ).
cnf(c_628,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80
| defn_70 ),
inference(resolve,[status(thm)],[c_480,c_627]) ).
cnf(c_629,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120
| defn_80 ),
inference(resolve,[status(thm)],[c_478,c_628]) ).
cnf(c_630,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160
| defn_120 ),
inference(resolve,[status(thm)],[c_475,c_629]) ).
cnf(c_631,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210
| defn_160 ),
inference(resolve,[status(thm)],[c_472,c_630]) ).
cnf(c_632,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220
| defn_210 ),
inference(resolve,[status(thm)],[c_470,c_631]) ).
cnf(c_633,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230
| defn_220 ),
inference(resolve,[status(thm)],[c_488,c_632]) ).
cnf(c_634,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240
| defn_230 ),
inference(resolve,[status(thm)],[c_489,c_633]) ).
cnf(c_635,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250
| defn_240 ),
inference(resolve,[status(thm)],[c_484,c_634]) ).
cnf(c_636,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260
| defn_250 ),
inference(resolve,[status(thm)],[c_476,c_635]) ).
cnf(c_637,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270
| defn_260 ),
inference(resolve,[status(thm)],[c_481,c_636]) ).
cnf(c_638,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280
| defn_270 ),
inference(resolve,[status(thm)],[c_473,c_637]) ).
cnf(c_639,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310
| defn_280 ),
inference(resolve,[status(thm)],[c_479,c_638]) ).
cnf(c_640,negated_conjecture,
( defn_420
| defn_410
| defn_320
| defn_310 ),
inference(resolve,[status(thm)],[c_471,c_639]) ).
cnf(c_641,negated_conjecture,
( defn_420
| defn_410
| defn_320 ),
inference(resolve,[status(thm)],[c_477,c_640]) ).
cnf(c_642,negated_conjecture,
( defn_420
| defn_410 ),
inference(resolve,[status(thm)],[c_485,c_641]) ).
cnf(c_643,negated_conjecture,
defn_420,
inference(resolve,[status(thm)],[c_474,c_642]) ).
cnf(c_491,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_482,c_643]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG044+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/0.37 % Computer : n006.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 21:01:25 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 2112859 was started by sandbox on n006,
% 0.09/0.37 % Sat Sep 26 21:01:25 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.95/1.26
% 0.95/1.26 % From the command line: assign(max_seconds, 300).
% 1.02/1.32
% 1.02/1.32 % SZS status Theorem for theBenchmark
% 1.02/1.32
% 1.02/1.32 % Proof 1 at 0.02 (+ 0.01) seconds.
% 1.02/1.32 % Length of proof is 158.
% 1.02/1.32 % Level of proof is 5.
% 1.02/1.32 % Maximum clause weight is 88.000.
% 1.02/1.32 % Given clauses 0.
% 1.02/1.32
% 1.02/1.32 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------