%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP387_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 : n008.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:46 AM UTC 2026
% Result : Theorem 79.08s 26.66s
% Output : Refutation 184.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 21
% Syntax : Number of formulae : 68 ( 68 unt; 0 typ; 14 def)
% Number of atoms : 68 ( 67 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 13 ( 13 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of FOOLs : 1 ( 1 fml; 0 var)
% Number of types : 147 ( 146 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 54 ( 52 usr; 1 prp; 0-4 aty)
% Number of functors : 447 ( 447 usr; 47 con; 0-4 aty)
% Number of variables : 39 ( 39 !; 0 ?; 39 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'A_a_prod_ell2$': $tType ).
tff(type_def_6,type,
'D_ell2_b_d_prod_ell2_cblinfun$': $tType ).
tff(type_def_7,type,
'A_ell2_a_ell2_cblinfun$': $tType ).
tff(type_def_8,type,
'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_fun$': $tType ).
tff(type_def_9,type,
'B_d_prod_ell2_a_c_prod_ell2_cblinfun$': $tType ).
tff(type_def_10,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod_bool_fun$': $tType ).
tff(type_def_11,type,
'B_d_prod$': $tType ).
tff(type_def_12,type,
'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod_bool_fun$': $tType ).
tff(type_def_13,type,
'B_ell2_b_ell2_cblinfun$': $tType ).
tff(type_def_14,type,
'C_a_c_prod_prod_ell2$': $tType ).
tff(type_def_15,type,
'D_ell2_complex_cblinfun$': $tType ).
tff(type_def_16,type,
'A_c_fun$': $tType ).
tff(type_def_17,type,
'A_c_prod_a_c_prod_ell2_fun$': $tType ).
tff(type_def_18,type,
'A_a_prod$': $tType ).
tff(type_def_19,type,
'Complex_d_ell2_cblinfun$': $tType ).
tff(type_def_20,type,
'A_c_bool_fun_fun$': $tType ).
tff(type_def_21,type,
'A_a_prod_ell2_a_c_prod_ell2_cblinfun$': $tType ).
tff(type_def_22,type,
'A_c_prod_a_c_prod_bool_fun_fun$': $tType ).
tff(type_def_23,type,
'Complex_a_c_prod_ell2_prod$': $tType ).
tff(type_def_24,type,
'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$': $tType ).
tff(type_def_25,type,
'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun_fun$': $tType ).
tff(type_def_26,type,
'A_c_prod_c_a_prod_fun$': $tType ).
tff(type_def_27,type,
'C_c_prod$': $tType ).
tff(type_def_28,type,
'C_ell2_d_ell2_cblinfun$': $tType ).
tff(type_def_29,type,
'A_c_prod_c_prod$': $tType ).
tff(type_def_30,type,
'A_c_prod_ell2$': $tType ).
tff(type_def_31,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_b_d_prod_ell2_cblinfun$': $tType ).
tff(type_def_32,type,
'A_c_prod_a_c_prod_prod_ell2_set$': $tType ).
tff(type_def_33,type,
'C_a_prod_set$': $tType ).
tff(type_def_34,type,
'C_ell2_d_ell2_cblinfun_set$': $tType ).
tff(type_def_35,type,
'A_c_prod_ell2_b_d_prod_ell2_fun$': $tType ).
tff(type_def_36,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_complex_fun$': $tType ).
tff(type_def_37,type,
'C_a_prod_ell2_d_b_prod_ell2_cblinfun$': $tType ).
tff(type_def_38,type,
'C_ell2_c_ell2_cblinfun$': $tType ).
tff(type_def_39,type,
'C_c_fun$': $tType ).
tff(type_def_40,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$': $tType ).
tff(type_def_41,type,
'D_ell2$': $tType ).
tff(type_def_42,type,
'C_a_prod$': $tType ).
tff(type_def_43,type,
'B_d_prod_ell2_itself$': $tType ).
tff(type_def_44,type,
'C_c_prod_ell2$': $tType ).
tff(type_def_45,type,
'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun_c_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun_bool_fun_fun$': $tType ).
tff(type_def_46,type,
'D$': $tType ).
tff(type_def_47,type,
'D_b_prod_ell2$': $tType ).
tff(type_def_48,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$': $tType ).
tff(type_def_49,type,
'B_d_prod_b_d_prod_prod_ell2$': $tType ).
tff(type_def_50,type,
'Complex_d_ell2_prod$': $tType ).
tff(type_def_51,type,
'B_d_prod_ell2_b_d_prod_ell2_cblinfun$': $tType ).
tff(type_def_52,type,
'B$': $tType ).
tff(type_def_53,type,
'A_c_prod_a_c_prod_prod_bool_fun$': $tType ).
tff(type_def_54,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod_set$': $tType ).
tff(type_def_55,type,
'D_d_prod_ell2$': $tType ).
tff(type_def_56,type,
'A_c_prod_a_prod$': $tType ).
tff(type_def_57,type,
'C_a_c_prod_fun$': $tType ).
tff(type_def_58,type,
'B_d_prod_ell2_a_c_prod_ell2_fun$': $tType ).
tff(type_def_59,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$': $tType ).
tff(type_def_60,type,
'B_d_prod_ell2_set$': $tType ).
tff(type_def_61,type,
'A_c_prod_ell2_ccsubspace$': $tType ).
tff(type_def_62,type,
'A_ell2_set$': $tType ).
tff(type_def_63,type,
'Complex_complex_cblinfun$': $tType ).
tff(type_def_64,type,
'A_c_prod_a_c_prod_prod$': $tType ).
tff(type_def_65,type,
'Complex$': $tType ).
tff(type_def_66,type,
'C_ell2_d_ell2_cblinfun_complex_fun$': $tType ).
tff(type_def_67,type,
'C$': $tType ).
tff(type_def_68,type,
'A_c_prod_c_prod_ell2$': $tType ).
tff(type_def_69,type,
'B_b_prod_ell2$': $tType ).
tff(type_def_70,type,
'C_ell2_d_ell2_fun$': $tType ).
tff(type_def_71,type,
'A_c_prod_bool_fun$': $tType ).
tff(type_def_72,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun_bool_fun_fun$': $tType ).
tff(type_def_73,type,
'A_c_prod_a_c_prod_fun$': $tType ).
tff(type_def_74,type,
'C_ell2_d_ell2_cblinfun_set_set$': $tType ).
tff(type_def_75,type,
'C_ell2$': $tType ).
tff(type_def_76,type,
'C_a_bool_fun_fun$': $tType ).
tff(type_def_77,type,
'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$': $tType ).
tff(type_def_78,type,
'C_ell2_d_ell2_cblinfun_bool_fun$': $tType ).
tff(type_def_79,type,
'A_a_c_prod_prod_ell2$': $tType ).
tff(type_def_80,type,
'A_a_prod_ell2_b_b_prod_ell2_cblinfun$': $tType ).
tff(type_def_81,type,
'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$': $tType ).
tff(type_def_82,type,
'B_ell2_b_d_prod_ell2_cblinfun$': $tType ).
tff(type_def_83,type,
'D_ell2_c_ell2_cblinfun$': $tType ).
tff(type_def_84,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun$': $tType ).
tff(type_def_85,type,
'A_c_prod_ell2_set$': $tType ).
tff(type_def_86,type,
'D_ell2_set$': $tType ).
tff(type_def_87,type,
'A_ell2_b_ell2_fun$': $tType ).
tff(type_def_88,type,
'B_d_prod_ell2_bool_fun$': $tType ).
tff(type_def_89,type,
'A_c_prod_set$': $tType ).
tff(type_def_90,type,
'A_c_prod_ell2_bool_fun$': $tType ).
tff(type_def_91,type,
'B_d_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$': $tType ).
tff(type_def_92,type,
'C_c_prod_ell2_b_d_prod_ell2_cblinfun$': $tType ).
tff(type_def_93,type,
'D_ell2_complex_prod$': $tType ).
tff(type_def_94,type,
'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$': $tType ).
tff(type_def_95,type,
'A_a_c_prod_prod$': $tType ).
tff(type_def_96,type,
'A_c_a_c_prod_fun_fun$': $tType ).
tff(type_def_97,type,
'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod_set$': $tType ).
tff(type_def_98,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set_set$': $tType ).
tff(type_def_99,type,
'C_ell2_a_ell2_cblinfun$': $tType ).
tff(type_def_100,type,
'B_d_prod_ell2_ccsubspace$': $tType ).
tff(type_def_101,type,
'A_bool_fun$': $tType ).
tff(type_def_102,type,
'A_set$': $tType ).
tff(type_def_103,type,
'C_a_prod_a_c_prod_fun$': $tType ).
tff(type_def_104,type,
'B_ell2_a_c_prod_ell2_cblinfun$': $tType ).
tff(type_def_105,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun$': $tType ).
tff(type_def_106,type,
'C_bool_fun$': $tType ).
tff(type_def_107,type,
'A_ell2$': $tType ).
tff(type_def_108,type,
'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun_fun$': $tType ).
tff(type_def_109,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun_fun$': $tType ).
tff(type_def_110,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_cblinfun$': $tType ).
tff(type_def_111,type,
'A$': $tType ).
tff(type_def_112,type,
'A_c_prod$': $tType ).
tff(type_def_113,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun$': $tType ).
tff(type_def_114,type,
'C_a_c_prod_prod$': $tType ).
tff(type_def_115,type,
'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod_bool_fun$': $tType ).
tff(type_def_116,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_fun_fun$': $tType ).
tff(type_def_117,type,
'A_c_prod_a_prod_ell2$': $tType ).
tff(type_def_118,type,
'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$': $tType ).
tff(type_def_119,type,
'Complex_set$': $tType ).
tff(type_def_120,type,
'C_ell2_b_ell2_cblinfun$': $tType ).
tff(type_def_121,type,
'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_cblinfun$': $tType ).
tff(type_def_122,type,
'A_a_fun$': $tType ).
tff(type_def_123,type,
'A_c_prod_ell2_itself$': $tType ).
tff(type_def_124,type,
'C_a_prod_ell2_a_c_prod_ell2_cblinfun$': $tType ).
tff(type_def_125,type,
'C_a_prod_ell2$': $tType ).
tff(type_def_126,type,
'D_ell2_a_c_prod_ell2_cblinfun$': $tType ).
tff(type_def_127,type,
'C_a_prod_bool_fun$': $tType ).
tff(type_def_128,type,
'C_ell2_set$': $tType ).
tff(type_def_129,type,
'A_c_prod_a_c_prod_prod_set$': $tType ).
tff(type_def_130,type,
'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_cblinfun$': $tType ).
tff(type_def_131,type,
'C_a_prod_ell2_b_d_prod_ell2_cblinfun$': $tType ).
tff(type_def_132,type,
'B_ell2_a_ell2_cblinfun$': $tType ).
tff(type_def_133,type,
'A_c_prod_ell2_a_c_prod_ell2_cblinfun$': $tType ).
tff(type_def_134,type,
'D_ell2_d_ell2_prod$': $tType ).
tff(type_def_135,type,
'C_c_prod_ell2_a_c_prod_ell2_cblinfun$': $tType ).
tff(type_def_136,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_cblinfun$': $tType ).
tff(type_def_137,type,
'Complex_complex_prod$': $tType ).
tff(type_def_138,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun_fun$': $tType ).
tff(type_def_139,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$': $tType ).
tff(type_def_140,type,
'D_ell2_d_ell2_cblinfun$': $tType ).
tff(type_def_141,type,
'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod_set$': $tType ).
tff(type_def_142,type,
'A_ell2_d_ell2_cblinfun$': $tType ).
tff(type_def_143,type,
'A_ell2_b_ell2_cblinfun$': $tType ).
tff(type_def_144,type,
'A_ell2_c_ell2_cblinfun$': $tType ).
tff(type_def_145,type,
'B_d_prod_ell2_a_c_prod_a_c_prod_prod_ell2_cblinfun$': $tType ).
tff(type_def_146,type,
'A_c_prod_a_c_prod_prod_ell2$': $tType ).
tff(type_def_147,type,
'B_ell2$': $tType ).
tff(type_def_148,type,
'B_d_prod_ell2$': $tType ).
tff(type_def_149,type,
'A_c_prod_ell2_complex_prod$': $tType ).
tff(type_def_150,type,
'C_c_prod_ell2_d_d_prod_ell2_cblinfun$': $tType ).
tff(func_def_0,type,
'less_eq$a': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun$' ).
tff(func_def_1,type,
'tensor_op$l': ( 'B_ell2_a_ell2_cblinfun$' * 'D_ell2_c_ell2_cblinfun$' ) > 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' ).
tff(func_def_2,type,
'cblinfun_extension$e': ( 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_fun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_3,type,
'image$d': ( 'A_c_prod_a_c_prod_fun$' * 'A_c_prod_set$' ) > 'A_c_prod_set$' ).
tff(func_def_4,type,
'tensor_ell2$j': ( 'A_c_prod_ell2$' * 'C_ell2$' ) > 'A_c_prod_c_prod_ell2$' ).
tff(func_def_5,type,
'pair$c': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ).
tff(func_def_6,type,
'fst$e': 'A_c_prod$' > 'A$' ).
tff(func_def_7,type,
'cspan$b': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ).
tff(func_def_8,type,
'cblinfun_apply$ab': ( 'D_ell2_b_d_prod_ell2_cblinfun$' * 'D_ell2$' ) > 'B_d_prod_ell2$' ).
tff(func_def_9,type,
'tensor_op$k': ( 'A_ell2_b_ell2_cblinfun$' * 'A_ell2_b_ell2_cblinfun$' ) > 'A_a_prod_ell2_b_b_prod_ell2_cblinfun$' ).
tff(func_def_10,type,
'cblinfun_apply$d': ( 'C_a_prod_ell2_b_d_prod_ell2_cblinfun$' * 'C_a_prod_ell2$' ) > 'B_d_prod_ell2$' ).
tff(func_def_11,type,
'plus$aa': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set_set$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set_set$' ).
tff(func_def_12,type,
'collect$': 'C_a_prod_bool_fun$' > 'C_a_prod_set$' ).
tff(func_def_13,type,
'tensor_ell2$l': ( 'C_ell2$' * 'A_c_prod_ell2$' ) > 'C_a_c_prod_prod_ell2$' ).
tff(func_def_14,type,
'plus$v': ( 'B_d_prod_ell2_set$' * 'B_d_prod_ell2_set$' ) > 'B_d_prod_ell2_set$' ).
tff(func_def_15,type,
'fst$h': 'D_ell2_complex_prod$' > 'D_ell2$' ).
tff(func_def_16,type,
'cblinfun_apply$f': ( 'A_ell2_d_ell2_cblinfun$' * 'A_ell2$' ) > 'D_ell2$' ).
tff(func_def_17,type,
'pair$s': ( 'C$' * 'A_c_prod$' ) > 'C_a_c_prod_prod$' ).
tff(func_def_18,type,
'cblinfun_apply$': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_fun_fun$' ).
tff(func_def_19,type,
'fst$': 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_20,type,
'snd$f': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_21,type,
'plus$r': ( 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' * 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' ) > 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' ).
tff(func_def_22,type,
'tensor_ell2$d': ( 'D_ell2$' * 'B_ell2$' ) > 'D_b_prod_ell2$' ).
tff(func_def_23,type,
'cblinfun_apply$i': ( 'A_ell2_c_ell2_cblinfun$' * 'A_ell2$' ) > 'C_ell2$' ).
tff(func_def_24,type,
'minus$a': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_25,type,
'fun_app$aj': ( 'A_c_prod_a_c_prod_fun$' * 'A_c_prod$' ) > 'A_c_prod$' ).
tff(func_def_26,type,
'image$b': ( 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$' * 'C_ell2_d_ell2_cblinfun_set$' ) > 'C_ell2_d_ell2_cblinfun_set$' ).
tff(func_def_27,type,
'snd$l': 'Complex_a_c_prod_ell2_prod$' > 'A_c_prod_ell2$' ).
tff(func_def_28,type,
'image$c': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ).
tff(func_def_29,type,
'plus$j': ( 'Complex_d_ell2_prod$' * 'Complex_d_ell2_prod$' ) > 'Complex_d_ell2_prod$' ).
tff(func_def_30,type,
'fun_app$q': ( 'A_c_a_c_prod_fun_fun$' * 'A$' ) > 'C_a_c_prod_fun$' ).
tff(func_def_31,type,
'fst$f': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_32,type,
'cblinfun_apply$y': ( 'D_ell2_c_ell2_cblinfun$' * 'D_ell2$' ) > 'C_ell2$' ).
tff(func_def_33,type,
'ket$m': 'C_a_c_prod_prod$' > 'C_a_c_prod_prod_ell2$' ).
tff(func_def_34,type,
'b2$': 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_35,type,
'tensor_op$n': ( 'B_ell2_a_c_prod_ell2_cblinfun$' * 'D_ell2_a_c_prod_ell2_cblinfun$' ) > 'B_d_prod_ell2_a_c_prod_a_c_prod_prod_ell2_cblinfun$' ).
tff(func_def_36,type,
'pair$k': ( 'A_c_prod$' * 'A_c_prod$' ) > 'A_c_prod_a_c_prod_prod$' ).
tff(func_def_37,type,
'tensor_op$g': ( 'C_ell2_b_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun$' ) > 'C_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_38,type,
'cblinfun_apply$ai': ( 'Complex_complex_cblinfun$' * 'Complex$' ) > 'Complex$' ).
tff(func_def_39,type,
'plus$f': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' ).
tff(func_def_40,type,
'apfst$': ( 'A_a_fun$' * 'A_c_prod$' ) > 'A_c_prod$' ).
tff(func_def_41,type,
'fun_app$l': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_fun_fun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_fun$' ).
tff(func_def_42,type,
'tensor_ell2$': ( 'B_ell2$' * 'D_ell2$' ) > 'B_d_prod_ell2$' ).
tff(func_def_43,type,
'ket$f': 'C_c_prod$' > 'C_c_prod_ell2$' ).
tff(func_def_44,type,
'cblinfun_extension$b': ( 'B_d_prod_ell2_set$' * 'B_d_prod_ell2_a_c_prod_ell2_fun$' ) > 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' ).
tff(func_def_45,type,
'plus$d': ( 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' * 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' ) > 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' ).
tff(func_def_46,type,
'cblinfun_apply$l': ( 'C_ell2_c_ell2_cblinfun$' * 'C_ell2$' ) > 'C_ell2$' ).
tff(func_def_47,type,
'cblinfun_apply$ah': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_48,type,
'plus$s': ( 'A_ell2_b_ell2_cblinfun$' * 'A_ell2_b_ell2_cblinfun$' ) > 'A_ell2_b_ell2_cblinfun$' ).
tff(func_def_49,type,
'cblinfun_apply$af': ( 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_cblinfun$' * 'C_ell2_d_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_50,type,
'pair$m': ( 'A$' * 'A$' ) > 'A_a_prod$' ).
tff(func_def_51,type,
'fun_app$t': ( 'A_ell2_b_ell2_fun$' * 'A_ell2$' ) > 'B_ell2$' ).
tff(func_def_52,type,
'collect$c': 'A_c_prod_ell2_bool_fun$' > 'A_c_prod_ell2_set$' ).
tff(func_def_53,type,
'cblinfun_apply$ag': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_54,type,
'tensor_op$b': ( 'C_ell2_b_ell2_cblinfun$' * 'A_ell2_d_ell2_cblinfun$' ) > 'C_a_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_55,type,
'fun_app$u': ( 'C_ell2_d_ell2_fun$' * 'C_ell2$' ) > 'D_ell2$' ).
tff(func_def_56,type,
'tensor_op$d': ( 'C_ell2_a_ell2_cblinfun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'C_c_prod_ell2_a_c_prod_ell2_cblinfun$' ).
tff(func_def_57,type,
'fun_app$al': ( 'C_c_fun$' * 'C$' ) > 'C$' ).
tff(func_def_58,type,
'ccspan$a': 'B_d_prod_ell2_set$' > 'B_d_prod_ell2_ccsubspace$' ).
tff(func_def_59,type,
'tensor_ell2$b': ( 'A_ell2$' * 'C_ell2$' ) > 'A_c_prod_ell2$' ).
tff(func_def_60,type,
'unitary$': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun$' ).
tff(func_def_61,type,
'fun_app$ak': ( 'A_a_fun$' * 'A$' ) > 'A$' ).
tff(func_def_62,type,
'cblinfun_apply$g': ( 'A_a_prod_ell2_a_c_prod_ell2_cblinfun$' * 'A_a_prod_ell2$' ) > 'A_c_prod_ell2$' ).
tff(func_def_63,type,
'id$': 'A_c_prod_a_c_prod_fun$' ).
tff(func_def_64,type,
'cblinfun_extension$a': ( 'A_c_prod_a_c_prod_prod_ell2_set$' * 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_fun$' ) > 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$' ).
tff(func_def_65,type,
'b1$': 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_66,type,
'uu$': 'C_a_prod_set$' > 'C_a_prod_bool_fun$' ).
tff(func_def_67,type,
'case_prod$': 'A_c_a_c_prod_fun_fun$' > 'A_c_prod_a_c_prod_fun$' ).
tff(func_def_68,type,
'tensor_ell2$i': ( 'A_c_prod_ell2$' * 'A_ell2$' ) > 'A_c_prod_a_prod_ell2$' ).
tff(func_def_69,type,
'cblinfun_apply$s': 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' > 'B_d_prod_ell2_a_c_prod_ell2_fun$' ).
tff(func_def_70,type,
'cblinfun_apply$j': ( 'C_c_prod_ell2_a_c_prod_ell2_cblinfun$' * 'C_c_prod_ell2$' ) > 'A_c_prod_ell2$' ).
tff(func_def_71,type,
'plus$u': ( 'B_d_prod_ell2$' * 'B_d_prod_ell2$' ) > 'B_d_prod_ell2$' ).
tff(func_def_72,type,
'i$': 'A$' ).
tff(func_def_73,type,
'swap$e': 'C_a_prod_a_c_prod_fun$' ).
tff(func_def_74,type,
'fun_app$ad': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'C_ell2_d_ell2_cblinfun_bool_fun$' ).
tff(func_def_75,type,
'plus$l': ( 'A_c_prod_ell2_complex_prod$' * 'A_c_prod_ell2_complex_prod$' ) > 'A_c_prod_ell2_complex_prod$' ).
tff(func_def_76,type,
'swap$b': 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ).
tff(func_def_77,type,
'snd$e': 'A_c_prod$' > 'C$' ).
tff(func_def_78,type,
'plus$p': ( 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$' * 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$' ) > 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$' ).
tff(func_def_79,type,
'ket$': 'A_c_prod_a_c_prod_ell2_fun$' ).
tff(func_def_80,type,
'image$e': ( 'A_c_prod_ell2_b_d_prod_ell2_fun$' * 'A_c_prod_ell2_set$' ) > 'B_d_prod_ell2_set$' ).
tff(func_def_81,type,
'image$f': ( 'A_c_prod_a_c_prod_ell2_fun$' * 'A_c_prod_set$' ) > 'A_c_prod_ell2_set$' ).
tff(func_def_82,type,
'cblinfun_apply$w': ( 'A_a_prod_ell2_b_b_prod_ell2_cblinfun$' * 'A_a_prod_ell2$' ) > 'B_b_prod_ell2$' ).
tff(func_def_83,type,
'ket$g': 'B_d_prod$' > 'B_d_prod_ell2$' ).
tff(func_def_84,type,
'heterogenous_cblinfun_id$a': 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' ).
tff(func_def_85,type,
'minus$e': ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_set$' ) > 'C_ell2_d_ell2_cblinfun_set$' ).
tff(func_def_86,type,
'pair$h': ( 'D_ell2$' * 'D_ell2$' ) > 'D_ell2_d_ell2_prod$' ).
tff(func_def_87,type,
'top$e': 'A_c_prod_ell2_ccsubspace$' ).
tff(func_def_88,type,
'cblinfun_apply$a': 'A_ell2_b_ell2_cblinfun$' > 'A_ell2_b_ell2_fun$' ).
tff(func_def_89,type,
'plus$ac': ( 'C_ell2_d_ell2_cblinfun_set_set$' * 'C_ell2_d_ell2_cblinfun_set_set$' ) > 'C_ell2_d_ell2_cblinfun_set_set$' ).
tff(func_def_90,type,
'ket$h': 'B$' > 'B_ell2$' ).
tff(func_def_91,type,
'uua$': 'A_c_prod_set$' > 'A_c_prod_bool_fun$' ).
tff(func_def_92,type,
'tensor_ell2$h': ( 'C_ell2$' * 'A_ell2$' ) > 'C_a_prod_ell2$' ).
tff(func_def_93,type,
'uug$': ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun$' ) > 'C_ell2_d_ell2_cblinfun_complex_fun$' ).
tff(func_def_94,type,
'a$': 'A_ell2_b_ell2_cblinfun$' ).
tff(func_def_95,type,
'plus$af': ( 'C_ell2$' * 'C_ell2$' ) > 'C_ell2$' ).
tff(func_def_96,type,
'fun_app$ai': ( 'C_a_prod_a_c_prod_fun$' * 'C_a_prod$' ) > 'A_c_prod$' ).
tff(func_def_97,type,
'tensor_ell2$e': ( 'A_c_prod_ell2$' * 'A_c_prod_ell2$' ) > 'A_c_prod_a_c_prod_prod_ell2$' ).
tff(func_def_98,type,
'type$': 'B_d_prod_ell2_itself$' ).
tff(func_def_99,type,
'pair$r': ( 'A$' * 'A_c_prod$' ) > 'A_a_c_prod_prod$' ).
tff(func_def_100,type,
'fun_app$s': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun_fun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun$' ).
tff(func_def_101,type,
'cblinfun_apply$m': ( 'A_c_prod_ell2_a_c_prod_ell2_cblinfun$' * 'A_c_prod_ell2$' ) > 'A_c_prod_ell2$' ).
tff(func_def_102,type,
'plus$h': ( 'D_ell2_complex_prod$' * 'D_ell2_complex_prod$' ) > 'D_ell2_complex_prod$' ).
tff(func_def_103,type,
'fst$k': 'A_c_prod_ell2_complex_prod$' > 'A_c_prod_ell2$' ).
tff(func_def_104,type,
'tensor_ell2$f': ( 'A_ell2$' * 'A_ell2$' ) > 'A_a_prod_ell2$' ).
tff(func_def_105,type,
'fst$i': 'Complex_d_ell2_prod$' > 'Complex$' ).
tff(func_def_106,type,
'elt_set_plus$a': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ).
tff(func_def_107,type,
'snd$g': 'Complex_complex_prod$' > 'Complex$' ).
tff(func_def_108,type,
'tensor_op$h': ( 'C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun$' ) > 'C_c_prod_ell2_d_d_prod_ell2_cblinfun$' ).
tff(func_def_109,type,
'cblinfun_apply$v': ( 'D_ell2_d_ell2_cblinfun$' * 'D_ell2$' ) > 'D_ell2$' ).
tff(func_def_110,type,
'swap$c': 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ).
tff(func_def_111,type,
'elt_set_plus$': ( 'C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun_set$' ) > 'C_ell2_d_ell2_cblinfun_set$' ).
tff(func_def_112,type,
'plus$ab': ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_set$' ) > 'C_ell2_d_ell2_cblinfun_set$' ).
tff(func_def_113,type,
'image$': ( 'A_c_prod_c_a_prod_fun$' * 'A_c_prod_set$' ) > 'C_a_prod_set$' ).
tff(func_def_114,type,
'closure$b': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ).
tff(func_def_115,type,
'cspan$a': 'C_ell2_d_ell2_cblinfun_set$' > 'C_ell2_d_ell2_cblinfun_set$' ).
tff(func_def_116,type,
'collect$a': 'A_c_prod_bool_fun$' > 'A_c_prod_set$' ).
tff(func_def_117,type,
'snd$b': 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_118,type,
'isometry$': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun$' ).
tff(func_def_119,type,
'fun_app$m': ( 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$' * 'C_ell2_d_ell2_cblinfun$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_120,type,
'fst$a': 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_121,type,
'uuc$': 'A_c_prod_ell2_set$' > 'A_c_prod_ell2_bool_fun$' ).
tff(func_def_122,type,
'pair$i': ( 'A_c_prod_ell2$' * 'Complex$' ) > 'A_c_prod_ell2_complex_prod$' ).
tff(func_def_123,type,
'ccspan$': 'A_c_prod_ell2_set$' > 'A_c_prod_ell2_ccsubspace$' ).
tff(func_def_124,type,
'pair$g': ( 'Complex$' * 'D_ell2$' ) > 'Complex_d_ell2_prod$' ).
tff(func_def_125,type,
'image$a': ( 'C_a_prod_a_c_prod_fun$' * 'C_a_prod_set$' ) > 'A_c_prod_set$' ).
tff(func_def_126,type,
'uub$': 'B_d_prod_ell2_set$' > 'B_d_prod_ell2_bool_fun$' ).
tff(func_def_127,type,
'plus$': ( 'Complex$' * 'Complex$' ) > 'Complex$' ).
tff(func_def_128,type,
'snd$a': 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_129,type,
'minus$f': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ).
tff(func_def_130,type,
'tensor_op$f': ( 'C_ell2_a_ell2_cblinfun$' * 'A_ell2_c_ell2_cblinfun$' ) > 'C_a_prod_ell2_a_c_prod_ell2_cblinfun$' ).
tff(func_def_131,type,
'zero$b': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_132,type,
'swap$': 'A_c_prod_a_c_prod_prod$' > 'A_c_prod_a_c_prod_prod$' ).
tff(func_def_133,type,
'fst$g': 'Complex_complex_prod$' > 'Complex$' ).
tff(func_def_134,type,
'snd$h': 'D_ell2_complex_prod$' > 'Complex$' ).
tff(func_def_135,type,
'plus$o': ( 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_cblinfun$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_cblinfun$' ) > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_cblinfun$' ).
tff(func_def_136,type,
'collect$b': 'B_d_prod_ell2_bool_fun$' > 'B_d_prod_ell2_set$' ).
tff(func_def_137,type,
'cblinfun_apply$e': ( 'C_ell2_b_ell2_cblinfun$' * 'C_ell2$' ) > 'B_ell2$' ).
tff(func_def_138,type,
'plus$a': 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun_fun$' ).
tff(func_def_139,type,
'divide$': 'C_ell2_d_ell2_cblinfun$' > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$' ).
tff(func_def_140,type,
'uud$': 'A_set$' > 'A_bool_fun$' ).
tff(func_def_141,type,
'fun_app$w': ( 'B_d_prod_ell2_a_c_prod_ell2_fun$' * 'B_d_prod_ell2$' ) > 'A_c_prod_ell2$' ).
tff(func_def_142,type,
'plus$x': ( 'D_ell2_set$' * 'D_ell2_set$' ) > 'D_ell2_set$' ).
tff(func_def_143,type,
'cinner$': ( 'A_c_prod_ell2$' * 'A_c_prod_ell2$' ) > 'Complex$' ).
tff(func_def_144,type,
'fun_app$ac': ( 'A_c_bool_fun_fun$' * 'A$' ) > 'C_bool_fun$' ).
tff(func_def_145,type,
'collect$d': 'A_bool_fun$' > 'A_set$' ).
tff(func_def_146,type,
'fun_app$am': ( 'A_c_fun$' * 'A$' ) > 'C$' ).
tff(func_def_147,type,
'closure$': 'A_c_prod_ell2_set$' > 'A_c_prod_ell2_set$' ).
tff(func_def_148,type,
'cblinfun_apply$q': ( 'C_a_prod_ell2_d_b_prod_ell2_cblinfun$' * 'C_a_prod_ell2$' ) > 'D_b_prod_ell2$' ).
tff(func_def_149,type,
'uuf$': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun_fun$' ).
tff(func_def_150,type,
'minus$g': ( 'Complex$' * 'Complex$' ) > 'Complex$' ).
tff(func_def_151,type,
'fst$j': 'D_ell2_d_ell2_prod$' > 'D_ell2$' ).
tff(func_def_152,type,
'closure$a': 'C_ell2_d_ell2_cblinfun_set$' > 'C_ell2_d_ell2_cblinfun_set$' ).
tff(func_def_153,type,
'pair$a': ( 'C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun$' ) > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ).
tff(func_def_154,type,
'snd$j': 'D_ell2_d_ell2_prod$' > 'D_ell2$' ).
tff(func_def_155,type,
'plus$b': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun_fun$' ).
tff(func_def_156,type,
'fun_app$p': ( 'C_a_c_prod_fun$' * 'C$' ) > 'A_c_prod$' ).
tff(func_def_157,type,
'minus$c': ( 'B_d_prod_ell2$' * 'B_d_prod_ell2$' ) > 'B_d_prod_ell2$' ).
tff(func_def_158,type,
'tensor_op$c': ( 'A_ell2_a_ell2_cblinfun$' * 'A_ell2_c_ell2_cblinfun$' ) > 'A_a_prod_ell2_a_c_prod_ell2_cblinfun$' ).
tff(func_def_159,type,
'zero$d': 'Complex$' ).
tff(func_def_160,type,
'cblinfun_apply$aa': ( 'B_ell2_b_d_prod_ell2_cblinfun$' * 'B_ell2$' ) > 'B_d_prod_ell2$' ).
tff(func_def_161,type,
'minus$d': ( 'A_c_prod_ell2$' * 'A_c_prod_ell2$' ) > 'A_c_prod_ell2$' ).
tff(func_def_162,type,
'cblinfun_apply$ad': ( 'B_ell2_a_c_prod_ell2_cblinfun$' * 'B_ell2$' ) > 'A_c_prod_ell2$' ).
tff(func_def_163,type,
'plus$m': ( 'A_c_prod_ell2$' * 'A_c_prod_ell2$' ) > 'A_c_prod_ell2$' ).
tff(func_def_164,type,
'plus$z': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ).
tff(func_def_165,type,
'plus$k': ( 'D_ell2_d_ell2_prod$' * 'D_ell2_d_ell2_prod$' ) > 'D_ell2_d_ell2_prod$' ).
tff(func_def_166,type,
'cblinfun_apply$ae': ( 'D_ell2_a_c_prod_ell2_cblinfun$' * 'D_ell2$' ) > 'A_c_prod_ell2$' ).
tff(func_def_167,type,
'pair$': 'A_c_a_c_prod_fun_fun$' ).
tff(func_def_168,type,
'fun_app$n': ( 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun_fun$' * 'C_ell2_d_ell2_cblinfun$' ) > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$' ).
tff(func_def_169,type,
'scaleC$a': ( 'Complex$' * 'B_d_prod_ell2$' ) > 'B_d_prod_ell2$' ).
tff(func_def_170,type,
'heterogenous_cblinfun_id$': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_171,type,
'top$b': 'A_c_prod_ell2_set$' ).
tff(func_def_172,type,
'tensor_ell2$g': ( 'C_ell2$' * 'C_ell2$' ) > 'C_c_prod_ell2$' ).
tff(func_def_173,type,
'cblinfun_apply$b': 'C_ell2_d_ell2_cblinfun$' > 'C_ell2_d_ell2_fun$' ).
tff(func_def_174,type,
'cblinfun_apply$t': ( 'B_d_prod_ell2_b_d_prod_ell2_cblinfun$' * 'B_d_prod_ell2$' ) > 'B_d_prod_ell2$' ).
tff(func_def_175,type,
'top$a': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ).
tff(func_def_176,type,
'fst$l': 'Complex_a_c_prod_ell2_prod$' > 'Complex$' ).
tff(func_def_177,type,
'fun_app$af': ( 'A_c_prod_a_c_prod_bool_fun_fun$' * 'A_c_prod$' ) > 'A_c_prod_bool_fun$' ).
tff(func_def_178,type,
'tensor_op$a': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$' ).
tff(func_def_179,type,
'zero$': 'B_d_prod_ell2$' ).
tff(func_def_180,type,
'tensor_op$': ( 'A_ell2_b_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_181,type,
'fun_app$v': ( 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_fun$' * 'A_c_prod_a_c_prod_prod_ell2$' ) > 'B_d_prod_b_d_prod_prod_ell2$' ).
tff(func_def_182,type,
'swap$d': 'A_c_prod_c_a_prod_fun$' ).
tff(func_def_183,type,
'less_eq$': 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$' ).
tff(func_def_184,type,
'curry$c': 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod_bool_fun$' > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$' ).
tff(func_def_185,type,
'tensor_op$e': ( 'A_ell2_a_ell2_cblinfun$' * 'C_ell2_c_ell2_cblinfun$' ) > 'A_c_prod_ell2_a_c_prod_ell2_cblinfun$' ).
tff(func_def_186,type,
'map_prod$': ( 'A_a_fun$' * 'C_c_fun$' ) > 'A_c_prod_a_c_prod_fun$' ).
tff(func_def_187,type,
'tensor_op$m': ( 'B_ell2_b_d_prod_ell2_cblinfun$' * 'D_ell2_b_d_prod_ell2_cblinfun$' ) > 'B_d_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$' ).
tff(func_def_188,type,
'fst$c': 'A_c_prod_a_c_prod_prod$' > 'A_c_prod$' ).
tff(func_def_189,type,
'fun_app$j': ( 'C_ell2_d_ell2_cblinfun_complex_fun$' * 'C_ell2_d_ell2_cblinfun$' ) > 'Complex$' ).
tff(func_def_190,type,
'cblinfun_extension$': ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$' ) > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_cblinfun$' ).
tff(func_def_191,type,
'tensor_ell2$k': ( 'A_ell2$' * 'A_c_prod_ell2$' ) > 'A_a_c_prod_prod_ell2$' ).
tff(func_def_192,type,
'pair$o': ( 'B$' * 'D$' ) > 'B_d_prod$' ).
tff(func_def_193,type,
'cblinfun_apply$z': ( 'B_d_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$' * 'B_d_prod_ell2$' ) > 'B_d_prod_b_d_prod_prod_ell2$' ).
tff(func_def_194,type,
'prod_right$': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_fun_fun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_195,type,
'pair$n': ( 'C$' * 'C$' ) > 'C_c_prod$' ).
tff(func_def_196,type,
'pair$l': ( 'C$' * 'A$' ) > 'C_a_prod$' ).
tff(func_def_197,type,
'prod_left$': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_fun_fun$' * 'A_c_prod_ell2$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_b_d_prod_ell2_cblinfun$' ).
tff(func_def_198,type,
'ket$i': 'D$' > 'D_ell2$' ).
tff(func_def_199,type,
'cblinfun_extension$d': ( 'A_ell2_set$' * 'A_ell2_b_ell2_fun$' ) > 'A_ell2_b_ell2_cblinfun$' ).
tff(func_def_200,type,
'cblinfun_apply$ak': ( 'Complex_d_ell2_cblinfun$' * 'Complex$' ) > 'D_ell2$' ).
tff(func_def_201,type,
'cblinfun_apply$aj': ( 'D_ell2_complex_cblinfun$' * 'D_ell2$' ) > 'Complex$' ).
tff(func_def_202,type,
'top$d': 'A_c_prod_set$' ).
tff(func_def_203,type,
'fst$b': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_204,type,
'snd$': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_205,type,
'curry$': 'A_c_prod_bool_fun$' > 'A_c_bool_fun_fun$' ).
tff(func_def_206,type,
'ket$c': 'A_c_prod_a_c_prod_prod$' > 'A_c_prod_a_c_prod_prod_ell2$' ).
tff(func_def_207,type,
'cblinfun_image$': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_ccsubspace$' ) > 'B_d_prod_ell2_ccsubspace$' ).
tff(func_def_208,type,
'curry$a': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod_bool_fun$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$' ).
tff(func_def_209,type,
'pair$b': ( 'C_ell2_d_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' ).
tff(func_def_210,type,
'top$': 'C_ell2_d_ell2_cblinfun_set$' ).
tff(func_def_211,type,
'plus$n': ( 'Complex_a_c_prod_ell2_prod$' * 'Complex_a_c_prod_ell2_prod$' ) > 'Complex_a_c_prod_ell2_prod$' ).
tff(func_def_212,type,
'plus$ae': ( 'A_c_prod_a_c_prod_prod_ell2$' * 'A_c_prod_a_c_prod_prod_ell2$' ) > 'A_c_prod_a_c_prod_prod_ell2$' ).
tff(func_def_213,type,
'fun_app$ah': ( 'A_c_prod_c_a_prod_fun$' * 'A_c_prod$' ) > 'C_a_prod$' ).
tff(func_def_214,type,
'fun_app$o': ( 'A_c_prod_a_c_prod_ell2_fun$' * 'A_c_prod$' ) > 'A_c_prod_ell2$' ).
tff(func_def_215,type,
'ket$a': 'A$' > 'A_ell2$' ).
tff(func_def_216,type,
'cblinfun_apply$o': ( 'C_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'C_c_prod_ell2$' ) > 'B_d_prod_ell2$' ).
tff(func_def_217,type,
'pair$f': ( 'D_ell2$' * 'Complex$' ) > 'D_ell2_complex_prod$' ).
tff(func_def_218,type,
'cblinfun_apply$c': 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$' > 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_fun$' ).
tff(func_def_219,type,
'cblinfun_apply$r': 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_cblinfun$' > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$' ).
tff(func_def_220,type,
'plus$g': ( 'Complex_complex_prod$' * 'Complex_complex_prod$' ) > 'Complex_complex_prod$' ).
tff(func_def_221,type,
'cblinfun_apply$p': ( 'C_c_prod_ell2_d_d_prod_ell2_cblinfun$' * 'C_c_prod_ell2$' ) > 'D_d_prod_ell2$' ).
tff(func_def_222,type,
'cblinfun_apply$ac': ( 'B_d_prod_ell2_a_c_prod_a_c_prod_prod_ell2_cblinfun$' * 'B_d_prod_ell2$' ) > 'A_c_prod_a_c_prod_prod_ell2$' ).
tff(func_def_223,type,
'tensor_op$i': ( 'C_ell2_d_ell2_cblinfun$' * 'A_ell2_b_ell2_cblinfun$' ) > 'C_a_prod_ell2_d_b_prod_ell2_cblinfun$' ).
tff(func_def_224,type,
'plus$i': ( 'D_ell2$' * 'D_ell2$' ) > 'D_ell2$' ).
tff(func_def_225,type,
'cblinfun_apply$h': ( 'A_ell2_a_ell2_cblinfun$' * 'A_ell2$' ) > 'A_ell2$' ).
tff(func_def_226,type,
'ket$d': 'C_a_prod$' > 'C_a_prod_ell2$' ).
tff(func_def_227,type,
'top$c': 'B_d_prod_ell2_set$' ).
tff(func_def_228,type,
'snd$i': 'Complex_d_ell2_prod$' > 'D_ell2$' ).
tff(func_def_229,type,
'cspan$c': 'B_d_prod_ell2_set$' > 'B_d_prod_ell2_set$' ).
tff(func_def_230,type,
'pair$q': ( 'A_c_prod$' * 'C$' ) > 'A_c_prod_c_prod$' ).
tff(func_def_231,type,
'minus$': ( 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' * 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' ) > 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' ).
tff(func_def_232,type,
'uuh$': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_complex_fun$' ).
tff(func_def_233,type,
'plus$ad': ( 'A_ell2$' * 'A_ell2$' ) > 'A_ell2$' ).
tff(func_def_234,type,
'tensor_ell2$a': ( 'B_d_prod_ell2$' * 'B_d_prod_ell2$' ) > 'B_d_prod_b_d_prod_prod_ell2$' ).
tff(func_def_235,type,
'fun_app$ae': ( 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun_fun$' * 'C_ell2_d_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun$' ).
tff(func_def_236,type,
'ket$e': 'A_a_prod$' > 'A_a_prod_ell2$' ).
tff(func_def_237,type,
'tensor_ell2$m': ( 'B_ell2$' * 'B_ell2$' ) > 'B_b_prod_ell2$' ).
tff(func_def_238,type,
'apsnd$': ( 'C_c_fun$' * 'A_c_prod$' ) > 'A_c_prod$' ).
tff(func_def_239,type,
'snd$c': 'A_c_prod_a_c_prod_prod$' > 'A_c_prod$' ).
tff(func_def_240,type,
'fun_app$f': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun_fun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun$' ).
tff(func_def_241,type,
'uue$': 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$' ).
tff(func_def_242,type,
'pair$d': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' ).
tff(func_def_243,type,
'plus$w': ( 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_set$' ) > 'A_c_prod_ell2_set$' ).
tff(func_def_244,type,
'fun_app$k': ( 'A_c_prod_ell2_b_d_prod_ell2_fun$' * 'A_c_prod_ell2$' ) > 'B_d_prod_ell2$' ).
tff(func_def_245,type,
'divide$a': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_246,type,
'curry$d': 'A_c_prod_a_c_prod_prod_bool_fun$' > 'A_c_prod_a_c_prod_bool_fun_fun$' ).
tff(func_def_247,type,
'plus$e': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ).
tff(func_def_248,type,
'type$a': 'A_c_prod_ell2_itself$' ).
tff(func_def_249,type,
'in_rel$': 'A_c_prod_set$' > 'A_c_bool_fun_fun$' ).
tff(func_def_250,type,
'ket$b': 'C$' > 'C_ell2$' ).
tff(func_def_251,type,
'pair$p': ( 'A_c_prod$' * 'A$' ) > 'A_c_prod_a_prod$' ).
tff(func_def_252,type,
'tensor_op$j': ( 'B_ell2_b_ell2_cblinfun$' * 'D_ell2_d_ell2_cblinfun$' ) > 'B_d_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_253,type,
'minus$b': 'C_ell2_d_ell2_cblinfun$' > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$' ).
tff(func_def_254,type,
'plus$c': ( 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ) > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ).
tff(func_def_255,type,
'cblinfun_apply$k': ( 'C_ell2_a_ell2_cblinfun$' * 'C_ell2$' ) > 'A_ell2$' ).
tff(func_def_256,type,
'tensor_ell2$c': ( 'D_ell2$' * 'D_ell2$' ) > 'D_d_prod_ell2$' ).
tff(func_def_257,type,
'zero$c': 'A_c_prod_ell2$' ).
tff(func_def_258,type,
'scaleC$b': ( 'Complex$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_259,type,
'ket$k': 'A_c_prod_c_prod$' > 'A_c_prod_c_prod_ell2$' ).
tff(func_def_260,type,
'cblinfun_apply$u': ( 'B_ell2_b_ell2_cblinfun$' * 'B_ell2$' ) > 'B_ell2$' ).
tff(func_def_261,type,
'swap$a': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' ).
tff(func_def_262,type,
'crepresentation$a': ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun$' ) > 'C_ell2_d_ell2_cblinfun_complex_fun$' ).
tff(func_def_263,type,
'cspan$': 'A_c_prod_ell2_set$' > 'A_c_prod_ell2_set$' ).
tff(func_def_264,type,
'ket$l': 'A_a_c_prod_prod$' > 'A_a_c_prod_prod_ell2$' ).
tff(func_def_265,type,
'curry$e': 'C_a_prod_bool_fun$' > 'C_a_bool_fun_fun$' ).
tff(func_def_266,type,
'pair$j': ( 'Complex$' * 'A_c_prod_ell2$' ) > 'Complex_a_c_prod_ell2_prod$' ).
tff(func_def_267,type,
'plus$y': ( 'Complex_set$' * 'Complex_set$' ) > 'Complex_set$' ).
tff(func_def_268,type,
'snd$d': 'C_a_prod$' > 'A$' ).
tff(func_def_269,type,
'cinner$a': ( 'B_d_prod_ell2$' * 'B_d_prod_ell2$' ) > 'Complex$' ).
tff(func_def_270,type,
'fun_app$i': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_complex_fun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'Complex$' ).
tff(func_def_271,type,
'plus$q': ( 'B_d_prod_b_d_prod_prod_ell2$' * 'B_d_prod_b_d_prod_prod_ell2$' ) > 'B_d_prod_b_d_prod_prod_ell2$' ).
tff(func_def_272,type,
'gr$': ( 'A_set$' * 'A_c_fun$' ) > 'A_c_prod_set$' ).
tff(func_def_273,type,
'fun_app$r': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_274,type,
'scaleC$c': 'Complex$' > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$' ).
tff(func_def_275,type,
'pair$e': ( 'Complex$' * 'Complex$' ) > 'Complex_complex_prod$' ).
tff(func_def_276,type,
'curry$b': 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod_bool_fun$' > 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun_fun$' ).
tff(func_def_277,type,
'cblinfun_extension$c': ( 'C_ell2_set$' * 'C_ell2_d_ell2_fun$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_278,type,
'cblinfun_apply$x': ( 'B_ell2_a_ell2_cblinfun$' * 'B_ell2$' ) > 'A_ell2$' ).
tff(func_def_279,type,
'fun_app$h': ( 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$' * 'C_ell2_d_ell2_cblinfun$' ) > 'C_ell2_d_ell2_cblinfun_bool_fun$' ).
tff(func_def_280,type,
'fun_app$ag': ( 'C_a_bool_fun_fun$' * 'C$' ) > 'A_bool_fun$' ).
tff(func_def_281,type,
'rel_fun$c': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun_fun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun_fun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun_bool_fun_fun$' ).
tff(func_def_282,type,
'scaleC$': ( 'Complex$' * 'A_c_prod_ell2$' ) > 'A_c_prod_ell2$' ).
tff(func_def_283,type,
'plus$t': ( 'B_ell2$' * 'B_ell2$' ) > 'B_ell2$' ).
tff(func_def_284,type,
'rel_fun$a': ( 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$' ) > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun_c_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun_bool_fun_fun$' ).
tff(func_def_285,type,
'j$': 'C$' ).
tff(func_def_286,type,
'fst$d': 'C_a_prod$' > 'C$' ).
tff(func_def_287,type,
'cblinfun_apply$al': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'B_d_prod_ell2$' ).
tff(func_def_288,type,
'snd$k': 'A_c_prod_ell2_complex_prod$' > 'Complex$' ).
tff(func_def_289,type,
'zero$a': 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_290,type,
'cblinfun_apply$n': ( 'C_a_prod_ell2_a_c_prod_ell2_cblinfun$' * 'C_a_prod_ell2$' ) > 'A_c_prod_ell2$' ).
tff(func_def_291,type,
'ket$j': 'A_c_prod_a_prod$' > 'A_c_prod_a_prod_ell2$' ).
tff(func_def_292,type,
'crepresentation$': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_complex_fun$' ).
tff(func_def_293,type,
sK0: ( 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$' * 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$' ) > 'A_c_prod_a_c_prod_prod$' ).
tff(func_def_294,type,
sK1: ( 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' * 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' ) > 'B_d_prod$' ).
tff(func_def_295,type,
sK2: ( 'C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun$' ) > 'C$' ).
tff(func_def_296,type,
sK3: ( 'A_ell2_b_ell2_cblinfun$' * 'A_ell2_b_ell2_cblinfun$' ) > 'A$' ).
tff(func_def_297,type,
sK4: ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod$' ).
tff(func_def_298,type,
sK5: 'A_c_prod_a_c_prod_prod_bool_fun$' > 'A_c_prod$' ).
tff(func_def_299,type,
sK6: 'A_c_prod_a_c_prod_prod_bool_fun$' > 'A$' ).
tff(func_def_300,type,
sK7: 'A_c_prod_a_c_prod_prod_bool_fun$' > 'C$' ).
tff(func_def_301,type,
sK8: 'A_c_prod_a_c_prod_prod$' > 'A_c_prod$' ).
tff(func_def_302,type,
sK9: 'A_c_prod_a_c_prod_prod$' > 'A$' ).
tff(func_def_303,type,
sK10: 'A_c_prod_a_c_prod_prod$' > 'C$' ).
tff(func_def_304,type,
sK11: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod_bool_fun$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_305,type,
sK12: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod_bool_fun$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_306,type,
sK13: 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod_bool_fun$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_307,type,
sK14: 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod_bool_fun$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_308,type,
sK15: 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod_bool_fun$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_309,type,
sK16: 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod_bool_fun$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_310,type,
sK17: 'A_c_prod_a_c_prod_prod_bool_fun$' > 'A_c_prod$' ).
tff(func_def_311,type,
sK18: 'A_c_prod_a_c_prod_prod_bool_fun$' > 'A_c_prod$' ).
tff(func_def_312,type,
sK19: 'C_a_prod_bool_fun$' > 'C$' ).
tff(func_def_313,type,
sK20: 'C_a_prod_bool_fun$' > 'A$' ).
tff(func_def_314,type,
sK21: 'A_c_prod_bool_fun$' > 'A$' ).
tff(func_def_315,type,
sK22: 'A_c_prod_bool_fun$' > 'C$' ).
tff(func_def_316,type,
sK23: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_317,type,
sK24: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_318,type,
sK25: 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_319,type,
sK26: 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_320,type,
sK27: 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_321,type,
sK28: 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_322,type,
sK29: 'A_c_prod_a_c_prod_prod$' > 'A_c_prod$' ).
tff(func_def_323,type,
sK30: 'A_c_prod_a_c_prod_prod$' > 'A_c_prod$' ).
tff(func_def_324,type,
sK31: 'C_a_prod$' > 'C$' ).
tff(func_def_325,type,
sK32: 'C_a_prod$' > 'A$' ).
tff(func_def_326,type,
sK33: 'A_c_prod$' > 'A$' ).
tff(func_def_327,type,
sK34: 'A_c_prod$' > 'C$' ).
tff(func_def_328,type,
sK35: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_329,type,
sK36: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_330,type,
sK37: 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_331,type,
sK38: 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_332,type,
sK39: 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_333,type,
sK40: 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_334,type,
sK41: 'A_c_prod_a_c_prod_prod$' > 'A_c_prod$' ).
tff(func_def_335,type,
sK42: 'A_c_prod_a_c_prod_prod$' > 'A_c_prod$' ).
tff(func_def_336,type,
sK43: 'C_a_prod$' > 'C$' ).
tff(func_def_337,type,
sK44: 'C_a_prod$' > 'A$' ).
tff(func_def_338,type,
sK45: 'A_c_prod$' > 'A$' ).
tff(func_def_339,type,
sK46: 'A_c_prod$' > 'C$' ).
tff(func_def_340,type,
sK47: ( 'B_d_prod_ell2$' * 'B_d_prod_ell2_set$' * 'B_d_prod_ell2_set$' ) > 'B_d_prod_ell2$' ).
tff(func_def_341,type,
sK48: ( 'B_d_prod_ell2$' * 'B_d_prod_ell2_set$' * 'B_d_prod_ell2_set$' ) > 'B_d_prod_ell2$' ).
tff(func_def_342,type,
sK49: ( 'A_c_prod_ell2$' * 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_set$' ) > 'A_c_prod_ell2$' ).
tff(func_def_343,type,
sK50: ( 'A_c_prod_ell2$' * 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_set$' ) > 'A_c_prod_ell2$' ).
tff(func_def_344,type,
sK51: ( 'D_ell2$' * 'D_ell2_set$' * 'D_ell2_set$' ) > 'D_ell2$' ).
tff(func_def_345,type,
sK52: ( 'D_ell2$' * 'D_ell2_set$' * 'D_ell2_set$' ) > 'D_ell2$' ).
tff(func_def_346,type,
sK53: ( 'Complex$' * 'Complex_set$' * 'Complex_set$' ) > 'Complex$' ).
tff(func_def_347,type,
sK54: ( 'Complex$' * 'Complex_set$' * 'Complex_set$' ) > 'Complex$' ).
tff(func_def_348,type,
sK55: ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set_set$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ).
tff(func_def_349,type,
sK56: ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set_set$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ).
tff(func_def_350,type,
sK57: ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_set_set$' * 'C_ell2_d_ell2_cblinfun_set_set$' ) > 'C_ell2_d_ell2_cblinfun_set$' ).
tff(func_def_351,type,
sK58: ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_set_set$' * 'C_ell2_d_ell2_cblinfun_set_set$' ) > 'C_ell2_d_ell2_cblinfun_set$' ).
tff(func_def_352,type,
sK59: ( 'C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_set$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_353,type,
sK60: ( 'C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_set$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_354,type,
sK61: ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_355,type,
sK62: ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_356,type,
sK63: ( 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_cblinfun$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_cblinfun$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_357,type,
sK64: ( 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$' * 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$' ) > 'A_c_prod_a_c_prod_prod_ell2$' ).
tff(func_def_358,type,
sK65: ( 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' * 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' ) > 'B_d_prod_ell2$' ).
tff(func_def_359,type,
sK66: ( 'C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun$' ) > 'C_ell2$' ).
tff(func_def_360,type,
sK67: ( 'A_ell2_b_ell2_cblinfun$' * 'A_ell2_b_ell2_cblinfun$' ) > 'A_ell2$' ).
tff(func_def_361,type,
sK68: ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2$' ).
tff(func_def_362,type,
sK69: 'A_c_prod_a_c_prod_prod$' > 'A$' ).
tff(func_def_363,type,
sK70: 'A_c_prod_a_c_prod_prod$' > 'C$' ).
tff(func_def_364,type,
sK71: 'A_c_prod_a_c_prod_prod$' > 'A_c_prod$' ).
tff(func_def_365,type,
sK72: ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_cblinfun$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_366,type,
sK73: ( 'A_c_prod_a_c_prod_prod_ell2_set$' * 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$' * 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_fun$' ) > 'A_c_prod_a_c_prod_prod_ell2$' ).
tff(func_def_367,type,
sK74: ( 'B_d_prod_ell2_set$' * 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' * 'B_d_prod_ell2_a_c_prod_ell2_fun$' ) > 'B_d_prod_ell2$' ).
tff(func_def_368,type,
sK75: ( 'C_ell2_set$' * 'C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_fun$' ) > 'C_ell2$' ).
tff(func_def_369,type,
sK76: ( 'A_ell2_set$' * 'A_ell2_b_ell2_cblinfun$' * 'A_ell2_b_ell2_fun$' ) > 'A_ell2$' ).
tff(func_def_370,type,
sK77: ( 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_fun$' ) > 'A_c_prod_ell2$' ).
tff(func_def_371,type,
sK78: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_372,type,
sK79: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_373,type,
sK80: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ).
tff(func_def_374,type,
sK81: 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun_fun$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_375,type,
sK82: 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun_fun$' > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_376,type,
sK83: 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun_fun$' > 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' ).
tff(func_def_377,type,
sK84: 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_378,type,
sK85: 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$' > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_379,type,
sK86: 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$' > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ).
tff(func_def_380,type,
sK87: 'C_a_bool_fun_fun$' > 'C$' ).
tff(func_def_381,type,
sK88: 'C_a_bool_fun_fun$' > 'A$' ).
tff(func_def_382,type,
sK89: 'C_a_bool_fun_fun$' > 'C_a_prod$' ).
tff(func_def_383,type,
sK90: 'A_c_bool_fun_fun$' > 'A$' ).
tff(func_def_384,type,
sK91: 'A_c_bool_fun_fun$' > 'C$' ).
tff(func_def_385,type,
sK92: 'A_c_bool_fun_fun$' > 'A_c_prod$' ).
tff(func_def_386,type,
sK93: ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_cblinfun$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_387,type,
sK94: ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$' ) > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_cblinfun$' ).
tff(func_def_388,type,
sK95: ( 'A_c_prod_a_c_prod_prod_ell2_set$' * 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_fun$' * 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$' ) > 'A_c_prod_a_c_prod_prod_ell2$' ).
tff(func_def_389,type,
sK96: ( 'A_c_prod_a_c_prod_prod_ell2_set$' * 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_fun$' ) > 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_cblinfun$' ).
tff(func_def_390,type,
sK97: ( 'B_d_prod_ell2_set$' * 'B_d_prod_ell2_a_c_prod_ell2_fun$' * 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' ) > 'B_d_prod_ell2$' ).
tff(func_def_391,type,
sK98: ( 'B_d_prod_ell2_set$' * 'B_d_prod_ell2_a_c_prod_ell2_fun$' ) > 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' ).
tff(func_def_392,type,
sK99: ( 'C_ell2_set$' * 'C_ell2_d_ell2_fun$' * 'C_ell2_d_ell2_cblinfun$' ) > 'C_ell2$' ).
tff(func_def_393,type,
sK100: ( 'C_ell2_set$' * 'C_ell2_d_ell2_fun$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_394,type,
sK101: ( 'A_ell2_set$' * 'A_ell2_b_ell2_fun$' * 'A_ell2_b_ell2_cblinfun$' ) > 'A_ell2$' ).
tff(func_def_395,type,
sK102: ( 'A_ell2_set$' * 'A_ell2_b_ell2_fun$' ) > 'A_ell2_b_ell2_cblinfun$' ).
tff(func_def_396,type,
sK103: ( 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_fun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2$' ).
tff(func_def_397,type,
sK104: ( 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_fun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_398,type,
sK105: ( 'A_c_prod$' * 'A_c_prod_a_c_prod_prod$' ) > 'A_c_prod$' ).
tff(func_def_399,type,
sK106: ( 'C_ell2_d_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_400,type,
sK107: ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_401,type,
sK108: ( 'C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_402,type,
sK109: ( 'A$' * 'C_a_prod$' ) > 'C$' ).
tff(func_def_403,type,
sK110: ( 'C$' * 'A_c_prod$' ) > 'A$' ).
tff(func_def_404,type,
sK111: ( 'A_c_prod$' * 'A_c_prod_a_c_prod_prod$' ) > 'A_c_prod$' ).
tff(func_def_405,type,
sK112: ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_406,type,
sK113: ( 'C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_407,type,
sK114: ( 'C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_408,type,
sK115: ( 'C$' * 'C_a_prod$' ) > 'A$' ).
tff(func_def_409,type,
sK116: ( 'A$' * 'A_c_prod$' ) > 'C$' ).
tff(func_def_410,type,
sK117: ( 'A_c_prod$' * 'A_a_fun$' * 'C_c_fun$' * 'A_c_prod_set$' ) > 'A$' ).
tff(func_def_411,type,
sK118: ( 'A_c_prod$' * 'A_a_fun$' * 'C_c_fun$' * 'A_c_prod_set$' ) > 'C$' ).
tff(func_def_412,type,
sK119: ( 'A_c_prod$' * 'A_a_fun$' * 'A_c_prod$' ) > 'A$' ).
tff(func_def_413,type,
sK120: ( 'A_c_prod$' * 'A_a_fun$' * 'A_c_prod$' ) > 'C$' ).
tff(func_def_414,type,
sK121: ( 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2$' ).
tff(func_def_415,type,
sK122: ( 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2$' ).
tff(func_def_416,type,
sK123: ( 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2$' ).
tff(func_def_417,type,
sK124: ( 'A_c_prod_ell2_set$' * 'B_d_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ) > 'A_c_prod_ell2$' ).
tff(func_def_418,type,
sK125: ( 'A_c_prod_ell2_set$' * 'B_d_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ) > 'B_d_prod_ell2$' ).
tff(func_def_419,type,
sK126: ( 'A_c_prod_ell2_set$' * 'B_d_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2$' ).
tff(func_def_420,type,
sK127: ( 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2$' ).
tff(func_def_421,type,
sK128: ( 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2$' ).
tff(func_def_422,type,
sK129: ( 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2$' ).
tff(func_def_423,type,
sK130: ( 'A_c_prod_ell2$' * 'A_c_prod_ell2$' ) > 'A_c_prod$' ).
tff(func_def_424,type,
sK131: ( 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2$' ).
tff(func_def_425,type,
sK132: ( 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'A_c_prod_ell2$' ).
tff(func_def_426,type,
sK133: ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > 'B_d_prod_ell2$' ).
tff(func_def_427,type,
sK134: ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_bool_fun$' ) > 'Complex$' ).
tff(func_def_428,type,
sK135: ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_bool_fun$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_429,type,
sK136: ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_bool_fun$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_430,type,
sK137: ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun$' ) > 'Complex$' ).
tff(func_def_431,type,
sK138: ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_432,type,
sK139: ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_433,type,
sF140: 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$' ).
tff(func_def_434,type,
sF141: 'C_ell2_d_ell2_cblinfun$' ).
tff(func_def_435,type,
sF142: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_436,type,
sF143: 'A_c_prod_ell2_b_d_prod_ell2_fun$' ).
tff(func_def_437,type,
sF144: 'C_a_c_prod_fun$' ).
tff(func_def_438,type,
sF145: 'A_c_prod$' ).
tff(func_def_439,type,
sF146: 'A_c_prod_ell2$' ).
tff(func_def_440,type,
sF147: 'B_d_prod_ell2$' ).
tff(func_def_441,type,
sF148: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_442,type,
sF149: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun$' ).
tff(func_def_443,type,
sF150: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_444,type,
sF151: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(func_def_445,type,
sF152: 'A_c_prod_ell2_b_d_prod_ell2_fun$' ).
tff(func_def_446,type,
sF153: 'B_d_prod_ell2$' ).
tff(pred_def_1,type,
'fun_app$z': ( 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod_bool_fun$' * 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' ) > $o ).
tff(pred_def_2,type,
'fun_app$g': ( 'C_ell2_d_ell2_cblinfun_bool_fun$' * 'C_ell2_d_ell2_cblinfun$' ) > $o ).
tff(pred_def_3,type,
'member$h': ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_set_set$' ) > $o ).
tff(pred_def_4,type,
'fun_app$a': ( 'A_c_prod_bool_fun$' * 'A_c_prod$' ) > $o ).
tff(pred_def_5,type,
'member$d': ( 'A$' * 'A_set$' ) > $o ).
tff(pred_def_6,type,
'less_eq$g': ( 'A_c_prod_ell2_ccsubspace$' * 'A_c_prod_ell2_ccsubspace$' ) > $o ).
tff(pred_def_7,type,
'rel_fun$b': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun_fun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun_bool_fun_fun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun_fun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun_fun$' ) > $o ).
tff(pred_def_8,type,
'cdependent$': 'A_c_prod_ell2_set$' > $o ).
tff(pred_def_9,type,
'nO_MATCH$a': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'Complex$' ) > $o ).
tff(pred_def_10,type,
'member$a': ( 'A_c_prod$' * 'A_c_prod_set$' ) > $o ).
tff(pred_def_11,type,
'fun_app$y': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod_bool_fun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ) > $o ).
tff(pred_def_12,type,
'less_eq$b': ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_13,type,
'cdependent$b': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' > $o ).
tff(pred_def_14,type,
'cblinfun_extension_exists$b': ( 'B_d_prod_ell2_set$' * 'B_d_prod_ell2_a_c_prod_ell2_fun$' ) > $o ).
tff(pred_def_15,type,
'member$': ( 'C_a_prod$' * 'C_a_prod_set$' ) > $o ).
tff(pred_def_16,type,
'member$o': ( 'A_c_prod_a_c_prod_prod_ell2$' * 'A_c_prod_a_c_prod_prod_ell2_set$' ) > $o ).
tff(pred_def_17,type,
'cblinfun_extension_exists$c': ( 'C_ell2_set$' * 'C_ell2_d_ell2_fun$' ) > $o ).
tff(pred_def_18,type,
'member$j': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_19,type,
'member$f': ( 'Complex$' * 'Complex_set$' ) > $o ).
tff(pred_def_20,type,
'member$l': ( 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod$' * 'C_ell2_d_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_prod_set$' ) > $o ).
tff(pred_def_21,type,
'member$q': ( 'A_ell2$' * 'A_ell2_set$' ) > $o ).
tff(pred_def_22,type,
'less_eq$c': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_23,type,
'cblinfun_extension_exists$d': ( 'A_ell2_set$' * 'A_ell2_b_ell2_fun$' ) > $o ).
tff(pred_def_24,type,
'member$e': ( 'D_ell2$' * 'D_ell2_set$' ) > $o ).
tff(pred_def_25,type,
'heterogenous_same_type_cblinfun$a': ( 'A_c_prod_ell2_itself$' * 'B_d_prod_ell2_itself$' ) > $o ).
tff(pred_def_26,type,
'cblinfun_extension_exists$': ( 'C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$' ) > $o ).
tff(pred_def_27,type,
'fun_app$x': ( 'A_c_prod_a_c_prod_prod_bool_fun$' * 'A_c_prod_a_c_prod_prod$' ) > $o ).
tff(pred_def_28,type,
'member$n': ( 'A_c_prod_a_c_prod_prod$' * 'A_c_prod_a_c_prod_prod_set$' ) > $o ).
tff(pred_def_29,type,
'member$b': ( 'B_d_prod_ell2$' * 'B_d_prod_ell2_set$' ) > $o ).
tff(pred_def_30,type,
'fun_app$e': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ) > $o ).
tff(pred_def_31,type,
'member$p': ( 'C_ell2$' * 'C_ell2_set$' ) > $o ).
tff(pred_def_32,type,
'less_eq$d': ( 'A_c_prod_set$' * 'A_c_prod_set$' ) > $o ).
tff(pred_def_33,type,
'member$g': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set_set$' ) > $o ).
tff(pred_def_34,type,
'fun_app$b': ( 'B_d_prod_ell2_bool_fun$' * 'B_d_prod_ell2$' ) > $o ).
tff(pred_def_35,type,
'fun_app$aa': ( 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod_bool_fun$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' ) > $o ).
tff(pred_def_36,type,
'heterogenous_same_type_cblinfun$': ( 'B_d_prod_ell2_itself$' * 'A_c_prod_ell2_itself$' ) > $o ).
tff(pred_def_37,type,
'less_eq$f': ( 'Complex$' * 'Complex$' ) > $o ).
tff(pred_def_38,type,
'cblinfun_extension_exists$a': ( 'A_c_prod_a_c_prod_prod_ell2_set$' * 'A_c_prod_a_c_prod_prod_ell2_b_d_prod_b_d_prod_prod_ell2_fun$' ) > $o ).
tff(pred_def_39,type,
'is_ortho_set$': 'A_c_prod_ell2_set$' > $o ).
tff(pred_def_40,type,
'fun_app$c': ( 'A_c_prod_ell2_bool_fun$' * 'A_c_prod_ell2$' ) > $o ).
tff(pred_def_41,type,
'rel_fun$': ( 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun_c_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun_bool_fun_fun$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun_fun$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun_fun$' ) > $o ).
tff(pred_def_42,type,
'member$k': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod_set$' ) > $o ).
tff(pred_def_43,type,
'nO_MATCH$': ( 'C_ell2_d_ell2_cblinfun$' * 'Complex$' ) > $o ).
tff(pred_def_44,type,
'fun_app$ab': ( 'C_bool_fun$' * 'C$' ) > $o ).
tff(pred_def_45,type,
'member$m': ( 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod_set$' ) > $o ).
tff(pred_def_46,type,
'cdependent$a': 'C_ell2_d_ell2_cblinfun_set$' > $o ).
tff(pred_def_47,type,
'fun_app$': ( 'C_a_prod_bool_fun$' * 'C_a_prod$' ) > $o ).
tff(pred_def_48,type,
'cblinfun_extension_exists$e': ( 'A_c_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_fun$' ) > $o ).
tff(pred_def_49,type,
'fun_app$d': ( 'A_bool_fun$' * 'A$' ) > $o ).
tff(pred_def_50,type,
'member$i': ( 'C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun_set$' ) > $o ).
tff(pred_def_51,type,
'less_eq$e': ( 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' * 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$' ) > $o ).
tff(pred_def_52,type,
'member$c': ( 'A_c_prod_ell2$' * 'A_c_prod_ell2_set$' ) > $o ).
tff(f10,conjecture,
'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'('a$','fun_app$m'('fun_app$n'('plus$a','b1$'),'b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))) = 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b','tensor_op$'('a$','b1$')),'tensor_op$'('a$','b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture9) ).
tff(f11,negated_conjecture,
( ( ~ 'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'('a$','fun_app$m'('fun_app$n'('plus$a','b1$'),'b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))) ) = 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b','tensor_op$'('a$','b1$')),'tensor_op$'('a$','b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))) ),
inference(negated_conjecture,[status(cth)],[f10]) ).
tff(f22,axiom,
! [X0: 'A_ell2_b_ell2_cblinfun$',X1: 'C_ell2_d_ell2_cblinfun$',X2: 'A$',X3: 'C$'] : ( 'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'(X0,X1)),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$',X2),X3))) = 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X0),'ket$a'(X2)),'fun_app$u'('cblinfun_apply$b'(X1),'ket$b'(X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom20) ).
tff(f42,axiom,
! [X0: 'C_ell2_d_ell2_cblinfun$',X1: 'C_ell2_d_ell2_cblinfun$',X2: 'C_ell2$'] : ( 'fun_app$u'('cblinfun_apply$b'('fun_app$m'('fun_app$n'('plus$a',X0),X1)),X2) = 'plus$i'('fun_app$u'('cblinfun_apply$b'(X0),X2),'fun_app$u'('cblinfun_apply$b'(X1),X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom40) ).
tff(f43,axiom,
! [X0: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$',X1: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$',X2: 'A_c_prod_ell2$'] : ( 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b',X0),X1)),X2) = 'plus$u'('fun_app$k'('fun_app$l'('cblinfun_apply$',X0),X2),'fun_app$k'('fun_app$l'('cblinfun_apply$',X1),X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom41) ).
tff(f97,axiom,
! [X0: 'B_ell2$',X1: 'D_ell2$',X2: 'D_ell2$'] : ( 'tensor_ell2$'(X0,'plus$i'(X1,X2)) = 'plus$u'('tensor_ell2$'(X0,X1),'tensor_ell2$'(X0,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom95) ).
tff(f257,axiom,
! [X0: 'C_ell2_d_ell2_cblinfun$',X1: 'C_ell2_d_ell2_cblinfun$'] : ( 'fun_app$m'('fun_app$n'('plus$a',X0),X1) = 'fun_app$m'('fun_app$n'('plus$a',X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom255) ).
tff(f258,axiom,
! [X0: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$',X1: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$'] : ( 'fun_app$r'('fun_app$s'('plus$b',X0),X1) = 'fun_app$r'('fun_app$s'('plus$b',X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom256) ).
tff(f645,plain,
'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'('a$','fun_app$m'('fun_app$n'('plus$a','b1$'),'b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))) != 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b','tensor_op$'('a$','b1$')),'tensor_op$'('a$','b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))),
inference(flattening,[],[f11]) ).
tff(f1298,plain,
'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'('a$','fun_app$m'('fun_app$n'('plus$a','b1$'),'b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))) != 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b','tensor_op$'('a$','b1$')),'tensor_op$'('a$','b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))),
inference(cnf_transformation,[],[f645]) ).
tff(f1309,plain,
! [X2: 'A$',X3: 'C$',X0: 'A_ell2_b_ell2_cblinfun$',X1: 'C_ell2_d_ell2_cblinfun$'] : ( 'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'(X0,X1)),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$',X2),X3))) = 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X0),'ket$a'(X2)),'fun_app$u'('cblinfun_apply$b'(X1),'ket$b'(X3))) ),
inference(cnf_transformation,[],[f22]) ).
tff(f1329,plain,
! [X2: 'C_ell2$',X0: 'C_ell2_d_ell2_cblinfun$',X1: 'C_ell2_d_ell2_cblinfun$'] : ( 'fun_app$u'('cblinfun_apply$b'('fun_app$m'('fun_app$n'('plus$a',X0),X1)),X2) = 'plus$i'('fun_app$u'('cblinfun_apply$b'(X0),X2),'fun_app$u'('cblinfun_apply$b'(X1),X2)) ),
inference(cnf_transformation,[],[f42]) ).
tff(f1330,plain,
! [X2: 'A_c_prod_ell2$',X0: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$',X1: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$'] : ( 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b',X0),X1)),X2) = 'plus$u'('fun_app$k'('fun_app$l'('cblinfun_apply$',X0),X2),'fun_app$k'('fun_app$l'('cblinfun_apply$',X1),X2)) ),
inference(cnf_transformation,[],[f43]) ).
tff(f1422,plain,
! [X2: 'D_ell2$',X0: 'B_ell2$',X1: 'D_ell2$'] : ( 'tensor_ell2$'(X0,'plus$i'(X1,X2)) = 'plus$u'('tensor_ell2$'(X0,X1),'tensor_ell2$'(X0,X2)) ),
inference(cnf_transformation,[],[f97]) ).
tff(f1625,plain,
! [X0: 'C_ell2_d_ell2_cblinfun$',X1: 'C_ell2_d_ell2_cblinfun$'] : ( 'fun_app$m'('fun_app$n'('plus$a',X0),X1) = 'fun_app$m'('fun_app$n'('plus$a',X1),X0) ),
inference(cnf_transformation,[],[f257]) ).
tff(f1626,plain,
! [X0: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$',X1: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$'] : ( 'fun_app$r'('fun_app$s'('plus$b',X0),X1) = 'fun_app$r'('fun_app$s'('plus$b',X1),X0) ),
inference(cnf_transformation,[],[f258]) ).
tff(f2328,definition,
sF140 = 'fun_app$n'('plus$a','b1$'),
introduced(definition,[new_symbols(definition,[sF140])],[function_definition]) ).
tff(f2329,plain,
'fun_app$n'('plus$a','b1$') = sF140,
inference(reorient_equations,[],[f2328]) ).
tff(f2330,definition,
sF141 = 'fun_app$m'(sF140,'b2$'),
introduced(definition,[new_symbols(definition,[sF141])],[function_definition]) ).
tff(f2331,plain,
'fun_app$m'(sF140,'b2$') = sF141,
inference(reorient_equations,[],[f2330]) ).
tff(f2332,definition,
sF142 = 'tensor_op$'('a$',sF141),
introduced(definition,[new_symbols(definition,[sF142])],[function_definition]) ).
tff(f2333,plain,
'tensor_op$'('a$',sF141) = sF142,
inference(reorient_equations,[],[f2332]) ).
tff(f2334,definition,
sF143 = 'fun_app$l'('cblinfun_apply$',sF142),
introduced(definition,[new_symbols(definition,[sF143])],[function_definition]) ).
tff(f2335,plain,
'fun_app$l'('cblinfun_apply$',sF142) = sF143,
inference(reorient_equations,[],[f2334]) ).
tff(f2336,definition,
sF144 = 'fun_app$q'('pair$','i$'),
introduced(definition,[new_symbols(definition,[sF144])],[function_definition]) ).
tff(f2337,plain,
'fun_app$q'('pair$','i$') = sF144,
inference(reorient_equations,[],[f2336]) ).
tff(f2338,definition,
sF145 = 'fun_app$p'(sF144,'j$'),
introduced(definition,[new_symbols(definition,[sF145])],[function_definition]) ).
tff(f2339,plain,
'fun_app$p'(sF144,'j$') = sF145,
inference(reorient_equations,[],[f2338]) ).
tff(f2340,definition,
sF146 = 'fun_app$o'('ket$',sF145),
introduced(definition,[new_symbols(definition,[sF146])],[function_definition]) ).
tff(f2341,plain,
'fun_app$o'('ket$',sF145) = sF146,
inference(reorient_equations,[],[f2340]) ).
tff(f2342,definition,
sF147 = 'fun_app$k'(sF143,sF146),
introduced(definition,[new_symbols(definition,[sF147])],[function_definition]) ).
tff(f2343,plain,
'fun_app$k'(sF143,sF146) = sF147,
inference(reorient_equations,[],[f2342]) ).
tff(f2344,definition,
sF148 = 'tensor_op$'('a$','b1$'),
introduced(definition,[new_symbols(definition,[sF148])],[function_definition]) ).
tff(f2345,plain,
'tensor_op$'('a$','b1$') = sF148,
inference(reorient_equations,[],[f2344]) ).
tff(f2346,definition,
sF149 = 'fun_app$s'('plus$b',sF148),
introduced(definition,[new_symbols(definition,[sF149])],[function_definition]) ).
tff(f2347,plain,
'fun_app$s'('plus$b',sF148) = sF149,
inference(reorient_equations,[],[f2346]) ).
tff(f2348,definition,
sF150 = 'tensor_op$'('a$','b2$'),
introduced(definition,[new_symbols(definition,[sF150])],[function_definition]) ).
tff(f2349,plain,
'tensor_op$'('a$','b2$') = sF150,
inference(reorient_equations,[],[f2348]) ).
tff(f2350,definition,
sF151 = 'fun_app$r'(sF149,sF150),
introduced(definition,[new_symbols(definition,[sF151])],[function_definition]) ).
tff(f2351,plain,
'fun_app$r'(sF149,sF150) = sF151,
inference(reorient_equations,[],[f2350]) ).
tff(f2352,definition,
sF152 = 'fun_app$l'('cblinfun_apply$',sF151),
introduced(definition,[new_symbols(definition,[sF152])],[function_definition]) ).
tff(f2353,plain,
'fun_app$l'('cblinfun_apply$',sF151) = sF152,
inference(reorient_equations,[],[f2352]) ).
tff(f2354,definition,
sF153 = 'fun_app$k'(sF152,sF146),
introduced(definition,[new_symbols(definition,[sF153])],[function_definition]) ).
tff(f2355,plain,
'fun_app$k'(sF152,sF146) = sF153,
inference(reorient_equations,[],[f2354]) ).
tff(f2356,plain,
sF147 != sF153,
inference(definition_folding,[],[f1298,f2355,f2341,f2339,f2337,f2353,f2351,f2349,f2347,f2345,f2343,f2341,f2339,f2337,f2335,f2333,f2331,f2329]) ).
tff(f2438,plain,
'fun_app$m'('fun_app$n'('plus$a','b1$'),'b2$') = sF141,
inference(forward_demodulation,[],[f2331,f2329]) ).
tff(f2439,plain,
sF143 = 'fun_app$l'('cblinfun_apply$','tensor_op$'('a$',sF141)),
inference(forward_demodulation,[],[f2335,f2333]) ).
tff(f2440,plain,
'fun_app$p'('fun_app$q'('pair$','i$'),'j$') = sF145,
inference(forward_demodulation,[],[f2339,f2337]) ).
tff(f2441,plain,
'fun_app$k'(sF143,sF146) != sF153,
inference(backward_demodulation,[],[f2356,f2343]) ).
tff(f2442,plain,
'fun_app$s'('plus$b','tensor_op$'('a$','b1$')) = sF149,
inference(forward_demodulation,[],[f2347,f2345]) ).
tff(f2443,plain,
sF151 = 'fun_app$r'(sF149,'tensor_op$'('a$','b2$')),
inference(forward_demodulation,[],[f2351,f2349]) ).
tff(f2444,plain,
sF153 = 'fun_app$k'('fun_app$l'('cblinfun_apply$',sF151),sF146),
inference(forward_demodulation,[],[f2355,f2353]) ).
tff(f2458,plain,
sF141 = 'fun_app$m'('fun_app$n'('plus$a','b2$'),'b1$'),
inference(forward_demodulation,[],[f2438,f1625]) ).
tff(f2460,plain,
'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$')) = sF146,
inference(backward_demodulation,[],[f2341,f2440]) ).
tff(f2461,plain,
sF153 != 'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'('a$',sF141)),sF146),
inference(forward_demodulation,[],[f2441,f2439]) ).
tff(f2462,plain,
'fun_app$r'('fun_app$s'('plus$b','tensor_op$'('a$','b1$')),'tensor_op$'('a$','b2$')) = sF151,
inference(forward_demodulation,[],[f2443,f2442]) ).
tff(f2469,plain,
sF153 = 'fun_app$k'('fun_app$l'('cblinfun_apply$',sF151),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))),
inference(backward_demodulation,[],[f2444,f2460]) ).
tff(f2470,plain,
sF153 != 'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'('a$',sF141)),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))),
inference(forward_demodulation,[],[f2461,f2460]) ).
tff(f2471,plain,
sF151 = 'fun_app$r'('fun_app$s'('plus$b','tensor_op$'('a$','b2$')),'tensor_op$'('a$','b1$')),
inference(forward_demodulation,[],[f2462,f1626]) ).
tff(f2476,plain,
sF153 != 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'('a$'),'ket$a'('i$')),'fun_app$u'('cblinfun_apply$b'(sF141),'ket$b'('j$'))),
inference(forward_demodulation,[],[f2470,f1309]) ).
tff(f2477,plain,
sF153 = 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b','tensor_op$'('a$','b2$')),'tensor_op$'('a$','b1$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))),
inference(backward_demodulation,[],[f2469,f2471]) ).
tff(f2480,plain,
sF153 != 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'('a$'),'ket$a'('i$')),'fun_app$u'('cblinfun_apply$b'('fun_app$m'('fun_app$n'('plus$a','b2$'),'b1$')),'ket$b'('j$'))),
inference(forward_demodulation,[],[f2476,f2458]) ).
tff(f2482,plain,
sF153 != 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'('a$'),'ket$a'('i$')),'plus$i'('fun_app$u'('cblinfun_apply$b'('b2$'),'ket$b'('j$')),'fun_app$u'('cblinfun_apply$b'('b1$'),'ket$b'('j$')))),
inference(forward_demodulation,[],[f2480,f1329]) ).
tff(f2483,plain,
'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b','tensor_op$'('a$','b2$')),'tensor_op$'('a$','b1$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))) != 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'('a$'),'ket$a'('i$')),'plus$i'('fun_app$u'('cblinfun_apply$b'('b2$'),'ket$b'('j$')),'fun_app$u'('cblinfun_apply$b'('b1$'),'ket$b'('j$')))),
inference(forward_demodulation,[],[f2482,f2477]) ).
tff(f2494,plain,
! [X2: 'C_ell2_d_ell2_cblinfun$',X3: 'C$',X0: 'A_ell2_b_ell2_cblinfun$',X1: 'A$',X4: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$'] : ( 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b',X4),'tensor_op$'(X0,X2))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$',X1),X3))) = 'plus$u'('fun_app$k'('fun_app$l'('cblinfun_apply$',X4),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$',X1),X3))),'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X0),'ket$a'(X1)),'fun_app$u'('cblinfun_apply$b'(X2),'ket$b'(X3)))) ),
inference(superposition,[],[f1330,f1309]) ).
tff(f2989,plain,
'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'('a$'),'ket$a'('i$')),'plus$i'('fun_app$u'('cblinfun_apply$b'('b2$'),'ket$b'('j$')),'fun_app$u'('cblinfun_apply$b'('b1$'),'ket$b'('j$')))) != 'plus$u'('fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'('a$','b2$')),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))),'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'('a$'),'ket$a'('i$')),'fun_app$u'('cblinfun_apply$b'('b1$'),'ket$b'('j$')))),
inference(superposition,[],[f2483,f2494]) ).
tff(f2998,plain,
'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'('a$'),'ket$a'('i$')),'plus$i'('fun_app$u'('cblinfun_apply$b'('b2$'),'ket$b'('j$')),'fun_app$u'('cblinfun_apply$b'('b1$'),'ket$b'('j$')))) != 'plus$u'('tensor_ell2$'('fun_app$t'('cblinfun_apply$a'('a$'),'ket$a'('i$')),'fun_app$u'('cblinfun_apply$b'('b2$'),'ket$b'('j$'))),'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'('a$'),'ket$a'('i$')),'fun_app$u'('cblinfun_apply$b'('b1$'),'ket$b'('j$')))),
inference(forward_demodulation,[],[f2989,f1309]) ).
tff(f3001,plain,
$false,
inference(forward_subsumption_resolution,[],[f2998,f1422]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP387_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.10/0.38 % Computer : n008.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 12:57:54 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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
% 11.72/2.35 % (1200830)Detected formulas, will run a generic FOF schedule.
% 11.72/2.35 % (1200840)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2003612034:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.72/2.35 % (1200835)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=2028254011:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.72/2.35 % (1200839)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1286031465:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.72/2.35 % (1200841)dis-21_1_sil=8000:lcm=predicate:random_seed=3951973326: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)
% 11.72/2.35 % (1200838)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2590902275:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.72/2.35 % (1200836)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=3127762340:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.72/2.35 % (1200837)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=3216552528:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.72/2.35 % (1200838)Refutation not found, incomplete strategy
% 11.72/2.35 % (1200838)------------------------------
% 11.72/2.35 % (1200838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.35 % (1200838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.35 % (1200838)CaDiCaL version: 2.1.3
% 11.72/2.35 % (1200838)Termination reason: Refutation not found, incomplete strategy
% 11.72/2.35 % (1200838)Time elapsed: 0.005 s
% 11.72/2.35 % (1200838)Peak memory usage: 89 MB
% 11.72/2.35 % (1200838)Instructions burned: 8 (million)
% 11.72/2.35 % (1200840)Instruction limit reached!
% 11.72/2.35 % (1200840)------------------------------
% 11.72/2.35 % (1200840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.35 % (1200840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.35 % (1200840)CaDiCaL version: 2.1.3
% 11.72/2.35 % (1200840)Termination reason: Instruction limit
% 11.72/2.35 % (1200840)Termination phase: Saturation
% 11.72/2.35 % (1200840)Time elapsed: 0.045 s
% 11.72/2.35 % (1200840)Peak memory usage: 91 MB
% 11.72/2.35 % (1200840)Instructions burned: 140 (million)
% 11.72/2.35 % (1200839)Instruction limit reached!
% 11.72/2.35 % (1200839)------------------------------
% 11.72/2.35 % (1200839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.35 % (1200839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.35 % (1200839)CaDiCaL version: 2.1.3
% 11.72/2.35 % (1200839)Termination reason: Instruction limit
% 11.72/2.35 % (1200839)Termination phase: Saturation
% 11.72/2.35 % (1200839)Time elapsed: 0.059 s
% 11.72/2.35 % (1200839)Peak memory usage: 89 MB
% 11.72/2.35 % (1200839)Instructions burned: 121 (million)
% 11.72/2.35 % (1200841)Instruction limit reached!
% 11.72/2.35 % (1200841)------------------------------
% 11.72/2.35 % (1200841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.35 % (1200841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.35 % (1200841)CaDiCaL version: 2.1.3
% 11.72/2.35 % (1200841)Termination reason: Instruction limit
% 11.72/2.35 % (1200841)Termination phase: Saturation
% 11.72/2.35 % (1200841)Time elapsed: 0.065 s
% 11.72/2.35 % (1200841)Peak memory usage: 90 MB
% 11.72/2.35 % (1200841)Instructions burned: 131 (million)
% 11.72/2.35 % (1200849)lrs+10_1_sil=8000:sp=occurrence:random_seed=502218054:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.72/2.35 % (1200850)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3171556038:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 11.72/2.35 % (1200851)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2382662081:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 11.72/2.35 % (1200838)------------------------------
% 11.72/2.35 % (1200838)------------------------------
% 11.72/2.35 % (1200849)Instruction limit reached!
% 11.72/2.35 % (1200849)------------------------------
% 11.72/2.35 % (1200849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.51/3.42 % (1200849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.51/3.42 % (1200849)CaDiCaL version: 2.1.3
% 19.51/3.42 % (1200849)Termination reason: Instruction limit
% 19.51/3.42 % (1200849)Termination phase: Saturation
% 19.51/3.42 % (1200849)Time elapsed: 0.079 s
% 19.51/3.42 % (1200849)Peak memory usage: 90 MB
% 19.51/3.42 % (1200849)Instructions burned: 287 (million)
% 19.51/3.42 % (1200850)Instruction limit reached!
% 19.51/3.42 % (1200850)------------------------------
% 19.51/3.42 % (1200850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.51/3.42 % (1200850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.51/3.42 % (1200850)CaDiCaL version: 2.1.3
% 19.51/3.42 % (1200850)Termination reason: Instruction limit
% 19.51/3.42 % (1200850)Termination phase: Saturation
% 19.51/3.42 % (1200850)Time elapsed: 0.079 s
% 19.51/3.42 % (1200850)Peak memory usage: 89 MB
% 19.51/3.42 % (1200850)Instructions burned: 157 (million)
% 19.51/3.42 % (1200855)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=2327358779:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 19.51/3.42 % (1200851)Instruction limit reached!
% 19.51/3.42 % (1200851)------------------------------
% 19.51/3.42 % (1200851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.51/3.42 % (1200851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.51/3.42 % (1200851)CaDiCaL version: 2.1.3
% 19.51/3.42 % (1200851)Termination reason: Instruction limit
% 19.51/3.42 % (1200851)Termination phase: Saturation
% 19.51/3.42 % (1200851)Time elapsed: 0.159 s
% 19.51/3.42 % (1200851)Peak memory usage: 90 MB
% 19.51/3.42 % (1200851)Instructions burned: 326 (million)
% 19.51/3.42 % (1200856)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=409037554:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 19.51/3.42 % (1200855)Instruction limit reached!
% 19.51/3.42 % (1200855)------------------------------
% 19.51/3.42 % (1200855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.51/3.42 % (1200855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.51/3.42 % (1200855)CaDiCaL version: 2.1.3
% 19.51/3.42 % (1200855)Termination reason: Instruction limit
% 19.51/3.42 % (1200855)Termination phase: Saturation
% 19.51/3.42 % (1200855)Time elapsed: 0.070 s
% 19.51/3.42 % (1200855)Peak memory usage: 91 MB
% 19.51/3.42 % (1200855)Instructions burned: 251 (million)
% 19.51/3.42 % (1200857)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3330917259:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 19.51/3.42 % (1200859)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1644134531:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 19.51/3.42 % (1200856)Instruction limit reached!
% 19.51/3.42 % (1200856)------------------------------
% 19.51/3.42 % (1200856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.51/3.42 % (1200856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.51/3.42 % (1200856)CaDiCaL version: 2.1.3
% 19.51/3.42 % (1200856)Termination reason: Instruction limit
% 19.51/3.42 % (1200856)Termination phase: Saturation
% 19.51/3.42 % (1200856)Time elapsed: 0.120 s
% 19.51/3.42 % (1200856)Peak memory usage: 89 MB
% 19.51/3.42 % (1200856)Instructions burned: 294 (million)
% 19.51/3.42 % (1200861)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1466703083:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 19.51/3.42 % (1200861)Refutation not found, incomplete strategy
% 19.51/3.42 % (1200861)------------------------------
% 19.51/3.42 % (1200861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.51/3.42 % (1200861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.51/3.42 % (1200861)CaDiCaL version: 2.1.3
% 19.51/3.42 % (1200861)Termination reason: Refutation not found, incomplete strategy
% 19.51/3.42 % (1200861)Time elapsed: 0.014 s
% 19.51/3.42 % (1200861)Peak memory usage: 89 MB
% 19.51/3.42 % (1200861)Instructions burned: 52 (million)
% 19.51/3.42 % (1200859)Instruction limit reached!
% 19.51/3.42 % (1200859)------------------------------
% 19.51/3.42 % (1200859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.51/3.42 % (1200859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.51/3.42 % (1200859)CaDiCaL version: 2.1.3
% 33.54/5.43 % (1200859)Termination reason: Instruction limit
% 33.54/5.43 % (1200859)Termination phase: Saturation
% 33.54/5.43 % (1200859)Time elapsed: 0.063 s
% 33.54/5.43 % (1200859)Peak memory usage: 91 MB
% 33.54/5.43 % (1200859)Instructions burned: 114 (million)
% 33.54/5.43 % (1200864)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2527649247:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 33.54/5.43 % (1200861)------------------------------
% 33.54/5.43 % (1200861)------------------------------
% 33.54/5.43 % (1200866)lrs+10_1_sil=8000:sp=occurrence:random_seed=1206970890:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 33.54/5.43 % (1200864)Instruction limit reached!
% 33.54/5.43 % (1200864)------------------------------
% 33.54/5.43 % (1200864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.43 % (1200864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.43 % (1200864)CaDiCaL version: 2.1.3
% 33.54/5.43 % (1200864)Termination reason: Instruction limit
% 33.54/5.43 % (1200864)Termination phase: Saturation
% 33.54/5.43 % (1200864)Time elapsed: 0.061 s
% 33.54/5.43 % (1200864)Peak memory usage: 90 MB
% 33.54/5.43 % (1200864)Instructions burned: 116 (million)
% 33.54/5.43 % (1200868)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=972253190:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 33.54/5.43 % (1200870)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2555802963:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 33.54/5.43 % (1200868)Instruction limit reached!
% 33.54/5.43 % (1200868)------------------------------
% 33.54/5.43 % (1200868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.43 % (1200868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.43 % (1200868)CaDiCaL version: 2.1.3
% 33.54/5.43 % (1200868)Termination reason: Instruction limit
% 33.54/5.43 % (1200868)Termination phase: Saturation
% 33.54/5.43 % (1200868)Time elapsed: 0.125 s
% 33.54/5.43 % (1200868)Peak memory usage: 92 MB
% 33.54/5.43 % (1200868)Instructions burned: 440 (million)
% 33.54/5.43 % (1200873)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2703390602:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 33.54/5.43 % (1200873)Instruction limit reached!
% 33.54/5.43 % (1200873)------------------------------
% 33.54/5.43 % (1200873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.43 % (1200873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.43 % (1200873)CaDiCaL version: 2.1.3
% 33.54/5.43 % (1200873)Termination reason: Instruction limit
% 33.54/5.43 % (1200873)Termination phase: Saturation
% 33.54/5.43 % (1200873)Time elapsed: 0.041 s
% 33.54/5.43 % (1200873)Peak memory usage: 91 MB
% 33.54/5.43 % (1200873)Instructions burned: 136 (million)
% 33.54/5.43 % (1200875)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2016170722:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 33.54/5.43 % (1200866)Instruction limit reached!
% 33.54/5.43 % (1200866)------------------------------
% 33.54/5.43 % (1200866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.43 % (1200866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.43 % (1200866)CaDiCaL version: 2.1.3
% 33.54/5.43 % (1200866)Termination reason: Instruction limit
% 33.54/5.43 % (1200866)Termination phase: Saturation
% 33.54/5.43 % (1200866)Time elapsed: 0.548 s
% 33.54/5.43 % (1200866)Peak memory usage: 97 MB
% 33.54/5.43 % (1200866)Instructions burned: 908 (million)
% 33.54/5.43 % (1200875)Instruction limit reached!
% 33.54/5.43 % (1200875)------------------------------
% 33.54/5.43 % (1200875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.43 % (1200875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.43 % (1200875)CaDiCaL version: 2.1.3
% 33.54/5.43 % (1200875)Termination reason: Instruction limit
% 33.54/5.43 % (1200875)Termination phase: Saturation
% 33.54/5.43 % (1200875)Time elapsed: 0.162 s
% 33.54/5.43 % (1200875)Peak memory usage: 93 MB
% 33.54/5.43 % (1200875)Instructions burned: 596 (million)
% 33.54/5.43 % (1200877)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4280758492:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 33.54/5.43 % (1200878)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=3812321211:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 55.81/8.52 % (1200878)Instruction limit reached!
% 55.81/8.52 % (1200878)------------------------------
% 55.81/8.52 % (1200878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.81/8.52 % (1200878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.81/8.52 % (1200878)CaDiCaL version: 2.1.3
% 55.81/8.52 % (1200878)Termination reason: Instruction limit
% 55.81/8.52 % (1200878)Termination phase: Saturation
% 55.81/8.52 % (1200878)Time elapsed: 0.038 s
% 55.81/8.52 % (1200878)Peak memory usage: 90 MB
% 55.81/8.52 % (1200878)Instructions burned: 128 (million)
% 55.81/8.52 % (1200881)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3710461113:i=134:gtgl=5:slsql=off:gtg=exists_sym_2982 on theBenchmark for (2982ds/134Mi)
% 55.81/8.52 % (1200881)Instruction limit reached!
% 55.81/8.52 % (1200881)------------------------------
% 55.81/8.52 % (1200881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.81/8.52 % (1200881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.81/8.52 % (1200881)CaDiCaL version: 2.1.3
% 55.81/8.52 % (1200881)Termination reason: Instruction limit
% 55.81/8.52 % (1200881)Termination phase: Saturation
% 55.81/8.52 % (1200881)Time elapsed: 0.038 s
% 55.81/8.52 % (1200881)Peak memory usage: 92 MB
% 55.81/8.52 % (1200881)Instructions burned: 135 (million)
% 55.81/8.52 % (1200883)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2268767147:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi)
% 55.81/8.52 % (1200883)Refutation not found, incomplete strategy
% 55.81/8.52 % (1200883)------------------------------
% 55.81/8.52 % (1200883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.81/8.52 % (1200883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.81/8.52 % (1200883)CaDiCaL version: 2.1.3
% 55.81/8.52 % (1200883)Termination reason: Refutation not found, incomplete strategy
% 55.81/8.52 % (1200883)Time elapsed: 0.002 s
% 55.81/8.52 % (1200883)Peak memory usage: 89 MB
% 55.81/8.52 % (1200883)Instructions burned: 6 (million)
% 55.81/8.52 % (1200857)Instruction limit reached!
% 55.81/8.52 % (1200857)------------------------------
% 55.81/8.52 % (1200857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.81/8.52 % (1200857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.81/8.52 % (1200857)CaDiCaL version: 2.1.3
% 55.81/8.52 % (1200857)Termination reason: Instruction limit
% 55.81/8.52 % (1200857)Termination phase: Saturation
% 55.81/8.52 % (1200857)Time elapsed: 1.477 s
% 55.81/8.52 % (1200857)Peak memory usage: 144 MB
% 55.81/8.52 % (1200857)Instructions burned: 2351 (million)
% 55.81/8.52 % (1200883)------------------------------
% 55.81/8.52 % (1200883)------------------------------
% 55.81/8.52 % (1200885)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1925610419:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi)
% 55.81/8.52 % (1200885)Refutation not found, incomplete strategy
% 55.81/8.52 % (1200885)------------------------------
% 55.81/8.52 % (1200885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.81/8.52 % (1200885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.81/8.52 % (1200885)CaDiCaL version: 2.1.3
% 55.81/8.52 % (1200885)Termination reason: Refutation not found, incomplete strategy
% 55.81/8.52 % (1200885)Time elapsed: 0.010 s
% 55.81/8.52 % (1200885)Peak memory usage: 89 MB
% 55.81/8.52 % (1200885)Instructions burned: 15 (million)
% 55.81/8.52 % (1200886)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=631705420:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi)
% 55.81/8.52 % (1200885)------------------------------
% 55.81/8.52 % (1200885)------------------------------
% 55.81/8.52 % (1200889)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=4045754797:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi)
% 55.81/8.52 % (1200889)Instruction limit reached!
% 55.81/8.52 % (1200889)------------------------------
% 55.81/8.52 % (1200889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.29/13.29 % (1200889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.29/13.29 % (1200889)CaDiCaL version: 2.1.3
% 89.29/13.29 % (1200889)Termination reason: Instruction limit
% 89.29/13.29 % (1200889)Termination phase: Saturation
% 89.29/13.29 % (1200889)Time elapsed: 0.082 s
% 89.29/13.29 % (1200889)Peak memory usage: 91 MB
% 89.29/13.29 % (1200889)Instructions burned: 152 (million)
% 89.29/13.29 % (1200891)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1343331482:i=14155:bd=all_2971 on theBenchmark for (2971ds/14155Mi)
% 89.29/13.29 % (1200870)Instruction limit reached!
% 89.29/13.29 % (1200870)------------------------------
% 89.29/13.29 % (1200870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.29/13.29 % (1200870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.29/13.29 % (1200870)CaDiCaL version: 2.1.3
% 89.29/13.29 % (1200870)Termination reason: Instruction limit
% 89.29/13.29 % (1200870)Termination phase: Saturation
% 89.29/13.29 % (1200870)Time elapsed: 3.014 s
% 89.29/13.29 % (1200870)Peak memory usage: 161 MB
% 89.29/13.29 % (1200870)Instructions burned: 5204 (million)
% 89.29/13.29 % (1200893)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=62253890:i=667:av=off:fsr=off_2958 on theBenchmark for (2958ds/667Mi)
% 89.29/13.29 % (1200893)Refutation not found, incomplete strategy
% 89.29/13.29 % (1200893)------------------------------
% 89.29/13.29 % (1200893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.29/13.29 % (1200893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.29/13.29 % (1200893)CaDiCaL version: 2.1.3
% 89.29/13.29 % (1200893)Termination reason: Refutation not found, incomplete strategy
% 89.29/13.29 % (1200893)Time elapsed: 0.031 s
% 89.29/13.29 % (1200893)Peak memory usage: 90 MB
% 89.29/13.29 % (1200893)Instructions burned: 58 (million)
% 89.29/13.29 % (1200886)Instruction limit reached!
% 89.29/13.29 % (1200886)------------------------------
% 89.29/13.29 % (1200886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.29/13.29 % (1200886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.29/13.29 % (1200886)CaDiCaL version: 2.1.3
% 89.29/13.29 % (1200886)Termination reason: Instruction limit
% 89.29/13.29 % (1200886)Termination phase: Saturation
% 89.29/13.29 % (1200886)Time elapsed: 2.062 s
% 89.29/13.29 % (1200886)Peak memory usage: 181 MB
% 89.29/13.29 % (1200886)Instructions burned: 6063 (million)
% 89.29/13.29 % (1200895)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=4194065204:s2a=on:i=185:s2at=1.8:fdi=4_2955 on theBenchmark for (2955ds/185Mi)
% 89.29/13.29 % (1200893)------------------------------
% 89.29/13.29 % (1200893)------------------------------
% 89.29/13.29 % (1200895)Instruction limit reached!
% 89.29/13.29 % (1200895)------------------------------
% 89.29/13.29 % (1200895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.29/13.29 % (1200895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.29/13.29 % (1200895)CaDiCaL version: 2.1.3
% 89.29/13.29 % (1200895)Termination reason: Instruction limit
% 89.29/13.29 % (1200895)Termination phase: Saturation
% 89.29/13.29 % (1200895)Time elapsed: 0.056 s
% 89.29/13.29 % (1200895)Peak memory usage: 92 MB
% 89.29/13.29 % (1200895)Instructions burned: 186 (million)
% 89.29/13.29 % (1200897)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3158959168:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2954 on theBenchmark for (2954ds/193Mi)
% 89.29/13.29 % (1200898)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1070075712:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2954 on theBenchmark for (2954ds/4850Mi)
% 89.29/13.29 % (1200898)Refutation not found, incomplete strategy
% 89.29/13.29 % (1200898)------------------------------
% 89.29/13.29 % (1200898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.29/13.29 % (1200898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.29/13.29 % (1200898)CaDiCaL version: 2.1.3
% 89.29/13.29 % (1200898)Termination reason: Refutation not found, incomplete strategy
% 89.29/13.29 % (1200898)Time elapsed: 0.012 s
% 89.29/13.29 % (1200898)Peak memory usage: 89 MB
% 89.29/13.29 % (1200898)Instructions burned: 46 (million)
% 89.29/13.29 % (1200897)Instruction limit reached!
% 89.29/13.29 % (1200897)------------------------------
% 89.29/13.29 % (1200897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.87/16.42 % (1200897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.87/16.42 % (1200897)CaDiCaL version: 2.1.3
% 111.87/16.42 % (1200897)Termination reason: Instruction limit
% 111.87/16.42 % (1200897)Termination phase: Saturation
% 111.87/16.42 % (1200897)Time elapsed: 0.100 s
% 111.87/16.42 % (1200897)Peak memory usage: 90 MB
% 111.87/16.42 % (1200897)Instructions burned: 194 (million)
% 111.87/16.42 % (1200898)------------------------------
% 111.87/16.42 % (1200898)------------------------------
% 111.87/16.42 % (1200901)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3986686966:i=12111:sd=1:ss=included_2951 on theBenchmark for (2951ds/12111Mi)
% 111.87/16.42 % (1200902)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1347931140:i=319:kws=precedence:fsr=off_2951 on theBenchmark for (2951ds/319Mi)
% 111.87/16.42 % (1200902)Instruction limit reached!
% 111.87/16.42 % (1200902)------------------------------
% 111.87/16.42 % (1200902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.87/16.42 % (1200902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.87/16.42 % (1200902)CaDiCaL version: 2.1.3
% 111.87/16.42 % (1200902)Termination reason: Instruction limit
% 111.87/16.42 % (1200902)Termination phase: Saturation
% 111.87/16.42 % (1200902)Time elapsed: 0.096 s
% 111.87/16.42 % (1200902)Peak memory usage: 94 MB
% 111.87/16.42 % (1200902)Instructions burned: 320 (million)
% 111.87/16.42 % (1200905)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=667075438:i=2064:ep=RST_2949 on theBenchmark for (2949ds/2064Mi)
% 111.87/16.42 % (1200905)Instruction limit reached!
% 111.87/16.42 % (1200905)------------------------------
% 111.87/16.42 % (1200905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.87/16.42 % (1200905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.87/16.42 % (1200905)CaDiCaL version: 2.1.3
% 111.87/16.42 % (1200905)Termination reason: Instruction limit
% 111.87/16.42 % (1200905)Termination phase: Saturation
% 111.87/16.42 % (1200905)Time elapsed: 0.558 s
% 111.87/16.42 % (1200905)Peak memory usage: 99 MB
% 111.87/16.42 % (1200905)Instructions burned: 2066 (million)
% 111.87/16.42 % (1200907)dis-1011_128_sil=32000:random_seed=999818626:i=3706:ep=RST:av=off_2942 on theBenchmark for (2942ds/3706Mi)
% 111.87/16.42 % (1200907)Instruction limit reached!
% 111.87/16.42 % (1200907)------------------------------
% 111.87/16.42 % (1200907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.87/16.42 % (1200907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.87/16.42 % (1200907)CaDiCaL version: 2.1.3
% 111.87/16.42 % (1200907)Termination reason: Instruction limit
% 111.87/16.42 % (1200907)Termination phase: Saturation
% 111.87/16.42 % (1200907)Time elapsed: 0.718 s
% 111.87/16.42 % (1200907)Peak memory usage: 91 MB
% 111.87/16.42 % (1200907)Instructions burned: 3711 (million)
% 111.87/16.42 % (1200909)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2317100945:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2933 on theBenchmark for (2933ds/757Mi)
% 111.87/16.42 % (1200909)Instruction limit reached!
% 111.87/16.42 % (1200909)------------------------------
% 111.87/16.42 % (1200909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.87/16.42 % (1200909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.87/16.42 % (1200909)CaDiCaL version: 2.1.3
% 111.87/16.42 % (1200909)Termination reason: Instruction limit
% 111.87/16.42 % (1200909)Termination phase: Saturation
% 111.87/16.42 % (1200909)Time elapsed: 0.225 s
% 111.87/16.42 % (1200909)Peak memory usage: 93 MB
% 111.87/16.42 % (1200909)Instructions burned: 758 (million)
% 111.87/16.42 % (1200911)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=604258206:i=13913:ss=axioms:sgt=8_2930 on theBenchmark for (2930ds/13913Mi)
% 111.87/16.42 % (1200877)Instruction limit reached!
% 111.87/16.42 % (1200877)------------------------------
% 111.87/16.42 % (1200877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.87/16.42 % (1200877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.87/16.42 % (1200877)CaDiCaL version: 2.1.3
% 111.87/16.42 % (1200877)Termination reason: Instruction limit
% 111.87/16.42 % (1200877)Termination phase: Saturation
% 111.87/16.42 % (1200877)Time elapsed: 6.087 s
% 111.87/16.42 % (1200877)Peak memory usage: 159 MB
% 111.87/16.42 % (1200877)Instructions burned: 13194 (million)
% 111.87/16.42 % (1200913)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1649552227:i=9925:aac=none_2922 on theBenchmark for (2922ds/9925Mi)
% 141.90/20.67 % (1200911)Instruction limit reached!
% 141.90/20.67 % (1200911)------------------------------
% 141.90/20.67 % (1200911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.90/20.67 % (1200911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.90/20.67 % (1200911)CaDiCaL version: 2.1.3
% 141.90/20.67 % (1200911)Termination reason: Instruction limit
% 141.90/20.67 % (1200911)Termination phase: Saturation
% 141.90/20.67 % (1200911)Time elapsed: 3.443 s
% 141.90/20.67 % (1200911)Peak memory usage: 151 MB
% 141.90/20.67 % (1200911)Instructions burned: 13916 (million)
% 141.90/20.67 % (1200915)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4154725673:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2894 on theBenchmark for (2894ds/2479Mi)
% 141.90/20.67 % (1200915)Refutation not found, incomplete strategy
% 141.90/20.67 % (1200915)------------------------------
% 141.90/20.67 % (1200915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.90/20.67 % (1200915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.90/20.67 % (1200915)CaDiCaL version: 2.1.3
% 141.90/20.67 % (1200915)Termination reason: Refutation not found, incomplete strategy
% 141.90/20.67 % (1200915)Time elapsed: 0.004 s
% 141.90/20.67 % (1200915)Peak memory usage: 89 MB
% 141.90/20.67 % (1200915)Instructions burned: 11 (million)
% 141.90/20.67 % (1200915)------------------------------
% 141.90/20.67 % (1200915)------------------------------
% 141.90/20.67 % (1200917)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=4016409513:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2891 on theBenchmark for (2891ds/440Mi)
% 141.90/20.67 % (1200917)Instruction limit reached!
% 141.90/20.67 % (1200917)------------------------------
% 141.90/20.67 % (1200917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.90/20.67 % (1200917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.90/20.67 % (1200917)CaDiCaL version: 2.1.3
% 141.90/20.67 % (1200917)Termination reason: Instruction limit
% 141.90/20.67 % (1200917)Termination phase: Saturation
% 141.90/20.67 % (1200917)Time elapsed: 0.139 s
% 141.90/20.67 % (1200917)Peak memory usage: 97 MB
% 141.90/20.67 % (1200917)Instructions burned: 442 (million)
% 141.90/20.67 % (1200919)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2158502906:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2888 on theBenchmark for (2888ds/11145Mi)
% 141.90/20.67 % (1200891)Instruction limit reached!
% 141.90/20.67 % (1200891)------------------------------
% 141.90/20.67 % (1200891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.90/20.67 % (1200891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.90/20.67 % (1200891)CaDiCaL version: 2.1.3
% 141.90/20.67 % (1200891)Termination reason: Instruction limit
% 141.90/20.67 % (1200891)Termination phase: Saturation
% 141.90/20.67 % (1200891)Time elapsed: 8.964 s
% 141.90/20.67 % (1200891)Peak memory usage: 227 MB
% 141.90/20.67 % (1200891)Instructions burned: 14155 (million)
% 141.90/20.67 % (1200921)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=160874989:cts=off:i=3034:av=off:er=known:fsd=on_2880 on theBenchmark for (2880ds/3034Mi)
% 141.90/20.67 % (1200901)Instruction limit reached!
% 141.90/20.67 % (1200901)------------------------------
% 141.90/20.67 % (1200901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.90/20.67 % (1200901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.90/20.67 % (1200901)CaDiCaL version: 2.1.3
% 141.90/20.67 % (1200901)Termination reason: Instruction limit
% 141.90/20.67 % (1200901)Termination phase: Saturation
% 141.90/20.67 % (1200901)Time elapsed: 7.281 s
% 141.90/20.67 % (1200901)Peak memory usage: 240 MB
% 141.90/20.67 % (1200901)Instructions burned: 12113 (million)
% 141.90/20.67 % (1200923)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3740615809:st=2:s2a=on:i=524:s2at=2:ss=axioms_2877 on theBenchmark for (2877ds/524Mi)
% 141.90/20.67 % (1200923)Instruction limit reached!
% 141.90/20.67 % (1200923)------------------------------
% 141.90/20.67 % (1200923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.90/20.67 % (1200923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.08/26.66 % (1200923)CaDiCaL version: 2.1.3
% 79.08/26.66 % (1200923)Termination reason: Instruction limit
% 79.08/26.66 % (1200923)Termination phase: Saturation
% 79.08/26.66 % (1200923)Time elapsed: 0.227 s
% 79.08/26.66 % (1200923)Peak memory usage: 90 MB
% 79.08/26.66 % (1200923)Instructions burned: 526 (million)
% 79.08/26.66 % (1200925)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=752897807:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2873 on theBenchmark for (2873ds/1016Mi)
% 79.08/26.66 % (1200925)Instruction limit reached!
% 79.08/26.66 % (1200925)------------------------------
% 79.08/26.66 % (1200925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.08/26.66 % (1200925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.08/26.66 % (1200925)CaDiCaL version: 2.1.3
% 79.08/26.66 % (1200925)Termination reason: Instruction limit
% 79.08/26.66 % (1200925)Termination phase: Saturation
% 79.08/26.66 % (1200925)Time elapsed: 0.488 s
% 79.08/26.66 % (1200925)Peak memory usage: 92 MB
% 79.08/26.66 % (1200925)Instructions burned: 1017 (million)
% 79.08/26.66 % (1200928)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3014613427:i=14123:bd=preordered:ins=4_2866 on theBenchmark for (2866ds/14123Mi)
% 79.08/26.66 % (1200913)Instruction limit reached!
% 79.08/26.66 % (1200913)------------------------------
% 79.08/26.66 % (1200913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.08/26.66 % (1200913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.08/26.66 % (1200913)CaDiCaL version: 2.1.3
% 79.08/26.66 % (1200913)Termination reason: Instruction limit
% 79.08/26.66 % (1200913)Termination phase: Saturation
% 79.08/26.66 % (1200913)Time elapsed: 5.856 s
% 79.08/26.66 % (1200913)Peak memory usage: 185 MB
% 79.08/26.66 % (1200913)Instructions burned: 9925 (million)
% 79.08/26.66 % (1200931)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=171776001:i=5781:kws=precedence:bd=all:rawr=on_2862 on theBenchmark for (2862ds/5781Mi)
% 79.08/26.66 % (1200921)Instruction limit reached!
% 79.08/26.66 % (1200921)------------------------------
% 79.08/26.66 % (1200921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.08/26.66 % (1200921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.08/26.66 % (1200921)CaDiCaL version: 2.1.3
% 79.08/26.66 % (1200921)Termination reason: Instruction limit
% 79.08/26.66 % (1200921)Termination phase: Saturation
% 79.08/26.66 % (1200921)Time elapsed: 1.829 s
% 79.08/26.66 % (1200921)Peak memory usage: 150 MB
% 79.08/26.66 % (1200921)Instructions burned: 3035 (million)
% 79.08/26.66 % (1200958)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=3702496609:i=2448:gtgl=5:bd=preordered:gtg=all_2860 on theBenchmark for (2860ds/2448Mi)
% 79.08/26.66 % (1200919)Instruction limit reached!
% 79.08/26.66 % (1200919)------------------------------
% 79.08/26.66 % (1200919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.08/26.66 % (1200919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.08/26.66 % (1200919)CaDiCaL version: 2.1.3
% 79.08/26.66 % (1200919)Termination reason: Instruction limit
% 79.08/26.66 % (1200919)Termination phase: Saturation
% 79.08/26.66 % (1200919)Time elapsed: 3.129 s
% 79.08/26.66 % (1200919)Peak memory usage: 196 MB
% 79.08/26.66 % (1200919)Instructions burned: 11147 (million)
% 79.08/26.66 % (1201065)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1687931344:i=3223:kws=precedence:fgj=on:av=off_2856 on theBenchmark for (2856ds/3223Mi)
% 79.08/26.66 % (1201065)Instruction limit reached!
% 79.08/26.66 % (1201065)------------------------------
% 79.08/26.66 % (1201065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.08/26.66 % (1201065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.08/26.66 % (1201065)CaDiCaL version: 2.1.3
% 79.08/26.66 % (1201065)Termination reason: Instruction limit
% 79.08/26.66 % (1201065)Termination phase: Saturation
% 79.08/26.66 % (1201065)Time elapsed: 1.133 s
% 79.08/26.66 % (1201065)Peak memory usage: 152 MB
% 79.08/26.66 % (1201065)Instructions burned: 3226 (million)
% 79.08/26.66 % (1201210)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=4209882455:st=5.6:i=2033:sd=3:ss=axioms_2843 on theBenchmark for (2843ds/2033Mi)
% 79.08/26.66 % (1200958)Instruction limit reached!
% 79.08/26.66 % (1200958)------------------------------
% 79.08/26.66 % (1200958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.08/26.66 % (1200958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.08/26.66 % (1200958)CaDiCaL version: 2.1.3
% 79.08/26.66 % (1200958)Termination reason: Instruction limit
% 79.08/26.66 % (1200958)Termination phase: Saturation
% 79.08/26.66 % (1200958)Time elapsed: 1.683 s
% 79.08/26.66 % (1200958)Peak memory usage: 143 MB
% 79.08/26.66 % (1200958)Instructions burned: 2448 (million)
% 79.08/26.66 % (1201217)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1931233018:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2841 on theBenchmark for (2841ds/2055Mi)
% 79.08/26.66 % (1201210)Instruction limit reached!
% 79.08/26.66 % (1201210)------------------------------
% 79.08/26.66 % (1201210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.08/26.66 % (1201210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.08/26.66 % (1201210)CaDiCaL version: 2.1.3
% 79.08/26.66 % (1201210)Termination reason: Instruction limit
% 79.08/26.66 % (1201210)Termination phase: Saturation
% 79.08/26.66 % (1201210)Time elapsed: 1.062 s
% 79.08/26.66 % (1201210)Peak memory usage: 138 MB
% 79.08/26.66 % (1201210)Instructions burned: 2034 (million)
% 79.08/26.66 % (1201243)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=3081059399:i=21611:sd=3:ss=axioms_2831 on theBenchmark for (2831ds/21611Mi)
% 79.08/26.66 % (1200931)Instruction limit reached!
% 79.08/26.66 % (1200931)------------------------------
% 79.08/26.66 % (1200931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.08/26.66 % (1200931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.08/26.66 % (1200931)CaDiCaL version: 2.1.3
% 79.08/26.66 % (1200931)Termination reason: Instruction limit
% 79.08/26.66 % (1200931)Termination phase: Saturation
% 79.08/26.66 % (1200931)Time elapsed: 4.190 s
% 79.08/26.66 % (1200931)Peak memory usage: 113 MB
% 79.08/26.66 % (1200931)Instructions burned: 5781 (million)
% 79.08/26.66 % (1201217)Instruction limit reached!
% 79.08/26.66 % (1201217)------------------------------
% 79.08/26.66 % (1201217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.08/26.66 % (1201217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.08/26.66 % (1201217)CaDiCaL version: 2.1.3
% 79.08/26.66 % (1201217)Termination reason: Instruction limit
% 79.08/26.66 % (1201217)Termination phase: Saturation
% 79.08/26.66 % (1201217)Time elapsed: 2.051 s
% 79.08/26.66 % (1201217)Peak memory usage: 136 MB
% 79.08/26.66 % (1201217)Instructions burned: 2055 (million)
% 79.08/26.66 % (1201247)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1686395242:i=4835:sd=13:ss=axioms:sgt=23_2818 on theBenchmark for (2818ds/4835Mi)
% 79.08/26.66 % (1201248)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=2699245973:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2818 on theBenchmark for (2818ds/797Mi)
% 79.08/26.66 % (1201248)Instruction limit reached!
% 79.08/26.66 % (1201248)------------------------------
% 79.08/26.66 % (1201248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.08/26.66 % (1201248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.08/26.66 % (1201248)CaDiCaL version: 2.1.3
% 79.08/26.66 % (1201248)Termination reason: Instruction limit
% 79.08/26.66 % (1201248)Termination phase: Saturation
% 79.08/26.66 % (1201248)Time elapsed: 0.833 s
% 79.08/26.66 % (1201248)Peak memory usage: 100 MB
% 79.08/26.66 % (1201248)Instructions burned: 797 (million)
% 79.08/26.66 % (1201255)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=819218588:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2806 on theBenchmark for (2806ds/2326Mi)
% 79.08/26.66 % (1201255)Refutation not found, incomplete strategy
% 79.08/26.66 % (1201255)------------------------------
% 79.08/26.66 % (1201255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.08/26.66 % (1201255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.08/26.66 % (1201255)CaDiCaL version: 2.1.3
% 79.08/26.66 % (1201255)Termination reason: Refutation not found, incomplete strategy
% 79.08/26.66 % (1201255)Time elapsed: 0.092 s
% 79.08/26.66 % (1201255)Peak memory usage: 91 MB
% 79.08/26.66 % (1201255)Instructions burned: 94 (million)
% 79.08/26.66 % (1201255)------------------------------
% 79.08/26.66 % (1201255)------------------------------
% 79.08/26.66 % (1201259)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3284826109:i=6038:nm=6_2799 on theBenchmark for (2799ds/6038Mi)
% 79.08/26.66 % (1201259)Refutation not found, incomplete strategy
% 79.08/26.66 % (1201259)------------------------------
% 79.08/26.66 % (1201259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.08/26.66 % (1201259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.08/26.66 % (1201259)CaDiCaL version: 2.1.3
% 79.08/26.66 % (1201259)Termination reason: Refutation not found, incomplete strategy
% 79.08/26.66 % (1201259)Time elapsed: 0.917 s
% 79.08/26.66 % (1201259)Peak memory usage: 140 MB
% 79.08/26.66 % (1201259)Instructions burned: 1038 (million)
% 79.08/26.66 % (1201259)------------------------------
% 79.08/26.66 % (1201259)------------------------------
% 79.08/26.66 % (1201273)lrs+10_1_sil=32000:sp=occurrence:random_seed=1514112984:st=2:i=33334:sd=3:ss=included:sgt=32_2784 on theBenchmark for (2784ds/33334Mi)
% 79.08/26.66 % (1201247)Instruction limit reached!
% 79.08/26.66 % (1201247)------------------------------
% 79.08/26.66 % (1201247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.08/26.66 % (1201247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.08/26.66 % (1201247)CaDiCaL version: 2.1.3
% 79.08/26.66 % (1201247)Termination reason: Instruction limit
% 79.08/26.66 % (1201247)Termination phase: Saturation
% 79.08/26.66 % (1201247)Time elapsed: 4.506 s
% 79.08/26.66 % (1201247)Peak memory usage: 111 MB
% 79.08/26.66 % (1201247)Instructions burned: 4836 (million)
% 79.08/26.66 % (1201277)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=650152683:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2770 on theBenchmark for (2770ds/1008Mi)
% 79.08/26.66 % (1201277)Refutation not found, incomplete strategy
% 79.08/26.66 % (1201277)------------------------------
% 79.08/26.66 % (1201277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.08/26.66 % (1201277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.08/26.66 % (1201277)CaDiCaL version: 2.1.3
% 79.08/26.66 % (1201277)Termination reason: Refutation not found, incomplete strategy
% 79.08/26.66 % (1201277)Time elapsed: 0.073 s
% 79.08/26.66 % (1201277)Peak memory usage: 90 MB
% 79.08/26.66 % (1201277)Instructions burned: 66 (million)
% 79.08/26.66 % (1201277)------------------------------
% 79.08/26.66 % (1201277)------------------------------
% 79.08/26.66 % (1201279)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=3313359480:i=8327:s2at=5:bd=preordered_2762 on theBenchmark for (2762ds/8327Mi)
% 79.08/26.66 % (1201279)First to succeed.
% 79.08/26.66 % (1201279)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1200830"
% 79.08/26.66 % (1201279)Refutation found. Thanks to Tanya!
% 79.08/26.66 % SZS status Theorem for theBenchmark
% 79.08/26.66 % SZS output start Proof for theBenchmark
% See solution above
% 184.89/26.88 % (1201279)------------------------------
% 184.89/26.88 % (1201279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 184.89/26.88 % (1201279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.89/26.88 % (1201279)CaDiCaL version: 2.1.3
% 184.89/26.88 % (1201279)Termination reason: Refutation
% 184.89/26.88 % (1201279)Time elapsed: 1.471 s
% 184.89/26.88 % (1201279)Peak memory usage: 140 MB
% 184.89/26.88 % (1201279)Instructions burned: 1397 (million)
% 184.89/26.88 % (1201279)------------------------------
% 184.89/26.88 % (1201279)------------------------------
% 184.89/26.88 % (1200830)Success in time 26.039 s
% 184.89/26.88 % Vampire exiting
%------------------------------------------------------------------------------