%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC449_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n020.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:06:01 PM UTC 2026 % Result : Timeout 300.03s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWC449_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.18 % Computer : n020.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 09:38:50 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.22 Running first-order model finding % 0.07/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.68/0.80 % (56107)Will run a generic schedule for satisfiability detection. % 3.68/0.80 % (56112)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3052613818_2999 on theBenchmark for (2999ds/0Mi) % 3.68/0.80 % (56112)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.68/0.80 % (56112)Terminated due to inappropriate strategy. % 3.68/0.80 % (56112)------------------------------ % 3.68/0.80 % (56112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.80 % (56112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.80 % (56112)CaDiCaL version: 2.1.3 % 3.68/0.80 % (56112)Termination reason: Inappropriate % 3.68/0.80 % (56112)Time elapsed: 0.0000 s % 3.68/0.80 % (56112)Peak memory usage: 10 MB % 3.68/0.80 % (56112)Instructions burned: 1 (million) % 3.68/0.80 % (56112)------------------------------ % 3.68/0.80 % (56112)------------------------------ % 3.68/0.80 % (56113)% WARNING: option uhcvi not known. % 3.68/0.80 % (56117)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3319953591:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.68/0.80 % (56113)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=317694930:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.68/0.80 % (56114)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3188101613:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.68/0.80 % (56115)dis+10_1_sil=32000:sp=arity:random_seed=3212676396:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.68/0.80 % (56116)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1201254370:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.68/0.80 % (56118)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2855035714:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.68/0.80 % (56120)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3500298028:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.68/0.80 % (56120)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.68/0.80 % (56120)Terminated due to inappropriate strategy. % 3.68/0.80 % (56120)------------------------------ % 3.68/0.80 % (56120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.80 % (56120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.80 % (56120)CaDiCaL version: 2.1.3 % 3.68/0.80 % (56120)Termination reason: Inappropriate % 3.68/0.80 % (56120)Time elapsed: 0.0000 s % 3.68/0.80 % (56120)Peak memory usage: 11 MB % 3.68/0.80 % (56120)Instructions burned: 1 (million) % 3.68/0.80 % (56120)------------------------------ % 3.68/0.80 % (56120)------------------------------ % 3.68/0.80 % (56128)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2594903137:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.68/0.80 % (56128)Instruction limit reached! % 3.68/0.80 % (56128)------------------------------ % 3.68/0.80 % (56128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.80 % (56128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.80 % (56128)CaDiCaL version: 2.1.3 % 3.68/0.80 % (56128)Termination reason: Instruction limit % 3.68/0.80 % (56128)Termination phase: Saturation % 3.68/0.80 % (56128)Time elapsed: 0.050 s % 3.68/0.80 % (56128)Peak memory usage: 12 MB % 3.68/0.80 % (56128)Instructions burned: 144 (million) % 3.68/0.80 % (56115)Instruction limit reached! % 3.68/0.80 % (56115)------------------------------ % 3.68/0.80 % (56115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.80 % (56115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.80 % (56115)CaDiCaL version: 2.1.3 % 3.68/0.80 % (56115)Termination reason: Instruction limit % 3.68/0.80 % (56115)Termination phase: Saturation % 3.68/0.80 % (56115)Time elapsed: 0.067 s % 3.68/0.80 % (56115)Peak memory usage: 12 MB % 3.68/0.80 % (56115)Instructions burned: 108 (million) % 3.68/0.80 % (56116)Instruction limit reached! % 3.68/0.80 % (56116)------------------------------ % 3.68/0.80 % (56116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.68/0.80 % (56116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.68/0.80 % (56116)CaDiCaL version: 2.1.3 % 3.68/0.80 % (56116)Termination reason: Instruction limit % 3.68/0.80 % (56116)Termination phase: Saturation % 3.68/0.80 % (56116)Time elapsed: 0.073 s % 3.68/0.80 % (56116)Peak memory usage: 12 MB % 7.27/1.32 % (56116)Instructions burned: 116 (million) % 7.27/1.32 % (56130)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=1419434640:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.27/1.32 % (56117)Instruction limit reached! % 7.27/1.32 % (56117)------------------------------ % 7.27/1.32 % (56117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.27/1.32 % (56117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.27/1.32 % (56117)CaDiCaL version: 2.1.3 % 7.27/1.32 % (56117)Termination reason: Instruction limit % 7.27/1.32 % (56117)Termination phase: Saturation % 7.27/1.32 % (56117)Time elapsed: 0.081 s % 7.27/1.32 % (56117)Peak memory usage: 13 MB % 7.27/1.32 % (56117)Instructions burned: 131 (million) % 7.27/1.32 % (56131)ott-21_1_sil=16000:fs=off:random_seed=401115440:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.27/1.32 % (56132)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3892856437:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.27/1.32 % (56134)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2911138678:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.27/1.32 % (56118)Instruction limit reached! % 7.27/1.32 % (56118)------------------------------ % 7.27/1.32 % (56118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.27/1.32 % (56118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.27/1.32 % (56118)CaDiCaL version: 2.1.3 % 7.27/1.32 % (56118)Termination reason: Instruction limit % 7.27/1.32 % (56118)Termination phase: Saturation % 7.27/1.32 % (56118)Time elapsed: 0.099 s % 7.27/1.32 % (56118)Peak memory usage: 12 MB % 7.27/1.32 % (56118)Instructions burned: 160 (million) % 7.27/1.32 % (56134)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.27/1.32 % (56134)Terminated due to inappropriate strategy. % 7.27/1.32 % (56134)------------------------------ % 7.27/1.32 % (56134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.27/1.32 % (56134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.27/1.32 % (56134)CaDiCaL version: 2.1.3 % 7.27/1.32 % (56134)Termination reason: Inappropriate % 7.27/1.32 % (56134)Time elapsed: 0.001 s % 7.27/1.32 % (56134)Peak memory usage: 10 MB % 7.27/1.32 % (56134)Instructions burned: 1 (million) % 7.27/1.32 % (56134)------------------------------ % 7.27/1.32 % (56134)------------------------------ % 7.27/1.32 % (56138)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=912573885:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.27/1.32 % (56139)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=65135430:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.27/1.32 % (56139)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.27/1.32 % (56139)Terminated due to inappropriate strategy. % 7.27/1.32 % (56139)------------------------------ % 7.27/1.32 % (56139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.27/1.32 % (56139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.27/1.32 % (56139)CaDiCaL version: 2.1.3 % 7.27/1.32 % (56139)Termination reason: Inappropriate % 7.27/1.32 % (56139)Time elapsed: 0.001 s % 7.27/1.32 % (56139)Peak memory usage: 10 MB % 7.27/1.32 % (56139)Instructions burned: 1 (million) % 7.27/1.32 % (56139)------------------------------ % 7.27/1.32 % (56139)------------------------------ % 7.27/1.32 % (56142)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=2799951664: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) % 7.27/1.32 % (56131)Instruction limit reached! % 7.27/1.32 % (56131)------------------------------ % 7.27/1.32 % (56131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.27/1.32 % (56131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.27/1.32 % (56131)CaDiCaL version: 2.1.3 % 7.27/1.32 % (56131)Termination reason: Instruction limit % 7.27/1.32 % (56131)Termination phase: Saturation % 7.27/1.32 % (56131)Time elapsed: 0.082 s % 7.27/1.32 % (56131)Peak memory usage: 12 MB % 7.27/1.32 % (56131)Instructions burned: 180 (million) % 7.27/1.32 % (56144)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2304126077:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.48/3.44 % (56130)Instruction limit reached! % 22.48/3.44 % (56130)------------------------------ % 22.48/3.44 % (56130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.48/3.44 % (56130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.48/3.44 % (56130)CaDiCaL version: 2.1.3 % 22.48/3.44 % (56130)Termination reason: Instruction limit % 22.48/3.44 % (56130)Termination phase: Saturation % 22.48/3.44 % (56130)Time elapsed: 0.198 s % 22.48/3.44 % (56130)Peak memory usage: 17 MB % 22.48/3.44 % (56130)Instructions burned: 688 (million) % 22.48/3.44 % (56146)fmb+10_1_sil=64000:random_seed=2869175698:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 22.48/3.44 % (56146)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.48/3.44 % (56146)Terminated due to inappropriate strategy. % 22.48/3.44 % (56146)------------------------------ % 22.48/3.44 % (56146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.48/3.44 % (56146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.48/3.44 % (56146)CaDiCaL version: 2.1.3 % 22.48/3.44 % (56146)Termination reason: Inappropriate % 22.48/3.44 % (56146)Time elapsed: 0.0000 s % 22.48/3.44 % (56146)Peak memory usage: 11 MB % 22.48/3.44 % (56146)Instructions burned: 1 (million) % 22.48/3.44 % (56146)------------------------------ % 22.48/3.44 % (56146)------------------------------ % 22.48/3.44 % (56148)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1965975953:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 22.48/3.44 % (56148)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.48/3.44 % (56148)Terminated due to inappropriate strategy. % 22.48/3.44 % (56148)------------------------------ % 22.48/3.44 % (56148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.48/3.44 % (56148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.48/3.44 % (56148)CaDiCaL version: 2.1.3 % 22.48/3.44 % (56148)Termination reason: Inappropriate % 22.48/3.44 % (56148)Time elapsed: 0.0000 s % 22.48/3.44 % (56148)Peak memory usage: 11 MB % 22.48/3.44 % (56148)Instructions burned: 1 (million) % 22.48/3.44 % (56148)------------------------------ % 22.48/3.44 % (56148)------------------------------ % 22.48/3.44 % (56150)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1967627671:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 22.48/3.44 % (56150)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.48/3.44 % (56150)Terminated due to inappropriate strategy. % 22.48/3.44 % (56150)------------------------------ % 22.48/3.44 % (56150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.48/3.44 % (56150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.48/3.44 % (56150)CaDiCaL version: 2.1.3 % 22.48/3.44 % (56150)Termination reason: Inappropriate % 22.48/3.44 % (56150)Time elapsed: 0.0000 s % 22.48/3.44 % (56150)Peak memory usage: 10 MB % 22.48/3.44 % (56150)Instructions burned: 1 (million) % 22.48/3.44 % (56150)------------------------------ % 22.48/3.44 % (56150)------------------------------ % 22.48/3.44 % (56152)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=389070244:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 22.48/3.44 % (56132)Instruction limit reached! % 22.48/3.44 % (56132)------------------------------ % 22.48/3.44 % (56132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.48/3.44 % (56132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.48/3.44 % (56132)CaDiCaL version: 2.1.3 % 22.48/3.44 % (56132)Termination reason: Instruction limit % 22.48/3.44 % (56132)Termination phase: Saturation % 22.48/3.44 % (56132)Time elapsed: 0.312 s % 22.48/3.44 % (56132)Peak memory usage: 13 MB % 22.48/3.44 % (56132)Instructions burned: 477 (million) % 22.48/3.44 % (56154)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1567580488:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 22.48/3.44 % (56142)Instruction limit reached! % 22.48/3.44 % (56142)------------------------------ % 22.48/3.44 % (56142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.48/3.44 % (56142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.48/3.44 % (56142)CaDiCaL version: 2.1.3 % 22.48/3.44 % (56142)Termination reason: Instruction limit % 22.48/3.44 % (56142)Termination phase: Saturation % 22.48/3.44 % (56142)Time elapsed: 0.393 s % 22.48/3.44 % (56142)Peak memory usage: 17 MB % 38.08/5.69 % (56142)Instructions burned: 692 (million) % 38.08/5.69 % (56156)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=539915781:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 38.08/5.69 % (56156)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.08/5.69 % (56156)Terminated due to inappropriate strategy. % 38.08/5.69 % (56156)------------------------------ % 38.08/5.69 % (56156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.08/5.69 % (56156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.08/5.69 % (56156)CaDiCaL version: 2.1.3 % 38.08/5.69 % (56156)Termination reason: Inappropriate % 38.08/5.69 % (56156)Time elapsed: 0.001 s % 38.08/5.69 % (56156)Peak memory usage: 10 MB % 38.08/5.69 % (56156)Instructions burned: 1 (million) % 38.08/5.69 % (56156)------------------------------ % 38.08/5.69 % (56156)------------------------------ % 38.08/5.69 % (56158)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2908797588:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 38.08/5.69 % (56158)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.08/5.69 % (56158)Terminated due to inappropriate strategy. % 38.08/5.69 % (56158)------------------------------ % 38.08/5.69 % (56158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.08/5.69 % (56158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.08/5.69 % (56158)CaDiCaL version: 2.1.3 % 38.08/5.69 % (56158)Termination reason: Inappropriate % 38.08/5.69 % (56158)Time elapsed: 0.001 s % 38.08/5.69 % (56158)Peak memory usage: 10 MB % 38.08/5.69 % (56158)Instructions burned: 1 (million) % 38.08/5.69 % (56158)------------------------------ % 38.08/5.69 % (56158)------------------------------ % 38.08/5.69 % (56160)ott-2_1_sil=16000:newcnf=on:random_seed=3101290911:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 38.08/5.69 % (56144)Instruction limit reached! % 38.08/5.69 % (56144)------------------------------ % 38.08/5.69 % (56144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.08/5.69 % (56144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.08/5.69 % (56144)CaDiCaL version: 2.1.3 % 38.08/5.69 % (56144)Termination reason: Instruction limit % 38.08/5.69 % (56144)Termination phase: Saturation % 38.08/5.69 % (56144)Time elapsed: 0.502 s % 38.08/5.69 % (56144)Peak memory usage: 20 MB % 38.08/5.69 % (56144)Instructions burned: 879 (million) % 38.08/5.69 % (56162)ott+10_1_sil=32000:tgt=ground:random_seed=3294132002:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 38.08/5.69 % (56138)Instruction limit reached! % 38.08/5.69 % (56138)------------------------------ % 38.08/5.69 % (56138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.08/5.69 % (56138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.08/5.69 % (56138)CaDiCaL version: 2.1.3 % 38.08/5.69 % (56138)Termination reason: Instruction limit % 38.08/5.69 % (56138)Termination phase: Saturation % 38.08/5.69 % (56138)Time elapsed: 0.601 s % 38.08/5.69 % (56138)Peak memory usage: 16 MB % 38.08/5.69 % (56138)Instructions burned: 1179 (million) % 38.08/5.69 % (56164)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=835086431:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 38.08/5.69 % (56164)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 38.08/5.69 % (56164)Terminated due to inappropriate strategy. % 38.08/5.69 % (56164)------------------------------ % 38.08/5.69 % (56164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.08/5.69 % (56164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.08/5.69 % (56164)CaDiCaL version: 2.1.3 % 38.08/5.69 % (56164)Termination reason: Inappropriate % 38.08/5.69 % (56164)Time elapsed: 0.001 s % 38.08/5.69 % (56164)Peak memory usage: 10 MB % 38.08/5.69 % (56164)Instructions burned: 1 (million) % 38.08/5.69 % (56164)------------------------------ % 38.08/5.69 % (56164)------------------------------ % 38.08/5.69 % (56166)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1997329538:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 38.08/5.69 % (56160)Instruction limit reached! % 38.08/5.69 % (56160)------------------------------ % 38.08/5.69 % (56160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 38.08/5.69 % (56160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.08/5.69 % (56160)CaDiCaL version: 2.1.3 % 109.09/15.63 % (56160)Termination reason: Instruction limit % 109.09/15.63 % (56160)Termination phase: Saturation % 109.09/15.63 % (56160)Time elapsed: 0.455 s % 109.09/15.63 % (56160)Peak memory usage: 16 MB % 109.09/15.63 % (56160)Instructions burned: 871 (million) % 109.09/15.63 % (56168)dis+21_1_sil=32000:sas=cadical:random_seed=3084553321:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 109.09/15.63 % (56154)Instruction limit reached! % 109.09/15.63 % (56154)------------------------------ % 109.09/15.63 % (56154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.09/15.63 % (56154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.09/15.63 % (56154)CaDiCaL version: 2.1.3 % 109.09/15.63 % (56154)Termination reason: Instruction limit % 109.09/15.63 % (56154)Termination phase: Saturation % 109.09/15.63 % (56154)Time elapsed: 0.856 s % 109.09/15.63 % (56154)Peak memory usage: 25 MB % 109.09/15.63 % (56154)Instructions burned: 1473 (million) % 109.09/15.63 % (56170)ott+11_1_sil=16000:gs=on:random_seed=1786691365:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 109.09/15.63 % (56152)Instruction limit reached! % 109.09/15.63 % (56152)------------------------------ % 109.09/15.63 % (56152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.09/15.63 % (56152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.09/15.63 % (56152)CaDiCaL version: 2.1.3 % 109.09/15.63 % (56152)Termination reason: Instruction limit % 109.09/15.63 % (56152)Termination phase: Saturation % 109.09/15.63 % (56152)Time elapsed: 1.492 s % 109.09/15.63 % (56152)Peak memory usage: 42 MB % 109.09/15.63 % (56152)Instructions burned: 5134 (million) % 109.09/15.63 % (56172)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3274492350:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 109.09/15.63 % (56172)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 109.09/15.63 % (56172)Terminated due to inappropriate strategy. % 109.09/15.63 % (56172)------------------------------ % 109.09/15.63 % (56172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.09/15.63 % (56172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.09/15.63 % (56172)CaDiCaL version: 2.1.3 % 109.09/15.63 % (56172)Termination reason: Inappropriate % 109.09/15.63 % (56172)Time elapsed: 0.0000 s % 109.09/15.63 % (56172)Peak memory usage: 10 MB % 109.09/15.63 % (56172)Instructions burned: 1 (million) % 109.09/15.63 % (56172)------------------------------ % 109.09/15.63 % (56172)------------------------------ % 109.09/15.63 % (56174)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3799123225:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 109.09/15.63 % (56170)Instruction limit reached! % 109.09/15.63 % (56170)------------------------------ % 109.09/15.63 % (56170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.09/15.63 % (56170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.09/15.63 % (56170)CaDiCaL version: 2.1.3 % 109.09/15.63 % (56170)Termination reason: Instruction limit % 109.09/15.63 % (56170)Termination phase: Saturation % 109.09/15.63 % (56170)Time elapsed: 1.258 s % 109.09/15.63 % (56170)Peak memory usage: 23 MB % 109.09/15.63 % (56170)Instructions burned: 2251 (million) % 109.09/15.63 % (56176)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2119024779:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 109.09/15.63 % (56166)Instruction limit reached! % 109.09/15.63 % (56166)------------------------------ % 109.09/15.63 % (56166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.09/15.63 % (56166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.09/15.63 % (56166)CaDiCaL version: 2.1.3 % 109.09/15.63 % (56166)Termination reason: Instruction limit % 109.09/15.63 % (56166)Termination phase: Saturation % 109.09/15.63 % (56166)Time elapsed: 1.922 s % 109.09/15.63 % (56166)Peak memory usage: 42 MB % 109.09/15.63 % (56166)Instructions burned: 3512 (million) % 109.09/15.63 % (56178)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1911297980:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 109.09/15.63 % (56174)Instruction limit reached! % 109.09/15.63 % (56174)------------------------------ % 109.09/15.63 % (56174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.09/15.63 % (56174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.09/15.63 % (56174)CaDiCaL version: 2.1.3 % 109.09/15.63 % (56174)Termination reason: Instruction limit % 119.99/17.16 % (56174)Termination phase: Saturation % 119.99/17.16 % (56174)Time elapsed: 1.325 s % 119.99/17.16 % (56174)Peak memory usage: 50 MB % 119.99/17.16 % (56174)Instructions burned: 4593 (million) % 119.99/17.16 % (56180)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3152796388:i=5497:nm=2_2967 on theBenchmark for (2967ds/5497Mi) % 119.99/17.16 % (56168)Instruction limit reached! % 119.99/17.16 % (56168)------------------------------ % 119.99/17.16 % (56168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.99/17.16 % (56168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.99/17.16 % (56168)CaDiCaL version: 2.1.3 % 119.99/17.16 % (56168)Termination reason: Instruction limit % 119.99/17.16 % (56168)Termination phase: Saturation % 119.99/17.16 % (56168)Time elapsed: 2.111 s % 119.99/17.16 % (56168)Peak memory usage: 38 MB % 119.99/17.16 % (56168)Instructions burned: 3773 (million) % 119.99/17.16 % (56180)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 119.99/17.16 % (56180)Terminated due to inappropriate strategy. % 119.99/17.16 % (56180)------------------------------ % 119.99/17.16 % (56180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.99/17.16 % (56180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.99/17.16 % (56180)CaDiCaL version: 2.1.3 % 119.99/17.16 % (56180)Termination reason: Inappropriate % 119.99/17.16 % (56180)Time elapsed: 0.0000 s % 119.99/17.16 % (56180)Peak memory usage: 10 MB % 119.99/17.16 % (56180)Instructions burned: 1 (million) % 119.99/17.16 % (56180)------------------------------ % 119.99/17.16 % (56180)------------------------------ % 119.99/17.16 % (56182)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=470448973:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 119.99/17.16 % (56182)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 119.99/17.16 % (56182)Terminated due to inappropriate strategy. % 119.99/17.16 % (56182)------------------------------ % 119.99/17.16 % (56182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.99/17.16 % (56182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.99/17.16 % (56182)CaDiCaL version: 2.1.3 % 119.99/17.16 % (56182)Termination reason: Inappropriate % 119.99/17.16 % (56182)Time elapsed: 0.0000 s % 119.99/17.16 % (56182)Peak memory usage: 10 MB % 119.99/17.16 % (56182)Instructions burned: 1 (million) % 119.99/17.16 % (56182)------------------------------ % 119.99/17.16 % (56182)------------------------------ % 119.99/17.16 % (56185)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3137739478:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 119.99/17.16 % (56183)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=456403404:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 119.99/17.16 % (56183)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 119.99/17.16 % (56183)Terminated due to inappropriate strategy. % 119.99/17.16 % (56183)------------------------------ % 119.99/17.16 % (56183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.99/17.16 % (56183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.99/17.16 % (56183)CaDiCaL version: 2.1.3 % 119.99/17.16 % (56183)Termination reason: Inappropriate % 119.99/17.16 % (56183)Time elapsed: 0.001 s % 119.99/17.16 % (56183)Peak memory usage: 10 MB % 119.99/17.16 % (56183)Instructions burned: 1 (million) % 119.99/17.16 % (56183)------------------------------ % 119.99/17.16 % (56183)------------------------------ % 119.99/17.16 % (56188)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2459467477:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 119.99/17.16 % (56162)Instruction limit reached! % 119.99/17.16 % (56162)------------------------------ % 119.99/17.16 % (56162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.99/17.16 % (56162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.99/17.16 % (56162)CaDiCaL version: 2.1.3 % 119.99/17.16 % (56162)Termination reason: Instruction limit % 119.99/17.16 % (56162)Termination phase: Saturation % 119.99/17.16 % (56162)Time elapsed: 3.249 s % 119.99/17.16 % (56162)Peak memory usage: 33 MB % 119.99/17.16 % (56162)Instructions burned: 5115 (million) % 119.99/17.16 % (56190)dis+10_16:1_sil=16000:random_seed=2896762871:i=9155:fsr=off_2959 on theBenchmark for (2959ds/9155Mi) % 119.99/17.16 % (56178)Instruction limit reached! % 119.99/17.16 % (56178)------------------------------ % 119.99/17.16 % (56178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 119.99/17.16 % (56178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.33/19.39 % (56178)CaDiCaL version: 2.1.3 % 135.33/19.39 % (56178)Termination reason: Instruction limit % 135.33/19.39 % (56178)Termination phase: Saturation % 135.33/19.39 % (56178)Time elapsed: 2.716 s % 135.33/19.39 % (56178)Peak memory usage: 44 MB % 135.33/19.39 % (56178)Instructions burned: 5212 (million) % 135.33/19.39 % (56192)ott-3_8_sil=64000:random_seed=2301917978:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi) % 135.33/19.39 % (56188)Instruction limit reached! % 135.33/19.39 % (56188)------------------------------ % 135.33/19.39 % (56188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.33/19.39 % (56188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.33/19.39 % (56188)CaDiCaL version: 2.1.3 % 135.33/19.39 % (56188)Termination reason: Instruction limit % 135.33/19.39 % (56188)Termination phase: Saturation % 135.33/19.39 % (56188)Time elapsed: 5.080 s % 135.33/19.39 % (56188)Peak memory usage: 53 MB % 135.33/19.39 % (56188)Instructions burned: 8173 (million) % 135.33/19.39 % (56194)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1381276119:fmbsr=2:i=32576_2916 on theBenchmark for (2916ds/32576Mi) % 135.33/19.39 % (56194)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.33/19.39 % (56194)Terminated due to inappropriate strategy. % 135.33/19.39 % (56194)------------------------------ % 135.33/19.39 % (56194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.33/19.39 % (56194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.33/19.39 % (56194)CaDiCaL version: 2.1.3 % 135.33/19.39 % (56194)Termination reason: Inappropriate % 135.33/19.39 % (56194)Time elapsed: 0.001 s % 135.33/19.39 % (56194)Peak memory usage: 10 MB % 135.33/19.39 % (56194)Instructions burned: 1 (million) % 135.33/19.39 % (56194)------------------------------ % 135.33/19.39 % (56194)------------------------------ % 135.33/19.39 % (56196)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1944959838:i=11404_2916 on theBenchmark for (2916ds/11404Mi) % 135.33/19.39 % (56190)Instruction limit reached! % 135.33/19.39 % (56190)------------------------------ % 135.33/19.39 % (56190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.33/19.39 % (56190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.33/19.39 % (56190)CaDiCaL version: 2.1.3 % 135.33/19.39 % (56190)Termination reason: Instruction limit % 135.33/19.39 % (56190)Termination phase: Saturation % 135.33/19.39 % (56190)Time elapsed: 4.665 s % 135.33/19.39 % (56190)Peak memory usage: 53 MB % 135.33/19.39 % (56190)Instructions burned: 9156 (million) % 135.33/19.39 % (56198)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3570241673:i=14134_2913 on theBenchmark for (2913ds/14134Mi) % 135.33/19.39 % (56185)Instruction limit reached! % 135.33/19.39 % (56185)------------------------------ % 135.33/19.39 % (56185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.33/19.39 % (56185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.33/19.39 % (56185)CaDiCaL version: 2.1.3 % 135.33/19.39 % (56185)Termination reason: Instruction limit % 135.33/19.39 % (56185)Termination phase: Saturation % 135.33/19.39 % (56185)Time elapsed: 6.846 s % 135.33/19.39 % (56185)Peak memory usage: 568 MB % 135.33/19.39 % (56185)Instructions burned: 22565 (million) % 135.33/19.39 % (56200)dis+33_16_sil=32000:sac=on:random_seed=4260878994:i=15851:nm=0_2898 on theBenchmark for (2898ds/15851Mi) % 135.33/19.39 % (56200)Instruction limit reached! % 135.33/19.39 % (56200)------------------------------ % 135.33/19.39 % (56200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.33/19.39 % (56200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.33/19.39 % (56200)CaDiCaL version: 2.1.3 % 135.33/19.39 % (56200)Termination reason: Instruction limit % 135.33/19.39 % (56200)Termination phase: Saturation % 135.33/19.39 % (56200)Time elapsed: 3.733 s % 135.33/19.39 % (56200)Peak memory usage: 205 MB % 135.33/19.39 % (56200)Instructions burned: 15852 (million) % 135.33/19.39 % (56202)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3766037667:avsq=on:i=17627:add=on:amm=off_2860 on theBenchmark for (2860ds/17627Mi) % 135.33/19.39 % (56196)Instruction limit reached! % 135.33/19.39 % (56196)------------------------------ % 135.33/19.39 % (56196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.33/19.39 % (56196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.33/19.39 % (56196)CaDiCaL version: 2.1.3 % 135.33/19.39 % (56196)Termination reason: Instruction limit % 135.33/19.39 % (56196)Termination phase: Saturation % 139.50/19.90 % (56196)Time elapsed: 7.005 s % 139.50/19.90 % (56196)Peak memory usage: 61 MB % 139.50/19.90 % (56196)Instructions burned: 11405 (million) % 139.50/19.90 % (56204)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4196131078:s2a=on:i=53295_2845 on theBenchmark for (2845ds/53295Mi) % 139.50/19.90 % (56176)Instruction limit reached! % 139.50/19.90 % (56176)------------------------------ % 139.50/19.90 % (56176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.50/19.90 % (56176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.50/19.90 % (56176)CaDiCaL version: 2.1.3 % 139.50/19.90 % (56176)Termination reason: Instruction limit % 139.50/19.90 % (56176)Termination phase: Saturation % 139.50/19.90 % (56176)Time elapsed: 13.845 s % 139.50/19.90 % (56176)Peak memory usage: 100 MB % 139.50/19.90 % (56176)Instructions burned: 29340 (million) % 139.50/19.90 % (56206)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1456827029:i=26857:ins=20_2835 on theBenchmark for (2835ds/26857Mi) % 139.50/19.90 % (56206)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 139.50/19.90 % (56206)Terminated due to inappropriate strategy. % 139.50/19.90 % (56206)------------------------------ % 139.50/19.90 % (56206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.50/19.90 % (56206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.50/19.90 % (56206)CaDiCaL version: 2.1.3 % 139.50/19.90 % (56206)Termination reason: Inappropriate % 139.50/19.90 % (56206)Time elapsed: 0.001 s % 139.50/19.90 % (56206)Peak memory usage: 10 MB % 139.50/19.90 % (56206)Instructions burned: 1 (million) % 139.50/19.90 % (56206)------------------------------ % 139.50/19.90 % (56206)------------------------------ % 139.50/19.90 % (56208)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1096932749:i=28120:bs=on:fsr=off_2834 on theBenchmark for (2834ds/28120Mi) % 139.50/19.90 % (56192)Instruction limit reached! % 139.50/19.90 % (56192)------------------------------ % 139.50/19.90 % (56192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.50/19.90 % (56192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.50/19.90 % (56192)CaDiCaL version: 2.1.3 % 139.50/19.90 % (56192)Termination reason: Instruction limit % 139.50/19.90 % (56192)Termination phase: Saturation % 139.50/19.90 % (56192)Time elapsed: 11.372 s % 139.50/19.90 % (56192)Peak memory usage: 72 MB % 139.50/19.90 % (56192)Instructions burned: 20140 (million) % 139.50/19.90 % (56210)fmb+10_1_sil=256000:fmbss=7:random_seed=3990008452:fmbsr=1.6:i=182295_2831 on theBenchmark for (2831ds/182295Mi) % 139.50/19.90 % (56210)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 139.50/19.90 % (56210)Terminated due to inappropriate strategy. % 139.50/19.90 % (56210)------------------------------ % 139.50/19.90 % (56210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.50/19.90 % (56210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.50/19.90 % (56210)CaDiCaL version: 2.1.3 % 139.50/19.90 % (56210)Termination reason: Inappropriate % 139.50/19.90 % (56210)Time elapsed: 0.001 s % 139.50/19.90 % (56210)Peak memory usage: 10 MB % 139.50/19.90 % (56210)Instructions burned: 1 (million) % 139.50/19.90 % (56210)------------------------------ % 139.50/19.90 % (56210)------------------------------ % 139.50/19.90 % (56212)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1825634888:i=44625:gsp=on_2831 on theBenchmark for (2831ds/44625Mi) % 139.50/19.90 % (56212)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 139.50/19.90 % (56212)Terminated due to inappropriate strategy. % 139.50/19.90 % (56212)------------------------------ % 139.50/19.90 % (56212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.50/19.90 % (56212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.50/19.90 % (56212)CaDiCaL version: 2.1.3 % 139.50/19.90 % (56212)Termination reason: Inappropriate % 139.50/19.90 % (56212)Time elapsed: 0.001 s % 139.50/19.90 % (56212)Peak memory usage: 10 MB % 139.50/19.90 % (56212)Instructions burned: 1 (million) % 139.50/19.90 % (56212)------------------------------ % 139.50/19.90 % (56212)------------------------------ % 139.50/19.90 % (56214)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=230321696:i=160505_2830 on theBenchmark for (2830ds/160505Mi) % 139.50/19.90 % (56214)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 139.50/19.90 % (56214)Terminated due to inappropriate strategy. % 139.50/19.90 % (56214)------------------------------ % 139.50/19.90 % (56214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.96/21.58 % (56214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.96/21.58 % (56214)CaDiCaL version: 2.1.3 % 150.96/21.58 % (56214)Termination reason: Inappropriate % 150.96/21.58 % (56214)Time elapsed: 0.001 s % 150.96/21.58 % (56214)Peak memory usage: 10 MB % 150.96/21.58 % (56214)Instructions burned: 1 (million) % 150.96/21.58 % (56214)------------------------------ % 150.96/21.58 % (56214)------------------------------ % 150.96/21.58 % (56216)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2813773503:fmbsr=1.3:i=225729_2830 on theBenchmark for (2830ds/225729Mi) % 150.96/21.58 % (56216)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.96/21.58 % (56216)Terminated due to inappropriate strategy. % 150.96/21.58 % (56216)------------------------------ % 150.96/21.58 % (56216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.96/21.58 % (56216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.96/21.58 % (56216)CaDiCaL version: 2.1.3 % 150.96/21.58 % (56216)Termination reason: Inappropriate % 150.96/21.58 % (56216)Time elapsed: 0.001 s % 150.96/21.58 % (56216)Peak memory usage: 10 MB % 150.96/21.58 % (56216)Instructions burned: 1 (million) % 150.96/21.58 % (56216)------------------------------ % 150.96/21.58 % (56216)------------------------------ % 150.96/21.58 % (56218)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=482346113:fmbsr=2:i=185024:ins=7_2830 on theBenchmark for (2830ds/185024Mi) % 150.96/21.58 % (56218)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.96/21.58 % (56218)Terminated due to inappropriate strategy. % 150.96/21.58 % (56218)------------------------------ % 150.96/21.58 % (56218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.96/21.58 % (56218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.96/21.58 % (56218)CaDiCaL version: 2.1.3 % 150.96/21.58 % (56218)Termination reason: Inappropriate % 150.96/21.58 % (56218)Time elapsed: 0.001 s % 150.96/21.58 % (56218)Peak memory usage: 10 MB % 150.96/21.58 % (56218)Instructions burned: 1 (million) % 150.96/21.58 % (56218)------------------------------ % 150.96/21.58 % (56218)------------------------------ % 150.96/21.58 % (56220)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1189984495:rtra=on_2830 on theBenchmark for (2830ds/0Mi) % 150.96/21.58 % (56220)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.96/21.58 % (56220)Terminated due to inappropriate strategy. % 150.96/21.58 % (56220)------------------------------ % 150.96/21.58 % (56220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.96/21.58 % (56220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.96/21.58 % (56220)CaDiCaL version: 2.1.3 % 150.96/21.58 % (56220)Termination reason: Inappropriate % 150.96/21.58 % (56220)Time elapsed: 0.001 s % 150.96/21.58 % (56220)Peak memory usage: 10 MB % 150.96/21.58 % (56220)Instructions burned: 1 (million) % 150.96/21.58 % (56220)------------------------------ % 150.96/21.58 % (56220)------------------------------ % 150.96/21.58 % (56222)% WARNING: option uhcvi not known. % 150.96/21.58 % (56222)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3472465898:i=271062:add=off:rtra=on:rawr=on_2830 on theBenchmark for (2830ds/271062Mi) % 150.96/21.58 % (56198)Instruction limit reached! % 150.96/21.58 % (56198)------------------------------ % 150.96/21.58 % (56198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.96/21.58 % (56198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.96/21.58 % (56198)CaDiCaL version: 2.1.3 % 150.96/21.58 % (56198)Termination reason: Instruction limit % 150.96/21.58 % (56198)Termination phase: Saturation % 150.96/21.58 % (56198)Time elapsed: 8.564 s % 150.96/21.58 % (56198)Peak memory usage: 76 MB % 150.96/21.58 % (56198)Instructions burned: 14135 (million) % 150.96/21.58 % (56224)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3979294449:i=176048:add=on:rtra=on:rawr=on_2827 on theBenchmark for (2827ds/176048Mi) % 150.96/21.58 % (56202)Instruction limit reached! % 150.96/21.58 % (56202)------------------------------ % 150.96/21.58 % (56202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.96/21.58 % (56202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.96/21.58 % (56202)CaDiCaL version: 2.1.3 % 150.96/21.58 % (56202)Termination reason: Instruction limit % 150.96/21.58 % (56202)Termination phase: Saturation % 150.96/21.58 % (56202)Time elapsed: 5.243 s % 158.75/22.63 % (56202)Peak memory usage: 79 MB % 158.75/22.63 % (56202)Instructions burned: 17630 (million) % 158.75/22.63 % (56226)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2763394597:i=206:fgj=on:rtra=on_2808 on theBenchmark for (2808ds/206Mi) % 158.75/22.63 % (56226)Instruction limit reached! % 158.75/22.63 % (56226)------------------------------ % 158.75/22.63 % (56226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.75/22.63 % (56226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.75/22.63 % (56226)CaDiCaL version: 2.1.3 % 158.75/22.63 % (56226)Termination reason: Instruction limit % 158.75/22.63 % (56226)Termination phase: Saturation % 158.75/22.63 % (56226)Time elapsed: 0.068 s % 158.75/22.63 % (56226)Peak memory usage: 14 MB % 158.75/22.63 % (56226)Instructions burned: 208 (million) % 158.75/22.63 % (56228)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4115329699:i=232:rtra=on_2807 on theBenchmark for (2807ds/232Mi) % 158.75/22.63 % (56228)Instruction limit reached! % 158.75/22.63 % (56228)------------------------------ % 158.75/22.63 % (56228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.75/22.63 % (56228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.75/22.63 % (56228)CaDiCaL version: 2.1.3 % 158.75/22.63 % (56228)Termination reason: Instruction limit % 158.75/22.63 % (56228)Termination phase: Saturation % 158.75/22.63 % (56228)Time elapsed: 0.077 s % 158.75/22.63 % (56228)Peak memory usage: 13 MB % 158.75/22.63 % (56228)Instructions burned: 232 (million) % 158.75/22.63 % (56230)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2773582664:i=262:rtra=on_2806 on theBenchmark for (2806ds/262Mi) % 158.75/22.63 % (56230)Instruction limit reached! % 158.75/22.63 % (56230)------------------------------ % 158.75/22.63 % (56230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.75/22.63 % (56230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.75/22.63 % (56230)CaDiCaL version: 2.1.3 % 158.75/22.63 % (56230)Termination reason: Instruction limit % 158.75/22.63 % (56230)Termination phase: Saturation % 158.75/22.63 % (56230)Time elapsed: 0.082 s % 158.75/22.63 % (56230)Peak memory usage: 14 MB % 158.75/22.63 % (56230)Instructions burned: 262 (million) % 158.75/22.63 % (56232)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3003895294:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2805 on theBenchmark for (2805ds/318Mi) % 158.75/22.63 % (56232)Instruction limit reached! % 158.75/22.63 % (56232)------------------------------ % 158.75/22.63 % (56232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.75/22.63 % (56232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.75/22.63 % (56232)CaDiCaL version: 2.1.3 % 158.75/22.63 % (56232)Termination reason: Instruction limit % 158.75/22.63 % (56232)Termination phase: Saturation % 158.75/22.63 % (56232)Time elapsed: 0.117 s % 158.75/22.63 % (56232)Peak memory usage: 15 MB % 158.75/22.63 % (56232)Instructions burned: 320 (million) % 158.75/22.63 % (56234)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3920981783:i=1428:nm=2:rtra=on_2804 on theBenchmark for (2804ds/1428Mi) % 158.75/22.63 % (56234)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.75/22.63 % (56234)Terminated due to inappropriate strategy. % 158.75/22.63 % (56234)------------------------------ % 158.75/22.63 % (56234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.75/22.63 % (56234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.75/22.63 % (56234)CaDiCaL version: 2.1.3 % 158.75/22.63 % (56234)Termination reason: Inappropriate % 158.75/22.63 % (56234)Time elapsed: 0.0000 s % 158.75/22.63 % (56234)Peak memory usage: 10 MB % 158.75/22.63 % (56234)Instructions burned: 1 (million) % 158.75/22.63 % (56234)------------------------------ % 158.75/22.63 % (56234)------------------------------ % 158.75/22.63 % (56236)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2786038347:i=262:bd=preordered:rtra=on:fsd=on_2804 on theBenchmark for (2804ds/262Mi) % 158.75/22.63 % (56236)Instruction limit reached! % 158.75/22.63 % (56236)------------------------------ % 158.75/22.63 % (56236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.75/22.63 % (56236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.75/22.63 % (56236)CaDiCaL version: 2.1.3 % 158.75/22.63 % (56236)Termination reason: Instruction limit % 158.75/22.63 % (56236)Termination phase: Saturation % 158.75/22.63 % (56236)Time elapsed: 0.088 s % 158.75/22.63 % (56236)Peak memory usage: 13 MB % 158.75/22.63 % (56236)Instructions burned: 263 (million) % 211.51/30.05 % (56238)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=225494135:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2803 on theBenchmark for (2803ds/1368Mi) % 211.51/30.05 % (56238)Instruction limit reached! % 211.51/30.05 % (56238)------------------------------ % 211.51/30.05 % (56238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.51/30.05 % (56238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.51/30.05 % (56238)CaDiCaL version: 2.1.3 % 211.51/30.05 % (56238)Termination reason: Instruction limit % 211.51/30.05 % (56238)Termination phase: Saturation % 211.51/30.05 % (56238)Time elapsed: 0.417 s % 211.51/30.05 % (56238)Peak memory usage: 21 MB % 211.51/30.05 % (56238)Instructions burned: 1370 (million) % 211.51/30.05 % (56240)ott-21_1_sil=16000:si=on:fs=off:random_seed=2350238482:i=360:av=off:fsr=off:rtra=on_2798 on theBenchmark for (2798ds/360Mi) % 211.51/30.05 % (56240)Instruction limit reached! % 211.51/30.05 % (56240)------------------------------ % 211.51/30.05 % (56240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.51/30.06 % (56240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.51/30.06 % (56240)CaDiCaL version: 2.1.3 % 211.51/30.06 % (56240)Termination reason: Instruction limit % 211.51/30.06 % (56240)Termination phase: Saturation % 211.51/30.06 % (56240)Time elapsed: 0.084 s % 211.51/30.06 % (56240)Peak memory usage: 13 MB % 211.51/30.06 % (56240)Instructions burned: 360 (million) % 211.51/30.06 % (56242)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2395157065:i=954:bd=all:rtra=on_2798 on theBenchmark for (2798ds/954Mi) % 211.51/30.06 % (56242)Instruction limit reached! % 211.51/30.06 % (56242)------------------------------ % 211.51/30.06 % (56242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.51/30.06 % (56242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.51/30.06 % (56242)CaDiCaL version: 2.1.3 % 211.51/30.06 % (56242)Termination reason: Instruction limit % 211.51/30.06 % (56242)Termination phase: Saturation % 211.51/30.06 % (56242)Time elapsed: 0.339 s % 211.51/30.06 % (56242)Peak memory usage: 16 MB % 211.51/30.06 % (56242)Instructions burned: 954 (million) % 211.51/30.06 % (56244)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3131567222:fmbsr=1.3:i=1730:ins=25:rtra=on_2794 on theBenchmark for (2794ds/1730Mi) % 211.51/30.06 % (56244)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 211.51/30.06 % (56244)Terminated due to inappropriate strategy. % 211.51/30.06 % (56244)------------------------------ % 211.51/30.06 % (56244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.51/30.06 % (56244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.51/30.06 % (56244)CaDiCaL version: 2.1.3 % 211.51/30.06 % (56244)Termination reason: Inappropriate % 211.51/30.06 % (56244)Time elapsed: 0.0000 s % 211.51/30.06 % (56244)Peak memory usage: 10 MB % 211.51/30.06 % (56244)Instructions burned: 1 (million) % 211.51/30.06 % (56244)------------------------------ % 211.51/30.06 % (56244)------------------------------ % 211.51/30.06 % (56246)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1155551846:i=2358:rtra=on_2794 on theBenchmark for (2794ds/2358Mi) % 211.51/30.06 % (56246)Instruction limit reached! % 211.51/30.06 % (56246)------------------------------ % 211.51/30.06 % (56246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.51/30.06 % (56246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.51/30.06 % (56246)CaDiCaL version: 2.1.3 % 211.51/30.06 % (56246)Termination reason: Instruction limit % 211.51/30.06 % (56246)Termination phase: Saturation % 211.51/30.06 % (56246)Time elapsed: 0.766 s % 211.51/30.06 % (56246)Peak memory usage: 23 MB % 211.51/30.06 % (56246)Instructions burned: 2358 (million) % 211.51/30.06 % (56248)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1754962690:i=1778:ins=1:rtra=on_2786 on theBenchmark for (2786ds/1778Mi) % 211.51/30.06 % (56248)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 211.51/30.06 % (56248)Terminated due to inappropriate strategy. % 211.51/30.06 % (56248)------------------------------ % 211.51/30.06 % (56248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.51/30.06 % (56248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.51/30.06 % (56248)CaDiCaL version: 2.1.3 % 211.51/30.06 % (56248)Termination reason: Inappropriate % 211.51/30.06 % (56248)Time elapsed: 0.0000 s % 245.31/34.93 % (56248)Peak memory usage: 10 MB % 245.31/34.93 % (56248)Instructions burned: 1 (million) % 245.31/34.93 % (56248)------------------------------ % 245.31/34.93 % (56248)------------------------------ % 245.31/34.93 % (56250)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=380565798:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2786 on theBenchmark for (2786ds/1384Mi) % 245.31/34.93 % (56250)Instruction limit reached! % 245.31/34.93 % (56250)------------------------------ % 245.31/34.93 % (56250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.31/34.93 % (56250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.31/34.93 % (56250)CaDiCaL version: 2.1.3 % 245.31/34.93 % (56250)Termination reason: Instruction limit % 245.31/34.93 % (56250)Termination phase: Saturation % 245.31/34.93 % (56250)Time elapsed: 0.440 s % 245.31/34.93 % (56250)Peak memory usage: 23 MB % 245.31/34.93 % (56250)Instructions burned: 1384 (million) % 245.31/34.93 % (56252)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=4116867219:i=1758:kws=inv_precedence:fsr=off:rtra=on_2781 on theBenchmark for (2781ds/1758Mi) % 245.31/34.93 % (56252)Instruction limit reached! % 245.31/34.93 % (56252)------------------------------ % 245.31/34.93 % (56252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.31/34.93 % (56252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.31/34.93 % (56252)CaDiCaL version: 2.1.3 % 245.31/34.93 % (56252)Termination reason: Instruction limit % 245.31/34.93 % (56252)Termination phase: Saturation % 245.31/34.93 % (56252)Time elapsed: 0.539 s % 245.31/34.93 % (56252)Peak memory usage: 27 MB % 245.31/34.93 % (56252)Instructions burned: 1760 (million) % 245.31/34.93 % (56254)fmb+10_1_sil=64000:si=on:random_seed=1508433017:i=44122:nm=2:rtra=on:gsp=on_2776 on theBenchmark for (2776ds/44122Mi) % 245.31/34.93 % (56254)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 245.31/34.93 % (56254)Terminated due to inappropriate strategy. % 245.31/34.93 % (56254)------------------------------ % 245.31/34.93 % (56254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.31/34.93 % (56254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.31/34.93 % (56254)CaDiCaL version: 2.1.3 % 245.31/34.93 % (56254)Termination reason: Inappropriate % 245.31/34.93 % (56254)Time elapsed: 0.0000 s % 245.31/34.93 % (56254)Peak memory usage: 10 MB % 245.31/34.93 % (56254)Instructions burned: 1 (million) % 245.31/34.93 % (56254)------------------------------ % 245.31/34.93 % (56254)------------------------------ % 245.31/34.93 % (56256)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1139919425:i=19030:nm=5:rtra=on_2776 on theBenchmark for (2776ds/19030Mi) % 245.31/34.93 % (56256)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 245.31/34.93 % (56256)Terminated due to inappropriate strategy. % 245.31/34.93 % (56256)------------------------------ % 245.31/34.93 % (56256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.31/34.93 % (56256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.31/34.93 % (56256)CaDiCaL version: 2.1.3 % 245.31/34.93 % (56256)Termination reason: Inappropriate % 245.31/34.93 % (56256)Time elapsed: 0.0000 s % 245.31/34.93 % (56256)Peak memory usage: 10 MB % 245.31/34.93 % (56256)Instructions burned: 1 (million) % 245.31/34.93 % (56256)------------------------------ % 245.31/34.93 % (56256)------------------------------ % 245.31/34.93 % (56258)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2113651812:fmbsr=1.7:i=1840:rtra=on_2776 on theBenchmark for (2776ds/1840Mi) % 245.31/34.93 % (56258)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 245.31/34.93 % (56258)Terminated due to inappropriate strategy. % 245.31/34.93 % (56258)------------------------------ % 245.31/34.93 % (56258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.31/34.93 % (56258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.31/34.93 % (56258)CaDiCaL version: 2.1.3 % 245.31/34.93 % (56258)Termination reason: Inappropriate % 245.31/34.93 % (56258)Time elapsed: 0.0000 s % 245.31/34.93 % (56258)Peak memory usage: 10 MB % 245.31/34.93 % (56258)Instructions burned: 1 (million) % 245.31/34.93 % (56258)------------------------------ % 245.31/34.93 % (56258)------------------------------ % 245.31/34.93 % (56260)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3600297355:i=10262:rtra=on_2776 on theBenchmark for (2776ds/10262Mi) % 274.46/38.91 % (56260)Instruction limit reached! % 274.46/38.91 % (56260)------------------------------ % 274.46/38.91 % (56260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.46/38.91 % (56260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.46/38.91 % (56260)CaDiCaL version: 2.1.3 % 274.46/38.91 % (56260)Termination reason: Instruction limit % 274.46/38.91 % (56260)Termination phase: Saturation % 274.46/38.91 % (56260)Time elapsed: 3.191 s % 274.46/38.91 % (56260)Peak memory usage: 70 MB % 274.46/38.91 % (56260)Instructions burned: 10264 (million) % 274.46/38.91 % (56262)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=362406687:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2744 on theBenchmark for (2744ds/2944Mi) % 274.46/38.91 % (56262)Instruction limit reached! % 274.46/38.91 % (56262)------------------------------ % 274.46/38.91 % (56262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.46/38.91 % (56262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.46/38.91 % (56262)CaDiCaL version: 2.1.3 % 274.46/38.91 % (56262)Termination reason: Instruction limit % 274.46/38.91 % (56262)Termination phase: Saturation % 274.46/38.91 % (56262)Time elapsed: 0.891 s % 274.46/38.91 % (56262)Peak memory usage: 65 MB % 274.46/38.91 % (56262)Instructions burned: 2944 (million) % 274.46/38.91 % (56264)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=972482933:i=12648:rtra=on_2734 on theBenchmark for (2734ds/12648Mi) % 274.46/38.91 % (56264)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 274.46/38.91 % (56264)Terminated due to inappropriate strategy. % 274.46/38.91 % (56264)------------------------------ % 274.46/38.91 % (56264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.46/38.91 % (56264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.46/38.91 % (56264)CaDiCaL version: 2.1.3 % 274.46/38.91 % (56264)Termination reason: Inappropriate % 274.46/38.91 % (56264)Time elapsed: 0.0000 s % 274.46/38.91 % (56264)Peak memory usage: 10 MB % 274.46/38.91 % (56264)Instructions burned: 1 (million) % 274.46/38.91 % (56264)------------------------------ % 274.46/38.91 % (56264)------------------------------ % 274.46/38.91 % (56266)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1814368901:fmbsr=2.30978:i=4348:rtra=on_2734 on theBenchmark for (2734ds/4348Mi) % 274.46/38.91 % (56266)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 274.46/38.91 % (56266)Terminated due to inappropriate strategy. % 274.46/38.91 % (56266)------------------------------ % 274.46/38.91 % (56266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.46/38.91 % (56266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.46/38.91 % (56266)CaDiCaL version: 2.1.3 % 274.46/38.91 % (56266)Termination reason: Inappropriate % 274.46/38.91 % (56266)Time elapsed: 0.0000 s % 274.46/38.91 % (56266)Peak memory usage: 10 MB % 274.46/38.91 % (56266)Instructions burned: 1 (million) % 274.46/38.91 % (56266)------------------------------ % 274.46/38.91 % (56266)------------------------------ % 274.46/38.91 % (56268)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=4108207090:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2734 on theBenchmark for (2734ds/1738Mi) % 274.46/38.91 % (56268)Instruction limit reached! % 274.46/38.91 % (56268)------------------------------ % 274.46/38.91 % (56268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.46/38.91 % (56268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.46/38.91 % (56268)CaDiCaL version: 2.1.3 % 274.46/38.91 % (56268)Termination reason: Instruction limit % 274.46/38.91 % (56268)Termination phase: Saturation % 274.46/38.91 % (56268)Time elapsed: 0.531 s % 274.46/38.91 % (56268)Peak memory usage: 20 MB % 274.46/38.91 % (56268)Instructions burned: 1739 (million) % 274.46/38.91 % (56270)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2700379318:i=10228:av=off:rtra=on_2729 on theBenchmark for (2729ds/10228Mi) % 274.46/38.91 % (56208)Instruction limit reached! % 274.46/38.91 % (56208)------------------------------ % 274.46/38.91 % (56208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.46/38.91 % (56208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.46/38.91 % (56208)CaDiCaL version: 2.1.3 % 274.46/38.91 % (56208)Termination reason: Instruction limit % 274.46/38.91 % (56208)Termination phase: Saturation % 274.46/38.91 % (56208)Time elapsed: 13.305 s % 274.46/38.91 % (56208)Peak memory usage: 36 MB % 300.03/42.54 Terminated % 300.03/42.54 % Vampire exiting % 300.03/42.54 Terminated %------------------------------------------------------------------------------