Beagle---0.9.52.THM-CRf.s

%------------------------------------------------------------------------------
% File     : Beagle---0.9.52
% Problem  : ITP383_1 : TPTP v9.0.0. Released v8.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s

% Computer : n015.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Wed Apr  9 06:53:44 PM UTC 2025

% Result   : Theorem 21.05s 7.41s
% Output   : CNFRefutation 21.05s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12  % Problem  : ITP383_1 : TPTP v9.0.0. Released v8.0.0.
% 0.10/0.13  % Command  : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34  % Computer : n015.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 300
% 0.13/0.34  % DateTime : Tue Apr  8 02:21:05 EDT 2025
% 0.13/0.34  % CPUTime  : 
% 21.05/7.41  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.05/7.41  
% 21.05/7.41  % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.05/7.45  %$ rel_fun$y > rel_fun$u > rel_fun$q > rel_fun$m > rel_fun$i > rel_fun$e > rel_fun$ag > rel_fun$ac > rel_fun$ > quotient$m > quotient$l > quotient$k > quotient$j > quotient$i > quotient$h > quotient$g > quotient$f > quotient$e > quotient$d > quotient$c > quotient$b > quotient$a > quotient$ > type_definition$j > type_definition$i > type_definition$h > type_definition$g > type_definition$f > type_definition$e > type_definition$d > type_definition$c > type_definition$b > type_definition$a > type_definition$ > pred_fun$d > pred_fun$b > pred_fun$ > separating$e > separating$d > separating$c > separating$b > separating$a > separating$ > member$g > member$f > member$e > member$d > member$c > member$b > member$a > member$ > less_eq$ > fun_app$k > fun_app$j > fun_app$i > fun_app$aq > fun_app$an > fun_app$aj > fun_app$ai > fun_app$ah > fun_app$ag > compatible$z > compatible$y > compatible$x > compatible$w > compatible$v > compatible$u > compatible$t > compatible$s > compatible$q > compatible$p > compatible$o > compatible$n > compatible$l > compatible$k > compatible$j > compatible$i > compatible$h > compatible$f > compatible$e > compatible$c > compatible$b > compatible$as > compatible$ar > compatible$aq > compatible$ap > compatible$ao > compatible$an > compatible$am > compatible$al > compatible$ak > compatible$aj > compatible$ai > compatible$ah > compatible$ag > compatible$af > compatible$ae > compatible$ac > compatible$ab > compatible$aa > compatible$a > register$z > register$y > register$x > register$w > register$v > register$u > register$t > register$s > register$r > register$q > register$p > register$o > register$n > register$m > register$l > register$k > register$j > register$i > register$h > register$g > register$f > register$d > register$c > register$bm > register$bl > register$bk > register$bj > register$bi > register$bh > register$bg > register$bf > register$be > register$bd > register$bc > register$bb > register$ba > register$b > register$az > register$ay > register$ax > register$aw > register$av > register$au > register$at > register$as > register$ar > register$aq > register$ap > register$ao > register$an > register$am > register$al > register$ak > register$aj > register$ai > register$ah > register$ag > register$af > register$ad > register$ac > register$ab > register$aa > register$a > preregister$p > preregister$o > preregister$n > preregister$m > preregister$l > preregister$k > preregister$h > preregister$g > preregister$f > preregister$e > preregister$d > preregister$c > preregister$b > preregister$ > register_pair$r > register_pair$q > register_pair$p > register_pair$o > register_pair$n > uvw$ > tensor_update$o > tensor_update$n > tensor_update$m > tensor_update$l > tensor_update$k > tensor_update$j > tensor_update$i > tensor_update$h > tensor_update$g > tensor_update$f > tensor_update$e > relcompp$m > relcompp$l > relcompp$k > relcompp$j > relcompp$i > relcompp$h > relcompp$g > relcompp$f > relcompp$e > relcompp$d > relcompp$c > relcompp$b > relcompp$a > relcompp$ > rel_fun$z > rel_fun$x > rel_fun$w > rel_fun$v > rel_fun$t > rel_fun$s > rel_fun$r > rel_fun$p > rel_fun$o > rel_fun$n > rel_fun$l > rel_fun$k > rel_fun$j > rel_fun$h > rel_fun$g > rel_fun$f > rel_fun$d > rel_fun$c > rel_fun$b > rel_fun$am > rel_fun$al > rel_fun$ak > rel_fun$aj > rel_fun$ai > rel_fun$ah > rel_fun$af > rel_fun$ae > rel_fun$ad > rel_fun$ab > rel_fun$aa > rel_fun$a > register_tensor$z > register_tensor$y > register_tensor$x > register_tensor$w > register_tensor$v > register_tensor$u > register_tensor$t > register_tensor$s > register_tensor$r > register_tensor$q > register_tensor$p > register_tensor$o > register_tensor$n > register_tensor$m > register_tensor$l > register_tensor$k > register_tensor$j > register_tensor$i > register_tensor$h > register_tensor$g > register_tensor$f > register_tensor$e > register_tensor$d > register_tensor$c > register_tensor$b > register_tensor$af > register_tensor$ae > register_tensor$ad > register_tensor$ac > register_tensor$ab > register_tensor$aa > register_tensor$a > register_tensor$ > register_pair$x > register_pair$w > register_pair$v > register_pair$u > register_pair$t > register_pair$s > register_pair$m > register_pair$l > register_pair$k > register_pair$j > register_pair$i > register_pair$h > register_pair$g > register_pair$f > register_pair$e > register_pair$d > register_pair$c > register_pair$b > register_pair$a > register_pair$ > pred_fun$e > pred_fun$c > pred_fun$a > map_prod$r > map_prod$q > map_prod$p > map_prod$o > map_prod$n > map_prod$m > map_prod$l > map_prod$k > map_prod$j > map_prod$i > map_prod$h > map_prod$g > map_prod$f > map_prod$e > map_prod$d > map_prod$c > map_prod$b > map_prod$a > map_prod$ > map_fun$n > map_fun$m > map_fun$l > map_fun$k > map_fun$j > map_fun$i > map_fun$h > map_fun$g > map_fun$f > map_fun$e > map_fun$d > map_fun$c > map_fun$b > map_fun$a > map_fun$ > image$f > image$e > image$d > image$c > image$b > image$a > image$ > grp$c > grp$b > grp$a > grp$ > fun_app$z > fun_app$y > fun_app$x > fun_app$w > fun_app$v > fun_app$u > fun_app$t > fun_app$s > fun_app$r > fun_app$q > fun_app$p > fun_app$o > fun_app$n > fun_app$m > fun_app$l > fun_app$h > fun_app$g > fun_app$f > fun_app$e > fun_app$dy > fun_app$dx > fun_app$dw > fun_app$dv > fun_app$du > fun_app$dt > fun_app$ds > fun_app$dr > fun_app$dq > fun_app$dp > fun_app$do > fun_app$dn > fun_app$dm > fun_app$dl > fun_app$dk > fun_app$dj > fun_app$di > fun_app$dh > fun_app$dg > fun_app$df > fun_app$de > fun_app$dd > fun_app$dc > fun_app$db > fun_app$da > fun_app$d > fun_app$cz > fun_app$cy > fun_app$cx > fun_app$cw > fun_app$cv > fun_app$cu > fun_app$ct > fun_app$cs > fun_app$cr > fun_app$cq > fun_app$cp > fun_app$co > fun_app$cn > fun_app$cm > fun_app$cl > fun_app$ck > fun_app$cj > fun_app$ci > fun_app$ch > fun_app$cg > fun_app$cf > fun_app$ce > fun_app$cd > fun_app$cc > fun_app$cb > fun_app$ca > fun_app$c > fun_app$bz > fun_app$by > fun_app$bx > fun_app$bw > fun_app$bv > fun_app$bu > fun_app$bt > fun_app$bs > fun_app$br > fun_app$bq > fun_app$bp > fun_app$bo > fun_app$bn > fun_app$bm > fun_app$bl > fun_app$bk > fun_app$bj > fun_app$bi > fun_app$bh > fun_app$bg > fun_app$bf > fun_app$be > fun_app$bd > fun_app$bc > fun_app$bb > fun_app$ba > fun_app$b > fun_app$az > fun_app$ay > fun_app$ax > fun_app$aw > fun_app$av > fun_app$au > fun_app$at > fun_app$as > fun_app$ar > fun_app$ap > fun_app$ao > fun_app$am > fun_app$al > fun_app$ak > fun_app$af > fun_app$ae > fun_app$ad > fun_app$ac > fun_app$ab > fun_app$aa > fun_app$a > fun_app$ > fcomp$g > fcomp$f > fcomp$e > fcomp$d > fcomp$c > fcomp$b > fcomp$a > fcomp$ > convol$f > convol$e > convol$d > convol$c > convol$b > convol$a > convol$ > comp_update$l > comp_update$k > comp_update$j > comp_update$i > comp_update$h > comp_update$g > comp_update$f > comp_update$e > comp_update$d > comp$z > comp$y > comp$x > comp$w > comp$v > comp$u > comp$t > comp$s > comp$r > comp$q > comp$p > comp$o > comp$n > comp$m > comp$l > comp$k > comp$i > comp$h > comp$g > comp$f > comp$e > comp$d > comp$cg > comp$cf > comp$ce > comp$cd > comp$cc > comp$cb > comp$ca > comp$c > comp$bz > comp$by > comp$bx > comp$bw > comp$bv > comp$bu > comp$bt > comp$bs > comp$br > comp$bq > comp$bp > comp$bo > comp$bn > comp$bm > comp$bl > comp$bk > comp$bj > comp$bi > comp$bh > comp$bg > comp$bf > comp$be > comp$bd > comp$bc > comp$bb > comp$ba > comp$b > comp$az > comp$ay > comp$ax > comp$aw > comp$av > comp$au > comp$at > comp$as > comp$ar > comp$aq > comp$ap > comp$ao > comp$an > comp$am > comp$al > comp$ak > comp$aj > comp$ai > comp$ah > comp$ag > comp$af > comp$ae > comp$ad > comp$ac > comp$ab > comp$aa > #nlpp > uwc$ > uwb$ > uwa$ > uvs$ > uvr$ > uvq$ > uvp$ > uvo$ > uvn$ > uvm$ > uvl$ > uvk$ > uvj$ > uvi$ > uvh$ > uvg$ > uvf$ > uuz$ > uuy$ > uux$ > uuw$ > uuv$ > uuu$ > uut$ > uus$ > uur$ > uuq$ > uup$ > uuo$ > uun$ > uum$ > uul$ > uuk$ > uuj$ > uui$ > uuh$ > uug$ > uuf$ > uue$ > uud$ > uuc$ > uub$ > uua$ > uu$ > tensor_update$d > tensor_update$c > tensor_update$b > tensor_update$a > tensor_update$ > conversep$c > conversep$b > conversep$a > conversep$ > compatible$r > compatible$m > compatible$g > compatible$d > compatible$ad > compatible$ > comp_update$m > comp_update$c > comp_update$b > comp_update$a > comp_update$ > collect$f > collect$e > collect$d > collect$c > collect$b > collect$a > collect$ > uwf$ > uwe$ > uwd$ > uvz$ > uvy$ > uvx$ > uvv$ > uvu$ > uvt$ > uve$ > uvd$ > uvc$ > uvb$ > uva$ > type$ > top$d > top$c > top$b > top$a > top$ > register$e > register$ae > register$ > preregister$j > preregister$i > preregister$a > id_update$c > id_update$b > id_update$a > id_update$ > id$ > h$ > g$ > f$ > comp$j > comp$a > comp$ > #skF_46 > #skF_9 > #skF_56 > #skF_52 > #skF_58 > #skF_28 > #skF_83 > #skF_105 > #skF_68 > #skF_118 > #skF_11 > #skF_106 > #skF_12 > #skF_80 > #skF_5 > #skF_25 > #skF_59 > #skF_54 > #skF_91 > #skF_27 > #skF_30 > #skF_18 > #skF_86 > #skF_10 > #skF_121 > #skF_61 > #skF_104 > #skF_102 > #skF_95 > #skF_29 > #skF_69 > #skF_31 > #skF_23 > #skF_47 > #skF_116 > #skF_34 > #skF_122 > #skF_41 > #skF_77 > #skF_19 > #skF_94 > #skF_113 > #skF_108 > #skF_79 > #skF_103 > #skF_32 > #skF_111 > #skF_40 > #skF_60 > #skF_71 > #skF_51 > #skF_93 > #skF_26 > #skF_22 > #skF_90 > #skF_96 > #skF_7 > #skF_110 > #skF_115 > #skF_114 > #skF_62 > #skF_67 > #skF_35 > #skF_36 > #skF_72 > #skF_38 > #skF_87 > #skF_66 > #skF_8 > #skF_64 > #skF_53 > #skF_44 > #skF_16 > #skF_84 > #skF_89 > #skF_117 > #skF_1 > #skF_65 > #skF_3 > #skF_98 > #skF_75 > #skF_99 > #skF_48 > #skF_6 > #skF_88 > #skF_74 > #skF_107 > #skF_57 > #skF_4 > #skF_112 > #skF_21 > #skF_17 > #skF_119 > #skF_109 > #skF_37 > #skF_101 > #skF_50 > #skF_2 > #skF_33 > #skF_73 > #skF_120 > #skF_20 > #skF_81 > #skF_15 > #skF_82 > #skF_49 > #skF_76 > #skF_63 > #skF_42 > #skF_13 > #skF_92 > #skF_70 > #skF_78 > #skF_97 > #skF_39 > #skF_45 > #skF_43 > #skF_14 > #skF_100 > #skF_85 > #skF_24 > #skF_55
% 21.05/7.45  
% 21.05/7.45  %Foreground sorts:
% 21.05/7.45  tff(B_a_prod_update$, type, B_a_prod_update$: $tType ).
% 21.05/7.45  tff(D_a_prod_update_a_b_prod_update_fun$, type, D_a_prod_update_a_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_c_d_prod_update_prod_b_update_b_update_prod_fun$, type, C_d_prod_update_c_d_prod_update_prod_b_update_b_update_prod_fun$: $tType ).
% 21.05/7.45  tff(C_c_prod_update_a_update_fun$, type, C_c_prod_update_a_update_fun$: $tType ).
% 21.05/7.45  tff(B_update_a_b_prod_update_fun$, type, B_update_a_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_c_d_prod_prod_update_b_b_prod_update_fun$, type, C_c_d_prod_prod_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_update_c_update_bool_fun_fun$, type, D_update_c_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(A_update_d_b_prod_update_fun$, type, A_update_d_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_c_d_prod_update_prod_a_update_a_update_prod_fun$, type, C_d_prod_update_c_d_prod_update_prod_a_update_a_update_prod_fun$: $tType ).
% 21.05/7.45  tff(C_update_d_b_prod_update_fun$, type, C_update_d_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_a_update_fun_bool_fun$, type, C_d_prod_update_a_update_fun_bool_fun$: $tType ).
% 21.05/7.45  tff(C_b_prod_update$, type, C_b_prod_update$: $tType ).
% 21.05/7.45  tff(C_update_c_d_prod_update_prod_b_update_b_update_prod_fun$, type, C_update_c_d_prod_update_prod_b_update_b_update_prod_fun$: $tType ).
% 21.05/7.45  tff(C_update_b_a_prod_update_fun$, type, C_update_b_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(A_update$, type, A_update$: $tType ).
% 21.05/7.45  tff(C_d_prod_c_d_prod_prod_update_b_b_prod_update_fun$, type, C_d_prod_c_d_prod_prod_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(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$, type, 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$: $tType ).
% 21.05/7.45  tff(B_update_d_update_fun_d_update_b_update_fun_fun$, type, B_update_d_update_fun_d_update_b_update_fun_fun$: $tType ).
% 21.05/7.45  tff(D_update_d_update_bool_fun_fun$, type, D_update_d_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(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$, type, 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$: $tType ).
% 21.05/7.45  tff(A_c_prod_update_b_a_prod_update_fun$, type, A_c_prod_update_b_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_a_c_prod_update_fun$, type, C_update_a_c_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_b_update_fun$, type, C_d_prod_update_b_update_fun$: $tType ).
% 21.05/7.45  tff(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$, type, 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$: $tType ).
% 21.05/7.45  tff(C_update_a_update_fun_set$, type, C_update_a_update_fun_set$: $tType ).
% 21.05/7.45  tff(A_update_a_d_prod_update_fun$, type, A_update_a_d_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_update_d_b_prod_update_fun$, type, D_update_d_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_update_b_update_b_update_prod_fun$, type, D_update_b_update_b_update_prod_fun$: $tType ).
% 21.05/7.45  tff(A_update_a_update_fun_c_d_prod_update_b_update_fun_fun$, type, A_update_a_update_fun_c_d_prod_update_b_update_fun_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_d_update_bool_fun_fun$, type, C_d_prod_update_d_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(D_c_d_prod_prod_update_a_a_prod_update_fun$, type, D_c_d_prod_prod_update_a_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(B_update_a_update_bool_fun_fun$, type, B_update_a_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_a_update_fun$, type, C_d_prod_update_a_update_fun$: $tType ).
% 21.05/7.45  tff(D_update_a_update_fun_bool_fun$, type, D_update_a_update_fun_bool_fun$: $tType ).
% 21.05/7.45  tff(D_update_b_update_fun_d_update_b_update_fun_bool_fun_fun$, type, D_update_b_update_fun_d_update_b_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(A_update_a_update_fun_d_update_b_update_fun_fun$, type, A_update_a_update_fun_d_update_b_update_fun_fun$: $tType ).
% 21.05/7.45  tff(D_update_d_update_prod$, type, D_update_d_update_prod$: $tType ).
% 21.05/7.45  tff(A_update_set$, type, A_update_set$: $tType ).
% 21.05/7.45  tff(C_c_prod_update_b_b_prod_update_fun$, type, C_c_prod_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_a_prod_update$, type, C_a_prod_update$: $tType ).
% 21.05/7.45  tff(A_update_a_a_prod_update_fun$, type, A_update_a_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(A_update_c_update_bool_fun_fun$, type, A_update_c_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(A_update_b_update_bool_fun_fun$, type, A_update_b_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(D_update_a_update_bool_fun_fun$, type, D_update_a_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(A_update_b_update_fun_c_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_fun$, type, A_update_b_update_fun_c_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_fun$: $tType ).
% 21.05/7.45  tff(B_update_bool_fun$, type, B_update_bool_fun$: $tType ).
% 21.05/7.45  tff(B_update_c_update_fun$, type, B_update_c_update_fun$: $tType ).
% 21.05/7.45  tff(B_update_d_b_prod_update_fun$, type, B_update_d_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_d_update_bool_fun_fun$, type, C_update_d_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(C_c_prod_update_a_b_prod_update_fun$, type, C_c_prod_update_a_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_set$, type, C_d_prod_update_set$: $tType ).
% 21.05/7.45  tff(C_d_prod_c_prod_update_b_b_prod_update_fun$, type, C_d_prod_c_prod_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_c_update_prod_b_update_b_update_prod_fun$, type, C_d_prod_update_c_update_prod_b_update_b_update_prod_fun$: $tType ).
% 21.05/7.45  tff(B_update_d_a_prod_update_fun$, type, B_update_d_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(A_update_b_update_fun_bool_fun$, type, A_update_b_update_fun_bool_fun$: $tType ).
% 21.05/7.45  tff(C_update_b_update_bool_fun_fun$, type, C_update_b_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(C_update_a_b_prod_update_fun$, type, C_update_a_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(B_itself$, type, B_itself$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_b_update_fun_c_d_prod_update_b_update_fun_bool_fun_fun$, type, C_d_prod_update_b_update_fun_c_d_prod_update_b_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(A_a_prod_update_b_b_prod_update_fun$, type, A_a_prod_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update$, type, C_d_prod_update$: $tType ).
% 21.05/7.45  tff(D_update_a_update_fun_c_d_prod_update_a_update_fun_bool_fun_fun$, type, D_update_a_update_fun_c_d_prod_update_a_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(D_update_b_a_prod_update_fun$, type, D_update_b_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_c_prod_update_a_a_prod_update_fun$, type, C_d_prod_c_prod_update_a_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(A_c_prod_update_b_update_fun$, type, A_c_prod_update_b_update_fun$: $tType ).
% 21.05/7.45  tff(C_c_prod_update_b_a_prod_update_fun$, type, C_c_prod_update_b_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_d_update_fun$, type, C_update_d_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_a_update_a_update_prod_fun$, type, C_update_a_update_a_update_prod_fun$: $tType ).
% 21.05/7.45  tff(C_update_c_d_prod_update_bool_fun_fun$, type, C_update_c_d_prod_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(C_update_c_update_prod_a_update_a_update_prod_fun$, type, C_update_c_update_prod_a_update_a_update_prod_fun$: $tType ).
% 21.05/7.45  tff(D_d_prod_update$, type, D_d_prod_update$: $tType ).
% 21.05/7.45  tff(C_update_a_update_fun_c_update_b_update_fun_fun$, type, C_update_a_update_fun_c_update_b_update_fun_fun$: $tType ).
% 21.05/7.45  tff(C_update_c_update_fun$, type, C_update_c_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_b_update_fun$, type, C_update_b_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_a_update_bool_fun_fun$, type, C_d_prod_update_a_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(A_update_bool_fun$, type, A_update_bool_fun$: $tType ).
% 21.05/7.45  tff(C_update_c_d_prod_update_fun$, type, C_update_c_d_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_d_a_prod_update_fun$, type, C_update_d_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$, type, D_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(C_update_c_d_prod_update_prod$, type, C_update_c_d_prod_update_prod$: $tType ).
% 21.05/7.45  tff(D_update_a_update_a_update_prod_fun$, type, D_update_a_update_a_update_prod_fun$: $tType ).
% 21.05/7.45  tff(D_update_a_update_fun_d_update_a_update_fun_bool_fun_fun$, type, D_update_a_update_fun_d_update_a_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(B_update_c_update_fun_a_update_a_update_fun_fun$, type, B_update_c_update_fun_a_update_a_update_fun_fun$: $tType ).
% 21.05/7.45  tff(B_b_prod_update$, type, B_b_prod_update$: $tType ).
% 21.05/7.45  tff(A_update_b_update_fun_d_update_a_update_fun_d_update_b_update_fun_fun_fun$, type, A_update_b_update_fun_d_update_a_update_fun_d_update_b_update_fun_fun_fun$: $tType ).
% 21.05/7.45  tff(A_update_a_update_fun$, type, A_update_a_update_fun$: $tType ).
% 21.05/7.45  tff(D_update_d_update_fun$, type, D_update_d_update_fun$: $tType ).
% 21.05/7.45  tff(A_update_d_update_fun$, type, A_update_d_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_c_update_prod$, type, C_d_prod_update_c_update_prod$: $tType ).
% 21.05/7.45  tff(A_c_prod_update$, type, A_c_prod_update$: $tType ).
% 21.05/7.45  tff(A_update_a_b_prod_update_fun$, type, A_update_a_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_update_c_update_prod$, type, D_update_c_update_prod$: $tType ).
% 21.05/7.45  tff(A_d_prod_update_b_a_prod_update_fun$, type, A_d_prod_update_b_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(A_a_prod_update$, type, A_a_prod_update$: $tType ).
% 21.05/7.45  tff(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$, type, 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$: $tType ).
% 21.05/7.45  tff(A_update_b_a_prod_update_fun$, type, A_update_b_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(B_update_c_update_fun_c_d_prod_update_b_update_fun_fun$, type, B_update_c_update_fun_c_d_prod_update_b_update_fun_fun$: $tType ).
% 21.05/7.45  tff(D_c_prod_update_a_b_prod_update_fun$, type, D_c_prod_update_a_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(B_update_b_a_prod_update_fun$, type, B_update_b_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_b_prod_update$, type, D_b_prod_update$: $tType ).
% 21.05/7.45  tff(A_update_d_update_bool_fun_fun$, type, A_update_d_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(B_update_a_update_fun$, type, B_update_a_update_fun$: $tType ).
% 21.05/7.45  tff(D_update_c_d_prod_update_bool_fun_fun$, type, D_update_c_d_prod_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(D_update_b_update_fun$, type, D_update_b_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_d_prod_update_a_a_prod_update_fun$, type, C_d_prod_d_prod_update_a_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(B_update_set$, type, B_update_set$: $tType ).
% 21.05/7.45  tff(C_d_prod_c_d_prod_prod_update_a_a_prod_update_fun$, type, C_d_prod_c_d_prod_prod_update_a_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_update_c_update_fun$, type, D_update_c_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_b_update_b_update_prod_fun$, type, C_d_prod_update_b_update_b_update_prod_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_c_d_prod_update_fun$, type, C_d_prod_update_c_d_prod_update_fun$: $tType ).
% 21.05/7.45  tff(A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$, type, A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(A_update_a_update_fun_c_update_b_update_fun_fun$, type, A_update_a_update_fun_c_update_b_update_fun_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_d_update_prod$, type, C_d_prod_update_d_update_prod$: $tType ).
% 21.05/7.45  tff(C_update_a_update_fun_d_update_a_update_fun_bool_fun_fun$, type, C_update_a_update_fun_d_update_a_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(B_a_prod_update_b_update_fun$, type, B_a_prod_update_b_update_fun$: $tType ).
% 21.05/7.45  tff(B_update_c_d_prod_update_fun_d_update_b_update_fun_fun$, type, B_update_c_d_prod_update_fun_d_update_b_update_fun_fun$: $tType ).
% 21.05/7.45  tff(B_update_d_update_fun_c_update_b_update_fun_fun$, type, B_update_d_update_fun_c_update_b_update_fun_fun$: $tType ).
% 21.05/7.45  tff(B_update_b_update_prod$, type, B_update_b_update_prod$: $tType ).
% 21.05/7.45  tff(B_update_d_update_fun_c_d_prod_update_b_update_fun_fun$, type, B_update_d_update_fun_c_d_prod_update_b_update_fun_fun$: $tType ).
% 21.05/7.45  tff(A_b_prod_update_b_update_fun$, type, A_b_prod_update_b_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_a_update_fun_c_d_prod_update_a_update_fun_bool_fun_fun$, type, C_update_a_update_fun_c_d_prod_update_a_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(B_update_b_update_bool_fun_fun$, type, B_update_b_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(B_update_d_update_fun$, type, B_update_d_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_c_update_bool_fun_fun$, type, C_update_c_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(D_update_a_update_fun_d_update_b_update_fun_bool_fun_fun$, type, D_update_a_update_fun_d_update_b_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(D_d_prod_update_b_b_prod_update_fun$, type, D_d_prod_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(A_update_a_update_bool_fun_fun$, type, A_update_a_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(C_update_b_d_prod_update_fun$, type, C_update_b_d_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_b_update_fun_c_d_prod_update_b_update_fun_bool_fun_fun$, type, C_update_b_update_fun_c_d_prod_update_b_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(A_update_d_c_prod_update_fun$, type, A_update_d_c_prod_update_fun$: $tType ).
% 21.05/7.45  tff(A_a_prod_update_b_update_fun$, type, A_a_prod_update_b_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_c_update_prod$, type, C_update_c_update_prod$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_b_update_fun_d_update_b_update_fun_bool_fun_fun$, type, C_d_prod_update_b_update_fun_d_update_b_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_b_update_bool_fun_fun$, type, C_d_prod_update_b_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(D_update_b_d_prod_update_fun$, type, D_update_b_d_prod_update_fun$: $tType ).
% 21.05/7.45  tff(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$, type, 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$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_a_update_fun_d_update_a_update_fun_bool_fun_fun$, type, C_d_prod_update_a_update_fun_d_update_a_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(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$, type, 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$: $tType ).
% 21.05/7.45  tff(A_update_b_b_prod_update_fun$, type, A_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(A_c_prod_update_b_b_prod_update_fun$, type, A_c_prod_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(A_update_b_update_fun$, type, A_update_b_update_fun$: $tType ).
% 21.05/7.45  tff(A_a_prod_update_a_a_prod_update_fun$, type, A_a_prod_update_a_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_c_prod_update$, type, C_c_prod_update$: $tType ).
% 21.05/7.45  tff(B_update_c_d_prod_update_fun$, type, B_update_c_d_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_update_c_d_prod_update_prod_b_update_b_update_prod_fun$, type, D_update_c_d_prod_update_prod_b_update_b_update_prod_fun$: $tType ).
% 21.05/7.45  tff(B_update_c_update_fun_d_update_b_update_fun_fun$, type, B_update_c_update_fun_d_update_b_update_fun_fun$: $tType ).
% 21.05/7.45  tff(C_update_a_a_prod_update_fun$, type, C_update_a_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_c_prod_update_b_b_prod_update_fun$, type, D_c_prod_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_a_update_fun$, type, C_update_a_update_fun$: $tType ).
% 21.05/7.45  tff(A_update_a_update_prod_b_update_b_update_prod_fun$, type, A_update_a_update_prod_b_update_b_update_prod_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_d_update_prod_b_update_b_update_prod_fun$, type, C_d_prod_update_d_update_prod_b_update_b_update_prod_fun$: $tType ).
% 21.05/7.45  tff(B_update_c_update_fun_c_update_b_update_fun_fun$, type, B_update_c_update_fun_c_update_b_update_fun_fun$: $tType ).
% 21.05/7.45  tff(D_update_c_update_prod_b_update_b_update_prod_fun$, type, D_update_c_update_prod_b_update_b_update_prod_fun$: $tType ).
% 21.05/7.45  tff(B_update_c_d_prod_update_fun_c_update_b_update_fun_fun$, type, B_update_c_d_prod_update_fun_c_update_b_update_fun_fun$: $tType ).
% 21.05/7.45  tff(C_update_a_update_bool_fun_fun$, type, C_update_a_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_bool_fun_fun$, type, C_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(A_d_prod_update$, type, A_d_prod_update$: $tType ).
% 21.05/7.45  tff(C_update_d_update_prod$, type, C_update_d_update_prod$: $tType ).
% 21.05/7.45  tff(D_update_a_update_fun_set$, type, D_update_a_update_fun_set$: $tType ).
% 21.05/7.45  tff(A_update_c_d_prod_update_bool_fun_fun$, type, A_update_c_d_prod_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_d_prod_update_b_b_prod_update_fun$, type, C_d_prod_d_prod_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(A_update_a_c_prod_update_fun$, type, A_update_a_c_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_c_d_prod_prod_update_a_a_prod_update_fun$, type, C_c_d_prod_prod_update_a_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_c_update_prod_a_update_a_update_prod_fun$, type, C_d_prod_update_c_update_prod_a_update_a_update_prod_fun$: $tType ).
% 21.05/7.45  tff(D_update_d_update_prod_b_update_b_update_prod_fun$, type, D_update_d_update_prod_b_update_b_update_prod_fun$: $tType ).
% 21.05/7.45  tff(D_update_b_update_bool_fun_fun$, type, D_update_b_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(B_update_b_d_prod_update_fun$, type, B_update_b_d_prod_update_fun$: $tType ).
% 21.05/7.45  tff(B_update_b_update_fun$, type, B_update_b_update_fun$: $tType ).
% 21.05/7.45  tff(B_c_prod_update$, type, B_c_prod_update$: $tType ).
% 21.05/7.45  tff(B_update$, type, B_update$: $tType ).
% 21.05/7.45  tff(D_update_c_d_prod_update_prod_a_update_a_update_prod_fun$, type, D_update_c_d_prod_update_prod_a_update_a_update_prod_fun$: $tType ).
% 21.05/7.45  tff(C_update_c_update_prod_b_update_b_update_prod_fun$, type, C_update_c_update_prod_b_update_b_update_prod_fun$: $tType ).
% 21.05/7.45  tff(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$, type, 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$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_a_update_fun_set$, type, C_d_prod_update_a_update_fun_set$: $tType ).
% 21.05/7.45  tff(D_update_set$, type, D_update_set$: $tType ).
% 21.05/7.45  tff(A_update_d_a_prod_update_fun$, type, A_update_d_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_update_a_d_prod_update_fun$, type, D_update_a_d_prod_update_fun$: $tType ).
% 21.05/7.45  tff(B_update_c_d_prod_update_fun_c_d_prod_update_b_update_fun_fun$, type, B_update_c_d_prod_update_fun_c_d_prod_update_b_update_fun_fun$: $tType ).
% 21.05/7.45  tff(C_update_c_d_prod_update_prod_a_update_a_update_prod_fun$, type, C_update_c_d_prod_update_prod_a_update_a_update_prod_fun$: $tType ).
% 21.05/7.45  tff(A_itself$, type, A_itself$: $tType ).
% 21.05/7.45  tff(A_d_prod_update_b_update_fun$, type, A_d_prod_update_b_update_fun$: $tType ).
% 21.05/7.45  tff(C_a_prod_update_b_update_fun$, type, C_a_prod_update_b_update_fun$: $tType ).
% 21.05/7.45  tff(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$, type, 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$: $tType ).
% 21.05/7.45  tff(C_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$, type, C_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(A_update_a_update_prod$, type, A_update_a_update_prod$: $tType ).
% 21.05/7.45  tff(D_a_prod_update$, type, D_a_prod_update$: $tType ).
% 21.05/7.45  tff(D_c_prod_update_a_a_prod_update_fun$, type, D_c_prod_update_a_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(A_d_prod_update_b_b_prod_update_fun$, type, A_d_prod_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_a_a_prod_update_fun$, type, C_d_prod_update_a_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_update_b_update_fun_c_d_prod_update_b_update_fun_bool_fun_fun$, type, D_update_b_update_fun_c_d_prod_update_b_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(C_c_prod_update_a_a_prod_update_fun$, type, C_c_prod_update_a_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_update_c_update_prod_a_update_a_update_prod_fun$, type, D_update_c_update_prod_a_update_a_update_prod_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$, type, C_d_prod_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(B_update_c_update_bool_fun_fun$, type, B_update_c_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(A_update_c_update_fun$, type, A_update_c_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_b_update_b_update_prod_fun$, type, C_update_b_update_b_update_prod_fun$: $tType ).
% 21.05/7.45  tff(C_update$, type, C_update$: $tType ).
% 21.05/7.45  tff(C_update_set$, type, C_update_set$: $tType ).
% 21.05/7.45  tff(D_d_prod_update_a_b_prod_update_fun$, type, D_d_prod_update_a_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(A_b_prod_update_a_update_fun$, type, A_b_prod_update_a_update_fun$: $tType ).
% 21.05/7.45  tff(B_d_prod_update$, type, B_d_prod_update$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun$, type, C_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun$: $tType ).
% 21.05/7.45  tff(C_update_b_b_prod_update_fun$, type, C_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_a_update_fun_c_update_b_update_fun_bool_fun_fun$, type, C_update_a_update_fun_c_update_b_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(B_update_d_update_bool_fun_fun$, type, B_update_d_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_a_update_fun_c_d_prod_update_a_update_fun_bool_fun_fun$, type, C_d_prod_update_a_update_fun_c_d_prod_update_a_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(D_c_d_prod_prod_update_b_b_prod_update_fun$, type, D_c_d_prod_prod_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_a_update_fun_bool_fun$, type, C_update_a_update_fun_bool_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$, type, C_d_prod_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_a_b_prod_update_fun$, type, C_d_prod_update_a_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(B_update_d_update_fun_a_update_a_update_fun_fun$, type, B_update_d_update_fun_a_update_a_update_fun_fun$: $tType ).
% 21.05/7.45  tff(A_update_b_d_prod_update_fun$, type, A_update_b_d_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_c_prod_update$, type, D_c_prod_update$: $tType ).
% 21.05/7.45  tff(D_update_bool_fun$, type, D_update_bool_fun$: $tType ).
% 21.05/7.45  tff(C_c_prod_update_b_update_fun$, type, C_c_prod_update_b_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_bool_fun$, type, C_d_prod_update_bool_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_d_update_prod_a_update_a_update_prod_fun$, type, C_d_prod_update_d_update_prod_a_update_a_update_prod_fun$: $tType ).
% 21.05/7.45  tff(B_update_c_d_prod_update_bool_fun_fun$, type, B_update_c_d_prod_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(D_update_a_b_prod_update_fun$, type, D_update_a_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(B_update_set_b_update_fun$, type, B_update_set_b_update_fun$: $tType ).
% 21.05/7.45  tff(B_update_c_d_prod_update_fun_a_update_a_update_fun_fun$, type, B_update_c_d_prod_update_fun_a_update_a_update_fun_fun$: $tType ).
% 21.05/7.45  tff(D_d_prod_update_b_update_fun$, type, D_d_prod_update_b_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_d_update_prod_b_update_b_update_prod_fun$, type, C_update_d_update_prod_b_update_b_update_prod_fun$: $tType ).
% 21.05/7.45  tff(A_update_c_d_prod_update_fun$, type, A_update_c_d_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_a_update_a_update_prod_fun$, type, C_d_prod_update_a_update_a_update_prod_fun$: $tType ).
% 21.05/7.45  tff(C_update_b_update_fun_d_update_b_update_fun_bool_fun_fun$, type, C_update_b_update_fun_d_update_b_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(D_a_prod_update_b_update_fun$, type, D_a_prod_update_b_update_fun$: $tType ).
% 21.05/7.45  tff(A_update_d_d_prod_update_fun$, type, A_update_d_d_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$, type, C_update_b_update_fun_c_update_b_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(C_update_d_update_prod_a_update_a_update_prod_fun$, type, C_update_d_update_prod_a_update_a_update_prod_fun$: $tType ).
% 21.05/7.45  tff(D_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$, type, D_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(A_a_prod_update_c_c_prod_update_fun$, type, A_a_prod_update_c_c_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_c_update_bool_fun_fun$, type, C_d_prod_update_c_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_b_b_prod_update_fun$, type, C_d_prod_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_update$, type, D_update$: $tType ).
% 21.05/7.45  tff(A_b_prod_update$, type, A_b_prod_update$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_c_d_prod_update_prod$, type, C_d_prod_update_c_d_prod_update_prod$: $tType ).
% 21.05/7.45  tff(A_update_b_update_b_update_prod_fun$, type, A_update_b_update_b_update_prod_fun$: $tType ).
% 21.05/7.45  tff(D_d_prod_update_a_a_prod_update_fun$, type, D_d_prod_update_a_a_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_update_a_update_fun$, type, D_update_a_update_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_c_update_fun$, type, C_d_prod_update_c_update_fun$: $tType ).
% 21.05/7.45  tff(D_update_c_d_prod_update_prod$, type, D_update_c_d_prod_update_prod$: $tType ).
% 21.05/7.45  tff(D_update_d_update_prod_a_update_a_update_prod_fun$, type, D_update_d_update_prod_a_update_a_update_prod_fun$: $tType ).
% 21.05/7.45  tff(A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$, type, A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$: $tType ).
% 21.05/7.45  tff(D_update_a_update_fun_d_update_b_update_fun_fun$, type, D_update_a_update_fun_d_update_b_update_fun_fun$: $tType ).
% 21.05/7.45  tff(C_d_prod_update_c_d_prod_update_bool_fun_fun$, type, C_d_prod_update_c_d_prod_update_bool_fun_fun$: $tType ).
% 21.05/7.45  tff(C_update_bool_fun$, type, C_update_bool_fun$: $tType ).
% 21.05/7.45  tff(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$, type, 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$: $tType ).
% 21.05/7.45  tff(D_update_b_b_prod_update_fun$, type, D_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(C_a_prod_update_b_b_prod_update_fun$, type, C_a_prod_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(B_update_b_b_prod_update_fun$, type, B_update_b_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(D_c_prod_update_b_update_fun$, type, D_c_prod_update_b_update_fun$: $tType ).
% 21.05/7.45  tff(C_a_prod_update_a_b_prod_update_fun$, type, C_a_prod_update_a_b_prod_update_fun$: $tType ).
% 21.05/7.45  tff(A_d_prod_update_a_update_fun$, type, A_d_prod_update_a_update_fun$: $tType ).
% 21.05/7.45  
% 21.05/7.45  %Background operators:
% 21.05/7.45  
% 21.05/7.45  
% 21.05/7.45  %Foreground operators:
% 21.05/7.45  tff(fun_app$cl, type, fun_app$cl: (D_a_prod_update_b_update_fun$ * D_a_prod_update$) > B_update$).
% 21.05/7.45  tff(register_pair$g, type, register_pair$g: (C_update_b_update_fun$ * C_update_b_update_fun$) > C_c_prod_update_b_update_fun$).
% 21.05/7.45  tff(comp$au, 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$).
% 21.05/7.45  tff(uvl$, type, uvl$: C_update_a_update_fun$ > C_update_a_a_prod_update_fun$).
% 21.05/7.45  tff(register$au, type, register$au: D_update_b_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(register_tensor$, type, register_tensor$: (C_update_a_update_fun$ * C_update_a_update_fun$) > C_c_prod_update_a_a_prod_update_fun$).
% 21.05/7.45  tff(separating$d, type, separating$d: (B_itself$ * A_update_set$) > $o).
% 21.05/7.45  tff(fun_app$az, type, fun_app$az: (B_update_a_update_fun$ * B_update$) > A_update$).
% 21.05/7.45  tff(map_fun$m, type, map_fun$m: (D_update_b_update_fun$ * C_d_prod_update_b_update_fun$) > B_update_c_d_prod_update_fun_d_update_b_update_fun_fun$).
% 21.05/7.45  tff(comp$q, 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$).
% 21.05/7.45  tff(register_pair$c, type, register_pair$c: (D_update_b_update_fun$ * D_update_b_update_fun$) > D_d_prod_update_b_update_fun$).
% 21.05/7.45  tff('#skF_46', type, '#skF_46': (C_update_b_update_fun$ * A_update_b_update_fun$ * C_update$ * A_update$) > A_update$).
% 21.05/7.45  tff(map_prod$n, 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$).
% 21.05/7.45  tff(register$ba, type, register$ba: B_update_d_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(uwd$, type, uwd$: A_update_b_update_fun_a_update_b_update_fun_bool_fun_fun$).
% 21.05/7.45  tff(top$d, type, top$d: B_update_set$).
% 21.05/7.45  tff(relcompp$g, type, relcompp$g: (C_update_a_update_bool_fun_fun$ * A_update_b_update_bool_fun_fun$) > C_update_b_update_bool_fun_fun$).
% 21.05/7.45  tff(fun_app$dq, type, fun_app$dq: (D_update_c_d_prod_update_prod_b_update_b_update_prod_fun$ * D_update_c_d_prod_update_prod$) > B_update_b_update_prod$).
% 21.05/7.45  tff('#skF_9', type, '#skF_9': (A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff('#skF_56', type, '#skF_56': (D_update_b_update_fun$ * A_update_b_update_fun$ * D_update$ * A_update$) > A_update$).
% 21.05/7.45  tff(relcompp$j, 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$).
% 21.05/7.45  tff(uvj$, type, uvj$: A_update_b_update_fun$ > A_update_b_b_prod_update_fun$).
% 21.05/7.45  tff(register$r, type, register$r: D_update_d_update_fun$ > $o).
% 21.05/7.45  tff(comp$ce, type, comp$ce: (A_update_c_d_prod_update_fun$ * B_update_a_update_fun$) > B_update_c_d_prod_update_fun$).
% 21.05/7.45  tff(register$ag, type, register$ag: C_c_prod_update_b_update_fun$ > $o).
% 21.05/7.45  tff('#skF_52', type, '#skF_52': (A_update_b_update_fun$ * D_update_b_update_fun$ * A_update$ * D_update$) > D_update$).
% 21.05/7.45  tff(separating$e, type, separating$e: (B_itself$ * C_d_prod_update_set$) > $o).
% 21.05/7.45  tff(comp$t, 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$).
% 21.05/7.45  tff(map_prod$q, 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$).
% 21.05/7.45  tff('#skF_58', type, '#skF_58': (D_update_b_update_fun$ * D_update_b_update_fun$ * D_update$ * D_update$) > D_update$).
% 21.05/7.45  tff(register_tensor$aa, 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$).
% 21.05/7.45  tff(fun_app$bm, type, fun_app$bm: (C_c_prod_update_a_b_prod_update_fun$ * C_c_prod_update$) > A_b_prod_update$).
% 21.05/7.45  tff(pred_fun$e, type, pred_fun$e: (D_update_bool_fun$ * A_update_bool_fun$) > D_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(fun_app$cf, type, fun_app$cf: (C_c_prod_update_a_update_fun$ * C_c_prod_update$) > A_update$).
% 21.05/7.45  tff(register_pair$, type, register_pair$: (C_update_a_update_fun$ * D_update_a_update_fun$) > C_d_prod_update_a_update_fun$).
% 21.05/7.45  tff(fun_app$db, type, fun_app$db: (C_update_c_update_prod_a_update_a_update_prod_fun$ * C_update_c_update_prod$) > A_update_a_update_prod$).
% 21.05/7.45  tff(fun_app$av, type, fun_app$av: (C_update_d_b_prod_update_fun$ * C_update$) > D_b_prod_update$).
% 21.05/7.45  tff('#skF_28', type, '#skF_28': (A_update_b_update_fun$ * C_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff(comp$ah, 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$).
% 21.05/7.45  tff(comp$z, type, comp$z: (C_update_b_update_fun$ * B_update_c_update_fun$) > B_update_b_update_fun$).
% 21.05/7.45  tff(comp$bw, 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$).
% 21.05/7.45  tff(comp$aa, 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$).
% 21.05/7.45  tff('#skF_83', type, '#skF_83': (D_update_a_update_fun_bool_fun$ * D_update_a_update_fun_bool_fun$) > D_update_a_update_fun$).
% 21.05/7.45  tff(register$f, type, register$f: B_update_a_update_fun$ > $o).
% 21.05/7.45  tff(uvg$, type, uvg$: A_update_b_update_fun$ > A_update_b_a_prod_update_fun$).
% 21.05/7.45  tff('#skF_105', type, '#skF_105': (B_itself$ * C_d_prod_update_set$) > C_d_prod_update_b_update_fun$).
% 21.05/7.45  tff(register_pair$b, type, register_pair$b: (A_update_b_update_fun$ * A_update_b_update_fun$) > A_a_prod_update_b_update_fun$).
% 21.05/7.45  tff(register$bh, type, register$bh: B_update_a_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(fcomp$c, type, fcomp$c: (B_update_d_update_fun_a_update_a_update_fun_fun$ * A_update_a_update_fun_c_update_b_update_fun_fun$) > B_update_d_update_fun_c_update_b_update_fun_fun$).
% 21.05/7.45  tff(collect$a, type, collect$a: D_update_bool_fun$ > D_update_set$).
% 21.05/7.45  tff(relcompp$k, type, relcompp$k: (D_update_a_update_bool_fun_fun$ * A_update_d_update_bool_fun_fun$) > D_update_d_update_bool_fun_fun$).
% 21.05/7.45  tff(compatible$h, type, compatible$h: (D_update_b_update_fun$ * C_update_b_update_fun$) > $o).
% 21.05/7.45  tff(collect$d, type, collect$d: D_update_a_update_fun_bool_fun$ > D_update_a_update_fun_set$).
% 21.05/7.45  tff(comp$bx, 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$).
% 21.05/7.45  tff('#skF_68', type, '#skF_68': (C_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(convol$a, type, convol$a: (A_update_b_update_fun$ * A_update_b_update_fun$) > A_update_b_update_b_update_prod_fun$).
% 21.05/7.45  tff('#skF_118', type, '#skF_118': (C_d_prod_update_a_update_fun$ * A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(id_update$c, type, id_update$c: B_update$).
% 21.05/7.45  tff(member$b, type, member$b: (C_update$ * C_update_set$) > $o).
% 21.05/7.45  tff(compatible$j, type, compatible$j: (B_update_b_update_fun$ * A_update_b_update_fun$) > $o).
% 21.05/7.45  tff(register$u, type, register$u: C_d_prod_update_b_update_fun$ > $o).
% 21.05/7.45  tff('#skF_11', type, '#skF_11': (A_update_b_update_fun$ * D_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff('#skF_106', type, '#skF_106': (B_itself$ * C_d_prod_update_set$ * C_d_prod_update_b_update_fun$ * C_d_prod_update_b_update_fun$) > C_d_prod_update$).
% 21.05/7.45  tff(uvn$, type, uvn$: D_update_b_update_fun$ > D_update_b_a_prod_update_fun$).
% 21.05/7.45  tff('#skF_12', type, '#skF_12': (A_update_b_update_fun$ * D_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff(fun_app$ai, type, fun_app$ai: (C_update_bool_fun$ * C_update$) > $o).
% 21.05/7.45  tff(rel_fun$al, 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$).
% 21.05/7.45  tff(map_prod$b, 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$).
% 21.05/7.45  tff(register_tensor$g, type, register_tensor$g: (C_update_b_update_fun$ * D_update_b_update_fun$) > C_d_prod_update_b_b_prod_update_fun$).
% 21.05/7.45  tff(compatible$, type, compatible$: C_update_a_update_fun$ > D_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(collect$f, type, collect$f: C_update_a_update_fun_bool_fun$ > C_update_a_update_fun_set$).
% 21.05/7.45  tff('#skF_80', type, '#skF_80': (D_update_b_update_fun$ * D_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff('#skF_5', type, '#skF_5': (C_update_b_update_fun$ * A_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff(fun_app$b, type, fun_app$b: (A_update_a_d_prod_update_fun$ * A_update$) > A_d_prod_update$).
% 21.05/7.45  tff(rel_fun$ak, 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$).
% 21.05/7.45  tff(fun_app$ao, type, fun_app$ao: (B_update_b_update_bool_fun_fun$ * B_update$) > B_update_bool_fun$).
% 21.05/7.45  tff(fun_app$dp, 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$).
% 21.05/7.45  tff(tensor_update$, type, tensor_update$: B_update$ > A_update_b_a_prod_update_fun$).
% 21.05/7.45  tff(fun_app$df, 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$).
% 21.05/7.45  tff(register$ao, type, register$ao: D_update_b_d_prod_update_fun$ > $o).
% 21.05/7.45  tff(fun_app$du, type, fun_app$du: (B_update_c_update_fun_c_d_prod_update_b_update_fun_fun$ * B_update_c_update_fun$) > C_d_prod_update_b_update_fun$).
% 21.05/7.45  tff(fun_app$s, type, fun_app$s: (C_update_b_a_prod_update_fun$ * C_update$) > B_a_prod_update$).
% 21.05/7.45  tff('#skF_25', type, '#skF_25': (C_update_b_update_fun$ * A_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff(fun_app$co, 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$).
% 21.05/7.45  tff('#skF_59', type, '#skF_59': (C_update_a_update_fun$ * D_update_a_update_fun$ * C_update$ * D_update$) > C_update$).
% 21.05/7.45  tff(register_pair$p, type, register_pair$p: (B_update_c_update_fun$ * A_update_c_update_fun$ * B_a_prod_update$) > C_update$).
% 21.05/7.45  tff(fun_app$a, type, fun_app$a: (A_update_b_a_prod_update_fun$ * A_update$) > B_a_prod_update$).
% 21.05/7.45  tff(comp$bg, type, comp$bg: (C_update_a_update_a_update_prod_fun$ * D_update_c_update_fun$) > D_update_a_update_a_update_prod_fun$).
% 21.05/7.45  tff(rel_fun$r, 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$).
% 21.05/7.45  tff('#skF_54', type, '#skF_54': (D_update_b_update_fun$ * C_update_b_update_fun$ * D_update$ * C_update$) > C_update$).
% 21.05/7.45  tff(type_definition$c, type, type_definition$c: (C_update_d_update_fun$ * D_update_c_update_fun$ * D_update_set$) > $o).
% 21.05/7.45  tff('#skF_91', type, '#skF_91': (A_itself$ * D_update_set$ * D_update_a_update_fun$ * D_update_a_update_fun$) > D_update$).
% 21.05/7.45  tff(comp$az, type, comp$az: (C_d_prod_update_a_update_fun$ * C_update_c_d_prod_update_fun$) > C_update_a_update_fun$).
% 21.05/7.45  tff(tensor_update$i, type, tensor_update$i: (D_update$ * B_update$) > D_b_prod_update$).
% 21.05/7.45  tff(compatible$i, type, compatible$i: (C_update_b_update_fun$ * A_update_b_update_fun$) > $o).
% 21.05/7.45  tff(type_definition$e, type, type_definition$e: (D_update_d_update_fun$ * D_update_d_update_fun$ * D_update_set$) > $o).
% 21.05/7.45  tff(rel_fun$u, 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).
% 21.05/7.45  tff(register_tensor$d, type, register_tensor$d: (C_update_b_update_fun$ * C_update_a_update_fun$) > C_c_prod_update_b_a_prod_update_fun$).
% 21.05/7.45  tff(fun_app$ct, 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$).
% 21.05/7.45  tff('#skF_27', type, '#skF_27': (A_update_b_update_fun$ * C_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(relcompp$c, 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$).
% 21.05/7.45  tff(register$, type, register$: C_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(fun_app$bx, type, fun_app$bx: (C_update_c_update_fun$ * C_update$) > C_update$).
% 21.05/7.45  tff(fun_app$aj, type, fun_app$aj: (A_update_bool_fun$ * A_update$) > $o).
% 21.05/7.45  tff(fun_app$bw, 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$).
% 21.05/7.45  tff(preregister$g, type, preregister$g: A_update_c_update_fun$ > $o).
% 21.05/7.45  tff(collect$, type, collect$: C_d_prod_update_bool_fun$ > C_d_prod_update_set$).
% 21.05/7.45  tff(fun_app$bh, type, fun_app$bh: (D_update_c_update_fun$ * D_update$) > C_update$).
% 21.05/7.45  tff(type_definition$b, type, type_definition$b: (C_update_c_update_fun$ * C_update_c_update_fun$ * C_update_set$) > $o).
% 21.05/7.45  tff(map_prod$p, 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$).
% 21.05/7.45  tff(comp$aw, 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$).
% 21.05/7.45  tff(collect$b, type, collect$b: C_update_bool_fun$ > C_update_set$).
% 21.05/7.45  tff(comp$an, type, comp$an: (D_update_b_update_fun$ * C_update_d_update_fun$) > C_update_b_update_fun$).
% 21.05/7.45  tff('#skF_30', type, '#skF_30': (A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(comp$bj, type, comp$bj: (A_update_b_update_b_update_prod_fun$ * C_update_a_update_fun$) > C_update_b_update_b_update_prod_fun$).
% 21.05/7.45  tff(convol$f, type, convol$f: (C_d_prod_update_a_update_fun$ * C_d_prod_update_a_update_fun$) > C_d_prod_update_a_update_a_update_prod_fun$).
% 21.05/7.45  tff(register_pair$q, type, register_pair$q: (A_update_d_update_fun$ * D_update_d_update_fun$ * A_d_prod_update$) > D_update$).
% 21.05/7.45  tff(register$l, type, register$l: C_c_prod_update_b_a_prod_update_fun$ > $o).
% 21.05/7.45  tff('#skF_18', type, '#skF_18': (D_update_b_update_fun$ * D_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff(compatible$ar, type, compatible$ar: (C_update_a_b_prod_update_fun$ * D_update_a_b_prod_update_fun$) > $o).
% 21.05/7.45  tff(fun_app$cb, type, fun_app$cb: (B_update_c_update_fun$ * B_update$) > C_update$).
% 21.05/7.45  tff(register_pair$v, 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$).
% 21.05/7.45  tff(register_tensor$z, 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$).
% 21.05/7.45  tff(fun_app$q, type, fun_app$q: (C_update_b_update_fun$ * C_update$) > B_update$).
% 21.05/7.45  tff(map_fun$c, 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$).
% 21.05/7.45  tff(uut$, type, uut$: D_update_b_update_fun$ > D_update_d_b_prod_update_fun$).
% 21.05/7.45  tff(fun_app$bd, type, fun_app$bd: (A_update_a_update_fun$ * A_update$) > A_update$).
% 21.05/7.45  tff(member$f, type, member$f: (C_update_a_update_fun$ * C_update_a_update_fun_set$) > $o).
% 21.05/7.45  tff(register_tensor$v, type, register_tensor$v: (D_update_a_update_fun$ * C_d_prod_update_a_update_fun$) > D_c_d_prod_prod_update_a_a_prod_update_fun$).
% 21.05/7.45  tff(register_tensor$x, 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$).
% 21.05/7.45  tff('#skF_86', type, '#skF_86': (C_d_prod_update_a_update_fun_bool_fun$ * C_d_prod_update_a_update_fun_bool_fun$) > C_d_prod_update_a_update_fun$).
% 21.05/7.45  tff(fun_app$am, type, fun_app$am: (C_update_c_update_bool_fun_fun$ * C_update$) > C_update_bool_fun$).
% 21.05/7.45  tff(comp_update$, type, comp_update$: A_update$ > A_update_a_update_fun$).
% 21.05/7.45  tff(register$ac, type, register$ac: A_a_prod_update_b_update_fun$ > $o).
% 21.05/7.45  tff(map_fun$k, type, map_fun$k: (D_update_a_update_fun$ * A_update_b_update_fun$) > A_update_a_update_fun_d_update_b_update_fun_fun$).
% 21.05/7.45  tff(comp$d, type, comp$d: (B_update_b_update_fun$ * C_update_b_update_fun$) > C_update_b_update_fun$).
% 21.05/7.45  tff(fun_app$j, type, fun_app$j: (D_update_a_update_fun_bool_fun$ * D_update_a_update_fun$) > $o).
% 21.05/7.45  tff('#skF_10', type, '#skF_10': (A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(register$b, type, register$b: A_update_a_update_fun$ > $o).
% 21.05/7.45  tff(register$an, type, register$an: A_update_b_d_prod_update_fun$ > $o).
% 21.05/7.45  tff(comp$bv, type, comp$bv: (A_update_a_update_prod_b_update_b_update_prod_fun$ * C_update_c_d_prod_update_prod_a_update_a_update_prod_fun$) > C_update_c_d_prod_update_prod_b_update_b_update_prod_fun$).
% 21.05/7.45  tff(compatible$m, type, compatible$m: C_update_a_update_fun$ > C_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(uur$, type, uur$: C_update_b_update_fun$ > C_update_d_b_prod_update_fun$).
% 21.05/7.45  tff(fun_app$n, type, fun_app$n: (D_update_b_b_prod_update_fun$ * D_update$) > B_b_prod_update$).
% 21.05/7.45  tff(comp$u, 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$).
% 21.05/7.45  tff(uug$, type, uug$: C_update_b_update_fun$ > C_update_b_d_prod_update_fun$).
% 21.05/7.45  tff(convol$b, type, convol$b: (C_update_a_update_fun$ * C_update_a_update_fun$) > C_update_a_update_a_update_prod_fun$).
% 21.05/7.45  tff(tensor_update$e, type, tensor_update$e: (B_update$ * D_update$) > B_d_prod_update$).
% 21.05/7.45  tff(preregister$, type, preregister$: C_d_prod_update_b_update_fun$ > $o).
% 21.05/7.45  tff(preregister$l, type, preregister$l: C_d_prod_update_c_d_prod_update_fun$ > $o).
% 21.05/7.45  tff(tensor_update$c, type, tensor_update$c: A_update$ > B_update_a_b_prod_update_fun$).
% 21.05/7.45  tff('#skF_121', type, '#skF_121': (C_d_prod_update_a_update_fun$ * C_d_prod_update_a_update_fun$ * A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(register_tensor$ae, type, register_tensor$ae: (A_update_a_update_fun$ * A_update_a_update_fun$) > A_a_prod_update_a_a_prod_update_fun$).
% 21.05/7.45  tff(register$bm, type, register$bm: A_update_a_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(uud$, type, uud$: D_update_a_update_fun_set$ > D_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(map_fun$e, 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$).
% 21.05/7.45  tff(register_tensor$w, 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$).
% 21.05/7.45  tff(fun_app$bp, type, fun_app$bp: (C_c_prod_update_b_a_prod_update_fun$ * C_c_prod_update$) > B_a_prod_update$).
% 21.05/7.45  tff(quotient$b, 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).
% 21.05/7.45  tff(register$x, type, register$x: C_update_c_update_fun$ > $o).
% 21.05/7.45  tff(register$bl, type, register$bl: A_update_a_c_prod_update_fun$ > $o).
% 21.05/7.45  tff(fun_app$t, type, fun_app$t: (C_update_a_b_prod_update_fun$ * C_update$) > A_b_prod_update$).
% 21.05/7.45  tff(comp$ax, 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$).
% 21.05/7.45  tff(compatible$ap, type, compatible$ap: (A_update_b_b_prod_update_fun$ * C_update_b_b_prod_update_fun$) > $o).
% 21.05/7.45  tff(fun_app$r, type, fun_app$r: (C_update_b_b_prod_update_fun$ * C_update$) > B_b_prod_update$).
% 21.05/7.45  tff(preregister$f, type, preregister$f: A_update_d_update_fun$ > $o).
% 21.05/7.45  tff(fun_app$bo, type, fun_app$bo: (C_d_prod_update_a_b_prod_update_fun$ * C_d_prod_update$) > A_b_prod_update$).
% 21.05/7.45  tff(fcomp$f, type, fcomp$f: (C_d_prod_update_a_update_fun$ * A_update_b_update_fun$) > C_d_prod_update_b_update_fun$).
% 21.05/7.45  tff(register$p, type, register$p: A_c_prod_update_b_a_prod_update_fun$ > $o).
% 21.05/7.45  tff(register_tensor$a, type, register_tensor$a: (C_update_a_update_fun$ * C_update_b_update_fun$) > C_c_prod_update_a_b_prod_update_fun$).
% 21.05/7.45  tff(comp$bc, type, comp$bc: (C_update_a_update_fun$ * C_d_prod_update_c_update_fun$) > C_d_prod_update_a_update_fun$).
% 21.05/7.45  tff(image$a, type, image$a: (D_update_a_update_fun$ * D_update_set$) > A_update_set$).
% 21.05/7.45  tff('#skF_61', type, '#skF_61': (C_d_prod_update_b_update_fun$ * C_d_prod_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff(compatible$r, type, compatible$r: B_update_a_update_fun$ > D_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(uvo$, type, uvo$: C_update_b_update_fun$ > C_update_a_b_prod_update_fun$).
% 21.05/7.45  tff(rel_fun$ah, 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$).
% 21.05/7.45  tff(fun_app$cj, type, fun_app$cj: (A_a_prod_update_b_update_fun$ * A_a_prod_update$) > B_update$).
% 21.05/7.45  tff('#skF_104', type, '#skF_104': (B_itself$ * C_d_prod_update_set$) > C_d_prod_update_b_update_fun$).
% 21.05/7.45  tff('#skF_102', type, '#skF_102': (B_itself$ * A_update_set$) > A_update_b_update_fun$).
% 21.05/7.45  tff(register_tensor$c, type, register_tensor$c: (C_update_a_update_fun$ * D_update_b_update_fun$) > C_d_prod_update_a_b_prod_update_fun$).
% 21.05/7.45  tff(register$a, type, register$a: A_update_b_update_fun$ > $o).
% 21.05/7.45  tff('#skF_95', type, '#skF_95': (A_itself$ * C_update_set$) > C_update_a_update_fun$).
% 21.05/7.45  tff('#skF_29', type, '#skF_29': (A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(fun_app$ds, 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$).
% 21.05/7.45  tff(register$bb, type, register$bb: B_update_d_a_prod_update_fun$ > $o).
% 21.05/7.45  tff(register$aj, type, register$aj: D_a_prod_update_b_update_fun$ > $o).
% 21.05/7.45  tff(uus$, type, uus$: A_update_b_update_fun$ > A_update_d_b_prod_update_fun$).
% 21.05/7.45  tff(uve$, type, uve$: A_update_a_a_prod_update_fun$).
% 21.05/7.45  tff(uvs$, type, uvs$: B_update$ > A_update_b_update_fun$).
% 21.05/7.45  tff('#skF_69', type, '#skF_69': (A_update_b_update_fun$ * C_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(fun_app$by, type, fun_app$by: (C_d_prod_update_a_update_fun$ * C_d_prod_update$) > A_update$).
% 21.05/7.45  tff(relcompp$h, type, relcompp$h: (C_d_prod_update_a_update_bool_fun_fun$ * A_update_c_d_prod_update_bool_fun_fun$) > C_d_prod_update_c_d_prod_update_bool_fun_fun$).
% 21.05/7.45  tff(register_tensor$ab, 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$).
% 21.05/7.45  tff(rel_fun$ae, type, rel_fun$ae: (D_update_c_d_prod_update_bool_fun_fun$ * A_update_a_update_bool_fun_fun$) > D_update_a_update_fun_c_d_prod_update_a_update_fun_bool_fun_fun$).
% 21.05/7.45  tff('#skF_31', type, '#skF_31': (A_update_b_update_fun$ * D_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(comp$w, type, comp$w: (C_d_prod_update_b_update_fun$ * C_d_prod_update_c_d_prod_update_fun$) > C_d_prod_update_b_update_fun$).
% 21.05/7.45  tff(preregister$m, type, preregister$m: D_update_d_update_fun$ > $o).
% 21.05/7.45  tff(fun_app$bt, type, fun_app$bt: (A_c_prod_update_b_a_prod_update_fun$ * A_c_prod_update$) > B_a_prod_update$).
% 21.05/7.45  tff(fun_app$ab, type, fun_app$ab: (A_update_c_d_prod_update_fun$ * A_update$) > C_d_prod_update$).
% 21.05/7.45  tff('#skF_23', type, '#skF_23': (C_update_b_update_fun$ * C_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff(register_pair$n, type, register_pair$n: (B_update_a_update_fun$ * A_update_a_update_fun$ * B_a_prod_update$) > A_update$).
% 21.05/7.45  tff(quotient$a, 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).
% 21.05/7.45  tff(separating$c, type, separating$c: (B_itself$ * B_update_set$) > $o).
% 21.05/7.45  tff(rel_fun$e, 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).
% 21.05/7.45  tff(compatible$l, type, compatible$l: (B_update_a_update_fun$ * A_update_a_update_fun$) > $o).
% 21.05/7.45  tff(uvu$, type, uvu$: C_d_prod_update_bool_fun$).
% 21.05/7.45  tff(fun_app$cg, type, fun_app$cg: (C_c_prod_update_b_update_fun$ * C_c_prod_update$) > B_update$).
% 21.05/7.45  tff(member$g, type, member$g: (B_update$ * B_update_set$) > $o).
% 21.05/7.45  tff(type_definition$h, type, type_definition$h: (A_update_d_update_fun$ * D_update_a_update_fun$ * D_update_set$) > $o).
% 21.05/7.45  tff('#skF_47', type, '#skF_47': (A_update_b_update_fun$ * C_update_b_update_fun$ * A_update$ * C_update$) > A_update$).
% 21.05/7.45  tff(register_pair$w, type, register_pair$w: (A_update_b_a_prod_update_fun$ * C_update_b_a_prod_update_fun$) > A_c_prod_update_b_a_prod_update_fun$).
% 21.05/7.45  tff('#skF_116', type, '#skF_116': (D_update_a_update_fun$ * D_update_a_update_fun$ * A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(rel_fun$z, type, rel_fun$z: (D_update_a_update_fun_c_update_a_update_fun_bool_fun_fun$ * D_update_b_update_fun_c_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$).
% 21.05/7.45  tff(uwe$, type, uwe$: A_update_a_update_bool_fun_fun$).
% 21.05/7.45  tff(compatible$y, type, compatible$y: (A_update_c_update_fun$ * D_update_c_update_fun$) > $o).
% 21.05/7.45  tff(compatible$w, type, compatible$w: (B_update_c_update_fun$ * A_update_c_update_fun$) > $o).
% 21.05/7.45  tff(fun_app$k, type, fun_app$k: (C_update_a_update_fun_bool_fun$ * C_update_a_update_fun$) > $o).
% 21.05/7.45  tff(uub$, type, uub$: C_update_set$ > C_update_bool_fun$).
% 21.05/7.45  tff(comp$bf, type, comp$bf: (C_update_b_update_b_update_prod_fun$ * A_update_c_update_fun$) > A_update_b_update_b_update_prod_fun$).
% 21.05/7.45  tff(comp$r, type, comp$r: (A_b_prod_update_b_update_fun$ * C_c_prod_update_a_b_prod_update_fun$) > C_c_prod_update_b_update_fun$).
% 21.05/7.45  tff(id_update$, type, id_update$: A_update$).
% 21.05/7.45  tff('#skF_34', type, '#skF_34': (D_update_b_update_fun$ * C_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff(compatible$aq, type, compatible$aq: (C_update_a_b_prod_update_fun$ * A_update_a_b_prod_update_fun$) > $o).
% 21.05/7.45  tff('#skF_122', type, '#skF_122': (D_update_a_update_fun$ * D_update_a_update_fun$ * A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff('#skF_41', type, '#skF_41': (C_update_a_update_fun$ * C_update_a_update_fun$ * C_update$ * C_update$) > C_update$).
% 21.05/7.45  tff(tensor_update$b, type, tensor_update$b: A_update$ > C_update_a_c_prod_update_fun$).
% 21.05/7.45  tff(compatible$n, type, compatible$n: (C_update_b_update_fun$ * C_update_b_update_fun$) > $o).
% 21.05/7.45  tff(register_tensor$b, type, register_tensor$b: (C_update_a_update_fun$ * A_update_b_update_fun$) > C_a_prod_update_a_b_prod_update_fun$).
% 21.05/7.45  tff(comp$i, type, comp$i: (C_update_b_update_fun$ * A_update_c_update_fun$) > A_update_b_update_fun$).
% 21.05/7.45  tff(separating$a, type, separating$a: (B_itself$ * C_update_set$) > $o).
% 21.05/7.45  tff(register$al, type, register$al: C_update_d_update_fun$ > $o).
% 21.05/7.45  tff(comp$bn, 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$).
% 21.05/7.45  tff(quotient$l, 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).
% 21.05/7.45  tff(fun_app$cx, type, fun_app$cx: (C_update_d_update_fun$ * C_update$) > D_update$).
% 21.05/7.45  tff(map_prod$, type, map_prod$: (A_update_b_update_fun$ * A_update_b_update_fun$) > A_update_a_update_prod_b_update_b_update_prod_fun$).
% 21.05/7.45  tff(compatible$o, type, compatible$o: (A_update_b_update_fun$ * D_update_b_update_fun$) > $o).
% 21.05/7.45  tff(register$c, type, register$c: C_update_b_update_fun$ > $o).
% 21.05/7.45  tff(comp_update$j, type, comp_update$j: (D_c_prod_update$ * D_c_prod_update$) > D_c_prod_update$).
% 21.05/7.45  tff(comp$af, 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$).
% 21.05/7.45  tff(register_pair$r, type, register_pair$r: (A_update_c_update_fun$ * D_update_c_update_fun$ * A_d_prod_update$) > C_update$).
% 21.05/7.45  tff(fcomp$d, 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$).
% 21.05/7.45  tff(register_tensor$e, type, register_tensor$e: (C_update_b_update_fun$ * C_update_b_update_fun$) > C_c_prod_update_b_b_prod_update_fun$).
% 21.05/7.45  tff('#skF_77', type, '#skF_77': (D_update_b_update_fun$ * A_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff('#skF_19', type, '#skF_19': (C_update_a_update_fun$ * D_update_a_update_fun$) > C_update$).
% 21.05/7.45  tff('#skF_94', type, '#skF_94': (B_itself$ * C_update_set$ * C_update_b_update_fun$ * C_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff(register$as, type, register$as: C_update_b_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(compatible$ah, type, compatible$ah: (C_update_b_a_prod_update_fun$ * C_update_b_a_prod_update_fun$) > $o).
% 21.05/7.45  tff(map_fun$, type, map_fun$: (C_update_a_update_fun$ * A_update_b_update_fun$) > A_update_a_update_fun_c_update_b_update_fun_fun$).
% 21.05/7.45  tff(register_tensor$o, type, register_tensor$o: (A_update_b_update_fun$ * D_update_a_update_fun$) > A_d_prod_update_b_a_prod_update_fun$).
% 21.05/7.45  tff('#skF_113', type, '#skF_113': (C_d_prod_update_a_update_fun$ * C_d_prod_update_a_update_fun$ * A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(conversep$b, type, conversep$b: C_d_prod_update_a_update_bool_fun_fun$ > A_update_c_d_prod_update_bool_fun_fun$).
% 21.05/7.45  tff(fun_app$bq, type, fun_app$bq: (C_c_prod_update_b_b_prod_update_fun$ * C_c_prod_update$) > B_b_prod_update$).
% 21.05/7.45  tff(register_tensor$l, type, register_tensor$l: (D_update_a_update_fun$ * C_update_b_update_fun$) > D_c_prod_update_a_b_prod_update_fun$).
% 21.05/7.45  tff(preregister$e, type, preregister$e: B_update_a_update_fun$ > $o).
% 21.05/7.45  tff(uvi$, type, uvi$: C_update_a_update_fun$ > C_update_b_a_prod_update_fun$).
% 21.05/7.45  tff('#skF_108', type, '#skF_108': (C_update_a_update_fun$ * C_update_set$ * A_update_b_update_fun$ * A_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff(comp$bt, type, comp$bt: (B_update_bool_fun$ * A_update_b_update_fun$) > A_update_bool_fun$).
% 21.05/7.45  tff(uvz$, type, uvz$: D_update_d_update_bool_fun_fun$).
% 21.05/7.45  tff(register$ay, type, register$ay: A_update_d_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(fun_app$ag, type, fun_app$ag: (C_d_prod_update_bool_fun$ * C_d_prod_update$) > $o).
% 21.05/7.45  tff(register$bj, type, register$bj: B_update_b_a_prod_update_fun$ > $o).
% 21.05/7.45  tff(comp$a, type, comp$a: A_update_b_update_fun_c_d_prod_update_a_update_fun_c_d_prod_update_b_update_fun_fun_fun$).
% 21.05/7.45  tff(rel_fun$ab, 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$).
% 21.05/7.45  tff(type_definition$, type, type_definition$: (A_update_a_update_fun$ * A_update_a_update_fun$ * A_update_set$) > $o).
% 21.05/7.45  tff('#skF_79', type, '#skF_79': (D_update_b_update_fun$ * D_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff(comp$al, type, comp$al: (C_update_b_update_fun$ * D_update_c_update_fun$) > D_update_b_update_fun$).
% 21.05/7.45  tff('#skF_103', type, '#skF_103': (B_itself$ * A_update_set$ * A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(collect$e, type, collect$e: C_d_prod_update_a_update_fun_bool_fun$ > C_d_prod_update_a_update_fun_set$).
% 21.05/7.45  tff('#skF_32', type, '#skF_32': (A_update_b_update_fun$ * D_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff(preregister$o, type, preregister$o: C_update_c_update_fun$ > $o).
% 21.05/7.45  tff(rel_fun$b, 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$).
% 21.05/7.45  tff(preregister$a, type, preregister$a: C_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(quotient$g, 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).
% 21.05/7.45  tff('#skF_111', type, '#skF_111': (C_update_a_update_fun$ * C_update_a_update_fun$ * A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(fun_app$m, type, fun_app$m: (D_update_b_update_fun$ * D_update$) > B_update$).
% 21.05/7.45  tff(fun_app$bj, 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$).
% 21.05/7.45  tff(relcompp$e, type, relcompp$e: (C_update_a_update_bool_fun_fun$ * A_update_c_update_bool_fun_fun$) > C_update_c_update_bool_fun_fun$).
% 21.05/7.45  tff(top$a, type, top$a: D_update_set$).
% 21.05/7.45  tff('#skF_40', type, '#skF_40': (C_update_a_update_fun$ * D_update_a_update_fun$) > D_update$).
% 21.05/7.45  tff('#skF_60', type, '#skF_60': (C_update_a_update_fun$ * D_update_a_update_fun$ * C_update$ * D_update$) > D_update$).
% 21.05/7.45  tff('#skF_71', type, '#skF_71': (A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(comp$aq, type, comp$aq: (A_update_a_update_fun$ * B_update_a_update_fun$) > B_update_a_update_fun$).
% 21.05/7.45  tff(comp$s, 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$).
% 21.05/7.45  tff(fun_app$bi, type, fun_app$bi: (B_update_d_update_fun$ * B_update$) > D_update$).
% 21.05/7.45  tff('#skF_51', type, '#skF_51': (A_update_b_update_fun$ * D_update_b_update_fun$ * A_update$ * D_update$) > A_update$).
% 21.05/7.45  tff(quotient$e, 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).
% 21.05/7.45  tff(compatible$x, type, compatible$x: (A_update_d_update_fun$ * D_update_d_update_fun$) > $o).
% 21.05/7.45  tff(register_tensor$af, type, register_tensor$af: (A_update_b_update_fun$ * D_update_b_update_fun$) > A_d_prod_update_b_b_prod_update_fun$).
% 21.05/7.45  tff(comp$ak, type, comp$ak: (C_update_a_update_fun$ * A_update_c_update_fun$) > A_update_a_update_fun$).
% 21.05/7.45  tff(comp$bi, type, comp$bi: (A_update_b_update_b_update_prod_fun$ * A_update_a_update_fun$) > A_update_b_update_b_update_prod_fun$).
% 21.05/7.45  tff(comp$e, type, comp$e: (C_update_a_update_fun$ * C_update_c_update_fun$) > C_update_a_update_fun$).
% 21.05/7.45  tff(tensor_update$d, type, tensor_update$d: A_update$ > A_update_a_a_prod_update_fun$).
% 21.05/7.45  tff(quotient$j, 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).
% 21.05/7.45  tff(comp_update$e, type, comp_update$e: (B_d_prod_update$ * B_d_prod_update$) > B_d_prod_update$).
% 21.05/7.45  tff(grp$a, 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$).
% 21.05/7.45  tff(fun_app$dv, type, fun_app$dv: (B_update_c_d_prod_update_fun_c_d_prod_update_b_update_fun_fun$ * B_update_c_d_prod_update_fun$) > C_d_prod_update_b_update_fun$).
% 21.05/7.45  tff(fun_app$di, type, fun_app$di: (C_d_prod_update_c_update_prod_b_update_b_update_prod_fun$ * C_d_prod_update_c_update_prod$) > B_update_b_update_prod$).
% 21.05/7.45  tff(register_tensor$t, type, register_tensor$t: (C_d_prod_update_a_update_fun$ * D_update_a_update_fun$) > C_d_prod_d_prod_update_a_a_prod_update_fun$).
% 21.05/7.45  tff(comp$as, type, comp$as: (C_update_a_update_fun$ * D_update_c_update_fun$) > D_update_a_update_fun$).
% 21.05/7.45  tff(comp$l, 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$).
% 21.05/7.45  tff(id$, type, id$: B_update_b_update_fun$).
% 21.05/7.45  tff(fun_app$v, type, fun_app$v: (C_update_a_a_prod_update_fun$ * C_update$) > A_a_prod_update$).
% 21.05/7.45  tff(fun_app$ad, type, fun_app$ad: (A_update_b_d_prod_update_fun$ * A_update$) > B_d_prod_update$).
% 21.05/7.45  tff(register_tensor$q, type, register_tensor$q: (D_update_b_update_fun$ * D_update_b_update_fun$) > D_d_prod_update_b_b_prod_update_fun$).
% 21.05/7.45  tff(register$i, type, register$i: C_c_prod_update_a_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(register_tensor$ad, type, register_tensor$ad: (A_update_c_update_fun$ * A_update_c_update_fun$) > A_a_prod_update_c_c_prod_update_fun$).
% 21.05/7.45  tff(fun_app$at, type, fun_app$at: (D_update_a_b_prod_update_fun$ * D_update$) > A_b_prod_update$).
% 21.05/7.45  tff(comp$ar, type, comp$ar: (D_update_a_update_fun$ * A_update_d_update_fun$) > A_update_a_update_fun$).
% 21.05/7.45  tff(preregister$p, type, preregister$p: B_update_c_update_fun$ > $o).
% 21.05/7.45  tff(quotient$c, 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).
% 21.05/7.45  tff(quotient$f, 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).
% 21.05/7.45  tff(comp_update$i, type, comp_update$i: (D_d_prod_update$ * D_d_prod_update$) > D_d_prod_update$).
% 21.05/7.45  tff('#skF_93', type, '#skF_93': (B_itself$ * C_update_set$) > C_update_b_update_fun$).
% 21.05/7.45  tff(rel_fun$l, type, rel_fun$l: (C_update_d_update_bool_fun_fun$ * B_update_b_update_bool_fun_fun$) > C_update_b_update_fun_d_update_b_update_fun_bool_fun_fun$).
% 21.05/7.45  tff(register_tensor$j, type, register_tensor$j: (D_update_a_update_fun$ * D_update_a_update_fun$) > D_d_prod_update_a_a_prod_update_fun$).
% 21.05/7.45  tff(comp$cb, 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$).
% 21.05/7.45  tff('#skF_26', type, '#skF_26': (C_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(register_pair$x, 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$).
% 21.05/7.45  tff(fun_app$da, 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$).
% 21.05/7.45  tff(uwc$, type, uwc$: A_update_set$ > D_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(register$ab, type, register$ab: A_b_prod_update_b_update_fun$ > $o).
% 21.05/7.45  tff(comp$n, 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$).
% 21.05/7.45  tff(fun_app$bc, type, fun_app$bc: (A_update_d_a_prod_update_fun$ * A_update$) > D_a_prod_update$).
% 21.05/7.45  tff(fun_app$aq, type, fun_app$aq: (A_update_b_update_fun_bool_fun$ * A_update_b_update_fun$) > $o).
% 21.05/7.45  tff(comp$ab, 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$).
% 21.05/7.45  tff(top$c, type, top$c: A_update_set$).
% 21.05/7.45  tff(rel_fun$q, 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).
% 21.05/7.45  tff(uva$, type, uva$: B_update_b_a_prod_update_fun$).
% 21.05/7.45  tff(fun_app$dr, 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$).
% 21.05/7.45  tff(rel_fun$aa, 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$).
% 21.05/7.45  tff(convol$c, type, convol$c: (D_update_a_update_fun$ * D_update_a_update_fun$) > D_update_a_update_a_update_prod_fun$).
% 21.05/7.45  tff(compatible$d, type, compatible$d: A_update_a_update_fun$ > D_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(rel_fun$, 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).
% 21.05/7.45  tff(pred_fun$b, type, pred_fun$b: (C_d_prod_update_bool_fun$ * B_update_bool_fun$ * C_d_prod_update_b_update_fun$) > $o).
% 21.05/7.45  tff(preregister$h, type, preregister$h: A_update_a_update_fun$ > $o).
% 21.05/7.45  tff(preregister$k, type, preregister$k: B_update_b_update_fun$ > $o).
% 21.05/7.45  tff(type_definition$j, type, type_definition$j: (B_update_d_update_fun$ * D_update_b_update_fun$ * D_update_set$) > $o).
% 21.05/7.45  tff(register_tensor$s, type, register_tensor$s: (C_update_a_update_fun$ * D_update_a_update_fun$) > C_d_prod_update_a_a_prod_update_fun$).
% 21.05/7.45  tff(rel_fun$i, 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).
% 21.05/7.45  tff(compatible$f, type, compatible$f: (C_update_b_update_fun$ * D_update_b_update_fun$) > $o).
% 21.05/7.45  tff(register_tensor$k, type, register_tensor$k: (D_update_a_update_fun$ * C_update_a_update_fun$) > D_c_prod_update_a_a_prod_update_fun$).
% 21.05/7.45  tff(rel_fun$c, type, rel_fun$c: (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$).
% 21.05/7.45  tff(quotient$d, 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).
% 21.05/7.45  tff(fun_app$bu, type, fun_app$bu: (A_c_prod_update_b_b_prod_update_fun$ * A_c_prod_update$) > B_b_prod_update$).
% 21.05/7.45  tff(fun_app$x, type, fun_app$x: (B_update_b_update_fun$ * B_update$) > B_update$).
% 21.05/7.45  tff('#skF_22', type, '#skF_22': (C_update_a_update_fun$ * C_update_a_update_fun$) > C_update$).
% 21.05/7.45  tff(register$am, type, register$am: C_update_b_d_prod_update_fun$ > $o).
% 21.05/7.45  tff(uwb$, type, uwb$: A_update_set$ > C_d_prod_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(uwf$, type, uwf$: B_update_b_update_bool_fun_fun$).
% 21.05/7.45  tff(fun_app$dk, type, fun_app$dk: (C_d_prod_update_c_d_prod_update_prod_b_update_b_update_prod_fun$ * C_d_prod_update_c_d_prod_update_prod$) > B_update_b_update_prod$).
% 21.05/7.45  tff(grp$b, 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$).
% 21.05/7.45  tff(rel_fun$ag, 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).
% 21.05/7.45  tff(fun_app$cm, type, fun_app$cm: (D_d_prod_update_b_update_fun$ * D_d_prod_update$) > B_update$).
% 21.05/7.45  tff(fun_app$dg, 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$).
% 21.05/7.45  tff('#skF_90', type, '#skF_90': (A_itself$ * D_update_set$) > D_update_a_update_fun$).
% 21.05/7.45  tff(fun_app$ak, 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$).
% 21.05/7.45  tff(fun_app$al, type, fun_app$al: (D_update_d_update_bool_fun_fun$ * D_update$) > D_update_bool_fun$).
% 21.05/7.45  tff(map_prod$d, 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$).
% 21.05/7.45  tff(register$ai, type, register$ai: D_c_prod_update_b_update_fun$ > $o).
% 21.05/7.45  tff(compatible$aj, type, compatible$aj: (C_update_b_a_prod_update_fun$ * D_update_b_a_prod_update_fun$) > $o).
% 21.05/7.45  tff(fun_app$cu, 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$).
% 21.05/7.45  tff(quotient$m, 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).
% 21.05/7.45  tff(register$t, type, register$t: B_update_d_update_fun$ > $o).
% 21.05/7.45  tff(comp_update$f, type, comp_update$f: (B_c_prod_update$ * B_c_prod_update$) > B_c_prod_update$).
% 21.05/7.45  tff(comp$ae, 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$).
% 21.05/7.45  tff(map_prod$f, 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$).
% 21.05/7.45  tff(uuy$, type, uuy$: A_update_a_update_fun$ > A_update_d_a_prod_update_fun$).
% 21.05/7.45  tff(rel_fun$k, type, rel_fun$k: (C_update_d_update_bool_fun_fun$ * A_update_a_update_bool_fun_fun$) > C_update_a_update_fun_d_update_a_update_fun_bool_fun_fun$).
% 21.05/7.45  tff(type_definition$g, type, type_definition$g: (B_update_a_update_fun$ * A_update_b_update_fun$ * A_update_set$) > $o).
% 21.05/7.45  tff(type_definition$i, type, type_definition$i: (B_update_c_update_fun$ * C_update_b_update_fun$ * C_update_set$) > $o).
% 21.05/7.45  tff(comp_update$l, type, comp_update$l: (C_a_prod_update$ * C_a_prod_update$) > C_a_prod_update$).
% 21.05/7.45  tff(register$k, type, register$k: C_d_prod_update_a_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(tensor_update$f, type, tensor_update$f: (B_update$ * B_update$) > B_b_prod_update$).
% 21.05/7.45  tff('#skF_96', type, '#skF_96': (A_itself$ * C_update_set$) > C_update_a_update_fun$).
% 21.05/7.45  tff(uvp$, type, uvp$: C_update_a_update_fun$ > C_update_a_b_prod_update_fun$).
% 21.05/7.45  tff(compatible$c, type, compatible$c: (A_update_b_update_fun$ * A_update_b_update_fun$) > $o).
% 21.05/7.45  tff(relcompp$b, type, relcompp$b: (B_update_a_update_bool_fun_fun$ * A_update_c_update_bool_fun_fun$) > B_update_c_update_bool_fun_fun$).
% 21.05/7.45  tff('#skF_7', type, '#skF_7': (A_update_b_update_fun$ * C_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(fun_app$g, type, fun_app$g: (B_update_a_b_prod_update_fun$ * B_update$) > A_b_prod_update$).
% 21.05/7.45  tff(fun_app$dl, type, fun_app$dl: (C_d_prod_update_d_update_prod_a_update_a_update_prod_fun$ * C_d_prod_update_d_update_prod$) > A_update_a_update_prod$).
% 21.05/7.45  tff(collect$c, type, collect$c: A_update_bool_fun$ > A_update_set$).
% 21.05/7.45  tff(comp$ac, 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$).
% 21.05/7.45  tff(fun_app$h, type, fun_app$h: (A_update_a_a_prod_update_fun$ * A_update$) > A_a_prod_update$).
% 21.05/7.45  tff(grp$c, type, grp$c: (D_update_a_update_fun_set$ * D_update_a_update_fun_d_update_b_update_fun_fun$) > D_update_a_update_fun_d_update_b_update_fun_bool_fun_fun$).
% 21.05/7.45  tff(compatible$u, type, compatible$u: (B_update_b_update_fun$ * B_update_b_update_fun$) > $o).
% 21.05/7.45  tff(preregister$c, type, preregister$c: A_update_b_update_fun$ > $o).
% 21.05/7.45  tff(map_fun$d, type, map_fun$d: (C_update_b_update_fun$ * C_d_prod_update_b_update_fun$) > B_update_c_d_prod_update_fun_c_update_b_update_fun_fun$).
% 21.05/7.45  tff(relcompp$, type, relcompp$: (B_update_a_update_bool_fun_fun$ * A_update_b_update_bool_fun_fun$) > B_update_b_update_bool_fun_fun$).
% 21.05/7.45  tff(map_fun$n, type, map_fun$n: (D_update_b_update_fun$ * D_update_b_update_fun$) > B_update_d_update_fun_d_update_b_update_fun_fun$).
% 21.05/7.45  tff(comp$av, type, comp$av: (A_update_a_update_fun_d_update_b_update_fun_fun$ * B_update_c_update_fun_a_update_a_update_fun_fun$) > B_update_c_update_fun_d_update_b_update_fun_fun$).
% 21.05/7.45  tff(compatible$as, type, compatible$as: (A_update_b_a_prod_update_fun$ * C_update_b_a_prod_update_fun$) > $o).
% 21.05/7.45  tff(comp$bu, 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$).
% 21.05/7.45  tff(register$aq, type, register$aq: A_update_d_d_prod_update_fun$ > $o).
% 21.05/7.45  tff('#skF_110', type, '#skF_110': (D_update_a_update_fun$ * D_update_set$ * A_update_b_update_fun$ * A_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff(tensor_update$n, type, tensor_update$n: (B_update$ * C_update$) > B_c_prod_update$).
% 21.05/7.45  tff(grp$, type, grp$: (A_update_set$ * A_update_b_update_fun$) > A_update_b_update_bool_fun_fun$).
% 21.05/7.45  tff(comp$bl, type, comp$bl: (A_update_b_update_b_update_prod_fun$ * D_update_a_update_fun$) > D_update_b_update_b_update_prod_fun$).
% 21.05/7.45  tff('#skF_115', type, '#skF_115': (D_update_a_update_fun$ * D_update_a_update_fun$ * A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(compatible$ag, type, compatible$ag: (C_update_a_a_prod_update_fun$ * C_update_a_a_prod_update_fun$) > $o).
% 21.05/7.45  tff(comp$bq, 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$).
% 21.05/7.45  tff(fun_app$c, type, fun_app$c: (D_update_a_d_prod_update_fun$ * D_update$) > A_d_prod_update$).
% 21.05/7.45  tff(rel_fun$m, 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).
% 21.05/7.45  tff(uu$, type, uu$: C_d_prod_update_set$ > C_d_prod_update_bool_fun$).
% 21.05/7.45  tff('#skF_114', type, '#skF_114': (C_d_prod_update_a_update_fun$ * C_d_prod_update_a_update_fun$ * A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(pred_fun$d, type, pred_fun$d: (D_update_bool_fun$ * B_update_bool_fun$ * D_update_b_update_fun$) > $o).
% 21.05/7.45  tff('#skF_62', type, '#skF_62': (C_d_prod_update_b_update_fun$ * C_d_prod_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff(fun_app$, type, fun_app$: (B_update_b_a_prod_update_fun$ * B_update$) > B_a_prod_update$).
% 21.05/7.45  tff(conversep$, type, conversep$: B_update_a_update_bool_fun_fun$ > A_update_b_update_bool_fun_fun$).
% 21.05/7.45  tff(uuc$, type, uuc$: A_update_set$ > A_update_bool_fun$).
% 21.05/7.45  tff(quotient$h, 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).
% 21.05/7.45  tff(convol$, type, convol$: (C_update_b_update_fun$ * C_update_b_update_fun$) > C_update_b_update_b_update_prod_fun$).
% 21.05/7.45  tff(uuv$, type, uuv$: B_update_a_update_fun$ > B_update_d_a_prod_update_fun$).
% 21.05/7.45  tff(map_fun$a, 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$).
% 21.05/7.45  tff(separating$, type, separating$: (A_itself$ * D_update_set$) > $o).
% 21.05/7.45  tff(map_fun$f, 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$).
% 21.05/7.45  tff(quotient$i, 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).
% 21.05/7.45  tff(map_fun$b, 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$).
% 21.05/7.45  tff(comp$j, type, comp$j: A_update_b_update_fun_d_update_a_update_fun_d_update_b_update_fun_fun_fun$).
% 21.05/7.45  tff(fun_app$bk, 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$).
% 21.05/7.45  tff(compatible$q, type, compatible$q: (D_update_b_update_fun$ * D_update_b_update_fun$) > $o).
% 21.05/7.45  tff(comp$ad, 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$).
% 21.05/7.45  tff(fun_app$bf, type, fun_app$bf: (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$).
% 21.05/7.45  tff(compatible$s, type, compatible$s: (B_update_b_update_fun$ * D_update_b_update_fun$) > $o).
% 21.05/7.45  tff('#skF_67', type, '#skF_67': (C_update_b_update_fun$ * A_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff('#skF_35', type, '#skF_35': (D_update_b_update_fun$ * A_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff(uuj$, type, uuj$: B_update_b_update_fun$ > B_update_b_d_prod_update_fun$).
% 21.05/7.45  tff('#skF_36', type, '#skF_36': (D_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(comp$bo, 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$).
% 21.05/7.45  tff(fun_app$ca, type, fun_app$ca: (B_a_prod_update_b_update_fun$ * B_a_prod_update$) > B_update$).
% 21.05/7.45  tff(compatible$t, type, compatible$t: (B_update_b_update_fun$ * C_update_b_update_fun$) > $o).
% 21.05/7.45  tff(fun_app$ax, type, fun_app$ax: (B_update_d_b_prod_update_fun$ * B_update$) > D_b_prod_update$).
% 21.05/7.45  tff(pred_fun$c, type, pred_fun$c: (C_d_prod_update_bool_fun$ * A_update_bool_fun$) > C_d_prod_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(uum$, type, uum$: C_update_b_update_fun$ > C_update_b_b_prod_update_fun$).
% 21.05/7.45  tff(fun_app$i, type, fun_app$i: (C_d_prod_update_a_update_fun_bool_fun$ * C_d_prod_update_a_update_fun$) > $o).
% 21.05/7.45  tff(fun_app$ap, type, fun_app$ap: (A_update_a_update_bool_fun_fun$ * A_update$) > A_update_bool_fun$).
% 21.05/7.45  tff(compatible$z, type, compatible$z: (C_update_a_update_fun$ * B_update_a_update_fun$) > $o).
% 21.05/7.45  tff(rel_fun$ac, 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).
% 21.05/7.45  tff(uue$, type, uue$: C_d_prod_update_a_update_fun_set$ > C_d_prod_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff('#skF_72', type, '#skF_72': (A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(fun_app$bv, type, fun_app$bv: (D_update_a_update_fun_d_update_b_update_fun_fun$ * D_update_a_update_fun$) > D_update_b_update_fun$).
% 21.05/7.45  tff(fun_app$cn, type, fun_app$cn: (B_update_d_update_fun_d_update_b_update_fun_fun$ * B_update_d_update_fun$) > D_update_b_update_fun$).
% 21.05/7.45  tff(comp$aj, 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$).
% 21.05/7.45  tff('#skF_38', type, '#skF_38': (D_update_b_update_fun$ * D_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff(fun_app$dn, 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$).
% 21.05/7.45  tff(pred_fun$a, type, pred_fun$a: (C_update_bool_fun$ * A_update_bool_fun$) > C_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(register$j, type, register$j: C_a_prod_update_a_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(rel_fun$t, 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$).
% 21.05/7.45  tff(pred_fun$, type, pred_fun$: (C_update_bool_fun$ * B_update_bool_fun$ * C_update_b_update_fun$) > $o).
% 21.05/7.45  tff(relcompp$f, type, relcompp$f: (A_update_a_update_bool_fun_fun$ * A_update_c_update_bool_fun_fun$) > A_update_c_update_bool_fun_fun$).
% 21.05/7.45  tff(fun_app$ce, type, fun_app$ce: (C_d_prod_update_c_d_prod_update_fun$ * C_d_prod_update$) > C_d_prod_update$).
% 21.05/7.45  tff(register$ar, type, register$ar: A_update_c_d_prod_update_fun$ > $o).
% 21.05/7.45  tff(register_tensor$i, type, register_tensor$i: (A_update_b_update_fun$ * C_update_b_update_fun$) > A_c_prod_update_b_b_prod_update_fun$).
% 21.05/7.45  tff(register$z, type, register$z: A_d_prod_update_b_update_fun$ > $o).
% 21.05/7.45  tff('#skF_87', type, '#skF_87': (C_update_a_update_fun_bool_fun$ * C_update_a_update_fun_bool_fun$) > C_update_a_update_fun$).
% 21.05/7.45  tff(register$bg, type, register$bg: C_update_a_c_prod_update_fun$ > $o).
% 21.05/7.45  tff('#skF_66', type, '#skF_66': (C_update_b_update_fun$ * C_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff(compatible$ae, type, compatible$ae: (C_update_c_update_fun$ * D_update_c_update_fun$) > $o).
% 21.05/7.45  tff(uvc$, type, uvc$: A_update_a_c_prod_update_fun$).
% 21.05/7.45  tff(conversep$a, type, conversep$a: C_update_a_update_bool_fun_fun$ > A_update_c_update_bool_fun_fun$).
% 21.05/7.45  tff(comp$bk, 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$).
% 21.05/7.45  tff(quotient$, 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).
% 21.05/7.45  tff(register$bf, type, register$bf: D_update_a_d_prod_update_fun$ > $o).
% 21.05/7.45  tff(register_pair$h, type, register_pair$h: (C_update_b_update_fun$ * A_update_b_update_fun$) > C_a_prod_update_b_update_fun$).
% 21.05/7.45  tff('#skF_8', type, '#skF_8': (A_update_b_update_fun$ * C_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff(fun_app$bl, type, fun_app$bl: (C_c_prod_update_a_a_prod_update_fun$ * C_c_prod_update$) > A_a_prod_update$).
% 21.05/7.45  tff(map_prod$j, 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$).
% 21.05/7.45  tff(fun_app$f, type, fun_app$f: (A_update_a_b_prod_update_fun$ * A_update$) > A_b_prod_update$).
% 21.05/7.45  tff(register_pair$e, type, register_pair$e: (A_update_b_update_fun$ * B_update_b_update_fun$) > A_b_prod_update_b_update_fun$).
% 21.05/7.45  tff(comp$bh, type, comp$bh: (C_update_a_update_a_update_prod_fun$ * C_update_c_update_fun$) > C_update_a_update_a_update_prod_fun$).
% 21.05/7.45  tff(fcomp$a, 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$).
% 21.05/7.45  tff(tensor_update$m, type, tensor_update$m: (C_update$ * A_update$) > C_a_prod_update$).
% 21.05/7.45  tff(compatible$ak, type, compatible$ak: (C_update_a_b_prod_update_fun$ * C_update_a_b_prod_update_fun$) > $o).
% 21.05/7.45  tff('#skF_64', type, '#skF_64': (C_update_a_update_fun$ * C_update_a_update_fun$) > C_update$).
% 21.05/7.45  tff(uvw$, type, uvw$: (A_update_b_update_fun$ * A_update_b_update_fun$) > A_update_bool_fun$).
% 21.05/7.45  tff(register$ak, type, register$ak: D_d_prod_update_b_update_fun$ > $o).
% 21.05/7.45  tff('#skF_53', type, '#skF_53': (D_update_b_update_fun$ * C_update_b_update_fun$ * D_update$ * C_update$) > D_update$).
% 21.05/7.45  tff(comp$bb, type, comp$bb: (C_update_b_update_fun$ * C_d_prod_update_c_update_fun$) > C_d_prod_update_b_update_fun$).
% 21.05/7.45  tff('#skF_44', type, '#skF_44': (C_update_b_update_fun$ * C_update_b_update_fun$ * C_update$ * C_update$) > C_update$).
% 21.05/7.45  tff(register$q, type, register$q: A_c_prod_update_b_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(rel_fun$x, type, rel_fun$x: (C_d_prod_update_d_update_bool_fun_fun$ * B_update_b_update_bool_fun_fun$) > C_d_prod_update_b_update_fun_d_update_b_update_fun_bool_fun_fun$).
% 21.05/7.45  tff(fun_app$cv, 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$).
% 21.05/7.45  tff('#skF_16', type, '#skF_16': (D_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(fun_app$dj, 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$).
% 21.05/7.45  tff(compatible$af, type, compatible$af: (C_update_d_update_fun$ * D_update_d_update_fun$) > $o).
% 21.05/7.45  tff(register_tensor$p, type, register_tensor$p: (A_update_b_update_fun$ * A_update_b_update_fun$) > A_a_prod_update_b_b_prod_update_fun$).
% 21.05/7.45  tff(register_pair$o, type, register_pair$o: (B_update_d_update_fun$ * A_update_d_update_fun$ * B_a_prod_update$) > D_update$).
% 21.05/7.45  tff(fun_app$de, 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$).
% 21.05/7.45  tff(comp$ag, 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$).
% 21.05/7.45  tff(fun_app$aa, type, fun_app$aa: (A_update_d_update_fun$ * A_update$) > D_update$).
% 21.05/7.45  tff(rel_fun$h, 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$).
% 21.05/7.45  tff(uuf$, type, uuf$: C_update_a_update_fun_set$ > C_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(uwa$, type, uwa$: A_update_set$ > C_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff('#skF_84', type, '#skF_84': (D_update_a_update_fun_bool_fun$ * D_update_a_update_fun_bool_fun$) > D_update_a_update_fun$).
% 21.05/7.45  tff(f$, type, f$: A_update_b_update_fun$).
% 21.05/7.45  tff(compatible$p, type, compatible$p: (D_update_b_update_fun$ * A_update_b_update_fun$) > $o).
% 21.05/7.45  tff(comp$bp, type, comp$bp: (A_update_a_update_fun_d_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_d_update_b_update_fun_fun$).
% 21.05/7.45  tff('#skF_89', type, '#skF_89': (A_itself$ * D_update_set$) > D_update_a_update_fun$).
% 21.05/7.45  tff(fcomp$g, type, fcomp$g: (D_update_a_update_fun$ * A_update_b_update_fun$) > D_update_b_update_fun$).
% 21.05/7.45  tff(comp$bs, 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$).
% 21.05/7.45  tff(member$d, type, member$d: (C_d_prod_update_a_update_fun$ * C_d_prod_update_a_update_fun_set$) > $o).
% 21.05/7.45  tff(register_tensor$f, type, register_tensor$f: (C_update_b_update_fun$ * A_update_b_update_fun$) > C_a_prod_update_b_b_prod_update_fun$).
% 21.05/7.45  tff('#skF_117', type, '#skF_117': (C_update_a_update_fun$ * A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(register_pair$k, type, register_pair$k: (A_update_a_update_fun$ * D_update_a_update_fun$) > A_d_prod_update_a_update_fun$).
% 21.05/7.45  tff(register$af, type, register$af: C_c_prod_update_a_update_fun$ > $o).
% 21.05/7.45  tff('#skF_1', type, '#skF_1': (C_update_a_update_fun$ * C_update_a_update_fun$) > C_update$).
% 21.05/7.45  tff(register$av, type, register$av: B_update_b_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(uuo$, type, uuo$: D_update_b_update_fun$ > D_update_b_b_prod_update_fun$).
% 21.05/7.45  tff(comp$ai, 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$).
% 21.05/7.45  tff('#skF_65', type, '#skF_65': (C_update_b_update_fun$ * C_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff(fun_app$y, type, fun_app$y: (B_update_b_b_prod_update_fun$ * B_update$) > B_b_prod_update$).
% 21.05/7.45  tff(register$o, type, register$o: C_d_prod_update_b_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(compatible$am, type, compatible$am: (C_update_b_b_prod_update_fun$ * A_update_b_b_prod_update_fun$) > $o).
% 21.05/7.45  tff(fun_app$ck, type, fun_app$ck: (D_c_prod_update_b_update_fun$ * D_c_prod_update$) > B_update$).
% 21.05/7.45  tff(rel_fun$aj, type, rel_fun$aj: (D_update_d_update_bool_fun_fun$ * B_update_b_update_bool_fun_fun$) > D_update_b_update_fun_d_update_b_update_fun_bool_fun_fun$).
% 21.05/7.45  tff(relcompp$i, 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$).
% 21.05/7.45  tff(map_prod$l, 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$).
% 21.05/7.45  tff(fcomp$, 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$).
% 21.05/7.45  tff(rel_fun$n, 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$).
% 21.05/7.45  tff(register_tensor$n, type, register_tensor$n: (D_update_a_update_fun$ * D_update_b_update_fun$) > D_d_prod_update_a_b_prod_update_fun$).
% 21.05/7.45  tff('#skF_3', type, '#skF_3': (C_update_b_update_fun$ * C_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff('#skF_98', type, '#skF_98': (B_itself$ * B_update_set$) > B_update_b_update_fun$).
% 21.05/7.45  tff(comp$x, type, comp$x: (D_update_a_update_fun$ * D_update_d_update_fun$) > D_update_a_update_fun$).
% 21.05/7.45  tff('#skF_75', type, '#skF_75': (D_update_b_update_fun$ * C_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff(register_tensor$ac, 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$).
% 21.05/7.45  tff(image$e, type, image$e: (D_update_b_update_fun$ * D_update_set$) > B_update_set$).
% 21.05/7.45  tff(fun_app$ay, type, fun_app$ay: (B_update_d_a_prod_update_fun$ * B_update$) > D_a_prod_update$).
% 21.05/7.45  tff('#skF_99', type, '#skF_99': (B_itself$ * B_update_set$) > B_update_b_update_fun$).
% 21.05/7.45  tff(comp$g, type, comp$g: (B_update_b_update_fun$ * A_update_b_update_fun$) > A_update_b_update_fun$).
% 21.05/7.45  tff(comp_update$k, type, comp_update$k: (C_b_prod_update$ * C_b_prod_update$) > C_b_prod_update$).
% 21.05/7.45  tff(comp$y, type, comp$y: (D_update_a_update_fun$ * C_update_d_update_fun$) > C_update_a_update_fun$).
% 21.05/7.45  tff(map_prod$o, 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$).
% 21.05/7.45  tff('#skF_48', type, '#skF_48': (A_update_b_update_fun$ * C_update_b_update_fun$ * A_update$ * C_update$) > C_update$).
% 21.05/7.45  tff(compatible$e, type, compatible$e: (A_update_a_update_fun$ * B_update_a_update_fun$) > $o).
% 21.05/7.45  tff(register_pair$m, type, register_pair$m: (A_update_a_update_fun$ * B_update_a_update_fun$) > A_b_prod_update_a_update_fun$).
% 21.05/7.45  tff(map_fun$j, 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$).
% 21.05/7.45  tff('#skF_6', type, '#skF_6': (C_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(comp$ay, 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$).
% 21.05/7.45  tff(uvh$, type, uvh$: D_update_a_update_fun$ > D_update_b_a_prod_update_fun$).
% 21.05/7.45  tff(register$aa, type, register$aa: A_c_prod_update_b_update_fun$ > $o).
% 21.05/7.45  tff(comp_update$h, type, comp_update$h: (D_a_prod_update$ * D_a_prod_update$) > D_a_prod_update$).
% 21.05/7.45  tff(map_prod$r, type, map_prod$r: (D_update_a_update_fun$ * D_update_a_update_fun$) > D_update_d_update_prod_a_update_a_update_prod_fun$).
% 21.05/7.45  tff(tensor_update$g, type, tensor_update$g: (D_update$ * D_update$) > D_d_prod_update$).
% 21.05/7.45  tff(register$d, type, register$d: B_update_b_update_fun$ > $o).
% 21.05/7.45  tff(compatible$ao, type, compatible$ao: (A_update_a_b_prod_update_fun$ * C_update_a_b_prod_update_fun$) > $o).
% 21.05/7.45  tff(rel_fun$p, 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$).
% 21.05/7.45  tff(comp$cf, type, comp$cf: (A_update_d_update_fun$ * B_update_a_update_fun$) > B_update_d_update_fun$).
% 21.05/7.45  tff(comp$h, type, comp$h: (D_update_b_update_fun$ * A_update_d_update_fun$) > A_update_b_update_fun$).
% 21.05/7.45  tff(fun_app$ae, type, fun_app$ae: (A_update_b_update_fun$ * A_update$) > B_update$).
% 21.05/7.45  tff('#skF_88', type, '#skF_88': (C_update_a_update_fun_bool_fun$ * C_update_a_update_fun_bool_fun$) > C_update_a_update_fun$).
% 21.05/7.45  tff(compatible$g, type, compatible$g: D_update_a_update_fun$ > C_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(relcompp$m, type, relcompp$m: (D_update_a_update_bool_fun_fun$ * A_update_b_update_bool_fun_fun$) > D_update_b_update_bool_fun_fun$).
% 21.05/7.45  tff('#skF_74', type, '#skF_74': (A_update_b_update_fun$ * D_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff(fun_app$an, type, fun_app$an: (B_update_bool_fun$ * B_update$) > $o).
% 21.05/7.45  tff(comp$bz, type, comp$bz: (A_update_a_update_prod_b_update_b_update_prod_fun$ * C_d_prod_update_d_update_prod_a_update_a_update_prod_fun$) > C_d_prod_update_d_update_prod_b_update_b_update_prod_fun$).
% 21.05/7.45  tff(top$b, type, top$b: C_update_set$).
% 21.05/7.45  tff(map_prod$g, 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$).
% 21.05/7.45  tff(comp$c, type, comp$c: (B_update_a_update_fun$ * C_update_b_update_fun$) > C_update_a_update_fun$).
% 21.05/7.45  tff(fun_app$w, type, fun_app$w: (B_update_b_d_prod_update_fun$ * B_update$) > B_d_prod_update$).
% 21.05/7.45  tff('#skF_107', type, '#skF_107': (C_d_prod_update_set$ * C_d_prod_update_b_update_fun$ * C_d_prod_update_b_update_fun$) > C_d_prod_update$).
% 21.05/7.45  tff(map_prod$k, type, map_prod$k: (C_d_prod_update_b_update_fun$ * D_update_b_update_fun$) > C_d_prod_update_d_update_prod_b_update_b_update_prod_fun$).
% 21.05/7.45  tff(register$aw, type, register$aw: C_update_d_a_prod_update_fun$ > $o).
% 21.05/7.45  tff(uuz$, type, uuz$: C_update_b_update_fun$ > C_update_b_b_prod_update_fun$).
% 21.05/7.45  tff(comp$v, type, comp$v: (B_update_b_update_fun$ * C_d_prod_update_b_update_fun$) > C_d_prod_update_b_update_fun$).
% 21.05/7.45  tff('#skF_57', type, '#skF_57': (D_update_b_update_fun$ * D_update_b_update_fun$ * D_update$ * D_update$) > D_update$).
% 21.05/7.45  tff(tensor_update$k, type, tensor_update$k: (D_update$ * C_update$) > D_c_prod_update$).
% 21.05/7.45  tff('#skF_4', type, '#skF_4': (C_update_b_update_fun$ * C_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff('#skF_112', type, '#skF_112': (C_update_a_update_fun$ * C_update_a_update_fun$ * A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(rel_fun$s, type, rel_fun$s: (C_d_prod_update_c_d_prod_update_bool_fun_fun$ * A_update_a_update_bool_fun_fun$) > C_d_prod_update_a_update_fun_c_d_prod_update_a_update_fun_bool_fun_fun$).
% 21.05/7.45  tff(convol$d, 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$).
% 21.05/7.45  tff(uvd$, type, uvd$: A_update_a_b_prod_update_fun$).
% 21.05/7.45  tff(uvb$, type, uvb$: A_update_a_d_prod_update_fun$).
% 21.05/7.45  tff(comp_update$a, type, comp_update$a: B_update$ > B_update_b_update_fun$).
% 21.05/7.45  tff(fun_app$cw, type, fun_app$cw: (B_update_c_update_fun_c_update_b_update_fun_fun$ * B_update_c_update_fun$) > C_update_b_update_fun$).
% 21.05/7.45  tff(comp$br, 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$).
% 21.05/7.45  tff(fun_app$br, type, fun_app$br: (C_a_prod_update_b_b_prod_update_fun$ * C_a_prod_update$) > B_b_prod_update$).
% 21.05/7.45  tff(tensor_update$h, type, tensor_update$h: (C_update$ * D_update$) > C_d_prod_update$).
% 21.05/7.45  tff(fun_app$cq, 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$).
% 21.05/7.45  tff(comp$cc, type, comp$cc: (A_update_a_update_prod_b_update_b_update_prod_fun$ * D_update_d_update_prod_a_update_a_update_prod_fun$) > D_update_d_update_prod_b_update_b_update_prod_fun$).
% 21.05/7.45  tff(fun_app$dc, 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$).
% 21.05/7.45  tff(compatible$ad, type, compatible$ad: D_update_a_update_fun$ > D_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(fun_app$aw, type, fun_app$aw: (C_update_d_a_prod_update_fun$ * C_update$) > D_a_prod_update$).
% 21.05/7.45  tff(fun_app$do, 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$).
% 21.05/7.45  tff(fun_app$cr, 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$).
% 21.05/7.45  tff(relcompp$d, type, relcompp$d: (B_update_a_update_bool_fun_fun$ * A_update_d_update_bool_fun_fun$) > B_update_d_update_bool_fun_fun$).
% 21.05/7.45  tff(comp$ap, type, comp$ap: (B_update_a_update_fun$ * D_update_b_update_fun$) > D_update_a_update_fun$).
% 21.05/7.45  tff(image$b, type, image$b: (C_update_a_update_fun$ * C_update_set$) > A_update_set$).
% 21.05/7.45  tff(map_fun$l, type, map_fun$l: (D_update_b_update_fun$ * C_update_b_update_fun$) > B_update_c_update_fun_d_update_b_update_fun_fun$).
% 21.05/7.45  tff(fun_app$bz, type, fun_app$bz: (C_d_prod_update_b_update_fun$ * C_d_prod_update$) > B_update$).
% 21.05/7.45  tff(separating$b, type, separating$b: (A_itself$ * C_update_set$) > $o).
% 21.05/7.45  tff(rel_fun$v, type, rel_fun$v: (C_d_prod_update_a_update_fun_d_update_a_update_fun_bool_fun_fun$ * C_d_prod_update_b_update_fun_d_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$).
% 21.05/7.45  tff(comp_update$m, type, comp_update$m: C_d_prod_update$ > C_d_prod_update_c_d_prod_update_fun$).
% 21.05/7.45  tff(fun_app$p, type, fun_app$p: (C_update_b_d_prod_update_fun$ * C_update$) > B_d_prod_update$).
% 21.05/7.45  tff(id_update$a, type, id_update$a: D_update$).
% 21.05/7.45  tff(rel_fun$a, 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$).
% 21.05/7.45  tff(comp_update$c, type, comp_update$c: C_update$ > C_update_c_update_fun$).
% 21.05/7.45  tff('#skF_21', type, '#skF_21': (C_update_a_update_fun$ * C_update_a_update_fun$) > C_update$).
% 21.05/7.45  tff(compatible$al, type, compatible$al: (C_update_b_b_prod_update_fun$ * C_update_b_b_prod_update_fun$) > $o).
% 21.05/7.45  tff(type$, type, type$: B_itself$).
% 21.05/7.45  tff(fun_app$dx, 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$).
% 21.05/7.45  tff(fun_app$dm, 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$).
% 21.05/7.45  tff(preregister$j, type, preregister$j: C_d_prod_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(fun_app$cd, type, fun_app$cd: (A_d_prod_update_b_update_fun$ * A_d_prod_update$) > B_update$).
% 21.05/7.45  tff(uvr$, type, uvr$: D_update_b_update_fun$ > D_update_a_b_prod_update_fun$).
% 21.05/7.45  tff(register$g, type, register$g: D_update_b_update_fun$ > $o).
% 21.05/7.45  tff(fun_app$as, type, fun_app$as: (D_update_d_b_prod_update_fun$ * D_update$) > D_b_prod_update$).
% 21.05/7.45  tff(uul$, type, uul$: A_update_c_update_fun$ > A_update_c_d_prod_update_fun$).
% 21.05/7.45  tff(compatible$b, type, compatible$b: (A_update_b_update_fun$ * B_update_b_update_fun$) > $o).
% 21.05/7.45  tff(comp$m, type, comp$m: (A_b_prod_update_b_update_fun$ * D_c_prod_update_a_b_prod_update_fun$) > D_c_prod_update_b_update_fun$).
% 21.05/7.45  tff(register_pair$i, type, register_pair$i: (B_update_b_update_fun$ * A_update_b_update_fun$) > B_a_prod_update_b_update_fun$).
% 21.05/7.45  tff(comp$cg, type, comp$cg: (D_update_b_update_fun$ * B_update_d_update_fun$) > B_update_b_update_fun$).
% 21.05/7.45  tff(compatible$ac, type, compatible$ac: (C_update_a_update_fun$ * A_update_a_update_fun$) > $o).
% 21.05/7.45  tff(comp_update$g, type, comp_update$g: (D_b_prod_update$ * D_b_prod_update$) > D_b_prod_update$).
% 21.05/7.45  tff(rel_fun$o, 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$).
% 21.05/7.45  tff(preregister$n, type, preregister$n: C_update_d_update_fun$ > $o).
% 21.05/7.45  tff(map_prod$c, 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$).
% 21.05/7.45  tff(register$be, type, register$be: A_update_b_a_prod_update_fun$ > $o).
% 21.05/7.45  tff(register$ax, type, register$ax: C_update_d_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(register$ap, type, register$ap: B_update_b_d_prod_update_fun$ > $o).
% 21.05/7.45  tff(register_pair$a, type, register_pair$a: (C_update_b_update_fun$ * D_update_b_update_fun$) > C_d_prod_update_b_update_fun$).
% 21.05/7.45  tff(comp_update$d, type, comp_update$d: (B_b_prod_update$ * B_b_prod_update$) > B_b_prod_update$).
% 21.05/7.45  tff(comp$f, type, comp$f: (C_update_b_update_fun$ * C_update_c_update_fun$) > C_update_b_update_fun$).
% 21.05/7.45  tff(preregister$b, type, preregister$b: C_update_b_update_fun$ > $o).
% 21.05/7.45  tff(relcompp$a, type, relcompp$a: (A_update_a_update_bool_fun_fun$ * A_update_b_update_bool_fun_fun$) > A_update_b_update_bool_fun_fun$).
% 21.05/7.45  tff(register$h, type, register$h: C_c_prod_update_a_a_prod_update_fun$ > $o).
% 21.05/7.45  tff(comp$bd, type, comp$bd: (A_update_a_update_fun$ * C_d_prod_update_a_update_fun$) > C_d_prod_update_a_update_fun$).
% 21.05/7.45  tff(uvm$, type, uvm$: C_update_b_update_fun$ > C_update_b_a_prod_update_fun$).
% 21.05/7.45  tff(comp$o, 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$).
% 21.05/7.45  tff(comp$, type, comp$: A_update_b_update_fun_c_update_a_update_fun_c_update_b_update_fun_fun_fun$).
% 21.05/7.45  tff(comp$ca, 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$).
% 21.05/7.45  tff('#skF_17', type, '#skF_17': (D_update_b_update_fun$ * D_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff(register_tensor$m, type, register_tensor$m: (D_update_a_update_fun$ * A_update_b_update_fun$) > D_a_prod_update_a_b_prod_update_fun$).
% 21.05/7.45  tff(image$d, type, image$d: (C_d_prod_update_b_update_fun$ * C_d_prod_update_set$) > B_update_set$).
% 21.05/7.45  tff(tensor_update$o, type, tensor_update$o: (C_update$ * B_update$) > C_b_prod_update$).
% 21.05/7.45  tff(compatible$ab, type, compatible$ab: (A_update_a_update_fun$ * A_update_a_update_fun$) > $o).
% 21.05/7.45  tff(register_pair$j, type, register_pair$j: (A_update_b_update_fun$ * D_update_b_update_fun$) > A_d_prod_update_b_update_fun$).
% 21.05/7.45  tff(register$s, type, register$s: D_update_c_update_fun$ > $o).
% 21.05/7.45  tff(comp$k, type, comp$k: (A_a_prod_update_b_update_fun$ * D_d_prod_update_a_a_prod_update_fun$) > D_d_prod_update_b_update_fun$).
% 21.05/7.45  tff(relcompp$l, type, relcompp$l: (A_update_a_update_bool_fun_fun$ * A_update_d_update_bool_fun_fun$) > A_update_d_update_bool_fun_fun$).
% 21.05/7.45  tff(uvf$, type, uvf$: D_update_b_update_fun$ > D_update_b_b_prod_update_fun$).
% 21.05/7.45  tff(map_fun$i, type, map_fun$i: (C_d_prod_update_b_update_fun$ * C_d_prod_update_b_update_fun$) > B_update_c_d_prod_update_fun_c_d_prod_update_b_update_fun_fun$).
% 21.05/7.45  tff('#skF_119', type, '#skF_119': (D_update_a_update_fun$ * A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(rel_fun$f, type, rel_fun$f: (C_update_a_update_fun_c_d_prod_update_a_update_fun_bool_fun_fun$ * C_update_b_update_fun_c_d_prod_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$).
% 21.05/7.45  tff(register_pair$d, type, register_pair$d: (D_update_b_update_fun$ * C_update_b_update_fun$) > D_c_prod_update_b_update_fun$).
% 21.05/7.45  tff(image$, type, image$: (C_d_prod_update_a_update_fun$ * C_d_prod_update_set$) > A_update_set$).
% 21.05/7.45  tff(fun_app$cp, type, fun_app$cp: (B_update_d_update_fun_a_update_a_update_fun_fun$ * B_update_d_update_fun$) > A_update_a_update_fun$).
% 21.05/7.45  tff('#skF_109', type, '#skF_109': (C_d_prod_update_a_update_fun$ * C_d_prod_update_set$ * A_update_b_update_fun$ * A_update_b_update_fun$) > C_d_prod_update$).
% 21.05/7.45  tff(compatible$an, type, compatible$an: (C_update_b_b_prod_update_fun$ * D_update_b_b_prod_update_fun$) > $o).
% 21.05/7.45  tff(map_prod$m, 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$).
% 21.05/7.45  tff(rel_fun$j, 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$).
% 21.05/7.45  tff(register_tensor$h, type, register_tensor$h: (A_update_b_update_fun$ * C_update_a_update_fun$) > A_c_prod_update_b_a_prod_update_fun$).
% 21.05/7.45  tff(h$, type, h$: D_update_a_update_fun$).
% 21.05/7.45  tff(fun_app$bb, type, fun_app$bb: (A_update_d_b_prod_update_fun$ * A_update$) > D_b_prod_update$).
% 21.05/7.45  tff(rel_fun$am, type, rel_fun$am: (D_update_d_update_bool_fun_fun$ * A_update_b_update_bool_fun_fun$) > D_update_a_update_fun_d_update_b_update_fun_bool_fun_fun$).
% 21.05/7.45  tff(register$ah, type, register$ah: C_a_prod_update_b_update_fun$ > $o).
% 21.05/7.45  tff(comp$bm, 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$).
% 21.05/7.45  tff(register$n, type, register$n: C_a_prod_update_b_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(compatible$v, type, compatible$v: (B_update_d_update_fun$ * A_update_d_update_fun$) > $o).
% 21.05/7.45  tff('#skF_37', type, '#skF_37': (D_update_b_update_fun$ * D_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff(register$v, type, register$v: A_update_d_update_fun$ > $o).
% 21.05/7.45  tff(fun_app$cz, type, fun_app$cz: (C_update_c_d_prod_update_fun$ * C_update$) > C_d_prod_update$).
% 21.05/7.45  tff(fun_app$cy, type, fun_app$cy: (C_d_prod_update_c_update_fun$ * C_d_prod_update$) > C_update$).
% 21.05/7.45  tff(comp$at, type, comp$at: (A_update_a_update_fun$ * D_update_a_update_fun$) > D_update_a_update_fun$).
% 21.05/7.45  tff(member$e, type, member$e: (D_update_a_update_fun$ * D_update_a_update_fun_set$) > $o).
% 21.05/7.45  tff('#skF_101', type, '#skF_101': (B_itself$ * A_update_set$) > A_update_b_update_fun$).
% 21.05/7.45  tff(fun_app$z, type, fun_app$z: (A_update_d_d_prod_update_fun$ * A_update$) > D_d_prod_update$).
% 21.05/7.45  tff(fun_app$au, type, fun_app$au: (D_update_a_update_fun$ * D_update$) > A_update$).
% 21.05/7.45  tff('#skF_50', type, '#skF_50': (A_update_b_update_fun$ * A_update_b_update_fun$ * A_update$ * A_update$) > A_update$).
% 21.05/7.45  tff(register_pair$t, type, register_pair$t: (A_update_b_b_prod_update_fun$ * D_update_b_b_prod_update_fun$) > A_d_prod_update_b_b_prod_update_fun$).
% 21.05/7.45  tff(member$, type, member$: (C_d_prod_update$ * C_d_prod_update_set$) > $o).
% 21.05/7.45  tff('#skF_2', type, '#skF_2': (C_update_a_update_fun$ * C_update_a_update_fun$) > C_update$).
% 21.05/7.45  tff(register$ad, type, register$ad: A_b_prod_update_a_update_fun$ > $o).
% 21.05/7.45  tff(uux$, type, uux$: A_update_c_update_fun$ > A_update_d_c_prod_update_fun$).
% 21.05/7.45  tff(register$y, type, register$y: A_d_prod_update_a_update_fun$ > $o).
% 21.05/7.45  tff(conversep$c, type, conversep$c: D_update_a_update_bool_fun_fun$ > A_update_d_update_bool_fun_fun$).
% 21.05/7.45  tff(map_prod$a, 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$).
% 21.05/7.45  tff(fun_app$dd, type, fun_app$dd: (C_update_c_d_prod_update_prod_a_update_a_update_prod_fun$ * C_update_c_d_prod_update_prod$) > A_update_a_update_prod$).
% 21.05/7.45  tff('#skF_33', type, '#skF_33': (D_update_b_update_fun$ * C_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff(map_fun$h, 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$).
% 21.05/7.45  tff(register$w, type, register$w: A_update_c_update_fun$ > $o).
% 21.05/7.45  tff(convol$e, type, convol$e: (D_update_b_update_fun$ * D_update_b_update_fun$) > D_update_b_update_b_update_prod_fun$).
% 21.05/7.45  tff(tensor_update$l, type, tensor_update$l: (C_update$ * C_update$) > C_c_prod_update$).
% 21.05/7.45  tff('#skF_73', type, '#skF_73': (A_update_b_update_fun$ * D_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(uuw$, type, uuw$: A_update_d_update_fun$ > A_update_d_d_prod_update_fun$).
% 21.05/7.45  tff(register_pair$l, type, register_pair$l: (A_update_b_update_fun$ * C_update_b_update_fun$) > A_c_prod_update_b_update_fun$).
% 21.05/7.45  tff('#skF_120', type, '#skF_120': (C_update_a_update_fun$ * C_update_a_update_fun$ * A_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff('#skF_20', type, '#skF_20': (C_update_a_update_fun$ * D_update_a_update_fun$) > D_update$).
% 21.05/7.45  tff(fun_app$bn, type, fun_app$bn: (C_a_prod_update_a_b_prod_update_fun$ * C_a_prod_update$) > A_b_prod_update$).
% 21.05/7.45  tff(uuk$, type, uuk$: A_update_d_update_fun$ > A_update_d_d_prod_update_fun$).
% 21.05/7.45  tff(fun_app$l, type, fun_app$l: (D_update_b_d_prod_update_fun$ * D_update$) > B_d_prod_update$).
% 21.05/7.45  tff(register$bk, type, register$bk: A_update_a_d_prod_update_fun$ > $o).
% 21.05/7.45  tff(register_pair$s, type, register_pair$s: (C_update_a_update_fun$ * C_update_a_update_fun$) > C_c_prod_update_a_update_fun$).
% 21.05/7.45  tff(fun_app$be, 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$).
% 21.05/7.45  tff('#skF_81', type, '#skF_81': (C_update_a_update_fun$ * D_update_a_update_fun$) > C_update$).
% 21.05/7.45  tff(map_prod$e, 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$).
% 21.05/7.45  tff(register$at, type, register$at: A_update_b_b_prod_update_fun$ > $o).
% 21.05/7.45  tff('#skF_15', type, '#skF_15': (D_update_b_update_fun$ * A_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff('#skF_82', type, '#skF_82': (C_update_a_update_fun$ * D_update_a_update_fun$) > D_update$).
% 21.05/7.45  tff(fun_app$u, type, fun_app$u: (C_update_a_update_fun$ * C_update$) > A_update$).
% 21.05/7.45  tff(fun_app$bs, type, fun_app$bs: (C_d_prod_update_b_b_prod_update_fun$ * C_d_prod_update$) > B_b_prod_update$).
% 21.05/7.45  tff(comp$ba, type, comp$ba: (C_d_prod_update_b_update_fun$ * C_update_c_d_prod_update_fun$) > C_update_b_update_fun$).
% 21.05/7.45  tff(type_definition$a, type, type_definition$a: (B_update_b_update_fun$ * B_update_b_update_fun$ * B_update_set$) > $o).
% 21.05/7.45  tff(g$, type, g$: C_update_a_update_fun$).
% 21.05/7.45  tff('#skF_49', type, '#skF_49': (A_update_b_update_fun$ * A_update_b_update_fun$ * A_update$ * A_update$) > A_update$).
% 21.05/7.45  tff('#skF_76', type, '#skF_76': (D_update_b_update_fun$ * C_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff(uvv$, type, uvv$: D_update_bool_fun$).
% 21.05/7.45  tff(fun_app$dh, 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$).
% 21.05/7.45  tff(uui$, type, uui$: D_update_b_update_fun$ > D_update_b_d_prod_update_fun$).
% 21.05/7.45  tff(comp$cd, type, comp$cd: (A_update_c_update_fun$ * B_update_a_update_fun$) > B_update_c_update_fun$).
% 21.05/7.45  tff(fun_app$ci, type, fun_app$ci: (A_c_prod_update_b_update_fun$ * A_c_prod_update$) > B_update$).
% 21.05/7.45  tff(image$f, type, image$f: (A_update_b_update_fun$ * A_update_set$) > B_update_set$).
% 21.05/7.45  tff(uvq$, type, uvq$: A_update_b_update_fun$ > A_update_a_b_prod_update_fun$).
% 21.05/7.45  tff(rel_fun$g, type, rel_fun$g: (C_update_c_d_prod_update_bool_fun_fun$ * A_update_a_update_bool_fun_fun$) > C_update_a_update_fun_c_d_prod_update_a_update_fun_bool_fun_fun$).
% 21.05/7.45  tff('#skF_63', type, '#skF_63': (C_update_a_update_fun$ * C_update_a_update_fun$) > C_update$).
% 21.05/7.45  tff('#skF_42', type, '#skF_42': (C_update_a_update_fun$ * C_update_a_update_fun$ * C_update$ * C_update$) > C_update$).
% 21.05/7.45  tff(comp$b, type, comp$b: (A_update_a_update_fun$ * C_update_a_update_fun$) > C_update_a_update_fun$).
% 21.05/7.45  tff(uuu$, type, uuu$: B_update_b_update_fun$ > B_update_d_b_prod_update_fun$).
% 21.05/7.45  tff(rel_fun$af, 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$).
% 21.05/7.45  tff(compatible$a, type, compatible$a: (A_update_b_update_fun$ * C_update_b_update_fun$) > $o).
% 21.05/7.45  tff(fun_app$ac, type, fun_app$ac: (A_update_c_update_fun$ * A_update$) > C_update$).
% 21.05/7.45  tff('#skF_13', type, '#skF_13': (D_update_b_update_fun$ * C_update_b_update_fun$) > D_update$).
% 21.05/7.45  tff(register_tensor$u, 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$).
% 21.05/7.45  tff(comp$am, type, comp$am: (A_update_b_update_fun$ * A_update_a_update_fun$) > A_update_b_update_fun$).
% 21.05/7.45  tff(fun_app$o, type, fun_app$o: (D_update_b_a_prod_update_fun$ * D_update$) > B_a_prod_update$).
% 21.05/7.45  tff(rel_fun$w, 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$).
% 21.05/7.45  tff(register$az, type, register$az: D_update_d_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(fun_app$dw, type, fun_app$dw: (B_update_d_update_fun_c_d_prod_update_b_update_fun_fun$ * B_update_d_update_fun$) > C_d_prod_update_b_update_fun$).
% 21.05/7.45  tff(comp$p, type, comp$p: (B_update_b_update_fun$ * D_update_b_update_fun$) > D_update_b_update_fun$).
% 21.05/7.45  tff(fun_app$d, type, fun_app$d: (A_update_a_c_prod_update_fun$ * A_update$) > A_c_prod_update$).
% 21.05/7.45  tff(register$bd, type, register$bd: A_update_d_a_prod_update_fun$ > $o).
% 21.05/7.45  tff(register$e, type, register$e: D_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(preregister$d, type, preregister$d: D_update_b_update_fun$ > $o).
% 21.05/7.45  tff(top$, type, top$: C_d_prod_update_set$).
% 21.05/7.45  tff(uvk$, type, uvk$: C_update_a_update_fun$ > C_update_a_a_prod_update_fun$).
% 21.05/7.45  tff(register$m, type, register$m: C_c_prod_update_b_b_prod_update_fun$ > $o).
% 21.05/7.45  tff(tensor_update$j, type, tensor_update$j: (D_update$ * A_update$) > D_a_prod_update$).
% 21.05/7.45  tff('#skF_92', type, '#skF_92': (B_itself$ * C_update_set$) > C_update_b_update_fun$).
% 21.05/7.45  tff(fun_app$cc, type, fun_app$cc: (A_d_prod_update_a_update_fun$ * A_d_prod_update$) > A_update$).
% 21.05/7.45  tff(register_pair$u, 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$).
% 21.05/7.45  tff(comp$ao, type, comp$ao: (D_update_b_update_fun$ * D_update_d_update_fun$) > D_update_b_update_fun$).
% 21.05/7.45  tff(register$bi, type, register$bi: A_update_a_a_prod_update_fun$ > $o).
% 21.05/7.45  tff(fun_app$dt, type, fun_app$dt: (A_update_a_update_fun_c_d_prod_update_b_update_fun_fun$ * A_update_a_update_fun$) > C_d_prod_update_b_update_fun$).
% 21.05/7.45  tff('#skF_70', type, '#skF_70': (A_update_b_update_fun$ * C_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff(map_prod$h, type, map_prod$h: (C_d_prod_update_a_update_fun$ * C_update_a_update_fun$) > C_d_prod_update_c_update_prod_a_update_a_update_prod_fun$).
% 21.05/7.45  tff(member$a, type, member$a: (D_update$ * D_update_set$) > $o).
% 21.05/7.45  tff(fun_app$ah, type, fun_app$ah: (D_update_bool_fun$ * D_update$) > $o).
% 21.05/7.45  tff(uua$, type, uua$: D_update_set$ > D_update_bool_fun$).
% 21.05/7.45  tff('#skF_78', type, '#skF_78': (D_update_b_update_fun$ * A_update_b_update_fun$) > A_update$).
% 21.05/7.45  tff(uuq$, type, uuq$: C_update_a_update_fun$ > C_update_d_a_prod_update_fun$).
% 21.05/7.45  tff(fcomp$b, 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$).
% 21.05/7.45  tff(uup$, type, uup$: B_update_b_update_fun$ > B_update_b_b_prod_update_fun$).
% 21.05/7.45  tff('#skF_97', type, '#skF_97': (A_itself$ * C_update_set$ * C_update_a_update_fun$ * C_update_a_update_fun$) > C_update$).
% 21.05/7.45  tff(rel_fun$ai, 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$).
% 21.05/7.45  tff(fun_app$bg, type, fun_app$bg: (D_update_d_update_fun$ * D_update$) > D_update$).
% 21.05/7.45  tff(map_fun$g, type, map_fun$g: (C_d_prod_update_a_update_fun$ * A_update_b_update_fun$) > A_update_a_update_fun_c_d_prod_update_b_update_fun_fun$).
% 21.05/7.45  tff(less_eq$, type, less_eq$: (A_update_set$ * A_update_set$) > $o).
% 21.05/7.45  tff(compatible$ai, type, compatible$ai: (C_update_b_a_prod_update_fun$ * A_update_b_a_prod_update_fun$) > $o).
% 21.05/7.45  tff(register_tensor$r, type, register_tensor$r: (D_update_b_update_fun$ * C_update_b_update_fun$) > D_c_prod_update_b_b_prod_update_fun$).
% 21.05/7.45  tff(uvt$, type, uvt$: C_update_bool_fun$).
% 21.05/7.45  tff(comp$by, type, comp$by: (A_update_a_update_prod_b_update_b_update_prod_fun$ * C_d_prod_update_c_d_prod_update_prod_a_update_a_update_prod_fun$) > C_d_prod_update_c_d_prod_update_prod_b_update_b_update_prod_fun$).
% 21.05/7.45  tff(fun_app$ba, type, fun_app$ba: (A_update_d_c_prod_update_fun$ * A_update$) > D_c_prod_update$).
% 21.05/7.45  tff(rel_fun$ad, 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$).
% 21.05/7.45  tff(preregister$i, type, preregister$i: D_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(id_update$b, type, id_update$b: C_update$).
% 21.05/7.45  tff(fun_app$e, type, fun_app$e: (C_update_a_c_prod_update_fun$ * C_update$) > A_c_prod_update$).
% 21.05/7.45  tff(uvy$, type, uvy$: C_d_prod_update_c_d_prod_update_bool_fun_fun$).
% 21.05/7.45  tff(register$ae, type, register$ae: C_d_prod_update_a_update_fun_bool_fun$).
% 21.05/7.45  tff(compatible$k, type, compatible$k: (D_update_a_update_fun$ * A_update_a_update_fun$) > $o).
% 21.05/7.45  tff(type_definition$f, type, type_definition$f: (A_update_c_update_fun$ * C_update_a_update_fun$ * C_update_set$) > $o).
% 21.05/7.45  tff('#skF_39', type, '#skF_39': (C_update_a_update_fun$ * D_update_a_update_fun$) > C_update$).
% 21.05/7.45  tff(compatible$aa, type, compatible$aa: (C_update_b_update_fun$ * B_update_b_update_fun$) > $o).
% 21.05/7.45  tff(fun_app$ar, 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$).
% 21.05/7.45  tff(rel_fun$y, 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).
% 21.05/7.45  tff('#skF_45', type, '#skF_45': (C_update_b_update_fun$ * A_update_b_update_fun$ * C_update$ * A_update$) > C_update$).
% 21.05/7.45  tff(uvx$, type, uvx$: C_update_c_update_bool_fun_fun$).
% 21.05/7.45  tff(type_definition$d, type, type_definition$d: (D_update_c_update_fun$ * C_update_d_update_fun$ * C_update_set$) > $o).
% 21.05/7.45  tff(register$bc, type, register$bc: A_update_d_c_prod_update_fun$ > $o).
% 21.05/7.45  tff(fun_app$af, type, fun_app$af: (A_update_b_b_prod_update_fun$ * A_update$) > B_b_prod_update$).
% 21.05/7.45  tff('#skF_43', type, '#skF_43': (C_update_b_update_fun$ * C_update_b_update_fun$ * C_update$ * C_update$) > C_update$).
% 21.05/7.45  tff(comp$be, type, comp$be: (C_update_b_update_b_update_prod_fun$ * C_update_c_update_fun$) > C_update_b_update_b_update_prod_fun$).
% 21.05/7.45  tff(quotient$k, 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).
% 21.05/7.45  tff(uuh$, type, uuh$: A_update_b_update_fun$ > A_update_b_d_prod_update_fun$).
% 21.05/7.45  tff('#skF_14', type, '#skF_14': (D_update_b_update_fun$ * C_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff(fcomp$e, type, fcomp$e: (C_update_a_update_fun$ * A_update_b_update_fun$) > C_update_b_update_fun$).
% 21.05/7.45  tff(uun$, type, uun$: A_update_b_update_fun$ > A_update_b_b_prod_update_fun$).
% 21.05/7.45  tff(fun_app$ch, type, fun_app$ch: (C_a_prod_update_b_update_fun$ * C_a_prod_update$) > B_update$).
% 21.05/7.45  tff('#skF_100', type, '#skF_100': (B_itself$ * B_update_set$ * B_update_b_update_fun$ * B_update_b_update_fun$) > B_update$).
% 21.05/7.45  tff(comp_update$b, type, comp_update$b: D_update$ > D_update_d_update_fun$).
% 21.05/7.45  tff(map_prod$i, type, map_prod$i: (C_d_prod_update_b_update_fun$ * C_d_prod_update_b_update_fun$) > C_d_prod_update_c_d_prod_update_prod_b_update_b_update_prod_fun$).
% 21.05/7.45  tff(fun_app$dy, type, fun_app$dy: (B_update_set_b_update_fun$ * B_update_set$) > B_update$).
% 21.05/7.45  tff('#skF_85', type, '#skF_85': (C_d_prod_update_a_update_fun_bool_fun$ * C_d_prod_update_a_update_fun_bool_fun$) > C_d_prod_update_a_update_fun$).
% 21.05/7.45  tff(fun_app$cs, 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$).
% 21.05/7.45  tff(image$c, type, image$c: (C_update_b_update_fun$ * C_update_set$) > B_update_set$).
% 21.05/7.45  tff(rel_fun$d, 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$).
% 21.05/7.45  tff(member$c, type, member$c: (A_update$ * A_update_set$) > $o).
% 21.05/7.45  tff(register_pair$f, type, register_pair$f: (D_update_b_update_fun$ * A_update_b_update_fun$) > D_a_prod_update_b_update_fun$).
% 21.05/7.45  tff(tensor_update$a, type, tensor_update$a: A_update$ > D_update_a_d_prod_update_fun$).
% 21.05/7.45  tff(register_tensor$y, type, register_tensor$y: (C_d_prod_update_b_update_fun$ * C_update_b_update_fun$) > C_d_prod_c_prod_update_b_b_prod_update_fun$).
% 21.05/7.45  tff('#skF_24', type, '#skF_24': (C_update_b_update_fun$ * C_update_b_update_fun$) > C_update$).
% 21.05/7.45  tff('#skF_55', type, '#skF_55': (D_update_b_update_fun$ * A_update_b_update_fun$ * D_update$ * A_update$) > D_update$).
% 21.05/7.45  
% 21.05/7.46  tff(f_249, negated_conjecture, ~fun_app$k(register$, g$), file('/export/starexec/sandbox/benchmark/theBenchmark.p', conjecture59)).
% 21.05/7.46  tff(f_251, axiom, fun_app$j(compatible$(g$), h$), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom60)).
% 21.05/7.46  tff(f_643, axiom, (![A__questionmark_v0:C_update_a_update_fun$, A__questionmark_v1:D_update_a_update_fun$]: (fun_app$j(compatible$(A__questionmark_v0), A__questionmark_v1) <=> ((fun_app$k(register$, A__questionmark_v0) & fun_app$j(register$e, A__questionmark_v1)) & (![A__questionmark_v2:C_update$, A__questionmark_v3:D_update$]: (fun_app$bd(comp_update$(fun_app$u(A__questionmark_v0, A__questionmark_v2)), fun_app$au(A__questionmark_v1, A__questionmark_v3)) = fun_app$bd(comp_update$(fun_app$au(A__questionmark_v1, A__questionmark_v3)), fun_app$u(A__questionmark_v0, A__questionmark_v2))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom115)).
% 21.05/7.46  tff(c_154, plain, (~fun_app$k(register$, g$)), inference(cnfTransformation, [status(thm)], [f_249])).
% 21.05/7.46  tff(c_156, plain, (fun_app$j(compatible$(g$), h$)), inference(cnfTransformation, [status(thm)], [f_251])).
% 21.05/7.46  tff(c_2425, plain, (![A__questionmark_v0_2581:C_update_a_update_fun$, A__questionmark_v1_2582:D_update_a_update_fun$]: (fun_app$k(register$, A__questionmark_v0_2581) | ~fun_app$j(compatible$(A__questionmark_v0_2581), A__questionmark_v1_2582))), inference(cnfTransformation, [status(thm)], [f_643])).
% 21.05/7.46  tff(c_2428, plain, (fun_app$k(register$, g$)), inference(resolution, [status(thm)], [c_156, c_2425])).
% 21.05/7.46  tff(c_2432, plain, $false, inference(negUnitSimplification, [status(thm)], [c_154, c_2428])).
% 21.05/7.46  % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------