%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX147_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 : n013.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 300.37s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX147_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.07/0.19 % Computer : n013.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 15:04:06 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.23 Running first-order model finding % 0.07/0.23 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 % 3.31/0.82 % (1251514)Will run a generic schedule for satisfiability detection. % 3.31/0.82 % (1251550)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3751150326:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.31/0.82 % (1251546)% WARNING: option uhcvi not known. % 3.31/0.82 % (1251548)dis+10_1_sil=32000:sp=arity:random_seed=1466659471:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.31/0.82 % (1251545)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2474696400_2999 on theBenchmark for (2999ds/0Mi) % 3.31/0.82 % (1251547)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3760887965:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.31/0.82 % (1251546)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3221693511:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.31/0.82 % (1251549)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1754591844:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.31/0.82 % (1251551)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4144228645:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.31/0.82 % (1251545)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.31/0.82 % (1251545)Terminated due to inappropriate strategy. % 3.31/0.82 % (1251545)------------------------------ % 3.31/0.82 % (1251545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.31/0.82 % (1251545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.31/0.82 % (1251545)CaDiCaL version: 2.1.3 % 3.31/0.82 % (1251545)Termination reason: Inappropriate % 3.31/0.82 % (1251545)Time elapsed: 0.025 s % 3.31/0.82 % (1251545)Peak memory usage: 11 MB % 3.31/0.82 % (1251545)Instructions burned: 60 (million) % 3.31/0.82 % (1251550)Instruction limit reached! % 3.31/0.82 % (1251550)------------------------------ % 3.31/0.82 % (1251550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.31/0.82 % (1251550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.31/0.82 % (1251550)CaDiCaL version: 2.1.3 % 3.31/0.82 % (1251550)Termination reason: Instruction limit % 3.31/0.82 % (1251550)Termination phase: Saturation % 3.31/0.82 % (1251550)Time elapsed: 0.033 s % 3.31/0.82 % (1251550)Peak memory usage: 14 MB % 3.31/0.82 % (1251550)Instructions burned: 132 (million) % 3.31/0.82 % (1251545)------------------------------ % 3.31/0.82 % (1251545)------------------------------ % 3.31/0.82 % (1251575)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=834679658:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 3.31/0.82 % (1251548)Instruction limit reached! % 3.31/0.82 % (1251548)------------------------------ % 3.31/0.82 % (1251548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.31/0.82 % (1251548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.31/0.82 % (1251548)CaDiCaL version: 2.1.3 % 3.31/0.82 % (1251548)Termination reason: Instruction limit % 3.31/0.82 % (1251548)Termination phase: Saturation % 3.31/0.82 % (1251548)Time elapsed: 0.044 s % 3.31/0.82 % (1251548)Peak memory usage: 12 MB % 3.31/0.82 % (1251548)Instructions burned: 104 (million) % 3.31/0.82 % (1251576)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=506557526:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 3.31/0.82 % (1251549)Instruction limit reached! % 3.31/0.82 % (1251549)------------------------------ % 3.31/0.82 % (1251549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.31/0.82 % (1251549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.31/0.82 % (1251549)CaDiCaL version: 2.1.3 % 3.31/0.82 % (1251549)Termination reason: Instruction limit % 3.31/0.82 % (1251549)Termination phase: Saturation % 3.31/0.82 % (1251549)Time elapsed: 0.050 s % 3.31/0.82 % (1251549)Peak memory usage: 13 MB % 3.31/0.82 % (1251549)Instructions burned: 116 (million) % 3.31/0.82 % (1251575)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.31/0.82 % (1251575)Terminated due to inappropriate strategy. % 3.31/0.82 % (1251575)------------------------------ % 3.31/0.82 % (1251575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.31/0.82 % (1251575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.31/0.82 % (1251575)CaDiCaL version: 2.1.3 % 3.31/0.82 % (1251575)Termination reason: Inappropriate % 3.31/0.82 % (1251575)Time elapsed: 0.013 s % 3.77/0.98 % (1251575)Peak memory usage: 11 MB % 3.77/0.98 % (1251575)Instructions burned: 60 (million) % 3.77/0.98 % (1251575)------------------------------ % 3.77/0.98 % (1251575)------------------------------ % 3.77/0.98 % (1251587)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=566542931:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 3.77/0.98 % (1251583)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=3554190856:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 3.77/0.98 % (1251585)ott-21_1_sil=16000:fs=off:random_seed=956599748:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 3.77/0.98 % (1251551)Instruction limit reached! % 3.77/0.98 % (1251551)------------------------------ % 3.77/0.98 % (1251551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.77/0.98 % (1251551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.77/0.98 % (1251551)CaDiCaL version: 2.1.3 % 3.77/0.98 % (1251551)Termination reason: Instruction limit % 3.77/0.98 % (1251551)Termination phase: Saturation % 3.77/0.98 % (1251551)Time elapsed: 0.082 s % 3.77/0.98 % (1251551)Peak memory usage: 14 MB % 3.77/0.98 % (1251551)Instructions burned: 161 (million) % 3.77/0.98 % (1251603)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1854849325:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 3.77/0.98 % (1251576)Instruction limit reached! % 3.77/0.98 % (1251576)------------------------------ % 3.77/0.98 % (1251576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.77/0.98 % (1251576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.77/0.98 % (1251576)CaDiCaL version: 2.1.3 % 3.77/0.98 % (1251576)Termination reason: Instruction limit % 3.77/0.98 % (1251576)Termination phase: Saturation % 3.77/0.98 % (1251576)Time elapsed: 0.057 s % 3.77/0.98 % (1251576)Peak memory usage: 14 MB % 3.77/0.98 % (1251576)Instructions burned: 134 (million) % 3.77/0.98 % (1251603)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.77/0.98 % (1251603)Terminated due to inappropriate strategy. % 3.77/0.98 % (1251603)------------------------------ % 3.77/0.98 % (1251603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.77/0.98 % (1251603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.77/0.98 % (1251603)CaDiCaL version: 2.1.3 % 3.77/0.98 % (1251603)Termination reason: Inappropriate % 3.77/0.98 % (1251603)Time elapsed: 0.019 s % 3.77/0.98 % (1251603)Peak memory usage: 11 MB % 3.77/0.98 % (1251603)Instructions burned: 45 (million) % 3.77/0.98 % (1251609)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3339761926:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 3.77/0.98 % (1251603)------------------------------ % 3.77/0.98 % (1251603)------------------------------ % 3.77/0.98 % (1251622)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4167169149:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 3.77/0.98 % (1251585)Instruction limit reached! % 3.77/0.98 % (1251585)------------------------------ % 3.77/0.98 % (1251585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.77/0.98 % (1251585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.77/0.98 % (1251585)CaDiCaL version: 2.1.3 % 3.77/0.98 % (1251585)Termination reason: Instruction limit % 3.77/0.98 % (1251585)Termination phase: Saturation % 3.77/0.98 % (1251585)Time elapsed: 0.078 s % 3.77/0.98 % (1251585)Peak memory usage: 14 MB % 3.77/0.98 % (1251585)Instructions burned: 182 (million) % 3.77/0.98 % (1251622)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.77/0.98 % (1251622)Terminated due to inappropriate strategy. % 3.77/0.98 % (1251622)------------------------------ % 3.77/0.98 % (1251622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.77/0.98 % (1251622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.77/0.98 % (1251622)CaDiCaL version: 2.1.3 % 3.77/0.98 % (1251622)Termination reason: Inappropriate % 3.77/0.98 % (1251622)Time elapsed: 0.019 s % 3.77/0.98 % (1251622)Peak memory usage: 11 MB % 3.77/0.98 % (1251622)Instructions burned: 45 (million) % 3.77/0.98 % (1251622)------------------------------ % 3.77/0.98 % (1251622)------------------------------ % 3.77/0.98 % (1251587)Instruction limit reached! % 3.77/0.98 % (1251587)------------------------------ % 3.77/0.98 % (1251587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.27/2.38 % (1251587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.27/2.38 % (1251587)CaDiCaL version: 2.1.3 % 14.27/2.38 % (1251587)Termination reason: Instruction limit % 14.27/2.38 % (1251587)Termination phase: Saturation % 14.27/2.38 % (1251587)Time elapsed: 0.104 s % 14.27/2.38 % (1251587)Peak memory usage: 14 MB % 14.27/2.38 % (1251587)Instructions burned: 480 (million) % 14.27/2.38 % (1251640)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=198979685:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 14.27/2.38 % (1251650)fmb+10_1_sil=64000:random_seed=3318171036:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 14.27/2.38 % (1251647)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=345999220:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 14.27/2.38 % (1251650)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.27/2.38 % (1251650)Terminated due to inappropriate strategy. % 14.27/2.38 % (1251650)------------------------------ % 14.27/2.38 % (1251650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.27/2.38 % (1251650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.27/2.38 % (1251650)CaDiCaL version: 2.1.3 % 14.27/2.38 % (1251650)Termination reason: Inappropriate % 14.27/2.38 % (1251650)Time elapsed: 0.013 s % 14.27/2.38 % (1251650)Peak memory usage: 11 MB % 14.27/2.38 % (1251650)Instructions burned: 60 (million) % 14.27/2.38 % (1251650)------------------------------ % 14.27/2.38 % (1251650)------------------------------ % 14.27/2.38 % (1251657)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1352743420:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 14.27/2.38 % (1251657)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.27/2.38 % (1251657)Terminated due to inappropriate strategy. % 14.27/2.38 % (1251657)------------------------------ % 14.27/2.38 % (1251657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.27/2.38 % (1251657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.27/2.38 % (1251657)CaDiCaL version: 2.1.3 % 14.27/2.38 % (1251657)Termination reason: Inappropriate % 14.27/2.38 % (1251657)Time elapsed: 0.013 s % 14.27/2.38 % (1251657)Peak memory usage: 11 MB % 14.27/2.38 % (1251657)Instructions burned: 60 (million) % 14.27/2.38 % (1251657)------------------------------ % 14.27/2.38 % (1251657)------------------------------ % 14.27/2.38 % (1251659)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=897263152:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 14.27/2.38 % (1251659)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 14.27/2.38 % (1251659)Terminated due to inappropriate strategy. % 14.27/2.38 % (1251659)------------------------------ % 14.27/2.38 % (1251659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.27/2.38 % (1251659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.27/2.38 % (1251659)CaDiCaL version: 2.1.3 % 14.27/2.38 % (1251659)Termination reason: Inappropriate % 14.27/2.38 % (1251659)Time elapsed: 0.013 s % 14.27/2.38 % (1251659)Peak memory usage: 11 MB % 14.27/2.38 % (1251659)Instructions burned: 60 (million) % 14.27/2.38 % (1251659)------------------------------ % 14.27/2.38 % (1251659)------------------------------ % 14.27/2.38 % (1251661)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3738123066:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 14.27/2.38 % (1251583)Instruction limit reached! % 14.27/2.38 % (1251583)------------------------------ % 14.27/2.38 % (1251583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.27/2.38 % (1251583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.27/2.38 % (1251583)CaDiCaL version: 2.1.3 % 14.27/2.38 % (1251583)Termination reason: Instruction limit % 14.27/2.38 % (1251583)Termination phase: Saturation % 14.27/2.38 % (1251583)Time elapsed: 0.282 s % 14.27/2.38 % (1251583)Peak memory usage: 16 MB % 14.27/2.38 % (1251583)Instructions burned: 686 (million) % 14.27/2.38 % (1251663)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1006434262:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 14.27/2.38 % (1251640)Instruction limit reached! % 14.27/2.38 % (1251640)------------------------------ % 16.85/2.89 % (1251640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.89 % (1251640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/2.89 % (1251640)CaDiCaL version: 2.1.3 % 16.85/2.89 % (1251640)Termination reason: Instruction limit % 16.85/2.89 % (1251640)Termination phase: Saturation % 16.85/2.89 % (1251640)Time elapsed: 0.333 s % 16.85/2.89 % (1251640)Peak memory usage: 19 MB % 16.85/2.89 % (1251640)Instructions burned: 693 (million) % 16.85/2.89 % (1251665)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2578285389:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 16.85/2.89 % (1251647)Instruction limit reached! % 16.85/2.89 % (1251647)------------------------------ % 16.85/2.89 % (1251647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.89 % (1251647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/2.89 % (1251647)CaDiCaL version: 2.1.3 % 16.85/2.89 % (1251647)Termination reason: Instruction limit % 16.85/2.89 % (1251647)Termination phase: Saturation % 16.85/2.89 % (1251647)Time elapsed: 0.347 s % 16.85/2.89 % (1251647)Peak memory usage: 15 MB % 16.85/2.89 % (1251647)Instructions burned: 880 (million) % 16.85/2.89 % (1251665)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.85/2.89 % (1251665)Terminated due to inappropriate strategy. % 16.85/2.89 % (1251665)------------------------------ % 16.85/2.89 % (1251665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.89 % (1251665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/2.89 % (1251665)CaDiCaL version: 2.1.3 % 16.85/2.89 % (1251665)Termination reason: Inappropriate % 16.85/2.89 % (1251665)Time elapsed: 0.024 s % 16.85/2.89 % (1251665)Peak memory usage: 11 MB % 16.85/2.89 % (1251665)Instructions burned: 60 (million) % 16.85/2.89 % (1251665)------------------------------ % 16.85/2.89 % (1251665)------------------------------ % 16.85/2.89 % (1251667)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1213423:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 16.85/2.89 % (1251669)ott-2_1_sil=16000:newcnf=on:random_seed=2281760797:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 16.85/2.89 % (1251667)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.85/2.89 % (1251667)Terminated due to inappropriate strategy. % 16.85/2.89 % (1251667)------------------------------ % 16.85/2.89 % (1251667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.89 % (1251667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/2.89 % (1251667)CaDiCaL version: 2.1.3 % 16.85/2.89 % (1251667)Termination reason: Inappropriate % 16.85/2.89 % (1251667)Time elapsed: 0.024 s % 16.85/2.89 % (1251667)Peak memory usage: 11 MB % 16.85/2.89 % (1251667)Instructions burned: 60 (million) % 16.85/2.89 % (1251667)------------------------------ % 16.85/2.89 % (1251667)------------------------------ % 16.85/2.89 % (1251671)ott+10_1_sil=32000:tgt=ground:random_seed=3937193618:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 16.85/2.89 % (1251609)Instruction limit reached! % 16.85/2.89 % (1251609)------------------------------ % 16.85/2.89 % (1251609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.89 % (1251609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/2.89 % (1251609)CaDiCaL version: 2.1.3 % 16.85/2.89 % (1251609)Termination reason: Instruction limit % 16.85/2.89 % (1251609)Termination phase: Saturation % 16.85/2.89 % (1251609)Time elapsed: 0.487 s % 16.85/2.89 % (1251609)Peak memory usage: 17 MB % 16.85/2.89 % (1251609)Instructions burned: 1180 (million) % 16.85/2.89 % (1251673)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=15443457:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 16.85/2.89 % (1251673)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.85/2.89 % (1251673)Terminated due to inappropriate strategy. % 16.85/2.89 % (1251673)------------------------------ % 16.85/2.89 % (1251673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.89 % (1251673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/2.89 % (1251673)CaDiCaL version: 2.1.3 % 16.85/2.89 % (1251673)Termination reason: Inappropriate % 16.85/2.89 % (1251673)Time elapsed: 0.024 s % 16.85/2.89 % (1251673)Peak memory usage: 11 MB % 16.85/2.89 % (1251673)Instructions burned: 60 (million) % 71.12/10.32 % (1251673)------------------------------ % 71.12/10.32 % (1251673)------------------------------ % 71.12/10.32 % (1251675)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2835580064:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 71.12/10.32 % (1251669)Instruction limit reached! % 71.12/10.32 % (1251669)------------------------------ % 71.12/10.32 % (1251669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.12/10.32 % (1251669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.12/10.32 % (1251669)CaDiCaL version: 2.1.3 % 71.12/10.32 % (1251669)Termination reason: Instruction limit % 71.12/10.32 % (1251669)Termination phase: Saturation % 71.12/10.32 % (1251669)Time elapsed: 0.404 s % 71.12/10.32 % (1251669)Peak memory usage: 18 MB % 71.12/10.32 % (1251669)Instructions burned: 872 (million) % 71.12/10.32 % (1251677)dis+21_1_sil=32000:sas=cadical:random_seed=3864922378:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 71.12/10.32 % (1251663)Instruction limit reached! % 71.12/10.32 % (1251663)------------------------------ % 71.12/10.32 % (1251663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.12/10.32 % (1251663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.12/10.32 % (1251663)CaDiCaL version: 2.1.3 % 71.12/10.32 % (1251663)Termination reason: Instruction limit % 71.12/10.32 % (1251663)Termination phase: Saturation % 71.12/10.32 % (1251663)Time elapsed: 0.658 s % 71.12/10.32 % (1251663)Peak memory usage: 17 MB % 71.12/10.32 % (1251663)Instructions burned: 1472 (million) % 71.12/10.32 % (1251679)ott+11_1_sil=16000:gs=on:random_seed=3285524673:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 71.12/10.32 % (1251661)Instruction limit reached! % 71.12/10.32 % (1251661)------------------------------ % 71.12/10.32 % (1251661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.12/10.32 % (1251661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.12/10.32 % (1251661)CaDiCaL version: 2.1.3 % 71.12/10.32 % (1251661)Termination reason: Instruction limit % 71.12/10.32 % (1251661)Termination phase: Saturation % 71.12/10.32 % (1251661)Time elapsed: 1.058 s % 71.12/10.32 % (1251661)Peak memory usage: 17 MB % 71.12/10.32 % (1251661)Instructions burned: 5132 (million) % 71.12/10.32 % (1251681)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=441291313:fmbsr=1.6:i=67534_2986 on theBenchmark for (2986ds/67534Mi) % 71.12/10.32 % (1251681)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 71.12/10.32 % (1251681)Terminated due to inappropriate strategy. % 71.12/10.32 % (1251681)------------------------------ % 71.12/10.32 % (1251681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.12/10.32 % (1251681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.12/10.32 % (1251681)CaDiCaL version: 2.1.3 % 71.12/10.32 % (1251681)Termination reason: Inappropriate % 71.12/10.32 % (1251681)Time elapsed: 0.013 s % 71.12/10.32 % (1251681)Peak memory usage: 11 MB % 71.12/10.32 % (1251681)Instructions burned: 60 (million) % 71.12/10.32 % (1251681)------------------------------ % 71.12/10.32 % (1251681)------------------------------ % 71.12/10.32 % (1251683)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1420204282:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2985 on theBenchmark for (2985ds/4591Mi) % 71.12/10.32 % (1251679)Instruction limit reached! % 71.12/10.32 % (1251679)------------------------------ % 71.12/10.32 % (1251679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.12/10.32 % (1251679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.12/10.32 % (1251679)CaDiCaL version: 2.1.3 % 71.12/10.32 % (1251679)Termination reason: Instruction limit % 71.12/10.32 % (1251679)Termination phase: Saturation % 71.12/10.32 % (1251679)Time elapsed: 0.877 s % 71.12/10.32 % (1251679)Peak memory usage: 17 MB % 71.12/10.32 % (1251679)Instructions burned: 2251 (million) % 71.12/10.32 % (1251685)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2991876511:i=29340_2979 on theBenchmark for (2979ds/29340Mi) % 71.12/10.32 % (1251675)Instruction limit reached! % 71.12/10.32 % (1251675)------------------------------ % 71.12/10.32 % (1251675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.12/10.32 % (1251675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.12/10.32 % (1251675)CaDiCaL version: 2.1.3 % 71.12/10.32 % (1251675)Termination reason: Instruction limit % 83.40/12.13 % (1251675)Termination phase: Saturation % 83.40/12.13 % (1251675)Time elapsed: 1.384 s % 83.40/12.13 % (1251675)Peak memory usage: 17 MB % 83.40/12.13 % (1251675)Instructions burned: 3514 (million) % 83.40/12.13 % (1251687)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1550516064:i=5211_2978 on theBenchmark for (2978ds/5211Mi) % 83.40/12.13 % (1251677)Instruction limit reached! % 83.40/12.13 % (1251677)------------------------------ % 83.40/12.13 % (1251677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.40/12.13 % (1251677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.40/12.13 % (1251677)CaDiCaL version: 2.1.3 % 83.40/12.13 % (1251677)Termination reason: Instruction limit % 83.40/12.13 % (1251677)Termination phase: Saturation % 83.40/12.13 % (1251677)Time elapsed: 1.439 s % 83.40/12.13 % (1251677)Peak memory usage: 17 MB % 83.40/12.13 % (1251677)Instructions burned: 3773 (million) % 83.40/12.13 % (1251689)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2463592261:i=5497:nm=2_2974 on theBenchmark for (2974ds/5497Mi) % 83.40/12.13 % (1251689)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.40/12.13 % (1251689)Terminated due to inappropriate strategy. % 83.40/12.13 % (1251689)------------------------------ % 83.40/12.13 % (1251689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.40/12.13 % (1251689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.40/12.13 % (1251689)CaDiCaL version: 2.1.3 % 83.40/12.13 % (1251689)Termination reason: Inappropriate % 83.40/12.13 % (1251689)Time elapsed: 0.024 s % 83.40/12.13 % (1251689)Peak memory usage: 11 MB % 83.40/12.13 % (1251689)Instructions burned: 60 (million) % 83.40/12.13 % (1251689)------------------------------ % 83.40/12.13 % (1251689)------------------------------ % 83.40/12.13 % (1251691)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2113026640:fmbsr=2:i=46332_2974 on theBenchmark for (2974ds/46332Mi) % 83.40/12.13 % (1251683)Instruction limit reached! % 83.40/12.13 % (1251683)------------------------------ % 83.40/12.13 % (1251683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.40/12.13 % (1251683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.40/12.13 % (1251683)CaDiCaL version: 2.1.3 % 83.40/12.13 % (1251683)Termination reason: Instruction limit % 83.40/12.13 % (1251683)Termination phase: Saturation % 83.40/12.13 % (1251683)Time elapsed: 1.171 s % 83.40/12.13 % (1251683)Peak memory usage: 31 MB % 83.40/12.13 % (1251683)Instructions burned: 4593 (million) % 83.40/12.13 % (1251691)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.40/12.13 % (1251691)Terminated due to inappropriate strategy. % 83.40/12.13 % (1251691)------------------------------ % 83.40/12.13 % (1251691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.40/12.13 % (1251691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.40/12.13 % (1251691)CaDiCaL version: 2.1.3 % 83.40/12.13 % (1251691)Termination reason: Inappropriate % 83.40/12.13 % (1251691)Time elapsed: 0.024 s % 83.40/12.13 % (1251691)Peak memory usage: 11 MB % 83.40/12.13 % (1251691)Instructions burned: 60 (million) % 83.40/12.13 % (1251691)------------------------------ % 83.40/12.13 % (1251691)------------------------------ % 83.40/12.13 % (1251693)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1411880780:i=14071_2973 on theBenchmark for (2973ds/14071Mi) % 83.40/12.13 % (1251693)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.40/12.13 % (1251693)Terminated due to inappropriate strategy. % 83.40/12.13 % (1251693)------------------------------ % 83.40/12.13 % (1251693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.40/12.13 % (1251693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.40/12.13 % (1251693)CaDiCaL version: 2.1.3 % 83.40/12.13 % (1251693)Termination reason: Inappropriate % 83.40/12.13 % (1251693)Time elapsed: 0.013 s % 83.40/12.13 % (1251693)Peak memory usage: 11 MB % 83.40/12.13 % (1251693)Instructions burned: 60 (million) % 83.40/12.13 % (1251694)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1194680753:i=22565:add=on:rawr=on_2973 on theBenchmark for (2973ds/22565Mi) % 83.40/12.13 % (1251693)------------------------------ % 83.40/12.13 % (1251693)------------------------------ % 83.40/12.13 % (1251697)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=366566173:i=8173:av=off_2973 on theBenchmark for (2973ds/8173Mi) % 83.40/12.13 % (1251671)Instruction limit reached! % 85.05/12.36 % (1251671)------------------------------ % 85.05/12.36 % (1251671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.05/12.36 % (1251671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.05/12.36 % (1251671)CaDiCaL version: 2.1.3 % 85.05/12.36 % (1251671)Termination reason: Instruction limit % 85.05/12.36 % (1251671)Termination phase: Saturation % 85.05/12.36 % (1251671)Time elapsed: 1.973 s % 85.05/12.36 % (1251671)Peak memory usage: 17 MB % 85.05/12.36 % (1251671)Instructions burned: 5116 (million) % 85.05/12.36 % (1251699)dis+10_16:1_sil=16000:random_seed=1895528089:i=9155:fsr=off_2973 on theBenchmark for (2973ds/9155Mi) % 85.05/12.36 % (1251687)Instruction limit reached! % 85.05/12.36 % (1251687)------------------------------ % 85.05/12.36 % (1251687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.05/12.36 % (1251687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.05/12.36 % (1251687)CaDiCaL version: 2.1.3 % 85.05/12.36 % (1251687)Termination reason: Instruction limit % 85.05/12.36 % (1251687)Termination phase: Saturation % 85.05/12.36 % (1251687)Time elapsed: 1.987 s % 85.05/12.36 % (1251687)Peak memory usage: 17 MB % 85.05/12.36 % (1251687)Instructions burned: 5212 (million) % 85.05/12.36 % (1251701)ott-3_8_sil=64000:random_seed=1858382373:i=20139:bs=on_2958 on theBenchmark for (2958ds/20139Mi) % 85.05/12.36 % (1251697)Instruction limit reached! % 85.05/12.36 % (1251697)------------------------------ % 85.05/12.36 % (1251697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.05/12.36 % (1251697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.05/12.36 % (1251697)CaDiCaL version: 2.1.3 % 85.05/12.36 % (1251697)Termination reason: Instruction limit % 85.05/12.36 % (1251697)Termination phase: Saturation % 85.05/12.36 % (1251697)Time elapsed: 1.714 s % 85.05/12.36 % (1251697)Peak memory usage: 17 MB % 85.05/12.36 % (1251697)Instructions burned: 8176 (million) % 85.05/12.36 % (1251703)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1806398654:fmbsr=2:i=32576_2956 on theBenchmark for (2956ds/32576Mi) % 85.05/12.36 % (1251703)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 85.05/12.36 % (1251703)Terminated due to inappropriate strategy. % 85.05/12.36 % (1251703)------------------------------ % 85.05/12.36 % (1251703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.05/12.36 % (1251703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.05/12.36 % (1251703)CaDiCaL version: 2.1.3 % 85.05/12.36 % (1251703)Termination reason: Inappropriate % 85.05/12.36 % (1251703)Time elapsed: 0.013 s % 85.05/12.36 % (1251703)Peak memory usage: 11 MB % 85.05/12.36 % (1251703)Instructions burned: 60 (million) % 85.05/12.36 % (1251703)------------------------------ % 85.05/12.36 % (1251703)------------------------------ % 85.05/12.36 % (1251705)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2475586914:i=11404_2956 on theBenchmark for (2956ds/11404Mi) % 85.05/12.36 % (1251699)Instruction limit reached! % 85.05/12.36 % (1251699)------------------------------ % 85.05/12.36 % (1251699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.05/12.36 % (1251699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.05/12.36 % (1251699)CaDiCaL version: 2.1.3 % 85.05/12.36 % (1251699)Termination reason: Instruction limit % 85.05/12.36 % (1251699)Termination phase: Saturation % 85.05/12.36 % (1251699)Time elapsed: 3.450 s % 85.05/12.36 % (1251699)Peak memory usage: 19 MB % 85.05/12.36 % (1251699)Instructions burned: 9157 (million) % 85.05/12.36 % (1251707)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=173771870:i=14134_2938 on theBenchmark for (2938ds/14134Mi) % 85.05/12.36 % (1251705)Instruction limit reached! % 85.05/12.36 % (1251705)------------------------------ % 85.05/12.36 % (1251705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.05/12.36 % (1251705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.05/12.36 % (1251705)CaDiCaL version: 2.1.3 % 85.05/12.36 % (1251705)Termination reason: Instruction limit % 85.05/12.36 % (1251705)Termination phase: Saturation % 85.05/12.36 % (1251705)Time elapsed: 2.373 s % 85.05/12.36 % (1251705)Peak memory usage: 18 MB % 85.05/12.36 % (1251705)Instructions burned: 11407 (million) % 85.05/12.36 % (1251709)dis+33_16_sil=32000:sac=on:random_seed=2706939803:i=15851:nm=0_2932 on theBenchmark for (2932ds/15851Mi) % 85.05/12.36 % (1251709)Instruction limit reached! % 85.05/12.36 % (1251709)------------------------------ % 85.05/12.36 % (1251709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.34/14.70 % (1251709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.34/14.70 % (1251709)CaDiCaL version: 2.1.3 % 102.34/14.70 % (1251709)Termination reason: Instruction limit % 102.34/14.70 % (1251709)Termination phase: Saturation % 102.34/14.70 % (1251709)Time elapsed: 3.308 s % 102.34/14.70 % (1251709)Peak memory usage: 23 MB % 102.34/14.70 % (1251709)Instructions burned: 15852 (million) % 102.34/14.70 % (1251711)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3750041617:avsq=on:i=17627:add=on:amm=off_2899 on theBenchmark for (2899ds/17627Mi) % 102.34/14.70 % (1251707)Instruction limit reached! % 102.34/14.70 % (1251707)------------------------------ % 102.34/14.70 % (1251707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.34/14.70 % (1251707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.34/14.70 % (1251707)CaDiCaL version: 2.1.3 % 102.34/14.70 % (1251707)Termination reason: Instruction limit % 102.34/14.70 % (1251707)Termination phase: Saturation % 102.34/14.70 % (1251707)Time elapsed: 5.479 s % 102.34/14.70 % (1251707)Peak memory usage: 18 MB % 102.34/14.70 % (1251707)Instructions burned: 14134 (million) % 102.34/14.70 % (1251713)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1838120403:s2a=on:i=53295_2883 on theBenchmark for (2883ds/53295Mi) % 102.34/14.70 % (1251701)Instruction limit reached! % 102.34/14.70 % (1251701)------------------------------ % 102.34/14.70 % (1251701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.34/14.70 % (1251701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.34/14.70 % (1251701)CaDiCaL version: 2.1.3 % 102.34/14.70 % (1251701)Termination reason: Instruction limit % 102.34/14.70 % (1251701)Termination phase: Saturation % 102.34/14.70 % (1251701)Time elapsed: 7.600 s % 102.34/14.70 % (1251701)Peak memory usage: 20 MB % 102.34/14.70 % (1251701)Instructions burned: 20139 (million) % 102.34/14.70 % (1251694)Instruction limit reached! % 102.34/14.70 % (1251694)------------------------------ % 102.34/14.70 % (1251694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.34/14.70 % (1251694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.34/14.70 % (1251694)CaDiCaL version: 2.1.3 % 102.34/14.70 % (1251694)Termination reason: Instruction limit % 102.34/14.70 % (1251694)Termination phase: Saturation % 102.34/14.70 % (1251694)Time elapsed: 9.166 s % 102.34/14.70 % (1251694)Peak memory usage: 18 MB % 102.34/14.70 % (1251694)Instructions burned: 22567 (million) % 102.34/14.70 % (1251715)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1539615236:i=26857:ins=20_2882 on theBenchmark for (2882ds/26857Mi) % 102.34/14.70 % (1251717)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3253200681:i=28120:bs=on:fsr=off_2882 on theBenchmark for (2882ds/28120Mi) % 102.34/14.70 % (1251715)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 102.34/14.70 % (1251715)Terminated due to inappropriate strategy. % 102.34/14.70 % (1251715)------------------------------ % 102.34/14.70 % (1251715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.34/14.70 % (1251715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.34/14.70 % (1251715)CaDiCaL version: 2.1.3 % 102.34/14.70 % (1251715)Termination reason: Inappropriate % 102.34/14.70 % (1251715)Time elapsed: 0.025 s % 102.34/14.70 % (1251715)Peak memory usage: 11 MB % 102.34/14.70 % (1251715)Instructions burned: 60 (million) % 102.34/14.70 % (1251715)------------------------------ % 102.34/14.70 % (1251715)------------------------------ % 102.34/14.70 % (1251719)fmb+10_1_sil=256000:fmbss=7:random_seed=1645718166:fmbsr=1.6:i=182295_2881 on theBenchmark for (2881ds/182295Mi) % 102.34/14.70 % (1251719)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 102.34/14.70 % (1251719)Terminated due to inappropriate strategy. % 102.34/14.70 % (1251719)------------------------------ % 102.34/14.70 % (1251719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 102.34/14.70 % (1251719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.34/14.70 % (1251719)CaDiCaL version: 2.1.3 % 102.34/14.70 % (1251719)Termination reason: Inappropriate % 102.34/14.70 % (1251719)Time elapsed: 0.024 s % 102.34/14.70 % (1251719)Peak memory usage: 11 MB % 102.34/14.70 % (1251719)Instructions burned: 60 (million) % 102.34/14.70 % (1251719)------------------------------ % 102.34/14.70 % (1251719)------------------------------ % 102.34/14.70 % (1251721)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2166396520:i=44625:gsp=on_2881 on theBenchmark for (2881ds/44625Mi) % 107.29/15.41 % (1251721)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 107.29/15.41 % (1251721)Terminated due to inappropriate strategy. % 107.29/15.41 % (1251721)------------------------------ % 107.29/15.41 % (1251721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.29/15.41 % (1251721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.29/15.41 % (1251721)CaDiCaL version: 2.1.3 % 107.29/15.41 % (1251721)Termination reason: Inappropriate % 107.29/15.41 % (1251721)Time elapsed: 0.025 s % 107.29/15.41 % (1251721)Peak memory usage: 11 MB % 107.29/15.41 % (1251721)Instructions burned: 60 (million) % 107.29/15.41 % (1251721)------------------------------ % 107.29/15.41 % (1251721)------------------------------ % 107.29/15.41 % (1251723)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1255624989:i=160505_2880 on theBenchmark for (2880ds/160505Mi) % 107.29/15.41 % (1251723)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 107.29/15.41 % (1251723)Terminated due to inappropriate strategy. % 107.29/15.41 % (1251723)------------------------------ % 107.29/15.41 % (1251723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.29/15.41 % (1251723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.29/15.41 % (1251723)CaDiCaL version: 2.1.3 % 107.29/15.41 % (1251723)Termination reason: Inappropriate % 107.29/15.41 % (1251723)Time elapsed: 0.024 s % 107.29/15.41 % (1251723)Peak memory usage: 11 MB % 107.29/15.41 % (1251723)Instructions burned: 60 (million) % 107.29/15.41 % (1251723)------------------------------ % 107.29/15.41 % (1251723)------------------------------ % 107.29/15.41 % (1251725)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2593279405:fmbsr=1.3:i=225729_2880 on theBenchmark for (2880ds/225729Mi) % 107.29/15.41 % (1251725)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 107.29/15.41 % (1251725)Terminated due to inappropriate strategy. % 107.29/15.41 % (1251725)------------------------------ % 107.29/15.41 % (1251725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.29/15.41 % (1251725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.29/15.41 % (1251725)CaDiCaL version: 2.1.3 % 107.29/15.41 % (1251725)Termination reason: Inappropriate % 107.29/15.41 % (1251725)Time elapsed: 0.024 s % 107.29/15.41 % (1251725)Peak memory usage: 11 MB % 107.29/15.41 % (1251725)Instructions burned: 60 (million) % 107.29/15.41 % (1251725)------------------------------ % 107.29/15.41 % (1251725)------------------------------ % 107.29/15.41 % (1251727)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3893546416:fmbsr=2:i=185024:ins=7_2879 on theBenchmark for (2879ds/185024Mi) % 107.29/15.41 % (1251727)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 107.29/15.41 % (1251727)Terminated due to inappropriate strategy. % 107.29/15.41 % (1251727)------------------------------ % 107.29/15.41 % (1251727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.29/15.41 % (1251727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.29/15.41 % (1251727)CaDiCaL version: 2.1.3 % 107.29/15.41 % (1251727)Termination reason: Inappropriate % 107.29/15.41 % (1251727)Time elapsed: 0.024 s % 107.29/15.41 % (1251727)Peak memory usage: 11 MB % 107.29/15.41 % (1251727)Instructions burned: 60 (million) % 107.29/15.41 % (1251727)------------------------------ % 107.29/15.41 % (1251727)------------------------------ % 107.29/15.41 % (1251729)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4877784:rtra=on_2879 on theBenchmark for (2879ds/0Mi) % 107.29/15.41 % (1251729)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 107.29/15.41 % (1251729)Terminated due to inappropriate strategy. % 107.29/15.41 % (1251729)------------------------------ % 107.29/15.41 % (1251729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.29/15.41 % (1251729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.29/15.41 % (1251729)CaDiCaL version: 2.1.3 % 107.29/15.41 % (1251729)Termination reason: Inappropriate % 107.29/15.41 % (1251729)Time elapsed: 0.025 s % 107.29/15.41 % (1251729)Peak memory usage: 11 MB % 107.29/15.41 % (1251729)Instructions burned: 61 (million) % 107.29/15.41 % (1251729)------------------------------ % 107.29/15.41 % (1251729)------------------------------ % 107.29/15.41 % (1251731)% WARNING: option uhcvi not known. % 107.29/15.41 % (1251731)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=583973822:i=271062:add=off:rtra=on:rawr=on_2878 on theBenchmark for (2878ds/271062Mi) % 115.47/16.65 % (1251685)Instruction limit reached! % 115.47/16.65 % (1251685)------------------------------ % 115.47/16.65 % (1251685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.47/16.65 % (1251685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.47/16.65 % (1251685)CaDiCaL version: 2.1.3 % 115.47/16.65 % (1251685)Termination reason: Instruction limit % 115.47/16.65 % (1251685)Termination phase: Saturation % 115.47/16.65 % (1251685)Time elapsed: 11.696 s % 115.47/16.65 % (1251685)Peak memory usage: 26 MB % 115.47/16.65 % (1251685)Instructions burned: 29342 (million) % 115.47/16.65 % (1251735)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=890584154:i=176048:add=on:rtra=on:rawr=on_2862 on theBenchmark for (2862ds/176048Mi) % 115.47/16.65 % (1251711)Instruction limit reached! % 115.47/16.65 % (1251711)------------------------------ % 115.47/16.65 % (1251711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.47/16.65 % (1251711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.47/16.65 % (1251711)CaDiCaL version: 2.1.3 % 115.47/16.65 % (1251711)Termination reason: Instruction limit % 115.47/16.65 % (1251711)Termination phase: Saturation % 115.47/16.65 % (1251711)Time elapsed: 4.065 s % 115.47/16.65 % (1251711)Peak memory usage: 87 MB % 115.47/16.65 % (1251711)Instructions burned: 17628 (million) % 115.47/16.65 % (1251880)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3193936912:i=206:fgj=on:rtra=on_2858 on theBenchmark for (2858ds/206Mi) % 115.47/16.65 % (1251880)Instruction limit reached! % 115.47/16.65 % (1251880)------------------------------ % 115.47/16.65 % (1251880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.47/16.65 % (1251880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.47/16.65 % (1251880)CaDiCaL version: 2.1.3 % 115.47/16.65 % (1251880)Termination reason: Instruction limit % 115.47/16.65 % (1251880)Termination phase: Saturation % 115.47/16.65 % (1251880)Time elapsed: 0.046 s % 115.47/16.65 % (1251880)Peak memory usage: 13 MB % 115.47/16.65 % (1251880)Instructions burned: 208 (million) % 115.47/16.65 % (1251900)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2912396645:i=232:rtra=on_2857 on theBenchmark for (2857ds/232Mi) % 115.47/16.65 % (1251900)Instruction limit reached! % 115.47/16.65 % (1251900)------------------------------ % 115.47/16.65 % (1251900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.47/16.65 % (1251900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.47/16.65 % (1251900)CaDiCaL version: 2.1.3 % 115.47/16.65 % (1251900)Termination reason: Instruction limit % 115.47/16.65 % (1251900)Termination phase: Saturation % 115.47/16.65 % (1251900)Time elapsed: 0.050 s % 115.47/16.65 % (1251900)Peak memory usage: 13 MB % 115.47/16.65 % (1251900)Instructions burned: 236 (million) % 115.47/16.65 % (1251930)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3343183370:i=262:rtra=on_2857 on theBenchmark for (2857ds/262Mi) % 115.47/16.65 % (1251930)Instruction limit reached! % 115.47/16.65 % (1251930)------------------------------ % 115.47/16.65 % (1251930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.47/16.65 % (1251930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.47/16.65 % (1251930)CaDiCaL version: 2.1.3 % 115.47/16.65 % (1251930)Termination reason: Instruction limit % 115.47/16.65 % (1251930)Termination phase: Saturation % 115.47/16.65 % (1251930)Time elapsed: 0.062 s % 115.47/16.65 % (1251930)Peak memory usage: 13 MB % 115.47/16.65 % (1251930)Instructions burned: 263 (million) % 115.47/16.65 % (1251948)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=469806119:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2856 on theBenchmark for (2856ds/318Mi) % 115.47/16.65 % (1251948)Instruction limit reached! % 115.47/16.65 % (1251948)------------------------------ % 115.47/16.65 % (1251948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.47/16.65 % (1251948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.47/16.65 % (1251948)CaDiCaL version: 2.1.3 % 115.47/16.65 % (1251948)Termination reason: Instruction limit % 115.47/16.65 % (1251948)Termination phase: Saturation % 115.47/16.65 % (1251948)Time elapsed: 0.075 s % 115.47/16.65 % (1251948)Peak memory usage: 15 MB % 115.47/16.65 % (1251948)Instructions burned: 323 (million) % 115.47/16.65 % (1251950)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2435556375:i=1428:nm=2:rtra=on_2855 on theBenchmark for (2855ds/1428Mi) % 135.69/19.49 % (1251950)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.69/19.49 % (1251950)Terminated due to inappropriate strategy. % 135.69/19.49 % (1251950)------------------------------ % 135.69/19.49 % (1251950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.69/19.49 % (1251950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.69/19.49 % (1251950)CaDiCaL version: 2.1.3 % 135.69/19.49 % (1251950)Termination reason: Inappropriate % 135.69/19.49 % (1251950)Time elapsed: 0.013 s % 135.69/19.49 % (1251950)Peak memory usage: 11 MB % 135.69/19.49 % (1251950)Instructions burned: 62 (million) % 135.69/19.49 % (1251950)------------------------------ % 135.69/19.49 % (1251950)------------------------------ % 135.69/19.49 % (1251952)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2951018777:i=262:bd=preordered:rtra=on:fsd=on_2855 on theBenchmark for (2855ds/262Mi) % 135.69/19.49 % (1251952)Instruction limit reached! % 135.69/19.49 % (1251952)------------------------------ % 135.69/19.49 % (1251952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.69/19.49 % (1251952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.69/19.49 % (1251952)CaDiCaL version: 2.1.3 % 135.69/19.49 % (1251952)Termination reason: Instruction limit % 135.69/19.49 % (1251952)Termination phase: Saturation % 135.69/19.49 % (1251952)Time elapsed: 0.056 s % 135.69/19.49 % (1251952)Peak memory usage: 15 MB % 135.69/19.49 % (1251952)Instructions burned: 264 (million) % 135.69/19.49 % (1251973)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=4147866262:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2854 on theBenchmark for (2854ds/1368Mi) % 135.69/19.49 % (1251973)Instruction limit reached! % 135.69/19.49 % (1251973)------------------------------ % 135.69/19.49 % (1251973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.69/19.49 % (1251973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.69/19.49 % (1251973)CaDiCaL version: 2.1.3 % 135.69/19.49 % (1251973)Termination reason: Instruction limit % 135.69/19.49 % (1251973)Termination phase: Saturation % 135.69/19.49 % (1251973)Time elapsed: 0.298 s % 135.69/19.49 % (1251973)Peak memory usage: 17 MB % 135.69/19.49 % (1251973)Instructions burned: 1369 (million) % 135.69/19.49 % (1252077)ott-21_1_sil=16000:si=on:fs=off:random_seed=1292550514:i=360:av=off:fsr=off:rtra=on_2851 on theBenchmark for (2851ds/360Mi) % 135.69/19.49 % (1252077)Instruction limit reached! % 135.69/19.49 % (1252077)------------------------------ % 135.69/19.49 % (1252077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.69/19.49 % (1252077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.69/19.49 % (1252077)CaDiCaL version: 2.1.3 % 135.69/19.49 % (1252077)Termination reason: Instruction limit % 135.69/19.49 % (1252077)Termination phase: Saturation % 135.69/19.49 % (1252077)Time elapsed: 0.075 s % 135.69/19.49 % (1252077)Peak memory usage: 13 MB % 135.69/19.49 % (1252077)Instructions burned: 365 (million) % 135.69/19.49 % (1252110)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=526442828:i=954:bd=all:rtra=on_2850 on theBenchmark for (2850ds/954Mi) % 135.69/19.49 % (1252110)Instruction limit reached! % 135.69/19.49 % (1252110)------------------------------ % 135.69/19.49 % (1252110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.69/19.49 % (1252110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.69/19.49 % (1252110)CaDiCaL version: 2.1.3 % 135.69/19.49 % (1252110)Termination reason: Instruction limit % 135.69/19.49 % (1252110)Termination phase: Saturation % 135.69/19.49 % (1252110)Time elapsed: 0.201 s % 135.69/19.49 % (1252110)Peak memory usage: 15 MB % 135.69/19.49 % (1252110)Instructions burned: 957 (million) % 135.69/19.49 % (1252112)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=557122553:fmbsr=1.3:i=1730:ins=25:rtra=on_2848 on theBenchmark for (2848ds/1730Mi) % 135.69/19.49 % (1252112)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.69/19.49 % (1252112)Terminated due to inappropriate strategy. % 135.69/19.49 % (1252112)------------------------------ % 135.69/19.49 % (1252112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.69/19.49 % (1252112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.69/19.49 % (1252112)CaDiCaL version: 2.1.3 % 135.69/19.49 % (1252112)Termination reason: Inappropriate % 164.78/23.51 % (1252112)Time elapsed: 0.010 s % 164.78/23.51 % (1252112)Peak memory usage: 11 MB % 164.78/23.51 % (1252112)Instructions burned: 46 (million) % 164.78/23.51 % (1252112)------------------------------ % 164.78/23.51 % (1252112)------------------------------ % 164.78/23.51 % (1252114)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1664728700:i=2358:rtra=on_2848 on theBenchmark for (2848ds/2358Mi) % 164.78/23.51 % (1252114)Instruction limit reached! % 164.78/23.51 % (1252114)------------------------------ % 164.78/23.51 % (1252114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.78/23.51 % (1252114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.78/23.51 % (1252114)CaDiCaL version: 2.1.3 % 164.78/23.51 % (1252114)Termination reason: Instruction limit % 164.78/23.51 % (1252114)Termination phase: Saturation % 164.78/23.51 % (1252114)Time elapsed: 0.493 s % 164.78/23.51 % (1252114)Peak memory usage: 14 MB % 164.78/23.51 % (1252114)Instructions burned: 2360 (million) % 164.78/23.51 % (1252116)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4078080861:i=1778:ins=1:rtra=on_2843 on theBenchmark for (2843ds/1778Mi) % 164.78/23.51 % (1252116)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.78/23.51 % (1252116)Terminated due to inappropriate strategy. % 164.78/23.51 % (1252116)------------------------------ % 164.78/23.51 % (1252116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.78/23.51 % (1252116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.78/23.51 % (1252116)CaDiCaL version: 2.1.3 % 164.78/23.51 % (1252116)Termination reason: Inappropriate % 164.78/23.51 % (1252116)Time elapsed: 0.010 s % 164.78/23.51 % (1252116)Peak memory usage: 11 MB % 164.78/23.51 % (1252116)Instructions burned: 47 (million) % 164.78/23.51 % (1252116)------------------------------ % 164.78/23.51 % (1252116)------------------------------ % 164.78/23.51 % (1252118)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=46083663:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2842 on theBenchmark for (2842ds/1384Mi) % 164.78/23.51 % (1252118)Instruction limit reached! % 164.78/23.51 % (1252118)------------------------------ % 164.78/23.51 % (1252118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.78/23.51 % (1252118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.78/23.51 % (1252118)CaDiCaL version: 2.1.3 % 164.78/23.51 % (1252118)Termination reason: Instruction limit % 164.78/23.51 % (1252118)Termination phase: Saturation % 164.78/23.51 % (1252118)Time elapsed: 0.287 s % 164.78/23.51 % (1252118)Peak memory usage: 15 MB % 164.78/23.51 % (1252118)Instructions burned: 1384 (million) % 164.78/23.51 % (1252120)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1673048035:i=1758:kws=inv_precedence:fsr=off:rtra=on_2840 on theBenchmark for (2840ds/1758Mi) % 164.78/23.51 % (1252120)Instruction limit reached! % 164.78/23.51 % (1252120)------------------------------ % 164.78/23.51 % (1252120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.78/23.51 % (1252120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.78/23.51 % (1252120)CaDiCaL version: 2.1.3 % 164.78/23.51 % (1252120)Termination reason: Instruction limit % 164.78/23.51 % (1252120)Termination phase: Saturation % 164.78/23.51 % (1252120)Time elapsed: 0.364 s % 164.78/23.51 % (1252120)Peak memory usage: 15 MB % 164.78/23.51 % (1252120)Instructions burned: 1759 (million) % 164.78/23.51 % (1252122)fmb+10_1_sil=64000:si=on:random_seed=2113859255:i=44122:nm=2:rtra=on:gsp=on_2836 on theBenchmark for (2836ds/44122Mi) % 164.78/23.51 % (1252122)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.78/23.51 % (1252122)Terminated due to inappropriate strategy. % 164.78/23.51 % (1252122)------------------------------ % 164.78/23.51 % (1252122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.78/23.51 % (1252122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.78/23.51 % (1252122)CaDiCaL version: 2.1.3 % 164.78/23.51 % (1252122)Termination reason: Inappropriate % 164.78/23.51 % (1252122)Time elapsed: 0.013 s % 164.78/23.51 % (1252122)Peak memory usage: 11 MB % 164.78/23.51 % (1252122)Instructions burned: 62 (million) % 164.78/23.51 % (1252122)------------------------------ % 164.78/23.51 % (1252122)------------------------------ % 164.78/23.51 % (1252124)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3813179931:i=19030:nm=5:rtra=on_2835 on theBenchmark for (2835ds/19030Mi) % 200.99/28.61 % (1252124)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.99/28.61 % (1252124)Terminated due to inappropriate strategy. % 200.99/28.61 % (1252124)------------------------------ % 200.99/28.61 % (1252124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.99/28.61 % (1252124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.99/28.61 % (1252124)CaDiCaL version: 2.1.3 % 200.99/28.61 % (1252124)Termination reason: Inappropriate % 200.99/28.61 % (1252124)Time elapsed: 0.013 s % 200.99/28.61 % (1252124)Peak memory usage: 11 MB % 200.99/28.61 % (1252124)Instructions burned: 62 (million) % 200.99/28.61 % (1252124)------------------------------ % 200.99/28.61 % (1252124)------------------------------ % 200.99/28.61 % (1252126)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=866152846:fmbsr=1.7:i=1840:rtra=on_2835 on theBenchmark for (2835ds/1840Mi) % 200.99/28.61 % (1252126)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.99/28.61 % (1252126)Terminated due to inappropriate strategy. % 200.99/28.61 % (1252126)------------------------------ % 200.99/28.61 % (1252126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.99/28.61 % (1252126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.99/28.61 % (1252126)CaDiCaL version: 2.1.3 % 200.99/28.61 % (1252126)Termination reason: Inappropriate % 200.99/28.61 % (1252126)Time elapsed: 0.013 s % 200.99/28.61 % (1252126)Peak memory usage: 11 MB % 200.99/28.61 % (1252126)Instructions burned: 62 (million) % 200.99/28.61 % (1252126)------------------------------ % 200.99/28.61 % (1252126)------------------------------ % 200.99/28.61 % (1252128)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=877615208:i=10262:rtra=on_2835 on theBenchmark for (2835ds/10262Mi) % 200.99/28.61 % (1252128)Instruction limit reached! % 200.99/28.61 % (1252128)------------------------------ % 200.99/28.61 % (1252128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.99/28.61 % (1252128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.99/28.61 % (1252128)CaDiCaL version: 2.1.3 % 200.99/28.61 % (1252128)Termination reason: Instruction limit % 200.99/28.61 % (1252128)Termination phase: Saturation % 200.99/28.61 % (1252128)Time elapsed: 2.117 s % 200.99/28.61 % (1252128)Peak memory usage: 19 MB % 200.99/28.61 % (1252128)Instructions burned: 10263 (million) % 200.99/28.61 % (1252130)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=390274951:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2814 on theBenchmark for (2814ds/2944Mi) % 200.99/28.61 % (1252130)Instruction limit reached! % 200.99/28.61 % (1252130)------------------------------ % 200.99/28.61 % (1252130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.99/28.61 % (1252130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.99/28.61 % (1252130)CaDiCaL version: 2.1.3 % 200.99/28.61 % (1252130)Termination reason: Instruction limit % 200.99/28.61 % (1252130)Termination phase: Saturation % 200.99/28.61 % (1252130)Time elapsed: 0.611 s % 200.99/28.61 % (1252130)Peak memory usage: 17 MB % 200.99/28.61 % (1252130)Instructions burned: 2945 (million) % 200.99/28.61 % (1252132)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=957039986:i=12648:rtra=on_2807 on theBenchmark for (2807ds/12648Mi) % 200.99/28.61 % (1252132)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.99/28.61 % (1252132)Terminated due to inappropriate strategy. % 200.99/28.61 % (1252132)------------------------------ % 200.99/28.61 % (1252132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.99/28.61 % (1252132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.99/28.61 % (1252132)CaDiCaL version: 2.1.3 % 200.99/28.61 % (1252132)Termination reason: Inappropriate % 200.99/28.61 % (1252132)Time elapsed: 0.013 s % 200.99/28.61 % (1252132)Peak memory usage: 11 MB % 200.99/28.61 % (1252132)Instructions burned: 62 (million) % 200.99/28.61 % (1252132)------------------------------ % 200.99/28.61 % (1252132)------------------------------ % 200.99/28.61 % (1252134)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2730406001:fmbsr=2.30978:i=4348:rtra=on_2807 on theBenchmark for (2807ds/4348Mi) % 200.99/28.61 % (1252134)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.99/28.61 % (1252134)Terminated due to inappropriate strategy. % 200.99/28.61 % (1252134)------------------------------ % 200.99/28.61 % (1252134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.96/39.36 % (1252134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.96/39.36 % (1252134)CaDiCaL version: 2.1.3 % 276.96/39.36 % (1252134)Termination reason: Inappropriate % 276.96/39.36 % (1252134)Time elapsed: 0.013 s % 276.96/39.36 % (1252134)Peak memory usage: 11 MB % 276.96/39.36 % (1252134)Instructions burned: 61 (million) % 276.96/39.36 % (1252134)------------------------------ % 276.96/39.36 % (1252134)------------------------------ % 276.96/39.36 % (1252136)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2012813814:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2807 on theBenchmark for (2807ds/1738Mi) % 276.96/39.36 % (1252136)Instruction limit reached! % 276.96/39.36 % (1252136)------------------------------ % 276.96/39.36 % (1252136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.96/39.36 % (1252136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.96/39.36 % (1252136)CaDiCaL version: 2.1.3 % 276.96/39.36 % (1252136)Termination reason: Instruction limit % 276.96/39.36 % (1252136)Termination phase: Saturation % 276.96/39.36 % (1252136)Time elapsed: 0.363 s % 276.96/39.36 % (1252136)Peak memory usage: 16 MB % 276.96/39.36 % (1252136)Instructions burned: 1744 (million) % 276.96/39.36 % (1252138)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=200173210:i=10228:av=off:rtra=on_2803 on theBenchmark for (2803ds/10228Mi) % 276.96/39.36 % (1252138)Instruction limit reached! % 276.96/39.36 % (1252138)------------------------------ % 276.96/39.36 % (1252138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.96/39.36 % (1252138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.96/39.36 % (1252138)CaDiCaL version: 2.1.3 % 276.96/39.36 % (1252138)Termination reason: Instruction limit % 276.96/39.36 % (1252138)Termination phase: Saturation % 276.96/39.36 % (1252138)Time elapsed: 2.108 s % 276.96/39.36 % (1252138)Peak memory usage: 19 MB % 276.96/39.36 % (1252138)Instructions burned: 10233 (million) % 276.96/39.36 % (1252140)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3294085265:i=108564:rtra=on_2782 on theBenchmark for (2782ds/108564Mi) % 276.96/39.36 % (1252140)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 276.96/39.36 % (1252140)Terminated due to inappropriate strategy. % 276.96/39.36 % (1252140)------------------------------ % 276.96/39.36 % (1252140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.96/39.36 % (1252140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.96/39.36 % (1252140)CaDiCaL version: 2.1.3 % 276.96/39.36 % (1252140)Termination reason: Inappropriate % 276.96/39.36 % (1252140)Time elapsed: 0.013 s % 276.96/39.36 % (1252140)Peak memory usage: 11 MB % 276.96/39.36 % (1252140)Instructions burned: 62 (million) % 276.96/39.36 % (1252140)------------------------------ % 276.96/39.36 % (1252140)------------------------------ % 276.96/39.36 % (1252142)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1281012723:i=7024:aac=none:rtra=on_2782 on theBenchmark for (2782ds/7024Mi) % 276.96/39.36 % (1251717)Instruction limit reached! % 276.96/39.36 % (1251717)------------------------------ % 276.96/39.36 % (1251717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.96/39.36 % (1251717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.96/39.36 % (1251717)CaDiCaL version: 2.1.3 % 276.96/39.36 % (1251717)Termination reason: Instruction limit % 276.96/39.36 % (1251717)Termination phase: Saturation % 276.96/39.36 % (1251717)Time elapsed: 10.889 s % 276.96/39.36 % (1251717)Peak memory usage: 19 MB % 276.96/39.36 % (1251717)Instructions burned: 28121 (million) % 276.96/39.36 % (1252144)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3653379096:i=7546:rtra=on:amm=off_2772 on theBenchmark for (2772ds/7546Mi) % 276.96/39.36 % (1252142)Instruction limit reached! % 276.96/39.36 % (1252142)------------------------------ % 276.96/39.36 % (1252142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.96/39.36 % (1252142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.96/39.36 % (1252142)CaDiCaL version: 2.1.3 % 276.96/39.36 % (1252142)Termination reason: Instruction limit % 276.96/39.36 % (1252142)Termination phase: Saturation % 276.96/39.36 % (1252142)Time elapsed: 1.480 s % 276.96/39.36 % (1252142)Peak memory usage: 21 MB % 276.96/39.36 % (1252142)Instructions burned: 7027 (million) % 276.96/39.36 % (1252146)ott+11_1_sil=16000:si=on:gs=on:random_seed=985026664:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2767 on theBenchmark for (2767ds/4502Mi) % 300.37/42.63 % (1252146)Instruction limit reached! % 300.37/42.63 % (1252146)------------------------------ % 300.37/42.63 % (1252146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.37/42.63 % (1252146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.37/42.63 % (1252146)CaDiCaL version: 2.1.3 % 300.37/42.63 % (1252146)Termination reason: Instruction limit % 300.37/42.63 % (1252146)Termination phase: Saturation % 300.37/42.63 % (1252146)Time elapsed: 0.943 s % 300.37/42.63 % (1252146)Peak memory usage: 17 MB % 300.37/42.63 % (1252146)Instructions burned: 4505 (million) % 300.37/42.63 % (1252148)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=3604093427:fmbsr=1.6:i=135068:rtra=on_2757 on theBenchmark for (2757ds/135068Mi) % 300.37/42.63 % (1252148)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.37/42.63 % (1252148)Terminated due to inappropriate strategy. % 300.37/42.63 % (1252148)------------------------------ % 300.37/42.63 % (1252148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.37/42.63 % (1252148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.37/42.63 % (1252148)CaDiCaL version: 2.1.3 % 300.37/42.63 % (1252148)Termination reason: Inappropriate % 300.37/42.63 % (1252148)Time elapsed: 0.013 s % 300.37/42.63 % (1252148)Peak memory usage: 11 MB % 300.37/42.63 % (1252148)Instructions burned: 62 (million) % 300.37/42.63 % (1252148)------------------------------ % 300.37/42.63 % (1252148)------------------------------ % 300.37/42.63 % (1252150)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3123430608:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2757 on theBenchmark for (2757ds/9182Mi) % 300.37/42.63 % (1252144)Instruction limit reached! % 300.37/42.63 % (1252144)------------------------------ % 300.37/42.63 % (1252144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.37/42.63 % (1252144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.37/42.63 % (1252144)CaDiCaL version: 2.1.3 % 300.37/42.63 % (1252144)Termination reason: Instruction limit % 300.37/42.63 % (1252144)Termination phase: Saturation % 300.37/42.63 % (1252144)Time elapsed: 2.885 s % 300.37/42.63 % (1252144)Peak memory usage: 19 MB % 300.37/42.63 % (1252144)Instructions burned: 7549 (million) % 300.37/42.63 % (1252152)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=192361379:i=58680:rtra=on_2743 on theBenchmark for (2743ds/58680Mi) % 300.37/42.63 % (1252150)Instruction limit reached! % 300.37/42.63 % (1252150)------------------------------ % 300.37/42.63 % (1252150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.37/42.63 % (1252150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.37/42.63 % (1252150)CaDiCaL version: 2.1.3 % 300.37/42.63 % (1252150)Termination reason: Instruction limit % 300.37/42.63 % (1252150)Termination phase: Saturation % 300.37/42.63 % (1252150)Time elapsed: 1.890 s % 300.37/42.63 % (1252150)Peak memory usage: 19 MB % 300.37/42.63 % (1252150)Instructions burned: 9183 (million) % 300.37/42.63 % (1252154)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=3133148328:i=10422:rtra=on_2738 on theBenchmark for (2738ds/10422Mi) % 300.37/42.63 % (1252154)Instruction limit reached! % 300.37/42.63 % (1252154)------------------------------ % 300.37/42.63 % (1252154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.37/42.63 % (1252154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.37/42.63 % (1252154)CaDiCaL version: 2.1.3 % 300.37/42.63 % (1252154)Termination reason: Instruction limit % 300.37/42.63 % (1252154)Termination phase: Saturation % 300.37/42.63 % (1252154)Time elapsed: 2.185 s % 300.37/42.63 % (1252154)Peak memory usage: 22 MB % 300.37/42.63 % (1252154)Instructions burned: 10424 (million) % 300.37/42.63 % (1252156)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=2415744904:i=10994:nm=2:rtra=on_2716 on theBenchmark for (2716ds/10994Mi) % 300.37/42.63 % (1252156)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.37/42.63 % (1252156)Terminated due to inappropriate strategy. % 300.37/42.63 % (1252156)------------------------------ % 300.37/42.63 % (1252156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.37/42.63 % (1252156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.37/42.63 % (1252156)CaDiCaL version: 2.1.3 % 300.37/42.63 % (1252156)Termination reason: Inappropriate % 300.37/42.63 % (1252156)Tim % 300.37/42.63 Terminated % 300.37/42.64 % Vampire exiting %------------------------------------------------------------------------------