%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX127_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n005.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:32 PM UTC 2026 % Result : Timeout 289.08s 41.04s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX127_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.17 % Computer : n005.cluster.edu % 0.06/0.17 % Model : x86_64 x86_64 % 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.17 % Memory : 8046.5625MB % 0.06/0.17 % OS : Linux 6.8.0-71-generic % 0.06/0.17 % CPULimit : 300 % 0.06/0.17 % WCLimit : 300 % 0.06/0.17 % DateTime : Mon Sep 28 15:02:47 UTC 2026 % 0.06/0.17 % CPUTime : % 0.06/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.20 Running first-order model finding % 0.06/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.38/0.59 % (845238)Will run a generic schedule for satisfiability detection. % 2.38/0.59 % (845247)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3996666216:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.38/0.59 % (845244)% WARNING: option uhcvi not known. % 2.38/0.59 % (845243)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1737136249_2999 on theBenchmark for (2999ds/0Mi) % 2.38/0.59 % (845244)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3535563810:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.38/0.59 % (845246)dis+10_1_sil=32000:sp=arity:random_seed=2099921921:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.38/0.59 % (845245)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2894287315:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.38/0.59 % (845248)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2933881158:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.38/0.59 % (845249)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2297429545:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.38/0.59 % (845243)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.38/0.59 % (845243)Terminated due to inappropriate strategy. % 2.38/0.59 % (845243)------------------------------ % 2.38/0.59 % (845243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.38/0.59 % (845243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.38/0.59 % (845243)CaDiCaL version: 2.1.3 % 2.38/0.59 % (845243)Termination reason: Inappropriate % 2.38/0.59 % (845243)Time elapsed: 0.007 s % 2.38/0.59 % (845243)Peak memory usage: 10 MB % 2.38/0.59 % (845243)Instructions burned: 16 (million) % 2.38/0.59 % (845243)------------------------------ % 2.38/0.59 % (845243)------------------------------ % 2.38/0.59 % (845247)Instruction limit reached! % 2.38/0.59 % (845247)------------------------------ % 2.38/0.59 % (845247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.38/0.59 % (845247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.38/0.59 % (845247)CaDiCaL version: 2.1.3 % 2.38/0.59 % (845247)Termination reason: Instruction limit % 2.38/0.59 % (845247)Termination phase: Saturation % 2.38/0.59 % (845247)Time elapsed: 0.028 s % 2.38/0.59 % (845247)Peak memory usage: 13 MB % 2.38/0.59 % (845247)Instructions burned: 118 (million) % 2.38/0.59 % (845257)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1834353151:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.38/0.59 % (845258)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3822933427:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.38/0.59 % (845257)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.38/0.59 % (845257)Terminated due to inappropriate strategy. % 2.38/0.59 % (845257)------------------------------ % 2.38/0.59 % (845257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.38/0.59 % (845257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.38/0.59 % (845257)CaDiCaL version: 2.1.3 % 2.38/0.59 % (845257)Termination reason: Inappropriate % 2.38/0.59 % (845257)Time elapsed: 0.007 s % 2.38/0.59 % (845257)Peak memory usage: 10 MB % 2.38/0.59 % (845257)Instructions burned: 16 (million) % 2.38/0.59 % (845257)------------------------------ % 2.38/0.59 % (845257)------------------------------ % 2.38/0.59 % (845246)Instruction limit reached! % 2.38/0.59 % (845246)------------------------------ % 2.38/0.59 % (845246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.38/0.59 % (845246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.38/0.59 % (845246)CaDiCaL version: 2.1.3 % 2.38/0.59 % (845246)Termination reason: Instruction limit % 2.38/0.59 % (845246)Termination phase: Saturation % 2.38/0.59 % (845246)Time elapsed: 0.044 s % 2.38/0.59 % (845246)Peak memory usage: 12 MB % 2.38/0.59 % (845246)Instructions burned: 103 (million) % 2.38/0.59 % (845261)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=393084940:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 2.38/0.59 % (845248)Instruction limit reached! % 2.38/0.59 % (845248)------------------------------ % 2.38/0.59 % (845248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.67/1.02 % (845248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/1.02 % (845248)CaDiCaL version: 2.1.3 % 3.67/1.02 % (845248)Termination reason: Instruction limit % 3.67/1.02 % (845248)Termination phase: Saturation % 3.67/1.02 % (845248)Time elapsed: 0.057 s % 3.67/1.02 % (845248)Peak memory usage: 13 MB % 3.67/1.02 % (845248)Instructions burned: 132 (million) % 3.67/1.02 % (845262)ott-21_1_sil=16000:fs=off:random_seed=339084752:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.67/1.02 % (845258)Instruction limit reached! % 3.67/1.02 % (845258)------------------------------ % 3.67/1.02 % (845258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.67/1.02 % (845258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/1.02 % (845258)CaDiCaL version: 2.1.3 % 3.67/1.02 % (845258)Termination reason: Instruction limit % 3.67/1.02 % (845258)Termination phase: Saturation % 3.67/1.02 % (845258)Time elapsed: 0.031 s % 3.67/1.02 % (845258)Peak memory usage: 13 MB % 3.67/1.02 % (845258)Instructions burned: 133 (million) % 3.67/1.02 % (845266)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1749908637:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 3.67/1.02 % (845264)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2950759396:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 3.67/1.02 % (845266)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.67/1.02 % (845266)Terminated due to inappropriate strategy. % 3.67/1.02 % (845266)------------------------------ % 3.67/1.02 % (845266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.67/1.02 % (845266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/1.02 % (845266)CaDiCaL version: 2.1.3 % 3.67/1.02 % (845266)Termination reason: Inappropriate % 3.67/1.02 % (845266)Time elapsed: 0.003 s % 3.67/1.02 % (845266)Peak memory usage: 10 MB % 3.67/1.02 % (845266)Instructions burned: 12 (million) % 3.67/1.02 % (845266)------------------------------ % 3.67/1.02 % (845266)------------------------------ % 3.67/1.02 % (845249)Instruction limit reached! % 3.67/1.02 % (845249)------------------------------ % 3.67/1.02 % (845249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.67/1.02 % (845249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/1.02 % (845249)CaDiCaL version: 2.1.3 % 3.67/1.02 % (845249)Termination reason: Instruction limit % 3.67/1.02 % (845249)Termination phase: Saturation % 3.67/1.02 % (845249)Time elapsed: 0.079 s % 3.67/1.02 % (845249)Peak memory usage: 13 MB % 3.67/1.02 % (845249)Instructions burned: 161 (million) % 3.67/1.02 % (845270)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2098329838:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 3.67/1.02 % (845270)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.67/1.02 % (845270)Terminated due to inappropriate strategy. % 3.67/1.02 % (845270)------------------------------ % 3.67/1.02 % (845270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.67/1.02 % (845270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/1.02 % (845270)CaDiCaL version: 2.1.3 % 3.67/1.02 % (845270)Termination reason: Inappropriate % 3.67/1.02 % (845270)Time elapsed: 0.003 s % 3.67/1.02 % (845270)Peak memory usage: 10 MB % 3.67/1.02 % (845270)Instructions burned: 12 (million) % 3.67/1.02 % (845270)------------------------------ % 3.67/1.02 % (845270)------------------------------ % 3.67/1.02 % (845269)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4066874194:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 3.67/1.02 % (845272)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=3719870547: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) % 3.67/1.02 % (845262)Instruction limit reached! % 3.67/1.02 % (845262)------------------------------ % 3.67/1.02 % (845262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.67/1.02 % (845262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/1.02 % (845262)CaDiCaL version: 2.1.3 % 3.67/1.02 % (845262)Termination reason: Instruction limit % 3.67/1.02 % (845262)Termination phase: Saturation % 3.67/1.02 % (845262)Time elapsed: 0.074 s % 3.67/1.02 % (845262)Peak memory usage: 12 MB % 3.67/1.02 % (845262)Instructions burned: 182 (million) % 15.09/2.48 % (845275)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1396134255:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 15.09/2.48 % (845272)Instruction limit reached! % 15.09/2.48 % (845272)------------------------------ % 15.09/2.48 % (845272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.09/2.48 % (845272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.09/2.48 % (845272)CaDiCaL version: 2.1.3 % 15.09/2.48 % (845272)Termination reason: Instruction limit % 15.09/2.48 % (845272)Termination phase: Saturation % 15.09/2.48 % (845272)Time elapsed: 0.147 s % 15.09/2.48 % (845272)Peak memory usage: 14 MB % 15.09/2.48 % (845272)Instructions burned: 694 (million) % 15.09/2.48 % (845277)fmb+10_1_sil=64000:random_seed=1961427734:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 15.09/2.48 % (845264)Instruction limit reached! % 15.09/2.48 % (845264)------------------------------ % 15.09/2.48 % (845264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.09/2.48 % (845264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.09/2.48 % (845264)CaDiCaL version: 2.1.3 % 15.09/2.48 % (845264)Termination reason: Instruction limit % 15.09/2.48 % (845264)Termination phase: Saturation % 15.09/2.48 % (845264)Time elapsed: 0.185 s % 15.09/2.48 % (845264)Peak memory usage: 12 MB % 15.09/2.48 % (845264)Instructions burned: 478 (million) % 15.09/2.48 % (845277)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 15.09/2.48 % (845277)Terminated due to inappropriate strategy. % 15.09/2.48 % (845277)------------------------------ % 15.09/2.48 % (845277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.09/2.48 % (845277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.09/2.48 % (845277)CaDiCaL version: 2.1.3 % 15.09/2.48 % (845277)Termination reason: Inappropriate % 15.09/2.48 % (845277)Time elapsed: 0.003 s % 15.09/2.48 % (845277)Peak memory usage: 10 MB % 15.09/2.48 % (845277)Instructions burned: 16 (million) % 15.09/2.48 % (845277)------------------------------ % 15.09/2.48 % (845277)------------------------------ % 15.09/2.48 % (845280)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3598253844:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 15.09/2.48 % (845280)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 15.09/2.48 % (845280)Terminated due to inappropriate strategy. % 15.09/2.48 % (845280)------------------------------ % 15.09/2.48 % (845280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.09/2.48 % (845280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.09/2.48 % (845280)CaDiCaL version: 2.1.3 % 15.09/2.48 % (845280)Termination reason: Inappropriate % 15.09/2.48 % (845280)Time elapsed: 0.003 s % 15.09/2.48 % (845280)Peak memory usage: 10 MB % 15.09/2.48 % (845280)Instructions burned: 16 (million) % 15.09/2.48 % (845280)------------------------------ % 15.09/2.48 % (845280)------------------------------ % 15.09/2.48 % (845279)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4022233209:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 15.09/2.48 % (845279)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 15.09/2.48 % (845279)Terminated due to inappropriate strategy. % 15.09/2.48 % (845279)------------------------------ % 15.09/2.48 % (845279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.09/2.48 % (845279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.09/2.48 % (845279)CaDiCaL version: 2.1.3 % 15.09/2.48 % (845279)Termination reason: Inappropriate % 15.09/2.48 % (845279)Time elapsed: 0.007 s % 15.09/2.48 % (845279)Peak memory usage: 10 MB % 15.09/2.48 % (845279)Instructions burned: 16 (million) % 15.09/2.48 % (845279)------------------------------ % 15.09/2.48 % (845279)------------------------------ % 15.09/2.48 % (845282)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4027299551:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 15.09/2.48 % (845284)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2681726282:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 15.09/2.48 % (845261)Instruction limit reached! % 15.09/2.48 % (845261)------------------------------ % 15.09/2.48 % (845261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.09/2.48 % (845261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.97/3.05 % (845261)CaDiCaL version: 2.1.3 % 19.97/3.05 % (845261)Termination reason: Instruction limit % 19.97/3.05 % (845261)Termination phase: Saturation % 19.97/3.05 % (845261)Time elapsed: 0.289 s % 19.97/3.05 % (845261)Peak memory usage: 15 MB % 19.97/3.05 % (845261)Instructions burned: 685 (million) % 19.97/3.05 % (845287)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1974739159:i=6324_2996 on theBenchmark for (2996ds/6324Mi) % 19.97/3.05 % (845287)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.97/3.05 % (845287)Terminated due to inappropriate strategy. % 19.97/3.05 % (845287)------------------------------ % 19.97/3.05 % (845287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.97/3.05 % (845287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.97/3.05 % (845287)CaDiCaL version: 2.1.3 % 19.97/3.05 % (845287)Termination reason: Inappropriate % 19.97/3.05 % (845287)Time elapsed: 0.007 s % 19.97/3.05 % (845287)Peak memory usage: 10 MB % 19.97/3.05 % (845287)Instructions burned: 16 (million) % 19.97/3.05 % (845287)------------------------------ % 19.97/3.05 % (845287)------------------------------ % 19.97/3.05 % (845289)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4051010580:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 19.97/3.05 % (845289)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.97/3.05 % (845289)Terminated due to inappropriate strategy. % 19.97/3.05 % (845289)------------------------------ % 19.97/3.05 % (845289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.97/3.05 % (845289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.97/3.05 % (845289)CaDiCaL version: 2.1.3 % 19.97/3.05 % (845289)Termination reason: Inappropriate % 19.97/3.05 % (845289)Time elapsed: 0.007 s % 19.97/3.05 % (845289)Peak memory usage: 10 MB % 19.97/3.05 % (845289)Instructions burned: 16 (million) % 19.97/3.05 % (845289)------------------------------ % 19.97/3.05 % (845289)------------------------------ % 19.97/3.05 % (845291)ott-2_1_sil=16000:newcnf=on:random_seed=1695965859:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi) % 19.97/3.05 % (845275)Instruction limit reached! % 19.97/3.05 % (845275)------------------------------ % 19.97/3.05 % (845275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.97/3.05 % (845275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.97/3.05 % (845275)CaDiCaL version: 2.1.3 % 19.97/3.05 % (845275)Termination reason: Instruction limit % 19.97/3.05 % (845275)Termination phase: Saturation % 19.97/3.05 % (845275)Time elapsed: 0.335 s % 19.97/3.05 % (845275)Peak memory usage: 13 MB % 19.97/3.05 % (845275)Instructions burned: 880 (million) % 19.97/3.05 % (845293)ott+10_1_sil=32000:tgt=ground:random_seed=2934313479:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi) % 19.97/3.05 % (845269)Instruction limit reached! % 19.97/3.05 % (845269)------------------------------ % 19.97/3.05 % (845269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.97/3.05 % (845269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.97/3.05 % (845269)CaDiCaL version: 2.1.3 % 19.97/3.05 % (845269)Termination reason: Instruction limit % 19.97/3.05 % (845269)Termination phase: Saturation % 19.97/3.05 % (845269)Time elapsed: 0.456 s % 19.97/3.05 % (845269)Peak memory usage: 13 MB % 19.97/3.05 % (845269)Instructions burned: 1181 (million) % 19.97/3.05 % (845295)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1793346781:i=54282_2994 on theBenchmark for (2994ds/54282Mi) % 19.97/3.05 % (845295)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.97/3.05 % (845295)Terminated due to inappropriate strategy. % 19.97/3.05 % (845295)------------------------------ % 19.97/3.05 % (845295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.97/3.05 % (845295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.97/3.05 % (845295)CaDiCaL version: 2.1.3 % 19.97/3.05 % (845295)Termination reason: Inappropriate % 19.97/3.05 % (845295)Time elapsed: 0.007 s % 19.97/3.05 % (845295)Peak memory usage: 10 MB % 19.97/3.05 % (845295)Instructions burned: 16 (million) % 19.97/3.05 % (845295)------------------------------ % 19.97/3.05 % (845295)------------------------------ % 19.97/3.05 % (845297)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=48889352:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi) % 19.97/3.05 % (845291)Instruction limit reached! % 72.93/10.57 % (845291)------------------------------ % 72.93/10.57 % (845291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.93/10.57 % (845291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.93/10.57 % (845291)CaDiCaL version: 2.1.3 % 72.93/10.57 % (845291)Termination reason: Instruction limit % 72.93/10.57 % (845291)Termination phase: Saturation % 72.93/10.57 % (845291)Time elapsed: 0.349 s % 72.93/10.57 % (845291)Peak memory usage: 14 MB % 72.93/10.57 % (845291)Instructions burned: 870 (million) % 72.93/10.57 % (845299)dis+21_1_sil=32000:sas=cadical:random_seed=1707663578:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 72.93/10.57 % (845284)Instruction limit reached! % 72.93/10.57 % (845284)------------------------------ % 72.93/10.57 % (845284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.93/10.57 % (845284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.93/10.57 % (845284)CaDiCaL version: 2.1.3 % 72.93/10.57 % (845284)Termination reason: Instruction limit % 72.93/10.57 % (845284)Termination phase: Saturation % 72.93/10.57 % (845284)Time elapsed: 0.760 s % 72.93/10.57 % (845284)Peak memory usage: 24 MB % 72.93/10.57 % (845284)Instructions burned: 1473 (million) % 72.93/10.57 % (845301)ott+11_1_sil=16000:gs=on:random_seed=3121310072:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 72.93/10.57 % (845282)Instruction limit reached! % 72.93/10.57 % (845282)------------------------------ % 72.93/10.57 % (845282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.93/10.57 % (845282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.93/10.57 % (845282)CaDiCaL version: 2.1.3 % 72.93/10.57 % (845282)Termination reason: Instruction limit % 72.93/10.57 % (845282)Termination phase: Saturation % 72.93/10.57 % (845282)Time elapsed: 1.074 s % 72.93/10.57 % (845282)Peak memory usage: 19 MB % 72.93/10.57 % (845282)Instructions burned: 5135 (million) % 72.93/10.57 % (845303)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=444760599:fmbsr=1.6:i=67534_2985 on theBenchmark for (2985ds/67534Mi) % 72.93/10.57 % (845303)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 72.93/10.57 % (845303)Terminated due to inappropriate strategy. % 72.93/10.57 % (845303)------------------------------ % 72.93/10.57 % (845303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.93/10.57 % (845303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.93/10.57 % (845303)CaDiCaL version: 2.1.3 % 72.93/10.57 % (845303)Termination reason: Inappropriate % 72.93/10.57 % (845303)Time elapsed: 0.003 s % 72.93/10.57 % (845303)Peak memory usage: 10 MB % 72.93/10.57 % (845303)Instructions burned: 16 (million) % 72.93/10.57 % (845303)------------------------------ % 72.93/10.57 % (845303)------------------------------ % 72.93/10.57 % (845305)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2190364287:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2985 on theBenchmark for (2985ds/4591Mi) % 72.93/10.57 % (845301)Instruction limit reached! % 72.93/10.57 % (845301)------------------------------ % 72.93/10.57 % (845301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.93/10.57 % (845301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.93/10.57 % (845301)CaDiCaL version: 2.1.3 % 72.93/10.57 % (845301)Termination reason: Instruction limit % 72.93/10.57 % (845301)Termination phase: Saturation % 72.93/10.57 % (845301)Time elapsed: 0.842 s % 72.93/10.57 % (845301)Peak memory usage: 13 MB % 72.93/10.57 % (845301)Instructions burned: 2252 (million) % 72.93/10.57 % (845307)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=941564228:i=29340_2980 on theBenchmark for (2980ds/29340Mi) % 72.93/10.57 % (845297)Instruction limit reached! % 72.93/10.57 % (845297)------------------------------ % 72.93/10.57 % (845297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.93/10.57 % (845297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.93/10.57 % (845297)CaDiCaL version: 2.1.3 % 72.93/10.57 % (845297)Termination reason: Instruction limit % 72.93/10.57 % (845297)Termination phase: Saturation % 72.93/10.57 % (845297)Time elapsed: 1.368 s % 72.93/10.57 % (845297)Peak memory usage: 17 MB % 72.93/10.57 % (845297)Instructions burned: 3514 (million) % 72.93/10.57 % (845309)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2062582591:i=5211_2979 on theBenchmark for (2979ds/5211Mi) % 72.93/10.57 % (845299)Instruction limit reached! % 83.81/12.10 % (845299)------------------------------ % 83.81/12.10 % (845299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.81/12.10 % (845299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.81/12.10 % (845299)CaDiCaL version: 2.1.3 % 83.81/12.10 % (845299)Termination reason: Instruction limit % 83.81/12.10 % (845299)Termination phase: Saturation % 83.81/12.10 % (845299)Time elapsed: 1.443 s % 83.81/12.10 % (845299)Peak memory usage: 16 MB % 83.81/12.10 % (845299)Instructions burned: 3775 (million) % 83.81/12.10 % (845311)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2060263953:i=5497:nm=2_2977 on theBenchmark for (2977ds/5497Mi) % 83.81/12.10 % (845311)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.81/12.10 % (845311)Terminated due to inappropriate strategy. % 83.81/12.10 % (845311)------------------------------ % 83.81/12.10 % (845311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.81/12.10 % (845311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.81/12.10 % (845311)CaDiCaL version: 2.1.3 % 83.81/12.10 % (845311)Termination reason: Inappropriate % 83.81/12.10 % (845311)Time elapsed: 0.007 s % 83.81/12.10 % (845311)Peak memory usage: 10 MB % 83.81/12.10 % (845311)Instructions burned: 16 (million) % 83.81/12.10 % (845311)------------------------------ % 83.81/12.10 % (845311)------------------------------ % 83.81/12.10 % (845313)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1713288527:fmbsr=2:i=46332_2976 on theBenchmark for (2976ds/46332Mi) % 83.81/12.10 % (845313)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.81/12.10 % (845313)Terminated due to inappropriate strategy. % 83.81/12.10 % (845313)------------------------------ % 83.81/12.10 % (845313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.81/12.10 % (845313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.81/12.10 % (845313)CaDiCaL version: 2.1.3 % 83.81/12.10 % (845313)Termination reason: Inappropriate % 83.81/12.10 % (845313)Time elapsed: 0.007 s % 83.81/12.10 % (845313)Peak memory usage: 10 MB % 83.81/12.10 % (845313)Instructions burned: 16 (million) % 83.81/12.10 % (845313)------------------------------ % 83.81/12.10 % (845313)------------------------------ % 83.81/12.10 % (845315)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2127261087:i=14071_2976 on theBenchmark for (2976ds/14071Mi) % 83.81/12.10 % (845315)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.81/12.10 % (845315)Terminated due to inappropriate strategy. % 83.81/12.10 % (845315)------------------------------ % 83.81/12.10 % (845315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.81/12.10 % (845315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.81/12.10 % (845315)CaDiCaL version: 2.1.3 % 83.81/12.10 % (845315)Termination reason: Inappropriate % 83.81/12.10 % (845315)Time elapsed: 0.007 s % 83.81/12.10 % (845315)Peak memory usage: 11 MB % 83.81/12.10 % (845315)Instructions burned: 16 (million) % 83.81/12.10 % (845315)------------------------------ % 83.81/12.10 % (845315)------------------------------ % 83.81/12.10 % (845317)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1498472147:i=22565:add=on:rawr=on_2976 on theBenchmark for (2976ds/22565Mi) % 83.81/12.10 % (845293)Instruction limit reached! % 83.81/12.10 % (845293)------------------------------ % 83.81/12.10 % (845293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.81/12.10 % (845293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.81/12.10 % (845293)CaDiCaL version: 2.1.3 % 83.81/12.10 % (845293)Termination reason: Instruction limit % 83.81/12.10 % (845293)Termination phase: Saturation % 83.81/12.10 % (845293)Time elapsed: 1.961 s % 83.81/12.10 % (845293)Peak memory usage: 14 MB % 83.81/12.10 % (845293)Instructions burned: 5115 (million) % 83.81/12.10 % (845319)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3281618852:i=8173:av=off_2974 on theBenchmark for (2974ds/8173Mi) % 83.81/12.10 % (845305)Instruction limit reached! % 83.81/12.10 % (845305)------------------------------ % 83.81/12.10 % (845305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.81/12.10 % (845305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.81/12.10 % (845305)CaDiCaL version: 2.1.3 % 83.81/12.10 % (845305)Termination reason: Instruction limit % 83.81/12.10 % (845305)Termination phase: Saturation % 92.11/13.28 % (845305)Time elapsed: 1.411 s % 92.11/13.28 % (845305)Peak memory usage: 48 MB % 92.11/13.28 % (845305)Instructions burned: 4594 (million) % 92.11/13.28 % (845321)dis+10_16:1_sil=16000:random_seed=3410097203:i=9155:fsr=off_2971 on theBenchmark for (2971ds/9155Mi) % 92.11/13.28 % (845309)Instruction limit reached! % 92.11/13.28 % (845309)------------------------------ % 92.11/13.28 % (845309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.11/13.28 % (845309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.11/13.28 % (845309)CaDiCaL version: 2.1.3 % 92.11/13.28 % (845309)Termination reason: Instruction limit % 92.11/13.28 % (845309)Termination phase: Saturation % 92.11/13.28 % (845309)Time elapsed: 1.979 s % 92.11/13.28 % (845309)Peak memory usage: 21 MB % 92.11/13.28 % (845309)Instructions burned: 5212 (million) % 92.11/13.28 % (845323)ott-3_8_sil=64000:random_seed=1817238803:i=20139:bs=on_2959 on theBenchmark for (2959ds/20139Mi) % 92.11/13.28 % (845321)Instruction limit reached! % 92.11/13.28 % (845321)------------------------------ % 92.11/13.28 % (845321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.11/13.28 % (845321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.11/13.28 % (845321)CaDiCaL version: 2.1.3 % 92.11/13.28 % (845321)Termination reason: Instruction limit % 92.11/13.28 % (845321)Termination phase: Saturation % 92.11/13.28 % (845321)Time elapsed: 1.836 s % 92.11/13.28 % (845321)Peak memory usage: 18 MB % 92.11/13.28 % (845321)Instructions burned: 9159 (million) % 92.11/13.28 % (845325)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3290362354:fmbsr=2:i=32576_2953 on theBenchmark for (2953ds/32576Mi) % 92.11/13.28 % (845325)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 92.11/13.28 % (845325)Terminated due to inappropriate strategy. % 92.11/13.28 % (845325)------------------------------ % 92.11/13.28 % (845325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.11/13.28 % (845325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.11/13.28 % (845325)CaDiCaL version: 2.1.3 % 92.11/13.28 % (845325)Termination reason: Inappropriate % 92.11/13.28 % (845325)Time elapsed: 0.003 s % 92.11/13.28 % (845325)Peak memory usage: 10 MB % 92.11/13.28 % (845325)Instructions burned: 16 (million) % 92.11/13.28 % (845325)------------------------------ % 92.11/13.28 % (845325)------------------------------ % 92.11/13.28 % (845327)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1067349489:i=11404_2952 on theBenchmark for (2952ds/11404Mi) % 92.11/13.28 % (845319)Instruction limit reached! % 92.11/13.28 % (845319)------------------------------ % 92.11/13.28 % (845319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.11/13.28 % (845319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.11/13.28 % (845319)CaDiCaL version: 2.1.3 % 92.11/13.28 % (845319)Termination reason: Instruction limit % 92.11/13.28 % (845319)Termination phase: Saturation % 92.11/13.28 % (845319)Time elapsed: 3.125 s % 92.11/13.28 % (845319)Peak memory usage: 15 MB % 92.11/13.28 % (845319)Instructions burned: 8175 (million) % 92.11/13.28 % (845329)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1915425897:i=14134_2943 on theBenchmark for (2943ds/14134Mi) % 92.11/13.28 % (845327)Instruction limit reached! % 92.11/13.28 % (845327)------------------------------ % 92.11/13.28 % (845327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.11/13.28 % (845327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.11/13.28 % (845327)CaDiCaL version: 2.1.3 % 92.11/13.28 % (845327)Termination reason: Instruction limit % 92.11/13.28 % (845327)Termination phase: Saturation % 92.11/13.28 % (845327)Time elapsed: 2.343 s % 92.11/13.28 % (845327)Peak memory usage: 17 MB % 92.11/13.28 % (845327)Instructions burned: 11407 (million) % 92.11/13.28 % (845331)dis+33_16_sil=32000:sac=on:random_seed=4080937552:i=15851:nm=0_2929 on theBenchmark for (2929ds/15851Mi) % 92.11/13.28 % (845331)Instruction limit reached! % 92.11/13.28 % (845331)------------------------------ % 92.11/13.28 % (845331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 92.11/13.28 % (845331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.11/13.28 % (845331)CaDiCaL version: 2.1.3 % 92.11/13.28 % (845331)Termination reason: Instruction limit % 92.11/13.28 % (845331)Termination phase: Saturation % 92.11/13.28 % (845331)Time elapsed: 3.277 s % 92.11/13.28 % (845331)Peak memory usage: 25 MB % 92.11/13.28 % (845331)Instructions burned: 15855 (million) % 92.11/13.28 % (845333)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1314607311:avsq=on:i=17627:add=on:amm=off_2896 on theBenchmark for (2896ds/17627Mi) % 105.92/15.17 % (845329)Instruction limit reached! % 105.92/15.17 % (845329)------------------------------ % 105.92/15.17 % (845329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.92/15.17 % (845329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.92/15.17 % (845329)CaDiCaL version: 2.1.3 % 105.92/15.17 % (845329)Termination reason: Instruction limit % 105.92/15.17 % (845329)Termination phase: Saturation % 105.92/15.17 % (845329)Time elapsed: 5.382 s % 105.92/15.17 % (845329)Peak memory usage: 18 MB % 105.92/15.17 % (845329)Instructions burned: 14135 (million) % 105.92/15.17 % (845335)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3485590570:s2a=on:i=53295_2889 on theBenchmark for (2889ds/53295Mi) % 105.92/15.17 % (845317)Instruction limit reached! % 105.92/15.17 % (845317)------------------------------ % 105.92/15.17 % (845317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.92/15.17 % (845317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.92/15.17 % (845317)CaDiCaL version: 2.1.3 % 105.92/15.17 % (845317)Termination reason: Instruction limit % 105.92/15.17 % (845317)Termination phase: Saturation % 105.92/15.17 % (845317)Time elapsed: 9.125 s % 105.92/15.17 % (845317)Peak memory usage: 17 MB % 105.92/15.17 % (845317)Instructions burned: 22566 (million) % 105.92/15.17 % (845337)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=964549641:i=26857:ins=20_2885 on theBenchmark for (2885ds/26857Mi) % 105.92/15.17 % (845337)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 105.92/15.17 % (845337)Terminated due to inappropriate strategy. % 105.92/15.17 % (845337)------------------------------ % 105.92/15.17 % (845337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.92/15.17 % (845337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.92/15.17 % (845337)CaDiCaL version: 2.1.3 % 105.92/15.17 % (845337)Termination reason: Inappropriate % 105.92/15.17 % (845337)Time elapsed: 0.007 s % 105.92/15.17 % (845337)Peak memory usage: 10 MB % 105.92/15.17 % (845337)Instructions burned: 16 (million) % 105.92/15.17 % (845337)------------------------------ % 105.92/15.17 % (845337)------------------------------ % 105.92/15.17 % (845339)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3008131403:i=28120:bs=on:fsr=off_2884 on theBenchmark for (2884ds/28120Mi) % 105.92/15.17 % (845323)Instruction limit reached! % 105.92/15.17 % (845323)------------------------------ % 105.92/15.17 % (845323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.92/15.17 % (845323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.92/15.17 % (845323)CaDiCaL version: 2.1.3 % 105.92/15.17 % (845323)Termination reason: Instruction limit % 105.92/15.17 % (845323)Termination phase: Saturation % 105.92/15.17 % (845323)Time elapsed: 7.804 s % 105.92/15.17 % (845323)Peak memory usage: 22 MB % 105.92/15.17 % (845323)Instructions burned: 20140 (million) % 105.92/15.17 % (845341)fmb+10_1_sil=256000:fmbss=7:random_seed=1060173972:fmbsr=1.6:i=182295_2881 on theBenchmark for (2881ds/182295Mi) % 105.92/15.17 % (845341)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 105.92/15.17 % (845341)Terminated due to inappropriate strategy. % 105.92/15.17 % (845341)------------------------------ % 105.92/15.17 % (845341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.92/15.17 % (845341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.92/15.17 % (845341)CaDiCaL version: 2.1.3 % 105.92/15.17 % (845341)Termination reason: Inappropriate % 105.92/15.17 % (845341)Time elapsed: 0.007 s % 105.92/15.17 % (845341)Peak memory usage: 10 MB % 105.92/15.17 % (845341)Instructions burned: 16 (million) % 105.92/15.17 % (845341)------------------------------ % 105.92/15.17 % (845341)------------------------------ % 105.92/15.17 % (845343)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3733414602:i=44625:gsp=on_2881 on theBenchmark for (2881ds/44625Mi) % 105.92/15.17 % (845343)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 105.92/15.17 % (845343)Terminated due to inappropriate strategy. % 105.92/15.17 % (845343)------------------------------ % 105.92/15.17 % (845343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 105.92/15.17 % (845343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.92/15.17 % (845343)CaDiCaL version: 2.1.3 % 105.92/15.17 % (845343)Termination reason: Inappropriate % 134.75/19.24 % (845343)Time elapsed: 0.007 s % 134.75/19.24 % (845343)Peak memory usage: 10 MB % 134.75/19.24 % (845343)Instructions burned: 16 (million) % 134.75/19.24 % (845343)------------------------------ % 134.75/19.24 % (845343)------------------------------ % 134.75/19.24 % (845345)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=786112513:i=160505_2881 on theBenchmark for (2881ds/160505Mi) % 134.75/19.24 % (845345)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.75/19.24 % (845345)Terminated due to inappropriate strategy. % 134.75/19.24 % (845345)------------------------------ % 134.75/19.24 % (845345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.75/19.24 % (845345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.75/19.24 % (845345)CaDiCaL version: 2.1.3 % 134.75/19.24 % (845345)Termination reason: Inappropriate % 134.75/19.24 % (845345)Time elapsed: 0.007 s % 134.75/19.24 % (845345)Peak memory usage: 10 MB % 134.75/19.24 % (845345)Instructions burned: 16 (million) % 134.75/19.24 % (845345)------------------------------ % 134.75/19.24 % (845345)------------------------------ % 134.75/19.24 % (845347)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4225505698:fmbsr=1.3:i=225729_2880 on theBenchmark for (2880ds/225729Mi) % 134.75/19.24 % (845347)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.75/19.24 % (845347)Terminated due to inappropriate strategy. % 134.75/19.24 % (845347)------------------------------ % 134.75/19.24 % (845347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.75/19.24 % (845347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.75/19.24 % (845347)CaDiCaL version: 2.1.3 % 134.75/19.24 % (845347)Termination reason: Inappropriate % 134.75/19.24 % (845347)Time elapsed: 0.007 s % 134.75/19.24 % (845347)Peak memory usage: 10 MB % 134.75/19.24 % (845347)Instructions burned: 16 (million) % 134.75/19.24 % (845347)------------------------------ % 134.75/19.24 % (845347)------------------------------ % 134.75/19.24 % (845349)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1572987684:fmbsr=2:i=185024:ins=7_2880 on theBenchmark for (2880ds/185024Mi) % 134.75/19.24 % (845349)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.75/19.24 % (845349)Terminated due to inappropriate strategy. % 134.75/19.24 % (845349)------------------------------ % 134.75/19.24 % (845349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.75/19.24 % (845349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.75/19.24 % (845349)CaDiCaL version: 2.1.3 % 134.75/19.24 % (845349)Termination reason: Inappropriate % 134.75/19.24 % (845349)Time elapsed: 0.007 s % 134.75/19.24 % (845349)Peak memory usage: 10 MB % 134.75/19.24 % (845349)Instructions burned: 16 (million) % 134.75/19.24 % (845349)------------------------------ % 134.75/19.24 % (845349)------------------------------ % 134.75/19.24 % (845351)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2355062635:rtra=on_2880 on theBenchmark for (2880ds/0Mi) % 134.75/19.24 % (845351)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.75/19.24 % (845351)Terminated due to inappropriate strategy. % 134.75/19.24 % (845351)------------------------------ % 134.75/19.24 % (845351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.75/19.24 % (845351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.75/19.24 % (845351)CaDiCaL version: 2.1.3 % 134.75/19.24 % (845351)Termination reason: Inappropriate % 134.75/19.24 % (845351)Time elapsed: 0.007 s % 134.75/19.24 % (845351)Peak memory usage: 10 MB % 134.75/19.24 % (845351)Instructions burned: 16 (million) % 134.75/19.24 % (845351)------------------------------ % 134.75/19.24 % (845351)------------------------------ % 134.75/19.24 % (845353)% WARNING: option uhcvi not known. % 134.75/19.24 % (845353)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1664755783:i=271062:add=off:rtra=on:rawr=on_2879 on theBenchmark for (2879ds/271062Mi) % 134.75/19.24 % (845307)Instruction limit reached! % 134.75/19.24 % (845307)------------------------------ % 134.75/19.24 % (845307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.75/19.24 % (845307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.75/19.24 % (845307)CaDiCaL version: 2.1.3 % 134.75/19.24 % (845307)Termination reason: Instruction limit % 134.75/19.24 % (845307)Termination phase: Saturation % 134.75/19.24 % (845307)Time elapsed: 11.081 s % 134.75/19.24 % (845307)Peak memory usage: 25 MB % 134.75/19.24 % (845307)Instructions burned: 29340 (million) % 151.79/21.67 % (845355)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3831774606:i=176048:add=on:rtra=on:rawr=on_2869 on theBenchmark for (2869ds/176048Mi) % 151.79/21.67 % (845333)Instruction limit reached! % 151.79/21.67 % (845333)------------------------------ % 151.79/21.67 % (845333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.79/21.67 % (845333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.79/21.67 % (845333)CaDiCaL version: 2.1.3 % 151.79/21.67 % (845333)Termination reason: Instruction limit % 151.79/21.67 % (845333)Termination phase: Saturation % 151.79/21.67 % (845333)Time elapsed: 4.133 s % 151.79/21.67 % (845333)Peak memory usage: 109 MB % 151.79/21.67 % (845333)Instructions burned: 17632 (million) % 151.79/21.67 % (845619)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2757729798:i=206:fgj=on:rtra=on_2854 on theBenchmark for (2854ds/206Mi) % 151.79/21.67 % (845619)Instruction limit reached! % 151.79/21.67 % (845619)------------------------------ % 151.79/21.67 % (845619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.79/21.67 % (845619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.79/21.67 % (845619)CaDiCaL version: 2.1.3 % 151.79/21.67 % (845619)Termination reason: Instruction limit % 151.79/21.67 % (845619)Termination phase: Saturation % 151.79/21.67 % (845619)Time elapsed: 0.044 s % 151.79/21.67 % (845619)Peak memory usage: 12 MB % 151.79/21.67 % (845619)Instructions burned: 209 (million) % 151.79/21.67 % (845621)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4047144501:i=232:rtra=on_2854 on theBenchmark for (2854ds/232Mi) % 151.79/21.67 % (845621)Instruction limit reached! % 151.79/21.67 % (845621)------------------------------ % 151.79/21.67 % (845621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.79/21.67 % (845621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.79/21.67 % (845621)CaDiCaL version: 2.1.3 % 151.79/21.67 % (845621)Termination reason: Instruction limit % 151.79/21.67 % (845621)Termination phase: Saturation % 151.79/21.67 % (845621)Time elapsed: 0.084 s % 151.79/21.67 % (845621)Peak memory usage: 12 MB % 151.79/21.67 % (845621)Instructions burned: 233 (million) % 151.79/21.67 % (845638)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3195182893:i=262:rtra=on_2853 on theBenchmark for (2853ds/262Mi) % 151.79/21.67 % (845638)Instruction limit reached! % 151.79/21.67 % (845638)------------------------------ % 151.79/21.67 % (845638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.79/21.67 % (845638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.79/21.67 % (845638)CaDiCaL version: 2.1.3 % 151.79/21.67 % (845638)Termination reason: Instruction limit % 151.79/21.67 % (845638)Termination phase: Saturation % 151.79/21.67 % (845638)Time elapsed: 0.097 s % 151.79/21.67 % (845638)Peak memory usage: 12 MB % 151.79/21.67 % (845638)Instructions burned: 263 (million) % 151.79/21.67 % (845651)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2165787857:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2852 on theBenchmark for (2852ds/318Mi) % 151.79/21.67 % (845651)Instruction limit reached! % 151.79/21.67 % (845651)------------------------------ % 151.79/21.67 % (845651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.79/21.67 % (845651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.79/21.67 % (845651)CaDiCaL version: 2.1.3 % 151.79/21.67 % (845651)Termination reason: Instruction limit % 151.79/21.67 % (845651)Termination phase: Saturation % 151.79/21.67 % (845651)Time elapsed: 0.126 s % 151.79/21.67 % (845651)Peak memory usage: 13 MB % 151.79/21.67 % (845651)Instructions burned: 320 (million) % 151.79/21.67 % (845659)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2072700675:i=1428:nm=2:rtra=on_2850 on theBenchmark for (2850ds/1428Mi) % 151.79/21.67 % (845659)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 151.79/21.67 % (845659)Terminated due to inappropriate strategy. % 151.79/21.67 % (845659)------------------------------ % 151.79/21.67 % (845659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 151.79/21.67 % (845659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.79/21.67 % (845659)CaDiCaL version: 2.1.3 % 151.79/21.67 % (845659)Termination reason: Inappropriate % 151.79/21.67 % (845659)Time elapsed: 0.014 s % 151.79/21.67 % (845659)Peak memory usage: 10 MB % 151.79/21.67 % (845659)Instructions burned: 17 (million) % 151.79/21.67 % (845659)------------------------------ % 214.38/30.43 % (845659)------------------------------ % 214.38/30.43 % (845663)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2376925954:i=262:bd=preordered:rtra=on:fsd=on_2850 on theBenchmark for (2850ds/262Mi) % 214.38/30.43 % (845663)Instruction limit reached! % 214.38/30.43 % (845663)------------------------------ % 214.38/30.43 % (845663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.38/30.43 % (845663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.38/30.43 % (845663)CaDiCaL version: 2.1.3 % 214.38/30.43 % (845663)Termination reason: Instruction limit % 214.38/30.43 % (845663)Termination phase: Saturation % 214.38/30.43 % (845663)Time elapsed: 0.197 s % 214.38/30.43 % (845663)Peak memory usage: 12 MB % 214.38/30.43 % (845663)Instructions burned: 263 (million) % 214.38/30.43 % (845669)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=3809953112:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2848 on theBenchmark for (2848ds/1368Mi) % 214.38/30.43 % (845669)Instruction limit reached! % 214.38/30.43 % (845669)------------------------------ % 214.38/30.43 % (845669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.38/30.43 % (845669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.38/30.43 % (845669)CaDiCaL version: 2.1.3 % 214.38/30.43 % (845669)Termination reason: Instruction limit % 214.38/30.43 % (845669)Termination phase: Saturation % 214.38/30.43 % (845669)Time elapsed: 1.103 s % 214.38/30.43 % (845669)Peak memory usage: 19 MB % 214.38/30.43 % (845669)Instructions burned: 1369 (million) % 214.38/30.43 % (845692)ott-21_1_sil=16000:si=on:fs=off:random_seed=4030922629:i=360:av=off:fsr=off:rtra=on_2836 on theBenchmark for (2836ds/360Mi) % 214.38/30.43 % (845692)Instruction limit reached! % 214.38/30.43 % (845692)------------------------------ % 214.38/30.43 % (845692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.38/30.43 % (845692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.38/30.43 % (845692)CaDiCaL version: 2.1.3 % 214.38/30.43 % (845692)Termination reason: Instruction limit % 214.38/30.43 % (845692)Termination phase: Saturation % 214.38/30.43 % (845692)Time elapsed: 0.272 s % 214.38/30.43 % (845692)Peak memory usage: 12 MB % 214.38/30.43 % (845692)Instructions burned: 360 (million) % 214.38/30.43 % (845696)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3880510052:i=954:bd=all:rtra=on_2833 on theBenchmark for (2833ds/954Mi) % 214.38/30.43 % (845696)Instruction limit reached! % 214.38/30.43 % (845696)------------------------------ % 214.38/30.43 % (845696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.38/30.43 % (845696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.38/30.43 % (845696)CaDiCaL version: 2.1.3 % 214.38/30.43 % (845696)Termination reason: Instruction limit % 214.38/30.43 % (845696)Termination phase: Saturation % 214.38/30.43 % (845696)Time elapsed: 0.716 s % 214.38/30.43 % (845696)Peak memory usage: 13 MB % 214.38/30.43 % (845696)Instructions burned: 955 (million) % 214.38/30.43 % (845702)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3788338447:fmbsr=1.3:i=1730:ins=25:rtra=on_2826 on theBenchmark for (2826ds/1730Mi) % 214.38/30.43 % (845702)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 214.38/30.43 % (845702)Terminated due to inappropriate strategy. % 214.38/30.43 % (845702)------------------------------ % 214.38/30.43 % (845702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.38/30.43 % (845702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.38/30.43 % (845702)CaDiCaL version: 2.1.3 % 214.38/30.43 % (845702)Termination reason: Inappropriate % 214.38/30.43 % (845702)Time elapsed: 0.011 s % 214.38/30.43 % (845702)Peak memory usage: 11 MB % 214.38/30.43 % (845702)Instructions burned: 12 (million) % 214.38/30.43 % (845702)------------------------------ % 214.38/30.43 % (845702)------------------------------ % 214.38/30.43 % (845704)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2394330368:i=2358:rtra=on_2825 on theBenchmark for (2825ds/2358Mi) % 214.38/30.43 % (845704)Instruction limit reached! % 214.38/30.43 % (845704)------------------------------ % 214.38/30.43 % (845704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 214.38/30.43 % (845704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.38/30.43 % (845704)CaDiCaL version: 2.1.3 % 214.38/30.43 % (845704)Termination reason: Instruction limit % 289.08/41.04 % (845704)Termination phase: Saturation % 289.08/41.04 % (845704)Time elapsed: 1.575 s % 289.08/41.04 % (845704)Peak memory usage: 14 MB % 289.08/41.04 % (845704)Instructions burned: 2358 (million) % 289.08/41.04 % (845714)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=578336422:i=1778:ins=1:rtra=on_2809 on theBenchmark for (2809ds/1778Mi) % 289.08/41.04 % (845714)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 289.08/41.04 % (845714)Terminated due to inappropriate strategy. % 289.08/41.04 % (845714)------------------------------ % 289.08/41.04 % (845714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.08/41.04 % (845714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.08/41.04 % (845714)CaDiCaL version: 2.1.3 % 289.08/41.04 % (845714)Termination reason: Inappropriate % 289.08/41.04 % (845714)Time elapsed: 0.006 s % 289.08/41.04 % (845714)Peak memory usage: 10 MB % 289.08/41.04 % (845714)Instructions burned: 12 (million) % 289.08/41.04 % (845714)------------------------------ % 289.08/41.04 % (845714)------------------------------ % 289.08/41.04 % (845716)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=1102488255:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2809 on theBenchmark for (2809ds/1384Mi) % 289.08/41.04 % (845716)Instruction limit reached! % 289.08/41.04 % (845716)------------------------------ % 289.08/41.04 % (845716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.08/41.04 % (845716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.08/41.04 % (845716)CaDiCaL version: 2.1.3 % 289.08/41.04 % (845716)Termination reason: Instruction limit % 289.08/41.04 % (845716)Termination phase: Saturation % 289.08/41.04 % (845716)Time elapsed: 1.010 s % 289.08/41.04 % (845716)Peak memory usage: 15 MB % 289.08/41.04 % (845716)Instructions burned: 1384 (million) % 289.08/41.04 % (845726)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1234312377:i=1758:kws=inv_precedence:fsr=off:rtra=on_2799 on theBenchmark for (2799ds/1758Mi) % 289.08/41.04 % (845726)Instruction limit reached! % 289.08/41.04 % (845726)------------------------------ % 289.08/41.04 % (845726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.08/41.04 % (845726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.08/41.04 % (845726)CaDiCaL version: 2.1.3 % 289.08/41.04 % (845726)Termination reason: Instruction limit % 289.08/41.04 % (845726)Termination phase: Saturation % 289.08/41.04 % (845726)Time elapsed: 1.248 s % 289.08/41.04 % (845726)Peak memory usage: 15 MB % 289.08/41.04 % (845726)Instructions burned: 1758 (million) % 289.08/41.04 % (845728)fmb+10_1_sil=64000:si=on:random_seed=2277338340:i=44122:nm=2:rtra=on:gsp=on_2786 on theBenchmark for (2786ds/44122Mi) % 289.08/41.04 % (845728)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 289.08/41.04 % (845728)Terminated due to inappropriate strategy. % 289.08/41.04 % (845728)------------------------------ % 289.08/41.04 % (845728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.08/41.04 % (845728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.08/41.04 % (845728)CaDiCaL version: 2.1.3 % 289.08/41.04 % (845728)Termination reason: Inappropriate % 289.08/41.04 % (845728)Time elapsed: 0.009 s % 289.08/41.04 % (845728)Peak memory usage: 10 MB % 289.08/41.04 % (845728)Instructions burned: 16 (million) % 289.08/41.04 % (845728)------------------------------ % 289.08/41.04 % (845728)------------------------------ % 289.08/41.04 % (845730)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=367566241:i=19030:nm=5:rtra=on_2785 on theBenchmark for (2785ds/19030Mi) % 289.08/41.04 % (845730)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 289.08/41.04 % (845730)Terminated due to inappropriate strategy. % 289.08/41.04 % (845730)------------------------------ % 289.08/41.04 % (845730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.08/41.04 % (845730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.08/41.04 % (845730)CaDiCaL version: 2.1.3 % 289.08/41.04 % (845730)Termination reason: Inappropriate % 289.08/41.04 % (845730)Time elapsed: 0.008 s % 289.08/41.04 % (845730)Peak memory usage: 10 MB % 289.08/41.04 % (845730)Instructions burned: 16 (million) % 289.08/41.04 % (845730)------------------------------ % 289.08/41.04 % (845730)------------------------------ % 289.08/41.04 % (845732)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2304929919:fmbTerminated %------------------------------------------------------------------------------