%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW027_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n009.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:38:26 PM UTC 2026 % Result : Timeout 300.05s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW027_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n009.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 13:09:15 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 Running first-order model finding % 0.09/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.03/0.76 % (3016478)Will run a generic schedule for satisfiability detection. % 3.03/0.76 % (3016487)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=410058999:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.03/0.76 % (3016484)% WARNING: option uhcvi not known. % 3.03/0.76 % (3016483)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1974084430_2999 on theBenchmark for (2999ds/0Mi) % 3.03/0.76 % (3016484)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2962895915:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.03/0.76 % (3016485)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1216037802:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.03/0.76 % (3016486)dis+10_1_sil=32000:sp=arity:random_seed=4136476773:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.03/0.76 % (3016488)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1883393824:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.03/0.76 % (3016489)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=19947425:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.03/0.76 % (3016487)Instruction limit reached! % 3.03/0.76 % (3016487)------------------------------ % 3.03/0.76 % (3016487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.03/0.76 % (3016487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.03/0.76 % (3016487)CaDiCaL version: 2.1.3 % 3.03/0.76 % (3016487)Termination reason: Instruction limit % 3.03/0.76 % (3016487)Termination phase: Saturation % 3.03/0.76 % (3016487)Time elapsed: 0.029 s % 3.03/0.76 % (3016487)Peak memory usage: 15 MB % 3.03/0.76 % (3016487)Instructions burned: 120 (million) % 3.03/0.76 % (3016483)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.03/0.76 % (3016483)Terminated due to inappropriate strategy. % 3.03/0.76 % (3016483)------------------------------ % 3.03/0.76 % (3016483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.03/0.76 % (3016483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.03/0.76 % (3016483)CaDiCaL version: 2.1.3 % 3.03/0.76 % (3016483)Termination reason: Inappropriate % 3.03/0.76 % (3016483)Time elapsed: 0.031 s % 3.03/0.76 % (3016483)Peak memory usage: 13 MB % 3.03/0.76 % (3016483)Instructions burned: 74 (million) % 3.03/0.76 % (3016483)------------------------------ % 3.03/0.76 % (3016483)------------------------------ % 3.03/0.76 % (3016497)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2044564406:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.03/0.76 % (3016486)Instruction limit reached! % 3.03/0.76 % (3016486)------------------------------ % 3.03/0.76 % (3016486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.03/0.76 % (3016486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.03/0.76 % (3016486)CaDiCaL version: 2.1.3 % 3.03/0.76 % (3016486)Termination reason: Instruction limit % 3.03/0.76 % (3016486)Termination phase: Saturation % 3.03/0.76 % (3016486)Time elapsed: 0.046 s % 3.03/0.76 % (3016486)Peak memory usage: 14 MB % 3.03/0.76 % (3016486)Instructions burned: 103 (million) % 3.03/0.76 % (3016497)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.03/0.76 % (3016497)Terminated due to inappropriate strategy. % 3.03/0.76 % (3016497)------------------------------ % 3.03/0.76 % (3016497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.03/0.76 % (3016497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.03/0.76 % (3016497)CaDiCaL version: 2.1.3 % 3.03/0.76 % (3016497)Termination reason: Inappropriate % 3.03/0.76 % (3016497)Time elapsed: 0.017 s % 3.03/0.76 % (3016497)Peak memory usage: 13 MB % 3.03/0.76 % (3016497)Instructions burned: 74 (million) % 3.03/0.76 % (3016498)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2517421804:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 3.03/0.76 % (3016497)------------------------------ % 3.03/0.76 % (3016497)------------------------------ % 3.03/0.76 % (3016488)Instruction limit reached! % 3.03/0.76 % (3016488)------------------------------ % 3.03/0.76 % (3016488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.03/0.76 % (3016488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.03/0.76 % (3016488)CaDiCaL version: 2.1.3 % 3.03/0.76 % (3016488)Termination reason: Instruction limit % 5.41/1.06 % (3016488)Termination phase: Saturation % 5.41/1.06 % (3016488)Time elapsed: 0.054 s % 5.41/1.06 % (3016488)Peak memory usage: 14 MB % 5.41/1.06 % (3016488)Instructions burned: 134 (million) % 5.41/1.06 % (3016502)ott-21_1_sil=16000:fs=off:random_seed=2328849297:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.41/1.06 % (3016489)Instruction limit reached! % 5.41/1.06 % (3016489)------------------------------ % 5.41/1.06 % (3016489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.41/1.06 % (3016489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.41/1.06 % (3016489)CaDiCaL version: 2.1.3 % 5.41/1.06 % (3016489)Termination reason: Instruction limit % 5.41/1.06 % (3016489)Termination phase: Saturation % 5.41/1.06 % (3016489)Time elapsed: 0.064 s % 5.41/1.06 % (3016489)Peak memory usage: 15 MB % 5.41/1.06 % (3016489)Instructions burned: 160 (million) % 5.41/1.06 % (3016500)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=2755604406:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.41/1.06 % (3016503)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=442594823:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.41/1.06 % (3016506)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2561928138:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.41/1.06 % (3016498)Instruction limit reached! % 5.41/1.06 % (3016498)------------------------------ % 5.41/1.06 % (3016498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.41/1.06 % (3016498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.41/1.06 % (3016498)CaDiCaL version: 2.1.3 % 5.41/1.06 % (3016498)Termination reason: Instruction limit % 5.41/1.06 % (3016498)Termination phase: Saturation % 5.41/1.06 % (3016498)Time elapsed: 0.055 s % 5.41/1.06 % (3016498)Peak memory usage: 15 MB % 5.41/1.06 % (3016498)Instructions burned: 133 (million) % 5.41/1.06 % (3016502)Instruction limit reached! % 5.41/1.06 % (3016502)------------------------------ % 5.41/1.06 % (3016502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.41/1.06 % (3016502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.41/1.06 % (3016502)CaDiCaL version: 2.1.3 % 5.41/1.06 % (3016502)Termination reason: Instruction limit % 5.41/1.06 % (3016502)Termination phase: Saturation % 5.41/1.06 % (3016502)Time elapsed: 0.046 s % 5.41/1.06 % (3016502)Peak memory usage: 15 MB % 5.41/1.06 % (3016502)Instructions burned: 182 (million) % 5.41/1.06 % (3016506)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.41/1.06 % (3016506)Terminated due to inappropriate strategy. % 5.41/1.06 % (3016506)------------------------------ % 5.41/1.06 % (3016506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.41/1.06 % (3016506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.41/1.06 % (3016506)CaDiCaL version: 2.1.3 % 5.41/1.06 % (3016506)Termination reason: Inappropriate % 5.41/1.06 % (3016506)Time elapsed: 0.031 s % 5.41/1.06 % (3016506)Peak memory usage: 13 MB % 5.41/1.06 % (3016506)Instructions burned: 73 (million) % 5.41/1.06 % (3016506)------------------------------ % 5.41/1.06 % (3016506)------------------------------ % 5.41/1.06 % (3016510)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3113964053:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.41/1.06 % (3016509)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4237632184:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.41/1.06 % (3016511)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=709864285:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 5.41/1.06 % (3016510)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.41/1.06 % (3016510)Terminated due to inappropriate strategy. % 5.41/1.06 % (3016510)------------------------------ % 5.41/1.06 % (3016510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.41/1.06 % (3016510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.41/1.06 % (3016510)CaDiCaL version: 2.1.3 % 5.41/1.06 % (3016510)Termination reason: Inappropriate % 5.41/1.06 % (3016510)Time elapsed: 0.024 s % 5.41/1.06 % (3016510)Peak memory usage: 15 MB % 16.85/2.84 % (3016510)Instructions burned: 103 (million) % 16.85/2.84 % (3016510)------------------------------ % 16.85/2.84 % (3016510)------------------------------ % 16.85/2.84 % (3016515)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3258730581:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 16.85/2.84 % (3016503)Instruction limit reached! % 16.85/2.84 % (3016503)------------------------------ % 16.85/2.84 % (3016503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.84 % (3016503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/2.84 % (3016503)CaDiCaL version: 2.1.3 % 16.85/2.84 % (3016503)Termination reason: Instruction limit % 16.85/2.84 % (3016503)Termination phase: Saturation % 16.85/2.84 % (3016503)Time elapsed: 0.253 s % 16.85/2.84 % (3016503)Peak memory usage: 16 MB % 16.85/2.84 % (3016503)Instructions burned: 478 (million) % 16.85/2.84 % (3016517)fmb+10_1_sil=64000:random_seed=969822977:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 16.85/2.84 % (3016517)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.85/2.84 % (3016517)Terminated due to inappropriate strategy. % 16.85/2.84 % (3016517)------------------------------ % 16.85/2.84 % (3016517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.84 % (3016517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/2.84 % (3016517)CaDiCaL version: 2.1.3 % 16.85/2.84 % (3016517)Termination reason: Inappropriate % 16.85/2.84 % (3016517)Time elapsed: 0.035 s % 16.85/2.84 % (3016517)Peak memory usage: 13 MB % 16.85/2.84 % (3016517)Instructions burned: 81 (million) % 16.85/2.84 % (3016517)------------------------------ % 16.85/2.84 % (3016517)------------------------------ % 16.85/2.84 % (3016500)Instruction limit reached! % 16.85/2.84 % (3016500)------------------------------ % 16.85/2.84 % (3016500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.84 % (3016500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/2.84 % (3016500)CaDiCaL version: 2.1.3 % 16.85/2.84 % (3016500)Termination reason: Instruction limit % 16.85/2.84 % (3016500)Termination phase: Saturation % 16.85/2.84 % (3016500)Time elapsed: 0.331 s % 16.85/2.84 % (3016500)Peak memory usage: 19 MB % 16.85/2.84 % (3016500)Instructions burned: 684 (million) % 16.85/2.84 % (3016519)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3241033383:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 16.85/2.84 % (3016520)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=583451716:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 16.85/2.84 % (3016515)Instruction limit reached! % 16.85/2.84 % (3016515)------------------------------ % 16.85/2.84 % (3016515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.84 % (3016515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/2.84 % (3016515)CaDiCaL version: 2.1.3 % 16.85/2.84 % (3016515)Termination reason: Instruction limit % 16.85/2.84 % (3016515)Termination phase: Saturation % 16.85/2.84 % (3016515)Time elapsed: 0.262 s % 16.85/2.84 % (3016515)Peak memory usage: 21 MB % 16.85/2.84 % (3016515)Instructions burned: 879 (million) % 16.85/2.84 % (3016523)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=124165792:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 16.85/2.84 % (3016519)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.85/2.84 % (3016519)Terminated due to inappropriate strategy. % 16.85/2.84 % (3016519)------------------------------ % 16.85/2.84 % (3016519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.84 % (3016519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.85/2.84 % (3016519)CaDiCaL version: 2.1.3 % 16.85/2.84 % (3016519)Termination reason: Inappropriate % 16.85/2.84 % (3016519)Time elapsed: 0.031 s % 16.85/2.84 % (3016519)Peak memory usage: 13 MB % 16.85/2.84 % (3016519)Instructions burned: 74 (million) % 16.85/2.84 % (3016519)------------------------------ % 16.85/2.84 % (3016519)------------------------------ % 16.85/2.84 % (3016520)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.85/2.84 % (3016520)Terminated due to inappropriate strategy. % 16.85/2.84 % (3016520)------------------------------ % 16.85/2.84 % (3016520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.85/2.84 % (3016520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.93/3.46 % (3016520)CaDiCaL version: 2.1.3 % 21.93/3.46 % (3016520)Termination reason: Inappropriate % 21.93/3.46 % (3016520)Time elapsed: 0.032 s % 21.93/3.46 % (3016520)Peak memory usage: 13 MB % 21.93/3.46 % (3016520)Instructions burned: 74 (million) % 21.93/3.46 % (3016520)------------------------------ % 21.93/3.46 % (3016520)------------------------------ % 21.93/3.46 % (3016525)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=797831302:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 21.93/3.46 % (3016526)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1143000844:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 21.93/3.46 % (3016511)Instruction limit reached! % 21.93/3.46 % (3016511)------------------------------ % 21.93/3.46 % (3016511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.93/3.46 % (3016511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.93/3.46 % (3016511)CaDiCaL version: 2.1.3 % 21.93/3.46 % (3016511)Termination reason: Instruction limit % 21.93/3.46 % (3016511)Termination phase: Saturation % 21.93/3.46 % (3016511)Time elapsed: 0.350 s % 21.93/3.46 % (3016511)Peak memory usage: 20 MB % 21.93/3.46 % (3016511)Instructions burned: 692 (million) % 21.93/3.46 % (3016526)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.93/3.46 % (3016526)Terminated due to inappropriate strategy. % 21.93/3.46 % (3016526)------------------------------ % 21.93/3.46 % (3016526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.93/3.46 % (3016526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.93/3.46 % (3016526)CaDiCaL version: 2.1.3 % 21.93/3.46 % (3016526)Termination reason: Inappropriate % 21.93/3.46 % (3016526)Time elapsed: 0.032 s % 21.93/3.46 % (3016526)Peak memory usage: 13 MB % 21.93/3.46 % (3016526)Instructions burned: 74 (million) % 21.93/3.46 % (3016526)------------------------------ % 21.93/3.46 % (3016526)------------------------------ % 21.93/3.46 % (3016529)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1159297411:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 21.93/3.46 % (3016530)ott-2_1_sil=16000:newcnf=on:random_seed=2514539885:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 21.93/3.46 % (3016529)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.93/3.46 % (3016529)Terminated due to inappropriate strategy. % 21.93/3.46 % (3016529)------------------------------ % 21.93/3.46 % (3016529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.93/3.46 % (3016529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.93/3.46 % (3016529)CaDiCaL version: 2.1.3 % 21.93/3.46 % (3016529)Termination reason: Inappropriate % 21.93/3.46 % (3016529)Time elapsed: 0.032 s % 21.93/3.46 % (3016529)Peak memory usage: 13 MB % 21.93/3.46 % (3016529)Instructions burned: 74 (million) % 21.93/3.46 % (3016529)------------------------------ % 21.93/3.46 % (3016529)------------------------------ % 21.93/3.46 % (3016533)ott+10_1_sil=32000:tgt=ground:random_seed=2039916791:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 21.93/3.46 % (3016509)Instruction limit reached! % 21.93/3.46 % (3016509)------------------------------ % 21.93/3.46 % (3016509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.93/3.46 % (3016509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.93/3.46 % (3016509)CaDiCaL version: 2.1.3 % 21.93/3.46 % (3016509)Termination reason: Instruction limit % 21.93/3.46 % (3016509)Termination phase: Saturation % 21.93/3.46 % (3016509)Time elapsed: 0.575 s % 21.93/3.46 % (3016509)Peak memory usage: 19 MB % 21.93/3.46 % (3016509)Instructions burned: 1179 (million) % 21.93/3.46 % (3016535)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1099037444:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 21.93/3.46 % (3016535)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.93/3.46 % (3016535)Terminated due to inappropriate strategy. % 21.93/3.46 % (3016535)------------------------------ % 21.93/3.46 % (3016535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.93/3.46 % (3016535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.93/3.46 % (3016535)CaDiCaL version: 2.1.3 % 21.93/3.46 % (3016535)Termination reason: Inappropriate % 21.93/3.46 % (3016535)Time elapsed: 0.031 s % 21.93/3.46 % (3016535)Peak memory usage: 13 MB % 21.93/3.46 % (3016535)Instructions burned: 74 (million) % 90.57/13.11 % (3016535)------------------------------ % 90.57/13.11 % (3016535)------------------------------ % 90.57/13.11 % (3016537)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3388952732:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 90.57/13.11 % (3016530)Instruction limit reached! % 90.57/13.11 % (3016530)------------------------------ % 90.57/13.11 % (3016530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.57/13.11 % (3016530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.57/13.11 % (3016530)CaDiCaL version: 2.1.3 % 90.57/13.11 % (3016530)Termination reason: Instruction limit % 90.57/13.11 % (3016530)Termination phase: Saturation % 90.57/13.11 % (3016530)Time elapsed: 0.485 s % 90.57/13.11 % (3016530)Peak memory usage: 19 MB % 90.57/13.11 % (3016530)Instructions burned: 870 (million) % 90.57/13.11 % (3016539)dis+21_1_sil=32000:sas=cadical:random_seed=1816020569:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 90.57/13.11 % (3016525)Instruction limit reached! % 90.57/13.11 % (3016525)------------------------------ % 90.57/13.11 % (3016525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.57/13.11 % (3016525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.57/13.11 % (3016525)CaDiCaL version: 2.1.3 % 90.57/13.11 % (3016525)Termination reason: Instruction limit % 90.57/13.11 % (3016525)Termination phase: Saturation % 90.57/13.11 % (3016525)Time elapsed: 0.596 s % 90.57/13.11 % (3016525)Peak memory usage: 18 MB % 90.57/13.11 % (3016525)Instructions burned: 1473 (million) % 90.57/13.11 % (3016541)ott+11_1_sil=16000:gs=on:random_seed=2540525020:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 90.57/13.11 % (3016523)Instruction limit reached! % 90.57/13.11 % (3016523)------------------------------ % 90.57/13.11 % (3016523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.57/13.11 % (3016523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.57/13.11 % (3016523)CaDiCaL version: 2.1.3 % 90.57/13.11 % (3016523)Termination reason: Instruction limit % 90.57/13.11 % (3016523)Termination phase: Saturation % 90.57/13.11 % (3016523)Time elapsed: 1.428 s % 90.57/13.11 % (3016523)Peak memory usage: 43 MB % 90.57/13.11 % (3016523)Instructions burned: 5133 (million) % 90.57/13.11 % (3016543)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1750319182:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 90.57/13.11 % (3016543)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 90.57/13.11 % (3016543)Terminated due to inappropriate strategy. % 90.57/13.11 % (3016543)------------------------------ % 90.57/13.11 % (3016543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.57/13.11 % (3016543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.57/13.11 % (3016543)CaDiCaL version: 2.1.3 % 90.57/13.11 % (3016543)Termination reason: Inappropriate % 90.57/13.11 % (3016543)Time elapsed: 0.022 s % 90.57/13.11 % (3016543)Peak memory usage: 13 MB % 90.57/13.11 % (3016543)Instructions burned: 100 (million) % 90.57/13.11 % (3016543)------------------------------ % 90.57/13.11 % (3016543)------------------------------ % 90.57/13.11 % (3016545)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2644570033:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 90.57/13.11 % (3016541)Instruction limit reached! % 90.57/13.11 % (3016541)------------------------------ % 90.57/13.11 % (3016541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.57/13.11 % (3016541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.57/13.11 % (3016541)CaDiCaL version: 2.1.3 % 90.57/13.11 % (3016541)Termination reason: Instruction limit % 90.57/13.11 % (3016541)Termination phase: Saturation % 90.57/13.11 % (3016541)Time elapsed: 0.923 s % 90.57/13.11 % (3016541)Peak memory usage: 19 MB % 90.57/13.11 % (3016541)Instructions burned: 2254 (million) % 90.57/13.11 % (3016547)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3122471019:i=29340_2979 on theBenchmark for (2979ds/29340Mi) % 90.57/13.11 % (3016537)Instruction limit reached! % 90.57/13.11 % (3016537)------------------------------ % 90.57/13.11 % (3016537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 90.57/13.11 % (3016537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.57/13.11 % (3016537)CaDiCaL version: 2.1.3 % 90.57/13.11 % (3016537)Termination reason: Instruction limit % 121.58/17.46 % (3016537)Termination phase: Saturation % 121.58/17.46 % (3016537)Time elapsed: 1.753 s % 121.58/17.46 % (3016537)Peak memory usage: 29 MB % 121.58/17.46 % (3016537)Instructions burned: 3513 (million) % 121.58/17.46 % (3016549)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1342902506:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 121.58/17.46 % (3016539)Instruction limit reached! % 121.58/17.46 % (3016539)------------------------------ % 121.58/17.46 % (3016539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.58/17.46 % (3016539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.58/17.46 % (3016539)CaDiCaL version: 2.1.3 % 121.58/17.46 % (3016539)Termination reason: Instruction limit % 121.58/17.46 % (3016539)Termination phase: Saturation % 121.58/17.46 % (3016539)Time elapsed: 1.627 s % 121.58/17.46 % (3016539)Peak memory usage: 23 MB % 121.58/17.46 % (3016539)Instructions burned: 3773 (million) % 121.58/17.46 % (3016551)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2190673354:i=5497:nm=2_2972 on theBenchmark for (2972ds/5497Mi) % 121.58/17.46 % (3016551)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.58/17.46 % (3016551)Terminated due to inappropriate strategy. % 121.58/17.46 % (3016551)------------------------------ % 121.58/17.46 % (3016551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.58/17.46 % (3016551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.58/17.46 % (3016551)CaDiCaL version: 2.1.3 % 121.58/17.46 % (3016551)Termination reason: Inappropriate % 121.58/17.46 % (3016551)Time elapsed: 0.031 s % 121.58/17.46 % (3016551)Peak memory usage: 13 MB % 121.58/17.46 % (3016551)Instructions burned: 74 (million) % 121.58/17.46 % (3016551)------------------------------ % 121.58/17.46 % (3016551)------------------------------ % 121.58/17.46 % (3016553)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4093811895:fmbsr=2:i=46332_2972 on theBenchmark for (2972ds/46332Mi) % 121.58/17.46 % (3016553)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.58/17.46 % (3016553)Terminated due to inappropriate strategy. % 121.58/17.46 % (3016553)------------------------------ % 121.58/17.46 % (3016553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.58/17.46 % (3016553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.58/17.46 % (3016553)CaDiCaL version: 2.1.3 % 121.58/17.46 % (3016553)Termination reason: Inappropriate % 121.58/17.46 % (3016553)Time elapsed: 0.043 s % 121.58/17.46 % (3016553)Peak memory usage: 13 MB % 121.58/17.46 % (3016553)Instructions burned: 103 (million) % 121.58/17.46 % (3016553)------------------------------ % 121.58/17.46 % (3016553)------------------------------ % 121.58/17.46 % (3016555)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1238203855:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 121.58/17.46 % (3016555)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.58/17.46 % (3016555)Terminated due to inappropriate strategy. % 121.58/17.46 % (3016555)------------------------------ % 121.58/17.46 % (3016555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.58/17.46 % (3016555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.58/17.46 % (3016555)CaDiCaL version: 2.1.3 % 121.58/17.46 % (3016555)Termination reason: Inappropriate % 121.58/17.46 % (3016555)Time elapsed: 0.044 s % 121.58/17.46 % (3016555)Peak memory usage: 13 MB % 121.58/17.46 % (3016555)Instructions burned: 103 (million) % 121.58/17.46 % (3016555)------------------------------ % 121.58/17.46 % (3016555)------------------------------ % 121.58/17.46 % (3016557)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1227658601:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 121.58/17.46 % (3016545)Instruction limit reached! % 121.58/17.46 % (3016545)------------------------------ % 121.58/17.46 % (3016545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.58/17.46 % (3016545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.58/17.46 % (3016545)CaDiCaL version: 2.1.3 % 121.58/17.46 % (3016545)Termination reason: Instruction limit % 121.58/17.46 % (3016545)Termination phase: Saturation % 121.58/17.46 % (3016545)Time elapsed: 1.229 s % 121.58/17.46 % (3016545)Peak memory usage: 39 MB % 121.58/17.46 % (3016545)Instructions burned: 4592 (million) % 121.58/17.46 % (3016559)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=956941164:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 122.96/17.62 % (3016533)Instruction limit reached! % 122.96/17.62 % (3016533)------------------------------ % 122.96/17.62 % (3016533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.96/17.62 % (3016533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.96/17.62 % (3016533)CaDiCaL version: 2.1.3 % 122.96/17.62 % (3016533)Termination reason: Instruction limit % 122.96/17.62 % (3016533)Termination phase: Saturation % 122.96/17.62 % (3016533)Time elapsed: 2.908 s % 122.96/17.62 % (3016533)Peak memory usage: 32 MB % 122.96/17.62 % (3016533)Instructions burned: 5114 (million) % 122.96/17.62 % (3016561)dis+10_16:1_sil=16000:random_seed=2568387282:i=9155:fsr=off_2964 on theBenchmark for (2964ds/9155Mi) % 122.96/17.62 % (3016559)Instruction limit reached! % 122.96/17.62 % (3016559)------------------------------ % 122.96/17.62 % (3016559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.96/17.62 % (3016559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.96/17.62 % (3016559)CaDiCaL version: 2.1.3 % 122.96/17.62 % (3016559)Termination reason: Instruction limit % 122.96/17.62 % (3016559)Termination phase: Saturation % 122.96/17.62 % (3016559)Time elapsed: 1.782 s % 122.96/17.62 % (3016559)Peak memory usage: 30 MB % 122.96/17.62 % (3016559)Instructions burned: 8176 (million) % 122.96/17.62 % (3016563)ott-3_8_sil=64000:random_seed=3919181604:i=20139:bs=on_2949 on theBenchmark for (2949ds/20139Mi) % 122.96/17.62 % (3016549)Instruction limit reached! % 122.96/17.62 % (3016549)------------------------------ % 122.96/17.62 % (3016549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.96/17.62 % (3016549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.96/17.62 % (3016549)CaDiCaL version: 2.1.3 % 122.96/17.62 % (3016549)Termination reason: Instruction limit % 122.96/17.62 % (3016549)Termination phase: Saturation % 122.96/17.62 % (3016549)Time elapsed: 2.763 s % 122.96/17.62 % (3016549)Peak memory usage: 47 MB % 122.96/17.62 % (3016549)Instructions burned: 5212 (million) % 122.96/17.62 % (3016565)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2094792765:fmbsr=2:i=32576_2946 on theBenchmark for (2946ds/32576Mi) % 122.96/17.62 % (3016565)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 122.96/17.62 % (3016565)Terminated due to inappropriate strategy. % 122.96/17.62 % (3016565)------------------------------ % 122.96/17.62 % (3016565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.96/17.62 % (3016565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.96/17.62 % (3016565)CaDiCaL version: 2.1.3 % 122.96/17.62 % (3016565)Termination reason: Inappropriate % 122.96/17.62 % (3016565)Time elapsed: 0.041 s % 122.96/17.62 % (3016565)Peak memory usage: 13 MB % 122.96/17.62 % (3016565)Instructions burned: 100 (million) % 122.96/17.62 % (3016565)------------------------------ % 122.96/17.62 % (3016565)------------------------------ % 122.96/17.62 % (3016567)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2719041007:i=11404_2945 on theBenchmark for (2945ds/11404Mi) % 122.96/17.62 % (3016561)Instruction limit reached! % 122.96/17.62 % (3016561)------------------------------ % 122.96/17.62 % (3016561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.96/17.62 % (3016561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.96/17.62 % (3016561)CaDiCaL version: 2.1.3 % 122.96/17.62 % (3016561)Termination reason: Instruction limit % 122.96/17.62 % (3016561)Termination phase: Saturation % 122.96/17.62 % (3016561)Time elapsed: 4.742 s % 122.96/17.62 % (3016561)Peak memory usage: 57 MB % 122.96/17.62 % (3016561)Instructions burned: 9156 (million) % 122.96/17.62 % (3016569)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=710039377:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 122.96/17.62 % (3016563)Instruction limit reached! % 122.96/17.62 % (3016563)------------------------------ % 122.96/17.62 % (3016563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.96/17.62 % (3016563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.96/17.62 % (3016563)CaDiCaL version: 2.1.3 % 122.96/17.62 % (3016563)Termination reason: Instruction limit % 122.96/17.62 % (3016563)Termination phase: Saturation % 122.96/17.62 % (3016563)Time elapsed: 6.524 s % 122.96/17.62 % (3016563)Peak memory usage: 67 MB % 122.96/17.62 % (3016563)Instructions burned: 20139 (million) % 122.96/17.62 % (3016571)dis+33_16_sil=32000:sac=on:random_seed=2540874626:i=15851:nm=0_2884 on theBenchmark for (2884ds/15851Mi) % 122.96/17.62 % (3016567)Instruction limit reached! % 122.96/17.62 % (3016567)------------------------------ % 122.96/17.62 % (3016567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.68/23.53 % (3016567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.68/23.53 % (3016567)CaDiCaL version: 2.1.3 % 164.68/23.53 % (3016567)Termination reason: Instruction limit % 164.68/23.53 % (3016567)Termination phase: Saturation % 164.68/23.53 % (3016567)Time elapsed: 7.400 s % 164.68/23.53 % (3016567)Peak memory usage: 47 MB % 164.68/23.53 % (3016567)Instructions burned: 11404 (million) % 164.68/23.53 % (3016573)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=230547815:avsq=on:i=17627:add=on:amm=off_2871 on theBenchmark for (2871ds/17627Mi) % 164.68/23.53 % (3016571)Instruction limit reached! % 164.68/23.53 % (3016571)------------------------------ % 164.68/23.53 % (3016571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.68/23.53 % (3016571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.68/23.53 % (3016571)CaDiCaL version: 2.1.3 % 164.68/23.53 % (3016571)Termination reason: Instruction limit % 164.68/23.53 % (3016571)Termination phase: Saturation % 164.68/23.53 % (3016571)Time elapsed: 3.619 s % 164.68/23.53 % (3016571)Peak memory usage: 31 MB % 164.68/23.53 % (3016571)Instructions burned: 15853 (million) % 164.68/23.53 % (3016575)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2147987632:s2a=on:i=53295_2848 on theBenchmark for (2848ds/53295Mi) % 164.68/23.53 % (3016547)Instruction limit reached! % 164.68/23.53 % (3016547)------------------------------ % 164.68/23.53 % (3016547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.68/23.53 % (3016547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.68/23.53 % (3016547)CaDiCaL version: 2.1.3 % 164.68/23.53 % (3016547)Termination reason: Instruction limit % 164.68/23.53 % (3016547)Termination phase: Saturation % 164.68/23.53 % (3016547)Time elapsed: 13.927 s % 164.68/23.53 % (3016547)Peak memory usage: 47 MB % 164.68/23.53 % (3016547)Instructions burned: 29340 (million) % 164.68/23.53 % (3016577)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1319271302:i=26857:ins=20_2839 on theBenchmark for (2839ds/26857Mi) % 164.68/23.53 % (3016577)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.68/23.53 % (3016577)Terminated due to inappropriate strategy. % 164.68/23.53 % (3016577)------------------------------ % 164.68/23.53 % (3016577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.68/23.53 % (3016577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.68/23.53 % (3016577)CaDiCaL version: 2.1.3 % 164.68/23.53 % (3016577)Termination reason: Inappropriate % 164.68/23.53 % (3016577)Time elapsed: 0.033 s % 164.68/23.53 % (3016577)Peak memory usage: 13 MB % 164.68/23.53 % (3016577)Instructions burned: 74 (million) % 164.68/23.53 % (3016577)------------------------------ % 164.68/23.53 % (3016577)------------------------------ % 164.68/23.53 % (3016579)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=718722999:i=28120:bs=on:fsr=off_2839 on theBenchmark for (2839ds/28120Mi) % 164.68/23.53 % (3016569)Instruction limit reached! % 164.68/23.53 % (3016569)------------------------------ % 164.68/23.53 % (3016569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.68/23.53 % (3016569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.68/23.53 % (3016569)CaDiCaL version: 2.1.3 % 164.68/23.53 % (3016569)Termination reason: Instruction limit % 164.68/23.53 % (3016569)Termination phase: Saturation % 164.68/23.53 % (3016569)Time elapsed: 8.829 s % 164.68/23.53 % (3016569)Peak memory usage: 51 MB % 164.68/23.53 % (3016569)Instructions burned: 14140 (million) % 164.68/23.53 % (3016557)Instruction limit reached! % 164.68/23.53 % (3016557)------------------------------ % 164.68/23.53 % (3016557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.68/23.53 % (3016557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.68/23.53 % (3016557)CaDiCaL version: 2.1.3 % 164.68/23.53 % (3016557)Termination reason: Instruction limit % 164.68/23.53 % (3016557)Termination phase: Saturation % 164.68/23.53 % (3016557)Time elapsed: 14.234 s % 164.68/23.53 % (3016557)Peak memory usage: 207 MB % 164.68/23.53 % (3016557)Instructions burned: 22566 (million) % 164.68/23.53 % (3016582)fmb+10_1_sil=256000:fmbss=7:random_seed=2033081091:fmbsr=1.6:i=182295_2828 on theBenchmark for (2828ds/182295Mi) % 164.68/23.53 % (3016584)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2325252333:i=44625:gsp=on_2828 on theBenchmark for (2828ds/44625Mi) % 164.68/23.53 % (3016582)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.93/25.30 % (3016582)Terminated due to inappropriate strategy. % 176.93/25.30 % (3016582)------------------------------ % 176.93/25.30 % (3016582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.93/25.30 % (3016582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.93/25.30 % (3016582)CaDiCaL version: 2.1.3 % 176.93/25.30 % (3016582)Termination reason: Inappropriate % 176.93/25.30 % (3016582)Time elapsed: 0.032 s % 176.93/25.30 % (3016582)Peak memory usage: 13 MB % 176.93/25.30 % (3016582)Instructions burned: 74 (million) % 176.93/25.30 % (3016582)------------------------------ % 176.93/25.30 % (3016582)------------------------------ % 176.93/25.30 % (3016586)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=379966745:i=160505_2827 on theBenchmark for (2827ds/160505Mi) % 176.93/25.30 % (3016584)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.93/25.30 % (3016584)Terminated due to inappropriate strategy. % 176.93/25.30 % (3016584)------------------------------ % 176.93/25.30 % (3016584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.93/25.30 % (3016584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.93/25.30 % (3016584)CaDiCaL version: 2.1.3 % 176.93/25.30 % (3016584)Termination reason: Inappropriate % 176.93/25.30 % (3016584)Time elapsed: 0.036 s % 176.93/25.30 % (3016584)Peak memory usage: 14 MB % 176.93/25.30 % (3016584)Instructions burned: 78 (million) % 176.93/25.30 % (3016584)------------------------------ % 176.93/25.30 % (3016584)------------------------------ % 176.93/25.30 % (3016588)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=766915742:fmbsr=1.3:i=225729_2827 on theBenchmark for (2827ds/225729Mi) % 176.93/25.30 % (3016586)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.93/25.30 % (3016586)Terminated due to inappropriate strategy. % 176.93/25.30 % (3016586)------------------------------ % 176.93/25.30 % (3016586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.93/25.30 % (3016586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.93/25.30 % (3016586)CaDiCaL version: 2.1.3 % 176.93/25.30 % (3016586)Termination reason: Inappropriate % 176.93/25.30 % (3016586)Time elapsed: 0.032 s % 176.93/25.30 % (3016586)Peak memory usage: 13 MB % 176.93/25.30 % (3016586)Instructions burned: 74 (million) % 176.93/25.30 % (3016586)------------------------------ % 176.93/25.30 % (3016586)------------------------------ % 176.93/25.30 % (3016590)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=412480682:fmbsr=2:i=185024:ins=7_2827 on theBenchmark for (2827ds/185024Mi) % 176.93/25.30 % (3016588)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.93/25.30 % (3016588)Terminated due to inappropriate strategy. % 176.93/25.30 % (3016588)------------------------------ % 176.93/25.30 % (3016588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.93/25.30 % (3016588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.93/25.30 % (3016588)CaDiCaL version: 2.1.3 % 176.93/25.30 % (3016588)Termination reason: Inappropriate % 176.93/25.30 % (3016588)Time elapsed: 0.043 s % 176.93/25.30 % (3016588)Peak memory usage: 13 MB % 176.93/25.30 % (3016588)Instructions burned: 103 (million) % 176.93/25.30 % (3016588)------------------------------ % 176.93/25.30 % (3016588)------------------------------ % 176.93/25.30 % (3016592)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2615876932:rtra=on_2826 on theBenchmark for (2826ds/0Mi) % 176.93/25.30 % (3016590)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 176.93/25.30 % (3016590)Terminated due to inappropriate strategy. % 176.93/25.30 % (3016590)------------------------------ % 176.93/25.30 % (3016590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.93/25.30 % (3016590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.93/25.30 % (3016590)CaDiCaL version: 2.1.3 % 176.93/25.30 % (3016590)Termination reason: Inappropriate % 176.93/25.30 % (3016590)Time elapsed: 0.043 s % 176.93/25.30 % (3016590)Peak memory usage: 13 MB % 176.93/25.30 % (3016590)Instructions burned: 104 (million) % 176.93/25.30 % (3016590)------------------------------ % 176.93/25.30 % (3016590)------------------------------ % 176.93/25.30 % (3016594)% WARNING: option uhcvi not known. % 176.93/25.30 % (3016594)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=53893195:i=271062:add=off:rtra=on:rawr=on_2826 on theBenchmark for (2826ds/271062Mi) % 176.93/25.30 % (3016592)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 194.67/27.77 % (3016592)Terminated due to inappropriate strategy. % 194.67/27.77 % (3016592)------------------------------ % 194.67/27.77 % (3016592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.67/27.77 % (3016592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.67/27.77 % (3016592)CaDiCaL version: 2.1.3 % 194.67/27.77 % (3016592)Termination reason: Inappropriate % 194.67/27.77 % (3016592)Time elapsed: 0.042 s % 194.67/27.77 % (3016592)Peak memory usage: 14 MB % 194.67/27.77 % (3016592)Instructions burned: 87 (million) % 194.67/27.77 % (3016592)------------------------------ % 194.67/27.77 % (3016592)------------------------------ % 194.67/27.77 % (3016596)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3410156390:i=176048:add=on:rtra=on:rawr=on_2826 on theBenchmark for (2826ds/176048Mi) % 194.67/27.77 % (3016573)Instruction limit reached! % 194.67/27.77 % (3016573)------------------------------ % 194.67/27.77 % (3016573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.67/27.77 % (3016573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.67/27.77 % (3016573)CaDiCaL version: 2.1.3 % 194.67/27.77 % (3016573)Termination reason: Instruction limit % 194.67/27.77 % (3016573)Termination phase: Saturation % 194.67/27.77 % (3016573)Time elapsed: 9.747 s % 194.67/27.77 % (3016573)Peak memory usage: 103 MB % 194.67/27.77 % (3016573)Instructions burned: 17627 (million) % 194.67/27.77 % (3016598)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1893644080:i=206:fgj=on:rtra=on_2773 on theBenchmark for (2773ds/206Mi) % 194.67/27.77 % (3016598)Instruction limit reached! % 194.67/27.77 % (3016598)------------------------------ % 194.67/27.77 % (3016598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.67/27.77 % (3016598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.67/27.77 % (3016598)CaDiCaL version: 2.1.3 % 194.67/27.77 % (3016598)Termination reason: Instruction limit % 194.67/27.77 % (3016598)Termination phase: Saturation % 194.67/27.77 % (3016598)Time elapsed: 0.106 s % 194.67/27.77 % (3016598)Peak memory usage: 17 MB % 194.67/27.77 % (3016598)Instructions burned: 208 (million) % 194.67/27.77 % (3016600)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=748307675:i=232:rtra=on_2772 on theBenchmark for (2772ds/232Mi) % 194.67/27.77 % (3016600)Instruction limit reached! % 194.67/27.77 % (3016600)------------------------------ % 194.67/27.77 % (3016600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.67/27.77 % (3016600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.67/27.77 % (3016600)CaDiCaL version: 2.1.3 % 194.67/27.77 % (3016600)Termination reason: Instruction limit % 194.67/27.77 % (3016600)Termination phase: Saturation % 194.67/27.77 % (3016600)Time elapsed: 0.113 s % 194.67/27.77 % (3016600)Peak memory usage: 16 MB % 194.67/27.77 % (3016600)Instructions burned: 234 (million) % 194.67/27.77 % (3016602)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1407576853:i=262:rtra=on_2770 on theBenchmark for (2770ds/262Mi) % 194.67/27.77 % (3016602)Instruction limit reached! % 194.67/27.77 % (3016602)------------------------------ % 194.67/27.77 % (3016602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.67/27.77 % (3016602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.67/27.77 % (3016602)CaDiCaL version: 2.1.3 % 194.67/27.77 % (3016602)Termination reason: Instruction limit % 194.67/27.77 % (3016602)Termination phase: Saturation % 194.67/27.77 % (3016602)Time elapsed: 0.128 s % 194.67/27.77 % (3016602)Peak memory usage: 18 MB % 194.67/27.77 % (3016602)Instructions burned: 263 (million) % 194.67/27.77 % (3016604)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=952129762:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2769 on theBenchmark for (2769ds/318Mi) % 194.67/27.77 % (3016604)Instruction limit reached! % 194.67/27.77 % (3016604)------------------------------ % 194.67/27.77 % (3016604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.67/27.77 % (3016604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.67/27.77 % (3016604)CaDiCaL version: 2.1.3 % 194.67/27.77 % (3016604)Termination reason: Instruction limit % 194.67/27.77 % (3016604)Termination phase: Saturation % 194.67/27.77 % (3016604)Time elapsed: 0.175 s % 194.67/27.77 % (3016604)Peak memory usage: 18 MB % 194.67/27.77 % (3016604)Instructions burned: 318 (million) % 194.67/27.77 % (3016606)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1177131740:i=1428:nm=2:rtra=on_2767 on theBenchmark for (2767ds/1428Mi) % 202.23/28.84 % (3016606)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.23/28.84 % (3016606)Terminated due to inappropriate strategy. % 202.23/28.84 % (3016606)------------------------------ % 202.23/28.84 % (3016606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.23/28.84 % (3016606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.23/28.84 % (3016606)CaDiCaL version: 2.1.3 % 202.23/28.84 % (3016606)Termination reason: Inappropriate % 202.23/28.84 % (3016606)Time elapsed: 0.042 s % 202.23/28.84 % (3016606)Peak memory usage: 14 MB % 202.23/28.84 % (3016606)Instructions burned: 87 (million) % 202.23/28.84 % (3016606)------------------------------ % 202.23/28.84 % (3016606)------------------------------ % 202.23/28.84 % (3016608)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2556552676:i=262:bd=preordered:rtra=on:fsd=on_2766 on theBenchmark for (2766ds/262Mi) % 202.23/28.84 % (3016608)Instruction limit reached! % 202.23/28.84 % (3016608)------------------------------ % 202.23/28.84 % (3016608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.23/28.84 % (3016608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.23/28.84 % (3016608)CaDiCaL version: 2.1.3 % 202.23/28.84 % (3016608)Termination reason: Instruction limit % 202.23/28.84 % (3016608)Termination phase: Saturation % 202.23/28.84 % (3016608)Time elapsed: 0.121 s % 202.23/28.84 % (3016608)Peak memory usage: 16 MB % 202.23/28.84 % (3016608)Instructions burned: 264 (million) % 202.23/28.84 % (3016610)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=3305899544:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2765 on theBenchmark for (2765ds/1368Mi) % 202.23/28.84 % (3016610)Instruction limit reached! % 202.23/28.84 % (3016610)------------------------------ % 202.23/28.84 % (3016610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.23/28.84 % (3016610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.23/28.84 % (3016610)CaDiCaL version: 2.1.3 % 202.23/28.84 % (3016610)Termination reason: Instruction limit % 202.23/28.84 % (3016610)Termination phase: Saturation % 202.23/28.84 % (3016610)Time elapsed: 0.724 s % 202.23/28.84 % (3016610)Peak memory usage: 22 MB % 202.23/28.84 % (3016610)Instructions burned: 1368 (million) % 202.23/28.84 % (3016612)ott-21_1_sil=16000:si=on:fs=off:random_seed=3085379828:i=360:av=off:fsr=off:rtra=on_2757 on theBenchmark for (2757ds/360Mi) % 202.23/28.84 % (3016612)Instruction limit reached! % 202.23/28.84 % (3016612)------------------------------ % 202.23/28.84 % (3016612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.23/28.84 % (3016612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.23/28.84 % (3016612)CaDiCaL version: 2.1.3 % 202.23/28.84 % (3016612)Termination reason: Instruction limit % 202.23/28.84 % (3016612)Termination phase: Saturation % 202.23/28.84 % (3016612)Time elapsed: 0.182 s % 202.23/28.84 % (3016612)Peak memory usage: 16 MB % 202.23/28.84 % (3016612)Instructions burned: 362 (million) % 202.23/28.84 % (3016614)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1358797686:i=954:bd=all:rtra=on_2755 on theBenchmark for (2755ds/954Mi) % 202.23/28.84 % (3016614)Instruction limit reached! % 202.23/28.84 % (3016614)------------------------------ % 202.23/28.84 % (3016614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.23/28.84 % (3016614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.23/28.84 % (3016614)CaDiCaL version: 2.1.3 % 202.23/28.84 % (3016614)Termination reason: Instruction limit % 202.23/28.84 % (3016614)Termination phase: Saturation % 202.23/28.84 % (3016614)Time elapsed: 0.546 s % 202.23/28.84 % (3016614)Peak memory usage: 20 MB % 202.23/28.84 % (3016614)Instructions burned: 955 (million) % 202.23/28.84 % (3016616)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1142144859:fmbsr=1.3:i=1730:ins=25:rtra=on_2750 on theBenchmark for (2750ds/1730Mi) % 202.23/28.84 % (3016616)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 202.23/28.84 % (3016616)Terminated due to inappropriate strategy. % 202.23/28.84 % (3016616)------------------------------ % 202.23/28.84 % (3016616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.23/28.84 % (3016616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.23/28.84 % (3016616)CaDiCaL version: 2.1.3 % 202.23/28.84 % (3016616)Termination reason: Inappropriate % 237.47/33.85 % (3016616)Time elapsed: 0.042 s % 237.47/33.85 % (3016616)Peak memory usage: 14 MB % 237.47/33.85 % (3016616)Instructions burned: 86 (million) % 237.47/33.85 % (3016616)------------------------------ % 237.47/33.85 % (3016616)------------------------------ % 237.47/33.85 % (3016618)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2197736554:i=2358:rtra=on_2749 on theBenchmark for (2749ds/2358Mi) % 237.47/33.85 % (3016618)Instruction limit reached! % 237.47/33.85 % (3016618)------------------------------ % 237.47/33.85 % (3016618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.47/33.85 % (3016618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.47/33.85 % (3016618)CaDiCaL version: 2.1.3 % 237.47/33.85 % (3016618)Termination reason: Instruction limit % 237.47/33.85 % (3016618)Termination phase: Saturation % 237.47/33.85 % (3016618)Time elapsed: 1.399 s % 237.47/33.85 % (3016618)Peak memory usage: 25 MB % 237.47/33.85 % (3016618)Instructions burned: 2358 (million) % 237.47/33.85 % (3016620)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1352990076:i=1778:ins=1:rtra=on_2735 on theBenchmark for (2735ds/1778Mi) % 237.47/33.85 % (3016620)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 237.47/33.85 % (3016620)Terminated due to inappropriate strategy. % 237.47/33.85 % (3016620)------------------------------ % 237.47/33.85 % (3016620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.47/33.85 % (3016620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.47/33.85 % (3016620)CaDiCaL version: 2.1.3 % 237.47/33.85 % (3016620)Termination reason: Inappropriate % 237.47/33.85 % (3016620)Time elapsed: 0.057 s % 237.47/33.85 % (3016620)Peak memory usage: 16 MB % 237.47/33.85 % (3016620)Instructions burned: 116 (million) % 237.47/33.85 % (3016620)------------------------------ % 237.47/33.85 % (3016620)------------------------------ % 237.47/33.85 % (3016622)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=1811732311:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2734 on theBenchmark for (2734ds/1384Mi) % 237.47/33.85 % (3016579)Instruction limit reached! % 237.47/33.85 % (3016579)------------------------------ % 237.47/33.85 % (3016579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.47/33.85 % (3016579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.47/33.85 % (3016579)CaDiCaL version: 2.1.3 % 237.47/33.85 % (3016579)Termination reason: Instruction limit % 237.47/33.85 % (3016579)Termination phase: Saturation % 237.47/33.85 % (3016579)Time elapsed: 11.340 s % 237.47/33.85 % (3016579)Peak memory usage: 27 MB % 237.47/33.85 % (3016579)Instructions burned: 28121 (million) % 237.47/33.85 % (3016622)Instruction limit reached! % 237.47/33.85 % (3016622)------------------------------ % 237.47/33.85 % (3016622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.47/33.85 % (3016622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.47/33.85 % (3016622)CaDiCaL version: 2.1.3 % 237.47/33.85 % (3016622)Termination reason: Instruction limit % 237.47/33.85 % (3016622)Termination phase: Saturation % 237.47/33.85 % (3016622)Time elapsed: 0.863 s % 237.47/33.85 % (3016622)Peak memory usage: 27 MB % 237.47/33.85 % (3016622)Instructions burned: 1385 (million) % 237.47/33.85 % (3016624)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=552415593:i=1758:kws=inv_precedence:fsr=off:rtra=on_2725 on theBenchmark for (2725ds/1758Mi) % 237.47/33.85 % (3016625)fmb+10_1_sil=64000:si=on:random_seed=1678095278:i=44122:nm=2:rtra=on:gsp=on_2725 on theBenchmark for (2725ds/44122Mi) % 237.47/33.85 % (3016625)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 237.47/33.85 % (3016625)Terminated due to inappropriate strategy. % 237.47/33.85 % (3016625)------------------------------ % 237.47/33.85 % (3016625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 237.47/33.85 % (3016625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.47/33.85 % (3016625)CaDiCaL version: 2.1.3 % 237.47/33.85 % (3016625)Termination reason: Inappropriate % 237.47/33.85 % (3016625)Time elapsed: 0.046 s % 237.47/33.85 % (3016625)Peak memory usage: 14 MB % 237.47/33.85 % (3016625)Instructions burned: 94 (million) % 237.47/33.85 % (3016625)------------------------------ % 237.47/33.85 % (3016625)------------------------------ % 237.47/33.85 % (3016628)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2019017440:i=19030:nm=5:rtra=on_2724 on theBenchmark for (2724ds/19030Mi) % 276.30/39.24 % (3016628)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 276.30/39.24 % (3016628)Terminated due to inappropriate strategy. % 276.30/39.24 % (3016628)------------------------------ % 276.30/39.24 % (3016628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.30/39.24 % (3016628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.30/39.24 % (3016628)CaDiCaL version: 2.1.3 % 276.30/39.24 % (3016628)Termination reason: Inappropriate % 276.30/39.24 % (3016628)Time elapsed: 0.041 s % 276.30/39.24 % (3016628)Peak memory usage: 14 MB % 276.30/39.24 % (3016628)Instructions burned: 87 (million) % 276.30/39.24 % (3016628)------------------------------ % 276.30/39.24 % (3016628)------------------------------ % 276.30/39.24 % (3016630)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=259550656:fmbsr=1.7:i=1840:rtra=on_2724 on theBenchmark for (2724ds/1840Mi) % 276.30/39.24 % (3016630)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 276.30/39.24 % (3016630)Terminated due to inappropriate strategy. % 276.30/39.24 % (3016630)------------------------------ % 276.30/39.24 % (3016630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.30/39.24 % (3016630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.30/39.24 % (3016630)CaDiCaL version: 2.1.3 % 276.30/39.24 % (3016630)Termination reason: Inappropriate % 276.30/39.24 % (3016630)Time elapsed: 0.042 s % 276.30/39.24 % (3016630)Peak memory usage: 14 MB % 276.30/39.24 % (3016630)Instructions burned: 87 (million) % 276.30/39.24 % (3016630)------------------------------ % 276.30/39.24 % (3016630)------------------------------ % 276.30/39.24 % (3016632)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=778416638:i=10262:rtra=on_2723 on theBenchmark for (2723ds/10262Mi) % 276.30/39.24 % (3016575)Instruction limit reached! % 276.30/39.24 % (3016575)------------------------------ % 276.30/39.24 % (3016575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.30/39.24 % (3016575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.30/39.24 % (3016575)CaDiCaL version: 2.1.3 % 276.30/39.24 % (3016575)Termination reason: Instruction limit % 276.30/39.24 % (3016575)Termination phase: Saturation % 276.30/39.24 % (3016575)Time elapsed: 13.119 s % 276.30/39.24 % (3016575)Peak memory usage: 138 MB % 276.30/39.24 % (3016575)Instructions burned: 53295 (million) % 276.30/39.24 % (3016634)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3469100938:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2716 on theBenchmark for (2716ds/2944Mi) % 276.30/39.24 % (3016624)Instruction limit reached! % 276.30/39.24 % (3016624)------------------------------ % 276.30/39.24 % (3016624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.30/39.24 % (3016624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.30/39.24 % (3016624)CaDiCaL version: 2.1.3 % 276.30/39.24 % (3016624)Termination reason: Instruction limit % 276.30/39.24 % (3016624)Termination phase: Saturation % 276.30/39.24 % (3016624)Time elapsed: 1.010 s % 276.30/39.24 % (3016624)Peak memory usage: 27 MB % 276.30/39.24 % (3016624)Instructions burned: 1758 (million) % 276.30/39.24 % (3016636)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=940840527:i=12648:rtra=on_2715 on theBenchmark for (2715ds/12648Mi) % 276.30/39.24 % (3016636)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 276.30/39.24 % (3016636)Terminated due to inappropriate strategy. % 276.30/39.24 % (3016636)------------------------------ % 276.30/39.24 % (3016636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.30/39.24 % (3016636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.30/39.24 % (3016636)CaDiCaL version: 2.1.3 % 276.30/39.24 % (3016636)Termination reason: Inappropriate % 276.30/39.24 % (3016636)Time elapsed: 0.041 s % 276.30/39.24 % (3016636)Peak memory usage: 14 MB % 276.30/39.24 % (3016636)Instructions burned: 87 (million) % 276.30/39.24 % (3016636)------------------------------ % 276.30/39.24 % (3016636)------------------------------ % 276.30/39.24 % (3016638)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2700913362:fmbsr=2.30978:i=4348:rtra=on_2714 on theBenchmark for (2714ds/4348Mi) % 276.30/39.24 % (3016638)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 276.30/39.24 % (3016638)Terminated due to inappropriate strategy. % 276.30/39.24 % (3016638)-----------------Terminated % 300.05/42.63 % Vampire exiting %------------------------------------------------------------------------------