%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW631_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n019.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:40:33 PM UTC 2026
% Result : Theorem 38.81s 5.95s
% Output : Refutation 38.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW631_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.25/0.27 % Computer : n019.cluster.edu
% 0.25/0.27 % Model : x86_64 x86_64
% 0.25/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.25/0.27 % Memory : 8046.5625MB
% 0.25/0.27 % OS : Linux 6.8.0-71-generic
% 0.25/0.27 % CPULimit : 300
% 0.25/0.27 % WCLimit : 300
% 0.25/0.27 % DateTime : Mon Sep 28 14:23:18 UTC 2026
% 0.25/0.28 % CPUTime :
% 0.25/0.28 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.25/0.32 Running first-order model finding
% 0.25/0.32 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
% 6.74/1.38 % (4031061)Will run a generic schedule for satisfiability detection.
% 6.74/1.38 % (4031071)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1321407710:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.74/1.38 % (4031067)% WARNING: option uhcvi not known.
% 6.74/1.38 % (4031072)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4020974935:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.74/1.38 % (4031069)dis+10_1_sil=32000:sp=arity:random_seed=2651421653:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.74/1.38 % (4031070)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3340972406:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.74/1.38 % (4031066)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=647969200_2999 on theBenchmark for (2999ds/0Mi)
% 6.74/1.38 % (4031067)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3307541928:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.74/1.38 % (4031068)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1199863744:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.74/1.38 % (4031066)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.74/1.38 % (4031066)Terminated due to inappropriate strategy.
% 6.74/1.38 % (4031066)------------------------------
% 6.74/1.38 % (4031066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.38 % (4031066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.38 % (4031066)CaDiCaL version: 2.1.3
% 6.74/1.38 % (4031066)Termination reason: Inappropriate
% 6.74/1.38 % (4031066)Time elapsed: 0.006 s
% 6.74/1.38 % (4031066)Peak memory usage: 10 MB
% 6.74/1.38 % (4031066)Instructions burned: 5 (million)
% 6.74/1.38 % (4031066)------------------------------
% 6.74/1.38 % (4031066)------------------------------
% 6.74/1.38 % (4031080)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2723671258:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.74/1.38 % (4031080)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.74/1.38 % (4031080)Terminated due to inappropriate strategy.
% 6.74/1.38 % (4031080)------------------------------
% 6.74/1.38 % (4031080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.38 % (4031080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.38 % (4031080)CaDiCaL version: 2.1.3
% 6.74/1.38 % (4031080)Termination reason: Inappropriate
% 6.74/1.38 % (4031080)Time elapsed: 0.003 s
% 6.74/1.38 % (4031080)Peak memory usage: 11 MB
% 6.74/1.38 % (4031080)Instructions burned: 5 (million)
% 6.74/1.38 % (4031080)------------------------------
% 6.74/1.38 % (4031080)------------------------------
% 6.74/1.38 % (4031082)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3995549571:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.74/1.38 % (4031071)Instruction limit reached!
% 6.74/1.38 % (4031071)------------------------------
% 6.74/1.38 % (4031071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.38 % (4031071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.38 % (4031071)CaDiCaL version: 2.1.3
% 6.74/1.38 % (4031071)Termination reason: Instruction limit
% 6.74/1.38 % (4031071)Termination phase: Saturation
% 6.74/1.38 % (4031071)Time elapsed: 0.072 s
% 6.74/1.38 % (4031071)Peak memory usage: 13 MB
% 6.74/1.38 % (4031071)Instructions burned: 131 (million)
% 6.74/1.38 % (4031084)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=3740515809:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 6.74/1.38 % (4031069)Instruction limit reached!
% 6.74/1.38 % (4031069)------------------------------
% 6.74/1.38 % (4031069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.74/1.38 % (4031069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.74/1.38 % (4031069)CaDiCaL version: 2.1.3
% 6.74/1.38 % (4031069)Termination reason: Instruction limit
% 6.74/1.38 % (4031069)Termination phase: Saturation
% 6.74/1.38 % (4031069)Time elapsed: 0.108 s
% 6.74/1.38 % (4031069)Peak memory usage: 13 MB
% 6.74/1.38 % (4031069)Instructions burned: 104 (million)
% 6.74/1.38 % (4031070)Instruction limit reached!
% 6.74/1.38 % (4031070)------------------------------
% 6.74/1.38 % (4031070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.14/1.81 % (4031070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.14/1.81 % (4031070)CaDiCaL version: 2.1.3
% 9.14/1.81 % (4031070)Termination reason: Instruction limit
% 9.14/1.81 % (4031070)Termination phase: Saturation
% 9.14/1.81 % (4031070)Time elapsed: 0.121 s
% 9.14/1.81 % (4031070)Peak memory usage: 13 MB
% 9.14/1.81 % (4031070)Instructions burned: 116 (million)
% 9.14/1.81 % (4031086)ott-21_1_sil=16000:fs=off:random_seed=2584375752:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 9.14/1.81 % (4031072)Instruction limit reached!
% 9.14/1.81 % (4031072)------------------------------
% 9.14/1.81 % (4031072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.14/1.81 % (4031072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.14/1.81 % (4031072)CaDiCaL version: 2.1.3
% 9.14/1.81 % (4031072)Termination reason: Instruction limit
% 9.14/1.81 % (4031072)Termination phase: Saturation
% 9.14/1.81 % (4031072)Time elapsed: 0.152 s
% 9.14/1.81 % (4031072)Peak memory usage: 13 MB
% 9.14/1.81 % (4031072)Instructions burned: 159 (million)
% 9.14/1.81 % (4031087)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2724000241:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 9.14/1.81 % (4031089)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3213306853:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 9.14/1.81 % (4031089)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 9.14/1.81 % (4031089)Terminated due to inappropriate strategy.
% 9.14/1.81 % (4031089)------------------------------
% 9.14/1.81 % (4031089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.14/1.81 % (4031089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.14/1.81 % (4031089)CaDiCaL version: 2.1.3
% 9.14/1.81 % (4031089)Termination reason: Inappropriate
% 9.14/1.81 % (4031089)Time elapsed: 0.004 s
% 9.14/1.81 % (4031089)Peak memory usage: 11 MB
% 9.14/1.81 % (4031089)Instructions burned: 5 (million)
% 9.14/1.81 % (4031089)------------------------------
% 9.14/1.81 % (4031089)------------------------------
% 9.14/1.81 % (4031092)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2045840197:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 9.14/1.81 % (4031082)Instruction limit reached!
% 9.14/1.81 % (4031082)------------------------------
% 9.14/1.81 % (4031082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.14/1.81 % (4031082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.14/1.81 % (4031082)CaDiCaL version: 2.1.3
% 9.14/1.81 % (4031082)Termination reason: Instruction limit
% 9.14/1.81 % (4031082)Termination phase: Saturation
% 9.14/1.81 % (4031082)Time elapsed: 0.166 s
% 9.14/1.81 % (4031082)Peak memory usage: 13 MB
% 9.14/1.81 % (4031082)Instructions burned: 131 (million)
% 9.14/1.81 % (4031094)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=453765984:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 9.14/1.81 % (4031094)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 9.14/1.81 % (4031094)Terminated due to inappropriate strategy.
% 9.14/1.81 % (4031094)------------------------------
% 9.14/1.81 % (4031094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.14/1.81 % (4031094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.14/1.81 % (4031094)CaDiCaL version: 2.1.3
% 9.14/1.81 % (4031094)Termination reason: Inappropriate
% 9.14/1.81 % (4031094)Time elapsed: 0.005 s
% 9.14/1.81 % (4031094)Peak memory usage: 10 MB
% 9.14/1.81 % (4031094)Instructions burned: 5 (million)
% 9.14/1.81 % (4031094)------------------------------
% 9.14/1.81 % (4031094)------------------------------
% 9.14/1.81 % (4031096)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=3148402483:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 9.14/1.81 % (4031086)Instruction limit reached!
% 9.14/1.81 % (4031086)------------------------------
% 9.14/1.81 % (4031086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.14/1.81 % (4031086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.14/1.81 % (4031086)CaDiCaL version: 2.1.3
% 9.14/1.81 % (4031086)Termination reason: Instruction limit
% 9.14/1.81 % (4031086)Termination phase: Saturation
% 32.04/5.03 % (4031086)Time elapsed: 0.162 s
% 32.04/5.03 % (4031086)Peak memory usage: 13 MB
% 32.04/5.03 % (4031086)Instructions burned: 181 (million)
% 32.04/5.03 % (4031098)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1838291797:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 32.04/5.03 % (4031084)Instruction limit reached!
% 32.04/5.03 % (4031084)------------------------------
% 32.04/5.03 % (4031084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.04/5.03 % (4031084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.04/5.03 % (4031084)CaDiCaL version: 2.1.3
% 32.04/5.03 % (4031084)Termination reason: Instruction limit
% 32.04/5.03 % (4031084)Termination phase: Saturation
% 32.04/5.03 % (4031084)Time elapsed: 0.341 s
% 32.04/5.03 % (4031084)Peak memory usage: 16 MB
% 32.04/5.03 % (4031084)Instructions burned: 685 (million)
% 32.04/5.03 % (4031100)fmb+10_1_sil=64000:random_seed=1616581162:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 32.04/5.03 % (4031100)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 32.04/5.03 % (4031100)Terminated due to inappropriate strategy.
% 32.04/5.03 % (4031100)------------------------------
% 32.04/5.03 % (4031100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.04/5.03 % (4031100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.04/5.03 % (4031100)CaDiCaL version: 2.1.3
% 32.04/5.03 % (4031100)Termination reason: Inappropriate
% 32.04/5.03 % (4031100)Time elapsed: 0.003 s
% 32.04/5.03 % (4031100)Peak memory usage: 11 MB
% 32.04/5.03 % (4031100)Instructions burned: 5 (million)
% 32.04/5.03 % (4031100)------------------------------
% 32.04/5.03 % (4031100)------------------------------
% 32.04/5.03 % (4031102)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2679124110:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 32.04/5.03 % (4031102)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 32.04/5.03 % (4031102)Terminated due to inappropriate strategy.
% 32.04/5.03 % (4031102)------------------------------
% 32.04/5.03 % (4031102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.04/5.03 % (4031102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.04/5.03 % (4031102)CaDiCaL version: 2.1.3
% 32.04/5.03 % (4031102)Termination reason: Inappropriate
% 32.04/5.03 % (4031102)Time elapsed: 0.003 s
% 32.04/5.03 % (4031102)Peak memory usage: 11 MB
% 32.04/5.03 % (4031102)Instructions burned: 5 (million)
% 32.04/5.03 % (4031102)------------------------------
% 32.04/5.03 % (4031102)------------------------------
% 32.04/5.03 % (4031104)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1904884662:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 32.04/5.03 % (4031104)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 32.04/5.03 % (4031104)Terminated due to inappropriate strategy.
% 32.04/5.03 % (4031104)------------------------------
% 32.04/5.03 % (4031104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.04/5.03 % (4031104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.04/5.03 % (4031104)CaDiCaL version: 2.1.3
% 32.04/5.03 % (4031104)Termination reason: Inappropriate
% 32.04/5.03 % (4031104)Time elapsed: 0.004 s
% 32.04/5.03 % (4031104)Peak memory usage: 11 MB
% 32.04/5.03 % (4031104)Instructions burned: 5 (million)
% 32.04/5.03 % (4031104)------------------------------
% 32.04/5.03 % (4031104)------------------------------
% 32.04/5.03 % (4031106)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3458953621:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 32.04/5.03 % (4031087)Instruction limit reached!
% 32.04/5.03 % (4031087)------------------------------
% 32.04/5.03 % (4031087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.04/5.03 % (4031087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.04/5.03 % (4031087)CaDiCaL version: 2.1.3
% 32.04/5.03 % (4031087)Termination reason: Instruction limit
% 32.04/5.03 % (4031087)Termination phase: Saturation
% 32.04/5.03 % (4031087)Time elapsed: 0.513 s
% 32.04/5.03 % (4031087)Peak memory usage: 14 MB
% 32.04/5.03 % (4031087)Instructions burned: 477 (million)
% 32.04/5.03 % (4031108)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=216540324:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 32.04/5.03 % (4031096)Instruction limit reached!
% 32.04/5.03 % (4031096)------------------------------
% 38.81/5.95 % (4031096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.81/5.95 % (4031096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.81/5.95 % (4031096)CaDiCaL version: 2.1.3
% 38.81/5.95 % (4031096)Termination reason: Instruction limit
% 38.81/5.95 % (4031096)Termination phase: Saturation
% 38.81/5.95 % (4031096)Time elapsed: 0.716 s
% 38.81/5.95 % (4031096)Peak memory usage: 19 MB
% 38.81/5.95 % (4031096)Instructions burned: 693 (million)
% 38.81/5.95 % (4031110)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4245727978:i=6324_2989 on theBenchmark for (2989ds/6324Mi)
% 38.81/5.95 % (4031110)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 38.81/5.95 % (4031110)Terminated due to inappropriate strategy.
% 38.81/5.95 % (4031110)------------------------------
% 38.81/5.95 % (4031110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.81/5.95 % (4031110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.81/5.95 % (4031110)CaDiCaL version: 2.1.3
% 38.81/5.95 % (4031110)Termination reason: Inappropriate
% 38.81/5.95 % (4031110)Time elapsed: 0.007 s
% 38.81/5.95 % (4031110)Peak memory usage: 11 MB
% 38.81/5.95 % (4031110)Instructions burned: 5 (million)
% 38.81/5.95 % (4031110)------------------------------
% 38.81/5.95 % (4031110)------------------------------
% 38.81/5.95 % (4031112)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1610409009:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi)
% 38.81/5.95 % (4031112)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 38.81/5.95 % (4031112)Terminated due to inappropriate strategy.
% 38.81/5.95 % (4031112)------------------------------
% 38.81/5.95 % (4031112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.81/5.95 % (4031112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.81/5.95 % (4031112)CaDiCaL version: 2.1.3
% 38.81/5.95 % (4031112)Termination reason: Inappropriate
% 38.81/5.95 % (4031112)Time elapsed: 0.003 s
% 38.81/5.95 % (4031112)Peak memory usage: 11 MB
% 38.81/5.95 % (4031112)Instructions burned: 5 (million)
% 38.81/5.95 % (4031112)------------------------------
% 38.81/5.95 % (4031112)------------------------------
% 38.81/5.95 % (4031114)ott-2_1_sil=16000:newcnf=on:random_seed=1426855328:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi)
% 38.81/5.95 % (4031098)Instruction limit reached!
% 38.81/5.95 % (4031098)------------------------------
% 38.81/5.95 % (4031098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.81/5.95 % (4031098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.81/5.95 % (4031098)CaDiCaL version: 2.1.3
% 38.81/5.95 % (4031098)Termination reason: Instruction limit
% 38.81/5.95 % (4031098)Termination phase: Saturation
% 38.81/5.95 % (4031098)Time elapsed: 0.794 s
% 38.81/5.95 % (4031098)Peak memory usage: 18 MB
% 38.81/5.95 % (4031098)Instructions burned: 879 (million)
% 38.81/5.95 % (4031116)ott+10_1_sil=32000:tgt=ground:random_seed=2575036618:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi)
% 38.81/5.95 % (4031092)Instruction limit reached!
% 38.81/5.95 % (4031092)------------------------------
% 38.81/5.95 % (4031092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.81/5.95 % (4031092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.81/5.95 % (4031092)CaDiCaL version: 2.1.3
% 38.81/5.95 % (4031092)Termination reason: Instruction limit
% 38.81/5.95 % (4031092)Termination phase: Saturation
% 38.81/5.95 % (4031092)Time elapsed: 1.194 s
% 38.81/5.95 % (4031092)Peak memory usage: 20 MB
% 38.81/5.95 % (4031092)Instructions burned: 1179 (million)
% 38.81/5.95 % (4031119)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=829527322:i=54282_2985 on theBenchmark for (2985ds/54282Mi)
% 38.81/5.95 % (4031119)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 38.81/5.95 % (4031119)Terminated due to inappropriate strategy.
% 38.81/5.95 % (4031119)------------------------------
% 38.81/5.95 % (4031119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.81/5.95 % (4031119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.81/5.95 % (4031119)CaDiCaL version: 2.1.3
% 38.81/5.95 % (4031119)Termination reason: Inappropriate
% 38.81/5.95 % (4031119)Time elapsed: 0.003 s
% 38.81/5.95 % (4031119)Peak memory usage: 11 MB
% 38.81/5.95 % (4031119)Instructions burned: 5 (million)
% 38.81/5.95 % (4031119)------------------------------
% 38.81/5.95 % (4031119)------------------------------
% 38.81/5.95 % (4031122)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1945545641:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi)
% 38.81/5.95 % (4031114)Instruction limit reached!
% 38.81/5.95 % (4031114)------------------------------
% 38.81/5.95 % (4031114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.81/5.95 % (4031114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.81/5.95 % (4031114)CaDiCaL version: 2.1.3
% 38.81/5.95 % (4031114)Termination reason: Instruction limit
% 38.81/5.95 % (4031114)Termination phase: Saturation
% 38.81/5.95 % (4031114)Time elapsed: 0.852 s
% 38.81/5.95 % (4031114)Peak memory usage: 18 MB
% 38.81/5.95 % (4031114)Instructions burned: 869 (million)
% 38.81/5.95 % (4031124)dis+21_1_sil=32000:sas=cadical:random_seed=3521518304:i=3773:amm=off_2979 on theBenchmark for (2979ds/3773Mi)
% 38.81/5.95 % (4031108)Instruction limit reached!
% 38.81/5.95 % (4031108)------------------------------
% 38.81/5.95 % (4031108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.81/5.95 % (4031108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.81/5.95 % (4031108)CaDiCaL version: 2.1.3
% 38.81/5.95 % (4031108)Termination reason: Instruction limit
% 38.81/5.95 % (4031108)Termination phase: Saturation
% 38.81/5.95 % (4031108)Time elapsed: 1.379 s
% 38.81/5.95 % (4031108)Peak memory usage: 29 MB
% 38.81/5.95 % (4031108)Instructions burned: 1472 (million)
% 38.81/5.95 % (4031127)ott+11_1_sil=16000:gs=on:random_seed=1589989666:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi)
% 38.81/5.95 % (4031127)Instruction limit reached!
% 38.81/5.95 % (4031127)------------------------------
% 38.81/5.95 % (4031127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.81/5.95 % (4031127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.81/5.95 % (4031127)CaDiCaL version: 2.1.3
% 38.81/5.95 % (4031127)Termination reason: Instruction limit
% 38.81/5.95 % (4031127)Termination phase: Saturation
% 38.81/5.95 % (4031127)Time elapsed: 1.259 s
% 38.81/5.95 % (4031127)Peak memory usage: 26 MB
% 38.81/5.95 % (4031127)Instructions burned: 2253 (million)
% 38.81/5.95 % (4031134)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1974678498:fmbsr=1.6:i=67534_2966 on theBenchmark for (2966ds/67534Mi)
% 38.81/5.95 % (4031134)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 38.81/5.95 % (4031134)Terminated due to inappropriate strategy.
% 38.81/5.95 % (4031134)------------------------------
% 38.81/5.95 % (4031134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.81/5.95 % (4031134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.81/5.95 % (4031134)CaDiCaL version: 2.1.3
% 38.81/5.95 % (4031134)Termination reason: Inappropriate
% 38.81/5.95 % (4031134)Time elapsed: 0.003 s
% 38.81/5.95 % (4031134)Peak memory usage: 11 MB
% 38.81/5.95 % (4031134)Instructions burned: 5 (million)
% 38.81/5.95 % (4031134)------------------------------
% 38.81/5.95 % (4031134)------------------------------
% 38.81/5.95 % (4031136)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2093139376:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2965 on theBenchmark for (2965ds/4591Mi)
% 38.81/5.95 % (4031106)Instruction limit reached!
% 38.81/5.95 % (4031106)------------------------------
% 38.81/5.95 % (4031106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.81/5.95 % (4031106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.81/5.95 % (4031106)CaDiCaL version: 2.1.3
% 38.81/5.95 % (4031106)Termination reason: Instruction limit
% 38.81/5.95 % (4031106)Termination phase: Saturation
% 38.81/5.95 % (4031106)Time elapsed: 3.433 s
% 38.81/5.95 % (4031106)Peak memory usage: 30 MB
% 38.81/5.95 % (4031106)Instructions burned: 5131 (million)
% 38.81/5.95 % (4031138)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2068119174:i=29340_2959 on theBenchmark for (2959ds/29340Mi)
% 38.81/5.95 % (4031122)Instruction limit reached!
% 38.81/5.95 % (4031122)------------------------------
% 38.81/5.95 % (4031122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.81/5.95 % (4031122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.81/5.95 % (4031122)CaDiCaL version: 2.1.3
% 38.81/5.95 % (4031122)Termination reason: Instruction limit
% 38.81/5.95 % (4031122)Termination phase: Saturation
% 38.81/5.95 % (4031122)Time elapsed: 3.191 s
% 38.81/5.95 % (4031122)Peak memory usage: 30 MB
% 38.81/5.95 % (4031122)Instructions burned: 3513 (million)
% 38.81/5.95 % (4031154)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4114214674:i=5211_2952 on theBenchmark for (2952ds/5211Mi)
% 38.81/5.95 % (4031116) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4031061-4031116"...
% 38.81/5.95 % (4031116)...printing done.
% 38.81/5.95 % (4031116)Refutation found. Thanks to Tanya!
% 38.81/5.95 % SZS status Theorem for theBenchmark
% 38.81/5.95 % SZS output start Proof for theBenchmark
% 38.81/5.95 tff(type_def_5, type, uni: $tType).
% 38.81/5.95 tff(type_def_6, type, ty: $tType).
% 38.81/5.95 tff(type_def_7, type, bool: $tType).
% 38.81/5.95 tff(type_def_8, type, tuple0: $tType).
% 38.81/5.95 tff(type_def_9, type, map_int_int: $tType).
% 38.81/5.95 tff(func_def_0, type, witness: ty > uni).
% 38.81/5.95 tff(func_def_1, type, int: ty).
% 38.81/5.95 tff(func_def_2, type, real: ty).
% 38.81/5.95 tff(func_def_3, type, bool1: ty).
% 38.81/5.95 tff(func_def_4, type, true: bool).
% 38.81/5.95 tff(func_def_5, type, false: bool).
% 38.81/5.95 tff(func_def_6, type, match_bool: (ty * bool * uni * uni) > uni).
% 38.81/5.95 tff(func_def_7, type, tuple01: ty).
% 38.81/5.95 tff(func_def_8, type, tuple02: tuple0).
% 38.81/5.95 tff(func_def_9, type, qtmark: ty).
% 38.81/5.95 tff(func_def_12, type, ref: ty > ty).
% 38.81/5.95 tff(func_def_13, type, mk_ref: (ty * uni) > uni).
% 38.81/5.95 tff(func_def_14, type, contents: (ty * uni) > uni).
% 38.81/5.95 tff(func_def_15, type, map: (ty * ty) > ty).
% 38.81/5.95 tff(func_def_16, type, get: (ty * ty * uni * uni) > uni).
% 38.81/5.95 tff(func_def_17, type, set: (ty * ty * uni * uni * uni) > uni).
% 38.81/5.95 tff(func_def_18, type, const: (ty * ty * uni) > uni).
% 38.81/5.95 tff(func_def_19, type, array: ty > ty).
% 38.81/5.95 tff(func_def_20, type, mk_array: (ty * $int * uni) > uni).
% 38.81/5.95 tff(func_def_21, type, length: (ty * uni) > $int).
% 38.81/5.95 tff(func_def_22, type, elts: (ty * uni) > uni).
% 38.81/5.95 tff(func_def_23, type, get1: (ty * uni * $int) > uni).
% 38.81/5.95 tff(func_def_24, type, t2tb: $int > uni).
% 38.81/5.95 tff(func_def_25, type, tb2t: uni > $int).
% 38.81/5.95 tff(func_def_26, type, set1: (ty * uni * $int * uni) > uni).
% 38.81/5.95 tff(func_def_27, type, make: (ty * $int * uni) > uni).
% 38.81/5.95 tff(func_def_28, type, n: $int).
% 38.81/5.95 tff(func_def_29, type, f: $int > $int).
% 38.81/5.95 tff(func_def_32, type, t2tb1: map_int_int > uni).
% 38.81/5.95 tff(func_def_33, type, tb2t1: uni > map_int_int).
% 38.81/5.95 tff(func_def_36, type, sK1: ($int * $int) > $int).
% 38.81/5.95 tff(func_def_37, type, sK2: ($int * $int) > $int).
% 38.81/5.95 tff(func_def_38, type, sK3: ($int * $int) > $int).
% 38.81/5.95 tff(func_def_39, type, sK4: map_int_int).
% 38.81/5.95 tff(func_def_40, type, sK5: $int).
% 38.81/5.95 tff(func_def_41, type, sK6: map_int_int).
% 38.81/5.95 tff(func_def_42, type, sK7: map_int_int).
% 38.81/5.95 tff(func_def_43, type, sK8: $int).
% 38.81/5.95 tff(func_def_44, type, sK9: $int).
% 38.81/5.95 tff(func_def_45, type, sK10: $int).
% 38.81/5.95 tff(func_def_46, type, sK11: $int).
% 38.81/5.95 tff(func_def_47, type, sK12: $int).
% 38.81/5.95 tff(func_def_48, type, sK13: $int).
% 38.81/5.95 tff(func_def_49, type, sF14: uni).
% 38.81/5.95 tff(func_def_50, type, sF15: uni).
% 38.81/5.95 tff(func_def_51, type, sF16: uni).
% 38.81/5.95 tff(func_def_52, type, sF17: $int).
% 38.81/5.95 tff(func_def_53, type, sF18: uni).
% 38.81/5.95 tff(func_def_54, type, sF19: uni).
% 38.81/5.95 tff(func_def_55, type, sF20: $int).
% 38.81/5.95 tff(func_def_56, type, sF21: uni).
% 38.81/5.95 tff(func_def_57, type, sF22: uni).
% 38.81/5.95 tff(func_def_58, type, sF23: uni).
% 38.81/5.95 tff(func_def_59, type, sF24: $int).
% 38.81/5.95 tff(func_def_60, type, sF25: $int).
% 38.81/5.95 tff(func_def_61, type, sF26: $int).
% 38.81/5.95 tff(func_def_62, type, sF27: $int).
% 38.81/5.95 tff(func_def_63, type, sF28: $int).
% 38.81/5.95 tff(func_def_64, type, sF29: uni).
% 38.81/5.95 tff(func_def_65, type, sF30: $int).
% 38.81/5.95 tff(func_def_66, type, sF31: $int).
% 38.81/5.95 tff(func_def_67, type, sF32: uni).
% 38.81/5.95 tff(func_def_68, type, sF33: uni).
% 38.81/5.95 tff(func_def_69, type, sF34: $int).
% 38.81/5.95 tff(func_def_70, type, sF35: uni).
% 38.81/5.95 tff(func_def_71, type, sF36: $int).
% 38.81/5.95 tff(func_def_72, type, sF37: uni).
% 38.81/5.95 tff(func_def_73, type, sF38: uni).
% 38.81/5.95 tff(func_def_74, type, sF39: $int).
% 38.81/5.95 tff(func_def_75, type, sF40: $int).
% 38.81/5.95 tff(func_def_76, type, sF41: $int).
% 38.81/5.95 tff(func_def_77, type, sF42: uni).
% 38.81/5.95 tff(func_def_78, type, sF43: uni).
% 38.81/5.95 tff(func_def_79, type, sF44: uni).
% 38.81/5.95 tff(func_def_80, type, sF45: map_int_int).
% 38.81/5.95 tff(pred_def_1, type, sort: (ty * uni) > $o).
% 38.81/5.95 tff(pred_def_4, type, path: ($int * $int) > $o).
% 38.81/5.95 tff(pred_def_5, type, distance: ($int * $int) > $o).
% 38.81/5.95 tff(pred_def_6, type, sP0: ($int * $int) > $o).
% 38.81/5.95 tff(f26,axiom,(
% 38.81/5.95 ! [X0 : $int] : tb2t(t2tb(X0)) = X0),
% 38.81/5.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeL)).
% 38.81/5.95 tff(f27,axiom,(
% 38.81/5.95 ! [X0 : uni] : t2tb(tb2t(X0)) = X0),
% 38.81/5.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR)).
% 38.81/5.95 tff(f34,axiom,(
% 38.81/5.95 ! [X0 : $int] : (($less(0,X0) & $less(X0,n)) => ($lesseq(0,f(X0)) & $less(f(X0),X0)))),
% 38.81/5.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f_prop)).
% 38.81/5.95 tff(f42,conjecture,(
% 38.81/5.95 $lesseq(0,n) => ($lesseq(0,n) => (($lesseq(0,0) & $less(0,n)) => ! [X0 : map_int_int] : (($lesseq(0,n) & X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1))))) => ($lesseq(0,n) => ($lesseq(0,n) => ($lesseq(1,$difference(n,1)) => ! [X1 : $int,X2 : map_int_int,X3 : map_int_int,X4 : $int] : (($lesseq(1,X4) & $lesseq(X4,$difference(n,1))) => ((tb2t(get(int,int,t2tb1(X2),t2tb(0))) = 0 & tb2t(get(int,int,t2tb1(X3),t2tb(0))) = $uminus(1) & $lesseq($sum(X1,tb2t(get(int,int,t2tb1(X2),t2tb($difference(X4,1))))),$difference(X4,1)) & ! [X5 : $int] : (($less(0,X5) & $less(X5,X4)) => ($less(tb2t(get(int,int,t2tb1(X3),get(int,int,t2tb1(X3),t2tb(X5)))),f(X5)) & $lesseq(f(X5),tb2t(get(int,int,t2tb1(X3),t2tb(X5)))) & $less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X5) & $less(0,tb2t(get(int,int,t2tb1(X2),t2tb(X5)))) & tb2t(get(int,int,t2tb1(X2),t2tb(X5))) = $sum(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),1) & ! [X6 : $int] : (($less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X6) & $less(X6,X5)) => $less(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),tb2t(get(int,int,t2tb1(X2),t2tb(X6))))))) & ! [X5 : $int] : (($lesseq(0,X5) & $less(X5,X4)) => path(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),X5))) => ! [X7 : $int,X8 : $int] : (($lesseq(f(X4),X7) & $less(X7,X4) & $lesseq($sum(X8,tb2t(get(int,int,t2tb1(X2),t2tb(X7)))),$difference(X4,1)) & ! [X5 : $int] : (($less(X7,X5) & $less(X5,X4)) => $less(tb2t(get(int,int,t2tb1(X2),t2tb(X7))),tb2t(get(int,int,t2tb1(X2),t2tb(X5)))))) => (($lesseq(0,n) & $lesseq(0,X7) & $less(X7,n)) => ($lesseq(f(X4),tb2t(get(int,int,t2tb1(X3),t2tb(X7)))) => ! [X9 : $int] : (X9 = $sum(X8,1) => (($lesseq(0,X7) & $less(X7,n)) => ! [X10 : $int] : (X10 = tb2t(get(int,int,t2tb1(X3),t2tb(X7))) => ! [X5 : $int] : (($less(X10,X5) & $less(X5,X4)) => $less(tb2t(get(int,int,t2tb1(X2),t2tb(X10))),tb2t(get(int,int,t2tb1(X2),t2tb(X5)))))))))))))))))))),
% 38.81/5.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_distance)).
% 38.81/5.95 tff(f43,negated_conjecture,(
% 38.81/5.95 ~($lesseq(0,n) => ($lesseq(0,n) => (($lesseq(0,0) & $less(0,n)) => ! [X0 : map_int_int] : (($lesseq(0,n) & X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1))))) => ($lesseq(0,n) => ($lesseq(0,n) => ($lesseq(1,$difference(n,1)) => ! [X1 : $int,X2 : map_int_int,X3 : map_int_int,X4 : $int] : (($lesseq(1,X4) & $lesseq(X4,$difference(n,1))) => ((tb2t(get(int,int,t2tb1(X2),t2tb(0))) = 0 & tb2t(get(int,int,t2tb1(X3),t2tb(0))) = $uminus(1) & $lesseq($sum(X1,tb2t(get(int,int,t2tb1(X2),t2tb($difference(X4,1))))),$difference(X4,1)) & ! [X5 : $int] : (($less(0,X5) & $less(X5,X4)) => ($less(tb2t(get(int,int,t2tb1(X3),get(int,int,t2tb1(X3),t2tb(X5)))),f(X5)) & $lesseq(f(X5),tb2t(get(int,int,t2tb1(X3),t2tb(X5)))) & $less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X5) & $less(0,tb2t(get(int,int,t2tb1(X2),t2tb(X5)))) & tb2t(get(int,int,t2tb1(X2),t2tb(X5))) = $sum(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),1) & ! [X6 : $int] : (($less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X6) & $less(X6,X5)) => $less(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),tb2t(get(int,int,t2tb1(X2),t2tb(X6))))))) & ! [X5 : $int] : (($lesseq(0,X5) & $less(X5,X4)) => path(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),X5))) => ! [X7 : $int,X8 : $int] : (($lesseq(f(X4),X7) & $less(X7,X4) & $lesseq($sum(X8,tb2t(get(int,int,t2tb1(X2),t2tb(X7)))),$difference(X4,1)) & ! [X5 : $int] : (($less(X7,X5) & $less(X5,X4)) => $less(tb2t(get(int,int,t2tb1(X2),t2tb(X7))),tb2t(get(int,int,t2tb1(X2),t2tb(X5)))))) => (($lesseq(0,n) & $lesseq(0,X7) & $less(X7,n)) => ($lesseq(f(X4),tb2t(get(int,int,t2tb1(X3),t2tb(X7)))) => ! [X9 : $int] : (X9 = $sum(X8,1) => (($lesseq(0,X7) & $less(X7,n)) => ! [X10 : $int] : (X10 = tb2t(get(int,int,t2tb1(X3),t2tb(X7))) => ! [X5 : $int] : (($less(X10,X5) & $less(X5,X4)) => $less(tb2t(get(int,int,t2tb1(X2),t2tb(X10))),tb2t(get(int,int,t2tb1(X2),t2tb(X5))))))))))))))))))))),
% 38.81/5.95 inference(negated_conjecture,[status(cth)],[f42])).
% 38.81/5.95 tff(f45,plain,(
% 38.81/5.95 ! [X0 : $int] : (($less(0,X0) & $less(X0,n)) => (~$less(f(X0),0) & $less(f(X0),X0)))),
% 38.81/5.95 inference(theory_normalization,[],[f34])).
% 38.81/5.95 tff(f49,plain,(
% 38.81/5.95 ~(~$less(n,0) => (~$less(n,0) => ((~$less(0,0) & $less(0,n)) => ! [X0 : map_int_int] : ((~$less(n,0) & X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1))))) => (~$less(n,0) => (~$less(n,0) => (~$less($sum(n,$uminus(1)),1) => ! [X1 : $int,X2 : map_int_int,X3 : map_int_int,X4 : $int] : ((~$less(X4,1) & ~$less($sum(n,$uminus(1)),X4)) => ((tb2t(get(int,int,t2tb1(X2),t2tb(0))) = 0 & tb2t(get(int,int,t2tb1(X3),t2tb(0))) = $uminus(1) & ~$less($sum(X4,$uminus(1)),$sum(X1,tb2t(get(int,int,t2tb1(X2),t2tb($sum(X4,$uminus(1))))))) & ! [X5 : $int] : (($less(0,X5) & $less(X5,X4)) => ($less(tb2t(get(int,int,t2tb1(X3),get(int,int,t2tb1(X3),t2tb(X5)))),f(X5)) & ~$less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),f(X5)) & $less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X5) & $less(0,tb2t(get(int,int,t2tb1(X2),t2tb(X5)))) & tb2t(get(int,int,t2tb1(X2),t2tb(X5))) = $sum(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),1) & ! [X6 : $int] : (($less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X6) & $less(X6,X5)) => $less(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),tb2t(get(int,int,t2tb1(X2),t2tb(X6))))))) & ! [X5 : $int] : ((~$less(X5,0) & $less(X5,X4)) => path(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),X5))) => ! [X7 : $int,X8 : $int] : ((~$less(X7,f(X4)) & $less(X7,X4) & ~$less($sum(X4,$uminus(1)),$sum(X8,tb2t(get(int,int,t2tb1(X2),t2tb(X7))))) & ! [X5 : $int] : (($less(X7,X5) & $less(X5,X4)) => $less(tb2t(get(int,int,t2tb1(X2),t2tb(X7))),tb2t(get(int,int,t2tb1(X2),t2tb(X5)))))) => ((~$less(n,0) & ~$less(X7,0) & $less(X7,n)) => (~$less(tb2t(get(int,int,t2tb1(X3),t2tb(X7))),f(X4)) => ! [X9 : $int] : (X9 = $sum(X8,1) => ((~$less(X7,0) & $less(X7,n)) => ! [X10 : $int] : (X10 = tb2t(get(int,int,t2tb1(X3),t2tb(X7))) => ! [X5 : $int] : (($less(X10,X5) & $less(X5,X4)) => $less(tb2t(get(int,int,t2tb1(X2),t2tb(X10))),tb2t(get(int,int,t2tb1(X2),t2tb(X5))))))))))))))))))))),
% 38.81/5.95 inference(theory_normalization,[],[f43])).
% 38.81/5.95 tff(f50,definition,(
% 38.81/5.95 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 38.81/5.95 introduced(theory,[tha_commutativity])).
% 38.81/5.95 tff(f51,definition,(
% 38.81/5.95 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 38.81/5.95 introduced(theory,[tha_associativity])).
% 38.81/5.95 tff(f54,definition,(
% 38.81/5.95 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 38.81/5.95 introduced(theory,[tha_inverse_op_unit])).
% 38.81/5.95 tff(f55,definition,(
% 38.81/5.95 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 38.81/5.95 introduced(theory,[tha_non-reflexivity])).
% 38.81/5.95 tff(f56,definition,(
% 38.81/5.95 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 38.81/5.95 introduced(theory,[tha_transitivity])).
% 38.81/5.95 tff(f57,definition,(
% 38.81/5.95 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 38.81/5.95 introduced(theory,[tha_order_totality])).
% 38.81/5.95 tff(f58,definition,(
% 38.81/5.95 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,X2),$sum(X1,X2)) | ~$less(X0,X1)) )),
% 38.81/5.95 introduced(theory,[tha_order_monotonicity])).
% 38.81/5.95 tff(f59,definition,(
% 38.81/5.95 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 38.81/5.95 introduced(theory,[tha_order_plus_one_dichotomy])).
% 38.81/5.95 tff(f67,definition,(
% 38.81/5.95 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,X1)) )),
% 38.81/5.95 introduced(theory,[tha_extra_integer_ordering])).
% 38.81/5.95 tff(f68,plain,(
% 38.81/5.95 ~(~$less(n,0) => (~$less(n,0) => ((~$less(0,0) & $less(0,n)) => ! [X0 : map_int_int] : ((~$less(n,0) & X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1))))) => (~$less(n,0) => (~$less(n,0) => (~$less($sum(n,$uminus(1)),1) => ! [X1 : $int,X2 : map_int_int,X3 : map_int_int,X4 : $int] : ((~$less(X4,1) & ~$less($sum(n,$uminus(1)),X4)) => ((tb2t(get(int,int,t2tb1(X2),t2tb(0))) = 0 & tb2t(get(int,int,t2tb1(X3),t2tb(0))) = $uminus(1) & ~$less($sum(X4,$uminus(1)),$sum(X1,tb2t(get(int,int,t2tb1(X2),t2tb($sum(X4,$uminus(1))))))) & ! [X5 : $int] : (($less(0,X5) & $less(X5,X4)) => ($less(tb2t(get(int,int,t2tb1(X3),get(int,int,t2tb1(X3),t2tb(X5)))),f(X5)) & ~$less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),f(X5)) & $less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X5) & $less(0,tb2t(get(int,int,t2tb1(X2),t2tb(X5)))) & tb2t(get(int,int,t2tb1(X2),t2tb(X5))) = $sum(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),1) & ! [X6 : $int] : (($less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X6) & $less(X6,X5)) => $less(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),tb2t(get(int,int,t2tb1(X2),t2tb(X6))))))) & ! [X7 : $int] : ((~$less(X7,0) & $less(X7,X4)) => path(tb2t(get(int,int,t2tb1(X2),t2tb(X7))),X7))) => ! [X8 : $int,X9 : $int] : ((~$less(X8,f(X4)) & $less(X8,X4) & ~$less($sum(X4,$uminus(1)),$sum(X9,tb2t(get(int,int,t2tb1(X2),t2tb(X8))))) & ! [X10 : $int] : (($less(X8,X10) & $less(X10,X4)) => $less(tb2t(get(int,int,t2tb1(X2),t2tb(X8))),tb2t(get(int,int,t2tb1(X2),t2tb(X10)))))) => ((~$less(n,0) & ~$less(X8,0) & $less(X8,n)) => (~$less(tb2t(get(int,int,t2tb1(X3),t2tb(X8))),f(X4)) => ! [X11 : $int] : ($sum(X9,1) = X11 => ((~$less(X8,0) & $less(X8,n)) => ! [X12 : $int] : (tb2t(get(int,int,t2tb1(X3),t2tb(X8))) = X12 => ! [X13 : $int] : (($less(X12,X13) & $less(X13,X4)) => $less(tb2t(get(int,int,t2tb1(X2),t2tb(X12))),tb2t(get(int,int,t2tb1(X2),t2tb(X13))))))))))))))))))))),
% 38.81/5.95 inference(rectify,[],[f49])).
% 38.81/5.95 tff(f81,plain,(
% 38.81/5.95 ! [X0 : $int] : ((~$less(f(X0),0) & $less(f(X0),X0)) | (~$less(0,X0) | ~$less(X0,n)))),
% 38.81/5.95 inference(ennf_transformation,[],[f45])).
% 38.81/5.95 tff(f82,plain,(
% 38.81/5.95 ! [X0 : $int] : ((~$less(f(X0),0) & $less(f(X0),X0)) | ~$less(0,X0) | ~$less(X0,n))),
% 38.81/5.95 inference(flattening,[],[f81])).
% 38.81/5.95 tff(f87,plain,(
% 38.81/5.95 ((? [X0 : map_int_int] : ((((? [X1 : $int,X2 : map_int_int,X3 : map_int_int,X4 : $int] : ((? [X8 : $int,X9 : $int] : (((? [X11 : $int] : ((? [X12 : $int] : (? [X13 : $int] : (~$less(tb2t(get(int,int,t2tb1(X2),t2tb(X12))),tb2t(get(int,int,t2tb1(X2),t2tb(X13)))) & ($less(X12,X13) & $less(X13,X4))) & tb2t(get(int,int,t2tb1(X3),t2tb(X8))) = X12) & (~$less(X8,0) & $less(X8,n))) & $sum(X9,1) = X11) & ~$less(tb2t(get(int,int,t2tb1(X3),t2tb(X8))),f(X4))) & (~$less(n,0) & ~$less(X8,0) & $less(X8,n))) & (~$less(X8,f(X4)) & $less(X8,X4) & ~$less($sum(X4,$uminus(1)),$sum(X9,tb2t(get(int,int,t2tb1(X2),t2tb(X8))))) & ! [X10 : $int] : ($less(tb2t(get(int,int,t2tb1(X2),t2tb(X8))),tb2t(get(int,int,t2tb1(X2),t2tb(X10)))) | (~$less(X8,X10) | ~$less(X10,X4))))) & (tb2t(get(int,int,t2tb1(X2),t2tb(0))) = 0 & tb2t(get(int,int,t2tb1(X3),t2tb(0))) = $uminus(1) & ~$less($sum(X4,$uminus(1)),$sum(X1,tb2t(get(int,int,t2tb1(X2),t2tb($sum(X4,$uminus(1))))))) & ! [X5 : $int] : (($less(tb2t(get(int,int,t2tb1(X3),get(int,int,t2tb1(X3),t2tb(X5)))),f(X5)) & ~$less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),f(X5)) & $less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X5) & $less(0,tb2t(get(int,int,t2tb1(X2),t2tb(X5)))) & tb2t(get(int,int,t2tb1(X2),t2tb(X5))) = $sum(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),1) & ! [X6 : $int] : ($less(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),tb2t(get(int,int,t2tb1(X2),t2tb(X6)))) | (~$less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X6) | ~$less(X6,X5)))) | (~$less(0,X5) | ~$less(X5,X4))) & ! [X7 : $int] : (path(tb2t(get(int,int,t2tb1(X2),t2tb(X7))),X7) | ($less(X7,0) | ~$less(X7,X4))))) & (~$less(X4,1) & ~$less($sum(n,$uminus(1)),X4))) & ~$less($sum(n,$uminus(1)),1)) & ~$less(n,0)) & ~$less(n,0)) & (~$less(n,0) & X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1)))))) & (~$less(0,0) & $less(0,n))) & ~$less(n,0)) & ~$less(n,0)),
% 38.81/5.95 inference(ennf_transformation,[],[f68])).
% 38.81/5.95 tff(f88,plain,(
% 38.81/5.95 ? [X0 : map_int_int] : (? [X1 : $int,X2 : map_int_int,X3 : map_int_int,X4 : $int] : (? [X8 : $int,X9 : $int] : (? [X11 : $int] : (? [X12 : $int] : (? [X13 : $int] : (~$less(tb2t(get(int,int,t2tb1(X2),t2tb(X12))),tb2t(get(int,int,t2tb1(X2),t2tb(X13)))) & $less(X12,X13) & $less(X13,X4)) & tb2t(get(int,int,t2tb1(X3),t2tb(X8))) = X12) & ~$less(X8,0) & $less(X8,n) & $sum(X9,1) = X11) & ~$less(tb2t(get(int,int,t2tb1(X3),t2tb(X8))),f(X4)) & ~$less(n,0) & ~$less(X8,0) & $less(X8,n) & ~$less(X8,f(X4)) & $less(X8,X4) & ~$less($sum(X4,$uminus(1)),$sum(X9,tb2t(get(int,int,t2tb1(X2),t2tb(X8))))) & ! [X10 : $int] : ($less(tb2t(get(int,int,t2tb1(X2),t2tb(X8))),tb2t(get(int,int,t2tb1(X2),t2tb(X10)))) | ~$less(X8,X10) | ~$less(X10,X4))) & tb2t(get(int,int,t2tb1(X2),t2tb(0))) = 0 & tb2t(get(int,int,t2tb1(X3),t2tb(0))) = $uminus(1) & ~$less($sum(X4,$uminus(1)),$sum(X1,tb2t(get(int,int,t2tb1(X2),t2tb($sum(X4,$uminus(1))))))) & ! [X5 : $int] : (($less(tb2t(get(int,int,t2tb1(X3),get(int,int,t2tb1(X3),t2tb(X5)))),f(X5)) & ~$less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),f(X5)) & $less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X5) & $less(0,tb2t(get(int,int,t2tb1(X2),t2tb(X5)))) & tb2t(get(int,int,t2tb1(X2),t2tb(X5))) = $sum(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),1) & ! [X6 : $int] : ($less(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),tb2t(get(int,int,t2tb1(X2),t2tb(X6)))) | ~$less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X6) | ~$less(X6,X5))) | ~$less(0,X5) | ~$less(X5,X4)) & ! [X7 : $int] : (path(tb2t(get(int,int,t2tb1(X2),t2tb(X7))),X7) | $less(X7,0) | ~$less(X7,X4)) & ~$less(X4,1) & ~$less($sum(n,$uminus(1)),X4)) & ~$less($sum(n,$uminus(1)),1) & ~$less(n,0) & ~$less(n,0) & ~$less(n,0) & X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1))))) & ~$less(0,0) & $less(0,n) & ~$less(n,0) & ~$less(n,0)),
% 38.81/5.95 inference(flattening,[],[f87])).
% 38.81/5.95 tff(f93,plain,(
% 38.81/5.95 ? [X0 : map_int_int] : (? [X1 : $int,X2 : map_int_int,X3 : map_int_int,X4 : $int] : (? [X5 : $int,X6 : $int] : (? [X7 : $int] : (? [X8 : $int] : (? [X9 : $int] : (~$less(tb2t(get(int,int,t2tb1(X2),t2tb(X8))),tb2t(get(int,int,t2tb1(X2),t2tb(X9)))) & $less(X8,X9) & $less(X9,X4)) & tb2t(get(int,int,t2tb1(X3),t2tb(X5))) = X8) & ~$less(X5,0) & $less(X5,n) & $sum(X6,1) = X7) & ~$less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),f(X4)) & ~$less(n,0) & ~$less(X5,0) & $less(X5,n) & ~$less(X5,f(X4)) & $less(X5,X4) & ~$less($sum(X4,$uminus(1)),$sum(X6,tb2t(get(int,int,t2tb1(X2),t2tb(X5))))) & ! [X10 : $int] : ($less(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),tb2t(get(int,int,t2tb1(X2),t2tb(X10)))) | ~$less(X5,X10) | ~$less(X10,X4))) & tb2t(get(int,int,t2tb1(X2),t2tb(0))) = 0 & tb2t(get(int,int,t2tb1(X3),t2tb(0))) = $uminus(1) & ~$less($sum(X4,$uminus(1)),$sum(X1,tb2t(get(int,int,t2tb1(X2),t2tb($sum(X4,$uminus(1))))))) & ! [X11 : $int] : (($less(tb2t(get(int,int,t2tb1(X3),get(int,int,t2tb1(X3),t2tb(X11)))),f(X11)) & ~$less(tb2t(get(int,int,t2tb1(X3),t2tb(X11))),f(X11)) & $less(tb2t(get(int,int,t2tb1(X3),t2tb(X11))),X11) & $less(0,tb2t(get(int,int,t2tb1(X2),t2tb(X11)))) & tb2t(get(int,int,t2tb1(X2),t2tb(X11))) = $sum(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X11)))),1) & ! [X12 : $int] : ($less(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X11)))),tb2t(get(int,int,t2tb1(X2),t2tb(X12)))) | ~$less(tb2t(get(int,int,t2tb1(X3),t2tb(X11))),X12) | ~$less(X12,X11))) | ~$less(0,X11) | ~$less(X11,X4)) & ! [X13 : $int] : (path(tb2t(get(int,int,t2tb1(X2),t2tb(X13))),X13) | $less(X13,0) | ~$less(X13,X4)) & ~$less(X4,1) & ~$less($sum(n,$uminus(1)),X4)) & ~$less($sum(n,$uminus(1)),1) & ~$less(n,0) & ~$less(n,0) & ~$less(n,0) & X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1))))) & ~$less(0,0) & $less(0,n) & ~$less(n,0) & ~$less(n,0)),
% 38.81/5.95 inference(rectify,[],[f88])).
% 38.81/5.95 tff(f94,plain,(
% 38.81/5.95 ((((((~$less(tb2t(get(int,int,t2tb1(sK6),t2tb(sK12))),tb2t(get(int,int,t2tb1(sK6),t2tb(sK13)))) & $less(sK12,sK13) & $less(sK13,sK8)) & sK12 = tb2t(get(int,int,t2tb1(sK7),t2tb(sK9)))) & ~$less(sK9,0) & $less(sK9,n) & sK11 = $sum(sK10,1)) & ~$less(tb2t(get(int,int,t2tb1(sK7),t2tb(sK9))),f(sK8)) & ~$less(n,0) & ~$less(sK9,0) & $less(sK9,n) & ~$less(sK9,f(sK8)) & $less(sK9,sK8) & ~$less($sum(sK8,$uminus(1)),$sum(sK10,tb2t(get(int,int,t2tb1(sK6),t2tb(sK9))))) & ! [X10 : $int] : ($less(tb2t(get(int,int,t2tb1(sK6),t2tb(sK9))),tb2t(get(int,int,t2tb1(sK6),t2tb(X10)))) | ~$less(sK9,X10) | ~$less(X10,sK8))) & 0 = tb2t(get(int,int,t2tb1(sK6),t2tb(0))) & $uminus(1) = tb2t(get(int,int,t2tb1(sK7),t2tb(0))) & ~$less($sum(sK8,$uminus(1)),$sum(sK5,tb2t(get(int,int,t2tb1(sK6),t2tb($sum(sK8,$uminus(1))))))) & ! [X11 : $int] : (($less(tb2t(get(int,int,t2tb1(sK7),get(int,int,t2tb1(sK7),t2tb(X11)))),f(X11)) & ~$less(tb2t(get(int,int,t2tb1(sK7),t2tb(X11))),f(X11)) & $less(tb2t(get(int,int,t2tb1(sK7),t2tb(X11))),X11) & $less(0,tb2t(get(int,int,t2tb1(sK6),t2tb(X11)))) & tb2t(get(int,int,t2tb1(sK6),t2tb(X11))) = $sum(tb2t(get(int,int,t2tb1(sK6),get(int,int,t2tb1(sK7),t2tb(X11)))),1) & ! [X12 : $int] : ($less(tb2t(get(int,int,t2tb1(sK6),get(int,int,t2tb1(sK7),t2tb(X11)))),tb2t(get(int,int,t2tb1(sK6),t2tb(X12)))) | ~$less(tb2t(get(int,int,t2tb1(sK7),t2tb(X11))),X12) | ~$less(X12,X11))) | ~$less(0,X11) | ~$less(X11,sK8)) & ! [X13 : $int] : (path(tb2t(get(int,int,t2tb1(sK6),t2tb(X13))),X13) | $less(X13,0) | ~$less(X13,sK8)) & ~$less(sK8,1) & ~$less($sum(n,$uminus(1)),sK8)) & ~$less($sum(n,$uminus(1)),1) & ~$less(n,0) & ~$less(n,0) & ~$less(n,0) & tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1)))) = sK4) & ~$less(0,0) & $less(0,n) & ~$less(n,0) & ~$less(n,0)),
% 38.81/5.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6),skolemize(X3,sK7),skolemize(X4,sK8),skolemize(X5,sK9),skolemize(X6,sK10),skolemize(X7,sK11),skolemize(X8,sK12),skolemize(X9,sK13)],[f93])).
% 38.81/5.95 tff(f120,plain,(
% 38.81/5.95 ( ! [X0 : $int] : (tb2t(t2tb(X0)) = X0) )),
% 38.81/5.95 inference(cnf_transformation,[],[f26])).
% 38.81/5.95 tff(f121,plain,(
% 38.81/5.95 ( ! [X0 : uni] : (t2tb(tb2t(X0)) = X0) )),
% 38.81/5.95 inference(cnf_transformation,[],[f27])).
% 38.81/5.95 tff(f129,plain,(
% 38.81/5.95 ( ! [X0 : $int] : (~$less(f(X0),0) | ~$less(0,X0) | ~$less(X0,n)) )),
% 38.81/5.95 inference(cnf_transformation,[],[f82])).
% 38.81/5.95 tff(f153,plain,(
% 38.81/5.95 ~$less($sum(n,$uminus(1)),sK8)),
% 38.81/5.95 inference(cnf_transformation,[],[f94])).
% 38.81/5.95 tff(f156,plain,(
% 38.81/5.95 ( ! [X11 : $int,X12 : $int] : ($less(tb2t(get(int,int,t2tb1(sK6),get(int,int,t2tb1(sK7),t2tb(X11)))),tb2t(get(int,int,t2tb1(sK6),t2tb(X12)))) | ~$less(tb2t(get(int,int,t2tb1(sK7),t2tb(X11))),X12) | ~$less(X12,X11) | ~$less(0,X11) | ~$less(X11,sK8)) )),
% 38.81/5.95 inference(cnf_transformation,[],[f94])).
% 38.81/5.95 tff(f157,plain,(
% 38.81/5.95 ( ! [X11 : $int] : (tb2t(get(int,int,t2tb1(sK6),t2tb(X11))) = $sum(tb2t(get(int,int,t2tb1(sK6),get(int,int,t2tb1(sK7),t2tb(X11)))),1) | ~$less(0,X11) | ~$less(X11,sK8)) )),
% 38.81/5.95 inference(cnf_transformation,[],[f94])).
% 38.81/5.95 tff(f163,plain,(
% 38.81/5.95 $uminus(1) = tb2t(get(int,int,t2tb1(sK7),t2tb(0)))),
% 38.81/5.95 inference(cnf_transformation,[],[f94])).
% 38.81/5.95 tff(f165,plain,(
% 38.81/5.95 ( ! [X10 : $int] : ($less(tb2t(get(int,int,t2tb1(sK6),t2tb(sK9))),tb2t(get(int,int,t2tb1(sK6),t2tb(X10)))) | ~$less(sK9,X10) | ~$less(X10,sK8)) )),
% 38.81/5.95 inference(cnf_transformation,[],[f94])).
% 38.81/5.95 tff(f167,plain,(
% 38.81/5.95 $less(sK9,sK8)),
% 38.81/5.95 inference(cnf_transformation,[],[f94])).
% 38.81/5.95 tff(f170,plain,(
% 38.81/5.95 ~$less(sK9,0)),
% 38.81/5.95 inference(cnf_transformation,[],[f94])).
% 38.81/5.95 tff(f172,plain,(
% 38.81/5.95 ~$less(tb2t(get(int,int,t2tb1(sK7),t2tb(sK9))),f(sK8))),
% 38.81/5.95 inference(cnf_transformation,[],[f94])).
% 38.81/5.95 tff(f176,plain,(
% 38.81/5.95 sK12 = tb2t(get(int,int,t2tb1(sK7),t2tb(sK9)))),
% 38.81/5.95 inference(cnf_transformation,[],[f94])).
% 38.81/5.95 tff(f177,plain,(
% 38.81/5.95 $less(sK13,sK8)),
% 38.81/5.95 inference(cnf_transformation,[],[f94])).
% 38.81/5.95 tff(f178,plain,(
% 38.81/5.95 $less(sK12,sK13)),
% 38.81/5.95 inference(cnf_transformation,[],[f94])).
% 38.81/5.95 tff(f179,plain,(
% 38.81/5.95 ~$less(tb2t(get(int,int,t2tb1(sK6),t2tb(sK12))),tb2t(get(int,int,t2tb1(sK6),t2tb(sK13))))),
% 38.81/5.95 inference(cnf_transformation,[],[f94])).
% 38.81/5.95 tff(f185,definition,(
% 38.81/5.95 sF14 = t2tb1(sK6)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 38.81/5.95 tff(f186,plain,(
% 38.81/5.95 t2tb1(sK6) = sF14),
% 38.81/5.95 inference(reorient_equations,[],[f185])).
% 38.81/5.95 tff(f187,definition,(
% 38.81/5.95 sF15 = t2tb(sK12)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 38.81/5.95 tff(f188,plain,(
% 38.81/5.95 t2tb(sK12) = sF15),
% 38.81/5.95 inference(reorient_equations,[],[f187])).
% 38.81/5.95 tff(f189,definition,(
% 38.81/5.95 sF16 = get(int,int,sF14,sF15)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF16])],[function_definition])).
% 38.81/5.95 tff(f190,plain,(
% 38.81/5.95 get(int,int,sF14,sF15) = sF16),
% 38.81/5.95 inference(reorient_equations,[],[f189])).
% 38.81/5.95 tff(f191,definition,(
% 38.81/5.95 sF17 = tb2t(sF16)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF17])],[function_definition])).
% 38.81/5.95 tff(f192,plain,(
% 38.81/5.95 tb2t(sF16) = sF17),
% 38.81/5.95 inference(reorient_equations,[],[f191])).
% 38.81/5.95 tff(f193,definition,(
% 38.81/5.95 sF18 = t2tb(sK13)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF18])],[function_definition])).
% 38.81/5.95 tff(f194,plain,(
% 38.81/5.95 t2tb(sK13) = sF18),
% 38.81/5.95 inference(reorient_equations,[],[f193])).
% 38.81/5.95 tff(f195,definition,(
% 38.81/5.95 sF19 = get(int,int,sF14,sF18)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF19])],[function_definition])).
% 38.81/5.95 tff(f196,plain,(
% 38.81/5.95 get(int,int,sF14,sF18) = sF19),
% 38.81/5.95 inference(reorient_equations,[],[f195])).
% 38.81/5.95 tff(f197,definition,(
% 38.81/5.95 sF20 = tb2t(sF19)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF20])],[function_definition])).
% 38.81/5.95 tff(f198,plain,(
% 38.81/5.95 tb2t(sF19) = sF20),
% 38.81/5.95 inference(reorient_equations,[],[f197])).
% 38.81/5.95 tff(f199,plain,(
% 38.81/5.95 ~$less(sF17,sF20)),
% 38.81/5.95 inference(definition_folding,[],[f179,f198,f196,f194,f186,f192,f190,f188,f186])).
% 38.81/5.95 tff(f200,definition,(
% 38.81/5.95 sF21 = t2tb1(sK7)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF21])],[function_definition])).
% 38.81/5.95 tff(f201,plain,(
% 38.81/5.95 t2tb1(sK7) = sF21),
% 38.81/5.95 inference(reorient_equations,[],[f200])).
% 38.81/5.95 tff(f202,definition,(
% 38.81/5.95 sF22 = t2tb(sK9)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF22])],[function_definition])).
% 38.81/5.95 tff(f203,plain,(
% 38.81/5.95 t2tb(sK9) = sF22),
% 38.81/5.95 inference(reorient_equations,[],[f202])).
% 38.81/5.95 tff(f204,definition,(
% 38.81/5.95 sF23 = get(int,int,sF21,sF22)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF23])],[function_definition])).
% 38.81/5.95 tff(f205,plain,(
% 38.81/5.95 get(int,int,sF21,sF22) = sF23),
% 38.81/5.95 inference(reorient_equations,[],[f204])).
% 38.81/5.95 tff(f206,definition,(
% 38.81/5.95 sF24 = tb2t(sF23)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF24])],[function_definition])).
% 38.81/5.95 tff(f207,plain,(
% 38.81/5.95 tb2t(sF23) = sF24),
% 38.81/5.95 inference(reorient_equations,[],[f206])).
% 38.81/5.95 tff(f208,plain,(
% 38.81/5.95 sK12 = sF24),
% 38.81/5.95 inference(definition_folding,[],[f176,f207,f205,f203,f201])).
% 38.81/5.95 tff(f212,definition,(
% 38.81/5.95 sF26 = f(sK8)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF26])],[function_definition])).
% 38.81/5.95 tff(f213,plain,(
% 38.81/5.95 f(sK8) = sF26),
% 38.81/5.95 inference(reorient_equations,[],[f212])).
% 38.81/5.95 tff(f214,plain,(
% 38.81/5.95 ~$less(sF24,sF26)),
% 38.81/5.95 inference(definition_folding,[],[f172,f213,f207,f205,f203,f201])).
% 38.81/5.95 tff(f216,definition,(
% 38.81/5.95 sF27 = $uminus(1)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF27])],[function_definition])).
% 38.81/5.95 tff(f217,plain,(
% 38.81/5.95 $uminus(1) = sF27),
% 38.81/5.95 inference(reorient_equations,[],[f216])).
% 38.81/5.95 tff(f220,definition,(
% 38.81/5.95 sF29 = get(int,int,sF14,sF22)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF29])],[function_definition])).
% 38.81/5.95 tff(f221,plain,(
% 38.81/5.95 get(int,int,sF14,sF22) = sF29),
% 38.81/5.95 inference(reorient_equations,[],[f220])).
% 38.81/5.95 tff(f222,definition,(
% 38.81/5.95 sF30 = tb2t(sF29)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF30])],[function_definition])).
% 38.81/5.95 tff(f223,plain,(
% 38.81/5.95 tb2t(sF29) = sF30),
% 38.81/5.95 inference(reorient_equations,[],[f222])).
% 38.81/5.95 tff(f227,plain,(
% 38.81/5.95 ( ! [X10 : $int] : ($less(sF30,tb2t(get(int,int,sF14,t2tb(X10)))) | ~$less(sK9,X10) | ~$less(X10,sK8)) )),
% 38.81/5.95 inference(definition_folding,[],[f165,f186,f223,f221,f203,f186])).
% 38.81/5.95 tff(f228,definition,(
% 38.81/5.95 sF32 = t2tb(0)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF32])],[function_definition])).
% 38.81/5.95 tff(f229,plain,(
% 38.81/5.95 t2tb(0) = sF32),
% 38.81/5.95 inference(reorient_equations,[],[f228])).
% 38.81/5.95 tff(f235,definition,(
% 38.81/5.95 sF35 = get(int,int,sF21,sF32)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF35])],[function_definition])).
% 38.81/5.95 tff(f236,plain,(
% 38.81/5.95 get(int,int,sF21,sF32) = sF35),
% 38.81/5.95 inference(reorient_equations,[],[f235])).
% 38.81/5.95 tff(f237,definition,(
% 38.81/5.95 sF36 = tb2t(sF35)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF36])],[function_definition])).
% 38.81/5.95 tff(f238,plain,(
% 38.81/5.95 tb2t(sF35) = sF36),
% 38.81/5.95 inference(reorient_equations,[],[f237])).
% 38.81/5.95 tff(f239,plain,(
% 38.81/5.95 sF27 = sF36),
% 38.81/5.95 inference(definition_folding,[],[f163,f238,f236,f229,f201,f217])).
% 38.81/5.95 tff(f253,plain,(
% 38.81/5.95 ( ! [X11 : $int] : (~$less(0,X11) | tb2t(get(int,int,sF14,t2tb(X11))) = $sum(tb2t(get(int,int,sF14,get(int,int,sF21,t2tb(X11)))),1) | ~$less(X11,sK8)) )),
% 38.81/5.95 inference(definition_folding,[],[f157,f201,f186,f186])).
% 38.81/5.95 tff(f254,plain,(
% 38.81/5.95 ( ! [X11 : $int,X12 : $int] : ($less(tb2t(get(int,int,sF14,get(int,int,sF21,t2tb(X11)))),tb2t(get(int,int,sF14,t2tb(X12)))) | ~$less(tb2t(get(int,int,sF21,t2tb(X11))),X12) | ~$less(X12,X11) | ~$less(0,X11) | ~$less(X11,sK8)) )),
% 38.81/5.95 inference(definition_folding,[],[f156,f201,f186,f201,f186])).
% 38.81/5.95 tff(f256,definition,(
% 38.81/5.95 sF41 = $sum(n,sF27)),
% 38.81/5.95 introduced(definition,[new_symbols(definition,[sF41])],[function_definition])).
% 38.81/5.95 tff(f257,plain,(
% 38.81/5.95 $sum(n,sF27) = sF41),
% 38.81/5.95 inference(reorient_equations,[],[f256])).
% 38.81/5.95 tff(f258,plain,(
% 38.81/5.95 ~$less(sF41,sK8)),
% 38.81/5.95 inference(definition_folding,[],[f153,f257,f217])).
% 38.81/5.95 tff(f269,plain,(
% 38.81/5.95 sF27 = -1),
% 38.81/5.95 inference(evaluation,[],[f217])).
% 38.81/5.95 tff(f270,plain,(
% 38.81/5.95 sK12 = tb2t(sF23)),
% 38.81/5.95 inference(forward_demodulation,[],[f207,f208])).
% 38.81/5.95 tff(f275,plain,(
% 38.81/5.95 sF27 = tb2t(sF35)),
% 38.81/5.95 inference(forward_demodulation,[],[f238,f239])).
% 38.81/5.95 tff(f277,plain,(
% 38.81/5.95 sF41 = $sum(n,-1)),
% 38.81/5.95 inference(forward_demodulation,[],[f257,f269])).
% 38.81/5.95 tff(f280,plain,(
% 38.81/5.95 tb2t(sF35) = -1),
% 38.81/5.95 inference(forward_demodulation,[],[f275,f269])).
% 38.81/5.95 tff(f281,plain,(
% 38.81/5.95 sF41 = $sum(-1,n)),
% 38.81/5.95 inference(forward_demodulation,[],[f277,f50])).
% 38.81/5.95 tff(f282,plain,(
% 38.81/5.95 ~$less(sK12,sF26)),
% 38.81/5.95 inference(superposition,[],[f214,f208])).
% 38.81/5.95 tff(f339,plain,(
% 38.81/5.95 ( ! [X0 : $int] : ($less(tb2t(get(int,int,sF14,get(int,int,sF21,sF22))),tb2t(get(int,int,sF14,t2tb(X0)))) | ~$less(tb2t(get(int,int,sF21,sF22)),X0) | ~$less(X0,sK9) | ~$less(0,sK9) | ~$less(sK9,sK8)) )),
% 38.81/5.95 inference(superposition,[],[f254,f203])).
% 38.81/5.95 tff(f342,plain,(
% 38.81/5.95 ( ! [X0 : $int] : ($less(tb2t(get(int,int,sF14,get(int,int,sF21,sF22))),tb2t(get(int,int,sF14,t2tb(X0)))) | ~$less(tb2t(get(int,int,sF21,sF22)),X0) | ~$less(X0,sK9) | ~$less(0,sK9)) )),
% 38.81/5.95 inference(forward_subsumption_resolution,[],[f339,f167])).
% 38.81/5.95 tff(f349,plain,(
% 38.81/5.95 ( ! [X0 : $int] : ($less(tb2t(get(int,int,sF14,sF23)),tb2t(get(int,int,sF14,t2tb(X0)))) | ~$less(tb2t(get(int,int,sF21,sF22)),X0) | ~$less(X0,sK9) | ~$less(0,sK9)) )),
% 38.81/5.95 inference(forward_demodulation,[],[f342,f205])).
% 38.81/5.95 tff(f356,plain,(
% 38.81/5.95 ( ! [X0 : $int] : (~$less(tb2t(sF23),X0) | $less(tb2t(get(int,int,sF14,sF23)),tb2t(get(int,int,sF14,t2tb(X0)))) | ~$less(X0,sK9) | ~$less(0,sK9)) )),
% 38.81/5.95 inference(forward_demodulation,[],[f349,f205])).
% 38.81/5.95 tff(f361,plain,(
% 38.81/5.95 ( ! [X0 : $int] : ($less(tb2t(get(int,int,sF14,sF23)),tb2t(get(int,int,sF14,t2tb(X0)))) | ~$less(sK12,X0) | ~$less(X0,sK9) | ~$less(0,sK9)) )),
% 38.81/5.95 inference(forward_demodulation,[],[f356,f270])).
% 38.81/5.95 tff(f407,plain,(
% 38.81/5.95 sK12 = tb2t(sF15)),
% 38.81/5.95 inference(superposition,[],[f120,f188])).
% 38.81/5.95 tff(f413,plain,(
% 38.81/5.95 t2tb(sK12) = sF23),
% 38.81/5.95 inference(superposition,[],[f121,f270])).
% 38.81/5.95 tff(f428,plain,(
% 38.81/5.95 sF15 = sF23),
% 38.81/5.95 inference(forward_demodulation,[],[f413,f188])).
% 38.81/5.95 tff(f585,plain,(
% 38.81/5.95 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(1,X0)) | $less(X0,X1)) )),
% 38.81/5.95 inference(superposition,[],[f59,f50])).
% 38.81/5.95 tff(f590,plain,(
% 38.81/5.95 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(1,X0)) | ~$less(X0,X1)) )),
% 38.81/5.95 inference(superposition,[],[f67,f50])).
% 38.81/5.95 tff(f626,plain,(
% 38.81/5.95 ( ! [X0 : $int,X1 : $int] : ($less(X0,tb2t(get(int,int,sF14,t2tb(X1)))) | ~$less(X0,sF30) | ~$less(sK9,X1) | ~$less(X1,sK8)) )),
% 38.81/5.95 inference(resolution,[],[f56,f227])).
% 38.81/5.95 tff(f673,plain,(
% 38.81/5.95 $less(0,sK9) | 0 = sK9),
% 38.81/5.95 inference(resolution,[],[f57,f170])).
% 38.81/5.95 tff(f680,plain,(
% 38.81/5.95 $less(sK8,sF41) | sK8 = sF41),
% 38.81/5.95 inference(resolution,[],[f57,f258])).
% 38.81/5.95 tff(f753,plain,(
% 38.81/5.95 ( ! [X0 : $int] : ($less(sF41,$sum(X0,n)) | ~$less(-1,X0)) )),
% 38.81/5.95 inference(superposition,[],[f58,f281])).
% 38.81/5.95 tff(f793,plain,(
% 38.81/5.95 0 = sK9 | tb2t(get(int,int,sF14,t2tb(sK9))) = $sum(tb2t(get(int,int,sF14,get(int,int,sF21,t2tb(sK9)))),1) | ~$less(sK9,sK8)),
% 38.81/5.95 inference(resolution,[],[f673,f253])).
% 38.81/5.95 tff(f797,plain,(
% 38.81/5.95 0 = sK9 | tb2t(get(int,int,sF14,t2tb(sK9))) = $sum(tb2t(get(int,int,sF14,get(int,int,sF21,t2tb(sK9)))),1)),
% 38.81/5.95 inference(forward_subsumption_resolution,[],[f793,f167])).
% 38.81/5.95 tff(f798,plain,(
% 38.81/5.95 tb2t(get(int,int,sF14,t2tb(sK9))) = $sum(1,tb2t(get(int,int,sF14,get(int,int,sF21,t2tb(sK9))))) | 0 = sK9),
% 38.81/5.95 inference(forward_demodulation,[],[f797,f50])).
% 38.81/5.95 tff(f799,plain,(
% 38.81/5.95 tb2t(get(int,int,sF14,sF22)) = $sum(1,tb2t(get(int,int,sF14,get(int,int,sF21,sF22)))) | 0 = sK9),
% 38.81/5.95 inference(forward_demodulation,[],[f798,f203])).
% 38.81/5.95 tff(f800,plain,(
% 38.81/5.95 tb2t(get(int,int,sF14,sF22)) = $sum(1,tb2t(get(int,int,sF14,sF23))) | 0 = sK9),
% 38.81/5.95 inference(forward_demodulation,[],[f799,f205])).
% 38.81/5.95 tff(f801,plain,(
% 38.81/5.95 tb2t(get(int,int,sF14,sF22)) = $sum(1,tb2t(get(int,int,sF14,sF15))) | 0 = sK9),
% 38.81/5.95 inference(forward_demodulation,[],[f800,f428])).
% 38.81/5.95 tff(f802,plain,(
% 38.81/5.95 tb2t(get(int,int,sF14,sF22)) = $sum(1,tb2t(sF16)) | 0 = sK9),
% 38.81/5.95 inference(forward_demodulation,[],[f801,f190])).
% 38.81/5.95 tff(f803,plain,(
% 38.81/5.95 tb2t(get(int,int,sF14,sF22)) = $sum(1,sF17) | 0 = sK9),
% 38.81/5.95 inference(forward_demodulation,[],[f802,f192])).
% 38.81/5.95 tff(f804,plain,(
% 38.81/5.95 tb2t(sF29) = $sum(1,sF17) | 0 = sK9),
% 38.81/5.95 inference(forward_demodulation,[],[f803,f221])).
% 38.81/5.95 tff(f805,plain,(
% 38.81/5.95 sF30 = $sum(1,sF17) | 0 = sK9),
% 38.81/5.95 inference(forward_demodulation,[],[f804,f223])).
% 38.81/5.95 tff(f816,plain,(
% 38.81/5.95 ( ! [X0 : $int] : (~$less(X0,sK8) | sK8 = sF41 | $less(X0,sF41)) )),
% 38.81/5.95 inference(resolution,[],[f680,f56])).
% 38.81/5.95 tff(f841,plain,(
% 38.81/5.95 ~$less(sF26,0) | ~$less(0,sK8) | ~$less(sK8,n)),
% 38.81/5.95 inference(superposition,[],[f129,f213])).
% 38.81/5.95 tff(f888,plain,(
% 38.81/5.95 ( ! [X0 : $int] : ($sum(-1,$sum(n,X0)) = $sum(sF41,X0)) )),
% 38.81/5.95 inference(superposition,[],[f51,f281])).
% 38.81/5.95 tff(f1174,plain,(
% 38.81/5.95 ( ! [X0 : $int] : (~$less(tb2t(get(int,int,sF14,t2tb(X0))),sF30) | ~$less(sK9,X0) | ~$less(X0,sK8)) )),
% 38.81/5.95 inference(resolution,[],[f626,f55])).
% 38.81/5.95 tff(f1267,plain,(
% 38.81/5.95 $less(tb2t(get(int,int,sF14,sF23)),tb2t(get(int,int,sF14,sF18))) | ~$less(sK12,sK13) | ~$less(sK13,sK9) | ~$less(0,sK9)),
% 38.81/5.95 inference(superposition,[],[f361,f194])).
% 38.81/5.95 tff(f1275,plain,(
% 38.81/5.95 $less(tb2t(get(int,int,sF14,sF23)),tb2t(get(int,int,sF14,sF18))) | ~$less(sK13,sK9) | ~$less(0,sK9)),
% 38.81/5.95 inference(forward_subsumption_resolution,[],[f1267,f178])).
% 38.81/5.95 tff(f1283,plain,(
% 38.81/5.95 $less(tb2t(get(int,int,sF14,sF23)),tb2t(sF19)) | ~$less(sK13,sK9) | ~$less(0,sK9)),
% 38.81/5.95 inference(forward_demodulation,[],[f1275,f196])).
% 38.81/5.95 tff(f1291,plain,(
% 38.81/5.95 $less(tb2t(get(int,int,sF14,sF23)),sF20) | ~$less(sK13,sK9) | ~$less(0,sK9)),
% 38.81/5.95 inference(forward_demodulation,[],[f1283,f198])).
% 38.81/5.95 tff(f1297,plain,(
% 38.81/5.95 $less(tb2t(get(int,int,sF14,sF15)),sF20) | ~$less(sK13,sK9) | ~$less(0,sK9)),
% 38.81/5.95 inference(forward_demodulation,[],[f1291,f428])).
% 38.81/5.95 tff(f1300,plain,(
% 38.81/5.95 $less(tb2t(sF16),sF20) | ~$less(sK13,sK9) | ~$less(0,sK9)),
% 38.81/5.95 inference(forward_demodulation,[],[f1297,f190])).
% 38.81/5.95 tff(f1302,plain,(
% 38.81/5.95 $less(sF17,sF20) | ~$less(sK13,sK9) | ~$less(0,sK9)),
% 38.81/5.95 inference(forward_demodulation,[],[f1300,f192])).
% 38.81/5.95 tff(f1303,plain,(
% 38.81/5.95 ~$less(sK13,sK9) | ~$less(0,sK9)),
% 38.81/5.95 inference(forward_subsumption_resolution,[],[f1302,f199])).
% 38.81/5.95 tff(f1305,plain,(
% 38.81/5.95 ~$less(0,sK9) | $less(sK9,sK13) | sK9 = sK13),
% 38.81/5.95 inference(resolution,[],[f1303,f57])).
% 38.81/5.95 tff(f1901,plain,(
% 38.81/5.95 $less(sK9,sK13) | sK9 = sK13 | 0 = sK9),
% 38.81/5.95 inference(resolution,[],[f1305,f673])).
% 38.81/5.95 tff(f2299,plain,(
% 38.81/5.95 ( ! [X0 : $int] : ($less(sF17,X0) | $less(X0,sF30) | 0 = sK9) )),
% 38.81/5.95 inference(superposition,[],[f585,f805])).
% 38.81/5.95 tff(f2301,plain,(
% 38.81/5.95 ( ! [X0 : $int] : ($less(X0,0) | $less($uminus(1),X0)) )),
% 38.81/5.95 inference(superposition,[],[f585,f54])).
% 38.81/5.95 tff(f2304,plain,(
% 38.81/5.95 ( ! [X0 : $int] : ($less(X0,0) | $less(-1,X0)) )),
% 38.81/5.95 inference(evaluation,[],[f2301])).
% 38.81/5.95 tff(f2306,plain,(
% 38.81/5.95 $less(sF17,sF30) | 0 = sK9),
% 38.81/5.95 inference(resolution,[],[f2299,f55])).
% 38.81/5.95 tff(f2412,plain,(
% 38.81/5.95 ~$less(-1,1) | ~$less(n,sF41)),
% 38.81/5.95 inference(resolution,[],[f753,f590])).
% 38.81/5.95 tff(f2418,plain,(
% 38.81/5.95 ~$less(n,sF41)),
% 38.81/5.95 inference(evaluation,[],[f2412])).
% 38.81/5.95 tff(f2765,plain,(
% 38.81/5.95 $sum(-1,0) = $sum(sF41,$uminus(n))),
% 38.81/5.95 inference(superposition,[],[f888,f54])).
% 38.81/5.95 tff(f2771,plain,(
% 38.81/5.95 -1 = $sum(sF41,$uminus(n))),
% 38.81/5.95 inference(evaluation,[],[f2765])).
% 38.81/5.95 tff(f8908,plain,(
% 38.81/5.95 ~$less(tb2t(get(int,int,sF14,sF18)),sF30) | ~$less(sK9,sK13) | ~$less(sK13,sK8)),
% 38.81/5.95 inference(superposition,[],[f1174,f194])).
% 38.81/5.95 tff(f8919,plain,(
% 38.81/5.95 ~$less(tb2t(get(int,int,sF14,sF18)),sF30) | ~$less(sK9,sK13)),
% 38.81/5.95 inference(forward_subsumption_resolution,[],[f8908,f177])).
% 38.81/5.95 tff(f8923,plain,(
% 38.81/5.95 ~$less(tb2t(sF19),sF30) | ~$less(sK9,sK13)),
% 38.81/5.95 inference(forward_demodulation,[],[f8919,f196])).
% 38.81/5.95 tff(f8925,plain,(
% 38.81/5.95 ~$less(sF20,sF30) | ~$less(sK9,sK13)),
% 38.81/5.95 inference(forward_demodulation,[],[f8923,f198])).
% 38.81/5.95 tff(f8943,plain,(
% 38.81/5.95 ~$less(sK9,sK13) | $less(sF17,sF20) | 0 = sK9),
% 38.81/5.95 inference(resolution,[],[f8925,f2299])).
% 38.81/5.95 tff(f8946,plain,(
% 38.81/5.95 ~$less(sK9,sK13) | 0 = sK9),
% 38.81/5.95 inference(forward_subsumption_resolution,[],[f8943,f199])).
% 38.81/5.95 tff(f8966,plain,(
% 38.81/5.95 0 = sK9 | sK9 = sK13 | 0 = sK9),
% 38.81/5.95 inference(resolution,[],[f8946,f1901])).
% 38.81/5.95 tff(f8967,plain,(
% 38.81/5.95 sK9 = sK13 | 0 = sK9),
% 38.81/5.95 inference(duplicate_literal_removal,[],[f8966])).
% 38.81/5.95 tff(f8998,plain,(
% 38.81/5.95 t2tb(sK9) = sF18 | 0 = sK9),
% 38.81/5.95 inference(superposition,[],[f194,f8967])).
% 38.81/5.95 tff(f9058,plain,(
% 38.81/5.95 sF18 = sF22 | 0 = sK9),
% 38.81/5.95 inference(forward_demodulation,[],[f8998,f203])).
% 38.81/5.95 tff(f9111,plain,(
% 38.81/5.95 sF19 = get(int,int,sF14,sF22) | 0 = sK9),
% 38.81/5.95 inference(superposition,[],[f196,f9058])).
% 38.81/5.95 tff(f9129,plain,(
% 38.81/5.95 sF19 = sF29 | 0 = sK9),
% 38.81/5.95 inference(forward_demodulation,[],[f9111,f221])).
% 38.81/5.95 tff(f9146,plain,(
% 38.81/5.95 tb2t(sF19) = sF30 | 0 = sK9),
% 38.81/5.95 inference(superposition,[],[f223,f9129])).
% 38.81/5.95 tff(f9155,plain,(
% 38.81/5.95 sF20 = sF30 | 0 = sK9),
% 38.81/5.95 inference(forward_demodulation,[],[f9146,f198])).
% 38.81/5.95 tff(f9185,plain,(
% 38.81/5.95 ~$less(sF17,sF30) | 0 = sK9),
% 38.81/5.95 inference(superposition,[],[f199,f9155])).
% 38.81/5.95 tff(f9205,plain,(
% 38.81/5.95 0 = sK9),
% 38.81/5.95 inference(forward_subsumption_resolution,[],[f9185,f2306])).
% 38.81/5.95 tff(f9216,plain,(
% 38.81/5.95 $less(0,sK8)),
% 38.81/5.95 inference(superposition,[],[f167,f9205])).
% 38.81/5.95 tff(f9219,plain,(
% 38.81/5.95 t2tb(0) = sF22),
% 38.81/5.95 inference(superposition,[],[f203,f9205])).
% 38.81/5.95 tff(f9267,plain,(
% 38.81/5.95 sF22 = sF32),
% 38.81/5.95 inference(forward_demodulation,[],[f9219,f229])).
% 38.81/5.95 tff(f9331,plain,(
% 38.81/5.95 sF23 = get(int,int,sF21,sF32)),
% 38.81/5.95 inference(superposition,[],[f205,f9267])).
% 38.81/5.95 tff(f9332,plain,(
% 38.81/5.95 sF15 = get(int,int,sF21,sF32)),
% 38.81/5.95 inference(forward_demodulation,[],[f9331,f428])).
% 38.81/5.95 tff(f10006,plain,(
% 38.81/5.95 sF15 = sF35),
% 38.81/5.95 inference(superposition,[],[f236,f9332])).
% 38.81/5.95 tff(f10044,plain,(
% 38.81/5.95 -1 = tb2t(sF15)),
% 38.81/5.95 inference(superposition,[],[f280,f10006])).
% 38.81/5.95 tff(f10078,plain,(
% 38.81/5.95 sK12 = -1),
% 38.81/5.95 inference(superposition,[],[f407,f10044])).
% 38.81/5.95 tff(f10116,plain,(
% 38.81/5.95 ~$less(-1,sF26)),
% 38.81/5.95 inference(superposition,[],[f282,f10078])).
% 38.81/5.95 tff(f35705,plain,(
% 38.81/5.95 $less(-1,sF26) | ~$less(0,sK8) | ~$less(sK8,n)),
% 38.81/5.95 inference(resolution,[],[f2304,f841])).
% 38.81/5.95 tff(f35764,plain,(
% 38.81/5.95 ~$less(0,sK8) | ~$less(sK8,n)),
% 38.81/5.95 inference(forward_subsumption_resolution,[],[f35705,f10116])).
% 38.81/5.95 tff(f35777,plain,(
% 38.81/5.95 ~$less(sK8,n)),
% 38.81/5.95 inference(forward_subsumption_resolution,[],[f35764,f9216])).
% 38.81/5.95 tff(f35806,plain,(
% 38.81/5.95 $less(n,sK8) | n = sK8),
% 38.81/5.95 inference(resolution,[],[f35777,f57])).
% 38.81/5.95 tff(f36574,plain,(
% 38.81/5.95 n = sK8 | sK8 = sF41 | $less(n,sF41)),
% 38.81/5.95 inference(resolution,[],[f35806,f816])).
% 38.81/5.95 tff(f36588,plain,(
% 38.81/5.95 sK8 = sF41 | n = sK8),
% 38.81/5.95 inference(forward_subsumption_resolution,[],[f36574,f2418])).
% 38.81/5.95 tff(f37360,plain,(
% 38.81/5.95 ~$less(n,sK8) | n = sK8),
% 38.81/5.95 inference(superposition,[],[f2418,f36588])).
% 38.81/5.95 tff(f37398,plain,(
% 38.81/5.95 n = sK8),
% 38.81/5.95 inference(forward_subsumption_resolution,[],[f37360,f35806])).
% 38.81/5.95 tff(f37422,plain,(
% 38.81/5.95 $less(n,sF41) | n = sF41),
% 38.81/5.95 inference(superposition,[],[f680,f37398])).
% 38.81/5.95 tff(f37559,plain,(
% 38.81/5.95 n = sF41),
% 38.81/5.95 inference(forward_subsumption_resolution,[],[f37422,f2418])).
% 38.81/5.95 tff(f37653,plain,(
% 38.81/5.95 -1 = $sum(n,$uminus(n))),
% 38.81/5.95 inference(superposition,[],[f2771,f37559])).
% 38.81/5.95 tff(f37703,plain,(
% 38.81/5.95 0 = -1),
% 38.81/5.95 inference(forward_demodulation,[],[f37653,f54])).
% 38.81/5.95 tff(f37704,plain,(
% 38.81/5.95 $false),
% 38.81/5.95 inference(evaluation,[],[f37703])).
% 38.81/5.95 % SZS output end Proof for theBenchmark
% 38.81/5.95 % (4031116)------------------------------
% 38.81/5.95 % (4031116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.81/5.95 % (4031116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.81/5.95 % (4031116)CaDiCaL version: 2.1.3
% 38.81/5.95 % (4031116)Termination reason: Refutation
% 38.81/5.95 % (4031116)Time elapsed: 4.398 s
% 38.81/5.95 % (4031116)Peak memory usage: 25 MB
% 38.81/5.95 % (4031116)Instructions burned: 4564 (million)
% 38.81/5.95 % (4031061)Success in time 5.615 s
% 38.81/5.95 % Vampire exiting
%------------------------------------------------------------------------------