%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC523_1 : TPTP v9.3.1. Bugfixed v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:11 PM UTC 2026
% Result : Theorem 1.42s 0.39s
% Output : Refutation 1.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWC523_1 : TPTP v9.3.1. Bugfixed v9.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 09:41:19 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.13 Running first-order model finding
% 0.09/0.13 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.42/0.39 % (3265544)Will run a generic schedule for satisfiability detection.
% 1.42/0.39 % (3265550)% WARNING: option uhcvi not known.
% 1.42/0.39 % (3265549)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1853877220_2999 on theBenchmark for (2999ds/0Mi)
% 1.42/0.39 % (3265551)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2884362082:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.42/0.39 % (3265552)dis+10_1_sil=32000:sp=arity:random_seed=1479626528:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.42/0.39 % (3265550)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2631609775:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.42/0.39 % (3265553)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3842883475:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.42/0.39 % (3265554)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4229619895:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.42/0.39 % (3265555)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3216787238:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.42/0.39 % (3265549)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.42/0.39 % (3265549)Terminated due to inappropriate strategy.
% 1.42/0.39 % (3265549)------------------------------
% 1.42/0.39 % (3265549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.39 % (3265549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.39 % (3265549)CaDiCaL version: 2.1.3
% 1.42/0.39 % (3265549)Termination reason: Inappropriate
% 1.42/0.39 % (3265549)Time elapsed: 0.011 s
% 1.42/0.39 % (3265549)Peak memory usage: 12 MB
% 1.42/0.39 % (3265549)Instructions burned: 43 (million)
% 1.42/0.39 % (3265549)------------------------------
% 1.42/0.39 % (3265549)------------------------------
% 1.42/0.39 % (3265563)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=858156380:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.42/0.39 % (3265552)Instruction limit reached!
% 1.42/0.39 % (3265552)------------------------------
% 1.42/0.39 % (3265552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.39 % (3265552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.39 % (3265552)CaDiCaL version: 2.1.3
% 1.42/0.39 % (3265552)Termination reason: Instruction limit
% 1.42/0.39 % (3265552)Termination phase: Saturation
% 1.42/0.39 % (3265552)Time elapsed: 0.030 s
% 1.42/0.39 % (3265552)Peak memory usage: 14 MB
% 1.42/0.39 % (3265552)Instructions burned: 103 (million)
% 1.42/0.39 % (3265553)Instruction limit reached!
% 1.42/0.39 % (3265553)------------------------------
% 1.42/0.39 % (3265553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.39 % (3265553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.39 % (3265553)CaDiCaL version: 2.1.3
% 1.42/0.39 % (3265553)Termination reason: Instruction limit
% 1.42/0.39 % (3265553)Termination phase: Saturation
% 1.42/0.39 % (3265553)Time elapsed: 0.032 s
% 1.42/0.39 % (3265553)Peak memory usage: 14 MB
% 1.42/0.39 % (3265553)Instructions burned: 116 (million)
% 1.42/0.39 % (3265563)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.42/0.39 % (3265563)Terminated due to inappropriate strategy.
% 1.42/0.39 % (3265563)------------------------------
% 1.42/0.39 % (3265563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.39 % (3265563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.39 % (3265563)CaDiCaL version: 2.1.3
% 1.42/0.39 % (3265563)Termination reason: Inappropriate
% 1.42/0.39 % (3265563)Time elapsed: 0.009 s
% 1.42/0.39 % (3265563)Peak memory usage: 11 MB
% 1.42/0.39 % (3265563)Instructions burned: 33 (million)
% 1.42/0.39 % (3265563)------------------------------
% 1.42/0.39 % (3265563)------------------------------
% 1.42/0.39 % (3265554)Instruction limit reached!
% 1.42/0.39 % (3265554)------------------------------
% 1.42/0.39 % (3265554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.39 % (3265554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.39 % (3265554)CaDiCaL version: 2.1.3
% 1.42/0.39 % (3265554)Termination reason: Instruction limit
% 1.42/0.39 % (3265554)Termination phase: Saturation
% 1.42/0.39 % (3265554)Time elapsed: 0.037 s
% 1.42/0.39 % (3265554)Peak memory usage: 14 MB
% 1.42/0.39 % (3265554)Instructions burned: 131 (million)
% 1.42/0.39 % (3265565)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2763951878:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.42/0.39 % (3265566)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=1349575780:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.42/0.39 % (3265567)ott-21_1_sil=16000:fs=off:random_seed=2852137448:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 1.42/0.39 % (3265568)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1240019508:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 1.42/0.39 % (3265555)Instruction limit reached!
% 1.42/0.39 % (3265555)------------------------------
% 1.42/0.39 % (3265555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.39 % (3265555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.39 % (3265555)CaDiCaL version: 2.1.3
% 1.42/0.39 % (3265555)Termination reason: Instruction limit
% 1.42/0.39 % (3265555)Termination phase: Saturation
% 1.42/0.39 % (3265555)Time elapsed: 0.070 s
% 1.42/0.39 % (3265555)Peak memory usage: 15 MB
% 1.42/0.39 % (3265555)Instructions burned: 159 (million)
% 1.42/0.39 % (3265565)Instruction limit reached!
% 1.42/0.39 % (3265565)------------------------------
% 1.42/0.39 % (3265565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.39 % (3265565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.39 % (3265565)CaDiCaL version: 2.1.3
% 1.42/0.39 % (3265565)Termination reason: Instruction limit
% 1.42/0.39 % (3265565)Termination phase: Saturation
% 1.42/0.39 % (3265565)Time elapsed: 0.039 s
% 1.42/0.39 % (3265565)Peak memory usage: 15 MB
% 1.42/0.39 % (3265565)Instructions burned: 132 (million)
% 1.42/0.39 % (3265573)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3313685234:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 1.42/0.39 % (3265574)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1474470074:i=1179_2999 on theBenchmark for (2999ds/1179Mi)
% 1.42/0.39 % (3265567)Instruction limit reached!
% 1.42/0.39 % (3265567)------------------------------
% 1.42/0.39 % (3265567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.39 % (3265567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.39 % (3265567)CaDiCaL version: 2.1.3
% 1.42/0.39 % (3265567)Termination reason: Instruction limit
% 1.42/0.39 % (3265567)Termination phase: Saturation
% 1.42/0.39 % (3265567)Time elapsed: 0.049 s
% 1.42/0.39 % (3265567)Peak memory usage: 14 MB
% 1.42/0.39 % (3265567)Instructions burned: 181 (million)
% 1.42/0.39 % (3265573)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.42/0.39 % (3265573)Terminated due to inappropriate strategy.
% 1.42/0.39 % (3265573)------------------------------
% 1.42/0.39 % (3265573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.39 % (3265573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.39 % (3265573)CaDiCaL version: 2.1.3
% 1.42/0.39 % (3265573)Termination reason: Inappropriate
% 1.42/0.39 % (3265573)Time elapsed: 0.009 s
% 1.42/0.39 % (3265573)Peak memory usage: 12 MB
% 1.42/0.39 % (3265573)Instructions burned: 33 (million)
% 1.42/0.39 % (3265573)------------------------------
% 1.42/0.39 % (3265573)------------------------------
% 1.42/0.39 % (3265580)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=550778457:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 1.42/0.39 % (3265581)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=3571936228:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 1.42/0.39 % (3265580)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.42/0.39 % (3265580)Terminated due to inappropriate strategy.
% 1.42/0.39 % (3265580)------------------------------
% 1.42/0.39 % (3265580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.39 % (3265580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.39 % (3265580)CaDiCaL version: 2.1.3
% 1.42/0.39 % (3265580)Termination reason: Inappropriate
% 1.42/0.39 % (3265580)Time elapsed: 0.009 s
% 1.42/0.39 % (3265580)Peak memory usage: 11 MB
% 1.42/0.39 % (3265580)Instructions burned: 34 (million)
% 1.42/0.39 % (3265580)------------------------------
% 1.42/0.39 % (3265580)------------------------------
% 1.42/0.39 % (3265592)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3708715460:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 1.42/0.39 % (3265568)Instruction limit reached!
% 1.42/0.39 % (3265568)------------------------------
% 1.42/0.39 % (3265568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.39 % (3265568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.39 % (3265568)CaDiCaL version: 2.1.3
% 1.42/0.39 % (3265568)Termination reason: Instruction limit
% 1.42/0.39 % (3265568)Termination phase: Saturation
% 1.42/0.39 % (3265568)Time elapsed: 0.150 s
% 1.42/0.39 % (3265568)Peak memory usage: 15 MB
% 1.42/0.39 % (3265568)Instructions burned: 477 (million)
% 1.42/0.39 % (3265629)fmb+10_1_sil=64000:random_seed=1738726546:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 1.42/0.39 % (3265629)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 1.42/0.39 % (3265629)Terminated due to inappropriate strategy.
% 1.42/0.39 % (3265629)------------------------------
% 1.42/0.39 % (3265629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.39 % (3265629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.39 % (3265629)CaDiCaL version: 2.1.3
% 1.42/0.39 % (3265629)Termination reason: Inappropriate
% 1.42/0.39 % (3265629)Time elapsed: 0.009 s
% 1.42/0.39 % (3265629)Peak memory usage: 11 MB
% 1.42/0.39 % (3265629)Instructions burned: 35 (million)
% 1.42/0.39 % (3265629)------------------------------
% 1.42/0.39 % (3265629)------------------------------
% 1.42/0.39 % (3265642)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2696907015:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 1.42/0.39 % (3265550) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3265544-3265550"...
% 1.42/0.39 % (3265550)...printing done.
% 1.42/0.39 % (3265550)Refutation found. Thanks to Tanya!
% 1.42/0.39 % SZS status Theorem for theBenchmark
% 1.42/0.39 % SZS output start Proof for theBenchmark
% 1.42/0.39 tff(type_def_5, type, set_0: $tType).
% 1.42/0.39 tff(type_def_6, type, set_2: $tType).
% 1.42/0.39 tff(type_def_7, type, set_3: $tType).
% 1.42/0.39 tff(type_def_8, type, set_4: $tType).
% 1.42/0.39 tff(func_def_0, type, min_int: $int).
% 1.42/0.39 tff(func_def_1, type, max_int: $int).
% 1.42/0.39 tff(func_def_5, type, g_s0_0: set_0).
% 1.42/0.39 tff(func_def_6, type, g_s1_1: $int).
% 1.42/0.39 tff(func_def_7, type, g_s2_2: $int).
% 1.42/0.39 tff(func_def_8, type, g_s3_3: set_0).
% 1.42/0.39 tff(func_def_9, type, g_s4_4: $int).
% 1.42/0.39 tff(func_def_10, type, g_s5_5: $int).
% 1.42/0.39 tff(func_def_11, type, g_s6_6: set_0).
% 1.42/0.39 tff(func_def_12, type, g_s7_7: $int).
% 1.42/0.39 tff(func_def_13, type, g_s8_8: $int).
% 1.42/0.39 tff(func_def_14, type, g_s9_9: set_0).
% 1.42/0.39 tff(func_def_15, type, g_s10_10: $int).
% 1.42/0.39 tff(func_def_16, type, g_s11_11: $int).
% 1.42/0.39 tff(func_def_17, type, g_s12_12: $int).
% 1.42/0.39 tff(func_def_18, type, g_s13_13: $int).
% 1.42/0.39 tff(func_def_19, type, g_s14_14: $int).
% 1.42/0.39 tff(func_def_20, type, g_s15_15: $int).
% 1.42/0.39 tff(func_def_21, type, g_s16_16: $int).
% 1.42/0.39 tff(func_def_22, type, g_s17_17: $int).
% 1.42/0.39 tff(func_def_23, type, g_s18_18: $int).
% 1.42/0.39 tff(func_def_24, type, g_s19_19: set_0).
% 1.42/0.39 tff(func_def_25, type, g_s20_20: $int).
% 1.42/0.39 tff(func_def_26, type, g_s21_21: $int).
% 1.42/0.39 tff(func_def_27, type, g_s22_22: set_0).
% 1.42/0.39 tff(func_def_28, type, g_s23_23: $int).
% 1.42/0.39 tff(func_def_29, type, g_s24_24: $int).
% 1.42/0.39 tff(func_def_30, type, g_s25_25: $int).
% 1.42/0.39 tff(func_def_31, type, g_s26_26: $int).
% 1.42/0.39 tff(func_def_32, type, g_s27_27: $int).
% 1.42/0.39 tff(func_def_33, type, g_s28_28: $int).
% 1.42/0.39 tff(func_def_34, type, g_s29_29: $int).
% 1.42/0.39 tff(func_def_35, type, g_s30_30: $int).
% 1.42/0.39 tff(func_def_36, type, g_s31_31: $int).
% 1.42/0.39 tff(func_def_37, type, g_s33_32: set_0).
% 1.42/0.39 tff(func_def_38, type, g_s32_33: $int).
% 1.42/0.39 tff(func_def_39, type, g_s35_34: set_0).
% 1.42/0.39 tff(func_def_40, type, g_s34_35: $int).
% 1.42/0.39 tff(func_def_41, type, g_s37_36: set_0).
% 1.42/0.39 tff(func_def_42, type, g_s36_37: $int).
% 1.42/0.39 tff(func_def_43, type, g_s38_38: $int).
% 1.42/0.39 tff(func_def_44, type, g_s39_39: $int).
% 1.42/0.39 tff(func_def_45, type, g_s40_40: set_0).
% 1.42/0.39 tff(func_def_46, type, set_2_empty: set_2).
% 1.42/0.39 tff(func_def_47, type, set_2_insert: set_2 > set_2).
% 1.42/0.39 tff(func_def_48, type, g_s41_41: set_2).
% 1.42/0.39 tff(func_def_49, type, set_3_empty: set_3).
% 1.42/0.39 tff(func_def_50, type, set_3_insert: set_3 > set_3).
% 1.42/0.39 tff(func_def_51, type, g_s42_42: set_3).
% 1.42/0.39 tff(func_def_52, type, set_4_empty: set_4).
% 1.42/0.39 tff(func_def_53, type, set_4_insert: set_4 > set_4).
% 1.42/0.39 tff(func_def_54, type, g_s43_43: set_4).
% 1.42/0.39 tff(func_def_55, type, g_s44_44: set_4).
% 1.42/0.39 tff(func_def_56, type, g_s45_45: set_3).
% 1.42/0.39 tff(func_def_57, type, g_s46_46: set_4).
% 1.42/0.39 tff(func_def_58, type, g_s47_47: set_4).
% 1.42/0.39 tff(func_def_59, type, g_s48_48: set_3).
% 1.42/0.39 tff(func_def_60, type, g_s49_49: set_4).
% 1.42/0.39 tff(func_def_61, type, g_s50_50: set_4).
% 1.42/0.39 tff(func_def_62, type, g_s51_51: set_4).
% 1.42/0.39 tff(func_def_63, type, g_s52_52: set_4).
% 1.42/0.39 tff(func_def_64, type, g_s53_53: set_4).
% 1.42/0.39 tff(func_def_65, type, g_s54_54: set_4).
% 1.42/0.39 tff(func_def_66, type, g_s55_55: set_4).
% 1.42/0.39 tff(func_def_67, type, g_s56_56: set_4).
% 1.42/0.39 tff(func_def_68, type, g_s57_57: set_4).
% 1.42/0.39 tff(func_def_69, type, g_s58_58: set_4).
% 1.42/0.39 tff(func_def_70, type, g_s59_59: set_4).
% 1.42/0.39 tff(func_def_71, type, g_s60_60: set_4).
% 1.42/0.39 tff(func_def_72, type, g_s66_61: $int).
% 1.42/0.39 tff(func_def_73, type, g_s67_62: $int).
% 1.42/0.39 tff(func_def_74, type, g_s68_63: $int).
% 1.42/0.39 tff(func_def_75, type, g_s69_64: $int).
% 1.42/0.39 tff(func_def_76, type, g_s70_65: $int).
% 1.42/0.39 tff(func_def_77, type, g_s71_66: $int).
% 1.42/0.39 tff(func_def_78, type, g_s72_67: $int).
% 1.42/0.39 tff(func_def_79, type, g_s73_68: $int).
% 1.42/0.39 tff(func_def_80, type, g_s74_69: $int).
% 1.42/0.39 tff(func_def_81, type, g_s75_70: $int).
% 1.42/0.39 tff(func_def_82, type, g_s76_71: $int).
% 1.42/0.39 tff(func_def_83, type, g_s77_72: $int).
% 1.42/0.39 tff(func_def_84, type, g_s78_73: $int).
% 1.42/0.39 tff(func_def_85, type, g_s79_74: $int).
% 1.42/0.39 tff(func_def_86, type, g_s80_75: $int).
% 1.42/0.39 tff(func_def_87, type, g_s81_76: $int).
% 1.42/0.39 tff(func_def_88, type, g_s82_77: $int).
% 1.42/0.39 tff(func_def_89, type, g_s83_78: $int).
% 1.42/0.39 tff(func_def_90, type, g_s84_79: $int).
% 1.42/0.39 tff(func_def_91, type, g_s85_80: $int).
% 1.42/0.39 tff(func_def_92, type, g_s86_81: $int).
% 1.42/0.39 tff(func_def_93, type, g_s87_82: $int).
% 1.42/0.39 tff(func_def_94, type, g_s88_83: $int).
% 1.42/0.39 tff(func_def_95, type, g_s89_84: $int).
% 1.42/0.39 tff(func_def_96, type, g_s90_85: $int).
% 1.42/0.39 tff(func_def_97, type, g_s91_86: $int).
% 1.42/0.39 tff(func_def_98, type, g_s92_87: $int).
% 1.42/0.39 tff(func_def_99, type, g_s93_88: $int).
% 1.42/0.39 tff(func_def_100, type, g_s94_89: $int).
% 1.42/0.39 tff(func_def_101, type, g_s95_90: $int).
% 1.42/0.39 tff(func_def_102, type, g_s96_91: $int).
% 1.42/0.39 tff(func_def_103, type, g_s97_92: $int).
% 1.42/0.39 tff(func_def_104, type, g_s98_93: $int).
% 1.42/0.39 tff(func_def_105, type, g_s99_94: $int).
% 1.42/0.39 tff(func_def_106, type, g_s100_95: $int).
% 1.42/0.39 tff(func_def_107, type, g_s101_96: $int).
% 1.42/0.39 tff(func_def_108, type, g_s102_97: $int).
% 1.42/0.39 tff(func_def_109, type, g_s103_98: $int).
% 1.42/0.39 tff(func_def_110, type, g_s104_99: $int).
% 1.42/0.39 tff(func_def_111, type, g_s105_100: $int).
% 1.42/0.39 tff(func_def_112, type, g_s106_101: $int).
% 1.42/0.39 tff(func_def_113, type, g_s107_102: $int).
% 1.42/0.39 tff(func_def_114, type, g_s108_103: $int).
% 1.42/0.39 tff(func_def_115, type, g_s109_104: $int).
% 1.42/0.39 tff(func_def_116, type, g_s110_105: $int).
% 1.42/0.39 tff(func_def_117, type, g_s111_106: $int).
% 1.42/0.39 tff(func_def_118, type, g_s112_107: $int).
% 1.42/0.39 tff(func_def_119, type, g_s113_108: $int).
% 1.42/0.39 tff(func_def_120, type, g_s114_109: $int).
% 1.42/0.39 tff(func_def_121, type, g_s115_110: $int).
% 1.42/0.39 tff(func_def_122, type, g_s116_111: $int).
% 1.42/0.39 tff(func_def_123, type, g_s117_112: $int).
% 1.42/0.39 tff(func_def_124, type, g_s118_113: $int).
% 1.42/0.39 tff(func_def_125, type, g_s119_114: $int).
% 1.42/0.39 tff(func_def_126, type, g_s120_115: $int).
% 1.42/0.39 tff(func_def_127, type, g_s121_116: $int).
% 1.42/0.39 tff(func_def_128, type, g_s122_117: $int).
% 1.42/0.39 tff(func_def_129, type, g_s123_118: $int).
% 1.42/0.39 tff(func_def_130, type, g_s124_119: $int).
% 1.42/0.39 tff(func_def_131, type, g_s125_120: $int).
% 1.42/0.39 tff(func_def_132, type, g_s126_121: $int).
% 1.42/0.39 tff(func_def_133, type, g_s127_122: $int).
% 1.42/0.39 tff(func_def_134, type, g_s128_123: $int).
% 1.42/0.39 tff(func_def_135, type, g_s129_124: $int).
% 1.42/0.39 tff(func_def_136, type, g_s130_125: $int).
% 1.42/0.39 tff(func_def_137, type, g_s131_126: $int).
% 1.42/0.39 tff(func_def_138, type, g_s132_127: $int).
% 1.42/0.39 tff(func_def_139, type, g_s133_128: $int).
% 1.42/0.39 tff(func_def_140, type, g_s134_129: $int).
% 1.42/0.39 tff(func_def_141, type, g_s135_130: $int).
% 1.42/0.39 tff(func_def_142, type, g_s136_131: $int).
% 1.42/0.39 tff(func_def_143, type, g_s137_132: $int).
% 1.42/0.39 tff(func_def_144, type, g_s138_133: $int).
% 1.42/0.39 tff(func_def_145, type, g_s139_134: $int).
% 1.42/0.39 tff(func_def_146, type, g_s140_135: $int).
% 1.42/0.39 tff(func_def_147, type, g_s141_136: $int).
% 1.42/0.39 tff(func_def_148, type, g_s142_137: $int).
% 1.42/0.39 tff(func_def_149, type, g_s143_138: $int).
% 1.42/0.39 tff(func_def_150, type, g_s144_139: $int).
% 1.42/0.39 tff(func_def_151, type, g_s145_140: $int).
% 1.42/0.39 tff(func_def_152, type, g_s146_141: $int).
% 1.42/0.39 tff(func_def_153, type, g_s147_142: $int).
% 1.42/0.39 tff(func_def_154, type, g_s148_143: $int).
% 1.42/0.39 tff(func_def_155, type, g_s149_144: $int).
% 1.42/0.39 tff(func_def_156, type, g_s150_145: $int).
% 1.42/0.39 tff(func_def_157, type, g_s151_146: $int).
% 1.42/0.39 tff(func_def_158, type, g_s152_147: $int).
% 1.42/0.39 tff(func_def_159, type, g_s153_148: $int).
% 1.42/0.39 tff(func_def_160, type, g_s154_149: $int).
% 1.42/0.39 tff(func_def_161, type, g_s155_150: $int).
% 1.42/0.39 tff(func_def_162, type, g_s156_151: $int).
% 1.42/0.39 tff(func_def_163, type, g_s157_152: $int).
% 1.42/0.39 tff(func_def_164, type, g_s158_153: $int).
% 1.42/0.39 tff(func_def_165, type, g_s159_154: $int).
% 1.42/0.39 tff(func_def_166, type, g_s160_155: $int).
% 1.42/0.39 tff(func_def_167, type, g_s161_156: $int).
% 1.42/0.39 tff(func_def_168, type, g_s162_157: $int).
% 1.42/0.39 tff(func_def_169, type, g_s163_158: $int).
% 1.42/0.39 tff(func_def_170, type, g_s164_159: $int).
% 1.42/0.39 tff(func_def_171, type, g_s165_160: $int).
% 1.42/0.39 tff(func_def_172, type, g_s166_161: $int).
% 1.42/0.39 tff(func_def_173, type, g_s167_162: $int).
% 1.42/0.39 tff(func_def_174, type, g_s168_163: $int).
% 1.42/0.39 tff(func_def_175, type, g_s169_164: $int).
% 1.42/0.39 tff(func_def_176, type, g_s170_165: $int).
% 1.42/0.39 tff(func_def_177, type, g_s171_166: $int).
% 1.42/0.39 tff(func_def_178, type, g_s172_167: $int).
% 1.42/0.39 tff(func_def_179, type, g_s173_168: $int).
% 1.42/0.39 tff(func_def_180, type, g_s174_169: $int).
% 1.42/0.39 tff(func_def_181, type, g_s175_170: $int).
% 1.42/0.39 tff(func_def_182, type, g_s176_171: $int).
% 1.42/0.39 tff(func_def_183, type, g_s177_172: $int).
% 1.42/0.39 tff(func_def_184, type, g_s178_173: $int).
% 1.42/0.39 tff(func_def_185, type, g_s179_174: $int).
% 1.42/0.39 tff(func_def_186, type, g_s180_175: $int).
% 1.42/0.39 tff(func_def_187, type, g_s181_176: $int).
% 1.42/0.39 tff(func_def_188, type, g_s182_177: $int).
% 1.42/0.39 tff(func_def_189, type, g_s183_178: $int).
% 1.42/0.39 tff(func_def_190, type, g_s184_179: $int).
% 1.42/0.39 tff(func_def_191, type, g_s185_180: set_0).
% 1.42/0.39 tff(func_def_192, type, g_s186_181: set_0).
% 1.42/0.39 tff(func_def_193, type, g_s187_182: $int).
% 1.42/0.39 tff(func_def_194, type, g_s188_183: $int).
% 1.42/0.39 tff(func_def_195, type, g_s189_184: $int).
% 1.42/0.39 tff(func_def_196, type, g_s190_185: $int).
% 1.42/0.39 tff(func_def_197, type, g_s191_186: $int).
% 1.42/0.39 tff(func_def_198, type, g_s192_187: $int).
% 1.42/0.39 tff(func_def_199, type, g_s193_188: $int).
% 1.42/0.39 tff(func_def_200, type, g_s194_189: $int).
% 1.42/0.39 tff(func_def_201, type, g_s195_190: $int).
% 1.42/0.39 tff(func_def_202, type, g_s196_191: $int).
% 1.42/0.39 tff(func_def_203, type, g_s197_192: $int).
% 1.42/0.39 tff(func_def_204, type, g_s198_193: $int).
% 1.42/0.39 tff(func_def_205, type, g_s199_194: $int).
% 1.42/0.39 tff(func_def_206, type, g_s200_195: $int).
% 1.42/0.39 tff(func_def_207, type, g_s201_196: $int).
% 1.42/0.39 tff(func_def_208, type, g_s202_197: $int).
% 1.42/0.39 tff(func_def_209, type, g_s203_198: $int).
% 1.42/0.39 tff(func_def_210, type, g_s204_199: $int).
% 1.42/0.39 tff(func_def_211, type, g_s205_200: $int).
% 1.42/0.39 tff(func_def_212, type, g_s206_201: $int).
% 1.42/0.39 tff(func_def_213, type, g_s207_202: $int).
% 1.42/0.39 tff(func_def_214, type, g_s208_203: $int).
% 1.42/0.39 tff(func_def_215, type, g_s209_204: $int).
% 1.42/0.39 tff(func_def_216, type, g_s210_205: $int).
% 1.42/0.39 tff(func_def_217, type, g_s211_206: $int).
% 1.42/0.39 tff(func_def_218, type, g_s212_207: $int).
% 1.42/0.39 tff(func_def_219, type, g_s213_208: $int).
% 1.42/0.39 tff(func_def_220, type, g_s214_209: $int).
% 1.42/0.39 tff(func_def_221, type, g_s215_210: $int).
% 1.42/0.39 tff(func_def_222, type, g_s216_211: $int).
% 1.42/0.39 tff(func_def_223, type, g_s217_212: $int).
% 1.42/0.39 tff(func_def_224, type, g_s218_213: $int).
% 1.42/0.39 tff(func_def_225, type, g_s219_214: $int).
% 1.42/0.39 tff(func_def_226, type, g_s220_215: $int).
% 1.42/0.39 tff(func_def_227, type, g_s221_216: $int).
% 1.42/0.39 tff(func_def_228, type, g_s222_217: $int).
% 1.42/0.39 tff(func_def_229, type, g_s223_218: $int).
% 1.42/0.39 tff(func_def_230, type, g_s224_219: $int).
% 1.42/0.39 tff(func_def_231, type, g_s225_220: $int).
% 1.42/0.39 tff(func_def_232, type, g_s226_221: $int).
% 1.42/0.39 tff(func_def_233, type, g_s227_222: $int).
% 1.42/0.39 tff(func_def_234, type, g_s228_223: $int).
% 1.42/0.39 tff(func_def_235, type, g_s229_224: $int).
% 1.42/0.39 tff(func_def_236, type, g_s230_225: $int).
% 1.42/0.39 tff(func_def_237, type, g_s231_226: $int).
% 1.42/0.39 tff(func_def_238, type, g_s232_227: $int).
% 1.42/0.39 tff(func_def_239, type, g_s233_228: $int).
% 1.42/0.39 tff(func_def_240, type, g_s234_229: $int).
% 1.42/0.39 tff(func_def_241, type, g_s235_230: $int).
% 1.42/0.39 tff(func_def_242, type, g_s236_231: $int).
% 1.42/0.39 tff(func_def_243, type, g_s237_232: $int).
% 1.42/0.39 tff(func_def_244, type, g_s238_233: $int).
% 1.42/0.39 tff(func_def_245, type, g_s239_234: $int).
% 1.42/0.39 tff(func_def_246, type, g_s240_235: $int).
% 1.42/0.39 tff(func_def_247, type, g_s241_236: $int).
% 1.42/0.39 tff(func_def_248, type, g_s242_237: $int).
% 1.42/0.39 tff(func_def_249, type, g_s243_238: $int).
% 1.42/0.39 tff(func_def_250, type, g_s244_239: $int).
% 1.42/0.39 tff(func_def_251, type, g_s245_240: $int).
% 1.42/0.39 tff(func_def_252, type, g_s246_241: $int).
% 1.42/0.39 tff(func_def_253, type, g_s247_242: $int).
% 1.42/0.39 tff(func_def_254, type, g_s248_243: $int).
% 1.42/0.39 tff(func_def_255, type, g_s249_244: $int).
% 1.42/0.39 tff(func_def_256, type, g_s250_245: $int).
% 1.42/0.39 tff(func_def_257, type, g_s251_246: $int).
% 1.42/0.39 tff(func_def_258, type, g_s252_247: $int).
% 1.42/0.39 tff(func_def_259, type, g_s253_248: $int).
% 1.42/0.39 tff(func_def_260, type, g_s254_249: $int).
% 1.42/0.39 tff(func_def_261, type, g_s255_250: $int).
% 1.42/0.39 tff(func_def_262, type, g_s256_251: $int).
% 1.42/0.39 tff(func_def_263, type, g_s257_252: $int).
% 1.42/0.39 tff(func_def_264, type, g_s258_253: $int).
% 1.42/0.39 tff(func_def_265, type, g_s259_254: $int).
% 1.42/0.39 tff(func_def_266, type, g_s260_255: $int).
% 1.42/0.39 tff(func_def_267, type, g_s261_256: $int).
% 1.42/0.39 tff(func_def_268, type, g_s262_257: $int).
% 1.42/0.39 tff(func_def_269, type, g_s263_258: $int).
% 1.42/0.39 tff(func_def_270, type, g_s264_259: $int).
% 1.42/0.39 tff(func_def_271, type, g_s265_260: $int).
% 1.42/0.39 tff(func_def_272, type, g_s266_261: $int).
% 1.42/0.39 tff(func_def_273, type, g_s267_262: $int).
% 1.42/0.39 tff(func_def_274, type, g_s268_263: $int).
% 1.42/0.39 tff(func_def_275, type, g_s269_264: $int).
% 1.42/0.39 tff(func_def_276, type, g_s270_265: $int).
% 1.42/0.39 tff(func_def_277, type, g_s271_266: $int).
% 1.42/0.39 tff(func_def_278, type, g_s272_267: $int).
% 1.42/0.39 tff(func_def_279, type, g_s273_268: $int).
% 1.42/0.39 tff(func_def_280, type, g_s274_269: $int).
% 1.42/0.39 tff(func_def_281, type, g_s275_270: $int).
% 1.42/0.39 tff(func_def_282, type, g_s276_271: $int).
% 1.42/0.39 tff(func_def_283, type, g_s277_272: $int).
% 1.42/0.39 tff(func_def_284, type, g_s278_273: $int).
% 1.42/0.39 tff(func_def_285, type, g_s279_274: $int).
% 1.42/0.39 tff(func_def_286, type, g_s280_275: $int).
% 1.42/0.39 tff(func_def_287, type, g_s281_276: $int).
% 1.42/0.39 tff(func_def_288, type, g_s282_277: $int).
% 1.42/0.39 tff(func_def_289, type, g_s283_278: $int).
% 1.42/0.39 tff(func_def_290, type, g_s284_279: $int).
% 1.42/0.39 tff(func_def_291, type, g_s285_280: $int).
% 1.42/0.39 tff(func_def_292, type, g_s286_281: $int).
% 1.42/0.39 tff(func_def_293, type, g_s287_282: $int).
% 1.42/0.39 tff(func_def_294, type, g_s288_283: $int).
% 1.42/0.39 tff(func_def_295, type, g_s289_284: $int).
% 1.42/0.39 tff(func_def_296, type, g_s290_285: $int).
% 1.42/0.39 tff(func_def_297, type, g_s291_286: $int).
% 1.42/0.39 tff(func_def_298, type, g_s292_287: $int).
% 1.42/0.39 tff(func_def_299, type, g_s293_288: $int).
% 1.42/0.39 tff(func_def_300, type, g_s294_289: $int).
% 1.42/0.39 tff(func_def_301, type, g_s295_290: $int).
% 1.42/0.39 tff(func_def_302, type, g_s296_291: $int).
% 1.42/0.39 tff(func_def_303, type, g_s297_292: $int).
% 1.42/0.39 tff(func_def_304, type, g_s298_293: $int).
% 1.42/0.39 tff(func_def_305, type, g_s299_294: $int).
% 1.42/0.39 tff(func_def_306, type, g_s300_295: $int).
% 1.42/0.39 tff(func_def_307, type, g_s301_296: set_4).
% 1.42/0.39 tff(func_def_308, type, g_s302_297: set_3).
% 1.42/0.39 tff(func_def_309, type, g_s303_298: set_4).
% 1.42/0.39 tff(func_def_310, type, g_s304_299: set_3).
% 1.42/0.39 tff(func_def_311, type, g_s305_300: set_4).
% 1.42/0.39 tff(func_def_312, type, g_s306_301: set_0).
% 1.42/0.39 tff(func_def_313, type, g_s307_302: set_0).
% 1.42/0.39 tff(func_def_314, type, g_s308_303: set_0).
% 1.42/0.39 tff(func_def_315, type, g_s309_304: set_0).
% 1.42/0.39 tff(func_def_316, type, g_s310_305: set_3).
% 1.42/0.39 tff(func_def_317, type, g_s311_306: set_3).
% 1.42/0.39 tff(func_def_318, type, g_s312_307: set_3).
% 1.42/0.39 tff(func_def_319, type, g_s313_308: set_3).
% 1.42/0.39 tff(func_def_320, type, g_s314_309: set_0).
% 1.42/0.39 tff(func_def_321, type, g_s315_310: set_0).
% 1.42/0.39 tff(func_def_322, type, g_s316_311: set_0).
% 1.42/0.39 tff(func_def_323, type, g_s317_312: set_0).
% 1.42/0.39 tff(func_def_324, type, g_s318_313: set_3).
% 1.42/0.39 tff(func_def_325, type, g_s319_314: set_3).
% 1.42/0.39 tff(func_def_326, type, g_s320_315: set_0).
% 1.42/0.39 tff(func_def_327, type, g_s321_316: set_3).
% 1.42/0.39 tff(func_def_328, type, g_s326_317: $int).
% 1.42/0.39 tff(func_def_329, type, g_s327_318: $int).
% 1.42/0.39 tff(func_def_330, type, g_s328_319: $int).
% 1.42/0.39 tff(func_def_331, type, g_s336_320: $int).
% 1.42/0.39 tff(func_def_332, type, g_s329_321: $int).
% 1.42/0.39 tff(func_def_333, type, g_s335_322: set_3).
% 1.42/0.39 tff(func_def_334, type, g_s331_323: $int).
% 1.42/0.39 tff(func_def_335, type, g_s337_324: set_3).
% 1.42/0.39 tff(func_def_336, type, g_s330_325: $int).
% 1.42/0.39 tff(func_def_337, type, g_s332_326: $int).
% 1.42/0.39 tff(func_def_338, type, g_s334_327: $int).
% 1.42/0.39 tff(func_def_339, type, g_s333_328: $int).
% 1.42/0.39 tff(func_def_340, type, g_s338_329: set_3).
% 1.42/0.39 tff(func_def_341, type, g_s339_1_330: $int).
% 1.42/0.39 tff(func_def_342, type, g_s340_1_331: $int).
% 1.42/0.39 tff(func_def_343, type, g_s341_1_332: $int).
% 1.42/0.39 tff(func_def_344, type, g_s342_1_333: $int).
% 1.42/0.39 tff(func_def_345, type, g_s343_1_334: $int).
% 1.42/0.39 tff(func_def_346, type, g_s344_1_335: $int).
% 1.42/0.39 tff(func_def_347, type, g_s345_1_336: $int).
% 1.42/0.39 tff(func_def_348, type, g_s346_1_337: $int).
% 1.42/0.39 tff(func_def_349, type, g_s347_1_338: $int).
% 1.42/0.39 tff(func_def_350, type, g_s348_1_343: $int).
% 1.42/0.39 tff(func_def_351, type, g_s349_1_344: $int).
% 1.42/0.39 tff(func_def_352, type, g_s350_1_345: $int).
% 1.42/0.39 tff(func_def_353, type, g_s351_1_346: $int).
% 1.42/0.39 tff(func_def_354, type, g_s352_1_347: $int).
% 1.42/0.39 tff(func_def_355, type, g_s353_1_348: $int).
% 1.42/0.39 tff(func_def_356, type, g_s359_349: $int).
% 1.42/0.39 tff(func_def_357, type, g_s363_350: $int).
% 1.42/0.39 tff(func_def_358, type, g_s364_351: $int).
% 1.42/0.39 tff(func_def_359, type, g_s365_352: $int).
% 1.42/0.39 tff(func_def_360, type, g_s359_1_353: $int).
% 1.42/0.39 tff(func_def_361, type, g_s363_1_354: $int).
% 1.42/0.39 tff(func_def_362, type, g_s344_355: $int).
% 1.42/0.39 tff(func_def_363, type, g_s345_356: $int).
% 1.42/0.39 tff(func_def_364, type, g_s346_357: $int).
% 1.42/0.39 tff(func_def_365, type, g_s347_358: $int).
% 1.42/0.39 tff(func_def_366, type, g_s366_359: $int).
% 1.42/0.39 tff(func_def_379, type, sK0: $int).
% 1.42/0.39 tff(func_def_380, type, sK1: $int).
% 1.42/0.39 tff(func_def_381, type, sK2: $int).
% 1.42/0.39 tff(func_def_382, type, sK3: $int).
% 1.42/0.39 tff(func_def_383, type, sK4: $int).
% 1.42/0.39 tff(func_def_384, type, sK5: $int).
% 1.42/0.39 tff(func_def_385, type, sK6: $int > $int).
% 1.42/0.39 tff(func_def_386, type, sK7: $int > $int).
% 1.42/0.39 tff(func_def_387, type, sK8: $int > $int).
% 1.42/0.39 tff(func_def_390, type, sK13: set_3).
% 1.42/0.39 tff(func_def_391, type, sK14: $int > $int).
% 1.42/0.39 tff(func_def_392, type, sK15: set_4).
% 1.42/0.39 tff(func_def_393, type, sK16: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_394, type, sK17: set_4).
% 1.42/0.39 tff(func_def_395, type, sK18: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_396, type, sK19: set_3).
% 1.42/0.39 tff(func_def_397, type, sK20: $int > $int).
% 1.42/0.39 tff(func_def_398, type, sK21: set_4).
% 1.42/0.39 tff(func_def_399, type, sK22: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_400, type, sK23: set_4).
% 1.42/0.39 tff(func_def_401, type, sK24: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_402, type, sK25: set_3).
% 1.42/0.39 tff(func_def_403, type, sK26: $int > $int).
% 1.42/0.39 tff(func_def_404, type, sK27: set_4).
% 1.42/0.39 tff(func_def_405, type, sK28: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_406, type, sK29: set_4).
% 1.42/0.39 tff(func_def_407, type, sK30: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_408, type, sK31: set_4).
% 1.42/0.39 tff(func_def_409, type, sK32: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_410, type, sK33: set_4).
% 1.42/0.39 tff(func_def_411, type, sK34: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_412, type, sK35: set_4).
% 1.42/0.39 tff(func_def_413, type, sK36: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_414, type, sK37: set_4).
% 1.42/0.39 tff(func_def_415, type, sK38: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_416, type, sK39: set_4).
% 1.42/0.39 tff(func_def_417, type, sK40: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_418, type, sK41: set_4).
% 1.42/0.39 tff(func_def_419, type, sK42: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_420, type, sK43: set_4).
% 1.42/0.39 tff(func_def_421, type, sK44: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_422, type, sK45: set_4).
% 1.42/0.39 tff(func_def_423, type, sK46: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_424, type, sK47: set_4).
% 1.42/0.39 tff(func_def_425, type, sK48: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_426, type, sK49: set_4).
% 1.42/0.39 tff(func_def_427, type, sK50: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_428, type, sK51: set_4).
% 1.42/0.39 tff(func_def_429, type, sK52: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_430, type, sK53: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_431, type, sK54: set_4).
% 1.42/0.39 tff(func_def_432, type, sK55: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_433, type, sK56: set_4).
% 1.42/0.39 tff(func_def_434, type, sK57: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_435, type, sK58: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_436, type, sK59: ($int * $int) > $int).
% 1.42/0.39 tff(func_def_437, type, sK60: set_3).
% 1.42/0.39 tff(func_def_438, type, sK61: $int > $int).
% 1.42/0.39 tff(func_def_439, type, sK62: set_3).
% 1.42/0.39 tff(func_def_440, type, sK63: $int > $int).
% 1.42/0.39 tff(func_def_441, type, sK64: set_3).
% 1.42/0.39 tff(func_def_442, type, sK65: $int > $int).
% 1.42/0.39 tff(func_def_443, type, sK66: set_3).
% 1.42/0.39 tff(func_def_444, type, sK67: $int > $int).
% 1.42/0.39 tff(func_def_445, type, sK68: set_3).
% 1.42/0.39 tff(func_def_446, type, sK69: $int > $int).
% 1.42/0.39 tff(func_def_447, type, sK70: set_3 > $int).
% 1.42/0.39 tff(func_def_448, type, sK71: set_3 > $int).
% 1.42/0.39 tff(func_def_449, type, sK72: set_3 > $int).
% 1.42/0.39 tff(func_def_450, type, sK73: ($int * set_3) > $int).
% 1.42/0.39 tff(func_def_451, type, sK75: ($int * set_3) > $int).
% 1.42/0.39 tff(func_def_452, type, sK76: set_3 > $int).
% 1.42/0.39 tff(func_def_453, type, sK77: set_3 > $int).
% 1.42/0.39 tff(func_def_454, type, sK78: set_3 > $int).
% 1.42/0.39 tff(func_def_455, type, sK79: set_3 > $int).
% 1.42/0.39 tff(func_def_456, type, sK80: (set_3 * set_3) > $int).
% 1.42/0.39 tff(func_def_457, type, sK81: (set_3 * set_3) > $int).
% 1.42/0.39 tff(func_def_458, type, sK83: ($int * set_3) > $int).
% 1.42/0.39 tff(func_def_459, type, sK86: (set_3 * $int) > $int).
% 1.42/0.39 tff(func_def_460, type, sK87: set_3 > $int).
% 1.42/0.39 tff(func_def_461, type, sK88: set_3 > $int).
% 1.42/0.39 tff(func_def_462, type, sK89: set_3 > $int).
% 1.42/0.39 tff(func_def_463, type, sK90: ($int * set_3) > $int).
% 1.42/0.39 tff(func_def_464, type, sK92: ($int * set_3) > $int).
% 1.42/0.39 tff(func_def_465, type, sK93: set_3 > $int).
% 1.42/0.39 tff(func_def_466, type, sK94: set_3 > $int).
% 1.42/0.39 tff(func_def_467, type, sK95: set_3 > $int).
% 1.42/0.39 tff(func_def_468, type, sK96: set_3 > $int).
% 1.42/0.39 tff(func_def_469, type, sK97: (set_3 * set_3) > $int).
% 1.42/0.39 tff(func_def_470, type, sK98: (set_3 * set_3) > $int).
% 1.42/0.39 tff(func_def_471, type, sK100: ($int * set_3) > $int).
% 1.42/0.39 tff(func_def_472, type, sK103: (set_3 * $int) > $int).
% 1.42/0.39 tff(func_def_473, type, sK104: set_3 > $int).
% 1.42/0.39 tff(func_def_474, type, sK105: set_3 > $int).
% 1.42/0.39 tff(func_def_475, type, sK106: set_3 > $int).
% 1.42/0.39 tff(func_def_476, type, sK107: ($int * set_3) > $int).
% 1.42/0.39 tff(func_def_477, type, sK109: ($int * set_3) > $int).
% 1.42/0.39 tff(func_def_478, type, sK110: set_3 > $int).
% 1.42/0.39 tff(func_def_479, type, sK111: set_3 > $int).
% 1.42/0.39 tff(func_def_480, type, sK112: set_3 > $int).
% 1.42/0.39 tff(func_def_481, type, sK113: set_3 > $int).
% 1.42/0.39 tff(func_def_482, type, sK114: (set_3 * set_3) > $int).
% 1.42/0.39 tff(func_def_483, type, sK115: (set_3 * set_3) > $int).
% 1.42/0.39 tff(func_def_484, type, sK117: ($int * set_3) > $int).
% 1.42/0.39 tff(func_def_485, type, sK120: (set_3 * $int) > $int).
% 1.42/0.39 tff(func_def_486, type, sK121: $int).
% 1.42/0.39 tff(func_def_487, type, sK123: $int).
% 1.42/0.39 tff(func_def_488, type, sK125: $int).
% 1.42/0.39 tff(func_def_489, type, sK126: $int).
% 1.42/0.39 tff(func_def_490, type, sK128: $int).
% 1.42/0.39 tff(func_def_491, type, sK130: $int).
% 1.42/0.39 tff(func_def_492, type, sK131: $int).
% 1.42/0.39 tff(func_def_493, type, sK133: $int).
% 1.42/0.39 tff(func_def_494, type, sK134: $int).
% 1.42/0.39 tff(func_def_495, type, sK135: $int).
% 1.42/0.39 tff(pred_def_1, type, mem0: ($int * set_0) > $o).
% 1.42/0.39 tff(pred_def_2, type, mem2: ($o * $int * set_2) > $o).
% 1.42/0.39 tff(pred_def_3, type, mem3: ($int * $int * set_3) > $o).
% 1.42/0.39 tff(pred_def_4, type, mem4: ($int * $int * $int * set_4) > $o).
% 1.42/0.39 tff(pred_def_13, type, sP9: $o > $o).
% 1.42/0.39 tff(pred_def_15, type, sP11: $o > $o).
% 1.42/0.39 tff(pred_def_17, type, sP74: (set_3 * set_3 * $int) > $o).
% 1.42/0.39 tff(pred_def_18, type, sP82: ($int * $int * set_3 * set_3) > $o).
% 1.42/0.39 tff(pred_def_19, type, sP84: $int > $o).
% 1.42/0.39 tff(pred_def_20, type, sP85: ($int * set_3) > $o).
% 1.42/0.39 tff(pred_def_21, type, sP91: (set_3 * set_3 * $int) > $o).
% 1.42/0.39 tff(pred_def_22, type, sP99: ($int * $int * set_3 * set_3) > $o).
% 1.42/0.39 tff(pred_def_23, type, sP101: $int > $o).
% 1.42/0.39 tff(pred_def_24, type, sP102: ($int * set_3) > $o).
% 1.42/0.39 tff(pred_def_25, type, sP108: (set_3 * set_3 * $int) > $o).
% 1.42/0.39 tff(pred_def_26, type, sP116: ($int * $int * set_3 * set_3) > $o).
% 1.42/0.39 tff(pred_def_27, type, sP118: $int > $o).
% 1.42/0.39 tff(pred_def_28, type, sP119: ($int * set_3) > $o).
% 1.42/0.39 tff(pred_def_29, type, sK122: $int > $o).
% 1.42/0.39 tff(pred_def_31, type, sK127: $int > $o).
% 1.42/0.39 tff(pred_def_33, type, sK132: $int > $o).
% 1.42/0.39 tff(f28,axiom,(
% 1.42/0.39 $greatereq(g_s336_320,0)),
% 1.42/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:abs:31')).
% 1.42/0.39 tff(f39,axiom,(
% 1.42/0.39 ! [X0 : $int,X1 : $int] : (mem3(X1,X0,g_s338_329) => ($greatereq(X1,0) & $greatereq(X0,0))) & ! [X2 : $int,X3 : $int,X4 : $int] : ((mem3(X2,X3,g_s338_329) & mem3(X2,X4,g_s338_329)) => X3 = X4)),
% 1.42/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:abs:41')).
% 1.42/0.39 tff(f45,axiom,(
% 1.42/0.39 ! [X0 : $int] : (? [X1 : $int] : mem3(X0,X1,g_s338_329) <=> ($greatereq(X0,1) & $lesseq(X0,g_s336_320)))),
% 1.42/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:abs:47')).
% 1.42/0.39 tff(f86,axiom,(
% 1.42/0.39 g_s36_37 = 255),
% 1.42/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:ctx:13')).
% 1.42/0.39 tff(f403,axiom,(
% 1.42/0.39 ! [X0 : $int,X1 : $int,X2 : $int] : (mem4(X2,X1,X0,g_s58_58) <=> (mem0(X2,g_s37_36) & mem0(X1,g_s37_36) & X0 = $remainder_f($sum(X2,X1),$sum(g_s36_37,1))))),
% 1.42/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:ctx:47')).
% 1.42/0.39 tff(f489,axiom,(
% 1.42/0.39 ! [X0 : $int] : (mem0(X0,g_s306_301) => ($greatereq(X0,1) & $lesseq(X0,g_s126_121)))),
% 1.42/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:seext:0')).
% 1.42/0.39 tff(f527,axiom,(
% 1.42/0.39 $lesseq(g_s363_1_354,g_s127_122)),
% 1.42/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Local_Hyp:19')).
% 1.42/0.39 tff(f531,axiom,(
% 1.42/0.39 ! [X0 : $int] : (X0 = $sum(g_s363_1_354,1) => mem0(X0,g_s306_301))),
% 1.42/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Local_Hyp:23')).
% 1.42/0.39 tff(f534,axiom,(
% 1.42/0.39 ~ ! [X0 : $o] : ((X0 <=> ! [X1 : $int] : (X1 = $sum(g_s363_1_354,1) => mem0(X1,g_s307_302))) => mem2(X0,g_s38_38,g_s41_41))),
% 1.42/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Local_Hyp:40')).
% 1.42/0.39 tff(f535,axiom,(
% 1.42/0.39 ~ ! [X0 : $int] : (X0 = $sum(g_s363_1_354,1) => mem0(X0,g_s307_302))),
% 1.42/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Local_Hyp:41')).
% 1.42/0.39 tff(f542,axiom,(
% 1.42/0.39 ! [X0 : $int,X1 : $int] : ((X0 = 1 & X1 = $sum(g_s363_1_354,1)) => mem4(g_s363_1_354,X0,X1,g_s58_58))),
% 1.42/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Local_Hyp:36')).
% 1.42/0.39 tff(f543,conjecture,(
% 1.42/0.39 ! [X0 : $int,X1 : $int] : ((! [X2 : $int] : (X2 = 1 => mem4(g_s363_1_354,X2,X0,g_s58_58)) & ! [X3 : $int] : (X3 = 1 => mem4(g_s363_1_354,X3,X1,g_s58_58))) => ($greatereq(X0,0) & $lesseq(X1,$sum(g_s127_122,1))))),
% 1.42/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Goal')).
% 1.42/0.39 tff(f544,negated_conjecture,(
% 1.42/0.39 ~ ! [X0 : $int,X1 : $int] : ((! [X2 : $int] : (X2 = 1 => mem4(g_s363_1_354,X2,X0,g_s58_58)) & ! [X3 : $int] : (X3 = 1 => mem4(g_s363_1_354,X3,X1,g_s58_58))) => ($greatereq(X0,0) & $lesseq(X1,$sum(g_s127_122,1))))),
% 1.42/0.39 inference(negated_conjecture,[status(cth)],[f543])).
% 1.42/0.39 tff(f563,plain,(
% 1.42/0.39 ~$less(g_s336_320,0)),
% 1.42/0.39 inference(theory_normalization,[],[f28])).
% 1.42/0.39 tff(f569,plain,(
% 1.42/0.39 ! [X0 : $int,X1 : $int] : (mem3(X1,X0,g_s338_329) => (~$less(X1,0) & ~$less(X0,0))) & ! [X2 : $int,X3 : $int,X4 : $int] : ((mem3(X2,X3,g_s338_329) & mem3(X2,X4,g_s338_329)) => X3 = X4)),
% 1.42/0.39 inference(theory_normalization,[],[f39])).
% 1.42/0.39 tff(f575,plain,(
% 1.42/0.39 ! [X0 : $int] : (? [X1 : $int] : mem3(X0,X1,g_s338_329) <=> (~$less(X0,1) & ~$less(g_s336_320,X0)))),
% 1.42/0.39 inference(theory_normalization,[],[f45])).
% 1.42/0.39 tff(f690,plain,(
% 1.42/0.39 ! [X0 : $int] : (mem0(X0,g_s306_301) => (~$less(X0,1) & ~$less(g_s126_121,X0)))),
% 1.42/0.39 inference(theory_normalization,[],[f489])).
% 1.42/0.39 tff(f722,plain,(
% 1.42/0.39 ~$less(g_s127_122,g_s363_1_354)),
% 1.42/0.39 inference(theory_normalization,[],[f527])).
% 1.42/0.39 tff(f726,plain,(
% 1.42/0.39 ~ ! [X0 : $o] : ((X0 <=> ! [X1 : $int] : (X1 = $sum(g_s363_1_354,1) => mem0(X1,g_s307_302))) => mem2(X0,g_s38_38,g_s41_41))),
% 1.42/0.39 inference(theory_normalization,[],[f534])).
% 1.42/0.39 tff(f730,plain,(
% 1.42/0.39 ~ ! [X0 : $int,X1 : $int] : ((! [X2 : $int] : (X2 = 1 => mem4(g_s363_1_354,X2,X0,g_s58_58)) & ! [X3 : $int] : (X3 = 1 => mem4(g_s363_1_354,X3,X1,g_s58_58))) => (~$less(X0,0) & ~$less($sum(g_s127_122,1),X1)))),
% 1.42/0.39 inference(theory_normalization,[],[f544])).
% 1.42/0.39 tff(f731,definition,(
% 1.42/0.39 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 1.42/0.39 introduced(theory,[tha_commutativity])).
% 1.42/0.39 tff(f736,definition,(
% 1.42/0.39 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 1.42/0.39 introduced(theory,[tha_non-reflexivity])).
% 1.42/0.39 tff(f737,definition,(
% 1.42/0.39 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 1.42/0.39 introduced(theory,[tha_transitivity])).
% 1.42/0.39 tff(f738,definition,(
% 1.42/0.39 ( ! [X0 : $int,X1 : $int] : ($less(X0,X1) | $less(X1,X0) | X0 = X1) )),
% 1.42/0.39 introduced(theory,[tha_order_totality])).
% 1.42/0.39 tff(f739,definition,(
% 1.42/0.39 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | $less($sum(X0,X2),$sum(X1,X2))) )),
% 1.42/0.39 introduced(theory,[tha_order_monotonicity])).
% 1.42/0.39 tff(f740,definition,(
% 1.42/0.39 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 1.42/0.39 introduced(theory,[tha_order_plus_one_dichotomy])).
% 1.42/0.39 tff(f748,definition,(
% 1.42/0.39 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,X1)) )),
% 1.42/0.39 introduced(theory,[tha_extra_integer_ordering])).
% 1.42/0.39 tff(f755,plain,(
% 1.42/0.39 ~ ! [X0 : $o] : ((X0 <=> ! [X1 : $int] : (X1 = $sum(g_s363_1_354,1) => mem0(X1,g_s307_302))) => mem2(X0,g_s38_38,g_s41_41))),
% 1.42/0.39 inference(rectify,[],[f726])).
% 1.42/0.39 tff(f775,plain,(
% 1.42/0.39 ! [X0 : $int,X1 : $int] : ((~$less(X1,0) & ~$less(X0,0)) | ~mem3(X1,X0,g_s338_329)) & ! [X2 : $int,X3 : $int,X4 : $int] : (X3 = X4 | (~mem3(X2,X3,g_s338_329) | ~mem3(X2,X4,g_s338_329)))),
% 1.42/0.39 inference(ennf_transformation,[],[f569])).
% 1.42/0.39 tff(f776,plain,(
% 1.42/0.39 ! [X0 : $int,X1 : $int] : ((~$less(X1,0) & ~$less(X0,0)) | ~mem3(X1,X0,g_s338_329)) & ! [X2 : $int,X3 : $int,X4 : $int] : (X3 = X4 | ~mem3(X2,X3,g_s338_329) | ~mem3(X2,X4,g_s338_329))),
% 1.42/0.39 inference(flattening,[],[f775])).
% 1.42/0.39 tff(f825,plain,(
% 1.42/0.39 ! [X0 : $int] : ((~$less(X0,1) & ~$less(g_s126_121,X0)) | ~mem0(X0,g_s306_301))),
% 1.42/0.39 inference(ennf_transformation,[],[f690])).
% 1.42/0.39 tff(f861,plain,(
% 1.42/0.39 ! [X0 : $int] : (mem0(X0,g_s306_301) | $sum(g_s363_1_354,1) != X0)),
% 1.42/0.39 inference(ennf_transformation,[],[f531])).
% 1.42/0.39 tff(f865,plain,(
% 1.42/0.39 ? [X0 : $o] : (~mem2(X0,g_s38_38,g_s41_41) & (X0 <=> ! [X1 : $int] : (mem0(X1,g_s307_302) | $sum(g_s363_1_354,1) != X1)))),
% 1.42/0.39 inference(ennf_transformation,[],[f755])).
% 1.42/0.39 tff(f866,plain,(
% 1.42/0.39 ? [X0 : $int] : (~mem0(X0,g_s307_302) & X0 = $sum(g_s363_1_354,1))),
% 1.42/0.39 inference(ennf_transformation,[],[f535])).
% 1.42/0.39 tff(f871,plain,(
% 1.42/0.39 ! [X0 : $int,X1 : $int] : (mem4(g_s363_1_354,X0,X1,g_s58_58) | (1 != X0 | $sum(g_s363_1_354,1) != X1))),
% 1.42/0.39 inference(ennf_transformation,[],[f542])).
% 1.42/0.39 tff(f872,plain,(
% 1.42/0.39 ! [X0 : $int,X1 : $int] : (mem4(g_s363_1_354,X0,X1,g_s58_58) | 1 != X0 | $sum(g_s363_1_354,1) != X1)),
% 1.42/0.39 inference(flattening,[],[f871])).
% 1.42/0.39 tff(f873,plain,(
% 1.42/0.39 ? [X0 : $int,X1 : $int] : (($less(X0,0) | $less($sum(g_s127_122,1),X1)) & (! [X2 : $int] : (mem4(g_s363_1_354,X2,X0,g_s58_58) | 1 != X2) & ! [X3 : $int] : (mem4(g_s363_1_354,X3,X1,g_s58_58) | 1 != X3)))),
% 1.42/0.39 inference(ennf_transformation,[],[f730])).
% 1.42/0.39 tff(f874,plain,(
% 1.42/0.39 ? [X0 : $int,X1 : $int] : (($less(X0,0) | $less($sum(g_s127_122,1),X1)) & ! [X2 : $int] : (mem4(g_s363_1_354,X2,X0,g_s58_58) | 1 != X2) & ! [X3 : $int] : (mem4(g_s363_1_354,X3,X1,g_s58_58) | 1 != X3))),
% 1.42/0.39 inference(flattening,[],[f873])).
% 1.42/0.39 tff(f903,plain,(
% 1.42/0.39 ~$less(g_s336_320,0)),
% 1.42/0.39 inference(cnf_transformation,[],[f563])).
% 1.42/0.39 tff(f915,plain,(
% 1.42/0.39 ( ! [X0 : $int,X1 : $int] : (~mem3(X1,X0,g_s338_329) | ~$less(X1,0)) )),
% 1.42/0.39 inference(cnf_transformation,[],[f776])).
% 1.42/0.39 tff(f928,plain,(
% 1.42/0.39 ( ! [X0 : $int] : ($less(g_s336_320,X0) | $less(X0,1) | mem3(X0,sK8(X0),g_s338_329)) )),
% 1.42/0.39 inference(cnf_transformation,[],[f575])).
% 1.42/0.39 tff(f972,plain,(
% 1.42/0.39 g_s36_37 = 255),
% 1.42/0.39 inference(cnf_transformation,[],[f86])).
% 1.42/0.39 tff(f1528,plain,(
% 1.42/0.39 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($remainder_f($sum(X2,X1),$sum(g_s36_37,1)) = X0 | ~mem4(X2,X1,X0,g_s58_58)) )),
% 1.42/0.39 inference(cnf_transformation,[],[f403])).
% 1.42/0.39 tff(f1640,plain,(
% 1.42/0.39 ( ! [X0 : $int] : (~mem0(X0,g_s306_301) | ~$less(X0,1)) )),
% 1.42/0.39 inference(cnf_transformation,[],[f825])).
% 1.42/0.39 tff(f1818,plain,(
% 1.42/0.39 ~$less(g_s127_122,g_s363_1_354)),
% 1.42/0.39 inference(cnf_transformation,[],[f722])).
% 1.42/0.39 tff(f1825,plain,(
% 1.42/0.39 ( ! [X0 : $int] : ($sum(g_s363_1_354,1) != X0 | mem0(X0,g_s306_301)) )),
% 1.42/0.39 inference(cnf_transformation,[],[f861])).
% 1.42/0.39 tff(f1832,plain,(
% 1.42/0.39 sK124 | $sum(g_s363_1_354,1) = sK125),
% 1.42/0.39 inference(cnf_transformation,[],[f865])).
% 1.42/0.39 tff(f1834,plain,(
% 1.42/0.39 ( ! [X1 : $int] : (~sK124 | mem0(X1,g_s307_302) | $sum(g_s363_1_354,1) != X1) )),
% 1.42/0.39 inference(cnf_transformation,[],[f865])).
% 1.42/0.39 tff(f1837,plain,(
% 1.42/0.39 $sum(g_s363_1_354,1) = sK126),
% 1.42/0.39 inference(cnf_transformation,[],[f866])).
% 1.42/0.39 tff(f1838,plain,(
% 1.42/0.39 ~mem0(sK126,g_s307_302)),
% 1.42/0.39 inference(cnf_transformation,[],[f866])).
% 1.42/0.39 tff(f1858,plain,(
% 1.42/0.39 ( ! [X0 : $int,X1 : $int] : ($sum(g_s363_1_354,1) != X1 | 1 != X0 | mem4(g_s363_1_354,X0,X1,g_s58_58)) )),
% 1.42/0.39 inference(cnf_transformation,[],[f872])).
% 1.42/0.39 tff(f1859,plain,(
% 1.42/0.39 ( ! [X2 : $int] : (1 != X2 | mem4(g_s363_1_354,X2,sK134,g_s58_58)) )),
% 1.42/0.39 inference(cnf_transformation,[],[f874])).
% 1.42/0.39 tff(f1860,plain,(
% 1.42/0.39 ( ! [X3 : $int] : (1 != X3 | mem4(g_s363_1_354,X3,sK135,g_s58_58)) )),
% 1.42/0.39 inference(cnf_transformation,[],[f874])).
% 1.42/0.39 tff(f1861,plain,(
% 1.42/0.39 $less($sum(g_s127_122,1),sK135) | $less(sK134,0)),
% 1.42/0.39 inference(cnf_transformation,[],[f874])).
% 1.42/0.39 tff(f1937,plain,(
% 1.42/0.39 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($remainder_f($sum(X2,X1),$sum(255,1)) = X0 | ~mem4(X2,X1,X0,g_s58_58)) )),
% 1.42/0.39 inference(definition_unfolding,[],[f1528,f972])).
% 1.42/0.39 tff(f2028,plain,(
% 1.42/0.39 mem0($sum(g_s363_1_354,1),g_s306_301)),
% 1.42/0.39 inference(equality_resolution,[],[f1825])).
% 1.42/0.39 tff(f2032,plain,(
% 1.42/0.39 ~sK124 | mem0($sum(g_s363_1_354,1),g_s307_302)),
% 1.42/0.39 inference(equality_resolution,[],[f1834])).
% 1.42/0.39 tff(f2036,plain,(
% 1.42/0.39 ( ! [X0 : $int] : (1 != X0 | mem4(g_s363_1_354,X0,$sum(g_s363_1_354,1),g_s58_58)) )),
% 1.42/0.39 inference(equality_resolution,[],[f1858])).
% 1.42/0.39 tff(f2037,plain,(
% 1.42/0.39 mem4(g_s363_1_354,1,$sum(g_s363_1_354,1),g_s58_58)),
% 1.42/0.39 inference(equality_resolution,[],[f2036])).
% 1.42/0.39 tff(f2038,plain,(
% 1.42/0.39 mem4(g_s363_1_354,1,sK135,g_s58_58)),
% 1.42/0.39 inference(equality_resolution,[],[f1860])).
% 1.42/0.39 tff(f2039,plain,(
% 1.42/0.39 mem4(g_s363_1_354,1,sK134,g_s58_58)),
% 1.42/0.39 inference(equality_resolution,[],[f1859])).
% 1.42/0.39 tff(f2068,plain,(
% 1.42/0.39 ( ! [X0 : $int,X1 : $int] : (~$less(X1,0) | mem3(X1,X0,g_s338_329)) )),
% 1.42/0.39 inference(consistent_polarity_flipping,[],[f915])).
% 1.42/0.39 tff(f2076,plain,(
% 1.42/0.39 ( ! [X0 : $int] : (~mem3(X0,sK8(X0),g_s338_329) | $less(X0,1) | $less(g_s336_320,X0)) )),
% 1.42/0.39 inference(consistent_polarity_flipping,[],[f928])).
% 1.42/0.39 tff(f2497,plain,(
% 1.42/0.39 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($remainder_f($sum(X2,X1),$sum(255,1)) = X0 | mem4(X2,X1,X0,g_s58_58)) )),
% 1.42/0.39 inference(consistent_polarity_flipping,[],[f1937])).
% 1.42/0.39 tff(f2560,plain,(
% 1.42/0.39 ( ! [X0 : $int] : (~$less(X0,1) | mem0(X0,g_s306_301)) )),
% 1.42/0.39 inference(consistent_polarity_flipping,[],[f1640])).
% 1.42/0.39 tff(f2715,plain,(
% 1.42/0.39 ~mem0($sum(g_s363_1_354,1),g_s306_301)),
% 1.42/0.39 inference(consistent_polarity_flipping,[],[f2028])).
% 1.42/0.39 tff(f2722,plain,(
% 1.42/0.39 ~sK124 | ~mem0($sum(g_s363_1_354,1),g_s307_302)),
% 1.42/0.39 inference(consistent_polarity_flipping,[],[f2032])).
% 1.42/0.39 tff(f2724,plain,(
% 1.42/0.39 mem0(sK126,g_s307_302)),
% 1.42/0.39 inference(consistent_polarity_flipping,[],[f1838])).
% 1.42/0.39 tff(f2739,plain,(
% 1.42/0.39 ~mem4(g_s363_1_354,1,$sum(g_s363_1_354,1),g_s58_58)),
% 1.42/0.39 inference(consistent_polarity_flipping,[],[f2037])).
% 1.42/0.39 tff(f2740,plain,(
% 1.42/0.39 ~mem4(g_s363_1_354,1,sK135,g_s58_58)),
% 1.42/0.39 inference(consistent_polarity_flipping,[],[f2038])).
% 1.42/0.39 tff(f2741,plain,(
% 1.42/0.39 ~mem4(g_s363_1_354,1,sK134,g_s58_58)),
% 1.42/0.39 inference(consistent_polarity_flipping,[],[f2039])).
% 1.42/0.39 tff(f2747,plain,(
% 1.42/0.39 ( ! [X2 : $int,X0 : $int,X1 : $int] : (mem4(X2,X1,X0,g_s58_58) | $remainder_f($sum(X2,X1),256) = X0) )),
% 1.42/0.39 inference(evaluation,[],[f2497])).
% 1.42/0.39 tff(f2783,definition,(
% 1.42/0.39 spl136_1 <=> $less(sK134,0)),
% 1.42/0.39 introduced(definition,[new_symbols(definition,[spl136_1])],[avatar_definition])).
% 1.42/0.39 tff(f2785,plain,(
% 1.42/0.39 $less(sK134,0) | ~spl136_1),
% 1.42/0.39 inference(avatar_component_clause,[],[f2783])).
% 1.42/0.39 tff(f2787,definition,(
% 1.42/0.39 spl136_2 <=> $less($sum(g_s127_122,1),sK135)),
% 1.42/0.39 introduced(definition,[new_symbols(definition,[spl136_2])],[avatar_definition])).
% 1.42/0.39 tff(f2789,plain,(
% 1.42/0.39 $less($sum(g_s127_122,1),sK135) | ~spl136_2),
% 1.42/0.39 inference(avatar_component_clause,[],[f2787])).
% 1.42/0.39 tff(f2790,plain,(
% 1.42/0.39 spl136_1 | spl136_2),
% 1.42/0.39 inference(avatar_split_clause,[],[f1861,f2787,f2783])).
% 1.42/0.39 tff(f2851,definition,(
% 1.42/0.39 spl136_16 <=> mem0($sum(g_s363_1_354,1),g_s307_302)),
% 1.42/0.39 introduced(definition,[new_symbols(definition,[spl136_16])],[avatar_definition])).
% 1.42/0.39 tff(f2853,plain,(
% 1.42/0.39 ~mem0($sum(g_s363_1_354,1),g_s307_302) | spl136_16),
% 1.42/0.39 inference(avatar_component_clause,[],[f2851])).
% 1.42/0.39 tff(f2859,definition,(
% 1.42/0.39 spl136_18 <=> $sum(g_s363_1_354,1) = sK125),
% 1.42/0.39 introduced(definition,[new_symbols(definition,[spl136_18])],[avatar_definition])).
% 1.42/0.39 tff(f2861,plain,(
% 1.42/0.39 $sum(g_s363_1_354,1) = sK125 | ~spl136_18),
% 1.42/0.39 inference(avatar_component_clause,[],[f2859])).
% 1.42/0.39 tff(f2863,definition,(
% 1.42/0.39 spl136_19 <=> sK124),
% 1.42/0.39 introduced(definition,[new_symbols(definition,[spl136_19])],[avatar_definition])).
% 1.42/0.39 tff(f2866,plain,(
% 1.42/0.39 spl136_18 | spl136_19),
% 1.42/0.39 inference(avatar_split_clause,[],[f1832,f2863,f2859])).
% 1.42/0.39 tff(f2872,plain,(
% 1.42/0.39 ~spl136_16 | ~spl136_19),
% 1.42/0.39 inference(avatar_split_clause,[],[f2722,f2863,f2851])).
% 1.42/0.39 tff(f2889,definition,(
% 1.42/0.39 spl136_24 <=> mem0($sum(g_s363_1_354,1),g_s306_301)),
% 1.42/0.39 introduced(definition,[new_symbols(definition,[spl136_24])],[avatar_definition])).
% 1.42/0.39 tff(f2891,plain,(
% 1.42/0.39 ~mem0($sum(g_s363_1_354,1),g_s306_301) | spl136_24),
% 1.42/0.39 inference(avatar_component_clause,[],[f2889])).
% 1.42/0.39 tff(f2896,plain,(
% 1.42/0.39 ~spl136_24),
% 1.42/0.39 inference(avatar_split_clause,[],[f2715,f2889])).
% 1.42/0.39 tff(f3152,plain,(
% 1.42/0.39 ~mem0(sK126,g_s307_302) | spl136_16),
% 1.42/0.39 inference(forward_demodulation,[],[f2853,f1837])).
% 1.42/0.39 tff(f3153,plain,(
% 1.42/0.39 $false | spl136_16),
% 1.42/0.39 inference(forward_subsumption_resolution,[],[f3152,f2724])).
% 1.42/0.39 tff(f3154,plain,(
% 1.42/0.39 spl136_16),
% 1.42/0.39 inference(avatar_contradiction_clause,[],[f3153])).
% 1.42/0.39 tff(f3156,plain,(
% 1.42/0.39 sK125 = sK126 | ~spl136_18),
% 1.42/0.39 inference(superposition,[],[f2861,f1837])).
% 1.42/0.39 tff(f3161,plain,(
% 1.42/0.39 ~mem0(sK126,g_s306_301) | spl136_24),
% 1.42/0.39 inference(forward_demodulation,[],[f2891,f1837])).
% 1.42/0.39 tff(f3162,plain,(
% 1.42/0.39 ~mem0(sK125,g_s306_301) | (~spl136_18 | spl136_24)),
% 1.42/0.39 inference(forward_demodulation,[],[f3161,f3156])).
% 1.42/0.39 tff(f3189,plain,(
% 1.42/0.39 ~mem4(g_s363_1_354,1,sK126,g_s58_58)),
% 1.42/0.39 inference(forward_demodulation,[],[f2739,f1837])).
% 1.42/0.39 tff(f3190,plain,(
% 1.42/0.39 ~mem4(g_s363_1_354,1,sK125,g_s58_58) | ~spl136_18),
% 1.42/0.39 inference(forward_demodulation,[],[f3189,f3156])).
% 1.42/0.39 tff(f3224,plain,(
% 1.42/0.39 sK125 = $sum(1,g_s363_1_354) | ~spl136_18),
% 1.42/0.39 inference(superposition,[],[f731,f2861])).
% 1.42/0.39 tff(f3406,plain,(
% 1.42/0.39 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(1,X0)) | $less(X0,X1)) )),
% 1.42/0.39 inference(superposition,[],[f740,f731])).
% 1.42/0.39 tff(f3418,plain,(
% 1.42/0.39 ( ! [X0 : $int] : (~$less(X0,sK125) | ~$less(g_s363_1_354,X0)) ) | ~spl136_18),
% 1.42/0.39 inference(superposition,[],[f748,f2861])).
% 1.42/0.39 tff(f3573,plain,(
% 1.42/0.39 ( ! [X0 : $int] : (~$less(X0,$sum(g_s127_122,1)) | $less(X0,sK135)) ) | ~spl136_2),
% 1.42/0.39 inference(resolution,[],[f737,f2789])).
% 1.42/0.39 tff(f3575,plain,(
% 1.42/0.39 ( ! [X0 : $int] : (~$less(X0,$sum(1,g_s127_122)) | $less(X0,sK135)) ) | ~spl136_2),
% 1.42/0.39 inference(forward_demodulation,[],[f3573,f731])).
% 1.42/0.39 tff(f3603,plain,(
% 1.42/0.39 $less(g_s363_1_354,g_s127_122) | g_s127_122 = g_s363_1_354),
% 1.42/0.39 inference(resolution,[],[f738,f1818])).
% 1.42/0.39 tff(f4663,definition,(
% 1.42/0.39 spl136_244 <=> g_s127_122 = g_s363_1_354),
% 1.42/0.39 introduced(definition,[new_symbols(definition,[spl136_244])],[avatar_definition])).
% 1.42/0.39 tff(f4665,plain,(
% 1.42/0.39 g_s127_122 = g_s363_1_354 | ~spl136_244),
% 1.42/0.39 inference(avatar_component_clause,[],[f4663])).
% 1.42/0.39 tff(f4667,definition,(
% 1.42/0.39 spl136_245 <=> $less(g_s363_1_354,g_s127_122)),
% 1.42/0.39 introduced(definition,[new_symbols(definition,[spl136_245])],[avatar_definition])).
% 1.42/0.39 tff(f4669,plain,(
% 1.42/0.39 $less(g_s363_1_354,g_s127_122) | ~spl136_245),
% 1.42/0.39 inference(avatar_component_clause,[],[f4667])).
% 1.42/0.39 tff(f4784,plain,(
% 1.42/0.39 spl136_244 | spl136_245),
% 1.42/0.39 inference(avatar_split_clause,[],[f3603,f4667,f4663])).
% 1.42/0.39 tff(f5018,plain,(
% 1.42/0.39 ( ! [X0 : $int] : (mem3(sK134,X0,g_s338_329)) ) | ~spl136_1),
% 1.42/0.39 inference(resolution,[],[f2785,f2068])).
% 1.42/0.39 tff(f5024,plain,(
% 1.42/0.39 ( ! [X0 : $int] : (~$less(X0,sK134) | $less(X0,0)) ) | ~spl136_1),
% 1.42/0.39 inference(resolution,[],[f2785,f737])).
% 1.42/0.39 tff(f5032,definition,(
% 1.42/0.39 spl136_283 <=> $less(sK135,$sum(1,g_s127_122))),
% 1.42/0.39 introduced(definition,[new_symbols(definition,[spl136_283])],[avatar_definition])).
% 1.42/0.39 tff(f5033,plain,(
% 1.42/0.39 ~$less(sK135,$sum(1,g_s127_122)) | spl136_283),
% 1.42/0.39 inference(avatar_component_clause,[],[f5032])).
% 1.42/0.39 tff(f5034,plain,(
% 1.42/0.39 $less(sK135,$sum(1,g_s127_122)) | ~spl136_283),
% 1.42/0.39 inference(avatar_component_clause,[],[f5032])).
% 1.42/0.39 tff(f5038,plain,(
% 1.42/0.39 $less($sum(1,g_s127_122),sK135) | ~spl136_2),
% 1.42/0.39 inference(forward_demodulation,[],[f2789,f731])).
% 1.42/0.39 tff(f5425,definition,(
% 1.42/0.39 spl136_286 <=> $less(g_s336_320,sK134)),
% 1.42/0.39 introduced(definition,[new_symbols(definition,[spl136_286])],[avatar_definition])).
% 1.42/0.39 tff(f5427,plain,(
% 1.42/0.39 $less(g_s336_320,sK134) | ~spl136_286),
% 1.42/0.39 inference(avatar_component_clause,[],[f5425])).
% 1.42/0.39 tff(f5429,definition,(
% 1.42/0.39 spl136_287 <=> $less(sK134,1)),
% 1.42/0.39 introduced(definition,[new_symbols(definition,[spl136_287])],[avatar_definition])).
% 1.42/0.39 tff(f5431,plain,(
% 1.42/0.39 $less(sK134,1) | ~spl136_287),
% 1.42/0.39 inference(avatar_component_clause,[],[f5429])).
% 1.42/0.39 tff(f5691,plain,(
% 1.42/0.39 sK135 = $remainder_f($sum(g_s363_1_354,1),256)),
% 1.42/0.39 inference(resolution,[],[f2747,f2740])).
% 1.42/0.39 tff(f5692,plain,(
% 1.42/0.39 sK134 = $remainder_f($sum(g_s363_1_354,1),256)),
% 1.42/0.39 inference(resolution,[],[f2747,f2741])).
% 1.42/0.39 tff(f5693,plain,(
% 1.42/0.39 sK125 = $remainder_f($sum(g_s363_1_354,1),256) | ~spl136_18),
% 1.42/0.39 inference(resolution,[],[f2747,f3190])).
% 1.42/0.39 tff(f5696,plain,(
% 1.42/0.39 sK125 = $remainder_f(sK126,256) | ~spl136_18),
% 1.42/0.39 inference(forward_demodulation,[],[f5693,f1837])).
% 1.42/0.39 tff(f5697,plain,(
% 1.42/0.39 sK134 = $remainder_f(sK126,256)),
% 1.42/0.39 inference(forward_demodulation,[],[f5692,f1837])).
% 1.42/0.39 tff(f5698,plain,(
% 1.42/0.39 sK135 = $remainder_f(sK126,256)),
% 1.42/0.39 inference(forward_demodulation,[],[f5691,f1837])).
% 1.42/0.39 tff(f5699,plain,(
% 1.42/0.39 sK125 = $remainder_f(sK125,256) | ~spl136_18),
% 1.42/0.39 inference(forward_demodulation,[],[f5696,f3156])).
% 1.42/0.39 tff(f5700,plain,(
% 1.42/0.39 sK134 = $remainder_f(sK125,256) | ~spl136_18),
% 1.42/0.39 inference(forward_demodulation,[],[f5697,f3156])).
% 1.42/0.39 tff(f5701,plain,(
% 1.42/0.39 sK135 = $remainder_f(sK125,256) | ~spl136_18),
% 1.42/0.39 inference(forward_demodulation,[],[f5698,f3156])).
% 1.42/0.39 tff(f5773,plain,(
% 1.42/0.39 $less(sK134,1) | $less(g_s336_320,sK134) | ~spl136_1),
% 1.42/0.39 inference(resolution,[],[f5018,f2076])).
% 1.42/0.39 tff(f9814,plain,(
% 1.42/0.39 sK134 = sK135 | ~spl136_18),
% 1.42/0.39 inference(forward_demodulation,[],[f5701,f5700])).
% 1.42/0.39 tff(f11075,plain,(
% 1.42/0.39 $less(g_s336_320,0) | (~spl136_1 | ~spl136_286)),
% 1.42/0.39 inference(resolution,[],[f5024,f5427])).
% 1.42/0.39 tff(f11080,plain,(
% 1.42/0.39 $false | (~spl136_1 | ~spl136_286)),
% 1.42/0.39 inference(forward_subsumption_resolution,[],[f11075,f903])).
% 1.42/0.39 tff(f11081,plain,(
% 1.42/0.39 ~spl136_1 | ~spl136_286),
% 1.42/0.39 inference(avatar_contradiction_clause,[],[f11080])).
% 1.42/0.39 tff(f11085,plain,(
% 1.42/0.39 spl136_286 | spl136_287 | ~spl136_1),
% 1.42/0.39 inference(avatar_split_clause,[],[f5773,f2783,f5429,f5425])).
% 1.42/0.39 tff(f11086,plain,(
% 1.42/0.39 ( ! [X0 : $int] : (~$less(X0,$sum(1,g_s127_122)) | $less(X0,sK134)) ) | (~spl136_2 | ~spl136_18)),
% 1.42/0.39 inference(forward_demodulation,[],[f3575,f9814])).
% 1.42/0.39 tff(f11096,plain,(
% 1.42/0.39 mem0(sK134,g_s306_301) | ~spl136_287),
% 1.42/0.39 inference(resolution,[],[f5431,f2560])).
% 1.42/0.39 tff(f11228,plain,(
% 1.42/0.39 $less($sum(1,g_s363_1_354),sK135) | (~spl136_2 | ~spl136_244)),
% 1.42/0.39 inference(superposition,[],[f5038,f4665])).
% 1.42/0.39 tff(f11234,plain,(
% 1.42/0.39 $less($sum(1,g_s363_1_354),sK134) | (~spl136_2 | ~spl136_18 | ~spl136_244)),
% 1.42/0.39 inference(forward_demodulation,[],[f11228,f9814])).
% 1.42/0.39 tff(f11237,plain,(
% 1.42/0.39 $less(sK125,sK134) | (~spl136_2 | ~spl136_18 | ~spl136_244)),
% 1.42/0.39 inference(forward_demodulation,[],[f11234,f3224])).
% 1.42/0.39 tff(f11244,plain,(
% 1.42/0.39 ( ! [X0 : $int] : ($less($sum(sK125,X0),$sum(sK134,X0))) ) | (~spl136_2 | ~spl136_18 | ~spl136_244)),
% 1.42/0.39 inference(resolution,[],[f11237,f739])).
% 1.42/0.39 tff(f13061,plain,(
% 1.42/0.39 sK125 = sK134 | ~spl136_18),
% 1.42/0.39 inference(superposition,[],[f5699,f5700])).
% 1.42/0.39 tff(f13177,plain,(
% 1.42/0.39 mem0(sK125,g_s306_301) | (~spl136_18 | ~spl136_287)),
% 1.42/0.39 inference(superposition,[],[f11096,f13061])).
% 1.42/0.39 tff(f13201,plain,(
% 1.42/0.39 $false | (~spl136_18 | spl136_24 | ~spl136_287)),
% 1.42/0.39 inference(forward_subsumption_resolution,[],[f13177,f3162])).
% 1.42/0.39 tff(f13202,plain,(
% 1.42/0.39 ~spl136_18 | spl136_24 | ~spl136_287),
% 1.42/0.39 inference(avatar_contradiction_clause,[],[f13201])).
% 1.42/0.39 tff(f13531,plain,(
% 1.42/0.39 $less(sK134,$sum(1,g_s127_122)) | (~spl136_18 | ~spl136_283)),
% 1.42/0.39 inference(forward_demodulation,[],[f5034,f9814])).
% 1.42/0.39 tff(f13569,plain,(
% 1.42/0.39 ( ! [X0 : $int] : (~$less(X0,$sum(1,g_s127_122)) | $less(X0,sK125)) ) | (~spl136_2 | ~spl136_18)),
% 1.42/0.39 inference(forward_demodulation,[],[f11086,f13061])).
% 1.42/0.39 tff(f13575,plain,(
% 1.42/0.39 $less(sK125,$sum(1,g_s127_122)) | (~spl136_18 | ~spl136_283)),
% 1.42/0.39 inference(forward_demodulation,[],[f13531,f13061])).
% 1.42/0.39 tff(f13671,definition,(
% 1.42/0.39 spl136_1209 <=> $less(g_s127_122,sK125)),
% 1.42/0.39 introduced(definition,[new_symbols(definition,[spl136_1209])],[avatar_definition])).
% 1.42/0.39 tff(f13673,plain,(
% 1.42/0.39 $less(g_s127_122,sK125) | ~spl136_1209),
% 1.42/0.39 inference(avatar_component_clause,[],[f13671])).
% 1.42/0.39 tff(f13713,plain,(
% 1.42/0.39 ~$less(sK134,$sum(1,g_s127_122)) | (~spl136_18 | spl136_283)),
% 1.42/0.39 inference(forward_demodulation,[],[f5033,f9814])).
% 1.42/0.39 tff(f13714,plain,(
% 1.42/0.39 ~$less(sK125,$sum(1,g_s127_122)) | (~spl136_18 | spl136_283)),
% 1.42/0.39 inference(forward_demodulation,[],[f13713,f13061])).
% 1.42/0.39 tff(f13950,plain,(
% 1.42/0.39 ( ! [X0 : $int] : ($less($sum(sK125,X0),$sum(sK125,X0))) ) | (~spl136_2 | ~spl136_18 | ~spl136_244)),
% 1.42/0.39 inference(forward_demodulation,[],[f11244,f13061])).
% 1.42/0.39 tff(f13973,plain,(
% 1.42/0.39 $false | (~spl136_2 | ~spl136_18 | ~spl136_244)),
% 1.42/0.39 inference(forward_subsumption_resolution,[],[f13950,f736])).
% 1.42/0.39 tff(f13974,plain,(
% 1.42/0.39 ~spl136_2 | ~spl136_18 | ~spl136_244),
% 1.42/0.39 inference(avatar_contradiction_clause,[],[f13973])).
% 1.42/0.39 tff(f21269,plain,(
% 1.42/0.39 $less(sK125,sK125) | (~spl136_2 | ~spl136_18 | ~spl136_283)),
% 1.42/0.39 inference(resolution,[],[f13569,f13575])).
% 1.42/0.39 tff(f21270,plain,(
% 1.42/0.39 $false | (~spl136_2 | ~spl136_18 | ~spl136_283)),
% 1.42/0.39 inference(forward_subsumption_resolution,[],[f21269,f736])).
% 1.42/0.39 tff(f21271,plain,(
% 1.42/0.39 ~spl136_2 | ~spl136_18 | ~spl136_283),
% 1.42/0.39 inference(avatar_contradiction_clause,[],[f21270])).
% 1.42/0.39 tff(f21274,plain,(
% 1.42/0.39 $less(g_s127_122,sK125) | (~spl136_18 | spl136_283)),
% 1.42/0.39 inference(resolution,[],[f13714,f3406])).
% 1.42/0.39 tff(f21870,plain,(
% 1.42/0.39 ~$less(g_s363_1_354,g_s127_122) | (~spl136_18 | ~spl136_1209)),
% 1.42/0.39 inference(resolution,[],[f3418,f13673])).
% 1.42/0.39 tff(f21876,plain,(
% 1.42/0.39 $false | (~spl136_18 | ~spl136_245 | ~spl136_1209)),
% 1.42/0.39 inference(forward_subsumption_resolution,[],[f21870,f4669])).
% 1.42/0.39 tff(f21877,plain,(
% 1.42/0.39 ~spl136_18 | ~spl136_245 | ~spl136_1209),
% 1.42/0.39 inference(avatar_contradiction_clause,[],[f21876])).
% 1.42/0.39 tff(f21889,plain,(
% 1.42/0.39 spl136_1209 | ~spl136_18 | spl136_283),
% 1.42/0.39 inference(avatar_split_clause,[],[f21274,f5032,f2859,f13671])).
% 1.42/0.39 cnf(s1, plain, spl136_1 | spl136_2, inference(sat_conversion,[],[f2790])).
% 1.42/0.39 cnf(s13, plain, spl136_18 | spl136_19, inference(sat_conversion,[],[f2866])).
% 1.42/0.39 cnf(s15, plain, ~spl136_16 | ~spl136_19, inference(sat_conversion,[],[f2872])).
% 1.42/0.39 cnf(s21, plain, ~spl136_24, inference(sat_conversion,[],[f2896])).
% 1.42/0.39 cnf(s76, plain, spl136_16, inference(sat_conversion,[],[f3154])).
% 1.42/0.39 cnf(s256, plain, spl136_244 | spl136_245, inference(sat_conversion,[],[f4784])).
% 1.42/0.39 cnf(s930, plain, ~spl136_1 | ~spl136_286, inference(sat_conversion,[],[f11081])).
% 1.42/0.39 cnf(s933, plain, ~spl136_1 | spl136_286 | spl136_287, inference(sat_conversion,[],[f11085])).
% 1.42/0.39 cnf(s1134, plain, ~spl136_18 | spl136_24 | ~spl136_287, inference(sat_conversion,[],[f13202])).
% 1.42/0.39 cnf(s1225, plain, ~spl136_2 | ~spl136_18 | ~spl136_244, inference(sat_conversion,[],[f13974])).
% 1.42/0.39 cnf(s2065, plain, ~spl136_2 | ~spl136_18 | ~spl136_283, inference(sat_conversion,[],[f21271])).
% 1.42/0.39 cnf(s2078, plain, ~spl136_18 | ~spl136_245 | ~spl136_1209, inference(sat_conversion,[],[f21877])).
% 1.42/0.39 cnf(s2084, plain, ~spl136_18 | spl136_283 | spl136_1209, inference(sat_conversion,[],[f21889])).
% 1.42/0.39 cnf(s2180, plain, ~spl136_19, inference(rat,[],[s15,s76])).
% 1.42/0.39 cnf(s2185, plain, spl136_18, inference(rat,[],[s13,s2180])).
% 1.42/0.39 cnf(s2188, plain, ~spl136_287, inference(rat,[],[s1134,s21,s2185])).
% 1.42/0.39 cnf(s2205, plain, ~spl136_2, inference(rat,[],[s2078,s256,s2084,s1225,s2065,s2185])).
% 1.42/0.39 cnf(s2206, plain, spl136_1, inference(rat,[],[s1,s2205])).
% 1.42/0.39 cnf(s2207, plain, spl136_286, inference(rat,[],[s933,s2188,s2206])).
% 1.42/0.39 cnf(s2208, plain, $false, inference(rat,[],[s930,s2207,s2206])).
% 1.42/0.39 tff(f21958,plain,(
% 1.42/0.39 $false),
% 1.42/0.39 inference(avatar_sat_refutation,[],[s2208])).
% 1.42/0.39 % SZS output end Proof for theBenchmark
% 1.42/0.39 % (3265550)------------------------------
% 1.42/0.39 % (3265550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.39 % (3265550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.39 % (3265550)CaDiCaL version: 2.1.3
% 1.42/0.39 % (3265550)Termination reason: Refutation
% 1.42/0.39 % (3265550)Time elapsed: 0.237 s
% 1.42/0.39 % (3265550)Peak memory usage: 23 MB
% 1.42/0.39 % (3265550)Instructions burned: 768 (million)
% 1.42/0.39 % (3265544)Success in time 0.259 s
% 1.42/0.39 % Vampire exiting
%------------------------------------------------------------------------------