%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW007_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:38:11 PM UTC 2026 % Result : Timeout 300.05s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW007_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.16 % Computer : n013.cluster.edu % 0.11/0.16 % Model : x86_64 x86_64 % 0.11/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.16 % Memory : 8046.5625MB % 0.11/0.16 % OS : Linux 6.8.0-71-generic % 0.11/0.17 % CPULimit : 300 % 0.11/0.17 % WCLimit : 300 % 0.11/0.17 % DateTime : Mon Sep 28 13:07:51 UTC 2026 % 0.11/0.17 % CPUTime : % 0.11/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.20 Running first-order model finding % 0.11/0.20 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.91/0.70 % (1164156)Will run a generic schedule for satisfiability detection. % 2.91/0.70 % (1164161)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=348795492_2999 on theBenchmark for (2999ds/0Mi) % 2.91/0.70 % (1164162)% WARNING: option uhcvi not known. % 2.91/0.70 % (1164165)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2887874184:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.91/0.70 % (1164162)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1087454453:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.91/0.70 % (1164163)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2618958404:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.91/0.70 % (1164164)dis+10_1_sil=32000:sp=arity:random_seed=3437125531:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.91/0.70 % (1164166)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3832324752:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.91/0.70 % (1164167)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4076011760:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.91/0.70 % (1164161)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.91/0.70 % (1164161)Terminated due to inappropriate strategy. % 2.91/0.70 % (1164161)------------------------------ % 2.91/0.70 % (1164161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.91/0.70 % (1164161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.91/0.70 % (1164161)CaDiCaL version: 2.1.3 % 2.91/0.70 % (1164161)Termination reason: Inappropriate % 2.91/0.70 % (1164161)Time elapsed: 0.016 s % 2.91/0.70 % (1164161)Peak memory usage: 12 MB % 2.91/0.70 % (1164161)Instructions burned: 67 (million) % 2.91/0.70 % (1164161)------------------------------ % 2.91/0.70 % (1164161)------------------------------ % 2.91/0.70 % (1164175)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3565336204:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.91/0.70 % (1164175)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.91/0.70 % (1164175)Terminated due to inappropriate strategy. % 2.91/0.70 % (1164175)------------------------------ % 2.91/0.70 % (1164175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.91/0.70 % (1164175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.91/0.70 % (1164175)CaDiCaL version: 2.1.3 % 2.91/0.70 % (1164175)Termination reason: Inappropriate % 2.91/0.70 % (1164175)Time elapsed: 0.016 s % 2.91/0.70 % (1164175)Peak memory usage: 12 MB % 2.91/0.70 % (1164175)Instructions burned: 67 (million) % 2.91/0.70 % (1164175)------------------------------ % 2.91/0.70 % (1164175)------------------------------ % 2.91/0.70 % (1164164)Instruction limit reached! % 2.91/0.70 % (1164164)------------------------------ % 2.91/0.70 % (1164164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.91/0.70 % (1164164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.91/0.70 % (1164164)CaDiCaL version: 2.1.3 % 2.91/0.70 % (1164164)Termination reason: Instruction limit % 2.91/0.70 % (1164164)Termination phase: Saturation % 2.91/0.70 % (1164164)Time elapsed: 0.048 s % 2.91/0.70 % (1164164)Peak memory usage: 14 MB % 2.91/0.70 % (1164164)Instructions burned: 104 (million) % 2.91/0.70 % (1164177)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2331565951:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.91/0.70 % (1164165)Instruction limit reached! % 2.91/0.70 % (1164165)------------------------------ % 2.91/0.70 % (1164165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.91/0.70 % (1164165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.91/0.70 % (1164165)CaDiCaL version: 2.1.3 % 2.91/0.70 % (1164165)Termination reason: Instruction limit % 2.91/0.70 % (1164165)Termination phase: Saturation % 2.91/0.70 % (1164165)Time elapsed: 0.052 s % 2.91/0.70 % (1164165)Peak memory usage: 14 MB % 2.91/0.70 % (1164165)Instructions burned: 116 (million) % 2.91/0.70 % (1164166)Instruction limit reached! % 2.91/0.70 % (1164166)------------------------------ % 2.91/0.70 % (1164166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.91/0.70 % (1164166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.91/0.70 % (1164166)CaDiCaL version: 2.1.3 % 2.91/0.70 % (1164166)Termination reason: Instruction limit % 4.14/0.99 % (1164166)Termination phase: Saturation % 4.14/0.99 % (1164166)Time elapsed: 0.055 s % 4.14/0.99 % (1164166)Peak memory usage: 14 MB % 4.14/0.99 % (1164166)Instructions burned: 132 (million) % 4.14/0.99 % (1164178)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=2179305489:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 4.14/0.99 % (1164167)Instruction limit reached! % 4.14/0.99 % (1164167)------------------------------ % 4.14/0.99 % (1164167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.14/0.99 % (1164167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.14/0.99 % (1164167)CaDiCaL version: 2.1.3 % 4.14/0.99 % (1164167)Termination reason: Instruction limit % 4.14/0.99 % (1164167)Termination phase: Saturation % 4.14/0.99 % (1164167)Time elapsed: 0.068 s % 4.14/0.99 % (1164167)Peak memory usage: 15 MB % 4.14/0.99 % (1164167)Instructions burned: 160 (million) % 4.14/0.99 % (1164180)ott-21_1_sil=16000:fs=off:random_seed=1812057355:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 4.14/0.99 % (1164181)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=692389957:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 4.14/0.99 % (1164177)Instruction limit reached! % 4.14/0.99 % (1164177)------------------------------ % 4.14/0.99 % (1164177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.14/0.99 % (1164177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.14/0.99 % (1164177)CaDiCaL version: 2.1.3 % 4.14/0.99 % (1164177)Termination reason: Instruction limit % 4.14/0.99 % (1164177)Termination phase: Saturation % 4.14/0.99 % (1164177)Time elapsed: 0.029 s % 4.14/0.99 % (1164177)Peak memory usage: 14 MB % 4.14/0.99 % (1164177)Instructions burned: 134 (million) % 4.14/0.99 % (1164183)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=155907912:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 4.14/0.99 % (1164186)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=29439327:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 4.14/0.99 % (1164183)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.14/0.99 % (1164183)Terminated due to inappropriate strategy. % 4.14/0.99 % (1164183)------------------------------ % 4.14/0.99 % (1164183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.14/0.99 % (1164183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.14/0.99 % (1164183)CaDiCaL version: 2.1.3 % 4.14/0.99 % (1164183)Termination reason: Inappropriate % 4.14/0.99 % (1164183)Time elapsed: 0.029 s % 4.14/0.99 % (1164183)Peak memory usage: 12 MB % 4.14/0.99 % (1164183)Instructions burned: 66 (million) % 4.14/0.99 % (1164183)------------------------------ % 4.14/0.99 % (1164183)------------------------------ % 4.14/0.99 % (1164189)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3000272018:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 4.14/0.99 % (1164180)Instruction limit reached! % 4.14/0.99 % (1164180)------------------------------ % 4.14/0.99 % (1164180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.14/0.99 % (1164180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.14/0.99 % (1164180)CaDiCaL version: 2.1.3 % 4.14/0.99 % (1164180)Termination reason: Instruction limit % 4.14/0.99 % (1164180)Termination phase: Saturation % 4.14/0.99 % (1164180)Time elapsed: 0.085 s % 4.14/0.99 % (1164180)Peak memory usage: 14 MB % 4.14/0.99 % (1164180)Instructions burned: 180 (million) % 4.14/0.99 % (1164191)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=2629070957: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) % 4.14/0.99 % (1164189)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.14/0.99 % (1164189)Terminated due to inappropriate strategy. % 4.14/0.99 % (1164189)------------------------------ % 4.14/0.99 % (1164189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.14/0.99 % (1164189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.14/0.99 % (1164189)CaDiCaL version: 2.1.3 % 4.14/0.99 % (1164189)Termination reason: Inappropriate % 4.14/0.99 % (1164189)Time elapsed: 0.042 s % 4.14/0.99 % (1164189)Peak memory usage: 14 MB % 16.36/2.67 % (1164189)Instructions burned: 93 (million) % 16.36/2.67 % (1164189)------------------------------ % 16.36/2.67 % (1164189)------------------------------ % 16.36/2.67 % (1164193)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1394416997:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 16.36/2.67 % (1164181)Instruction limit reached! % 16.36/2.67 % (1164181)------------------------------ % 16.36/2.67 % (1164181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.36/2.67 % (1164181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.36/2.67 % (1164181)CaDiCaL version: 2.1.3 % 16.36/2.67 % (1164181)Termination reason: Instruction limit % 16.36/2.67 % (1164181)Termination phase: Saturation % 16.36/2.67 % (1164181)Time elapsed: 0.210 s % 16.36/2.67 % (1164181)Peak memory usage: 15 MB % 16.36/2.67 % (1164181)Instructions burned: 479 (million) % 16.36/2.67 % (1164195)fmb+10_1_sil=64000:random_seed=2023245450:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 16.36/2.67 % (1164195)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.36/2.67 % (1164195)Terminated due to inappropriate strategy. % 16.36/2.67 % (1164195)------------------------------ % 16.36/2.67 % (1164195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.36/2.67 % (1164195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.36/2.67 % (1164195)CaDiCaL version: 2.1.3 % 16.36/2.67 % (1164195)Termination reason: Inappropriate % 16.36/2.67 % (1164195)Time elapsed: 0.032 s % 16.36/2.67 % (1164195)Peak memory usage: 13 MB % 16.36/2.67 % (1164195)Instructions burned: 73 (million) % 16.36/2.67 % (1164195)------------------------------ % 16.36/2.67 % (1164195)------------------------------ % 16.36/2.67 % (1164197)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1252745806:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 16.36/2.67 % (1164178)Instruction limit reached! % 16.36/2.67 % (1164178)------------------------------ % 16.36/2.67 % (1164178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.36/2.67 % (1164178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.36/2.67 % (1164178)CaDiCaL version: 2.1.3 % 16.36/2.67 % (1164178)Termination reason: Instruction limit % 16.36/2.67 % (1164178)Termination phase: Saturation % 16.36/2.67 % (1164178)Time elapsed: 0.320 s % 16.36/2.67 % (1164178)Peak memory usage: 17 MB % 16.36/2.67 % (1164178)Instructions burned: 686 (million) % 16.36/2.67 % (1164197)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.36/2.67 % (1164197)Terminated due to inappropriate strategy. % 16.36/2.67 % (1164197)------------------------------ % 16.36/2.67 % (1164197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.36/2.67 % (1164197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.36/2.67 % (1164197)CaDiCaL version: 2.1.3 % 16.36/2.67 % (1164197)Termination reason: Inappropriate % 16.36/2.67 % (1164197)Time elapsed: 0.030 s % 16.36/2.67 % (1164197)Peak memory usage: 12 MB % 16.36/2.67 % (1164197)Instructions burned: 67 (million) % 16.36/2.67 % (1164197)------------------------------ % 16.36/2.67 % (1164197)------------------------------ % 16.36/2.67 % (1164186)Instruction limit reached! % 16.36/2.67 % (1164186)------------------------------ % 16.36/2.67 % (1164186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.36/2.67 % (1164186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.36/2.67 % (1164186)CaDiCaL version: 2.1.3 % 16.36/2.67 % (1164186)Termination reason: Instruction limit % 16.36/2.67 % (1164186)Termination phase: Saturation % 16.36/2.67 % (1164186)Time elapsed: 0.313 s % 16.36/2.67 % (1164186)Peak memory usage: 19 MB % 16.36/2.67 % (1164186)Instructions burned: 1180 (million) % 16.36/2.67 % (1164199)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=820807537:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 16.36/2.67 % (1164200)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1585922850:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 16.36/2.67 % (1164201)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3400220474:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 16.36/2.67 % (1164199)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 16.36/2.67 % (1164199)Terminated due to inappropriate strategy. % 16.36/2.67 % (1164199)------------------------------ % 16.36/2.67 % (1164199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.43/3.88 % (1164199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.43/3.88 % (1164199)CaDiCaL version: 2.1.3 % 24.43/3.88 % (1164199)Termination reason: Inappropriate % 24.43/3.88 % (1164199)Time elapsed: 0.028 s % 24.43/3.88 % (1164199)Peak memory usage: 12 MB % 24.43/3.88 % (1164199)Instructions burned: 67 (million) % 24.43/3.88 % (1164199)------------------------------ % 24.43/3.88 % (1164199)------------------------------ % 24.43/3.88 % (1164205)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=725380200:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 24.43/3.88 % (1164205)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.43/3.88 % (1164205)Terminated due to inappropriate strategy. % 24.43/3.88 % (1164205)------------------------------ % 24.43/3.88 % (1164205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.43/3.88 % (1164205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.43/3.88 % (1164205)CaDiCaL version: 2.1.3 % 24.43/3.88 % (1164205)Termination reason: Inappropriate % 24.43/3.88 % (1164205)Time elapsed: 0.028 s % 24.43/3.88 % (1164205)Peak memory usage: 13 MB % 24.43/3.88 % (1164205)Instructions burned: 67 (million) % 24.43/3.88 % (1164205)------------------------------ % 24.43/3.88 % (1164205)------------------------------ % 24.43/3.88 % (1164207)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2701884207:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 24.43/3.88 % (1164207)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.43/3.88 % (1164207)Terminated due to inappropriate strategy. % 24.43/3.88 % (1164207)------------------------------ % 24.43/3.88 % (1164207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.43/3.88 % (1164207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.43/3.88 % (1164207)CaDiCaL version: 2.1.3 % 24.43/3.88 % (1164207)Termination reason: Inappropriate % 24.43/3.88 % (1164207)Time elapsed: 0.028 s % 24.43/3.88 % (1164207)Peak memory usage: 13 MB % 24.43/3.88 % (1164207)Instructions burned: 67 (million) % 24.43/3.88 % (1164207)------------------------------ % 24.43/3.88 % (1164207)------------------------------ % 24.43/3.88 % (1164209)ott-2_1_sil=16000:newcnf=on:random_seed=2198085930:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 24.43/3.88 % (1164191)Instruction limit reached! % 24.43/3.88 % (1164191)------------------------------ % 24.43/3.88 % (1164191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.43/3.88 % (1164191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.43/3.88 % (1164191)CaDiCaL version: 2.1.3 % 24.43/3.88 % (1164191)Termination reason: Instruction limit % 24.43/3.88 % (1164191)Termination phase: Saturation % 24.43/3.88 % (1164191)Time elapsed: 0.384 s % 24.43/3.88 % (1164191)Peak memory usage: 20 MB % 24.43/3.88 % (1164191)Instructions burned: 693 (million) % 24.43/3.88 % (1164211)ott+10_1_sil=32000:tgt=ground:random_seed=1953323142:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 24.43/3.88 % (1164193)Instruction limit reached! % 24.43/3.88 % (1164193)------------------------------ % 24.43/3.88 % (1164193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.43/3.88 % (1164193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.43/3.88 % (1164193)CaDiCaL version: 2.1.3 % 24.43/3.88 % (1164193)Termination reason: Instruction limit % 24.43/3.88 % (1164193)Termination phase: Saturation % 24.43/3.88 % (1164193)Time elapsed: 0.473 s % 24.43/3.88 % (1164193)Peak memory usage: 20 MB % 24.43/3.88 % (1164193)Instructions burned: 880 (million) % 24.43/3.88 % (1164213)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=655279635:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 24.43/3.88 % (1164213)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 24.43/3.88 % (1164213)Terminated due to inappropriate strategy. % 24.43/3.88 % (1164213)------------------------------ % 24.43/3.88 % (1164213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 24.43/3.88 % (1164213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.43/3.88 % (1164213)CaDiCaL version: 2.1.3 % 24.43/3.88 % (1164213)Termination reason: Inappropriate % 24.43/3.88 % (1164213)Time elapsed: 0.029 s % 24.43/3.88 % (1164213)Peak memory usage: 12 MB % 24.43/3.88 % (1164213)Instructions burned: 67 (million) % 98.72/14.18 % (1164213)------------------------------ % 98.72/14.18 % (1164213)------------------------------ % 98.72/14.18 % (1164201)Instruction limit reached! % 98.72/14.18 % (1164201)------------------------------ % 98.72/14.18 % (1164201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.72/14.18 % (1164201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.72/14.18 % (1164201)CaDiCaL version: 2.1.3 % 98.72/14.18 % (1164201)Termination reason: Instruction limit % 98.72/14.18 % (1164201)Termination phase: Saturation % 98.72/14.18 % (1164201)Time elapsed: 0.328 s % 98.72/14.18 % (1164201)Peak memory usage: 19 MB % 98.72/14.18 % (1164201)Instructions burned: 1475 (million) % 98.72/14.18 % (1164215)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=823927479:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 98.72/14.18 % (1164216)dis+21_1_sil=32000:sas=cadical:random_seed=1674435636:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 98.72/14.18 % (1164209)Instruction limit reached! % 98.72/14.18 % (1164209)------------------------------ % 98.72/14.18 % (1164209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.72/14.18 % (1164209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.72/14.18 % (1164209)CaDiCaL version: 2.1.3 % 98.72/14.18 % (1164209)Termination reason: Instruction limit % 98.72/14.18 % (1164209)Termination phase: Saturation % 98.72/14.18 % (1164209)Time elapsed: 0.439 s % 98.72/14.18 % (1164209)Peak memory usage: 19 MB % 98.72/14.18 % (1164209)Instructions burned: 869 (million) % 98.72/14.18 % (1164219)ott+11_1_sil=16000:gs=on:random_seed=448187304:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi) % 98.72/14.18 % (1164216)Instruction limit reached! % 98.72/14.18 % (1164216)------------------------------ % 98.72/14.18 % (1164216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.72/14.18 % (1164216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.72/14.18 % (1164216)CaDiCaL version: 2.1.3 % 98.72/14.18 % (1164216)Termination reason: Instruction limit % 98.72/14.18 % (1164216)Termination phase: Saturation % 98.72/14.18 % (1164216)Time elapsed: 0.836 s % 98.72/14.18 % (1164216)Peak memory usage: 22 MB % 98.72/14.18 % (1164216)Instructions burned: 3779 (million) % 98.72/14.18 % (1164221)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1546868621:fmbsr=1.6:i=67534_2983 on theBenchmark for (2983ds/67534Mi) % 98.72/14.18 % (1164221)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 98.72/14.18 % (1164221)Terminated due to inappropriate strategy. % 98.72/14.18 % (1164221)------------------------------ % 98.72/14.18 % (1164221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.72/14.18 % (1164221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.72/14.18 % (1164221)CaDiCaL version: 2.1.3 % 98.72/14.18 % (1164221)Termination reason: Inappropriate % 98.72/14.18 % (1164221)Time elapsed: 0.020 s % 98.72/14.18 % (1164221)Peak memory usage: 13 MB % 98.72/14.18 % (1164221)Instructions burned: 90 (million) % 98.72/14.18 % (1164221)------------------------------ % 98.72/14.18 % (1164221)------------------------------ % 98.72/14.18 % (1164223)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1305532738:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2983 on theBenchmark for (2983ds/4591Mi) % 98.72/14.18 % (1164219)Instruction limit reached! % 98.72/14.18 % (1164219)------------------------------ % 98.72/14.18 % (1164219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.72/14.18 % (1164219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.72/14.18 % (1164219)CaDiCaL version: 2.1.3 % 98.72/14.18 % (1164219)Termination reason: Instruction limit % 98.72/14.18 % (1164219)Termination phase: Saturation % 98.72/14.18 % (1164219)Time elapsed: 0.846 s % 98.72/14.18 % (1164219)Peak memory usage: 17 MB % 98.72/14.18 % (1164219)Instructions burned: 2252 (million) % 98.72/14.18 % (1164225)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1689267006:i=29340_2980 on theBenchmark for (2980ds/29340Mi) % 98.72/14.18 % (1164215)Instruction limit reached! % 98.72/14.18 % (1164215)------------------------------ % 98.72/14.18 % (1164215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.72/14.18 % (1164215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.72/14.18 % (1164215)CaDiCaL version: 2.1.3 % 98.72/14.18 % (1164215)Termination reason: Instruction limit % 110.95/15.92 % (1164215)Termination phase: Saturation % 110.95/15.92 % (1164215)Time elapsed: 1.663 s % 110.95/15.92 % (1164215)Peak memory usage: 25 MB % 110.95/15.92 % (1164215)Instructions burned: 3512 (million) % 110.95/15.92 % (1164227)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3870510536:i=5211_2975 on theBenchmark for (2975ds/5211Mi) % 110.95/15.92 % (1164223)Instruction limit reached! % 110.95/15.92 % (1164223)------------------------------ % 110.95/15.92 % (1164223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.95/15.92 % (1164223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.95/15.92 % (1164223)CaDiCaL version: 2.1.3 % 110.95/15.92 % (1164223)Termination reason: Instruction limit % 110.95/15.92 % (1164223)Termination phase: Saturation % 110.95/15.92 % (1164223)Time elapsed: 1.287 s % 110.95/15.92 % (1164223)Peak memory usage: 37 MB % 110.95/15.92 % (1164223)Instructions burned: 4593 (million) % 110.95/15.92 % (1164229)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2561505856:i=5497:nm=2_2970 on theBenchmark for (2970ds/5497Mi) % 110.95/15.92 % (1164229)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.95/15.92 % (1164229)Terminated due to inappropriate strategy. % 110.95/15.92 % (1164229)------------------------------ % 110.95/15.92 % (1164229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.95/15.92 % (1164229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.95/15.92 % (1164229)CaDiCaL version: 2.1.3 % 110.95/15.92 % (1164229)Termination reason: Inappropriate % 110.95/15.92 % (1164229)Time elapsed: 0.015 s % 110.95/15.92 % (1164229)Peak memory usage: 12 MB % 110.95/15.92 % (1164229)Instructions burned: 67 (million) % 110.95/15.92 % (1164229)------------------------------ % 110.95/15.92 % (1164229)------------------------------ % 110.95/15.92 % (1164231)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2835288138:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 110.95/15.92 % (1164231)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.95/15.92 % (1164231)Terminated due to inappropriate strategy. % 110.95/15.92 % (1164231)------------------------------ % 110.95/15.92 % (1164231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.95/15.92 % (1164231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.95/15.92 % (1164231)CaDiCaL version: 2.1.3 % 110.95/15.92 % (1164231)Termination reason: Inappropriate % 110.95/15.92 % (1164231)Time elapsed: 0.020 s % 110.95/15.92 % (1164231)Peak memory usage: 13 MB % 110.95/15.92 % (1164231)Instructions burned: 93 (million) % 110.95/15.92 % (1164231)------------------------------ % 110.95/15.92 % (1164231)------------------------------ % 110.95/15.92 % (1164233)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=619696211:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 110.95/15.92 % (1164233)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 110.95/15.92 % (1164233)Terminated due to inappropriate strategy. % 110.95/15.92 % (1164233)------------------------------ % 110.95/15.92 % (1164233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.95/15.92 % (1164233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.95/15.92 % (1164233)CaDiCaL version: 2.1.3 % 110.95/15.92 % (1164233)Termination reason: Inappropriate % 110.95/15.92 % (1164233)Time elapsed: 0.020 s % 110.95/15.92 % (1164233)Peak memory usage: 13 MB % 110.95/15.92 % (1164233)Instructions burned: 93 (million) % 110.95/15.92 % (1164233)------------------------------ % 110.95/15.92 % (1164233)------------------------------ % 110.95/15.92 % (1164235)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2172876484:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi) % 110.95/15.92 % (1164200)Instruction limit reached! % 110.95/15.92 % (1164200)------------------------------ % 110.95/15.92 % (1164200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 110.95/15.92 % (1164200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.95/15.92 % (1164200)CaDiCaL version: 2.1.3 % 110.95/15.92 % (1164200)Termination reason: Instruction limit % 110.95/15.92 % (1164200)Termination phase: Saturation % 110.95/15.92 % (1164200)Time elapsed: 2.690 s % 110.95/15.92 % (1164200)Peak memory usage: 41 MB % 110.95/15.92 % (1164200)Instructions burned: 5133 (million) % 110.95/15.92 % (1164237)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3448289153:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 110.95/15.92 % (1164211)Instruction limit reached! % 113.34/16.20 % (1164211)------------------------------ % 113.34/16.20 % (1164211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.34/16.20 % (1164211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.34/16.20 % (1164211)CaDiCaL version: 2.1.3 % 113.34/16.20 % (1164211)Termination reason: Instruction limit % 113.34/16.20 % (1164211)Termination phase: Saturation % 113.34/16.20 % (1164211)Time elapsed: 3.039 s % 113.34/16.20 % (1164211)Peak memory usage: 32 MB % 113.34/16.20 % (1164211)Instructions burned: 5116 (million) % 113.34/16.20 % (1164239)dis+10_16:1_sil=16000:random_seed=4048193712:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 113.34/16.20 % (1164227)Instruction limit reached! % 113.34/16.20 % (1164227)------------------------------ % 113.34/16.20 % (1164227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.34/16.20 % (1164227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.34/16.20 % (1164227)CaDiCaL version: 2.1.3 % 113.34/16.20 % (1164227)Termination reason: Instruction limit % 113.34/16.20 % (1164227)Termination phase: Saturation % 113.34/16.20 % (1164227)Time elapsed: 2.710 s % 113.34/16.20 % (1164227)Peak memory usage: 44 MB % 113.34/16.20 % (1164227)Instructions burned: 5211 (million) % 113.34/16.20 % (1164241)ott-3_8_sil=64000:random_seed=1259367337:i=20139:bs=on_2947 on theBenchmark for (2947ds/20139Mi) % 113.34/16.20 % (1164237)Instruction limit reached! % 113.34/16.20 % (1164237)------------------------------ % 113.34/16.20 % (1164237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.34/16.20 % (1164237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.34/16.20 % (1164237)CaDiCaL version: 2.1.3 % 113.34/16.20 % (1164237)Termination reason: Instruction limit % 113.34/16.20 % (1164237)Termination phase: Saturation % 113.34/16.20 % (1164237)Time elapsed: 3.731 s % 113.34/16.20 % (1164237)Peak memory usage: 35 MB % 113.34/16.20 % (1164237)Instructions burned: 8174 (million) % 113.34/16.20 % (1164243)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2911893109:fmbsr=2:i=32576_2930 on theBenchmark for (2930ds/32576Mi) % 113.34/16.20 % (1164243)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 113.34/16.20 % (1164243)Terminated due to inappropriate strategy. % 113.34/16.20 % (1164243)------------------------------ % 113.34/16.20 % (1164243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.34/16.20 % (1164243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.34/16.20 % (1164243)CaDiCaL version: 2.1.3 % 113.34/16.20 % (1164243)Termination reason: Inappropriate % 113.34/16.20 % (1164243)Time elapsed: 0.038 s % 113.34/16.20 % (1164243)Peak memory usage: 13 MB % 113.34/16.20 % (1164243)Instructions burned: 90 (million) % 113.34/16.20 % (1164243)------------------------------ % 113.34/16.20 % (1164243)------------------------------ % 113.34/16.20 % (1164245)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1766976201:i=11404_2930 on theBenchmark for (2930ds/11404Mi) % 113.34/16.20 % (1164239)Instruction limit reached! % 113.34/16.20 % (1164239)------------------------------ % 113.34/16.20 % (1164239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.34/16.20 % (1164239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.34/16.20 % (1164239)CaDiCaL version: 2.1.3 % 113.34/16.20 % (1164239)Termination reason: Instruction limit % 113.34/16.20 % (1164239)Termination phase: Saturation % 113.34/16.20 % (1164239)Time elapsed: 4.695 s % 113.34/16.20 % (1164239)Peak memory usage: 48 MB % 113.34/16.20 % (1164239)Instructions burned: 9155 (million) % 113.34/16.20 % (1164247)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3615283580:i=14134_2915 on theBenchmark for (2915ds/14134Mi) % 113.34/16.20 % (1164235)Instruction limit reached! % 113.34/16.20 % (1164235)------------------------------ % 113.34/16.20 % (1164235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.34/16.20 % (1164235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.34/16.20 % (1164235)CaDiCaL version: 2.1.3 % 113.34/16.20 % (1164235)Termination reason: Instruction limit % 113.34/16.20 % (1164235)Termination phase: Saturation % 113.34/16.20 % (1164235)Time elapsed: 7.186 s % 113.34/16.20 % (1164235)Peak memory usage: 280 MB % 113.34/16.20 % (1164235)Instructions burned: 22567 (million) % 113.34/16.20 % (1164249)dis+33_16_sil=32000:sac=on:random_seed=2745098470:i=15851:nm=0_2897 on theBenchmark for (2897ds/15851Mi) % 113.34/16.20 % (1164249)Instruction limit reached! % 113.34/16.20 % (1164249)------------------------------ % 113.34/16.20 % (1164249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.57/20.08 % (1164249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.57/20.08 % (1164249)CaDiCaL version: 2.1.3 % 140.57/20.08 % (1164249)Termination reason: Instruction limit % 140.57/20.08 % (1164249)Termination phase: Saturation % 140.57/20.08 % (1164249)Time elapsed: 3.671 s % 140.57/20.08 % (1164249)Peak memory usage: 35 MB % 140.57/20.08 % (1164249)Instructions burned: 15851 (million) % 140.57/20.08 % (1164251)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1810840665:avsq=on:i=17627:add=on:amm=off_2860 on theBenchmark for (2860ds/17627Mi) % 140.57/20.08 % (1164245)Instruction limit reached! % 140.57/20.08 % (1164245)------------------------------ % 140.57/20.08 % (1164245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.57/20.08 % (1164245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.57/20.08 % (1164245)CaDiCaL version: 2.1.3 % 140.57/20.08 % (1164245)Termination reason: Instruction limit % 140.57/20.08 % (1164245)Termination phase: Saturation % 140.57/20.08 % (1164245)Time elapsed: 7.268 s % 140.57/20.08 % (1164245)Peak memory usage: 47 MB % 140.57/20.08 % (1164245)Instructions burned: 11404 (million) % 140.57/20.08 % (1164253)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1494492884:s2a=on:i=53295_2857 on theBenchmark for (2857ds/53295Mi) % 140.57/20.08 % (1164247)Instruction limit reached! % 140.57/20.08 % (1164247)------------------------------ % 140.57/20.08 % (1164247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.57/20.08 % (1164247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.57/20.08 % (1164247)CaDiCaL version: 2.1.3 % 140.57/20.08 % (1164247)Termination reason: Instruction limit % 140.57/20.08 % (1164247)Termination phase: Saturation % 140.57/20.08 % (1164247)Time elapsed: 6.972 s % 140.57/20.08 % (1164247)Peak memory usage: 49 MB % 140.57/20.08 % (1164247)Instructions burned: 14135 (million) % 140.57/20.08 % (1164255)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=972389114:i=26857:ins=20_2845 on theBenchmark for (2845ds/26857Mi) % 140.57/20.08 % (1164255)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 140.57/20.08 % (1164255)Terminated due to inappropriate strategy. % 140.57/20.08 % (1164255)------------------------------ % 140.57/20.08 % (1164255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.57/20.08 % (1164255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.57/20.08 % (1164255)CaDiCaL version: 2.1.3 % 140.57/20.08 % (1164255)Termination reason: Inappropriate % 140.57/20.08 % (1164255)Time elapsed: 0.029 s % 140.57/20.08 % (1164255)Peak memory usage: 12 MB % 140.57/20.08 % (1164255)Instructions burned: 67 (million) % 140.57/20.08 % (1164255)------------------------------ % 140.57/20.08 % (1164255)------------------------------ % 140.57/20.08 % (1164257)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4059004857:i=28120:bs=on:fsr=off_2845 on theBenchmark for (2845ds/28120Mi) % 140.57/20.08 % (1164225)Instruction limit reached! % 140.57/20.08 % (1164225)------------------------------ % 140.57/20.08 % (1164225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.57/20.08 % (1164225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.57/20.08 % (1164225)CaDiCaL version: 2.1.3 % 140.57/20.08 % (1164225)Termination reason: Instruction limit % 140.57/20.08 % (1164225)Termination phase: Saturation % 140.57/20.08 % (1164225)Time elapsed: 13.703 s % 140.57/20.08 % (1164225)Peak memory usage: 39 MB % 140.57/20.08 % (1164225)Instructions burned: 29341 (million) % 140.57/20.08 % (1164259)fmb+10_1_sil=256000:fmbss=7:random_seed=3635867715:fmbsr=1.6:i=182295_2843 on theBenchmark for (2843ds/182295Mi) % 140.57/20.08 % (1164259)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 140.57/20.08 % (1164259)Terminated due to inappropriate strategy. % 140.57/20.08 % (1164259)------------------------------ % 140.57/20.08 % (1164259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.57/20.08 % (1164259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.57/20.08 % (1164259)CaDiCaL version: 2.1.3 % 140.57/20.08 % (1164259)Termination reason: Inappropriate % 140.57/20.08 % (1164259)Time elapsed: 0.029 s % 140.57/20.08 % (1164259)Peak memory usage: 12 MB % 140.57/20.08 % (1164259)Instructions burned: 67 (million) % 140.57/20.08 % (1164259)------------------------------ % 140.57/20.08 % (1164259)------------------------------ % 140.57/20.08 % (1164261)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3971359963:i=44625:gsp=on_2843 on theBenchmark for (2843ds/44625Mi) % 146.46/20.95 % (1164261)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.46/20.95 % (1164261)Terminated due to inappropriate strategy. % 146.46/20.95 % (1164261)------------------------------ % 146.46/20.95 % (1164261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.46/20.95 % (1164261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.46/20.95 % (1164261)CaDiCaL version: 2.1.3 % 146.46/20.95 % (1164261)Termination reason: Inappropriate % 146.46/20.95 % (1164261)Time elapsed: 0.032 s % 146.46/20.95 % (1164261)Peak memory usage: 13 MB % 146.46/20.95 % (1164261)Instructions burned: 70 (million) % 146.46/20.95 % (1164261)------------------------------ % 146.46/20.95 % (1164261)------------------------------ % 146.46/20.95 % (1164263)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1016417910:i=160505_2842 on theBenchmark for (2842ds/160505Mi) % 146.46/20.95 % (1164263)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.46/20.95 % (1164263)Terminated due to inappropriate strategy. % 146.46/20.95 % (1164263)------------------------------ % 146.46/20.95 % (1164263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.46/20.95 % (1164263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.46/20.95 % (1164263)CaDiCaL version: 2.1.3 % 146.46/20.95 % (1164263)Termination reason: Inappropriate % 146.46/20.95 % (1164263)Time elapsed: 0.029 s % 146.46/20.95 % (1164263)Peak memory usage: 12 MB % 146.46/20.95 % (1164263)Instructions burned: 67 (million) % 146.46/20.95 % (1164263)------------------------------ % 146.46/20.95 % (1164263)------------------------------ % 146.46/20.95 % (1164265)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3174852769:fmbsr=1.3:i=225729_2841 on theBenchmark for (2841ds/225729Mi) % 146.46/20.95 % (1164265)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.46/20.95 % (1164265)Terminated due to inappropriate strategy. % 146.46/20.95 % (1164265)------------------------------ % 146.46/20.95 % (1164265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.46/20.95 % (1164265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.46/20.95 % (1164265)CaDiCaL version: 2.1.3 % 146.46/20.95 % (1164265)Termination reason: Inappropriate % 146.46/20.95 % (1164265)Time elapsed: 0.039 s % 146.46/20.95 % (1164265)Peak memory usage: 13 MB % 146.46/20.95 % (1164265)Instructions burned: 93 (million) % 146.46/20.95 % (1164265)------------------------------ % 146.46/20.95 % (1164265)------------------------------ % 146.46/20.95 % (1164267)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1415495344:fmbsr=2:i=185024:ins=7_2841 on theBenchmark for (2841ds/185024Mi) % 146.46/20.95 % (1164267)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.46/20.95 % (1164267)Terminated due to inappropriate strategy. % 146.46/20.95 % (1164267)------------------------------ % 146.46/20.95 % (1164267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.46/20.95 % (1164267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.46/20.95 % (1164267)CaDiCaL version: 2.1.3 % 146.46/20.95 % (1164267)Termination reason: Inappropriate % 146.46/20.95 % (1164267)Time elapsed: 0.039 s % 146.46/20.95 % (1164267)Peak memory usage: 13 MB % 146.46/20.95 % (1164267)Instructions burned: 93 (million) % 146.46/20.95 % (1164267)------------------------------ % 146.46/20.95 % (1164267)------------------------------ % 146.46/20.95 % (1164269)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1608615520:rtra=on_2840 on theBenchmark for (2840ds/0Mi) % 146.46/20.95 % (1164269)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 146.46/20.95 % (1164269)Terminated due to inappropriate strategy. % 146.46/20.95 % (1164269)------------------------------ % 146.46/20.95 % (1164269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.46/20.95 % (1164269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.46/20.95 % (1164269)CaDiCaL version: 2.1.3 % 146.46/20.95 % (1164269)Termination reason: Inappropriate % 146.46/20.95 % (1164269)Time elapsed: 0.038 s % 146.46/20.95 % (1164269)Peak memory usage: 14 MB % 146.46/20.95 % (1164269)Instructions burned: 79 (million) % 146.46/20.95 % (1164269)------------------------------ % 146.46/20.95 % (1164269)------------------------------ % 146.46/20.95 % (1164271)% WARNING: option uhcvi not known. % 146.46/20.95 % (1164271)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=588227049:i=271062:add=off:rtra=on:rawr=on_2840 on theBenchmark for (2840ds/271062Mi) % 158.97/22.77 % (1164241)Instruction limit reached! % 158.97/22.77 % (1164241)------------------------------ % 158.97/22.77 % (1164241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.97/22.77 % (1164241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.97/22.77 % (1164241)CaDiCaL version: 2.1.3 % 158.97/22.77 % (1164241)Termination reason: Instruction limit % 158.97/22.77 % (1164241)Termination phase: Saturation % 158.97/22.77 % (1164241)Time elapsed: 10.947 s % 158.97/22.77 % (1164241)Peak memory usage: 58 MB % 158.97/22.77 % (1164241)Instructions burned: 20140 (million) % 158.97/22.77 % (1164273)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1063152790:i=176048:add=on:rtra=on:rawr=on_2838 on theBenchmark for (2838ds/176048Mi) % 158.97/22.77 % (1164251)Instruction limit reached! % 158.97/22.77 % (1164251)------------------------------ % 158.97/22.77 % (1164251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.97/22.77 % (1164251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.97/22.77 % (1164251)CaDiCaL version: 2.1.3 % 158.97/22.77 % (1164251)Termination reason: Instruction limit % 158.97/22.77 % (1164251)Termination phase: Saturation % 158.97/22.77 % (1164251)Time elapsed: 5.544 s % 158.97/22.77 % (1164251)Peak memory usage: 142 MB % 158.97/22.77 % (1164251)Instructions burned: 17629 (million) % 158.97/22.77 % (1164277)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3834272618:i=206:fgj=on:rtra=on_2804 on theBenchmark for (2804ds/206Mi) % 158.97/22.77 % (1164277)Instruction limit reached! % 158.97/22.77 % (1164277)------------------------------ % 158.97/22.77 % (1164277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.97/22.77 % (1164277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.97/22.77 % (1164277)CaDiCaL version: 2.1.3 % 158.97/22.77 % (1164277)Termination reason: Instruction limit % 158.97/22.77 % (1164277)Termination phase: Saturation % 158.97/22.77 % (1164277)Time elapsed: 0.057 s % 158.97/22.77 % (1164277)Peak memory usage: 16 MB % 158.97/22.77 % (1164277)Instructions burned: 208 (million) % 158.97/22.77 % (1164279)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3141201817:i=232:rtra=on_2803 on theBenchmark for (2803ds/232Mi) % 158.97/22.77 % (1164279)Instruction limit reached! % 158.97/22.77 % (1164279)------------------------------ % 158.97/22.77 % (1164279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.97/22.77 % (1164279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.97/22.77 % (1164279)CaDiCaL version: 2.1.3 % 158.97/22.77 % (1164279)Termination reason: Instruction limit % 158.97/22.77 % (1164279)Termination phase: Saturation % 158.97/22.77 % (1164279)Time elapsed: 0.060 s % 158.97/22.77 % (1164279)Peak memory usage: 16 MB % 158.97/22.77 % (1164279)Instructions burned: 235 (million) % 158.97/22.77 % (1164281)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3157998007:i=262:rtra=on_2803 on theBenchmark for (2803ds/262Mi) % 158.97/22.77 % (1164281)Instruction limit reached! % 158.97/22.77 % (1164281)------------------------------ % 158.97/22.77 % (1164281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.97/22.77 % (1164281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.97/22.77 % (1164281)CaDiCaL version: 2.1.3 % 158.97/22.77 % (1164281)Termination reason: Instruction limit % 158.97/22.77 % (1164281)Termination phase: Saturation % 158.97/22.77 % (1164281)Time elapsed: 0.061 s % 158.97/22.77 % (1164281)Peak memory usage: 16 MB % 158.97/22.77 % (1164281)Instructions burned: 264 (million) % 158.97/22.77 % (1164283)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1448396425:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2802 on theBenchmark for (2802ds/318Mi) % 158.97/22.77 % (1164283)Instruction limit reached! % 158.97/22.77 % (1164283)------------------------------ % 158.97/22.77 % (1164283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.97/22.77 % (1164283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.97/22.77 % (1164283)CaDiCaL version: 2.1.3 % 158.97/22.77 % (1164283)Termination reason: Instruction limit % 158.97/22.77 % (1164283)Termination phase: Saturation % 158.97/22.77 % (1164283)Time elapsed: 0.092 s % 158.97/22.77 % (1164283)Peak memory usage: 18 MB % 158.97/22.77 % (1164283)Instructions burned: 321 (million) % 158.97/22.77 % (1164285)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2596951103:i=1428:nm=2:rtra=on_2801 on theBenchmark for (2801ds/1428Mi) % 188.62/26.88 % (1164285)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 188.62/26.88 % (1164285)Terminated due to inappropriate strategy. % 188.62/26.88 % (1164285)------------------------------ % 188.62/26.88 % (1164285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.62/26.88 % (1164285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.62/26.88 % (1164285)CaDiCaL version: 2.1.3 % 188.62/26.88 % (1164285)Termination reason: Inappropriate % 188.62/26.88 % (1164285)Time elapsed: 0.020 s % 188.62/26.88 % (1164285)Peak memory usage: 14 MB % 188.62/26.88 % (1164285)Instructions burned: 79 (million) % 188.62/26.88 % (1164285)------------------------------ % 188.62/26.88 % (1164285)------------------------------ % 188.62/26.88 % (1164287)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3700869209:i=262:bd=preordered:rtra=on:fsd=on_2801 on theBenchmark for (2801ds/262Mi) % 188.62/26.88 % (1164287)Instruction limit reached! % 188.62/26.88 % (1164287)------------------------------ % 188.62/26.88 % (1164287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.62/26.88 % (1164287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.62/26.88 % (1164287)CaDiCaL version: 2.1.3 % 188.62/26.88 % (1164287)Termination reason: Instruction limit % 188.62/26.88 % (1164287)Termination phase: Saturation % 188.62/26.88 % (1164287)Time elapsed: 0.063 s % 188.62/26.88 % (1164287)Peak memory usage: 16 MB % 188.62/26.88 % (1164287)Instructions burned: 265 (million) % 188.62/26.88 % (1164289)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=36629539:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2800 on theBenchmark for (2800ds/1368Mi) % 188.62/26.88 % (1164289)Instruction limit reached! % 188.62/26.88 % (1164289)------------------------------ % 188.62/26.88 % (1164289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.62/26.88 % (1164289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.62/26.88 % (1164289)CaDiCaL version: 2.1.3 % 188.62/26.88 % (1164289)Termination reason: Instruction limit % 188.62/26.88 % (1164289)Termination phase: Saturation % 188.62/26.88 % (1164289)Time elapsed: 0.349 s % 188.62/26.88 % (1164289)Peak memory usage: 19 MB % 188.62/26.88 % (1164289)Instructions burned: 1370 (million) % 188.62/26.88 % (1164291)ott-21_1_sil=16000:si=on:fs=off:random_seed=2186857786:i=360:av=off:fsr=off:rtra=on_2796 on theBenchmark for (2796ds/360Mi) % 188.62/26.88 % (1164291)Instruction limit reached! % 188.62/26.88 % (1164291)------------------------------ % 188.62/26.88 % (1164291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.62/26.88 % (1164291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.62/26.88 % (1164291)CaDiCaL version: 2.1.3 % 188.62/26.88 % (1164291)Termination reason: Instruction limit % 188.62/26.88 % (1164291)Termination phase: Saturation % 188.62/26.88 % (1164291)Time elapsed: 0.093 s % 188.62/26.88 % (1164291)Peak memory usage: 16 MB % 188.62/26.88 % (1164291)Instructions burned: 361 (million) % 188.62/26.88 % (1164293)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3147761983:i=954:bd=all:rtra=on_2795 on theBenchmark for (2795ds/954Mi) % 188.62/26.88 % (1164293)Instruction limit reached! % 188.62/26.88 % (1164293)------------------------------ % 188.62/26.88 % (1164293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.62/26.88 % (1164293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.62/26.88 % (1164293)CaDiCaL version: 2.1.3 % 188.62/26.88 % (1164293)Termination reason: Instruction limit % 188.62/26.88 % (1164293)Termination phase: Saturation % 188.62/26.88 % (1164293)Time elapsed: 0.266 s % 188.62/26.88 % (1164293)Peak memory usage: 18 MB % 188.62/26.88 % (1164293)Instructions burned: 955 (million) % 188.62/26.88 % (1164295)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2375606554:fmbsr=1.3:i=1730:ins=25:rtra=on_2792 on theBenchmark for (2792ds/1730Mi) % 188.62/26.88 % (1164295)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 188.62/26.88 % (1164295)Terminated due to inappropriate strategy. % 188.62/26.88 % (1164295)------------------------------ % 188.62/26.88 % (1164295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.62/26.88 % (1164295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.62/26.88 % (1164295)CaDiCaL version: 2.1.3 % 188.62/26.88 % (1164295)Termination reason: Inappropriate % 219.42/31.17 % (1164295)Time elapsed: 0.020 s % 219.42/31.17 % (1164295)Peak memory usage: 14 MB % 219.42/31.17 % (1164295)Instructions burned: 78 (million) % 219.42/31.17 % (1164295)------------------------------ % 219.42/31.17 % (1164295)------------------------------ % 219.42/31.17 % (1164297)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2814455284:i=2358:rtra=on_2792 on theBenchmark for (2792ds/2358Mi) % 219.42/31.17 % (1164297)Instruction limit reached! % 219.42/31.17 % (1164297)------------------------------ % 219.42/31.17 % (1164297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.42/31.17 % (1164297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.42/31.17 % (1164297)CaDiCaL version: 2.1.3 % 219.42/31.17 % (1164297)Termination reason: Instruction limit % 219.42/31.17 % (1164297)Termination phase: Saturation % 219.42/31.17 % (1164297)Time elapsed: 0.740 s % 219.42/31.17 % (1164297)Peak memory usage: 25 MB % 219.42/31.17 % (1164297)Instructions burned: 2358 (million) % 219.42/31.17 % (1164299)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1977758949:i=1778:ins=1:rtra=on_2784 on theBenchmark for (2784ds/1778Mi) % 219.42/31.17 % (1164299)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 219.42/31.17 % (1164299)Terminated due to inappropriate strategy. % 219.42/31.17 % (1164299)------------------------------ % 219.42/31.17 % (1164299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.42/31.17 % (1164299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.42/31.17 % (1164299)CaDiCaL version: 2.1.3 % 219.42/31.17 % (1164299)Termination reason: Inappropriate % 219.42/31.17 % (1164299)Time elapsed: 0.027 s % 219.42/31.17 % (1164299)Peak memory usage: 15 MB % 219.42/31.17 % (1164299)Instructions burned: 105 (million) % 219.42/31.17 % (1164299)------------------------------ % 219.42/31.17 % (1164299)------------------------------ % 219.42/31.17 % (1164301)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=2948960772:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2784 on theBenchmark for (2784ds/1384Mi) % 219.42/31.17 % (1164301)Instruction limit reached! % 219.42/31.17 % (1164301)------------------------------ % 219.42/31.17 % (1164301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.42/31.17 % (1164301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.42/31.17 % (1164301)CaDiCaL version: 2.1.3 % 219.42/31.17 % (1164301)Termination reason: Instruction limit % 219.42/31.17 % (1164301)Termination phase: Saturation % 219.42/31.17 % (1164301)Time elapsed: 0.412 s % 219.42/31.17 % (1164301)Peak memory usage: 22 MB % 219.42/31.17 % (1164301)Instructions burned: 1385 (million) % 219.42/31.17 % (1164303)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1919108028:i=1758:kws=inv_precedence:fsr=off:rtra=on_2780 on theBenchmark for (2780ds/1758Mi) % 219.42/31.17 % (1164303)Instruction limit reached! % 219.42/31.17 % (1164303)------------------------------ % 219.42/31.17 % (1164303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.42/31.17 % (1164303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.42/31.17 % (1164303)CaDiCaL version: 2.1.3 % 219.42/31.17 % (1164303)Termination reason: Instruction limit % 219.42/31.17 % (1164303)Termination phase: Saturation % 219.42/31.17 % (1164303)Time elapsed: 0.535 s % 219.42/31.17 % (1164303)Peak memory usage: 28 MB % 219.42/31.17 % (1164303)Instructions burned: 1758 (million) % 219.42/31.17 % (1164305)fmb+10_1_sil=64000:si=on:random_seed=3310607126:i=44122:nm=2:rtra=on:gsp=on_2774 on theBenchmark for (2774ds/44122Mi) % 219.42/31.17 % (1164305)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 219.42/31.17 % (1164305)Terminated due to inappropriate strategy. % 219.42/31.17 % (1164305)------------------------------ % 219.42/31.17 % (1164305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.42/31.17 % (1164305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.42/31.17 % (1164305)CaDiCaL version: 2.1.3 % 219.42/31.17 % (1164305)Termination reason: Inappropriate % 219.42/31.17 % (1164305)Time elapsed: 0.022 s % 219.42/31.17 % (1164305)Peak memory usage: 14 MB % 219.42/31.17 % (1164305)Instructions burned: 85 (million) % 219.42/31.17 % (1164305)------------------------------ % 219.42/31.17 % (1164305)------------------------------ % 219.42/31.17 % (1164307)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2347341408:i=19030:nm=5:rtra=on_2774 on theBenchmark for (2774ds/19030Mi) % 247.81/35.19 % (1164307)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 247.81/35.19 % (1164307)Terminated due to inappropriate strategy. % 247.81/35.19 % (1164307)------------------------------ % 247.81/35.19 % (1164307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.81/35.19 % (1164307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.81/35.19 % (1164307)CaDiCaL version: 2.1.3 % 247.81/35.19 % (1164307)Termination reason: Inappropriate % 247.81/35.19 % (1164307)Time elapsed: 0.020 s % 247.81/35.19 % (1164307)Peak memory usage: 14 MB % 247.81/35.19 % (1164307)Instructions burned: 78 (million) % 247.81/35.19 % (1164307)------------------------------ % 247.81/35.19 % (1164307)------------------------------ % 247.81/35.19 % (1164309)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1250341375:fmbsr=1.7:i=1840:rtra=on_2774 on theBenchmark for (2774ds/1840Mi) % 247.81/35.19 % (1164309)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 247.81/35.19 % (1164309)Terminated due to inappropriate strategy. % 247.81/35.19 % (1164309)------------------------------ % 247.81/35.19 % (1164309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.81/35.19 % (1164309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.81/35.19 % (1164309)CaDiCaL version: 2.1.3 % 247.81/35.19 % (1164309)Termination reason: Inappropriate % 247.81/35.19 % (1164309)Time elapsed: 0.020 s % 247.81/35.19 % (1164309)Peak memory usage: 14 MB % 247.81/35.19 % (1164309)Instructions burned: 78 (million) % 247.81/35.19 % (1164309)------------------------------ % 247.81/35.19 % (1164309)------------------------------ % 247.81/35.19 % (1164311)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=446837340:i=10262:rtra=on_2773 on theBenchmark for (2773ds/10262Mi) % 247.81/35.19 % (1164311)Instruction limit reached! % 247.81/35.19 % (1164311)------------------------------ % 247.81/35.19 % (1164311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.81/35.19 % (1164311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.81/35.19 % (1164311)CaDiCaL version: 2.1.3 % 247.81/35.19 % (1164311)Termination reason: Instruction limit % 247.81/35.19 % (1164311)Termination phase: Saturation % 247.81/35.19 % (1164311)Time elapsed: 3.152 s % 247.81/35.19 % (1164311)Peak memory usage: 66 MB % 247.81/35.19 % (1164311)Instructions burned: 10264 (million) % 247.81/35.19 % (1164313)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3266502198:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2742 on theBenchmark for (2742ds/2944Mi) % 247.81/35.19 % (1164313)Instruction limit reached! % 247.81/35.19 % (1164313)------------------------------ % 247.81/35.19 % (1164313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.81/35.19 % (1164313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.81/35.19 % (1164313)CaDiCaL version: 2.1.3 % 247.81/35.19 % (1164313)Termination reason: Instruction limit % 247.81/35.19 % (1164313)Termination phase: Saturation % 247.81/35.19 % (1164313)Time elapsed: 0.805 s % 247.81/35.19 % (1164313)Peak memory usage: 28 MB % 247.81/35.19 % (1164313)Instructions burned: 2947 (million) % 247.81/35.19 % (1164315)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3016471655:i=12648:rtra=on_2733 on theBenchmark for (2733ds/12648Mi) % 247.81/35.19 % (1164315)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 247.81/35.19 % (1164315)Terminated due to inappropriate strategy. % 247.81/35.19 % (1164315)------------------------------ % 247.81/35.19 % (1164315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.81/35.19 % (1164315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.81/35.19 % (1164315)CaDiCaL version: 2.1.3 % 247.81/35.19 % (1164315)Termination reason: Inappropriate % 247.81/35.19 % (1164315)Time elapsed: 0.020 s % 247.81/35.19 % (1164315)Peak memory usage: 14 MB % 247.81/35.19 % (1164315)Instructions burned: 79 (million) % 247.81/35.19 % (1164315)------------------------------ % 247.81/35.19 % (1164315)------------------------------ % 247.81/35.19 % (1164317)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1126756948:fmbsr=2.30978:i=4348:rtra=on_2733 on theBenchmark for (2733ds/4348Mi) % 247.81/35.19 % (1164317)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 247.81/35.19 % (1164317)Terminated due to inappropriate strategy. % 247.81/35.19 % (1164317)--------------------Terminated % 300.05/42.54 % Vampire exiting %------------------------------------------------------------------------------