%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW639_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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:34 PM UTC 2026
% Result : Theorem 4.12s 0.94s
% Output : Refutation 4.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW639_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n008.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 14:24:24 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.18/0.76 % (2286285)Will run a generic schedule for satisfiability detection.
% 3.18/0.76 % (2286291)% WARNING: option uhcvi not known.
% 3.18/0.76 % (2286296)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3140136086:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.18/0.76 % (2286291)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1165363918:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.18/0.76 % (2286290)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4134707447_2999 on theBenchmark for (2999ds/0Mi)
% 3.18/0.76 % (2286292)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=272168509:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.18/0.76 % (2286294)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=41645793:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.18/0.76 % (2286293)dis+10_1_sil=32000:sp=arity:random_seed=505409100:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.18/0.76 % (2286295)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=951971630:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.18/0.76 % (2286290)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.18/0.76 % (2286290)Terminated due to inappropriate strategy.
% 3.18/0.76 % (2286290)------------------------------
% 3.18/0.76 % (2286290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.18/0.76 % (2286290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.18/0.76 % (2286290)CaDiCaL version: 2.1.3
% 3.18/0.76 % (2286290)Termination reason: Inappropriate
% 3.18/0.76 % (2286290)Time elapsed: 0.006 s
% 3.18/0.76 % (2286290)Peak memory usage: 11 MB
% 3.18/0.76 % (2286290)Instructions burned: 11 (million)
% 3.18/0.76 % (2286290)------------------------------
% 3.18/0.76 % (2286290)------------------------------
% 3.18/0.76 % (2286304)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1405607506:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.18/0.76 % (2286304)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.18/0.76 % (2286304)Terminated due to inappropriate strategy.
% 3.18/0.76 % (2286304)------------------------------
% 3.18/0.76 % (2286304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.18/0.76 % (2286304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.18/0.76 % (2286304)CaDiCaL version: 2.1.3
% 3.18/0.76 % (2286304)Termination reason: Inappropriate
% 3.18/0.76 % (2286304)Time elapsed: 0.006 s
% 3.18/0.76 % (2286304)Peak memory usage: 11 MB
% 3.18/0.76 % (2286304)Instructions burned: 9 (million)
% 3.18/0.76 % (2286304)------------------------------
% 3.18/0.76 % (2286304)------------------------------
% 3.18/0.76 % (2286296)Instruction limit reached!
% 3.18/0.76 % (2286296)------------------------------
% 3.18/0.76 % (2286296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.18/0.76 % (2286296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.18/0.76 % (2286296)CaDiCaL version: 2.1.3
% 3.18/0.76 % (2286296)Termination reason: Instruction limit
% 3.18/0.76 % (2286296)Termination phase: Saturation
% 3.18/0.76 % (2286296)Time elapsed: 0.052 s
% 3.18/0.76 % (2286296)Peak memory usage: 13 MB
% 3.18/0.76 % (2286296)Instructions burned: 161 (million)
% 3.18/0.76 % (2286307)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=3668459500:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.18/0.76 % (2286306)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4287675072:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.18/0.76 % (2286293)Instruction limit reached!
% 3.18/0.76 % (2286293)------------------------------
% 3.18/0.76 % (2286293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.18/0.76 % (2286293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.18/0.76 % (2286293)CaDiCaL version: 2.1.3
% 3.18/0.76 % (2286293)Termination reason: Instruction limit
% 3.18/0.76 % (2286293)Termination phase: Saturation
% 3.18/0.76 % (2286293)Time elapsed: 0.066 s
% 3.18/0.76 % (2286293)Peak memory usage: 12 MB
% 3.18/0.76 % (2286293)Instructions burned: 104 (million)
% 3.18/0.76 % (2286294)Instruction limit reached!
% 3.18/0.76 % (2286294)------------------------------
% 3.18/0.76 % (2286294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.93 % (2286294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.93 % (2286294)CaDiCaL version: 2.1.3
% 4.12/0.93 % (2286294)Termination reason: Instruction limit
% 4.12/0.93 % (2286294)Termination phase: Saturation
% 4.12/0.93 % (2286294)Time elapsed: 0.071 s
% 4.12/0.93 % (2286294)Peak memory usage: 13 MB
% 4.12/0.93 % (2286294)Instructions burned: 117 (million)
% 4.12/0.93 % (2286311)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2636181933:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 4.12/0.93 % (2286310)ott-21_1_sil=16000:fs=off:random_seed=2986388777:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.12/0.93 % (2286295)Instruction limit reached!
% 4.12/0.93 % (2286295)------------------------------
% 4.12/0.93 % (2286295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.93 % (2286295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.93 % (2286295)CaDiCaL version: 2.1.3
% 4.12/0.93 % (2286295)Termination reason: Instruction limit
% 4.12/0.93 % (2286295)Termination phase: Saturation
% 4.12/0.93 % (2286295)Time elapsed: 0.119 s
% 4.12/0.93 % (2286295)Peak memory usage: 13 MB
% 4.12/0.93 % (2286295)Instructions burned: 137 (million)
% 4.12/0.93 % (2286314)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2863756133:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 4.12/0.93 % (2286314)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.12/0.93 % (2286314)Terminated due to inappropriate strategy.
% 4.12/0.93 % (2286314)------------------------------
% 4.12/0.93 % (2286314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.93 % (2286314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.93 % (2286314)CaDiCaL version: 2.1.3
% 4.12/0.93 % (2286314)Termination reason: Inappropriate
% 4.12/0.93 % (2286314)Time elapsed: 0.005 s
% 4.12/0.93 % (2286314)Peak memory usage: 10 MB
% 4.12/0.93 % (2286314)Instructions burned: 10 (million)
% 4.12/0.93 % (2286314)------------------------------
% 4.12/0.93 % (2286314)------------------------------
% 4.12/0.93 % (2286306)Instruction limit reached!
% 4.12/0.93 % (2286306)------------------------------
% 4.12/0.94 % (2286306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.94 % (2286306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.94 % (2286306)CaDiCaL version: 2.1.3
% 4.12/0.94 % (2286306)Termination reason: Instruction limit
% 4.12/0.94 % (2286306)Termination phase: Saturation
% 4.12/0.94 % (2286306)Time elapsed: 0.094 s
% 4.12/0.94 % (2286306)Peak memory usage: 13 MB
% 4.12/0.94 % (2286306)Instructions burned: 133 (million)
% 4.12/0.94 % (2286317)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2915282007:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 4.12/0.94 % (2286316)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=251784009:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 4.12/0.94 % (2286317)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.12/0.94 % (2286317)Terminated due to inappropriate strategy.
% 4.12/0.94 % (2286317)------------------------------
% 4.12/0.94 % (2286317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.94 % (2286317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.94 % (2286317)CaDiCaL version: 2.1.3
% 4.12/0.94 % (2286317)Termination reason: Inappropriate
% 4.12/0.94 % (2286317)Time elapsed: 0.003 s
% 4.12/0.94 % (2286317)Peak memory usage: 11 MB
% 4.12/0.94 % (2286317)Instructions burned: 10 (million)
% 4.12/0.94 % (2286317)------------------------------
% 4.12/0.94 % (2286317)------------------------------
% 4.12/0.94 % (2286320)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=921429663: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)
% 4.12/0.94 % (2286310)Instruction limit reached!
% 4.12/0.94 % (2286310)------------------------------
% 4.12/0.94 % (2286310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.94 % (2286310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.94 % (2286310)CaDiCaL version: 2.1.3
% 4.12/0.94 % (2286310)Termination reason: Instruction limit
% 4.12/0.94 % (2286310)Termination phase: Saturation
% 4.12/0.94 % (2286310)Time elapsed: 0.096 s
% 4.12/0.94 % (2286310)Peak memory usage: 13 MB
% 4.12/0.94 % (2286310)Instructions burned: 180 (million)
% 4.12/0.94 % (2286322)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1608257697:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 4.12/0.94 % (2286307)Instruction limit reached!
% 4.12/0.94 % (2286307)------------------------------
% 4.12/0.94 % (2286307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.94 % (2286307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.94 % (2286307)CaDiCaL version: 2.1.3
% 4.12/0.94 % (2286307)Termination reason: Instruction limit
% 4.12/0.94 % (2286307)Termination phase: Saturation
% 4.12/0.94 % (2286307)Time elapsed: 0.300 s
% 4.12/0.94 % (2286307)Peak memory usage: 18 MB
% 4.12/0.94 % (2286307)Instructions burned: 687 (million)
% 4.12/0.94 % (2286387)fmb+10_1_sil=64000:random_seed=590541266:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 4.12/0.94 % (2286387)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.12/0.94 % (2286387)Terminated due to inappropriate strategy.
% 4.12/0.94 % (2286387)------------------------------
% 4.12/0.94 % (2286387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.94 % (2286387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.94 % (2286387)CaDiCaL version: 2.1.3
% 4.12/0.94 % (2286387)Termination reason: Inappropriate
% 4.12/0.94 % (2286387)Time elapsed: 0.005 s
% 4.12/0.94 % (2286387)Peak memory usage: 11 MB
% 4.12/0.94 % (2286387)Instructions burned: 10 (million)
% 4.12/0.94 % (2286387)------------------------------
% 4.12/0.94 % (2286387)------------------------------
% 4.12/0.94 % (2286395)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4230283142:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 4.12/0.94 % (2286311)Instruction limit reached!
% 4.12/0.94 % (2286311)------------------------------
% 4.12/0.94 % (2286311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.94 % (2286311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.94 % (2286311)CaDiCaL version: 2.1.3
% 4.12/0.94 % (2286311)Termination reason: Instruction limit
% 4.12/0.94 % (2286311)Termination phase: Saturation
% 4.12/0.94 % (2286311)Time elapsed: 0.319 s
% 4.12/0.94 % (2286311)Peak memory usage: 14 MB
% 4.12/0.94 % (2286311)Instructions burned: 478 (million)
% 4.12/0.94 % (2286395)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.12/0.94 % (2286395)Terminated due to inappropriate strategy.
% 4.12/0.94 % (2286395)------------------------------
% 4.12/0.94 % (2286395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.94 % (2286395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.94 % (2286395)CaDiCaL version: 2.1.3
% 4.12/0.94 % (2286395)Termination reason: Inappropriate
% 4.12/0.94 % (2286395)Time elapsed: 0.005 s
% 4.12/0.94 % (2286395)Peak memory usage: 11 MB
% 4.12/0.94 % (2286395)Instructions burned: 9 (million)
% 4.12/0.94 % (2286395)------------------------------
% 4.12/0.94 % (2286395)------------------------------
% 4.12/0.94 % (2286404)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1499374275:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 4.12/0.94 % (2286405)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2648510713:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 4.12/0.94 % (2286404)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.12/0.94 % (2286404)Terminated due to inappropriate strategy.
% 4.12/0.94 % (2286404)------------------------------
% 4.12/0.94 % (2286404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.94 % (2286404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.94 % (2286404)CaDiCaL version: 2.1.3
% 4.12/0.94 % (2286404)Termination reason: Inappropriate
% 4.12/0.94 % (2286404)Time elapsed: 0.005 s
% 4.12/0.94 % (2286404)Peak memory usage: 11 MB
% 4.12/0.94 % (2286404)Instructions burned: 10 (million)
% 4.12/0.94 % (2286404)------------------------------
% 4.12/0.94 % (2286404)------------------------------
% 4.12/0.94 % (2286415)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3118387060:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 4.12/0.94 % (2286322)Instruction limit reached!
% 4.12/0.94 % (2286322)------------------------------
% 4.12/0.94 % (2286322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.94 % (2286322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.94 % (2286322)CaDiCaL version: 2.1.3
% 4.12/0.94 % (2286322)Termination reason: Instruction limit
% 4.12/0.94 % (2286322)Termination phase: Saturation
% 4.12/0.94 % (2286322)Time elapsed: 0.279 s
% 4.12/0.94 % (2286322)Peak memory usage: 19 MB
% 4.12/0.94 % (2286322)Instructions burned: 882 (million)
% 4.12/0.94 % (2286433)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1527717228:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 4.12/0.94 % (2286433)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.12/0.94 % (2286433)Terminated due to inappropriate strategy.
% 4.12/0.94 % (2286433)------------------------------
% 4.12/0.94 % (2286433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.94 % (2286433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.94 % (2286433)CaDiCaL version: 2.1.3
% 4.12/0.94 % (2286433)Termination reason: Inappropriate
% 4.12/0.94 % (2286433)Time elapsed: 0.003 s
% 4.12/0.94 % (2286433)Peak memory usage: 11 MB
% 4.12/0.94 % (2286433)Instructions burned: 11 (million)
% 4.12/0.94 % (2286433)------------------------------
% 4.12/0.94 % (2286433)------------------------------
% 4.12/0.94 % (2286435)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1070076318:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 4.12/0.94 % (2286435)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.12/0.94 % (2286435)Terminated due to inappropriate strategy.
% 4.12/0.94 % (2286435)------------------------------
% 4.12/0.94 % (2286435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.94 % (2286435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.94 % (2286435)CaDiCaL version: 2.1.3
% 4.12/0.94 % (2286435)Termination reason: Inappropriate
% 4.12/0.94 % (2286435)Time elapsed: 0.002 s
% 4.12/0.94 % (2286435)Peak memory usage: 11 MB
% 4.12/0.94 % (2286435)Instructions burned: 10 (million)
% 4.12/0.94 % (2286435)------------------------------
% 4.12/0.94 % (2286435)------------------------------
% 4.12/0.94 % (2286441)ott-2_1_sil=16000:newcnf=on:random_seed=98604852:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 4.12/0.94 % (2286320)Instruction limit reached!
% 4.12/0.94 % (2286320)------------------------------
% 4.12/0.94 % (2286320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.94 % (2286320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.94 % (2286320)CaDiCaL version: 2.1.3
% 4.12/0.94 % (2286320)Termination reason: Instruction limit
% 4.12/0.94 % (2286320)Termination phase: Saturation
% 4.12/0.94 % (2286320)Time elapsed: 0.445 s
% 4.12/0.94 % (2286320)Peak memory usage: 19 MB
% 4.12/0.94 % (2286320)Instructions burned: 693 (million)
% 4.12/0.94 % (2286291) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2286285-2286291"...
% 4.12/0.94 % (2286291)...printing done.
% 4.12/0.94 % (2286291)Refutation found. Thanks to Tanya!
% 4.12/0.94 % SZS status Theorem for theBenchmark
% 4.12/0.94 % SZS output start Proof for theBenchmark
% 4.12/0.94 tff(type_def_5, type, uni: $tType).
% 4.12/0.94 tff(type_def_6, type, ty: $tType).
% 4.12/0.94 tff(type_def_7, type, bool1: $tType).
% 4.12/0.94 tff(type_def_8, type, tuple02: $tType).
% 4.12/0.94 tff(type_def_9, type, map_int_int: $tType).
% 4.12/0.94 tff(type_def_10, type, array_int: $tType).
% 4.12/0.94 tff(type_def_11, type, rarray_int: $tType).
% 4.12/0.94 tff(func_def_0, type, witness1: ty > uni).
% 4.12/0.94 tff(func_def_1, type, int: ty).
% 4.12/0.94 tff(func_def_2, type, real: ty).
% 4.12/0.94 tff(func_def_3, type, bool: ty).
% 4.12/0.94 tff(func_def_4, type, true1: bool1).
% 4.12/0.94 tff(func_def_5, type, false1: bool1).
% 4.12/0.94 tff(func_def_6, type, match_bool1: (ty * bool1 * uni * uni) > uni).
% 4.12/0.94 tff(func_def_7, type, tuple0: ty).
% 4.12/0.94 tff(func_def_8, type, tuple03: tuple02).
% 4.12/0.94 tff(func_def_9, type, qtmark: ty).
% 4.12/0.94 tff(func_def_12, type, min1: ($int * $int) > $int).
% 4.12/0.94 tff(func_def_13, type, max1: ($int * $int) > $int).
% 4.12/0.94 tff(func_def_14, type, map: (ty * ty) > ty).
% 4.12/0.94 tff(func_def_15, type, get: (ty * ty * uni * uni) > uni).
% 4.12/0.94 tff(func_def_16, type, set: (ty * ty * uni * uni * uni) > uni).
% 4.12/0.94 tff(func_def_17, type, const: (ty * ty * uni) > uni).
% 4.12/0.94 tff(func_def_18, type, array: ty > ty).
% 4.12/0.94 tff(func_def_19, type, mk_array1: (ty * $int * uni) > uni).
% 4.12/0.94 tff(func_def_20, type, length2: (ty * uni) > $int).
% 4.12/0.94 tff(func_def_21, type, elts: (ty * uni) > uni).
% 4.12/0.94 tff(func_def_22, type, get2: (ty * uni * $int) > uni).
% 4.12/0.94 tff(func_def_23, type, t2tb: $int > uni).
% 4.12/0.94 tff(func_def_24, type, tb2t: uni > $int).
% 4.12/0.94 tff(func_def_25, type, set2: (ty * uni * $int * uni) > uni).
% 4.12/0.94 tff(func_def_26, type, make2: (ty * $int * uni) > uni).
% 4.12/0.94 tff(func_def_27, type, rarray: ty > ty).
% 4.12/0.94 tff(func_def_28, type, mk_rarray1: (ty * uni * $int * uni) > uni).
% 4.12/0.94 tff(func_def_29, type, dummy: (ty * uni) > uni).
% 4.12/0.94 tff(func_def_30, type, length3: (ty * uni) > $int).
% 4.12/0.94 tff(func_def_31, type, data: (ty * uni) > uni).
% 4.12/0.94 tff(func_def_32, type, mixfix_lbrb1: (ty * uni * $int) > uni).
% 4.12/0.94 tff(func_def_33, type, mixfix_lblsmnrb1: (ty * uni * $int * uni) > uni).
% 4.12/0.94 tff(func_def_34, type, make3: (ty * $int * uni) > uni).
% 4.12/0.94 tff(func_def_35, type, t2tb1: map_int_int > uni).
% 4.12/0.94 tff(func_def_36, type, tb2t1: uni > map_int_int).
% 4.12/0.94 tff(func_def_37, type, t2tb2: array_int > uni).
% 4.12/0.94 tff(func_def_38, type, tb2t2: uni > array_int).
% 4.12/0.94 tff(func_def_39, type, t2tb3: rarray_int > uni).
% 4.12/0.94 tff(func_def_40, type, tb2t3: uni > rarray_int).
% 4.12/0.94 tff(func_def_49, type, sK0: $int).
% 4.12/0.94 tff(func_def_50, type, sK1: $int).
% 4.12/0.94 tff(func_def_51, type, sK2: array_int).
% 4.12/0.94 tff(func_def_52, type, sK3: map_int_int).
% 4.12/0.94 tff(func_def_53, type, sK4: $int).
% 4.12/0.94 tff(func_def_54, type, sK5: $int).
% 4.12/0.94 tff(func_def_55, type, sK6: array_int).
% 4.12/0.94 tff(func_def_56, type, sK7: $int).
% 4.12/0.94 tff(func_def_57, type, sK8: $int).
% 4.12/0.94 tff(func_def_58, type, sK9: array_int).
% 4.12/0.94 tff(func_def_59, type, sK10: $int).
% 4.12/0.94 tff(func_def_60, type, sK11: map_int_int).
% 4.12/0.94 tff(func_def_61, type, sK12: $int).
% 4.12/0.94 tff(func_def_62, type, sK13: $int).
% 4.12/0.94 tff(func_def_63, type, sK14: array_int).
% 4.12/0.94 tff(func_def_64, type, sK15: map_int_int).
% 4.12/0.94 tff(func_def_65, type, sK16: $int).
% 4.12/0.94 tff(func_def_66, type, sK17: $int).
% 4.12/0.94 tff(func_def_67, type, sK18: array_int).
% 4.12/0.94 tff(func_def_68, type, sK19: $int).
% 4.12/0.94 tff(func_def_69, type, sK20: $int).
% 4.12/0.94 tff(func_def_70, type, sK21: array_int).
% 4.12/0.94 tff(func_def_71, type, sK22: $int).
% 4.12/0.94 tff(func_def_72, type, sK23: map_int_int).
% 4.12/0.94 tff(func_def_73, type, sK24: $int).
% 4.12/0.94 tff(func_def_74, type, sK25: $int).
% 4.12/0.94 tff(func_def_75, type, sK26: map_int_int).
% 4.12/0.94 tff(func_def_76, type, sK27: $int).
% 4.12/0.94 tff(func_def_77, type, sK28: $int).
% 4.12/0.94 tff(func_def_78, type, sK29: array_int).
% 4.12/0.94 tff(pred_def_1, type, sort1: (ty * uni) > $o).
% 4.12/0.94 tff(f9,axiom,(
% 4.12/0.94 ! [X0 : $int,X1 : $int] : ($lesseq(X0,max1(X0,X1)) & $lesseq(X1,max1(X0,X1)))),
% 4.12/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',max_is_ge)).
% 4.12/0.94 tff(f11,axiom,(
% 4.12/0.94 ! [X0 : $int,X1 : $int] : ($lesseq(min1(X0,X1),X0) & $lesseq(min1(X0,X1),X1))),
% 4.12/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',min_is_le)).
% 4.12/0.94 tff(f13,axiom,(
% 4.12/0.94 ! [X0 : $int,X1 : $int] : ($lesseq(X1,X0) => max1(X0,X1) = X0)),
% 4.12/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',max_x)).
% 4.12/0.94 tff(f16,axiom,(
% 4.12/0.94 ! [X0 : $int,X1 : $int] : ($lesseq(X1,X0) => min1(X0,X1) = X1)),
% 4.12/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',min_y)).
% 4.12/0.94 tff(f17,axiom,(
% 4.12/0.94 ! [X0 : $int,X1 : $int] : ($lesseq(X1,X0) => max1(X0,X1) = max1(X1,X0))),
% 4.12/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',max_sym)).
% 4.12/0.94 tff(f21,axiom,(
% 4.12/0.94 ! [X0 : ty,X1 : ty,X2 : uni,X3 : uni,X4 : uni,X5 : uni] : (sort1(X1,X5) => (X3 = X4 => get(X1,X0,set(X1,X0,X2,X3,X5),X4) = X5))),
% 4.12/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',select_eq)).
% 4.12/0.94 tff(f31,axiom,(
% 4.12/0.94 ! [X0 : $int] : sort1(int,t2tb(X0))),
% 4.12/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort)).
% 4.12/0.94 tff(f32,axiom,(
% 4.12/0.94 ! [X0 : $int] : tb2t(t2tb(X0)) = X0),
% 4.12/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL)).
% 4.12/0.94 tff(f38,axiom,(
% 4.12/0.94 ! [X0 : ty,X1 : $int,X2 : uni] : make2(X0,X1,X2) = mk_array1(X0,X1,const(X0,int,X2))),
% 4.12/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',make_def)).
% 4.12/0.94 tff(f42,axiom,(
% 4.12/0.94 ! [X0 : ty,X1 : uni,X2 : $int,X3 : uni] : length3(X0,mk_rarray1(X0,X1,X2,X3)) = X2),
% 4.12/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',length_def3)).
% 4.12/0.94 tff(f44,axiom,(
% 4.12/0.94 ! [X0 : ty,X1 : uni,X2 : $int,X3 : uni] : data(X0,mk_rarray1(X0,X1,X2,X3)) = X3),
% 4.12/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',data_def1)).
% 4.12/0.94 tff(f51,axiom,(
% 4.12/0.94 ! [X0 : ty,X1 : $int,X2 : uni] : make3(X0,X1,X2) = mk_rarray1(X0,X2,X1,make2(X0,X1,X2))),
% 4.12/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',make_def1)).
% 4.12/0.94 tff(f54,axiom,(
% 4.12/0.94 ! [X0 : uni] : t2tb1(tb2t1(X0)) = X0),
% 4.12/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR1)).
% 4.12/0.94 tff(f60,axiom,(
% 4.12/0.94 ! [X0 : uni] : t2tb3(tb2t3(X0)) = X0),
% 4.12/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR3)).
% 4.12/0.94 tff(f61,conjecture,(
% 4.12/0.94 $lesseq(0,10) & (($lesseq(0,length3(int,make3(int,10,t2tb(0)))) & $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0))))) & ! [X0 : $int] : (($lesseq(length3(int,make3(int,10,t2tb(0))),X0) & $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & $lesseq(0,length2(int,t2tb2(X3))))) => ($lesseq(0,0) & $less(0,length3(int,make3(int,10,t2tb(0)))) & ! [X4 : map_int_int] : (($lesseq(0,length3(int,make3(int,10,t2tb(0)))) & $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0))))) & ! [X0 : $int] : (($lesseq(length3(int,make3(int,10,t2tb(0))),X0) & $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(get(int,int,t2tb1(X4),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & $lesseq(0,length2(int,t2tb2(X3)))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & tb2t(dummy(int,make3(int,10,t2tb(0)))) = X1 & length3(int,make3(int,10,t2tb(0))) = X2 & ? [X5 : $int,X6 : map_int_int] : (X3 = tb2t2(mk_array1(int,X5,t2tb1(X6))) & length2(int,data(int,make3(int,10,t2tb(0)))) = X5 & tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = X4))) => ($lesseq(0,10) & (($lesseq(0,length3(int,make3(int,10,t2tb(0)))) & $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0))))) & ! [X0 : $int] : (($lesseq(length3(int,make3(int,10,t2tb(0))),X0) & $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & $lesseq(0,length2(int,t2tb2(X3))))) => ($lesseq(0,0) & $less(0,length3(int,make3(int,10,t2tb(0)))) & ! [X7 : map_int_int] : (($lesseq(0,length3(int,make3(int,10,t2tb(0)))) & $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0))))) & ! [X0 : $int] : (($lesseq(length3(int,make3(int,10,t2tb(0))),X0) & $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(get(int,int,t2tb1(X7),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & $lesseq(0,length2(int,t2tb2(X3)))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & tb2t(dummy(int,make3(int,10,t2tb(0)))) = X1 & length3(int,make3(int,10,t2tb(0))) = X2 & ? [X5 : $int,X6 : map_int_int] : (X3 = tb2t2(mk_array1(int,X5,t2tb1(X6))) & length2(int,data(int,make3(int,10,t2tb(0)))) = X5 & tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = X7))) => ! [X8 : $int,X9 : map_int_int,X10 : $int] : (($lesseq(0,X10) & $lesseq(X10,X8) & ! [X0 : $int] : (($lesseq(X10,X0) & $less(X0,X8)) => tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & $lesseq(0,X8)) & X10 = $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) & ! [X0 : $int] : (($lesseq(0,X0) & $less(X0,X10)) => (($less(X0,length3(int,make3(int,10,t2tb(0)))) => tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(get(int,int,t2tb1(X4),t2tb(X0)))) & ($lesseq(length3(int,make3(int,10,t2tb(0))),X0) => tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(get(int,int,t2tb1(X7),t2tb($difference(X0,length3(int,make3(int,10,t2tb(0))))))))))) => (X10 = 20 & tb2t(get(int,int,t2tb1(X9),t2tb(0))) = 17 & $lesseq(0,10) & $less(10,X10) & tb2t(get(int,int,t2tb1(X9),t2tb(10))) = 42 & $lesseq(0,0) & $less(0,length3(int,make3(int,10,t2tb(0)))) & tb2t(get(int,int,t2tb1(X7),t2tb(0))) = 42)))))))))),
% 4.12/0.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_test2)).
% 4.12/0.94 tff(f62,negated_conjecture,(
% 4.12/0.94 ~($lesseq(0,10) & (($lesseq(0,length3(int,make3(int,10,t2tb(0)))) & $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0))))) & ! [X0 : $int] : (($lesseq(length3(int,make3(int,10,t2tb(0))),X0) & $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & $lesseq(0,length2(int,t2tb2(X3))))) => ($lesseq(0,0) & $less(0,length3(int,make3(int,10,t2tb(0)))) & ! [X4 : map_int_int] : (($lesseq(0,length3(int,make3(int,10,t2tb(0)))) & $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0))))) & ! [X0 : $int] : (($lesseq(length3(int,make3(int,10,t2tb(0))),X0) & $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(get(int,int,t2tb1(X4),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & $lesseq(0,length2(int,t2tb2(X3)))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & tb2t(dummy(int,make3(int,10,t2tb(0)))) = X1 & length3(int,make3(int,10,t2tb(0))) = X2 & ? [X5 : $int,X6 : map_int_int] : (X3 = tb2t2(mk_array1(int,X5,t2tb1(X6))) & length2(int,data(int,make3(int,10,t2tb(0)))) = X5 & tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = X4))) => ($lesseq(0,10) & (($lesseq(0,length3(int,make3(int,10,t2tb(0)))) & $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0))))) & ! [X0 : $int] : (($lesseq(length3(int,make3(int,10,t2tb(0))),X0) & $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & $lesseq(0,length2(int,t2tb2(X3))))) => ($lesseq(0,0) & $less(0,length3(int,make3(int,10,t2tb(0)))) & ! [X7 : map_int_int] : (($lesseq(0,length3(int,make3(int,10,t2tb(0)))) & $lesseq(length3(int,make3(int,10,t2tb(0))),length2(int,data(int,make3(int,10,t2tb(0))))) & ! [X0 : $int] : (($lesseq(length3(int,make3(int,10,t2tb(0))),X0) & $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(get(int,int,t2tb1(X7),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & $lesseq(0,length2(int,t2tb2(X3)))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & tb2t(dummy(int,make3(int,10,t2tb(0)))) = X1 & length3(int,make3(int,10,t2tb(0))) = X2 & ? [X5 : $int,X6 : map_int_int] : (X3 = tb2t2(mk_array1(int,X5,t2tb1(X6))) & length2(int,data(int,make3(int,10,t2tb(0)))) = X5 & tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = X7))) => ! [X8 : $int,X9 : map_int_int,X10 : $int] : (($lesseq(0,X10) & $lesseq(X10,X8) & ! [X0 : $int] : (($lesseq(X10,X0) & $less(X0,X8)) => tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & $lesseq(0,X8)) & X10 = $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) & ! [X0 : $int] : (($lesseq(0,X0) & $less(X0,X10)) => (($less(X0,length3(int,make3(int,10,t2tb(0)))) => tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(get(int,int,t2tb1(X4),t2tb(X0)))) & ($lesseq(length3(int,make3(int,10,t2tb(0))),X0) => tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(get(int,int,t2tb1(X7),t2tb($difference(X0,length3(int,make3(int,10,t2tb(0))))))))))) => (X10 = 20 & tb2t(get(int,int,t2tb1(X9),t2tb(0))) = 17 & $lesseq(0,10) & $less(10,X10) & tb2t(get(int,int,t2tb1(X9),t2tb(10))) = 42 & $lesseq(0,0) & $less(0,length3(int,make3(int,10,t2tb(0)))) & tb2t(get(int,int,t2tb1(X7),t2tb(0))) = 42))))))))))),
% 4.12/0.94 inference(negated_conjecture,[status(cth)],[f61])).
% 4.12/0.94 tff(f64,plain,(
% 4.12/0.94 ! [X0 : $int,X1 : $int] : (~$less(max1(X0,X1),X0) & ~$less(max1(X0,X1),X1))),
% 4.12/0.94 inference(theory_normalization,[],[f9])).
% 4.12/0.94 tff(f65,plain,(
% 4.12/0.94 ! [X0 : $int,X1 : $int] : (~$less(X0,min1(X0,X1)) & ~$less(X1,min1(X0,X1)))),
% 4.12/0.94 inference(theory_normalization,[],[f11])).
% 4.12/0.94 tff(f66,plain,(
% 4.12/0.94 ! [X0 : $int,X1 : $int] : (~$less(X0,X1) => max1(X0,X1) = X0)),
% 4.12/0.94 inference(theory_normalization,[],[f13])).
% 4.12/0.94 tff(f69,plain,(
% 4.12/0.94 ! [X0 : $int,X1 : $int] : (~$less(X0,X1) => min1(X0,X1) = X1)),
% 4.12/0.94 inference(theory_normalization,[],[f16])).
% 4.12/0.94 tff(f70,plain,(
% 4.12/0.94 ! [X0 : $int,X1 : $int] : (~$less(X0,X1) => max1(X0,X1) = max1(X1,X0))),
% 4.12/0.94 inference(theory_normalization,[],[f17])).
% 4.12/0.94 tff(f72,plain,(
% 4.12/0.94 ~(~$less(10,0) & ((~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X0 : $int] : ((~$less(X0,length3(int,make3(int,10,t2tb(0)))) & $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & ~$less(length2(int,t2tb2(X3)),0))) => (~$less(0,0) & $less(0,length3(int,make3(int,10,t2tb(0)))) & ! [X4 : map_int_int] : ((~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X0 : $int] : ((~$less(X0,length3(int,make3(int,10,t2tb(0)))) & $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(get(int,int,t2tb1(X4),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & ~$less(length2(int,t2tb2(X3)),0)) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & tb2t(dummy(int,make3(int,10,t2tb(0)))) = X1 & length3(int,make3(int,10,t2tb(0))) = X2 & ? [X5 : $int,X6 : map_int_int] : (X3 = tb2t2(mk_array1(int,X5,t2tb1(X6))) & length2(int,data(int,make3(int,10,t2tb(0)))) = X5 & tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = X4))) => (~$less(10,0) & ((~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X0 : $int] : ((~$less(X0,length3(int,make3(int,10,t2tb(0)))) & $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & ~$less(length2(int,t2tb2(X3)),0))) => (~$less(0,0) & $less(0,length3(int,make3(int,10,t2tb(0)))) & ! [X7 : map_int_int] : ((~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X0 : $int] : ((~$less(X0,length3(int,make3(int,10,t2tb(0)))) & $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(get(int,int,t2tb1(X7),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & ~$less(length2(int,t2tb2(X3)),0)) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & tb2t(dummy(int,make3(int,10,t2tb(0)))) = X1 & length3(int,make3(int,10,t2tb(0))) = X2 & ? [X5 : $int,X6 : map_int_int] : (X3 = tb2t2(mk_array1(int,X5,t2tb1(X6))) & length2(int,data(int,make3(int,10,t2tb(0)))) = X5 & tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = X7))) => ! [X8 : $int,X9 : map_int_int,X10 : $int] : ((~$less(X10,0) & ~$less(X8,X10) & ! [X0 : $int] : ((~$less(X0,X10) & $less(X0,X8)) => tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & ~$less(X8,0)) & X10 = $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) & ! [X0 : $int] : ((~$less(X0,0) & $less(X0,X10)) => (($less(X0,length3(int,make3(int,10,t2tb(0)))) => tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(get(int,int,t2tb1(X4),t2tb(X0)))) & (~$less(X0,length3(int,make3(int,10,t2tb(0)))) => tb2t(get(int,int,t2tb1(X9),t2tb(X0))) = tb2t(get(int,int,t2tb1(X7),t2tb($sum(X0,$uminus(length3(int,make3(int,10,t2tb(0)))))))))))) => (X10 = 20 & tb2t(get(int,int,t2tb1(X9),t2tb(0))) = 17 & ~$less(10,0) & $less(10,X10) & tb2t(get(int,int,t2tb1(X9),t2tb(10))) = 42 & ~$less(0,0) & $less(0,length3(int,make3(int,10,t2tb(0)))) & tb2t(get(int,int,t2tb1(X7),t2tb(0))) = 42))))))))))),
% 4.12/0.94 inference(theory_normalization,[],[f62])).
% 4.12/0.94 tff(f78,definition,(
% 4.12/0.94 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 4.12/0.94 introduced(theory,[tha_non-reflexivity])).
% 4.12/0.94 tff(f91,plain,(
% 4.12/0.94 ~(~$less(10,0) & ((~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X0 : $int] : ((~$less(X0,length3(int,make3(int,10,t2tb(0)))) & $less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & ~$less(length2(int,t2tb2(X3)),0))) => (~$less(0,0) & $less(0,length3(int,make3(int,10,t2tb(0)))) & ! [X4 : map_int_int] : ((~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X5 : $int] : ((~$less(X5,length3(int,make3(int,10,t2tb(0)))) & $less(X5,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X4),t2tb(X5)))) & ? [X6 : $int,X7 : $int,X8 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X6),X7,t2tb2(X8))) & ~$less(length2(int,t2tb2(X8)),0)) & ? [X9 : $int,X10 : $int,X11 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X9),X10,t2tb2(X11))) & tb2t(dummy(int,make3(int,10,t2tb(0)))) = X9 & length3(int,make3(int,10,t2tb(0))) = X10 & ? [X12 : $int,X13 : map_int_int] : (tb2t2(mk_array1(int,X12,t2tb1(X13))) = X11 & length2(int,data(int,make3(int,10,t2tb(0)))) = X12 & tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = X4))) => (~$less(10,0) & ((~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X14 : $int] : ((~$less(X14,length3(int,make3(int,10,t2tb(0)))) & $less(X14,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X14)))) & ? [X15 : $int,X16 : $int,X17 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X15),X16,t2tb2(X17))) & ~$less(length2(int,t2tb2(X17)),0))) => (~$less(0,0) & $less(0,length3(int,make3(int,10,t2tb(0)))) & ! [X18 : map_int_int] : ((~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X19 : $int] : ((~$less(X19,length3(int,make3(int,10,t2tb(0)))) & $less(X19,length2(int,data(int,make3(int,10,t2tb(0)))))) => tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X18),t2tb(X19)))) & ? [X20 : $int,X21 : $int,X22 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X20),X21,t2tb2(X22))) & ~$less(length2(int,t2tb2(X22)),0)) & ? [X23 : $int,X24 : $int,X25 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X23),X24,t2tb2(X25))) & tb2t(dummy(int,make3(int,10,t2tb(0)))) = X23 & length3(int,make3(int,10,t2tb(0))) = X24 & ? [X26 : $int,X27 : map_int_int] : (tb2t2(mk_array1(int,X26,t2tb1(X27))) = X25 & length2(int,data(int,make3(int,10,t2tb(0)))) = X26 & tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = X18))) => ! [X28 : $int,X29 : map_int_int,X30 : $int] : ((~$less(X30,0) & ~$less(X28,X30) & ! [X31 : $int] : ((~$less(X31,X30) & $less(X31,X28)) => tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X29),t2tb(X31)))) & ? [X32 : $int,X33 : $int,X34 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X32),X33,t2tb2(X34))) & ~$less(X28,0)) & $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) = X30 & ! [X35 : $int] : ((~$less(X35,0) & $less(X35,X30)) => (($less(X35,length3(int,make3(int,10,t2tb(0)))) => tb2t(get(int,int,t2tb1(X4),t2tb(X35))) = tb2t(get(int,int,t2tb1(X29),t2tb(X35)))) & (~$less(X35,length3(int,make3(int,10,t2tb(0)))) => tb2t(get(int,int,t2tb1(X29),t2tb(X35))) = tb2t(get(int,int,t2tb1(X18),t2tb($sum(X35,$uminus(length3(int,make3(int,10,t2tb(0)))))))))))) => (20 = X30 & 17 = tb2t(get(int,int,t2tb1(X29),t2tb(0))) & ~$less(10,0) & $less(10,X30) & 42 = tb2t(get(int,int,t2tb1(X29),t2tb(10))) & ~$less(0,0) & $less(0,length3(int,make3(int,10,t2tb(0)))) & 42 = tb2t(get(int,int,t2tb1(X18),t2tb(0)))))))))))))),
% 4.12/0.94 inference(rectify,[],[f72])).
% 4.12/0.94 tff(f96,plain,(
% 4.12/0.94 ! [X0 : $int,X1 : $int] : (max1(X0,X1) = X0 | $less(X0,X1))),
% 4.12/0.94 inference(ennf_transformation,[],[f66])).
% 4.12/0.94 tff(f99,plain,(
% 4.12/0.94 ! [X0 : $int,X1 : $int] : (min1(X0,X1) = X1 | $less(X0,X1))),
% 4.12/0.94 inference(ennf_transformation,[],[f69])).
% 4.12/0.94 tff(f100,plain,(
% 4.12/0.94 ! [X0 : $int,X1 : $int] : (max1(X0,X1) = max1(X1,X0) | $less(X0,X1))),
% 4.12/0.94 inference(ennf_transformation,[],[f70])).
% 4.12/0.94 tff(f102,plain,(
% 4.12/0.94 ! [X0 : ty,X1 : ty,X2 : uni,X3 : uni,X4 : uni,X5 : uni] : ((get(X1,X0,set(X1,X0,X2,X3,X5),X4) = X5 | X3 != X4) | ~sort1(X1,X5))),
% 4.12/0.94 inference(ennf_transformation,[],[f21])).
% 4.12/0.94 tff(f103,plain,(
% 4.12/0.94 ! [X0 : ty,X1 : ty,X2 : uni,X3 : uni,X4 : uni,X5 : uni] : (get(X1,X0,set(X1,X0,X2,X3,X5),X4) = X5 | X3 != X4 | ~sort1(X1,X5))),
% 4.12/0.94 inference(flattening,[],[f102])).
% 4.12/0.94 tff(f109,plain,(
% 4.12/0.94 $less(10,0) | (($less(0,0) | ~$less(0,length3(int,make3(int,10,t2tb(0)))) | ? [X4 : map_int_int] : (($less(10,0) | (($less(0,0) | ~$less(0,length3(int,make3(int,10,t2tb(0)))) | ? [X18 : map_int_int] : (? [X28 : $int,X29 : map_int_int,X30 : $int] : ((20 != X30 | 17 != tb2t(get(int,int,t2tb1(X29),t2tb(0))) | $less(10,0) | ~$less(10,X30) | 42 != tb2t(get(int,int,t2tb1(X29),t2tb(10))) | $less(0,0) | ~$less(0,length3(int,make3(int,10,t2tb(0)))) | 42 != tb2t(get(int,int,t2tb1(X18),t2tb(0)))) & (~$less(X30,0) & ~$less(X28,X30) & ! [X31 : $int] : (tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X29),t2tb(X31))) | ($less(X31,X30) | ~$less(X31,X28))) & ? [X32 : $int,X33 : $int,X34 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X32),X33,t2tb2(X34))) & ~$less(X28,0)) & $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) = X30 & ! [X35 : $int] : (((tb2t(get(int,int,t2tb1(X4),t2tb(X35))) = tb2t(get(int,int,t2tb1(X29),t2tb(X35))) | ~$less(X35,length3(int,make3(int,10,t2tb(0))))) & (tb2t(get(int,int,t2tb1(X29),t2tb(X35))) = tb2t(get(int,int,t2tb1(X18),t2tb($sum(X35,$uminus(length3(int,make3(int,10,t2tb(0)))))))) | $less(X35,length3(int,make3(int,10,t2tb(0)))))) | ($less(X35,0) | ~$less(X35,X30))))) & (~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X19 : $int] : (tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X18),t2tb(X19))) | ($less(X19,length3(int,make3(int,10,t2tb(0)))) | ~$less(X19,length2(int,data(int,make3(int,10,t2tb(0))))))) & ? [X20 : $int,X21 : $int,X22 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X20),X21,t2tb2(X22))) & ~$less(length2(int,t2tb2(X22)),0)) & ? [X23 : $int,X24 : $int,X25 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X23),X24,t2tb2(X25))) & tb2t(dummy(int,make3(int,10,t2tb(0)))) = X23 & length3(int,make3(int,10,t2tb(0))) = X24 & ? [X26 : $int,X27 : map_int_int] : (tb2t2(mk_array1(int,X26,t2tb1(X27))) = X25 & length2(int,data(int,make3(int,10,t2tb(0)))) = X26 & tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = X18))))) & (~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X14 : $int] : (tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X14))) | ($less(X14,length3(int,make3(int,10,t2tb(0)))) | ~$less(X14,length2(int,data(int,make3(int,10,t2tb(0))))))) & ? [X15 : $int,X16 : $int,X17 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X15),X16,t2tb2(X17))) & ~$less(length2(int,t2tb2(X17)),0))))) & (~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X5 : $int] : (tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X4),t2tb(X5))) | ($less(X5,length3(int,make3(int,10,t2tb(0)))) | ~$less(X5,length2(int,data(int,make3(int,10,t2tb(0))))))) & ? [X6 : $int,X7 : $int,X8 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X6),X7,t2tb2(X8))) & ~$less(length2(int,t2tb2(X8)),0)) & ? [X9 : $int,X10 : $int,X11 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X9),X10,t2tb2(X11))) & tb2t(dummy(int,make3(int,10,t2tb(0)))) = X9 & length3(int,make3(int,10,t2tb(0))) = X10 & ? [X12 : $int,X13 : map_int_int] : (tb2t2(mk_array1(int,X12,t2tb1(X13))) = X11 & length2(int,data(int,make3(int,10,t2tb(0)))) = X12 & tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = X4))))) & (~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X0 : $int] : (tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) | ($less(X0,length3(int,make3(int,10,t2tb(0)))) | ~$less(X0,length2(int,data(int,make3(int,10,t2tb(0))))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & ~$less(length2(int,t2tb2(X3)),0))))),
% 4.12/0.94 inference(ennf_transformation,[],[f91])).
% 4.12/0.94 tff(f110,plain,(
% 4.12/0.94 $less(10,0) | (($less(0,0) | ~$less(0,length3(int,make3(int,10,t2tb(0)))) | ? [X4 : map_int_int] : (($less(10,0) | (($less(0,0) | ~$less(0,length3(int,make3(int,10,t2tb(0)))) | ? [X18 : map_int_int] : (? [X28 : $int,X29 : map_int_int,X30 : $int] : ((20 != X30 | 17 != tb2t(get(int,int,t2tb1(X29),t2tb(0))) | $less(10,0) | ~$less(10,X30) | 42 != tb2t(get(int,int,t2tb1(X29),t2tb(10))) | $less(0,0) | ~$less(0,length3(int,make3(int,10,t2tb(0)))) | 42 != tb2t(get(int,int,t2tb1(X18),t2tb(0)))) & ~$less(X30,0) & ~$less(X28,X30) & ! [X31 : $int] : (tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X29),t2tb(X31))) | $less(X31,X30) | ~$less(X31,X28)) & ? [X32 : $int,X33 : $int,X34 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X32),X33,t2tb2(X34))) & ~$less(X28,0)) & $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) = X30 & ! [X35 : $int] : (((tb2t(get(int,int,t2tb1(X4),t2tb(X35))) = tb2t(get(int,int,t2tb1(X29),t2tb(X35))) | ~$less(X35,length3(int,make3(int,10,t2tb(0))))) & (tb2t(get(int,int,t2tb1(X29),t2tb(X35))) = tb2t(get(int,int,t2tb1(X18),t2tb($sum(X35,$uminus(length3(int,make3(int,10,t2tb(0)))))))) | $less(X35,length3(int,make3(int,10,t2tb(0)))))) | $less(X35,0) | ~$less(X35,X30))) & ~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X19 : $int] : (tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X18),t2tb(X19))) | $less(X19,length3(int,make3(int,10,t2tb(0)))) | ~$less(X19,length2(int,data(int,make3(int,10,t2tb(0)))))) & ? [X20 : $int,X21 : $int,X22 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X20),X21,t2tb2(X22))) & ~$less(length2(int,t2tb2(X22)),0)) & ? [X23 : $int,X24 : $int,X25 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X23),X24,t2tb2(X25))) & tb2t(dummy(int,make3(int,10,t2tb(0)))) = X23 & length3(int,make3(int,10,t2tb(0))) = X24 & ? [X26 : $int,X27 : map_int_int] : (tb2t2(mk_array1(int,X26,t2tb1(X27))) = X25 & length2(int,data(int,make3(int,10,t2tb(0)))) = X26 & tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = X18)))) & ~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X14 : $int] : (tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X14))) | $less(X14,length3(int,make3(int,10,t2tb(0)))) | ~$less(X14,length2(int,data(int,make3(int,10,t2tb(0)))))) & ? [X15 : $int,X16 : $int,X17 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X15),X16,t2tb2(X17))) & ~$less(length2(int,t2tb2(X17)),0)))) & ~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X5 : $int] : (tb2t(dummy(int,make3(int,10,t2tb(0)))) = tb2t(get(int,int,t2tb1(X4),t2tb(X5))) | $less(X5,length3(int,make3(int,10,t2tb(0)))) | ~$less(X5,length2(int,data(int,make3(int,10,t2tb(0)))))) & ? [X6 : $int,X7 : $int,X8 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X6),X7,t2tb2(X8))) & ~$less(length2(int,t2tb2(X8)),0)) & ? [X9 : $int,X10 : $int,X11 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X9),X10,t2tb2(X11))) & tb2t(dummy(int,make3(int,10,t2tb(0)))) = X9 & length3(int,make3(int,10,t2tb(0))) = X10 & ? [X12 : $int,X13 : map_int_int] : (tb2t2(mk_array1(int,X12,t2tb1(X13))) = X11 & length2(int,data(int,make3(int,10,t2tb(0)))) = X12 & tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = X4)))) & ~$less(length3(int,make3(int,10,t2tb(0))),0) & ~$less(length2(int,data(int,make3(int,10,t2tb(0)))),length3(int,make3(int,10,t2tb(0)))) & ! [X0 : $int] : (tb2t(get(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(X0))) = tb2t(dummy(int,make3(int,10,t2tb(0)))) | $less(X0,length3(int,make3(int,10,t2tb(0)))) | ~$less(X0,length2(int,data(int,make3(int,10,t2tb(0)))))) & ? [X1 : $int,X2 : $int,X3 : array_int] : (tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(X1),X2,t2tb2(X3))) & ~$less(length2(int,t2tb2(X3)),0)))),
% 4.12/0.94 inference(flattening,[],[f109])).
% 4.12/0.94 tff(f120,plain,(
% 4.12/0.94 ( ! [X0 : $int,X1 : $int] : (~$less(max1(X0,X1),X0)) )),
% 4.12/0.94 inference(cnf_transformation,[],[f64])).
% 4.12/0.94 tff(f123,plain,(
% 4.12/0.94 ( ! [X0 : $int,X1 : $int] : (~$less(X0,min1(X0,X1))) )),
% 4.12/0.94 inference(cnf_transformation,[],[f65])).
% 4.12/0.94 tff(f125,plain,(
% 4.12/0.94 ( ! [X0 : $int,X1 : $int] : ($less(X0,X1) | max1(X0,X1) = X0) )),
% 4.12/0.94 inference(cnf_transformation,[],[f96])).
% 4.12/0.94 tff(f128,plain,(
% 4.12/0.94 ( ! [X0 : $int,X1 : $int] : ($less(X0,X1) | min1(X0,X1) = X1) )),
% 4.12/0.94 inference(cnf_transformation,[],[f99])).
% 4.12/0.94 tff(f129,plain,(
% 4.12/0.94 ( ! [X0 : $int,X1 : $int] : ($less(X0,X1) | max1(X0,X1) = max1(X1,X0)) )),
% 4.12/0.94 inference(cnf_transformation,[],[f100])).
% 4.12/0.94 tff(f133,plain,(
% 4.12/0.94 ( ! [X2 : uni,X3 : uni,X0 : ty,X1 : ty,X4 : uni,X5 : uni] : (~sort1(X1,X5) | X3 != X4 | get(X1,X0,set(X1,X0,X2,X3,X5),X4) = X5) )),
% 4.12/0.94 inference(cnf_transformation,[],[f103])).
% 4.12/0.94 tff(f143,plain,(
% 4.12/0.94 ( ! [X0 : $int] : (sort1(int,t2tb(X0))) )),
% 4.12/0.94 inference(cnf_transformation,[],[f31])).
% 4.12/0.94 tff(f144,plain,(
% 4.12/0.94 ( ! [X0 : $int] : (tb2t(t2tb(X0)) = X0) )),
% 4.12/0.94 inference(cnf_transformation,[],[f32])).
% 4.12/0.94 tff(f150,plain,(
% 4.12/0.94 ( ! [X2 : uni,X0 : ty,X1 : $int] : (make2(X0,X1,X2) = mk_array1(X0,X1,const(X0,int,X2))) )),
% 4.12/0.94 inference(cnf_transformation,[],[f38])).
% 4.12/0.94 tff(f154,plain,(
% 4.12/0.94 ( ! [X2 : $int,X3 : uni,X0 : ty,X1 : uni] : (length3(X0,mk_rarray1(X0,X1,X2,X3)) = X2) )),
% 4.12/0.94 inference(cnf_transformation,[],[f42])).
% 4.12/0.94 tff(f156,plain,(
% 4.12/0.94 ( ! [X2 : $int,X3 : uni,X0 : ty,X1 : uni] : (data(X0,mk_rarray1(X0,X1,X2,X3)) = X3) )),
% 4.12/0.94 inference(cnf_transformation,[],[f44])).
% 4.12/0.94 tff(f163,plain,(
% 4.12/0.94 ( ! [X2 : uni,X0 : ty,X1 : $int] : (make3(X0,X1,X2) = mk_rarray1(X0,X2,X1,make2(X0,X1,X2))) )),
% 4.12/0.94 inference(cnf_transformation,[],[f51])).
% 4.12/0.94 tff(f166,plain,(
% 4.12/0.94 ( ! [X0 : uni] : (t2tb1(tb2t1(X0)) = X0) )),
% 4.12/0.94 inference(cnf_transformation,[],[f54])).
% 4.12/0.94 tff(f172,plain,(
% 4.12/0.94 ( ! [X0 : uni] : (t2tb3(tb2t3(X0)) = X0) )),
% 4.12/0.94 inference(cnf_transformation,[],[f60])).
% 4.12/0.94 tff(f173,plain,(
% 4.12/0.94 ( ! [X35 : $int] : (~$less(X35,sK24) | $less(X35,0) | ~$less(X35,length3(int,make3(int,10,t2tb(0)))) | tb2t(get(int,int,t2tb1(sK3),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) | ~$less(0,length3(int,make3(int,10,t2tb(0)))) | $less(0,0) | $less(10,0)) )),
% 4.12/0.94 inference(cnf_transformation,[],[f110])).
% 4.12/0.94 tff(f174,plain,(
% 4.12/0.94 ( ! [X35 : $int] : (~$less(X35,sK24) | $less(X35,0) | $less(X35,length3(int,make3(int,10,t2tb(0)))) | tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK15),t2tb($sum(X35,$uminus(length3(int,make3(int,10,t2tb(0)))))))) | ~$less(0,length3(int,make3(int,10,t2tb(0)))) | $less(0,0) | $less(10,0)) )),
% 4.12/0.94 inference(cnf_transformation,[],[f110])).
% 4.12/0.94 tff(f178,plain,(
% 4.12/0.94 tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(42))) = sK15 | ~$less(0,length3(int,make3(int,10,t2tb(0)))) | $less(0,0) | $less(10,0)),
% 4.12/0.94 inference(cnf_transformation,[],[f110])).
% 4.12/0.94 tff(f181,plain,(
% 4.12/0.94 42 != tb2t(get(int,int,t2tb1(sK15),t2tb(0))) | 42 != tb2t(get(int,int,t2tb1(sK23),t2tb(10))) | ~$less(10,sK24) | 17 != tb2t(get(int,int,t2tb1(sK23),t2tb(0))) | 20 != sK24 | ~$less(0,length3(int,make3(int,10,t2tb(0)))) | $less(0,0) | $less(10,0)),
% 4.12/0.94 inference(cnf_transformation,[],[f110])).
% 4.12/0.94 tff(f182,plain,(
% 4.12/0.94 $sum(length3(int,make3(int,10,t2tb(0))),length3(int,make3(int,10,t2tb(0)))) = sK24 | ~$less(0,length3(int,make3(int,10,t2tb(0)))) | $less(0,0) | $less(10,0)),
% 4.12/0.94 inference(cnf_transformation,[],[f110])).
% 4.12/0.94 tff(f196,plain,(
% 4.12/0.94 tb2t1(set(int,int,elts(int,data(int,make3(int,10,t2tb(0)))),t2tb(0),t2tb(17))) = sK3 | ~$less(0,length3(int,make3(int,10,t2tb(0)))) | $less(0,0) | $less(10,0)),
% 4.12/0.94 inference(cnf_transformation,[],[f110])).
% 4.12/0.94 tff(f211,plain,(
% 4.12/0.94 tb2t3(make3(int,10,t2tb(0))) = tb2t3(mk_rarray1(int,t2tb(sK0),sK1,t2tb2(sK2))) | $less(10,0)),
% 4.12/0.94 inference(cnf_transformation,[],[f110])).
% 4.12/0.94 tff(f213,plain,(
% 4.12/0.94 ~$less(length3(int,make3(int,10,t2tb(0))),0) | $less(10,0)),
% 4.12/0.94 inference(cnf_transformation,[],[f110])).
% 4.12/0.94 tff(f216,plain,(
% 4.12/0.94 ( ! [X2 : uni,X0 : ty,X1 : $int] : (make3(X0,X1,X2) = mk_rarray1(X0,X2,X1,mk_array1(X0,X1,const(X0,int,X2)))) )),
% 4.12/0.94 inference(definition_unfolding,[],[f163,f150])).
% 4.12/0.94 tff(f223,plain,(
% 4.12/0.94 ~$less(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))),0) | $less(10,0)),
% 4.12/0.94 inference(definition_unfolding,[],[f213,f216])).
% 4.12/0.94 tff(f225,plain,(
% 4.12/0.94 tb2t3(mk_rarray1(int,t2tb(sK0),sK1,t2tb2(sK2))) = tb2t3(mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))) | $less(10,0)),
% 4.12/0.94 inference(definition_unfolding,[],[f211,f216])).
% 4.12/0.94 tff(f239,plain,(
% 4.12/0.94 sK3 = tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),t2tb(0),t2tb(17))) | ~$less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | $less(0,0) | $less(10,0)),
% 4.12/0.94 inference(definition_unfolding,[],[f196,f216,f216])).
% 4.12/0.94 tff(f253,plain,(
% 4.12/0.94 sK24 = $sum(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))),length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | ~$less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | $less(0,0) | $less(10,0)),
% 4.12/0.94 inference(definition_unfolding,[],[f182,f216,f216,f216])).
% 4.12/0.94 tff(f254,plain,(
% 4.12/0.94 42 != tb2t(get(int,int,t2tb1(sK15),t2tb(0))) | 42 != tb2t(get(int,int,t2tb1(sK23),t2tb(10))) | ~$less(10,sK24) | 17 != tb2t(get(int,int,t2tb1(sK23),t2tb(0))) | 20 != sK24 | ~$less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | $less(0,0) | $less(10,0)),
% 4.12/0.94 inference(definition_unfolding,[],[f181,f216])).
% 4.12/0.94 tff(f257,plain,(
% 4.12/0.94 sK15 = tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),t2tb(0),t2tb(42))) | ~$less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | $less(0,0) | $less(10,0)),
% 4.12/0.94 inference(definition_unfolding,[],[f178,f216,f216])).
% 4.12/0.94 tff(f261,plain,(
% 4.12/0.94 ( ! [X35 : $int] : (~$less(X35,sK24) | $less(X35,0) | $less(X35,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK15),t2tb($sum(X35,$uminus(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))))))) | ~$less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | $less(0,0) | $less(10,0)) )),
% 4.12/0.94 inference(definition_unfolding,[],[f174,f216,f216,f216])).
% 4.12/0.94 tff(f262,plain,(
% 4.12/0.94 ( ! [X35 : $int] : (~$less(X35,sK24) | $less(X35,0) | ~$less(X35,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | tb2t(get(int,int,t2tb1(sK3),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) | ~$less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | $less(0,0) | $less(10,0)) )),
% 4.12/0.94 inference(definition_unfolding,[],[f173,f216,f216])).
% 4.12/0.94 tff(f264,plain,(
% 4.12/0.94 ( ! [X2 : uni,X0 : ty,X1 : ty,X4 : uni,X5 : uni] : (~sort1(X1,X5) | get(X1,X0,set(X1,X0,X2,X4,X5),X4) = X5) )),
% 4.12/0.94 inference(equality_resolution,[],[f133])).
% 4.12/0.94 tff(f265,plain,(
% 4.12/0.94 ( ! [X35 : $int] : (~$less(X35,sK24) | $less(X35,0) | ~$less(X35,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | tb2t(get(int,int,t2tb1(sK3),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) | ~$less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))) )),
% 4.12/0.94 inference(evaluation,[],[f262])).
% 4.12/0.94 tff(f266,plain,(
% 4.12/0.94 ( ! [X35 : $int] : (~$less(X35,sK24) | $less(X35,0) | $less(X35,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK15),t2tb($sum(X35,$uminus(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))))))) | ~$less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))) )),
% 4.12/0.94 inference(evaluation,[],[f261])).
% 4.12/0.94 tff(f270,plain,(
% 4.12/0.94 sK15 = tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),t2tb(0),t2tb(42))) | ~$less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))),
% 4.12/0.94 inference(evaluation,[],[f257])).
% 4.12/0.94 tff(f273,plain,(
% 4.12/0.94 42 != tb2t(get(int,int,t2tb1(sK15),t2tb(0))) | 42 != tb2t(get(int,int,t2tb1(sK23),t2tb(10))) | ~$less(10,sK24) | 17 != tb2t(get(int,int,t2tb1(sK23),t2tb(0))) | 20 != sK24 | ~$less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))),
% 4.12/0.94 inference(evaluation,[],[f254])).
% 4.12/0.94 tff(f274,plain,(
% 4.12/0.94 sK24 = $sum(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))),length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | ~$less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))),
% 4.12/0.94 inference(evaluation,[],[f253])).
% 4.12/0.94 tff(f288,plain,(
% 4.12/0.94 sK3 = tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),t2tb(0),t2tb(17))) | ~$less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))),
% 4.12/0.94 inference(evaluation,[],[f239])).
% 4.12/0.94 tff(f303,plain,(
% 4.12/0.94 tb2t3(mk_rarray1(int,t2tb(sK0),sK1,t2tb2(sK2))) = tb2t3(mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),
% 4.12/0.94 inference(evaluation,[],[f225])).
% 4.12/0.94 tff(f305,plain,(
% 4.12/0.94 ~$less(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))),0)),
% 4.12/0.94 inference(evaluation,[],[f223])).
% 4.12/0.94 tff(f307,definition,(
% 4.12/0.94 spl30_1 <=> $less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_1])],[avatar_definition])).
% 4.12/0.94 tff(f309,plain,(
% 4.12/0.94 ~$less(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | spl30_1),
% 4.12/0.94 inference(avatar_component_clause,[],[f307])).
% 4.12/0.94 tff(f311,definition,(
% 4.12/0.94 spl30_2 <=> ! [X35 : $int] : (~$less(X35,sK24) | tb2t(get(int,int,t2tb1(sK3),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) | ~$less(X35,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | $less(X35,0))),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_2])],[avatar_definition])).
% 4.12/0.94 tff(f312,plain,(
% 4.12/0.94 ( ! [X35 : $int] : (~$less(X35,sK24) | tb2t(get(int,int,t2tb1(sK3),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) | ~$less(X35,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | $less(X35,0)) ) | ~spl30_2),
% 4.12/0.94 inference(avatar_component_clause,[],[f311])).
% 4.12/0.94 tff(f313,plain,(
% 4.12/0.94 ~spl30_1 | spl30_2),
% 4.12/0.94 inference(avatar_split_clause,[],[f265,f311,f307])).
% 4.12/0.94 tff(f315,definition,(
% 4.12/0.94 spl30_3 <=> ! [X35 : $int] : (~$less(X35,sK24) | tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK15),t2tb($sum(X35,$uminus(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))))))) | $less(X35,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | $less(X35,0))),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_3])],[avatar_definition])).
% 4.12/0.94 tff(f316,plain,(
% 4.12/0.94 ( ! [X35 : $int] : (~$less(X35,sK24) | tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK15),t2tb($sum(X35,$uminus(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))))))) | $less(X35,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | $less(X35,0)) ) | ~spl30_3),
% 4.12/0.94 inference(avatar_component_clause,[],[f315])).
% 4.12/0.94 tff(f317,plain,(
% 4.12/0.94 ~spl30_1 | spl30_3),
% 4.12/0.94 inference(avatar_split_clause,[],[f266,f315,f307])).
% 4.12/0.94 tff(f333,definition,(
% 4.12/0.94 spl30_7 <=> sK15 = tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),t2tb(0),t2tb(42)))),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_7])],[avatar_definition])).
% 4.12/0.94 tff(f335,plain,(
% 4.12/0.94 sK15 = tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),t2tb(0),t2tb(42))) | ~spl30_7),
% 4.12/0.94 inference(avatar_component_clause,[],[f333])).
% 4.12/0.94 tff(f336,plain,(
% 4.12/0.94 ~spl30_1 | spl30_7),
% 4.12/0.94 inference(avatar_split_clause,[],[f270,f333,f307])).
% 4.12/0.94 tff(f348,definition,(
% 4.12/0.94 spl30_10 <=> 20 = sK24),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_10])],[avatar_definition])).
% 4.12/0.94 tff(f349,plain,(
% 4.12/0.94 20 = sK24 | ~spl30_10),
% 4.12/0.94 inference(avatar_component_clause,[],[f348])).
% 4.12/0.94 tff(f352,definition,(
% 4.12/0.94 spl30_11 <=> 17 = tb2t(get(int,int,t2tb1(sK23),t2tb(0)))),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_11])],[avatar_definition])).
% 4.12/0.94 tff(f354,plain,(
% 4.12/0.94 17 != tb2t(get(int,int,t2tb1(sK23),t2tb(0))) | spl30_11),
% 4.12/0.94 inference(avatar_component_clause,[],[f352])).
% 4.12/0.94 tff(f356,definition,(
% 4.12/0.94 spl30_12 <=> $less(10,sK24)),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_12])],[avatar_definition])).
% 4.12/0.94 tff(f358,plain,(
% 4.12/0.94 ~$less(10,sK24) | spl30_12),
% 4.12/0.94 inference(avatar_component_clause,[],[f356])).
% 4.12/0.94 tff(f360,definition,(
% 4.12/0.94 spl30_13 <=> 42 = tb2t(get(int,int,t2tb1(sK23),t2tb(10)))),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_13])],[avatar_definition])).
% 4.12/0.94 tff(f364,definition,(
% 4.12/0.94 spl30_14 <=> 42 = tb2t(get(int,int,t2tb1(sK15),t2tb(0)))),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_14])],[avatar_definition])).
% 4.12/0.94 tff(f366,plain,(
% 4.12/0.94 42 != tb2t(get(int,int,t2tb1(sK15),t2tb(0))) | spl30_14),
% 4.12/0.94 inference(avatar_component_clause,[],[f364])).
% 4.12/0.94 tff(f367,plain,(
% 4.12/0.94 ~spl30_1 | ~spl30_10 | ~spl30_11 | ~spl30_12 | ~spl30_13 | ~spl30_14),
% 4.12/0.94 inference(avatar_split_clause,[],[f273,f364,f360,f356,f352,f348,f307])).
% 4.12/0.94 tff(f369,definition,(
% 4.12/0.94 spl30_15 <=> sK24 = $sum(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))),length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))))),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_15])],[avatar_definition])).
% 4.12/0.94 tff(f371,plain,(
% 4.12/0.94 sK24 = $sum(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))),length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | ~spl30_15),
% 4.12/0.94 inference(avatar_component_clause,[],[f369])).
% 4.12/0.94 tff(f372,plain,(
% 4.12/0.94 ~spl30_1 | spl30_15),
% 4.12/0.94 inference(avatar_split_clause,[],[f274,f369,f307])).
% 4.12/0.94 tff(f418,definition,(
% 4.12/0.94 spl30_25 <=> $less(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))),0)),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_25])],[avatar_definition])).
% 4.12/0.94 tff(f420,plain,(
% 4.12/0.94 ~$less(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))),0) | spl30_25),
% 4.12/0.94 inference(avatar_component_clause,[],[f418])).
% 4.12/0.94 tff(f437,definition,(
% 4.12/0.94 spl30_29 <=> sK3 = tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),t2tb(0),t2tb(17)))),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_29])],[avatar_definition])).
% 4.12/0.94 tff(f439,plain,(
% 4.12/0.94 sK3 = tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))),t2tb(0),t2tb(17))) | ~spl30_29),
% 4.12/0.94 inference(avatar_component_clause,[],[f437])).
% 4.12/0.94 tff(f440,plain,(
% 4.12/0.94 ~spl30_1 | spl30_29),
% 4.12/0.94 inference(avatar_split_clause,[],[f288,f437,f307])).
% 4.12/0.94 tff(f486,plain,(
% 4.12/0.94 ~spl30_25),
% 4.12/0.94 inference(avatar_split_clause,[],[f305,f418])).
% 4.12/0.94 tff(f492,plain,(
% 4.12/0.94 mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))) = t2tb3(tb2t3(mk_rarray1(int,t2tb(sK0),sK1,t2tb2(sK2))))),
% 4.12/0.94 inference(superposition,[],[f172,f303])).
% 4.12/0.94 tff(f494,plain,(
% 4.12/0.94 mk_rarray1(int,t2tb(sK0),sK1,t2tb2(sK2)) = mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))),
% 4.12/0.94 inference(forward_demodulation,[],[f492,f172])).
% 4.12/0.94 tff(f673,plain,(
% 4.12/0.94 ~$less(0,10) | spl30_1),
% 4.12/0.94 inference(superposition,[],[f309,f154])).
% 4.12/0.94 tff(f677,plain,(
% 4.12/0.94 $false | spl30_1),
% 4.12/0.94 inference(evaluation,[],[f673])).
% 4.12/0.94 tff(f678,plain,(
% 4.12/0.94 spl30_1),
% 4.12/0.94 inference(avatar_contradiction_clause,[],[f677])).
% 4.12/0.94 tff(f681,plain,(
% 4.12/0.94 ( ! [X35 : $int] : (~$less(X35,10) | ~$less(X35,sK24) | tb2t(get(int,int,t2tb1(sK3),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) | $less(X35,0)) ) | ~spl30_2),
% 4.12/0.94 inference(forward_demodulation,[],[f312,f154])).
% 4.12/0.94 tff(f682,plain,(
% 4.12/0.94 ( ! [X35 : $int] : (tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK15),t2tb($sum(X35,$uminus(10))))) | ~$less(X35,sK24) | $less(X35,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | $less(X35,0)) ) | ~spl30_3),
% 4.12/0.94 inference(forward_demodulation,[],[f316,f154])).
% 4.12/0.94 tff(f683,plain,(
% 4.12/0.94 ( ! [X35 : $int] : (tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK15),t2tb($sum(X35,-10)))) | ~$less(X35,sK24) | $less(X35,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) | $less(X35,0)) ) | ~spl30_3),
% 4.12/0.94 inference(evaluation,[],[f682])).
% 4.12/0.94 tff(f686,plain,(
% 4.12/0.94 sK15 = tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(sK0),sK1,t2tb2(sK2)))),t2tb(0),t2tb(42))) | ~spl30_7),
% 4.12/0.94 inference(forward_demodulation,[],[f335,f494])).
% 4.12/0.94 tff(f688,plain,(
% 4.12/0.94 sK24 = $sum(10,10) | ~spl30_15),
% 4.12/0.94 inference(forward_demodulation,[],[f371,f154])).
% 4.12/0.94 tff(f689,plain,(
% 4.12/0.94 20 = sK24 | ~spl30_15),
% 4.12/0.94 inference(evaluation,[],[f688])).
% 4.12/0.94 tff(f696,plain,(
% 4.12/0.94 sK3 = tb2t1(set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(sK0),sK1,t2tb2(sK2)))),t2tb(0),t2tb(17))) | ~spl30_29),
% 4.12/0.94 inference(forward_demodulation,[],[f439,f494])).
% 4.12/0.94 tff(f707,plain,(
% 4.12/0.94 ( ! [X35 : $int] : ($less(X35,10) | tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK15),t2tb($sum(X35,-10)))) | ~$less(X35,sK24) | $less(X35,0)) ) | ~spl30_3),
% 4.12/0.94 inference(forward_demodulation,[],[f683,f154])).
% 4.12/0.94 tff(f708,plain,(
% 4.12/0.94 spl30_10 | ~spl30_15),
% 4.12/0.94 inference(avatar_split_clause,[],[f689,f369,f348])).
% 4.12/0.94 tff(f741,plain,(
% 4.12/0.94 ~$less(10,20) | (~spl30_10 | spl30_12)),
% 4.12/0.94 inference(forward_demodulation,[],[f358,f349])).
% 4.12/0.94 tff(f742,plain,(
% 4.12/0.94 $false | (~spl30_10 | spl30_12)),
% 4.12/0.94 inference(evaluation,[],[f741])).
% 4.12/0.94 tff(f743,plain,(
% 4.12/0.94 ~spl30_10 | spl30_12),
% 4.12/0.94 inference(avatar_contradiction_clause,[],[f742])).
% 4.12/0.94 tff(f854,plain,(
% 4.12/0.94 t2tb1(sK15) = set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(sK0),sK1,t2tb2(sK2)))),t2tb(0),t2tb(42)) | ~spl30_7),
% 4.12/0.94 inference(superposition,[],[f166,f686])).
% 4.12/0.94 tff(f855,plain,(
% 4.12/0.94 t2tb1(sK3) = set(int,int,elts(int,data(int,mk_rarray1(int,t2tb(sK0),sK1,t2tb2(sK2)))),t2tb(0),t2tb(17)) | ~spl30_29),
% 4.12/0.94 inference(superposition,[],[f166,f696])).
% 4.12/0.94 tff(f859,plain,(
% 4.12/0.94 ( ! [X35 : $int] : (~$less(X35,20) | ~$less(X35,10) | tb2t(get(int,int,t2tb1(sK3),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) | $less(X35,0)) ) | (~spl30_2 | ~spl30_10)),
% 4.12/0.94 inference(forward_demodulation,[],[f681,f349])).
% 4.12/0.94 tff(f862,plain,(
% 4.12/0.94 ( ! [X0 : $int] : (~$less(X0,10) | tb2t(get(int,int,t2tb1(sK3),t2tb(X0))) = tb2t(get(int,int,t2tb1(sK23),t2tb(X0))) | $less(X0,0) | 20 = min1(X0,20)) ) | (~spl30_2 | ~spl30_10)),
% 4.12/0.94 inference(resolution,[],[f859,f128])).
% 4.12/0.94 tff(f866,plain,(
% 4.12/0.94 ( ! [X35 : $int] : (~$less(X35,20) | $less(X35,10) | tb2t(get(int,int,t2tb1(sK23),t2tb(X35))) = tb2t(get(int,int,t2tb1(sK15),t2tb($sum(X35,-10)))) | $less(X35,0)) ) | (~spl30_3 | ~spl30_10)),
% 4.12/0.94 inference(forward_demodulation,[],[f707,f349])).
% 4.12/0.94 tff(f870,plain,(
% 4.12/0.94 ( ! [X0 : $int] : ($less(X0,10) | tb2t(get(int,int,t2tb1(sK23),t2tb(X0))) = tb2t(get(int,int,t2tb1(sK15),t2tb($sum(X0,-10)))) | $less(X0,0) | 20 = min1(X0,20)) ) | (~spl30_3 | ~spl30_10)),
% 4.12/0.94 inference(resolution,[],[f866,f128])).
% 4.12/0.94 tff(f1015,plain,(
% 4.12/0.94 max1(0,length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0)))))) = max1(length3(int,mk_rarray1(int,t2tb(0),10,mk_array1(int,10,const(int,int,t2tb(0))))),0) | spl30_25),
% 4.12/0.94 inference(resolution,[],[f129,f420])).
% 4.12/0.94 tff(f1022,plain,(
% 4.12/0.94 max1(0,10) = max1(10,0) | spl30_25),
% 4.12/0.94 inference(forward_demodulation,[],[f1015,f154])).
% 4.12/0.94 tff(f1232,plain,(
% 4.12/0.94 ( ! [X2 : uni,X3 : $int,X0 : ty,X1 : uni] : (t2tb(X3) = get(int,X0,set(int,X0,X1,X2,t2tb(X3)),X2)) )),
% 4.12/0.94 inference(resolution,[],[f264,f143])).
% 4.12/0.94 tff(f1377,definition,(
% 4.12/0.94 spl30_56 <=> 0 = max1(10,0)),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_56])],[avatar_definition])).
% 4.12/0.94 tff(f1378,plain,(
% 4.12/0.94 0 != max1(10,0) | spl30_56),
% 4.12/0.94 inference(avatar_component_clause,[],[f1377])).
% 4.12/0.94 tff(f1379,plain,(
% 4.12/0.94 0 = max1(10,0) | ~spl30_56),
% 4.12/0.94 inference(avatar_component_clause,[],[f1377])).
% 4.12/0.94 tff(f1461,plain,(
% 4.12/0.94 ~$less(0,10) | ~spl30_56),
% 4.12/0.94 inference(superposition,[],[f120,f1379])).
% 4.12/0.94 tff(f1463,plain,(
% 4.12/0.94 $false | ~spl30_56),
% 4.12/0.94 inference(evaluation,[],[f1461])).
% 4.12/0.94 tff(f1464,plain,(
% 4.12/0.94 ~spl30_56),
% 4.12/0.94 inference(avatar_contradiction_clause,[],[f1463])).
% 4.12/0.94 tff(f1467,plain,(
% 4.12/0.94 0 != max1(0,10) | (spl30_25 | spl30_56)),
% 4.12/0.94 inference(superposition,[],[f1378,f1022])).
% 4.12/0.94 tff(f1827,plain,(
% 4.12/0.94 t2tb1(sK15) = set(int,int,elts(int,t2tb2(sK2)),t2tb(0),t2tb(42)) | ~spl30_7),
% 4.12/0.94 inference(forward_demodulation,[],[f854,f156])).
% 4.12/0.94 tff(f1836,plain,(
% 4.12/0.94 t2tb1(sK3) = set(int,int,elts(int,t2tb2(sK2)),t2tb(0),t2tb(17)) | ~spl30_29),
% 4.12/0.94 inference(forward_demodulation,[],[f855,f156])).
% 4.12/0.94 tff(f1893,plain,(
% 4.12/0.94 ( ! [X0 : $int] : ($less(X0,0) | tb2t(get(int,int,t2tb1(sK3),t2tb(X0))) = tb2t(get(int,int,t2tb1(sK23),t2tb(X0))) | 20 = min1(X0,20) | max1(X0,10) = X0) ) | (~spl30_2 | ~spl30_10)),
% 4.12/0.94 inference(resolution,[],[f862,f125])).
% 4.12/0.94 tff(f1936,plain,(
% 4.12/0.94 tb2t(get(int,int,t2tb1(sK23),t2tb(10))) = tb2t(get(int,int,t2tb1(sK15),t2tb($sum(10,-10)))) | $less(10,0) | 20 = min1(10,20) | (~spl30_3 | ~spl30_10)),
% 4.12/0.94 inference(resolution,[],[f870,f78])).
% 4.12/0.94 tff(f1942,plain,(
% 4.12/0.94 tb2t(get(int,int,t2tb1(sK15),t2tb(0))) = tb2t(get(int,int,t2tb1(sK23),t2tb(10))) | 20 = min1(10,20) | (~spl30_3 | ~spl30_10)),
% 4.12/0.94 inference(evaluation,[],[f1936])).
% 4.12/0.94 tff(f1952,definition,(
% 4.12/0.94 spl30_62 <=> 20 = min1(10,20)),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_62])],[avatar_definition])).
% 4.12/0.94 tff(f1954,plain,(
% 4.12/0.94 20 = min1(10,20) | ~spl30_62),
% 4.12/0.94 inference(avatar_component_clause,[],[f1952])).
% 4.12/0.94 tff(f1956,definition,(
% 4.12/0.94 spl30_63 <=> tb2t(get(int,int,t2tb1(sK15),t2tb(0))) = tb2t(get(int,int,t2tb1(sK23),t2tb(10)))),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_63])],[avatar_definition])).
% 4.12/0.94 tff(f1958,plain,(
% 4.12/0.94 tb2t(get(int,int,t2tb1(sK15),t2tb(0))) = tb2t(get(int,int,t2tb1(sK23),t2tb(10))) | ~spl30_63),
% 4.12/0.94 inference(avatar_component_clause,[],[f1956])).
% 4.12/0.94 tff(f1959,plain,(
% 4.12/0.94 spl30_62 | spl30_63 | ~spl30_3 | ~spl30_10),
% 4.12/0.94 inference(avatar_split_clause,[],[f1942,f348,f315,f1956,f1952])).
% 4.12/0.94 tff(f2581,plain,(
% 4.12/0.94 ~$less(10,20) | ~spl30_62),
% 4.12/0.94 inference(superposition,[],[f123,f1954])).
% 4.12/0.94 tff(f2583,plain,(
% 4.12/0.94 $false | ~spl30_62),
% 4.12/0.94 inference(evaluation,[],[f2581])).
% 4.12/0.94 tff(f2584,plain,(
% 4.12/0.94 ~spl30_62),
% 4.12/0.94 inference(avatar_contradiction_clause,[],[f2583])).
% 4.12/0.94 tff(f6256,plain,(
% 4.12/0.94 t2tb(42) = get(int,int,t2tb1(sK15),t2tb(0)) | ~spl30_7),
% 4.12/0.94 inference(superposition,[],[f1232,f1827])).
% 4.12/0.94 tff(f6257,plain,(
% 4.12/0.94 t2tb(17) = get(int,int,t2tb1(sK3),t2tb(0)) | ~spl30_29),
% 4.12/0.94 inference(superposition,[],[f1232,f1836])).
% 4.12/0.94 tff(f11887,plain,(
% 4.12/0.94 tb2t(get(int,int,t2tb1(sK23),t2tb(10))) = tb2t(t2tb(42)) | (~spl30_7 | ~spl30_63)),
% 4.12/0.94 inference(forward_demodulation,[],[f1958,f6256])).
% 4.12/0.94 tff(f11888,plain,(
% 4.12/0.94 42 = tb2t(get(int,int,t2tb1(sK23),t2tb(10))) | (~spl30_7 | ~spl30_63)),
% 4.12/0.94 inference(forward_demodulation,[],[f11887,f144])).
% 4.12/0.94 tff(f11889,plain,(
% 4.12/0.94 spl30_13 | ~spl30_7 | ~spl30_63),
% 4.12/0.94 inference(avatar_split_clause,[],[f11888,f1956,f333,f360])).
% 4.12/0.94 tff(f12737,plain,(
% 4.12/0.94 tb2t(get(int,int,t2tb1(sK23),t2tb(0))) = tb2t(get(int,int,t2tb1(sK3),t2tb(0))) | 20 = min1(0,20) | 0 = max1(0,10) | (~spl30_2 | ~spl30_10)),
% 4.12/0.94 inference(resolution,[],[f1893,f78])).
% 4.12/0.94 tff(f12784,plain,(
% 4.12/0.94 tb2t(get(int,int,t2tb1(sK23),t2tb(0))) = tb2t(get(int,int,t2tb1(sK3),t2tb(0))) | 20 = min1(0,20) | (~spl30_2 | ~spl30_10 | spl30_25 | spl30_56)),
% 4.12/0.94 inference(forward_subsumption_resolution,[],[f12737,f1467])).
% 4.12/0.94 tff(f12794,plain,(
% 4.12/0.94 tb2t(get(int,int,t2tb1(sK23),t2tb(0))) = tb2t(t2tb(17)) | 20 = min1(0,20) | (~spl30_2 | ~spl30_10 | spl30_25 | ~spl30_29 | spl30_56)),
% 4.12/0.94 inference(forward_demodulation,[],[f12784,f6257])).
% 4.12/0.94 tff(f12803,plain,(
% 4.12/0.94 17 = tb2t(get(int,int,t2tb1(sK23),t2tb(0))) | 20 = min1(0,20) | (~spl30_2 | ~spl30_10 | spl30_25 | ~spl30_29 | spl30_56)),
% 4.12/0.94 inference(forward_demodulation,[],[f12794,f144])).
% 4.12/0.94 tff(f12812,plain,(
% 4.12/0.94 20 = min1(0,20) | (~spl30_2 | ~spl30_10 | spl30_11 | spl30_25 | ~spl30_29 | spl30_56)),
% 4.12/0.94 inference(forward_subsumption_resolution,[],[f12803,f354])).
% 4.12/0.94 tff(f13646,plain,(
% 4.12/0.94 42 != tb2t(t2tb(42)) | (~spl30_7 | spl30_14)),
% 4.12/0.94 inference(forward_demodulation,[],[f366,f6256])).
% 4.12/0.94 tff(f13980,definition,(
% 4.12/0.94 spl30_91 <=> 20 = min1(0,20)),
% 4.12/0.94 introduced(definition,[new_symbols(definition,[spl30_91])],[avatar_definition])).
% 4.12/0.94 tff(f13982,plain,(
% 4.12/0.94 20 = min1(0,20) | ~spl30_91),
% 4.12/0.94 inference(avatar_component_clause,[],[f13980])).
% 4.12/0.94 tff(f13984,plain,(
% 4.12/0.94 $false | (~spl30_7 | spl30_14)),
% 4.12/0.94 inference(forward_subsumption_resolution,[],[f13646,f144])).
% 4.12/0.94 tff(f13985,plain,(
% 4.12/0.94 ~spl30_7 | spl30_14),
% 4.12/0.94 inference(avatar_contradiction_clause,[],[f13984])).
% 4.12/0.94 tff(f14479,plain,(
% 4.12/0.94 spl30_91 | ~spl30_2 | ~spl30_10 | spl30_11 | spl30_25 | ~spl30_29 | spl30_56),
% 4.12/0.94 inference(avatar_split_clause,[],[f12812,f1377,f437,f418,f352,f348,f311,f13980])).
% 4.12/0.94 tff(f20493,plain,(
% 4.12/0.94 ~$less(0,20) | ~spl30_91),
% 4.12/0.94 inference(superposition,[],[f123,f13982])).
% 4.12/0.94 tff(f20502,plain,(
% 4.12/0.94 $false | ~spl30_91),
% 4.12/0.94 inference(evaluation,[],[f20493])).
% 4.12/0.94 tff(f20503,plain,(
% 4.12/0.94 ~spl30_91),
% 4.12/0.94 inference(avatar_contradiction_clause,[],[f20502])).
% 4.12/0.94 cnf(s1, plain, ~spl30_1 | spl30_2, inference(sat_conversion,[],[f313])).
% 4.12/0.94 cnf(s2, plain, ~spl30_1 | spl30_3, inference(sat_conversion,[],[f317])).
% 4.12/0.94 cnf(s6, plain, ~spl30_1 | spl30_7, inference(sat_conversion,[],[f336])).
% 4.12/0.94 cnf(s9, plain, ~spl30_1 | ~spl30_10 | ~spl30_11 | ~spl30_12 | ~spl30_13 | ~spl30_14, inference(sat_conversion,[],[f367])).
% 4.12/0.94 cnf(s10, plain, ~spl30_1 | spl30_15, inference(sat_conversion,[],[f372])).
% 4.12/0.94 cnf(s24, plain, ~spl30_1 | spl30_29, inference(sat_conversion,[],[f440])).
% 4.12/0.94 cnf(s39, plain, ~spl30_25, inference(sat_conversion,[],[f486])).
% 4.12/0.94 cnf(s46, plain, spl30_1, inference(sat_conversion,[],[f678])).
% 4.12/0.94 cnf(s47, plain, spl30_10 | ~spl30_15, inference(sat_conversion,[],[f708])).
% 4.12/0.94 cnf(s52, plain, ~spl30_10 | spl30_12, inference(sat_conversion,[],[f743])).
% 4.12/0.94 cnf(s78, plain, ~spl30_56, inference(sat_conversion,[],[f1464])).
% 4.12/0.94 cnf(s83, plain, ~spl30_3 | ~spl30_10 | spl30_62 | spl30_63, inference(sat_conversion,[],[f1959])).
% 4.12/0.94 cnf(s116, plain, ~spl30_62, inference(sat_conversion,[],[f2584])).
% 4.12/0.94 cnf(s119, plain, ~spl30_7 | spl30_13 | ~spl30_63, inference(sat_conversion,[],[f11889])).
% 4.12/0.94 cnf(s142, plain, ~spl30_7 | spl30_14, inference(sat_conversion,[],[f13985])).
% 4.12/0.94 cnf(s157, plain, ~spl30_2 | ~spl30_10 | spl30_11 | spl30_25 | ~spl30_29 | spl30_56 | spl30_91, inference(sat_conversion,[],[f14479])).
% 4.12/0.94 cnf(s463, plain, ~spl30_91, inference(sat_conversion,[],[f20503])).
% 4.12/0.94 cnf(s472, plain, ~spl30_2 | ~spl30_10 | spl30_11 | spl30_25 | ~spl30_29 | spl30_56, inference(rat,[],[s157,s463])).
% 4.12/0.94 cnf(s475, plain, ~spl30_3 | ~spl30_10 | spl30_63, inference(rat,[],[s83,s116])).
% 4.12/0.94 cnf(s495, plain, spl30_29, inference(rat,[],[s24,s46])).
% 4.12/0.94 cnf(s510, plain, spl30_15, inference(rat,[],[s10,s46])).
% 4.12/0.94 cnf(s511, plain, spl30_10, inference(rat,[],[s47,s510])).
% 4.12/0.94 cnf(s517, plain, spl30_12, inference(rat,[],[s52,s511])).
% 4.12/0.94 cnf(s518, plain, ~spl30_11 | ~spl30_13 | ~spl30_14, inference(rat,[],[s9,s517,s511,s46])).
% 4.12/0.94 cnf(s521, plain, spl30_7, inference(rat,[],[s6,s46])).
% 4.12/0.94 cnf(s522, plain, spl30_14, inference(rat,[],[s142,s521])).
% 4.12/0.94 cnf(s529, plain, spl30_3, inference(rat,[],[s2,s46])).
% 4.12/0.94 cnf(s530, plain, spl30_63, inference(rat,[],[s475,s511,s529])).
% 4.12/0.94 cnf(s531, plain, spl30_13, inference(rat,[],[s119,s521,s530])).
% 4.12/0.94 cnf(s532, plain, ~spl30_11, inference(rat,[],[s518,s522,s531])).
% 4.12/0.94 cnf(s533, plain, ~spl30_2, inference(rat,[],[s472,s78,s495,s39,s511,s532])).
% 4.12/0.94 cnf(s534, plain, $false, inference(rat,[],[s1,s533,s46])).
% 4.12/0.94 tff(f20507,plain,(
% 4.12/0.94 $false),
% 4.12/0.94 inference(avatar_sat_refutation,[],[s534])).
% 4.12/0.94 % SZS output end Proof for theBenchmark
% 4.12/0.94 % (2286291)------------------------------
% 4.12/0.94 % (2286291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.12/0.94 % (2286291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.12/0.94 % (2286291)CaDiCaL version: 2.1.3
% 4.12/0.94 % (2286291)Termination reason: Refutation
% 4.12/0.94 % (2286291)Time elapsed: 0.646 s
% 4.12/0.94 % (2286291)Peak memory usage: 20 MB
% 4.12/0.94 % (2286291)Instructions burned: 1166 (million)
% 4.12/0.94 % (2286285)Success in time 0.694 s
% 4.12/0.94 % Vampire exiting
%------------------------------------------------------------------------------