%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX144_1 : TPTP v9.3.1. Released v9.3.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:46:33 PM UTC 2026 % Result : Timeout 289.83s 41.35s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX144_1 : TPTP v9.3.1. Released v9.3.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.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Mon Sep 28 15:05:20 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 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.74/1.10 % (228359)Will run a generic schedule for satisfiability detection. % 3.74/1.10 % (228367)dis+10_1_sil=32000:sp=arity:random_seed=826352681:i=103:fgj=on_2996 on theBenchmark for (2996ds/103Mi) % 3.74/1.10 % (228365)% WARNING: option uhcvi not known. % 3.74/1.10 % (228364)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4120859260_2996 on theBenchmark for (2996ds/0Mi) % 3.74/1.10 % (228365)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3860950344:i=135531:add=off:rawr=on_2996 on theBenchmark for (2996ds/135531Mi) % 3.74/1.10 % (228366)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4099359714:i=88024:add=on:rawr=on_2996 on theBenchmark for (2996ds/88024Mi) % 3.74/1.10 % (228368)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2055785782:i=116_2996 on theBenchmark for (2996ds/116Mi) % 3.74/1.10 % (228369)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=522045797:i=131_2996 on theBenchmark for (2996ds/131Mi) % 3.74/1.10 % (228370)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2191953469:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2996 on theBenchmark for (2996ds/159Mi) % 3.74/1.10 % (228367)Instruction limit reached! % 3.74/1.10 % (228367)------------------------------ % 3.74/1.10 % (228367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.74/1.10 % (228367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.74/1.10 % (228367)CaDiCaL version: 2.1.3 % 3.74/1.10 % (228367)Termination reason: Instruction limit % 3.74/1.10 % (228367)Termination phase: Property scanning % 3.74/1.10 % (228367)Time elapsed: 0.022 s % 3.74/1.10 % (228367)Peak memory usage: 10 MB % 3.74/1.10 % (228367)Instructions burned: 103 (million) % 3.74/1.10 % (228378)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4012990017:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi) % 3.74/1.10 % (228368)Instruction limit reached! % 3.74/1.10 % (228368)------------------------------ % 3.74/1.10 % (228368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.74/1.10 % (228368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.74/1.10 % (228368)CaDiCaL version: 2.1.3 % 3.74/1.10 % (228368)Termination reason: Instruction limit % 3.74/1.10 % (228368)Termination phase: Property scanning % 3.74/1.10 % (228368)Time elapsed: 0.047 s % 3.74/1.10 % (228368)Peak memory usage: 10 MB % 3.74/1.10 % (228368)Instructions burned: 118 (million) % 3.74/1.10 % (228369)Instruction limit reached! % 3.74/1.10 % (228369)------------------------------ % 3.74/1.10 % (228369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.74/1.10 % (228369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.74/1.10 % (228369)CaDiCaL version: 2.1.3 % 3.74/1.10 % (228369)Termination reason: Instruction limit % 3.74/1.10 % (228369)Termination phase: Property scanning % 3.74/1.10 % (228369)Time elapsed: 0.052 s % 3.74/1.10 % (228369)Peak memory usage: 10 MB % 3.74/1.10 % (228369)Instructions burned: 131 (million) % 3.74/1.10 % (228370)Instruction limit reached! % 3.74/1.10 % (228370)------------------------------ % 3.74/1.10 % (228370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.74/1.10 % (228370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.74/1.10 % (228370)CaDiCaL version: 2.1.3 % 3.74/1.10 % (228370)Termination reason: Instruction limit % 3.74/1.10 % (228370)Termination phase: Property scanning % 3.74/1.10 % (228370)Time elapsed: 0.064 s % 3.74/1.10 % (228370)Peak memory usage: 10 MB % 3.74/1.10 % (228370)Instructions burned: 162 (million) % 3.74/1.10 % (228380)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1163161566:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi) % 3.74/1.10 % (228381)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=466681315:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi) % 3.74/1.10 % (228382)ott-21_1_sil=16000:fs=off:random_seed=2778544020:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi) % 3.74/1.10 % (228380)Instruction limit reached! % 3.74/1.10 % (228380)------------------------------ % 3.74/1.10 % (228380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.74/1.10 % (228380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.74/1.10 % (228380)CaDiCaL version: 2.1.3 % 3.74/1.10 % (228380)Termination reason: Instruction limit % 6.00/1.62 % (228380)Termination phase: Property scanning % 6.00/1.62 % (228380)Time elapsed: 0.052 s % 6.00/1.62 % (228380)Peak memory usage: 10 MB % 6.00/1.62 % (228380)Instructions burned: 132 (million) % 6.00/1.62 % (228378)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.00/1.62 % (228378)Terminated due to inappropriate strategy. % 6.00/1.62 % (228378)------------------------------ % 6.00/1.62 % (228378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.00/1.62 % (228378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.00/1.62 % (228378)CaDiCaL version: 2.1.3 % 6.00/1.62 % (228378)Termination reason: Inappropriate % 6.00/1.62 % (228378)Time elapsed: 0.094 s % 6.00/1.62 % (228378)Peak memory usage: 11 MB % 6.00/1.62 % (228378)Instructions burned: 467 (million) % 6.00/1.62 % (228378)------------------------------ % 6.00/1.62 % (228378)------------------------------ % 6.00/1.62 % (228387)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=66434851:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 6.00/1.62 % (228386)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4289454845:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi) % 6.00/1.62 % (228382)Instruction limit reached! % 6.00/1.62 % (228382)------------------------------ % 6.00/1.62 % (228382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.00/1.62 % (228382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.00/1.62 % (228382)CaDiCaL version: 2.1.3 % 6.00/1.62 % (228382)Termination reason: Instruction limit % 6.00/1.62 % (228382)Termination phase: Property scanning % 6.00/1.62 % (228382)Time elapsed: 0.071 s % 6.00/1.62 % (228382)Peak memory usage: 10 MB % 6.00/1.62 % (228382)Instructions burned: 182 (million) % 6.00/1.62 % (228390)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3432816005:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 6.00/1.62 % (228364)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.00/1.62 % (228364)Terminated due to inappropriate strategy. % 6.00/1.62 % (228364)------------------------------ % 6.00/1.62 % (228364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.00/1.62 % (228364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.00/1.62 % (228364)CaDiCaL version: 2.1.3 % 6.00/1.62 % (228364)Termination reason: Inappropriate % 6.00/1.62 % (228364)Time elapsed: 0.177 s % 6.00/1.62 % (228364)Peak memory usage: 11 MB % 6.00/1.62 % (228364)Instructions burned: 467 (million) % 6.00/1.62 % (228364)------------------------------ % 6.00/1.62 % (228364)------------------------------ % 6.00/1.62 % (228392)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=777266074:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 6.00/1.62 % (228387)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.00/1.62 % (228387)Terminated due to inappropriate strategy. % 6.00/1.62 % (228387)------------------------------ % 6.00/1.62 % (228387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.00/1.62 % (228387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.00/1.62 % (228387)CaDiCaL version: 2.1.3 % 6.00/1.62 % (228387)Termination reason: Inappropriate % 6.00/1.62 % (228387)Time elapsed: 0.072 s % 6.00/1.62 % (228387)Peak memory usage: 11 MB % 6.00/1.62 % (228387)Instructions burned: 354 (million) % 6.00/1.62 % (228387)------------------------------ % 6.00/1.62 % (228387)------------------------------ % 6.00/1.62 % (228394)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=2878071620:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 6.00/1.62 % (228386)Instruction limit reached! % 6.00/1.62 % (228386)------------------------------ % 6.00/1.62 % (228386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.00/1.62 % (228386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.00/1.62 % (228386)CaDiCaL version: 2.1.3 % 6.00/1.62 % (228386)Termination reason: Instruction limit % 6.00/1.62 % (228386)Termination phase: Saturation % 6.00/1.62 % (228386)Time elapsed: 0.182 s % 6.00/1.62 % (228386)Peak memory usage: 12 MB % 6.00/1.62 % (228386)Instructions burned: 479 (million) % 6.00/1.62 % (228392)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.15/3.14 % (228392)Terminated due to inappropriate strategy. % 18.15/3.14 % (228392)------------------------------ % 18.15/3.14 % (228392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.15/3.14 % (228392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.15/3.14 % (228392)CaDiCaL version: 2.1.3 % 18.15/3.14 % (228392)Termination reason: Inappropriate % 18.15/3.14 % (228392)Time elapsed: 0.135 s % 18.15/3.14 % (228392)Peak memory usage: 11 MB % 18.15/3.14 % (228392)Instructions burned: 354 (million) % 18.15/3.14 % (228392)------------------------------ % 18.15/3.14 % (228392)------------------------------ % 18.15/3.14 % (228381)Instruction limit reached! % 18.15/3.14 % (228381)------------------------------ % 18.15/3.14 % (228381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.15/3.14 % (228381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.15/3.14 % (228381)CaDiCaL version: 2.1.3 % 18.15/3.14 % (228381)Termination reason: Instruction limit % 18.15/3.14 % (228381)Termination phase: Saturation % 18.15/3.14 % (228381)Time elapsed: 0.264 s % 18.15/3.14 % (228381)Peak memory usage: 13 MB % 18.15/3.14 % (228381)Instructions burned: 686 (million) % 18.15/3.14 % (228396)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1966723874:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 18.15/3.14 % (228397)fmb+10_1_sil=64000:random_seed=2908409349:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 18.15/3.14 % (228398)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2678641373:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi) % 18.15/3.14 % (228394)Instruction limit reached! % 18.15/3.14 % (228394)------------------------------ % 18.15/3.14 % (228394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.15/3.14 % (228394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.15/3.14 % (228394)CaDiCaL version: 2.1.3 % 18.15/3.14 % (228394)Termination reason: Instruction limit % 18.15/3.14 % (228394)Termination phase: Saturation % 18.15/3.14 % (228394)Time elapsed: 0.142 s % 18.15/3.14 % (228394)Peak memory usage: 13 MB % 18.15/3.14 % (228394)Instructions burned: 696 (million) % 18.15/3.14 % (228402)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3298758307:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 18.15/3.14 % (228402)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.15/3.14 % (228402)Terminated due to inappropriate strategy. % 18.15/3.14 % (228402)------------------------------ % 18.15/3.14 % (228402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.15/3.14 % (228402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.15/3.14 % (228402)CaDiCaL version: 2.1.3 % 18.15/3.14 % (228402)Termination reason: Inappropriate % 18.15/3.14 % (228402)Time elapsed: 0.093 s % 18.15/3.14 % (228402)Peak memory usage: 11 MB % 18.15/3.14 % (228402)Instructions burned: 467 (million) % 18.15/3.14 % (228402)------------------------------ % 18.15/3.14 % (228402)------------------------------ % 18.15/3.14 % (228404)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3675707598:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 18.15/3.14 % (228397)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.15/3.14 % (228397)Terminated due to inappropriate strategy. % 18.15/3.14 % (228397)------------------------------ % 18.15/3.14 % (228397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.15/3.14 % (228397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.15/3.14 % (228397)CaDiCaL version: 2.1.3 % 18.15/3.14 % (228397)Termination reason: Inappropriate % 18.15/3.14 % (228397)Time elapsed: 0.177 s % 18.15/3.14 % (228397)Peak memory usage: 11 MB % 18.15/3.14 % (228397)Instructions burned: 467 (million) % 18.15/3.14 % (228397)------------------------------ % 18.15/3.14 % (228397)------------------------------ % 18.15/3.14 % (228398)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.15/3.14 % (228398)Terminated due to inappropriate strategy. % 18.15/3.14 % (228398)------------------------------ % 18.15/3.14 % (228398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.15/3.14 % (228398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.15/3.14 % (228398)CaDiCaL version: 2.1.3 % 18.15/3.14 % (228398)Termination reason: Inappropriate % 18.15/3.14 % (228398)Time elapsed: 0.177 s % 18.15/3.14 % (228398)Peak memory usage: 11 MB % 22.42/3.81 % (228398)Instructions burned: 467 (million) % 22.42/3.81 % (228398)------------------------------ % 22.42/3.81 % (228398)------------------------------ % 22.42/3.81 % (228406)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4103433904:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 22.42/3.81 % (228407)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2495432301:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 22.42/3.81 % (228390)Instruction limit reached! % 22.42/3.81 % (228390)------------------------------ % 22.42/3.81 % (228390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.42/3.81 % (228390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.42/3.81 % (228390)CaDiCaL version: 2.1.3 % 22.42/3.81 % (228390)Termination reason: Instruction limit % 22.42/3.81 % (228390)Termination phase: Saturation % 22.42/3.81 % (228390)Time elapsed: 0.471 s % 22.42/3.81 % (228390)Peak memory usage: 18 MB % 22.42/3.81 % (228390)Instructions burned: 1181 (million) % 22.42/3.81 % (228410)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=689035948:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 22.42/3.81 % (228396)Instruction limit reached! % 22.42/3.81 % (228396)------------------------------ % 22.42/3.81 % (228396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.42/3.81 % (228396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.42/3.81 % (228396)CaDiCaL version: 2.1.3 % 22.42/3.81 % (228396)Termination reason: Instruction limit % 22.42/3.81 % (228396)Termination phase: Saturation % 22.42/3.81 % (228396)Time elapsed: 0.350 s % 22.42/3.81 % (228396)Peak memory usage: 15 MB % 22.42/3.81 % (228396)Instructions burned: 880 (million) % 22.42/3.81 % (228412)ott-2_1_sil=16000:newcnf=on:random_seed=1177874038:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 22.42/3.81 % (228407)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.42/3.81 % (228407)Terminated due to inappropriate strategy. % 22.42/3.81 % (228407)------------------------------ % 22.42/3.81 % (228407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.42/3.81 % (228407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.42/3.81 % (228407)CaDiCaL version: 2.1.3 % 22.42/3.81 % (228407)Termination reason: Inappropriate % 22.42/3.81 % (228407)Time elapsed: 0.177 s % 22.42/3.81 % (228407)Peak memory usage: 11 MB % 22.42/3.81 % (228407)Instructions burned: 467 (million) % 22.42/3.81 % (228407)------------------------------ % 22.42/3.81 % (228407)------------------------------ % 22.42/3.81 % (228414)ott+10_1_sil=32000:tgt=ground:random_seed=3134273278:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 22.42/3.81 % (228410)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.42/3.81 % (228410)Terminated due to inappropriate strategy. % 22.42/3.81 % (228410)------------------------------ % 22.42/3.81 % (228410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.42/3.81 % (228410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.42/3.81 % (228410)CaDiCaL version: 2.1.3 % 22.42/3.81 % (228410)Termination reason: Inappropriate % 22.42/3.81 % (228410)Time elapsed: 0.177 s % 22.42/3.81 % (228410)Peak memory usage: 11 MB % 22.42/3.81 % (228410)Instructions burned: 467 (million) % 22.42/3.81 % (228410)------------------------------ % 22.42/3.81 % (228410)------------------------------ % 22.42/3.81 % (228416)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=876415222:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 22.42/3.81 % (228416)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.42/3.81 % (228416)Terminated due to inappropriate strategy. % 22.42/3.81 % (228416)------------------------------ % 22.42/3.81 % (228416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.42/3.81 % (228416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.42/3.81 % (228416)CaDiCaL version: 2.1.3 % 22.42/3.81 % (228416)Termination reason: Inappropriate % 22.42/3.81 % (228416)Time elapsed: 0.177 s % 22.42/3.81 % (228416)Peak memory usage: 11 MB % 22.42/3.81 % (228416)Instructions burned: 467 (million) % 22.42/3.81 % (228416)------------------------------ % 22.42/3.81 % (228416)------------------------------ % 22.42/3.81 % (228418)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2272197886:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi) % 118.81/17.28 % (228412)Instruction limit reached! % 118.81/17.28 % (228412)------------------------------ % 118.81/17.28 % (228412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.81/17.28 % (228412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.81/17.28 % (228412)CaDiCaL version: 2.1.3 % 118.81/17.28 % (228412)Termination reason: Instruction limit % 118.81/17.28 % (228412)Termination phase: Saturation % 118.81/17.28 % (228412)Time elapsed: 0.368 s % 118.81/17.28 % (228412)Peak memory usage: 17 MB % 118.81/17.28 % (228412)Instructions burned: 870 (million) % 118.81/17.28 % (228420)dis+21_1_sil=32000:sas=cadical:random_seed=2401261327:i=3773:amm=off_2985 on theBenchmark for (2985ds/3773Mi) % 118.81/17.28 % (228406)Instruction limit reached! % 118.81/17.28 % (228406)------------------------------ % 118.81/17.28 % (228406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.81/17.28 % (228406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.81/17.28 % (228406)CaDiCaL version: 2.1.3 % 118.81/17.28 % (228406)Termination reason: Instruction limit % 118.81/17.28 % (228406)Termination phase: Saturation % 118.81/17.28 % (228406)Time elapsed: 0.597 s % 118.81/17.28 % (228406)Peak memory usage: 18 MB % 118.81/17.28 % (228406)Instructions burned: 1475 (million) % 118.81/17.28 % (228422)ott+11_1_sil=16000:gs=on:random_seed=61095454:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2985 on theBenchmark for (2985ds/2251Mi) % 118.81/17.28 % (228404)Instruction limit reached! % 118.81/17.28 % (228404)------------------------------ % 118.81/17.28 % (228404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.81/17.28 % (228404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.81/17.28 % (228404)CaDiCaL version: 2.1.3 % 118.81/17.28 % (228404)Termination reason: Instruction limit % 118.81/17.28 % (228404)Termination phase: Saturation % 118.81/17.28 % (228404)Time elapsed: 1.201 s % 118.81/17.28 % (228404)Peak memory usage: 21 MB % 118.81/17.28 % (228404)Instructions burned: 5133 (million) % 118.81/17.28 % (228495)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3223011112:fmbsr=1.6:i=67534_2979 on theBenchmark for (2979ds/67534Mi) % 118.81/17.28 % (228495)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 118.81/17.28 % (228495)Terminated due to inappropriate strategy. % 118.81/17.28 % (228495)------------------------------ % 118.81/17.28 % (228495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.81/17.28 % (228495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.81/17.28 % (228495)CaDiCaL version: 2.1.3 % 118.81/17.28 % (228495)Termination reason: Inappropriate % 118.81/17.28 % (228495)Time elapsed: 0.095 s % 118.81/17.28 % (228495)Peak memory usage: 11 MB % 118.81/17.28 % (228495)Instructions burned: 467 (million) % 118.81/17.28 % (228495)------------------------------ % 118.81/17.28 % (228495)------------------------------ % 118.81/17.28 % (228497)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2851535132:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2978 on theBenchmark for (2978ds/4591Mi) % 118.81/17.28 % (228422)Instruction limit reached! % 118.81/17.28 % (228422)------------------------------ % 118.81/17.28 % (228422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.81/17.28 % (228422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.81/17.28 % (228422)CaDiCaL version: 2.1.3 % 118.81/17.28 % (228422)Termination reason: Instruction limit % 118.81/17.28 % (228422)Termination phase: Saturation % 118.81/17.28 % (228422)Time elapsed: 0.881 s % 118.81/17.28 % (228422)Peak memory usage: 19 MB % 118.81/17.28 % (228422)Instructions burned: 2251 (million) % 118.81/17.28 % (228499)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4199394797:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 118.81/17.28 % (228418)Instruction limit reached! % 118.81/17.28 % (228418)------------------------------ % 118.81/17.28 % (228418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 118.81/17.28 % (228418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.81/17.28 % (228418)CaDiCaL version: 2.1.3 % 118.81/17.28 % (228418)Termination reason: Instruction limit % 118.81/17.28 % (228418)Termination phase: Saturation % 118.81/17.28 % (228418)Time elapsed: 1.497 s % 118.81/17.28 % (228418)Peak memory usage: 20 MB % 118.81/17.28 % (228418)Instructions burned: 3512 (million) % 118.81/17.28 % (228630)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=101568486:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 148.52/21.50 % (228420)Instruction limit reached! % 148.52/21.50 % (228420)------------------------------ % 148.52/21.50 % (228420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.52/21.50 % (228420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.52/21.50 % (228420)CaDiCaL version: 2.1.3 % 148.52/21.50 % (228420)Termination reason: Instruction limit % 148.52/21.50 % (228420)Termination phase: Saturation % 148.52/21.50 % (228420)Time elapsed: 1.734 s % 148.52/21.50 % (228420)Peak memory usage: 19 MB % 148.52/21.50 % (228420)Instructions burned: 3773 (million) % 148.52/21.50 % (228660)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3291099189:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 148.52/21.50 % (228414)Instruction limit reached! % 148.52/21.50 % (228414)------------------------------ % 148.52/21.50 % (228414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.52/21.50 % (228414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.52/21.50 % (228414)CaDiCaL version: 2.1.3 % 148.52/21.50 % (228414)Termination reason: Instruction limit % 148.52/21.50 % (228414)Termination phase: Saturation % 148.52/21.50 % (228414)Time elapsed: 2.116 s % 148.52/21.50 % (228414)Peak memory usage: 29 MB % 148.52/21.50 % (228414)Instructions burned: 5114 (million) % 148.52/21.50 % (228663)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2381995791:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 148.52/21.50 % (228497)Instruction limit reached! % 148.52/21.50 % (228497)------------------------------ % 148.52/21.50 % (228497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.52/21.50 % (228497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.52/21.50 % (228497)CaDiCaL version: 2.1.3 % 148.52/21.50 % (228497)Termination reason: Instruction limit % 148.52/21.50 % (228497)Termination phase: Saturation % 148.52/21.50 % (228497)Time elapsed: 1.215 s % 148.52/21.50 % (228497)Peak memory usage: 18 MB % 148.52/21.50 % (228497)Instructions burned: 4591 (million) % 148.52/21.50 % (228672)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1272233136:i=14071_2966 on theBenchmark for (2966ds/14071Mi) % 148.52/21.50 % (228663)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.52/21.50 % (228663)Terminated due to inappropriate strategy. % 148.52/21.50 % (228663)------------------------------ % 148.52/21.50 % (228663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.52/21.50 % (228663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.52/21.50 % (228663)CaDiCaL version: 2.1.3 % 148.52/21.50 % (228663)Termination reason: Inappropriate % 148.52/21.50 % (228663)Time elapsed: 0.301 s % 148.52/21.50 % (228663)Peak memory usage: 11 MB % 148.52/21.50 % (228663)Instructions burned: 467 (million) % 148.52/21.50 % (228672)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.52/21.50 % (228672)Terminated due to inappropriate strategy. % 148.52/21.50 % (228672)------------------------------ % 148.52/21.50 % (228672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.52/21.50 % (228672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.52/21.50 % (228672)CaDiCaL version: 2.1.3 % 148.52/21.50 % (228672)Termination reason: Inappropriate % 148.52/21.50 % (228672)Time elapsed: 0.183 s % 148.52/21.50 % (228672)Peak memory usage: 11 MB % 148.52/21.50 % (228672)Instructions burned: 467 (million) % 148.52/21.50 % (228672)------------------------------ % 148.52/21.50 % (228672)------------------------------ % 148.52/21.50 % (228663)------------------------------ % 148.52/21.50 % (228663)------------------------------ % 148.52/21.50 % (228681)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1417573882:i=22565:add=on:rawr=on_2964 on theBenchmark for (2964ds/22565Mi) % 148.52/21.50 % (228660)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.52/21.50 % (228660)Terminated due to inappropriate strategy. % 148.52/21.50 % (228660)------------------------------ % 148.52/21.50 % (228660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.52/21.50 % (228660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.52/21.50 % (228660)CaDiCaL version: 2.1.3 % 148.52/21.50 % (228660)Termination reason: Inappropriate % 148.52/21.50 % (228660)Time elapsed: 0.378 s % 148.52/21.50 % (228660)Peak memory usage: 11 MB % 148.52/21.50 % (228660)Instructions burned: 467 (million) % 148.52/21.50 % (228682)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3875329165:i=8173:av=off_2964 on theBenchmark for (2964ds/8173Mi) % 165.60/23.86 % (228660)------------------------------ % 165.60/23.86 % (228660)------------------------------ % 165.60/23.86 % (228685)dis+10_16:1_sil=16000:random_seed=3470274247:i=9155:fsr=off_2964 on theBenchmark for (2964ds/9155Mi) % 165.60/23.86 % (228630)Instruction limit reached! % 165.60/23.86 % (228630)------------------------------ % 165.60/23.86 % (228630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.60/23.86 % (228630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.60/23.86 % (228630)CaDiCaL version: 2.1.3 % 165.60/23.86 % (228630)Termination reason: Instruction limit % 165.60/23.86 % (228630)Termination phase: Saturation % 165.60/23.86 % (228630)Time elapsed: 4.050 s % 165.60/23.86 % (228630)Peak memory usage: 21 MB % 165.60/23.86 % (228630)Instructions burned: 5212 (million) % 165.60/23.86 % (228713)ott-3_8_sil=64000:random_seed=1073235682:i=20139:bs=on_2930 on theBenchmark for (2930ds/20139Mi) % 165.60/23.86 % (228682)Instruction limit reached! % 165.60/23.86 % (228682)------------------------------ % 165.60/23.86 % (228682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.60/23.86 % (228682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.60/23.86 % (228682)CaDiCaL version: 2.1.3 % 165.60/23.86 % (228682)Termination reason: Instruction limit % 165.60/23.86 % (228682)Termination phase: Saturation % 165.60/23.86 % (228682)Time elapsed: 5.400 s % 165.60/23.86 % (228682)Peak memory usage: 29 MB % 165.60/23.86 % (228682)Instructions burned: 8174 (million) % 165.60/23.86 % (228727)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4064808648:fmbsr=2:i=32576_2910 on theBenchmark for (2910ds/32576Mi) % 165.60/23.86 % (228727)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 165.60/23.86 % (228727)Terminated due to inappropriate strategy. % 165.60/23.86 % (228727)------------------------------ % 165.60/23.86 % (228727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.60/23.86 % (228727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.60/23.86 % (228727)CaDiCaL version: 2.1.3 % 165.60/23.86 % (228727)Termination reason: Inappropriate % 165.60/23.86 % (228727)Time elapsed: 0.266 s % 165.60/23.86 % (228727)Peak memory usage: 11 MB % 165.60/23.86 % (228727)Instructions burned: 467 (million) % 165.60/23.86 % (228727)------------------------------ % 165.60/23.86 % (228727)------------------------------ % 165.60/23.86 % (228729)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=314486578:i=11404_2907 on theBenchmark for (2907ds/11404Mi) % 165.60/23.86 % (228685)Instruction limit reached! % 165.60/23.86 % (228685)------------------------------ % 165.60/23.86 % (228685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.60/23.86 % (228685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.60/23.86 % (228685)CaDiCaL version: 2.1.3 % 165.60/23.86 % (228685)Termination reason: Instruction limit % 165.60/23.86 % (228685)Termination phase: Saturation % 165.60/23.86 % (228685)Time elapsed: 6.764 s % 165.60/23.86 % (228685)Peak memory usage: 22 MB % 165.60/23.86 % (228685)Instructions burned: 9156 (million) % 165.60/23.86 % (228732)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3421374199:i=14134_2896 on theBenchmark for (2896ds/14134Mi) % 165.60/23.86 % (228681)Instruction limit reached! % 165.60/23.86 % (228681)------------------------------ % 165.60/23.86 % (228681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.60/23.86 % (228681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.60/23.86 % (228681)CaDiCaL version: 2.1.3 % 165.60/23.86 % (228681)Termination reason: Instruction limit % 165.60/23.86 % (228681)Termination phase: Saturation % 165.60/23.86 % (228681)Time elapsed: 7.931 s % 165.60/23.86 % (228681)Peak memory usage: 17 MB % 165.60/23.86 % (228681)Instructions burned: 22566 (million) % 165.60/23.86 % (228740)dis+33_16_sil=32000:sac=on:random_seed=1326532104:i=15851:nm=0_2884 on theBenchmark for (2884ds/15851Mi) % 165.60/23.86 % (228729)Instruction limit reached! % 165.60/23.86 % (228729)------------------------------ % 165.60/23.86 % (228729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.60/23.86 % (228729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.60/23.86 % (228729)CaDiCaL version: 2.1.3 % 165.60/23.86 % (228729)Termination reason: Instruction limit % 165.60/23.86 % (228729)Termination phase: Saturation % 165.60/23.86 % (228729)Time elapsed: 7.734 s % 165.60/23.86 % (228729)Peak memory usage: 29 MB % 165.60/23.86 % (228729)Instructions burned: 11405 (million) % 227.12/32.51 % (228746)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1376749049:avsq=on:i=17627:add=on:amm=off_2829 on theBenchmark for (2829ds/17627Mi) % 227.12/32.51 % (228740)Instruction limit reached! % 227.12/32.51 % (228740)------------------------------ % 227.12/32.51 % (228740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.12/32.51 % (228740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.12/32.51 % (228740)CaDiCaL version: 2.1.3 % 227.12/32.51 % (228740)Termination reason: Instruction limit % 227.12/32.51 % (228740)Termination phase: Saturation % 227.12/32.51 % (228740)Time elapsed: 6.448 s % 227.12/32.51 % (228740)Peak memory usage: 26 MB % 227.12/32.51 % (228740)Instructions burned: 15852 (million) % 227.12/32.51 % (228748)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2107368241:s2a=on:i=53295_2820 on theBenchmark for (2820ds/53295Mi) % 227.12/32.51 % (228732)Instruction limit reached! % 227.12/32.51 % (228732)------------------------------ % 227.12/32.51 % (228732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.12/32.51 % (228732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.12/32.51 % (228732)CaDiCaL version: 2.1.3 % 227.12/32.51 % (228732)Termination reason: Instruction limit % 227.12/32.51 % (228732)Termination phase: Saturation % 227.12/32.51 % (228732)Time elapsed: 9.750 s % 227.12/32.51 % (228732)Peak memory usage: 29 MB % 227.12/32.51 % (228732)Instructions burned: 14134 (million) % 227.12/32.51 % (228750)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1470474297:i=26857:ins=20_2798 on theBenchmark for (2798ds/26857Mi) % 227.12/32.51 % (228713)Instruction limit reached! % 227.12/32.51 % (228713)------------------------------ % 227.12/32.51 % (228713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.12/32.51 % (228713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.12/32.51 % (228713)CaDiCaL version: 2.1.3 % 227.12/32.51 % (228713)Termination reason: Instruction limit % 227.12/32.51 % (228713)Termination phase: Saturation % 227.12/32.51 % (228713)Time elapsed: 13.457 s % 227.12/32.51 % (228713)Peak memory usage: 31 MB % 227.12/32.51 % (228713)Instructions burned: 20139 (million) % 227.12/32.51 % (228752)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1027203484:i=28120:bs=on:fsr=off_2795 on theBenchmark for (2795ds/28120Mi) % 227.12/32.51 % (228750)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.12/32.51 % (228750)Terminated due to inappropriate strategy. % 227.12/32.51 % (228750)------------------------------ % 227.12/32.51 % (228750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.12/32.51 % (228750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.12/32.51 % (228750)CaDiCaL version: 2.1.3 % 227.12/32.51 % (228750)Termination reason: Inappropriate % 227.12/32.51 % (228750)Time elapsed: 0.377 s % 227.12/32.51 % (228750)Peak memory usage: 11 MB % 227.12/32.51 % (228750)Instructions burned: 467 (million) % 227.12/32.51 % (228750)------------------------------ % 227.12/32.51 % (228750)------------------------------ % 227.12/32.51 % (228754)fmb+10_1_sil=256000:fmbss=7:random_seed=2649461844:fmbsr=1.6:i=182295_2794 on theBenchmark for (2794ds/182295Mi) % 227.12/32.51 % (228754)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.12/32.51 % (228754)Terminated due to inappropriate strategy. % 227.12/32.51 % (228754)------------------------------ % 227.12/32.51 % (228754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.12/32.51 % (228754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.12/32.51 % (228754)CaDiCaL version: 2.1.3 % 227.12/32.51 % (228754)Termination reason: Inappropriate % 227.12/32.51 % (228754)Time elapsed: 0.378 s % 227.12/32.51 % (228754)Peak memory usage: 11 MB % 227.12/32.51 % (228754)Instructions burned: 467 (million) % 227.12/32.51 % (228754)------------------------------ % 227.12/32.51 % (228754)------------------------------ % 227.12/32.51 % (228756)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1321600388:i=44625:gsp=on_2789 on theBenchmark for (2789ds/44625Mi) % 227.12/32.51 % (228756)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.12/32.51 % (228756)Terminated due to inappropriate strategy. % 227.12/32.51 % (228756)------------------------------ % 227.12/32.51 % (228756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.12/32.51 % (228756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.78/36.57 % (228756)CaDiCaL version: 2.1.3 % 255.78/36.57 % (228756)Termination reason: Inappropriate % 255.78/36.57 % (228756)Time elapsed: 0.246 s % 255.78/36.57 % (228756)Peak memory usage: 11 MB % 255.78/36.57 % (228756)Instructions burned: 467 (million) % 255.78/36.57 % (228756)------------------------------ % 255.78/36.57 % (228756)------------------------------ % 255.78/36.57 % (228760)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=186965316:i=160505_2787 on theBenchmark for (2787ds/160505Mi) % 255.78/36.57 % (228760)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 255.78/36.57 % (228760)Terminated due to inappropriate strategy. % 255.78/36.57 % (228760)------------------------------ % 255.78/36.57 % (228760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.78/36.57 % (228760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.78/36.57 % (228760)CaDiCaL version: 2.1.3 % 255.78/36.57 % (228760)Termination reason: Inappropriate % 255.78/36.57 % (228760)Time elapsed: 0.333 s % 255.78/36.57 % (228760)Peak memory usage: 11 MB % 255.78/36.57 % (228760)Instructions burned: 467 (million) % 255.78/36.57 % (228760)------------------------------ % 255.78/36.57 % (228760)------------------------------ % 255.78/36.57 % (228762)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2013909216:fmbsr=1.3:i=225729_2783 on theBenchmark for (2783ds/225729Mi) % 255.78/36.57 % (228762)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 255.78/36.57 % (228762)Terminated due to inappropriate strategy. % 255.78/36.57 % (228762)------------------------------ % 255.78/36.57 % (228762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.78/36.57 % (228762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.78/36.57 % (228762)CaDiCaL version: 2.1.3 % 255.78/36.57 % (228762)Termination reason: Inappropriate % 255.78/36.57 % (228762)Time elapsed: 0.377 s % 255.78/36.57 % (228762)Peak memory usage: 11 MB % 255.78/36.57 % (228762)Instructions burned: 467 (million) % 255.78/36.57 % (228762)------------------------------ % 255.78/36.57 % (228762)------------------------------ % 255.78/36.57 % (228764)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1115039360:fmbsr=2:i=185024:ins=7_2779 on theBenchmark for (2779ds/185024Mi) % 255.78/36.57 % (228764)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 255.78/36.57 % (228764)Terminated due to inappropriate strategy. % 255.78/36.57 % (228764)------------------------------ % 255.78/36.57 % (228764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.78/36.57 % (228764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.78/36.57 % (228764)CaDiCaL version: 2.1.3 % 255.78/36.57 % (228764)Termination reason: Inappropriate % 255.78/36.57 % (228764)Time elapsed: 0.233 s % 255.78/36.57 % (228764)Peak memory usage: 11 MB % 255.78/36.57 % (228764)Instructions burned: 467 (million) % 255.78/36.57 % (228764)------------------------------ % 255.78/36.57 % (228764)------------------------------ % 255.78/36.57 % (228766)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2038027238:rtra=on_2776 on theBenchmark for (2776ds/0Mi) % 255.78/36.57 % (228766)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 255.78/36.57 % (228766)Terminated due to inappropriate strategy. % 255.78/36.57 % (228766)------------------------------ % 255.78/36.57 % (228766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.78/36.57 % (228766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.78/36.57 % (228766)CaDiCaL version: 2.1.3 % 255.78/36.57 % (228766)Termination reason: Inappropriate % 255.78/36.57 % (228766)Time elapsed: 0.230 s % 255.78/36.57 % (228766)Peak memory usage: 11 MB % 255.78/36.57 % (228766)Instructions burned: 469 (million) % 255.78/36.57 % (228766)------------------------------ % 255.78/36.57 % (228766)------------------------------ % 255.78/36.57 % (228768)% WARNING: option uhcvi not known. % 255.78/36.57 % (228768)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3716018320:i=271062:add=off:rtra=on:rawr=on_2774 on theBenchmark for (2774ds/271062Mi) % 255.78/36.57 % (228499)Instruction limit reached! % 255.78/36.57 % (228499)------------------------------ % 255.78/36.57 % (228499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.78/36.57 % (228499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.78/36.57 % (228499)CaDiCaL version: 2.1.3 % 255.78/36.57 % (228499)Termination reason: Instruction limit % 255.78/36.57 % (228499)Termination phase: Saturation % 255.78/36.57 % (228499)Time elapsed: 21.228 s % 255.78/36.57 % (228499)Peak memory usage: 17 MB % 279.20/39.89 % (228499)Instructions burned: 29340 (million) % 279.20/39.89 % (228772)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1066755808:i=176048:add=on:rtra=on:rawr=on_2763 on theBenchmark for (2763ds/176048Mi) % 279.20/39.89 % (228746)Instruction limit reached! % 279.20/39.89 % (228746)------------------------------ % 279.20/39.89 % (228746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.20/39.89 % (228746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.20/39.89 % (228746)CaDiCaL version: 2.1.3 % 279.20/39.89 % (228746)Termination reason: Instruction limit % 279.20/39.89 % (228746)Termination phase: Saturation % 279.20/39.89 % (228746)Time elapsed: 13.907 s % 279.20/39.89 % (228746)Peak memory usage: 91 MB % 279.20/39.89 % (228746)Instructions burned: 17628 (million) % 279.20/39.89 % (228812)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3220071089:i=206:fgj=on:rtra=on_2689 on theBenchmark for (2689ds/206Mi) % 279.20/39.89 % (228812)Instruction limit reached! % 279.20/39.89 % (228812)------------------------------ % 279.20/39.89 % (228812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.20/39.89 % (228812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.20/39.89 % (228812)CaDiCaL version: 2.1.3 % 279.20/39.89 % (228812)Termination reason: Instruction limit % 279.20/39.89 % (228812)Termination phase: Property scanning % 279.20/39.89 % (228812)Time elapsed: 0.167 s % 279.20/39.89 % (228812)Peak memory usage: 10 MB % 279.20/39.89 % (228812)Instructions burned: 206 (million) % 279.20/39.89 % (228814)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=613753519:i=232:rtra=on_2687 on theBenchmark for (2687ds/232Mi) % 279.20/39.89 % (228814)Instruction limit reached! % 279.20/39.89 % (228814)------------------------------ % 279.20/39.89 % (228814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.20/39.89 % (228814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.20/39.89 % (228814)CaDiCaL version: 2.1.3 % 279.20/39.89 % (228814)Termination reason: Instruction limit % 279.20/39.89 % (228814)Termination phase: Property scanning % 279.20/39.89 % (228814)Time elapsed: 0.113 s % 279.20/39.89 % (228814)Peak memory usage: 11 MB % 279.20/39.89 % (228814)Instructions burned: 234 (million) % 279.20/39.89 % (228816)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4182618713:i=262:rtra=on_2686 on theBenchmark for (2686ds/262Mi) % 279.20/39.89 % (228816)Instruction limit reached! % 279.20/39.89 % (228816)------------------------------ % 279.20/39.89 % (228816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.20/39.89 % (228816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.20/39.89 % (228816)CaDiCaL version: 2.1.3 % 279.20/39.89 % (228816)Termination reason: Instruction limit % 279.20/39.89 % (228816)Termination phase: Property scanning % 279.20/39.89 % (228816)Time elapsed: 0.224 s % 279.20/39.89 % (228816)Peak memory usage: 11 MB % 279.20/39.89 % (228816)Instructions burned: 263 (million) % 279.20/39.89 % (228819)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3864801592:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2683 on theBenchmark for (2683ds/318Mi) % 279.20/39.89 % (228819)Instruction limit reached! % 279.20/39.89 % (228819)------------------------------ % 279.20/39.89 % (228819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.20/39.89 % (228819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.20/39.89 % (228819)CaDiCaL version: 2.1.3 % 279.20/39.89 % (228819)Termination reason: Instruction limit % 279.20/39.89 % (228819)Termination phase: Property scanning % 279.20/39.89 % (228819)Time elapsed: 0.257 s % 279.20/39.89 % (228819)Peak memory usage: 11 MB % 279.20/39.89 % (228819)Instructions burned: 318 (million) % 279.20/39.89 % (228824)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1242210609:i=1428:nm=2:rtra=on_2680 on theBenchmark for (2680ds/1428Mi) % 279.20/39.89 % (228824)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 279.20/39.89 % (228824)Terminated due to inappropriate strategy. % 279.20/39.89 % (228824)------------------------------ % 279.20/39.89 % (228824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.20/39.89 % (228824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.20/39.89 % (228824)CaDiCaL version: 2.1.3 % 279.20/39.89 % (228824)Termination reason: Inappropriate % 279.20/39.89 % (228824)Time elapsed: 0.352 s % 279.20/39.89 % (228824)Peak memory usage: 11 MB % 289.83/41.35 % (228824)Instructions burned: 468 (million) % 289.83/41.35 % (228824)------------------------------ % 289.83/41.35 % (228824)------------------------------ % 289.83/41.35 % (228826)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=572653303:i=262:bd=preordered:rtra=on:fsd=on_2677 on theBenchmark for (2677ds/262Mi) % 289.83/41.35 % (228826)Instruction limit reached! % 289.83/41.35 % (228826)------------------------------ % 289.83/41.35 % (228826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/41.35 % (228826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.83/41.35 % (228826)CaDiCaL version: 2.1.3 % 289.83/41.35 % (228826)Termination reason: Instruction limit % 289.83/41.35 % (228826)Termination phase: Property scanning % 289.83/41.35 % (228826)Time elapsed: 0.174 s % 289.83/41.35 % (228826)Peak memory usage: 11 MB % 289.83/41.35 % (228826)Instructions burned: 262 (million) % 289.83/41.35 % (228828)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=2038336530:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2675 on theBenchmark for (2675ds/1368Mi) % 289.83/41.35 % (228828)Instruction limit reached! % 289.83/41.35 % (228828)------------------------------ % 289.83/41.35 % (228828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/41.35 % (228828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.83/41.35 % (228828)CaDiCaL version: 2.1.3 % 289.83/41.35 % (228828)Termination reason: Instruction limit % 289.83/41.35 % (228828)Termination phase: Saturation % 289.83/41.35 % (228828)Time elapsed: 0.949 s % 289.83/41.35 % (228828)Peak memory usage: 17 MB % 289.83/41.35 % (228828)Instructions burned: 1368 (million) % 289.83/41.35 % (228834)ott-21_1_sil=16000:si=on:fs=off:random_seed=2165336177:i=360:av=off:fsr=off:rtra=on_2665 on theBenchmark for (2665ds/360Mi) % 289.83/41.35 % (228834)Instruction limit reached! % 289.83/41.35 % (228834)------------------------------ % 289.83/41.35 % (228834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/41.35 % (228834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.83/41.35 % (228834)CaDiCaL version: 2.1.3 % 289.83/41.35 % (228834)Termination reason: Instruction limit % 289.83/41.35 % (228834)Termination phase: Property scanning % 289.83/41.35 % (228834)Time elapsed: 0.209 s % 289.83/41.35 % (228834)Peak memory usage: 11 MB % 289.83/41.35 % (228834)Instructions burned: 362 (million) % 289.83/41.35 % (228836)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=702745693:i=954:bd=all:rtra=on_2663 on theBenchmark for (2663ds/954Mi) % 289.83/41.35 % (228836)Instruction limit reached! % 289.83/41.35 % (228836)------------------------------ % 289.83/41.35 % (228836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/41.35 % (228836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.83/41.35 % (228836)CaDiCaL version: 2.1.3 % 289.83/41.35 % (228836)Termination reason: Instruction limit % 289.83/41.35 % (228836)Termination phase: Saturation % 289.83/41.35 % (228836)Time elapsed: 0.539 s % 289.83/41.35 % (228836)Peak memory usage: 15 MB % 289.83/41.35 % (228836)Instructions burned: 955 (million) % 289.83/41.35 % (228840)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2036529747:fmbsr=1.3:i=1730:ins=25:rtra=on_2657 on theBenchmark for (2657ds/1730Mi) % 289.83/41.35 % (228840)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 289.83/41.35 % (228840)Terminated due to inappropriate strategy. % 289.83/41.35 % (228840)------------------------------ % 289.83/41.35 % (228840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/41.35 % (228840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.83/41.35 % (228840)CaDiCaL version: 2.1.3 % 289.83/41.35 % (228840)Termination reason: Inappropriate % 289.83/41.35 % (228840)Time elapsed: 0.289 s % 289.83/41.35 % (228840)Peak memory usage: 11 MB % 289.83/41.35 % (228840)Instructions burned: 355 (million) % 289.83/41.35 % (228840)------------------------------ % 289.83/41.35 % (228840)------------------------------ % 289.83/41.35 % (228842)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=56763967:i=2358:rtra=on_2654 on theBenchmark for (2654ds/2358Mi) % 289.83/41.35 % (228842)Instruction limit reached! % 289.83/41.35 % (228842)------------------------------ % 289.83/41.35 % (228842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.83/41.35 % (228842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 Terminated % 300.40/42.84 % Vampire exiting %------------------------------------------------------------------------------