%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX146_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 : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:46:33 PM UTC 2026 % Result : Timeout 289.71s 41.17s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWX146_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.26 % Computer : n020.cluster.edu % 0.09/0.26 % Model : x86_64 x86_64 % 0.09/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.26 % Memory : 8046.5625MB % 0.09/0.26 % OS : Linux 6.8.0-71-generic % 0.09/0.26 % CPULimit : 300 % 0.09/0.26 % WCLimit : 300 % 0.09/0.26 % DateTime : Mon Sep 28 15:05:23 UTC 2026 % 0.09/0.26 % CPUTime : % 0.09/0.27 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.26/0.30 Running first-order model finding % 0.26/0.30 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 5.82/1.22 % (228626)Will run a generic schedule for satisfiability detection. % 5.82/1.22 % (228636)dis+10_1_sil=32000:sp=arity:random_seed=2590462190:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 5.82/1.22 % (228633)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3820587319_2999 on theBenchmark for (2999ds/0Mi) % 5.82/1.22 % (228634)% WARNING: option uhcvi not known. % 5.82/1.22 % (228635)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=478451782:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 5.82/1.22 % (228634)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1439427919:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 5.82/1.22 % (228638)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2184532476:i=131_2999 on theBenchmark for (2999ds/131Mi) % 5.82/1.22 % (228639)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2922947060:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 5.82/1.22 % (228637)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4052241375:i=116_2999 on theBenchmark for (2999ds/116Mi) % 5.82/1.22 % (228633)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.82/1.22 % (228633)Terminated due to inappropriate strategy. % 5.82/1.22 % (228633)------------------------------ % 5.82/1.22 % (228633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.82/1.22 % (228633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.82/1.22 % (228633)CaDiCaL version: 2.1.3 % 5.82/1.22 % (228633)Termination reason: Inappropriate % 5.82/1.22 % (228633)Time elapsed: 0.042 s % 5.82/1.22 % (228633)Peak memory usage: 11 MB % 5.82/1.22 % (228633)Instructions burned: 60 (million) % 5.82/1.22 % (228636)Instruction limit reached! % 5.82/1.22 % (228636)------------------------------ % 5.82/1.22 % (228636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.82/1.22 % (228636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.82/1.22 % (228636)CaDiCaL version: 2.1.3 % 5.82/1.22 % (228636)Termination reason: Instruction limit % 5.82/1.22 % (228636)Termination phase: Saturation % 5.82/1.23 % (228636)Time elapsed: 0.044 s % 5.82/1.23 % (228636)Peak memory usage: 12 MB % 5.82/1.23 % (228636)Instructions burned: 104 (million) % 5.82/1.23 % (228633)------------------------------ % 5.82/1.23 % (228633)------------------------------ % 5.82/1.23 % (228648)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2255217159:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 5.82/1.23 % (228647)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3903372070:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 5.82/1.23 % (228637)Instruction limit reached! % 5.82/1.23 % (228637)------------------------------ % 5.82/1.23 % (228637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.82/1.23 % (228637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.82/1.23 % (228637)CaDiCaL version: 2.1.3 % 5.82/1.23 % (228637)Termination reason: Instruction limit % 5.82/1.23 % (228637)Termination phase: Saturation % 5.82/1.23 % (228637)Time elapsed: 0.095 s % 5.82/1.23 % (228637)Peak memory usage: 13 MB % 5.82/1.23 % (228637)Instructions burned: 116 (million) % 5.82/1.23 % (228638)Instruction limit reached! % 5.82/1.23 % (228638)------------------------------ % 5.82/1.23 % (228638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.82/1.23 % (228638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.82/1.23 % (228638)CaDiCaL version: 2.1.3 % 5.82/1.23 % (228638)Termination reason: Instruction limit % 5.82/1.23 % (228638)Termination phase: Saturation % 5.82/1.23 % (228638)Time elapsed: 0.107 s % 5.82/1.23 % (228638)Peak memory usage: 14 MB % 5.82/1.23 % (228638)Instructions burned: 131 (million) % 5.82/1.23 % (228648)Instruction limit reached! % 5.82/1.23 % (228648)------------------------------ % 5.82/1.23 % (228648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.82/1.23 % (228648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.82/1.23 % (228648)CaDiCaL version: 2.1.3 % 5.82/1.23 % (228648)Termination reason: Instruction limit % 5.82/1.23 % (228648)Termination phase: Saturation % 5.82/1.23 % (228648)Time elapsed: 0.057 s % 5.82/1.23 % (228648)Peak memory usage: 14 MB % 5.82/1.23 % (228648)Instructions burned: 136 (million) % 5.82/1.23 % (228647)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.87/2.13 % (228647)Terminated due to inappropriate strategy. % 11.87/2.13 % (228647)------------------------------ % 11.87/2.13 % (228647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.87/2.13 % (228647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.87/2.13 % (228647)CaDiCaL version: 2.1.3 % 11.87/2.13 % (228647)Termination reason: Inappropriate % 11.87/2.13 % (228647)Time elapsed: 0.050 s % 11.87/2.13 % (228647)Peak memory usage: 11 MB % 11.87/2.13 % (228647)Instructions burned: 60 (million) % 11.87/2.13 % (228647)------------------------------ % 11.87/2.13 % (228647)------------------------------ % 11.87/2.13 % (228651)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=1241839420:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 11.87/2.13 % (228653)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=907430635:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 11.87/2.13 % (228639)Instruction limit reached! % 11.87/2.13 % (228639)------------------------------ % 11.87/2.13 % (228639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.87/2.13 % (228639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.87/2.13 % (228639)CaDiCaL version: 2.1.3 % 11.87/2.13 % (228639)Termination reason: Instruction limit % 11.87/2.13 % (228639)Termination phase: Saturation % 11.87/2.13 % (228639)Time elapsed: 0.141 s % 11.87/2.13 % (228639)Peak memory usage: 14 MB % 11.87/2.13 % (228639)Instructions burned: 160 (million) % 11.87/2.13 % (228652)ott-21_1_sil=16000:fs=off:random_seed=2753600099:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 11.87/2.13 % (228654)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=829258506:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 11.87/2.13 % (228657)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1705390993:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 11.87/2.13 % (228654)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.87/2.13 % (228654)Terminated due to inappropriate strategy. % 11.87/2.13 % (228654)------------------------------ % 11.87/2.13 % (228654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.87/2.13 % (228654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.87/2.13 % (228654)CaDiCaL version: 2.1.3 % 11.87/2.13 % (228654)Termination reason: Inappropriate % 11.87/2.13 % (228654)Time elapsed: 0.038 s % 11.87/2.13 % (228654)Peak memory usage: 11 MB % 11.87/2.13 % (228654)Instructions burned: 45 (million) % 11.87/2.13 % (228654)------------------------------ % 11.87/2.13 % (228654)------------------------------ % 11.87/2.13 % (228664)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=647936081:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi) % 11.87/2.13 % (228664)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 11.87/2.13 % (228664)Terminated due to inappropriate strategy. % 11.87/2.13 % (228664)------------------------------ % 11.87/2.13 % (228664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.87/2.13 % (228664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.87/2.13 % (228664)CaDiCaL version: 2.1.3 % 11.87/2.13 % (228664)Termination reason: Inappropriate % 11.87/2.13 % (228664)Time elapsed: 0.025 s % 11.87/2.13 % (228664)Peak memory usage: 11 MB % 11.87/2.13 % (228664)Instructions burned: 45 (million) % 11.87/2.13 % (228664)------------------------------ % 11.87/2.13 % (228664)------------------------------ % 11.87/2.13 % (228667)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=401702968:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 11.87/2.13 % (228652)Instruction limit reached! % 11.87/2.13 % (228652)------------------------------ % 11.87/2.13 % (228652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.87/2.13 % (228652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.87/2.13 % (228652)CaDiCaL version: 2.1.3 % 11.87/2.13 % (228652)Termination reason: Instruction limit % 11.87/2.13 % (228652)Termination phase: Saturation % 11.87/2.13 % (228652)Time elapsed: 0.136 s % 11.87/2.13 % (228652)Peak memory usage: 13 MB % 11.87/2.13 % (228652)Instructions burned: 181 (million) % 30.71/4.85 % (228669)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=655804077:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi) % 30.71/4.85 % (228653)Instruction limit reached! % 30.71/4.85 % (228653)------------------------------ % 30.71/4.85 % (228653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.71/4.85 % (228653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.71/4.85 % (228653)CaDiCaL version: 2.1.3 % 30.71/4.85 % (228653)Termination reason: Instruction limit % 30.71/4.85 % (228653)Termination phase: Saturation % 30.71/4.85 % (228653)Time elapsed: 0.190 s % 30.71/4.85 % (228653)Peak memory usage: 14 MB % 30.71/4.85 % (228653)Instructions burned: 478 (million) % 30.71/4.85 % (228671)fmb+10_1_sil=64000:random_seed=2809802898:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 30.71/4.85 % (228671)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.71/4.85 % (228671)Terminated due to inappropriate strategy. % 30.71/4.85 % (228671)------------------------------ % 30.71/4.85 % (228671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.71/4.85 % (228671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.71/4.85 % (228671)CaDiCaL version: 2.1.3 % 30.71/4.85 % (228671)Termination reason: Inappropriate % 30.71/4.85 % (228671)Time elapsed: 0.026 s % 30.71/4.85 % (228671)Peak memory usage: 11 MB % 30.71/4.85 % (228671)Instructions burned: 60 (million) % 30.71/4.85 % (228671)------------------------------ % 30.71/4.85 % (228671)------------------------------ % 30.71/4.85 % (228675)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=829991494:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 30.71/4.85 % (228675)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.71/4.85 % (228675)Terminated due to inappropriate strategy. % 30.71/4.85 % (228675)------------------------------ % 30.71/4.85 % (228675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.71/4.85 % (228675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.71/4.85 % (228675)CaDiCaL version: 2.1.3 % 30.71/4.85 % (228675)Termination reason: Inappropriate % 30.71/4.85 % (228675)Time elapsed: 0.026 s % 30.71/4.85 % (228675)Peak memory usage: 11 MB % 30.71/4.85 % (228675)Instructions burned: 60 (million) % 30.71/4.85 % (228675)------------------------------ % 30.71/4.85 % (228675)------------------------------ % 30.71/4.85 % (228677)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3886729091:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 30.71/4.85 % (228677)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 30.71/4.85 % (228677)Terminated due to inappropriate strategy. % 30.71/4.85 % (228677)------------------------------ % 30.71/4.85 % (228677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.71/4.85 % (228677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.71/4.85 % (228677)CaDiCaL version: 2.1.3 % 30.71/4.85 % (228677)Termination reason: Inappropriate % 30.71/4.85 % (228677)Time elapsed: 0.026 s % 30.71/4.85 % (228677)Peak memory usage: 11 MB % 30.71/4.85 % (228677)Instructions burned: 60 (million) % 30.71/4.85 % (228677)------------------------------ % 30.71/4.85 % (228677)------------------------------ % 30.71/4.85 % (228679)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2892519461:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 30.71/4.85 % (228651)Instruction limit reached! % 30.71/4.85 % (228651)------------------------------ % 30.71/4.85 % (228651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.71/4.85 % (228651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.71/4.85 % (228651)CaDiCaL version: 2.1.3 % 30.71/4.85 % (228651)Termination reason: Instruction limit % 30.71/4.85 % (228651)Termination phase: Saturation % 30.71/4.85 % (228651)Time elapsed: 0.524 s % 30.71/4.85 % (228651)Peak memory usage: 16 MB % 30.71/4.85 % (228651)Instructions burned: 685 (million) % 30.71/4.85 % (228687)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=892474333:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 30.71/4.85 % (228667)Instruction limit reached! % 30.71/4.85 % (228667)------------------------------ % 30.71/4.85 % (228667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.71/4.85 % (228667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.29/5.02 % (228667)CaDiCaL version: 2.1.3 % 31.29/5.02 % (228667)Termination reason: Instruction limit % 31.29/5.02 % (228667)Termination phase: Saturation % 31.29/5.02 % (228667)Time elapsed: 0.513 s % 31.29/5.02 % (228667)Peak memory usage: 19 MB % 31.29/5.02 % (228667)Instructions burned: 693 (million) % 31.29/5.02 % (228689)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1680758213:i=6324_2990 on theBenchmark for (2990ds/6324Mi) % 31.29/5.02 % (228689)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.29/5.02 % (228689)Terminated due to inappropriate strategy. % 31.29/5.02 % (228689)------------------------------ % 31.29/5.02 % (228689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.29/5.02 % (228689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.29/5.02 % (228689)CaDiCaL version: 2.1.3 % 31.29/5.02 % (228689)Termination reason: Inappropriate % 31.29/5.02 % (228689)Time elapsed: 0.031 s % 31.29/5.02 % (228689)Peak memory usage: 11 MB % 31.29/5.02 % (228689)Instructions burned: 60 (million) % 31.29/5.02 % (228689)------------------------------ % 31.29/5.02 % (228689)------------------------------ % 31.29/5.02 % (228691)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1879694064:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 31.29/5.02 % (228669)Instruction limit reached! % 31.29/5.02 % (228669)------------------------------ % 31.29/5.02 % (228669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.29/5.02 % (228669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.29/5.02 % (228669)CaDiCaL version: 2.1.3 % 31.29/5.02 % (228669)Termination reason: Instruction limit % 31.29/5.02 % (228669)Termination phase: Saturation % 31.29/5.02 % (228669)Time elapsed: 0.596 s % 31.29/5.02 % (228669)Peak memory usage: 15 MB % 31.29/5.02 % (228669)Instructions burned: 880 (million) % 31.29/5.02 % (228691)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.29/5.02 % (228691)Terminated due to inappropriate strategy. % 31.29/5.02 % (228691)------------------------------ % 31.29/5.02 % (228691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.29/5.02 % (228691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.29/5.02 % (228691)CaDiCaL version: 2.1.3 % 31.29/5.02 % (228691)Termination reason: Inappropriate % 31.29/5.02 % (228691)Time elapsed: 0.033 s % 31.29/5.02 % (228691)Peak memory usage: 11 MB % 31.29/5.02 % (228691)Instructions burned: 60 (million) % 31.29/5.02 % (228691)------------------------------ % 31.29/5.02 % (228691)------------------------------ % 31.29/5.02 % (228694)ott+10_1_sil=32000:tgt=ground:random_seed=2958284520:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 31.29/5.02 % (228693)ott-2_1_sil=16000:newcnf=on:random_seed=789206191:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 31.29/5.02 % (228657)Instruction limit reached! % 31.29/5.02 % (228657)------------------------------ % 31.29/5.02 % (228657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.29/5.02 % (228657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.29/5.02 % (228657)CaDiCaL version: 2.1.3 % 31.29/5.02 % (228657)Termination reason: Instruction limit % 31.29/5.02 % (228657)Termination phase: Saturation % 31.29/5.02 % (228657)Time elapsed: 0.819 s % 31.29/5.02 % (228657)Peak memory usage: 17 MB % 31.29/5.02 % (228657)Instructions burned: 1179 (million) % 31.29/5.02 % (228697)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3013608908:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 31.29/5.02 % (228697)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.29/5.02 % (228697)Terminated due to inappropriate strategy. % 31.29/5.02 % (228697)------------------------------ % 31.29/5.02 % (228697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.29/5.02 % (228697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.29/5.02 % (228697)CaDiCaL version: 2.1.3 % 31.29/5.02 % (228697)Termination reason: Inappropriate % 31.29/5.02 % (228697)Time elapsed: 0.050 s % 31.29/5.02 % (228697)Peak memory usage: 11 MB % 31.29/5.02 % (228697)Instructions burned: 60 (million) % 31.29/5.02 % (228697)------------------------------ % 31.29/5.02 % (228697)------------------------------ % 31.29/5.02 % (228699)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2780787695:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 31.29/5.02 % (228693)Instruction limit reached! % 128.88/18.51 % (228693)------------------------------ % 128.88/18.51 % (228693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.88/18.51 % (228693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.88/18.51 % (228693)CaDiCaL version: 2.1.3 % 128.88/18.51 % (228693)Termination reason: Instruction limit % 128.88/18.51 % (228693)Termination phase: Saturation % 128.88/18.51 % (228693)Time elapsed: 0.760 s % 128.88/18.51 % (228693)Peak memory usage: 20 MB % 128.88/18.51 % (228693)Instructions burned: 869 (million) % 128.88/18.51 % (228701)dis+21_1_sil=32000:sas=cadical:random_seed=1727618744:i=3773:amm=off_2981 on theBenchmark for (2981ds/3773Mi) % 128.88/18.51 % (228687)Instruction limit reached! % 128.88/18.51 % (228687)------------------------------ % 128.88/18.51 % (228687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.88/18.51 % (228687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.88/18.51 % (228687)CaDiCaL version: 2.1.3 % 128.88/18.51 % (228687)Termination reason: Instruction limit % 128.88/18.51 % (228687)Termination phase: Saturation % 128.88/18.51 % (228687)Time elapsed: 1.140 s % 128.88/18.51 % (228687)Peak memory usage: 17 MB % 128.88/18.51 % (228687)Instructions burned: 1472 (million) % 128.88/18.51 % (228703)ott+11_1_sil=16000:gs=on:random_seed=2026032556:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2980 on theBenchmark for (2980ds/2251Mi) % 128.88/18.51 % (228679)Instruction limit reached! % 128.88/18.51 % (228679)------------------------------ % 128.88/18.51 % (228679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.88/18.51 % (228679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.88/18.51 % (228679)CaDiCaL version: 2.1.3 % 128.88/18.51 % (228679)Termination reason: Instruction limit % 128.88/18.51 % (228679)Termination phase: Saturation % 128.88/18.51 % (228679)Time elapsed: 1.948 s % 128.88/18.51 % (228679)Peak memory usage: 17 MB % 128.88/18.51 % (228679)Instructions burned: 5131 (million) % 128.88/18.51 % (228705)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1530643277:fmbsr=1.6:i=67534_2974 on theBenchmark for (2974ds/67534Mi) % 128.88/18.51 % (228705)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.88/18.51 % (228705)Terminated due to inappropriate strategy. % 128.88/18.51 % (228705)------------------------------ % 128.88/18.51 % (228705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.88/18.51 % (228705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.88/18.51 % (228705)CaDiCaL version: 2.1.3 % 128.88/18.51 % (228705)Termination reason: Inappropriate % 128.88/18.51 % (228705)Time elapsed: 0.028 s % 128.88/18.51 % (228705)Peak memory usage: 11 MB % 128.88/18.51 % (228705)Instructions burned: 60 (million) % 128.88/18.51 % (228705)------------------------------ % 128.88/18.51 % (228705)------------------------------ % 128.88/18.51 % (228707)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=556817464:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2973 on theBenchmark for (2973ds/4591Mi) % 128.88/18.51 % (228703)Instruction limit reached! % 128.88/18.51 % (228703)------------------------------ % 128.88/18.51 % (228703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.88/18.51 % (228703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.88/18.51 % (228703)CaDiCaL version: 2.1.3 % 128.88/18.51 % (228703)Termination reason: Instruction limit % 128.88/18.51 % (228703)Termination phase: Saturation % 128.88/18.51 % (228703)Time elapsed: 1.582 s % 128.88/18.51 % (228703)Peak memory usage: 17 MB % 128.88/18.51 % (228703)Instructions burned: 2252 (million) % 128.88/18.51 % (228709)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1728180001:i=29340_2964 on theBenchmark for (2964ds/29340Mi) % 128.88/18.51 % (228699)Instruction limit reached! % 128.88/18.51 % (228699)------------------------------ % 128.88/18.51 % (228699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.88/18.51 % (228699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.88/18.51 % (228699)CaDiCaL version: 2.1.3 % 128.88/18.51 % (228699)Termination reason: Instruction limit % 128.88/18.51 % (228699)Termination phase: Saturation % 128.88/18.51 % (228699)Time elapsed: 2.489 s % 128.88/18.51 % (228699)Peak memory usage: 18 MB % 128.88/18.51 % (228699)Instructions burned: 3512 (million) % 128.88/18.51 % (228711)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1955479160:i=5211_2962 on theBenchmark for (2962ds/5211Mi) % 128.88/18.51 % (228701)Instruction limit reached! % 152.74/21.92 % (228701)------------------------------ % 152.74/21.92 % (228701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.74/21.92 % (228701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.74/21.92 % (228701)CaDiCaL version: 2.1.3 % 152.74/21.92 % (228701)Termination reason: Instruction limit % 152.74/21.92 % (228701)Termination phase: Saturation % 152.74/21.92 % (228701)Time elapsed: 2.683 s % 152.74/21.92 % (228701)Peak memory usage: 17 MB % 152.74/21.92 % (228701)Instructions burned: 3773 (million) % 152.74/21.92 % (228715)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3363803994:i=5497:nm=2_2954 on theBenchmark for (2954ds/5497Mi) % 152.74/21.92 % (228715)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 152.74/21.92 % (228715)Terminated due to inappropriate strategy. % 152.74/21.92 % (228715)------------------------------ % 152.74/21.92 % (228715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.74/21.92 % (228715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.74/21.92 % (228715)CaDiCaL version: 2.1.3 % 152.74/21.92 % (228715)Termination reason: Inappropriate % 152.74/21.92 % (228715)Time elapsed: 0.034 s % 152.74/21.92 % (228715)Peak memory usage: 11 MB % 152.74/21.92 % (228715)Instructions burned: 60 (million) % 152.74/21.92 % (228715)------------------------------ % 152.74/21.92 % (228715)------------------------------ % 152.74/21.92 % (228717)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=915591592:fmbsr=2:i=46332_2954 on theBenchmark for (2954ds/46332Mi) % 152.74/21.92 % (228707)Instruction limit reached! % 152.74/21.92 % (228707)------------------------------ % 152.74/21.92 % (228707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.74/21.92 % (228707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.74/21.92 % (228707)CaDiCaL version: 2.1.3 % 152.74/21.92 % (228707)Termination reason: Instruction limit % 152.74/21.92 % (228707)Termination phase: Saturation % 152.74/21.92 % (228707)Time elapsed: 2.017 s % 152.74/21.92 % (228707)Peak memory usage: 32 MB % 152.74/21.92 % (228707)Instructions burned: 4592 (million) % 152.74/21.92 % (228694)Instruction limit reached! % 152.74/21.92 % (228694)------------------------------ % 152.74/21.92 % (228694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.74/21.92 % (228694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.74/21.92 % (228694)CaDiCaL version: 2.1.3 % 152.74/21.92 % (228694)Termination reason: Instruction limit % 152.74/21.92 % (228694)Termination phase: Saturation % 152.74/21.92 % (228694)Time elapsed: 3.606 s % 152.74/21.92 % (228694)Peak memory usage: 17 MB % 152.74/21.92 % (228694)Instructions burned: 5115 (million) % 152.74/21.92 % (228719)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3920451580:i=14071_2953 on theBenchmark for (2953ds/14071Mi) % 152.74/21.92 % (228717)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 152.74/21.92 % (228717)Terminated due to inappropriate strategy. % 152.74/21.92 % (228717)------------------------------ % 152.74/21.92 % (228717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.74/21.92 % (228717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.74/21.92 % (228717)CaDiCaL version: 2.1.3 % 152.74/21.92 % (228717)Termination reason: Inappropriate % 152.74/21.92 % (228717)Time elapsed: 0.049 s % 152.74/21.92 % (228717)Peak memory usage: 11 MB % 152.74/21.92 % (228717)Instructions burned: 60 (million) % 152.74/21.92 % (228717)------------------------------ % 152.74/21.92 % (228717)------------------------------ % 152.74/21.92 % (228720)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3484764487:i=22565:add=on:rawr=on_2953 on theBenchmark for (2953ds/22565Mi) % 152.74/21.92 % (228719)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 152.74/21.92 % (228719)Terminated due to inappropriate strategy. % 152.74/21.92 % (228719)------------------------------ % 152.74/21.92 % (228719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.74/21.92 % (228719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.74/21.92 % (228719)CaDiCaL version: 2.1.3 % 152.74/21.92 % (228719)Termination reason: Inappropriate % 152.74/21.92 % (228719)Time elapsed: 0.033 s % 152.74/21.92 % (228719)Peak memory usage: 11 MB % 152.74/21.92 % (228719)Instructions burned: 60 (million) % 152.74/21.92 % (228722)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1598319727:i=8173:av=off_2953 on theBenchmark for (2953ds/8173Mi) % 174.33/24.90 % (228719)------------------------------ % 174.33/24.90 % (228719)------------------------------ % 174.33/24.90 % (228725)dis+10_16:1_sil=16000:random_seed=1527532251:i=9155:fsr=off_2952 on theBenchmark for (2952ds/9155Mi) % 174.33/24.90 % (228711)Instruction limit reached! % 174.33/24.90 % (228711)------------------------------ % 174.33/24.90 % (228711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.33/24.90 % (228711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.33/24.90 % (228711)CaDiCaL version: 2.1.3 % 174.33/24.90 % (228711)Termination reason: Instruction limit % 174.33/24.90 % (228711)Termination phase: Saturation % 174.33/24.90 % (228711)Time elapsed: 3.764 s % 174.33/24.90 % (228711)Peak memory usage: 17 MB % 174.33/24.90 % (228711)Instructions burned: 5211 (million) % 174.33/24.90 % (228734)ott-3_8_sil=64000:random_seed=1891535268:i=20139:bs=on_2924 on theBenchmark for (2924ds/20139Mi) % 174.33/24.90 % (228722)Instruction limit reached! % 174.33/24.90 % (228722)------------------------------ % 174.33/24.90 % (228722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.33/24.90 % (228722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.33/24.90 % (228722)CaDiCaL version: 2.1.3 % 174.33/24.90 % (228722)Termination reason: Instruction limit % 174.33/24.90 % (228722)Termination phase: Saturation % 174.33/24.90 % (228722)Time elapsed: 3.044 s % 174.33/24.90 % (228722)Peak memory usage: 18 MB % 174.33/24.90 % (228722)Instructions burned: 8176 (million) % 174.33/24.90 % (228736)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1545898630:fmbsr=2:i=32576_2922 on theBenchmark for (2922ds/32576Mi) % 174.33/24.90 % (228736)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 174.33/24.90 % (228736)Terminated due to inappropriate strategy. % 174.33/24.90 % (228736)------------------------------ % 174.33/24.90 % (228736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.33/24.90 % (228736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.33/24.90 % (228736)CaDiCaL version: 2.1.3 % 174.33/24.90 % (228736)Termination reason: Inappropriate % 174.33/24.90 % (228736)Time elapsed: 0.032 s % 174.33/24.90 % (228736)Peak memory usage: 11 MB % 174.33/24.90 % (228736)Instructions burned: 60 (million) % 174.33/24.90 % (228736)------------------------------ % 174.33/24.90 % (228736)------------------------------ % 174.33/24.90 % (228738)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1444834522:i=11404_2921 on theBenchmark for (2921ds/11404Mi) % 174.33/24.90 % (228725)Instruction limit reached! % 174.33/24.90 % (228725)------------------------------ % 174.33/24.90 % (228725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.33/24.90 % (228725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.33/24.90 % (228725)CaDiCaL version: 2.1.3 % 174.33/24.90 % (228725)Termination reason: Instruction limit % 174.33/24.90 % (228725)Termination phase: Saturation % 174.33/24.90 % (228725)Time elapsed: 6.666 s % 174.33/24.90 % (228725)Peak memory usage: 19 MB % 174.33/24.90 % (228725)Instructions burned: 9156 (million) % 174.33/24.90 % (228742)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=476677347:i=14134_2885 on theBenchmark for (2885ds/14134Mi) % 174.33/24.90 % (228738)Instruction limit reached! % 174.33/24.90 % (228738)------------------------------ % 174.33/24.90 % (228738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.33/24.90 % (228738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.33/24.90 % (228738)CaDiCaL version: 2.1.3 % 174.33/24.90 % (228738)Termination reason: Instruction limit % 174.33/24.90 % (228738)Termination phase: Saturation % 174.33/24.90 % (228738)Time elapsed: 4.297 s % 174.33/24.90 % (228738)Peak memory usage: 17 MB % 174.33/24.90 % (228738)Instructions burned: 11407 (million) % 174.33/24.90 % (228744)dis+33_16_sil=32000:sac=on:random_seed=2360324438:i=15851:nm=0_2878 on theBenchmark for (2878ds/15851Mi) % 174.33/24.90 % (228744)Instruction limit reached! % 174.33/24.90 % (228744)------------------------------ % 174.33/24.90 % (228744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.33/24.90 % (228744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.33/24.90 % (228744)CaDiCaL version: 2.1.3 % 174.33/24.90 % (228744)Termination reason: Instruction limit % 174.33/24.90 % (228744)Termination phase: Saturation % 174.33/24.90 % (228744)Time elapsed: 6.004 s % 174.33/24.90 % (228744)Peak memory usage: 23 MB % 174.33/24.90 % (228744)Instructions burned: 15852 (million) % 174.33/24.90 % (228758)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2835166130:avsq=on:i=17627:add=on:amm=off_2818 on theBenchmark for (2818ds/17627Mi) % 187.10/26.76 % (228720)Instruction limit reached! % 187.10/26.76 % (228720)------------------------------ % 187.10/26.76 % (228720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.10/26.76 % (228720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.10/26.76 % (228720)CaDiCaL version: 2.1.3 % 187.10/26.76 % (228720)Termination reason: Instruction limit % 187.10/26.76 % (228720)Termination phase: Saturation % 187.10/26.76 % (228720)Time elapsed: 15.287 s % 187.10/26.76 % (228720)Peak memory usage: 18 MB % 187.10/26.76 % (228720)Instructions burned: 22565 (million) % 187.10/26.76 % (228770)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4081051657:s2a=on:i=53295_2800 on theBenchmark for (2800ds/53295Mi) % 187.10/26.76 % (228742)Instruction limit reached! % 187.10/26.76 % (228742)------------------------------ % 187.10/26.76 % (228742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.10/26.76 % (228742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.10/26.76 % (228742)CaDiCaL version: 2.1.3 % 187.10/26.76 % (228742)Termination reason: Instruction limit % 187.10/26.76 % (228742)Termination phase: Saturation % 187.10/26.76 % (228742)Time elapsed: 9.807 s % 187.10/26.76 % (228742)Peak memory usage: 18 MB % 187.10/26.76 % (228742)Instructions burned: 14134 (million) % 187.10/26.76 % (228774)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4225355608:i=26857:ins=20_2787 on theBenchmark for (2787ds/26857Mi) % 187.10/26.76 % (228774)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.10/26.76 % (228774)Terminated due to inappropriate strategy. % 187.10/26.76 % (228774)------------------------------ % 187.10/26.76 % (228774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.10/26.76 % (228774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.10/26.76 % (228774)CaDiCaL version: 2.1.3 % 187.10/26.76 % (228774)Termination reason: Inappropriate % 187.10/26.76 % (228774)Time elapsed: 0.040 s % 187.10/26.76 % (228774)Peak memory usage: 11 MB % 187.10/26.76 % (228774)Instructions burned: 60 (million) % 187.10/26.76 % (228774)------------------------------ % 187.10/26.76 % (228774)------------------------------ % 187.10/26.76 % (228776)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=548718954:i=28120:bs=on:fsr=off_2786 on theBenchmark for (2786ds/28120Mi) % 187.10/26.76 % (228734)Instruction limit reached! % 187.10/26.76 % (228734)------------------------------ % 187.10/26.76 % (228734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.10/26.76 % (228734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.10/26.76 % (228734)CaDiCaL version: 2.1.3 % 187.10/26.76 % (228734)Termination reason: Instruction limit % 187.10/26.76 % (228734)Termination phase: Saturation % 187.10/26.76 % (228734)Time elapsed: 13.947 s % 187.10/26.76 % (228734)Peak memory usage: 20 MB % 187.10/26.76 % (228734)Instructions burned: 20139 (million) % 187.10/26.76 % (228778)fmb+10_1_sil=256000:fmbss=7:random_seed=1072967569:fmbsr=1.6:i=182295_2785 on theBenchmark for (2785ds/182295Mi) % 187.10/26.76 % (228778)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.10/26.76 % (228778)Terminated due to inappropriate strategy. % 187.10/26.76 % (228778)------------------------------ % 187.10/26.76 % (228778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.10/26.76 % (228778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.10/26.76 % (228778)CaDiCaL version: 2.1.3 % 187.10/26.76 % (228778)Termination reason: Inappropriate % 187.10/26.76 % (228778)Time elapsed: 0.030 s % 187.10/26.76 % (228778)Peak memory usage: 11 MB % 187.10/26.76 % (228778)Instructions burned: 60 (million) % 187.10/26.76 % (228778)------------------------------ % 187.10/26.76 % (228778)------------------------------ % 187.10/26.76 % (228780)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=414489072:i=44625:gsp=on_2784 on theBenchmark for (2784ds/44625Mi) % 187.10/26.76 % (228780)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.10/26.76 % (228780)Terminated due to inappropriate strategy. % 187.10/26.76 % (228780)------------------------------ % 187.10/26.76 % (228780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.10/26.76 % (228780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.10/26.76 % (228780)CaDiCaL version: 2.1.3 % 187.10/26.76 % (228780)Termination reason: Inappropriate % 213.40/30.45 % (228780)Time elapsed: 0.030 s % 213.40/30.45 % (228780)Peak memory usage: 11 MB % 213.40/30.45 % (228780)Instructions burned: 60 (million) % 213.40/30.45 % (228780)------------------------------ % 213.40/30.45 % (228780)------------------------------ % 213.40/30.45 % (228782)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2389294498:i=160505_2783 on theBenchmark for (2783ds/160505Mi) % 213.40/30.45 % (228782)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.40/30.45 % (228782)Terminated due to inappropriate strategy. % 213.40/30.45 % (228782)------------------------------ % 213.40/30.45 % (228782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.40/30.45 % (228782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.40/30.45 % (228782)CaDiCaL version: 2.1.3 % 213.40/30.45 % (228782)Termination reason: Inappropriate % 213.40/30.45 % (228782)Time elapsed: 0.027 s % 213.40/30.45 % (228782)Peak memory usage: 11 MB % 213.40/30.45 % (228782)Instructions burned: 60 (million) % 213.40/30.45 % (228782)------------------------------ % 213.40/30.45 % (228782)------------------------------ % 213.40/30.45 % (228784)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3356090081:fmbsr=1.3:i=225729_2783 on theBenchmark for (2783ds/225729Mi) % 213.40/30.45 % (228784)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.40/30.45 % (228784)Terminated due to inappropriate strategy. % 213.40/30.45 % (228784)------------------------------ % 213.40/30.45 % (228784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.40/30.45 % (228784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.40/30.45 % (228784)CaDiCaL version: 2.1.3 % 213.40/30.45 % (228784)Termination reason: Inappropriate % 213.40/30.45 % (228784)Time elapsed: 0.053 s % 213.40/30.45 % (228784)Peak memory usage: 11 MB % 213.40/30.45 % (228784)Instructions burned: 60 (million) % 213.40/30.45 % (228784)------------------------------ % 213.40/30.45 % (228784)------------------------------ % 213.40/30.45 % (228786)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1815604875:fmbsr=2:i=185024:ins=7_2782 on theBenchmark for (2782ds/185024Mi) % 213.40/30.45 % (228786)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.40/30.45 % (228786)Terminated due to inappropriate strategy. % 213.40/30.45 % (228786)------------------------------ % 213.40/30.45 % (228786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.40/30.45 % (228786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.40/30.45 % (228786)CaDiCaL version: 2.1.3 % 213.40/30.45 % (228786)Termination reason: Inappropriate % 213.40/30.45 % (228786)Time elapsed: 0.028 s % 213.40/30.45 % (228786)Peak memory usage: 11 MB % 213.40/30.45 % (228786)Instructions burned: 60 (million) % 213.40/30.45 % (228786)------------------------------ % 213.40/30.45 % (228786)------------------------------ % 213.40/30.45 % (228788)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1595061802:rtra=on_2782 on theBenchmark for (2782ds/0Mi) % 213.40/30.45 % (228788)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.40/30.45 % (228788)Terminated due to inappropriate strategy. % 213.40/30.45 % (228788)------------------------------ % 213.40/30.45 % (228788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.40/30.45 % (228788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.40/30.45 % (228788)CaDiCaL version: 2.1.3 % 213.40/30.45 % (228788)Termination reason: Inappropriate % 213.40/30.45 % (228788)Time elapsed: 0.047 s % 213.40/30.45 % (228788)Peak memory usage: 11 MB % 213.40/30.45 % (228788)Instructions burned: 62 (million) % 213.40/30.45 % (228788)------------------------------ % 213.40/30.45 % (228788)------------------------------ % 213.40/30.45 % (228790)% WARNING: option uhcvi not known. % 213.40/30.45 % (228790)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1343048366:i=271062:add=off:rtra=on:rawr=on_2781 on theBenchmark for (2781ds/271062Mi) % 213.40/30.45 % (228709)Instruction limit reached! % 213.40/30.45 % (228709)------------------------------ % 213.40/30.45 % (228709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.40/30.45 % (228709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.40/30.45 % (228709)CaDiCaL version: 2.1.3 % 213.40/30.45 % (228709)Termination reason: Instruction limit % 213.40/30.45 % (228709)Termination phase: Saturation % 213.40/30.45 % (228709)Time elapsed: 21.012 s % 213.40/30.45 % (228709)Peak memory usage: 26 MB % 213.40/30.45 % (228709)Instructions burned: 29341 (million) % 228.30/32.56 % (228792)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4281142024:i=176048:add=on:rtra=on:rawr=on_2754 on theBenchmark for (2754ds/176048Mi) % 228.30/32.56 % (228758)Instruction limit reached! % 228.30/32.56 % (228758)------------------------------ % 228.30/32.56 % (228758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.30/32.56 % (228758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.30/32.56 % (228758)CaDiCaL version: 2.1.3 % 228.30/32.56 % (228758)Termination reason: Instruction limit % 228.30/32.56 % (228758)Termination phase: Saturation % 228.30/32.56 % (228758)Time elapsed: 7.360 s % 228.30/32.56 % (228758)Peak memory usage: 87 MB % 228.30/32.56 % (228758)Instructions burned: 17628 (million) % 228.30/32.56 % (228794)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3180870593:i=206:fgj=on:rtra=on_2744 on theBenchmark for (2744ds/206Mi) % 228.30/32.56 % (228794)Instruction limit reached! % 228.30/32.56 % (228794)------------------------------ % 228.30/32.56 % (228794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.30/32.56 % (228794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.30/32.56 % (228794)CaDiCaL version: 2.1.3 % 228.30/32.56 % (228794)Termination reason: Instruction limit % 228.30/32.56 % (228794)Termination phase: Saturation % 228.30/32.56 % (228794)Time elapsed: 0.160 s % 228.30/32.56 % (228794)Peak memory usage: 13 MB % 228.30/32.56 % (228794)Instructions burned: 207 (million) % 228.30/32.56 % (228796)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1278900040:i=232:rtra=on_2742 on theBenchmark for (2742ds/232Mi) % 228.30/32.56 % (228796)Instruction limit reached! % 228.30/32.56 % (228796)------------------------------ % 228.30/32.56 % (228796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.30/32.56 % (228796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.30/32.56 % (228796)CaDiCaL version: 2.1.3 % 228.30/32.56 % (228796)Termination reason: Instruction limit % 228.30/32.56 % (228796)Termination phase: Saturation % 228.30/32.56 % (228796)Time elapsed: 0.146 s % 228.30/32.56 % (228796)Peak memory usage: 13 MB % 228.30/32.56 % (228796)Instructions burned: 232 (million) % 228.30/32.56 % (228798)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3210616422:i=262:rtra=on_2740 on theBenchmark for (2740ds/262Mi) % 228.30/32.56 % (228798)Instruction limit reached! % 228.30/32.56 % (228798)------------------------------ % 228.30/32.56 % (228798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.30/32.56 % (228798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.30/32.56 % (228798)CaDiCaL version: 2.1.3 % 228.30/32.56 % (228798)Termination reason: Instruction limit % 228.30/32.56 % (228798)Termination phase: Saturation % 228.30/32.56 % (228798)Time elapsed: 0.125 s % 228.30/32.56 % (228798)Peak memory usage: 13 MB % 228.30/32.56 % (228798)Instructions burned: 264 (million) % 228.30/32.56 % (228800)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2222175042:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2739 on theBenchmark for (2739ds/318Mi) % 228.30/32.56 % (228800)Instruction limit reached! % 228.30/32.56 % (228800)------------------------------ % 228.30/32.56 % (228800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.30/32.56 % (228800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.30/32.56 % (228800)CaDiCaL version: 2.1.3 % 228.30/32.56 % (228800)Termination reason: Instruction limit % 228.30/32.56 % (228800)Termination phase: Saturation % 228.30/32.56 % (228800)Time elapsed: 0.250 s % 228.30/32.56 % (228800)Peak memory usage: 15 MB % 228.30/32.56 % (228800)Instructions burned: 319 (million) % 228.30/32.56 % (228802)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3294198077:i=1428:nm=2:rtra=on_2736 on theBenchmark for (2736ds/1428Mi) % 228.30/32.56 % (228802)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 228.30/32.56 % (228802)Terminated due to inappropriate strategy. % 228.30/32.56 % (228802)------------------------------ % 228.30/32.56 % (228802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.30/32.56 % (228802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.30/32.56 % (228802)CaDiCaL version: 2.1.3 % 228.30/32.56 % (228802)Termination reason: Inappropriate % 228.30/32.56 % (228802)Time elapsed: 0.051 s % 228.30/32.56 % (228802)Peak memory usage: 11 MB % 228.30/32.56 % (228802)Instructions burned: 62 (million) % 228.30/32.56 % (228802)------------------------------ % 289.71/41.17 % (228802)------------------------------ % 289.71/41.17 % (228804)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1744078122:i=262:bd=preordered:rtra=on:fsd=on_2735 on theBenchmark for (2735ds/262Mi) % 289.71/41.17 % (228804)Instruction limit reached! % 289.71/41.17 % (228804)------------------------------ % 289.71/41.17 % (228804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.71/41.17 % (228804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.71/41.17 % (228804)CaDiCaL version: 2.1.3 % 289.71/41.17 % (228804)Termination reason: Instruction limit % 289.71/41.17 % (228804)Termination phase: Saturation % 289.71/41.17 % (228804)Time elapsed: 0.194 s % 289.71/41.17 % (228804)Peak memory usage: 13 MB % 289.71/41.17 % (228804)Instructions burned: 263 (million) % 289.71/41.17 % (228806)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=3695363172:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2733 on theBenchmark for (2733ds/1368Mi) % 289.71/41.17 % (228806)Instruction limit reached! % 289.71/41.17 % (228806)------------------------------ % 289.71/41.17 % (228806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.71/41.17 % (228806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.71/41.17 % (228806)CaDiCaL version: 2.1.3 % 289.71/41.17 % (228806)Termination reason: Instruction limit % 289.71/41.17 % (228806)Termination phase: Saturation % 289.71/41.17 % (228806)Time elapsed: 1.041 s % 289.71/41.17 % (228806)Peak memory usage: 17 MB % 289.71/41.17 % (228806)Instructions burned: 1368 (million) % 289.71/41.17 % (228808)ott-21_1_sil=16000:si=on:fs=off:random_seed=56180439:i=360:av=off:fsr=off:rtra=on_2722 on theBenchmark for (2722ds/360Mi) % 289.71/41.17 % (228808)Instruction limit reached! % 289.71/41.17 % (228808)------------------------------ % 289.71/41.17 % (228808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.71/41.17 % (228808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.71/41.17 % (228808)CaDiCaL version: 2.1.3 % 289.71/41.17 % (228808)Termination reason: Instruction limit % 289.71/41.17 % (228808)Termination phase: Saturation % 289.71/41.17 % (228808)Time elapsed: 0.223 s % 289.71/41.17 % (228808)Peak memory usage: 13 MB % 289.71/41.17 % (228808)Instructions burned: 361 (million) % 289.71/41.17 % (228810)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1857941894:i=954:bd=all:rtra=on_2720 on theBenchmark for (2720ds/954Mi) % 289.71/41.17 % (228810)Instruction limit reached! % 289.71/41.17 % (228810)------------------------------ % 289.71/41.17 % (228810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.71/41.17 % (228810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.71/41.17 % (228810)CaDiCaL version: 2.1.3 % 289.71/41.17 % (228810)Termination reason: Instruction limit % 289.71/41.17 % (228810)Termination phase: Saturation % 289.71/41.17 % (228810)Time elapsed: 0.683 s % 289.71/41.17 % (228810)Peak memory usage: 14 MB % 289.71/41.17 % (228810)Instructions burned: 954 (million) % 289.71/41.17 % (228818)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1166177845:fmbsr=1.3:i=1730:ins=25:rtra=on_2712 on theBenchmark for (2712ds/1730Mi) % 289.71/41.17 % (228818)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 289.71/41.17 % (228818)Terminated due to inappropriate strategy. % 289.71/41.17 % (228818)------------------------------ % 289.71/41.17 % (228818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.71/41.17 % (228818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.71/41.17 % (228818)CaDiCaL version: 2.1.3 % 289.71/41.17 % (228818)Termination reason: Inappropriate % 289.71/41.17 % (228818)Time elapsed: 0.039 s % 289.71/41.17 % (228818)Peak memory usage: 11 MB % 289.71/41.17 % (228818)Instructions burned: 47 (million) % 289.71/41.17 % (228818)------------------------------ % 289.71/41.17 % (228818)------------------------------ % 289.71/41.17 % (228822)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=754391633:i=2358:rtra=on_2712 on theBenchmark for (2712ds/2358Mi) % 289.71/41.17 % (228822)Instruction limit reached! % 289.71/41.17 % (228822)------------------------------ % 289.71/41.17 % (228822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.71/41.17 % (228822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.71/41.17 % (228822)CaDiCaL version: 2.1.3 % 289.71/41.17 % (228822)Termination reason: Instruction limit % 289.71/41.17 % (228822)Termination phase: Saturation % 300.13/42.64 % (228822)Time elapsed: 1.325 s % 300.13/42.64 % (228822)Peak memory usage: 14 MB % 300.13/42.64 % (228822)Instructions burned: 2359 (million) % 300.13/42.64 % (228830)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=107365223:i=1778:ins=1:rtra=on_2698 on theBenchmark for (2698ds/1778Mi) % 300.13/42.64 % (228830)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.13/42.64 % (228830)Terminated due to inappropriate strategy. % 300.13/42.64 % (228830)------------------------------ % 300.13/42.64 % (228830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.13/42.64 % (228830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/42.64 % (228830)CaDiCaL version: 2.1.3 % 300.13/42.64 % (228830)Termination reason: Inappropriate % 300.13/42.64 % (228830)Time elapsed: 0.025 s % 300.13/42.64 % (228830)Peak memory usage: 11 MB % 300.13/42.64 % (228830)Instructions burned: 46 (million) % 300.13/42.64 % (228830)------------------------------ % 300.13/42.64 % (228830)------------------------------ % 300.13/42.64 % (228832)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=1763735638:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2698 on theBenchmark for (2698ds/1384Mi) % 300.13/42.64 % (228832)Instruction limit reached! % 300.13/42.64 % (228832)------------------------------ % 300.13/42.64 % (228832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.13/42.64 % (228832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/42.64 % (228832)CaDiCaL version: 2.1.3 % 300.13/42.64 % (228832)Termination reason: Instruction limit % 300.13/42.64 % (228832)Termination phase: Saturation % 300.13/42.64 % (228832)Time elapsed: 0.713 s % 300.13/42.64 % (228832)Peak memory usage: 15 MB % 300.13/42.64 % (228832)Instructions burned: 1384 (million) % 300.13/42.64 % (228838)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2259947236:i=1758:kws=inv_precedence:fsr=off:rtra=on_2690 on theBenchmark for (2690ds/1758Mi) % 300.13/42.64 % (228838)Instruction limit reached! % 300.13/42.64 % (228838)------------------------------ % 300.13/42.64 % (228838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.13/42.64 % (228838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/42.64 % (228838)CaDiCaL version: 2.1.3 % 300.13/42.64 % (228838)Termination reason: Instruction limit % 300.13/42.64 % (228838)Termination phase: Saturation % 300.13/42.64 % (228838)Time elapsed: 1.135 s % 300.13/42.64 % (228838)Peak memory usage: 15 MB % 300.13/42.64 % (228838)Instructions burned: 1758 (million) % 300.13/42.64 % (228844)fmb+10_1_sil=64000:si=on:random_seed=4123825180:i=44122:nm=2:rtra=on:gsp=on_2679 on theBenchmark for (2679ds/44122Mi) % 300.13/42.64 % (228844)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.13/42.64 % (228844)Terminated due to inappropriate strategy. % 300.13/42.64 % (228844)------------------------------ % 300.13/42.64 % (228844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.13/42.64 % (228844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/42.64 % (228844)CaDiCaL version: 2.1.3 % 300.13/42.64 % (228844)Termination reason: Inappropriate % 300.13/42.64 % (228844)Time elapsed: 0.031 s % 300.13/42.64 % (228844)Peak memory usage: 11 MB % 300.13/42.64 % (228844)Instructions burned: 62 (million) % 300.13/42.64 % (228844)------------------------------ % 300.13/42.64 % (228844)------------------------------ % 300.13/42.64 % (228846)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3221483011:i=19030:nm=5:rtra=on_2678 on theBenchmark for (2678ds/19030Mi) % 300.13/42.64 % (228846)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.13/42.64 % (228846)Terminated due to inappropriate strategy. % 300.13/42.64 % (228846)------------------------------ % 300.13/42.64 % (228846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.13/42.64 % (228846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/42.64 % (228846)CaDiCaL version: 2.1.3 % 300.13/42.64 % (228846)Termination reason: Inappropriate % 300.13/42.64 % (228846)Time elapsed: 0.047 s % 300.13/42.64 % (228846)Peak memory usage: 11 MB % 300.13/42.64 % (228846)Instructions burned: 61 (million) % 300.13/42.64 % (228846)------------------------------ % 300.13/42.64 % (228846)------------------------------ % 300.13/42.64 % (228848)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=4135693074:fmbsr=1.7: % 300.13/42.64 Terminated % 300.13/42.64 % Vampire exiting %------------------------------------------------------------------------------