%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW605_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 : n011.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:31 PM UTC 2026
% Result : Theorem 149.30s 22.07s
% Output : Refutation 149.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW605_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n011.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 14:21:15 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 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
% 3.31/0.73 % (3413807)Will run a generic schedule for satisfiability detection.
% 3.31/0.73 % (3413816)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2692903447:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.31/0.73 % (3413813)% WARNING: option uhcvi not known.
% 3.31/0.73 % (3413815)dis+10_1_sil=32000:sp=arity:random_seed=777885513:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.31/0.73 % (3413812)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1739739632_2999 on theBenchmark for (2999ds/0Mi)
% 3.31/0.73 % (3413813)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1297800503:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.31/0.73 % (3413814)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1283469494:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.31/0.73 % (3413817)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3538834526:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.31/0.73 % (3413812)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.31/0.73 % (3413812)Terminated due to inappropriate strategy.
% 3.31/0.73 % (3413812)------------------------------
% 3.31/0.73 % (3413812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.31/0.73 % (3413812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.73 % (3413812)CaDiCaL version: 2.1.3
% 3.31/0.73 % (3413812)Termination reason: Inappropriate
% 3.31/0.73 % (3413812)Time elapsed: 0.006 s
% 3.31/0.73 % (3413812)Peak memory usage: 11 MB
% 3.31/0.73 % (3413812)Instructions burned: 11 (million)
% 3.31/0.73 % (3413818)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3587022953:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.31/0.73 % (3413812)------------------------------
% 3.31/0.73 % (3413812)------------------------------
% 3.31/0.73 % (3413826)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3806125438:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.31/0.73 % (3413816)Instruction limit reached!
% 3.31/0.73 % (3413816)------------------------------
% 3.31/0.73 % (3413816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.31/0.73 % (3413816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.73 % (3413816)CaDiCaL version: 2.1.3
% 3.31/0.73 % (3413816)Termination reason: Instruction limit
% 3.31/0.73 % (3413816)Termination phase: Saturation
% 3.31/0.73 % (3413816)Time elapsed: 0.043 s
% 3.31/0.73 % (3413816)Peak memory usage: 13 MB
% 3.31/0.73 % (3413816)Instructions burned: 116 (million)
% 3.31/0.73 % (3413826)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.31/0.73 % (3413826)Terminated due to inappropriate strategy.
% 3.31/0.73 % (3413826)------------------------------
% 3.31/0.73 % (3413826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.31/0.73 % (3413826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.73 % (3413826)CaDiCaL version: 2.1.3
% 3.31/0.73 % (3413826)Termination reason: Inappropriate
% 3.31/0.73 % (3413826)Time elapsed: 0.006 s
% 3.31/0.73 % (3413826)Peak memory usage: 11 MB
% 3.31/0.73 % (3413826)Instructions burned: 9 (million)
% 3.31/0.73 % (3413826)------------------------------
% 3.31/0.73 % (3413826)------------------------------
% 3.31/0.73 % (3413828)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4133249318:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.31/0.73 % (3413829)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=351094929:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.31/0.73 % (3413815)Instruction limit reached!
% 3.31/0.73 % (3413815)------------------------------
% 3.31/0.73 % (3413815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.31/0.73 % (3413815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.31/0.73 % (3413815)CaDiCaL version: 2.1.3
% 3.31/0.73 % (3413815)Termination reason: Instruction limit
% 3.31/0.73 % (3413815)Termination phase: Saturation
% 3.31/0.73 % (3413815)Time elapsed: 0.071 s
% 3.31/0.73 % (3413815)Peak memory usage: 13 MB
% 3.31/0.73 % (3413815)Instructions burned: 104 (million)
% 3.31/0.73 % (3413817)Instruction limit reached!
% 3.31/0.73 % (3413817)------------------------------
% 3.31/0.73 % (3413817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.24 % (3413817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.24 % (3413817)CaDiCaL version: 2.1.3
% 6.67/1.24 % (3413817)Termination reason: Instruction limit
% 6.67/1.24 % (3413817)Termination phase: Saturation
% 6.67/1.24 % (3413817)Time elapsed: 0.088 s
% 6.67/1.24 % (3413817)Peak memory usage: 14 MB
% 6.67/1.24 % (3413817)Instructions burned: 132 (million)
% 6.67/1.24 % (3413832)ott-21_1_sil=16000:fs=off:random_seed=725939416:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.67/1.24 % (3413828)Instruction limit reached!
% 6.67/1.24 % (3413828)------------------------------
% 6.67/1.24 % (3413828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.24 % (3413828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.24 % (3413828)CaDiCaL version: 2.1.3
% 6.67/1.24 % (3413828)Termination reason: Instruction limit
% 6.67/1.24 % (3413828)Termination phase: Saturation
% 6.67/1.24 % (3413828)Time elapsed: 0.049 s
% 6.67/1.24 % (3413828)Peak memory usage: 13 MB
% 6.67/1.24 % (3413828)Instructions burned: 132 (million)
% 6.67/1.24 % (3413818)Instruction limit reached!
% 6.67/1.24 % (3413818)------------------------------
% 6.67/1.24 % (3413818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.24 % (3413818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.24 % (3413818)CaDiCaL version: 2.1.3
% 6.67/1.24 % (3413818)Termination reason: Instruction limit
% 6.67/1.24 % (3413818)Termination phase: Saturation
% 6.67/1.24 % (3413818)Time elapsed: 0.100 s
% 6.67/1.24 % (3413818)Peak memory usage: 14 MB
% 6.67/1.24 % (3413818)Instructions burned: 160 (million)
% 6.67/1.24 % (3413844)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1956996835:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 6.67/1.24 % (3413844)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.67/1.24 % (3413844)Terminated due to inappropriate strategy.
% 6.67/1.24 % (3413844)------------------------------
% 6.67/1.24 % (3413844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.24 % (3413844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.24 % (3413844)CaDiCaL version: 2.1.3
% 6.67/1.24 % (3413844)Termination reason: Inappropriate
% 6.67/1.24 % (3413844)Time elapsed: 0.002 s
% 6.67/1.24 % (3413844)Peak memory usage: 10 MB
% 6.67/1.24 % (3413844)Instructions burned: 10 (million)
% 6.67/1.24 % (3413844)------------------------------
% 6.67/1.24 % (3413844)------------------------------
% 6.67/1.24 % (3413841)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=904811987:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.67/1.24 % (3413850)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=105465212:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 6.67/1.24 % (3413853)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3232674039:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 6.67/1.24 % (3413853)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.67/1.24 % (3413853)Terminated due to inappropriate strategy.
% 6.67/1.24 % (3413853)------------------------------
% 6.67/1.24 % (3413853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.24 % (3413853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.24 % (3413853)CaDiCaL version: 2.1.3
% 6.67/1.24 % (3413853)Termination reason: Inappropriate
% 6.67/1.24 % (3413853)Time elapsed: 0.005 s
% 6.67/1.24 % (3413853)Peak memory usage: 10 MB
% 6.67/1.24 % (3413853)Instructions burned: 10 (million)
% 6.67/1.24 % (3413853)------------------------------
% 6.67/1.24 % (3413853)------------------------------
% 6.67/1.24 % (3413863)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=2624703040:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 6.67/1.24 % (3413832)Instruction limit reached!
% 6.67/1.24 % (3413832)------------------------------
% 6.67/1.24 % (3413832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.24 % (3413832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.24 % (3413832)CaDiCaL version: 2.1.3
% 6.67/1.24 % (3413832)Termination reason: Instruction limit
% 6.67/1.24 % (3413832)Termination phase: Saturation
% 28.15/4.25 % (3413832)Time elapsed: 0.091 s
% 28.15/4.25 % (3413832)Peak memory usage: 13 MB
% 28.15/4.25 % (3413832)Instructions burned: 180 (million)
% 28.15/4.25 % (3413884)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2269511786:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 28.15/4.25 % (3413841)Instruction limit reached!
% 28.15/4.25 % (3413841)------------------------------
% 28.15/4.25 % (3413841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.15/4.25 % (3413841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.15/4.25 % (3413841)CaDiCaL version: 2.1.3
% 28.15/4.25 % (3413841)Termination reason: Instruction limit
% 28.15/4.25 % (3413841)Termination phase: Saturation
% 28.15/4.25 % (3413841)Time elapsed: 0.247 s
% 28.15/4.25 % (3413841)Peak memory usage: 13 MB
% 28.15/4.25 % (3413841)Instructions burned: 479 (million)
% 28.15/4.25 % (3413929)fmb+10_1_sil=64000:random_seed=1308632131:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 28.15/4.25 % (3413929)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.15/4.25 % (3413929)Terminated due to inappropriate strategy.
% 28.15/4.25 % (3413929)------------------------------
% 28.15/4.25 % (3413929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.15/4.25 % (3413929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.15/4.25 % (3413929)CaDiCaL version: 2.1.3
% 28.15/4.25 % (3413929)Termination reason: Inappropriate
% 28.15/4.25 % (3413929)Time elapsed: 0.007 s
% 28.15/4.25 % (3413929)Peak memory usage: 11 MB
% 28.15/4.25 % (3413929)Instructions burned: 10 (million)
% 28.15/4.25 % (3413929)------------------------------
% 28.15/4.25 % (3413929)------------------------------
% 28.15/4.25 % (3413863)Instruction limit reached!
% 28.15/4.25 % (3413863)------------------------------
% 28.15/4.25 % (3413863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.15/4.25 % (3413863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.15/4.25 % (3413863)CaDiCaL version: 2.1.3
% 28.15/4.25 % (3413863)Termination reason: Instruction limit
% 28.15/4.25 % (3413863)Termination phase: Saturation
% 28.15/4.25 % (3413863)Time elapsed: 0.242 s
% 28.15/4.25 % (3413863)Peak memory usage: 19 MB
% 28.15/4.25 % (3413863)Instructions burned: 694 (million)
% 28.15/4.25 % (3413945)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2047057779:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 28.15/4.25 % (3413938)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2728758212:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 28.15/4.25 % (3413945)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.15/4.25 % (3413945)Terminated due to inappropriate strategy.
% 28.15/4.25 % (3413945)------------------------------
% 28.15/4.25 % (3413945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.15/4.25 % (3413945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.15/4.25 % (3413945)CaDiCaL version: 2.1.3
% 28.15/4.25 % (3413945)Termination reason: Inappropriate
% 28.15/4.25 % (3413945)Time elapsed: 0.003 s
% 28.15/4.25 % (3413945)Peak memory usage: 11 MB
% 28.15/4.25 % (3413945)Instructions burned: 10 (million)
% 28.15/4.25 % (3413945)------------------------------
% 28.15/4.25 % (3413945)------------------------------
% 28.15/4.25 % (3413938)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.15/4.25 % (3413938)Terminated due to inappropriate strategy.
% 28.15/4.25 % (3413938)------------------------------
% 28.15/4.25 % (3413938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.15/4.25 % (3413938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.15/4.25 % (3413938)CaDiCaL version: 2.1.3
% 28.15/4.25 % (3413938)Termination reason: Inappropriate
% 28.15/4.25 % (3413938)Time elapsed: 0.005 s
% 28.15/4.25 % (3413938)Peak memory usage: 11 MB
% 28.15/4.25 % (3413938)Instructions burned: 9 (million)
% 28.15/4.25 % (3413938)------------------------------
% 28.15/4.25 % (3413938)------------------------------
% 28.15/4.25 % (3413951)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1867319314:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 28.15/4.25 % (3413952)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3747619072:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 28.15/4.25 % (3413829)Instruction limit reached!
% 28.15/4.25 % (3413829)------------------------------
% 35.59/5.30 % (3413829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.59/5.30 % (3413829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.59/5.30 % (3413829)CaDiCaL version: 2.1.3
% 35.59/5.30 % (3413829)Termination reason: Instruction limit
% 35.59/5.30 % (3413829)Termination phase: Saturation
% 35.59/5.30 % (3413829)Time elapsed: 0.403 s
% 35.59/5.30 % (3413829)Peak memory usage: 18 MB
% 35.59/5.30 % (3413829)Instructions burned: 685 (million)
% 35.59/5.30 % (3413962)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1349210836:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 35.59/5.30 % (3413962)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 35.59/5.30 % (3413962)Terminated due to inappropriate strategy.
% 35.59/5.30 % (3413962)------------------------------
% 35.59/5.30 % (3413962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.59/5.30 % (3413962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.59/5.30 % (3413962)CaDiCaL version: 2.1.3
% 35.59/5.30 % (3413962)Termination reason: Inappropriate
% 35.59/5.30 % (3413962)Time elapsed: 0.006 s
% 35.59/5.30 % (3413962)Peak memory usage: 11 MB
% 35.59/5.30 % (3413962)Instructions burned: 11 (million)
% 35.59/5.30 % (3413962)------------------------------
% 35.59/5.30 % (3413962)------------------------------
% 35.59/5.30 % (3413969)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3115940708:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 35.59/5.30 % (3413969)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 35.59/5.30 % (3413969)Terminated due to inappropriate strategy.
% 35.59/5.30 % (3413969)------------------------------
% 35.59/5.30 % (3413969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.59/5.30 % (3413969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.59/5.30 % (3413969)CaDiCaL version: 2.1.3
% 35.59/5.30 % (3413969)Termination reason: Inappropriate
% 35.59/5.30 % (3413969)Time elapsed: 0.005 s
% 35.59/5.30 % (3413969)Peak memory usage: 11 MB
% 35.59/5.30 % (3413969)Instructions burned: 10 (million)
% 35.59/5.30 % (3413969)------------------------------
% 35.59/5.30 % (3413969)------------------------------
% 35.59/5.30 % (3413977)ott-2_1_sil=16000:newcnf=on:random_seed=2953638607:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 35.59/5.30 % (3413884)Instruction limit reached!
% 35.59/5.30 % (3413884)------------------------------
% 35.59/5.30 % (3413884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.59/5.30 % (3413884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.59/5.30 % (3413884)CaDiCaL version: 2.1.3
% 35.59/5.30 % (3413884)Termination reason: Instruction limit
% 35.59/5.30 % (3413884)Termination phase: Saturation
% 35.59/5.30 % (3413884)Time elapsed: 0.558 s
% 35.59/5.30 % (3413884)Peak memory usage: 18 MB
% 35.59/5.30 % (3413884)Instructions burned: 880 (million)
% 35.59/5.30 % (3413992)ott+10_1_sil=32000:tgt=ground:random_seed=2971694496:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi)
% 35.59/5.30 % (3413850)Instruction limit reached!
% 35.59/5.30 % (3413850)------------------------------
% 35.59/5.30 % (3413850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.59/5.30 % (3413850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.59/5.30 % (3413850)CaDiCaL version: 2.1.3
% 35.59/5.30 % (3413850)Termination reason: Instruction limit
% 35.59/5.30 % (3413850)Termination phase: Saturation
% 35.59/5.30 % (3413850)Time elapsed: 0.815 s
% 35.59/5.30 % (3413850)Peak memory usage: 22 MB
% 35.59/5.30 % (3413850)Instructions burned: 1180 (million)
% 35.59/5.30 % (3413994)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=606699557:i=54282_2990 on theBenchmark for (2990ds/54282Mi)
% 35.59/5.30 % (3413994)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 35.59/5.30 % (3413994)Terminated due to inappropriate strategy.
% 35.59/5.30 % (3413994)------------------------------
% 35.59/5.30 % (3413994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.59/5.30 % (3413994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.59/5.30 % (3413994)CaDiCaL version: 2.1.3
% 35.59/5.30 % (3413994)Termination reason: Inappropriate
% 35.59/5.30 % (3413994)Time elapsed: 0.006 s
% 35.59/5.30 % (3413994)Peak memory usage: 11 MB
% 35.59/5.30 % (3413994)Instructions burned: 11 (million)
% 117.57/16.85 % (3413994)------------------------------
% 117.57/16.85 % (3413994)------------------------------
% 117.57/16.85 % (3413996)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3697070759:i=3512:aac=none_2989 on theBenchmark for (2989ds/3512Mi)
% 117.57/16.85 % (3413977)Instruction limit reached!
% 117.57/16.85 % (3413977)------------------------------
% 117.57/16.85 % (3413977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.57/16.85 % (3413977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.57/16.85 % (3413977)CaDiCaL version: 2.1.3
% 117.57/16.85 % (3413977)Termination reason: Instruction limit
% 117.57/16.85 % (3413977)Termination phase: Saturation
% 117.57/16.85 % (3413977)Time elapsed: 0.485 s
% 117.57/16.85 % (3413977)Peak memory usage: 15 MB
% 117.57/16.85 % (3413977)Instructions burned: 870 (million)
% 117.57/16.85 % (3413998)dis+21_1_sil=32000:sas=cadical:random_seed=3405349322:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi)
% 117.57/16.85 % (3413952)Instruction limit reached!
% 117.57/16.85 % (3413952)------------------------------
% 117.57/16.85 % (3413952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.57/16.85 % (3413952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.57/16.85 % (3413952)CaDiCaL version: 2.1.3
% 117.57/16.85 % (3413952)Termination reason: Instruction limit
% 117.57/16.85 % (3413952)Termination phase: Saturation
% 117.57/16.85 % (3413952)Time elapsed: 1.142 s
% 117.57/16.85 % (3413952)Peak memory usage: 28 MB
% 117.57/16.85 % (3413952)Instructions burned: 1472 (million)
% 117.57/16.85 % (3414035)ott+11_1_sil=16000:gs=on:random_seed=1211586290:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2983 on theBenchmark for (2983ds/2251Mi)
% 117.57/16.85 % (3413951)Instruction limit reached!
% 117.57/16.85 % (3413951)------------------------------
% 117.57/16.85 % (3413951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.57/16.85 % (3413951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.57/16.85 % (3413951)CaDiCaL version: 2.1.3
% 117.57/16.85 % (3413951)Termination reason: Instruction limit
% 117.57/16.85 % (3413951)Termination phase: Saturation
% 117.57/16.85 % (3413951)Time elapsed: 2.157 s
% 117.57/16.85 % (3413951)Peak memory usage: 42 MB
% 117.57/16.85 % (3413951)Instructions burned: 5132 (million)
% 117.57/16.85 % (3414083)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1003139765:fmbsr=1.6:i=67534_2973 on theBenchmark for (2973ds/67534Mi)
% 117.57/16.85 % (3414083)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 117.57/16.85 % (3414083)Terminated due to inappropriate strategy.
% 117.57/16.85 % (3414083)------------------------------
% 117.57/16.85 % (3414083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.57/16.85 % (3414083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.57/16.85 % (3414083)CaDiCaL version: 2.1.3
% 117.57/16.85 % (3414083)Termination reason: Inappropriate
% 117.57/16.85 % (3414083)Time elapsed: 0.005 s
% 117.57/16.85 % (3414083)Peak memory usage: 11 MB
% 117.57/16.85 % (3414083)Instructions burned: 10 (million)
% 117.57/16.85 % (3414083)------------------------------
% 117.57/16.85 % (3414083)------------------------------
% 117.57/16.85 % (3414085)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1635659164:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2973 on theBenchmark for (2973ds/4591Mi)
% 117.57/16.85 % (3414035)Instruction limit reached!
% 117.57/16.85 % (3414035)------------------------------
% 117.57/16.85 % (3414035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.57/16.85 % (3414035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.57/16.85 % (3414035)CaDiCaL version: 2.1.3
% 117.57/16.85 % (3414035)Termination reason: Instruction limit
% 117.57/16.85 % (3414035)Termination phase: Saturation
% 117.57/16.85 % (3414035)Time elapsed: 1.989 s
% 117.57/16.85 % (3414035)Peak memory usage: 21 MB
% 117.57/16.85 % (3414035)Instructions burned: 2251 (million)
% 117.57/16.85 % (3414116)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1396832072:i=29340_2963 on theBenchmark for (2963ds/29340Mi)
% 117.57/16.85 % (3413996)Instruction limit reached!
% 117.57/16.85 % (3413996)------------------------------
% 117.57/16.85 % (3413996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.57/16.85 % (3413996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.57/16.85 % (3413996)CaDiCaL version: 2.1.3
% 117.57/16.85 % (3413996)Termination reason: Instruction limit
% 140.28/20.07 % (3413996)Termination phase: Saturation
% 140.28/20.07 % (3413996)Time elapsed: 2.993 s
% 140.28/20.07 % (3413996)Peak memory usage: 39 MB
% 140.28/20.07 % (3413996)Instructions burned: 3512 (million)
% 140.28/20.07 % (3414129)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3742436304:i=5211_2959 on theBenchmark for (2959ds/5211Mi)
% 140.28/20.07 % (3413998)Instruction limit reached!
% 140.28/20.07 % (3413998)------------------------------
% 140.28/20.07 % (3413998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.28/20.07 % (3413998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.28/20.07 % (3413998)CaDiCaL version: 2.1.3
% 140.28/20.07 % (3413998)Termination reason: Instruction limit
% 140.28/20.07 % (3413998)Termination phase: Saturation
% 140.28/20.07 % (3413998)Time elapsed: 3.456 s
% 140.28/20.07 % (3413998)Peak memory usage: 37 MB
% 140.28/20.07 % (3413998)Instructions burned: 3774 (million)
% 140.28/20.07 % (3414142)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=718287200:i=5497:nm=2_2954 on theBenchmark for (2954ds/5497Mi)
% 140.28/20.07 % (3414142)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 140.28/20.07 % (3414142)Terminated due to inappropriate strategy.
% 140.28/20.07 % (3414142)------------------------------
% 140.28/20.07 % (3414142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.28/20.07 % (3414142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.28/20.07 % (3414142)CaDiCaL version: 2.1.3
% 140.28/20.07 % (3414142)Termination reason: Inappropriate
% 140.28/20.07 % (3414142)Time elapsed: 0.011 s
% 140.28/20.07 % (3414142)Peak memory usage: 11 MB
% 140.28/20.07 % (3414142)Instructions burned: 11 (million)
% 140.28/20.07 % (3414142)------------------------------
% 140.28/20.07 % (3414142)------------------------------
% 140.28/20.07 % (3414144)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1795276131:fmbsr=2:i=46332_2953 on theBenchmark for (2953ds/46332Mi)
% 140.28/20.07 % (3414144)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 140.28/20.07 % (3414144)Terminated due to inappropriate strategy.
% 140.28/20.07 % (3414144)------------------------------
% 140.28/20.07 % (3414144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.28/20.07 % (3414144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.28/20.07 % (3414144)CaDiCaL version: 2.1.3
% 140.28/20.07 % (3414144)Termination reason: Inappropriate
% 140.28/20.07 % (3414144)Time elapsed: 0.006 s
% 140.28/20.07 % (3414144)Peak memory usage: 11 MB
% 140.28/20.07 % (3414144)Instructions burned: 10 (million)
% 140.28/20.07 % (3414144)------------------------------
% 140.28/20.07 % (3414144)------------------------------
% 140.28/20.07 % (3414148)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1778825881:i=14071_2953 on theBenchmark for (2953ds/14071Mi)
% 140.28/20.07 % (3414148)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 140.28/20.07 % (3414148)Terminated due to inappropriate strategy.
% 140.28/20.07 % (3414148)------------------------------
% 140.28/20.07 % (3414148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.28/20.07 % (3414148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.28/20.07 % (3414148)CaDiCaL version: 2.1.3
% 140.28/20.07 % (3414148)Termination reason: Inappropriate
% 140.28/20.07 % (3414148)Time elapsed: 0.009 s
% 140.28/20.07 % (3414148)Peak memory usage: 11 MB
% 140.28/20.07 % (3414148)Instructions burned: 10 (million)
% 140.28/20.07 % (3414148)------------------------------
% 140.28/20.07 % (3414148)------------------------------
% 140.28/20.07 % (3414150)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4268363579:i=22565:add=on:rawr=on_2953 on theBenchmark for (2953ds/22565Mi)
% 140.28/20.07 % (3414085)Instruction limit reached!
% 140.28/20.07 % (3414085)------------------------------
% 140.28/20.07 % (3414085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.28/20.07 % (3414085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.28/20.07 % (3414085)CaDiCaL version: 2.1.3
% 140.28/20.07 % (3414085)Termination reason: Instruction limit
% 140.28/20.07 % (3414085)Termination phase: Saturation
% 140.28/20.07 % (3414085)Time elapsed: 2.380 s
% 140.28/20.07 % (3414085)Peak memory usage: 58 MB
% 140.28/20.07 % (3414085)Instructions burned: 4591 (million)
% 140.28/20.07 % (3414159)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2483720267:i=8173:av=off_2949 on theBenchmark for (2949ds/8173Mi)
% 141.23/20.21 % (3413992)Instruction limit reached!
% 141.23/20.21 % (3413992)------------------------------
% 141.23/20.21 % (3413992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 141.23/20.21 % (3413992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.23/20.21 % (3413992)CaDiCaL version: 2.1.3
% 141.23/20.21 % (3413992)Termination reason: Instruction limit
% 141.23/20.21 % (3413992)Termination phase: Saturation
% 141.23/20.21 % (3413992)Time elapsed: 4.334 s
% 141.23/20.21 % (3413992)Peak memory usage: 43 MB
% 141.23/20.21 % (3413992)Instructions burned: 5114 (million)
% 141.23/20.21 % (3414161)dis+10_16:1_sil=16000:random_seed=2560585244:i=9155:fsr=off_2948 on theBenchmark for (2948ds/9155Mi)
% 141.23/20.21 % (3414129)Instruction limit reached!
% 141.23/20.21 % (3414129)------------------------------
% 141.23/20.21 % (3414129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 141.23/20.21 % (3414129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.23/20.21 % (3414129)CaDiCaL version: 2.1.3
% 141.23/20.21 % (3414129)Termination reason: Instruction limit
% 141.23/20.21 % (3414129)Termination phase: Saturation
% 141.23/20.21 % (3414129)Time elapsed: 3.014 s
% 141.23/20.21 % (3414129)Peak memory usage: 43 MB
% 141.23/20.21 % (3414129)Instructions burned: 5212 (million)
% 141.23/20.21 % (3414316)ott-3_8_sil=64000:random_seed=2638736236:i=20139:bs=on_2929 on theBenchmark for (2929ds/20139Mi)
% 141.23/20.21 % (3414159)Instruction limit reached!
% 141.23/20.21 % (3414159)------------------------------
% 141.23/20.21 % (3414159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 141.23/20.21 % (3414159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.23/20.21 % (3414159)CaDiCaL version: 2.1.3
% 141.23/20.21 % (3414159)Termination reason: Instruction limit
% 141.23/20.21 % (3414159)Termination phase: Saturation
% 141.23/20.21 % (3414159)Time elapsed: 2.519 s
% 141.23/20.21 % (3414159)Peak memory usage: 71 MB
% 141.23/20.21 % (3414159)Instructions burned: 8174 (million)
% 141.23/20.21 % (3414318)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1431353024:fmbsr=2:i=32576_2924 on theBenchmark for (2924ds/32576Mi)
% 141.23/20.21 % (3414318)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 141.23/20.21 % (3414318)Terminated due to inappropriate strategy.
% 141.23/20.21 % (3414318)------------------------------
% 141.23/20.21 % (3414318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 141.23/20.21 % (3414318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.23/20.21 % (3414318)CaDiCaL version: 2.1.3
% 141.23/20.21 % (3414318)Termination reason: Inappropriate
% 141.23/20.21 % (3414318)Time elapsed: 0.006 s
% 141.23/20.21 % (3414318)Peak memory usage: 11 MB
% 141.23/20.21 % (3414318)Instructions burned: 11 (million)
% 141.23/20.21 % (3414318)------------------------------
% 141.23/20.21 % (3414318)------------------------------
% 141.23/20.21 % (3414320)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3504126743:i=11404_2923 on theBenchmark for (2923ds/11404Mi)
% 141.23/20.21 % (3414161)Instruction limit reached!
% 141.23/20.21 % (3414161)------------------------------
% 141.23/20.21 % (3414161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 141.23/20.21 % (3414161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.23/20.21 % (3414161)CaDiCaL version: 2.1.3
% 141.23/20.21 % (3414161)Termination reason: Instruction limit
% 141.23/20.21 % (3414161)Termination phase: Saturation
% 141.23/20.21 % (3414161)Time elapsed: 4.843 s
% 141.23/20.21 % (3414161)Peak memory usage: 53 MB
% 141.23/20.21 % (3414161)Instructions burned: 9155 (million)
% 141.23/20.21 % (3414322)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=574278574:i=14134_2899 on theBenchmark for (2899ds/14134Mi)
% 141.23/20.21 % (3414320)Instruction limit reached!
% 141.23/20.21 % (3414320)------------------------------
% 141.23/20.21 % (3414320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 141.23/20.21 % (3414320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.23/20.21 % (3414320)CaDiCaL version: 2.1.3
% 141.23/20.21 % (3414320)Termination reason: Instruction limit
% 141.23/20.21 % (3414320)Termination phase: Saturation
% 141.23/20.21 % (3414320)Time elapsed: 3.794 s
% 141.23/20.21 % (3414320)Peak memory usage: 76 MB
% 141.23/20.21 % (3414320)Instructions burned: 11406 (million)
% 141.23/20.21 % (3414324)dis+33_16_sil=32000:sac=on:random_seed=1069082480:i=15851:nm=0_2885 on theBenchmark for (2885ds/15851Mi)
% 141.23/20.21 % (3414324)Instruction limit reached!
% 141.23/20.21 % (3414324)------------------------------
% 141.23/20.21 % (3414324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.30/22.07 % (3414324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.30/22.07 % (3414324)CaDiCaL version: 2.1.3
% 149.30/22.07 % (3414324)Termination reason: Instruction limit
% 149.30/22.07 % (3414324)Termination phase: Saturation
% 149.30/22.07 % (3414324)Time elapsed: 5.173 s
% 149.30/22.07 % (3414324)Peak memory usage: 178 MB
% 149.30/22.07 % (3414324)Instructions burned: 15852 (million)
% 149.30/22.07 % (3414374)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4195565768:avsq=on:i=17627:add=on:amm=off_2833 on theBenchmark for (2833ds/17627Mi)
% 149.30/22.07 % (3414322)Instruction limit reached!
% 149.30/22.07 % (3414322)------------------------------
% 149.30/22.07 % (3414322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.30/22.07 % (3414322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.30/22.07 % (3414322)CaDiCaL version: 2.1.3
% 149.30/22.07 % (3414322)Termination reason: Instruction limit
% 149.30/22.07 % (3414322)Termination phase: Saturation
% 149.30/22.07 % (3414322)Time elapsed: 8.616 s
% 149.30/22.07 % (3414322)Peak memory usage: 82 MB
% 149.30/22.07 % (3414322)Instructions burned: 14135 (million)
% 149.30/22.07 % (3414377)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3092360897:s2a=on:i=53295_2813 on theBenchmark for (2813ds/53295Mi)
% 149.30/22.07 % (3414116)Instruction limit reached!
% 149.30/22.07 % (3414116)------------------------------
% 149.30/22.07 % (3414116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.30/22.07 % (3414116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.30/22.07 % (3414116)CaDiCaL version: 2.1.3
% 149.30/22.07 % (3414116)Termination reason: Instruction limit
% 149.30/22.07 % (3414116)Termination phase: Saturation
% 149.30/22.07 % (3414116)Time elapsed: 15.042 s
% 149.30/22.07 % (3414116)Peak memory usage: 235 MB
% 149.30/22.07 % (3414116)Instructions burned: 29342 (million)
% 149.30/22.07 % (3414379)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3994300621:i=26857:ins=20_2812 on theBenchmark for (2812ds/26857Mi)
% 149.30/22.07 % (3414379)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 149.30/22.07 % (3414379)Terminated due to inappropriate strategy.
% 149.30/22.07 % (3414379)------------------------------
% 149.30/22.07 % (3414379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.30/22.07 % (3414379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.30/22.07 % (3414379)CaDiCaL version: 2.1.3
% 149.30/22.07 % (3414379)Termination reason: Inappropriate
% 149.30/22.07 % (3414379)Time elapsed: 0.005 s
% 149.30/22.07 % (3414379)Peak memory usage: 11 MB
% 149.30/22.07 % (3414379)Instructions burned: 10 (million)
% 149.30/22.07 % (3414379)------------------------------
% 149.30/22.07 % (3414379)------------------------------
% 149.30/22.07 % (3414381)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1023894754:i=28120:bs=on:fsr=off_2812 on theBenchmark for (2812ds/28120Mi)
% 149.30/22.07 % (3414316)Instruction limit reached!
% 149.30/22.07 % (3414316)------------------------------
% 149.30/22.07 % (3414316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.30/22.07 % (3414316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.30/22.07 % (3414316)CaDiCaL version: 2.1.3
% 149.30/22.07 % (3414316)Termination reason: Instruction limit
% 149.30/22.07 % (3414316)Termination phase: Saturation
% 149.30/22.07 % (3414316)Time elapsed: 12.653 s
% 149.30/22.07 % (3414316)Peak memory usage: 163 MB
% 149.30/22.07 % (3414316)Instructions burned: 20140 (million)
% 149.30/22.07 % (3414383)fmb+10_1_sil=256000:fmbss=7:random_seed=1779330840:fmbsr=1.6:i=182295_2802 on theBenchmark for (2802ds/182295Mi)
% 149.30/22.07 % (3414383)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 149.30/22.07 % (3414383)Terminated due to inappropriate strategy.
% 149.30/22.07 % (3414383)------------------------------
% 149.30/22.07 % (3414383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.30/22.07 % (3414383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.30/22.07 % (3414383)CaDiCaL version: 2.1.3
% 149.30/22.07 % (3414383)Termination reason: Inappropriate
% 149.30/22.07 % (3414383)Time elapsed: 0.005 s
% 149.30/22.07 % (3414383)Peak memory usage: 11 MB
% 149.30/22.07 % (3414383)Instructions burned: 10 (million)
% 149.30/22.07 % (3414383)------------------------------
% 149.30/22.07 % (3414383)------------------------------
% 149.30/22.07 % (3414385)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=52280114:i=44625:gsp=on_2801 on theBenchmark for (2801ds/44625Mi)
% 149.30/22.07 % (3414385)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 149.30/22.07 % (3414385)Terminated due to inappropriate strategy.
% 149.30/22.07 % (3414385)------------------------------
% 149.30/22.07 % (3414385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.30/22.07 % (3414385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.30/22.07 % (3414385)CaDiCaL version: 2.1.3
% 149.30/22.07 % (3414385)Termination reason: Inappropriate
% 149.30/22.07 % (3414385)Time elapsed: 0.006 s
% 149.30/22.07 % (3414385)Peak memory usage: 11 MB
% 149.30/22.07 % (3414385)Instructions burned: 10 (million)
% 149.30/22.07 % (3414385)------------------------------
% 149.30/22.07 % (3414385)------------------------------
% 149.30/22.07 % (3414387)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3865484071:i=160505_2801 on theBenchmark for (2801ds/160505Mi)
% 149.30/22.07 % (3414387)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 149.30/22.07 % (3414387)Terminated due to inappropriate strategy.
% 149.30/22.07 % (3414387)------------------------------
% 149.30/22.07 % (3414387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.30/22.07 % (3414387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.30/22.07 % (3414387)CaDiCaL version: 2.1.3
% 149.30/22.07 % (3414387)Termination reason: Inappropriate
% 149.30/22.07 % (3414387)Time elapsed: 0.005 s
% 149.30/22.07 % (3414387)Peak memory usage: 11 MB
% 149.30/22.07 % (3414387)Instructions burned: 10 (million)
% 149.30/22.07 % (3414387)------------------------------
% 149.30/22.07 % (3414387)------------------------------
% 149.30/22.07 % (3414389)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3850370281:fmbsr=1.3:i=225729_2801 on theBenchmark for (2801ds/225729Mi)
% 149.30/22.07 % (3414389)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 149.30/22.07 % (3414389)Terminated due to inappropriate strategy.
% 149.30/22.07 % (3414389)------------------------------
% 149.30/22.07 % (3414389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.30/22.07 % (3414389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.30/22.07 % (3414389)CaDiCaL version: 2.1.3
% 149.30/22.07 % (3414389)Termination reason: Inappropriate
% 149.30/22.07 % (3414389)Time elapsed: 0.006 s
% 149.30/22.07 % (3414389)Peak memory usage: 11 MB
% 149.30/22.07 % (3414389)Instructions burned: 10 (million)
% 149.30/22.07 % (3414389)------------------------------
% 149.30/22.07 % (3414389)------------------------------
% 149.30/22.07 % (3414391)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3409841928:fmbsr=2:i=185024:ins=7_2801 on theBenchmark for (2801ds/185024Mi)
% 149.30/22.07 % (3414391)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 149.30/22.07 % (3414391)Terminated due to inappropriate strategy.
% 149.30/22.07 % (3414391)------------------------------
% 149.30/22.07 % (3414391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.30/22.07 % (3414391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.30/22.07 % (3414391)CaDiCaL version: 2.1.3
% 149.30/22.07 % (3414391)Termination reason: Inappropriate
% 149.30/22.07 % (3414391)Time elapsed: 0.006 s
% 149.30/22.07 % (3414391)Peak memory usage: 11 MB
% 149.30/22.07 % (3414391)Instructions burned: 10 (million)
% 149.30/22.07 % (3414391)------------------------------
% 149.30/22.07 % (3414391)------------------------------
% 149.30/22.07 % (3414393)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3906357283:rtra=on_2800 on theBenchmark for (2800ds/0Mi)
% 149.30/22.07 % (3414393)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 149.30/22.07 % (3414393)Terminated due to inappropriate strategy.
% 149.30/22.07 % (3414393)------------------------------
% 149.30/22.07 % (3414393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.30/22.07 % (3414393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.30/22.07 % (3414393)CaDiCaL version: 2.1.3
% 149.30/22.07 % (3414393)Termination reason: Inappropriate
% 149.30/22.07 % (3414393)Time elapsed: 0.007 s
% 149.30/22.07 % (3414393)Peak memory usage: 11 MB
% 149.30/22.07 % (3414393)Instructions burned: 12 (million)
% 149.30/22.07 % (3414393)------------------------------
% 149.30/22.07 % (3414393)------------------------------
% 149.30/22.07 % (3414395)% WARNING: option uhcvi not known.
% 149.30/22.07 % (3414395)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3464365267:i=271062:add=off:rtra=on:rawr=on_2800 on theBenchmark for (2800ds/271062Mi)
% 149.30/22.07 % (3414150)Instruction limit reached!
% 149.30/22.07 % (3414150)------------------------------
% 149.30/22.07 % (3414150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.30/22.07 % (3414150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.30/22.07 % (3414150)CaDiCaL version: 2.1.3
% 149.30/22.07 % (3414150)Termination reason: Instruction limit
% 149.30/22.07 % (3414150)Termination phase: Saturation
% 149.30/22.07 % (3414150)Time elapsed: 15.576 s
% 149.30/22.07 % (3414150)Peak memory usage: 135 MB
% 149.30/22.07 % (3414150)Instructions burned: 22566 (million)
% 149.30/22.07 % (3414397)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2794086588:i=176048:add=on:rtra=on:rawr=on_2796 on theBenchmark for (2796ds/176048Mi)
% 149.30/22.07 % (3414374)Instruction limit reached!
% 149.30/22.07 % (3414374)------------------------------
% 149.30/22.07 % (3414374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.30/22.07 % (3414374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.30/22.07 % (3414374)CaDiCaL version: 2.1.3
% 149.30/22.07 % (3414374)Termination reason: Instruction limit
% 149.30/22.07 % (3414374)Termination phase: Saturation
% 149.30/22.07 % (3414374)Time elapsed: 5.104 s
% 149.30/22.07 % (3414374)Peak memory usage: 336 MB
% 149.30/22.07 % (3414374)Instructions burned: 17628 (million)
% 149.30/22.07 % (3414399)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3916359779:i=206:fgj=on:rtra=on_2782 on theBenchmark for (2782ds/206Mi)
% 149.30/22.07 % (3414395) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3413807-3414395"...
% 149.30/22.07 % (3414395)...printing done.
% 149.30/22.07 % (3414395)Refutation found. Thanks to Tanya!
% 149.30/22.07 % SZS status Theorem for theBenchmark
% 149.30/22.07 % SZS output start Proof for theBenchmark
% 149.30/22.07 tff(type_def_5, type, uni: $tType).
% 149.30/22.07 tff(type_def_6, type, ty: $tType).
% 149.30/22.07 tff(type_def_7, type, bool1: $tType).
% 149.30/22.07 tff(type_def_8, type, tuple02: $tType).
% 149.30/22.07 tff(type_def_9, type, key1: $tType).
% 149.30/22.07 tff(type_def_10, type, a1: $tType).
% 149.30/22.07 tff(type_def_11, type, map_int_lplist_lpkeycm_a1rprp: $tType).
% 149.30/22.07 tff(type_def_12, type, map_key_lpoption_a1rp: $tType).
% 149.30/22.07 tff(type_def_13, type, option_a1: $tType).
% 149.30/22.07 tff(type_def_14, type, array_lplist_lpkeycm_a1rprp: $tType).
% 149.30/22.07 tff(type_def_15, type, list_lpkeycm_a1rp: $tType).
% 149.30/22.07 tff(type_def_16, type, lpkeycm_a1rp: $tType).
% 149.30/22.07 tff(func_def_0, type, witness1: ty > uni).
% 149.30/22.07 tff(func_def_1, type, int: ty).
% 149.30/22.07 tff(func_def_2, type, real: ty).
% 149.30/22.07 tff(func_def_3, type, bool: ty).
% 149.30/22.07 tff(func_def_4, type, true1: bool1).
% 149.30/22.07 tff(func_def_5, type, false1: bool1).
% 149.30/22.07 tff(func_def_6, type, match_bool1: (ty * bool1 * uni * uni) > uni).
% 149.30/22.07 tff(func_def_7, type, tuple0: ty).
% 149.30/22.07 tff(func_def_8, type, tuple03: tuple02).
% 149.30/22.07 tff(func_def_9, type, qtmark: ty).
% 149.30/22.07 tff(func_def_12, type, abs1: $int > $int).
% 149.30/22.07 tff(func_def_14, type, div1: ($int * $int) > $int).
% 149.30/22.07 tff(func_def_15, type, mod1: ($int * $int) > $int).
% 149.30/22.07 tff(func_def_18, type, option: ty > ty).
% 149.30/22.07 tff(func_def_19, type, none: ty > uni).
% 149.30/22.07 tff(func_def_20, type, some: (ty * uni) > uni).
% 149.30/22.07 tff(func_def_21, type, match_option1: (ty * ty * uni * uni * uni) > uni).
% 149.30/22.07 tff(func_def_22, type, some_proj_11: (ty * uni) > uni).
% 149.30/22.07 tff(func_def_23, type, list: ty > ty).
% 149.30/22.07 tff(func_def_24, type, nil: ty > uni).
% 149.30/22.07 tff(func_def_25, type, cons: (ty * uni * uni) > uni).
% 149.30/22.07 tff(func_def_26, type, match_list1: (ty * ty * uni * uni * uni) > uni).
% 149.30/22.07 tff(func_def_27, type, cons_proj_11: (ty * uni) > uni).
% 149.30/22.07 tff(func_def_28, type, cons_proj_21: (ty * uni) > uni).
% 149.30/22.07 tff(func_def_29, type, map: (ty * ty) > ty).
% 149.30/22.07 tff(func_def_30, type, get: (ty * ty * uni * uni) > uni).
% 149.30/22.07 tff(func_def_31, type, set: (ty * ty * uni * uni * uni) > uni).
% 149.30/22.07 tff(func_def_32, type, const: (ty * ty * uni) > uni).
% 149.30/22.07 tff(func_def_33, type, array: ty > ty).
% 149.30/22.07 tff(func_def_34, type, mk_array1: (ty * $int * uni) > uni).
% 149.30/22.07 tff(func_def_35, type, length1: (ty * uni) > $int).
% 149.30/22.07 tff(func_def_36, type, elts: (ty * uni) > uni).
% 149.30/22.07 tff(func_def_37, type, get2: (ty * uni * $int) > uni).
% 149.30/22.07 tff(func_def_38, type, t2tb: $int > uni).
% 149.30/22.07 tff(func_def_39, type, tb2t: uni > $int).
% 149.30/22.07 tff(func_def_40, type, set2: (ty * uni * $int * uni) > uni).
% 149.30/22.07 tff(func_def_41, type, make1: (ty * $int * uni) > uni).
% 149.30/22.07 tff(func_def_42, type, key: ty).
% 149.30/22.07 tff(func_def_43, type, hash1: key1 > $int).
% 149.30/22.07 tff(func_def_44, type, bucket1: (key1 * $int) > $int).
% 149.30/22.07 tff(func_def_45, type, tuple2: (ty * ty) > ty).
% 149.30/22.07 tff(func_def_46, type, tuple21: (ty * ty * uni * uni) > uni).
% 149.30/22.07 tff(func_def_47, type, tuple2_proj_11: (ty * ty * uni) > uni).
% 149.30/22.07 tff(func_def_48, type, tuple2_proj_21: (ty * ty * uni) > uni).
% 149.30/22.07 tff(func_def_49, type, t2tb1: key1 > uni).
% 149.30/22.07 tff(func_def_50, type, tb2t1: uni > key1).
% 149.30/22.07 tff(func_def_51, type, t: ty > ty).
% 149.30/22.07 tff(func_def_52, type, mk_t1: (ty * $int * uni * uni) > uni).
% 149.30/22.07 tff(func_def_53, type, size1: (ty * uni) > $int).
% 149.30/22.07 tff(func_def_54, type, data: (ty * uni) > uni).
% 149.30/22.07 tff(func_def_55, type, view: (ty * uni) > uni).
% 149.30/22.07 tff(func_def_56, type, a: ty).
% 149.30/22.07 tff(func_def_57, type, t2tb2: map_int_lplist_lpkeycm_a1rprp > uni).
% 149.30/22.07 tff(func_def_58, type, tb2t2: uni > map_int_lplist_lpkeycm_a1rprp).
% 149.30/22.07 tff(func_def_59, type, t2tb3: map_key_lpoption_a1rp > uni).
% 149.30/22.07 tff(func_def_60, type, tb2t3: uni > map_key_lpoption_a1rp).
% 149.30/22.07 tff(func_def_61, type, t2tb4: option_a1 > uni).
% 149.30/22.07 tff(func_def_62, type, tb2t4: uni > option_a1).
% 149.30/22.07 tff(func_def_63, type, t2tb5: array_lplist_lpkeycm_a1rprp > uni).
% 149.30/22.07 tff(func_def_64, type, tb2t5: uni > array_lplist_lpkeycm_a1rprp).
% 149.30/22.07 tff(func_def_65, type, t2tb6: list_lpkeycm_a1rp > uni).
% 149.30/22.07 tff(func_def_66, type, tb2t6: uni > list_lpkeycm_a1rp).
% 149.30/22.07 tff(func_def_67, type, t2tb8: lpkeycm_a1rp > uni).
% 149.30/22.07 tff(func_def_68, type, tb2t8: uni > lpkeycm_a1rp).
% 149.30/22.07 tff(func_def_69, type, t2tb7: a1 > uni).
% 149.30/22.07 tff(func_def_70, type, tb2t7: uni > a1).
% 149.30/22.07 tff(func_def_72, type, sK0: map_int_lplist_lpkeycm_a1rprp).
% 149.30/22.07 tff(func_def_73, type, sK1: map_key_lpoption_a1rp).
% 149.30/22.07 tff(func_def_74, type, sK2: $int).
% 149.30/22.07 tff(func_def_75, type, sK3: map_int_lplist_lpkeycm_a1rprp).
% 149.30/22.07 tff(func_def_76, type, sK4: map_int_lplist_lpkeycm_a1rprp).
% 149.30/22.07 tff(func_def_77, type, sK5: list_lpkeycm_a1rp).
% 149.30/22.07 tff(func_def_78, type, sK6: $int).
% 149.30/22.07 tff(func_def_79, type, sK7: $int).
% 149.30/22.07 tff(func_def_80, type, sK8: map_key_lpoption_a1rp).
% 149.30/22.07 tff(func_def_81, type, sK9: key1).
% 149.30/22.07 tff(func_def_82, type, sK10: a1).
% 149.30/22.07 tff(func_def_83, type, sK12: ($int * ty * uni) > key1).
% 149.30/22.07 tff(func_def_84, type, sK13: ($int * ty * uni) > uni).
% 149.30/22.07 tff(pred_def_1, type, sort1: (ty * uni) > $o).
% 149.30/22.07 tff(pred_def_4, type, mem: (ty * uni * uni) > $o).
% 149.30/22.07 tff(pred_def_5, type, in_data1: (ty * key1 * uni * uni) > $o).
% 149.30/22.07 tff(pred_def_6, type, good_data1: (ty * key1 * uni * uni * uni) > $o).
% 149.30/22.07 tff(pred_def_7, type, good_hash1: (ty * uni * $int) > $o).
% 149.30/22.07 tff(pred_def_8, type, sP11: (a1 * key1 * list_lpkeycm_a1rp * map_int_lplist_lpkeycm_a1rprp * $int) > $o).
% 149.30/22.07 tff(f27,axiom,(
% 149.30/22.07 ! [X1 : uni,X0 : ty] : sort1(option(X0),some(X0,X1))),
% 149.30/22.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',some_sort2)).
% 149.30/22.07 tff(f46,axiom,(
% 149.30/22.07 ! [X0 : ty,X1 : uni] : (sort1(X0,X1) => (~mem(X0,X1,nil(X0)) & ! [X3 : uni,X2 : uni] : (sort1(X0,X2) => (mem(X0,X1,cons(X0,X2,X3)) <=> (mem(X0,X1,X3) | X1 = X2)))))),
% 149.30/22.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_def)).
% 149.30/22.07 tff(f47,axiom,(
% 149.30/22.07 ! [X1 : ty,X0 : ty,X2 : uni,X3 : uni] : sort1(X1,get(X1,X0,X2,X3))),
% 149.30/22.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',get_sort4)).
% 149.30/22.07 tff(f68,axiom,(
% 149.30/22.07 ! [X0 : key1,X1 : $int] : bucket1(X0,X1) = mod1(hash1(X0),X1)),
% 149.30/22.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bucket_def)).
% 149.30/22.07 tff(f69,axiom,(
% 149.30/22.07 ! [X0 : $int] : ($less(0,X0) => ! [X1 : key1] : ($less(bucket1(X1,X0),X0) & $lesseq(0,bucket1(X1,X0))))),
% 149.30/22.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bucket_bounds)).
% 149.30/22.07 tff(f70,axiom,(
% 149.30/22.07 ! [X0 : ty,X3 : uni,X1 : ty,X2 : uni] : sort1(tuple2(X1,X0),tuple21(X1,X0,X2,X3))),
% 149.30/22.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tuple2_sort2)).
% 149.30/22.07 tff(f80,axiom,(
% 149.30/22.07 ! [X1 : key1,X2 : uni,X3 : uni,X4 : uni,X0 : ty] : ((get(option(X0),key,X3,t2tb1(X1)) = some(X0,X2) <=> in_data1(X0,X1,X2,X4)) <=> good_data1(X0,X1,X2,X3,X4))),
% 149.30/22.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',good_data_def)).
% 149.30/22.07 tff(f97,axiom,(
% 149.30/22.07 ! [X0 : uni] : (sort1(option(a),X0) => t2tb4(tb2t4(X0)) = X0)),
% 149.30/22.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR4)).
% 149.30/22.07 tff(f103,axiom,(
% 149.30/22.07 ! [X0 : uni] : t2tb6(tb2t6(X0)) = X0),
% 149.30/22.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR6)).
% 149.30/22.07 tff(f110,conjecture,(
% 149.30/22.07 ! [X2 : map_key_lpoption_a1rp,X1 : map_int_lplist_lpkeycm_a1rprp,X0 : $int] : ((! [X3 : $int] : (($less(X3,X0) & $lesseq(0,X3)) => good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)),X3)) & $less(0,X0) & $lesseq(0,X0) & ! [X4 : key1,X5 : a1] : good_data1(a,X4,t2tb7(X5),t2tb3(X2),mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)))) => ($lesseq(0,$sum($product(2,X0),1)) => ($lesseq(0,$sum($product(2,X0),1)) => ! [X8 : map_key_lpoption_a1rp,X7 : map_int_lplist_lpkeycm_a1rprp,X9 : $int,X10 : map_int_lplist_lpkeycm_a1rprp,X6 : list_lpkeycm_a1rp,X3 : $int] : (($less(0,X9) & ! [X5 : a1,X4 : key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),X9,t2tb2(X10))) & ! [X4 : key1,X5 : a1] : ((~($less(bucket1(X4,X0),X3) & $lesseq(0,bucket1(X4,X0))) & ((bucket1(X4,X0) != X3 & ~in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)))) | ((tb2t4(get(option(a),key,t2tb3(X8),t2tb1(X4))) = tb2t4(some(a,t2tb7(X5))) <=> (mem(tuple2(key,a),tuple21(key,a,t2tb1(X4),t2tb7(X5)),t2tb6(X6)) | in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))))) & bucket1(X4,X0) = X3))) | ($lesseq(0,bucket1(X4,X0)) & $less(bucket1(X4,X0),X3) & good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))))) & ! [X11 : $int] : (($less(X11,X9) & $lesseq(0,X11)) => good_hash1(a,mk_array1(list(tuple2(key,a)),X9,t2tb2(X10)),X11)) & $lesseq(0,X9) & ! [X12 : $int] : (($lesseq(0,X12) & $less(X12,$sum($product(2,X0),1))) => good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)),X12)) & $lesseq(0,$sum($product(2,X0),1)) & ! [X5 : a1,X4 : key1] : (mem(tuple2(key,a),tuple21(key,a,t2tb1(X4),t2tb7(X5)),t2tb6(X6)) => bucket1(X4,X0) = X3)) => (X6 = tb2t6(nil(tuple2(key,a))) => ! [X4 : key1,X5 : a1] : ((~($lesseq(0,bucket1(X4,X0)) & $lesseq(bucket1(X4,X0),X3)) => ~in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)))) & (($lesseq(bucket1(X4,X0),X3) & $lesseq(0,bucket1(X4,X0))) => good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))))))))))),
% 149.30/22.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_resize)).
% 149.30/22.07 tff(f111,negated_conjecture,(
% 149.30/22.07 ~ ! [X2 : map_key_lpoption_a1rp,X1 : map_int_lplist_lpkeycm_a1rprp,X0 : $int] : ((! [X3 : $int] : (($less(X3,X0) & $lesseq(0,X3)) => good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)),X3)) & $less(0,X0) & $lesseq(0,X0) & ! [X4 : key1,X5 : a1] : good_data1(a,X4,t2tb7(X5),t2tb3(X2),mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)))) => ($lesseq(0,$sum($product(2,X0),1)) => ($lesseq(0,$sum($product(2,X0),1)) => ! [X8 : map_key_lpoption_a1rp,X7 : map_int_lplist_lpkeycm_a1rprp,X9 : $int,X10 : map_int_lplist_lpkeycm_a1rprp,X6 : list_lpkeycm_a1rp,X3 : $int] : (($less(0,X9) & ! [X5 : a1,X4 : key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),X9,t2tb2(X10))) & ! [X4 : key1,X5 : a1] : ((~($less(bucket1(X4,X0),X3) & $lesseq(0,bucket1(X4,X0))) & ((bucket1(X4,X0) != X3 & ~in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)))) | ((tb2t4(get(option(a),key,t2tb3(X8),t2tb1(X4))) = tb2t4(some(a,t2tb7(X5))) <=> (mem(tuple2(key,a),tuple21(key,a,t2tb1(X4),t2tb7(X5)),t2tb6(X6)) | in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))))) & bucket1(X4,X0) = X3))) | ($lesseq(0,bucket1(X4,X0)) & $less(bucket1(X4,X0),X3) & good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))))) & ! [X11 : $int] : (($less(X11,X9) & $lesseq(0,X11)) => good_hash1(a,mk_array1(list(tuple2(key,a)),X9,t2tb2(X10)),X11)) & $lesseq(0,X9) & ! [X12 : $int] : (($lesseq(0,X12) & $less(X12,$sum($product(2,X0),1))) => good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)),X12)) & $lesseq(0,$sum($product(2,X0),1)) & ! [X5 : a1,X4 : key1] : (mem(tuple2(key,a),tuple21(key,a,t2tb1(X4),t2tb7(X5)),t2tb6(X6)) => bucket1(X4,X0) = X3)) => (X6 = tb2t6(nil(tuple2(key,a))) => ! [X4 : key1,X5 : a1] : ((~($lesseq(0,bucket1(X4,X0)) & $lesseq(bucket1(X4,X0),X3)) => ~in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)))) & (($lesseq(bucket1(X4,X0),X3) & $lesseq(0,bucket1(X4,X0))) => good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))))))))))),
% 149.30/22.07 inference(negated_conjecture,[status(cth)],[f110])).
% 149.30/22.07 tff(f115,plain,(
% 149.30/22.07 ~ ! [X2 : map_key_lpoption_a1rp,X1 : map_int_lplist_lpkeycm_a1rprp,X0 : $int] : ((! [X3 : $int] : (($less(X3,X0) & ~$less(X3,0)) => good_hash1(a,mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)),X3)) & $less(0,X0) & ~$less(X0,0) & ! [X4 : key1,X5 : a1] : good_data1(a,X4,t2tb7(X5),t2tb3(X2),mk_array1(list(tuple2(key,a)),X0,t2tb2(X1)))) => (~$less($sum($product(2,X0),1),0) => (~$less($sum($product(2,X0),1),0) => ! [X8 : map_key_lpoption_a1rp,X7 : map_int_lplist_lpkeycm_a1rprp,X9 : $int,X10 : map_int_lplist_lpkeycm_a1rprp,X6 : list_lpkeycm_a1rp,X3 : $int] : (($less(0,X9) & ! [X5 : a1,X4 : key1] : good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),X9,t2tb2(X10))) & ! [X4 : key1,X5 : a1] : ((~($less(bucket1(X4,X0),X3) & ~$less(bucket1(X4,X0),0)) & ((bucket1(X4,X0) != X3 & ~in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)))) | ((tb2t4(get(option(a),key,t2tb3(X8),t2tb1(X4))) = tb2t4(some(a,t2tb7(X5))) <=> (mem(tuple2(key,a),tuple21(key,a,t2tb1(X4),t2tb7(X5)),t2tb6(X6)) | in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))))) & bucket1(X4,X0) = X3))) | (~$less(bucket1(X4,X0),0) & $less(bucket1(X4,X0),X3) & good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))))) & ! [X11 : $int] : (($less(X11,X9) & ~$less(X11,0)) => good_hash1(a,mk_array1(list(tuple2(key,a)),X9,t2tb2(X10)),X11)) & ~$less(X9,0) & ! [X12 : $int] : ((~$less(X12,0) & $less(X12,$sum($product(2,X0),1))) => good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)),X12)) & ~$less($sum($product(2,X0),1),0) & ! [X5 : a1,X4 : key1] : (mem(tuple2(key,a),tuple21(key,a,t2tb1(X4),t2tb7(X5)),t2tb6(X6)) => bucket1(X4,X0) = X3)) => (X6 = tb2t6(nil(tuple2(key,a))) => ! [X4 : key1,X5 : a1] : ((~(~$less(bucket1(X4,X0),0) & ~$less(X3,bucket1(X4,X0))) => ~in_data1(a,X4,t2tb7(X5),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7)))) & ((~$less(X3,bucket1(X4,X0)) & ~$less(bucket1(X4,X0),0)) => good_data1(a,X4,t2tb7(X5),t2tb3(X8),mk_array1(list(tuple2(key,a)),$sum($product(2,X0),1),t2tb2(X7))))))))))),
% 149.30/22.07 inference(theory_normalization,[],[f111])).
% 149.30/22.07 tff(f125,plain,(
% 149.30/22.07 ! [X0 : $int] : ($less(0,X0) => ! [X1 : key1] : (~$less(bucket1(X1,X0),0) & $less(bucket1(X1,X0),X0)))),
% 149.30/22.07 inference(theory_normalization,[],[f69])).
% 149.30/22.07 tff(f129,definition,(
% 149.30/22.07 ( ! [X0 : $int,X1 : $int] : ($sum(X1,X0) = $sum(X0,X1)) )),
% 149.30/22.07 introduced(theory,[tha_commutativity])).
% 149.30/22.07 tff(f134,definition,(
% 149.30/22.07 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 149.30/22.07 introduced(theory,[tha_non-reflexivity])).
% 149.30/22.07 tff(f135,definition,(
% 149.30/22.07 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,X2) | $less(X0,X2)) )),
% 149.30/22.07 introduced(theory,[tha_transitivity])).
% 149.30/22.07 tff(f136,definition,(
% 149.30/22.07 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 149.30/22.07 introduced(theory,[tha_order_totality])).
% 149.30/22.07 tff(f151,plain,(
% 149.30/22.07 ! [X0 : ty,X1 : uni,X2 : ty,X3 : uni] : sort1(tuple2(X2,X0),tuple21(X2,X0,X3,X1))),
% 149.30/22.07 inference(rectify,[],[f70])).
% 149.30/22.07 tff(f161,plain,(
% 149.30/22.07 ! [X0 : ty,X1 : uni] : (sort1(X0,X1) => (~mem(X0,X1,nil(X0)) & ! [X3 : uni,X2 : uni] : (sort1(X0,X3) => ((mem(X0,X1,X2) | X1 = X3) <=> mem(X0,X1,cons(X0,X3,X2))))))),
% 149.30/22.07 inference(rectify,[],[f46])).
% 149.30/22.07 tff(f164,plain,(
% 149.30/22.07 ~ ! [X1 : map_int_lplist_lpkeycm_a1rprp,X2 : $int,X0 : map_key_lpoption_a1rp] : ((! [X4 : key1,X5 : a1] : good_data1(a,X4,t2tb7(X5),t2tb3(X0),mk_array1(list(tuple2(key,a)),X2,t2tb2(X1))) & ! [X3 : $int] : ((~$less(X3,0) & $less(X3,X2)) => good_hash1(a,mk_array1(list(tuple2(key,a)),X2,t2tb2(X1)),X3)) & $less(0,X2) & ~$less(X2,0)) => (~$less($sum($product(2,X2),1),0) => (~$less($sum($product(2,X2),1),0) => ! [X11 : $int,X10 : list_lpkeycm_a1rp,X7 : map_int_lplist_lpkeycm_a1rprp,X8 : $int,X9 : map_int_lplist_lpkeycm_a1rprp,X6 : map_key_lpoption_a1rp] : ((~$less(X8,0) & $less(0,X8) & ! [X17 : $int] : ((~$less(X17,0) & $less(X17,$sum($product(2,X2),1))) => good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7)),X17)) & ! [X18 : a1,X19 : key1] : (mem(tuple2(key,a),tuple21(key,a,t2tb1(X19),t2tb7(X18)),t2tb6(X10)) => bucket1(X19,X2) = X11) & ~$less($sum($product(2,X2),1),0) & ! [X15 : a1,X14 : key1] : (($less(bucket1(X14,X2),X11) & good_data1(a,X14,t2tb7(X15),t2tb3(X6),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7))) & ~$less(bucket1(X14,X2),0)) | (~(~$less(bucket1(X14,X2),0) & $less(bucket1(X14,X2),X11)) & ((~in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7))) & bucket1(X14,X2) != X11) | (bucket1(X14,X2) = X11 & ((mem(tuple2(key,a),tuple21(key,a,t2tb1(X14),t2tb7(X15)),t2tb6(X10)) | in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7)))) <=> tb2t4(some(a,t2tb7(X15))) = tb2t4(get(option(a),key,t2tb3(X6),t2tb1(X14)))))))) & ! [X12 : a1,X13 : key1] : good_data1(a,X13,t2tb7(X12),t2tb3(X6),mk_array1(list(tuple2(key,a)),X8,t2tb2(X9))) & ! [X16 : $int] : ((~$less(X16,0) & $less(X16,X8)) => good_hash1(a,mk_array1(list(tuple2(key,a)),X8,t2tb2(X9)),X16))) => (tb2t6(nil(tuple2(key,a))) = X10 => ! [X21 : a1,X20 : key1] : ((~(~$less(bucket1(X20,X2),0) & ~$less(X11,bucket1(X20,X2))) => ~in_data1(a,X20,t2tb7(X21),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7)))) & ((~$less(X11,bucket1(X20,X2)) & ~$less(bucket1(X20,X2),0)) => good_data1(a,X20,t2tb7(X21),t2tb3(X6),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7))))))))))),
% 149.30/22.07 inference(rectify,[],[f115])).
% 149.30/22.07 tff(f176,plain,(
% 149.30/22.07 ! [X3 : uni,X0 : ty,X2 : uni,X1 : ty] : sort1(X0,get(X0,X1,X2,X3))),
% 149.30/22.07 inference(rectify,[],[f47])).
% 149.30/22.07 tff(f193,plain,(
% 149.30/22.07 ! [X0 : uni,X1 : ty] : sort1(option(X1),some(X1,X0))),
% 149.30/22.07 inference(rectify,[],[f27])).
% 149.30/22.07 tff(f203,plain,(
% 149.30/22.07 ! [X1 : uni,X4 : ty,X2 : uni,X3 : uni,X0 : key1] : (good_data1(X4,X0,X1,X2,X3) <=> (in_data1(X4,X0,X1,X3) <=> get(option(X4),key,X2,t2tb1(X0)) = some(X4,X1)))),
% 149.30/22.07 inference(rectify,[],[f80])).
% 149.30/22.07 tff(f213,plain,(
% 149.30/22.07 ! [X0 : uni] : (~sort1(option(a),X0) | t2tb4(tb2t4(X0)) = X0)),
% 149.30/22.07 inference(ennf_transformation,[],[f97])).
% 149.30/22.07 tff(f227,plain,(
% 149.30/22.07 ? [X1 : map_int_lplist_lpkeycm_a1rprp,X2 : $int,X0 : map_key_lpoption_a1rp] : (((? [X11 : $int,X10 : list_lpkeycm_a1rp,X7 : map_int_lplist_lpkeycm_a1rprp,X8 : $int,X9 : map_int_lplist_lpkeycm_a1rprp,X6 : map_key_lpoption_a1rp] : ((? [X21 : a1,X20 : key1] : ((in_data1(a,X20,t2tb7(X21),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7))) & ($less(X11,bucket1(X20,X2)) | $less(bucket1(X20,X2),0))) | (~good_data1(a,X20,t2tb7(X21),t2tb3(X6),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7))) & (~$less(X11,bucket1(X20,X2)) & ~$less(bucket1(X20,X2),0)))) & tb2t6(nil(tuple2(key,a))) = X10) & (~$less(X8,0) & $less(0,X8) & ! [X17 : $int] : (good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7)),X17) | ($less(X17,0) | ~$less(X17,$sum($product(2,X2),1)))) & ! [X18 : a1,X19 : key1] : (~mem(tuple2(key,a),tuple21(key,a,t2tb1(X19),t2tb7(X18)),t2tb6(X10)) | bucket1(X19,X2) = X11) & ~$less($sum($product(2,X2),1),0) & ! [X14 : key1,X15 : a1] : ((((~in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7))) & bucket1(X14,X2) != X11) | (bucket1(X14,X2) = X11 & ((mem(tuple2(key,a),tuple21(key,a,t2tb1(X14),t2tb7(X15)),t2tb6(X10)) | in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7)))) <=> tb2t4(some(a,t2tb7(X15))) = tb2t4(get(option(a),key,t2tb3(X6),t2tb1(X14)))))) & (~$less(bucket1(X14,X2),X11) | $less(bucket1(X14,X2),0))) | ($less(bucket1(X14,X2),X11) & good_data1(a,X14,t2tb7(X15),t2tb3(X6),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7))) & ~$less(bucket1(X14,X2),0))) & ! [X12 : a1,X13 : key1] : good_data1(a,X13,t2tb7(X12),t2tb3(X6),mk_array1(list(tuple2(key,a)),X8,t2tb2(X9))) & ! [X16 : $int] : (good_hash1(a,mk_array1(list(tuple2(key,a)),X8,t2tb2(X9)),X16) | ($less(X16,0) | ~$less(X16,X8))))) & ~$less($sum($product(2,X2),1),0)) & ~$less($sum($product(2,X2),1),0)) & (! [X4 : key1,X5 : a1] : good_data1(a,X4,t2tb7(X5),t2tb3(X0),mk_array1(list(tuple2(key,a)),X2,t2tb2(X1))) & ! [X3 : $int] : (good_hash1(a,mk_array1(list(tuple2(key,a)),X2,t2tb2(X1)),X3) | ($less(X3,0) | ~$less(X3,X2))) & $less(0,X2) & ~$less(X2,0)))),
% 149.30/22.07 inference(ennf_transformation,[],[f164])).
% 149.30/22.07 tff(f228,plain,(
% 149.30/22.07 ? [X1 : map_int_lplist_lpkeycm_a1rprp,X0 : map_key_lpoption_a1rp,X2 : $int] : (! [X3 : $int] : (~$less(X3,X2) | $less(X3,0) | good_hash1(a,mk_array1(list(tuple2(key,a)),X2,t2tb2(X1)),X3)) & ~$less($sum($product(2,X2),1),0) & ~$less(X2,0) & ! [X4 : key1,X5 : a1] : good_data1(a,X4,t2tb7(X5),t2tb3(X0),mk_array1(list(tuple2(key,a)),X2,t2tb2(X1))) & ? [X7 : map_int_lplist_lpkeycm_a1rprp,X9 : map_int_lplist_lpkeycm_a1rprp,X10 : list_lpkeycm_a1rp,X11 : $int,X8 : $int,X6 : map_key_lpoption_a1rp] : ($less(0,X8) & ~$less(X8,0) & ! [X18 : a1,X19 : key1] : (~mem(tuple2(key,a),tuple21(key,a,t2tb1(X19),t2tb7(X18)),t2tb6(X10)) | bucket1(X19,X2) = X11) & ! [X14 : key1,X15 : a1] : ((((~in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7))) & bucket1(X14,X2) != X11) | (bucket1(X14,X2) = X11 & ((mem(tuple2(key,a),tuple21(key,a,t2tb1(X14),t2tb7(X15)),t2tb6(X10)) | in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7)))) <=> tb2t4(some(a,t2tb7(X15))) = tb2t4(get(option(a),key,t2tb3(X6),t2tb1(X14)))))) & (~$less(bucket1(X14,X2),X11) | $less(bucket1(X14,X2),0))) | ($less(bucket1(X14,X2),X11) & good_data1(a,X14,t2tb7(X15),t2tb3(X6),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7))) & ~$less(bucket1(X14,X2),0))) & ~$less($sum($product(2,X2),1),0) & ! [X17 : $int] : (~$less(X17,$sum($product(2,X2),1)) | good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7)),X17) | $less(X17,0)) & tb2t6(nil(tuple2(key,a))) = X10 & ! [X12 : a1,X13 : key1] : good_data1(a,X13,t2tb7(X12),t2tb3(X6),mk_array1(list(tuple2(key,a)),X8,t2tb2(X9))) & ? [X20 : key1,X21 : a1] : ((in_data1(a,X20,t2tb7(X21),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7))) & ($less(X11,bucket1(X20,X2)) | $less(bucket1(X20,X2),0))) | (~$less(bucket1(X20,X2),0) & ~good_data1(a,X20,t2tb7(X21),t2tb3(X6),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7))) & ~$less(X11,bucket1(X20,X2)))) & ! [X16 : $int] : (good_hash1(a,mk_array1(list(tuple2(key,a)),X8,t2tb2(X9)),X16) | ~$less(X16,X8) | $less(X16,0))) & ~$less($sum($product(2,X2),1),0) & $less(0,X2))),
% 149.30/22.07 inference(flattening,[],[f227])).
% 149.30/22.07 tff(f237,plain,(
% 149.30/22.07 ! [X0 : $int] : (! [X1 : key1] : (~$less(bucket1(X1,X0),0) & $less(bucket1(X1,X0),X0)) | ~$less(0,X0))),
% 149.30/22.07 inference(ennf_transformation,[],[f125])).
% 149.30/22.07 tff(f250,plain,(
% 149.30/22.07 ! [X0 : ty,X1 : uni] : (~sort1(X0,X1) | (! [X3 : uni,X2 : uni] : (((mem(X0,X1,X2) | X1 = X3) <=> mem(X0,X1,cons(X0,X3,X2))) | ~sort1(X0,X3)) & ~mem(X0,X1,nil(X0))))),
% 149.30/22.07 inference(ennf_transformation,[],[f161])).
% 149.30/22.07 tff(f275,plain,(
% 149.30/22.07 ( ! [X0 : ty,X1 : uni] : (~mem(X0,X1,nil(X0)) | ~sort1(X0,X1)) )),
% 149.30/22.07 inference(cnf_transformation,[],[f250])).
% 149.30/22.07 tff(f281,plain,(
% 149.30/22.07 ( ! [X2 : $int,X10 : list_lpkeycm_a1rp,X7 : map_int_lplist_lpkeycm_a1rprp,X14 : key1,X15 : a1] : (~in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7))) | sP11(X15,X14,X10,X7,X2)) )),
% 149.30/22.07 inference(cnf_transformation,[],[f228])).
% 149.30/22.07 tff(f283,plain,(
% 149.30/22.07 ( ! [X2 : $int,X10 : list_lpkeycm_a1rp,X7 : map_int_lplist_lpkeycm_a1rprp,X14 : key1,X15 : a1] : (in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7))) | ~sP11(X15,X14,X10,X7,X2) | mem(tuple2(key,a),tuple21(key,a,t2tb1(X14),t2tb7(X15)),t2tb6(X10))) )),
% 149.30/22.07 inference(cnf_transformation,[],[f228])).
% 149.30/22.07 tff(f285,plain,(
% 149.30/22.07 ( ! [X14 : key1,X15 : a1] : ($less(bucket1(X14,sK2),sK6) | tb2t4(some(a,t2tb7(X15))) = tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(X14))) | ~sP11(X15,X14,sK5,sK3,sK2) | ~in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3)))) )),
% 149.30/22.07 inference(cnf_transformation,[],[f228])).
% 149.30/22.07 tff(f286,plain,(
% 149.30/22.07 ( ! [X14 : key1,X15 : a1] : ($less(bucket1(X14,sK2),sK6) | tb2t4(some(a,t2tb7(X15))) != tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(X14))) | sP11(X15,X14,sK5,sK3,sK2) | sK6 != bucket1(X14,sK2)) )),
% 149.30/22.07 inference(cnf_transformation,[],[f228])).
% 149.30/22.07 tff(f298,plain,(
% 149.30/22.07 ( ! [X14 : key1,X15 : a1] : ($less(bucket1(X14,sK2),sK6) | sK6 = bucket1(X14,sK2) | ~in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3)))) )),
% 149.30/22.07 inference(cnf_transformation,[],[f228])).
% 149.30/22.07 tff(f299,plain,(
% 149.30/22.07 ( ! [X14 : key1,X15 : a1] : (good_data1(a,X14,t2tb7(X15),t2tb3(sK8),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3))) | $less(bucket1(X14,sK2),0) | ~$less(bucket1(X14,sK2),sK6)) )),
% 149.30/22.07 inference(cnf_transformation,[],[f228])).
% 149.30/22.07 tff(f300,plain,(
% 149.30/22.07 ~good_data1(a,sK9,t2tb7(sK10),t2tb3(sK8),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3))) | $less(bucket1(sK9,sK2),0) | $less(sK6,bucket1(sK9,sK2))),
% 149.30/22.07 inference(cnf_transformation,[],[f228])).
% 149.30/22.07 tff(f303,plain,(
% 149.30/22.07 ~$less(sK6,bucket1(sK9,sK2)) | in_data1(a,sK9,t2tb7(sK10),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3)))),
% 149.30/22.07 inference(cnf_transformation,[],[f228])).
% 149.30/22.07 tff(f309,plain,(
% 149.30/22.07 tb2t6(nil(tuple2(key,a))) = sK5),
% 149.30/22.07 inference(cnf_transformation,[],[f228])).
% 149.30/22.07 tff(f313,plain,(
% 149.30/22.07 $less(0,sK2)),
% 149.30/22.07 inference(cnf_transformation,[],[f228])).
% 149.30/22.07 tff(f322,plain,(
% 149.30/22.07 ( ! [X0 : key1,X1 : $int] : (bucket1(X0,X1) = mod1(hash1(X0),X1)) )),
% 149.30/22.07 inference(cnf_transformation,[],[f68])).
% 149.30/22.07 tff(f326,plain,(
% 149.30/22.07 ( ! [X0 : $int,X1 : key1] : (~$less(0,X0) | ~$less(bucket1(X1,X0),0)) )),
% 149.30/22.07 inference(cnf_transformation,[],[f237])).
% 149.30/22.07 tff(f338,plain,(
% 149.30/22.07 ( ! [X0 : uni] : (t2tb6(tb2t6(X0)) = X0) )),
% 149.30/22.07 inference(cnf_transformation,[],[f103])).
% 149.30/22.07 tff(f370,plain,(
% 149.30/22.07 ( ! [X0 : uni] : (~sort1(option(a),X0) | t2tb4(tb2t4(X0)) = X0) )),
% 149.30/22.07 inference(cnf_transformation,[],[f213])).
% 149.30/22.07 tff(f373,plain,(
% 149.30/22.07 ( ! [X2 : uni,X3 : uni,X0 : ty,X1 : ty] : (sort1(X0,get(X0,X1,X2,X3))) )),
% 149.30/22.07 inference(cnf_transformation,[],[f176])).
% 149.30/22.07 tff(f393,plain,(
% 149.30/22.07 ( ! [X2 : uni,X3 : uni,X0 : key1,X1 : uni,X4 : ty] : (good_data1(X4,X0,X1,X2,X3) | in_data1(X4,X0,X1,X3) | get(option(X4),key,X2,t2tb1(X0)) = some(X4,X1)) )),
% 149.30/22.07 inference(cnf_transformation,[],[f203])).
% 149.30/22.07 tff(f394,plain,(
% 149.30/22.07 ( ! [X2 : uni,X3 : uni,X0 : key1,X1 : uni,X4 : ty] : (get(option(X4),key,X2,t2tb1(X0)) != some(X4,X1) | good_data1(X4,X0,X1,X2,X3) | ~in_data1(X4,X0,X1,X3)) )),
% 149.30/22.07 inference(cnf_transformation,[],[f203])).
% 149.30/22.07 tff(f406,plain,(
% 149.30/22.07 ( ! [X0 : uni,X1 : ty] : (sort1(option(X1),some(X1,X0))) )),
% 149.30/22.07 inference(cnf_transformation,[],[f193])).
% 149.30/22.07 tff(f414,plain,(
% 149.30/22.07 ( ! [X2 : ty,X3 : uni,X0 : ty,X1 : uni] : (sort1(tuple2(X2,X0),tuple21(X2,X0,X3,X1))) )),
% 149.30/22.07 inference(cnf_transformation,[],[f151])).
% 149.30/22.07 tff(f422,plain,(
% 149.30/22.07 ~$less(sK6,mod1(hash1(sK9),sK2)) | in_data1(a,sK9,t2tb7(sK10),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3)))),
% 149.30/22.07 inference(definition_unfolding,[],[f303,f322])).
% 149.30/22.07 tff(f424,plain,(
% 149.30/22.07 $less(sK6,mod1(hash1(sK9),sK2)) | ~good_data1(a,sK9,t2tb7(sK10),t2tb3(sK8),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3))) | $less(mod1(hash1(sK9),sK2),0)),
% 149.30/22.07 inference(definition_unfolding,[],[f300,f322,f322])).
% 149.30/22.07 tff(f425,plain,(
% 149.30/22.07 ( ! [X14 : key1,X15 : a1] : (~$less(mod1(hash1(X14),sK2),sK6) | $less(mod1(hash1(X14),sK2),0) | good_data1(a,X14,t2tb7(X15),t2tb3(sK8),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3)))) )),
% 149.30/22.07 inference(definition_unfolding,[],[f299,f322,f322])).
% 149.30/22.07 tff(f426,plain,(
% 149.30/22.07 ( ! [X14 : key1,X15 : a1] : (~in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3))) | $less(mod1(hash1(X14),sK2),sK6) | sK6 = mod1(hash1(X14),sK2)) )),
% 149.30/22.07 inference(definition_unfolding,[],[f298,f322,f322])).
% 149.30/22.07 tff(f436,plain,(
% 149.30/22.07 ( ! [X14 : key1,X15 : a1] : (sP11(X15,X14,sK5,sK3,sK2) | $less(mod1(hash1(X14),sK2),sK6) | tb2t4(some(a,t2tb7(X15))) != tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(X14))) | sK6 != mod1(hash1(X14),sK2)) )),
% 149.30/22.07 inference(definition_unfolding,[],[f286,f322,f322])).
% 149.30/22.07 tff(f437,plain,(
% 149.30/22.07 ( ! [X14 : key1,X15 : a1] : ($less(mod1(hash1(X14),sK2),sK6) | tb2t4(some(a,t2tb7(X15))) = tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(X14))) | ~in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3))) | ~sP11(X15,X14,sK5,sK3,sK2)) )),
% 149.30/22.07 inference(definition_unfolding,[],[f285,f322])).
% 149.30/22.07 tff(f439,plain,(
% 149.30/22.07 ( ! [X0 : $int,X1 : key1] : (~$less(mod1(hash1(X1),X0),0) | ~$less(0,X0)) )),
% 149.30/22.07 inference(definition_unfolding,[],[f326,f322])).
% 149.30/22.07 tff(f454,plain,(
% 149.30/22.07 ( ! [X2 : $int,X10 : list_lpkeycm_a1rp,X7 : map_int_lplist_lpkeycm_a1rprp,X14 : key1,X15 : a1] : (~in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7))) | ~sP11(X15,X14,X10,X7,X2)) )),
% 149.30/22.07 inference(consistent_polarity_flipping,[],[f281])).
% 149.30/22.07 tff(f455,plain,(
% 149.30/22.07 ( ! [X2 : $int,X10 : list_lpkeycm_a1rp,X7 : map_int_lplist_lpkeycm_a1rprp,X14 : key1,X15 : a1] : (mem(tuple2(key,a),tuple21(key,a,t2tb1(X14),t2tb7(X15)),t2tb6(X10)) | sP11(X15,X14,X10,X7,X2) | in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,X2),1),t2tb2(X7)))) )),
% 149.30/22.07 inference(consistent_polarity_flipping,[],[f283])).
% 149.30/22.07 tff(f464,plain,(
% 149.30/22.07 ( ! [X14 : key1,X15 : a1] : (sP11(X15,X14,sK5,sK3,sK2) | $less(mod1(hash1(X14),sK2),sK6) | ~in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3))) | tb2t4(some(a,t2tb7(X15))) = tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(X14)))) )),
% 149.30/22.07 inference(consistent_polarity_flipping,[],[f437])).
% 149.30/22.07 tff(f472,plain,(
% 149.30/22.07 ( ! [X14 : key1,X15 : a1] : (sK6 != mod1(hash1(X14),sK2) | tb2t4(some(a,t2tb7(X15))) != tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(X14))) | $less(mod1(hash1(X14),sK2),sK6) | ~sP11(X15,X14,sK5,sK3,sK2)) )),
% 149.30/22.07 inference(consistent_polarity_flipping,[],[f436])).
% 149.30/22.07 tff(f476,definition,(
% 149.30/22.07 spl14_1 <=> $less(sK6,mod1(hash1(sK9),sK2))),
% 149.30/22.07 introduced(definition,[new_symbols(definition,[spl14_1])],[avatar_definition])).
% 149.30/22.07 tff(f477,plain,(
% 149.30/22.07 $less(sK6,mod1(hash1(sK9),sK2)) | ~spl14_1),
% 149.30/22.07 inference(avatar_component_clause,[],[f476])).
% 149.30/22.07 tff(f480,definition,(
% 149.30/22.07 spl14_2 <=> in_data1(a,sK9,t2tb7(sK10),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3)))),
% 149.30/22.07 introduced(definition,[new_symbols(definition,[spl14_2])],[avatar_definition])).
% 149.30/22.07 tff(f481,plain,(
% 149.30/22.07 ~in_data1(a,sK9,t2tb7(sK10),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3))) | spl14_2),
% 149.30/22.07 inference(avatar_component_clause,[],[f480])).
% 149.30/22.07 tff(f482,plain,(
% 149.30/22.07 in_data1(a,sK9,t2tb7(sK10),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3))) | ~spl14_2),
% 149.30/22.07 inference(avatar_component_clause,[],[f480])).
% 149.30/22.07 tff(f483,plain,(
% 149.30/22.07 ~spl14_1 | spl14_2),
% 149.30/22.07 inference(avatar_split_clause,[],[f422,f480,f476])).
% 149.30/22.07 tff(f485,definition,(
% 149.30/22.07 spl14_3 <=> $less(mod1(hash1(sK9),sK2),0)),
% 149.30/22.07 introduced(definition,[new_symbols(definition,[spl14_3])],[avatar_definition])).
% 149.30/22.07 tff(f486,plain,(
% 149.30/22.07 $less(mod1(hash1(sK9),sK2),0) | ~spl14_3),
% 149.30/22.07 inference(avatar_component_clause,[],[f485])).
% 149.30/22.07 tff(f487,plain,(
% 149.30/22.07 ~$less(mod1(hash1(sK9),sK2),0) | spl14_3),
% 149.30/22.07 inference(avatar_component_clause,[],[f485])).
% 149.30/22.07 tff(f490,definition,(
% 149.30/22.07 spl14_4 <=> good_data1(a,sK9,t2tb7(sK10),t2tb3(sK8),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3)))),
% 149.30/22.07 introduced(definition,[new_symbols(definition,[spl14_4])],[avatar_definition])).
% 149.30/22.07 tff(f492,plain,(
% 149.30/22.07 ~good_data1(a,sK9,t2tb7(sK10),t2tb3(sK8),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3))) | spl14_4),
% 149.30/22.07 inference(avatar_component_clause,[],[f490])).
% 149.30/22.07 tff(f494,plain,(
% 149.30/22.07 spl14_1 | ~spl14_4 | spl14_3),
% 149.30/22.07 inference(avatar_split_clause,[],[f424,f485,f490,f476])).
% 149.30/22.07 tff(f504,definition,(
% 149.30/22.07 spl14_5 <=> sK6 = mod1(hash1(sK9),sK2)),
% 149.30/22.07 introduced(definition,[new_symbols(definition,[spl14_5])],[avatar_definition])).
% 149.30/22.07 tff(f506,plain,(
% 149.30/22.07 sK6 = mod1(hash1(sK9),sK2) | ~spl14_5),
% 149.30/22.07 inference(avatar_component_clause,[],[f504])).
% 149.30/22.07 tff(f508,plain,(
% 149.30/22.07 ( ! [X0 : list_lpkeycm_a1rp] : (mem(tuple2(key,a),tuple21(key,a,t2tb1(sK9),t2tb7(sK10)),t2tb6(X0)) | sP11(sK10,sK9,X0,sK3,sK2)) ) | spl14_2),
% 149.30/22.07 inference(resolution,[],[f481,f455])).
% 149.30/22.07 tff(f512,definition,(
% 149.30/22.07 spl14_6 <=> sP11(sK10,sK9,sK5,sK3,sK2)),
% 149.30/22.07 introduced(definition,[new_symbols(definition,[spl14_6])],[avatar_definition])).
% 149.30/22.07 tff(f514,plain,(
% 149.30/22.07 sP11(sK10,sK9,sK5,sK3,sK2) | ~spl14_6),
% 149.30/22.07 inference(avatar_component_clause,[],[f512])).
% 149.30/22.07 tff(f516,plain,(
% 149.30/22.07 sK6 = mod1(hash1(sK9),sK2) | $less(mod1(hash1(sK9),sK2),sK6) | ~spl14_2),
% 149.30/22.07 inference(resolution,[],[f482,f426])).
% 149.30/22.07 tff(f519,definition,(
% 149.30/22.07 spl14_7 <=> $less(mod1(hash1(sK9),sK2),sK6)),
% 149.30/22.07 introduced(definition,[new_symbols(definition,[spl14_7])],[avatar_definition])).
% 149.30/22.07 tff(f521,plain,(
% 149.30/22.07 $less(mod1(hash1(sK9),sK2),sK6) | ~spl14_7),
% 149.30/22.07 inference(avatar_component_clause,[],[f519])).
% 149.30/22.07 tff(f522,plain,(
% 149.30/22.07 spl14_7 | spl14_5 | ~spl14_2),
% 149.30/22.07 inference(avatar_split_clause,[],[f516,f480,f504,f519])).
% 149.30/22.07 tff(f523,plain,(
% 149.30/22.07 $less(sK6,sK6) | (~spl14_1 | ~spl14_5)),
% 149.30/22.07 inference(superposition,[],[f477,f506])).
% 149.30/22.07 tff(f525,plain,(
% 149.30/22.07 ( ! [X0 : a1] : ($less(sK6,sK6) | sK6 != sK6 | ~sP11(X0,sK9,sK5,sK3,sK2) | tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(sK9))) != tb2t4(some(a,t2tb7(X0)))) ) | ~spl14_5),
% 149.30/22.07 inference(superposition,[],[f472,f506])).
% 149.30/22.07 tff(f533,plain,(
% 149.30/22.07 ( ! [X0 : a1] : (tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(sK9))) != tb2t4(some(a,t2tb7(X0))) | $less(sK6,sK6) | ~sP11(X0,sK9,sK5,sK3,sK2)) ) | ~spl14_5),
% 149.30/22.07 inference(trivial_inequality_removal,[],[f525])).
% 149.30/22.07 tff(f542,plain,(
% 149.30/22.07 $false | (~spl14_1 | ~spl14_5)),
% 149.30/22.07 inference(forward_subsumption_resolution,[],[f523,f134])).
% 149.30/22.07 tff(f543,plain,(
% 149.30/22.07 ~spl14_1 | ~spl14_5),
% 149.30/22.07 inference(avatar_contradiction_clause,[],[f542])).
% 149.30/22.07 tff(f545,definition,(
% 149.30/22.07 spl14_10 <=> ! [X0 : a1] : (tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(sK9))) != tb2t4(some(a,t2tb7(X0))) | ~sP11(X0,sK9,sK5,sK3,sK2))),
% 149.30/22.07 introduced(definition,[new_symbols(definition,[spl14_10])],[avatar_definition])).
% 149.30/22.07 tff(f546,plain,(
% 149.30/22.07 ( ! [X0 : a1] : (tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(sK9))) != tb2t4(some(a,t2tb7(X0))) | ~sP11(X0,sK9,sK5,sK3,sK2)) ) | ~spl14_10),
% 149.30/22.07 inference(avatar_component_clause,[],[f545])).
% 149.30/22.07 tff(f549,plain,(
% 149.30/22.07 ( ! [X0 : a1] : (tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(sK9))) != tb2t4(some(a,t2tb7(X0))) | ~sP11(X0,sK9,sK5,sK3,sK2)) ) | ~spl14_5),
% 149.30/22.07 inference(forward_subsumption_resolution,[],[f533,f134])).
% 149.30/22.07 tff(f552,plain,(
% 149.30/22.07 spl14_10 | ~spl14_5),
% 149.30/22.07 inference(avatar_split_clause,[],[f549,f504,f545])).
% 149.30/22.07 tff(f553,plain,(
% 149.30/22.07 ( ! [X14 : key1,X15 : a1] : (~in_data1(a,X14,t2tb7(X15),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3))) | $less(mod1(hash1(X14),sK2),sK6) | tb2t4(some(a,t2tb7(X15))) = tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(X14)))) )),
% 149.30/22.07 inference(forward_subsumption_resolution,[],[f464,f454])).
% 149.30/22.07 tff(f555,plain,(
% 149.30/22.07 tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(sK9))) = tb2t4(some(a,t2tb7(sK10))) | $less(mod1(hash1(sK9),sK2),sK6) | ~spl14_2),
% 149.30/22.07 inference(resolution,[],[f553,f482])).
% 149.30/22.07 tff(f557,definition,(
% 149.30/22.07 spl14_11 <=> tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(sK9))) = tb2t4(some(a,t2tb7(sK10)))),
% 149.30/22.07 introduced(definition,[new_symbols(definition,[spl14_11])],[avatar_definition])).
% 149.30/22.07 tff(f559,plain,(
% 149.30/22.07 tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(sK9))) = tb2t4(some(a,t2tb7(sK10))) | ~spl14_11),
% 149.30/22.07 inference(avatar_component_clause,[],[f557])).
% 149.30/22.07 tff(f593,plain,(
% 149.30/22.07 nil(tuple2(key,a)) = t2tb6(sK5)),
% 149.30/22.07 inference(superposition,[],[f338,f309])).
% 149.30/22.07 tff(f661,plain,(
% 149.30/22.07 in_data1(a,sK9,t2tb7(sK10),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,sK2)),t2tb2(sK3))) | ~spl14_2),
% 149.30/22.07 inference(superposition,[],[f482,f129])).
% 149.30/22.07 tff(f730,plain,(
% 149.30/22.07 ( ! [X0 : uni] : (~mem(tuple2(key,a),X0,t2tb6(sK5)) | ~sort1(tuple2(key,a),X0)) )),
% 149.30/22.07 inference(superposition,[],[f275,f593])).
% 149.30/22.07 tff(f773,plain,(
% 149.30/22.07 ( ! [X0 : $int] : (~$less(mod1(hash1(sK9),sK2),X0) | $less(sK6,X0)) ) | ~spl14_1),
% 149.30/22.07 inference(resolution,[],[f135,f477])).
% 149.30/22.07 tff(f789,plain,(
% 149.30/22.07 ( ! [X0 : key1,X1 : a1] : ($less(sK6,mod1(hash1(X0),sK2)) | good_data1(a,X0,t2tb7(X1),t2tb3(sK8),mk_array1(list(tuple2(key,a)),$sum($product(2,sK2),1),t2tb2(sK3))) | $less(mod1(hash1(X0),sK2),0) | sK6 = mod1(hash1(X0),sK2)) )),
% 149.30/22.07 inference(resolution,[],[f136,f425])).
% 149.30/22.07 tff(f825,plain,(
% 149.30/22.07 ( ! [X0 : key1,X1 : a1] : (good_data1(a,X0,t2tb7(X1),t2tb3(sK8),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,sK2)),t2tb2(sK3))) | $less(mod1(hash1(X0),sK2),0) | sK6 = mod1(hash1(X0),sK2) | $less(sK6,mod1(hash1(X0),sK2))) )),
% 149.30/22.07 inference(forward_demodulation,[],[f789,f129])).
% 149.30/22.07 tff(f887,plain,(
% 149.30/22.07 ( ! [X0 : uni] : (some(a,X0) = t2tb4(tb2t4(some(a,X0)))) )),
% 149.30/22.07 inference(resolution,[],[f370,f406])).
% 149.30/22.07 tff(f894,plain,(
% 149.30/22.07 ( ! [X2 : uni,X0 : ty,X1 : uni] : (t2tb4(tb2t4(get(option(a),X0,X1,X2))) = get(option(a),X0,X1,X2)) )),
% 149.30/22.07 inference(resolution,[],[f370,f373])).
% 149.30/22.07 tff(f907,plain,(
% 149.30/22.07 ~$less(0,sK2) | ~spl14_3),
% 149.30/22.07 inference(resolution,[],[f439,f486])).
% 149.30/22.07 tff(f912,plain,(
% 149.30/22.07 $false | ~spl14_3),
% 149.30/22.07 inference(forward_subsumption_resolution,[],[f907,f313])).
% 149.30/22.07 tff(f913,plain,(
% 149.30/22.07 ~spl14_3),
% 149.30/22.07 inference(avatar_contradiction_clause,[],[f912])).
% 149.30/22.07 tff(f1406,plain,(
% 149.30/22.07 ~in_data1(a,sK9,t2tb7(sK10),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,sK2)),t2tb2(sK3))) | spl14_2),
% 149.30/22.07 inference(forward_demodulation,[],[f481,f129])).
% 149.30/22.07 tff(f1408,plain,(
% 149.30/22.07 ~good_data1(a,sK9,t2tb7(sK10),t2tb3(sK8),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,sK2)),t2tb2(sK3))) | spl14_4),
% 149.30/22.07 inference(forward_demodulation,[],[f492,f129])).
% 149.30/22.07 tff(f1943,plain,(
% 149.30/22.07 in_data1(a,sK9,t2tb7(sK10),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,sK2)),t2tb2(sK3))) | get(option(a),key,t2tb3(sK8),t2tb1(sK9)) = some(a,t2tb7(sK10)) | spl14_4),
% 149.30/22.07 inference(resolution,[],[f393,f1408])).
% 149.30/22.07 tff(f1946,plain,(
% 149.30/22.07 get(option(a),key,t2tb3(sK8),t2tb1(sK9)) = some(a,t2tb7(sK10)) | (spl14_2 | spl14_4)),
% 149.30/22.07 inference(forward_subsumption_resolution,[],[f1943,f1406])).
% 149.30/22.07 tff(f2300,plain,(
% 149.30/22.07 sP11(sK10,sK9,sK5,sK3,sK2) | ~sort1(tuple2(key,a),tuple21(key,a,t2tb1(sK9),t2tb7(sK10))) | spl14_2),
% 149.30/22.07 inference(resolution,[],[f508,f730])).
% 149.30/22.07 tff(f2302,plain,(
% 149.30/22.07 sP11(sK10,sK9,sK5,sK3,sK2) | spl14_2),
% 149.30/22.07 inference(forward_subsumption_resolution,[],[f2300,f414])).
% 149.30/22.07 tff(f2305,plain,(
% 149.30/22.07 spl14_6 | spl14_2),
% 149.30/22.07 inference(avatar_split_clause,[],[f2302,f480,f512])).
% 149.30/22.07 tff(f2594,plain,(
% 149.30/22.07 $less(sK6,mod1(hash1(sK9),sK2)) | $less(mod1(hash1(sK9),sK2),0) | sK6 = mod1(hash1(sK9),sK2) | spl14_4),
% 149.30/22.07 inference(resolution,[],[f825,f1408])).
% 149.30/22.07 tff(f2621,plain,(
% 149.30/22.07 $less(sK6,sK6) | (~spl14_1 | ~spl14_7)),
% 149.30/22.07 inference(resolution,[],[f773,f521])).
% 149.30/22.07 tff(f2660,plain,(
% 149.30/22.07 $false | (~spl14_1 | ~spl14_7)),
% 149.30/22.07 inference(forward_subsumption_resolution,[],[f2621,f134])).
% 149.30/22.07 tff(f2661,plain,(
% 149.30/22.07 ~spl14_1 | ~spl14_7),
% 149.30/22.07 inference(avatar_contradiction_clause,[],[f2660])).
% 149.30/22.07 tff(f2675,definition,(
% 149.30/22.07 spl14_55 <=> in_data1(a,sK9,t2tb7(sK10),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,sK2)),t2tb2(sK3)))),
% 149.30/22.07 introduced(definition,[new_symbols(definition,[spl14_55])],[avatar_definition])).
% 149.30/22.07 tff(f2677,plain,(
% 149.30/22.07 in_data1(a,sK9,t2tb7(sK10),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,sK2)),t2tb2(sK3))) | ~spl14_55),
% 149.30/22.07 inference(avatar_component_clause,[],[f2675])).
% 149.30/22.07 tff(f2679,definition,(
% 149.30/22.07 spl14_56 <=> get(option(a),key,t2tb3(sK8),t2tb1(sK9)) = some(a,t2tb7(sK10))),
% 149.30/22.07 introduced(definition,[new_symbols(definition,[spl14_56])],[avatar_definition])).
% 149.30/22.07 tff(f2681,plain,(
% 149.30/22.07 get(option(a),key,t2tb3(sK8),t2tb1(sK9)) = some(a,t2tb7(sK10)) | ~spl14_56),
% 149.30/22.07 inference(avatar_component_clause,[],[f2679])).
% 149.30/22.07 tff(f2685,plain,(
% 149.30/22.07 $less(sK6,mod1(hash1(sK9),sK2)) | sK6 = mod1(hash1(sK9),sK2) | (spl14_3 | spl14_4)),
% 149.30/22.07 inference(forward_subsumption_resolution,[],[f2594,f487])).
% 149.30/22.07 tff(f2694,plain,(
% 149.30/22.07 spl14_5 | spl14_1 | spl14_3 | spl14_4),
% 149.30/22.07 inference(avatar_split_clause,[],[f2685,f490,f485,f476,f504])).
% 149.30/22.07 tff(f2760,plain,(
% 149.30/22.07 spl14_56 | spl14_2 | spl14_4),
% 149.30/22.07 inference(avatar_split_clause,[],[f1946,f490,f480,f2679])).
% 149.30/22.07 tff(f2761,plain,(
% 149.30/22.07 ( ! [X0 : uni,X1 : uni] : (good_data1(a,sK9,X0,t2tb3(sK8),X1) | some(a,X0) != some(a,t2tb7(sK10)) | ~in_data1(a,sK9,X0,X1)) ) | ~spl14_56),
% 149.30/22.07 inference(superposition,[],[f394,f2681])).
% 149.30/22.07 tff(f3200,definition,(
% 149.30/22.07 spl14_70 <=> ! [X0 : a1] : (tb2t4(some(a,t2tb7(X0))) != tb2t4(some(a,t2tb7(sK10))) | ~sP11(X0,sK9,sK5,sK3,sK2))),
% 149.30/22.07 introduced(definition,[new_symbols(definition,[spl14_70])],[avatar_definition])).
% 149.30/22.07 tff(f3201,plain,(
% 149.30/22.07 ( ! [X0 : a1] : (~sP11(X0,sK9,sK5,sK3,sK2) | tb2t4(some(a,t2tb7(X0))) != tb2t4(some(a,t2tb7(sK10)))) ) | ~spl14_70),
% 149.30/22.07 inference(avatar_component_clause,[],[f3200])).
% 149.30/22.07 tff(f44279,plain,(
% 149.30/22.07 tb2t4(some(a,t2tb7(sK10))) != tb2t4(some(a,t2tb7(sK10))) | (~spl14_6 | ~spl14_70)),
% 149.30/22.07 inference(resolution,[],[f3201,f514])).
% 149.30/22.07 tff(f44280,plain,(
% 149.30/22.07 $false | (~spl14_6 | ~spl14_70)),
% 149.30/22.07 inference(trivial_inequality_removal,[],[f44279])).
% 149.30/22.07 tff(f44281,plain,(
% 149.30/22.07 ~spl14_6 | ~spl14_70),
% 149.30/22.07 inference(avatar_contradiction_clause,[],[f44280])).
% 149.30/22.07 tff(f52671,plain,(
% 149.30/22.07 ( ! [X0 : a1] : (~sP11(X0,sK9,sK5,sK3,sK2) | tb2t4(some(a,t2tb7(X0))) != tb2t4(some(a,t2tb7(sK10)))) ) | (~spl14_10 | ~spl14_56)),
% 149.30/22.07 inference(forward_demodulation,[],[f546,f2681])).
% 149.30/22.07 tff(f52672,plain,(
% 149.30/22.07 spl14_70 | ~spl14_10 | ~spl14_56),
% 149.30/22.07 inference(avatar_split_clause,[],[f52671,f2679,f545,f3200])).
% 149.30/22.07 tff(f52673,plain,(
% 149.30/22.07 spl14_55 | ~spl14_2),
% 149.30/22.07 inference(avatar_split_clause,[],[f661,f480,f2675])).
% 149.30/22.07 tff(f52677,plain,(
% 149.30/22.07 tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(sK9))) = tb2t4(some(a,t2tb7(sK10))) | $less(sK6,sK6) | (~spl14_2 | ~spl14_5)),
% 149.30/22.07 inference(forward_demodulation,[],[f555,f506])).
% 149.30/22.07 tff(f52680,plain,(
% 149.30/22.07 tb2t4(get(option(a),key,t2tb3(sK8),t2tb1(sK9))) = tb2t4(some(a,t2tb7(sK10))) | (~spl14_2 | ~spl14_5)),
% 149.30/22.07 inference(forward_subsumption_resolution,[],[f52677,f134])).
% 149.30/22.07 tff(f52681,plain,(
% 149.30/22.07 spl14_11 | ~spl14_2 | ~spl14_5),
% 149.30/22.07 inference(avatar_split_clause,[],[f52680,f504,f480,f557])).
% 149.30/22.07 tff(f52684,plain,(
% 149.30/22.07 get(option(a),key,t2tb3(sK8),t2tb1(sK9)) = t2tb4(tb2t4(some(a,t2tb7(sK10)))) | ~spl14_11),
% 149.30/22.07 inference(superposition,[],[f894,f559])).
% 149.30/22.07 tff(f52685,plain,(
% 149.30/22.07 get(option(a),key,t2tb3(sK8),t2tb1(sK9)) = some(a,t2tb7(sK10)) | ~spl14_11),
% 149.30/22.07 inference(forward_demodulation,[],[f52684,f887])).
% 149.30/22.07 tff(f52688,plain,(
% 149.30/22.07 spl14_56 | ~spl14_11),
% 149.30/22.07 inference(avatar_split_clause,[],[f52685,f557,f2679])).
% 149.30/22.07 tff(f52719,plain,(
% 149.30/22.07 some(a,t2tb7(sK10)) != some(a,t2tb7(sK10)) | ~in_data1(a,sK9,t2tb7(sK10),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,sK2)),t2tb2(sK3))) | (spl14_4 | ~spl14_56)),
% 149.30/22.07 inference(resolution,[],[f2761,f1408])).
% 149.30/22.07 tff(f52722,plain,(
% 149.30/22.07 ~in_data1(a,sK9,t2tb7(sK10),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,sK2)),t2tb2(sK3))) | (spl14_4 | ~spl14_56)),
% 149.30/22.07 inference(trivial_inequality_removal,[],[f52719])).
% 149.30/22.07 tff(f52724,plain,(
% 149.30/22.07 $false | (spl14_4 | ~spl14_55 | ~spl14_56)),
% 149.30/22.07 inference(forward_subsumption_resolution,[],[f52722,f2677])).
% 149.30/22.07 tff(f52725,plain,(
% 149.30/22.07 spl14_4 | ~spl14_55 | ~spl14_56),
% 149.30/22.07 inference(avatar_contradiction_clause,[],[f52724])).
% 149.30/22.07 cnf(s1, plain, ~spl14_1 | spl14_2, inference(sat_conversion,[],[f483])).
% 149.30/22.07 cnf(s4, plain, spl14_1 | spl14_3 | ~spl14_4, inference(sat_conversion,[],[f494])).
% 149.30/22.07 cnf(s7, plain, ~spl14_2 | spl14_5 | spl14_7, inference(sat_conversion,[],[f522])).
% 149.30/22.07 cnf(s9, plain, ~spl14_1 | ~spl14_5, inference(sat_conversion,[],[f543])).
% 149.30/22.07 cnf(s13, plain, ~spl14_5 | spl14_10, inference(sat_conversion,[],[f552])).
% 149.30/22.07 cnf(s26, plain, ~spl14_3, inference(sat_conversion,[],[f913])).
% 149.30/22.07 cnf(s71, plain, spl14_2 | spl14_6, inference(sat_conversion,[],[f2305])).
% 149.30/22.07 cnf(s86, plain, ~spl14_1 | ~spl14_7, inference(sat_conversion,[],[f2661])).
% 149.30/22.07 cnf(s103, plain, spl14_1 | spl14_3 | spl14_4 | spl14_5, inference(sat_conversion,[],[f2694])).
% 149.30/22.07 cnf(s111, plain, spl14_2 | spl14_4 | spl14_56, inference(sat_conversion,[],[f2760])).
% 149.30/22.07 cnf(s1695, plain, ~spl14_6 | ~spl14_70, inference(sat_conversion,[],[f44281])).
% 149.30/22.07 cnf(s2154, plain, ~spl14_10 | ~spl14_56 | spl14_70, inference(sat_conversion,[],[f52672])).
% 149.30/22.07 cnf(s2155, plain, ~spl14_2 | spl14_55, inference(sat_conversion,[],[f52673])).
% 149.30/22.07 cnf(s2163, plain, ~spl14_2 | ~spl14_5 | spl14_11, inference(sat_conversion,[],[f52681])).
% 149.30/22.07 cnf(s2165, plain, ~spl14_11 | spl14_56, inference(sat_conversion,[],[f52688])).
% 149.30/22.07 cnf(s2167, plain, spl14_4 | ~spl14_55 | ~spl14_56, inference(sat_conversion,[],[f52725])).
% 149.30/22.07 cnf(s2229, plain, spl14_1 | ~spl14_4, inference(rat,[],[s4,s26])).
% 149.30/22.07 cnf(s2230, plain, spl14_2 | spl14_1, inference(rat,[],[s1695,s2154,s71,s111,s13,s103,s2229,s26])).
% 149.30/22.07 cnf(s2231, plain, spl14_4 | spl14_1, inference(rat,[],[s2167,s2165,s2155,s2163,s2230,s103,s26])).
% 149.30/22.07 cnf(s2232, plain, spl14_1, inference(rat,[],[s2231,s2229])).
% 149.30/22.07 cnf(s2233, plain, ~spl14_7, inference(rat,[],[s86,s2232])).
% 149.30/22.07 cnf(s2234, plain, ~spl14_5, inference(rat,[],[s9,s2232])).
% 149.30/22.07 cnf(s2235, plain, spl14_2, inference(rat,[],[s1,s2232])).
% 149.30/22.07 cnf(s2236, plain, $false, inference(rat,[],[s7,s2234,s2233,s2235])).
% 149.30/22.07 tff(f52726,plain,(
% 149.30/22.07 $false),
% 149.30/22.07 inference(avatar_sat_refutation,[],[s2236])).
% 149.30/22.07 % SZS output end Proof for theBenchmark
% 149.30/22.07 % (3414395)------------------------------
% 149.30/22.07 % (3414395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.30/22.07 % (3414395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.30/22.07 % (3414395)CaDiCaL version: 2.1.3
% 149.30/22.07 % (3414395)Termination reason: Refutation
% 149.30/22.07 % (3414395)Time elapsed: 1.830 s
% 149.30/22.07 % (3414395)Peak memory usage: 32 MB
% 149.30/22.07 % (3414395)Instructions burned: 2958 (million)
% 149.30/22.07 % (3413807)Success in time 21.84 s
% 149.30/22.07 % Vampire exiting
%------------------------------------------------------------------------------