%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC504_1 : TPTP v9.3.1. Bugfixed v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:06:07 PM UTC 2026
% Result : Theorem 1.51s 0.48s
% Output : Refutation 1.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC504_1 : TPTP v9.3.1. Bugfixed v9.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n007.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 09:39:10 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.51/0.48 % (2275124)Will run a generic schedule for satisfiability detection.
% 1.51/0.48 % (2275131)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4183742514:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.51/0.48 % (2275130)% WARNING: option uhcvi not known.
% 1.51/0.48 % (2275129)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1243411344_2999 on theBenchmark for (2999ds/0Mi)
% 1.51/0.48 % (2275130)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=579465785:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.51/0.48 % (2275132)dis+10_1_sil=32000:sp=arity:random_seed=1830252924:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.51/0.48 % (2275133)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3558541564:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.51/0.48 % (2275134)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=408968966:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.51/0.48 % (2275135)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3188971265:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.51/0.48 % (2275129)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.51/0.48 % (2275129)Terminated due to inappropriate strategy.
% 1.51/0.48 % (2275129)------------------------------
% 1.51/0.48 % (2275129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.48 % (2275129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.48 % (2275129)CaDiCaL version: 2.1.3
% 1.51/0.48 % (2275129)Termination reason: Inappropriate
% 1.51/0.48 % (2275129)Time elapsed: 0.041 s
% 1.51/0.48 % (2275129)Peak memory usage: 14 MB
% 1.51/0.48 % (2275129)Instructions burned: 86 (million)
% 1.51/0.48 % (2275129)------------------------------
% 1.51/0.48 % (2275129)------------------------------
% 1.51/0.48 % (2275132)Instruction limit reached!
% 1.51/0.48 % (2275132)------------------------------
% 1.51/0.48 % (2275132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.48 % (2275132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.48 % (2275132)CaDiCaL version: 2.1.3
% 1.51/0.48 % (2275132)Termination reason: Instruction limit
% 1.51/0.48 % (2275132)Termination phase: Saturation
% 1.51/0.48 % (2275132)Time elapsed: 0.049 s
% 1.51/0.48 % (2275132)Peak memory usage: 15 MB
% 1.51/0.48 % (2275132)Instructions burned: 104 (million)
% 1.51/0.48 % (2275133)Instruction limit reached!
% 1.51/0.48 % (2275133)------------------------------
% 1.51/0.48 % (2275133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.48 % (2275133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.48 % (2275133)CaDiCaL version: 2.1.3
% 1.51/0.48 % (2275133)Termination reason: Instruction limit
% 1.51/0.48 % (2275133)Termination phase: Property scanning
% 1.51/0.48 % (2275133)Time elapsed: 0.053 s
% 1.51/0.48 % (2275133)Peak memory usage: 14 MB
% 1.51/0.48 % (2275133)Instructions burned: 116 (million)
% 1.51/0.48 % (2275143)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3996092762:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.51/0.48 % (2275134)Instruction limit reached!
% 1.51/0.48 % (2275134)------------------------------
% 1.51/0.48 % (2275134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.48 % (2275134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.48 % (2275134)CaDiCaL version: 2.1.3
% 1.51/0.48 % (2275134)Termination reason: Instruction limit
% 1.51/0.48 % (2275134)Termination phase: Saturation
% 1.51/0.48 % (2275134)Time elapsed: 0.063 s
% 1.51/0.48 % (2275134)Peak memory usage: 16 MB
% 1.51/0.48 % (2275134)Instructions burned: 132 (million)
% 1.51/0.48 % (2275144)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=763469978:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.51/0.48 % (2275145)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2143772821:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.51/0.48 % (2275135)Instruction limit reached!
% 1.51/0.48 % (2275135)------------------------------
% 1.51/0.48 % (2275135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.48 % (2275135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.48 % (2275135)CaDiCaL version: 2.1.3
% 1.51/0.48 % (2275135)Termination reason: Instruction limit
% 1.51/0.48 % (2275135)Termination phase: Saturation
% 1.51/0.48 % (2275135)Time elapsed: 0.076 s
% 1.51/0.48 % (2275135)Peak memory usage: 16 MB
% 1.51/0.48 % (2275135)Instructions burned: 159 (million)
% 1.51/0.48 % (2275147)ott-21_1_sil=16000:fs=off:random_seed=310044427:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.51/0.48 % (2275150)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=506329531:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.51/0.48 % (2275143)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.51/0.48 % (2275143)Terminated due to inappropriate strategy.
% 1.51/0.48 % (2275143)------------------------------
% 1.51/0.48 % (2275143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.48 % (2275143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.48 % (2275143)CaDiCaL version: 2.1.3
% 1.51/0.48 % (2275143)Termination reason: Inappropriate
% 1.51/0.48 % (2275143)Time elapsed: 0.035 s
% 1.51/0.48 % (2275143)Peak memory usage: 14 MB
% 1.51/0.48 % (2275143)Instructions burned: 73 (million)
% 1.51/0.48 % (2275143)------------------------------
% 1.51/0.48 % (2275143)------------------------------
% 1.51/0.48 % (2275153)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4069178784:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.51/0.48 % (2275144)Instruction limit reached!
% 1.51/0.48 % (2275144)------------------------------
% 1.51/0.48 % (2275144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.48 % (2275144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.48 % (2275144)CaDiCaL version: 2.1.3
% 1.51/0.48 % (2275144)Termination reason: Instruction limit
% 1.51/0.48 % (2275144)Termination phase: Saturation
% 1.51/0.48 % (2275144)Time elapsed: 0.067 s
% 1.51/0.48 % (2275144)Peak memory usage: 16 MB
% 1.51/0.48 % (2275144)Instructions burned: 132 (million)
% 1.51/0.48 % (2275153)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.51/0.48 % (2275153)Terminated due to inappropriate strategy.
% 1.51/0.48 % (2275153)------------------------------
% 1.51/0.48 % (2275153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.48 % (2275153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.48 % (2275153)CaDiCaL version: 2.1.3
% 1.51/0.48 % (2275153)Termination reason: Inappropriate
% 1.51/0.48 % (2275153)Time elapsed: 0.032 s
% 1.51/0.48 % (2275153)Peak memory usage: 14 MB
% 1.51/0.48 % (2275153)Instructions burned: 70 (million)
% 1.51/0.48 % (2275153)------------------------------
% 1.51/0.48 % (2275153)------------------------------
% 1.51/0.48 % (2275155)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1927851134:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 1.51/0.48 % (2275147)Instruction limit reached!
% 1.51/0.48 % (2275147)------------------------------
% 1.51/0.48 % (2275147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.48 % (2275147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.48 % (2275147)CaDiCaL version: 2.1.3
% 1.51/0.48 % (2275147)Termination reason: Instruction limit
% 1.51/0.48 % (2275147)Termination phase: Saturation
% 1.51/0.48 % (2275147)Time elapsed: 0.084 s
% 1.51/0.48 % (2275147)Peak memory usage: 16 MB
% 1.51/0.48 % (2275147)Instructions burned: 181 (million)
% 1.51/0.48 % (2275156)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=243741201:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 1.51/0.48 % (2275131) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2275124-2275131"...
% 1.51/0.48 % (2275158)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3958486646:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 1.51/0.48 % (2275131)...printing done.
% 1.51/0.48 % (2275131)Refutation found. Thanks to Tanya!
% 1.51/0.48 % SZS status Theorem for theBenchmark
% 1.51/0.48 % SZS output start Proof for theBenchmark
% 1.51/0.48 tff(type_def_5, type, set_0: $tType).
% 1.51/0.48 tff(type_def_6, type, set_2: $tType).
% 1.51/0.48 tff(type_def_7, type, set_3: $tType).
% 1.51/0.48 tff(type_def_8, type, set_4: $tType).
% 1.51/0.48 tff(type_def_9, type, set_5: $tType).
% 1.51/0.48 tff(type_def_10, type, set_6: $tType).
% 1.51/0.48 tff(func_def_0, type, min_int: $int).
% 1.51/0.48 tff(func_def_1, type, max_int: $int).
% 1.51/0.48 tff(func_def_5, type, divB: ($int * $int) > $int).
% 1.51/0.48 tff(func_def_8, type, g_s0_0: set_0).
% 1.51/0.48 tff(func_def_9, type, g_s1_1: $int).
% 1.51/0.48 tff(func_def_10, type, g_s2_2: $int).
% 1.51/0.48 tff(func_def_11, type, g_s3_3: $int).
% 1.51/0.48 tff(func_def_12, type, g_s4_4: set_0).
% 1.51/0.48 tff(func_def_13, type, g_s5_5: $int).
% 1.51/0.48 tff(func_def_14, type, g_s6_6: $int).
% 1.51/0.48 tff(func_def_15, type, g_s7_7: $int).
% 1.51/0.48 tff(func_def_16, type, g_s8_8: set_0).
% 1.51/0.48 tff(func_def_17, type, g_s9_9: $int).
% 1.51/0.48 tff(func_def_18, type, g_s10_10: $int).
% 1.51/0.48 tff(func_def_19, type, g_s11_11: $int).
% 1.51/0.48 tff(func_def_20, type, g_s12_12: set_0).
% 1.51/0.48 tff(func_def_21, type, g_s13_13: $int).
% 1.51/0.48 tff(func_def_22, type, g_s14_14: $int).
% 1.51/0.48 tff(func_def_23, type, g_s15_15: $int).
% 1.51/0.48 tff(func_def_24, type, g_s16_16: $int).
% 1.51/0.48 tff(func_def_25, type, g_s17_17: $int).
% 1.51/0.48 tff(func_def_26, type, g_s18_18: set_0).
% 1.51/0.48 tff(func_def_27, type, g_s19_19: $int).
% 1.51/0.48 tff(func_def_28, type, g_s20_20: $int).
% 1.51/0.48 tff(func_def_29, type, g_s21_21: set_0).
% 1.51/0.48 tff(func_def_30, type, g_s22_22: $int).
% 1.51/0.48 tff(func_def_31, type, g_s23_23: $int).
% 1.51/0.48 tff(func_def_32, type, g_s24_24: $int).
% 1.51/0.48 tff(func_def_33, type, g_s25_25: $int).
% 1.51/0.48 tff(func_def_34, type, g_s26_26: set_0).
% 1.51/0.48 tff(func_def_35, type, g_s27_27: $int).
% 1.51/0.48 tff(func_def_36, type, g_s28_28: $int).
% 1.51/0.48 tff(func_def_37, type, g_s29_29: $int).
% 1.51/0.48 tff(func_def_38, type, g_s30_30: $int).
% 1.51/0.48 tff(func_def_39, type, g_s31_31: $int).
% 1.51/0.48 tff(func_def_40, type, g_s32_32: set_0).
% 1.51/0.48 tff(func_def_41, type, g_s33_33: $int).
% 1.51/0.48 tff(func_def_42, type, g_s34_34: $int).
% 1.51/0.48 tff(func_def_43, type, g_s35_35: $int).
% 1.51/0.48 tff(func_def_44, type, g_s36_36: set_0).
% 1.51/0.48 tff(func_def_45, type, g_s37_37: $int).
% 1.51/0.48 tff(func_def_46, type, g_s38_38: $int).
% 1.51/0.48 tff(func_def_47, type, g_s39_39: set_0).
% 1.51/0.48 tff(func_def_48, type, g_s40_40: $int).
% 1.51/0.48 tff(func_def_49, type, g_s41_41: $int).
% 1.51/0.48 tff(func_def_50, type, g_s42_42: $int).
% 1.51/0.48 tff(func_def_51, type, g_s43_43: set_0).
% 1.51/0.48 tff(func_def_52, type, g_s44_44: $int).
% 1.51/0.48 tff(func_def_53, type, g_s45_45: $int).
% 1.51/0.48 tff(func_def_54, type, g_s46_46: $int).
% 1.51/0.48 tff(func_def_55, type, g_s47_47: set_0).
% 1.51/0.48 tff(func_def_56, type, g_s48_48: $int).
% 1.51/0.48 tff(func_def_57, type, g_s49_49: $int).
% 1.51/0.48 tff(func_def_58, type, g_s50_50: $int).
% 1.51/0.48 tff(func_def_59, type, g_s51_51: set_0).
% 1.51/0.48 tff(func_def_60, type, g_s52_52: $int).
% 1.51/0.48 tff(func_def_61, type, g_s53_53: $int).
% 1.51/0.48 tff(func_def_62, type, g_s54_54: $int).
% 1.51/0.48 tff(func_def_63, type, g_s55_55: $int).
% 1.51/0.48 tff(func_def_64, type, g_s56_56: set_0).
% 1.51/0.48 tff(func_def_65, type, g_s57_57: $int).
% 1.51/0.48 tff(func_def_66, type, g_s58_58: $int).
% 1.51/0.48 tff(func_def_67, type, g_s59_59: $int).
% 1.51/0.48 tff(func_def_68, type, g_s60_60: $int).
% 1.51/0.48 tff(func_def_69, type, g_s61_61: $int).
% 1.51/0.48 tff(func_def_70, type, g_s62_62: $int).
% 1.51/0.48 tff(func_def_71, type, g_s63_63: $int).
% 1.51/0.48 tff(func_def_72, type, g_s64_64: $int).
% 1.51/0.48 tff(func_def_73, type, g_s65_65: $int).
% 1.51/0.48 tff(func_def_74, type, g_s66_66: $int).
% 1.51/0.48 tff(func_def_75, type, g_s67_67: $int).
% 1.51/0.48 tff(func_def_76, type, g_s68_68: $int).
% 1.51/0.48 tff(func_def_77, type, g_s69_69: $int).
% 1.51/0.48 tff(func_def_78, type, g_s70_70: $int).
% 1.51/0.48 tff(func_def_79, type, g_s71_71: $int).
% 1.51/0.48 tff(func_def_80, type, g_s72_72: set_0).
% 1.51/0.48 tff(func_def_81, type, g_s73_73: $int).
% 1.51/0.48 tff(func_def_82, type, g_s74_74: $int).
% 1.51/0.48 tff(func_def_83, type, g_s75_75: $int).
% 1.51/0.48 tff(func_def_84, type, g_s76_76: $int).
% 1.51/0.48 tff(func_def_85, type, g_s77_77: $int).
% 1.51/0.48 tff(func_def_86, type, g_s78_78: $int).
% 1.51/0.48 tff(func_def_87, type, g_s79_79: $int).
% 1.51/0.48 tff(func_def_88, type, g_s80_80: $int).
% 1.51/0.48 tff(func_def_89, type, g_s81_81: $int).
% 1.51/0.48 tff(func_def_90, type, g_s82_82: $int).
% 1.51/0.48 tff(func_def_91, type, g_s83_83: $int).
% 1.51/0.48 tff(func_def_92, type, g_s84_84: $int).
% 1.51/0.48 tff(func_def_93, type, g_s85_85: $int).
% 1.51/0.48 tff(func_def_94, type, g_s86_86: $int).
% 1.51/0.48 tff(func_def_95, type, g_s87_87: $int).
% 1.51/0.48 tff(func_def_96, type, g_s88_88: $int).
% 1.51/0.48 tff(func_def_97, type, g_s89_89: $int).
% 1.51/0.48 tff(func_def_98, type, g_s90_90: $int).
% 1.51/0.48 tff(func_def_99, type, g_s91_91: $int).
% 1.51/0.48 tff(func_def_100, type, g_s92_92: $int).
% 1.51/0.48 tff(func_def_101, type, g_s93_93: $int).
% 1.51/0.48 tff(func_def_102, type, g_s94_94: $int).
% 1.51/0.48 tff(func_def_103, type, g_s95_95: $int).
% 1.51/0.48 tff(func_def_104, type, g_s96_96: $int).
% 1.51/0.48 tff(func_def_105, type, g_s97_97: $int).
% 1.51/0.48 tff(func_def_106, type, g_s98_98: $int).
% 1.51/0.48 tff(func_def_107, type, g_s99_99: $int).
% 1.51/0.48 tff(func_def_108, type, g_s100_100: $int).
% 1.51/0.48 tff(func_def_109, type, g_s101_101: $int).
% 1.51/0.48 tff(func_def_110, type, g_s102_102: $int).
% 1.51/0.48 tff(func_def_111, type, g_s103_103: $int).
% 1.51/0.48 tff(func_def_112, type, g_s104_104: $int).
% 1.51/0.48 tff(func_def_113, type, g_s105_105: set_0).
% 1.51/0.48 tff(func_def_114, type, g_s106_106: $int).
% 1.51/0.48 tff(func_def_115, type, g_s107_107: $int).
% 1.51/0.48 tff(func_def_116, type, g_s108_108: $int).
% 1.51/0.48 tff(func_def_117, type, g_s109_109: $int).
% 1.51/0.48 tff(func_def_118, type, g_s110_110: set_0).
% 1.51/0.48 tff(func_def_119, type, g_s111_111: $int).
% 1.51/0.48 tff(func_def_120, type, g_s112_112: $int).
% 1.51/0.48 tff(func_def_121, type, g_s113_113: $int).
% 1.51/0.48 tff(func_def_122, type, g_s114_114: $int).
% 1.51/0.48 tff(func_def_123, type, g_s115_115: $int).
% 1.51/0.48 tff(func_def_124, type, g_s116_116: $int).
% 1.51/0.48 tff(func_def_125, type, g_s117_117: $int).
% 1.51/0.48 tff(func_def_126, type, g_s118_118: set_0).
% 1.51/0.48 tff(func_def_127, type, g_s119_119: $int).
% 1.51/0.48 tff(func_def_128, type, g_s120_120: $int).
% 1.51/0.48 tff(func_def_129, type, g_s121_121: $int).
% 1.51/0.48 tff(func_def_130, type, g_s122_122: $int).
% 1.51/0.48 tff(func_def_131, type, g_s123_123: set_0).
% 1.51/0.48 tff(func_def_132, type, g_s124_124: $int).
% 1.51/0.48 tff(func_def_133, type, g_s125_125: $int).
% 1.51/0.48 tff(func_def_134, type, g_s126_126: $int).
% 1.51/0.48 tff(func_def_135, type, g_s127_127: $int).
% 1.51/0.48 tff(func_def_136, type, g_s128_128: $int).
% 1.51/0.48 tff(func_def_137, type, g_s129_129: set_0).
% 1.51/0.48 tff(func_def_138, type, g_s130_130: $int).
% 1.51/0.48 tff(func_def_139, type, g_s131_131: $int).
% 1.51/0.48 tff(func_def_140, type, g_s132_132: $int).
% 1.51/0.48 tff(func_def_141, type, g_s133_133: $int).
% 1.51/0.48 tff(func_def_142, type, g_s134_134: $int).
% 1.51/0.48 tff(func_def_143, type, g_s135_135: $int).
% 1.51/0.48 tff(func_def_144, type, g_s136_136: set_0).
% 1.51/0.48 tff(func_def_145, type, g_s137_137: $int).
% 1.51/0.48 tff(func_def_146, type, g_s138_138: $int).
% 1.51/0.48 tff(func_def_147, type, g_s139_139: $int).
% 1.51/0.48 tff(func_def_148, type, g_s140_140: $int).
% 1.51/0.48 tff(func_def_149, type, g_s141_141: $int).
% 1.51/0.48 tff(func_def_150, type, g_s142_142: $int).
% 1.51/0.48 tff(func_def_151, type, g_s143_143: set_0).
% 1.51/0.48 tff(func_def_152, type, g_s144_144: $int).
% 1.51/0.48 tff(func_def_153, type, g_s145_145: $int).
% 1.51/0.48 tff(func_def_154, type, g_s146_146: $int).
% 1.51/0.48 tff(func_def_155, type, g_s147_147: set_0).
% 1.51/0.48 tff(func_def_156, type, g_s148_148: $int).
% 1.51/0.48 tff(func_def_157, type, g_s149_149: $int).
% 1.51/0.48 tff(func_def_158, type, g_s150_150: $int).
% 1.51/0.48 tff(func_def_159, type, g_s151_151: $int).
% 1.51/0.48 tff(func_def_160, type, g_s152_152: set_0).
% 1.51/0.48 tff(func_def_161, type, g_s153_153: $int).
% 1.51/0.48 tff(func_def_162, type, g_s154_154: $int).
% 1.51/0.48 tff(func_def_163, type, g_s155_155: $int).
% 1.51/0.48 tff(func_def_164, type, g_s156_156: set_0).
% 1.51/0.48 tff(func_def_165, type, g_s157_157: $int).
% 1.51/0.48 tff(func_def_166, type, g_s158_158: $int).
% 1.51/0.48 tff(func_def_167, type, g_s159_159: $int).
% 1.51/0.48 tff(func_def_168, type, g_s160_160: $int).
% 1.51/0.48 tff(func_def_169, type, g_s161_161: set_0).
% 1.51/0.48 tff(func_def_170, type, g_s162_162: $int).
% 1.51/0.48 tff(func_def_171, type, g_s163_163: $int).
% 1.51/0.48 tff(func_def_172, type, g_s164_164: $int).
% 1.51/0.48 tff(func_def_173, type, g_s165_165: $int).
% 1.51/0.48 tff(func_def_174, type, g_s166_166: set_0).
% 1.51/0.48 tff(func_def_175, type, g_s167_167: $int).
% 1.51/0.48 tff(func_def_176, type, g_s168_168: $int).
% 1.51/0.48 tff(func_def_177, type, g_s169_169: $int).
% 1.51/0.48 tff(func_def_178, type, g_s170_170: $int).
% 1.51/0.48 tff(func_def_179, type, g_s171_171: set_0).
% 1.51/0.48 tff(func_def_180, type, g_s172_172: $int).
% 1.51/0.48 tff(func_def_181, type, g_s173_173: $int).
% 1.51/0.48 tff(func_def_182, type, g_s174_174: $int).
% 1.51/0.48 tff(func_def_183, type, g_s175_175: set_0).
% 1.51/0.48 tff(func_def_184, type, g_s176_176: $int).
% 1.51/0.48 tff(func_def_185, type, g_s177_177: $int).
% 1.51/0.48 tff(func_def_186, type, g_s178_178: $int).
% 1.51/0.48 tff(func_def_187, type, set_2_empty: set_2).
% 1.51/0.48 tff(func_def_188, type, set_2_insert: $o > set_2).
% 1.51/0.48 tff(func_def_189, type, g_s179_179: set_2).
% 1.51/0.48 tff(func_def_190, type, g_s180_180: set_2).
% 1.51/0.48 tff(func_def_191, type, g_s181_181: set_0).
% 1.51/0.48 tff(func_def_192, type, g_s182_182: set_0).
% 1.51/0.48 tff(func_def_193, type, g_s183_183: set_0).
% 1.51/0.48 tff(func_def_194, type, g_s184_184: set_0).
% 1.51/0.48 tff(func_def_195, type, g_s185_185: set_0).
% 1.51/0.48 tff(func_def_196, type, g_s186_186: set_0).
% 1.51/0.48 tff(func_def_197, type, g_s187_187: set_2).
% 1.51/0.48 tff(func_def_198, type, g_s188_188: set_0).
% 1.51/0.48 tff(func_def_199, type, g_s189_189: set_0).
% 1.51/0.48 tff(func_def_200, type, g_s190_190: $int).
% 1.51/0.48 tff(func_def_201, type, g_s191_191: $int).
% 1.51/0.48 tff(func_def_202, type, g_s192_192: $int).
% 1.51/0.48 tff(func_def_203, type, g_s193_193: $int).
% 1.51/0.48 tff(func_def_204, type, g_s194_194: $int).
% 1.51/0.48 tff(func_def_205, type, g_s195_195: $int).
% 1.51/0.48 tff(func_def_206, type, g_s196_196: $int).
% 1.51/0.48 tff(func_def_207, type, g_s197_197: $int).
% 1.51/0.48 tff(func_def_208, type, g_s198_198: $int).
% 1.51/0.48 tff(func_def_209, type, g_s199_199: $int).
% 1.51/0.48 tff(func_def_210, type, g_s200_200: $int).
% 1.51/0.48 tff(func_def_211, type, g_s201_201: $int).
% 1.51/0.48 tff(func_def_212, type, g_s202_202: $int).
% 1.51/0.48 tff(func_def_213, type, g_s203_203: $int).
% 1.51/0.48 tff(func_def_214, type, g_s204_204: $int).
% 1.51/0.48 tff(func_def_215, type, g_s205_205: $int).
% 1.51/0.48 tff(func_def_216, type, g_s206_206: $int).
% 1.51/0.48 tff(func_def_217, type, g_s207_207: $int).
% 1.51/0.48 tff(func_def_218, type, g_s208_208: $int).
% 1.51/0.48 tff(func_def_219, type, g_s209_209: $int).
% 1.51/0.48 tff(func_def_220, type, g_s210_210: $int).
% 1.51/0.48 tff(func_def_221, type, g_s211_211: $int).
% 1.51/0.48 tff(func_def_222, type, g_s212_212: $int).
% 1.51/0.48 tff(func_def_223, type, g_s213_213: $int).
% 1.51/0.48 tff(func_def_224, type, g_s214_214: $int).
% 1.51/0.48 tff(func_def_225, type, g_s215_215: $int).
% 1.51/0.48 tff(func_def_226, type, g_s216_216: $int).
% 1.51/0.48 tff(func_def_227, type, g_s217_217: $int).
% 1.51/0.48 tff(func_def_228, type, g_s218_218: $int).
% 1.51/0.48 tff(func_def_229, type, g_s219_219: $int).
% 1.51/0.48 tff(func_def_230, type, g_s220_220: $int).
% 1.51/0.48 tff(func_def_231, type, g_s221_221: $int).
% 1.51/0.48 tff(func_def_232, type, set_3_empty: set_3).
% 1.51/0.48 tff(func_def_233, type, set_3_insert: set_3 > set_3).
% 1.51/0.48 tff(func_def_234, type, g_s222_222: set_3).
% 1.51/0.48 tff(func_def_235, type, g_s224_223: set_3).
% 1.51/0.48 tff(func_def_236, type, g_s225_224: set_3).
% 1.51/0.48 tff(func_def_237, type, g_s226_225: set_3).
% 1.51/0.48 tff(func_def_238, type, set_4_empty: set_4).
% 1.51/0.48 tff(func_def_239, type, set_4_insert: set_4 > set_4).
% 1.51/0.48 tff(func_def_240, type, g_s227_226: set_4).
% 1.51/0.48 tff(func_def_241, type, g_s230_227: set_4).
% 1.51/0.48 tff(func_def_242, type, g_s231_228: set_4).
% 1.51/0.48 tff(func_def_243, type, g_s232_229: set_4).
% 1.51/0.48 tff(func_def_244, type, g_s233_230: set_4).
% 1.51/0.48 tff(func_def_245, type, g_s234_231: set_4).
% 1.51/0.48 tff(func_def_246, type, set_5_empty: set_5).
% 1.51/0.48 tff(func_def_247, type, set_5_insert: set_5 > set_5).
% 1.51/0.48 tff(func_def_248, type, g_s235_232: set_5).
% 1.51/0.48 tff(func_def_249, type, g_s238_233: set_5).
% 1.51/0.48 tff(func_def_250, type, g_s239_234: set_5).
% 1.51/0.48 tff(func_def_251, type, g_s240_235: set_5).
% 1.51/0.48 tff(func_def_252, type, g_s241_236: set_5).
% 1.51/0.48 tff(func_def_253, type, g_s242_237: set_5).
% 1.51/0.48 tff(func_def_254, type, g_s243_238: set_5).
% 1.51/0.48 tff(func_def_255, type, g_s244_239: set_5).
% 1.51/0.48 tff(func_def_256, type, g_s245_240: set_5).
% 1.51/0.48 tff(func_def_257, type, g_s246_241: set_5).
% 1.51/0.48 tff(func_def_258, type, g_s247_242: set_5).
% 1.51/0.48 tff(func_def_259, type, g_s248_243: set_5).
% 1.51/0.48 tff(func_def_260, type, g_s249_244: set_5).
% 1.51/0.48 tff(func_def_261, type, g_s250_245: set_5).
% 1.51/0.48 tff(func_def_262, type, g_s251_246: set_3).
% 1.51/0.48 tff(func_def_263, type, g_s252_247: set_3).
% 1.51/0.48 tff(func_def_264, type, g_s253_248: set_3).
% 1.51/0.48 tff(func_def_265, type, g_s254_249: set_3).
% 1.51/0.48 tff(func_def_266, type, g_s255_250: set_3).
% 1.51/0.48 tff(func_def_267, type, g_s256_251: set_5).
% 1.51/0.48 tff(func_def_268, type, g_s259_252: set_5).
% 1.51/0.48 tff(func_def_269, type, set_6_empty: set_6).
% 1.51/0.48 tff(func_def_270, type, set_6_insert: set_6 > set_6).
% 1.51/0.48 tff(func_def_271, type, g_s260_253: set_6).
% 1.51/0.48 tff(func_def_272, type, g_s262_254: set_6).
% 1.51/0.48 tff(func_def_273, type, g_s263_255: set_6).
% 1.51/0.48 tff(func_def_274, type, g_s265_256: set_3).
% 1.51/0.48 tff(func_def_275, type, g_s268_259: $int).
% 1.51/0.48 tff(func_def_276, type, g_s269_260: $int).
% 1.51/0.48 tff(func_def_277, type, g_s270_261: $int).
% 1.51/0.48 tff(func_def_278, type, g_s271_262: $int).
% 1.51/0.48 tff(func_def_279, type, g_s272_263: $int).
% 1.51/0.48 tff(func_def_280, type, g_s273_264: $int).
% 1.51/0.48 tff(func_def_281, type, g_s274_265: $int).
% 1.51/0.48 tff(func_def_282, type, g_s275_266: $int).
% 1.51/0.48 tff(func_def_283, type, g_s276_267: $int).
% 1.51/0.48 tff(func_def_284, type, g_s277_268: $int).
% 1.51/0.48 tff(func_def_285, type, g_s278_269: $int).
% 1.51/0.48 tff(func_def_286, type, g_s279_270: $int).
% 1.51/0.48 tff(func_def_287, type, g_s280_271: $int).
% 1.51/0.48 tff(func_def_288, type, g_s281_272: $int).
% 1.51/0.48 tff(func_def_289, type, g_s282_273: $int).
% 1.51/0.48 tff(func_def_290, type, g_s283_274: $int).
% 1.51/0.48 tff(func_def_291, type, g_s284_275: $int).
% 1.51/0.48 tff(func_def_292, type, g_s285_276: $int).
% 1.51/0.48 tff(func_def_293, type, g_s286_277: $int).
% 1.51/0.48 tff(func_def_294, type, g_s287_278: $int).
% 1.51/0.48 tff(func_def_295, type, g_s288_279: $int).
% 1.51/0.48 tff(func_def_296, type, g_s289_280: $int).
% 1.51/0.48 tff(func_def_297, type, g_s290_281: $int).
% 1.51/0.48 tff(func_def_298, type, g_s291_282: $int).
% 1.51/0.48 tff(func_def_299, type, g_s292_283: $int).
% 1.51/0.48 tff(func_def_300, type, g_s293_284: $int).
% 1.51/0.48 tff(func_def_301, type, g_s294_285: $int).
% 1.51/0.48 tff(func_def_302, type, g_s295_286: $int).
% 1.51/0.48 tff(func_def_303, type, g_s296_287: $int).
% 1.51/0.48 tff(func_def_304, type, g_s297_288: $int).
% 1.51/0.48 tff(func_def_305, type, g_s298_289: $int).
% 1.51/0.48 tff(func_def_306, type, g_s299_290: $int).
% 1.51/0.48 tff(func_def_307, type, g_s300_291: $int).
% 1.51/0.48 tff(func_def_308, type, g_s301_292: $int).
% 1.51/0.48 tff(func_def_309, type, g_s302_293: $int).
% 1.51/0.48 tff(func_def_310, type, g_s303_294: $int).
% 1.51/0.48 tff(func_def_311, type, g_s304_295: $int).
% 1.51/0.48 tff(func_def_312, type, g_s305_296: $int).
% 1.51/0.48 tff(func_def_313, type, g_s306_297: $int).
% 1.51/0.48 tff(func_def_314, type, g_s307_298: $int).
% 1.51/0.48 tff(func_def_315, type, g_s308_299: $int).
% 1.51/0.48 tff(func_def_316, type, g_s309_300: $int).
% 1.51/0.48 tff(func_def_317, type, g_s310_301: $int).
% 1.51/0.48 tff(func_def_318, type, g_s311_302: $int).
% 1.51/0.48 tff(func_def_319, type, g_s312_303: $int).
% 1.51/0.48 tff(func_def_320, type, g_s313_304: $int).
% 1.51/0.48 tff(func_def_321, type, g_s314_305: $int).
% 1.51/0.48 tff(func_def_322, type, g_s315_306: $int).
% 1.51/0.48 tff(func_def_323, type, g_s316_307: $int).
% 1.51/0.48 tff(func_def_324, type, g_s317_308: $int).
% 1.51/0.48 tff(func_def_325, type, g_s318_309: $int).
% 1.51/0.48 tff(func_def_326, type, g_s319_310: $int).
% 1.51/0.48 tff(func_def_327, type, g_s320_311: $int).
% 1.51/0.48 tff(func_def_328, type, g_s321_312: $int).
% 1.51/0.48 tff(func_def_329, type, g_s322_313: $int).
% 1.51/0.48 tff(func_def_330, type, g_s323_314: $int).
% 1.51/0.48 tff(func_def_331, type, g_s324_315: $int).
% 1.51/0.48 tff(func_def_332, type, g_s325_316: $int).
% 1.51/0.48 tff(func_def_333, type, g_s326_317: $int).
% 1.51/0.48 tff(func_def_334, type, g_s327_318: $int).
% 1.51/0.48 tff(func_def_335, type, g_s328_319: $int).
% 1.51/0.48 tff(func_def_336, type, g_s329_320: $int).
% 1.51/0.48 tff(func_def_337, type, g_s330_321: $int).
% 1.51/0.48 tff(func_def_338, type, g_s331_322: $int).
% 1.51/0.48 tff(func_def_339, type, g_s332_323: $int).
% 1.51/0.48 tff(func_def_340, type, g_s333_324: $int).
% 1.51/0.48 tff(func_def_341, type, g_s334_325: $int).
% 1.51/0.48 tff(func_def_342, type, g_s335_326: $int).
% 1.51/0.48 tff(func_def_343, type, g_s336_327: $int).
% 1.51/0.49 tff(func_def_344, type, g_s337_328: $int).
% 1.51/0.49 tff(func_def_345, type, g_s338_329: $int).
% 1.51/0.49 tff(func_def_346, type, g_s339_330: $int).
% 1.51/0.49 tff(func_def_347, type, g_s340_331: $int).
% 1.51/0.49 tff(func_def_348, type, g_s341_332: $int).
% 1.51/0.49 tff(func_def_349, type, g_s342_333: $int).
% 1.51/0.49 tff(func_def_350, type, g_s343_334: $int).
% 1.51/0.49 tff(func_def_351, type, g_s344_335: $int).
% 1.51/0.49 tff(func_def_352, type, g_s345_336: $int).
% 1.51/0.49 tff(func_def_353, type, g_s346_337: $int).
% 1.51/0.49 tff(func_def_354, type, g_s347_338: $int).
% 1.51/0.49 tff(func_def_355, type, g_s348_339: $int).
% 1.51/0.49 tff(func_def_356, type, g_s349_340: $int).
% 1.51/0.49 tff(func_def_357, type, g_s350_341: $int).
% 1.51/0.49 tff(func_def_358, type, g_s351_342: $int).
% 1.51/0.49 tff(func_def_359, type, g_s352_343: $int).
% 1.51/0.49 tff(func_def_360, type, g_s353_344: $int).
% 1.51/0.49 tff(func_def_361, type, g_s354_345: $int).
% 1.51/0.49 tff(func_def_362, type, g_s355_346: $int).
% 1.51/0.49 tff(func_def_363, type, g_s356_347: $int).
% 1.51/0.49 tff(func_def_364, type, g_s357_348: $int).
% 1.51/0.49 tff(func_def_365, type, g_s358_349: $int).
% 1.51/0.49 tff(func_def_366, type, g_s359_350: $int).
% 1.51/0.49 tff(func_def_367, type, g_s360_351: $int).
% 1.51/0.49 tff(func_def_368, type, g_s361_352: $int).
% 1.51/0.49 tff(func_def_369, type, g_s362_353: $int).
% 1.51/0.49 tff(func_def_370, type, g_s363_354: $int).
% 1.51/0.49 tff(func_def_371, type, g_s364_355: set_0).
% 1.51/0.49 tff(func_def_372, type, g_s365_356: set_0).
% 1.51/0.49 tff(func_def_373, type, g_s366_357: set_0).
% 1.51/0.49 tff(func_def_374, type, g_s367_358: set_0).
% 1.51/0.49 tff(func_def_375, type, g_s368_359: set_0).
% 1.51/0.49 tff(func_def_376, type, g_s369_360: set_0).
% 1.51/0.49 tff(func_def_377, type, g_s370_361: set_0).
% 1.51/0.49 tff(func_def_378, type, g_s371_362: set_0).
% 1.51/0.49 tff(func_def_379, type, g_s372_363: set_0).
% 1.51/0.49 tff(func_def_380, type, g_s373_364: set_0).
% 1.51/0.49 tff(func_def_381, type, g_s374_365: set_0).
% 1.51/0.49 tff(func_def_382, type, g_s375_366: set_0).
% 1.51/0.49 tff(func_def_383, type, g_s376_367: set_0).
% 1.51/0.49 tff(func_def_384, type, g_s377_368: set_0).
% 1.51/0.49 tff(func_def_385, type, g_s378_369: set_0).
% 1.51/0.49 tff(func_def_386, type, g_s379_370: set_0).
% 1.51/0.49 tff(func_def_387, type, g_s380_371: set_0).
% 1.51/0.49 tff(func_def_388, type, g_s381_372: set_0).
% 1.51/0.49 tff(func_def_389, type, g_s382_373: set_0).
% 1.51/0.49 tff(func_def_390, type, g_s383_374: set_0).
% 1.51/0.49 tff(func_def_391, type, g_s384_375: set_0).
% 1.51/0.49 tff(func_def_392, type, g_s385_376: set_0).
% 1.51/0.49 tff(func_def_393, type, g_s386_377: set_0).
% 1.51/0.49 tff(func_def_394, type, g_s387_378: set_0).
% 1.51/0.49 tff(func_def_395, type, g_s388_379: set_0).
% 1.51/0.49 tff(func_def_396, type, g_s389_380: set_0).
% 1.51/0.49 tff(func_def_397, type, g_s390_381: set_0).
% 1.51/0.49 tff(func_def_398, type, g_s391_382: $int).
% 1.51/0.49 tff(func_def_399, type, g_s392_383: $int).
% 1.51/0.49 tff(func_def_400, type, g_s393_384: set_0).
% 1.51/0.49 tff(func_def_401, type, g_s394_385: set_0).
% 1.51/0.49 tff(func_def_402, type, g_s395_386: $int).
% 1.51/0.49 tff(func_def_403, type, g_s396_387: set_0).
% 1.51/0.49 tff(func_def_404, type, g_s397_388: set_0).
% 1.51/0.49 tff(func_def_405, type, g_s398_389: set_0).
% 1.51/0.49 tff(func_def_406, type, g_s399_390: set_0).
% 1.51/0.49 tff(func_def_407, type, g_s400_391: $int).
% 1.51/0.49 tff(func_def_408, type, g_s401_392: set_0).
% 1.51/0.49 tff(func_def_409, type, g_s402_393: set_0).
% 1.51/0.49 tff(func_def_410, type, g_s403_394: set_0).
% 1.51/0.49 tff(func_def_411, type, g_s404_395: set_2).
% 1.51/0.49 tff(func_def_412, type, g_s405_396: set_2).
% 1.51/0.49 tff(func_def_413, type, g_s406_397: set_0).
% 1.51/0.49 tff(func_def_414, type, g_s407_398: $int).
% 1.51/0.49 tff(func_def_415, type, g_s408_399: $int).
% 1.51/0.49 tff(func_def_416, type, g_s409_400: $int).
% 1.51/0.49 tff(func_def_417, type, g_s410_401: $int).
% 1.51/0.49 tff(func_def_418, type, g_s411_402: $int).
% 1.51/0.49 tff(func_def_419, type, g_s412_403: $int).
% 1.51/0.49 tff(func_def_420, type, g_s413_404: $int).
% 1.51/0.49 tff(func_def_421, type, g_s414_405: $int).
% 1.51/0.49 tff(func_def_422, type, g_s415_406: $int).
% 1.51/0.49 tff(func_def_423, type, g_s416_407: $int).
% 1.51/0.49 tff(func_def_424, type, g_s417_408: $int).
% 1.51/0.49 tff(func_def_425, type, g_s418_409: $int).
% 1.51/0.49 tff(func_def_426, type, g_s419_410: $int).
% 1.51/0.49 tff(func_def_427, type, g_s420_411: $int).
% 1.51/0.49 tff(func_def_428, type, g_s421_412: $int).
% 1.51/0.49 tff(func_def_429, type, g_s422_413: $int).
% 1.51/0.49 tff(func_def_430, type, g_s423_414: $int).
% 1.51/0.49 tff(func_def_431, type, g_s424_415: $int).
% 1.51/0.49 tff(func_def_432, type, g_s425_416: $int).
% 1.51/0.49 tff(func_def_433, type, g_s426_417: $int).
% 1.51/0.49 tff(func_def_434, type, g_s427_418: $int).
% 1.51/0.49 tff(func_def_435, type, g_s428_419: $int).
% 1.51/0.49 tff(func_def_436, type, g_s429_420: $int).
% 1.51/0.49 tff(func_def_437, type, g_s430_421: $int).
% 1.51/0.49 tff(func_def_438, type, g_s431_422: $int).
% 1.51/0.49 tff(func_def_439, type, g_s432_423: $int).
% 1.51/0.49 tff(func_def_440, type, g_s433_424: $int).
% 1.51/0.49 tff(func_def_441, type, g_s434_425: $int).
% 1.51/0.49 tff(func_def_442, type, g_s435_426: $int).
% 1.51/0.49 tff(func_def_443, type, g_s436_427: $int).
% 1.51/0.49 tff(func_def_444, type, g_s437_428: $int).
% 1.51/0.49 tff(func_def_445, type, g_s438_429: $int).
% 1.51/0.49 tff(func_def_446, type, g_s439_430: $int).
% 1.51/0.49 tff(func_def_447, type, g_s440_431: $int).
% 1.51/0.49 tff(func_def_448, type, g_s441_432: $int).
% 1.51/0.49 tff(func_def_449, type, g_s442_433: $int).
% 1.51/0.49 tff(func_def_450, type, g_s443_434: $int).
% 1.51/0.49 tff(func_def_451, type, g_s444_435: $int).
% 1.51/0.49 tff(func_def_452, type, g_s445_436: set_0).
% 1.51/0.49 tff(func_def_453, type, g_s446_437: $int).
% 1.51/0.49 tff(func_def_454, type, g_s447_438: $int).
% 1.51/0.49 tff(func_def_455, type, g_s448_439: $int).
% 1.51/0.49 tff(func_def_456, type, g_s449_440: $int).
% 1.51/0.49 tff(func_def_457, type, g_s450_441: $int).
% 1.51/0.49 tff(func_def_458, type, g_s451_442: $int).
% 1.51/0.49 tff(func_def_459, type, g_s452_443: $int).
% 1.51/0.49 tff(func_def_460, type, g_s453_444: $int).
% 1.51/0.49 tff(func_def_461, type, g_s454_445: $int).
% 1.51/0.49 tff(func_def_462, type, g_s455_446: $int).
% 1.51/0.49 tff(func_def_463, type, g_s456_447: $int).
% 1.51/0.49 tff(func_def_464, type, g_s457_448: $int).
% 1.51/0.49 tff(func_def_465, type, g_s458_449: $int).
% 1.51/0.49 tff(func_def_466, type, g_s459_450: $int).
% 1.51/0.49 tff(func_def_467, type, g_s460_451: $int).
% 1.51/0.49 tff(func_def_468, type, g_s461_452: $int).
% 1.51/0.49 tff(func_def_469, type, g_s462_453: $int).
% 1.51/0.49 tff(func_def_470, type, g_s463_454: $int).
% 1.51/0.49 tff(func_def_471, type, g_s464_455: $int).
% 1.51/0.49 tff(func_def_472, type, g_s465_456: $int).
% 1.51/0.49 tff(func_def_473, type, g_s466_457: $int).
% 1.51/0.49 tff(func_def_474, type, g_s467_458: $int).
% 1.51/0.49 tff(func_def_475, type, g_s468_459: $int).
% 1.51/0.49 tff(func_def_476, type, g_s469_460: $int).
% 1.51/0.49 tff(func_def_477, type, g_s470_461: $int).
% 1.51/0.49 tff(func_def_478, type, g_s471_462: $int).
% 1.51/0.49 tff(func_def_479, type, g_s472_463: $int).
% 1.51/0.49 tff(func_def_480, type, g_s473_464: $int).
% 1.51/0.49 tff(func_def_481, type, g_s474_465: $int).
% 1.51/0.49 tff(func_def_482, type, g_s475_466: $int).
% 1.51/0.49 tff(func_def_483, type, g_s476_467: $int).
% 1.51/0.49 tff(func_def_484, type, g_s477_468: $int).
% 1.51/0.49 tff(func_def_485, type, g_s478_469: $int).
% 1.51/0.49 tff(func_def_486, type, g_s479_470: $int).
% 1.51/0.49 tff(func_def_487, type, g_s480_471: $int).
% 1.51/0.49 tff(func_def_488, type, g_s481_472: $int).
% 1.51/0.49 tff(func_def_489, type, g_s482_473: $int).
% 1.51/0.49 tff(func_def_490, type, g_s483_474: $int).
% 1.51/0.49 tff(func_def_491, type, g_s484_475: $int).
% 1.51/0.49 tff(func_def_492, type, g_s485_476: $int).
% 1.51/0.49 tff(func_def_493, type, g_s486_477: $int).
% 1.51/0.49 tff(func_def_494, type, g_s487_478: $int).
% 1.51/0.49 tff(func_def_495, type, g_s488_479: $int).
% 1.51/0.49 tff(func_def_496, type, g_s489_480: $int).
% 1.51/0.49 tff(func_def_497, type, g_s490_481: $int).
% 1.51/0.49 tff(func_def_498, type, g_s491_482: $int).
% 1.51/0.49 tff(func_def_499, type, g_s492_483: $int).
% 1.51/0.49 tff(func_def_500, type, g_s493_484: $int).
% 1.51/0.49 tff(func_def_501, type, g_s494_485: $int).
% 1.51/0.49 tff(func_def_502, type, g_s495_486: $int).
% 1.51/0.49 tff(func_def_503, type, g_s496_487: $int).
% 1.51/0.49 tff(func_def_504, type, g_s497_488: $int).
% 1.51/0.49 tff(func_def_505, type, g_s498_489: $int).
% 1.51/0.49 tff(func_def_506, type, g_s499_490: $int).
% 1.51/0.49 tff(func_def_507, type, g_s500_491: $int).
% 1.51/0.49 tff(func_def_508, type, g_s501_492: $int).
% 1.51/0.49 tff(func_def_509, type, g_s502_493: $int).
% 1.51/0.49 tff(func_def_510, type, g_s503_494: $int).
% 1.51/0.49 tff(func_def_511, type, g_s504_495: $int).
% 1.51/0.49 tff(func_def_512, type, g_s505_496: $int).
% 1.51/0.49 tff(func_def_513, type, g_s506_497: $int).
% 1.51/0.49 tff(func_def_514, type, g_s507_498: $int).
% 1.51/0.49 tff(func_def_515, type, g_s508_499: $int).
% 1.51/0.49 tff(func_def_516, type, g_s509_500: $int).
% 1.51/0.49 tff(func_def_517, type, g_s510_501: $int).
% 1.51/0.49 tff(func_def_518, type, g_s511_502: $int).
% 1.51/0.49 tff(func_def_519, type, g_s512_503: $int).
% 1.51/0.49 tff(func_def_520, type, g_s513_504: $int).
% 1.51/0.49 tff(func_def_521, type, g_s514_505: $int).
% 1.51/0.49 tff(func_def_522, type, g_s515_506: $int).
% 1.51/0.49 tff(func_def_523, type, g_s516_507: $int).
% 1.51/0.49 tff(func_def_524, type, g_s517_508: $int).
% 1.51/0.49 tff(func_def_525, type, g_s518_509: $int).
% 1.51/0.49 tff(func_def_526, type, g_s519_510: $int).
% 1.51/0.49 tff(func_def_527, type, g_s520_511: $int).
% 1.51/0.49 tff(func_def_528, type, g_s521_512: $int).
% 1.51/0.49 tff(func_def_529, type, g_s522_513: $int).
% 1.51/0.49 tff(func_def_530, type, g_s523_514: $int).
% 1.51/0.49 tff(func_def_531, type, g_s524_515: $int).
% 1.51/0.49 tff(func_def_532, type, g_s525_516: $int).
% 1.51/0.49 tff(func_def_533, type, g_s526_517: $int).
% 1.51/0.49 tff(func_def_534, type, g_s527_518: $int).
% 1.51/0.49 tff(func_def_535, type, g_s528_519: $int).
% 1.51/0.49 tff(func_def_536, type, g_s529_520: $int).
% 1.51/0.49 tff(func_def_537, type, g_s530_521: $int).
% 1.51/0.49 tff(func_def_538, type, g_s531_522: $int).
% 1.51/0.49 tff(func_def_539, type, g_s532_523: $int).
% 1.51/0.49 tff(func_def_540, type, g_s533_524: $int).
% 1.51/0.49 tff(func_def_541, type, g_s534_525: $int).
% 1.51/0.49 tff(func_def_542, type, g_s535_526: $int).
% 1.51/0.49 tff(func_def_543, type, g_s536_527: $int).
% 1.51/0.49 tff(func_def_544, type, g_s537_528: $int).
% 1.51/0.49 tff(func_def_545, type, g_s538_529: $int).
% 1.51/0.49 tff(func_def_546, type, g_s539_530: $int).
% 1.51/0.49 tff(func_def_547, type, g_s540_531: $int).
% 1.51/0.49 tff(func_def_548, type, g_s541_532: $int).
% 1.51/0.49 tff(func_def_549, type, g_s542_533: $int).
% 1.51/0.49 tff(func_def_550, type, g_s543_534: $int).
% 1.51/0.49 tff(func_def_551, type, g_s544_535: $int).
% 1.51/0.49 tff(func_def_552, type, g_s545_536: $int).
% 1.51/0.49 tff(func_def_553, type, g_s546_537: $int).
% 1.51/0.49 tff(func_def_554, type, g_s547_538: $int).
% 1.51/0.49 tff(func_def_555, type, g_s548_539: $int).
% 1.51/0.49 tff(func_def_556, type, g_s549_540: $int).
% 1.51/0.49 tff(func_def_557, type, g_s550_541: $int).
% 1.51/0.49 tff(func_def_558, type, g_s551_542: $int).
% 1.51/0.49 tff(func_def_559, type, g_s552_543: $int).
% 1.51/0.49 tff(func_def_560, type, g_s553_544: $int).
% 1.51/0.49 tff(func_def_561, type, g_s554_545: $int).
% 1.51/0.49 tff(func_def_562, type, g_s555_546: $int).
% 1.51/0.49 tff(func_def_563, type, g_s556_547: $int).
% 1.51/0.49 tff(func_def_564, type, g_s557_548: $int).
% 1.51/0.49 tff(func_def_565, type, g_s558_549: $int).
% 1.51/0.49 tff(func_def_566, type, g_s559_550: $int).
% 1.51/0.49 tff(func_def_567, type, g_s560_551: $int).
% 1.51/0.49 tff(func_def_568, type, g_s561_552: $int).
% 1.51/0.49 tff(func_def_569, type, g_s562_553: $int).
% 1.51/0.49 tff(func_def_570, type, g_s563_554: $int).
% 1.51/0.49 tff(func_def_571, type, g_s564_555: $int).
% 1.51/0.49 tff(func_def_572, type, g_s565_556: $int).
% 1.51/0.49 tff(func_def_573, type, g_s566_557: $int).
% 1.51/0.49 tff(func_def_574, type, g_s567_558: $int).
% 1.51/0.49 tff(func_def_575, type, g_s568_559: $int).
% 1.51/0.49 tff(func_def_576, type, g_s569_560: $int).
% 1.51/0.49 tff(func_def_577, type, g_s570_561: $int).
% 1.51/0.49 tff(func_def_578, type, g_s571_562: $int).
% 1.51/0.49 tff(func_def_579, type, g_s572_563: $int).
% 1.51/0.49 tff(func_def_580, type, g_s573_564: $int).
% 1.51/0.49 tff(func_def_581, type, g_s574_565: $int).
% 1.51/0.49 tff(func_def_582, type, g_s575_566: $int).
% 1.51/0.49 tff(func_def_583, type, g_s576_567: $int).
% 1.51/0.49 tff(func_def_584, type, g_s577_568: $int).
% 1.51/0.49 tff(func_def_585, type, g_s578_569: $int).
% 1.51/0.49 tff(func_def_586, type, g_s579_570: $int).
% 1.51/0.49 tff(func_def_587, type, g_s580_571: $int).
% 1.51/0.49 tff(func_def_588, type, g_s581_572: $int).
% 1.51/0.49 tff(func_def_589, type, g_s582_573: $int).
% 1.51/0.49 tff(func_def_590, type, g_s583_574: $int).
% 1.51/0.49 tff(func_def_591, type, g_s584_575: $int).
% 1.51/0.49 tff(func_def_592, type, g_s585_576: $int).
% 1.51/0.49 tff(func_def_593, type, g_s586_577: $int).
% 1.51/0.49 tff(func_def_594, type, g_s587_578: $int).
% 1.51/0.49 tff(func_def_595, type, g_s588_579: $int).
% 1.51/0.49 tff(func_def_596, type, g_s589_580: $int).
% 1.51/0.49 tff(func_def_597, type, g_s590_581: $int).
% 1.51/0.49 tff(func_def_598, type, g_s591_582: $int).
% 1.51/0.49 tff(func_def_599, type, g_s592_583: $int).
% 1.51/0.49 tff(func_def_600, type, g_s593_584: $int).
% 1.51/0.49 tff(func_def_601, type, g_s594_585: $int).
% 1.51/0.49 tff(func_def_602, type, g_s595_586: $int).
% 1.51/0.49 tff(func_def_603, type, g_s596_587: $int).
% 1.51/0.49 tff(func_def_604, type, g_s597_588: $int).
% 1.51/0.49 tff(func_def_605, type, g_s598_589: $int).
% 1.51/0.49 tff(func_def_606, type, g_s599_590: $int).
% 1.51/0.49 tff(func_def_607, type, g_s600_591: $int).
% 1.51/0.49 tff(func_def_608, type, g_s601_592: $int).
% 1.51/0.49 tff(func_def_609, type, g_s602_593: $int).
% 1.51/0.49 tff(func_def_610, type, g_s603_594: $int).
% 1.51/0.49 tff(func_def_611, type, g_s604_595: $int).
% 1.51/0.49 tff(func_def_612, type, g_s605_596: $int).
% 1.51/0.49 tff(func_def_613, type, g_s606_597: $int).
% 1.51/0.49 tff(func_def_614, type, g_s607_598: set_0).
% 1.51/0.49 tff(func_def_615, type, g_s608_599: set_0).
% 1.51/0.49 tff(func_def_616, type, g_s609_600: set_0).
% 1.51/0.49 tff(func_def_617, type, g_s610_601: set_0).
% 1.51/0.49 tff(func_def_618, type, g_s611_602: $int).
% 1.51/0.49 tff(func_def_619, type, g_s612_603: $int).
% 1.51/0.49 tff(func_def_620, type, g_s613_604: $int).
% 1.51/0.49 tff(func_def_621, type, g_s614_605: set_6).
% 1.51/0.49 tff(func_def_622, type, g_s615_606: set_0).
% 1.51/0.49 tff(func_def_623, type, g_s616_607: set_6).
% 1.51/0.49 tff(func_def_624, type, g_s617_608: set_0).
% 1.51/0.49 tff(func_def_625, type, g_s618_609: set_6).
% 1.51/0.49 tff(func_def_626, type, g_s619_610: set_0).
% 1.51/0.49 tff(func_def_627, type, g_s620_611: set_6).
% 1.51/0.49 tff(func_def_628, type, g_s621_612: set_6).
% 1.51/0.49 tff(func_def_629, type, g_s622_613: set_6).
% 1.51/0.49 tff(func_def_630, type, g_s623_614: set_6).
% 1.51/0.49 tff(func_def_631, type, g_s624_615: set_0).
% 1.51/0.49 tff(func_def_632, type, g_s625_616: set_6).
% 1.51/0.49 tff(func_def_633, type, g_s626_617: set_6).
% 1.51/0.49 tff(func_def_634, type, g_s627_618: set_6).
% 1.51/0.49 tff(func_def_635, type, g_s628_619: set_6).
% 1.51/0.49 tff(func_def_636, type, g_s629_620: set_6).
% 1.51/0.49 tff(func_def_637, type, g_s630_621: set_6).
% 1.51/0.49 tff(func_def_638, type, g_s631_622: set_6).
% 1.51/0.49 tff(func_def_639, type, g_s654_1_623: $int).
% 1.51/0.49 tff(func_def_640, type, g_s655_1_624: $int).
% 1.51/0.49 tff(func_def_641, type, g_s656_1_625: $int).
% 1.51/0.49 tff(func_def_642, type, g_s650_1_626: $int).
% 1.51/0.49 tff(func_def_643, type, g_s651_1_627: $int).
% 1.51/0.49 tff(func_def_644, type, g_s657_1_628: $int).
% 1.51/0.49 tff(func_def_645, type, g_s648_1_629: $int).
% 1.51/0.49 tff(func_def_646, type, g_s649_1_630: $int).
% 1.51/0.49 tff(func_def_647, type, g_s644_1_631: $int).
% 1.51/0.49 tff(func_def_648, type, g_s645_1_632: $int).
% 1.51/0.49 tff(func_def_649, type, g_s646_1_633: $int).
% 1.51/0.49 tff(func_def_650, type, g_s647_1_634: $int).
% 1.51/0.49 tff(func_def_651, type, g_s636_641: $int).
% 1.51/0.49 tff(func_def_652, type, g_s637_642: $int).
% 1.51/0.49 tff(func_def_653, type, g_s638_643: $int).
% 1.51/0.49 tff(func_def_654, type, g_s644_649: $int).
% 1.51/0.49 tff(func_def_655, type, g_s645_650: $int).
% 1.51/0.49 tff(func_def_656, type, g_s646_651: $int).
% 1.51/0.49 tff(func_def_657, type, g_s647_652: $int).
% 1.51/0.49 tff(func_def_658, type, g_s648_653: $int).
% 1.51/0.49 tff(func_def_659, type, g_s649_654: $int).
% 1.51/0.49 tff(func_def_660, type, g_s650_655: $int).
% 1.51/0.49 tff(func_def_661, type, g_s651_656: $int).
% 1.51/0.49 tff(func_def_662, type, g_s659_659: $int).
% 1.51/0.49 tff(func_def_663, type, g_s660_660: $int).
% 1.51/0.49 tff(func_def_664, type, g_s662_661: $int).
% 1.51/0.49 tff(func_def_665, type, g_s663_662: $int).
% 1.51/0.49 tff(func_def_666, type, g_s665_664: $int).
% 1.51/0.49 tff(func_def_667, type, g_s666_665: $int).
% 1.51/0.49 tff(func_def_668, type, g_s667_666: set_6).
% 1.51/0.49 tff(func_def_669, type, g_s649_2_667: $int).
% 1.51/0.49 tff(func_def_670, type, g_s668_668: $int).
% 1.51/0.49 tff(func_def_671, type, g_s669_669: $int).
% 1.51/0.49 tff(func_def_763, type, bG0: $o).
% 1.51/0.49 tff(func_def_766, type, bG1: $o).
% 1.51/0.49 tff(func_def_767, type, bG2: $o > $o).
% 1.51/0.49 tff(func_def_768, type, bG3: $o > $o).
% 1.51/0.49 tff(func_def_769, type, bG4: $o > $o).
% 1.51/0.49 tff(func_def_770, type, bG5: $o > $o).
% 1.51/0.49 tff(func_def_771, type, bG6: $o > $o).
% 1.51/0.49 tff(func_def_772, type, bG7: $o > $o).
% 1.51/0.49 tff(func_def_773, type, bG8: $o > $o).
% 1.51/0.49 tff(func_def_774, type, bG9: $o > $o).
% 1.51/0.49 tff(func_def_775, type, bG10: $o > $o).
% 1.51/0.49 tff(func_def_776, type, bG11: $o > $o).
% 1.51/0.49 tff(func_def_777, type, bG12: $o > $o).
% 1.51/0.49 tff(func_def_778, type, bG13: $o > $o).
% 1.51/0.49 tff(func_def_779, type, bG14: $o > $o).
% 1.51/0.49 tff(func_def_780, type, bG15: $o > $o).
% 1.51/0.49 tff(func_def_781, type, bG16: $o > $o).
% 1.51/0.49 tff(func_def_782, type, bG17: $o > $o).
% 1.51/0.49 tff(func_def_783, type, bG18: $o > $o).
% 1.51/0.49 tff(func_def_784, type, bG19: $o > $o).
% 1.51/0.49 tff(func_def_785, type, bG20: $o > $o).
% 1.51/0.49 tff(func_def_786, type, bG21: $o > $o).
% 1.51/0.49 tff(func_def_787, type, bG22: $o > $o).
% 1.51/0.49 tff(func_def_788, type, bG23: $o > $o).
% 1.51/0.49 tff(func_def_789, type, bG24: $o > $o).
% 1.51/0.49 tff(func_def_790, type, bG25: $o > $o).
% 1.51/0.49 tff(func_def_791, type, bG26: $o > $o).
% 1.51/0.49 tff(func_def_792, type, bG27: $o > $o).
% 1.51/0.49 tff(func_def_793, type, bG28: $o > $o).
% 1.51/0.49 tff(func_def_794, type, bG29: $o > $o).
% 1.51/0.49 tff(func_def_795, type, bG30: $o > $o).
% 1.51/0.49 tff(func_def_796, type, bG31: $o > $o).
% 1.51/0.49 tff(func_def_797, type, bG32: $o > $o).
% 1.51/0.49 tff(func_def_798, type, bG33: $o > $o).
% 1.51/0.49 tff(func_def_799, type, bG34: $o > $o).
% 1.51/0.49 tff(func_def_800, type, bG35: $o > $o).
% 1.51/0.49 tff(func_def_801, type, bG36: $o > $o).
% 1.51/0.49 tff(func_def_802, type, bG37: $o > $o).
% 1.51/0.49 tff(func_def_803, type, bG38: $o > $o).
% 1.51/0.49 tff(func_def_804, type, bG39: $o > $o).
% 1.51/0.49 tff(func_def_805, type, bG40: $o > $o).
% 1.51/0.49 tff(func_def_806, type, bG41: $o > $o).
% 1.51/0.49 tff(func_def_807, type, bG42: $o > $o).
% 1.51/0.49 tff(func_def_808, type, bG43: $o > $o).
% 1.51/0.49 tff(func_def_809, type, bG44: $o > $o).
% 1.51/0.49 tff(func_def_810, type, bG45: $o > $o).
% 1.51/0.49 tff(func_def_811, type, bG46: $o > $o).
% 1.51/0.49 tff(func_def_812, type, bG47: $o > $o).
% 1.51/0.49 tff(func_def_813, type, bG48: $o > $o).
% 1.51/0.49 tff(func_def_814, type, bG49: $o > $o).
% 1.51/0.49 tff(func_def_815, type, bG50: $o > $o).
% 1.51/0.49 tff(func_def_816, type, bG51: $o > $o).
% 1.51/0.49 tff(func_def_817, type, bG52: $o > $o).
% 1.51/0.49 tff(func_def_818, type, bG53: $o > $o).
% 1.51/0.49 tff(func_def_819, type, bG54: $o > $o).
% 1.51/0.49 tff(func_def_820, type, bG55: $o > $o).
% 1.51/0.49 tff(func_def_821, type, bG56: $o > $o).
% 1.51/0.49 tff(func_def_822, type, bG57: $o > $o).
% 1.51/0.49 tff(func_def_823, type, bG58: $o > $o).
% 1.51/0.49 tff(func_def_824, type, bG59: $o > $o).
% 1.51/0.49 tff(func_def_825, type, bG60: $o > $o).
% 1.51/0.49 tff(func_def_826, type, bG61: $o > $o).
% 1.51/0.49 tff(func_def_827, type, bG62: $o > $o).
% 1.51/0.49 tff(func_def_828, type, bG63: $o > $o).
% 1.51/0.49 tff(func_def_829, type, bG64: $o > $o).
% 1.51/0.49 tff(func_def_830, type, bG65: $o > $o).
% 1.51/0.49 tff(func_def_831, type, bG66: $o > $o).
% 1.51/0.49 tff(func_def_832, type, bG67: $o > $o).
% 1.51/0.49 tff(func_def_833, type, bG68: $o > $o).
% 1.51/0.49 tff(func_def_834, type, bG69: $o > $o).
% 1.51/0.49 tff(func_def_835, type, bG70: $o > $o).
% 1.51/0.49 tff(func_def_836, type, bG71: $o > $o).
% 1.51/0.49 tff(func_def_837, type, bG72: $o > $o).
% 1.51/0.49 tff(func_def_838, type, bG73: $o > $o).
% 1.51/0.49 tff(func_def_839, type, bG74: $o > $o).
% 1.51/0.49 tff(func_def_840, type, bG75: $o > $o).
% 1.51/0.49 tff(func_def_841, type, bG76: $o > $o).
% 1.51/0.49 tff(func_def_842, type, bG77: $o > $o).
% 1.51/0.49 tff(func_def_843, type, bG78: $o > $o).
% 1.51/0.49 tff(func_def_844, type, bG79: $o > $o).
% 1.51/0.49 tff(func_def_845, type, bG80: $o > $o).
% 1.51/0.49 tff(func_def_846, type, bG81: $o > $o).
% 1.51/0.49 tff(func_def_847, type, bG82: $o > $o).
% 1.51/0.49 tff(func_def_848, type, bG83: $o > $o).
% 1.51/0.49 tff(func_def_849, type, bG84: $o > $o).
% 1.51/0.49 tff(func_def_850, type, bG85: $o > $o).
% 1.51/0.49 tff(func_def_851, type, bG86: $o > $o).
% 1.51/0.49 tff(func_def_852, type, bG87: $o > $o).
% 1.51/0.49 tff(func_def_853, type, bG88: $o > $o).
% 1.51/0.49 tff(func_def_854, type, bG89: $o > $o).
% 1.51/0.49 tff(func_def_855, type, bG90: $o > $o).
% 1.51/0.49 tff(func_def_856, type, bG91: $o > $o).
% 1.51/0.49 tff(func_def_857, type, bG92: $o > $o).
% 1.51/0.49 tff(func_def_858, type, bG93: $o > $o).
% 1.51/0.49 tff(func_def_859, type, bG94: $o > $o).
% 1.51/0.49 tff(func_def_860, type, bG95: $o > $o).
% 1.51/0.49 tff(func_def_861, type, bG96: $o > $o).
% 1.51/0.49 tff(func_def_862, type, bG97: $o > $o).
% 1.51/0.49 tff(func_def_863, type, bG98: $o > $o).
% 1.51/0.49 tff(func_def_864, type, bG99: $o > $o).
% 1.51/0.49 tff(func_def_865, type, bG100: $o > $o).
% 1.51/0.49 tff(func_def_866, type, bG101: $o > $o).
% 1.51/0.49 tff(func_def_867, type, bG102: $o > $o).
% 1.51/0.49 tff(func_def_868, type, bG103: $o > $o).
% 1.51/0.49 tff(func_def_869, type, bG104: $o > $o).
% 1.51/0.49 tff(func_def_870, type, bG105: $o > $o).
% 1.51/0.49 tff(func_def_871, type, bG106: $o > $o).
% 1.51/0.49 tff(func_def_872, type, bG107: $o > $o).
% 1.51/0.49 tff(func_def_873, type, bG108: $o > $o).
% 1.51/0.49 tff(func_def_874, type, bG109: $o > $o).
% 1.51/0.49 tff(func_def_875, type, bG110: $o > $o).
% 1.51/0.49 tff(func_def_876, type, bG111: $o > $o).
% 1.51/0.49 tff(func_def_877, type, bG112: $o > $o).
% 1.51/0.49 tff(func_def_878, type, bG113: $o > $o).
% 1.51/0.49 tff(func_def_879, type, bG114: $o > $o).
% 1.51/0.49 tff(func_def_880, type, bG115: $o > $o).
% 1.51/0.49 tff(func_def_881, type, bG116: $o > $o).
% 1.51/0.49 tff(func_def_882, type, bG117: $o > $o).
% 1.51/0.49 tff(func_def_883, type, bG118: $o > $o).
% 1.51/0.49 tff(func_def_884, type, bG119: $o > $o).
% 1.51/0.49 tff(func_def_885, type, bG120: $o > $o).
% 1.51/0.49 tff(func_def_886, type, bG121: $o > $o).
% 1.51/0.49 tff(func_def_887, type, bG122: $o > $o).
% 1.51/0.49 tff(func_def_888, type, bG123: $o > $o).
% 1.51/0.49 tff(func_def_889, type, bG124: $o > $o).
% 1.51/0.49 tff(func_def_890, type, bG125: $o > $o).
% 1.51/0.49 tff(func_def_891, type, bG126: $o > $o).
% 1.51/0.49 tff(func_def_892, type, bG127: $o > $o).
% 1.51/0.49 tff(func_def_893, type, bG128: $o > $o).
% 1.51/0.49 tff(func_def_894, type, bG129: $o > $o).
% 1.51/0.49 tff(func_def_895, type, bG130: $o > $o).
% 1.51/0.49 tff(func_def_896, type, bG131: $o > $o).
% 1.51/0.49 tff(func_def_897, type, bG132: $o > $o).
% 1.51/0.49 tff(func_def_898, type, bG133: $o > $o).
% 1.51/0.49 tff(func_def_899, type, bG134: $o > $o).
% 1.51/0.49 tff(func_def_900, type, bG135: $o > $o).
% 1.51/0.49 tff(func_def_901, type, bG136: $o > $o).
% 1.51/0.49 tff(func_def_902, type, bG137: $o > $o).
% 1.51/0.49 tff(func_def_903, type, bG138: $o > $o).
% 1.51/0.49 tff(func_def_904, type, bG139: $o > $o).
% 1.51/0.49 tff(func_def_905, type, bG140: $o > $o).
% 1.51/0.49 tff(func_def_906, type, bG141: $o > $o).
% 1.51/0.49 tff(func_def_907, type, bG142: $o > $o).
% 1.51/0.49 tff(func_def_908, type, bG143: $o > $o).
% 1.51/0.49 tff(func_def_909, type, bG144: $o > $o).
% 1.51/0.49 tff(func_def_910, type, bG145: $o > $o).
% 1.51/0.49 tff(func_def_911, type, bG146: $o > $o).
% 1.51/0.49 tff(func_def_912, type, bG147: $o > $o).
% 1.51/0.49 tff(func_def_913, type, bG148: $o > $o).
% 1.51/0.49 tff(func_def_914, type, bG149: $o > $o).
% 1.51/0.49 tff(func_def_915, type, bG150: $o > $o).
% 1.51/0.49 tff(func_def_916, type, bG151: $o > $o).
% 1.51/0.49 tff(func_def_917, type, bG152: $o > $o).
% 1.51/0.49 tff(func_def_918, type, bG153: $o > $o).
% 1.51/0.49 tff(func_def_919, type, bG154: $o > $o).
% 1.51/0.49 tff(func_def_920, type, bG155: $o > $o).
% 1.51/0.49 tff(func_def_921, type, bG156: $o > $o).
% 1.51/0.49 tff(func_def_922, type, bG157: $o > $o).
% 1.51/0.49 tff(func_def_923, type, bG158: $o > $o).
% 1.51/0.49 tff(func_def_924, type, bG159: $o > $o).
% 1.51/0.49 tff(func_def_925, type, bG160: $o > $o).
% 1.51/0.49 tff(func_def_926, type, bG161: $o > $o).
% 1.51/0.49 tff(func_def_927, type, bG162: $o > $o).
% 1.51/0.49 tff(func_def_928, type, bG163: $o > $o).
% 1.51/0.49 tff(func_def_929, type, bG164: $o > $o).
% 1.51/0.49 tff(func_def_930, type, bG165: $o > $o).
% 1.51/0.49 tff(func_def_931, type, bG166: $o).
% 1.51/0.49 tff(func_def_932, type, bG167: $o).
% 1.51/0.49 tff(func_def_933, type, bG168: $o > $o).
% 1.51/0.49 tff(func_def_934, type, bG169: $o > $o).
% 1.51/0.49 tff(func_def_935, type, bG170: $o > $o).
% 1.51/0.49 tff(func_def_936, type, bG171: $o > $o).
% 1.51/0.49 tff(func_def_937, type, bG172: $o > $o).
% 1.51/0.49 tff(func_def_938, type, bG173: $o > $o).
% 1.51/0.49 tff(func_def_939, type, bG174: $o > $o).
% 1.51/0.49 tff(func_def_940, type, bG175: $o > $o).
% 1.51/0.49 tff(func_def_941, type, bG176: $o > $o).
% 1.51/0.49 tff(func_def_942, type, bG177: $o > $o).
% 1.51/0.49 tff(func_def_943, type, bG178: $o > $o).
% 1.51/0.49 tff(func_def_944, type, bG179: $o > $o).
% 1.51/0.49 tff(func_def_945, type, bG180: $o > $o).
% 1.51/0.49 tff(func_def_946, type, bG181: $o > $o).
% 1.51/0.49 tff(func_def_947, type, bG182: $o > $o).
% 1.51/0.49 tff(func_def_948, type, bG183: $o > $o).
% 1.51/0.49 tff(func_def_949, type, bG184: $o > $o).
% 1.51/0.49 tff(func_def_950, type, bG185: $o > $o).
% 1.51/0.49 tff(func_def_951, type, bG186: $o > $o).
% 1.51/0.49 tff(func_def_952, type, bG187: $o > $o).
% 1.51/0.49 tff(func_def_953, type, bG188: $o > $o).
% 1.51/0.49 tff(func_def_954, type, bG189: $o > $o).
% 1.51/0.49 tff(func_def_955, type, bG190: $o > $o).
% 1.51/0.49 tff(func_def_956, type, bG191: $o > $o).
% 1.51/0.49 tff(func_def_957, type, bG192: $o > $o).
% 1.51/0.49 tff(func_def_958, type, bG193: $o > $o).
% 1.51/0.49 tff(func_def_959, type, bG194: $o > $o).
% 1.51/0.49 tff(func_def_960, type, bG195: $o > $o).
% 1.51/0.49 tff(func_def_961, type, bG196: $o > $o).
% 1.51/0.49 tff(func_def_962, type, bG197: $o > $o).
% 1.51/0.49 tff(func_def_963, type, bG198: $o > $o).
% 1.51/0.49 tff(func_def_964, type, bG199: $o > $o).
% 1.51/0.49 tff(func_def_965, type, bG200: $o > $o).
% 1.51/0.49 tff(func_def_966, type, bG201: $o > $o).
% 1.51/0.49 tff(func_def_967, type, bG202: $o > $o).
% 1.51/0.49 tff(func_def_968, type, bG203: $o > $o).
% 1.51/0.49 tff(func_def_969, type, bG204: $o > $o).
% 1.51/0.49 tff(func_def_970, type, bG205: $o > $o).
% 1.51/0.49 tff(func_def_971, type, bG206: $o > $o).
% 1.51/0.49 tff(func_def_972, type, bG207: $o > $o).
% 1.51/0.49 tff(func_def_973, type, bG208: $o > $o).
% 1.51/0.49 tff(func_def_974, type, bG209: $o > $o).
% 1.51/0.49 tff(func_def_975, type, bG210: $o > $o).
% 1.51/0.49 tff(func_def_976, type, bG211: $o > $o).
% 1.51/0.49 tff(func_def_977, type, bG212: $o > $o).
% 1.51/0.49 tff(func_def_978, type, bG213: $o > $o).
% 1.51/0.49 tff(func_def_979, type, bG214: $o > $o).
% 1.51/0.49 tff(func_def_980, type, bG215: $o > $o).
% 1.51/0.49 tff(func_def_981, type, bG216: $o > $o).
% 1.51/0.49 tff(func_def_982, type, bG217: $o > $o).
% 1.51/0.49 tff(func_def_983, type, bG218: $o > $o).
% 1.51/0.49 tff(func_def_984, type, bG219: $o > $o).
% 1.51/0.49 tff(func_def_985, type, bG220: $o > $o).
% 1.51/0.49 tff(func_def_986, type, bG221: $o > $o).
% 1.51/0.49 tff(func_def_987, type, bG222: $o > $o).
% 1.51/0.49 tff(func_def_988, type, bG223: $o > $o).
% 1.51/0.49 tff(func_def_989, type, bG224: $o > $o).
% 1.51/0.49 tff(func_def_990, type, bG225: $o > $o).
% 1.51/0.49 tff(func_def_991, type, bG226: $o > $o).
% 1.51/0.49 tff(func_def_992, type, bG227: $o > $o).
% 1.51/0.49 tff(func_def_993, type, bG228: $o > $o).
% 1.51/0.49 tff(func_def_994, type, bG229: $o > $o).
% 1.51/0.49 tff(func_def_995, type, bG230: $o > $o).
% 1.51/0.49 tff(func_def_996, type, bG231: $o > $o).
% 1.51/0.49 tff(func_def_997, type, bG232: $o > $o).
% 1.51/0.49 tff(func_def_998, type, bG233: $o > $o).
% 1.51/0.49 tff(func_def_999, type, bG234: $o > $o).
% 1.51/0.49 tff(func_def_1000, type, bG235: $o > $o).
% 1.51/0.49 tff(func_def_1001, type, bG236: $o > $o).
% 1.51/0.49 tff(func_def_1002, type, bG237: $o > $o).
% 1.51/0.49 tff(func_def_1003, type, bG238: $o > $o).
% 1.51/0.49 tff(func_def_1004, type, bG239: $o > $o).
% 1.51/0.49 tff(func_def_1005, type, bG240: $o > $o).
% 1.51/0.49 tff(func_def_1006, type, bG241: $o > $o).
% 1.51/0.49 tff(func_def_1007, type, bG242: $o > $o).
% 1.51/0.49 tff(func_def_1008, type, bG243: $o > $o).
% 1.51/0.49 tff(func_def_1009, type, bG244: $o > $o).
% 1.51/0.49 tff(func_def_1010, type, bG245: $o > $o).
% 1.51/0.49 tff(func_def_1011, type, bG246: $o > $o).
% 1.51/0.49 tff(func_def_1012, type, bG247: $o > $o).
% 1.51/0.49 tff(func_def_1013, type, bG248: $o > $o).
% 1.51/0.49 tff(func_def_1014, type, bG249: $o > $o).
% 1.51/0.49 tff(func_def_1015, type, bG250: $o > $o).
% 1.51/0.49 tff(func_def_1016, type, bG251: $o > $o).
% 1.51/0.49 tff(func_def_1017, type, bG252: $o > $o).
% 1.51/0.49 tff(func_def_1018, type, bG253: $o > $o).
% 1.51/0.49 tff(func_def_1019, type, bG254: $o > $o).
% 1.51/0.49 tff(func_def_1020, type, bG255: $o > $o).
% 1.51/0.49 tff(func_def_1021, type, bG256: $o > $o).
% 1.51/0.49 tff(func_def_1022, type, bG257: $o > $o).
% 1.51/0.49 tff(func_def_1023, type, bG258: $o > $o).
% 1.51/0.49 tff(func_def_1024, type, bG259: $o > $o).
% 1.51/0.49 tff(func_def_1025, type, bG260: $o > $o).
% 1.51/0.49 tff(func_def_1026, type, bG261: $o > $o).
% 1.51/0.49 tff(func_def_1027, type, bG262: $o > $o).
% 1.51/0.49 tff(func_def_1028, type, bG263: $o > $o).
% 1.51/0.49 tff(func_def_1029, type, bG264: $o > $o).
% 1.51/0.49 tff(func_def_1030, type, bG265: $o > $o).
% 1.51/0.49 tff(func_def_1031, type, bG266: $o > $o).
% 1.51/0.49 tff(func_def_1032, type, bG267: $o > $o).
% 1.51/0.49 tff(func_def_1033, type, bG268: $o > $o).
% 1.51/0.49 tff(func_def_1034, type, bG269: $o > $o).
% 1.51/0.49 tff(func_def_1035, type, bG270: $o > $o).
% 1.51/0.49 tff(func_def_1036, type, bG271: $o > $o).
% 1.51/0.49 tff(func_def_1037, type, bG272: $o > $o).
% 1.51/0.49 tff(func_def_1038, type, bG273: $o > $o).
% 1.51/0.49 tff(func_def_1039, type, bG274: $o > $o).
% 1.51/0.49 tff(func_def_1040, type, bG275: $o > $o).
% 1.51/0.49 tff(func_def_1041, type, bG276: $o > $o).
% 1.51/0.49 tff(func_def_1042, type, bG277: $o > $o).
% 1.51/0.49 tff(func_def_1043, type, bG278: $o > $o).
% 1.51/0.49 tff(func_def_1044, type, bG279: $o > $o).
% 1.51/0.49 tff(func_def_1045, type, bG280: $o > $o).
% 1.51/0.49 tff(func_def_1046, type, bG281: $o > $o).
% 1.51/0.49 tff(func_def_1047, type, bG282: $o > $o).
% 1.51/0.49 tff(func_def_1048, type, bG283: $o > $o).
% 1.51/0.49 tff(func_def_1049, type, bG284: $o > $o).
% 1.51/0.49 tff(func_def_1050, type, bG285: $o > $o).
% 1.51/0.49 tff(func_def_1051, type, bG286: $o > $o).
% 1.51/0.49 tff(func_def_1052, type, bG287: $o > $o).
% 1.51/0.49 tff(func_def_1053, type, bG288: $o > $o).
% 1.51/0.49 tff(func_def_1054, type, bG289: $o > $o).
% 1.51/0.49 tff(func_def_1055, type, bG290: $o > $o).
% 1.51/0.49 tff(func_def_1056, type, bG291: $o > $o).
% 1.51/0.49 tff(func_def_1057, type, bG292: $o > $o).
% 1.51/0.49 tff(func_def_1058, type, bG293: $o > $o).
% 1.51/0.49 tff(func_def_1059, type, bG294: $o > $o).
% 1.51/0.49 tff(func_def_1060, type, bG295: $o > $o).
% 1.51/0.49 tff(func_def_1061, type, bG296: $o > $o).
% 1.51/0.49 tff(func_def_1062, type, bG297: $o > $o).
% 1.51/0.49 tff(func_def_1063, type, bG298: $o > $o).
% 1.51/0.49 tff(func_def_1064, type, bG299: $o > $o).
% 1.51/0.49 tff(func_def_1065, type, bG300: $o > $o).
% 1.51/0.49 tff(func_def_1066, type, bG301: $o > $o).
% 1.51/0.49 tff(func_def_1067, type, bG302: $o > $o).
% 1.51/0.49 tff(func_def_1068, type, bG303: $o > $o).
% 1.51/0.49 tff(func_def_1069, type, bG304: $o > $o).
% 1.51/0.49 tff(func_def_1070, type, bG305: $o > $o).
% 1.51/0.49 tff(func_def_1071, type, bG306: $o > $o).
% 1.51/0.49 tff(func_def_1072, type, bG307: $o > $o).
% 1.51/0.49 tff(func_def_1073, type, bG308: $o > $o).
% 1.51/0.49 tff(func_def_1074, type, bG309: $o > $o).
% 1.51/0.49 tff(func_def_1075, type, bG310: $o > $o).
% 1.51/0.49 tff(func_def_1076, type, bG311: $o > $o).
% 1.51/0.49 tff(func_def_1077, type, bG312: $o > $o).
% 1.51/0.49 tff(func_def_1078, type, bG313: $o > $o).
% 1.51/0.49 tff(func_def_1079, type, bG314: $o > $o).
% 1.51/0.49 tff(func_def_1080, type, bG315: $o > $o).
% 1.51/0.49 tff(func_def_1081, type, bG316: $o > $o).
% 1.51/0.49 tff(func_def_1082, type, bG317: $o > $o).
% 1.51/0.49 tff(func_def_1083, type, bG318: $o > $o).
% 1.51/0.49 tff(func_def_1084, type, bG319: $o > $o).
% 1.51/0.49 tff(func_def_1085, type, bG320: $o > $o).
% 1.51/0.49 tff(func_def_1086, type, bG321: $o > $o).
% 1.51/0.49 tff(func_def_1087, type, bG322: $o > $o).
% 1.51/0.49 tff(func_def_1088, type, bG323: $o > $o).
% 1.51/0.49 tff(func_def_1089, type, bG324: $o > $o).
% 1.51/0.49 tff(func_def_1090, type, bG325: $o > $o).
% 1.51/0.49 tff(func_def_1091, type, bG326: $o > $o).
% 1.51/0.49 tff(func_def_1092, type, bG327: $o > $o).
% 1.51/0.49 tff(func_def_1093, type, bG328: $o > $o).
% 1.51/0.49 tff(func_def_1094, type, bG329: $o > $o).
% 1.51/0.49 tff(func_def_1095, type, bG330: $o > $o).
% 1.51/0.49 tff(func_def_1096, type, bG331: $o > $o).
% 1.51/0.49 tff(func_def_1097, type, bG332: $o > $o).
% 1.51/0.49 tff(func_def_1098, type, bG333: $o > $o).
% 1.51/0.49 tff(func_def_1099, type, bG334: $o > $o).
% 1.51/0.49 tff(func_def_1100, type, bG335: $o > $o).
% 1.51/0.49 tff(func_def_1101, type, bG336: $o > $o).
% 1.51/0.49 tff(func_def_1102, type, bG337: $o > $o).
% 1.51/0.49 tff(func_def_1103, type, bG338: $o > $o).
% 1.51/0.49 tff(func_def_1104, type, bG339: $o > $o).
% 1.51/0.49 tff(func_def_1105, type, bG340: $o > $o).
% 1.51/0.49 tff(func_def_1106, type, bG341: $o > $o).
% 1.51/0.49 tff(func_def_1107, type, bG342: $o > $o).
% 1.51/0.49 tff(func_def_1108, type, bG343: $o > $o).
% 1.51/0.49 tff(func_def_1109, type, bG344: $o > $o).
% 1.51/0.49 tff(func_def_1110, type, bG345: $o > $o).
% 1.51/0.49 tff(func_def_1111, type, bG346: $o > $o).
% 1.51/0.49 tff(func_def_1112, type, bG347: $o > $o).
% 1.51/0.49 tff(func_def_1113, type, bG348: $o > $o).
% 1.51/0.49 tff(func_def_1114, type, bG349: $o > $o).
% 1.51/0.49 tff(func_def_1115, type, bG350: $o > $o).
% 1.51/0.49 tff(func_def_1116, type, bG351: $o > $o).
% 1.51/0.49 tff(func_def_1117, type, bG352: $o > $o).
% 1.51/0.49 tff(func_def_1118, type, bG353: $o > $o).
% 1.51/0.49 tff(func_def_1119, type, bG354: $o > $o).
% 1.51/0.49 tff(func_def_1120, type, bG355: $o > $o).
% 1.51/0.49 tff(func_def_1121, type, bG356: $o > $o).
% 1.51/0.49 tff(func_def_1122, type, bG357: $o > $o).
% 1.51/0.49 tff(func_def_1123, type, bG358: $o > $o).
% 1.51/0.49 tff(func_def_1124, type, bG359: $o > $o).
% 1.51/0.49 tff(func_def_1125, type, bG360: $o > $o).
% 1.51/0.49 tff(func_def_1126, type, bG361: $o > $o).
% 1.51/0.49 tff(func_def_1127, type, bG362: $o > $o).
% 1.51/0.49 tff(func_def_1128, type, bG363: $o > $o).
% 1.51/0.49 tff(func_def_1129, type, bG364: $o > $o).
% 1.51/0.49 tff(func_def_1130, type, bG365: $o > $o).
% 1.51/0.49 tff(func_def_1131, type, bG366: $o > $o).
% 1.51/0.49 tff(func_def_1132, type, bG367: $o > $o).
% 1.51/0.49 tff(func_def_1133, type, bG368: $o > $o).
% 1.51/0.49 tff(func_def_1134, type, bG369: $o > $o).
% 1.51/0.49 tff(func_def_1135, type, bG370: $o > $o).
% 1.51/0.49 tff(func_def_1136, type, bG371: $o > $o).
% 1.51/0.49 tff(func_def_1137, type, bG372: $o > $o).
% 1.51/0.49 tff(func_def_1138, type, bG373: $o > $o).
% 1.51/0.49 tff(func_def_1139, type, bG374: $o > $o).
% 1.51/0.49 tff(func_def_1140, type, bG375: $o > $o).
% 1.51/0.49 tff(func_def_1141, type, bG376: $o > $o).
% 1.51/0.49 tff(func_def_1142, type, bG377: $o > $o).
% 1.51/0.49 tff(func_def_1143, type, bG378: $o > $o).
% 1.51/0.49 tff(func_def_1144, type, bG379: $o > $o).
% 1.51/0.49 tff(func_def_1145, type, bG380: $o > $o).
% 1.51/0.49 tff(func_def_1146, type, bG381: $o > $o).
% 1.51/0.49 tff(func_def_1147, type, bG382: $o > $o).
% 1.51/0.49 tff(func_def_1148, type, bG383: $o > $o).
% 1.51/0.49 tff(func_def_1149, type, bG384: $o > $o).
% 1.51/0.49 tff(func_def_1150, type, bG385: $o > $o).
% 1.51/0.49 tff(func_def_1151, type, bG386: $o > $o).
% 1.51/0.49 tff(func_def_1152, type, bG387: $o > $o).
% 1.51/0.49 tff(func_def_1153, type, bG388: $o > $o).
% 1.51/0.49 tff(func_def_1154, type, bG389: $o > $o).
% 1.51/0.49 tff(func_def_1155, type, bG390: $o > $o).
% 1.51/0.49 tff(func_def_1156, type, bG391: $o > $o).
% 1.51/0.49 tff(func_def_1157, type, bG392: $o > $o).
% 1.51/0.49 tff(func_def_1158, type, bG393: $o > $o).
% 1.51/0.49 tff(func_def_1159, type, bG394: $o > $o).
% 1.51/0.49 tff(func_def_1160, type, bG395: $o > $o).
% 1.51/0.49 tff(func_def_1161, type, bG396: $o > $o).
% 1.51/0.49 tff(func_def_1162, type, bG397: $o > $o).
% 1.51/0.49 tff(func_def_1163, type, bG398: $o > $o).
% 1.51/0.49 tff(func_def_1164, type, bG399: $o > $o).
% 1.51/0.49 tff(func_def_1165, type, bG400: $o > $o).
% 1.51/0.49 tff(func_def_1166, type, bG401: $o > $o).
% 1.51/0.49 tff(func_def_1167, type, bG402: $o > $o).
% 1.51/0.49 tff(func_def_1168, type, bG403: $o).
% 1.51/0.49 tff(func_def_1169, type, bG404: $o).
% 1.51/0.49 tff(func_def_1170, type, bG405: $o).
% 1.51/0.49 tff(func_def_1171, type, bG406: $o).
% 1.51/0.49 tff(func_def_1172, type, bG407: $o).
% 1.51/0.49 tff(func_def_1173, type, bG408: $o).
% 1.51/0.49 tff(func_def_1174, type, bG409: $o).
% 1.51/0.49 tff(func_def_1175, type, bG410: $o).
% 1.51/0.49 tff(func_def_1176, type, bG411: $o).
% 1.51/0.49 tff(func_def_1177, type, bG412: $o).
% 1.51/0.49 tff(func_def_1178, type, bG413: $o).
% 1.51/0.49 tff(func_def_1179, type, sK414: set_5).
% 1.51/0.49 tff(func_def_1180, type, sK415: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1181, type, sK416: set_5).
% 1.51/0.49 tff(func_def_1182, type, sK417: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1183, type, sK418: set_5).
% 1.51/0.49 tff(func_def_1184, type, sK419: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1185, type, sK420: set_5).
% 1.51/0.49 tff(func_def_1186, type, sK421: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1187, type, sK422: set_5).
% 1.51/0.49 tff(func_def_1188, type, sK423: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1189, type, sK424: set_5).
% 1.51/0.49 tff(func_def_1190, type, sK425: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1191, type, sK426: set_5).
% 1.51/0.49 tff(func_def_1192, type, sK427: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1193, type, sK428: set_5).
% 1.51/0.49 tff(func_def_1194, type, sK429: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1195, type, sK430: set_5).
% 1.51/0.49 tff(func_def_1196, type, sK431: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1197, type, sK432: set_5).
% 1.51/0.49 tff(func_def_1198, type, sK433: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1199, type, sK434: set_3).
% 1.51/0.49 tff(func_def_1200, type, sK435: $o > $o).
% 1.51/0.49 tff(func_def_1201, type, sK436: set_3).
% 1.51/0.49 tff(func_def_1202, type, sK437: $o > $o).
% 1.51/0.49 tff(func_def_1203, type, sK438: set_3).
% 1.51/0.49 tff(func_def_1204, type, sK439: $o > $o).
% 1.51/0.49 tff(func_def_1205, type, sK440: set_3).
% 1.51/0.49 tff(func_def_1206, type, sK441: $o > $o).
% 1.51/0.49 tff(func_def_1207, type, sK442: set_3).
% 1.51/0.49 tff(func_def_1208, type, sK443: $o > $o).
% 1.51/0.49 tff(func_def_1209, type, sK444: set_5).
% 1.51/0.49 tff(func_def_1210, type, sK445: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1211, type, sK446: set_5).
% 1.51/0.49 tff(func_def_1212, type, sK447: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1213, type, sK448: set_6).
% 1.51/0.49 tff(func_def_1214, type, sK449: $int > $int).
% 1.51/0.49 tff(func_def_1215, type, sK450: $int > $int).
% 1.51/0.49 tff(func_def_1216, type, sK451: set_6).
% 1.51/0.49 tff(func_def_1217, type, sK452: $int > $int).
% 1.51/0.49 tff(func_def_1218, type, sK453: $int > $int).
% 1.51/0.49 tff(func_def_1219, type, sK454: $int).
% 1.51/0.49 tff(func_def_1220, type, sK455: $int).
% 1.51/0.49 tff(func_def_1221, type, sK456: $int).
% 1.51/0.49 tff(func_def_1222, type, sK457: set_3).
% 1.51/0.49 tff(func_def_1223, type, sK458: $o > $o).
% 1.51/0.49 tff(func_def_1224, type, sK459: set_3).
% 1.51/0.49 tff(func_def_1225, type, sK460: $o > $o).
% 1.51/0.49 tff(func_def_1226, type, sK461: set_6).
% 1.51/0.49 tff(func_def_1227, type, sK462: $int > $int).
% 1.51/0.49 tff(func_def_1228, type, sK463: set_6).
% 1.51/0.49 tff(func_def_1229, type, sK464: $int > $int).
% 1.51/0.49 tff(func_def_1230, type, sK465: set_6).
% 1.51/0.49 tff(func_def_1231, type, sK466: $int > $int).
% 1.51/0.49 tff(func_def_1232, type, sK467: set_6).
% 1.51/0.49 tff(func_def_1233, type, sK468: $int > $int).
% 1.51/0.49 tff(func_def_1234, type, sK469: set_6).
% 1.51/0.49 tff(func_def_1235, type, sK470: $int > $int).
% 1.51/0.49 tff(func_def_1236, type, sK471: set_3).
% 1.51/0.49 tff(func_def_1237, type, sK472: $o > $o).
% 1.51/0.49 tff(func_def_1238, type, sK473: set_6).
% 1.51/0.49 tff(func_def_1239, type, sK474: $int > $int).
% 1.51/0.49 tff(func_def_1240, type, sK475: set_6).
% 1.51/0.49 tff(func_def_1241, type, sK476: $int > $int).
% 1.51/0.49 tff(func_def_1242, type, sK477: set_6).
% 1.51/0.49 tff(func_def_1243, type, sK478: $int > $int).
% 1.51/0.49 tff(func_def_1244, type, sK479: set_6).
% 1.51/0.49 tff(func_def_1245, type, sK480: $int > $int).
% 1.51/0.49 tff(func_def_1246, type, sK481: set_6).
% 1.51/0.49 tff(func_def_1247, type, sK482: $int > $int).
% 1.51/0.49 tff(func_def_1248, type, sK483: set_6).
% 1.51/0.49 tff(func_def_1249, type, sK484: $int > $int).
% 1.51/0.49 tff(func_def_1250, type, sK485: set_6).
% 1.51/0.49 tff(func_def_1251, type, sK486: $int > $int).
% 1.51/0.49 tff(func_def_1252, type, sK487: set_6).
% 1.51/0.49 tff(func_def_1253, type, sK488: $int > $int).
% 1.51/0.49 tff(func_def_1254, type, sK489: set_6).
% 1.51/0.49 tff(func_def_1255, type, sK490: $int > $int).
% 1.51/0.49 tff(func_def_1256, type, sK491: set_3).
% 1.51/0.49 tff(func_def_1257, type, sK492: $o > $o).
% 1.51/0.49 tff(func_def_1258, type, sK493: set_4).
% 1.51/0.49 tff(func_def_1259, type, sK494: ($o * $o) > $o).
% 1.51/0.49 tff(func_def_1260, type, sK495: set_4).
% 1.51/0.49 tff(func_def_1261, type, sK496: ($o * $o) > $o).
% 1.51/0.49 tff(func_def_1262, type, sK497: set_4).
% 1.51/0.49 tff(func_def_1263, type, sK498: ($o * $o) > $o).
% 1.51/0.49 tff(func_def_1264, type, sK499: set_4).
% 1.51/0.49 tff(func_def_1265, type, sK500: ($o * $o) > $o).
% 1.51/0.49 tff(func_def_1266, type, sK501: set_4).
% 1.51/0.49 tff(func_def_1267, type, sK502: ($o * $o) > $o).
% 1.51/0.49 tff(func_def_1268, type, sK503: set_4).
% 1.51/0.49 tff(func_def_1269, type, sK504: ($o * $o) > $o).
% 1.51/0.49 tff(func_def_1270, type, sK505: set_5).
% 1.51/0.49 tff(func_def_1271, type, sK506: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1272, type, sK507: set_5).
% 1.51/0.49 tff(func_def_1273, type, sK508: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1274, type, sK509: set_5).
% 1.51/0.49 tff(func_def_1275, type, sK510: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1276, type, sK511: set_5).
% 1.51/0.49 tff(func_def_1277, type, sK512: ($int * $int) > $o).
% 1.51/0.49 tff(func_def_1278, type, sK513: $int > $int).
% 1.51/0.49 tff(func_def_1279, type, sK514: $int > $int).
% 1.51/0.49 tff(func_def_1280, type, sK515: $int > $int).
% 1.51/0.49 tff(func_def_1281, type, sK516: $int > $int).
% 1.51/0.49 tff(func_def_1282, type, sK517: $int > $int).
% 1.51/0.49 tff(pred_def_1, type, mem0: ($int * set_0) > $o).
% 1.51/0.49 tff(pred_def_4, type, mem2: ($o * set_2) > $o).
% 1.51/0.49 tff(pred_def_5, type, mem3: ($o * $o * set_3) > $o).
% 1.51/0.49 tff(pred_def_6, type, mem4: ($o * $o * $o * set_4) > $o).
% 1.51/0.49 tff(pred_def_7, type, mem5: ($int * $int * $o * set_5) > $o).
% 1.51/0.49 tff(pred_def_8, type, mem6: ($int * $int * set_6) > $o).
% 1.51/0.49 tff(f2,axiom,(
% 1.51/0.49 max_int = 2147483647),
% 1.51/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',max_int_axiom)).
% 1.51/0.49 tff(f284,axiom,(
% 1.51/0.49 ! [X0 : $int] : (mem0(X0,g_s367_358) <=> ($greatereq(X0,min_int) & $lesseq(X0,max_int)))),
% 1.51/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p','Define:ctx:339')).
% 1.51/0.49 tff(f835,axiom,(
% 1.51/0.49 ! [X0 : $int] : (! [X1 : $int,X2 : $int] : ((! [X3 : $int] : (X3 = $difference(g_s665_664,g_s666_665) => mem6(X3,X1,g_s667_666)) & mem6(g_s654_1_623,X2,g_s667_666)) => X0 = divB($sum($product(g_s660_660,$difference(X1,X2)),g_s657_1_628),2)) => mem0(X0,g_s367_358))),
% 1.51/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p','Local_Hyp:13')).
% 1.51/0.49 tff(f842,conjecture,(
% 1.51/0.49 ? [X0 : $int] : ! [X1 : $int] : (X1 = $difference(g_s665_664,g_s666_665) => mem6(X1,X0,g_s667_666))),
% 1.51/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p','Goal')).
% 1.51/0.49 tff(f843,negated_conjecture,(
% 1.51/0.49 ~ ? [X0 : $int] : ! [X1 : $int] : (X1 = $difference(g_s665_664,g_s666_665) => mem6(X1,X0,g_s667_666))),
% 1.51/0.49 inference(negated_conjecture,[status(cth)],[f842])).
% 1.51/0.49 tff(f894,plain,(
% 1.51/0.49 ! [X0 : $int] : (mem0(X0,g_s367_358) <=> (~$less(X0,min_int) & ~$less(max_int,X0)))),
% 1.51/0.49 inference(theory_normalization,[],[f284])).
% 1.51/0.49 tff(f980,plain,(
% 1.51/0.49 ! [X0 : $int] : (! [X1 : $int,X2 : $int] : ((! [X3 : $int] : ($sum(g_s665_664,$uminus(g_s666_665)) = X3 => mem6(X3,X1,g_s667_666)) & mem6(g_s654_1_623,X2,g_s667_666)) => divB($sum($product(g_s660_660,$sum(X1,$uminus(X2))),g_s657_1_628),2) = X0) => mem0(X0,g_s367_358))),
% 1.51/0.49 inference(theory_normalization,[],[f835])).
% 1.51/0.49 tff(f985,plain,(
% 1.51/0.49 ~ ? [X0 : $int] : ! [X1 : $int] : ($sum(g_s665_664,$uminus(g_s666_665)) = X1 => mem6(X1,X0,g_s667_666))),
% 1.51/0.49 inference(theory_normalization,[],[f843])).
% 1.51/0.49 tff(f991,definition,(
% 1.51/0.49 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 1.51/0.49 introduced(theory,[tha_non-reflexivity])).
% 1.51/0.49 tff(f995,definition,(
% 1.51/0.49 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 1.51/0.49 introduced(theory,[tha_order_plus_one_dichotomy])).
% 1.51/0.49 tff(f2105,plain,(
% 1.51/0.49 ! [X0 : $int] : (mem0(X0,g_s367_358) | ? [X1 : $int,X2 : $int] : (divB($sum($product(g_s660_660,$sum(X1,$uminus(X2))),g_s657_1_628),2) != X0 & (! [X3 : $int] : (mem6(X3,X1,g_s667_666) | $sum(g_s665_664,$uminus(g_s666_665)) != X3) & mem6(g_s654_1_623,X2,g_s667_666))))),
% 1.51/0.49 inference(ennf_transformation,[],[f980])).
% 1.51/0.49 tff(f2106,plain,(
% 1.51/0.49 ! [X0 : $int] : (mem0(X0,g_s367_358) | ? [X1 : $int,X2 : $int] : (divB($sum($product(g_s660_660,$sum(X1,$uminus(X2))),g_s657_1_628),2) != X0 & ! [X3 : $int] : (mem6(X3,X1,g_s667_666) | $sum(g_s665_664,$uminus(g_s666_665)) != X3) & mem6(g_s654_1_623,X2,g_s667_666)))),
% 1.51/0.49 inference(flattening,[],[f2105])).
% 1.51/0.49 tff(f2111,plain,(
% 1.51/0.49 ! [X0 : $int] : ? [X1 : $int] : (~mem6(X1,X0,g_s667_666) & $sum(g_s665_664,$uminus(g_s666_665)) = X1)),
% 1.51/0.49 inference(ennf_transformation,[],[f985])).
% 1.51/0.49 tff(f2663,plain,(
% 1.51/0.49 ! [X0 : $int] : ((mem0(X0,g_s367_358) | ($less(X0,min_int) | $less(max_int,X0))) & ((~$less(X0,min_int) & ~$less(max_int,X0)) | ~mem0(X0,g_s367_358)))),
% 1.51/0.49 inference(nnf_transformation,[],[f894])).
% 1.51/0.49 tff(f2664,plain,(
% 1.51/0.49 ! [X0 : $int] : ((mem0(X0,g_s367_358) | $less(X0,min_int) | $less(max_int,X0)) & ((~$less(X0,min_int) & ~$less(max_int,X0)) | ~mem0(X0,g_s367_358)))),
% 1.51/0.49 inference(flattening,[],[f2663])).
% 1.51/0.49 tff(f2841,plain,(
% 1.51/0.49 ! [X0 : $int] : (mem0(X0,g_s367_358) | (divB($sum($product(g_s660_660,$sum(sK515(X0),$uminus(sK516(X0)))),g_s657_1_628),2) != X0 & ! [X3 : $int] : (mem6(X3,sK515(X0),g_s667_666) | $sum(g_s665_664,$uminus(g_s666_665)) != X3) & mem6(g_s654_1_623,sK516(X0),g_s667_666)))),
% 1.51/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK515,sK516]),skolemize(X1,sK515(X0)),skolemize(X2,sK516(X0))],[f2106])).
% 1.51/0.49 tff(f2842,plain,(
% 1.51/0.49 ! [X0 : $int] : (~mem6(sK517(X0),X0,g_s667_666) & $sum(g_s665_664,$uminus(g_s666_665)) = sK517(X0))),
% 1.51/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK517]),skolemize(X1,sK517(X0))],[f2111])).
% 1.51/0.49 tff(f3654,plain,(
% 1.51/0.49 max_int = 2147483647),
% 1.51/0.49 inference(cnf_transformation,[],[f2])).
% 1.51/0.49 tff(f4314,plain,(
% 1.51/0.49 ( ! [X0 : $int] : (~$less(max_int,X0) | ~mem0(X0,g_s367_358)) )),
% 1.51/0.49 inference(cnf_transformation,[],[f2664])).
% 1.51/0.49 tff(f5143,plain,(
% 1.51/0.49 ( ! [X3 : $int,X0 : $int] : (mem0(X0,g_s367_358) | mem6(X3,sK515(X0),g_s667_666) | $sum(g_s665_664,$uminus(g_s666_665)) != X3) )),
% 1.51/0.49 inference(cnf_transformation,[],[f2841])).
% 1.51/0.49 tff(f5151,plain,(
% 1.51/0.49 ( ! [X0 : $int] : ($sum(g_s665_664,$uminus(g_s666_665)) = sK517(X0)) )),
% 1.51/0.49 inference(cnf_transformation,[],[f2842])).
% 1.51/0.49 tff(f5152,plain,(
% 1.51/0.49 ( ! [X0 : $int] : (~mem6(sK517(X0),X0,g_s667_666)) )),
% 1.51/0.49 inference(cnf_transformation,[],[f2842])).
% 1.51/0.49 tff(f5309,plain,(
% 1.51/0.49 ( ! [X0 : $int] : (~$less(2147483647,X0) | ~mem0(X0,g_s367_358)) )),
% 1.51/0.49 inference(definition_unfolding,[],[f4314,f3654])).
% 1.51/0.49 tff(f5558,plain,(
% 1.51/0.49 ( ! [X0 : $int] : (~mem6($sum(g_s665_664,$uminus(g_s666_665)),X0,g_s667_666)) )),
% 1.51/0.49 inference(definition_unfolding,[],[f5152,f5151])).
% 1.51/0.49 tff(f6173,plain,(
% 1.51/0.49 ( ! [X0 : $int] : (mem0(X0,g_s367_358) | mem6($sum(g_s665_664,$uminus(g_s666_665)),sK515(X0),g_s667_666)) )),
% 1.51/0.49 inference(equality_resolution,[],[f5143])).
% 1.51/0.49 tff(f6211,definition,(
% 1.51/0.49 spl518_7 <=> ! [X0 : $int] : ~$less(2147483647,X0)),
% 1.51/0.49 introduced(definition,[new_symbols(definition,[spl518_7])],[avatar_definition])).
% 1.51/0.49 tff(f6212,plain,(
% 1.51/0.49 ( ! [X0 : $int] : (~$less(2147483647,X0)) ) | ~spl518_7),
% 1.51/0.49 inference(avatar_component_clause,[],[f6211])).
% 1.51/0.49 tff(f21876,plain,(
% 1.51/0.49 ( ! [X0 : $int] : ($less(X0,2147483647)) ) | ~spl518_7),
% 1.51/0.49 inference(resolution,[],[f995,f6212])).
% 1.51/0.49 tff(f21978,plain,(
% 1.51/0.49 $false | ~spl518_7),
% 1.51/0.49 inference(resolution,[],[f21876,f991])).
% 1.51/0.49 tff(f21991,plain,(
% 1.51/0.49 ~spl518_7),
% 1.51/0.49 inference(avatar_contradiction_clause,[],[f21978])).
% 1.51/0.49 tff(f22129,plain,(
% 1.51/0.49 ( ! [X0 : $int] : (mem0(X0,g_s367_358)) )),
% 1.51/0.49 inference(forward_subsumption_resolution,[],[f6173,f5558])).
% 1.51/0.49 tff(f22131,plain,(
% 1.51/0.49 ( ! [X0 : $int] : (mem0(X0,g_s367_358)) )),
% 1.51/0.49 inference(global_subsumption,[],[f22129])).
% 1.51/0.49 tff(f22267,plain,(
% 1.51/0.49 ( ! [X0 : $int] : (~$less(2147483647,X0)) )),
% 1.51/0.49 inference(global_subsumption,[],[f22131,f5309])).
% 1.51/0.49 tff(f22391,plain,(
% 1.51/0.49 spl518_7),
% 1.51/0.49 inference(avatar_split_clause,[],[f22267,f6211])).
% 1.51/0.49 cnf(s9916, plain, ~spl518_7, inference(sat_conversion,[],[f21991])).
% 1.51/0.49 cnf(s10332, plain, spl518_7, inference(sat_conversion,[],[f22391])).
% 1.51/0.49 cnf(s10335, plain, $false, inference(rat,[],[s9916,s10332])).
% 1.51/0.49 tff(f22392,plain,(
% 1.51/0.49 $false),
% 1.51/0.49 inference(avatar_sat_refutation,[],[s10335])).
% 1.51/0.49 % SZS output end Proof for theBenchmark
% 1.51/0.49 % (2275131)------------------------------
% 1.51/0.49 % (2275131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.49 % (2275131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.49 % (2275131)CaDiCaL version: 2.1.3
% 1.51/0.49 % (2275131)Termination reason: Refutation
% 1.51/0.49 % (2275131)Time elapsed: 0.202 s
% 1.51/0.49 % (2275131)Peak memory usage: 25 MB
% 1.51/0.49 % (2275131)Instructions burned: 730 (million)
% 1.51/0.49 % (2275124)Success in time 0.25 s
% 1.51/0.49 % Vampire exiting
%------------------------------------------------------------------------------