%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ITP384_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 : n002.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:31 PM UTC 2026
% Result : Theorem 4.95s 2.49s
% Output : CNFRefutation 4.95s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP384_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.58 % Computer : n002.cluster.edu
% 0.09/0.58 % Model : x86_64 x86_64
% 0.09/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.58 % Memory : 8046.5625MB
% 0.09/0.58 % OS : Linux 6.8.0-71-generic
% 0.09/0.58 % CPULimit : 300
% 0.09/0.58 % WCLimit : 300
% 0.09/0.58 % DateTime : Wed Sep 23 18:33:20 UTC 2026
% 0.09/0.59 % CPUTime :
% 0.09/0.59 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.62 Running first-order theorem proving
% 0.09/0.62 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.13/0.63
% 0.13/0.63 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.63
% 0.13/0.63 % Detected problem language: tptp
% 0.13/0.65 % Proving...
% 4.95/2.49 % SZS status Started for theBenchmark.p
% 4.95/2.49 % SZS status Theorem for theBenchmark.p
% 4.95/2.49
% 4.95/2.49 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.95/2.49
% 4.95/2.49 % ------ iProver source info
% 4.95/2.49
% 4.95/2.49 % git: date: 2026-07-19 20:42:38 +0200
% 4.95/2.49 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.95/2.49 % git: non_committed_changes: false
% 4.95/2.49
% 4.95/2.49 % ------ Parsing...
% 4.95/2.49 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 4.95/2.49 %
% 4.95/2.49
% 4.95/2.49 % ------ Preprocessing... sup_sim: 36 pe_s pe_e sup_sim: 0 pe_s pe_e %
% 4.95/2.49
% 4.95/2.49 % ------ Preprocessing...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 4.95/2.49 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
% 4.95/2.49 %
% 4.95/2.49
% 4.95/2.49 % ------ Preprocessing...
% 4.95/2.49 % ------ Proving...
% 4.95/2.49 % ------ Problem Properties
% 4.95/2.49
% 4.95/2.49 %
% 4.95/2.49 % clauses 139
% 4.95/2.49 % conjectures 0
% 4.95/2.49 % EPR 13
% 4.95/2.49 % Horn 139
% 4.95/2.49 % unary 44
% 4.95/2.49 % binary 85
% 4.95/2.49 % lits 252
% 4.95/2.49 % lits eq 178
% 4.95/2.49 % fd_pure 0
% 4.95/2.49 % fd_pseudo 0
% 4.95/2.49 % fd_cond 3
% 4.95/2.49 % fd_pseudo_cond 5
% 4.95/2.49 % AC symbols 0
% 4.95/2.49
% 4.95/2.49 % ------ Schedule dynamic 5 is on
% 4.95/2.49
% 4.95/2.49 % ------ no conjectures: strip conj schedule
% 4.95/2.49
% 4.95/2.49 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 4.95/2.49
% 4.95/2.49
% 4.95/2.49 % ------
% 4.95/2.49 % Current options:
% 4.95/2.49 % ------
% 4.95/2.49
% 4.95/2.49
% 4.95/2.49 %
% 4.95/2.49
% 4.95/2.49 % ------ Proving...
% 4.95/2.49 %
% 4.95/2.49
% 4.95/2.49 % SZS status Theorem for theBenchmark.p
% 4.95/2.49
% 4.95/2.49 % SZS output start CNFRefutation for theBenchmark.p
% 4.95/2.49
% 4.95/2.49 tff(func_def_0, type, 'fun_app$at': ('B_b_prod_update_a_update_fun$' * 'B_b_prod_update$') > 'A_update$').
% 4.95/2.49 tff(pred_def_1, type, 'inj_on$d': ('A_update_b_update_fun_a_update_a_update_fun_fun$' * 'A_update_b_update_fun_set$') > $o).
% 4.95/2.49 tff(pred_def_2, type, 'preregister$h': 'C_update_b_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_3, type, 'iso_tuple_surjective_proof_assist$a': ('B_update$' * 'B_update$' * 'B_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_4, type, 'rel_fun$au': ('A_update_c_update_fun_a_update_c_update_fun_bool_fun_fun$' * 'B_update_a_update_fun_b_update_c_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_bool_fun_fun$' * 'A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$' * 'A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_5, type, 'fun_app$bw': ('C_update_c_update_fun_bool_fun$' * 'C_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_6, type, 'less_eq$a': ('A_update_set$' * 'A_update_set$') > $o).
% 4.95/2.49 tff(pred_def_7, type, 'member$': ('A_update$' * 'A_update_set$') > $o).
% 4.95/2.49 tff(pred_def_8, type, 'compatible$m': ('C_update_c_update_fun$' * 'C_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_9, type, 'rel_fun$be': ('A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'C_update_a_update_fun_c_update_b_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$' * 'A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$' * 'A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_10, type, 'fun_app$ca': ('A_update_a_update_fun_bool_fun$' * 'A_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_11, type, 'rel_fun$z': ('A_update_c_update_fun_b_update_a_update_fun_bool_fun_fun$' * 'C_update_a_update_fun_c_update_c_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_bool_fun_fun$' * 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$' * 'B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_12, type, 'member$a': ('B_update$' * 'B_update_set$') > $o).
% 4.95/2.49 tff(pred_def_13, type, 'pred_fun$b': ('B_update_bool_fun$' * 'A_update_bool_fun$' * 'B_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_14, type, 'compatible$s': ('A_update_a_c_prod_update_fun$' * 'B_update_a_c_prod_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_15, type, 'type_definition$d': ('B_update_b_update_fun$' * 'B_update_b_update_fun$' * 'B_update_set$') > $o).
% 4.95/2.49 tff(pred_def_16, type, 'pred_fun$': ('A_update_bool_fun$' * 'B_update_bool_fun$' * 'A_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_17, type, 'rel_fun$ba': ('A_update_b_update_fun_a_update_c_update_fun_bool_fun_fun$' * 'C_update_a_update_fun_c_update_b_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_bool_fun_fun$' * 'A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$' * 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_18, type, 'fun_app$': ('A_update_b_update_fun_bool_fun$' * 'A_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_19, type, 'inj_on$c': ('A_update_c_update_fun$' * 'A_update_set$') > $o).
% 4.95/2.49 tff(pred_def_20, type, 'preregister$': 'C_update_c_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_21, type, 'compatible$w': ('B_update_a_c_prod_update_fun$' * 'A_update_a_c_prod_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_22, type, 'iso_register$d': 'C_update_c_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_23, type, 'quotient3$f': ('C_update_c_update_bool_fun_fun$' * 'C_update_a_update_fun$' * 'A_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_24, type, 'inj_on$m': ('B_update_b_update_fun$' * 'B_update_set$') > $o).
% 4.95/2.49 tff(pred_def_25, type, 'compatible$g': ('C_update_a_update_fun$' * 'B_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_26, type, 'quotient3$b': ('A_update_a_update_bool_fun_fun$' * 'A_update_a_update_fun$' * 'A_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_27, type, 'inj_on$h': ('B_update_a_update_fun_b_update_b_update_fun_fun$' * 'B_update_a_update_fun_set$') > $o).
% 4.95/2.49 tff(pred_def_28, type, 'rel_fun$bh': ('A_update_b_update_fun_a_update_c_update_fun_bool_fun_fun$' * 'B_update_a_update_fun_b_update_b_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_bool_fun_fun$' * 'A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$' * 'A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_29, type, 'type_definition$f': ('A_update_b_update_fun$' * 'B_update_a_update_fun$' * 'B_update_set$') > $o).
% 4.95/2.49 tff(pred_def_30, type, 'iso_tuple_update_accessor_cong_assist$b': ('A_update_a_update_fun_a_update_a_update_fun_fun$' * 'A_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_31, type, 'fun_app$k': ('B_update_bool_fun$' * 'B_update$') > $o).
% 4.95/2.49 tff(pred_def_32, type, 'rel_fun$o': ('B_update_a_update_fun_a_update_c_update_fun_bool_fun_fun$' * 'A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_bool_fun_fun$' * 'B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$' * 'A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_33, type, 'pred_fun$d': ('C_update_bool_fun$' * 'C_update_bool_fun$' * 'C_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_34, type, 'inj_on$j': ('C_update_c_update_fun$' * 'C_update_set$') > $o).
% 4.95/2.49 tff(pred_def_35, type, 'register$f': 'B_a_prod_update_a_c_prod_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_36, type, 'quotient3$d': ('A_update_a_update_bool_fun_fun$' * 'A_update_c_update_fun$' * 'C_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_37, type, 'compatible$v': ('A_update_c_a_prod_update_fun$' * 'B_update_c_a_prod_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_38, type, 'register$i': 'B_update_c_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_39, type, 'inj_on$e': ('C_update_a_update_fun_c_update_c_update_fun_fun$' * 'C_update_a_update_fun_set$') > $o).
% 4.95/2.49 tff(pred_def_40, type, 'iso_register$a': 'A_update_b_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_41, type, 'type_definition$c': ('C_update_b_update_fun$' * 'B_update_c_update_fun$' * 'B_update_set$') > $o).
% 4.95/2.49 tff(pred_def_42, type, 'inj_on$i': ('A_update_a_update_fun$' * 'A_update_set$') > $o).
% 4.95/2.49 tff(pred_def_43, type, 'rel_fun$j': ('B_update_a_update_fun_a_update_c_update_fun_bool_fun_fun$' * 'A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_bool_fun_fun$' * 'B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$' * 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_44, type, 'inj_on$a': ('C_update_a_update_fun$' * 'C_update_set$') > $o).
% 4.95/2.49 tff(pred_def_45, type, 'fun_app$a': ('C_update_a_update_fun_bool_fun$' * 'C_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_46, type, 'register$c': 'A_update_b_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_47, type, 'preregister$b': 'A_update_a_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_48, type, 'register$l': 'A_update_a_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_49, type, 'compatible$j': ('C_update_b_update_fun$' * 'B_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_50, type, 'quotient3$h': ('B_update_b_update_bool_fun_fun$' * 'B_update_c_update_fun$' * 'C_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_51, type, 'quotient3$c': ('B_update_b_update_bool_fun_fun$' * 'B_update_a_update_fun$' * 'A_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_52, type, 'rel_fun$br': ('A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'C_update_a_update_fun_c_update_b_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$' * 'A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$' * 'A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_53, type, 'rel_fun$ae': ('A_update_c_update_fun_a_update_c_update_fun_bool_fun_fun$' * 'C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_bool_fun_fun$' * 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$' * 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_54, type, 'member$b': ('C_update$' * 'C_update_set$') > $o).
% 4.95/2.49 tff(pred_def_55, type, 'rel_fun$bx': ('B_update_c_update_bool_fun_fun$' * 'B_update_c_update_bool_fun_fun$' * 'B_update_b_update_fun$' * 'C_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_56, type, 'fun_app$by': ('B_update_b_update_fun_bool_fun$' * 'B_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_57, type, 'rel_fun$an': ('A_update_c_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$' * 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$' * 'A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_58, type, 'iso_tuple_surjective_proof_assist$': ('C_update$' * 'C_update$' * 'C_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_59, type, 'inj_on$b': ('B_update_a_update_fun$' * 'B_update_set$') > $o).
% 4.95/2.49 tff(pred_def_60, type, 'pred_fun$c': ('A_update_bool_fun$' * 'A_update_bool_fun$' * 'A_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_61, type, 'quotient3$a': ('B_update_b_update_bool_fun_fun$' * 'B_update_b_update_fun$' * 'B_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_62, type, 'quotient3$g': ('C_update_c_update_bool_fun_fun$' * 'C_update_b_update_fun$' * 'B_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_63, type, 'compatible$e': ('A_update_b_update_fun$' * 'C_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_64, type, 'iso_register$e': 'B_update_c_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_65, type, 'rel_fun$ar': ('A_update_c_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$' * 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$' * 'A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_66, type, 'preregister$c': 'A_update_c_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_67, type, 'compatible$n': ('C_update_c_update_fun$' * 'B_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_68, type, 'iso_tuple_update_accessor_cong_assist$e': ('B_update_b_update_fun_c_update_c_update_fun_fun$' * 'C_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_69, type, 'type_definition$h': ('B_update_a_update_fun$' * 'A_update_b_update_fun$' * 'A_update_set$') > $o).
% 4.95/2.49 tff(pred_def_70, type, 'less_eq$': ('B_update_set$' * 'B_update_set$') > $o).
% 4.95/2.49 tff(pred_def_71, type, 'iso_register$b': 'A_update_c_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_72, type, 'register$': 'A_update_c_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_73, type, 'compatible$f': ('B_update_a_update_fun$' * 'A_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_74, type, 'rel_fun$e': ('B_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$' * 'A_update_b_update_fun_a_update_a_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_bool_fun_fun$' * 'B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$' * 'B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_75, type, 'bijection$a': 'B_update_b_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_76, type, 'register$b': 'C_update_a_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_77, type, 'compatible$h': ('C_update_a_update_fun$' * 'C_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_78, type, 'fun_app$m': ('A_update_bool_fun$' * 'A_update$') > $o).
% 4.95/2.49 tff(pred_def_79, type, 'rel_fun$aj': ('A_update_c_update_fun_a_update_c_update_fun_bool_fun_fun$' * 'C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_bool_fun_fun$' * 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$' * 'A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_80, type, 'compatible$u': ('B_update_a_a_prod_update_fun$' * 'B_update_a_a_prod_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_81, type, 'register$m': 'A_a_prod_update_c_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_82, type, 'type_definition$e': ('A_update_a_update_fun$' * 'A_update_a_update_fun$' * 'A_update_set$') > $o).
% 4.95/2.49 tff(pred_def_83, type, 'compatible$': ('B_update_a_update_fun$' * 'B_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_84, type, 'iso_register$h': 'A_update_a_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_85, type, 'iso_register$g': 'B_update_b_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_86, type, 'register$h': 'C_update_c_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_87, type, 'preregister$g': 'B_update_c_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_88, type, 'rel_fun$bu': ('A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'B_update_a_update_fun_b_update_b_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$' * 'A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$' * 'A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_89, type, 'rel_fun$by': ('B_update_a_update_bool_fun_fun$' * 'B_update_a_update_bool_fun_fun$' * 'B_update_b_update_fun$' * 'A_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_90, type, 'compatible$d': ('A_update_c_update_fun$' * 'C_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_91, type, 'compatible$k': ('B_update_b_update_fun$' * 'C_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_92, type, 'preregister$e': 'A_update_b_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_93, type, 'compatible$q': ('A_update_a_update_fun$' * 'A_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_94, type, 'register$d': 'A_a_prod_update_c_c_prod_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_95, type, 'fun_app$p': ('A_update_c_update_fun_bool_fun$' * 'A_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_96, type, 'compatible$p': ('B_update_c_update_fun$' * 'B_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_97, type, 'pred_fun$e': ('B_update_bool_fun$' * 'C_update_bool_fun$' * 'B_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_98, type, 'pred_fun$a': ('C_update_bool_fun$' * 'A_update_bool_fun$' * 'C_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_99, type, 'rel_fun$bk': ('A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'B_update_a_update_fun_b_update_b_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$' * 'A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$' * 'A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_100, type, 'rel_fun$s': ('B_update_a_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$' * 'B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$' * 'A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_101, type, 'iso_tuple_update_accessor_cong_assist$g': ('A_update_a_update_fun_c_update_c_update_fun_fun$' * 'C_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_102, type, 'rel_fun$bn': ('A_update_c_update_fun_a_update_c_update_fun_bool_fun_fun$' * 'B_update_a_update_fun_b_update_c_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_bool_fun_fun$' * 'A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$' * 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_103, type, 'bijection$': 'C_update_c_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_104, type, 'pred_fun$g': ('B_update_bool_fun$' * 'B_update_bool_fun$' * 'B_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_105, type, 'iso_tuple_update_accessor_cong_assist$d': ('C_update_c_update_fun_a_update_a_update_fun_fun$' * 'A_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_106, type, 'compatible$a': ('A_update_c_update_fun$' * 'A_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_107, type, 'register$a': 'B_update_a_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_108, type, 'iso_register$f': 'C_update_b_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_109, type, 'iso_register$c': 'B_update_a_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_110, type, 'iso_tuple_update_accessor_cong_assist$h': ('A_update_a_update_fun_b_update_b_update_fun_fun$' * 'B_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_111, type, 'type_definition$': ('C_update_c_update_fun$' * 'C_update_c_update_fun$' * 'C_update_set$') > $o).
% 4.95/2.49 tff(pred_def_112, type, 'preregister$f': 'C_update_a_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_113, type, 'compatible$o': ('B_update_c_update_fun$' * 'C_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_114, type, 'iso_tuple_update_accessor_cong_assist$c': ('C_update_c_update_fun_b_update_b_update_fun_fun$' * 'B_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_115, type, 'compatible$r': ('A_update_c_c_prod_update_fun$' * 'A_update_c_c_prod_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_116, type, 'register$n': 'B_b_prod_update_a_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_117, type, 'quotient3$e': ('A_update_a_update_bool_fun_fun$' * 'A_update_b_update_fun$' * 'B_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_118, type, 'bijection$b': 'A_update_a_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_119, type, 'pred_fun$f': ('C_update_bool_fun$' * 'B_update_bool_fun$' * 'C_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_120, type, 'register$e': 'A_b_prod_update_c_a_prod_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_121, type, 'compatible$l': ('B_update_b_update_fun$' * 'B_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_122, type, 'inj_on$': ('A_update_b_update_fun$' * 'A_update_set$') > $o).
% 4.95/2.49 tff(pred_def_123, type, 'iso_tuple_update_accessor_cong_assist$a': ('B_update_b_update_fun_b_update_b_update_fun_fun$' * 'B_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_124, type, 'compatible$i': ('C_update_b_update_fun$' * 'C_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_125, type, 'compatible$b': ('A_update_b_update_fun$' * 'A_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_126, type, 'type_definition$g': ('C_update_a_update_fun$' * 'A_update_c_update_fun$' * 'A_update_set$') > $o).
% 4.95/2.49 tff(pred_def_127, type, 'compatible$t': ('B_update_c_a_prod_update_fun$' * 'A_update_c_a_prod_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_128, type, 'rel_fun$w': ('B_update_a_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$' * 'B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$' * 'A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_129, type, 'rel_fun$ax': ('A_update_c_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'B_update_a_update_fun_b_update_c_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$' * 'A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$' * 'A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$') > $o).
% 4.95/2.49 tff(pred_def_130, type, 'compatible$c': ('B_update_a_update_fun$' * 'C_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_131, type, 'iso_tuple_update_accessor_cong_assist$f': ('B_update_b_update_fun_a_update_a_update_fun_fun$' * 'A_update_b_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_132, type, 'inj_on$l': ('C_update_b_update_fun$' * 'C_update_set$') > $o).
% 4.95/2.49 tff(pred_def_133, type, 'type_definition$b': ('A_update_c_update_fun$' * 'C_update_a_update_fun$' * 'C_update_set$') > $o).
% 4.95/2.49 tff(pred_def_134, type, 'iso_tuple_update_accessor_cong_assist$': ('C_update_c_update_fun_c_update_c_update_fun_fun$' * 'C_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_135, type, 'fun_app$i': ('C_update_bool_fun$' * 'C_update$') > $o).
% 4.95/2.49 tff(pred_def_136, type, 'register$k': 'B_update_b_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_137, type, 'register$j': 'C_update_b_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_138, type, 'iso_tuple_surjective_proof_assist$b': ('A_update$' * 'A_update$' * 'A_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_139, type, 'type_definition$a': ('B_update_c_update_fun$' * 'C_update_b_update_fun$' * 'C_update_set$') > $o).
% 4.95/2.49 tff(pred_def_140, type, 'iso_register$': 'C_update_a_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_141, type, 'preregister$a': 'B_update_b_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_142, type, 'preregister$d': 'B_update_a_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_143, type, 'register$g': 'B_b_prod_update_a_a_prod_update_fun$' > $o).
% 4.95/2.49 tff(pred_def_144, type, 'fun_app$b': ('B_update_a_update_fun_bool_fun$' * 'B_update_a_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_145, type, 'inj_on$g': ('C_update_a_update_fun_c_update_b_update_fun_fun$' * 'C_update_a_update_fun_set$') > $o).
% 4.95/2.49 tff(pred_def_146, type, 'quotient3$': ('C_update_c_update_bool_fun_fun$' * 'C_update_c_update_fun$' * 'C_update_c_update_fun$') > $o).
% 4.95/2.49 tff(pred_def_147, type, 'inj_on$f': ('B_update_a_update_fun_b_update_c_update_fun_fun$' * 'B_update_a_update_fun_set$') > $o).
% 4.95/2.49 tff(pred_def_148, type, 'inj_on$k': ('B_update_c_update_fun$' * 'B_update_set$') > $o).
% 4.95/2.49 tff(func_def_149, type, 'fun_app$h': ('A_update_c_a_prod_update_fun$' * 'A_update$') > 'C_a_prod_update$').
% 4.95/2.49 tff(func_def_150, type, 'fun_app$bk': ('C_update_b_update_fun_c_update_c_update_fun_fun$' * 'C_update_b_update_fun$') > 'C_update_c_update_fun$').
% 4.95/2.49 tff(func_def_151, type, 'fun_app$u': ('A_update_b_update_fun$' * 'A_update$') > 'B_update$').
% 4.95/2.49 tff(func_def_152, type, 'rel_fun$bd': ('C_update_c_update_bool_fun_fun$' * 'B_update_c_update_bool_fun_fun$') > 'C_update_b_update_fun_c_update_c_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_153, type, 'id$d': 'C_b_prod_update_c_b_prod_update_fun$').
% 4.95/2.49 tff(func_def_154, type, 'grp$a': ('B_update_set$' * 'B_update_b_update_fun$') > 'B_update_b_update_bool_fun_fun$').
% 4.95/2.49 tff(func_def_155, type, 'rel_fun$a': ('C_update_c_update_bool_fun_fun$' * 'A_update_c_update_bool_fun_fun$') > 'C_update_a_update_fun_c_update_c_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_156, type, 'map_fun$aq': ('B_update_c_update_fun$' * 'C_update_c_update_fun$') > 'C_update_c_update_fun_b_update_c_update_fun_fun$').
% 4.95/2.49 tff(func_def_157, type, 'rel_fun$at': ('C_update_b_update_bool_fun_fun$' * 'C_update_b_update_bool_fun_fun$') > 'C_update_c_update_fun_b_update_b_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_158, type, 'comp_update$': 'C_update$' > 'C_update_c_update_fun$').
% 4.95/2.49 tff(func_def_159, type, 'pred_DEADID$': 'C_update_bool_fun$').
% 4.95/2.49 tff(func_def_160, type, 'rel_fun$q': ('A_update_b_update_bool_fun_fun$' * 'B_update_a_update_bool_fun_fun$') > 'A_update_b_update_fun_b_update_a_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_161, type, 'rel_fun$ao': ('A_update_a_update_bool_fun_fun$' * 'C_update_b_update_bool_fun_fun$') > 'A_update_c_update_fun_a_update_b_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_162, type, 'comp$a': 'A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_163, type, 'rel_fun$ab': ('C_update_a_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'C_update_c_update_fun_a_update_a_update_fun_bool_fun_fun$') > 'C_update_a_update_fun_c_update_c_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_164, type, 'comp$bi': ('A_update_b_update_fun_c_update_a_update_fun_fun$' * 'C_update_a_update_fun_a_update_b_update_fun_fun$') > 'C_update_a_update_fun_c_update_a_update_fun_fun$').
% 4.95/2.49 tff(func_def_165, type, 'register_tensor$n': ('C_update_a_update_fun$' * 'C_update_a_update_fun$') > 'C_c_prod_update_a_a_prod_update_fun$').
% 4.95/2.49 tff(func_def_166, type, 'map_fun$aa': ('A_update_c_update_fun_b_update_a_update_fun_fun$' * 'A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$' * 'B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$') > 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_167, type, 'comp$ap': ('A_c_prod_update_b_update_fun$' * 'C_a_prod_update_a_c_prod_update_fun$') > 'C_a_prod_update_b_update_fun$').
% 4.95/2.49 tff(func_def_168, type, 'uuk$': 'A_update_bool_fun$').
% 4.95/2.49 tff(func_def_169, type, 'uue$': 'A_update_c_update_fun$' > 'A_update_a_c_prod_update_fun$').
% 4.95/2.49 tff(func_def_170, type, 'rel_fun$aw': ('B_update_b_update_bool_fun_fun$' * 'C_update_c_update_bool_fun_fun$') > 'B_update_c_update_fun_b_update_c_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_171, type, 'the_inv_into$g': ('C_update_set$' * 'C_update_b_update_fun$') > 'B_update_c_update_fun$').
% 4.95/2.49 tff(func_def_172, type, 'comp$ah': ('C_update_c_update_fun$' * 'A_update_c_update_fun$') > 'A_update_c_update_fun$').
% 4.95/2.49 tff(func_def_173, type, 'map_fun$af': ('A_update_b_update_fun_b_update_a_update_fun_fun$' * 'A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$' * 'B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$') > 'A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_174, type, 'uum$': 'C_update_bool_fun$').
% 4.95/2.49 tff(func_def_175, type, 'rel_fun$x': ('A_update_b_update_fun_b_update_a_update_fun_bool_fun_fun$' * 'A_update_a_update_fun_b_update_b_update_fun_bool_fun_fun$') > 'A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_176, type, 'rel_fun$d': ('B_update_b_update_bool_fun_fun$' * 'A_update_b_update_bool_fun_fun$') > 'B_update_a_update_fun_b_update_b_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_177, type, 'comp$d': 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_178, type, 'the_inv_into$b': ('A_update_set$' * 'A_update_b_update_fun$') > 'B_update_a_update_fun$').
% 4.95/2.49 tff(func_def_179, type, 'fun_app$as': ('A_a_prod_update_c_update_fun$' * 'A_a_prod_update$') > 'C_update$').
% 4.95/2.49 tff(func_def_180, type, 'uuv$': ('B_update_set$' * 'B_update_a_update_fun$' * 'B_update$') > 'A_update_b_update_fun$').
% 4.95/2.49 tff(func_def_181, type, 'map_fun$i': ('A_update_a_update_fun$' * 'C_update_b_update_fun$') > 'A_update_c_update_fun_a_update_b_update_fun_fun$').
% 4.95/2.49 tff(func_def_182, type, 'fun_app$aq': ('B_a_prod_update_a_c_prod_update_fun$' * 'B_a_prod_update$') > 'A_c_prod_update$').
% 4.95/2.49 tff(func_def_183, type, 'fun_app$d': ('B_update_a_update_fun$' * 'B_update$') > 'A_update$').
% 4.95/2.49 tff(func_def_184, type, 'comp$bn': ('A_update_bool_fun$' * 'B_update_a_update_fun$') > 'B_update_bool_fun$').
% 4.95/2.49 tff(func_def_185, type, 'id$m': 'B_update_b_update_fun_b_update_b_update_fun_fun$').
% 4.95/2.49 tff(func_def_186, type, 'inv_into$b': ('A_update_set$' * 'A_update_b_update_fun$') > 'B_update_a_update_fun$').
% 4.95/2.49 tff(func_def_187, type, 'register_tensor$k': ('B_update_a_update_fun$' * 'A_update_c_update_fun$') > 'B_a_prod_update_a_c_prod_update_fun$').
% 4.95/2.49 tff(func_def_188, type, 'fun_app$ao': ('A_a_prod_update_c_c_prod_update_fun$' * 'A_a_prod_update$') > 'C_c_prod_update$').
% 4.95/2.49 tff(func_def_189, type, 'register_tensor$d': ('B_update_b_update_fun$' * 'B_update_b_update_fun$') > 'B_b_prod_update_b_b_prod_update_fun$').
% 4.95/2.49 tff(func_def_190, type, 'id$j': 'A_b_prod_update_a_b_prod_update_fun$').
% 4.95/2.49 tff(func_def_191, type, 'register_pair$f': ('B_update_a_update_fun$' * 'C_update_a_update_fun$') > 'B_c_prod_update_a_update_fun$').
% 4.95/2.49 tff(func_def_192, type, 'map_fun$al': ('A_update_c_update_fun_a_update_c_update_fun_fun$' * 'C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$' * 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$') > 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_193, type, 'map_fun$ak': ('A_update_b_update_fun_c_update_a_update_fun_fun$' * 'C_update_c_update_fun_a_update_a_update_fun_fun$') > 'C_update_a_update_fun_c_update_c_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_194, type, 'comp$aj': ('B_update_c_update_fun$' * 'A_update_b_update_fun$') > 'A_update_c_update_fun$').
% 4.95/2.49 tff(func_def_195, type, 'uux$': 'A_update_set$' > 'C_update_a_update_fun_bool_fun$').
% 4.95/2.49 tff(func_def_196, type, 'id$g': 'B_b_prod_update_b_b_prod_update_fun$').
% 4.95/2.49 tff(func_def_197, type, 'map_fun$aw': ('C_update_b_update_fun$' * 'B_update_c_update_fun$') > 'B_update_b_update_fun_c_update_c_update_fun_fun$').
% 4.95/2.49 tff(func_def_198, type, 'comp$bb': ('A_update_c_update_fun$' * 'B_b_prod_update_a_update_fun$') > 'B_b_prod_update_c_update_fun$').
% 4.95/2.49 tff(func_def_199, type, 'rel_fun$az': ('B_update_b_update_bool_fun_fun$' * 'C_update_b_update_bool_fun_fun$') > 'B_update_c_update_fun_b_update_b_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_200, type, 'map_fun$u': ('C_update_c_update_fun$' * 'B_update_b_update_fun$') > 'C_update_b_update_fun_c_update_b_update_fun_fun$').
% 4.95/2.49 tff(func_def_201, type, 'top$c': 'A_update_b_update_fun_set$').
% 4.95/2.49 tff(func_def_202, type, 'fun_app$s': ('B_update_c_a_prod_update_fun$' * 'B_update$') > 'C_a_prod_update$').
% 4.95/2.49 tff(func_def_203, type, 'rel_fun$bw': ('B_update_c_update_bool_fun_fun$' * 'B_update_b_update_bool_fun_fun$') > 'B_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_204, type, 'fun_app$x': ('C_update_a_update_fun_c_update_b_update_fun_fun$' * 'C_update_a_update_fun$') > 'C_update_b_update_fun$').
% 4.95/2.49 tff(func_def_205, type, 'map_fun$ab': ('C_update_a_update_fun_a_update_b_update_fun_fun$' * 'A_update_a_update_fun_c_update_c_update_fun_fun$') > 'A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_206, type, 'fun_app$q': ('A_update_c_update_fun_a_update_c_update_fun_bool_fun_fun$' * 'A_update_c_update_fun$') > 'A_update_c_update_fun_bool_fun$').
% 4.95/2.49 tff(func_def_207, type, 'rel_fun$ap': ('C_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$' * 'C_update_c_update_fun_c_update_b_update_fun_bool_fun_fun$') > 'C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_208, type, 'comp$bd': ('B_update_b_update_fun_a_update_a_update_fun_fun$' * 'A_update_a_update_fun_b_update_b_update_fun_fun$') > 'A_update_a_update_fun_a_update_a_update_fun_fun$').
% 4.95/2.49 tff(func_def_209, type, 'comp$i': ('B_update_b_update_fun$' * 'C_update_b_update_fun$') > 'C_update_b_update_fun$').
% 4.95/2.49 tff(func_def_210, type, 'fun_app$bt': ('C_update_set_c_update_fun$' * 'C_update_set$') > 'C_update$').
% 4.95/2.49 tff(func_def_211, type, 'id$': 'C_update_c_update_fun$').
% 4.95/2.49 tff(func_def_212, type, 'comp$s': ('A_a_prod_update_b_c_prod_update_fun$' * 'B_b_prod_update_a_a_prod_update_fun$') > 'B_b_prod_update_b_c_prod_update_fun$').
% 4.95/2.49 tff(func_def_213, type, 'uul$': ('B_update_a_update_fun$' * 'B_update_a_update_fun$') > 'B_update_bool_fun$').
% 4.95/2.49 tff(func_def_214, type, 'rel_fun$g': ('A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'A_update_a_update_fun_a_update_a_update_fun_bool_fun_fun$') > 'A_update_b_update_fun_a_update_a_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_215, type, 'relcompp$a': ('C_update_c_update_bool_fun_fun$' * 'C_update_c_update_bool_fun_fun$') > 'C_update_c_update_bool_fun_fun$').
% 4.95/2.49 tff(func_def_216, type, 'fun_app$bu': ('B_update_set_b_update_fun$' * 'B_update_set$') > 'B_update$').
% 4.95/2.49 tff(func_def_217, type, 'grp$': ('C_update_set$' * 'C_update_c_update_fun$') > 'C_update_c_update_bool_fun_fun$').
% 4.95/2.49 tff(func_def_218, type, 'id$a': 'B_update_b_update_fun$').
% 4.95/2.49 tff(func_def_219, type, 'rel_fun$c': ('C_update_c_update_bool_fun_fun$' * 'A_update_b_update_bool_fun_fun$') > 'C_update_a_update_fun_c_update_b_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_220, type, 'image$d': 'C_update_c_update_fun$' > 'C_update_set_c_update_set_fun$').
% 4.95/2.49 tff(func_def_221, type, 'register_tensor$o': ('C_update_b_update_fun$' * 'C_update_b_update_fun$') > 'C_c_prod_update_b_b_prod_update_fun$').
% 4.95/2.49 tff(func_def_222, type, 'comp$ay': ('A_update_c_update_fun$' * 'C_c_prod_update_a_update_fun$') > 'C_c_prod_update_c_update_fun$').
% 4.95/2.49 tff(func_def_223, type, 'rel_fun$ag': ('C_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$' * 'C_update_c_update_fun_c_update_c_update_fun_bool_fun_fun$') > 'C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_224, type, 'image$a': ('C_update_a_update_fun$' * 'C_update_set$') > 'A_update_set$').
% 4.95/2.49 tff(func_def_225, type, 'map_fun$ae': ('B_update_a_update_fun$' * 'A_update_c_update_fun$') > 'A_update_a_update_fun_b_update_c_update_fun_fun$').
% 4.95/2.49 tff(func_def_226, type, 'the_inv_into$f': ('B_update_set$' * 'B_update_c_update_fun$') > 'C_update_b_update_fun$').
% 4.95/2.49 tff(func_def_227, type, 'fun_app$ap': ('A_b_prod_update_c_a_prod_update_fun$' * 'A_b_prod_update$') > 'C_a_prod_update$').
% 4.95/2.49 tff(func_def_228, type, 'rel_fun$p': ('A_update_b_update_fun_b_update_a_update_fun_bool_fun_fun$' * 'A_update_a_update_fun_b_update_c_update_fun_bool_fun_fun$') > 'A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_229, type, 'rel_fun$t': ('B_update_a_update_bool_fun_fun$' * 'A_update_b_update_bool_fun_fun$') > 'B_update_a_update_fun_a_update_b_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_230, type, 'comp$am': ('A_a_prod_update_b_update_fun$' * 'C_c_prod_update_a_a_prod_update_fun$') > 'C_c_prod_update_b_update_fun$').
% 4.95/2.49 tff(func_def_231, type, 'tensor_update$e': ('B_update$' * 'A_update$') > 'B_a_prod_update$').
% 4.95/2.49 tff(func_def_232, type, 'rel_fun$bq': ('B_update_c_update_bool_fun_fun$' * 'C_update_c_update_bool_fun_fun$') > 'B_update_c_update_fun_c_update_c_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_233, type, 'register_pair$q': ('B_update_b_update_fun$' * 'C_update_b_update_fun$') > 'B_c_prod_update_b_update_fun$').
% 4.95/2.49 tff(func_def_234, type, 'fun_app$v': ('B_update_a_update_fun_b_update_c_update_fun_fun$' * 'B_update_a_update_fun$') > 'B_update_c_update_fun$').
% 4.95/2.49 tff(func_def_235, type, 'uuf$': 'B_update_a_update_fun$' > 'B_update_a_c_prod_update_fun$').
% 4.95/2.49 tff(func_def_236, type, 'rel_fun$ac': ('C_update_a_update_bool_fun_fun$' * 'A_update_b_update_bool_fun_fun$') > 'C_update_a_update_fun_a_update_b_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_237, type, 'fun_app$an': ('B_update_b_update_fun_b_update_b_update_fun_fun$' * 'B_update_b_update_fun$') > 'B_update_b_update_fun$').
% 4.95/2.49 tff(func_def_238, type, 'comp_update$a': 'A_update$' > 'A_update_a_update_fun$').
% 4.95/2.49 tff(func_def_239, type, 'rel_fun$l': ('A_update_b_update_fun_c_update_a_update_fun_bool_fun_fun$' * 'A_update_a_update_fun_c_update_c_update_fun_bool_fun_fun$') > 'A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_240, type, 'comp$bo': ('C_update_bool_fun$' * 'A_update_c_update_fun$') > 'A_update_bool_fun$').
% 4.95/2.49 tff(func_def_241, type, 'uuo$': 'B_update_bool_fun$').
% 4.95/2.49 tff(func_def_242, type, 'register_tensor$r': ('B_update_a_update_fun$' * 'C_update_a_update_fun$') > 'B_c_prod_update_a_a_prod_update_fun$').
% 4.95/2.49 tff(func_def_243, type, 'inv_into$e': 'B_update_set$' > 'B_update_b_update_fun_b_update_b_update_fun_fun$').
% 4.95/2.49 tff(func_def_244, type, 'id$r': 'B_update_a_update_fun_b_update_a_update_fun_fun$').
% 4.95/2.49 tff(func_def_245, type, 'rel_fun$v': ('A_update_c_update_bool_fun_fun$' * 'A_update_b_update_bool_fun_fun$') > 'A_update_a_update_fun_c_update_b_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_246, type, 'register_tensor$l': ('B_update_a_update_fun$' * 'B_update_a_update_fun$') > 'B_b_prod_update_a_a_prod_update_fun$').
% 4.95/2.49 tff(func_def_247, type, 'register_tensor$h': ('A_update_a_update_fun$' * 'A_update_a_update_fun$') > 'A_a_prod_update_a_a_prod_update_fun$').
% 4.95/2.49 tff(func_def_248, type, 'top$a': 'C_update_set$').
% 4.95/2.49 tff(func_def_249, type, 'fun_app$bh': ('A_update_a_update_fun_c_update_c_update_fun_fun$' * 'A_update_a_update_fun$') > 'C_update_c_update_fun$').
% 4.95/2.49 tff(func_def_250, type, 'uub$': 'B_update$' > 'A_update_b_update_fun$').
% 4.95/2.49 tff(func_def_251, type, 'register_pair$b': ('A_update_c_update_fun$' * 'A_update_c_update_fun$') > 'A_a_prod_update_c_update_fun$').
% 4.95/2.49 tff(func_def_252, type, 'register_pair$g': ('A_update_c_update_fun$' * 'C_update_c_update_fun$') > 'A_c_prod_update_c_update_fun$').
% 4.95/2.49 tff(func_def_253, type, 'map_fun$p': ('C_update_c_update_fun$' * 'C_update_c_update_fun$') > 'C_update_c_update_fun_c_update_c_update_fun_fun$').
% 4.95/2.49 tff(func_def_254, type, 'fun_app$ad': ('B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$' * 'B_update_a_update_fun$') > 'A_update_b_update_fun_a_update_a_update_fun_fun$').
% 4.95/2.49 tff(func_def_255, type, 'register_tensor$e': ('B_update_b_update_fun$' * 'A_update_a_update_fun$') > 'B_a_prod_update_b_a_prod_update_fun$').
% 4.95/2.49 tff(func_def_256, type, 'fun_app$ac': ('A_update_b_update_fun_a_update_a_update_fun_fun$' * 'A_update_b_update_fun$') > 'A_update_a_update_fun$').
% 4.95/2.49 tff(func_def_257, type, 'rel_fun$ah': ('C_update_c_update_bool_fun_fun$' * 'A_update_a_update_bool_fun_fun$') > 'C_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_258, type, 'register_pair$j': ('C_update_b_update_fun$' * 'A_update_b_update_fun$') > 'C_a_prod_update_b_update_fun$').
% 4.95/2.49 tff(func_def_259, type, 'relcompp$b': ('B_update_b_update_bool_fun_fun$' * 'B_update_b_update_bool_fun_fun$') > 'B_update_b_update_bool_fun_fun$').
% 4.95/2.49 tff(func_def_260, type, 'map_fun$m': ('C_update_c_update_fun$' * 'A_update_a_update_fun$') > 'C_update_a_update_fun_c_update_a_update_fun_fun$').
% 4.95/2.49 tff(func_def_261, type, 'fcomp$a': ('C_update_a_update_fun$' * 'A_update_c_update_fun$') > 'C_update_c_update_fun$').
% 4.95/2.49 tff(func_def_262, type, 'register_tensor$ac': ('A_update_c_update_fun$' * 'A_update_b_update_fun$') > 'A_a_prod_update_c_b_prod_update_fun$').
% 4.95/2.49 tff(func_def_263, type, 'image$h': ('C_update_b_update_fun$' * 'C_update_set$') > 'B_update_set$').
% 4.95/2.49 tff(func_def_264, type, 'uup$': ('A_update_b_update_fun$' * 'A_update_b_update_fun$') > 'A_update_bool_fun$').
% 4.95/2.49 tff(func_def_265, type, 'comp$f': 'A_update_a_update_fun$' > 'A_update_a_update_fun_a_update_a_update_fun_fun$').
% 4.95/2.49 tff(func_def_266, type, 'comp$ao': ('A_c_prod_update_c_update_fun$' * 'C_a_prod_update_a_c_prod_update_fun$') > 'C_a_prod_update_c_update_fun$').
% 4.95/2.49 tff(func_def_267, type, 'rel_fun$bo': ('B_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$' * 'B_update_c_update_fun_c_update_c_update_fun_bool_fun_fun$') > 'B_update_a_update_fun_b_update_c_update_fun_fun_c_update_a_update_fun_c_update_c_update_fun_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_268, type, 'map_fun$ag': ('C_update_a_update_fun_a_update_b_update_fun_fun$' * 'A_update_a_update_fun_c_update_b_update_fun_fun$') > 'A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_269, type, 'map_fun$j': ('A_update_a_update_fun$' * 'B_update_b_update_fun$') > 'A_update_b_update_fun_a_update_b_update_fun_fun$').
% 4.95/2.49 tff(func_def_270, type, 'comp$au': ('A_update_b_update_fun$' * 'C_c_prod_update_a_update_fun$') > 'C_c_prod_update_b_update_fun$').
% 4.95/2.49 tff(func_def_271, type, 'comp$ak': ('B_b_prod_update_a_update_fun$' * 'A_a_prod_update_b_b_prod_update_fun$') > 'A_a_prod_update_a_update_fun$').
% 4.95/2.49 tff(func_def_272, type, 'rel_fun$ak': ('C_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$' * 'C_update_c_update_fun_b_update_c_update_fun_bool_fun_fun$') > 'C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_273, type, 'comp$h': ('C_update_c_update_fun$' * 'B_update_c_update_fun$') > 'B_update_c_update_fun$').
% 4.95/2.49 tff(func_def_274, type, 'fun_app$al': ('A_update_a_update_fun_a_update_a_update_fun_fun$' * 'A_update_a_update_fun$') > 'A_update_a_update_fun$').
% 4.95/2.49 tff(func_def_275, type, 'id$w': 'A_update_set_a_update_set_fun$').
% 4.95/2.49 tff(func_def_276, type, 'register_pair$': ('B_update_a_update_fun$' * 'B_update_a_update_fun$') > 'B_b_prod_update_a_update_fun$').
% 4.95/2.49 tff(func_def_277, type, 'register_tensor$p': ('C_update_a_update_fun$' * 'B_update_a_update_fun$') > 'C_b_prod_update_a_a_prod_update_fun$').
% 4.95/2.49 tff(func_def_278, type, 'vimage$b': 'A_update_a_update_fun$' > 'A_update_set_a_update_set_fun$').
% 4.95/2.49 tff(func_def_279, type, 'id$s': 'A_update_c_update_fun_a_update_c_update_fun_fun$').
% 4.95/2.49 tff(func_def_280, type, 'rel_fun$as': ('C_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$' * 'C_update_c_update_fun_b_update_b_update_fun_bool_fun_fun$') > 'C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_281, type, 'fun_app$bq': ('A_update_set_a_update_set_fun$' * 'A_update_set$') > 'A_update_set$').
% 4.95/2.49 tff(func_def_282, type, 'conversep$a': 'B_update_b_update_bool_fun_fun$' > 'B_update_b_update_bool_fun_fun$').
% 4.95/2.49 tff(func_def_283, type, 'register_pair$n': ('C_update_b_update_fun$' * 'B_update_b_update_fun$') > 'C_b_prod_update_b_update_fun$').
% 4.95/2.49 tff(func_def_284, type, 'uud$': 'A_update_c_update_fun$' > 'A_update_c_c_prod_update_fun$').
% 4.95/2.49 tff(func_def_285, type, 'rel_fun$bg': ('C_update_c_update_bool_fun_fun$' * 'B_update_b_update_bool_fun_fun$') > 'C_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_286, type, 'register_pair$h': ('C_update_c_update_fun$' * 'A_update_c_update_fun$') > 'C_a_prod_update_c_update_fun$').
% 4.95/2.49 tff(func_def_287, type, 'fcomp$b': ('B_update_a_update_fun$' * 'A_update_c_update_fun$') > 'B_update_c_update_fun$').
% 4.95/2.49 tff(func_def_288, type, 'register_tensor$q': ('C_update_b_update_fun$' * 'B_update_b_update_fun$') > 'C_b_prod_update_b_b_prod_update_fun$').
% 4.95/2.49 tff(func_def_289, type, 'comp$ag': ('C_update_b_update_fun$' * 'C_update_c_update_fun$') > 'C_update_b_update_fun$').
% 4.95/2.49 tff(func_def_290, type, 'map_fun$ao': ('B_update_a_update_fun_c_update_a_update_fun_fun$' * 'C_update_c_update_fun_b_update_c_update_fun_fun$') > 'C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_291, type, 'comp$': ('B_update_c_update_fun$' * 'C_update_b_update_fun$') > 'C_update_c_update_fun$').
% 4.95/2.49 tff(func_def_292, type, 'image$b': ('B_update_a_update_fun$' * 'B_update_set$') > 'A_update_set$').
% 4.95/2.49 tff(func_def_293, type, 'comp_update$b': 'B_update$' > 'B_update_b_update_fun$').
% 4.95/2.49 tff(func_def_294, type, 'comp$bf': ('B_update_a_update_fun_a_update_c_update_fun_fun$' * 'A_update_b_update_fun_b_update_a_update_fun_fun$') > 'A_update_b_update_fun_a_update_c_update_fun_fun$').
% 4.95/2.49 tff(func_def_295, type, 'map_fun$an': ('A_update_c_update_fun_a_update_c_update_fun_fun$' * 'C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$' * 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$') > 'A_update_c_update_fun_b_update_a_update_fun_b_update_c_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_296, type, 'fun_app$c': ('B_update_a_c_prod_update_fun$' * 'B_update$') > 'A_c_prod_update$').
% 4.95/2.49 tff(func_def_297, type, 'comp$l': ('A_a_prod_update_b_b_prod_update_fun$' * 'C_c_prod_update_a_a_prod_update_fun$') > 'C_c_prod_update_b_b_prod_update_fun$').
% 4.95/2.49 tff(func_def_298, type, 'collect$b': 'B_update_a_update_fun_bool_fun$' > 'B_update_a_update_fun_set$').
% 4.95/2.49 tff(func_def_299, type, 'register_tensor$u': ('C_update_b_update_fun$' * 'C_update_c_update_fun$') > 'C_c_prod_update_b_c_prod_update_fun$').
% 4.95/2.49 tff(func_def_300, type, 'rel_fun$f': ('B_update_b_update_bool_fun_fun$' * 'A_update_a_update_bool_fun_fun$') > 'B_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_301, type, 'fun_app$bg': ('C_update_a_update_fun_c_update_a_update_fun_fun$' * 'C_update_a_update_fun$') > 'C_update_a_update_fun$').
% 4.95/2.49 tff(func_def_302, type, 'uut$': ('A_update_set$' * 'A_update_b_update_fun$' * 'A_update$') > 'B_update_a_update_fun$').
% 4.95/2.49 tff(func_def_303, type, 'comp$g': 'C_update_c_update_fun$' > 'C_update_c_update_fun_c_update_c_update_fun_fun$').
% 4.95/2.49 tff(func_def_304, type, 'comp$x': ('B_update_b_update_fun$' * 'A_update_b_update_fun$') > 'A_update_b_update_fun$').
% 4.95/2.49 tff(func_def_305, type, 'register_pair$o': ('C_update_a_update_fun$' * 'B_update_a_update_fun$') > 'C_b_prod_update_a_update_fun$').
% 4.95/2.49 tff(func_def_306, type, 'top$': 'A_update_set$').
% 4.95/2.49 tff(func_def_307, type, 'comp$r': ('A_a_prod_update_b_c_prod_update_fun$' * 'B_c_prod_update_a_a_prod_update_fun$') > 'B_c_prod_update_b_c_prod_update_fun$').
% 4.95/2.49 tff(func_def_308, type, 'register_pair$m': ('C_update_c_update_fun$' * 'B_update_c_update_fun$') > 'C_b_prod_update_c_update_fun$').
% 4.95/2.49 tff(func_def_309, type, 'map_fun$n': ('C_update_a_update_fun$' * 'A_update_c_update_fun$') > 'A_update_a_update_fun_c_update_c_update_fun_fun$').
% 4.95/2.49 tff(func_def_310, type, 'rel_fun$u': ('A_update_b_update_fun_c_update_a_update_fun_bool_fun_fun$' * 'A_update_a_update_fun_c_update_b_update_fun_bool_fun_fun$') > 'A_update_b_update_fun_a_update_a_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_311, type, 'the_inv_into$a': ('B_update_set$' * 'B_update_a_update_fun$') > 'A_update_b_update_fun$').
% 4.95/2.49 tff(func_def_312, type, 'register_pair$d': ('A_update_b_update_fun$' * 'A_update_b_update_fun$') > 'A_a_prod_update_b_update_fun$').
% 4.95/2.49 tff(func_def_313, type, 'map_fun$ai': ('B_update_a_update_fun_a_update_b_update_fun_fun$' * 'A_update_a_update_fun_b_update_b_update_fun_fun$') > 'A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_314, type, 'map_fun$as': ('C_update_a_update_fun_c_update_a_update_fun_fun$' * 'C_update_c_update_fun_c_update_b_update_fun_fun$') > 'C_update_a_update_fun_c_update_c_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_315, type, 'comp$m': ('A_a_prod_update_b_b_prod_update_fun$' * 'C_b_prod_update_a_a_prod_update_fun$') > 'C_b_prod_update_b_b_prod_update_fun$').
% 4.95/2.49 tff(func_def_316, type, 'comp$as': ('A_a_prod_update_b_update_fun$' * 'C_b_prod_update_a_a_prod_update_fun$') > 'C_b_prod_update_b_update_fun$').
% 4.95/2.49 tff(func_def_317, type, 'fun_app$bm': ('C_update_c_update_fun_c_update_b_update_fun_fun$' * 'C_update_c_update_fun$') > 'C_update_b_update_fun$').
% 4.95/2.49 tff(func_def_318, type, 'inv_into$': ('B_update_set$' * 'B_update_a_update_fun$') > 'A_update_b_update_fun$').
% 4.95/2.49 tff(func_def_319, type, 'vimage$': 'C_update_c_update_fun$' > 'C_update_set_c_update_set_fun$').
% 4.95/2.49 tff(func_def_320, type, 'conversep$b': 'A_update_a_update_bool_fun_fun$' > 'A_update_a_update_bool_fun_fun$').
% 4.95/2.49 tff(func_def_321, type, 'uui$': 'B_update_a_update_fun$' > 'B_update_a_a_prod_update_fun$').
% 4.95/2.49 tff(func_def_322, type, 'grp$e': ('A_update_set$' * 'A_update_c_update_fun$') > 'A_update_c_update_bool_fun_fun$').
% 4.95/2.49 tff(func_def_323, type, 'rel_fun$': ('A_update_a_update_bool_fun_fun$' * 'B_update_a_update_bool_fun_fun$') > 'A_update_b_update_fun_a_update_a_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_324, type, 'id$v': 'B_update_set_b_update_set_fun$').
% 4.95/2.49 tff(func_def_325, type, 'rel_fun$bp': ('B_update_c_update_bool_fun_fun$' * 'A_update_a_update_bool_fun_fun$') > 'B_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_326, type, 'comp$y': ('B_update_a_update_fun$' * 'B_update_b_update_fun$') > 'B_update_a_update_fun$').
% 4.95/2.49 tff(func_def_327, type, 'fun_app$aa': ('B_update_b_update_fun$' * 'B_update$') > 'B_update$').
% 4.95/2.49 tff(func_def_328, type, 'comp$ae': ('B_update_a_update_fun$' * 'C_update_b_update_fun$') > 'C_update_a_update_fun$').
% 4.95/2.49 tff(func_def_329, type, 'f$a': 'A_update_b_update_fun$').
% 4.95/2.49 tff(func_def_330, type, 'comp$bp': ('B_update_bool_fun$' * 'A_update_b_update_fun$') > 'A_update_bool_fun$').
% 4.95/2.49 tff(func_def_331, type, 'rel_fun$ai': ('C_update_c_update_bool_fun_fun$' * 'C_update_c_update_bool_fun_fun$') > 'C_update_c_update_fun_c_update_c_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_332, type, 'comp$bm': ('A_update_a_update_fun_c_update_b_update_fun_fun$' * 'C_update_b_update_fun_a_update_a_update_fun_fun$') > 'C_update_b_update_fun_c_update_b_update_fun_fun$').
% 4.95/2.49 tff(func_def_333, type, 'fun_app$bb': ('B_update_a_update_fun_a_update_b_update_fun_fun$' * 'B_update_a_update_fun$') > 'A_update_b_update_fun$').
% 4.95/2.49 tff(func_def_334, type, 'conversep$': 'C_update_c_update_bool_fun_fun$' > 'C_update_c_update_bool_fun_fun$').
% 4.95/2.49 tff(func_def_335, type, 'map_fun$x': ('B_update_b_update_fun$' * 'A_update_a_update_fun$') > 'B_update_a_update_fun_b_update_a_update_fun_fun$').
% 4.95/2.49 tff(func_def_336, type, 'map_fun$l': ('A_update_c_update_fun$' * 'A_update_b_update_fun$') > 'C_update_a_update_fun_a_update_b_update_fun_fun$').
% 4.95/2.49 tff(func_def_337, type, 'comp$t': ('A_b_prod_update_b_a_prod_update_fun$' * 'C_a_prod_update_a_b_prod_update_fun$') > 'C_a_prod_update_b_a_prod_update_fun$').
% 4.95/2.49 tff(func_def_338, type, 'grp$c': ('B_update_set$' * 'B_update_a_update_fun$') > 'B_update_a_update_bool_fun_fun$').
% 4.95/2.49 tff(func_def_339, type, 'fun_app$bj': ('C_update_b_update_fun_a_update_a_update_fun_fun$' * 'C_update_b_update_fun$') > 'A_update_a_update_fun$').
% 4.95/2.49 tff(func_def_340, type, 'rel_fun$ay': ('B_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$' * 'B_update_c_update_fun_b_update_b_update_fun_bool_fun_fun$') > 'B_update_a_update_fun_b_update_c_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_341, type, 'comp$aa': ('A_update_a_update_fun$' * 'C_update_a_update_fun$') > 'C_update_a_update_fun$').
% 4.95/2.49 tff(func_def_342, type, 'fun_app$bi': ('C_update_c_update_fun_a_update_a_update_fun_fun$' * 'C_update_c_update_fun$') > 'A_update_a_update_fun$').
% 4.95/2.49 tff(func_def_343, type, 'rel_fun$av': ('B_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$' * 'B_update_c_update_fun_b_update_c_update_fun_bool_fun_fun$') > 'B_update_a_update_fun_b_update_c_update_fun_fun_b_update_a_update_fun_b_update_c_update_fun_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_344, type, 'rel_fun$aa': ('A_update_b_update_bool_fun_fun$' * 'C_update_a_update_bool_fun_fun$') > 'A_update_c_update_fun_b_update_a_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_345, type, 'pred_DEADID$b': 'A_update_bool_fun$').
% 4.95/2.49 tff(func_def_346, type, 'register_pair$t': ('B_update_c_update_fun$' * 'B_update_c_update_fun$') > 'B_b_prod_update_c_update_fun$').
% 4.95/2.49 tff(func_def_347, type, 'fun_app$bd': ('A_update_b_update_fun_a_update_b_update_fun_fun$' * 'A_update_b_update_fun$') > 'A_update_b_update_fun$').
% 4.95/2.49 tff(func_def_348, type, 'tensor_update$a': ('A_update$' * 'A_update$') > 'A_a_prod_update$').
% 4.95/2.49 tff(func_def_349, type, 'fun_app$y': ('A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$' * 'A_update_b_update_fun$') > 'C_update_a_update_fun_c_update_b_update_fun_fun$').
% 4.95/2.49 tff(func_def_350, type, 'fun_app$f': ('A_update_c_c_prod_update_fun$' * 'A_update$') > 'C_c_prod_update$').
% 4.95/2.49 tff(func_def_351, type, 'rel_fun$n': ('A_update_c_update_bool_fun_fun$' * 'A_update_c_update_bool_fun_fun$') > 'A_update_a_update_fun_c_update_c_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_352, type, 'comp$z': ('C_update_a_update_fun$' * 'C_update_c_update_fun$') > 'C_update_a_update_fun$').
% 4.95/2.49 tff(func_def_353, type, 'inv_into$c': ('A_update_set$' * 'A_update_c_update_fun$') > 'C_update_a_update_fun$').
% 4.95/2.49 tff(func_def_354, type, 'fun_app$bn': ('C_update_b_update_fun_c_update_b_update_fun_fun$' * 'C_update_b_update_fun$') > 'C_update_b_update_fun$').
% 4.95/2.49 tff(func_def_355, type, 'fun_app$av': ('A_update_a_update_fun_b_update_b_update_fun_fun$' * 'A_update_a_update_fun$') > 'B_update_b_update_fun$').
% 4.95/2.49 tff(func_def_356, type, 'fun_app$cb': ('C_update_c_update_fun_a_update_a_update_fun_bool_fun_fun$' * 'C_update_c_update_fun$') > 'A_update_a_update_fun_bool_fun$').
% 4.95/2.49 tff(func_def_357, type, 'comp$al': ('A_a_prod_update_c_update_fun$' * 'C_c_prod_update_a_a_prod_update_fun$') > 'C_c_prod_update_c_update_fun$').
% 4.95/2.49 tff(func_def_358, type, 'top$e': 'B_update_a_update_fun_set$').
% 4.95/2.49 tff(func_def_359, type, 'grp$h': ('A_update_set$' * 'A_update_b_update_fun$') > 'A_update_b_update_bool_fun_fun$').
% 4.95/2.49 tff(func_def_360, type, 'rel_fun$k': ('B_update_a_update_bool_fun_fun$' * 'A_update_c_update_bool_fun_fun$') > 'B_update_a_update_fun_a_update_c_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_361, type, 'id_update$b': 'B_update$').
% 4.95/2.49 tff(func_def_362, type, 'register_tensor$w': ('B_update_b_update_fun$' * 'B_update_c_update_fun$') > 'B_b_prod_update_b_c_prod_update_fun$').
% 4.95/2.49 tff(func_def_363, type, 'fun_app$bz': ('C_update_c_update_fun_b_update_b_update_fun_bool_fun_fun$' * 'C_update_c_update_fun$') > 'B_update_b_update_fun_bool_fun$').
% 4.95/2.49 tff(func_def_364, type, 'map_fun$ah': ('A_update_b_update_fun_b_update_a_update_fun_fun$' * 'A_update_b_update_fun_a_update_a_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$' * 'B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$') > 'A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_365, type, 'map_fun$aj': ('B_update_a_update_fun_a_update_c_update_fun_fun$' * 'C_update_a_update_fun_c_update_c_update_fun_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$' * 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$') > 'B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_366, type, 'fun_app$cd': ('A_update_a_update_fun_c_update_c_update_fun_bool_fun_fun$' * 'A_update_a_update_fun$') > 'C_update_c_update_fun_bool_fun$').
% 4.95/2.49 tff(func_def_367, type, 'comp$aw': ('A_update_b_update_fun$' * 'B_c_prod_update_a_update_fun$') > 'B_c_prod_update_b_update_fun$').
% 4.95/2.49 tff(func_def_368, type, 'id$h': 'B_a_prod_update_b_a_prod_update_fun$').
% 4.95/2.49 tff(func_def_369, type, 'grp$j': ('B_update_a_update_fun_set$' * 'B_update_a_update_fun_b_update_b_update_fun_fun$') > 'B_update_a_update_fun_b_update_b_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_370, type, 'relcompp$': ('A_update_a_update_bool_fun_fun$' * 'A_update_a_update_bool_fun_fun$') > 'A_update_a_update_bool_fun_fun$').
% 4.95/2.49 tff(func_def_371, type, 'fun_app$t': ('A_update_a_c_prod_update_fun$' * 'A_update$') > 'A_c_prod_update$').
% 4.95/2.49 tff(func_def_372, type, 'map_fun$at': ('A_update_b_update_fun_a_update_c_update_fun_fun$' * 'C_update_a_update_fun_c_update_c_update_fun_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$' * 'A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$') > 'A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_373, type, 'map_fun$d': ('B_update_a_update_fun$' * 'C_update_a_update_fun$') > 'A_update_c_update_fun_b_update_a_update_fun_fun$').
% 4.95/2.49 tff(func_def_374, type, 'comp$u': ('A_b_prod_update_b_a_prod_update_fun$' * 'B_a_prod_update_a_b_prod_update_fun$') > 'B_a_prod_update_b_a_prod_update_fun$').
% 4.95/2.49 tff(func_def_375, type, 'map_fun$r': ('C_update_c_update_fun$' * 'B_update_c_update_fun$') > 'C_update_b_update_fun_c_update_c_update_fun_fun$').
% 4.95/2.49 tff(func_def_376, type, 'fun_app$ax': ('A_update_c_update_fun_b_update_a_update_fun_fun$' * 'A_update_c_update_fun$') > 'B_update_a_update_fun$').
% 4.95/2.49 tff(func_def_377, type, 'comp$c': 'B_update_a_update_fun_a_update_b_update_fun_a_update_a_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_378, type, 'comp$w': ('A_update_b_update_fun$' * 'A_update_a_update_fun$') > 'A_update_b_update_fun$').
% 4.95/2.49 tff(func_def_379, type, 'comp$ax': ('A_update_b_update_fun$' * 'B_b_prod_update_a_update_fun$') > 'B_b_prod_update_b_update_fun$').
% 4.95/2.49 tff(func_def_380, type, 'id$t': 'A_update_b_update_fun_a_update_b_update_fun_fun$').
% 4.95/2.49 tff(func_def_381, type, 'fun_app$bf': ('C_update_a_update_fun_a_update_b_update_fun_fun$' * 'C_update_a_update_fun$') > 'A_update_b_update_fun$').
% 4.95/2.49 tff(func_def_382, type, 'uuh$': 'A_update_c_update_fun$' > 'A_update_c_a_prod_update_fun$').
% 4.95/2.49 tff(func_def_383, type, 'register_tensor$y': ('C_update_a_update_fun$' * 'A_update_b_update_fun$') > 'C_a_prod_update_a_b_prod_update_fun$').
% 4.95/2.49 tff(func_def_384, type, 'fun_app$j': ('C_update_c_update_bool_fun_fun$' * 'C_update$') > 'C_update_bool_fun$').
% 4.95/2.49 tff(func_def_385, type, 'register_tensor$g': ('A_update_a_update_fun$' * 'B_update_b_update_fun$') > 'A_b_prod_update_a_b_prod_update_fun$').
% 4.95/2.49 tff(func_def_386, type, 'comp$ac': ('C_update_a_update_fun$' * 'B_update_c_update_fun$') > 'B_update_a_update_fun$').
% 4.95/2.49 tff(func_def_387, type, 'top$d': 'C_update_a_update_fun_set$').
% 4.95/2.49 tff(func_def_388, type, 'g$a': 'C_update_a_update_fun$').
% 4.95/2.49 tff(func_def_389, type, 'the_inv_into$d': 'C_update_set$' > 'C_update_c_update_fun_c_update_c_update_fun_fun$').
% 4.95/2.49 tff(func_def_390, type, 'uuz$': 'B_update_a_update_fun_b_update_a_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_391, type, 'fun_app$ba': ('A_update_b_update_fun_a_update_c_update_fun_fun$' * 'A_update_b_update_fun$') > 'A_update_c_update_fun$').
% 4.95/2.49 tff(func_def_392, type, 'register_tensor$s': ('B_update_b_update_fun$' * 'C_update_b_update_fun$') > 'B_c_prod_update_b_b_prod_update_fun$').
% 4.95/2.49 tff(func_def_393, type, 'pred_DEADID$a': 'B_update_bool_fun$').
% 4.95/2.49 tff(func_def_394, type, 'inv_into$a': ('C_update_set$' * 'C_update_a_update_fun$') > 'A_update_c_update_fun$').
% 4.95/2.49 tff(func_def_395, type, 'uuj$': 'B_update_a_update_fun$' > 'B_update_a_a_prod_update_fun$').
% 4.95/2.49 tff(func_def_396, type, 'the_inv_into$h': 'B_update_set$' > 'B_update_b_update_fun_b_update_b_update_fun_fun$').
% 4.95/2.49 tff(func_def_397, type, 'comp$an': ('B_c_prod_update_a_update_fun$' * 'A_a_prod_update_b_c_prod_update_fun$') > 'A_a_prod_update_a_update_fun$').
% 4.95/2.49 tff(func_def_398, type, 'register_tensor$': ('C_update_c_update_fun$' * 'C_update_c_update_fun$') > 'C_c_prod_update_c_c_prod_update_fun$').
% 4.95/2.49 tff(func_def_399, type, 'iso_tuple_update_accessor_eq_assist$': ('C_update_c_update_fun_c_update_c_update_fun_fun$' * 'C_update_c_update_fun$' * 'C_update$' * 'C_update_c_update_fun$') > 'C_update_c_update_bool_fun_fun$').
% 4.95/2.49 tff(func_def_400, type, 'vimage$a': 'B_update_b_update_fun$' > 'B_update_set_b_update_set_fun$').
% 4.95/2.49 tff(func_def_401, type, 'map_fun$w': ('B_update_b_update_fun$' * 'B_update_b_update_fun$') > 'B_update_b_update_fun_b_update_b_update_fun_fun$').
% 4.95/2.49 tff(func_def_402, type, 'fun_app$cf': ('A_update_a_update_fun_a_update_a_update_fun_bool_fun_fun$' * 'A_update_a_update_fun$') > 'A_update_a_update_fun_bool_fun$').
% 4.95/2.49 tff(func_def_403, type, 'rel_fun$ad': ('C_update_a_update_bool_fun_fun$' * 'C_update_a_update_bool_fun_fun$') > 'C_update_c_update_fun_a_update_a_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_404, type, 'image$c': ('A_update_c_update_fun$' * 'A_update_set$') > 'C_update_set$').
% 4.95/2.49 tff(func_def_405, type, 'comp$bg': ('B_update_a_update_fun_a_update_b_update_fun_fun$' * 'A_update_c_update_fun_b_update_a_update_fun_fun$') > 'A_update_c_update_fun_a_update_b_update_fun_fun$').
% 4.95/2.49 tff(func_def_406, type, 'register_tensor$x': ('A_update_b_update_fun$' * 'B_update_a_update_fun$') > 'A_b_prod_update_b_a_prod_update_fun$').
% 4.95/2.49 tff(func_def_407, type, 'id_update$a': 'A_update$').
% 4.95/2.49 tff(func_def_408, type, 'map_fun$': ('A_update_b_update_fun$' * 'B_update_a_update_fun$') > 'B_update_b_update_fun_a_update_a_update_fun_fun$').
% 4.95/2.49 tff(func_def_409, type, 'comp$ba': ('A_update_c_update_fun$' * 'B_c_prod_update_a_update_fun$') > 'B_c_prod_update_c_update_fun$').
% 4.95/2.49 tff(func_def_410, type, 'rel_fun$r': ('A_update_b_update_bool_fun_fun$' * 'A_update_c_update_bool_fun_fun$') > 'A_update_a_update_fun_b_update_c_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_411, type, 'collect$': 'A_update_b_update_fun_bool_fun$' > 'A_update_b_update_fun_set$').
% 4.95/2.49 tff(func_def_412, type, 'comp$e': 'A_update_b_update_fun_b_update_a_update_fun_b_update_b_update_fun_fun_fun$').
% 4.95/2.49 tff(func_def_413, type, 'tensor_update$': ('A_update$' * 'C_update$') > 'A_c_prod_update$').
% 4.95/2.49 tff(func_def_414, type, 'g$': 'A_update_c_update_fun$').
% 4.95/2.49 tff(func_def_415, type, 'fun_app$af': ('A_update_c_update_fun_c_update_a_update_fun_c_update_c_update_fun_fun_fun$' * 'A_update_c_update_fun$') > 'C_update_a_update_fun_c_update_c_update_fun_fun$').
% 4.95/2.49 tff(func_def_416, type, 'id$i': 'A_c_prod_update_a_c_prod_update_fun$').
% 4.95/2.49 tff(func_def_417, type, 'fun_app$ah': ('B_update_c_update_fun$' * 'B_update$') > 'C_update$').
% 4.95/2.49 tff(func_def_418, type, 'comp$ai': ('C_update_b_update_fun$' * 'A_update_c_update_fun$') > 'A_update_b_update_fun$').
% 4.95/2.49 tff(func_def_419, type, 'grp$f': ('C_update_a_update_fun_set$' * 'C_update_a_update_fun_c_update_c_update_fun_fun$') > 'C_update_a_update_fun_c_update_c_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_420, type, 'comp$bj': ('A_update_a_update_fun_c_update_c_update_fun_fun$' * 'C_update_c_update_fun_a_update_a_update_fun_fun$') > 'C_update_c_update_fun_c_update_c_update_fun_fun$').
% 4.95/2.49 tff(func_def_421, type, 'fun_app$l': ('B_update_b_update_bool_fun_fun$' * 'B_update$') > 'B_update_bool_fun$').
% 4.95/2.49 tff(func_def_422, type, 'comp$bc': ('B_update_a_update_fun$' * 'A_a_prod_update_b_update_fun$') > 'A_a_prod_update_a_update_fun$').
% 4.95/2.49 tff(func_def_423, type, 'id$o': 'C_update_b_update_fun_c_update_b_update_fun_fun$').
% 4.95/2.49 tff(func_def_424, type, 'fun_app$ai': ('C_update_b_update_fun$' * 'C_update$') > 'B_update$').
% 4.95/2.49 tff(func_def_425, type, 'rel_fun$aq': ('C_update_c_update_bool_fun_fun$' * 'C_update_b_update_bool_fun_fun$') > 'C_update_c_update_fun_c_update_b_update_fun_bool_fun_fun$').
% 4.95/2.49 tff(func_def_426, type, 'the_inv_into$c': 'A_update_set$' > 'A_update_a_update_fun_a_update_a_update_fun_fun$').
% 4.95/2.49 tff(func_def_427, type, 'map_fun$t': ('C_update_c_update_fun$' * 'C_update_b_update_fun$') > 'C_update_c_update_fun_c_update_b_update_fun_fun$').
% 4.95/2.49 tff(func_def_428, type, 'id$p': 'C_update_a_update_fun_c_update_a_update_fun_fun$').
% 4.95/2.49 tff(func_def_429, type, 'comp$p': ('A_a_prod_update_b_c_prod_update_fun$' * 'C_c_prod_update_a_a_prod_update_fun$') > 'C_c_prod_update_b_c_prod_update_fun$').
% 4.95/2.49 tff(func_def_430, type, 'inv_into$d': 'C_update_set$' > 'C_update_c_update_fun_c_update_c_update_fun_fun$').
% 4.95/2.49 tff(func_def_431, type, 'map_fun$e': ('A_update_a_update_fun$' * 'C_update_c_update_fun$') > 'A_update_c_update_fun_a_update_c_update_fun_fun$').
% 4.95/2.49 tff(func_def_432, type, 'comp$be': ('B_update_a_update_fun_a_update_c_update_fun_fun$' * 'A_update_c_update_fun_b_update_a_update_fun_fun$') > 'A_update_c_update_fun_a_update_c_update_fun_fun$').
% 4.95/2.49 tff(func_def_433, type, 'fun_app$au': ('B_update_b_update_fun_a_update_a_update_fun_fun$' * 'B_update_b_update_fun$') > 'A_update_a_update_fun$').
% 4.95/2.49 tff(func_def_434, type, 'map_fun$k': ('C_update_a_update_fun$' * 'B_update_a_update_fun$') > 'A_update_b_update_fun_c_update_a_update_fun_fun$').
% 4.95/2.49 tff(func_def_435, type, 'fcomp$d': ('B_update_a_update_fun$' * 'A_update_b_update_fun$') > 'B_update_b_update_fun$').
% 4.95/2.49 tff(func_def_436, type, 'register_tensor$t': ('A_update_b_update_fun$' * 'A_update_c_update_fun$') > 'A_a_prod_update_b_c_prod_update_fun$').
% 4.95/2.49 tff(func_def_437, type, 'comp$ad': ('A_update_a_update_fun$' * 'B_update_a_update_fun$') > 'B_update_a_update_fun$').
% 4.95/2.49 tff(func_def_438, type, 'inv_into$f': 'A_update_set$' > 'A_update_a_update_fun_a_update_a_update_fun_fun$').
% 4.95/2.49 tff(func_def_439, type, sK0: 'B_update_a_update_fun$').
% 4.95/2.49 tff(func_def_440, type, sK1: 'A_update_c_update_fun$').
% 4.95/2.49 tff(func_def_441, type, sK2: 'C_update_c_update_fun$' > 'C_update$').
% 4.95/2.49 tff(func_def_442, type, sK3: 'A_update_a_update_fun$' > 'A_update$').
% 4.95/2.49 tff(func_def_443, type, sK4: 'A_update_b_update_fun$' > 'B_update_a_update_fun$').
% 4.95/2.49 tff(func_def_444, type, sK5: 'C_update_a_update_fun$' > 'A_update_c_update_fun$').
% 4.95/2.49 tff(func_def_445, type, sK6: 'B_update_b_update_fun$' > 'B_update$').
% 4.95/2.49 tff(func_def_446, type, sK7: 'B_update_a_update_fun$' > 'A_update_b_update_fun$').
% 4.95/2.49 tff(func_def_447, type, sK8: 'A_update_c_update_fun$' > 'C_update_a_update_fun$').
% 4.95/2.49 tff(func_def_448, type, sK9: ('B_update_a_update_fun$' * 'A_update_c_update_fun$' * 'A_update_c_update_fun$') > 'B_update$').
% 4.95/2.49 tff(f30,conjecture,(
% 4.95/2.49 'comp$'('fun_app$v'('fun_app$w'('comp$a','g$'),'f$'),'fun_app$x'('fun_app$y'('comp$b','f$a'),'g$a')) = 'id$'),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture29)).
% 4.95/2.49
% 4.95/2.49 tff(f31,negated_conjecture,(
% 4.95/2.49 ~ 'comp$'('fun_app$v'('fun_app$w'('comp$a','g$'),'f$'),'fun_app$x'('fun_app$y'('comp$b','f$a'),'g$a')) = 'id$'),
% 4.95/2.49 inference(negated_conjecture,[status(cth)],[f30])).
% 4.95/2.49
% 4.95/2.49 tff(f33,axiom,(
% 4.95/2.49 'iso_register$a'('f$a')),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom31)).
% 4.95/2.49
% 4.95/2.49 tff(f44,axiom,(
% 4.95/2.49 'fun_app$ae'('fun_app$af'('comp$d','g$'),'g$a') = 'id$'),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom42)).
% 4.95/2.49
% 4.95/2.49 tff(f71,axiom,(
% 4.95/2.49 'fun_app$ac'('fun_app$ad'('comp$c','f$'),'f$a') = 'id$b'),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom69)).
% 4.95/2.49
% 4.95/2.49 tff(f134,axiom,(
% 4.95/2.49 ! [X0 : 'B_update_a_update_fun$',X1 : 'C_update_b_update_fun$',X2 : 'C_update_a_update_fun$',X3 : 'A_update_c_update_fun$'] : ('comp$ae'(X0,X1) = X2 => 'comp$'('fun_app$v'('fun_app$w'('comp$a',X3),X0),X1) = 'fun_app$ae'('fun_app$af'('comp$d',X3),X2))),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom132)).
% 4.95/2.49
% 4.95/2.49 tff(f146,axiom,(
% 4.95/2.49 ! [X0 : 'B_update_c_update_fun$',X1 : 'A_update_b_update_fun$',X2 : 'A_update_c_update_fun$',X3 : 'C_update_a_update_fun$'] : ('comp$aj'(X0,X1) = X2 => 'comp$'(X0,'fun_app$x'('fun_app$y'('comp$b',X1),X3)) = 'fun_app$ae'('fun_app$af'('comp$d',X2),X3))),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom144)).
% 4.95/2.49
% 4.95/2.49 tff(f166,axiom,(
% 4.95/2.49 ! [X0 : 'B_update_a_update_fun$',X1 : 'A_update_b_update_fun$',X2 : 'C_update_a_update_fun$'] : 'comp$aa'('fun_app$ac'('fun_app$ad'('comp$c',X0),X1),X2) = 'comp$ae'(X0,'fun_app$x'('fun_app$y'('comp$b',X1),X2))),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom164)).
% 4.95/2.49
% 4.95/2.49 tff(f171,axiom,(
% 4.95/2.49 ! [X0 : 'A_update_c_update_fun$',X1 : 'B_update_a_update_fun$',X2 : 'A_update_b_update_fun$'] : 'comp$aj'('fun_app$v'('fun_app$w'('comp$a',X0),X1),X2) = 'comp$ab'(X0,'fun_app$ac'('fun_app$ad'('comp$c',X1),X2))),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom169)).
% 4.95/2.49
% 4.95/2.49 tff(f172,axiom,(
% 4.95/2.49 ! [X0 : 'A_update_c_update_fun$',X1 : 'B_update_a_update_fun$',X2 : 'C_update_b_update_fun$'] : 'comp$'('fun_app$v'('fun_app$w'('comp$a',X0),X1),X2) = 'fun_app$ae'('fun_app$af'('comp$d',X0),'comp$ae'(X1,X2))),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom170)).
% 4.95/2.49
% 4.95/2.49 tff(f181,axiom,(
% 4.95/2.49 ! [X0 : 'A_update_c_update_fun$',X1 : 'B_update_a_update_fun$',X2 : 'A_update_b_update_fun$'] : 'comp$ab'(X0,'fun_app$ac'('fun_app$ad'('comp$c',X1),X2)) = 'comp$aj'('fun_app$v'('fun_app$w'('comp$a',X0),X1),X2)),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom179)).
% 4.95/2.49
% 4.95/2.49 tff(f188,axiom,(
% 4.95/2.49 ! [X0 : 'B_update_a_update_fun$',X1 : 'A_update_b_update_fun$',X2 : 'C_update_a_update_fun$'] : 'comp$ae'(X0,'fun_app$x'('fun_app$y'('comp$b',X1),X2)) = 'comp$aa'('fun_app$ac'('fun_app$ad'('comp$c',X0),X1),X2)),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom186)).
% 4.95/2.49
% 4.95/2.49 tff(f402,axiom,(
% 4.95/2.49 ! [X0 : 'A_update_b_update_fun$'] : ('iso_register$a'(X0) => 'fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0)),X0) = 'id$b')),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom400)).
% 4.95/2.49
% 4.95/2.49 tff(f470,axiom,(
% 4.95/2.49 ! [X0 : 'A_update_b_update_fun$'] : ('inj_on$'(X0,'top$') => 'fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0)),X0) = 'id$b')),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom468)).
% 4.95/2.49
% 4.95/2.49 tff(f481,axiom,(
% 4.95/2.49 ! [X0 : 'A_update_b_update_fun$',X1 : 'A_update_c_update_fun$'] : ('inj_on$'(X0,'top$') => 'comp$aj'('fun_app$v'('fun_app$w'('comp$a',X1),'inv_into$b'('top$',X0)),X0) = X1)),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom479)).
% 4.95/2.49
% 4.95/2.49 tff(f484,axiom,(
% 4.95/2.49 ! [X0 : 'A_update_b_update_fun$',X1 : 'A_update_a_update_fun$'] : ('inj_on$'(X0,'top$') => 'fun_app$ac'('fun_app$ad'('comp$c','comp$ad'(X1,'inv_into$b'('top$',X0))),X0) = X1)),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom482)).
% 4.95/2.49
% 4.95/2.49 tff(f577,axiom,(
% 4.95/2.49 ! [X0 : 'A_update_b_update_fun$'] : ('inj_on$'(X0,'top$') <=> 'fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0)),X0) = 'id$b')),
% 4.95/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom575)).
% 4.95/2.49
% 4.95/2.49 tff(f671,plain,(
% 4.95/2.49 'comp$'('fun_app$v'('fun_app$w'('comp$a','g$'),'f$'),'fun_app$x'('fun_app$y'('comp$b','f$a'),'g$a')) != 'id$'),
% 4.95/2.49 inference(flattening,[],[f31])).
% 4.95/2.49
% 4.95/2.49 tff(f682,plain,(
% 4.95/2.49 ! [X0 : 'B_update_c_update_fun$',X1 : 'A_update_b_update_fun$',X2 : 'A_update_c_update_fun$',X3 : 'C_update_a_update_fun$'] : ('comp$'(X0,'fun_app$x'('fun_app$y'('comp$b',X1),X3)) = 'fun_app$ae'('fun_app$af'('comp$d',X2),X3) | 'comp$aj'(X0,X1) != X2)),
% 4.95/2.49 inference(ennf_transformation,[],[f146])).
% 4.95/2.49
% 4.95/2.49 tff(f683,plain,(
% 4.95/2.49 ! [X0 : 'B_update_a_update_fun$',X1 : 'C_update_b_update_fun$',X2 : 'C_update_a_update_fun$',X3 : 'A_update_c_update_fun$'] : ('comp$'('fun_app$v'('fun_app$w'('comp$a',X3),X0),X1) = 'fun_app$ae'('fun_app$af'('comp$d',X3),X2) | 'comp$ae'(X0,X1) != X2)),
% 4.95/2.49 inference(ennf_transformation,[],[f134])).
% 4.95/2.49
% 4.95/2.49 tff(f715,plain,(
% 4.95/2.49 ! [X0 : 'A_update_b_update_fun$',X1 : 'A_update_c_update_fun$'] : ('comp$aj'('fun_app$v'('fun_app$w'('comp$a',X1),'inv_into$b'('top$',X0)),X0) = X1 | ~'inj_on$'(X0,'top$'))),
% 4.95/2.49 inference(ennf_transformation,[],[f481])).
% 4.95/2.49
% 4.95/2.49 tff(f725,plain,(
% 4.95/2.49 ! [X0 : 'A_update_b_update_fun$'] : ('fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0)),X0) = 'id$b' | ~'iso_register$a'(X0))),
% 4.95/2.49 inference(ennf_transformation,[],[f402])).
% 4.95/2.49
% 4.95/2.49 tff(f749,plain,(
% 4.95/2.49 ! [X0 : 'A_update_b_update_fun$',X1 : 'A_update_a_update_fun$'] : ('fun_app$ac'('fun_app$ad'('comp$c','comp$ad'(X1,'inv_into$b'('top$',X0))),X0) = X1 | ~'inj_on$'(X0,'top$'))),
% 4.95/2.49 inference(ennf_transformation,[],[f484])).
% 4.95/2.49
% 4.95/2.49 tff(f751,plain,(
% 4.95/2.49 ! [X0 : 'A_update_b_update_fun$'] : ('fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0)),X0) = 'id$b' | ~'inj_on$'(X0,'top$'))),
% 4.95/2.49 inference(ennf_transformation,[],[f470])).
% 4.95/2.49
% 4.95/2.49 tff(f843,plain,(
% 4.95/2.49 ! [X0 : 'A_update_b_update_fun$'] : (('inj_on$'(X0,'top$') | 'id$b' != 'fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0)),X0)) & ('fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0)),X0) = 'id$b' | ~'inj_on$'(X0,'top$')))),
% 4.95/2.49 inference(nnf_transformation,[],[f577])).
% 4.95/2.49
% 4.95/2.49 tff(f856,plain,(
% 4.95/2.49 'comp$'('fun_app$v'('fun_app$w'('comp$a','g$'),'f$'),'fun_app$x'('fun_app$y'('comp$b','f$a'),'g$a')) != 'id$'),
% 4.95/2.49 inference(cnf_transformation,[],[f671])).
% 4.95/2.49
% 4.95/2.49 tff(f857,plain,(
% 4.95/2.49 'id$b' = 'fun_app$ac'('fun_app$ad'('comp$c','f$'),'f$a')),
% 4.95/2.49 inference(cnf_transformation,[],[f71])).
% 4.95/2.49
% 4.95/2.49 tff(f862,plain,(
% 4.95/2.49 ( ! [X2 : 'C_update_b_update_fun$',X0 : 'A_update_c_update_fun$',X1 : 'B_update_a_update_fun$'] : ('comp$'('fun_app$v'('fun_app$w'('comp$a',X0),X1),X2) = 'fun_app$ae'('fun_app$af'('comp$d',X0),'comp$ae'(X1,X2))) )),
% 4.95/2.49 inference(cnf_transformation,[],[f172])).
% 4.95/2.49
% 4.95/2.49 tff(f863,plain,(
% 4.95/2.49 ( ! [X2 : 'A_update_c_update_fun$',X3 : 'C_update_a_update_fun$',X0 : 'B_update_c_update_fun$',X1 : 'A_update_b_update_fun$'] : ('fun_app$ae'('fun_app$af'('comp$d',X2),X3) = 'comp$'(X0,'fun_app$x'('fun_app$y'('comp$b',X1),X3)) | 'comp$aj'(X0,X1) != X2) )),
% 4.95/2.49 inference(cnf_transformation,[],[f682])).
% 4.95/2.49
% 4.95/2.49 tff(f864,plain,(
% 4.95/2.49 ( ! [X2 : 'C_update_a_update_fun$',X3 : 'A_update_c_update_fun$',X0 : 'B_update_a_update_fun$',X1 : 'C_update_b_update_fun$'] : ('fun_app$ae'('fun_app$af'('comp$d',X3),X2) = 'comp$'('fun_app$v'('fun_app$w'('comp$a',X3),X0),X1) | 'comp$ae'(X0,X1) != X2) )),
% 4.95/2.49 inference(cnf_transformation,[],[f683])).
% 4.95/2.49
% 4.95/2.49 tff(f873,plain,(
% 4.95/2.49 'iso_register$a'('f$a')),
% 4.95/2.49 inference(cnf_transformation,[],[f33])).
% 4.95/2.49
% 4.95/2.49 tff(f875,plain,(
% 4.95/2.49 'id$' = 'fun_app$ae'('fun_app$af'('comp$d','g$'),'g$a')),
% 4.95/2.49 inference(cnf_transformation,[],[f44])).
% 4.95/2.49
% 4.95/2.49 tff(f918,plain,(
% 4.95/2.49 ( ! [X0 : 'A_update_b_update_fun$',X1 : 'A_update_c_update_fun$'] : ('comp$aj'('fun_app$v'('fun_app$w'('comp$a',X1),'inv_into$b'('top$',X0)),X0) = X1 | ~'inj_on$'(X0,'top$')) )),
% 4.95/2.49 inference(cnf_transformation,[],[f715])).
% 4.95/2.49
% 4.95/2.49 tff(f919,plain,(
% 4.95/2.49 ( ! [X2 : 'A_update_b_update_fun$',X0 : 'A_update_c_update_fun$',X1 : 'B_update_a_update_fun$'] : ('comp$aj'('fun_app$v'('fun_app$w'('comp$a',X0),X1),X2) = 'comp$ab'(X0,'fun_app$ac'('fun_app$ad'('comp$c',X1),X2))) )),
% 4.95/2.49 inference(cnf_transformation,[],[f181])).
% 4.95/2.49
% 4.95/2.49 tff(f920,plain,(
% 4.95/2.49 ( ! [X2 : 'A_update_b_update_fun$',X0 : 'A_update_c_update_fun$',X1 : 'B_update_a_update_fun$'] : ('comp$aj'('fun_app$v'('fun_app$w'('comp$a',X0),X1),X2) = 'comp$ab'(X0,'fun_app$ac'('fun_app$ad'('comp$c',X1),X2))) )),
% 4.95/2.49 inference(cnf_transformation,[],[f171])).
% 4.95/2.49
% 4.95/2.49 tff(f921,plain,(
% 4.95/2.49 ( ! [X2 : 'C_update_a_update_fun$',X0 : 'B_update_a_update_fun$',X1 : 'A_update_b_update_fun$'] : ('comp$aa'('fun_app$ac'('fun_app$ad'('comp$c',X0),X1),X2) = 'comp$ae'(X0,'fun_app$x'('fun_app$y'('comp$b',X1),X2))) )),
% 4.95/2.49 inference(cnf_transformation,[],[f188])).
% 4.95/2.49
% 4.95/2.49 tff(f922,plain,(
% 4.95/2.49 ( ! [X2 : 'C_update_a_update_fun$',X0 : 'B_update_a_update_fun$',X1 : 'A_update_b_update_fun$'] : ('comp$aa'('fun_app$ac'('fun_app$ad'('comp$c',X0),X1),X2) = 'comp$ae'(X0,'fun_app$x'('fun_app$y'('comp$b',X1),X2))) )),
% 4.95/2.49 inference(cnf_transformation,[],[f166])).
% 4.95/2.49
% 4.95/2.49 tff(f929,plain,(
% 4.95/2.49 ( ! [X0 : 'A_update_b_update_fun$'] : ('id$b' = 'fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0)),X0) | ~'iso_register$a'(X0)) )),
% 4.95/2.49 inference(cnf_transformation,[],[f725])).
% 4.95/2.49
% 4.95/2.49 tff(f973,plain,(
% 4.95/2.49 ( ! [X0 : 'A_update_b_update_fun$'] : ('inj_on$'(X0,'top$') | 'id$b' != 'fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0)),X0)) )),
% 4.95/2.49 inference(cnf_transformation,[],[f843])).
% 4.95/2.49
% 4.95/2.49 tff(f974,plain,(
% 4.95/2.49 ( ! [X0 : 'A_update_b_update_fun$',X1 : 'A_update_a_update_fun$'] : ('fun_app$ac'('fun_app$ad'('comp$c','comp$ad'(X1,'inv_into$b'('top$',X0))),X0) = X1 | ~'inj_on$'(X0,'top$')) )),
% 4.95/2.49 inference(cnf_transformation,[],[f749])).
% 4.95/2.49
% 4.95/2.49 tff(f978,plain,(
% 4.95/2.49 ( ! [X0 : 'A_update_b_update_fun$'] : ('id$b' = 'fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0)),X0) | ~'inj_on$'(X0,'top$')) )),
% 4.95/2.49 inference(cnf_transformation,[],[f751])).
% 4.95/2.49
% 4.95/2.49 tff(f1061,plain,(
% 4.95/2.49 ( ! [X3 : 'C_update_a_update_fun$',X0 : 'B_update_c_update_fun$',X1 : 'A_update_b_update_fun$'] : ('comp$'(X0,'fun_app$x'('fun_app$y'('comp$b',X1),X3)) = 'fun_app$ae'('fun_app$af'('comp$d','comp$aj'(X0,X1)),X3)) )),
% 4.95/2.49 inference(equality_resolution,[],[f863])).
% 4.95/2.49
% 4.95/2.49 tff(f1062,plain,(
% 4.95/2.49 ( ! [X3 : 'A_update_c_update_fun$',X0 : 'B_update_a_update_fun$',X1 : 'C_update_b_update_fun$'] : ('comp$'('fun_app$v'('fun_app$w'('comp$a',X3),X0),X1) = 'fun_app$ae'('fun_app$af'('comp$d',X3),'comp$ae'(X0,X1))) )),
% 4.95/2.49 inference(equality_resolution,[],[f864])).
% 4.95/2.49
% 4.95/2.49 tcf(c_49,negated_conjecture,
% 4.95/2.49 ('comp$'('fun_app$v'('fun_app$w'('comp$a','g$'),'f$'),'fun_app$x'('fun_app$y'('comp$b','f$a'),'g$a')) != 'id$'),
% 4.95/2.49 inference(cnf_transformation,[],[f856])).
% 4.95/2.49
% 4.95/2.49 tcf(c_50,plain,
% 4.95/2.49 ('fun_app$ac'('fun_app$ad'('comp$c','f$'),'f$a') = 'id$b'),
% 4.95/2.49 inference(cnf_transformation,[],[f857])).
% 4.95/2.49
% 4.95/2.49 tcf(c_55,plain,![X0_'B_update_a_update_fun':'B_update_a_update_fun$',X0_'C_update_b_update_fun':'C_update_b_update_fun$',X0_'A_update_c_update_fun':'A_update_c_update_fun$']:
% 4.95/2.49 ('fun_app$ae'('fun_app$af'('comp$d',X0_'A_update_c_update_fun'),'comp$ae'(X0_'B_update_a_update_fun',X0_'C_update_b_update_fun')) = 'comp$'('fun_app$v'('fun_app$w'('comp$a',X0_'A_update_c_update_fun'),X0_'B_update_a_update_fun'),X0_'C_update_b_update_fun')),
% 4.95/2.49 inference(cnf_transformation,[],[f862])).
% 4.95/2.49
% 4.95/2.49 tcf(c_56,plain,![X0_'A_update_b_update_fun':'A_update_b_update_fun$',X0_'B_update_c_update_fun':'B_update_c_update_fun$',X0_'C_update_a_update_fun':'C_update_a_update_fun$']:
% 4.95/2.49 ('fun_app$ae'('fun_app$af'('comp$d','comp$aj'(X0_'B_update_c_update_fun',X0_'A_update_b_update_fun')),X0_'C_update_a_update_fun') = 'comp$'(X0_'B_update_c_update_fun','fun_app$x'('fun_app$y'('comp$b',X0_'A_update_b_update_fun'),X0_'C_update_a_update_fun'))),
% 4.95/2.49 inference(cnf_transformation,[],[f1061])).
% 4.95/2.49
% 4.95/2.49 tcf(c_57,plain,![X0_'B_update_a_update_fun':'B_update_a_update_fun$',X0_'C_update_b_update_fun':'C_update_b_update_fun$',X0_'A_update_c_update_fun':'A_update_c_update_fun$']:
% 4.95/2.49 ('fun_app$ae'('fun_app$af'('comp$d',X0_'A_update_c_update_fun'),'comp$ae'(X0_'B_update_a_update_fun',X0_'C_update_b_update_fun')) = 'comp$'('fun_app$v'('fun_app$w'('comp$a',X0_'A_update_c_update_fun'),X0_'B_update_a_update_fun'),X0_'C_update_b_update_fun')),
% 4.95/2.49 inference(cnf_transformation,[],[f1062])).
% 4.95/2.49
% 4.95/2.49 tcf(c_66,plain,
% 4.95/2.49 ('iso_register$a'('f$a')),
% 4.95/2.49 inference(cnf_transformation,[],[f873])).
% 4.95/2.49
% 4.95/2.49 tcf(c_68,plain,
% 4.95/2.49 ('fun_app$ae'('fun_app$af'('comp$d','g$'),'g$a') = 'id$'),
% 4.95/2.49 inference(cnf_transformation,[],[f875])).
% 4.95/2.49
% 4.95/2.49 tcf(c_111,plain,![X0_'A_update_b_update_fun':'A_update_b_update_fun$',X0_'A_update_c_update_fun':'A_update_c_update_fun$']:
% 4.95/2.49 (~'inj_on$'(X0_'A_update_b_update_fun','top$')|'comp$aj'('fun_app$v'('fun_app$w'('comp$a',X0_'A_update_c_update_fun'),'inv_into$b'('top$',X0_'A_update_b_update_fun')),X0_'A_update_b_update_fun') = X0_'A_update_c_update_fun'),
% 4.95/2.49 inference(cnf_transformation,[],[f918])).
% 4.95/2.49
% 4.95/2.49 tcf(c_112,plain,![X0_'B_update_a_update_fun':'B_update_a_update_fun$',X0_'A_update_b_update_fun':'A_update_b_update_fun$',X0_'A_update_c_update_fun':'A_update_c_update_fun$']:
% 4.95/2.49 ('comp$ab'(X0_'A_update_c_update_fun','fun_app$ac'('fun_app$ad'('comp$c',X0_'B_update_a_update_fun'),X0_'A_update_b_update_fun')) = 'comp$aj'('fun_app$v'('fun_app$w'('comp$a',X0_'A_update_c_update_fun'),X0_'B_update_a_update_fun'),X0_'A_update_b_update_fun')),
% 4.95/2.49 inference(cnf_transformation,[],[f919])).
% 4.95/2.49
% 4.95/2.49 tcf(c_113,plain,![X0_'B_update_a_update_fun':'B_update_a_update_fun$',X0_'A_update_b_update_fun':'A_update_b_update_fun$',X0_'A_update_c_update_fun':'A_update_c_update_fun$']:
% 4.95/2.49 ('comp$ab'(X0_'A_update_c_update_fun','fun_app$ac'('fun_app$ad'('comp$c',X0_'B_update_a_update_fun'),X0_'A_update_b_update_fun')) = 'comp$aj'('fun_app$v'('fun_app$w'('comp$a',X0_'A_update_c_update_fun'),X0_'B_update_a_update_fun'),X0_'A_update_b_update_fun')),
% 4.95/2.49 inference(cnf_transformation,[],[f920])).
% 4.95/2.49
% 4.95/2.49 tcf(c_114,plain,![X0_'B_update_a_update_fun':'B_update_a_update_fun$',X0_'A_update_b_update_fun':'A_update_b_update_fun$',X0_'C_update_a_update_fun':'C_update_a_update_fun$']:
% 4.95/2.49 ('comp$ae'(X0_'B_update_a_update_fun','fun_app$x'('fun_app$y'('comp$b',X0_'A_update_b_update_fun'),X0_'C_update_a_update_fun')) = 'comp$aa'('fun_app$ac'('fun_app$ad'('comp$c',X0_'B_update_a_update_fun'),X0_'A_update_b_update_fun'),X0_'C_update_a_update_fun')),
% 4.95/2.49 inference(cnf_transformation,[],[f921])).
% 4.95/2.49
% 4.95/2.49 tcf(c_115,plain,![X0_'B_update_a_update_fun':'B_update_a_update_fun$',X0_'A_update_b_update_fun':'A_update_b_update_fun$',X0_'C_update_a_update_fun':'C_update_a_update_fun$']:
% 4.95/2.49 ('comp$ae'(X0_'B_update_a_update_fun','fun_app$x'('fun_app$y'('comp$b',X0_'A_update_b_update_fun'),X0_'C_update_a_update_fun')) = 'comp$aa'('fun_app$ac'('fun_app$ad'('comp$c',X0_'B_update_a_update_fun'),X0_'A_update_b_update_fun'),X0_'C_update_a_update_fun')),
% 4.95/2.49 inference(cnf_transformation,[],[f922])).
% 4.95/2.49
% 4.95/2.49 tcf(c_122,plain,![X0_'A_update_b_update_fun':'A_update_b_update_fun$']:
% 4.95/2.49 (~'iso_register$a'(X0_'A_update_b_update_fun')|'fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0_'A_update_b_update_fun')),X0_'A_update_b_update_fun') = 'id$b'),
% 4.95/2.49 inference(cnf_transformation,[],[f929])).
% 4.95/2.49
% 4.95/2.49 tcf(c_165,plain,![X0_'A_update_b_update_fun':'A_update_b_update_fun$']:
% 4.95/2.49 ('fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0_'A_update_b_update_fun')),X0_'A_update_b_update_fun') != 'id$b'|
% 4.95/2.49 'inj_on$'(X0_'A_update_b_update_fun','top$')),
% 4.95/2.49 inference(cnf_transformation,[],[f973])).
% 4.95/2.49
% 4.95/2.49 tcf(c_167,plain,![X0_'A_update_a_update_fun':'A_update_a_update_fun$',X0_'A_update_b_update_fun':'A_update_b_update_fun$']:
% 4.95/2.49 (~'inj_on$'(X0_'A_update_b_update_fun','top$')|'fun_app$ac'('fun_app$ad'('comp$c','comp$ad'(X0_'A_update_a_update_fun','inv_into$b'('top$',X0_'A_update_b_update_fun'))),X0_'A_update_b_update_fun') = X0_'A_update_a_update_fun'),
% 4.95/2.49 inference(cnf_transformation,[],[f974])).
% 4.95/2.49
% 4.95/2.49 tcf(c_171,plain,![X0_'A_update_b_update_fun':'A_update_b_update_fun$']:
% 4.95/2.49 (~'inj_on$'(X0_'A_update_b_update_fun','top$')|'fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0_'A_update_b_update_fun')),X0_'A_update_b_update_fun') = 'id$b'),
% 4.95/2.49 inference(cnf_transformation,[],[f978])).
% 4.95/2.49
% 4.95/2.49 tcf(c_466,plain,![X0_'A_update_b_update_fun':'A_update_b_update_fun$',X0_'A_update_c_update_fun':'A_update_c_update_fun$']:
% 4.95/2.49 (~'inj_on$'(X0_'A_update_b_update_fun','top$')|'comp$aj'('fun_app$v'('fun_app$w'('comp$a',X0_'A_update_c_update_fun'),'inv_into$b'('top$',X0_'A_update_b_update_fun')),X0_'A_update_b_update_fun') = X0_'A_update_c_update_fun'),
% 4.95/2.49 inference(prop_impl_just,[status(thm)],[c_111])).
% 4.95/2.49
% 4.95/2.49 tcf(c_472,plain,![X0_'A_update_b_update_fun':'A_update_b_update_fun$']:
% 4.95/2.49 ('inj_on$'(X0_'A_update_b_update_fun','top$')|~'iso_register$a'(X0_'A_update_b_update_fun')),
% 4.95/2.49 inference(prop_impl_just,[status(thm)],[c_122,c_165])).
% 4.95/2.49
% 4.95/2.49 tcf(c_473,plain,![X0_'A_update_b_update_fun':'A_update_b_update_fun$']:
% 4.95/2.49 (~'iso_register$a'(X0_'A_update_b_update_fun')|'inj_on$'(X0_'A_update_b_update_fun','top$')),
% 4.95/2.49 inference(renaming,[status(thm)],[c_472])).
% 4.95/2.49
% 4.95/2.49 tcf(c_1675,plain,![X0_'A_update_b_update_fun':'A_update_b_update_fun$',X0_'A_update_c_update_fun':'A_update_c_update_fun$']:
% 4.95/2.49 (~'inj_on$'(X0_'A_update_b_update_fun','top$')|'comp$ab'(X0_'A_update_c_update_fun','fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0_'A_update_b_update_fun')),X0_'A_update_b_update_fun')) = X0_'A_update_c_update_fun'),
% 4.95/2.49 inference(demodulation,[status(thm)],[c_466,c_112])).
% 4.95/2.49
% 4.95/2.49 tcf(c_1686,plain,
% 4.95/2.49 ('fun_app$ae'('fun_app$af'('comp$d','g$'),'comp$ae'('f$','fun_app$x'('fun_app$y'('comp$b','f$a'),'g$a'))) != 'id$'),
% 4.95/2.49 inference(demodulation,[status(thm)],[c_49,c_55])).
% 4.95/2.49
% 4.95/2.49 tcf(c_1687,plain,
% 4.95/2.49 ('fun_app$ae'('fun_app$af'('comp$d','g$'),'comp$aa'('id$b','g$a')) != 'id$'),
% 4.95/2.49 inference(demodulation,[status(thm)],[c_1686,c_50,c_114])).
% 4.95/2.49
% 4.95/2.49 tcf(c_3642,plain,![X0_'A_update_b_update_fun':'A_update_b_update_fun$',X0_'A_update_c_update_fun':'A_update_c_update_fun$']:
% 4.95/2.49 (~'inj_on$'(X0_'A_update_b_update_fun','top$')|'comp$ab'(X0_'A_update_c_update_fun','fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0_'A_update_b_update_fun')),X0_'A_update_b_update_fun')) = X0_'A_update_c_update_fun'),
% 4.95/2.49 inference(prop_impl_just,[status(thm)],[c_1675])).
% 4.95/2.49
% 4.95/2.49 tcf(c_3644,plain,![X0_'A_update_b_update_fun':'A_update_b_update_fun$']:
% 4.95/2.49 ('inj_on$'(X0_'A_update_b_update_fun','top$')|~'iso_register$a'(X0_'A_update_b_update_fun')),
% 4.95/2.49 inference(prop_impl_just,[status(thm)],[c_473])).
% 4.95/2.49
% 4.95/2.49 tcf(c_3645,plain,![X0_'A_update_b_update_fun':'A_update_b_update_fun$']:
% 4.95/2.49 (~'iso_register$a'(X0_'A_update_b_update_fun')|'inj_on$'(X0_'A_update_b_update_fun','top$')),
% 4.95/2.49 inference(renaming,[status(thm)],[c_3644])).
% 4.95/2.49
% 4.95/2.49 tcf(c_10400,plain,![X0_'A_update_b_update_fun':'A_update_b_update_fun$']:
% 4.95/2.49 (~'iso_register$a'(X0_'A_update_b_update_fun')|'fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$',X0_'A_update_b_update_fun')),X0_'A_update_b_update_fun') = 'id$b'),
% 4.95/2.49 inference(superposition,[status(thm)],[c_3645,c_171])).
% 4.95/2.49
% 4.95/2.49 tcf(c_10418,plain,
% 4.95/2.49 ('fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$','f$a')),'f$a') = 'id$b'),
% 4.95/2.49 inference(superposition,[status(thm)],[c_66,c_10400])).
% 4.95/2.49
% 4.95/2.49 tcf(c_10424,plain,
% 4.95/2.49 ('inj_on$'('f$a','top$')),
% 4.95/2.49 inference(superposition,[status(thm)],[c_10418,c_165])).
% 4.95/2.49
% 4.95/2.49 tcf(c_10474,plain,![X0_'B_update_a_update_fun':'B_update_a_update_fun$',X0_'A_update_b_update_fun':'A_update_b_update_fun$',X0_'A_update_c_update_fun':'A_update_c_update_fun$',X0_'C_update_a_update_fun':'C_update_a_update_fun$']:
% 4.95/2.49 ('fun_app$ae'('fun_app$af'('comp$d','comp$aj'('fun_app$v'('fun_app$w'('comp$a',X0_'A_update_c_update_fun'),X0_'B_update_a_update_fun'),X0_'A_update_b_update_fun')),X0_'C_update_a_update_fun') = 'fun_app$ae'('fun_app$af'('comp$d',X0_'A_update_c_update_fun'),'comp$ae'(X0_'B_update_a_update_fun','fun_app$x'('fun_app$y'('comp$b',X0_'A_update_b_update_fun'),X0_'C_update_a_update_fun')))),
% 4.95/2.49 inference(superposition,[status(thm)],[c_56,c_57])).
% 4.95/2.49
% 4.95/2.49 tcf(c_10476,plain,![X0_'B_update_a_update_fun':'B_update_a_update_fun$',X0_'A_update_b_update_fun':'A_update_b_update_fun$',X0_'A_update_c_update_fun':'A_update_c_update_fun$',X0_'C_update_a_update_fun':'C_update_a_update_fun$']:
% 4.95/2.49 ('fun_app$ae'('fun_app$af'('comp$d','comp$ab'(X0_'A_update_c_update_fun','fun_app$ac'('fun_app$ad'('comp$c',X0_'B_update_a_update_fun'),X0_'A_update_b_update_fun'))),X0_'C_update_a_update_fun') = 'fun_app$ae'('fun_app$af'('comp$d',X0_'A_update_c_update_fun'),'comp$aa'('fun_app$ac'('fun_app$ad'('comp$c',X0_'B_update_a_update_fun'),X0_'A_update_b_update_fun'),X0_'C_update_a_update_fun'))),
% 4.95/2.49 inference(light_normalisation,[status(thm)],[c_10474,c_113,c_115])).
% 4.95/2.49
% 4.95/2.49 tcf(c_10576,plain,![X0_'A_update_a_update_fun':'A_update_a_update_fun$']:
% 4.95/2.49 ('fun_app$ac'('fun_app$ad'('comp$c','comp$ad'(X0_'A_update_a_update_fun','inv_into$b'('top$','f$a'))),'f$a') = X0_'A_update_a_update_fun'),
% 4.95/2.49 inference(superposition,[status(thm)],[c_10424,c_167])).
% 4.95/2.49
% 4.95/2.49 tcf(c_10851,plain,![X0_'A_update_a_update_fun':'A_update_a_update_fun$',X0_'A_update_c_update_fun':'A_update_c_update_fun$',X0_'C_update_a_update_fun':'C_update_a_update_fun$']:
% 4.95/2.49 ('fun_app$ae'('fun_app$af'('comp$d','comp$ab'(X0_'A_update_c_update_fun',X0_'A_update_a_update_fun')),X0_'C_update_a_update_fun') = 'fun_app$ae'('fun_app$af'('comp$d',X0_'A_update_c_update_fun'),'comp$aa'(X0_'A_update_a_update_fun',X0_'C_update_a_update_fun'))),
% 4.95/2.49 inference(superposition,[status(thm)],[c_10576,c_10476])).
% 4.95/2.49
% 4.95/2.49 tcf(c_10896,plain,![X0_'A_update_c_update_fun':'A_update_c_update_fun$']:
% 4.95/2.49 ('comp$ab'(X0_'A_update_c_update_fun','fun_app$ac'('fun_app$ad'('comp$c','inv_into$b'('top$','f$a')),'f$a')) = X0_'A_update_c_update_fun'),
% 4.95/2.49 inference(superposition,[status(thm)],[c_10424,c_3642])).
% 4.95/2.49
% 4.95/2.49 tcf(c_10897,plain,![X0_'A_update_c_update_fun':'A_update_c_update_fun$']:
% 4.95/2.49 ('comp$ab'(X0_'A_update_c_update_fun','id$b') = X0_'A_update_c_update_fun'),
% 4.95/2.49 inference(light_normalisation,[status(thm)],[c_10896,c_10418])).
% 4.95/2.49
% 4.95/2.49 tcf(c_15595,plain,![X0_'A_update_c_update_fun':'A_update_c_update_fun$',X0_'C_update_a_update_fun':'C_update_a_update_fun$']:
% 4.95/2.49 ('fun_app$ae'('fun_app$af'('comp$d',X0_'A_update_c_update_fun'),'comp$aa'('id$b',X0_'C_update_a_update_fun')) = 'fun_app$ae'('fun_app$af'('comp$d',X0_'A_update_c_update_fun'),X0_'C_update_a_update_fun')),
% 4.95/2.49 inference(superposition,[status(thm)],[c_10897,c_10851])).
% 4.95/2.49
% 4.95/2.49 tcf(c_15643,plain,
% 4.95/2.49 ('fun_app$ae'('fun_app$af'('comp$d','g$'),'g$a') != 'id$'),
% 4.95/2.49 inference(demodulation,[status(thm)],[c_1687,c_15595])).
% 4.95/2.49
% 4.95/2.49 tcf(c_15644,plain,
% 4.95/2.49 ($false),
% 4.95/2.49 inference(ground_joinability,[status(thm)],[c_15643,c_68])).
% 4.95/2.49
% 4.95/2.49
% 4.95/2.49 % SZS output end CNFRefutation for theBenchmark.p
% 4.95/2.49
% 4.95/2.49
%------------------------------------------------------------------------------