%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX122_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n006.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:46:31 PM UTC 2026 % Result : Timeout 300.43s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX122_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.23 % Computer : n006.cluster.edu % 0.10/0.23 % Model : x86_64 x86_64 % 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.23 % Memory : 8046.5625MB % 0.10/0.23 % OS : Linux 6.8.0-71-generic % 0.10/0.23 % CPULimit : 300 % 0.10/0.24 % WCLimit : 300 % 0.10/0.24 % DateTime : Mon Sep 28 15:02:10 UTC 2026 % 0.10/0.24 % CPUTime : % 0.10/0.24 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.24/0.28 Running first-order model finding % 0.24/0.28 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 5.48/1.13 % (4033055)Will run a generic schedule for satisfiability detection. % 5.48/1.13 % (4033060)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1029746844_2999 on theBenchmark for (2999ds/0Mi) % 5.48/1.13 % (4033062)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1688109458:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 5.48/1.13 % (4033060)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.48/1.13 % (4033060)Terminated due to inappropriate strategy. % 5.48/1.13 % (4033060)------------------------------ % 5.48/1.13 % (4033060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.48/1.13 % (4033060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.48/1.13 % (4033060)CaDiCaL version: 2.1.3 % 5.48/1.13 % (4033060)Termination reason: Inappropriate % 5.48/1.13 % (4033060)Time elapsed: 0.007 s % 5.48/1.13 % (4033060)Peak memory usage: 10 MB % 5.48/1.13 % (4033060)Instructions burned: 16 (million) % 5.48/1.13 % (4033061)% WARNING: option uhcvi not known. % 5.48/1.13 % (4033060)------------------------------ % 5.48/1.13 % (4033060)------------------------------ % 5.48/1.13 % (4033061)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2188735704:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 5.48/1.13 % (4033063)dis+10_1_sil=32000:sp=arity:random_seed=3871429597:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 5.48/1.13 % (4033064)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3548054639:i=116_2999 on theBenchmark for (2999ds/116Mi) % 5.48/1.13 % (4033065)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3365847262:i=131_2999 on theBenchmark for (2999ds/131Mi) % 5.48/1.13 % (4033066)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3971475508:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 5.48/1.13 % (4033069)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=629030108:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 5.48/1.13 % (4033069)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.48/1.13 % (4033069)Terminated due to inappropriate strategy. % 5.48/1.13 % (4033069)------------------------------ % 5.48/1.13 % (4033069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.48/1.13 % (4033069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.48/1.13 % (4033069)CaDiCaL version: 2.1.3 % 5.48/1.13 % (4033069)Termination reason: Inappropriate % 5.48/1.13 % (4033069)Time elapsed: 0.014 s % 5.48/1.13 % (4033069)Peak memory usage: 11 MB % 5.48/1.13 % (4033069)Instructions burned: 16 (million) % 5.48/1.13 % (4033069)------------------------------ % 5.48/1.13 % (4033069)------------------------------ % 5.48/1.13 % (4033076)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3876924122:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 5.48/1.13 % (4033063)Instruction limit reached! % 5.48/1.13 % (4033063)------------------------------ % 5.48/1.13 % (4033063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.48/1.13 % (4033063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.48/1.13 % (4033063)CaDiCaL version: 2.1.3 % 5.48/1.13 % (4033063)Termination reason: Instruction limit % 5.48/1.13 % (4033063)Termination phase: Saturation % 5.48/1.13 % (4033063)Time elapsed: 0.080 s % 5.48/1.13 % (4033063)Peak memory usage: 12 MB % 5.48/1.13 % (4033063)Instructions burned: 103 (million) % 5.48/1.13 % (4033064)Instruction limit reached! % 5.48/1.13 % (4033064)------------------------------ % 5.48/1.13 % (4033064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.48/1.13 % (4033064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.48/1.13 % (4033064)CaDiCaL version: 2.1.3 % 5.48/1.13 % (4033064)Termination reason: Instruction limit % 5.48/1.13 % (4033064)Termination phase: Saturation % 5.48/1.13 % (4033064)Time elapsed: 0.091 s % 5.48/1.13 % (4033064)Peak memory usage: 13 MB % 5.48/1.13 % (4033064)Instructions burned: 120 (million) % 5.48/1.13 % (4033065)Instruction limit reached! % 5.48/1.13 % (4033065)------------------------------ % 5.48/1.13 % (4033065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.48/1.13 % (4033065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.48/1.13 % (4033065)CaDiCaL version: 2.1.3 % 5.48/1.13 % (4033065)Termination reason: Instruction limit % 7.23/1.42 % (4033065)Termination phase: Saturation % 7.23/1.42 % (4033065)Time elapsed: 0.101 s % 7.23/1.42 % (4033065)Peak memory usage: 13 MB % 7.23/1.42 % (4033065)Instructions burned: 131 (million) % 7.23/1.42 % (4033078)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=1700340352:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.23/1.42 % (4033079)ott-21_1_sil=16000:fs=off:random_seed=2153819579:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.23/1.42 % (4033080)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=983396282:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.23/1.42 % (4033066)Instruction limit reached! % 7.23/1.42 % (4033066)------------------------------ % 7.23/1.42 % (4033066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.23/1.42 % (4033066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.23/1.42 % (4033066)CaDiCaL version: 2.1.3 % 7.23/1.42 % (4033066)Termination reason: Instruction limit % 7.23/1.42 % (4033066)Termination phase: Saturation % 7.23/1.42 % (4033066)Time elapsed: 0.136 s % 7.23/1.42 % (4033066)Peak memory usage: 13 MB % 7.23/1.42 % (4033066)Instructions burned: 159 (million) % 7.23/1.42 % (4033076)Instruction limit reached! % 7.23/1.42 % (4033076)------------------------------ % 7.23/1.42 % (4033076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.23/1.42 % (4033076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.23/1.42 % (4033076)CaDiCaL version: 2.1.3 % 7.23/1.42 % (4033076)Termination reason: Instruction limit % 7.23/1.42 % (4033076)Termination phase: Saturation % 7.23/1.42 % (4033076)Time elapsed: 0.084 s % 7.23/1.42 % (4033076)Peak memory usage: 13 MB % 7.23/1.42 % (4033076)Instructions burned: 131 (million) % 7.23/1.42 % (4033084)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1549240165:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.23/1.42 % (4033084)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.23/1.42 % (4033084)Terminated due to inappropriate strategy. % 7.23/1.42 % (4033084)------------------------------ % 7.23/1.42 % (4033084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.23/1.42 % (4033084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.23/1.42 % (4033084)CaDiCaL version: 2.1.3 % 7.23/1.42 % (4033084)Termination reason: Inappropriate % 7.23/1.42 % (4033084)Time elapsed: 0.011 s % 7.23/1.42 % (4033084)Peak memory usage: 10 MB % 7.23/1.42 % (4033084)Instructions burned: 12 (million) % 7.23/1.42 % (4033085)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3920325312:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.23/1.42 % (4033084)------------------------------ % 7.23/1.42 % (4033084)------------------------------ % 7.23/1.42 % (4033088)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2581148476:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 7.23/1.42 % (4033088)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.23/1.42 % (4033088)Terminated due to inappropriate strategy. % 7.23/1.42 % (4033088)------------------------------ % 7.23/1.42 % (4033088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.23/1.42 % (4033088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.23/1.42 % (4033088)CaDiCaL version: 2.1.3 % 7.23/1.42 % (4033088)Termination reason: Inappropriate % 7.23/1.42 % (4033088)Time elapsed: 0.013 s % 7.23/1.42 % (4033088)Peak memory usage: 10 MB % 7.23/1.42 % (4033088)Instructions burned: 12 (million) % 7.23/1.42 % (4033088)------------------------------ % 7.23/1.42 % (4033088)------------------------------ % 7.23/1.42 % (4033079)Instruction limit reached! % 7.23/1.42 % (4033079)------------------------------ % 7.23/1.42 % (4033079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.23/1.42 % (4033079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.23/1.42 % (4033079)CaDiCaL version: 2.1.3 % 7.23/1.42 % (4033079)Termination reason: Instruction limit % 7.23/1.42 % (4033079)Termination phase: Saturation % 7.23/1.42 % (4033079)Time elapsed: 0.134 s % 7.23/1.42 % (4033079)Peak memory usage: 12 MB % 7.23/1.42 % (4033079)Instructions burned: 181 (million) % 7.23/1.42 % (4033090)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=2913371332:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 30.66/4.83 % (4033091)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=570323703:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 30.66/4.83 % (4033080)Instruction limit reached! % 30.66/4.83 % (4033080)------------------------------ % 30.66/4.83 % (4033080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.66/4.83 % (4033080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.66/4.83 % (4033080)CaDiCaL version: 2.1.3 % 30.66/4.83 % (4033080)Termination reason: Instruction limit % 30.66/4.83 % (4033080)Termination phase: Saturation % 30.66/4.83 % (4033080)Time elapsed: 0.361 s % 30.66/4.83 % (4033080)Peak memory usage: 13 MB % 30.66/4.83 % (4033080)Instructions burned: 477 (million) % 30.66/4.83 % (4033094)fmb+10_1_sil=64000:random_seed=1095740806:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 30.66/4.83 % (4033094)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.66/4.83 % (4033094)Terminated due to inappropriate strategy. % 30.66/4.83 % (4033094)------------------------------ % 30.66/4.83 % (4033094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.66/4.83 % (4033094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.66/4.83 % (4033094)CaDiCaL version: 2.1.3 % 30.66/4.83 % (4033094)Termination reason: Inappropriate % 30.66/4.83 % (4033094)Time elapsed: 0.009 s % 30.66/4.83 % (4033094)Peak memory usage: 11 MB % 30.66/4.83 % (4033094)Instructions burned: 16 (million) % 30.66/4.83 % (4033094)------------------------------ % 30.66/4.83 % (4033094)------------------------------ % 30.66/4.83 % (4033096)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=405955218:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 30.66/4.83 % (4033096)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.66/4.83 % (4033096)Terminated due to inappropriate strategy. % 30.66/4.83 % (4033096)------------------------------ % 30.66/4.83 % (4033096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.66/4.83 % (4033096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.66/4.83 % (4033096)CaDiCaL version: 2.1.3 % 30.66/4.83 % (4033096)Termination reason: Inappropriate % 30.66/4.83 % (4033096)Time elapsed: 0.011 s % 30.66/4.83 % (4033096)Peak memory usage: 11 MB % 30.66/4.83 % (4033096)Instructions burned: 16 (million) % 30.66/4.83 % (4033096)------------------------------ % 30.66/4.83 % (4033096)------------------------------ % 30.66/4.83 % (4033098)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1582549588:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 30.66/4.83 % (4033098)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.66/4.83 % (4033098)Terminated due to inappropriate strategy. % 30.66/4.83 % (4033098)------------------------------ % 30.66/4.83 % (4033098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.66/4.83 % (4033098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.66/4.83 % (4033098)CaDiCaL version: 2.1.3 % 30.66/4.83 % (4033098)Termination reason: Inappropriate % 30.66/4.83 % (4033098)Time elapsed: 0.008 s % 30.66/4.83 % (4033098)Peak memory usage: 11 MB % 30.66/4.83 % (4033098)Instructions burned: 16 (million) % 30.66/4.83 % (4033098)------------------------------ % 30.66/4.83 % (4033098)------------------------------ % 30.66/4.83 % (4033100)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3148208777:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 30.66/4.83 % (4033078)Instruction limit reached! % 30.66/4.83 % (4033078)------------------------------ % 30.66/4.83 % (4033078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.66/4.83 % (4033078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.66/4.83 % (4033078)CaDiCaL version: 2.1.3 % 30.66/4.83 % (4033078)Termination reason: Instruction limit % 30.66/4.83 % (4033078)Termination phase: Saturation % 30.66/4.83 % (4033078)Time elapsed: 0.556 s % 30.66/4.83 % (4033078)Peak memory usage: 15 MB % 30.66/4.83 % (4033078)Instructions burned: 685 (million) % 30.66/4.83 % (4033102)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=140143281:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 30.66/4.83 % (4033090)Instruction limit reached! % 30.66/4.83 % (4033090)------------------------------ % 31.12/5.04 % (4033090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.12/5.04 % (4033090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.12/5.04 % (4033090)CaDiCaL version: 2.1.3 % 31.12/5.04 % (4033090)Termination reason: Instruction limit % 31.12/5.04 % (4033090)Termination phase: Saturation % 31.12/5.04 % (4033090)Time elapsed: 0.526 s % 31.12/5.04 % (4033090)Peak memory usage: 14 MB % 31.12/5.04 % (4033090)Instructions burned: 694 (million) % 31.12/5.04 % (4033104)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1306691126:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 31.12/5.04 % (4033104)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.12/5.04 % (4033104)Terminated due to inappropriate strategy. % 31.12/5.04 % (4033104)------------------------------ % 31.12/5.04 % (4033104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.12/5.04 % (4033104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.12/5.04 % (4033104)CaDiCaL version: 2.1.3 % 31.12/5.04 % (4033104)Termination reason: Inappropriate % 31.12/5.04 % (4033104)Time elapsed: 0.009 s % 31.12/5.04 % (4033104)Peak memory usage: 11 MB % 31.12/5.04 % (4033104)Instructions burned: 16 (million) % 31.12/5.04 % (4033104)------------------------------ % 31.12/5.04 % (4033104)------------------------------ % 31.12/5.04 % (4033106)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2131473196:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi) % 31.12/5.04 % (4033106)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.12/5.04 % (4033106)Terminated due to inappropriate strategy. % 31.12/5.04 % (4033106)------------------------------ % 31.12/5.04 % (4033106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.12/5.04 % (4033106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.12/5.04 % (4033106)CaDiCaL version: 2.1.3 % 31.12/5.04 % (4033106)Termination reason: Inappropriate % 31.12/5.04 % (4033106)Time elapsed: 0.014 s % 31.12/5.04 % (4033106)Peak memory usage: 10 MB % 31.12/5.04 % (4033106)Instructions burned: 16 (million) % 31.12/5.04 % (4033106)------------------------------ % 31.12/5.04 % (4033106)------------------------------ % 31.12/5.04 % (4033108)ott-2_1_sil=16000:newcnf=on:random_seed=2082177733:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 31.12/5.04 % (4033091)Instruction limit reached! % 31.12/5.04 % (4033091)------------------------------ % 31.12/5.04 % (4033091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.12/5.04 % (4033091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.12/5.04 % (4033091)CaDiCaL version: 2.1.3 % 31.12/5.04 % (4033091)Termination reason: Instruction limit % 31.12/5.04 % (4033091)Termination phase: Saturation % 31.12/5.04 % (4033091)Time elapsed: 0.658 s % 31.12/5.04 % (4033091)Peak memory usage: 14 MB % 31.12/5.04 % (4033091)Instructions burned: 880 (million) % 31.12/5.04 % (4033110)ott+10_1_sil=32000:tgt=ground:random_seed=3622836209:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi) % 31.12/5.04 % (4033085)Instruction limit reached! % 31.12/5.04 % (4033085)------------------------------ % 31.12/5.04 % (4033085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.12/5.04 % (4033085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.12/5.04 % (4033085)CaDiCaL version: 2.1.3 % 31.12/5.04 % (4033085)Termination reason: Instruction limit % 31.12/5.04 % (4033085)Termination phase: Saturation % 31.12/5.04 % (4033085)Time elapsed: 0.847 s % 31.12/5.04 % (4033085)Peak memory usage: 13 MB % 31.12/5.04 % (4033085)Instructions burned: 1179 (million) % 31.12/5.04 % (4033112)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=473072185:i=54282_2989 on theBenchmark for (2989ds/54282Mi) % 31.12/5.04 % (4033112)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.12/5.04 % (4033112)Terminated due to inappropriate strategy. % 31.12/5.04 % (4033112)------------------------------ % 31.12/5.04 % (4033112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.12/5.04 % (4033112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.12/5.04 % (4033112)CaDiCaL version: 2.1.3 % 31.12/5.04 % (4033112)Termination reason: Inappropriate % 31.12/5.04 % (4033112)Time elapsed: 0.014 s % 31.12/5.04 % (4033112)Peak memory usage: 10 MB % 31.12/5.04 % (4033112)Instructions burned: 16 (million) % 125.15/17.93 % (4033112)------------------------------ % 125.15/17.93 % (4033112)------------------------------ % 125.15/17.93 % (4033114)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4188869714:i=3512:aac=none_2988 on theBenchmark for (2988ds/3512Mi) % 125.15/17.93 % (4033108)Instruction limit reached! % 125.15/17.93 % (4033108)------------------------------ % 125.15/17.93 % (4033108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.15/17.93 % (4033108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.15/17.93 % (4033108)CaDiCaL version: 2.1.3 % 125.15/17.93 % (4033108)Termination reason: Instruction limit % 125.15/17.93 % (4033108)Termination phase: Saturation % 125.15/17.93 % (4033108)Time elapsed: 0.782 s % 125.15/17.93 % (4033108)Peak memory usage: 18 MB % 125.15/17.93 % (4033108)Instructions burned: 870 (million) % 125.15/17.93 % (4033116)dis+21_1_sil=32000:sas=cadical:random_seed=2111216829:i=3773:amm=off_2982 on theBenchmark for (2982ds/3773Mi) % 125.15/17.93 % (4033102)Instruction limit reached! % 125.15/17.93 % (4033102)------------------------------ % 125.15/17.93 % (4033102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.15/17.93 % (4033102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.15/17.93 % (4033102)CaDiCaL version: 2.1.3 % 125.15/17.93 % (4033102)Termination reason: Instruction limit % 125.15/17.93 % (4033102)Termination phase: Saturation % 125.15/17.93 % (4033102)Time elapsed: 1.394 s % 125.15/17.93 % (4033102)Peak memory usage: 23 MB % 125.15/17.93 % (4033102)Instructions burned: 1473 (million) % 125.15/17.93 % (4033118)ott+11_1_sil=16000:gs=on:random_seed=651834953:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 125.15/17.93 % (4033114)Instruction limit reached! % 125.15/17.93 % (4033114)------------------------------ % 125.15/17.93 % (4033114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.15/17.93 % (4033114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.15/17.93 % (4033114)CaDiCaL version: 2.1.3 % 125.15/17.93 % (4033114)Termination reason: Instruction limit % 125.15/17.93 % (4033114)Termination phase: Saturation % 125.15/17.93 % (4033114)Time elapsed: 2.591 s % 125.15/17.93 % (4033114)Peak memory usage: 17 MB % 125.15/17.93 % (4033114)Instructions burned: 3512 (million) % 125.15/17.93 % (4033120)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4242758016:fmbsr=1.6:i=67534_2962 on theBenchmark for (2962ds/67534Mi) % 125.15/17.93 % (4033120)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 125.15/17.93 % (4033120)Terminated due to inappropriate strategy. % 125.15/17.93 % (4033120)------------------------------ % 125.15/17.93 % (4033120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.15/17.93 % (4033120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.15/17.93 % (4033120)CaDiCaL version: 2.1.3 % 125.15/17.93 % (4033120)Termination reason: Inappropriate % 125.15/17.93 % (4033120)Time elapsed: 0.014 s % 125.15/17.93 % (4033120)Peak memory usage: 10 MB % 125.15/17.93 % (4033120)Instructions burned: 16 (million) % 125.15/17.93 % (4033120)------------------------------ % 125.15/17.93 % (4033120)------------------------------ % 125.15/17.93 % (4033122)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2811664920:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2962 on theBenchmark for (2962ds/4591Mi) % 125.15/17.93 % (4033118)Instruction limit reached! % 125.15/17.93 % (4033118)------------------------------ % 125.15/17.93 % (4033118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.15/17.93 % (4033118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.15/17.93 % (4033118)CaDiCaL version: 2.1.3 % 125.15/17.93 % (4033118)Termination reason: Instruction limit % 125.15/17.93 % (4033118)Termination phase: Saturation % 125.15/17.93 % (4033118)Time elapsed: 1.630 s % 125.15/17.93 % (4033118)Peak memory usage: 13 MB % 125.15/17.93 % (4033118)Instructions burned: 2252 (million) % 125.15/17.93 % (4033125)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2404539088:i=29340_2961 on theBenchmark for (2961ds/29340Mi) % 125.15/17.93 % (4033116)Instruction limit reached! % 125.15/17.93 % (4033116)------------------------------ % 125.15/17.93 % (4033116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.15/17.93 % (4033116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.15/17.93 % (4033116)CaDiCaL version: 2.1.3 % 125.15/17.93 % (4033116)Termination reason: Instruction limit % 141.02/20.18 % (4033116)Termination phase: Saturation % 141.02/20.18 % (4033116)Time elapsed: 2.757 s % 141.02/20.18 % (4033116)Peak memory usage: 16 MB % 141.02/20.18 % (4033116)Instructions burned: 3774 (million) % 141.02/20.18 % (4033100)Instruction limit reached! % 141.02/20.18 % (4033100)------------------------------ % 141.02/20.18 % (4033100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.02/20.18 % (4033100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.02/20.18 % (4033100)CaDiCaL version: 2.1.3 % 141.02/20.18 % (4033100)Termination reason: Instruction limit % 141.02/20.18 % (4033100)Termination phase: Saturation % 141.02/20.18 % (4033100)Time elapsed: 3.867 s % 141.02/20.18 % (4033100)Peak memory usage: 18 MB % 141.02/20.18 % (4033100)Instructions burned: 5131 (million) % 141.02/20.18 % (4033130)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=721078265:i=5211_2954 on theBenchmark for (2954ds/5211Mi) % 141.02/20.18 % (4033131)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=429128829:i=5497:nm=2_2954 on theBenchmark for (2954ds/5497Mi) % 141.02/20.18 % (4033131)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.02/20.18 % (4033131)Terminated due to inappropriate strategy. % 141.02/20.18 % (4033131)------------------------------ % 141.02/20.18 % (4033131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.02/20.18 % (4033131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.02/20.18 % (4033131)CaDiCaL version: 2.1.3 % 141.02/20.18 % (4033131)Termination reason: Inappropriate % 141.02/20.18 % (4033131)Time elapsed: 0.014 s % 141.02/20.18 % (4033131)Peak memory usage: 10 MB % 141.02/20.18 % (4033131)Instructions burned: 16 (million) % 141.02/20.18 % (4033131)------------------------------ % 141.02/20.18 % (4033131)------------------------------ % 141.02/20.18 % (4033134)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2564771610:fmbsr=2:i=46332_2953 on theBenchmark for (2953ds/46332Mi) % 141.02/20.18 % (4033134)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.02/20.18 % (4033134)Terminated due to inappropriate strategy. % 141.02/20.18 % (4033134)------------------------------ % 141.02/20.18 % (4033134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.02/20.18 % (4033134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.02/20.18 % (4033134)CaDiCaL version: 2.1.3 % 141.02/20.18 % (4033134)Termination reason: Inappropriate % 141.02/20.18 % (4033134)Time elapsed: 0.014 s % 141.02/20.18 % (4033134)Peak memory usage: 10 MB % 141.02/20.18 % (4033134)Instructions burned: 16 (million) % 141.02/20.18 % (4033134)------------------------------ % 141.02/20.18 % (4033134)------------------------------ % 141.02/20.18 % (4033110)Instruction limit reached! % 141.02/20.18 % (4033110)------------------------------ % 141.02/20.18 % (4033110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.02/20.18 % (4033110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.02/20.18 % (4033110)CaDiCaL version: 2.1.3 % 141.02/20.18 % (4033110)Termination reason: Instruction limit % 141.02/20.18 % (4033110)Termination phase: Saturation % 141.02/20.18 % (4033110)Time elapsed: 3.674 s % 141.02/20.18 % (4033110)Peak memory usage: 14 MB % 141.02/20.18 % (4033110)Instructions burned: 5115 (million) % 141.02/20.18 % (4033136)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3630056009:i=14071_2953 on theBenchmark for (2953ds/14071Mi) % 141.02/20.18 % (4033136)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 141.02/20.18 % (4033136)Terminated due to inappropriate strategy. % 141.02/20.18 % (4033136)------------------------------ % 141.02/20.18 % (4033136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 141.02/20.18 % (4033136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.02/20.18 % (4033136)CaDiCaL version: 2.1.3 % 141.02/20.18 % (4033136)Termination reason: Inappropriate % 141.02/20.18 % (4033136)Time elapsed: 0.014 s % 141.02/20.18 % (4033136)Peak memory usage: 10 MB % 141.02/20.18 % (4033136)Instructions burned: 16 (million) % 141.02/20.18 % (4033136)------------------------------ % 141.02/20.18 % (4033136)------------------------------ % 141.02/20.18 % (4033138)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2158387772:i=22565:add=on:rawr=on_2953 on theBenchmark for (2953ds/22565Mi) % 141.02/20.18 % (4033139)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4084946470:i=8173:av=off_2952 on theBenchmark for (2952ds/8173Mi) % 142.19/20.32 % (4033130)Instruction limit reached! % 142.19/20.32 % (4033130)------------------------------ % 142.19/20.32 % (4033130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.19/20.32 % (4033130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.19/20.32 % (4033130)CaDiCaL version: 2.1.3 % 142.19/20.32 % (4033130)Termination reason: Instruction limit % 142.19/20.32 % (4033130)Termination phase: Saturation % 142.19/20.32 % (4033130)Time elapsed: 3.809 s % 142.19/20.32 % (4033130)Peak memory usage: 22 MB % 142.19/20.32 % (4033130)Instructions burned: 5211 (million) % 142.19/20.32 % (4033152)dis+10_16:1_sil=16000:random_seed=1217156066:i=9155:fsr=off_2916 on theBenchmark for (2916ds/9155Mi) % 142.19/20.32 % (4033122)Instruction limit reached! % 142.19/20.32 % (4033122)------------------------------ % 142.19/20.32 % (4033122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.19/20.32 % (4033122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.19/20.32 % (4033122)CaDiCaL version: 2.1.3 % 142.19/20.32 % (4033122)Termination reason: Instruction limit % 142.19/20.32 % (4033122)Termination phase: Saturation % 142.19/20.32 % (4033122)Time elapsed: 4.666 s % 142.19/20.32 % (4033122)Peak memory usage: 44 MB % 142.19/20.32 % (4033122)Instructions burned: 4591 (million) % 142.19/20.32 % (4033154)ott-3_8_sil=64000:random_seed=685149419:i=20139:bs=on_2915 on theBenchmark for (2915ds/20139Mi) % 142.19/20.32 % (4033139)Instruction limit reached! % 142.19/20.32 % (4033139)------------------------------ % 142.19/20.32 % (4033139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.19/20.32 % (4033139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.19/20.32 % (4033139)CaDiCaL version: 2.1.3 % 142.19/20.32 % (4033139)Termination reason: Instruction limit % 142.19/20.32 % (4033139)Termination phase: Saturation % 142.19/20.32 % (4033139)Time elapsed: 6.041 s % 142.19/20.32 % (4033139)Peak memory usage: 15 MB % 142.19/20.32 % (4033139)Instructions burned: 8174 (million) % 142.19/20.32 % (4033156)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=507931777:fmbsr=2:i=32576_2892 on theBenchmark for (2892ds/32576Mi) % 142.19/20.32 % (4033156)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 142.19/20.32 % (4033156)Terminated due to inappropriate strategy. % 142.19/20.32 % (4033156)------------------------------ % 142.19/20.32 % (4033156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.19/20.32 % (4033156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.19/20.32 % (4033156)CaDiCaL version: 2.1.3 % 142.19/20.32 % (4033156)Termination reason: Inappropriate % 142.19/20.32 % (4033156)Time elapsed: 0.008 s % 142.19/20.32 % (4033156)Peak memory usage: 11 MB % 142.19/20.32 % (4033156)Instructions burned: 16 (million) % 142.19/20.32 % (4033156)------------------------------ % 142.19/20.32 % (4033156)------------------------------ % 142.19/20.32 % (4033158)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1907940114:i=11404_2891 on theBenchmark for (2891ds/11404Mi) % 142.19/20.32 % (4033152)Instruction limit reached! % 142.19/20.32 % (4033152)------------------------------ % 142.19/20.32 % (4033152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.19/20.32 % (4033152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.19/20.32 % (4033152)CaDiCaL version: 2.1.3 % 142.19/20.32 % (4033152)Termination reason: Instruction limit % 142.19/20.32 % (4033152)Termination phase: Saturation % 142.19/20.32 % (4033152)Time elapsed: 5.966 s % 142.19/20.32 % (4033152)Peak memory usage: 18 MB % 142.19/20.32 % (4033152)Instructions burned: 9157 (million) % 142.19/20.32 % (4033321)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2907144358:i=14134_2856 on theBenchmark for (2856ds/14134Mi) % 142.19/20.32 % (4033158)Instruction limit reached! % 142.19/20.32 % (4033158)------------------------------ % 142.19/20.32 % (4033158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.19/20.32 % (4033158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.19/20.32 % (4033158)CaDiCaL version: 2.1.3 % 142.19/20.32 % (4033158)Termination reason: Instruction limit % 142.19/20.32 % (4033158)Termination phase: Saturation % 142.19/20.32 % (4033158)Time elapsed: 5.626 s % 142.19/20.32 % (4033158)Peak memory usage: 17 MB % 142.19/20.32 % (4033158)Instructions burned: 11406 (million) % 142.19/20.32 % (4033324)dis+33_16_sil=32000:sac=on:random_seed=2173777852:i=15851:nm=0_2835 on theBenchmark for (2835ds/15851Mi) % 142.19/20.32 % (4033138)Instruction limit reached! % 142.19/20.32 % (4033138)------------------------------ % 142.19/20.32 % (4033138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.47/25.72 % (4033138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.47/25.72 % (4033138)CaDiCaL version: 2.1.3 % 180.47/25.72 % (4033138)Termination reason: Instruction limit % 180.47/25.72 % (4033138)Termination phase: Saturation % 180.47/25.72 % (4033138)Time elapsed: 12.918 s % 180.47/25.72 % (4033138)Peak memory usage: 17 MB % 180.47/25.72 % (4033138)Instructions burned: 22565 (million) % 180.47/25.72 % (4033326)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2681220054:avsq=on:i=17627:add=on:amm=off_2823 on theBenchmark for (2823ds/17627Mi) % 180.47/25.72 % (4033154)Instruction limit reached! % 180.47/25.72 % (4033154)------------------------------ % 180.47/25.72 % (4033154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.47/25.72 % (4033154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.47/25.72 % (4033154)CaDiCaL version: 2.1.3 % 180.47/25.72 % (4033154)Termination reason: Instruction limit % 180.47/25.72 % (4033154)Termination phase: Saturation % 180.47/25.72 % (4033154)Time elapsed: 10.114 s % 180.47/25.72 % (4033154)Peak memory usage: 22 MB % 180.47/25.72 % (4033154)Instructions burned: 20141 (million) % 180.47/25.72 % (4033328)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1060073275:s2a=on:i=53295_2813 on theBenchmark for (2813ds/53295Mi) % 180.47/25.72 % (4033125)Instruction limit reached! % 180.47/25.72 % (4033125)------------------------------ % 180.47/25.72 % (4033125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.47/25.72 % (4033125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.47/25.72 % (4033125)CaDiCaL version: 2.1.3 % 180.47/25.72 % (4033125)Termination reason: Instruction limit % 180.47/25.72 % (4033125)Termination phase: Saturation % 180.47/25.72 % (4033125)Time elapsed: 15.529 s % 180.47/25.72 % (4033125)Peak memory usage: 25 MB % 180.47/25.72 % (4033125)Instructions burned: 29342 (million) % 180.47/25.72 % (4033330)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1961880884:i=26857:ins=20_2805 on theBenchmark for (2805ds/26857Mi) % 180.47/25.72 % (4033330)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.47/25.72 % (4033330)Terminated due to inappropriate strategy. % 180.47/25.72 % (4033330)------------------------------ % 180.47/25.72 % (4033330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.47/25.72 % (4033330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.47/25.72 % (4033330)CaDiCaL version: 2.1.3 % 180.47/25.72 % (4033330)Termination reason: Inappropriate % 180.47/25.72 % (4033330)Time elapsed: 0.004 s % 180.47/25.72 % (4033330)Peak memory usage: 11 MB % 180.47/25.72 % (4033330)Instructions burned: 16 (million) % 180.47/25.72 % (4033330)------------------------------ % 180.47/25.72 % (4033330)------------------------------ % 180.47/25.72 % (4033332)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1766223066:i=28120:bs=on:fsr=off_2805 on theBenchmark for (2805ds/28120Mi) % 180.47/25.72 % (4033321)Instruction limit reached! % 180.47/25.72 % (4033321)------------------------------ % 180.47/25.72 % (4033321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.47/25.72 % (4033321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.47/25.72 % (4033321)CaDiCaL version: 2.1.3 % 180.47/25.72 % (4033321)Termination reason: Instruction limit % 180.47/25.72 % (4033321)Termination phase: Saturation % 180.47/25.72 % (4033321)Time elapsed: 5.443 s % 180.47/25.72 % (4033321)Peak memory usage: 18 MB % 180.47/25.72 % (4033321)Instructions burned: 14136 (million) % 180.47/25.72 % (4033334)fmb+10_1_sil=256000:fmbss=7:random_seed=3225527647:fmbsr=1.6:i=182295_2801 on theBenchmark for (2801ds/182295Mi) % 180.47/25.72 % (4033334)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.47/25.72 % (4033334)Terminated due to inappropriate strategy. % 180.47/25.72 % (4033334)------------------------------ % 180.47/25.72 % (4033334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.47/25.72 % (4033334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.47/25.72 % (4033334)CaDiCaL version: 2.1.3 % 180.47/25.72 % (4033334)Termination reason: Inappropriate % 180.47/25.72 % (4033334)Time elapsed: 0.007 s % 180.47/25.72 % (4033334)Peak memory usage: 10 MB % 180.47/25.72 % (4033334)Instructions burned: 16 (million) % 180.47/25.72 % (4033334)------------------------------ % 180.47/25.72 % (4033334)------------------------------ % 180.47/25.72 % (4033336)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=76202337:i=44625:gsp=on_2801 on theBenchmark for (2801ds/44625Mi) % 183.97/26.21 % (4033336)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 183.97/26.21 % (4033336)Terminated due to inappropriate strategy. % 183.97/26.21 % (4033336)------------------------------ % 183.97/26.21 % (4033336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.97/26.21 % (4033336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.97/26.21 % (4033336)CaDiCaL version: 2.1.3 % 183.97/26.21 % (4033336)Termination reason: Inappropriate % 183.97/26.21 % (4033336)Time elapsed: 0.007 s % 183.97/26.21 % (4033336)Peak memory usage: 10 MB % 183.97/26.21 % (4033336)Instructions burned: 16 (million) % 183.97/26.21 % (4033336)------------------------------ % 183.97/26.21 % (4033336)------------------------------ % 183.97/26.21 % (4033338)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3432576642:i=160505_2801 on theBenchmark for (2801ds/160505Mi) % 183.97/26.21 % (4033338)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 183.97/26.21 % (4033338)Terminated due to inappropriate strategy. % 183.97/26.21 % (4033338)------------------------------ % 183.97/26.21 % (4033338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.97/26.21 % (4033338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.97/26.21 % (4033338)CaDiCaL version: 2.1.3 % 183.97/26.21 % (4033338)Termination reason: Inappropriate % 183.97/26.21 % (4033338)Time elapsed: 0.007 s % 183.97/26.21 % (4033338)Peak memory usage: 10 MB % 183.97/26.21 % (4033338)Instructions burned: 16 (million) % 183.97/26.21 % (4033338)------------------------------ % 183.97/26.21 % (4033338)------------------------------ % 183.97/26.21 % (4033340)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2227149901:fmbsr=1.3:i=225729_2800 on theBenchmark for (2800ds/225729Mi) % 183.97/26.21 % (4033340)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 183.97/26.21 % (4033340)Terminated due to inappropriate strategy. % 183.97/26.21 % (4033340)------------------------------ % 183.97/26.21 % (4033340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.97/26.21 % (4033340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.97/26.21 % (4033340)CaDiCaL version: 2.1.3 % 183.97/26.21 % (4033340)Termination reason: Inappropriate % 183.97/26.21 % (4033340)Time elapsed: 0.007 s % 183.97/26.21 % (4033340)Peak memory usage: 10 MB % 183.97/26.21 % (4033340)Instructions burned: 16 (million) % 183.97/26.21 % (4033340)------------------------------ % 183.97/26.21 % (4033340)------------------------------ % 183.97/26.21 % (4033342)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=606531969:fmbsr=2:i=185024:ins=7_2800 on theBenchmark for (2800ds/185024Mi) % 183.97/26.21 % (4033342)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 183.97/26.21 % (4033342)Terminated due to inappropriate strategy. % 183.97/26.21 % (4033342)------------------------------ % 183.97/26.21 % (4033342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.97/26.21 % (4033342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.97/26.21 % (4033342)CaDiCaL version: 2.1.3 % 183.97/26.21 % (4033342)Termination reason: Inappropriate % 183.97/26.21 % (4033342)Time elapsed: 0.007 s % 183.97/26.21 % (4033342)Peak memory usage: 10 MB % 183.97/26.21 % (4033342)Instructions burned: 16 (million) % 183.97/26.21 % (4033342)------------------------------ % 183.97/26.21 % (4033342)------------------------------ % 183.97/26.21 % (4033344)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2768731654:rtra=on_2800 on theBenchmark for (2800ds/0Mi) % 183.97/26.21 % (4033344)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 183.97/26.21 % (4033344)Terminated due to inappropriate strategy. % 183.97/26.21 % (4033344)------------------------------ % 183.97/26.21 % (4033344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.97/26.21 % (4033344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.97/26.21 % (4033344)CaDiCaL version: 2.1.3 % 183.97/26.21 % (4033344)Termination reason: Inappropriate % 183.97/26.21 % (4033344)Time elapsed: 0.007 s % 183.97/26.21 % (4033344)Peak memory usage: 10 MB % 183.97/26.21 % (4033344)Instructions burned: 16 (million) % 183.97/26.21 % (4033344)------------------------------ % 183.97/26.21 % (4033344)------------------------------ % 183.97/26.21 % (4033346)% WARNING: option uhcvi not known. % 183.97/26.21 % (4033346)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1581754913:i=271062:add=off:rtra=on:rawr=on_2799 on theBenchmark for (2799ds/271062Mi) % 188.09/27.03 % (4033324)Instruction limit reached! % 188.09/27.03 % (4033324)------------------------------ % 188.09/27.03 % (4033324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.09/27.03 % (4033324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.09/27.03 % (4033324)CaDiCaL version: 2.1.3 % 188.09/27.03 % (4033324)Termination reason: Instruction limit % 188.09/27.03 % (4033324)Termination phase: Saturation % 188.09/27.03 % (4033324)Time elapsed: 6.139 s % 188.09/27.03 % (4033324)Peak memory usage: 25 MB % 188.09/27.03 % (4033324)Instructions burned: 15853 (million) % 188.09/27.03 % (4033348)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3288969547:i=176048:add=on:rtra=on:rawr=on_2773 on theBenchmark for (2773ds/176048Mi) % 188.09/27.03 % (4033332)Instruction limit reached! % 188.09/27.03 % (4033332)------------------------------ % 188.09/27.03 % (4033332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.09/27.03 % (4033332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.09/27.03 % (4033332)CaDiCaL version: 2.1.3 % 188.09/27.03 % (4033332)Termination reason: Instruction limit % 188.09/27.03 % (4033332)Termination phase: Saturation % 188.09/27.03 % (4033332)Time elapsed: 5.719 s % 188.09/27.03 % (4033332)Peak memory usage: 23 MB % 188.09/27.03 % (4033332)Instructions burned: 28123 (million) % 188.09/27.03 % (4033350)dis+10_1_sil=32000:si=on:sp=arity:random_seed=204303372:i=206:fgj=on:rtra=on_2748 on theBenchmark for (2748ds/206Mi) % 188.09/27.03 % (4033350)Instruction limit reached! % 188.09/27.03 % (4033350)------------------------------ % 188.09/27.03 % (4033350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.09/27.03 % (4033350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.09/27.03 % (4033350)CaDiCaL version: 2.1.3 % 188.09/27.03 % (4033350)Termination reason: Instruction limit % 188.09/27.03 % (4033350)Termination phase: Saturation % 188.09/27.03 % (4033350)Time elapsed: 0.044 s % 188.09/27.03 % (4033350)Peak memory usage: 12 MB % 188.09/27.03 % (4033350)Instructions burned: 208 (million) % 188.09/27.03 % (4033352)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2730194753:i=232:rtra=on_2747 on theBenchmark for (2747ds/232Mi) % 188.09/27.03 % (4033352)Instruction limit reached! % 188.09/27.03 % (4033352)------------------------------ % 188.09/27.03 % (4033352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.09/27.03 % (4033352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.09/27.03 % (4033352)CaDiCaL version: 2.1.3 % 188.09/27.03 % (4033352)Termination reason: Instruction limit % 188.09/27.03 % (4033352)Termination phase: Saturation % 188.09/27.03 % (4033352)Time elapsed: 0.049 s % 188.09/27.03 % (4033352)Peak memory usage: 12 MB % 188.09/27.03 % (4033352)Instructions burned: 236 (million) % 188.09/27.03 % (4033354)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3784151768:i=262:rtra=on_2747 on theBenchmark for (2747ds/262Mi) % 188.09/27.03 % (4033354)Instruction limit reached! % 188.09/27.03 % (4033354)------------------------------ % 188.09/27.03 % (4033354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.09/27.03 % (4033354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.09/27.03 % (4033354)CaDiCaL version: 2.1.3 % 188.09/27.03 % (4033354)Termination reason: Instruction limit % 188.09/27.03 % (4033354)Termination phase: Saturation % 188.09/27.03 % (4033354)Time elapsed: 0.055 s % 188.09/27.03 % (4033354)Peak memory usage: 12 MB % 188.09/27.03 % (4033354)Instructions burned: 264 (million) % 188.09/27.03 % (4033356)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1388402551:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2746 on theBenchmark for (2746ds/318Mi) % 188.09/27.03 % (4033356)Instruction limit reached! % 188.09/27.03 % (4033356)------------------------------ % 188.09/27.03 % (4033356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.09/27.03 % (4033356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.09/27.03 % (4033356)CaDiCaL version: 2.1.3 % 188.09/27.03 % (4033356)Termination reason: Instruction limit % 188.09/27.03 % (4033356)Termination phase: Saturation % 188.09/27.03 % (4033356)Time elapsed: 0.071 s % 188.09/27.03 % (4033356)Peak memory usage: 13 MB % 188.09/27.03 % (4033356)Instructions burned: 322 (million) % 188.09/27.03 % (4033358)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2614955857:i=1428:nm=2:rtra=on_2745 on theBenchmark for (2745ds/1428Mi) % 199.66/28.46 % (4033358)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 199.66/28.46 % (4033358)Terminated due to inappropriate strategy. % 199.66/28.46 % (4033358)------------------------------ % 199.66/28.46 % (4033358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.66/28.46 % (4033358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.66/28.46 % (4033358)CaDiCaL version: 2.1.3 % 199.66/28.46 % (4033358)Termination reason: Inappropriate % 199.66/28.46 % (4033358)Time elapsed: 0.003 s % 199.66/28.46 % (4033358)Peak memory usage: 10 MB % 199.66/28.46 % (4033358)Instructions burned: 16 (million) % 199.66/28.46 % (4033358)------------------------------ % 199.66/28.46 % (4033358)------------------------------ % 199.66/28.46 % (4033360)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1625626197:i=262:bd=preordered:rtra=on:fsd=on_2745 on theBenchmark for (2745ds/262Mi) % 199.66/28.46 % (4033360)Instruction limit reached! % 199.66/28.46 % (4033360)------------------------------ % 199.66/28.46 % (4033360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.66/28.46 % (4033360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.66/28.46 % (4033360)CaDiCaL version: 2.1.3 % 199.66/28.46 % (4033360)Termination reason: Instruction limit % 199.66/28.46 % (4033360)Termination phase: Saturation % 199.66/28.46 % (4033360)Time elapsed: 0.055 s % 199.66/28.46 % (4033360)Peak memory usage: 12 MB % 199.66/28.46 % (4033360)Instructions burned: 265 (million) % 199.66/28.46 % (4033362)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=604455797:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2745 on theBenchmark for (2745ds/1368Mi) % 199.66/28.46 % (4033326)Instruction limit reached! % 199.66/28.46 % (4033326)------------------------------ % 199.66/28.46 % (4033326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.66/28.46 % (4033326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.66/28.46 % (4033326)CaDiCaL version: 2.1.3 % 199.66/28.46 % (4033326)Termination reason: Instruction limit % 199.66/28.46 % (4033326)Termination phase: Saturation % 199.66/28.46 % (4033326)Time elapsed: 8.057 s % 199.66/28.46 % (4033326)Peak memory usage: 161 MB % 199.66/28.46 % (4033326)Instructions burned: 17628 (million) % 199.66/28.46 % (4033364)ott-21_1_sil=16000:si=on:fs=off:random_seed=2425192208:i=360:av=off:fsr=off:rtra=on_2742 on theBenchmark for (2742ds/360Mi) % 199.66/28.46 % (4033362)Instruction limit reached! % 199.66/28.46 % (4033362)------------------------------ % 199.66/28.46 % (4033362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.66/28.46 % (4033362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.66/28.46 % (4033362)CaDiCaL version: 2.1.3 % 199.66/28.46 % (4033362)Termination reason: Instruction limit % 199.66/28.46 % (4033362)Termination phase: Saturation % 199.66/28.46 % (4033362)Time elapsed: 0.308 s % 199.66/28.46 % (4033362)Peak memory usage: 17 MB % 199.66/28.46 % (4033362)Instructions burned: 1372 (million) % 199.66/28.46 % (4033366)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1596781485:i=954:bd=all:rtra=on_2741 on theBenchmark for (2741ds/954Mi) % 199.66/28.46 % (4033364)Instruction limit reached! % 199.66/28.46 % (4033364)------------------------------ % 199.66/28.46 % (4033364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.66/28.46 % (4033364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.66/28.46 % (4033364)CaDiCaL version: 2.1.3 % 199.66/28.46 % (4033364)Termination reason: Instruction limit % 199.66/28.46 % (4033364)Termination phase: Saturation % 199.66/28.46 % (4033364)Time elapsed: 0.134 s % 199.66/28.46 % (4033364)Peak memory usage: 12 MB % 199.66/28.46 % (4033364)Instructions burned: 362 (million) % 199.66/28.46 % (4033368)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1984948617:fmbsr=1.3:i=1730:ins=25:rtra=on_2741 on theBenchmark for (2741ds/1730Mi) % 199.66/28.46 % (4033368)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 199.66/28.46 % (4033368)Terminated due to inappropriate strategy. % 199.66/28.46 % (4033368)------------------------------ % 199.66/28.46 % (4033368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.66/28.46 % (4033368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.66/28.46 % (4033368)CaDiCaL version: 2.1.3 % 199.66/28.46 % (4033368)Termination reason: Inappropriate % 216.61/30.89 % (4033368)Time elapsed: 0.005 s % 216.61/30.89 % (4033368)Peak memory usage: 10 MB % 216.61/30.89 % (4033368)Instructions burned: 12 (million) % 216.61/30.89 % (4033368)------------------------------ % 216.61/30.89 % (4033368)------------------------------ % 216.61/30.89 % (4033370)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1216907921:i=2358:rtra=on_2740 on theBenchmark for (2740ds/2358Mi) % 216.61/30.89 % (4033366)Instruction limit reached! % 216.61/30.89 % (4033366)------------------------------ % 216.61/30.89 % (4033366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.61/30.89 % (4033366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.61/30.89 % (4033366)CaDiCaL version: 2.1.3 % 216.61/30.89 % (4033366)Termination reason: Instruction limit % 216.61/30.89 % (4033366)Termination phase: Saturation % 216.61/30.89 % (4033366)Time elapsed: 0.200 s % 216.61/30.89 % (4033366)Peak memory usage: 13 MB % 216.61/30.89 % (4033366)Instructions burned: 957 (million) % 216.61/30.89 % (4033372)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3448590714:i=1778:ins=1:rtra=on_2739 on theBenchmark for (2739ds/1778Mi) % 216.61/30.89 % (4033372)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 216.61/30.89 % (4033372)Terminated due to inappropriate strategy. % 216.61/30.89 % (4033372)------------------------------ % 216.61/30.89 % (4033372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.61/30.89 % (4033372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.61/30.89 % (4033372)CaDiCaL version: 2.1.3 % 216.61/30.89 % (4033372)Termination reason: Inappropriate % 216.61/30.89 % (4033372)Time elapsed: 0.003 s % 216.61/30.89 % (4033372)Peak memory usage: 10 MB % 216.61/30.89 % (4033372)Instructions burned: 12 (million) % 216.61/30.89 % (4033372)------------------------------ % 216.61/30.89 % (4033372)------------------------------ % 216.61/30.89 % (4033374)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3989152284:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2739 on theBenchmark for (2739ds/1384Mi) % 216.61/30.89 % (4033374)Instruction limit reached! % 216.61/30.89 % (4033374)------------------------------ % 216.61/30.89 % (4033374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.61/30.89 % (4033374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.61/30.89 % (4033374)CaDiCaL version: 2.1.3 % 216.61/30.89 % (4033374)Termination reason: Instruction limit % 216.61/30.89 % (4033374)Termination phase: Saturation % 216.61/30.89 % (4033374)Time elapsed: 0.289 s % 216.61/30.89 % (4033374)Peak memory usage: 15 MB % 216.61/30.89 % (4033374)Instructions burned: 1387 (million) % 216.61/30.89 % (4033376)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=4158204761:i=1758:kws=inv_precedence:fsr=off:rtra=on_2736 on theBenchmark for (2736ds/1758Mi) % 216.61/30.89 % (4033376)Instruction limit reached! % 216.61/30.89 % (4033376)------------------------------ % 216.61/30.89 % (4033376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.61/30.89 % (4033376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.61/30.89 % (4033376)CaDiCaL version: 2.1.3 % 216.61/30.89 % (4033376)Termination reason: Instruction limit % 216.61/30.89 % (4033376)Termination phase: Saturation % 216.61/30.89 % (4033376)Time elapsed: 0.357 s % 216.61/30.89 % (4033376)Peak memory usage: 16 MB % 216.61/30.89 % (4033376)Instructions burned: 1762 (million) % 216.61/30.89 % (4033378)fmb+10_1_sil=64000:si=on:random_seed=649611491:i=44122:nm=2:rtra=on:gsp=on_2732 on theBenchmark for (2732ds/44122Mi) % 216.61/30.89 % (4033378)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 216.61/30.89 % (4033378)Terminated due to inappropriate strategy. % 216.61/30.89 % (4033378)------------------------------ % 216.61/30.89 % (4033378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.61/30.89 % (4033378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.61/30.89 % (4033378)CaDiCaL version: 2.1.3 % 216.61/30.89 % (4033378)Termination reason: Inappropriate % 216.61/30.89 % (4033378)Time elapsed: 0.004 s % 216.61/30.89 % (4033378)Peak memory usage: 10 MB % 216.61/30.89 % (4033378)Instructions burned: 17 (million) % 216.61/30.89 % (4033378)------------------------------ % 216.61/30.89 % (4033378)------------------------------ % 216.61/30.89 % (4033380)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2875075047:i=19030:nm=5:rtra=on_2732 on theBenchmark for (2732ds/19030Mi) % 246.74/35.13 % (4033380)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 246.74/35.13 % (4033380)Terminated due to inappropriate strategy. % 246.74/35.13 % (4033380)------------------------------ % 246.74/35.13 % (4033380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.74/35.13 % (4033380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.74/35.13 % (4033380)CaDiCaL version: 2.1.3 % 246.74/35.13 % (4033380)Termination reason: Inappropriate % 246.74/35.13 % (4033380)Time elapsed: 0.003 s % 246.74/35.13 % (4033380)Peak memory usage: 11 MB % 246.74/35.13 % (4033380)Instructions burned: 17 (million) % 246.74/35.13 % (4033380)------------------------------ % 246.74/35.13 % (4033380)------------------------------ % 246.74/35.13 % (4033382)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3372775266:fmbsr=1.7:i=1840:rtra=on_2732 on theBenchmark for (2732ds/1840Mi) % 246.74/35.13 % (4033382)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 246.74/35.13 % (4033382)Terminated due to inappropriate strategy. % 246.74/35.13 % (4033382)------------------------------ % 246.74/35.13 % (4033382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.74/35.13 % (4033382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.74/35.13 % (4033382)CaDiCaL version: 2.1.3 % 246.74/35.13 % (4033382)Termination reason: Inappropriate % 246.74/35.13 % (4033382)Time elapsed: 0.003 s % 246.74/35.13 % (4033382)Peak memory usage: 11 MB % 246.74/35.13 % (4033382)Instructions burned: 16 (million) % 246.74/35.13 % (4033382)------------------------------ % 246.74/35.13 % (4033382)------------------------------ % 246.74/35.13 % (4033384)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=738067770:i=10262:rtra=on_2732 on theBenchmark for (2732ds/10262Mi) % 246.74/35.13 % (4033370)Instruction limit reached! % 246.74/35.13 % (4033370)------------------------------ % 246.74/35.13 % (4033370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.74/35.13 % (4033370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.74/35.13 % (4033370)CaDiCaL version: 2.1.3 % 246.74/35.13 % (4033370)Termination reason: Instruction limit % 246.74/35.13 % (4033370)Termination phase: Saturation % 246.74/35.13 % (4033370)Time elapsed: 0.886 s % 246.74/35.13 % (4033370)Peak memory usage: 13 MB % 246.74/35.13 % (4033370)Instructions burned: 2358 (million) % 246.74/35.13 % (4033386)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3490492577:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2731 on theBenchmark for (2731ds/2944Mi) % 246.74/35.13 % (4033386)Instruction limit reached! % 246.74/35.13 % (4033386)------------------------------ % 246.74/35.13 % (4033386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.74/35.13 % (4033386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.74/35.13 % (4033386)CaDiCaL version: 2.1.3 % 246.74/35.13 % (4033386)Termination reason: Instruction limit % 246.74/35.13 % (4033386)Termination phase: Saturation % 246.74/35.13 % (4033386)Time elapsed: 1.271 s % 246.74/35.13 % (4033386)Peak memory usage: 30 MB % 246.74/35.13 % (4033386)Instructions burned: 2945 (million) % 246.74/35.13 % (4033388)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2315346673:i=12648:rtra=on_2718 on theBenchmark for (2718ds/12648Mi) % 246.74/35.13 % (4033388)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 246.74/35.13 % (4033388)Terminated due to inappropriate strategy. % 246.74/35.13 % (4033388)------------------------------ % 246.74/35.13 % (4033388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.74/35.13 % (4033388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.74/35.13 % (4033388)CaDiCaL version: 2.1.3 % 246.74/35.13 % (4033388)Termination reason: Inappropriate % 246.74/35.13 % (4033388)Time elapsed: 0.007 s % 246.74/35.13 % (4033388)Peak memory usage: 10 MB % 246.74/35.13 % (4033388)Instructions burned: 16 (million) % 246.74/35.13 % (4033388)------------------------------ % 246.74/35.13 % (4033388)------------------------------ % 246.74/35.13 % (4033390)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1394340109:fmbsr=2.30978:i=4348:rtra=on_2718 on theBenchmark for (2718ds/4348Mi) % 246.74/35.13 % (4033390)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 246.74/35.13 % (4033390)Terminated due to inappropriate strategy. % 246.74/35.13 % (4033390)------------------------------ % 300.43/42.64 % (4033390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.64 % (4033390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.64 % (4033390)CaDiCaL version: 2.1.3 % 300.43/42.64 % (4033390)Termination reason: Inappropriate % 300.43/42.64 % (4033390)Time elapsed: 0.007 s % 300.43/42.64 % (4033390)Peak memory usage: 10 MB % 300.43/42.64 % (4033390)Instructions burned: 16 (million) % 300.43/42.64 % (4033390)------------------------------ % 300.43/42.64 % (4033390)------------------------------ % 300.43/42.64 % (4033392)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3055225375:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2718 on theBenchmark for (2718ds/1738Mi) % 300.43/42.64 % (4033392)Instruction limit reached! % 300.43/42.64 % (4033392)------------------------------ % 300.43/42.64 % (4033392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.64 % (4033392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.64 % (4033392)CaDiCaL version: 2.1.3 % 300.43/42.64 % (4033392)Termination reason: Instruction limit % 300.43/42.64 % (4033392)Termination phase: Saturation % 300.43/42.64 % (4033392)Time elapsed: 0.695 s % 300.43/42.64 % (4033392)Peak memory usage: 15 MB % 300.43/42.64 % (4033392)Instructions burned: 1738 (million) % 300.43/42.64 % (4033395)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1675224700:i=10228:av=off:rtra=on_2711 on theBenchmark for (2711ds/10228Mi) % 300.43/42.64 % (4033384)Instruction limit reached! % 300.43/42.64 % (4033384)------------------------------ % 300.43/42.64 % (4033384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.64 % (4033384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.64 % (4033384)CaDiCaL version: 2.1.3 % 300.43/42.64 % (4033384)Termination reason: Instruction limit % 300.43/42.64 % (4033384)Termination phase: Saturation % 300.43/42.64 % (4033384)Time elapsed: 2.139 s % 300.43/42.64 % (4033384)Peak memory usage: 21 MB % 300.43/42.64 % (4033384)Instructions burned: 10266 (million) % 300.43/42.64 % (4033397)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1771988873:i=108564:rtra=on_2710 on theBenchmark for (2710ds/108564Mi) % 300.43/42.64 % (4033397)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.43/42.64 % (4033397)Terminated due to inappropriate strategy. % 300.43/42.64 % (4033397)------------------------------ % 300.43/42.64 % (4033397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.64 % (4033397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.64 % (4033397)CaDiCaL version: 2.1.3 % 300.43/42.64 % (4033397)Termination reason: Inappropriate % 300.43/42.64 % (4033397)Time elapsed: 0.004 s % 300.43/42.64 % (4033397)Peak memory usage: 10 MB % 300.43/42.64 % (4033397)Instructions burned: 17 (million) % 300.43/42.64 % (4033397)------------------------------ % 300.43/42.64 % (4033397)------------------------------ % 300.43/42.64 % (4033399)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3472948804:i=7024:aac=none:rtra=on_2710 on theBenchmark for (2710ds/7024Mi) % 300.43/42.64 % (4033399)Instruction limit reached! % 300.43/42.64 % (4033399)------------------------------ % 300.43/42.64 % (4033399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.64 % (4033399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.64 % (4033399)CaDiCaL version: 2.1.3 % 300.43/42.64 % (4033399)Termination reason: Instruction limit % 300.43/42.64 % (4033399)Termination phase: Saturation % 300.43/42.64 % (4033399)Time elapsed: 1.480 s % 300.43/42.64 % (4033399)Peak memory usage: 18 MB % 300.43/42.64 % (4033399)Instructions burned: 7029 (million) % 300.43/42.64 % (4033759)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1391398377:i=7546:rtra=on:amm=off_2695 on theBenchmark for (2695ds/7546Mi) % 300.43/42.64 % (4033062)Instruction limit reached! % 300.43/42.64 % (4033062)------------------------------ % 300.43/42.64 % (4033062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.64 % (4033062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.64 % (4033062)CaDiCaL version: 2.1.3 % 300.43/42.64 % (4033062)Termination reason: Instruction limit % 300.43/42.64 % (4033062)Termination phase: Saturation % 300.43/42.64 % (4033062)Time elapsed: 30.535 s % 300.43/42.64 % (4033062)Peak memory usage: 22 MB % 300.43/42.64 % (4033062)Instructions burned: 88026 (million) % 300.43/42.64 % (4033761)ott+11_1_sil=16000:si=on:gs=on:random_seed=714603073:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fs % 300.43/42.64 Terminated % 300.43/42.64 % Vampire exiting %------------------------------------------------------------------------------