%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP020_1 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:35:52 AM UTC 2026
% Result : Theorem 98.87s 29.46s
% Output : Refutation 98.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 17
% Syntax : Number of formulae : 69 ( 38 unt; 0 typ; 4 def)
% Number of atoms : 143 ( 41 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 129 ( 55 ~; 42 |; 21 &)
% ( 9 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of types : 19 ( 18 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 19 ( 17 usr; 5 prp; 0-3 aty)
% Number of functors : 115 ( 115 usr; 28 con; 0-4 aty)
% Number of variables : 104 ( 0 sgn 95 !; 9 ?; 104 :)
% 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_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29: $tType ).
tff(type_def_12,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29_29: $tType ).
tff(type_def_13,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29: $tType ).
tff(type_def_14,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29: $tType ).
tff(type_def_15,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29_29: $tType ).
tff(type_def_16,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29: $tType ).
tff(type_def_17,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29: $tType ).
tff(type_def_18,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29_29: $tType ).
tff(type_def_19,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29: $tType ).
tff(type_def_20,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29: $tType ).
tff(type_def_21,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29: $tType ).
tff(type_def_22,type,
mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29: $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,
tyop_2Epair_2Eprod: ( d * d ) > d ).
tff(func_def_4,type,
s: ( d * u ) > du ).
tff(func_def_5,type,
app_2E2: ( du * du ) > u ).
tff(func_def_6,type,
combin_i_2E0: u ).
tff(func_def_7,type,
combin_k_2E0: u ).
tff(func_def_8,type,
combin_s_2E0: u ).
tff(func_def_9,type,
c_2Ebool_2E_21_2E0: u ).
tff(func_def_10,type,
c_2Ebool_2E_21_2E1: du > u ).
tff(func_def_11,type,
c_2Ebool_2E_2F_5C_2E0: u ).
tff(func_def_12,type,
c_2Ebool_2E_2F_5C_2E2: ( du * du ) > u ).
tff(func_def_13,type,
c_2Emin_2E_3D_2E0: u ).
tff(func_def_14,type,
c_2Emin_2E_3D_2E2: ( du * du ) > u ).
tff(func_def_15,type,
c_2Emin_2E_3D_3D_3E_2E0: u ).
tff(func_def_16,type,
c_2Emin_2E_3D_3D_3E_2E2: ( du * du ) > u ).
tff(func_def_17,type,
c_2Ebool_2E_3F_2E0: u ).
tff(func_def_18,type,
c_2Ebool_2E_3F_2E1: du > u ).
tff(func_def_19,type,
c_2Epred__set_2EBIJ_2E0: u ).
tff(func_def_20,type,
c_2Epred__set_2EBIJ_2E3: ( du * du * du ) > u ).
tff(func_def_21,type,
c_2Epred__set_2ECROSS_2E0: u ).
tff(func_def_22,type,
c_2Epred__set_2ECROSS_2E2: ( du * du ) > u ).
tff(func_def_23,type,
c_2Ebool_2EF_2E0: u ).
tff(func_def_24,type,
c_2Ebool_2ET_2E0: u ).
tff(func_def_25,type,
c_2Epred__set_2EUNIV_2E0: u ).
tff(func_def_26,type,
c_2Ebool_2E_5C_2F_2E0: u ).
tff(func_def_27,type,
c_2Ebool_2E_5C_2F_2E2: ( du * du ) > u ).
tff(func_def_28,type,
c_2Ebool_2E_7E_2E0: u ).
tff(func_def_29,type,
c_2Ebool_2E_7E_2E1: du > u ).
tff(func_def_30,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_31,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_32,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool: ( mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 * mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_33,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29: ( mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29_29 * mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 ) > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_34,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29: ( mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 * mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 ) > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_35,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29: ( mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29 * mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 ) > mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_36,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29: ( mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29_29 * mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 ) > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_37,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool: ( mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 * mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29 ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_38,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29: ( mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 * mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29 ) > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_39,type,
mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29: ( mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29_29 * mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29 ) > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_40,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_41,type,
mono_2Ec_2Ebool_2E_2F_5C_2E2: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_42,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_43,type,
mono_2Ec_2Emin_2E_3D_3D_3E_2E2: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_44,type,
mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29_29 ).
tff(func_def_45,type,
mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29: ( mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 * mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 * mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29 ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_46,type,
mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29_29 ).
tff(func_def_47,type,
mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum: ( mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29 * mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29 * mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_48,type,
mono_2Ec_2Epred__set_2ECROSS_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29_29 ).
tff(func_def_49,type,
mono_2Ec_2Epred__set_2ECROSS_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum: ( mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 * mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 ) > mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_50,type,
mono_2Ec_2Ebool_2EF_2E0: mono_2Etyop_2Emin_2Ebool ).
tff(func_def_51,type,
mono_2Ec_2Ebool_2ET_2E0: mono_2Etyop_2Emin_2Ebool ).
tff(func_def_52,type,
mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_53,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_54,type,
mono_2Ec_2Ebool_2E_5C_2F_2E2: ( mono_2Etyop_2Emin_2Ebool * mono_2Etyop_2Emin_2Ebool ) > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_55,type,
mono_2Ec_2Ebool_2E_7E_2E0: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_56,type,
mono_2Ec_2Ebool_2E_7E_2E1: mono_2Etyop_2Emin_2Ebool > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_57,type,
i_mono_2Etyop_2Emin_2Ebool: mono_2Etyop_2Emin_2Ebool > u ).
tff(func_def_58,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_59,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_60,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 > u ).
tff(func_def_61,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29_29: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29_29 > u ).
tff(func_def_62,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 > u ).
tff(func_def_63,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29 > u ).
tff(func_def_64,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29_29: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29_29 > u ).
tff(func_def_65,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 > u ).
tff(func_def_66,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 > u ).
tff(func_def_67,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29_29: mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29_29 > u ).
tff(func_def_68,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_69,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 > u ).
tff(func_def_70,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29 > u ).
tff(func_def_71,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29 > u ).
tff(func_def_72,type,
j_mono_2Etyop_2Emin_2Ebool: du > mono_2Etyop_2Emin_2Ebool ).
tff(func_def_73,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_74,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_75,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_76,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29_29 ).
tff(func_def_77,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_78,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_79,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29_29 ).
tff(func_def_80,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_81,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29 ).
tff(func_def_82,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29_29 ).
tff(func_def_83,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_84,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 ).
tff(func_def_85,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29 ).
tff(func_def_86,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29: du > mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29 ).
tff(func_def_87,type,
sK12: ( d * d * u * u ) > u ).
tff(func_def_88,type,
sK13: ( d * u ) > u ).
tff(func_def_89,type,
sK14: ( d * u ) > u ).
tff(func_def_90,type,
sK15: ( d * u ) > u ).
tff(func_def_91,type,
sK16: ( d * u ) > u ).
tff(func_def_92,type,
sK17: ( d * u * mono_2Etyop_2Emin_2Ebool ) > u ).
tff(func_def_93,type,
sK18: ( d * u ) > u ).
tff(func_def_94,type,
sK19: ( d * mono_2Etyop_2Emin_2Ebool * u ) > u ).
tff(func_def_95,type,
sK20: ( d * u ) > u ).
tff(func_def_96,type,
sK21: ( d * u ) > u ).
tff(func_def_97,type,
sK22: ( d * u * mono_2Etyop_2Emin_2Ebool ) > u ).
tff(func_def_98,type,
sK23: ( d * u ) > u ).
tff(func_def_99,type,
sK24: ( d * mono_2Etyop_2Emin_2Ebool * u ) > u ).
tff(func_def_100,type,
sK25: ( d * u * mono_2Etyop_2Emin_2Ebool ) > u ).
tff(func_def_101,type,
sK26: ( d * u ) > u ).
tff(func_def_102,type,
sK27: ( d * mono_2Etyop_2Emin_2Ebool * u ) > u ).
tff(func_def_103,type,
sK28: ( d * u ) > u ).
tff(func_def_104,type,
sK29: ( d * u ) > u ).
tff(func_def_105,type,
sK30: ( d * mono_2Etyop_2Emin_2Ebool * u ) > u ).
tff(func_def_106,type,
sK31: ( d * u ) > u ).
tff(func_def_107,type,
sK32: ( d * mono_2Etyop_2Emin_2Ebool * u ) > u ).
tff(func_def_108,type,
sK33: ( d * d * u * u ) > u ).
tff(func_def_109,type,
sK34: ( d * d * u * u ) > u ).
tff(func_def_110,type,
sK35: ( d * d * u ) > u ).
tff(func_def_111,type,
sK36: ( d * d * u ) > u ).
tff(func_def_112,type,
sK37: ( d * d * u * u ) > u ).
tff(func_def_113,type,
sK38: ( d * d * u * u ) > u ).
tff(func_def_114,type,
sK39: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29 ).
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(f28,axiom,
! [X0: u] : ( s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X0)))) = s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29) ).
tff(f31,axiom,
! [X0: mono_2Etyop_2Emin_2Ebool] : ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(X0))) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Emin_2Ebool) ).
tff(f53,axiom,
! [X0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29,X2: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29] : ( mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(X0,X1,X2) = mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29,X0),X1),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29) ).
tff(f54,axiom,
! [X0: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29,X2: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29] : ( mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum(X0,X1,X2) = mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum,X0),X1),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum) ).
tff(f55,axiom,
! [X0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29] : ( mono_2Ec_2Epred__set_2ECROSS_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(X0,X1) = mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2ECROSS_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arityeq2_2Ec_2Epred__set_2ECROSS_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum) ).
tff(f69,axiom,
! [X0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29,X2: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29] : ( s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(X0,X1,X2))) = s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(X0)),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(X1)),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(X2)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',monoeq_2Emono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29) ).
tff(f71,axiom,
! [X0: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29,X2: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29] : ( s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum(X0,X1,X2))) = s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29(X0)),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(X1)),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(X2)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',monoeq_2Emono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum) ).
tff(f75,axiom,
p(mono_2Ec_2Ebool_2ET_2E0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ETRUTH) ).
tff(f77,axiom,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ( p(X0)
=> p(mono_2Ec_2Ebool_2EF_2E0) )
=> ~ p(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2EIMP__F) ).
tff(f82,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(f94,axiom,
! [X0: d,X1: d,X2: u,X3: u] :
( ? [X4: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X0,X1),X4),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
<=> ? [X5: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X1,X0),X5),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Epred__set_2EBIJ__SYM) ).
tff(f105,axiom,
? [X0: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29] : p(mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum(X0,mono_2Ec_2Epred__set_2ECROSS_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eutil__prob_2ENUM__2D__BIJ) ).
tff(f106,conjecture,
? [X0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29] : p(mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(X0,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2ECROSS_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eutil__prob_2ENUM__2D__BIJ__INV) ).
tff(f107,negated_conjecture,
~ ? [X0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29] : p(mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(X0,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2ECROSS_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum))),
inference(negated_conjecture,[status(cth)],[f106]) ).
tff(f114,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ~ p(X0)
| ( ~ p(mono_2Ec_2Ebool_2EF_2E0)
& p(X0) ) ),
inference(ennf_transformation,[],[f77]) ).
tff(f128,plain,
! [X0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29] : ~ p(mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(X0,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2ECROSS_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum))),
inference(ennf_transformation,[],[f107]) ).
tff(f176,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,[],[f82]) ).
tff(f177,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,[],[f176]) ).
tff(f218,plain,
! [X0: d,X1: d,X2: u,X3: u] :
( ( ? [X4: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X0,X1),X4),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
| ! [X5: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X1,X0),X5),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2))))) )
& ( ? [X5: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X1,X0),X5),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2)))))
| ! [X4: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X0,X1),X4),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))) ) ),
inference(nnf_transformation,[],[f94]) ).
tff(f219,plain,
! [X0: d,X1: d,X2: u,X3: u] :
( ( ? [X4: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X0,X1),X4),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
| ! [X5: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X1,X0),X5),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2))))) )
& ( ? [X6: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X1,X0),X6),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2)))))
| ! [X7: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X0,X1),X7),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))) ) ),
inference(rectify,[],[f218]) ).
tff(f220,plain,
! [X0: d,X1: d,X2: u,X3: u] :
( ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X0,X1),sK37(X0,X1,X2,X3)),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
| ! [X5: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X1,X0),X5),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2))))) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X1,X0),sK38(X0,X1,X2,X3)),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2)))))
| ! [X7: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X0,X1),X7),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3))))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37,sK38]),skolemize(X4,sK37(X0,X1,X2,X3)),skolemize(X6,sK38(X0,X1,X2,X3))],[f219]) ).
tff(f268,plain,
p(mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum(sK39,mono_2Ec_2Epred__set_2ECROSS_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39]),skolemize(X0,sK39)],[f105]) ).
tff(f307,plain,
! [X0: u] : ( s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X0) = s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X0)))) ),
inference(cnf_transformation,[],[f28]) ).
tff(f310,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] : ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(X0))) = X0 ),
inference(cnf_transformation,[],[f31]) ).
tff(f337,plain,
! [X2: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29,X0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29] : ( mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(X0,X1,X2) = mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29,X0),X1),X2) ),
inference(cnf_transformation,[],[f53]) ).
tff(f338,plain,
! [X2: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29,X0: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29] : ( mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum(X0,X1,X2) = mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum,X0),X1),X2) ),
inference(cnf_transformation,[],[f54]) ).
tff(f339,plain,
! [X0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29] : ( mono_2Ec_2Epred__set_2ECROSS_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(X0,X1) = mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2ECROSS_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum,X0),X1) ),
inference(cnf_transformation,[],[f55]) ).
tff(f356,plain,
! [X2: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29,X0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29] : ( s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(X0,X1,X2))) = s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(X0)),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(X1)),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(X2)))) ),
inference(cnf_transformation,[],[f69]) ).
tff(f358,plain,
! [X2: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29,X0: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29] : ( s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum(X0,X1,X2))) = s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29(X0)),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(X1)),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(X2)))) ),
inference(cnf_transformation,[],[f71]) ).
tff(f362,plain,
p(mono_2Ec_2Ebool_2ET_2E0),
inference(cnf_transformation,[],[f75]) ).
tff(f368,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( ~ p(X0)
| ~ p(mono_2Ec_2Ebool_2EF_2E0) ),
inference(cnf_transformation,[],[f114]) ).
tff(f394,plain,
! [X0: mono_2Etyop_2Emin_2Ebool] :
( p(X0)
| ( mono_2Ec_2Ebool_2EF_2E0 = X0 ) ),
inference(cnf_transformation,[],[f177]) ).
tff(f441,plain,
! [X2: u,X3: u,X0: d,X1: d,X7: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X0,X1),X7),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X1,X0),sK38(X0,X1,X2,X3)),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X2))))) ),
inference(cnf_transformation,[],[f220]) ).
tff(f549,plain,
p(mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum(sK39,mono_2Ec_2Epred__set_2ECROSS_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum)),
inference(cnf_transformation,[],[f268]) ).
tff(f550,plain,
! [X0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29] : ~ p(mono_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29(X0,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2ECROSS_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum(mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum))),
inference(cnf_transformation,[],[f128]) ).
tff(f551,plain,
! [X2: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29,X0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29] : ( s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(X0)),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(X1)),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(X2)))) = s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29,X0),X1),X2))) ),
inference(definition_unfolding,[],[f356,f337]) ).
tff(f552,plain,
! [X2: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29,X0: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29] : ( s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29(X0)),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(X1)),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(X2)))) = s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum,X0),X1),X2))) ),
inference(definition_unfolding,[],[f358,f338]) ).
tff(f554,plain,
p(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum,sK39),mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2ECROSS_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum)),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum)),
inference(definition_unfolding,[],[f549,f338,f339]) ).
tff(f555,plain,
! [X0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29] : ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29,X0),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum),mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2ECROSS_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum))),
inference(definition_unfolding,[],[f550,f337,f339]) ).
tff(f570,definition,
( spl40_2
<=> p(mono_2Ec_2Ebool_2EF_2E0) ),
introduced(definition,[new_symbols(definition,[spl40_2])],[avatar_definition]) ).
tff(f597,definition,
( spl40_8
<=> ! [X1: mono_2Etyop_2Emin_2Ebool] : ~ p(X1) ),
introduced(definition,[new_symbols(definition,[spl40_8])],[avatar_definition]) ).
tff(f598,plain,
( ! [X1: mono_2Etyop_2Emin_2Ebool] : ~ p(X1)
| ~ spl40_8 ),
inference(avatar_component_clause,[],[f597]) ).
tff(f625,definition,
( spl40_15
<=> p(mono_2Ec_2Ebool_2ET_2E0) ),
introduced(definition,[new_symbols(definition,[spl40_15])],[avatar_definition]) ).
tff(f627,plain,
( p(mono_2Ec_2Ebool_2ET_2E0)
| ~ spl40_15 ),
inference(avatar_component_clause,[],[f625]) ).
tff(f640,plain,
( ~ spl40_2
| spl40_8 ),
inference(avatar_split_clause,[],[f368,f597,f570]) ).
tff(f641,plain,
spl40_15,
inference(avatar_split_clause,[],[f362,f625]) ).
tff(f646,plain,
( $false
| ~ spl40_8
| ~ spl40_15 ),
inference(resolution,[],[f627,f598]) ).
tff(f647,plain,
( ~ spl40_8
| ~ spl40_15 ),
inference(avatar_contradiction_clause,[],[f646]) ).
tff(f649,plain,
! [X0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29] : ( mono_2Ec_2Ebool_2EF_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29,X0),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum),mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2ECROSS_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum)) ),
inference(resolution,[],[f394,f555]) ).
tff(f674,definition,
( spl40_19
<=> ! [X0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29] : ( mono_2Ec_2Ebool_2EF_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29,X0),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum),mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2ECROSS_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum)) ) ),
introduced(definition,[new_symbols(definition,[spl40_19])],[avatar_definition]) ).
tff(f675,plain,
( ! [X0: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29] : ( mono_2Ec_2Ebool_2EF_2E0 = mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29,X0),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum),mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2ECROSS_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum)) )
| ~ spl40_19 ),
inference(avatar_component_clause,[],[f674]) ).
tff(f684,plain,
spl40_19,
inference(avatar_split_clause,[],[f649,f674]) ).
tff(f2526,plain,
! [X2: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29,X0: u,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29] : ( s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29,j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X0))),X1),X2))) = s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(X1)),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(X2)))) ),
inference(superposition,[],[f551,f307]) ).
tff(f2909,plain,
! [X2: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29,X0: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum,X0),X1),X2)))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),sK38(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum,i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(X1),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(X2))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(X2)),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(X1)))))) ),
inference(superposition,[],[f441,f552]) ).
tff(f2915,plain,
! [X2: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29,X0: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29] :
( ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum,X0),X1),X2))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),sK38(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum,i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(X1),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(X2))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(X2)),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(X1)))))) ),
inference(forward_demodulation,[],[f2909,f310]) ).
tff(f42531,plain,
! [X2: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29,X0: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29,j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),sK38(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum,i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(X1),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(X2))))),X2),X1)))))
| ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum,X0),X1),X2)) ),
inference(forward_demodulation,[],[f2915,f2526]) ).
tff(f42532,plain,
! [X2: mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29,X0: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29,X1: mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29] :
( ~ p(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum,X0),X1),X2))
| p(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29,j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),sK38(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum,i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(X1),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(X2))))),X2),X1)) ),
inference(forward_demodulation,[],[f42531,f310]) ).
tff(f42533,plain,
p(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2EBIJ_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29,j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),sK38(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum,i_mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2ECROSS_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum)),i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29(mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum))))),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum),mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29(mono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_2Ctyop_2Emin_2Efun_28tyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_2Ctyop_2Emin_2Ebool_29_29(mono_2Ec_2Epred__set_2ECROSS_2E0_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum,mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum),mono_2Ec_2Epred__set_2EUNIV_2E0_2Emono_2Etyop_2Enum_2Enum))),
inference(resolution,[],[f42532,f554]) ).
tff(f42609,plain,
( p(mono_2Ec_2Ebool_2EF_2E0)
| ~ spl40_19 ),
inference(forward_demodulation,[],[f42533,f675]) ).
tff(f42611,plain,
( spl40_2
| ~ spl40_19 ),
inference(avatar_split_clause,[],[f42609,f674,f570]) ).
cnf(s29,plain,
( ~ spl40_2
| spl40_8 ),
inference(sat_conversion,[],[f640]) ).
cnf(s30,plain,
spl40_15,
inference(sat_conversion,[],[f641]) ).
cnf(s37,plain,
( ~ spl40_8
| ~ spl40_15 ),
inference(sat_conversion,[],[f647]) ).
cnf(s43,plain,
spl40_19,
inference(sat_conversion,[],[f684]) ).
cnf(s2990,plain,
( spl40_2
| ~ spl40_19 ),
inference(sat_conversion,[],[f42611]) ).
cnf(s3007,plain,
spl40_2,
inference(rat,[],[s2990,s43]) ).
cnf(s3049,plain,
~ spl40_8,
inference(rat,[],[s37,s30]) ).
cnf(s3109,plain,
$false,
inference(rat,[],[s29,s3049,s3007]) ).
tff(f42612,plain,
$false,
inference(avatar_sat_refutation,[],[s3109]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP020_1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39 % Computer : n014.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Sun Sep 27 12:05:46 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.42 Running first-order model finding
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.25/1.44 % (692386)Will run a generic schedule for satisfiability detection.
% 6.25/1.44 % (692394)dis+10_1_sil=32000:sp=arity:random_seed=2449988991:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.25/1.44 % (692392)% WARNING: option uhcvi not known.
% 6.25/1.44 % (692391)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2484976651_2999 on theBenchmark for (2999ds/0Mi)
% 6.25/1.44 % (692392)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=847743550:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.25/1.44 % (692393)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3538944609:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.25/1.44 % (692395)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1671070799:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.25/1.44 % (692397)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=44618872:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.25/1.44 % (692396)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3034871496:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.25/1.44 % (692394)Instruction limit reached!
% 6.25/1.44 % (692394)------------------------------
% 6.25/1.44 % (692394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.25/1.44 % (692394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.44 % (692394)CaDiCaL version: 2.1.3
% 6.25/1.44 % (692394)Termination reason: Instruction limit
% 6.25/1.44 % (692394)Termination phase: Saturation
% 6.25/1.44 % (692394)Time elapsed: 0.030 s
% 6.25/1.44 % (692394)Peak memory usage: 12 MB
% 6.25/1.44 % (692394)Instructions burned: 105 (million)
% 6.25/1.44 % (692405)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=348597879:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.25/1.44 % (692395)Instruction limit reached!
% 6.25/1.44 % (692395)------------------------------
% 6.25/1.44 % (692395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.25/1.44 % (692395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.44 % (692395)CaDiCaL version: 2.1.3
% 6.25/1.44 % (692395)Termination reason: Instruction limit
% 6.25/1.44 % (692395)Termination phase: Saturation
% 6.25/1.44 % (692395)Time elapsed: 0.065 s
% 6.25/1.44 % (692395)Peak memory usage: 13 MB
% 6.25/1.44 % (692395)Instructions burned: 116 (million)
% 6.25/1.44 % (692396)Instruction limit reached!
% 6.25/1.44 % (692396)------------------------------
% 6.25/1.44 % (692396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.25/1.44 % (692396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.44 % (692396)CaDiCaL version: 2.1.3
% 6.25/1.44 % (692396)Termination reason: Instruction limit
% 6.25/1.44 % (692396)Termination phase: Saturation
% 6.25/1.44 % (692396)Time elapsed: 0.073 s
% 6.25/1.44 % (692396)Peak memory usage: 13 MB
% 6.25/1.44 % (692396)Instructions burned: 132 (million)
% 6.25/1.44 % (692407)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=268975530:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 6.25/1.44 % TRYING [1]
% 6.25/1.44 % TRYING [2]
% 6.25/1.44 % (692408)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3930111610:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.25/1.44 % TRYING [3]
% 6.25/1.44 % (692397)Instruction limit reached!
% 6.25/1.44 % (692397)------------------------------
% 6.25/1.44 % (692397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.25/1.44 % (692397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.44 % (692397)CaDiCaL version: 2.1.3
% 6.25/1.44 % (692397)Termination reason: Instruction limit
% 6.25/1.44 % (692397)Termination phase: Saturation
% 6.25/1.44 % (692397)Time elapsed: 0.124 s
% 6.25/1.44 % (692397)Peak memory usage: 13 MB
% 6.25/1.44 % (692397)Instructions burned: 159 (million)
% 6.25/1.44 % (692411)ott-21_1_sil=16000:fs=off:random_seed=4206224682:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.25/1.44 % (692407)Instruction limit reached!
% 6.25/1.44 % (692407)------------------------------
% 6.25/1.44 % (692407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.25/1.44 % (692407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/1.44 % (692407)CaDiCaL version: 2.1.3
% 8.53/1.90 % (692407)Termination reason: Instruction limit
% 8.53/1.90 % (692407)Termination phase: Saturation
% 8.53/1.90 % (692407)Time elapsed: 0.072 s
% 8.53/1.90 % (692407)Peak memory usage: 13 MB
% 8.53/1.90 % (692407)Instructions burned: 131 (million)
% 8.53/1.90 % (692413)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2245537445:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 8.53/1.90 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % Detected maximum model sizes of [max,max,2,max,max,max,max,max,max,max,max,max,max,max,max,max,max]
% 8.53/1.90 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [1,1,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [1,1,2,3,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % (692405)Instruction limit reached!
% 8.53/1.90 % (692405)------------------------------
% 8.53/1.90 % (692405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.53/1.90 % (692405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.53/1.90 % (692405)CaDiCaL version: 2.1.3
% 8.53/1.90 % (692405)Termination reason: Instruction limit
% 8.53/1.90 % (692405)Termination phase: Finite model building SAT solving
% 8.53/1.90 % (692405)Time elapsed: 0.169 s
% 8.53/1.90 % (692405)Peak memory usage: 44 MB
% 8.53/1.90 % (692405)Instructions burned: 714 (million)
% 8.53/1.90 % TRYING [1,1,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [1,1,2,3,2,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [1,1,2,4,2,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % (692415)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1148066573:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 8.53/1.90 % TRYING [1,1,2,3,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [1,1,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [2,1,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [1,2,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [2,2,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % (692411)Instruction limit reached!
% 8.53/1.90 % (692411)------------------------------
% 8.53/1.90 % (692411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.53/1.90 % (692411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.53/1.90 % (692411)CaDiCaL version: 2.1.3
% 8.53/1.90 % (692411)Termination reason: Instruction limit
% 8.53/1.90 % (692411)Termination phase: Saturation
% 8.53/1.90 % (692411)Time elapsed: 0.122 s
% 8.53/1.90 % (692411)Peak memory usage: 13 MB
% 8.53/1.90 % (692411)Instructions burned: 180 (million)
% 8.53/1.90 % (692417)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3544005154:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 8.53/1.90 % TRYING [1,3,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [2,3,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % Detected maximum model sizes of [max,max,2,max,max,max,max,max,max,max,max,max,max,max,max,max,max]
% 8.53/1.90 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [1,1,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [1,1,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [1,1,2,3,2,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [1,1,2,3,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [1,1,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [2,1,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [1,2,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [1,4,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [2,2,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % TRYING [3,1,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 8.53/1.90 % (692415)Instruction limit reached!
% 8.53/1.90 % (692415)------------------------------
% 8.53/1.90 % (692415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.53/1.90 % (692415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.53/1.90 % (692415)CaDiCaL version: 2.1.3
% 8.53/1.90 % (692415)Termination reason: Instruction limit
% 8.53/1.90 % (692415)Termination phase: Finite model building SAT solving
% 8.53/1.90 % (692415)Time elapsed: 0.197 s
% 8.53/1.90 % (692415)Peak memory usage: 19 MB
% 8.53/1.90 % (692415)Instructions burned: 866 (million)
% 8.53/1.90 % (692408)Instruction limit reached!
% 8.53/1.90 % (692408)------------------------------
% 8.53/1.90 % (692408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.53/1.90 % (692408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.53/1.90 % (692408)CaDiCaL version: 2.1.3
% 8.53/1.90 % (692408)Termination reason: Instruction limit
% 8.53/1.90 % (692408)Termination phase: Saturation
% 24.55/4.03 % (692408)Time elapsed: 0.327 s
% 24.55/4.03 % (692408)Peak memory usage: 16 MB
% 24.55/4.03 % (692408)Instructions burned: 685 (million)
% 24.55/4.03 % (692419)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=174182399:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 24.55/4.03 % (692421)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3405452522:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 24.55/4.03 % (692413)Instruction limit reached!
% 24.55/4.03 % (692413)------------------------------
% 24.55/4.03 % (692413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.55/4.03 % TRYING [2,4,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % (692413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.55/4.03 % (692413)CaDiCaL version: 2.1.3
% 24.55/4.03 % (692413)Termination reason: Instruction limit
% 24.55/4.03 % (692413)Termination phase: Saturation
% 24.55/4.03 % (692413)Time elapsed: 0.278 s
% 24.55/4.03 % (692413)Peak memory usage: 14 MB
% 24.55/4.03 % (692413)Instructions burned: 478 (million)
% 24.55/4.03 % (692423)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3668181940:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 24.55/4.03 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % Detected maximum model sizes of [max,max,2,max,max,max,max,max,max,max,max,max,max,max,max,max,max]
% 24.55/4.03 % fmb_start_size (= 14) larger than a detected sort maximum size!
% 24.55/4.03 % (692419)Refutation not found, incomplete strategy
% 24.55/4.03 % (692419)------------------------------
% 24.55/4.03 % (692419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.55/4.03 % (692419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.55/4.03 % (692419)CaDiCaL version: 2.1.3
% 24.55/4.03 % (692419)Termination reason: Refutation not found, incomplete strategy
% 24.55/4.03 % (692419)Time elapsed: 0.098 s
% 24.55/4.03 % (692419)Peak memory usage: 16 MB
% 24.55/4.03 % (692419)Instructions burned: 423 (million)
% 24.55/4.03 % (692419)------------------------------
% 24.55/4.03 % (692419)------------------------------
% 24.55/4.03 % (692425)fmb+10_1_sil=64000:random_seed=3471183604:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 24.55/4.03 % TRYING [1,5,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % TRYING [3,2,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % Detected maximum model sizes of [max,max,2,max,max,max,max,max,max,max,max,max,max,max,max,max,max]
% 24.55/4.03 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % TRYING [1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % TRYING [1,1,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % TRYING [1,1,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % TRYING [1,1,2,3,2,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % TRYING [1,1,2,3,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % TRYING [1,1,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % TRYING [2,1,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % TRYING [1,2,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % TRYING [2,2,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % TRYING [1,3,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % TRYING [2,5,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % TRYING [2,3,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % (692421)Instruction limit reached!
% 24.55/4.03 % (692421)------------------------------
% 24.55/4.03 % (692421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.55/4.03 % (692421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.55/4.03 % (692421)CaDiCaL version: 2.1.3
% 24.55/4.03 % (692421)Termination reason: Instruction limit
% 24.55/4.03 % (692421)Termination phase: Saturation
% 24.55/4.03 % (692421)Time elapsed: 0.378 s
% 24.55/4.03 % (692421)Peak memory usage: 18 MB
% 24.55/4.03 % (692421)Instructions burned: 693 (million)
% 24.55/4.03 % (692427)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1789906917:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 24.55/4.03 % TRYING [1,4,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % TRYING [3,1,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 24.55/4.03 % (692423)Instruction limit reached!
% 24.55/4.03 % (692423)------------------------------
% 24.55/4.03 % (692423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.55/4.03 % (692423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.55/4.03 % (692423)CaDiCaL version: 2.1.3
% 24.55/4.03 % (692423)Termination reason: Instruction limit
% 24.55/4.03 % (692423)Termination phase: Saturation
% 49.42/7.40 % (692423)Time elapsed: 0.487 s
% 49.42/7.40 % (692423)Peak memory usage: 20 MB
% 49.42/7.40 % (692423)Instructions burned: 880 (million)
% 49.42/7.40 % (692417)Instruction limit reached!
% 49.42/7.40 % (692417)------------------------------
% 49.42/7.40 % (692417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.42/7.40 % (692417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.42/7.40 % (692417)CaDiCaL version: 2.1.3
% 49.42/7.40 % (692417)Termination reason: Instruction limit
% 49.42/7.40 % (692417)Termination phase: Saturation
% 49.42/7.40 % (692417)Time elapsed: 0.681 s
% 49.42/7.40 % (692417)Peak memory usage: 23 MB
% 49.42/7.40 % (692417)Instructions burned: 1180 (million)
% 49.42/7.40 % (692429)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2082726806:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 49.42/7.40 % (692430)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2121304378:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 49.42/7.40 % TRYING [2,4,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 49.42/7.40 % TRYING [1,6,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 49.42/7.40 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 49.42/7.41 % Detected maximum model sizes of [max,max,2,max,max,max,max,max,max,max,max,max,max,max,max,max,max]
% 49.42/7.41 % fmb_start_size (= 20) larger than a detected sort maximum size!
% 49.42/7.41 % (692427)Refutation not found, incomplete strategy
% 49.42/7.41 % (692427)------------------------------
% 49.42/7.41 % (692427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.42/7.41 % (692427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.42/7.41 % (692427)CaDiCaL version: 2.1.3
% 49.42/7.41 % (692427)Termination reason: Refutation not found, incomplete strategy
% 49.42/7.41 % (692427)Time elapsed: 0.189 s
% 49.42/7.41 % (692427)Peak memory usage: 15 MB
% 49.42/7.41 % (692427)Instructions burned: 424 (million)
% 49.42/7.41 % (692427)------------------------------
% 49.42/7.41 % (692427)------------------------------
% 49.42/7.41 % (692433)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2027068967:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi)
% 49.42/7.41 % TRYING [3,3,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 49.42/7.41 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 49.42/7.41 % Detected maximum model sizes of [max,max,2,max,max,max,max,max,max,max,max,max,max,max,max,max,max]
% 49.42/7.41 % fmb_start_size (= 8) larger than a detected sort maximum size!
% 49.42/7.41 % (692429)Refutation not found, incomplete strategy
% 49.42/7.41 % (692429)------------------------------
% 49.42/7.41 % (692429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.42/7.41 % (692429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.42/7.41 % (692429)CaDiCaL version: 2.1.3
% 49.42/7.41 % (692429)Termination reason: Refutation not found, incomplete strategy
% 49.42/7.41 % (692429)Time elapsed: 0.185 s
% 49.42/7.41 % (692429)Peak memory usage: 15 MB
% 49.42/7.41 % (692429)Instructions burned: 423 (million)
% 49.42/7.41 % (692429)------------------------------
% 49.42/7.41 % (692429)------------------------------
% 49.42/7.41 % TRYING [1,5,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 49.42/7.41 % (692435)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2925362127:i=6324_2987 on theBenchmark for (2987ds/6324Mi)
% 49.42/7.41 % TRYING [3,2,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 49.42/7.41 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 49.42/7.41 % Detected maximum model sizes of [max,max,2,max,max,max,max,max,max,max,max,max,max,max,max,max,max]
% 49.42/7.41 % fmb_start_size (= 77) larger than a detected sort maximum size!
% 49.42/7.41 % (692435)Refutation not found, incomplete strategy
% 49.42/7.41 % (692435)------------------------------
% 49.42/7.41 % (692435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.42/7.41 % (692435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.42/7.41 % (692435)CaDiCaL version: 2.1.3
% 49.42/7.41 % (692435)Termination reason: Refutation not found, incomplete strategy
% 49.42/7.41 % (692435)Time elapsed: 0.187 s
% 49.42/7.41 % (692435)Peak memory usage: 16 MB
% 49.42/7.41 % (692435)Instructions burned: 423 (million)
% 49.42/7.41 % (692435)------------------------------
% 49.42/7.41 % (692435)------------------------------
% 49.42/7.41 % (692437)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3213271688:fmbsr=2.30978:i=2174_2985 on theBenchmark for (2985ds/2174Mi)
% 49.42/7.41 % TRYING [2,5,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [2,6,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [16]
% 129.71/18.73 % TRYING [1,6,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % (692433)Instruction limit reached!
% 129.71/18.73 % (692433)------------------------------
% 129.71/18.73 % (692433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.71/18.73 % (692433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.71/18.73 % (692433)CaDiCaL version: 2.1.3
% 129.71/18.73 % (692433)Termination reason: Instruction limit
% 129.71/18.73 % (692433)Termination phase: Saturation
% 129.71/18.73 % (692433)Time elapsed: 0.702 s
% 129.71/18.73 % (692433)Peak memory usage: 19 MB
% 129.71/18.73 % (692433)Instructions burned: 1474 (million)
% 129.71/18.73 % (692439)ott-2_1_sil=16000:newcnf=on:random_seed=1560892668:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2981 on theBenchmark for (2981ds/869Mi)
% 129.71/18.73 % TRYING [3,3,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % (692437)Instruction limit reached!
% 129.71/18.73 % (692437)------------------------------
% 129.71/18.73 % (692437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.71/18.73 % (692437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.71/18.73 % (692437)CaDiCaL version: 2.1.3
% 129.71/18.73 % (692437)Termination reason: Instruction limit
% 129.71/18.73 % (692437)Termination phase: Finite model building constraint generation
% 129.71/18.73 % (692437)Time elapsed: 0.768 s
% 129.71/18.73 % (692437)Peak memory usage: 129 MB
% 129.71/18.73 % (692437)Instructions burned: 2175 (million)
% 129.71/18.73 % (692439)Instruction limit reached!
% 129.71/18.73 % (692439)------------------------------
% 129.71/18.73 % (692439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.71/18.73 % (692439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.71/18.73 % (692439)CaDiCaL version: 2.1.3
% 129.71/18.73 % (692439)Termination reason: Instruction limit
% 129.71/18.73 % (692439)Termination phase: Saturation
% 129.71/18.73 % (692439)Time elapsed: 0.405 s
% 129.71/18.73 % (692439)Peak memory usage: 15 MB
% 129.71/18.73 % (692439)Instructions burned: 869 (million)
% 129.71/18.73 % (692442)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=173361204:i=54282_2977 on theBenchmark for (2977ds/54282Mi)
% 129.71/18.73 % (692441)ott+10_1_sil=32000:tgt=ground:random_seed=623605463:i=5114:av=off_2977 on theBenchmark for (2977ds/5114Mi)
% 129.71/18.73 % TRYING [1,7,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [2,6,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [4,1,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % Detected maximum model sizes of [max,max,2,max,max,max,max,max,max,max,max,max,max,max,max,max,max]
% 129.71/18.73 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [1,1,2,2,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [1,1,2,3,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [1,1,2,2,2,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [1,1,2,3,2,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [1,1,2,4,2,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [1,1,2,3,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [1,1,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [2,1,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [1,2,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [2,2,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [1,3,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [2,7,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [2,3,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [1,4,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [3,1,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [2,4,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [1,5,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [1,7,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [3,2,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [4,1,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [2,5,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [1,6,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [2,7,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [1,8,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [3,3,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % TRYING [3,4,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 129.71/18.73 % (692430)Instruction limit reached!
% 129.71/18.73 % (692430)------------------------------
% 129.71/18.73 % (692430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.71/18.73 % (692430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.71/18.73 % (692430)CaDiCaL version: 2.1.3
% 129.71/18.73 % (692430)Termination reason: Instruction limit
% 129.71/18.73 % (692430)Termination phase: Saturation
% 202.21/29.02 % (692430)Time elapsed: 2.556 s
% 202.21/29.02 % (692430)Peak memory usage: 33 MB
% 202.21/29.02 % (692430)Instructions burned: 5133 (million)
% 202.21/29.02 % (692445)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3502001113:i=3512:aac=none_2963 on theBenchmark for (2963ds/3512Mi)
% 202.21/29.02 % TRYING [2,6,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 202.21/29.02 % TRYING [4,2,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 202.21/29.02 % TRYING [1,8,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 202.21/29.02 % TRYING [4,2,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 202.21/29.02 % TRYING [1,7,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 202.21/29.02 % TRYING [2,8,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 202.21/29.02 % TRYING [4,1,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 202.21/29.02 % TRYING [2,7,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 202.21/29.02 % (692441)Instruction limit reached!
% 202.21/29.02 % (692441)------------------------------
% 202.21/29.02 % (692441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.21/29.02 % (692441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.21/29.02 % (692441)CaDiCaL version: 2.1.3
% 202.21/29.02 % (692441)Termination reason: Instruction limit
% 202.21/29.02 % (692441)Termination phase: Saturation
% 202.21/29.02 % (692441)Time elapsed: 2.770 s
% 202.21/29.02 % (692441)Peak memory usage: 40 MB
% 202.21/29.02 % (692441)Instructions burned: 5114 (million)
% 202.21/29.02 % (692447)dis+21_1_sil=32000:sas=cadical:random_seed=253783334:i=3773:amm=off_2949 on theBenchmark for (2949ds/3773Mi)
% 202.21/29.02 % TRYING [3,4,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 202.21/29.02 % (692445)Instruction limit reached!
% 202.21/29.02 % (692445)------------------------------
% 202.21/29.02 % (692445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.21/29.02 % (692445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.21/29.02 % (692445)CaDiCaL version: 2.1.3
% 202.21/29.02 % (692445)Termination reason: Instruction limit
% 202.21/29.02 % (692445)Termination phase: Saturation
% 202.21/29.02 % (692445)Time elapsed: 1.750 s
% 202.21/29.02 % (692445)Peak memory usage: 28 MB
% 202.21/29.02 % (692445)Instructions burned: 3513 (million)
% 202.21/29.02 % (692449)ott+11_1_sil=16000:gs=on:random_seed=62217619:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2946 on theBenchmark for (2946ds/2251Mi)
% 202.21/29.02 % (692425)Instruction limit reached!
% 202.21/29.02 % (692425)------------------------------
% 202.21/29.02 % (692425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.21/29.02 % (692425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.21/29.02 % (692425)CaDiCaL version: 2.1.3
% 202.21/29.02 % (692425)Termination reason: Instruction limit
% 202.21/29.02 % (692425)Termination phase: Finite model building SAT solving
% 202.21/29.02 % (692425)Time elapsed: 5.005 s
% 202.21/29.02 % (692425)Peak memory usage: 117 MB
% 202.21/29.02 % (692425)Instructions burned: 22063 (million)
% 202.21/29.02 % (692451)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=288525078:fmbsr=1.6:i=67534_2944 on theBenchmark for (2944ds/67534Mi)
% 202.21/29.02 % TRYING [1,8,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 202.21/29.02 % TRYING [3,4,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 202.21/29.02 % TRYING [1,9,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 202.21/29.02 % TRYING [4,3,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 202.21/29.02 % TRYING [4,2,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 202.21/29.02 % (692449)Instruction limit reached!
% 202.21/29.02 % (692449)------------------------------
% 202.21/29.02 % (692449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.21/29.02 % (692449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.21/29.02 % (692449)CaDiCaL version: 2.1.3
% 202.21/29.02 % (692449)Termination reason: Instruction limit
% 202.21/29.02 % (692449)Termination phase: Saturation
% 202.21/29.02 % (692449)Time elapsed: 1.038 s
% 202.21/29.02 % (692449)Peak memory usage: 17 MB
% 202.21/29.02 % (692449)Instructions burned: 2251 (million)
% 202.21/29.02 % TRYING [7]
% 202.21/29.02 % (692453)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=764095958:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2935 on theBenchmark for (2935ds/4591Mi)
% 202.21/29.02 % TRYING [2,8,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 202.21/29.02 % (692447)Instruction limit reached!
% 202.21/29.02 % (692447)------------------------------
% 202.21/29.02 % (692447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.21/29.02 % (692447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.21/29.02 % (692447)CaDiCaL version: 2.1.3
% 202.21/29.02 % (692447)Termination reason: Instruction limit
% 202.21/29.02 % (692447)Termination phase: Saturation
% 202.21/29.02 % (692447)Time elapsed: 1.931 s
% 202.21/29.02 % (692447)Peak memory usage: 31 MB
% 98.87/29.45 % (692447)Instructions burned: 3774 (million)
% 98.87/29.45 % (692455)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3450428325:i=29340_2930 on theBenchmark for (2930ds/29340Mi)
% 98.87/29.45 % TRYING [3,3,2,5,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [4,3,2,5,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [1,9,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [4,3,2,4,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [3,3,2,5,4,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % (692453)Instruction limit reached!
% 98.87/29.45 % (692453)------------------------------
% 98.87/29.45 % (692453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.87/29.45 % (692453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.87/29.45 % (692453)CaDiCaL version: 2.1.3
% 98.87/29.45 % (692453)Termination reason: Instruction limit
% 98.87/29.45 % (692453)Termination phase: Saturation
% 98.87/29.45 % (692453)Time elapsed: 2.019 s
% 98.87/29.45 % (692453)Peak memory usage: 31 MB
% 98.87/29.45 % (692453)Instructions burned: 4594 (million)
% 98.87/29.45 % (692457)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2671764285:i=5211_2915 on theBenchmark for (2915ds/5211Mi)
% 98.87/29.45 % TRYING [4,3,2,5,4,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [3,3,2,5,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [4,3,2,5,3,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [3,3,2,5,5,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [4,3,2,5,5,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [3,3,2,5,4,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % (692457)Instruction limit reached!
% 98.87/29.45 % (692457)------------------------------
% 98.87/29.45 % (692457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.87/29.45 % (692457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.87/29.45 % (692457)CaDiCaL version: 2.1.3
% 98.87/29.45 % (692457)Termination reason: Instruction limit
% 98.87/29.45 % (692457)Termination phase: Saturation
% 98.87/29.45 % (692457)Time elapsed: 2.541 s
% 98.87/29.45 % (692457)Peak memory usage: 49 MB
% 98.87/29.45 % (692457)Instructions burned: 5212 (million)
% 98.87/29.45 % TRYING [4,3,2,5,4,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % (692464)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2150771101:i=5497:nm=2_2889 on theBenchmark for (2889ds/5497Mi)
% 98.87/29.45 % TRYING [3,3,2,5,6,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % Detected maximum model sizes of [max,max,2,max,max,max,max,max,max,max,max,max,max,max,max,max,max]
% 98.87/29.45 % fmb_start_size (= 17) larger than a detected sort maximum size!
% 98.87/29.45 % (692464)Refutation not found, incomplete strategy
% 98.87/29.45 % (692464)------------------------------
% 98.87/29.45 % (692464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.87/29.45 % (692464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.87/29.45 % (692464)CaDiCaL version: 2.1.3
% 98.87/29.45 % (692464)Termination reason: Refutation not found, incomplete strategy
% 98.87/29.45 % (692464)Time elapsed: 0.192 s
% 98.87/29.45 % (692464)Peak memory usage: 16 MB
% 98.87/29.45 % (692464)Instructions burned: 427 (million)
% 98.87/29.45 % (692464)------------------------------
% 98.87/29.45 % (692464)------------------------------
% 98.87/29.45 % (692466)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=450085484:fmbsr=2:i=46332_2887 on theBenchmark for (2887ds/46332Mi)
% 98.87/29.45 % TRYING [15]
% 98.87/29.45 % TRYING [4,3,2,5,6,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [3,3,2,5,5,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [4,3,2,5,5,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [3,3,2,5,7,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [4,3,2,5,7,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [3,3,2,5,6,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [4,3,2,5,6,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [3,3,2,5,8,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [4,3,2,5,8,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [3,3,2,5,7,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [4,3,2,5,7,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [3,3,2,5,9,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [4,3,2,5,9,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [3,3,2,5,8,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [4,3,2,5,8,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [3,3,2,5,10,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [4,3,2,5,10,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [3,3,2,5,9,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % TRYING [4,3,2,5,9,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.45 % (692455)Instruction limit reached!
% 98.87/29.45 % (692455)------------------------------
% 98.87/29.45 % (692455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.87/29.45 % (692455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.87/29.46 % (692455)CaDiCaL version: 2.1.3
% 98.87/29.46 % (692455)Termination reason: Instruction limit
% 98.87/29.46 % (692455)Termination phase: Saturation
% 98.87/29.46 % (692455)Time elapsed: 11.300 s
% 98.87/29.46 % (692455)Peak memory usage: 109 MB
% 98.87/29.46 % (692455)Instructions burned: 29342 (million)
% 98.87/29.46 % (692468)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2500787628:i=14071_2816 on theBenchmark for (2816ds/14071Mi)
% 98.87/29.46 % TRYING [3,3,2,5,11,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % Detected maximum model sizes of [max,max,2,max,max,max,max,max,max,max,max,max,max,max,max,max,max]
% 98.87/29.46 % fmb_start_size (= 12) larger than a detected sort maximum size!
% 98.87/29.46 % (692468)Refutation not found, incomplete strategy
% 98.87/29.46 % (692468)------------------------------
% 98.87/29.46 % (692468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.87/29.46 % (692468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.87/29.46 % (692468)CaDiCaL version: 2.1.3
% 98.87/29.46 % (692468)Termination reason: Refutation not found, incomplete strategy
% 98.87/29.46 % (692468)Time elapsed: 0.189 s
% 98.87/29.46 % (692468)Peak memory usage: 15 MB
% 98.87/29.46 % (692468)Instructions burned: 423 (million)
% 98.87/29.46 % (692468)------------------------------
% 98.87/29.46 % (692468)------------------------------
% 98.87/29.46 % (692470)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=164217303:i=22565:add=on:rawr=on_2814 on theBenchmark for (2814ds/22565Mi)
% 98.87/29.46 % TRYING [4,3,2,5,11,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [3,3,2,5,10,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [4,3,2,5,10,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [3,3,2,5,12,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [4,3,2,5,12,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [3,3,2,5,11,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [4,3,2,5,11,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [3,3,2,5,13,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % (692451)Instruction limit reached!
% 98.87/29.46 % (692451)------------------------------
% 98.87/29.46 % (692451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.87/29.46 % (692451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.87/29.46 % (692451)CaDiCaL version: 2.1.3
% 98.87/29.46 % (692451)Termination reason: Instruction limit
% 98.87/29.46 % (692451)Termination phase: Finite model building constraint generation
% 98.87/29.46 % (692451)Time elapsed: 16.532 s
% 98.87/29.46 % (692451)Peak memory usage: 3409 MB
% 98.87/29.46 % (692451)Instructions burned: 67534 (million)
% 98.87/29.46 % TRYING [4,3,2,5,13,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % (692651)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2027653185:i=8173:av=off_2773 on theBenchmark for (2773ds/8173Mi)
% 98.87/29.46 % TRYING [3,3,2,5,12,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [4,3,2,5,12,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [3,3,2,5,14,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [3,3,2,5,13,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [4,3,2,5,13,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [4,3,2,5,14,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [3,3,2,5,14,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [4,3,2,5,14,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [3,3,2,5,15,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [3,3,2,5,15,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % TRYING [4,3,2,5,15,1,1,1,1,1,1,1,1,1,1,1,1]
% 98.87/29.46 % (692442)Instruction limit reached!
% 98.87/29.46 % (692442)------------------------------
% 98.87/29.46 % (692442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.87/29.46 % (692442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.87/29.46 % (692442)CaDiCaL version: 2.1.3
% 98.87/29.46 % (692442)Termination reason: Instruction limit
% 98.87/29.46 % (692442)Termination phase: Finite model building constraint generation
% 98.87/29.46 % (692442)Time elapsed: 25.094 s
% 98.87/29.46 % (692442)Peak memory usage: 199 MB
% 98.87/29.46 % (692442)Instructions burned: 54285 (million)
% 98.87/29.46 % (692786)dis+10_16:1_sil=16000:random_seed=3176283211:i=9155:fsr=off_2726 on theBenchmark for (2726ds/9155Mi)
% 98.87/29.46 % (692651)Instruction limit reached!
% 98.87/29.46 % (692651)------------------------------
% 98.87/29.46 % (692651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.87/29.46 % (692651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.87/29.46 % (692651)CaDiCaL version: 2.1.3
% 98.87/29.46 % (692651)Termination reason: Instruction limit
% 98.87/29.46 % (692651)Termination phase: Saturation
% 98.87/29.46 % (692651)Time elapsed: 5.850 s
% 98.87/29.46 % (692651)Peak memory usage: 44 MB
% 98.87/29.46 % (692651)Instructions burned: 8174 (million)
% 98.87/29.46 % (692786) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-692386-692786"...
% 98.87/29.46 % (692808)ott-3_8_sil=64000:random_seed=425642020:i=20139:bs=on_2714 on theBenchmark for (2714ds/20139Mi)
% 98.87/29.46 % (692786)...printing done.
% 98.87/29.46 % (692786)Refutation found. Thanks to Tanya!
% 98.87/29.46 % SZS status Theorem for theBenchmark
% 98.87/29.46 % SZS output start Proof for theBenchmark
% See solution above
% 98.87/29.46 % (692786)------------------------------
% 98.87/29.46 % (692786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.87/29.46 % (692786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.87/29.46 % (692786)CaDiCaL version: 2.1.3
% 98.87/29.46 % (692786)Termination reason: Refutation
% 98.87/29.46 % (692786)Time elapsed: 1.241 s
% 98.87/29.46 % (692786)Peak memory usage: 28 MB
% 98.87/29.46 % (692786)Instructions burned: 2785 (million)
% 98.87/29.46 % (692386)Success in time 29.026 s
% 98.87/29.46 % Vampire exiting
%------------------------------------------------------------------------------