%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW664_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 : n010.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:36 PM UTC 2026
% Result : Theorem 73.81s 10.87s
% Output : Refutation 73.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW664_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.26 % Computer : n010.cluster.edu
% 0.10/0.26 % Model : x86_64 x86_64
% 0.10/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.26 % Memory : 8046.5625MB
% 0.10/0.26 % OS : Linux 6.8.0-71-generic
% 0.10/0.26 % CPULimit : 300
% 0.10/0.26 % WCLimit : 300
% 0.10/0.26 % DateTime : Mon Sep 28 14:25:02 UTC 2026
% 0.10/0.27 % CPUTime :
% 0.10/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.26/0.31 Running first-order model finding
% 0.26/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
% 5.26/1.08 % (1957278)Will run a generic schedule for satisfiability detection.
% 5.26/1.08 % (1957287)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4128391975:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.26/1.08 % (1957284)% WARNING: option uhcvi not known.
% 5.26/1.08 % (1957284)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3535884029:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.26/1.08 % (1957283)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3842438199_2999 on theBenchmark for (2999ds/0Mi)
% 5.26/1.08 % (1957285)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2148676103:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.26/1.08 % (1957286)dis+10_1_sil=32000:sp=arity:random_seed=1543299732:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.26/1.08 % (1957288)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=840761610:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.26/1.08 % (1957289)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=311154701:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.26/1.08 % (1957283)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.26/1.08 % (1957283)Terminated due to inappropriate strategy.
% 5.26/1.08 % (1957283)------------------------------
% 5.26/1.08 % (1957283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.08 % (1957283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.08 % (1957283)CaDiCaL version: 2.1.3
% 5.26/1.08 % (1957283)Termination reason: Inappropriate
% 5.26/1.08 % (1957283)Time elapsed: 0.009 s
% 5.26/1.08 % (1957283)Peak memory usage: 10 MB
% 5.26/1.08 % (1957283)Instructions burned: 9 (million)
% 5.26/1.08 % (1957283)------------------------------
% 5.26/1.08 % (1957283)------------------------------
% 5.26/1.08 % (1957297)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3922989939:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.26/1.08 % (1957287)Instruction limit reached!
% 5.26/1.08 % (1957287)------------------------------
% 5.26/1.08 % (1957287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.08 % (1957287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.08 % (1957287)CaDiCaL version: 2.1.3
% 5.26/1.08 % (1957287)Termination reason: Instruction limit
% 5.26/1.08 % (1957287)Termination phase: Saturation
% 5.26/1.08 % (1957287)Time elapsed: 0.064 s
% 5.26/1.08 % (1957287)Peak memory usage: 13 MB
% 5.26/1.08 % (1957287)Instructions burned: 116 (million)
% 5.26/1.08 % (1957297)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.26/1.08 % (1957297)Terminated due to inappropriate strategy.
% 5.26/1.08 % (1957297)------------------------------
% 5.26/1.08 % (1957297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.08 % (1957297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.08 % (1957297)CaDiCaL version: 2.1.3
% 5.26/1.08 % (1957297)Termination reason: Inappropriate
% 5.26/1.08 % (1957297)Time elapsed: 0.008 s
% 5.26/1.08 % (1957297)Peak memory usage: 10 MB
% 5.26/1.08 % (1957297)Instructions burned: 8 (million)
% 5.26/1.08 % (1957297)------------------------------
% 5.26/1.08 % (1957297)------------------------------
% 5.26/1.08 % (1957299)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1492374433:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.26/1.08 % (1957300)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=1548015074:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 5.26/1.08 % (1957286)Instruction limit reached!
% 5.26/1.08 % (1957286)------------------------------
% 5.26/1.08 % (1957286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.08 % (1957286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.08 % (1957286)CaDiCaL version: 2.1.3
% 5.26/1.08 % (1957286)Termination reason: Instruction limit
% 5.26/1.08 % (1957286)Termination phase: Saturation
% 5.26/1.08 % (1957286)Time elapsed: 0.105 s
% 5.26/1.08 % (1957286)Peak memory usage: 13 MB
% 5.26/1.08 % (1957286)Instructions burned: 103 (million)
% 5.26/1.08 % (1957288)Instruction limit reached!
% 5.26/1.08 % (1957288)------------------------------
% 5.26/1.08 % (1957288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.31/1.82 % (1957288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/1.82 % (1957288)CaDiCaL version: 2.1.3
% 8.31/1.82 % (1957288)Termination reason: Instruction limit
% 8.31/1.82 % (1957288)Termination phase: Saturation
% 8.31/1.82 % (1957288)Time elapsed: 0.136 s
% 8.31/1.82 % (1957288)Peak memory usage: 13 MB
% 8.31/1.82 % (1957288)Instructions burned: 131 (million)
% 8.31/1.82 % (1957303)ott-21_1_sil=16000:fs=off:random_seed=119974277:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.31/1.82 % (1957299)Instruction limit reached!
% 8.31/1.82 % (1957299)------------------------------
% 8.31/1.82 % (1957299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.31/1.82 % (1957299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/1.82 % (1957299)CaDiCaL version: 2.1.3
% 8.31/1.82 % (1957299)Termination reason: Instruction limit
% 8.31/1.82 % (1957299)Termination phase: Saturation
% 8.31/1.82 % (1957299)Time elapsed: 0.085 s
% 8.31/1.82 % (1957299)Peak memory usage: 13 MB
% 8.31/1.82 % (1957299)Instructions burned: 132 (million)
% 8.31/1.82 % (1957304)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3330165330:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.31/1.82 % (1957306)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2676680006:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 8.31/1.82 % (1957289)Instruction limit reached!
% 8.31/1.82 % (1957289)------------------------------
% 8.31/1.82 % (1957289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.31/1.82 % (1957289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/1.82 % (1957289)CaDiCaL version: 2.1.3
% 8.31/1.82 % (1957289)Termination reason: Instruction limit
% 8.31/1.82 % (1957289)Termination phase: Saturation
% 8.31/1.82 % (1957289)Time elapsed: 0.177 s
% 8.31/1.82 % (1957289)Peak memory usage: 14 MB
% 8.31/1.82 % (1957289)Instructions burned: 159 (million)
% 8.31/1.82 % (1957306)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.31/1.82 % (1957306)Terminated due to inappropriate strategy.
% 8.31/1.82 % (1957306)------------------------------
% 8.31/1.82 % (1957306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.31/1.82 % (1957306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/1.82 % (1957306)CaDiCaL version: 2.1.3
% 8.31/1.82 % (1957306)Termination reason: Inappropriate
% 8.31/1.82 % (1957306)Time elapsed: 0.004 s
% 8.31/1.82 % (1957306)Peak memory usage: 10 MB
% 8.31/1.82 % (1957306)Instructions burned: 8 (million)
% 8.31/1.82 % (1957306)------------------------------
% 8.31/1.82 % (1957306)------------------------------
% 8.31/1.82 % (1957310)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3200106457:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 8.31/1.82 % (1957310)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.31/1.82 % (1957310)Terminated due to inappropriate strategy.
% 8.31/1.82 % (1957310)------------------------------
% 8.31/1.82 % (1957310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.31/1.82 % (1957310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/1.82 % (1957310)CaDiCaL version: 2.1.3
% 8.31/1.82 % (1957310)Termination reason: Inappropriate
% 8.31/1.82 % (1957310)Time elapsed: 0.004 s
% 8.31/1.82 % (1957310)Peak memory usage: 11 MB
% 8.31/1.82 % (1957310)Instructions burned: 8 (million)
% 8.31/1.82 % (1957310)------------------------------
% 8.31/1.82 % (1957310)------------------------------
% 8.31/1.82 % (1957309)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3749361286:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 8.31/1.82 % (1957312)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=3294539123:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 8.31/1.82 % (1957303)Instruction limit reached!
% 8.31/1.82 % (1957303)------------------------------
% 8.31/1.82 % (1957303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.31/1.82 % (1957303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.31/1.82 % (1957303)CaDiCaL version: 2.1.3
% 8.31/1.82 % (1957303)Termination reason: Instruction limit
% 8.31/1.82 % (1957303)Termination phase: Saturation
% 35.45/5.39 % (1957303)Time elapsed: 0.164 s
% 35.45/5.39 % (1957303)Peak memory usage: 13 MB
% 35.45/5.39 % (1957303)Instructions burned: 180 (million)
% 35.45/5.39 % (1957317)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3018835255:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 35.45/5.39 % (1957312)Instruction limit reached!
% 35.45/5.39 % (1957312)------------------------------
% 35.45/5.39 % (1957312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.45/5.39 % (1957312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.45/5.39 % (1957312)CaDiCaL version: 2.1.3
% 35.45/5.39 % (1957312)Termination reason: Instruction limit
% 35.45/5.39 % (1957312)Termination phase: Saturation
% 35.45/5.39 % (1957312)Time elapsed: 0.400 s
% 35.45/5.39 % (1957312)Peak memory usage: 19 MB
% 35.45/5.39 % (1957312)Instructions burned: 693 (million)
% 35.45/5.39 % (1957319)fmb+10_1_sil=64000:random_seed=3193008253:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 35.45/5.39 % (1957319)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 35.45/5.39 % (1957319)Terminated due to inappropriate strategy.
% 35.45/5.39 % (1957319)------------------------------
% 35.45/5.39 % (1957319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.45/5.39 % (1957319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.45/5.39 % (1957319)CaDiCaL version: 2.1.3
% 35.45/5.39 % (1957319)Termination reason: Inappropriate
% 35.45/5.39 % (1957319)Time elapsed: 0.004 s
% 35.45/5.39 % (1957319)Peak memory usage: 11 MB
% 35.45/5.39 % (1957319)Instructions burned: 8 (million)
% 35.45/5.39 % (1957319)------------------------------
% 35.45/5.39 % (1957319)------------------------------
% 35.45/5.39 % (1957321)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3752020115:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi)
% 35.45/5.39 % (1957321)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 35.45/5.39 % (1957321)Terminated due to inappropriate strategy.
% 35.45/5.39 % (1957321)------------------------------
% 35.45/5.39 % (1957321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.45/5.39 % (1957321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.45/5.39 % (1957321)CaDiCaL version: 2.1.3
% 35.45/5.39 % (1957321)Termination reason: Inappropriate
% 35.45/5.39 % (1957321)Time elapsed: 0.004 s
% 35.45/5.39 % (1957321)Peak memory usage: 11 MB
% 35.45/5.39 % (1957321)Instructions burned: 8 (million)
% 35.45/5.39 % (1957321)------------------------------
% 35.45/5.39 % (1957321)------------------------------
% 35.45/5.39 % (1957323)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4242837956:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi)
% 35.45/5.39 % (1957304)Instruction limit reached!
% 35.45/5.39 % (1957304)------------------------------
% 35.45/5.39 % (1957304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.45/5.39 % (1957304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.45/5.39 % (1957304)CaDiCaL version: 2.1.3
% 35.45/5.39 % (1957304)Termination reason: Instruction limit
% 35.45/5.39 % (1957304)Termination phase: Saturation
% 35.45/5.39 % (1957304)Time elapsed: 0.534 s
% 35.45/5.39 % (1957304)Peak memory usage: 14 MB
% 35.45/5.39 % (1957304)Instructions burned: 477 (million)
% 35.45/5.39 % (1957323)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 35.45/5.39 % (1957323)Terminated due to inappropriate strategy.
% 35.45/5.39 % (1957323)------------------------------
% 35.45/5.39 % (1957323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.45/5.39 % (1957323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.45/5.39 % (1957323)CaDiCaL version: 2.1.3
% 35.45/5.39 % (1957323)Termination reason: Inappropriate
% 35.45/5.39 % (1957323)Time elapsed: 0.004 s
% 35.45/5.39 % (1957323)Peak memory usage: 11 MB
% 35.45/5.39 % (1957323)Instructions burned: 8 (million)
% 35.45/5.39 % (1957323)------------------------------
% 35.45/5.39 % (1957323)------------------------------
% 35.45/5.39 % (1957300)Instruction limit reached!
% 35.45/5.39 % (1957300)------------------------------
% 35.45/5.39 % (1957300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.45/5.39 % (1957300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.45/5.39 % (1957300)CaDiCaL version: 2.1.3
% 35.45/5.39 % (1957300)Termination reason: Instruction limit
% 35.45/5.39 % (1957300)Termination phase: Saturation
% 43.69/6.60 % (1957300)Time elapsed: 0.629 s
% 43.69/6.60 % (1957300)Peak memory usage: 17 MB
% 43.69/6.60 % (1957300)Instructions burned: 685 (million)
% 43.69/6.60 % (1957326)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1851769245:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 43.69/6.60 % (1957325)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=952090202:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 43.69/6.60 % (1957327)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3055371030:i=6324_2992 on theBenchmark for (2992ds/6324Mi)
% 43.69/6.60 % (1957327)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 43.69/6.60 % (1957327)Terminated due to inappropriate strategy.
% 43.69/6.60 % (1957327)------------------------------
% 43.69/6.60 % (1957327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.69/6.60 % (1957327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.69/6.60 % (1957327)CaDiCaL version: 2.1.3
% 43.69/6.60 % (1957327)Termination reason: Inappropriate
% 43.69/6.60 % (1957327)Time elapsed: 0.009 s
% 43.69/6.60 % (1957327)Peak memory usage: 11 MB
% 43.69/6.60 % (1957327)Instructions burned: 8 (million)
% 43.69/6.60 % (1957327)------------------------------
% 43.69/6.60 % (1957327)------------------------------
% 43.69/6.60 % (1957331)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2727755631:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi)
% 43.69/6.60 % (1957331)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 43.69/6.60 % (1957331)Terminated due to inappropriate strategy.
% 43.69/6.60 % (1957331)------------------------------
% 43.69/6.60 % (1957331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.69/6.60 % (1957331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.69/6.60 % (1957331)CaDiCaL version: 2.1.3
% 43.69/6.60 % (1957331)Termination reason: Inappropriate
% 43.69/6.60 % (1957331)Time elapsed: 0.008 s
% 43.69/6.60 % (1957331)Peak memory usage: 11 MB
% 43.69/6.60 % (1957331)Instructions burned: 8 (million)
% 43.69/6.60 % (1957331)------------------------------
% 43.69/6.60 % (1957331)------------------------------
% 43.69/6.60 % (1957333)ott-2_1_sil=16000:newcnf=on:random_seed=3103387062:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi)
% 43.69/6.60 % (1957317)Instruction limit reached!
% 43.69/6.60 % (1957317)------------------------------
% 43.69/6.60 % (1957317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.69/6.60 % (1957317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.69/6.60 % (1957317)CaDiCaL version: 2.1.3
% 43.69/6.60 % (1957317)Termination reason: Instruction limit
% 43.69/6.60 % (1957317)Termination phase: Saturation
% 43.69/6.60 % (1957317)Time elapsed: 0.871 s
% 43.69/6.60 % (1957317)Peak memory usage: 19 MB
% 43.69/6.60 % (1957317)Instructions burned: 879 (million)
% 43.69/6.60 % (1957335)ott+10_1_sil=32000:tgt=ground:random_seed=3475636043:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi)
% 43.69/6.60 % (1957309)Instruction limit reached!
% 43.69/6.60 % (1957309)------------------------------
% 43.69/6.60 % (1957309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.69/6.60 % (1957309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.69/6.60 % (1957309)CaDiCaL version: 2.1.3
% 43.69/6.60 % (1957309)Termination reason: Instruction limit
% 43.69/6.60 % (1957309)Termination phase: Saturation
% 43.69/6.60 % (1957309)Time elapsed: 1.191 s
% 43.69/6.60 % (1957309)Peak memory usage: 22 MB
% 43.69/6.60 % (1957309)Instructions burned: 1179 (million)
% 43.69/6.60 % (1957326)Instruction limit reached!
% 43.69/6.60 % (1957326)------------------------------
% 43.69/6.60 % (1957326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.69/6.60 % (1957326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.69/6.60 % (1957326)CaDiCaL version: 2.1.3
% 43.69/6.60 % (1957326)Termination reason: Instruction limit
% 43.69/6.60 % (1957326)Termination phase: Saturation
% 43.69/6.60 % (1957326)Time elapsed: 0.703 s
% 43.69/6.60 % (1957326)Peak memory usage: 24 MB
% 43.69/6.60 % (1957326)Instructions burned: 1474 (million)
% 43.69/6.60 % (1957337)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2021017416:i=54282_2985 on theBenchmark for (2985ds/54282Mi)
% 43.69/6.60 % (1957337)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 73.81/10.87 % (1957337)Terminated due to inappropriate strategy.
% 73.81/10.87 % (1957337)------------------------------
% 73.81/10.87 % (1957337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957337)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957337)Termination reason: Inappropriate
% 73.81/10.87 % (1957337)Time elapsed: 0.009 s
% 73.81/10.87 % (1957337)Peak memory usage: 11 MB
% 73.81/10.87 % (1957337)Instructions burned: 9 (million)
% 73.81/10.87 % (1957337)------------------------------
% 73.81/10.87 % (1957337)------------------------------
% 73.81/10.87 % (1957338)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=795452751:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi)
% 73.81/10.87 % (1957341)dis+21_1_sil=32000:sas=cadical:random_seed=4160915802:i=3773:amm=off_2985 on theBenchmark for (2985ds/3773Mi)
% 73.81/10.87 % (1957333)Instruction limit reached!
% 73.81/10.87 % (1957333)------------------------------
% 73.81/10.87 % (1957333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957333)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957333)Termination reason: Instruction limit
% 73.81/10.87 % (1957333)Termination phase: Saturation
% 73.81/10.87 % (1957333)Time elapsed: 0.794 s
% 73.81/10.87 % (1957333)Peak memory usage: 18 MB
% 73.81/10.87 % (1957333)Instructions burned: 870 (million)
% 73.81/10.87 % (1957343)ott+11_1_sil=16000:gs=on:random_seed=673462650:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2983 on theBenchmark for (2983ds/2251Mi)
% 73.81/10.87 % (1957338)Instruction limit reached!
% 73.81/10.87 % (1957338)------------------------------
% 73.81/10.87 % (1957338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957338)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957338)Termination reason: Instruction limit
% 73.81/10.87 % (1957338)Termination phase: Saturation
% 73.81/10.87 % (1957338)Time elapsed: 1.791 s
% 73.81/10.87 % (1957338)Peak memory usage: 31 MB
% 73.81/10.87 % (1957338)Instructions burned: 3512 (million)
% 73.81/10.87 % (1957353)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3092780792:fmbsr=1.6:i=67534_2967 on theBenchmark for (2967ds/67534Mi)
% 73.81/10.87 % (1957353)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 73.81/10.87 % (1957353)Terminated due to inappropriate strategy.
% 73.81/10.87 % (1957353)------------------------------
% 73.81/10.87 % (1957353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957353)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957353)Termination reason: Inappropriate
% 73.81/10.87 % (1957353)Time elapsed: 0.004 s
% 73.81/10.87 % (1957353)Peak memory usage: 11 MB
% 73.81/10.87 % (1957353)Instructions burned: 8 (million)
% 73.81/10.87 % (1957353)------------------------------
% 73.81/10.87 % (1957353)------------------------------
% 73.81/10.87 % (1957355)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4294647309:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2966 on theBenchmark for (2966ds/4591Mi)
% 73.81/10.87 % (1957343)Instruction limit reached!
% 73.81/10.87 % (1957343)------------------------------
% 73.81/10.87 % (1957343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957343)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957343)Termination reason: Instruction limit
% 73.81/10.87 % (1957343)Termination phase: Saturation
% 73.81/10.87 % (1957343)Time elapsed: 2.008 s
% 73.81/10.87 % (1957343)Peak memory usage: 18 MB
% 73.81/10.87 % (1957343)Instructions burned: 2252 (million)
% 73.81/10.87 % (1957361)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2006035564:i=29340_2962 on theBenchmark for (2962ds/29340Mi)
% 73.81/10.87 % (1957341)Instruction limit reached!
% 73.81/10.87 % (1957341)------------------------------
% 73.81/10.87 % (1957341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957341)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957341)Termination reason: Instruction limit
% 73.81/10.87 % (1957341)Termination phase: Saturation
% 73.81/10.87 % (1957341)Time elapsed: 3.529 s
% 73.81/10.87 % (1957341)Peak memory usage: 33 MB
% 73.81/10.87 % (1957341)Instructions burned: 3773 (million)
% 73.81/10.87 % (1957363)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=850891287:i=5211_2949 on theBenchmark for (2949ds/5211Mi)
% 73.81/10.87 % (1957325)Instruction limit reached!
% 73.81/10.87 % (1957325)------------------------------
% 73.81/10.87 % (1957325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957325)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957325)Termination reason: Instruction limit
% 73.81/10.87 % (1957325)Termination phase: Saturation
% 73.81/10.87 % (1957325)Time elapsed: 4.599 s
% 73.81/10.87 % (1957325)Peak memory usage: 34 MB
% 73.81/10.87 % (1957325)Instructions burned: 5132 (million)
% 73.81/10.87 % (1957365)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=892247567:i=5497:nm=2_2946 on theBenchmark for (2946ds/5497Mi)
% 73.81/10.87 % (1957365)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 73.81/10.87 % (1957365)Terminated due to inappropriate strategy.
% 73.81/10.87 % (1957365)------------------------------
% 73.81/10.87 % (1957365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957365)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957365)Termination reason: Inappropriate
% 73.81/10.87 % (1957365)Time elapsed: 0.006 s
% 73.81/10.87 % (1957365)Peak memory usage: 11 MB
% 73.81/10.87 % (1957365)Instructions burned: 8 (million)
% 73.81/10.87 % (1957365)------------------------------
% 73.81/10.87 % (1957365)------------------------------
% 73.81/10.87 % (1957367)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2173236164:fmbsr=2:i=46332_2945 on theBenchmark for (2945ds/46332Mi)
% 73.81/10.87 % (1957367)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 73.81/10.87 % (1957367)Terminated due to inappropriate strategy.
% 73.81/10.87 % (1957367)------------------------------
% 73.81/10.87 % (1957367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957367)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957367)Termination reason: Inappropriate
% 73.81/10.87 % (1957367)Time elapsed: 0.006 s
% 73.81/10.87 % (1957367)Peak memory usage: 11 MB
% 73.81/10.87 % (1957367)Instructions burned: 8 (million)
% 73.81/10.87 % (1957367)------------------------------
% 73.81/10.87 % (1957367)------------------------------
% 73.81/10.87 % (1957369)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1305222115:i=14071_2945 on theBenchmark for (2945ds/14071Mi)
% 73.81/10.87 % (1957369)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 73.81/10.87 % (1957369)Terminated due to inappropriate strategy.
% 73.81/10.87 % (1957369)------------------------------
% 73.81/10.87 % (1957369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957369)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957369)Termination reason: Inappropriate
% 73.81/10.87 % (1957369)Time elapsed: 0.008 s
% 73.81/10.87 % (1957369)Peak memory usage: 11 MB
% 73.81/10.87 % (1957369)Instructions burned: 8 (million)
% 73.81/10.87 % (1957369)------------------------------
% 73.81/10.87 % (1957369)------------------------------
% 73.81/10.87 % (1957371)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1004607065:i=22565:add=on:rawr=on_2945 on theBenchmark for (2945ds/22565Mi)
% 73.81/10.87 % (1957355)Instruction limit reached!
% 73.81/10.87 % (1957355)------------------------------
% 73.81/10.87 % (1957355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957355)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957355)Termination reason: Instruction limit
% 73.81/10.87 % (1957355)Termination phase: Saturation
% 73.81/10.87 % (1957355)Time elapsed: 2.534 s
% 73.81/10.87 % (1957355)Peak memory usage: 50 MB
% 73.81/10.87 % (1957355)Instructions burned: 4594 (million)
% 73.81/10.87 % (1957373)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4029638497:i=8173:av=off_2941 on theBenchmark for (2941ds/8173Mi)
% 73.81/10.87 % (1957335)Instruction limit reached!
% 73.81/10.87 % (1957335)------------------------------
% 73.81/10.87 % (1957335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957335)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957335)Termination reason: Instruction limit
% 73.81/10.87 % (1957335)Termination phase: Saturation
% 73.81/10.87 % (1957335)Time elapsed: 4.990 s
% 73.81/10.87 % (1957335)Peak memory usage: 38 MB
% 73.81/10.87 % (1957335)Instructions burned: 5115 (million)
% 73.81/10.87 % (1957375)dis+10_16:1_sil=16000:random_seed=2128673319:i=9155:fsr=off_2937 on theBenchmark for (2937ds/9155Mi)
% 73.81/10.87 % (1957363)Instruction limit reached!
% 73.81/10.87 % (1957363)------------------------------
% 73.81/10.87 % (1957363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957363)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957363)Termination reason: Instruction limit
% 73.81/10.87 % (1957363)Termination phase: Saturation
% 73.81/10.87 % (1957363)Time elapsed: 4.720 s
% 73.81/10.87 % (1957363)Peak memory usage: 48 MB
% 73.81/10.87 % (1957363)Instructions burned: 5211 (million)
% 73.81/10.87 % (1957379)ott-3_8_sil=64000:random_seed=2523934668:i=20139:bs=on_2901 on theBenchmark for (2901ds/20139Mi)
% 73.81/10.87 % (1957373)Instruction limit reached!
% 73.81/10.87 % (1957373)------------------------------
% 73.81/10.87 % (1957373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957373)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957373)Termination reason: Instruction limit
% 73.81/10.87 % (1957373)Termination phase: Saturation
% 73.81/10.87 % (1957373)Time elapsed: 4.427 s
% 73.81/10.87 % (1957373)Peak memory usage: 64 MB
% 73.81/10.87 % (1957373)Instructions burned: 8175 (million)
% 73.81/10.87 % (1957383)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2087491973:fmbsr=2:i=32576_2896 on theBenchmark for (2896ds/32576Mi)
% 73.81/10.87 % (1957383)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 73.81/10.87 % (1957383)Terminated due to inappropriate strategy.
% 73.81/10.87 % (1957383)------------------------------
% 73.81/10.87 % (1957383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957383)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957383)Termination reason: Inappropriate
% 73.81/10.87 % (1957383)Time elapsed: 0.005 s
% 73.81/10.87 % (1957383)Peak memory usage: 11 MB
% 73.81/10.87 % (1957383)Instructions burned: 9 (million)
% 73.81/10.87 % (1957383)------------------------------
% 73.81/10.87 % (1957383)------------------------------
% 73.81/10.87 % (1957385)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3414505448:i=11404_2896 on theBenchmark for (2896ds/11404Mi)
% 73.81/10.87 % (1957385) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1957278-1957385"...
% 73.81/10.87 % (1957385)...printing done.
% 73.81/10.87 % (1957385)Refutation found. Thanks to Tanya!
% 73.81/10.87 % SZS status Theorem for theBenchmark
% 73.81/10.87 % SZS output start Proof for theBenchmark
% 73.81/10.87 tff(type_def_5, type, uni: $tType).
% 73.81/10.87 tff(type_def_6, type, ty: $tType).
% 73.81/10.87 tff(type_def_7, type, bool1: $tType).
% 73.81/10.87 tff(type_def_8, type, tuple02: $tType).
% 73.81/10.87 tff(type_def_9, type, map_int_int: $tType).
% 73.81/10.87 tff(type_def_10, type, array_int: $tType).
% 73.81/10.87 tff(func_def_0, type, witness1: ty > uni).
% 73.81/10.87 tff(func_def_1, type, int: ty).
% 73.81/10.87 tff(func_def_2, type, real: ty).
% 73.81/10.87 tff(func_def_3, type, bool: ty).
% 73.81/10.87 tff(func_def_4, type, true1: bool1).
% 73.81/10.87 tff(func_def_5, type, false1: bool1).
% 73.81/10.87 tff(func_def_6, type, match_bool1: (ty * bool1 * uni * uni) > uni).
% 73.81/10.87 tff(func_def_7, type, tuple0: ty).
% 73.81/10.87 tff(func_def_8, type, tuple03: tuple02).
% 73.81/10.87 tff(func_def_9, type, qtmark: ty).
% 73.81/10.87 tff(func_def_12, type, abs1: $int > $int).
% 73.81/10.87 tff(func_def_14, type, div1: ($int * $int) > $int).
% 73.81/10.87 tff(func_def_15, type, mod1: ($int * $int) > $int).
% 73.81/10.87 tff(func_def_18, type, power1: ($int * $int) > $int).
% 73.81/10.87 tff(func_def_20, type, map: (ty * ty) > ty).
% 73.81/10.87 tff(func_def_21, type, get: (ty * ty * uni * uni) > uni).
% 73.81/10.87 tff(func_def_22, type, set: (ty * ty * uni * uni * uni) > uni).
% 73.81/10.87 tff(func_def_23, type, const: (ty * ty * uni) > uni).
% 73.81/10.87 tff(func_def_24, type, array: ty > ty).
% 73.81/10.87 tff(func_def_25, type, mk_array1: (ty * $int * uni) > uni).
% 73.81/10.87 tff(func_def_26, type, length1: (ty * uni) > $int).
% 73.81/10.87 tff(func_def_27, type, elts: (ty * uni) > uni).
% 73.81/10.87 tff(func_def_28, type, get2: (ty * uni * $int) > uni).
% 73.81/10.87 tff(func_def_29, type, t2tb: $int > uni).
% 73.81/10.87 tff(func_def_30, type, tb2t: uni > $int).
% 73.81/10.87 tff(func_def_31, type, set2: (ty * uni * $int * uni) > uni).
% 73.81/10.87 tff(func_def_32, type, make1: (ty * $int * uni) > uni).
% 73.81/10.87 tff(func_def_33, type, sum2: (map_int_int * $int * $int) > $int).
% 73.81/10.87 tff(func_def_34, type, t2tb1: map_int_int > uni).
% 73.81/10.87 tff(func_def_35, type, tb2t1: uni > map_int_int).
% 73.81/10.87 tff(func_def_36, type, sum3: (array_int * $int * $int) > $int).
% 73.81/10.87 tff(func_def_37, type, t2tb2: array_int > uni).
% 73.81/10.87 tff(func_def_38, type, tb2t2: uni > array_int).
% 73.81/10.87 tff(func_def_40, type, go_left1: ($int * $int) > $int).
% 73.81/10.87 tff(func_def_41, type, go_right1: ($int * $int) > $int).
% 73.81/10.87 tff(func_def_42, type, sK1: (map_int_int * map_int_int * $int * $int) > $int).
% 73.81/10.87 tff(func_def_43, type, sK2: $int > $int).
% 73.81/10.87 tff(func_def_44, type, sK3: ($int * $int * array_int * array_int) > $int).
% 73.81/10.87 tff(func_def_45, type, sK4: ($int * $int * array_int * array_int) > $int).
% 73.81/10.87 tff(func_def_46, type, sK5: ($int * $int * array_int * array_int) > array_int).
% 73.81/10.87 tff(func_def_47, type, sK6: ($int * $int * array_int * array_int) > array_int).
% 73.81/10.87 tff(func_def_48, type, sK7: ($int * $int * array_int * array_int) > $int).
% 73.81/10.87 tff(func_def_49, type, sK8: ($int * $int * array_int * array_int) > array_int).
% 73.81/10.87 tff(func_def_50, type, sK9: ($int * $int * array_int * array_int) > array_int).
% 73.81/10.87 tff(func_def_51, type, sK10: ($int * $int * array_int * array_int) > $int).
% 73.81/10.87 tff(func_def_52, type, sK11: ($int * $int * array_int * array_int) > $int).
% 73.81/10.87 tff(func_def_53, type, sK12: $int).
% 73.81/10.87 tff(func_def_54, type, sK13: $int).
% 73.81/10.87 tff(func_def_55, type, sK14: $int).
% 73.81/10.87 tff(func_def_56, type, sK15: map_int_int).
% 73.81/10.87 tff(func_def_57, type, sK16: $int).
% 73.81/10.87 tff(func_def_58, type, sK17: map_int_int).
% 73.81/10.87 tff(pred_def_1, type, sort1: (ty * uni) > $o).
% 73.81/10.87 tff(pred_def_4, type, is_power_of_21: $int > $o).
% 73.81/10.87 tff(pred_def_5, type, phase11: ($int * $int * array_int * array_int) > $o).
% 73.81/10.87 tff(pred_def_6, type, partial_sum1: ($int * $int * array_int * array_int) > $o).
% 73.81/10.87 tff(pred_def_7, type, sP0: ($int * $int * array_int * array_int) > $o).
% 73.81/10.87 tff(f42,axiom,(
% 73.81/10.87 ! [X0 : ty,X1 : $int,X2 : uni] : (sort1(map(int,X0),X2) => elts(X0,mk_array1(X0,X1,X2)) = X2)),
% 73.81/10.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',elts_def1)).
% 73.81/10.87 tff(f48,axiom,(
% 73.81/10.87 ! [X0 : ty,X1 : uni,X2 : $int] : get2(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2))),
% 73.81/10.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',get_def)).
% 73.81/10.87 tff(f53,axiom,(
% 73.81/10.87 ! [X0 : map_int_int,X1 : $int,X2 : $int] : ($lesseq(X2,X1) => sum2(X0,X1,X2) = 0)),
% 73.81/10.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_def_empty)).
% 73.81/10.87 tff(f54,axiom,(
% 73.81/10.87 ! [X0 : map_int_int] : sort1(map(int,int),t2tb1(X0))),
% 73.81/10.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort1)).
% 73.81/10.87 tff(f55,axiom,(
% 73.81/10.87 ! [X0 : map_int_int] : tb2t1(t2tb1(X0)) = X0),
% 73.81/10.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeL1)).
% 73.81/10.87 tff(f57,axiom,(
% 73.81/10.87 ! [X0 : map_int_int,X1 : $int,X2 : $int] : ($less(X1,X2) => sum2(X0,X1,X2) = $sum(tb2t(get(int,int,t2tb1(X0),t2tb(X1))),sum2(X0,$sum(X1,1),X2)))),
% 73.81/10.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_def_non_empty)).
% 73.81/10.87 tff(f63,axiom,(
% 73.81/10.87 ! [X0 : uni] : t2tb2(tb2t2(X0)) = X0),
% 73.81/10.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR2)).
% 73.81/10.87 tff(f64,axiom,(
% 73.81/10.87 ! [X0 : array_int,X1 : $int,X2 : $int] : sum3(X0,X1,X2) = sum2(tb2t1(elts(int,t2tb2(X0))),X1,X2)),
% 73.81/10.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_def)).
% 73.81/10.87 tff(f72,axiom,(
% 73.81/10.87 ! [X0 : $int,X1 : $int,X2 : array_int,X3 : array_int] : (phase11(X0,X1,X2,X3) => (? [X4 : $int,X5 : array_int,X6 : array_int] : (tb2t(get2(int,t2tb2(X6),X4)) = tb2t(get2(int,t2tb2(X5),X4)) & X0 = X4 & X1 = $sum(X4,1) & X2 = X5 & X3 = X6) | ? [X4 : $int,X7 : $int,X5 : array_int,X6 : array_int] : ($less($sum(X4,1),X7) & phase11(go_left1(X4,X7),X4,X5,X6) & phase11(go_right1(X4,X7),X7,X5,X6) & tb2t(get2(int,t2tb2(X6),X4)) = sum3(X5,$sum($difference(X4,$difference(X7,X4)),1),$sum(X4,1)) & X0 = X4 & X1 = X7 & X2 = X5 & X3 = X6)))),
% 73.81/10.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',phase1_inversion)).
% 73.81/10.87 tff(f76,conjecture,(
% 73.81/10.87 ! [X0 : $int,X1 : $int,X2 : $int,X3 : map_int_int,X4 : $int,X5 : map_int_int] : (($lesseq(0,X2) & $lesseq(0,X4) & $lesseq(0,X0) & $less(X0,X1) & $less(X1,X4) & $lesseq($uminus(1),$difference(X0,$difference(X1,X0))) & is_power_of_21($difference(X1,X0)) & tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($difference(X0,$difference(X1,X0)),1)) & phase11(X0,X1,tb2t2(mk_array1(int,X2,t2tb1(X3))),tb2t2(mk_array1(int,X4,t2tb1(X5))))) => (($lesseq(0,X1) & $less(X1,X4)) => (tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($difference(X0,$difference(X1,X0)),1)) => tb2t(get(int,int,t2tb1(X5),t2tb(X0))) = sum2(X3,$sum($difference(X0,$difference(X1,X0)),1),$sum(X0,1)))))),
% 73.81/10.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_downsweep)).
% 73.81/10.87 tff(f77,negated_conjecture,(
% 73.81/10.87 ~ ! [X0 : $int,X1 : $int,X2 : $int,X3 : map_int_int,X4 : $int,X5 : map_int_int] : (($lesseq(0,X2) & $lesseq(0,X4) & $lesseq(0,X0) & $less(X0,X1) & $less(X1,X4) & $lesseq($uminus(1),$difference(X0,$difference(X1,X0))) & is_power_of_21($difference(X1,X0)) & tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($difference(X0,$difference(X1,X0)),1)) & phase11(X0,X1,tb2t2(mk_array1(int,X2,t2tb1(X3))),tb2t2(mk_array1(int,X4,t2tb1(X5))))) => (($lesseq(0,X1) & $less(X1,X4)) => (tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($difference(X0,$difference(X1,X0)),1)) => tb2t(get(int,int,t2tb1(X5),t2tb(X0))) = sum2(X3,$sum($difference(X0,$difference(X1,X0)),1),$sum(X0,1)))))),
% 73.81/10.87 inference(negated_conjecture,[status(cth)],[f76])).
% 73.81/10.87 tff(f97,plain,(
% 73.81/10.87 ! [X0 : map_int_int,X1 : $int,X2 : $int] : (~$less(X1,X2) => sum2(X0,X1,X2) = 0)),
% 73.81/10.87 inference(theory_normalization,[],[f53])).
% 73.81/10.87 tff(f106,plain,(
% 73.81/10.87 ! [X0 : $int,X1 : $int,X2 : array_int,X3 : array_int] : (phase11(X0,X1,X2,X3) => (? [X4 : $int,X5 : array_int,X6 : array_int] : (tb2t(get2(int,t2tb2(X6),X4)) = tb2t(get2(int,t2tb2(X5),X4)) & X0 = X4 & X1 = $sum(X4,1) & X2 = X5 & X3 = X6) | ? [X4 : $int,X7 : $int,X5 : array_int,X6 : array_int] : ($less($sum(X4,1),X7) & phase11(go_left1(X4,X7),X4,X5,X6) & phase11(go_right1(X4,X7),X7,X5,X6) & tb2t(get2(int,t2tb2(X6),X4)) = sum3(X5,$sum($sum(X4,$uminus($sum(X7,$uminus(X4)))),1),$sum(X4,1)) & X0 = X4 & X1 = X7 & X2 = X5 & X3 = X6)))),
% 73.81/10.87 inference(theory_normalization,[],[f72])).
% 73.81/10.87 tff(f110,plain,(
% 73.81/10.87 ~ ! [X0 : $int,X1 : $int,X2 : $int,X3 : map_int_int,X4 : $int,X5 : map_int_int] : ((~$less(X2,0) & ~$less(X4,0) & ~$less(X0,0) & $less(X0,X1) & $less(X1,X4) & ~$less($sum(X0,$uminus($sum(X1,$uminus(X0)))),$uminus(1)) & is_power_of_21($sum(X1,$uminus(X0))) & tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($sum(X0,$uminus($sum(X1,$uminus(X0)))),1)) & phase11(X0,X1,tb2t2(mk_array1(int,X2,t2tb1(X3))),tb2t2(mk_array1(int,X4,t2tb1(X5))))) => ((~$less(X1,0) & $less(X1,X4)) => (tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($sum(X0,$uminus($sum(X1,$uminus(X0)))),1)) => tb2t(get(int,int,t2tb1(X5),t2tb(X0))) = sum2(X3,$sum($sum(X0,$uminus($sum(X1,$uminus(X0)))),1),$sum(X0,1)))))),
% 73.81/10.87 inference(theory_normalization,[],[f77])).
% 73.81/10.87 tff(f111,definition,(
% 73.81/10.87 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 73.81/10.87 introduced(theory,[tha_commutativity])).
% 73.81/10.87 tff(f112,definition,(
% 73.81/10.87 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 73.81/10.87 introduced(theory,[tha_associativity])).
% 73.81/10.87 tff(f114,definition,(
% 73.81/10.87 ( ! [X0 : $int,X1 : $int] : ($uminus($sum(X0,X1)) = $sum($uminus(X1),$uminus(X0))) )),
% 73.81/10.87 introduced(theory,[tha_inverse_op_op_inverses])).
% 73.81/10.87 tff(f115,definition,(
% 73.81/10.87 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 73.81/10.87 introduced(theory,[tha_inverse_op_unit])).
% 73.81/10.87 tff(f116,definition,(
% 73.81/10.87 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 73.81/10.87 introduced(theory,[tha_non-reflexivity])).
% 73.81/10.87 tff(f120,definition,(
% 73.81/10.87 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 73.81/10.87 introduced(theory,[tha_order_plus_one_dichotomy])).
% 73.81/10.87 tff(f121,definition,(
% 73.81/10.87 ( ! [X0 : $int] : ($uminus($uminus(X0)) = X0) )),
% 73.81/10.87 introduced(theory,[tha_minus_minus_x])).
% 73.81/10.87 tff(f129,plain,(
% 73.81/10.87 ! [X0 : $int,X1 : $int,X2 : array_int,X3 : array_int] : (phase11(X0,X1,X2,X3) => (? [X4 : $int,X5 : array_int,X6 : array_int] : (tb2t(get2(int,t2tb2(X6),X4)) = tb2t(get2(int,t2tb2(X5),X4)) & X0 = X4 & X1 = $sum(X4,1) & X2 = X5 & X3 = X6) | ? [X7 : $int,X8 : $int,X9 : array_int,X10 : array_int] : ($less($sum(X7,1),X8) & phase11(go_left1(X7,X8),X7,X9,X10) & phase11(go_right1(X7,X8),X8,X9,X10) & tb2t(get2(int,t2tb2(X10),X7)) = sum3(X9,$sum($sum(X7,$uminus($sum(X8,$uminus(X7)))),1),$sum(X7,1)) & X0 = X7 & X1 = X8 & X2 = X9 & X3 = X10)))),
% 73.81/10.87 inference(rectify,[],[f106])).
% 73.81/10.87 tff(f168,plain,(
% 73.81/10.87 ! [X0 : ty,X1 : $int,X2 : uni] : (elts(X0,mk_array1(X0,X1,X2)) = X2 | ~sort1(map(int,X0),X2))),
% 73.81/10.87 inference(ennf_transformation,[],[f42])).
% 73.81/10.87 tff(f169,plain,(
% 73.81/10.87 ! [X0 : map_int_int,X1 : $int,X2 : $int] : (sum2(X0,X1,X2) = 0 | $less(X1,X2))),
% 73.81/10.87 inference(ennf_transformation,[],[f97])).
% 73.81/10.87 tff(f170,plain,(
% 73.81/10.87 ! [X0 : map_int_int,X1 : $int,X2 : $int] : (sum2(X0,X1,X2) = $sum(tb2t(get(int,int,t2tb1(X0),t2tb(X1))),sum2(X0,$sum(X1,1),X2)) | ~$less(X1,X2))),
% 73.81/10.87 inference(ennf_transformation,[],[f57])).
% 73.81/10.87 tff(f183,plain,(
% 73.81/10.87 ! [X0 : $int,X1 : $int,X2 : array_int,X3 : array_int] : ((? [X4 : $int,X5 : array_int,X6 : array_int] : (tb2t(get2(int,t2tb2(X6),X4)) = tb2t(get2(int,t2tb2(X5),X4)) & X0 = X4 & X1 = $sum(X4,1) & X2 = X5 & X3 = X6) | ? [X7 : $int,X8 : $int,X9 : array_int,X10 : array_int] : ($less($sum(X7,1),X8) & phase11(go_left1(X7,X8),X7,X9,X10) & phase11(go_right1(X7,X8),X8,X9,X10) & tb2t(get2(int,t2tb2(X10),X7)) = sum3(X9,$sum($sum(X7,$uminus($sum(X8,$uminus(X7)))),1),$sum(X7,1)) & X0 = X7 & X1 = X8 & X2 = X9 & X3 = X10)) | ~phase11(X0,X1,X2,X3))),
% 73.81/10.87 inference(ennf_transformation,[],[f129])).
% 73.81/10.87 tff(f184,plain,(
% 73.81/10.87 ! [X0 : $int,X1 : $int,X2 : array_int,X3 : array_int] : (? [X4 : $int,X5 : array_int,X6 : array_int] : (tb2t(get2(int,t2tb2(X6),X4)) = tb2t(get2(int,t2tb2(X5),X4)) & X0 = X4 & X1 = $sum(X4,1) & X2 = X5 & X3 = X6) | ? [X7 : $int,X8 : $int,X9 : array_int,X10 : array_int] : ($less($sum(X7,1),X8) & phase11(go_left1(X7,X8),X7,X9,X10) & phase11(go_right1(X7,X8),X8,X9,X10) & tb2t(get2(int,t2tb2(X10),X7)) = sum3(X9,$sum($sum(X7,$uminus($sum(X8,$uminus(X7)))),1),$sum(X7,1)) & X0 = X7 & X1 = X8 & X2 = X9 & X3 = X10) | ~phase11(X0,X1,X2,X3))),
% 73.81/10.87 inference(flattening,[],[f183])).
% 73.81/10.87 tff(f189,plain,(
% 73.81/10.87 ? [X0 : $int,X1 : $int,X2 : $int,X3 : map_int_int,X4 : $int,X5 : map_int_int] : (((tb2t(get(int,int,t2tb1(X5),t2tb(X0))) != sum2(X3,$sum($sum(X0,$uminus($sum(X1,$uminus(X0)))),1),$sum(X0,1)) & tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($sum(X0,$uminus($sum(X1,$uminus(X0)))),1))) & (~$less(X1,0) & $less(X1,X4))) & (~$less(X2,0) & ~$less(X4,0) & ~$less(X0,0) & $less(X0,X1) & $less(X1,X4) & ~$less($sum(X0,$uminus($sum(X1,$uminus(X0)))),$uminus(1)) & is_power_of_21($sum(X1,$uminus(X0))) & tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($sum(X0,$uminus($sum(X1,$uminus(X0)))),1)) & phase11(X0,X1,tb2t2(mk_array1(int,X2,t2tb1(X3))),tb2t2(mk_array1(int,X4,t2tb1(X5))))))),
% 73.81/10.87 inference(ennf_transformation,[],[f110])).
% 73.81/10.87 tff(f190,plain,(
% 73.81/10.87 ? [X0 : $int,X1 : $int,X2 : $int,X3 : map_int_int,X4 : $int,X5 : map_int_int] : (tb2t(get(int,int,t2tb1(X5),t2tb(X0))) != sum2(X3,$sum($sum(X0,$uminus($sum(X1,$uminus(X0)))),1),$sum(X0,1)) & tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($sum(X0,$uminus($sum(X1,$uminus(X0)))),1)) & ~$less(X1,0) & $less(X1,X4) & ~$less(X2,0) & ~$less(X4,0) & ~$less(X0,0) & $less(X0,X1) & $less(X1,X4) & ~$less($sum(X0,$uminus($sum(X1,$uminus(X0)))),$uminus(1)) & is_power_of_21($sum(X1,$uminus(X0))) & tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($sum(X0,$uminus($sum(X1,$uminus(X0)))),1)) & phase11(X0,X1,tb2t2(mk_array1(int,X2,t2tb1(X3))),tb2t2(mk_array1(int,X4,t2tb1(X5)))))),
% 73.81/10.87 inference(flattening,[],[f189])).
% 73.81/10.87 tff(f191,definition,(
% 73.81/10.87 ! [X0 : $int,X1 : $int,X2 : array_int,X3 : array_int] : (? [X7 : $int,X8 : $int,X9 : array_int,X10 : array_int] : ($less($sum(X7,1),X8) & phase11(go_left1(X7,X8),X7,X9,X10) & phase11(go_right1(X7,X8),X8,X9,X10) & tb2t(get2(int,t2tb2(X10),X7)) = sum3(X9,$sum($sum(X7,$uminus($sum(X8,$uminus(X7)))),1),$sum(X7,1)) & X0 = X7 & X1 = X8 & X2 = X9 & X3 = X10) | ~ sP0(X0,X1,X2,X3))),
% 73.81/10.87 introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction])).
% 73.81/10.87 tff(f192,plain,(
% 73.81/10.87 ! [X0 : $int,X1 : $int,X2 : array_int,X3 : array_int] : (? [X4 : $int,X5 : array_int,X6 : array_int] : (tb2t(get2(int,t2tb2(X6),X4)) = tb2t(get2(int,t2tb2(X5),X4)) & X0 = X4 & X1 = $sum(X4,1) & X2 = X5 & X3 = X6) | sP0(X0,X1,X2,X3) | ~phase11(X0,X1,X2,X3))),
% 73.81/10.87 inference(definition_folding,[],[f184,f191])).
% 73.81/10.87 tff(f199,plain,(
% 73.81/10.87 ! [X0 : $int,X1 : $int,X2 : array_int,X3 : array_int] : (? [X7 : $int,X8 : $int,X9 : array_int,X10 : array_int] : ($less($sum(X7,1),X8) & phase11(go_left1(X7,X8),X7,X9,X10) & phase11(go_right1(X7,X8),X8,X9,X10) & tb2t(get2(int,t2tb2(X10),X7)) = sum3(X9,$sum($sum(X7,$uminus($sum(X8,$uminus(X7)))),1),$sum(X7,1)) & X0 = X7 & X1 = X8 & X2 = X9 & X3 = X10) | ~sP0(X0,X1,X2,X3))),
% 73.81/10.87 inference(nnf_transformation,[],[f191])).
% 73.81/10.87 tff(f200,plain,(
% 73.81/10.87 ! [X0 : $int,X1 : $int,X2 : array_int,X3 : array_int] : (? [X4 : $int,X5 : $int,X6 : array_int,X7 : array_int] : ($less($sum(X4,1),X5) & phase11(go_left1(X4,X5),X4,X6,X7) & phase11(go_right1(X4,X5),X5,X6,X7) & tb2t(get2(int,t2tb2(X7),X4)) = sum3(X6,$sum($sum(X4,$uminus($sum(X5,$uminus(X4)))),1),$sum(X4,1)) & X0 = X4 & X1 = X5 & X2 = X6 & X3 = X7) | ~sP0(X0,X1,X2,X3))),
% 73.81/10.87 inference(rectify,[],[f199])).
% 73.81/10.87 tff(f201,plain,(
% 73.81/10.87 ! [X0 : $int,X1 : $int,X2 : array_int,X3 : array_int] : (($less($sum(sK3(X0,X1,X2,X3),1),sK4(X0,X1,X2,X3)) & phase11(go_left1(sK3(X0,X1,X2,X3),sK4(X0,X1,X2,X3)),sK3(X0,X1,X2,X3),sK5(X0,X1,X2,X3),sK6(X0,X1,X2,X3)) & phase11(go_right1(sK3(X0,X1,X2,X3),sK4(X0,X1,X2,X3)),sK4(X0,X1,X2,X3),sK5(X0,X1,X2,X3),sK6(X0,X1,X2,X3)) & tb2t(get2(int,t2tb2(sK6(X0,X1,X2,X3)),sK3(X0,X1,X2,X3))) = sum3(sK5(X0,X1,X2,X3),$sum($sum(sK3(X0,X1,X2,X3),$uminus($sum(sK4(X0,X1,X2,X3),$uminus(sK3(X0,X1,X2,X3))))),1),$sum(sK3(X0,X1,X2,X3),1)) & sK3(X0,X1,X2,X3) = X0 & sK4(X0,X1,X2,X3) = X1 & sK5(X0,X1,X2,X3) = X2 & sK6(X0,X1,X2,X3) = X3) | ~sP0(X0,X1,X2,X3))),
% 73.81/10.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6]),skolemize(X4,sK3(X0,X1,X2,X3)),skolemize(X5,sK4(X0,X1,X2,X3)),skolemize(X6,sK5(X0,X1,X2,X3)),skolemize(X7,sK6(X0,X1,X2,X3))],[f200])).
% 73.81/10.87 tff(f202,plain,(
% 73.81/10.87 ! [X0 : $int,X1 : $int,X2 : array_int,X3 : array_int] : ((tb2t(get2(int,t2tb2(sK9(X0,X1,X2,X3)),sK7(X0,X1,X2,X3))) = tb2t(get2(int,t2tb2(sK8(X0,X1,X2,X3)),sK7(X0,X1,X2,X3))) & sK7(X0,X1,X2,X3) = X0 & $sum(sK7(X0,X1,X2,X3),1) = X1 & sK8(X0,X1,X2,X3) = X2 & sK9(X0,X1,X2,X3) = X3) | sP0(X0,X1,X2,X3) | ~phase11(X0,X1,X2,X3))),
% 73.81/10.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8,sK9]),skolemize(X4,sK7(X0,X1,X2,X3)),skolemize(X5,sK8(X0,X1,X2,X3)),skolemize(X6,sK9(X0,X1,X2,X3))],[f192])).
% 73.81/10.87 tff(f205,plain,(
% 73.81/10.87 tb2t(get(int,int,t2tb1(sK17),t2tb(sK12))) != sum2(sK15,$sum($sum(sK12,$uminus($sum(sK13,$uminus(sK12)))),1),$sum(sK12,1)) & tb2t(get(int,int,t2tb1(sK17),t2tb(sK13))) = sum2(sK15,0,$sum($sum(sK12,$uminus($sum(sK13,$uminus(sK12)))),1)) & ~$less(sK13,0) & $less(sK13,sK16) & ~$less(sK14,0) & ~$less(sK16,0) & ~$less(sK12,0) & $less(sK12,sK13) & $less(sK13,sK16) & ~$less($sum(sK12,$uminus($sum(sK13,$uminus(sK12)))),$uminus(1)) & is_power_of_21($sum(sK13,$uminus(sK12))) & tb2t(get(int,int,t2tb1(sK17),t2tb(sK13))) = sum2(sK15,0,$sum($sum(sK12,$uminus($sum(sK13,$uminus(sK12)))),1)) & phase11(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))),
% 73.81/10.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13,sK14,sK15,sK16,sK17]),skolemize(X0,sK12),skolemize(X1,sK13),skolemize(X2,sK14),skolemize(X3,sK15),skolemize(X4,sK16),skolemize(X5,sK17)],[f190])).
% 73.81/10.87 tff(f252,plain,(
% 73.81/10.87 ( ! [X2 : uni,X0 : ty,X1 : $int] : (~sort1(map(int,X0),X2) | elts(X0,mk_array1(X0,X1,X2)) = X2) )),
% 73.81/10.87 inference(cnf_transformation,[],[f168])).
% 73.81/10.87 tff(f258,plain,(
% 73.81/10.87 ( ! [X2 : $int,X0 : ty,X1 : uni] : (get2(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2))) )),
% 73.81/10.87 inference(cnf_transformation,[],[f48])).
% 73.81/10.87 tff(f263,plain,(
% 73.81/10.87 ( ! [X2 : $int,X0 : map_int_int,X1 : $int] : ($less(X1,X2) | 0 = sum2(X0,X1,X2)) )),
% 73.81/10.87 inference(cnf_transformation,[],[f169])).
% 73.81/10.87 tff(f264,plain,(
% 73.81/10.87 ( ! [X0 : map_int_int] : (sort1(map(int,int),t2tb1(X0))) )),
% 73.81/10.87 inference(cnf_transformation,[],[f54])).
% 73.81/10.87 tff(f265,plain,(
% 73.81/10.87 ( ! [X0 : map_int_int] : (tb2t1(t2tb1(X0)) = X0) )),
% 73.81/10.87 inference(cnf_transformation,[],[f55])).
% 73.81/10.87 tff(f267,plain,(
% 73.81/10.87 ( ! [X2 : $int,X0 : map_int_int,X1 : $int] : (~$less(X1,X2) | sum2(X0,X1,X2) = $sum(tb2t(get(int,int,t2tb1(X0),t2tb(X1))),sum2(X0,$sum(X1,1),X2))) )),
% 73.81/10.87 inference(cnf_transformation,[],[f170])).
% 73.81/10.87 tff(f275,plain,(
% 73.81/10.87 ( ! [X0 : uni] : (t2tb2(tb2t2(X0)) = X0) )),
% 73.81/10.87 inference(cnf_transformation,[],[f63])).
% 73.81/10.87 tff(f276,plain,(
% 73.81/10.87 ( ! [X2 : $int,X0 : array_int,X1 : $int] : (sum3(X0,X1,X2) = sum2(tb2t1(elts(int,t2tb2(X0))),X1,X2)) )),
% 73.81/10.87 inference(cnf_transformation,[],[f64])).
% 73.81/10.87 tff(f287,plain,(
% 73.81/10.87 ( ! [X2 : array_int,X3 : array_int,X0 : $int,X1 : $int] : (~sP0(X0,X1,X2,X3) | sK6(X0,X1,X2,X3) = X3) )),
% 73.81/10.87 inference(cnf_transformation,[],[f201])).
% 73.81/10.87 tff(f288,plain,(
% 73.81/10.87 ( ! [X2 : array_int,X3 : array_int,X0 : $int,X1 : $int] : (~sP0(X0,X1,X2,X3) | sK5(X0,X1,X2,X3) = X2) )),
% 73.81/10.87 inference(cnf_transformation,[],[f201])).
% 73.81/10.87 tff(f289,plain,(
% 73.81/10.87 ( ! [X2 : array_int,X3 : array_int,X0 : $int,X1 : $int] : (~sP0(X0,X1,X2,X3) | sK4(X0,X1,X2,X3) = X1) )),
% 73.81/10.87 inference(cnf_transformation,[],[f201])).
% 73.81/10.87 tff(f290,plain,(
% 73.81/10.87 ( ! [X2 : array_int,X3 : array_int,X0 : $int,X1 : $int] : (~sP0(X0,X1,X2,X3) | sK3(X0,X1,X2,X3) = X0) )),
% 73.81/10.87 inference(cnf_transformation,[],[f201])).
% 73.81/10.87 tff(f291,plain,(
% 73.81/10.87 ( ! [X2 : array_int,X3 : array_int,X0 : $int,X1 : $int] : (tb2t(get2(int,t2tb2(sK6(X0,X1,X2,X3)),sK3(X0,X1,X2,X3))) = sum3(sK5(X0,X1,X2,X3),$sum($sum(sK3(X0,X1,X2,X3),$uminus($sum(sK4(X0,X1,X2,X3),$uminus(sK3(X0,X1,X2,X3))))),1),$sum(sK3(X0,X1,X2,X3),1)) | ~sP0(X0,X1,X2,X3)) )),
% 73.81/10.87 inference(cnf_transformation,[],[f201])).
% 73.81/10.87 tff(f295,plain,(
% 73.81/10.87 ( ! [X2 : array_int,X3 : array_int,X0 : $int,X1 : $int] : (~phase11(X0,X1,X2,X3) | sP0(X0,X1,X2,X3) | sK9(X0,X1,X2,X3) = X3) )),
% 73.81/10.87 inference(cnf_transformation,[],[f202])).
% 73.81/10.87 tff(f296,plain,(
% 73.81/10.87 ( ! [X2 : array_int,X3 : array_int,X0 : $int,X1 : $int] : (~phase11(X0,X1,X2,X3) | sP0(X0,X1,X2,X3) | sK8(X0,X1,X2,X3) = X2) )),
% 73.81/10.87 inference(cnf_transformation,[],[f202])).
% 73.81/10.87 tff(f297,plain,(
% 73.81/10.87 ( ! [X2 : array_int,X3 : array_int,X0 : $int,X1 : $int] : (~phase11(X0,X1,X2,X3) | sP0(X0,X1,X2,X3) | $sum(sK7(X0,X1,X2,X3),1) = X1) )),
% 73.81/10.87 inference(cnf_transformation,[],[f202])).
% 73.81/10.87 tff(f298,plain,(
% 73.81/10.87 ( ! [X2 : array_int,X3 : array_int,X0 : $int,X1 : $int] : (~phase11(X0,X1,X2,X3) | sP0(X0,X1,X2,X3) | sK7(X0,X1,X2,X3) = X0) )),
% 73.81/10.87 inference(cnf_transformation,[],[f202])).
% 73.81/10.87 tff(f299,plain,(
% 73.81/10.87 ( ! [X2 : array_int,X3 : array_int,X0 : $int,X1 : $int] : (tb2t(get2(int,t2tb2(sK9(X0,X1,X2,X3)),sK7(X0,X1,X2,X3))) = tb2t(get2(int,t2tb2(sK8(X0,X1,X2,X3)),sK7(X0,X1,X2,X3))) | sP0(X0,X1,X2,X3) | ~phase11(X0,X1,X2,X3)) )),
% 73.81/10.87 inference(cnf_transformation,[],[f202])).
% 73.81/10.87 tff(f306,plain,(
% 73.81/10.87 phase11(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))),
% 73.81/10.87 inference(cnf_transformation,[],[f205])).
% 73.81/10.87 tff(f318,plain,(
% 73.81/10.87 tb2t(get(int,int,t2tb1(sK17),t2tb(sK12))) != sum2(sK15,$sum($sum(sK12,$uminus($sum(sK13,$uminus(sK12)))),1),$sum(sK12,1))),
% 73.81/10.87 inference(cnf_transformation,[],[f205])).
% 73.81/10.87 tff(f326,plain,(
% 73.81/10.87 ( ! [X2 : array_int,X3 : array_int,X0 : $int,X1 : $int] : (~sP0(X0,X1,X2,X3) | tb2t(get(int,int,elts(int,t2tb2(sK6(X0,X1,X2,X3))),t2tb(sK3(X0,X1,X2,X3)))) = sum2(tb2t1(elts(int,t2tb2(sK5(X0,X1,X2,X3)))),$sum($sum(sK3(X0,X1,X2,X3),$uminus($sum(sK4(X0,X1,X2,X3),$uminus(sK3(X0,X1,X2,X3))))),1),$sum(sK3(X0,X1,X2,X3),1))) )),
% 73.81/10.87 inference(definition_unfolding,[],[f291,f258,f276])).
% 73.81/10.87 tff(f327,plain,(
% 73.81/10.87 ( ! [X2 : array_int,X3 : array_int,X0 : $int,X1 : $int] : (~phase11(X0,X1,X2,X3) | sP0(X0,X1,X2,X3) | tb2t(get(int,int,elts(int,t2tb2(sK9(X0,X1,X2,X3))),t2tb(sK7(X0,X1,X2,X3)))) = tb2t(get(int,int,elts(int,t2tb2(sK8(X0,X1,X2,X3))),t2tb(sK7(X0,X1,X2,X3))))) )),
% 73.81/10.87 inference(definition_unfolding,[],[f299,f258,f258])).
% 73.81/10.87 tff(f358,plain,(
% 73.81/10.87 tb2t(get(int,int,t2tb1(sK17),t2tb(sK12))) != sum2(sK15,$sum($sum(sK12,$uminus($sum(sK13,$uminus(sK12)))),1),$sum(1,sK12))),
% 73.81/10.87 inference(superposition,[],[f318,f111])).
% 73.81/10.87 tff(f359,plain,(
% 73.81/10.87 tb2t(get(int,int,t2tb1(sK17),t2tb(sK12))) != sum2(sK15,$sum(1,$sum(sK12,$uminus($sum(sK13,$uminus(sK12))))),$sum(1,sK12))),
% 73.81/10.87 inference(forward_demodulation,[],[f358,f111])).
% 73.81/10.87 tff(f385,plain,(
% 73.81/10.87 ( ! [X0 : $int] : ($less(X0,$sum(X0,1))) )),
% 73.81/10.87 inference(resolution,[],[f120,f116])).
% 73.81/10.87 tff(f480,plain,(
% 73.81/10.87 ( ! [X0 : map_int_int,X1 : $int] : (0 = sum2(X0,X1,X1)) )),
% 73.81/10.87 inference(resolution,[],[f263,f116])).
% 73.81/10.87 tff(f500,plain,(
% 73.81/10.87 ( ! [X0 : $int,X1 : $int] : ($uminus($sum(X1,$uminus(X0))) = $sum(X0,$uminus(X1))) )),
% 73.81/10.87 inference(superposition,[],[f114,f121])).
% 73.81/10.87 tff(f573,plain,(
% 73.81/10.87 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 73.81/10.87 inference(superposition,[],[f112,f115])).
% 73.81/10.87 tff(f592,plain,(
% 73.81/10.87 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 73.81/10.87 inference(evaluation,[],[f573])).
% 73.81/10.87 tff(f780,plain,(
% 73.81/10.87 ( ! [X0 : $int,X1 : map_int_int] : (t2tb1(X1) = elts(int,mk_array1(int,X0,t2tb1(X1)))) )),
% 73.81/10.87 inference(resolution,[],[f252,f264])).
% 73.81/10.87 tff(f1022,plain,(
% 73.81/10.87 sP0(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))) | tb2t2(mk_array1(int,sK16,t2tb1(sK17))) = sK9(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))),
% 73.81/10.87 inference(resolution,[],[f295,f306])).
% 73.81/10.87 tff(f1054,definition,(
% 73.81/10.87 spl18_18 <=> tb2t2(mk_array1(int,sK16,t2tb1(sK17))) = sK9(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))),
% 73.81/10.87 introduced(definition,[new_symbols(definition,[spl18_18])],[avatar_definition])).
% 73.81/10.87 tff(f1056,plain,(
% 73.81/10.87 tb2t2(mk_array1(int,sK16,t2tb1(sK17))) = sK9(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))) | ~spl18_18),
% 73.81/10.87 inference(avatar_component_clause,[],[f1054])).
% 73.81/10.87 tff(f1058,definition,(
% 73.81/10.87 spl18_19 <=> sP0(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))),
% 73.81/10.87 introduced(definition,[new_symbols(definition,[spl18_19])],[avatar_definition])).
% 73.81/10.87 tff(f1059,plain,(
% 73.81/10.87 ~sP0(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))) | spl18_19),
% 73.81/10.87 inference(avatar_component_clause,[],[f1058])).
% 73.81/10.87 tff(f1060,plain,(
% 73.81/10.87 sP0(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))) | ~spl18_19),
% 73.81/10.87 inference(avatar_component_clause,[],[f1058])).
% 73.81/10.87 tff(f1061,plain,(
% 73.81/10.87 spl18_18 | spl18_19),
% 73.81/10.87 inference(avatar_split_clause,[],[f1022,f1058,f1054])).
% 73.81/10.87 tff(f1062,plain,(
% 73.81/10.87 sP0(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))) | tb2t2(mk_array1(int,sK14,t2tb1(sK15))) = sK8(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))),
% 73.81/10.87 inference(resolution,[],[f296,f306])).
% 73.81/10.87 tff(f1064,definition,(
% 73.81/10.87 spl18_20 <=> tb2t2(mk_array1(int,sK14,t2tb1(sK15))) = sK8(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))),
% 73.81/10.87 introduced(definition,[new_symbols(definition,[spl18_20])],[avatar_definition])).
% 73.81/10.87 tff(f1066,plain,(
% 73.81/10.87 tb2t2(mk_array1(int,sK14,t2tb1(sK15))) = sK8(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))) | ~spl18_20),
% 73.81/10.87 inference(avatar_component_clause,[],[f1064])).
% 73.81/10.87 tff(f1067,plain,(
% 73.81/10.87 spl18_20 | spl18_19),
% 73.81/10.87 inference(avatar_split_clause,[],[f1062,f1058,f1064])).
% 73.81/10.87 tff(f1068,plain,(
% 73.81/10.87 sP0(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))) | sK12 = sK7(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))),
% 73.81/10.87 inference(resolution,[],[f298,f306])).
% 73.81/10.87 tff(f1116,plain,(
% 73.81/10.87 sP0(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))) | sK13 = $sum(sK7(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))),1)),
% 73.81/10.87 inference(resolution,[],[f297,f306])).
% 73.81/10.87 tff(f1427,plain,(
% 73.81/10.87 sP0(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))) | tb2t(get(int,int,elts(int,t2tb2(sK9(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK7(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))))) = tb2t(get(int,int,elts(int,t2tb2(sK8(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK7(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))))),
% 73.81/10.87 inference(resolution,[],[f327,f306])).
% 73.81/10.87 tff(f2114,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK6(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK3(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))))) = sum2(tb2t1(elts(int,t2tb2(sK5(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))))),$sum($sum(sK3(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))),$uminus($sum(sK4(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))),$uminus(sK3(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))))),1),$sum(sK3(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))),1)) | ~spl18_19),
% 73.81/10.87 inference(resolution,[],[f1060,f326])).
% 73.81/10.87 tff(f2116,plain,(
% 73.81/10.87 sK12 = sK3(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))) | ~spl18_19),
% 73.81/10.87 inference(resolution,[],[f1060,f290])).
% 73.81/10.87 tff(f2117,plain,(
% 73.81/10.87 sK13 = sK4(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))) | ~spl18_19),
% 73.81/10.87 inference(resolution,[],[f1060,f289])).
% 73.81/10.87 tff(f2118,plain,(
% 73.81/10.87 tb2t2(mk_array1(int,sK14,t2tb1(sK15))) = sK5(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))) | ~spl18_19),
% 73.81/10.87 inference(resolution,[],[f1060,f288])).
% 73.81/10.87 tff(f2119,plain,(
% 73.81/10.87 tb2t2(mk_array1(int,sK16,t2tb1(sK17))) = sK6(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))) | ~spl18_19),
% 73.81/10.87 inference(resolution,[],[f1060,f287])).
% 73.81/10.87 tff(f2121,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK6(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK3(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))))) = sum2(tb2t1(elts(int,t2tb2(sK5(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))))),$sum($sum(sK3(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))),$uminus($sum(sK4(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))),$uminus(sK3(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))))),1),$sum(1,sK3(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))) | ~spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f2114,f111])).
% 73.81/10.87 tff(f2123,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK6(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) = sum2(tb2t1(elts(int,t2tb2(sK5(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))))),$sum($sum(sK12,$uminus($sum(sK4(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))),$uminus(sK12)))),1),$sum(1,sK12)) | ~spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f2121,f2116])).
% 73.81/10.87 tff(f2125,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK6(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) = sum2(tb2t1(elts(int,t2tb2(sK5(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))))),$sum(1,$sum(sK12,$uminus($sum(sK4(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))),$uminus(sK12))))),$sum(1,sK12)) | ~spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f2123,f111])).
% 73.81/10.87 tff(f2126,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK6(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) = sum2(tb2t1(elts(int,t2tb2(sK5(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))))),$sum(1,$sum(sK12,$sum(sK12,$uminus(sK4(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))))),$sum(1,sK12)) | ~spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f2125,f500])).
% 73.81/10.87 tff(f2127,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK6(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) = sum2(tb2t1(elts(int,t2tb2(sK5(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))))),$sum(1,$sum(sK12,$sum(sK12,$uminus(sK13)))),$sum(1,sK12)) | ~spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f2126,f2117])).
% 73.81/10.87 tff(f2128,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK6(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) = sum2(tb2t1(elts(int,t2tb2(tb2t2(mk_array1(int,sK14,t2tb1(sK15)))))),$sum(1,$sum(sK12,$sum(sK12,$uminus(sK13)))),$sum(1,sK12)) | ~spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f2127,f2118])).
% 73.81/10.87 tff(f2129,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK6(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) = sum2(tb2t1(elts(int,mk_array1(int,sK14,t2tb1(sK15)))),$sum(1,$sum(sK12,$sum(sK12,$uminus(sK13)))),$sum(1,sK12)) | ~spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f2128,f275])).
% 73.81/10.87 tff(f2130,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK6(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) = sum2(tb2t1(t2tb1(sK15)),$sum(1,$sum(sK12,$sum(sK12,$uminus(sK13)))),$sum(1,sK12)) | ~spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f2129,f780])).
% 73.81/10.87 tff(f2131,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK6(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) = sum2(sK15,$sum(1,$sum(sK12,$sum(sK12,$uminus(sK13)))),$sum(1,sK12)) | ~spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f2130,f265])).
% 73.81/10.87 tff(f2132,plain,(
% 73.81/10.87 sum2(sK15,$sum(1,$sum(sK12,$sum(sK12,$uminus(sK13)))),$sum(1,sK12)) = tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK16,t2tb1(sK17))))),t2tb(sK12))) | ~spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f2131,f2119])).
% 73.81/10.87 tff(f2133,plain,(
% 73.81/10.87 sum2(sK15,$sum(1,$sum(sK12,$sum(sK12,$uminus(sK13)))),$sum(1,sK12)) = tb2t(get(int,int,elts(int,mk_array1(int,sK16,t2tb1(sK17))),t2tb(sK12))) | ~spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f2132,f275])).
% 73.81/10.87 tff(f2134,plain,(
% 73.81/10.87 tb2t(get(int,int,t2tb1(sK17),t2tb(sK12))) = sum2(sK15,$sum(1,$sum(sK12,$sum(sK12,$uminus(sK13)))),$sum(1,sK12)) | ~spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f2133,f780])).
% 73.81/10.87 tff(f3037,plain,(
% 73.81/10.87 ( ! [X0 : map_int_int,X1 : $int] : (sum2(X0,X1,$sum(X1,1)) = $sum(tb2t(get(int,int,t2tb1(X0),t2tb(X1))),sum2(X0,$sum(X1,1),$sum(X1,1)))) )),
% 73.81/10.87 inference(resolution,[],[f385,f267])).
% 73.81/10.87 tff(f3048,plain,(
% 73.81/10.87 ( ! [X0 : map_int_int,X1 : $int] : (sum2(X0,X1,$sum(X1,1)) = $sum(tb2t(get(int,int,t2tb1(X0),t2tb(X1))),0)) )),
% 73.81/10.87 inference(forward_demodulation,[],[f3037,f480])).
% 73.81/10.87 tff(f3049,plain,(
% 73.81/10.87 ( ! [X0 : map_int_int,X1 : $int] : (tb2t(get(int,int,t2tb1(X0),t2tb(X1))) = sum2(X0,X1,$sum(X1,1))) )),
% 73.81/10.87 inference(evaluation,[],[f3048])).
% 73.81/10.87 tff(f3212,plain,(
% 73.81/10.87 ( ! [X0 : $int,X1 : $int] : ($sum(X1,$sum(X0,$uminus(X1))) = X0) )),
% 73.81/10.87 inference(superposition,[],[f592,f111])).
% 73.81/10.87 tff(f3677,plain,(
% 73.81/10.87 tb2t(get(int,int,t2tb1(sK17),t2tb(sK12))) != sum2(sK15,$sum($sum(sK12,$sum(sK12,$uminus(sK13))),1),$sum(sK12,1))),
% 73.81/10.87 inference(superposition,[],[f318,f500])).
% 73.81/10.87 tff(f3699,plain,(
% 73.81/10.87 tb2t(get(int,int,t2tb1(sK17),t2tb(sK12))) != sum2(sK15,$sum($sum(sK12,$sum(sK12,$uminus(sK13))),1),$sum(1,sK12))),
% 73.81/10.87 inference(forward_demodulation,[],[f3677,f111])).
% 73.81/10.87 tff(f3709,plain,(
% 73.81/10.87 tb2t(get(int,int,t2tb1(sK17),t2tb(sK12))) != sum2(sK15,$sum(1,$sum(sK12,$sum(sK12,$uminus(sK13)))),$sum(1,sK12))),
% 73.81/10.87 inference(forward_demodulation,[],[f3699,f111])).
% 73.81/10.87 tff(f3716,plain,(
% 73.81/10.87 $false | ~spl18_19),
% 73.81/10.87 inference(forward_subsumption_resolution,[],[f3709,f2134])).
% 73.81/10.87 tff(f3717,plain,(
% 73.81/10.87 ~spl18_19),
% 73.81/10.87 inference(avatar_contradiction_clause,[],[f3716])).
% 73.81/10.87 tff(f3726,plain,(
% 73.81/10.87 sK12 = sK7(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))) | spl18_19),
% 73.81/10.87 inference(forward_subsumption_resolution,[],[f1068,f1059])).
% 73.81/10.87 tff(f3727,plain,(
% 73.81/10.87 sK13 = $sum(sK7(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))),1) | spl18_19),
% 73.81/10.87 inference(forward_subsumption_resolution,[],[f1116,f1059])).
% 73.81/10.87 tff(f3728,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK9(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK7(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))))) = tb2t(get(int,int,elts(int,t2tb2(sK8(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK7(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))))) | spl18_19),
% 73.81/10.87 inference(forward_subsumption_resolution,[],[f1427,f1059])).
% 73.81/10.87 tff(f3731,plain,(
% 73.81/10.87 sK13 = $sum(1,sK7(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17))))) | spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f3727,f111])).
% 73.81/10.87 tff(f3732,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK9(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) = tb2t(get(int,int,elts(int,t2tb2(sK8(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) | spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f3728,f3726])).
% 73.81/10.87 tff(f3735,plain,(
% 73.81/10.87 sK13 = $sum(1,sK12) | spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f3731,f3726])).
% 73.81/10.87 tff(f3736,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK9(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) = tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK14,t2tb1(sK15))))),t2tb(sK12))) | (spl18_19 | ~spl18_20)),
% 73.81/10.87 inference(forward_demodulation,[],[f3732,f1066])).
% 73.81/10.87 tff(f3737,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK9(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) = tb2t(get(int,int,elts(int,mk_array1(int,sK14,t2tb1(sK15))),t2tb(sK12))) | (spl18_19 | ~spl18_20)),
% 73.81/10.87 inference(forward_demodulation,[],[f3736,f275])).
% 73.81/10.87 tff(f3738,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK9(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) = tb2t(get(int,int,t2tb1(sK15),t2tb(sK12))) | (spl18_19 | ~spl18_20)),
% 73.81/10.87 inference(forward_demodulation,[],[f3737,f780])).
% 73.81/10.87 tff(f3739,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK9(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) = sum2(sK15,sK12,$sum(sK12,1)) | (spl18_19 | ~spl18_20)),
% 73.81/10.87 inference(forward_demodulation,[],[f3738,f3049])).
% 73.81/10.87 tff(f3740,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK9(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) = sum2(sK15,sK12,$sum(1,sK12)) | (spl18_19 | ~spl18_20)),
% 73.81/10.87 inference(forward_demodulation,[],[f3739,f111])).
% 73.81/10.87 tff(f3741,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(sK9(sK12,sK13,tb2t2(mk_array1(int,sK14,t2tb1(sK15))),tb2t2(mk_array1(int,sK16,t2tb1(sK17)))))),t2tb(sK12))) = sum2(sK15,sK12,sK13) | (spl18_19 | ~spl18_20)),
% 73.81/10.87 inference(forward_demodulation,[],[f3740,f3735])).
% 73.81/10.87 tff(f3742,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK16,t2tb1(sK17))))),t2tb(sK12))) = sum2(sK15,sK12,sK13) | (~spl18_18 | spl18_19 | ~spl18_20)),
% 73.81/10.87 inference(forward_demodulation,[],[f3741,f1056])).
% 73.81/10.87 tff(f3743,plain,(
% 73.81/10.87 tb2t(get(int,int,elts(int,mk_array1(int,sK16,t2tb1(sK17))),t2tb(sK12))) = sum2(sK15,sK12,sK13) | (~spl18_18 | spl18_19 | ~spl18_20)),
% 73.81/10.87 inference(forward_demodulation,[],[f3742,f275])).
% 73.81/10.87 tff(f3744,plain,(
% 73.81/10.87 tb2t(get(int,int,t2tb1(sK17),t2tb(sK12))) = sum2(sK15,sK12,sK13) | (~spl18_18 | spl18_19 | ~spl18_20)),
% 73.81/10.87 inference(forward_demodulation,[],[f3743,f780])).
% 73.81/10.87 tff(f3745,plain,(
% 73.81/10.87 sum2(sK17,sK12,$sum(sK12,1)) = sum2(sK15,sK12,sK13) | (~spl18_18 | spl18_19 | ~spl18_20)),
% 73.81/10.87 inference(forward_demodulation,[],[f3744,f3049])).
% 73.81/10.87 tff(f3746,plain,(
% 73.81/10.87 sum2(sK17,sK12,$sum(1,sK12)) = sum2(sK15,sK12,sK13) | (~spl18_18 | spl18_19 | ~spl18_20)),
% 73.81/10.87 inference(forward_demodulation,[],[f3745,f111])).
% 73.81/10.87 tff(f3747,plain,(
% 73.81/10.87 sum2(sK15,sK12,sK13) = sum2(sK17,sK12,sK13) | (~spl18_18 | spl18_19 | ~spl18_20)),
% 73.81/10.87 inference(forward_demodulation,[],[f3746,f3735])).
% 73.81/10.87 tff(f3748,plain,(
% 73.81/10.87 tb2t(get(int,int,t2tb1(sK17),t2tb(sK12))) != sum2(sK15,$sum(1,$sum(sK12,$uminus($sum(sK13,$uminus(sK12))))),sK13) | spl18_19),
% 73.81/10.87 inference(superposition,[],[f359,f3735])).
% 73.81/10.87 tff(f3753,plain,(
% 73.81/10.87 ( ! [X0 : $int] : ($sum(sK13,X0) = $sum(1,$sum(sK12,X0))) ) | spl18_19),
% 73.81/10.87 inference(superposition,[],[f112,f3735])).
% 73.81/10.87 tff(f3757,plain,(
% 73.81/10.87 tb2t(get(int,int,t2tb1(sK17),t2tb(sK12))) != sum2(sK15,$sum(sK13,$uminus($sum(sK13,$uminus(sK12)))),sK13) | spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f3748,f3753])).
% 73.81/10.87 tff(f3759,plain,(
% 73.81/10.87 tb2t(get(int,int,t2tb1(sK17),t2tb(sK12))) != sum2(sK15,$sum(sK13,$sum(sK12,$uminus(sK13))),sK13) | spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f3757,f500])).
% 73.81/10.87 tff(f3761,plain,(
% 73.81/10.87 tb2t(get(int,int,t2tb1(sK17),t2tb(sK12))) != sum2(sK15,sK12,sK13) | spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f3759,f3212])).
% 73.81/10.87 tff(f3763,plain,(
% 73.81/10.87 sum2(sK17,sK12,$sum(sK12,1)) != sum2(sK15,sK12,sK13) | spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f3761,f3049])).
% 73.81/10.87 tff(f3765,plain,(
% 73.81/10.87 sum2(sK17,sK12,$sum(1,sK12)) != sum2(sK15,sK12,sK13) | spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f3763,f111])).
% 73.81/10.87 tff(f3766,plain,(
% 73.81/10.87 sum2(sK15,sK12,sK13) != sum2(sK17,sK12,sK13) | spl18_19),
% 73.81/10.87 inference(forward_demodulation,[],[f3765,f3735])).
% 73.81/10.87 tff(f3767,plain,(
% 73.81/10.87 $false | (~spl18_18 | spl18_19 | ~spl18_20)),
% 73.81/10.87 inference(forward_subsumption_resolution,[],[f3766,f3747])).
% 73.81/10.87 tff(f3768,plain,(
% 73.81/10.87 ~spl18_18 | spl18_19 | ~spl18_20),
% 73.81/10.87 inference(avatar_contradiction_clause,[],[f3767])).
% 73.81/10.87 cnf(s441, plain, spl18_18 | spl18_19, inference(sat_conversion,[],[f1061])).
% 73.81/10.87 cnf(s448, plain, spl18_19 | spl18_20, inference(sat_conversion,[],[f1067])).
% 73.81/10.87 cnf(s1387, plain, ~spl18_19, inference(sat_conversion,[],[f3717])).
% 73.81/10.87 cnf(s1402, plain, ~spl18_18 | spl18_19 | ~spl18_20, inference(sat_conversion,[],[f3768])).
% 73.81/10.87 cnf(s1403, plain, spl18_20, inference(rat,[],[s448,s1387])).
% 73.81/10.87 cnf(s1404, plain, ~spl18_18, inference(rat,[],[s1402,s1387,s1403])).
% 73.81/10.87 cnf(s1405, plain, $false, inference(rat,[],[s441,s1387,s1404])).
% 73.81/10.87 tff(f3769,plain,(
% 73.81/10.87 $false),
% 73.81/10.87 inference(avatar_sat_refutation,[],[s1405])).
% 73.81/10.87 % SZS output end Proof for theBenchmark
% 73.81/10.87 % (1957385)------------------------------
% 73.81/10.87 % (1957385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 73.81/10.87 % (1957385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.81/10.87 % (1957385)CaDiCaL version: 2.1.3
% 73.81/10.87 % (1957385)Termination reason: Refutation
% 73.81/10.87 % (1957385)Time elapsed: 0.127 s
% 73.81/10.87 % (1957385)Peak memory usage: 15 MB
% 73.81/10.87 % (1957385)Instructions burned: 225 (million)
% 73.81/10.87 % (1957278)Success in time 10.538 s
% 73.81/10.87 % Vampire exiting
%------------------------------------------------------------------------------