%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC441_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:06:01 PM UTC 2026 % Result : Timeout 300.69s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC441_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.21 % Computer : n013.cluster.edu % 0.07/0.21 % Model : x86_64 x86_64 % 0.07/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.21 % Memory : 8046.5625MB % 0.07/0.21 % OS : Linux 6.8.0-71-generic % 0.07/0.21 % CPULimit : 300 % 0.07/0.21 % WCLimit : 300 % 0.07/0.21 % DateTime : Mon Sep 28 09:38:01 UTC 2026 % 0.07/0.21 % CPUTime : % 0.07/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.24 Running first-order model finding % 0.07/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.81/0.85 % (1051030)Will run a generic schedule for satisfiability detection. % 3.81/0.85 % (1051037)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=850967737:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.81/0.85 % (1051036)% WARNING: option uhcvi not known. % 3.81/0.85 % (1051035)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1816531426_2999 on theBenchmark for (2999ds/0Mi) % 3.81/0.85 % (1051036)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2358435567:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.81/0.85 % (1051038)dis+10_1_sil=32000:sp=arity:random_seed=358639232:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.81/0.85 % (1051039)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=87145297:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.81/0.85 % (1051040)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=917005103:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.81/0.85 % (1051041)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=825873047:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.81/0.85 % (1051035)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.81/0.85 % (1051035)Terminated due to inappropriate strategy. % 3.81/0.85 % (1051035)------------------------------ % 3.81/0.85 % (1051035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.81/0.85 % (1051035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.81/0.85 % (1051035)CaDiCaL version: 2.1.3 % 3.81/0.85 % (1051035)Termination reason: Inappropriate % 3.81/0.85 % (1051035)Time elapsed: 0.002 s % 3.81/0.85 % (1051035)Peak memory usage: 10 MB % 3.81/0.85 % (1051035)Instructions burned: 3 (million) % 3.81/0.85 % (1051035)------------------------------ % 3.81/0.85 % (1051035)------------------------------ % 3.81/0.85 % (1051049)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2862968861:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.81/0.85 % (1051049)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.81/0.85 % (1051049)Terminated due to inappropriate strategy. % 3.81/0.85 % (1051049)------------------------------ % 3.81/0.85 % (1051049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.81/0.85 % (1051049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.81/0.85 % (1051049)CaDiCaL version: 2.1.3 % 3.81/0.85 % (1051049)Termination reason: Inappropriate % 3.81/0.85 % (1051049)Time elapsed: 0.002 s % 3.81/0.85 % (1051049)Peak memory usage: 10 MB % 3.81/0.85 % (1051049)Instructions burned: 3 (million) % 3.81/0.85 % (1051049)------------------------------ % 3.81/0.85 % (1051049)------------------------------ % 3.81/0.85 % (1051051)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1217150289:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.81/0.85 % (1051038)Instruction limit reached! % 3.81/0.85 % (1051038)------------------------------ % 3.81/0.85 % (1051038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.81/0.85 % (1051038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.81/0.85 % (1051038)CaDiCaL version: 2.1.3 % 3.81/0.85 % (1051038)Termination reason: Instruction limit % 3.81/0.85 % (1051038)Termination phase: Saturation % 3.81/0.85 % (1051038)Time elapsed: 0.061 s % 3.81/0.85 % (1051038)Peak memory usage: 12 MB % 3.81/0.85 % (1051038)Instructions burned: 104 (million) % 3.81/0.85 % (1051040)Instruction limit reached! % 3.81/0.85 % (1051040)------------------------------ % 3.81/0.85 % (1051040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.81/0.85 % (1051040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.81/0.85 % (1051040)CaDiCaL version: 2.1.3 % 3.81/0.85 % (1051040)Termination reason: Instruction limit % 3.81/0.85 % (1051040)Termination phase: Saturation % 3.81/0.85 % (1051040)Time elapsed: 0.064 s % 3.81/0.85 % (1051040)Peak memory usage: 13 MB % 3.81/0.85 % (1051040)Instructions burned: 133 (million) % 3.81/0.85 % (1051039)Instruction limit reached! % 3.81/0.85 % (1051039)------------------------------ % 3.81/0.85 % (1051039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.81/0.85 % (1051039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.81/0.85 % (1051039)CaDiCaL version: 2.1.3 % 3.81/0.85 % (1051039)Termination reason: Instruction limit % 5.57/1.04 % (1051039)Termination phase: Saturation % 5.57/1.04 % (1051039)Time elapsed: 0.065 s % 5.57/1.04 % (1051039)Peak memory usage: 13 MB % 5.57/1.04 % (1051039)Instructions burned: 116 (million) % 5.57/1.04 % (1051053)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=173764409:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 5.57/1.04 % (1051054)ott-21_1_sil=16000:fs=off:random_seed=2754828282:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 5.57/1.04 % (1051055)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3004044486:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 5.57/1.04 % (1051041)Instruction limit reached! % 5.57/1.04 % (1051041)------------------------------ % 5.57/1.04 % (1051041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.57/1.04 % (1051041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.04 % (1051041)CaDiCaL version: 2.1.3 % 5.57/1.04 % (1051041)Termination reason: Instruction limit % 5.57/1.04 % (1051041)Termination phase: Saturation % 5.57/1.04 % (1051041)Time elapsed: 0.099 s % 5.57/1.04 % (1051041)Peak memory usage: 13 MB % 5.57/1.04 % (1051041)Instructions burned: 160 (million) % 5.57/1.04 % (1051051)Instruction limit reached! % 5.57/1.04 % (1051051)------------------------------ % 5.57/1.04 % (1051051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.57/1.04 % (1051051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.04 % (1051051)CaDiCaL version: 2.1.3 % 5.57/1.04 % (1051051)Termination reason: Instruction limit % 5.57/1.04 % (1051051)Termination phase: Saturation % 5.57/1.04 % (1051051)Time elapsed: 0.071 s % 5.57/1.04 % (1051051)Peak memory usage: 12 MB % 5.57/1.04 % (1051051)Instructions burned: 131 (million) % 5.57/1.04 % (1051059)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3409876598:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.57/1.04 % (1051059)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.57/1.04 % (1051059)Terminated due to inappropriate strategy. % 5.57/1.04 % (1051059)------------------------------ % 5.57/1.04 % (1051059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.57/1.04 % (1051059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.04 % (1051059)CaDiCaL version: 2.1.3 % 5.57/1.04 % (1051059)Termination reason: Inappropriate % 5.57/1.04 % (1051059)Time elapsed: 0.002 s % 5.57/1.04 % (1051059)Peak memory usage: 10 MB % 5.57/1.04 % (1051059)Instructions burned: 3 (million) % 5.57/1.04 % (1051059)------------------------------ % 5.57/1.04 % (1051059)------------------------------ % 5.57/1.04 % (1051060)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2210231292:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.57/1.04 % (1051062)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=826240864:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.57/1.04 % (1051062)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.57/1.04 % (1051062)Terminated due to inappropriate strategy. % 5.57/1.04 % (1051062)------------------------------ % 5.57/1.04 % (1051062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.57/1.04 % (1051062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.04 % (1051062)CaDiCaL version: 2.1.3 % 5.57/1.04 % (1051062)Termination reason: Inappropriate % 5.57/1.04 % (1051062)Time elapsed: 0.002 s % 5.57/1.04 % (1051062)Peak memory usage: 10 MB % 5.57/1.04 % (1051062)Instructions burned: 3 (million) % 5.57/1.04 % (1051062)------------------------------ % 5.57/1.04 % (1051062)------------------------------ % 5.57/1.04 % (1051065)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=2665003017:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 5.57/1.04 % (1051054)Instruction limit reached! % 5.57/1.04 % (1051054)------------------------------ % 5.57/1.04 % (1051054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.57/1.04 % (1051054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.57/1.04 % (1051054)CaDiCaL version: 2.1.3 % 5.57/1.04 % (1051054)Termination reason: Instruction limit % 5.57/1.04 % (1051054)Termination phase: Saturation % 20.93/3.27 % (1051054)Time elapsed: 0.082 s % 20.93/3.27 % (1051054)Peak memory usage: 12 MB % 20.93/3.27 % (1051054)Instructions burned: 182 (million) % 20.93/3.27 % (1051067)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4031214805:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 20.93/3.27 % (1051055)Instruction limit reached! % 20.93/3.27 % (1051055)------------------------------ % 20.93/3.27 % (1051055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.93/3.27 % (1051055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/3.27 % (1051055)CaDiCaL version: 2.1.3 % 20.93/3.27 % (1051055)Termination reason: Instruction limit % 20.93/3.27 % (1051055)Termination phase: Saturation % 20.93/3.27 % (1051055)Time elapsed: 0.303 s % 20.93/3.27 % (1051055)Peak memory usage: 14 MB % 20.93/3.27 % (1051055)Instructions burned: 477 (million) % 20.93/3.27 % (1051069)fmb+10_1_sil=64000:random_seed=3593879040:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 20.93/3.27 % (1051069)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.93/3.27 % (1051069)Terminated due to inappropriate strategy. % 20.93/3.27 % (1051069)------------------------------ % 20.93/3.27 % (1051069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.93/3.27 % (1051069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/3.27 % (1051069)CaDiCaL version: 2.1.3 % 20.93/3.27 % (1051069)Termination reason: Inappropriate % 20.93/3.27 % (1051069)Time elapsed: 0.002 s % 20.93/3.27 % (1051069)Peak memory usage: 10 MB % 20.93/3.27 % (1051069)Instructions burned: 3 (million) % 20.93/3.27 % (1051069)------------------------------ % 20.93/3.27 % (1051069)------------------------------ % 20.93/3.27 % (1051071)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4076800117:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 20.93/3.27 % (1051071)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.93/3.27 % (1051071)Terminated due to inappropriate strategy. % 20.93/3.27 % (1051071)------------------------------ % 20.93/3.27 % (1051071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.93/3.27 % (1051071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/3.27 % (1051071)CaDiCaL version: 2.1.3 % 20.93/3.27 % (1051071)Termination reason: Inappropriate % 20.93/3.27 % (1051071)Time elapsed: 0.002 s % 20.93/3.27 % (1051071)Peak memory usage: 10 MB % 20.93/3.27 % (1051071)Instructions burned: 3 (million) % 20.93/3.27 % (1051071)------------------------------ % 20.93/3.27 % (1051071)------------------------------ % 20.93/3.27 % (1051073)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1522798706:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 20.93/3.27 % (1051073)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.93/3.27 % (1051073)Terminated due to inappropriate strategy. % 20.93/3.27 % (1051073)------------------------------ % 20.93/3.27 % (1051073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.93/3.27 % (1051073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/3.27 % (1051073)CaDiCaL version: 2.1.3 % 20.93/3.27 % (1051073)Termination reason: Inappropriate % 20.93/3.27 % (1051073)Time elapsed: 0.002 s % 20.93/3.27 % (1051073)Peak memory usage: 10 MB % 20.93/3.27 % (1051073)Instructions burned: 3 (million) % 20.93/3.27 % (1051073)------------------------------ % 20.93/3.27 % (1051073)------------------------------ % 20.93/3.27 % (1051053)Instruction limit reached! % 20.93/3.27 % (1051053)------------------------------ % 20.93/3.27 % (1051053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.93/3.27 % (1051053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.93/3.27 % (1051053)CaDiCaL version: 2.1.3 % 20.93/3.27 % (1051053)Termination reason: Instruction limit % 20.93/3.27 % (1051053)Termination phase: Saturation % 20.93/3.27 % (1051053)Time elapsed: 0.389 s % 20.93/3.27 % (1051053)Peak memory usage: 18 MB % 20.93/3.27 % (1051053)Instructions burned: 684 (million) % 20.93/3.27 % (1051075)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2531703141:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 20.93/3.27 % (1051076)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1776212432:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 20.93/3.27 % (1051065)Instruction limit reached! % 20.93/3.27 % (1051065)------------------------------ % 35.14/5.20 % (1051065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.14/5.20 % (1051065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.14/5.20 % (1051065)CaDiCaL version: 2.1.3 % 35.14/5.20 % (1051065)Termination reason: Instruction limit % 35.14/5.20 % (1051065)Termination phase: Saturation % 35.14/5.20 % (1051065)Time elapsed: 0.405 s % 35.14/5.20 % (1051065)Peak memory usage: 18 MB % 35.14/5.20 % (1051065)Instructions burned: 693 (million) % 35.14/5.20 % (1051079)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=307348695:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 35.14/5.20 % (1051079)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.14/5.20 % (1051079)Terminated due to inappropriate strategy. % 35.14/5.20 % (1051079)------------------------------ % 35.14/5.20 % (1051079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.14/5.20 % (1051079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.14/5.20 % (1051079)CaDiCaL version: 2.1.3 % 35.14/5.20 % (1051079)Termination reason: Inappropriate % 35.14/5.20 % (1051079)Time elapsed: 0.002 s % 35.14/5.20 % (1051079)Peak memory usage: 10 MB % 35.14/5.20 % (1051079)Instructions burned: 3 (million) % 35.14/5.20 % (1051079)------------------------------ % 35.14/5.20 % (1051079)------------------------------ % 35.14/5.20 % (1051081)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=310323685:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 35.14/5.20 % (1051081)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.14/5.20 % (1051081)Terminated due to inappropriate strategy. % 35.14/5.20 % (1051081)------------------------------ % 35.14/5.20 % (1051081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.14/5.20 % (1051081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.14/5.20 % (1051081)CaDiCaL version: 2.1.3 % 35.14/5.20 % (1051081)Termination reason: Inappropriate % 35.14/5.20 % (1051081)Time elapsed: 0.002 s % 35.14/5.20 % (1051081)Peak memory usage: 10 MB % 35.14/5.20 % (1051081)Instructions burned: 3 (million) % 35.14/5.20 % (1051081)------------------------------ % 35.14/5.20 % (1051081)------------------------------ % 35.14/5.20 % (1051083)ott-2_1_sil=16000:newcnf=on:random_seed=1877125217:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 35.14/5.20 % (1051067)Instruction limit reached! % 35.14/5.20 % (1051067)------------------------------ % 35.14/5.20 % (1051067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.14/5.20 % (1051067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.14/5.20 % (1051067)CaDiCaL version: 2.1.3 % 35.14/5.20 % (1051067)Termination reason: Instruction limit % 35.14/5.20 % (1051067)Termination phase: Saturation % 35.14/5.20 % (1051067)Time elapsed: 0.491 s % 35.14/5.20 % (1051067)Peak memory usage: 19 MB % 35.14/5.20 % (1051067)Instructions burned: 881 (million) % 35.14/5.20 % (1051085)ott+10_1_sil=32000:tgt=ground:random_seed=2137268185:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 35.14/5.20 % (1051060)Instruction limit reached! % 35.14/5.20 % (1051060)------------------------------ % 35.14/5.20 % (1051060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.14/5.20 % (1051060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.14/5.20 % (1051060)CaDiCaL version: 2.1.3 % 35.14/5.20 % (1051060)Termination reason: Instruction limit % 35.14/5.20 % (1051060)Termination phase: Saturation % 35.14/5.20 % (1051060)Time elapsed: 0.600 s % 35.14/5.20 % (1051060)Peak memory usage: 18 MB % 35.14/5.20 % (1051060)Instructions burned: 1179 (million) % 35.14/5.20 % (1051087)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1193562677:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 35.14/5.20 % (1051087)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.14/5.20 % (1051087)Terminated due to inappropriate strategy. % 35.14/5.20 % (1051087)------------------------------ % 35.14/5.20 % (1051087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.14/5.20 % (1051087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.14/5.20 % (1051087)CaDiCaL version: 2.1.3 % 35.14/5.20 % (1051087)Termination reason: Inappropriate % 35.14/5.20 % (1051087)Time elapsed: 0.002 s % 35.14/5.20 % (1051087)Peak memory usage: 10 MB % 35.14/5.20 % (1051087)Instructions burned: 3 (million) % 106.84/15.34 % (1051087)------------------------------ % 106.84/15.34 % (1051087)------------------------------ % 106.84/15.34 % (1051089)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3307194788:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 106.84/15.34 % (1051083)Instruction limit reached! % 106.84/15.34 % (1051083)------------------------------ % 106.84/15.34 % (1051083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.84/15.34 % (1051083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.84/15.34 % (1051083)CaDiCaL version: 2.1.3 % 106.84/15.34 % (1051083)Termination reason: Instruction limit % 106.84/15.34 % (1051083)Termination phase: Saturation % 106.84/15.34 % (1051083)Time elapsed: 0.498 s % 106.84/15.34 % (1051083)Peak memory usage: 16 MB % 106.84/15.34 % (1051083)Instructions burned: 869 (million) % 106.84/15.34 % (1051091)dis+21_1_sil=32000:sas=cadical:random_seed=3870398141:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 106.84/15.34 % (1051076)Instruction limit reached! % 106.84/15.34 % (1051076)------------------------------ % 106.84/15.34 % (1051076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.84/15.34 % (1051076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.84/15.34 % (1051076)CaDiCaL version: 2.1.3 % 106.84/15.34 % (1051076)Termination reason: Instruction limit % 106.84/15.34 % (1051076)Termination phase: Saturation % 106.84/15.34 % (1051076)Time elapsed: 0.864 s % 106.84/15.34 % (1051076)Peak memory usage: 29 MB % 106.84/15.34 % (1051076)Instructions burned: 1473 (million) % 106.84/15.34 % (1051093)ott+11_1_sil=16000:gs=on:random_seed=4181295866:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 106.84/15.34 % (1051089)Instruction limit reached! % 106.84/15.34 % (1051089)------------------------------ % 106.84/15.34 % (1051089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.84/15.34 % (1051089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.84/15.34 % (1051089)CaDiCaL version: 2.1.3 % 106.84/15.34 % (1051089)Termination reason: Instruction limit % 106.84/15.34 % (1051089)Termination phase: Saturation % 106.84/15.34 % (1051089)Time elapsed: 1.739 s % 106.84/15.34 % (1051089)Peak memory usage: 31 MB % 106.84/15.34 % (1051089)Instructions burned: 3513 (million) % 106.84/15.34 % (1051095)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2778797119:fmbsr=1.6:i=67534_2974 on theBenchmark for (2974ds/67534Mi) % 106.84/15.34 % (1051095)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 106.84/15.34 % (1051095)Terminated due to inappropriate strategy. % 106.84/15.34 % (1051095)------------------------------ % 106.84/15.34 % (1051095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.84/15.34 % (1051095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.84/15.34 % (1051095)CaDiCaL version: 2.1.3 % 106.84/15.34 % (1051095)Termination reason: Inappropriate % 106.84/15.34 % (1051095)Time elapsed: 0.002 s % 106.84/15.34 % (1051095)Peak memory usage: 11 MB % 106.84/15.34 % (1051095)Instructions burned: 3 (million) % 106.84/15.34 % (1051095)------------------------------ % 106.84/15.34 % (1051095)------------------------------ % 106.84/15.34 % (1051097)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=330911099:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2974 on theBenchmark for (2974ds/4591Mi) % 106.84/15.34 % (1051093)Instruction limit reached! % 106.84/15.34 % (1051093)------------------------------ % 106.84/15.34 % (1051093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.84/15.34 % (1051093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.84/15.34 % (1051093)CaDiCaL version: 2.1.3 % 106.84/15.34 % (1051093)Termination reason: Instruction limit % 106.84/15.34 % (1051093)Termination phase: Saturation % 106.84/15.34 % (1051093)Time elapsed: 1.216 s % 106.84/15.34 % (1051093)Peak memory usage: 23 MB % 106.84/15.34 % (1051093)Instructions burned: 2251 (million) % 106.84/15.34 % (1051099)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3107954626:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 106.84/15.34 % (1051091)Instruction limit reached! % 106.84/15.34 % (1051091)------------------------------ % 106.84/15.34 % (1051091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.84/15.34 % (1051091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.84/15.34 % (1051091)CaDiCaL version: 2.1.3 % 106.84/15.34 % (1051091)Termination reason: Instruction limit % 126.99/18.19 % (1051091)Termination phase: Saturation % 126.99/18.19 % (1051091)Time elapsed: 1.844 s % 126.99/18.19 % (1051091)Peak memory usage: 27 MB % 126.99/18.19 % (1051091)Instructions burned: 3774 (million) % 126.99/18.19 % (1051101)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=577534109:i=5211_2969 on theBenchmark for (2969ds/5211Mi) % 126.99/18.19 % (1051075)Instruction limit reached! % 126.99/18.19 % (1051075)------------------------------ % 126.99/18.19 % (1051075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.99/18.19 % (1051075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.99/18.19 % (1051075)CaDiCaL version: 2.1.3 % 126.99/18.19 % (1051075)Termination reason: Instruction limit % 126.99/18.19 % (1051075)Termination phase: Saturation % 126.99/18.19 % (1051075)Time elapsed: 2.553 s % 126.99/18.19 % (1051075)Peak memory usage: 35 MB % 126.99/18.19 % (1051075)Instructions burned: 5131 (million) % 126.99/18.19 % (1051103)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1465539208:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 126.99/18.19 % (1051103)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.99/18.19 % (1051103)Terminated due to inappropriate strategy. % 126.99/18.19 % (1051103)------------------------------ % 126.99/18.19 % (1051103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.99/18.19 % (1051103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.99/18.19 % (1051103)CaDiCaL version: 2.1.3 % 126.99/18.19 % (1051103)Termination reason: Inappropriate % 126.99/18.19 % (1051103)Time elapsed: 0.002 s % 126.99/18.19 % (1051103)Peak memory usage: 10 MB % 126.99/18.19 % (1051103)Instructions burned: 3 (million) % 126.99/18.19 % (1051103)------------------------------ % 126.99/18.19 % (1051103)------------------------------ % 126.99/18.19 % (1051105)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2261582452:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 126.99/18.19 % (1051105)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.99/18.19 % (1051105)Terminated due to inappropriate strategy. % 126.99/18.19 % (1051105)------------------------------ % 126.99/18.19 % (1051105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.99/18.19 % (1051105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.99/18.19 % (1051105)CaDiCaL version: 2.1.3 % 126.99/18.19 % (1051105)Termination reason: Inappropriate % 126.99/18.19 % (1051105)Time elapsed: 0.002 s % 126.99/18.19 % (1051105)Peak memory usage: 10 MB % 126.99/18.19 % (1051105)Instructions burned: 3 (million) % 126.99/18.19 % (1051105)------------------------------ % 126.99/18.19 % (1051105)------------------------------ % 126.99/18.19 % (1051107)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2859990270:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 126.99/18.19 % (1051107)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.99/18.19 % (1051107)Terminated due to inappropriate strategy. % 126.99/18.19 % (1051107)------------------------------ % 126.99/18.19 % (1051107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.99/18.19 % (1051107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.99/18.19 % (1051107)CaDiCaL version: 2.1.3 % 126.99/18.19 % (1051107)Termination reason: Inappropriate % 126.99/18.19 % (1051107)Time elapsed: 0.002 s % 126.99/18.19 % (1051107)Peak memory usage: 10 MB % 126.99/18.19 % (1051107)Instructions burned: 3 (million) % 126.99/18.19 % (1051107)------------------------------ % 126.99/18.19 % (1051107)------------------------------ % 126.99/18.19 % (1051109)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3682186838:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 126.99/18.19 % (1051085)Instruction limit reached! % 126.99/18.19 % (1051085)------------------------------ % 126.99/18.19 % (1051085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.99/18.19 % (1051085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.99/18.19 % (1051085)CaDiCaL version: 2.1.3 % 126.99/18.19 % (1051085)Termination reason: Instruction limit % 126.99/18.19 % (1051085)Termination phase: Saturation % 126.99/18.19 % (1051085)Time elapsed: 3.081 s % 126.99/18.19 % (1051085)Peak memory usage: 35 MB % 126.99/18.19 % (1051085)Instructions burned: 5394 (million) % 126.99/18.19 % (1051112)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1617591629:i=8173:av=off_2961 on theBenchmark for (2961ds/8173Mi) % 126.99/18.19 % (1051097)Instruction limit reached! % 128.15/18.31 % (1051097)------------------------------ % 128.15/18.31 % (1051097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.15/18.31 % (1051097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.15/18.31 % (1051097)CaDiCaL version: 2.1.3 % 128.15/18.31 % (1051097)Termination reason: Instruction limit % 128.15/18.31 % (1051097)Termination phase: Saturation % 128.15/18.31 % (1051097)Time elapsed: 2.363 s % 128.15/18.31 % (1051097)Peak memory usage: 40 MB % 128.15/18.31 % (1051097)Instructions burned: 4592 (million) % 128.15/18.31 % (1051134)dis+10_16:1_sil=16000:random_seed=1723766004:i=9155:fsr=off_2950 on theBenchmark for (2950ds/9155Mi) % 128.15/18.31 % (1051101)Instruction limit reached! % 128.15/18.31 % (1051101)------------------------------ % 128.15/18.31 % (1051101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.15/18.31 % (1051101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.15/18.31 % (1051101)CaDiCaL version: 2.1.3 % 128.15/18.31 % (1051101)Termination reason: Instruction limit % 128.15/18.31 % (1051101)Termination phase: Saturation % 128.15/18.31 % (1051101)Time elapsed: 2.590 s % 128.15/18.31 % (1051101)Peak memory usage: 41 MB % 128.15/18.31 % (1051101)Instructions burned: 5211 (million) % 128.15/18.31 % (1051162)ott-3_8_sil=64000:random_seed=1567363087:i=20139:bs=on_2943 on theBenchmark for (2943ds/20139Mi) % 128.15/18.31 % (1051112)Instruction limit reached! % 128.15/18.31 % (1051112)------------------------------ % 128.15/18.31 % (1051112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.15/18.31 % (1051112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.15/18.31 % (1051112)CaDiCaL version: 2.1.3 % 128.15/18.31 % (1051112)Termination reason: Instruction limit % 128.15/18.31 % (1051112)Termination phase: Saturation % 128.15/18.31 % (1051112)Time elapsed: 4.815 s % 128.15/18.31 % (1051112)Peak memory usage: 66 MB % 128.15/18.31 % (1051112)Instructions burned: 8173 (million) % 128.15/18.31 % (1051164)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2234336632:fmbsr=2:i=32576_2913 on theBenchmark for (2913ds/32576Mi) % 128.15/18.31 % (1051164)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 128.15/18.31 % (1051164)Terminated due to inappropriate strategy. % 128.15/18.31 % (1051164)------------------------------ % 128.15/18.31 % (1051164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.15/18.31 % (1051164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.15/18.31 % (1051164)CaDiCaL version: 2.1.3 % 128.15/18.31 % (1051164)Termination reason: Inappropriate % 128.15/18.31 % (1051164)Time elapsed: 0.002 s % 128.15/18.31 % (1051164)Peak memory usage: 10 MB % 128.15/18.31 % (1051164)Instructions burned: 3 (million) % 128.15/18.31 % (1051164)------------------------------ % 128.15/18.31 % (1051164)------------------------------ % 128.15/18.31 % (1051166)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1072704558:i=11404_2913 on theBenchmark for (2913ds/11404Mi) % 128.15/18.31 % (1051134)Instruction limit reached! % 128.15/18.31 % (1051134)------------------------------ % 128.15/18.31 % (1051134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.15/18.31 % (1051134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.15/18.31 % (1051134)CaDiCaL version: 2.1.3 % 128.15/18.31 % (1051134)Termination reason: Instruction limit % 128.15/18.31 % (1051134)Termination phase: Saturation % 128.15/18.31 % (1051134)Time elapsed: 4.357 s % 128.15/18.31 % (1051134)Peak memory usage: 45 MB % 128.15/18.31 % (1051134)Instructions burned: 9155 (million) % 128.15/18.31 % (1051168)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3831403159:i=14134_2906 on theBenchmark for (2906ds/14134Mi) % 128.15/18.31 % (1051109)Instruction limit reached! % 128.15/18.31 % (1051109)------------------------------ % 128.15/18.31 % (1051109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.15/18.31 % (1051109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.15/18.31 % (1051109)CaDiCaL version: 2.1.3 % 128.15/18.31 % (1051109)Termination reason: Instruction limit % 128.15/18.31 % (1051109)Termination phase: Saturation % 128.15/18.31 % (1051109)Time elapsed: 9.553 s % 128.15/18.31 % (1051109)Peak memory usage: 78 MB % 128.15/18.31 % (1051109)Instructions burned: 22566 (million) % 128.15/18.31 % (1051170)dis+33_16_sil=32000:sac=on:random_seed=3207517390:i=15851:nm=0_2872 on theBenchmark for (2872ds/15851Mi) % 128.15/18.31 % (1051099)Instruction limit reached! % 128.15/18.31 % (1051099)------------------------------ % 128.15/18.31 % (1051099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.87/21.50 % (1051099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.87/21.50 % (1051099)CaDiCaL version: 2.1.3 % 150.87/21.50 % (1051099)Termination reason: Instruction limit % 150.87/21.50 % (1051099)Termination phase: Saturation % 150.87/21.50 % (1051099)Time elapsed: 12.442 s % 150.87/21.50 % (1051099)Peak memory usage: 169 MB % 150.87/21.50 % (1051099)Instructions burned: 29342 (million) % 150.87/21.50 % (1051172)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1405211700:avsq=on:i=17627:add=on:amm=off_2848 on theBenchmark for (2848ds/17627Mi) % 150.87/21.50 % (1051166)Instruction limit reached! % 150.87/21.50 % (1051166)------------------------------ % 150.87/21.50 % (1051166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.87/21.50 % (1051166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.87/21.50 % (1051166)CaDiCaL version: 2.1.3 % 150.87/21.50 % (1051166)Termination reason: Instruction limit % 150.87/21.50 % (1051166)Termination phase: Saturation % 150.87/21.50 % (1051166)Time elapsed: 6.579 s % 150.87/21.50 % (1051166)Peak memory usage: 60 MB % 150.87/21.50 % (1051166)Instructions burned: 11405 (million) % 150.87/21.50 % (1051174)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3904695117:s2a=on:i=53295_2847 on theBenchmark for (2847ds/53295Mi) % 150.87/21.50 % (1051168)Instruction limit reached! % 150.87/21.50 % (1051168)------------------------------ % 150.87/21.50 % (1051168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.87/21.50 % (1051168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.87/21.50 % (1051168)CaDiCaL version: 2.1.3 % 150.87/21.50 % (1051168)Termination reason: Instruction limit % 150.87/21.50 % (1051168)Termination phase: Saturation % 150.87/21.50 % (1051168)Time elapsed: 8.200 s % 150.87/21.50 % (1051168)Peak memory usage: 72 MB % 150.87/21.50 % (1051168)Instructions burned: 14136 (million) % 150.87/21.50 % (1051176)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3553134280:i=26857:ins=20_2824 on theBenchmark for (2824ds/26857Mi) % 150.87/21.50 % (1051176)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.87/21.50 % (1051176)Terminated due to inappropriate strategy. % 150.87/21.50 % (1051176)------------------------------ % 150.87/21.50 % (1051176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.87/21.50 % (1051176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.87/21.50 % (1051176)CaDiCaL version: 2.1.3 % 150.87/21.50 % (1051176)Termination reason: Inappropriate % 150.87/21.50 % (1051176)Time elapsed: 0.002 s % 150.87/21.50 % (1051176)Peak memory usage: 10 MB % 150.87/21.50 % (1051176)Instructions burned: 3 (million) % 150.87/21.50 % (1051176)------------------------------ % 150.87/21.50 % (1051176)------------------------------ % 150.87/21.50 % (1051178)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3953787176:i=28120:bs=on:fsr=off_2824 on theBenchmark for (2824ds/28120Mi) % 150.87/21.50 % (1051162)Instruction limit reached! % 150.87/21.50 % (1051162)------------------------------ % 150.87/21.50 % (1051162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.87/21.50 % (1051162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.87/21.50 % (1051162)CaDiCaL version: 2.1.3 % 150.87/21.50 % (1051162)Termination reason: Instruction limit % 150.87/21.50 % (1051162)Termination phase: Saturation % 150.87/21.50 % (1051162)Time elapsed: 12.231 s % 150.87/21.50 % (1051162)Peak memory usage: 80 MB % 150.87/21.50 % (1051162)Instructions burned: 20141 (million) % 150.87/21.50 % (1051180)fmb+10_1_sil=256000:fmbss=7:random_seed=527243830:fmbsr=1.6:i=182295_2820 on theBenchmark for (2820ds/182295Mi) % 150.87/21.50 % (1051180)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 150.87/21.50 % (1051180)Terminated due to inappropriate strategy. % 150.87/21.50 % (1051180)------------------------------ % 150.87/21.50 % (1051180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.87/21.50 % (1051180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.87/21.50 % (1051180)CaDiCaL version: 2.1.3 % 150.87/21.50 % (1051180)Termination reason: Inappropriate % 150.87/21.50 % (1051180)Time elapsed: 0.002 s % 150.87/21.50 % (1051180)Peak memory usage: 10 MB % 150.87/21.50 % (1051180)Instructions burned: 3 (million) % 150.87/21.50 % (1051180)------------------------------ % 150.87/21.50 % (1051180)------------------------------ % 150.87/21.50 % (1051182)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2869616927:i=44625:gsp=on_2820 on theBenchmark for (2820ds/44625Mi) % 156.98/22.49 % (1051182)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.98/22.49 % (1051182)Terminated due to inappropriate strategy. % 156.98/22.49 % (1051182)------------------------------ % 156.98/22.49 % (1051182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.98/22.49 % (1051182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.98/22.49 % (1051182)CaDiCaL version: 2.1.3 % 156.98/22.49 % (1051182)Termination reason: Inappropriate % 156.98/22.49 % (1051182)Time elapsed: 0.002 s % 156.98/22.49 % (1051182)Peak memory usage: 11 MB % 156.98/22.49 % (1051182)Instructions burned: 3 (million) % 156.98/22.49 % (1051182)------------------------------ % 156.98/22.49 % (1051182)------------------------------ % 156.98/22.49 % (1051184)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2059158276:i=160505_2820 on theBenchmark for (2820ds/160505Mi) % 156.98/22.49 % (1051184)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.98/22.49 % (1051184)Terminated due to inappropriate strategy. % 156.98/22.49 % (1051184)------------------------------ % 156.98/22.49 % (1051184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.98/22.49 % (1051184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.98/22.49 % (1051184)CaDiCaL version: 2.1.3 % 156.98/22.49 % (1051184)Termination reason: Inappropriate % 156.98/22.49 % (1051184)Time elapsed: 0.002 s % 156.98/22.49 % (1051184)Peak memory usage: 10 MB % 156.98/22.49 % (1051184)Instructions burned: 3 (million) % 156.98/22.49 % (1051184)------------------------------ % 156.98/22.49 % (1051184)------------------------------ % 156.98/22.49 % (1051186)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2940561092:fmbsr=1.3:i=225729_2820 on theBenchmark for (2820ds/225729Mi) % 156.98/22.49 % (1051186)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.98/22.49 % (1051186)Terminated due to inappropriate strategy. % 156.98/22.49 % (1051186)------------------------------ % 156.98/22.49 % (1051186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.98/22.49 % (1051186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.98/22.49 % (1051186)CaDiCaL version: 2.1.3 % 156.98/22.49 % (1051186)Termination reason: Inappropriate % 156.98/22.49 % (1051186)Time elapsed: 0.002 s % 156.98/22.49 % (1051186)Peak memory usage: 10 MB % 156.98/22.49 % (1051186)Instructions burned: 3 (million) % 156.98/22.49 % (1051186)------------------------------ % 156.98/22.49 % (1051186)------------------------------ % 156.98/22.49 % (1051188)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3517126859:fmbsr=2:i=185024:ins=7_2820 on theBenchmark for (2820ds/185024Mi) % 156.98/22.49 % (1051188)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.98/22.49 % (1051188)Terminated due to inappropriate strategy. % 156.98/22.49 % (1051188)------------------------------ % 156.98/22.49 % (1051188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.98/22.49 % (1051188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.98/22.49 % (1051188)CaDiCaL version: 2.1.3 % 156.98/22.49 % (1051188)Termination reason: Inappropriate % 156.98/22.49 % (1051188)Time elapsed: 0.002 s % 156.98/22.49 % (1051188)Peak memory usage: 10 MB % 156.98/22.49 % (1051188)Instructions burned: 3 (million) % 156.98/22.49 % (1051188)------------------------------ % 156.98/22.49 % (1051188)------------------------------ % 156.98/22.49 % (1051190)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3751572458:rtra=on_2819 on theBenchmark for (2819ds/0Mi) % 156.98/22.49 % (1051190)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.98/22.49 % (1051190)Terminated due to inappropriate strategy. % 156.98/22.49 % (1051190)------------------------------ % 156.98/22.49 % (1051190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.98/22.49 % (1051190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.98/22.49 % (1051190)CaDiCaL version: 2.1.3 % 156.98/22.49 % (1051190)Termination reason: Inappropriate % 156.98/22.49 % (1051190)Time elapsed: 0.002 s % 156.98/22.49 % (1051190)Peak memory usage: 10 MB % 156.98/22.49 % (1051190)Instructions burned: 3 (million) % 156.98/22.49 % (1051190)------------------------------ % 156.98/22.49 % (1051190)------------------------------ % 156.98/22.49 % (1051192)% WARNING: option uhcvi not known. % 156.98/22.49 % (1051192)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=179134451:i=271062:add=off:rtra=on:rawr=on_2819 on theBenchmark for (2819ds/271062Mi) % 170.05/24.22 % (1051170)Instruction limit reached! % 170.05/24.22 % (1051170)------------------------------ % 170.05/24.22 % (1051170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.05/24.22 % (1051170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.05/24.22 % (1051170)CaDiCaL version: 2.1.3 % 170.05/24.22 % (1051170)Termination reason: Instruction limit % 170.05/24.22 % (1051170)Termination phase: Saturation % 170.05/24.22 % (1051170)Time elapsed: 7.555 s % 170.05/24.22 % (1051170)Peak memory usage: 170 MB % 170.05/24.22 % (1051170)Instructions burned: 15853 (million) % 170.05/24.22 % (1051194)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3694952309:i=176048:add=on:rtra=on:rawr=on_2796 on theBenchmark for (2796ds/176048Mi) % 170.05/24.22 % (1051037)Instruction limit reached! % 170.05/24.22 % (1051037)------------------------------ % 170.05/24.22 % (1051037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.05/24.22 % (1051037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.05/24.22 % (1051037)CaDiCaL version: 2.1.3 % 170.05/24.22 % (1051037)Termination reason: Instruction limit % 170.05/24.22 % (1051037)Termination phase: Saturation % 170.05/24.22 % (1051037)Time elapsed: 20.756 s % 170.05/24.22 % (1051037)Peak memory usage: 1139 MB % 170.05/24.22 % (1051037)Instructions burned: 88027 (million) % 170.05/24.22 % (1051196)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2130554888:i=206:fgj=on:rtra=on_2791 on theBenchmark for (2791ds/206Mi) % 170.05/24.22 % (1051196)Instruction limit reached! % 170.05/24.22 % (1051196)------------------------------ % 170.05/24.22 % (1051196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.05/24.22 % (1051196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.05/24.22 % (1051196)CaDiCaL version: 2.1.3 % 170.05/24.22 % (1051196)Termination reason: Instruction limit % 170.05/24.22 % (1051196)Termination phase: Saturation % 170.05/24.22 % (1051196)Time elapsed: 0.066 s % 170.05/24.22 % (1051196)Peak memory usage: 13 MB % 170.05/24.22 % (1051196)Instructions burned: 207 (million) % 170.05/24.22 % (1051198)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1891561580:i=232:rtra=on_2790 on theBenchmark for (2790ds/232Mi) % 170.05/24.22 % (1051198)Instruction limit reached! % 170.05/24.22 % (1051198)------------------------------ % 170.05/24.22 % (1051198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.05/24.22 % (1051198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.05/24.22 % (1051198)CaDiCaL version: 2.1.3 % 170.05/24.22 % (1051198)Termination reason: Instruction limit % 170.05/24.22 % (1051198)Termination phase: Saturation % 170.05/24.22 % (1051198)Time elapsed: 0.076 s % 170.05/24.22 % (1051198)Peak memory usage: 14 MB % 170.05/24.22 % (1051198)Instructions burned: 233 (million) % 170.05/24.22 % (1051200)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3854732798:i=262:rtra=on_2789 on theBenchmark for (2789ds/262Mi) % 170.05/24.22 % (1051200)Instruction limit reached! % 170.05/24.22 % (1051200)------------------------------ % 170.05/24.22 % (1051200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.05/24.22 % (1051200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.05/24.22 % (1051200)CaDiCaL version: 2.1.3 % 170.05/24.22 % (1051200)Termination reason: Instruction limit % 170.05/24.22 % (1051200)Termination phase: Saturation % 170.05/24.22 % (1051200)Time elapsed: 0.065 s % 170.05/24.22 % (1051200)Peak memory usage: 13 MB % 170.05/24.22 % (1051200)Instructions burned: 262 (million) % 170.05/24.22 % (1051202)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1038783647:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2788 on theBenchmark for (2788ds/318Mi) % 170.05/24.22 % (1051202)Instruction limit reached! % 170.05/24.22 % (1051202)------------------------------ % 170.05/24.22 % (1051202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.05/24.22 % (1051202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.05/24.22 % (1051202)CaDiCaL version: 2.1.3 % 170.05/24.22 % (1051202)Termination reason: Instruction limit % 170.05/24.22 % (1051202)Termination phase: Saturation % 170.05/24.22 % (1051202)Time elapsed: 0.114 s % 170.05/24.22 % (1051202)Peak memory usage: 15 MB % 170.05/24.22 % (1051202)Instructions burned: 318 (million) % 170.05/24.22 % (1051204)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2207079617:i=1428:nm=2:rtra=on_2787 on theBenchmark for (2787ds/1428Mi) % 187.76/26.75 % (1051204)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.76/26.75 % (1051204)Terminated due to inappropriate strategy. % 187.76/26.75 % (1051204)------------------------------ % 187.76/26.75 % (1051204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.76/26.75 % (1051204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.76/26.75 % (1051204)CaDiCaL version: 2.1.3 % 187.76/26.75 % (1051204)Termination reason: Inappropriate % 187.76/26.75 % (1051204)Time elapsed: 0.001 s % 187.76/26.75 % (1051204)Peak memory usage: 10 MB % 187.76/26.75 % (1051204)Instructions burned: 3 (million) % 187.76/26.75 % (1051204)------------------------------ % 187.76/26.75 % (1051204)------------------------------ % 187.76/26.75 % (1051206)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=756980769:i=262:bd=preordered:rtra=on:fsd=on_2787 on theBenchmark for (2787ds/262Mi) % 187.76/26.75 % (1051206)Instruction limit reached! % 187.76/26.75 % (1051206)------------------------------ % 187.76/26.75 % (1051206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.76/26.75 % (1051206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.76/26.75 % (1051206)CaDiCaL version: 2.1.3 % 187.76/26.75 % (1051206)Termination reason: Instruction limit % 187.76/26.75 % (1051206)Termination phase: Saturation % 187.76/26.75 % (1051206)Time elapsed: 0.079 s % 187.76/26.75 % (1051206)Peak memory usage: 13 MB % 187.76/26.75 % (1051206)Instructions burned: 264 (million) % 187.76/26.75 % (1051208)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=2438096531:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2786 on theBenchmark for (2786ds/1368Mi) % 187.76/26.75 % (1051208)Instruction limit reached! % 187.76/26.75 % (1051208)------------------------------ % 187.76/26.75 % (1051208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.76/26.75 % (1051208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.76/26.75 % (1051208)CaDiCaL version: 2.1.3 % 187.76/26.75 % (1051208)Termination reason: Instruction limit % 187.76/26.75 % (1051208)Termination phase: Saturation % 187.76/26.75 % (1051208)Time elapsed: 0.427 s % 187.76/26.75 % (1051208)Peak memory usage: 22 MB % 187.76/26.75 % (1051208)Instructions burned: 1369 (million) % 187.76/26.75 % (1051210)ott-21_1_sil=16000:si=on:fs=off:random_seed=15282115:i=360:av=off:fsr=off:rtra=on_2782 on theBenchmark for (2782ds/360Mi) % 187.76/26.75 % (1051210)Instruction limit reached! % 187.76/26.75 % (1051210)------------------------------ % 187.76/26.75 % (1051210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.76/26.75 % (1051210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.76/26.75 % (1051210)CaDiCaL version: 2.1.3 % 187.76/26.75 % (1051210)Termination reason: Instruction limit % 187.76/26.75 % (1051210)Termination phase: Saturation % 187.76/26.75 % (1051210)Time elapsed: 0.085 s % 187.76/26.75 % (1051210)Peak memory usage: 13 MB % 187.76/26.75 % (1051210)Instructions burned: 360 (million) % 187.76/26.75 % (1051212)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2129673609:i=954:bd=all:rtra=on_2781 on theBenchmark for (2781ds/954Mi) % 187.76/26.75 % (1051212)Instruction limit reached! % 187.76/26.75 % (1051212)------------------------------ % 187.76/26.75 % (1051212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.76/26.75 % (1051212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.76/26.75 % (1051212)CaDiCaL version: 2.1.3 % 187.76/26.75 % (1051212)Termination reason: Instruction limit % 187.76/26.75 % (1051212)Termination phase: Saturation % 187.76/26.75 % (1051212)Time elapsed: 0.337 s % 187.76/26.75 % (1051212)Peak memory usage: 16 MB % 187.76/26.75 % (1051212)Instructions burned: 955 (million) % 187.76/26.75 % (1051214)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1635583320:fmbsr=1.3:i=1730:ins=25:rtra=on_2777 on theBenchmark for (2777ds/1730Mi) % 187.76/26.75 % (1051214)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 187.76/26.75 % (1051214)Terminated due to inappropriate strategy. % 187.76/26.75 % (1051214)------------------------------ % 187.76/26.75 % (1051214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 187.76/26.75 % (1051214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.76/26.75 % (1051214)CaDiCaL version: 2.1.3 % 187.76/26.75 % (1051214)Termination reason: Inappropriate % 187.76/26.75 % (1051214)Time elapsed: 0.001 s % 217.61/30.99 % (1051214)Peak memory usage: 10 MB % 217.61/30.99 % (1051214)Instructions burned: 3 (million) % 217.61/30.99 % (1051214)------------------------------ % 217.61/30.99 % (1051214)------------------------------ % 217.61/30.99 % (1051216)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=688313028:i=2358:rtra=on_2777 on theBenchmark for (2777ds/2358Mi) % 217.61/30.99 % (1051216)Instruction limit reached! % 217.61/30.99 % (1051216)------------------------------ % 217.61/30.99 % (1051216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.61/30.99 % (1051216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.61/30.99 % (1051216)CaDiCaL version: 2.1.3 % 217.61/30.99 % (1051216)Termination reason: Instruction limit % 217.61/30.99 % (1051216)Termination phase: Saturation % 217.61/30.99 % (1051216)Time elapsed: 0.666 s % 217.61/30.99 % (1051216)Peak memory usage: 21 MB % 217.61/30.99 % (1051216)Instructions burned: 2359 (million) % 217.61/30.99 % (1051218)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=352842217:i=1778:ins=1:rtra=on_2770 on theBenchmark for (2770ds/1778Mi) % 217.61/30.99 % (1051218)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 217.61/30.99 % (1051218)Terminated due to inappropriate strategy. % 217.61/30.99 % (1051218)------------------------------ % 217.61/30.99 % (1051218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.61/30.99 % (1051218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.61/30.99 % (1051218)CaDiCaL version: 2.1.3 % 217.61/30.99 % (1051218)Termination reason: Inappropriate % 217.61/30.99 % (1051218)Time elapsed: 0.001 s % 217.61/30.99 % (1051218)Peak memory usage: 10 MB % 217.61/30.99 % (1051218)Instructions burned: 3 (million) % 217.61/30.99 % (1051218)------------------------------ % 217.61/30.99 % (1051218)------------------------------ % 217.61/30.99 % (1051220)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=2972642481:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2770 on theBenchmark for (2770ds/1384Mi) % 217.61/30.99 % (1051220)Instruction limit reached! % 217.61/30.99 % (1051220)------------------------------ % 217.61/30.99 % (1051220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.61/30.99 % (1051220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.61/30.99 % (1051220)CaDiCaL version: 2.1.3 % 217.61/30.99 % (1051220)Termination reason: Instruction limit % 217.61/30.99 % (1051220)Termination phase: Saturation % 217.61/30.99 % (1051220)Time elapsed: 0.464 s % 217.61/30.99 % (1051220)Peak memory usage: 25 MB % 217.61/30.99 % (1051220)Instructions burned: 1387 (million) % 217.61/30.99 % (1051222)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1505063600:i=1758:kws=inv_precedence:fsr=off:rtra=on_2765 on theBenchmark for (2765ds/1758Mi) % 217.61/30.99 % (1051222)Instruction limit reached! % 217.61/30.99 % (1051222)------------------------------ % 217.61/30.99 % (1051222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.61/30.99 % (1051222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.61/30.99 % (1051222)CaDiCaL version: 2.1.3 % 217.61/30.99 % (1051222)Termination reason: Instruction limit % 217.61/30.99 % (1051222)Termination phase: Saturation % 217.61/30.99 % (1051222)Time elapsed: 0.523 s % 217.61/30.99 % (1051222)Peak memory usage: 27 MB % 217.61/30.99 % (1051222)Instructions burned: 1759 (million) % 217.61/30.99 % (1051224)fmb+10_1_sil=64000:si=on:random_seed=2774149659:i=44122:nm=2:rtra=on:gsp=on_2760 on theBenchmark for (2760ds/44122Mi) % 217.61/30.99 % (1051224)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 217.61/30.99 % (1051224)Terminated due to inappropriate strategy. % 217.61/30.99 % (1051224)------------------------------ % 217.61/30.99 % (1051224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.61/30.99 % (1051224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.61/30.99 % (1051224)CaDiCaL version: 2.1.3 % 217.61/30.99 % (1051224)Termination reason: Inappropriate % 217.61/30.99 % (1051224)Time elapsed: 0.001 s % 217.61/30.99 % (1051224)Peak memory usage: 10 MB % 217.61/30.99 % (1051224)Instructions burned: 3 (million) % 217.61/30.99 % (1051224)------------------------------ % 217.61/30.99 % (1051224)------------------------------ % 217.61/30.99 % (1051226)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=866563772:i=19030:nm=5:rtra=on_2760 on theBenchmark for (2760ds/19030Mi) % 253.10/35.96 % (1051226)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 253.10/35.96 % (1051226)Terminated due to inappropriate strategy. % 253.10/35.96 % (1051226)------------------------------ % 253.10/35.96 % (1051226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.10/35.96 % (1051226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.10/35.96 % (1051226)CaDiCaL version: 2.1.3 % 253.10/35.96 % (1051226)Termination reason: Inappropriate % 253.10/35.96 % (1051226)Time elapsed: 0.001 s % 253.10/35.96 % (1051226)Peak memory usage: 10 MB % 253.10/35.96 % (1051226)Instructions burned: 3 (million) % 253.10/35.96 % (1051226)------------------------------ % 253.10/35.96 % (1051226)------------------------------ % 253.10/35.96 % (1051228)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1851503030:fmbsr=1.7:i=1840:rtra=on_2760 on theBenchmark for (2760ds/1840Mi) % 253.10/35.96 % (1051228)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 253.10/35.96 % (1051228)Terminated due to inappropriate strategy. % 253.10/35.96 % (1051228)------------------------------ % 253.10/35.96 % (1051228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.10/35.96 % (1051228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.10/35.96 % (1051228)CaDiCaL version: 2.1.3 % 253.10/35.96 % (1051228)Termination reason: Inappropriate % 253.10/35.96 % (1051228)Time elapsed: 0.001 s % 253.10/35.96 % (1051228)Peak memory usage: 10 MB % 253.10/35.96 % (1051228)Instructions burned: 3 (million) % 253.10/35.96 % (1051228)------------------------------ % 253.10/35.96 % (1051228)------------------------------ % 253.10/35.96 % (1051230)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=4055399867:i=10262:rtra=on_2760 on theBenchmark for (2760ds/10262Mi) % 253.10/35.96 % (1051172)Instruction limit reached! % 253.10/35.96 % (1051172)------------------------------ % 253.10/35.96 % (1051172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.10/35.96 % (1051172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.10/35.96 % (1051172)CaDiCaL version: 2.1.3 % 253.10/35.96 % (1051172)Termination reason: Instruction limit % 253.10/35.96 % (1051172)Termination phase: Saturation % 253.10/35.96 % (1051172)Time elapsed: 9.679 s % 253.10/35.96 % (1051172)Peak memory usage: 103 MB % 253.10/35.96 % (1051172)Instructions burned: 17628 (million) % 253.10/35.96 % (1051232)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1778234147:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2751 on theBenchmark for (2751ds/2944Mi) % 253.10/35.96 % (1051232)Instruction limit reached! % 253.10/35.96 % (1051232)------------------------------ % 253.10/35.96 % (1051232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.10/35.96 % (1051232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.10/35.96 % (1051232)CaDiCaL version: 2.1.3 % 253.10/35.96 % (1051232)Termination reason: Instruction limit % 253.10/35.96 % (1051232)Termination phase: Saturation % 253.10/35.96 % (1051232)Time elapsed: 1.611 s % 253.10/35.96 % (1051232)Peak memory usage: 29 MB % 253.10/35.96 % (1051232)Instructions burned: 2946 (million) % 253.10/35.96 % (1051234)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=4122308739:i=12648:rtra=on_2735 on theBenchmark for (2735ds/12648Mi) % 253.10/35.96 % (1051234)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 253.10/35.96 % (1051234)Terminated due to inappropriate strategy. % 253.10/35.96 % (1051234)------------------------------ % 253.10/35.96 % (1051234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.10/35.96 % (1051234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.10/35.96 % (1051234)CaDiCaL version: 2.1.3 % 253.10/35.96 % (1051234)Termination reason: Inappropriate % 253.10/35.96 % (1051234)Time elapsed: 0.002 s % 253.10/35.96 % (1051234)Peak memory usage: 10 MB % 253.10/35.96 % (1051234)Instructions burned: 3 (million) % 253.10/35.96 % (1051234)------------------------------ % 253.10/35.96 % (1051234)------------------------------ % 253.10/35.96 % (1051236)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=222760583:fmbsr=2.30978:i=4348:rtra=on_2735 on theBenchmark for (2735ds/4348Mi) % 253.10/35.96 % (1051236)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 253.10/35.96 % (1051236)Terminated due to inappropriate strategy. % 253.10/35.96 % (1051236)------------------------------ % 253.10/35.96 % (1051236)Version: Terminated % 300.69/42.64 % Vampire exiting % 300.69/42.64 Terminated %------------------------------------------------------------------------------