%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ITP383_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 : n026.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 2.25s 1.29s
% Output : CNFRefutation 2.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP383_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.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 18:33:39 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 2.25/1.29 % SZS status Started for theBenchmark.p
% 2.25/1.29 % SZS status Theorem for theBenchmark.p
% 2.25/1.29
% 2.25/1.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.25/1.29
% 2.25/1.29 % ------ iProver source info
% 2.25/1.29
% 2.25/1.29 % git: date: 2026-07-19 20:42:38 +0200
% 2.25/1.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.25/1.29 % git: non_committed_changes: false
% 2.25/1.29
% 2.25/1.29 % ------ Parsing...
% 2.25/1.29 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 2.25/1.29 %
% 2.25/1.29
% 2.25/1.29 % ------ Preprocessing...%
% 2.25/1.29
% 2.25/1.29 % SZS status Theorem for theBenchmark.p
% 2.25/1.29
% 2.25/1.29 % SZS output start CNFRefutation for theBenchmark.p
% 2.25/1.29
% 2.25/1.29 tff(func_def_0, type, 'comp$s': ('A_b_prod_update_b_update_fun$' * 'C_a_prod_update_a_b_prod_update_fun$') > 'C_a_prod_update_b_update_fun$').
% 2.25/1.29 tff(pred_def_1, type, 'register$au': 'D_update_b_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_2, type, 'type_definition$j': ('B_update_d_update_fun$' * 'D_update_b_update_fun$' * 'D_update_set$') > $o).
% 2.25/1.29 tff(pred_def_3, type, 'quotient$a': ('A_update_a_update_bool_fun_fun$' * 'A_update_c_update_fun$' * 'C_update_a_update_fun$' * 'A_update_c_update_bool_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_4, type, 'preregister$n': 'C_update_d_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_5, type, 'pred_fun$': ('C_update_bool_fun$' * 'B_update_bool_fun$' * 'C_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_6, type, 'quotient$l': ('D_update_d_update_bool_fun_fun$' * 'D_update_a_update_fun$' * 'A_update_d_update_fun$' * 'D_update_a_update_bool_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_7, type, 'member$d': ('C_d_prod_update_a_update_fun$' * 'C_d_prod_update_a_update_fun_set$') > $o).
% 2.25/1.29 tff(pred_def_8, type, 'register$ai': 'D_c_prod_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_9, type, 'register$ao': 'D_update_b_d_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_10, type, 'rel_fun$i': ('A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'C_update_a_update_fun_c_update_b_update_fun_fun_d_update_a_update_fun_d_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_d_update_a_update_fun_d_update_b_update_fun_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_11, type, 'register$ay': 'A_update_d_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_12, type, 'separating$c': ('B_itself$' * 'B_update_set$') > $o).
% 2.25/1.29 tff(pred_def_13, type, 'compatible$j': ('B_update_b_update_fun$' * 'A_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_14, type, 'preregister$o': 'C_update_c_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_15, type, 'fun_app$an': ('B_update_bool_fun$' * 'B_update$') > $o).
% 2.25/1.29 tff(pred_def_16, type, 'register$q': 'A_c_prod_update_b_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_17, type, 'fun_app$ai': ('C_update_bool_fun$' * 'C_update$') > $o).
% 2.25/1.29 tff(pred_def_18, type, 'type_definition$b': ('C_update_c_update_fun$' * 'C_update_c_update_fun$' * 'C_update_set$') > $o).
% 2.25/1.29 tff(pred_def_19, type, 'register$m': 'C_c_prod_update_b_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_20, type, 'register$as': 'C_update_b_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_21, type, 'register$ak': 'D_d_prod_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_22, type, 'compatible$n': ('C_update_b_update_fun$' * 'C_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_23, type, 'compatible$x': ('A_update_d_update_fun$' * 'D_update_d_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_24, type, 'register$ax': 'C_update_d_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_25, type, 'preregister$g': 'A_update_c_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_26, type, 'compatible$k': ('D_update_a_update_fun$' * 'A_update_a_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_27, type, 'register$n': 'C_a_prod_update_b_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_28, type, 'fun_app$aj': ('A_update_bool_fun$' * 'A_update$') > $o).
% 2.25/1.29 tff(pred_def_29, type, 'preregister$e': 'B_update_a_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_30, type, 'compatible$z': ('C_update_a_update_fun$' * 'B_update_a_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_31, type, 'register$ap': 'B_update_b_d_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_32, type, 'separating$d': ('B_itself$' * 'A_update_set$') > $o).
% 2.25/1.29 tff(pred_def_33, type, 'compatible$aa': ('C_update_b_update_fun$' * 'B_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_34, type, 'register$aw': 'C_update_d_a_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_35, type, 'register$d': 'B_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_36, type, 'compatible$as': ('A_update_b_a_prod_update_fun$' * 'C_update_b_a_prod_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_37, type, 'separating$': ('A_itself$' * 'D_update_set$') > $o).
% 2.25/1.29 tff(pred_def_38, type, 'register$bi': 'A_update_a_a_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_39, type, 'preregister$': 'C_d_prod_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_40, type, 'fun_app$k': ('C_update_a_update_fun_bool_fun$' * 'C_update_a_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_41, type, 'register$ab': 'A_b_prod_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_42, type, 'register$x': 'C_update_c_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_43, type, 'register$o': 'C_d_prod_update_b_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_44, type, 'quotient$': ('B_update_b_update_bool_fun_fun$' * 'B_update_a_update_fun$' * 'A_update_b_update_fun$' * 'B_update_a_update_bool_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_45, type, 'register$ac': 'A_a_prod_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_46, type, 'preregister$c': 'A_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_47, type, 'quotient$m': ('D_update_d_update_bool_fun_fun$' * 'D_update_b_update_fun$' * 'B_update_d_update_fun$' * 'D_update_b_update_bool_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_48, type, 'type_definition$f': ('A_update_c_update_fun$' * 'C_update_a_update_fun$' * 'C_update_set$') > $o).
% 2.25/1.29 tff(pred_def_49, type, 'quotient$b': ('B_update_b_update_bool_fun_fun$' * 'B_update_c_update_fun$' * 'C_update_b_update_fun$' * 'B_update_c_update_bool_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_50, type, 'compatible$o': ('A_update_b_update_fun$' * 'D_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_51, type, 'compatible$af': ('C_update_d_update_fun$' * 'D_update_d_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_52, type, 'member$f': ('C_update_a_update_fun$' * 'C_update_a_update_fun_set$') > $o).
% 2.25/1.29 tff(pred_def_53, type, 'preregister$b': 'C_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_54, type, 'member$c': ('A_update$' * 'A_update_set$') > $o).
% 2.25/1.29 tff(pred_def_55, type, 'register$bl': 'A_update_a_c_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_56, type, 'register$c': 'C_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_57, type, 'member$g': ('B_update$' * 'B_update_set$') > $o).
% 2.25/1.29 tff(pred_def_58, type, 'compatible$c': ('A_update_b_update_fun$' * 'A_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_59, type, 'register$u': 'C_d_prod_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_60, type, 'register$y': 'A_d_prod_update_a_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_61, type, 'register$al': 'C_update_d_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_62, type, 'quotient$e': ('A_update_a_update_bool_fun_fun$' * 'A_update_d_update_fun$' * 'D_update_a_update_fun$' * 'A_update_d_update_bool_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_63, type, 'register$k': 'C_d_prod_update_a_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_64, type, 'register$s': 'D_update_c_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_65, type, 'preregister$f': 'A_update_d_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_66, type, 'register$be': 'A_update_b_a_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_67, type, 'member$b': ('C_update$' * 'C_update_set$') > $o).
% 2.25/1.29 tff(pred_def_68, type, 'compatible$t': ('B_update_b_update_fun$' * 'C_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_69, type, 'rel_fun$ag': ('A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'D_update_a_update_fun_d_update_b_update_fun_fun_d_update_a_update_fun_d_update_b_update_fun_fun_bool_fun_fun$' * 'A_update_b_update_fun_d_update_a_update_fun_d_update_b_update_fun_fun_fun$' * 'A_update_b_update_fun_d_update_a_update_fun_d_update_b_update_fun_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_70, type, 'register$bd': 'A_update_d_a_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_71, type, 'type_definition$a': ('B_update_b_update_fun$' * 'B_update_b_update_fun$' * 'B_update_set$') > $o).
% 2.25/1.29 tff(pred_def_72, type, 'register$v': 'A_update_d_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_73, type, 'compatible$s': ('B_update_b_update_fun$' * 'D_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_74, type, 'separating$a': ('B_itself$' * 'C_update_set$') > $o).
% 2.25/1.29 tff(pred_def_75, type, 'register$g': 'D_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_76, type, 'register$b': 'A_update_a_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_77, type, 'rel_fun$y': ('A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'D_update_a_update_fun_d_update_b_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$' * 'A_update_b_update_fun_d_update_a_update_fun_d_update_b_update_fun_fun_fun$' * 'A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_78, type, 'register$ag': 'C_c_prod_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_79, type, 'quotient$d': ('B_update_b_update_bool_fun_fun$' * 'B_update_c_d_prod_update_fun$' * 'C_d_prod_update_b_update_fun$' * 'B_update_c_d_prod_update_bool_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_80, type, 'register$bm': 'A_update_a_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_81, type, 'compatible$am': ('C_update_b_b_prod_update_fun$' * 'A_update_b_b_prod_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_82, type, 'register$i': 'C_c_prod_update_a_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_83, type, 'compatible$l': ('B_update_a_update_fun$' * 'A_update_a_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_84, type, 'register$aa': 'A_c_prod_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_85, type, 'quotient$g': ('C_update_c_update_bool_fun_fun$' * 'C_update_a_update_fun$' * 'A_update_c_update_fun$' * 'C_update_a_update_bool_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_86, type, 'rel_fun$': ('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).
% 2.25/1.29 tff(pred_def_87, type, 'compatible$aj': ('C_update_b_a_prod_update_fun$' * 'D_update_b_a_prod_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_88, type, 'compatible$v': ('B_update_d_update_fun$' * 'A_update_d_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_89, type, 'register$bj': 'B_update_b_a_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_90, type, 'quotient$f': ('B_update_b_update_bool_fun_fun$' * 'B_update_d_update_fun$' * 'D_update_b_update_fun$' * 'B_update_d_update_bool_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_91, type, 'register$f': 'B_update_a_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_92, type, 'compatible$ag': ('C_update_a_a_prod_update_fun$' * 'C_update_a_a_prod_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_93, type, 'pred_fun$d': ('D_update_bool_fun$' * 'B_update_bool_fun$' * 'D_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_94, type, 'preregister$p': 'B_update_c_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_95, type, 'register$r': 'D_update_d_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_96, type, 'register$j': 'C_a_prod_update_a_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_97, type, 'quotient$c': ('A_update_a_update_bool_fun_fun$' * 'A_update_c_d_prod_update_fun$' * 'C_d_prod_update_a_update_fun$' * 'A_update_c_d_prod_update_bool_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_98, type, 'compatible$y': ('A_update_c_update_fun$' * 'D_update_c_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_99, type, 'register$aj': 'D_a_prod_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_100, type, 'compatible$aq': ('C_update_a_b_prod_update_fun$' * 'A_update_a_b_prod_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_101, type, 'register$az': 'D_update_d_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_102, type, 'compatible$f': ('C_update_b_update_fun$' * 'D_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_103, type, 'compatible$a': ('A_update_b_update_fun$' * 'C_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_104, type, 'compatible$h': ('D_update_b_update_fun$' * 'C_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_105, type, 'compatible$an': ('C_update_b_b_prod_update_fun$' * 'D_update_b_b_prod_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_106, type, 'register$bc': 'A_update_d_c_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_107, type, 'type_definition$h': ('A_update_d_update_fun$' * 'D_update_a_update_fun$' * 'D_update_set$') > $o).
% 2.25/1.29 tff(pred_def_108, type, 'preregister$m': 'D_update_d_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_109, type, 'compatible$ae': ('C_update_c_update_fun$' * 'D_update_c_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_110, type, 'fun_app$ag': ('C_d_prod_update_bool_fun$' * 'C_d_prod_update$') > $o).
% 2.25/1.29 tff(pred_def_111, type, 'rel_fun$q': ('A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'C_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_c_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_bool_fun_fun$' * 'A_update_b_update_fun_c_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_fun$' * 'A_update_b_update_fun_c_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_112, type, 'register$ar': 'A_update_c_d_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_113, type, 'register$bg': 'C_update_a_c_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_114, type, 'register$t': 'B_update_d_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_115, type, 'compatible$w': ('B_update_c_update_fun$' * 'A_update_c_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_116, type, 'rel_fun$m': ('A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'C_d_prod_update_a_update_fun_c_d_prod_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_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_fun$' * 'A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_117, type, 'register$an': 'A_update_b_d_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_118, type, 'register$bk': 'A_update_a_d_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_119, type, 'rel_fun$ac': ('A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'D_update_a_update_fun_d_update_b_update_fun_fun_c_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_bool_fun_fun$' * 'A_update_b_update_fun_d_update_a_update_fun_d_update_b_update_fun_fun_fun$' * 'A_update_b_update_fun_c_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_120, type, 'compatible$b': ('A_update_b_update_fun$' * 'B_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_121, type, 'rel_fun$u': ('A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'C_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_d_update_a_update_fun_d_update_b_update_fun_fun_bool_fun_fun$' * 'A_update_b_update_fun_c_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_fun$' * 'A_update_b_update_fun_d_update_a_update_fun_d_update_b_update_fun_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_122, type, 'register$bb': 'B_update_d_a_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_123, type, 'fun_app$ah': ('D_update_bool_fun$' * 'D_update$') > $o).
% 2.25/1.29 tff(pred_def_124, type, 'compatible$ab': ('A_update_a_update_fun$' * 'A_update_a_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_125, type, 'pred_fun$b': ('C_d_prod_update_bool_fun$' * 'B_update_bool_fun$' * 'C_d_prod_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_126, type, 'type_definition$c': ('C_update_d_update_fun$' * 'D_update_c_update_fun$' * 'D_update_set$') > $o).
% 2.25/1.29 tff(pred_def_127, type, 'type_definition$i': ('B_update_c_update_fun$' * 'C_update_b_update_fun$' * 'C_update_set$') > $o).
% 2.25/1.29 tff(pred_def_128, type, 'compatible$p': ('D_update_b_update_fun$' * 'A_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_129, type, 'register$h': 'C_c_prod_update_a_a_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_130, type, 'separating$b': ('A_itself$' * 'C_update_set$') > $o).
% 2.25/1.29 tff(pred_def_131, type, 'compatible$i': ('C_update_b_update_fun$' * 'A_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_132, type, 'compatible$ak': ('C_update_a_b_prod_update_fun$' * 'C_update_a_b_prod_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_133, type, 'compatible$ap': ('A_update_b_b_prod_update_fun$' * 'C_update_b_b_prod_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_134, type, 'register$z': 'A_d_prod_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_135, type, 'register$l': 'C_c_prod_update_b_a_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_136, type, 'compatible$ar': ('C_update_a_b_prod_update_fun$' * 'D_update_a_b_prod_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_137, type, 'register$av': 'B_update_b_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_138, type, 'register$p': 'A_c_prod_update_b_a_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_139, type, 'separating$e': ('B_itself$' * 'C_d_prod_update_set$') > $o).
% 2.25/1.29 tff(pred_def_140, type, 'compatible$q': ('D_update_b_update_fun$' * 'D_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_141, type, 'compatible$al': ('C_update_b_b_prod_update_fun$' * 'C_update_b_b_prod_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_142, type, 'register$aq': 'A_update_d_d_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_143, type, 'compatible$ai': ('C_update_b_a_prod_update_fun$' * 'A_update_b_a_prod_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_144, type, 'preregister$l': 'C_d_prod_update_c_d_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_145, type, 'register$am': 'C_update_b_d_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_146, type, 'member$a': ('D_update$' * 'D_update_set$') > $o).
% 2.25/1.29 tff(pred_def_147, type, 'fun_app$aq': ('A_update_b_update_fun_bool_fun$' * 'A_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_148, type, 'quotient$k': ('C_d_prod_update_c_d_prod_update_bool_fun_fun$' * 'C_d_prod_update_b_update_fun$' * 'B_update_c_d_prod_update_fun$' * 'C_d_prod_update_b_update_bool_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_149, type, 'preregister$k': 'B_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_150, type, 'quotient$i': ('C_update_c_update_bool_fun_fun$' * 'C_update_b_update_fun$' * 'B_update_c_update_fun$' * 'C_update_b_update_bool_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_151, type, 'compatible$ac': ('C_update_a_update_fun$' * 'A_update_a_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_152, type, 'type_definition$d': ('D_update_c_update_fun$' * 'C_update_d_update_fun$' * 'C_update_set$') > $o).
% 2.25/1.29 tff(pred_def_153, type, 'register$ba': 'B_update_d_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_154, type, 'register$at': 'A_update_b_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_155, type, 'type_definition$e': ('D_update_d_update_fun$' * 'D_update_d_update_fun$' * 'D_update_set$') > $o).
% 2.25/1.29 tff(pred_def_156, type, 'register$bh': 'B_update_a_b_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_157, type, 'type_definition$': ('A_update_a_update_fun$' * 'A_update_a_update_fun$' * 'A_update_set$') > $o).
% 2.25/1.29 tff(pred_def_158, type, 'member$': ('C_d_prod_update$' * 'C_d_prod_update_set$') > $o).
% 2.25/1.29 tff(pred_def_159, type, 'register$a': 'A_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_160, type, 'quotient$j': ('C_d_prod_update_c_d_prod_update_bool_fun_fun$' * 'C_d_prod_update_a_update_fun$' * 'A_update_c_d_prod_update_fun$' * 'C_d_prod_update_a_update_bool_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_161, type, 'rel_fun$e': ('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_d_prod_update_a_update_fun_c_d_prod_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_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_162, type, 'fun_app$i': ('C_d_prod_update_a_update_fun_bool_fun$' * 'C_d_prod_update_a_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_163, type, 'compatible$e': ('A_update_a_update_fun$' * 'B_update_a_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_164, type, 'preregister$d': 'D_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_165, type, 'member$e': ('D_update_a_update_fun$' * 'D_update_a_update_fun_set$') > $o).
% 2.25/1.29 tff(pred_def_166, type, 'preregister$h': 'A_update_a_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_167, type, 'register$w': 'A_update_c_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_168, type, 'compatible$ah': ('C_update_b_a_prod_update_fun$' * 'C_update_b_a_prod_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_169, type, 'compatible$ao': ('A_update_a_b_prod_update_fun$' * 'C_update_a_b_prod_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_170, type, 'register$ah': 'C_a_prod_update_b_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_171, type, 'compatible$u': ('B_update_b_update_fun$' * 'B_update_b_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_172, type, 'register$ad': 'A_b_prod_update_a_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_173, type, 'less_eq$': ('A_update_set$' * 'A_update_set$') > $o).
% 2.25/1.29 tff(pred_def_174, type, 'quotient$h': ('A_update_a_update_bool_fun_fun$' * 'A_update_b_update_fun$' * 'B_update_a_update_fun$' * 'A_update_b_update_bool_fun_fun$') > $o).
% 2.25/1.29 tff(pred_def_175, type, 'register$bf': 'D_update_a_d_prod_update_fun$' > $o).
% 2.25/1.29 tff(pred_def_176, type, 'type_definition$g': ('B_update_a_update_fun$' * 'A_update_b_update_fun$' * 'A_update_set$') > $o).
% 2.25/1.29 tff(pred_def_177, type, 'fun_app$j': ('D_update_a_update_fun_bool_fun$' * 'D_update_a_update_fun$') > $o).
% 2.25/1.29 tff(pred_def_178, type, 'register$af': 'C_c_prod_update_a_update_fun$' > $o).
% 2.25/1.29 tff(func_def_179, type, 'fun_app$m': ('D_update_b_update_fun$' * 'D_update$') > 'B_update$').
% 2.25/1.29 tff(func_def_180, type, 'register_pair$n': ('B_update_a_update_fun$' * 'A_update_a_update_fun$' * 'B_a_prod_update$') > 'A_update$').
% 2.25/1.29 tff(func_def_181, type, 'fun_app$cz': ('C_update_c_d_prod_update_fun$' * 'C_update$') > 'C_d_prod_update$').
% 2.25/1.29 tff(func_def_182, type, 'comp$bq': ('A_update_a_update_prod_b_update_b_update_prod_fun$' * 'C_update_a_update_a_update_prod_fun$') > 'C_update_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_183, type, 'register_pair$v': ('A_update_b_b_prod_update_fun$' * 'C_update_b_b_prod_update_fun$') > 'A_c_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_184, type, 'type$': 'B_itself$').
% 2.25/1.29 tff(func_def_185, type, 'rel_fun$aa': ('D_update_c_update_bool_fun_fun$' * 'A_update_a_update_bool_fun_fun$') > 'D_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_186, type, 'rel_fun$ai': ('D_update_d_update_bool_fun_fun$' * 'A_update_a_update_bool_fun_fun$') > 'D_update_a_update_fun_d_update_a_update_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_187, type, 'top$a': 'D_update_set$').
% 2.25/1.29 tff(func_def_188, type, 'fun_app$cb': ('B_update_c_update_fun$' * 'B_update$') > 'C_update$').
% 2.25/1.29 tff(func_def_189, type, 'rel_fun$af': ('D_update_c_d_prod_update_bool_fun_fun$' * 'B_update_b_update_bool_fun_fun$') > 'D_update_b_update_fun_c_d_prod_update_b_update_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_190, type, 'top$': 'C_d_prod_update_set$').
% 2.25/1.29 tff(func_def_191, type, 'map_prod$': ('A_update_b_update_fun$' * 'A_update_b_update_fun$') > 'A_update_a_update_prod_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_192, type, 'uwd$': 'A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_193, type, 'fcomp$': ('B_update_d_update_fun_a_update_a_update_fun_fun$' * 'A_update_a_update_fun_d_update_b_update_fun_fun$') > 'B_update_d_update_fun_d_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_194, type, 'comp$ca': ('A_update_a_update_prod_b_update_b_update_prod_fun$' * 'D_update_c_update_prod_a_update_a_update_prod_fun$') > 'D_update_c_update_prod_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_195, type, 'uus$': 'A_update_b_update_fun$' > 'A_update_d_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_196, type, 'uvs$': 'B_update$' > 'A_update_b_update_fun$').
% 2.25/1.29 tff(func_def_197, type, 'comp$aa': ('A_a_prod_update_b_b_prod_update_fun$' * 'D_d_prod_update_a_a_prod_update_fun$') > 'D_d_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_198, type, 'rel_fun$b': ('C_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$' * 'C_update_b_update_fun_c_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$').
% 2.25/1.29 tff(func_def_199, type, 'id_update$a': 'D_update$').
% 2.25/1.29 tff(func_def_200, type, 'comp$e': ('C_update_a_update_fun$' * 'C_update_c_update_fun$') > 'C_update_a_update_fun$').
% 2.25/1.29 tff(func_def_201, type, 'fun_app$au': ('D_update_a_update_fun$' * 'D_update$') > 'A_update$').
% 2.25/1.29 tff(func_def_202, type, 'fun_app$bz': ('C_d_prod_update_b_update_fun$' * 'C_d_prod_update$') > 'B_update$').
% 2.25/1.29 tff(func_def_203, type, 'register_tensor$o': ('A_update_b_update_fun$' * 'D_update_a_update_fun$') > 'A_d_prod_update_b_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_204, type, 'comp$bx': ('A_update_a_update_prod_b_update_b_update_prod_fun$' * 'C_d_prod_update_c_update_prod_a_update_a_update_prod_fun$') > 'C_d_prod_update_c_update_prod_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_205, type, 'comp$ak': ('C_update_a_update_fun$' * 'A_update_c_update_fun$') > 'A_update_a_update_fun$').
% 2.25/1.29 tff(func_def_206, type, 'comp$at': ('A_update_a_update_fun$' * 'D_update_a_update_fun$') > 'D_update_a_update_fun$').
% 2.25/1.29 tff(func_def_207, type, 'comp$ai': ('A_a_prod_update_b_b_prod_update_fun$' * 'C_d_prod_c_d_prod_prod_update_a_a_prod_update_fun$') > 'C_d_prod_c_d_prod_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_208, type, 'comp$d': ('B_update_b_update_fun$' * 'C_update_b_update_fun$') > 'C_update_b_update_fun$').
% 2.25/1.29 tff(func_def_209, type, 'rel_fun$ak': ('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$').
% 2.25/1.29 tff(func_def_210, type, 'uwb$': 'A_update_set$' > 'C_d_prod_update_a_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_211, type, 'comp$u': ('B_a_prod_update_b_update_fun$' * 'A_d_prod_update_b_a_prod_update_fun$') > 'A_d_prod_update_b_update_fun$').
% 2.25/1.29 tff(func_def_212, type, 'fun_app$as': ('D_update_d_b_prod_update_fun$' * 'D_update$') > 'D_b_prod_update$').
% 2.25/1.29 tff(func_def_213, type, 'register_pair$d': ('D_update_b_update_fun$' * 'C_update_b_update_fun$') > 'D_c_prod_update_b_update_fun$').
% 2.25/1.29 tff(func_def_214, type, 'comp$aj': ('C_c_prod_update_a_a_prod_update_fun$' * 'A_a_prod_update_c_c_prod_update_fun$') > 'A_a_prod_update_a_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_215, type, 'comp$aw': ('A_update_a_update_fun_c_update_b_update_fun_fun$' * 'B_update_c_d_prod_update_fun_a_update_a_update_fun_fun$') > 'B_update_c_d_prod_update_fun_c_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_216, type, 'uux$': 'A_update_c_update_fun$' > 'A_update_d_c_prod_update_fun$').
% 2.25/1.29 tff(func_def_217, type, 'fun_app$az': ('B_update_a_update_fun$' * 'B_update$') > 'A_update$').
% 2.25/1.29 tff(func_def_218, type, 'uvq$': 'A_update_b_update_fun$' > 'A_update_a_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_219, type, 'register_tensor$m': ('D_update_a_update_fun$' * 'A_update_b_update_fun$') > 'D_a_prod_update_a_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_220, type, 'comp$bl': ('A_update_b_update_b_update_prod_fun$' * 'D_update_a_update_fun$') > 'D_update_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_221, type, 'compatible$': 'C_update_a_update_fun$' > 'D_update_a_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_222, type, 'comp$ay': ('A_update_a_update_fun_c_update_b_update_fun_fun$' * 'B_update_c_update_fun_a_update_a_update_fun_fun$') > 'B_update_c_update_fun_c_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_223, type, 'uvw$': ('A_update_b_update_fun$' * 'A_update_b_update_fun$') > 'A_update_bool_fun$').
% 2.25/1.29 tff(func_def_224, type, 'map_fun$h': ('C_d_prod_update_b_update_fun$' * 'C_update_b_update_fun$') > 'B_update_c_update_fun_c_d_prod_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_225, type, 'map_prod$a': ('C_update_b_update_fun$' * 'C_update_b_update_fun$') > 'C_update_c_update_prod_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_226, type, 'fun_app$c': ('D_update_a_d_prod_update_fun$' * 'D_update$') > 'A_d_prod_update$').
% 2.25/1.29 tff(func_def_227, type, 'fun_app$ar': ('A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$' * 'A_update_b_update_fun$') > 'A_update_b_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_228, type, 'fun_app$de': ('C_update_c_d_prod_update_prod_b_update_b_update_prod_fun$' * 'C_update_c_d_prod_update_prod$') > 'B_update_b_update_prod$').
% 2.25/1.29 tff(func_def_229, type, 'fun_app$ce': ('C_d_prod_update_c_d_prod_update_fun$' * 'C_d_prod_update$') > 'C_d_prod_update$').
% 2.25/1.29 tff(func_def_230, type, 'relcompp$d': ('B_update_a_update_bool_fun_fun$' * 'A_update_d_update_bool_fun_fun$') > 'B_update_d_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_231, type, 'fun_app$cr': ('B_update_c_update_fun_a_update_a_update_fun_fun$' * 'B_update_c_update_fun$') > 'A_update_a_update_fun$').
% 2.25/1.29 tff(func_def_232, type, 'register_tensor$f': ('C_update_b_update_fun$' * 'A_update_b_update_fun$') > 'C_a_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_233, type, 'fun_app$dy': ('B_update_set_b_update_fun$' * 'B_update_set$') > 'B_update$').
% 2.25/1.29 tff(func_def_234, type, 'comp$bk': ('A_update_b_update_b_update_prod_fun$' * 'C_d_prod_update_a_update_fun$') > 'C_d_prod_update_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_235, type, 'fun_app$aw': ('C_update_d_a_prod_update_fun$' * 'C_update$') > 'D_a_prod_update$').
% 2.25/1.29 tff(func_def_236, type, 'uve$': 'A_update_a_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_237, type, 'top$c': 'A_update_set$').
% 2.25/1.29 tff(func_def_238, type, 'comp$ac': ('A_a_prod_update_b_b_prod_update_fun$' * 'C_d_prod_update_a_a_prod_update_fun$') > 'C_d_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_239, type, 'register_pair$b': ('A_update_b_update_fun$' * 'A_update_b_update_fun$') > 'A_a_prod_update_b_update_fun$').
% 2.25/1.29 tff(func_def_240, type, 'uvf$': 'D_update_b_update_fun$' > 'D_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_241, type, 'fun_app$cl': ('D_a_prod_update_b_update_fun$' * 'D_a_prod_update$') > 'B_update$').
% 2.25/1.29 tff(func_def_242, type, 'comp$t': ('B_a_prod_update_b_update_fun$' * 'C_c_prod_update_b_a_prod_update_fun$') > 'C_c_prod_update_b_update_fun$').
% 2.25/1.29 tff(func_def_243, type, 'rel_fun$h': ('C_update_c_d_prod_update_bool_fun_fun$' * 'B_update_b_update_bool_fun_fun$') > 'C_update_b_update_fun_c_d_prod_update_b_update_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_244, type, 'collect$': 'C_d_prod_update_bool_fun$' > 'C_d_prod_update_set$').
% 2.25/1.29 tff(func_def_245, type, 'fun_app$bl': ('C_c_prod_update_a_a_prod_update_fun$' * 'C_c_prod_update$') > 'A_a_prod_update$').
% 2.25/1.29 tff(func_def_246, type, 'rel_fun$al': ('C_d_prod_update_c_d_prod_update_bool_fun_fun$' * 'A_update_b_update_bool_fun_fun$') > 'C_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_247, type, 'fun_app$t': ('C_update_a_b_prod_update_fun$' * 'C_update$') > 'A_b_prod_update$').
% 2.25/1.29 tff(func_def_248, type, 'fun_app$b': ('A_update_a_d_prod_update_fun$' * 'A_update$') > 'A_d_prod_update$').
% 2.25/1.29 tff(func_def_249, type, 'comp_update$m': 'C_d_prod_update$' > 'C_d_prod_update_c_d_prod_update_fun$').
% 2.25/1.29 tff(func_def_250, type, 'comp$ap': ('B_update_a_update_fun$' * 'D_update_b_update_fun$') > 'D_update_a_update_fun$').
% 2.25/1.29 tff(func_def_251, type, 'register_pair$j': ('A_update_b_update_fun$' * 'D_update_b_update_fun$') > 'A_d_prod_update_b_update_fun$').
% 2.25/1.29 tff(func_def_252, type, 'comp$z': ('C_update_b_update_fun$' * 'B_update_c_update_fun$') > 'B_update_b_update_fun$').
% 2.25/1.29 tff(func_def_253, type, 'convol$d': ('C_d_prod_update_b_update_fun$' * 'C_d_prod_update_b_update_fun$') > 'C_d_prod_update_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_254, type, 'comp$bh': ('C_update_a_update_a_update_prod_fun$' * 'C_update_c_update_fun$') > 'C_update_a_update_a_update_prod_fun$').
% 2.25/1.29 tff(func_def_255, type, 'fun_app$bw': ('A_update_b_update_fun_d_update_a_update_fun_d_update_b_update_fun_fun_fun$' * 'A_update_b_update_fun$') > 'D_update_a_update_fun_d_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_256, type, 'comp$bu': ('A_update_a_update_prod_b_update_b_update_prod_fun$' * 'C_update_c_update_prod_a_update_a_update_prod_fun$') > 'C_update_c_update_prod_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_257, type, 'compatible$ad': 'D_update_a_update_fun$' > 'D_update_a_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_258, type, 'tensor_update$m': ('C_update$' * 'A_update$') > 'C_a_prod_update$').
% 2.25/1.29 tff(func_def_259, type, 'conversep$a': 'C_update_a_update_bool_fun_fun$' > 'A_update_c_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_260, type, 'relcompp$c': ('B_update_a_update_bool_fun_fun$' * 'A_update_c_d_prod_update_bool_fun_fun$') > 'B_update_c_d_prod_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_261, type, 'collect$f': 'C_update_a_update_fun_bool_fun$' > 'C_update_a_update_fun_set$').
% 2.25/1.29 tff(func_def_262, type, 'fun_app$x': ('B_update_b_update_fun$' * 'B_update$') > 'B_update$').
% 2.25/1.29 tff(func_def_263, type, 'comp$br': ('A_update_a_update_prod_b_update_b_update_prod_fun$' * 'C_d_prod_update_a_update_a_update_prod_fun$') > 'C_d_prod_update_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_264, type, 'id_update$': 'A_update$').
% 2.25/1.29 tff(func_def_265, type, 'convol$a': ('A_update_b_update_fun$' * 'A_update_b_update_fun$') > 'A_update_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_266, type, 'pred_fun$e': ('D_update_bool_fun$' * 'A_update_bool_fun$') > 'D_update_a_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_267, type, 'rel_fun$w': ('C_d_prod_update_d_update_bool_fun_fun$' * 'A_update_a_update_bool_fun_fun$') > 'C_d_prod_update_a_update_fun_d_update_a_update_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_268, type, 'conversep$b': 'C_d_prod_update_a_update_bool_fun_fun$' > 'A_update_c_d_prod_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_269, type, 'comp_update$f': ('B_c_prod_update$' * 'B_c_prod_update$') > 'B_c_prod_update$').
% 2.25/1.29 tff(func_def_270, type, 'relcompp$e': ('C_update_a_update_bool_fun_fun$' * 'A_update_c_update_bool_fun_fun$') > 'C_update_c_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_271, type, 'map_prod$l': ('C_d_prod_update_a_update_fun$' * 'D_update_a_update_fun$') > 'C_d_prod_update_d_update_prod_a_update_a_update_prod_fun$').
% 2.25/1.29 tff(func_def_272, type, 'collect$b': 'C_update_bool_fun$' > 'C_update_set$').
% 2.25/1.29 tff(func_def_273, type, 'register_pair$g': ('C_update_b_update_fun$' * 'C_update_b_update_fun$') > 'C_c_prod_update_b_update_fun$').
% 2.25/1.29 tff(func_def_274, type, 'fun_app$': ('B_update_b_a_prod_update_fun$' * 'B_update$') > 'B_a_prod_update$').
% 2.25/1.29 tff(func_def_275, type, 'comp$bf': ('C_update_b_update_b_update_prod_fun$' * 'A_update_c_update_fun$') > 'A_update_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_276, type, 'map_fun$a': ('A_update_b_update_fun$' * 'C_update_a_update_fun$') > 'B_update_c_update_fun_a_update_a_update_fun_fun$').
% 2.25/1.29 tff(func_def_277, type, 'uvx$': 'C_update_c_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_278, type, 'compatible$m': 'C_update_a_update_fun$' > 'C_update_a_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_279, type, 'rel_fun$ah': ('D_update_a_update_fun_d_update_a_update_fun_bool_fun_fun$' * 'D_update_b_update_fun_d_update_b_update_fun_bool_fun_fun$') > 'D_update_a_update_fun_d_update_b_update_fun_fun_d_update_a_update_fun_d_update_b_update_fun_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_280, type, 'comp$ae': ('A_a_prod_update_b_b_prod_update_fun$' * 'C_d_prod_d_prod_update_a_a_prod_update_fun$') > 'C_d_prod_d_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_281, type, 'fun_app$dn': ('D_update_c_update_prod_a_update_a_update_prod_fun$' * 'D_update_c_update_prod$') > 'A_update_a_update_prod$').
% 2.25/1.29 tff(func_def_282, type, 'fun_app$bc': ('A_update_d_a_prod_update_fun$' * 'A_update$') > 'D_a_prod_update$').
% 2.25/1.29 tff(func_def_283, type, 'relcompp$g': ('C_update_a_update_bool_fun_fun$' * 'A_update_b_update_bool_fun_fun$') > 'C_update_b_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_284, type, 'map_fun$e': ('A_update_b_update_fun$' * 'D_update_a_update_fun$') > 'B_update_d_update_fun_a_update_a_update_fun_fun$').
% 2.25/1.29 tff(func_def_285, type, 'uuf$': 'C_update_a_update_fun_set$' > 'C_update_a_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_286, type, 'register_tensor$r': ('D_update_b_update_fun$' * 'C_update_b_update_fun$') > 'D_c_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_287, type, 'image$f': ('A_update_b_update_fun$' * 'A_update_set$') > 'B_update_set$').
% 2.25/1.29 tff(func_def_288, type, 'uud$': 'D_update_a_update_fun_set$' > 'D_update_a_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_289, type, 'conversep$c': 'D_update_a_update_bool_fun_fun$' > 'A_update_d_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_290, type, 'uvd$': 'A_update_a_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_291, type, 'fun_app$n': ('D_update_b_b_prod_update_fun$' * 'D_update$') > 'B_b_prod_update$').
% 2.25/1.29 tff(func_def_292, type, 'fun_app$cq': ('B_update_c_update_fun_d_update_b_update_fun_fun$' * 'B_update_c_update_fun$') > 'D_update_b_update_fun$').
% 2.25/1.29 tff(func_def_293, type, 'uuc$': 'A_update_set$' > 'A_update_bool_fun$').
% 2.25/1.29 tff(func_def_294, type, 'h$': 'D_update_a_update_fun$').
% 2.25/1.29 tff(func_def_295, type, 'register_tensor$ac': ('C_d_prod_update_b_update_fun$' * 'C_d_prod_update_b_update_fun$') > 'C_d_prod_c_d_prod_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_296, type, 'fun_app$da': ('A_update_a_update_prod_b_update_b_update_prod_fun$' * 'A_update_a_update_prod$') > 'B_update_b_update_prod$').
% 2.25/1.29 tff(func_def_297, type, 'comp$az': ('C_d_prod_update_a_update_fun$' * 'C_update_c_d_prod_update_fun$') > 'C_update_a_update_fun$').
% 2.25/1.29 tff(func_def_298, type, 'comp$y': ('D_update_a_update_fun$' * 'C_update_d_update_fun$') > 'C_update_a_update_fun$').
% 2.25/1.29 tff(func_def_299, type, 'fun_app$dr': ('D_update_d_update_prod_a_update_a_update_prod_fun$' * 'D_update_d_update_prod$') > 'A_update_a_update_prod$').
% 2.25/1.29 tff(func_def_300, type, 'uvb$': 'A_update_a_d_prod_update_fun$').
% 2.25/1.29 tff(func_def_301, type, 'register_tensor$c': ('C_update_a_update_fun$' * 'D_update_b_update_fun$') > 'C_d_prod_update_a_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_302, type, 'tensor_update$b': 'A_update$' > 'C_update_a_c_prod_update_fun$').
% 2.25/1.29 tff(func_def_303, type, 'uva$': 'B_update_b_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_304, type, 'comp$bs': ('A_update_a_update_prod_b_update_b_update_prod_fun$' * 'D_update_a_update_a_update_prod_fun$') > 'D_update_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_305, type, 'fun_app$ao': ('B_update_b_update_bool_fun_fun$' * 'B_update$') > 'B_update_bool_fun$').
% 2.25/1.29 tff(func_def_306, type, 'register_pair$r': ('A_update_c_update_fun$' * 'D_update_c_update_fun$' * 'A_d_prod_update$') > 'C_update$').
% 2.25/1.29 tff(func_def_307, type, 'uwf$': 'B_update_b_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_308, type, 'fun_app$bs': ('C_d_prod_update_b_b_prod_update_fun$' * 'C_d_prod_update$') > 'B_b_prod_update$').
% 2.25/1.29 tff(func_def_309, type, 'comp$bo': ('A_update_a_update_fun_c_d_prod_update_b_update_fun_fun$' * 'B_update_d_update_fun_a_update_a_update_fun_fun$') > 'B_update_d_update_fun_c_d_prod_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_310, type, 'map_prod$p': ('D_update_a_update_fun$' * 'C_d_prod_update_a_update_fun$') > 'D_update_c_d_prod_update_prod_a_update_a_update_prod_fun$').
% 2.25/1.29 tff(func_def_311, type, 'comp_update$b': 'D_update$' > 'D_update_d_update_fun$').
% 2.25/1.29 tff(func_def_312, type, 'comp_update$g': ('D_b_prod_update$' * 'D_b_prod_update$') > 'D_b_prod_update$').
% 2.25/1.29 tff(func_def_313, type, 'fun_app$dg': ('C_update_d_update_prod_b_update_b_update_prod_fun$' * 'C_update_d_update_prod$') > 'B_update_b_update_prod$').
% 2.25/1.29 tff(func_def_314, type, 'fun_app$ds': ('D_update_d_update_prod_b_update_b_update_prod_fun$' * 'D_update_d_update_prod$') > 'B_update_b_update_prod$').
% 2.25/1.29 tff(func_def_315, type, 'image$e': ('D_update_b_update_fun$' * 'D_update_set$') > 'B_update_set$').
% 2.25/1.29 tff(func_def_316, type, 'top$b': 'C_update_set$').
% 2.25/1.29 tff(func_def_317, type, 'register_tensor$': ('C_update_a_update_fun$' * 'C_update_a_update_fun$') > 'C_c_prod_update_a_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_318, type, 'uvu$': 'C_d_prod_update_bool_fun$').
% 2.25/1.29 tff(func_def_319, type, 'comp$bc': ('C_update_a_update_fun$' * 'C_d_prod_update_c_update_fun$') > 'C_d_prod_update_a_update_fun$').
% 2.25/1.29 tff(func_def_320, type, 'fun_app$ae': ('A_update_b_update_fun$' * 'A_update$') > 'B_update$').
% 2.25/1.29 tff(func_def_321, type, 'image$d': ('C_d_prod_update_b_update_fun$' * 'C_d_prod_update_set$') > 'B_update_set$').
% 2.25/1.29 tff(func_def_322, type, 'comp$bj': ('A_update_b_update_b_update_prod_fun$' * 'C_update_a_update_fun$') > 'C_update_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_323, type, 'register_tensor$aa': ('C_update_b_update_fun$' * 'C_d_prod_update_b_update_fun$') > 'C_c_d_prod_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_324, type, 'uua$': 'D_update_set$' > 'D_update_bool_fun$').
% 2.25/1.29 tff(func_def_325, type, 'uuv$': 'B_update_a_update_fun$' > 'B_update_d_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_326, type, 'map_prod$j': ('C_d_prod_update_a_update_fun$' * 'C_d_prod_update_a_update_fun$') > 'C_d_prod_update_c_d_prod_update_prod_a_update_a_update_prod_fun$').
% 2.25/1.29 tff(func_def_327, type, 'fun_app$ac': ('A_update_c_update_fun$' * 'A_update$') > 'C_update$').
% 2.25/1.29 tff(func_def_328, type, 'fun_app$cs': ('B_update_c_d_prod_update_fun_c_update_b_update_fun_fun$' * 'B_update_c_d_prod_update_fun$') > 'C_update_b_update_fun$').
% 2.25/1.29 tff(func_def_329, type, 'uvy$': 'C_d_prod_update_c_d_prod_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_330, type, 'comp$bd': ('A_update_a_update_fun$' * 'C_d_prod_update_a_update_fun$') > 'C_d_prod_update_a_update_fun$').
% 2.25/1.29 tff(func_def_331, type, 'register_pair$l': ('A_update_b_update_fun$' * 'C_update_b_update_fun$') > 'A_c_prod_update_b_update_fun$').
% 2.25/1.29 tff(func_def_332, type, 'map_fun$c': ('A_update_b_update_fun$' * 'C_d_prod_update_a_update_fun$') > 'B_update_c_d_prod_update_fun_a_update_a_update_fun_fun$').
% 2.25/1.29 tff(func_def_333, type, 'register_pair$p': ('B_update_c_update_fun$' * 'A_update_c_update_fun$' * 'B_a_prod_update$') > 'C_update$').
% 2.25/1.29 tff(func_def_334, type, 'tensor_update$l': ('C_update$' * 'C_update$') > 'C_c_prod_update$').
% 2.25/1.29 tff(func_def_335, type, 'grp$': ('A_update_set$' * 'A_update_b_update_fun$') > 'A_update_b_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_336, type, 'comp$cd': ('A_update_c_update_fun$' * 'B_update_a_update_fun$') > 'B_update_c_update_fun$').
% 2.25/1.29 tff(func_def_337, type, 'uvo$': 'C_update_b_update_fun$' > 'C_update_a_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_338, type, 'fun_app$dj': ('C_d_prod_update_c_d_prod_update_prod_a_update_a_update_prod_fun$' * 'C_d_prod_update_c_d_prod_update_prod$') > 'A_update_a_update_prod$').
% 2.25/1.29 tff(func_def_339, type, 'fun_app$r': ('C_update_b_b_prod_update_fun$' * 'C_update$') > 'B_b_prod_update$').
% 2.25/1.29 tff(func_def_340, type, 'comp$ad': ('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$').
% 2.25/1.29 tff(func_def_341, type, 'map_fun$': ('C_update_a_update_fun$' * 'A_update_b_update_fun$') > 'A_update_a_update_fun_c_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_342, type, 'register_pair$c': ('D_update_b_update_fun$' * 'D_update_b_update_fun$') > 'D_d_prod_update_b_update_fun$').
% 2.25/1.29 tff(func_def_343, type, 'image$c': ('C_update_b_update_fun$' * 'C_update_set$') > 'B_update_set$').
% 2.25/1.29 tff(func_def_344, type, 'comp$l': ('A_a_prod_update_b_update_fun$' * 'D_c_prod_update_a_a_prod_update_fun$') > 'D_c_prod_update_b_update_fun$').
% 2.25/1.29 tff(func_def_345, type, 'fun_app$q': ('C_update_b_update_fun$' * 'C_update$') > 'B_update$').
% 2.25/1.29 tff(func_def_346, type, 'register_tensor$i': ('A_update_b_update_fun$' * 'C_update_b_update_fun$') > 'A_c_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_347, type, 'register_tensor$g': ('C_update_b_update_fun$' * 'D_update_b_update_fun$') > 'C_d_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_348, type, 'map_prod$n': ('D_update_a_update_fun$' * 'C_update_a_update_fun$') > 'D_update_c_update_prod_a_update_a_update_prod_fun$').
% 2.25/1.29 tff(func_def_349, type, 'uuu$': 'B_update_b_update_fun$' > 'B_update_d_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_350, type, 'rel_fun$a': ('A_update_a_update_bool_fun_fun$' * 'B_update_b_update_bool_fun_fun$') > 'A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_351, type, 'map_fun$j': ('C_d_prod_update_b_update_fun$' * 'D_update_b_update_fun$') > 'B_update_d_update_fun_c_d_prod_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_352, type, 'register_pair$s': ('C_update_a_update_fun$' * 'C_update_a_update_fun$') > 'C_c_prod_update_a_update_fun$').
% 2.25/1.29 tff(func_def_353, type, 'compatible$d': 'A_update_a_update_fun$' > 'D_update_a_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_354, type, 'map_fun$f': ('C_update_b_update_fun$' * 'D_update_b_update_fun$') > 'B_update_d_update_fun_c_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_355, type, 'register_tensor$ae': ('A_update_a_update_fun$' * 'A_update_a_update_fun$') > 'A_a_prod_update_a_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_356, type, 'fun_app$cu': ('B_update_c_d_prod_update_fun_a_update_a_update_fun_fun$' * 'B_update_c_d_prod_update_fun$') > 'A_update_a_update_fun$').
% 2.25/1.29 tff(func_def_357, type, 'fun_app$h': ('A_update_a_a_prod_update_fun$' * 'A_update$') > 'A_a_prod_update$').
% 2.25/1.29 tff(func_def_358, type, 'comp$cb': ('A_update_a_update_prod_b_update_b_update_prod_fun$' * 'D_update_c_d_prod_update_prod_a_update_a_update_prod_fun$') > 'D_update_c_d_prod_update_prod_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_359, type, 'comp_update$c': 'C_update$' > 'C_update_c_update_fun$').
% 2.25/1.29 tff(func_def_360, type, 'comp$bm': ('A_update_a_update_fun_c_d_prod_update_b_update_fun_fun$' * 'B_update_c_update_fun_a_update_a_update_fun_fun$') > 'B_update_c_update_fun_c_d_prod_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_361, type, 'rel_fun$ad': ('D_update_a_update_fun_c_d_prod_update_a_update_fun_bool_fun_fun$' * 'D_update_b_update_fun_c_d_prod_update_b_update_fun_bool_fun_fun$') > 'D_update_a_update_fun_d_update_b_update_fun_fun_c_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_362, type, 'fun_app$av': ('C_update_d_b_prod_update_fun$' * 'C_update$') > 'D_b_prod_update$').
% 2.25/1.29 tff(func_def_363, type, 'register_tensor$j': ('D_update_a_update_fun$' * 'D_update_a_update_fun$') > 'D_d_prod_update_a_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_364, type, 'fun_app$bd': ('A_update_a_update_fun$' * 'A_update$') > 'A_update$').
% 2.25/1.29 tff(func_def_365, type, 'comp$bw': ('A_update_a_update_prod_b_update_b_update_prod_fun$' * 'C_update_d_update_prod_a_update_a_update_prod_fun$') > 'C_update_d_update_prod_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_366, type, 'comp$': 'A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$').
% 2.25/1.29 tff(func_def_367, type, 'comp$ag': ('A_a_prod_update_b_b_prod_update_fun$' * 'C_d_prod_c_prod_update_a_a_prod_update_fun$') > 'C_d_prod_c_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_368, type, 'fun_app$cv': ('B_update_d_update_fun_c_update_b_update_fun_fun$' * 'B_update_d_update_fun$') > 'C_update_b_update_fun$').
% 2.25/1.29 tff(func_def_369, type, 'fun_app$dh': ('C_d_prod_update_c_update_prod_a_update_a_update_prod_fun$' * 'C_d_prod_update_c_update_prod$') > 'A_update_a_update_prod$').
% 2.25/1.29 tff(func_def_370, type, 'relcompp$b': ('B_update_a_update_bool_fun_fun$' * 'A_update_c_update_bool_fun_fun$') > 'B_update_c_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_371, type, 'uuy$': 'A_update_a_update_fun$' > 'A_update_d_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_372, type, 'comp$au': ('A_update_a_update_fun_d_update_b_update_fun_fun$' * 'B_update_d_update_fun_a_update_a_update_fun_fun$') > 'B_update_d_update_fun_d_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_373, type, 'rel_fun$o': ('C_d_prod_update_c_update_bool_fun_fun$' * 'A_update_a_update_bool_fun_fun$') > 'C_d_prod_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_374, type, 'map_prod$f': ('C_update_a_update_fun$' * 'D_update_a_update_fun$') > 'C_update_d_update_prod_a_update_a_update_prod_fun$').
% 2.25/1.29 tff(func_def_375, type, 'uul$': 'A_update_c_update_fun$' > 'A_update_c_d_prod_update_fun$').
% 2.25/1.29 tff(func_def_376, type, 'map_prod$b': ('C_update_a_update_fun$' * 'C_update_a_update_fun$') > 'C_update_c_update_prod_a_update_a_update_prod_fun$').
% 2.25/1.29 tff(func_def_377, type, 'comp$ax': ('A_update_a_update_fun_c_update_b_update_fun_fun$' * 'B_update_d_update_fun_a_update_a_update_fun_fun$') > 'B_update_d_update_fun_c_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_378, type, 'map_prod$d': ('C_update_a_update_fun$' * 'C_d_prod_update_a_update_fun$') > 'C_update_c_d_prod_update_prod_a_update_a_update_prod_fun$').
% 2.25/1.29 tff(func_def_379, type, 'fcomp$a': ('B_update_c_update_fun_a_update_a_update_fun_fun$' * 'A_update_a_update_fun_d_update_b_update_fun_fun$') > 'B_update_c_update_fun_d_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_380, type, 'comp$af': ('A_a_prod_update_b_b_prod_update_fun$' * 'D_c_d_prod_prod_update_a_a_prod_update_fun$') > 'D_c_d_prod_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_381, type, 'uug$': 'C_update_b_update_fun$' > 'C_update_b_d_prod_update_fun$').
% 2.25/1.29 tff(func_def_382, type, 'compatible$g': 'D_update_a_update_fun$' > 'C_update_a_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_383, type, 'tensor_update$j': ('D_update$' * 'A_update$') > 'D_a_prod_update$').
% 2.25/1.29 tff(func_def_384, type, 'fun_app$bj': ('C_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun$' * 'C_d_prod_update_a_update_fun$') > 'C_d_prod_update_b_update_fun$').
% 2.25/1.29 tff(func_def_385, type, 'fun_app$by': ('C_d_prod_update_a_update_fun$' * 'C_d_prod_update$') > 'A_update$').
% 2.25/1.29 tff(func_def_386, type, 'register_pair$x': ('A_update_b_b_prod_update_fun$' * 'A_update_b_b_prod_update_fun$') > 'A_a_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_387, type, 'map_fun$b': ('C_update_b_update_fun$' * 'C_update_b_update_fun$') > 'B_update_c_update_fun_c_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_388, type, 'register_pair$i': ('B_update_b_update_fun$' * 'A_update_b_update_fun$') > 'B_a_prod_update_b_update_fun$').
% 2.25/1.29 tff(func_def_389, type, 'register_tensor$z': ('C_update_a_update_fun$' * 'C_d_prod_update_a_update_fun$') > 'C_c_d_prod_prod_update_a_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_390, type, 'fun_app$ay': ('B_update_d_a_prod_update_fun$' * 'B_update$') > 'D_a_prod_update$').
% 2.25/1.29 tff(func_def_391, type, 'grp$a': ('C_update_a_update_fun_set$' * 'C_update_a_update_fun_c_update_b_update_fun_fun$') > 'C_update_a_update_fun_c_update_b_update_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_392, type, 'fun_app$am': ('C_update_c_update_bool_fun_fun$' * 'C_update$') > 'C_update_bool_fun$').
% 2.25/1.29 tff(func_def_393, type, 'compatible$r': 'B_update_a_update_fun$' > 'D_update_a_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_394, type, 'convol$e': ('D_update_b_update_fun$' * 'D_update_b_update_fun$') > 'D_update_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_395, type, 'fun_app$bt': ('A_c_prod_update_b_a_prod_update_fun$' * 'A_c_prod_update$') > 'B_a_prod_update$').
% 2.25/1.29 tff(func_def_396, type, 'comp$f': ('C_update_b_update_fun$' * 'C_update_c_update_fun$') > 'C_update_b_update_fun$').
% 2.25/1.29 tff(func_def_397, type, 'register_pair$k': ('A_update_a_update_fun$' * 'D_update_a_update_fun$') > 'A_d_prod_update_a_update_fun$').
% 2.25/1.29 tff(func_def_398, type, 'relcompp$j': ('C_d_prod_update_a_update_bool_fun_fun$' * 'A_update_b_update_bool_fun_fun$') > 'C_d_prod_update_b_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_399, type, 'register_tensor$w': ('D_update_b_update_fun$' * 'C_d_prod_update_b_update_fun$') > 'D_c_d_prod_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_400, type, 'fun_app$ax': ('B_update_d_b_prod_update_fun$' * 'B_update$') > 'D_b_prod_update$').
% 2.25/1.29 tff(func_def_401, type, 'tensor_update$': 'B_update$' > 'A_update_b_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_402, type, 'rel_fun$r': ('C_d_prod_update_a_update_fun_c_d_prod_update_a_update_fun_bool_fun_fun$' * 'C_d_prod_update_b_update_fun_c_d_prod_update_b_update_fun_bool_fun_fun$') > 'C_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_c_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_403, type, 'uup$': 'B_update_b_update_fun$' > 'B_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_404, type, 'rel_fun$ab': ('D_update_c_update_bool_fun_fun$' * 'B_update_b_update_bool_fun_fun$') > 'D_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_405, type, 'uue$': 'C_d_prod_update_a_update_fun_set$' > 'C_d_prod_update_a_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_406, type, 'rel_fun$j': ('C_update_a_update_fun_d_update_a_update_fun_bool_fun_fun$' * 'C_update_b_update_fun_d_update_b_update_fun_bool_fun_fun$') > 'C_update_a_update_fun_c_update_b_update_fun_fun_d_update_a_update_fun_d_update_b_update_fun_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_407, type, 'fun_app$p': ('C_update_b_d_prod_update_fun$' * 'C_update$') > 'B_d_prod_update$').
% 2.25/1.29 tff(func_def_408, type, 'map_prod$o': ('D_update_b_update_fun$' * 'C_d_prod_update_b_update_fun$') > 'D_update_c_d_prod_update_prod_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_409, type, 'uuo$': 'D_update_b_update_fun$' > 'D_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_410, type, 'uuh$': 'A_update_b_update_fun$' > 'A_update_b_d_prod_update_fun$').
% 2.25/1.29 tff(func_def_411, type, 'comp$ce': ('A_update_c_d_prod_update_fun$' * 'B_update_a_update_fun$') > 'B_update_c_d_prod_update_fun$').
% 2.25/1.29 tff(func_def_412, type, 'image$a': ('D_update_a_update_fun$' * 'D_update_set$') > 'A_update_set$').
% 2.25/1.29 tff(func_def_413, type, 'register_pair$m': ('A_update_a_update_fun$' * 'B_update_a_update_fun$') > 'A_b_prod_update_a_update_fun$').
% 2.25/1.29 tff(func_def_414, type, 'fun_app$d': ('A_update_a_c_prod_update_fun$' * 'A_update$') > 'A_c_prod_update$').
% 2.25/1.29 tff(func_def_415, type, 'grp$b': ('C_d_prod_update_a_update_fun_set$' * 'C_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun$') > 'C_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_416, type, 'rel_fun$p': ('C_d_prod_update_c_update_bool_fun_fun$' * 'B_update_b_update_bool_fun_fun$') > 'C_d_prod_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_417, type, 'fun_app$dc': ('C_update_c_update_prod_b_update_b_update_prod_fun$' * 'C_update_c_update_prod$') > 'B_update_b_update_prod$').
% 2.25/1.29 tff(func_def_418, type, 'fcomp$f': ('C_d_prod_update_a_update_fun$' * 'A_update_b_update_fun$') > 'C_d_prod_update_b_update_fun$').
% 2.25/1.29 tff(func_def_419, type, 'uuj$': 'B_update_b_update_fun$' > 'B_update_b_d_prod_update_fun$').
% 2.25/1.29 tff(func_def_420, type, 'comp$g': ('B_update_b_update_fun$' * 'A_update_b_update_fun$') > 'A_update_b_update_fun$').
% 2.25/1.29 tff(func_def_421, type, 'uvv$': 'D_update_bool_fun$').
% 2.25/1.29 tff(func_def_422, type, 'preregister$a': 'C_update_a_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_423, type, 'relcompp$': ('B_update_a_update_bool_fun_fun$' * 'A_update_b_update_bool_fun_fun$') > 'B_update_b_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_424, type, 'uuz$': 'C_update_b_update_fun$' > 'C_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_425, type, 'comp$p': ('B_update_b_update_fun$' * 'D_update_b_update_fun$') > 'D_update_b_update_fun$').
% 2.25/1.29 tff(func_def_426, type, 'fun_app$bx': ('C_update_c_update_fun$' * 'C_update$') > 'C_update$').
% 2.25/1.29 tff(func_def_427, type, 'uuq$': 'C_update_a_update_fun$' > 'C_update_d_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_428, type, 'uvi$': 'C_update_a_update_fun$' > 'C_update_b_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_429, type, 'register_tensor$n': ('D_update_a_update_fun$' * 'D_update_b_update_fun$') > 'D_d_prod_update_a_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_430, type, 'map_prod$m': ('D_update_b_update_fun$' * 'C_update_b_update_fun$') > 'D_update_c_update_prod_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_431, type, 'id_update$b': 'C_update$').
% 2.25/1.29 tff(func_def_432, type, 'comp$ba': ('C_d_prod_update_b_update_fun$' * 'C_update_c_d_prod_update_fun$') > 'C_update_b_update_fun$').
% 2.25/1.29 tff(func_def_433, type, 'comp$o': ('A_b_prod_update_b_update_fun$' * 'D_d_prod_update_a_b_prod_update_fun$') > 'D_d_prod_update_b_update_fun$').
% 2.25/1.29 tff(func_def_434, type, 'relcompp$m': ('D_update_a_update_bool_fun_fun$' * 'A_update_b_update_bool_fun_fun$') > 'D_update_b_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_435, type, 'uwe$': 'A_update_a_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_436, type, 'map_prod$q': ('D_update_b_update_fun$' * 'D_update_b_update_fun$') > 'D_update_d_update_prod_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_437, type, 'uvp$': 'C_update_a_update_fun$' > 'C_update_a_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_438, type, 'comp$c': ('B_update_a_update_fun$' * 'C_update_b_update_fun$') > 'C_update_a_update_fun$').
% 2.25/1.29 tff(func_def_439, type, 'comp$al': ('C_update_b_update_fun$' * 'D_update_c_update_fun$') > 'D_update_b_update_fun$').
% 2.25/1.29 tff(func_def_440, type, 'image$': ('C_d_prod_update_a_update_fun$' * 'C_d_prod_update_set$') > 'A_update_set$').
% 2.25/1.29 tff(func_def_441, type, 'comp$am': ('A_update_b_update_fun$' * 'A_update_a_update_fun$') > 'A_update_b_update_fun$').
% 2.25/1.29 tff(func_def_442, type, 'fun_app$bi': ('B_update_d_update_fun$' * 'B_update$') > 'D_update$').
% 2.25/1.29 tff(func_def_443, type, 'register_pair$o': ('B_update_d_update_fun$' * 'A_update_d_update_fun$' * 'B_a_prod_update$') > 'D_update$').
% 2.25/1.29 tff(func_def_444, type, 'map_prod$c': ('C_update_b_update_fun$' * 'C_d_prod_update_b_update_fun$') > 'C_update_c_d_prod_update_prod_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_445, type, 'uwc$': 'A_update_set$' > 'D_update_a_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_446, type, 'fun_app$y': ('B_update_b_b_prod_update_fun$' * 'B_update$') > 'B_b_prod_update$').
% 2.25/1.29 tff(func_def_447, type, 'uvr$': 'D_update_b_update_fun$' > 'D_update_a_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_448, type, 'register_tensor$x': ('C_d_prod_update_a_update_fun$' * 'C_update_a_update_fun$') > 'C_d_prod_c_prod_update_a_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_449, type, 'fcomp$d': ('B_update_c_update_fun_a_update_a_update_fun_fun$' * 'A_update_a_update_fun_c_update_b_update_fun_fun$') > 'B_update_c_update_fun_c_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_450, type, 'fun_app$dm': ('C_d_prod_update_d_update_prod_b_update_b_update_prod_fun$' * 'C_d_prod_update_d_update_prod$') > 'B_update_b_update_prod$').
% 2.25/1.29 tff(func_def_451, type, 'register_pair$u': ('A_update_b_a_prod_update_fun$' * 'D_update_b_a_prod_update_fun$') > 'A_d_prod_update_b_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_452, type, 'fun_app$do': ('D_update_c_update_prod_b_update_b_update_prod_fun$' * 'D_update_c_update_prod$') > 'B_update_b_update_prod$').
% 2.25/1.29 tff(func_def_453, type, 'pred_fun$c': ('C_d_prod_update_bool_fun$' * 'A_update_bool_fun$') > 'C_d_prod_update_a_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_454, type, 'fun_app$dp': ('D_update_c_d_prod_update_prod_a_update_a_update_prod_fun$' * 'D_update_c_d_prod_update_prod$') > 'A_update_a_update_prod$').
% 2.25/1.29 tff(func_def_455, type, 'fun_app$af': ('A_update_b_b_prod_update_fun$' * 'A_update$') > 'B_b_prod_update$').
% 2.25/1.29 tff(func_def_456, type, 'fun_app$ap': ('A_update_a_update_bool_fun_fun$' * 'A_update$') > 'A_update_bool_fun$').
% 2.25/1.29 tff(func_def_457, type, 'collect$a': 'D_update_bool_fun$' > 'D_update_set$').
% 2.25/1.29 tff(func_def_458, type, 'comp$bn': ('A_update_a_update_fun_c_d_prod_update_b_update_fun_fun$' * 'B_update_c_d_prod_update_fun_a_update_a_update_fun_fun$') > 'B_update_c_d_prod_update_fun_c_d_prod_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_459, type, 'tensor_update$i': ('D_update$' * 'B_update$') > 'D_b_prod_update$').
% 2.25/1.29 tff(func_def_460, type, 'comp$n': ('A_b_prod_update_b_update_fun$' * 'D_a_prod_update_a_b_prod_update_fun$') > 'D_a_prod_update_b_update_fun$').
% 2.25/1.29 tff(func_def_461, type, 'fun_app$o': ('D_update_b_a_prod_update_fun$' * 'D_update$') > 'B_a_prod_update$').
% 2.25/1.29 tff(func_def_462, type, 'relcompp$a': ('A_update_a_update_bool_fun_fun$' * 'A_update_b_update_bool_fun_fun$') > 'A_update_b_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_463, type, 'comp$ab': ('A_a_prod_update_b_b_prod_update_fun$' * 'D_c_prod_update_a_a_prod_update_fun$') > 'D_c_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_464, type, 'rel_fun$d': ('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$').
% 2.25/1.29 tff(func_def_465, type, 'relcompp$i': ('A_update_a_update_bool_fun_fun$' * 'A_update_c_d_prod_update_bool_fun_fun$') > 'A_update_c_d_prod_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_466, type, 'comp$ah': ('A_a_prod_update_b_b_prod_update_fun$' * 'C_c_d_prod_prod_update_a_a_prod_update_fun$') > 'C_c_d_prod_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_467, type, 'register_tensor$e': ('C_update_b_update_fun$' * 'C_update_b_update_fun$') > 'C_c_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_468, type, 'uvg$': 'A_update_b_update_fun$' > 'A_update_b_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_469, type, 'fun_app$co': ('A_update_a_update_fun_d_update_b_update_fun_fun$' * 'A_update_a_update_fun$') > 'D_update_b_update_fun$').
% 2.25/1.29 tff(func_def_470, type, 'register_tensor$u': ('C_d_prod_update_b_update_fun$' * 'D_update_b_update_fun$') > 'C_d_prod_d_prod_update_b_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_471, type, 'rel_fun$n': ('C_d_prod_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$' * 'C_d_prod_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$') > 'C_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_c_update_a_update_fun_c_update_b_update_fun_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_472, type, 'uvz$': 'D_update_d_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_473, type, 'register$e': 'D_update_a_update_fun_bool_fun$').
% 2.25/1.29 tff(func_def_474, type, 'map_prod$g': ('C_d_prod_update_b_update_fun$' * 'C_update_b_update_fun$') > 'C_d_prod_update_c_update_prod_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_475, type, 'fun_app$be': ('C_update_a_update_fun_c_update_b_update_fun_fun$' * 'C_update_a_update_fun$') > 'C_update_b_update_fun$').
% 2.25/1.29 tff(func_def_476, type, 'collect$d': 'D_update_a_update_fun_bool_fun$' > 'D_update_a_update_fun_set$').
% 2.25/1.29 tff(func_def_477, type, 'register_tensor$ab': ('C_d_prod_update_a_update_fun$' * 'C_d_prod_update_a_update_fun$') > 'C_d_prod_c_d_prod_prod_update_a_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_478, type, 'uut$': 'D_update_b_update_fun$' > 'D_update_d_b_prod_update_fun$').
% 2.25/1.29 tff(func_def_479, type, 'fun_app$cf': ('C_c_prod_update_a_update_fun$' * 'C_c_prod_update$') > 'A_update$').
% 2.25/1.29 tff(func_def_480, type, 'relcompp$k': ('D_update_a_update_bool_fun_fun$' * 'A_update_d_update_bool_fun_fun$') > 'D_update_d_update_bool_fun_fun$').
% 2.25/1.29 tff(func_def_481, type, 'fcomp$g': ('D_update_a_update_fun$' * 'A_update_b_update_fun$') > 'D_update_b_update_fun$').
% 2.25/1.29 tff(func_def_482, type, 'comp$q': ('A_a_prod_update_b_update_fun$' * 'C_c_prod_update_a_a_prod_update_fun$') > 'C_c_prod_update_b_update_fun$').
% 2.25/1.29 tff(func_def_483, type, 'comp_update$h': ('D_a_prod_update$' * 'D_a_prod_update$') > 'D_a_prod_update$').
% 2.25/1.29 tff(func_def_484, type, 'fun_app$df': ('C_update_d_update_prod_a_update_a_update_prod_fun$' * 'C_update_d_update_prod$') > 'A_update_a_update_prod$').
% 2.25/1.29 tff(func_def_485, type, 'fun_app$ci': ('A_c_prod_update_b_update_fun$' * 'A_c_prod_update$') > 'B_update$').
% 2.25/1.29 tff(func_def_486, type, 'fun_app$z': ('A_update_d_d_prod_update_fun$' * 'A_update$') > 'D_d_prod_update$').
% 2.25/1.29 tff(func_def_487, type, 'fun_app$dx': ('B_update_c_d_prod_update_fun_d_update_b_update_fun_fun$' * 'B_update_c_d_prod_update_fun$') > 'D_update_b_update_fun$').
% 2.25/1.29 tff(func_def_488, type, 'comp$b': ('A_update_a_update_fun$' * 'C_update_a_update_fun$') > 'C_update_a_update_fun$').
% 2.25/1.29 tff(func_def_489, type, 'fun_app$ak': ('C_d_prod_update_c_d_prod_update_bool_fun_fun$' * 'C_d_prod_update$') > 'C_d_prod_update_bool_fun$').
% 2.25/1.29 tff(func_def_490, type, 'comp$ar': ('D_update_a_update_fun$' * 'A_update_d_update_fun$') > 'A_update_a_update_fun$').
% 2.25/1.29 tff(func_def_491, type, 'fcomp$b': ('B_update_c_d_prod_update_fun_a_update_a_update_fun_fun$' * 'A_update_a_update_fun_c_update_b_update_fun_fun$') > 'B_update_c_d_prod_update_fun_c_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_492, type, 'top$d': 'B_update_set$').
% 2.25/1.29 tff(func_def_493, type, 'map_prod$e': ('C_update_b_update_fun$' * 'D_update_b_update_fun$') > 'C_update_d_update_prod_b_update_b_update_prod_fun$').
% 2.25/1.29 tff(func_def_494, type, 'rel_fun$t': ('C_d_prod_update_c_d_prod_update_bool_fun_fun$' * 'B_update_b_update_bool_fun_fun$') > 'C_d_prod_update_b_update_fun_c_d_prod_update_b_update_fun_bool_fun_fun$').
% 2.25/1.29 tff(func_def_495, type, 'uvk$': 'C_update_a_update_fun$' > 'C_update_a_a_prod_update_fun$').
% 2.25/1.29 tff(func_def_496, type, 'fun_app$bk': ('A_update_b_update_fun_c_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_fun$' * 'A_update_b_update_fun$') > 'C_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun$').
% 2.25/1.29 tff(func_def_497, type, 'fun_app$at': ('D_update_a_b_prod_update_fun$' * 'D_update$') > 'A_b_prod_update$').
% 2.25/1.29 tff(func_def_498, type, 'fun_app$ct': ('A_update_a_update_fun_c_update_b_update_fun_fun$' * 'A_update_a_update_fun$') > 'C_update_b_update_fun$').
% 2.25/1.29 tff(func_def_499, type, sK0: ('C_d_prod_update_b_update_fun$' * 'C_d_prod_update_b_update_fun$') > 'C_update$').
% 2.25/1.29 tff(func_def_500, type, sK1: ('C_d_prod_update_b_update_fun$' * 'C_d_prod_update_b_update_fun$') > 'D_update$').
% 2.25/1.29 tff(func_def_501, type, sK2: ('C_update_a_update_fun$' * 'D_update_a_update_fun$') > 'C_update$').
% 2.25/1.29 tff(func_def_502, type, sK3: ('C_update_a_update_fun$' * 'D_update_a_update_fun$') > 'D_update$').
% 2.25/1.29 tff(func_def_503, type, sK4: ('C_update_a_update_fun$' * 'D_update_a_update_fun$') > 'C_update$').
% 2.25/1.29 tff(func_def_504, type, sK5: ('C_update_a_update_fun$' * 'D_update_a_update_fun$') > 'D_update$').
% 2.25/1.29 tff(func_def_505, type, sK6: ('C_update_a_update_fun$' * 'D_update_a_update_fun$') > 'C_update$').
% 2.25/1.29 tff(func_def_506, type, sK7: ('C_update_a_update_fun$' * 'D_update_a_update_fun$') > 'D_update$').
% 2.25/1.29 tff(f60,conjecture,(
% 2.25/1.29 'fun_app$k'('register$','g$')),
% 2.25/1.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture59)).
% 2.25/1.29
% 2.25/1.29 tff(f61,negated_conjecture,(
% 2.25/1.29 ~ 'fun_app$k'('register$','g$')),
% 2.25/1.29 inference(negated_conjecture,[status(cth)],[f60])).
% 2.25/1.29
% 2.25/1.29 tff(f62,axiom,(
% 2.25/1.29 'fun_app$j'('compatible$'('g$'),'h$')),
% 2.25/1.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom60)).
% 2.25/1.29
% 2.25/1.29 tff(f68,axiom,(
% 2.25/1.29 ! [X0 : 'C_update_a_update_fun$',X1 : 'D_update_a_update_fun$'] : ('fun_app$j'('compatible$'(X0),X1) => 'fun_app$k'('register$',X0))),
% 2.25/1.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom66)).
% 2.25/1.29
% 2.25/1.29 tff(f698,plain,(
% 2.25/1.29 ~'fun_app$k'('register$','g$')),
% 2.25/1.29 inference(flattening,[],[f61])).
% 2.25/1.29
% 2.25/1.29 tff(f722,plain,(
% 2.25/1.29 ! [X0 : 'C_update_a_update_fun$',X1 : 'D_update_a_update_fun$'] : ('fun_app$k'('register$',X0) | ~'fun_app$j'('compatible$'(X0),X1))),
% 2.25/1.29 inference(ennf_transformation,[],[f68])).
% 2.25/1.29
% 2.25/1.29 tff(f767,plain,(
% 2.25/1.29 ~'fun_app$k'('register$','g$')),
% 2.25/1.29 inference(cnf_transformation,[],[f698])).
% 2.25/1.29
% 2.25/1.29 tff(f771,plain,(
% 2.25/1.29 'fun_app$j'('compatible$'('g$'),'h$')),
% 2.25/1.29 inference(cnf_transformation,[],[f62])).
% 2.25/1.29
% 2.25/1.29 tff(f790,plain,(
% 2.25/1.29 ( ! [X0 : 'C_update_a_update_fun$',X1 : 'D_update_a_update_fun$'] : ('fun_app$k'('register$',X0) | ~'fun_app$j'('compatible$'(X0),X1)) )),
% 2.25/1.29 inference(cnf_transformation,[],[f722])).
% 2.25/1.29
% 2.25/1.29 tcf(c_49,negated_conjecture,
% 2.25/1.29 (~'fun_app$k'('register$','g$')),
% 2.25/1.29 inference(cnf_transformation,[],[f767])).
% 2.25/1.29
% 2.25/1.29 tcf(c_53,plain,
% 2.25/1.29 ('fun_app$j'('compatible$'('g$'),'h$')),
% 2.25/1.29 inference(cnf_transformation,[],[f771])).
% 2.25/1.29
% 2.25/1.29 tcf(c_72,plain,![X0_'D_update_a_update_fun':'D_update_a_update_fun$',X0_'C_update_a_update_fun':'C_update_a_update_fun$']:
% 2.25/1.29 (~'fun_app$j'('compatible$'(X0_'C_update_a_update_fun'),X0_'D_update_a_update_fun')|
% 2.25/1.29 'fun_app$k'('register$',X0_'C_update_a_update_fun')),
% 2.25/1.29 inference(cnf_transformation,[],[f790])).
% 2.25/1.29
% 2.25/1.29 tcf(c_128,plain,
% 2.25/1.29 (~'fun_app$j'('compatible$'('g$'),'h$')|'fun_app$k'('register$','g$')),
% 2.25/1.29 inference(instantiation,[status(thm)],[c_72])).
% 2.25/1.29
% 2.25/1.29 tcf(c_129,plain,
% 2.25/1.29 ($false),
% 2.25/1.29 inference(prop_impl_just,[status(thm)],[c_128,c_53,c_49])).
% 2.25/1.29
% 2.25/1.29
% 2.25/1.29 % SZS output end CNFRefutation for theBenchmark.p
% 2.25/1.29
% 2.25/1.29
%------------------------------------------------------------------------------