%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX152_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 : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:46:33 PM UTC 2026 % Result : Timeout 300.36s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX152_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n015.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 15:08:02 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.23 Running first-order model finding % 0.08/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 % 4.48/0.90 % (2699903)Will run a generic schedule for satisfiability detection. % 4.48/0.90 % (2699913)% WARNING: option uhcvi not known. % 4.48/0.90 % (2699913)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3033505122:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 4.48/0.90 % (2699915)dis+10_1_sil=32000:sp=arity:random_seed=3909702991:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 4.48/0.90 % (2699912)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2012022799_2999 on theBenchmark for (2999ds/0Mi) % 4.48/0.90 % (2699917)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=521430797:i=116_2999 on theBenchmark for (2999ds/116Mi) % 4.48/0.90 % (2699912)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.48/0.90 % (2699912)Terminated due to inappropriate strategy. % 4.48/0.90 % (2699912)------------------------------ % 4.48/0.90 % (2699912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.48/0.90 % (2699912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.48/0.90 % (2699912)CaDiCaL version: 2.1.3 % 4.48/0.90 % (2699912)Termination reason: Inappropriate % 4.48/0.90 % (2699912)Time elapsed: 0.001 s % 4.48/0.90 % (2699912)Peak memory usage: 10 MB % 4.48/0.90 % (2699912)Instructions burned: 2 (million) % 4.48/0.90 % (2699914)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1093948272:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 4.48/0.90 % (2699912)------------------------------ % 4.48/0.90 % (2699912)------------------------------ % 4.48/0.90 % (2699919)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3364708262:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 4.48/0.90 % (2699918)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=793567904:i=131_2999 on theBenchmark for (2999ds/131Mi) % 4.48/0.90 % (2699933)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1435270681:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 4.48/0.90 % (2699933)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.48/0.90 % (2699933)Terminated due to inappropriate strategy. % 4.48/0.90 % (2699933)------------------------------ % 4.48/0.90 % (2699933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.48/0.90 % (2699933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.48/0.90 % (2699933)CaDiCaL version: 2.1.3 % 4.48/0.90 % (2699933)Termination reason: Inappropriate % 4.48/0.90 % (2699933)Time elapsed: 0.001 s % 4.48/0.90 % (2699933)Peak memory usage: 10 MB % 4.48/0.90 % (2699933)Instructions burned: 2 (million) % 4.48/0.90 % (2699933)------------------------------ % 4.48/0.90 % (2699933)------------------------------ % 4.48/0.90 % (2699940)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4067123143:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.48/0.90 % (2699915)Instruction limit reached! % 4.48/0.90 % (2699915)------------------------------ % 4.48/0.90 % (2699915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.48/0.90 % (2699915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.48/0.90 % (2699915)CaDiCaL version: 2.1.3 % 4.48/0.90 % (2699915)Termination reason: Instruction limit % 4.48/0.90 % (2699915)Termination phase: Saturation % 4.48/0.90 % (2699915)Time elapsed: 0.066 s % 4.48/0.90 % (2699915)Peak memory usage: 13 MB % 4.48/0.90 % (2699915)Instructions burned: 104 (million) % 4.48/0.90 % (2699918)Instruction limit reached! % 4.48/0.90 % (2699918)------------------------------ % 4.48/0.90 % (2699918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.48/0.90 % (2699918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.48/0.90 % (2699918)CaDiCaL version: 2.1.3 % 4.48/0.90 % (2699918)Termination reason: Instruction limit % 4.48/0.90 % (2699918)Termination phase: Saturation % 4.48/0.90 % (2699918)Time elapsed: 0.076 s % 4.48/0.90 % (2699918)Peak memory usage: 14 MB % 4.48/0.90 % (2699918)Instructions burned: 132 (million) % 4.48/0.90 % (2699917)Instruction limit reached! % 4.48/0.90 % (2699917)------------------------------ % 4.48/0.90 % (2699917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.48/0.90 % (2699917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.48/0.90 % (2699917)CaDiCaL version: 2.1.3 % 4.48/0.90 % (2699917)Termination reason: Instruction limit % 5.69/1.15 % (2699917)Termination phase: Saturation % 5.69/1.15 % (2699917)Time elapsed: 0.086 s % 5.69/1.15 % (2699917)Peak memory usage: 13 MB % 5.69/1.15 % (2699917)Instructions burned: 117 (million) % 5.69/1.15 % (2699948)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=2019333944:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 5.69/1.15 % (2699952)ott-21_1_sil=16000:fs=off:random_seed=444130084:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.69/1.15 % (2699954)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3198653298:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.69/1.15 % (2699919)Instruction limit reached! % 5.69/1.15 % (2699919)------------------------------ % 5.69/1.15 % (2699919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.69/1.15 % (2699919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.69/1.15 % (2699919)CaDiCaL version: 2.1.3 % 5.69/1.15 % (2699919)Termination reason: Instruction limit % 5.69/1.15 % (2699919)Termination phase: Saturation % 5.69/1.15 % (2699919)Time elapsed: 0.118 s % 5.69/1.15 % (2699919)Peak memory usage: 13 MB % 5.69/1.15 % (2699919)Instructions burned: 160 (million) % 5.69/1.15 % (2699940)Instruction limit reached! % 5.69/1.15 % (2699940)------------------------------ % 5.69/1.15 % (2699940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.69/1.15 % (2699940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.69/1.15 % (2699940)CaDiCaL version: 2.1.3 % 5.69/1.15 % (2699940)Termination reason: Instruction limit % 5.69/1.15 % (2699940)Termination phase: Saturation % 5.69/1.15 % (2699940)Time elapsed: 0.088 s % 5.69/1.15 % (2699940)Peak memory usage: 14 MB % 5.69/1.15 % (2699940)Instructions burned: 131 (million) % 5.69/1.15 % (2699970)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2228288068:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.69/1.15 % (2699966)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3130504020:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.69/1.15 % (2699966)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.69/1.15 % (2699966)Terminated due to inappropriate strategy. % 5.69/1.15 % (2699966)------------------------------ % 5.69/1.15 % (2699966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.69/1.15 % (2699966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.69/1.15 % (2699966)CaDiCaL version: 2.1.3 % 5.69/1.15 % (2699966)Termination reason: Inappropriate % 5.69/1.15 % (2699966)Time elapsed: 0.002 s % 5.69/1.15 % (2699966)Peak memory usage: 10 MB % 5.69/1.15 % (2699966)Instructions burned: 2 (million) % 5.69/1.15 % (2699966)------------------------------ % 5.69/1.15 % (2699966)------------------------------ % 5.69/1.15 % (2699975)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1076852347:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.69/1.15 % (2699975)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.69/1.15 % (2699975)Terminated due to inappropriate strategy. % 5.69/1.15 % (2699975)------------------------------ % 5.69/1.15 % (2699975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.69/1.15 % (2699975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.69/1.15 % (2699975)CaDiCaL version: 2.1.3 % 5.69/1.15 % (2699975)Termination reason: Inappropriate % 5.69/1.15 % (2699975)Time elapsed: 0.001 s % 5.69/1.15 % (2699975)Peak memory usage: 10 MB % 5.69/1.15 % (2699975)Instructions burned: 2 (million) % 5.69/1.15 % (2699975)------------------------------ % 5.69/1.15 % (2699975)------------------------------ % 5.69/1.15 % (2699952)Instruction limit reached! % 5.69/1.15 % (2699952)------------------------------ % 5.69/1.15 % (2699952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.69/1.15 % (2699952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.69/1.15 % (2699952)CaDiCaL version: 2.1.3 % 5.69/1.15 % (2699952)Termination reason: Instruction limit % 5.69/1.15 % (2699952)Termination phase: Saturation % 5.69/1.15 % (2699952)Time elapsed: 0.091 s % 5.69/1.15 % (2699952)Peak memory usage: 12 MB % 5.69/1.15 % (2699952)Instructions burned: 181 (million) % 5.69/1.15 % (2699985)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=3419422802:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 31.60/4.75 % (2699986)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2182156449:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 31.60/4.75 % (2699948)Instruction limit reached! % 31.60/4.75 % (2699948)------------------------------ % 31.60/4.75 % (2699948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.60/4.75 % (2699948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.60/4.75 % (2699948)CaDiCaL version: 2.1.3 % 31.60/4.75 % (2699948)Termination reason: Instruction limit % 31.60/4.75 % (2699948)Termination phase: Saturation % 31.60/4.75 % (2699948)Time elapsed: 0.388 s % 31.60/4.75 % (2699948)Peak memory usage: 16 MB % 31.60/4.75 % (2699948)Instructions burned: 685 (million) % 31.60/4.75 % (2699989)fmb+10_1_sil=64000:random_seed=769479032:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 31.60/4.75 % (2699989)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.60/4.75 % (2699989)Terminated due to inappropriate strategy. % 31.60/4.75 % (2699989)------------------------------ % 31.60/4.75 % (2699989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.60/4.75 % (2699989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.60/4.75 % (2699989)CaDiCaL version: 2.1.3 % 31.60/4.75 % (2699989)Termination reason: Inappropriate % 31.60/4.75 % (2699989)Time elapsed: 0.001 s % 31.60/4.75 % (2699989)Peak memory usage: 10 MB % 31.60/4.75 % (2699989)Instructions burned: 2 (million) % 31.60/4.75 % (2699989)------------------------------ % 31.60/4.75 % (2699989)------------------------------ % 31.60/4.75 % (2699991)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3803224050:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 31.60/4.75 % (2699991)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.60/4.75 % (2699991)Terminated due to inappropriate strategy. % 31.60/4.75 % (2699991)------------------------------ % 31.60/4.75 % (2699991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.60/4.75 % (2699991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.60/4.75 % (2699991)CaDiCaL version: 2.1.3 % 31.60/4.75 % (2699991)Termination reason: Inappropriate % 31.60/4.75 % (2699991)Time elapsed: 0.001 s % 31.60/4.75 % (2699991)Peak memory usage: 10 MB % 31.60/4.75 % (2699991)Instructions burned: 2 (million) % 31.60/4.75 % (2699991)------------------------------ % 31.60/4.75 % (2699991)------------------------------ % 31.60/4.75 % (2699993)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1596936806:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 31.60/4.75 % (2699993)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.60/4.75 % (2699993)Terminated due to inappropriate strategy. % 31.60/4.75 % (2699993)------------------------------ % 31.60/4.75 % (2699993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.60/4.75 % (2699993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.60/4.75 % (2699993)CaDiCaL version: 2.1.3 % 31.60/4.75 % (2699993)Termination reason: Inappropriate % 31.60/4.75 % (2699993)Time elapsed: 0.001 s % 31.60/4.75 % (2699993)Peak memory usage: 10 MB % 31.60/4.75 % (2699993)Instructions burned: 2 (million) % 31.60/4.75 % (2699993)------------------------------ % 31.60/4.75 % (2699993)------------------------------ % 31.60/4.75 % (2699954)Instruction limit reached! % 31.60/4.75 % (2699954)------------------------------ % 31.60/4.75 % (2699954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.60/4.75 % (2699954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.60/4.75 % (2699954)CaDiCaL version: 2.1.3 % 31.60/4.75 % (2699954)Termination reason: Instruction limit % 31.60/4.75 % (2699954)Termination phase: Saturation % 31.60/4.75 % (2699954)Time elapsed: 0.441 s % 31.60/4.75 % (2699954)Peak memory usage: 14 MB % 31.60/4.75 % (2699954)Instructions burned: 478 (million) % 31.60/4.75 % (2699995)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3628880171:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 31.60/4.75 % (2699996)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1234957093:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 31.60/4.75 % (2699985)Instruction limit reached! % 31.60/4.75 % (2699985)------------------------------ % 50.06/7.33 % (2699985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.06/7.33 % (2699985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.06/7.33 % (2699985)CaDiCaL version: 2.1.3 % 50.06/7.33 % (2699985)Termination reason: Instruction limit % 50.06/7.33 % (2699985)Termination phase: Saturation % 50.06/7.33 % (2699985)Time elapsed: 0.406 s % 50.06/7.33 % (2699985)Peak memory usage: 16 MB % 50.06/7.33 % (2699985)Instructions burned: 693 (million) % 50.06/7.33 % (2699999)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3346725522:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 50.06/7.33 % (2699999)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 50.06/7.33 % (2699999)Terminated due to inappropriate strategy. % 50.06/7.33 % (2699999)------------------------------ % 50.06/7.33 % (2699999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.06/7.33 % (2699999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.06/7.33 % (2699999)CaDiCaL version: 2.1.3 % 50.06/7.33 % (2699999)Termination reason: Inappropriate % 50.06/7.33 % (2699999)Time elapsed: 0.001 s % 50.06/7.33 % (2699999)Peak memory usage: 10 MB % 50.06/7.33 % (2699999)Instructions burned: 2 (million) % 50.06/7.33 % (2699999)------------------------------ % 50.06/7.33 % (2699999)------------------------------ % 50.06/7.33 % (2700001)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=938632105:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 50.06/7.33 % (2700001)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 50.06/7.33 % (2700001)Terminated due to inappropriate strategy. % 50.06/7.33 % (2700001)------------------------------ % 50.06/7.33 % (2700001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.06/7.33 % (2700001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.06/7.33 % (2700001)CaDiCaL version: 2.1.3 % 50.06/7.33 % (2700001)Termination reason: Inappropriate % 50.06/7.33 % (2700001)Time elapsed: 0.001 s % 50.06/7.33 % (2700001)Peak memory usage: 10 MB % 50.06/7.33 % (2700001)Instructions burned: 2 (million) % 50.06/7.33 % (2700001)------------------------------ % 50.06/7.33 % (2700001)------------------------------ % 50.06/7.33 % (2700003)ott-2_1_sil=16000:newcnf=on:random_seed=1739016310:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 50.06/7.33 % (2699986)Instruction limit reached! % 50.06/7.33 % (2699986)------------------------------ % 50.06/7.33 % (2699986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.06/7.33 % (2699986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.06/7.33 % (2699986)CaDiCaL version: 2.1.3 % 50.06/7.33 % (2699986)Termination reason: Instruction limit % 50.06/7.33 % (2699986)Termination phase: Saturation % 50.06/7.33 % (2699986)Time elapsed: 0.498 s % 50.06/7.33 % (2699986)Peak memory usage: 22 MB % 50.06/7.33 % (2699986)Instructions burned: 881 (million) % 50.06/7.33 % (2700005)ott+10_1_sil=32000:tgt=ground:random_seed=252464150:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 50.06/7.33 % (2699970)Instruction limit reached! % 50.06/7.33 % (2699970)------------------------------ % 50.06/7.33 % (2699970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.06/7.33 % (2699970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.06/7.33 % (2699970)CaDiCaL version: 2.1.3 % 50.06/7.33 % (2699970)Termination reason: Instruction limit % 50.06/7.33 % (2699970)Termination phase: Saturation % 50.06/7.33 % (2699970)Time elapsed: 0.701 s % 50.06/7.33 % (2699970)Peak memory usage: 19 MB % 50.06/7.33 % (2699970)Instructions burned: 1180 (million) % 50.06/7.33 % (2700008)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2620816201:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 50.06/7.33 % (2700008)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 50.06/7.33 % (2700008)Terminated due to inappropriate strategy. % 50.06/7.33 % (2700008)------------------------------ % 50.06/7.33 % (2700008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.06/7.33 % (2700008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.06/7.33 % (2700008)CaDiCaL version: 2.1.3 % 50.06/7.33 % (2700008)Termination reason: Inappropriate % 50.06/7.33 % (2700008)Time elapsed: 0.001 s % 50.06/7.33 % (2700008)Peak memory usage: 10 MB % 50.06/7.33 % (2700008)Instructions burned: 2 (million) % 148.89/21.24 % (2700008)------------------------------ % 148.89/21.24 % (2700008)------------------------------ % 148.89/21.24 % (2700010)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1688966819:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 148.89/21.24 % (2700003)Instruction limit reached! % 148.89/21.24 % (2700003)------------------------------ % 148.89/21.24 % (2700003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.89/21.24 % (2700003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.89/21.24 % (2700003)CaDiCaL version: 2.1.3 % 148.89/21.24 % (2700003)Termination reason: Instruction limit % 148.89/21.24 % (2700003)Termination phase: Saturation % 148.89/21.24 % (2700003)Time elapsed: 0.655 s % 148.89/21.24 % (2700003)Peak memory usage: 16 MB % 148.89/21.24 % (2700003)Instructions burned: 869 (million) % 148.89/21.24 % (2700036)dis+21_1_sil=32000:sas=cadical:random_seed=1257792863:i=3773:amm=off_2986 on theBenchmark for (2986ds/3773Mi) % 148.89/21.24 % (2699996)Instruction limit reached! % 148.89/21.24 % (2699996)------------------------------ % 148.89/21.24 % (2699996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.89/21.24 % (2699996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.89/21.24 % (2699996)CaDiCaL version: 2.1.3 % 148.89/21.24 % (2699996)Termination reason: Instruction limit % 148.89/21.24 % (2699996)Termination phase: Saturation % 148.89/21.24 % (2699996)Time elapsed: 1.178 s % 148.89/21.24 % (2699996)Peak memory usage: 24 MB % 148.89/21.24 % (2699996)Instructions burned: 1472 (million) % 148.89/21.24 % (2700060)ott+11_1_sil=16000:gs=on:random_seed=1623852732:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2982 on theBenchmark for (2982ds/2251Mi) % 148.89/21.24 % (2700010)Instruction limit reached! % 148.89/21.24 % (2700010)------------------------------ % 148.89/21.24 % (2700010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.89/21.24 % (2700010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.89/21.24 % (2700010)CaDiCaL version: 2.1.3 % 148.89/21.24 % (2700010)Termination reason: Instruction limit % 148.89/21.24 % (2700010)Termination phase: Saturation % 148.89/21.24 % (2700010)Time elapsed: 2.728 s % 148.89/21.24 % (2700010)Peak memory usage: 30 MB % 148.89/21.24 % (2700010)Instructions burned: 3512 (million) % 148.89/21.24 % (2700127)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1255240594:fmbsr=1.6:i=67534_2963 on theBenchmark for (2963ds/67534Mi) % 148.89/21.24 % (2700127)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.89/21.24 % (2700127)Terminated due to inappropriate strategy. % 148.89/21.24 % (2700127)------------------------------ % 148.89/21.24 % (2700127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.89/21.24 % (2700127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.89/21.24 % (2700127)CaDiCaL version: 2.1.3 % 148.89/21.24 % (2700127)Termination reason: Inappropriate % 148.89/21.24 % (2700127)Time elapsed: 0.002 s % 148.89/21.24 % (2700127)Peak memory usage: 10 MB % 148.89/21.24 % (2700127)Instructions burned: 2 (million) % 148.89/21.24 % (2700127)------------------------------ % 148.89/21.24 % (2700127)------------------------------ % 148.89/21.24 % (2700129)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2008786645:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2962 on theBenchmark for (2962ds/4591Mi) % 148.89/21.24 % (2700060)Instruction limit reached! % 148.89/21.24 % (2700060)------------------------------ % 148.89/21.24 % (2700060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.89/21.24 % (2700060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.89/21.24 % (2700060)CaDiCaL version: 2.1.3 % 148.89/21.24 % (2700060)Termination reason: Instruction limit % 148.89/21.24 % (2700060)Termination phase: Saturation % 148.89/21.24 % (2700060)Time elapsed: 1.923 s % 148.89/21.24 % (2700060)Peak memory usage: 23 MB % 148.89/21.24 % (2700060)Instructions burned: 2251 (million) % 148.89/21.24 % (2700133)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3488328093:i=29340_2962 on theBenchmark for (2962ds/29340Mi) % 148.89/21.24 % (2700036)Instruction limit reached! % 148.89/21.24 % (2700036)------------------------------ % 148.89/21.24 % (2700036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.89/21.24 % (2700036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.89/21.24 % (2700036)CaDiCaL version: 2.1.3 % 148.89/21.24 % (2700036)Termination reason: Instruction limit % 191.60/27.24 % (2700036)Termination phase: Saturation % 191.60/27.24 % (2700036)Time elapsed: 3.093 s % 191.60/27.24 % (2700036)Peak memory usage: 31 MB % 191.60/27.24 % (2700036)Instructions burned: 3773 (million) % 191.60/27.24 % (2700152)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=273834575:i=5211_2954 on theBenchmark for (2954ds/5211Mi) % 191.60/27.24 % (2699995)Instruction limit reached! % 191.60/27.24 % (2699995)------------------------------ % 191.60/27.24 % (2699995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.60/27.24 % (2699995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.60/27.24 % (2699995)CaDiCaL version: 2.1.3 % 191.60/27.24 % (2699995)Termination reason: Instruction limit % 191.60/27.24 % (2699995)Termination phase: Saturation % 191.60/27.24 % (2699995)Time elapsed: 3.982 s % 191.60/27.24 % (2699995)Peak memory usage: 40 MB % 191.60/27.24 % (2699995)Instructions burned: 5131 (million) % 191.60/27.24 % (2700157)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1865391844:i=5497:nm=2_2954 on theBenchmark for (2954ds/5497Mi) % 191.60/27.24 % (2700157)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.60/27.24 % (2700157)Terminated due to inappropriate strategy. % 191.60/27.24 % (2700157)------------------------------ % 191.60/27.24 % (2700157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.60/27.24 % (2700157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.60/27.24 % (2700157)CaDiCaL version: 2.1.3 % 191.60/27.24 % (2700157)Termination reason: Inappropriate % 191.60/27.24 % (2700157)Time elapsed: 0.002 s % 191.60/27.24 % (2700157)Peak memory usage: 10 MB % 191.60/27.24 % (2700157)Instructions burned: 2 (million) % 191.60/27.24 % (2700157)------------------------------ % 191.60/27.24 % (2700157)------------------------------ % 191.60/27.24 % (2700160)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4167233937:fmbsr=2:i=46332_2953 on theBenchmark for (2953ds/46332Mi) % 191.60/27.24 % (2700160)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.60/27.24 % (2700160)Terminated due to inappropriate strategy. % 191.60/27.24 % (2700160)------------------------------ % 191.60/27.24 % (2700160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.60/27.24 % (2700160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.60/27.24 % (2700160)CaDiCaL version: 2.1.3 % 191.60/27.24 % (2700160)Termination reason: Inappropriate % 191.60/27.24 % (2700160)Time elapsed: 0.002 s % 191.60/27.24 % (2700160)Peak memory usage: 10 MB % 191.60/27.24 % (2700160)Instructions burned: 2 (million) % 191.60/27.24 % (2700160)------------------------------ % 191.60/27.24 % (2700160)------------------------------ % 191.60/27.24 % (2700163)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3256772599:i=14071_2953 on theBenchmark for (2953ds/14071Mi) % 191.60/27.24 % (2700163)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 191.60/27.24 % (2700163)Terminated due to inappropriate strategy. % 191.60/27.24 % (2700163)------------------------------ % 191.60/27.24 % (2700163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.60/27.24 % (2700163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.60/27.24 % (2700163)CaDiCaL version: 2.1.3 % 191.60/27.24 % (2700163)Termination reason: Inappropriate % 191.60/27.24 % (2700163)Time elapsed: 0.001 s % 191.60/27.24 % (2700163)Peak memory usage: 10 MB % 191.60/27.24 % (2700163)Instructions burned: 2 (million) % 191.60/27.24 % (2700163)------------------------------ % 191.60/27.24 % (2700163)------------------------------ % 191.60/27.24 % (2700165)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=489866010:i=22565:add=on:rawr=on_2953 on theBenchmark for (2953ds/22565Mi) % 191.60/27.24 % (2700005)Instruction limit reached! % 191.60/27.24 % (2700005)------------------------------ % 191.60/27.24 % (2700005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.60/27.24 % (2700005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.60/27.24 % (2700005)CaDiCaL version: 2.1.3 % 191.60/27.24 % (2700005)Termination reason: Instruction limit % 191.60/27.24 % (2700005)Termination phase: Saturation % 191.60/27.24 % (2700005)Time elapsed: 4.493 s % 191.60/27.24 % (2700005)Peak memory usage: 31 MB % 191.60/27.24 % (2700005)Instructions burned: 5114 (million) % 191.60/27.24 % (2700183)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3138019413:i=8173:av=off_2947 on theBenchmark for (2947ds/8173Mi) % 191.60/27.24 % (2700129)Instruction limit reached! % 192.32/27.37 % (2700129)------------------------------ % 192.32/27.37 % (2700129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.32/27.37 % (2700129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.32/27.37 % (2700129)CaDiCaL version: 2.1.3 % 192.32/27.37 % (2700129)Termination reason: Instruction limit % 192.32/27.37 % (2700129)Termination phase: Saturation % 192.32/27.37 % (2700129)Time elapsed: 3.339 s % 192.32/27.37 % (2700129)Peak memory usage: 25 MB % 192.32/27.37 % (2700129)Instructions burned: 4592 (million) % 192.32/27.37 % (2700218)dis+10_16:1_sil=16000:random_seed=2491196352:i=9155:fsr=off_2929 on theBenchmark for (2929ds/9155Mi) % 192.32/27.37 % (2700152)Instruction limit reached! % 192.32/27.37 % (2700152)------------------------------ % 192.32/27.37 % (2700152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.32/27.37 % (2700152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.32/27.37 % (2700152)CaDiCaL version: 2.1.3 % 192.32/27.37 % (2700152)Termination reason: Instruction limit % 192.32/27.37 % (2700152)Termination phase: Saturation % 192.32/27.37 % (2700152)Time elapsed: 4.512 s % 192.32/27.37 % (2700152)Peak memory usage: 61 MB % 192.32/27.37 % (2700152)Instructions burned: 5212 (million) % 192.32/27.37 % (2700244)ott-3_8_sil=64000:random_seed=2072078591:i=20139:bs=on_2909 on theBenchmark for (2909ds/20139Mi) % 192.32/27.37 % (2700183)Instruction limit reached! % 192.32/27.37 % (2700183)------------------------------ % 192.32/27.37 % (2700183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.32/27.37 % (2700183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.32/27.37 % (2700183)CaDiCaL version: 2.1.3 % 192.32/27.37 % (2700183)Termination reason: Instruction limit % 192.32/27.37 % (2700183)Termination phase: Saturation % 192.32/27.37 % (2700183)Time elapsed: 7.902 s % 192.32/27.37 % (2700183)Peak memory usage: 46 MB % 192.32/27.37 % (2700183)Instructions burned: 8173 (million) % 192.32/27.37 % (2700276)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4219937120:fmbsr=2:i=32576_2867 on theBenchmark for (2867ds/32576Mi) % 192.32/27.37 % (2700276)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.32/27.37 % (2700276)Terminated due to inappropriate strategy. % 192.32/27.37 % (2700276)------------------------------ % 192.32/27.37 % (2700276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.32/27.37 % (2700276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.32/27.37 % (2700276)CaDiCaL version: 2.1.3 % 192.32/27.37 % (2700276)Termination reason: Inappropriate % 192.32/27.37 % (2700276)Time elapsed: 0.002 s % 192.32/27.37 % (2700276)Peak memory usage: 10 MB % 192.32/27.37 % (2700276)Instructions burned: 2 (million) % 192.32/27.37 % (2700276)------------------------------ % 192.32/27.37 % (2700276)------------------------------ % 192.32/27.37 % (2700279)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2450857835:i=11404_2867 on theBenchmark for (2867ds/11404Mi) % 192.32/27.37 % (2700218)Instruction limit reached! % 192.32/27.37 % (2700218)------------------------------ % 192.32/27.37 % (2700218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.32/27.37 % (2700218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.32/27.37 % (2700218)CaDiCaL version: 2.1.3 % 192.32/27.37 % (2700218)Termination reason: Instruction limit % 192.32/27.37 % (2700218)Termination phase: Saturation % 192.32/27.37 % (2700218)Time elapsed: 7.675 s % 192.32/27.37 % (2700218)Peak memory usage: 51 MB % 192.32/27.37 % (2700218)Instructions burned: 9156 (million) % 192.32/27.37 % (2700284)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1903095606:i=14134_2851 on theBenchmark for (2851ds/14134Mi) % 192.32/27.37 % (2700279)Instruction limit reached! % 192.32/27.37 % (2700279)------------------------------ % 192.32/27.37 % (2700279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.32/27.37 % (2700279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.32/27.37 % (2700279)CaDiCaL version: 2.1.3 % 192.32/27.37 % (2700279)Termination reason: Instruction limit % 192.32/27.37 % (2700279)Termination phase: Saturation % 192.32/27.37 % (2700279)Time elapsed: 6.069 s % 192.32/27.37 % (2700279)Peak memory usage: 44 MB % 192.32/27.37 % (2700279)Instructions burned: 11405 (million) % 192.32/27.37 % (2700299)dis+33_16_sil=32000:sac=on:random_seed=1343855579:i=15851:nm=0_2806 on theBenchmark for (2806ds/15851Mi) % 192.32/27.37 % (2700165)Instruction limit reached! % 192.32/27.37 % (2700165)------------------------------ % 192.32/27.37 % (2700165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.14/37.43 % (2700165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.14/37.43 % (2700165)CaDiCaL version: 2.1.3 % 264.14/37.43 % (2700165)Termination reason: Instruction limit % 264.14/37.43 % (2700165)Termination phase: Saturation % 264.14/37.43 % (2700165)Time elapsed: 16.299 s % 264.14/37.43 % (2700165)Peak memory usage: 182 MB % 264.14/37.43 % (2700165)Instructions burned: 22565 (million) % 264.14/37.43 % (2700307)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3305138243:avsq=on:i=17627:add=on:amm=off_2789 on theBenchmark for (2789ds/17627Mi) % 264.14/37.43 % (2700299)Instruction limit reached! % 264.14/37.43 % (2700299)------------------------------ % 264.14/37.43 % (2700299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.14/37.43 % (2700299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.14/37.43 % (2700299)CaDiCaL version: 2.1.3 % 264.14/37.43 % (2700299)Termination reason: Instruction limit % 264.14/37.43 % (2700299)Termination phase: Saturation % 264.14/37.43 % (2700299)Time elapsed: 6.735 s % 264.14/37.43 % (2700299)Peak memory usage: 42 MB % 264.14/37.43 % (2700299)Instructions burned: 15852 (million) % 264.14/37.43 % (2700324)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3864385634:s2a=on:i=53295_2738 on theBenchmark for (2738ds/53295Mi) % 264.14/37.43 % (2700244)Instruction limit reached! % 264.14/37.43 % (2700244)------------------------------ % 264.14/37.43 % (2700244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.14/37.43 % (2700244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.14/37.43 % (2700244)CaDiCaL version: 2.1.3 % 264.14/37.43 % (2700244)Termination reason: Instruction limit % 264.14/37.43 % (2700244)Termination phase: Saturation % 264.14/37.43 % (2700244)Time elapsed: 17.447 s % 264.14/37.43 % (2700244)Peak memory usage: 57 MB % 264.14/37.43 % (2700244)Instructions burned: 20139 (million) % 264.14/37.43 % (2700328)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=747707415:i=26857:ins=20_2734 on theBenchmark for (2734ds/26857Mi) % 264.14/37.43 % (2700328)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 264.14/37.43 % (2700328)Terminated due to inappropriate strategy. % 264.14/37.43 % (2700328)------------------------------ % 264.14/37.43 % (2700328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.14/37.43 % (2700328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.14/37.43 % (2700328)CaDiCaL version: 2.1.3 % 264.14/37.43 % (2700328)Termination reason: Inappropriate % 264.14/37.43 % (2700328)Time elapsed: 0.002 s % 264.14/37.43 % (2700328)Peak memory usage: 10 MB % 264.14/37.43 % (2700328)Instructions burned: 2 (million) % 264.14/37.43 % (2700328)------------------------------ % 264.14/37.43 % (2700328)------------------------------ % 264.14/37.43 % (2700330)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2492099979:i=28120:bs=on:fsr=off_2733 on theBenchmark for (2733ds/28120Mi) % 264.14/37.43 % (2700133)Instruction limit reached! % 264.14/37.43 % (2700133)------------------------------ % 264.14/37.43 % (2700133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.14/37.43 % (2700133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.14/37.43 % (2700133)CaDiCaL version: 2.1.3 % 264.14/37.43 % (2700133)Termination reason: Instruction limit % 264.14/37.43 % (2700133)Termination phase: Saturation % 264.14/37.43 % (2700133)Time elapsed: 23.110 s % 264.14/37.43 % (2700133)Peak memory usage: 148 MB % 264.14/37.43 % (2700133)Instructions burned: 29341 (million) % 264.14/37.43 % (2700332)fmb+10_1_sil=256000:fmbss=7:random_seed=1391577211:fmbsr=1.6:i=182295_2730 on theBenchmark for (2730ds/182295Mi) % 264.14/37.43 % (2700332)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 264.14/37.43 % (2700332)Terminated due to inappropriate strategy. % 264.14/37.43 % (2700332)------------------------------ % 264.14/37.43 % (2700332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 264.14/37.43 % (2700332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.14/37.43 % (2700332)CaDiCaL version: 2.1.3 % 264.14/37.43 % (2700332)Termination reason: Inappropriate % 264.14/37.43 % (2700332)Time elapsed: 0.003 s % 264.14/37.43 % (2700332)Peak memory usage: 10 MB % 264.14/37.43 % (2700332)Instructions burned: 2 (million) % 264.14/37.43 % (2700332)------------------------------ % 264.14/37.43 % (2700332)------------------------------ % 264.14/37.43 % (2700334)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=988313831:i=44625:gsp=on_2730 on theBenchmark for (2730ds/44625Mi) % 284.75/40.30 % (2700334)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.75/40.30 % (2700334)Terminated due to inappropriate strategy. % 284.75/40.30 % (2700334)------------------------------ % 284.75/40.30 % (2700334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.75/40.30 % (2700334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.75/40.30 % (2700334)CaDiCaL version: 2.1.3 % 284.75/40.30 % (2700334)Termination reason: Inappropriate % 284.75/40.30 % (2700334)Time elapsed: 0.002 s % 284.75/40.30 % (2700334)Peak memory usage: 10 MB % 284.75/40.30 % (2700334)Instructions burned: 2 (million) % 284.75/40.30 % (2700334)------------------------------ % 284.75/40.30 % (2700334)------------------------------ % 284.75/40.30 % (2700336)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2226515952:i=160505_2729 on theBenchmark for (2729ds/160505Mi) % 284.75/40.30 % (2700336)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.75/40.30 % (2700336)Terminated due to inappropriate strategy. % 284.75/40.30 % (2700336)------------------------------ % 284.75/40.30 % (2700336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.75/40.30 % (2700336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.75/40.30 % (2700336)CaDiCaL version: 2.1.3 % 284.75/40.30 % (2700336)Termination reason: Inappropriate % 284.75/40.30 % (2700336)Time elapsed: 0.001 s % 284.75/40.30 % (2700336)Peak memory usage: 10 MB % 284.75/40.30 % (2700336)Instructions burned: 2 (million) % 284.75/40.30 % (2700336)------------------------------ % 284.75/40.30 % (2700336)------------------------------ % 284.75/40.30 % (2700338)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=630136610:fmbsr=1.3:i=225729_2729 on theBenchmark for (2729ds/225729Mi) % 284.75/40.30 % (2700338)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.75/40.30 % (2700338)Terminated due to inappropriate strategy. % 284.75/40.30 % (2700338)------------------------------ % 284.75/40.30 % (2700338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.75/40.30 % (2700338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.75/40.30 % (2700338)CaDiCaL version: 2.1.3 % 284.75/40.30 % (2700338)Termination reason: Inappropriate % 284.75/40.30 % (2700338)Time elapsed: 0.001 s % 284.75/40.30 % (2700338)Peak memory usage: 10 MB % 284.75/40.30 % (2700338)Instructions burned: 2 (million) % 284.75/40.30 % (2700338)------------------------------ % 284.75/40.30 % (2700338)------------------------------ % 284.75/40.30 % (2700340)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=886041402:fmbsr=2:i=185024:ins=7_2729 on theBenchmark for (2729ds/185024Mi) % 284.75/40.30 % (2700340)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.75/40.30 % (2700340)Terminated due to inappropriate strategy. % 284.75/40.30 % (2700340)------------------------------ % 284.75/40.30 % (2700340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.75/40.30 % (2700340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.75/40.30 % (2700340)CaDiCaL version: 2.1.3 % 284.75/40.30 % (2700340)Termination reason: Inappropriate % 284.75/40.30 % (2700340)Time elapsed: 0.002 s % 284.75/40.30 % (2700340)Peak memory usage: 10 MB % 284.75/40.30 % (2700340)Instructions burned: 2 (million) % 284.75/40.30 % (2700340)------------------------------ % 284.75/40.30 % (2700340)------------------------------ % 284.75/40.30 % (2700342)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3706564052:rtra=on_2729 on theBenchmark for (2729ds/0Mi) % 284.75/40.30 % (2700342)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.75/40.30 % (2700342)Terminated due to inappropriate strategy. % 284.75/40.30 % (2700342)------------------------------ % 284.75/40.30 % (2700342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.75/40.30 % (2700342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.75/40.30 % (2700342)CaDiCaL version: 2.1.3 % 284.75/40.30 % (2700342)Termination reason: Inappropriate % 284.75/40.30 % (2700342)Time elapsed: 0.002 s % 284.75/40.30 % (2700342)Peak memory usage: 10 MB % 284.75/40.30 % (2700342)Instructions burned: 2 (million) % 284.75/40.30 % (2700342)------------------------------ % 284.75/40.30 % (2700342)------------------------------ % 284.75/40.30 % (2700344)% WARNING: option uhcvi not known. % 284.75/40.30 % (2700344)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=919009090:i=2710Terminated % 300.36/42.54 % Vampire exiting % 300.36/42.54 Terminated %------------------------------------------------------------------------------