%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX106_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:46:30 PM UTC 2026 % Result : Timeout 300.99s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX106_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.17 % Computer : n009.cluster.edu % 0.07/0.17 % Model : x86_64 x86_64 % 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.17 % Memory : 8046.5625MB % 0.07/0.17 % OS : Linux 6.8.0-71-generic % 0.07/0.17 % CPULimit : 300 % 0.07/0.17 % WCLimit : 300 % 0.07/0.17 % DateTime : Mon Sep 28 15:01:45 UTC 2026 % 0.07/0.17 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.20 Running first-order model finding % 0.07/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 % 3.77/0.83 % (3126576)Will run a generic schedule for satisfiability detection. % 3.77/0.83 % (3126602)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=428663731:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.77/0.83 % (3126598)% WARNING: option uhcvi not known. % 3.77/0.83 % (3126597)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=164448798_2999 on theBenchmark for (2999ds/0Mi) % 3.77/0.83 % (3126600)dis+10_1_sil=32000:sp=arity:random_seed=1994060489:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.77/0.83 % (3126599)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1850356419:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.77/0.83 % (3126598)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1790520047:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.77/0.83 % (3126601)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2434805963:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.77/0.83 % (3126603)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3033514562:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.77/0.83 % (3126597)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.77/0.83 % (3126597)Terminated due to inappropriate strategy. % 3.77/0.83 % (3126597)------------------------------ % 3.77/0.83 % (3126597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.77/0.83 % (3126597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.77/0.83 % (3126597)CaDiCaL version: 2.1.3 % 3.77/0.83 % (3126597)Termination reason: Inappropriate % 3.77/0.83 % (3126597)Time elapsed: 0.002 s % 3.77/0.83 % (3126597)Peak memory usage: 10 MB % 3.77/0.83 % (3126597)Instructions burned: 3 (million) % 3.77/0.83 % (3126597)------------------------------ % 3.77/0.83 % (3126597)------------------------------ % 3.77/0.83 % (3126617)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1121888972:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.77/0.83 % (3126617)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.77/0.83 % (3126617)Terminated due to inappropriate strategy. % 3.77/0.83 % (3126617)------------------------------ % 3.77/0.83 % (3126617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.77/0.83 % (3126617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.77/0.83 % (3126617)CaDiCaL version: 2.1.3 % 3.77/0.83 % (3126617)Termination reason: Inappropriate % 3.77/0.83 % (3126617)Time elapsed: 0.002 s % 3.77/0.83 % (3126617)Peak memory usage: 10 MB % 3.77/0.83 % (3126617)Instructions burned: 3 (million) % 3.77/0.83 % (3126617)------------------------------ % 3.77/0.83 % (3126617)------------------------------ % 3.77/0.83 % (3126602)Instruction limit reached! % 3.77/0.83 % (3126602)------------------------------ % 3.77/0.83 % (3126602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.77/0.83 % (3126602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.77/0.83 % (3126602)CaDiCaL version: 2.1.3 % 3.77/0.83 % (3126602)Termination reason: Instruction limit % 3.77/0.83 % (3126602)Termination phase: Saturation % 3.77/0.83 % (3126602)Time elapsed: 0.045 s % 3.77/0.83 % (3126602)Peak memory usage: 13 MB % 3.77/0.83 % (3126602)Instructions burned: 134 (million) % 3.77/0.83 % (3126633)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=3484200064:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.77/0.83 % (3126629)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=858145819:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.77/0.83 % (3126600)Instruction limit reached! % 3.77/0.83 % (3126600)------------------------------ % 3.77/0.83 % (3126600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.77/0.83 % (3126600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.77/0.83 % (3126600)CaDiCaL version: 2.1.3 % 3.77/0.83 % (3126600)Termination reason: Instruction limit % 3.77/0.83 % (3126600)Termination phase: Saturation % 3.77/0.83 % (3126600)Time elapsed: 0.068 s % 3.77/0.83 % (3126600)Peak memory usage: 13 MB % 3.77/0.83 % (3126600)Instructions burned: 104 (million) % 3.77/0.83 % (3126601)Instruction limit reached! % 3.77/0.83 % (3126601)------------------------------ % 3.77/0.83 % (3126601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.76/1.09 % (3126601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.76/1.09 % (3126601)CaDiCaL version: 2.1.3 % 5.76/1.09 % (3126601)Termination reason: Instruction limit % 5.76/1.09 % (3126601)Termination phase: Saturation % 5.76/1.09 % (3126601)Time elapsed: 0.071 s % 5.76/1.09 % (3126601)Peak memory usage: 12 MB % 5.76/1.09 % (3126601)Instructions burned: 116 (million) % 5.76/1.09 % (3126644)ott-21_1_sil=16000:fs=off:random_seed=3317867155:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.76/1.09 % (3126647)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3540328985:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.76/1.09 % (3126603)Instruction limit reached! % 5.76/1.09 % (3126603)------------------------------ % 5.76/1.09 % (3126603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.76/1.09 % (3126603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.76/1.09 % (3126603)CaDiCaL version: 2.1.3 % 5.76/1.09 % (3126603)Termination reason: Instruction limit % 5.76/1.09 % (3126603)Termination phase: Saturation % 5.76/1.09 % (3126603)Time elapsed: 0.115 s % 5.76/1.09 % (3126603)Peak memory usage: 14 MB % 5.76/1.09 % (3126603)Instructions burned: 159 (million) % 5.76/1.09 % (3126664)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=689700044:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.76/1.09 % (3126664)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.76/1.09 % (3126664)Terminated due to inappropriate strategy. % 5.76/1.09 % (3126664)------------------------------ % 5.76/1.09 % (3126664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.76/1.09 % (3126664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.76/1.09 % (3126664)CaDiCaL version: 2.1.3 % 5.76/1.09 % (3126664)Termination reason: Inappropriate % 5.76/1.09 % (3126664)Time elapsed: 0.001 s % 5.76/1.09 % (3126664)Peak memory usage: 10 MB % 5.76/1.09 % (3126664)Instructions burned: 2 (million) % 5.76/1.09 % (3126664)------------------------------ % 5.76/1.09 % (3126664)------------------------------ % 5.76/1.09 % (3126629)Instruction limit reached! % 5.76/1.09 % (3126629)------------------------------ % 5.76/1.09 % (3126629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.76/1.09 % (3126629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.76/1.09 % (3126629)CaDiCaL version: 2.1.3 % 5.76/1.09 % (3126629)Termination reason: Instruction limit % 5.76/1.09 % (3126629)Termination phase: Saturation % 5.76/1.09 % (3126629)Time elapsed: 0.089 s % 5.76/1.09 % (3126629)Peak memory usage: 13 MB % 5.76/1.09 % (3126629)Instructions burned: 131 (million) % 5.76/1.09 % (3126676)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3304583732:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.76/1.09 % (3126678)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1698243388:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.76/1.09 % (3126678)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.76/1.09 % (3126678)Terminated due to inappropriate strategy. % 5.76/1.09 % (3126678)------------------------------ % 5.76/1.09 % (3126678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.76/1.09 % (3126678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.76/1.09 % (3126678)CaDiCaL version: 2.1.3 % 5.76/1.09 % (3126678)Termination reason: Inappropriate % 5.76/1.09 % (3126678)Time elapsed: 0.002 s % 5.76/1.09 % (3126678)Peak memory usage: 10 MB % 5.76/1.09 % (3126678)Instructions burned: 3 (million) % 5.76/1.09 % (3126678)------------------------------ % 5.76/1.09 % (3126678)------------------------------ % 5.76/1.09 % (3126644)Instruction limit reached! % 5.76/1.09 % (3126644)------------------------------ % 5.76/1.09 % (3126644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.76/1.09 % (3126644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.76/1.09 % (3126644)CaDiCaL version: 2.1.3 % 5.76/1.09 % (3126644)Termination reason: Instruction limit % 5.76/1.09 % (3126644)Termination phase: Saturation % 5.76/1.09 % (3126644)Time elapsed: 0.084 s % 5.76/1.09 % (3126644)Peak memory usage: 12 MB % 5.76/1.09 % (3126644)Instructions burned: 181 (million) % 5.76/1.09 % (3126695)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=2135328874: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) % 19.95/3.04 % (3126703)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=904039084:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 19.95/3.04 % (3126633)Instruction limit reached! % 19.95/3.04 % (3126633)------------------------------ % 19.95/3.04 % (3126633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.95/3.04 % (3126633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.95/3.04 % (3126633)CaDiCaL version: 2.1.3 % 19.95/3.04 % (3126633)Termination reason: Instruction limit % 19.95/3.04 % (3126633)Termination phase: Saturation % 19.95/3.04 % (3126633)Time elapsed: 0.236 s % 19.95/3.04 % (3126633)Peak memory usage: 18 MB % 19.95/3.04 % (3126633)Instructions burned: 693 (million) % 19.95/3.04 % (3126716)fmb+10_1_sil=64000:random_seed=783073003:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 19.95/3.04 % (3126716)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.95/3.04 % (3126716)Terminated due to inappropriate strategy. % 19.95/3.04 % (3126716)------------------------------ % 19.95/3.04 % (3126716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.95/3.04 % (3126716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.95/3.04 % (3126716)CaDiCaL version: 2.1.3 % 19.95/3.04 % (3126716)Termination reason: Inappropriate % 19.95/3.04 % (3126716)Time elapsed: 0.001 s % 19.95/3.04 % (3126716)Peak memory usage: 10 MB % 19.95/3.04 % (3126716)Instructions burned: 3 (million) % 19.95/3.04 % (3126716)------------------------------ % 19.95/3.04 % (3126716)------------------------------ % 19.95/3.04 % (3126718)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=700341381:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 19.95/3.04 % (3126718)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.95/3.04 % (3126718)Terminated due to inappropriate strategy. % 19.95/3.04 % (3126718)------------------------------ % 19.95/3.04 % (3126718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.95/3.04 % (3126718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.95/3.04 % (3126718)CaDiCaL version: 2.1.3 % 19.95/3.04 % (3126718)Termination reason: Inappropriate % 19.95/3.04 % (3126718)Time elapsed: 0.001 s % 19.95/3.04 % (3126718)Peak memory usage: 11 MB % 19.95/3.04 % (3126718)Instructions burned: 3 (million) % 19.95/3.04 % (3126718)------------------------------ % 19.95/3.04 % (3126718)------------------------------ % 19.95/3.04 % (3126720)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1093164165:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 19.95/3.04 % (3126720)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.95/3.04 % (3126720)Terminated due to inappropriate strategy. % 19.95/3.04 % (3126720)------------------------------ % 19.95/3.04 % (3126720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.95/3.04 % (3126720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.95/3.04 % (3126720)CaDiCaL version: 2.1.3 % 19.95/3.04 % (3126720)Termination reason: Inappropriate % 19.95/3.04 % (3126720)Time elapsed: 0.001 s % 19.95/3.04 % (3126720)Peak memory usage: 11 MB % 19.95/3.04 % (3126720)Instructions burned: 3 (million) % 19.95/3.04 % (3126720)------------------------------ % 19.95/3.04 % (3126720)------------------------------ % 19.95/3.04 % (3126722)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3637832380:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 19.95/3.04 % (3126647)Instruction limit reached! % 19.95/3.04 % (3126647)------------------------------ % 19.95/3.04 % (3126647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.95/3.04 % (3126647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.95/3.04 % (3126647)CaDiCaL version: 2.1.3 % 19.95/3.04 % (3126647)Termination reason: Instruction limit % 19.95/3.04 % (3126647)Termination phase: Saturation % 19.95/3.04 % (3126647)Time elapsed: 0.333 s % 19.95/3.04 % (3126647)Peak memory usage: 14 MB % 19.95/3.04 % (3126647)Instructions burned: 477 (million) % 19.95/3.04 % (3126724)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1459011026:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 19.95/3.04 % (3126695)Instruction limit reached! % 19.95/3.04 % (3126695)------------------------------ % 27.04/4.06 % (3126695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.04/4.06 % (3126695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.04/4.06 % (3126695)CaDiCaL version: 2.1.3 % 27.04/4.06 % (3126695)Termination reason: Instruction limit % 27.04/4.06 % (3126695)Termination phase: Saturation % 27.04/4.06 % (3126695)Time elapsed: 0.402 s % 27.04/4.06 % (3126695)Peak memory usage: 17 MB % 27.04/4.06 % (3126695)Instructions burned: 694 (million) % 27.04/4.06 % (3126726)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3215451053:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 27.04/4.06 % (3126726)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.04/4.06 % (3126726)Terminated due to inappropriate strategy. % 27.04/4.06 % (3126726)------------------------------ % 27.04/4.06 % (3126726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.04/4.06 % (3126726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.04/4.06 % (3126726)CaDiCaL version: 2.1.3 % 27.04/4.06 % (3126726)Termination reason: Inappropriate % 27.04/4.06 % (3126726)Time elapsed: 0.002 s % 27.04/4.06 % (3126726)Peak memory usage: 10 MB % 27.04/4.06 % (3126726)Instructions burned: 3 (million) % 27.04/4.06 % (3126726)------------------------------ % 27.04/4.06 % (3126726)------------------------------ % 27.04/4.06 % (3126728)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1742978542:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 27.04/4.06 % (3126728)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.04/4.06 % (3126728)Terminated due to inappropriate strategy. % 27.04/4.06 % (3126728)------------------------------ % 27.04/4.06 % (3126728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.04/4.06 % (3126728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.04/4.06 % (3126728)CaDiCaL version: 2.1.3 % 27.04/4.06 % (3126728)Termination reason: Inappropriate % 27.04/4.06 % (3126728)Time elapsed: 0.002 s % 27.04/4.06 % (3126728)Peak memory usage: 10 MB % 27.04/4.06 % (3126728)Instructions burned: 3 (million) % 27.04/4.06 % (3126728)------------------------------ % 27.04/4.06 % (3126728)------------------------------ % 27.04/4.06 % (3126730)ott-2_1_sil=16000:newcnf=on:random_seed=3715319793:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 27.04/4.06 % (3126703)Instruction limit reached! % 27.04/4.06 % (3126703)------------------------------ % 27.04/4.06 % (3126703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.04/4.06 % (3126703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.04/4.06 % (3126703)CaDiCaL version: 2.1.3 % 27.04/4.06 % (3126703)Termination reason: Instruction limit % 27.04/4.06 % (3126703)Termination phase: Saturation % 27.04/4.06 % (3126703)Time elapsed: 0.519 s % 27.04/4.06 % (3126703)Peak memory usage: 19 MB % 27.04/4.06 % (3126703)Instructions burned: 880 (million) % 27.04/4.06 % (3126732)ott+10_1_sil=32000:tgt=ground:random_seed=1647643528:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 27.04/4.06 % (3126676)Instruction limit reached! % 27.04/4.06 % (3126676)------------------------------ % 27.04/4.06 % (3126676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.04/4.06 % (3126676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.04/4.06 % (3126676)CaDiCaL version: 2.1.3 % 27.04/4.06 % (3126676)Termination reason: Instruction limit % 27.04/4.06 % (3126676)Termination phase: Saturation % 27.04/4.06 % (3126676)Time elapsed: 0.661 s % 27.04/4.06 % (3126676)Peak memory usage: 19 MB % 27.04/4.06 % (3126676)Instructions burned: 1180 (million) % 27.04/4.06 % (3126735)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1280566431:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 27.04/4.06 % (3126735)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.04/4.06 % (3126735)Terminated due to inappropriate strategy. % 27.04/4.06 % (3126735)------------------------------ % 27.04/4.06 % (3126735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.04/4.06 % (3126735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.04/4.06 % (3126735)CaDiCaL version: 2.1.3 % 27.04/4.06 % (3126735)Termination reason: Inappropriate % 27.04/4.06 % (3126735)Time elapsed: 0.002 s % 27.04/4.06 % (3126735)Peak memory usage: 10 MB % 27.04/4.06 % (3126735)Instructions burned: 3 (million) % 94.96/13.60 % (3126735)------------------------------ % 94.96/13.60 % (3126735)------------------------------ % 94.96/13.60 % (3126737)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2534216523:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 94.96/13.60 % (3126730)Instruction limit reached! % 94.96/13.60 % (3126730)------------------------------ % 94.96/13.60 % (3126730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.96/13.60 % (3126730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.96/13.60 % (3126730)CaDiCaL version: 2.1.3 % 94.96/13.60 % (3126730)Termination reason: Instruction limit % 94.96/13.60 % (3126730)Termination phase: Saturation % 94.96/13.60 % (3126730)Time elapsed: 0.555 s % 94.96/13.60 % (3126730)Peak memory usage: 18 MB % 94.96/13.60 % (3126730)Instructions burned: 869 (million) % 94.96/13.60 % (3126739)dis+21_1_sil=32000:sas=cadical:random_seed=122820693:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 94.96/13.60 % (3126724)Instruction limit reached! % 94.96/13.60 % (3126724)------------------------------ % 94.96/13.60 % (3126724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.96/13.60 % (3126724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.96/13.60 % (3126724)CaDiCaL version: 2.1.3 % 94.96/13.60 % (3126724)Termination reason: Instruction limit % 94.96/13.60 % (3126724)Termination phase: Saturation % 94.96/13.60 % (3126724)Time elapsed: 0.888 s % 94.96/13.60 % (3126724)Peak memory usage: 29 MB % 94.96/13.60 % (3126724)Instructions burned: 1473 (million) % 94.96/13.60 % (3126741)ott+11_1_sil=16000:gs=on:random_seed=3544978136:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 94.96/13.60 % (3126722)Instruction limit reached! % 94.96/13.60 % (3126722)------------------------------ % 94.96/13.60 % (3126722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.96/13.60 % (3126722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.96/13.60 % (3126722)CaDiCaL version: 2.1.3 % 94.96/13.60 % (3126722)Termination reason: Instruction limit % 94.96/13.60 % (3126722)Termination phase: Saturation % 94.96/13.60 % (3126722)Time elapsed: 1.504 s % 94.96/13.60 % (3126722)Peak memory usage: 42 MB % 94.96/13.60 % (3126722)Instructions burned: 5134 (million) % 94.96/13.61 % (3126743)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1346320833:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 94.96/13.61 % (3126743)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 94.96/13.61 % (3126743)Terminated due to inappropriate strategy. % 94.96/13.61 % (3126743)------------------------------ % 94.96/13.61 % (3126743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.96/13.61 % (3126743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.96/13.61 % (3126743)CaDiCaL version: 2.1.3 % 94.96/13.61 % (3126743)Termination reason: Inappropriate % 94.96/13.61 % (3126743)Time elapsed: 0.001 s % 94.96/13.61 % (3126743)Peak memory usage: 10 MB % 94.96/13.61 % (3126743)Instructions burned: 3 (million) % 94.96/13.61 % (3126743)------------------------------ % 94.96/13.61 % (3126743)------------------------------ % 94.96/13.61 % (3126745)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3501534275:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 94.96/13.61 % (3126741)Instruction limit reached! % 94.96/13.61 % (3126741)------------------------------ % 94.96/13.61 % (3126741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.96/13.61 % (3126741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.96/13.61 % (3126741)CaDiCaL version: 2.1.3 % 94.96/13.61 % (3126741)Termination reason: Instruction limit % 94.96/13.61 % (3126741)Termination phase: Saturation % 94.96/13.61 % (3126741)Time elapsed: 1.278 s % 94.96/13.61 % (3126741)Peak memory usage: 25 MB % 94.96/13.61 % (3126741)Instructions burned: 2251 (million) % 94.96/13.61 % (3126747)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1371469420:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 94.96/13.61 % (3126737)Instruction limit reached! % 94.96/13.61 % (3126737)------------------------------ % 94.96/13.61 % (3126737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.96/13.61 % (3126737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.96/13.61 % (3126737)CaDiCaL version: 2.1.3 % 94.96/13.61 % (3126737)Termination reason: Instruction limit % 112.10/18.24 % (3126737)Termination phase: Saturation % 112.10/18.24 % (3126737)Time elapsed: 1.929 s % 112.10/18.24 % (3126737)Peak memory usage: 35 MB % 112.10/18.24 % (3126737)Instructions burned: 3512 (million) % 112.10/18.24 % (3126745)Instruction limit reached! % 112.10/18.24 % (3126745)------------------------------ % 112.10/18.24 % (3126745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.10/18.24 % (3126745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.10/18.24 % (3126745)CaDiCaL version: 2.1.3 % 112.10/18.24 % (3126745)Termination reason: Instruction limit % 112.10/18.24 % (3126745)Termination phase: Saturation % 112.10/18.24 % (3126745)Time elapsed: 0.930 s % 112.10/18.24 % (3126745)Peak memory usage: 33 MB % 112.10/18.24 % (3126745)Instructions burned: 4597 (million) % 112.10/18.24 % (3126749)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=755110354:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 112.10/18.24 % (3126750)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=275095611:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 112.10/18.24 % (3126750)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.10/18.24 % (3126750)Terminated due to inappropriate strategy. % 112.10/18.24 % (3126750)------------------------------ % 112.10/18.24 % (3126750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.10/18.24 % (3126750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.10/18.24 % (3126750)CaDiCaL version: 2.1.3 % 112.10/18.24 % (3126750)Termination reason: Inappropriate % 112.10/18.24 % (3126750)Time elapsed: 0.001 s % 112.10/18.24 % (3126750)Peak memory usage: 10 MB % 112.10/18.24 % (3126750)Instructions burned: 3 (million) % 112.10/18.24 % (3126750)------------------------------ % 112.10/18.24 % (3126750)------------------------------ % 112.10/18.24 % (3126753)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3802677678:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 112.10/18.24 % (3126753)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.10/18.24 % (3126753)Terminated due to inappropriate strategy. % 112.10/18.24 % (3126753)------------------------------ % 112.10/18.24 % (3126753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.10/18.24 % (3126753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.10/18.24 % (3126753)CaDiCaL version: 2.1.3 % 112.10/18.24 % (3126753)Termination reason: Inappropriate % 112.10/18.24 % (3126753)Time elapsed: 0.001 s % 112.10/18.24 % (3126753)Peak memory usage: 10 MB % 112.10/18.24 % (3126753)Instructions burned: 3 (million) % 112.10/18.24 % (3126753)------------------------------ % 112.10/18.24 % (3126753)------------------------------ % 112.10/18.24 % (3126755)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1994505514:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 112.10/18.24 % (3126755)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 112.10/18.24 % (3126755)Terminated due to inappropriate strategy. % 112.10/18.24 % (3126755)------------------------------ % 112.10/18.24 % (3126755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.10/18.24 % (3126755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.10/18.24 % (3126755)CaDiCaL version: 2.1.3 % 112.10/18.24 % (3126755)Termination reason: Inappropriate % 112.10/18.24 % (3126755)Time elapsed: 0.001 s % 112.10/18.24 % (3126755)Peak memory usage: 10 MB % 112.10/18.24 % (3126755)Instructions burned: 3 (million) % 112.10/18.24 % (3126755)------------------------------ % 112.10/18.24 % (3126755)------------------------------ % 112.10/18.24 % (3126757)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2163631928:i=22565:add=on:rawr=on_2971 on theBenchmark for (2971ds/22565Mi) % 112.10/18.24 % (3126739)Instruction limit reached! % 112.10/18.24 % (3126739)------------------------------ % 112.10/18.24 % (3126739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 112.10/18.24 % (3126739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.10/18.24 % (3126739)CaDiCaL version: 2.1.3 % 112.10/18.24 % (3126739)Termination reason: Instruction limit % 112.10/18.24 % (3126739)Termination phase: Saturation % 112.10/18.24 % (3126739)Time elapsed: 1.891 s % 112.10/18.24 % (3126739)Peak memory usage: 34 MB % 112.10/18.24 % (3126739)Instructions burned: 3775 (million) % 112.10/18.24 % (3126759)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4097630451:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 112.10/18.24 % (3126732)Instruction limit reached! % 128.31/18.36 % (3126732)------------------------------ % 128.31/18.36 % (3126732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.31/18.36 % (3126732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.31/18.36 % (3126732)CaDiCaL version: 2.1.3 % 128.31/18.36 % (3126732)Termination reason: Instruction limit % 128.31/18.36 % (3126732)Termination phase: Saturation % 128.31/18.36 % (3126732)Time elapsed: 3.074 s % 128.31/18.36 % (3126732)Peak memory usage: 33 MB % 128.31/18.36 % (3126732)Instructions burned: 5115 (million) % 128.31/18.36 % (3126761)dis+10_16:1_sil=16000:random_seed=2606556904:i=9155:fsr=off_2961 on theBenchmark for (2961ds/9155Mi) % 128.31/18.36 % (3126749)Instruction limit reached! % 128.31/18.36 % (3126749)------------------------------ % 128.31/18.36 % (3126749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.31/18.36 % (3126749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.31/18.36 % (3126749)CaDiCaL version: 2.1.3 % 128.31/18.36 % (3126749)Termination reason: Instruction limit % 128.31/18.36 % (3126749)Termination phase: Saturation % 128.31/18.36 % (3126749)Time elapsed: 2.780 s % 128.31/18.36 % (3126749)Peak memory usage: 52 MB % 128.31/18.36 % (3126749)Instructions burned: 5211 (million) % 128.31/18.36 % (3126763)ott-3_8_sil=64000:random_seed=2319072172:i=20139:bs=on_2943 on theBenchmark for (2943ds/20139Mi) % 128.31/18.36 % (3126759)Instruction limit reached! % 128.31/18.36 % (3126759)------------------------------ % 128.31/18.36 % (3126759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.31/18.36 % (3126759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.31/18.36 % (3126759)CaDiCaL version: 2.1.3 % 128.31/18.36 % (3126759)Termination reason: Instruction limit % 128.31/18.36 % (3126759)Termination phase: Saturation % 128.31/18.36 % (3126759)Time elapsed: 4.982 s % 128.31/18.36 % (3126759)Peak memory usage: 48 MB % 128.31/18.36 % (3126759)Instructions burned: 8173 (million) % 128.31/18.36 % (3126765)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1528588465:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi) % 128.31/18.36 % (3126765)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.31/18.36 % (3126765)Terminated due to inappropriate strategy. % 128.31/18.36 % (3126765)------------------------------ % 128.31/18.36 % (3126765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.31/18.36 % (3126765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.31/18.36 % (3126765)CaDiCaL version: 2.1.3 % 128.31/18.36 % (3126765)Termination reason: Inappropriate % 128.31/18.36 % (3126765)Time elapsed: 0.002 s % 128.31/18.36 % (3126765)Peak memory usage: 10 MB % 128.31/18.36 % (3126765)Instructions burned: 3 (million) % 128.31/18.36 % (3126765)------------------------------ % 128.31/18.36 % (3126765)------------------------------ % 128.31/18.36 % (3126767)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2329096333:i=11404_2918 on theBenchmark for (2918ds/11404Mi) % 128.31/18.36 % (3126757)Instruction limit reached! % 128.31/18.36 % (3126757)------------------------------ % 128.31/18.36 % (3126757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.31/18.36 % (3126757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.31/18.36 % (3126757)CaDiCaL version: 2.1.3 % 128.31/18.36 % (3126757)Termination reason: Instruction limit % 128.31/18.36 % (3126757)Termination phase: Saturation % 128.31/18.36 % (3126757)Time elapsed: 5.519 s % 128.31/18.36 % (3126757)Peak memory usage: 326 MB % 128.31/18.36 % (3126757)Instructions burned: 22565 (million) % 128.31/18.36 % (3126769)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3567093238:i=14134_2915 on theBenchmark for (2915ds/14134Mi) % 128.31/18.36 % (3126761)Instruction limit reached! % 128.31/18.36 % (3126761)------------------------------ % 128.31/18.36 % (3126761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.31/18.36 % (3126761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.31/18.36 % (3126761)CaDiCaL version: 2.1.3 % 128.31/18.36 % (3126761)Termination reason: Instruction limit % 128.31/18.36 % (3126761)Termination phase: Saturation % 128.31/18.36 % (3126761)Time elapsed: 4.767 s % 128.31/18.36 % (3126761)Peak memory usage: 53 MB % 128.31/18.36 % (3126761)Instructions burned: 9157 (million) % 128.31/18.36 % (3126771)dis+33_16_sil=32000:sac=on:random_seed=2428096103:i=15851:nm=0_2913 on theBenchmark for (2913ds/15851Mi) % 128.31/18.36 % (3126769)Instruction limit reached! % 128.31/18.36 % (3126769)------------------------------ % 128.31/18.36 % (3126769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.03/19.45 % (3126769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.03/19.45 % (3126769)CaDiCaL version: 2.1.3 % 136.03/19.45 % (3126769)Termination reason: Instruction limit % 136.03/19.45 % (3126769)Termination phase: Saturation % 136.03/19.45 % (3126769)Time elapsed: 4.946 s % 136.03/19.45 % (3126769)Peak memory usage: 73 MB % 136.03/19.45 % (3126769)Instructions burned: 14134 (million) % 136.03/19.45 % (3126773)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3528532031:avsq=on:i=17627:add=on:amm=off_2865 on theBenchmark for (2865ds/17627Mi) % 136.03/19.45 % (3126767)Instruction limit reached! % 136.03/19.45 % (3126767)------------------------------ % 136.03/19.45 % (3126767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.03/19.45 % (3126767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.03/19.45 % (3126767)CaDiCaL version: 2.1.3 % 136.03/19.45 % (3126767)Termination reason: Instruction limit % 136.03/19.45 % (3126767)Termination phase: Saturation % 136.03/19.45 % (3126767)Time elapsed: 7.393 s % 136.03/19.45 % (3126767)Peak memory usage: 63 MB % 136.03/19.45 % (3126767)Instructions burned: 11404 (million) % 136.03/19.45 % (3127060)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2309201266:s2a=on:i=53295_2843 on theBenchmark for (2843ds/53295Mi) % 136.03/19.45 % (3126771)Instruction limit reached! % 136.03/19.45 % (3126771)------------------------------ % 136.03/19.45 % (3126771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.03/19.45 % (3126771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.03/19.45 % (3126771)CaDiCaL version: 2.1.3 % 136.03/19.45 % (3126771)Termination reason: Instruction limit % 136.03/19.45 % (3126771)Termination phase: Saturation % 136.03/19.45 % (3126771)Time elapsed: 8.864 s % 136.03/19.45 % (3126771)Peak memory usage: 140 MB % 136.03/19.45 % (3126771)Instructions burned: 15851 (million) % 136.03/19.45 % (3127215)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4194521699:i=26857:ins=20_2824 on theBenchmark for (2824ds/26857Mi) % 136.03/19.45 % (3127215)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.03/19.45 % (3127215)Terminated due to inappropriate strategy. % 136.03/19.45 % (3127215)------------------------------ % 136.03/19.45 % (3127215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.03/19.45 % (3127215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.03/19.45 % (3127215)CaDiCaL version: 2.1.3 % 136.03/19.45 % (3127215)Termination reason: Inappropriate % 136.03/19.45 % (3127215)Time elapsed: 0.002 s % 136.03/19.45 % (3127215)Peak memory usage: 10 MB % 136.03/19.45 % (3127215)Instructions burned: 3 (million) % 136.03/19.45 % (3127215)------------------------------ % 136.03/19.45 % (3127215)------------------------------ % 136.03/19.45 % (3127217)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4250008903:i=28120:bs=on:fsr=off_2824 on theBenchmark for (2824ds/28120Mi) % 136.03/19.45 % (3126747)Instruction limit reached! % 136.03/19.45 % (3126747)------------------------------ % 136.03/19.45 % (3126747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.03/19.45 % (3126747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.03/19.45 % (3126747)CaDiCaL version: 2.1.3 % 136.03/19.45 % (3126747)Termination reason: Instruction limit % 136.03/19.45 % (3126747)Termination phase: Saturation % 136.03/19.45 % (3126747)Time elapsed: 15.278 s % 136.03/19.45 % (3126747)Peak memory usage: 114 MB % 136.03/19.45 % (3126747)Instructions burned: 29340 (million) % 136.03/19.45 % (3127219)fmb+10_1_sil=256000:fmbss=7:random_seed=771846422:fmbsr=1.6:i=182295_2820 on theBenchmark for (2820ds/182295Mi) % 136.03/19.45 % (3127219)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.03/19.45 % (3127219)Terminated due to inappropriate strategy. % 136.03/19.45 % (3127219)------------------------------ % 136.03/19.45 % (3127219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.03/19.45 % (3127219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.03/19.45 % (3127219)CaDiCaL version: 2.1.3 % 136.03/19.45 % (3127219)Termination reason: Inappropriate % 136.03/19.45 % (3127219)Time elapsed: 0.002 s % 136.03/19.45 % (3127219)Peak memory usage: 10 MB % 136.03/19.45 % (3127219)Instructions burned: 3 (million) % 136.03/19.45 % (3127219)------------------------------ % 136.03/19.45 % (3127219)------------------------------ % 136.03/19.45 % (3127221)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3194184496:i=44625:gsp=on_2819 on theBenchmark for (2819ds/44625Mi) % 142.95/20.49 % (3127221)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 142.95/20.49 % (3127221)Terminated due to inappropriate strategy. % 142.95/20.49 % (3127221)------------------------------ % 142.95/20.49 % (3127221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.95/20.49 % (3127221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.95/20.49 % (3127221)CaDiCaL version: 2.1.3 % 142.95/20.49 % (3127221)Termination reason: Inappropriate % 142.95/20.49 % (3127221)Time elapsed: 0.002 s % 142.95/20.49 % (3127221)Peak memory usage: 10 MB % 142.95/20.49 % (3127221)Instructions burned: 3 (million) % 142.95/20.49 % (3127221)------------------------------ % 142.95/20.49 % (3127221)------------------------------ % 142.95/20.49 % (3127223)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1086997539:i=160505_2819 on theBenchmark for (2819ds/160505Mi) % 142.95/20.49 % (3127223)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 142.95/20.49 % (3127223)Terminated due to inappropriate strategy. % 142.95/20.49 % (3127223)------------------------------ % 142.95/20.49 % (3127223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.95/20.49 % (3127223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.95/20.49 % (3127223)CaDiCaL version: 2.1.3 % 142.95/20.49 % (3127223)Termination reason: Inappropriate % 142.95/20.49 % (3127223)Time elapsed: 0.002 s % 142.95/20.49 % (3127223)Peak memory usage: 10 MB % 142.95/20.49 % (3127223)Instructions burned: 3 (million) % 142.95/20.49 % (3127223)------------------------------ % 142.95/20.49 % (3127223)------------------------------ % 142.95/20.49 % (3127225)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1171595871:fmbsr=1.3:i=225729_2819 on theBenchmark for (2819ds/225729Mi) % 142.95/20.49 % (3127225)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 142.95/20.49 % (3127225)Terminated due to inappropriate strategy. % 142.95/20.49 % (3127225)------------------------------ % 142.95/20.49 % (3127225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.95/20.49 % (3127225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.95/20.49 % (3127225)CaDiCaL version: 2.1.3 % 142.95/20.49 % (3127225)Termination reason: Inappropriate % 142.95/20.49 % (3127225)Time elapsed: 0.002 s % 142.95/20.49 % (3127225)Peak memory usage: 10 MB % 142.95/20.49 % (3127225)Instructions burned: 3 (million) % 142.95/20.49 % (3127225)------------------------------ % 142.95/20.49 % (3127225)------------------------------ % 142.95/20.49 % (3127227)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3816618979:fmbsr=2:i=185024:ins=7_2819 on theBenchmark for (2819ds/185024Mi) % 142.95/20.49 % (3127227)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 142.95/20.49 % (3127227)Terminated due to inappropriate strategy. % 142.95/20.49 % (3127227)------------------------------ % 142.95/20.49 % (3127227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.95/20.49 % (3127227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.95/20.49 % (3127227)CaDiCaL version: 2.1.3 % 142.95/20.49 % (3127227)Termination reason: Inappropriate % 142.95/20.49 % (3127227)Time elapsed: 0.002 s % 142.95/20.49 % (3127227)Peak memory usage: 10 MB % 142.95/20.49 % (3127227)Instructions burned: 3 (million) % 142.95/20.49 % (3127227)------------------------------ % 142.95/20.49 % (3127227)------------------------------ % 142.95/20.49 % (3127229)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=708067240:rtra=on_2818 on theBenchmark for (2818ds/0Mi) % 142.95/20.49 % (3127229)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 142.95/20.49 % (3127229)Terminated due to inappropriate strategy. % 142.95/20.49 % (3127229)------------------------------ % 142.95/20.49 % (3127229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 142.95/20.49 % (3127229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.95/20.49 % (3127229)CaDiCaL version: 2.1.3 % 142.95/20.49 % (3127229)Termination reason: Inappropriate % 142.95/20.49 % (3127229)Time elapsed: 0.003 s % 142.95/20.49 % (3127229)Peak memory usage: 10 MB % 142.95/20.49 % (3127229)Instructions burned: 4 (million) % 142.95/20.49 % (3127229)------------------------------ % 142.95/20.49 % (3127229)------------------------------ % 142.95/20.49 % (3127231)% WARNING: option uhcvi not known. % 142.95/20.49 % (3127231)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4116257262:i=271062:add=off:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/271062Mi) % 155.52/22.18 % (3126763)Instruction limit reached! % 155.52/22.18 % (3126763)------------------------------ % 155.52/22.18 % (3126763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.52/22.18 % (3126763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.52/22.18 % (3126763)CaDiCaL version: 2.1.3 % 155.52/22.18 % (3126763)Termination reason: Instruction limit % 155.52/22.18 % (3126763)Termination phase: Saturation % 155.52/22.18 % (3126763)Time elapsed: 12.929 s % 155.52/22.18 % (3126763)Peak memory usage: 95 MB % 155.52/22.18 % (3126763)Instructions burned: 20142 (million) % 155.52/22.18 % (3127233)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=794823765:i=176048:add=on:rtra=on:rawr=on_2813 on theBenchmark for (2813ds/176048Mi) % 155.52/22.18 % (3126773)Instruction limit reached! % 155.52/22.18 % (3126773)------------------------------ % 155.52/22.18 % (3126773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.52/22.18 % (3126773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.52/22.18 % (3126773)CaDiCaL version: 2.1.3 % 155.52/22.18 % (3126773)Termination reason: Instruction limit % 155.52/22.18 % (3126773)Termination phase: Saturation % 155.52/22.18 % (3126773)Time elapsed: 5.386 s % 155.52/22.18 % (3126773)Peak memory usage: 211 MB % 155.52/22.18 % (3126773)Instructions burned: 17630 (million) % 155.52/22.18 % (3127235)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1987856326:i=206:fgj=on:rtra=on_2811 on theBenchmark for (2811ds/206Mi) % 155.52/22.18 % (3127235)Instruction limit reached! % 155.52/22.18 % (3127235)------------------------------ % 155.52/22.18 % (3127235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.52/22.18 % (3127235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.52/22.18 % (3127235)CaDiCaL version: 2.1.3 % 155.52/22.18 % (3127235)Termination reason: Instruction limit % 155.52/22.18 % (3127235)Termination phase: Saturation % 155.52/22.18 % (3127235)Time elapsed: 0.073 s % 155.52/22.18 % (3127235)Peak memory usage: 14 MB % 155.52/22.18 % (3127235)Instructions burned: 209 (million) % 155.52/22.18 % (3127237)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2130148583:i=232:rtra=on_2811 on theBenchmark for (2811ds/232Mi) % 155.52/22.18 % (3127237)Instruction limit reached! % 155.52/22.18 % (3127237)------------------------------ % 155.52/22.18 % (3127237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.52/22.18 % (3127237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.52/22.18 % (3127237)CaDiCaL version: 2.1.3 % 155.52/22.18 % (3127237)Termination reason: Instruction limit % 155.52/22.18 % (3127237)Termination phase: Saturation % 155.52/22.18 % (3127237)Time elapsed: 0.081 s % 155.52/22.18 % (3127237)Peak memory usage: 14 MB % 155.52/22.18 % (3127237)Instructions burned: 233 (million) % 155.52/22.18 % (3127239)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1765122245:i=262:rtra=on_2810 on theBenchmark for (2810ds/262Mi) % 155.52/22.18 % (3127239)Instruction limit reached! % 155.52/22.18 % (3127239)------------------------------ % 155.52/22.18 % (3127239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.52/22.18 % (3127239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.52/22.18 % (3127239)CaDiCaL version: 2.1.3 % 155.52/22.18 % (3127239)Termination reason: Instruction limit % 155.52/22.18 % (3127239)Termination phase: Saturation % 155.52/22.18 % (3127239)Time elapsed: 0.086 s % 155.52/22.18 % (3127239)Peak memory usage: 14 MB % 155.52/22.18 % (3127239)Instructions burned: 265 (million) % 155.52/22.18 % (3127241)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=107839480:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2809 on theBenchmark for (2809ds/318Mi) % 155.52/22.18 % (3127241)Instruction limit reached! % 155.52/22.18 % (3127241)------------------------------ % 155.52/22.18 % (3127241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.52/22.18 % (3127241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.52/22.18 % (3127241)CaDiCaL version: 2.1.3 % 155.52/22.18 % (3127241)Termination reason: Instruction limit % 155.52/22.18 % (3127241)Termination phase: Saturation % 155.52/22.18 % (3127241)Time elapsed: 0.123 s % 155.52/22.18 % (3127241)Peak memory usage: 16 MB % 155.52/22.18 % (3127241)Instructions burned: 320 (million) % 155.52/22.18 % (3127243)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2682618917:i=1428:nm=2:rtra=on_2807 on theBenchmark for (2807ds/1428Mi) % 185.06/26.37 % (3127243)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.06/26.37 % (3127243)Terminated due to inappropriate strategy. % 185.06/26.37 % (3127243)------------------------------ % 185.06/26.37 % (3127243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.06/26.37 % (3127243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.06/26.37 % (3127243)CaDiCaL version: 2.1.3 % 185.06/26.37 % (3127243)Termination reason: Inappropriate % 185.06/26.37 % (3127243)Time elapsed: 0.001 s % 185.06/26.37 % (3127243)Peak memory usage: 10 MB % 185.06/26.37 % (3127243)Instructions burned: 3 (million) % 185.06/26.37 % (3127243)------------------------------ % 185.06/26.37 % (3127243)------------------------------ % 185.06/26.37 % (3127245)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2637682961:i=262:bd=preordered:rtra=on:fsd=on_2807 on theBenchmark for (2807ds/262Mi) % 185.06/26.37 % (3127245)Instruction limit reached! % 185.06/26.37 % (3127245)------------------------------ % 185.06/26.37 % (3127245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.06/26.37 % (3127245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.06/26.37 % (3127245)CaDiCaL version: 2.1.3 % 185.06/26.37 % (3127245)Termination reason: Instruction limit % 185.06/26.37 % (3127245)Termination phase: Saturation % 185.06/26.37 % (3127245)Time elapsed: 0.095 s % 185.06/26.37 % (3127245)Peak memory usage: 13 MB % 185.06/26.37 % (3127245)Instructions burned: 264 (million) % 185.06/26.37 % (3127247)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=2286577353:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2806 on theBenchmark for (2806ds/1368Mi) % 185.06/26.37 % (3127247)Instruction limit reached! % 185.06/26.37 % (3127247)------------------------------ % 185.06/26.37 % (3127247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.06/26.37 % (3127247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.06/26.37 % (3127247)CaDiCaL version: 2.1.3 % 185.06/26.37 % (3127247)Termination reason: Instruction limit % 185.06/26.37 % (3127247)Termination phase: Saturation % 185.06/26.37 % (3127247)Time elapsed: 0.443 s % 185.06/26.37 % (3127247)Peak memory usage: 44 MB % 185.06/26.37 % (3127247)Instructions burned: 1371 (million) % 185.06/26.37 % (3127249)ott-21_1_sil=16000:si=on:fs=off:random_seed=827675353:i=360:av=off:fsr=off:rtra=on_2801 on theBenchmark for (2801ds/360Mi) % 185.06/26.37 % (3127249)Instruction limit reached! % 185.06/26.37 % (3127249)------------------------------ % 185.06/26.37 % (3127249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.06/26.37 % (3127249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.06/26.37 % (3127249)CaDiCaL version: 2.1.3 % 185.06/26.37 % (3127249)Termination reason: Instruction limit % 185.06/26.37 % (3127249)Termination phase: Saturation % 185.06/26.37 % (3127249)Time elapsed: 0.087 s % 185.06/26.37 % (3127249)Peak memory usage: 13 MB % 185.06/26.37 % (3127249)Instructions burned: 362 (million) % 185.06/26.37 % (3127251)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=288025419:i=954:bd=all:rtra=on_2800 on theBenchmark for (2800ds/954Mi) % 185.06/26.37 % (3127251)Instruction limit reached! % 185.06/26.37 % (3127251)------------------------------ % 185.06/26.37 % (3127251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.06/26.37 % (3127251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.06/26.37 % (3127251)CaDiCaL version: 2.1.3 % 185.06/26.37 % (3127251)Termination reason: Instruction limit % 185.06/26.37 % (3127251)Termination phase: Saturation % 185.06/26.37 % (3127251)Time elapsed: 0.352 s % 185.06/26.37 % (3127251)Peak memory usage: 17 MB % 185.06/26.37 % (3127251)Instructions burned: 957 (million) % 185.06/26.37 % (3127253)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=4119199230:fmbsr=1.3:i=1730:ins=25:rtra=on_2797 on theBenchmark for (2797ds/1730Mi) % 185.06/26.37 % (3127253)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 185.06/26.37 % (3127253)Terminated due to inappropriate strategy. % 185.06/26.37 % (3127253)------------------------------ % 185.06/26.37 % (3127253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 185.06/26.37 % (3127253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.06/26.37 % (3127253)CaDiCaL version: 2.1.3 % 185.06/26.37 % (3127253)Termination reason: Inappropriate % 185.06/26.37 % (3127253)Time elapsed: 0.001 s % 245.51/34.87 % (3127253)Peak memory usage: 10 MB % 245.51/34.87 % (3127253)Instructions burned: 2 (million) % 245.51/34.87 % (3127253)------------------------------ % 245.51/34.87 % (3127253)------------------------------ % 245.51/34.87 % (3127255)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=411992144:i=2358:rtra=on_2797 on theBenchmark for (2797ds/2358Mi) % 245.51/34.87 % (3127255)Instruction limit reached! % 245.51/34.87 % (3127255)------------------------------ % 245.51/34.87 % (3127255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.51/34.87 % (3127255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.51/34.87 % (3127255)CaDiCaL version: 2.1.3 % 245.51/34.87 % (3127255)Termination reason: Instruction limit % 245.51/34.87 % (3127255)Termination phase: Saturation % 245.51/34.87 % (3127255)Time elapsed: 0.632 s % 245.51/34.87 % (3127255)Peak memory usage: 25 MB % 245.51/34.87 % (3127255)Instructions burned: 2360 (million) % 245.51/34.87 % (3127257)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2324424463:i=1778:ins=1:rtra=on_2790 on theBenchmark for (2790ds/1778Mi) % 245.51/34.87 % (3127257)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 245.51/34.87 % (3127257)Terminated due to inappropriate strategy. % 245.51/34.87 % (3127257)------------------------------ % 245.51/34.87 % (3127257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.51/34.87 % (3127257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.51/34.87 % (3127257)CaDiCaL version: 2.1.3 % 245.51/34.87 % (3127257)Termination reason: Inappropriate % 245.51/34.87 % (3127257)Time elapsed: 0.001 s % 245.51/34.87 % (3127257)Peak memory usage: 10 MB % 245.51/34.87 % (3127257)Instructions burned: 3 (million) % 245.51/34.87 % (3127257)------------------------------ % 245.51/34.87 % (3127257)------------------------------ % 245.51/34.87 % (3127259)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=4193779134:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2790 on theBenchmark for (2790ds/1384Mi) % 245.51/34.87 % (3127259)Instruction limit reached! % 245.51/34.87 % (3127259)------------------------------ % 245.51/34.87 % (3127259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.51/34.87 % (3127259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.51/34.87 % (3127259)CaDiCaL version: 2.1.3 % 245.51/34.87 % (3127259)Termination reason: Instruction limit % 245.51/34.87 % (3127259)Termination phase: Saturation % 245.51/34.87 % (3127259)Time elapsed: 0.426 s % 245.51/34.87 % (3127259)Peak memory usage: 20 MB % 245.51/34.87 % (3127259)Instructions burned: 1384 (million) % 245.51/34.87 % (3127261)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1263213721:i=1758:kws=inv_precedence:fsr=off:rtra=on_2786 on theBenchmark for (2786ds/1758Mi) % 245.51/34.87 % (3127261)Instruction limit reached! % 245.51/34.87 % (3127261)------------------------------ % 245.51/34.87 % (3127261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.51/34.87 % (3127261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.51/34.87 % (3127261)CaDiCaL version: 2.1.3 % 245.51/34.87 % (3127261)Termination reason: Instruction limit % 245.51/34.87 % (3127261)Termination phase: Saturation % 245.51/34.87 % (3127261)Time elapsed: 0.551 s % 245.51/34.87 % (3127261)Peak memory usage: 28 MB % 245.51/34.87 % (3127261)Instructions burned: 1761 (million) % 245.51/34.87 % (3127263)fmb+10_1_sil=64000:si=on:random_seed=2296690743:i=44122:nm=2:rtra=on:gsp=on_2780 on theBenchmark for (2780ds/44122Mi) % 245.51/34.87 % (3127263)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 245.51/34.87 % (3127263)Terminated due to inappropriate strategy. % 245.51/34.87 % (3127263)------------------------------ % 245.51/34.87 % (3127263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.51/34.87 % (3127263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.51/34.87 % (3127263)CaDiCaL version: 2.1.3 % 245.51/34.87 % (3127263)Termination reason: Inappropriate % 245.51/34.87 % (3127263)Time elapsed: 0.001 s % 245.51/34.87 % (3127263)Peak memory usage: 10 MB % 245.51/34.87 % (3127263)Instructions burned: 3 (million) % 245.51/34.87 % (3127263)------------------------------ % 245.51/34.87 % (3127263)------------------------------ % 245.51/34.87 % (3127265)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2896400908:i=19030:nm=5:rtra=on_2780 on theBenchmark fTerminated % 300.99/42.64 % Vampire exiting % 300.99/42.64 Terminated %------------------------------------------------------------------------------