%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW062_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 : n001.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:58 PM UTC 2026 % Result : Timeout 300.20s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW062_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.06/0.18 % Computer : n001.cluster.edu % 0.06/0.18 % Model : x86_64 x86_64 % 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.18 % Memory : 8046.5625MB % 0.06/0.18 % OS : Linux 6.8.0-71-generic % 0.06/0.18 % CPULimit : 300 % 0.06/0.18 % WCLimit : 300 % 0.06/0.18 % DateTime : Mon Sep 28 13:16:33 UTC 2026 % 0.06/0.18 % CPUTime : % 0.06/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.21 Running first-order model finding % 0.06/0.21 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.61/0.90 % (340998)Will run a generic schedule for satisfiability detection. % 3.61/0.90 % (341010)dis+10_1_sil=32000:sp=arity:random_seed=380995105:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.61/0.90 % (341008)% WARNING: option uhcvi not known. % 3.61/0.90 % (341008)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1943797691:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.61/0.90 % (341007)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=970237383_2999 on theBenchmark for (2999ds/0Mi) % 3.61/0.90 % (341012)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3921540899:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.61/0.90 % (341011)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1948048111:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.61/0.90 % (341009)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=702808243:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.61/0.90 % (341013)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=274471709:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.61/0.90 % (341010)Instruction limit reached! % 3.61/0.90 % (341010)------------------------------ % 3.61/0.90 % (341010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.90 % (341010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.90 % (341010)CaDiCaL version: 2.1.3 % 3.61/0.90 % (341010)Termination reason: Instruction limit % 3.61/0.90 % (341010)Termination phase: Saturation % 3.61/0.90 % (341010)Time elapsed: 0.025 s % 3.61/0.90 % (341010)Peak memory usage: 15 MB % 3.61/0.90 % (341010)Instructions burned: 105 (million) % 3.61/0.90 % (341030)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=75051036:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.61/0.90 % (341007)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.61/0.90 % (341007)Terminated due to inappropriate strategy. % 3.61/0.90 % (341007)------------------------------ % 3.61/0.90 % (341007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.90 % (341007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.90 % (341007)CaDiCaL version: 2.1.3 % 3.61/0.90 % (341007)Termination reason: Inappropriate % 3.61/0.90 % (341007)Time elapsed: 0.040 s % 3.61/0.90 % (341007)Peak memory usage: 14 MB % 3.61/0.90 % (341007)Instructions burned: 91 (million) % 3.61/0.90 % (341007)------------------------------ % 3.61/0.90 % (341007)------------------------------ % 3.61/0.90 % (341030)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.61/0.90 % (341030)Terminated due to inappropriate strategy. % 3.61/0.90 % (341030)------------------------------ % 3.61/0.90 % (341030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.90 % (341030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.90 % (341030)CaDiCaL version: 2.1.3 % 3.61/0.90 % (341030)Termination reason: Inappropriate % 3.61/0.90 % (341030)Time elapsed: 0.021 s % 3.61/0.90 % (341030)Peak memory usage: 14 MB % 3.61/0.90 % (341030)Instructions burned: 91 (million) % 3.61/0.90 % (341030)------------------------------ % 3.61/0.90 % (341030)------------------------------ % 3.61/0.90 % (341012)Instruction limit reached! % 3.61/0.90 % (341012)------------------------------ % 3.61/0.90 % (341012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.90 % (341012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.90 % (341012)CaDiCaL version: 2.1.3 % 3.61/0.90 % (341012)Termination reason: Instruction limit % 3.61/0.90 % (341012)Termination phase: Saturation % 3.61/0.90 % (341012)Time elapsed: 0.055 s % 3.61/0.90 % (341012)Peak memory usage: 15 MB % 3.61/0.90 % (341012)Instructions burned: 132 (million) % 3.61/0.90 % (341011)Instruction limit reached! % 3.61/0.90 % (341011)------------------------------ % 3.61/0.90 % (341011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.90 % (341011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.90 % (341011)CaDiCaL version: 2.1.3 % 3.61/0.90 % (341011)Termination reason: Instruction limit % 3.61/0.90 % (341011)Termination phase: Saturation % 3.61/0.90 % (341011)Time elapsed: 0.058 s % 3.61/0.90 % (341011)Peak memory usage: 16 MB % 3.61/0.90 % (341011)Instructions burned: 116 (million) % 3.61/0.90 % (341036)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3124471761:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 6.52/1.23 % (341041)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=2185280756:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.52/1.23 % (341013)Instruction limit reached! % 6.52/1.23 % (341013)------------------------------ % 6.52/1.23 % (341013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.52/1.23 % (341013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.52/1.23 % (341013)CaDiCaL version: 2.1.3 % 6.52/1.23 % (341013)Termination reason: Instruction limit % 6.52/1.23 % (341013)Termination phase: Saturation % 6.52/1.23 % (341013)Time elapsed: 0.066 s % 6.52/1.23 % (341013)Peak memory usage: 15 MB % 6.52/1.23 % (341013)Instructions burned: 160 (million) % 6.52/1.23 % (341042)ott-21_1_sil=16000:fs=off:random_seed=3076558253:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.52/1.23 % (341045)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3536458450:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.52/1.23 % (341051)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2785642649:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.52/1.23 % (341036)Instruction limit reached! % 6.52/1.23 % (341036)------------------------------ % 6.52/1.23 % (341036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.52/1.23 % (341036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.52/1.23 % (341036)CaDiCaL version: 2.1.3 % 6.52/1.23 % (341036)Termination reason: Instruction limit % 6.52/1.23 % (341036)Termination phase: Saturation % 6.52/1.23 % (341036)Time elapsed: 0.057 s % 6.52/1.23 % (341036)Peak memory usage: 15 MB % 6.52/1.23 % (341036)Instructions burned: 132 (million) % 6.52/1.23 % (341051)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.52/1.23 % (341051)Terminated due to inappropriate strategy. % 6.52/1.23 % (341051)------------------------------ % 6.52/1.23 % (341051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.52/1.23 % (341051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.52/1.23 % (341051)CaDiCaL version: 2.1.3 % 6.52/1.23 % (341051)Termination reason: Inappropriate % 6.52/1.23 % (341051)Time elapsed: 0.039 s % 6.52/1.23 % (341051)Peak memory usage: 14 MB % 6.52/1.23 % (341051)Instructions burned: 90 (million) % 6.52/1.23 % (341051)------------------------------ % 6.52/1.23 % (341051)------------------------------ % 6.52/1.23 % (341077)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1632140376:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.52/1.23 % (341083)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2358698596:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 6.52/1.23 % (341042)Instruction limit reached! % 6.52/1.23 % (341042)------------------------------ % 6.52/1.23 % (341042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.52/1.23 % (341042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.52/1.23 % (341042)CaDiCaL version: 2.1.3 % 6.52/1.23 % (341042)Termination reason: Instruction limit % 6.52/1.23 % (341042)Termination phase: Saturation % 6.52/1.23 % (341042)Time elapsed: 0.082 s % 6.52/1.23 % (341042)Peak memory usage: 15 MB % 6.52/1.23 % (341042)Instructions burned: 182 (million) % 6.52/1.23 % (341098)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=2434633975: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) % 6.52/1.23 % (341083)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.52/1.23 % (341083)Terminated due to inappropriate strategy. % 6.52/1.23 % (341083)------------------------------ % 6.52/1.23 % (341083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.52/1.23 % (341083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.52/1.23 % (341083)CaDiCaL version: 2.1.3 % 6.52/1.23 % (341083)Termination reason: Inappropriate % 6.52/1.23 % (341083)Time elapsed: 0.056 s % 6.52/1.23 % (341083)Peak memory usage: 16 MB % 6.52/1.23 % (341083)Instructions burned: 125 (million) % 6.52/1.23 % (341083)------------------------------ % 6.52/1.23 % (341083)------------------------------ % 23.14/3.70 % (341107)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1779933799:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 23.14/3.70 % (341041)Instruction limit reached! % 23.14/3.70 % (341041)------------------------------ % 23.14/3.70 % (341041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.14/3.70 % (341041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.14/3.70 % (341041)CaDiCaL version: 2.1.3 % 23.14/3.70 % (341041)Termination reason: Instruction limit % 23.14/3.70 % (341041)Termination phase: Saturation % 23.14/3.70 % (341041)Time elapsed: 0.172 s % 23.14/3.70 % (341041)Peak memory usage: 20 MB % 23.14/3.70 % (341041)Instructions burned: 688 (million) % 23.14/3.70 % (341119)fmb+10_1_sil=64000:random_seed=802732358:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 23.14/3.70 % (341119)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.14/3.70 % (341119)Terminated due to inappropriate strategy. % 23.14/3.70 % (341119)------------------------------ % 23.14/3.70 % (341119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.14/3.70 % (341119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.14/3.70 % (341119)CaDiCaL version: 2.1.3 % 23.14/3.70 % (341119)Termination reason: Inappropriate % 23.14/3.70 % (341119)Time elapsed: 0.023 s % 23.14/3.70 % (341119)Peak memory usage: 14 MB % 23.14/3.70 % (341119)Instructions burned: 100 (million) % 23.14/3.70 % (341119)------------------------------ % 23.14/3.70 % (341119)------------------------------ % 23.14/3.70 % (341122)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=740337168:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 23.14/3.70 % (341122)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.14/3.70 % (341122)Terminated due to inappropriate strategy. % 23.14/3.70 % (341122)------------------------------ % 23.14/3.70 % (341122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.14/3.70 % (341122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.14/3.70 % (341122)CaDiCaL version: 2.1.3 % 23.14/3.70 % (341122)Termination reason: Inappropriate % 23.14/3.70 % (341122)Time elapsed: 0.023 s % 23.14/3.70 % (341122)Peak memory usage: 14 MB % 23.14/3.70 % (341122)Instructions burned: 91 (million) % 23.14/3.70 % (341122)------------------------------ % 23.14/3.70 % (341122)------------------------------ % 23.14/3.70 % (341136)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2359428037:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 23.14/3.70 % (341136)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.14/3.70 % (341136)Terminated due to inappropriate strategy. % 23.14/3.70 % (341136)------------------------------ % 23.14/3.70 % (341136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.14/3.70 % (341136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.14/3.70 % (341136)CaDiCaL version: 2.1.3 % 23.14/3.70 % (341136)Termination reason: Inappropriate % 23.14/3.70 % (341136)Time elapsed: 0.021 s % 23.14/3.70 % (341136)Peak memory usage: 14 MB % 23.14/3.70 % (341136)Instructions burned: 91 (million) % 23.14/3.70 % (341136)------------------------------ % 23.14/3.70 % (341136)------------------------------ % 23.14/3.70 % (341146)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1602584715:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 23.14/3.70 % (341045)Instruction limit reached! % 23.14/3.70 % (341045)------------------------------ % 23.14/3.70 % (341045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.14/3.70 % (341045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.14/3.70 % (341045)CaDiCaL version: 2.1.3 % 23.14/3.70 % (341045)Termination reason: Instruction limit % 23.14/3.70 % (341045)Termination phase: Saturation % 23.14/3.70 % (341045)Time elapsed: 0.297 s % 23.14/3.70 % (341045)Peak memory usage: 17 MB % 23.14/3.70 % (341045)Instructions burned: 477 (million) % 23.14/3.70 % (341154)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3582072436:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 23.14/3.70 % (341098)Instruction limit reached! % 23.14/3.70 % (341098)------------------------------ % 23.14/3.70 % (341098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.14/3.70 % (341098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.64/4.58 % (341098)CaDiCaL version: 2.1.3 % 29.64/4.58 % (341098)Termination reason: Instruction limit % 29.64/4.58 % (341098)Termination phase: Saturation % 29.64/4.58 % (341098)Time elapsed: 0.424 s % 29.64/4.58 % (341098)Peak memory usage: 22 MB % 29.64/4.58 % (341098)Instructions burned: 692 (million) % 29.64/4.58 % (341177)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3543339265:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 29.64/4.58 % (341177)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.64/4.58 % (341177)Terminated due to inappropriate strategy. % 29.64/4.58 % (341177)------------------------------ % 29.64/4.58 % (341177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.64/4.58 % (341177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.64/4.58 % (341177)CaDiCaL version: 2.1.3 % 29.64/4.58 % (341177)Termination reason: Inappropriate % 29.64/4.58 % (341177)Time elapsed: 0.039 s % 29.64/4.58 % (341177)Peak memory usage: 14 MB % 29.64/4.58 % (341177)Instructions burned: 91 (million) % 29.64/4.58 % (341177)------------------------------ % 29.64/4.58 % (341177)------------------------------ % 29.64/4.58 % (341077)Instruction limit reached! % 29.64/4.58 % (341077)------------------------------ % 29.64/4.58 % (341077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.64/4.58 % (341077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.64/4.58 % (341077)CaDiCaL version: 2.1.3 % 29.64/4.58 % (341077)Termination reason: Instruction limit % 29.64/4.58 % (341077)Termination phase: Saturation % 29.64/4.58 % (341077)Time elapsed: 0.537 s % 29.64/4.58 % (341077)Peak memory usage: 20 MB % 29.64/4.58 % (341077)Instructions burned: 1179 (million) % 29.64/4.58 % (341179)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2951046751:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi) % 29.64/4.58 % (341180)ott-2_1_sil=16000:newcnf=on:random_seed=1526312124:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 29.64/4.58 % (341179)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.64/4.58 % (341179)Terminated due to inappropriate strategy. % 29.64/4.58 % (341179)------------------------------ % 29.64/4.58 % (341179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.64/4.58 % (341179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.64/4.58 % (341179)CaDiCaL version: 2.1.3 % 29.64/4.58 % (341179)Termination reason: Inappropriate % 29.64/4.58 % (341179)Time elapsed: 0.039 s % 29.64/4.58 % (341179)Peak memory usage: 14 MB % 29.64/4.58 % (341179)Instructions burned: 91 (million) % 29.64/4.58 % (341179)------------------------------ % 29.64/4.58 % (341179)------------------------------ % 29.64/4.58 % (341183)ott+10_1_sil=32000:tgt=ground:random_seed=3310836663:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 29.64/4.58 % (341107)Instruction limit reached! % 29.64/4.58 % (341107)------------------------------ % 29.64/4.58 % (341107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.64/4.58 % (341107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.64/4.58 % (341107)CaDiCaL version: 2.1.3 % 29.64/4.58 % (341107)Termination reason: Instruction limit % 29.64/4.58 % (341107)Termination phase: Saturation % 29.64/4.58 % (341107)Time elapsed: 0.647 s % 29.64/4.58 % (341107)Peak memory usage: 21 MB % 29.64/4.58 % (341107)Instructions burned: 879 (million) % 29.64/4.58 % (341185)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2718333203:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 29.64/4.58 % (341154)Instruction limit reached! % 29.64/4.58 % (341154)------------------------------ % 29.64/4.58 % (341154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.64/4.58 % (341154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.64/4.58 % (341154)CaDiCaL version: 2.1.3 % 29.64/4.58 % (341154)Termination reason: Instruction limit % 29.64/4.58 % (341154)Termination phase: Saturation % 29.64/4.58 % (341154)Time elapsed: 0.523 s % 29.64/4.58 % (341154)Peak memory usage: 17 MB % 29.64/4.58 % (341154)Instructions burned: 1472 (million) % 29.64/4.58 % (341185)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 29.64/4.58 % (341185)Terminated due to inappropriate strategy. % 29.64/4.58 % (341185)------------------------------ % 29.64/4.58 % (341185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.64/4.58 % (341185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.32/13.41 % (341185)CaDiCaL version: 2.1.3 % 93.32/13.41 % (341185)Termination reason: Inappropriate % 93.32/13.41 % (341185)Time elapsed: 0.040 s % 93.32/13.41 % (341185)Peak memory usage: 14 MB % 93.32/13.41 % (341185)Instructions burned: 91 (million) % 93.32/13.41 % (341185)------------------------------ % 93.32/13.41 % (341185)------------------------------ % 93.32/13.41 % (341187)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2430082412:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 93.32/13.41 % (341188)dis+21_1_sil=32000:sas=cadical:random_seed=489929770:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 93.32/13.41 % (341180)Instruction limit reached! % 93.32/13.41 % (341180)------------------------------ % 93.32/13.41 % (341180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.32/13.41 % (341180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.32/13.41 % (341180)CaDiCaL version: 2.1.3 % 93.32/13.41 % (341180)Termination reason: Instruction limit % 93.32/13.41 % (341180)Termination phase: Saturation % 93.32/13.41 % (341180)Time elapsed: 0.474 s % 93.32/13.41 % (341180)Peak memory usage: 20 MB % 93.32/13.41 % (341180)Instructions burned: 869 (million) % 93.32/13.41 % (341199)ott+11_1_sil=16000:gs=on:random_seed=1546166522:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 93.32/13.41 % (341146)Instruction limit reached! % 93.32/13.41 % (341146)------------------------------ % 93.32/13.41 % (341146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.32/13.41 % (341146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.32/13.41 % (341146)CaDiCaL version: 2.1.3 % 93.32/13.41 % (341146)Termination reason: Instruction limit % 93.32/13.41 % (341146)Termination phase: Saturation % 93.32/13.41 % (341146)Time elapsed: 1.736 s % 93.32/13.41 % (341146)Peak memory usage: 44 MB % 93.32/13.41 % (341146)Instructions burned: 5133 (million) % 93.32/13.41 % (341255)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2909503437:fmbsr=1.6:i=67534_2978 on theBenchmark for (2978ds/67534Mi) % 93.32/13.41 % (341255)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 93.32/13.41 % (341255)Terminated due to inappropriate strategy. % 93.32/13.41 % (341255)------------------------------ % 93.32/13.41 % (341255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.32/13.41 % (341255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.32/13.41 % (341255)CaDiCaL version: 2.1.3 % 93.32/13.41 % (341255)Termination reason: Inappropriate % 93.32/13.41 % (341255)Time elapsed: 0.046 s % 93.32/13.41 % (341255)Peak memory usage: 14 MB % 93.32/13.41 % (341255)Instructions burned: 122 (million) % 93.32/13.41 % (341255)------------------------------ % 93.32/13.41 % (341255)------------------------------ % 93.32/13.41 % (341260)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=893611014:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2977 on theBenchmark for (2977ds/4591Mi) % 93.32/13.41 % (341199)Instruction limit reached! % 93.32/13.41 % (341199)------------------------------ % 93.32/13.41 % (341199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.32/13.41 % (341199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.32/13.41 % (341199)CaDiCaL version: 2.1.3 % 93.32/13.41 % (341199)Termination reason: Instruction limit % 93.32/13.41 % (341199)Termination phase: Saturation % 93.32/13.41 % (341199)Time elapsed: 1.483 s % 93.32/13.41 % (341199)Peak memory usage: 20 MB % 93.32/13.41 % (341199)Instructions burned: 2251 (million) % 93.32/13.41 % (341282)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2838740057:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 93.32/13.41 % (341188)Instruction limit reached! % 93.32/13.41 % (341188)------------------------------ % 93.32/13.41 % (341188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.32/13.41 % (341188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.32/13.41 % (341188)CaDiCaL version: 2.1.3 % 93.32/13.41 % (341188)Termination reason: Instruction limit % 93.32/13.41 % (341188)Termination phase: Saturation % 93.32/13.41 % (341188)Time elapsed: 2.351 s % 93.32/13.41 % (341188)Peak memory usage: 25 MB % 93.32/13.41 % (341188)Instructions burned: 3774 (million) % 93.32/13.41 % (341312)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=175981999:i=5211_2966 on theBenchmark for (2966ds/5211Mi) % 93.32/13.41 % (341187)Instruction limit reached! % 123.77/17.74 % (341187)------------------------------ % 123.77/17.74 % (341187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.77/17.74 % (341187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.77/17.74 % (341187)CaDiCaL version: 2.1.3 % 123.77/17.74 % (341187)Termination reason: Instruction limit % 123.77/17.74 % (341187)Termination phase: Saturation % 123.77/17.74 % (341187)Time elapsed: 2.460 s % 123.77/17.74 % (341187)Peak memory usage: 30 MB % 123.77/17.74 % (341187)Instructions burned: 3512 (million) % 123.77/17.74 % (341349)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1985318321:i=5497:nm=2_2965 on theBenchmark for (2965ds/5497Mi) % 123.77/17.74 % (341349)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.77/17.74 % (341349)Terminated due to inappropriate strategy. % 123.77/17.74 % (341349)------------------------------ % 123.77/17.74 % (341349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.77/17.74 % (341349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.77/17.74 % (341349)CaDiCaL version: 2.1.3 % 123.77/17.74 % (341349)Termination reason: Inappropriate % 123.77/17.74 % (341349)Time elapsed: 0.039 s % 123.77/17.74 % (341349)Peak memory usage: 14 MB % 123.77/17.74 % (341349)Instructions burned: 91 (million) % 123.77/17.74 % (341349)------------------------------ % 123.77/17.74 % (341349)------------------------------ % 123.77/17.74 % (341368)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2461173155:fmbsr=2:i=46332_2964 on theBenchmark for (2964ds/46332Mi) % 123.77/17.74 % (341368)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.77/17.74 % (341368)Terminated due to inappropriate strategy. % 123.77/17.74 % (341368)------------------------------ % 123.77/17.74 % (341368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.77/17.74 % (341368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.77/17.74 % (341368)CaDiCaL version: 2.1.3 % 123.77/17.74 % (341368)Termination reason: Inappropriate % 123.77/17.74 % (341368)Time elapsed: 0.053 s % 123.77/17.74 % (341368)Peak memory usage: 14 MB % 123.77/17.74 % (341368)Instructions burned: 126 (million) % 123.77/17.74 % (341368)------------------------------ % 123.77/17.74 % (341368)------------------------------ % 123.77/17.74 % (341390)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1984452594:i=14071_2963 on theBenchmark for (2963ds/14071Mi) % 123.77/17.74 % (341390)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 123.77/17.74 % (341390)Terminated due to inappropriate strategy. % 123.77/17.74 % (341390)------------------------------ % 123.77/17.74 % (341390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.77/17.74 % (341390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.77/17.74 % (341390)CaDiCaL version: 2.1.3 % 123.77/17.74 % (341390)Termination reason: Inappropriate % 123.77/17.74 % (341390)Time elapsed: 0.053 s % 123.77/17.74 % (341390)Peak memory usage: 14 MB % 123.77/17.74 % (341390)Instructions burned: 126 (million) % 123.77/17.74 % (341390)------------------------------ % 123.77/17.74 % (341390)------------------------------ % 123.77/17.74 % (341403)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1810843767:i=22565:add=on:rawr=on_2963 on theBenchmark for (2963ds/22565Mi) % 123.77/17.74 % (341260)Instruction limit reached! % 123.77/17.74 % (341260)------------------------------ % 123.77/17.74 % (341260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.77/17.74 % (341260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.77/17.74 % (341260)CaDiCaL version: 2.1.3 % 123.77/17.74 % (341260)Termination reason: Instruction limit % 123.77/17.74 % (341260)Termination phase: Saturation % 123.77/17.74 % (341260)Time elapsed: 1.500 s % 123.77/17.74 % (341260)Peak memory usage: 43 MB % 123.77/17.74 % (341260)Instructions burned: 4594 (million) % 123.77/17.74 % (341410)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4005931939:i=8173:av=off_2962 on theBenchmark for (2962ds/8173Mi) % 123.77/17.74 % (341183)Instruction limit reached! % 123.77/17.74 % (341183)------------------------------ % 123.77/17.74 % (341183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.77/17.74 % (341183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.77/17.74 % (341183)CaDiCaL version: 2.1.3 % 123.77/17.74 % (341183)Termination reason: Instruction limit % 123.77/17.74 % (341183)Termination phase: Saturation % 131.64/18.99 % (341183)Time elapsed: 3.544 s % 131.64/18.99 % (341183)Peak memory usage: 33 MB % 131.64/18.99 % (341183)Instructions burned: 5116 (million) % 131.64/18.99 % (341412)dis+10_16:1_sil=16000:random_seed=1590835932:i=9155:fsr=off_2956 on theBenchmark for (2956ds/9155Mi) % 131.64/18.99 % (341410)Instruction limit reached! % 131.64/18.99 % (341410)------------------------------ % 131.64/18.99 % (341410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.64/18.99 % (341410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.64/18.99 % (341410)CaDiCaL version: 2.1.3 % 131.64/18.99 % (341410)Termination reason: Instruction limit % 131.64/18.99 % (341410)Termination phase: Saturation % 131.64/18.99 % (341410)Time elapsed: 1.785 s % 131.64/18.99 % (341410)Peak memory usage: 37 MB % 131.64/18.99 % (341410)Instructions burned: 8174 (million) % 131.64/18.99 % (341414)ott-3_8_sil=64000:random_seed=1660059374:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 131.64/18.99 % (341312)Instruction limit reached! % 131.64/18.99 % (341312)------------------------------ % 131.64/18.99 % (341312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.64/18.99 % (341312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.64/18.99 % (341312)CaDiCaL version: 2.1.3 % 131.64/18.99 % (341312)Termination reason: Instruction limit % 131.64/18.99 % (341312)Termination phase: Saturation % 131.64/18.99 % (341312)Time elapsed: 2.776 s % 131.64/18.99 % (341312)Peak memory usage: 52 MB % 131.64/18.99 % (341312)Instructions burned: 5212 (million) % 131.64/18.99 % (341416)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2736920204:fmbsr=2:i=32576_2938 on theBenchmark for (2938ds/32576Mi) % 131.64/18.99 % (341416)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 131.64/18.99 % (341416)Terminated due to inappropriate strategy. % 131.64/18.99 % (341416)------------------------------ % 131.64/18.99 % (341416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.64/18.99 % (341416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.64/18.99 % (341416)CaDiCaL version: 2.1.3 % 131.64/18.99 % (341416)Termination reason: Inappropriate % 131.64/18.99 % (341416)Time elapsed: 0.051 s % 131.64/18.99 % (341416)Peak memory usage: 14 MB % 131.64/18.99 % (341416)Instructions burned: 123 (million) % 131.64/18.99 % (341416)------------------------------ % 131.64/18.99 % (341416)------------------------------ % 131.64/18.99 % (341418)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1751465782:i=11404_2937 on theBenchmark for (2937ds/11404Mi) % 131.64/18.99 % (341412)Instruction limit reached! % 131.64/18.99 % (341412)------------------------------ % 131.64/18.99 % (341412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.64/18.99 % (341412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.64/18.99 % (341412)CaDiCaL version: 2.1.3 % 131.64/18.99 % (341412)Termination reason: Instruction limit % 131.64/18.99 % (341412)Termination phase: Saturation % 131.64/18.99 % (341412)Time elapsed: 4.736 s % 131.64/18.99 % (341412)Peak memory usage: 56 MB % 131.64/18.99 % (341412)Instructions burned: 9155 (million) % 131.64/18.99 % (341420)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2803373793:i=14134_2908 on theBenchmark for (2908ds/14134Mi) % 131.64/18.99 % (341414)Instruction limit reached! % 131.64/18.99 % (341414)------------------------------ % 131.64/18.99 % (341414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.64/18.99 % (341414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.64/18.99 % (341414)CaDiCaL version: 2.1.3 % 131.64/18.99 % (341414)Termination reason: Instruction limit % 131.64/18.99 % (341414)Termination phase: Saturation % 131.64/18.99 % (341414)Time elapsed: 5.961 s % 131.64/18.99 % (341414)Peak memory usage: 56 MB % 131.64/18.99 % (341414)Instructions burned: 20140 (million) % 131.64/18.99 % (341464)dis+33_16_sil=32000:sac=on:random_seed=1320239176:i=15851:nm=0_2884 on theBenchmark for (2884ds/15851Mi) % 131.64/18.99 % (341403)Instruction limit reached! % 131.64/18.99 % (341403)------------------------------ % 131.64/18.99 % (341403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.64/18.99 % (341403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.64/18.99 % (341403)CaDiCaL version: 2.1.3 % 131.64/18.99 % (341403)Termination reason: Instruction limit % 131.64/18.99 % (341403)Termination phase: Saturation % 131.64/18.99 % (341403)Time elapsed: 9.457 s % 131.64/18.99 % (341403)Peak memory usage: 77 MB % 131.64/18.99 % (341403)Instructions burned: 22566 (million) % 131.64/18.99 % (341466)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=206860820:avsq=on:i=17627:add=on:amm=off_2868 on theBenchmark for (2868ds/17627Mi) % 182.06/25.95 % (341418)Instruction limit reached! % 182.06/25.95 % (341418)------------------------------ % 182.06/25.95 % (341418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.06/25.95 % (341418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.06/25.95 % (341418)CaDiCaL version: 2.1.3 % 182.06/25.95 % (341418)Termination reason: Instruction limit % 182.06/25.95 % (341418)Termination phase: Saturation % 182.06/25.95 % (341418)Time elapsed: 7.372 s % 182.06/25.95 % (341418)Peak memory usage: 49 MB % 182.06/25.95 % (341418)Instructions burned: 11404 (million) % 182.06/25.95 % (341470)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=72532864:s2a=on:i=53295_2863 on theBenchmark for (2863ds/53295Mi) % 182.06/25.95 % (341464)Instruction limit reached! % 182.06/25.95 % (341464)------------------------------ % 182.06/25.95 % (341464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.06/25.95 % (341464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.06/25.95 % (341464)CaDiCaL version: 2.1.3 % 182.06/25.95 % (341464)Termination reason: Instruction limit % 182.06/25.95 % (341464)Termination phase: Saturation % 182.06/25.95 % (341464)Time elapsed: 3.617 s % 182.06/25.95 % (341464)Peak memory usage: 33 MB % 182.06/25.95 % (341464)Instructions burned: 15853 (million) % 182.06/25.95 % (341732)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4038826002:i=26857:ins=20_2848 on theBenchmark for (2848ds/26857Mi) % 182.06/25.95 % (341732)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 182.06/25.95 % (341732)Terminated due to inappropriate strategy. % 182.06/25.95 % (341732)------------------------------ % 182.06/25.95 % (341732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.06/25.95 % (341732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.06/25.95 % (341732)CaDiCaL version: 2.1.3 % 182.06/25.95 % (341732)Termination reason: Inappropriate % 182.06/25.95 % (341732)Time elapsed: 0.021 s % 182.06/25.95 % (341732)Peak memory usage: 14 MB % 182.06/25.95 % (341732)Instructions burned: 91 (million) % 182.06/25.95 % (341732)------------------------------ % 182.06/25.95 % (341732)------------------------------ % 182.06/25.95 % (341734)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2201158754:i=28120:bs=on:fsr=off_2847 on theBenchmark for (2847ds/28120Mi) % 182.06/25.95 % (341282)Instruction limit reached! % 182.06/25.95 % (341282)------------------------------ % 182.06/25.95 % (341282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.06/25.95 % (341282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.06/25.95 % (341282)CaDiCaL version: 2.1.3 % 182.06/25.95 % (341282)Termination reason: Instruction limit % 182.06/25.95 % (341282)Termination phase: Saturation % 182.06/25.95 % (341282)Time elapsed: 14.460 s % 182.06/25.95 % (341282)Peak memory usage: 31 MB % 182.06/25.95 % (341282)Instructions burned: 29341 (million) % 182.06/25.95 % (341811)fmb+10_1_sil=256000:fmbss=7:random_seed=721352696:fmbsr=1.6:i=182295_2827 on theBenchmark for (2827ds/182295Mi) % 182.06/25.95 % (341811)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 182.06/25.95 % (341811)Terminated due to inappropriate strategy. % 182.06/25.95 % (341811)------------------------------ % 182.06/25.95 % (341811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.06/25.95 % (341811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.06/25.95 % (341811)CaDiCaL version: 2.1.3 % 182.06/25.95 % (341811)Termination reason: Inappropriate % 182.06/25.95 % (341811)Time elapsed: 0.043 s % 182.06/25.95 % (341811)Peak memory usage: 14 MB % 182.06/25.95 % (341811)Instructions burned: 91 (million) % 182.06/25.95 % (341811)------------------------------ % 182.06/25.95 % (341811)------------------------------ % 182.06/25.95 % (341814)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2324206105:i=44625:gsp=on_2826 on theBenchmark for (2826ds/44625Mi) % 182.06/25.95 % (341814)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 182.06/25.95 % (341814)Terminated due to inappropriate strategy. % 182.06/25.95 % (341814)------------------------------ % 182.06/25.95 % (341814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.06/25.95 % (341814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.06/25.95 % (341814)CaDiCaL version: 2.1.3 % 182.06/25.95 % (341814)Termination reason: Inappropriate % 187.94/26.86 % (341814)Time elapsed: 0.089 s % 187.94/26.86 % (341814)Peak memory usage: 15 MB % 187.94/26.86 % (341814)Instructions burned: 96 (million) % 187.94/26.86 % (341814)------------------------------ % 187.94/26.86 % (341814)------------------------------ % 187.94/26.86 % (341822)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3668349299:i=160505_2824 on theBenchmark for (2824ds/160505Mi) % 187.94/26.86 % (341822)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.94/26.86 % (341822)Terminated due to inappropriate strategy. % 187.94/26.86 % (341822)------------------------------ % 187.94/26.86 % (341822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.94/26.86 % (341822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.94/26.86 % (341822)CaDiCaL version: 2.1.3 % 187.94/26.86 % (341822)Termination reason: Inappropriate % 187.94/26.86 % (341822)Time elapsed: 0.075 s % 187.94/26.86 % (341822)Peak memory usage: 14 MB % 187.94/26.86 % (341822)Instructions burned: 91 (million) % 187.94/26.86 % (341822)------------------------------ % 187.94/26.86 % (341822)------------------------------ % 187.94/26.86 % (341827)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2205662419:fmbsr=1.3:i=225729_2823 on theBenchmark for (2823ds/225729Mi) % 187.94/26.86 % (341827)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.94/26.86 % (341827)Terminated due to inappropriate strategy. % 187.94/26.86 % (341827)------------------------------ % 187.94/26.86 % (341827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.94/26.86 % (341827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.94/26.86 % (341827)CaDiCaL version: 2.1.3 % 187.94/26.86 % (341827)Termination reason: Inappropriate % 187.94/26.86 % (341827)Time elapsed: 0.084 s % 187.94/26.86 % (341827)Peak memory usage: 14 MB % 187.94/26.86 % (341827)Instructions burned: 126 (million) % 187.94/26.86 % (341827)------------------------------ % 187.94/26.86 % (341827)------------------------------ % 187.94/26.86 % (341832)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3952763375:fmbsr=2:i=185024:ins=7_2822 on theBenchmark for (2822ds/185024Mi) % 187.94/26.86 % (341832)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.94/26.86 % (341832)Terminated due to inappropriate strategy. % 187.94/26.86 % (341832)------------------------------ % 187.94/26.86 % (341832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.94/26.86 % (341832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.94/26.86 % (341832)CaDiCaL version: 2.1.3 % 187.94/26.86 % (341832)Termination reason: Inappropriate % 187.94/26.86 % (341832)Time elapsed: 0.109 s % 187.94/26.86 % (341832)Peak memory usage: 14 MB % 187.94/26.86 % (341832)Instructions burned: 126 (million) % 187.94/26.86 % (341832)------------------------------ % 187.94/26.86 % (341832)------------------------------ % 187.94/26.86 % (341834)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3439431159:rtra=on_2820 on theBenchmark for (2820ds/0Mi) % 187.94/26.86 % (341834)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.94/26.86 % (341834)Terminated due to inappropriate strategy. % 187.94/26.86 % (341834)------------------------------ % 187.94/26.86 % (341834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.94/26.86 % (341834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.94/26.86 % (341834)CaDiCaL version: 2.1.3 % 187.94/26.86 % (341834)Termination reason: Inappropriate % 187.94/26.86 % (341834)Time elapsed: 0.027 s % 187.94/26.86 % (341834)Peak memory usage: 15 MB % 187.94/26.86 % (341834)Instructions burned: 106 (million) % 187.94/26.86 % (341834)------------------------------ % 187.94/26.86 % (341834)------------------------------ % 187.94/26.86 % (341836)% WARNING: option uhcvi not known. % 187.94/26.86 % (341836)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2787613166:i=271062:add=off:rtra=on:rawr=on_2820 on theBenchmark for (2820ds/271062Mi) % 187.94/26.86 % (341420)Instruction limit reached! % 187.94/26.86 % (341420)------------------------------ % 187.94/26.86 % (341420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.94/26.86 % (341420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.94/26.86 % (341420)CaDiCaL version: 2.1.3 % 187.94/26.86 % (341420)Termination reason: Instruction limit % 187.94/26.86 % (341420)Termination phase: Saturation % 187.94/26.86 % (341420)Time elapsed: 9.620 s % 187.94/26.86 % (341420)Peak memory usage: 54 MB % 187.94/26.86 % (341420)Instructions burned: 14135 (million) % 199.08/28.35 % (341944)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2391412969:i=176048:add=on:rtra=on:rawr=on_2812 on theBenchmark for (2812ds/176048Mi) % 199.08/28.35 % (341734)Instruction limit reached! % 199.08/28.35 % (341734)------------------------------ % 199.08/28.35 % (341734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.08/28.35 % (341734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.08/28.35 % (341734)CaDiCaL version: 2.1.3 % 199.08/28.35 % (341734)Termination reason: Instruction limit % 199.08/28.35 % (341734)Termination phase: Saturation % 199.08/28.35 % (341734)Time elapsed: 9.813 s % 199.08/28.35 % (341734)Peak memory usage: 28 MB % 199.08/28.35 % (341734)Instructions burned: 28121 (million) % 199.08/28.35 % (341993)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2294336441:i=206:fgj=on:rtra=on_2749 on theBenchmark for (2749ds/206Mi) % 199.08/28.35 % (341993)Instruction limit reached! % 199.08/28.35 % (341993)------------------------------ % 199.08/28.35 % (341993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.08/28.35 % (341993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.08/28.35 % (341993)CaDiCaL version: 2.1.3 % 199.08/28.35 % (341993)Termination reason: Instruction limit % 199.08/28.35 % (341993)Termination phase: Saturation % 199.08/28.35 % (341993)Time elapsed: 0.105 s % 199.08/28.35 % (341993)Peak memory usage: 17 MB % 199.08/28.35 % (341993)Instructions burned: 207 (million) % 199.08/28.35 % (341995)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4013772466:i=232:rtra=on_2748 on theBenchmark for (2748ds/232Mi) % 199.08/28.35 % (341995)Instruction limit reached! % 199.08/28.35 % (341995)------------------------------ % 199.08/28.35 % (341995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.08/28.35 % (341995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.08/28.35 % (341995)CaDiCaL version: 2.1.3 % 199.08/28.35 % (341995)Termination reason: Instruction limit % 199.08/28.35 % (341995)Termination phase: Saturation % 199.08/28.35 % (341995)Time elapsed: 0.108 s % 199.08/28.35 % (341995)Peak memory usage: 17 MB % 199.08/28.35 % (341995)Instructions burned: 232 (million) % 199.08/28.35 % (341997)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2370780918:i=262:rtra=on_2746 on theBenchmark for (2746ds/262Mi) % 199.08/28.35 % (341997)Instruction limit reached! % 199.08/28.35 % (341997)------------------------------ % 199.08/28.35 % (341997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.08/28.35 % (341997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.08/28.35 % (341997)CaDiCaL version: 2.1.3 % 199.08/28.35 % (341997)Termination reason: Instruction limit % 199.08/28.35 % (341997)Termination phase: Saturation % 199.08/28.35 % (341997)Time elapsed: 0.120 s % 199.08/28.35 % (341997)Peak memory usage: 17 MB % 199.08/28.35 % (341997)Instructions burned: 262 (million) % 199.08/28.35 % (341999)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2797847835:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2745 on theBenchmark for (2745ds/318Mi) % 199.08/28.35 % (341999)Instruction limit reached! % 199.08/28.35 % (341999)------------------------------ % 199.08/28.35 % (341999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.08/28.35 % (341999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.08/28.35 % (341999)CaDiCaL version: 2.1.3 % 199.08/28.35 % (341999)Termination reason: Instruction limit % 199.08/28.35 % (341999)Termination phase: Saturation % 199.08/28.35 % (341999)Time elapsed: 0.167 s % 199.08/28.35 % (341999)Peak memory usage: 19 MB % 199.08/28.35 % (341999)Instructions burned: 319 (million) % 199.08/28.35 % (342001)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1069517956:i=1428:nm=2:rtra=on_2743 on theBenchmark for (2743ds/1428Mi) % 199.08/28.35 % (342001)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 199.08/28.35 % (342001)Terminated due to inappropriate strategy. % 199.08/28.35 % (342001)------------------------------ % 199.08/28.35 % (342001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 199.08/28.35 % (342001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.08/28.35 % (342001)CaDiCaL version: 2.1.3 % 199.08/28.35 % (342001)Termination reason: Inappropriate % 199.08/28.35 % (342001)Time elapsed: 0.053 s % 199.08/28.35 % (342001)Peak memory usage: 15 MB % 199.08/28.35 % (342001)Instructions burned: 106 (million) % 199.08/28.35 % (342001)------------------------------ % 224.66/31.92 % (342001)------------------------------ % 224.66/31.92 % (341466)Instruction limit reached! % 224.66/31.92 % (341466)------------------------------ % 224.66/31.92 % (341466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.66/31.92 % (341466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.66/31.92 % (341466)CaDiCaL version: 2.1.3 % 224.66/31.92 % (341466)Termination reason: Instruction limit % 224.66/31.92 % (341466)Termination phase: Saturation % 224.66/31.92 % (341466)Time elapsed: 12.544 s % 224.66/31.92 % (341466)Peak memory usage: 235 MB % 224.66/31.92 % (341466)Instructions burned: 17627 (million) % 224.66/31.92 % (342003)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=702969199:i=262:bd=preordered:rtra=on:fsd=on_2742 on theBenchmark for (2742ds/262Mi) % 224.66/31.92 % (342005)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=1081133281:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2742 on theBenchmark for (2742ds/1368Mi) % 224.66/31.92 % (342003)Instruction limit reached! % 224.66/31.92 % (342003)------------------------------ % 224.66/31.93 % (342003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.66/31.93 % (342003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.66/31.93 % (342003)CaDiCaL version: 2.1.3 % 224.66/31.93 % (342003)Termination reason: Instruction limit % 224.66/31.93 % (342003)Termination phase: Saturation % 224.66/31.93 % (342003)Time elapsed: 0.121 s % 224.66/31.93 % (342003)Peak memory usage: 17 MB % 224.66/31.93 % (342003)Instructions burned: 264 (million) % 224.66/31.93 % (342007)ott-21_1_sil=16000:si=on:fs=off:random_seed=3429935762:i=360:av=off:fsr=off:rtra=on_2741 on theBenchmark for (2741ds/360Mi) % 224.66/31.93 % (342007)Instruction limit reached! % 224.66/31.93 % (342007)------------------------------ % 224.66/31.93 % (342007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.66/31.93 % (342007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.66/31.93 % (342007)CaDiCaL version: 2.1.3 % 224.66/31.93 % (342007)Termination reason: Instruction limit % 224.66/31.93 % (342007)Termination phase: Saturation % 224.66/31.93 % (342007)Time elapsed: 0.181 s % 224.66/31.93 % (342007)Peak memory usage: 17 MB % 224.66/31.93 % (342007)Instructions burned: 362 (million) % 224.66/31.93 % (342009)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1845613470:i=954:bd=all:rtra=on_2739 on theBenchmark for (2739ds/954Mi) % 224.66/31.93 % (342005)Instruction limit reached! % 224.66/31.93 % (342005)------------------------------ % 224.66/31.93 % (342005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.66/31.93 % (342005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.66/31.93 % (342005)CaDiCaL version: 2.1.3 % 224.66/31.93 % (342005)Termination reason: Instruction limit % 224.66/31.93 % (342005)Termination phase: Saturation % 224.66/31.93 % (342005)Time elapsed: 0.693 s % 224.66/31.93 % (342005)Peak memory usage: 22 MB % 224.66/31.93 % (342005)Instructions burned: 1368 (million) % 224.66/31.93 % (342011)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=20701699:fmbsr=1.3:i=1730:ins=25:rtra=on_2735 on theBenchmark for (2735ds/1730Mi) % 224.66/31.93 % (342011)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 224.66/31.93 % (342011)Terminated due to inappropriate strategy. % 224.66/31.93 % (342011)------------------------------ % 224.66/31.93 % (342011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.66/31.93 % (342011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.66/31.93 % (342011)CaDiCaL version: 2.1.3 % 224.66/31.93 % (342011)Termination reason: Inappropriate % 224.66/31.93 % (342011)Time elapsed: 0.050 s % 224.66/31.93 % (342011)Peak memory usage: 15 MB % 224.66/31.93 % (342011)Instructions burned: 105 (million) % 224.66/31.93 % (342011)------------------------------ % 224.66/31.93 % (342011)------------------------------ % 224.66/31.93 % (342013)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3028736085:i=2358:rtra=on_2734 on theBenchmark for (2734ds/2358Mi) % 224.66/31.93 % (342009)Instruction limit reached! % 224.66/31.93 % (342009)------------------------------ % 224.66/31.93 % (342009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 224.66/31.93 % (342009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.66/31.93 % (342009)CaDiCaL version: 2.1.3 % 224.66/31.93 % (342009)Termination reason: Instruction limit % 275.24/39.09 % (342009)Termination phase: Saturation % 275.24/39.09 % (342009)Time elapsed: 0.549 s % 275.24/39.09 % (342009)Peak memory usage: 21 MB % 275.24/39.09 % (342009)Instructions burned: 954 (million) % 275.24/39.09 % (342015)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3409220484:i=1778:ins=1:rtra=on_2733 on theBenchmark for (2733ds/1778Mi) % 275.24/39.09 % (342015)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 275.24/39.09 % (342015)Terminated due to inappropriate strategy. % 275.24/39.09 % (342015)------------------------------ % 275.24/39.09 % (342015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.24/39.09 % (342015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.24/39.09 % (342015)CaDiCaL version: 2.1.3 % 275.24/39.09 % (342015)Termination reason: Inappropriate % 275.24/39.09 % (342015)Time elapsed: 0.069 s % 275.24/39.09 % (342015)Peak memory usage: 17 MB % 275.24/39.09 % (342015)Instructions burned: 141 (million) % 275.24/39.09 % (342015)------------------------------ % 275.24/39.09 % (342015)------------------------------ % 275.24/39.09 % (342017)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=233702172:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2732 on theBenchmark for (2732ds/1384Mi) % 275.24/39.09 % (342017)Instruction limit reached! % 275.24/39.09 % (342017)------------------------------ % 275.24/39.09 % (342017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.24/39.09 % (342017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.24/39.09 % (342017)CaDiCaL version: 2.1.3 % 275.24/39.09 % (342017)Termination reason: Instruction limit % 275.24/39.09 % (342017)Termination phase: Saturation % 275.24/39.09 % (342017)Time elapsed: 0.844 s % 275.24/39.09 % (342017)Peak memory usage: 27 MB % 275.24/39.09 % (342017)Instructions burned: 1384 (million) % 275.24/39.09 % (342019)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1354171087:i=1758:kws=inv_precedence:fsr=off:rtra=on_2723 on theBenchmark for (2723ds/1758Mi) % 275.24/39.09 % (342013)Instruction limit reached! % 275.24/39.09 % (342013)------------------------------ % 275.24/39.09 % (342013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.24/39.09 % (342013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.24/39.09 % (342013)CaDiCaL version: 2.1.3 % 275.24/39.09 % (342013)Termination reason: Instruction limit % 275.24/39.09 % (342013)Termination phase: Saturation % 275.24/39.09 % (342013)Time elapsed: 1.373 s % 275.24/39.09 % (342013)Peak memory usage: 26 MB % 275.24/39.09 % (342013)Instructions burned: 2359 (million) % 275.24/39.09 % (342021)fmb+10_1_sil=64000:si=on:random_seed=909210003:i=44122:nm=2:rtra=on:gsp=on_2720 on theBenchmark for (2720ds/44122Mi) % 275.24/39.09 % (342021)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 275.24/39.09 % (342021)Terminated due to inappropriate strategy. % 275.24/39.09 % (342021)------------------------------ % 275.24/39.09 % (342021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.24/39.09 % (342021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.24/39.09 % (342021)CaDiCaL version: 2.1.3 % 275.24/39.09 % (342021)Termination reason: Inappropriate % 275.24/39.09 % (342021)Time elapsed: 0.058 s % 275.24/39.09 % (342021)Peak memory usage: 16 MB % 275.24/39.09 % (342021)Instructions burned: 115 (million) % 275.24/39.09 % (342021)------------------------------ % 275.24/39.09 % (342021)------------------------------ % 275.24/39.09 % (342023)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1783088868:i=19030:nm=5:rtra=on_2719 on theBenchmark for (2719ds/19030Mi) % 275.24/39.09 % (342023)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 275.24/39.09 % (342023)Terminated due to inappropriate strategy. % 275.24/39.09 % (342023)------------------------------ % 275.24/39.09 % (342023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 275.24/39.09 % (342023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.24/39.09 % (342023)CaDiCaL version: 2.1.3 % 275.24/39.09 % (342023)Termination reason: Inappropriate % 275.24/39.09 % (342023)Time elapsed: 0.053 s % 275.24/39.09 % (342023)Peak memory usage: 15 MB % 275.24/39.09 % (342023)Instructions burned: 106 (million) % 275.24/39.09 % (342023)------------------------------ % 275.24/39.09 % (342023)------------------------------ % 275.24/39.09 % (342025)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=74744763Terminated % 300.20/42.63 % Vampire exiting % 300.20/42.63 Terminated %------------------------------------------------------------------------------