%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX139_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 : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:46:32 PM UTC 2026 % Result : Timeout 295.62s 42.04s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX139_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.09/0.20 % Computer : n017.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 15:00:06 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.24 Running first-order model finding % 0.09/0.24 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.50/0.77 % (3617345)Will run a generic schedule for satisfiability detection. % 2.50/0.77 % (3617353)dis+10_1_sil=32000:sp=arity:random_seed=2572199718:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.50/0.77 % (3617351)% WARNING: option uhcvi not known. % 2.50/0.77 % (3617352)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4282220162:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.50/0.77 % (3617351)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1628268770:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.50/0.77 % (3617350)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2935019762_2999 on theBenchmark for (2999ds/0Mi) % 2.50/0.77 % (3617354)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2965231219:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.50/0.77 % (3617356)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=242276651:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.50/0.77 % (3617355)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3595111610:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.50/0.77 % (3617353)Instruction limit reached! % 2.50/0.77 % (3617353)------------------------------ % 2.50/0.77 % (3617353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.50/0.77 % (3617353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.50/0.77 % (3617353)CaDiCaL version: 2.1.3 % 2.50/0.77 % (3617353)Termination reason: Instruction limit % 2.50/0.77 % (3617353)Termination phase: Property scanning % 2.50/0.77 % (3617353)Time elapsed: 0.022 s % 2.50/0.77 % (3617353)Peak memory usage: 10 MB % 2.50/0.77 % (3617353)Instructions burned: 107 (million) % 2.50/0.77 % (3617373)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2162338342:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 2.50/0.77 % (3617350)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.50/0.77 % (3617350)Terminated due to inappropriate strategy. % 2.50/0.77 % (3617350)------------------------------ % 2.50/0.77 % (3617350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.50/0.77 % (3617350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.50/0.77 % (3617350)CaDiCaL version: 2.1.3 % 2.50/0.77 % (3617350)Termination reason: Inappropriate % 2.50/0.77 % (3617350)Time elapsed: 0.045 s % 2.50/0.77 % (3617354)Instruction limit reached! % 2.50/0.77 % (3617354)------------------------------ % 2.50/0.77 % (3617354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.50/0.77 % (3617350)Peak memory usage: 10 MB % 2.50/0.77 % (3617350)Instructions burned: 118 (million) % 2.50/0.77 % (3617354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.50/0.77 % (3617354)CaDiCaL version: 2.1.3 % 2.50/0.77 % (3617354)Termination reason: Instruction limit % 2.50/0.77 % (3617354)Termination phase: Blocked clause elimination % 2.50/0.77 % (3617354)Time elapsed: 0.045 s % 2.50/0.77 % (3617354)Peak memory usage: 10 MB % 2.50/0.77 % (3617354)Instructions burned: 118 (million) % 2.50/0.77 % (3617350)------------------------------ % 2.50/0.77 % (3617350)------------------------------ % 2.50/0.77 % (3617373)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.50/0.77 % (3617373)Terminated due to inappropriate strategy. % 2.50/0.77 % (3617373)------------------------------ % 2.50/0.77 % (3617373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.50/0.77 % (3617373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.50/0.77 % (3617373)CaDiCaL version: 2.1.3 % 2.50/0.77 % (3617373)Termination reason: Inappropriate % 2.50/0.77 % (3617373)Time elapsed: 0.024 s % 2.50/0.77 % (3617373)Peak memory usage: 10 MB % 2.50/0.77 % (3617373)Instructions burned: 118 (million) % 2.50/0.77 % (3617373)------------------------------ % 2.50/0.77 % (3617373)------------------------------ % 2.50/0.77 % (3617355)Instruction limit reached! % 2.50/0.77 % (3617355)------------------------------ % 2.50/0.77 % (3617355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.50/0.77 % (3617355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.50/0.77 % (3617355)CaDiCaL version: 2.1.3 % 2.50/0.77 % (3617355)Termination reason: Instruction limit % 2.50/0.77 % (3617355)Termination phase: Saturation % 2.50/0.77 % (3617355)Time elapsed: 0.052 s % 2.50/0.77 % (3617355)Peak memory usage: 12 MB % 3.41/1.02 % (3617355)Instructions burned: 132 (million) % 3.41/1.02 % (3617380)ott-21_1_sil=16000:fs=off:random_seed=2942711150:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 3.41/1.02 % (3617377)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2117164963:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 3.41/1.02 % (3617378)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=2346559656:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 3.41/1.02 % (3617356)Instruction limit reached! % 3.41/1.02 % (3617356)------------------------------ % 3.41/1.02 % (3617356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.41/1.02 % (3617356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.41/1.02 % (3617356)CaDiCaL version: 2.1.3 % 3.41/1.02 % (3617356)Termination reason: Instruction limit % 3.41/1.02 % (3617356)Termination phase: Saturation % 3.41/1.02 % (3617356)Time elapsed: 0.063 s % 3.41/1.02 % (3617356)Peak memory usage: 12 MB % 3.41/1.02 % (3617356)Instructions burned: 162 (million) % 3.41/1.02 % (3617384)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2130534641:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 3.41/1.02 % (3617390)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3438073901:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 3.41/1.02 % (3617380)Instruction limit reached! % 3.41/1.02 % (3617380)------------------------------ % 3.41/1.02 % (3617380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.41/1.02 % (3617380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.41/1.02 % (3617380)CaDiCaL version: 2.1.3 % 3.41/1.02 % (3617380)Termination reason: Instruction limit % 3.41/1.02 % (3617380)Termination phase: Saturation % 3.41/1.02 % (3617380)Time elapsed: 0.037 s % 3.41/1.02 % (3617380)Peak memory usage: 11 MB % 3.41/1.02 % (3617380)Instructions burned: 183 (million) % 3.41/1.02 % (3617401)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3066483835:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 3.41/1.02 % (3617377)Instruction limit reached! % 3.41/1.02 % (3617377)------------------------------ % 3.41/1.02 % (3617377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.41/1.02 % (3617377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.41/1.02 % (3617377)CaDiCaL version: 2.1.3 % 3.41/1.02 % (3617377)Termination reason: Instruction limit % 3.41/1.02 % (3617377)Termination phase: Saturation % 3.41/1.02 % (3617377)Time elapsed: 0.052 s % 3.41/1.02 % (3617377)Peak memory usage: 12 MB % 3.41/1.02 % (3617377)Instructions burned: 134 (million) % 3.41/1.02 % (3617390)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.41/1.02 % (3617390)Terminated due to inappropriate strategy. % 3.41/1.02 % (3617390)------------------------------ % 3.41/1.02 % (3617390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.41/1.02 % (3617390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.41/1.02 % (3617390)CaDiCaL version: 2.1.3 % 3.41/1.02 % (3617390)Termination reason: Inappropriate % 3.41/1.02 % (3617390)Time elapsed: 0.035 s % 3.41/1.02 % (3617390)Peak memory usage: 11 MB % 3.41/1.02 % (3617390)Instructions burned: 89 (million) % 3.41/1.02 % (3617390)------------------------------ % 3.41/1.02 % (3617390)------------------------------ % 3.41/1.02 % (3617408)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2360227373:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 3.41/1.02 % (3617412)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=46672925: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) % 3.41/1.02 % (3617408)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.41/1.02 % (3617408)Terminated due to inappropriate strategy. % 3.41/1.02 % (3617408)------------------------------ % 3.41/1.02 % (3617408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.41/1.02 % (3617408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.41/1.02 % (3617408)CaDiCaL version: 2.1.3 % 3.41/1.02 % (3617408)Termination reason: Inappropriate % 3.41/1.02 % (3617408)Time elapsed: 0.034 s % 19.43/3.12 % (3617408)Peak memory usage: 10 MB % 19.43/3.12 % (3617408)Instructions burned: 89 (million) % 19.43/3.12 % (3617408)------------------------------ % 19.43/3.12 % (3617408)------------------------------ % 19.43/3.12 % (3617430)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1023036350:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 19.43/3.12 % (3617384)Instruction limit reached! % 19.43/3.12 % (3617384)------------------------------ % 19.43/3.12 % (3617384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.43/3.12 % (3617384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.12 % (3617384)CaDiCaL version: 2.1.3 % 19.43/3.12 % (3617384)Termination reason: Instruction limit % 19.43/3.12 % (3617384)Termination phase: Saturation % 19.43/3.12 % (3617384)Time elapsed: 0.186 s % 19.43/3.12 % (3617384)Peak memory usage: 13 MB % 19.43/3.12 % (3617384)Instructions burned: 479 (million) % 19.43/3.12 % (3617463)fmb+10_1_sil=64000:random_seed=1301752522:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 19.43/3.12 % (3617463)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.43/3.12 % (3617463)Terminated due to inappropriate strategy. % 19.43/3.12 % (3617463)------------------------------ % 19.43/3.12 % (3617463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.43/3.12 % (3617463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.12 % (3617463)CaDiCaL version: 2.1.3 % 19.43/3.12 % (3617463)Termination reason: Inappropriate % 19.43/3.12 % (3617463)Time elapsed: 0.049 s % 19.43/3.12 % (3617463)Peak memory usage: 11 MB % 19.43/3.12 % (3617463)Instructions burned: 118 (million) % 19.43/3.12 % (3617463)------------------------------ % 19.43/3.12 % (3617463)------------------------------ % 19.43/3.12 % (3617378)Instruction limit reached! % 19.43/3.12 % (3617378)------------------------------ % 19.43/3.12 % (3617378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.43/3.12 % (3617378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.12 % (3617378)CaDiCaL version: 2.1.3 % 19.43/3.12 % (3617378)Termination reason: Instruction limit % 19.43/3.12 % (3617378)Termination phase: Saturation % 19.43/3.12 % (3617378)Time elapsed: 0.275 s % 19.43/3.12 % (3617378)Peak memory usage: 15 MB % 19.43/3.12 % (3617378)Instructions burned: 686 (million) % 19.43/3.12 % (3617475)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2621520198:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 19.43/3.12 % (3617401)Instruction limit reached! % 19.43/3.12 % (3617401)------------------------------ % 19.43/3.12 % (3617401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.43/3.12 % (3617401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.12 % (3617401)CaDiCaL version: 2.1.3 % 19.43/3.12 % (3617401)Termination reason: Instruction limit % 19.43/3.12 % (3617401)Termination phase: Saturation % 19.43/3.12 % (3617401)Time elapsed: 0.251 s % 19.43/3.12 % (3617401)Peak memory usage: 17 MB % 19.43/3.12 % (3617401)Instructions burned: 1181 (million) % 19.43/3.12 % (3617479)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2809945550:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 19.43/3.12 % (3617488)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1876205270:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 19.43/3.12 % (3617475)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.43/3.12 % (3617475)Terminated due to inappropriate strategy. % 19.43/3.12 % (3617475)------------------------------ % 19.43/3.12 % (3617475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.43/3.12 % (3617475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.12 % (3617475)CaDiCaL version: 2.1.3 % 19.43/3.12 % (3617475)Termination reason: Inappropriate % 19.43/3.12 % (3617475)Time elapsed: 0.046 s % 19.43/3.12 % (3617475)Peak memory usage: 10 MB % 19.43/3.12 % (3617475)Instructions burned: 118 (million) % 19.43/3.12 % (3617475)------------------------------ % 19.43/3.12 % (3617475)------------------------------ % 19.43/3.12 % (3617479)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.43/3.12 % (3617479)Terminated due to inappropriate strategy. % 19.43/3.12 % (3617479)------------------------------ % 19.43/3.12 % (3617479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.43/3.12 % (3617479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.57/4.12 % (3617479)CaDiCaL version: 2.1.3 % 26.57/4.12 % (3617479)Termination reason: Inappropriate % 26.57/4.12 % (3617479)Time elapsed: 0.046 s % 26.57/4.12 % (3617479)Peak memory usage: 10 MB % 26.57/4.12 % (3617479)Instructions burned: 118 (million) % 26.57/4.12 % (3617479)------------------------------ % 26.57/4.12 % (3617479)------------------------------ % 26.57/4.12 % (3617500)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3367313907:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 26.57/4.12 % (3617503)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3276942163:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 26.57/4.12 % (3617412)Instruction limit reached! % 26.57/4.12 % (3617412)------------------------------ % 26.57/4.12 % (3617412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.57/4.12 % (3617412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.57/4.12 % (3617412)CaDiCaL version: 2.1.3 % 26.57/4.12 % (3617412)Termination reason: Instruction limit % 26.57/4.12 % (3617412)Termination phase: Saturation % 26.57/4.12 % (3617412)Time elapsed: 0.294 s % 26.57/4.12 % (3617412)Peak memory usage: 16 MB % 26.57/4.12 % (3617412)Instructions burned: 694 (million) % 26.57/4.12 % (3617517)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3164947603:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 26.57/4.12 % (3617503)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.57/4.12 % (3617503)Terminated due to inappropriate strategy. % 26.57/4.12 % (3617503)------------------------------ % 26.57/4.12 % (3617503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.57/4.12 % (3617503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.57/4.12 % (3617503)CaDiCaL version: 2.1.3 % 26.57/4.12 % (3617503)Termination reason: Inappropriate % 26.57/4.12 % (3617503)Time elapsed: 0.045 s % 26.57/4.12 % (3617503)Peak memory usage: 10 MB % 26.57/4.12 % (3617503)Instructions burned: 118 (million) % 26.57/4.12 % (3617503)------------------------------ % 26.57/4.12 % (3617503)------------------------------ % 26.57/4.12 % (3617528)ott-2_1_sil=16000:newcnf=on:random_seed=2776892867:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 26.57/4.12 % (3617517)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.57/4.12 % (3617517)Terminated due to inappropriate strategy. % 26.57/4.12 % (3617517)------------------------------ % 26.57/4.12 % (3617517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.57/4.12 % (3617517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.57/4.12 % (3617517)CaDiCaL version: 2.1.3 % 26.57/4.12 % (3617517)Termination reason: Inappropriate % 26.57/4.12 % (3617517)Time elapsed: 0.047 s % 26.57/4.12 % (3617517)Peak memory usage: 10 MB % 26.57/4.12 % (3617517)Instructions burned: 118 (million) % 26.57/4.12 % (3617517)------------------------------ % 26.57/4.12 % (3617517)------------------------------ % 26.57/4.12 % (3617530)ott+10_1_sil=32000:tgt=ground:random_seed=2754909791:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 26.57/4.12 % (3617430)Instruction limit reached! % 26.57/4.12 % (3617430)------------------------------ % 26.57/4.12 % (3617430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.57/4.13 % (3617430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.57/4.13 % (3617430)CaDiCaL version: 2.1.3 % 26.57/4.13 % (3617430)Termination reason: Instruction limit % 26.57/4.13 % (3617430)Termination phase: Saturation % 26.57/4.13 % (3617430)Time elapsed: 0.363 s % 26.57/4.13 % (3617430)Peak memory usage: 13 MB % 26.57/4.13 % (3617430)Instructions burned: 881 (million) % 26.57/4.13 % (3617532)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=979527341:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 26.57/4.13 % (3617532)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.57/4.13 % (3617532)Terminated due to inappropriate strategy. % 26.57/4.13 % (3617532)------------------------------ % 26.57/4.13 % (3617532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.57/4.13 % (3617532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.57/4.13 % (3617532)CaDiCaL version: 2.1.3 % 26.57/4.13 % (3617532)Termination reason: Inappropriate % 26.57/4.13 % (3617532)Time elapsed: 0.071 s % 26.57/4.13 % (3617532)Peak memory usage: 10 MB % 124.93/17.99 % (3617532)Instructions burned: 118 (million) % 124.93/17.99 % (3617532)------------------------------ % 124.93/17.99 % (3617532)------------------------------ % 124.93/17.99 % (3617534)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2722924075:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 124.93/17.99 % (3617528)Instruction limit reached! % 124.93/17.99 % (3617528)------------------------------ % 124.93/17.99 % (3617528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.93/17.99 % (3617528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.93/17.99 % (3617528)CaDiCaL version: 2.1.3 % 124.93/17.99 % (3617528)Termination reason: Instruction limit % 124.93/17.99 % (3617528)Termination phase: Saturation % 124.93/17.99 % (3617528)Time elapsed: 0.365 s % 124.93/17.99 % (3617528)Peak memory usage: 18 MB % 124.93/17.99 % (3617528)Instructions burned: 871 (million) % 124.93/17.99 % (3617537)dis+21_1_sil=32000:sas=cadical:random_seed=2654654725:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 124.93/17.99 % (3617500)Instruction limit reached! % 124.93/17.99 % (3617500)------------------------------ % 124.93/17.99 % (3617500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.93/17.99 % (3617500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.93/17.99 % (3617500)CaDiCaL version: 2.1.3 % 124.93/17.99 % (3617500)Termination reason: Instruction limit % 124.93/17.99 % (3617500)Termination phase: Saturation % 124.93/17.99 % (3617500)Time elapsed: 0.662 s % 124.93/17.99 % (3617500)Peak memory usage: 15 MB % 124.93/17.99 % (3617500)Instructions burned: 1472 (million) % 124.93/17.99 % (3617554)ott+11_1_sil=16000:gs=on:random_seed=2810082805:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 124.93/17.99 % (3617488)Instruction limit reached! % 124.93/17.99 % (3617488)------------------------------ % 124.93/17.99 % (3617488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.93/17.99 % (3617488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.93/17.99 % (3617488)CaDiCaL version: 2.1.3 % 124.93/17.99 % (3617488)Termination reason: Instruction limit % 124.93/17.99 % (3617488)Termination phase: Saturation % 124.93/17.99 % (3617488)Time elapsed: 1.743 s % 124.93/17.99 % (3617488)Peak memory usage: 15 MB % 124.93/17.99 % (3617488)Instructions burned: 5133 (million) % 124.93/17.99 % (3617613)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2878814091:fmbsr=1.6:i=67534_2977 on theBenchmark for (2977ds/67534Mi) % 124.93/17.99 % (3617613)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 124.93/17.99 % (3617613)Terminated due to inappropriate strategy. % 124.93/17.99 % (3617613)------------------------------ % 124.93/17.99 % (3617613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.93/17.99 % (3617613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.93/17.99 % (3617613)CaDiCaL version: 2.1.3 % 124.93/17.99 % (3617613)Termination reason: Inappropriate % 124.93/17.99 % (3617613)Time elapsed: 0.024 s % 124.93/17.99 % (3617613)Peak memory usage: 11 MB % 124.93/17.99 % (3617613)Instructions burned: 118 (million) % 124.93/17.99 % (3617613)------------------------------ % 124.93/17.99 % (3617613)------------------------------ % 124.93/17.99 % (3617617)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=304086483:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2977 on theBenchmark for (2977ds/4591Mi) % 124.93/17.99 % (3617554)Instruction limit reached! % 124.93/17.99 % (3617554)------------------------------ % 124.93/17.99 % (3617554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.93/17.99 % (3617554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.93/17.99 % (3617554)CaDiCaL version: 2.1.3 % 124.93/17.99 % (3617554)Termination reason: Instruction limit % 124.93/17.99 % (3617554)Termination phase: Saturation % 124.93/17.99 % (3617554)Time elapsed: 1.455 s % 124.93/17.99 % (3617554)Peak memory usage: 16 MB % 124.93/17.99 % (3617554)Instructions burned: 2251 (million) % 124.93/17.99 % (3617633)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3471343787:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 124.93/17.99 % (3617534)Instruction limit reached! % 124.93/17.99 % (3617534)------------------------------ % 124.93/17.99 % (3617534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.93/17.99 % (3617534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.93/17.99 % (3617534)CaDiCaL version: 2.1.3 % 145.51/20.83 % (3617534)Termination reason: Instruction limit % 145.51/20.83 % (3617534)Termination phase: Saturation % 145.51/20.83 % (3617534)Time elapsed: 2.073 s % 145.51/20.83 % (3617534)Peak memory usage: 15 MB % 145.51/20.83 % (3617534)Instructions burned: 3514 (million) % 145.51/20.83 % (3617637)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=308487420:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 145.51/20.83 % (3617537)Instruction limit reached! % 145.51/20.83 % (3617537)------------------------------ % 145.51/20.83 % (3617537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.51/20.83 % (3617537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.51/20.83 % (3617537)CaDiCaL version: 2.1.3 % 145.51/20.83 % (3617537)Termination reason: Instruction limit % 145.51/20.83 % (3617537)Termination phase: Saturation % 145.51/20.83 % (3617537)Time elapsed: 2.475 s % 145.51/20.83 % (3617537)Peak memory usage: 15 MB % 145.51/20.83 % (3617537)Instructions burned: 3773 (million) % 145.51/20.83 % (3617662)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1439711249:i=5497:nm=2_2965 on theBenchmark for (2965ds/5497Mi) % 145.51/20.83 % (3617662)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.51/20.83 % (3617662)Terminated due to inappropriate strategy. % 145.51/20.83 % (3617662)------------------------------ % 145.51/20.83 % (3617662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.51/20.83 % (3617662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.51/20.83 % (3617662)CaDiCaL version: 2.1.3 % 145.51/20.83 % (3617662)Termination reason: Inappropriate % 145.51/20.83 % (3617662)Time elapsed: 0.077 s % 145.51/20.83 % (3617662)Peak memory usage: 11 MB % 145.51/20.83 % (3617662)Instructions burned: 118 (million) % 145.51/20.83 % (3617662)------------------------------ % 145.51/20.83 % (3617662)------------------------------ % 145.51/20.83 % (3617668)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2957313228:fmbsr=2:i=46332_2964 on theBenchmark for (2964ds/46332Mi) % 145.51/20.83 % (3617530)Instruction limit reached! % 145.51/20.83 % (3617530)------------------------------ % 145.51/20.83 % (3617530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.51/20.83 % (3617530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.51/20.83 % (3617530)CaDiCaL version: 2.1.3 % 145.51/20.83 % (3617530)Termination reason: Instruction limit % 145.51/20.83 % (3617530)Termination phase: Saturation % 145.51/20.83 % (3617530)Time elapsed: 3.024 s % 145.51/20.83 % (3617530)Peak memory usage: 15 MB % 145.51/20.83 % (3617530)Instructions burned: 5115 (million) % 145.51/20.83 % (3617672)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4045204076:i=14071_2963 on theBenchmark for (2963ds/14071Mi) % 145.51/20.83 % (3617668)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.51/20.83 % (3617668)Terminated due to inappropriate strategy. % 145.51/20.83 % (3617668)------------------------------ % 145.51/20.83 % (3617668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.51/20.83 % (3617668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.51/20.83 % (3617668)CaDiCaL version: 2.1.3 % 145.51/20.83 % (3617668)Termination reason: Inappropriate % 145.51/20.83 % (3617668)Time elapsed: 0.091 s % 145.51/20.83 % (3617668)Peak memory usage: 10 MB % 145.51/20.83 % (3617668)Instructions burned: 118 (million) % 145.51/20.83 % (3617668)------------------------------ % 145.51/20.83 % (3617668)------------------------------ % 145.51/20.83 % (3617678)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1165110303:i=22565:add=on:rawr=on_2962 on theBenchmark for (2962ds/22565Mi) % 145.51/20.83 % (3617672)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.51/20.83 % (3617672)Terminated due to inappropriate strategy. % 145.51/20.83 % (3617672)------------------------------ % 145.51/20.83 % (3617672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.51/20.83 % (3617672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.51/20.83 % (3617672)CaDiCaL version: 2.1.3 % 145.51/20.83 % (3617672)Termination reason: Inappropriate % 145.51/20.83 % (3617672)Time elapsed: 0.122 s % 145.51/20.83 % (3617672)Peak memory usage: 11 MB % 145.51/20.83 % (3617672)Instructions burned: 118 (million) % 145.51/20.83 % (3617672)------------------------------ % 145.51/20.83 % (3617672)------------------------------ % 145.51/20.83 % (3617681)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=462167883:i=8173:av=off_2961 on theBenchmark for (2961ds/8173Mi) % 149.02/21.37 % (3617617)Instruction limit reached! % 149.02/21.37 % (3617617)------------------------------ % 149.02/21.37 % (3617617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.02/21.37 % (3617617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.02/21.37 % (3617617)CaDiCaL version: 2.1.3 % 149.02/21.37 % (3617617)Termination reason: Instruction limit % 149.02/21.37 % (3617617)Termination phase: Saturation % 149.02/21.37 % (3617617)Time elapsed: 2.303 s % 149.02/21.37 % (3617617)Peak memory usage: 43 MB % 149.02/21.37 % (3617617)Instructions burned: 4591 (million) % 149.02/21.37 % (3617704)dis+10_16:1_sil=16000:random_seed=2869661167:i=9155:fsr=off_2953 on theBenchmark for (2953ds/9155Mi) % 149.02/21.37 % (3617637)Instruction limit reached! % 149.02/21.37 % (3617637)------------------------------ % 149.02/21.37 % (3617637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.02/21.37 % (3617637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.02/21.37 % (3617637)CaDiCaL version: 2.1.3 % 149.02/21.37 % (3617637)Termination reason: Instruction limit % 149.02/21.37 % (3617637)Termination phase: Saturation % 149.02/21.37 % (3617637)Time elapsed: 3.511 s % 149.02/21.37 % (3617637)Peak memory usage: 17 MB % 149.02/21.37 % (3617637)Instructions burned: 5212 (million) % 149.02/21.37 % (3617742)ott-3_8_sil=64000:random_seed=43020904:i=20139:bs=on_2935 on theBenchmark for (2935ds/20139Mi) % 149.02/21.37 % (3617704)Instruction limit reached! % 149.02/21.37 % (3617704)------------------------------ % 149.02/21.37 % (3617704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.02/21.37 % (3617704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.02/21.37 % (3617704)CaDiCaL version: 2.1.3 % 149.02/21.37 % (3617704)Termination reason: Instruction limit % 149.02/21.37 % (3617704)Termination phase: Saturation % 149.02/21.37 % (3617704)Time elapsed: 3.030 s % 149.02/21.37 % (3617704)Peak memory usage: 16 MB % 149.02/21.37 % (3617704)Instructions burned: 9156 (million) % 149.02/21.37 % (3617766)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3100067898:fmbsr=2:i=32576_2922 on theBenchmark for (2922ds/32576Mi) % 149.02/21.37 % (3617766)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.02/21.37 % (3617766)Terminated due to inappropriate strategy. % 149.02/21.37 % (3617766)------------------------------ % 149.02/21.37 % (3617766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.02/21.37 % (3617766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.02/21.37 % (3617766)CaDiCaL version: 2.1.3 % 149.02/21.37 % (3617766)Termination reason: Inappropriate % 149.02/21.37 % (3617766)Time elapsed: 0.049 s % 149.02/21.37 % (3617766)Peak memory usage: 10 MB % 149.02/21.37 % (3617766)Instructions burned: 118 (million) % 149.02/21.37 % (3617766)------------------------------ % 149.02/21.37 % (3617766)------------------------------ % 149.02/21.37 % (3617768)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1239094512:i=11404_2922 on theBenchmark for (2922ds/11404Mi) % 149.02/21.37 % (3617681)Instruction limit reached! % 149.02/21.37 % (3617681)------------------------------ % 149.02/21.37 % (3617681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.02/21.37 % (3617681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.02/21.37 % (3617681)CaDiCaL version: 2.1.3 % 149.02/21.37 % (3617681)Termination reason: Instruction limit % 149.02/21.37 % (3617681)Termination phase: Saturation % 149.02/21.37 % (3617681)Time elapsed: 5.488 s % 149.02/21.37 % (3617681)Peak memory usage: 16 MB % 149.02/21.37 % (3617681)Instructions burned: 8174 (million) % 149.02/21.37 % (3617783)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2679963252:i=14134_2906 on theBenchmark for (2906ds/14134Mi) % 149.02/21.37 % (3617768)Instruction limit reached! % 149.02/21.37 % (3617768)------------------------------ % 149.02/21.37 % (3617768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.02/21.37 % (3617768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.02/21.37 % (3617768)CaDiCaL version: 2.1.3 % 149.02/21.37 % (3617768)Termination reason: Instruction limit % 149.02/21.37 % (3617768)Termination phase: Saturation % 149.02/21.37 % (3617768)Time elapsed: 4.019 s % 149.02/21.37 % (3617768)Peak memory usage: 16 MB % 149.02/21.37 % (3617768)Instructions burned: 11405 (million) % 149.02/21.37 % (3617802)dis+33_16_sil=32000:sac=on:random_seed=3575046274:i=15851:nm=0_2881 on theBenchmark for (2881ds/15851Mi) % 149.02/21.37 % (3617802)Instruction limit reached! % 149.02/21.37 % (3617802)------------------------------ % 180.25/25.76 % (3617802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.25/25.76 % (3617802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.25/25.76 % (3617802)CaDiCaL version: 2.1.3 % 180.25/25.76 % (3617802)Termination reason: Instruction limit % 180.25/25.76 % (3617802)Termination phase: Saturation % 180.25/25.76 % (3617802)Time elapsed: 5.907 s % 180.25/25.76 % (3617802)Peak memory usage: 20 MB % 180.25/25.76 % (3617802)Instructions burned: 15852 (million) % 180.25/25.76 % (3617825)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1737868706:avsq=on:i=17627:add=on:amm=off_2822 on theBenchmark for (2822ds/17627Mi) % 180.25/25.76 % (3617678)Instruction limit reached! % 180.25/25.76 % (3617678)------------------------------ % 180.25/25.76 % (3617678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.25/25.76 % (3617678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.25/25.76 % (3617678)CaDiCaL version: 2.1.3 % 180.25/25.76 % (3617678)Termination reason: Instruction limit % 180.25/25.76 % (3617678)Termination phase: Saturation % 180.25/25.76 % (3617678)Time elapsed: 15.072 s % 180.25/25.76 % (3617678)Peak memory usage: 17 MB % 180.25/25.76 % (3617678)Instructions burned: 22566 (million) % 180.25/25.76 % (3617831)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2890045815:s2a=on:i=53295_2811 on theBenchmark for (2811ds/53295Mi) % 180.25/25.76 % (3617783)Instruction limit reached! % 180.25/25.76 % (3617783)------------------------------ % 180.25/25.76 % (3617783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.25/25.76 % (3617783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.25/25.76 % (3617783)CaDiCaL version: 2.1.3 % 180.25/25.76 % (3617783)Termination reason: Instruction limit % 180.25/25.76 % (3617783)Termination phase: Saturation % 180.25/25.76 % (3617783)Time elapsed: 9.942 s % 180.25/25.76 % (3617783)Peak memory usage: 16 MB % 180.25/25.76 % (3617783)Instructions burned: 14135 (million) % 180.25/25.76 % (3617838)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1787488627:i=26857:ins=20_2806 on theBenchmark for (2806ds/26857Mi) % 180.25/25.76 % (3617838)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.25/25.76 % (3617838)Terminated due to inappropriate strategy. % 180.25/25.76 % (3617838)------------------------------ % 180.25/25.76 % (3617838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.25/25.76 % (3617838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.25/25.76 % (3617838)CaDiCaL version: 2.1.3 % 180.25/25.76 % (3617838)Termination reason: Inappropriate % 180.25/25.76 % (3617838)Time elapsed: 0.097 s % 180.25/25.76 % (3617838)Peak memory usage: 10 MB % 180.25/25.76 % (3617838)Instructions burned: 118 (million) % 180.25/25.76 % (3617838)------------------------------ % 180.25/25.76 % (3617838)------------------------------ % 180.25/25.76 % (3617842)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1220888524:i=28120:bs=on:fsr=off_2805 on theBenchmark for (2805ds/28120Mi) % 180.25/25.76 % (3617742)Instruction limit reached! % 180.25/25.76 % (3617742)------------------------------ % 180.25/25.76 % (3617742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.25/25.76 % (3617742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.25/25.76 % (3617742)CaDiCaL version: 2.1.3 % 180.25/25.76 % (3617742)Termination reason: Instruction limit % 180.25/25.76 % (3617742)Termination phase: Saturation % 180.25/25.76 % (3617742)Time elapsed: 14.013 s % 180.25/25.76 % (3617742)Peak memory usage: 18 MB % 180.25/25.76 % (3617742)Instructions burned: 20140 (million) % 180.25/25.76 % (3617845)fmb+10_1_sil=256000:fmbss=7:random_seed=2436501434:fmbsr=1.6:i=182295_2795 on theBenchmark for (2795ds/182295Mi) % 180.25/25.76 % (3617845)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 180.25/25.76 % (3617845)Terminated due to inappropriate strategy. % 180.25/25.76 % (3617845)------------------------------ % 180.25/25.76 % (3617845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.25/25.76 % (3617845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.25/25.76 % (3617845)CaDiCaL version: 2.1.3 % 180.25/25.76 % (3617845)Termination reason: Inappropriate % 180.25/25.76 % (3617845)Time elapsed: 0.061 s % 180.25/25.76 % (3617845)Peak memory usage: 11 MB % 180.25/25.76 % (3617845)Instructions burned: 118 (million) % 180.25/25.76 % (3617845)------------------------------ % 180.25/25.76 % (3617845)------------------------------ % 180.25/25.76 % (3617847)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4054862910:i=44625:gsp=on_2794 on theBenchmark for (2794ds/44625Mi) % 190.59/27.17 % (3617847)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.59/27.17 % (3617847)Terminated due to inappropriate strategy. % 190.59/27.17 % (3617847)------------------------------ % 190.59/27.17 % (3617847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.59/27.17 % (3617847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.59/27.17 % (3617847)CaDiCaL version: 2.1.3 % 190.59/27.17 % (3617847)Termination reason: Inappropriate % 190.59/27.17 % (3617847)Time elapsed: 0.055 s % 190.59/27.17 % (3617847)Peak memory usage: 11 MB % 190.59/27.17 % (3617847)Instructions burned: 118 (million) % 190.59/27.17 % (3617847)------------------------------ % 190.59/27.17 % (3617847)------------------------------ % 190.59/27.17 % (3617849)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2163159999:i=160505_2793 on theBenchmark for (2793ds/160505Mi) % 190.59/27.17 % (3617849)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.59/27.17 % (3617849)Terminated due to inappropriate strategy. % 190.59/27.17 % (3617849)------------------------------ % 190.59/27.17 % (3617849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.59/27.17 % (3617849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.59/27.17 % (3617849)CaDiCaL version: 2.1.3 % 190.59/27.17 % (3617849)Termination reason: Inappropriate % 190.59/27.17 % (3617849)Time elapsed: 0.108 s % 190.59/27.17 % (3617849)Peak memory usage: 10 MB % 190.59/27.17 % (3617849)Instructions burned: 118 (million) % 190.59/27.17 % (3617849)------------------------------ % 190.59/27.17 % (3617849)------------------------------ % 190.59/27.17 % (3617851)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3359274658:fmbsr=1.3:i=225729_2792 on theBenchmark for (2792ds/225729Mi) % 190.59/27.17 % (3617851)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.59/27.17 % (3617851)Terminated due to inappropriate strategy. % 190.59/27.17 % (3617851)------------------------------ % 190.59/27.17 % (3617851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.59/27.17 % (3617851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.59/27.17 % (3617851)CaDiCaL version: 2.1.3 % 190.59/27.17 % (3617851)Termination reason: Inappropriate % 190.59/27.17 % (3617851)Time elapsed: 0.051 s % 190.59/27.17 % (3617851)Peak memory usage: 11 MB % 190.59/27.17 % (3617851)Instructions burned: 118 (million) % 190.59/27.17 % (3617851)------------------------------ % 190.59/27.17 % (3617851)------------------------------ % 190.59/27.17 % (3617853)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2105434165:fmbsr=2:i=185024:ins=7_2791 on theBenchmark for (2791ds/185024Mi) % 190.59/27.17 % (3617853)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.59/27.17 % (3617853)Terminated due to inappropriate strategy. % 190.59/27.17 % (3617853)------------------------------ % 190.59/27.17 % (3617853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.59/27.17 % (3617853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.59/27.17 % (3617853)CaDiCaL version: 2.1.3 % 190.59/27.17 % (3617853)Termination reason: Inappropriate % 190.59/27.17 % (3617853)Time elapsed: 0.106 s % 190.59/27.17 % (3617853)Peak memory usage: 11 MB % 190.59/27.17 % (3617853)Instructions burned: 118 (million) % 190.59/27.17 % (3617853)------------------------------ % 190.59/27.17 % (3617853)------------------------------ % 190.59/27.17 % (3617855)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3313852530:rtra=on_2790 on theBenchmark for (2790ds/0Mi) % 190.59/27.17 % (3617855)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.59/27.17 % (3617855)Terminated due to inappropriate strategy. % 190.59/27.17 % (3617855)------------------------------ % 190.59/27.17 % (3617855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.59/27.17 % (3617855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.59/27.17 % (3617855)CaDiCaL version: 2.1.3 % 190.59/27.17 % (3617855)Termination reason: Inappropriate % 190.59/27.17 % (3617855)Time elapsed: 0.072 s % 190.59/27.17 % (3617855)Peak memory usage: 11 MB % 190.59/27.17 % (3617855)Instructions burned: 118 (million) % 190.59/27.17 % (3617855)------------------------------ % 190.59/27.17 % (3617855)------------------------------ % 190.59/27.17 % (3617857)% WARNING: option uhcvi not known. % 190.59/27.17 % (3617857)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=492072975:i=271062:add=off:rtra=on:rawr=on_2789 on theBenchmark for (2789ds/271062Mi) % 206.65/29.45 % (3617633)Instruction limit reached! % 206.65/29.45 % (3617633)------------------------------ % 206.65/29.45 % (3617633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.65/29.45 % (3617633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.65/29.45 % (3617633)CaDiCaL version: 2.1.3 % 206.65/29.45 % (3617633)Termination reason: Instruction limit % 206.65/29.45 % (3617633)Termination phase: Saturation % 206.65/29.45 % (3617633)Time elapsed: 20.051 s % 206.65/29.45 % (3617633)Peak memory usage: 16 MB % 206.65/29.45 % (3617633)Instructions burned: 29340 (million) % 206.65/29.45 % (3617863)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=78760379:i=176048:add=on:rtra=on:rawr=on_2772 on theBenchmark for (2772ds/176048Mi) % 206.65/29.45 % (3617825)Instruction limit reached! % 206.65/29.45 % (3617825)------------------------------ % 206.65/29.45 % (3617825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.65/29.45 % (3617825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.65/29.45 % (3617825)CaDiCaL version: 2.1.3 % 206.65/29.45 % (3617825)Termination reason: Instruction limit % 206.65/29.45 % (3617825)Termination phase: Saturation % 206.65/29.45 % (3617825)Time elapsed: 7.181 s % 206.65/29.45 % (3617825)Peak memory usage: 91 MB % 206.65/29.45 % (3617825)Instructions burned: 17630 (million) % 206.65/29.45 % (3617867)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3421174116:i=206:fgj=on:rtra=on_2750 on theBenchmark for (2750ds/206Mi) % 206.65/29.45 % (3617867)Instruction limit reached! % 206.65/29.45 % (3617867)------------------------------ % 206.65/29.45 % (3617867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.65/29.45 % (3617867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.65/29.45 % (3617867)CaDiCaL version: 2.1.3 % 206.65/29.45 % (3617867)Termination reason: Instruction limit % 206.65/29.45 % (3617867)Termination phase: Saturation % 206.65/29.45 % (3617867)Time elapsed: 0.091 s % 206.65/29.45 % (3617867)Peak memory usage: 13 MB % 206.65/29.45 % (3617867)Instructions burned: 207 (million) % 206.65/29.45 % (3617869)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3031668962:i=232:rtra=on_2749 on theBenchmark for (2749ds/232Mi) % 206.65/29.45 % (3617869)Instruction limit reached! % 206.65/29.45 % (3617869)------------------------------ % 206.65/29.45 % (3617869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.65/29.45 % (3617869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.65/29.45 % (3617869)CaDiCaL version: 2.1.3 % 206.65/29.45 % (3617869)Termination reason: Instruction limit % 206.65/29.45 % (3617869)Termination phase: Saturation % 206.65/29.45 % (3617869)Time elapsed: 0.097 s % 206.65/29.45 % (3617869)Peak memory usage: 13 MB % 206.65/29.45 % (3617869)Instructions burned: 232 (million) % 206.65/29.45 % (3617871)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3140191874:i=262:rtra=on_2748 on theBenchmark for (2748ds/262Mi) % 206.65/29.45 % (3617871)Instruction limit reached! % 206.65/29.45 % (3617871)------------------------------ % 206.65/29.45 % (3617871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.65/29.45 % (3617871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.65/29.45 % (3617871)CaDiCaL version: 2.1.3 % 206.65/29.45 % (3617871)Termination reason: Instruction limit % 206.65/29.45 % (3617871)Termination phase: Saturation % 206.65/29.45 % (3617871)Time elapsed: 0.105 s % 206.65/29.45 % (3617871)Peak memory usage: 13 MB % 206.65/29.45 % (3617871)Instructions burned: 263 (million) % 206.65/29.45 % (3617873)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1569108942:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2746 on theBenchmark for (2746ds/318Mi) % 206.65/29.45 % (3617873)Instruction limit reached! % 206.65/29.45 % (3617873)------------------------------ % 206.65/29.45 % (3617873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.65/29.45 % (3617873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.65/29.45 % (3617873)CaDiCaL version: 2.1.3 % 206.65/29.45 % (3617873)Termination reason: Instruction limit % 206.65/29.45 % (3617873)Termination phase: Saturation % 206.65/29.45 % (3617873)Time elapsed: 0.131 s % 206.65/29.45 % (3617873)Peak memory usage: 14 MB % 206.65/29.45 % (3617873)Instructions burned: 320 (million) % 206.65/29.45 % (3617876)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1270312426:i=1428:nm=2:rtra=on_2745 on theBenchmark for (2745ds/1428Mi) % 244.34/34.78 % (3617876)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 244.34/34.78 % (3617876)Terminated due to inappropriate strategy. % 244.34/34.78 % (3617876)------------------------------ % 244.34/34.78 % (3617876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.34/34.78 % (3617876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.34/34.78 % (3617876)CaDiCaL version: 2.1.3 % 244.34/34.78 % (3617876)Termination reason: Inappropriate % 244.34/34.78 % (3617876)Time elapsed: 0.051 s % 244.34/34.78 % (3617876)Peak memory usage: 11 MB % 244.34/34.78 % (3617876)Instructions burned: 118 (million) % 244.34/34.78 % (3617876)------------------------------ % 244.34/34.78 % (3617876)------------------------------ % 244.34/34.78 % (3617878)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2390097348:i=262:bd=preordered:rtra=on:fsd=on_2744 on theBenchmark for (2744ds/262Mi) % 244.34/34.78 % (3617878)Instruction limit reached! % 244.34/34.78 % (3617878)------------------------------ % 244.34/34.78 % (3617878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.34/34.78 % (3617878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.34/34.78 % (3617878)CaDiCaL version: 2.1.3 % 244.34/34.78 % (3617878)Termination reason: Instruction limit % 244.34/34.78 % (3617878)Termination phase: Saturation % 244.34/34.78 % (3617878)Time elapsed: 0.108 s % 244.34/34.78 % (3617878)Peak memory usage: 13 MB % 244.34/34.78 % (3617878)Instructions burned: 264 (million) % 244.34/34.78 % (3617881)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=501067847:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2743 on theBenchmark for (2743ds/1368Mi) % 244.34/34.78 % (3617881)Instruction limit reached! % 244.34/34.78 % (3617881)------------------------------ % 244.34/34.78 % (3617881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.34/34.78 % (3617881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.34/34.78 % (3617881)CaDiCaL version: 2.1.3 % 244.34/34.78 % (3617881)Termination reason: Instruction limit % 244.34/34.78 % (3617881)Termination phase: Saturation % 244.34/34.78 % (3617881)Time elapsed: 0.556 s % 244.34/34.78 % (3617881)Peak memory usage: 16 MB % 244.34/34.78 % (3617881)Instructions burned: 1370 (million) % 244.34/34.78 % (3617884)ott-21_1_sil=16000:si=on:fs=off:random_seed=2797744545:i=360:av=off:fsr=off:rtra=on_2737 on theBenchmark for (2737ds/360Mi) % 244.34/34.78 % (3617884)Instruction limit reached! % 244.34/34.78 % (3617884)------------------------------ % 244.34/34.78 % (3617884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.34/34.78 % (3617884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.34/34.78 % (3617884)CaDiCaL version: 2.1.3 % 244.34/34.78 % (3617884)Termination reason: Instruction limit % 244.34/34.78 % (3617884)Termination phase: Saturation % 244.34/34.78 % (3617884)Time elapsed: 0.180 s % 244.34/34.78 % (3617884)Peak memory usage: 12 MB % 244.34/34.78 % (3617884)Instructions burned: 361 (million) % 244.34/34.78 % (3617887)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2205028777:i=954:bd=all:rtra=on_2735 on theBenchmark for (2735ds/954Mi) % 244.34/34.78 % (3617887)Instruction limit reached! % 244.34/34.78 % (3617887)------------------------------ % 244.34/34.78 % (3617887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.34/34.78 % (3617887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.34/34.78 % (3617887)CaDiCaL version: 2.1.3 % 244.34/34.78 % (3617887)Termination reason: Instruction limit % 244.34/34.78 % (3617887)Termination phase: Saturation % 244.34/34.78 % (3617887)Time elapsed: 0.365 s % 244.34/34.78 % (3617887)Peak memory usage: 14 MB % 244.34/34.78 % (3617887)Instructions burned: 956 (million) % 244.34/34.78 % (3617889)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2475774343:fmbsr=1.3:i=1730:ins=25:rtra=on_2731 on theBenchmark for (2731ds/1730Mi) % 244.34/34.78 % (3617889)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 244.34/34.78 % (3617889)Terminated due to inappropriate strategy. % 244.34/34.78 % (3617889)------------------------------ % 244.34/34.78 % (3617889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 244.34/34.78 % (3617889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.34/34.78 % (3617889)CaDiCaL version: 2.1.3 % 295.62/42.04 % (3617889)Termination reason: Inappropriate % 295.62/42.04 % (3617889)Time elapsed: 0.041 s % 295.62/42.04 % (3617889)Peak memory usage: 11 MB % 295.62/42.04 % (3617889)Instructions burned: 90 (million) % 295.62/42.04 % (3617889)------------------------------ % 295.62/42.04 % (3617889)------------------------------ % 295.62/42.04 % (3617891)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2121895292:i=2358:rtra=on_2730 on theBenchmark for (2730ds/2358Mi) % 295.62/42.04 % (3617891)Instruction limit reached! % 295.62/42.04 % (3617891)------------------------------ % 295.62/42.04 % (3617891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.62/42.04 % (3617891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.62/42.04 % (3617891)CaDiCaL version: 2.1.3 % 295.62/42.04 % (3617891)Termination reason: Instruction limit % 295.62/42.04 % (3617891)Termination phase: Saturation % 295.62/42.04 % (3617891)Time elapsed: 0.881 s % 295.62/42.04 % (3617891)Peak memory usage: 13 MB % 295.62/42.04 % (3617891)Instructions burned: 2360 (million) % 295.62/42.04 % (3617893)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2310232310:i=1778:ins=1:rtra=on_2721 on theBenchmark for (2721ds/1778Mi) % 295.62/42.04 % (3617893)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 295.62/42.04 % (3617893)Terminated due to inappropriate strategy. % 295.62/42.04 % (3617893)------------------------------ % 295.62/42.04 % (3617893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.62/42.04 % (3617893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.62/42.04 % (3617893)CaDiCaL version: 2.1.3 % 295.62/42.04 % (3617893)Termination reason: Inappropriate % 295.62/42.04 % (3617893)Time elapsed: 0.038 s % 295.62/42.04 % (3617893)Peak memory usage: 10 MB % 295.62/42.04 % (3617893)Instructions burned: 90 (million) % 295.62/42.04 % (3617893)------------------------------ % 295.62/42.04 % (3617893)------------------------------ % 295.62/42.04 % (3617895)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=3151588285:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2721 on theBenchmark for (2721ds/1384Mi) % 295.62/42.04 % (3617895)Instruction limit reached! % 295.62/42.04 % (3617895)------------------------------ % 295.62/42.04 % (3617895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.62/42.04 % (3617895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.62/42.04 % (3617895)CaDiCaL version: 2.1.3 % 295.62/42.04 % (3617895)Termination reason: Instruction limit % 295.62/42.04 % (3617895)Termination phase: Saturation % 295.62/42.04 % (3617895)Time elapsed: 0.504 s % 295.62/42.04 % (3617895)Peak memory usage: 17 MB % 295.62/42.04 % (3617895)Instructions burned: 1385 (million) % 295.62/42.04 % (3617897)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3402656197:i=1758:kws=inv_precedence:fsr=off:rtra=on_2715 on theBenchmark for (2715ds/1758Mi) % 295.62/42.04 % (3617897)Instruction limit reached! % 295.62/42.04 % (3617897)------------------------------ % 295.62/42.04 % (3617897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.62/42.04 % (3617897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.62/42.04 % (3617897)CaDiCaL version: 2.1.3 % 295.62/42.04 % (3617897)Termination reason: Instruction limit % 295.62/42.04 % (3617897)Termination phase: Saturation % 295.62/42.04 % (3617897)Time elapsed: 0.674 s % 295.62/42.04 % (3617897)Peak memory usage: 15 MB % 295.62/42.04 % (3617897)Instructions burned: 1760 (million) % 295.62/42.04 % (3617899)fmb+10_1_sil=64000:si=on:random_seed=4122487827:i=44122:nm=2:rtra=on:gsp=on_2708 on theBenchmark for (2708ds/44122Mi) % 295.62/42.04 % (3617899)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 295.62/42.04 % (3617899)Terminated due to inappropriate strategy. % 295.62/42.04 % (3617899)------------------------------ % 295.62/42.04 % (3617899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.62/42.04 % (3617899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.62/42.04 % (3617899)CaDiCaL version: 2.1.3 % 295.62/42.04 % (3617899)Termination reason: Inappropriate % 295.62/42.04 % (3617899)Time elapsed: 0.052 s % 295.62/42.04 % (3617899)Peak memory usage: 11 MB % 295.62/42.04 % (3617899)Instructions burned: 118 (million) % 295.62/42.04 % (3617899)------------------------------ % 295.62/42.04 % (3617899)------------------------------ % 295.62/42.04 % (3617901)fmb+10_1_sil=16000:sas=cadical:si=on:fmbTerminated % 300.03/42.64 % Vampire exiting %------------------------------------------------------------------------------