%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ITP387_1 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p 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 : Fri Sep 25 01:49:32 PM UTC 2026
% Result : Theorem 138.92s 29.07s
% Output : CNFRefutation 138.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP387_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n008.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 18:31:55 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.41
% 0.10/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.41
% 0.10/0.41 % Detected problem language: tptp
% 0.10/0.42 % Proving...
% 138.92/29.07 % SZS status Started for theBenchmark.p
% 138.92/29.07 % SZS status Theorem for theBenchmark.p
% 138.92/29.07
% 138.92/29.07 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 138.92/29.07
% 138.92/29.07 % ------ iProver source info
% 138.92/29.07
% 138.92/29.07 % git: date: 2026-07-19 20:42:38 +0200
% 138.92/29.07 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 138.92/29.07 % git: non_committed_changes: false
% 138.92/29.07
% 138.92/29.07 % ------ Parsing...
% 138.92/29.07 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 138.92/29.07 %
% 138.92/29.07
% 138.92/29.07 % ------ Preprocessing... sup_sim: 2 pe_s pe_e sup_sim: 0 pe_s pe_e %
% 138.92/29.07
% 138.92/29.07 % ------ Preprocessing...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 138.92/29.07 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e % ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 138.92/29.07 %
% 138.92/29.07
% 138.92/29.07 % ------ Preprocessing...
% 138.92/29.07 % ------ Proving...
% 138.92/29.07 % ------ Problem Properties
% 138.92/29.07
% 138.92/29.07 %
% 138.92/29.07 % clauses 41
% 138.92/29.07 % conjectures 0
% 138.92/29.07 % EPR 0
% 138.92/29.07 % Horn 41
% 138.92/29.07 % unary 19
% 138.92/29.07 % binary 22
% 138.92/29.07 % lits 63
% 138.92/29.07 % lits eq 63
% 138.92/29.07 % fd_pure 0
% 138.92/29.07 % fd_pseudo 0
% 138.92/29.07 % fd_cond 0
% 138.92/29.07 % fd_pseudo_cond 22
% 138.92/29.07 % AC symbols 2
% 138.92/29.07
% 138.92/29.07 % ------ Schedule dynamic 5 is on
% 138.92/29.07
% 138.92/29.07 % ------ no conjectures: strip conj schedule
% 138.92/29.07
% 138.92/29.07 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 138.92/29.07
% 138.92/29.07
% 138.92/29.07 % ------
% 138.92/29.07 % Current options:
% 138.92/29.07 % ------
% 138.92/29.07
% 138.92/29.07
% 138.92/29.07 %
% 138.92/29.07
% 138.92/29.07 % ------ Proving...
% 138.92/29.07 % Proof_search_loop: time out after: 4613 full_loop iterations
% 138.92/29.07
% 138.92/29.07 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" stripped conjectures Time Limit: 15.
% 138.92/29.07
% 138.92/29.07
% 138.92/29.07 % ------
% 138.92/29.07 % Current options:
% 138.92/29.07 % ------
% 138.92/29.07
% 138.92/29.07
% 138.92/29.07 %
% 138.92/29.07
% 138.92/29.07 % ------ Proving...
% 138.92/29.07 % Proof_search_loop: time out after: 7317 full_loop iterations
% 138.92/29.07
% 138.92/29.07 % ------ Option_1: Negative Selections stripped conjectures Time Limit: 35.
% 138.92/29.07
% 138.92/29.07
% 138.92/29.07 % ------
% 138.92/29.07 % Current options:
% 138.92/29.07 % ------
% 138.92/29.07
% 138.92/29.07
% 138.92/29.07 %
% 138.92/29.07
% 138.92/29.07 % ------ Proving...
% 138.92/29.07 %
% 138.92/29.07
% 138.92/29.07 % SZS status Theorem for theBenchmark.p
% 138.92/29.07
% 138.92/29.07 % SZS output start CNFRefutation for theBenchmark.p
% 138.92/29.07
% 138.92/29.07 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$').
% 138.92/29.07 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).
% 138.92/29.07 tff(pred_def_2, type, 'fun_app$g': ('C_ell2_d_ell2_cblinfun_bool_fun$' * 'C_ell2_d_ell2_cblinfun$') > $o).
% 138.92/29.07 tff(pred_def_3, type, 'member$h': ('C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_set_set$') > $o).
% 138.92/29.07 tff(pred_def_4, type, 'fun_app$a': ('A_c_prod_bool_fun$' * 'A_c_prod$') > $o).
% 138.92/29.07 tff(pred_def_5, type, 'member$d': ('A$' * 'A_set$') > $o).
% 138.92/29.07 tff(pred_def_6, type, 'less_eq$g': ('A_c_prod_ell2_ccsubspace$' * 'A_c_prod_ell2_ccsubspace$') > $o).
% 138.92/29.07 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).
% 138.92/29.07 tff(pred_def_8, type, 'cdependent$': 'A_c_prod_ell2_set$' > $o).
% 138.92/29.07 tff(pred_def_9, type, 'nO_MATCH$a': ('A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'Complex$') > $o).
% 138.92/29.07 tff(pred_def_10, type, 'member$a': ('A_c_prod$' * 'A_c_prod_set$') > $o).
% 138.92/29.07 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).
% 138.92/29.07 tff(pred_def_12, type, 'less_eq$b': ('C_ell2_d_ell2_cblinfun_set$' * 'C_ell2_d_ell2_cblinfun_set$') > $o).
% 138.92/29.07 tff(pred_def_13, type, 'cdependent$b': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$' > $o).
% 138.92/29.07 tff(pred_def_14, type, 'cblinfun_extension_exists$b': ('B_d_prod_ell2_set$' * 'B_d_prod_ell2_a_c_prod_ell2_fun$') > $o).
% 138.92/29.07 tff(pred_def_15, type, 'member$': ('C_a_prod$' * 'C_a_prod_set$') > $o).
% 138.92/29.07 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).
% 138.92/29.07 tff(pred_def_17, type, 'cblinfun_extension_exists$c': ('C_ell2_set$' * 'C_ell2_d_ell2_fun$') > $o).
% 138.92/29.07 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).
% 138.92/29.07 tff(pred_def_19, type, 'member$f': ('Complex$' * 'Complex_set$') > $o).
% 138.92/29.07 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).
% 138.92/29.07 tff(pred_def_21, type, 'member$q': ('A_ell2$' * 'A_ell2_set$') > $o).
% 138.92/29.07 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).
% 138.92/29.07 tff(pred_def_23, type, 'cblinfun_extension_exists$d': ('A_ell2_set$' * 'A_ell2_b_ell2_fun$') > $o).
% 138.92/29.07 tff(pred_def_24, type, 'member$e': ('D_ell2$' * 'D_ell2_set$') > $o).
% 138.92/29.07 tff(pred_def_25, type, 'heterogenous_same_type_cblinfun$a': ('A_c_prod_ell2_itself$' * 'B_d_prod_ell2_itself$') > $o).
% 138.92/29.07 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).
% 138.92/29.07 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).
% 138.92/29.07 tff(pred_def_28, type, 'member$n': ('A_c_prod_a_c_prod_prod$' * 'A_c_prod_a_c_prod_prod_set$') > $o).
% 138.92/29.07 tff(pred_def_29, type, 'member$b': ('B_d_prod_ell2$' * 'B_d_prod_ell2_set$') > $o).
% 138.92/29.07 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).
% 138.92/29.07 tff(pred_def_31, type, 'member$p': ('C_ell2$' * 'C_ell2_set$') > $o).
% 138.92/29.07 tff(pred_def_32, type, 'less_eq$d': ('A_c_prod_set$' * 'A_c_prod_set$') > $o).
% 138.92/29.07 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).
% 138.92/29.07 tff(pred_def_34, type, 'fun_app$b': ('B_d_prod_ell2_bool_fun$' * 'B_d_prod_ell2$') > $o).
% 138.92/29.07 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).
% 138.92/29.07 tff(pred_def_36, type, 'heterogenous_same_type_cblinfun$': ('B_d_prod_ell2_itself$' * 'A_c_prod_ell2_itself$') > $o).
% 138.92/29.07 tff(pred_def_37, type, 'less_eq$f': ('Complex$' * 'Complex$') > $o).
% 138.92/29.07 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).
% 138.92/29.07 tff(pred_def_39, type, 'is_ortho_set$': 'A_c_prod_ell2_set$' > $o).
% 138.92/29.07 tff(pred_def_40, type, 'fun_app$c': ('A_c_prod_ell2_bool_fun$' * 'A_c_prod_ell2$') > $o).
% 138.92/29.07 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).
% 138.92/29.07 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).
% 138.92/29.07 tff(pred_def_43, type, 'nO_MATCH$': ('C_ell2_d_ell2_cblinfun$' * 'Complex$') > $o).
% 138.92/29.07 tff(pred_def_44, type, 'fun_app$ab': ('C_bool_fun$' * 'C$') > $o).
% 138.92/29.07 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).
% 138.92/29.07 tff(pred_def_46, type, 'cdependent$a': 'C_ell2_d_ell2_cblinfun_set$' > $o).
% 138.92/29.07 tff(pred_def_47, type, 'fun_app$': ('C_a_prod_bool_fun$' * 'C_a_prod$') > $o).
% 138.92/29.07 tff(pred_def_48, type, 'cblinfun_extension_exists$e': ('A_c_prod_ell2_set$' * 'A_c_prod_ell2_b_d_prod_ell2_fun$') > $o).
% 138.92/29.07 tff(pred_def_49, type, 'fun_app$d': ('A_bool_fun$' * 'A$') > $o).
% 138.92/29.07 tff(pred_def_50, type, 'member$i': ('C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun_set$') > $o).
% 138.92/29.07 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).
% 138.92/29.07 tff(pred_def_52, type, 'member$c': ('A_c_prod_ell2$' * 'A_c_prod_ell2_set$') > $o).
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_55, type, 'fun_app$u': ('C_ell2_d_ell2_fun$' * 'C_ell2$') > 'D_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_57, type, 'fun_app$al': ('C_c_fun$' * 'C$') > 'C$').
% 138.92/29.07 tff(func_def_58, type, 'ccspan$a': 'B_d_prod_ell2_set$' > 'B_d_prod_ell2_ccsubspace$').
% 138.92/29.07 tff(func_def_59, type, 'tensor_ell2$b': ('A_ell2$' * 'C_ell2$') > 'A_c_prod_ell2$').
% 138.92/29.07 tff(func_def_60, type, 'unitary$': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun$').
% 138.92/29.07 tff(func_def_61, type, 'fun_app$ak': ('A_a_fun$' * 'A$') > 'A$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_63, type, 'id$': 'A_c_prod_a_c_prod_fun$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_65, type, 'b1$': 'C_ell2_d_ell2_cblinfun$').
% 138.92/29.07 tff(func_def_66, type, 'uu$': 'C_a_prod_set$' > 'C_a_prod_bool_fun$').
% 138.92/29.07 tff(func_def_67, type, 'case_prod$': 'A_c_a_c_prod_fun_fun$' > 'A_c_prod_a_c_prod_fun$').
% 138.92/29.07 tff(func_def_68, type, 'tensor_ell2$i': ('A_c_prod_ell2$' * 'A_ell2$') > 'A_c_prod_a_prod_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_71, type, 'plus$u': ('B_d_prod_ell2$' * 'B_d_prod_ell2$') > 'B_d_prod_ell2$').
% 138.92/29.07 tff(func_def_72, type, 'i$': 'A$').
% 138.92/29.07 tff(func_def_73, type, 'swap$e': 'C_a_prod_a_c_prod_fun$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_77, type, 'snd$e': 'A_c_prod$' > 'C$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_79, type, 'ket$': 'A_c_prod_a_c_prod_ell2_fun$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_81, type, 'image$f': ('A_c_prod_a_c_prod_ell2_fun$' * 'A_c_prod_set$') > 'A_c_prod_ell2_set$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_83, type, 'ket$g': 'B_d_prod$' > 'B_d_prod_ell2$').
% 138.92/29.07 tff(func_def_84, type, 'heterogenous_cblinfun_id$a': 'B_d_prod_ell2_a_c_prod_ell2_cblinfun$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_86, type, 'pair$h': ('D_ell2$' * 'D_ell2$') > 'D_ell2_d_ell2_prod$').
% 138.92/29.07 tff(func_def_87, type, 'top$e': 'A_c_prod_ell2_ccsubspace$').
% 138.92/29.07 tff(func_def_88, type, 'cblinfun_apply$a': 'A_ell2_b_ell2_cblinfun$' > 'A_ell2_b_ell2_fun$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_90, type, 'ket$h': 'B$' > 'B_ell2$').
% 138.92/29.07 tff(func_def_91, type, 'uua$': 'A_c_prod_set$' > 'A_c_prod_bool_fun$').
% 138.92/29.07 tff(func_def_92, type, 'tensor_ell2$h': ('C_ell2$' * 'A_ell2$') > 'C_a_prod_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_94, type, 'a$': 'A_ell2_b_ell2_cblinfun$').
% 138.92/29.07 tff(func_def_95, type, 'plus$af': ('C_ell2$' * 'C_ell2$') > 'C_ell2$').
% 138.92/29.07 tff(func_def_96, type, 'fun_app$ai': ('C_a_prod_a_c_prod_fun$' * 'C_a_prod$') > 'A_c_prod$').
% 138.92/29.07 tff(func_def_97, type, 'tensor_ell2$e': ('A_c_prod_ell2$' * 'A_c_prod_ell2$') > 'A_c_prod_a_c_prod_prod_ell2$').
% 138.92/29.07 tff(func_def_98, type, 'type$': 'B_d_prod_ell2_itself$').
% 138.92/29.07 tff(func_def_99, type, 'pair$r': ('A$' * 'A_c_prod$') > 'A_a_c_prod_prod$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_102, type, 'plus$h': ('D_ell2_complex_prod$' * 'D_ell2_complex_prod$') > 'D_ell2_complex_prod$').
% 138.92/29.07 tff(func_def_103, type, 'fst$k': 'A_c_prod_ell2_complex_prod$' > 'A_c_prod_ell2$').
% 138.92/29.07 tff(func_def_104, type, 'tensor_ell2$f': ('A_ell2$' * 'A_ell2$') > 'A_a_prod_ell2$').
% 138.92/29.07 tff(func_def_105, type, 'fst$i': 'Complex_d_ell2_prod$' > 'Complex$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_107, type, 'snd$g': 'Complex_complex_prod$' > 'Complex$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_109, type, 'cblinfun_apply$v': ('D_ell2_d_ell2_cblinfun$' * 'D_ell2$') > 'D_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_113, type, 'image$': ('A_c_prod_c_a_prod_fun$' * 'A_c_prod_set$') > 'C_a_prod_set$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_115, type, 'cspan$a': 'C_ell2_d_ell2_cblinfun_set$' > 'C_ell2_d_ell2_cblinfun_set$').
% 138.92/29.07 tff(func_def_116, type, 'collect$a': 'A_c_prod_bool_fun$' > 'A_c_prod_set$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_118, type, 'isometry$': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_bool_fun$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_120, type, 'fst$a': 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun$').
% 138.92/29.07 tff(func_def_121, type, 'uuc$': 'A_c_prod_ell2_set$' > 'A_c_prod_ell2_bool_fun$').
% 138.92/29.07 tff(func_def_122, type, 'pair$i': ('A_c_prod_ell2$' * 'Complex$') > 'A_c_prod_ell2_complex_prod$').
% 138.92/29.07 tff(func_def_123, type, 'ccspan$': 'A_c_prod_ell2_set$' > 'A_c_prod_ell2_ccsubspace$').
% 138.92/29.07 tff(func_def_124, type, 'pair$g': ('Complex$' * 'D_ell2$') > 'Complex_d_ell2_prod$').
% 138.92/29.07 tff(func_def_125, type, 'image$a': ('C_a_prod_a_c_prod_fun$' * 'C_a_prod_set$') > 'A_c_prod_set$').
% 138.92/29.07 tff(func_def_126, type, 'uub$': 'B_d_prod_ell2_set$' > 'B_d_prod_ell2_bool_fun$').
% 138.92/29.07 tff(func_def_127, type, 'plus$': ('Complex$' * 'Complex$') > 'Complex$').
% 138.92/29.07 tff(func_def_128, type, 'snd$a': 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_prod$' > 'C_ell2_d_ell2_cblinfun$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_131, type, 'zero$b': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$').
% 138.92/29.07 tff(func_def_132, type, 'swap$': 'A_c_prod_a_c_prod_prod$' > 'A_c_prod_a_c_prod_prod$').
% 138.92/29.07 tff(func_def_133, type, 'fst$g': 'Complex_complex_prod$' > 'Complex$').
% 138.92/29.07 tff(func_def_134, type, 'snd$h': 'D_ell2_complex_prod$' > 'Complex$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_136, type, 'collect$b': 'B_d_prod_ell2_bool_fun$' > 'B_d_prod_ell2_set$').
% 138.92/29.07 tff(func_def_137, type, 'cblinfun_apply$e': ('C_ell2_b_ell2_cblinfun$' * 'C_ell2$') > 'B_ell2$').
% 138.92/29.07 tff(func_def_138, type, 'plus$a': 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun_fun$').
% 138.92/29.07 tff(func_def_139, type, 'divide$': 'C_ell2_d_ell2_cblinfun$' > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$').
% 138.92/29.07 tff(func_def_140, type, 'uud$': 'A_set$' > 'A_bool_fun$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_142, type, 'plus$x': ('D_ell2_set$' * 'D_ell2_set$') > 'D_ell2_set$').
% 138.92/29.07 tff(func_def_143, type, 'cinner$': ('A_c_prod_ell2$' * 'A_c_prod_ell2$') > 'Complex$').
% 138.92/29.07 tff(func_def_144, type, 'fun_app$ac': ('A_c_bool_fun_fun$' * 'A$') > 'C_bool_fun$').
% 138.92/29.07 tff(func_def_145, type, 'collect$d': 'A_bool_fun$' > 'A_set$').
% 138.92/29.07 tff(func_def_146, type, 'fun_app$am': ('A_c_fun$' * 'A$') > 'C$').
% 138.92/29.07 tff(func_def_147, type, 'closure$': 'A_c_prod_ell2_set$' > 'A_c_prod_ell2_set$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_150, type, 'minus$g': ('Complex$' * 'Complex$') > 'Complex$').
% 138.92/29.07 tff(func_def_151, type, 'fst$j': 'D_ell2_d_ell2_prod$' > 'D_ell2$').
% 138.92/29.07 tff(func_def_152, type, 'closure$a': 'C_ell2_d_ell2_cblinfun_set$' > 'C_ell2_d_ell2_cblinfun_set$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_154, type, 'snd$j': 'D_ell2_d_ell2_prod$' > 'D_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_156, type, 'fun_app$p': ('C_a_c_prod_fun$' * 'C$') > 'A_c_prod$').
% 138.92/29.07 tff(func_def_157, type, 'minus$c': ('B_d_prod_ell2$' * 'B_d_prod_ell2$') > 'B_d_prod_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_159, type, 'zero$d': 'Complex$').
% 138.92/29.07 tff(func_def_160, type, 'cblinfun_apply$aa': ('B_ell2_b_d_prod_ell2_cblinfun$' * 'B_ell2$') > 'B_d_prod_ell2$').
% 138.92/29.07 tff(func_def_161, type, 'minus$d': ('A_c_prod_ell2$' * 'A_c_prod_ell2$') > 'A_c_prod_ell2$').
% 138.92/29.07 tff(func_def_162, type, 'cblinfun_apply$ad': ('B_ell2_a_c_prod_ell2_cblinfun$' * 'B_ell2$') > 'A_c_prod_ell2$').
% 138.92/29.07 tff(func_def_163, type, 'plus$m': ('A_c_prod_ell2$' * 'A_c_prod_ell2$') > 'A_c_prod_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_165, type, 'plus$k': ('D_ell2_d_ell2_prod$' * 'D_ell2_d_ell2_prod$') > 'D_ell2_d_ell2_prod$').
% 138.92/29.07 tff(func_def_166, type, 'cblinfun_apply$ae': ('D_ell2_a_c_prod_ell2_cblinfun$' * 'D_ell2$') > 'A_c_prod_ell2$').
% 138.92/29.07 tff(func_def_167, type, 'pair$': 'A_c_a_c_prod_fun_fun$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_169, type, 'scaleC$a': ('Complex$' * 'B_d_prod_ell2$') > 'B_d_prod_ell2$').
% 138.92/29.07 tff(func_def_170, type, 'heterogenous_cblinfun_id$': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$').
% 138.92/29.07 tff(func_def_171, type, 'top$b': 'A_c_prod_ell2_set$').
% 138.92/29.07 tff(func_def_172, type, 'tensor_ell2$g': ('C_ell2$' * 'C_ell2$') > 'C_c_prod_ell2$').
% 138.92/29.07 tff(func_def_173, type, 'cblinfun_apply$b': 'C_ell2_d_ell2_cblinfun$' > 'C_ell2_d_ell2_fun$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_175, type, 'top$a': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_set$').
% 138.92/29.07 tff(func_def_176, type, 'fst$l': 'Complex_a_c_prod_ell2_prod$' > 'Complex$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_179, type, 'zero$': 'B_d_prod_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_182, type, 'swap$d': 'A_c_prod_c_a_prod_fun$').
% 138.92/29.07 tff(func_def_183, type, 'less_eq$': 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_186, type, 'map_prod$': ('A_a_fun$' * 'C_c_fun$') > 'A_c_prod_a_c_prod_fun$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_188, type, 'fst$c': 'A_c_prod_a_c_prod_prod$' > 'A_c_prod$').
% 138.92/29.07 tff(func_def_189, type, 'fun_app$j': ('C_ell2_d_ell2_cblinfun_complex_fun$' * 'C_ell2_d_ell2_cblinfun$') > 'Complex$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_191, type, 'tensor_ell2$k': ('A_ell2$' * 'A_c_prod_ell2$') > 'A_a_c_prod_prod_ell2$').
% 138.92/29.07 tff(func_def_192, type, 'pair$o': ('B$' * 'D$') > 'B_d_prod$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_195, type, 'pair$n': ('C$' * 'C$') > 'C_c_prod$').
% 138.92/29.07 tff(func_def_196, type, 'pair$l': ('C$' * 'A$') > 'C_a_prod$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_198, type, 'ket$i': 'D$' > 'D_ell2$').
% 138.92/29.07 tff(func_def_199, type, 'cblinfun_extension$d': ('A_ell2_set$' * 'A_ell2_b_ell2_fun$') > 'A_ell2_b_ell2_cblinfun$').
% 138.92/29.07 tff(func_def_200, type, 'cblinfun_apply$ak': ('Complex_d_ell2_cblinfun$' * 'Complex$') > 'D_ell2$').
% 138.92/29.07 tff(func_def_201, type, 'cblinfun_apply$aj': ('D_ell2_complex_cblinfun$' * 'D_ell2$') > 'Complex$').
% 138.92/29.07 tff(func_def_202, type, 'top$d': 'A_c_prod_set$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_205, type, 'curry$': 'A_c_prod_bool_fun$' > 'A_c_bool_fun_fun$').
% 138.92/29.07 tff(func_def_206, type, 'ket$c': 'A_c_prod_a_c_prod_prod$' > 'A_c_prod_a_c_prod_prod_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_210, type, 'top$': 'C_ell2_d_ell2_cblinfun_set$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_213, type, 'fun_app$ah': ('A_c_prod_c_a_prod_fun$' * 'A_c_prod$') > 'C_a_prod$').
% 138.92/29.07 tff(func_def_214, type, 'fun_app$o': ('A_c_prod_a_c_prod_ell2_fun$' * 'A_c_prod$') > 'A_c_prod_ell2$').
% 138.92/29.07 tff(func_def_215, type, 'ket$a': 'A$' > 'A_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_217, type, 'pair$f': ('D_ell2$' * 'Complex$') > 'D_ell2_complex_prod$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_220, type, 'plus$g': ('Complex_complex_prod$' * 'Complex_complex_prod$') > 'Complex_complex_prod$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_224, type, 'plus$i': ('D_ell2$' * 'D_ell2$') > 'D_ell2$').
% 138.92/29.07 tff(func_def_225, type, 'cblinfun_apply$h': ('A_ell2_a_ell2_cblinfun$' * 'A_ell2$') > 'A_ell2$').
% 138.92/29.07 tff(func_def_226, type, 'ket$d': 'C_a_prod$' > 'C_a_prod_ell2$').
% 138.92/29.07 tff(func_def_227, type, 'top$c': 'B_d_prod_ell2_set$').
% 138.92/29.07 tff(func_def_228, type, 'snd$i': 'Complex_d_ell2_prod$' > 'D_ell2$').
% 138.92/29.07 tff(func_def_229, type, 'cspan$c': 'B_d_prod_ell2_set$' > 'B_d_prod_ell2_set$').
% 138.92/29.07 tff(func_def_230, type, 'pair$q': ('A_c_prod$' * 'C$') > 'A_c_prod_c_prod$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_233, type, 'plus$ad': ('A_ell2$' * 'A_ell2$') > 'A_ell2$').
% 138.92/29.07 tff(func_def_234, type, 'tensor_ell2$a': ('B_d_prod_ell2$' * 'B_d_prod_ell2$') > 'B_d_prod_b_d_prod_prod_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_236, type, 'ket$e': 'A_a_prod$' > 'A_a_prod_ell2$').
% 138.92/29.07 tff(func_def_237, type, 'tensor_ell2$m': ('B_ell2$' * 'B_ell2$') > 'B_b_prod_ell2$').
% 138.92/29.07 tff(func_def_238, type, 'apsnd$': ('C_c_fun$' * 'A_c_prod$') > 'A_c_prod$').
% 138.92/29.07 tff(func_def_239, type, 'snd$c': 'A_c_prod_a_c_prod_prod$' > 'A_c_prod$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_241, type, 'uue$': 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_bool_fun_fun$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_243, type, 'plus$w': ('A_c_prod_ell2_set$' * 'A_c_prod_ell2_set$') > 'A_c_prod_ell2_set$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_248, type, 'type$a': 'A_c_prod_ell2_itself$').
% 138.92/29.07 tff(func_def_249, type, 'in_rel$': 'A_c_prod_set$' > 'A_c_bool_fun_fun$').
% 138.92/29.07 tff(func_def_250, type, 'ket$b': 'C$' > 'C_ell2$').
% 138.92/29.07 tff(func_def_251, type, 'pair$p': ('A_c_prod$' * 'A$') > 'A_c_prod_a_prod$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_253, type, 'minus$b': 'C_ell2_d_ell2_cblinfun$' > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_255, type, 'cblinfun_apply$k': ('C_ell2_a_ell2_cblinfun$' * 'C_ell2$') > 'A_ell2$').
% 138.92/29.07 tff(func_def_256, type, 'tensor_ell2$c': ('D_ell2$' * 'D_ell2$') > 'D_d_prod_ell2$').
% 138.92/29.07 tff(func_def_257, type, 'zero$c': 'A_c_prod_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_259, type, 'ket$k': 'A_c_prod_c_prod$' > 'A_c_prod_c_prod_ell2$').
% 138.92/29.07 tff(func_def_260, type, 'cblinfun_apply$u': ('B_ell2_b_ell2_cblinfun$' * 'B_ell2$') > 'B_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_263, type, 'cspan$': 'A_c_prod_ell2_set$' > 'A_c_prod_ell2_set$').
% 138.92/29.07 tff(func_def_264, type, 'ket$l': 'A_a_c_prod_prod$' > 'A_a_c_prod_prod_ell2$').
% 138.92/29.07 tff(func_def_265, type, 'curry$e': 'C_a_prod_bool_fun$' > 'C_a_bool_fun_fun$').
% 138.92/29.07 tff(func_def_266, type, 'pair$j': ('Complex$' * 'A_c_prod_ell2$') > 'Complex_a_c_prod_ell2_prod$').
% 138.92/29.07 tff(func_def_267, type, 'plus$y': ('Complex_set$' * 'Complex_set$') > 'Complex_set$').
% 138.92/29.07 tff(func_def_268, type, 'snd$d': 'C_a_prod$' > 'A$').
% 138.92/29.07 tff(func_def_269, type, 'cinner$a': ('B_d_prod_ell2$' * 'B_d_prod_ell2$') > 'Complex$').
% 138.92/29.07 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$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_272, type, 'gr$': ('A_set$' * 'A_c_fun$') > 'A_c_prod_set$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_274, type, 'scaleC$c': 'Complex$' > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$').
% 138.92/29.07 tff(func_def_275, type, 'pair$e': ('Complex$' * 'Complex$') > 'Complex_complex_prod$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_277, type, 'cblinfun_extension$c': ('C_ell2_set$' * 'C_ell2_d_ell2_fun$') > 'C_ell2_d_ell2_cblinfun$').
% 138.92/29.07 tff(func_def_278, type, 'cblinfun_apply$x': ('B_ell2_a_ell2_cblinfun$' * 'B_ell2$') > 'A_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_280, type, 'fun_app$ag': ('C_a_bool_fun_fun$' * 'C$') > 'A_bool_fun$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_282, type, 'scaleC$': ('Complex$' * 'A_c_prod_ell2$') > 'A_c_prod_ell2$').
% 138.92/29.07 tff(func_def_283, type, 'plus$t': ('B_ell2$' * 'B_ell2$') > 'B_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_285, type, 'j$': 'C$').
% 138.92/29.07 tff(func_def_286, type, 'fst$d': 'C_a_prod$' > 'C$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_288, type, 'snd$k': 'A_c_prod_ell2_complex_prod$' > 'Complex$').
% 138.92/29.07 tff(func_def_289, type, 'zero$a': 'C_ell2_d_ell2_cblinfun$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_291, type, 'ket$j': 'A_c_prod_a_prod$' > 'A_c_prod_a_prod_ell2$').
% 138.92/29.07 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$').
% 138.92/29.07 tff(func_def_293, type, sK0: ('A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$') > 'A_c_prod_ell2$').
% 138.92/29.07 tff(func_def_294, type, sK1: 'A_c_prod$' > 'A$').
% 138.92/29.07 tff(func_def_295, type, sK2: 'A_c_prod$' > 'C$').
% 138.92/29.07 tff(func_def_296, type, sK3: 'A_c_prod$' > 'A$').
% 138.92/29.07 tff(func_def_297, type, sK4: 'A_c_prod$' > 'C$').
% 138.92/29.07 tff(func_def_298, type, sK5: ('A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$') > 'A_c_prod$').
% 138.92/29.07 tff(func_def_299, type, sK6: ('A_ell2_b_ell2_cblinfun$' * 'A_ell2_b_ell2_cblinfun$') > 'A_ell2$').
% 138.92/29.07 tff(func_def_300, type, sK7: ('A_ell2_b_ell2_cblinfun$' * 'A_ell2_b_ell2_cblinfun$') > 'A$').
% 138.92/29.07 tff(func_def_301, type, sK8: ('C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun$') > 'C_ell2$').
% 138.92/29.07 tff(func_def_302, type, sK9: ('C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun$') > 'C$').
% 138.92/29.07 tff(f10,conjecture,(
% 138.92/29.07 '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$')))),
% 138.92/29.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture9)).
% 138.92/29.07
% 138.92/29.07 tff(f11,negated_conjecture,(
% 138.92/29.07 ~ '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$')))),
% 138.92/29.07 inference(negated_conjecture,[status(cth)],[f10])).
% 138.92/29.07
% 138.92/29.07 tff(f36,axiom,(
% 138.92/29.07 ! [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))),
% 138.92/29.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom34)).
% 138.92/29.07
% 138.92/29.07 tff(f37,axiom,(
% 138.92/29.07 ! [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))),
% 138.92/29.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom35)).
% 138.92/29.07
% 138.92/29.07 tff(f83,axiom,(
% 138.92/29.07 ! [X0 : 'A$',X1 : 'C$'] : 'tensor_ell2$b'('ket$a'(X0),'ket$b'(X1)) = 'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$',X0),X1))),
% 138.92/29.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom81)).
% 138.92/29.07
% 138.92/29.07 tff(f97,axiom,(
% 138.92/29.07 ! [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))),
% 138.92/29.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom95)).
% 138.92/29.07
% 138.92/29.07 tff(f212,axiom,(
% 138.92/29.07 ! [X0 : 'A_ell2_b_ell2_cblinfun$',X1 : 'C_ell2_d_ell2_cblinfun$',X2 : 'A_ell2$',X3 : 'C_ell2$'] : 'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'(X0,X1)),'tensor_ell2$b'(X2,X3)) = 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X0),X2),'fun_app$u'('cblinfun_apply$b'(X1),X3))),
% 138.92/29.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom210)).
% 138.92/29.07
% 138.92/29.07 tff(f257,axiom,(
% 138.92/29.07 ! [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)),
% 138.92/29.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom255)).
% 138.92/29.07
% 138.92/29.07 tff(f258,axiom,(
% 138.92/29.07 ! [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)),
% 138.92/29.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom256)).
% 138.92/29.07
% 138.92/29.07 tff(f645,plain,(
% 138.92/29.07 '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$')))),
% 138.92/29.07 inference(flattening,[],[f11])).
% 138.92/29.07
% 138.92/29.07 tff(f711,plain,(
% 138.92/29.07 '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$')))),
% 138.92/29.07 inference(cnf_transformation,[],[f645])).
% 138.92/29.07
% 138.92/29.07 tff(f729,plain,(
% 138.92/29.07 ( ! [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)) )),
% 138.92/29.07 inference(cnf_transformation,[],[f258])).
% 138.92/29.07
% 138.92/29.07 tff(f750,plain,(
% 138.92/29.07 ( ! [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)) )),
% 138.92/29.07 inference(cnf_transformation,[],[f257])).
% 138.92/29.07
% 138.92/29.07 tff(f770,plain,(
% 138.92/29.07 ( ! [X2 : 'A_ell2$',X3 : 'C_ell2$',X0 : 'A_ell2_b_ell2_cblinfun$',X1 : 'C_ell2_d_ell2_cblinfun$'] : ('fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'(X0,X1)),'tensor_ell2$b'(X2,X3)) = 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X0),X2),'fun_app$u'('cblinfun_apply$b'(X1),X3))) )),
% 138.92/29.07 inference(cnf_transformation,[],[f212])).
% 138.92/29.07
% 138.92/29.07 tff(f772,plain,(
% 138.92/29.07 ( ! [X0 : 'A$',X1 : 'C$'] : ('tensor_ell2$b'('ket$a'(X0),'ket$b'(X1)) = 'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$',X0),X1))) )),
% 138.92/29.07 inference(cnf_transformation,[],[f83])).
% 138.92/29.07
% 138.92/29.07 tff(f773,plain,(
% 138.92/29.07 ( ! [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))) )),
% 138.92/29.07 inference(cnf_transformation,[],[f97])).
% 138.92/29.07
% 138.92/29.07 tff(f779,plain,(
% 138.92/29.07 ( ! [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))) )),
% 138.92/29.07 inference(cnf_transformation,[],[f36])).
% 138.92/29.07
% 138.92/29.07 tff(f790,plain,(
% 138.92/29.07 ( ! [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))) )),
% 138.92/29.07 inference(cnf_transformation,[],[f37])).
% 138.92/29.07
% 138.92/29.07 tcf(c_49,negated_conjecture,
% 138.92/29.07 ('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$'))) != '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$')))),
% 138.92/29.07 inference(cnf_transformation,[],[f711])).
% 138.92/29.07
% 138.92/29.07 tcf(c_63,plain,![X0_'A_c_prod_ell2_b_d_prod_ell2_cblinfun':'A_c_prod_ell2_b_d_prod_ell2_cblinfun$',X1_'A_c_prod_ell2_b_d_prod_ell2_cblinfun':'A_c_prod_ell2_b_d_prod_ell2_cblinfun$']:
% 138.92/29.07 ('fun_app$r'('fun_app$s'('plus$b',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',X1_'A_c_prod_ell2_b_d_prod_ell2_cblinfun'),X0_'A_c_prod_ell2_b_d_prod_ell2_cblinfun')),
% 138.92/29.07 inference(cnf_transformation,[],[f729])).
% 138.92/29.07
% 138.92/29.07 tcf(c_79,plain,![X0_'C_ell2_d_ell2_cblinfun':'C_ell2_d_ell2_cblinfun$',X1_'C_ell2_d_ell2_cblinfun':'C_ell2_d_ell2_cblinfun$']:
% 138.92/29.07 ('fun_app$m'('fun_app$n'('plus$a',X0_'C_ell2_d_ell2_cblinfun'),X1_'C_ell2_d_ell2_cblinfun') = 'fun_app$m'('fun_app$n'('plus$a',X1_'C_ell2_d_ell2_cblinfun'),X0_'C_ell2_d_ell2_cblinfun')),
% 138.92/29.07 inference(cnf_transformation,[],[f750])).
% 138.92/29.07
% 138.92/29.07 tcf(c_94,plain,![X0_'C_ell2_d_ell2_cblinfun':'C_ell2_d_ell2_cblinfun$',X0_'C_ell2':'C_ell2$',X0_'A_ell2':'A_ell2$',X0_'A_ell2_b_ell2_cblinfun':'A_ell2_b_ell2_cblinfun$']:
% 138.92/29.07 ('tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X0_'A_ell2_b_ell2_cblinfun'),X0_'A_ell2'),'fun_app$u'('cblinfun_apply$b'(X0_'C_ell2_d_ell2_cblinfun'),X0_'C_ell2')) = 'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'(X0_'A_ell2_b_ell2_cblinfun',X0_'C_ell2_d_ell2_cblinfun')),'tensor_ell2$b'(X0_'A_ell2',X0_'C_ell2'))),
% 138.92/29.07 inference(cnf_transformation,[],[f770])).
% 138.92/29.07
% 138.92/29.07 tcf(c_96,plain,![X0_'C':'C$',X0_'A':'A$']:
% 138.92/29.07 ('fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$',X0_'A'),X0_'C')) = 'tensor_ell2$b'('ket$a'(X0_'A'),'ket$b'(X0_'C'))),
% 138.92/29.07 inference(cnf_transformation,[],[f772])).
% 138.92/29.07
% 138.92/29.07 tcf(c_97,plain,![X0_'D_ell2':'D_ell2$',X0_'B_ell2':'B_ell2$',X1_'D_ell2':'D_ell2$']:
% 138.92/29.07 ('plus$u'('tensor_ell2$'(X0_'B_ell2',X0_'D_ell2'),'tensor_ell2$'(X0_'B_ell2',X1_'D_ell2')) = 'tensor_ell2$'(X0_'B_ell2','plus$i'(X0_'D_ell2',X1_'D_ell2'))),
% 138.92/29.07 inference(cnf_transformation,[],[f773])).
% 138.92/29.07
% 138.92/29.07 tcf(c_103,plain,![X0_'C_ell2_d_ell2_cblinfun':'C_ell2_d_ell2_cblinfun$',X0_'C_ell2':'C_ell2$',X1_'C_ell2_d_ell2_cblinfun':'C_ell2_d_ell2_cblinfun$']:
% 138.92/29.07 ('plus$i'('fun_app$u'('cblinfun_apply$b'(X0_'C_ell2_d_ell2_cblinfun'),X0_'C_ell2'),'fun_app$u'('cblinfun_apply$b'(X1_'C_ell2_d_ell2_cblinfun'),X0_'C_ell2')) = 'fun_app$u'('cblinfun_apply$b'('fun_app$m'('fun_app$n'('plus$a',X0_'C_ell2_d_ell2_cblinfun'),X1_'C_ell2_d_ell2_cblinfun')),X0_'C_ell2')),
% 138.92/29.07 inference(cnf_transformation,[],[f779])).
% 138.92/29.07
% 138.92/29.07 tcf(c_110,plain,![X0_'A_c_prod_ell2':'A_c_prod_ell2$',X0_'A_c_prod_ell2_b_d_prod_ell2_cblinfun':'A_c_prod_ell2_b_d_prod_ell2_cblinfun$',X1_'A_c_prod_ell2_b_d_prod_ell2_cblinfun':'A_c_prod_ell2_b_d_prod_ell2_cblinfun$']:
% 138.92/29.07 ('plus$u'('fun_app$k'('fun_app$l'('cblinfun_apply$',X0_'A_c_prod_ell2_b_d_prod_ell2_cblinfun'),X0_'A_c_prod_ell2'),'fun_app$k'('fun_app$l'('cblinfun_apply$',X1_'A_c_prod_ell2_b_d_prod_ell2_cblinfun'),X0_'A_c_prod_ell2')) = 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b',X0_'A_c_prod_ell2_b_d_prod_ell2_cblinfun'),X1_'A_c_prod_ell2_b_d_prod_ell2_cblinfun')),X0_'A_c_prod_ell2')),
% 138.92/29.07 inference(cnf_transformation,[],[f790])).
% 138.92/29.07
% 138.92/29.07 tcf(c_395,plain,
% 138.92/29.07 ('fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b','tensor_op$'('a$','b2$')),'tensor_op$'('a$','b1$'))),'tensor_ell2$b'('ket$a'('i$'),'ket$b'('j$'))) != 'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'('a$','fun_app$m'('fun_app$n'('plus$a','b2$'),'b1$'))),'tensor_ell2$b'('ket$a'('i$'),'ket$b'('j$')))),
% 138.92/29.07 inference(demodulation,[status(thm)],[c_49,c_63,c_79,c_96])).
% 138.92/29.07
% 138.92/29.07 tcf(c_355795,plain,![X0_'C_ell2_d_ell2_cblinfun':'C_ell2_d_ell2_cblinfun$',X0_'D_ell2':'D_ell2$',X0_'C_ell2':'C_ell2$',X0_'A_ell2':'A_ell2$',X0_'A_ell2_b_ell2_cblinfun':'A_ell2_b_ell2_cblinfun$']:
% 138.92/29.07 ('plus$u'('fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'(X0_'A_ell2_b_ell2_cblinfun',X0_'C_ell2_d_ell2_cblinfun')),'tensor_ell2$b'(X0_'A_ell2',X0_'C_ell2')),'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X0_'A_ell2_b_ell2_cblinfun'),X0_'A_ell2'),X0_'D_ell2')) = 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X0_'A_ell2_b_ell2_cblinfun'),X0_'A_ell2'),'plus$i'('fun_app$u'('cblinfun_apply$b'(X0_'C_ell2_d_ell2_cblinfun'),X0_'C_ell2'),X0_'D_ell2'))),
% 138.92/29.07 inference(superposition,[status(thm)],[c_94,c_97])).
% 138.92/29.07
% 138.92/29.07 tcf(c_357848,plain,![X0_'C_ell2_d_ell2_cblinfun':'C_ell2_d_ell2_cblinfun$',X0_'C_ell2':'C_ell2$',X0_'A_ell2':'A_ell2$',X0_'A_ell2_b_ell2_cblinfun':'A_ell2_b_ell2_cblinfun$',X1_'C_ell2_d_ell2_cblinfun':'C_ell2_d_ell2_cblinfun$',X1_'C_ell2':'C_ell2$']:
% 138.92/29.07 ('plus$u'('fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'(X0_'A_ell2_b_ell2_cblinfun',X0_'C_ell2_d_ell2_cblinfun')),'tensor_ell2$b'(X0_'A_ell2',X0_'C_ell2')),'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'(X0_'A_ell2_b_ell2_cblinfun',X1_'C_ell2_d_ell2_cblinfun')),'tensor_ell2$b'(X0_'A_ell2',X1_'C_ell2'))) = 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X0_'A_ell2_b_ell2_cblinfun'),X0_'A_ell2'),'plus$i'('fun_app$u'('cblinfun_apply$b'(X0_'C_ell2_d_ell2_cblinfun'),X0_'C_ell2'),'fun_app$u'('cblinfun_apply$b'(X1_'C_ell2_d_ell2_cblinfun'),X1_'C_ell2')))),
% 138.92/29.07 inference(superposition,[status(thm)],[c_94,c_355795])).
% 138.92/29.07
% 138.92/29.07 tcf(c_392471,plain,![X0_'C_ell2_d_ell2_cblinfun':'C_ell2_d_ell2_cblinfun$',X0_'C_ell2':'C_ell2$',X0_'A_ell2':'A_ell2$',X0_'A_ell2_b_ell2_cblinfun':'A_ell2_b_ell2_cblinfun$',X1_'C_ell2_d_ell2_cblinfun':'C_ell2_d_ell2_cblinfun$']:
% 138.92/29.07 ('fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b','tensor_op$'(X0_'A_ell2_b_ell2_cblinfun',X0_'C_ell2_d_ell2_cblinfun')),'tensor_op$'(X0_'A_ell2_b_ell2_cblinfun',X1_'C_ell2_d_ell2_cblinfun'))),'tensor_ell2$b'(X0_'A_ell2',X0_'C_ell2')) = 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X0_'A_ell2_b_ell2_cblinfun'),X0_'A_ell2'),'plus$i'('fun_app$u'('cblinfun_apply$b'(X0_'C_ell2_d_ell2_cblinfun'),X0_'C_ell2'),'fun_app$u'('cblinfun_apply$b'(X1_'C_ell2_d_ell2_cblinfun'),X0_'C_ell2')))),
% 138.92/29.07 inference(superposition,[status(thm)],[c_357848,c_110])).
% 138.92/29.07
% 138.92/29.07 tcf(c_392472,plain,![X0_'C_ell2_d_ell2_cblinfun':'C_ell2_d_ell2_cblinfun$',X0_'C_ell2':'C_ell2$',X0_'A_ell2':'A_ell2$',X0_'A_ell2_b_ell2_cblinfun':'A_ell2_b_ell2_cblinfun$',X1_'C_ell2_d_ell2_cblinfun':'C_ell2_d_ell2_cblinfun$']:
% 138.92/29.07 ('fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b','tensor_op$'(X0_'A_ell2_b_ell2_cblinfun',X0_'C_ell2_d_ell2_cblinfun')),'tensor_op$'(X0_'A_ell2_b_ell2_cblinfun',X1_'C_ell2_d_ell2_cblinfun'))),'tensor_ell2$b'(X0_'A_ell2',X0_'C_ell2')) = 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X0_'A_ell2_b_ell2_cblinfun'),X0_'A_ell2'),'fun_app$u'('cblinfun_apply$b'('fun_app$m'('fun_app$n'('plus$a',X0_'C_ell2_d_ell2_cblinfun'),X1_'C_ell2_d_ell2_cblinfun')),X0_'C_ell2'))),
% 138.92/29.07 inference(light_normalisation,[status(thm)],[c_392471,c_103])).
% 138.92/29.07
% 138.92/29.07 tcf(c_392473,plain,
% 138.92/29.07 ('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$'))) != 'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'('a$','fun_app$m'('fun_app$n'('plus$a','b2$'),'b1$'))),'tensor_ell2$b'('ket$a'('i$'),'ket$b'('j$')))),
% 138.92/29.07 inference(demodulation,[status(thm)],[c_395,c_392472])).
% 138.92/29.07
% 138.92/29.07 tcf(c_392474,plain,
% 138.92/29.07 ($false),
% 138.92/29.07 inference(ground_joinability,[status(thm)],[c_392473,c_94])).
% 138.92/29.07
% 138.92/29.07
% 138.92/29.07 % SZS output end CNFRefutation for theBenchmark.p
% 138.92/29.07
% 138.92/29.07
%------------------------------------------------------------------------------