%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP003_1 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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 : Tue Sep 29 11:27:41 AM UTC 2026
% Result : Theorem 18.47s 4.31s
% Output : Refutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 50
% Syntax : Number of formulae : 278 ( 118 unt; 0 typ; 21 def)
% Number of atoms : 628 ( 223 equ)
% Maximal formula atoms : 30 ( 2 avg)
% Number of connectives : 584 ( 234 ~; 254 |; 62 &)
% ( 28 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of types : 14 ( 13 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 26 ( 24 usr; 12 prp; 0-3 aty)
% Number of functors : 149 ( 149 usr; 58 con; 0-4 aty)
% Number of variables : 221 ( 0 sgn 213 !; 8 ?; 221 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
u: $tType ).
tff(type_def_6,type,
d: $tType ).
tff(type_def_7,type,
du: $tType ).
tff(type_def_8,type,
mono_2Etyop_2Emin_2Ebool: $tType ).
tff(type_def_9,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: $tType ).
tff(type_def_10,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: $tType ).
tff(type_def_11,type,
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: $tType ).
tff(type_def_12,type,
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: $tType ).
tff(type_def_13,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29: $tType ).
tff(type_def_14,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29: $tType ).
tff(type_def_15,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29: $tType ).
tff(type_def_16,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29: $tType ).
tff(type_def_17,type,
mono_2Etyop_2Enum_2Enum: $tType ).
tff(func_def_0,type,
tyop_2Emin_2Ebool: d ).
tff(func_def_1,type,
tyop_2Emin_2Efun: ( d * d ) > d ).
tff(func_def_2,type,
tyop_2Enum_2Enum: d ).
tff(func_def_3,type,
s: ( d * u ) > du ).
tff(func_def_4,type,
app_2E2: ( du * du ) > u ).
tff(func_def_5,type,
combin_i_2E0: u ).
tff(func_def_6,type,
combin_k_2E0: u ).
tff(func_def_7,type,
combin_s_2E0: u ).
tff(func_def_8,type,
c_2Ebool_2E_21_2E0: u ).
tff(func_def_9,type,
c_2Ebool_2E_21_2E1: du > u ).
tff(func_def_10,type,
c_2Earithmetic_2E_2A_2E0: u ).
tff(func_def_11,type,
c_2Earithmetic_2E_2A_2E2: ( du * du ) > u ).
tff(func_def_12,type,
c_2Earithmetic_2E_2B_2E0: u ).
tff(func_def_13,type,
c_2Earithmetic_2E_2B_2E2: ( du * du ) > u ).
tff(func_def_14,type,
c_2Ebool_2E_2F_5C_2E0: u ).
tff(func_def_15,type,
c_2Ebool_2E_2F_5C_2E2: ( du * du ) > u ).
tff(func_def_16,type,
c_2Enum_2E0_2E0: u ).
tff(func_def_17,type,
c_2Eprim__rec_2E_3C_2E0: u ).
tff(func_def_18,type,
c_2Eprim__rec_2E_3C_2E2: ( du * du ) > u ).
tff(func_def_19,type,
c_2Emin_2E_3D_2E0: u ).
tff(func_def_20,type,
c_2Emin_2E_3D_2E2: ( du * du ) > u ).
tff(func_def_21,type,
c_2Emin_2E_3D_3D_3E_2E0: u ).
tff(func_def_22,type,
c_2Emin_2E_3D_3D_3E_2E2: ( du * du ) > u ).
tff(func_def_23,type,
c_2Ebool_2E_3F_2E0: u ).
tff(func_def_24,type,
c_2Ebool_2E_3F_2E1: du > u ).
tff(func_def_25,type,
c_2Earithmetic_2EBIT1_2E0: u ).
tff(func_def_26,type,
c_2Earithmetic_2EBIT1_2E1: du > u ).
tff(func_def_27,type,
c_2Earithmetic_2EBIT2_2E0: u ).
tff(func_def_28,type,
c_2Earithmetic_2EBIT2_2E1: du > u ).
tff(func_def_29,type,
c_2Ebool_2ECOND_2E0: u ).
tff(func_def_30,type,
c_2Ebool_2ECOND_2E3: ( du * du * du ) > u ).
tff(func_def_31,type,
c_2Earithmetic_2EEVEN_2E0: u ).
tff(func_def_32,type,
c_2Earithmetic_2EEVEN_2E1: du > u ).
tff(func_def_33,type,
c_2Ebool_2EF_2E0: u ).
tff(func_def_34,type,
c_2Earithmetic_2EMOD_2E0: u ).
tff(func_def_35,type,
c_2Earithmetic_2EMOD_2E2: ( du * du ) > u ).
tff(func_def_36,type,
c_2Earithmetic_2ENUMERAL_2E0: u ).
tff(func_def_37,type,
c_2Earithmetic_2ENUMERAL_2E1: du > u ).
tff(func_def_38,type,
c_2Earithmetic_2EODD_2E0: u ).
tff(func_def_39,type,
c_2Earithmetic_2EODD_2E1: du > u ).
tff(func_def_40,type,
c_2Enum_2ESUC_2E0: u ).
tff(func_def_41,type,
c_2Enum_2ESUC_2E1: du > u ).
tff(func_def_42,type,
c_2Ebool_2ET_2E0: u ).
tff(func_def_43,type,
c_2Earithmetic_2EZERO_2E0: u ).
tff(func_def_44,type,
c_2Ebool_2E_5C_2F_2E0: u ).
tff(func_def_45,type,
c_2Ebool_2E_5C_2F_2E2: ( du * du ) > u ).
tff(func_def_46,type,
c_2Ebool_2E_7E_2E0: u ).
tff(func_def_47,type,
c_2Ebool_2E_7E_2E1: du > u ).
tff(func_def_48,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool: ( mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_49,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: ( mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_50,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: ( 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 * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_51,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29: ( 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 * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 ).
tff(func_def_52,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool: ( mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 * mono_2Etyop_2Enum_2Enum ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_53,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29: ( mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29 * mono_2Etyop_2Enum_2Enum ) > mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_54,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29: ( mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 * mono_2Etyop_2Enum_2Enum ) > mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 ).
tff(func_def_55,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum: ( mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 * mono_2Etyop_2Enum_2Enum ) > mono_2Etyop_2Enum_2Enum ).
tff(func_def_56,type,
mono_2Ec_2Earithmetic_2E_2A_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 ).
tff(func_def_57,type,
mono_2Ec_2Earithmetic_2E_2A_2E2: ( mono_2Etyop_2Enum_2Enum * mono_2Etyop_2Enum_2Enum ) > mono_2Etyop_2Enum_2Enum ).
tff(func_def_58,type,
mono_2Ec_2Earithmetic_2E_2B_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 ).
tff(func_def_59,type,
mono_2Ec_2Earithmetic_2E_2B_2E2: ( mono_2Etyop_2Enum_2Enum * mono_2Etyop_2Enum_2Enum ) > mono_2Etyop_2Enum_2Enum ).
tff(func_def_60,type,
mono_2Ec_2Ebool_2E_2F_5C_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_61,type,
mono_2Ec_2Ebool_2E_2F_5C_2E2: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_62,type,
mono_2Ec_2Enum_2E0_2E0: mono_2Etyop_2Enum_2Enum ).
tff(func_def_63,type,
mono_2Ec_2Eprim__rec_2E_3C_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_64,type,
mono_2Ec_2Eprim__rec_2E_3C_2E2: ( mono_2Etyop_2Enum_2Enum * mono_2Etyop_2Enum_2Enum ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_65,type,
mono_2Ec_2Emin_2E_3D_3D_3E_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_66,type,
mono_2Ec_2Emin_2E_3D_3D_3E_2E2: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_67,type,
mono_2Ec_2Earithmetic_2EBIT1_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 ).
tff(func_def_68,type,
mono_2Ec_2Earithmetic_2EBIT1_2E1: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
tff(func_def_69,type,
mono_2Ec_2Earithmetic_2EBIT2_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 ).
tff(func_def_70,type,
mono_2Ec_2Earithmetic_2EBIT2_2E1: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
tff(func_def_71,type,
mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Emin_2Ebool: 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 ).
tff(func_def_72,type,
mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Emin_2Ebool: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_73,type,
mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Enum_2Enum: 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 ).
tff(func_def_74,type,
mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Enum_2Enum: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Enum_2Enum * mono_2Etyop_2Enum_2Enum ) > mono_2Etyop_2Enum_2Enum ).
tff(func_def_75,type,
mono_2Ec_2Earithmetic_2EEVEN_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_76,type,
mono_2Ec_2Earithmetic_2EEVEN_2E1: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_77,type,
mono_2Ec_2Ebool_2EF_2E0: mono_2Etyop_2Emin_2Ebool ).
tff(func_def_78,type,
mono_2Ec_2Earithmetic_2EMOD_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 ).
tff(func_def_79,type,
mono_2Ec_2Earithmetic_2EMOD_2E2: ( mono_2Etyop_2Enum_2Enum * mono_2Etyop_2Enum_2Enum ) > mono_2Etyop_2Enum_2Enum ).
tff(func_def_80,type,
mono_2Ec_2Earithmetic_2ENUMERAL_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 ).
tff(func_def_81,type,
mono_2Ec_2Earithmetic_2ENUMERAL_2E1: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
tff(func_def_82,type,
mono_2Ec_2Earithmetic_2EODD_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_83,type,
mono_2Ec_2Earithmetic_2EODD_2E1: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_84,type,
mono_2Ec_2Enum_2ESUC_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 ).
tff(func_def_85,type,
mono_2Ec_2Enum_2ESUC_2E1: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
tff(func_def_86,type,
mono_2Ec_2Ebool_2ET_2E0: mono_2Etyop_2Emin_2Ebool ).
tff(func_def_87,type,
mono_2Ec_2Earithmetic_2EZERO_2E0: mono_2Etyop_2Enum_2Enum ).
tff(func_def_88,type,
mono_2Ec_2Ebool_2E_5C_2F_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_89,type,
mono_2Ec_2Ebool_2E_5C_2F_2E2: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_90,type,
mono_2Ec_2Ebool_2E_7E_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_91,type,
mono_2Ec_2Ebool_2E_7E_2E1: mono_2Etyop_2Emin_2Ebool > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_92,type,
i_mono_2Etyop_2Emin_2Ebool: mono_2Etyop_2Emin_2Ebool > u ).
tff(func_def_93,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 > u ).
tff(func_def_94,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 > u ).
tff(func_def_95,type,
i_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: 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 > u ).
tff(func_def_96,type,
i_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: 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 > u ).
tff(func_def_97,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 > u ).
tff(func_def_98,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29 > u ).
tff(func_def_99,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 > u ).
tff(func_def_100,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 > u ).
tff(func_def_101,type,
i_mono_2Etyop_2Enum_2Enum: mono_2Etyop_2Enum_2Enum > u ).
tff(func_def_102,type,
j_mono_2Etyop_2Emin_2Ebool: du > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_103,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_104,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_105,type,
j_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: du > 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 ).
tff(func_def_106,type,
j_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: du > 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 ).
tff(func_def_107,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_108,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_109,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 ).
tff(func_def_110,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 ).
tff(func_def_111,type,
j_mono_2Etyop_2Enum_2Enum: du > mono_2Etyop_2Enum_2Enum ).
tff(func_def_112,type,
sK12: ( d * d * u * u ) > u ).
tff(func_def_113,type,
sK13: ( d * u ) > u ).
tff(func_def_114,type,
sK14: ( d * u ) > u ).
tff(func_def_115,type,
sK15: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
tff(func_def_116,type,
sK16: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
tff(func_def_117,type,
sK17: ( d * u ) > u ).
tff(func_def_118,type,
sK18: ( d * u ) > u ).
tff(func_def_119,type,
sK19: ( d * u * mono_2Etyop_2Emin_2Ebool ) > u ).
tff(func_def_120,type,
sK20: ( d * u ) > u ).
tff(func_def_121,type,
sK21: ( d * u * u ) > u ).
tff(func_def_122,type,
sK22: ( d * u ) > u ).
tff(func_def_123,type,
sK23: ( d * u ) > u ).
tff(func_def_124,type,
sK24: ( d * u ) > u ).
tff(func_def_125,type,
sK25: ( d * u * mono_2Etyop_2Emin_2Ebool ) > u ).
tff(func_def_126,type,
sK26: ( d * u ) > u ).
tff(func_def_127,type,
sK27: ( d * mono_2Etyop_2Emin_2Ebool * u ) > u ).
tff(func_def_128,type,
sK28: ( d * u * mono_2Etyop_2Emin_2Ebool ) > u ).
tff(func_def_129,type,
sK29: ( d * u ) > u ).
tff(func_def_130,type,
sK30: ( d * mono_2Etyop_2Emin_2Ebool * u ) > u ).
tff(func_def_131,type,
sK31: ( d * u ) > u ).
tff(func_def_132,type,
sK32: ( d * u ) > u ).
tff(func_def_133,type,
sK33: ( d * mono_2Etyop_2Emin_2Ebool * u ) > u ).
tff(func_def_134,type,
sK34: ( d * d * u * u ) > u ).
tff(func_def_135,type,
sK35: ( d * d * u * u ) > u ).
tff(func_def_136,type,
sK36: ( d * d * u ) > u ).
tff(func_def_137,type,
sK37: ( d * d * u ) > u ).
tff(func_def_138,type,
sK38: mono_2Etyop_2Enum_2Enum ).
tff(func_def_139,type,
sF39: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 ).
tff(func_def_140,type,
sF40: mono_2Etyop_2Enum_2Enum ).
tff(func_def_141,type,
sF41: mono_2Etyop_2Enum_2Enum ).
tff(func_def_142,type,
sF42: mono_2Etyop_2Enum_2Enum ).
tff(func_def_143,type,
sF43: mono_2Etyop_2Emin_2Ebool ).
tff(func_def_144,type,
sF44: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 ).
tff(func_def_145,type,
sF45: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 ).
tff(func_def_146,type,
sF46: mono_2Etyop_2Enum_2Enum ).
tff(func_def_147,type,
sF47: mono_2Etyop_2Enum_2Enum ).
tff(func_def_148,type,
sF48: mono_2Etyop_2Enum_2Enum ).
tff(pred_def_1,type,
p: mono_2Etyop_2Emin_2Ebool > $o ).
tff(pred_def_2,type,
sP0: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > $o ).
tff(pred_def_3,type,
sP1: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > $o ).
tff(pred_def_4,type,
sP2: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > $o ).
tff(pred_def_5,type,
sP3: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > $o ).
tff(pred_def_6,type,
sP4: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > $o ).
tff(pred_def_7,type,
sP5: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > $o ).
tff(pred_def_8,type,
sP6: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > $o ).
tff(pred_def_9,type,
sP7: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > $o ).
tff(pred_def_10,type,
sP8: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > $o ).
tff(pred_def_11,type,
sP9: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > $o ).
tff(pred_def_12,type,
sP10: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > $o ).
tff(pred_def_13,type,
sP11: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > $o ).
tff(f35,axiom,
! [X0: mono_2Etyop_2Enum_2Enum] : ( j_mono_2Etyop_2Enum_2Enum(s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(X0))) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Enum_2Enum) ).
tff(f37,axiom,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2E_2A_2E2(X0,X1) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq2_2Ec_2Earithmetic_2E_2A_2E2) ).
tff(f38,axiom,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2E_2B_2E2(X0,X1) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2B_2E0,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq2_2Ec_2Earithmetic_2E_2B_2E2) ).
tff(f40,axiom,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Eprim__rec_2E_3C_2E2(X0,X1) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq2_2Ec_2Eprim__rec_2E_3C_2E2) ).
tff(f44,axiom,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EBIT1_2E1(X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT1_2E0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq1_2Ec_2Earithmetic_2EBIT1_2E1) ).
tff(f45,axiom,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EBIT2_2E1(X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT2_2E0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq1_2Ec_2Earithmetic_2EBIT2_2E1) ).
tff(f50,axiom,
! [X0: mono_2Etyop_2Emin_2Ebool,X1: mono_2Etyop_2Enum_2Enum,X2: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Enum_2Enum(X0,X1,X2) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Enum_2Enum,X0),X1),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq3_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Enum_2Enum) ).
tff(f51,axiom,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EEVEN_2E1(X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq1_2Ec_2Earithmetic_2EEVEN_2E1) ).
tff(f52,axiom,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EMOD_2E2(X0,X1) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq2_2Ec_2Earithmetic_2EMOD_2E2) ).
tff(f53,axiom,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2ENUMERAL_2E1(X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq1_2Ec_2Earithmetic_2ENUMERAL_2E1) ).
tff(f54,axiom,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EODD_2E1(X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq1_2Ec_2Earithmetic_2EODD_2E1) ).
tff(f55,axiom,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Enum_2ESUC_2E1(X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq1_2Ec_2Enum_2ESUC_2E1) ).
tff(f69,axiom,
! [X0: mono_2Etyop_2Emin_2Ebool,X1: mono_2Etyop_2Enum_2Enum,X2: mono_2Etyop_2Enum_2Enum] : ( s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Enum_2Enum(X0,X1,X2))) = s(tyop_2Enum_2Enum,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(X0)),s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(X1)),s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(X2)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',monoeq_2Emono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Enum_2Enum) ).
tff(f70,axiom,
mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT1_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)) = mono_2Ec_2Enum_2ESUC_2E1(mono_2Ec_2Enum_2E0_2E0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Earithmetic_2EONE) ).
tff(f71,axiom,
mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)) = mono_2Ec_2Enum_2ESUC_2E1(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT1_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Earithmetic_2ETWO) ).
tff(f72,axiom,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2E_2B_2E2(X0,mono_2Ec_2Enum_2E0_2E0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Earithmetic_2EADD__0) ).
tff(f73,axiom,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Eprim__rec_2E_3C_2E2(mono_2Ec_2Enum_2ESUC_2E1(X0),mono_2Ec_2Enum_2ESUC_2E1(X1)) = mono_2Ec_2Eprim__rec_2E_3C_2E2(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Earithmetic_2ELESS__MONO__EQ) ).
tff(f74,axiom,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Enum_2ESUC_2E1(X0) = mono_2Ec_2Earithmetic_2E_2B_2E2(X0,mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT1_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Earithmetic_2EADD1) ).
tff(f75,axiom,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2E_2A_2E2(X0,X1) = mono_2Ec_2Earithmetic_2E_2A_2E2(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Earithmetic_2EMULT__COMM) ).
tff(f77,axiom,
! [X0: mono_2Etyop_2Enum_2Enum] :
( p(mono_2Ec_2Earithmetic_2EODD_2E1(X0))
<=> ~ p(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Earithmetic_2EODD__EVEN) ).
tff(f78,axiom,
! [X0: mono_2Etyop_2Enum_2Enum] :
( p(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0))
<=> ? [X1: mono_2Etyop_2Enum_2Enum] : ( X0 = mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Earithmetic_2EEVEN__EXISTS) ).
tff(f79,axiom,
! [X0: mono_2Etyop_2Enum_2Enum] :
( p(mono_2Ec_2Earithmetic_2EODD_2E1(X0))
<=> ? [X1: mono_2Etyop_2Enum_2Enum] : ( X0 = mono_2Ec_2Enum_2ESUC_2E1(mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Earithmetic_2EODD__EXISTS) ).
tff(f80,axiom,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum,X2: mono_2Etyop_2Enum_2Enum] :
( ? [X3: mono_2Etyop_2Enum_2Enum] :
( ( X1 = mono_2Ec_2Earithmetic_2E_2B_2E2(mono_2Ec_2Earithmetic_2E_2A_2E2(X3,X0),X2) )
& p(mono_2Ec_2Eprim__rec_2E_3C_2E2(X2,X0)) )
=> ( mono_2Ec_2Earithmetic_2EMOD_2E2(X1,X0) = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Earithmetic_2EMOD__UNIQUE) ).
tff(f81,axiom,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( X0 = mono_2Ec_2Ebool_2ET_2E0 )
| ( X0 = mono_2Ec_2Ebool_2EF_2E0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2EBOOL__CASES__AX) ).
tff(f90,axiom,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( ( p(mono_2Ec_2Ebool_2ET_2E0)
=> p(X0) )
<=> p(X0) )
& ( ( p(X0)
=> p(mono_2Ec_2Ebool_2ET_2E0) )
<=> p(mono_2Ec_2Ebool_2ET_2E0) )
& ( ( p(mono_2Ec_2Ebool_2EF_2E0)
=> p(X0) )
<=> p(mono_2Ec_2Ebool_2ET_2E0) )
& ( ( p(X0)
=> p(X0) )
<=> p(mono_2Ec_2Ebool_2ET_2E0) )
& ( ( p(X0)
=> p(mono_2Ec_2Ebool_2EF_2E0) )
<=> ~ p(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2EIMP__CLAUSES) ).
tff(f94,axiom,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( ( mono_2Ec_2Ebool_2ET_2E0 = X0 )
<=> p(X0) )
& ( ( X0 = mono_2Ec_2Ebool_2ET_2E0 )
<=> p(X0) )
& ( ( mono_2Ec_2Ebool_2EF_2E0 = X0 )
<=> ~ p(X0) )
& ( ( X0 = mono_2Ec_2Ebool_2EF_2E0 )
<=> ~ p(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2EEQ__CLAUSES) ).
tff(f95,axiom,
! [X0: d,X1: u,X2: u] :
( ( s(X0,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0)),s(X0,X1),s(X0,X2))) = s(X0,X1) )
& ( s(X0,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0)),s(X0,X1),s(X0,X2))) = s(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ECOND__CLAUSES) ).
tff(f111,axiom,
! [X0: mono_2Etyop_2Enum_2Enum] : p(mono_2Ec_2Eprim__rec_2E_3C_2E2(mono_2Ec_2Enum_2E0_2E0,mono_2Ec_2Enum_2ESUC_2E1(X0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eprim__rec_2ELESS__0) ).
tff(f127,conjecture,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EMOD_2E2(X0,mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0))) = mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0),mono_2Ec_2Enum_2E0_2E0,mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT1_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Earithmetic_2EMOD__2) ).
tff(f128,negated_conjecture,
~ ! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EMOD_2E2(X0,mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0))) = mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0),mono_2Ec_2Enum_2E0_2E0,mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT1_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0))) ),
inference(negated_conjecture,[status(cth)],[f127]) ).
tff(f133,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum,X2: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2EMOD_2E2(X1,X0) = X2 )
| ! [X3: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2B_2E2(mono_2Ec_2Earithmetic_2E_2A_2E2(X3,X0),X2) != X1 )
| ~ p(mono_2Ec_2Eprim__rec_2E_3C_2E2(X2,X0)) ) ),
inference(ennf_transformation,[],[f80]) ).
tff(f140,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( ( p(X0)
| ~ p(mono_2Ec_2Ebool_2ET_2E0) )
<=> p(X0) )
& ( ( p(mono_2Ec_2Ebool_2ET_2E0)
| ~ p(X0) )
<=> p(mono_2Ec_2Ebool_2ET_2E0) )
& ( ( p(X0)
| ~ p(mono_2Ec_2Ebool_2EF_2E0) )
<=> p(mono_2Ec_2Ebool_2ET_2E0) )
& ( ( p(X0)
| ~ p(X0) )
<=> p(mono_2Ec_2Ebool_2ET_2E0) )
& ( ( p(mono_2Ec_2Ebool_2EF_2E0)
| ~ p(X0) )
<=> ~ p(X0) ) ),
inference(ennf_transformation,[],[f90]) ).
tff(f161,plain,
? [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EMOD_2E2(X0,mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0))) != mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0),mono_2Ec_2Enum_2E0_2E0,mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT1_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0))) ),
inference(ennf_transformation,[],[f128]) ).
tff(f205,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( p(mono_2Ec_2Earithmetic_2EODD_2E1(X0))
| p(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0)) )
& ( ~ p(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0))
| ~ p(mono_2Ec_2Earithmetic_2EODD_2E1(X0)) ) ),
inference(nnf_transformation,[],[f77]) ).
tff(f206,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( p(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0))
| ! [X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),X1) != X0 ) )
& ( ? [X1: mono_2Etyop_2Enum_2Enum] : ( X0 = mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),X1) )
| ~ p(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0)) ) ),
inference(nnf_transformation,[],[f78]) ).
tff(f207,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( p(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0))
| ! [X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),X1) != X0 ) )
& ( ? [X2: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),X2) = X0 )
| ~ p(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0)) ) ),
inference(rectify,[],[f206]) ).
tff(f208,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( p(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0))
| ! [X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),X1) != X0 ) )
& ( ( mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),sK15(X0)) = X0 )
| ~ p(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X2,sK15(X0))],[f207]) ).
tff(f209,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( p(mono_2Ec_2Earithmetic_2EODD_2E1(X0))
| ! [X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Enum_2ESUC_2E1(mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),X1)) != X0 ) )
& ( ? [X1: mono_2Etyop_2Enum_2Enum] : ( X0 = mono_2Ec_2Enum_2ESUC_2E1(mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),X1)) )
| ~ p(mono_2Ec_2Earithmetic_2EODD_2E1(X0)) ) ),
inference(nnf_transformation,[],[f79]) ).
tff(f210,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( p(mono_2Ec_2Earithmetic_2EODD_2E1(X0))
| ! [X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Enum_2ESUC_2E1(mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),X1)) != X0 ) )
& ( ? [X2: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Enum_2ESUC_2E1(mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),X2)) = X0 )
| ~ p(mono_2Ec_2Earithmetic_2EODD_2E1(X0)) ) ),
inference(rectify,[],[f209]) ).
tff(f211,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( p(mono_2Ec_2Earithmetic_2EODD_2E1(X0))
| ! [X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Enum_2ESUC_2E1(mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),X1)) != X0 ) )
& ( ( mono_2Ec_2Enum_2ESUC_2E1(mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),sK16(X0))) = X0 )
| ~ p(mono_2Ec_2Earithmetic_2EODD_2E1(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X2,sK16(X0))],[f210]) ).
tff(f216,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( p(X0)
| ~ p(mono_2Ec_2Ebool_2ET_2E0)
| ~ p(X0) )
& ( p(X0)
| ( ~ p(X0)
& p(mono_2Ec_2Ebool_2ET_2E0) ) )
& ( p(mono_2Ec_2Ebool_2ET_2E0)
| ~ p(X0)
| ~ p(mono_2Ec_2Ebool_2ET_2E0) )
& ( p(mono_2Ec_2Ebool_2ET_2E0)
| ( ~ p(mono_2Ec_2Ebool_2ET_2E0)
& p(X0) ) )
& ( p(X0)
| ~ p(mono_2Ec_2Ebool_2EF_2E0)
| ~ p(mono_2Ec_2Ebool_2ET_2E0) )
& ( p(mono_2Ec_2Ebool_2ET_2E0)
| ( ~ p(X0)
& p(mono_2Ec_2Ebool_2EF_2E0) ) )
& ( p(X0)
| ~ p(X0)
| ~ p(mono_2Ec_2Ebool_2ET_2E0) )
& ( p(mono_2Ec_2Ebool_2ET_2E0)
| ( ~ p(X0)
& p(X0) ) )
& ( p(mono_2Ec_2Ebool_2EF_2E0)
| ~ p(X0)
| p(X0) )
& ( ~ p(X0)
| ( ~ p(mono_2Ec_2Ebool_2EF_2E0)
& p(X0) ) ) ),
inference(nnf_transformation,[],[f140]) ).
tff(f217,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( p(X0)
| ~ p(mono_2Ec_2Ebool_2ET_2E0)
| ~ p(X0) )
& ( p(X0)
| ( ~ p(X0)
& p(mono_2Ec_2Ebool_2ET_2E0) ) )
& ( p(mono_2Ec_2Ebool_2ET_2E0)
| ~ p(X0)
| ~ p(mono_2Ec_2Ebool_2ET_2E0) )
& ( p(mono_2Ec_2Ebool_2ET_2E0)
| ( ~ p(mono_2Ec_2Ebool_2ET_2E0)
& p(X0) ) )
& ( p(X0)
| ~ p(mono_2Ec_2Ebool_2EF_2E0)
| ~ p(mono_2Ec_2Ebool_2ET_2E0) )
& ( p(mono_2Ec_2Ebool_2ET_2E0)
| ( ~ p(X0)
& p(mono_2Ec_2Ebool_2EF_2E0) ) )
& ( p(X0)
| ~ p(X0)
| ~ p(mono_2Ec_2Ebool_2ET_2E0) )
& ( p(mono_2Ec_2Ebool_2ET_2E0)
| ( ~ p(X0)
& p(X0) ) )
& ( p(mono_2Ec_2Ebool_2EF_2E0)
| ~ p(X0)
| p(X0) )
& ( ~ p(X0)
| ( ~ p(mono_2Ec_2Ebool_2EF_2E0)
& p(X0) ) ) ),
inference(flattening,[],[f216]) ).
tff(f222,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( ( mono_2Ec_2Ebool_2ET_2E0 = X0 )
| ~ p(X0) )
& ( p(X0)
| ( mono_2Ec_2Ebool_2ET_2E0 != X0 ) )
& ( ( X0 = mono_2Ec_2Ebool_2ET_2E0 )
| ~ p(X0) )
& ( p(X0)
| ( mono_2Ec_2Ebool_2ET_2E0 != X0 ) )
& ( ( mono_2Ec_2Ebool_2EF_2E0 = X0 )
| p(X0) )
& ( ~ p(X0)
| ( mono_2Ec_2Ebool_2EF_2E0 != X0 ) )
& ( ( X0 = mono_2Ec_2Ebool_2EF_2E0 )
| p(X0) )
& ( ~ p(X0)
| ( mono_2Ec_2Ebool_2EF_2E0 != X0 ) ) ),
inference(nnf_transformation,[],[f94]) ).
tff(f223,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( ( mono_2Ec_2Ebool_2ET_2E0 = X0 )
| ~ p(X0) )
& ( p(X0)
| ( mono_2Ec_2Ebool_2ET_2E0 != X0 ) )
& ( ( X0 = mono_2Ec_2Ebool_2ET_2E0 )
| ~ p(X0) )
& ( p(X0)
| ( mono_2Ec_2Ebool_2ET_2E0 != X0 ) )
& ( ( mono_2Ec_2Ebool_2EF_2E0 = X0 )
| p(X0) )
& ( ~ p(X0)
| ( mono_2Ec_2Ebool_2EF_2E0 != X0 ) )
& ( ( X0 = mono_2Ec_2Ebool_2EF_2E0 )
| p(X0) )
& ( ~ p(X0)
| ( mono_2Ec_2Ebool_2EF_2E0 != X0 ) ) ),
inference(flattening,[],[f222]) ).
tff(f313,plain,
mono_2Ec_2Earithmetic_2EMOD_2E2(sK38,mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0))) != mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EEVEN_2E1(sK38),mono_2Ec_2Enum_2E0_2E0,mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT1_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0))),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38]),skolemize(X0,sK38)],[f161]) ).
tff(f359,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : ( j_mono_2Etyop_2Enum_2Enum(s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(X0))) = X0 ),
inference(cnf_transformation,[],[f35]) ).
tff(f361,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2E_2A_2E2(X0,X1) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,X0),X1) ),
inference(cnf_transformation,[],[f37]) ).
tff(f362,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2E_2B_2E2(X0,X1) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2B_2E0,X0),X1) ),
inference(cnf_transformation,[],[f38]) ).
tff(f366,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Eprim__rec_2E_3C_2E2(X0,X1) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,X0),X1) ),
inference(cnf_transformation,[],[f40]) ).
tff(f373,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EBIT1_2E1(X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT1_2E0,X0) ),
inference(cnf_transformation,[],[f44]) ).
tff(f374,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EBIT2_2E1(X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT2_2E0,X0) ),
inference(cnf_transformation,[],[f45]) ).
tff(f379,plain,
! [X2: mono_2Etyop_2Enum_2Enum,X0: mono_2Etyop_2Emin_2Ebool,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Enum_2Enum(X0,X1,X2) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Enum_2Enum,X0),X1),X2) ),
inference(cnf_transformation,[],[f50]) ).
tff(f380,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EEVEN_2E1(X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0) ),
inference(cnf_transformation,[],[f51]) ).
tff(f381,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EMOD_2E2(X0,X1) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,X0),X1) ),
inference(cnf_transformation,[],[f52]) ).
tff(f382,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2ENUMERAL_2E1(X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,X0) ),
inference(cnf_transformation,[],[f53]) ).
tff(f383,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2EODD_2E1(X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,X0) ),
inference(cnf_transformation,[],[f54]) ).
tff(f384,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Enum_2ESUC_2E1(X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,X0) ),
inference(cnf_transformation,[],[f55]) ).
tff(f401,plain,
! [X2: mono_2Etyop_2Enum_2Enum,X0: mono_2Etyop_2Emin_2Ebool,X1: mono_2Etyop_2Enum_2Enum] : ( s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Enum_2Enum(X0,X1,X2))) = s(tyop_2Enum_2Enum,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(X0)),s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(X1)),s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(X2)))) ),
inference(cnf_transformation,[],[f69]) ).
tff(f402,plain,
mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT1_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)) = mono_2Ec_2Enum_2ESUC_2E1(mono_2Ec_2Enum_2E0_2E0),
inference(cnf_transformation,[],[f70]) ).
tff(f403,plain,
mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)) = mono_2Ec_2Enum_2ESUC_2E1(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT1_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0))),
inference(cnf_transformation,[],[f71]) ).
tff(f404,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2E_2B_2E2(X0,mono_2Ec_2Enum_2E0_2E0) = X0 ),
inference(cnf_transformation,[],[f72]) ).
tff(f405,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Eprim__rec_2E_3C_2E2(X0,X1) = mono_2Ec_2Eprim__rec_2E_3C_2E2(mono_2Ec_2Enum_2ESUC_2E1(X0),mono_2Ec_2Enum_2ESUC_2E1(X1)) ),
inference(cnf_transformation,[],[f73]) ).
tff(f406,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Enum_2ESUC_2E1(X0) = mono_2Ec_2Earithmetic_2E_2B_2E2(X0,mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT1_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0))) ),
inference(cnf_transformation,[],[f74]) ).
tff(f407,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Earithmetic_2E_2A_2E2(X0,X1) = mono_2Ec_2Earithmetic_2E_2A_2E2(X1,X0) ),
inference(cnf_transformation,[],[f75]) ).
tff(f410,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ~ p(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0))
| ~ p(mono_2Ec_2Earithmetic_2EODD_2E1(X0)) ),
inference(cnf_transformation,[],[f205]) ).
tff(f411,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( p(mono_2Ec_2Earithmetic_2EODD_2E1(X0))
| p(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0)) ),
inference(cnf_transformation,[],[f205]) ).
tff(f412,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),sK15(X0)) = X0 )
| ~ p(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0)) ),
inference(cnf_transformation,[],[f208]) ).
tff(f413,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] :
( p(mono_2Ec_2Earithmetic_2EEVEN_2E1(X0))
| ( mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),X1) != X0 ) ),
inference(cnf_transformation,[],[f208]) ).
tff(f414,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Enum_2ESUC_2E1(mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),sK16(X0))) = X0 )
| ~ p(mono_2Ec_2Earithmetic_2EODD_2E1(X0)) ),
inference(cnf_transformation,[],[f211]) ).
tff(f415,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] :
( p(mono_2Ec_2Earithmetic_2EODD_2E1(X0))
| ( mono_2Ec_2Enum_2ESUC_2E1(mono_2Ec_2Earithmetic_2E_2A_2E2(mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0)),X1)) != X0 ) ),
inference(cnf_transformation,[],[f211]) ).
tff(f416,plain,
! [X2: mono_2Etyop_2Enum_2Enum,X3: mono_2Etyop_2Enum_2Enum,X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Earithmetic_2EMOD_2E2(X1,X0) = X2 )
| ( mono_2Ec_2Earithmetic_2E_2B_2E2(mono_2Ec_2Earithmetic_2E_2A_2E2(X3,X0),X2) != X1 )
| ~ p(mono_2Ec_2Eprim__rec_2E_3C_2E2(X2,X0)) ),
inference(cnf_transformation,[],[f133]) ).
tff(f417,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2ET_2E0 = X0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) ),
inference(cnf_transformation,[],[f81]) ).
tff(f466,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( p(X0)
| ~ p(mono_2Ec_2Ebool_2EF_2E0)
| ~ p(mono_2Ec_2Ebool_2ET_2E0) ),
inference(cnf_transformation,[],[f217]) ).
tff(f484,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2EF_2E0 = X0 )
| p(X0) ),
inference(cnf_transformation,[],[f223]) ).
tff(f487,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( p(X0)
| ( mono_2Ec_2Ebool_2ET_2E0 != X0 ) ),
inference(cnf_transformation,[],[f223]) ).
tff(f488,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2ET_2E0 = X0 )
| ~ p(X0) ),
inference(cnf_transformation,[],[f223]) ).
tff(f491,plain,
! [X2: u,X0: d,X1: u] : ( s(X0,X2) = s(X0,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0)),s(X0,X1),s(X0,X2))) ),
inference(cnf_transformation,[],[f95]) ).
tff(f492,plain,
! [X2: u,X0: d,X1: u] : ( s(X0,X1) = s(X0,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0)),s(X0,X1),s(X0,X2))) ),
inference(cnf_transformation,[],[f95]) ).
tff(f551,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : p(mono_2Ec_2Eprim__rec_2E_3C_2E2(mono_2Ec_2Enum_2E0_2E0,mono_2Ec_2Enum_2ESUC_2E1(X0))),
inference(cnf_transformation,[],[f111]) ).
tff(f663,plain,
mono_2Ec_2Earithmetic_2EMOD_2E2(sK38,mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT2_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0))) != mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EEVEN_2E1(sK38),mono_2Ec_2Enum_2E0_2E0,mono_2Ec_2Earithmetic_2ENUMERAL_2E1(mono_2Ec_2Earithmetic_2EBIT1_2E1(mono_2Ec_2Earithmetic_2EZERO_2E0))),
inference(cnf_transformation,[],[f313]) ).
tff(f665,plain,
! [X2: mono_2Etyop_2Enum_2Enum,X0: mono_2Etyop_2Emin_2Ebool,X1: mono_2Etyop_2Enum_2Enum] : ( s(tyop_2Enum_2Enum,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(X0)),s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(X1)),s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(X2)))) = s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Enum_2Enum,X0),X1),X2))) ),
inference(definition_unfolding,[],[f401,f379]) ).
tff(f666,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT1_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0)) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Ec_2Enum_2E0_2E0),
inference(definition_unfolding,[],[f402,f382,f373,f384]) ).
tff(f667,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT2_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0)) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT1_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0))),
inference(definition_unfolding,[],[f403,f382,f374,f384,f382,f373]) ).
tff(f668,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2B_2E0,X0),mono_2Ec_2Enum_2E0_2E0) = X0 ),
inference(definition_unfolding,[],[f404,f362]) ).
tff(f669,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,X0),X1) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,X0)),mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,X1)) ),
inference(definition_unfolding,[],[f405,f366,f366,f384,f384]) ).
tff(f670,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2B_2E0,X0),mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT1_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0))) ),
inference(definition_unfolding,[],[f406,f384,f362,f382,f373]) ).
tff(f671,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,X0),X1) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,X1),X0) ),
inference(definition_unfolding,[],[f407,f361,f361]) ).
tff(f674,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,X0))
| p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0)) ),
inference(definition_unfolding,[],[f411,f383,f380]) ).
tff(f675,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0))
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,X0)) ),
inference(definition_unfolding,[],[f410,f380,f383]) ).
tff(f676,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] :
( p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0))
| ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT2_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0))),X1) != X0 ) ),
inference(definition_unfolding,[],[f413,f380,f361,f382,f374]) ).
tff(f677,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT2_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0))),sK15(X0)) = X0 )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0)) ),
inference(definition_unfolding,[],[f412,f361,f382,f374,f380]) ).
tff(f678,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] :
( p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,X0))
| ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT2_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0))),X1)) != X0 ) ),
inference(definition_unfolding,[],[f415,f383,f384,f361,f382,f374]) ).
tff(f679,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT2_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0))),sK16(X0))) = X0 )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,X0)) ),
inference(definition_unfolding,[],[f414,f384,f361,f382,f374,f383]) ).
tff(f680,plain,
! [X2: mono_2Etyop_2Enum_2Enum,X3: mono_2Etyop_2Enum_2Enum,X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,X1),X0) = X2 )
| ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2B_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,X3),X0)),X2) != X1 )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,X2),X0)) ),
inference(definition_unfolding,[],[f416,f381,f362,f361,f366]) ).
tff(f687,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,mono_2Ec_2Enum_2E0_2E0),mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,X0))),
inference(definition_unfolding,[],[f551,f366,f384]) ).
tff(f688,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,sK38),mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT2_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0))) != mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,sK38)),mono_2Ec_2Enum_2E0_2E0),mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT1_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0))),
inference(definition_unfolding,[],[f663,f381,f382,f374,f379,f380,f382,f373]) ).
tff(f689,plain,
! [X1: mono_2Etyop_2Enum_2Enum] : p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT2_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0))),X1))),
inference(equality_resolution,[],[f676]) ).
tff(f690,plain,
! [X1: mono_2Etyop_2Enum_2Enum] : p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT2_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0))),X1)))),
inference(equality_resolution,[],[f678]) ).
tff(f691,plain,
! [X2: mono_2Etyop_2Enum_2Enum,X3: mono_2Etyop_2Enum_2Enum,X0: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2B_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,X3),X0)),X2)),X0) = X2 )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,X2),X0)) ),
inference(equality_resolution,[],[f680]) ).
tff(f693,plain,
p(mono_2Ec_2Ebool_2ET_2E0),
inference(equality_resolution,[],[f487]) ).
tff(f698,definition,
sF39 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,sK38),
introduced(definition,[new_symbols(definition,[sF39])],[function_definition]) ).
tff(f699,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,sK38) = sF39,
inference(reorient_equations,[],[f698]) ).
tff(f700,definition,
sF40 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT2_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0),
introduced(definition,[new_symbols(definition,[sF40])],[function_definition]) ).
tff(f701,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT2_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0) = sF40,
inference(reorient_equations,[],[f700]) ).
tff(f702,definition,
sF41 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,sF40),
introduced(definition,[new_symbols(definition,[sF41])],[function_definition]) ).
tff(f703,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,sF40) = sF41,
inference(reorient_equations,[],[f702]) ).
tff(f704,definition,
sF42 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(sF39,sF41),
introduced(definition,[new_symbols(definition,[sF42])],[function_definition]) ).
tff(f705,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(sF39,sF41) = sF42,
inference(reorient_equations,[],[f704]) ).
tff(f706,definition,
sF43 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,sK38),
introduced(definition,[new_symbols(definition,[sF43])],[function_definition]) ).
tff(f707,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,sK38) = sF43,
inference(reorient_equations,[],[f706]) ).
tff(f708,definition,
sF44 = mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Enum_2Enum,sF43),
introduced(definition,[new_symbols(definition,[sF44])],[function_definition]) ).
tff(f709,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Enum_2Enum,sF43) = sF44,
inference(reorient_equations,[],[f708]) ).
tff(f710,definition,
sF45 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(sF44,mono_2Ec_2Enum_2E0_2E0),
introduced(definition,[new_symbols(definition,[sF45])],[function_definition]) ).
tff(f711,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(sF44,mono_2Ec_2Enum_2E0_2E0) = sF45,
inference(reorient_equations,[],[f710]) ).
tff(f712,definition,
sF46 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT1_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0),
introduced(definition,[new_symbols(definition,[sF46])],[function_definition]) ).
tff(f713,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT1_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0) = sF46,
inference(reorient_equations,[],[f712]) ).
tff(f714,definition,
sF47 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,sF46),
introduced(definition,[new_symbols(definition,[sF47])],[function_definition]) ).
tff(f715,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,sF46) = sF47,
inference(reorient_equations,[],[f714]) ).
tff(f716,definition,
sF48 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(sF45,sF47),
introduced(definition,[new_symbols(definition,[sF48])],[function_definition]) ).
tff(f717,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(sF45,sF47) = sF48,
inference(reorient_equations,[],[f716]) ).
tff(f718,plain,
sF42 != sF48,
inference(definition_folding,[],[f688,f717,f715,f713,f711,f709,f707,f705,f703,f701,f699]) ).
tff(f739,definition,
( spl49_2
<=> p(mono_2Ec_2Ebool_2EF_2E0) ),
introduced(definition,[new_symbols(definition,[spl49_2])],[avatar_definition]) ).
tff(f740,plain,
( ~ p(mono_2Ec_2Ebool_2EF_2E0)
| spl49_2 ),
inference(avatar_component_clause,[],[f739]) ).
tff(f758,definition,
( spl49_6
<=> ! [X1: mono_2Etyop_2Emin_2Ebool] : p(X1) ),
introduced(definition,[new_symbols(definition,[spl49_6])],[avatar_definition]) ).
tff(f759,plain,
( ! [X1: mono_2Etyop_2Emin_2Ebool] : p(X1)
| ~ spl49_6 ),
inference(avatar_component_clause,[],[f758]) ).
tff(f788,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( p(X0)
| ~ p(mono_2Ec_2Ebool_2EF_2E0) ),
inference(forward_subsumption_resolution,[],[f466,f693]) ).
tff(f795,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2EBIT2_2E0,mono_2Ec_2Earithmetic_2EZERO_2E0)) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Ec_2Enum_2E0_2E0)),
inference(backward_demodulation,[],[f667,f666]) ).
tff(f796,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2B_2E0,X0),mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Ec_2Enum_2E0_2E0)) ),
inference(backward_demodulation,[],[f670,f666]) ).
tff(f797,plain,
! [X1: mono_2Etyop_2Enum_2Enum] : p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,sF40)),X1))),
inference(backward_demodulation,[],[f689,f701]) ).
tff(f798,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,sF40)),sK15(X0)) = X0 )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0)) ),
inference(backward_demodulation,[],[f677,f701]) ).
tff(f799,plain,
! [X1: mono_2Etyop_2Enum_2Enum] : p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,sF40)),X1)))),
inference(backward_demodulation,[],[f690,f701]) ).
tff(f800,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,sF40)),sK16(X0))) = X0 )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,X0)) ),
inference(backward_demodulation,[],[f679,f701]) ).
tff(f801,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Ec_2Enum_2E0_2E0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,sF46),
inference(backward_demodulation,[],[f666,f713]) ).
tff(f802,plain,
( ~ spl49_2
| spl49_6 ),
inference(avatar_split_clause,[],[f788,f758,f739]) ).
tff(f803,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Earithmetic_2ENUMERAL_2E0,sF40) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Ec_2Enum_2E0_2E0)),
inference(forward_demodulation,[],[f795,f701]) ).
tff(f804,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,sF41),sK16(X0))) = X0 )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,X0)) ),
inference(forward_demodulation,[],[f800,f703]) ).
tff(f805,plain,
! [X1: mono_2Etyop_2Enum_2Enum] : p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,sF41),X1)))),
inference(forward_demodulation,[],[f799,f703]) ).
tff(f806,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,sF41),sK15(X0)) = X0 )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0)) ),
inference(forward_demodulation,[],[f798,f703]) ).
tff(f807,plain,
! [X1: mono_2Etyop_2Enum_2Enum] : p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,sF41),X1))),
inference(forward_demodulation,[],[f797,f703]) ).
tff(f808,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Ec_2Enum_2E0_2E0) = sF47,
inference(forward_demodulation,[],[f801,f715]) ).
tff(f809,plain,
sF41 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Ec_2Enum_2E0_2E0)),
inference(forward_demodulation,[],[f803,f703]) ).
tff(f810,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2B_2E0,X0),sF47) ),
inference(backward_demodulation,[],[f796,f808]) ).
tff(f811,plain,
sF41 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,sF47),
inference(forward_demodulation,[],[f809,f808]) ).
tff(f820,plain,
! [X2: mono_2Etyop_2Enum_2Enum,X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2B_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,X0),X1)),X2)),X0) = X2 )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,X2),X0)) ),
inference(superposition,[],[f691,f671]) ).
tff(f821,plain,
( ! [X2: mono_2Etyop_2Enum_2Enum,X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2B_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,X0),X1)),X2)),X0) = X2 )
| ~ spl49_6 ),
inference(forward_subsumption_resolution,[],[f820,f759]) ).
tff(f826,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,X0),sF41))),
inference(superposition,[],[f807,f671]) ).
tff(f834,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2B_2E0,X0),X1)),sF41) = X1 )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0)) )
| ~ spl49_6 ),
inference(superposition,[],[f821,f806]) ).
tff(f837,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2B_2E0,X0),X1)),sF41) = X1 )
| ~ spl49_6 ),
inference(forward_subsumption_resolution,[],[f834,f759]) ).
tff(f844,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Enum_2E0_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,X0),sF41) )
| ~ spl49_6 ),
inference(superposition,[],[f837,f668]) ).
tff(f846,plain,
( ! [X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Enum_2E0_2E0 = X1 )
| ~ spl49_6 ),
inference(backward_demodulation,[],[f837,f844]) ).
tff(f880,plain,
( ( mono_2Ec_2Enum_2E0_2E0 != sF48 )
| ~ spl49_6 ),
inference(backward_demodulation,[],[f718,f846]) ).
tff(f884,plain,
( $false
| ~ spl49_6 ),
inference(forward_subsumption_resolution,[],[f880,f846]) ).
tff(f885,plain,
~ spl49_6,
inference(avatar_contradiction_clause,[],[f884]) ).
tff(f901,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2B_2E0,X0),X1)),sF41) = X1 )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,X1),sF41))
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0)) ),
inference(superposition,[],[f820,f806]) ).
tff(f903,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] :
( ( sF47 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,X0),X1))),X0) )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,sF47),X0)) ),
inference(superposition,[],[f820,f810]) ).
tff(f909,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Enum_2E0_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,X0),sF41) )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,mono_2Ec_2Enum_2E0_2E0),sF41))
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0)) ),
inference(superposition,[],[f901,f668]) ).
tff(f920,definition,
( spl49_15
<=> p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,mono_2Ec_2Enum_2E0_2E0),sF41)) ),
introduced(definition,[new_symbols(definition,[spl49_15])],[avatar_definition]) ).
tff(f922,plain,
( ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,mono_2Ec_2Enum_2E0_2E0),sF41))
| spl49_15 ),
inference(avatar_component_clause,[],[f920]) ).
tff(f924,definition,
( spl49_16
<=> ! [X0: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Enum_2E0_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,X0),sF41) )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl49_16])],[avatar_definition]) ).
tff(f925,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Enum_2E0_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,X0),sF41) )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0)) )
| ~ spl49_16 ),
inference(avatar_component_clause,[],[f924]) ).
tff(f926,plain,
( ~ spl49_15
| spl49_16 ),
inference(avatar_split_clause,[],[f909,f924,f920]) ).
tff(f935,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Ebool_2ET_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,X0),sF41)) ),
inference(unit_resulting_resolution,[],[f488,f826]) ).
tff(f944,plain,
! [X0: mono_2Etyop_2Emin_2Ebool,X1: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2EF_2E0 = X0 )
| ~ p(X1)
| ( X0 = X1 ) ),
inference(superposition,[],[f488,f417]) ).
tff(f946,plain,
( ( sF44 = mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Ebool_2ET_2E0) )
| ( mono_2Ec_2Ebool_2EF_2E0 = sF43 ) ),
inference(superposition,[],[f709,f417]) ).
tff(f947,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2ET_2E0 != mono_2Ec_2Ebool_2EF_2E0 )
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) ),
inference(equality_factoring,[],[f417]) ).
tff(f949,definition,
( spl49_17
<=> ! [X0: mono_2Etyop_2Emin_2Ebool] : ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl49_17])],[avatar_definition]) ).
tff(f950,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] : ( mono_2Ec_2Ebool_2EF_2E0 = X0 )
| ~ spl49_17 ),
inference(avatar_component_clause,[],[f949]) ).
tff(f952,definition,
( spl49_18
<=> ( mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0 ) ),
introduced(definition,[new_symbols(definition,[spl49_18])],[avatar_definition]) ).
tff(f954,plain,
( ( mono_2Ec_2Ebool_2ET_2E0 != mono_2Ec_2Ebool_2EF_2E0 )
| spl49_18 ),
inference(avatar_component_clause,[],[f952]) ).
tff(f955,plain,
( spl49_17
| ~ spl49_18 ),
inference(avatar_split_clause,[],[f947,f952,f949]) ).
tff(f957,definition,
( spl49_19
<=> ( mono_2Ec_2Ebool_2EF_2E0 = sF43 ) ),
introduced(definition,[new_symbols(definition,[spl49_19])],[avatar_definition]) ).
tff(f958,plain,
( ( mono_2Ec_2Ebool_2EF_2E0 != sF43 )
| spl49_19 ),
inference(avatar_component_clause,[],[f957]) ).
tff(f959,plain,
( ( mono_2Ec_2Ebool_2EF_2E0 = sF43 )
| ~ spl49_19 ),
inference(avatar_component_clause,[],[f957]) ).
tff(f961,definition,
( spl49_20
<=> ( sF44 = mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Ebool_2ET_2E0) ) ),
introduced(definition,[new_symbols(definition,[spl49_20])],[avatar_definition]) ).
tff(f963,plain,
( ( sF44 = mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Ebool_2ET_2E0) )
| ~ spl49_20 ),
inference(avatar_component_clause,[],[f961]) ).
tff(f964,plain,
( spl49_19
| spl49_20 ),
inference(avatar_split_clause,[],[f946,f961,f957]) ).
tff(f966,plain,
( ( sF44 = mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Ebool_2EF_2E0) )
| ~ spl49_19 ),
inference(backward_demodulation,[],[f709,f959]) ).
tff(f967,plain,
( ( mono_2Ec_2Ebool_2EF_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,sK38) )
| ~ spl49_19 ),
inference(backward_demodulation,[],[f707,f959]) ).
tff(f979,plain,
p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,mono_2Ec_2Enum_2E0_2E0),sF47)),
inference(superposition,[],[f687,f808]) ).
tff(f980,plain,
p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,mono_2Ec_2Enum_2E0_2E0),sF41)),
inference(superposition,[],[f687,f811]) ).
tff(f983,plain,
( $false
| spl49_15 ),
inference(forward_subsumption_resolution,[],[f980,f922]) ).
tff(f984,plain,
spl49_15,
inference(avatar_contradiction_clause,[],[f983]) ).
tff(f993,plain,
mono_2Ec_2Ebool_2ET_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,mono_2Ec_2Enum_2E0_2E0),sF47),
inference(unit_resulting_resolution,[],[f488,f979]) ).
tff(f998,plain,
( ( mono_2Ec_2Enum_2E0_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(sF39,sF41) )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,sK38))
| ~ spl49_16 ),
inference(superposition,[],[f925,f699]) ).
tff(f1007,plain,
( ( mono_2Ec_2Enum_2E0_2E0 = sF42 )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,sK38))
| ~ spl49_16 ),
inference(forward_demodulation,[],[f998,f705]) ).
tff(f1014,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,X0)))
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0)) ),
inference(superposition,[],[f805,f806]) ).
tff(f1044,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( sF47 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,X0),sF41) )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,sF47),sF41))
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,X0)) ),
inference(superposition,[],[f903,f804]) ).
tff(f1075,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(X0)) = s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Ebool_2EF_2E0),X1),X0))) ),
inference(superposition,[],[f665,f491]) ).
tff(f1076,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(X0)) = s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(sF44,X1),X0))) )
| ~ spl49_19 ),
inference(forward_demodulation,[],[f1075,f966]) ).
tff(f1078,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum] : ( s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(X0)) = s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(sF45,X0))) )
| ~ spl49_19 ),
inference(superposition,[],[f1076,f711]) ).
tff(f1133,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(X0)) = s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Ebool_2ET_2E0),X0),X1))) ),
inference(superposition,[],[f665,f492]) ).
tff(f1262,plain,
! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,mono_2Ec_2Enum_2E0_2E0),X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,sF47),mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,X0)) ),
inference(superposition,[],[f669,f808]) ).
tff(f1283,plain,
mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,sF47),sF41) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,mono_2Ec_2Enum_2E0_2E0),sF47),
inference(superposition,[],[f1262,f811]) ).
tff(f1295,plain,
mono_2Ec_2Ebool_2ET_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Eprim__rec_2E_3C_2E0,sF47),sF41),
inference(forward_demodulation,[],[f1283,f993]) ).
tff(f1304,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ~ p(mono_2Ec_2Ebool_2ET_2E0)
| ( sF47 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,X0),sF41) )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,X0)) ),
inference(forward_demodulation,[],[f1044,f1295]) ).
tff(f1309,plain,
! [X0: mono_2Etyop_2Enum_2Enum] :
( ( sF47 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2EMOD_2E0,X0),sF41) )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,X0)) ),
inference(forward_subsumption_resolution,[],[f1304,f693]) ).
tff(f1314,definition,
( spl49_26
<=> ( mono_2Ec_2Enum_2E0_2E0 = sF47 ) ),
introduced(definition,[new_symbols(definition,[spl49_26])],[avatar_definition]) ).
tff(f1315,plain,
( ( mono_2Ec_2Enum_2E0_2E0 != sF47 )
| spl49_26 ),
inference(avatar_component_clause,[],[f1314]) ).
tff(f1316,plain,
( ( mono_2Ec_2Enum_2E0_2E0 = sF47 )
| ~ spl49_26 ),
inference(avatar_component_clause,[],[f1314]) ).
tff(f1326,plain,
( ( mono_2Ec_2Enum_2E0_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Ec_2Enum_2E0_2E0) )
| ~ spl49_26 ),
inference(backward_demodulation,[],[f808,f1316]) ).
tff(f1327,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,X0) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2B_2E0,X0),mono_2Ec_2Enum_2E0_2E0) )
| ~ spl49_26 ),
inference(backward_demodulation,[],[f810,f1316]) ).
tff(f1328,plain,
( ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,mono_2Ec_2Enum_2E0_2E0) = sF41 )
| ~ spl49_26 ),
inference(backward_demodulation,[],[f811,f1316]) ).
tff(f1362,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Enum_2ESUC_2E0,X0) = X0 )
| ~ spl49_26 ),
inference(forward_demodulation,[],[f1327,f668]) ).
tff(f1363,plain,
( ( mono_2Ec_2Enum_2E0_2E0 = sF41 )
| ~ spl49_26 ),
inference(backward_demodulation,[],[f1328,f1326]) ).
tff(f1383,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum] :
( p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,X0))
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0)) )
| ~ spl49_26 ),
inference(backward_demodulation,[],[f1014,f1362]) ).
tff(f1408,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Ebool_2ET_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Ec_2Earithmetic_2E_2A_2E0,X0),mono_2Ec_2Enum_2E0_2E0)) )
| ~ spl49_26 ),
inference(backward_demodulation,[],[f935,f1363]) ).
tff(f1441,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum] : ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0))
| ~ spl49_26 ),
inference(forward_subsumption_resolution,[],[f1383,f675]) ).
tff(f1461,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Ebool_2EF_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,X0) )
| ~ spl49_26 ),
inference(unit_resulting_resolution,[],[f484,f1441]) ).
tff(f1481,plain,
( ( mono_2Ec_2Ebool_2ET_2E0 = mono_2Ec_2Ebool_2EF_2E0 )
| ~ spl49_26 ),
inference(backward_demodulation,[],[f1408,f1461]) ).
tff(f1485,plain,
( $false
| spl49_18
| ~ spl49_26 ),
inference(forward_subsumption_resolution,[],[f1481,f954]) ).
tff(f1486,plain,
( spl49_18
| ~ spl49_26 ),
inference(avatar_contradiction_clause,[],[f1485]) ).
tff(f1606,plain,
( ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(sF39,sF41) = sF47 )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,sK38)) ),
inference(superposition,[],[f1309,f699]) ).
tff(f1623,plain,
( ( sF42 = sF47 )
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,sK38)) ),
inference(forward_demodulation,[],[f1606,f705]) ).
tff(f1629,definition,
( spl49_28
<=> p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,sK38)) ),
introduced(definition,[new_symbols(definition,[spl49_28])],[avatar_definition]) ).
tff(f1631,plain,
( ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,sK38))
| spl49_28 ),
inference(avatar_component_clause,[],[f1629]) ).
tff(f1633,definition,
( spl49_29
<=> ( sF42 = sF47 ) ),
introduced(definition,[new_symbols(definition,[spl49_29])],[avatar_definition]) ).
tff(f1635,plain,
( ( sF42 = sF47 )
| ~ spl49_29 ),
inference(avatar_component_clause,[],[f1633]) ).
tff(f1636,plain,
( ~ spl49_28
| spl49_29 ),
inference(avatar_split_clause,[],[f1623,f1633,f1629]) ).
tff(f1642,plain,
( ( mono_2Ec_2Ebool_2EF_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,sK38) )
| spl49_28 ),
inference(unit_resulting_resolution,[],[f484,f1631]) ).
tff(f1666,plain,
( p(mono_2Ec_2Ebool_2EF_2E0)
| p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,sK38))
| spl49_28 ),
inference(superposition,[],[f674,f1642]) ).
tff(f1670,plain,
( p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,sK38))
| spl49_2
| spl49_28 ),
inference(forward_subsumption_resolution,[],[f1666,f740]) ).
tff(f1671,plain,
( p(mono_2Ec_2Ebool_2EF_2E0)
| spl49_2
| ~ spl49_19
| spl49_28 ),
inference(forward_demodulation,[],[f1670,f967]) ).
tff(f1672,plain,
( $false
| spl49_2
| ~ spl49_19
| spl49_28 ),
inference(forward_subsumption_resolution,[],[f1671,f740]) ).
tff(f1673,plain,
( spl49_2
| ~ spl49_19
| spl49_28 ),
inference(avatar_contradiction_clause,[],[f1672]) ).
tff(f1675,plain,
( ( sF48 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(sF45,sF42) )
| ~ spl49_29 ),
inference(backward_demodulation,[],[f717,f1635]) ).
tff(f1704,plain,
( ( mono_2Ec_2Enum_2E0_2E0 != sF42 )
| spl49_26
| ~ spl49_29 ),
inference(backward_demodulation,[],[f1315,f1635]) ).
tff(f1908,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( j_mono_2Etyop_2Enum_2Enum(s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(X0))) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Ebool_2ET_2E0),X0),X1) ),
inference(superposition,[],[f359,f1133]) ).
tff(f1909,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum] : ( j_mono_2Etyop_2Enum_2Enum(s(tyop_2Enum_2Enum,i_mono_2Etyop_2Enum_2Enum(X0))) = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(sF45,X0) )
| ~ spl49_19 ),
inference(superposition,[],[f359,f1078]) ).
tff(f1910,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(sF45,X0) = X0 )
| ~ spl49_19 ),
inference(forward_demodulation,[],[f1909,f359]) ).
tff(f1911,plain,
! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(mono_2Ec_2Ebool_2ECOND_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Ebool_2ET_2E0),X0),X1) = X0 ),
inference(forward_demodulation,[],[f1908,f359]) ).
tff(f1913,plain,
( ( sF42 = sF48 )
| ~ spl49_19
| ~ spl49_29 ),
inference(backward_demodulation,[],[f1675,f1910]) ).
tff(f1914,plain,
( $false
| ~ spl49_19
| ~ spl49_29 ),
inference(forward_subsumption_resolution,[],[f1913,f718]) ).
tff(f1915,plain,
( ~ spl49_19
| ~ spl49_29 ),
inference(avatar_contradiction_clause,[],[f1914]) ).
tff(f1916,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum,X1: mono_2Etyop_2Enum_2Enum] : ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(sF44,X0),X1) = X0 )
| ~ spl49_20 ),
inference(backward_demodulation,[],[f1911,f963]) ).
tff(f1917,plain,
( p(sF43)
| spl49_2
| spl49_28 ),
inference(backward_demodulation,[],[f1670,f707]) ).
tff(f1918,plain,
( ~ p(sF43)
| ( mono_2Ec_2Enum_2E0_2E0 = sF42 )
| ~ spl49_16 ),
inference(forward_demodulation,[],[f1007,f707]) ).
tff(f1922,plain,
( ( mono_2Ec_2Enum_2E0_2E0 = sF42 )
| spl49_2
| ~ spl49_16
| spl49_28 ),
inference(forward_subsumption_resolution,[],[f1918,f1917]) ).
tff(f1927,plain,
( ( mono_2Ec_2Enum_2E0_2E0 != sF48 )
| spl49_2
| ~ spl49_16
| spl49_28 ),
inference(backward_demodulation,[],[f718,f1922]) ).
tff(f1941,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( mono_2Ec_2Ebool_2EF_2E0 = sF43 )
| ~ p(X0)
| ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,sK38) = X0 ) ),
inference(superposition,[],[f707,f944]) ).
tff(f1942,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ~ p(X0)
| ( mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EEVEN_2E0,sK38) = X0 ) )
| spl49_19 ),
inference(forward_subsumption_resolution,[],[f1941,f958]) ).
tff(f1945,plain,
( ! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( sF43 = X0 )
| ~ p(X0) )
| spl49_19 ),
inference(forward_demodulation,[],[f1942,f707]) ).
tff(f1950,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum] : ( mono_2Ec_2Enum_2E0_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(sF45,X0) )
| ~ spl49_20 ),
inference(superposition,[],[f1916,f711]) ).
tff(f1951,plain,
( ( mono_2Ec_2Enum_2E0_2E0 = sF48 )
| ~ spl49_20 ),
inference(backward_demodulation,[],[f717,f1950]) ).
tff(f1952,plain,
( $false
| spl49_2
| ~ spl49_16
| ~ spl49_20
| spl49_28 ),
inference(forward_subsumption_resolution,[],[f1951,f1927]) ).
tff(f1953,plain,
( spl49_2
| ~ spl49_16
| ~ spl49_20
| spl49_28 ),
inference(avatar_contradiction_clause,[],[f1952]) ).
tff(f1987,plain,
( ~ p(sF43)
| ~ spl49_16
| spl49_26
| ~ spl49_29 ),
inference(forward_subsumption_resolution,[],[f1918,f1704]) ).
tff(f1997,plain,
( ( mono_2Ec_2Ebool_2ET_2E0 = sF43 )
| spl49_19 ),
inference(unit_resulting_resolution,[],[f1945,f693]) ).
tff(f2003,plain,
( ~ p(mono_2Ec_2Ebool_2ET_2E0)
| ~ spl49_16
| spl49_19
| spl49_26
| ~ spl49_29 ),
inference(backward_demodulation,[],[f1987,f1997]) ).
tff(f2009,plain,
( $false
| ~ spl49_16
| spl49_19
| spl49_26
| ~ spl49_29 ),
inference(forward_subsumption_resolution,[],[f2003,f693]) ).
tff(f2010,plain,
( ~ spl49_16
| spl49_19
| spl49_26
| ~ spl49_29 ),
inference(avatar_contradiction_clause,[],[f2009]) ).
tff(f2080,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum] :
( p(mono_2Ec_2Ebool_2EF_2E0)
| p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,X0)) )
| ~ spl49_17 ),
inference(backward_demodulation,[],[f674,f950]) ).
tff(f2201,plain,
( ! [X0: mono_2Etyop_2Enum_2Enum] : p(mono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Earithmetic_2EODD_2E0,X0))
| spl49_2
| ~ spl49_17 ),
inference(forward_subsumption_resolution,[],[f2080,f740]) ).
tff(f2231,plain,
( p(mono_2Ec_2Ebool_2EF_2E0)
| spl49_2
| ~ spl49_17 ),
inference(forward_demodulation,[],[f2201,f950]) ).
tff(f2238,plain,
( $false
| spl49_2
| ~ spl49_17 ),
inference(forward_subsumption_resolution,[],[f2231,f740]) ).
tff(f2239,plain,
( spl49_2
| ~ spl49_17 ),
inference(avatar_contradiction_clause,[],[f2238]) ).
cnf(s25,plain,
( ~ spl49_2
| spl49_6 ),
inference(sat_conversion,[],[f802]) ).
cnf(s27,plain,
~ spl49_6,
inference(sat_conversion,[],[f885]) ).
cnf(s29,plain,
( ~ spl49_15
| spl49_16 ),
inference(sat_conversion,[],[f926]) ).
cnf(s30,plain,
( spl49_17
| ~ spl49_18 ),
inference(sat_conversion,[],[f955]) ).
cnf(s31,plain,
( spl49_19
| spl49_20 ),
inference(sat_conversion,[],[f964]) ).
cnf(s32,plain,
spl49_15,
inference(sat_conversion,[],[f984]) ).
cnf(s41,plain,
( spl49_18
| ~ spl49_26 ),
inference(sat_conversion,[],[f1486]) ).
cnf(s42,plain,
( ~ spl49_28
| spl49_29 ),
inference(sat_conversion,[],[f1636]) ).
cnf(s43,plain,
( spl49_2
| ~ spl49_19
| spl49_28 ),
inference(sat_conversion,[],[f1673]) ).
cnf(s45,plain,
( ~ spl49_19
| ~ spl49_29 ),
inference(sat_conversion,[],[f1915]) ).
cnf(s48,plain,
( spl49_2
| ~ spl49_16
| ~ spl49_20
| spl49_28 ),
inference(sat_conversion,[],[f1953]) ).
cnf(s49,plain,
( ~ spl49_16
| spl49_19
| spl49_26
| ~ spl49_29 ),
inference(sat_conversion,[],[f2010]) ).
cnf(s76,plain,
( spl49_2
| ~ spl49_17 ),
inference(sat_conversion,[],[f2239]) ).
cnf(s77,plain,
spl49_16,
inference(rat,[],[s29,s32]) ).
cnf(s79,plain,
~ spl49_2,
inference(rat,[],[s25,s27]) ).
cnf(s80,plain,
~ spl49_17,
inference(rat,[],[s76,s79]) ).
cnf(s81,plain,
~ spl49_18,
inference(rat,[],[s30,s80]) ).
cnf(s82,plain,
~ spl49_26,
inference(rat,[],[s41,s81]) ).
cnf(s89,plain,
spl49_19,
inference(rat,[],[s48,s42,s31,s49,s77,s79,s82]) ).
cnf(s90,plain,
~ spl49_29,
inference(rat,[],[s45,s89]) ).
cnf(s91,plain,
spl49_28,
inference(rat,[],[s43,s79,s89]) ).
cnf(s92,plain,
$false,
inference(rat,[],[s42,s90,s91]) ).
tff(f2240,plain,
$false,
inference(avatar_sat_refutation,[],[s92]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP003_1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n006.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 11:48:26 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.17/2.38 % (2835703)Detected formulas, will run a generic FOF schedule.
% 10.17/2.38 % (2835710)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3393350635:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.17/2.38 % (2835711)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1730501397:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.17/2.38 % (2835708)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3506893559:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.17/2.38 % (2835713)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=219237116:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.17/2.38 % (2835712)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2040431725:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.17/2.38 % (2835709)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=210879910:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.17/2.38 % (2835714)dis-21_1_sil=8000:lcm=predicate:random_seed=2016375924:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.17/2.38 % (2835711)Refutation not found, incomplete strategy
% 10.17/2.38 % (2835711)------------------------------
% 10.17/2.38 % (2835711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.38 % (2835711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.38 % (2835711)CaDiCaL version: 2.1.3
% 10.17/2.38 % (2835711)Termination reason: Refutation not found, incomplete strategy
% 10.17/2.38 % (2835711)Time elapsed: 0.002 s
% 10.17/2.38 % (2835711)Peak memory usage: 88 MB
% 10.17/2.38 % (2835711)Instructions burned: 1 (million)
% 10.17/2.38 % (2835712)Instruction limit reached!
% 10.17/2.38 % (2835712)------------------------------
% 10.17/2.38 % (2835712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.38 % (2835712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.38 % (2835712)CaDiCaL version: 2.1.3
% 10.17/2.38 % (2835712)Termination reason: Instruction limit
% 10.17/2.38 % (2835712)Termination phase: Saturation
% 10.17/2.38 % (2835712)Time elapsed: 0.068 s
% 10.17/2.38 % (2835712)Peak memory usage: 89 MB
% 10.17/2.38 % (2835712)Instructions burned: 119 (million)
% 10.17/2.38 % (2835714)Instruction limit reached!
% 10.17/2.38 % (2835714)------------------------------
% 10.17/2.38 % (2835714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.38 % (2835714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.38 % (2835714)CaDiCaL version: 2.1.3
% 10.17/2.38 % (2835714)Termination reason: Instruction limit
% 10.17/2.38 % (2835714)Termination phase: Saturation
% 10.17/2.38 % (2835714)Time elapsed: 0.072 s
% 10.17/2.38 % (2835714)Peak memory usage: 89 MB
% 10.17/2.38 % (2835714)Instructions burned: 129 (million)
% 10.17/2.38 % (2835713)Instruction limit reached!
% 10.17/2.38 % (2835713)------------------------------
% 10.17/2.38 % (2835713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.38 % (2835713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.38 % (2835713)CaDiCaL version: 2.1.3
% 10.17/2.38 % (2835713)Termination reason: Instruction limit
% 10.17/2.38 % (2835713)Termination phase: Saturation
% 10.17/2.38 % (2835713)Time elapsed: 0.089 s
% 10.17/2.38 % (2835713)Peak memory usage: 90 MB
% 10.17/2.38 % (2835713)Instructions burned: 139 (million)
% 10.17/2.38 % (2835723)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4157050860:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.17/2.38 % (2835722)lrs+10_1_sil=8000:sp=occurrence:random_seed=1118826092:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.17/2.38 % (2835723)Refutation not found, incomplete strategy
% 10.17/2.38 % (2835723)------------------------------
% 10.17/2.38 % (2835723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.38 % (2835723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.38 % (2835723)CaDiCaL version: 2.1.3
% 10.17/2.38 % (2835723)Termination reason: Refutation not found, incomplete strategy
% 13.73/3.03 % (2835723)Time elapsed: 0.005 s
% 13.73/3.03 % (2835723)Peak memory usage: 89 MB
% 13.73/3.03 % (2835723)Instructions burned: 6 (million)
% 13.73/3.03 % (2835711)------------------------------
% 13.73/3.03 % (2835711)------------------------------
% 13.73/3.03 % (2835724)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1737504657:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.73/3.03 % (2835724)Refutation not found, incomplete strategy
% 13.73/3.03 % (2835724)------------------------------
% 13.73/3.03 % (2835724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.73/3.03 % (2835724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.73/3.03 % (2835724)CaDiCaL version: 2.1.3
% 13.73/3.03 % (2835724)Termination reason: Refutation not found, incomplete strategy
% 13.73/3.03 % (2835724)Time elapsed: 0.005 s
% 13.73/3.03 % (2835724)Peak memory usage: 89 MB
% 13.73/3.03 % (2835724)Instructions burned: 6 (million)
% 13.73/3.03 % (2835710)Refutation not found, incomplete strategy
% 13.73/3.03 % (2835710)------------------------------
% 13.73/3.03 % (2835710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.73/3.03 % (2835710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.73/3.03 % (2835710)CaDiCaL version: 2.1.3
% 13.73/3.03 % (2835710)Termination reason: Refutation not found, incomplete strategy
% 13.73/3.03 % (2835710)Time elapsed: 0.401 s
% 13.73/3.03 % (2835710)Peak memory usage: 132 MB
% 13.73/3.03 % (2835710)Instructions burned: 965 (million)
% 13.73/3.03 % (2835722)Instruction limit reached!
% 13.73/3.03 % (2835722)------------------------------
% 13.73/3.03 % (2835722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.73/3.03 % (2835722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.73/3.03 % (2835722)CaDiCaL version: 2.1.3
% 13.73/3.03 % (2835722)Termination reason: Instruction limit
% 13.73/3.03 % (2835722)Termination phase: Saturation
% 13.73/3.03 % (2835722)Time elapsed: 0.146 s
% 13.73/3.03 % (2835722)Peak memory usage: 89 MB
% 13.73/3.03 % (2835722)Instructions burned: 286 (million)
% 13.73/3.03 % (2835728)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3158680359:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 13.73/3.03 % (2835723)------------------------------
% 13.73/3.03 % (2835723)------------------------------
% 13.73/3.03 % (2835724)------------------------------
% 13.73/3.03 % (2835724)------------------------------
% 13.73/3.03 % (2835710)------------------------------
% 13.73/3.03 % (2835710)------------------------------
% 13.73/3.03 % (2835729)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2160800799:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 13.73/3.03 % (2835729)Refutation not found, incomplete strategy
% 13.73/3.03 % (2835729)------------------------------
% 13.73/3.03 % (2835729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.73/3.03 % (2835729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.73/3.03 % (2835729)CaDiCaL version: 2.1.3
% 13.73/3.03 % (2835729)Termination reason: Refutation not found, incomplete strategy
% 13.73/3.03 % (2835729)Time elapsed: 0.009 s
% 13.73/3.03 % (2835729)Peak memory usage: 88 MB
% 13.73/3.03 % (2835729)Instructions burned: 13 (million)
% 13.73/3.03 % (2835728)Instruction limit reached!
% 13.73/3.03 % (2835728)------------------------------
% 13.73/3.03 % (2835728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.73/3.03 % (2835728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.73/3.03 % (2835728)CaDiCaL version: 2.1.3
% 13.73/3.03 % (2835728)Termination reason: Instruction limit
% 13.73/3.03 % (2835728)Termination phase: Saturation
% 13.73/3.03 % (2835728)Time elapsed: 0.137 s
% 13.73/3.03 % (2835728)Peak memory usage: 93 MB
% 13.73/3.03 % (2835728)Instructions burned: 250 (million)
% 13.73/3.03 % (2835731)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2800834708:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 13.73/3.03 % (2835733)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3313924712:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 13.73/3.03 % (2835732)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3970543111:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 13.73/3.03 % (2835733)Refutation not found, incomplete strategy
% 18.47/4.31 % (2835733)------------------------------
% 18.47/4.31 % (2835733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835733)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835733)Termination reason: Refutation not found, incomplete strategy
% 18.47/4.31 % (2835733)Time elapsed: 0.006 s
% 18.47/4.31 % (2835733)Peak memory usage: 88 MB
% 18.47/4.31 % (2835733)Instructions burned: 21 (million)
% 18.47/4.31 % (2835732)Refutation not found, incomplete strategy
% 18.47/4.31 % (2835732)------------------------------
% 18.47/4.31 % (2835732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835732)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835732)Termination reason: Refutation not found, incomplete strategy
% 18.47/4.31 % (2835732)Time elapsed: 0.012 s
% 18.47/4.31 % (2835732)Peak memory usage: 89 MB
% 18.47/4.31 % (2835732)Instructions burned: 21 (million)
% 18.47/4.31 % (2835735)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3773993124:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 18.47/4.31 % (2835735)Instruction limit reached!
% 18.47/4.31 % (2835735)------------------------------
% 18.47/4.31 % (2835735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835735)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835735)Termination reason: Instruction limit
% 18.47/4.31 % (2835735)Termination phase: Saturation
% 18.47/4.31 % (2835735)Time elapsed: 0.055 s
% 18.47/4.31 % (2835735)Peak memory usage: 89 MB
% 18.47/4.31 % (2835735)Instructions burned: 114 (million)
% 18.47/4.31 % (2835729)------------------------------
% 18.47/4.31 % (2835729)------------------------------
% 18.47/4.31 % (2835733)------------------------------
% 18.47/4.31 % (2835733)------------------------------
% 18.47/4.31 % (2835732)------------------------------
% 18.47/4.31 % (2835732)------------------------------
% 18.47/4.31 % (2835741)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1765808044:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 18.47/4.31 % (2835740)lrs+10_1_sil=8000:sp=occurrence:random_seed=2461625508:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 18.47/4.31 % (2835741)Refutation not found, incomplete strategy
% 18.47/4.31 % (2835741)------------------------------
% 18.47/4.31 % (2835741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835741)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835741)Termination reason: Refutation not found, incomplete strategy
% 18.47/4.31 % (2835741)Time elapsed: 0.006 s
% 18.47/4.31 % (2835741)Peak memory usage: 89 MB
% 18.47/4.31 % (2835741)Instructions burned: 20 (million)
% 18.47/4.31 % (2835742)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1318087767:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 18.47/4.31 % (2835743)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=435600082:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 18.47/4.31 % (2835741)------------------------------
% 18.47/4.31 % (2835741)------------------------------
% 18.47/4.31 % (2835743)Instruction limit reached!
% 18.47/4.31 % (2835743)------------------------------
% 18.47/4.31 % (2835743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835743)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835743)Termination reason: Instruction limit
% 18.47/4.31 % (2835743)Termination phase: Saturation
% 18.47/4.31 % (2835743)Time elapsed: 0.075 s
% 18.47/4.31 % (2835743)Peak memory usage: 92 MB
% 18.47/4.31 % (2835743)Instructions burned: 134 (million)
% 18.47/4.31 % (2835748)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4051590742:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 18.47/4.31 % (2835749)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3500150970:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 18.47/4.31 % (2835748)Instruction limit reached!
% 18.47/4.31 % (2835748)------------------------------
% 18.47/4.31 % (2835748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835748)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835748)Termination reason: Instruction limit
% 18.47/4.31 % (2835748)Termination phase: Saturation
% 18.47/4.31 % (2835748)Time elapsed: 0.164 s
% 18.47/4.31 % (2835748)Peak memory usage: 93 MB
% 18.47/4.31 % (2835748)Instructions burned: 592 (million)
% 18.47/4.31 % (2835740)Instruction limit reached!
% 18.47/4.31 % (2835740)------------------------------
% 18.47/4.31 % (2835740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835740)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835740)Termination reason: Instruction limit
% 18.47/4.31 % (2835740)Termination phase: Saturation
% 18.47/4.31 % (2835740)Time elapsed: 0.487 s
% 18.47/4.31 % (2835740)Peak memory usage: 95 MB
% 18.47/4.31 % (2835740)Instructions burned: 908 (million)
% 18.47/4.31 % (2835752)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3858628157:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 18.47/4.31 % (2835752)Instruction limit reached!
% 18.47/4.31 % (2835752)------------------------------
% 18.47/4.31 % (2835752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835752)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835752)Termination reason: Instruction limit
% 18.47/4.31 % (2835752)Termination phase: Saturation
% 18.47/4.31 % (2835752)Time elapsed: 0.038 s
% 18.47/4.31 % (2835752)Peak memory usage: 91 MB
% 18.47/4.31 % (2835752)Instructions burned: 128 (million)
% 18.47/4.31 % (2835753)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=185796412:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi)
% 18.47/4.31 % (2835755)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1554118309:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi)
% 18.47/4.31 % (2835755)Refutation not found, incomplete strategy
% 18.47/4.31 % (2835755)------------------------------
% 18.47/4.31 % (2835755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835755)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835755)Termination reason: Refutation not found, incomplete strategy
% 18.47/4.31 % (2835755)Time elapsed: 0.001 s
% 18.47/4.31 % (2835755)Peak memory usage: 88 MB
% 18.47/4.31 % (2835755)Instructions burned: 1 (million)
% 18.47/4.31 % (2835753)Instruction limit reached!
% 18.47/4.31 % (2835753)------------------------------
% 18.47/4.31 % (2835753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835753)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835753)Termination reason: Instruction limit
% 18.47/4.31 % (2835753)Termination phase: Saturation
% 18.47/4.31 % (2835753)Time elapsed: 0.077 s
% 18.47/4.31 % (2835753)Peak memory usage: 90 MB
% 18.47/4.31 % (2835753)Instructions burned: 135 (million)
% 18.47/4.31 % (2835755)------------------------------
% 18.47/4.31 % (2835755)------------------------------
% 18.47/4.31 % (2835758)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1636900379:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi)
% 18.47/4.31 % (2835759)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=479828945:i=6060:aac=none:ins=25_2980 on theBenchmark for (2980ds/6060Mi)
% 18.47/4.31 % (2835731)Instruction limit reached!
% 18.47/4.31 % (2835731)------------------------------
% 18.47/4.31 % (2835731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835731)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835731)Termination reason: Instruction limit
% 18.47/4.31 % (2835731)Termination phase: Saturation
% 18.47/4.31 % (2835731)Time elapsed: 1.371 s
% 18.47/4.31 % (2835731)Peak memory usage: 135 MB
% 18.47/4.31 % (2835731)Instructions burned: 2351 (million)
% 18.47/4.31 % (2835758)Instruction limit reached!
% 18.47/4.31 % (2835758)------------------------------
% 18.47/4.31 % (2835758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835758)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835758)Termination reason: Instruction limit
% 18.47/4.31 % (2835758)Termination phase: Saturation
% 18.47/4.31 % (2835758)Time elapsed: 0.191 s
% 18.47/4.31 % (2835758)Peak memory usage: 91 MB
% 18.47/4.31 % (2835758)Instructions burned: 433 (million)
% 18.47/4.31 % (2835762)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1621680651:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2978 on theBenchmark for (2978ds/150Mi)
% 18.47/4.31 % (2835763)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2300971609:i=14155:bd=all_2978 on theBenchmark for (2978ds/14155Mi)
% 18.47/4.31 % (2835762)Instruction limit reached!
% 18.47/4.31 % (2835762)------------------------------
% 18.47/4.31 % (2835762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835762)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835762)Termination reason: Instruction limit
% 18.47/4.31 % (2835762)Termination phase: Saturation
% 18.47/4.31 % (2835762)Time elapsed: 0.080 s
% 18.47/4.31 % (2835762)Peak memory usage: 90 MB
% 18.47/4.31 % (2835762)Instructions burned: 151 (million)
% 18.47/4.31 % (2835766)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2618565305:i=667:av=off:fsr=off_2975 on theBenchmark for (2975ds/667Mi)
% 18.47/4.31 % (2835766)Refutation not found, incomplete strategy
% 18.47/4.31 % (2835766)------------------------------
% 18.47/4.31 % (2835766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835766)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835766)Termination reason: Refutation not found, incomplete strategy
% 18.47/4.31 % (2835766)Time elapsed: 0.010 s
% 18.47/4.31 % (2835766)Peak memory usage: 89 MB
% 18.47/4.31 % (2835766)Instructions burned: 18 (million)
% 18.47/4.31 % (2835766)------------------------------
% 18.47/4.31 % (2835766)------------------------------
% 18.47/4.31 % (2835768)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2324110997:s2a=on:i=185:s2at=1.8:fdi=4_2971 on theBenchmark for (2971ds/185Mi)
% 18.47/4.31 % (2835768)Instruction limit reached!
% 18.47/4.31 % (2835768)------------------------------
% 18.47/4.31 % (2835768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835768)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835768)Termination reason: Instruction limit
% 18.47/4.31 % (2835768)Termination phase: Saturation
% 18.47/4.31 % (2835768)Time elapsed: 0.101 s
% 18.47/4.31 % (2835768)Peak memory usage: 91 MB
% 18.47/4.31 % (2835768)Instructions burned: 186 (million)
% 18.47/4.31 % (2835763)First to succeed.
% 18.47/4.31 % (2835763)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2835703"
% 18.47/4.31 % (2835770)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3575801866:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2969 on theBenchmark for (2969ds/193Mi)
% 18.47/4.31 % (2835770)Instruction limit reached!
% 18.47/4.31 % (2835770)------------------------------
% 18.47/4.31 % (2835770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.47/4.31 % (2835770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.47/4.31 % (2835770)CaDiCaL version: 2.1.3
% 18.47/4.31 % (2835770)Termination reason: Instruction limit
% 18.47/4.31 % (2835770)Termination phase: Saturation
% 18.47/4.31 % (2835770)Time elapsed: 0.111 s
% 18.47/4.31 % (2835770)Peak memory usage: 90 MB
% 18.47/4.31 % (2835770)Instructions burned: 194 (million)
% 18.47/4.31 % (2835759)Also succeeded, but the first one will report.
% 18.47/4.31 % (2835763)Refutation found. Thanks to Tanya!
% 18.47/4.31 % SZS status Theorem for theBenchmark
% 18.47/4.31 % SZS output start Proof for theBenchmark
% See solution above
% 0.15/4.40 % (2835763)------------------------------
% 0.15/4.40 % (2835763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.15/4.40 % (2835763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/4.40 % (2835763)CaDiCaL version: 2.1.3
% 0.15/4.40 % (2835763)Termination reason: Refutation
% 0.15/4.40 % (2835763)Time elapsed: 0.832 s
% 0.15/4.40 % (2835763)Peak memory usage: 133 MB
% 0.15/4.40 % (2835763)Instructions burned: 1277 (million)
% 0.15/4.40 % (2835763)------------------------------
% 0.15/4.40 % (2835763)------------------------------
% 0.15/4.40 % (2835703)Success in time 3.445 s
% 0.15/4.40 % Vampire exiting
%------------------------------------------------------------------------------