%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC440_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 : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:06:00 PM UTC 2026 % Result : Timeout 300.55s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWC440_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 : n003.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:40:21 UTC 2026 % 0.07/0.22 % CPUTime : % 0.07/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.25 Running first-order model finding % 0.07/0.25 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.50/0.88 % (1466318)Will run a generic schedule for satisfiability detection. % 3.50/0.88 % (1466328)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=503433597:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.50/0.88 % (1466324)% WARNING: option uhcvi not known. % 3.50/0.88 % (1466323)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2084227595_2999 on theBenchmark for (2999ds/0Mi) % 3.50/0.88 % (1466324)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3564940096:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.50/0.88 % (1466329)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3354675467:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.50/0.88 % (1466325)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1543557448:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.50/0.88 % (1466326)dis+10_1_sil=32000:sp=arity:random_seed=2265187853:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.50/0.88 % (1466327)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1418213351:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.50/0.88 % (1466323)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.50/0.88 % (1466323)Terminated due to inappropriate strategy. % 3.50/0.88 % (1466323)------------------------------ % 3.50/0.88 % (1466323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.50/0.88 % (1466323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.50/0.88 % (1466323)CaDiCaL version: 2.1.3 % 3.50/0.88 % (1466323)Termination reason: Inappropriate % 3.50/0.88 % (1466323)Time elapsed: 0.001 s % 3.50/0.88 % (1466323)Peak memory usage: 10 MB % 3.50/0.88 % (1466323)Instructions burned: 1 (million) % 3.50/0.88 % (1466323)------------------------------ % 3.50/0.88 % (1466323)------------------------------ % 3.50/0.88 % (1466337)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1501445390:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.50/0.88 % (1466337)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.50/0.88 % (1466337)Terminated due to inappropriate strategy. % 3.50/0.88 % (1466337)------------------------------ % 3.50/0.88 % (1466337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.50/0.88 % (1466337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.50/0.88 % (1466337)CaDiCaL version: 2.1.3 % 3.50/0.88 % (1466337)Termination reason: Inappropriate % 3.50/0.88 % (1466337)Time elapsed: 0.001 s % 3.50/0.88 % (1466337)Peak memory usage: 11 MB % 3.50/0.88 % (1466337)Instructions burned: 1 (million) % 3.50/0.88 % (1466337)------------------------------ % 3.50/0.88 % (1466337)------------------------------ % 3.50/0.88 % (1466328)Instruction limit reached! % 3.50/0.88 % (1466328)------------------------------ % 3.50/0.88 % (1466328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.50/0.88 % (1466328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.50/0.88 % (1466328)CaDiCaL version: 2.1.3 % 3.50/0.88 % (1466328)Termination reason: Instruction limit % 3.50/0.88 % (1466328)Termination phase: Saturation % 3.50/0.88 % (1466328)Time elapsed: 0.044 s % 3.50/0.88 % (1466328)Peak memory usage: 13 MB % 3.50/0.88 % (1466328)Instructions burned: 132 (million) % 3.50/0.88 % (1466339)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2794314603:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.50/0.88 % (1466340)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=3331885863:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.50/0.88 % (1466326)Instruction limit reached! % 3.50/0.88 % (1466326)------------------------------ % 3.50/0.88 % (1466326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.50/0.88 % (1466326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.50/0.88 % (1466326)CaDiCaL version: 2.1.3 % 3.50/0.88 % (1466326)Termination reason: Instruction limit % 3.50/0.88 % (1466326)Termination phase: Saturation % 3.50/0.88 % (1466326)Time elapsed: 0.064 s % 3.50/0.88 % (1466326)Peak memory usage: 13 MB % 3.50/0.88 % (1466326)Instructions burned: 104 (million) % 3.50/0.88 % (1466327)Instruction limit reached! % 3.50/0.88 % (1466327)------------------------------ % 3.50/0.88 % (1466327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.99/1.03 % (1466327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.99/1.03 % (1466327)CaDiCaL version: 2.1.3 % 3.99/1.03 % (1466327)Termination reason: Instruction limit % 3.99/1.03 % (1466327)Termination phase: Saturation % 3.99/1.03 % (1466327)Time elapsed: 0.071 s % 3.99/1.03 % (1466327)Peak memory usage: 12 MB % 3.99/1.03 % (1466327)Instructions burned: 117 (million) % 3.99/1.03 % (1466343)ott-21_1_sil=16000:fs=off:random_seed=4203665218:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.99/1.03 % (1466344)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4098013404:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 3.99/1.03 % (1466329)Instruction limit reached! % 3.99/1.03 % (1466329)------------------------------ % 3.99/1.03 % (1466329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.99/1.03 % (1466329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.99/1.03 % (1466329)CaDiCaL version: 2.1.3 % 3.99/1.03 % (1466329)Termination reason: Instruction limit % 3.99/1.03 % (1466329)Termination phase: Saturation % 3.99/1.03 % (1466329)Time elapsed: 0.105 s % 3.99/1.03 % (1466329)Peak memory usage: 13 MB % 3.99/1.03 % (1466329)Instructions burned: 159 (million) % 3.99/1.03 % (1466339)Instruction limit reached! % 3.99/1.03 % (1466339)------------------------------ % 3.99/1.03 % (1466339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.99/1.03 % (1466339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.99/1.03 % (1466339)CaDiCaL version: 2.1.3 % 3.99/1.03 % (1466339)Termination reason: Instruction limit % 3.99/1.03 % (1466339)Termination phase: Saturation % 3.99/1.03 % (1466339)Time elapsed: 0.079 s % 3.99/1.03 % (1466339)Peak memory usage: 13 MB % 3.99/1.03 % (1466339)Instructions burned: 131 (million) % 3.99/1.03 % (1466347)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=310629853:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 3.99/1.03 % (1466347)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.99/1.03 % (1466347)Terminated due to inappropriate strategy. % 3.99/1.03 % (1466347)------------------------------ % 3.99/1.03 % (1466347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.99/1.03 % (1466347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.99/1.03 % (1466347)CaDiCaL version: 2.1.3 % 3.99/1.03 % (1466347)Termination reason: Inappropriate % 3.99/1.03 % (1466347)Time elapsed: 0.001 s % 3.99/1.03 % (1466347)Peak memory usage: 10 MB % 3.99/1.03 % (1466347)Instructions burned: 1 (million) % 3.99/1.03 % (1466347)------------------------------ % 3.99/1.03 % (1466347)------------------------------ % 3.99/1.03 % (1466350)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=835548531:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 3.99/1.03 % (1466350)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.99/1.03 % (1466350)Terminated due to inappropriate strategy. % 3.99/1.03 % (1466350)------------------------------ % 3.99/1.03 % (1466350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.99/1.03 % (1466350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.99/1.03 % (1466350)CaDiCaL version: 2.1.3 % 3.99/1.03 % (1466350)Termination reason: Inappropriate % 3.99/1.03 % (1466350)Time elapsed: 0.001 s % 3.99/1.03 % (1466350)Peak memory usage: 10 MB % 3.99/1.03 % (1466350)Instructions burned: 1 (million) % 3.99/1.03 % (1466350)------------------------------ % 3.99/1.03 % (1466350)------------------------------ % 3.99/1.03 % (1466348)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3036831174:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 3.99/1.03 % (1466343)Instruction limit reached! % 3.99/1.03 % (1466343)------------------------------ % 3.99/1.03 % (1466343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.99/1.03 % (1466343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.99/1.03 % (1466343)CaDiCaL version: 2.1.3 % 3.99/1.03 % (1466343)Termination reason: Instruction limit % 3.99/1.03 % (1466343)Termination phase: Saturation % 3.99/1.03 % (1466343)Time elapsed: 0.081 s % 3.99/1.03 % (1466343)Peak memory usage: 12 MB % 3.99/1.03 % (1466343)Instructions burned: 182 (million) % 3.99/1.03 % (1466352)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=2121899793: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) % 17.27/2.90 % (1466354)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2966204973:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 17.27/2.90 % (1466340)Instruction limit reached! % 17.27/2.90 % (1466340)------------------------------ % 17.27/2.90 % (1466340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.27/2.90 % (1466340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.27/2.90 % (1466340)CaDiCaL version: 2.1.3 % 17.27/2.90 % (1466340)Termination reason: Instruction limit % 17.27/2.90 % (1466340)Termination phase: Saturation % 17.27/2.90 % (1466340)Time elapsed: 0.198 s % 17.27/2.90 % (1466340)Peak memory usage: 18 MB % 17.27/2.90 % (1466340)Instructions burned: 684 (million) % 17.27/2.90 % (1466357)fmb+10_1_sil=64000:random_seed=3859662458:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 17.27/2.90 % (1466357)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.27/2.90 % (1466357)Terminated due to inappropriate strategy. % 17.27/2.90 % (1466357)------------------------------ % 17.27/2.90 % (1466357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.27/2.90 % (1466357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.27/2.90 % (1466357)CaDiCaL version: 2.1.3 % 17.27/2.90 % (1466357)Termination reason: Inappropriate % 17.27/2.90 % (1466357)Time elapsed: 0.0000 s % 17.27/2.90 % (1466357)Peak memory usage: 10 MB % 17.27/2.90 % (1466357)Instructions burned: 1 (million) % 17.27/2.90 % (1466357)------------------------------ % 17.27/2.90 % (1466357)------------------------------ % 17.27/2.90 % (1466359)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=585126715:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 17.27/2.90 % (1466359)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.27/2.90 % (1466359)Terminated due to inappropriate strategy. % 17.27/2.90 % (1466359)------------------------------ % 17.27/2.90 % (1466359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.27/2.90 % (1466359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.27/2.90 % (1466359)CaDiCaL version: 2.1.3 % 17.27/2.90 % (1466359)Termination reason: Inappropriate % 17.27/2.90 % (1466359)Time elapsed: 0.0000 s % 17.27/2.90 % (1466359)Peak memory usage: 10 MB % 17.27/2.90 % (1466359)Instructions burned: 1 (million) % 17.27/2.90 % (1466359)------------------------------ % 17.27/2.90 % (1466359)------------------------------ % 17.27/2.90 % (1466361)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=188408256:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 17.27/2.90 % (1466361)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 17.27/2.90 % (1466361)Terminated due to inappropriate strategy. % 17.27/2.90 % (1466361)------------------------------ % 17.27/2.90 % (1466361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.27/2.90 % (1466361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.27/2.90 % (1466361)CaDiCaL version: 2.1.3 % 17.27/2.90 % (1466361)Termination reason: Inappropriate % 17.27/2.90 % (1466361)Time elapsed: 0.0000 s % 17.27/2.90 % (1466361)Peak memory usage: 10 MB % 17.27/2.90 % (1466361)Instructions burned: 1 (million) % 17.27/2.90 % (1466361)------------------------------ % 17.27/2.90 % (1466361)------------------------------ % 17.27/2.90 % (1466363)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=528766762:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 17.27/2.90 % (1466344)Instruction limit reached! % 17.27/2.90 % (1466344)------------------------------ % 17.27/2.90 % (1466344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 17.27/2.90 % (1466344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.27/2.90 % (1466344)CaDiCaL version: 2.1.3 % 17.27/2.90 % (1466344)Termination reason: Instruction limit % 17.27/2.90 % (1466344)Termination phase: Saturation % 17.27/2.90 % (1466344)Time elapsed: 0.263 s % 17.27/2.90 % (1466344)Peak memory usage: 13 MB % 17.27/2.90 % (1466344)Instructions burned: 478 (million) % 17.27/2.90 % (1466365)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2998989170:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 17.27/2.90 % (1466352)Instruction limit reached! % 17.27/2.90 % (1466352)------------------------------ % 27.53/4.16 % (1466352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.53/4.16 % (1466352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.53/4.16 % (1466352)CaDiCaL version: 2.1.3 % 27.53/4.16 % (1466352)Termination reason: Instruction limit % 27.53/4.16 % (1466352)Termination phase: Saturation % 27.53/4.16 % (1466352)Time elapsed: 0.424 s % 27.53/4.16 % (1466352)Peak memory usage: 18 MB % 27.53/4.16 % (1466352)Instructions burned: 693 (million) % 27.53/4.16 % (1466367)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2141035235:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 27.53/4.16 % (1466367)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.53/4.16 % (1466367)Terminated due to inappropriate strategy. % 27.53/4.16 % (1466367)------------------------------ % 27.53/4.16 % (1466367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.53/4.16 % (1466367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.53/4.16 % (1466367)CaDiCaL version: 2.1.3 % 27.53/4.16 % (1466367)Termination reason: Inappropriate % 27.53/4.16 % (1466367)Time elapsed: 0.001 s % 27.53/4.16 % (1466367)Peak memory usage: 10 MB % 27.53/4.16 % (1466367)Instructions burned: 1 (million) % 27.53/4.16 % (1466367)------------------------------ % 27.53/4.16 % (1466367)------------------------------ % 27.53/4.16 % (1466369)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1313423949:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 27.53/4.16 % (1466369)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.53/4.16 % (1466369)Terminated due to inappropriate strategy. % 27.53/4.16 % (1466369)------------------------------ % 27.53/4.16 % (1466369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.53/4.16 % (1466369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.53/4.16 % (1466369)CaDiCaL version: 2.1.3 % 27.53/4.16 % (1466369)Termination reason: Inappropriate % 27.53/4.16 % (1466369)Time elapsed: 0.001 s % 27.53/4.16 % (1466369)Peak memory usage: 10 MB % 27.53/4.16 % (1466369)Instructions burned: 1 (million) % 27.53/4.16 % (1466369)------------------------------ % 27.53/4.16 % (1466369)------------------------------ % 27.53/4.16 % (1466371)ott-2_1_sil=16000:newcnf=on:random_seed=2280832615:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 27.53/4.16 % (1466354)Instruction limit reached! % 27.53/4.16 % (1466354)------------------------------ % 27.53/4.16 % (1466354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.53/4.16 % (1466354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.53/4.16 % (1466354)CaDiCaL version: 2.1.3 % 27.53/4.16 % (1466354)Termination reason: Instruction limit % 27.53/4.16 % (1466354)Termination phase: Saturation % 27.53/4.16 % (1466354)Time elapsed: 0.496 s % 27.53/4.16 % (1466354)Peak memory usage: 18 MB % 27.53/4.16 % (1466354)Instructions burned: 879 (million) % 27.53/4.16 % (1466373)ott+10_1_sil=32000:tgt=ground:random_seed=2429197948:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 27.53/4.16 % (1466348)Instruction limit reached! % 27.53/4.16 % (1466348)------------------------------ % 27.53/4.16 % (1466348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.53/4.16 % (1466348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.53/4.16 % (1466348)CaDiCaL version: 2.1.3 % 27.53/4.16 % (1466348)Termination reason: Instruction limit % 27.53/4.16 % (1466348)Termination phase: Saturation % 27.53/4.16 % (1466348)Time elapsed: 0.575 s % 27.53/4.16 % (1466348)Peak memory usage: 22 MB % 27.53/4.16 % (1466348)Instructions burned: 1181 (million) % 27.53/4.16 % (1466375)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3253104259:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 27.53/4.16 % (1466375)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.53/4.16 % (1466375)Terminated due to inappropriate strategy. % 27.53/4.16 % (1466375)------------------------------ % 27.53/4.16 % (1466375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.53/4.16 % (1466375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.53/4.16 % (1466375)CaDiCaL version: 2.1.3 % 27.53/4.16 % (1466375)Termination reason: Inappropriate % 27.53/4.16 % (1466375)Time elapsed: 0.001 s % 27.53/4.16 % (1466375)Peak memory usage: 11 MB % 27.53/4.16 % (1466375)Instructions burned: 1 (million) % 84.33/12.18 % (1466375)------------------------------ % 84.33/12.18 % (1466375)------------------------------ % 84.33/12.18 % (1466377)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3968592844:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 84.33/12.18 % (1466371)Instruction limit reached! % 84.33/12.18 % (1466371)------------------------------ % 84.33/12.18 % (1466371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.33/12.18 % (1466371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.33/12.18 % (1466371)CaDiCaL version: 2.1.3 % 84.33/12.18 % (1466371)Termination reason: Instruction limit % 84.33/12.18 % (1466371)Termination phase: Saturation % 84.33/12.18 % (1466371)Time elapsed: 0.460 s % 84.33/12.18 % (1466371)Peak memory usage: 16 MB % 84.33/12.18 % (1466371)Instructions burned: 869 (million) % 84.33/12.18 % (1466379)dis+21_1_sil=32000:sas=cadical:random_seed=2105655924:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 84.33/12.18 % (1466365)Instruction limit reached! % 84.33/12.18 % (1466365)------------------------------ % 84.33/12.18 % (1466365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.33/12.18 % (1466365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.33/12.18 % (1466365)CaDiCaL version: 2.1.3 % 84.33/12.18 % (1466365)Termination reason: Instruction limit % 84.33/12.18 % (1466365)Termination phase: Saturation % 84.33/12.18 % (1466365)Time elapsed: 0.859 s % 84.33/12.18 % (1466365)Peak memory usage: 25 MB % 84.33/12.18 % (1466365)Instructions burned: 1473 (million) % 84.33/12.18 % (1466381)ott+11_1_sil=16000:gs=on:random_seed=3589335298:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 84.33/12.18 % (1466363)Instruction limit reached! % 84.33/12.18 % (1466363)------------------------------ % 84.33/12.18 % (1466363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.33/12.18 % (1466363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.33/12.18 % (1466363)CaDiCaL version: 2.1.3 % 84.33/12.18 % (1466363)Termination reason: Instruction limit % 84.33/12.18 % (1466363)Termination phase: Saturation % 84.33/12.18 % (1466363)Time elapsed: 1.462 s % 84.33/12.18 % (1466363)Peak memory usage: 42 MB % 84.33/12.18 % (1466363)Instructions burned: 5132 (million) % 84.33/12.18 % (1466383)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=818009778:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 84.33/12.18 % (1466383)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 84.33/12.18 % (1466383)Terminated due to inappropriate strategy. % 84.33/12.18 % (1466383)------------------------------ % 84.33/12.18 % (1466383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.33/12.18 % (1466383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.33/12.18 % (1466383)CaDiCaL version: 2.1.3 % 84.33/12.18 % (1466383)Termination reason: Inappropriate % 84.33/12.18 % (1466383)Time elapsed: 0.0000 s % 84.33/12.18 % (1466383)Peak memory usage: 10 MB % 84.33/12.18 % (1466383)Instructions burned: 1 (million) % 84.33/12.18 % (1466383)------------------------------ % 84.33/12.18 % (1466383)------------------------------ % 84.33/12.18 % (1466385)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1674241515:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 84.33/12.18 % (1466381)Instruction limit reached! % 84.33/12.18 % (1466381)------------------------------ % 84.33/12.18 % (1466381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.33/12.18 % (1466381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.33/12.18 % (1466381)CaDiCaL version: 2.1.3 % 84.33/12.18 % (1466381)Termination reason: Instruction limit % 84.33/12.18 % (1466381)Termination phase: Saturation % 84.33/12.18 % (1466381)Time elapsed: 1.221 s % 84.33/12.18 % (1466381)Peak memory usage: 23 MB % 84.33/12.18 % (1466381)Instructions burned: 2252 (million) % 84.33/12.18 % (1466387)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1572772082:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 84.33/12.18 % (1466377)Instruction limit reached! % 84.33/12.18 % (1466377)------------------------------ % 84.33/12.18 % (1466377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 84.33/12.18 % (1466377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.33/12.18 % (1466377)CaDiCaL version: 2.1.3 % 84.33/12.18 % (1466377)Termination reason: Instruction limit % 116.71/16.76 % (1466377)Termination phase: Saturation % 116.71/16.76 % (1466377)Time elapsed: 1.841 s % 116.71/16.76 % (1466377)Peak memory usage: 32 MB % 116.71/16.76 % (1466377)Instructions burned: 3512 (million) % 116.71/16.76 % (1466389)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2563170003:i=5211_2973 on theBenchmark for (2973ds/5211Mi) % 116.71/16.76 % (1466385)Instruction limit reached! % 116.71/16.76 % (1466385)------------------------------ % 116.71/16.76 % (1466385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.71/16.76 % (1466385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.71/16.76 % (1466385)CaDiCaL version: 2.1.3 % 116.71/16.76 % (1466385)Termination reason: Instruction limit % 116.71/16.76 % (1466385)Termination phase: Saturation % 116.71/16.76 % (1466385)Time elapsed: 1.274 s % 116.71/16.76 % (1466385)Peak memory usage: 48 MB % 116.71/16.76 % (1466385)Instructions burned: 4591 (million) % 116.71/16.76 % (1466391)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1953002666:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 116.71/16.76 % (1466391)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.71/16.76 % (1466391)Terminated due to inappropriate strategy. % 116.71/16.76 % (1466391)------------------------------ % 116.71/16.76 % (1466391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.71/16.76 % (1466391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.71/16.76 % (1466391)CaDiCaL version: 2.1.3 % 116.71/16.76 % (1466391)Termination reason: Inappropriate % 116.71/16.76 % (1466391)Time elapsed: 0.0000 s % 116.71/16.76 % (1466391)Peak memory usage: 10 MB % 116.71/16.76 % (1466391)Instructions burned: 1 (million) % 116.71/16.76 % (1466391)------------------------------ % 116.71/16.76 % (1466391)------------------------------ % 116.71/16.76 % (1466393)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1866394633:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 116.71/16.76 % (1466393)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.71/16.76 % (1466393)Terminated due to inappropriate strategy. % 116.71/16.76 % (1466393)------------------------------ % 116.71/16.76 % (1466393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.71/16.76 % (1466393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.71/16.76 % (1466393)CaDiCaL version: 2.1.3 % 116.71/16.76 % (1466393)Termination reason: Inappropriate % 116.71/16.76 % (1466393)Time elapsed: 0.0000 s % 116.71/16.76 % (1466393)Peak memory usage: 10 MB % 116.71/16.76 % (1466393)Instructions burned: 1 (million) % 116.71/16.76 % (1466393)------------------------------ % 116.71/16.76 % (1466393)------------------------------ % 116.71/16.76 % (1466395)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1421585584:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 116.71/16.76 % (1466395)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.71/16.76 % (1466395)Terminated due to inappropriate strategy. % 116.71/16.76 % (1466395)------------------------------ % 116.71/16.76 % (1466395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.71/16.76 % (1466395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.71/16.76 % (1466395)CaDiCaL version: 2.1.3 % 116.71/16.76 % (1466395)Termination reason: Inappropriate % 116.71/16.76 % (1466395)Time elapsed: 0.0000 s % 116.71/16.76 % (1466395)Peak memory usage: 10 MB % 116.71/16.76 % (1466395)Instructions burned: 1 (million) % 116.71/16.76 % (1466395)------------------------------ % 116.71/16.76 % (1466395)------------------------------ % 116.71/16.76 % (1466397)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2241582791:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 116.71/16.76 % (1466379)Instruction limit reached! % 116.71/16.76 % (1466379)------------------------------ % 116.71/16.76 % (1466379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.71/16.76 % (1466379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.71/16.76 % (1466379)CaDiCaL version: 2.1.3 % 116.71/16.76 % (1466379)Termination reason: Instruction limit % 116.71/16.76 % (1466379)Termination phase: Saturation % 116.71/16.76 % (1466379)Time elapsed: 2.060 s % 116.71/16.76 % (1466379)Peak memory usage: 33 MB % 116.71/16.76 % (1466379)Instructions burned: 3774 (million) % 116.71/16.76 % (1466399)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=432765530:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 116.71/16.76 % (1466373)Instruction limit reached! % 117.41/16.86 % (1466373)------------------------------ % 117.41/16.86 % (1466373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.41/16.86 % (1466373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.41/16.86 % (1466373)CaDiCaL version: 2.1.3 % 117.41/16.86 % (1466373)Termination reason: Instruction limit % 117.41/16.86 % (1466373)Termination phase: Saturation % 117.41/16.86 % (1466373)Time elapsed: 3.168 s % 117.41/16.86 % (1466373)Peak memory usage: 34 MB % 117.41/16.86 % (1466373)Instructions burned: 5114 (million) % 117.41/16.86 % (1466401)dis+10_16:1_sil=16000:random_seed=3335709767:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 117.41/16.86 % (1466389)Instruction limit reached! % 117.41/16.86 % (1466389)------------------------------ % 117.41/16.86 % (1466389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.41/16.86 % (1466389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.41/16.86 % (1466389)CaDiCaL version: 2.1.3 % 117.41/16.86 % (1466389)Termination reason: Instruction limit % 117.41/16.86 % (1466389)Termination phase: Saturation % 117.41/16.87 % (1466389)Time elapsed: 2.555 s % 117.41/16.87 % (1466389)Peak memory usage: 42 MB % 117.41/16.87 % (1466389)Instructions burned: 5211 (million) % 117.41/16.87 % (1466403)ott-3_8_sil=64000:random_seed=3720645251:i=20139:bs=on_2947 on theBenchmark for (2947ds/20139Mi) % 117.41/16.87 % (1466397)Instruction limit reached! % 117.41/16.87 % (1466397)------------------------------ % 117.41/16.87 % (1466397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.41/16.87 % (1466397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.41/16.87 % (1466397)CaDiCaL version: 2.1.3 % 117.41/16.87 % (1466397)Termination reason: Instruction limit % 117.41/16.87 % (1466397)Termination phase: Saturation % 117.41/16.87 % (1466397)Time elapsed: 4.943 s % 117.41/16.87 % (1466397)Peak memory usage: 21 MB % 117.41/16.87 % (1466397)Instructions burned: 22570 (million) % 117.41/16.87 % (1466405)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2006640060:fmbsr=2:i=32576_2919 on theBenchmark for (2919ds/32576Mi) % 117.41/16.87 % (1466405)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.41/16.87 % (1466405)Terminated due to inappropriate strategy. % 117.41/16.87 % (1466405)------------------------------ % 117.41/16.87 % (1466405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.41/16.87 % (1466405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.41/16.87 % (1466405)CaDiCaL version: 2.1.3 % 117.41/16.87 % (1466405)Termination reason: Inappropriate % 117.41/16.87 % (1466405)Time elapsed: 0.0000 s % 117.41/16.87 % (1466405)Peak memory usage: 10 MB % 117.41/16.87 % (1466405)Instructions burned: 1 (million) % 117.41/16.87 % (1466405)------------------------------ % 117.41/16.87 % (1466405)------------------------------ % 117.41/16.87 % (1466407)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2172460414:i=11404_2919 on theBenchmark for (2919ds/11404Mi) % 117.41/16.87 % (1466399)Instruction limit reached! % 117.41/16.87 % (1466399)------------------------------ % 117.41/16.87 % (1466399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.41/16.87 % (1466399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.41/16.87 % (1466399)CaDiCaL version: 2.1.3 % 117.41/16.87 % (1466399)Termination reason: Instruction limit % 117.41/16.87 % (1466399)Termination phase: Saturation % 117.41/16.87 % (1466399)Time elapsed: 5.047 s % 117.41/16.87 % (1466399)Peak memory usage: 55 MB % 117.41/16.87 % (1466399)Instructions burned: 8174 (million) % 117.41/16.87 % (1466409)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=948091038:i=14134_2917 on theBenchmark for (2917ds/14134Mi) % 117.41/16.87 % (1466401)Instruction limit reached! % 117.41/16.87 % (1466401)------------------------------ % 117.41/16.87 % (1466401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.41/16.87 % (1466401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.41/16.87 % (1466401)CaDiCaL version: 2.1.3 % 117.41/16.87 % (1466401)Termination reason: Instruction limit % 117.41/16.87 % (1466401)Termination phase: Saturation % 117.41/16.87 % (1466401)Time elapsed: 4.627 s % 117.41/16.87 % (1466401)Peak memory usage: 52 MB % 117.41/16.87 % (1466401)Instructions burned: 9156 (million) % 117.41/16.87 % (1466411)dis+33_16_sil=32000:sac=on:random_seed=3061890950:i=15851:nm=0_2914 on theBenchmark for (2914ds/15851Mi) % 117.41/16.87 % (1466407)Instruction limit reached! % 117.41/16.87 % (1466407)------------------------------ % 117.41/16.87 % (1466407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.83/18.17 % (1466407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.83/18.17 % (1466407)CaDiCaL version: 2.1.3 % 126.83/18.17 % (1466407)Termination reason: Instruction limit % 126.83/18.17 % (1466407)Termination phase: Saturation % 126.83/18.17 % (1466407)Time elapsed: 3.824 s % 126.83/18.17 % (1466407)Peak memory usage: 63 MB % 126.83/18.17 % (1466407)Instructions burned: 11409 (million) % 126.83/18.17 % (1466413)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1609611662:avsq=on:i=17627:add=on:amm=off_2880 on theBenchmark for (2880ds/17627Mi) % 126.83/18.17 % (1466387)Instruction limit reached! % 126.83/18.17 % (1466387)------------------------------ % 126.83/18.17 % (1466387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.83/18.17 % (1466387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.83/18.17 % (1466387)CaDiCaL version: 2.1.3 % 126.83/18.17 % (1466387)Termination reason: Instruction limit % 126.83/18.17 % (1466387)Termination phase: Saturation % 126.83/18.17 % (1466387)Time elapsed: 12.143 s % 126.83/18.17 % (1466387)Peak memory usage: 122 MB % 126.83/18.17 % (1466387)Instructions burned: 29340 (million) % 126.83/18.17 % (1466415)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1176343896:s2a=on:i=53295_2853 on theBenchmark for (2853ds/53295Mi) % 126.83/18.17 % (1466411)Instruction limit reached! % 126.83/18.17 % (1466411)------------------------------ % 126.83/18.17 % (1466411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.83/18.17 % (1466411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.83/18.17 % (1466411)CaDiCaL version: 2.1.3 % 126.83/18.17 % (1466411)Termination reason: Instruction limit % 126.83/18.17 % (1466411)Termination phase: Saturation % 126.83/18.17 % (1466411)Time elapsed: 7.127 s % 126.83/18.17 % (1466411)Peak memory usage: 136 MB % 126.83/18.17 % (1466411)Instructions burned: 15853 (million) % 126.83/18.17 % (1466417)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=415031682:i=26857:ins=20_2842 on theBenchmark for (2842ds/26857Mi) % 126.83/18.17 % (1466417)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.83/18.17 % (1466417)Terminated due to inappropriate strategy. % 126.83/18.17 % (1466417)------------------------------ % 126.83/18.17 % (1466417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.83/18.17 % (1466417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.83/18.17 % (1466417)CaDiCaL version: 2.1.3 % 126.83/18.17 % (1466417)Termination reason: Inappropriate % 126.83/18.17 % (1466417)Time elapsed: 0.001 s % 126.83/18.17 % (1466417)Peak memory usage: 10 MB % 126.83/18.17 % (1466417)Instructions burned: 1 (million) % 126.83/18.17 % (1466417)------------------------------ % 126.83/18.17 % (1466417)------------------------------ % 126.83/18.17 % (1466419)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4083594563:i=28120:bs=on:fsr=off_2842 on theBenchmark for (2842ds/28120Mi) % 126.83/18.17 % (1466403)Instruction limit reached! % 126.83/18.17 % (1466403)------------------------------ % 126.83/18.17 % (1466403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.83/18.17 % (1466403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.83/18.17 % (1466403)CaDiCaL version: 2.1.3 % 126.83/18.17 % (1466403)Termination reason: Instruction limit % 126.83/18.17 % (1466403)Termination phase: Saturation % 126.83/18.17 % (1466403)Time elapsed: 11.209 s % 126.83/18.17 % (1466403)Peak memory usage: 69 MB % 126.83/18.17 % (1466403)Instructions burned: 20139 (million) % 126.83/18.17 % (1466422)fmb+10_1_sil=256000:fmbss=7:random_seed=2089179645:fmbsr=1.6:i=182295_2835 on theBenchmark for (2835ds/182295Mi) % 126.83/18.17 % (1466422)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.83/18.17 % (1466422)Terminated due to inappropriate strategy. % 126.83/18.17 % (1466422)------------------------------ % 126.83/18.17 % (1466422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.83/18.17 % (1466422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.83/18.17 % (1466422)CaDiCaL version: 2.1.3 % 126.83/18.17 % (1466422)Termination reason: Inappropriate % 126.83/18.17 % (1466422)Time elapsed: 0.001 s % 126.83/18.17 % (1466422)Peak memory usage: 10 MB % 126.83/18.17 % (1466422)Instructions burned: 1 (million) % 126.83/18.17 % (1466422)------------------------------ % 126.83/18.17 % (1466422)------------------------------ % 126.83/18.17 % (1466424)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3379055951:i=44625:gsp=on_2835 on theBenchmark for (2835ds/44625Mi) % 133.27/19.11 % (1466424)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 133.27/19.11 % (1466424)Terminated due to inappropriate strategy. % 133.27/19.11 % (1466424)------------------------------ % 133.27/19.11 % (1466424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.27/19.11 % (1466424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.27/19.11 % (1466424)CaDiCaL version: 2.1.3 % 133.27/19.11 % (1466424)Termination reason: Inappropriate % 133.27/19.11 % (1466424)Time elapsed: 0.001 s % 133.27/19.11 % (1466424)Peak memory usage: 11 MB % 133.27/19.11 % (1466424)Instructions burned: 1 (million) % 133.27/19.11 % (1466424)------------------------------ % 133.27/19.11 % (1466424)------------------------------ % 133.27/19.11 % (1466426)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=275025523:i=160505_2834 on theBenchmark for (2834ds/160505Mi) % 133.27/19.11 % (1466426)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 133.27/19.11 % (1466426)Terminated due to inappropriate strategy. % 133.27/19.11 % (1466426)------------------------------ % 133.27/19.11 % (1466426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.27/19.11 % (1466426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.27/19.11 % (1466426)CaDiCaL version: 2.1.3 % 133.27/19.11 % (1466426)Termination reason: Inappropriate % 133.27/19.11 % (1466426)Time elapsed: 0.001 s % 133.27/19.11 % (1466426)Peak memory usage: 10 MB % 133.27/19.11 % (1466426)Instructions burned: 1 (million) % 133.27/19.11 % (1466426)------------------------------ % 133.27/19.11 % (1466426)------------------------------ % 133.27/19.11 % (1466428)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1202036919:fmbsr=1.3:i=225729_2834 on theBenchmark for (2834ds/225729Mi) % 133.27/19.11 % (1466428)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 133.27/19.11 % (1466428)Terminated due to inappropriate strategy. % 133.27/19.11 % (1466428)------------------------------ % 133.27/19.11 % (1466428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.27/19.11 % (1466428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.27/19.11 % (1466428)CaDiCaL version: 2.1.3 % 133.27/19.11 % (1466428)Termination reason: Inappropriate % 133.27/19.11 % (1466428)Time elapsed: 0.001 s % 133.27/19.11 % (1466428)Peak memory usage: 10 MB % 133.27/19.11 % (1466428)Instructions burned: 1 (million) % 133.27/19.11 % (1466428)------------------------------ % 133.27/19.11 % (1466428)------------------------------ % 133.27/19.11 % (1466430)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1272380260:fmbsr=2:i=185024:ins=7_2834 on theBenchmark for (2834ds/185024Mi) % 133.27/19.11 % (1466430)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 133.27/19.11 % (1466430)Terminated due to inappropriate strategy. % 133.27/19.11 % (1466430)------------------------------ % 133.27/19.11 % (1466430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.27/19.11 % (1466430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.27/19.11 % (1466430)CaDiCaL version: 2.1.3 % 133.27/19.11 % (1466430)Termination reason: Inappropriate % 133.27/19.11 % (1466430)Time elapsed: 0.001 s % 133.27/19.11 % (1466430)Peak memory usage: 10 MB % 133.27/19.11 % (1466430)Instructions burned: 1 (million) % 133.27/19.11 % (1466430)------------------------------ % 133.27/19.11 % (1466430)------------------------------ % 133.27/19.11 % (1466432)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=617173951:rtra=on_2834 on theBenchmark for (2834ds/0Mi) % 133.27/19.11 % (1466432)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 133.27/19.11 % (1466432)Terminated due to inappropriate strategy. % 133.27/19.11 % (1466432)------------------------------ % 133.27/19.11 % (1466432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 133.27/19.11 % (1466432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.27/19.11 % (1466432)CaDiCaL version: 2.1.3 % 133.27/19.11 % (1466432)Termination reason: Inappropriate % 133.27/19.11 % (1466432)Time elapsed: 0.001 s % 133.27/19.11 % (1466432)Peak memory usage: 10 MB % 133.27/19.11 % (1466432)Instructions burned: 1 (million) % 133.27/19.11 % (1466432)------------------------------ % 133.27/19.11 % (1466432)------------------------------ % 133.27/19.11 % (1466434)% WARNING: option uhcvi not known. % 133.27/19.11 % (1466434)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=954445828:i=271062:add=off:rtra=on:rawr=on_2834 on theBenchmark for (2834ds/271062Mi) % 144.57/20.73 % (1466409)Instruction limit reached! % 144.57/20.73 % (1466409)------------------------------ % 144.57/20.73 % (1466409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.57/20.73 % (1466409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.57/20.73 % (1466409)CaDiCaL version: 2.1.3 % 144.57/20.73 % (1466409)Termination reason: Instruction limit % 144.57/20.73 % (1466409)Termination phase: Saturation % 144.57/20.73 % (1466409)Time elapsed: 8.743 s % 144.57/20.73 % (1466409)Peak memory usage: 77 MB % 144.57/20.73 % (1466409)Instructions burned: 14135 (million) % 144.57/20.73 % (1466436)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=960540276:i=176048:add=on:rtra=on:rawr=on_2829 on theBenchmark for (2829ds/176048Mi) % 144.57/20.73 % (1466413)Instruction limit reached! % 144.57/20.73 % (1466413)------------------------------ % 144.57/20.73 % (1466413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.57/20.73 % (1466413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.57/20.73 % (1466413)CaDiCaL version: 2.1.3 % 144.57/20.73 % (1466413)Termination reason: Instruction limit % 144.57/20.73 % (1466413)Termination phase: Saturation % 144.57/20.73 % (1466413)Time elapsed: 5.572 s % 144.57/20.73 % (1466413)Peak memory usage: 142 MB % 144.57/20.73 % (1466413)Instructions burned: 17630 (million) % 144.57/20.73 % (1466438)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4251298856:i=206:fgj=on:rtra=on_2824 on theBenchmark for (2824ds/206Mi) % 144.57/20.73 % (1466438)Instruction limit reached! % 144.57/20.73 % (1466438)------------------------------ % 144.57/20.73 % (1466438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.57/20.73 % (1466438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.57/20.73 % (1466438)CaDiCaL version: 2.1.3 % 144.57/20.73 % (1466438)Termination reason: Instruction limit % 144.57/20.73 % (1466438)Termination phase: Saturation % 144.57/20.73 % (1466438)Time elapsed: 0.066 s % 144.57/20.73 % (1466438)Peak memory usage: 13 MB % 144.57/20.73 % (1466438)Instructions burned: 210 (million) % 144.57/20.73 % (1466440)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=25855206:i=232:rtra=on_2824 on theBenchmark for (2824ds/232Mi) % 144.57/20.73 % (1466440)Instruction limit reached! % 144.57/20.73 % (1466440)------------------------------ % 144.57/20.73 % (1466440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.57/20.73 % (1466440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.57/20.73 % (1466440)CaDiCaL version: 2.1.3 % 144.57/20.73 % (1466440)Termination reason: Instruction limit % 144.57/20.73 % (1466440)Termination phase: Saturation % 144.57/20.73 % (1466440)Time elapsed: 0.078 s % 144.57/20.73 % (1466440)Peak memory usage: 13 MB % 144.57/20.73 % (1466440)Instructions burned: 235 (million) % 144.57/20.73 % (1466442)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2364292465:i=262:rtra=on_2823 on theBenchmark for (2823ds/262Mi) % 144.57/20.73 % (1466442)Instruction limit reached! % 144.57/20.73 % (1466442)------------------------------ % 144.57/20.73 % (1466442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.57/20.73 % (1466442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.57/20.73 % (1466442)CaDiCaL version: 2.1.3 % 144.57/20.73 % (1466442)Termination reason: Instruction limit % 144.57/20.73 % (1466442)Termination phase: Saturation % 144.57/20.73 % (1466442)Time elapsed: 0.085 s % 144.57/20.73 % (1466442)Peak memory usage: 14 MB % 144.57/20.73 % (1466442)Instructions burned: 265 (million) % 144.57/20.73 % (1466444)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=626384453:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2822 on theBenchmark for (2822ds/318Mi) % 144.57/20.73 % (1466444)Instruction limit reached! % 144.57/20.73 % (1466444)------------------------------ % 144.57/20.73 % (1466444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 144.57/20.73 % (1466444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.57/20.73 % (1466444)CaDiCaL version: 2.1.3 % 144.57/20.73 % (1466444)Termination reason: Instruction limit % 144.57/20.73 % (1466444)Termination phase: Saturation % 144.57/20.73 % (1466444)Time elapsed: 0.114 s % 144.57/20.73 % (1466444)Peak memory usage: 15 MB % 144.57/20.73 % (1466444)Instructions burned: 320 (million) % 144.57/20.73 % (1466446)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2760747445:i=1428:nm=2:rtra=on_2820 on theBenchmark for (2820ds/1428Mi) % 174.90/24.92 % (1466446)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 174.90/24.92 % (1466446)Terminated due to inappropriate strategy. % 174.90/24.92 % (1466446)------------------------------ % 174.90/24.92 % (1466446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.90/24.92 % (1466446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/24.92 % (1466446)CaDiCaL version: 2.1.3 % 174.90/24.92 % (1466446)Termination reason: Inappropriate % 174.90/24.92 % (1466446)Time elapsed: 0.0000 s % 174.90/24.92 % (1466446)Peak memory usage: 10 MB % 174.90/24.92 % (1466446)Instructions burned: 1 (million) % 174.90/24.92 % (1466446)------------------------------ % 174.90/24.92 % (1466446)------------------------------ % 174.90/24.92 % (1466448)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3710580288:i=262:bd=preordered:rtra=on:fsd=on_2820 on theBenchmark for (2820ds/262Mi) % 174.90/24.92 % (1466448)Instruction limit reached! % 174.90/24.92 % (1466448)------------------------------ % 174.90/24.92 % (1466448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.90/24.92 % (1466448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/24.92 % (1466448)CaDiCaL version: 2.1.3 % 174.90/24.92 % (1466448)Termination reason: Instruction limit % 174.90/24.92 % (1466448)Termination phase: Saturation % 174.90/24.92 % (1466448)Time elapsed: 0.085 s % 174.90/24.92 % (1466448)Peak memory usage: 13 MB % 174.90/24.92 % (1466448)Instructions burned: 264 (million) % 174.90/24.92 % (1466450)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=1192945718:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2819 on theBenchmark for (2819ds/1368Mi) % 174.90/24.92 % (1466450)Instruction limit reached! % 174.90/24.92 % (1466450)------------------------------ % 174.90/24.92 % (1466450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.90/24.92 % (1466450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/24.92 % (1466450)CaDiCaL version: 2.1.3 % 174.90/24.92 % (1466450)Termination reason: Instruction limit % 174.90/24.92 % (1466450)Termination phase: Saturation % 174.90/24.92 % (1466450)Time elapsed: 0.407 s % 174.90/24.92 % (1466450)Peak memory usage: 22 MB % 174.90/24.92 % (1466450)Instructions burned: 1368 (million) % 174.90/24.92 % (1466452)ott-21_1_sil=16000:si=on:fs=off:random_seed=2738315830:i=360:av=off:fsr=off:rtra=on_2815 on theBenchmark for (2815ds/360Mi) % 174.90/24.92 % (1466452)Instruction limit reached! % 174.90/24.92 % (1466452)------------------------------ % 174.90/24.92 % (1466452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.90/24.92 % (1466452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/24.92 % (1466452)CaDiCaL version: 2.1.3 % 174.90/24.92 % (1466452)Termination reason: Instruction limit % 174.90/24.92 % (1466452)Termination phase: Saturation % 174.90/24.92 % (1466452)Time elapsed: 0.085 s % 174.90/24.92 % (1466452)Peak memory usage: 13 MB % 174.90/24.92 % (1466452)Instructions burned: 363 (million) % 174.90/24.92 % (1466454)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=611942364:i=954:bd=all:rtra=on_2814 on theBenchmark for (2814ds/954Mi) % 174.90/24.92 % (1466454)Instruction limit reached! % 174.90/24.92 % (1466454)------------------------------ % 174.90/24.92 % (1466454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.90/24.92 % (1466454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/24.92 % (1466454)CaDiCaL version: 2.1.3 % 174.90/24.92 % (1466454)Termination reason: Instruction limit % 174.90/24.92 % (1466454)Termination phase: Saturation % 174.90/24.92 % (1466454)Time elapsed: 0.303 s % 174.90/24.92 % (1466454)Peak memory usage: 15 MB % 174.90/24.92 % (1466454)Instructions burned: 956 (million) % 174.90/24.92 % (1466456)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2976800109:fmbsr=1.3:i=1730:ins=25:rtra=on_2811 on theBenchmark for (2811ds/1730Mi) % 174.90/24.92 % (1466456)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 174.90/24.92 % (1466456)Terminated due to inappropriate strategy. % 174.90/24.92 % (1466456)------------------------------ % 174.90/24.92 % (1466456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.90/24.92 % (1466456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/24.92 % (1466456)CaDiCaL version: 2.1.3 % 174.90/24.92 % (1466456)Termination reason: Inappropriate % 223.18/31.72 % (1466456)Time elapsed: 0.0000 s % 223.18/31.72 % (1466456)Peak memory usage: 10 MB % 223.18/31.72 % (1466456)Instructions burned: 1 (million) % 223.18/31.72 % (1466456)------------------------------ % 223.18/31.72 % (1466456)------------------------------ % 223.18/31.72 % (1466458)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1435483480:i=2358:rtra=on_2811 on theBenchmark for (2811ds/2358Mi) % 223.18/31.72 % (1466458)Instruction limit reached! % 223.18/31.72 % (1466458)------------------------------ % 223.18/31.72 % (1466458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.18/31.72 % (1466458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.18/31.72 % (1466458)CaDiCaL version: 2.1.3 % 223.18/31.72 % (1466458)Termination reason: Instruction limit % 223.18/31.72 % (1466458)Termination phase: Saturation % 223.18/31.72 % (1466458)Time elapsed: 0.614 s % 223.18/31.72 % (1466458)Peak memory usage: 25 MB % 223.18/31.72 % (1466458)Instructions burned: 2362 (million) % 223.18/31.72 % (1466460)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=709480564:i=1778:ins=1:rtra=on_2805 on theBenchmark for (2805ds/1778Mi) % 223.18/31.72 % (1466460)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 223.18/31.72 % (1466460)Terminated due to inappropriate strategy. % 223.18/31.72 % (1466460)------------------------------ % 223.18/31.72 % (1466460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.18/31.72 % (1466460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.18/31.72 % (1466460)CaDiCaL version: 2.1.3 % 223.18/31.72 % (1466460)Termination reason: Inappropriate % 223.18/31.72 % (1466460)Time elapsed: 0.0000 s % 223.18/31.72 % (1466460)Peak memory usage: 10 MB % 223.18/31.72 % (1466460)Instructions burned: 1 (million) % 223.18/31.72 % (1466460)------------------------------ % 223.18/31.72 % (1466460)------------------------------ % 223.18/31.72 % (1466462)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=3714484313:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2805 on theBenchmark for (2805ds/1384Mi) % 223.18/31.72 % (1466462)Instruction limit reached! % 223.18/31.72 % (1466462)------------------------------ % 223.18/31.72 % (1466462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.18/31.72 % (1466462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.18/31.72 % (1466462)CaDiCaL version: 2.1.3 % 223.18/31.72 % (1466462)Termination reason: Instruction limit % 223.18/31.72 % (1466462)Termination phase: Saturation % 223.18/31.72 % (1466462)Time elapsed: 0.407 s % 223.18/31.72 % (1466462)Peak memory usage: 22 MB % 223.18/31.72 % (1466462)Instructions burned: 1386 (million) % 223.18/31.72 % (1466464)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2455846551:i=1758:kws=inv_precedence:fsr=off:rtra=on_2800 on theBenchmark for (2800ds/1758Mi) % 223.18/31.72 % (1466464)Instruction limit reached! % 223.18/31.72 % (1466464)------------------------------ % 223.18/31.72 % (1466464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.18/31.72 % (1466464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.18/31.72 % (1466464)CaDiCaL version: 2.1.3 % 223.18/31.72 % (1466464)Termination reason: Instruction limit % 223.18/31.72 % (1466464)Termination phase: Saturation % 223.18/31.72 % (1466464)Time elapsed: 0.520 s % 223.18/31.72 % (1466464)Peak memory usage: 23 MB % 223.18/31.72 % (1466464)Instructions burned: 1758 (million) % 223.18/31.72 % (1466466)fmb+10_1_sil=64000:si=on:random_seed=2088136310:i=44122:nm=2:rtra=on:gsp=on_2795 on theBenchmark for (2795ds/44122Mi) % 223.18/31.72 % (1466466)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 223.18/31.72 % (1466466)Terminated due to inappropriate strategy. % 223.18/31.72 % (1466466)------------------------------ % 223.18/31.72 % (1466466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.18/31.72 % (1466466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.18/31.72 % (1466466)CaDiCaL version: 2.1.3 % 223.18/31.72 % (1466466)Termination reason: Inappropriate % 223.18/31.72 % (1466466)Time elapsed: 0.0000 s % 223.18/31.72 % (1466466)Peak memory usage: 10 MB % 223.18/31.72 % (1466466)Instructions burned: 2 (million) % 223.18/31.72 % (1466466)------------------------------ % 223.18/31.72 % (1466466)------------------------------ % 223.18/31.72 % (1466468)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1783095829:i=19030:nm=5:rtra=on_2795 on theBenchmark for (2795ds/19030Mi) % 231.17/35.82 % (1466468)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 231.17/35.82 % (1466468)Terminated due to inappropriate strategy. % 231.17/35.82 % (1466468)------------------------------ % 231.17/35.82 % (1466468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.17/35.82 % (1466468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.17/35.82 % (1466468)CaDiCaL version: 2.1.3 % 231.17/35.82 % (1466468)Termination reason: Inappropriate % 231.17/35.82 % (1466468)Time elapsed: 0.0000 s % 231.17/35.82 % (1466468)Peak memory usage: 10 MB % 231.17/35.82 % (1466468)Instructions burned: 1 (million) % 231.17/35.82 % (1466468)------------------------------ % 231.17/35.82 % (1466468)------------------------------ % 231.17/35.82 % (1466470)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=390565292:fmbsr=1.7:i=1840:rtra=on_2795 on theBenchmark for (2795ds/1840Mi) % 231.17/35.82 % (1466470)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 231.17/35.82 % (1466470)Terminated due to inappropriate strategy. % 231.17/35.82 % (1466470)------------------------------ % 231.17/35.82 % (1466470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.17/35.82 % (1466470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.17/35.82 % (1466470)CaDiCaL version: 2.1.3 % 231.17/35.82 % (1466470)Termination reason: Inappropriate % 231.17/35.82 % (1466470)Time elapsed: 0.0000 s % 231.17/35.82 % (1466470)Peak memory usage: 10 MB % 231.17/35.82 % (1466470)Instructions burned: 1 (million) % 231.17/35.82 % (1466470)------------------------------ % 231.17/35.82 % (1466470)------------------------------ % 231.17/35.82 % (1466472)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3557378046:i=10262:rtra=on_2795 on theBenchmark for (2795ds/10262Mi) % 231.17/35.82 % (1466472)Instruction limit reached! % 231.17/35.82 % (1466472)------------------------------ % 231.17/35.82 % (1466472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.17/35.82 % (1466472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.17/35.82 % (1466472)CaDiCaL version: 2.1.3 % 231.17/35.82 % (1466472)Termination reason: Instruction limit % 231.17/35.82 % (1466472)Termination phase: Saturation % 231.17/35.82 % (1466472)Time elapsed: 3.165 s % 231.17/35.82 % (1466472)Peak memory usage: 68 MB % 231.17/35.82 % (1466472)Instructions burned: 10263 (million) % 231.17/35.82 % (1466474)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=829876893:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2763 on theBenchmark for (2763ds/2944Mi) % 231.17/35.82 % (1466474)Instruction limit reached! % 231.17/35.82 % (1466474)------------------------------ % 231.17/35.82 % (1466474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.17/35.82 % (1466474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.17/35.82 % (1466474)CaDiCaL version: 2.1.3 % 231.17/35.82 % (1466474)Termination reason: Instruction limit % 231.17/35.82 % (1466474)Termination phase: Saturation % 231.17/35.82 % (1466474)Time elapsed: 0.961 s % 231.17/35.82 % (1466474)Peak memory usage: 29 MB % 231.17/35.82 % (1466474)Instructions burned: 2946 (million) % 231.17/35.82 % (1466476)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3012518064:i=12648:rtra=on_2753 on theBenchmark for (2753ds/12648Mi) % 231.17/35.82 % (1466476)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 231.17/35.82 % (1466476)Terminated due to inappropriate strategy. % 231.17/35.82 % (1466476)------------------------------ % 231.17/35.82 % (1466476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 231.17/35.82 % (1466476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.17/35.82 % (1466476)CaDiCaL version: 2.1.3 % 231.17/35.82 % (1466476)Termination reason: Inappropriate % 231.17/35.82 % (1466476)Time elapsed: 0.0000 s % 231.17/35.82 % (1466476)Peak memory usage: 10 MB % 231.17/35.82 % (1466476)Instructions burned: 1 (million) % 231.17/35.82 % (1466476)------------------------------ % 231.17/35.82 % (1466476)------------------------------ % 231.17/35.82 % (1466478)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1076154643:fmbsr=2.30978:i=4348:rtra=on_2753 on theBenchmark for (2753ds/4348Mi) % 231.17/35.82 % (1466478)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 231.17/35.82 % (1466478)Terminated due to inappropriate strategy. % 231.17/35.82 % (1466478)------------------------------ % 231.17/35.82 % (1466478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.55/42.64 % (1466478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.64 % (1466478)CaDiCaL version: 2.1.3 % 300.55/42.64 % (1466478)Termination reason: Inappropriate % 300.55/42.64 % (1466478)Time elapsed: 0.0000 s % 300.55/42.64 % (1466478)Peak memory usage: 10 MB % 300.55/42.64 % (1466478)Instructions burned: 1 (million) % 300.55/42.64 % (1466478)------------------------------ % 300.55/42.64 % (1466478)------------------------------ % 300.55/42.64 % (1466480)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2732076235:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2753 on theBenchmark for (2753ds/1738Mi) % 300.55/42.64 % (1466480)Instruction limit reached! % 300.55/42.64 % (1466480)------------------------------ % 300.55/42.64 % (1466480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.55/42.64 % (1466480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.64 % (1466480)CaDiCaL version: 2.1.3 % 300.55/42.64 % (1466480)Termination reason: Instruction limit % 300.55/42.64 % (1466480)Termination phase: Saturation % 300.55/42.64 % (1466480)Time elapsed: 0.569 s % 300.55/42.64 % (1466480)Peak memory usage: 24 MB % 300.55/42.64 % (1466480)Instructions burned: 1738 (million) % 300.55/42.64 % (1466482)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2401337927:i=10228:av=off:rtra=on_2747 on theBenchmark for (2747ds/10228Mi) % 300.55/42.64 % (1466419)Instruction limit reached! % 300.55/42.64 % (1466419)------------------------------ % 300.55/42.64 % (1466419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.55/42.64 % (1466419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.64 % (1466419)CaDiCaL version: 2.1.3 % 300.55/42.64 % (1466419)Termination reason: Instruction limit % 300.55/42.64 % (1466419)Termination phase: Saturation % 300.55/42.64 % (1466419)Time elapsed: 11.913 s % 300.55/42.64 % (1466419)Peak memory usage: 28 MB % 300.55/42.64 % (1466419)Instructions burned: 28120 (million) % 300.55/42.64 % (1466484)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1879120882:i=108564:rtra=on_2723 on theBenchmark for (2723ds/108564Mi) % 300.55/42.64 % (1466484)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.55/42.64 % (1466484)Terminated due to inappropriate strategy. % 300.55/42.64 % (1466484)------------------------------ % 300.55/42.64 % (1466484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.55/42.64 % (1466484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.64 % (1466484)CaDiCaL version: 2.1.3 % 300.55/42.64 % (1466484)Termination reason: Inappropriate % 300.55/42.64 % (1466484)Time elapsed: 0.001 s % 300.55/42.64 % (1466484)Peak memory usage: 10 MB % 300.55/42.64 % (1466484)Instructions burned: 1 (million) % 300.55/42.64 % (1466484)------------------------------ % 300.55/42.64 % (1466484)------------------------------ % 300.55/42.64 % (1466486)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=610764756:i=7024:aac=none:rtra=on_2723 on theBenchmark for (2723ds/7024Mi) % 300.55/42.64 % (1466482)Instruction limit reached! % 300.55/42.64 % (1466482)------------------------------ % 300.55/42.64 % (1466482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.55/42.64 % (1466482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.64 % (1466482)CaDiCaL version: 2.1.3 % 300.55/42.64 % (1466482)Termination reason: Instruction limit % 300.55/42.64 % (1466482)Termination phase: Saturation % 300.55/42.64 % (1466482)Time elapsed: 3.831 s % 300.55/42.64 % (1466482)Peak memory usage: 54 MB % 300.55/42.64 % (1466482)Instructions burned: 10230 (million) % 300.55/42.64 % (1466488)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=2790156356:i=7546:rtra=on:amm=off_2709 on theBenchmark for (2709ds/7546Mi) % 300.55/42.64 % (1466488)Instruction limit reached! % 300.55/42.64 % (1466488)------------------------------ % 300.55/42.64 % (1466488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.55/42.64 % (1466488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.55/42.64 % (1466488)CaDiCaL version: 2.1.3 % 300.55/42.64 % (1466488)Termination reason: Instruction limit % 300.55/42.64 % (1466488)Termination phase: Saturation % 300.55/42.64 % (1466488)Time elapsed: 2.341 s % 300.55/42.64 % (1466488)Peak memory usage: 49 MB % 300.55/42.64 % (1466488)Instructions burned: 7547 (million) % 300.55/42.64 % (1466490)ott+11_1_sil=16000:si=on:gs=on:random_seed=1420846908:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2685 on theB % 300.55/42.64 Terminated % 300.55/42.64 % Vampire exiting % 300.55/42.64 Terminated %------------------------------------------------------------------------------