%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC429_1 : TPTP v9.3.1. Bugfixed v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n010.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:06:00 PM UTC 2026 % Result : Timeout 293.22s 41.51s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC429_1 : TPTP v9.3.1. Bugfixed v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.19 % Computer : n010.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 09:37:17 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.22 Running first-order model finding % 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.59/0.84 % (1800858)Will run a generic schedule for satisfiability detection. % 3.59/0.84 % (1800880)dis+10_1_sil=32000:sp=arity:random_seed=1990390740:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.59/0.84 % (1800877)% WARNING: option uhcvi not known. % 3.59/0.84 % (1800877)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2460793872:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.59/0.84 % (1800876)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3218589522_2999 on theBenchmark for (2999ds/0Mi) % 3.59/0.84 % (1800878)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1244564581:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.59/0.84 % (1800882)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1152494575:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.59/0.84 % (1800881)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2546138615:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.59/0.84 % (1800883)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2336157447:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.59/0.84 % (1800876)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.59/0.84 % (1800876)Terminated due to inappropriate strategy. % 3.59/0.84 % (1800876)------------------------------ % 3.59/0.84 % (1800876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.59/0.84 % (1800876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.59/0.84 % (1800876)CaDiCaL version: 2.1.3 % 3.59/0.84 % (1800876)Termination reason: Inappropriate % 3.59/0.84 % (1800876)Time elapsed: 0.001 s % 3.59/0.84 % (1800876)Peak memory usage: 10 MB % 3.59/0.84 % (1800876)Instructions burned: 1 (million) % 3.59/0.84 % (1800876)------------------------------ % 3.59/0.84 % (1800876)------------------------------ % 3.59/0.84 % (1800900)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1605816285:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.59/0.84 % (1800900)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.59/0.84 % (1800900)Terminated due to inappropriate strategy. % 3.59/0.84 % (1800900)------------------------------ % 3.59/0.84 % (1800900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.59/0.84 % (1800900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.59/0.84 % (1800900)CaDiCaL version: 2.1.3 % 3.59/0.84 % (1800900)Termination reason: Inappropriate % 3.59/0.84 % (1800900)Time elapsed: 0.001 s % 3.59/0.84 % (1800900)Peak memory usage: 10 MB % 3.59/0.84 % (1800900)Instructions burned: 1 (million) % 3.59/0.84 % (1800900)------------------------------ % 3.59/0.84 % (1800900)------------------------------ % 3.59/0.84 % (1800880)Instruction limit reached! % 3.59/0.84 % (1800880)------------------------------ % 3.59/0.84 % (1800880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.59/0.84 % (1800880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.59/0.84 % (1800880)CaDiCaL version: 2.1.3 % 3.59/0.84 % (1800880)Termination reason: Instruction limit % 3.59/0.84 % (1800880)Termination phase: Saturation % 3.59/0.84 % (1800880)Time elapsed: 0.036 s % 3.59/0.84 % (1800880)Peak memory usage: 12 MB % 3.59/0.84 % (1800880)Instructions burned: 106 (million) % 3.59/0.84 % (1800916)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=247308736:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.59/0.84 % (1800912)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1945415281:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.59/0.84 % (1800881)Instruction limit reached! % 3.59/0.84 % (1800881)------------------------------ % 3.59/0.84 % (1800881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.59/0.84 % (1800881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.59/0.84 % (1800881)CaDiCaL version: 2.1.3 % 3.59/0.84 % (1800881)Termination reason: Instruction limit % 3.59/0.84 % (1800881)Termination phase: Saturation % 3.59/0.84 % (1800881)Time elapsed: 0.071 s % 3.59/0.84 % (1800881)Peak memory usage: 12 MB % 3.59/0.84 % (1800881)Instructions burned: 116 (million) % 3.59/0.84 % (1800882)Instruction limit reached! % 3.59/0.84 % (1800882)------------------------------ % 3.59/0.84 % (1800882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.31/1.16 % (1800882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.16 % (1800882)CaDiCaL version: 2.1.3 % 6.31/1.16 % (1800882)Termination reason: Instruction limit % 6.31/1.16 % (1800882)Termination phase: Saturation % 6.31/1.16 % (1800882)Time elapsed: 0.081 s % 6.31/1.16 % (1800882)Peak memory usage: 12 MB % 6.31/1.16 % (1800882)Instructions burned: 133 (million) % 6.31/1.16 % (1800935)ott-21_1_sil=16000:fs=off:random_seed=53999726:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.31/1.16 % (1800940)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4151824812:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.31/1.16 % (1800883)Instruction limit reached! % 6.31/1.16 % (1800883)------------------------------ % 6.31/1.16 % (1800883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.31/1.16 % (1800883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.16 % (1800883)CaDiCaL version: 2.1.3 % 6.31/1.16 % (1800883)Termination reason: Instruction limit % 6.31/1.16 % (1800883)Termination phase: Saturation % 6.31/1.16 % (1800883)Time elapsed: 0.108 s % 6.31/1.16 % (1800883)Peak memory usage: 13 MB % 6.31/1.16 % (1800883)Instructions burned: 160 (million) % 6.31/1.16 % (1800955)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1340148867:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.31/1.16 % (1800912)Instruction limit reached! % 6.31/1.16 % (1800912)------------------------------ % 6.31/1.16 % (1800912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.31/1.16 % (1800912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.16 % (1800912)CaDiCaL version: 2.1.3 % 6.31/1.16 % (1800912)Termination reason: Instruction limit % 6.31/1.16 % (1800912)Termination phase: Saturation % 6.31/1.16 % (1800912)Time elapsed: 0.086 s % 6.31/1.16 % (1800912)Peak memory usage: 12 MB % 6.31/1.16 % (1800912)Instructions burned: 131 (million) % 6.31/1.16 % (1800955)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.31/1.16 % (1800955)Terminated due to inappropriate strategy. % 6.31/1.16 % (1800955)------------------------------ % 6.31/1.16 % (1800955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.31/1.16 % (1800955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.16 % (1800955)CaDiCaL version: 2.1.3 % 6.31/1.16 % (1800955)Termination reason: Inappropriate % 6.31/1.16 % (1800955)Time elapsed: 0.001 s % 6.31/1.16 % (1800955)Peak memory usage: 10 MB % 6.31/1.16 % (1800955)Instructions burned: 1 (million) % 6.31/1.16 % (1800955)------------------------------ % 6.31/1.16 % (1800955)------------------------------ % 6.31/1.16 % (1800963)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1514298590:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.31/1.16 % (1800965)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3370540050:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.31/1.16 % (1800965)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.31/1.16 % (1800965)Terminated due to inappropriate strategy. % 6.31/1.16 % (1800965)------------------------------ % 6.31/1.16 % (1800965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.31/1.16 % (1800965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.16 % (1800965)CaDiCaL version: 2.1.3 % 6.31/1.16 % (1800965)Termination reason: Inappropriate % 6.31/1.16 % (1800965)Time elapsed: 0.001 s % 6.31/1.16 % (1800965)Peak memory usage: 10 MB % 6.31/1.16 % (1800965)Instructions burned: 1 (million) % 6.31/1.16 % (1800965)------------------------------ % 6.31/1.16 % (1800965)------------------------------ % 6.31/1.16 % (1800977)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=539607923:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 6.31/1.16 % (1800935)Instruction limit reached! % 6.31/1.16 % (1800935)------------------------------ % 6.31/1.16 % (1800935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.31/1.16 % (1800935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.31/1.16 % (1800935)CaDiCaL version: 2.1.3 % 6.31/1.16 % (1800935)Termination reason: Instruction limit % 6.31/1.16 % (1800935)Termination phase: Saturation % 17.95/3.03 % (1800935)Time elapsed: 0.080 s % 17.95/3.03 % (1800935)Peak memory usage: 12 MB % 17.95/3.03 % (1800935)Instructions burned: 181 (million) % 17.95/3.03 % (1800985)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2284612379:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 17.95/3.03 % (1800916)Instruction limit reached! % 17.95/3.03 % (1800916)------------------------------ % 17.95/3.03 % (1800916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.95/3.03 % (1800916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.95/3.03 % (1800916)CaDiCaL version: 2.1.3 % 17.95/3.03 % (1800916)Termination reason: Instruction limit % 17.95/3.03 % (1800916)Termination phase: Saturation % 17.95/3.03 % (1800916)Time elapsed: 0.196 s % 17.95/3.03 % (1800916)Peak memory usage: 17 MB % 17.95/3.03 % (1800916)Instructions burned: 685 (million) % 17.95/3.03 % (1801002)fmb+10_1_sil=64000:random_seed=2002356625:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 17.95/3.03 % (1801002)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.95/3.03 % (1801002)Terminated due to inappropriate strategy. % 17.95/3.03 % (1801002)------------------------------ % 17.95/3.03 % (1801002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.95/3.03 % (1801002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.95/3.03 % (1801002)CaDiCaL version: 2.1.3 % 17.95/3.03 % (1801002)Termination reason: Inappropriate % 17.95/3.03 % (1801002)Time elapsed: 0.0000 s % 17.95/3.03 % (1801002)Peak memory usage: 10 MB % 17.95/3.03 % (1801002)Instructions burned: 1 (million) % 17.95/3.03 % (1801002)------------------------------ % 17.95/3.03 % (1801002)------------------------------ % 17.95/3.03 % (1801009)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3770318961:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 17.95/3.03 % (1801009)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.95/3.03 % (1801009)Terminated due to inappropriate strategy. % 17.95/3.03 % (1801009)------------------------------ % 17.95/3.03 % (1801009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.95/3.03 % (1801009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.95/3.03 % (1801009)CaDiCaL version: 2.1.3 % 17.95/3.03 % (1801009)Termination reason: Inappropriate % 17.95/3.03 % (1801009)Time elapsed: 0.0000 s % 17.95/3.03 % (1801009)Peak memory usage: 10 MB % 17.95/3.03 % (1801009)Instructions burned: 1 (million) % 17.95/3.03 % (1801009)------------------------------ % 17.95/3.03 % (1801009)------------------------------ % 17.95/3.03 % (1801014)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2026564449:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 17.95/3.03 % (1801014)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.95/3.03 % (1801014)Terminated due to inappropriate strategy. % 17.95/3.03 % (1801014)------------------------------ % 17.95/3.03 % (1801014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.95/3.03 % (1801014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.95/3.03 % (1801014)CaDiCaL version: 2.1.3 % 17.95/3.03 % (1801014)Termination reason: Inappropriate % 17.95/3.03 % (1801014)Time elapsed: 0.0000 s % 17.95/3.03 % (1801014)Peak memory usage: 10 MB % 17.95/3.03 % (1801014)Instructions burned: 1 (million) % 17.95/3.03 % (1801014)------------------------------ % 17.95/3.03 % (1801014)------------------------------ % 17.95/3.03 % (1801020)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2272444472:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 17.95/3.03 % (1800940)Instruction limit reached! % 17.95/3.03 % (1800940)------------------------------ % 17.95/3.03 % (1800940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.95/3.03 % (1800940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.95/3.03 % (1800940)CaDiCaL version: 2.1.3 % 17.95/3.03 % (1800940)Termination reason: Instruction limit % 17.95/3.03 % (1800940)Termination phase: Saturation % 17.95/3.03 % (1800940)Time elapsed: 0.292 s % 17.95/3.03 % (1800940)Peak memory usage: 14 MB % 17.95/3.03 % (1800940)Instructions burned: 479 (million) % 17.95/3.03 % (1801057)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4146769236:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 17.95/3.03 % (1800977)Instruction limit reached! % 17.95/3.03 % (1800977)------------------------------ % 28.08/4.25 % (1800977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.08/4.25 % (1800977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.08/4.25 % (1800977)CaDiCaL version: 2.1.3 % 28.08/4.25 % (1800977)Termination reason: Instruction limit % 28.08/4.25 % (1800977)Termination phase: Saturation % 28.08/4.25 % (1800977)Time elapsed: 0.398 s % 28.08/4.25 % (1800977)Peak memory usage: 16 MB % 28.08/4.25 % (1800977)Instructions burned: 693 (million) % 28.08/4.25 % (1801059)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=117350692:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 28.08/4.25 % (1801059)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.08/4.25 % (1801059)Terminated due to inappropriate strategy. % 28.08/4.25 % (1801059)------------------------------ % 28.08/4.25 % (1801059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.08/4.25 % (1801059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.08/4.25 % (1801059)CaDiCaL version: 2.1.3 % 28.08/4.25 % (1801059)Termination reason: Inappropriate % 28.08/4.25 % (1801059)Time elapsed: 0.001 s % 28.08/4.25 % (1801059)Peak memory usage: 10 MB % 28.08/4.25 % (1801059)Instructions burned: 1 (million) % 28.08/4.25 % (1801059)------------------------------ % 28.08/4.25 % (1801059)------------------------------ % 28.08/4.25 % (1801061)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1881931614:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 28.08/4.25 % (1801061)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.08/4.25 % (1801061)Terminated due to inappropriate strategy. % 28.08/4.25 % (1801061)------------------------------ % 28.08/4.25 % (1801061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.08/4.25 % (1801061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.08/4.25 % (1801061)CaDiCaL version: 2.1.3 % 28.08/4.25 % (1801061)Termination reason: Inappropriate % 28.08/4.25 % (1801061)Time elapsed: 0.001 s % 28.08/4.25 % (1801061)Peak memory usage: 10 MB % 28.08/4.25 % (1801061)Instructions burned: 1 (million) % 28.08/4.25 % (1801061)------------------------------ % 28.08/4.25 % (1801061)------------------------------ % 28.08/4.25 % (1801063)ott-2_1_sil=16000:newcnf=on:random_seed=1568913132:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 28.08/4.25 % (1800985)Instruction limit reached! % 28.08/4.25 % (1800985)------------------------------ % 28.08/4.25 % (1800985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.08/4.25 % (1800985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.08/4.25 % (1800985)CaDiCaL version: 2.1.3 % 28.08/4.25 % (1800985)Termination reason: Instruction limit % 28.08/4.25 % (1800985)Termination phase: Saturation % 28.08/4.25 % (1800985)Time elapsed: 0.496 s % 28.08/4.25 % (1800985)Peak memory usage: 18 MB % 28.08/4.25 % (1800985)Instructions burned: 880 (million) % 28.08/4.25 % (1801065)ott+10_1_sil=32000:tgt=ground:random_seed=691524474:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 28.08/4.25 % (1800963)Instruction limit reached! % 28.08/4.25 % (1800963)------------------------------ % 28.08/4.25 % (1800963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.08/4.25 % (1800963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.08/4.25 % (1800963)CaDiCaL version: 2.1.3 % 28.08/4.25 % (1800963)Termination reason: Instruction limit % 28.08/4.25 % (1800963)Termination phase: Saturation % 28.08/4.25 % (1800963)Time elapsed: 0.713 s % 28.08/4.25 % (1800963)Peak memory usage: 18 MB % 28.08/4.25 % (1800963)Instructions burned: 1180 (million) % 28.08/4.25 % (1801067)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1729608156:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 28.08/4.25 % (1801067)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.08/4.25 % (1801067)Terminated due to inappropriate strategy. % 28.08/4.25 % (1801067)------------------------------ % 28.08/4.25 % (1801067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.08/4.25 % (1801067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.08/4.25 % (1801067)CaDiCaL version: 2.1.3 % 28.08/4.25 % (1801067)Termination reason: Inappropriate % 28.08/4.25 % (1801067)Time elapsed: 0.001 s % 28.08/4.25 % (1801067)Peak memory usage: 10 MB % 28.08/4.25 % (1801067)Instructions burned: 1 (million) % 84.89/12.21 % (1801067)------------------------------ % 84.89/12.21 % (1801067)------------------------------ % 84.89/12.21 % (1801069)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3773624587:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 84.89/12.21 % (1801063)Instruction limit reached! % 84.89/12.21 % (1801063)------------------------------ % 84.89/12.21 % (1801063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.89/12.21 % (1801063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.89/12.21 % (1801063)CaDiCaL version: 2.1.3 % 84.89/12.21 % (1801063)Termination reason: Instruction limit % 84.89/12.21 % (1801063)Termination phase: Saturation % 84.89/12.21 % (1801063)Time elapsed: 0.525 s % 84.89/12.21 % (1801063)Peak memory usage: 14 MB % 84.89/12.21 % (1801063)Instructions burned: 869 (million) % 84.89/12.21 % (1801071)dis+21_1_sil=32000:sas=cadical:random_seed=718726790:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 84.89/12.21 % (1801057)Instruction limit reached! % 84.89/12.21 % (1801057)------------------------------ % 84.89/12.21 % (1801057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.89/12.21 % (1801057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.89/12.21 % (1801057)CaDiCaL version: 2.1.3 % 84.89/12.21 % (1801057)Termination reason: Instruction limit % 84.89/12.21 % (1801057)Termination phase: Saturation % 84.89/12.21 % (1801057)Time elapsed: 0.844 s % 84.89/12.21 % (1801057)Peak memory usage: 23 MB % 84.89/12.21 % (1801057)Instructions burned: 1473 (million) % 84.89/12.21 % (1801073)ott+11_1_sil=16000:gs=on:random_seed=126977915:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 84.89/12.21 % (1801020)Instruction limit reached! % 84.89/12.21 % (1801020)------------------------------ % 84.89/12.21 % (1801020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.89/12.21 % (1801020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.89/12.21 % (1801020)CaDiCaL version: 2.1.3 % 84.89/12.21 % (1801020)Termination reason: Instruction limit % 84.89/12.21 % (1801020)Termination phase: Saturation % 84.89/12.21 % (1801020)Time elapsed: 1.483 s % 84.89/12.21 % (1801020)Peak memory usage: 43 MB % 84.89/12.21 % (1801020)Instructions burned: 5133 (million) % 84.89/12.21 % (1801075)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3507974543:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 84.89/12.21 % (1801075)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 84.89/12.21 % (1801075)Terminated due to inappropriate strategy. % 84.89/12.21 % (1801075)------------------------------ % 84.89/12.21 % (1801075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.89/12.21 % (1801075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.89/12.21 % (1801075)CaDiCaL version: 2.1.3 % 84.89/12.21 % (1801075)Termination reason: Inappropriate % 84.89/12.21 % (1801075)Time elapsed: 0.0000 s % 84.89/12.21 % (1801075)Peak memory usage: 10 MB % 84.89/12.21 % (1801075)Instructions burned: 1 (million) % 84.89/12.21 % (1801075)------------------------------ % 84.89/12.21 % (1801075)------------------------------ % 84.89/12.21 % (1801077)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2411999976:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 84.89/12.21 % (1801073)Instruction limit reached! % 84.89/12.21 % (1801073)------------------------------ % 84.89/12.21 % (1801073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.89/12.21 % (1801073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.89/12.21 % (1801073)CaDiCaL version: 2.1.3 % 84.89/12.21 % (1801073)Termination reason: Instruction limit % 84.89/12.21 % (1801073)Termination phase: Saturation % 84.89/12.21 % (1801073)Time elapsed: 1.261 s % 84.89/12.21 % (1801073)Peak memory usage: 23 MB % 84.89/12.21 % (1801073)Instructions burned: 2252 (million) % 84.89/12.21 % (1801079)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2258015896:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 84.89/12.21 % (1801069)Instruction limit reached! % 84.89/12.21 % (1801069)------------------------------ % 84.89/12.21 % (1801069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.89/12.21 % (1801069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.89/12.21 % (1801069)CaDiCaL version: 2.1.3 % 84.89/12.21 % (1801069)Termination reason: Instruction limit % 127.52/18.21 % (1801069)Termination phase: Saturation % 127.52/18.21 % (1801069)Time elapsed: 1.849 s % 127.52/18.21 % (1801069)Peak memory usage: 35 MB % 127.52/18.21 % (1801069)Instructions burned: 3512 (million) % 127.52/18.21 % (1801081)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2469290725:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 127.52/18.21 % (1801077)Instruction limit reached! % 127.52/18.21 % (1801077)------------------------------ % 127.52/18.21 % (1801077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.52/18.21 % (1801077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.52/18.21 % (1801077)CaDiCaL version: 2.1.3 % 127.52/18.21 % (1801077)Termination reason: Instruction limit % 127.52/18.21 % (1801077)Termination phase: Saturation % 127.52/18.21 % (1801077)Time elapsed: 1.230 s % 127.52/18.21 % (1801077)Peak memory usage: 45 MB % 127.52/18.21 % (1801077)Instructions burned: 4595 (million) % 127.52/18.21 % (1801083)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=666999906:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 127.52/18.21 % (1801083)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.52/18.21 % (1801083)Terminated due to inappropriate strategy. % 127.52/18.21 % (1801083)------------------------------ % 127.52/18.21 % (1801083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.52/18.21 % (1801083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.52/18.21 % (1801083)CaDiCaL version: 2.1.3 % 127.52/18.21 % (1801083)Termination reason: Inappropriate % 127.52/18.21 % (1801083)Time elapsed: 0.0000 s % 127.52/18.21 % (1801083)Peak memory usage: 10 MB % 127.52/18.21 % (1801083)Instructions burned: 1 (million) % 127.52/18.21 % (1801083)------------------------------ % 127.52/18.21 % (1801083)------------------------------ % 127.52/18.21 % (1801085)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2688110503:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 127.52/18.21 % (1801085)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.52/18.21 % (1801085)Terminated due to inappropriate strategy. % 127.52/18.21 % (1801085)------------------------------ % 127.52/18.21 % (1801085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.52/18.21 % (1801085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.52/18.21 % (1801085)CaDiCaL version: 2.1.3 % 127.52/18.21 % (1801085)Termination reason: Inappropriate % 127.52/18.21 % (1801085)Time elapsed: 0.0000 s % 127.52/18.21 % (1801085)Peak memory usage: 10 MB % 127.52/18.21 % (1801085)Instructions burned: 1 (million) % 127.52/18.21 % (1801085)------------------------------ % 127.52/18.21 % (1801085)------------------------------ % 127.52/18.21 % (1801087)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=488056676:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 127.52/18.21 % (1801087)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 127.52/18.21 % (1801087)Terminated due to inappropriate strategy. % 127.52/18.21 % (1801087)------------------------------ % 127.52/18.21 % (1801087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.52/18.21 % (1801087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.52/18.21 % (1801087)CaDiCaL version: 2.1.3 % 127.52/18.21 % (1801087)Termination reason: Inappropriate % 127.52/18.21 % (1801087)Time elapsed: 0.0000 s % 127.52/18.21 % (1801087)Peak memory usage: 10 MB % 127.52/18.21 % (1801087)Instructions burned: 1 (million) % 127.52/18.21 % (1801087)------------------------------ % 127.52/18.21 % (1801087)------------------------------ % 127.52/18.21 % (1801089)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1779708419:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 127.52/18.21 % (1801071)Instruction limit reached! % 127.52/18.21 % (1801071)------------------------------ % 127.52/18.21 % (1801071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 127.52/18.21 % (1801071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 127.52/18.21 % (1801071)CaDiCaL version: 2.1.3 % 127.52/18.21 % (1801071)Termination reason: Instruction limit % 127.52/18.21 % (1801071)Termination phase: Saturation % 127.52/18.21 % (1801071)Time elapsed: 2.016 s % 127.52/18.21 % (1801071)Peak memory usage: 31 MB % 127.52/18.21 % (1801071)Instructions burned: 3773 (million) % 127.52/18.21 % (1801091)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4097318953:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 127.52/18.21 % (1801065)Instruction limit reached! % 128.23/18.31 % (1801065)------------------------------ % 128.23/18.31 % (1801065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.23/18.31 % (1801065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.23/18.31 % (1801065)CaDiCaL version: 2.1.3 % 128.23/18.31 % (1801065)Termination reason: Instruction limit % 128.23/18.31 % (1801065)Termination phase: Saturation % 128.23/18.31 % (1801065)Time elapsed: 3.271 s % 128.23/18.31 % (1801065)Peak memory usage: 35 MB % 128.23/18.31 % (1801065)Instructions burned: 5114 (million) % 128.23/18.31 % (1801093)dis+10_16:1_sil=16000:random_seed=2505552683:i=9155:fsr=off_2959 on theBenchmark for (2959ds/9155Mi) % 128.23/18.31 % (1801081)Instruction limit reached! % 128.23/18.31 % (1801081)------------------------------ % 128.23/18.31 % (1801081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.23/18.31 % (1801081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.23/18.31 % (1801081)CaDiCaL version: 2.1.3 % 128.23/18.31 % (1801081)Termination reason: Instruction limit % 128.23/18.31 % (1801081)Termination phase: Saturation % 128.23/18.31 % (1801081)Time elapsed: 2.701 s % 128.23/18.31 % (1801081)Peak memory usage: 47 MB % 128.23/18.31 % (1801081)Instructions burned: 5211 (million) % 128.23/18.31 % (1801095)ott-3_8_sil=64000:random_seed=3992134013:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 128.23/18.31 % (1801089)Instruction limit reached! % 128.23/18.31 % (1801089)------------------------------ % 128.23/18.31 % (1801089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.23/18.31 % (1801089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.23/18.31 % (1801089)CaDiCaL version: 2.1.3 % 128.23/18.31 % (1801089)Termination reason: Instruction limit % 128.23/18.31 % (1801089)Termination phase: Saturation % 128.23/18.31 % (1801089)Time elapsed: 5.059 s % 128.23/18.31 % (1801089)Peak memory usage: 79 MB % 128.23/18.31 % (1801089)Instructions burned: 22569 (million) % 128.23/18.31 % (1801097)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=759135882:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi) % 128.23/18.31 % (1801097)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.23/18.31 % (1801097)Terminated due to inappropriate strategy. % 128.23/18.31 % (1801097)------------------------------ % 128.23/18.31 % (1801097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.23/18.31 % (1801097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.23/18.31 % (1801097)CaDiCaL version: 2.1.3 % 128.23/18.31 % (1801097)Termination reason: Inappropriate % 128.23/18.31 % (1801097)Time elapsed: 0.0000 s % 128.23/18.31 % (1801097)Peak memory usage: 10 MB % 128.23/18.31 % (1801097)Instructions burned: 1 (million) % 128.23/18.31 % (1801097)------------------------------ % 128.23/18.31 % (1801097)------------------------------ % 128.23/18.31 % (1801099)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2740570796:i=11404_2918 on theBenchmark for (2918ds/11404Mi) % 128.23/18.31 % (1801091)Instruction limit reached! % 128.23/18.31 % (1801091)------------------------------ % 128.23/18.31 % (1801091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.23/18.31 % (1801091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.23/18.31 % (1801091)CaDiCaL version: 2.1.3 % 128.23/18.31 % (1801091)Termination reason: Instruction limit % 128.23/18.31 % (1801091)Termination phase: Saturation % 128.23/18.31 % (1801091)Time elapsed: 5.079 s % 128.23/18.31 % (1801091)Peak memory usage: 54 MB % 128.23/18.31 % (1801091)Instructions burned: 8174 (million) % 128.23/18.31 % (1801101)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2644341365:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 128.23/18.31 % (1801093)Instruction limit reached! % 128.23/18.31 % (1801093)------------------------------ % 128.23/18.31 % (1801093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.23/18.31 % (1801093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.23/18.31 % (1801093)CaDiCaL version: 2.1.3 % 128.23/18.31 % (1801093)Termination reason: Instruction limit % 128.23/18.31 % (1801093)Termination phase: Saturation % 128.23/18.31 % (1801093)Time elapsed: 4.616 s % 128.23/18.31 % (1801093)Peak memory usage: 52 MB % 128.23/18.31 % (1801093)Instructions burned: 9155 (million) % 128.23/18.31 % (1801103)dis+33_16_sil=32000:sac=on:random_seed=3412140389:i=15851:nm=0_2913 on theBenchmark for (2913ds/15851Mi) % 128.23/18.31 % (1801099)Instruction limit reached! % 128.23/18.31 % (1801099)------------------------------ % 128.23/18.31 % (1801099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.26/19.16 % (1801099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.26/19.16 % (1801099)CaDiCaL version: 2.1.3 % 134.26/19.16 % (1801099)Termination reason: Instruction limit % 134.26/19.16 % (1801099)Termination phase: Saturation % 134.26/19.16 % (1801099)Time elapsed: 3.782 s % 134.26/19.16 % (1801099)Peak memory usage: 64 MB % 134.26/19.16 % (1801099)Instructions burned: 11405 (million) % 134.26/19.16 % (1801105)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=515306476:avsq=on:i=17627:add=on:amm=off_2880 on theBenchmark for (2880ds/17627Mi) % 134.26/19.16 % (1801079)Instruction limit reached! % 134.26/19.16 % (1801079)------------------------------ % 134.26/19.16 % (1801079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.26/19.16 % (1801079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.26/19.16 % (1801079)CaDiCaL version: 2.1.3 % 134.26/19.16 % (1801079)Termination reason: Instruction limit % 134.26/19.16 % (1801079)Termination phase: Saturation % 134.26/19.16 % (1801079)Time elapsed: 14.500 s % 134.26/19.16 % (1801079)Peak memory usage: 123 MB % 134.26/19.16 % (1801079)Instructions burned: 29341 (million) % 134.26/19.16 % (1801430)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=339587403:s2a=on:i=53295_2828 on theBenchmark for (2828ds/53295Mi) % 134.26/19.16 % (1801103)Instruction limit reached! % 134.26/19.16 % (1801103)------------------------------ % 134.26/19.16 % (1801103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.26/19.16 % (1801103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.26/19.16 % (1801103)CaDiCaL version: 2.1.3 % 134.26/19.16 % (1801103)Termination reason: Instruction limit % 134.26/19.16 % (1801103)Termination phase: Saturation % 134.26/19.16 % (1801103)Time elapsed: 8.676 s % 134.26/19.16 % (1801103)Peak memory usage: 152 MB % 134.26/19.16 % (1801103)Instructions burned: 15852 (million) % 134.26/19.16 % (1801440)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2133465375:i=26857:ins=20_2826 on theBenchmark for (2826ds/26857Mi) % 134.26/19.16 % (1801440)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.26/19.16 % (1801440)Terminated due to inappropriate strategy. % 134.26/19.16 % (1801440)------------------------------ % 134.26/19.16 % (1801440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.26/19.16 % (1801440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.26/19.16 % (1801440)CaDiCaL version: 2.1.3 % 134.26/19.16 % (1801440)Termination reason: Inappropriate % 134.26/19.16 % (1801440)Time elapsed: 0.001 s % 134.26/19.16 % (1801440)Peak memory usage: 10 MB % 134.26/19.16 % (1801440)Instructions burned: 1 (million) % 134.26/19.16 % (1801440)------------------------------ % 134.26/19.16 % (1801440)------------------------------ % 134.26/19.16 % (1801442)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3307962703:i=28120:bs=on:fsr=off_2825 on theBenchmark for (2825ds/28120Mi) % 134.26/19.16 % (1801101)Instruction limit reached! % 134.26/19.16 % (1801101)------------------------------ % 134.26/19.16 % (1801101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.26/19.16 % (1801101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.26/19.16 % (1801101)CaDiCaL version: 2.1.3 % 134.26/19.16 % (1801101)Termination reason: Instruction limit % 134.26/19.16 % (1801101)Termination phase: Saturation % 134.26/19.16 % (1801101)Time elapsed: 9.527 s % 134.26/19.16 % (1801101)Peak memory usage: 77 MB % 134.26/19.16 % (1801101)Instructions burned: 14134 (million) % 134.26/19.16 % (1801457)fmb+10_1_sil=256000:fmbss=7:random_seed=3380303442:fmbsr=1.6:i=182295_2820 on theBenchmark for (2820ds/182295Mi) % 134.26/19.16 % (1801457)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 134.26/19.16 % (1801457)Terminated due to inappropriate strategy. % 134.26/19.16 % (1801457)------------------------------ % 134.26/19.16 % (1801457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.26/19.16 % (1801457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.26/19.16 % (1801457)CaDiCaL version: 2.1.3 % 134.26/19.16 % (1801457)Termination reason: Inappropriate % 134.26/19.16 % (1801457)Time elapsed: 0.001 s % 134.26/19.16 % (1801457)Peak memory usage: 10 MB % 134.26/19.16 % (1801457)Instructions burned: 1 (million) % 134.26/19.16 % (1801457)------------------------------ % 134.26/19.16 % (1801457)------------------------------ % 134.26/19.16 % (1801459)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3427195911:i=44625:gsp=on_2820 on theBenchmark for (2820ds/44625Mi) % 145.52/20.88 % (1801459)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.52/20.88 % (1801459)Terminated due to inappropriate strategy. % 145.52/20.88 % (1801459)------------------------------ % 145.52/20.88 % (1801459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.52/20.88 % (1801459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.52/20.88 % (1801459)CaDiCaL version: 2.1.3 % 145.52/20.88 % (1801459)Termination reason: Inappropriate % 145.52/20.88 % (1801459)Time elapsed: 0.001 s % 145.52/20.88 % (1801459)Peak memory usage: 10 MB % 145.52/20.88 % (1801459)Instructions burned: 1 (million) % 145.52/20.88 % (1801459)------------------------------ % 145.52/20.88 % (1801459)------------------------------ % 145.52/20.88 % (1801461)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2919670746:i=160505_2820 on theBenchmark for (2820ds/160505Mi) % 145.52/20.88 % (1801461)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.52/20.88 % (1801461)Terminated due to inappropriate strategy. % 145.52/20.88 % (1801461)------------------------------ % 145.52/20.88 % (1801461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.52/20.88 % (1801461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.52/20.88 % (1801461)CaDiCaL version: 2.1.3 % 145.52/20.88 % (1801461)Termination reason: Inappropriate % 145.52/20.88 % (1801461)Time elapsed: 0.001 s % 145.52/20.88 % (1801461)Peak memory usage: 10 MB % 145.52/20.88 % (1801461)Instructions burned: 1 (million) % 145.52/20.88 % (1801461)------------------------------ % 145.52/20.88 % (1801461)------------------------------ % 145.52/20.88 % (1801105)Instruction limit reached! % 145.52/20.88 % (1801105)------------------------------ % 145.52/20.88 % (1801105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.52/20.88 % (1801105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.52/20.88 % (1801105)CaDiCaL version: 2.1.3 % 145.52/20.88 % (1801105)Termination reason: Instruction limit % 145.52/20.88 % (1801105)Termination phase: Saturation % 145.52/20.88 % (1801105)Time elapsed: 6.036 s % 145.52/20.88 % (1801105)Peak memory usage: 78 MB % 145.52/20.88 % (1801105)Instructions burned: 17629 (million) % 145.52/20.88 % (1801465)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2974142525:fmbsr=1.3:i=225729_2819 on theBenchmark for (2819ds/225729Mi) % 145.52/20.88 % (1801465)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.52/20.88 % (1801465)Terminated due to inappropriate strategy. % 145.52/20.88 % (1801465)------------------------------ % 145.52/20.88 % (1801465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.52/20.88 % (1801465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.52/20.88 % (1801465)CaDiCaL version: 2.1.3 % 145.52/20.88 % (1801465)Termination reason: Inappropriate % 145.52/20.88 % (1801465)Time elapsed: 0.001 s % 145.52/20.88 % (1801465)Peak memory usage: 11 MB % 145.52/20.88 % (1801465)Instructions burned: 1 (million) % 145.52/20.88 % (1801465)------------------------------ % 145.52/20.88 % (1801465)------------------------------ % 145.52/20.88 % (1801467)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3110101802:fmbsr=2:i=185024:ins=7_2819 on theBenchmark for (2819ds/185024Mi) % 145.52/20.88 % (1801467)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.52/20.88 % (1801467)Terminated due to inappropriate strategy. % 145.52/20.88 % (1801467)------------------------------ % 145.52/20.88 % (1801467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.52/20.88 % (1801467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.52/20.88 % (1801467)CaDiCaL version: 2.1.3 % 145.52/20.88 % (1801467)Termination reason: Inappropriate % 145.52/20.88 % (1801467)Time elapsed: 0.001 s % 145.52/20.88 % (1801467)Peak memory usage: 10 MB % 145.52/20.88 % (1801467)Instructions burned: 1 (million) % 145.52/20.88 % (1801467)------------------------------ % 145.52/20.88 % (1801467)------------------------------ % 145.52/20.88 % (1801469)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4060147076:rtra=on_2819 on theBenchmark for (2819ds/0Mi) % 145.52/20.88 % (1801469)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 145.52/20.88 % (1801469)Terminated due to inappropriate strategy. % 145.52/20.88 % (1801469)------------------------------ % 145.52/20.88 % (1801469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 145.52/20.88 % (1801469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.56/23.76 % (1801469)CaDiCaL version: 2.1.3 % 166.56/23.76 % (1801469)Termination reason: Inappropriate % 166.56/23.76 % (1801469)Time elapsed: 0.001 s % 166.56/23.76 % (1801469)Peak memory usage: 10 MB % 166.56/23.76 % (1801469)Instructions burned: 1 (million) % 166.56/23.76 % (1801469)------------------------------ % 166.56/23.76 % (1801469)------------------------------ % 166.56/23.76 % (1801472)% WARNING: option uhcvi not known. % 166.56/23.76 % (1801475)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2934378992:i=176048:add=on:rtra=on:rawr=on_2819 on theBenchmark for (2819ds/176048Mi) % 166.56/23.76 % (1801472)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3545477429:i=271062:add=off:rtra=on:rawr=on_2819 on theBenchmark for (2819ds/271062Mi) % 166.56/23.76 % (1801095)Instruction limit reached! % 166.56/23.76 % (1801095)------------------------------ % 166.56/23.76 % (1801095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.56/23.76 % (1801095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.56/23.76 % (1801095)CaDiCaL version: 2.1.3 % 166.56/23.76 % (1801095)Termination reason: Instruction limit % 166.56/23.76 % (1801095)Termination phase: Saturation % 166.56/23.76 % (1801095)Time elapsed: 12.727 s % 166.56/23.76 % (1801095)Peak memory usage: 61 MB % 166.56/23.76 % (1801095)Instructions burned: 20139 (million) % 166.56/23.76 % (1801482)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3207417792:i=206:fgj=on:rtra=on_2817 on theBenchmark for (2817ds/206Mi) % 166.56/23.76 % (1801482)Instruction limit reached! % 166.56/23.76 % (1801482)------------------------------ % 166.56/23.76 % (1801482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.56/23.76 % (1801482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.56/23.76 % (1801482)CaDiCaL version: 2.1.3 % 166.56/23.76 % (1801482)Termination reason: Instruction limit % 166.56/23.76 % (1801482)Termination phase: Saturation % 166.56/23.76 % (1801482)Time elapsed: 0.106 s % 166.56/23.76 % (1801482)Peak memory usage: 13 MB % 166.56/23.76 % (1801482)Instructions burned: 208 (million) % 166.56/23.76 % (1801488)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2962651328:i=232:rtra=on_2815 on theBenchmark for (2815ds/232Mi) % 166.56/23.76 % (1801488)Instruction limit reached! % 166.56/23.76 % (1801488)------------------------------ % 166.56/23.76 % (1801488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.56/23.76 % (1801488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.56/23.76 % (1801488)CaDiCaL version: 2.1.3 % 166.56/23.76 % (1801488)Termination reason: Instruction limit % 166.56/23.76 % (1801488)Termination phase: Saturation % 166.56/23.76 % (1801488)Time elapsed: 0.094 s % 166.56/23.76 % (1801488)Peak memory usage: 13 MB % 166.56/23.76 % (1801488)Instructions burned: 234 (million) % 166.56/23.76 % (1801492)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2835656401:i=262:rtra=on_2814 on theBenchmark for (2814ds/262Mi) % 166.56/23.76 % (1801492)Instruction limit reached! % 166.56/23.76 % (1801492)------------------------------ % 166.56/23.76 % (1801492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.56/23.76 % (1801492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.56/23.76 % (1801492)CaDiCaL version: 2.1.3 % 166.56/23.76 % (1801492)Termination reason: Instruction limit % 166.56/23.76 % (1801492)Termination phase: Saturation % 166.56/23.76 % (1801492)Time elapsed: 0.128 s % 166.56/23.76 % (1801492)Peak memory usage: 14 MB % 166.56/23.76 % (1801492)Instructions burned: 263 (million) % 166.56/23.76 % (1801498)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2183003022:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2813 on theBenchmark for (2813ds/318Mi) % 166.56/23.76 % (1801498)Instruction limit reached! % 166.56/23.76 % (1801498)------------------------------ % 166.56/23.76 % (1801498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.56/23.76 % (1801498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.56/23.76 % (1801498)CaDiCaL version: 2.1.3 % 166.56/23.76 % (1801498)Termination reason: Instruction limit % 166.56/23.76 % (1801498)Termination phase: Saturation % 166.56/23.76 % (1801498)Time elapsed: 0.186 s % 166.56/23.76 % (1801498)Peak memory usage: 14 MB % 166.56/23.76 % (1801498)Instructions burned: 319 (million) % 166.56/23.76 % (1801504)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=857220551:i=1428:nm=2:rtra=on_2811 on theBenchmark for (2811ds/1428Mi) % 216.34/30.73 % (1801504)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 216.34/30.73 % (1801504)Terminated due to inappropriate strategy. % 216.34/30.73 % (1801504)------------------------------ % 216.34/30.73 % (1801504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.34/30.73 % (1801504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.34/30.73 % (1801504)CaDiCaL version: 2.1.3 % 216.34/30.73 % (1801504)Termination reason: Inappropriate % 216.34/30.73 % (1801504)Time elapsed: 0.001 s % 216.34/30.73 % (1801504)Peak memory usage: 10 MB % 216.34/30.73 % (1801504)Instructions burned: 1 (million) % 216.34/30.73 % (1801504)------------------------------ % 216.34/30.73 % (1801504)------------------------------ % 216.34/30.73 % (1801509)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3407808583:i=262:bd=preordered:rtra=on:fsd=on_2810 on theBenchmark for (2810ds/262Mi) % 216.34/30.73 % (1801509)Instruction limit reached! % 216.34/30.73 % (1801509)------------------------------ % 216.34/30.73 % (1801509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.34/30.73 % (1801509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.34/30.73 % (1801509)CaDiCaL version: 2.1.3 % 216.34/30.73 % (1801509)Termination reason: Instruction limit % 216.34/30.73 % (1801509)Termination phase: Saturation % 216.34/30.73 % (1801509)Time elapsed: 0.125 s % 216.34/30.73 % (1801509)Peak memory usage: 14 MB % 216.34/30.73 % (1801509)Instructions burned: 262 (million) % 216.34/30.73 % (1801513)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=3301749052:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2809 on theBenchmark for (2809ds/1368Mi) % 216.34/30.73 % (1801513)Instruction limit reached! % 216.34/30.73 % (1801513)------------------------------ % 216.34/30.73 % (1801513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.34/30.73 % (1801513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.34/30.73 % (1801513)CaDiCaL version: 2.1.3 % 216.34/30.73 % (1801513)Termination reason: Instruction limit % 216.34/30.73 % (1801513)Termination phase: Saturation % 216.34/30.73 % (1801513)Time elapsed: 0.728 s % 216.34/30.73 % (1801513)Peak memory usage: 23 MB % 216.34/30.73 % (1801513)Instructions burned: 1371 (million) % 216.34/30.73 % (1801533)ott-21_1_sil=16000:si=on:fs=off:random_seed=3122545565:i=360:av=off:fsr=off:rtra=on_2801 on theBenchmark for (2801ds/360Mi) % 216.34/30.73 % (1801533)Instruction limit reached! % 216.34/30.73 % (1801533)------------------------------ % 216.34/30.73 % (1801533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.34/30.73 % (1801533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.34/30.73 % (1801533)CaDiCaL version: 2.1.3 % 216.34/30.73 % (1801533)Termination reason: Instruction limit % 216.34/30.73 % (1801533)Termination phase: Saturation % 216.34/30.73 % (1801533)Time elapsed: 0.235 s % 216.34/30.73 % (1801533)Peak memory usage: 13 MB % 216.34/30.73 % (1801533)Instructions burned: 361 (million) % 216.34/30.73 % (1801544)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=629041510:i=954:bd=all:rtra=on_2798 on theBenchmark for (2798ds/954Mi) % 216.34/30.73 % (1801544)Instruction limit reached! % 216.34/30.73 % (1801544)------------------------------ % 216.34/30.73 % (1801544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.34/30.73 % (1801544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.34/30.73 % (1801544)CaDiCaL version: 2.1.3 % 216.34/30.73 % (1801544)Termination reason: Instruction limit % 216.34/30.73 % (1801544)Termination phase: Saturation % 216.34/30.73 % (1801544)Time elapsed: 0.460 s % 216.34/30.73 % (1801544)Peak memory usage: 16 MB % 216.34/30.73 % (1801544)Instructions burned: 955 (million) % 216.34/30.73 % (1801553)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=51961168:fmbsr=1.3:i=1730:ins=25:rtra=on_2793 on theBenchmark for (2793ds/1730Mi) % 216.34/30.73 % (1801553)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 216.34/30.73 % (1801553)Terminated due to inappropriate strategy. % 216.34/30.73 % (1801553)------------------------------ % 216.34/30.73 % (1801553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.34/30.73 % (1801553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.34/30.73 % (1801553)CaDiCaL version: 2.1.3 % 216.34/30.73 % (1801553)Termination reason: Inappropriate % 293.22/41.51 % (1801553)Time elapsed: 0.001 s % 293.22/41.51 % (1801553)Peak memory usage: 10 MB % 293.22/41.51 % (1801553)Instructions burned: 1 (million) % 293.22/41.51 % (1801553)------------------------------ % 293.22/41.51 % (1801553)------------------------------ % 293.22/41.51 % (1801555)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2383974904:i=2358:rtra=on_2793 on theBenchmark for (2793ds/2358Mi) % 293.22/41.51 % (1801555)Instruction limit reached! % 293.22/41.51 % (1801555)------------------------------ % 293.22/41.51 % (1801555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.22/41.51 % (1801555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.22/41.51 % (1801555)CaDiCaL version: 2.1.3 % 293.22/41.51 % (1801555)Termination reason: Instruction limit % 293.22/41.51 % (1801555)Termination phase: Saturation % 293.22/41.51 % (1801555)Time elapsed: 1.165 s % 293.22/41.51 % (1801555)Peak memory usage: 23 MB % 293.22/41.51 % (1801555)Instructions burned: 2358 (million) % 293.22/41.51 % (1801576)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3226923039:i=1778:ins=1:rtra=on_2781 on theBenchmark for (2781ds/1778Mi) % 293.22/41.51 % (1801576)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 293.22/41.51 % (1801576)Terminated due to inappropriate strategy. % 293.22/41.51 % (1801576)------------------------------ % 293.22/41.51 % (1801576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.22/41.51 % (1801576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.22/41.51 % (1801576)CaDiCaL version: 2.1.3 % 293.22/41.51 % (1801576)Termination reason: Inappropriate % 293.22/41.51 % (1801576)Time elapsed: 0.001 s % 293.22/41.51 % (1801576)Peak memory usage: 10 MB % 293.22/41.51 % (1801576)Instructions burned: 1 (million) % 293.22/41.51 % (1801576)------------------------------ % 293.22/41.51 % (1801576)------------------------------ % 293.22/41.51 % (1801578)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=197306799:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2780 on theBenchmark for (2780ds/1384Mi) % 293.22/41.51 % (1801578)Instruction limit reached! % 293.22/41.51 % (1801578)------------------------------ % 293.22/41.51 % (1801578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.22/41.51 % (1801578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.22/41.51 % (1801578)CaDiCaL version: 2.1.3 % 293.22/41.51 % (1801578)Termination reason: Instruction limit % 293.22/41.51 % (1801578)Termination phase: Saturation % 293.22/41.51 % (1801578)Time elapsed: 0.663 s % 293.22/41.51 % (1801578)Peak memory usage: 22 MB % 293.22/41.51 % (1801578)Instructions burned: 1384 (million) % 293.22/41.51 % (1801593)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=562314503:i=1758:kws=inv_precedence:fsr=off:rtra=on_2774 on theBenchmark for (2774ds/1758Mi) % 293.22/41.51 % (1801593)Instruction limit reached! % 293.22/41.51 % (1801593)------------------------------ % 293.22/41.51 % (1801593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.22/41.51 % (1801593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.22/41.51 % (1801593)CaDiCaL version: 2.1.3 % 293.22/41.51 % (1801593)Termination reason: Instruction limit % 293.22/41.51 % (1801593)Termination phase: Saturation % 293.22/41.51 % (1801593)Time elapsed: 0.817 s % 293.22/41.51 % (1801593)Peak memory usage: 25 MB % 293.22/41.51 % (1801593)Instructions burned: 1758 (million) % 293.22/41.51 % (1801604)fmb+10_1_sil=64000:si=on:random_seed=231836238:i=44122:nm=2:rtra=on:gsp=on_2765 on theBenchmark for (2765ds/44122Mi) % 293.22/41.51 % (1801604)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 293.22/41.51 % (1801604)Terminated due to inappropriate strategy. % 293.22/41.51 % (1801604)------------------------------ % 293.22/41.51 % (1801604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.22/41.51 % (1801604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.22/41.51 % (1801604)CaDiCaL version: 2.1.3 % 293.22/41.51 % (1801604)Termination reason: Inappropriate % 293.22/41.51 % (1801604)Time elapsed: 0.002 s % 293.22/41.51 % (1801604)Peak memory usage: 10 MB % 293.22/41.51 % (1801604)Instructions burned: 1 (million) % 293.22/41.51 % (1801604)------------------------------ % 293.22/41.51 % (1801604)------------------------------ % 293.22/41.51 % (1801608)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2166587583:i=19030:nm=5:rtra=on_2765 on theBenchmarTerminated % 300.33/42.54 % Vampire exiting % 300.33/42.54 Terminated %------------------------------------------------------------------------------