%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP397_1 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:33:47 AM UTC 2026
% Result : Theorem 25.64s 4.56s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 44
% Syntax : Number of formulae : 248 ( 81 unt; 0 typ; 6 def)
% Number of atoms : 569 ( 321 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 570 ( 249 ~; 240 |; 48 &)
% ( 14 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of FOOLs : 1 ( 1 fml; 0 var)
% Number of types : 71 ( 70 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 69 ( 67 usr; 7 prp; 0-2 aty)
% Number of functors : 313 ( 313 usr; 35 con; 0-4 aty)
% Number of variables : 400 ( 0 sgn 369 !; 31 ?; 400 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$': $tType ).
tff(type_def_6,type,
'A_ell2_a_ell2_cblinfun$': $tType ).
tff(type_def_7,type,
'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_8,type,
'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$': $tType ).
tff(type_def_9,type,
'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_10,type,
'B_ell2_b_ell2_cblinfun$': $tType ).
tff(type_def_11,type,
'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$': $tType ).
tff(type_def_12,type,
'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_13,type,
'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_14,type,
'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_15,type,
'Nat_set_nat_fun$': $tType ).
tff(type_def_16,type,
'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$': $tType ).
tff(type_def_17,type,
'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$': $tType ).
tff(type_def_18,type,
'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_19,type,
'Nat_nat_fun_set$': $tType ).
tff(type_def_20,type,
'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$': $tType ).
tff(type_def_21,type,
'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_22,type,
'C_ell2_c_ell2_cblinfun$': $tType ).
tff(type_def_23,type,
'C_ell2_c_ell2_cblinfun_bool_fun$': $tType ).
tff(type_def_24,type,
'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_25,type,
'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_26,type,
'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_27,type,
'Nat_nat_fun_nat_nat_fun_fun$': $tType ).
tff(type_def_28,type,
'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_29,type,
'Nat_nat_fun$': $tType ).
tff(type_def_30,type,
'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$': $tType ).
tff(type_def_31,type,
'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_32,type,
'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$': $tType ).
tff(type_def_33,type,
'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_34,type,
'Nat$': $tType ).
tff(type_def_35,type,
'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$': $tType ).
tff(type_def_36,type,
'A_ell2_a_ell2_cblinfun_bool_fun$': $tType ).
tff(type_def_37,type,
'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_38,type,
'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_39,type,
'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_40,type,
'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$': $tType ).
tff(type_def_41,type,
'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_42,type,
'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$': $tType ).
tff(type_def_43,type,
'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$': $tType ).
tff(type_def_44,type,
'B_ell2_b_ell2_cblinfun_set$': $tType ).
tff(type_def_45,type,
'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_46,type,
'A_ell2_a_ell2_cblinfun_set$': $tType ).
tff(type_def_47,type,
'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_48,type,
'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_49,type,
'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_50,type,
'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_51,type,
'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$': $tType ).
tff(type_def_52,type,
'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_53,type,
'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_54,type,
'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_55,type,
'C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$': $tType ).
tff(type_def_56,type,
'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$': $tType ).
tff(type_def_57,type,
'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$': $tType ).
tff(type_def_58,type,
'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_59,type,
'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$': $tType ).
tff(type_def_60,type,
'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$': $tType ).
tff(type_def_61,type,
'A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$': $tType ).
tff(type_def_62,type,
'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_63,type,
'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$': $tType ).
tff(type_def_64,type,
'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_65,type,
'B_ell2_b_ell2_cblinfun_bool_fun$': $tType ).
tff(type_def_66,type,
'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_67,type,
'Nat_set$': $tType ).
tff(type_def_68,type,
'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_69,type,
'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$': $tType ).
tff(type_def_70,type,
'C_ell2_c_ell2_cblinfun_set$': $tType ).
tff(type_def_71,type,
'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_72,type,
'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_73,type,
'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$': $tType ).
tff(type_def_74,type,
'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$': $tType ).
tff(func_def_0,type,
'top$i': 'C_ell2_c_ell2_cblinfun_bool_fun$' ).
tff(func_def_1,type,
'register_tensor$v': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_2,type,
'image$b': ( 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > 'C_ell2_c_ell2_cblinfun_set$' ).
tff(func_def_3,type,
'inv_into$n': ( 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$' * 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ) > 'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_4,type,
'comp$af': ( 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' * 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff(func_def_5,type,
'inv_into$d': ( 'Nat_set$' * 'Nat_nat_fun$' ) > 'Nat_nat_fun$' ).
tff(func_def_6,type,
'image$': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > 'C_ell2_c_ell2_cblinfun_set$' ).
tff(func_def_7,type,
'register_tensor$f': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff(func_def_8,type,
'inv_into$': ( 'A_ell2_a_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_9,type,
'fun_app$o': ( 'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > 'A_ell2_a_ell2_cblinfun_set$' ).
tff(func_def_10,type,
'fun_app$k': ( 'Nat_nat_fun_nat_nat_fun_fun$' * 'Nat_nat_fun$' ) > 'Nat_nat_fun$' ).
tff(func_def_11,type,
'inv_into$b': ( 'A_ell2_a_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_12,type,
'fun_app$b': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_13,type,
'register_tensor$h': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_14,type,
'image$h': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > 'A_ell2_a_ell2_cblinfun_set$' ).
tff(func_def_15,type,
'top$d': 'B_ell2_b_ell2_cblinfun_bool_fun$' ).
tff(func_def_16,type,
'comp$h': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_17,type,
'comp$p': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_18,type,
'inv_into$g': ( 'B_ell2_b_ell2_cblinfun_set$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_19,type,
'inv_into$f': ( 'C_ell2_c_ell2_cblinfun_set$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_20,type,
'f$': 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_21,type,
'register_tensor$e': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_22,type,
'register_tensor$d': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff(func_def_23,type,
'comp$e': ( 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_24,type,
'inv_into$e': ( 'C_ell2_c_ell2_cblinfun_set$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_25,type,
'comp$ae': ( 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' * 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff(func_def_26,type,
'fun_app$l': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_27,type,
'top$c': 'A_ell2_a_ell2_cblinfun_bool_fun$' ).
tff(func_def_28,type,
'fun_app$t': ( 'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_29,type,
'register_tensor$u': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_30,type,
'image$a': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > 'C_ell2_c_ell2_cblinfun_set$' ).
tff(func_def_31,type,
'comp$j': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_32,type,
'fun_app$h': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_33,type,
'register_tensor$m': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_34,type,
'collect$': 'C_ell2_c_ell2_cblinfun_bool_fun$' > 'C_ell2_c_ell2_cblinfun_set$' ).
tff(func_def_35,type,
'register_tensor$b': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff(func_def_36,type,
'id$a': 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_37,type,
'register_tensor$a': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_38,type,
'id$g': 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_39,type,
'comp$ai': ( 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' * 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff(func_def_40,type,
'comp$g': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_41,type,
'inv_into$r': ( 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$' * 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_42,type,
'fun_app$f': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_43,type,
'id$f': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_44,type,
'register_tensor$i': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_a_prod_ell2_c_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_45,type,
'comp$': 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$' ).
tff(func_def_46,type,
'id$j': 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_47,type,
'comp$ag': ( 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' * 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_48,type,
'image$g': ( 'Nat_nat_fun$' * 'Nat_set$' ) > 'Nat_set$' ).
tff(func_def_49,type,
'comp$ad': ( 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' * 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_50,type,
'top$j': 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$' ).
tff(func_def_51,type,
'comp$n': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_52,type,
'collect$a': 'A_ell2_a_ell2_cblinfun_bool_fun$' > 'A_ell2_a_ell2_cblinfun_set$' ).
tff(func_def_53,type,
'comp$q': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_54,type,
'inv_into$m': ( 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$' * 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_55,type,
'register_tensor$s': ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_56,type,
'id$c': 'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$' ).
tff(func_def_57,type,
'commutant$a': 'A_ell2_a_ell2_cblinfun_set$' > 'A_ell2_a_ell2_cblinfun_set$' ).
tff(func_def_58,type,
'comp$s': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_59,type,
'register_tensor$l': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff(func_def_60,type,
'top$a': 'B_ell2_b_ell2_cblinfun_set$' ).
tff(func_def_61,type,
'commutant$': 'C_ell2_c_ell2_cblinfun_set$' > 'C_ell2_c_ell2_cblinfun_set$' ).
tff(func_def_62,type,
'top$g': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$' ).
tff(func_def_63,type,
'id$e': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_64,type,
'fun_app$e': ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_65,type,
'comp$r': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_66,type,
'image$c': 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun_set_a_ell2_a_ell2_cblinfun_set_fun$' ).
tff(func_def_67,type,
'i$': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_68,type,
'top$m': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$' ).
tff(func_def_69,type,
'fun_app$i': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_70,type,
'inv_into$k': ( 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$' * 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_71,type,
'top$l': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$' ).
tff(func_def_72,type,
'comp$a': 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$' ).
tff(func_def_73,type,
'fun_app$s': ( 'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_74,type,
'fun_app$c': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_75,type,
'comp$aa': ( 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' * 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff(func_def_76,type,
'comp$w': ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_77,type,
'register_tensor$w': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_78,type,
'fun_app$j': ( 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_79,type,
'id$i': 'Nat_nat_fun_nat_nat_fun_fun$' ).
tff(func_def_80,type,
'id_cblinfun$': 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_81,type,
'inv_into$l': ( 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$' * 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_82,type,
'register_tensor$': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff(func_def_83,type,
'top$b': 'C_ell2_c_ell2_cblinfun_set$' ).
tff(func_def_84,type,
'inv_into$j': ( 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_set$' * 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_85,type,
'g$': 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_86,type,
'register_tensor$t': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_87,type,
'image$i': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > 'B_ell2_b_ell2_cblinfun_set$' ).
tff(func_def_88,type,
'collect$b': 'B_ell2_b_ell2_cblinfun_bool_fun$' > 'B_ell2_b_ell2_cblinfun_set$' ).
tff(func_def_89,type,
'comp$o': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_90,type,
'register_tensor$q': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_91,type,
'comp$aj': ( 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' * 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff(func_def_92,type,
'inv_into$i': ( 'C_ell2_c_ell2_cblinfun_set$' * 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_93,type,
'commutant$b': 'B_ell2_b_ell2_cblinfun_set$' > 'B_ell2_b_ell2_cblinfun_set$' ).
tff(func_def_94,type,
'inv_into$q': ( 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$' * 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ) > 'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_95,type,
'comp$i': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_96,type,
'image$f': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > 'B_ell2_b_ell2_cblinfun_set$' ).
tff(func_def_97,type,
'fun_app$p': ( 'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > 'B_ell2_b_ell2_cblinfun_set$' ).
tff(func_def_98,type,
'comp$v': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_99,type,
'inv_into$o': ( 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_set$' * 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ) > 'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_100,type,
'fun_app$m': ( 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_101,type,
'register_tensor$z': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_102,type,
'id$b': 'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$' ).
tff(func_def_103,type,
'comp$ac': ( 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' * 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_104,type,
'register_tensor$k': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_a_prod_ell2_c_a_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_105,type,
'inv_into$c': ( 'B_ell2_b_ell2_cblinfun_set$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_106,type,
'comp$ab': ( 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' * 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' ).
tff(func_def_107,type,
'register_tensor$ab': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_108,type,
'comp$l': ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_109,type,
'top$f': 'Nat_nat_fun_set$' ).
tff(func_def_110,type,
'comp$m': ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_111,type,
'uu$': 'C_ell2_c_ell2_cblinfun_set$' > 'C_ell2_c_ell2_cblinfun_bool_fun$' ).
tff(func_def_112,type,
'register_tensor$j': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_113,type,
'fun_app$d': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_114,type,
'j$': 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_115,type,
'register_tensor$o': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_116,type,
'fun_app$g': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_117,type,
'register_tensor$c': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_118,type,
'register_tensor$y': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_119,type,
'id_cblinfun$a': 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_120,type,
'register_tensor$ad': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff(func_def_121,type,
'register_tensor$ac': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_122,type,
'id$d': 'Nat_nat_fun$' ).
tff(func_def_123,type,
'register_tensor$r': ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_124,type,
'fun_app$u': ( 'Nat_set_nat_fun$' * 'Nat_set$' ) > 'Nat$' ).
tff(func_def_125,type,
'comp$b': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$' ).
tff(func_def_126,type,
'register_tensor$ae': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff(func_def_127,type,
'image$e': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > 'A_ell2_a_ell2_cblinfun_set$' ).
tff(func_def_128,type,
'top$e': 'Nat_set$' ).
tff(func_def_129,type,
'fun_app$v': ( 'C_ell2_c_ell2_cblinfun_set_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_130,type,
'comp$y': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_131,type,
'top$k': 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_set$' ).
tff(func_def_132,type,
'comp$d': ( 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_133,type,
'comp$x': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_134,type,
'comp$u': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_135,type,
'inv_into$h': ( 'A_ell2_a_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_136,type,
'fun_app$a': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_137,type,
'register_tensor$p': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_138,type,
'comp$t': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_139,type,
'suc$': 'Nat_nat_fun$' ).
tff(func_def_140,type,
'comp$k': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_141,type,
'inv_into$p': ( 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_set$' * 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ) > 'A_c_prod_ell2_a_c_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_142,type,
'top$h': 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$' ).
tff(func_def_143,type,
'register_tensor$n': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' ).
tff(func_def_144,type,
'register_tensor$g': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_c_prod_ell2_c_c_prod_ell2_cblinfun_b_b_prod_ell2_b_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_145,type,
'comp$z': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_146,type,
'comp$ah': ( 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' * 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ) > 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_147,type,
'id$': 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_148,type,
'register_tensor$x': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_b_a_prod_ell2_b_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_149,type,
'fun_app$n': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_150,type,
'top$': 'A_ell2_a_ell2_cblinfun_set$' ).
tff(func_def_151,type,
'comp$c': 'Nat_nat_fun$' > 'Nat_nat_fun_nat_nat_fun_fun$' ).
tff(func_def_152,type,
'register_tensor$aa': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_b_prod_ell2_a_b_prod_ell2_cblinfun_fun$' ).
tff(func_def_153,type,
'id$h': 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' ).
tff(func_def_154,type,
'comp$f': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_155,type,
'inv_into$a': ( 'B_ell2_b_ell2_cblinfun_set$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_156,type,
'image$d': 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun_set_b_ell2_b_ell2_cblinfun_set_fun$' ).
tff(func_def_157,type,
sK0: ( 'A_ell2_a_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_158,type,
sK1: ( 'A_ell2_a_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_159,type,
sK2: ( 'B_ell2_b_ell2_cblinfun_set$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_160,type,
sK3: ( 'B_ell2_b_ell2_cblinfun_set$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_161,type,
sK4: ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_162,type,
sK5: ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_163,type,
sK6: ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_164,type,
sK7: ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_165,type,
sK8: ( 'A_ell2_a_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_166,type,
sK9: ( 'B_ell2_b_ell2_cblinfun_set$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_167,type,
sK10: ( 'A_ell2_a_ell2_cblinfun_set$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_168,type,
sK11: ( 'B_ell2_b_ell2_cblinfun_set$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_169,type,
sK12: ( 'A_ell2_a_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_170,type,
sK13: ( 'A_ell2_a_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_171,type,
sK14: ( 'B_ell2_b_ell2_cblinfun_set$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_172,type,
sK15: ( 'B_ell2_b_ell2_cblinfun_set$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_173,type,
sK16: ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' * 'C_ell2_c_ell2_cblinfun_bool_fun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_174,type,
sK17: ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' * 'C_ell2_c_ell2_cblinfun_bool_fun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_175,type,
sK18: ( 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' * 'C_ell2_c_ell2_cblinfun_bool_fun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_176,type,
sK19: ( 'A_ell2_a_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_177,type,
sK20: ( 'B_ell2_b_ell2_cblinfun_set$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_178,type,
sK21: ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' * 'C_ell2_c_ell2_cblinfun_bool_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_179,type,
sK22: ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' * 'C_ell2_c_ell2_cblinfun_bool_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_180,type,
sK23: ( 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' * 'C_ell2_c_ell2_cblinfun_bool_fun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_181,type,
sK24: ( 'C_ell2_c_ell2_cblinfun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_182,type,
sK25: ( 'C_ell2_c_ell2_cblinfun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_183,type,
sK26: ( 'C_ell2_c_ell2_cblinfun$' * 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_184,type,
sK27: ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' * 'A_ell2_a_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_185,type,
sK28: ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_186,type,
sK29: ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' * 'B_ell2_b_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_187,type,
sK30: ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_188,type,
sK31: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_189,type,
sK32: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_190,type,
sK33: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_191,type,
sK34: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_192,type,
sK35: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_193,type,
sK36: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_194,type,
sK37: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_195,type,
sK38: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_196,type,
sK39: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_197,type,
sK40: ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_198,type,
sK41: 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_199,type,
sK42: ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_200,type,
sK43: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_201,type,
sK44: ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_202,type,
sK45: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_203,type,
sK46: ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_204,type,
sK47: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_205,type,
sK48: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_206,type,
sK49: 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_207,type,
sK50: ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_208,type,
sK51: ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_209,type,
sK52: ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_210,type,
sK53: ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_211,type,
sK54: ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_212,type,
sK55: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_213,type,
sK56: ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_214,type,
sK57: ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_215,type,
sK58: ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_216,type,
sK59: ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_217,type,
sK60: ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_218,type,
sK61: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_219,type,
sK62: ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_220,type,
sK63: ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_221,type,
sK64: ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_222,type,
sK65: ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_223,type,
sK66: ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_224,type,
sK67: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_225,type,
sK68: ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_226,type,
sK69: ( 'Nat_nat_fun$' * 'Nat_nat_fun$' * 'Nat_nat_fun$' * 'Nat_nat_fun$' ) > 'Nat$' ).
tff(func_def_227,type,
sK70: ( 'Nat_nat_fun$' * 'Nat_nat_fun$' * 'Nat_nat_fun$' * 'Nat_nat_fun$' ) > 'Nat$' ).
tff(func_def_228,type,
sK71: ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_229,type,
sK72: ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_230,type,
sK73: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_231,type,
sK74: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_232,type,
sK75: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_233,type,
sK76: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_234,type,
sK77: ( 'Nat_nat_fun$' * 'Nat_nat_fun$' * 'Nat_nat_fun$' ) > 'Nat$' ).
tff(func_def_235,type,
sK78: ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_236,type,
sK79: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_237,type,
sK80: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_238,type,
sK81: ( 'Nat_nat_fun$' * 'Nat_nat_fun$' * 'Nat_nat_fun$' ) > 'Nat$' ).
tff(func_def_239,type,
sK82: ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_240,type,
sK83: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_241,type,
sK84: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_242,type,
sK85: 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_243,type,
sK86: 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_244,type,
sK87: 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_245,type,
sK88: 'C_ell2_c_ell2_cblinfun_set$' > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_246,type,
sK89: 'A_ell2_a_ell2_cblinfun_set$' > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_247,type,
sK90: 'B_ell2_b_ell2_cblinfun_set$' > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_248,type,
sK91: ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_bool_fun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_249,type,
sK92: ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_bool_fun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_250,type,
sK93: ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_251,type,
sK94: ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_252,type,
sK95: ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_253,type,
sK96: ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_254,type,
sK97: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_255,type,
sK98: 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_256,type,
sK99: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_257,type,
sK100: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_258,type,
sK101: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_259,type,
sK102: 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_260,type,
sK103: ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_261,type,
sK104: ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_262,type,
sK105: ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_263,type,
sK106: ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_264,type,
sK107: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_265,type,
sK108: ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_266,type,
sK109: ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_267,type,
sK110: ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_268,type,
sK111: ( 'Nat_nat_fun$' * 'Nat_set$' * 'Nat_nat_fun$' * 'Nat_nat_fun$' ) > 'Nat$' ).
tff(func_def_269,type,
sK112: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_270,type,
sK113: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_271,type,
sK114: ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_272,type,
sK115: 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_273,type,
sK116: 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_274,type,
sK117: ( 'A_ell2_a_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_275,type,
sK118: ( 'B_ell2_b_ell2_cblinfun_set$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_276,type,
sK119: ( 'A_ell2_a_ell2_cblinfun_set$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_277,type,
sK120: ( 'B_ell2_b_ell2_cblinfun_set$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_278,type,
sK121: 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_279,type,
sK122: 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_280,type,
sK123: 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_281,type,
sK124: 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_282,type,
sK125: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_283,type,
sK126: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_284,type,
sK127: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_285,type,
sK128: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_286,type,
sK129: 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_287,type,
sK130: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_288,type,
sK131: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_289,type,
sK132: 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_290,type,
sK133: 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_291,type,
sK134: 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_292,type,
sK135: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_293,type,
sK136: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_294,type,
sK137: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_295,type,
sK138: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_296,type,
sK139: 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_297,type,
sK140: 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' ).
tff(func_def_298,type,
sK141: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ).
tff(func_def_299,type,
sK142: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ).
tff(func_def_300,type,
sK143: ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_301,type,
sK144: ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_302,type,
sK145: ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_303,type,
sK146: ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_304,type,
sK147: ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_305,type,
sK148: ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_306,type,
sK149: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_307,type,
sK150: ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(func_def_308,type,
sK151: ( 'Nat_nat_fun$' * 'Nat_nat_fun$' ) > 'Nat$' ).
tff(func_def_309,type,
sK152: ( 'Nat_nat_fun$' * 'Nat_nat_fun$' ) > 'Nat$' ).
tff(func_def_310,type,
sK153: ( 'C_ell2_c_ell2_cblinfun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'C_ell2_c_ell2_cblinfun$' ).
tff(func_def_311,type,
sK154: ( 'A_ell2_a_ell2_cblinfun$' * 'A_ell2_a_ell2_cblinfun$' ) > 'A_ell2_a_ell2_cblinfun$' ).
tff(func_def_312,type,
sK155: ( 'B_ell2_b_ell2_cblinfun$' * 'B_ell2_b_ell2_cblinfun$' ) > 'B_ell2_b_ell2_cblinfun$' ).
tff(pred_def_1,type,
'register$k': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' > $o ).
tff(pred_def_2,type,
'register$j': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' > $o ).
tff(pred_def_3,type,
'clinear$g': 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff(pred_def_4,type,
'fun_app$q': ( 'A_ell2_a_ell2_cblinfun_bool_fun$' * 'A_ell2_a_ell2_cblinfun$' ) > $o ).
tff(pred_def_5,type,
'inj_on$': ( 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_6,type,
'register$n': 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' > $o ).
tff(pred_def_7,type,
'inj_on$d': ( 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_8,type,
'member$a': ( 'A_ell2_a_ell2_cblinfun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_9,type,
'iso_register$h': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_a_prod_ell2_a_a_prod_ell2_cblinfun_fun$' > $o ).
tff(pred_def_10,type,
'clinear$b': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff(pred_def_11,type,
'iso_register$d': 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff(pred_def_12,type,
'iso_register$': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff(pred_def_13,type,
'inj_on$a': ( 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_14,type,
'inj_on$m': ( 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_15,type,
'inj_on$j': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$' ) > $o ).
tff(pred_def_16,type,
'member$b': ( 'B_ell2_b_ell2_cblinfun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_17,type,
'register$q': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' > $o ).
tff(pred_def_18,type,
'inj_on$e': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_19,type,
'iso_register$f': 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff(pred_def_20,type,
'clinear$d': 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff(pred_def_21,type,
'iso_register$c': 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff(pred_def_22,type,
'member$c': ( 'Nat$' * 'Nat_set$' ) > $o ).
tff(pred_def_23,type,
'iso_register$e': 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff(pred_def_24,type,
'register$b': 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff(pred_def_25,type,
'clinear$a': 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff(pred_def_26,type,
'bijection$b': 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff(pred_def_27,type,
'register$p': 'A_a_prod_ell2_a_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' > $o ).
tff(pred_def_28,type,
'register$f': 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff(pred_def_29,type,
'inj_on$b': ( 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_30,type,
'iso_register$b': 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff(pred_def_31,type,
'register$r': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_a_c_prod_ell2_a_c_prod_ell2_cblinfun_fun$' > $o ).
tff(pred_def_32,type,
'register$h': 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff(pred_def_33,type,
'iso_register$a': 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff(pred_def_34,type,
'register$c': 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff(pred_def_35,type,
'bijection$': 'Nat_nat_fun$' > $o ).
tff(pred_def_36,type,
'inj_on$k': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_a_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_fun$' * 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_set$' ) > $o ).
tff(pred_def_37,type,
'register$': 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff(pred_def_38,type,
'register$l': 'B_a_prod_ell2_b_a_prod_ell2_cblinfun_c_b_prod_ell2_c_b_prod_ell2_cblinfun_fun$' > $o ).
tff(pred_def_39,type,
'clinear$c': 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff(pred_def_40,type,
'register$m': 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' > $o ).
tff(pred_def_41,type,
'inj_on$h': ( 'Nat_nat_fun_nat_nat_fun_fun$' * 'Nat_nat_fun_set$' ) > $o ).
tff(pred_def_42,type,
'iso_register$g': 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff(pred_def_43,type,
'register$d': 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff(pred_def_44,type,
'clinear$': 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff(pred_def_45,type,
'bijection$a': 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff(pred_def_46,type,
'member$': ( 'C_ell2_c_ell2_cblinfun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_47,type,
'clinear$f': 'C_ell2_c_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff(pred_def_48,type,
'inj_on$c': ( 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'B_ell2_b_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_49,type,
'inj_on$f': ( 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' * 'A_ell2_a_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_50,type,
'register$o': 'A_b_prod_ell2_a_b_prod_ell2_cblinfun_c_a_prod_ell2_c_a_prod_ell2_cblinfun_fun$' > $o ).
tff(pred_def_51,type,
'fun_app$r': ( 'B_ell2_b_ell2_cblinfun_bool_fun$' * 'B_ell2_b_ell2_cblinfun$' ) > $o ).
tff(pred_def_52,type,
'register$g': 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff(pred_def_53,type,
'inj_on$g': ( 'Nat_nat_fun$' * 'Nat_set$' ) > $o ).
tff(pred_def_54,type,
'inj_on$i': ( 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_b_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun_fun$' * 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun_set$' ) > $o ).
tff(pred_def_55,type,
'register$i': 'B_b_prod_ell2_b_b_prod_ell2_cblinfun_c_c_prod_ell2_c_c_prod_ell2_cblinfun_fun$' > $o ).
tff(pred_def_56,type,
'clinear$h': 'C_ell2_c_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$' > $o ).
tff(pred_def_57,type,
'register$a': 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$' > $o ).
tff(pred_def_58,type,
'inj_on$l': ( 'C_ell2_c_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' * 'C_ell2_c_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_59,type,
'clinear$e': 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff(pred_def_60,type,
'fun_app$': ( 'C_ell2_c_ell2_cblinfun_bool_fun$' * 'C_ell2_c_ell2_cblinfun$' ) > $o ).
tff(pred_def_61,type,
'register$e': 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$' > $o ).
tff(f2,conjecture,
'fun_app$a'('comp$'('f$'),'i$') = 'g$',
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture1) ).
tff(f3,negated_conjecture,
( ( ~ 'fun_app$a'('comp$'('f$'),'i$') ) = 'g$' ),
inference(negated_conjecture,[status(cth)],[f2]) ).
tff(f6,axiom,
'iso_register$'('i$'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom4) ).
tff(f12,axiom,
'register$b'('i$'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom10) ).
tff(f15,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$d'('i$',X0) = 'fun_app$l'('inv_into$'('top$','f$'),'fun_app$b'('g$',X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom13) ).
tff(f48,axiom,
! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X2: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X3: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'fun_app$a'('comp$'(X0),X1) = X2 )
=> ( 'fun_app$c'(X0,'fun_app$d'(X1,X3)) = 'fun_app$b'(X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom46) ).
tff(f49,axiom,
! [X0: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X2: 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X3: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'fun_app$f'('comp$a'(X0),X1) = X2 )
=> ( 'fun_app$g'(X0,'fun_app$d'(X1,X3)) = 'fun_app$e'(X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom47) ).
tff(f50,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X2: 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X3: 'A_ell2_a_ell2_cblinfun$'] :
( ( 'fun_app$i'('comp$b'(X0),X1) = X2 )
=> ( 'fun_app$d'(X0,'fun_app$g'(X1,X3)) = 'fun_app$h'(X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom48) ).
tff(f52,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun$'] : 'member$'('fun_app$b'('g$',X0),'image$'('f$','top$')),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom50) ).
tff(f58,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( 'register$b'(X0)
=> 'clinear$b'(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom56) ).
tff(f127,axiom,
! [X0: 'C_ell2_c_ell2_cblinfun$',X1: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X2: 'A_ell2_a_ell2_cblinfun_set$'] :
( 'member$'(X0,'image$'(X1,X2))
<=> ? [X3: 'A_ell2_a_ell2_cblinfun$'] :
( 'member$a'(X3,X2)
& ( X0 = 'fun_app$c'(X1,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom125) ).
tff(f128,axiom,
! [X0: 'C_ell2_c_ell2_cblinfun$',X1: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X2: 'B_ell2_b_ell2_cblinfun_set$'] :
( 'member$'(X0,'image$a'(X1,X2))
<=> ? [X3: 'B_ell2_b_ell2_cblinfun$'] :
( 'member$b'(X3,X2)
& ( X0 = 'fun_app$b'(X1,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom126) ).
tff(f141,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'C_ell2_c_ell2_cblinfun$'] :
( 'inj_on$a'(X0,'top$a')
=> ( 'member$'(X1,'image$a'(X0,'top$a'))
<=> ? [X2: 'B_ell2_b_ell2_cblinfun$'] :
( ( X1 = 'fun_app$b'(X0,X2) )
& ! [X3: 'B_ell2_b_ell2_cblinfun$'] :
( ( X1 = 'fun_app$b'(X0,X3) )
=> ( X3 = X2 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom139) ).
tff(f174,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun$'] : 'member$'('fun_app$b'(X0,X1),'image$a'(X0,'top$a')),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom172) ).
tff(f186,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun$',X2: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'inj_on$a'(X0,'top$a')
& ( 'fun_app$b'(X0,X1) = 'fun_app$b'(X0,X2) ) )
=> ( X1 = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom184) ).
tff(f188,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X2: 'A_ell2_a_ell2_cblinfun_set$'] :
( 'inj_on$b'('fun_app$i'('comp$b'(X0),X1),X2)
=> 'inj_on$f'(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom186) ).
tff(f195,axiom,
! [X0: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ( 'image$f'(X0,'top$') = 'top$a' )
<=> ! [X1: 'B_ell2_b_ell2_cblinfun$'] :
? [X2: 'A_ell2_a_ell2_cblinfun$'] : ( X1 = 'fun_app$g'(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom193) ).
tff(f197,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( 'image$e'(X0,'top$a') = 'top$' )
<=> ! [X1: 'A_ell2_a_ell2_cblinfun$'] :
? [X2: 'B_ell2_b_ell2_cblinfun$'] : ( X1 = 'fun_app$d'(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom195) ).
tff(f218,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X2: 'A_ell2_a_ell2_cblinfun_set$'] : ( 'image$e'(X0,'image$f'(X1,X2)) = 'fun_app$o'('image$c'('fun_app$i'('comp$b'(X0),X1)),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom216) ).
tff(f279,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( 'register$b'(X0)
=> 'inj_on$e'(X0,'top$a') ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom277) ).
tff(f287,axiom,
! [X0: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( 'inj_on$f'(X0,'top$')
=> ( 'comp$k'('fun_app$a'('comp$'(X1),'inv_into$b'('top$',X0)),X0) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom285) ).
tff(f291,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( 'inj_on$e'(X0,'top$a')
=> ( 'fun_app$a'('comp$'('comp$k'(X1,'inv_into$c'('top$a',X0))),X0) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom289) ).
tff(f338,axiom,
'inj_on$a'('g$','top$a'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom336) ).
tff(f339,axiom,
! [X0: 'A_ell2_a_ell2_cblinfun$'] : 'member$'('fun_app$c'('f$',X0),'image$a'('g$','top$a')),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom337) ).
tff(f340,axiom,
! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$g'('j$',X0) = 'fun_app$n'('inv_into$a'('top$a','g$'),'fun_app$c'('f$',X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom338) ).
tff(f383,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun$',X2: 'C_ell2_c_ell2_cblinfun$'] :
( ( 'inj_on$a'(X0,'top$a')
& ( 'fun_app$b'(X0,X1) = X2 ) )
=> ( 'fun_app$n'('inv_into$a'('top$a',X0),X2) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom381) ).
tff(f387,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_set$',X2: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X3: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ( ( 'image$e'(X0,X1) = 'top$' )
& ! [X4: 'B_ell2_b_ell2_cblinfun$'] :
( 'member$b'(X4,X1)
=> ( 'fun_app$b'('fun_app$a'('comp$'(X2),X0),X4) = 'fun_app$b'('fun_app$a'('comp$'(X3),X0),X4) ) ) )
=> ( X2 = X3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom385) ).
tff(f390,axiom,
'fun_app$f'('comp$a'('j$'),'i$') = 'id$',
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom388) ).
tff(f391,axiom,
'fun_app$i'('comp$b'('i$'),'j$') = 'id$a',
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom389) ).
tff(f428,axiom,
'image$c'('id$a') = 'id$c',
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom426) ).
tff(f449,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ! [X1: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$e'(X0,X1) = X1 )
<=> ( X0 = 'id$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom447) ).
tff(f450,axiom,
! [X0: 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ! [X1: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$h'(X0,X1) = X1 )
<=> ( X0 = 'id$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom448) ).
tff(f457,axiom,
! [X0: 'A_ell2_a_ell2_cblinfun_set$'] : 'inj_on$b'('id$a',X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom455) ).
tff(f474,axiom,
'fun_app$o'('image$c'('id$a'),'top$') = 'top$',
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom472) ).
tff(f523,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( 'clinear$b'(X0)
& ( 'image$e'(X0,'top$a') = 'top$' ) )
=> ? [X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( 'clinear$c'(X1)
& ( 'fun_app$i'('comp$b'(X0),X1) = 'id$a' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom521) ).
tff(f545,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( 'iso_register$'(X0)
=> ( 'fun_app$i'('comp$b'(X0),'inv_into$c'('top$a',X0)) = 'id$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom543) ).
tff(f549,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( 'iso_register$'(X0)
=> ( 'fun_app$f'('comp$a'('inv_into$c'('top$a',X0)),X0) = 'id$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom547) ).
tff(f621,axiom,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X2: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X3: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( 'comp$k'(X0,X1) = X2 )
=> ( 'comp$j'(X0,'fun_app$f'('comp$a'(X1),X3)) = 'fun_app$a'('comp$'(X2),X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom619) ).
tff(f627,axiom,
! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X2: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X3: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ( 'fun_app$a'('comp$'(X0),X1) = X2 )
=> ( 'comp$n'(X0,'fun_app$i'('comp$b'(X1),X3)) = 'comp$k'(X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom625) ).
tff(f642,plain,
'fun_app$a'('comp$'('f$'),'i$') != 'g$',
inference(flattening,[],[f3]) ).
tff(f683,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X2: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X3: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'fun_app$c'(X0,'fun_app$d'(X1,X3)) = 'fun_app$b'(X2,X3) )
| ( 'fun_app$a'('comp$'(X0),X1) != X2 ) ),
inference(ennf_transformation,[],[f48]) ).
tff(f684,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X2: 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X3: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'fun_app$g'(X0,'fun_app$d'(X1,X3)) = 'fun_app$e'(X2,X3) )
| ( 'fun_app$f'('comp$a'(X0),X1) != X2 ) ),
inference(ennf_transformation,[],[f49]) ).
tff(f685,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X2: 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X3: 'A_ell2_a_ell2_cblinfun$'] :
( ( 'fun_app$d'(X0,'fun_app$g'(X1,X3)) = 'fun_app$h'(X2,X3) )
| ( 'fun_app$i'('comp$b'(X0),X1) != X2 ) ),
inference(ennf_transformation,[],[f50]) ).
tff(f691,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( 'clinear$b'(X0)
| ~ 'register$b'(X0) ),
inference(ennf_transformation,[],[f58]) ).
tff(f804,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'C_ell2_c_ell2_cblinfun$'] :
( ( 'member$'(X1,'image$a'(X0,'top$a'))
<=> ? [X2: 'B_ell2_b_ell2_cblinfun$'] :
( ( X1 = 'fun_app$b'(X0,X2) )
& ! [X3: 'B_ell2_b_ell2_cblinfun$'] :
( ( X3 = X2 )
| ( 'fun_app$b'(X0,X3) != X1 ) ) ) )
| ~ 'inj_on$a'(X0,'top$a') ),
inference(ennf_transformation,[],[f141]) ).
tff(f855,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun$',X2: 'B_ell2_b_ell2_cblinfun$'] :
( ( X1 = X2 )
| ~ 'inj_on$a'(X0,'top$a')
| ( 'fun_app$b'(X0,X2) != 'fun_app$b'(X0,X1) ) ),
inference(ennf_transformation,[],[f186]) ).
tff(f856,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun$',X2: 'B_ell2_b_ell2_cblinfun$'] :
( ( X1 = X2 )
| ~ 'inj_on$a'(X0,'top$a')
| ( 'fun_app$b'(X0,X2) != 'fun_app$b'(X0,X1) ) ),
inference(flattening,[],[f855]) ).
tff(f858,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X2: 'A_ell2_a_ell2_cblinfun_set$'] :
( 'inj_on$f'(X1,X2)
| ~ 'inj_on$b'('fun_app$i'('comp$b'(X0),X1),X2) ),
inference(ennf_transformation,[],[f188]) ).
tff(f952,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( 'inj_on$e'(X0,'top$a')
| ~ 'register$b'(X0) ),
inference(ennf_transformation,[],[f279]) ).
tff(f957,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ( 'comp$k'('fun_app$a'('comp$'(X1),'inv_into$b'('top$',X0)),X0) = X1 )
| ~ 'inj_on$f'(X0,'top$') ),
inference(ennf_transformation,[],[f287]) ).
tff(f961,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ( 'fun_app$a'('comp$'('comp$k'(X1,'inv_into$c'('top$a',X0))),X0) = X1 )
| ~ 'inj_on$e'(X0,'top$a') ),
inference(ennf_transformation,[],[f291]) ).
tff(f1082,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun$',X2: 'C_ell2_c_ell2_cblinfun$'] :
( ( 'fun_app$n'('inv_into$a'('top$a',X0),X2) = X1 )
| ~ 'inj_on$a'(X0,'top$a')
| ( 'fun_app$b'(X0,X1) != X2 ) ),
inference(ennf_transformation,[],[f383]) ).
tff(f1083,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun$',X2: 'C_ell2_c_ell2_cblinfun$'] :
( ( 'fun_app$n'('inv_into$a'('top$a',X0),X2) = X1 )
| ~ 'inj_on$a'(X0,'top$a')
| ( 'fun_app$b'(X0,X1) != X2 ) ),
inference(flattening,[],[f1082]) ).
tff(f1090,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_set$',X2: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X3: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ( X2 = X3 )
| ( 'top$' != 'image$e'(X0,X1) )
| ? [X4: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'fun_app$b'('fun_app$a'('comp$'(X2),X0),X4) != 'fun_app$b'('fun_app$a'('comp$'(X3),X0),X4) )
& 'member$b'(X4,X1) ) ),
inference(ennf_transformation,[],[f387]) ).
tff(f1091,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_set$',X2: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X3: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ( X2 = X3 )
| ( 'top$' != 'image$e'(X0,X1) )
| ? [X4: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'fun_app$b'('fun_app$a'('comp$'(X2),X0),X4) != 'fun_app$b'('fun_app$a'('comp$'(X3),X0),X4) )
& 'member$b'(X4,X1) ) ),
inference(flattening,[],[f1090]) ).
tff(f1210,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ? [X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( 'clinear$c'(X1)
& ( 'fun_app$i'('comp$b'(X0),X1) = 'id$a' ) )
| ~ 'clinear$b'(X0)
| ( 'top$' != 'image$e'(X0,'top$a') ) ),
inference(ennf_transformation,[],[f523]) ).
tff(f1211,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ? [X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( 'clinear$c'(X1)
& ( 'fun_app$i'('comp$b'(X0),X1) = 'id$a' ) )
| ~ 'clinear$b'(X0)
| ( 'top$' != 'image$e'(X0,'top$a') ) ),
inference(flattening,[],[f1210]) ).
tff(f1239,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( 'fun_app$i'('comp$b'(X0),'inv_into$c'('top$a',X0)) = 'id$a' )
| ~ 'iso_register$'(X0) ),
inference(ennf_transformation,[],[f545]) ).
tff(f1243,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( 'fun_app$f'('comp$a'('inv_into$c'('top$a',X0)),X0) = 'id$' )
| ~ 'iso_register$'(X0) ),
inference(ennf_transformation,[],[f549]) ).
tff(f1334,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X2: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X3: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( 'comp$j'(X0,'fun_app$f'('comp$a'(X1),X3)) = 'fun_app$a'('comp$'(X2),X3) )
| ( 'comp$k'(X0,X1) != X2 ) ),
inference(ennf_transformation,[],[f621]) ).
tff(f1340,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X2: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X3: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ( 'comp$n'(X0,'fun_app$i'('comp$b'(X1),X3)) = 'comp$k'(X2,X3) )
| ( 'fun_app$a'('comp$'(X0),X1) != X2 ) ),
inference(ennf_transformation,[],[f627]) ).
tff(f1389,plain,
! [X0: 'C_ell2_c_ell2_cblinfun$',X1: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X2: 'A_ell2_a_ell2_cblinfun_set$'] :
( ( 'member$'(X0,'image$'(X1,X2))
| ! [X3: 'A_ell2_a_ell2_cblinfun$'] :
( ~ 'member$a'(X3,X2)
| ( 'fun_app$c'(X1,X3) != X0 ) ) )
& ( ? [X3: 'A_ell2_a_ell2_cblinfun$'] :
( 'member$a'(X3,X2)
& ( X0 = 'fun_app$c'(X1,X3) ) )
| ~ 'member$'(X0,'image$'(X1,X2)) ) ),
inference(nnf_transformation,[],[f127]) ).
tff(f1390,plain,
! [X0: 'C_ell2_c_ell2_cblinfun$',X1: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X2: 'A_ell2_a_ell2_cblinfun_set$'] :
( ( 'member$'(X0,'image$'(X1,X2))
| ! [X3: 'A_ell2_a_ell2_cblinfun$'] :
( ~ 'member$a'(X3,X2)
| ( 'fun_app$c'(X1,X3) != X0 ) ) )
& ( ? [X4: 'A_ell2_a_ell2_cblinfun$'] :
( 'member$a'(X4,X2)
& ( 'fun_app$c'(X1,X4) = X0 ) )
| ~ 'member$'(X0,'image$'(X1,X2)) ) ),
inference(rectify,[],[f1389]) ).
tff(f1391,plain,
! [X0: 'C_ell2_c_ell2_cblinfun$',X1: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X2: 'A_ell2_a_ell2_cblinfun_set$'] :
( ( 'member$'(X0,'image$'(X1,X2))
| ! [X3: 'A_ell2_a_ell2_cblinfun$'] :
( ~ 'member$a'(X3,X2)
| ( 'fun_app$c'(X1,X3) != X0 ) ) )
& ( ( 'member$a'(sK24(X0,X1,X2),X2)
& ( 'fun_app$c'(X1,sK24(X0,X1,X2)) = X0 ) )
| ~ 'member$'(X0,'image$'(X1,X2)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(X4,sK24(X0,X1,X2))],[f1390]) ).
tff(f1392,plain,
! [X0: 'C_ell2_c_ell2_cblinfun$',X1: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X2: 'B_ell2_b_ell2_cblinfun_set$'] :
( ( 'member$'(X0,'image$a'(X1,X2))
| ! [X3: 'B_ell2_b_ell2_cblinfun$'] :
( ~ 'member$b'(X3,X2)
| ( 'fun_app$b'(X1,X3) != X0 ) ) )
& ( ? [X3: 'B_ell2_b_ell2_cblinfun$'] :
( 'member$b'(X3,X2)
& ( X0 = 'fun_app$b'(X1,X3) ) )
| ~ 'member$'(X0,'image$a'(X1,X2)) ) ),
inference(nnf_transformation,[],[f128]) ).
tff(f1393,plain,
! [X0: 'C_ell2_c_ell2_cblinfun$',X1: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X2: 'B_ell2_b_ell2_cblinfun_set$'] :
( ( 'member$'(X0,'image$a'(X1,X2))
| ! [X3: 'B_ell2_b_ell2_cblinfun$'] :
( ~ 'member$b'(X3,X2)
| ( 'fun_app$b'(X1,X3) != X0 ) ) )
& ( ? [X4: 'B_ell2_b_ell2_cblinfun$'] :
( 'member$b'(X4,X2)
& ( 'fun_app$b'(X1,X4) = X0 ) )
| ~ 'member$'(X0,'image$a'(X1,X2)) ) ),
inference(rectify,[],[f1392]) ).
tff(f1394,plain,
! [X0: 'C_ell2_c_ell2_cblinfun$',X1: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X2: 'B_ell2_b_ell2_cblinfun_set$'] :
( ( 'member$'(X0,'image$a'(X1,X2))
| ! [X3: 'B_ell2_b_ell2_cblinfun$'] :
( ~ 'member$b'(X3,X2)
| ( 'fun_app$b'(X1,X3) != X0 ) ) )
& ( ( 'member$b'(sK25(X0,X1,X2),X2)
& ( 'fun_app$b'(X1,sK25(X0,X1,X2)) = X0 ) )
| ~ 'member$'(X0,'image$a'(X1,X2)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(X4,sK25(X0,X1,X2))],[f1393]) ).
tff(f1407,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'C_ell2_c_ell2_cblinfun$'] :
( ( ( 'member$'(X1,'image$a'(X0,'top$a'))
| ! [X2: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'fun_app$b'(X0,X2) != X1 )
| ? [X3: 'B_ell2_b_ell2_cblinfun$'] :
( ( X2 != X3 )
& ( 'fun_app$b'(X0,X3) = X1 ) ) ) )
& ( ? [X2: 'B_ell2_b_ell2_cblinfun$'] :
( ( X1 = 'fun_app$b'(X0,X2) )
& ! [X3: 'B_ell2_b_ell2_cblinfun$'] :
( ( X3 = X2 )
| ( 'fun_app$b'(X0,X3) != X1 ) ) )
| ~ 'member$'(X1,'image$a'(X0,'top$a')) ) )
| ~ 'inj_on$a'(X0,'top$a') ),
inference(nnf_transformation,[],[f804]) ).
tff(f1408,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'C_ell2_c_ell2_cblinfun$'] :
( ( ( 'member$'(X1,'image$a'(X0,'top$a'))
| ! [X2: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'fun_app$b'(X0,X2) != X1 )
| ? [X3: 'B_ell2_b_ell2_cblinfun$'] :
( ( X2 != X3 )
& ( 'fun_app$b'(X0,X3) = X1 ) ) ) )
& ( ? [X4: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'fun_app$b'(X0,X4) = X1 )
& ! [X5: 'B_ell2_b_ell2_cblinfun$'] :
( ( X4 = X5 )
| ( 'fun_app$b'(X0,X5) != X1 ) ) )
| ~ 'member$'(X1,'image$a'(X0,'top$a')) ) )
| ~ 'inj_on$a'(X0,'top$a') ),
inference(rectify,[],[f1407]) ).
tff(f1409,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'C_ell2_c_ell2_cblinfun$'] :
( ( ( 'member$'(X1,'image$a'(X0,'top$a'))
| ! [X2: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'fun_app$b'(X0,X2) != X1 )
| ( ( sK29(X0,X1,X2) != X2 )
& ( 'fun_app$b'(X0,sK29(X0,X1,X2)) = X1 ) ) ) )
& ( ( ( 'fun_app$b'(X0,sK30(X0,X1)) = X1 )
& ! [X5: 'B_ell2_b_ell2_cblinfun$'] :
( ( sK30(X0,X1) = X5 )
| ( 'fun_app$b'(X0,X5) != X1 ) ) )
| ~ 'member$'(X1,'image$a'(X0,'top$a')) ) )
| ~ 'inj_on$a'(X0,'top$a') ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29,sK30]),skolemize(X3,sK29(X0,X1,X2)),skolemize(X4,sK30(X0,X1))],[f1408]) ).
tff(f1435,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ( ( 'image$f'(X0,'top$') = 'top$a' )
| ? [X1: 'B_ell2_b_ell2_cblinfun$'] :
! [X2: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$g'(X0,X2) != X1 ) )
& ( ! [X1: 'B_ell2_b_ell2_cblinfun$'] :
? [X2: 'A_ell2_a_ell2_cblinfun$'] : ( X1 = 'fun_app$g'(X0,X2) )
| ( 'top$a' != 'image$f'(X0,'top$') ) ) ),
inference(nnf_transformation,[],[f195]) ).
tff(f1436,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ( ( 'image$f'(X0,'top$') = 'top$a' )
| ? [X1: 'B_ell2_b_ell2_cblinfun$'] :
! [X2: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$g'(X0,X2) != X1 ) )
& ( ! [X3: 'B_ell2_b_ell2_cblinfun$'] :
? [X4: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$g'(X0,X4) = X3 )
| ( 'top$a' != 'image$f'(X0,'top$') ) ) ),
inference(rectify,[],[f1435]) ).
tff(f1437,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ( ( 'image$f'(X0,'top$') = 'top$a' )
| ! [X2: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$g'(X0,X2) != sK43(X0) ) )
& ( ! [X3: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$g'(X0,sK44(X0,X3)) = X3 )
| ( 'top$a' != 'image$f'(X0,'top$') ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43,sK44]),skolemize(X1,sK43(X0)),skolemize(X4,sK44(X0,X3))],[f1436]) ).
tff(f1441,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( ( 'image$e'(X0,'top$a') = 'top$' )
| ? [X1: 'A_ell2_a_ell2_cblinfun$'] :
! [X2: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$d'(X0,X2) != X1 ) )
& ( ! [X1: 'A_ell2_a_ell2_cblinfun$'] :
? [X2: 'B_ell2_b_ell2_cblinfun$'] : ( X1 = 'fun_app$d'(X0,X2) )
| ( 'top$' != 'image$e'(X0,'top$a') ) ) ),
inference(nnf_transformation,[],[f197]) ).
tff(f1442,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( ( 'image$e'(X0,'top$a') = 'top$' )
| ? [X1: 'A_ell2_a_ell2_cblinfun$'] :
! [X2: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$d'(X0,X2) != X1 ) )
& ( ! [X3: 'A_ell2_a_ell2_cblinfun$'] :
? [X4: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$d'(X0,X4) = X3 )
| ( 'top$' != 'image$e'(X0,'top$a') ) ) ),
inference(rectify,[],[f1441]) ).
tff(f1443,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( ( 'image$e'(X0,'top$a') = 'top$' )
| ! [X2: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$d'(X0,X2) != sK47(X0) ) )
& ( ! [X3: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$d'(X0,sK48(X0,X3)) = X3 )
| ( 'top$' != 'image$e'(X0,'top$a') ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47,sK48]),skolemize(X1,sK47(X0)),skolemize(X4,sK48(X0,X3))],[f1442]) ).
tff(f1514,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_set$',X2: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X3: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ( X2 = X3 )
| ( 'top$' != 'image$e'(X0,X1) )
| ( ( 'fun_app$b'('fun_app$a'('comp$'(X2),X0),sK112(X0,X1,X2,X3)) != 'fun_app$b'('fun_app$a'('comp$'(X3),X0),sK112(X0,X1,X2,X3)) )
& 'member$b'(sK112(X0,X1,X2,X3),X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK112]),skolemize(X4,sK112(X0,X1,X2,X3))],[f1091]) ).
tff(f1520,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ( ! [X1: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$e'(X0,X1) = X1 )
| ( 'id$' != X0 ) )
& ( ( X0 = 'id$' )
| ? [X1: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$e'(X0,X1) != X1 ) ) ),
inference(nnf_transformation,[],[f449]) ).
tff(f1521,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ( ! [X1: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$e'(X0,X1) = X1 )
| ( 'id$' != X0 ) )
& ( ( X0 = 'id$' )
| ? [X2: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$e'(X0,X2) != X2 ) ) ),
inference(rectify,[],[f1520]) ).
tff(f1522,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ( ! [X1: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$e'(X0,X1) = X1 )
| ( 'id$' != X0 ) )
& ( ( X0 = 'id$' )
| ( sK115(X0) != 'fun_app$e'(X0,sK115(X0)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK115]),skolemize(X2,sK115(X0))],[f1521]) ).
tff(f1523,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( ! [X1: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$h'(X0,X1) = X1 )
| ( 'id$a' != X0 ) )
& ( ( X0 = 'id$a' )
| ? [X1: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$h'(X0,X1) != X1 ) ) ),
inference(nnf_transformation,[],[f450]) ).
tff(f1524,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( ! [X1: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$h'(X0,X1) = X1 )
| ( 'id$a' != X0 ) )
& ( ( X0 = 'id$a' )
| ? [X2: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$h'(X0,X2) != X2 ) ) ),
inference(rectify,[],[f1523]) ).
tff(f1525,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( ! [X1: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$h'(X0,X1) = X1 )
| ( 'id$a' != X0 ) )
& ( ( X0 = 'id$a' )
| ( sK116(X0) != 'fun_app$h'(X0,sK116(X0)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK116]),skolemize(X2,sK116(X0))],[f1524]) ).
tff(f1571,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( 'clinear$c'(sK131(X0))
& ( 'id$a' = 'fun_app$i'('comp$b'(X0),sK131(X0)) ) )
| ~ 'clinear$b'(X0)
| ( 'top$' != 'image$e'(X0,'top$a') ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK131]),skolemize(X1,sK131(X0))],[f1211]) ).
tff(f1625,plain,
'fun_app$a'('comp$'('f$'),'i$') != 'g$',
inference(cnf_transformation,[],[f642]) ).
tff(f1628,plain,
'iso_register$'('i$'),
inference(cnf_transformation,[],[f6]) ).
tff(f1634,plain,
'register$b'('i$'),
inference(cnf_transformation,[],[f12]) ).
tff(f1637,plain,
! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$d'('i$',X0) = 'fun_app$l'('inv_into$'('top$','f$'),'fun_app$b'('g$',X0)) ),
inference(cnf_transformation,[],[f15]) ).
tff(f1670,plain,
! [X2: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X3: 'B_ell2_b_ell2_cblinfun$',X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( 'fun_app$c'(X0,'fun_app$d'(X1,X3)) = 'fun_app$b'(X2,X3) )
| ( 'fun_app$a'('comp$'(X0),X1) != X2 ) ),
inference(cnf_transformation,[],[f683]) ).
tff(f1671,plain,
! [X2: 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X3: 'B_ell2_b_ell2_cblinfun$',X0: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( 'fun_app$g'(X0,'fun_app$d'(X1,X3)) = 'fun_app$e'(X2,X3) )
| ( 'fun_app$f'('comp$a'(X0),X1) != X2 ) ),
inference(cnf_transformation,[],[f684]) ).
tff(f1672,plain,
! [X2: 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X3: 'A_ell2_a_ell2_cblinfun$',X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ( 'fun_app$d'(X0,'fun_app$g'(X1,X3)) = 'fun_app$h'(X2,X3) )
| ( 'fun_app$i'('comp$b'(X0),X1) != X2 ) ),
inference(cnf_transformation,[],[f685]) ).
tff(f1674,plain,
! [X0: 'B_ell2_b_ell2_cblinfun$'] : 'member$'('fun_app$b'('g$',X0),'image$'('f$','top$')),
inference(cnf_transformation,[],[f52]) ).
tff(f1680,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ~ 'register$b'(X0)
| 'clinear$b'(X0) ),
inference(cnf_transformation,[],[f691]) ).
tff(f1795,plain,
! [X2: 'A_ell2_a_ell2_cblinfun_set$',X0: 'C_ell2_c_ell2_cblinfun$',X1: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ~ 'member$'(X0,'image$'(X1,X2))
| ( 'fun_app$c'(X1,sK24(X0,X1,X2)) = X0 ) ),
inference(cnf_transformation,[],[f1391]) ).
tff(f1798,plain,
! [X2: 'B_ell2_b_ell2_cblinfun_set$',X0: 'C_ell2_c_ell2_cblinfun$',X1: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ~ 'member$'(X0,'image$a'(X1,X2))
| ( 'fun_app$b'(X1,sK25(X0,X1,X2)) = X0 ) ),
inference(cnf_transformation,[],[f1394]) ).
tff(f1824,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'C_ell2_c_ell2_cblinfun$',X5: 'B_ell2_b_ell2_cblinfun$'] :
( ( sK30(X0,X1) = X5 )
| ( 'fun_app$b'(X0,X5) != X1 )
| ~ 'member$'(X1,'image$a'(X0,'top$a'))
| ~ 'inj_on$a'(X0,'top$a') ),
inference(cnf_transformation,[],[f1409]) ).
tff(f1869,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun$'] : 'member$'('fun_app$b'(X0,X1),'image$a'(X0,'top$a')),
inference(cnf_transformation,[],[f174]) ).
tff(f1889,plain,
! [X2: 'B_ell2_b_ell2_cblinfun$',X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun$'] :
( ~ 'inj_on$a'(X0,'top$a')
| ( X1 = X2 )
| ( 'fun_app$b'(X0,X2) != 'fun_app$b'(X0,X1) ) ),
inference(cnf_transformation,[],[f856]) ).
tff(f1891,plain,
! [X2: 'A_ell2_a_ell2_cblinfun_set$',X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ~ 'inj_on$b'('fun_app$i'('comp$b'(X0),X1),X2)
| 'inj_on$f'(X1,X2) ),
inference(cnf_transformation,[],[f858]) ).
tff(f1900,plain,
! [X3: 'B_ell2_b_ell2_cblinfun$',X0: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ( 'top$a' != 'image$f'(X0,'top$') )
| ( 'fun_app$g'(X0,sK44(X0,X3)) = X3 ) ),
inference(cnf_transformation,[],[f1437]) ).
tff(f1901,plain,
! [X2: 'A_ell2_a_ell2_cblinfun$',X0: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ( 'fun_app$g'(X0,X2) != sK43(X0) )
| ( 'top$a' = 'image$f'(X0,'top$') ) ),
inference(cnf_transformation,[],[f1437]) ).
tff(f1904,plain,
! [X3: 'A_ell2_a_ell2_cblinfun$',X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( 'top$' != 'image$e'(X0,'top$a') )
| ( 'fun_app$d'(X0,sK48(X0,X3)) = X3 ) ),
inference(cnf_transformation,[],[f1443]) ).
tff(f1927,plain,
! [X2: 'A_ell2_a_ell2_cblinfun_set$',X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] : ( 'image$e'(X0,'image$f'(X1,X2)) = 'fun_app$o'('image$c'('fun_app$i'('comp$b'(X0),X1)),X2) ),
inference(cnf_transformation,[],[f218]) ).
tff(f2008,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( 'inj_on$e'(X0,'top$a')
| ~ 'register$b'(X0) ),
inference(cnf_transformation,[],[f952]) ).
tff(f2016,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ~ 'inj_on$f'(X0,'top$')
| ( 'comp$k'('fun_app$a'('comp$'(X1),'inv_into$b'('top$',X0)),X0) = X1 ) ),
inference(cnf_transformation,[],[f957]) ).
tff(f2020,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ~ 'inj_on$e'(X0,'top$a')
| ( 'fun_app$a'('comp$'('comp$k'(X1,'inv_into$c'('top$a',X0))),X0) = X1 ) ),
inference(cnf_transformation,[],[f961]) ).
tff(f2069,plain,
'inj_on$a'('g$','top$a'),
inference(cnf_transformation,[],[f338]) ).
tff(f2070,plain,
! [X0: 'A_ell2_a_ell2_cblinfun$'] : 'member$'('fun_app$c'('f$',X0),'image$a'('g$','top$a')),
inference(cnf_transformation,[],[f339]) ).
tff(f2071,plain,
! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$g'('j$',X0) = 'fun_app$n'('inv_into$a'('top$a','g$'),'fun_app$c'('f$',X0)) ),
inference(cnf_transformation,[],[f340]) ).
tff(f2120,plain,
! [X2: 'C_ell2_c_ell2_cblinfun$',X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'fun_app$n'('inv_into$a'('top$a',X0),X2) = X1 )
| ~ 'inj_on$a'(X0,'top$a')
| ( 'fun_app$b'(X0,X1) != X2 ) ),
inference(cnf_transformation,[],[f1083]) ).
tff(f2126,plain,
! [X2: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X3: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_set$'] :
( ( 'top$' != 'image$e'(X0,X1) )
| ( X2 = X3 )
| ( 'fun_app$b'('fun_app$a'('comp$'(X2),X0),sK112(X0,X1,X2,X3)) != 'fun_app$b'('fun_app$a'('comp$'(X3),X0),sK112(X0,X1,X2,X3)) ) ),
inference(cnf_transformation,[],[f1514]) ).
tff(f2131,plain,
'fun_app$f'('comp$a'('j$'),'i$') = 'id$',
inference(cnf_transformation,[],[f390]) ).
tff(f2132,plain,
'fun_app$i'('comp$b'('i$'),'j$') = 'id$a',
inference(cnf_transformation,[],[f391]) ).
tff(f2172,plain,
'image$c'('id$a') = 'id$c',
inference(cnf_transformation,[],[f428]) ).
tff(f2194,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'fun_app$e'(X0,X1) = X1 )
| ( 'id$' != X0 ) ),
inference(cnf_transformation,[],[f1522]) ).
tff(f2196,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun$'] :
( ( 'fun_app$h'(X0,X1) = X1 )
| ( 'id$a' != X0 ) ),
inference(cnf_transformation,[],[f1525]) ).
tff(f2203,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_set$'] : 'inj_on$b'('id$a',X0),
inference(cnf_transformation,[],[f457]) ).
tff(f2220,plain,
'top$' = 'fun_app$o'('image$c'('id$a'),'top$'),
inference(cnf_transformation,[],[f474]) ).
tff(f2314,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( 'top$' != 'image$e'(X0,'top$a') )
| ~ 'clinear$b'(X0)
| ( 'id$a' = 'fun_app$i'('comp$b'(X0),sK131(X0)) ) ),
inference(cnf_transformation,[],[f1571]) ).
tff(f2353,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ~ 'iso_register$'(X0)
| ( 'id$a' = 'fun_app$i'('comp$b'(X0),'inv_into$c'('top$a',X0)) ) ),
inference(cnf_transformation,[],[f1239]) ).
tff(f2357,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ~ 'iso_register$'(X0)
| ( 'id$' = 'fun_app$f'('comp$a'('inv_into$c'('top$a',X0)),X0) ) ),
inference(cnf_transformation,[],[f1243]) ).
tff(f2459,plain,
! [X2: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X3: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] :
( ( 'fun_app$a'('comp$'(X2),X3) = 'comp$j'(X0,'fun_app$f'('comp$a'(X1),X3)) )
| ( 'comp$k'(X0,X1) != X2 ) ),
inference(cnf_transformation,[],[f1334]) ).
tff(f2465,plain,
! [X2: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X3: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] :
( ( 'comp$k'(X2,X3) = 'comp$n'(X0,'fun_app$i'('comp$b'(X1),X3)) )
| ( 'fun_app$a'('comp$'(X0),X1) != X2 ) ),
inference(cnf_transformation,[],[f1340]) ).
tff(f2480,plain,
! [X3: 'B_ell2_b_ell2_cblinfun$',X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] : ( 'fun_app$c'(X0,'fun_app$d'(X1,X3)) = 'fun_app$b'('fun_app$a'('comp$'(X0),X1),X3) ),
inference(equality_resolution,[],[f1670]) ).
tff(f2481,plain,
! [X3: 'B_ell2_b_ell2_cblinfun$',X0: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] : ( 'fun_app$g'(X0,'fun_app$d'(X1,X3)) = 'fun_app$e'('fun_app$f'('comp$a'(X0),X1),X3) ),
inference(equality_resolution,[],[f1671]) ).
tff(f2482,plain,
! [X3: 'A_ell2_a_ell2_cblinfun$',X0: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] : ( 'fun_app$d'(X0,'fun_app$g'(X1,X3)) = 'fun_app$h'('fun_app$i'('comp$b'(X0),X1),X3) ),
inference(equality_resolution,[],[f1672]) ).
tff(f2506,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X5: 'B_ell2_b_ell2_cblinfun$'] :
( ( sK30(X0,'fun_app$b'(X0,X5)) = X5 )
| ~ 'member$'('fun_app$b'(X0,X5),'image$a'(X0,'top$a'))
| ~ 'inj_on$a'(X0,'top$a') ),
inference(equality_resolution,[],[f1824]) ).
tff(f2524,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun$'] :
( ~ 'inj_on$a'(X0,'top$a')
| ( 'fun_app$n'('inv_into$a'('top$a',X0),'fun_app$b'(X0,X1)) = X1 ) ),
inference(equality_resolution,[],[f2120]) ).
tff(f2525,plain,
! [X1: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$e'('id$',X1) = X1 ),
inference(equality_resolution,[],[f2194]) ).
tff(f2526,plain,
! [X1: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$h'('id$a',X1) = X1 ),
inference(equality_resolution,[],[f2196]) ).
tff(f2593,plain,
! [X3: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$',X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$'] : ( 'comp$j'(X0,'fun_app$f'('comp$a'(X1),X3)) = 'fun_app$a'('comp$'('comp$k'(X0,X1)),X3) ),
inference(equality_resolution,[],[f2459]) ).
tff(f2599,plain,
! [X3: 'A_ell2_a_ell2_cblinfun_b_ell2_b_ell2_cblinfun_fun$',X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun_a_ell2_a_ell2_cblinfun_fun$'] : ( 'comp$n'(X0,'fun_app$i'('comp$b'(X1),X3)) = 'comp$k'('fun_app$a'('comp$'(X0),X1),X3) ),
inference(equality_resolution,[],[f2465]) ).
tff(f2622,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X5: 'B_ell2_b_ell2_cblinfun$'] :
( ~ 'inj_on$a'(X0,'top$a')
| ( sK30(X0,'fun_app$b'(X0,X5)) = X5 ) ),
inference(forward_subsumption_resolution,[],[f2506,f1869]) ).
tff(f2631,plain,
'clinear$b'('i$'),
inference(resolution,[],[f1680,f1634]) ).
tff(f2663,plain,
! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$c'('f$',X0) = 'fun_app$b'('g$',sK25('fun_app$c'('f$',X0),'g$','top$a')) ),
inference(resolution,[],[f1798,f2070]) ).
tff(f2670,plain,
! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$d'('i$',sK25('fun_app$c'('f$',X0),'g$','top$a')) = 'fun_app$l'('inv_into$'('top$','f$'),'fun_app$c'('f$',X0)) ),
inference(superposition,[],[f1637,f2663]) ).
tff(f2692,plain,
! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$e'('id$',X0) = 'fun_app$g'('j$','fun_app$d'('i$',X0)) ),
inference(superposition,[],[f2481,f2131]) ).
tff(f2693,plain,
! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$g'('j$','fun_app$d'('i$',X0)) = X0 ),
inference(forward_demodulation,[],[f2692,f2525]) ).
tff(f2695,plain,
! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( sK25('fun_app$c'('f$',X0),'g$','top$a') = 'fun_app$g'('j$','fun_app$l'('inv_into$'('top$','f$'),'fun_app$c'('f$',X0))) ),
inference(superposition,[],[f2693,f2670]) ).
tff(f2706,plain,
! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$n'('inv_into$a'('top$a','g$'),'fun_app$b'('g$',X0)) = X0 ),
inference(resolution,[],[f2524,f2069]) ).
tff(f2710,plain,
! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$n'('inv_into$a'('top$a','g$'),'fun_app$c'('f$',X0)) = sK25('fun_app$c'('f$',X0),'g$','top$a') ),
inference(superposition,[],[f2706,f2663]) ).
tff(f2711,plain,
! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$g'('j$',X0) = sK25('fun_app$c'('f$',X0),'g$','top$a') ),
inference(forward_demodulation,[],[f2710,f2071]) ).
tff(f2713,plain,
! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$c'('f$',X0) = 'fun_app$b'('g$','fun_app$g'('j$',X0)) ),
inference(superposition,[],[f2663,f2711]) ).
tff(f2715,plain,
! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$b'('g$',X0) = 'fun_app$c'('f$','fun_app$d'('i$',X0)) ),
inference(superposition,[],[f2713,f2693]) ).
tff(f2750,plain,
! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$b'('g$',X0) = 'fun_app$c'('f$',sK24('fun_app$b'('g$',X0),'f$','top$')) ),
inference(resolution,[],[f1795,f1674]) ).
tff(f2758,plain,
! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( sK25('fun_app$b'('g$',X0),'g$','top$a') = 'fun_app$g'('j$','fun_app$l'('inv_into$'('top$','f$'),'fun_app$b'('g$',X0))) ),
inference(superposition,[],[f2695,f2750]) ).
tff(f2759,plain,
! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$g'('j$',sK24('fun_app$b'('g$',X0),'f$','top$')) = sK25('fun_app$b'('g$',X0),'g$','top$a') ),
inference(superposition,[],[f2711,f2750]) ).
tff(f2762,plain,
! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$g'('j$','fun_app$d'('i$',X0)) = sK25('fun_app$b'('g$',X0),'g$','top$a') ),
inference(forward_demodulation,[],[f2758,f1637]) ).
tff(f2766,plain,
! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( sK25('fun_app$b'('g$',X0),'g$','top$a') = X0 ),
inference(forward_demodulation,[],[f2762,f2693]) ).
tff(f2852,plain,
! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$h'('id$a',X0) = 'fun_app$d'('i$','fun_app$g'('j$',X0)) ),
inference(superposition,[],[f2482,f2132]) ).
tff(f2855,plain,
! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$d'('i$','fun_app$g'('j$',X0)) = X0 ),
inference(forward_demodulation,[],[f2852,f2526]) ).
tff(f2890,plain,
! [X0: 'B_ell2_b_ell2_cblinfun$',X1: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'fun_app$b'('g$',X0) != 'fun_app$b'('g$',X1) )
| ( X0 = X1 ) ),
inference(resolution,[],[f1889,f2069]) ).
tff(f2900,plain,
! [X0: 'A_ell2_a_ell2_cblinfun$',X1: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'fun_app$c'('f$',X0) != 'fun_app$b'('g$',X1) )
| ( 'fun_app$g'('j$',X0) = X1 ) ),
inference(superposition,[],[f2890,f2713]) ).
tff(f2942,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'comp$j'(X0,'id$') = 'fun_app$a'('comp$'('comp$k'(X0,'j$')),'i$') ),
inference(superposition,[],[f2593,f2131]) ).
tff(f3263,plain,
! [X0: 'B_ell2_b_ell2_cblinfun$'] :
( ( sK25('fun_app$b'('g$',X0),'g$','top$a') != sK43('j$') )
| ( 'top$a' = 'image$f'('j$','top$') ) ),
inference(superposition,[],[f1901,f2759]) ).
tff(f3284,plain,
! [X0: 'B_ell2_b_ell2_cblinfun$'] :
( ( sK43('j$') != X0 )
| ( 'top$a' = 'image$f'('j$','top$') ) ),
inference(forward_demodulation,[],[f3263,f2766]) ).
tff(f3286,definition,
( spl156_5
<=> ( 'top$a' = 'image$f'('j$','top$') ) ),
introduced(definition,[new_symbols(definition,[spl156_5])],[avatar_definition]) ).
tff(f3287,plain,
( ( 'top$a' = 'image$f'('j$','top$') )
| ~ spl156_5 ),
inference(avatar_component_clause,[],[f3286]) ).
tff(f3293,definition,
( spl156_7
<=> ! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( sK43('j$') != X0 ) ),
introduced(definition,[new_symbols(definition,[spl156_7])],[avatar_definition]) ).
tff(f3294,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( sK43('j$') != X0 )
| ~ spl156_7 ),
inference(avatar_component_clause,[],[f3293]) ).
tff(f3298,plain,
( spl156_5
| spl156_7 ),
inference(avatar_split_clause,[],[f3284,f3293,f3286]) ).
tff(f3455,plain,
'top$' = 'fun_app$o'('id$c','top$'),
inference(superposition,[],[f2220,f2172]) ).
tff(f3498,plain,
'id$a' = 'fun_app$i'('comp$b'('i$'),'inv_into$c'('top$a','i$')),
inference(resolution,[],[f2353,f1628]) ).
tff(f3501,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_set$'] : ( 'fun_app$o'('image$c'('id$a'),X0) = 'image$e'('i$','image$f'('inv_into$c'('top$a','i$'),X0)) ),
inference(superposition,[],[f1927,f3498]) ).
tff(f3502,plain,
! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$h'('id$a',X0) = 'fun_app$d'('i$','fun_app$g'('inv_into$c'('top$a','i$'),X0)) ),
inference(superposition,[],[f2482,f3498]) ).
tff(f3503,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'comp$n'(X0,'id$a') = 'comp$k'('fun_app$a'('comp$'(X0),'i$'),'inv_into$c'('top$a','i$')) ),
inference(superposition,[],[f2599,f3498]) ).
tff(f3504,plain,
! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$d'('i$','fun_app$g'('inv_into$c'('top$a','i$'),X0)) = X0 ),
inference(forward_demodulation,[],[f3502,f2526]) ).
tff(f3505,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_set$'] : ( 'fun_app$o'('id$c',X0) = 'image$e'('i$','image$f'('inv_into$c'('top$a','i$'),X0)) ),
inference(forward_demodulation,[],[f3501,f2172]) ).
tff(f3509,plain,
! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$g'('j$',X0) = 'fun_app$g'('inv_into$c'('top$a','i$'),X0) ),
inference(superposition,[],[f2693,f3504]) ).
tff(f3528,plain,
! [X0: 'A_ell2_a_ell2_cblinfun$'] :
( ( 'fun_app$g'('j$',X0) != sK43('inv_into$c'('top$a','i$')) )
| ( 'top$a' = 'image$f'('inv_into$c'('top$a','i$'),'top$') ) ),
inference(superposition,[],[f1901,f3509]) ).
tff(f3530,definition,
( spl156_8
<=> ( 'top$a' = 'image$f'('inv_into$c'('top$a','i$'),'top$') ) ),
introduced(definition,[new_symbols(definition,[spl156_8])],[avatar_definition]) ).
tff(f3531,plain,
( ( 'top$a' = 'image$f'('inv_into$c'('top$a','i$'),'top$') )
| ~ spl156_8 ),
inference(avatar_component_clause,[],[f3530]) ).
tff(f3533,definition,
( spl156_9
<=> ! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$g'('j$',X0) != sK43('inv_into$c'('top$a','i$')) ) ),
introduced(definition,[new_symbols(definition,[spl156_9])],[avatar_definition]) ).
tff(f3534,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$g'('j$',X0) != sK43('inv_into$c'('top$a','i$')) )
| ~ spl156_9 ),
inference(avatar_component_clause,[],[f3533]) ).
tff(f3535,plain,
( spl156_8
| spl156_9 ),
inference(avatar_split_clause,[],[f3528,f3533,f3530]) ).
tff(f3537,plain,
( ( 'image$e'('i$','top$a') = 'fun_app$o'('id$c','top$') )
| ~ spl156_8 ),
inference(superposition,[],[f3505,f3531]) ).
tff(f3616,definition,
( spl156_16
<=> 'inj_on$e'('i$','top$a') ),
introduced(definition,[new_symbols(definition,[spl156_16])],[avatar_definition]) ).
tff(f3617,plain,
( 'inj_on$e'('i$','top$a')
| ~ spl156_16 ),
inference(avatar_component_clause,[],[f3616]) ).
tff(f3644,plain,
( ( 'top$' = 'image$e'('i$','top$a') )
| ~ spl156_8 ),
inference(forward_demodulation,[],[f3537,f3455]) ).
tff(f3646,definition,
( spl156_21
<=> ( 'top$' = 'image$e'('i$','top$a') ) ),
introduced(definition,[new_symbols(definition,[spl156_21])],[avatar_definition]) ).
tff(f3647,plain,
( ( 'top$' = 'image$e'('i$','top$a') )
| ~ spl156_21 ),
inference(avatar_component_clause,[],[f3646]) ).
tff(f3660,plain,
( spl156_21
| ~ spl156_8 ),
inference(avatar_split_clause,[],[f3644,f3530,f3646]) ).
tff(f3676,plain,
( $false
| ~ spl156_7 ),
inference(unit_resulting_resolution,[],[f2622,f2069,f3294]) ).
tff(f3694,plain,
~ spl156_7,
inference(avatar_contradiction_clause,[],[f3676]) ).
tff(f3706,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ( 'top$' != 'top$' )
| ( X0 = X1 )
| ( 'fun_app$b'('fun_app$a'('comp$'(X0),'i$'),sK112('i$','top$a',X0,X1)) != 'fun_app$b'('fun_app$a'('comp$'(X1),'i$'),sK112('i$','top$a',X0,X1)) ) )
| ~ spl156_21 ),
inference(superposition,[],[f2126,f3647]) ).
tff(f3707,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ( X0 = X1 )
| ( 'fun_app$b'('fun_app$a'('comp$'(X0),'i$'),sK112('i$','top$a',X0,X1)) != 'fun_app$b'('fun_app$a'('comp$'(X1),'i$'),sK112('i$','top$a',X0,X1)) ) )
| ~ spl156_21 ),
inference(trivial_inequality_removal,[],[f3706]) ).
tff(f3708,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ( 'fun_app$b'('fun_app$a'('comp$'(X0),'i$'),sK112('i$','top$a',X0,X1)) != 'fun_app$c'(X1,'fun_app$d'('i$',sK112('i$','top$a',X0,X1))) )
| ( X0 = X1 ) )
| ~ spl156_21 ),
inference(forward_demodulation,[],[f3707,f2480]) ).
tff(f3712,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ( 'fun_app$c'(X1,'fun_app$d'('i$',sK112('i$','top$a',X0,X1))) != 'fun_app$c'(X0,'fun_app$d'('i$',sK112('i$','top$a',X0,X1))) )
| ( X0 = X1 ) )
| ~ spl156_21 ),
inference(forward_demodulation,[],[f3708,f2480]) ).
tff(f3828,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun$'] :
( ( 'top$a' != 'top$a' )
| ( 'fun_app$g'('j$',sK44('j$',X0)) = X0 ) )
| ~ spl156_5 ),
inference(superposition,[],[f1900,f3287]) ).
tff(f3829,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$g'('j$',sK44('j$',X0)) = X0 )
| ~ spl156_5 ),
inference(trivial_inequality_removal,[],[f3828]) ).
tff(f3834,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$d'('i$',X0) = sK44('j$',X0) )
| ~ spl156_5 ),
inference(superposition,[],[f2855,f3829]) ).
tff(f3835,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$b'('g$',X0) = 'fun_app$c'('f$',sK44('j$',X0)) )
| ~ spl156_5 ),
inference(superposition,[],[f2713,f3829]) ).
tff(f4382,plain,
'id$' = 'fun_app$f'('comp$a'('inv_into$c'('top$a','i$')),'i$'),
inference(resolution,[],[f2357,f1628]) ).
tff(f4387,plain,
! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'comp$j'(X0,'id$') = 'fun_app$a'('comp$'('comp$k'(X0,'inv_into$c'('top$a','i$'))),'i$') ),
inference(superposition,[],[f2593,f4382]) ).
tff(f4447,plain,
( ~ 'inj_on$e'('i$','top$a')
| spl156_16 ),
inference(avatar_component_clause,[],[f3616]) ).
tff(f4455,plain,
( ~ 'register$b'('i$')
| spl156_16 ),
inference(resolution,[],[f4447,f2008]) ).
tff(f4457,plain,
( $false
| spl156_16 ),
inference(forward_subsumption_resolution,[],[f4455,f1634]) ).
tff(f4458,plain,
spl156_16,
inference(avatar_contradiction_clause,[],[f4457]) ).
tff(f4472,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'fun_app$a'('comp$'('comp$k'(X0,'inv_into$c'('top$a','i$'))),'i$') = X0 )
| ~ spl156_16 ),
inference(resolution,[],[f3617,f2020]) ).
tff(f5043,plain,
( $false
| ~ spl156_9 ),
inference(unit_resulting_resolution,[],[f2900,f2715,f3534]) ).
tff(f5063,plain,
~ spl156_9,
inference(avatar_contradiction_clause,[],[f5043]) ).
tff(f5908,plain,
( ( 'top$' != 'top$' )
| ~ 'clinear$b'('i$')
| ( 'id$a' = 'fun_app$i'('comp$b'('i$'),sK131('i$')) )
| ~ spl156_21 ),
inference(superposition,[],[f2314,f3647]) ).
tff(f5913,plain,
( ~ 'clinear$b'('i$')
| ( 'id$a' = 'fun_app$i'('comp$b'('i$'),sK131('i$')) )
| ~ spl156_21 ),
inference(trivial_inequality_removal,[],[f5908]) ).
tff(f5922,plain,
( ( 'id$a' = 'fun_app$i'('comp$b'('i$'),sK131('i$')) )
| ~ spl156_21 ),
inference(forward_subsumption_resolution,[],[f5913,f2631]) ).
tff(f5931,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'comp$n'(X0,'id$a') = 'comp$k'('fun_app$a'('comp$'(X0),'i$'),sK131('i$')) )
| ~ spl156_21 ),
inference(superposition,[],[f2599,f5922]) ).
tff(f6985,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_set$'] :
( ~ 'inj_on$b'('id$a',X0)
| 'inj_on$f'('inv_into$c'('top$a','i$'),X0) ),
inference(superposition,[],[f1891,f3498]) ).
tff(f6999,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_set$'] : 'inj_on$f'('inv_into$c'('top$a','i$'),X0),
inference(forward_subsumption_resolution,[],[f6985,f2203]) ).
tff(f7035,plain,
! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'comp$k'('fun_app$a'('comp$'(X0),'inv_into$b'('top$','inv_into$c'('top$a','i$'))),'inv_into$c'('top$a','i$')) = X0 ),
inference(resolution,[],[f6999,f2016]) ).
tff(f7714,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun$'] :
( ( 'top$' != 'top$' )
| ( 'fun_app$d'('i$',sK48('i$',X0)) = X0 ) )
| ~ spl156_21 ),
inference(superposition,[],[f1904,f3647]) ).
tff(f7721,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$d'('i$',sK48('i$',X0)) = X0 )
| ~ spl156_21 ),
inference(trivial_inequality_removal,[],[f7714]) ).
tff(f7725,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( sK44('j$',sK48('i$',X0)) = X0 )
| ~ spl156_5
| ~ spl156_21 ),
inference(forward_demodulation,[],[f7721,f3834]) ).
tff(f7729,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$c'('f$',X0) = 'fun_app$b'('g$',sK48('i$',X0)) )
| ~ spl156_5
| ~ spl156_21 ),
inference(superposition,[],[f3835,f7725]) ).
tff(f9882,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'fun_app$a'('comp$'(X0),'i$') = 'fun_app$a'('comp$'(X0),'inv_into$b'('top$','inv_into$c'('top$a','i$'))) )
| ~ spl156_16 ),
inference(superposition,[],[f4472,f7035]) ).
tff(f9886,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'comp$j'(X0,'id$') = X0 )
| ~ spl156_16 ),
inference(superposition,[],[f4387,f4472]) ).
tff(f9890,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'comp$k'(X0,'inv_into$c'('top$a','i$')) = 'comp$n'('comp$k'(X0,'inv_into$c'('top$a','i$')),'id$a') )
| ~ spl156_16 ),
inference(superposition,[],[f3503,f4472]) ).
tff(f9891,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'comp$n'('comp$k'(X0,'inv_into$c'('top$a','i$')),'id$a') = 'comp$k'(X0,sK131('i$')) )
| ~ spl156_16
| ~ spl156_21 ),
inference(superposition,[],[f5931,f4472]) ).
tff(f9931,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'comp$k'(X0,'inv_into$c'('top$a','i$')) = 'comp$k'(X0,sK131('i$')) )
| ~ spl156_16
| ~ spl156_21 ),
inference(forward_demodulation,[],[f9890,f9891]) ).
tff(f10734,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'comp$k'('fun_app$a'('comp$'(X0),'i$'),'inv_into$c'('top$a','i$')) = X0 )
| ~ spl156_16 ),
inference(superposition,[],[f7035,f9882]) ).
tff(f10782,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'comp$k'('fun_app$a'('comp$'(X0),'i$'),sK131('i$')) = X0 )
| ~ spl156_16
| ~ spl156_21 ),
inference(forward_demodulation,[],[f10734,f9931]) ).
tff(f10819,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'comp$k'(X0,'j$') = 'comp$k'('comp$j'(X0,'id$'),sK131('i$')) )
| ~ spl156_16
| ~ spl156_21 ),
inference(superposition,[],[f10782,f2942]) ).
tff(f10831,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'comp$k'(X0,'j$') = 'comp$k'(X0,sK131('i$')) )
| ~ spl156_16
| ~ spl156_21 ),
inference(forward_demodulation,[],[f10819,f9886]) ).
tff(f11016,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'fun_app$a'('comp$'('comp$k'(X0,sK131('i$'))),'i$') = X0 )
| ~ spl156_16
| ~ spl156_21 ),
inference(superposition,[],[f4472,f9931]) ).
tff(f11037,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'fun_app$a'('comp$'('comp$k'(X0,'j$')),'i$') = X0 )
| ~ spl156_16
| ~ spl156_21 ),
inference(forward_demodulation,[],[f11016,f10831]) ).
tff(f11083,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$b'(X0,X1) = 'fun_app$c'('comp$k'(X0,'j$'),'fun_app$d'('i$',X1)) )
| ~ spl156_16
| ~ spl156_21 ),
inference(superposition,[],[f2480,f11037]) ).
tff(f11094,plain,
( ! [X0: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$',X1: 'B_ell2_b_ell2_cblinfun$'] : ( 'fun_app$b'(X0,X1) = 'fun_app$c'('comp$k'(X0,'j$'),sK44('j$',X1)) )
| ~ spl156_5
| ~ spl156_16
| ~ spl156_21 ),
inference(forward_demodulation,[],[f11083,f3834]) ).
tff(f14671,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun$',X1: 'B_ell2_b_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] : ( 'fun_app$c'('comp$k'(X1,'j$'),X0) = 'fun_app$b'(X1,sK48('i$',X0)) )
| ~ spl156_5
| ~ spl156_16
| ~ spl156_21 ),
inference(superposition,[],[f11094,f7725]) ).
tff(f14963,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun$'] : ( 'fun_app$c'('f$',X0) = 'fun_app$c'('comp$k'('g$','j$'),X0) )
| ~ spl156_5
| ~ spl156_16
| ~ spl156_21 ),
inference(superposition,[],[f7729,f14671]) ).
tff(f15038,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ( 'fun_app$c'('f$','fun_app$d'('i$',sK112('i$','top$a',X0,'comp$k'('g$','j$')))) != 'fun_app$c'(X0,'fun_app$d'('i$',sK112('i$','top$a',X0,'comp$k'('g$','j$')))) )
| ( 'comp$k'('g$','j$') = X0 ) )
| ~ spl156_5
| ~ spl156_16
| ~ spl156_21 ),
inference(superposition,[],[f3712,f14963]) ).
tff(f15050,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ( 'fun_app$c'('f$',sK44('j$',sK112('i$','top$a',X0,'comp$k'('g$','j$')))) != 'fun_app$c'(X0,sK44('j$',sK112('i$','top$a',X0,'comp$k'('g$','j$')))) )
| ( 'comp$k'('g$','j$') = X0 ) )
| ~ spl156_5
| ~ spl156_16
| ~ spl156_21 ),
inference(forward_demodulation,[],[f15038,f3834]) ).
tff(f15055,plain,
( ! [X0: 'A_ell2_a_ell2_cblinfun_c_ell2_c_ell2_cblinfun_fun$'] :
( ( 'fun_app$c'(X0,sK44('j$',sK112('i$','top$a',X0,'comp$k'('g$','j$')))) != 'fun_app$b'('g$',sK112('i$','top$a',X0,'comp$k'('g$','j$'))) )
| ( 'comp$k'('g$','j$') = X0 ) )
| ~ spl156_5
| ~ spl156_16
| ~ spl156_21 ),
inference(forward_demodulation,[],[f15050,f3835]) ).
tff(f15099,plain,
( ( 'fun_app$b'('g$',sK112('i$','top$a','f$','comp$k'('g$','j$'))) != 'fun_app$b'('g$',sK112('i$','top$a','f$','comp$k'('g$','j$'))) )
| ( 'f$' = 'comp$k'('g$','j$') )
| ~ spl156_5
| ~ spl156_16
| ~ spl156_21 ),
inference(superposition,[],[f15055,f3835]) ).
tff(f15102,plain,
( ( 'f$' = 'comp$k'('g$','j$') )
| ~ spl156_5
| ~ spl156_16
| ~ spl156_21 ),
inference(trivial_inequality_removal,[],[f15099]) ).
tff(f15116,plain,
( ( 'fun_app$a'('comp$'('f$'),'i$') = 'comp$j'('g$','id$') )
| ~ spl156_5
| ~ spl156_16
| ~ spl156_21 ),
inference(superposition,[],[f2942,f15102]) ).
tff(f15137,plain,
( ( 'fun_app$a'('comp$'('f$'),'i$') = 'g$' )
| ~ spl156_5
| ~ spl156_16
| ~ spl156_21 ),
inference(forward_demodulation,[],[f15116,f9886]) ).
tff(f15143,plain,
( $false
| ~ spl156_5
| ~ spl156_16
| ~ spl156_21 ),
inference(forward_subsumption_resolution,[],[f15137,f1625]) ).
tff(f15144,plain,
( ~ spl156_5
| ~ spl156_16
| ~ spl156_21 ),
inference(avatar_contradiction_clause,[],[f15143]) ).
cnf(s7,plain,
( spl156_5
| spl156_7 ),
inference(sat_conversion,[],[f3298]) ).
cnf(s26,plain,
( spl156_8
| spl156_9 ),
inference(sat_conversion,[],[f3535]) ).
cnf(s39,plain,
( ~ spl156_8
| spl156_21 ),
inference(sat_conversion,[],[f3660]) ).
cnf(s56,plain,
~ spl156_7,
inference(sat_conversion,[],[f3694]) ).
cnf(s60,plain,
spl156_16,
inference(sat_conversion,[],[f4458]) ).
cnf(s70,plain,
~ spl156_9,
inference(sat_conversion,[],[f5063]) ).
cnf(s164,plain,
( ~ spl156_5
| ~ spl156_16
| ~ spl156_21 ),
inference(sat_conversion,[],[f15144]) ).
cnf(s180,plain,
spl156_8,
inference(rat,[],[s26,s70]) ).
cnf(s181,plain,
spl156_21,
inference(rat,[],[s39,s180]) ).
cnf(s185,plain,
~ spl156_5,
inference(rat,[],[s164,s60,s181]) ).
cnf(s188,plain,
$false,
inference(rat,[],[s7,s56,s185]) ).
tff(f15147,plain,
$false,
inference(avatar_sat_refutation,[],[s188]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP397_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.38 % Computer : n016.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sun Sep 27 13:01:32 UTC 2026
% 0.09/0.39 % CPUTime :
% 0.09/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.42 Running first-order theorem proving
% 0.09/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.08/4.01 % (2619153)Detected formulas, will run a generic FOF schedule.
% 21.08/4.01 % (2619239)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1568260069:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 21.08/4.01 % (2619240)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1040712140:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 21.08/4.01 % (2619240)Refutation not found, incomplete strategy
% 21.08/4.01 % (2619240)------------------------------
% 21.08/4.01 % (2619240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.08/4.01 % (2619240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.08/4.01 % (2619240)CaDiCaL version: 2.1.3
% 21.08/4.01 % (2619240)Termination reason: Refutation not found, incomplete strategy
% 21.08/4.01 % (2619240)Time elapsed: 0.005 s
% 21.08/4.01 % (2619240)Peak memory usage: 88 MB
% 21.08/4.01 % (2619240)Instructions burned: 2 (million)
% 21.08/4.01 % (2619234)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1761763055:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 21.08/4.01 % (2619233)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=772263590:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 21.08/4.01 % (2619241)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2018861836:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 21.08/4.01 % (2619242)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1397624264:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 21.08/4.01 % (2619244)dis-21_1_sil=8000:lcm=predicate:random_seed=3193521514:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 21.08/4.01 % (2619244)Instruction limit reached!
% 21.08/4.01 % (2619244)------------------------------
% 21.08/4.01 % (2619244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.08/4.01 % (2619244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.08/4.01 % (2619244)CaDiCaL version: 2.1.3
% 21.08/4.01 % (2619244)Termination reason: Instruction limit
% 21.08/4.01 % (2619244)Termination phase: Saturation
% 21.08/4.01 % (2619244)Time elapsed: 0.123 s
% 21.08/4.01 % (2619244)Peak memory usage: 91 MB
% 21.08/4.01 % (2619244)Instructions burned: 130 (million)
% 21.08/4.01 % (2619241)Instruction limit reached!
% 21.08/4.01 % (2619241)------------------------------
% 21.08/4.01 % (2619241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.08/4.01 % (2619241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.08/4.01 % (2619241)CaDiCaL version: 2.1.3
% 21.08/4.01 % (2619241)Termination reason: Instruction limit
% 21.08/4.01 % (2619241)Termination phase: Saturation
% 21.08/4.01 % (2619241)Time elapsed: 0.123 s
% 21.08/4.01 % (2619241)Peak memory usage: 89 MB
% 21.08/4.01 % (2619241)Instructions burned: 119 (million)
% 21.08/4.01 % (2619242)Instruction limit reached!
% 21.08/4.01 % (2619242)------------------------------
% 21.08/4.01 % (2619242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.08/4.01 % (2619242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.08/4.01 % (2619242)CaDiCaL version: 2.1.3
% 21.08/4.01 % (2619242)Termination reason: Instruction limit
% 21.08/4.01 % (2619242)Termination phase: Saturation
% 21.08/4.01 % (2619242)Time elapsed: 0.149 s
% 21.08/4.01 % (2619242)Peak memory usage: 91 MB
% 21.08/4.01 % (2619242)Instructions burned: 139 (million)
% 21.08/4.01 % (2619240)------------------------------
% 21.08/4.01 % (2619240)------------------------------
% 21.08/4.01 % (2619275)lrs+10_1_sil=8000:sp=occurrence:random_seed=1991190520:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 21.08/4.01 % (2619276)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2820906028:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 21.08/4.01 % (2619276)Refutation not found, incomplete strategy
% 21.08/4.01 % (2619276)------------------------------
% 21.08/4.01 % (2619276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.08/4.01 % (2619276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.64/4.56 % (2619276)CaDiCaL version: 2.1.3
% 25.64/4.56 % (2619276)Termination reason: Refutation not found, incomplete strategy
% 25.64/4.56 % (2619276)Time elapsed: 0.011 s
% 25.64/4.56 % (2619276)Peak memory usage: 89 MB
% 25.64/4.56 % (2619276)Instructions burned: 10 (million)
% 25.64/4.56 % (2619278)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1281250652:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 25.64/4.56 % (2619278)Refutation not found, incomplete strategy
% 25.64/4.56 % (2619278)------------------------------
% 25.64/4.56 % (2619278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.64/4.56 % (2619278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.64/4.56 % (2619278)CaDiCaL version: 2.1.3
% 25.64/4.56 % (2619278)Termination reason: Refutation not found, incomplete strategy
% 25.64/4.56 % (2619278)Time elapsed: 0.005 s
% 25.64/4.56 % (2619278)Peak memory usage: 88 MB
% 25.64/4.56 % (2619278)Instructions burned: 3 (million)
% 25.64/4.56 % (2619275)Instruction limit reached!
% 25.64/4.56 % (2619275)------------------------------
% 25.64/4.56 % (2619275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.64/4.56 % (2619275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.64/4.56 % (2619275)CaDiCaL version: 2.1.3
% 25.64/4.56 % (2619275)Termination reason: Instruction limit
% 25.64/4.56 % (2619275)Termination phase: Saturation
% 25.64/4.56 % (2619275)Time elapsed: 0.226 s
% 25.64/4.56 % (2619275)Peak memory usage: 91 MB
% 25.64/4.56 % (2619275)Instructions burned: 286 (million)
% 25.64/4.56 % (2619281)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=225710508:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 25.64/4.56 % (2619276)------------------------------
% 25.64/4.56 % (2619276)------------------------------
% 25.64/4.56 % (2619278)------------------------------
% 25.64/4.56 % (2619278)------------------------------
% 25.64/4.56 % (2619288)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=403116155:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2990 on theBenchmark for (2990ds/294Mi)
% 25.64/4.56 % (2619281)Instruction limit reached!
% 25.64/4.56 % (2619281)------------------------------
% 25.64/4.56 % (2619281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.64/4.56 % (2619281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.64/4.56 % (2619281)CaDiCaL version: 2.1.3
% 25.64/4.56 % (2619281)Termination reason: Instruction limit
% 25.64/4.56 % (2619281)Termination phase: Saturation
% 25.64/4.56 % (2619281)Time elapsed: 0.247 s
% 25.64/4.56 % (2619281)Peak memory usage: 91 MB
% 25.64/4.56 % (2619281)Instructions burned: 249 (million)
% 25.64/4.56 % (2619288)Refutation not found, incomplete strategy
% 25.64/4.56 % (2619288)------------------------------
% 25.64/4.56 % (2619288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.64/4.56 % (2619288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.64/4.56 % (2619288)CaDiCaL version: 2.1.3
% 25.64/4.56 % (2619288)Termination reason: Refutation not found, incomplete strategy
% 25.64/4.56 % (2619288)Time elapsed: 0.045 s
% 25.64/4.56 % (2619288)Peak memory usage: 90 MB
% 25.64/4.56 % (2619288)Instructions burned: 43 (million)
% 25.64/4.56 % (2619293)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1506288353:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 25.64/4.56 % (2619294)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=139645126:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 25.64/4.56 % (2619297)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=327658418:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 25.64/4.56 % (2619294)Instruction limit reached!
% 25.64/4.56 % (2619294)------------------------------
% 25.64/4.56 % (2619294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.64/4.56 % (2619294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.64/4.56 % (2619294)CaDiCaL version: 2.1.3
% 25.64/4.56 % (2619294)Termination reason: Instruction limit
% 25.64/4.56 % (2619294)Termination phase: Saturation
% 25.64/4.56 % (2619294)Time elapsed: 0.112 s
% 25.64/4.56 % (2619294)Peak memory usage: 91 MB
% 25.64/4.56 % (2619294)Instructions burned: 113 (million)
% 25.64/4.56 % (2619297)Refutation not found, incomplete strategy
% 25.64/4.56 % (2619297)------------------------------
% 25.64/4.56 % (2619297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.64/4.56 % (2619297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.64/4.56 % (2619297)CaDiCaL version: 2.1.3
% 25.64/4.56 % (2619297)Termination reason: Refutation not found, incomplete strategy
% 25.64/4.56 % (2619297)Time elapsed: 0.038 s
% 25.64/4.56 % (2619297)Peak memory usage: 89 MB
% 25.64/4.56 % (2619297)Instructions burned: 41 (million)
% 25.64/4.56 % (2619288)------------------------------
% 25.64/4.56 % (2619288)------------------------------
% 25.64/4.56 % (2619302)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=697308734:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 25.64/4.56 % (2619297)------------------------------
% 25.64/4.56 % (2619297)------------------------------
% 25.64/4.56 % (2619302)Instruction limit reached!
% 25.64/4.56 % (2619302)------------------------------
% 25.64/4.56 % (2619302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.64/4.56 % (2619302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.64/4.56 % (2619302)CaDiCaL version: 2.1.3
% 25.64/4.56 % (2619302)Termination reason: Instruction limit
% 25.64/4.56 % (2619302)Termination phase: Saturation
% 25.64/4.56 % (2619302)Time elapsed: 0.111 s
% 25.64/4.56 % (2619302)Peak memory usage: 90 MB
% 25.64/4.56 % (2619302)Instructions burned: 114 (million)
% 25.64/4.56 % (2619304)lrs+10_1_sil=8000:sp=occurrence:random_seed=3452877152:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2983 on theBenchmark for (2983ds/907Mi)
% 25.64/4.56 % (2619309)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=757257035:i=437:sd=1:aac=none:ss=included_2981 on theBenchmark for (2981ds/437Mi)
% 25.64/4.56 % (2619310)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=100945067:i=5202:ss=axioms:sgt=16_2980 on theBenchmark for (2980ds/5202Mi)
% 25.64/4.56 % (2619309)Instruction limit reached!
% 25.64/4.56 % (2619309)------------------------------
% 25.64/4.56 % (2619309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.64/4.56 % (2619309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.64/4.56 % (2619309)CaDiCaL version: 2.1.3
% 25.64/4.56 % (2619309)Termination reason: Instruction limit
% 25.64/4.56 % (2619309)Termination phase: Saturation
% 25.64/4.56 % (2619309)Time elapsed: 0.207 s
% 25.64/4.56 % (2619309)Peak memory usage: 92 MB
% 25.64/4.56 % (2619309)Instructions burned: 439 (million)
% 25.64/4.56 % (2619318)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1735664798:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2977 on theBenchmark for (2977ds/134Mi)
% 25.64/4.56 % (2619318)Instruction limit reached!
% 25.64/4.56 % (2619318)------------------------------
% 25.64/4.56 % (2619318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.64/4.56 % (2619318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.64/4.56 % (2619318)CaDiCaL version: 2.1.3
% 25.64/4.56 % (2619318)Termination reason: Instruction limit
% 25.64/4.56 % (2619318)Termination phase: Saturation
% 25.64/4.56 % (2619318)Time elapsed: 0.145 s
% 25.64/4.56 % (2619318)Peak memory usage: 92 MB
% 25.64/4.56 % (2619318)Instructions burned: 134 (million)
% 25.64/4.56 % (2619304)Instruction limit reached!
% 25.64/4.56 % (2619304)------------------------------
% 25.64/4.56 % (2619304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.64/4.56 % (2619304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.64/4.56 % (2619304)CaDiCaL version: 2.1.3
% 25.64/4.56 % (2619304)Termination reason: Instruction limit
% 25.64/4.56 % (2619304)Termination phase: Saturation
% 25.64/4.56 % (2619304)Time elapsed: 0.877 s
% 25.64/4.56 % (2619304)Peak memory usage: 99 MB
% 25.64/4.56 % (2619304)Instructions burned: 907 (million)
% 25.64/4.56 % (2619320)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3413355155:st=8:i=592:sd=3:ep=RST:ss=axioms_2972 on theBenchmark for (2972ds/592Mi)
% 25.64/4.56 % (2619323)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=658703348:st=3:i=13193:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/13193Mi)
% 25.64/4.56 % (2619293)Instruction limit reached!
% 25.64/4.56 % (2619293)------------------------------
% 25.64/4.56 % (2619293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.64/4.56 % (2619293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.64/4.56 % (2619293)CaDiCaL version: 2.1.3
% 25.64/4.56 % (2619293)Termination reason: Instruction limit
% 25.64/4.56 % (2619293)Termination phase: Saturation
% 25.64/4.56 % (2619293)Time elapsed: 1.788 s
% 25.64/4.56 % (2619293)Peak memory usage: 143 MB
% 25.64/4.56 % (2619293)Instructions burned: 2350 (million)
% 25.64/4.56 % (2619234)First to succeed.
% 25.64/4.56 % (2619234)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2619153"
% 25.64/4.56 % (2619326)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1729685409:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/125Mi)
% 25.64/4.56 % (2619326)Instruction limit reached!
% 25.64/4.56 % (2619326)------------------------------
% 25.64/4.56 % (2619326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.64/4.56 % (2619326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.64/4.56 % (2619326)CaDiCaL version: 2.1.3
% 25.64/4.56 % (2619326)Termination reason: Instruction limit
% 25.64/4.56 % (2619326)Termination phase: Saturation
% 25.64/4.56 % (2619326)Time elapsed: 0.070 s
% 25.64/4.56 % (2619326)Peak memory usage: 91 MB
% 25.64/4.56 % (2619326)Instructions burned: 126 (million)
% 25.64/4.56 % (2619320)Instruction limit reached!
% 25.64/4.56 % (2619320)------------------------------
% 25.64/4.56 % (2619320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.64/4.56 % (2619320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.64/4.56 % (2619320)CaDiCaL version: 2.1.3
% 25.64/4.56 % (2619320)Termination reason: Instruction limit
% 25.64/4.56 % (2619320)Termination phase: Saturation
% 25.64/4.56 % (2619320)Time elapsed: 0.566 s
% 25.64/4.56 % (2619320)Peak memory usage: 93 MB
% 25.64/4.56 % (2619320)Instructions burned: 593 (million)
% 25.64/4.56 % (2619234)Refutation found. Thanks to Tanya!
% 25.64/4.56 % SZS status Theorem for theBenchmark
% 25.64/4.56 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/4.81 % (2619234)------------------------------
% 0.17/4.81 % (2619234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/4.81 % (2619234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/4.81 % (2619234)CaDiCaL version: 2.1.3
% 0.17/4.81 % (2619234)Termination reason: Refutation
% 0.17/4.81 % (2619234)Time elapsed: 2.969 s
% 0.17/4.81 % (2619234)Peak memory usage: 151 MB
% 0.17/4.81 % (2619234)Instructions burned: 3104 (million)
% 0.17/4.81 % (2619234)------------------------------
% 0.17/4.81 % (2619234)------------------------------
% 0.17/4.81 % (2619153)Success in time 3.697 s
% 0.17/4.81 % Vampire exiting
%------------------------------------------------------------------------------