%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : ITP005_4 : TPTP v8.1.0. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Sun Jul 17 00:33:06 EDT 2022
% Result : Theorem 59.32s 59.56s
% Output : Refutation 59.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 8
% Syntax : Number of formulae : 12 ( 12 unt; 0 typ; 0 def)
% Number of atoms : 250 ( 11 equ)
% Maximal formula atoms : 1 ( 20 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of FOOLs : 238 ( 238 fml; 0 var)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 20 ( 18 usr; 11 prp; 0-2 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 28 ( 0 sgn 28 !; 0 ?; 28 :)
% Comments :
%------------------------------------------------------------------------------
tff(2272,axiom,
! [X: d,Y: d,Z: d,U: u] : ( s(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,Z)),c_2Epair_2ECURRY_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),Z),U))) = s(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,Z)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),Z),tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,Z))),c_2Epair_2ECURRY_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),Z),U))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP014_4.ax',arityeq1_2Ec_2Epair_2ECURRY_2E1_2Emono_2EA_27a_20mono_2EA_27b_20mono_2EA_27c) ).
tff(2285,axiom,
! [X: d,Y: d,Z: d,U: u] : ( s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),Z),c_2Epair_2EUNCURRY_2E1(s(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,Z)),U))) = s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),Z),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,Z)),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),Z)),c_2Epair_2EUNCURRY_2E0),s(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,Z)),U))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP014_4.ax',arityeq1_2Ec_2Epair_2EUNCURRY_2E1_2Emono_2EA_27a_20mono_2EA_27b_20mono_2EA_27c) ).
tff(2364,axiom,
! [X: d,Y: d,Z: d,U: u] : ( s(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,Z)),c_2Epair_2ECURRY_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),Z),c_2Epair_2EUNCURRY_2E1(s(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,Z)),U))))) = s(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,Z)),U) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP014_4.ax',thm_2Epair_2ECURRY__UNCURRY__THM) ).
tff(10475,axiom,
! [X: d,Y: d,Z: u] : ( s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),tyop_2Emin_2Ebool),c_2Eset__relation_2Erel__to__reln_2E1(s(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,tyop_2Emin_2Ebool)),Z))) = s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),tyop_2Emin_2Ebool)),c_2Eset__relation_2Erel__to__reln_2E0),s(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,tyop_2Emin_2Ebool)),Z))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq1_2Ec_2Eset__relation_2Erel__to__reln_2E1_2Emono_2EA_27a_20mono_2EA_27b) ).
tff(10476,axiom,
! [X: d,Y: d,Z: u] : ( s(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,tyop_2Emin_2Ebool)),c_2Eset__relation_2Ereln__to__rel_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),tyop_2Emin_2Ebool),Z))) = s(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,tyop_2Emin_2Ebool))),c_2Eset__relation_2Ereln__to__rel_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),tyop_2Emin_2Ebool),Z))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq1_2Ec_2Eset__relation_2Ereln__to__rel_2E1_2Emono_2EA_27a_20mono_2EA_27b) ).
tff(10874,axiom,
! [X: d,Y: d] : ( s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),tyop_2Emin_2Ebool)),c_2Eset__relation_2Erel__to__reln_2E0) = s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),tyop_2Emin_2Ebool)),c_2Epair_2EUNCURRY_2E0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eset__relation_2Erel__to__reln__IS__UNCURRY) ).
tff(10875,axiom,
! [X: d,Y: d] : ( s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,tyop_2Emin_2Ebool))),c_2Eset__relation_2Ereln__to__rel_2E0) = s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,tyop_2Emin_2Ebool))),c_2Epair_2ECURRY_2E0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eset__relation_2Ereln__to__rel__IS__CURRY) ).
tff(10876,negated_conjecture,
s(tyop_2Emin_2Efun('SKOLEMAAAV2312.d',tyop_2Emin_2Efun('SKOLEMAAAV2313.d',tyop_2Emin_2Ebool)),c_2Eset__relation_2Ereln__to__rel_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod('SKOLEMAAAV2312.d','SKOLEMAAAV2313.d'),tyop_2Emin_2Ebool),c_2Eset__relation_2Erel__to__reln_2E1(s(tyop_2Emin_2Efun('SKOLEMAAAV2312.d',tyop_2Emin_2Efun('SKOLEMAAAV2313.d',tyop_2Emin_2Ebool)),'SKOLEMAAAV2314.u'))))) != s(tyop_2Emin_2Efun('SKOLEMAAAV2312.d',tyop_2Emin_2Efun('SKOLEMAAAV2313.d',tyop_2Emin_2Ebool)),'SKOLEMAAAV2314.u'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eset__relation_2Erel__to__reln__inv) ).
tff(10877,plain,
! [X: d,Y: d,Z: u] : ( s(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,tyop_2Emin_2Ebool)),c_2Eset__relation_2Ereln__to__rel_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),tyop_2Emin_2Ebool),Z))) = s(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,tyop_2Emin_2Ebool)),c_2Epair_2ECURRY_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),tyop_2Emin_2Ebool),Z))) ),
inference('REWRITE',[status(thm)],[10476,2272,10875,theory(equality)]) ).
tff(10880,plain,
s(tyop_2Emin_2Efun('SKOLEMAAAV2312.d',tyop_2Emin_2Efun('SKOLEMAAAV2313.d',tyop_2Emin_2Ebool)),c_2Epair_2ECURRY_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod('SKOLEMAAAV2312.d','SKOLEMAAAV2313.d'),tyop_2Emin_2Ebool),c_2Eset__relation_2Erel__to__reln_2E1(s(tyop_2Emin_2Efun('SKOLEMAAAV2312.d',tyop_2Emin_2Efun('SKOLEMAAAV2313.d',tyop_2Emin_2Ebool)),'SKOLEMAAAV2314.u'))))) != s(tyop_2Emin_2Efun('SKOLEMAAAV2312.d',tyop_2Emin_2Efun('SKOLEMAAAV2313.d',tyop_2Emin_2Ebool)),'SKOLEMAAAV2314.u'),
inference('REWRITE',[status(thm)],[10876,10877,theory(equality)]) ).
tff(10881,plain,
! [X: d,Y: d,Z: u] : ( s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),tyop_2Emin_2Ebool),c_2Eset__relation_2Erel__to__reln_2E1(s(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,tyop_2Emin_2Ebool)),Z))) = s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X,Y),tyop_2Emin_2Ebool),c_2Epair_2EUNCURRY_2E1(s(tyop_2Emin_2Efun(X,tyop_2Emin_2Efun(Y,tyop_2Emin_2Ebool)),Z))) ),
inference('REWRITE',[status(thm)],[10475,2285,10874,theory(equality)]) ).
cnf(10882,plain,
$false,
inference('REWRITE',[status(thm)],[10880,2364,10881,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : ITP005_4 : TPTP v8.1.0. Bugfixed v7.5.0.
% 0.12/0.13 % Command : run-snark %s %d
% 0.13/0.35 % Computer : n022.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Fri Jun 3 11:40:51 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.20/0.46 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.47 *
% 0.20/0.47 *
% 0.20/0.48 #<PACKAGE "SNARK-USER">
% 0.20/0.48 *
% 0.20/0.48 SNARK-TPTP-OPTIONS
% 0.20/0.48 *
% 0.20/0.48 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.20/0.48 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.20/0.48 (USE-FACTORING :POS)
% 0.20/0.48 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.20/0.48 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.20/0.48 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.20/0.48 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.20/0.48 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.20/0.48 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.20/0.48 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.20/0.48 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.20/0.48 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.20/0.48 (DECLARE-TPTP-SYMBOLS2))
% 0.20/0.48 *
% 0.20/0.48 "."
% 0.20/0.48 *
% 0.20/0.48 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-03T11:40:52
% 0.20/0.48 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n022.cluster.edu at 2022-06-03T11:40:52
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29_29| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29_29| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Eind| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Eone_2Eone| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Enum_2Enum| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Enum_2Enum| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.74 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.74 WARNING:
% 2.54/2.74 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Enum_2Enum| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Enum_2Enum| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Enum_2Enum| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Eone_2Eone| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Enum_2Enum| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Enum_2Enum| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Enum_2Enum| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Enum_2Enum| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Enum_2Enum| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Enum_2Enum| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Enum_2Enum| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Enum_2Enum| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Eoption_2Eoption_28tyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Enum_2Enum| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Eone_2Eone| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Eoption_2Eoption_28tyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Enum_2Enum| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |u| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |d| has already been declared.
% 2.54/2.75 WARNING: Ignoring sort declaration; |du| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Ebool| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29| has already been declared.
% 2.54/2.75 WARNING:
% 2.54/2.75 Ignoring sort declaration; |mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29| has already been declared.
% 2.73/2.91 WARNING: In quantification, variable ?F0_2E0 is being rebound.
% 3.36/3.52 WARNING:
% 3.36/3.52 Cannot use equality or equivalence (= ?X.mono_2Etyop_2Eone_2Eone
% 3.36/3.52 mono_2Ec_2Eone_2Eone_2E0) as rewrite.
% 59.32/59.56
% 59.32/59.56
% 59.32/59.56 #||
% 59.32/59.56 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 59.32/59.56 % SZS output start Refutation
% See solution above
% 59.32/59.56 ||#
% 59.32/59.56
% 59.32/59.56 ; Summary of computation:
% 59.32/59.56 ; 15376 formulas have been input or derived (from 1 formulas).
% 59.32/59.56 ; 10882 (71%) were retained. Of these,
% 59.32/59.56 ; 5076 (47%) were simplified or subsumed later,
% 59.32/59.56 ; 5806 (53%) are still being kept.
% 59.32/59.56 ;
% 59.32/59.56 ; Run time in seconds excluding printing time:
% 59.32/59.56 ; 2.250 4% Read assertion file (1 call)
% 59.32/59.56 ; 0.246 0% Assert (6,578 calls)
% 59.32/59.56 ; 2.704 5% Process new row (10,352 calls)
% 59.32/59.56 ; 0.175 0% Condensing (5,675 calls)
% 59.32/59.56 ; 5.359 9% Forward subsumption (5,675 calls)
% 59.32/59.56 ; 1.337 2% Backward subsumption (4,355 calls)
% 59.32/59.56 ; 0.076 0% Clause clause subsumption (4,671 calls)
% 59.32/59.56 ; 1.908 3% Forward simplification (10,352 calls)
% 59.32/59.56 ; 0.332 1% Backward simplification (6,802 calls)
% 59.32/59.56 ; 44.570 75% Ordering (56,670 calls)
% 59.32/59.56 ; 0.001 0% Sortal reasoning (1,511 calls)
% 59.32/59.56 ; 0.006 0% Purity testing (1 call)
% 59.32/59.56 ; 0.105 0% Other
% 59.32/59.56 ; 59.069 Total
% 59.32/59.56 ; 59.076 Real time
% 59.32/59.56 ;
% 59.32/59.57 ; Term-hash-array has 44,102 terms in all.
% 59.32/59.57 ; Feature-vector-row-index has 3,690 entries (3,691 at peak, 4,355 added, 665 deleted).
% 59.32/59.57 ; Feature-vector-row-index has 81,640 nodes (81,680 at peak, 95,782 added, 14,142 deleted).
% 59.32/59.57 ; Retrieved 32,985 possibly forward subsuming rows in 5,675 calls.
% 59.32/59.57 ; Retrieved 17,751 possibly backward subsumed rows in 4,355 calls.
% 59.32/59.57 ; Path-index has 38,888 entries (38,929 at peak, 44,955 added, 6,067 deleted).
% 59.32/59.57 ; Path-index has 353,896 nodes (354,071 at peak, 372,613 added, 18,717 deleted).
% 59.32/59.57 ; Trie-index has 38,888 entries (38,929 at peak, 44,955 added, 6,067 deleted).
% 59.32/59.57 ; Trie-index has 382,282 nodes (382,811 at peak, 447,992 added, 65,710 deleted).
% 59.32/59.57 ; Retrieved 66,295 generalization terms in 150,858 calls.
% 59.32/59.57 ; Retrieved 7,215 instance terms in 3,543 calls.
% 59.32/59.57 ;
% 59.32/59.57 ; The agenda of backward simplifiable rows to process has 941 entries:
% 59.32/59.57 ; 941 with value 0
% 59.32/59.57 ; The agenda of input rows to give has 5805 entries:
% 59.32/59.57 ; 3 with value 3 5 with value 127 9 with value 269
% 59.32/59.57 ; 10 with value 4 20 with value 128 3 with value 271
% 59.32/59.57 ; 12 with value 5 8 with value 129 2 with value 273
% 59.32/59.57 ; 29 with value 6 8 with value 130 3 with value 274
% 59.32/59.57 ; 21 with value 7 13 with value 131 3 with value 275
% 59.32/59.57 ; 94 with value 8 18 with value 132 1 with value 276
% 59.32/59.57 ; 23 with value 9 6 with value 133 1 with value 277
% 59.32/59.57 ; 52 with value 10 9 with value 134 5 with value 279
% 59.32/59.57 ; 39 with value 11 11 with value 135 1 with value 281
% 59.32/59.57 ; 106 with value 12 16 with value 136 5 with value 282
% 59.32/59.57 ; 50 with value 13 10 with value 137 1 with value 284
% 59.32/59.57 ; 50 with value 14 20 with value 138 1 with value 286
% 59.32/59.57 ; 44 with value 15 9 with value 139 3 with value 290
% 59.32/59.57 ; 78 with value 16 11 with value 140 1 with value 291
% 59.32/59.57 ; 37 with value 17 3 with value 141 4 with value 292
% 59.32/59.57 ; 60 with value 18 9 with value 142 5 with value 293
% 59.32/59.57 ; 38 with value 19 1 with value 143 9 with value 295
% 59.32/59.57 ; 65 with value 20 14 with value 144 2 with value 300
% 59.32/59.57 ; 69 with value 21 7 with value 145 2 with value 303
% 59.32/59.57 ; 54 with value 22 7 with value 146 2 with value 305
% 59.32/59.57 ; 79 with value 23 30 with value 147 1 with value 308
% 59.32/59.57 ; 47 with value 24 9 with value 148 2 with value 317
% 59.32/59.57 ; 56 with value 25 42 with value 149 6 with value 318
% 59.32/59.57 ; 60 with value 26 5 with value 150 1 with value 320
% 59.32/59.57 ; 54 with value 27 10 with value 151 4 with value 321
% 59.32/59.57 ; 61 with value 28 6 with value 152 1 with value 323
% 59.32/59.57 ; 42 with value 29 4 with value 153 3 with value 324
% 59.32/59.57 ; 97 with value 30 30 with value 154 6 with value 325
% 59.32/59.57 ; 36 with value 31 5 with value 155 1 with value 326
% 59.32/59.57 ; 51 with value 32 6 with value 156 2 with value 327
% 59.32/59.57 ; 67 with value 33 8 with value 157 1 with value 331
% 59.32/59.57 ; 43 with value 34 18 with value 158 2 with value 332
% 59.32/59.57 ; 51 with value 35 3 with value 159 5 with value 333
% 59.32/59.57 ; 42 with value 36 11 with value 160 1 with value 336
% 59.32/59.57 ; 115 with value 37 9 with value 161 4 with value 337
% 59.32/59.57 ; 69 with value 38 13 with value 162 2 with value 338
% 59.32/59.57 ; 57 with value 39 5 with value 163 1 with value 340
% 59.32/59.57 ; 88 with value 40 8 with value 164 1 with value 341
% 59.32/59.57 ; 33 with value 41 8 with value 165 3 with value 342
% 59.32/59.57 ; 47 with value 42 12 with value 166 3 with value 345
% 59.32/59.57 ; 116 with value 43 5 with value 167 4 with value 349
% 59.32/59.57 ; 79 with value 44 7 with value 168 1 with value 350
% 59.32/59.57 ; 32 with value 45 2 with value 169 2 with value 354
% 59.32/59.57 ; 47 with value 46 8 with value 170 1 with value 355
% 59.32/59.57 ; 53 with value 47 3 with value 171 5 with value 356
% 59.32/59.57 ; 40 with value 48 7 with value 172 2 with value 364
% 59.32/59.57 ; 69 with value 49 12 with value 173 8 with value 365
% 59.32/59.57 ; 87 with value 50 9 with value 174 1 with value 372
% 59.32/59.57 ; 40 with value 51 8 with value 175 1 with value 373
% 59.32/59.57 ; 41 with value 52 15 with value 176 1 with value 375
% 59.32/59.57 ; 45 with value 53 5 with value 177 1 with value 376
% 59.32/59.57 ; 51 with value 54 17 with value 178 1 with value 381
% 59.32/59.57 ; 47 with value 55 8 with value 179 1 with value 382
% 59.32/59.57 ; 37 with value 56 6 with value 180 2 with value 384
% 59.32/59.57 ; 53 with value 57 1 with value 181 1 with value 385
% 59.32/59.57 ; 65 with value 58 2 with value 182 4 with value 388
% 59.32/59.57 ; 36 with value 59 7 with value 183 2 with value 392
% 59.32/59.57 ; 31 with value 60 7 with value 184 1 with value 399
% 59.32/59.57 ; 32 with value 61 2 with value 185 2 with value 400
% 59.32/59.57 ; 70 with value 62 10 with value 186 1 with value 402
% 59.32/59.57 ; 55 with value 63 12 with value 187 4 with value 403
% 59.32/59.57 ; 39 with value 64 6 with value 188 1 with value 405
% 59.32/59.57 ; 37 with value 65 5 with value 189 1 with value 413
% 59.32/59.57 ; 28 with value 66 1 with value 190 1 with value 420
% 59.32/59.57 ; 27 with value 67 2 with value 191 1 with value 421
% 59.32/59.57 ; 39 with value 68 4 with value 192 3 with value 422
% 59.32/59.57 ; 36 with value 69 4 with value 193 4 with value 425
% 59.32/59.57 ; 38 with value 70 4 with value 194 2 with value 426
% 59.32/59.57 ; 42 with value 71 15 with value 195 6 with value 427
% 59.32/59.57 ; 31 with value 72 2 with value 196 1 with value 428
% 59.32/59.57 ; 32 with value 73 4 with value 197 2 with value 430
% 59.32/59.57 ; 41 with value 74 5 with value 198 1 with value 437
% 59.32/59.57 ; 32 with value 75 6 with value 199 1 with value 439
% 59.32/59.57 ; 43 with value 76 6 with value 200 1 with value 441
% 59.32/59.57 ; 41 with value 77 4 with value 201 3 with value 445
% 59.32/59.57 ; 21 with value 78 4 with value 202 1 with value 446
% 59.32/59.57 ; 23 with value 79 4 with value 204 4 with value 448
% 59.32/59.57 ; 39 with value 80 1 with value 206 1 with value 451
% 59.32/59.57 ; 16 with value 81 1 with value 207 2 with value 452
% 59.32/59.57 ; 26 with value 82 4 with value 208 1 with value 459
% 59.32/59.57 ; 21 with value 83 6 with value 209 4 with value 460
% 59.32/59.57 ; 35 with value 84 4 with value 210 2 with value 462
% 59.32/59.57 ; 37 with value 85 5 with value 211 2 with value 465
% 59.32/59.57 ; 31 with value 86 1 with value 212 2 with value 470
% 59.32/59.57 ; 37 with value 87 5 with value 213 8 with value 471
% 59.32/59.57 ; 19 with value 88 5 with value 214 1 with value 476
% 59.32/59.57 ; 13 with value 89 5 with value 215 4 with value 483
% 59.32/59.57 ; 29 with value 90 4 with value 216 11 with value 494
% 59.32/59.57 ; 19 with value 91 3 with value 217 1 with value 496
% 59.32/59.57 ; 27 with value 92 6 with value 218 1 with value 499
% 59.32/59.57 ; 14 with value 93 3 with value 219 1 with value 500
% 59.32/59.57 ; 19 with value 94 4 with value 220 1 with value 506
% 59.32/59.57 ; 21 with value 95 6 with value 222 1 with value 520
% 59.32/59.57 ; 21 with value 96 5 with value 224 4 with value 524
% 59.32/59.57 ; 18 with value 97 7 with value 225 1 with value 540
% 59.32/59.57 ; 10 with value 98 6 with value 226 2 with value 545
% 59.32/59.57 ; 9 with value 99 3 with value 227 2 with value 557
% 59.32/59.57 ; 15 with value 100 6 with value 228 4 with value 562
% 59.32/59.57 ; 28 with value 101 1 with value 229 2 with value 565
% 59.32/59.57 ; 21 with value 102 8 with value 230 1 with value 574
% 59.32/59.57 ; 9 with value 103 4 with value 231 1 with value 575
% 59.32/59.57 ; 12 with value 104 1 with value 233 1 with value 579
% 59.32/59.57 ; 26 with value 105 2 with value 236 2 with value 585
% 59.32/59.57 ; 15 with value 106 3 with value 238 1 with value 589
% 59.32/59.57 ; 7 with value 107 15 with value 239 3 with value 593
% 59.32/59.57 ; 14 with value 108 1 with value 240 3 with value 608
% 59.32/59.57 ; 23 with value 109 1 with value 241 2 with value 609
% 59.32/59.57 ; 10 with value 110 1 with value 242 4 with value 611
% 59.32/59.57 ; 5 with value 111 2 with value 243 1 with value 618
% 59.32/59.57 ; 14 with value 112 2 with value 244 1 with value 633
% 59.32/59.57 ; 10 with value 113 2 with value 245 2 with value 634
% 59.32/59.57 ; 18 with value 114 1 with value 246 1 with value 649
% 59.32/59.57 ; 12 with value 115 6 with value 247 1 with value 653
% 59.32/59.57 ; 15 with value 116 4 with value 248 2 with value 664
% 59.32/59.57 ; 16 with value 117 9 with value 249 1 with value 1180
% 59.32/59.57 ; 14 with value 118 2 with value 250 1 with value 1195
% 59.32/59.57 ; 12 with value 119 7 with value 253 1 with value 1218
% 59.32/59.57 ; 30 with value 120 1 with value 257 1 with value 1258
% 59.32/59.57 ; 9 with value 121 2 with value 258 1 with value 1273
% 59.32/59.57 ; 11 with value 122 1 with value 260 1 with value 1277
% 59.32/59.57 ; 23 with value 123 7 with value 262 1 with value 1292
% 59.32/59.57 ; 6 with value 124 1 with value 264 1 with value 1296
% 59.32/59.57 ; 10 with value 125 1 with value 266 1 with value 1315
% 59.32/59.57 ; 16 with value 126 2 with value 268
% 59.32/59.57 Evaluation took:
% 59.32/59.57 59.086 seconds of real time
% 59.32/59.57 57.91973 seconds of user run time
% 59.32/59.57 1.162628 seconds of system run time
% 59.32/59.57 [Run times include 8.805 seconds GC run time.]
% 59.32/59.57 0 calls to %EVAL
% 59.32/59.57 0 page faults and
% 59.32/59.57 3,658,929,952 bytes consed.
% 59.32/59.57 :PROOF-FOUND
% 59.32/59.57 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-03T11:41:51
% 59.32/59.57 :PROOF-FOUND
% 59.32/59.57 *
%------------------------------------------------------------------------------